UF (Single Query Track)
Competition results for the UF
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 2857
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 | iProver v3.9 |
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 | 1177 | 243333.832979 | 243501.107816 | 1177 | 421 | 756 | 1680 | 0 | 1680 | 0 |
| iProver v3.9 | 0 | 784 | 70798.317829 | 18577.768879 | 839 | 267 | 572 | 2018 | 0 | 2015 | 3 |
| Yices2 | 0 | 314 | 13971.829459 | 14005.798889 | 314 | 36 | 278 | 2543 | 0 | 2542 | 0 |
| SMTInterpol | 0 | 202 | 16793.067609 | 13285.602205 | 203 | 11 | 192 | 2654 | 0 | 2159 | 161 |
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 | 1177 | 243333.832979 | 243501.107816 | 1177 | 421 | 756 | 1680 | 0 | 1680 | 0 |
| iProver v3.9 | 0 | 839 | 189591.230697 | 48609.627132 | 839 | 267 | 572 | 2018 | 0 | 2015 | 3 |
| Yices2 | 0 | 314 | 13971.829459 | 14005.798889 | 314 | 36 | 278 | 2543 | 0 | 2542 | 0 |
| SMTInterpol | 0 | 203 | 18230.861567 | 14014.342467 | 203 | 11 | 192 | 2654 | 0 | 2159 | 161 |
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 | 421 | 217393.865137 | 217480.224613 | 421 | 421 | 0 | 27 | 2409 | 27 | 0 |
| iProver v3.9 | 0 | 267 | 34441.692753 | 8887.426488 | 267 | 267 | 0 | 181 | 2409 | 181 | 0 |
| Yices2 | 0 | 36 | 98.939345 | 102.541518 | 36 | 36 | 0 | 412 | 2409 | 412 | 0 |
| SMTInterpol | 0 | 11 | 339.966394 | 297.280678 | 11 | 11 | 0 | 437 | 2409 | 314 | 45 |
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 | 756 | 25939.967842 | 26020.883203 | 756 | 0 | 756 | 29 | 2072 | 29 | 0 |
| iProver v3.9 | 0 | 572 | 155149.537944 | 39722.200644 | 572 | 0 | 572 | 213 | 2072 | 212 | 1 |
| Yices2 | 0 | 278 | 13872.890113 | 13903.25737 | 278 | 0 | 278 | 507 | 2072 | 506 | 0 |
| SMTInterpol | 0 | 192 | 17890.895174 | 13717.06179 | 192 | 0 | 192 | 593 | 2072 | 501 | 27 |
24 seconds Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| iProver v3.9 | 0 | 631 | 6893.061268 | 2144.90493 | 631 | 227 | 404 | 0 | 2226 | 0 | 0 |
| cvc5 | 0 | 619 | 582.037475 | 643.864213 | 619 | 15 | 604 | 0 | 2238 | 0 | 0 |
| Yices2 | 0 | 262 | 332.269374 | 358.511077 | 262 | 34 | 228 | 1 | 2594 | 0 | 0 |
| SMTInterpol | 0 | 127 | 1269.606422 | 578.033212 | 127 | 9 | 118 | 17 | 2713 | 0 | 0 |