NIA (Single Query Track)
Competition results for the NIA
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 254
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 | Amaya |
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 | 227 | 27525.112849 | 27556.245512 | 227 | 78 | 149 | 27 | 0 | 27 | 0 |
| Amaya | 0 | 199 | 763.390038 | 784.840409 | 199 | 51 | 148 | 55 | 0 | 12 | 2 |
| YicesQS | 0 | 107 | 614.045965 | 624.982565 | 107 | 65 | 42 | 147 | 0 | 147 | 0 |
| iProver v3.9 | 0 | 38 | 4508.832964 | 1180.75247 | 46 | 0 | 46 | 208 | 0 | 208 | 0 |
| SMTInterpol | 0 | 20 | 55.493564 | 24.146853 | 20 | 13 | 7 | 234 | 0 | 0 | 0 |
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 | 227 | 27525.112849 | 27556.245512 | 227 | 78 | 149 | 27 | 0 | 27 | 0 |
| Amaya | 0 | 199 | 763.390038 | 784.840409 | 199 | 51 | 148 | 55 | 0 | 12 | 2 |
| YicesQS | 0 | 107 | 614.045965 | 624.982565 | 107 | 65 | 42 | 147 | 0 | 147 | 0 |
| iProver v3.9 | 0 | 46 | 28837.689134 | 7310.710587 | 46 | 0 | 46 | 208 | 0 | 208 | 0 |
| SMTInterpol | 0 | 20 | 55.493564 | 24.146853 | 20 | 13 | 7 | 234 | 0 | 0 | 0 |
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 | 78 | 612.067238 | 620.274614 | 78 | 78 | 0 | 4 | 172 | 4 | 0 |
| YicesQS | 0 | 65 | 537.547352 | 544.216626 | 65 | 65 | 0 | 17 | 172 | 17 | 0 |
| Amaya | 0 | 51 | 440.56887 | 446.076133 | 51 | 51 | 0 | 31 | 172 | 1 | 2 |
| SMTInterpol | 0 | 13 | 49.367473 | 20.144905 | 13 | 13 | 0 | 69 | 172 | 0 | 0 |
| iProver v3.9 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 82 | 172 | 82 | 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 | 149 | 26913.045611 | 26935.970899 | 149 | 0 | 149 | 0 | 105 | 0 | 0 |
| Amaya | 0 | 134 | 316.63289 | 331.076128 | 134 | 0 | 134 | 15 | 105 | 8 | 0 |
| iProver v3.9 | 0 | 45 | 28815.894544 | 7304.316011 | 45 | 0 | 45 | 104 | 105 | 104 | 0 |
| YicesQS | 0 | 42 | 76.498613 | 80.76594 | 42 | 0 | 42 | 107 | 105 | 107 | 0 |
| SMTInterpol | 0 | 7 | 6.126091 | 4.001948 | 7 | 0 | 7 | 142 | 105 | 0 | 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 |
|---|
| Amaya | 0 | 189 | 283.393722 | 303.729793 | 189 | 45 | 144 | 36 | 29 | 0 | 0 |
| cvc5 | 0 | 136 | 96.570102 | 110.735518 | 136 | 77 | 59 | 0 | 118 | 0 | 0 |
| YicesQS | 0 | 105 | 57.715231 | 68.340844 | 105 | 64 | 41 | 0 | 149 | 0 | 0 |
| iProver v3.9 | 0 | 30 | 614.078373 | 184.000891 | 30 | 0 | 30 | 0 | 224 | 0 | 0 |
| SMTInterpol | 0 | 20 | 55.493564 | 24.146853 | 20 | 13 | 7 | 230 | 4 | 0 | 0 |