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 |