LIA (Single Query Track)
Competition results for the LIA
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 300
Time Limit: 1200 seconds
Memory Limit: 20480 GB
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 | 300 | 83.629631 | 115.355105 | 300 | 137 | 163 | 0 | 0 | 0 | 0 |
| YicesQS | 0 | 205 | 1292.826431 | 1313.933479 | 205 | 124 | 81 | 95 | 0 | 95 | 0 |
| iProver v3.9 | 0 | 115 | 3097.980179 | 905.47332 | 119 | 0 | 119 | 181 | 0 | 170 | 0 |
| SMTInterpol | 0 | 99 | 94.087085 | 61.481499 | 99 | 9 | 90 | 201 | 0 | 92 | 0 |
| Amaya | 15 | 154 | 190.306808 | 208.386429 | 169 | 29 | 140 | 131 | 0 | 24 | 73 |
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 | 300 | 83.629631 | 115.355105 | 300 | 137 | 163 | 0 | 0 | 0 | 0 |
| YicesQS | 0 | 205 | 1292.826431 | 1313.933479 | 205 | 124 | 81 | 95 | 0 | 95 | 0 |
| iProver v3.9 | 0 | 119 | 11381.129806 | 3004.948298 | 119 | 0 | 119 | 181 | 0 | 170 | 0 |
| SMTInterpol | 0 | 99 | 94.087085 | 61.481499 | 99 | 9 | 90 | 201 | 0 | 92 | 0 |
| Amaya | 15 | 154 | 190.306808 | 208.386429 | 169 | 29 | 140 | 131 | 0 | 24 | 73 |
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 | 137 | 54.30787 | 68.910051 | 137 | 137 | 0 | 0 | 163 | 0 | 0 |
| YicesQS | 0 | 124 | 1274.507288 | 1287.319446 | 124 | 124 | 0 | 13 | 163 | 13 | 0 |
| SMTInterpol | 0 | 9 | 3.621637 | 3.549696 | 9 | 9 | 0 | 128 | 163 | 74 | 0 |
| iProver v3.9 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 137 | 163 | 132 | 0 |
| Amaya | 11 | 25 | 50.440353 | 54.317506 | 36 | 25 | 11 | 101 | 163 | 19 | 52 |
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 | 163 | 29.321761 | 46.445054 | 163 | 0 | 163 | 0 | 137 | 0 | 0 |
| iProver v3.9 | 0 | 119 | 11381.129806 | 3004.948298 | 119 | 0 | 119 | 44 | 137 | 38 | 0 |
| SMTInterpol | 0 | 90 | 90.465448 | 57.931802 | 90 | 0 | 90 | 73 | 137 | 18 | 0 |
| YicesQS | 0 | 81 | 18.319142 | 26.614034 | 81 | 0 | 81 | 82 | 137 | 82 | 0 |
| Amaya | 4 | 129 | 139.866454 | 154.068923 | 133 | 4 | 129 | 30 | 137 | 5 | 21 |
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 | 300 | 83.629631 | 115.355105 | 300 | 137 | 163 | 0 | 0 | 0 | 0 |
| YicesQS | 0 | 199 | 67.792441 | 88.213614 | 199 | 118 | 81 | 0 | 101 | 0 | 0 |
| iProver v3.9 | 0 | 110 | 2011.679809 | 616.672554 | 110 | 0 | 110 | 5 | 185 | 0 | 0 |
| SMTInterpol | 0 | 99 | 94.087085 | 61.481499 | 99 | 9 | 90 | 72 | 129 | 0 | 0 |
| Amaya | 15 | 153 | 156.258473 | 174.171699 | 168 | 29 | 139 | 2 | 130 | 0 | 0 |