Equality (Single Query Track)
Competition results for the Equality
division
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 4426
Time Limit: 1200 seconds
Memory Limit: 30720 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 | 1714 | 304081.09 | 304332.02 | 1714 | 502 | 1212 | 2712 | 0 | 2712 | 0 |
| iProver v3.9.3 | 0 | 1058 | 98190.91 | 25955.13 | 1141 | 235 | 906 | 3285 | 0 | 3281 | 2 |
| Yices2 | 0 | 323 | 17347.38 | 17389.88 | 323 | 33 | 290 | 2534 | 1569 | 2532 | 0 |
| SMTInterpol | 0 | 317 | 26676.94 | 21144.64 | 319 | 10 | 309 | 4107 | 0 | 2361 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 2857 | 1569 | 0 | 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 | 1714 | 304081.09 | 304332.02 | 1714 | 502 | 1212 | 2712 | 0 | 2712 | 0 |
| iProver v3.9.3 | 0 | 1141 | 324376.65 | 83047.70 | 1141 | 235 | 906 | 3285 | 0 | 3281 | 2 |
| Yices2 | 0 | 323 | 17347.38 | 17389.88 | 323 | 33 | 290 | 2534 | 1569 | 2532 | 0 |
| SMTInterpol | 0 | 319 | 29828.15 | 22526.31 | 319 | 10 | 309 | 4107 | 0 | 2361 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 2857 | 1569 | 0 | 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 | 502 | 260147.82 | 260243.12 | 502 | 502 | 0 | 23 | 3901 | 23 | 0 |
| iProver v3.9.3 | 0 | 235 | 29214.12 | 7517.25 | 235 | 235 | 0 | 290 | 3901 | 289 | 0 |
| Yices2 | 0 | 33 | 342.53 | 346.73 | 33 | 33 | 0 | 384 | 4009 | 384 | 0 |
| SMTInterpol | 0 | 10 | 50.62 | 31.09 | 10 | 10 | 0 | 515 | 3901 | 236 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 417 | 4009 | 0 | 0 |
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 | 1212 | 43933.27 | 44088.91 | 1212 | 0 | 1212 | 40 | 3174 | 40 | 0 |
| iProver v3.9.3 | 0 | 906 | 295162.53 | 75530.44 | 906 | 0 | 906 | 346 | 3174 | 346 | 0 |
| SMTInterpol | 0 | 309 | 29777.53 | 22495.22 | 309 | 0 | 309 | 943 | 3174 | 585 | 0 |
| Yices2 | 0 | 290 | 17004.85 | 17043.15 | 290 | 0 | 290 | 497 | 3639 | 496 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 787 | 3639 | 0 | 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 | 1005 | 800.38 | 924.76 | 1005 | 15 | 990 | 0 | 3421 | 0 | 0 |
| iProver v3.9.3 | 0 | 799 | 10536.67 | 3283.43 | 799 | 199 | 600 | 0 | 3627 | 0 | 0 |
| Yices2 | 0 | 264 | 411.87 | 444.42 | 264 | 30 | 234 | 2 | 4160 | 0 | 0 |
| SMTInterpol | 0 | 214 | 2135.53 | 1083.87 | 214 | 9 | 205 | 55 | 4157 | 0 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 2857 | 1569 | 0 | 0 |