QF_AUFLIA (Single Query Track)
Competition results for the QF_AUFLIA
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 534
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| winner_seq | winner_par | winner_sat | winner_unsat | winner_24s |
|---|
| Yices2 | Yices2 | Yices2 | Yices2 | Yices2 |
Sequential Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 534 | 78.92374 | 132.342905 | 534 | 257 | 277 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 534 | 255.323872 | 308.614322 | 534 | 257 | 277 | 0 | 0 | 0 | 0 |
| OpenSMT | 0 | 534 | 464.923754 | 518.409879 | 534 | 257 | 277 | 0 | 0 | 0 | 0 |
| SMTInterpol | 0 | 534 | 1154.312621 | 528.832687 | 534 | 257 | 277 | 0 | 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 |
|---|
| Yices2 | 0 | 534 | 78.92374 | 132.342905 | 534 | 257 | 277 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 534 | 255.323872 | 308.614322 | 534 | 257 | 277 | 0 | 0 | 0 | 0 |
| OpenSMT | 0 | 534 | 464.923754 | 518.409879 | 534 | 257 | 277 | 0 | 0 | 0 | 0 |
| SMTInterpol | 0 | 534 | 1154.312621 | 528.832687 | 534 | 257 | 277 | 0 | 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 |
|---|
| Yices2 | 0 | 257 | 34.936226 | 60.646435 | 257 | 257 | 0 | 0 | 277 | 0 | 0 |
| OpenSMT | 0 | 257 | 115.905807 | 141.640197 | 257 | 257 | 0 | 0 | 277 | 0 | 0 |
| cvc5 | 0 | 257 | 120.89776 | 146.541602 | 257 | 257 | 0 | 0 | 277 | 0 | 0 |
| SMTInterpol | 0 | 257 | 283.382097 | 161.739019 | 257 | 257 | 0 | 0 | 277 | 0 | 0 |
UNSAT Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 277 | 43.987514 | 71.69647 | 277 | 0 | 277 | 0 | 257 | 0 | 0 |
| cvc5 | 0 | 277 | 134.426112 | 162.07272 | 277 | 0 | 277 | 0 | 257 | 0 | 0 |
| SMTInterpol | 0 | 277 | 870.930524 | 367.093668 | 277 | 0 | 277 | 0 | 257 | 0 | 0 |
| OpenSMT | 0 | 277 | 349.017946 | 376.769682 | 277 | 0 | 277 | 0 | 257 | 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 |
|---|
| Yices2 | 0 | 534 | 78.92374 | 132.342905 | 534 | 257 | 277 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 534 | 255.323872 | 308.614322 | 534 | 257 | 277 | 0 | 0 | 0 | 0 |
| SMTInterpol | 0 | 534 | 1154.312621 | 528.832687 | 534 | 257 | 277 | 0 | 0 | 0 | 0 |
| OpenSMT | 0 | 533 | 266.228221 | 319.606909 | 533 | 257 | 276 | 0 | 1 | 0 | 0 |