The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFLIRA logic in the Single Query Track.
Page generated on 2023-07-06 16:04:53 +0000
Benchmarks: 1683 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | — | cvc5 | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1566 | 7160.571 | 7215.571 | 1566 | 0 | 1566 | 117 | 113 | 0 |
| 2022-cvc5n | 0 | 1566 | 7716.853 | 7827.777 | 1566 | 0 | 1566 | 117 | 114 | 0 |
| Vampire | 0 | 1538 | 19713.641 | 5124.839 | 1538 | 0 | 1538 | 145 | 145 | 0 |
| iProver | 0 | 1305 | 40031.025 | 10692.18 | 1305 | 0 | 1305 | 378 | 378 | 0 |
| iProver Fixedn | 0 | 1303 | 40279.583 | 10806.505 | 1303 | 0 | 1303 | 380 | 380 | 0 |
| SMTInterpol | 0 | 1247 | 11087.186 | 9275.642 | 1247 | 0 | 1247 | 436 | 432 | 0 |
| UltimateEliminator+MathSAT | 0 | 3 | 17.986 | 10.253 | 3 | 0 | 3 | 1680 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1566 | 7160.571 | 7215.571 | 1566 | 0 | 1566 | 117 | 113 | 0 |
| 2022-cvc5n | 0 | 1566 | 7716.853 | 7827.777 | 1566 | 0 | 1566 | 117 | 114 | 0 |
| Vampire | 0 | 1546 | 30744.261 | 7897.161 | 1546 | 0 | 1546 | 137 | 137 | 0 |
| iProver | 0 | 1369 | 158245.115 | 40572.545 | 1369 | 0 | 1369 | 314 | 314 | 0 |
| iProver Fixedn | 0 | 1365 | 152394.883 | 39179.063 | 1365 | 0 | 1365 | 318 | 318 | 0 |
| SMTInterpol | 0 | 1248 | 12306.106 | 10370.602 | 1248 | 0 | 1248 | 435 | 425 | 0 |
| UltimateEliminator+MathSAT | 0 | 3 | 17.986 | 10.253 | 3 | 0 | 3 | 1680 | 0 | 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 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 42 | 1641 | 114 | 0 |
| Vampire | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 42 | 1641 | 137 | 0 |
| cvc5 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 42 | 1641 | 113 | 0 |
| SMTInterpol | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 42 | 1641 | 425 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 42 | 1641 | 0 | 0 |
| iProver | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 42 | 1641 | 314 | 0 |
| iProver Fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 42 | 1641 | 318 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1566 | 7160.571 | 7215.571 | 1566 | 0 | 1566 | 3 | 114 | 113 | 0 |
| 2022-cvc5n | 0 | 1566 | 7716.853 | 7827.777 | 1566 | 0 | 1566 | 3 | 114 | 114 | 0 |
| Vampire | 0 | 1546 | 30744.261 | 7897.161 | 1546 | 0 | 1546 | 23 | 114 | 137 | 0 |
| iProver | 0 | 1369 | 158245.115 | 40572.545 | 1369 | 0 | 1369 | 200 | 114 | 314 | 0 |
| iProver Fixedn | 0 | 1365 | 152394.883 | 39179.063 | 1365 | 0 | 1365 | 204 | 114 | 318 | 0 |
| SMTInterpol | 0 | 1248 | 12306.106 | 10370.602 | 1248 | 0 | 1248 | 321 | 114 | 425 | 0 |
| UltimateEliminator+MathSAT | 0 | 3 | 17.986 | 10.253 | 3 | 0 | 3 | 1566 | 114 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1519 | 1656.651 | 584.28 | 1519 | 0 | 1519 | 164 | 164 | 0 |
| cvc5 | 0 | 1495 | 165.485 | 164.87 | 1495 | 0 | 1495 | 188 | 188 | 0 |
| 2022-cvc5n | 0 | 1495 | 188.076 | 187.533 | 1495 | 0 | 1495 | 188 | 188 | 0 |
| SMTInterpol | 0 | 1219 | 1909.636 | 1001.962 | 1219 | 0 | 1219 | 464 | 463 | 0 |
| iProver | 0 | 1174 | 4056.272 | 1517.884 | 1174 | 0 | 1174 | 509 | 509 | 0 |
| iProver Fixedn | 0 | 1166 | 3909.011 | 1477.08 | 1166 | 0 | 1166 | 517 | 517 | 0 |
| UltimateEliminator+MathSAT | 0 | 3 | 17.986 | 10.253 | 3 | 0 | 3 | 1680 | 12 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.