The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFDTNIRA logic in the Single Query Track.
Page generated on 2023-07-06 16:04:53 +0000
Benchmarks: 762 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | — | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-cvc5n | 0 | 616 | 265.75 | 265.574 | 616 | 0 | 616 | 146 | 119 | 0 |
| cvc5 | 0 | 616 | 1453.326 | 1453.237 | 616 | 0 | 616 | 146 | 118 | 0 |
| Vampire | 0 | 589 | 94812.928 | 23836.173 | 589 | 0 | 589 | 173 | 173 | 0 |
| iProver | 0 | 491 | 25464.387 | 6659.676 | 491 | 0 | 491 | 271 | 271 | 0 |
| iProver Fixedn | 0 | 490 | 20359.006 | 5409.744 | 490 | 0 | 490 | 272 | 272 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-cvc5n | 0 | 616 | 265.75 | 265.574 | 616 | 0 | 616 | 146 | 119 | 0 |
| cvc5 | 0 | 616 | 1453.326 | 1453.237 | 616 | 0 | 616 | 146 | 118 | 0 |
| Vampire | 0 | 597 | 111801.348 | 28114.348 | 597 | 0 | 597 | 165 | 165 | 0 |
| iProver | 0 | 503 | 47389.047 | 12213.133 | 503 | 0 | 503 | 259 | 259 | 0 |
| iProver Fixedn | 0 | 502 | 45027.136 | 11652.024 | 502 | 0 | 502 | 260 | 260 | 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 | 0 | 762 | 119 | 0 |
| Vampire | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 762 | 165 | 0 |
| cvc5 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 762 | 118 | 0 |
| iProver | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 762 | 259 | 0 |
| iProver Fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 762 | 260 | 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 | 616 | 265.75 | 265.574 | 616 | 0 | 616 | 3 | 143 | 119 | 0 |
| cvc5 | 0 | 616 | 1453.326 | 1453.237 | 616 | 0 | 616 | 3 | 143 | 118 | 0 |
| Vampire | 0 | 597 | 111801.348 | 28114.348 | 597 | 0 | 597 | 22 | 143 | 165 | 0 |
| iProver | 0 | 503 | 47389.047 | 12213.133 | 503 | 0 | 503 | 116 | 143 | 259 | 0 |
| iProver Fixedn | 0 | 502 | 45027.136 | 11652.024 | 502 | 0 | 502 | 117 | 143 | 260 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-cvc5n | 0 | 614 | 137.639 | 137.449 | 614 | 0 | 614 | 148 | 121 | 0 |
| cvc5 | 0 | 613 | 53.684 | 53.387 | 613 | 0 | 613 | 149 | 121 | 0 |
| iProver Fixedn | 0 | 443 | 2014.274 | 684.824 | 443 | 0 | 443 | 319 | 319 | 0 |
| iProver | 0 | 436 | 1773.037 | 625.582 | 436 | 0 | 436 | 326 | 326 | 0 |
| Vampire | 0 | 420 | 1469.749 | 409.307 | 420 | 0 | 420 | 342 | 342 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.