NRA (Single Query Track)
Competition results for the NRA
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 99
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| winner_seq | winner_par | winner_sat | winner_unsat | winner_24s |
|---|
| SMT-RAT | SMT-RAT | YicesQS | SMT-RAT | SMT-RAT |
Sequential Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMT-RAT | 0 | 93 | 261.164964 | 270.64359 | 93 | 3 | 90 | 6 | 0 | 6 | 0 |
| YicesQS | 0 | 93 | 984.021953 | 993.587881 | 93 | 4 | 89 | 6 | 0 | 6 | 0 |
| cvc5 | 0 | 88 | 2237.40273 | 2247.098267 | 88 | 4 | 84 | 11 | 0 | 11 | 0 |
| iProver v3.9 | 0 | 74 | 4162.530785 | 1112.134836 | 85 | 0 | 85 | 14 | 0 | 13 | 1 |
| SMTInterpol | 0 | 40 | 28.034721 | 20.652564 | 40 | 1 | 39 | 59 | 0 | 0 | 0 |
Parallel Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMT-RAT | 0 | 93 | 261.164964 | 270.64359 | 93 | 3 | 90 | 6 | 0 | 6 | 0 |
| YicesQS | 0 | 93 | 984.021953 | 993.587881 | 93 | 4 | 89 | 6 | 0 | 6 | 0 |
| cvc5 | 0 | 88 | 2237.40273 | 2247.098267 | 88 | 4 | 84 | 11 | 0 | 11 | 0 |
| iProver v3.9 | 0 | 85 | 35458.777429 | 9005.022566 | 85 | 0 | 85 | 14 | 0 | 13 | 1 |
| SMTInterpol | 0 | 40 | 28.034721 | 20.652564 | 40 | 1 | 39 | 59 | 0 | 0 | 0 |
SAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| YicesQS | 0 | 4 | 0.89813 | 1.298632 | 4 | 4 | 0 | 1 | 94 | 1 | 0 |
| cvc5 | 0 | 4 | 301.842854 | 302.268112 | 4 | 4 | 0 | 1 | 94 | 1 | 0 |
| SMT-RAT | 0 | 3 | 0.385131 | 0.68494 | 3 | 3 | 0 | 2 | 94 | 2 | 0 |
| SMTInterpol | 0 | 1 | 0.554483 | 0.451561 | 1 | 1 | 0 | 4 | 94 | 0 | 0 |
| iProver v3.9 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 5 | 94 | 5 | 0 |
UNSAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMT-RAT | 0 | 90 | 260.779832 | 269.958649 | 90 | 0 | 90 | 3 | 6 | 3 | 0 |
| YicesQS | 0 | 89 | 983.123824 | 992.289249 | 89 | 0 | 89 | 4 | 6 | 4 | 0 |
| cvc5 | 0 | 84 | 1935.559876 | 1944.830155 | 84 | 0 | 84 | 9 | 6 | 9 | 0 |
| iProver v3.9 | 0 | 84 | 35148.35309 | 8925.467876 | 84 | 0 | 84 | 9 | 6 | 8 | 1 |
| SMTInterpol | 0 | 39 | 27.480238 | 20.201003 | 39 | 0 | 39 | 54 | 6 | 0 | 0 |
24 seconds Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMT-RAT | 0 | 92 | 25.324187 | 34.575586 | 92 | 3 | 89 | 0 | 7 | 0 | 0 |
| YicesQS | 0 | 91 | 15.379599 | 24.720346 | 91 | 4 | 87 | 0 | 8 | 0 | 0 |
| cvc5 | 0 | 84 | 13.53897 | 22.446028 | 84 | 3 | 81 | 0 | 15 | 0 | 0 |
| iProver v3.9 | 0 | 66 | 595.975943 | 195.284229 | 66 | 0 | 66 | 0 | 33 | 0 | 0 |
| SMTInterpol | 0 | 40 | 28.034721 | 20.652564 | 40 | 1 | 39 | 59 | 0 | 0 | 0 |