The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UF logic in the Single Query Track.
Page generated on 2021-07-18 17:29:07 +0000
Benchmarks: 2857 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Vampire | Vampire | Vampire | cvc5 | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1153 | 2109996.921 | 2061770.947 | 1153 | 451 | 702 | 1704 | 1704 | 0 |
| 2020-CVC4n | 0 | 1144 | 2241065.961 | 2257999.15 | 1144 | 375 | 769 | 1713 | 1713 | 0 |
| 2020-Vampiren | 0 | 1142 | 2101683.098 | 2052188.063 | 1142 | 448 | 694 | 1715 | 1696 | 0 |
| Vampire - fixedn | 0 | 1130 | 2113938.746 | 2065569.103 | 1130 | 443 | 687 | 1727 | 1707 | 0 |
| cvc5 | 0 | 933 | 1143159.619 | 2400654.272 | 933 | 164 | 769 | 1924 | 1924 | 0 |
| iProver - fixed2n | 0 | 744 | 2591812.106 | 2550436.216 | 744 | 215 | 529 | 2113 | 1975 | 138 |
| iProver - fixedn | 0 | 733 | 2597168.253 | 2559502.022 | 733 | 213 | 520 | 2124 | 1974 | 147 |
| veriT | 0 | 693 | 2573610.821 | 2573921.446 | 693 | 0 | 693 | 2164 | 2044 | 62 |
| z3n | 0 | 462 | 2178898.243 | 2180506.489 | 462 | 58 | 404 | 2395 | 1390 | 36 |
| Yices2 | 0 | 349 | 3027820.971 | 3028157.786 | 349 | 39 | 310 | 2508 | 2508 | 0 |
| SMTInterpol | 0 | 221 | 3168208.061 | 3162365.695 | 221 | 9 | 212 | 2636 | 2617 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 15142.87 | 8638.235 | 0 | 0 | 0 | 2857 | 0 | 0 |
| iProver | 12 | 827 | 2482069.235 | 2435358.888 | 827 | 214 | 613 | 2030 | 1872 | 144 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1194 | 2176451.071 | 2041645.326 | 1194 | 454 | 740 | 1663 | 1662 | 0 |
| 2020-Vampiren | 0 | 1178 | 2149905.798 | 2031233.621 | 1178 | 452 | 726 | 1679 | 1658 | 0 |
| Vampire - fixedn | 0 | 1172 | 2180112.406 | 2043509.724 | 1172 | 445 | 727 | 1685 | 1664 | 0 |
| 2020-CVC4n | 0 | 1144 | 2255285.231 | 2257918.87 | 1144 | 375 | 769 | 1713 | 1713 | 0 |
| cvc5 | 0 | 933 | 2399219.537 | 2400555.872 | 933 | 164 | 769 | 1924 | 1924 | 0 |
| iProver - fixed2n | 0 | 772 | 2622410.466 | 2533299.992 | 772 | 219 | 553 | 2085 | 1946 | 138 |
| iProver - fixedn | 0 | 761 | 2640175.243 | 2545135.962 | 761 | 216 | 545 | 2096 | 1946 | 147 |
| veriT | 0 | 693 | 2573855.701 | 2573844.546 | 693 | 0 | 693 | 2164 | 2044 | 62 |
| z3n | 0 | 462 | 2179799.123 | 2180444.109 | 462 | 58 | 404 | 2395 | 1390 | 36 |
| Yices2 | 0 | 349 | 3028078.401 | 3028073.076 | 349 | 39 | 310 | 2508 | 2508 | 0 |
| SMTInterpol | 0 | 227 | 3330026.391 | 3138872.245 | 227 | 9 | 218 | 2630 | 2525 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 15142.87 | 8638.235 | 0 | 0 | 0 | 2857 | 0 | 0 |
| iProver | 13 | 847 | 2506554.725 | 2421794.696 | 847 | 217 | 630 | 2010 | 1850 | 144 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 454 | 48189.666 | 25763.988 | 454 | 454 | 0 | 15 | 2388 | 1662 | 0 |
| 2020-Vampiren | 0 | 452 | 51928.118 | 24903.907 | 452 | 452 | 0 | 17 | 2388 | 1658 | 0 |
| Vampire - fixedn | 0 | 445 | 48189.405 | 26663.211 | 445 | 445 | 0 | 24 | 2388 | 1664 | 0 |
| 2020-CVC4n | 0 | 375 | 290664.636 | 293224.118 | 375 | 375 | 0 | 94 | 2388 | 1713 | 0 |
| iProver - fixed2n | 0 | 219 | 316546.101 | 304276.107 | 219 | 219 | 0 | 250 | 2388 | 1946 | 138 |
| iProver | 0 | 217 | 299872.063 | 289272.964 | 217 | 217 | 0 | 252 | 2388 | 1850 | 144 |
| iProver - fixedn | 0 | 216 | 316642.514 | 306083.394 | 216 | 216 | 0 | 253 | 2388 | 1946 | 147 |
| cvc5 | 0 | 164 | 440630.302 | 441989.397 | 164 | 164 | 0 | 305 | 2388 | 1924 | 0 |
| z3n | 0 | 58 | 362832.59 | 363361.109 | 58 | 58 | 0 | 411 | 2388 | 1390 | 36 |
| Yices2 | 0 | 39 | 516147.715 | 516147.864 | 39 | 39 | 0 | 430 | 2388 | 2508 | 0 |
| SMTInterpol | 0 | 9 | 568504.578 | 527817.881 | 9 | 9 | 0 | 460 | 2388 | 2525 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 2399.753 | 1394.121 | 0 | 0 | 0 | 469 | 2388 | 0 | 0 |
| veriT | 0 | 0 | 521861.826 | 521856.521 | 0 | 0 | 0 | 469 | 2388 | 2044 | 62 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 769 | 187389.235 | 187366.476 | 769 | 0 | 769 | 143 | 1945 | 1924 | 0 |
| 2020-CVC4n | 0 | 769 | 193420.595 | 193494.752 | 769 | 0 | 769 | 143 | 1945 | 1713 | 0 |
| Vampire | 0 | 740 | 357061.405 | 244681.339 | 740 | 0 | 740 | 172 | 1945 | 1662 | 0 |
| Vampire - fixedn | 0 | 727 | 357122.96 | 245672.833 | 727 | 0 | 727 | 185 | 1945 | 1664 | 0 |
| 2020-Vampiren | 0 | 726 | 326777.679 | 235129.714 | 726 | 0 | 726 | 186 | 1945 | 1658 | 0 |
| veriT | 0 | 693 | 281078.045 | 281071.766 | 693 | 0 | 693 | 219 | 1945 | 2044 | 62 |
| iProver - fixed2n | 0 | 553 | 534664.364 | 457823.885 | 553 | 0 | 553 | 359 | 1945 | 1946 | 138 |
| iProver - fixedn | 0 | 545 | 552332.729 | 467852.568 | 545 | 0 | 545 | 367 | 1945 | 1946 | 147 |
| z3n | 0 | 404 | 493182.144 | 493202.608 | 404 | 0 | 404 | 508 | 1945 | 1390 | 36 |
| Yices2 | 0 | 310 | 740730.686 | 740725.213 | 310 | 0 | 310 | 602 | 1945 | 2508 | 0 |
| SMTInterpol | 0 | 218 | 887807.013 | 854480.675 | 218 | 0 | 218 | 694 | 1945 | 2525 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 4866.299 | 2774.282 | 0 | 0 | 0 | 912 | 1945 | 0 | 0 |
| iProver | 13 | 630 | 435620.516 | 363150.98 | 630 | 0 | 630 | 282 | 1945 | 1850 | 144 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Vampiren | 0 | 931 | 52525.143 | 47685.193 | 931 | 367 | 564 | 1926 | 1912 | 0 |
| Vampire | 0 | 928 | 53426.804 | 48210.03 | 928 | 364 | 564 | 1929 | 1929 | 0 |
| Vampire - fixedn | 0 | 910 | 53440.154 | 48267.455 | 910 | 356 | 554 | 1947 | 1932 | 0 |
| cvc5 | 0 | 655 | 53511.295 | 53476.896 | 655 | 10 | 645 | 2202 | 2202 | 0 |
| veriT | 0 | 650 | 53301.039 | 53293.096 | 650 | 0 | 650 | 2207 | 2128 | 62 |
| 2020-CVC4n | 0 | 629 | 54202.132 | 54173.228 | 629 | 9 | 620 | 2228 | 2228 | 0 |
| iProver - fixed2n | 0 | 626 | 62135.614 | 55949.203 | 626 | 196 | 430 | 2231 | 2093 | 138 |
| iProver - fixedn | 0 | 620 | 61999.829 | 56025.515 | 620 | 195 | 425 | 2237 | 2090 | 147 |
| z3n | 0 | 425 | 58880.078 | 58877.524 | 425 | 54 | 371 | 2432 | 2396 | 36 |
| Yices2 | 0 | 288 | 62205.668 | 62198.453 | 288 | 37 | 251 | 2569 | 2569 | 0 |
| SMTInterpol | 0 | 142 | 66274.158 | 65516.037 | 142 | 8 | 134 | 2715 | 2702 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 15142.87 | 8638.235 | 0 | 0 | 0 | 2857 | 0 | 0 |
| iProver | 4 | 689 | 62355.883 | 54821.59 | 689 | 196 | 493 | 2168 | 2020 | 144 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.