InstanceRuntimeResult
normalized-3col-left3reg-l070-r069-n1.opb16.372UNSATISFIABLE
normalized-3col-left3reg-l030-r029-n1.opb0.987331UNSATISFIABLE
normalized-3col-almost3reg-l080-r079-n1.opb1798.762UNKNOWN
normalized-3col-almost3reg-l030-r029-n1.opb7.60388UNSATISFIABLE
normalized-3col-left3reg-l040-r039-n1.opb1.37444UNSATISFIABLE
normalized-3col-almost3reg-l070-r069-n1.opb1798.736UNKNOWN
normalized-3col-left3reg-l100-r099-n1.opb23.2568UNSATISFIABLE
normalized-3col-almost3reg-l060-r059-n1.opb1773.91UNSATISFIABLE
normalized-3col-almost3reg-l010-r009-n1.opb0.105718UNSATISFIABLE
normalized-3col-almost3reg-l040-r039-n1.opb16.3732UNSATISFIABLE
normalized-3col-almost3reg-l090-r089-n1.opb1798.746UNKNOWN
normalized-3col-left3reg-l050-r049-n1.opb5.84067UNSATISFIABLE
normalized-3col-almost3reg-l015-r014-n1.opb0.267266UNSATISFIABLE
normalized-3col-almost3reg-l065-r064-n1.opb1800.467UNKNOWN
normalized-3col-left3reg-l080-r079-n1.opb34.3509UNSATISFIABLE
normalized-3col-almost3reg-l020-r019-n1.opb0.474734UNSATISFIABLE
normalized-3col-almost3reg-l055-r054-n1.opb1798.779UNKNOWN
normalized-3col-left3reg-l060-r059-n1.opb16.1272UNSATISFIABLE
normalized-3col-almost3reg-l050-r049-n1.opb496.231UNSATISFIABLE
normalized-3col-almost3reg-l100-r099-n1.opb1798.734UNKNOWN
normalized-3col-left3reg-l010-r010-n1.opb0.079835UNSATISFIABLE
normalized-3col-left3reg-l090-r089-n1.opb75.2701UNSATISFIABLE
normalized-3col-almost3reg-l045-r044-n1.opb32.9681UNSATISFIABLE
normalized-3col-almost3reg-l025-r024-n1.opb1.01882UNSATISFIABLE
normalized-3col-left3reg-l020-r019-n1.opb0.419419UNSATISFIABLE
normalized-3col-almost3reg-l035-r034-n1.opb6.20366UNSATISFIABLE
normalized-subsetcard-eq-fixedbandwidth-60.opb1798.695UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-25.opb1798.777UNKNOWN
normalized-subsetcard-geq-random4regular-75.opb1798.727UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-60.opb1798.753UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-65.opb1798.779UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-15.opb45.7602UNSATISFIABLE
normalized-subsetcard-eq-random4regular-35.opb1798.764UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-15.opb35.9063UNSATISFIABLE
normalized-subsetcard-eq-fixedbandwidth-35.opb1798.768UNKNOWN
normalized-subsetcard-eq-random4regular-55.opb1798.739UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-70.opb1800.463UNKNOWN
normalized-subsetcard-eq-random4regular-75.opb1798.788UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-30.opb1798.749UNKNOWN
normalized-subsetcard-eq-random4regular-50.opb1798.749UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-25.opb1798.744UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-45.opb1798.752UNKNOWN
normalized-subsetcard-geq-random4regular-35.opb1798.758UNKNOWN
normalized-subsetcard-eq-random4regular-20.opb53.6325UNSATISFIABLE
normalized-subsetcard-geq-random4regular-60.opb1798.747UNKNOWN
normalized-subsetcard-eq-random4regular-70.opb1798.740UNKNOWN
normalized-subsetcard-geq-random4regular-65.opb1798.755UNKNOWN
normalized-subsetcard-geq-random4regular-15.opb3.97545UNSATISFIABLE
normalized-subsetcard-eq-fixedbandwidth-80.opb1798.756UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-70.opb1798.744UNKNOWN
normalized-subsetcard-eq-random4regular-30.opb1798.749UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-80.opb1798.789UNKNOWN
normalized-subsetcard-eq-random4regular-25.opb988.079UNSATISFIABLE
normalized-subsetcard-geq-random4regular-80.opb1800.466UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-40.opb1798.769UNKNOWN
normalized-subsetcard-geq-random4regular-70.opb1798.759UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-35.opb1798.766UNKNOWN
normalized-subsetcard-eq-random4regular-40.opb1798.760UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-65.opb1798.756UNKNOWN
normalized-subsetcard-eq-random4regular-45.opb1798.753UNKNOWN
normalized-subsetcard-eq-random4regular-80.opb1800.470UNKNOWN
normalized-subsetcard-geq-random4regular-20.opb59.7983UNSATISFIABLE
normalized-subsetcard-eq-random4regular-65.opb1798.740UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-30.opb1798.757UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-50.opb1798.752UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-50.opb1798.744UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-45.opb1798.725UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-75.opb1798.645UNKNOWN
normalized-subsetcard-geq-random4regular-40.opb1798.768UNKNOWN
normalized-subsetcard-eq-random4regular-15.opb5.16005UNSATISFIABLE
normalized-subsetcard-eq-fixedbandwidth-55.opb1798.729UNKNOWN
normalized-subsetcard-geq-random4regular-55.opb1798.750UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-75.opb1798.746UNKNOWN
normalized-subsetcard-geq-random4regular-50.opb1798.723UNKNOWN
normalized-subsetcard-geq-random4regular-25.opb1582.02UNSATISFIABLE
normalized-subsetcard-geq-fixedbandwidth-20.opb1084.92UNSATISFIABLE
normalized-subsetcard-eq-random4regular-60.opb1798.758UNKNOWN
normalized-subsetcard-geq-fixedbandwidth-55.opb1798.757UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-20.opb1798.765UNKNOWN
normalized-subsetcard-geq-random4regular-30.opb1798.776UNKNOWN
normalized-subsetcard-eq-fixedbandwidth-40.opb1798.731UNKNOWN
normalized-subsetcard-geq-random4regular-45.opb1798.765UNKNOWN
normalized-ECrand6reg-v111-n1.opb1798.728UNKNOWN
normalized-ECrand6reg-v101-n1.opb1798.730UNKNOWN
normalized-ECrand4regsplit-v110-n1.opb1800.472UNKNOWN
normalized-ECrand6reg-v081-n1.opb1798.758UNKNOWN
normalized-ECrand6reg-v041-n1.opb1798.742UNKNOWN
normalized-ECrand4regsplit-v100-n1.opb1798.794UNKNOWN
normalized-ECrand4regsplit-v020-n1.opb0.168779UNSATISFIABLE
normalized-ECrand4regsplit-v060-n1.opb1798.769UNKNOWN
normalized-ECrand4regsplit-v080-n1.opb1798.792UNKNOWN
normalized-ECrand6reg-v051-n1.opb1798.747UNKNOWN
normalized-ECrand6reg-v031-n1.opb1798.759UNKNOWN
normalized-ECrand4regsplit-v070-n1.opb1798.764UNKNOWN
normalized-ECrand4regsplit-v010-n1.opb0.006655UNSATISFIABLE
normalized-ECrand4regsplit-v030-n1.opb1.46482UNSATISFIABLE
normalized-ECrand6reg-v021-n1.opb1798.763UNKNOWN
normalized-ECrand4regsplit-v040-n1.opb959.895UNSATISFIABLE
normalized-ECrand6reg-v011-n1.opb5.94158UNSATISFIABLE
normalized-ECrand6reg-v061-n1.opb1798.757UNKNOWN
normalized-ECrand4regsplit-v050-n1.opb1798.757UNKNOWN
normalized-ECrand6reg-v071-n1.opb1798.708UNKNOWN
normalized-ECrand6reg-v091-n1.opb1798.730UNKNOWN
normalized-ECrand4regsplit-v090-n1.opb1798.697UNKNOWN
normalized-ECgrid5x130split.opb1800.457UNKNOWN
normalized-ECgrid3x70split.opb42.6665UNSATISFIABLE
normalized-ECgrid5x150split.opb1798.722UNKNOWN
normalized-ECgrid3x20split.opb2.56118UNSATISFIABLE
normalized-ECgrid5x30split.opb1798.760UNKNOWN
normalized-ECgrid5x120split.opb1798.594UNKNOWN
normalized-ECgrid5x50split.opb1798.603UNKNOWN
normalized-ECgrid5x10split.opb222.959UNSATISFIABLE
normalized-ECgrid3x40split.opb14.5719UNSATISFIABLE
normalized-ECgrid5x140split.opb1798.748UNKNOWN
normalized-ECgrid5x70split.opb1798.738UNKNOWN
normalized-ECgrid3x80split.opb51.0999UNSATISFIABLE
normalized-ECgrid5x90split.opb1798.751UNKNOWN
normalized-ECgrid3x100split.opb54.6508UNSATISFIABLE
normalized-ECgrid5x100split.opb1798.774UNKNOWN
normalized-ECgrid5x80split.opb1798.728UNKNOWN
normalized-ECgrid3x10split.opb0.3847UNSATISFIABLE
normalized-ECgrid5x40split.opb1798.749UNKNOWN
normalized-ECgrid3x60split.opb28.5053UNSATISFIABLE
normalized-ECgrid3x30split.opb9.22318UNSATISFIABLE
normalized-ECgrid5x20split.opb1798.739UNKNOWN
normalized-ECgrid5x60split.opb1798.767UNKNOWN
normalized-ECgrid3x90split.opb85.3207UNSATISFIABLE
normalized-ECgrid5x110split.opb1798.725UNKNOWN
normalized-ECgrid3x50split.opb31.561UNSATISFIABLE
normalized-sumineqArity3pyramidP0064.opb7.65014UNSATISFIABLE
normalized-sumineqArity4pyramidP0016.opb0.219746UNSATISFIABLE
normalized-sumineqArity3pyramidP0016.opb0.13787UNSATISFIABLE
normalized-sumineqArity5houseP128.opb471.938UNSATISFIABLE
normalized-sumineqArity4pyramidP0064.opb26.9935UNSATISFIABLE
normalized-sumineqArity5pyramidP0032.opb5.50306UNSATISFIABLE
normalized-sumineqArity4pyramidP0032.opb2.60245UNSATISFIABLE
normalized-sumineqArity5pyramidP0064.opb33.7996UNSATISFIABLE
normalized-sumineqArity3houseP016.opb0.274902UNSATISFIABLE
normalized-sumineqArity3houseP032.opb2.29458UNSATISFIABLE
normalized-sumineqArity4pyramidP0125.opb191.353UNSATISFIABLE
normalized-sumineqArity5houseP032.opb16.6178UNSATISFIABLE
normalized-sumineqArity3pyramidP0032.opb0.766999UNSATISFIABLE
normalized-sumineqArity3houseP128.opb200.371UNSATISFIABLE
normalized-sumineqArity4houseP064.opb63.4252UNSATISFIABLE
normalized-sumineqArity4houseP128.opb412.901UNSATISFIABLE
normalized-sumineqArity3pyramidP0125.opb54.5289UNSATISFIABLE
normalized-sumineqArity3houseP064.opb23.9756UNSATISFIABLE
normalized-sumineqArity5pyramidP0016.opb0.642414UNSATISFIABLE
normalized-sumineqArity5houseP016.opb1.71084UNSATISFIABLE
normalized-sumineqArity5houseP064.opb73.1799UNSATISFIABLE
normalized-sumineqArity4houseP032.opb7.08728UNSATISFIABLE
normalized-sumineqArity5pyramidP0125.opb173.858UNSATISFIABLE
normalized-sumineqArity4houseP016.opb0.652659UNSATISFIABLE
normalized-vertexcover-grid8x11-hard.opb0.615114UNSATISFIABLE
normalized-vertexcover-grid10x29.opb0.962597UNSATISFIABLE
normalized-vertexcover-grid8x23-hard.opb1.77391UNSATISFIABLE
normalized-vertexcover-grid4x15-hard.opb0.123269UNSATISFIABLE
normalized-vertexcover-grid6x11.opb0.142668UNSATISFIABLE
normalized-vertexcover-grid8x21-hard.opb1.60023UNSATISFIABLE
normalized-vertexcover-grid8x9.opb0.179444UNSATISFIABLE
normalized-vertexcover-grid6x19.opb0.163572UNSATISFIABLE
normalized-vertexcover-grid6x13-hard.opb0.322056UNSATISFIABLE
normalized-vertexcover-completegraph-5.opb0.000618UNSATISFIABLE
normalized-vertexcover-grid4x27-hard.opb0.143546UNSATISFIABLE
normalized-vertexcover-grid10x15-hard.opb1.71672UNSATISFIABLE
normalized-vertexcover-grid6x9.opb0.078422UNSATISFIABLE
normalized-vertexcover-grid6x7-hard.opb0.055883UNSATISFIABLE
normalized-vertexcover-grid6x25.opb0.301575UNSATISFIABLE
normalized-vertexcover-grid4x9-hard.opb0.029025UNSATISFIABLE
normalized-vertexcover-grid4x21.opb0.288045UNSATISFIABLE
normalized-vertexcover-grid10x23.opb0.413196UNSATISFIABLE
normalized-vertexcover-completegraph-17.opb0.002316UNSATISFIABLE
normalized-vertexcover-grid4x11.opb0.04693UNSATISFIABLE
normalized-vertexcover-completegraph-29.opb0.007119UNSATISFIABLE
normalized-vertexcover-grid6x17.opb0.125851UNSATISFIABLE
normalized-vertexcover-grid6x7.opb0.042332UNSATISFIABLE
normalized-vertexcover-grid4x9.opb0.027699UNSATISFIABLE
normalized-vertexcover-grid6x23-hard.opb0.42545UNSATISFIABLE
normalized-vertexcover-grid4x23-hard.opb0.46664UNSATISFIABLE
normalized-vertexcover-grid10x17-hard.opb1.89461UNSATISFIABLE
normalized-vertexcover-grid10x13-hard.opb1.1453UNSATISFIABLE
normalized-vertexcover-completegraph-25.opb0.005151UNSATISFIABLE
normalized-vertexcover-grid4x23.opb0.385616UNSATISFIABLE
normalized-vertexcover-grid6x25-hard.opb0.563521UNSATISFIABLE
normalized-vertexcover-completegraph-43.opb0.014651UNSATISFIABLE
normalized-vertexcover-grid4x19.opb0.223763UNSATISFIABLE
normalized-vertexcover-grid8x17-hard.opb0.68049UNSATISFIABLE
normalized-vertexcover-grid10x13.opb0.198932UNSATISFIABLE
normalized-vertexcover-grid8x19-hard.opb1.19576UNSATISFIABLE
normalized-vertexcover-completegraph-3.opb0.000492UNSATISFIABLE
normalized-vertexcover-completegraph-39.opb0.01152UNSATISFIABLE
normalized-vertexcover-grid4x11-hard.opb0.052775UNSATISFIABLE
normalized-vertexcover-grid10x21-hard.opb2.84291UNSATISFIABLE
normalized-vertexcover-grid6x15-hard.opb0.492251UNSATISFIABLE
normalized-vertexcover-grid10x27.opb0.66953UNSATISFIABLE
normalized-vertexcover-completegraph-9.opb0.000744UNSATISFIABLE
normalized-vertexcover-grid6x15.opb0.362875UNSATISFIABLE
normalized-vertexcover-grid10x11-hard.opb0.767414UNSATISFIABLE
normalized-vertexcover-completegraph-7.opb0.000515UNSATISFIABLE
normalized-vertexcover-grid8x9-hard.opb0.326859UNSATISFIABLE
normalized-vertexcover-completegraph-47.opb0.012087UNSATISFIABLE
normalized-vertexcover-grid6x17-hard.opb0.229293UNSATISFIABLE
normalized-vertexcover-grid4x27.opb0.121643UNSATISFIABLE
normalized-vertexcover-grid10x17.opb0.425414UNSATISFIABLE
normalized-vertexcover-completegraph-41.opb0.013833UNSATISFIABLE
normalized-vertexcover-grid4x7-hard.opb0.018474UNSATISFIABLE
normalized-vertexcover-grid4x5-hard.opb0.008937UNSATISFIABLE
normalized-vertexcover-grid10x11.opb0.149779UNSATISFIABLE
normalized-vertexcover-completegraph-19.opb0.002942UNSATISFIABLE
normalized-vertexcover-grid4x7.opb0.014981UNSATISFIABLE
normalized-vertexcover-grid4x13.opb0.071803UNSATISFIABLE
normalized-vertexcover-grid10x19-hard.opb3.26126UNSATISFIABLE
normalized-vertexcover-grid10x21.opb0.331758UNSATISFIABLE
normalized-vertexcover-grid8x25-hard.opb2.14135UNSATISFIABLE
normalized-vertexcover-grid6x23.opb0.248796UNSATISFIABLE
normalized-vertexcover-grid4x13-hard.opb0.079529UNSATISFIABLE
normalized-vertexcover-grid6x9-hard.opb0.111651UNSATISFIABLE
normalized-vertexcover-grid10x25.opb0.495383UNSATISFIABLE
normalized-vertexcover-grid8x29-hard.opb1.37524UNSATISFIABLE
normalized-vertexcover-grid10x29-hard.opb6.40385UNSATISFIABLE
normalized-vertexcover-grid10x25-hard.opb3.99035UNSATISFIABLE
normalized-vertexcover-grid4x29-hard.opb0.180957UNSATISFIABLE
normalized-vertexcover-grid8x27-hard.opb1.28901UNSATISFIABLE
normalized-vertexcover-grid4x25.opb0.495568UNSATISFIABLE
normalized-vertexcover-completegraph-51.opb0.019191UNSATISFIABLE
normalized-vertexcover-grid6x27.opb0.378338UNSATISFIABLE
normalized-vertexcover-completegraph-15.opb0.001489UNSATISFIABLE
normalized-vertexcover-grid6x27-hard.opb0.707038UNSATISFIABLE
normalized-vertexcover-grid8x15-hard.opb0.507278UNSATISFIABLE
normalized-vertexcover-grid4x21-hard.opb0.350509UNSATISFIABLE
normalized-vertexcover-grid4x25-hard.opb0.60053UNSATISFIABLE
normalized-vertexcover-grid4x17.opb0.1539UNSATISFIABLE
normalized-vertexcover-grid8x13-hard.opb0.354875UNSATISFIABLE
normalized-vertexcover-grid4x19-hard.opb0.264208UNSATISFIABLE
normalized-vertexcover-grid6x21.opb0.199248UNSATISFIABLE
normalized-vertexcover-completegraph-35.opb0.007664UNSATISFIABLE
normalized-vertexcover-grid4x29.opb0.1413UNSATISFIABLE
normalized-vertexcover-grid10x23-hard.opb2.67734UNSATISFIABLE
normalized-vertexcover-grid6x19-hard.opb0.270534UNSATISFIABLE
normalized-vertexcover-completegraph-27.opb0.005492UNSATISFIABLE
normalized-vertexcover-completegraph-45.opb0.016388UNSATISFIABLE
normalized-vertexcover-completegraph-49.opb0.013233UNSATISFIABLE
normalized-vertexcover-grid6x11-hard.opb0.190857UNSATISFIABLE
normalized-vertexcover-grid6x29.opb0.527779UNSATISFIABLE
normalized-vertexcover-grid4x5.opb0.006366UNSATISFIABLE
normalized-vertexcover-grid6x29-hard.opb0.966777UNSATISFIABLE
normalized-vertexcover-grid10x15.opb0.322485UNSATISFIABLE
normalized-vertexcover-grid10x27-hard.opb5.15154UNSATISFIABLE
normalized-vertexcover-completegraph-11.opb0.001515UNSATISFIABLE
normalized-vertexcover-completegraph-33.opb0.006648UNSATISFIABLE
normalized-vertexcover-grid6x21-hard.opb0.334758UNSATISFIABLE
normalized-vertexcover-completegraph-31.opb0.006824UNSATISFIABLE
normalized-vertexcover-grid4x17-hard.opb0.182566UNSATISFIABLE
normalized-vertexcover-completegraph-21.opb0.003468UNSATISFIABLE
normalized-vertexcover-completegraph-13.opb0.001773UNSATISFIABLE
normalized-vertexcover-grid4x15.opb0.110451UNSATISFIABLE
normalized-vertexcover-completegraph-23.opb0.004138UNSATISFIABLE
normalized-vertexcover-grid10x19.opb0.658872UNSATISFIABLE
normalized-vertexcover-completegraph-37.opb0.007098UNSATISFIABLE
normalized-vertexcover-grid6x13.opb0.228144UNSATISFIABLE
normalized-rand6reg-v071-n2.opb1798.770UNKNOWN
normalized-rand6reg-v071-n3.opb1798.760UNKNOWN
normalized-rand6reg-v051-n3.opb1798.745UNKNOWN
normalized-rand6reg-v061-n3.opb1800.471UNKNOWN
normalized-rand6reg-v091-n1.opb1798.715UNKNOWN
normalized-rand6reg-v081-n1.opb1798.742UNKNOWN
normalized-rand6reg-v041-n2.opb1798.778UNKNOWN
normalized-rand6reg-v111-n2.opb1798.766UNKNOWN
normalized-rand6reg-v101-n2.opb1798.747UNKNOWN
normalized-rand6reg-v081-n2.opb1798.764UNKNOWN
normalized-rand6reg-v021-n2.opb1.36048UNSATISFIABLE
normalized-rand6reg-v021-n1.opb1.0741UNSATISFIABLE
normalized-rand6reg-v011-n2.opb0.011392UNSATISFIABLE
normalized-rand6reg-v101-n3.opb1798.796UNKNOWN
normalized-rand6reg-v051-n2.opb1798.762UNKNOWN
normalized-rand6reg-v111-n3.opb1798.767UNKNOWN
normalized-rand6reg-v031-n3.opb90.0883UNSATISFIABLE
normalized-rand6reg-v061-n2.opb1798.791UNKNOWN
normalized-rand6reg-v031-n1.opb372.468UNSATISFIABLE
normalized-rand6reg-v041-n1.opb1798.767UNKNOWN
normalized-rand6reg-v111-n1.opb1800.474UNKNOWN
normalized-rand6reg-v011-n1.opb0.01798UNSATISFIABLE
normalized-rand6reg-v091-n2.opb1798.744UNKNOWN
normalized-rand6reg-v041-n3.opb1798.729UNKNOWN
normalized-rand6reg-v071-n1.opb1798.750UNKNOWN
normalized-rand6reg-v061-n1.opb1798.775UNKNOWN
normalized-rand6reg-v031-n2.opb198.8UNSATISFIABLE
normalized-rand6reg-v021-n3.opb0.676385UNSATISFIABLE
normalized-rand6reg-v081-n3.opb1798.774UNKNOWN
normalized-rand6reg-v011-n3.opb0.012799UNSATISFIABLE
normalized-rand6reg-v101-n1.opb1798.743UNKNOWN
normalized-rand6reg-v051-n1.opb1798.756UNKNOWN
normalized-rand6reg-v091-n3.opb1798.741UNKNOWN
normalized-5_6_8.opb0.024418UNSATISFIABLE
normalized-4_7_0.opb0.000992UNSATISFIABLE
normalized-4_5_1.opb0.000745UNSATISFIABLE
normalized-5_6_23.opb309.869UNSATISFIABLE
normalized-5_6_15.opb1.18316UNSATISFIABLE
normalized-3_6_0.opb0.000892UNSATISFIABLE
normalized-3_5_6.opb0.007546UNSATISFIABLE
normalized-5_7_4.opb0.0058UNSATISFIABLE
normalized-4_5_8.opb0.019484UNSATISFIABLE
normalized-6_6_18.opb17.4364UNSATISFIABLE
normalized-2_7_2.opb0.001188UNSATISFIABLE
normalized-4_7_4.opb0.004644UNSATISFIABLE
normalized-4_5_13.opb0.079232UNSATISFIABLE
normalized-5_7_9.opb0.008079SATISFIABLE
normalized-6_6_13.opb0.26224UNSATISFIABLE
normalized-7_7_3.opb0.004162UNSATISFIABLE
normalized-3_4_7.opb0.005961UNSATISFIABLE
normalized-7_7_9.opb0.065059UNSATISFIABLE
normalized-7_7_11.opb0.218042UNSATISFIABLE
normalized-5_6_14.opb1.0207UNSATISFIABLE
normalized-7_7_10.opb0.226798UNSATISFIABLE
normalized-3_5_5.opb0.003478UNSATISFIABLE
normalized-4_6_6.opb0.013943UNSATISFIABLE
normalized-7_6_25.opb601.329UNSATISFIABLE
normalized-3_7_2.opb0.001739UNSATISFIABLE
normalized-2_6_3.opb0.002012SATISFIABLE
normalized-6_6_11.opb0.072545UNSATISFIABLE
normalized-8_6_29.opb1798.754UNKNOWN
normalized-6_6_12.opb0.266367UNSATISFIABLE
normalized-2_4_2.opb0.001089UNSATISFIABLE
normalized-3_7_0.opb0.000696UNSATISFIABLE
normalized-5_6_0.opb0.00142UNSATISFIABLE
normalized-5_6_3.opb0.003021UNSATISFIABLE
normalized-2_5_3.opb0.001438SATISFIABLE
normalized-2_7_0.opb0.000492UNSATISFIABLE
normalized-7_7_18.opb2.38097SATISFIABLE
normalized-6_6_5.opb0.004054UNSATISFIABLE
normalized-4_7_6.opb0.013576UNSATISFIABLE
normalized-8_6_20.opb22.2011UNSATISFIABLE
normalized-4_6_1.opb0.001508UNSATISFIABLE
normalized-4_5_16.opb0.510435UNSATISFIABLE
normalized-8_6_28.opb702.284UNSATISFIABLE
normalized-3_6_6.opb0.004064SATISFIABLE
normalized-6_6_9.opb0.023506UNSATISFIABLE
normalized-2_6_1.opb0.000725UNSATISFIABLE
normalized-2_7_1.opb0.000775UNSATISFIABLE
normalized-5_6_32.opb1798.747UNKNOWN
normalized-6_6_34.opb1798.756UNKNOWN
normalized-2_4_0.opb0.00051UNSATISFIABLE
normalized-4_5_20.opb2.25524UNSATISFIABLE
normalized-4_5_3.opb0.00211UNSATISFIABLE
normalized-5_6_13.opb0.308415UNSATISFIABLE
normalized-7_6_23.opb285.149UNSATISFIABLE
normalized-6_6_32.opb1798.750UNKNOWN
normalized-5_6_35.opb1798.740UNKNOWN
normalized-7_7_1.opb0.002346UNSATISFIABLE
normalized-3_5_9.opb0.017751UNSATISFIABLE
normalized-8_6_23.opb115.522UNSATISFIABLE
normalized-4_5_0.opb0.001018UNSATISFIABLE
normalized-5_6_28.opb1798.765UNKNOWN
normalized-5_6_36.opb1798.746UNKNOWN
normalized-2_3_2.opb0.001158UNSATISFIABLE
normalized-5_6_34.opb1798.747UNKNOWN
normalized-4_6_5.opb0.006031UNSATISFIABLE
normalized-4_5_28.opb21.6662UNSATISFIABLE
normalized-7_6_28.opb1800.469UNKNOWN
normalized-7_6_27.opb1685.36UNSATISFIABLE
normalized-3_4_13.opb0.020546UNSATISFIABLE
normalized-4_5_21.opb1.99344UNSATISFIABLE
normalized-5_6_19.opb17.7368UNSATISFIABLE
normalized-3_6_2.opb0.00171UNSATISFIABLE
normalized-3_4_9.opb0.008583UNSATISFIABLE
normalized-5_6_2.opb0.002368UNSATISFIABLE
normalized-8_7_19.opb270.764UNSATISFIABLE
normalized-5_7_1.opb0.002226UNSATISFIABLE
normalized-6_6_16.opb4.76568UNSATISFIABLE
normalized-3_4_11.opb0.014079UNSATISFIABLE
normalized-3_5_3.opb0.001709UNSATISFIABLE
normalized-6_6_14.opb1.06153UNSATISFIABLE
normalized-4_5_2.opb0.001698UNSATISFIABLE
normalized-2_6_0.opb0.000471UNSATISFIABLE
normalized-3_4_6.opb0.005577UNSATISFIABLE
normalized-2_3_5.opb0.002643UNSATISFIABLE
normalized-4_7_7.opb0.01167SATISFIABLE
normalized-7_7_6.opb0.019183UNSATISFIABLE
normalized-5_6_17.opb4.35009UNSATISFIABLE
normalized-6_6_31.opb1798.761UNKNOWN
normalized-7_6_26.opb572.086UNSATISFIABLE
normalized-2_3_1.opb0.000635UNSATISFIABLE
normalized-3_5_11.opb0.029338UNSATISFIABLE
normalized-5_6_6.opb0.015717UNSATISFIABLE
normalized-2_4_4.opb0.002205UNSATISFIABLE
normalized-7_7_12.opb1.05504UNSATISFIABLE
normalized-4_6_3.opb0.002177UNSATISFIABLE
normalized-4_7_1.opb0.001518UNSATISFIABLE
normalized-5_6_29.opb1798.777UNKNOWN
normalized-7_6_21.opb37.7154UNSATISFIABLE
normalized-7_6_19.opb11.8092UNSATISFIABLE
normalized-3_7_4.opb0.002884SATISFIABLE
normalized-4_5_24.opb8.18658UNSATISFIABLE
normalized-5_6_18.opb22.0341UNSATISFIABLE
normalized-4_5_22.opb4.22068UNSATISFIABLE
normalized-5_6_27.opb1798.729UNKNOWN
normalized-2_3_4.opb0.002063UNSATISFIABLE
normalized-8_6_25.opb351.353UNSATISFIABLE
normalized-6_6_6.opb0.006909UNSATISFIABLE
normalized-2_4_6.opb0.003673SATISFIABLE
normalized-3_7_3.opb0.002938UNSATISFIABLE
normalized-8_6_18.opb11.2001UNSATISFIABLE
normalized-4_5_5.opb0.004957UNSATISFIABLE
normalized-6_6_4.opb0.002998UNSATISFIABLE
normalized-7_7_14.opb8.2975UNSATISFIABLE
normalized-6_6_2.opb0.002727UNSATISFIABLE
normalized-3_5_1.opb0.00104UNSATISFIABLE
normalized-3_5_4.opb0.002597UNSATISFIABLE
normalized-2_7_3.opb0.002074SATISFIABLE
normalized-3_4_5.opb0.003802UNSATISFIABLE
normalized-8_6_19.opb5.73974UNSATISFIABLE
normalized-7_7_7.opb0.02272UNSATISFIABLE
normalized-8_6_22.opb131.203UNSATISFIABLE
normalized-4_5_9.opb0.016946UNSATISFIABLE
normalized-5_6_10.opb0.08462UNSATISFIABLE
normalized-5_6_20.opb104.622UNSATISFIABLE
normalized-5_6_26.opb1800.470UNKNOWN
normalized-7_6_18.opb16.0578UNSATISFIABLE
normalized-4_5_7.opb0.012197UNSATISFIABLE
normalized-7_6_22.opb137.86UNSATISFIABLE
normalized-5_6_33.opb1798.723UNKNOWN
normalized-4_5_27.opb13.1359UNSATISFIABLE
normalized-5_6_37.opb1798.755UNKNOWN
normalized-6_6_21.opb65.4124UNSATISFIABLE
normalized-5_7_0.opb0.001727UNSATISFIABLE
normalized-6_6_33.opb1798.775UNKNOWN
normalized-5_6_24.opb1537.07UNSATISFIABLE
normalized-8_7_18.opb77.6661UNSATISFIABLE
normalized-6_6_23.opb213.114UNSATISFIABLE
normalized-6_6_30.opb1798.764UNKNOWN
normalized-8_7_20.opb0.658896SATISFIABLE
normalized-6_6_8.opb0.024136UNSATISFIABLE
normalized-3_4_3.opb0.00171UNSATISFIABLE
normalized-4_7_5.opb0.006482UNSATISFIABLE
normalized-4_5_23.opb3.48961UNSATISFIABLE
normalized-2_3_6.opb0.003751UNSATISFIABLE
normalized-6_6_22.opb223.824UNSATISFIABLE
normalized-3_5_2.opb0.001297UNSATISFIABLE
normalized-7_7_13.opb1.10681UNSATISFIABLE
normalized-7_7_5.opb0.007176UNSATISFIABLE
normalized-2_3_3.opb0.001012UNSATISFIABLE
normalized-4_5_17.opb0.398315UNSATISFIABLE
normalized-3_6_3.opb0.002198UNSATISFIABLE
normalized-4_5_11.opb0.033186UNSATISFIABLE
normalized-6_6_10.opb0.059175UNSATISFIABLE
normalized-7_7_4.opb0.008398UNSATISFIABLE
normalized-4_5_4.opb0.004099UNSATISFIABLE
normalized-7_6_20.opb53.8578UNSATISFIABLE
normalized-4_5_10.opb0.032708UNSATISFIABLE
normalized-4_5_12.opb0.078431UNSATISFIABLE
normalized-5_6_22.opb524.905UNSATISFIABLE
normalized-4_6_4.opb0.004564UNSATISFIABLE
normalized-7_6_30.opb1798.709UNKNOWN
normalized-4_5_6.opb0.009122UNSATISFIABLE
normalized-5_6_5.opb0.00685UNSATISFIABLE
normalized-3_4_4.opb0.00311UNSATISFIABLE
normalized-4_5_26.opb17.1456UNSATISFIABLE
normalized-6_6_7.opb0.009152UNSATISFIABLE
normalized-7_7_0.opb0.001807UNSATISFIABLE
normalized-5_7_5.opb0.007278UNSATISFIABLE
normalized-7_7_8.opb0.046885UNSATISFIABLE
normalized-2_4_1.opb0.000758UNSATISFIABLE
normalized-5_7_7.opb0.016849UNSATISFIABLE
normalized-5_6_31.opb1798.788UNKNOWN
normalized-3_6_1.opb0.001076UNSATISFIABLE
normalized-8_6_30.opb1639.19UNSATISFIABLE
normalized-2_6_2.opb0.00124UNSATISFIABLE
normalized-7_6_29.opb1680.32UNSATISFIABLE
normalized-2_3_0.opb0.000695UNSATISFIABLE
normalized-4_6_2.opb0.001676UNSATISFIABLE
normalized-5_6_25.opb1426.59UNSATISFIABLE
normalized-2_5_0.opb0.00048UNSATISFIABLE
normalized-3_5_8.opb0.015776UNSATISFIABLE
normalized-4_5_19.opb0.947308UNSATISFIABLE
normalized-7_7_15.opb6.12509UNSATISFIABLE
normalized-3_4_12.opb0.021164UNSATISFIABLE
normalized-5_6_9.opb0.029008UNSATISFIABLE
normalized-3_6_4.opb0.003611UNSATISFIABLE
normalized-4_5_18.opb0.991742UNSATISFIABLE
normalized-3_5_7.opb0.007487UNSATISFIABLE
normalized-6_6_3.opb0.001806UNSATISFIABLE
normalized-2_5_1.opb0.000752UNSATISFIABLE
normalized-5_6_21.opb107.772UNSATISFIABLE
normalized-8_6_21.opb25.5481UNSATISFIABLE
normalized-6_6_17.opb3.21687UNSATISFIABLE
normalized-7_7_16.opb37.6564UNSATISFIABLE
normalized-5_6_7.opb0.013867UNSATISFIABLE
normalized-4_6_0.opb0.001006UNSATISFIABLE
normalized-5_6_16.opb4.39713UNSATISFIABLE
normalized-4_6_8.opb0.009371SATISFIABLE
normalized-4_5_14.opb0.182198UNSATISFIABLE
normalized-3_4_8.opb0.011243UNSATISFIABLE
normalized-6_6_19.opb15.7774UNSATISFIABLE
normalized-3_5_12.opb0.006382SATISFIABLE
normalized-3_5_10.opb0.030334UNSATISFIABLE
normalized-3_7_1.opb0.001307UNSATISFIABLE
normalized-4_7_3.opb0.002521UNSATISFIABLE
normalized-2_5_2.opb0.001203UNSATISFIABLE
normalized-2_4_3.opb0.001301UNSATISFIABLE
normalized-6_6_15.opb0.986621UNSATISFIABLE
normalized-5_6_11.opb0.080297UNSATISFIABLE
normalized-5_7_2.opb0.002166UNSATISFIABLE
normalized-4_7_2.opb0.00241UNSATISFIABLE
normalized-5_7_3.opb0.001756UNSATISFIABLE
normalized-5_6_38.opb1798.739UNKNOWN
normalized-5_6_4.opb0.004903UNSATISFIABLE
normalized-4_5_25.opb6.28591UNSATISFIABLE
normalized-5_6_1.opb0.001482UNSATISFIABLE
normalized-3_5_0.opb0.000738UNSATISFIABLE
normalized-4_5_15.opb0.196235UNSATISFIABLE
normalized-5_7_6.opb0.01171UNSATISFIABLE
normalized-3_4_10.opb0.015003UNSATISFIABLE
normalized-3_6_5.opb0.004874UNSATISFIABLE
normalized-2_4_5.opb0.001799UNSATISFIABLE
normalized-4_6_7.opb0.014181UNSATISFIABLE
normalized-5_7_8.opb0.055606UNSATISFIABLE
normalized-8_6_26.opb817.8UNSATISFIABLE
normalized-3_4_0.opb0.00072UNSATISFIABLE
normalized-6_6_20.opb102.987UNSATISFIABLE
normalized-7_6_24.opb300.015UNSATISFIABLE
normalized-3_4_1.opb0.000668UNSATISFIABLE
normalized-5_6_30.opb1798.754UNKNOWN
normalized-7_7_2.opb0.003335UNSATISFIABLE
normalized-8_6_24.opb203.8UNSATISFIABLE
normalized-8_6_27.opb1587.97UNSATISFIABLE
normalized-3_4_2.opb0.001472UNSATISFIABLE
normalized-5_6_12.opb0.255553UNSATISFIABLE
normalized-compression16_3.opb0.0166UNSATISFIABLE
normalized-compression8_15.opb0.074342SATISFIABLE
normalized-compression32_7.opb3.79913UNSATISFIABLE
normalized-compression8_19.opb0.606502SATISFIABLE
normalized-compression64_26.opb3.1845SATISFIABLE
normalized-compression64_10.opb1800.460UNKNOWN
normalized-compression64_24.opb345.627SATISFIABLE
normalized-compression32_14.opb1798.712UNKNOWN
normalized-compression16_5.opb0.033855UNSATISFIABLE
normalized-compression32_5.opb0.230617UNSATISFIABLE
normalized-compression32_11.opb1798.770UNKNOWN
normalized-compression64_9.opb1798.773UNKNOWN
normalized-compression64_14.opb1798.709UNKNOWN
normalized-compression16_6.opb0.080481UNSATISFIABLE
normalized-compression16_13.opb0.069478SATISFIABLE
normalized-compression16_11.opb55.5491SATISFIABLE
normalized-compression32_12.opb1798.762UNKNOWN
normalized-compression32_9.opb79.5794UNSATISFIABLE
normalized-compression32_13.opb1798.758UNKNOWN
normalized-compression16_12.opb7.43682SATISFIABLE
normalized-compression64_8.opb359.158UNSATISFIABLE
normalized-compression32_17.opb36.6442SATISFIABLE
normalized-compression32_18.opb0.577674SATISFIABLE
normalized-compression64_3.opb0.27645UNSATISFIABLE
normalized-compression64_11.opb1798.696UNKNOWN
normalized-compression16_15.opb0.041935SATISFIABLE
normalized-compression64_5.opb2.27137UNSATISFIABLE
normalized-compression64_12.opb1798.714UNKNOWN
normalized-compression32_6.opb0.626535UNSATISFIABLE
normalized-compression32_15.opb854.303SATISFIABLE
normalized-compression64_28.opb1.44724SATISFIABLE
normalized-compression64_20.opb1798.716UNKNOWN
normalized-compression64_22.opb13.1248SATISFIABLE
normalized-compression64_21.opb1798.718UNKNOWN
normalized-compression8_20.opb1.11992SATISFIABLE
normalized-compression64_19.opb1798.728UNKNOWN
normalized-compression16_7.opb0.210134UNSATISFIABLE
normalized-compression64_17.opb1798.708UNKNOWN
normalized-compression8_21.opb1.57915SATISFIABLE
normalized-compression64_16.opb1798.703UNKNOWN
normalized-compression16_10.opb21.0765UNSATISFIABLE
normalized-compression32_16.opb155.05SATISFIABLE
normalized-compression8_18.opb0.742083SATISFIABLE
normalized-compression32_10.opb291.863UNSATISFIABLE
normalized-compression64_15.opb1798.755UNKNOWN
normalized-compression8_17.opb6.00269SATISFIABLE
normalized-compression16_9.opb3.45207UNSATISFIABLE
normalized-compression64_30.opb2.08902SATISFIABLE
normalized-compression8_16.opb0.327234SATISFIABLE
normalized-compression64_27.opb1.58374SATISFIABLE
normalized-compression64_6.opb13.474UNSATISFIABLE
normalized-compression8_26.opb0.092276SATISFIABLE
normalized-compression64_13.opb1798.773UNKNOWN
normalized-compression8_14.opb17.8101UNSATISFIABLE
normalized-compression64_4.opb1.40021UNSATISFIABLE
normalized-compression16_4.opb0.029498UNSATISFIABLE
normalized-compression8_23.opb0.245781SATISFIABLE
normalized-compression32_19.opb0.500856SATISFIABLE
normalized-compression8_25.opb0.509338SATISFIABLE
normalized-compression16_8.opb0.659712UNSATISFIABLE
normalized-compression64_23.opb1798.711UNKNOWN
normalized-compression32_8.opb14.7501UNSATISFIABLE
normalized-compression64_7.opb104.196UNSATISFIABLE
normalized-compression64_29.opb1.50457SATISFIABLE
normalized-compression16_16.opb0.046341SATISFIABLE
normalized-compression64_25.opb54.1035SATISFIABLE
normalized-compression64_18.opb1798.725UNKNOWN
normalized-compression8_24.opb0.225551SATISFIABLE
normalized-compression16_14.opb0.074679SATISFIABLE
normalized-compression32_20.opb0.747492SATISFIABLE
normalized-sha1-size128-round22-2.opb1798.720UNKNOWN
normalized-sha1-size80-round21-1.opb39.234SATISFIABLE
normalized-sha1-size160-round23-6.opb1798.743UNKNOWN
normalized-sha1-size80-round23-6.opb1798.708UNKNOWN
normalized-sha1-size160-round23-8.opb1798.699UNKNOWN
normalized-sha1-size96-round23-2.opb1798.734UNKNOWN
normalized-sha1-size96-round21-1.opb5.45034SATISFIABLE
normalized-sha1-size96-round21-3.opb9.17966SATISFIABLE
normalized-sha1-size96-round22-5.opb1798.700UNKNOWN
normalized-sha1-size80-round23-9.opb1798.705UNKNOWN
normalized-sha1-size144-round21-6.opb219.829SATISFIABLE
normalized-sha1-size144-round22-7.opb1798.716UNKNOWN
normalized-sha1-size160-round21-0.opb670.586SATISFIABLE
normalized-sha1-size160-round23-7.opb1798.715UNKNOWN
normalized-sha1-size80-round21-5.opb140.173SATISFIABLE
normalized-sha1-size112-round23-4.opb1798.743UNKNOWN
normalized-sha1-size112-round21-8.opb1263.09SATISFIABLE
normalized-sha1-size160-round21-9.opb79.5365SATISFIABLE
normalized-sha1-size96-round21-0.opb240.764SATISFIABLE
normalized-sha1-size112-round22-7.opb1798.683UNKNOWN
normalized-sha1-size144-round21-2.opb995.719SATISFIABLE
normalized-sha1-size80-round21-4.opb13.0109SATISFIABLE
normalized-sha1-size160-round21-2.opb626.029SATISFIABLE
normalized-sha1-size160-round22-2.opb1798.692UNKNOWN
normalized-sha1-size144-round23-6.opb1800.448UNKNOWN
normalized-sha1-size112-round23-5.opb1798.705UNKNOWN
normalized-sha1-size80-round22-7.opb1798.712UNKNOWN
normalized-sha1-size128-round22-0.opb1798.720UNKNOWN
normalized-sha1-size112-round23-1.opb1800.459UNKNOWN
normalized-sha1-size80-round23-8.opb1798.690UNKNOWN
normalized-sha1-size160-round22-6.opb1798.686UNKNOWN
normalized-sha1-size160-round22-9.opb1798.708UNKNOWN
normalized-sha1-size80-round22-9.opb1635.88SATISFIABLE
normalized-sha1-size112-round22-4.opb1798.692UNKNOWN
normalized-sha1-size96-round22-6.opb1798.714UNKNOWN
normalized-sha1-size128-round23-9.opb1798.712UNKNOWN
normalized-sha1-size80-round21-8.opb31.2733SATISFIABLE
normalized-sha1-size128-round22-8.opb1798.713UNKNOWN
normalized-sha1-size128-round22-4.opb1798.701UNKNOWN
normalized-sha1-size144-round23-9.opb1798.731UNKNOWN
normalized-sha1-size128-round21-5.opb72.9217SATISFIABLE
normalized-sha1-size96-round21-9.opb471.517SATISFIABLE
normalized-sha1-size144-round23-4.opb1798.712UNKNOWN
normalized-sha1-size80-round21-3.opb147.097SATISFIABLE
normalized-sha1-size112-round23-8.opb1798.695UNKNOWN
normalized-sha1-size160-round23-5.opb1798.691UNKNOWN
normalized-sha1-size160-round21-1.opb489.7SATISFIABLE
normalized-sha1-size80-round23-1.opb1800.459UNKNOWN
normalized-sha1-size96-round23-9.opb1798.700UNKNOWN
normalized-sha1-size80-round21-7.opb54.4746SATISFIABLE
normalized-sha1-size96-round22-8.opb1798.706UNKNOWN
normalized-sha1-size128-round21-6.opb631.976SATISFIABLE
normalized-sha1-size160-round23-2.opb1798.710UNKNOWN
normalized-sha1-size80-round22-3.opb1798.711UNKNOWN
normalized-sha1-size112-round22-8.opb1798.699UNKNOWN
normalized-sha1-size128-round23-8.opb1798.695UNKNOWN
normalized-sha1-size160-round22-8.opb1798.677UNKNOWN
normalized-sha1-size96-round22-4.opb1798.692UNKNOWN
normalized-sha1-size160-round22-4.opb1798.692UNKNOWN
normalized-sha1-size112-round21-5.opb337.756SATISFIABLE
normalized-sha1-size80-round23-4.opb1798.736UNKNOWN
normalized-sha1-size128-round21-3.opb1089.43SATISFIABLE
normalized-sha1-size160-round22-1.opb1798.712UNKNOWN
normalized-sha1-size144-round22-8.opb1798.684UNKNOWN
normalized-sha1-size96-round23-0.opb1798.738UNKNOWN
normalized-sha1-size144-round22-9.opb1798.690UNKNOWN
normalized-sha1-size144-round21-1.opb1228.41SATISFIABLE
normalized-sha1-size128-round23-7.opb1798.693UNKNOWN
normalized-sha1-size96-round21-4.opb618.536SATISFIABLE
normalized-sha1-size160-round21-8.opb1798.705UNKNOWN
normalized-sha1-size80-round22-0.opb1798.725UNKNOWN
normalized-sha1-size160-round23-9.opb1798.704UNKNOWN
normalized-sha1-size112-round23-6.opb1798.697UNKNOWN
normalized-sha1-size80-round22-8.opb1798.701UNKNOWN
normalized-sha1-size144-round21-0.opb529.145SATISFIABLE
normalized-sha1-size80-round23-3.opb1798.693UNKNOWN
normalized-sha1-size160-round21-5.opb196.097SATISFIABLE
normalized-sha1-size80-round21-6.opb34.2588SATISFIABLE
normalized-sha1-size96-round21-7.opb89.3109SATISFIABLE
normalized-sha1-size160-round22-5.opb1798.711UNKNOWN
normalized-sha1-size128-round22-1.opb1798.743UNKNOWN
normalized-sha1-size144-round22-3.opb1798.700UNKNOWN
normalized-sha1-size160-round21-4.opb1004.36SATISFIABLE
normalized-sha1-size112-round21-9.opb3.89984SATISFIABLE
normalized-sha1-size112-round22-5.opb1798.711UNKNOWN
normalized-sha1-size96-round22-3.opb1193.69SATISFIABLE
normalized-sha1-size112-round23-7.opb1798.682UNKNOWN
normalized-sha1-size80-round22-5.opb1798.722UNKNOWN
normalized-sha1-size80-round21-9.opb31.1271SATISFIABLE
normalized-sha1-size128-round21-8.opb119.777SATISFIABLE
normalized-sha1-size80-round23-5.opb1798.701UNKNOWN
normalized-sha1-size80-round22-2.opb1798.689UNKNOWN
normalized-sha1-size112-round21-7.opb288.004SATISFIABLE
normalized-sha1-size160-round23-0.opb1798.687UNKNOWN
normalized-sha1-size128-round22-9.opb1798.702UNKNOWN
normalized-sha1-size128-round23-4.opb1798.704UNKNOWN
normalized-sha1-size96-round22-9.opb1800.450UNKNOWN
normalized-sha1-size80-round22-1.opb1798.728UNKNOWN
normalized-sha1-size128-round22-7.opb1798.699UNKNOWN
normalized-sha1-size112-round23-0.opb1798.704UNKNOWN
normalized-sha1-size96-round22-2.opb1135.65SATISFIABLE
normalized-sha1-size112-round23-2.opb1798.705UNKNOWN
normalized-sha1-size112-round22-1.opb1798.730UNKNOWN
normalized-sha1-size144-round23-3.opb1798.687UNKNOWN
normalized-sha1-size144-round23-7.opb1798.740UNKNOWN
normalized-sha1-size112-round22-0.opb1441.69SATISFIABLE
normalized-sha1-size112-round21-0.opb79.1674SATISFIABLE
normalized-sha1-size96-round23-5.opb1798.711UNKNOWN
normalized-sha1-size80-round23-0.opb1798.713UNKNOWN
normalized-sha1-size144-round22-4.opb1798.687UNKNOWN
normalized-sha1-size112-round21-3.opb491.369SATISFIABLE
normalized-sha1-size128-round21-2.opb345SATISFIABLE
normalized-sha1-size80-round21-2.opb80.0156SATISFIABLE
normalized-sha1-size144-round23-8.opb1798.703UNKNOWN
normalized-sha1-size160-round23-1.opb1798.723UNKNOWN
normalized-sha1-size96-round21-8.opb60.5998SATISFIABLE
normalized-sha1-size112-round21-6.opb243.952SATISFIABLE
normalized-sha1-size96-round23-6.opb1798.702UNKNOWN
normalized-sha1-size144-round21-3.opb1800.445UNKNOWN
normalized-sha1-size160-round23-3.opb1800.458UNKNOWN
normalized-sha1-size96-round22-7.opb1798.711UNKNOWN
normalized-sha1-size144-round23-1.opb1798.702UNKNOWN
normalized-sha1-size96-round22-1.opb1798.735UNKNOWN
normalized-sha1-size144-round22-1.opb1798.720UNKNOWN
normalized-sha1-size128-round23-2.opb1798.736UNKNOWN
normalized-sha1-size128-round21-4.opb287.401SATISFIABLE
normalized-sha1-size144-round23-5.opb1798.709UNKNOWN
normalized-sha1-size128-round22-3.opb266.854SATISFIABLE
normalized-sha1-size112-round22-6.opb1798.691UNKNOWN
normalized-sha1-size80-round23-7.opb1798.698UNKNOWN
normalized-sha1-size128-round23-1.opb1798.711UNKNOWN
normalized-sha1-size160-round21-7.opb850.862SATISFIABLE
normalized-sha1-size128-round22-6.opb1798.709UNKNOWN
normalized-sha1-size112-round21-4.opb54.136SATISFIABLE
normalized-sha1-size96-round23-1.opb1798.704UNKNOWN
normalized-sha1-size96-round23-4.opb1798.691UNKNOWN
normalized-sha1-size144-round22-6.opb1798.727UNKNOWN
normalized-sha1-size144-round21-7.opb36.2606SATISFIABLE
normalized-sha1-size160-round22-3.opb1798.724UNKNOWN
normalized-sha1-size128-round21-1.opb90.733SATISFIABLE
normalized-sha1-size128-round23-6.opb1798.708UNKNOWN
normalized-sha1-size112-round23-3.opb1798.711UNKNOWN
normalized-sha1-size128-round21-0.opb999.334SATISFIABLE
normalized-sha1-size96-round23-3.opb1798.702UNKNOWN
normalized-sha1-size144-round21-8.opb481.444SATISFIABLE
normalized-sha1-size96-round23-7.opb1798.695UNKNOWN
normalized-sha1-size96-round22-0.opb1704.61SATISFIABLE
normalized-sha1-size128-round21-9.opb626.239SATISFIABLE
normalized-sha1-size144-round21-5.opb141.102SATISFIABLE
normalized-sha1-size96-round23-8.opb1798.704UNKNOWN
normalized-sha1-size144-round22-0.opb1798.694UNKNOWN
normalized-sha1-size112-round22-9.opb1798.689UNKNOWN
normalized-sha1-size112-round21-1.opb539.848SATISFIABLE
normalized-sha1-size128-round22-5.opb1800.456UNKNOWN
normalized-sha1-size80-round21-0.opb336.129SATISFIABLE
normalized-sha1-size160-round21-6.opb367.311SATISFIABLE
normalized-sha1-size160-round22-0.opb1798.709UNKNOWN
normalized-sha1-size128-round23-5.opb1798.713UNKNOWN
normalized-sha1-size96-round21-2.opb245.469SATISFIABLE
normalized-sha1-size112-round21-2.opb202.458SATISFIABLE
normalized-sha1-size80-round22-6.opb1111.22SATISFIABLE
normalized-sha1-size144-round21-4.opb876.796SATISFIABLE
normalized-sha1-size144-round22-5.opb1798.725UNKNOWN
normalized-sha1-size96-round21-6.opb78.4342SATISFIABLE
normalized-sha1-size160-round21-3.opb365.786SATISFIABLE
normalized-sha1-size80-round23-2.opb1798.745UNKNOWN
normalized-sha1-size144-round21-9.opb1798.721UNKNOWN
normalized-sha1-size128-round23-0.opb1798.731UNKNOWN
normalized-sha1-size112-round23-9.opb1798.703UNKNOWN
normalized-sha1-size128-round21-7.opb841.488SATISFIABLE
normalized-sha1-size144-round22-2.opb1798.719UNKNOWN
normalized-sha1-size144-round23-2.opb1798.675UNKNOWN
normalized-sha1-size128-round23-3.opb1798.728UNKNOWN
normalized-sha1-size112-round22-3.opb1367.47SATISFIABLE
normalized-sha1-size160-round22-7.opb1798.691UNKNOWN
normalized-sha1-size112-round22-2.opb1798.702UNKNOWN
normalized-sha1-size160-round23-4.opb1798.727UNKNOWN
normalized-sha1-size80-round22-4.opb1798.678UNKNOWN
normalized-sha1-size144-round23-0.opb1798.707UNKNOWN
normalized-sha1-size96-round21-5.opb702.75SATISFIABLE
normalized-hw128-vm50p-dec.opb.negationfix.opbUNKNOWN
normalized-hw128-vm75p-dec.opb.negationfix.opbUNKNOWN
normalized-hw128-vm25p-dec.opb.negationfix.opbUNKNOWN
normalized-hw128-vm85p-dec.opb.negationfix.opbUNKNOWN
normalized-tseitin-regular-n66-d3-i3-f.cnf.gz-plain.pb.metafix.opb75.8058UNSATISFIABLE
normalized-tseitin-regular-n88-d3-i3-r1.cnf.gz-plain.pb.metafix.opb576.524UNSATISFIABLE
normalized-tseitin-regular-n68-d3-i3-r1.cnf.gz-plain.pb.metafix.opb61.2147UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i2-r2.cnf.gz-plain.pb.metafix.opb287.758UNSATISFIABLE
normalized-tseitin-regular-n56-d3-i1-r2.cnf.gz-plain.pb.metafix.opb11.4523UNSATISFIABLE
normalized-subsetCardinalitySigma-25-3.cnf.gz-plain.pb.metafix.opb89.6638UNSATISFIABLE
normalized-tseitin-regular-n38-d3-i3-f.cnf.gz-plain.pb.metafix.opb0.440731UNSATISFIABLE
normalized-regular-n20-d4-i3.cnf.gz-plain.pb.metafix.opb90.2037UNSATISFIABLE
normalized-tseitin-regular-n52-d3-i1-r1.cnf.gz-plain.pb.metafix.opb2.25916UNSATISFIABLE
normalized-tseitin-regular-n90-d3-i1-r2.cnf.gz-plain.pb.metafix.opb367.837UNSATISFIABLE
normalized-fixed-bandwidth-92.cnf.gz-extracted.pb.metafix.opb1798.737UNKNOWN
normalized-fixed-bandwidth-72.cnf.gz-extracted.pb.metafix.opb1798.779UNKNOWN
normalized-tseitin-regular-n94-d3-i2-r2.cnf.gz-plain.pb.metafix.opb1473.2UNSATISFIABLE
normalized-fixed-bandwidth-61.cnf.gz-extracted.pb.metafix.opb1798.761UNKNOWN
normalized-subsetCardinalitySigma-24-2.cnf.gz-extracted.pb.metafix.opb201.201UNSATISFIABLE
normalized-tseitin-regular-n64-d3-i3-r1.cnf.gz-plain.pb.metafix.opb7.5995UNSATISFIABLE
normalized-regular-n24-d4-i1.cnf.gz-plain.pb.metafix.opb1798.783UNKNOWN
normalized-tseitin-regular-n56-d3-i3-r1.cnf.gz-plain.pb.metafix.opb11.7597UNSATISFIABLE
normalized-fixed-bandwidth-60.cnf.gz-extracted.pb.metafix.opb1798.767UNKNOWN
normalized-tseitin-regular-n90-d3-i1-f.cnf.gz-plain.pb.metafix.opb410.36UNSATISFIABLE
normalized-tseitin-regular-n66-d3-i3-r1.cnf.gz-plain.pb.metafix.opb89.5314UNSATISFIABLE
normalized-tseitin-regular-n42-d3-i2-r1.cnf.gz-plain.pb.metafix.opb0.267072UNSATISFIABLE
normalized-fixed-bandwidth-65.cnf.gz-extracted.pb.metafix.opb1798.765UNKNOWN
normalized-regular-n23-d4-i1.cnf.gz-plain.pb.metafix.opb345.717UNSATISFIABLE
normalized-fixed-bandwidth-88.cnf.gz-extracted.pb.metafix.opb1798.750UNKNOWN
normalized-tseitin-regular-n82-d3-i1-f.cnf.gz-plain.pb.metafix.opb329.769UNSATISFIABLE
normalized-fixed-bandwidth-98.cnf.gz-extracted.pb.metafix.opb1798.729UNKNOWN
normalized-tseitin-regular-n66-d3-i1-f.cnf.gz-plain.pb.metafix.opb4.16218UNSATISFIABLE
normalized-tseitin-regular-n86-d3-i1-r2.cnf.gz-plain.pb.metafix.opb946.365UNSATISFIABLE
normalized-tseitin-regular-n58-d3-i3-f.cnf.gz-plain.pb.metafix.opb8.87263UNSATISFIABLE
normalized-tseitin-regular-n50-d3-i3-r2.cnf.gz-plain.pb.metafix.opb0.627749UNSATISFIABLE
normalized-subsetCardinalitySigma-25-2.cnf.gz-extracted.pb.metafix.opb934.88UNSATISFIABLE
normalized-tseitin-regular-n74-d3-i1-r2.cnf.gz-plain.pb.metafix.opb32.9477UNSATISFIABLE
normalized-tseitin-regular-n42-d3-i2-r2.cnf.gz-plain.pb.metafix.opb0.262529UNSATISFIABLE
normalized-tseitin-regular-n58-d3-i1-r1.cnf.gz-plain.pb.metafix.opb4.65928UNSATISFIABLE
normalized-subsetCardinalitySigma-28-2.cnf.gz-plain.pb.metafix.opb850.216UNSATISFIABLE
normalized-tseitin-regular-n76-d3-i1-r1.cnf.gz-plain.pb.metafix.opb305.994UNSATISFIABLE
normalized-tseitin-regular-n44-d3-i1-r1.cnf.gz-plain.pb.metafix.opb0.236996UNSATISFIABLE
normalized-fixed-bandwidth-27.cnf.gz-extracted.pb.metafix.opb1798.769UNKNOWN
normalized-tseitin-regular-n60-d3-i2-r1.cnf.gz-plain.pb.metafix.opb4.76033UNSATISFIABLE
normalized-tseitin-regular-n68-d3-i1-r2.cnf.gz-plain.pb.metafix.opb27.59UNSATISFIABLE
normalized-regular-n22-d4-i1.cnf.gz-extracted.pb.metafix.opb157.865UNSATISFIABLE
normalized-regular-n24-d4-i3.cnf.gz-extracted.pb.metafix.opb1798.771UNKNOWN
normalized-tseitin-regular-n72-d3-i2-r1.cnf.gz-plain.pb.metafix.opb140.575UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i1-r2.cnf.gz-plain.pb.metafix.opb10.0765UNSATISFIABLE
normalized-tseitin-regular-n92-d3-i1-r1.cnf.gz-plain.pb.metafix.opb654.139UNSATISFIABLE
normalized-tseitin-regular-n54-d3-i2-r2.cnf.gz-plain.pb.metafix.opb0.171202UNSATISFIABLE
normalized-regular-n21-d4-i3.cnf.gz-extracted.pb.metafix.opb101.037UNSATISFIABLE
normalized-tseitin-regular-n38-d3-i1-r2.cnf.gz-plain.pb.metafix.opb0.291651UNSATISFIABLE
normalized-subsetCardinalitySigma-22-3.cnf.gz-plain.pb.metafix.opb149.735UNSATISFIABLE
normalized-regular-n26-d4-i3.cnf.gz-extracted.pb.metafix.opb1798.774UNKNOWN
normalized-tseitin-regular-n40-d3-i1-r1.cnf.gz-plain.pb.metafix.opb0.331239UNSATISFIABLE
normalized-fixed-bandwidth-68.cnf.gz-extracted.pb.metafix.opb1798.740UNKNOWN
normalized-fixed-bandwidth-51.cnf.gz-extracted.pb.metafix.opb1798.710UNKNOWN
normalized-tseitin-regular-n90-d3-i1-r1.cnf.gz-plain.pb.metafix.opb330.525UNSATISFIABLE
normalized-subsetCardinalitySigma-24-1.cnf.gz-plain.pb.metafix.opb153.324UNSATISFIABLE
normalized-tseitin-regular-n80-d3-i1-r2.cnf.gz-plain.pb.metafix.opb123.419UNSATISFIABLE
normalized-subsetCardinalitySigma-23-1.cnf.gz-plain.pb.metafix.opb113.836UNSATISFIABLE
normalized-subsetCardinalitySigma-22-1.cnf.gz-plain.pb.metafix.opb132.785UNSATISFIABLE
normalized-tseitin-regular-n62-d3-i3-f.cnf.gz-plain.pb.metafix.opb15.4846UNSATISFIABLE
normalized-regular-n18-d4-i2.cnf.gz-plain.pb.metafix.opb37.4403UNSATISFIABLE
normalized-tseitin-regular-n56-d3-i1-r1.cnf.gz-plain.pb.metafix.opb10.9065UNSATISFIABLE
normalized-tseitin-regular-n42-d3-i1-r2.cnf.gz-plain.pb.metafix.opb1.72534UNSATISFIABLE
normalized-tseitin-regular-n44-d3-i3-r2.cnf.gz-plain.pb.metafix.opb0.88605UNSATISFIABLE
normalized-regular-n26-d4-i3.cnf.gz-plain.pb.metafix.opb1798.761UNKNOWN
normalized-tseitin-regular-n52-d3-i1-r2.cnf.gz-plain.pb.metafix.opb2.26421UNSATISFIABLE
normalized-tseitin-regular-n52-d3-i2-r2.cnf.gz-plain.pb.metafix.opb6.94524UNSATISFIABLE
normalized-tseitin-regular-n58-d3-i1-f.cnf.gz-plain.pb.metafix.opb4.6341UNSATISFIABLE
normalized-tseitin-regular-n76-d3-i2-r2.cnf.gz-plain.pb.metafix.opb935.511UNSATISFIABLE
normalized-tseitin-regular-n48-d3-i3-f.cnf.gz-plain.pb.metafix.opb2.10641UNSATISFIABLE
normalized-regular-n17-d4-i3.cnf.gz-plain.pb.metafix.opb27.8529UNSATISFIABLE
normalized-subsetCardinalitySigma-24-3.cnf.gz-plain.pb.metafix.opb158.102UNSATISFIABLE
normalized-fixed-bandwidth-71.cnf.gz-extracted.pb.metafix.opb1798.762UNKNOWN
normalized-tseitin-regular-n64-d3-i2-f.cnf.gz-plain.pb.metafix.opb4.83978UNSATISFIABLE
normalized-subsetCardinalitySigma-21-2.cnf.gz-plain.pb.metafix.opb26.7531UNSATISFIABLE
normalized-subsetCardinalitySigma-25-3.cnf.gz-extracted.pb.metafix.opb115.82UNSATISFIABLE
normalized-tseitin-regular-n40-d3-i3-r2.cnf.gz-plain.pb.metafix.opb1.56836UNSATISFIABLE
normalized-fixed-bandwidth-64.cnf.gz-extracted.pb.metafix.opb1798.747UNKNOWN
normalized-tseitin-regular-n94-d3-i2-f.cnf.gz-plain.pb.metafix.opb764.01UNSATISFIABLE
normalized-fixed-bandwidth-22.cnf.gz-extracted.pb.metafix.opb1798.768UNKNOWN
normalized-tseitin-regular-n56-d3-i3-r2.cnf.gz-plain.pb.metafix.opb12.0734UNSATISFIABLE
normalized-tseitin-regular-n60-d3-i1-f.cnf.gz-plain.pb.metafix.opb4.58559UNSATISFIABLE
normalized-tseitin-regular-n40-d3-i2-f.cnf.gz-plain.pb.metafix.opb0.590896UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i3-f.cnf.gz-plain.pb.metafix.opb399.472UNSATISFIABLE
normalized-tseitin-regular-n64-d3-i3-r2.cnf.gz-plain.pb.metafix.opb6.70011UNSATISFIABLE
normalized-fixed-bandwidth-16.cnf.gz-plain.pb.metafix.opb71.2285UNSATISFIABLE
normalized-fixed-bandwidth-84.cnf.gz-extracted.pb.metafix.opb1798.784UNKNOWN
normalized-fixed-bandwidth-95.cnf.gz-extracted.pb.metafix.opb1798.746UNKNOWN
normalized-fixed-bandwidth-89.cnf.gz-extracted.pb.metafix.opb1798.742UNKNOWN
normalized-fixed-bandwidth-19.cnf.gz-plain.pb.metafix.opb625.613UNSATISFIABLE
normalized-subsetCardinalitySigma-21-1.cnf.gz-plain.pb.metafix.opb68.4278UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i2-r2.cnf.gz-plain.pb.metafix.opb25.3881UNSATISFIABLE
normalized-subsetCardinalitySigma-27-3.cnf.gz-extracted.pb.metafix.opb998.164UNSATISFIABLE
normalized-tseitin-regular-n92-d3-i3-f.cnf.gz-plain.pb.metafix.opb1686.96UNSATISFIABLE
normalized-tseitin-regular-n64-d3-i1-r1.cnf.gz-plain.pb.metafix.opb3.76122UNSATISFIABLE
normalized-regular-n22-d4-i2.cnf.gz-extracted.pb.metafix.opb150.851UNSATISFIABLE
normalized-tseitin-regular-n74-d3-i3-r1.cnf.gz-plain.pb.metafix.opb72.5153UNSATISFIABLE
normalized-tseitin-regular-n68-d3-i2-r1.cnf.gz-plain.pb.metafix.opb26.9455UNSATISFIABLE
normalized-subsetCardinalitySigma-26-1.cnf.gz-plain.pb.metafix.opb532.881UNSATISFIABLE
normalized-tseitin-regular-n76-d3-i2-r1.cnf.gz-plain.pb.metafix.opb1092.01UNSATISFIABLE
normalized-tseitin-regular-n84-d3-i2-r2.cnf.gz-plain.pb.metafix.opb1519.23UNSATISFIABLE
normalized-subsetCardinalitySigma-29-3.cnf.gz-extracted.pb.metafix.opb1798.760UNKNOWN
normalized-tseitin-regular-n66-d3-i2-r1.cnf.gz-plain.pb.metafix.opb27.014UNSATISFIABLE
normalized-fixed-bandwidth-83.cnf.gz-extracted.pb.metafix.opb1798.739UNKNOWN
normalized-regular-n16-d4-i2.cnf.gz-plain.pb.metafix.opb11.7399UNSATISFIABLE
normalized-tseitin-regular-n72-d3-i3-f.cnf.gz-plain.pb.metafix.opb10.6972UNSATISFIABLE
normalized-tseitin-regular-n52-d3-i3-r1.cnf.gz-plain.pb.metafix.opb1.24215UNSATISFIABLE
normalized-fixed-bandwidth-17.cnf.gz-plain.pb.metafix.opb160.521UNSATISFIABLE
normalized-regular-n21-d4-i1.cnf.gz-plain.pb.metafix.opb23.9748UNSATISFIABLE
normalized-regular-n26-d4-i1.cnf.gz-extracted.pb.metafix.opb1798.754UNKNOWN
normalized-subsetCardinalitySigma-20-3.cnf.gz-plain.pb.metafix.opb29.5859UNSATISFIABLE
normalized-tseitin-regular-n76-d3-i3-r2.cnf.gz-plain.pb.metafix.opb218.021UNSATISFIABLE
normalized-tseitin-regular-n62-d3-i3-r2.cnf.gz-plain.pb.metafix.opb15.4968UNSATISFIABLE
normalized-subsetCardinalitySigma-17-3.cnf.gz-plain.pb.metafix.opb2.97605UNSATISFIABLE
normalized-subsetCardinalitySigma-24-2.cnf.gz-plain.pb.metafix.opb201.399UNSATISFIABLE
normalized-tseitin-regular-n90-d3-i2-r2.cnf.gz-plain.pb.metafix.opb1447.94UNSATISFIABLE
normalized-regular-n19-d4-i3.cnf.gz-plain.pb.metafix.opb28.5119UNSATISFIABLE
normalized-tseitin-regular-n84-d3-i2-r1.cnf.gz-plain.pb.metafix.opb1520.88UNSATISFIABLE
normalized-tseitin-regular-n76-d3-i2-f.cnf.gz-plain.pb.metafix.opb746.94UNSATISFIABLE
normalized-fixed-bandwidth-100.cnf.gz-extracted.pb.metafix.opb1798.748UNKNOWN
normalized-tseitin-regular-n84-d3-i3-r1.cnf.gz-plain.pb.metafix.opb727.47UNSATISFIABLE
normalized-fixed-bandwidth-91.cnf.gz-extracted.pb.metafix.opb1798.715UNKNOWN
normalized-tseitin-regular-n46-d3-i3-r1.cnf.gz-plain.pb.metafix.opb0.65304UNSATISFIABLE
normalized-tseitin-regular-n38-d3-i3-r2.cnf.gz-plain.pb.metafix.opb0.442785UNSATISFIABLE
normalized-tseitin-regular-n46-d3-i1-r2.cnf.gz-plain.pb.metafix.opb2.9512UNSATISFIABLE
normalized-fixed-bandwidth-97.cnf.gz-extracted.pb.metafix.opb1798.713UNKNOWN
normalized-subsetCardinalitySigma-27-1.cnf.gz-plain.pb.metafix.opb844.84UNSATISFIABLE
normalized-tseitin-regular-n72-d3-i1-r1.cnf.gz-plain.pb.metafix.opb46.3468UNSATISFIABLE
normalized-tseitin-regular-n48-d3-i1-r1.cnf.gz-plain.pb.metafix.opb0.727246UNSATISFIABLE
normalized-tseitin-regular-n84-d3-i1-r1.cnf.gz-plain.pb.metafix.opb319.624UNSATISFIABLE
normalized-tseitin-regular-n50-d3-i2-r2.cnf.gz-plain.pb.metafix.opb0.376543UNSATISFIABLE
normalized-tseitin-regular-n86-d3-i3-r1.cnf.gz-plain.pb.metafix.opb553.201UNSATISFIABLE
normalized-tseitin-regular-n86-d3-i2-f.cnf.gz-plain.pb.metafix.opb1158.3UNSATISFIABLE
normalized-tseitin-regular-n80-d3-i1-f.cnf.gz-plain.pb.metafix.opb131.916UNSATISFIABLE
normalized-subsetCardinalitySigma-20-1.cnf.gz-plain.pb.metafix.opb12.4582UNSATISFIABLE
normalized-tseitin-regular-n74-d3-i1-r1.cnf.gz-plain.pb.metafix.opb54.4995UNSATISFIABLE
normalized-tseitin-regular-n60-d3-i2-f.cnf.gz-plain.pb.metafix.opb4.76248UNSATISFIABLE
normalized-subsetCardinalitySigma-20-2.cnf.gz-plain.pb.metafix.opb20.0177UNSATISFIABLE
normalized-tseitin-regular-n50-d3-i2-r1.cnf.gz-plain.pb.metafix.opb0.600383UNSATISFIABLE
normalized-tseitin-regular-n54-d3-i2-f.cnf.gz-plain.pb.metafix.opb0.172607UNSATISFIABLE
normalized-tseitin-regular-n62-d3-i1-r2.cnf.gz-plain.pb.metafix.opb18.0235UNSATISFIABLE
normalized-tseitin-regular-n86-d3-i3-r2.cnf.gz-plain.pb.metafix.opb498.946UNSATISFIABLE
normalized-fixed-bandwidth-81.cnf.gz-extracted.pb.metafix.opb1798.738UNKNOWN
normalized-tseitin-regular-n66-d3-i2-f.cnf.gz-plain.pb.metafix.opb26.2024UNSATISFIABLE
normalized-tseitin-regular-n52-d3-i3-f.cnf.gz-plain.pb.metafix.opb1.27749UNSATISFIABLE
normalized-tseitin-regular-n88-d3-i3-f.cnf.gz-plain.pb.metafix.opb734.744UNSATISFIABLE
normalized-tseitin-regular-n72-d3-i1-r2.cnf.gz-plain.pb.metafix.opb45.9899UNSATISFIABLE
normalized-regular-n18-d4-i1.cnf.gz-plain.pb.metafix.opb26.8667UNSATISFIABLE
normalized-tseitin-regular-n58-d3-i1-r2.cnf.gz-plain.pb.metafix.opb4.31083UNSATISFIABLE
normalized-tseitin-regular-n84-d3-i3-f.cnf.gz-plain.pb.metafix.opb1194.33UNSATISFIABLE
normalized-tseitin-regular-n68-d3-i2-r2.cnf.gz-plain.pb.metafix.opb33.7681UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i1-r1.cnf.gz-plain.pb.metafix.opb10.0908UNSATISFIABLE
normalized-regular-n23-d4-i2.cnf.gz-plain.pb.metafix.opb65.3594UNSATISFIABLE
normalized-fixed-bandwidth-66.cnf.gz-extracted.pb.metafix.opb1798.731UNKNOWN
normalized-fixed-bandwidth-75.cnf.gz-extracted.pb.metafix.opb1798.755UNKNOWN
normalized-fixed-bandwidth-17.cnf.gz-extracted.pb.metafix.opb138.466UNSATISFIABLE
normalized-fixed-bandwidth-85.cnf.gz-extracted.pb.metafix.opb1798.742UNKNOWN
normalized-tseitin-regular-n68-d3-i1-f.cnf.gz-plain.pb.metafix.opb26.4141UNSATISFIABLE
normalized-subsetCardinalitySigma-29-1.cnf.gz-extracted.pb.metafix.opb1798.793UNKNOWN
normalized-tseitin-regular-n58-d3-i2-r1.cnf.gz-plain.pb.metafix.opb21.4175UNSATISFIABLE
normalized-tseitin-regular-n84-d3-i3-r2.cnf.gz-plain.pb.metafix.opb950.928UNSATISFIABLE
normalized-tseitin-regular-n46-d3-i1-f.cnf.gz-plain.pb.metafix.opb2.18725UNSATISFIABLE
normalized-subsetCardinalitySigma-30-2.cnf.gz-extracted.pb.metafix.opb1798.774UNKNOWN
normalized-subsetCardinalitySigma-23-2.cnf.gz-extracted.pb.metafix.opb176.432UNSATISFIABLE
normalized-tseitin-regular-n88-d3-i1-r2.cnf.gz-plain.pb.metafix.opb580.88UNSATISFIABLE
normalized-fixed-bandwidth-70.cnf.gz-extracted.pb.metafix.opb1798.732UNKNOWN
normalized-tseitin-regular-n48-d3-i1-f.cnf.gz-plain.pb.metafix.opb0.72893UNSATISFIABLE
normalized-tseitin-regular-n92-d3-i3-r1.cnf.gz-plain.pb.metafix.opb1745.11UNSATISFIABLE
normalized-tseitin-regular-n68-d3-i3-f.cnf.gz-plain.pb.metafix.opb61.1713UNSATISFIABLE
normalized-tseitin-regular-n52-d3-i1-f.cnf.gz-plain.pb.metafix.opb1.955UNSATISFIABLE
normalized-fixed-bandwidth-87.cnf.gz-extracted.pb.metafix.opb1798.718UNKNOWN
normalized-regular-n21-d4-i3.cnf.gz-plain.pb.metafix.opb271.049UNSATISFIABLE
normalized-fixed-bandwidth-67.cnf.gz-extracted.pb.metafix.opb1798.760UNKNOWN
normalized-fixed-bandwidth-23.cnf.gz-extracted.pb.metafix.opb1798.688UNKNOWN
normalized-regular-n17-d4-i2.cnf.gz-plain.pb.metafix.opb12.128UNSATISFIABLE
normalized-fixed-bandwidth-94.cnf.gz-extracted.pb.metafix.opb1800.460UNKNOWN
normalized-regular-n29-d4-i2.cnf.gz-plain.pb.metafix.opb1798.762UNKNOWN
normalized-subsetCardinalitySigma-23-2.cnf.gz-plain.pb.metafix.opb363.356UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i3-r1.cnf.gz-plain.pb.metafix.opb399.74UNSATISFIABLE
normalized-tseitin-regular-n82-d3-i3-r2.cnf.gz-plain.pb.metafix.opb479.131UNSATISFIABLE
normalized-regular-n26-d4-i2.cnf.gz-extracted.pb.metafix.opb1798.732UNKNOWN
normalized-fixed-bandwidth-18.cnf.gz-extracted.pb.metafix.opb378.293UNSATISFIABLE
normalized-regular-n22-d4-i2.cnf.gz-plain.pb.metafix.opb157.567UNSATISFIABLE
normalized-subsetCardinalitySigma-18-1.cnf.gz-plain.pb.metafix.opb4.88856UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i3-r2.cnf.gz-plain.pb.metafix.opb5.06635UNSATISFIABLE
normalized-tseitin-regular-n90-d3-i2-r1.cnf.gz-plain.pb.metafix.opb1448.33UNSATISFIABLE
normalized-tseitin-regular-n40-d3-i2-r2.cnf.gz-plain.pb.metafix.opb1.18799UNSATISFIABLE
normalized-tseitin-regular-n40-d3-i2-r1.cnf.gz-plain.pb.metafix.opb0.993043UNSATISFIABLE
normalized-regular-n19-d4-i1.cnf.gz-plain.pb.metafix.opb67.1223UNSATISFIABLE
normalized-regular-n25-d4-i2.cnf.gz-extracted.pb.metafix.opb1798.803UNKNOWN
normalized-tseitin-regular-n50-d3-i2-f.cnf.gz-plain.pb.metafix.opb0.374819UNSATISFIABLE
normalized-tseitin-regular-n56-d3-i2-r2.cnf.gz-plain.pb.metafix.opb7.64087UNSATISFIABLE
normalized-tseitin-regular-n90-d3-i3-r1.cnf.gz-plain.pb.metafix.opb1641.1UNSATISFIABLE
normalized-fixed-bandwidth-80.cnf.gz-extracted.pb.metafix.opb1798.768UNKNOWN
normalized-subsetCardinalitySigma-24-3.cnf.gz-extracted.pb.metafix.opb97.9906UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i3-r1.cnf.gz-plain.pb.metafix.opb5.14715UNSATISFIABLE
normalized-tseitin-regular-n80-d3-i3-f.cnf.gz-plain.pb.metafix.opb1543.84UNSATISFIABLE
normalized-tseitin-regular-n96-d3-i1-r2.cnf.gz-plain.pb.metafix.opb1781.57UNSATISFIABLE
normalized-tseitin-regular-n56-d3-i2-r1.cnf.gz-plain.pb.metafix.opb10.9791UNSATISFIABLE
normalized-fixed-bandwidth-21.cnf.gz-extracted.pb.metafix.opb1798.761UNKNOWN
normalized-tseitin-regular-n44-d3-i2-r2.cnf.gz-plain.pb.metafix.opb0.292409UNSATISFIABLE
normalized-tseitin-regular-n76-d3-i3-f.cnf.gz-plain.pb.metafix.opb343.504UNSATISFIABLE
normalized-tseitin-regular-n44-d3-i1-f.cnf.gz-plain.pb.metafix.opb0.257418UNSATISFIABLE
normalized-tseitin-regular-n54-d3-i3-f.cnf.gz-plain.pb.metafix.opb4.46673UNSATISFIABLE
normalized-fixed-bandwidth-26.cnf.gz-extracted.pb.metafix.opb1800.465UNKNOWN
normalized-tseitin-regular-n76-d3-i1-r2.cnf.gz-plain.pb.metafix.opb481.712UNSATISFIABLE
normalized-tseitin-regular-n82-d3-i2-r1.cnf.gz-plain.pb.metafix.opb59.567UNSATISFIABLE
normalized-tseitin-regular-n74-d3-i3-r2.cnf.gz-plain.pb.metafix.opb96.3159UNSATISFIABLE
normalized-fixed-bandwidth-16.cnf.gz-extracted.pb.metafix.opb130.223UNSATISFIABLE
normalized-tseitin-regular-n80-d3-i3-r1.cnf.gz-plain.pb.metafix.opb1315.95UNSATISFIABLE
normalized-tseitin-regular-n60-d3-i3-f.cnf.gz-plain.pb.metafix.opb16.7691UNSATISFIABLE
normalized-tseitin-regular-n82-d3-i1-r1.cnf.gz-plain.pb.metafix.opb247.015UNSATISFIABLE
normalized-tseitin-regular-n66-d3-i1-r1.cnf.gz-plain.pb.metafix.opb3.38803UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i1-f.cnf.gz-plain.pb.metafix.opb140.646UNSATISFIABLE
normalized-subsetCardinalitySigma-22-2.cnf.gz-plain.pb.metafix.opb12.3381UNSATISFIABLE
normalized-regular-n23-d4-i2.cnf.gz-extracted.pb.metafix.opb72.7405UNSATISFIABLE
normalized-tseitin-regular-n72-d3-i1-f.cnf.gz-plain.pb.metafix.opb45.8812UNSATISFIABLE
normalized-tseitin-regular-n50-d3-i1-r2.cnf.gz-plain.pb.metafix.opb2.13741UNSATISFIABLE
normalized-tseitin-regular-n46-d3-i1-r1.cnf.gz-plain.pb.metafix.opb2.95495UNSATISFIABLE
normalized-tseitin-regular-n74-d3-i3-f.cnf.gz-plain.pb.metafix.opb155.205UNSATISFIABLE
normalized-tseitin-regular-n94-d3-i1-f.cnf.gz-plain.pb.metafix.opb1510.2UNSATISFIABLE
normalized-tseitin-regular-n92-d3-i3-r2.cnf.gz-plain.pb.metafix.opb1705.52UNSATISFIABLE
normalized-tseitin-regular-n62-d3-i2-r2.cnf.gz-plain.pb.metafix.opb9.59516UNSATISFIABLE
normalized-subsetCardinalitySigma-25-1.cnf.gz-plain.pb.metafix.opb194.464UNSATISFIABLE
normalized-tseitin-regular-n72-d3-i2-f.cnf.gz-plain.pb.metafix.opb140.93UNSATISFIABLE
normalized-tseitin-regular-n46-d3-i2-r1.cnf.gz-plain.pb.metafix.opb0.934782UNSATISFIABLE
normalized-fixed-bandwidth-58.cnf.gz-extracted.pb.metafix.opb1798.761UNKNOWN
normalized-tseitin-regular-n38-d3-i2-f.cnf.gz-plain.pb.metafix.opb0.35851UNSATISFIABLE
normalized-tseitin-regular-n50-d3-i1-r1.cnf.gz-plain.pb.metafix.opb2.13489UNSATISFIABLE
normalized-fixed-bandwidth-76.cnf.gz-extracted.pb.metafix.opb1798.719UNKNOWN
normalized-tseitin-regular-n44-d3-i3-r1.cnf.gz-plain.pb.metafix.opb0.834629UNSATISFIABLE
normalized-subsetCardinalitySigma-28-3.cnf.gz-extracted.pb.metafix.opb1800.474UNKNOWN
normalized-tseitin-regular-n50-d3-i1-f.cnf.gz-plain.pb.metafix.opb2.04557UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i1-r2.cnf.gz-plain.pb.metafix.opb75.3949UNSATISFIABLE
normalized-tseitin-regular-n58-d3-i2-f.cnf.gz-plain.pb.metafix.opb26.9509UNSATISFIABLE
normalized-tseitin-regular-n82-d3-i2-f.cnf.gz-plain.pb.metafix.opb61.6848UNSATISFIABLE
normalized-subsetCardinalitySigma-22-1.cnf.gz-extracted.pb.metafix.opb156.857UNSATISFIABLE
normalized-fixed-bandwidth-63.cnf.gz-extracted.pb.metafix.opb1798.778UNKNOWN
normalized-tseitin-regular-n48-d3-i2-r1.cnf.gz-plain.pb.metafix.opb9.82058UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i2-r1.cnf.gz-plain.pb.metafix.opb24.8195UNSATISFIABLE
normalized-tseitin-regular-n86-d3-i1-f.cnf.gz-plain.pb.metafix.opb1165.17UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i2-r1.cnf.gz-plain.pb.metafix.opb328.617UNSATISFIABLE
normalized-fixed-bandwidth-69.cnf.gz-extracted.pb.metafix.opb1798.754UNKNOWN
normalized-tseitin-regular-n74-d3-i1-f.cnf.gz-plain.pb.metafix.opb29.0261UNSATISFIABLE
normalized-fixed-bandwidth-86.cnf.gz-extracted.pb.metafix.opb1798.754UNKNOWN
normalized-tseitin-regular-n72-d3-i3-r1.cnf.gz-plain.pb.metafix.opb17.5904UNSATISFIABLE
normalized-fixed-bandwidth-19.cnf.gz-extracted.pb.metafix.opb977.019UNSATISFIABLE
normalized-tseitin-regular-n62-d3-i2-r1.cnf.gz-plain.pb.metafix.opb10.6838UNSATISFIABLE
normalized-regular-n28-d4-i3.cnf.gz-extracted.pb.metafix.opb1800.465UNKNOWN
normalized-fixed-bandwidth-55.cnf.gz-extracted.pb.metafix.opb1798.737UNKNOWN
normalized-tseitin-regular-n56-d3-i1-f.cnf.gz-plain.pb.metafix.opb10.9428UNSATISFIABLE
normalized-subsetCardinalitySigma-19-2.cnf.gz-plain.pb.metafix.opb35.6806UNSATISFIABLE
normalized-tseitin-regular-n74-d3-i2-f.cnf.gz-plain.pb.metafix.opb315.067UNSATISFIABLE
normalized-tseitin-regular-n48-d3-i3-r2.cnf.gz-plain.pb.metafix.opb2.10472UNSATISFIABLE
normalized-tseitin-regular-n46-d3-i3-f.cnf.gz-plain.pb.metafix.opb0.805141UNSATISFIABLE
normalized-subsetCardinalitySigma-23-3.cnf.gz-plain.pb.metafix.opb150.726UNSATISFIABLE
normalized-tseitin-regular-n38-d3-i1-f.cnf.gz-plain.pb.metafix.opb0.290758UNSATISFIABLE
normalized-tseitin-regular-n94-d3-i2-r1.cnf.gz-plain.pb.metafix.opb737.851UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i2-f.cnf.gz-plain.pb.metafix.opb287.839UNSATISFIABLE
normalized-tseitin-regular-n52-d3-i3-r2.cnf.gz-plain.pb.metafix.opb1.81003UNSATISFIABLE
normalized-tseitin-regular-n68-d3-i2-f.cnf.gz-plain.pb.metafix.opb26.0395UNSATISFIABLE
normalized-subsetCardinalitySigma-19-3.cnf.gz-plain.pb.metafix.opb26.924UNSATISFIABLE
normalized-regular-n27-d4-i3.cnf.gz-extracted.pb.metafix.opb1798.801UNKNOWN
normalized-tseitin-regular-n84-d3-i1-r2.cnf.gz-plain.pb.metafix.opb319.12UNSATISFIABLE
normalized-tseitin-regular-n64-d3-i1-f.cnf.gz-plain.pb.metafix.opb5.27928UNSATISFIABLE
normalized-subsetCardinalitySigma-25-1.cnf.gz-extracted.pb.metafix.opb177.856UNSATISFIABLE
normalized-fixed-bandwidth-20.cnf.gz-extracted.pb.metafix.opb955.196UNSATISFIABLE
normalized-tseitin-regular-n40-d3-i3-f.cnf.gz-plain.pb.metafix.opb1.56796UNSATISFIABLE
normalized-subsetCardinalitySigma-27-1.cnf.gz-extracted.pb.metafix.opb932.267UNSATISFIABLE
normalized-tseitin-regular-n42-d3-i1-r1.cnf.gz-plain.pb.metafix.opb0.966794UNSATISFIABLE
normalized-tseitin-regular-n82-d3-i3-f.cnf.gz-plain.pb.metafix.opb394.372UNSATISFIABLE
normalized-regular-n23-d4-i3.cnf.gz-extracted.pb.metafix.opb1434.04UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i3-f.cnf.gz-plain.pb.metafix.opb5.14295UNSATISFIABLE
normalized-regular-n29-d4-i2.cnf.gz-extracted.pb.metafix.opb1798.725UNKNOWN
normalized-tseitin-regular-n52-d3-i2-r1.cnf.gz-plain.pb.metafix.opb6.94248UNSATISFIABLE
normalized-fixed-bandwidth-77.cnf.gz-extracted.pb.metafix.opb1798.733UNKNOWN
normalized-tseitin-regular-n44-d3-i2-f.cnf.gz-plain.pb.metafix.opb0.354447UNSATISFIABLE
normalized-subsetCardinalitySigma-27-2.cnf.gz-plain.pb.metafix.opb1798.786UNKNOWN
normalized-regular-n21-d4-i2.cnf.gz-extracted.pb.metafix.opb102.262UNSATISFIABLE
normalized-tseitin-regular-n64-d3-i1-r2.cnf.gz-plain.pb.metafix.opb3.54503UNSATISFIABLE
normalized-tseitin-regular-n64-d3-i2-r2.cnf.gz-plain.pb.metafix.opb4.71033UNSATISFIABLE
normalized-subsetCardinalitySigma-27-2.cnf.gz-extracted.pb.metafix.opb1798.550UNKNOWN
normalized-fixed-bandwidth-73.cnf.gz-extracted.pb.metafix.opb1800.461UNKNOWN
normalized-subsetCardinalitySigma-26-2.cnf.gz-extracted.pb.metafix.opb435.45UNSATISFIABLE
normalized-tseitin-regular-n48-d3-i2-f.cnf.gz-plain.pb.metafix.opb4.61746UNSATISFIABLE
normalized-tseitin-regular-n54-d3-i1-r1.cnf.gz-plain.pb.metafix.opb1.98222UNSATISFIABLE
normalized-subsetCardinalitySigma-26-1.cnf.gz-extracted.pb.metafix.opb1419.76UNSATISFIABLE
normalized-tseitin-regular-n60-d3-i1-r2.cnf.gz-plain.pb.metafix.opb2.98216UNSATISFIABLE
normalized-fixed-bandwidth-62.cnf.gz-extracted.pb.metafix.opb1798.734UNKNOWN
normalized-tseitin-regular-n48-d3-i2-r2.cnf.gz-plain.pb.metafix.opb9.80326UNSATISFIABLE
normalized-regular-n25-d4-i2.cnf.gz-plain.pb.metafix.opb1798.765UNKNOWN
normalized-regular-n25-d4-i3.cnf.gz-plain.pb.metafix.opb1798.775UNKNOWN
normalized-regular-n24-d4-i3.cnf.gz-plain.pb.metafix.opb1798.782UNKNOWN
normalized-regular-n22-d4-i3.cnf.gz-plain.pb.metafix.opb367.671UNSATISFIABLE
normalized-tseitin-regular-n36-d3-i3-r2.cnf.gz-plain.pb.metafix.opb0.579811UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i1-f.cnf.gz-plain.pb.metafix.opb10.078UNSATISFIABLE
normalized-subsetCardinalitySigma-31-1.cnf.gz-extracted.pb.metafix.opb1798.754UNKNOWN
normalized-tseitin-regular-n42-d3-i3-f.cnf.gz-plain.pb.metafix.opb0.379205UNSATISFIABLE
normalized-tseitin-regular-n42-d3-i1-f.cnf.gz-plain.pb.metafix.opb0.964898UNSATISFIABLE
normalized-regular-n19-d4-i1.cnf.gz-extracted.pb.metafix.opb69.7193UNSATISFIABLE
normalized-tseitin-regular-n80-d3-i3-r2.cnf.gz-plain.pb.metafix.opb934.727UNSATISFIABLE
normalized-tseitin-regular-n80-d3-i1-r1.cnf.gz-plain.pb.metafix.opb128.42UNSATISFIABLE
normalized-subsetCardinalitySigma-23-3.cnf.gz-extracted.pb.metafix.opb115.078UNSATISFIABLE
normalized-tseitin-regular-n54-d3-i2-r1.cnf.gz-plain.pb.metafix.opb0.125591UNSATISFIABLE
normalized-tseitin-regular-n94-d3-i1-r1.cnf.gz-plain.pb.metafix.opb1438.88UNSATISFIABLE
normalized-tseitin-regular-n84-d3-i2-f.cnf.gz-plain.pb.metafix.opb918.324UNSATISFIABLE
normalized-regular-n25-d4-i1.cnf.gz-extracted.pb.metafix.opb1635.71UNSATISFIABLE
normalized-tseitin-regular-n68-d3-i3-r2.cnf.gz-plain.pb.metafix.opb58.3361UNSATISFIABLE
normalized-tseitin-regular-n88-d3-i1-r1.cnf.gz-plain.pb.metafix.opb574.608UNSATISFIABLE
normalized-tseitin-regular-n60-d3-i2-r2.cnf.gz-plain.pb.metafix.opb4.75567UNSATISFIABLE
normalized-fixed-bandwidth-93.cnf.gz-extracted.pb.metafix.opb1798.775UNKNOWN
normalized-regular-n23-d4-i1.cnf.gz-extracted.pb.metafix.opb212.201UNSATISFIABLE
normalized-tseitin-regular-n42-d3-i3-r1.cnf.gz-plain.pb.metafix.opb0.283985UNSATISFIABLE
normalized-tseitin-regular-n52-d3-i2-f.cnf.gz-plain.pb.metafix.opb10.3675UNSATISFIABLE
normalized-regular-n17-d4-i1.cnf.gz-plain.pb.metafix.opb15.8221UNSATISFIABLE
normalized-tseitin-regular-n38-d3-i3-r1.cnf.gz-plain.pb.metafix.opb0.440535UNSATISFIABLE
normalized-fixed-bandwidth-18.cnf.gz-plain.pb.metafix.opb329.988UNSATISFIABLE
normalized-fixed-bandwidth-78.cnf.gz-extracted.pb.metafix.opb1798.757UNKNOWN
normalized-tseitin-regular-n96-d3-i3-f.cnf.gz-plain.pb.metafix.opb1798.810UNKNOWN
normalized-fixed-bandwidth-90.cnf.gz-extracted.pb.metafix.opb1798.737UNKNOWN
normalized-subsetCardinalitySigma-25-2.cnf.gz-plain.pb.metafix.opb612.188UNSATISFIABLE
normalized-tseitin-regular-n44-d3-i3-f.cnf.gz-plain.pb.metafix.opb0.829044UNSATISFIABLE
normalized-tseitin-regular-n62-d3-i3-r1.cnf.gz-plain.pb.metafix.opb11.4078UNSATISFIABLE
normalized-tseitin-regular-n78-d3-i1-r1.cnf.gz-plain.pb.metafix.opb122.324UNSATISFIABLE
normalized-regular-n24-d4-i2.cnf.gz-extracted.pb.metafix.opb841.994UNSATISFIABLE
normalized-regular-n27-d4-i2.cnf.gz-extracted.pb.metafix.opb1798.774UNKNOWN
normalized-tseitin-regular-n58-d3-i3-r2.cnf.gz-plain.pb.metafix.opb4.9592UNSATISFIABLE
normalized-regular-n20-d4-i1.cnf.gz-plain.pb.metafix.opb22.7429UNSATISFIABLE
normalized-tseitin-regular-n42-d3-i2-f.cnf.gz-plain.pb.metafix.opb0.180686UNSATISFIABLE
normalized-tseitin-regular-n40-d3-i1-f.cnf.gz-plain.pb.metafix.opb0.224746UNSATISFIABLE
normalized-tseitin-regular-n40-d3-i3-r1.cnf.gz-plain.pb.metafix.opb1.97784UNSATISFIABLE
normalized-regular-n22-d4-i3.cnf.gz-extracted.pb.metafix.opb933.232UNSATISFIABLE
normalized-subsetCardinalitySigma-28-2.cnf.gz-extracted.pb.metafix.opb895.177UNSATISFIABLE
normalized-tseitin-regular-n48-d3-i1-r2.cnf.gz-plain.pb.metafix.opb0.726273UNSATISFIABLE
normalized-tseitin-regular-n70-d3-i2-f.cnf.gz-plain.pb.metafix.opb25.3942UNSATISFIABLE
normalized-fixed-bandwidth-24.cnf.gz-extracted.pb.metafix.opb1798.752UNKNOWN
normalized-subsetCardinalitySigma-26-3.cnf.gz-extracted.pb.metafix.opb426.724UNSATISFIABLE
normalized-regular-n24-d4-i2.cnf.gz-plain.pb.metafix.opb837.127UNSATISFIABLE
normalized-tseitin-regular-n38-d3-i2-r1.cnf.gz-plain.pb.metafix.opb0.43819UNSATISFIABLE
normalized-subsetCardinalitySigma-26-2.cnf.gz-plain.pb.metafix.opb370.765UNSATISFIABLE
normalized-tseitin-regular-n46-d3-i3-r2.cnf.gz-plain.pb.metafix.opb0.806019UNSATISFIABLE
normalized-tseitin-regular-n46-d3-i2-r2.cnf.gz-plain.pb.metafix.opb1.29223UNSATISFIABLE
normalized-tseitin-regular-n60-d3-i3-r1.cnf.gz-plain.pb.metafix.opb16.7667UNSATISFIABLE
normalized-fixed-bandwidth-25.cnf.gz-extracted.pb.metafix.opb1798.794UNKNOWN
normalized-tseitin-regular-n92-d3-i1-r2.cnf.gz-plain.pb.metafix.opb650.467UNSATISFIABLE
normalized-regular-n28-d4-i3.cnf.gz-plain.pb.metafix.opb1769.86UNSATISFIABLE
normalized-fixed-bandwidth-15.cnf.gz-plain.pb.metafix.opb37.6879UNSATISFIABLE
normalized-subsetCardinalitySigma-27-3.cnf.gz-plain.pb.metafix.opb461.548UNSATISFIABLE
normalized-129.opb1798.657UNKNOWN
normalized-41.opb383.181SATISFIABLE
normalized-130.opb1798.664UNKNOWN
normalized-137.opb1798.628UNKNOWN
normalized-185.opb1419.68SATISFIABLE
normalized-20.opb1798.643UNKNOWN
normalized-112.opb1798.727UNKNOWN
normalized-24.opb1798.665UNKNOWN
normalized-37.opb1798.687UNKNOWN
normalized-70.opb1798.647UNKNOWN
normalized-154.opb1798.667UNKNOWN
normalized-178.opb1800.458UNKNOWN
normalized-40.opb1798.651UNKNOWN
normalized-141.opb1798.712UNKNOWN
normalized-173.opb1798.548UNKNOWN
normalized-117.opb70.444SATISFIABLE
normalized-175.opb1798.582UNKNOWN
normalized-73.opb1800.430UNKNOWN
normalized-164.opb990.322SATISFIABLE
normalized-89.opb1798.667UNKNOWN
normalized-146.opb1798.674UNKNOWN
normalized-123.opb1798.710UNKNOWN
normalized-05.opb1798.665UNKNOWN
normalized-147.opb1798.680UNKNOWN
normalized-48.opb1177.6SATISFIABLE
normalized-47.opb1798.637UNKNOWN
normalized-21.opb1798.697UNKNOWN
normalized-172.opb1798.542UNKNOWN
normalized-60.opb1798.692UNKNOWN
normalized-91.opb1798.636UNKNOWN
normalized-188.opb3.37017UNSATISFIABLE
normalized-53.opb1798.630UNKNOWN
normalized-122.opb1800.437UNKNOWN
normalized-107.opb105.115SATISFIABLE
normalized-99.opb1011.11UNSATISFIABLE
normalized-153.opb1798.658UNKNOWN
normalized-27.opb1798.593UNKNOWN
normalized-116.opb1798.654UNKNOWN
normalized-167.opb1798.633UNKNOWN
normalized-101.opb1798.686UNKNOWN
normalized-61.opb1798.627UNKNOWN
normalized-184.opb1798.347UNKNOWN
normalized-135.opb1798.652UNKNOWN
normalized-170.opb687.528SATISFIABLE
normalized-76.opb1798.687UNKNOWN
normalized-162.opb222.314SATISFIABLE
normalized-181.opb1798.482UNKNOWN
normalized-120.opb1798.682UNKNOWN
normalized-180.opb1798.539UNKNOWN
normalized-31.opb1798.660UNKNOWN
normalized-182.opb1798.375UNKNOWN
normalized-j3017_6-sat.opb0.048026SATISFIABLE
normalized-j3030_6-sat.opb0.863582SATISFIABLE
normalized-j3048_8-sat.opb0.282908SATISFIABLE
normalized-j3025_7-sat.opb0.386869SATISFIABLE
normalized-j308_1-unsat.opb0.056994UNSATISFIABLE
normalized-j3029_8-unsat.opb31.8707UNSATISFIABLE
normalized-j3024_3-sat.opb0.130905SATISFIABLE
normalized-j3027_8-sat.opb0.191747SATISFIABLE
normalized-j307_10-sat.opb0.098391SATISFIABLE
normalized-j3029_6-sat.opb18.073SATISFIABLE
normalized-j307_9-unsat.opb0.075027UNSATISFIABLE
normalized-j3024_5-sat.opb0.09211SATISFIABLE
normalized-j3024_4-sat.opb0.098789SATISFIABLE
normalized-j308_6-unsat.opb0.064623UNSATISFIABLE
normalized-j3041_4-unsat.opb0.451157UNSATISFIABLE
normalized-j301_4-unsat.opb0.040685UNSATISFIABLE
normalized-j3031_7-sat.opb0.313709SATISFIABLE
normalized-j3037_5-sat.opb0.146053SATISFIABLE
normalized-j309_10-unsat.opb0.997043UNSATISFIABLE
normalized-j309_6-sat.opb0.312988SATISFIABLE
normalized-j3046_4-unsat.opb0.29829UNSATISFIABLE
normalized-j3025_1-sat.opb0.804118SATISFIABLE
normalized-j3024_2-sat.opb0.119179SATISFIABLE
normalized-j309_9-sat.opb0.511683SATISFIABLE
normalized-j308_6-sat.opb0.102313SATISFIABLE
normalized-j3025_10-sat.opb0.197562SATISFIABLE
normalized-j3043_8-sat.opb0.224283SATISFIABLE
normalized-j3042_5-unsat.opb0.10485UNSATISFIABLE
normalized-j3011_9-unsat.opb0.131106UNSATISFIABLE
normalized-j3020_1-sat.opb0.053484SATISFIABLE
normalized-j605_7-sat.opb1.30688SATISFIABLE
normalized-j605_1-unsat.opb10.928UNSATISFIABLE
normalized-j607_4-unsat.opb0.264212UNSATISFIABLE
normalized-j605_10-unsat.opb29.9268UNSATISFIABLE
normalized-j6027_4-unsat.opb0.53576UNSATISFIABLE
normalized-j6010_7-unsat.opb0.49752UNSATISFIABLE
normalized-j606_1-unsat.opb0.211149UNSATISFIABLE
normalized-j6041_4-sat.opb7.03542SATISFIABLE
normalized-j6040_1-sat.opb0.630513SATISFIABLE
normalized-j6030_9-unsat.opb0.945498UNSATISFIABLE
normalized-j6048_4-sat.opb1.5703SATISFIABLE
normalized-j6029_8-unsat.opb1798.549UNKNOWN
normalized-j6027_9-unsat.opb0.624796UNSATISFIABLE
normalized-j6020_9-sat.opb0.16509SATISFIABLE
normalized-j6028_7-sat.opb1.60624SATISFIABLE
normalized-j6014_2-sat.opb2.70698SATISFIABLE
normalized-j602_7-unsat.opb0.097295UNSATISFIABLE
normalized-j6040_10-sat.opb0.525763SATISFIABLE
normalized-j6030_8-sat.opb2.22431SATISFIABLE
normalized-j6022_1-sat.opb0.374355SATISFIABLE
normalized-j6013_2-unsat.opb1798.632UNKNOWN
normalized-j6015_4-sat.opb2.36644SATISFIABLE
normalized-j601_8-unsat.opb0.103912UNSATISFIABLE
normalized-j6018_3-sat.opb0.15443SATISFIABLE
normalized-j6016_10-unsat.opb1.20223UNSATISFIABLE
normalized-j6032_1-unsat.opb1.43746UNSATISFIABLE
normalized-j6033_2-unsat.opb0.12555UNSATISFIABLE
normalized-j603_2-unsat.opb0.103308UNSATISFIABLE
normalized-j6028_9-unsat.opb0.774301UNSATISFIABLE
normalized-j6010_2-unsat.opb0.518414UNSATISFIABLE
normalized-j6035_10-sat.opb0.160802SATISFIABLE
normalized-j6040_3-sat.opb0.572866SATISFIABLE
normalized-j6043_4-sat.opb1.07234SATISFIABLE
normalized-j6042_2-sat.opb0.793927SATISFIABLE
normalized-j12049_6-unsat.opb1.08552UNSATISFIABLE
normalized-j12041_4-unsat.opb2.66046UNSATISFIABLE
normalized-j12056_10-unsat.opb1798.590UNKNOWN
normalized-j12023_3-unsat.opb0.343283UNSATISFIABLE
normalized-j12038_8-unsat.opb1798.500UNKNOWN
normalized-j12034_4-sat.opb5.51194SATISFIABLE
normalized-j1208_6-sat.opb1501.37SATISFIABLE
normalized-j12058_4-sat.opb1798.529UNKNOWN
normalized-j12032_3-unsat.opb1798.594UNKNOWN
normalized-j1204_7-sat.opb0.55676SATISFIABLE
normalized-j1209_4-sat.opb98.875SATISFIABLE
normalized-j12047_6-sat.opb1798.586UNKNOWN
normalized-j12035_4-sat.opb4.98545SATISFIABLE
normalized-j12046_2-sat.opb1798.576UNKNOWN
normalized-j12027_7-unsat.opb14.2555UNSATISFIABLE
normalized-j12033_3-sat.opb1798.595UNKNOWN
normalized-j12022_9-sat.opb0.588862SATISFIABLE
normalized-j12059_3-unsat.opb3.49761UNSATISFIABLE
normalized-j1208_10-unsat.opb1798.561UNKNOWN
normalized-j12038_7-unsat.opb1798.516UNKNOWN
normalized-j1203_2-sat.opb0.464824SATISFIABLE
normalized-j12036_4-sat.opb1798.601UNKNOWN
normalized-j12038_3-sat.opb1798.553UNKNOWN
normalized-j12010_10-sat.opb1.97567SATISFIABLE
normalized-j12016_4-sat.opb1798.623UNKNOWN
normalized-j12037_7-sat.opb1798.536UNKNOWN
normalized-j1205_1-unsat.opb0.356156UNSATISFIABLE
normalized-j12048_4-unsat.opb1800.448UNKNOWN
normalized-j12015_3-unsat.opb2.01395UNSATISFIABLE
normalized-j12045_10-sat.opb0.559113SATISFIABLE
normalized-j1201_5-sat.opb1.08709SATISFIABLE
normalized-j12026_5-unsat.opb431.057UNSATISFIABLE
normalized-j12032_8-unsat.opb1798.601UNKNOWN
normalized-j1206_8-unsat.opb255.469UNSATISFIABLE
normalized-j1206_6-sat.opb1798.637UNKNOWN
normalized-j12039_7-sat.opb1798.523UNKNOWN
normalized-j1205_3-unsat.opb0.303876UNSATISFIABLE
normalized-j12021_4-sat.opb3.09785SATISFIABLE
normalized-j12052_5-unsat.opb1798.632UNKNOWN
normalized-j12036_3-sat.opb1798.608UNKNOWN
normalized-j12028_8-sat.opb1115.44SATISFIABLE
normalized-j12013_1-unsat.opb1.85211UNSATISFIABLE
normalized-j12047_10-unsat.opb1798.638UNKNOWN
normalized-j9015_10-unsat.opb2.28811UNSATISFIABLE
normalized-j9040_1-unsat.opb0.817201UNSATISFIABLE
normalized-j9010_8-sat.opb2.55756SATISFIABLE
normalized-j9010_10-unsat.opb1.09668UNSATISFIABLE
normalized-j9015_7-unsat.opb2.50952UNSATISFIABLE
normalized-j9043_2-sat.opb2.29364SATISFIABLE
normalized-j901_6-sat.opb0.321089SATISFIABLE
normalized-j9042_4-sat.opb2.5225SATISFIABLE
normalized-j907_8-unsat.opb0.66645UNSATISFIABLE
normalized-j9045_1-sat.opb1798.573UNKNOWN
normalized-j9048_1-unsat.opb3.51045UNSATISFIABLE
normalized-j9012_5-sat.opb4.02847SATISFIABLE
normalized-j9028_2-unsat.opb1.87794UNSATISFIABLE
normalized-j9039_3-unsat.opb0.711623UNSATISFIABLE
normalized-j905_6-unsat.opb6.39282UNSATISFIABLE
normalized-j9035_5-sat.opb0.407079SATISFIABLE
normalized-j9042_5-sat.opb2.64532SATISFIABLE
normalized-j906_2-sat.opb1.15701SATISFIABLE
normalized-j9016_7-sat.opb4.79174SATISFIABLE
normalized-j9012_2-unsat.opb2.01214UNSATISFIABLE
normalized-j9048_9-sat.opb4.8499SATISFIABLE
normalized-j903_10-unsat.opb0.191651UNSATISFIABLE
normalized-j9010_6-unsat.opb1.31872UNSATISFIABLE
normalized-j9014_1-unsat.opb2.135UNSATISFIABLE
normalized-j902_5-sat.opb0.38599SATISFIABLE
normalized-j9038_3-unsat.opb0.872743UNSATISFIABLE
normalized-j9027_5-sat.opb3.72974SATISFIABLE
normalized-j908_8-unsat.opb0.883422UNSATISFIABLE
normalized-j9035_1-unsat.opb0.279262UNSATISFIABLE
normalized-j9040_1-sat.opb1.37294SATISFIABLE
normalized-1096.cudf.paranoid.opb0.00083SATISFIABLE
normalized-NG_K131.opb1798.710UNKNOWN
normalized-NG_K132.opb1798.731UNKNOWN
normalized-NG_K152.opb1798.720UNKNOWN
normalized-NG_K129.opb1798.715UNKNOWN
normalized-NG_K143.opb1798.718UNKNOWN
normalized-NG_K168.opb1798.741UNKNOWN
normalized-NG_K183.opb1798.706UNKNOWN
normalized-NG_K200.opb1798.693UNKNOWN
normalized-NG_K125.opb1798.732UNKNOWN
normalized-NG_K167.opb1798.698UNKNOWN
normalized-NG_K156.opb1798.723UNKNOWN
normalized-NG_K139.opb1798.698UNKNOWN
normalized-NG_K175.opb1798.706UNKNOWN
normalized-NG_K160.opb1798.711UNKNOWN
normalized-NG_K196.opb1798.696UNKNOWN
normalized-NG_K192.opb1798.688UNKNOWN
normalized-NG_K126.opb1798.720UNKNOWN
normalized-NG_K164.opb1798.709UNKNOWN
normalized-NG_K128.opb1798.691UNKNOWN
normalized-NG_K140.opb1798.711UNKNOWN
normalized-NG_K176.opb1798.715UNKNOWN
normalized-NG_K199.opb1798.710UNKNOWN
normalized-NG_K138.opb1798.724UNKNOWN
normalized-NG_K180.opb1798.738UNKNOWN
normalized-NG_K163.opb1798.671UNKNOWN
normalized-NG_K148.opb1798.703UNKNOWN
normalized-NG_K141.opb1798.715UNKNOWN
normalized-NG_K181.opb1800.456UNKNOWN
normalized-NG_K133.opb1800.275UNKNOWN
normalized-NG_K177.opb1798.681UNKNOWN
normalized-BeauxArts_K75.opb44.345SATISFIABLE
normalized-BeauxArts_K73.opb123.889SATISFIABLE
normalized-BeauxArts_K80.opb33.0458SATISFIABLE
normalized-BeauxArts_K70.opb171.899SATISFIABLE
normalized-BeauxArts_K68.opb710.714SATISFIABLE
normalized-BeauxArts_K69.opb198.924SATISFIABLE
normalized-BeauxArts_K72.opb55.9807SATISFIABLE
normalized-BeauxArts_K77.opb47.0544SATISFIABLE
normalized-BeauxArts_K66.opb1798.751UNKNOWN
normalized-BeauxArts_K65.opb1798.722UNKNOWN
normalized-BeauxArts_K67.opb72.4757SATISFIABLE
normalized-BeauxArts_K76.opb31.2581SATISFIABLE
normalized-BeauxArts_K78.opb10.3198SATISFIABLE
normalized-BeauxArts_K74.opb101.463SATISFIABLE
normalized-BeauxArts_K71.opb56.4357SATISFIABLE
normalized-BeauxArts_K79.opb8.77256SATISFIABLE
normalized-TateBritain_K104.opb1798.733UNKNOWN
normalized-TateBritain_K84.opb1798.739UNKNOWN
normalized-TateBritain_K86.opb1798.742UNKNOWN
normalized-TateBritain_K102.opb1798.766UNKNOWN
normalized-TateBritain_K98.opb1798.760UNKNOWN
normalized-TateBritain_K97.opb1798.649UNKNOWN
normalized-TateBritain_K93.opb1798.573UNKNOWN
normalized-TateBritain_K94.opb1798.760UNKNOWN
normalized-TateBritain_K87.opb1798.754UNKNOWN
normalized-TateBritain_K85.opb1798.758UNKNOWN
normalized-TateBritain_K83.opb1800.518UNKNOWN
normalized-TateBritain_K101.opb1309.01SATISFIABLE
normalized-TateBritain_K96.opb1798.781UNKNOWN
normalized-TateBritain_K95.opb1798.703UNKNOWN
normalized-TateBritain_K99.opb1798.734UNKNOWN
normalized-TateBritain_K107.opb1798.784UNKNOWN
normalized-TateBritain_K108.opb1798.715UNKNOWN
normalized-TateBritain_K80.opb1798.750UNKNOWN
normalized-TateBritain_K82.opb1798.686UNKNOWN
normalized-TateBritain_K109.opb597.682SATISFIABLE
normalized-TateBritain_K81.opb1798.746UNKNOWN
normalized-TateBritain_K88.opb1798.749UNKNOWN
normalized-TateBritain_K103.opb1798.747UNKNOWN
normalized-TateBritain_K89.opb1798.724UNKNOWN
normalized-TateBritain_K106.opb1798.725UNKNOWN
normalized-TateBritain_K90.opb1798.707UNKNOWN
normalized-TateBritain_K105.opb1798.763UNKNOWN
normalized-TateBritain_K91.opb1798.708UNKNOWN
normalized-TateBritain_K100.opb1798.753UNKNOWN
normalized-TateBritain_K92.opb1798.756UNKNOWN
normalized-neos-849702.opb410.644SATISFIABLE
normalized-neos808444.opb1.66116SATISFIABLE
normalized-neos-820157.opb1798.748UNKNOWN
normalized-neos-820146.opb1798.761UNKNOWN
normalized-fpga14_12_sat_pb.cnf.cr.opb0.019628SATISFIABLE
normalized-chnl10_20_pb.cnf.cr.opb9.44571UNSATISFIABLE
normalized-fpga30_29_sat_pb.cnf.cr.opb0.062348SATISFIABLE
normalized-fpga15_13_sat_pb.cnf.cr.opb0.021504SATISFIABLE
normalized-fpga25_25_sat_pb.cnf.cr.opb0.13941SATISFIABLE
normalized-fpga11_10_sat_pb.cnf.cr.opb0.014803SATISFIABLE
normalized-chnl15_20_pb.cnf.cr.opb1798.738UNKNOWN
normalized-fpga13_13_sat_pb.cnf.cr.opb0.026923SATISFIABLE
normalized-fpga11_9_sat_pb.cnf.cr.opb0.013992SATISFIABLE
normalized-fpga35_33_sat_pb.cnf.cr.opb0.289315SATISFIABLE
normalized-fpga10_10_sat_pb.cnf.cr.opb0.010956SATISFIABLE
normalized-chnl30_35_pb.cnf.cr.opb1800.463UNKNOWN
normalized-chnl15_25_pb.cnf.cr.opb1798.736UNKNOWN
normalized-fpga35_35_sat_pb.cnf.cr.opb0.121109SATISFIABLE
normalized-chnl20_21_pb.cnf.cr.opb1798.742UNKNOWN
normalized-chnl30_40_pb.cnf.cr.opb1798.751UNKNOWN
normalized-fpga45_43_sat_pb.cnf.cr.opb0.387527SATISFIABLE
normalized-chnl10_11_pb.cnf.cr.opb172.005UNSATISFIABLE
normalized-fpga14_13_sat_pb.cnf.cr.opb0.021266SATISFIABLE
normalized-fpga10_8_sat_pb.cnf.cr.opb0.018855SATISFIABLE
normalized-fpga15_14_sat_pb.cnf.cr.opb0.039727SATISFIABLE
normalized-fpga30_28_sat_pb.cnf.cr.opb0.075149SATISFIABLE
normalized-fpga30_30_sat_pb.cnf.cr.opb0.176369SATISFIABLE
normalized-chnl40_50_pb.cnf.cr.opb1798.604UNKNOWN
normalized-fpga40_39_sat_pb.cnf.cr.opb0.398925SATISFIABLE
normalized-chnl50_55_pb.cnf.cr.opb1798.742UNKNOWN
normalized-chnl10_15_pb.cnf.cr.opb22.8498UNSATISFIABLE
normalized-fpga12_10_sat_pb.cnf.cr.opb0.009818SATISFIABLE
normalized-chnl20_30_pb.cnf.cr.opb1798.748UNKNOWN
normalized-chnl35_36_pb.cnf.cr.opb1798.748UNKNOWN
normalized-fpga45_45_sat_pb.cnf.cr.opb0.598885SATISFIABLE
normalized-fpga20_20_sat_pb.cnf.cr.opb0.032904SATISFIABLE
normalized-fpga15_15_sat_pb.cnf.cr.opb0.048891SATISFIABLE
normalized-fpga13_11_sat_pb.cnf.cr.opb0.015821SATISFIABLE
normalized-fpga20_18_sat_pb.cnf.cr.opb0.046481SATISFIABLE
normalized-fpga12_11_sat_pb.cnf.cr.opb0.014478SATISFIABLE
normalized-chnl40_41_pb.cnf.cr.opb1798.740UNKNOWN
normalized-fpga45_44_sat_pb.cnf.cr.opb0.27602SATISFIABLE
normalized-chnl30_31_pb.cnf.cr.opb1798.746UNKNOWN
normalized-chnl20_25_pb.cnf.cr.opb1798.672UNKNOWN
normalized-chnl50_60_pb.cnf.cr.opb1798.634UNKNOWN
normalized-fpga25_24_sat_pb.cnf.cr.opb0.712386SATISFIABLE
normalized-fpga12_12_sat_pb.cnf.cr.opb0.015348SATISFIABLE
normalized-fpga25_23_sat_pb.cnf.cr.opb0.114201SATISFIABLE
normalized-chnl35_40_pb.cnf.cr.opb1798.605UNKNOWN
normalized-chnl15_16_pb.cnf.cr.opb1798.706UNKNOWN
normalized-fpga10_9_sat_pb.cnf.cr.opb0.020759SATISFIABLE
normalized-chnl35_45_pb.cnf.cr.opb1798.761UNKNOWN
normalized-fpga13_12_sat_pb.cnf.cr.opb0.019022SATISFIABLE
normalized-fpga35_34_sat_pb.cnf.cr.opb0.098469SATISFIABLE
normalized-fpga40_38_sat_pb.cnf.cr.opb0.243906SATISFIABLE
normalized-chnl50_51_pb.cnf.cr.opb1798.745UNKNOWN
normalized-fpga11_11_sat_pb.cnf.cr.opb0.022111SATISFIABLE
normalized-fpga40_40_sat_pb.cnf.cr.opb0.344437SATISFIABLE
normalized-fpga20_19_sat_pb.cnf.cr.opb0.02999SATISFIABLE
normalized-chnl40_45_pb.cnf.cr.opb1798.787UNKNOWN
normalized-fpga14_14_sat_pb.cnf.cr.opb0.172366SATISFIABLE
normalized-ppp:1,3-13,19.opb37.2329SATISFIABLE
normalized-ppp:1-11,19,21.opb1798.736UNKNOWN
normalized-ppp:1-12,16.opb0.254777SATISFIABLE
normalized-ppp:1-13.opb2.85147SATISFIABLE
normalized-ppp:3-13,25,26.opb1798.653UNKNOWN
normalized-ppp:1-9,16-19.opb1798.752UNKNOWN
normalized-cache-ibm-q-unbounded.Ih1arity.ucl.opb534.75UNSATISFIABLE
normalized-ooo.ex.mem.LdValue.ucl.opb299.89UNSATISFIABLE
normalized-46s.smv.opb0.119027UNSATISFIABLE
normalized-ooo.rf6.ucl.opb0.057962UNSATISFIABLE
normalized-ooo.tag12.ucl.opb14.0722UNSATISFIABLE
normalized-elf.rf7.ucl.opb0.033607UNSATISFIABLE
normalized-25s.smv.opb0.222785UNSATISFIABLE
normalized-ooo.ex.br.mem.Src1Valid_Src1ValidBar.ucl.opb374.375UNSATISFIABLE
normalized-cache.inv12.ucl.opb12.2358UNSATISFIABLE
normalized-dlx1c.rwmem.ucl.opb0.779962UNSATISFIABLE
normalized-ooo.burch_dill.3.accl.ucl.opb6.08327UNSATISFIABLE
normalized-elf.rf10.ucl.opb5.06762UNSATISFIABLE
normalized-ooo.unbounded.all.ucl.opb281.811UNSATISFIABLE
normalized-44s.smv.opb0.048738UNSATISFIABLE
normalized-ooo.ex.br.mem.RobRegValid_bar.ucl.opb36.1868UNSATISFIABLE
normalized-ooo.rf8.ucl.opb0.794307UNSATISFIABLE
normalized-ooo.burch_dill.6.accl.ucl.opb1798.707UNKNOWN
normalized-blast-floppy1-8.ucl.opb0.127949UNSATISFIABLE
normalized-blast-floppy1-6.ucl.opb0.115536UNSATISFIABLE
normalized-cache-ibm-q-full.all.ucl.opb638.27UNSATISFIABLE
normalized-ooo.tag8.ucl.opb0.798964UNSATISFIABLE
normalized-cache.inv10.ucl.opb0.083883UNSATISFIABLE
normalized-cache-ibm-q-unbounded.Ic22arity.ucl.opb18.9649UNSATISFIABLE
normalized-22s.smv.opb0.325285UNSATISFIABLE
normalized-cache-ibm-q-unbounded.Ih2arity.ucl.opb1.35851SATISFIABLE
normalized-dlx1c.rwmem1.ucl.opb0.691607UNSATISFIABLE
normalized-elf.rf9.ucl.opb0.6587UNSATISFIABLE
normalized-ooo.rf10.ucl.opb14.3122UNSATISFIABLE
normalized-cache.inv8.ucl.opb0.027593UNSATISFIABLE
normalized-ooo.burch_dill.4.accl.ucl.opb0.2365UNSATISFIABLE
normalized-ooo.burch_dill.2.accl.ucl.opb1.87888UNSATISFIABLE
normalized-cache-ibm-q-unbounded.Icl2arity.ucl.opb1.51723UNSATISFIABLE
normalized-ooo.ex.mem.LsqHdStrong.ucl.opb1065.98UNSATISFIABLE
normalized-elf.rf8.ucl.opb0.138068UNSATISFIABLE
normalized-elf.rf6.ucl.opb0.002164UNSATISFIABLE
normalized-ooo.rf7.ucl.opb0.162902UNSATISFIABLE
normalized-ooo.tag10.ucl.opb4.52291UNSATISFIABLE
normalized-43s.smv.opb0.551641UNSATISFIABLE
normalized-ooo.burch_dill.8.accl.ucl.opb390.694UNSATISFIABLE
normalized-dlx1c.ucl.opb0.294722UNSATISFIABLE
normalized-ooo.rf9.ucl.opb2.34783UNSATISFIABLE
normalized-blast-floppy1-3.ucl.opb0.008707UNSATISFIABLE
normalized-blast-floppy1-7.ucl.opb0.116516UNSATISFIABLE
normalized-blast-floppy1-2.ucl.opb0.026042UNSATISFIABLE
normalized-ooo.tag14.ucl.opb60.8003UNSATISFIABLE
normalized-blast-floppy1-4.ucl.opb0.004608UNSATISFIABLE
normalized-cache.inv14.ucl.opb1085.96UNSATISFIABLE
normalized-blast-tlan3.ucl.opb0.406604UNSATISFIABLE
normalized-37s.smv.opb0.059139UNSATISFIABLE
normalized-blast-tlan2.ucl.opb0.075923UNSATISFIABLE
normalized-reduced-prob2.opb1.28261SATISFIABLE
normalized-reduced-prob3.opb8.97472SATISFIABLE
normalized-reduced-prob5.opb1.49604SATISFIABLE
normalized-reduced-cuww2.opb1.82286SATISFIABLE
normalized-reduced-prob8.opb11.1116SATISFIABLE
normalized-reduced-prob6.opb1.74289SATISFIABLE
normalized-reduced-prob4.opb1.27194SATISFIABLE
normalized-reduced-prob7.opb4.67351SATISFIABLE
normalized-reduced-cuww1.opb11.6928SATISFIABLE
normalized-reduced-cuww3.opb490.202SATISFIABLE
normalized-reduced-prob10.opb1.46391SATISFIABLE
normalized-reduced-cuww5.opbUNKNOWN
normalized-reduced-prob1.opb1.95786SATISFIABLE
normalized-reduced-cuww4.opb11.8969SATISFIABLE
normalized-dbst_v30_e350_d15_mw10_2.opb.PB06.opb3.07613SATISFIABLE
normalized-dbst_v50_e1000_d25_mw10_5.opb.PB06.opb40.3817SATISFIABLE
normalized-dbst_v40_e600_d20_mw10_9.opb.PB06.opb10.2114SATISFIABLE
normalized-dbst_v40_e600_d20_mw10_6.opb.PB06.opb9.47951SATISFIABLE
normalized-dbst_v50_e1000_d25_mw10_1.opb.PB06.opb22.2SATISFIABLE
normalized-dbst_v40_e600_d20_mw10_0.opb.PB06.opb8.80961SATISFIABLE
normalized-dbst_v30_e350_d15_mw10_8.opb.PB06.opb3.33397SATISFIABLE
normalized-dbst_v30_e350_d15_mw10_3.opb.PB06.opb3.45612SATISFIABLE
normalized-dbst_v40_e600_d20_mw10_5.opb.PB06.opb9.31875SATISFIABLE
normalized-dbst_v50_e1000_d25_mw10_3.opb.PB06.opb35.0218SATISFIABLE
normalized-dbst_v30_e350_d15_mw10_9.opb.PB06.opb3.25199SATISFIABLE
normalized-dbst_v30_e350_d15_mw10_1.opb.PB06.opb3.09975SATISFIABLE
normalized-dbst_v50_e1000_d25_mw10_9.opb.PB06.opb25.0612SATISFIABLE
normalized-dbst_v50_e1000_d25_mw10_6.opb.PB06.opb28.008SATISFIABLE
normalized-dbst_v40_e600_d20_mw10_2.opb.PB06.opb8.33812SATISFIABLE
normalized-vdw_k4_l4_n360.opb1798.705UNKNOWN
normalized-vdw_k5_l4_n750.opb1798.711UNKNOWN
normalized-vdw_k3_l6_n1500.opb2.62485SATISFIABLE
normalized-vdw_k3_l5_n550.opb706.262SATISFIABLE
normalized-vdw_k6_l3_n170.opb1798.734UNKNOWN
normalized-pigeon-cardinality-41-40.opb1798.711UNKNOWN
normalized-pigeon-cardinality-55-50.opb1800.463UNKNOWN
normalized-pigeon-cardinality-45-40.opb1798.765UNKNOWN
normalized-pigeon-cardinality-11-10.opb222.035UNSATISFIABLE
normalized-pigeon-cardinality-95-90.opb1798.724UNKNOWN
normalized-pigeon-cardinality-61-60.opb1798.649UNKNOWN
normalized-pigeon-cardinality-51-50.opb1798.751UNKNOWN
normalized-pigeon-cardinality-65-60.opb1798.608UNKNOWN
normalized-pigeon-cardinality-31-30.opb1798.741UNKNOWN
normalized-pigeon-cardinality-91-90.opb1798.725UNKNOWN
normalized-pigeon-cardinality-15-10.opb47.0763UNSATISFIABLE
normalized-pigeon-cardinality-21-20.opb1798.773UNKNOWN
normalized-pigeon-cardinality-75-70.opb1798.553UNKNOWN
normalized-pigeon-cardinality-85-80.opb1798.740UNKNOWN
normalized-pigeon-cardinality-25-20.opb1798.736UNKNOWN
normalized-pigeon-cardinality-81-80.opb1798.631UNKNOWN
normalized-pigeon-cardinality-71-70.opb1798.730UNKNOWN
normalized-pigeon-cardinality-101-100.opb1798.605UNKNOWN
normalized-pigeon-cardinality-105-100.opb1798.749UNKNOWN
normalized-pigeon-cardinality-35-30.opb1798.786UNKNOWN
normalized-army11.17bt.opb4.46871SATISFIABLE
normalized-army10.14ls.opb67.5453SATISFIABLE
normalized-army11.17ls.opb185.516SATISFIABLE
normalized-army12.21bt.opb1798.579UNKNOWN
normalized-army9.12bt.opb209.49SATISFIABLE
normalized-army9.12ls.opb19.9688SATISFIABLE
normalized-army13.24ls.opb1798.606UNKNOWN
normalized-army8.9bt.opb1.55658SATISFIABLE
normalized-army10.14bt.opb131.961SATISFIABLE
normalized-army12.21ls.opb1798.754UNKNOWN
normalized-army13.24bt.opb1798.596UNKNOWN
normalized-army8.9ls.opb2.6272SATISFIABLE
normalized-robin14.opb1798.710UNKNOWN
normalized-robin12.opb587.709SATISFIABLE
normalized-robin16.opb1798.674UNKNOWN
normalized-robin8.opb0.224741SATISFIABLE
normalized-robin18.opb1798.692UNKNOWN
normalized-robin10.opb0.571878SATISFIABLE
normalized-t3002.11tsp11.1900561384.opb0.494624SATISFIABLE
normalized-t3002.11tsp11.1900581320.opb543.106UNSATISFIABLE
normalized-t3002.11tsp11.1900567985.opb1179.74UNSATISFIABLE
normalized-t3002.11tsp11.1900562192.opb227.178UNSATISFIABLE
normalized-t3002.11tsp11.1900565527.opb11.0336SATISFIABLE
normalized-t3002.11tsp11.1900576918.opb0.446285SATISFIABLE
normalized-t3002.11tsp11.1900574864.opb265.655UNSATISFIABLE
normalized-t3002.11tsp11.1900547416.opb1.55583SATISFIABLE
normalized-t3002.11tsp11.1900582376.opb0.513037SATISFIABLE
normalized-t3002.11tsp11.1900574974.opb0.137793SATISFIABLE
normalized-t3002.11tsp11.1900550006.opb899.463UNSATISFIABLE
normalized-t3002.11tsp11.1900576360.opb183.01UNSATISFIABLE
normalized-t3002.11tsp11.1900553812.opb108.405UNSATISFIABLE
normalized-t3002.11tsp11.1900584219.opb366.056UNSATISFIABLE
normalized-t3002.11tsp11.1900549974.opb2.85116SATISFIABLE
normalized-t3002.11tsp11.1900554154.opb1.05995SATISFIABLE
normalized-t3002.11tsp11.1900567003.opb1.19068SATISFIABLE
normalized-t3002.11tsp11.1900670167.opb270.44UNSATISFIABLE
normalized-t3002.11tsp11.1900546076.opb16.9079UNSATISFIABLE
normalized-t3002.11tsp11.1900547334.opb0.108859SATISFIABLE
normalized-t3002.11tsp11.1900569834.opb211.537UNSATISFIABLE
normalized-t3002.11tsp11.1900568952.opb0.666092SATISFIABLE
normalized-t3002.11tsp11.1900570242.opb178.583UNSATISFIABLE
normalized-t3002.11tsp11.1900566151.opb0.335508SATISFIABLE
normalized-t3002.11tsp11.1900552288.opb336.27UNSATISFIABLE
normalized-t3002.11tsp11.1900552735.opb315.88UNSATISFIABLE
normalized-t3002.11tsp11.1900571761.opb646.311UNSATISFIABLE
normalized-t3002.11tsp11.1900559676.opb1380.47UNSATISFIABLE
normalized-t3002.11tsp11.1900554373.opb0.208604SATISFIABLE
normalized-t3002.11tsp11.1900553647.opb335.337UNSATISFIABLE
normalized-t3002.11tsp11.1900583053.opb784.045UNSATISFIABLE
normalized-t3002.11tsp11.1900544484.opb164.2UNSATISFIABLE
normalized-t3002.11tsp11.1900554067.opb0.915885SATISFIABLE
normalized-t3002.11tsp11.1900568706.opb251.201UNSATISFIABLE
normalized-t3002.11tsp11.1900559641.opb2.37837SATISFIABLE
normalized-t3002.11tsp11.1900553644.opb0.37619SATISFIABLE
normalized-t3002.11tsp11.1900547461.opb2.76607SATISFIABLE
normalized-t3002.11tsp11.1900567135.opb114.967UNSATISFIABLE
normalized-t3002.11tsp11.1900565534.opb446.244UNSATISFIABLE
normalized-t3002.11tsp11.1900669309.opb4.50378SATISFIABLE
normalized-t3002.11tsp11.1900670234.opb716.976UNSATISFIABLE
normalized-t3002.11tsp11.1900554375.opb0.333644SATISFIABLE
normalized-t3002.11tsp11.1900546417.opb432.821UNSATISFIABLE
normalized-t3002.11tsp11.1900670675.opb100.9UNSATISFIABLE
normalized-t3002.11tsp11.1900576927.opb349.57UNSATISFIABLE
normalized-t3002.11tsp11.1900545610.opb568.936UNSATISFIABLE
normalized-t3002.11tsp11.1900557362.opb232.113UNSATISFIABLE
normalized-t3002.11tsp11.1900558739.opb385.958UNSATISFIABLE
normalized-t3002.11tsp11.1900573901.opb423.319UNSATISFIABLE
normalized-t3002.11tsp11.1900576151.opb544.415UNSATISFIABLE
normalized-t3002.11tsp11.1900554072.opb234.411UNSATISFIABLE
normalized-t3002.11tsp11.1900575442.opb211.937UNSATISFIABLE
normalized-t3002.11tsp11.1900667195.opb738.705UNSATISFIABLE
normalized-t3002.11tsp11.1900559365.opb0.530223SATISFIABLE
normalized-t3002.11tsp11.1900579996.opb691.249UNSATISFIABLE
normalized-t3002.11tsp11.1900581321.opb0.169373SATISFIABLE
normalized-t3002.11tsp11.1900561389.opb2.46825SATISFIABLE
normalized-t3002.11tsp11.1900561288.opb1201.15UNSATISFIABLE
normalized-t3002.11tsp11.1900566263.opb0.471384SATISFIABLE
normalized-t3002.11tsp11.1900669797.opb390.183UNSATISFIABLE
normalized-t3002.11tsp11.1900577000.opb0.466824SATISFIABLE
normalized-t3002.11tsp11.1900574948.opb0.356963SATISFIABLE
normalized-t3002.11tsp11.1900554389.opb0.136366SATISFIABLE
normalized-t3002.11tsp11.1900547427.opb0.274692SATISFIABLE
normalized-t3002.11tsp11.1900557957.opb309.824UNSATISFIABLE
normalized-t3002.11tsp11.1900564824.opb4.44871UNSATISFIABLE
normalized-t3002.11tsp11.1900563801.opb56.4475UNSATISFIABLE
normalized-t3002.11tsp11.1900571132.opb250.458UNSATISFIABLE
normalized-t3002.11tsp11.1900567024.opb123.398UNSATISFIABLE
normalized-t3002.11tsp11.1900547353.opb1.81972SATISFIABLE
normalized-t3002.11tsp11.1900544463.opb2.10866SATISFIABLE
normalized-t3002.11tsp11.1900571131.opb0.264171SATISFIABLE
normalized-t3002.11tsp11.1900551347.opb247.003UNSATISFIABLE
normalized-t3002.11tsp11.1900557568.opb0.209764SATISFIABLE
normalized-t3002.11tsp11.1900566270.opb8.01791SATISFIABLE
normalized-t3002.11tsp11.1900564281.opb153.588UNSATISFIABLE
normalized-t3002.11tsp11.1900558106.opb16.5869UNSATISFIABLE
normalized-t3002.11tsp11.1900550720.opb682.434UNSATISFIABLE
normalized-t3002.11tsp11.1900559416.opb14.9843SATISFIABLE
normalized-t3002.11tsp11.1900564822.opb0.173566SATISFIABLE
normalized-t3002.11tsp11.1900577940.opb707.719UNSATISFIABLE
normalized-t3002.11tsp11.1900567939.opb4.61925SATISFIABLE
normalized-t3002.11tsp11.1900553606.opb4.81978SATISFIABLE
normalized-t3002.11tsp11.1900557413.opb0.458341SATISFIABLE
normalized-t3002.11tsp11.1900554420.opb182.394UNSATISFIABLE
normalized-t3002.11tsp11.1900557574.opb229.11UNSATISFIABLE
normalized-t3002.11tsp11.1900551864.opb181.285UNSATISFIABLE
normalized-t3002.11tsp11.1900547389.opb282.877UNSATISFIABLE
normalized-t3002.11tsp11.1900573137.opb581.534UNSATISFIABLE
normalized-t3002.11tsp11.1900552423.opb6.37264UNSATISFIABLE
normalized-t3002.11tsp11.1900552311.opb0.352704SATISFIABLE
normalized-t3002.11tsp11.1900556231.opb348.584UNSATISFIABLE
normalized-t3002.11tsp11.1900584106.opb153.239UNSATISFIABLE
normalized-t3002.11tsp11.1900563250.opb765.976UNSATISFIABLE
normalized-t3002.11tsp11.1900582300.opb658.375UNSATISFIABLE
normalized-t3002.11tsp11.1900669299.opb1.90232SATISFIABLE
normalized-t3002.11tsp11.1900670756.opb1.92557SATISFIABLE
normalized-t3002.11tsp11.1900548667.opb1203.51UNSATISFIABLE
normalized-t3002.11tsp11.1900568186.opb231.184UNSATISFIABLE
normalized-t3002.11tsp11.1900566157.opb115.044UNSATISFIABLE
normalized-t2001.13queen13.1110974372.opb27.1546UNSATISFIABLE
normalized-t2001.13queen13.1110970277.opb1.67809SATISFIABLE
normalized-t2001.13queen13.1111224059.opb15.452UNSATISFIABLE
normalized-t2001.13queen13.1111227418.opb10.5358SATISFIABLE
normalized-t2001.13queen13.1110967327.opb0.812305SATISFIABLE
normalized-t2001.13queen13.1111227861.opb38.9239UNSATISFIABLE
normalized-t2001.13queen13.1111219348.opb27.6688UNSATISFIABLE
normalized-t2001.13queen13.1110975607.opb19.2806UNSATISFIABLE
normalized-t2001.13queen13.1111223220.opb41.2449UNSATISFIABLE
normalized-t2001.13queen13.1111212476.opb60.9917UNSATISFIABLE
normalized-t2001.13queen13.1111221203.opb34.2932UNSATISFIABLE
normalized-t2001.13queen13.1111223416.opb3.24471SATISFIABLE
normalized-t2001.13queen13.1111217392.opb32.0668UNSATISFIABLE
normalized-t2001.13queen13.1110967523.opb42.5535UNSATISFIABLE
normalized-t2001.13queen13.1110971363.opb33.652UNSATISFIABLE
normalized-t2001.13queen13.1110973863.opb42.6347SATISFIABLE
normalized-t2001.13queen13.1111226284.opb21.3259SATISFIABLE
normalized-t2001.13queen13.1111220546.opb31.7943UNSATISFIABLE
normalized-t2001.13queen13.1111226680.opb29.6577UNSATISFIABLE
normalized-t2001.13queen13.1110971097.opb40.5196SATISFIABLE
normalized-t2001.13queen13.1110971697.opb34.5873UNSATISFIABLE
normalized-t2001.13queen13.1110978334.opb34.7844UNSATISFIABLE
normalized-t2001.13queen13.1110976735.opb7.30839SATISFIABLE
normalized-t2001.13queen13.1110972958.opb7.36516SATISFIABLE
normalized-t2001.13queen13.1111221953.opb20.3047SATISFIABLE
normalized-t2001.13queen13.1110976730.opb62.4383UNSATISFIABLE
normalized-t2001.13queen13.1111213868.opb29.926UNSATISFIABLE
normalized-t2001.13queen13.1111223004.opb37.8668UNSATISFIABLE
normalized-t2001.13queen13.1111222080.opb19.0476SATISFIABLE
normalized-t2001.13queen13.1111224929.opb22.7058UNSATISFIABLE
normalized-t2001.13queen13.1111217380.opb7.3407SATISFIABLE
normalized-t2001.13queen13.1111225605.opb27.974UNSATISFIABLE
normalized-t2001.13queen13.1110970170.opb25.1645SATISFIABLE
normalized-t2001.13queen13.1111219399.opb14.9418SATISFIABLE
normalized-t2001.13queen13.1111226062.opb22.315UNSATISFIABLE
normalized-t2001.13queen13.1111222539.opb42.7173UNSATISFIABLE
normalized-t2001.13queen13.1110968094.opb30.4861UNSATISFIABLE
normalized-t2001.13queen13.1110967142.opb64.6173UNSATISFIABLE
normalized-t2001.13queen13.1111216188.opb28.5675SATISFIABLE
normalized-t2001.13queen13.1110969577.opb24.5755UNSATISFIABLE
normalized-t2001.13queen13.1111216864.opb22.5013SATISFIABLE
normalized-t2001.13queen13.1111212923.opb28.6822UNSATISFIABLE
normalized-t2001.13queen13.1110970631.opb21.5922UNSATISFIABLE
normalized-t2001.13queen13.1111224255.opb37.2963UNSATISFIABLE
normalized-t2001.13queen13.1111223689.opb18.8007SATISFIABLE
normalized-t2001.13queen13.1110969933.opb6.84369SATISFIABLE
normalized-t2001.13queen13.1111217555.opb36.1917UNSATISFIABLE
normalized-t2001.13queen13.1110969170.opb32.9697UNSATISFIABLE
normalized-t2001.13queen13.1110971766.opb0.378499SATISFIABLE
normalized-t2001.13queen13.1111212272.opb37.4124UNSATISFIABLE
normalized-t2001.13queen13.1110974180.opb39.4026UNSATISFIABLE
normalized-t2001.13queen13.1111218955.opb23.3777UNSATISFIABLE
normalized-t2001.13queen13.1110974553.opb19.5362SATISFIABLE
normalized-t2001.13queen13.1110977273.opb38.8059UNSATISFIABLE
normalized-t2001.13queen13.1111216823.opb31.6987UNSATISFIABLE
normalized-t2001.13queen13.1111213670.opb33.6749UNSATISFIABLE
normalized-t2001.13queen13.1111218024.opb35.7803UNSATISFIABLE
normalized-t2001.13queen13.1111221624.opb43.7326UNSATISFIABLE
normalized-t2001.13queen13.1111223596.opb7.00024SATISFIABLE
normalized-t2001.13queen13.1110975832.opb6.27211SATISFIABLE
normalized-t2001.13queen13.1110975965.opb73.6393UNSATISFIABLE
normalized-t2001.13queen13.1110976935.opb23.5512UNSATISFIABLE
normalized-t2001.13queen13.1110977266.opb43.0372SATISFIABLE
normalized-t2001.13queen13.1110977464.opb15.863SATISFIABLE
normalized-t2001.13queen13.1110973364.opb19.8663UNSATISFIABLE
normalized-t2001.13queen13.1111222257.opb27.5156UNSATISFIABLE
normalized-t2001.13queen13.1111219799.opb29.7446UNSATISFIABLE
normalized-t2001.13queen13.1110972154.opb43.5342UNSATISFIABLE
normalized-t2001.13queen13.1110968561.opb45.4639UNSATISFIABLE
normalized-t2001.13queen13.1111220767.opb42.8629UNSATISFIABLE
normalized-t2001.13queen13.1110978113.opb70.4953UNSATISFIABLE
normalized-t2001.13queen13.1110966688.opb21.7491UNSATISFIABLE
normalized-t2001.13queen13.1110972763.opb33.1806UNSATISFIABLE
normalized-t2001.13queen13.1111223696.opb16.5098SATISFIABLE
normalized-t2001.13queen13.1110973478.opb37.5803SATISFIABLE
normalized-t2001.13queen13.1110973670.opb45.6893UNSATISFIABLE
normalized-t2001.13queen13.1111224451.opb25.2037UNSATISFIABLE
normalized-t2001.13queen13.1111228076.opb49.1185UNSATISFIABLE
normalized-t2001.13queen13.1110973163.opb71.2624UNSATISFIABLE
normalized-t2001.13queen13.1110977780.opb25.378UNSATISFIABLE
normalized-t2001.13queen13.1111217374.opb2.7824SATISFIABLE
normalized-t2001.13queen13.1111220019.opb32.8806UNSATISFIABLE
normalized-t2001.13queen13.1111224522.opb3.19316SATISFIABLE
normalized-t2001.13queen13.1110975678.opb19.1081SATISFIABLE
normalized-t2001.13queen13.1110968898.opb49.7276UNSATISFIABLE
normalized-t2001.13queen13.1110970444.opb18.7633UNSATISFIABLE
normalized-t2001.13queen13.1111226368.opb20.7134UNSATISFIABLE
normalized-t2001.13queen13.1110969860.opb59.2363UNSATISFIABLE
normalized-t2001.13queen13.1111222248.opb10.8691SATISFIABLE
normalized-t2001.13queen13.1111227326.opb15.6746UNSATISFIABLE
normalized-t2001.13queen13.1111227012.opb36.224UNSATISFIABLE
normalized-t2001.13queen13.1110976157.opb29.33UNSATISFIABLE
normalized-t2001.13queen13.1111218757.opb46.3894UNSATISFIABLE
normalized-t2001.13queen13.1110967729.opb13.8263UNSATISFIABLE
normalized-t2001.13queen13.1111226241.opb40.5232SATISFIABLE
normalized-t2001.13queen13.1111225122.opb17.3481UNSATISFIABLE
normalized-t2001.13queen13.1110966483.opb12.5836UNSATISFIABLE
normalized-t2001.13queen13.1111216411.opb38.6126UNSATISFIABLE
normalized-t2001.13queen13.1110968431.opb9.11099SATISFIABLE
normalized-t2001.13queen13.1111218308.opb95.606UNSATISFIABLE