LRA (Single Query Track)
Competition results for the LRA
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 1013
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| YicesQS | YicesQS | YicesQS | YicesQS | YicesQS |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| YicesQS | 0 | 1003 | 307.599288 | 409.677363 | 1003 | 387 | 616 | 10 | 0 | 10 | 0 |
| cvc5 | 0 | 857 | 20929.037168 | 21023.630185 | 857 | 336 | 521 | 156 | 0 | 156 | 0 |
| SMTInterpol | 0 | 169 | 1587.144761 | 655.038314 | 169 | 2 | 167 | 844 | 0 | 50 | 0 |
| iProver v3.9 | 9 | 192 | 41319.686043 | 10795.257061 | 235 | 0 | 235 | 778 | 0 | 778 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| YicesQS | 0 | 1003 | 307.599288 | 409.677363 | 1003 | 387 | 616 | 10 | 0 | 10 | 0 |
| cvc5 | 0 | 857 | 20929.037168 | 21023.630185 | 857 | 336 | 521 | 156 | 0 | 156 | 0 |
| SMTInterpol | 0 | 169 | 1587.144761 | 655.038314 | 169 | 2 | 167 | 844 | 0 | 50 | 0 |
| iProver v3.9 | 9 | 226 | 135654.470163 | 34688.832004 | 235 | 0 | 235 | 778 | 0 | 778 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| YicesQS | 0 | 387 | 117.476848 | 156.920688 | 387 | 387 | 0 | 3 | 623 | 3 | 0 |
| cvc5 | 0 | 336 | 4571.560218 | 4607.664483 | 336 | 336 | 0 | 54 | 623 | 54 | 0 |
| SMTInterpol | 0 | 2 | 0.874378 | 0.804264 | 2 | 2 | 0 | 388 | 623 | 37 | 0 |
| iProver v3.9 | 9 | 0 | 3587.388883 | 929.635337 | 9 | 0 | 9 | 381 | 623 | 381 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| YicesQS | 0 | 616 | 190.12244 | 252.756675 | 616 | 0 | 616 | 7 | 390 | 7 | 0 |
| cvc5 | 0 | 521 | 16357.47695 | 16415.965701 | 521 | 0 | 521 | 102 | 390 | 102 | 0 |
| iProver v3.9 | 0 | 226 | 132067.081279 | 33759.196667 | 226 | 0 | 226 | 397 | 390 | 397 | 0 |
| SMTInterpol | 0 | 167 | 1586.270383 | 654.23405 | 167 | 0 | 167 | 456 | 390 | 13 | 0 |
24 seconds Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| YicesQS | 0 | 1002 | 273.716033 | 375.677223 | 1002 | 387 | 615 | 0 | 11 | 0 | 0 |
| cvc5 | 0 | 739 | 390.161633 | 467.882843 | 739 | 281 | 458 | 0 | 274 | 0 | 0 |
| SMTInterpol | 0 | 166 | 1309.382086 | 466.055166 | 166 | 2 | 164 | 770 | 77 | 0 | 0 |
| iProver v3.9 | 1 | 96 | 1275.86653 | 400.029709 | 97 | 0 | 97 | 0 | 916 | 0 | 0 |