Arith (Single Query Track)
Competition results for the Arith
division
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 1666
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:- LIA : 300 benchmarks
- LRA : 1013 benchmarks
- NIA : 254 benchmarks
- NRA : 99 benchmarks
Winners
| winner_seq | winner_par | winner_sat | winner_unsat | winner_24s |
|---|
| cvc5 | cvc5 | YicesQS | cvc5 | YicesQS |
Sequential Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 1472 | 50775.182378 | 50942.329068 | 1472 | 555 | 917 | 194 | 0 | 194 | 0 |
| YicesQS | 0 | 1408 | 3198.493637 | 3342.181288 | 1408 | 580 | 828 | 258 | 0 | 258 | 0 |
| SMTInterpol | 0 | 328 | 1764.760131 | 761.31923 | 328 | 25 | 303 | 1338 | 0 | 142 | 0 |
| SMT-RAT | 0 | 93 | 261.164964 | 270.64359 | 93 | 3 | 90 | 6 | 1567 | 6 | 0 |
| iProver v3.9 | 9 | 428 | 53089.02997 | 13993.617687 | 485 | 0 | 485 | 1181 | 0 | 1169 | 1 |
| Amaya | 15 | 368 | 953.696846 | 993.226838 | 368 | 80 | 288 | 186 | 1112 | 36 | 75 |
Parallel Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 1472 | 50775.182378 | 50942.329068 | 1472 | 555 | 917 | 194 | 0 | 194 | 0 |
| YicesQS | 0 | 1408 | 3198.493637 | 3342.181288 | 1408 | 580 | 828 | 258 | 0 | 258 | 0 |
| SMTInterpol | 0 | 328 | 1764.760131 | 761.31923 | 328 | 25 | 303 | 1338 | 0 | 142 | 0 |
| SMT-RAT | 0 | 93 | 261.164964 | 270.64359 | 93 | 3 | 90 | 6 | 1567 | 6 | 0 |
| iProver v3.9 | 9 | 485 | 211332.066532 | 54009.513455 | 485 | 0 | 485 | 1181 | 0 | 1169 | 1 |
| Amaya | 15 | 368 | 953.696846 | 993.226838 | 368 | 80 | 288 | 186 | 1112 | 36 | 75 |
SAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| YicesQS | 0 | 580 | 1930.429618 | 1989.755391 | 580 | 580 | 0 | 34 | 1052 | 34 | 0 |
| cvc5 | 0 | 555 | 5539.77818 | 5599.11726 | 555 | 555 | 0 | 59 | 1052 | 59 | 0 |
| SMTInterpol | 0 | 25 | 54.41797 | 24.950427 | 25 | 25 | 0 | 589 | 1052 | 111 | 0 |
| SMT-RAT | 0 | 3 | 0.385131 | 0.68494 | 3 | 3 | 0 | 2 | 1661 | 2 | 0 |
| iProver v3.9 | 9 | 9 | 3587.388883 | 929.635337 | 9 | 0 | 9 | 605 | 1052 | 600 | 0 |
| Amaya | 11 | 87 | 491.009224 | 500.39364 | 87 | 76 | 11 | 132 | 1447 | 20 | 54 |
UNSAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 917 | 45235.404198 | 45343.211808 | 917 | 0 | 917 | 111 | 638 | 111 | 0 |
| YicesQS | 0 | 828 | 1268.064019 | 1352.425897 | 828 | 0 | 828 | 200 | 638 | 200 | 0 |
| iProver v3.9 | 0 | 474 | 207412.458719 | 52993.928852 | 474 | 0 | 474 | 554 | 638 | 547 | 1 |
| SMTInterpol | 0 | 303 | 1710.342161 | 736.368803 | 303 | 0 | 303 | 725 | 638 | 31 | 0 |
| SMT-RAT | 0 | 90 | 260.779832 | 269.958649 | 90 | 0 | 90 | 3 | 1573 | 3 | 0 |
| Amaya | 4 | 267 | 456.499344 | 485.145051 | 267 | 4 | 263 | 45 | 1354 | 13 | 21 |
24 seconds Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| YicesQS | 0 | 1397 | 414.603304 | 556.952027 | 1397 | 573 | 824 | 0 | 269 | 0 | 0 |
| cvc5 | 0 | 1259 | 583.900336 | 716.419494 | 1259 | 498 | 761 | 0 | 407 | 0 | 0 |
| SMTInterpol | 0 | 325 | 1486.997456 | 572.336082 | 325 | 25 | 300 | 1131 | 210 | 0 | 0 |
| SMT-RAT | 0 | 92 | 25.324187 | 34.575586 | 92 | 3 | 89 | 0 | 1574 | 0 | 0 |
| iProver v3.9 | 1 | 303 | 4497.600655 | 1395.987384 | 303 | 0 | 303 | 5 | 1358 | 0 | 0 |
| Amaya | 15 | 357 | 439.652196 | 477.901492 | 357 | 74 | 283 | 38 | 1271 | 0 | 0 |