Equality (Single Query Track)
Competition results for the Equality
division
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 4426
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics:- UF : 2857 benchmarks
- UFDT : 1569 benchmarks
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| cvc5 | cvc5 | cvc5 | cvc5 | cvc5 |
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 | 1748 | 325510.252204 | 325750.683047 | 1748 | 553 | 1195 | 2678 | 0 | 2675 | 0 |
| iProver v3.9 | 0 | 1090 | 112770.142085 | 29788.64549 | 1178 | 267 | 911 | 3248 | 0 | 3242 | 3 |
| SMTInterpol | 0 | 319 | 26407.368893 | 20717.460522 | 322 | 13 | 309 | 4104 | 0 | 3424 | 183 |
| Yices2 | 0 | 314 | 13971.829459 | 14005.798889 | 314 | 36 | 278 | 2543 | 1569 | 2542 | 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 | 1748 | 325510.252204 | 325750.683047 | 1748 | 553 | 1195 | 2678 | 0 | 2675 | 0 |
| iProver v3.9 | 0 | 1178 | 322510.038361 | 82906.855145 | 1178 | 267 | 911 | 3248 | 0 | 3242 | 3 |
| SMTInterpol | 0 | 322 | 30919.494554 | 23418.650294 | 322 | 13 | 309 | 4104 | 0 | 3424 | 183 |
| Yices2 | 0 | 314 | 13971.829459 | 14005.798889 | 314 | 36 | 278 | 2543 | 1569 | 2542 | 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 | 553 | 282890.729996 | 283002.247471 | 553 | 553 | 0 | 27 | 3846 | 27 | 0 |
| iProver v3.9 | 0 | 267 | 34441.692753 | 8887.426488 | 267 | 267 | 0 | 313 | 3846 | 310 | 0 |
| Yices2 | 0 | 36 | 98.939345 | 102.541518 | 36 | 36 | 0 | 412 | 3978 | 412 | 0 |
| SMTInterpol | 0 | 13 | 341.216714 | 298.234568 | 13 | 13 | 0 | 567 | 3846 | 412 | 47 |
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 | 1195 | 42619.522208 | 42748.435577 | 1195 | 0 | 1195 | 51 | 3180 | 51 | 0 |
| iProver v3.9 | 0 | 911 | 288068.345608 | 74019.428656 | 911 | 0 | 911 | 335 | 3180 | 334 | 1 |
| SMTInterpol | 0 | 309 | 30578.27784 | 23120.415726 | 309 | 0 | 309 | 937 | 3180 | 801 | 31 |
| Yices2 | 0 | 278 | 13872.890113 | 13903.25737 | 278 | 0 | 278 | 507 | 3641 | 506 | 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 |
|---|
| cvc5 | 0 | 974 | 839.317062 | 936.619443 | 974 | 20 | 954 | 0 | 3452 | 0 | 0 |
| iProver v3.9 | 0 | 819 | 11940.708103 | 3674.851041 | 819 | 227 | 592 | 0 | 3607 | 0 | 0 |
| Yices2 | 0 | 262 | 332.269374 | 358.511077 | 262 | 34 | 228 | 1 | 4163 | 0 | 0 |
| SMTInterpol | 0 | 206 | 2181.598596 | 991.155968 | 206 | 11 | 195 | 54 | 4166 | 0 | 0 |