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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namemps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-aflow40b.opb
MD5SUM64cd8dd71c00255f05a721f3d3f16ae5
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 1364
Biggest coefficient in the objective function 500
Number of bits for the biggest coefficient in the objective function 9
Sum of the numbers in the objective function 230637
Number of bits of the sum of numbers in the objective function 18
Biggest number in a constraint 102400
Number of bits of the biggest number in a constraint 17
Biggest sum of numbers in a constraint 7037881
Number of bits of the biggest sum of numbers23
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables23384
Total number of constraints4170
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)1403
Number of constraints which are nor clauses,nor cardinality constraints2767
Minimum length of a constraint1
Maximum length of a constraint1202

Trace number 3895

Launcher Data

LAUNCH ON wulflinc10 THE 2005-09-19 03:27:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2900 boxname=wulflinc10 idbench=556 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  64cd8dd71c00255f05a721f3d3f16ae5  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-aflow40b.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-aflow40b.opb
IDLAUNCH: 2900
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        863440 kB
Buffers:         36968 kB
Cached:         106896 kB
SwapCached:        228 kB
Active:          69412 kB
Inactive:        77368 kB
HighTotal:      131008 kB
HighFree:        55188 kB
LowTotal:       903652 kB
LowFree:        808252 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6272 kB
Slab:            18776 kB
Committed_AS:    64128 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 03:47:37 (client local time) WITH STATUS 0 IN 1208 SECONDS
stats: 2900 7 1208 0

Solver Data

