The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFNIA logic in the Single Query Track.
Page generated on 2021-07-18 17:29:08 +0000
Benchmarks: 6278 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Vampire | iProver | UltimateEliminator+MathSAT | cvc5 | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 3520 | 3243340.495 | 3342065.676 | 3520 | 715 | 2805 | 2758 | 2666 | 0 |
| cvc5 - fixedn | 0 | 3512 | 1434716.467 | 3323677.667 | 3512 | 699 | 2813 | 2766 | 2724 | 0 |
| z3n | 0 | 2762 | 2643786.752 | 2645143.467 | 2762 | 636 | 2126 | 3516 | 1847 | 7 |
| Vampire | 0 | 2528 | 4726817.934 | 4502476.465 | 2528 | 0 | 2528 | 3750 | 3687 | 0 |
| Vampire - fixedn | 0 | 2500 | 4722387.266 | 4500336.329 | 2500 | 0 | 2500 | 3778 | 3686 | 0 |
| 2020-Vampiren | 0 | 2143 | 5064965.033 | 4887705.763 | 2143 | 0 | 2143 | 4135 | 4022 | 0 |
| iProver | 0 | 1264 | 6106625.727 | 6034885.732 | 1264 | 0 | 1264 | 5014 | 4975 | 33 |
| UltimateEliminator+MathSAT | 0 | 520 | 847225.283 | 833451.972 | 520 | 334 | 186 | 5758 | 657 | 0 |
| SMTInterpol | 0 | 176 | 16507.651 | 14720.999 | 176 | 83 | 93 | 6102 | 10 | 0 |
| cvc5 | 5 | 3520 | 1431264.659 | 3308167.573 | 3520 | 702 | 2818 | 2758 | 2708 | 0 |
| 2019-Par4n | 7 | 3763 | 3240230.998 | 3127014.429 | 3763 | 731 | 3032 | 2515 | 2507 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 3520 | 3337547.324 | 3341902.906 | 3520 | 715 | 2805 | 2758 | 2666 | 0 |
| cvc5 - fixedn | 0 | 3512 | 3322492.142 | 3323517.607 | 3512 | 699 | 2813 | 2766 | 2724 | 0 |
| z3n | 0 | 2762 | 2644440.302 | 2645069.887 | 2762 | 636 | 2126 | 3516 | 1847 | 7 |
| Vampire - fixedn | 0 | 2542 | 4939315.216 | 4400543.412 | 2542 | 0 | 2542 | 3736 | 3538 | 0 |
| 2020-Vampiren | 0 | 2328 | 5616578.693 | 4805726.846 | 2328 | 0 | 2328 | 3950 | 3801 | 0 |
| iProver | 0 | 1459 | 6454098.687 | 5948793.221 | 1459 | 0 | 1459 | 4819 | 4780 | 33 |
| UltimateEliminator+MathSAT | 0 | 520 | 847225.283 | 833451.972 | 520 | 334 | 186 | 5758 | 657 | 0 |
| SMTInterpol | 0 | 176 | 18263.131 | 14391.29 | 176 | 83 | 93 | 6102 | 9 | 0 |
| cvc5 | 5 | 3520 | 3307285.207 | 3308015.803 | 3520 | 702 | 2818 | 2758 | 2708 | 0 |
| 2019-Par4n | 7 | 3783 | 3248749.278 | 3119645.582 | 3783 | 735 | 3048 | 2495 | 2487 | 1 |
| Vampire | 26 | 2585 | 4958463.854 | 4379504.832 | 2585 | 0 | 2585 | 3693 | 3500 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 715 | 47933.458 | 48173.529 | 715 | 715 | 0 | 33 | 5530 | 2666 | 0 |
| cvc5 - fixedn | 0 | 699 | 56441.404 | 56619.659 | 699 | 699 | 0 | 49 | 5530 | 2724 | 0 |
| z3n | 0 | 636 | 102207.453 | 102206.752 | 636 | 636 | 0 | 112 | 5530 | 1847 | 7 |
| UltimateEliminator+MathSAT | 0 | 334 | 445314.03 | 444404.619 | 334 | 334 | 0 | 414 | 5530 | 657 | 0 |
| SMTInterpol | 0 | 83 | 9957.044 | 9873.081 | 83 | 83 | 0 | 665 | 5530 | 9 | 0 |
| Vampire | 0 | 0 | 880800.73 | 866383.16 | 0 | 0 | 0 | 748 | 5530 | 3500 | 0 |
| iProver | 0 | 0 | 890456.643 | 890425.759 | 0 | 0 | 0 | 748 | 5530 | 4780 | 33 |
| Vampire - fixedn | 0 | 0 | 922823.68 | 897555.65 | 0 | 0 | 0 | 748 | 5530 | 3538 | 0 |
| 2020-Vampiren | 0 | 0 | 912000.95 | 897581.39 | 0 | 0 | 0 | 748 | 5530 | 3801 | 0 |
| cvc5 | 5 | 702 | 54769.036 | 54853.315 | 702 | 702 | 0 | 46 | 5530 | 2708 | 0 |
| 2019-Par4n | 7 | 735 | 48568.506 | 32338.17 | 735 | 735 | 0 | 13 | 5530 | 2487 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3048 | 588980.772 | 476107.412 | 3048 | 0 | 3048 | 306 | 2924 | 2487 | 1 |
| cvc5 | 0 | 2818 | 649709.141 | 650339.777 | 2818 | 0 | 2818 | 536 | 2924 | 2708 | 0 |
| cvc5 - fixedn | 0 | 2813 | 663150.451 | 663991.926 | 2813 | 0 | 2813 | 541 | 2924 | 2724 | 0 |
| 2020-CVC4n | 0 | 2805 | 704792.757 | 708907.622 | 2805 | 0 | 2805 | 549 | 2924 | 2666 | 0 |
| Vampire - fixedn | 0 | 2542 | 1359090.376 | 891978.452 | 2542 | 0 | 2542 | 812 | 2924 | 3538 | 0 |
| 2020-Vampiren | 0 | 2328 | 2032417.073 | 1298847.904 | 2328 | 0 | 2328 | 1026 | 2924 | 3801 | 0 |
| z3n | 0 | 2126 | 850807.627 | 850689.919 | 2126 | 0 | 2126 | 1228 | 2924 | 1847 | 7 |
| iProver | 0 | 1459 | 2952442.044 | 2447167.462 | 1459 | 0 | 1459 | 1895 | 2924 | 4780 | 33 |
| UltimateEliminator+MathSAT | 0 | 186 | 345936.515 | 337367.058 | 186 | 0 | 186 | 3168 | 2924 | 657 | 0 |
| SMTInterpol | 0 | 93 | 6000.115 | 2548.829 | 93 | 0 | 93 | 3261 | 2924 | 9 | 0 |
| Vampire | 26 | 2585 | 1430461.164 | 901953.112 | 2585 | 0 | 2585 | 769 | 2924 | 3500 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 - fixedn | 0 | 3074 | 80434.801 | 80375.244 | 3074 | 678 | 2396 | 3204 | 3201 | 0 |
| 2020-CVC4n | 0 | 2860 | 85178.722 | 85095.022 | 2860 | 622 | 2238 | 3418 | 3414 | 0 |
| z3n | 0 | 2615 | 81823.125 | 81740.154 | 2615 | 609 | 2006 | 3663 | 3139 | 7 |
| Vampire | 0 | 1704 | 134619.757 | 116199.49 | 1704 | 0 | 1704 | 4574 | 4574 | 0 |
| Vampire - fixedn | 0 | 1658 | 134244.553 | 116553.538 | 1658 | 0 | 1658 | 4620 | 4597 | 0 |
| 2020-Vampiren | 0 | 1535 | 126795.211 | 116844.345 | 1535 | 0 | 1535 | 4743 | 4719 | 0 |
| iProver | 0 | 1055 | 141798.414 | 129979.563 | 1055 | 0 | 1055 | 5223 | 5184 | 33 |
| UltimateEliminator+MathSAT | 0 | 452 | 48054.563 | 36361.185 | 452 | 271 | 181 | 5826 | 791 | 0 |
| SMTInterpol | 0 | 175 | 4733.862 | 2952.455 | 175 | 82 | 93 | 6103 | 11 | 0 |
| cvc5 | 2 | 3079 | 80290.42 | 80233.712 | 3079 | 681 | 2398 | 3199 | 3193 | 0 |
| 2019-Par4n | 7 | 3204 | 80126.499 | 77171.176 | 3204 | 676 | 2528 | 3074 | 3066 | 1 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.