PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos11.opb
MD5SUM	6cda2e87049e07c7829c58ae7ae8c049
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1152
Optimality of the best value was proved	NO
Number of terms in the objective function	3600
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	188743500
Number of bits of the sum of numbers in the objective function	28
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	188743500
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.12
Number of variables	6100
Total number of constraints	3706
Number of constraints which are clauses	600
Number of constraints which are cardinality constraints (but not clauses)	1020
Number of constraints which are nor clauses,nor cardinality constraints	2086
Minimum length of a constraint	1
Maximum length of a constraint	300
Trace number 31295

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-05-25 23:55:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22687 boxname=wulflinc24 idbench=1503 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  6cda2e87049e07c7829c58ae7ae8c049  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-neos11.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-neos11.opb
IDLAUNCH: 22687
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 3
cpu MHz		: 451.080
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:        882376 kB
Buffers:         27260 kB
Cached:         103160 kB
SwapCached:        616 kB
Active:          22708 kB
Inactive:       109828 kB
HighTotal:      131008 kB
HighFree:        49756 kB
LowTotal:       903652 kB
LowFree:        832620 kB
SwapTotal:     2097892 kB
SwapFree:      2096416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5160 kB
Slab:            14204 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-26 00:16:20 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 22687 7 1229.86 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3042 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[3041]---> BDD-cost:    7
c ---[3040]---> BDD-cost:    7
c ---[3039]---> BDD-cost:    7
c ---[3038]---> BDD-cost:    7
c ---[3037]---> BDD-cost:    7
c ---[3036]---> BDD-cost:    7
c ---[3035]---> BDD-cost:    7
c ---[3034]---> BDD-cost:    7
c ---[3033]---> BDD-cost:    7
c ---[3032]---> BDD-cost:    7
c ---[3031]---> BDD-cost:    7
c ---[3030]---> BDD-cost:    7
c ---[3029]---> BDD-cost:    7
c ---[3028]---> BDD-cost:    7
c ---[3027]---> BDD-cost:    7
c ---[3026]---> BDD-cost:    7
c ---[3025]---> BDD-cost:    7
c ---[3024]---> BDD-cost:    7
c ---[3023]---> BDD-cost:    7
c ---[3022]---> BDD-cost:    7
c ---[3021]---> BDD-cost:    7
c ---[3020]---> BDD-cost:    7
c ---[3019]---> BDD-cost:    7
c ---[3018]---> BDD-cost:    7
c ---[3017]---> BDD-cost:    7
c ---[3016]---> BDD-cost:    7
c ---[3015]---> BDD-cost:    7
c ---[3014]---> BDD-cost:    7
c ---[3013]---> BDD-cost:    7
c ---[3012]---> BDD-cost:    7
c ---[3011]---> BDD-cost:    7
c ---[3010]---> BDD-cost:    7
c ---[3009]---> BDD-cost:    7
c ---[3008]---> BDD-cost:    7
c ---[3007]---> BDD-cost:    7
c ---[3006]---> BDD-cost:    7
c ---[3005]---> BDD-cost:    7
c ---[3004]---> BDD-cost:    7
c ---[3003]---> BDD-cost:    7
c ---[3002]---> BDD-cost:    7
c ---[3001]---> BDD-cost:    7
c ---[3000]---> BDD-cost:    7
c ---[2999]---> BDD-cost:    7
c ---[2998]---> BDD-cost:    7
c ---[2997]---> BDD-cost:    7
c ---[2996]---> BDD-cost:    7
c ---[2995]---> BDD-cost:    7
c ---[2994]---> BDD-cost:    7
c ---[2993]---> BDD-cost:    7
c ---[2992]---> BDD-cost:    7
c ---[2991]---> BDD-cost:    7
c ---[2990]---> BDD-cost:    7
c ---[2989]---> BDD-cost:    7
c ---[2988]---> BDD-cost:    7
c ---[2987]---> BDD-cost:    7
c ---[2986]---> BDD-cost:    7
c ---[2985]---> BDD-cost:    7
c ---[2984]---> BDD-cost:    7
c ---[2983]---> BDD-cost:    7
c ---[2982]---> BDD-cost:    7
c ---[2981]---> BDD-cost:    7
c ---[2980]---> BDD-cost:    7
c ---[2979]---> BDD-cost:    7
c ---[2978]---> BDD-cost:    7
c ---[2977]---> BDD-cost:    7
c ---[2976]---> BDD-cost:    7
c ---[2975]---> BDD-cost:    7
c ---[2974]---> BDD-cost:    7
c ---[2973]---> BDD-cost:    7
c ---[2972]---> BDD-cost:    7
c ---[2971]---> BDD-cost:    7
c ---[2970]---> BDD-cost:    7
c ---[2969]---> BDD-cost:    7
c ---[2968]---> BDD-cost:    7
c ---[2967]---> BDD-cost:    7
c ---[2966]---> BDD-cost:    7
c ---[2965]---> BDD-cost:    7
c ---[2964]---> BDD-cost:    7
c ---[2963]---> BDD-cost:    7
c ---[2962]---> BDD-cost:    7
c ---[2961]---> BDD-cost:    7
c ---[2960]---> BDD-cost:    7
c ---[2959]---> BDD-cost:    7
c ---[2958]---> BDD-cost:    7
c ---[2957]---> BDD-cost:    7
c ---[2956]---> BDD-cost:    7
c ---[2955]---> BDD-cost:    7
c ---[2954]---> BDD-cost:    7
c ---[2953]---> BDD-cost:    7
c ---[2952]---> BDD-cost:    7
c ---[2951]---> BDD-cost:    7
c ---[2950]---> BDD-cost:    7
c ---[2949]---> BDD-cost:    7
c ---[2948]---> BDD-cost:    7
c ---[2947]---> BDD-cost:    7
c ---[2946]---> BDD-cost:    7
c ---[2945]---> BDD-cost:    7
c ---[2944]---> BDD-cost:    7
c ---[2943]---> BDD-cost:    7
c ---[2942]---> BDD-cost:    7
c ---[2940]---> BDD-cost:   35
c ---[2938]---> BDD-cost:   35
c ---[2936]---> BDD-cost:   35
c ---[2934]---> BDD-cost:   35
c ---[2932]---> BDD-cost:   35
c ---[2930]---> BDD-cost:   35
c ---[2928]---> BDD-cost:   35
c ---[2926]---> BDD-cost:   35
c ---[2924]---> BDD-cost:   35
c ---[2922]---> BDD-cost:   35
c ---[2920]---> BDD-cost:   35
c ---[2918]---> BDD-cost:   35
c ---[2916]---> BDD-cost:   35
c ---[2914]---> BDD-cost:   35
c ---[2912]---> BDD-cost:   35
c ---[2910]---> BDD-cost:   35
c ---[2908]---> BDD-cost:   35
c ---[2906]---> BDD-cost:   35
c ---[2904]---> BDD-cost:   35
c ---[2902]---> BDD-cost:   35
c ---[2900]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2898]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2896]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2894]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2892]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2890]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2888]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2886]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2884]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2882]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[2881]---> BDD-cost:   22
c ---[2880]---> BDD-cost:   22
c ---[2879]---> BDD-cost:   22
c ---[2878]---> BDD-cost:   22
c ---[2877]---> BDD-cost:   22
c ---[2876]---> BDD-cost:   22
c ---[2875]---> BDD-cost:   22
c ---[2874]---> BDD-cost:   22
c ---[2873]---> BDD-cost:   22
c ---[2872]---> BDD-cost:   22
c ---[2871]---> BDD-cost:   22
c ---[2870]---> BDD-cost:   22
c ---[2869]---> BDD-cost:   22
c ---[2868]---> BDD-cost:   22
c ---[2867]---> BDD-cost:   22
c ---[2866]---> BDD-cost:   22
c ---[2865]---> BDD-cost:   22
c ---[2864]---> BDD-cost:   22
c ---[2863]---> BDD-cost:   22
c ---[2862]---> BDD-cost:   22
c ---[2861]---> BDD-cost:   22
c ---[2860]---> BDD-cost:   22
c ---[2859]---> BDD-cost:   22
c ---[2858]---> BDD-cost:   22
c ---[2857]---> BDD-cost:   22
c ---[2856]---> BDD-cost:   22
c ---[2855]---> BDD-cost:   22
c ---[2854]---> BDD-cost:   22
c ---[2853]---> BDD-cost:   22
c ---[2852]---> BDD-cost:   22
c ---[2851]---> BDD-cost:   22
c ---[2850]---> BDD-cost:   22
c ---[2849]---> BDD-cost:   22
c ---[2848]---> BDD-cost:   22
c ---[2847]---> BDD-cost:   22
c ---[2846]---> BDD-cost:   22
c ---[2845]---> BDD-cost:   22
c ---[2844]---> BDD-cost:   22
c ---[2843]---> BDD-cost:   22
c ---[2842]---> BDD-cost:   22
c ---[2841]---> BDD-cost:   22
c ---[2840]---> BDD-cost:   22
c ---[2839]---> BDD-cost:   22
c ---[2838]---> BDD-cost:   22
c ---[2837]---> BDD-cost:   22
c ---[2836]---> BDD-cost:   22
c ---[2835]---> BDD-cost:   22
c ---[2834]---> BDD-cost:   22
c ---[2833]---> BDD-cost:   22
c ---[2832]---> BDD-cost:   22
c ---[2831]---> BDD-cost:   22
c ---[2830]---> BDD-cost:   22
c ---[2829]---> BDD-cost:   22
c ---[2828]---> BDD-cost:   22
c ---[2827]---> BDD-cost:   22
c ---[2826]---> BDD-cost:   22
c ---[2825]---> BDD-cost:   22
c ---[2824]---> BDD-cost:   22
c ---[2823]---> BDD-cost:   22
c ---[2822]---> BDD-cost:   22
c ---[2821]---> BDD-cost:   22
c ---[2820]---> BDD-cost:   22
c ---[2819]---> BDD-cost:   22
c ---[2818]---> BDD-cost:   22
c ---[2817]---> BDD-cost:   22
c ---[2816]---> BDD-cost:   22
c ---[2815]---> BDD-cost:   22
c ---[2814]---> BDD-cost:   22
c ---[2813]---> BDD-cost:   22
c ---[2812]---> BDD-cost:   22
c ---[2811]---> BDD-cost:   22
c ---[2810]---> BDD-cost:   22
c ---[2809]---> BDD-cost:   22
c ---[2808]---> BDD-cost:   22
c ---[2807]---> BDD-cost:   22
c ---[2806]---> BDD-cost:   22
c ---[2805]---> BDD-cost:   22
c ---[2804]---> BDD-cost:   22
c ---[2803]---> BDD-cost:   22
c ---[2802]---> BDD-cost:   22
c ---[2801]---> BDD-cost:   22
c ---[2800]---> BDD-cost:   22
c ---[2799]---> BDD-cost:   22
c ---[2798]---> BDD-cost:   22
c ---[2797]---> BDD-cost:   22
c ---[2796]---> BDD-cost:   22
c ---[2795]---> BDD-cost:   22
c ---[2794]---> BDD-cost:   22
c ---[2793]---> BDD-cost:   22
c ---[2792]---> BDD-cost:   22
c ---[2791]---> BDD-cost:   22
c ---[2790]---> BDD-cost:   22
c ---[2789]---> BDD-cost:   22
c ---[2788]---> BDD-cost:   22
c ---[2787]---> BDD-cost:   22
c ---[2786]---> BDD-cost:   22
c ---[2785]---> BDD-cost:   22
c ---[2784]---> BDD-cost:   22
c ---[2783]---> BDD-cost:   22
c ---[2782]---> BDD-cost:   22
c ---[2781]---> BDD-cost:   22
c ---[2780]---> BDD-cost:   22
c ---[2779]---> BDD-cost:   22
c ---[2778]---> BDD-cost:   22
c ---[2777]---> BDD-cost:   22
c ---[2776]---> BDD-cost:   22
c ---[2775]---> BDD-cost:   22
c ---[2774]---> BDD-cost:   22
c ---[2773]---> BDD-cost:   22
c ---[2772]---> BDD-cost:   22
c ---[2771]---> BDD-cost:   22
c ---[2770]---> BDD-cost:   22
c ---[2769]---> BDD-cost:   22
c ---[2768]---> BDD-cost:   22
c ---[2767]---> BDD-cost:   22
c ---[2766]---> BDD-cost:   22
c ---[2765]---> BDD-cost:   22
c ---[2764]---> BDD-cost:   22
c ---[2763]---> BDD-cost:   22
c ---[2762]---> BDD-cost:   22
c ---[2761]---> BDD-cost:   22
c ---[2760]---> BDD-cost:   22
c ---[2759]---> BDD-cost:   22
c ---[2758]---> BDD-cost:   22
c ---[2757]---> BDD-cost:   22
c ---[2756]---> BDD-cost:   22
c ---[2755]---> BDD-cost:   22
c ---[2754]---> BDD-cost:   22
c ---[2753]---> BDD-cost:   22
c ---[2752]---> BDD-cost:   22
c ---[2751]---> BDD-cost:   22
c ---[2750]---> BDD-cost:   22
c ---[2749]---> BDD-cost:   22
c ---[2748]---> BDD-cost:   22
c ---[2747]---> BDD-cost:   22
c ---[2746]---> BDD-cost:   22
c ---[2745]---> BDD-cost:   22
c ---[2744]---> BDD-cost:   22
c ---[2743]---> BDD-cost:   22
c ---[2742]---> BDD-cost:   22
c ---[2741]---> BDD-cost:   22
c ---[2740]---> BDD-cost:   22
c ---[2739]---> BDD-cost:   22
c ---[2738]---> BDD-cost:   22
c ---[2737]---> BDD-cost:   22
c ---[2736]---> BDD-cost:   22
c ---[2735]---> BDD-cost:   22
c ---[2734]---> BDD-cost:   22
c ---[2733]---> BDD-cost:   22
c ---[2732]---> BDD-cost:   22
c ---[2731]---> BDD-cost:   22
c ---[2730]---> BDD-cost:   22
c ---[2729]---> BDD-cost:   22
c ---[2728]---> BDD-cost:   22
c ---[2727]---> BDD-cost:   22
c ---[2726]---> BDD-cost:   22
c ---[2725]---> BDD-cost:   22
c ---[2724]---> BDD-cost:   22
c ---[2723]---> BDD-cost:   22
c ---[2722]---> BDD-cost:   22
c ---[2721]---> BDD-cost:   22
c ---[2720]---> BDD-cost:   22
c ---[2719]---> BDD-cost:   22
c ---[2718]---> BDD-cost:   22
c ---[2717]---> BDD-cost:   22
c ---[2716]---> BDD-cost:   22
c ---[2715]---> BDD-cost:   22
c ---[2714]---> BDD-cost:   22
c ---[2713]---> BDD-cost:   22
c ---[2712]---> BDD-cost:   22
c ---[2711]---> BDD-cost:   22
c ---[2710]---> BDD-cost:   22
c ---[2709]---> BDD-cost:   22
c ---[2708]---> BDD-cost:   22
c ---[2707]---> BDD-cost:   22
c ---[2706]---> BDD-cost:   22
c ---[2705]---> BDD-cost:   22
c ---[2704]---> BDD-cost:   22
c ---[2703]---> BDD-cost:   22
c ---[2702]---> BDD-cost:   22
c ---[2701]---> BDD-cost:   22
c ---[2700]---> BDD-cost:   22
c ---[2699]---> BDD-cost:   22
c ---[2698]---> BDD-cost:   22
c ---[2697]---> BDD-cost:   22
c ---[2696]---> BDD-cost:   22
c ---[2695]---> BDD-cost:   22
c ---[2694]---> BDD-cost:   22
c ---[2693]---> BDD-cost:   22
c ---[2692]---> BDD-cost:   22
c ---[2691]---> BDD-cost:   22
c ---[2690]---> BDD-cost:   22
c ---[2689]---> BDD-cost:   22
c ---[2688]---> BDD-cost:   22
c ---[2687]---> BDD-cost:   22
c ---[2686]---> BDD-cost:   22
c ---[2685]---> BDD-cost:   22
c ---[2684]---> BDD-cost:   22
c ---[2683]---> BDD-cost:   22
c ---[2682]---> BDD-cost:   22
c ---[2680]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2
c ---[2678]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2676]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2674]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2672]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2670]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2
c ---[2668]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2666]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2664]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2662]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2660]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2
c ---[2658]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2656]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2654]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2652]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2650]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2
c ---[2648]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2646]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2644]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2642]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2640]---> Sorter-cost:  511     Base: 2 2 2 2 2 2 2 2
c ---[2638]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2636]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2634]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2632]---> Sorter-cost:  487     Base: 2 2 2 2 2 2 2
c ---[2631]---> BDD-cost:   29
c ---[2630]---> BDD-cost:   29
c ---[2629]---> BDD-cost:   29
c ---[2628]---> BDD-cost:   29
c ---[2627]---> BDD-cost:   87
c ---[2626]---> BDD-cost:   81
c ---[2625]---> BDD-cost:   81
c ---[2624]---> BDD-cost:   81
c ---[2623]---> BDD-cost:   87
c ---[2622]---> BDD-cost:   79
c ---[2621]---> BDD-cost:   81
c ---[2620]---> BDD-cost:   81
c ---[2619]---> BDD-cost:   87
c ---[2618]---> BDD-cost:   79
c ---[2617]---> BDD-cost:   79
c ---[2616]---> BDD-cost:   81
c ---[2615]---> BDD-cost:   87
c ---[2614]---> BDD-cost:   79
c ---[2613]---> BDD-cost:   79
c ---[2612]---> BDD-cost:   79
c ---[2611]---> BDD-cost:   29
c ---[2610]---> BDD-cost:   29
c ---[2609]---> BDD-cost:   29
c ---[2608]---> BDD-cost:   29
c ---[2607]---> BDD-cost:   88
c ---[2606]---> BDD-cost:   81
c ---[2605]---> BDD-cost:   81
c ---[2604]---> BDD-cost:   81
c ---[2603]---> BDD-cost:   87
c ---[2602]---> BDD-cost:   81
c ---[2601]---> BDD-cost:   81
c ---[2600]---> BDD-cost:   81
c ---[2599]---> BDD-cost:   87
c ---[2598]---> BDD-cost:   81
c ---[2597]---> BDD-cost:   79
c ---[2596]---> BDD-cost:   81
c ---[2595]---> BDD-cost:   87
c ---[2594]---> BDD-cost:   81
c ---[2593]---> BDD-cost:   79
c ---[2592]---> BDD-cost:   79
c ---[2591]---> BDD-cost:   29
c ---[2590]---> BDD-cost:   29
c ---[2589]---> BDD-cost:   29
c ---[2588]---> BDD-cost:   29
c ---[2587]---> BDD-cost:   88
c ---[2586]---> BDD-cost:   81
c ---[2585]---> BDD-cost:   81
c ---[2584]---> BDD-cost:   81
c ---[2583]---> BDD-cost:   88
c ---[2582]---> BDD-cost:   81
c ---[2581]---> BDD-cost:   81
c ---[2580]---> BDD-cost:   81
c ---[2579]---> BDD-cost:   87
c ---[2578]---> BDD-cost:   81
c ---[2577]---> BDD-cost:   81
c ---[2576]---> BDD-cost:   81
c ---[2575]---> BDD-cost:   87
c ---[2574]---> BDD-cost:   81
c ---[2573]---> BDD-cost:   81
c ---[2572]---> BDD-cost:   79
c ---[2571]---> BDD-cost:   29
c ---[2570]---> BDD-cost:   29
c ---[2569]---> BDD-cost:   29
c ---[2568]---> BDD-cost:   29
c ---[2567]---> BDD-cost:   88
c ---[2566]---> BDD-cost:   81
c ---[2565]---> BDD-cost:   81
c ---[2564]---> BDD-cost:   81
c ---[2563]---> BDD-cost:   88
c ---[2562]---> BDD-cost:   81
c ---[2561]---> BDD-cost:   81
c ---[2560]---> BDD-cost:   81
c ---[2559]---> BDD-cost:   88
c ---[2558]---> BDD-cost:   81
c ---[2557]---> BDD-cost:   81
c ---[2556]---> BDD-cost:   81
c ---[2555]---> BDD-cost:   87
c ---[2554]---> BDD-cost:   81
c ---[2553]---> BDD-cost:   81
c ---[2552]---> BDD-cost:   81
c ---[2551]---> BDD-cost:   29
c ---[2550]---> BDD-cost:   29
c ---[2549]---> BDD-cost:   29
c ---[2548]---> BDD-cost:   29
c ---[2547]---> BDD-cost:   88
c ---[2546]---> BDD-cost:   81
c ---[2545]---> BDD-cost:   81
c ---[2544]---> BDD-cost:   81
c ---[2543]---> BDD-cost:   88
c ---[2542]---> BDD-cost:   81
c ---[2541]---> BDD-cost:   81
c ---[2540]---> BDD-cost:   81
c ---[2539]---> BDD-cost:   88
c ---[2538]---> BDD-cost:   81
c ---[2537]---> BDD-cost:   81
c ---[2536]---> BDD-cost:   81
c ---[2535]---> BDD-cost:   88
c ---[2534]---> BDD-cost:   81
c ---[2533]---> BDD-cost:   81
c ---[2532]---> BDD-cost:   81
c ---[2530]---> BDD-cost:   33
c ---[2528]---> BDD-cost:   33
c ---[2526]---> Sorter-cost:   65     Base:
c ---[2524]---> BDD-cost:   33
c ---[2522]---> BDD-cost:   33
c ---[2520]---> BDD-cost:   33
c ---[2518]---> Sorter-cost:   65     Base:
c ---[2516]---> BDD-cost:   33
c ---[2514]---> BDD-cost:   33
c ---[2512]---> BDD-cost:   33
c ---[2510]---> Sorter-cost:   65     Base:
c ---[2508]---> BDD-cost:   33
c ---[2506]---> BDD-cost:   33
c ---[2504]---> BDD-cost:   33
c ---[2502]---> BDD-cost:   33
c ---[2500]---> BDD-cost:   33
c ---[2498]---> BDD-cost:   33
c ---[2496]---> BDD-cost:   33
c ---[2494]---> BDD-cost:   33
c ---[2492]---> Sorter-cost:   65     Base:
c ---[2490]---> BDD-cost:   33
c ---[2488]---> BDD-cost:   33
c ---[2486]---> Sorter-cost:   65     Base:
c ---[2484]---> BDD-cost:   33
c ---[2482]---> BDD-cost:   33
c ---[2480]---> BDD-cost:   33
c ---[2478]---> Sorter-cost:   65     Base:
c ---[2476]---> BDD-cost:   33
c ---[2474]---> BDD-cost:   33
c ---[2472]---> BDD-cost:   33
c ---[2470]---> Sorter-cost:   65     Base:
c ---[2468]---> BDD-cost:   33
c ---[2466]---> BDD-cost:   33
c ---[2464]---> BDD-cost:   33
c ---[2462]---> BDD-cost:   33
c ---[2460]---> BDD-cost:   33
c ---[2458]---> BDD-cost:   33
c ---[2456]---> BDD-cost:   33
c ---[2454]---> BDD-cost:   33
c ---[2452]---> Sorter-cost:   65     Base:
c ---[2450]---> BDD-cost:   33
c ---[2448]---> BDD-cost:   33
c ---[2446]---> Sorter-cost:   65     Base:
c ---[2444]---> BDD-cost:   33
c ---[2442]---> BDD-cost:   33
c ---[2440]---> BDD-cost:   33
c ---[2438]---> Sorter-cost:   65     Base:
c ---[2436]---> BDD-cost:   33
c ---[2434]---> BDD-cost:   33
c ---[2432]---> BDD-cost:   33
c ---[2430]---> Sorter-cost:   65     Base:
c ---[2428]---> BDD-cost:   33
c ---[2426]---> BDD-cost:   33
c ---[2424]---> BDD-cost:   33
c ---[2422]---> BDD-cost:   33
c ---[2420]---> BDD-cost:   33
c ---[2418]---> BDD-cost:   33
c ---[2416]---> BDD-cost:   33
c ---[2414]---> BDD-cost:   33
c ---[2412]---> Sorter-cost:   65     Base:
c ---[2410]---> BDD-cost:   33
c ---[2408]---> BDD-cost:   33
c ---[2406]---> Sorter-cost:   65     Base:
c ---[2404]---> BDD-cost:   33
c ---[2402]---> BDD-cost:   33
c ---[2400]---> BDD-cost:   33
c ---[2398]---> Sorter-cost:   65     Base:
c ---[2396]---> BDD-cost:   33
c ---[2394]---> BDD-cost:   33
c ---[2392]---> BDD-cost:   33
c ---[2390]---> Sorter-cost:   65     Base:
c ---[2388]---> BDD-cost:   33
c ---[2386]---> BDD-cost:   33
c ---[2384]---> BDD-cost:   33
c ---[2382]---> BDD-cost:   33
c ---[2380]---> BDD-cost:   33
c ---[2378]---> BDD-cost:   33
c ---[2376]---> BDD-cost:   33
c ---[2374]---> BDD-cost:   33
c ---[2372]---> Sorter-cost:   65     Base:
c ---[2370]---> BDD-cost:   33
c ---[2368]---> BDD-cost:   33
c ---[2366]---> BDD-cost:   33
c ---[2364]---> BDD-cost:   33
c ---[2362]---> BDD-cost:   33
c ---[2360]---> BDD-cost:   33
c ---[2358]---> BDD-cost:   33
c ---[2356]---> BDD-cost:   33
c ---[2354]---> BDD-cost:   33
c ---[2352]---> BDD-cost:   33
c ---[2350]---> BDD-cost:   33
c ---[2348]---> BDD-cost:   33
c ---[2346]---> BDD-cost:   33
c ---[2344]---> BDD-cost:   33
c ---[2342]---> BDD-cost:   33
c ---[2340]---> BDD-cost:   33
c ---[2338]---> BDD-cost:   33
c ---[2336]---> BDD-cost:   33
c ---[2334]---> BDD-cost:   33
c ---[2332]---> BDD-cost:   33
c ---[2330]---> BDD-cost:   33
c ---[2328]---> BDD-cost:   33
c ---[2326]---> BDD-cost:   33
c ---[2324]---> Sorter-cost:   65     Base:
c ---[2322]---> BDD-cost:   33
c ---[2320]---> BDD-cost:   33
c ---[2318]---> BDD-cost:   33
c ---[2316]---> Sorter-cost:   65     Base:
c ---[2314]---> BDD-cost:   33
c ---[2312]---> BDD-cost:   33
c ---[2310]---> BDD-cost:   33
c ---[2308]---> Sorter-cost:   65     Base:
c ---[2306]---> BDD-cost:   33
c ---[2304]---> BDD-cost:   33
c ---[2302]---> BDD-cost:   33
c ---[2300]---> Sorter-cost:   65     Base:
c ---[2298]---> BDD-cost:   33
c ---[2296]---> BDD-cost:   33
c ---[2294]---> BDD-cost:   33
c ---[2292]---> BDD-cost:   33
c ---[2290]---> BDD-cost:   33
c ---[2288]---> BDD-cost:   33
c ---[2286]---> BDD-cost:   33
c ---[2284]---> BDD-cost:   33
c ---[2282]---> BDD-cost:   33
c ---[2280]---> BDD-cost:   32
c ---[2278]---> BDD-cost:   41
c ---[2276]---> BDD-cost:   41
c ---[2274]---> BDD-cost:   41
c ---[2272]---> BDD-cost:   41
c ---[2270]---> BDD-cost:   32
c ---[2268]---> BDD-cost:   41
c ---[2266]---> BDD-cost:   41
c ---[2264]---> BDD-cost:   41
c ---[2262]---> BDD-cost:   41
c ---[2260]---> BDD-cost:   32
c ---[2258]---> BDD-cost:   41
c ---[2256]---> BDD-cost:   41
c ---[2254]---> BDD-cost:   41
c ---[2252]---> BDD-cost:   41
c ---[2250]---> BDD-cost:   32
c ---[2248]---> BDD-cost:   41
c ---[2246]---> BDD-cost:   41
c ---[2244]---> BDD-cost:   41
c ---[2242]---> BDD-cost:   41
c ---[2240]---> BDD-cost:   32
c ---[2238]---> BDD-cost:   41
c ---[2236]---> BDD-cost:   41
c ---[2234]---> BDD-cost:   41
c ---[2232]---> BDD-cost:   41
c ---[2230]---> BDD-cost:   33
c ---[2228]---> BDD-cost:   33
c ---[2226]---> BDD-cost:   33
c ---[2224]---> Sorter-cost:   65     Base:
c ---[2222]---> BDD-cost:   33
c ---[2220]---> BDD-cost:   32
c ---[2218]---> BDD-cost:   39
c ---[2216]---> BDD-cost:   39
c ---[2214]---> BDD-cost:   39
c ---[2212]---> BDD-cost:   39
c ---[2210]---> BDD-cost:   32
c ---[2208]---> BDD-cost:   39
c ---[2206]---> BDD-cost:   39
c ---[2204]---> BDD-cost:   39
c ---[2202]---> BDD-cost:   39
c ---[2200]---> BDD-cost:   32
c ---[2198]---> BDD-cost:   39
c ---[2196]---> BDD-cost:   39
c ---[2194]---> BDD-cost:   39
c ---[2192]---> BDD-cost:   39
c ---[2190]---> BDD-cost:   32
c ---[2188]---> BDD-cost:   39
c ---[2186]---> BDD-cost:   39
c ---[2184]---> BDD-cost:   39
c ---[2182]---> BDD-cost:   39
c ---[2180]---> BDD-cost:   32
c ---[2178]---> BDD-cost:   39
c ---[2176]---> BDD-cost:   39
c ---[2174]---> BDD-cost:   39
c ---[2172]---> BDD-cost:   39
c ---[2171]---> BDD-cost:   10
c ---[2170]---> BDD-cost:   10
c ---[2169]---> BDD-cost:   10
c ---[2168]---> BDD-cost:   10
c ---[2167]---> BDD-cost:   10
c ---[2166]---> BDD-cost:   10
c ---[2165]---> BDD-cost:   10
c ---[2164]---> BDD-cost:   10
c ---[2163]---> BDD-cost:   10
c ---[2162]---> BDD-cost:   10
c ---[2161]---> BDD-cost:   10
c ---[2160]---> BDD-cost:   10
c ---[2159]---> BDD-cost:   10
c ---[2158]---> BDD-cost:   10
c ---[2157]---> BDD-cost:   10
c ---[2156]---> BDD-cost:   10
c ---[2155]---> BDD-cost:   10
c ---[2154]---> BDD-cost:   10
c ---[2153]---> BDD-cost:   10
c ---[2152]---> BDD-cost:   10
c ---[2151]---> BDD-cost:   10
c ---[2150]---> BDD-cost:   10
c ---[2149]---> BDD-cost:   10
c ---[2148]---> BDD-cost:   10
c ---[2147]---> BDD-cost:   10
c ---[2146]---> BDD-cost:   10
c ---[2145]---> BDD-cost:   10
c ---[2144]---> BDD-cost:   10
c ---[2143]---> BDD-cost:   10
c ---[2142]---> BDD-cost:   10
c ---[2141]---> BDD-cost:   10
c ---[2140]---> BDD-cost:   10
c ---[2139]---> BDD-cost:   10
c ---[2138]---> BDD-cost:   10
c ---[2137]---> BDD-cost:   10
c ---[2136]---> BDD-cost:   10
c ---[2135]---> BDD-cost:   10
c ---[2134]---> BDD-cost:   10
c ---[2133]---> BDD-cost:   10
c ---[2132]---> BDD-cost:   10
c ---[2131]---> BDD-cost:   10
c ---[2130]---> BDD-cost:   10
c ---[2129]---> BDD-cost:   10
c ---[2128]---> BDD-cost:   10
c ---[2127]---> BDD-cost:   10
c ---[2126]---> BDD-cost:   10
c ---[2125]---> BDD-cost:   10
c ---[2124]---> BDD-cost:   10
c ---[2123]---> BDD-cost:   10
c ---[2122]---> BDD-cost:   10
c ---[2121]---> BDD-cost:   10
c ---[2120]---> BDD-cost:   10
c ---[2119]---> BDD-cost:   10
c ---[2118]---> BDD-cost:   10
c ---[2117]---> BDD-cost:   10
c ---[2116]---> BDD-cost:   10
c ---[2115]---> BDD-cost:   10
c ---[2114]---> BDD-cost:   10
c ---[2113]---> BDD-cost:   10
c ---[2112]---> BDD-cost:   10
c ---[2111]---> BDD-cost:   10
c ---[2110]---> BDD-cost:   10
c ---[2109]---> BDD-cost:   10
c ---[2108]---> BDD-cost:   10
c ---[2107]---> BDD-cost:   10
c ---[2106]---> BDD-cost:   10
c ---[2105]---> BDD-cost:   10
c ---[2104]---> BDD-cost:   10
c ---[2103]---> BDD-cost:   10
c ---[2102]---> BDD-cost:   10
c ---[2101]---> BDD-cost:   10
c ---[2100]---> BDD-cost:   10
c ---[2099]---> BDD-cost:   10
c ---[2098]---> BDD-cost:   10
c ---[2097]---> BDD-cost:   10
c ---[2096]---> BDD-cost:   10
c ---[2095]---> BDD-cost:   10
c ---[2094]---> BDD-cost:   10
c ---[2093]---> BDD-cost:   10
c ---[2092]---> BDD-cost:   10
c ---[2091]---> BDD-cost:    9
c ---[2090]---> BDD-cost:    9
c ---[2089]---> BDD-cost:    9
c ---[2088]---> BDD-cost:    9
c ---[2087]---> BDD-cost:    9
c ---[2086]---> BDD-cost:    9
c ---[2085]---> BDD-cost:    9
c ---[2084]---> BDD-cost:    9
c ---[2083]---> BDD-cost:    9
c ---[2082]---> BDD-cost:    9
c ---[2081]---> BDD-cost:    9
c ---[2080]---> BDD-cost:    9
c ---[2079]---> BDD-cost:    9
c ---[2078]---> BDD-cost:    9
c ---[2077]---> BDD-cost:    9
c ---[2076]---> BDD-cost:    9
c ---[2075]---> BDD-cost:    9
c ---[2074]---> BDD-cost:    9
c ---[2073]---> BDD-cost:    9
c ---[2072]---> BDD-cost:    9
c ---[2071]---> BDD-cost:    9
c ---[2070]---> BDD-cost:    9
c ---[2069]---> BDD-cost:    9
c ---[2068]---> BDD-cost:    9
c ---[2067]---> BDD-cost:    9
c ---[2066]---> BDD-cost:    9
c ---[2065]---> BDD-cost:    9
c ---[2064]---> BDD-cost:    9
c ---[2063]---> BDD-cost:    9
c ---[2062]---> BDD-cost:    9
c ---[2061]---> BDD-cost:    9
c ---[2060]---> BDD-cost:    9
c ---[2059]---> BDD-cost:    9
c ---[2058]---> BDD-cost:    9
c ---[2057]---> BDD-cost:    9
c ---[2056]---> BDD-cost:    9
c ---[2055]---> BDD-cost:    9
c ---[2054]---> BDD-cost:    9
c ---[2053]---> BDD-cost:    9
c ---[2052]---> BDD-cost:    9
c ---[2051]---> BDD-cost:    9
c ---[2050]---> BDD-cost:    9
c ---[2049]---> BDD-cost:    9
c ---[2048]---> BDD-cost:    9
c ---[2047]---> BDD-cost:    9
c ---[2046]---> BDD-cost:    9
c ---[2045]---> BDD-cost:    9
c ---[2044]---> BDD-cost:    9
c ---[2043]---> BDD-cost:    9
c ---[2042]---> BDD-cost:    9
c ---[2041]---> BDD-cost:    9
c ---[2040]---> BDD-cost:    9
c ---[2039]---> BDD-cost:    9
c ---[2038]---> BDD-cost:    9
c ---[2037]---> BDD-cost:    9
c ---[2036]---> BDD-cost:    9
c ---[2035]---> BDD-cost:    9
c ---[2034]---> BDD-cost:    9
c ---[2033]---> BDD-cost:    9
c ---[2032]---> BDD-cost:    9
c ---[2031]---> BDD-cost:    9
c ---[2030]---> BDD-cost:    9
c ---[2029]---> BDD-cost:    9
c ---[2028]---> BDD-cost:    9
c ---[2027]---> BDD-cost:    9
c ---[2026]---> BDD-cost:    9
c ---[2025]---> BDD-cost:    9
c ---[2024]---> BDD-cost:    9
c ---[2023]---> BDD-cost:    9
c ---[2022]---> BDD-cost:    9
c ---[2021]---> BDD-cost:    9
c ---[2020]---> BDD-cost:    9
c ---[2019]---> BDD-cost:    9
c ---[2018]---> BDD-cost:    9
c ---[2017]---> BDD-cost:    9
c ---[2016]---> BDD-cost:    9
c ---[2015]---> BDD-cost:    9
c ---[2014]---> BDD-cost:    9
c ---[2013]---> BDD-cost:    9
c ---[2012]---> BDD-cost:    9
c ---[2011]---> BDD-cost:    7
c ---[2010]---> BDD-cost:    7
c ---[2009]---> BDD-cost:    7
c ---[2008]---> BDD-cost:    7
c ---[2007]---> BDD-cost:    7
c ---[2006]---> BDD-cost:    7
c ---[2005]---> BDD-cost:    7
c ---[2004]---> BDD-cost:    7
c ---[2003]---> BDD-cost:    7
c ---[2002]---> BDD-cost:    7
c ---[2001]---> BDD-cost:    7
c ---[2000]---> BDD-cost:    7
c ---[1999]---> BDD-cost:    5
c ---[1998]---> BDD-cost:    5
c ---[1997]---> BDD-cost:    5
c ---[1996]---> BDD-cost:    5
c ---[1995]---> BDD-cost:    5
c ---[1994]---> BDD-cost:    5
c ---[1993]---> BDD-cost:    5
c ---[1992]---> BDD-cost:    5
c ---[1991]---> BDD-cost:    5
c ---[1990]---> BDD-cost:    5
c ---[1989]---> BDD-cost:    5
c ---[1988]---> BDD-cost:    5
c ---[1987]---> BDD-cost:    4
c ---[1986]---> BDD-cost:    4
c ---[1985]---> BDD-cost:    4
c ---[1984]---> BDD-cost:    4
c ---[1983]---> BDD-cost:    4
c ---[1982]---> BDD-cost:    4
c ---[1981]---> BDD-cost:    4
c ---[1980]---> BDD-cost:    4
c ---[1979]---> BDD-cost:    4
c ---[1978]---> BDD-cost:    4
c ---[1977]---> BDD-cost:    4
c ---[1976]---> BDD-cost:    4
c ---[1975]---> BDD-cost:    5
c ---[1974]---> BDD-cost:    5
c ---[1973]---> BDD-cost:    5
c ---[1972]---> BDD-cost:    5
c ---[1971]---> BDD-cost:    5
c ---[1970]---> BDD-cost:    5
c ---[1969]---> BDD-cost:    5
c ---[1968]---> BDD-cost:    5
c ---[1967]---> BDD-cost:    5
c ---[1966]---> BDD-cost:    5
c ---[1965]---> BDD-cost:    5
c ---[1964]---> BDD-cost:    5
c ---[1963]---> BDD-cost:    3
c ---[1962]---> BDD-cost:    3
c ---[1961]---> BDD-cost:    3
c ---[1960]---> BDD-cost:    3
c ---[1959]---> BDD-cost:    3
c ---[1958]---> BDD-cost:    3
c ---[1957]---> BDD-cost:    3
c ---[1956]---> BDD-cost:    3
c ---[1955]---> BDD-cost:    3
c ---[1954]---> BDD-cost:    3
c ---[1953]---> BDD-cost:    3
c ---[1952]---> BDD-cost:    3
c ---[1951]---> BDD-cost:    7
c ---[1950]---> BDD-cost:    7
c ---[1949]---> BDD-cost:    7
c ---[1948]---> BDD-cost:    7
c ---[1947]---> BDD-cost:    7
c ---[1946]---> BDD-cost:    7
c ---[1945]---> BDD-cost:    7
c ---[1944]---> BDD-cost:    7
c ---[1943]---> BDD-cost:    7
c ---[1942]---> BDD-cost:    7
c ---[1941]---> BDD-cost:    7
c ---[1940]---> BDD-cost:    7
c ---[1939]---> BDD-cost:    9
c ---[1938]---> BDD-cost:    9
c ---[1937]---> BDD-cost:    9
c ---[1936]---> BDD-cost:    9
c ---[1935]---> BDD-cost:    9
c ---[1934]---> BDD-cost:    9
c ---[1933]---> BDD-cost:    9
c ---[1932]---> BDD-cost:    9
c ---[1931]---> BDD-cost:    9
c ---[1930]---> BDD-cost:    9
c ---[1929]---> BDD-cost:    9
c ---[1928]---> BDD-cost:    9
c ---[1927]---> BDD-cost:    9
c ---[1926]---> BDD-cost:    9
c ---[1925]---> BDD-cost:    9
c ---[1924]---> BDD-cost:    9
c ---[1923]---> BDD-cost:    9
c ---[1922]---> BDD-cost:    9
c ---[1921]---> BDD-cost:    9
c ---[1920]---> BDD-cost:    9
c ---[1919]---> BDD-cost:    9
c ---[1918]---> BDD-cost:    9
c ---[1917]---> BDD-cost:    9
c ---[1916]---> BDD-cost:    9
c ---[1915]---> BDD-cost:    9
c ---[1914]---> BDD-cost:    9
c ---[1913]---> BDD-cost:    9
c ---[1912]---> BDD-cost:    9
c ---[1911]---> BDD-cost:    9
c ---[1910]---> BDD-cost:    9
c ---[1909]---> BDD-cost:    9
c ---[1908]---> BDD-cost:    9
c ---[1907]---> BDD-cost:    9
c ---[1906]---> BDD-cost:    9
c ---[1905]---> BDD-cost:    9
c ---[1904]---> BDD-cost:    9
c ---[1903]---> BDD-cost:    9
c ---[1902]---> BDD-cost:    9
c ---[1901]---> BDD-cost:    9
c ---[1900]---> BDD-cost:    9
c ---[1899]---> BDD-cost:    9
c ---[1898]---> BDD-cost:    9
c ---[1897]---> BDD-cost:    9
c ---[1896]---> BDD-cost:    9
c ---[1895]---> BDD-cost:    9
c ---[1894]---> BDD-cost:    9
c ---[1893]---> BDD-cost:    9
c ---[1892]---> BDD-cost:    9
c ---[1891]---> BDD-cost:    7
c ---[1890]---> BDD-cost:    7
c ---[1889]---> BDD-cost:    7
c ---[1888]---> BDD-cost:    7
c ---[1887]---> BDD-cost:    0
c ---[1886]---> BDD-cost:    0
c ---[1885]---> BDD-cost:    7
c ---[1884]---> BDD-cost:    0
c ---[1883]---> BDD-cost:    0
c ---[1882]---> BDD-cost:    7
c ---[1881]---> BDD-cost:    0
c ---[1880]---> BDD-cost:    0
c ---[1879]---> BDD-cost:    9
c ---[1878]---> BDD-cost:    9
c ---[1877]---> BDD-cost:    9
c ---[1876]---> BDD-cost:    9
c ---[1875]---> BDD-cost:    9
c ---[1874]---> BDD-cost:    9
c ---[1873]---> BDD-cost:    9
c ---[1872]---> BDD-cost:    9
c ---[1871]---> BDD-cost:    9
c ---[1870]---> BDD-cost:    9
c ---[1869]---> BDD-cost:    9
c ---[1868]---> BDD-cost:    9
c ---[1867]---> BDD-cost:    9
c ---[1866]---> BDD-cost:    9
c ---[1865]---> BDD-cost:    9
c ---[1864]---> BDD-cost:    9
c ---[1863]---> BDD-cost:    9
c ---[1862]---> BDD-cost:    9
c ---[1861]---> BDD-cost:    9
c ---[1860]---> BDD-cost:    9
c ---[1859]---> BDD-cost:    9
c ---[1858]---> BDD-cost:    9
c ---[1857]---> BDD-cost:    9
c ---[1856]---> BDD-cost:    9
c ---[1855]---> BDD-cost:    9
c ---[1854]---> BDD-cost:    9
c ---[1853]---> BDD-cost:    9
c ---[1852]---> BDD-cost:    9
c ---[1851]---> BDD-cost:    9
c ---[1850]---> BDD-cost:    9
c ---[1849]---> BDD-cost:    9
c ---[1848]---> BDD-cost:    9
c ---[1847]---> BDD-cost:    9
c ---[1846]---> BDD-cost:    9
c ---[1845]---> BDD-cost:    9
c ---[1844]---> BDD-cost:    9
c ---[1843]---> BDD-cost:    9
c ---[1842]---> BDD-cost:    9
c ---[1841]---> BDD-cost:    9
c ---[1840]---> BDD-cost:    9
c ---[1839]---> BDD-cost:    9
c ---[1838]---> BDD-cost:    9
c ---[1837]---> BDD-cost:    9
c ---[1836]---> BDD-cost:    9
c ---[1835]---> BDD-cost:    9
c ---[1834]---> BDD-cost:    9
c ---[1833]---> BDD-cost:    9
c ---[1832]---> BDD-cost:    9
c ---[1831]---> BDD-cost:    7
c ---[1830]---> BDD-cost:    0
c ---[1829]---> BDD-cost:    0
c ---[1828]---> BDD-cost:    7
c ---[1827]---> BDD-cost:    0
c ---[1826]---> BDD-cost:    0
c ---[1825]---> BDD-cost:    0
c ---[1824]---> BDD-cost:    0
c ---[1823]---> BDD-cost:    0
c ---[1822]---> BDD-cost:    0
c ---[1821]---> BDD-cost:    0
c ---[1820]---> BDD-cost:    0
c ---[1819]---> BDD-cost:    9
c ---[1818]---> BDD-cost:    9
c ---[1817]---> BDD-cost:    9
c ---[1816]---> BDD-cost:    9
c ---[1815]---> BDD-cost:    9
c ---[1814]---> BDD-cost:    9
c ---[1813]---> BDD-cost:    9
c ---[1812]---> BDD-cost:    9
c ---[1811]---> BDD-cost:    9
c ---[1810]---> BDD-cost:    9
c ---[1809]---> BDD-cost:    9
c ---[1808]---> BDD-cost:    9
c ---[1807]---> BDD-cost:    9
c ---[1806]---> BDD-cost:    9
c ---[1805]---> BDD-cost:    9
c ---[1804]---> BDD-cost:    9
c ---[1803]---> BDD-cost:    9
c ---[1802]---> BDD-cost:    9
c ---[1801]---> BDD-cost:    9
c ---[1800]---> BDD-cost:    9
c ---[1799]---> BDD-cost:    9
c ---[1798]---> BDD-cost:    9
c ---[1797]---> BDD-cost:    9
c ---[1796]---> BDD-cost:    9
c ---[1795]---> BDD-cost:    9
c ---[1794]---> BDD-cost:    9
c ---[1793]---> BDD-cost:    9
c ---[1792]---> BDD-cost:    9
c ---[1791]---> BDD-cost:    9
c ---[1790]---> BDD-cost:    9
c ---[1789]---> BDD-cost:    9
c ---[1788]---> BDD-cost:    9
c ---[1787]---> BDD-cost:    9
c ---[1786]---> BDD-cost:    9
c ---[1785]---> BDD-cost:    9
c ---[1784]---> BDD-cost:    9
c ---[1783]---> BDD-cost:    9
c ---[1782]---> BDD-cost:    9
c ---[1781]---> BDD-cost:    9
c ---[1780]---> BDD-cost:    9
c ---[1779]---> BDD-cost:    9
c ---[1778]---> BDD-cost:    9
c ---[1777]---> BDD-cost:    9
c ---[1776]---> BDD-cost:    9
c ---[1775]---> BDD-cost:    9
c ---[1774]---> BDD-cost:    9
c ---[1773]---> BDD-cost:    9
c ---[1772]---> BDD-cost:    9
c ---[1771]---> BDD-cost:    0
c ---[1770]---> BDD-cost:    0
c ---[1769]---> BDD-cost:    0
c ---[1768]---> BDD-cost:    0
c ---[1767]---> BDD-cost:    0
c ---[1766]---> BDD-cost:    0
c ---[1765]---> BDD-cost:    0
c ---[1764]---> BDD-cost:    0
c ---[1763]---> BDD-cost:    0
c ---[1762]---> BDD-cost:    0
c ---[1761]---> BDD-cost:    0
c ---[1760]---> BDD-cost:    0
c ---[1759]---> BDD-cost:    9
c ---[1758]---> BDD-cost:    9
c ---[1757]---> BDD-cost:    9
c ---[1756]---> BDD-cost:    9
c ---[1755]---> BDD-cost:    9
c ---[1754]---> BDD-cost:    9
c ---[1753]---> BDD-cost:    9
c ---[1752]---> BDD-cost:    9
c ---[1751]---> BDD-cost:    9
c ---[1750]---> BDD-cost:    9
c ---[1749]---> BDD-cost:    9
c ---[1748]---> BDD-cost:    9
c ---[1747]---> BDD-cost:    9
c ---[1746]---> BDD-cost:    9
c ---[1745]---> BDD-cost:    9
c ---[1744]---> BDD-cost:    9
c ---[1743]---> BDD-cost:    9
c ---[1742]---> BDD-cost:    9
c ---[1741]---> BDD-cost:    9
c ---[1740]---> BDD-cost:    9
c ---[1739]---> BDD-cost:    9
c ---[1738]---> BDD-cost:    9
c ---[1737]---> BDD-cost:    9
c ---[1736]---> BDD-cost:    9
c ---[1735]---> BDD-cost:    9
c ---[1734]---> BDD-cost:    9
c ---[1733]---> BDD-cost:    9
c ---[1732]---> BDD-cost:    9
c ---[1731]---> BDD-cost:    9
c ---[1730]---> BDD-cost:    9
c ---[1729]---> BDD-cost:    9
c ---[1728]---> BDD-cost:    9
c ---[1727]---> BDD-cost:    9
c ---[1726]---> BDD-cost:    9
c ---[1725]---> BDD-cost:    9
c ---[1724]---> BDD-cost:    9
c ---[1723]---> BDD-cost:    9
c ---[1722]---> BDD-cost:    9
c ---[1721]---> BDD-cost:    9
c ---[1720]---> BDD-cost:    9
c ---[1719]---> BDD-cost:    9
c ---[1718]---> BDD-cost:    9
c ---[1717]---> BDD-cost:    9
c ---[1716]---> BDD-cost:    9
c ---[1715]---> BDD-cost:    9
c ---[1714]---> BDD-cost:    9
c ---[1713]---> BDD-cost:    9
c ---[1712]---> BDD-cost:    9
c ---[1711]---> BDD-cost:    0
c ---[1710]---> BDD-cost:    0
c ---[1709]---> BDD-cost:    0
c ---[1708]---> BDD-cost:    0
c ---[1707]---> BDD-cost:    0
c ---[1706]---> BDD-cost:    0
c ---[1705]---> BDD-cost:    0
c ---[1704]---> BDD-cost:    0
c ---[1703]---> BDD-cost:    0
c ---[1702]---> BDD-cost:    0
c ---[1701]---> BDD-cost:    0
c ---[1700]---> BDD-cost:    0
c ---[1699]---> BDD-cost:    9
c ---[1698]---> BDD-cost:    9
c ---[1697]---> BDD-cost:    9
c ---[1696]---> BDD-cost:    9
c ---[1695]---> BDD-cost:    9
c ---[1694]---> BDD-cost:    9
c ---[1693]---> BDD-cost:    9
c ---[1692]---> BDD-cost:    9
c ---[1691]---> BDD-cost:    9
c ---[1690]---> BDD-cost:    9
c ---[1689]---> BDD-cost:    9
c ---[1688]---> BDD-cost:    9
c ---[1687]---> BDD-cost:    9
c ---[1686]---> BDD-cost:    9
c ---[1685]---> BDD-cost:    9
c ---[1684]---> BDD-cost:    9
c ---[1683]---> BDD-cost:    9
c ---[1682]---> BDD-cost:    9
c ---[1681]---> BDD-cost:    9
c ---[1680]---> BDD-cost:    9
c ---[1679]---> BDD-cost:    9
c ---[1678]---> BDD-cost:    9
c ---[1677]---> BDD-cost:    9
c ---[1676]---> BDD-cost:    9
c ---[1675]---> BDD-cost:    9
c ---[1674]---> BDD-cost:    9
c ---[1673]---> BDD-cost:    9
c ---[1672]---> BDD-cost:    9
c ---[1671]---> BDD-cost:    9
c ---[1670]---> BDD-cost:    9
c ---[1669]---> BDD-cost:    9
c ---[1668]---> BDD-cost:    9
c ---[1667]---> BDD-cost:    9
c ---[1666]---> BDD-cost:    9
c ---[1665]---> BDD-cost:    9
c ---[1664]---> BDD-cost:    9
c ---[1663]---> BDD-cost:    9
c ---[1662]---> BDD-cost:    9
c ---[1661]---> BDD-cost:    9
c ---[1660]---> BDD-cost:    9
c ---[1659]---> BDD-cost:    9
c ---[1658]---> BDD-cost:    9
c ---[1657]---> BDD-cost:    9
c ---[1656]---> BDD-cost:    9
c ---[1655]---> BDD-cost:    9
c ---[1654]---> BDD-cost:    9
c ---[1653]---> BDD-cost:    9
c ---[1652]---> BDD-cost:    9
c ---[ 300]---> Adder-cost: 280   maxlim: 14705   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  101193   266718 |   33731       0        0     nan |  0.000 % |
c |       100 |  100534   265202 |   37104      92      512     5.6 |  8.109 % |
c |       250 |  100502   265124 |   40814     240     2054     8.6 |  8.131 % |
c |       475 |  100138   264286 |   44895     440     4464    10.1 |  8.363 % |
c |       812 |   99950   263676 |   49385     755     9441    12.5 |  8.444 % |
c |      1319 |   99362   262289 |   54324    1244    17164    13.8 |  8.783 % |
c ==============================================================================
c [1mFound solution: 447616[0m
c ---[   0]---> Adder-cost: 6802   maxlim: 93924044   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1400 |  146849   432019 |   48949    1324    18215    13.8 |  8.783 % |
c |      1500 |  146849   432019 |   53843    1424    19965    14.0 |  8.033 % |
c |      1652 |  146732   431754 |   59228    1562    23861    15.3 |  8.163 % |
c |      1877 |  146529   431275 |   65151    1763    26436    15.0 |  8.199 % |
c |      2214 |  146506   431224 |   71666    2098    30500    14.5 |  8.212 % |
c |      2720 |  146393   430827 |   78832    2590    34833    13.4 |  8.252 % |
c |      3479 |  145329   428259 |   86716    3287    53181    16.2 |  8.841 % |
c |      4618 |  143893   425006 |   95387    4379    74780    17.1 |  9.723 % |
c |      6327 |  142756   421992 |  104926    6011   116646    19.4 | 10.261 % |
c |      8889 |  141873   419506 |  115419    8382   168338    20.1 | 10.665 % |
c |     12733 |  140707   416462 |  126961   12134   261737    21.6 | 11.284 % |
c ==============================================================================
c [1mFound solution: 350414[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94021246   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13997 |  139478   413612 |   46492   13289   274518    20.7 | 11.284 % |
c |     14097 |  139458   413567 |   51141   13388   276291    20.6 | 12.011 % |
c |     14247 |  139454   413558 |   56255   13536   278967    20.6 | 12.013 % |
c |     14472 |  139259   413084 |   61880   13733   281669    20.5 | 12.118 % |
c |     14811 |  138994   412455 |   68068   14053   286532    20.4 | 12.259 % |
c ==============================================================================
c [1mFound solution: 341229[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94030431   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15282 |  138876   412188 |   46292   14510   289549    20.0 | 12.259 % |
c |     15384 |  138876   412188 |   50921   14612   292634    20.0 | 12.339 % |
c |     15534 |  138876   412188 |   56013   14762   293371    19.9 | 12.339 % |
c ==============================================================================
c [1mFound solution: 339182[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94032478   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15726 |  138892   412333 |   46297   14954   295772    19.8 | 12.339 % |
c |     15826 |  138892   412333 |   50926   15054   296620    19.7 | 12.351 % |
c |     15976 |  138892   412333 |   56019   15204   297411    19.6 | 12.351 % |
c |     16201 |  138855   412240 |   61621   15426   300476    19.5 | 12.368 % |
c |     16538 |  138807   412119 |   67783   15759   303537    19.3 | 12.397 % |
c ==============================================================================
c [1mFound solution: 296942[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94074718   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16696 |  138791   412206 |   46263   15915   305467    19.2 | 12.397 % |
c ==============================================================================
c [1mFound solution: 296909[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94074751   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16770 |  138792   412219 |   46264   15989   305837    19.1 | 12.397 % |
c ==============================================================================
c [1mFound solution: 274925[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94096735   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16844 |  138559   411743 |   46186   16060   306610    19.1 | 12.397 % |
c ==============================================================================
c [1mFound solution: 274897[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94096763   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16927 |  138565   411799 |   46188   16143   307722    19.1 | 12.397 % |
c ==============================================================================
c [1mFound solution: 274893[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94096767   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16954 |  138566   411812 |   46188   16170   307814    19.0 | 12.397 % |
c ==============================================================================
c [1mFound solution: 274797[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94096863   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16970 |  138568   411841 |   46189   16186   307878    19.0 | 12.397 % |
c ==============================================================================
c [1mFound solution: 274765[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94096895   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16977 |  138569   411852 |   46189   16193   307901    19.0 | 12.397 % |
c |     17077 |  138421   411510 |   50807   16279   310101    19.0 | 12.692 % |
c ==============================================================================
c [1mFound solution: 274285[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94097375   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17102 |  138429   411572 |   46143   16304   310241    19.0 | 12.692 % |
c ==============================================================================
c [1mFound solution: 274253[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94097407   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17142 |  138422   411553 |   46140   16343   310368    19.0 | 12.692 % |
c |     17242 |  138406   411501 |   50754   16440   310799    18.9 | 12.708 % |
c |     17392 |  138351   411381 |   55829   16584   314320    19.0 | 12.743 % |
c |     17617 |  137649   409758 |   61412   16753   320156    19.1 | 13.152 % |
c ==============================================================================
c [1mFound solution: 270701[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94100959   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17812 |  137459   409335 |   45819   16938   323200    19.1 | 13.152 % |
c ==============================================================================
c [1mFound solution: 270669[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94100991   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17835 |  137461   409348 |   45820   16961   323274    19.1 | 13.152 % |
c ==============================================================================
c [1mFound solution: 270161[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94101499   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17851 |  137475   409460 |   45825   16977   323332    19.0 | 13.152 % |
c ==============================================================================
c [1mFound solution: 270157[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94101503   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17854 |  137476   409467 |   45825   16980   323354    19.0 | 13.152 % |
c ==============================================================================
c [1mFound solution: 266573[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94105087   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17856 |  137482   409502 |   45827   16982   323360    19.0 | 13.152 % |
c ==============================================================================
c [1mFound solution: 266061[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94105599   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17893 |  137033   408478 |   45677   17018   323763    19.0 | 13.152 % |
c |     17993 |  136921   408220 |   50244   17117   325712    19.0 | 13.595 % |
c ==============================================================================
c [1mFound solution: 262541[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94109119   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18045 |  136900   408209 |   45633   17168   326329    19.0 | 13.595 % |
c |     18146 |  136888   408170 |   50196   17266   327961    19.0 | 13.623 % |
c ==============================================================================
c [1mFound solution: 262205[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94109455   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18166 |  136893   408210 |   45631   17286   328225    19.0 | 13.623 % |
c ==============================================================================
c [1mFound solution: 262129[0m
c ---[   0]---> Adder-cost: 154   maxlim: 46923611   bits: 26/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18206 |  135677   403900 |   45225   17253   328574    19.0 | 13.623 % |
c |     18310 |  135456   403391 |   49747   17327   330665    19.1 | 14.639 % |
c |     18460 |  135142   402437 |   54722   17455   332626    19.1 | 14.772 % |
c ==============================================================================
c [1mFound solution: 262109[0m
c ---[   0]---> Adder-cost: 0   maxlim: 46923631   bits: 26/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18602 |  134962   402055 |   44987   17588   336264    19.1 | 14.772 % |
c |     18702 |  134873   401775 |   49485   17679   337780    19.1 | 14.909 % |
c |     18854 |  134864   401746 |   54434   17830   338774    19.0 | 14.913 % |
c |     19080 |  131859   394723 |   59877   17946   346404    19.3 | 16.634 % |
c |     19422 |  131852   394700 |   65865   18286   351198    19.2 | 16.636 % |
c ==============================================================================
c [1mFound solution: 262093[0m
c ---[   0]---> Adder-cost: 0   maxlim: 46923647   bits: 26/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19863 |  131696   394272 |   43898   18715   357423    19.1 | 16.636 % |
c ==============================================================================
c [1mFound solution: 262030[0m
c ---[   0]---> Adder-cost: 0   maxlim: 46923710   bits: 26/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19870 |  131706   394379 |   43902   18722   357462    19.1 | 16.636 % |
c ==============================================================================
c [1mFound solution: 262029[0m
c ---[   0]---> Adder-cost: 0   maxlim: 46923711   bits: 26/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19880 |  131708   394391 |   43902   18732   357529    19.1 | 16.636 % |
c ==============================================================================
c [1mFound solution: 261965[0m
c ---[   0]---> Adder-cost: 0   maxlim: 46923775   bits: 26/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19883 |  131684   394067 |   43894   18733   357537    19.1 | 16.636 % |
c |     19983 |  131288   392785 |   48283   18748   358133    19.1 | 16.868 % |
c |     20133 |  130870   391327 |   53111   18797   359662    19.1 | 16.993 % |
c ==============================================================================
c [1mFound solution: 242189[0m
c ---[   0]---> Adder-cost: 0   maxlim: 46943551   bits: 26/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20149 |  130879   391377 |   43626   18813   359725    19.1 | 16.993 % |
c ==============================================================================
c [1mFound solution: 242125[0m
c ---[   0]---> Adder-cost: 0   maxlim: 46943615   bits: 26/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20153 |  130881   391388 |   43627   18817   359751    19.1 | 16.993 % |
c ==============================================================================
c [1mFound solution: 242061[0m
c ---[   0]---> Adder-cost: 0   maxlim: 46943679   bits: 26/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20158 |  130883   391399 |   43627   18822   359769    19.1 | 16.993 % |
c ==============================================================================
c [1mFound solution: 241998[0m
c ---[   0]---> Adder-cost: 0   maxlim: 46943742   bits: 26/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20165 |  130895   391492 |   43631   18829   359803    19.1 | 16.993 % |
c ==============================================================================
c [1mFound solution: 239117[0m
c ---[   0]---> Adder-cost: 0   maxlim: 46946623   bits: 26/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20170 |  130902   391536 |   43634   18834   359829    19.1 | 16.993 % |
c ==============================================================================
c [1mFound solution: 81421[0m
c ---[   0]---> Adder-cost: 154   maxlim: 23511359   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20186 |  129358   385977 |   43119   18744   359535    19.2 | 16.993 % |
c |     20288 |  128999   384768 |   47430   18793   360282    19.2 | 18.092 % |
c |     20438 |  128999   384768 |   52173   18943   363075    19.2 | 18.092 % |
c ==============================================================================
c [1mFound solution: 81357[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23511423   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20575 |  128391   382652 |   42797   18877   362799    19.2 | 18.092 % |
c ==============================================================================
c [1mFound solution: 80366[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23512414   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20644 |  128189   382092 |   42729   18924   363587    19.2 | 18.092 % |
c |     20744 |  127918   381200 |   47001   18969   364522    19.2 | 18.514 % |
c |     20894 |  127909   381171 |   51702   19118   367822    19.2 | 18.518 % |
c ==============================================================================
c [1mFound solution: 79373[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23513407   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20923 |  127915   381199 |   42638   19147   367930    19.2 | 18.518 % |
c ==============================================================================
c [1mFound solution: 78605[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23514175   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20955 |  127919   381220 |   42639   19179   368047    19.2 | 18.518 % |
c ==============================================================================
c [1mFound solution: 78349[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23514431   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20982 |  127923   381234 |   42641   19206   368213    19.2 | 18.518 % |
c |     21083 |  127914   381205 |   46905   19302   369152    19.1 | 18.530 % |
c ==============================================================================
c [1mFound solution: 78285[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23514495   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21113 |  127916   381212 |   42638   19332   369316    19.1 | 18.530 % |
c ==============================================================================
c [1mFound solution: 78254[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23514526   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21160 |  127908   381238 |   42636   19377   369580    19.1 | 18.530 % |
c ==============================================================================
c [1mFound solution: 78221[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23514559   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21216 |  127889   381178 |   42629   19431   369864    19.0 | 18.530 % |
c ==============================================================================
c [1mFound solution: 78157[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23514623   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21259 |  127868   381134 |   42622   19472   370339    19.0 | 18.530 % |
c |     21360 |  127853   381101 |   46884   19572   371055    19.0 | 18.573 % |
c ==============================================================================
c [1mFound solution: 77869[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23514911   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21379 |  127856   381124 |   42618   19591   371250    19.0 | 18.573 % |
c |     21479 |  127649   380648 |   46879   19674   373215    19.0 | 18.699 % |
c ==============================================================================
c [1mFound solution: 77837[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23514943   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21537 |  127592   380456 |   42530   19725   373408    18.9 | 18.699 % |
c |     21637 |  127592   380456 |   46783   19825   375766    19.0 | 18.719 % |
c |     21787 |  127470   380034 |   51461   19955   376841    18.9 | 18.758 % |
c ==============================================================================
c [1mFound solution: 62269[0m
c ---[   0]---> Adder-cost: 154   maxlim: 11734031   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21925 |  126190   375384 |   42063   19922   376802    18.9 | 18.758 % |
c |     22025 |  125845   374465 |   46269   20005   377429    18.9 | 19.745 % |
c ==============================================================================
c [1mFound solution: 45885[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11750415   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22072 |  124806   370646 |   41602   19820   375974    19.0 | 19.745 % |
c |     22172 |  124773   370558 |   45762   19916   376603    18.9 | 20.109 % |
c |     22323 |  124619   370091 |   50338   20029   380089    19.0 | 20.167 % |
c |     22550 |  124385   369396 |   55372   20229   383179    18.9 | 20.274 % |
c ==============================================================================
c [1mFound solution: 31550[0m
c ---[   0]---> Adder-cost: 154   maxlim: 5866510   bits: 23/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22608 |  122974   363905 |   40991   20115   382917    19.0 | 20.274 % |
c |     22709 |  122974   363905 |   45090   20216   383656    19.0 | 21.150 % |
c |     22860 |  122797   363414 |   49599   20316   384515    18.9 | 21.229 % |
c |     23089 |  122619   362896 |   54559   20500   387239    18.9 | 21.306 % |
c ==============================================================================
c [1mFound solution: 31533[0m
c ---[   0]---> Adder-cost: 0   maxlim: 5866527   bits: 23/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23248 |  122612   362882 |   40870   20656   388991    18.8 | 21.306 % |
c |     23349 |  122593   362813 |   44957   20745   391469    18.9 | 21.312 % |
c |     23499 |  122471   362417 |   49452   20845   392908    18.8 | 21.355 % |
c |     23724 |  122416   362293 |   54397   21067   397103    18.8 | 21.389 % |
c ==============================================================================
c [1mFound solution: 31469[0m
c ---[   0]---> Adder-cost: 0   maxlim: 5866591   bits: 23/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24005 |  122062   361116 |   40687   21215   399760    18.8 | 21.389 % |
c |     24107 |  122053   361087 |   44755   21316   401813    18.9 | 21.515 % |
c |     24257 |  122003   360931 |   49231   21465   404686    18.9 | 21.535 % |
c |     24483 |  122003   360931 |   54154   21691   412381    19.0 | 21.535 % |
c |     24820 |  121440   359453 |   59569   21904   417833    19.1 | 21.831 % |
c |     25326 |  121341   359211 |   65526   22408   429692    19.2 | 21.889 % |
c ==============================================================================
c [1mFound solution: 31309[0m
c ---[   0]---> Adder-cost: 0   maxlim: 5866751   bits: 23/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25585 |  121343   359224 |   40447   22667   434928    19.2 | 21.889 % |
c ==============================================================================
c [1mFound solution: 27597[0m
c ---[   0]---> Adder-cost: 0   maxlim: 5870463   bits: 23/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25676 |  121349   359272 |   40449   22758   437297    19.2 | 21.889 % |
c ==============================================================================
c [1mFound solution: 16077[0m
c ---[   0]---> Adder-cost: 154   maxlim: 2932863   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25761 |  119844   353898 |   39948   22548   437384    19.4 | 21.889 % |
c ==============================================================================
c [1mFound solution: 15821[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2933119   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25779 |  119848   353923 |   39949   22566   437589    19.4 | 21.889 % |
c ==============================================================================
c [1mFound solution: 15693[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2933247   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25785 |  119850   353935 |   39950   22572   437627    19.4 | 21.889 % |
c ==============================================================================
c [1mFound solution: 15501[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2933439   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25793 |  119854   353964 |   39951   22580   437674    19.4 | 21.889 % |
c ==============================================================================
c [1mFound solution: 12814[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936126   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25839 |  118945   350758 |   39648   22367   436353    19.5 | 21.889 % |
c |     25939 |  118945   350758 |   43612   22467   440184    19.6 | 23.152 % |
c ==============================================================================
c [1mFound solution: 12749[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936191   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25951 |  118947   350769 |   39649   22479   440338    19.6 | 23.152 % |
c ==============================================================================
c [1mFound solution: 12621[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936319   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25960 |  118949   350779 |   39649   22488   440462    19.6 | 23.152 % |
c ==============================================================================
c [1mFound solution: 12301[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936639   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25965 |  118953   350801 |   39651   22493   440494    19.6 | 23.152 % |
c ==============================================================================
c [1mFound solution: 12237[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936703   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25976 |  118955   350812 |   39651   22504   440625    19.6 | 23.152 % |
c ==============================================================================
c [1mFound solution: 12110[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936830   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26019 |  118823   350565 |   39607   22527   440808    19.6 | 23.152 % |
c ==============================================================================
c [1mFound solution: 12109[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936831   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26024 |  118824   350572 |   39608   22532   440822    19.6 | 23.152 % |
c ==============================================================================
c [1mFound solution: 10957[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2937983   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26069 |  118828   350597 |   39609   22577   441095    19.5 | 23.152 % |
c |     26173 |  118819   350570 |   43569   22680   442370    19.5 | 23.259 % |
c |     26323 |  118784   350463 |   47926   22828   448750    19.7 | 23.272 % |
c ==============================================================================
c [1mFound solution: 10894[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2938046   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26442 |  117415   345654 |   39138   22639   449051    19.8 | 23.272 % |
c ==============================================================================
c [1mFound solution: 10893[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2938047   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26445 |  117417   345665 |   39139   22642   449087    19.8 | 23.272 % |
c |     26547 |  117401   345613 |   43052   22742   450419    19.8 | 23.778 % |
c ==============================================================================
c [1mFound solution: 10797[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2938143   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26593 |  117405   345631 |   39135   22788   451211    19.8 | 23.778 % |
c ==============================================================================
c [1mFound solution: 10765[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2938175   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26602 |  117407   345639 |   39135   22797   451331    19.8 | 23.778 % |
c ==============================================================================
c [1mFound solution: 10749[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2938191   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26628 |  117402   345632 |   39134   22820   451461    19.8 | 23.778 % |
c ==============================================================================
c [1mFound solution: 10701[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2938239   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26628 |  117404   345641 |   39134   22820   451461    19.8 | 23.778 % |
c ==============================================================================
c [1mFound solution: 10637[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2938303   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26628 |  117406   345651 |   39135   22820   451461    19.8 | 23.778 % |
c ==============================================================================
c [1mFound solution: 10573[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2938367   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26631 |  117408   345658 |   39136   22823   451469    19.8 | 23.778 % |
c ==============================================================================
c [1mFound solution: 10253[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2938687   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26631 |  117412   345674 |   39137   22823   451469    19.8 | 23.778 % |
c ==============================================================================
c [1mFound solution: 10189[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2938751   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26631 |  117414   345682 |   39138   22823   451469    19.8 | 23.778 % |
c ==============================================================================
c [1mFound solution: 10126[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2938814   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26631 |  117426   345748 |   39142   22823   451469    19.8 | 23.778 % |
c ==============================================================================
c [1mFound solution: 10125[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2938815   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26632 |  117428   345758 |   39142   22824   451480    19.8 | 23.778 % |
c ==============================================================================
c [1mFound solution: 10061[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2938879   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26651 |  117414   345712 |   39138   22841   451750    19.8 | 23.778 % |
c |     26751 |  117381   345622 |   43051   22937   453206    19.8 | 23.824 % |
c ==============================================================================
c [1mFound solution: 9933[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2939007   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26753 |  117383   345631 |   39127   22939   453226    19.8 | 23.824 % |
c ==============================================================================
c [1mFound solution: 9741[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2939199   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26762 |  117387   345645 |   39129   22948   453649    19.8 | 23.824 % |
c ==============================================================================
c [1mFound solution: 9485[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2939455   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26809 |  117391   345661 |   39130   22995   454365    19.8 | 23.824 % |
c ==============================================================================
c [1mFound solution: 7693[0m
c ---[   0]---> Adder-cost: 154   maxlim: 1466687   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26821 |  116716   343001 |   38905   22851   453994    19.9 | 23.824 % |
c ==============================================================================
c [1mFound solution: 7373[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1467007   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26872 |  116720   343022 |   38906   22902   454284    19.8 | 23.824 % |
c ==============================================================================
c [1mFound solution: 7325[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1467055   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26889 |  116724   343050 |   38908   22919   454909    19.8 | 23.824 % |
c |     26992 |  116724   343050 |   42798   23022   457175    19.9 | 24.440 % |
c ==============================================================================
c [1mFound solution: 7181[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1467199   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26997 |  116728   343075 |   38909   23027   457205    19.9 | 24.440 % |
c ==============================================================================
c [1mFound solution: 7117[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1467263   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26998 |  116730   343087 |   38910   23028   457208    19.9 | 24.440 % |
c ==============================================================================
c [1mFound solution: 6605[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1467775   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27000 |  116735   343115 |   38911   23030   457242    19.9 | 24.440 % |
c ==============================================================================
c [1mFound solution: 4670[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1469710   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27063 |  116747   343207 |   38915   23093   458996    19.9 | 24.440 % |
c |     27163 |  116273   341673 |   42806   22967   459682    20.0 | 24.621 % |
c ==============================================================================
c [1mFound solution: 4605[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1469775   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27209 |  115925   340888 |   38641   23012   461409    20.1 | 24.621 % |
c ==============================================================================
c [1mFound solution: 4589[0m
c ---[   0]---> Adder-cost: 0   maxlim: 1469791   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27246 |  115927   340901 |   38642   23049   461707    20.0 | 24.621 % |
c ==============================================================================
c [1mFound solution: 2878[0m
c ---[   0]---> Adder-cost: 154   maxlim: 734222   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27268 |  114886   337127 |   38295   22769   461618    20.3 | 24.621 % |
c |     27368 |  114886   337127 |   42124   22869   466900    20.4 | 25.600 % |
c |     27518 |  114757   336688 |   46336   22972   470663    20.5 | 25.637 % |
c ==============================================================================
c [1mFound solution: 2877[0m
c ---[   0]---> Adder-cost: 0   maxlim: 734223   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27632 |  114573   336063 |   38191   23052   474052    20.6 | 25.637 % |
c |     27733 |  114508   335896 |   42010   23152   479886    20.7 | 25.716 % |
c |     27887 |  114412   335676 |   46211   23298   483276    20.7 | 25.773 % |
c ==============================================================================
c [1mFound solution: 2849[0m
c ---[   0]---> Adder-cost: 0   maxlim: 734251   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27966 |  114417   335720 |   38139   23377   485520    20.8 | 25.773 % |
c |     28066 |  114394   335657 |   41952   23474   487829    20.8 | 25.789 % |
c ==============================================================================
c [1mFound solution: 2845[0m
c ---[   0]---> Adder-cost: 0   maxlim: 734255   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28190 |  113458   332438 |   37819   23269   488275    21.0 | 25.789 % |
c |     28292 |  113458   332438 |   41600   23371   491210    21.0 | 26.082 % |
c |     28442 |  113458   332438 |   45760   23521   498738    21.2 | 26.082 % |
c ==============================================================================
c [1mFound solution: 2829[0m
c ---[   0]---> Adder-cost: 0   maxlim: 734271   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28454 |  113460   332448 |   37820   23533   499193    21.2 | 26.082 % |
c ==============================================================================
c [1mFound solution: 2826[0m
c ---[   0]---> Adder-cost: 0   maxlim: 734274   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28475 |  113462   332481 |   37820   23554   500107    21.2 | 26.082 % |
c ==============================================================================
c [1mFound solution: 2825[0m
c ---[   0]---> Adder-cost: 0   maxlim: 734275   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28511 |  113463   332496 |   37821   23590   500608    21.2 | 26.082 % |
c ==============================================================================
c [1mFound solution: 2817[0m
c ---[   0]---> Adder-cost: 0   maxlim: 734283   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28526 |  113467   332526 |   37822   23605   501203    21.2 | 26.082 % |
c ==============================================================================
c [1mFound solution: 2816[0m
c ---[   0]---> Adder-cost: 0   maxlim: 734284   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28563 |  113469   332545 |   37823   23642   501707    21.2 | 26.082 % |
c |     28666 |  113469   332545 |   41605   23745   511479    21.5 | 26.090 % |
c ==============================================================================
c [1mFound solution: 2813[0m
c ---[   0]---> Adder-cost: 0   maxlim: 734287   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28694 |  113471   332558 |   37823   23773   511981    21.5 | 26.090 % |
c ==============================================================================
c [1mFound solution: 2765[0m
c ---[   0]---> Adder-cost: 0   maxlim: 734335   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28720 |  113473   332569 |   37824   23799   513643    21.6 | 26.090 % |
c ==============================================================================
c [1mFound solution: 2701[0m
c ---[   0]---> Adder-cost: 0   maxlim: 734399   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28739 |  113475   332581 |   37825   23818   514330    21.6 | 26.090 % |
c |     28840 |  113475   332581 |   41607   23919   518024    21.7 | 26.093 % |
c |     28991 |  113126   331376 |   45768   23878   520343    21.8 | 26.204 % |
c |     29216 |  113126   331376 |   50345   24103   534980    22.2 | 26.204 % |
c ==============================================================================
c [1mFound solution: 2700[0m
c ---[   0]---> Adder-cost: 0   maxlim: 734400   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29462 |  113127   331393 |   37709   24349   544884    22.4 | 26.204 % |
c |     29562 |  113085   331296 |   41479   24448   550813    22.5 | 26.225 % |
c |     29716 |  113085   331296 |   45627   24602   555768    22.6 | 26.225 % |
c ==============================================================================
c [1mFound solution: 2685[0m
c ---[   0]---> Adder-cost: 0   maxlim: 734415   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29735 |  113087   331311 |   37695   24621   556279    22.6 | 26.225 % |
c |     29836 |  113004   331016 |   41464   24678   557931    22.6 | 26.252 % |
c ==============================================================================
c [1mFound solution: 1853[0m
c ---[   0]---> Adder-cost: 154   maxlim: 366607   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29901 |  111274   324174 |   37091   24261   556139    22.9 | 26.252 % |
c |     30001 |  111274   324174 |   40800   24361   559291    23.0 | 27.192 % |
c |     30159 |  111274   324174 |   44880   24519   570868    23.3 | 27.192 % |
c ==============================================================================
c [1mFound solution: 1789[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366671   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30326 |  111186   323876 |   37062   24560   575134    23.4 | 27.192 % |
c ==============================================================================
c [1mFound solution: 1773[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366687   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30331 |  111188   323887 |   37062   24565   575171    23.4 | 27.192 % |
c ==============================================================================
c [1mFound solution: 1741[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366719   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30376 |  111189   323894 |   37063   24610   577037    23.4 | 27.192 % |
c |     30479 |  111189   323894 |   40769   24713   582908    23.6 | 27.222 % |
c |     30633 |  110906   322854 |   44846   24765   590452    23.8 | 27.309 % |
c |     30858 |  110906   322854 |   49330   24990   601437    24.1 | 27.309 % |
c |     31196 |  110906   322854 |   54263   25328   618119    24.4 | 27.309 % |
c |     31704 |  110906   322854 |   59690   25836   644673    25.0 | 27.309 % |
c |     32463 |  110810   322627 |   65659   26588   679806    25.6 | 27.362 % |
c |     33604 |  110405   321414 |   72225   27527   739929    26.9 | 27.533 % |
c ==============================================================================
c [1mFound solution: 1725[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366735   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34267 |  110407   321427 |   36802   28190   765391    27.2 | 27.533 % |
c |     34368 |  110407   321427 |   40482   28291   769032    27.2 | 27.534 % |
c |     34518 |  110324   321138 |   44530   28417   774973    27.3 | 27.558 % |
c |     34743 |  110324   321138 |   48983   28642   782733    27.3 | 27.558 % |
c |     35082 |  110238   320840 |   53881   28933   798288    27.6 | 27.584 % |
c |     35589 |  110238   320840 |   59269   29440   822276    27.9 | 27.584 % |
c |     36348 |  110142   320520 |   65196   30172   854066    28.3 | 27.614 % |
c |     37487 |  110066   320313 |   71716   31244   923446    29.6 | 27.650 % |
c ==============================================================================
c [1mFound solution: 1711[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366749   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38388 |  109596   318762 |   36532   31955   969322    30.3 | 27.650 % |
c |     38489 |  108969   316618 |   40185   31814   972879    30.6 | 28.042 % |
c ==============================================================================
c [1mFound solution: 1709[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366751   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38494 |  108971   316625 |   36323   31819   972991    30.6 | 28.042 % |
c |     38599 |  108915   316427 |   39955   31912   977291    30.6 | 28.070 % |
c ==============================================================================
c [1mFound solution: 1679[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366781   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38656 |  108923   316458 |   36307   31969   979499    30.6 | 28.070 % |
c |     38756 |  108923   316458 |   39937   32069   983604    30.7 | 28.073 % |
c ==============================================================================
c [1mFound solution: 1610[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366850   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38796 |  108928   316488 |   36309   32109   985365    30.7 | 28.073 % |
c |     38897 |  108928   316488 |   39939   32210   992189    30.8 | 28.076 % |
c |     39048 |  108729   315629 |   43933   32236   991849    30.8 | 28.135 % |
c |     39274 |  108729   315629 |   48327   32462  1000933    30.8 | 28.135 % |
c |     39611 |  108668   315488 |   53160   32796  1014157    30.9 | 28.172 % |
c |     40117 |  108661   315471 |   58476   33035  1019568    30.9 | 28.178 % |
c |     40878 |  108598   315324 |   64323   33789  1052419    31.1 | 28.213 % |
c ==============================================================================
c [1mFound solution: 1609[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366851   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41334 |  108600   315336 |   36200   34245  1072151    31.3 | 28.213 % |
c |     41434 |  108600   315336 |   39820   34345  1075160    31.3 | 28.213 % |
c |     41584 |  108600   315336 |   43802   34495  1079085    31.3 | 28.213 % |
c |     41810 |  108354   314762 |   48182   34704  1089214    31.4 | 28.354 % |
c |     42147 |  108354   314762 |   53000   35041  1101705    31.4 | 28.354 % |
c |     42654 |  108354   314762 |   58300   35548  1123418    31.6 | 28.354 % |
c |     43414 |  108354   314762 |   64130   36308  1165021    32.1 | 28.354 % |
c ==============================================================================
c [1mFound solution: 1607[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366853   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43541 |  108355   314773 |   36118   36435  1172349    32.2 | 28.354 % |
c |     43641 |  108355   314773 |   39729   36535  1178010    32.2 | 28.355 % |
c |     43791 |  107810   313518 |   43702   36681  1186416    32.3 | 28.657 % |
c |     44016 |  107810   313518 |   48073   36906  1199162    32.5 | 28.657 % |
c ==============================================================================
c [1mFound solution: 1597[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366863   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44321 |  106986   311591 |   35662   37208  1214639    32.6 | 28.657 % |
c |     44421 |  106986   311591 |   39228   37308  1219787    32.7 | 29.183 % |
c ==============================================================================
c [1mFound solution: 1567[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366893   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44425 |  106994   311632 |   35664   37312  1219941    32.7 | 29.183 % |
c |     44526 |  106994   311632 |   39230   37413  1224421    32.7 | 29.186 % |
c |     44676 |  106994   311632 |   43153   37563  1236789    32.9 | 29.186 % |
c |     44905 |  106994   311632 |   47468   37792  1250427    33.1 | 29.186 % |
c |     45242 |  106994   311632 |   52215   38129  1266460    33.2 | 29.186 % |
c |     45750 |  106990   311622 |   57437   38636  1294672    33.5 | 29.190 % |
c ==============================================================================
c [1mFound solution: 1565[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366895   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46190 |  106992   311630 |   35664   39076  1316421    33.7 | 29.190 % |
c |     46291 |  106992   311630 |   39230   39177  1321318    33.7 | 29.190 % |
c |     46442 |  106992   311630 |   43153   39328  1330902    33.8 | 29.190 % |
c |     46669 |  106969   311577 |   47468   39554  1343419    34.0 | 29.201 % |
c |     47006 |  106969   311577 |   52215   39891  1359640    34.1 | 29.201 % |
c ==============================================================================
c [1mFound solution: 1561[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366899   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47324 |  106970   311587 |   35656   40209  1374281    34.2 | 29.201 % |
c |     47424 |  106970   311587 |   39221   40309  1382170    34.3 | 29.203 % |
c ==============================================================================
c [1mFound solution: 1557[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366903   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47509 |  106972   311596 |   35657   40394  1386818    34.3 | 29.203 % |
c ==============================================================================
c [1mFound solution: 1553[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366907   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47509 |  106974   311605 |   35658   40394  1386818    34.3 | 29.203 % |
c ==============================================================================
c [1mFound solution: 1551[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366909   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47511 |  106976   311614 |   35658   40396  1386829    34.3 | 29.203 % |
c ==============================================================================
c [1mFound solution: 1549[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366911   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47516 |  106977   311617 |   35659   40401  1386901    34.3 | 29.203 % |
c ==============================================================================
c [1mFound solution: 1547[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366913   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47517 |  106979   311627 |   35659   40402  1386940    34.3 | 29.203 % |
c ==============================================================================
c [1mFound solution: 1539[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366921   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47521 |  106982   311647 |   35660   40406  1387096    34.3 | 29.203 % |
c ==============================================================================
c [1mFound solution: 1537[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366923   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47536 |  106984   311656 |   35661   40421  1387714    34.3 | 29.203 % |
c ==============================================================================
c [1mFound solution: 1536[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366924   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47538 |  106986   311665 |   35662   40423  1387731    34.3 | 29.203 % |
c |     47638 |  106986   311665 |   39228   40523  1392624    34.4 | 29.211 % |
c ==============================================================================
c [1mFound solution: 1535[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366925   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47703 |  106988   311676 |   35662   40588  1393841    34.3 | 29.211 % |
c |     47803 |  106988   311676 |   39228   40688  1397991    34.4 | 29.211 % |
c |     47954 |  106977   311652 |   43151   40838  1403476    34.4 | 29.219 % |
c |     48181 |  106943   311575 |   47466   41064  1414116    34.4 | 29.239 % |
c |     48518 |  106943   311575 |   52212   41401  1431110    34.6 | 29.239 % |
c |     49026 |  106879   311426 |   57434   41908  1454683    34.7 | 29.287 % |
c |     49788 |  106879   311426 |   63177   42670  1490984    34.9 | 29.287 % |
c |     50929 |  106879   311426 |   69495   43811  1552493    35.4 | 29.287 % |
c |     52639 |  106879   311426 |   76444   45521  1618250    35.5 | 29.287 % |
c |     55202 |  106879   311426 |   84089   48084  1743246    36.3 | 29.287 % |
c ==============================================================================
c [1mFound solution: 1533[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366927   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55556 |  106881   311433 |   35627   48438  1760919    36.4 | 29.287 % |
c |     55656 |  106881   311433 |   39189   48538  1765778    36.4 | 29.288 % |
c |     55807 |  106881   311433 |   43108   48689  1775576    36.5 | 29.288 % |
c |     56033 |  106881   311433 |   47419   48915  1787758    36.5 | 29.288 % |
c |     56371 |  106881   311433 |   52161   49253  1806407    36.7 | 29.288 % |
c |     56879 |  106881   311433 |   57377   49761  1830636    36.8 | 29.288 % |
c |     57638 |  106851   311365 |   63115   50519  1864949    36.9 | 29.304 % |
c ==============================================================================
c [1mFound solution: 1523[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366937   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     58747 |  106855   311385 |   35618   51628  1912551    37.0 | 29.304 % |
c |     58847 |  106855   311385 |   39179   17212   632867    36.8 | 29.306 % |
c |     58998 |  106855   311385 |   43097   17363   640134    36.9 | 29.306 % |
c |     59223 |  106855   311385 |   47407   17588   652897    37.1 | 29.306 % |
c |     59561 |  106802   311250 |   52148   17924   668389    37.3 | 29.339 % |
c |     60070 |  106802   311250 |   57363   18433   690957    37.5 | 29.339 % |
c |     60830 |  106802   311250 |   63099   19193   730351    38.1 | 29.339 % |
c |     61972 |  106802   311250 |   69409   20335   782320    38.5 | 29.339 % |
c |     63680 |  106802   311250 |   76350   22043   858777    39.0 | 29.339 % |
c |     66244 |  106267   310002 |   83985   24589   998230    40.6 | 29.656 % |
c |     70088 |  106222   309896 |   92383   28429  1169493    41.1 | 29.683 % |
c ==============================================================================
c [1mFound solution: 1517[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366943   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     71008 |  106224   309903 |   35408   29349  1230223    41.9 | 29.683 % |
c |     71108 |  106224   309903 |   38948   29449  1235287    41.9 | 29.684 % |
c |     71259 |  106224   309903 |   42843   29600  1242663    42.0 | 29.684 % |
c |     71484 |  106224   309903 |   47128   29825  1258794    42.2 | 29.684 % |
c |     71822 |  106224   309903 |   51840   30163  1277188    42.3 | 29.684 % |
c |     72328 |  106224   309903 |   57024   30669  1299966    42.4 | 29.684 % |
c |     73087 |  106224   309903 |   62727   31428  1335335    42.5 | 29.684 % |
c |     74227 |  105935   309221 |   69000   32567  1386953    42.6 | 29.829 % |
c |     75935 |  105909   309162 |   75900   34274  1463709    42.7 | 29.846 % |
c |     78498 |  105392   307961 |   83490   36834  1605370    43.6 | 30.142 % |
c ==============================================================================
c [1mFound solution: 1509[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366951   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79344 |  105394   307972 |   35131   37680  1649078    43.8 | 30.142 % |
c ==============================================================================
c [1mFound solution: 1505[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366955   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79345 |  105396   307983 |   35132   37681  1649081    43.8 | 30.142 % |
c ==============================================================================
c [1mFound solution: 1501[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366959   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79352 |  105398   307990 |   35132   37688  1649116    43.8 | 30.142 % |
c |     79454 |  105398   307990 |   38645   37790  1654149    43.8 | 30.145 % |
c ==============================================================================
c [1mFound solution: 1473[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366987   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79480 |  105404   308016 |   35134   37816  1655978    43.8 | 30.145 % |
c ==============================================================================
c [1mFound solution: 1470[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366990   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79483 |  105408   308038 |   35136   37819  1655995    43.8 | 30.145 % |
c |     79584 |  105408   308038 |   38649   37920  1659208    43.8 | 30.148 % |
c |     79738 |  105408   308038 |   42514   38074  1666745    43.8 | 30.148 % |
c |     79963 |  105408   308038 |   46766   38299  1676774    43.8 | 30.148 % |
c |     80301 |  105408   308038 |   51442   38637  1692181    43.8 | 30.148 % |
c |     80808 |  105408   308038 |   56586   39144  1717668    43.9 | 30.148 % |
c |     81569 |  105408   308038 |   62245   39905  1758508    44.1 | 30.148 % |
c ==============================================================================
c [1mFound solution: 1469[0m
c ---[   0]---> Adder-cost: 0   maxlim: 366991   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     81795 |  105410   308046 |   35136   40131  1769710    44.1 | 30.148 % |
c ==============================================================================
c [1mFound solution: 1453[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367007   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     81885 |  105412   308054 |   35137   40221  1773348    44.1 | 30.148 % |
c |     81985 |  105412   308054 |   38650   40321  1777722    44.1 | 30.150 % |
c |     82138 |  105412   308054 |   42515   40474  1787775    44.2 | 30.150 % |
c |     82363 |  105412   308054 |   46767   40699  1799618    44.2 | 30.150 % |
c |     82700 |  105412   308054 |   51444   41036  1817466    44.3 | 30.150 % |
c |     83208 |  105412   308054 |   56588   41544  1843255    44.4 | 30.150 % |
c |     83967 |  105412   308054 |   62247   42303  1878944    44.4 | 30.150 % |
c |     85106 |  105412   308054 |   68472   43442  1938299    44.6 | 30.150 % |
c ==============================================================================
c [1mFound solution: 1417[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367043   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86675 |  105336   307870 |   35112   45006  2015850    44.8 | 30.150 % |
c ==============================================================================
c [1mFound solution: 1409[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367051   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86714 |  105340   307888 |   35113   45045  2017666    44.8 | 30.150 % |
c ==============================================================================
c [1mFound solution: 1408[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367052   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86737 |  105342   307897 |   35114   45068  2018603    44.8 | 30.150 % |
c |     86838 |  105342   307897 |   38625   45169  2024179    44.8 | 30.201 % |
c |     86988 |  105342   307897 |   42487   45319  2031761    44.8 | 30.201 % |
c |     87215 |  105342   307897 |   46736   45546  2043050    44.9 | 30.201 % |
c |     87553 |  105342   307897 |   51410   45884  2059420    44.9 | 30.201 % |
c |     88061 |  105342   307897 |   56551   46392  2088256    45.0 | 30.201 % |
c |     88820 |  105342   307897 |   62206   47151  2121865    45.0 | 30.201 % |
c |     89959 |  105342   307897 |   68427   48290  2166513    44.9 | 30.201 % |
c |     91667 |  105278   307748 |   75269   49997  2267614    45.4 | 30.245 % |
c ==============================================================================
c [1mFound solution: 1395[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367065   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     92369 |  105186   307550 |   35062   50697  2303383    45.4 | 30.245 % |
c |     92469 |  105186   307550 |   38568   50797  2307700    45.4 | 30.301 % |
c |     92619 |  105186   307550 |   42425   50947  2317258    45.5 | 30.301 % |
c |     92844 |  105114   307385 |   46667   51167  2329445    45.5 | 30.345 % |
c |     93181 |  105114   307385 |   51334   51504  2347349    45.6 | 30.345 % |
c |     93687 |  105114   307385 |   56467   52010  2372171    45.6 | 30.345 % |
c ==============================================================================
c [1mFound solution: 1391[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367069   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     94421 |  105118   307405 |   35039   52744  2403147    45.6 | 30.345 % |
c |     94523 |  104545   306038 |   38542   17490   672678    38.5 | 30.681 % |
c |     94674 |  104545   306038 |   42397   17641   680392    38.6 | 30.681 % |
c |     94900 |  104545   306038 |   46636   17867   688556    38.5 | 30.681 % |
c |     95237 |  103912   304432 |   51300   18200   704418    38.7 | 31.079 % |
c |     95744 |  103436   303279 |   56430   18706   738469    39.5 | 31.412 % |
c |     96503 |  103436   303279 |   62073   19465   819656    42.1 | 31.412 % |
c ==============================================================================
c [1mFound solution: 1390[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367070   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97478 |  103315   303002 |   34438   20438   877863    43.0 | 31.412 % |
c |     97580 |  103315   303002 |   37881   20540   882339    43.0 | 31.497 % |
c |     97731 |  103303   302966 |   41669   20690   889387    43.0 | 31.504 % |
c |     97957 |  103303   302966 |   45836   20916   902460    43.1 | 31.504 % |
c |     98295 |  103303   302966 |   50420   21254   919378    43.3 | 31.504 % |
c |     98804 |  103303   302966 |   55462   21763   958036    44.0 | 31.504 % |
c |     99563 |  103269   302887 |   61009   22521  1012142    44.9 | 31.523 % |
c |    100702 |  103269   302887 |   67109   23660  1093286    46.2 | 31.523 % |
c |    102410 |  103252   302851 |   73820   25367  1179336    46.5 | 31.534 % |
c |    104976 |  103234   302811 |   81203   27931  1288961    46.1 | 31.559 % |
c ==============================================================================
c [1mFound solution: 1389[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367071   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108649 |  101545   298775 |   33848   31588  1438970    45.6 | 31.559 % |
c |    108749 |  101545   298775 |   37232   31688  1442786    45.5 | 32.623 % |
c |    108900 |  101545   298775 |   40956   31839  1446757    45.4 | 32.623 % |
c ==============================================================================
c [1mFound solution: 1326[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367134   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108957 |  101556   298826 |   33852   31896  1448483    45.4 | 32.623 % |
c ==============================================================================
c [1mFound solution: 1325[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367135   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108982 |  101558   298834 |   33852   31921  1448883    45.4 | 32.623 % |
c ==============================================================================
c [1mFound solution: 1317[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367143   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    109037 |  101560   298842 |   33853   31976  1451744    45.4 | 32.623 % |
c ==============================================================================
c [1mFound solution: 1309[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367151   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    109078 |  101562   298850 |   33854   32017  1453073    45.4 | 32.623 % |
c ==============================================================================
c [1mFound solution: 1301[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367159   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    109082 |  101564   298859 |   33854   32021  1453143    45.4 | 32.623 % |
c |    109187 |  101564   298859 |   37239   32126  1456767    45.3 | 32.630 % |
c ==============================================================================
c [1mFound solution: 1293[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367167   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    109216 |  101565   298862 |   33855   32155  1457269    45.3 | 32.630 % |
c ==============================================================================
c [1mFound solution: 1285[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367175   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    109216 |  101567   298870 |   33855   32155  1457269    45.3 | 32.630 % |
c ==============================================================================
c [1mFound solution: 1284[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367176   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    109217 |  101569   298884 |   33856   32156  1457273    45.3 | 32.630 % |
c ==============================================================================
c [1mFound solution: 1283[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367177   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    109217 |  101571   298896 |   33857   32156  1457273    45.3 | 32.630 % |
c ==============================================================================
c [1mFound solution: 1280[0m
c ---[   0]---> Adder-cost: 0   maxlim: 367180   bits: 19/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    109218 |  101575   298912 |   33858   32157  1457286    45.3 | 32.630 % |
c |    109318 |  101575   298912 |   37243   32257  1461887    45.3 | 32.635 % |
c |    109470 |  101575   298912 |   40968   32409  1470826    45.4 | 32.635 % |
c |    109695 |  101528   298804 |   45064   32632  1480689    45.4 | 32.664 % |
c |    110037 |  101528   298804 |   49571   32974  1497819    45.4 | 32.664 % |
c |    110544 |  101528   298804 |   54528   33481  1521269    45.4 | 32.664 % |
c |    111303 |  101528   298804 |   59981   34240  1567366    45.8 | 32.664 % |
c |    112443 |  101528   298804 |   65979   35380  1629710    46.1 | 32.664 % |
c |    114151 |  101528   298804 |   72577   37088  1705968    46.0 | 32.664 % |
c |    116720 |  101480   298694 |   79835   39656  1808149    45.6 | 32.692 % |
c |    120568 |  101480   298694 |   87818   43504  1984343    45.6 | 32.692 % |
c |    126335 |  101301   298273 |   96600   49207  2301465    46.8 | 32.787 % |
c |    134984 |  101093   297787 |  106260   57850  2830264    48.9 | 32.910 % |
c |    147961 |  101037   297656 |  116886   70824  3432680    48.5 | 32.945 % |
c |    167423 |  100243   295747 |  128575   90263  4400555    48.8 | 33.449 % |
c |    196617 |   99832   294793 |  141433  119441  5808019    48.6 | 33.708 % |
c |    240408 |   98780   292194 |  155576   24648   829251    33.6 | 34.370 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 26371 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.97 0.96 2/54 26367
Raw data (stat): 26367 (runsolver) R 26366 4613 4612 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 843003217 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20 s]
Raw data (loadavg): 0.94 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0009 s]
Raw data (loadavg): 0.95 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0005 s]
Raw data (loadavg): 0.95 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0012 s]
Raw data (loadavg): 0.96 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0009 s]
Raw data (loadavg): 0.97 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0006 s]
Raw data (loadavg): 0.97 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0013 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0013 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.001 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 26371
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.004 s]
Raw data (loadavg): 1.07 0.99 0.96 2/55 26424
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.003 s]
Raw data (loadavg): 1.14 1.00 0.97 2/55 26424
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.004 s]
Raw data (loadavg): 1.12 1.00 0.97 2/55 26424
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.005 s]
Raw data (loadavg): 1.10 1.00 0.97 2/55 26424
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.01 s]
Raw data (loadavg): 1.08 1.00 0.97 2/55 26424
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.01 s]
Raw data (loadavg): 1.07 1.00 0.97 2/55 26424
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.01 s]
Raw data (loadavg): 1.06 1.00 0.97 2/55 26424
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.011 s]
Raw data (loadavg): 1.05 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.01 s]
Raw data (loadavg): 1.04 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.011 s]
Raw data (loadavg): 1.04 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.012 s]
Raw data (loadavg): 1.03 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.011 s]
Raw data (loadavg): 1.02 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.011 s]
Raw data (loadavg): 1.02 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.012 s]
Raw data (loadavg): 1.02 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.012 s]
Raw data (loadavg): 1.01 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.013 s]
Raw data (loadavg): 1.01 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.013 s]
Raw data (loadavg): 1.01 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.013 s]
Raw data (loadavg): 1.01 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.013 s]
Raw data (loadavg): 1.01 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.014 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.015 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.015 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.015 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.016 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.016 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26426
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.021 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.021 s]
Raw data (loadavg): 1.07 1.02 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.021 s]
Raw data (loadavg): 1.06 1.02 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.021 s]
Raw data (loadavg): 1.05 1.01 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.022 s]
Raw data (loadavg): 1.04 1.01 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.022 s]
Raw data (loadavg): 1.04 1.01 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.023 s]
Raw data (loadavg): 1.03 1.01 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.023 s]
Raw data (loadavg): 1.02 1.01 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.024 s]
Raw data (loadavg): 1.02 1.01 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.023 s]
Raw data (loadavg): 1.02 1.01 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.024 s]
Raw data (loadavg): 1.01 1.01 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.025 s]
Raw data (loadavg): 1.01 1.01 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.03 s]
Raw data (loadavg): 1.01 1.01 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.031 s]
Raw data (loadavg): 1.01 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.032 s]
Raw data (loadavg): 1.01 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.032 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.032 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.032 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.034 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.034 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.034 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.035 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.042 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.042 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.042 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.044 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.044 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.044 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.045 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.045 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.046 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.046 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.046 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.046 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.045 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.05 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 1.00 1.00 0.97 1/53 26428
Raw data (stat): 26367 (minisat+_script) S 26366 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 843003217 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

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