c Parsing PB file...
c Converting 2884 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[3067]---> BDD-cost:   16
c ---[3066]---> BDD-cost:   16
c ---[3064]---> BDD-cost:   15
c ---[3063]---> BDD-cost:   16
c ---[3062]---> BDD-cost:   15
c ---[3061]---> BDD-cost:   14
c ---[3060]---> BDD-cost:   16
c ---[3059]---> BDD-cost:   16
c ---[3058]---> BDD-cost:   14
c ---[3056]---> BDD-cost:   14
c ---[3055]---> BDD-cost:   15
c ---[3053]---> BDD-cost:   16
c ---[3052]---> BDD-cost:   16
c ---[3051]---> BDD-cost:   13
c ---[3049]---> BDD-cost:   15
c ---[3048]---> BDD-cost:   16
c ---[3047]---> BDD-cost:   15
c ---[3046]---> BDD-cost:   16
c ---[3045]---> BDD-cost:   16
c ---[3044]---> BDD-cost:   16
c ---[3042]---> BDD-cost:   15
c ---[3040]---> BDD-cost:   14
c ---[3039]---> BDD-cost:   15
c ---[3038]---> BDD-cost:   15
c ---[3037]---> BDD-cost:   15
c ---[3036]---> BDD-cost:   15
c ---[3035]---> BDD-cost:   14
c ---[3034]---> BDD-cost:   14
c ---[3033]---> BDD-cost:   14
c ---[3032]---> BDD-cost:   16
c ---[3030]---> BDD-cost:   13
c ---[3028]---> BDD-cost:   14
c ---[3026]---> BDD-cost:   16
c ---[3025]---> BDD-cost:   16
c ---[3024]---> BDD-cost:   15
c ---[3023]---> BDD-cost:   16
c ---[3022]---> BDD-cost:   16
c ---[3021]---> BDD-cost:   16
c ---[3020]---> BDD-cost:   16
c ---[3019]---> BDD-cost:   15
c ---[3018]---> BDD-cost:   15
c ---[3017]---> BDD-cost:   14
c ---[3016]---> BDD-cost:   16
c ---[3015]---> BDD-cost:   16
c ---[3014]---> BDD-cost:   14
c ---[3013]---> BDD-cost:   16
c ---[3012]---> BDD-cost:   14
c ---[3011]---> BDD-cost:   14
c ---[3010]---> BDD-cost:   14
c ---[3009]---> BDD-cost:   16
c ---[3008]---> BDD-cost:   14
c ---[3007]---> BDD-cost:   16
c ---[3005]---> BDD-cost:   16
c ---[3004]---> BDD-cost:   16
c ---[3003]---> BDD-cost:   16
c ---[3002]---> BDD-cost:   15
c ---[3001]---> BDD-cost:   16
c ---[3000]---> BDD-cost:   15
c ---[2999]---> BDD-cost:   15
c ---[2998]---> BDD-cost:   15
c ---[2997]---> BDD-cost:   16
c ---[2996]---> BDD-cost:   15
c ---[2995]---> BDD-cost:   15
c ---[2994]---> BDD-cost:   16
c ---[2993]---> BDD-cost:   16
c ---[2992]---> BDD-cost:   16
c ---[2991]---> BDD-cost:   15
c ---[2990]---> BDD-cost:   16
c ---[2989]---> BDD-cost:   14
c ---[2988]---> BDD-cost:   13
c ---[2987]---> BDD-cost:   15
c ---[2986]---> BDD-cost:   15
c ---[2985]---> BDD-cost:   16
c ---[2984]---> BDD-cost:   14
c ---[2983]---> BDD-cost:   14
c ---[2982]---> BDD-cost:   16
c ---[2981]---> BDD-cost:   16
c ---[2980]---> BDD-cost:   16
c ---[2979]---> BDD-cost:   15
c ---[2978]---> BDD-cost:   15
c ---[2977]---> BDD-cost:   16
c ---[2976]---> BDD-cost:   15
c ---[2975]---> BDD-cost:   15
c ---[2974]---> BDD-cost:   16
c ---[2973]---> BDD-cost:   15
c ---[2972]---> BDD-cost:   15
c ---[2971]---> BDD-cost:   15
c ---[2969]---> BDD-cost:   16
c ---[2968]---> BDD-cost:   16
c ---[2967]---> BDD-cost:   15
c ---[2966]---> BDD-cost:   15
c ---[2965]---> BDD-cost:   15
c ---[2964]---> BDD-cost:   16
c ---[2963]---> BDD-cost:   16
c ---[2962]---> BDD-cost:   14
c ---[2961]---> BDD-cost:   16
c ---[2960]---> BDD-cost:   16
c ---[2959]---> BDD-cost:   14
c ---[2958]---> BDD-cost:   14
c ---[2955]---> BDD-cost:   16
c ---[2954]---> BDD-cost:   14
c ---[2953]---> BDD-cost:   16
c ---[2952]---> BDD-cost:   16
c ---[2951]---> BDD-cost:   15
c ---[2950]---> BDD-cost:   15
c ---[2949]---> BDD-cost:   15
c ---[2948]---> BDD-cost:   16
c ---[2947]---> BDD-cost:   15
c ---[2946]---> BDD-cost:   16
c ---[2945]---> BDD-cost:   15
c ---[2943]---> BDD-cost:   15
c ---[2942]---> BDD-cost:   16
c ---[2941]---> BDD-cost:   13
c ---[2940]---> BDD-cost:   16
c ---[2939]---> BDD-cost:   16
c ---[2938]---> BDD-cost:   16
c ---[2937]---> BDD-cost:   15
c ---[2935]---> BDD-cost:   15
c ---[2934]---> BDD-cost:   14
c ---[2933]---> BDD-cost:   16
c ---[2932]---> BDD-cost:   13
c ---[2930]---> BDD-cost:   15
c ---[2929]---> BDD-cost:   16
c ---[2928]---> BDD-cost:   16
c ---[2927]---> BDD-cost:   16
c ---[2926]---> BDD-cost:   16
c ---[2925]---> BDD-cost:   14
c ---[2924]---> BDD-cost:   16
c ---[2923]---> BDD-cost:   15
c ---[2922]---> BDD-cost:   16
c ---[2921]---> BDD-cost:   16
c ---[2919]---> BDD-cost:   15
c ---[2918]---> BDD-cost:   16
c ---[2917]---> BDD-cost:   15
c ---[2916]---> BDD-cost:   16
c ---[2915]---> BDD-cost:   13
c ---[2914]---> BDD-cost:   16
c ---[2913]---> BDD-cost:   15
c ---[2912]---> BDD-cost:   16
c ---[2911]---> BDD-cost:   14
c ---[2909]---> BDD-cost:   16
c ---[2907]---> BDD-cost:   16
c ---[2906]---> BDD-cost:   16
c ---[2905]---> BDD-cost:   14
c ---[2904]---> BDD-cost:   14
c ---[2902]---> BDD-cost:   16
c ---[2901]---> BDD-cost:   16
c ---[2900]---> BDD-cost:   16
c ---[2899]---> BDD-cost:   15
c ---[2898]---> BDD-cost:   16
c ---[2897]---> BDD-cost:   16
c ---[2896]---> BDD-cost:   15
c ---[2895]---> BDD-cost:   16
c ---[2894]---> BDD-cost:   14
c ---[2893]---> BDD-cost:   16
c ---[2892]---> BDD-cost:   16
c ---[2890]---> BDD-cost:   16
c ---[2889]---> BDD-cost:   15
c ---[2888]---> BDD-cost:   16
c ---[2887]---> BDD-cost:   13
c ---[2886]---> BDD-cost:   16
c ---[2884]---> BDD-cost:   16
c ---[2882]---> BDD-cost:   15
c ---[2881]---> BDD-cost:   16
c ---[2879]---> BDD-cost:   14
c ---[2877]---> BDD-cost:   15
c ---[2876]---> BDD-cost:   16
c ---[2875]---> BDD-cost:   16
c ---[2874]---> BDD-cost:   16
c ---[2873]---> BDD-cost:   16
c ---[2872]---> BDD-cost:   16
c ---[2871]---> BDD-cost:   16
c ---[2870]---> BDD-cost:   15
c ---[2869]---> BDD-cost:   16
c ---[2868]---> BDD-cost:   15
c ---[2866]---> BDD-cost:   16
c ---[2865]---> BDD-cost:   16
c ---[2864]---> BDD-cost:   14
c ---[2863]---> BDD-cost:   14
c ---[2862]---> BDD-cost:   14
c ---[2861]---> BDD-cost:   15
c ---[2860]---> BDD-cost:   15
c ---[2859]---> BDD-cost:   16
c ---[2858]---> BDD-cost:   16
c ---[2856]---> BDD-cost:   16
c ---[2855]---> BDD-cost:   15
c ---[2854]---> BDD-cost:   15
c ---[2853]---> BDD-cost:   15
c ---[2852]---> BDD-cost:   13
c ---[2851]---> BDD-cost:   14
c ---[2850]---> BDD-cost:   13
c ---[2849]---> BDD-cost:   15
c ---[2847]---> BDD-cost:   15
c ---[2846]---> BDD-cost:   13
c ---[2845]---> BDD-cost:   16
c ---[2844]---> BDD-cost:   16
c ---[2843]---> BDD-cost:   14
c ---[2842]---> BDD-cost:   16
c ---[2841]---> BDD-cost:   16
c ---[2840]---> BDD-cost:   16
c ---[2839]---> BDD-cost:   16
c ---[2838]---> BDD-cost:   15
c ---[2837]---> BDD-cost:   14
c ---[2836]---> BDD-cost:   14
c ---[2835]---> BDD-cost:   15
c ---[2834]---> BDD-cost:   16
c ---[2833]---> BDD-cost:   15
c ---[2832]---> BDD-cost:   14
c ---[2831]---> BDD-cost:   14
c ---[2830]---> BDD-cost:   15
c ---[2829]---> BDD-cost:   16
c ---[2828]---> BDD-cost:   14
c ---[2827]---> BDD-cost:   14
c ---[2826]---> BDD-cost:   16
c ---[2825]---> BDD-cost:   16
c ---[2824]---> BDD-cost:   14
c ---[2823]---> BDD-cost:   15
c ---[2822]---> BDD-cost:   16
c ---[2821]---> BDD-cost:   13
c ---[2820]---> BDD-cost:   16
c ---[2819]---> BDD-cost:   16
c ---[2817]---> BDD-cost:   16
c ---[2816]---> BDD-cost:   15
c ---[2815]---> BDD-cost:   13
c ---[2814]---> BDD-cost:   15
c ---[2813]---> BDD-cost:   15
c ---[2812]---> BDD-cost:   16
c ---[2811]---> BDD-cost:   14
c ---[2810]---> BDD-cost:   16
c ---[2808]---> BDD-cost:   16
c ---[2806]---> BDD-cost:   15
c ---[2805]---> BDD-cost:   14
c ---[2803]---> BDD-cost:   14
c ---[2802]---> BDD-cost:   16
c ---[2801]---> BDD-cost:   15
c ---[2800]---> BDD-cost:   16
c ---[2797]---> BDD-cost:   16
c ---[2796]---> BDD-cost:   15
c ---[2795]---> BDD-cost:   13
c ---[2794]---> BDD-cost:   16
c ---[2793]---> BDD-cost:   16
c ---[2792]---> BDD-cost:   16
c ---[2791]---> BDD-cost:   14
c ---[2790]---> BDD-cost:   16
c ---[2789]---> BDD-cost:   16
c ---[2788]---> BDD-cost:   16
c ---[2787]---> BDD-cost:   14
c ---[2786]---> BDD-cost:   16
c ---[2785]---> BDD-cost:   14
c ---[2784]---> BDD-cost:   15
c ---[2783]---> BDD-cost:   13
c ---[2781]---> BDD-cost:   16
c ---[2780]---> BDD-cost:   16
c ---[2779]---> BDD-cost:   15
c ---[2778]---> BDD-cost:   15
c ---[2777]---> BDD-cost:   16
c ---[2776]---> BDD-cost:   16
c ---[2775]---> BDD-cost:   16
c ---[2774]---> BDD-cost:   16
c ---[2773]---> BDD-cost:   16
c ---[2772]---> BDD-cost:   16
c ---[2771]---> BDD-cost:   16
c ---[2769]---> BDD-cost:   16
c ---[2768]---> BDD-cost:   16
c ---[2767]---> BDD-cost:   14
c ---[2766]---> BDD-cost:   15
c ---[2765]---> BDD-cost:   15
c ---[2764]---> BDD-cost:   16
c ---[2763]---> BDD-cost:   16
c ---[2762]---> BDD-cost:   16
c ---[2761]---> BDD-cost:   15
c ---[2760]---> BDD-cost:   15
c ---[2759]---> BDD-cost:   15
c ---[2758]---> BDD-cost:   16
c ---[2757]---> BDD-cost:   15
c ---[2756]---> BDD-cost:   16
c ---[2755]---> BDD-cost:   15
c ---[2754]---> BDD-cost:   16
c ---[2753]---> BDD-cost:   16
c ---[2752]---> BDD-cost:   13
c ---[2751]---> BDD-cost:   16
c ---[2750]---> BDD-cost:   14
c ---[2748]---> BDD-cost:   13
c ---[2747]---> BDD-cost:   16
c ---[2746]---> BDD-cost:   16
c ---[2744]---> BDD-cost:   13
c ---[2743]---> BDD-cost:   15
c ---[2742]---> BDD-cost:   16
c ---[2741]---> BDD-cost:   16
c ---[2740]---> BDD-cost:   16
c ---[2739]---> BDD-cost:   15
c ---[2737]---> BDD-cost:   16
c ---[2736]---> BDD-cost:   16
c ---[2735]---> BDD-cost:   15
c ---[2734]---> BDD-cost:   14
c ---[2733]---> BDD-cost:   16
c ---[2732]---> BDD-cost:   16
c ---[2731]---> BDD-cost:   16
c ---[2730]---> BDD-cost:   16
c ---[2728]---> BDD-cost:   16
c ---[2727]---> BDD-cost:   16
c ---[2726]---> BDD-cost:   16
c ---[2724]---> BDD-cost:   16
c ---[2723]---> BDD-cost:   15
c ---[2722]---> BDD-cost:   16
c ---[2721]---> BDD-cost:   16
c ---[2720]---> BDD-cost:   16
c ---[2719]---> BDD-cost:   15
c ---[2718]---> BDD-cost:   16
c ---[2717]---> BDD-cost:   14
c ---[2716]---> BDD-cost:   16
c ---[2715]---> BDD-cost:   15
c ---[2714]---> BDD-cost:   16
c ---[2712]---> BDD-cost:   16
c ---[2710]---> BDD-cost:   16
c ---[2709]---> BDD-cost:   16
c ---[2708]---> BDD-cost:   13
c ---[2706]---> BDD-cost:   16
c ---[2705]---> BDD-cost:   16
c ---[2704]---> BDD-cost:   15
c ---[2703]---> BDD-cost:   16
c ---[2701]---> BDD-cost:   16
c ---[2700]---> BDD-cost:   15
c ---[2699]---> BDD-cost:   15
c ---[2698]---> BDD-cost:   16
c ---[2697]---> BDD-cost:   16
c ---[2696]---> BDD-cost:   16
c ---[2695]---> BDD-cost:   16
c ---[2694]---> BDD-cost:   16
c ---[2693]---> BDD-cost:   16
c ---[2692]---> BDD-cost:   16
c ---[2691]---> BDD-cost:   14
c ---[2690]---> BDD-cost:   16
c ---[2689]---> BDD-cost:   15
c ---[2688]---> BDD-cost:   16
c ---[2687]---> BDD-cost:   16
c ---[2686]---> BDD-cost:   15
c ---[2685]---> BDD-cost:   15
c ---[2684]---> BDD-cost:   16
c ---[2683]---> BDD-cost:   16
c ---[2682]---> BDD-cost:   16
c ---[2681]---> BDD-cost:   14
c ---[2680]---> BDD-cost:   14
c ---[2679]---> BDD-cost:   16
c ---[2678]---> BDD-cost:   15
c ---[2677]---> BDD-cost:   15
c ---[2675]---> BDD-cost:   16
c ---[2674]---> BDD-cost:   16
c ---[2673]---> BDD-cost:   16
c ---[2672]---> BDD-cost:   15
c ---[2671]---> BDD-cost:   14
c ---[2670]---> BDD-cost:   15
c ---[2669]---> BDD-cost:   16
c ---[2668]---> BDD-cost:   13
c ---[2667]---> BDD-cost:   16
c ---[2665]---> BDD-cost:   15
c ---[2664]---> BDD-cost:   14
c ---[2662]---> BDD-cost:   16
c ---[2661]---> BDD-cost:   14
c ---[2660]---> BDD-cost:   14
c ---[2659]---> BDD-cost:   16
c ---[2658]---> BDD-cost:   15
c ---[2656]---> BDD-cost:   16
c ---[2654]---> BDD-cost:   16
c ---[2653]---> BDD-cost:   14
c ---[2652]---> BDD-cost:   15
c ---[2651]---> BDD-cost:   16
c ---[2650]---> BDD-cost:   15
c ---[2648]---> BDD-cost:   15
c ---[2647]---> BDD-cost:   14
c ---[2646]---> BDD-cost:   13
c ---[2645]---> BDD-cost:   15
c ---[2644]---> BDD-cost:   15
c ---[2643]---> BDD-cost:   15
c ---[2642]---> BDD-cost:   15
c ---[2641]---> BDD-cost:   16
c ---[2638]---> BDD-cost:   16
c ---[2637]---> BDD-cost:   15
c ---[2636]---> BDD-cost:   14
c ---[2635]---> BDD-cost:   14
c ---[2634]---> BDD-cost:   13
c ---[2633]---> BDD-cost:   16
c ---[2632]---> BDD-cost:   14
c ---[2631]---> BDD-cost:   15
c ---[2630]---> BDD-cost:   16
c ---[2629]---> BDD-cost:   14
c ---[2628]---> BDD-cost:   15
c ---[2627]---> BDD-cost:   16
c ---[2626]---> BDD-cost:   16
c ---[2625]---> BDD-cost:   15
c ---[2624]---> BDD-cost:   15
c ---[2623]---> BDD-cost:   16
c ---[2622]---> BDD-cost:   16
c ---[2621]---> BDD-cost:   16
c ---[2620]---> BDD-cost:   16
c ---[2619]---> BDD-cost:   14
c ---[2618]---> BDD-cost:   16
c ---[2617]---> BDD-cost:   15
c ---[2616]---> BDD-cost:   16
c ---[2615]---> BDD-cost:   16
c ---[2614]---> BDD-cost:   16
c ---[2613]---> BDD-cost:   15
c ---[2612]---> BDD-cost:   16
c ---[2611]---> BDD-cost:   16
c ---[2610]---> BDD-cost:   15
c ---[2609]---> BDD-cost:   15
c ---[2608]---> BDD-cost:   15
c ---[2606]---> BDD-cost:   15
c ---[2604]---> BDD-cost:   14
c ---[2603]---> BDD-cost:   15
c ---[2602]---> BDD-cost:   16
c ---[2601]---> BDD-cost:   16
c ---[2600]---> BDD-cost:   14
c ---[2599]---> BDD-cost:   16
c ---[2598]---> BDD-cost:   16
c ---[2597]---> BDD-cost:   14
c ---[2596]---> BDD-cost:   16
c ---[2595]---> BDD-cost:   16
c ---[2594]---> BDD-cost:   15
c ---[2593]---> BDD-cost:   16
c ---[2592]---> BDD-cost:   14
c ---[2591]---> BDD-cost:   16
c ---[2590]---> BDD-cost:   15
c ---[2589]---> BDD-cost:   16
c ---[2587]---> BDD-cost:   15
c ---[2586]---> BDD-cost:   16
c ---[2584]---> BDD-cost:   15
c ---[2583]---> BDD-cost:   16
c ---[2582]---> BDD-cost:   16
c ---[2581]---> BDD-cost:   16
c ---[2580]---> BDD-cost:   13
c ---[2579]---> BDD-cost:   14
c ---[2576]---> BDD-cost:   16
c ---[2575]---> BDD-cost:   16
c ---[2574]---> BDD-cost:   16
c ---[2572]---> BDD-cost:   14
c ---[2571]---> BDD-cost:   16
c ---[2570]---> BDD-cost:   16
c ---[2569]---> BDD-cost:   14
c ---[2568]---> BDD-cost:   16
c ---[2567]---> BDD-cost:   13
c ---[2566]---> BDD-cost:   15
c ---[2565]---> BDD-cost:   15
c ---[2564]---> BDD-cost:   16
c ---[2563]---> BDD-cost:   16
c ---[2562]---> BDD-cost:   16
c ---[2561]---> BDD-cost:   15
c ---[2559]---> BDD-cost:   15
c ---[2558]---> BDD-cost:   15
c ---[2557]---> BDD-cost:   16
c ---[2556]---> BDD-cost:   16
c ---[2554]---> BDD-cost:   14
c ---[2553]---> BDD-cost:   15
c ---[2550]---> BDD-cost:   15
c ---[2549]---> BDD-cost:   15
c ---[2548]---> BDD-cost:   14
c ---[2546]---> BDD-cost:   16
c ---[2545]---> BDD-cost:   13
c ---[2543]---> BDD-cost:   15
c ---[2541]---> BDD-cost:   16
c ---[2540]---> BDD-cost:   14
c ---[2539]---> BDD-cost:   16
c ---[2538]---> BDD-cost:   16
c ---[2537]---> BDD-cost:   16
c ---[2535]---> BDD-cost:   15
c ---[2533]---> BDD-cost:   15
c ---[2532]---> BDD-cost:   16
c ---[2531]---> BDD-cost:   14
c ---[2530]---> BDD-cost:   16
c ---[2529]---> BDD-cost:   15
c ---[2528]---> BDD-cost:   16
c ---[2527]---> BDD-cost:   16
c ---[2526]---> BDD-cost:   15
c ---[2524]---> BDD-cost:   16
c ---[2523]---> BDD-cost:   15
c ---[2522]---> BDD-cost:   16
c ---[2520]---> BDD-cost:   13
c ---[2519]---> BDD-cost:   15
c ---[2518]---> BDD-cost:   15
c ---[2517]---> BDD-cost:   16
c ---[2516]---> BDD-cost:   16
c ---[2515]---> BDD-cost:   15
c ---[2514]---> BDD-cost:   15
c ---[2513]---> BDD-cost:   15
c ---[2512]---> BDD-cost:   15
c ---[2511]---> BDD-cost:   16
c ---[2510]---> BDD-cost:   14
c ---[2509]---> BDD-cost:   16
c ---[2507]---> BDD-cost:   15
c ---[2506]---> BDD-cost:   15
c ---[2505]---> BDD-cost:   15
c ---[2504]---> BDD-cost:   16
c ---[2503]---> BDD-cost:   15
c ---[2502]---> BDD-cost:   16
c ---[2499]---> BDD-cost:   14
c ---[2498]---> BDD-cost:   16
c ---[2497]---> BDD-cost:   16
c ---[2495]---> BDD-cost:   16
c ---[2491]---> BDD-cost:   16
c ---[2489]---> BDD-cost:   15
c ---[2488]---> BDD-cost:   15
c ---[2484]---> BDD-cost:   15
c ---[2483]---> BDD-cost:   16
c ---[2482]---> BDD-cost:   16
c ---[2481]---> BDD-cost:   14
c ---[2479]---> BDD-cost:   13
c ---[2477]---> BDD-cost:   15
c ---[2476]---> BDD-cost:   16
c ---[2475]---> BDD-cost:   16
c ---[2474]---> BDD-cost:   16
c ---[2473]---> BDD-cost:   14
c ---[2472]---> BDD-cost:   16
c ---[2471]---> BDD-cost:   15
c ---[2470]---> BDD-cost:   16
c ---[2469]---> BDD-cost:   15
c ---[2468]---> BDD-cost:   15
c ---[2467]---> BDD-cost:   15
c ---[2466]---> BDD-cost:   16
c ---[2464]---> BDD-cost:   14
c ---[2463]---> BDD-cost:   15
c ---[2462]---> BDD-cost:   15
c ---[2460]---> BDD-cost:   14
c ---[2459]---> BDD-cost:   16
c ---[2457]---> BDD-cost:   14
c ---[2456]---> BDD-cost:   14
c ---[2454]---> BDD-cost:   16
c ---[2453]---> BDD-cost:   13
c ---[2451]---> BDD-cost:   16
c ---[2450]---> BDD-cost:   16
c ---[2449]---> BDD-cost:   16
c ---[2447]---> BDD-cost:   15
c ---[2446]---> BDD-cost:   16
c ---[2445]---> BDD-cost:   15
c ---[2444]---> BDD-cost:   13
c ---[2443]---> BDD-cost:   16
c ---[2442]---> BDD-cost:   16
c ---[2440]---> BDD-cost:   15
c ---[2439]---> BDD-cost:   16
c ---[2438]---> BDD-cost:   15
c ---[2437]---> BDD-cost:   15
c ---[2436]---> BDD-cost:   14
c ---[2435]---> BDD-cost:   16
c ---[2434]---> BDD-cost:   16
c ---[2433]---> BDD-cost:   16
c ---[2432]---> BDD-cost:   16
c ---[2431]---> BDD-cost:   16
c ---[2430]---> BDD-cost:   15
c ---[2429]---> BDD-cost:   16
c ---[2428]---> BDD-cost:   15
c ---[2427]---> BDD-cost:   16
c ---[2426]---> BDD-cost:   16
c ---[2425]---> BDD-cost:   15
c ---[2424]---> BDD-cost:   16
c ---[2423]---> BDD-cost:   14
c ---[2422]---> BDD-cost:   15
c ---[2421]---> BDD-cost:   13
c ---[2419]---> BDD-cost:   14
c ---[2418]---> BDD-cost:   14
c ---[2417]---> BDD-cost:   15
c ---[2416]---> BDD-cost:   16
c ---[2415]---> BDD-cost:   15
c ---[2413]---> BDD-cost:   15
c ---[2412]---> BDD-cost:   16
c ---[2410]---> BDD-cost:   16
c ---[2409]---> BDD-cost:   16
c ---[2408]---> BDD-cost:   14
c ---[2407]---> BDD-cost:   16
c ---[2406]---> BDD-cost:   14
c ---[2405]---> BDD-cost:   16
c ---[2404]---> BDD-cost:   15
c ---[2403]---> BDD-cost:   16
c ---[2402]---> BDD-cost:   14
c ---[2401]---> BDD-cost:   16
c ---[2400]---> BDD-cost:   15
c ---[2399]---> BDD-cost:   16
c ---[2398]---> BDD-cost:   13
c ---[2397]---> BDD-cost:   15
c ---[2396]---> BDD-cost:   15
c ---[2395]---> BDD-cost:   16
c ---[2394]---> BDD-cost:   15
c ---[2393]---> BDD-cost:   13
c ---[2392]---> BDD-cost:   16
c ---[2390]---> BDD-cost:   15
c ---[2389]---> BDD-cost:   14
c ---[2388]---> BDD-cost:   16
c ---[2387]---> BDD-cost:   14
c ---[2386]---> BDD-cost:   16
c ---[2385]---> BDD-cost:   15
c ---[2384]---> BDD-cost:   16
c ---[2383]---> BDD-cost:   16
c ---[2382]---> BDD-cost:   16
c ---[2381]---> BDD-cost:   13
c ---[2379]---> BDD-cost:   15
c ---[2378]---> BDD-cost:   15
c ---[2377]---> BDD-cost:   16
c ---[2376]---> BDD-cost:   16
c ---[2375]---> BDD-cost:   14
c ---[2374]---> BDD-cost:   15
c ---[2373]---> BDD-cost:   15
c ---[2372]---> BDD-cost:   15
c ---[2371]---> BDD-cost:   15
c ---[2370]---> BDD-cost:   13
c ---[2369]---> BDD-cost:   16
c ---[2367]---> BDD-cost:   15
c ---[2366]---> BDD-cost:   16
c ---[2365]---> BDD-cost:   16
c ---[2364]---> BDD-cost:   13
c ---[2363]---> BDD-cost:   16
c ---[2362]---> BDD-cost:   14
c ---[2361]---> BDD-cost:   16
c ---[2360]---> BDD-cost:   15
c ---[2359]---> BDD-cost:   15
c ---[2358]---> BDD-cost:   15
c ---[2357]---> BDD-cost:   16
c ---[2356]---> BDD-cost:   16
c ---[2354]---> BDD-cost:   14
c ---[2353]---> BDD-cost:   16
c ---[2352]---> BDD-cost:   16
c ---[2350]---> BDD-cost:   16
c ---[2348]---> BDD-cost:   13
c ---[2347]---> BDD-cost:   14
c ---[2346]---> BDD-cost:   16
c ---[2345]---> BDD-cost:   16
c ---[2344]---> BDD-cost:   16
c ---[2342]---> BDD-cost:   16
c ---[2341]---> BDD-cost:   16
c ---[2340]---> BDD-cost:   16
c ---[2338]---> BDD-cost:   16
c ---[2337]---> BDD-cost:   15
c ---[2336]---> BDD-cost:   16
c ---[2334]---> BDD-cost:   16
c ---[2333]---> BDD-cost:   16
c ---[2332]---> BDD-cost:   13
c ---[2331]---> BDD-cost:   15
c ---[2330]---> BDD-cost:   16
c ---[2329]---> BDD-cost:   16
c ---[2328]---> BDD-cost:   16
c ---[2327]---> BDD-cost:   16
c ---[2324]---> BDD-cost:   14
c ---[2321]---> BDD-cost:   16
c ---[2320]---> BDD-cost:   15
c ---[2319]---> BDD-cost:   16
c ---[2318]---> BDD-cost:   16
c ---[2317]---> BDD-cost:   16
c ---[2315]---> BDD-cost:   16
c ---[2314]---> BDD-cost:   14
c ---[2313]---> BDD-cost:   15
c ---[2312]---> BDD-cost:   16
c ---[2311]---> BDD-cost:   15
c ---[2310]---> BDD-cost:   15
c ---[2309]---> BDD-cost:   14
c ---[2307]---> BDD-cost:   16
c ---[2306]---> BDD-cost:   13
c ---[2305]---> BDD-cost:   13
c ---[2304]---> BDD-cost:   16
c ---[2303]---> BDD-cost:   16
c ---[2302]---> BDD-cost:   16
c ---[2301]---> BDD-cost:   16
c ---[2300]---> BDD-cost:   15
c ---[2299]---> BDD-cost:   15
c ---[2298]---> BDD-cost:   14
c ---[2297]---> BDD-cost:   13
c ---[2296]---> BDD-cost:   16
c ---[2294]---> BDD-cost:   15
c ---[2293]---> BDD-cost:   16
c ---[2292]---> BDD-cost:   15
c ---[2291]---> BDD-cost:   14
c ---[2290]---> BDD-cost:   15
c ---[2289]---> BDD-cost:   16
c ---[2288]---> BDD-cost:   14
c ---[2287]---> BDD-cost:   14
c ---[2286]---> BDD-cost:   15
c ---[2285]---> BDD-cost:   15
c ---[2284]---> BDD-cost:   16
c ---[2283]---> BDD-cost:   16
c ---[2282]---> BDD-cost:   14
c ---[2281]---> BDD-cost:   14
c ---[2280]---> BDD-cost:   15
c ---[2279]---> BDD-cost:   16
c ---[2277]---> BDD-cost:   15
c ---[2276]---> BDD-cost:   16
c ---[2275]---> BDD-cost:   16
c ---[2274]---> BDD-cost:   15
c ---[2273]---> BDD-cost:   16
c ---[2272]---> BDD-cost:   15
c ---[2271]---> BDD-cost:   15
c ---[2268]---> BDD-cost:   16
c ---[2267]---> BDD-cost:   14
c ---[2265]---> BDD-cost:   16
c ---[2264]---> BDD-cost:   15
c ---[2263]---> BDD-cost:   15
c ---[2262]---> BDD-cost:   13
c ---[2260]---> BDD-cost:   15
c ---[2259]---> BDD-cost:   15
c ---[2258]---> BDD-cost:   16
c ---[2257]---> BDD-cost:   15
c ---[2256]---> BDD-cost:   15
c ---[2255]---> BDD-cost:   16
c ---[2254]---> BDD-cost:   14
c ---[2253]---> BDD-cost:   16
c ---[2252]---> BDD-cost:   16
c ---[2251]---> BDD-cost:   15
c ---[2250]---> BDD-cost:   16
c ---[2249]---> BDD-cost:   16
c ---[2248]---> BDD-cost:   14
c ---[2247]---> BDD-cost:   15
c ---[2246]---> BDD-cost:   14
c ---[2245]---> BDD-cost:   15
c ---[2244]---> BDD-cost:   16
c ---[2243]---> BDD-cost:   16
c ---[2242]---> BDD-cost:   15
c ---[2241]---> BDD-cost:   16
c ---[2240]---> BDD-cost:   15
c ---[2239]---> BDD-cost:   16
c ---[2238]---> BDD-cost:   16
c ---[2237]---> BDD-cost:   15
c ---[2236]---> BDD-cost:   16
c ---[2235]---> BDD-cost:   14
c ---[2234]---> BDD-cost:   16
c ---[2233]---> BDD-cost:   16
c ---[2232]---> BDD-cost:   16
c ---[2231]---> BDD-cost:   15
c ---[2230]---> BDD-cost:   16
c ---[2229]---> BDD-cost:   14
c ---[2228]---> BDD-cost:   16
c ---[2226]---> BDD-cost:   15
c ---[2225]---> BDD-cost:   15
c ---[2224]---> BDD-cost:   15
c ---[2223]---> BDD-cost:   16
c ---[2222]---> BDD-cost:   16
c ---[2221]---> BDD-cost:   16
c ---[2220]---> BDD-cost:   15
c ---[2219]---> BDD-cost:   15
c ---[2218]---> BDD-cost:   13
c ---[2217]---> BDD-cost:   16
c ---[2216]---> BDD-cost:   16
c ---[2215]---> BDD-cost:   15
c ---[2214]---> BDD-cost:   15
c ---[2213]---> BDD-cost:   14
c ---[2212]---> BDD-cost:   13
c ---[2211]---> BDD-cost:   16
c ---[2210]---> BDD-cost:   16
c ---[2208]---> BDD-cost:   13
c ---[2207]---> BDD-cost:   15
c ---[2206]---> BDD-cost:   15
c ---[2205]---> BDD-cost:   16
c ---[2204]---> BDD-cost:   15
c ---[2203]---> BDD-cost:   16
c ---[2202]---> BDD-cost:   16
c ---[2200]---> BDD-cost:   16
c ---[2199]---> BDD-cost:   16
c ---[2198]---> BDD-cost:   14
c ---[2195]---> BDD-cost:   16
c ---[2194]---> BDD-cost:   13
c ---[2193]---> BDD-cost:   15
c ---[2192]---> BDD-cost:   14
c ---[2191]---> BDD-cost:   15
c ---[2190]---> BDD-cost:   16
c ---[2189]---> BDD-cost:   15
c ---[2188]---> BDD-cost:   16
c ---[2187]---> BDD-cost:   16
c ---[2186]---> BDD-cost:   16
c ---[2184]---> BDD-cost:   13
c ---[2182]---> BDD-cost:   16
c ---[2181]---> BDD-cost:   16
c ---[2180]---> BDD-cost:   14
c ---[2179]---> BDD-cost:   15
c ---[2178]---> BDD-cost:   16
c ---[2177]---> BDD-cost:   16
c ---[2175]---> BDD-cost:   16
c ---[2173]---> BDD-cost:   13
c ---[2172]---> BDD-cost:   15
c ---[2171]---> BDD-cost:   16
c ---[2170]---> BDD-cost:   14
c ---[2168]---> BDD-cost:   16
c ---[2167]---> BDD-cost:   15
c ---[2166]---> BDD-cost:   16
c ---[2165]---> BDD-cost:   16
c ---[2164]---> BDD-cost:   16
c ---[2163]---> BDD-cost:   16
c ---[2162]---> BDD-cost:   15
c ---[2161]---> BDD-cost:   15
c ---[2159]---> BDD-cost:   14
c ---[2158]---> BDD-cost:   15
c ---[2157]---> BDD-cost:   15
c ---[2155]---> BDD-cost:   15
c ---[2154]---> BDD-cost:   16
c ---[2153]---> BDD-cost:   16
c ---[2152]---> BDD-cost:   15
c ---[2151]---> BDD-cost:   16
c ---[2150]---> BDD-cost:   16
c ---[2149]---> BDD-cost:   16
c ---[2148]---> BDD-cost:   14
c ---[2147]---> BDD-cost:   14
c ---[2146]---> BDD-cost:   16
c ---[2145]---> BDD-cost:   16
c ---[2144]---> BDD-cost:   16
c ---[2143]---> BDD-cost:   16
c ---[2142]---> BDD-cost:   16
c ---[2141]---> BDD-cost:   13
c ---[2140]---> BDD-cost:   15
c ---[2139]---> BDD-cost:   13
c ---[2137]---> BDD-cost:   15
c ---[2136]---> BDD-cost:   16
c ---[2135]---> BDD-cost:   16
c ---[2134]---> BDD-cost:   16
c ---[2133]---> BDD-cost:   15
c ---[2132]---> BDD-cost:   15
c ---[2131]---> BDD-cost:   15
c ---[2130]---> BDD-cost:   15
c ---[2129]---> BDD-cost:   15
c ---[2128]---> BDD-cost:   16
c ---[2127]---> BDD-cost:   16
c ---[2126]---> BDD-cost:   15
c ---[2124]---> BDD-cost:   16
c ---[2123]---> BDD-cost:   15
c ---[2122]---> BDD-cost:   14
c ---[2121]---> BDD-cost:   13
c ---[2120]---> BDD-cost:   16
c ---[2119]---> BDD-cost:   15
c ---[2118]---> BDD-cost:   15
c ---[2117]---> BDD-cost:   14
c ---[2116]---> BDD-cost:   16
c ---[2115]---> BDD-cost:   16
c ---[2114]---> BDD-cost:   16
c ---[2113]---> BDD-cost:   15
c ---[2112]---> BDD-cost:   16
c ---[2111]---> BDD-cost:   16
c ---[2110]---> BDD-cost:   16
c ---[2109]---> BDD-cost:   16
c ---[2107]---> BDD-cost:   16
c ---[2106]---> BDD-cost:   13
c ---[2105]---> BDD-cost:   15
c ---[2104]---> BDD-cost:   16
c ---[2102]---> BDD-cost:   16
c ---[2101]---> BDD-cost:   15
c ---[2100]---> BDD-cost:   16
c ---[2099]---> BDD-cost:   16
c ---[2098]---> BDD-cost:   16
c ---[2097]---> BDD-cost:   16
c ---[2096]---> BDD-cost:   14
c ---[2095]---> BDD-cost:   16
c ---[2093]---> BDD-cost:   14
c ---[2092]---> BDD-cost:   14
c ---[2091]---> BDD-cost:   16
c ---[2090]---> BDD-cost:   16
c ---[2089]---> BDD-cost:   15
c ---[2088]---> BDD-cost:   15
c ---[2087]---> BDD-cost:   15
c ---[2086]---> BDD-cost:   16
c ---[2084]---> BDD-cost:   16
c ---[2083]---> BDD-cost:   16
c ---[2082]---> BDD-cost:   15
c ---[2081]---> BDD-cost:   15
c ---[2080]---> BDD-cost:   16
c ---[2079]---> BDD-cost:   16
c ---[2078]---> BDD-cost:   16
c ---[2077]---> BDD-cost:   15
c ---[2076]---> BDD-cost:   15
c ---[2075]---> BDD-cost:   14
c ---[2074]---> BDD-cost:   15
c ---[2073]---> BDD-cost:   15
c ---[2072]---> BDD-cost:   16
c ---[2071]---> BDD-cost:   16
c ---[2070]---> BDD-cost:   16
c ---[2069]---> BDD-cost:   16
c ---[2068]---> BDD-cost:   15
c ---[2067]---> BDD-cost:   14
c ---[2066]---> BDD-cost:   16
c ---[2065]---> BDD-cost:   16
c ---[2064]---> BDD-cost:   14
c ---[2063]---> BDD-cost:   15
c ---[2062]---> BDD-cost:   13
c ---[2061]---> BDD-cost:   16
c ---[2060]---> BDD-cost:   15
c ---[2059]---> BDD-cost:   14
c ---[2058]---> BDD-cost:   16
c ---[2057]---> BDD-cost:   15
c ---[2056]---> BDD-cost:   15
c ---[2055]---> BDD-cost:   14
c ---[2054]---> BDD-cost:   15
c ---[2052]---> BDD-cost:   16
c ---[2051]---> BDD-cost:   15
c ---[2050]---> BDD-cost:   16
c ---[2048]---> BDD-cost:   16
c ---[2047]---> BDD-cost:   15
c ---[2046]---> BDD-cost:   16
c ---[2045]---> BDD-cost:   16
c ---[2044]---> BDD-cost:   15
c ---[2042]---> BDD-cost:   15
c ---[2041]---> BDD-cost:   16
c ---[2040]---> BDD-cost:   16
c ---[2039]---> BDD-cost:   14
c ---[2038]---> BDD-cost:   15
c ---[2037]---> BDD-cost:   16
c ---[2036]---> BDD-cost:   16
c ---[2034]---> BDD-cost:   16
c ---[2033]---> BDD-cost:   15
c ---[2031]---> BDD-cost:   16
c ---[2030]---> BDD-cost:   13
c ---[2029]---> BDD-cost:   14
c ---[2028]---> BDD-cost:   15
c ---[2027]---> BDD-cost:   16
c ---[2026]---> BDD-cost:   16
c ---[2025]---> BDD-cost:   16
c ---[2024]---> BDD-cost:   16
c ---[2023]---> BDD-cost:   16
c ---[2022]---> BDD-cost:   15
c ---[2021]---> BDD-cost:   16
c ---[2020]---> BDD-cost:   15
c ---[2019]---> BDD-cost:   15
c ---[2018]---> BDD-cost:   14
c ---[2017]---> BDD-cost:   16
c ---[2015]---> BDD-cost:   16
c ---[2014]---> BDD-cost:   15
c ---[2013]---> BDD-cost:   15
c ---[2012]---> BDD-cost:   15
c ---[2011]---> BDD-cost:   16
c ---[2010]---> BDD-cost:   16
c ---[2009]---> BDD-cost:   16
c ---[2008]---> BDD-cost:   14
c ---[2007]---> BDD-cost:   16
c ---[2006]---> BDD-cost:   16
c ---[2005]---> BDD-cost:   16
c ---[2004]---> BDD-cost:   15
c ---[2003]---> BDD-cost:   16
c ---[2002]---> BDD-cost:   16
c ---[2001]---> BDD-cost:   16
c ---[2000]---> BDD-cost:   15
c ---[1999]---> BDD-cost:   15
c ---[1998]---> BDD-cost:   14
c ---[1997]---> BDD-cost:   16
c ---[1995]---> BDD-cost:   15
c ---[1994]---> BDD-cost:   14
c ---[1993]---> BDD-cost:   16
c ---[1992]---> BDD-cost:   15
c ---[1991]---> BDD-cost:   16
c ---[1990]---> BDD-cost:   15
c ---[1989]---> BDD-cost:   13
c ---[1988]---> BDD-cost:   15
c ---[1987]---> BDD-cost:   16
c ---[1986]---> BDD-cost:   14
c ---[1985]---> BDD-cost:   15
c ---[1984]---> BDD-cost:   15
c ---[1983]---> BDD-cost:   15
c ---[1982]---> BDD-cost:   15
c ---[1981]---> BDD-cost:   15
c ---[1980]---> BDD-cost:   14
c ---[1979]---> BDD-cost:   15
c ---[1978]---> BDD-cost:   16
c ---[1977]---> BDD-cost:   15
c ---[1975]---> BDD-cost:   15
c ---[1974]---> BDD-cost:   15
c ---[1973]---> BDD-cost:   14
c ---[1972]---> BDD-cost:   13
c ---[1971]---> BDD-cost:   16
c ---[1970]---> BDD-cost:   15
c ---[1969]---> BDD-cost:   15
c ---[1968]---> BDD-cost:   16
c ---[1967]---> BDD-cost:   15
c ---[1966]---> BDD-cost:   16
c ---[1965]---> BDD-cost:   14
c ---[1964]---> BDD-cost:   15
c ---[1963]---> BDD-cost:   15
c ---[1962]---> BDD-cost:   16
c ---[1960]---> BDD-cost:   16
c ---[1959]---> BDD-cost:   15
c ---[1958]---> BDD-cost:   14
c ---[1957]---> BDD-cost:   14
c ---[1956]---> BDD-cost:   16
c ---[1955]---> BDD-cost:   16
c ---[1954]---> BDD-cost:   16
c ---[1952]---> BDD-cost:   16
c ---[1951]---> BDD-cost:   16
c ---[1949]---> BDD-cost:   16
c ---[1948]---> BDD-cost:   15
c ---[1947]---> BDD-cost:   15
c ---[1946]---> BDD-cost:   16
c ---[1945]---> BDD-cost:   15
c ---[1944]---> BDD-cost:   16
c ---[1943]---> BDD-cost:   15
c ---[1942]---> BDD-cost:   15
c ---[1941]---> BDD-cost:   16
c ---[1940]---> BDD-cost:   15
c ---[1939]---> BDD-cost:   14
c ---[1935]---> BDD-cost:   16
c ---[1934]---> BDD-cost:   15
c ---[1931]---> BDD-cost:   16
c ---[1930]---> BDD-cost:   15
c ---[1929]---> BDD-cost:   15
c ---[1926]---> BDD-cost:   16
c ---[1924]---> BDD-cost:   16
c ---[1923]---> BDD-cost:   15
c ---[1922]---> BDD-cost:   16
c ---[1921]---> BDD-cost:   15
c ---[1920]---> BDD-cost:   16
c ---[1919]---> BDD-cost:   15
c ---[1918]---> BDD-cost:   15
c ---[1917]---> BDD-cost:   16
c ---[1916]---> BDD-cost:   16
c ---[1915]---> BDD-cost:   16
c ---[1914]---> BDD-cost:   16
c ---[1913]---> BDD-cost:   15
c ---[1912]---> BDD-cost:   15
c ---[1911]---> BDD-cost:   16
c ---[1910]---> BDD-cost:   16
c ---[1909]---> BDD-cost:   15
c ---[1908]---> BDD-cost:   16
c ---[1907]---> BDD-cost:   15
c ---[1906]---> BDD-cost:   16
c ---[1905]---> BDD-cost:   16
c ---[1904]---> BDD-cost:   15
c ---[1903]---> BDD-cost:   16
c ---[1902]---> BDD-cost:   16
c ---[1901]---> BDD-cost:   14
c ---[1900]---> BDD-cost:   14
c ---[1899]---> BDD-cost:   16
c ---[1898]---> BDD-cost:   16
c ---[1897]---> BDD-cost:   15
c ---[1896]---> BDD-cost:   15
c ---[1895]---> BDD-cost:   15
c ---[1893]---> BDD-cost:   13
c ---[1892]---> BDD-cost:   16
c ---[1891]---> BDD-cost:   13
c ---[1890]---> BDD-cost:   16
c ---[1889]---> BDD-cost:   16
c ---[1888]---> BDD-cost:   16
c ---[1887]---> BDD-cost:   14
c ---[1886]---> BDD-cost:   16
c ---[1885]---> BDD-cost:   16
c ---[1883]---> BDD-cost:   15
c ---[1882]---> BDD-cost:   14
c ---[1881]---> BDD-cost:   16
c ---[1879]---> BDD-cost:   15
c ---[1878]---> BDD-cost:   16
c ---[1877]---> BDD-cost:   16
c ---[1875]---> BDD-cost:   16
c ---[1874]---> BDD-cost:   16
c ---[1872]---> BDD-cost:   13
c ---[1871]---> BDD-cost:   16
c ---[1869]---> BDD-cost:   16
c ---[1868]---> BDD-cost:   16
c ---[1867]---> BDD-cost:   16
c ---[1865]---> BDD-cost:   16
c ---[1862]---> BDD-cost:   14
c ---[1861]---> BDD-cost:   15
c ---[1860]---> BDD-cost:   16
c ---[1859]---> BDD-cost:   15
c ---[1858]---> BDD-cost:   16
c ---[1857]---> BDD-cost:   15
c ---[1856]---> BDD-cost:   14
c ---[1855]---> BDD-cost:   16
c ---[1854]---> BDD-cost:   15
c ---[1853]---> BDD-cost:   15
c ---[1851]---> BDD-cost:   15
c ---[1850]---> BDD-cost:   16
c ---[1849]---> BDD-cost:   14
c ---[1848]---> BDD-cost:   14
c ---[1847]---> BDD-cost:   16
c ---[1846]---> BDD-cost:   15
c ---[1845]---> BDD-cost:   15
c ---[1844]---> BDD-cost:   15
c ---[1843]---> BDD-cost:   16
c ---[1842]---> BDD-cost:   14
c ---[1841]---> BDD-cost:   16
c ---[1840]---> BDD-cost:   14
c ---[1839]---> BDD-cost:   15
c ---[1838]---> BDD-cost:   15
c ---[1837]---> BDD-cost:   16
c ---[1836]---> BDD-cost:   16
c ---[1833]---> BDD-cost:   16
c ---[1832]---> BDD-cost:   14
c ---[1831]---> BDD-cost:   15
c ---[1830]---> BDD-cost:   16
c ---[1829]---> BDD-cost:   14
c ---[1828]---> BDD-cost:   14
c ---[1825]---> BDD-cost:   16
c ---[1824]---> BDD-cost:   16
c ---[1823]---> BDD-cost:   16
c ---[1822]---> BDD-cost:   14
c ---[1821]---> BDD-cost:   16
c ---[1820]---> BDD-cost:   16
c ---[1819]---> BDD-cost:   15
c ---[1818]---> BDD-cost:   16
c ---[1817]---> BDD-cost:   14
c ---[1816]---> BDD-cost:   16
c ---[1814]---> BDD-cost:   15
c ---[1813]---> BDD-cost:   16
c ---[1811]---> BDD-cost:   16
c ---[1810]---> BDD-cost:   15
c ---[1809]---> BDD-cost:   14
c ---[1807]---> BDD-cost:   16
c ---[1806]---> BDD-cost:   15
c ---[1805]---> BDD-cost:   13
c ---[1804]---> BDD-cost:   14
c ---[1803]---> BDD-cost:   16
c ---[1802]---> BDD-cost:   16
c ---[1800]---> BDD-cost:   14
c ---[1799]---> BDD-cost:   16
c ---[1798]---> BDD-cost:   15
c ---[1797]---> BDD-cost:   16
c ---[1796]---> BDD-cost:   15
c ---[1795]---> BDD-cost:   15
c ---[1794]---> BDD-cost:   16
c ---[1793]---> BDD-cost:   16
c ---[1792]---> BDD-cost:   16
c ---[1791]---> BDD-cost:   16
c ---[1788]---> BDD-cost:   16
c ---[1786]---> BDD-cost:   15
c ---[1785]---> BDD-cost:   16
c ---[1783]---> BDD-cost:   14
c ---[1782]---> BDD-cost:   15
c ---[1781]---> BDD-cost:   15
c ---[1780]---> BDD-cost:   16
c ---[1779]---> BDD-cost:   16
c ---[1778]---> BDD-cost:   14
c ---[1777]---> BDD-cost:   16
c ---[1776]---> BDD-cost:   13
c ---[1775]---> BDD-cost:   16
c ---[1774]---> BDD-cost:   16
c ---[1773]---> BDD-cost:   16
c ---[1772]---> BDD-cost:   14
c ---[1771]---> BDD-cost:   16
c ---[1769]---> BDD-cost:   15
c ---[1766]---> BDD-cost:   16
c ---[1765]---> BDD-cost:   15
c ---[1764]---> BDD-cost:   16
c ---[1763]---> BDD-cost:   16
c ---[1762]---> BDD-cost:   14
c ---[1761]---> BDD-cost:   15
c ---[1760]---> BDD-cost:   16
c ---[1759]---> BDD-cost:   14
c ---[1758]---> BDD-cost:   15
c ---[1757]---> BDD-cost:   16
c ---[1755]---> BDD-cost:   16
c ---[1753]---> BDD-cost:   15
c ---[1752]---> BDD-cost:   16
c ---[1751]---> BDD-cost:   16
c ---[1750]---> BDD-cost:   15
c ---[1749]---> BDD-cost:   16
c ---[1748]---> BDD-cost:   16
c ---[1747]---> BDD-cost:   14
c ---[1746]---> BDD-cost:   16
c ---[1745]---> BDD-cost:   16
c ---[1744]---> BDD-cost:   16
c ---[1743]---> BDD-cost:   15
c ---[1741]---> BDD-cost:   15
c ---[1740]---> BDD-cost:   15
c ---[1739]---> BDD-cost:   16
c ---[1738]---> BDD-cost:   15
c ---[1737]---> BDD-cost:   15
c ---[1736]---> BDD-cost:   16
c ---[1735]---> BDD-cost:   16
c ---[1734]---> BDD-cost:   15
c ---[1732]---> BDD-cost:   15
c ---[1731]---> BDD-cost:   16
c ---[1730]---> BDD-cost:   16
c ---[1729]---> BDD-cost:   16
c ---[1728]---> BDD-cost:   16
c ---[1727]---> BDD-cost:   14
c ---[1725]---> BDD-cost:   16
c ---[1724]---> BDD-cost:   14
c ---[1723]---> BDD-cost:   15
c ---[1722]---> BDD-cost:   15
c ---[1721]---> BDD-cost:   14
c ---[1719]---> BDD-cost:   15
c ---[1717]---> BDD-cost:   16
c ---[1716]---> BDD-cost:   15
c ---[1715]---> BDD-cost:   16
c ---[1714]---> BDD-cost:   14
c ---[1713]---> BDD-cost:   15
c ---[1712]---> BDD-cost:   16
c ---[1711]---> BDD-cost:   15
c ---[1710]---> BDD-cost:   15
c ---[1709]---> BDD-cost:   16
c ---[1708]---> BDD-cost:   16
c ---[1707]---> BDD-cost:   15
c ---[1706]---> BDD-cost:   15
c ---[1705]---> BDD-cost:   16
c ---[1704]---> BDD-cost:   15
c ---[1702]---> BDD-cost:   71
c ---[1700]---> BDD-cost:   69
c ---[1699]---> BDD-cost:    7
c ---[1698]---> BDD-cost:    5
c ---[1697]---> BDD-cost:    8
c ---[1696]---> BDD-cost:    5
c ---[1695]---> BDD-cost:    6
c ---[1694]---> BDD-cost:    7
c ---[1693]---> BDD-cost:   17
c ---[1692]---> BDD-cost:    8
c ---[1691]---> BDD-cost:    7
c ---[1690]---> BDD-cost:    4
c ---[1689]---> BDD-cost:    7
c ---[1688]---> BDD-cost:    8
c ---[1687]---> BDD-cost:    6
c ---[1686]---> BDD-cost:    3
c ---[1685]---> BDD-cost:    7
c ---[1684]---> BDD-cost:    5
c ---[1683]---> BDD-cost:    7
c ---[1682]---> BDD-cost:   22
c ---[1681]---> BDD-cost:    6
c ---[1680]---> BDD-cost:    6
c ---[1679]---> BDD-cost:   19
c ---[1678]---> BDD-cost:    6
c ---[1677]---> BDD-cost:    8
c ---[1676]---> BDD-cost:    8
c ---[1675]---> BDD-cost:    6
c ---[1674]---> BDD-cost:    6
c ---[1673]---> BDD-cost:    5
c ---[1672]---> BDD-cost:    8
c ---[1671]---> BDD-cost:    7
c ---[1670]---> BDD-cost:   19
c ---[1669]---> BDD-cost:   20
c ---[1668]---> BDD-cost:   20
c ---[1667]---> BDD-cost:    7
c ---[1666]---> BDD-cost:    5
c ---[1665]---> BDD-cost:    5
c ---[1664]---> BDD-cost:    7
c ---[1663]---> BDD-cost:    5
c ---[1662]---> BDD-cost:    6
c ---[1661]---> BDD-cost:   17
c ---[1660]---> BDD-cost:    5
c ---[1659]---> BDD-cost:    8
c ---[1658]---> BDD-cost:    8
c ---[1657]---> BDD-cost:    4
c ---[1656]---> BDD-cost:    3
c ---[1655]---> BDD-cost:    8
c ---[1654]---> BDD-cost:    5
c ---[1653]---> BDD-cost:    6
c ---[1652]---> BDD-cost:    7
c ---[1651]---> BDD-cost:    6
c ---[1650]---> BDD-cost:    8
c ---[1649]---> BDD-cost:    4
c ---[1648]---> BDD-cost:   19
c ---[1647]---> BDD-cost:    3
c ---[1646]---> BDD-cost:   17
c ---[1645]---> BDD-cost:    7
c ---[1644]---> BDD-cost:   22
c ---[1643]---> BDD-cost:    8
c ---[1642]---> BDD-cost:    3
c ---[1641]---> BDD-cost:    5
c ---[1640]---> BDD-cost:    8
c ---[1639]---> BDD-cost:    7
c ---[1638]---> BDD-cost:    7
c ---[1637]---> BDD-cost:    5
c ---[1636]---> BDD-cost:    8
c ---[1635]---> BDD-cost:   22
c ---[1634]---> BDD-cost:    7
c ---[1633]---> BDD-cost:    8
c ---[1632]---> BDD-cost:    8
c ---[1631]---> BDD-cost:    6
c ---[1630]---> BDD-cost:    7
c ---[1629]---> BDD-cost:    5
c ---[1628]---> BDD-cost:    7
c ---[1627]---> BDD-cost:    6
c ---[1626]---> BDD-cost:    7
c ---[1625]---> BDD-cost:   17
c ---[1624]---> BDD-cost:    5
c ---[1623]---> BDD-cost:   17
c ---[1622]---> BDD-cost:    7
c ---[1621]---> BDD-cost:   22
c ---[1620]---> BDD-cost:    5
c ---[1619]---> BDD-cost:    8
c ---[1618]---> BDD-cost:    3
c ---[1617]---> BDD-cost:    8
c ---[1616]---> BDD-cost:    8
c ---[1615]---> BDD-cost:    6
c ---[1614]---> BDD-cost:    7
c ---[1613]---> BDD-cost:    6
c ---[1612]---> BDD-cost:    5
c ---[1611]---> BDD-cost:    4
c ---[1610]---> BDD-cost:   18
c ---[1609]---> BDD-cost:    6
c ---[1608]---> BDD-cost:    5
c ---[1607]---> BDD-cost:    6
c ---[1606]---> BDD-cost:    7
c ---[1605]---> BDD-cost:   20
c ---[1604]---> BDD-cost:   22
c ---[1603]---> BDD-cost:    6
c ---[1602]---> BDD-cost:    8
c ---[1601]---> BDD-cost:    6
c ---[1600]---> BDD-cost:    8
c ---[1599]---> BDD-cost:    7
c ---[1598]---> BDD-cost:    6
c ---[1597]---> BDD-cost:    7
c ---[1596]---> BDD-cost:    5
c ---[1595]---> BDD-cost:    8
c ---[1594]---> BDD-cost:    8
c ---[1593]---> BDD-cost:    7
c ---[1592]---> BDD-cost:    6
c ---[1591]---> BDD-cost:   18
c ---[1590]---> BDD-cost:    7
c ---[1588]---> BDD-cost:   73
c ---[1587]---> BDD-cost:    6
c ---[1586]---> BDD-cost:    8
c ---[1585]---> BDD-cost:    8
c ---[1584]---> BDD-cost:    7
c ---[1583]---> BDD-cost:    5
c ---[1582]---> BDD-cost:    8
c ---[1581]---> BDD-cost:    8
c ---[1580]---> BDD-cost:    6
c ---[1579]---> BDD-cost:    8
c ---[1578]---> BDD-cost:    4
c ---[1577]---> BDD-cost:    6
c ---[1576]---> BDD-cost:    6
c ---[1575]---> BDD-cost:   22
c ---[1574]---> BDD-cost:   22
c ---[1573]---> BDD-cost:    7
c ---[1572]---> BDD-cost:    6
c ---[1571]---> BDD-cost:    6
c ---[1570]---> BDD-cost:    8
c ---[1569]---> BDD-cost:    5
c ---[1568]---> BDD-cost:    7
c ---[1567]---> BDD-cost:    8
c ---[1566]---> BDD-cost:    7
c ---[1565]---> BDD-cost:    4
c ---[1564]---> BDD-cost:    8
c ---[1563]---> BDD-cost:    8
c ---[1562]---> BDD-cost:    5
c ---[1561]---> BDD-cost:    7
c ---[1560]---> BDD-cost:    3
c ---[1559]---> BDD-cost:    3
c ---[1558]---> BDD-cost:    8
c ---[1557]---> BDD-cost:    5
c ---[1556]---> BDD-cost:    8
c ---[1555]---> BDD-cost:    4
c ---[1554]---> BDD-cost:    4
c ---[1553]---> BDD-cost:    5
c ---[1552]---> BDD-cost:    6
c ---[1551]---> BDD-cost:    6
c ---[1550]---> BDD-cost:    8
c ---[1549]---> BDD-cost:    6
c ---[1548]---> BDD-cost:    6
c ---[1547]---> BDD-cost:    8
c ---[1546]---> BDD-cost:    5
c ---[1545]---> BDD-cost:    3
c ---[1544]---> BDD-cost:   22
c ---[1543]---> BDD-cost:    8
c ---[1542]---> BDD-cost:    5
c ---[1541]---> BDD-cost:   22
c ---[1540]---> BDD-cost:   22
c ---[1539]---> BDD-cost:    8
c ---[1538]---> BDD-cost:    8
c ---[1537]---> BDD-cost:    3
c ---[1536]---> BDD-cost:    8
c ---[1535]---> BDD-cost:    7
c ---[1534]---> BDD-cost:    6
c ---[1533]---> BDD-cost:    4
c ---[1532]---> BDD-cost:    7
c ---[1531]---> BDD-cost:    8
c ---[1530]---> BDD-cost:   18
c ---[1529]---> BDD-cost:    8
c ---[1528]---> BDD-cost:   20
c ---[1527]---> BDD-cost:    6
c ---[1526]---> BDD-cost:    4
c ---[1525]---> BDD-cost:    7
c ---[1524]---> BDD-cost:   22
c ---[1523]---> BDD-cost:    7
c ---[1522]---> BDD-cost:    7
c ---[1521]---> BDD-cost:    5
c ---[1520]---> BDD-cost:    8
c ---[1519]---> BDD-cost:    8
c ---[1518]---> BDD-cost:    6
c ---[1517]---> BDD-cost:    6
c ---[1516]---> BDD-cost:    8
c ---[1515]---> BDD-cost:    7
c ---[1514]---> BDD-cost:   22
c ---[1513]---> BDD-cost:    4
c ---[1512]---> BDD-cost:    6
c ---[1511]---> BDD-cost:    4
c ---[1510]---> BDD-cost:   18
c ---[1509]---> BDD-cost:    4
c ---[1508]---> BDD-cost:    8
c ---[1507]---> BDD-cost:    5
c ---[1506]---> BDD-cost:   21
c ---[1505]---> BDD-cost:    7
c ---[1504]---> BDD-cost:    6
c ---[1503]---> BDD-cost:    3
c ---[1502]---> BDD-cost:   20
c ---[1501]---> BDD-cost:    7
c ---[1500]---> BDD-cost:    3
c ---[1499]---> BDD-cost:    5
c ---[1498]---> BDD-cost:    7
c ---[1497]---> BDD-cost:    7
c ---[1496]---> BDD-cost:    8
c ---[1495]---> BDD-cost:   21
c ---[1494]---> BDD-cost:    7
c ---[1493]---> BDD-cost:    4
c ---[1492]---> BDD-cost:    8
c ---[1491]---> BDD-cost:    6
c ---[1490]---> BDD-cost:    5
c ---[1489]---> BDD-cost:    7
c ---[1488]---> BDD-cost:   19
c ---[1487]---> BDD-cost:    7
c ---[1486]---> BDD-cost:    6
c ---[1485]---> BDD-cost:   22
c ---[1484]---> BDD-cost:    6
c ---[1483]---> BDD-cost:    7
c ---[1482]---> BDD-cost:    7
c ---[1481]---> BDD-cost:    6
c ---[1480]---> BDD-cost:    5
c ---[1479]---> BDD-cost:    6
c ---[1478]---> BDD-cost:    3
c ---[1476]---> BDD-cost:   69
c ---[1475]---> BDD-cost:    5
c ---[1474]---> BDD-cost:    8
c ---[1473]---> BDD-cost:    6
c ---[1472]---> BDD-cost:    3
c ---[1471]---> BDD-cost:    5
c ---[1470]---> BDD-cost:    8
c ---[1469]---> BDD-cost:    6
c ---[1468]---> BDD-cost:   22
c ---[1467]---> BDD-cost:    5
c ---[1466]---> BDD-cost:    5
c ---[1465]---> BDD-cost:    8
c ---[1464]---> BDD-cost:    3
c ---[1463]---> BDD-cost:    7
c ---[1462]---> BDD-cost:    6
c ---[1461]---> BDD-cost:    7
c ---[1460]---> BDD-cost:    8
c ---[1459]---> BDD-cost:    7
c ---[1458]---> BDD-cost:   18
c ---[1457]---> BDD-cost:    6
c ---[1456]---> BDD-cost:    7
c ---[1455]---> BDD-cost:    4
c ---[1454]---> BDD-cost:    8
c ---[1453]---> BDD-cost:    7
c ---[1452]---> BDD-cost:    3
c ---[1451]---> BDD-cost:    5
c ---[1450]---> BDD-cost:    6
c ---[1449]---> BDD-cost:    6
c ---[1448]---> BDD-cost:    7
c ---[1447]---> BDD-cost:   21
c ---[1446]---> BDD-cost:    7
c ---[1445]---> BDD-cost:    6
c ---[1444]---> BDD-cost:    7
c ---[1443]---> BDD-cost:    8
c ---[1442]---> BDD-cost:    7
c ---[1441]---> BDD-cost:    3
c ---[1440]---> BDD-cost:    4
c ---[1439]---> BDD-cost:    8
c ---[1438]---> BDD-cost:    7
c ---[1437]---> BDD-cost:    5
c ---[1436]---> BDD-cost:    7
c ---[1435]---> BDD-cost:    6
c ---[1434]---> BDD-cost:    6
c ---[1433]---> BDD-cost:    5
c ---[1432]---> BDD-cost:    6
c ---[1431]---> BDD-cost:    7
c ---[1430]---> BDD-cost:    7
c ---[1429]---> BDD-cost:    7
c ---[1428]---> BDD-cost:   22
c ---[1427]---> BDD-cost:    6
c ---[1426]---> BDD-cost:    6
c ---[1425]---> BDD-cost:    4
c ---[1424]---> BDD-cost:    8
c ---[1423]---> BDD-cost:    6
c ---[1422]---> BDD-cost:    8
c ---[1421]---> BDD-cost:    8
c ---[1420]---> BDD-cost:    8
c ---[1419]---> BDD-cost:   20
c ---[1418]---> BDD-cost:    7
c ---[1417]---> BDD-cost:    3
c ---[1416]---> BDD-cost:   20
c ---[1415]---> BDD-cost:    3
c ---[1414]---> BDD-cost:    7
c ---[1413]---> BDD-cost:   19
c ---[1412]---> BDD-cost:    5
c ---[1411]---> BDD-cost:    5
c ---[1410]---> BDD-cost:    7
c ---[1409]---> BDD-cost:    7
c ---[1408]---> BDD-cost:    8
c ---[1407]---> BDD-cost:    8
c ---[1406]---> BDD-cost:    8
c ---[1405]---> BDD-cost:    5
c ---[1404]---> BDD-cost:    3
c ---[1403]---> BDD-cost:   22
c ---[1402]---> BDD-cost:    7
c ---[1401]---> BDD-cost:    6
c ---[1400]---> BDD-cost:    3
c ---[1399]---> BDD-cost:    6
c ---[1398]---> BDD-cost:    7
c ---[1397]---> BDD-cost:    8
c ---[1396]---> BDD-cost:    7
c ---[1395]---> BDD-cost:    7
c ---[1394]---> BDD-cost:    7
c ---[1393]---> BDD-cost:    6
c ---[1392]---> BDD-cost:    8
c ---[1391]---> BDD-cost:   18
c ---[1390]---> BDD-cost:    7
c ---[1389]---> BDD-cost:    7
c ---[1388]---> BDD-cost:    6
c ---[1387]---> BDD-cost:    7
c ---[1386]---> BDD-cost:   21
c ---[1385]---> BDD-cost:    7
c ---[1384]---> BDD-cost:    5
c ---[1383]---> BDD-cost:    7
c ---[1382]---> BDD-cost:    8
c ---[1381]---> BDD-cost:    7
c ---[1380]---> BDD-cost:    7
c ---[1379]---> BDD-cost:    8
c ---[1378]---> BDD-cost:    5
c ---[1377]---> BDD-cost:    7
c ---[1376]---> BDD-cost:    6
c ---[1375]---> BDD-cost:    6
c ---[1374]---> BDD-cost:    6
c ---[1373]---> BDD-cost:   22
c ---[1372]---> BDD-cost:    6
c ---[1371]---> BDD-cost:    7
c ---[1370]---> BDD-cost:    6
c ---[1369]---> BDD-cost:    7
c ---[1368]---> BDD-cost:   19
c ---[1367]---> BDD-cost:   21
c ---[1366]---> BDD-cost:   22
c ---[1364]---> BDD-cost:   65
c ---[1363]---> BDD-cost:    8
c ---[1362]---> BDD-cost:    6
c ---[1361]---> BDD-cost:   21
c ---[1360]---> BDD-cost:    3
c ---[1359]---> BDD-cost:   20
c ---[1358]---> BDD-cost:    7
c ---[1357]---> BDD-cost:    8
c ---[1356]---> BDD-cost:    8
c ---[1355]---> BDD-cost:    7
c ---[1354]---> BDD-cost:    7
c ---[1353]---> BDD-cost:   22
c ---[1352]---> BDD-cost:    3
c ---[1351]---> BDD-cost:    4
c ---[1350]---> BDD-cost:    8
c ---[1349]---> BDD-cost:   19
c ---[1348]---> BDD-cost:    8
c ---[1347]---> BDD-cost:    7
c ---[1346]---> BDD-cost:    8
c ---[1345]---> BDD-cost:    6
c ---[1344]---> BDD-cost:    5
c ---[1343]---> BDD-cost:    6
c ---[1342]---> BDD-cost:    8
c ---[1341]---> BDD-cost:    6
c ---[1340]---> BDD-cost:    8
c ---[1339]---> BDD-cost:    6
c ---[1338]---> BDD-cost:    8
c ---[1337]---> BDD-cost:    8
c ---[1336]---> BDD-cost:    5
c ---[1335]---> BDD-cost:    6
c ---[1334]---> BDD-cost:    6
c ---[1333]---> BDD-cost:   18
c ---[1332]---> BDD-cost:    4
c ---[1331]---> BDD-cost:    7
c ---[1330]---> BDD-cost:    8
c ---[1329]---> BDD-cost:    6
c ---[1328]---> BDD-cost:    7
c ---[1327]---> BDD-cost:    6
c ---[1326]---> BDD-cost:    3
c ---[1325]---> BDD-cost:    6
c ---[1324]---> BDD-cost:    3
c ---[1323]---> BDD-cost:    5
c ---[1322]---> BDD-cost:    3
c ---[1321]---> BDD-cost:    7
c ---[1320]---> BDD-cost:    3
c ---[1319]---> BDD-cost:    6
c ---[1318]---> BDD-cost:    7
c ---[1317]---> BDD-cost:    3
c ---[1316]---> BDD-cost:    3
c ---[1315]---> BDD-cost:    6
c ---[1314]---> BDD-cost:    6
c ---[1313]---> BDD-cost:    6
c ---[1312]---> BDD-cost:    6
c ---[1311]---> BDD-cost:    8
c ---[1310]---> BDD-cost:    7
c ---[1309]---> BDD-cost:    7
c ---[1308]---> BDD-cost:    6
c ---[1307]---> BDD-cost:    7
c ---[1306]---> BDD-cost:    7
c ---[1305]---> BDD-cost:    8
c ---[1304]---> BDD-cost:    6
c ---[1303]---> BDD-cost:    3
c ---[1302]---> BDD-cost:    7
c ---[1301]---> BDD-cost:    7
c ---[1300]---> BDD-cost:    5
c ---[1299]---> BDD-cost:    6
c ---[1298]---> BDD-cost:   19
c ---[1297]---> BDD-cost:    5
c ---[1296]---> BDD-cost:    5
c ---[1295]---> BDD-cost:    5
c ---[1294]---> BDD-cost:    8
c ---[1293]---> BDD-cost:    7
c ---[1292]---> BDD-cost:   20
c ---[1291]---> BDD-cost:    6
c ---[1290]---> BDD-cost:    8
c ---[1289]---> BDD-cost:   20
c ---[1288]---> BDD-cost:   20
c ---[1287]---> BDD-cost:   22
c ---[1286]---> BDD-cost:    8
c ---[1285]---> BDD-cost:    8
c ---[1284]---> BDD-cost:    6
c ---[1283]---> BDD-cost:    5
c ---[1282]---> BDD-cost:    5
c ---[1281]---> BDD-cost:    8
c ---[1280]---> BDD-cost:    6
c ---[1279]---> BDD-cost:    8
c ---[1278]---> BDD-cost:    5
c ---[1277]---> BDD-cost:   22
c ---[1276]---> BDD-cost:   22
c ---[1275]---> BDD-cost:    5
c ---[1274]---> BDD-cost:   18
c ---[1273]---> BDD-cost:    8
c ---[1272]---> BDD-cost:    8
c ---[1271]---> BDD-cost:    7
c ---[1270]---> BDD-cost:    6
c ---[1269]---> BDD-cost:    3
c ---[1268]---> BDD-cost:    8
c ---[1267]---> BDD-cost:    7
c ---[1266]---> BDD-cost:    7
c ---[1265]---> BDD-cost:    5
c ---[1264]---> BDD-cost:    6
c ---[1263]---> BDD-cost:    4
c ---[1262]---> BDD-cost:    7
c ---[1261]---> BDD-cost:   20
c ---[1260]---> BDD-cost:    7
c ---[1259]---> BDD-cost:    7
c ---[1258]---> BDD-cost:    4
c ---[1257]---> BDD-cost:   20
c ---[1256]---> BDD-cost:    6
c ---[1255]---> BDD-cost:    7
c ---[1254]---> BDD-cost:    8
c ---[1252]---> BDD-cost:   73
c ---[1251]---> BDD-cost:   22
c ---[1250]---> BDD-cost:   22
c ---[1249]---> BDD-cost:    3
c ---[1248]---> BDD-cost:    6
c ---[1247]---> BDD-cost:    8
c ---[1246]---> BDD-cost:    3
c ---[1245]---> BDD-cost:    6
c ---[1244]---> BDD-cost:    7
c ---[1243]---> BDD-cost:   20
c ---[1242]---> BDD-cost:    7
c ---[1241]---> BDD-cost:    5
c ---[1240]---> BDD-cost:    8
c ---[1239]---> BDD-cost:    3
c ---[1238]---> BDD-cost:    8
c ---[1237]---> BDD-cost:    8
c ---[1236]---> BDD-cost:    7
c ---[1235]---> BDD-cost:    6
c ---[1234]---> BDD-cost:    6
c ---[1233]---> BDD-cost:   22
c ---[1232]---> BDD-cost:    7
c ---[1231]---> BDD-cost:    8
c ---[1230]---> BDD-cost:    7
c ---[1229]---> BDD-cost:    5
c ---[1228]---> BDD-cost:    6
c ---[1227]---> BDD-cost:    8
c ---[1226]---> BDD-cost:   22
c ---[1225]---> BDD-cost:   18
c ---[1224]---> BDD-cost:    8
c ---[1223]---> BDD-cost:    6
c ---[1222]---> BDD-cost:    6
c ---[1221]---> BDD-cost:    8
c ---[1220]---> BDD-cost:    3
c ---[1219]---> BDD-cost:    6
c ---[1218]---> BDD-cost:    6
c ---[1217]---> BDD-cost:    6
c ---[1216]---> BDD-cost:    7
c ---[1215]---> BDD-cost:    8
c ---[1214]---> BDD-cost:    6
c ---[1213]---> BDD-cost:    6
c ---[1212]---> BDD-cost:    8
c ---[1211]---> BDD-cost:   18
c ---[1210]---> BDD-cost:    5
c ---[1209]---> BDD-cost:    5
c ---[1208]---> BDD-cost:    8
c ---[1207]---> BDD-cost:    7
c ---[1206]---> BDD-cost:   20
c ---[1205]---> BDD-cost:    6
c ---[1204]---> BDD-cost:    7
c ---[1203]---> BDD-cost:    8
c ---[1202]---> BDD-cost:    7
c ---[1201]---> BDD-cost:    8
c ---[1200]---> BDD-cost:    8
c ---[1199]---> BDD-cost:    6
c ---[1197]---> BDD-cost:   67
c ---[1196]---> BDD-cost:    6
c ---[1195]---> BDD-cost:    6
c ---[1194]---> BDD-cost:    5
c ---[1193]---> BDD-cost:    6
c ---[1192]---> BDD-cost:   20
c ---[1191]---> BDD-cost:   19
c ---[1190]---> BDD-cost:    8
c ---[1189]---> BDD-cost:    5
c ---[1188]---> BDD-cost:    3
c ---[1187]---> BDD-cost:    8
c ---[1185]---> BDD-cost:   65
c ---[1184]---> BDD-cost:    6
c ---[1183]---> BDD-cost:    7
c ---[1182]---> BDD-cost:    7
c ---[1181]---> BDD-cost:    5
c ---[1180]---> BDD-cost:    6
c ---[1179]---> BDD-cost:    6
c ---[1178]---> BDD-cost:    7
c ---[1177]---> BDD-cost:   18
c ---[1176]---> BDD-cost:    6
c ---[1175]---> BDD-cost:    6
c ---[1173]---> BDD-cost:   65
c ---[1172]---> BDD-cost:    4
c ---[1171]---> BDD-cost:    8
c ---[1170]---> BDD-cost:    3
c ---[1169]---> BDD-cost:    8
c ---[1168]---> BDD-cost:    7
c ---[1167]---> BDD-cost:   18
c ---[1166]---> BDD-cost:    5
c ---[1165]---> BDD-cost:    6
c ---[1164]---> BDD-cost:    7
c ---[1163]---> BDD-cost:    4
c ---[1161]---> BDD-cost:   67
c ---[1160]---> BDD-cost:   20
c ---[1159]---> BDD-cost:    7
c ---[1158]---> BDD-cost:    6
c ---[1157]---> BDD-cost:   22
c ---[1156]---> BDD-cost:    7
c ---[1155]---> BDD-cost:    3
c ---[1154]---> BDD-cost:    6
c ---[1153]---> BDD-cost:   22
c ---[1152]---> BDD-cost:    3
c ---[1151]---> BDD-cost:    7
c ---[1149]---> BDD-cost:   67
c ---[1148]---> BDD-cost:    7
c ---[1147]---> BDD-cost:    3
c ---[1146]---> BDD-cost:    3
c ---[1145]---> BDD-cost:   18
c ---[1144]---> BDD-cost:    7
c ---[1143]---> BDD-cost:   18
c ---[1142]---> BDD-cost:    5
c ---[1141]---> BDD-cost:    8
c ---[1140]---> BDD-cost:   17
c ---[1139]---> BDD-cost:    6
c ---[1137]---> BDD-cost:   71
c ---[1135]---> BDD-cost:   65
c ---[1134]---> BDD-cost:   18
c ---[1133]---> BDD-cost:    7
c ---[1132]---> BDD-cost:    8
c ---[1131]---> BDD-cost:    8
c ---[1130]---> BDD-cost:    5
c ---[1129]---> BDD-cost:    7
c ---[1128]---> BDD-cost:    7
c ---[1127]---> BDD-cost:    7
c ---[1126]---> BDD-cost:    5
c ---[1125]---> BDD-cost:    3
c ---[1123]---> BDD-cost:   69
c ---[1122]---> BDD-cost:    7
c ---[1121]---> BDD-cost:   18
c ---[1120]---> BDD-cost:    8
c ---[1119]---> BDD-cost:    5
c ---[1118]---> BDD-cost:    3
c ---[1117]---> BDD-cost:    6
c ---[1116]---> BDD-cost:    3
c ---[1115]---> BDD-cost:    4
c ---[1114]---> BDD-cost:    6
c ---[1113]---> BDD-cost:    5
c ---[1111]---> BDD-cost:   69
c ---[1110]---> BDD-cost:    7
c ---[1109]---> BDD-cost:    5
c ---[1108]---> BDD-cost:    7
c ---[1107]---> BDD-cost:    8
c ---[1106]---> BDD-cost:    5
c ---[1105]---> BDD-cost:    5
c ---[1104]---> BDD-cost:    6
c ---[1103]---> BDD-cost:    7
c ---[1102]---> BDD-cost:    6
c ---[1101]---> BDD-cost:    7
c ---[1099]---> BDD-cost:   69
c ---[1098]---> BDD-cost:    7
c ---[1097]---> BDD-cost:    4
c ---[1096]---> BDD-cost:    7
c ---[1095]---> BDD-cost:    3
c ---[1094]---> BDD-cost:   21
c ---[1093]---> BDD-cost:    8
c ---[1092]---> BDD-cost:    5
c ---[1091]---> BDD-cost:    4
c ---[1090]---> BDD-cost:    6
c ---[1089]---> BDD-cost:    4
c ---[1087]---> BDD-cost:   67
c ---[1086]---> BDD-cost:    7
c ---[1085]---> BDD-cost:    6
c ---[1084]---> BDD-cost:    6
c ---[1083]---> BDD-cost:   20
c ---[1082]---> BDD-cost:    8
c ---[1081]---> BDD-cost:   22
c ---[1080]---> BDD-cost:    5
c ---[1079]---> BDD-cost:    5
c ---[1078]---> BDD-cost:   20
c ---[1077]---> BDD-cost:    3
c ---[1075]---> BDD-cost:   63
c ---[1074]---> BDD-cost:    8
c ---[1073]---> BDD-cost:    5
c ---[1072]---> BDD-cost:    7
c ---[1071]---> BDD-cost:    6
c ---[1070]---> BDD-cost:    7
c ---[1069]---> BDD-cost:    8
c ---[1068]---> BDD-cost:   19
c ---[1067]---> BDD-cost:    7
c ---[1066]---> BDD-cost:    6
c ---[1065]---> BDD-cost:    7
c ---[1063]---> BDD-cost:   65
c ---[1062]---> BDD-cost:    7
c ---[1061]---> BDD-cost:    7
c ---[1060]---> BDD-cost:    6
c ---[1059]---> BDD-cost:    7
c ---[1058]---> BDD-cost:    7
c ---[1057]---> BDD-cost:    7
c ---[1056]---> BDD-cost:    6
c ---[1055]---> BDD-cost:    7
c ---[1054]---> BDD-cost:    7
c ---[1053]---> BDD-cost:    7
c ---[1051]---> BDD-cost:   63
c ---[1050]---> BDD-cost:    7
c ---[1049]---> BDD-cost:    7
c ---[1048]---> BDD-cost:    7
c ---[1047]---> BDD-cost:    3
c ---[1046]---> BDD-cost:    8
c ---[1045]---> BDD-cost:    4
c ---[1044]---> BDD-cost:   21
c ---[1043]---> BDD-cost:    4
c ---[1042]---> BDD-cost:    8
c ---[1041]---> BDD-cost:    7
c ---[1039]---> BDD-cost:   63
c ---[1038]---> BDD-cost:   21
c ---[1037]---> BDD-cost:    4
c ---[1036]---> BDD-cost:    7
c ---[1035]---> BDD-cost:    7
c ---[1034]---> BDD-cost:    5
c ---[1033]---> BDD-cost:    5
c ---[1032]---> BDD-cost:    6
c ---[1031]---> BDD-cost:    8
c ---[1030]---> BDD-cost:   19
c ---[1029]---> BDD-cost:   22
c ---[1027]---> BDD-cost:   71
c ---[1026]---> BDD-cost:    6
c ---[1025]---> BDD-cost:    7
c ---[1024]---> BDD-cost:    3
c ---[1023]---> BDD-cost:   22
c ---[1022]---> BDD-cost:    8
c ---[1021]---> BDD-cost:    8
c ---[1020]---> BDD-cost:    6
c ---[1019]---> BDD-cost:    3
c ---[1018]---> BDD-cost:   19
c ---[1017]---> BDD-cost:    8
c ---[1015]---> BDD-cost:   69
c ---[1013]---> BDD-cost:   67
c ---[1012]---> BDD-cost:    4
c ---[1011]---> BDD-cost:    6
c ---[1010]---> BDD-cost:    8
c ---[1009]---> BDD-cost:    8
c ---[1008]---> BDD-cost:    8
c ---[1007]---> BDD-cost:    7
c ---[1006]---> BDD-cost:    7
c ---[1005]---> BDD-cost:    7
c ---[1004]---> BDD-cost:    8
c ---[1003]---> BDD-cost:    4
c ---[1001]---> BDD-cost:   65
c ---[1000]---> BDD-cost:    8
c ---[ 999]---> BDD-cost:    7
c ---[ 998]---> BDD-cost:    7
c ---[ 997]---> BDD-cost:    8
c ---[ 996]---> BDD-cost:    7
c ---[ 995]---> BDD-cost:    7
c ---[ 994]---> BDD-cost:    7
c ---[ 993]---> BDD-cost:    3
c ---[ 992]---> BDD-cost:    7
c ---[ 991]---> BDD-cost:    6
c ---[ 989]---> BDD-cost:   71
c ---[ 988]---> BDD-cost:    3
c ---[ 987]---> BDD-cost:    6
c ---[ 986]---> BDD-cost:    8
c ---[ 985]---> BDD-cost:    6
c ---[ 984]---> BDD-cost:    7
c ---[ 983]---> BDD-cost:    7
c ---[ 982]---> BDD-cost:    6
c ---[ 981]---> BDD-cost:   20
c ---[ 980]---> BDD-cost:    7
c ---[ 979]---> BDD-cost:    6
c ---[ 977]---> BDD-cost:   73
c ---[ 976]---> BDD-cost:    3
c ---[ 975]---> BDD-cost:    5
c ---[ 974]---> BDD-cost:    5
c ---[ 973]---> BDD-cost:    6
c ---[ 972]---> BDD-cost:    5
c ---[ 971]---> BDD-cost:    8
c ---[ 970]---> BDD-cost:   20
c ---[ 969]---> BDD-cost:   20
c ---[ 968]---> BDD-cost:    8
c ---[ 967]---> BDD-cost:    5
c ---[ 965]---> BDD-cost:   71
c ---[ 964]---> BDD-cost:    6
c ---[ 963]---> BDD-cost:    6
c ---[ 962]---> BDD-cost:    5
c ---[ 961]---> BDD-cost:    8
c ---[ 960]---> BDD-cost:    6
c ---[ 959]---> BDD-cost:    6
c ---[ 958]---> BDD-cost:    3
c ---[ 957]---> BDD-cost:    6
c ---[ 956]---> BDD-cost:    6
c ---[ 955]---> BDD-cost:    7
c ---[ 953]---> BDD-cost:   69
c ---[ 952]---> BDD-cost:    7
c ---[ 951]---> BDD-cost:    5
c ---[ 950]---> BDD-cost:    7
c ---[ 949]---> BDD-cost:    8
c ---[ 948]---> BDD-cost:    6
c ---[ 947]---> BDD-cost:    5
c ---[ 946]---> BDD-cost:    8
c ---[ 945]---> BDD-cost:    8
c ---[ 944]---> BDD-cost:    3
c ---[ 943]---> BDD-cost:    6
c ---[ 941]---> BDD-cost:   67
c ---[ 940]---> BDD-cost:    6
c ---[ 939]---> BDD-cost:    8
c ---[ 938]---> BDD-cost:    7
c ---[ 937]---> BDD-cost:    8
c ---[ 936]---> BDD-cost:   22
c ---[ 935]---> BDD-cost:    7
c ---[ 934]---> BDD-cost:    5
c ---[ 933]---> BDD-cost:   18
c ---[ 932]---> BDD-cost:    7
c ---[ 931]---> BDD-cost:    8
c ---[ 929]---> BDD-cost:   63
c ---[ 928]---> BDD-cost:    8
c ---[ 927]---> BDD-cost:    8
c ---[ 926]---> BDD-cost:    5
c ---[ 925]---> BDD-cost:    3
c ---[ 924]---> BDD-cost:   20
c ---[ 923]---> BDD-cost:   22
c ---[ 922]---> BDD-cost:    3
c ---[ 921]---> BDD-cost:    8
c ---[ 920]---> BDD-cost:    7
c ---[ 919]---> BDD-cost:   22
c ---[ 917]---> BDD-cost:   63
c ---[ 916]---> BDD-cost:    3
c ---[ 915]---> BDD-cost:    7
c ---[ 914]---> BDD-cost:    6
c ---[ 913]---> BDD-cost:    6
c ---[ 912]---> BDD-cost:    8
c ---[ 911]---> BDD-cost:    3
c ---[ 910]---> BDD-cost:    7
c ---[ 909]---> BDD-cost:    7
c ---[ 908]---> BDD-cost:    8
c ---[ 907]---> BDD-cost:    7
c ---[ 905]---> BDD-cost:   57
c ---[ 904]---> BDD-cost:    4
c ---[ 903]---> BDD-cost:    4
c ---[ 902]---> BDD-cost:    7
c ---[ 901]---> BDD-cost:    6
c ---[ 900]---> BDD-cost:    6
c ---[ 899]---> BDD-cost:    5
c ---[ 898]---> BDD-cost:   20
c ---[ 897]---> BDD-cost:    7
c ---[ 896]---> BDD-cost:   17
c ---[ 895]---> BDD-cost:    7
c ---[ 893]---> BDD-cost:   57
c ---[ 891]---> Adder-cost: 2156   maxlim: 2895835   bits: 23/22
c ---[ 890]---> BDD-cost:    8
c ---[ 889]---> BDD-cost:    6
c ---[ 888]---> BDD-cost:    7
c ---[ 887]---> BDD-cost:    7
c ---[ 886]---> BDD-cost:    8
c ---[ 885]---> BDD-cost:    8
c ---[ 884]---> BDD-cost:    3
c ---[ 883]---> BDD-cost:   21
c ---[ 882]---> BDD-cost:    8
c ---[ 881]---> BDD-cost:    7
c ---[ 879]---> Adder-cost: 2318   maxlim: 3144667   bits: 23/22
c ---[ 878]---> BDD-cost:    4
c ---[ 877]---> BDD-cost:   21
c ---[ 876]---> BDD-cost:    5
c ---[ 875]---> BDD-cost:    3
c ---[ 874]---> BDD-cost:    5
c ---[ 873]---> BDD-cost:    7
c ---[ 872]---> BDD-cost:    8
c ---[ 871]---> BDD-cost:    7
c ---[ 870]---> BDD-cost:    6
c ---[ 869]---> BDD-cost:    5
c ---[ 867]---> Adder-cost: 2324   maxlim: 3258332   bits: 23/22
c ---[ 866]---> BDD-cost:    6
c ---[ 865]---> BDD-cost:    3
c ---[ 864]---> BDD-cost:    3
c ---[ 863]---> BDD-cost:    3
c ---[ 862]---> BDD-cost:   20
c ---[ 861]---> BDD-cost:    6
c ---[ 860]---> BDD-cost:    3
c ---[ 859]---> BDD-cost:    8
c ---[ 858]---> BDD-cost:   19
c ---[ 857]---> BDD-cost:   19
c ---[ 855]---> Adder-cost: 1992   maxlim: 2337762   bits: 23/22
c ---[ 854]---> BDD-cost:    7
c ---[ 853]---> BDD-cost:    8
c ---[ 852]---> BDD-cost:    8
c ---[ 851]---> BDD-cost:    5
c ---[ 850]---> BDD-cost:   18
c ---[ 849]---> BDD-cost:    5
c ---[ 848]---> BDD-cost:   22
c ---[ 847]---> BDD-cost:    7
c ---[ 846]---> BDD-cost:    8
c ---[ 845]---> BDD-cost:    6
c ---[ 843]---> Adder-cost: 2106   maxlim: 3205085   bits: 23/22
c ---[ 842]---> BDD-cost:    8
c ---[ 841]---> BDD-cost:    6
c ---[ 840]---> BDD-cost:    8
c ---[ 839]---> BDD-cost:    6
c ---[ 838]---> BDD-cost:    7
c ---[ 837]---> BDD-cost:    3
c ---[ 836]---> BDD-cost:    7
c ---[ 835]---> BDD-cost:    5
c ---[ 834]---> BDD-cost:    7
c ---[ 833]---> BDD-cost:   21
c ---[ 831]---> Adder-cost: 2300   maxlim: 3529693   bits: 23/22
c ---[ 830]---> BDD-cost:    5
c ---[ 829]---> BDD-cost:    7
c ---[ 828]---> BDD-cost:    3
c ---[ 827]---> BDD-cost:   21
c ---[ 826]---> BDD-cost:    4
c ---[ 825]---> BDD-cost:    6
c ---[ 824]---> BDD-cost:   22
c ---[ 823]---> BDD-cost:    5
c ---[ 822]---> BDD-cost:   19
c ---[ 821]---> BDD-cost:    5
c ---[ 819]---> Adder-cost: 2034   maxlim: 2619359   bits: 23/22
c ---[ 818]---> BDD-cost:    7
c ---[ 817]---> BDD-cost:    8
c ---[ 816]---> BDD-cost:    7
c ---[ 815]---> BDD-cost:    5
c ---[ 814]---> BDD-cost:    7
c ---[ 813]---> BDD-cost:    7
c ---[ 812]---> BDD-cost:    7
c ---[ 811]---> BDD-cost:    8
c ---[ 810]---> BDD-cost:    6
c ---[ 809]---> BDD-cost:    3
c ---[ 807]---> Adder-cost: 2372   maxlim: 3350491   bits: 23/22
c ---[ 806]---> BDD-cost:    5
c ---[ 805]---> BDD-cost:    7
c ---[ 804]---> BDD-cost:    3
c ---[ 803]---> BDD-cost:   18
c ---[ 802]---> BDD-cost:    5
c ---[ 801]---> BDD-cost:    4
c ---[ 800]---> BDD-cost:    7
c ---[ 799]---> BDD-cost:    7
c ---[ 798]---> BDD-cost:    7
c ---[ 797]---> BDD-cost:   20
c ---[ 795]---> Adder-cost: 2032   maxlim: 2594782   bits: 23/22
c ---[ 794]---> BDD-cost:    7
c ---[ 793]---> BDD-cost:    8
c ---[ 792]---> BDD-cost:   18
c ---[ 791]---> BDD-cost:    7
c ---[ 790]---> BDD-cost:    7
c ---[ 789]---> BDD-cost:    6
c ---[ 788]---> BDD-cost:    3
c ---[ 787]---> BDD-cost:    8
c ---[ 786]---> BDD-cost:    5
c ---[ 785]---> BDD-cost:    5
c ---[ 783]---> Adder-cost: 2312   maxlim: 2893788   bits: 23/22
c ---[ 782]---> BDD-cost:    8
c ---[ 781]---> BDD-cost:    7
c ---[ 780]---> BDD-cost:   18
c ---[ 779]---> BDD-cost:    7
c ---[ 778]---> BDD-cost:    3
c ---[ 777]---> BDD-cost:    7
c ---[ 776]---> BDD-cost:    6
c ---[ 775]---> BDD-cost:    7
c ---[ 774]---> BDD-cost:    5
c ---[ 773]---> BDD-cost:   19
c ---[ 771]---> BDD-cost:   67
c ---[ 769]---> Adder-cost: 2158   maxlim: 3303386   bits: 23/22
c ---[ 768]---> BDD-cost:    7
c ---[ 767]---> BDD-cost:    7
c ---[ 766]---> BDD-cost:    8
c ---[ 765]---> BDD-cost:    7
c ---[ 764]---> BDD-cost:    4
c ---[ 763]---> BDD-cost:    6
c ---[ 762]---> BDD-cost:    6
c ---[ 761]---> BDD-cost:    5
c ---[ 760]---> BDD-cost:    7
c ---[ 759]---> BDD-cost:    3
c ---[ 757]---> Adder-cost: 2220   maxlim: 3007452   bits: 23/22
c ---[ 756]---> BDD-cost:    6
c ---[ 755]---> BDD-cost:   21
c ---[ 754]---> BDD-cost:    6
c ---[ 753]---> BDD-cost:    7
c ---[ 752]---> BDD-cost:    6
c ---[ 751]---> BDD-cost:    5
c ---[ 750]---> BDD-cost:    7
c ---[ 749]---> BDD-cost:    5
c ---[ 748]---> BDD-cost:    8
c ---[ 747]---> BDD-cost:    4
c ---[ 745]---> Adder-cost: 2192   maxlim: 3061726   bits: 23/22
c ---[ 744]---> BDD-cost:    7
c ---[ 743]---> BDD-cost:    5
c ---[ 742]---> BDD-cost:    4
c ---[ 741]---> BDD-cost:    6
c ---[ 740]---> BDD-cost:    8
c ---[ 739]---> BDD-cost:    5
c ---[ 738]---> BDD-cost:    5
c ---[ 737]---> BDD-cost:    8
c ---[ 736]---> BDD-cost:    7
c ---[ 735]---> BDD-cost:    6
c ---[ 733]---> Adder-cost: 2162   maxlim: 2943962   bits: 23/22
c ---[ 732]---> BDD-cost:    3
c ---[ 731]---> BDD-cost:    6
c ---[ 730]---> BDD-cost:   18
c ---[ 729]---> BDD-cost:    8
c ---[ 728]---> BDD-cost:    8
c ---[ 727]---> BDD-cost:    5
c ---[ 726]---> BDD-cost:    7
c ---[ 725]---> BDD-cost:    6
c ---[ 724]---> BDD-cost:    8
c ---[ 723]---> BDD-cost:    8
c ---[ 721]---> Adder-cost: 2194   maxlim: 2976733   bits: 23/22
c ---[ 720]---> BDD-cost:    8
c ---[ 719]---> BDD-cost:   20
c ---[ 718]---> BDD-cost:   22
c ---[ 717]---> BDD-cost:    6
c ---[ 716]---> BDD-cost:   18
c ---[ 715]---> BDD-cost:   18
c ---[ 714]---> BDD-cost:    8
c ---[ 713]---> BDD-cost:    3
c ---[ 712]---> BDD-cost:    7
c ---[ 711]---> BDD-cost:    6
c ---[ 709]---> Adder-cost: 2032   maxlim: 2712542   bits: 23/22
c ---[ 708]---> BDD-cost:    8
c ---[ 707]---> BDD-cost:   22
c ---[ 706]---> BDD-cost:    8
c ---[ 705]---> BDD-cost:    5
c ---[ 704]---> BDD-cost:    3
c ---[ 703]---> BDD-cost:   19
c ---[ 702]---> BDD-cost:    5
c ---[ 701]---> BDD-cost:    7
c ---[ 700]---> BDD-cost:    6
c ---[ 699]---> BDD-cost:    5
c ---[ 697]---> Adder-cost: 2150   maxlim: 2696158   bits: 23/22
c ---[ 696]---> BDD-cost:   19
c ---[ 695]---> BDD-cost:    8
c ---[ 694]---> BDD-cost:   17
c ---[ 693]---> BDD-cost:    7
c ---[ 692]---> BDD-cost:    4
c ---[ 691]---> BDD-cost:    6
c ---[ 690]---> BDD-cost:    7
c ---[ 689]---> BDD-cost:    8
c ---[ 688]---> BDD-cost:    7
c ---[ 687]---> BDD-cost:    5
c ---[ 685]---> Adder-cost: 2294   maxlim: 2912221   bits: 23/22
c ---[ 684]---> BDD-cost:    4
c ---[ 683]---> BDD-cost:    7
c ---[ 682]---> BDD-cost:    4
c ---[ 681]---> BDD-cost:   22
c ---[ 680]---> BDD-cost:    6
c ---[ 679]---> BDD-cost:    6
c ---[ 678]---> BDD-cost:    8
c ---[ 677]---> BDD-cost:    7
c ---[ 676]---> BDD-cost:    4
c ---[ 675]---> BDD-cost:    6
c ---[ 673]---> Adder-cost: 2282   maxlim: 3110877   bits: 23/22
c ---[ 672]---> BDD-cost:    6
c ---[ 671]---> BDD-cost:   22
c ---[ 670]---> BDD-cost:   18
c ---[ 669]---> BDD-cost:    5
c ---[ 668]---> BDD-cost:    6
c ---[ 667]---> BDD-cost:   22
c ---[ 666]---> BDD-cost:    5
c ---[ 665]---> BDD-cost:    7
c ---[ 664]---> BDD-cost:    7
c ---[ 663]---> BDD-cost:    6
c ---[ 661]---> Adder-cost: 2220   maxlim: 3010526   bits: 23/22
c ---[ 660]---> BDD-cost:    6
c ---[ 659]---> BDD-cost:    8
c ---[ 658]---> BDD-cost:    7
c ---[ 657]---> BDD-cost:   22
c ---[ 656]---> BDD-cost:    5
c ---[ 655]---> BDD-cost:    8
c ---[ 654]---> BDD-cost:    7
c ---[ 653]---> BDD-cost:    4
c ---[ 652]---> BDD-cost:    8
c ---[ 651]---> BDD-cost:    7
c ---[ 649]---> BDD-cost:   67
c ---[ 647]---> Adder-cost: 2178   maxlim: 3334108   bits: 23/22
c ---[ 646]---> BDD-cost:    7
c ---[ 645]---> BDD-cost:    4
c ---[ 644]---> BDD-cost:    6
c ---[ 643]---> BDD-cost:    8
c ---[ 642]---> BDD-cost:    6
c ---[ 641]---> BDD-cost:    8
c ---[ 640]---> BDD-cost:    7
c ---[ 639]---> BDD-cost:    4
c ---[ 638]---> BDD-cost:    7
c ---[ 637]---> BDD-cost:    7
c ---[ 635]---> Adder-cost: 2182   maxlim: 3058652   bits: 23/22
c ---[ 634]---> BDD-cost:    5
c ---[ 633]---> BDD-cost:    7
c ---[ 632]---> BDD-cost:   20
c ---[ 631]---> BDD-cost:    7
c ---[ 630]---> BDD-cost:    6
c ---[ 629]---> BDD-cost:    7
c ---[ 628]---> BDD-cost:    8
c ---[ 627]---> BDD-cost:    3
c ---[ 626]---> BDD-cost:    8
c ---[ 625]---> BDD-cost:    8
c ---[ 623]---> Adder-cost: 2348   maxlim: 2894812   bits: 23/22
c ---[ 622]---> BDD-cost:    5
c ---[ 621]---> BDD-cost:    5
c ---[ 620]---> BDD-cost:    3
c ---[ 619]---> BDD-cost:    5
c ---[ 618]---> BDD-cost:    4
c ---[ 617]---> BDD-cost:    4
c ---[ 616]---> BDD-cost:    5
c ---[ 615]---> BDD-cost:    7
c ---[ 614]---> BDD-cost:    6
c ---[ 613]---> BDD-cost:    6
c ---[ 611]---> Adder-cost: 2218   maxlim: 2889693   bits: 23/22
c ---[ 610]---> BDD-cost:    7
c ---[ 609]---> BDD-cost:    7
c ---[ 608]---> BDD-cost:    7
c ---[ 607]---> BDD-cost:    5
c ---[ 606]---> BDD-cost:   20
c ---[ 605]---> BDD-cost:   18
c ---[ 604]---> BDD-cost:    7
c ---[ 603]---> BDD-cost:    5
c ---[ 602]---> BDD-cost:    7
c ---[ 601]---> BDD-cost:    6
c ---[ 599]---> Adder-cost: 2072   maxlim: 2930655   bits: 23/22
c ---[ 598]---> BDD-cost:    6
c ---[ 597]---> BDD-cost:    7
c ---[ 596]---> BDD-cost:    7
c ---[ 595]---> BDD-cost:    7
c ---[ 594]---> BDD-cost:    8
c ---[ 593]---> BDD-cost:    7
c ---[ 592]---> BDD-cost:   19
c ---[ 591]---> BDD-cost:    3
c ---[ 590]---> BDD-cost:   22
c ---[ 589]---> BDD-cost:    8
c ---[ 587]---> Adder-cost: 2184   maxlim: 2863070   bits: 23/22
c ---[ 586]---> BDD-cost:    4
c ---[ 585]---> BDD-cost:    6
c ---[ 584]---> BDD-cost:    8
c ---[ 583]---> BDD-cost:    6
c ---[ 582]---> BDD-cost:    5
c ---[ 581]---> BDD-cost:    8
c ---[ 580]---> BDD-cost:    8
c ---[ 579]---> BDD-cost:    6
c ---[ 578]---> BDD-cost:    7
c ---[ 577]---> BDD-cost:   18
c ---[ 575]---> Adder-cost: 2030   maxlim: 2764767   bits: 23/22
c ---[ 574]---> BDD-cost:    5
c ---[ 573]---> BDD-cost:    7
c ---[ 572]---> BDD-cost:    6
c ---[ 571]---> BDD-cost:    5
c ---[ 570]---> BDD-cost:    6
c ---[ 569]---> BDD-cost:    7
c ---[ 568]---> BDD-cost:   21
c ---[ 567]---> BDD-cost:    4
c ---[ 566]---> BDD-cost:    4
c ---[ 565]---> BDD-cost:    8
c ---[ 563]---> Adder-cost: 2096   maxlim: 2895839   bits: 23/22
c ---[ 562]---> BDD-cost:    7
c ---[ 561]---> BDD-cost:    6
c ---[ 560]---> BDD-cost:    8
c ---[ 559]---> BDD-cost:    5
c ---[ 558]---> BDD-cost:    5
c ---[ 557]---> BDD-cost:    6
c ---[ 556]---> BDD-cost:    7
c ---[ 555]---> BDD-cost:    8
c ---[ 554]---> BDD-cost:    8
c ---[ 553]---> BDD-cost:    7
c ---[ 551]---> Adder-cost: 2270   maxlim: 3108827   bits: 23/22
c ---[ 550]---> BDD-cost:    5
c ---[ 549]---> BDD-cost:    3
c ---[ 548]---> BDD-cost:    4
c ---[ 547]---> BDD-cost:    5
c ---[ 546]---> BDD-cost:   22
c ---[ 545]---> BDD-cost:    6
c ---[ 544]---> BDD-cost:    7
c ---[ 543]---> BDD-cost:   19
c ---[ 542]---> BDD-cost:    3
c ---[ 541]---> BDD-cost:    8
c ---[ 539]---> Adder-cost: 2254   maxlim: 3202013   bits: 23/22
c ---[ 538]---> BDD-cost:    7
c ---[ 537]---> BDD-cost:    7
c ---[ 536]---> BDD-cost:    3
c ---[ 535]---> BDD-cost:    7
c ---[ 534]---> BDD-cost:   19
c ---[ 533]---> BDD-cost:    7
c ---[ 532]---> BDD-cost:    6
c ---[ 531]---> BDD-cost:    3
c ---[ 530]---> BDD-cost:    4
c ---[ 529]---> BDD-cost:    4
c ---[ 527]---> BDD-cost:   63
c ---[ 525]---> Adder-cost: 2152   maxlim: 2366430   bits: 23/22
c ---[ 524]---> BDD-cost:    3
c ---[ 523]---> BDD-cost:    6
c ---[ 522]---> BDD-cost:    7
c ---[ 521]---> BDD-cost:    5
c ---[ 520]---> BDD-cost:    8
c ---[ 519]---> BDD-cost:    8
c ---[ 518]---> BDD-cost:    8
c ---[ 517]---> BDD-cost:    7
c ---[ 516]---> BDD-cost:    7
c ---[ 515]---> BDD-cost:    8
c ---[ 513]---> Adder-cost: 2266   maxlim: 3364827   bits: 23/22
c ---[ 512]---> BDD-cost:    6
c ---[ 511]---> BDD-cost:    6
c ---[ 510]---> BDD-cost:   21
c ---[ 509]---> BDD-cost:    8
c ---[ 508]---> BDD-cost:    5
c ---[ 507]---> BDD-cost:    4
c ---[ 506]---> BDD-cost:    8
c ---[ 505]---> BDD-cost:   21
c ---[ 504]---> BDD-cost:    7
c ---[ 503]---> BDD-cost:    7
c ---[ 501]---> Adder-cost: 2314   maxlim: 2833370   bits: 23/22
c ---[ 500]---> BDD-cost:    8
c ---[ 499]---> BDD-cost:    3
c ---[ 498]---> BDD-cost:    8
c ---[ 497]---> BDD-cost:    7
c ---[ 496]---> BDD-cost:    7
c ---[ 495]---> BDD-cost:    8
c ---[ 494]---> BDD-cost:    8
c ---[ 493]---> BDD-cost:    8
c ---[ 492]---> BDD-cost:    6
c ---[ 491]---> BDD-cost:    7
c ---[ 489]---> Adder-cost: 2288   maxlim: 3790811   bits: 23/22
c ---[ 488]---> BDD-cost:    5
c ---[ 487]---> BDD-cost:    8
c ---[ 486]---> BDD-cost:   22
c ---[ 485]---> BDD-cost:   22
c ---[ 484]---> BDD-cost:    8
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    5
c ---[ 481]---> BDD-cost:    8
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    8
c ---[ 477]---> Adder-cost: 2324   maxlim: 2880476   bits: 23/22
c ---[ 476]---> BDD-cost:    7
c ---[ 475]---> BDD-cost:    4
c ---[ 474]---> BDD-cost:    5
c ---[ 473]---> BDD-cost:    6
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    8
c ---[ 470]---> BDD-cost:    8
c ---[ 469]---> BDD-cost:    6
c ---[ 468]---> BDD-cost:    8
c ---[ 467]---> BDD-cost:    5
c ---[ 465]---> Adder-cost: 2124   maxlim: 2808797   bits: 23/22
c ---[ 464]---> BDD-cost:    6
c ---[ 463]---> BDD-cost:    8
c ---[ 462]---> BDD-cost:    7
c ---[ 461]---> BDD-cost:    5
c ---[ 460]---> BDD-cost:    3
c ---[ 459]---> BDD-cost:    4
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 456]---> BDD-cost:    6
c ---[ 455]---> BDD-cost:    5
c ---[ 453]---> Adder-cost: 2224   maxlim: 2775007   bits: 23/22
c ---[ 452]---> BDD-cost:    3
c ---[ 451]---> BDD-cost:    5
c ---[ 450]---> BDD-cost:    7
c ---[ 449]---> BDD-cost:    6
c ---[ 448]---> BDD-cost:   20
c ---[ 447]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:    6
c ---[ 445]---> BDD-cost:    6
c ---[ 444]---> BDD-cost:    8
c ---[ 443]---> BDD-cost:    6
c ---[ 441]---> Adder-cost: 2096   maxlim: 2678751   bits: 23/22
c ---[ 440]---> BDD-cost:    6
c ---[ 439]---> BDD-cost:    6
c ---[ 438]---> BDD-cost:    8
c ---[ 437]---> BDD-cost:    7
c ---[ 436]---> BDD-cost:    5
c ---[ 435]---> BDD-cost:    8
c ---[ 434]---> BDD-cost:    5
c ---[ 433]---> BDD-cost:    6
c ---[ 432]---> BDD-cost:    7
c ---[ 431]---> BDD-cost:    8
c ---[ 429]---> Adder-cost: 2134   maxlim: 2991074   bits: 23/22
c ---[ 428]---> BDD-cost:    3
c ---[ 427]---> BDD-cost:   19
c ---[ 426]---> BDD-cost:    8
c ---[ 425]---> BDD-cost:    6
c ---[ 424]---> BDD-cost:   21
c ---[ 423]---> BDD-cost:    6
c ---[ 422]---> BDD-cost:    4
c ---[ 421]---> BDD-cost:    3
c ---[ 420]---> BDD-cost:    7
c ---[ 419]---> BDD-cost:    7
c ---[ 418]---> BDD-cost:    8
c ---[ 417]---> BDD-cost:    7
c ---[ 416]---> BDD-cost:    3
c ---[ 415]---> BDD-cost:    7
c ---[ 414]---> BDD-cost:    7
c ---[ 413]---> BDD-cost:    4
c ---[ 412]---> BDD-cost:    8
c ---[ 411]---> BDD-cost:   20
c ---[ 410]---> BDD-cost:    5
c ---[ 409]---> BDD-cost:    8
c ---[ 408]---> BDD-cost:    3
c ---[ 406]---> BDD-cost:   71
c ---[ 405]---> BDD-cost:    6
c ---[ 404]---> BDD-cost:    7
c ---[ 403]---> BDD-cost:    8
c ---[ 402]---> BDD-cost:    5
c ---[ 401]---> BDD-cost:   21
c ---[ 400]---> BDD-cost:    5
c ---[ 399]---> BDD-cost:    5
c ---[ 398]---> BDD-cost:    8
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    5
c ---[ 395]---> BDD-cost:    8
c ---[ 394]---> BDD-cost:    8
c ---[ 393]---> BDD-cost:    6
c ---[ 392]---> BDD-cost:    6
c ---[ 391]---> BDD-cost:    8
c ---[ 390]---> BDD-cost:    8
c ---[ 389]---> BDD-cost:    7
c ---[ 388]---> BDD-cost:    7
c ---[ 387]---> BDD-cost:    3
c ---[ 386]---> BDD-cost:    6
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:   22
c ---[ 383]---> BDD-cost:    8
c ---[ 382]---> BDD-cost:    6
c ---[ 381]---> BDD-cost:    3
c ---[ 380]---> BDD-cost:    8
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    6
c ---[ 377]---> BDD-cost:    3
c ---[ 376]---> BDD-cost:   21
c ---[ 375]---> BDD-cost:    8
c ---[ 374]---> BDD-cost:    3
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:   20
c ---[ 371]---> BDD-cost:    8
c ---[ 370]---> BDD-cost:    7
c ---[ 369]---> BDD-cost:   22
c ---[ 368]---> BDD-cost:   18
c ---[ 367]---> BDD-cost:    8
c ---[ 366]---> BDD-cost:    8
c ---[ 365]---> BDD-cost:    4
c ---[ 364]---> BDD-cost:    7
c ---[ 363]---> BDD-cost:    7
c ---[ 362]---> BDD-cost:   22
c ---[ 361]---> BDD-cost:    8
c ---[ 360]---> BDD-cost:    5
c ---[ 359]---> BDD-cost:    8
c ---[ 358]---> BDD-cost:    7
c ---[ 357]---> BDD-cost:   19
c ---[ 356]---> BDD-cost:    6
c ---[ 355]---> BDD-cost:    7
c ---[ 354]---> BDD-cost:    5
c ---[ 353]---> BDD-cost:    5
c ---[ 352]---> BDD-cost:    8
c ---[ 351]---> BDD-cost:    4
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    6
c ---[ 348]---> BDD-cost:    8
c ---[ 347]---> BDD-cost:    3
c ---[ 346]---> BDD-cost:    8
c ---[ 345]---> BDD-cost:    6
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:    6
c ---[ 342]---> BDD-cost:    7
c ---[ 341]---> BDD-cost:    7
c ---[ 340]---> BDD-cost:    8
c ---[ 339]---> BDD-cost:    5
c ---[ 338]---> BDD-cost:    8
c ---[ 337]---> BDD-cost:    7
c ---[ 336]---> BDD-cost:    8
c ---[ 335]---> BDD-cost:    5
c ---[ 334]---> BDD-cost:    6
c ---[ 333]---> BDD-cost:   22
c ---[ 332]---> BDD-cost:   20
c ---[ 331]---> BDD-cost:    7
c ---[ 330]---> BDD-cost:    4
c ---[ 329]---> BDD-cost:   17
c ---[ 328]---> BDD-cost:    6
c ---[ 327]---> BDD-cost:    8
c ---[ 326]---> BDD-cost:    8
c ---[ 325]---> BDD-cost:    6
c ---[ 324]---> BDD-cost:    4
c ---[ 323]---> BDD-cost:    6
c ---[ 322]---> BDD-cost:    3
c ---[ 321]---> BDD-cost:    7
c ---[ 320]---> BDD-cost:    7
c ---[ 319]---> BDD-cost:    7
c ---[ 318]---> BDD-cost:    6
c ---[ 317]---> BDD-cost:   20
c ---[ 316]---> BDD-cost:    8
c ---[ 315]---> BDD-cost:    6
c ---[ 314]---> BDD-cost:    8
c ---[ 313]---> BDD-cost:    3
c ---[ 312]---> BDD-cost:    6
c ---[ 311]---> BDD-cost:    7
c ---[ 310]---> BDD-cost:    5
c ---[ 309]---> BDD-cost:    6
c ---[ 308]---> BDD-cost:   22
c ---[ 307]---> BDD-cost:   20
c ---[ 306]---> BDD-cost:    7
c ---[ 305]---> BDD-cost:   17
c ---[ 304]---> BDD-cost:    7
c ---[ 303]---> BDD-cost:    3
c ---[ 302]---> BDD-cost:   22
c ---[ 301]---> BDD-cost:   22
c ---[ 300]---> BDD-cost:    5
c ---[ 299]---> BDD-cost:    7
c ---[ 298]---> BDD-cost:   20
c ---[ 297]---> BDD-cost:    5
c ---[ 296]---> BDD-cost:    5
c ---[ 294]---> BDD-cost:   65
c ---[ 293]---> BDD-cost:    5
c ---[ 292]---> BDD-cost:    8
c ---[ 291]---> BDD-cost:    3
c ---[ 290]---> BDD-cost:    7
c ---[ 289]---> BDD-cost:    3
c ---[ 288]---> BDD-cost:    8
c ---[ 287]---> BDD-cost:    7
c ---[ 286]---> BDD-cost:    5
c ---[ 285]---> BDD-cost:    7
c ---[ 284]---> BDD-cost:    7
c ---[ 283]---> BDD-cost:   18
c ---[ 282]---> BDD-cost:    7
c ---[ 281]---> BDD-cost:    6
c ---[ 280]---> BDD-cost:   22
c ---[ 279]---> BDD-cost:    6
c ---[ 278]---> BDD-cost:    3
c ---[ 277]---> BDD-cost:    5
c ---[ 276]---> BDD-cost:   19
c ---[ 275]---> BDD-cost:    8
c ---[ 274]---> BDD-cost:    8
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost:    8
c ---[ 271]---> BDD-cost:    8
c ---[ 270]---> BDD-cost:    7
c ---[ 269]---> BDD-cost:    6
c ---[ 268]---> BDD-cost:    8
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    8
c ---[ 264]---> BDD-cost:    5
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    3
c ---[ 261]---> BDD-cost:    6
c ---[ 260]---> BDD-cost:    5
c ---[ 259]---> BDD-cost:    8
c ---[ 258]---> BDD-cost:    8
c ---[ 257]---> BDD-cost:    7
c ---[ 256]---> BDD-cost:   19
c ---[ 255]---> BDD-cost:    8
c ---[ 254]---> BDD-cost:    8
c ---[ 253]---> BDD-cost:    6
c ---[ 252]---> BDD-cost:   20
c ---[ 251]---> BDD-cost:    8
c ---[ 250]---> BDD-cost:    7
c ---[ 249]---> BDD-cost:    8
c ---[ 248]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    8
c ---[ 246]---> BDD-cost:    7
c ---[ 245]---> BDD-cost:    4
c ---[ 244]---> BDD-cost:    3
c ---[ 243]---> BDD-cost:    3
c ---[ 242]---> BDD-cost:    7
c ---[ 241]---> BDD-cost:    7
c ---[ 240]---> BDD-cost:    4
c ---[ 239]---> BDD-cost:    3
c ---[ 238]---> BDD-cost:   19
c ---[ 237]---> BDD-cost:    8
c ---[ 236]---> BDD-cost:    6
c ---[ 235]---> BDD-cost:    8
c ---[ 234]---> BDD-cost:    6
c ---[ 233]---> BDD-cost:   21
c ---[ 232]---> BDD-cost:    6
c ---[ 231]---> BDD-cost:    6
c ---[ 230]---> BDD-cost:    8
c ---[ 229]---> BDD-cost:   21
c ---[ 228]---> BDD-cost:    7
c ---[ 227]---> BDD-cost:    8
c ---[ 226]---> BDD-cost:    8
c ---[ 225]---> BDD-cost:    8
c ---[ 224]---> BDD-cost:   21
c ---[ 223]---> BDD-cost:    6
c ---[ 222]---> BDD-cost:    7
c ---[ 221]---> BDD-cost:    6
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:   20
c ---[ 218]---> BDD-cost:   19
c ---[ 217]---> BDD-cost:   21
c ---[ 216]---> BDD-cost:    7
c ---[ 215]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:    3
c ---[ 213]---> BDD-cost:    4
c ---[ 212]---> BDD-cost:    8
c ---[ 211]---> BDD-cost:    6
c ---[ 210]---> BDD-cost:    6
c ---[ 209]---> BDD-cost:    8
c ---[ 208]---> BDD-cost:    3
c ---[ 207]---> BDD-cost:    7
c ---[ 206]---> BDD-cost:    7
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    6
c ---[ 203]---> BDD-cost:    5
c ---[ 202]---> BDD-cost:    7
c ---[ 201]---> BDD-cost:    4
c ---[ 200]---> BDD-cost:    6
c ---[ 199]---> BDD-cost:    7
c ---[ 198]---> BDD-cost:    7
c ---[ 197]---> BDD-cost:   21
c ---[ 196]---> BDD-cost:   21
c ---[ 195]---> BDD-cost:    3
c ---[ 194]---> BDD-cost:    8
c ---[ 193]---> BDD-cost:    6
c ---[ 192]---> BDD-cost:    8
c ---[ 191]---> BDD-cost:    6
c ---[ 190]---> BDD-cost:    8
c ---[ 189]---> BDD-cost:    6
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:    6
c ---[ 186]---> BDD-cost:    6
c ---[ 185]---> BDD-cost:    7
c ---[ 184]---> BDD-cost:    7
c ---[ 183]---> BDD-cost:    1
c ---[ 182]---> BDD-cost:    1
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:    1
c ---[ 174]---> BDD-cost:    1
c ---[ 173]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> BDD-cost:    1
c ---[ 169]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 167]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 165]---> BDD-cost:    1
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> BDD-cost:    1
c ---[ 162]---> BDD-cost:    1
c ---[ 161]---> BDD-cost:    1
c ---[ 160]---> BDD-cost:    1
c ---[ 159]---> BDD-cost:    1
c ---[ 158]---> BDD-cost:    1
c ---[ 157]---> BDD-cost:    1
c ---[ 156]---> BDD-cost:    1
c ---[ 155]---> BDD-cost:    1
c ---[ 154]---> BDD-cost:    1
c ---[ 153]---> BDD-cost:    1
c ---[ 152]---> BDD-cost:    1
c ---[ 151]---> BDD-cost:    1
c ---[ 150]---> BDD-cost:    1
c ---[ 149]---> BDD-cost:    1
c ---[ 148]---> BDD-cost:    1
c ---[ 147]---> BDD-cost:    1
c ---[ 146]---> BDD-cost:    1
c ---[ 145]---> BDD-cost:    1
c ---[ 144]---> BDD-cost:    1
c ---[ 143]---> BDD-cost:    1
c ---[ 142]---> BDD-cost:    1
c ---[ 141]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:    1
c ---[ 139]---> BDD-cost:    1
c ---[ 138]---> BDD-cost:    1
c ---[ 137]---> BDD-cost:    1
c ---[ 136]---> BDD-cost:    1
c ---[ 135]---> BDD-cost:    1
c ---[ 134]---> BDD-cost:    1
c ---[ 133]---> BDD-cost:    1
c ---[ 132]---> BDD-cost:    1
c ---[ 131]---> BDD-cost:    1
c ---[ 130]---> BDD-cost:    1
c ---[ 129]---> BDD-cost:    1
c ---[ 128]---> BDD-cost:    1
c ---[ 127]---> BDD-cost:    1
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:    1
c ---[ 122]---> BDD-cost:    1
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:    1
c ---[ 118]---> BDD-cost:    1
c ---[ 117]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:    1
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:    1
c ---[ 110]---> BDD-cost:    1
c ---[ 109]---> BDD-cost:    1
c ---[ 108]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:    1
c ---[ 106]---> BDD-cost:    1
c ---[ 105]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[ 103]---> BDD-cost:    1
c ---[ 102]---> BDD-cost:    1
c ---[ 101]---> BDD-cost:    1
c ---[ 100]---> BDD-cost:    1
c ---[  99]---> BDD-cost:    1
c ---[  98]---> BDD-cost:    1
c ---[  97]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  95]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  93]---> BDD-cost:    1
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:    1
c ---[  90]---> BDD-cost:    1
c ---[  89]---> BDD-cost:    1
c ---[  88]---> BDD-cost:    1
c ---[  87]---> BDD-cost:    1
c ---[  86]---> BDD-cost:    1
c ---[  85]---> BDD-cost:    1
c ---[  84]---> BDD-cost:    1
c ---[  83]---> BDD-cost:    1
c ---[  82]---> BDD-cost:    1
c ---[  81]---> BDD-cost:    1
c ---[  80]---> BDD-cost:    1
c ---[  79]---> BDD-cost:    1
c ---[  78]---> BDD-cost:    1
c ---[  77]---> BDD-cost:    1
c ---[  76]---> BDD-cost:    1
c ---[  75]---> BDD-cost:    1
c ---[  74]---> BDD-cost:    1
c ---[  73]---> BDD-cost:    1
c ---[  72]---> BDD-cost:    1
c ---[  71]---> BDD-cost:    1
c ---[  70]---> BDD-cost:    1
c ---[  69]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  67]---> BDD-cost:    1
c ---[  66]---> BDD-cost:    1
c ---[  65]---> BDD-cost:    1
c ---[  64]---> BDD-cost:    1
c ---[  63]---> BDD-cost:    1
c ---[  62]---> BDD-cost:    1
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:    1
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:    1
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:    1
c ---[  46]---> BDD-cost:    1
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    1
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:    1
c ---[  14]---> BDD-cost:    1
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:    1
c ---[  10]---> BDD-cost:    1
c ---[   9]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:    1
c ---[   6]---> BDD-cost:    1
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  633343  2209544 |  211114       0        0     nan |  0.000 % |
c |       101 |  633343  2209544 |  232225     101    25727   254.7 |  3.726 % |
c |       251 |  633317  2209456 |  255447     246    26346   107.1 |  3.728 % |
c |       476 |  633317  2209456 |  280992     471    41882    88.9 |  3.728 % |
c |       813 |  633317  2209456 |  309092     808    58307    72.2 |  3.728 % |
c |      1319 |  633309  2209430 |  340001    1313    92254    70.3 |  3.729 % |
c |      2078 |  633300  2209399 |  374001    2069   134137    64.8 |  3.730 % |
c |      3220 |  633300  2209399 |  411401    3211   265417    82.7 |  3.730 % |
c |      4928 |  633275  2209316 |  452541    4915   375378    76.4 |  3.732 % |
c |      7490 |  633214  2209109 |  497795    7463   576859    77.3 |  3.738 % |
c |     11334 |  633137  2208846 |  547575   11281   867591    76.9 |  3.746 % |
c |     17103 |  633110  2208753 |  602332   17035  1834608   107.7 |  3.748 % |
c |     25753 |  633067  2208608 |  662566   25675  3316189   129.2 |  3.752 % |
c |     38727 |  633017  2208438 |  728822   38636  6777196   175.4 |  3.757 % |
c |     58188 |  632974  2208293 |  801705   58086 11786524   202.9 |  3.761 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/3046/stat): 3046 (minisat+_script) R 3045 3046 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788459753 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/3046/statm): 174 3 169 147 0 27 0
[pid=3046] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=3047
New process pid=3048
New process pid=3049
execve syscall for /bin/sed executable
One traced child (pid=3048) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=3049) exited with status: 0
One traced child (pid=3047) exited with status: 0
New process pid=3050
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-aflow40b.opb

