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