Instance	Runtime	Result
normalized-3col-left3reg-l070-r069-n1.opb	16.372	UNSATISFIABLE
normalized-3col-left3reg-l030-r029-n1.opb	0.987331	UNSATISFIABLE
normalized-3col-almost3reg-l080-r079-n1.opb	1798.762	UNKNOWN
normalized-3col-almost3reg-l030-r029-n1.opb	7.60388	UNSATISFIABLE
normalized-3col-left3reg-l040-r039-n1.opb	1.37444	UNSATISFIABLE
normalized-3col-almost3reg-l070-r069-n1.opb	1798.736	UNKNOWN
normalized-3col-left3reg-l100-r099-n1.opb	23.2568	UNSATISFIABLE
normalized-3col-almost3reg-l060-r059-n1.opb	1773.91	UNSATISFIABLE
normalized-3col-almost3reg-l010-r009-n1.opb	0.105718	UNSATISFIABLE
normalized-3col-almost3reg-l040-r039-n1.opb	16.3732	UNSATISFIABLE
normalized-3col-almost3reg-l090-r089-n1.opb	1798.746	UNKNOWN
normalized-3col-left3reg-l050-r049-n1.opb	5.84067	UNSATISFIABLE
normalized-3col-almost3reg-l015-r014-n1.opb	0.267266	UNSATISFIABLE
normalized-3col-almost3reg-l065-r064-n1.opb	1800.467	UNKNOWN
normalized-3col-left3reg-l080-r079-n1.opb	34.3509	UNSATISFIABLE
normalized-3col-almost3reg-l020-r019-n1.opb	0.474734	UNSATISFIABLE
normalized-3col-almost3reg-l055-r054-n1.opb	1798.779	UNKNOWN
normalized-3col-left3reg-l060-r059-n1.opb	16.1272	UNSATISFIABLE
normalized-3col-almost3reg-l050-r049-n1.opb	496.231	UNSATISFIABLE
normalized-3col-almost3reg-l100-r099-n1.opb	1798.734	UNKNOWN
normalized-3col-left3reg-l010-r010-n1.opb	0.079835	UNSATISFIABLE
normalized-3col-left3reg-l090-r089-n1.opb	75.2701	UNSATISFIABLE
normalized-3col-almost3reg-l045-r044-n1.opb	32.9681	UNSATISFIABLE
normalized-3col-almost3reg-l025-r024-n1.opb	1.01882	UNSATISFIABLE
normalized-3col-left3reg-l020-r019-n1.opb	0.419419	UNSATISFIABLE
normalized-3col-almost3reg-l035-r034-n1.opb	6.20366	UNSATISFIABLE
normalized-subsetcard-eq-fixedbandwidth-60.opb	1798.695	UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-25.opb	1798.777	UNKNOWN
normalized-subsetcard-geq-random4regular-75.opb	1798.727	UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-60.opb	1798.753	UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-65.opb	1798.779	UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-15.opb	45.7602	UNSATISFIABLE
normalized-subsetcard-eq-random4regular-35.opb	1798.764	UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-15.opb	35.9063	UNSATISFIABLE
normalized-subsetcard-eq-fixedbandwidth-35.opb	1798.768	UNKNOWN
normalized-subsetcard-eq-random4regular-55.opb	1798.739	UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-70.opb	1800.463	UNKNOWN
normalized-subsetcard-eq-random4regular-75.opb	1798.788	UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-30.opb	1798.749	UNKNOWN
normalized-subsetcard-eq-random4regular-50.opb	1798.749	UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-25.opb	1798.744	UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-45.opb	1798.752	UNKNOWN
normalized-subsetcard-geq-random4regular-35.opb	1798.758	UNKNOWN
normalized-subsetcard-eq-random4regular-20.opb	53.6325	UNSATISFIABLE
normalized-subsetcard-geq-random4regular-60.opb	1798.747	UNKNOWN
normalized-subsetcard-eq-random4regular-70.opb	1798.740	UNKNOWN
normalized-subsetcard-geq-random4regular-65.opb	1798.755	UNKNOWN
normalized-subsetcard-geq-random4regular-15.opb	3.97545	UNSATISFIABLE
normalized-subsetcard-eq-fixedbandwidth-80.opb	1798.756	UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-70.opb	1798.744	UNKNOWN
normalized-subsetcard-eq-random4regular-30.opb	1798.749	UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-80.opb	1798.789	UNKNOWN
normalized-subsetcard-eq-random4regular-25.opb	988.079	UNSATISFIABLE
normalized-subsetcard-geq-random4regular-80.opb	1800.466	UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-40.opb	1798.769	UNKNOWN
normalized-subsetcard-geq-random4regular-70.opb	1798.759	UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-35.opb	1798.766	UNKNOWN
normalized-subsetcard-eq-random4regular-40.opb	1798.760	UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-65.opb	1798.756	UNKNOWN
normalized-subsetcard-eq-random4regular-45.opb	1798.753	UNKNOWN
normalized-subsetcard-eq-random4regular-80.opb	1800.470	UNKNOWN
normalized-subsetcard-geq-random4regular-20.opb	59.7983	UNSATISFIABLE
normalized-subsetcard-eq-random4regular-65.opb	1798.740	UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-30.opb	1798.757	UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-50.opb	1798.752	UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-50.opb	1798.744	UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-45.opb	1798.725	UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-75.opb	1798.645	UNKNOWN
normalized-subsetcard-geq-random4regular-40.opb	1798.768	UNKNOWN
normalized-subsetcard-eq-random4regular-15.opb	5.16005	UNSATISFIABLE
normalized-subsetcard-eq-fixedbandwidth-55.opb	1798.729	UNKNOWN
normalized-subsetcard-geq-random4regular-55.opb	1798.750	UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-75.opb	1798.746	UNKNOWN
normalized-subsetcard-geq-random4regular-50.opb	1798.723	UNKNOWN
normalized-subsetcard-geq-random4regular-25.opb	1582.02	UNSATISFIABLE
normalized-subsetcard-geq-fixedbandwidth-20.opb	1084.92	UNSATISFIABLE
normalized-subsetcard-eq-random4regular-60.opb	1798.758	UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-55.opb	1798.757	UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-20.opb	1798.765	UNKNOWN
normalized-subsetcard-geq-random4regular-30.opb	1798.776	UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-40.opb	1798.731	UNKNOWN
normalized-subsetcard-geq-random4regular-45.opb	1798.765	UNKNOWN
normalized-ECrand6reg-v111-n1.opb	1798.728	UNKNOWN
normalized-ECrand6reg-v101-n1.opb	1798.730	UNKNOWN
normalized-ECrand4regsplit-v110-n1.opb	1800.472	UNKNOWN
normalized-ECrand6reg-v081-n1.opb	1798.758	UNKNOWN
normalized-ECrand6reg-v041-n1.opb	1798.742	UNKNOWN
normalized-ECrand4regsplit-v100-n1.opb	1798.794	UNKNOWN
normalized-ECrand4regsplit-v020-n1.opb	0.168779	UNSATISFIABLE
normalized-ECrand4regsplit-v060-n1.opb	1798.769	UNKNOWN
normalized-ECrand4regsplit-v080-n1.opb	1798.792	UNKNOWN
normalized-ECrand6reg-v051-n1.opb	1798.747	UNKNOWN
normalized-ECrand6reg-v031-n1.opb	1798.759	UNKNOWN
normalized-ECrand4regsplit-v070-n1.opb	1798.764	UNKNOWN
normalized-ECrand4regsplit-v010-n1.opb	0.006655	UNSATISFIABLE
normalized-ECrand4regsplit-v030-n1.opb	1.46482	UNSATISFIABLE
normalized-ECrand6reg-v021-n1.opb	1798.763	UNKNOWN
normalized-ECrand4regsplit-v040-n1.opb	959.895	UNSATISFIABLE
normalized-ECrand6reg-v011-n1.opb	5.94158	UNSATISFIABLE
normalized-ECrand6reg-v061-n1.opb	1798.757	UNKNOWN
normalized-ECrand4regsplit-v050-n1.opb	1798.757	UNKNOWN
normalized-ECrand6reg-v071-n1.opb	1798.708	UNKNOWN
normalized-ECrand6reg-v091-n1.opb	1798.730	UNKNOWN
normalized-ECrand4regsplit-v090-n1.opb	1798.697	UNKNOWN
normalized-ECgrid5x130split.opb	1800.457	UNKNOWN
normalized-ECgrid3x70split.opb	42.6665	UNSATISFIABLE
normalized-ECgrid5x150split.opb	1798.722	UNKNOWN
normalized-ECgrid3x20split.opb	2.56118	UNSATISFIABLE
normalized-ECgrid5x30split.opb	1798.760	UNKNOWN
normalized-ECgrid5x120split.opb	1798.594	UNKNOWN
normalized-ECgrid5x50split.opb	1798.603	UNKNOWN
normalized-ECgrid5x10split.opb	222.959	UNSATISFIABLE
normalized-ECgrid3x40split.opb	14.5719	UNSATISFIABLE
normalized-ECgrid5x140split.opb	1798.748	UNKNOWN
normalized-ECgrid5x70split.opb	1798.738	UNKNOWN
normalized-ECgrid3x80split.opb	51.0999	UNSATISFIABLE
normalized-ECgrid5x90split.opb	1798.751	UNKNOWN
normalized-ECgrid3x100split.opb	54.6508	UNSATISFIABLE
normalized-ECgrid5x100split.opb	1798.774	UNKNOWN
normalized-ECgrid5x80split.opb	1798.728	UNKNOWN
normalized-ECgrid3x10split.opb	0.3847	UNSATISFIABLE
normalized-ECgrid5x40split.opb	1798.749	UNKNOWN
normalized-ECgrid3x60split.opb	28.5053	UNSATISFIABLE
normalized-ECgrid3x30split.opb	9.22318	UNSATISFIABLE
normalized-ECgrid5x20split.opb	1798.739	UNKNOWN
normalized-ECgrid5x60split.opb	1798.767	UNKNOWN
normalized-ECgrid3x90split.opb	85.3207	UNSATISFIABLE
normalized-ECgrid5x110split.opb	1798.725	UNKNOWN
normalized-ECgrid3x50split.opb	31.561	UNSATISFIABLE
normalized-sumineqArity3pyramidP0064.opb	7.65014	UNSATISFIABLE
normalized-sumineqArity4pyramidP0016.opb	0.219746	UNSATISFIABLE
normalized-sumineqArity3pyramidP0016.opb	0.13787	UNSATISFIABLE
normalized-sumineqArity5houseP128.opb	471.938	UNSATISFIABLE
normalized-sumineqArity4pyramidP0064.opb	26.9935	UNSATISFIABLE
normalized-sumineqArity5pyramidP0032.opb	5.50306	UNSATISFIABLE
normalized-sumineqArity4pyramidP0032.opb	2.60245	UNSATISFIABLE
normalized-sumineqArity5pyramidP0064.opb	33.7996	UNSATISFIABLE
normalized-sumineqArity3houseP016.opb	0.274902	UNSATISFIABLE
normalized-sumineqArity3houseP032.opb	2.29458	UNSATISFIABLE
normalized-sumineqArity4pyramidP0125.opb	191.353	UNSATISFIABLE
normalized-sumineqArity5houseP032.opb	16.6178	UNSATISFIABLE
normalized-sumineqArity3pyramidP0032.opb	0.766999	UNSATISFIABLE
normalized-sumineqArity3houseP128.opb	200.371	UNSATISFIABLE
normalized-sumineqArity4houseP064.opb	63.4252	UNSATISFIABLE
normalized-sumineqArity4houseP128.opb	412.901	UNSATISFIABLE
normalized-sumineqArity3pyramidP0125.opb	54.5289	UNSATISFIABLE
normalized-sumineqArity3houseP064.opb	23.9756	UNSATISFIABLE
normalized-sumineqArity5pyramidP0016.opb	0.642414	UNSATISFIABLE
normalized-sumineqArity5houseP016.opb	1.71084	UNSATISFIABLE
normalized-sumineqArity5houseP064.opb	73.1799	UNSATISFIABLE
normalized-sumineqArity4houseP032.opb	7.08728	UNSATISFIABLE
normalized-sumineqArity5pyramidP0125.opb	173.858	UNSATISFIABLE
normalized-sumineqArity4houseP016.opb	0.652659	UNSATISFIABLE
normalized-vertexcover-grid8x11-hard.opb	0.615114	UNSATISFIABLE
normalized-vertexcover-grid10x29.opb	0.962597	UNSATISFIABLE
normalized-vertexcover-grid8x23-hard.opb	1.77391	UNSATISFIABLE
normalized-vertexcover-grid4x15-hard.opb	0.123269	UNSATISFIABLE
normalized-vertexcover-grid6x11.opb	0.142668	UNSATISFIABLE
normalized-vertexcover-grid8x21-hard.opb	1.60023	UNSATISFIABLE
normalized-vertexcover-grid8x9.opb	0.179444	UNSATISFIABLE
normalized-vertexcover-grid6x19.opb	0.163572	UNSATISFIABLE
normalized-vertexcover-grid6x13-hard.opb	0.322056	UNSATISFIABLE
normalized-vertexcover-completegraph-5.opb	0.000618	UNSATISFIABLE
normalized-vertexcover-grid4x27-hard.opb	0.143546	UNSATISFIABLE
normalized-vertexcover-grid10x15-hard.opb	1.71672	UNSATISFIABLE
normalized-vertexcover-grid6x9.opb	0.078422	UNSATISFIABLE
normalized-vertexcover-grid6x7-hard.opb	0.055883	UNSATISFIABLE
normalized-vertexcover-grid6x25.opb	0.301575	UNSATISFIABLE
normalized-vertexcover-grid4x9-hard.opb	0.029025	UNSATISFIABLE
normalized-vertexcover-grid4x21.opb	0.288045	UNSATISFIABLE
normalized-vertexcover-grid10x23.opb	0.413196	UNSATISFIABLE
normalized-vertexcover-completegraph-17.opb	0.002316	UNSATISFIABLE
normalized-vertexcover-grid4x11.opb	0.04693	UNSATISFIABLE
normalized-vertexcover-completegraph-29.opb	0.007119	UNSATISFIABLE
normalized-vertexcover-grid6x17.opb	0.125851	UNSATISFIABLE
normalized-vertexcover-grid6x7.opb	0.042332	UNSATISFIABLE
normalized-vertexcover-grid4x9.opb	0.027699	UNSATISFIABLE
normalized-vertexcover-grid6x23-hard.opb	0.42545	UNSATISFIABLE
normalized-vertexcover-grid4x23-hard.opb	0.46664	UNSATISFIABLE
normalized-vertexcover-grid10x17-hard.opb	1.89461	UNSATISFIABLE
normalized-vertexcover-grid10x13-hard.opb	1.1453	UNSATISFIABLE
normalized-vertexcover-completegraph-25.opb	0.005151	UNSATISFIABLE
normalized-vertexcover-grid4x23.opb	0.385616	UNSATISFIABLE
normalized-vertexcover-grid6x25-hard.opb	0.563521	UNSATISFIABLE
normalized-vertexcover-completegraph-43.opb	0.014651	UNSATISFIABLE
normalized-vertexcover-grid4x19.opb	0.223763	UNSATISFIABLE
normalized-vertexcover-grid8x17-hard.opb	0.68049	UNSATISFIABLE
normalized-vertexcover-grid10x13.opb	0.198932	UNSATISFIABLE
normalized-vertexcover-grid8x19-hard.opb	1.19576	UNSATISFIABLE
normalized-vertexcover-completegraph-3.opb	0.000492	UNSATISFIABLE
normalized-vertexcover-completegraph-39.opb	0.01152	UNSATISFIABLE
normalized-vertexcover-grid4x11-hard.opb	0.052775	UNSATISFIABLE
normalized-vertexcover-grid10x21-hard.opb	2.84291	UNSATISFIABLE
normalized-vertexcover-grid6x15-hard.opb	0.492251	UNSATISFIABLE
normalized-vertexcover-grid10x27.opb	0.66953	UNSATISFIABLE
normalized-vertexcover-completegraph-9.opb	0.000744	UNSATISFIABLE
normalized-vertexcover-grid6x15.opb	0.362875	UNSATISFIABLE
normalized-vertexcover-grid10x11-hard.opb	0.767414	UNSATISFIABLE
normalized-vertexcover-completegraph-7.opb	0.000515	UNSATISFIABLE
normalized-vertexcover-grid8x9-hard.opb	0.326859	UNSATISFIABLE
normalized-vertexcover-completegraph-47.opb	0.012087	UNSATISFIABLE
normalized-vertexcover-grid6x17-hard.opb	0.229293	UNSATISFIABLE
normalized-vertexcover-grid4x27.opb	0.121643	UNSATISFIABLE
normalized-vertexcover-grid10x17.opb	0.425414	UNSATISFIABLE
normalized-vertexcover-completegraph-41.opb	0.013833	UNSATISFIABLE
normalized-vertexcover-grid4x7-hard.opb	0.018474	UNSATISFIABLE
normalized-vertexcover-grid4x5-hard.opb	0.008937	UNSATISFIABLE
normalized-vertexcover-grid10x11.opb	0.149779	UNSATISFIABLE
normalized-vertexcover-completegraph-19.opb	0.002942	UNSATISFIABLE
normalized-vertexcover-grid4x7.opb	0.014981	UNSATISFIABLE
normalized-vertexcover-grid4x13.opb	0.071803	UNSATISFIABLE
normalized-vertexcover-grid10x19-hard.opb	3.26126	UNSATISFIABLE
normalized-vertexcover-grid10x21.opb	0.331758	UNSATISFIABLE
normalized-vertexcover-grid8x25-hard.opb	2.14135	UNSATISFIABLE
normalized-vertexcover-grid6x23.opb	0.248796	UNSATISFIABLE
normalized-vertexcover-grid4x13-hard.opb	0.079529	UNSATISFIABLE
normalized-vertexcover-grid6x9-hard.opb	0.111651	UNSATISFIABLE
normalized-vertexcover-grid10x25.opb	0.495383	UNSATISFIABLE
normalized-vertexcover-grid8x29-hard.opb	1.37524	UNSATISFIABLE
normalized-vertexcover-grid10x29-hard.opb	6.40385	UNSATISFIABLE
normalized-vertexcover-grid10x25-hard.opb	3.99035	UNSATISFIABLE
normalized-vertexcover-grid4x29-hard.opb	0.180957	UNSATISFIABLE
normalized-vertexcover-grid8x27-hard.opb	1.28901	UNSATISFIABLE
normalized-vertexcover-grid4x25.opb	0.495568	UNSATISFIABLE
normalized-vertexcover-completegraph-51.opb	0.019191	UNSATISFIABLE
normalized-vertexcover-grid6x27.opb	0.378338	UNSATISFIABLE
normalized-vertexcover-completegraph-15.opb	0.001489	UNSATISFIABLE
normalized-vertexcover-grid6x27-hard.opb	0.707038	UNSATISFIABLE
normalized-vertexcover-grid8x15-hard.opb	0.507278	UNSATISFIABLE
normalized-vertexcover-grid4x21-hard.opb	0.350509	UNSATISFIABLE
normalized-vertexcover-grid4x25-hard.opb	0.60053	UNSATISFIABLE
normalized-vertexcover-grid4x17.opb	0.1539	UNSATISFIABLE
normalized-vertexcover-grid8x13-hard.opb	0.354875	UNSATISFIABLE
normalized-vertexcover-grid4x19-hard.opb	0.264208	UNSATISFIABLE
normalized-vertexcover-grid6x21.opb	0.199248	UNSATISFIABLE
normalized-vertexcover-completegraph-35.opb	0.007664	UNSATISFIABLE
normalized-vertexcover-grid4x29.opb	0.1413	UNSATISFIABLE
normalized-vertexcover-grid10x23-hard.opb	2.67734	UNSATISFIABLE
normalized-vertexcover-grid6x19-hard.opb	0.270534	UNSATISFIABLE
normalized-vertexcover-completegraph-27.opb	0.005492	UNSATISFIABLE
normalized-vertexcover-completegraph-45.opb	0.016388	UNSATISFIABLE
normalized-vertexcover-completegraph-49.opb	0.013233	UNSATISFIABLE
normalized-vertexcover-grid6x11-hard.opb	0.190857	UNSATISFIABLE
normalized-vertexcover-grid6x29.opb	0.527779	UNSATISFIABLE
normalized-vertexcover-grid4x5.opb	0.006366	UNSATISFIABLE
normalized-vertexcover-grid6x29-hard.opb	0.966777	UNSATISFIABLE
normalized-vertexcover-grid10x15.opb	0.322485	UNSATISFIABLE
normalized-vertexcover-grid10x27-hard.opb	5.15154	UNSATISFIABLE
normalized-vertexcover-completegraph-11.opb	0.001515	UNSATISFIABLE
normalized-vertexcover-completegraph-33.opb	0.006648	UNSATISFIABLE
normalized-vertexcover-grid6x21-hard.opb	0.334758	UNSATISFIABLE
normalized-vertexcover-completegraph-31.opb	0.006824	UNSATISFIABLE
normalized-vertexcover-grid4x17-hard.opb	0.182566	UNSATISFIABLE
normalized-vertexcover-completegraph-21.opb	0.003468	UNSATISFIABLE
normalized-vertexcover-completegraph-13.opb	0.001773	UNSATISFIABLE
normalized-vertexcover-grid4x15.opb	0.110451	UNSATISFIABLE
normalized-vertexcover-completegraph-23.opb	0.004138	UNSATISFIABLE
normalized-vertexcover-grid10x19.opb	0.658872	UNSATISFIABLE
normalized-vertexcover-completegraph-37.opb	0.007098	UNSATISFIABLE
normalized-vertexcover-grid6x13.opb	0.228144	UNSATISFIABLE
normalized-rand6reg-v071-n2.opb	1798.770	UNKNOWN
normalized-rand6reg-v071-n3.opb	1798.760	UNKNOWN
normalized-rand6reg-v051-n3.opb	1798.745	UNKNOWN
normalized-rand6reg-v061-n3.opb	1800.471	UNKNOWN
normalized-rand6reg-v091-n1.opb	1798.715	UNKNOWN
normalized-rand6reg-v081-n1.opb	1798.742	UNKNOWN
normalized-rand6reg-v041-n2.opb	1798.778	UNKNOWN
normalized-rand6reg-v111-n2.opb	1798.766	UNKNOWN
normalized-rand6reg-v101-n2.opb	1798.747	UNKNOWN
normalized-rand6reg-v081-n2.opb	1798.764	UNKNOWN
normalized-rand6reg-v021-n2.opb	1.36048	UNSATISFIABLE
normalized-rand6reg-v021-n1.opb	1.0741	UNSATISFIABLE
normalized-rand6reg-v011-n2.opb	0.011392	UNSATISFIABLE
normalized-rand6reg-v101-n3.opb	1798.796	UNKNOWN
normalized-rand6reg-v051-n2.opb	1798.762	UNKNOWN
normalized-rand6reg-v111-n3.opb	1798.767	UNKNOWN
normalized-rand6reg-v031-n3.opb	90.0883	UNSATISFIABLE
normalized-rand6reg-v061-n2.opb	1798.791	UNKNOWN
normalized-rand6reg-v031-n1.opb	372.468	UNSATISFIABLE
normalized-rand6reg-v041-n1.opb	1798.767	UNKNOWN
normalized-rand6reg-v111-n1.opb	1800.474	UNKNOWN
normalized-rand6reg-v011-n1.opb	0.01798	UNSATISFIABLE
normalized-rand6reg-v091-n2.opb	1798.744	UNKNOWN
normalized-rand6reg-v041-n3.opb	1798.729	UNKNOWN
normalized-rand6reg-v071-n1.opb	1798.750	UNKNOWN
normalized-rand6reg-v061-n1.opb	1798.775	UNKNOWN
normalized-rand6reg-v031-n2.opb	198.8	UNSATISFIABLE
normalized-rand6reg-v021-n3.opb	0.676385	UNSATISFIABLE
normalized-rand6reg-v081-n3.opb	1798.774	UNKNOWN
normalized-rand6reg-v011-n3.opb	0.012799	UNSATISFIABLE
normalized-rand6reg-v101-n1.opb	1798.743	UNKNOWN
normalized-rand6reg-v051-n1.opb	1798.756	UNKNOWN
normalized-rand6reg-v091-n3.opb	1798.741	UNKNOWN
normalized-5_6_8.opb	0.024418	UNSATISFIABLE
normalized-4_7_0.opb	0.000992	UNSATISFIABLE
normalized-4_5_1.opb	0.000745	UNSATISFIABLE
normalized-5_6_23.opb	309.869	UNSATISFIABLE
normalized-5_6_15.opb	1.18316	UNSATISFIABLE
normalized-3_6_0.opb	0.000892	UNSATISFIABLE
normalized-3_5_6.opb	0.007546	UNSATISFIABLE
normalized-5_7_4.opb	0.0058	UNSATISFIABLE
normalized-4_5_8.opb	0.019484	UNSATISFIABLE
normalized-6_6_18.opb	17.4364	UNSATISFIABLE
normalized-2_7_2.opb	0.001188	UNSATISFIABLE
normalized-4_7_4.opb	0.004644	UNSATISFIABLE
normalized-4_5_13.opb	0.079232	UNSATISFIABLE
normalized-5_7_9.opb	0.008079	SATISFIABLE
normalized-6_6_13.opb	0.26224	UNSATISFIABLE
normalized-7_7_3.opb	0.004162	UNSATISFIABLE
normalized-3_4_7.opb	0.005961	UNSATISFIABLE
normalized-7_7_9.opb	0.065059	UNSATISFIABLE
normalized-7_7_11.opb	0.218042	UNSATISFIABLE
normalized-5_6_14.opb	1.0207	UNSATISFIABLE
normalized-7_7_10.opb	0.226798	UNSATISFIABLE
normalized-3_5_5.opb	0.003478	UNSATISFIABLE
normalized-4_6_6.opb	0.013943	UNSATISFIABLE
normalized-7_6_25.opb	601.329	UNSATISFIABLE
normalized-3_7_2.opb	0.001739	UNSATISFIABLE
normalized-2_6_3.opb	0.002012	SATISFIABLE
normalized-6_6_11.opb	0.072545	UNSATISFIABLE
normalized-8_6_29.opb	1798.754	UNKNOWN
normalized-6_6_12.opb	0.266367	UNSATISFIABLE
normalized-2_4_2.opb	0.001089	UNSATISFIABLE
normalized-3_7_0.opb	0.000696	UNSATISFIABLE
normalized-5_6_0.opb	0.00142	UNSATISFIABLE
normalized-5_6_3.opb	0.003021	UNSATISFIABLE
normalized-2_5_3.opb	0.001438	SATISFIABLE
normalized-2_7_0.opb	0.000492	UNSATISFIABLE
normalized-7_7_18.opb	2.38097	SATISFIABLE
normalized-6_6_5.opb	0.004054	UNSATISFIABLE
normalized-4_7_6.opb	0.013576	UNSATISFIABLE
normalized-8_6_20.opb	22.2011	UNSATISFIABLE
normalized-4_6_1.opb	0.001508	UNSATISFIABLE
normalized-4_5_16.opb	0.510435	UNSATISFIABLE
normalized-8_6_28.opb	702.284	UNSATISFIABLE
normalized-3_6_6.opb	0.004064	SATISFIABLE
normalized-6_6_9.opb	0.023506	UNSATISFIABLE
normalized-2_6_1.opb	0.000725	UNSATISFIABLE
normalized-2_7_1.opb	0.000775	UNSATISFIABLE
normalized-5_6_32.opb	1798.747	UNKNOWN
normalized-6_6_34.opb	1798.756	UNKNOWN
normalized-2_4_0.opb	0.00051	UNSATISFIABLE
normalized-4_5_20.opb	2.25524	UNSATISFIABLE
normalized-4_5_3.opb	0.00211	UNSATISFIABLE
normalized-5_6_13.opb	0.308415	UNSATISFIABLE
normalized-7_6_23.opb	285.149	UNSATISFIABLE
normalized-6_6_32.opb	1798.750	UNKNOWN
normalized-5_6_35.opb	1798.740	UNKNOWN
normalized-7_7_1.opb	0.002346	UNSATISFIABLE
normalized-3_5_9.opb	0.017751	UNSATISFIABLE
normalized-8_6_23.opb	115.522	UNSATISFIABLE
normalized-4_5_0.opb	0.001018	UNSATISFIABLE
normalized-5_6_28.opb	1798.765	UNKNOWN
normalized-5_6_36.opb	1798.746	UNKNOWN
normalized-2_3_2.opb	0.001158	UNSATISFIABLE
normalized-5_6_34.opb	1798.747	UNKNOWN
normalized-4_6_5.opb	0.006031	UNSATISFIABLE
normalized-4_5_28.opb	21.6662	UNSATISFIABLE
normalized-7_6_28.opb	1800.469	UNKNOWN
normalized-7_6_27.opb	1685.36	UNSATISFIABLE
normalized-3_4_13.opb	0.020546	UNSATISFIABLE
normalized-4_5_21.opb	1.99344	UNSATISFIABLE
normalized-5_6_19.opb	17.7368	UNSATISFIABLE
normalized-3_6_2.opb	0.00171	UNSATISFIABLE
normalized-3_4_9.opb	0.008583	UNSATISFIABLE
normalized-5_6_2.opb	0.002368	UNSATISFIABLE
normalized-8_7_19.opb	270.764	UNSATISFIABLE
normalized-5_7_1.opb	0.002226	UNSATISFIABLE
normalized-6_6_16.opb	4.76568	UNSATISFIABLE
normalized-3_4_11.opb	0.014079	UNSATISFIABLE
normalized-3_5_3.opb	0.001709	UNSATISFIABLE
normalized-6_6_14.opb	1.06153	UNSATISFIABLE
normalized-4_5_2.opb	0.001698	UNSATISFIABLE
normalized-2_6_0.opb	0.000471	UNSATISFIABLE
normalized-3_4_6.opb	0.005577	UNSATISFIABLE
normalized-2_3_5.opb	0.002643	UNSATISFIABLE
normalized-4_7_7.opb	0.01167	SATISFIABLE
normalized-7_7_6.opb	0.019183	UNSATISFIABLE
normalized-5_6_17.opb	4.35009	UNSATISFIABLE
normalized-6_6_31.opb	1798.761	UNKNOWN
normalized-7_6_26.opb	572.086	UNSATISFIABLE
normalized-2_3_1.opb	0.000635	UNSATISFIABLE
normalized-3_5_11.opb	0.029338	UNSATISFIABLE
normalized-5_6_6.opb	0.015717	UNSATISFIABLE
normalized-2_4_4.opb	0.002205	UNSATISFIABLE
normalized-7_7_12.opb	1.05504	UNSATISFIABLE
normalized-4_6_3.opb	0.002177	UNSATISFIABLE
normalized-4_7_1.opb	0.001518	UNSATISFIABLE
normalized-5_6_29.opb	1798.777	UNKNOWN
normalized-7_6_21.opb	37.7154	UNSATISFIABLE
normalized-7_6_19.opb	11.8092	UNSATISFIABLE
normalized-3_7_4.opb	0.002884	SATISFIABLE
normalized-4_5_24.opb	8.18658	UNSATISFIABLE
normalized-5_6_18.opb	22.0341	UNSATISFIABLE
normalized-4_5_22.opb	4.22068	UNSATISFIABLE
normalized-5_6_27.opb	1798.729	UNKNOWN
normalized-2_3_4.opb	0.002063	UNSATISFIABLE
normalized-8_6_25.opb	351.353	UNSATISFIABLE
normalized-6_6_6.opb	0.006909	UNSATISFIABLE
normalized-2_4_6.opb	0.003673	SATISFIABLE
normalized-3_7_3.opb	0.002938	UNSATISFIABLE
normalized-8_6_18.opb	11.2001	UNSATISFIABLE
normalized-4_5_5.opb	0.004957	UNSATISFIABLE
normalized-6_6_4.opb	0.002998	UNSATISFIABLE
normalized-7_7_14.opb	8.2975	UNSATISFIABLE
normalized-6_6_2.opb	0.002727	UNSATISFIABLE
normalized-3_5_1.opb	0.00104	UNSATISFIABLE
normalized-3_5_4.opb	0.002597	UNSATISFIABLE
normalized-2_7_3.opb	0.002074	SATISFIABLE
normalized-3_4_5.opb	0.003802	UNSATISFIABLE
normalized-8_6_19.opb	5.73974	UNSATISFIABLE
normalized-7_7_7.opb	0.02272	UNSATISFIABLE
normalized-8_6_22.opb	131.203	UNSATISFIABLE
normalized-4_5_9.opb	0.016946	UNSATISFIABLE
normalized-5_6_10.opb	0.08462	UNSATISFIABLE
normalized-5_6_20.opb	104.622	UNSATISFIABLE
normalized-5_6_26.opb	1800.470	UNKNOWN
normalized-7_6_18.opb	16.0578	UNSATISFIABLE
normalized-4_5_7.opb	0.012197	UNSATISFIABLE
normalized-7_6_22.opb	137.86	UNSATISFIABLE
normalized-5_6_33.opb	1798.723	UNKNOWN
normalized-4_5_27.opb	13.1359	UNSATISFIABLE
normalized-5_6_37.opb	1798.755	UNKNOWN
normalized-6_6_21.opb	65.4124	UNSATISFIABLE
normalized-5_7_0.opb	0.001727	UNSATISFIABLE
normalized-6_6_33.opb	1798.775	UNKNOWN
normalized-5_6_24.opb	1537.07	UNSATISFIABLE
normalized-8_7_18.opb	77.6661	UNSATISFIABLE
normalized-6_6_23.opb	213.114	UNSATISFIABLE
normalized-6_6_30.opb	1798.764	UNKNOWN
normalized-8_7_20.opb	0.658896	SATISFIABLE
normalized-6_6_8.opb	0.024136	UNSATISFIABLE
normalized-3_4_3.opb	0.00171	UNSATISFIABLE
normalized-4_7_5.opb	0.006482	UNSATISFIABLE
normalized-4_5_23.opb	3.48961	UNSATISFIABLE
normalized-2_3_6.opb	0.003751	UNSATISFIABLE
normalized-6_6_22.opb	223.824	UNSATISFIABLE
normalized-3_5_2.opb	0.001297	UNSATISFIABLE
normalized-7_7_13.opb	1.10681	UNSATISFIABLE
normalized-7_7_5.opb	0.007176	UNSATISFIABLE
normalized-2_3_3.opb	0.001012	UNSATISFIABLE
normalized-4_5_17.opb	0.398315	UNSATISFIABLE
normalized-3_6_3.opb	0.002198	UNSATISFIABLE
normalized-4_5_11.opb	0.033186	UNSATISFIABLE
normalized-6_6_10.opb	0.059175	UNSATISFIABLE
normalized-7_7_4.opb	0.008398	UNSATISFIABLE
normalized-4_5_4.opb	0.004099	UNSATISFIABLE
normalized-7_6_20.opb	53.8578	UNSATISFIABLE
normalized-4_5_10.opb	0.032708	UNSATISFIABLE
normalized-4_5_12.opb	0.078431	UNSATISFIABLE
normalized-5_6_22.opb	524.905	UNSATISFIABLE
normalized-4_6_4.opb	0.004564	UNSATISFIABLE
normalized-7_6_30.opb	1798.709	UNKNOWN
normalized-4_5_6.opb	0.009122	UNSATISFIABLE
normalized-5_6_5.opb	0.00685	UNSATISFIABLE
normalized-3_4_4.opb	0.00311	UNSATISFIABLE
normalized-4_5_26.opb	17.1456	UNSATISFIABLE
normalized-6_6_7.opb	0.009152	UNSATISFIABLE
normalized-7_7_0.opb	0.001807	UNSATISFIABLE
normalized-5_7_5.opb	0.007278	UNSATISFIABLE
normalized-7_7_8.opb	0.046885	UNSATISFIABLE
normalized-2_4_1.opb	0.000758	UNSATISFIABLE
normalized-5_7_7.opb	0.016849	UNSATISFIABLE
normalized-5_6_31.opb	1798.788	UNKNOWN
normalized-3_6_1.opb	0.001076	UNSATISFIABLE
normalized-8_6_30.opb	1639.19	UNSATISFIABLE
normalized-2_6_2.opb	0.00124	UNSATISFIABLE
normalized-7_6_29.opb	1680.32	UNSATISFIABLE
normalized-2_3_0.opb	0.000695	UNSATISFIABLE
normalized-4_6_2.opb	0.001676	UNSATISFIABLE
normalized-5_6_25.opb	1426.59	UNSATISFIABLE
normalized-2_5_0.opb	0.00048	UNSATISFIABLE
normalized-3_5_8.opb	0.015776	UNSATISFIABLE
normalized-4_5_19.opb	0.947308	UNSATISFIABLE
normalized-7_7_15.opb	6.12509	UNSATISFIABLE
normalized-3_4_12.opb	0.021164	UNSATISFIABLE
normalized-5_6_9.opb	0.029008	UNSATISFIABLE
normalized-3_6_4.opb	0.003611	UNSATISFIABLE
normalized-4_5_18.opb	0.991742	UNSATISFIABLE
normalized-3_5_7.opb	0.007487	UNSATISFIABLE
normalized-6_6_3.opb	0.001806	UNSATISFIABLE
normalized-2_5_1.opb	0.000752	UNSATISFIABLE
normalized-5_6_21.opb	107.772	UNSATISFIABLE
normalized-8_6_21.opb	25.5481	UNSATISFIABLE
normalized-6_6_17.opb	3.21687	UNSATISFIABLE
normalized-7_7_16.opb	37.6564	UNSATISFIABLE
normalized-5_6_7.opb	0.013867	UNSATISFIABLE
normalized-4_6_0.opb	0.001006	UNSATISFIABLE
normalized-5_6_16.opb	4.39713	UNSATISFIABLE
normalized-4_6_8.opb	0.009371	SATISFIABLE
normalized-4_5_14.opb	0.182198	UNSATISFIABLE
normalized-3_4_8.opb	0.011243	UNSATISFIABLE
normalized-6_6_19.opb	15.7774	UNSATISFIABLE
normalized-3_5_12.opb	0.006382	SATISFIABLE
normalized-3_5_10.opb	0.030334	UNSATISFIABLE
normalized-3_7_1.opb	0.001307	UNSATISFIABLE
normalized-4_7_3.opb	0.002521	UNSATISFIABLE
normalized-2_5_2.opb	0.001203	UNSATISFIABLE
normalized-2_4_3.opb	0.001301	UNSATISFIABLE
normalized-6_6_15.opb	0.986621	UNSATISFIABLE
normalized-5_6_11.opb	0.080297	UNSATISFIABLE
normalized-5_7_2.opb	0.002166	UNSATISFIABLE
normalized-4_7_2.opb	0.00241	UNSATISFIABLE
normalized-5_7_3.opb	0.001756	UNSATISFIABLE
normalized-5_6_38.opb	1798.739	UNKNOWN
normalized-5_6_4.opb	0.004903	UNSATISFIABLE
normalized-4_5_25.opb	6.28591	UNSATISFIABLE
normalized-5_6_1.opb	0.001482	UNSATISFIABLE
normalized-3_5_0.opb	0.000738	UNSATISFIABLE
normalized-4_5_15.opb	0.196235	UNSATISFIABLE
normalized-5_7_6.opb	0.01171	UNSATISFIABLE
normalized-3_4_10.opb	0.015003	UNSATISFIABLE
normalized-3_6_5.opb	0.004874	UNSATISFIABLE
normalized-2_4_5.opb	0.001799	UNSATISFIABLE
normalized-4_6_7.opb	0.014181	UNSATISFIABLE
normalized-5_7_8.opb	0.055606	UNSATISFIABLE
normalized-8_6_26.opb	817.8	UNSATISFIABLE
normalized-3_4_0.opb	0.00072	UNSATISFIABLE
normalized-6_6_20.opb	102.987	UNSATISFIABLE
normalized-7_6_24.opb	300.015	UNSATISFIABLE
normalized-3_4_1.opb	0.000668	UNSATISFIABLE
normalized-5_6_30.opb	1798.754	UNKNOWN
normalized-7_7_2.opb	0.003335	UNSATISFIABLE
normalized-8_6_24.opb	203.8	UNSATISFIABLE
normalized-8_6_27.opb	1587.97	UNSATISFIABLE
normalized-3_4_2.opb	0.001472	UNSATISFIABLE
normalized-5_6_12.opb	0.255553	UNSATISFIABLE
normalized-compression16_3.opb	0.0166	UNSATISFIABLE
normalized-compression8_15.opb	0.074342	SATISFIABLE
normalized-compression32_7.opb	3.79913	UNSATISFIABLE
normalized-compression8_19.opb	0.606502	SATISFIABLE
normalized-compression64_26.opb	3.1845	SATISFIABLE
normalized-compression64_10.opb	1800.460	UNKNOWN
normalized-compression64_24.opb	345.627	SATISFIABLE
normalized-compression32_14.opb	1798.712	UNKNOWN
normalized-compression16_5.opb	0.033855	UNSATISFIABLE
normalized-compression32_5.opb	0.230617	UNSATISFIABLE
normalized-compression32_11.opb	1798.770	UNKNOWN
normalized-compression64_9.opb	1798.773	UNKNOWN
normalized-compression64_14.opb	1798.709	UNKNOWN
normalized-compression16_6.opb	0.080481	UNSATISFIABLE
normalized-compression16_13.opb	0.069478	SATISFIABLE
normalized-compression16_11.opb	55.5491	SATISFIABLE
normalized-compression32_12.opb	1798.762	UNKNOWN
normalized-compression32_9.opb	79.5794	UNSATISFIABLE
normalized-compression32_13.opb	1798.758	UNKNOWN
normalized-compression16_12.opb	7.43682	SATISFIABLE
normalized-compression64_8.opb	359.158	UNSATISFIABLE
normalized-compression32_17.opb	36.6442	SATISFIABLE
normalized-compression32_18.opb	0.577674	SATISFIABLE
normalized-compression64_3.opb	0.27645	UNSATISFIABLE
normalized-compression64_11.opb	1798.696	UNKNOWN
normalized-compression16_15.opb	0.041935	SATISFIABLE
normalized-compression64_5.opb	2.27137	UNSATISFIABLE
normalized-compression64_12.opb	1798.714	UNKNOWN
normalized-compression32_6.opb	0.626535	UNSATISFIABLE
normalized-compression32_15.opb	854.303	SATISFIABLE
normalized-compression64_28.opb	1.44724	SATISFIABLE
normalized-compression64_20.opb	1798.716	UNKNOWN
normalized-compression64_22.opb	13.1248	SATISFIABLE
normalized-compression64_21.opb	1798.718	UNKNOWN
normalized-compression8_20.opb	1.11992	SATISFIABLE
normalized-compression64_19.opb	1798.728	UNKNOWN
normalized-compression16_7.opb	0.210134	UNSATISFIABLE
normalized-compression64_17.opb	1798.708	UNKNOWN
normalized-compression8_21.opb	1.57915	SATISFIABLE
normalized-compression64_16.opb	1798.703	UNKNOWN
normalized-compression16_10.opb	21.0765	UNSATISFIABLE
normalized-compression32_16.opb	155.05	SATISFIABLE
normalized-compression8_18.opb	0.742083	SATISFIABLE
normalized-compression32_10.opb	291.863	UNSATISFIABLE
normalized-compression64_15.opb	1798.755	UNKNOWN
normalized-compression8_17.opb	6.00269	SATISFIABLE
normalized-compression16_9.opb	3.45207	UNSATISFIABLE
normalized-compression64_30.opb	2.08902	SATISFIABLE
normalized-compression8_16.opb	0.327234	SATISFIABLE
normalized-compression64_27.opb	1.58374	SATISFIABLE
normalized-compression64_6.opb	13.474	UNSATISFIABLE
normalized-compression8_26.opb	0.092276	SATISFIABLE
normalized-compression64_13.opb	1798.773	UNKNOWN
normalized-compression8_14.opb	17.8101	UNSATISFIABLE
normalized-compression64_4.opb	1.40021	UNSATISFIABLE
normalized-compression16_4.opb	0.029498	UNSATISFIABLE
normalized-compression8_23.opb	0.245781	SATISFIABLE
normalized-compression32_19.opb	0.500856	SATISFIABLE
normalized-compression8_25.opb	0.509338	SATISFIABLE
normalized-compression16_8.opb	0.659712	UNSATISFIABLE
normalized-compression64_23.opb	1798.711	UNKNOWN
normalized-compression32_8.opb	14.7501	UNSATISFIABLE
normalized-compression64_7.opb	104.196	UNSATISFIABLE
normalized-compression64_29.opb	1.50457	SATISFIABLE
normalized-compression16_16.opb	0.046341	SATISFIABLE
normalized-compression64_25.opb	54.1035	SATISFIABLE
normalized-compression64_18.opb	1798.725	UNKNOWN
normalized-compression8_24.opb	0.225551	SATISFIABLE
normalized-compression16_14.opb	0.074679	SATISFIABLE
normalized-compression32_20.opb	0.747492	SATISFIABLE
normalized-sha1-size128-round22-2.opb	1798.720	UNKNOWN
normalized-sha1-size80-round21-1.opb	39.234	SATISFIABLE
normalized-sha1-size160-round23-6.opb	1798.743	UNKNOWN
normalized-sha1-size80-round23-6.opb	1798.708	UNKNOWN
normalized-sha1-size160-round23-8.opb	1798.699	UNKNOWN
normalized-sha1-size96-round23-2.opb	1798.734	UNKNOWN
normalized-sha1-size96-round21-1.opb	5.45034	SATISFIABLE
normalized-sha1-size96-round21-3.opb	9.17966	SATISFIABLE
normalized-sha1-size96-round22-5.opb	1798.700	UNKNOWN
normalized-sha1-size80-round23-9.opb	1798.705	UNKNOWN
normalized-sha1-size144-round21-6.opb	219.829	SATISFIABLE
normalized-sha1-size144-round22-7.opb	1798.716	UNKNOWN
normalized-sha1-size160-round21-0.opb	670.586	SATISFIABLE
normalized-sha1-size160-round23-7.opb	1798.715	UNKNOWN
normalized-sha1-size80-round21-5.opb	140.173	SATISFIABLE
normalized-sha1-size112-round23-4.opb	1798.743	UNKNOWN
normalized-sha1-size112-round21-8.opb	1263.09	SATISFIABLE
normalized-sha1-size160-round21-9.opb	79.5365	SATISFIABLE
normalized-sha1-size96-round21-0.opb	240.764	SATISFIABLE
normalized-sha1-size112-round22-7.opb	1798.683	UNKNOWN
normalized-sha1-size144-round21-2.opb	995.719	SATISFIABLE
normalized-sha1-size80-round21-4.opb	13.0109	SATISFIABLE
normalized-sha1-size160-round21-2.opb	626.029	SATISFIABLE
normalized-sha1-size160-round22-2.opb	1798.692	UNKNOWN
normalized-sha1-size144-round23-6.opb	1800.448	UNKNOWN
normalized-sha1-size112-round23-5.opb	1798.705	UNKNOWN
normalized-sha1-size80-round22-7.opb	1798.712	UNKNOWN
normalized-sha1-size128-round22-0.opb	1798.720	UNKNOWN
normalized-sha1-size112-round23-1.opb	1800.459	UNKNOWN
normalized-sha1-size80-round23-8.opb	1798.690	UNKNOWN
normalized-sha1-size160-round22-6.opb	1798.686	UNKNOWN
normalized-sha1-size160-round22-9.opb	1798.708	UNKNOWN
normalized-sha1-size80-round22-9.opb	1635.88	SATISFIABLE
normalized-sha1-size112-round22-4.opb	1798.692	UNKNOWN
normalized-sha1-size96-round22-6.opb	1798.714	UNKNOWN
normalized-sha1-size128-round23-9.opb	1798.712	UNKNOWN
normalized-sha1-size80-round21-8.opb	31.2733	SATISFIABLE
normalized-sha1-size128-round22-8.opb	1798.713	UNKNOWN
normalized-sha1-size128-round22-4.opb	1798.701	UNKNOWN
normalized-sha1-size144-round23-9.opb	1798.731	UNKNOWN
normalized-sha1-size128-round21-5.opb	72.9217	SATISFIABLE
normalized-sha1-size96-round21-9.opb	471.517	SATISFIABLE
normalized-sha1-size144-round23-4.opb	1798.712	UNKNOWN
normalized-sha1-size80-round21-3.opb	147.097	SATISFIABLE
normalized-sha1-size112-round23-8.opb	1798.695	UNKNOWN
normalized-sha1-size160-round23-5.opb	1798.691	UNKNOWN
normalized-sha1-size160-round21-1.opb	489.7	SATISFIABLE
normalized-sha1-size80-round23-1.opb	1800.459	UNKNOWN
normalized-sha1-size96-round23-9.opb	1798.700	UNKNOWN
normalized-sha1-size80-round21-7.opb	54.4746	SATISFIABLE
normalized-sha1-size96-round22-8.opb	1798.706	UNKNOWN
normalized-sha1-size128-round21-6.opb	631.976	SATISFIABLE
normalized-sha1-size160-round23-2.opb	1798.710	UNKNOWN
normalized-sha1-size80-round22-3.opb	1798.711	UNKNOWN
normalized-sha1-size112-round22-8.opb	1798.699	UNKNOWN
normalized-sha1-size128-round23-8.opb	1798.695	UNKNOWN
normalized-sha1-size160-round22-8.opb	1798.677	UNKNOWN
normalized-sha1-size96-round22-4.opb	1798.692	UNKNOWN
normalized-sha1-size160-round22-4.opb	1798.692	UNKNOWN
normalized-sha1-size112-round21-5.opb	337.756	SATISFIABLE
normalized-sha1-size80-round23-4.opb	1798.736	UNKNOWN
normalized-sha1-size128-round21-3.opb	1089.43	SATISFIABLE
normalized-sha1-size160-round22-1.opb	1798.712	UNKNOWN
normalized-sha1-size144-round22-8.opb	1798.684	UNKNOWN
normalized-sha1-size96-round23-0.opb	1798.738	UNKNOWN
normalized-sha1-size144-round22-9.opb	1798.690	UNKNOWN
normalized-sha1-size144-round21-1.opb	1228.41	SATISFIABLE
normalized-sha1-size128-round23-7.opb	1798.693	UNKNOWN
normalized-sha1-size96-round21-4.opb	618.536	SATISFIABLE
normalized-sha1-size160-round21-8.opb	1798.705	UNKNOWN
normalized-sha1-size80-round22-0.opb	1798.725	UNKNOWN
normalized-sha1-size160-round23-9.opb	1798.704	UNKNOWN
normalized-sha1-size112-round23-6.opb	1798.697	UNKNOWN
normalized-sha1-size80-round22-8.opb	1798.701	UNKNOWN
normalized-sha1-size144-round21-0.opb	529.145	SATISFIABLE
normalized-sha1-size80-round23-3.opb	1798.693	UNKNOWN
normalized-sha1-size160-round21-5.opb	196.097	SATISFIABLE
normalized-sha1-size80-round21-6.opb	34.2588	SATISFIABLE
normalized-sha1-size96-round21-7.opb	89.3109	SATISFIABLE
normalized-sha1-size160-round22-5.opb	1798.711	UNKNOWN
normalized-sha1-size128-round22-1.opb	1798.743	UNKNOWN
normalized-sha1-size144-round22-3.opb	1798.700	UNKNOWN
normalized-sha1-size160-round21-4.opb	1004.36	SATISFIABLE
normalized-sha1-size112-round21-9.opb	3.89984	SATISFIABLE
normalized-sha1-size112-round22-5.opb	1798.711	UNKNOWN
normalized-sha1-size96-round22-3.opb	1193.69	SATISFIABLE
normalized-sha1-size112-round23-7.opb	1798.682	UNKNOWN
normalized-sha1-size80-round22-5.opb	1798.722	UNKNOWN
normalized-sha1-size80-round21-9.opb	31.1271	SATISFIABLE
normalized-sha1-size128-round21-8.opb	119.777	SATISFIABLE
normalized-sha1-size80-round23-5.opb	1798.701	UNKNOWN
normalized-sha1-size80-round22-2.opb	1798.689	UNKNOWN
normalized-sha1-size112-round21-7.opb	288.004	SATISFIABLE
normalized-sha1-size160-round23-0.opb	1798.687	UNKNOWN
normalized-sha1-size128-round22-9.opb	1798.702	UNKNOWN
normalized-sha1-size128-round23-4.opb	1798.704	UNKNOWN
normalized-sha1-size96-round22-9.opb	1800.450	UNKNOWN
normalized-sha1-size80-round22-1.opb	1798.728	UNKNOWN
normalized-sha1-size128-round22-7.opb	1798.699	UNKNOWN
normalized-sha1-size112-round23-0.opb	1798.704	UNKNOWN
normalized-sha1-size96-round22-2.opb	1135.65	SATISFIABLE
normalized-sha1-size112-round23-2.opb	1798.705	UNKNOWN
normalized-sha1-size112-round22-1.opb	1798.730	UNKNOWN
normalized-sha1-size144-round23-3.opb	1798.687	UNKNOWN
normalized-sha1-size144-round23-7.opb	1798.740	UNKNOWN
normalized-sha1-size112-round22-0.opb	1441.69	SATISFIABLE
normalized-sha1-size112-round21-0.opb	79.1674	SATISFIABLE
normalized-sha1-size96-round23-5.opb	1798.711	UNKNOWN
normalized-sha1-size80-round23-0.opb	1798.713	UNKNOWN
normalized-sha1-size144-round22-4.opb	1798.687	UNKNOWN
normalized-sha1-size112-round21-3.opb	491.369	SATISFIABLE
normalized-sha1-size128-round21-2.opb	345	SATISFIABLE
normalized-sha1-size80-round21-2.opb	80.0156	SATISFIABLE
normalized-sha1-size144-round23-8.opb	1798.703	UNKNOWN
normalized-sha1-size160-round23-1.opb	1798.723	UNKNOWN
normalized-sha1-size96-round21-8.opb	60.5998	SATISFIABLE
normalized-sha1-size112-round21-6.opb	243.952	SATISFIABLE
normalized-sha1-size96-round23-6.opb	1798.702	UNKNOWN
normalized-sha1-size144-round21-3.opb	1800.445	UNKNOWN
normalized-sha1-size160-round23-3.opb	1800.458	UNKNOWN
normalized-sha1-size96-round22-7.opb	1798.711	UNKNOWN
normalized-sha1-size144-round23-1.opb	1798.702	UNKNOWN
normalized-sha1-size96-round22-1.opb	1798.735	UNKNOWN
normalized-sha1-size144-round22-1.opb	1798.720	UNKNOWN
normalized-sha1-size128-round23-2.opb	1798.736	UNKNOWN
normalized-sha1-size128-round21-4.opb	287.401	SATISFIABLE
normalized-sha1-size144-round23-5.opb	1798.709	UNKNOWN
normalized-sha1-size128-round22-3.opb	266.854	SATISFIABLE
normalized-sha1-size112-round22-6.opb	1798.691	UNKNOWN
normalized-sha1-size80-round23-7.opb	1798.698	UNKNOWN
normalized-sha1-size128-round23-1.opb	1798.711	UNKNOWN
normalized-sha1-size160-round21-7.opb	850.862	SATISFIABLE
normalized-sha1-size128-round22-6.opb	1798.709	UNKNOWN
normalized-sha1-size112-round21-4.opb	54.136	SATISFIABLE
normalized-sha1-size96-round23-1.opb	1798.704	UNKNOWN
normalized-sha1-size96-round23-4.opb	1798.691	UNKNOWN
normalized-sha1-size144-round22-6.opb	1798.727	UNKNOWN
normalized-sha1-size144-round21-7.opb	36.2606	SATISFIABLE
normalized-sha1-size160-round22-3.opb	1798.724	UNKNOWN
normalized-sha1-size128-round21-1.opb	90.733	SATISFIABLE
normalized-sha1-size128-round23-6.opb	1798.708	UNKNOWN
normalized-sha1-size112-round23-3.opb	1798.711	UNKNOWN
normalized-sha1-size128-round21-0.opb	999.334	SATISFIABLE
normalized-sha1-size96-round23-3.opb	1798.702	UNKNOWN
normalized-sha1-size144-round21-8.opb	481.444	SATISFIABLE
normalized-sha1-size96-round23-7.opb	1798.695	UNKNOWN
normalized-sha1-size96-round22-0.opb	1704.61	SATISFIABLE
normalized-sha1-size128-round21-9.opb	626.239	SATISFIABLE
normalized-sha1-size144-round21-5.opb	141.102	SATISFIABLE
normalized-sha1-size96-round23-8.opb	1798.704	UNKNOWN
normalized-sha1-size144-round22-0.opb	1798.694	UNKNOWN
normalized-sha1-size112-round22-9.opb	1798.689	UNKNOWN
normalized-sha1-size112-round21-1.opb	539.848	SATISFIABLE
normalized-sha1-size128-round22-5.opb	1800.456	UNKNOWN
normalized-sha1-size80-round21-0.opb	336.129	SATISFIABLE
normalized-sha1-size160-round21-6.opb	367.311	SATISFIABLE
normalized-sha1-size160-round22-0.opb	1798.709	UNKNOWN
normalized-sha1-size128-round23-5.opb	1798.713	UNKNOWN
normalized-sha1-size96-round21-2.opb	245.469	SATISFIABLE
normalized-sha1-size112-round21-2.opb	202.458	SATISFIABLE
normalized-sha1-size80-round22-6.opb	1111.22	SATISFIABLE
normalized-sha1-size144-round21-4.opb	876.796	SATISFIABLE
normalized-sha1-size144-round22-5.opb	1798.725	UNKNOWN
normalized-sha1-size96-round21-6.opb	78.4342	SATISFIABLE
normalized-sha1-size160-round21-3.opb	365.786	SATISFIABLE
normalized-sha1-size80-round23-2.opb	1798.745	UNKNOWN
normalized-sha1-size144-round21-9.opb	1798.721	UNKNOWN
normalized-sha1-size128-round23-0.opb	1798.731	UNKNOWN
normalized-sha1-size112-round23-9.opb	1798.703	UNKNOWN
normalized-sha1-size128-round21-7.opb	841.488	SATISFIABLE
normalized-sha1-size144-round22-2.opb	1798.719	UNKNOWN
normalized-sha1-size144-round23-2.opb	1798.675	UNKNOWN
normalized-sha1-size128-round23-3.opb	1798.728	UNKNOWN
normalized-sha1-size112-round22-3.opb	1367.47	SATISFIABLE
normalized-sha1-size160-round22-7.opb	1798.691	UNKNOWN
normalized-sha1-size112-round22-2.opb	1798.702	UNKNOWN
normalized-sha1-size160-round23-4.opb	1798.727	UNKNOWN
normalized-sha1-size80-round22-4.opb	1798.678	UNKNOWN
normalized-sha1-size144-round23-0.opb	1798.707	UNKNOWN
normalized-sha1-size96-round21-5.opb	702.75	SATISFIABLE
normalized-hw128-vm50p-dec.opb.negationfix.opb	UNKNOWN
normalized-hw128-vm75p-dec.opb.negationfix.opb	UNKNOWN
normalized-hw128-vm25p-dec.opb.negationfix.opb	UNKNOWN
normalized-hw128-vm85p-dec.opb.negationfix.opb	UNKNOWN
normalized-tseitin-regular-n66-d3-i3-f.cnf.gz-plain.pb.metafix.opb	75.8058	UNSATISFIABLE
normalized-tseitin-regular-n88-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	576.524	UNSATISFIABLE
normalized-tseitin-regular-n68-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	61.2147	UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	287.758	UNSATISFIABLE
normalized-tseitin-regular-n56-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	11.4523	UNSATISFIABLE
normalized-subsetCardinalitySigma-25-3.cnf.gz-plain.pb.metafix.opb	89.6638	UNSATISFIABLE
normalized-tseitin-regular-n38-d3-i3-f.cnf.gz-plain.pb.metafix.opb	0.440731	UNSATISFIABLE
normalized-regular-n20-d4-i3.cnf.gz-plain.pb.metafix.opb	90.2037	UNSATISFIABLE
normalized-tseitin-regular-n52-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	2.25916	UNSATISFIABLE
normalized-tseitin-regular-n90-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	367.837	UNSATISFIABLE
normalized-fixed-bandwidth-92.cnf.gz-extracted.pb.metafix.opb	1798.737	UNKNOWN
normalized-fixed-bandwidth-72.cnf.gz-extracted.pb.metafix.opb	1798.779	UNKNOWN
normalized-tseitin-regular-n94-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	1473.2	UNSATISFIABLE
normalized-fixed-bandwidth-61.cnf.gz-extracted.pb.metafix.opb	1798.761	UNKNOWN
normalized-subsetCardinalitySigma-24-2.cnf.gz-extracted.pb.metafix.opb	201.201	UNSATISFIABLE
normalized-tseitin-regular-n64-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	7.5995	UNSATISFIABLE
normalized-regular-n24-d4-i1.cnf.gz-plain.pb.metafix.opb	1798.783	UNKNOWN
normalized-tseitin-regular-n56-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	11.7597	UNSATISFIABLE
normalized-fixed-bandwidth-60.cnf.gz-extracted.pb.metafix.opb	1798.767	UNKNOWN
normalized-tseitin-regular-n90-d3-i1-f.cnf.gz-plain.pb.metafix.opb	410.36	UNSATISFIABLE
normalized-tseitin-regular-n66-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	89.5314	UNSATISFIABLE
normalized-tseitin-regular-n42-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	0.267072	UNSATISFIABLE
normalized-fixed-bandwidth-65.cnf.gz-extracted.pb.metafix.opb	1798.765	UNKNOWN
normalized-regular-n23-d4-i1.cnf.gz-plain.pb.metafix.opb	345.717	UNSATISFIABLE
normalized-fixed-bandwidth-88.cnf.gz-extracted.pb.metafix.opb	1798.750	UNKNOWN
normalized-tseitin-regular-n82-d3-i1-f.cnf.gz-plain.pb.metafix.opb	329.769	UNSATISFIABLE
normalized-fixed-bandwidth-98.cnf.gz-extracted.pb.metafix.opb	1798.729	UNKNOWN
normalized-tseitin-regular-n66-d3-i1-f.cnf.gz-plain.pb.metafix.opb	4.16218	UNSATISFIABLE
normalized-tseitin-regular-n86-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	946.365	UNSATISFIABLE
normalized-tseitin-regular-n58-d3-i3-f.cnf.gz-plain.pb.metafix.opb	8.87263	UNSATISFIABLE
normalized-tseitin-regular-n50-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	0.627749	UNSATISFIABLE
normalized-subsetCardinalitySigma-25-2.cnf.gz-extracted.pb.metafix.opb	934.88	UNSATISFIABLE
normalized-tseitin-regular-n74-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	32.9477	UNSATISFIABLE
normalized-tseitin-regular-n42-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	0.262529	UNSATISFIABLE
normalized-tseitin-regular-n58-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	4.65928	UNSATISFIABLE
normalized-subsetCardinalitySigma-28-2.cnf.gz-plain.pb.metafix.opb	850.216	UNSATISFIABLE
normalized-tseitin-regular-n76-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	305.994	UNSATISFIABLE
normalized-tseitin-regular-n44-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	0.236996	UNSATISFIABLE
normalized-fixed-bandwidth-27.cnf.gz-extracted.pb.metafix.opb	1798.769	UNKNOWN
normalized-tseitin-regular-n60-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	4.76033	UNSATISFIABLE
normalized-tseitin-regular-n68-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	27.59	UNSATISFIABLE
normalized-regular-n22-d4-i1.cnf.gz-extracted.pb.metafix.opb	157.865	UNSATISFIABLE
normalized-regular-n24-d4-i3.cnf.gz-extracted.pb.metafix.opb	1798.771	UNKNOWN
normalized-tseitin-regular-n72-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	140.575	UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	10.0765	UNSATISFIABLE
normalized-tseitin-regular-n92-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	654.139	UNSATISFIABLE
normalized-tseitin-regular-n54-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	0.171202	UNSATISFIABLE
normalized-regular-n21-d4-i3.cnf.gz-extracted.pb.metafix.opb	101.037	UNSATISFIABLE
normalized-tseitin-regular-n38-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	0.291651	UNSATISFIABLE
normalized-subsetCardinalitySigma-22-3.cnf.gz-plain.pb.metafix.opb	149.735	UNSATISFIABLE
normalized-regular-n26-d4-i3.cnf.gz-extracted.pb.metafix.opb	1798.774	UNKNOWN
normalized-tseitin-regular-n40-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	0.331239	UNSATISFIABLE
normalized-fixed-bandwidth-68.cnf.gz-extracted.pb.metafix.opb	1798.740	UNKNOWN
normalized-fixed-bandwidth-51.cnf.gz-extracted.pb.metafix.opb	1798.710	UNKNOWN
normalized-tseitin-regular-n90-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	330.525	UNSATISFIABLE
normalized-subsetCardinalitySigma-24-1.cnf.gz-plain.pb.metafix.opb	153.324	UNSATISFIABLE
normalized-tseitin-regular-n80-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	123.419	UNSATISFIABLE
normalized-subsetCardinalitySigma-23-1.cnf.gz-plain.pb.metafix.opb	113.836	UNSATISFIABLE
normalized-subsetCardinalitySigma-22-1.cnf.gz-plain.pb.metafix.opb	132.785	UNSATISFIABLE
normalized-tseitin-regular-n62-d3-i3-f.cnf.gz-plain.pb.metafix.opb	15.4846	UNSATISFIABLE
normalized-regular-n18-d4-i2.cnf.gz-plain.pb.metafix.opb	37.4403	UNSATISFIABLE
normalized-tseitin-regular-n56-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	10.9065	UNSATISFIABLE
normalized-tseitin-regular-n42-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	1.72534	UNSATISFIABLE
normalized-tseitin-regular-n44-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	0.88605	UNSATISFIABLE
normalized-regular-n26-d4-i3.cnf.gz-plain.pb.metafix.opb	1798.761	UNKNOWN
normalized-tseitin-regular-n52-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	2.26421	UNSATISFIABLE
normalized-tseitin-regular-n52-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	6.94524	UNSATISFIABLE
normalized-tseitin-regular-n58-d3-i1-f.cnf.gz-plain.pb.metafix.opb	4.6341	UNSATISFIABLE
normalized-tseitin-regular-n76-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	935.511	UNSATISFIABLE
normalized-tseitin-regular-n48-d3-i3-f.cnf.gz-plain.pb.metafix.opb	2.10641	UNSATISFIABLE
normalized-regular-n17-d4-i3.cnf.gz-plain.pb.metafix.opb	27.8529	UNSATISFIABLE
normalized-subsetCardinalitySigma-24-3.cnf.gz-plain.pb.metafix.opb	158.102	UNSATISFIABLE
normalized-fixed-bandwidth-71.cnf.gz-extracted.pb.metafix.opb	1798.762	UNKNOWN
normalized-tseitin-regular-n64-d3-i2-f.cnf.gz-plain.pb.metafix.opb	4.83978	UNSATISFIABLE
normalized-subsetCardinalitySigma-21-2.cnf.gz-plain.pb.metafix.opb	26.7531	UNSATISFIABLE
normalized-subsetCardinalitySigma-25-3.cnf.gz-extracted.pb.metafix.opb	115.82	UNSATISFIABLE
normalized-tseitin-regular-n40-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	1.56836	UNSATISFIABLE
normalized-fixed-bandwidth-64.cnf.gz-extracted.pb.metafix.opb	1798.747	UNKNOWN
normalized-tseitin-regular-n94-d3-i2-f.cnf.gz-plain.pb.metafix.opb	764.01	UNSATISFIABLE
normalized-fixed-bandwidth-22.cnf.gz-extracted.pb.metafix.opb	1798.768	UNKNOWN
normalized-tseitin-regular-n56-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	12.0734	UNSATISFIABLE
normalized-tseitin-regular-n60-d3-i1-f.cnf.gz-plain.pb.metafix.opb	4.58559	UNSATISFIABLE
normalized-tseitin-regular-n40-d3-i2-f.cnf.gz-plain.pb.metafix.opb	0.590896	UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i3-f.cnf.gz-plain.pb.metafix.opb	399.472	UNSATISFIABLE
normalized-tseitin-regular-n64-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	6.70011	UNSATISFIABLE
normalized-fixed-bandwidth-16.cnf.gz-plain.pb.metafix.opb	71.2285	UNSATISFIABLE
normalized-fixed-bandwidth-84.cnf.gz-extracted.pb.metafix.opb	1798.784	UNKNOWN
normalized-fixed-bandwidth-95.cnf.gz-extracted.pb.metafix.opb	1798.746	UNKNOWN
normalized-fixed-bandwidth-89.cnf.gz-extracted.pb.metafix.opb	1798.742	UNKNOWN
normalized-fixed-bandwidth-19.cnf.gz-plain.pb.metafix.opb	625.613	UNSATISFIABLE
normalized-subsetCardinalitySigma-21-1.cnf.gz-plain.pb.metafix.opb	68.4278	UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	25.3881	UNSATISFIABLE
normalized-subsetCardinalitySigma-27-3.cnf.gz-extracted.pb.metafix.opb	998.164	UNSATISFIABLE
normalized-tseitin-regular-n92-d3-i3-f.cnf.gz-plain.pb.metafix.opb	1686.96	UNSATISFIABLE
normalized-tseitin-regular-n64-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	3.76122	UNSATISFIABLE
normalized-regular-n22-d4-i2.cnf.gz-extracted.pb.metafix.opb	150.851	UNSATISFIABLE
normalized-tseitin-regular-n74-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	72.5153	UNSATISFIABLE
normalized-tseitin-regular-n68-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	26.9455	UNSATISFIABLE
normalized-subsetCardinalitySigma-26-1.cnf.gz-plain.pb.metafix.opb	532.881	UNSATISFIABLE
normalized-tseitin-regular-n76-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	1092.01	UNSATISFIABLE
normalized-tseitin-regular-n84-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	1519.23	UNSATISFIABLE
normalized-subsetCardinalitySigma-29-3.cnf.gz-extracted.pb.metafix.opb	1798.760	UNKNOWN
normalized-tseitin-regular-n66-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	27.014	UNSATISFIABLE
normalized-fixed-bandwidth-83.cnf.gz-extracted.pb.metafix.opb	1798.739	UNKNOWN
normalized-regular-n16-d4-i2.cnf.gz-plain.pb.metafix.opb	11.7399	UNSATISFIABLE
normalized-tseitin-regular-n72-d3-i3-f.cnf.gz-plain.pb.metafix.opb	10.6972	UNSATISFIABLE
normalized-tseitin-regular-n52-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	1.24215	UNSATISFIABLE
normalized-fixed-bandwidth-17.cnf.gz-plain.pb.metafix.opb	160.521	UNSATISFIABLE
normalized-regular-n21-d4-i1.cnf.gz-plain.pb.metafix.opb	23.9748	UNSATISFIABLE
normalized-regular-n26-d4-i1.cnf.gz-extracted.pb.metafix.opb	1798.754	UNKNOWN
normalized-subsetCardinalitySigma-20-3.cnf.gz-plain.pb.metafix.opb	29.5859	UNSATISFIABLE
normalized-tseitin-regular-n76-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	218.021	UNSATISFIABLE
normalized-tseitin-regular-n62-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	15.4968	UNSATISFIABLE
normalized-subsetCardinalitySigma-17-3.cnf.gz-plain.pb.metafix.opb	2.97605	UNSATISFIABLE
normalized-subsetCardinalitySigma-24-2.cnf.gz-plain.pb.metafix.opb	201.399	UNSATISFIABLE
normalized-tseitin-regular-n90-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	1447.94	UNSATISFIABLE
normalized-regular-n19-d4-i3.cnf.gz-plain.pb.metafix.opb	28.5119	UNSATISFIABLE
normalized-tseitin-regular-n84-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	1520.88	UNSATISFIABLE
normalized-tseitin-regular-n76-d3-i2-f.cnf.gz-plain.pb.metafix.opb	746.94	UNSATISFIABLE
normalized-fixed-bandwidth-100.cnf.gz-extracted.pb.metafix.opb	1798.748	UNKNOWN
normalized-tseitin-regular-n84-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	727.47	UNSATISFIABLE
normalized-fixed-bandwidth-91.cnf.gz-extracted.pb.metafix.opb	1798.715	UNKNOWN
normalized-tseitin-regular-n46-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	0.65304	UNSATISFIABLE
normalized-tseitin-regular-n38-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	0.442785	UNSATISFIABLE
normalized-tseitin-regular-n46-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	2.9512	UNSATISFIABLE
normalized-fixed-bandwidth-97.cnf.gz-extracted.pb.metafix.opb	1798.713	UNKNOWN
normalized-subsetCardinalitySigma-27-1.cnf.gz-plain.pb.metafix.opb	844.84	UNSATISFIABLE
normalized-tseitin-regular-n72-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	46.3468	UNSATISFIABLE
normalized-tseitin-regular-n48-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	0.727246	UNSATISFIABLE
normalized-tseitin-regular-n84-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	319.624	UNSATISFIABLE
normalized-tseitin-regular-n50-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	0.376543	UNSATISFIABLE
normalized-tseitin-regular-n86-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	553.201	UNSATISFIABLE
normalized-tseitin-regular-n86-d3-i2-f.cnf.gz-plain.pb.metafix.opb	1158.3	UNSATISFIABLE
normalized-tseitin-regular-n80-d3-i1-f.cnf.gz-plain.pb.metafix.opb	131.916	UNSATISFIABLE
normalized-subsetCardinalitySigma-20-1.cnf.gz-plain.pb.metafix.opb	12.4582	UNSATISFIABLE
normalized-tseitin-regular-n74-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	54.4995	UNSATISFIABLE
normalized-tseitin-regular-n60-d3-i2-f.cnf.gz-plain.pb.metafix.opb	4.76248	UNSATISFIABLE
normalized-subsetCardinalitySigma-20-2.cnf.gz-plain.pb.metafix.opb	20.0177	UNSATISFIABLE
normalized-tseitin-regular-n50-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	0.600383	UNSATISFIABLE
normalized-tseitin-regular-n54-d3-i2-f.cnf.gz-plain.pb.metafix.opb	0.172607	UNSATISFIABLE
normalized-tseitin-regular-n62-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	18.0235	UNSATISFIABLE
normalized-tseitin-regular-n86-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	498.946	UNSATISFIABLE
normalized-fixed-bandwidth-81.cnf.gz-extracted.pb.metafix.opb	1798.738	UNKNOWN
normalized-tseitin-regular-n66-d3-i2-f.cnf.gz-plain.pb.metafix.opb	26.2024	UNSATISFIABLE
normalized-tseitin-regular-n52-d3-i3-f.cnf.gz-plain.pb.metafix.opb	1.27749	UNSATISFIABLE
normalized-tseitin-regular-n88-d3-i3-f.cnf.gz-plain.pb.metafix.opb	734.744	UNSATISFIABLE
normalized-tseitin-regular-n72-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	45.9899	UNSATISFIABLE
normalized-regular-n18-d4-i1.cnf.gz-plain.pb.metafix.opb	26.8667	UNSATISFIABLE
normalized-tseitin-regular-n58-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	4.31083	UNSATISFIABLE
normalized-tseitin-regular-n84-d3-i3-f.cnf.gz-plain.pb.metafix.opb	1194.33	UNSATISFIABLE
normalized-tseitin-regular-n68-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	33.7681	UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	10.0908	UNSATISFIABLE
normalized-regular-n23-d4-i2.cnf.gz-plain.pb.metafix.opb	65.3594	UNSATISFIABLE
normalized-fixed-bandwidth-66.cnf.gz-extracted.pb.metafix.opb	1798.731	UNKNOWN
normalized-fixed-bandwidth-75.cnf.gz-extracted.pb.metafix.opb	1798.755	UNKNOWN
normalized-fixed-bandwidth-17.cnf.gz-extracted.pb.metafix.opb	138.466	UNSATISFIABLE
normalized-fixed-bandwidth-85.cnf.gz-extracted.pb.metafix.opb	1798.742	UNKNOWN
normalized-tseitin-regular-n68-d3-i1-f.cnf.gz-plain.pb.metafix.opb	26.4141	UNSATISFIABLE
normalized-subsetCardinalitySigma-29-1.cnf.gz-extracted.pb.metafix.opb	1798.793	UNKNOWN
normalized-tseitin-regular-n58-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	21.4175	UNSATISFIABLE
normalized-tseitin-regular-n84-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	950.928	UNSATISFIABLE
normalized-tseitin-regular-n46-d3-i1-f.cnf.gz-plain.pb.metafix.opb	2.18725	UNSATISFIABLE
normalized-subsetCardinalitySigma-30-2.cnf.gz-extracted.pb.metafix.opb	1798.774	UNKNOWN
normalized-subsetCardinalitySigma-23-2.cnf.gz-extracted.pb.metafix.opb	176.432	UNSATISFIABLE
normalized-tseitin-regular-n88-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	580.88	UNSATISFIABLE
normalized-fixed-bandwidth-70.cnf.gz-extracted.pb.metafix.opb	1798.732	UNKNOWN
normalized-tseitin-regular-n48-d3-i1-f.cnf.gz-plain.pb.metafix.opb	0.72893	UNSATISFIABLE
normalized-tseitin-regular-n92-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	1745.11	UNSATISFIABLE
normalized-tseitin-regular-n68-d3-i3-f.cnf.gz-plain.pb.metafix.opb	61.1713	UNSATISFIABLE
normalized-tseitin-regular-n52-d3-i1-f.cnf.gz-plain.pb.metafix.opb	1.955	UNSATISFIABLE
normalized-fixed-bandwidth-87.cnf.gz-extracted.pb.metafix.opb	1798.718	UNKNOWN
normalized-regular-n21-d4-i3.cnf.gz-plain.pb.metafix.opb	271.049	UNSATISFIABLE
normalized-fixed-bandwidth-67.cnf.gz-extracted.pb.metafix.opb	1798.760	UNKNOWN
normalized-fixed-bandwidth-23.cnf.gz-extracted.pb.metafix.opb	1798.688	UNKNOWN
normalized-regular-n17-d4-i2.cnf.gz-plain.pb.metafix.opb	12.128	UNSATISFIABLE
normalized-fixed-bandwidth-94.cnf.gz-extracted.pb.metafix.opb	1800.460	UNKNOWN
normalized-regular-n29-d4-i2.cnf.gz-plain.pb.metafix.opb	1798.762	UNKNOWN
normalized-subsetCardinalitySigma-23-2.cnf.gz-plain.pb.metafix.opb	363.356	UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	399.74	UNSATISFIABLE
normalized-tseitin-regular-n82-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	479.131	UNSATISFIABLE
normalized-regular-n26-d4-i2.cnf.gz-extracted.pb.metafix.opb	1798.732	UNKNOWN
normalized-fixed-bandwidth-18.cnf.gz-extracted.pb.metafix.opb	378.293	UNSATISFIABLE
normalized-regular-n22-d4-i2.cnf.gz-plain.pb.metafix.opb	157.567	UNSATISFIABLE
normalized-subsetCardinalitySigma-18-1.cnf.gz-plain.pb.metafix.opb	4.88856	UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	5.06635	UNSATISFIABLE
normalized-tseitin-regular-n90-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	1448.33	UNSATISFIABLE
normalized-tseitin-regular-n40-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	1.18799	UNSATISFIABLE
normalized-tseitin-regular-n40-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	0.993043	UNSATISFIABLE
normalized-regular-n19-d4-i1.cnf.gz-plain.pb.metafix.opb	67.1223	UNSATISFIABLE
normalized-regular-n25-d4-i2.cnf.gz-extracted.pb.metafix.opb	1798.803	UNKNOWN
normalized-tseitin-regular-n50-d3-i2-f.cnf.gz-plain.pb.metafix.opb	0.374819	UNSATISFIABLE
normalized-tseitin-regular-n56-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	7.64087	UNSATISFIABLE
normalized-tseitin-regular-n90-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	1641.1	UNSATISFIABLE
normalized-fixed-bandwidth-80.cnf.gz-extracted.pb.metafix.opb	1798.768	UNKNOWN
normalized-subsetCardinalitySigma-24-3.cnf.gz-extracted.pb.metafix.opb	97.9906	UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	5.14715	UNSATISFIABLE
normalized-tseitin-regular-n80-d3-i3-f.cnf.gz-plain.pb.metafix.opb	1543.84	UNSATISFIABLE
normalized-tseitin-regular-n96-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	1781.57	UNSATISFIABLE
normalized-tseitin-regular-n56-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	10.9791	UNSATISFIABLE
normalized-fixed-bandwidth-21.cnf.gz-extracted.pb.metafix.opb	1798.761	UNKNOWN
normalized-tseitin-regular-n44-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	0.292409	UNSATISFIABLE
normalized-tseitin-regular-n76-d3-i3-f.cnf.gz-plain.pb.metafix.opb	343.504	UNSATISFIABLE
normalized-tseitin-regular-n44-d3-i1-f.cnf.gz-plain.pb.metafix.opb	0.257418	UNSATISFIABLE
normalized-tseitin-regular-n54-d3-i3-f.cnf.gz-plain.pb.metafix.opb	4.46673	UNSATISFIABLE
normalized-fixed-bandwidth-26.cnf.gz-extracted.pb.metafix.opb	1800.465	UNKNOWN
normalized-tseitin-regular-n76-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	481.712	UNSATISFIABLE
normalized-tseitin-regular-n82-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	59.567	UNSATISFIABLE
normalized-tseitin-regular-n74-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	96.3159	UNSATISFIABLE
normalized-fixed-bandwidth-16.cnf.gz-extracted.pb.metafix.opb	130.223	UNSATISFIABLE
normalized-tseitin-regular-n80-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	1315.95	UNSATISFIABLE
normalized-tseitin-regular-n60-d3-i3-f.cnf.gz-plain.pb.metafix.opb	16.7691	UNSATISFIABLE
normalized-tseitin-regular-n82-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	247.015	UNSATISFIABLE
normalized-tseitin-regular-n66-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	3.38803	UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i1-f.cnf.gz-plain.pb.metafix.opb	140.646	UNSATISFIABLE
normalized-subsetCardinalitySigma-22-2.cnf.gz-plain.pb.metafix.opb	12.3381	UNSATISFIABLE
normalized-regular-n23-d4-i2.cnf.gz-extracted.pb.metafix.opb	72.7405	UNSATISFIABLE
normalized-tseitin-regular-n72-d3-i1-f.cnf.gz-plain.pb.metafix.opb	45.8812	UNSATISFIABLE
normalized-tseitin-regular-n50-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	2.13741	UNSATISFIABLE
normalized-tseitin-regular-n46-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	2.95495	UNSATISFIABLE
normalized-tseitin-regular-n74-d3-i3-f.cnf.gz-plain.pb.metafix.opb	155.205	UNSATISFIABLE
normalized-tseitin-regular-n94-d3-i1-f.cnf.gz-plain.pb.metafix.opb	1510.2	UNSATISFIABLE
normalized-tseitin-regular-n92-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	1705.52	UNSATISFIABLE
normalized-tseitin-regular-n62-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	9.59516	UNSATISFIABLE
normalized-subsetCardinalitySigma-25-1.cnf.gz-plain.pb.metafix.opb	194.464	UNSATISFIABLE
normalized-tseitin-regular-n72-d3-i2-f.cnf.gz-plain.pb.metafix.opb	140.93	UNSATISFIABLE
normalized-tseitin-regular-n46-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	0.934782	UNSATISFIABLE
normalized-fixed-bandwidth-58.cnf.gz-extracted.pb.metafix.opb	1798.761	UNKNOWN
normalized-tseitin-regular-n38-d3-i2-f.cnf.gz-plain.pb.metafix.opb	0.35851	UNSATISFIABLE
normalized-tseitin-regular-n50-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	2.13489	UNSATISFIABLE
normalized-fixed-bandwidth-76.cnf.gz-extracted.pb.metafix.opb	1798.719	UNKNOWN
normalized-tseitin-regular-n44-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	0.834629	UNSATISFIABLE
normalized-subsetCardinalitySigma-28-3.cnf.gz-extracted.pb.metafix.opb	1800.474	UNKNOWN
normalized-tseitin-regular-n50-d3-i1-f.cnf.gz-plain.pb.metafix.opb	2.04557	UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	75.3949	UNSATISFIABLE
normalized-tseitin-regular-n58-d3-i2-f.cnf.gz-plain.pb.metafix.opb	26.9509	UNSATISFIABLE
normalized-tseitin-regular-n82-d3-i2-f.cnf.gz-plain.pb.metafix.opb	61.6848	UNSATISFIABLE
normalized-subsetCardinalitySigma-22-1.cnf.gz-extracted.pb.metafix.opb	156.857	UNSATISFIABLE
normalized-fixed-bandwidth-63.cnf.gz-extracted.pb.metafix.opb	1798.778	UNKNOWN
normalized-tseitin-regular-n48-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	9.82058	UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	24.8195	UNSATISFIABLE
normalized-tseitin-regular-n86-d3-i1-f.cnf.gz-plain.pb.metafix.opb	1165.17	UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	328.617	UNSATISFIABLE
normalized-fixed-bandwidth-69.cnf.gz-extracted.pb.metafix.opb	1798.754	UNKNOWN
normalized-tseitin-regular-n74-d3-i1-f.cnf.gz-plain.pb.metafix.opb	29.0261	UNSATISFIABLE
normalized-fixed-bandwidth-86.cnf.gz-extracted.pb.metafix.opb	1798.754	UNKNOWN
normalized-tseitin-regular-n72-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	17.5904	UNSATISFIABLE
normalized-fixed-bandwidth-19.cnf.gz-extracted.pb.metafix.opb	977.019	UNSATISFIABLE
normalized-tseitin-regular-n62-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	10.6838	UNSATISFIABLE
normalized-regular-n28-d4-i3.cnf.gz-extracted.pb.metafix.opb	1800.465	UNKNOWN
normalized-fixed-bandwidth-55.cnf.gz-extracted.pb.metafix.opb	1798.737	UNKNOWN
normalized-tseitin-regular-n56-d3-i1-f.cnf.gz-plain.pb.metafix.opb	10.9428	UNSATISFIABLE
normalized-subsetCardinalitySigma-19-2.cnf.gz-plain.pb.metafix.opb	35.6806	UNSATISFIABLE
normalized-tseitin-regular-n74-d3-i2-f.cnf.gz-plain.pb.metafix.opb	315.067	UNSATISFIABLE
normalized-tseitin-regular-n48-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	2.10472	UNSATISFIABLE
normalized-tseitin-regular-n46-d3-i3-f.cnf.gz-plain.pb.metafix.opb	0.805141	UNSATISFIABLE
normalized-subsetCardinalitySigma-23-3.cnf.gz-plain.pb.metafix.opb	150.726	UNSATISFIABLE
normalized-tseitin-regular-n38-d3-i1-f.cnf.gz-plain.pb.metafix.opb	0.290758	UNSATISFIABLE
normalized-tseitin-regular-n94-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	737.851	UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i2-f.cnf.gz-plain.pb.metafix.opb	287.839	UNSATISFIABLE
normalized-tseitin-regular-n52-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	1.81003	UNSATISFIABLE
normalized-tseitin-regular-n68-d3-i2-f.cnf.gz-plain.pb.metafix.opb	26.0395	UNSATISFIABLE
normalized-subsetCardinalitySigma-19-3.cnf.gz-plain.pb.metafix.opb	26.924	UNSATISFIABLE
normalized-regular-n27-d4-i3.cnf.gz-extracted.pb.metafix.opb	1798.801	UNKNOWN
normalized-tseitin-regular-n84-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	319.12	UNSATISFIABLE
normalized-tseitin-regular-n64-d3-i1-f.cnf.gz-plain.pb.metafix.opb	5.27928	UNSATISFIABLE
normalized-subsetCardinalitySigma-25-1.cnf.gz-extracted.pb.metafix.opb	177.856	UNSATISFIABLE
normalized-fixed-bandwidth-20.cnf.gz-extracted.pb.metafix.opb	955.196	UNSATISFIABLE
normalized-tseitin-regular-n40-d3-i3-f.cnf.gz-plain.pb.metafix.opb	1.56796	UNSATISFIABLE
normalized-subsetCardinalitySigma-27-1.cnf.gz-extracted.pb.metafix.opb	932.267	UNSATISFIABLE
normalized-tseitin-regular-n42-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	0.966794	UNSATISFIABLE
normalized-tseitin-regular-n82-d3-i3-f.cnf.gz-plain.pb.metafix.opb	394.372	UNSATISFIABLE
normalized-regular-n23-d4-i3.cnf.gz-extracted.pb.metafix.opb	1434.04	UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i3-f.cnf.gz-plain.pb.metafix.opb	5.14295	UNSATISFIABLE
normalized-regular-n29-d4-i2.cnf.gz-extracted.pb.metafix.opb	1798.725	UNKNOWN
normalized-tseitin-regular-n52-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	6.94248	UNSATISFIABLE
normalized-fixed-bandwidth-77.cnf.gz-extracted.pb.metafix.opb	1798.733	UNKNOWN
normalized-tseitin-regular-n44-d3-i2-f.cnf.gz-plain.pb.metafix.opb	0.354447	UNSATISFIABLE
normalized-subsetCardinalitySigma-27-2.cnf.gz-plain.pb.metafix.opb	1798.786	UNKNOWN
normalized-regular-n21-d4-i2.cnf.gz-extracted.pb.metafix.opb	102.262	UNSATISFIABLE
normalized-tseitin-regular-n64-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	3.54503	UNSATISFIABLE
normalized-tseitin-regular-n64-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	4.71033	UNSATISFIABLE
normalized-subsetCardinalitySigma-27-2.cnf.gz-extracted.pb.metafix.opb	1798.550	UNKNOWN
normalized-fixed-bandwidth-73.cnf.gz-extracted.pb.metafix.opb	1800.461	UNKNOWN
normalized-subsetCardinalitySigma-26-2.cnf.gz-extracted.pb.metafix.opb	435.45	UNSATISFIABLE
normalized-tseitin-regular-n48-d3-i2-f.cnf.gz-plain.pb.metafix.opb	4.61746	UNSATISFIABLE
normalized-tseitin-regular-n54-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	1.98222	UNSATISFIABLE
normalized-subsetCardinalitySigma-26-1.cnf.gz-extracted.pb.metafix.opb	1419.76	UNSATISFIABLE
normalized-tseitin-regular-n60-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	2.98216	UNSATISFIABLE
normalized-fixed-bandwidth-62.cnf.gz-extracted.pb.metafix.opb	1798.734	UNKNOWN
normalized-tseitin-regular-n48-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	9.80326	UNSATISFIABLE
normalized-regular-n25-d4-i2.cnf.gz-plain.pb.metafix.opb	1798.765	UNKNOWN
normalized-regular-n25-d4-i3.cnf.gz-plain.pb.metafix.opb	1798.775	UNKNOWN
normalized-regular-n24-d4-i3.cnf.gz-plain.pb.metafix.opb	1798.782	UNKNOWN
normalized-regular-n22-d4-i3.cnf.gz-plain.pb.metafix.opb	367.671	UNSATISFIABLE
normalized-tseitin-regular-n36-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	0.579811	UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i1-f.cnf.gz-plain.pb.metafix.opb	10.078	UNSATISFIABLE
normalized-subsetCardinalitySigma-31-1.cnf.gz-extracted.pb.metafix.opb	1798.754	UNKNOWN
normalized-tseitin-regular-n42-d3-i3-f.cnf.gz-plain.pb.metafix.opb	0.379205	UNSATISFIABLE
normalized-tseitin-regular-n42-d3-i1-f.cnf.gz-plain.pb.metafix.opb	0.964898	UNSATISFIABLE
normalized-regular-n19-d4-i1.cnf.gz-extracted.pb.metafix.opb	69.7193	UNSATISFIABLE
normalized-tseitin-regular-n80-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	934.727	UNSATISFIABLE
normalized-tseitin-regular-n80-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	128.42	UNSATISFIABLE
normalized-subsetCardinalitySigma-23-3.cnf.gz-extracted.pb.metafix.opb	115.078	UNSATISFIABLE
normalized-tseitin-regular-n54-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	0.125591	UNSATISFIABLE
normalized-tseitin-regular-n94-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	1438.88	UNSATISFIABLE
normalized-tseitin-regular-n84-d3-i2-f.cnf.gz-plain.pb.metafix.opb	918.324	UNSATISFIABLE
normalized-regular-n25-d4-i1.cnf.gz-extracted.pb.metafix.opb	1635.71	UNSATISFIABLE
normalized-tseitin-regular-n68-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	58.3361	UNSATISFIABLE
normalized-tseitin-regular-n88-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	574.608	UNSATISFIABLE
normalized-tseitin-regular-n60-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	4.75567	UNSATISFIABLE
normalized-fixed-bandwidth-93.cnf.gz-extracted.pb.metafix.opb	1798.775	UNKNOWN
normalized-regular-n23-d4-i1.cnf.gz-extracted.pb.metafix.opb	212.201	UNSATISFIABLE
normalized-tseitin-regular-n42-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	0.283985	UNSATISFIABLE
normalized-tseitin-regular-n52-d3-i2-f.cnf.gz-plain.pb.metafix.opb	10.3675	UNSATISFIABLE
normalized-regular-n17-d4-i1.cnf.gz-plain.pb.metafix.opb	15.8221	UNSATISFIABLE
normalized-tseitin-regular-n38-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	0.440535	UNSATISFIABLE
normalized-fixed-bandwidth-18.cnf.gz-plain.pb.metafix.opb	329.988	UNSATISFIABLE
normalized-fixed-bandwidth-78.cnf.gz-extracted.pb.metafix.opb	1798.757	UNKNOWN
normalized-tseitin-regular-n96-d3-i3-f.cnf.gz-plain.pb.metafix.opb	1798.810	UNKNOWN
normalized-fixed-bandwidth-90.cnf.gz-extracted.pb.metafix.opb	1798.737	UNKNOWN
normalized-subsetCardinalitySigma-25-2.cnf.gz-plain.pb.metafix.opb	612.188	UNSATISFIABLE
normalized-tseitin-regular-n44-d3-i3-f.cnf.gz-plain.pb.metafix.opb	0.829044	UNSATISFIABLE
normalized-tseitin-regular-n62-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	11.4078	UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i1-r1.cnf.gz-plain.pb.metafix.opb	122.324	UNSATISFIABLE
normalized-regular-n24-d4-i2.cnf.gz-extracted.pb.metafix.opb	841.994	UNSATISFIABLE
normalized-regular-n27-d4-i2.cnf.gz-extracted.pb.metafix.opb	1798.774	UNKNOWN
normalized-tseitin-regular-n58-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	4.9592	UNSATISFIABLE
normalized-regular-n20-d4-i1.cnf.gz-plain.pb.metafix.opb	22.7429	UNSATISFIABLE
normalized-tseitin-regular-n42-d3-i2-f.cnf.gz-plain.pb.metafix.opb	0.180686	UNSATISFIABLE
normalized-tseitin-regular-n40-d3-i1-f.cnf.gz-plain.pb.metafix.opb	0.224746	UNSATISFIABLE
normalized-tseitin-regular-n40-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	1.97784	UNSATISFIABLE
normalized-regular-n22-d4-i3.cnf.gz-extracted.pb.metafix.opb	933.232	UNSATISFIABLE
normalized-subsetCardinalitySigma-28-2.cnf.gz-extracted.pb.metafix.opb	895.177	UNSATISFIABLE
normalized-tseitin-regular-n48-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	0.726273	UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i2-f.cnf.gz-plain.pb.metafix.opb	25.3942	UNSATISFIABLE
normalized-fixed-bandwidth-24.cnf.gz-extracted.pb.metafix.opb	1798.752	UNKNOWN
normalized-subsetCardinalitySigma-26-3.cnf.gz-extracted.pb.metafix.opb	426.724	UNSATISFIABLE
normalized-regular-n24-d4-i2.cnf.gz-plain.pb.metafix.opb	837.127	UNSATISFIABLE
normalized-tseitin-regular-n38-d3-i2-r1.cnf.gz-plain.pb.metafix.opb	0.43819	UNSATISFIABLE
normalized-subsetCardinalitySigma-26-2.cnf.gz-plain.pb.metafix.opb	370.765	UNSATISFIABLE
normalized-tseitin-regular-n46-d3-i3-r2.cnf.gz-plain.pb.metafix.opb	0.806019	UNSATISFIABLE
normalized-tseitin-regular-n46-d3-i2-r2.cnf.gz-plain.pb.metafix.opb	1.29223	UNSATISFIABLE
normalized-tseitin-regular-n60-d3-i3-r1.cnf.gz-plain.pb.metafix.opb	16.7667	UNSATISFIABLE
normalized-fixed-bandwidth-25.cnf.gz-extracted.pb.metafix.opb	1798.794	UNKNOWN
normalized-tseitin-regular-n92-d3-i1-r2.cnf.gz-plain.pb.metafix.opb	650.467	UNSATISFIABLE
normalized-regular-n28-d4-i3.cnf.gz-plain.pb.metafix.opb	1769.86	UNSATISFIABLE
normalized-fixed-bandwidth-15.cnf.gz-plain.pb.metafix.opb	37.6879	UNSATISFIABLE
normalized-subsetCardinalitySigma-27-3.cnf.gz-plain.pb.metafix.opb	461.548	UNSATISFIABLE
normalized-129.opb	1798.657	UNKNOWN
normalized-41.opb	383.181	SATISFIABLE
normalized-130.opb	1798.664	UNKNOWN
normalized-137.opb	1798.628	UNKNOWN
normalized-185.opb	1419.68	SATISFIABLE
normalized-20.opb	1798.643	UNKNOWN
normalized-112.opb	1798.727	UNKNOWN
normalized-24.opb	1798.665	UNKNOWN
normalized-37.opb	1798.687	UNKNOWN
normalized-70.opb	1798.647	UNKNOWN
normalized-154.opb	1798.667	UNKNOWN
normalized-178.opb	1800.458	UNKNOWN
normalized-40.opb	1798.651	UNKNOWN
normalized-141.opb	1798.712	UNKNOWN
normalized-173.opb	1798.548	UNKNOWN
normalized-117.opb	70.444	SATISFIABLE
normalized-175.opb	1798.582	UNKNOWN
normalized-73.opb	1800.430	UNKNOWN
normalized-164.opb	990.322	SATISFIABLE
normalized-89.opb	1798.667	UNKNOWN
normalized-146.opb	1798.674	UNKNOWN
normalized-123.opb	1798.710	UNKNOWN
normalized-05.opb	1798.665	UNKNOWN
normalized-147.opb	1798.680	UNKNOWN
normalized-48.opb	1177.6	SATISFIABLE
normalized-47.opb	1798.637	UNKNOWN
normalized-21.opb	1798.697	UNKNOWN
normalized-172.opb	1798.542	UNKNOWN
normalized-60.opb	1798.692	UNKNOWN
normalized-91.opb	1798.636	UNKNOWN
normalized-188.opb	3.37017	UNSATISFIABLE
normalized-53.opb	1798.630	UNKNOWN
normalized-122.opb	1800.437	UNKNOWN
normalized-107.opb	105.115	SATISFIABLE
normalized-99.opb	1011.11	UNSATISFIABLE
normalized-153.opb	1798.658	UNKNOWN
normalized-27.opb	1798.593	UNKNOWN
normalized-116.opb	1798.654	UNKNOWN
normalized-167.opb	1798.633	UNKNOWN
normalized-101.opb	1798.686	UNKNOWN
normalized-61.opb	1798.627	UNKNOWN
normalized-184.opb	1798.347	UNKNOWN
normalized-135.opb	1798.652	UNKNOWN
normalized-170.opb	687.528	SATISFIABLE
normalized-76.opb	1798.687	UNKNOWN
normalized-162.opb	222.314	SATISFIABLE
normalized-181.opb	1798.482	UNKNOWN
normalized-120.opb	1798.682	UNKNOWN
normalized-180.opb	1798.539	UNKNOWN
normalized-31.opb	1798.660	UNKNOWN
normalized-182.opb	1798.375	UNKNOWN
normalized-j3017_6-sat.opb	0.048026	SATISFIABLE
normalized-j3030_6-sat.opb	0.863582	SATISFIABLE
normalized-j3048_8-sat.opb	0.282908	SATISFIABLE
normalized-j3025_7-sat.opb	0.386869	SATISFIABLE
normalized-j308_1-unsat.opb	0.056994	UNSATISFIABLE
normalized-j3029_8-unsat.opb	31.8707	UNSATISFIABLE
normalized-j3024_3-sat.opb	0.130905	SATISFIABLE
normalized-j3027_8-sat.opb	0.191747	SATISFIABLE
normalized-j307_10-sat.opb	0.098391	SATISFIABLE
normalized-j3029_6-sat.opb	18.073	SATISFIABLE
normalized-j307_9-unsat.opb	0.075027	UNSATISFIABLE
normalized-j3024_5-sat.opb	0.09211	SATISFIABLE
normalized-j3024_4-sat.opb	0.098789	SATISFIABLE
normalized-j308_6-unsat.opb	0.064623	UNSATISFIABLE
normalized-j3041_4-unsat.opb	0.451157	UNSATISFIABLE
normalized-j301_4-unsat.opb	0.040685	UNSATISFIABLE
normalized-j3031_7-sat.opb	0.313709	SATISFIABLE
normalized-j3037_5-sat.opb	0.146053	SATISFIABLE
normalized-j309_10-unsat.opb	0.997043	UNSATISFIABLE
normalized-j309_6-sat.opb	0.312988	SATISFIABLE
normalized-j3046_4-unsat.opb	0.29829	UNSATISFIABLE
normalized-j3025_1-sat.opb	0.804118	SATISFIABLE
normalized-j3024_2-sat.opb	0.119179	SATISFIABLE
normalized-j309_9-sat.opb	0.511683	SATISFIABLE
normalized-j308_6-sat.opb	0.102313	SATISFIABLE
normalized-j3025_10-sat.opb	0.197562	SATISFIABLE
normalized-j3043_8-sat.opb	0.224283	SATISFIABLE
normalized-j3042_5-unsat.opb	0.10485	UNSATISFIABLE
normalized-j3011_9-unsat.opb	0.131106	UNSATISFIABLE
normalized-j3020_1-sat.opb	0.053484	SATISFIABLE
normalized-j605_7-sat.opb	1.30688	SATISFIABLE
normalized-j605_1-unsat.opb	10.928	UNSATISFIABLE
normalized-j607_4-unsat.opb	0.264212	UNSATISFIABLE
normalized-j605_10-unsat.opb	29.9268	UNSATISFIABLE
normalized-j6027_4-unsat.opb	0.53576	UNSATISFIABLE
normalized-j6010_7-unsat.opb	0.49752	UNSATISFIABLE
normalized-j606_1-unsat.opb	0.211149	UNSATISFIABLE
normalized-j6041_4-sat.opb	7.03542	SATISFIABLE
normalized-j6040_1-sat.opb	0.630513	SATISFIABLE
normalized-j6030_9-unsat.opb	0.945498	UNSATISFIABLE
normalized-j6048_4-sat.opb	1.5703	SATISFIABLE
normalized-j6029_8-unsat.opb	1798.549	UNKNOWN
normalized-j6027_9-unsat.opb	0.624796	UNSATISFIABLE
normalized-j6020_9-sat.opb	0.16509	SATISFIABLE
normalized-j6028_7-sat.opb	1.60624	SATISFIABLE
normalized-j6014_2-sat.opb	2.70698	SATISFIABLE
normalized-j602_7-unsat.opb	0.097295	UNSATISFIABLE
normalized-j6040_10-sat.opb	0.525763	SATISFIABLE
normalized-j6030_8-sat.opb	2.22431	SATISFIABLE
normalized-j6022_1-sat.opb	0.374355	SATISFIABLE
normalized-j6013_2-unsat.opb	1798.632	UNKNOWN
normalized-j6015_4-sat.opb	2.36644	SATISFIABLE
normalized-j601_8-unsat.opb	0.103912	UNSATISFIABLE
normalized-j6018_3-sat.opb	0.15443	SATISFIABLE
normalized-j6016_10-unsat.opb	1.20223	UNSATISFIABLE
normalized-j6032_1-unsat.opb	1.43746	UNSATISFIABLE
normalized-j6033_2-unsat.opb	0.12555	UNSATISFIABLE
normalized-j603_2-unsat.opb	0.103308	UNSATISFIABLE
normalized-j6028_9-unsat.opb	0.774301	UNSATISFIABLE
normalized-j6010_2-unsat.opb	0.518414	UNSATISFIABLE
normalized-j6035_10-sat.opb	0.160802	SATISFIABLE
normalized-j6040_3-sat.opb	0.572866	SATISFIABLE
normalized-j6043_4-sat.opb	1.07234	SATISFIABLE
normalized-j6042_2-sat.opb	0.793927	SATISFIABLE
normalized-j12049_6-unsat.opb	1.08552	UNSATISFIABLE
normalized-j12041_4-unsat.opb	2.66046	UNSATISFIABLE
normalized-j12056_10-unsat.opb	1798.590	UNKNOWN
normalized-j12023_3-unsat.opb	0.343283	UNSATISFIABLE
normalized-j12038_8-unsat.opb	1798.500	UNKNOWN
normalized-j12034_4-sat.opb	5.51194	SATISFIABLE
normalized-j1208_6-sat.opb	1501.37	SATISFIABLE
normalized-j12058_4-sat.opb	1798.529	UNKNOWN
normalized-j12032_3-unsat.opb	1798.594	UNKNOWN
normalized-j1204_7-sat.opb	0.55676	SATISFIABLE
normalized-j1209_4-sat.opb	98.875	SATISFIABLE
normalized-j12047_6-sat.opb	1798.586	UNKNOWN
normalized-j12035_4-sat.opb	4.98545	SATISFIABLE
normalized-j12046_2-sat.opb	1798.576	UNKNOWN
normalized-j12027_7-unsat.opb	14.2555	UNSATISFIABLE
normalized-j12033_3-sat.opb	1798.595	UNKNOWN
normalized-j12022_9-sat.opb	0.588862	SATISFIABLE
normalized-j12059_3-unsat.opb	3.49761	UNSATISFIABLE
normalized-j1208_10-unsat.opb	1798.561	UNKNOWN
normalized-j12038_7-unsat.opb	1798.516	UNKNOWN
normalized-j1203_2-sat.opb	0.464824	SATISFIABLE
normalized-j12036_4-sat.opb	1798.601	UNKNOWN
normalized-j12038_3-sat.opb	1798.553	UNKNOWN
normalized-j12010_10-sat.opb	1.97567	SATISFIABLE
normalized-j12016_4-sat.opb	1798.623	UNKNOWN
normalized-j12037_7-sat.opb	1798.536	UNKNOWN
normalized-j1205_1-unsat.opb	0.356156	UNSATISFIABLE
normalized-j12048_4-unsat.opb	1800.448	UNKNOWN
normalized-j12015_3-unsat.opb	2.01395	UNSATISFIABLE
normalized-j12045_10-sat.opb	0.559113	SATISFIABLE
normalized-j1201_5-sat.opb	1.08709	SATISFIABLE
normalized-j12026_5-unsat.opb	431.057	UNSATISFIABLE
normalized-j12032_8-unsat.opb	1798.601	UNKNOWN
normalized-j1206_8-unsat.opb	255.469	UNSATISFIABLE
normalized-j1206_6-sat.opb	1798.637	UNKNOWN
normalized-j12039_7-sat.opb	1798.523	UNKNOWN
normalized-j1205_3-unsat.opb	0.303876	UNSATISFIABLE
normalized-j12021_4-sat.opb	3.09785	SATISFIABLE
normalized-j12052_5-unsat.opb	1798.632	UNKNOWN
normalized-j12036_3-sat.opb	1798.608	UNKNOWN
normalized-j12028_8-sat.opb	1115.44	SATISFIABLE
normalized-j12013_1-unsat.opb	1.85211	UNSATISFIABLE
normalized-j12047_10-unsat.opb	1798.638	UNKNOWN
normalized-j9015_10-unsat.opb	2.28811	UNSATISFIABLE
normalized-j9040_1-unsat.opb	0.817201	UNSATISFIABLE
normalized-j9010_8-sat.opb	2.55756	SATISFIABLE
normalized-j9010_10-unsat.opb	1.09668	UNSATISFIABLE
normalized-j9015_7-unsat.opb	2.50952	UNSATISFIABLE
normalized-j9043_2-sat.opb	2.29364	SATISFIABLE
normalized-j901_6-sat.opb	0.321089	SATISFIABLE
normalized-j9042_4-sat.opb	2.5225	SATISFIABLE
normalized-j907_8-unsat.opb	0.66645	UNSATISFIABLE
normalized-j9045_1-sat.opb	1798.573	UNKNOWN
normalized-j9048_1-unsat.opb	3.51045	UNSATISFIABLE
normalized-j9012_5-sat.opb	4.02847	SATISFIABLE
normalized-j9028_2-unsat.opb	1.87794	UNSATISFIABLE
normalized-j9039_3-unsat.opb	0.711623	UNSATISFIABLE
normalized-j905_6-unsat.opb	6.39282	UNSATISFIABLE
normalized-j9035_5-sat.opb	0.407079	SATISFIABLE
normalized-j9042_5-sat.opb	2.64532	SATISFIABLE
normalized-j906_2-sat.opb	1.15701	SATISFIABLE
normalized-j9016_7-sat.opb	4.79174	SATISFIABLE
normalized-j9012_2-unsat.opb	2.01214	UNSATISFIABLE
normalized-j9048_9-sat.opb	4.8499	SATISFIABLE
normalized-j903_10-unsat.opb	0.191651	UNSATISFIABLE
normalized-j9010_6-unsat.opb	1.31872	UNSATISFIABLE
normalized-j9014_1-unsat.opb	2.135	UNSATISFIABLE
normalized-j902_5-sat.opb	0.38599	SATISFIABLE
normalized-j9038_3-unsat.opb	0.872743	UNSATISFIABLE
normalized-j9027_5-sat.opb	3.72974	SATISFIABLE
normalized-j908_8-unsat.opb	0.883422	UNSATISFIABLE
normalized-j9035_1-unsat.opb	0.279262	UNSATISFIABLE
normalized-j9040_1-sat.opb	1.37294	SATISFIABLE
normalized-1096.cudf.paranoid.opb	0.00083	SATISFIABLE
normalized-NG_K131.opb	1798.710	UNKNOWN
normalized-NG_K132.opb	1798.731	UNKNOWN
normalized-NG_K152.opb	1798.720	UNKNOWN
normalized-NG_K129.opb	1798.715	UNKNOWN
normalized-NG_K143.opb	1798.718	UNKNOWN
normalized-NG_K168.opb	1798.741	UNKNOWN
normalized-NG_K183.opb	1798.706	UNKNOWN
normalized-NG_K200.opb	1798.693	UNKNOWN
normalized-NG_K125.opb	1798.732	UNKNOWN
normalized-NG_K167.opb	1798.698	UNKNOWN
normalized-NG_K156.opb	1798.723	UNKNOWN
normalized-NG_K139.opb	1798.698	UNKNOWN
normalized-NG_K175.opb	1798.706	UNKNOWN
normalized-NG_K160.opb	1798.711	UNKNOWN
normalized-NG_K196.opb	1798.696	UNKNOWN
normalized-NG_K192.opb	1798.688	UNKNOWN
normalized-NG_K126.opb	1798.720	UNKNOWN
normalized-NG_K164.opb	1798.709	UNKNOWN
normalized-NG_K128.opb	1798.691	UNKNOWN
normalized-NG_K140.opb	1798.711	UNKNOWN
normalized-NG_K176.opb	1798.715	UNKNOWN
normalized-NG_K199.opb	1798.710	UNKNOWN
normalized-NG_K138.opb	1798.724	UNKNOWN
normalized-NG_K180.opb	1798.738	UNKNOWN
normalized-NG_K163.opb	1798.671	UNKNOWN
normalized-NG_K148.opb	1798.703	UNKNOWN
normalized-NG_K141.opb	1798.715	UNKNOWN
normalized-NG_K181.opb	1800.456	UNKNOWN
normalized-NG_K133.opb	1800.275	UNKNOWN
normalized-NG_K177.opb	1798.681	UNKNOWN
normalized-BeauxArts_K75.opb	44.345	SATISFIABLE
normalized-BeauxArts_K73.opb	123.889	SATISFIABLE
normalized-BeauxArts_K80.opb	33.0458	SATISFIABLE
normalized-BeauxArts_K70.opb	171.899	SATISFIABLE
normalized-BeauxArts_K68.opb	710.714	SATISFIABLE
normalized-BeauxArts_K69.opb	198.924	SATISFIABLE
normalized-BeauxArts_K72.opb	55.9807	SATISFIABLE
normalized-BeauxArts_K77.opb	47.0544	SATISFIABLE
normalized-BeauxArts_K66.opb	1798.751	UNKNOWN
normalized-BeauxArts_K65.opb	1798.722	UNKNOWN
normalized-BeauxArts_K67.opb	72.4757	SATISFIABLE
normalized-BeauxArts_K76.opb	31.2581	SATISFIABLE
normalized-BeauxArts_K78.opb	10.3198	SATISFIABLE
normalized-BeauxArts_K74.opb	101.463	SATISFIABLE
normalized-BeauxArts_K71.opb	56.4357	SATISFIABLE
normalized-BeauxArts_K79.opb	8.77256	SATISFIABLE
normalized-TateBritain_K104.opb	1798.733	UNKNOWN
normalized-TateBritain_K84.opb	1798.739	UNKNOWN
normalized-TateBritain_K86.opb	1798.742	UNKNOWN
normalized-TateBritain_K102.opb	1798.766	UNKNOWN
normalized-TateBritain_K98.opb	1798.760	UNKNOWN
normalized-TateBritain_K97.opb	1798.649	UNKNOWN
normalized-TateBritain_K93.opb	1798.573	UNKNOWN
normalized-TateBritain_K94.opb	1798.760	UNKNOWN
normalized-TateBritain_K87.opb	1798.754	UNKNOWN
normalized-TateBritain_K85.opb	1798.758	UNKNOWN
normalized-TateBritain_K83.opb	1800.518	UNKNOWN
normalized-TateBritain_K101.opb	1309.01	SATISFIABLE
normalized-TateBritain_K96.opb	1798.781	UNKNOWN
normalized-TateBritain_K95.opb	1798.703	UNKNOWN
normalized-TateBritain_K99.opb	1798.734	UNKNOWN
normalized-TateBritain_K107.opb	1798.784	UNKNOWN
normalized-TateBritain_K108.opb	1798.715	UNKNOWN
normalized-TateBritain_K80.opb	1798.750	UNKNOWN
normalized-TateBritain_K82.opb	1798.686	UNKNOWN
normalized-TateBritain_K109.opb	597.682	SATISFIABLE
normalized-TateBritain_K81.opb	1798.746	UNKNOWN
normalized-TateBritain_K88.opb	1798.749	UNKNOWN
normalized-TateBritain_K103.opb	1798.747	UNKNOWN
normalized-TateBritain_K89.opb	1798.724	UNKNOWN
normalized-TateBritain_K106.opb	1798.725	UNKNOWN
normalized-TateBritain_K90.opb	1798.707	UNKNOWN
normalized-TateBritain_K105.opb	1798.763	UNKNOWN
normalized-TateBritain_K91.opb	1798.708	UNKNOWN
normalized-TateBritain_K100.opb	1798.753	UNKNOWN
normalized-TateBritain_K92.opb	1798.756	UNKNOWN
normalized-neos-849702.opb	410.644	SATISFIABLE
normalized-neos808444.opb	1.66116	SATISFIABLE
normalized-neos-820157.opb	1798.748	UNKNOWN
normalized-neos-820146.opb	1798.761	UNKNOWN
normalized-fpga14_12_sat_pb.cnf.cr.opb	0.019628	SATISFIABLE
normalized-chnl10_20_pb.cnf.cr.opb	9.44571	UNSATISFIABLE
normalized-fpga30_29_sat_pb.cnf.cr.opb	0.062348	SATISFIABLE
normalized-fpga15_13_sat_pb.cnf.cr.opb	0.021504	SATISFIABLE
normalized-fpga25_25_sat_pb.cnf.cr.opb	0.13941	SATISFIABLE
normalized-fpga11_10_sat_pb.cnf.cr.opb	0.014803	SATISFIABLE
normalized-chnl15_20_pb.cnf.cr.opb	1798.738	UNKNOWN
normalized-fpga13_13_sat_pb.cnf.cr.opb	0.026923	SATISFIABLE
normalized-fpga11_9_sat_pb.cnf.cr.opb	0.013992	SATISFIABLE
normalized-fpga35_33_sat_pb.cnf.cr.opb	0.289315	SATISFIABLE
normalized-fpga10_10_sat_pb.cnf.cr.opb	0.010956	SATISFIABLE
normalized-chnl30_35_pb.cnf.cr.opb	1800.463	UNKNOWN
normalized-chnl15_25_pb.cnf.cr.opb	1798.736	UNKNOWN
normalized-fpga35_35_sat_pb.cnf.cr.opb	0.121109	SATISFIABLE
normalized-chnl20_21_pb.cnf.cr.opb	1798.742	UNKNOWN
normalized-chnl30_40_pb.cnf.cr.opb	1798.751	UNKNOWN
normalized-fpga45_43_sat_pb.cnf.cr.opb	0.387527	SATISFIABLE
normalized-chnl10_11_pb.cnf.cr.opb	172.005	UNSATISFIABLE
normalized-fpga14_13_sat_pb.cnf.cr.opb	0.021266	SATISFIABLE
normalized-fpga10_8_sat_pb.cnf.cr.opb	0.018855	SATISFIABLE
normalized-fpga15_14_sat_pb.cnf.cr.opb	0.039727	SATISFIABLE
normalized-fpga30_28_sat_pb.cnf.cr.opb	0.075149	SATISFIABLE
normalized-fpga30_30_sat_pb.cnf.cr.opb	0.176369	SATISFIABLE
normalized-chnl40_50_pb.cnf.cr.opb	1798.604	UNKNOWN
normalized-fpga40_39_sat_pb.cnf.cr.opb	0.398925	SATISFIABLE
normalized-chnl50_55_pb.cnf.cr.opb	1798.742	UNKNOWN
normalized-chnl10_15_pb.cnf.cr.opb	22.8498	UNSATISFIABLE
normalized-fpga12_10_sat_pb.cnf.cr.opb	0.009818	SATISFIABLE
normalized-chnl20_30_pb.cnf.cr.opb	1798.748	UNKNOWN
normalized-chnl35_36_pb.cnf.cr.opb	1798.748	UNKNOWN
normalized-fpga45_45_sat_pb.cnf.cr.opb	0.598885	SATISFIABLE
normalized-fpga20_20_sat_pb.cnf.cr.opb	0.032904	SATISFIABLE
normalized-fpga15_15_sat_pb.cnf.cr.opb	0.048891	SATISFIABLE
normalized-fpga13_11_sat_pb.cnf.cr.opb	0.015821	SATISFIABLE
normalized-fpga20_18_sat_pb.cnf.cr.opb	0.046481	SATISFIABLE
normalized-fpga12_11_sat_pb.cnf.cr.opb	0.014478	SATISFIABLE
normalized-chnl40_41_pb.cnf.cr.opb	1798.740	UNKNOWN
normalized-fpga45_44_sat_pb.cnf.cr.opb	0.27602	SATISFIABLE
normalized-chnl30_31_pb.cnf.cr.opb	1798.746	UNKNOWN
normalized-chnl20_25_pb.cnf.cr.opb	1798.672	UNKNOWN
normalized-chnl50_60_pb.cnf.cr.opb	1798.634	UNKNOWN
normalized-fpga25_24_sat_pb.cnf.cr.opb	0.712386	SATISFIABLE
normalized-fpga12_12_sat_pb.cnf.cr.opb	0.015348	SATISFIABLE
normalized-fpga25_23_sat_pb.cnf.cr.opb	0.114201	SATISFIABLE
normalized-chnl35_40_pb.cnf.cr.opb	1798.605	UNKNOWN
normalized-chnl15_16_pb.cnf.cr.opb	1798.706	UNKNOWN
normalized-fpga10_9_sat_pb.cnf.cr.opb	0.020759	SATISFIABLE
normalized-chnl35_45_pb.cnf.cr.opb	1798.761	UNKNOWN
normalized-fpga13_12_sat_pb.cnf.cr.opb	0.019022	SATISFIABLE
normalized-fpga35_34_sat_pb.cnf.cr.opb	0.098469	SATISFIABLE
normalized-fpga40_38_sat_pb.cnf.cr.opb	0.243906	SATISFIABLE
normalized-chnl50_51_pb.cnf.cr.opb	1798.745	UNKNOWN
normalized-fpga11_11_sat_pb.cnf.cr.opb	0.022111	SATISFIABLE
normalized-fpga40_40_sat_pb.cnf.cr.opb	0.344437	SATISFIABLE
normalized-fpga20_19_sat_pb.cnf.cr.opb	0.02999	SATISFIABLE
normalized-chnl40_45_pb.cnf.cr.opb	1798.787	UNKNOWN
normalized-fpga14_14_sat_pb.cnf.cr.opb	0.172366	SATISFIABLE
normalized-ppp:1,3-13,19.opb	37.2329	SATISFIABLE
normalized-ppp:1-11,19,21.opb	1798.736	UNKNOWN
normalized-ppp:1-12,16.opb	0.254777	SATISFIABLE
normalized-ppp:1-13.opb	2.85147	SATISFIABLE
normalized-ppp:3-13,25,26.opb	1798.653	UNKNOWN
normalized-ppp:1-9,16-19.opb	1798.752	UNKNOWN
normalized-cache-ibm-q-unbounded.Ih1arity.ucl.opb	534.75	UNSATISFIABLE
normalized-ooo.ex.mem.LdValue.ucl.opb	299.89	UNSATISFIABLE
normalized-46s.smv.opb	0.119027	UNSATISFIABLE
normalized-ooo.rf6.ucl.opb	0.057962	UNSATISFIABLE
normalized-ooo.tag12.ucl.opb	14.0722	UNSATISFIABLE
normalized-elf.rf7.ucl.opb	0.033607	UNSATISFIABLE
normalized-25s.smv.opb	0.222785	UNSATISFIABLE
normalized-ooo.ex.br.mem.Src1Valid_Src1ValidBar.ucl.opb	374.375	UNSATISFIABLE
normalized-cache.inv12.ucl.opb	12.2358	UNSATISFIABLE
normalized-dlx1c.rwmem.ucl.opb	0.779962	UNSATISFIABLE
normalized-ooo.burch_dill.3.accl.ucl.opb	6.08327	UNSATISFIABLE
normalized-elf.rf10.ucl.opb	5.06762	UNSATISFIABLE
normalized-ooo.unbounded.all.ucl.opb	281.811	UNSATISFIABLE
normalized-44s.smv.opb	0.048738	UNSATISFIABLE
normalized-ooo.ex.br.mem.RobRegValid_bar.ucl.opb	36.1868	UNSATISFIABLE
normalized-ooo.rf8.ucl.opb	0.794307	UNSATISFIABLE
normalized-ooo.burch_dill.6.accl.ucl.opb	1798.707	UNKNOWN
normalized-blast-floppy1-8.ucl.opb	0.127949	UNSATISFIABLE
normalized-blast-floppy1-6.ucl.opb	0.115536	UNSATISFIABLE
normalized-cache-ibm-q-full.all.ucl.opb	638.27	UNSATISFIABLE
normalized-ooo.tag8.ucl.opb	0.798964	UNSATISFIABLE
normalized-cache.inv10.ucl.opb	0.083883	UNSATISFIABLE
normalized-cache-ibm-q-unbounded.Ic22arity.ucl.opb	18.9649	UNSATISFIABLE
normalized-22s.smv.opb	0.325285	UNSATISFIABLE
normalized-cache-ibm-q-unbounded.Ih2arity.ucl.opb	1.35851	SATISFIABLE
normalized-dlx1c.rwmem1.ucl.opb	0.691607	UNSATISFIABLE
normalized-elf.rf9.ucl.opb	0.6587	UNSATISFIABLE
normalized-ooo.rf10.ucl.opb	14.3122	UNSATISFIABLE
normalized-cache.inv8.ucl.opb	0.027593	UNSATISFIABLE
normalized-ooo.burch_dill.4.accl.ucl.opb	0.2365	UNSATISFIABLE
normalized-ooo.burch_dill.2.accl.ucl.opb	1.87888	UNSATISFIABLE
normalized-cache-ibm-q-unbounded.Icl2arity.ucl.opb	1.51723	UNSATISFIABLE
normalized-ooo.ex.mem.LsqHdStrong.ucl.opb	1065.98	UNSATISFIABLE
normalized-elf.rf8.ucl.opb	0.138068	UNSATISFIABLE
normalized-elf.rf6.ucl.opb	0.002164	UNSATISFIABLE
normalized-ooo.rf7.ucl.opb	0.162902	UNSATISFIABLE
normalized-ooo.tag10.ucl.opb	4.52291	UNSATISFIABLE
normalized-43s.smv.opb	0.551641	UNSATISFIABLE
normalized-ooo.burch_dill.8.accl.ucl.opb	390.694	UNSATISFIABLE
normalized-dlx1c.ucl.opb	0.294722	UNSATISFIABLE
normalized-ooo.rf9.ucl.opb	2.34783	UNSATISFIABLE
normalized-blast-floppy1-3.ucl.opb	0.008707	UNSATISFIABLE
normalized-blast-floppy1-7.ucl.opb	0.116516	UNSATISFIABLE
normalized-blast-floppy1-2.ucl.opb	0.026042	UNSATISFIABLE
normalized-ooo.tag14.ucl.opb	60.8003	UNSATISFIABLE
normalized-blast-floppy1-4.ucl.opb	0.004608	UNSATISFIABLE
normalized-cache.inv14.ucl.opb	1085.96	UNSATISFIABLE
normalized-blast-tlan3.ucl.opb	0.406604	UNSATISFIABLE
normalized-37s.smv.opb	0.059139	UNSATISFIABLE
normalized-blast-tlan2.ucl.opb	0.075923	UNSATISFIABLE
normalized-reduced-prob2.opb	1.28261	SATISFIABLE
normalized-reduced-prob3.opb	8.97472	SATISFIABLE
normalized-reduced-prob5.opb	1.49604	SATISFIABLE
normalized-reduced-cuww2.opb	1.82286	SATISFIABLE
normalized-reduced-prob8.opb	11.1116	SATISFIABLE
normalized-reduced-prob6.opb	1.74289	SATISFIABLE
normalized-reduced-prob4.opb	1.27194	SATISFIABLE
normalized-reduced-prob7.opb	4.67351	SATISFIABLE
normalized-reduced-cuww1.opb	11.6928	SATISFIABLE
normalized-reduced-cuww3.opb	490.202	SATISFIABLE
normalized-reduced-prob10.opb	1.46391	SATISFIABLE
normalized-reduced-cuww5.opb	UNKNOWN
normalized-reduced-prob1.opb	1.95786	SATISFIABLE
normalized-reduced-cuww4.opb	11.8969	SATISFIABLE
normalized-dbst_v30_e350_d15_mw10_2.opb.PB06.opb	3.07613	SATISFIABLE
normalized-dbst_v50_e1000_d25_mw10_5.opb.PB06.opb	40.3817	SATISFIABLE
normalized-dbst_v40_e600_d20_mw10_9.opb.PB06.opb	10.2114	SATISFIABLE
normalized-dbst_v40_e600_d20_mw10_6.opb.PB06.opb	9.47951	SATISFIABLE
normalized-dbst_v50_e1000_d25_mw10_1.opb.PB06.opb	22.2	SATISFIABLE
normalized-dbst_v40_e600_d20_mw10_0.opb.PB06.opb	8.80961	SATISFIABLE
normalized-dbst_v30_e350_d15_mw10_8.opb.PB06.opb	3.33397	SATISFIABLE
normalized-dbst_v30_e350_d15_mw10_3.opb.PB06.opb	3.45612	SATISFIABLE
normalized-dbst_v40_e600_d20_mw10_5.opb.PB06.opb	9.31875	SATISFIABLE
normalized-dbst_v50_e1000_d25_mw10_3.opb.PB06.opb	35.0218	SATISFIABLE
normalized-dbst_v30_e350_d15_mw10_9.opb.PB06.opb	3.25199	SATISFIABLE
normalized-dbst_v30_e350_d15_mw10_1.opb.PB06.opb	3.09975	SATISFIABLE
normalized-dbst_v50_e1000_d25_mw10_9.opb.PB06.opb	25.0612	SATISFIABLE
normalized-dbst_v50_e1000_d25_mw10_6.opb.PB06.opb	28.008	SATISFIABLE
normalized-dbst_v40_e600_d20_mw10_2.opb.PB06.opb	8.33812	SATISFIABLE
normalized-vdw_k4_l4_n360.opb	1798.705	UNKNOWN
normalized-vdw_k5_l4_n750.opb	1798.711	UNKNOWN
normalized-vdw_k3_l6_n1500.opb	2.62485	SATISFIABLE
normalized-vdw_k3_l5_n550.opb	706.262	SATISFIABLE
normalized-vdw_k6_l3_n170.opb	1798.734	UNKNOWN
normalized-pigeon-cardinality-41-40.opb	1798.711	UNKNOWN
normalized-pigeon-cardinality-55-50.opb	1800.463	UNKNOWN
normalized-pigeon-cardinality-45-40.opb	1798.765	UNKNOWN
normalized-pigeon-cardinality-11-10.opb	222.035	UNSATISFIABLE
normalized-pigeon-cardinality-95-90.opb	1798.724	UNKNOWN
normalized-pigeon-cardinality-61-60.opb	1798.649	UNKNOWN
normalized-pigeon-cardinality-51-50.opb	1798.751	UNKNOWN
normalized-pigeon-cardinality-65-60.opb	1798.608	UNKNOWN
normalized-pigeon-cardinality-31-30.opb	1798.741	UNKNOWN
normalized-pigeon-cardinality-91-90.opb	1798.725	UNKNOWN
normalized-pigeon-cardinality-15-10.opb	47.0763	UNSATISFIABLE
normalized-pigeon-cardinality-21-20.opb	1798.773	UNKNOWN
normalized-pigeon-cardinality-75-70.opb	1798.553	UNKNOWN
normalized-pigeon-cardinality-85-80.opb	1798.740	UNKNOWN
normalized-pigeon-cardinality-25-20.opb	1798.736	UNKNOWN
normalized-pigeon-cardinality-81-80.opb	1798.631	UNKNOWN
normalized-pigeon-cardinality-71-70.opb	1798.730	UNKNOWN
normalized-pigeon-cardinality-101-100.opb	1798.605	UNKNOWN
normalized-pigeon-cardinality-105-100.opb	1798.749	UNKNOWN
normalized-pigeon-cardinality-35-30.opb	1798.786	UNKNOWN
normalized-army11.17bt.opb	4.46871	SATISFIABLE
normalized-army10.14ls.opb	67.5453	SATISFIABLE
normalized-army11.17ls.opb	185.516	SATISFIABLE
normalized-army12.21bt.opb	1798.579	UNKNOWN
normalized-army9.12bt.opb	209.49	SATISFIABLE
normalized-army9.12ls.opb	19.9688	SATISFIABLE
normalized-army13.24ls.opb	1798.606	UNKNOWN
normalized-army8.9bt.opb	1.55658	SATISFIABLE
normalized-army10.14bt.opb	131.961	SATISFIABLE
normalized-army12.21ls.opb	1798.754	UNKNOWN
normalized-army13.24bt.opb	1798.596	UNKNOWN
normalized-army8.9ls.opb	2.6272	SATISFIABLE
normalized-robin14.opb	1798.710	UNKNOWN
normalized-robin12.opb	587.709	SATISFIABLE
normalized-robin16.opb	1798.674	UNKNOWN
normalized-robin8.opb	0.224741	SATISFIABLE
normalized-robin18.opb	1798.692	UNKNOWN
normalized-robin10.opb	0.571878	SATISFIABLE
normalized-t3002.11tsp11.1900561384.opb	0.494624	SATISFIABLE
normalized-t3002.11tsp11.1900581320.opb	543.106	UNSATISFIABLE
normalized-t3002.11tsp11.1900567985.opb	1179.74	UNSATISFIABLE
normalized-t3002.11tsp11.1900562192.opb	227.178	UNSATISFIABLE
normalized-t3002.11tsp11.1900565527.opb	11.0336	SATISFIABLE
normalized-t3002.11tsp11.1900576918.opb	0.446285	SATISFIABLE
normalized-t3002.11tsp11.1900574864.opb	265.655	UNSATISFIABLE
normalized-t3002.11tsp11.1900547416.opb	1.55583	SATISFIABLE
normalized-t3002.11tsp11.1900582376.opb	0.513037	SATISFIABLE
normalized-t3002.11tsp11.1900574974.opb	0.137793	SATISFIABLE
normalized-t3002.11tsp11.1900550006.opb	899.463	UNSATISFIABLE
normalized-t3002.11tsp11.1900576360.opb	183.01	UNSATISFIABLE
normalized-t3002.11tsp11.1900553812.opb	108.405	UNSATISFIABLE
normalized-t3002.11tsp11.1900584219.opb	366.056	UNSATISFIABLE
normalized-t3002.11tsp11.1900549974.opb	2.85116	SATISFIABLE
normalized-t3002.11tsp11.1900554154.opb	1.05995	SATISFIABLE
normalized-t3002.11tsp11.1900567003.opb	1.19068	SATISFIABLE
normalized-t3002.11tsp11.1900670167.opb	270.44	UNSATISFIABLE
normalized-t3002.11tsp11.1900546076.opb	16.9079	UNSATISFIABLE
normalized-t3002.11tsp11.1900547334.opb	0.108859	SATISFIABLE
normalized-t3002.11tsp11.1900569834.opb	211.537	UNSATISFIABLE
normalized-t3002.11tsp11.1900568952.opb	0.666092	SATISFIABLE
normalized-t3002.11tsp11.1900570242.opb	178.583	UNSATISFIABLE
normalized-t3002.11tsp11.1900566151.opb	0.335508	SATISFIABLE
normalized-t3002.11tsp11.1900552288.opb	336.27	UNSATISFIABLE
normalized-t3002.11tsp11.1900552735.opb	315.88	UNSATISFIABLE
normalized-t3002.11tsp11.1900571761.opb	646.311	UNSATISFIABLE
normalized-t3002.11tsp11.1900559676.opb	1380.47	UNSATISFIABLE
normalized-t3002.11tsp11.1900554373.opb	0.208604	SATISFIABLE
normalized-t3002.11tsp11.1900553647.opb	335.337	UNSATISFIABLE
normalized-t3002.11tsp11.1900583053.opb	784.045	UNSATISFIABLE
normalized-t3002.11tsp11.1900544484.opb	164.2	UNSATISFIABLE
normalized-t3002.11tsp11.1900554067.opb	0.915885	SATISFIABLE
normalized-t3002.11tsp11.1900568706.opb	251.201	UNSATISFIABLE
normalized-t3002.11tsp11.1900559641.opb	2.37837	SATISFIABLE
normalized-t3002.11tsp11.1900553644.opb	0.37619	SATISFIABLE
normalized-t3002.11tsp11.1900547461.opb	2.76607	SATISFIABLE
normalized-t3002.11tsp11.1900567135.opb	114.967	UNSATISFIABLE
normalized-t3002.11tsp11.1900565534.opb	446.244	UNSATISFIABLE
normalized-t3002.11tsp11.1900669309.opb	4.50378	SATISFIABLE
normalized-t3002.11tsp11.1900670234.opb	716.976	UNSATISFIABLE
normalized-t3002.11tsp11.1900554375.opb	0.333644	SATISFIABLE
normalized-t3002.11tsp11.1900546417.opb	432.821	UNSATISFIABLE
normalized-t3002.11tsp11.1900670675.opb	100.9	UNSATISFIABLE
normalized-t3002.11tsp11.1900576927.opb	349.57	UNSATISFIABLE
normalized-t3002.11tsp11.1900545610.opb	568.936	UNSATISFIABLE
normalized-t3002.11tsp11.1900557362.opb	232.113	UNSATISFIABLE
normalized-t3002.11tsp11.1900558739.opb	385.958	UNSATISFIABLE
normalized-t3002.11tsp11.1900573901.opb	423.319	UNSATISFIABLE
normalized-t3002.11tsp11.1900576151.opb	544.415	UNSATISFIABLE
normalized-t3002.11tsp11.1900554072.opb	234.411	UNSATISFIABLE
normalized-t3002.11tsp11.1900575442.opb	211.937	UNSATISFIABLE
normalized-t3002.11tsp11.1900667195.opb	738.705	UNSATISFIABLE
normalized-t3002.11tsp11.1900559365.opb	0.530223	SATISFIABLE
normalized-t3002.11tsp11.1900579996.opb	691.249	UNSATISFIABLE
normalized-t3002.11tsp11.1900581321.opb	0.169373	SATISFIABLE
normalized-t3002.11tsp11.1900561389.opb	2.46825	SATISFIABLE
normalized-t3002.11tsp11.1900561288.opb	1201.15	UNSATISFIABLE
normalized-t3002.11tsp11.1900566263.opb	0.471384	SATISFIABLE
normalized-t3002.11tsp11.1900669797.opb	390.183	UNSATISFIABLE
normalized-t3002.11tsp11.1900577000.opb	0.466824	SATISFIABLE
normalized-t3002.11tsp11.1900574948.opb	0.356963	SATISFIABLE
normalized-t3002.11tsp11.1900554389.opb	0.136366	SATISFIABLE
normalized-t3002.11tsp11.1900547427.opb	0.274692	SATISFIABLE
normalized-t3002.11tsp11.1900557957.opb	309.824	UNSATISFIABLE
normalized-t3002.11tsp11.1900564824.opb	4.44871	UNSATISFIABLE
normalized-t3002.11tsp11.1900563801.opb	56.4475	UNSATISFIABLE
normalized-t3002.11tsp11.1900571132.opb	250.458	UNSATISFIABLE
normalized-t3002.11tsp11.1900567024.opb	123.398	UNSATISFIABLE
normalized-t3002.11tsp11.1900547353.opb	1.81972	SATISFIABLE
normalized-t3002.11tsp11.1900544463.opb	2.10866	SATISFIABLE
normalized-t3002.11tsp11.1900571131.opb	0.264171	SATISFIABLE
normalized-t3002.11tsp11.1900551347.opb	247.003	UNSATISFIABLE
normalized-t3002.11tsp11.1900557568.opb	0.209764	SATISFIABLE
normalized-t3002.11tsp11.1900566270.opb	8.01791	SATISFIABLE
normalized-t3002.11tsp11.1900564281.opb	153.588	UNSATISFIABLE
normalized-t3002.11tsp11.1900558106.opb	16.5869	UNSATISFIABLE
normalized-t3002.11tsp11.1900550720.opb	682.434	UNSATISFIABLE
normalized-t3002.11tsp11.1900559416.opb	14.9843	SATISFIABLE
normalized-t3002.11tsp11.1900564822.opb	0.173566	SATISFIABLE
normalized-t3002.11tsp11.1900577940.opb	707.719	UNSATISFIABLE
normalized-t3002.11tsp11.1900567939.opb	4.61925	SATISFIABLE
normalized-t3002.11tsp11.1900553606.opb	4.81978	SATISFIABLE
normalized-t3002.11tsp11.1900557413.opb	0.458341	SATISFIABLE
normalized-t3002.11tsp11.1900554420.opb	182.394	UNSATISFIABLE
normalized-t3002.11tsp11.1900557574.opb	229.11	UNSATISFIABLE
normalized-t3002.11tsp11.1900551864.opb	181.285	UNSATISFIABLE
normalized-t3002.11tsp11.1900547389.opb	282.877	UNSATISFIABLE
normalized-t3002.11tsp11.1900573137.opb	581.534	UNSATISFIABLE
normalized-t3002.11tsp11.1900552423.opb	6.37264	UNSATISFIABLE
normalized-t3002.11tsp11.1900552311.opb	0.352704	SATISFIABLE
normalized-t3002.11tsp11.1900556231.opb	348.584	UNSATISFIABLE
normalized-t3002.11tsp11.1900584106.opb	153.239	UNSATISFIABLE
normalized-t3002.11tsp11.1900563250.opb	765.976	UNSATISFIABLE
normalized-t3002.11tsp11.1900582300.opb	658.375	UNSATISFIABLE
normalized-t3002.11tsp11.1900669299.opb	1.90232	SATISFIABLE
normalized-t3002.11tsp11.1900670756.opb	1.92557	SATISFIABLE
normalized-t3002.11tsp11.1900548667.opb	1203.51	UNSATISFIABLE
normalized-t3002.11tsp11.1900568186.opb	231.184	UNSATISFIABLE
normalized-t3002.11tsp11.1900566157.opb	115.044	UNSATISFIABLE
normalized-t2001.13queen13.1110974372.opb	27.1546	UNSATISFIABLE
normalized-t2001.13queen13.1110970277.opb	1.67809	SATISFIABLE
normalized-t2001.13queen13.1111224059.opb	15.452	UNSATISFIABLE
normalized-t2001.13queen13.1111227418.opb	10.5358	SATISFIABLE
normalized-t2001.13queen13.1110967327.opb	0.812305	SATISFIABLE
normalized-t2001.13queen13.1111227861.opb	38.9239	UNSATISFIABLE
normalized-t2001.13queen13.1111219348.opb	27.6688	UNSATISFIABLE
normalized-t2001.13queen13.1110975607.opb	19.2806	UNSATISFIABLE
normalized-t2001.13queen13.1111223220.opb	41.2449	UNSATISFIABLE
normalized-t2001.13queen13.1111212476.opb	60.9917	UNSATISFIABLE
normalized-t2001.13queen13.1111221203.opb	34.2932	UNSATISFIABLE
normalized-t2001.13queen13.1111223416.opb	3.24471	SATISFIABLE
normalized-t2001.13queen13.1111217392.opb	32.0668	UNSATISFIABLE
normalized-t2001.13queen13.1110967523.opb	42.5535	UNSATISFIABLE
normalized-t2001.13queen13.1110971363.opb	33.652	UNSATISFIABLE
normalized-t2001.13queen13.1110973863.opb	42.6347	SATISFIABLE
normalized-t2001.13queen13.1111226284.opb	21.3259	SATISFIABLE
normalized-t2001.13queen13.1111220546.opb	31.7943	UNSATISFIABLE
normalized-t2001.13queen13.1111226680.opb	29.6577	UNSATISFIABLE
normalized-t2001.13queen13.1110971097.opb	40.5196	SATISFIABLE
normalized-t2001.13queen13.1110971697.opb	34.5873	UNSATISFIABLE
normalized-t2001.13queen13.1110978334.opb	34.7844	UNSATISFIABLE
normalized-t2001.13queen13.1110976735.opb	7.30839	SATISFIABLE
normalized-t2001.13queen13.1110972958.opb	7.36516	SATISFIABLE
normalized-t2001.13queen13.1111221953.opb	20.3047	SATISFIABLE
normalized-t2001.13queen13.1110976730.opb	62.4383	UNSATISFIABLE
normalized-t2001.13queen13.1111213868.opb	29.926	UNSATISFIABLE
normalized-t2001.13queen13.1111223004.opb	37.8668	UNSATISFIABLE
normalized-t2001.13queen13.1111222080.opb	19.0476	SATISFIABLE
normalized-t2001.13queen13.1111224929.opb	22.7058	UNSATISFIABLE
normalized-t2001.13queen13.1111217380.opb	7.3407	SATISFIABLE
normalized-t2001.13queen13.1111225605.opb	27.974	UNSATISFIABLE
normalized-t2001.13queen13.1110970170.opb	25.1645	SATISFIABLE
normalized-t2001.13queen13.1111219399.opb	14.9418	SATISFIABLE
normalized-t2001.13queen13.1111226062.opb	22.315	UNSATISFIABLE
normalized-t2001.13queen13.1111222539.opb	42.7173	UNSATISFIABLE
normalized-t2001.13queen13.1110968094.opb	30.4861	UNSATISFIABLE
normalized-t2001.13queen13.1110967142.opb	64.6173	UNSATISFIABLE
normalized-t2001.13queen13.1111216188.opb	28.5675	SATISFIABLE
normalized-t2001.13queen13.1110969577.opb	24.5755	UNSATISFIABLE
normalized-t2001.13queen13.1111216864.opb	22.5013	SATISFIABLE
normalized-t2001.13queen13.1111212923.opb	28.6822	UNSATISFIABLE
normalized-t2001.13queen13.1110970631.opb	21.5922	UNSATISFIABLE
normalized-t2001.13queen13.1111224255.opb	37.2963	UNSATISFIABLE
normalized-t2001.13queen13.1111223689.opb	18.8007	SATISFIABLE
normalized-t2001.13queen13.1110969933.opb	6.84369	SATISFIABLE
normalized-t2001.13queen13.1111217555.opb	36.1917	UNSATISFIABLE
normalized-t2001.13queen13.1110969170.opb	32.9697	UNSATISFIABLE
normalized-t2001.13queen13.1110971766.opb	0.378499	SATISFIABLE
normalized-t2001.13queen13.1111212272.opb	37.4124	UNSATISFIABLE
normalized-t2001.13queen13.1110974180.opb	39.4026	UNSATISFIABLE
normalized-t2001.13queen13.1111218955.opb	23.3777	UNSATISFIABLE
normalized-t2001.13queen13.1110974553.opb	19.5362	SATISFIABLE
normalized-t2001.13queen13.1110977273.opb	38.8059	UNSATISFIABLE
normalized-t2001.13queen13.1111216823.opb	31.6987	UNSATISFIABLE
normalized-t2001.13queen13.1111213670.opb	33.6749	UNSATISFIABLE
normalized-t2001.13queen13.1111218024.opb	35.7803	UNSATISFIABLE
normalized-t2001.13queen13.1111221624.opb	43.7326	UNSATISFIABLE
normalized-t2001.13queen13.1111223596.opb	7.00024	SATISFIABLE
normalized-t2001.13queen13.1110975832.opb	6.27211	SATISFIABLE
normalized-t2001.13queen13.1110975965.opb	73.6393	UNSATISFIABLE
normalized-t2001.13queen13.1110976935.opb	23.5512	UNSATISFIABLE
normalized-t2001.13queen13.1110977266.opb	43.0372	SATISFIABLE
normalized-t2001.13queen13.1110977464.opb	15.863	SATISFIABLE
normalized-t2001.13queen13.1110973364.opb	19.8663	UNSATISFIABLE
normalized-t2001.13queen13.1111222257.opb	27.5156	UNSATISFIABLE
normalized-t2001.13queen13.1111219799.opb	29.7446	UNSATISFIABLE
normalized-t2001.13queen13.1110972154.opb	43.5342	UNSATISFIABLE
normalized-t2001.13queen13.1110968561.opb	45.4639	UNSATISFIABLE
normalized-t2001.13queen13.1111220767.opb	42.8629	UNSATISFIABLE
normalized-t2001.13queen13.1110978113.opb	70.4953	UNSATISFIABLE
normalized-t2001.13queen13.1110966688.opb	21.7491	UNSATISFIABLE
normalized-t2001.13queen13.1110972763.opb	33.1806	UNSATISFIABLE
normalized-t2001.13queen13.1111223696.opb	16.5098	SATISFIABLE
normalized-t2001.13queen13.1110973478.opb	37.5803	SATISFIABLE
normalized-t2001.13queen13.1110973670.opb	45.6893	UNSATISFIABLE
normalized-t2001.13queen13.1111224451.opb	25.2037	UNSATISFIABLE
normalized-t2001.13queen13.1111228076.opb	49.1185	UNSATISFIABLE
normalized-t2001.13queen13.1110973163.opb	71.2624	UNSATISFIABLE
normalized-t2001.13queen13.1110977780.opb	25.378	UNSATISFIABLE
normalized-t2001.13queen13.1111217374.opb	2.7824	SATISFIABLE
normalized-t2001.13queen13.1111220019.opb	32.8806	UNSATISFIABLE
normalized-t2001.13queen13.1111224522.opb	3.19316	SATISFIABLE
normalized-t2001.13queen13.1110975678.opb	19.1081	SATISFIABLE
normalized-t2001.13queen13.1110968898.opb	49.7276	UNSATISFIABLE
normalized-t2001.13queen13.1110970444.opb	18.7633	UNSATISFIABLE
normalized-t2001.13queen13.1111226368.opb	20.7134	UNSATISFIABLE
normalized-t2001.13queen13.1110969860.opb	59.2363	UNSATISFIABLE
normalized-t2001.13queen13.1111222248.opb	10.8691	SATISFIABLE
normalized-t2001.13queen13.1111227326.opb	15.6746	UNSATISFIABLE
normalized-t2001.13queen13.1111227012.opb	36.224	UNSATISFIABLE
normalized-t2001.13queen13.1110976157.opb	29.33	UNSATISFIABLE
normalized-t2001.13queen13.1111218757.opb	46.3894	UNSATISFIABLE
normalized-t2001.13queen13.1110967729.opb	13.8263	UNSATISFIABLE
normalized-t2001.13queen13.1111226241.opb	40.5232	SATISFIABLE
normalized-t2001.13queen13.1111225122.opb	17.3481	UNSATISFIABLE
normalized-t2001.13queen13.1110966483.opb	12.5836	UNSATISFIABLE
normalized-t2001.13queen13.1111216411.opb	38.6126	UNSATISFIABLE
normalized-t2001.13queen13.1110968431.opb	9.11099	SATISFIABLE
normalized-t2001.13queen13.1111218308.opb	95.606	UNSATISFIABLE