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 2023-07-06 16:04:54 +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 |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-cvc5n | 0 | 1176 | 213427.426 | 217818.07 | 1176 | 387 | 789 | 1681 | 1681 | 0 |
| Vampire | 0 | 1175 | 65866.165 | 16715.988 | 1175 | 472 | 703 | 1682 | 1682 | 0 |
| cvc5 | 0 | 1171 | 214413.233 | 221556.195 | 1171 | 386 | 785 | 1686 | 1686 | 0 |
| iProver Fixedn | 0 | 629 | 52583.782 | 13608.65 | 629 | 47 | 582 | 2228 | 2228 | 0 |
| iProver | 0 | 581 | 49697.186 | 12858.383 | 581 | 0 | 581 | 2276 | 2259 | 0 |
| Yices2 | 0 | 343 | 11422.427 | 11419.25 | 343 | 30 | 313 | 2514 | 2514 | 0 |
| SMTInterpol | 0 | 217 | 18278.523 | 13406.953 | 217 | 10 | 207 | 2640 | 2616 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 2857 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1237 | 216888.695 | 54715.785 | 1237 | 476 | 761 | 1620 | 1620 | 0 |
| 2022-cvc5n | 0 | 1176 | 213427.426 | 217818.07 | 1176 | 387 | 789 | 1681 | 1681 | 0 |
| cvc5 | 0 | 1171 | 214413.233 | 221556.195 | 1171 | 386 | 785 | 1686 | 1686 | 0 |
| Yices2 | 0 | 343 | 11422.427 | 11419.25 | 343 | 30 | 313 | 2514 | 2514 | 0 |
| SMTInterpol | 0 | 221 | 24922.633 | 17727.923 | 221 | 10 | 211 | 2636 | 2522 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 2857 | 0 | 0 |
| iProver Fixedn | 9 | 895 | 434006.382 | 110480.247 | 895 | 221 | 674 | 1962 | 1932 | 0 |
| iProver | 9 | 676 | 202496.096 | 51597.241 | 676 | 0 | 676 | 2181 | 2135 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 476 | 32206.695 | 8170.765 | 476 | 476 | 0 | 8 | 2373 | 1620 | 0 |
| 2022-cvc5n | 0 | 387 | 191038.162 | 195161.649 | 387 | 387 | 0 | 97 | 2373 | 1681 | 0 |
| cvc5 | 0 | 386 | 190476.73 | 196661.369 | 386 | 386 | 0 | 98 | 2373 | 1686 | 0 |
| iProver Fixedn | 0 | 221 | 245570.081 | 62357.353 | 221 | 221 | 0 | 263 | 2373 | 1932 | 0 |
| Yices2 | 0 | 30 | 8.696 | 8.788 | 30 | 30 | 0 | 454 | 2373 | 2514 | 0 |
| SMTInterpol | 0 | 10 | 274.832 | 229.718 | 10 | 10 | 0 | 474 | 2373 | 2522 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 484 | 2373 | 0 | 0 |
| iProver | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 484 | 2373 | 2135 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-cvc5n | 0 | 789 | 22389.264 | 22656.421 | 789 | 0 | 789 | 106 | 1962 | 1681 | 0 |
| cvc5 | 0 | 785 | 23936.502 | 24894.826 | 785 | 0 | 785 | 110 | 1962 | 1686 | 0 |
| Vampire | 0 | 761 | 184682.001 | 46545.021 | 761 | 0 | 761 | 134 | 1962 | 1620 | 0 |
| Yices2 | 0 | 313 | 11413.731 | 11410.462 | 313 | 0 | 313 | 582 | 1962 | 2514 | 0 |
| SMTInterpol | 0 | 211 | 24647.801 | 17498.205 | 211 | 0 | 211 | 684 | 1962 | 2522 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 895 | 1962 | 0 | 0 |
| iProver | 9 | 676 | 202496.096 | 51597.241 | 676 | 0 | 676 | 219 | 1962 | 2135 | 0 |
| iProver Fixedn | 9 | 674 | 188436.301 | 48122.894 | 674 | 0 | 674 | 221 | 1962 | 1932 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 926 | 6434.589 | 1732.82 | 926 | 355 | 571 | 1931 | 1931 | 0 |
| cvc5 | 0 | 668 | 641.487 | 635.894 | 668 | 12 | 656 | 2189 | 2189 | 0 |
| 2022-cvc5n | 0 | 666 | 549.146 | 545.465 | 666 | 14 | 652 | 2191 | 2191 | 0 |
| iProver Fixedn | 0 | 497 | 6821.612 | 1872.738 | 497 | 34 | 463 | 2360 | 2360 | 0 |
| iProver | 0 | 459 | 6217.639 | 1741.735 | 459 | 0 | 459 | 2398 | 2384 | 0 |
| Yices2 | 0 | 290 | 534.986 | 530.378 | 290 | 30 | 260 | 2567 | 2567 | 0 |
| SMTInterpol | 0 | 141 | 1414.888 | 646.357 | 141 | 8 | 133 | 2716 | 2701 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 2857 | 90 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.