[startup+10.003 s]
Raw data (loadavg): 0.89 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 10939 0 0 0 904 50 0 0 22 0 1 0 1788459758 48443392 10480 4294967295 134512640 135094434 3221224432 3221213664 134780516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 11827 10480 145 145 0 11682 0
[pid=3050] vsize: 47308
Current children cumulated CPU time (s) 9.55
Current children cumulated vsize (Kb) 49432

[startup+20.0036 s]
Raw data (loadavg): 0.91 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13135 0 0 0 1881 60 0 0 25 0 1 0 1788459758 55861248 12676 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 13638 12676 145 145 0 13493 0
[pid=3050] vsize: 54552
Current children cumulated CPU time (s) 19.42
Current children cumulated vsize (Kb) 56676

[startup+30.0042 s]
Raw data (loadavg): 0.92 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13183 0 0 0 2880 60 0 0 25 0 1 0 1788459758 56057856 12724 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 13686 12724 145 145 0 13541 0
[pid=3050] vsize: 54744
Current children cumulated CPU time (s) 29.41
Current children cumulated vsize (Kb) 56868

[startup+40.0047 s]
Raw data (loadavg): 0.93 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13236 0 0 0 3879 61 0 0 25 0 1 0 1788459758 56279040 12777 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 13740 12777 145 145 0 13595 0
[pid=3050] vsize: 54960
Current children cumulated CPU time (s) 39.41
Current children cumulated vsize (Kb) 57084

