PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos11.opb
MD5SUM	61549d48f99a5af6fe87bd8bf474bfaf
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	9216
Optimality of the best value was proved	NO
Number of terms in the objective function	5400
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	193273528140
Number of bits of the sum of numbers in the objective function	38
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	193273528140
Number of bits of the biggest sum of numbers	38
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1202.33
Number of variables	8600
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	450
Trace number 30911

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        646576 kB
Buffers:         15516 kB
Cached:         351608 kB
SwapCached:        416 kB
Active:          21224 kB
Inactive:       348168 kB
HighTotal:      131008 kB
HighFree:        55608 kB
LowTotal:       903652 kB
LowFree:        590968 kB
SwapTotal:     2097136 kB
SwapFree:      2096040 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5948 kB
Slab:            13000 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 21:05:07 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 22302 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:   10
c ---[3040]---> BDD-cost:   10
c ---[3039]---> BDD-cost:   10
c ---[3038]---> BDD-cost:   10
c ---[3037]---> BDD-cost:   10
c ---[3036]---> BDD-cost:   10
c ---[3035]---> BDD-cost:   10
c ---[3034]---> BDD-cost:   10
c ---[3033]---> BDD-cost:   10
c ---[3032]---> BDD-cost:   10
c ---[3031]---> BDD-cost:   10
c ---[3030]---> BDD-cost:   10
c ---[3029]---> BDD-cost:   10
c ---[3028]---> BDD-cost:   10
c ---[3027]---> BDD-cost:   10
c ---[3026]---> BDD-cost:   10
c ---[3025]---> BDD-cost:   10
c ---[3024]---> BDD-cost:   10
c ---[3023]---> BDD-cost:   10
c ---[3022]---> BDD-cost:   10
c ---[3021]---> BDD-cost:   10
c ---[3020]---> BDD-cost:   10
c ---[3019]---> BDD-cost:   10
c ---[3018]---> BDD-cost:   10
c ---[3017]---> BDD-cost:   10
c ---[3016]---> BDD-cost:   10
c ---[3015]---> BDD-cost:   10
c ---[3014]---> BDD-cost:   10
c ---[3013]---> BDD-cost:   10
c ---[3012]---> BDD-cost:   10
c ---[3011]---> BDD-cost:   10
c ---[3010]---> BDD-cost:   10
c ---[3009]---> BDD-cost:   10
c ---[3008]---> BDD-cost:   10
c ---[3007]---> BDD-cost:   10
c ---[3006]---> BDD-cost:   10
c ---[3005]---> BDD-cost:   10
c ---[3004]---> BDD-cost:   10
c ---[3003]---> BDD-cost:   10
c ---[3002]---> BDD-cost:   10
c ---[3001]---> BDD-cost:   10
c ---[3000]---> BDD-cost:   10
c ---[2999]---> BDD-cost:   10
c ---[2998]---> BDD-cost:   10
c ---[2997]---> BDD-cost:   10
c ---[2996]---> BDD-cost:   10
c ---[2995]---> BDD-cost:   10
c ---[2994]---> BDD-cost:   10
c ---[2993]---> BDD-cost:   10
c ---[2992]---> BDD-cost:   10
c ---[2991]---> BDD-cost:   10
c ---[2990]---> BDD-cost:   10
c ---[2989]---> BDD-cost:   10
c ---[2988]---> BDD-cost:   10
c ---[2987]---> BDD-cost:   10
c ---[2986]---> BDD-cost:   10
c ---[2985]---> BDD-cost:   10
c ---[2984]---> BDD-cost:   10
c ---[2983]---> BDD-cost:   10
c ---[2982]---> BDD-cost:   10
c ---[2981]---> BDD-cost:   10
c ---[2980]---> BDD-cost:   10
c ---[2979]---> BDD-cost:   10
c ---[2978]---> BDD-cost:   10
c ---[2977]---> BDD-cost:   10
c ---[2976]---> BDD-cost:   10
c ---[2975]---> BDD-cost:   10
c ---[2974]---> BDD-cost:   10
c ---[2973]---> BDD-cost:   10
c ---[2972]---> BDD-cost:   10
c ---[2971]---> BDD-cost:   10
c ---[2970]---> BDD-cost:   10
c ---[2969]---> BDD-cost:   10
c ---[2968]---> BDD-cost:   10
c ---[2967]---> BDD-cost:   10
c ---[2966]---> BDD-cost:   10
c ---[2965]---> BDD-cost:   10
c ---[2964]---> BDD-cost:   10
c ---[2963]---> BDD-cost:   10
c ---[2962]---> BDD-cost:   10
c ---[2961]---> BDD-cost:   10
c ---[2960]---> BDD-cost:   10
c ---[2959]---> BDD-cost:   10
c ---[2958]---> BDD-cost:   10
c ---[2957]---> BDD-cost:   10
c ---[2956]---> BDD-cost:   10
c ---[2955]---> BDD-cost:   10
c ---[2954]---> BDD-cost:   10
c ---[2953]---> BDD-cost:   10
c ---[2952]---> BDD-cost:   10
c ---[2951]---> BDD-cost:   10
c ---[2950]---> BDD-cost:   10
c ---[2949]---> BDD-cost:   10
c ---[2948]---> BDD-cost:   10
c ---[2947]---> BDD-cost:   10
c ---[2946]---> BDD-cost:   10
c ---[2945]---> BDD-cost:   10
c ---[2944]---> BDD-cost:   10
c ---[2943]---> BDD-cost:   10
c ---[2942]---> BDD-cost:   10
c ---[2940]---> BDD-cost:   50
c ---[2938]---> BDD-cost:   50
c ---[2936]---> BDD-cost:   50
c ---[2934]---> BDD-cost:   50
c ---[2932]---> BDD-cost:   50
c ---[2930]---> BDD-cost:   50
c ---[2928]---> BDD-cost:   50
c ---[2926]---> BDD-cost:   50
c ---[2924]---> BDD-cost:   50
c ---[2922]---> BDD-cost:   50
c ---[2920]---> BDD-cost:   50
c ---[2918]---> BDD-cost:   50
c ---[2916]---> BDD-cost:   50
c ---[2914]---> BDD-cost:   50
c ---[2912]---> BDD-cost:   50
c ---[2910]---> BDD-cost:   50
c ---[2908]---> BDD-cost:   50
c ---[2906]---> BDD-cost:   50
c ---[2904]---> BDD-cost:   50
c ---[2902]---> BDD-cost:   50
c ---[2900]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2898]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2896]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2894]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2892]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2890]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2888]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2886]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2884]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2882]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2881]---> BDD-cost:   31
c ---[2880]---> BDD-cost:   31
c ---[2879]---> BDD-cost:   31
c ---[2878]---> BDD-cost:   31
c ---[2877]---> BDD-cost:   31
c ---[2876]---> BDD-cost:   31
c ---[2875]---> BDD-cost:   31
c ---[2874]---> BDD-cost:   31
c ---[2873]---> BDD-cost:   31
c ---[2872]---> BDD-cost:   31
c ---[2871]---> BDD-cost:   31
c ---[2870]---> BDD-cost:   31
c ---[2869]---> BDD-cost:   31
c ---[2868]---> BDD-cost:   31
c ---[2867]---> BDD-cost:   31
c ---[2866]---> BDD-cost:   31
c ---[2865]---> BDD-cost:   31
c ---[2864]---> BDD-cost:   31
c ---[2863]---> BDD-cost:   31
c ---[2862]---> BDD-cost:   31
c ---[2861]---> BDD-cost:   31
c ---[2860]---> BDD-cost:   31
c ---[2859]---> BDD-cost:   31
c ---[2858]---> BDD-cost:   31
c ---[2857]---> BDD-cost:   31
c ---[2856]---> BDD-cost:   31
c ---[2855]---> BDD-cost:   31
c ---[2854]---> BDD-cost:   31
c ---[2853]---> BDD-cost:   31
c ---[2852]---> BDD-cost:   31
c ---[2851]---> BDD-cost:   31
c ---[2850]---> BDD-cost:   31
c ---[2849]---> BDD-cost:   31
c ---[2848]---> BDD-cost:   31
c ---[2847]---> BDD-cost:   31
c ---[2846]---> BDD-cost:   31
c ---[2845]---> BDD-cost:   31
c ---[2844]---> BDD-cost:   31
c ---[2843]---> BDD-cost:   31
c ---[2842]---> BDD-cost:   31
c ---[2841]---> BDD-cost:   31
c ---[2840]---> BDD-cost:   31
c ---[2839]---> BDD-cost:   31
c ---[2838]---> BDD-cost:   31
c ---[2837]---> BDD-cost:   31
c ---[2836]---> BDD-cost:   31
c ---[2835]---> BDD-cost:   31
c ---[2834]---> BDD-cost:   31
c ---[2833]---> BDD-cost:   31
c ---[2832]---> BDD-cost:   31
c ---[2831]---> BDD-cost:   31
c ---[2830]---> BDD-cost:   31
c ---[2829]---> BDD-cost:   31
c ---[2828]---> BDD-cost:   31
c ---[2827]---> BDD-cost:   31
c ---[2826]---> BDD-cost:   31
c ---[2825]---> BDD-cost:   31
c ---[2824]---> BDD-cost:   31
c ---[2823]---> BDD-cost:   31
c ---[2822]---> BDD-cost:   31
c ---[2821]---> BDD-cost:   31
c ---[2820]---> BDD-cost:   31
c ---[2819]---> BDD-cost:   31
c ---[2818]---> BDD-cost:   31
c ---[2817]---> BDD-cost:   31
c ---[2816]---> BDD-cost:   31
c ---[2815]---> BDD-cost:   31
c ---[2814]---> BDD-cost:   31
c ---[2813]---> BDD-cost:   31
c ---[2812]---> BDD-cost:   31
c ---[2811]---> BDD-cost:   31
c ---[2810]---> BDD-cost:   31
c ---[2809]---> BDD-cost:   31
c ---[2808]---> BDD-cost:   31
c ---[2807]---> BDD-cost:   31
c ---[2806]---> BDD-cost:   31
c ---[2805]---> BDD-cost:   31
c ---[2804]---> BDD-cost:   31
c ---[2803]---> BDD-cost:   31
c ---[2802]---> BDD-cost:   31
c ---[2801]---> BDD-cost:   31
c ---[2800]---> BDD-cost:   31
c ---[2799]---> BDD-cost:   31
c ---[2798]---> BDD-cost:   31
c ---[2797]---> BDD-cost:   31
c ---[2796]---> BDD-cost:   31
c ---[2795]---> BDD-cost:   31
c ---[2794]---> BDD-cost:   31
c ---[2793]---> BDD-cost:   31
c ---[2792]---> BDD-cost:   31
c ---[2791]---> BDD-cost:   31
c ---[2790]---> BDD-cost:   31
c ---[2789]---> BDD-cost:   31
c ---[2788]---> BDD-cost:   31
c ---[2787]---> BDD-cost:   31
c ---[2786]---> BDD-cost:   31
c ---[2785]---> BDD-cost:   31
c ---[2784]---> BDD-cost:   31
c ---[2783]---> BDD-cost:   31
c ---[2782]---> BDD-cost:   31
c ---[2781]---> BDD-cost:   31
c ---[2780]---> BDD-cost:   31
c ---[2779]---> BDD-cost:   31
c ---[2778]---> BDD-cost:   31
c ---[2777]---> BDD-cost:   31
c ---[2776]---> BDD-cost:   31
c ---[2775]---> BDD-cost:   31
c ---[2774]---> BDD-cost:   31
c ---[2773]---> BDD-cost:   31
c ---[2772]---> BDD-cost:   31
c ---[2771]---> BDD-cost:   31
c ---[2770]---> BDD-cost:   31
c ---[2769]---> BDD-cost:   31
c ---[2768]---> BDD-cost:   31
c ---[2767]---> BDD-cost:   31
c ---[2766]---> BDD-cost:   31
c ---[2765]---> BDD-cost:   31
c ---[2764]---> BDD-cost:   31
c ---[2763]---> BDD-cost:   31
c ---[2762]---> BDD-cost:   31
c ---[2761]---> BDD-cost:   31
c ---[2760]---> BDD-cost:   31
c ---[2759]---> BDD-cost:   31
c ---[2758]---> BDD-cost:   31
c ---[2757]---> BDD-cost:   31
c ---[2756]---> BDD-cost:   31
c ---[2755]---> BDD-cost:   31
c ---[2754]---> BDD-cost:   31
c ---[2753]---> BDD-cost:   31
c ---[2752]---> BDD-cost:   31
c ---[2751]---> BDD-cost:   31
c ---[2750]---> BDD-cost:   31
c ---[2749]---> BDD-cost:   31
c ---[2748]---> BDD-cost:   31
c ---[2747]---> BDD-cost:   31
c ---[2746]---> BDD-cost:   31
c ---[2745]---> BDD-cost:   31
c ---[2744]---> BDD-cost:   31
c ---[2743]---> BDD-cost:   31
c ---[2742]---> BDD-cost:   31
c ---[2741]---> BDD-cost:   31
c ---[2740]---> BDD-cost:   31
c ---[2739]---> BDD-cost:   31
c ---[2738]---> BDD-cost:   31
c ---[2737]---> BDD-cost:   31
c ---[2736]---> BDD-cost:   31
c ---[2735]---> BDD-cost:   31
c ---[2734]---> BDD-cost:   31
c ---[2733]---> BDD-cost:   31
c ---[2732]---> BDD-cost:   31
c ---[2731]---> BDD-cost:   31
c ---[2730]---> BDD-cost:   31
c ---[2729]---> BDD-cost:   31
c ---[2728]---> BDD-cost:   31
c ---[2727]---> BDD-cost:   31
c ---[2726]---> BDD-cost:   31
c ---[2725]---> BDD-cost:   31
c ---[2724]---> BDD-cost:   31
c ---[2723]---> BDD-cost:   31
c ---[2722]---> BDD-cost:   31
c ---[2721]---> BDD-cost:   31
c ---[2720]---> BDD-cost:   31
c ---[2719]---> BDD-cost:   31
c ---[2718]---> BDD-cost:   31
c ---[2717]---> BDD-cost:   31
c ---[2716]---> BDD-cost:   31
c ---[2715]---> BDD-cost:   31
c ---[2714]---> BDD-cost:   31
c ---[2713]---> BDD-cost:   31
c ---[2712]---> BDD-cost:   31
c ---[2711]---> BDD-cost:   31
c ---[2710]---> BDD-cost:   31
c ---[2709]---> BDD-cost:   31
c ---[2708]---> BDD-cost:   31
c ---[2707]---> BDD-cost:   31
c ---[2706]---> BDD-cost:   31
c ---[2705]---> BDD-cost:   31
c ---[2704]---> BDD-cost:   31
c ---[2703]---> BDD-cost:   31
c ---[2702]---> BDD-cost:   31
c ---[2701]---> BDD-cost:   31
c ---[2700]---> BDD-cost:   31
c ---[2699]---> BDD-cost:   31
c ---[2698]---> BDD-cost:   31
c ---[2697]---> BDD-cost:   31
c ---[2696]---> BDD-cost:   31
c ---[2695]---> BDD-cost:   31
c ---[2694]---> BDD-cost:   31
c ---[2693]---> BDD-cost:   31
c ---[2692]---> BDD-cost:   31
c ---[2691]---> BDD-cost:   31
c ---[2690]---> BDD-cost:   31
c ---[2689]---> BDD-cost:   31
c ---[2688]---> BDD-cost:   31
c ---[2687]---> BDD-cost:   31
c ---[2686]---> BDD-cost:   31
c ---[2685]---> BDD-cost:   31
c ---[2684]---> BDD-cost:   31
c ---[2683]---> BDD-cost:   31
c ---[2682]---> BDD-cost:   31
c ---[2680]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2678]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2676]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2674]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2672]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2670]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2668]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2666]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2664]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2662]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2660]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2658]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2656]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2654]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2652]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2650]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2648]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2646]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2644]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2642]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2640]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2638]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2636]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2634]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2632]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2
c ---[2631]---> BDD-cost:   38
c ---[2630]---> BDD-cost:   38
c ---[2629]---> BDD-cost:   38
c ---[2628]---> BDD-cost:   38
c ---[2627]---> BDD-cost:  114
c ---[2626]---> BDD-cost:  108
c ---[2625]---> BDD-cost:  108
c ---[2624]---> BDD-cost:  108
c ---[2623]---> BDD-cost:  114
c ---[2622]---> BDD-cost:  106
c ---[2621]---> BDD-cost:  108
c ---[2620]---> BDD-cost:  108
c ---[2619]---> BDD-cost:  114
c ---[2618]---> BDD-cost:  106
c ---[2617]---> BDD-cost:  106
c ---[2616]---> BDD-cost:  108
c ---[2615]---> BDD-cost:  114
c ---[2614]---> BDD-cost:  106
c ---[2613]---> BDD-cost:  106
c ---[2612]---> BDD-cost:  106
c ---[2611]---> BDD-cost:   38
c ---[2610]---> BDD-cost:   38
c ---[2609]---> BDD-cost:   38
c ---[2608]---> BDD-cost:   38
c ---[2607]---> BDD-cost:  115
c ---[2606]---> BDD-cost:  108
c ---[2605]---> BDD-cost:  108
c ---[2604]---> BDD-cost:  108
c ---[2603]---> BDD-cost:  114
c ---[2602]---> BDD-cost:  108
c ---[2601]---> BDD-cost:  108
c ---[2600]---> BDD-cost:  108
c ---[2599]---> BDD-cost:  114
c ---[2598]---> BDD-cost:  108
c ---[2597]---> BDD-cost:  106
c ---[2596]---> BDD-cost:  108
c ---[2595]---> BDD-cost:  114
c ---[2594]---> BDD-cost:  108
c ---[2593]---> BDD-cost:  106
c ---[2592]---> BDD-cost:  106
c ---[2591]---> BDD-cost:   38
c ---[2590]---> BDD-cost:   38
c ---[2589]---> BDD-cost:   38
c ---[2588]---> BDD-cost:   38
c ---[2587]---> BDD-cost:  115
c ---[2586]---> BDD-cost:  108
c ---[2585]---> BDD-cost:  108
c ---[2584]---> BDD-cost:  108
c ---[2583]---> BDD-cost:  115
c ---[2582]---> BDD-cost:  108
c ---[2581]---> BDD-cost:  108
c ---[2580]---> BDD-cost:  108
c ---[2579]---> BDD-cost:  114
c ---[2578]---> BDD-cost:  108
c ---[2577]---> BDD-cost:  108
c ---[2576]---> BDD-cost:  108
c ---[2575]---> BDD-cost:  114
c ---[2574]---> BDD-cost:  108
c ---[2573]---> BDD-cost:  108
c ---[2572]---> BDD-cost:  106
c ---[2571]---> BDD-cost:   38
c ---[2570]---> BDD-cost:   38
c ---[2569]---> BDD-cost:   38
c ---[2568]---> BDD-cost:   38
c ---[2567]---> BDD-cost:  115
c ---[2566]---> BDD-cost:  108
c ---[2565]---> BDD-cost:  108
c ---[2564]---> BDD-cost:  108
c ---[2563]---> BDD-cost:  115
c ---[2562]---> BDD-cost:  108
c ---[2561]---> BDD-cost:  108
c ---[2560]---> BDD-cost:  108
c ---[2559]---> BDD-cost:  115
c ---[2558]---> BDD-cost:  108
c ---[2557]---> BDD-cost:  108
c ---[2556]---> BDD-cost:  108
c ---[2555]---> BDD-cost:  114
c ---[2554]---> BDD-cost:  108
c ---[2553]---> BDD-cost:  108
c ---[2552]---> BDD-cost:  108
c ---[2551]---> BDD-cost:   38
c ---[2550]---> BDD-cost:   38
c ---[2549]---> BDD-cost:   38
c ---[2548]---> BDD-cost:   38
c ---[2547]---> BDD-cost:  115
c ---[2546]---> BDD-cost:  108
c ---[2545]---> BDD-cost:  108
c ---[2544]---> BDD-cost:  108
c ---[2543]---> BDD-cost:  115
c ---[2542]---> BDD-cost:  108
c ---[2541]---> BDD-cost:  108
c ---[2540]---> BDD-cost:  108
c ---[2539]---> BDD-cost:  115
c ---[2538]---> BDD-cost:  108
c ---[2537]---> BDD-cost:  108
c ---[2536]---> BDD-cost:  108
c ---[2535]---> BDD-cost:  115
c ---[2534]---> BDD-cost:  108
c ---[2533]---> BDD-cost:  108
c ---[2532]---> BDD-cost:  108
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: 364   maxlim: 117745   bits: 17/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  131409   344010 |   43803       0        0     nan |  0.000 % |
c |       100 |  131357   343892 |   48183      96      809     8.4 |  6.574 % |
c |       251 |  130254   341355 |   53001     229     5502    24.0 |  7.142 % |
c |       476 |  130238   341303 |   58301     452     7764    17.2 |  7.147 % |
c |       814 |  130132   341010 |   64131     782    20100    25.7 |  7.194 % |
c ==============================================================================
c [1mFound solution: 83899392[0m
c ---[   0]---> Adder-cost: 9666   maxlim: 24075291468   bits: 35/35
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1230 |  197703   582637 |   65901    1198    33631    28.1 |  7.194 % |
c |      1330 |  197552   582164 |   72491    1275    34494    27.1 |  7.054 % |
c |      1481 |  197526   582074 |   79740    1424    37351    26.2 |  7.061 % |
c |      1706 |  196999   580827 |   87714    1640    42327    25.8 |  7.309 % |
c |      2043 |  196598   579389 |   96485    1923    46927    24.4 |  7.407 % |
c |      2549 |  196598   579389 |  106134    2429    49793    20.5 |  7.407 % |
c |      3309 |  196544   579191 |  116747    3183    68422    21.5 |  7.420 % |
c |      4449 |  195979   577839 |  128422    4309    94010    21.8 |  7.667 % |
c |      6157 |  195549   576784 |  141264    5991   132861    22.2 |  7.839 % |
c |      8719 |  192770   570162 |  155391    8494   170145    20.0 |  9.094 % |
c |     12563 |  191206   566136 |  170930   12277   277841    22.6 |  9.645 % |
c ==============================================================================
c [1mFound solution: 43876397[0m
c ---[   0]---> Adder-cost: 154   maxlim: 12035718943   bits: 34/34
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16966 |  186316   553064 |   62105   16537   387141    23.4 |  9.645 % |
c |     17070 |  185899   552104 |   68315   16638   389272    23.4 | 12.036 % |
c |     17220 |  185691   551602 |   75147   16768   391399    23.3 | 12.126 % |
c |     17445 |  185691   551602 |   82661   16993   395977    23.3 | 12.126 % |
c |     17782 |  185427   550887 |   90927   17305   403619    23.3 | 12.220 % |
c ==============================================================================
c [1mFound solution: 43712829[0m
c ---[   0]---> Adder-cost: 0   maxlim: 12035882511   bits: 34/34
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18135 |  185324   550617 |   61774   17640   405212    23.0 | 12.220 % |
c |     18235 |  185182   550295 |   67951   17729   405648    22.9 | 12.323 % |
c |     18387 |  185094   550097 |   74746   17874   408410    22.8 | 12.361 % |
c |     18612 |  185062   549989 |   82221   18096   412645    22.8 | 12.368 % |
c |     18949 |  184852   549509 |   90443   18422   419103    22.8 | 12.453 % |
c |     19457 |  184059   547387 |   99487   18827   429100    22.8 | 12.762 % |
c ==============================================================================
c [1mFound solution: 31016429[0m
c ---[   0]---> Adder-cost: 154   maxlim: 6008781151   bits: 33/33
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19760 |  182460   541867 |   60820   19090   434558    22.8 | 12.762 % |
c |     19860 |  182353   541494 |   66902   19178   436363    22.8 | 13.569 % |
c |     20013 |  182309   541331 |   73592   19329   443369    22.9 | 13.569 % |
c |     20238 |  182165   540851 |   80951   19534   445989    22.8 | 13.609 % |
c ==============================================================================
c [1mFound solution: 29176589[0m
c ---[   0]---> Adder-cost: 0   maxlim: 6010620991   bits: 33/33
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20517 |  182063   540561 |   60687   19801   449544    22.7 | 13.609 % |
c |     20618 |  181815   539996 |   66755   19880   452965    22.8 | 13.748 % |
c |     20769 |  181674   539669 |   73431   20024   456644    22.8 | 13.809 % |
c |     20998 |  181674   539669 |   80774   20253   461870    22.8 | 13.809 % |
c ==============================================================================
c [1mFound solution: 29176205[0m
c ---[   0]---> Adder-cost: 0   maxlim: 6010621375   bits: 33/33
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21326 |  181677   539726 |   60559   20198   457954    22.7 | 13.809 % |
c |     21426 |  181637   539634 |   66614   20296   458396    22.6 | 13.831 % |
c |     21576 |  181261   538384 |   73276   20400   463184    22.7 | 13.935 % |
c |     21802 |  180888   537345 |   80604   20591   471310    22.9 | 14.063 % |
c ==============================================================================
c [1mFound solution: 27079069[0m
c ---[   0]---> Adder-cost: 0   maxlim: 6012718511   bits: 33/33
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21982 |  180757   537161 |   60252   20702   473653    22.9 | 14.063 % |
c |     22083 |  180579   536736 |   66277   20795   475731    22.9 | 14.209 % |
c |     22233 |  180579   536736 |   72904   20945   477431    22.8 | 14.209 % |
c |     22461 |  180508   536532 |   80195   21163   480993    22.7 | 14.235 % |
c ==============================================================================
c [1mFound solution: 27071037[0m
c ---[   0]---> Adder-cost: 0   maxlim: 6012726543   bits: 33/33
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22560 |  180517   536624 |   60172   21262   481484    22.6 | 14.235 % |
c ==============================================================================
c [1mFound solution: 18690093[0m
c ---[   0]---> Adder-cost: 0   maxlim: 6021107487   bits: 33/33
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22633 |  180538   536747 |   60179   21335   482273    22.6 | 14.235 % |
c |     22733 |  180538   536747 |   66196   21435   483852    22.6 | 14.252 % |
c |     22883 |  180538   536747 |   72816   21585   488787    22.6 | 14.252 % |
c |     23116 |  180025   535533 |   80098   21781   491651    22.6 | 14.462 % |
c ==============================================================================
c [1mFound solution: 14512685[0m
c ---[   0]---> Adder-cost: 154   maxlim: 3005386015   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23167 |  178637   530648 |   59545   21760   492221    22.6 | 14.462 % |
c ==============================================================================
c [1mFound solution: 14512669[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3005386031   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23174 |  178639   530675 |   59546   21767   492244    22.6 | 14.462 % |
c |     23274 |  178603   530543 |   65500   21863   492688    22.5 | 15.188 % |
c |     23424 |  178379   529747 |   72050   21980   494210    22.5 | 15.229 % |
c |     23649 |  177986   528363 |   79255   22112   500384    22.6 | 15.326 % |
c ==============================================================================
c [1mFound solution: 12399165[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3007499535   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23810 |  177371   525883 |   59123   22161   500889    22.6 | 15.326 % |
c |     23911 |  177193   525471 |   65035   22254   503956    22.6 | 15.549 % |
c |     24061 |  176156   523074 |   71538   22345   506641    22.7 | 16.008 % |
c |     24286 |  176156   523074 |   78692   22570   511731    22.7 | 16.008 % |
c ==============================================================================
c [1mFound solution: 12398653[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3007500047   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24383 |  176162   523129 |   58720   22667   514221    22.7 | 16.008 % |
c |     24483 |  176061   522780 |   64592   22748   516573    22.7 | 16.033 % |
c ==============================================================================
c [1mFound solution: 10301933[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009596767   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24631 |  175896   522297 |   58632   22872   518065    22.7 | 16.033 % |
c |     24731 |  175783   522041 |   64495   22965   521225    22.7 | 16.145 % |
c ==============================================================================
c [1mFound solution: 10301837[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009596863   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24787 |  175787   522070 |   58595   23021   521554    22.7 | 16.145 % |
c |     24887 |  175740   521961 |   64454   23099   522677    22.6 | 16.168 % |
c |     25037 |  175740   521961 |   70899   23249   526920    22.7 | 16.168 % |
c ==============================================================================
c [1mFound solution: 10301453[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009597247   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25108 |  175746   521997 |   58582   23320   527969    22.6 | 16.168 % |
c ==============================================================================
c [1mFound solution: 10301389[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009597311   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25159 |  175747   522015 |   58582   23371   528212    22.6 | 16.168 % |
c |     25259 |  175598   521646 |   64440   23460   529029    22.6 | 16.237 % |
c |     25410 |  175350   521072 |   70884   23573   531436    22.5 | 16.356 % |
c ==============================================================================
c [1mFound solution: 10301341[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009597359   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25467 |  174955   520192 |   58318   23592   531214    22.5 | 16.356 % |
c ==============================================================================
c [1mFound solution: 10301325[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009597375   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25480 |  174957   520213 |   58319   23605   531266    22.5 | 16.356 % |
c ==============================================================================
c [1mFound solution: 10301261[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009597439   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25494 |  174949   520197 |   58316   23618   531316    22.5 | 16.356 % |
c |     25594 |  174514   519174 |   64147   23699   532286    22.5 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10236317[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009662383   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25627 |  174531   519311 |   58177   23732   532900    22.5 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10236301[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009662399   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25661 |  174533   519331 |   58177   23766   533032    22.4 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10236237[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009662463   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25666 |  174535   519348 |   58178   23771   533057    22.4 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10235821[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009662879   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25670 |  174541   519405 |   58180   23775   533076    22.4 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10235789[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009662911   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25671 |  174543   519425 |   58181   23776   533084    22.4 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10235725[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009662975   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25733 |  174458   519245 |   58152   23832   533800    22.4 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10228109[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009670591   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25734 |  174470   519347 |   58156   23833   533804    22.4 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10228077[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009670623   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25740 |  174471   519367 |   58157   23839   533824    22.4 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10227629[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009671071   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25741 |  174479   519441 |   58159   23840   533832    22.4 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10227597[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009671103   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25742 |  174481   519461 |   58160   23841   533835    22.4 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10227533[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009671167   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25783 |  174448   519394 |   58149   23872   534081    22.4 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10224145[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009674555   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25812 |  174462   519534 |   58154   23901   534203    22.4 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10224141[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009674559   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25844 |  174464   519553 |   58154   23933   534381    22.3 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10224077[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009674623   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25885 |  174388   519395 |   58129   23964   534973    22.3 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10224013[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009674687   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25905 |  174390   519415 |   58130   23984   535097    22.3 | 16.726 % |
c ==============================================================================
c [1mFound solution: 10223949[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3009674751   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25933 |  174392   519429 |   58130   24012   535255    22.3 | 16.726 % |
c ==============================================================================
c [1mFound solution: 9778701[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010119999   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25974 |  174404   519517 |   58134   24053   535468    22.3 | 16.726 % |
c |     26076 |  174404   519517 |   63947   24155   537949    22.3 | 16.864 % |
c ==============================================================================
c [1mFound solution: 9777677[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010121023   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26182 |  174376   519440 |   58125   24255   538781    22.2 | 16.864 % |
c |     26282 |  173869   518280 |   63937   24321   541521    22.3 | 17.104 % |
c |     26432 |  169794   508736 |   70331   24402   545988    22.4 | 18.871 % |
c ==============================================================================
c [1mFound solution: 9253389[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010645311   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26538 |  169790   508741 |   56596   24506   547185    22.3 | 18.871 % |
c ==============================================================================
c [1mFound solution: 9253325[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010645375   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26566 |  169719   508497 |   56573   24515   547300    22.3 | 18.871 % |
c ==============================================================================
c [1mFound solution: 9253261[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010645439   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26578 |  169721   508510 |   56573   24527   547469    22.3 | 18.871 % |
c ==============================================================================
c [1mFound solution: 9253197[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010645503   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26599 |  169538   508101 |   56512   24541   548125    22.3 | 18.871 % |
c ==============================================================================
c [1mFound solution: 9253133[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010645567   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26613 |  169540   508122 |   56513   24555   548189    22.3 | 18.871 % |
c ==============================================================================
c [1mFound solution: 9253005[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010645695   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26642 |  169542   508159 |   56514   24584   548303    22.3 | 18.871 % |
c ==============================================================================
c [1mFound solution: 9252941[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010645759   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26665 |  169544   508172 |   56514   24607   548393    22.3 | 18.871 % |
c |     26765 |  169418   507882 |   62165   24672   550196    22.3 | 19.042 % |
c |     26918 |  169210   507294 |   68381   24811   553508    22.3 | 19.120 % |
c ==============================================================================
c [1mFound solution: 9252813[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010645887   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26955 |  169212   507307 |   56404   24848   553623    22.3 | 19.120 % |
c ==============================================================================
c [1mFound solution: 9252685[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010646015   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26964 |  169214   507320 |   56404   24857   553651    22.3 | 19.120 % |
c ==============================================================================
c [1mFound solution: 9245389[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010653311   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26971 |  169221   507376 |   56407   24864   553672    22.3 | 19.120 % |
c ==============================================================================
c [1mFound solution: 9245261[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010653439   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26980 |  169223   507389 |   56407   24873   553702    22.3 | 19.120 % |
c ==============================================================================
c [1mFound solution: 9244877[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010653823   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27028 |  169208   507381 |   56402   24920   554565    22.3 | 19.120 % |
c ==============================================================================
c [1mFound solution: 9244749[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010653951   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27036 |  169210   507397 |   56403   24928   554591    22.2 | 19.120 % |
c ==============================================================================
c [1mFound solution: 9244621[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010654079   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27039 |  169212   507413 |   56404   24931   554600    22.2 | 19.120 % |
c ==============================================================================
c [1mFound solution: 9244493[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010654207   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27045 |  169214   507426 |   56404   24937   554708    22.2 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8993485[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010905215   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27053 |  169224   507501 |   56408   24945   554758    22.2 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8993357[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3010905343   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27111 |  169191   507405 |   56397   24998   555065    22.2 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8731341[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011167359   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27203 |  169194   507449 |   56398   25089   555880    22.2 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8731213[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011167487   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27226 |  169155   507336 |   56385   25107   555938    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8730829[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011167871   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27229 |  169158   507372 |   56386   25110   555950    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8730701[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011167999   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27232 |  169160   507391 |   56386   25113   555959    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8730573[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011168127   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27254 |  169143   507367 |   56381   25133   556117    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8730445[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011168255   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27256 |  169145   507377 |   56381   25135   556126    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8729293[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011169407   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27256 |  169149   507405 |   56383   25135   556126    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8729165[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011169535   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27261 |  169151   507415 |   56383   25140   556155    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8728781[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011169919   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27261 |  169155   507444 |   56385   25140   556155    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8728653[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011170047   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27261 |  169157   507457 |   56385   25140   556155    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8728525[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011170175   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27262 |  169159   507470 |   56386   25141   556158    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8728397[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011170303   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27264 |  169161   507483 |   56387   25143   556167    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8721101[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011177599   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27266 |  169169   507537 |   56389   25145   556180    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8720973[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011177727   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27269 |  169171   507550 |   56390   25148   556194    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8720589[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011178111   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27272 |  169175   507579 |   56391   25151   556216    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8720337[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011178363   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27282 |  169186   507703 |   56395   25161   556309    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8720205[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011178495   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27284 |  169188   507715 |   56396   25163   556315    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 8665805[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3011232895   bits: 32/32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27286 |  169198   507783 |   56399   25165   556326    22.1 | 19.120 % |
c ==============================================================================
c [1mFound solution: 1946317[0m
c ---[   0]---> Adder-cost: 154   maxlim: 375540863   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27290 |  163827   487838 |   54609   24825   555104    22.4 | 19.120 % |
c ==============================================================================
c [1mFound solution: 1905229[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375581951   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27315 |  163837   487892 |   54612   24850   555253    22.3 | 19.120 % |
c |     27418 |  163534   486796 |   60073   24900   555561    22.3 | 21.260 % |
c ==============================================================================
c [1mFound solution: 1904717[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375582463   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27485 |  163176   485500 |   54392   24860   555266    22.3 | 21.260 % |
c ==============================================================================
c [1mFound solution: 1904589[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375582591   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27486 |  163178   485510 |   54392   24861   555269    22.3 | 21.260 % |
c |     27586 |  163093   485317 |   59831   24959   558610    22.4 | 21.375 % |
c ==============================================================================
c [1mFound solution: 1904461[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375582719   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27622 |  163095   485324 |   54365   24995   559550    22.4 | 21.375 % |
c ==============================================================================
c [1mFound solution: 1901261[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375585919   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27624 |  163101   485359 |   54367   24997   559556    22.4 | 21.375 % |
c ==============================================================================
c [1mFound solution: 1900749[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375586431   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27625 |  163105   485384 |   54368   24998   559561    22.4 | 21.375 % |
c ==============================================================================
c [1mFound solution: 1900493[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375586687   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27629 |  163109   485413 |   54369   25002   559579    22.4 | 21.375 % |
c ==============================================================================
c [1mFound solution: 1900365[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375586815   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27629 |  163111   485420 |   54370   25002   559579    22.4 | 21.375 % |
c ==============================================================================
c [1mFound solution: 1843917[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375643263   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27632 |  163122   485483 |   54374   25005   559588    22.4 | 21.375 % |
c ==============================================================================
c [1mFound solution: 1843661[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375643519   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27639 |  163126   485511 |   54375   25012   560158    22.4 | 21.375 % |
c ==============================================================================
c [1mFound solution: 1843181[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375643999   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27677 |  163134   485572 |   54378   25050   561031    22.4 | 21.375 % |
c ==============================================================================
c [1mFound solution: 1839565[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375647615   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27708 |  163144   485625 |   54381   25081   561694    22.4 | 21.375 % |
c |     27814 |  163144   485625 |   59819   25187   563608    22.4 | 21.396 % |
c ==============================================================================
c [1mFound solution: 1836493[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375650687   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27899 |  163152   485676 |   54384   25272   564863    22.4 | 21.396 % |
c ==============================================================================
c [1mFound solution: 1836365[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375650815   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27963 |  163110   485588 |   54370   25335   566595    22.4 | 21.396 % |
c ==============================================================================
c [1mFound solution: 1835981[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375651199   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27987 |  163114   485621 |   54371   25359   567154    22.4 | 21.396 % |
c ==============================================================================
c [1mFound solution: 1835853[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375651327   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27989 |  163116   485631 |   54372   25361   567190    22.4 | 21.396 % |
c ==============================================================================
c [1mFound solution: 1835469[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375651711   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27989 |  163120   485657 |   54373   25361   567190    22.4 | 21.396 % |
c ==============================================================================
c [1mFound solution: 1835341[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375651839   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27990 |  163122   485667 |   54374   25362   567196    22.4 | 21.396 % |
c ==============================================================================
c [1mFound solution: 1834957[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375652223   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27993 |  163126   485692 |   54375   25365   567207    22.4 | 21.396 % |
c ==============================================================================
c [1mFound solution: 1834829[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375652351   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28046 |  163068   485564 |   54356   25416   568989    22.4 | 21.396 % |
c ==============================================================================
c [1mFound solution: 1652173[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375835007   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28067 |  163080   485624 |   54360   25437   569068    22.4 | 21.396 % |
c ==============================================================================
c [1mFound solution: 1652045[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375835135   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28071 |  163082   485638 |   54360   25441   569080    22.4 | 21.396 % |
c ==============================================================================
c [1mFound solution: 1651661[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375835519   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28083 |  163086   485668 |   54362   25453   569138    22.4 | 21.396 % |
c ==============================================================================
c [1mFound solution: 1651533[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375835647   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28163 |  163041   485570 |   54347   25531   571176    22.4 | 21.396 % |
c |     28263 |  163001   485426 |   59781   25627   572963    22.4 | 21.501 % |
c |     28413 |  162760   484609 |   65759   25705   573355    22.3 | 21.564 % |
c |     28638 |  162719   484452 |   72335   25918   576158    22.2 | 21.574 % |
c ==============================================================================
c [1mFound solution: 1587661[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375899519   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28762 |  162700   484444 |   54233   26039   578301    22.2 | 21.574 % |
c ==============================================================================
c [1mFound solution: 1587533[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375899647   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28774 |  162702   484459 |   54234   26051   578622    22.2 | 21.574 % |
c ==============================================================================
c [1mFound solution: 1587149[0m
c ---[   0]---> Adder-cost: 0   maxlim: 375900031   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28797 |  162706   484489 |   54235   26074   578715    22.2 | 21.574 % |
c ==============================================================================
c [1mFound solution: 1389901[0m
c ---[   0]---> Adder-cost: 0   maxlim: 376097279   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28827 |  162717   484526 |   54239   26104   578879    22.2 | 21.574 % |
c ==============================================================================
c [1mFound solution: 1388877[0m
c ---[   0]---> Adder-cost: 0   maxlim: 376098303   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28870 |  162625   484318 |   54208   26132   579210    22.2 | 21.574 % |
c |     28972 |  162285   483104 |   59628   26139   579717    22.2 | 21.725 % |
c ==============================================================================
c [1mFound solution: 1388397[0m
c ---[   0]---> Adder-cost: 0   maxlim: 376098783   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28986 |  162293   483147 |   54097   26153   579801    22.2 | 21.725 % |
c ==============================================================================
c [1mFound solution: 1388365[0m
c ---[   0]---> Adder-cost: 0   maxlim: 376098815   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29026 |  162295   483154 |   54098   26193   580033    22.1 | 21.725 % |
c ==============================================================================
c [1mFound solution: 1385037[0m
c ---[   0]---> Adder-cost: 0   maxlim: 376102143   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29072 |  162301   483193 |   54100   26239   580802    22.1 | 21.725 % |
c ==============================================================================
c [1mFound solution: 1384525[0m
c ---[   0]---> Adder-cost: 0   maxlim: 376102655   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29111 |  162305   483219 |   54101   26278   581295    22.1 | 21.725 % |
c ==============================================================================
c [1mFound solution: 1381965[0m
c ---[   0]---> Adder-cost: 0   maxlim: 376105215   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29123 |  162311   483247 |   54103   26290   581462    22.1 | 21.725 % |
c ==============================================================================
c [1mFound solution: 1122893[0m
c ---[   0]---> Adder-cost: 0   maxlim: 376364287   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29137 |  162326   483314 |   54108   26304   581693    22.1 | 21.725 % |
c ==============================================================================
c [1mFound solution: 1061453[0m
c ---[   0]---> Adder-cost: 0   maxlim: 376425727   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29166 |  162338   483363 |   54112   26333   581887    22.1 | 21.725 % |
c ==============================================================================
c [1mFound solution: 795981[0m
c ---[   0]---> Adder-cost: 154   maxlim: 187947519   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29178 |  160683   477486 |   53561   26060   580798    22.3 | 21.725 % |
c |     29278 |  160486   477028 |   58917   26150   584301    22.3 | 22.575 % |
c ==============================================================================
c [1mFound solution: 790989[0m
c ---[   0]---> Adder-cost: 0   maxlim: 187952511   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29391 |  160156   476219 |   53385   26222   585005    22.3 | 22.575 % |
c ==============================================================================
c [1mFound solution: 790925[0m
c ---[   0]---> Adder-cost: 0   maxlim: 187952575   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29411 |  160158   476234 |   53386   26242   585072    22.3 | 22.575 % |
c ==============================================================================
c [1mFound solution: 790861[0m
c ---[   0]---> Adder-cost: 0   maxlim: 187952639   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29415 |  160160   476246 |   53386   26246   585128    22.3 | 22.575 % |
c ==============================================================================
c [1mFound solution: 790413[0m
c ---[   0]---> Adder-cost: 0   maxlim: 187953087   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29433 |  160061   476017 |   53353   26205   584622    22.3 | 22.575 % |
c ==============================================================================
c [1mFound solution: 602637[0m
c ---[   0]---> Adder-cost: 0   maxlim: 188140863   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29458 |  160073   476089 |   53357   26230   584707    22.3 | 22.575 % |
c ==============================================================================
c [1mFound solution: 602573[0m
c ---[   0]---> Adder-cost: 0   maxlim: 188140927   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29476 |  160075   476101 |   53358   26248   584780    22.3 | 22.575 % |
c ==============================================================================
c [1mFound solution: 601997[0m
c ---[   0]---> Adder-cost: 0   maxlim: 188141503   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29482 |  160083   476149 |   53361   26254   584803    22.3 | 22.575 % |
c |     29585 |  160083   476149 |   58697   26357   587710    22.3 | 22.765 % |
c ==============================================================================
c [1mFound solution: 601933[0m
c ---[   0]---> Adder-cost: 0   maxlim: 188141567   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29621 |  160085   476159 |   53361   26393   588341    22.3 | 22.765 % |
c |     29722 |  159129   473332 |   58697   26386   588707    22.3 | 23.087 % |
c |     29872 |  158850   472391 |   64566   26478   589545    22.3 | 23.151 % |
c ==============================================================================
c [1mFound solution: 598541[0m
c ---[   0]---> Adder-cost: 0   maxlim: 188144959   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29981 |  158851   472402 |   52950   26585   590846    22.2 | 23.151 % |
c ==============================================================================
c [1mFound solution: 598413[0m
c ---[   0]---> Adder-cost: 0   maxlim: 188145087   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29998 |  158855   472427 |   52951   26602   590902    22.2 | 23.151 % |
c |     30099 |  158849   472415 |   58246   26702   592143    22.2 | 23.161 % |
c ==============================================================================
c [1mFound solution: 598029[0m
c ---[   0]---> Adder-cost: 0   maxlim: 188145471   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30139 |  158855   472446 |   52951   26742   592859    22.2 | 23.161 % |
c ==============================================================================
c [1mFound solution: 467341[0m
c ---[   0]---> Adder-cost: 154   maxlim: 93904319   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30236 |  157147   465257 |   52382   26606   592308    22.3 | 23.161 % |
c |     30336 |  157147   465257 |   57620   26706   592808    22.2 | 23.893 % |
c |     30489 |  157029   464908 |   63382   26832   594227    22.1 | 23.930 % |
c |     30714 |  156581   463400 |   69720   26960   594993    22.1 | 24.039 % |
c |     31052 |  155864   460919 |   76692   27197   605422    22.3 | 24.216 % |
c ==============================================================================
c [1mFound solution: 340493[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94031167   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31475 |  155447   459739 |   51815   27532   613767    22.3 | 24.216 % |
c |     31576 |  155394   459554 |   56996   27611   614876    22.3 | 24.384 % |
c |     31726 |  154035   455349 |   62696   27464   614141    22.4 | 24.864 % |
c ==============================================================================
c [1mFound solution: 332301[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94039359   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31933 |  154004   455287 |   51334   27670   617509    22.3 | 24.864 % |
c |     32036 |  154004   455287 |   56467   27773   621068    22.4 | 24.886 % |
c |     32188 |  153179   453375 |   62114   27894   622067    22.3 | 25.260 % |
c ==============================================================================
c [1mFound solution: 331789[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94039871   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32261 |  153156   453297 |   51052   27956   622442    22.3 | 25.260 % |
c ==============================================================================
c [1mFound solution: 331661[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94039999   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32318 |  153104   453122 |   51034   27999   623125    22.3 | 25.260 % |
c ==============================================================================
c [1mFound solution: 329485[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94042175   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32322 |  153109   453147 |   51036   28003   623141    22.3 | 25.260 % |
c ==============================================================================
c [1mFound solution: 328077[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94043583   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32328 |  153117   453187 |   51039   28009   623161    22.2 | 25.260 % |
c |     32429 |  153117   453187 |   56142   28110   625375    22.2 | 25.287 % |
c ==============================================================================
c [1mFound solution: 328013[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94043647   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32497 |  153119   453194 |   51039   28178   625612    22.2 | 25.287 % |
c ==============================================================================
c [1mFound solution: 327693[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94043967   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32501 |  153024   452867 |   51008   28159   625538    22.2 | 25.287 % |
c ==============================================================================
c [1mFound solution: 327565[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94044095   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32551 |  153028   452890 |   51009   28209   626128    22.2 | 25.287 % |
c |     32654 |  152501   451719 |   56109   28308   627430    22.2 | 25.585 % |
c ==============================================================================
c [1mFound solution: 309005[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94062655   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32786 |  152439   451519 |   50813   28433   629237    22.1 | 25.585 % |
c |     32886 |  152078   450656 |   55894   28528   631187    22.1 | 25.774 % |
c ==============================================================================
c [1mFound solution: 292237[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94079423   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32996 |  152087   450707 |   50695   28638   632108    22.1 | 25.774 % |
c ==============================================================================
c [1mFound solution: 275981[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94095679   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33019 |  151652   449763 |   50550   28660   632376    22.1 | 25.774 % |
c ==============================================================================
c [1mFound solution: 274957[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94096703   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33023 |  151658   449786 |   50552   28664   632419    22.1 | 25.774 % |
c ==============================================================================
c [1mFound solution: 274829[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94096831   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33026 |  151662   449802 |   50554   28667   632432    22.1 | 25.774 % |
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 |     33030 |  151664   449810 |   50554   28671   632451    22.1 | 25.774 % |
c ==============================================================================
c [1mFound solution: 274317[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94097343   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33083 |  151670   449834 |   50556   28724   632950    22.0 | 25.774 % |
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 |     33088 |  151672   449842 |   50557   28729   632999    22.0 | 25.774 % |
c ==============================================================================
c [1mFound solution: 272909[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94098751   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33111 |  151677   449879 |   50559   28752   633144    22.0 | 25.774 % |
c ==============================================================================
c [1mFound solution: 270861[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94100799   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33176 |  151685   449914 |   50561   28817   634445    22.0 | 25.774 % |
c ==============================================================================
c [1mFound solution: 270733[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94100927   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33202 |  151630   449796 |   50543   28840   634715    22.0 | 25.774 % |
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 |     33281 |  151560   449628 |   50520   28910   636607    22.0 | 25.774 % |
c ==============================================================================
c [1mFound solution: 270637[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94101023   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33303 |  151562   449645 |   50520   28932   636693    22.0 | 25.774 % |
c ==============================================================================
c [1mFound solution: 270381[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94101279   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33322 |  151566   449665 |   50522   28951   636756    22.0 | 25.774 % |
c ==============================================================================
c [1mFound solution: 270221[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94101439   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33325 |  151570   449689 |   50523   28954   636771    22.0 | 25.774 % |
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 |     33364 |  151572   449697 |   50524   28993   637389    22.0 | 25.774 % |
c ==============================================================================
c [1mFound solution: 267021[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94104639   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33394 |  151578   449727 |   50526   29023   638004    22.0 | 25.774 % |
c ==============================================================================
c [1mFound solution: 266957[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94104703   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33403 |  151580   449738 |   50526   29032   638089    22.0 | 25.774 % |
c ==============================================================================
c [1mFound solution: 266765[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94104895   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33413 |  151541   449614 |   50513   29033   638145    22.0 | 25.774 % |
c ==============================================================================
c [1mFound solution: 266509[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94105151   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33428 |  151538   449614 |   50512   29046   638208    22.0 | 25.774 % |
c ==============================================================================
c [1mFound solution: 266445[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94105215   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33453 |  151010   447457 |   50336   29019   638570    22.0 | 25.774 % |
c |     33553 |  151001   447428 |   55369   29113   639074    22.0 | 26.232 % |
c ==============================================================================
c [1mFound solution: 266125[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94105535   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33653 |  150996   447426 |   50332   29212   640149    21.9 | 26.232 % |
c |     33753 |  150987   447397 |   55365   29310   640769    21.9 | 26.242 % |
c ==============================================================================
c [1mFound solution: 266101[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94105559   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33766 |  150989   447430 |   50329   29323   640850    21.9 | 26.242 % |
c ==============================================================================
c [1mFound solution: 266077[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94105583   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33776 |  150993   447463 |   50331   29333   640913    21.8 | 26.242 % |
c |     33878 |  150961   447359 |   55364   29424   641782    21.8 | 26.254 % |
c |     34030 |  150870   447148 |   60900   29555   646869    21.9 | 26.296 % |
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 |     34065 |  150863   447127 |   50287   29588   647007    21.9 | 26.296 % |
c ==============================================================================
c [1mFound solution: 262685[0m
c ---[   0]---> Adder-cost: 0   maxlim: 94108975   bits: 27/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34087 |  150855   447117 |   50285   29602   647076    21.9 | 26.296 % |
c ==============================================================================
c [1mFound solution: 225805[0m
c ---[   0]---> Adder-cost: 154   maxlim: 46959935   bits: 26/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34180 |  149755   442864 |   49918   29454   647207    22.0 | 26.296 % |
c ==============================================================================
c [1mFound solution: 225757[0m
c ---[   0]---> Adder-cost: 0   maxlim: 46959983   bits: 26/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34218 |  149759   442901 |   49919   29492   647909    22.0 | 26.296 % |
c ==============================================================================
c [1mFound solution: 225741[0m
c ---[   0]---> Adder-cost: 0   maxlim: 46959999   bits: 26/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34307 |  149761   442915 |   49920   29581   648707    21.9 | 26.296 % |
c |     34408 |  149589   442517 |   54912   29666   650520    21.9 | 26.949 % |
c |     34558 |  149541   442401 |   60403   29815   653743    21.9 | 26.974 % |
c ==============================================================================
c [1mFound solution: 123429[0m
c ---[   0]---> Adder-cost: 154   maxlim: 23469351   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34736 |  148382   438314 |   49460   29652   655127    22.1 | 26.974 % |
c |     34836 |  146813   432593 |   54406   29343   654728    22.3 | 27.942 % |
c ==============================================================================
c [1mFound solution: 123421[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23469359   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34922 |  146815   432607 |   48938   29429   655852    22.3 | 27.942 % |
c ==============================================================================
c [1mFound solution: 123413[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23469367   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34990 |  146791   432537 |   48930   29470   656259    22.3 | 27.942 % |
c ==============================================================================
c [1mFound solution: 119581[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23473199   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35014 |  146630   432019 |   48876   29401   656043    22.3 | 27.942 % |
c ==============================================================================
c [1mFound solution: 119573[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23473207   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35028 |  146632   432039 |   48877   29415   656223    22.3 | 27.942 % |
c ==============================================================================
c [1mFound solution: 119565[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23473215   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35057 |  146634   432052 |   48878   29444   656347    22.3 | 27.942 % |
c ==============================================================================
c [1mFound solution: 119517[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23473263   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35070 |  146638   432090 |   48879   29457   656386    22.3 | 27.942 % |
c |     35170 |  146034   430703 |   53766   29503   657855    22.3 | 28.247 % |
c ==============================================================================
c [1mFound solution: 119509[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23473271   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35212 |  146027   430694 |   48675   29540   658105    22.3 | 28.247 % |
c ==============================================================================
c [1mFound solution: 119501[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23473279   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35219 |  146029   430707 |   48676   29547   658191    22.3 | 28.247 % |
c |     35319 |  145893   430389 |   53543   29638   659058    22.2 | 28.307 % |
c ==============================================================================
c [1mFound solution: 81437[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23511343   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35336 |  145901   430454 |   48633   29655   659157    22.2 | 28.307 % |
c |     35436 |  145901   430454 |   53496   29755   660446    22.2 | 28.311 % |
c ==============================================================================
c [1mFound solution: 81421[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23511359   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35577 |  145130   428685 |   48376   29879   662536    22.2 | 28.311 % |
c |     35677 |  145130   428685 |   53213   29979   664725    22.2 | 28.647 % |
c ==============================================================================
c [1mFound solution: 81181[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23511599   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35750 |  145135   428733 |   48378   30052   665395    22.1 | 28.647 % |
c |     35855 |  144574   427273 |   53215   30085   666800    22.2 | 28.866 % |
c |     36005 |  144574   427273 |   58537   30235   671424    22.2 | 28.866 % |
c ==============================================================================
c [1mFound solution: 81165[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23511615   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36026 |  144576   427290 |   48192   30256   671669    22.2 | 28.866 % |
c ==============================================================================
c [1mFound solution: 80925[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23511855   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36104 |  144557   427260 |   48185   30333   672675    22.2 | 28.866 % |
c ==============================================================================
c [1mFound solution: 80413[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23512367   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36147 |  144565   427312 |   48188   30376   672988    22.2 | 28.866 % |
c ==============================================================================
c [1mFound solution: 80157[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23512623   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36194 |  144571   427355 |   48190   30423   673591    22.1 | 28.866 % |
c ==============================================================================
c [1mFound solution: 80141[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23512639   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36199 |  144573   427371 |   48191   30428   673609    22.1 | 28.866 % |
c ==============================================================================
c [1mFound solution: 79645[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23513135   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36201 |  144579   427415 |   48193   30430   673617    22.1 | 28.866 % |
c ==============================================================================
c [1mFound solution: 79629[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23513151   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36203 |  144581   427429 |   48193   30432   673623    22.1 | 28.866 % |
c ==============================================================================
c [1mFound solution: 79581[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23513199   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36205 |  144585   427465 |   48195   30434   673629    22.1 | 28.866 % |
c ==============================================================================
c [1mFound solution: 79565[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23513215   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36211 |  144497   427270 |   48165   30437   673560    22.1 | 28.866 % |
c ==============================================================================
c [1mFound solution: 79517[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23513263   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36221 |  144501   427308 |   48167   30447   673690    22.1 | 28.866 % |
c ==============================================================================
c [1mFound solution: 79501[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23513279   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36223 |  144503   427326 |   48167   30449   673696    22.1 | 28.866 % |
c ==============================================================================
c [1mFound solution: 79453[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23513327   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36224 |  144507   427364 |   48169   30450   673699    22.1 | 28.866 % |
c ==============================================================================
c [1mFound solution: 79437[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23513343   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36225 |  144509   427374 |   48169   30451   673702    22.1 | 28.866 % |
c ==============================================================================
c [1mFound solution: 79133[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23513647   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36225 |  144515   427416 |   48171   30451   673702    22.1 | 28.866 % |
c ==============================================================================
c [1mFound solution: 79117[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23513663   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36225 |  144517   427432 |   48172   30451   673702    22.1 | 28.866 % |
c ==============================================================================
c [1mFound solution: 79069[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23513711   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36241 |  144521   427468 |   48173   30467   673883    22.1 | 28.866 % |
c ==============================================================================
c [1mFound solution: 79053[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23513727   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36291 |  144016   425713 |   48005   30307   673608    22.2 | 28.866 % |
c ==============================================================================
c [1mFound solution: 76573[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23516207   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36346 |  144023   425762 |   48007   30362   674032    22.2 | 28.866 % |
c |     36446 |  144014   425733 |   52807   30455   676576    22.2 | 29.066 % |
c ==============================================================================
c [1mFound solution: 75489[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23517291   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36534 |  144023   425808 |   48007   30543   678029    22.2 | 29.066 % |
c |     36634 |  143913   425555 |   52807   30641   679754    22.2 | 29.117 % |
c |     36785 |  143821   425237 |   58088   30763   689453    22.4 | 29.138 % |
c ==============================================================================
c [1mFound solution: 71389[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23521391   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36967 |  143830   425293 |   47943   30945   693245    22.4 | 29.138 % |
c |     37068 |  143506   424162 |   52737   30964   696683    22.5 | 29.239 % |
c |     37219 |  143506   424162 |   58011   31115   704972    22.7 | 29.239 % |
c ==============================================================================
c [1mFound solution: 71381[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23521399   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37286 |  142949   422146 |   47649   30966   705478    22.8 | 29.239 % |
c |     37386 |  142949   422146 |   52413   31066   707664    22.8 | 29.386 % |
c |     37537 |  142949   422146 |   57655   31217   712096    22.8 | 29.386 % |
c ==============================================================================
c [1mFound solution: 71261[0m
c ---[   0]---> Adder-cost: 0   maxlim: 23521519   bits: 25/25
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37567 |  142957   422199 |   47652   31247   712865    22.8 | 29.386 % |
c ==============================================================================
c [1mFound solution: 64205[0m
c ---[   0]---> Adder-cost: 154   maxlim: 11732095   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37660 |  141695   418206 |   47231   31144   713712    22.9 | 29.386 % |
c ==============================================================================
c [1mFound solution: 64077[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11732223   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37662 |  141697   418219 |   47232   31146   713719    22.9 | 29.386 % |
c ==============================================================================
c [1mFound solution: 63949[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11732351   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37663 |  141699   418233 |   47233   31147   713722    22.9 | 29.386 % |
c ==============================================================================
c [1mFound solution: 63693[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11732607   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37667 |  141703   418261 |   47234   31151   713734    22.9 | 29.386 % |
c ==============================================================================
c [1mFound solution: 63437[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11732863   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37668 |  141707   418289 |   47235   31152   713737    22.9 | 29.386 % |
c ==============================================================================
c [1mFound solution: 63309[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11732991   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37669 |  141709   418300 |   47236   31153   713740    22.9 | 29.386 % |
c ==============================================================================
c [1mFound solution: 60109[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11736191   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37670 |  141715   418338 |   47238   31154   713754    22.9 | 29.386 % |
c |     37770 |  141715   418338 |   51961   31254   722627    23.1 | 30.114 % |
c |     37920 |  141715   418338 |   57157   31404   728264    23.2 | 30.114 % |
c ==============================================================================
c [1mFound solution: 47821[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11748479   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37955 |  141720   418367 |   47240   31439   728715    23.2 | 30.114 % |
c ==============================================================================
c [1mFound solution: 47325[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11748975   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37968 |  141728   418424 |   47242   31452   728905    23.2 | 30.114 % |
c ==============================================================================
c [1mFound solution: 40669[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11755631   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37973 |  141736   418479 |   47245   31457   729005    23.2 | 30.114 % |
c ==============================================================================
c [1mFound solution: 40653[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11755647   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37973 |  141738   418494 |   47246   31457   729005    23.2 | 30.114 % |
c ==============================================================================
c [1mFound solution: 40413[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11755887   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37973 |  141746   418553 |   47248   31457   729005    23.2 | 30.114 % |
c ==============================================================================
c [1mFound solution: 40157[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11756143   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37974 |  141754   418611 |   47251   31458   729009    23.2 | 30.114 % |
c ==============================================================================
c [1mFound solution: 40141[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11756159   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37974 |  141756   418626 |   47252   31458   729009    23.2 | 30.114 % |
c ==============================================================================
c [1mFound solution: 39901[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11756399   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37974 |  141764   418687 |   47254   31458   729009    23.2 | 30.114 % |
c ==============================================================================
c [1mFound solution: 39885[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11756415   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37975 |  141766   418702 |   47255   31459   729012    23.2 | 30.114 % |
c ==============================================================================
c [1mFound solution: 39805[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11756495   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37977 |  141770   418737 |   47256   31461   729018    23.2 | 30.114 % |
c ==============================================================================
c [1mFound solution: 39773[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11756527   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37979 |  141774   418770 |   47258   31463   729030    23.2 | 30.114 % |
c ==============================================================================
c [1mFound solution: 39757[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11756543   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37998 |  141776   418783 |   47258   31482   729290    23.2 | 30.114 % |
c |     38101 |  141198   417064 |   51983   31379   729299    23.2 | 30.300 % |
c ==============================================================================
c [1mFound solution: 39677[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11756623   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38181 |  141202   417098 |   47067   31459   730669    23.2 | 30.300 % |
c ==============================================================================
c [1mFound solution: 39661[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11756639   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38228 |  141201   417107 |   47067   31505   731635    23.2 | 30.300 % |
c ==============================================================================
c [1mFound solution: 39469[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11756831   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38253 |  141205   417134 |   47068   31530   731971    23.2 | 30.300 % |
c ==============================================================================
c [1mFound solution: 39437[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11756863   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38278 |  141207   417148 |   47069   31555   732269    23.2 | 30.300 % |
c ==============================================================================
c [1mFound solution: 39341[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11756959   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38283 |  141211   417178 |   47070   31560   732331    23.2 | 30.300 % |
c ==============================================================================
c [1mFound solution: 39309[0m
c ---[   0]---> Adder-cost: 0   maxlim: 11756991   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38305 |  141213   417193 |   47071   31582   732527    23.2 | 30.300 % |
c |     38407 |  141213   417193 |   51778   31684   740226    23.4 | 30.307 % |
c |     38557 |  141104   416840 |   56955   31785   747146    23.5 | 30.337 % |
c ==============================================================================
c [1mFound solution: 16189[0m
c ---[   0]---> Adder-cost: 154   maxlim: 2932751   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38708 |  138225   406542 |   46075   30920   745673    24.1 | 30.337 % |
c |     38810 |  138106   406263 |   50682   30997   747103    24.1 | 31.559 % |
c ==============================================================================
c [1mFound solution: 16109[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2932831   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38891 |  138110   406287 |   46036   31078   751655    24.2 | 31.559 % |
c |     38992 |  137983   405840 |   50639   31139   752806    24.2 | 31.583 % |
c |     39144 |  137715   404904 |   55703   31239   753806    24.1 | 31.644 % |
c |     39371 |  137706   404873 |   61273   31381   765043    24.4 | 31.645 % |
c |     39709 |  136799   401647 |   67401   31269   768650    24.6 | 31.859 % |
c |     40217 |  136552   400814 |   74141   31243   767519    24.6 | 31.926 % |
c |     40976 |  135871   397901 |   81555   31661   796802    25.2 | 32.099 % |
c ==============================================================================
c [1mFound solution: 14893[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2934047   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41024 |  135569   396865 |   45189   31480   795568    25.3 | 32.099 % |
c |     41124 |  135517   396679 |   49707   31552   799983    25.4 | 32.190 % |
c |     41275 |  135517   396679 |   54678   31703   805848    25.4 | 32.190 % |
c |     41500 |  135354   396252 |   60146   31856   809913    25.4 | 32.259 % |
c |     41837 |  135354   396252 |   66161   32193   832822    25.9 | 32.259 % |
c |     42343 |  135315   396136 |   72777   32599   857845    26.3 | 32.278 % |
c ==============================================================================
c [1mFound solution: 13837[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935103   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42488 |  135319   396149 |   45106   32744   864877    26.4 | 32.278 % |
c |     42588 |  135319   396149 |   49616   32844   869138    26.5 | 32.280 % |
c |     42739 |  135308   396106 |   54578   32994   874595    26.5 | 32.283 % |
c |     42965 |  135249   395909 |   60036   33183   881805    26.6 | 32.297 % |
c |     43303 |  135098   395392 |   66039   33462   893366    26.7 | 32.335 % |
c ==============================================================================
c [1mFound solution: 13789[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935151   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43499 |  135102   395409 |   45034   33658   902646    26.8 | 32.335 % |
c |     43602 |  135063   395318 |   49537   33758   907012    26.9 | 32.355 % |
c |     43752 |  135063   395318 |   54491   33908   918840    27.1 | 32.355 % |
c |     43977 |  134981   395059 |   59940   34110   928685    27.2 | 32.378 % |
c |     44315 |  134981   395059 |   65934   34448   946334    27.5 | 32.378 % |
c |     44821 |  134805   394624 |   72527   34951   966969    27.7 | 32.465 % |
c ==============================================================================
c [1mFound solution: 13773[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935167   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45228 |  134779   394534 |   44926   35348   991380    28.0 | 32.465 % |
c |     45328 |  134779   394534 |   49418   35448   994203    28.0 | 32.472 % |
c |     45478 |  134779   394534 |   54360   35598  1002309    28.2 | 32.472 % |
c |     45704 |  134779   394534 |   59796   35824  1012370    28.3 | 32.472 % |
c ==============================================================================
c [1mFound solution: 13725[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935215   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45763 |  134783   394554 |   44927   35883  1015286    28.3 | 32.472 % |
c |     45863 |  134783   394554 |   49419   35983  1023162    28.4 | 32.473 % |
c |     46014 |  134760   394500 |   54361   36132  1026498    28.4 | 32.484 % |
c |     46240 |  134618   394012 |   59797   36304  1038518    28.6 | 32.519 % |
c |     46577 |  134618   394012 |   65777   36641  1053969    28.8 | 32.519 % |
c |     47083 |  134618   394012 |   72355   37147  1073965    28.9 | 32.519 % |
c |     47842 |  134541   393739 |   79590   37877  1125542    29.7 | 32.537 % |
c |     48985 |  134362   393280 |   87550   38993  1210222    31.0 | 32.609 % |
c ==============================================================================
c [1mFound solution: 13705[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935235   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50485 |  134301   393130 |   44767   40481  1298156    32.1 | 32.609 % |
c |     50587 |  134301   393130 |   49243   40583  1305762    32.2 | 32.633 % |
c ==============================================================================
c [1mFound solution: 13677[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935263   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50690 |  134303   393140 |   44767   40686  1311652    32.2 | 32.633 % |
c |     50792 |  134303   393140 |   49243   40788  1317083    32.3 | 32.634 % |
c |     50944 |  134303   393140 |   54168   40940  1324818    32.4 | 32.634 % |
c |     51169 |  134303   393140 |   59584   41165  1342505    32.6 | 32.634 % |
c |     51510 |  134303   393140 |   65543   41506  1378175    33.2 | 32.634 % |
c ==============================================================================
c [1mFound solution: 13373[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935567   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51832 |  134309   393164 |   44769   41828  1399209    33.5 | 32.634 % |
c |     51932 |  134309   393164 |   49245   41928  1408301    33.6 | 32.635 % |
c |     52086 |  134309   393164 |   54170   42082  1420314    33.8 | 32.635 % |
c |     52311 |  134309   393164 |   59587   42307  1435820    33.9 | 32.635 % |
c |     52649 |  134309   393164 |   65546   42645  1469276    34.5 | 32.635 % |
c ==============================================================================
c [1mFound solution: 13367[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935573   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52845 |  134302   393160 |   44767   42816  1475860    34.5 | 32.635 % |
c |     52946 |  134302   393160 |   49243   42917  1480728    34.5 | 32.638 % |
c |     53098 |  134302   393160 |   54168   43069  1488239    34.6 | 32.638 % |
c ==============================================================================
c [1mFound solution: 13365[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935575   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53262 |  134199   392694 |   44733   43170  1496164    34.7 | 32.638 % |
c |     53362 |  134199   392694 |   49206   43270  1502290    34.7 | 32.663 % |
c ==============================================================================
c [1mFound solution: 13269[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935671   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53392 |  134207   392731 |   44735   43300  1503073    34.7 | 32.663 % |
c |     53492 |  134207   392731 |   49208   43400  1507532    34.7 | 32.665 % |
c |     53642 |  134207   392731 |   54129   43550  1516900    34.8 | 32.665 % |
c |     53871 |  134082   392439 |   59542   43768  1529433    34.9 | 32.715 % |
c |     54209 |  133962   392072 |   65496   44075  1544018    35.0 | 32.751 % |
c |     54717 |  133850   391809 |   72046   44570  1568264    35.2 | 32.798 % |
c |     55476 |  133804   391706 |   79250   45325  1616093    35.7 | 32.818 % |
c |     56615 |  133645   391191 |   87175   46414  1691690    36.4 | 32.860 % |
c |     58323 |  133607   391100 |   95893   48121  1842852    38.3 | 32.875 % |
c ==============================================================================
c [1mFound solution: 13261[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935679   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     58710 |  133609   391107 |   44536   48508  1863775    38.4 | 32.875 % |
c |     58810 |  133609   391107 |   48989   48608  1867906    38.4 | 32.875 % |
c |     58960 |  133609   391107 |   53888   48758  1878459    38.5 | 32.875 % |
c |     59187 |  133609   391107 |   59277   48985  1893606    38.7 | 32.875 % |
c |     59525 |  133609   391107 |   65205   49323  1910381    38.7 | 32.875 % |
c ==============================================================================
c [1mFound solution: 13245[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935695   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59567 |  133611   391120 |   44537   49365  1911710    38.7 | 32.875 % |
c |     59668 |  133611   391120 |   48990   49466  1918873    38.8 | 32.876 % |
c |     59819 |  133611   391120 |   53889   49617  1932373    38.9 | 32.876 % |
c |     60044 |  133603   391104 |   59278   49841  1950835    39.1 | 32.881 % |
c |     60381 |  133603   391104 |   65206   50178  1970431    39.3 | 32.881 % |
c |     60887 |  133603   391104 |   71727   50684  2021061    39.9 | 32.881 % |
c |     61646 |  133603   391104 |   78900   51443  2073601    40.3 | 32.881 % |
c |     62787 |  133430   390528 |   86790   52520  2146868    40.9 | 32.930 % |
c ==============================================================================
c [1mFound solution: 13213[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935727   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63504 |  133434   390548 |   44478   53237  2182770    41.0 | 32.930 % |
c |     63606 |  133434   390548 |   48925   53339  2187046    41.0 | 32.931 % |
c |     63759 |  132459   388290 |   53818   53478  2190761    41.0 | 33.357 % |
c |     63984 |  132459   388290 |   59200   53703  2205224    41.1 | 33.357 % |
c |     64322 |  132459   388290 |   65120   54041  2218674    41.1 | 33.357 % |
c |     64828 |  132372   387993 |   71632   54514  2257576    41.4 | 33.381 % |
c ==============================================================================
c [1mFound solution: 13197[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935743   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65511 |  132374   388002 |   44124   55197  2309638    41.8 | 33.381 % |
c |     65612 |  132374   388002 |   48536   55298  2318514    41.9 | 33.382 % |
c |     65765 |  132301   387832 |   53390   55450  2329732    42.0 | 33.422 % |
c |     65991 |  132089   386777 |   58729   55575  2346163    42.2 | 33.471 % |
c |     66329 |  132089   386777 |   64601   55913  2370159    42.4 | 33.471 % |
c |     66836 |  132089   386777 |   71062   56420  2401390    42.6 | 33.471 % |
c |     67595 |  132089   386777 |   78168   57179  2452580    42.9 | 33.471 % |
c ==============================================================================
c [1mFound solution: 13181[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935759   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67914 |  132091   386786 |   44030   57498  2473575    43.0 | 33.471 % |
c |     68017 |  132091   386786 |   48433   57601  2483257    43.1 | 33.471 % |
c ==============================================================================
c [1mFound solution: 13133[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2935807   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68039 |  132092   386789 |   44030   57623  2484317    43.1 | 33.471 % |
c |     68142 |  132092   386789 |   48433   57726  2489779    43.1 | 33.472 % |
c |     68294 |  132092   386789 |   53276   57878  2497748    43.2 | 33.472 % |
c |     68519 |  132092   386789 |   58603   58103  2518881    43.4 | 33.472 % |
c |     68857 |  132092   386789 |   64464   58441  2547557    43.6 | 33.472 % |
c |     69363 |  132092   386789 |   70910   58947  2575924    43.7 | 33.472 % |
c |     70123 |  132092   386789 |   78001   59707  2646757    44.3 | 33.472 % |
c |     71268 |  132092   386789 |   85802   60852  2746322    45.1 | 33.472 % |
c |     72980 |  132014   386608 |   94382   62561  2856226    45.7 | 33.508 % |
c |     75547 |  131967   386500 |  103820   65125  3016467    46.3 | 33.529 % |
c |     79395 |  131933   386424 |  114202   68971  3280608    47.6 | 33.546 % |
c |     85163 |  131886   386316 |  125622   74737  3739707    50.0 | 33.574 % |
c ==============================================================================
c [1mFound solution: 12549[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936391   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86975 |  131892   386342 |   43964   76549  3888717    50.8 | 33.574 % |
c |     87077 |  131892   386342 |   48360   17899  1005458    56.2 | 33.575 % |
c |     87228 |  131892   386342 |   53196   18050  1017360    56.4 | 33.575 % |
c |     87454 |  131892   386342 |   58516   18276  1033578    56.6 | 33.575 % |
c |     87792 |  131818   386176 |   64367   18612  1053032    56.6 | 33.609 % |
c |     88305 |  131453   385328 |   70804   19115  1074763    56.2 | 33.766 % |
c |     89066 |  131453   385328 |   77884   19876  1105354    55.6 | 33.766 % |
c |     90209 |  131309   385000 |   85673   21013  1148285    54.6 | 33.826 % |
c |     91917 |  130977   384240 |   94240   22703  1263228    55.6 | 33.969 % |
c |     94479 |  130977   384240 |  103664   25265  1408074    55.7 | 33.969 % |
c |     98330 |  130943   384162 |  114031   29115  1676019    57.6 | 33.985 % |
c |    104096 |  128222   377666 |  125434   34848  2075839    59.6 | 35.279 % |
c ==============================================================================
c [1mFound solution: 12525[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936415   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    105518 |  128175   377561 |   42725   36267  2116251    58.4 | 35.279 % |
c |    105619 |  128175   377561 |   46997   36368  2122497    58.4 | 35.302 % |
c |    105770 |  128175   377561 |   51697   36519  2131448    58.4 | 35.302 % |
c |    105995 |  128175   377561 |   56866   36744  2144647    58.4 | 35.302 % |
c |    106334 |  128175   377561 |   62553   37083  2168196    58.5 | 35.302 % |
c ==============================================================================
c [1mFound solution: 12509[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936431   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    106798 |  128177   377570 |   42725   37547  2208423    58.8 | 35.302 % |
c |    106898 |  128177   377570 |   46997   37647  2213121    58.8 | 35.302 % |
c |    107048 |  128177   377570 |   51697   37797  2220465    58.7 | 35.302 % |
c ==============================================================================
c [1mFound solution: 12501[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936439   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107114 |  128179   377581 |   42726   37863  2223220    58.7 | 35.302 % |
c ==============================================================================
c [1mFound solution: 12493[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936447   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107193 |  128181   377587 |   42727   37942  2227981    58.7 | 35.302 % |
c |    107294 |  128181   377587 |   46999   38043  2233198    58.7 | 35.303 % |
c |    107445 |  128158   377534 |   51699   38193  2243925    58.8 | 35.314 % |
c |    107671 |  128158   377534 |   56869   38419  2256031    58.7 | 35.314 % |
c |    108008 |  128158   377534 |   62556   38756  2281037    58.9 | 35.314 % |
c |    108518 |  128158   377534 |   68812   39266  2315916    59.0 | 35.314 % |
c |    109280 |  128158   377534 |   75693   40028  2369942    59.2 | 35.314 % |
c |    110420 |  128158   377534 |   83262   41168  2455008    59.6 | 35.314 % |
c ==============================================================================
c [1mFound solution: 12349[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936591   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    110792 |  128156   377535 |   42718   41539  2478960    59.7 | 35.314 % |
c ==============================================================================
c [1mFound solution: 12337[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936603   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    110869 |  128160   377563 |   42720   41616  2482655    59.7 | 35.314 % |
c |    110969 |  128160   377563 |   46992   41716  2490451    59.7 | 35.318 % |
c |    111119 |  128160   377563 |   51691   41866  2500229    59.7 | 35.318 % |
c |    111353 |  128160   377563 |   56860   42100  2512211    59.7 | 35.318 % |
c ==============================================================================
c [1mFound solution: 12333[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936607   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111360 |  128162   377570 |   42720   42107  2512236    59.7 | 35.318 % |
c ==============================================================================
c [1mFound solution: 12325[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936615   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111376 |  128164   377583 |   42721   42123  2512536    59.6 | 35.318 % |
c ==============================================================================
c [1mFound solution: 12319[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936621   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111385 |  128167   377611 |   42722   42132  2512808    59.6 | 35.318 % |
c ==============================================================================
c [1mFound solution: 12317[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936623   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111411 |  128169   377621 |   42723   42158  2512933    59.6 | 35.318 % |
c |    111514 |  128169   377621 |   46995   42261  2518541    59.6 | 35.321 % |
c ==============================================================================
c [1mFound solution: 12313[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936627   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111555 |  128171   377636 |   42723   42302  2520040    59.6 | 35.321 % |
c |    111657 |  128171   377636 |   46995   42404  2524669    59.5 | 35.321 % |
c ==============================================================================
c [1mFound solution: 12309[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936631   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111692 |  128173   377647 |   42724   42439  2526829    59.5 | 35.321 % |
c |    111794 |  128173   377647 |   46996   42541  2530971    59.5 | 35.322 % |
c |    111947 |  128166   377630 |   51696   42688  2538962    59.5 | 35.326 % |
c |    112174 |  128166   377630 |   56865   42915  2557545    59.6 | 35.326 % |
c |    112511 |  128043   377347 |   62552   43248  2579391    59.6 | 35.387 % |
c |    113017 |  127943   377104 |   68807   43752  2619003    59.9 | 35.426 % |
c |    113778 |  127912   377032 |   75688   44511  2680939    60.2 | 35.437 % |
c ==============================================================================
c [1mFound solution: 12305[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936635   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    114479 |  127914   377045 |   42638   45212  2733655    60.5 | 35.437 % |
c |    114579 |  127914   377045 |   46901   45312  2734774    60.4 | 35.438 % |
c |    114730 |  127892   376992 |   51591   45461  2743562    60.3 | 35.445 % |
c |    114956 |  127892   376992 |   56751   45687  2752152    60.2 | 35.445 % |
c |    115293 |  127790   376758 |   62426   46023  2769581    60.2 | 35.486 % |
c |    115802 |  127765   376699 |   68668   46530  2792986    60.0 | 35.498 % |
c |    116562 |  127765   376699 |   75535   47290  2845986    60.2 | 35.498 % |
c |    117701 |  127765   376699 |   83089   48429  2932223    60.5 | 35.498 % |
c |    119409 |  127628   376363 |   91398   50131  3015411    60.2 | 35.559 % |
c ==============================================================================
c [1mFound solution: 12303[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936637   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    120124 |  127630   376379 |   42543   50846  3079047    60.6 | 35.559 % |
c |    120224 |  127630   376379 |   46797   50946  3086663    60.6 | 35.559 % |
c |    120376 |  127630   376379 |   51477   51098  3091151    60.5 | 35.559 % |
c |    120601 |  127630   376379 |   56624   51323  3106957    60.5 | 35.559 % |
c |    120942 |  127630   376379 |   62287   51664  3131223    60.6 | 35.559 % |
c |    121448 |  127630   376379 |   68515   52170  3173238    60.8 | 35.559 % |
c |    122208 |  127630   376379 |   75367   52930  3225385    60.9 | 35.559 % |
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 |    122546 |  127632   376385 |   42544   53268  3247943    61.0 | 35.559 % |
c |    122646 |  127632   376385 |   46798   53368  3253289    61.0 | 35.560 % |
c |    122798 |  127632   376385 |   51478   53520  3264356    61.0 | 35.560 % |
c |    123029 |  127632   376385 |   56626   53751  3282980    61.1 | 35.560 % |
c |    123366 |  127588   376282 |   62288   54087  3310650    61.2 | 35.579 % |
c ==============================================================================
c [1mFound solution: 12295[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936645   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    123426 |  127592   376313 |   42530   54147  3314221    61.2 | 35.579 % |
c |    123530 |  127592   376313 |   46783   54251  3319651    61.2 | 35.580 % |
c |    123680 |  127592   376313 |   51461   54401  3327607    61.2 | 35.580 % |
c |    123906 |  127592   376313 |   56607   54627  3348142    61.3 | 35.580 % |
c |    124246 |  127592   376313 |   62268   54967  3379088    61.5 | 35.580 % |
c |    124755 |  127592   376313 |   68494   55476  3426981    61.8 | 35.580 % |
c |    125515 |  127592   376313 |   75344   56236  3496362    62.2 | 35.580 % |
c |    126656 |  127524   376156 |   82878   57375  3609044    62.9 | 35.606 % |
c ==============================================================================
c [1mFound solution: 12294[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936646   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    127238 |  127527   376177 |   42509   57957  3676834    63.4 | 35.606 % |
c |    127338 |  127527   376177 |   46759   58057  3684200    63.5 | 35.607 % |
c |    127490 |  127527   376177 |   51435   58209  3691342    63.4 | 35.607 % |
c |    127716 |  127527   376177 |   56579   58435  3700621    63.3 | 35.607 % |
c ==============================================================================
c [1mFound solution: 12291[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936649   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    127762 |  127530   376202 |   42510   58481  3703279    63.3 | 35.607 % |
c |    127862 |  127530   376202 |   46761   58581  3706615    63.3 | 35.609 % |
c |    128015 |  127530   376202 |   51437   58734  3719106    63.3 | 35.609 % |
c |    128247 |  126509   373690 |   56580   58959  3741651    63.5 | 36.132 % |
c |    128586 |  126509   373690 |   62238   59298  3776536    63.7 | 36.132 % |
c |    129093 |  126509   373690 |   68462   59805  3811598    63.7 | 36.132 % |
c |    129852 |  126509   373690 |   75309   60564  3860483    63.7 | 36.132 % |
c ==============================================================================
c [1mFound solution: 12290[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936650   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    129884 |  126510   373705 |   42170   60596  3861422    63.7 | 36.132 % |
c ==============================================================================
c [1mFound solution: 12288[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936652   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    129889 |  126514   373736 |   42171   60601  3861447    63.7 | 36.132 % |
c |    129990 |  126514   373736 |   46388   60702  3869999    63.8 | 36.134 % |
c |    130140 |  126514   373736 |   51026   60852  3881545    63.8 | 36.134 % |
c |    130367 |  126514   373736 |   56129   61079  3890829    63.7 | 36.134 % |
c |    130704 |  126514   373736 |   61742   61416  3907203    63.6 | 36.134 % |
c |    131211 |  126508   373716 |   67916   61913  3949760    63.8 | 36.135 % |
c |    131972 |  126502   373696 |   74708   62669  4002326    63.9 | 36.136 % |
c |    133112 |  126481   373648 |   82179   63808  4068190    63.8 | 36.145 % |
c |    134820 |  126076   372675 |   90397   65514  4207558    64.2 | 36.338 % |
c ==============================================================================
c [1mFound solution: 12269[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936671   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    135212 |  126078   372682 |   42026   65906  4230483    64.2 | 36.338 % |
c |    135315 |  126078   372682 |   46228   66009  4241134    64.3 | 36.339 % |
c |    135467 |  126078   372682 |   50851   66161  4255477    64.3 | 36.339 % |
c |    135693 |  126078   372682 |   55936   66387  4283481    64.5 | 36.339 % |
c |    136031 |  126078   372682 |   61530   66725  4324085    64.8 | 36.339 % |
c |    136542 |  126078   372682 |   67683   67236  4380819    65.2 | 36.339 % |
c |    137301 |  126078   372682 |   74451   67995  4468660    65.7 | 36.339 % |
c |    138444 |  126078   372682 |   81896   69138  4588230    66.4 | 36.339 % |
c |    140155 |  126042   372600 |   90086   70847  4770360    67.3 | 36.355 % |
c |    142717 |  125400   371052 |   99095   73398  4985406    67.9 | 36.649 % |
c |    146566 |  124826   369629 |  109004   77224  5273493    68.3 | 36.926 % |
c ==============================================================================
c [1mFound solution: 12257[0m
c ---[   0]---> Adder-cost: 0   maxlim: 2936683   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    151807 |  124767   369507 |   41589   82464  5583841    67.7 | 36.926 % |
c |    151907 |  124756   369483 |   45747   19966  1059187    53.0 | 36.959 % |
c |    152057 |  124756   369483 |   50322   20116  1064038    52.9 | 36.959 % |
c |    152282 |  124756   369483 |   55354   20341  1076334    52.9 | 36.959 % |
c |    152620 |  124756   369483 |   60890   20679  1094975    53.0 | 36.959 % |
c |    153130 |  124756   369483 |   66979   21189  1127442    53.2 | 36.959 % |
c |    153889 |  124756   369483 |   73677   21948  1167984    53.2 | 36.959 % |
c |    155028 |  122484   364069 |   81045   23071  1204807    52.2 | 38.032 % |
c |    156738 |  122466   364027 |   89149   24780  1282660    51.8 | 38.042 % |
c |    159304 |  122310   363653 |   98064   27343  1445954    52.9 | 38.107 % |
c |    163148 |  122273   363567 |  107871   31185  1620732    52.0 | 38.127 % |
c |    168914 |  121935   362773 |  118658   36939  2007753    54.4 | 38.290 % |
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 |    176573 |  121654   362120 |   40551   44593  2491953    55.9 | 38.290 % |
c |    176673 |  121651   362114 |   44606   44692  2495905    55.8 | 38.425 % |
c |    176826 |  121651   362114 |   49066   44845  2503475    55.8 | 38.425 % |
c |    177051 |  121651   362114 |   53973   45070  2514771    55.8 | 38.425 % |
c |    177391 |  121579   361949 |   59370   45408  2535554    55.8 | 38.458 % |
c |    177897 |  121540   361858 |   65307   45913  2557034    55.7 | 38.476 % |
c |    178656 |  121454   361655 |   71838   46666  2596713    55.6 | 38.518 % |
c |    179795 |  121454   361655 |   79022   47805  2686991    56.2 | 38.518 % |
c |    181504 |  121425   361586 |   86924   49510  2831186    57.2 | 38.533 % |
c |    184066 |  120919   360284 |   95617   52071  2995631    57.5 | 38.790 % |
c |    187920 |  120867   360164 |  105178   55924  3236043    57.9 | 38.815 % |
c |    193691 |  120790   359984 |  115696   61692  3625562    58.8 | 38.849 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 16561 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.92 0.95 0.95 2/54 16557
Raw data (stat): 16557 (runsolver) R 16556 1269 1268 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783643081 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.93 0.96 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0022 s]
Raw data (loadavg): 0.94 0.96 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.96 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.96 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0018 s]
Raw data (loadavg): 0.96 0.96 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0021 s]
Raw data (loadavg): 0.97 0.96 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0018 s]
Raw data (loadavg): 0.97 0.96 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0072 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0071 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.007 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.008 s]
Raw data (loadavg): 0.98 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 16561
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.029 s]
Raw data (loadavg): 1.07 0.99 0.96 3/58 16601
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.029 s]
Raw data (loadavg): 1.06 0.99 0.96 2/55 16614
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.029 s]
Raw data (loadavg): 1.05 0.99 0.96 2/55 16614
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.03 s]
Raw data (loadavg): 1.04 0.99 0.96 2/55 16614
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.03 s]
Raw data (loadavg): 1.04 0.99 0.96 2/55 16614
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.03 s]
Raw data (loadavg): 1.03 0.99 0.96 2/55 16614
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.03 s]
Raw data (loadavg): 1.03 0.99 0.96 2/55 16614
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.03 s]
Raw data (loadavg): 1.09 1.00 0.96 2/55 16614
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.03 s]
Raw data (loadavg): 1.08 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.03 s]
Raw data (loadavg): 1.07 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.03 s]
Raw data (loadavg): 1.06 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.03 s]
Raw data (loadavg): 1.05 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.03 s]
Raw data (loadavg): 1.04 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.03 s]
Raw data (loadavg): 1.03 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.03 s]
Raw data (loadavg): 1.03 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.03 s]
Raw data (loadavg): 1.02 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.03 s]
Raw data (loadavg): 1.02 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.03 s]
Raw data (loadavg): 1.02 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.73 s]
Raw data (loadavg): 1.00 1.00 0.96 1/53 16616
Raw data (stat): 16557 (minisat+_script) S 16556 1269 1268 0 -1 0 274 239 0 0 0 0 0 0 20 0 1 0 783643081 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

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