The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the ALIA logic in the Single Query Track.
Page generated on 2023-07-06 16:04:53 +0000
Benchmarks: 1537 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Vampire | Vampire | SMTInterpol | Vampire | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 401 | 16419.754 | 4178.287 | 401 | 0 | 401 | 1136 | 1136 | 0 |
| cvc5 | 0 | 294 | 11789.947 | 11847.707 | 294 | 18 | 276 | 1243 | 648 | 0 |
| 2022-cvc5n | 0 | 290 | 11699.024 | 11710.925 | 290 | 18 | 272 | 1247 | 652 | 0 |
| iProver Fixedn | 0 | 263 | 11484.518 | 3047.483 | 263 | 0 | 263 | 1274 | 1266 | 0 |
| iProver | 0 | 262 | 11099.53 | 2903.337 | 262 | 0 | 262 | 1275 | 1267 | 0 |
| SMTInterpol | 0 | 239 | 14657.261 | 12482.516 | 239 | 19 | 220 | 1298 | 466 | 0 |
| UltimateEliminator+MathSAT | 0 | 5 | 64.671 | 30.447 | 5 | 5 | 0 | 1532 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 406 | 31153.944 | 7879.408 | 406 | 0 | 406 | 1131 | 1131 | 0 |
| cvc5 | 0 | 294 | 11789.947 | 11847.707 | 294 | 18 | 276 | 1243 | 648 | 0 |
| 2022-cvc5n | 0 | 290 | 11699.024 | 11710.925 | 290 | 18 | 272 | 1247 | 652 | 0 |
| iProver Fixedn | 0 | 271 | 37231.938 | 9567.291 | 271 | 0 | 271 | 1266 | 1258 | 0 |
| iProver | 0 | 270 | 35231.65 | 9013.574 | 270 | 0 | 270 | 1267 | 1259 | 0 |
| SMTInterpol | 0 | 239 | 14657.261 | 12482.516 | 239 | 19 | 220 | 1298 | 464 | 0 |
| UltimateEliminator+MathSAT | 0 | 5 | 64.671 | 30.447 | 5 | 5 | 0 | 1532 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| SMTInterpol | 0 | 19 | 31.717 | 16.229 | 19 | 19 | 0 | 3 | 1515 | 464 | 0 |
| cvc5 | 0 | 18 | 1012.27 | 1014.377 | 18 | 18 | 0 | 4 | 1515 | 648 | 0 |
| 2022-cvc5n | 0 | 18 | 1029.09 | 1032.237 | 18 | 18 | 0 | 4 | 1515 | 652 | 0 |
| UltimateEliminator+MathSAT | 0 | 5 | 64.671 | 30.447 | 5 | 5 | 0 | 17 | 1515 | 0 | 0 |
| Vampire | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 22 | 1515 | 1131 | 0 |
| iProver | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 22 | 1515 | 1259 | 0 |
| iProver Fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 22 | 1515 | 1258 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 406 | 31153.944 | 7879.408 | 406 | 0 | 406 | 5 | 1126 | 1131 | 0 |
| cvc5 | 0 | 276 | 10777.677 | 10833.33 | 276 | 0 | 276 | 135 | 1126 | 648 | 0 |
| 2022-cvc5n | 0 | 272 | 10669.934 | 10678.689 | 272 | 0 | 272 | 139 | 1126 | 652 | 0 |
| iProver Fixedn | 0 | 271 | 37231.938 | 9567.291 | 271 | 0 | 271 | 140 | 1126 | 1258 | 0 |
| iProver | 0 | 270 | 35231.65 | 9013.574 | 270 | 0 | 270 | 141 | 1126 | 1259 | 0 |
| SMTInterpol | 0 | 220 | 14625.544 | 12466.287 | 220 | 0 | 220 | 191 | 1126 | 464 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 411 | 1126 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 364 | 1945.904 | 534.246 | 364 | 0 | 364 | 1173 | 1173 | 0 |
| 2022-cvc5n | 0 | 244 | 189.296 | 187.729 | 244 | 13 | 231 | 1293 | 949 | 0 |
| cvc5 | 0 | 242 | 174.606 | 174.537 | 242 | 13 | 229 | 1295 | 947 | 0 |
| iProver | 0 | 224 | 2900.973 | 814.363 | 224 | 0 | 224 | 1313 | 1306 | 0 |
| iProver Fixedn | 0 | 224 | 3017.297 | 842.835 | 224 | 0 | 224 | 1313 | 1306 | 0 |
| SMTInterpol | 0 | 193 | 575.746 | 322.774 | 193 | 19 | 174 | 1344 | 558 | 0 |
| UltimateEliminator+MathSAT | 0 | 5 | 64.671 | 30.447 | 5 | 5 | 0 | 1532 | 24 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.