The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFDTNIRA logic in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 2149 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 | 1962 | 1274.537 | 1273.777 | 1962 | 0 | 1962 | 187 | 114 | 0 |
| cvc5 | 0 | 1959 | 480.882 | 479.041 | 1959 | 0 | 1959 | 190 | 120 | 0 |
| Vampire | 0 | 1811 | 110734.201 | 28040.768 | 1811 | 0 | 1811 | 338 | 338 | 0 |
| iProver | 0 | 1609 | 71073.397 | 18705.054 | 1609 | 0 | 1609 | 540 | 540 | 0 |
| iProver Fixedn | 0 | 1602 | 66295.807 | 17532.746 | 1602 | 0 | 1602 | 547 | 547 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-cvc5n | 0 | 1962 | 1274.537 | 1273.777 | 1962 | 0 | 1962 | 187 | 114 | 0 |
| cvc5 | 0 | 1959 | 480.882 | 479.041 | 1959 | 0 | 1959 | 190 | 120 | 0 |
| Vampire | 0 | 1845 | 177633.291 | 44876.198 | 1845 | 0 | 1845 | 304 | 304 | 0 |
| iProver | 0 | 1623 | 96497.567 | 25310.068 | 1623 | 0 | 1623 | 526 | 526 | 0 |
| iProver Fixedn | 0 | 1621 | 102220.597 | 26636.048 | 1621 | 0 | 1621 | 528 | 528 | 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 | 2149 | 114 | 0 |
| Vampire | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 2149 | 304 | 0 |
| cvc5 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 2149 | 120 | 0 |
| iProver | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 2149 | 526 | 0 |
| iProver Fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 2149 | 528 | 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 | 1962 | 1274.537 | 1273.777 | 1962 | 0 | 1962 | 16 | 171 | 114 | 0 |
| cvc5 | 0 | 1959 | 480.882 | 479.041 | 1959 | 0 | 1959 | 19 | 171 | 120 | 0 |
| Vampire | 0 | 1845 | 177633.291 | 44876.198 | 1845 | 0 | 1845 | 133 | 171 | 304 | 0 |
| iProver | 0 | 1623 | 96497.567 | 25310.068 | 1623 | 0 | 1623 | 355 | 171 | 526 | 0 |
| iProver Fixedn | 0 | 1621 | 102220.597 | 26636.048 | 1621 | 0 | 1621 | 357 | 171 | 528 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 1958 | 201.41 | 199.514 | 1958 | 0 | 1958 | 191 | 124 | 0 |
| 2022-cvc5n | 0 | 1958 | 497.79 | 496.812 | 1958 | 0 | 1958 | 191 | 122 | 0 |
| Vampire | 0 | 1494 | 5078.941 | 1418.503 | 1494 | 0 | 1494 | 655 | 655 | 0 |
| iProver Fixedn | 0 | 1457 | 7597.869 | 2509.444 | 1457 | 0 | 1457 | 692 | 692 | 0 |
| iProver | 0 | 1456 | 7705.073 | 2523.411 | 1456 | 0 | 1456 | 693 | 693 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.