[startup+50.0063 s]
Raw data (loadavg): 0.94 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13319 0 0 0 4877 61 0 0 25 0 1 0 1788459758 56614912 12860 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 13822 12860 145 145 0 13677 0
[pid=3050] vsize: 55288
Current children cumulated CPU time (s) 49.39
Current children cumulated vsize (Kb) 57412

[startup+60.0068 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13378 0 0 0 5877 62 0 0 25 0 1 0 1788459758 56856576 12919 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 13881 12919 145 145 0 13736 0
[pid=3050] vsize: 55524
Current children cumulated CPU time (s) 59.4
Current children cumulated vsize (Kb) 57648

[startup+70.0074 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13455 0 0 0 6875 63 0 0 25 0 1 0 1788459758 57171968 12996 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 13958 12996 145 145 0 13813 0
[pid=3050] vsize: 55832
Current children cumulated CPU time (s) 69.39
Current children cumulated vsize (Kb) 57956

[startup+80.0089 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13493 0 0 0 7875 63 0 0 25 0 1 0 1788459758 57335808 13034 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 13998 13034 145 145 0 13853 0
[pid=3050] vsize: 55992
Current children cumulated CPU time (s) 79.39
Current children cumulated vsize (Kb) 58116

[startup+90.0095 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13533 0 0 0 8874 64 0 0 25 0 1 0 1788459758 57495552 13074 4294967295 134512640 135094434 3221224432 3221223024 134556876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 14037 13074 145 145 0 13892 0
[pid=3050] vsize: 56148
Current children cumulated CPU time (s) 89.39
Current children cumulated vsize (Kb) 58272

[startup+100.01 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13647 0 0 0 9873 64 0 0 25 0 1 0 1788459758 57958400 13188 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 14150 13188 145 145 0 14005 0
[pid=3050] vsize: 56600
Current children cumulated CPU time (s) 99.38
Current children cumulated vsize (Kb) 58724

[startup+110.011 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13712 0 0 0 10872 64 0 0 25 0 1 0 1788459758 58224640 13253 4294967295 134512640 135094434 3221224432 3221223104 134670313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 14215 13253 145 145 0 14070 0
[pid=3050] vsize: 56860
Current children cumulated CPU time (s) 109.37
Current children cumulated vsize (Kb) 58984

[startup+120.011 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13754 0 0 0 11872 65 0 0 25 0 1 0 1788459758 58425344 13295 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 14264 13295 145 145 0 14119 0
[pid=3050] vsize: 57056
Current children cumulated CPU time (s) 119.38
Current children cumulated vsize (Kb) 59180

[startup+130.012 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13790 0 0 0 12872 65 0 0 25 0 1 0 1788459758 58568704 13331 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 14299 13331 145 145 0 14154 0
[pid=3050] vsize: 57196
Current children cumulated CPU time (s) 129.38
Current children cumulated vsize (Kb) 59320

[startup+140.012 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13819 0 0 0 13871 65 0 0 25 0 1 0 1788459758 58687488 13360 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 14328 13360 145 145 0 14183 0
[pid=3050] vsize: 57312
Current children cumulated CPU time (s) 139.37
Current children cumulated vsize (Kb) 59436

[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13903 0 0 0 14870 66 0 0 25 0 1 0 1788459758 59027456 13444 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 14411 13444 145 145 0 14266 0
[pid=3050] vsize: 57644
Current children cumulated CPU time (s) 149.37
Current children cumulated vsize (Kb) 59768

[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 13979 0 0 0 15868 67 0 0 25 0 1 0 1788459758 59338752 13520 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 14487 13520 145 145 0 14342 0
[pid=3050] vsize: 57948
Current children cumulated CPU time (s) 159.36
Current children cumulated vsize (Kb) 60072

[startup+170.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 14045 0 0 0 16866 68 0 0 25 0 1 0 1788459758 59604992 13586 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 14552 13586 145 145 0 14407 0
[pid=3050] vsize: 58208
Current children cumulated CPU time (s) 169.35
Current children cumulated vsize (Kb) 60332

[startup+180.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 14142 0 0 0 17865 68 0 0 25 0 1 0 1788459758 59998208 13683 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 14648 13683 145 145 0 14503 0
[pid=3050] vsize: 58592
Current children cumulated CPU time (s) 179.34
Current children cumulated vsize (Kb) 60716

[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 14218 0 0 0 18863 70 0 0 25 0 1 0 1788459758 60309504 13759 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 14724 13759 145 145 0 14579 0
[pid=3050] vsize: 58896
Current children cumulated CPU time (s) 189.34
Current children cumulated vsize (Kb) 61020

[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 14322 0 0 0 19861 71 0 0 25 0 1 0 1788459758 60731392 13863 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 14827 13863 145 145 0 14682 0
[pid=3050] vsize: 59308
Current children cumulated CPU time (s) 199.33
Current children cumulated vsize (Kb) 61432

[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 14455 0 0 0 20858 73 0 0 25 0 1 0 1788459758 61276160 13996 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 14960 13996 145 145 0 14815 0
[pid=3050] vsize: 59840
Current children cumulated CPU time (s) 209.32
Current children cumulated vsize (Kb) 61964

[startup+220.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 14576 0 0 0 21856 74 0 0 25 0 1 0 1788459758 61767680 14117 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 15080 14117 145 145 0 14935 0
[pid=3050] vsize: 60320
Current children cumulated CPU time (s) 219.31
Current children cumulated vsize (Kb) 62444

[startup+230.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 14638 0 0 0 22854 75 0 0 25 0 1 0 1788459758 62021632 14179 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 15142 14179 145 145 0 14997 0
[pid=3050] vsize: 60568
Current children cumulated CPU time (s) 229.3
Current children cumulated vsize (Kb) 62692

[startup+240.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 14754 0 0 0 23852 76 0 0 25 0 1 0 1788459758 62492672 14295 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 15257 14295 145 145 0 15112 0
[pid=3050] vsize: 61028
Current children cumulated CPU time (s) 239.29
Current children cumulated vsize (Kb) 63152

[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 14873 0 0 0 24850 77 0 0 25 0 1 0 1788459758 62980096 14414 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 15376 14414 145 145 0 15231 0
[pid=3050] vsize: 61504
Current children cumulated CPU time (s) 249.28
Current children cumulated vsize (Kb) 63628

[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 15011 0 0 0 25848 78 0 0 25 0 1 0 1788459758 63606784 14552 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 15529 14552 145 145 0 15384 0
[pid=3050] vsize: 62116
Current children cumulated CPU time (s) 259.27
Current children cumulated vsize (Kb) 64240

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 15100 0 0 0 26845 79 0 0 25 0 1 0 1788459758 63967232 14641 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 15617 14641 145 145 0 15472 0
[pid=3050] vsize: 62468
Current children cumulated CPU time (s) 269.25
Current children cumulated vsize (Kb) 64592

[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 15213 0 0 0 27843 80 0 0 25 0 1 0 1788459758 64430080 14754 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 15730 14754 145 145 0 15585 0
[pid=3050] vsize: 62920
Current children cumulated CPU time (s) 279.24
Current children cumulated vsize (Kb) 65044

[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 15267 0 0 0 28842 81 0 0 25 0 1 0 1788459758 64647168 14808 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 15783 14808 145 145 0 15638 0
[pid=3050] vsize: 63132
Current children cumulated CPU time (s) 289.24
Current children cumulated vsize (Kb) 65256

[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 15371 0 0 0 29840 81 0 0 25 0 1 0 1788459758 65069056 14912 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 15886 14912 145 145 0 15741 0
[pid=3050] vsize: 63544
Current children cumulated CPU time (s) 299.22
Current children cumulated vsize (Kb) 65668

[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 15490 0 0 0 30838 82 0 0 25 0 1 0 1788459758 65556480 15031 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 16005 15031 145 145 0 15860 0
[pid=3050] vsize: 64020
Current children cumulated CPU time (s) 309.21
Current children cumulated vsize (Kb) 66144

[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 15556 0 0 0 31837 83 0 0 25 0 1 0 1788459758 65822720 15097 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 16070 15097 145 145 0 15925 0
[pid=3050] vsize: 64280
Current children cumulated CPU time (s) 319.21
Current children cumulated vsize (Kb) 66404

[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 15629 0 0 0 32836 84 0 0 25 0 1 0 1788459758 66117632 15170 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 16142 15170 145 145 0 15997 0
[pid=3050] vsize: 64568
Current children cumulated CPU time (s) 329.21
Current children cumulated vsize (Kb) 66692

[startup+340.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 15706 0 0 0 33834 85 0 0 25 0 1 0 1788459758 66433024 15247 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 16219 15247 145 145 0 16074 0
[pid=3050] vsize: 64876
Current children cumulated CPU time (s) 339.2
Current children cumulated vsize (Kb) 67000

[startup+350.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 15812 0 0 0 34832 86 0 0 25 0 1 0 1788459758 66863104 15353 4294967295 134512640 135094434 3221224432 3221223056 134557691 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 16324 15353 145 145 0 16179 0
[pid=3050] vsize: 65296
Current children cumulated CPU time (s) 349.19
Current children cumulated vsize (Kb) 67420

[startup+360.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 16030 0 0 0 35828 87 0 0 25 0 1 0 1788459758 67751936 15571 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 16541 15571 145 145 0 16396 0
[pid=3050] vsize: 66164
Current children cumulated CPU time (s) 359.16
Current children cumulated vsize (Kb) 68288

[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 16190 0 0 0 36825 89 0 0 25 0 1 0 1788459758 68407296 15731 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 16701 15731 145 145 0 16556 0
[pid=3050] vsize: 66804
Current children cumulated CPU time (s) 369.15
Current children cumulated vsize (Kb) 68928

[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 16306 0 0 0 37822 90 0 0 25 0 1 0 1788459758 68878336 15847 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 16816 15847 145 145 0 16671 0
[pid=3050] vsize: 67264
Current children cumulated CPU time (s) 379.13
Current children cumulated vsize (Kb) 69388

[startup+390.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 16442 0 0 0 38819 92 0 0 25 0 1 0 1788459758 69435392 15983 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 16952 15983 145 145 0 16807 0
[pid=3050] vsize: 67808
Current children cumulated CPU time (s) 389.12
Current children cumulated vsize (Kb) 69932

[startup+400.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 16642 0 0 0 39816 93 0 0 25 0 1 0 1788459758 70250496 16183 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 17151 16183 145 145 0 17006 0
[pid=3050] vsize: 68604
Current children cumulated CPU time (s) 399.1
Current children cumulated vsize (Kb) 70728

[startup+410.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 16763 0 0 0 40813 94 0 0 25 0 1 0 1788459758 70746112 16304 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 17272 16304 145 145 0 17127 0
[pid=3050] vsize: 69088
Current children cumulated CPU time (s) 409.08
Current children cumulated vsize (Kb) 71212

[startup+420.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 16985 0 0 0 41808 97 0 0 25 0 1 0 1788459758 71651328 16526 4294967295 134512640 135094434 3221224432 3221223104 134555274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 17493 16526 145 145 0 17348 0
[pid=3050] vsize: 69972
Current children cumulated CPU time (s) 419.06
Current children cumulated vsize (Kb) 72096

[startup+430.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 17267 0 0 0 42803 99 0 0 25 0 1 0 1788459758 72802304 16808 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 17774 16808 145 145 0 17629 0
[pid=3050] vsize: 71096
Current children cumulated CPU time (s) 429.03
Current children cumulated vsize (Kb) 73220

[startup+440.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 17523 0 0 0 43798 101 0 0 25 0 1 0 1788459758 73850880 17064 4294967295 134512640 135094434 3221224432 3221223088 134557832 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 18030 17064 145 145 0 17885 0
[pid=3050] vsize: 72120
Current children cumulated CPU time (s) 439
Current children cumulated vsize (Kb) 74244

[startup+450.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 17808 0 0 0 44793 102 0 0 25 0 1 0 1788459758 75014144 17349 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 18314 17349 145 145 0 18169 0
[pid=3050] vsize: 73256
Current children cumulated CPU time (s) 448.96
Current children cumulated vsize (Kb) 75380

[startup+460.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 18093 0 0 0 45789 104 0 0 25 0 1 0 1788459758 76177408 17634 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 18598 17634 145 145 0 18453 0
[pid=3050] vsize: 74392
Current children cumulated CPU time (s) 458.94
Current children cumulated vsize (Kb) 76516

[startup+470.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 18427 0 0 0 46782 106 0 0 25 0 1 0 1788459758 77541376 17968 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 18931 17968 145 145 0 18786 0
[pid=3050] vsize: 75724
Current children cumulated CPU time (s) 468.89
Current children cumulated vsize (Kb) 77848

[startup+480.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 18755 0 0 0 47776 109 0 0 25 0 1 0 1788459758 78884864 18296 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 19259 18296 145 145 0 19114 0
[pid=3050] vsize: 77036
Current children cumulated CPU time (s) 478.86
Current children cumulated vsize (Kb) 79160

[startup+490.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 18923 0 0 0 48774 110 0 0 25 0 1 0 1788459758 79572992 18464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 19427 18464 145 145 0 19282 0
[pid=3050] vsize: 77708
Current children cumulated CPU time (s) 488.85
Current children cumulated vsize (Kb) 79832

[startup+500.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 18983 0 0 0 49773 110 0 0 25 0 1 0 1788459758 79818752 18524 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 19487 18524 145 145 0 19342 0
[pid=3050] vsize: 77948
Current children cumulated CPU time (s) 498.84
Current children cumulated vsize (Kb) 80072

[startup+510.038 s]
Raw data (loadavg): 0.99 0.97 0.99 3/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 19091 0 0 0 50772 111 0 0 25 0 1 0 1788459758 80388096 18632 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 19626 18632 145 145 0 19481 0
[pid=3050] vsize: 78504
Current children cumulated CPU time (s) 508.84
Current children cumulated vsize (Kb) 80628

[startup+520.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 19182 0 0 0 51770 112 0 0 25 0 1 0 1788459758 80760832 18723 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 19717 18723 145 145 0 19572 0
[pid=3050] vsize: 78868
Current children cumulated CPU time (s) 518.83
Current children cumulated vsize (Kb) 80992

[startup+530.039 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 19294 0 0 0 52767 113 0 0 25 0 1 0 1788459758 81215488 18835 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 19828 18835 145 145 0 19683 0
[pid=3050] vsize: 79312
Current children cumulated CPU time (s) 528.81
Current children cumulated vsize (Kb) 81436

[startup+540.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 19415 0 0 0 53766 114 0 0 25 0 1 0 1788459758 81711104 18956 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 19949 18956 145 145 0 19804 0
[pid=3050] vsize: 79796
Current children cumulated CPU time (s) 538.81
Current children cumulated vsize (Kb) 81920

[startup+550.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 19534 0 0 0 54763 116 0 0 25 0 1 0 1788459758 82194432 19075 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 20067 19075 145 145 0 19922 0
[pid=3050] vsize: 80268
Current children cumulated CPU time (s) 548.8
Current children cumulated vsize (Kb) 82392

[startup+560.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 19646 0 0 0 55762 117 0 0 25 0 1 0 1788459758 82653184 19187 4294967295 134512640 135094434 3221224432 3221223088 134557859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 20179 19187 145 145 0 20034 0
[pid=3050] vsize: 80716
Current children cumulated CPU time (s) 558.8
Current children cumulated vsize (Kb) 82840

[startup+570.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 19734 0 0 0 56761 117 0 0 25 0 1 0 1788459758 83009536 19275 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 20266 19275 145 145 0 20121 0
[pid=3050] vsize: 81064
Current children cumulated CPU time (s) 568.79
Current children cumulated vsize (Kb) 83188

[startup+580.042 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 19836 0 0 0 57759 118 0 0 25 0 1 0 1788459758 83427328 19377 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 20368 19377 145 145 0 20223 0
[pid=3050] vsize: 81472
Current children cumulated CPU time (s) 578.78
Current children cumulated vsize (Kb) 83596

[startup+590.043 s]
Raw data (loadavg): 0.99 0.97 0.99 1/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) T 3046 3046 22582 0 -1 0 19913 0 0 0 58758 118 0 0 25 0 1 0 1788459758 83738624 19454 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3050/statm): 20444 19454 145 145 0 20299 0
[pid=3050] vsize: 81776
Current children cumulated CPU time (s) 588.77
Current children cumulated vsize (Kb) 83900

[startup+600.043 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 19986 0 0 0 59756 119 0 0 25 0 1 0 1788459758 84037632 19527 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 20517 19527 145 145 0 20372 0
[pid=3050] vsize: 82068
Current children cumulated CPU time (s) 598.76
Current children cumulated vsize (Kb) 84192

[startup+610.044 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 20081 0 0 0 60755 120 0 0 25 0 1 0 1788459758 84426752 19622 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 20612 19622 145 145 0 20467 0
[pid=3050] vsize: 82448
Current children cumulated CPU time (s) 608.76
Current children cumulated vsize (Kb) 84572

[startup+620.044 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 20161 0 0 0 61754 121 0 0 25 0 1 0 1788459758 84750336 19702 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 20691 19702 145 145 0 20546 0
[pid=3050] vsize: 82764
Current children cumulated CPU time (s) 618.76
Current children cumulated vsize (Kb) 84888

[startup+630.045 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 20246 0 0 0 62752 122 0 0 25 0 1 0 1788459758 85098496 19787 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 20776 19787 145 145 0 20631 0
[pid=3050] vsize: 83104
Current children cumulated CPU time (s) 628.75
Current children cumulated vsize (Kb) 85228

[startup+640.045 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 20332 0 0 0 63749 123 0 0 25 0 1 0 1788459758 85446656 19873 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 20861 19873 145 145 0 20716 0
[pid=3050] vsize: 83444
Current children cumulated CPU time (s) 638.73
Current children cumulated vsize (Kb) 85568

[startup+650.046 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 20491 0 0 0 64745 125 0 0 25 0 1 0 1788459758 86093824 20032 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 21019 20032 145 145 0 20874 0
[pid=3050] vsize: 84076
Current children cumulated CPU time (s) 648.71
Current children cumulated vsize (Kb) 86200

[startup+660.047 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 20624 0 0 0 65743 125 0 0 25 0 1 0 1788459758 86638592 20165 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 21152 20165 145 145 0 21007 0
[pid=3050] vsize: 84608
Current children cumulated CPU time (s) 658.69
Current children cumulated vsize (Kb) 86732

[startup+670.047 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 20761 0 0 0 66741 126 0 0 25 0 1 0 1788459758 87195648 20302 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 21288 20302 145 145 0 21143 0
[pid=3050] vsize: 85152
Current children cumulated CPU time (s) 668.68
Current children cumulated vsize (Kb) 87276

[startup+680.048 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 20897 0 0 0 67738 128 0 0 25 0 1 0 1788459758 87748608 20438 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 21423 20438 145 145 0 21278 0
[pid=3050] vsize: 85692
Current children cumulated CPU time (s) 678.67
Current children cumulated vsize (Kb) 87816

[startup+690.048 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 21013 0 0 0 68736 129 0 0 25 0 1 0 1788459758 88223744 20554 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 21539 20554 145 145 0 21394 0
[pid=3050] vsize: 86156
Current children cumulated CPU time (s) 688.66
Current children cumulated vsize (Kb) 88280

[startup+700.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 21140 0 0 0 69734 130 0 0 25 0 1 0 1788459758 88739840 20681 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 21665 20681 145 145 0 21520 0
[pid=3050] vsize: 86660
Current children cumulated CPU time (s) 698.65
Current children cumulated vsize (Kb) 88784

[startup+710.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 21270 0 0 0 70732 131 0 0 25 0 1 0 1788459758 89272320 20811 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 21795 20811 145 145 0 21650 0
[pid=3050] vsize: 87180
Current children cumulated CPU time (s) 708.64
Current children cumulated vsize (Kb) 89304

[startup+720.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 21409 0 0 0 71729 132 0 0 25 0 1 0 1788459758 89837568 20950 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 21933 20950 145 145 0 21788 0
[pid=3050] vsize: 87732
Current children cumulated CPU time (s) 718.62
Current children cumulated vsize (Kb) 89856

[startup+730.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 21547 0 0 0 72727 133 0 0 25 0 1 0 1788459758 90402816 21088 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 22071 21088 145 145 0 21926 0
[pid=3050] vsize: 88284
Current children cumulated CPU time (s) 728.61
Current children cumulated vsize (Kb) 90408

[startup+740.05 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 21692 0 0 0 73724 135 0 0 25 0 1 0 1788459758 90992640 21233 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 22215 21233 145 145 0 22070 0
[pid=3050] vsize: 88860
Current children cumulated CPU time (s) 738.6
Current children cumulated vsize (Kb) 90984

[startup+750.051 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 21859 0 0 0 74721 136 0 0 25 0 1 0 1788459758 91676672 21400 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 22382 21400 145 145 0 22237 0
[pid=3050] vsize: 89528
Current children cumulated CPU time (s) 748.58
Current children cumulated vsize (Kb) 91652

[startup+760.051 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 21996 0 0 0 75718 138 0 0 25 0 1 0 1788459758 92233728 21537 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 22518 21537 145 145 0 22373 0
[pid=3050] vsize: 90072
Current children cumulated CPU time (s) 758.57
Current children cumulated vsize (Kb) 92196

[startup+770.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 22092 0 0 0 76717 139 0 0 25 0 1 0 1788459758 92626944 21633 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 22614 21633 145 145 0 22469 0
[pid=3050] vsize: 90456
Current children cumulated CPU time (s) 768.57
Current children cumulated vsize (Kb) 92580

[startup+780.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 22190 0 0 0 77715 139 0 0 25 0 1 0 1788459758 93028352 21731 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 22712 21731 145 145 0 22567 0
[pid=3050] vsize: 90848
Current children cumulated CPU time (s) 778.55
Current children cumulated vsize (Kb) 92972

[startup+790.053 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 22306 0 0 0 78712 141 0 0 25 0 1 0 1788459758 93499392 21847 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 22827 21847 145 145 0 22682 0
[pid=3050] vsize: 91308
Current children cumulated CPU time (s) 788.54
Current children cumulated vsize (Kb) 93432

[startup+800.054 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 22421 0 0 0 79710 143 0 0 25 0 1 0 1788459758 93970432 21962 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 22942 21962 145 145 0 22797 0
[pid=3050] vsize: 91768
Current children cumulated CPU time (s) 798.54
Current children cumulated vsize (Kb) 93892

[startup+810.055 s]
Raw data (loadavg): 0.99 0.97 0.99 3/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 22545 0 0 0 80707 144 0 0 25 0 1 0 1788459758 94474240 22086 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 23065 22086 145 145 0 22920 0
[pid=3050] vsize: 92260
Current children cumulated CPU time (s) 808.52
Current children cumulated vsize (Kb) 94384

[startup+820.056 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 22673 0 0 0 81705 146 0 0 25 0 1 0 1788459758 94998528 22214 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 23193 22214 145 145 0 23048 0
[pid=3050] vsize: 92772
Current children cumulated CPU time (s) 818.52
Current children cumulated vsize (Kb) 94896

[startup+830.056 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 22778 0 0 0 82702 147 0 0 25 0 1 0 1788459758 95424512 22319 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 23297 22319 145 145 0 23152 0
[pid=3050] vsize: 93188
Current children cumulated CPU time (s) 828.5
Current children cumulated vsize (Kb) 95312

[startup+840.057 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 22887 0 0 0 83700 148 0 0 25 0 1 0 1788459758 95870976 22428 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 23406 22428 145 145 0 23261 0
[pid=3050] vsize: 93624
Current children cumulated CPU time (s) 838.49
Current children cumulated vsize (Kb) 95748

[startup+850.058 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 22986 0 0 0 84698 149 0 0 25 0 1 0 1788459758 96272384 22527 4294967295 134512640 135094434 3221224432 3221223056 134557583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 23504 22527 145 145 0 23359 0
[pid=3050] vsize: 94016
Current children cumulated CPU time (s) 848.48
Current children cumulated vsize (Kb) 96140

[startup+860.059 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 23097 0 0 0 85696 149 0 0 25 0 1 0 1788459758 96727040 22638 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 23615 22638 145 145 0 23470 0
[pid=3050] vsize: 94460
Current children cumulated CPU time (s) 858.46
Current children cumulated vsize (Kb) 96584

[startup+870.058 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 23195 0 0 0 86694 151 0 0 25 0 1 0 1788459758 97132544 22736 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 23714 22736 145 145 0 23569 0
[pid=3050] vsize: 94856
Current children cumulated CPU time (s) 868.46
Current children cumulated vsize (Kb) 96980

[startup+880.059 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 23311 0 0 0 87692 152 0 0 25 0 1 0 1788459758 97603584 22852 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 23829 22852 145 145 0 23684 0
[pid=3050] vsize: 95316
Current children cumulated CPU time (s) 878.45
Current children cumulated vsize (Kb) 97440

[startup+890.059 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 23431 0 0 0 88689 152 0 0 25 0 1 0 1788459758 98099200 22972 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 23950 22972 145 145 0 23805 0
[pid=3050] vsize: 95800
Current children cumulated CPU time (s) 888.42
Current children cumulated vsize (Kb) 97924

[startup+900.06 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 23544 0 0 0 89687 154 0 0 25 0 1 0 1788459758 98562048 23085 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 24063 23085 145 145 0 23918 0
[pid=3050] vsize: 96252
Current children cumulated CPU time (s) 898.42
Current children cumulated vsize (Kb) 98376

[startup+910.061 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 23662 0 0 0 90685 154 0 0 25 0 1 0 1788459758 99041280 23203 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 24180 23203 145 145 0 24035 0
[pid=3050] vsize: 96720
Current children cumulated CPU time (s) 908.4
Current children cumulated vsize (Kb) 98844

[startup+920.062 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 23777 0 0 0 91683 155 0 0 25 0 1 0 1788459758 99512320 23318 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 24295 23318 145 145 0 24150 0
[pid=3050] vsize: 97180
Current children cumulated CPU time (s) 918.39
Current children cumulated vsize (Kb) 99304

[startup+930.063 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 23932 0 0 0 92680 157 0 0 25 0 1 0 1788459758 100143104 23473 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 24449 23473 145 145 0 24304 0
[pid=3050] vsize: 97796
Current children cumulated CPU time (s) 928.38
Current children cumulated vsize (Kb) 99920

[startup+940.063 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 24065 0 0 0 93677 158 0 0 25 0 1 0 1788459758 100687872 23606 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 24582 23606 145 145 0 24437 0
[pid=3050] vsize: 98328
Current children cumulated CPU time (s) 938.36
Current children cumulated vsize (Kb) 100452

[startup+950.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 24186 0 0 0 94675 159 0 0 25 0 1 0 1788459758 101183488 23727 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 24703 23727 145 145 0 24558 0
[pid=3050] vsize: 98812
Current children cumulated CPU time (s) 948.35
Current children cumulated vsize (Kb) 100936

[startup+960.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 24347 0 0 0 95671 161 0 0 25 0 1 0 1788459758 101838848 23888 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 24863 23888 145 145 0 24718 0
[pid=3050] vsize: 99452
Current children cumulated CPU time (s) 958.33
Current children cumulated vsize (Kb) 101576

[startup+970.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 24506 0 0 0 96668 162 0 0 25 0 1 0 1788459758 102490112 24047 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3050/statm): 25022 24047 145 145 0 24877 0
[pid=3050] vsize: 100088
Current children cumulated CPU time (s) 968.31
Current children cumulated vsize (Kb) 102212

[startup+980.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 24639 0 0 0 97666 163 0 0 25 0 1 0 1788459758 103026688 24180 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 25153 24180 145 145 0 25008 0
[pid=3050] vsize: 100612
Current children cumulated CPU time (s) 978.3
Current children cumulated vsize (Kb) 102736

[startup+990.068 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 24772 0 0 0 98664 164 0 0 25 0 1 0 1788459758 103571456 24313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 25286 24313 145 145 0 25141 0
[pid=3050] vsize: 101144
Current children cumulated CPU time (s) 988.29
Current children cumulated vsize (Kb) 103268

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 24911 0 0 0 99661 165 0 0 25 0 1 0 1788459758 104136704 24452 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 25424 24452 145 145 0 25279 0
[pid=3050] vsize: 101696
Current children cumulated CPU time (s) 998.27
Current children cumulated vsize (Kb) 103820

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 25036 0 0 0 100659 166 0 0 25 0 1 0 1788459758 104648704 24577 4294967295 134512640 135094434 3221224432 3221223120 134554705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 25549 24577 145 145 0 25404 0
[pid=3050] vsize: 102196
Current children cumulated CPU time (s) 1008.26
Current children cumulated vsize (Kb) 104320

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 25177 0 0 0 101655 168 0 0 25 0 1 0 1788459758 105226240 24718 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 25690 24718 145 145 0 25545 0
[pid=3050] vsize: 102760
Current children cumulated CPU time (s) 1018.24
Current children cumulated vsize (Kb) 104884

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 25304 0 0 0 102654 168 0 0 25 0 1 0 1788459758 105738240 24845 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 25815 24845 145 145 0 25670 0
[pid=3050] vsize: 103260
Current children cumulated CPU time (s) 1028.23
Current children cumulated vsize (Kb) 105384

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 25458 0 0 0 103651 169 0 0 25 0 1 0 1788459758 106377216 24999 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 25971 24999 145 145 0 25826 0
[pid=3050] vsize: 103884
Current children cumulated CPU time (s) 1038.21
Current children cumulated vsize (Kb) 106008

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 25616 0 0 0 104648 170 0 0 25 0 1 0 1788459758 107020288 25157 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 26128 25157 145 145 0 25983 0
[pid=3050] vsize: 104512
Current children cumulated CPU time (s) 1048.19
Current children cumulated vsize (Kb) 106636

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 25765 0 0 0 105645 171 0 0 25 0 1 0 1788459758 107626496 25306 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 26276 25306 145 145 0 26131 0
[pid=3050] vsize: 105104
Current children cumulated CPU time (s) 1058.17
Current children cumulated vsize (Kb) 107228

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 26000 0 0 0 106641 173 0 0 25 0 1 0 1788459758 108589056 25541 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 26511 25541 145 145 0 26366 0
[pid=3050] vsize: 106044
Current children cumulated CPU time (s) 1068.15
Current children cumulated vsize (Kb) 108168

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 26096 0 0 0 107639 174 0 0 25 0 1 0 1788459758 108978176 25637 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 26606 25637 145 145 0 26461 0
[pid=3050] vsize: 106424
Current children cumulated CPU time (s) 1078.14
Current children cumulated vsize (Kb) 108548

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 26277 0 0 0 108636 175 0 0 25 0 1 0 1788459758 109719552 25818 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 26787 25818 145 145 0 26642 0
[pid=3050] vsize: 107148
Current children cumulated CPU time (s) 1088.12
Current children cumulated vsize (Kb) 109272

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 26463 0 0 0 109633 176 0 0 25 0 1 0 1788459758 110477312 26004 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 26972 26004 145 145 0 26827 0
[pid=3050] vsize: 107888
Current children cumulated CPU time (s) 1098.1
Current children cumulated vsize (Kb) 110012

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 26747 0 0 0 110627 179 0 0 25 0 1 0 1788459758 111640576 26288 4294967295 134512640 135094434 3221224432 3221223044 134563112 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 27256 26288 145 145 0 27111 0
[pid=3050] vsize: 109024
Current children cumulated CPU time (s) 1108.07
Current children cumulated vsize (Kb) 111148

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 26942 0 0 0 111624 181 0 0 25 0 1 0 1788459758 112435200 26483 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 27450 26483 145 145 0 27305 0
[pid=3050] vsize: 109800
Current children cumulated CPU time (s) 1118.06
Current children cumulated vsize (Kb) 111924

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 27155 0 0 0 112620 182 0 0 25 0 1 0 1788459758 113303552 26696 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 27662 26696 145 145 0 27517 0
[pid=3050] vsize: 110648
Current children cumulated CPU time (s) 1128.03
Current children cumulated vsize (Kb) 112772

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 27332 0 0 0 113618 183 0 0 25 0 1 0 1788459758 114028544 26873 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 27839 26873 145 145 0 27694 0
[pid=3050] vsize: 111356
Current children cumulated CPU time (s) 1138.02
Current children cumulated vsize (Kb) 113480

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 27500 0 0 0 114616 184 0 0 25 0 1 0 1788459758 114712576 27041 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 28006 27041 145 145 0 27861 0
[pid=3050] vsize: 112024
Current children cumulated CPU time (s) 1148.01
Current children cumulated vsize (Kb) 114148

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 27682 0 0 0 115613 186 0 0 25 0 1 0 1788459758 115458048 27223 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 28188 27223 145 145 0 28043 0
[pid=3050] vsize: 112752
Current children cumulated CPU time (s) 1158
Current children cumulated vsize (Kb) 114876

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 27882 0 0 0 116610 187 0 0 25 0 1 0 1788459758 116535296 27423 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 28451 27423 145 145 0 28306 0
[pid=3050] vsize: 113804
Current children cumulated CPU time (s) 1167.98
Current children cumulated vsize (Kb) 115928

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 28030 0 0 0 117607 188 0 0 25 0 1 0 1788459758 117141504 27571 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 28599 27571 145 145 0 28454 0
[pid=3050] vsize: 114396
Current children cumulated CPU time (s) 1177.96
Current children cumulated vsize (Kb) 116520

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 28136 0 0 0 118606 189 0 0 25 0 1 0 1788459758 117575680 27677 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 28705 27677 145 145 0 28560 0
[pid=3050] vsize: 114820
Current children cumulated CPU time (s) 1187.96
Current children cumulated vsize (Kb) 116944

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 28245 0 0 0 119604 189 0 0 25 0 1 0 1788459758 118018048 27786 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 28813 27786 145 145 0 28668 0
[pid=3050] vsize: 115252
Current children cumulated CPU time (s) 1197.94
Current children cumulated vsize (Kb) 117376

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 28331 0 0 0 120603 190 0 0 25 0 1 0 1788459758 118366208 27872 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 28898 27872 145 145 0 28753 0
[pid=3050] vsize: 115592
Current children cumulated CPU time (s) 1207.94
Current children cumulated vsize (Kb) 117716



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 3050
Raw data (/proc/3046/stat): 3046 (minisat+_script) S 3045 3046 22582 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1788459753 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3046/statm): 531 226 485 147 0 384 0
[pid=3046] vsize: 2124
Raw data (/proc/3050/stat): 3050 (minisat+_64-bit) R 3046 3046 22582 0 -1 0 28331 0 0 0 120603 190 0 0 25 0 1 0 1788459758 118366208 27872 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3050/statm): 28898 27872 145 145 0 28753 0
[pid=3050] vsize: 115592
Current children cumulated CPU time (s) 1207.94
Current children cumulated vsize (Kb) 117716

Sending SIGTERM to -3046
Sleeping 2 seconds
One traced child (pid=3046) ended because it received signal 15 (SIGTERM)
One traced child (pid=3050) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.14
CPU time (s): 1208
CPU user time (s): 1206.04
CPU system time (s): 1.9577
CPU usage (%): 99.823
Max. virtual memory (cumulated for all children) (Kb): 117716

Verifier Data

ERROR: no interpretation found !