Equality_LinearArith (Single Query Track)
Competition results for the Equality_LinearArith
division
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 16456
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| cvc5 | cvc5 | cvc5 | cvc5 | cvc5 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 12632 | 176656.051026 | 177956.997592 | 12632 | 815 | 11817 | 3824 | 0 | 2963 | 2 |
| iProver v3.9 | 0 | 9590 | 469753.757009 | 129400.257514 | 10126 | 0 | 10126 | 6330 | 0 | 6223 | 0 |
| SMTInterpol | 0 | 9284 | 165243.833827 | 124301.386132 | 9299 | 583 | 8716 | 7157 | 0 | 5010 | 97 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 12632 | 176656.051026 | 177956.997592 | 12632 | 815 | 11817 | 3824 | 0 | 2963 | 2 |
| iProver v3.9 | 0 | 10126 | 1.913604021065e+06 | 495904.827496 | 10126 | 0 | 10126 | 6330 | 0 | 6223 | 0 |
| SMTInterpol | 0 | 9299 | 187356.978484 | 139607.666001 | 9299 | 583 | 8716 | 7157 | 0 | 5010 | 97 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 815 | 48263.925056 | 48354.323251 | 815 | 815 | 0 | 90 | 15551 | 56 | 0 |
| SMTInterpol | 0 | 583 | 426.123115 | 306.099356 | 583 | 583 | 0 | 322 | 15551 | 89 | 1 |
| iProver v3.9 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 905 | 15551 | 821 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 11817 | 128392.125969 | 129602.674341 | 11817 | 0 | 11817 | 169 | 4470 | 149 | 0 |
| iProver v3.9 | 0 | 10126 | 1.913604021065e+06 | 495904.827496 | 10126 | 0 | 10126 | 1860 | 4470 | 1854 | 0 |
| SMTInterpol | 0 | 8716 | 186930.85537 | 139301.566645 | 8716 | 0 | 8716 | 3270 | 4470 | 2879 | 36 |
24 seconds Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 11891 | 4436.204267 | 5627.213633 | 11891 | 674 | 11217 | 393 | 4172 | 0 | 1 |
| SMTInterpol | 0 | 8819 | 36142.821244 | 17002.608987 | 8819 | 583 | 8236 | 1543 | 6094 | 0 | 0 |
| iProver v3.9 | 0 | 8247 | 75712.939797 | 25895.284574 | 8247 | 0 | 8247 | 82 | 8127 | 0 | 0 |