QF_Equality (Single Query Track)
Competition results for the QF_Equality
division
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 3821
Time Limit: 1200 seconds
Memory Limit: 30720 GB
Logics:
Winners
| Sequential Performance |
Parallel Performance |
SAT Performance (parallel) |
UNSAT Performance (parallel) |
24 seconds Performance (parallel) |
|
Yices2
|
Yices2
|
Yices2
|
Yices2
|
Yices2
|
Sequential Performance Performance
| Solver |
Error Score |
Correct Score |
CPU Time Score |
Wall Time Score |
Solved |
Solved SAT |
Solved UNSAT |
Unsolved |
Abstained |
Timeout |
Memout |
|
Yices2
|
0
|
3821
|
1646.35 |
2119.78 |
3821 |
1621 |
2200 |
0 |
0 |
0 |
0 |
|
OpenSMT
|
0
|
3820
|
7611.09 |
8085.56 |
3820 |
1621 |
2199 |
1 |
0 |
1 |
0 |
|
cvc5
|
0
|
3819
|
5162.81 |
5633.47 |
3819 |
1621 |
2198 |
2 |
0 |
2 |
0 |
|
SMTInterpol
|
0
|
3743
|
25386.50 |
11800.75 |
3743 |
1621 |
2122 |
78 |
0 |
24 |
0 |
Parallel Performance Performance
| Solver |
Error Score |
Correct Score |
CPU Time Score |
Wall Time Score |
Solved |
Solved SAT |
Solved UNSAT |
Unsolved |
Abstained |
Timeout |
Memout |
|
Yices2
|
0
|
3821
|
1646.35 |
2119.78 |
3821 |
1621 |
2200 |
0 |
0 |
0 |
0 |
|
OpenSMT
|
0
|
3820
|
7611.09 |
8085.56 |
3820 |
1621 |
2199 |
1 |
0 |
1 |
0 |
|
cvc5
|
0
|
3819
|
5162.81 |
5633.47 |
3819 |
1621 |
2198 |
2 |
0 |
2 |
0 |
|
SMTInterpol
|
0
|
3743
|
25386.50 |
11800.75 |
3743 |
1621 |
2122 |
78 |
0 |
24 |
0 |
SAT Performance Performance
| Solver |
Error Score |
Correct Score |
CPU Time Score |
Wall Time Score |
Solved |
Solved SAT |
Solved UNSAT |
Unsolved |
Abstained |
Timeout |
Memout |
|
Yices2
|
0
|
1621
|
268.99 |
470.12 |
1621 |
1621 |
0 |
0 |
2200 |
0 |
0 |
|
OpenSMT
|
0
|
1621
|
416.09 |
617.44 |
1621 |
1621 |
0 |
0 |
2200 |
0 |
0 |
|
cvc5
|
0
|
1621
|
502.87 |
702.86 |
1621 |
1621 |
0 |
0 |
2200 |
0 |
0 |
|
SMTInterpol
|
0
|
1621
|
3834.58 |
1832.77 |
1621 |
1621 |
0 |
0 |
2200 |
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 |
|
Yices2
|
0
|
2200
|
1377.36 |
1649.66 |
2200 |
0 |
2200 |
0 |
1621 |
0 |
0 |
|
OpenSMT
|
0
|
2199
|
7195.00 |
7468.13 |
2199 |
0 |
2199 |
1 |
1621 |
1 |
0 |
|
cvc5
|
0
|
2198
|
4659.94 |
4930.60 |
2198 |
0 |
2198 |
2 |
1621 |
2 |
0 |
|
SMTInterpol
|
0
|
2122
|
21551.93 |
9967.99 |
2122 |
0 |
2122 |
78 |
1621 |
24 |
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 |
|
Yices2
|
0
|
3818
|
733.61 |
1206.55 |
3818 |
1621 |
2197 |
0 |
3 |
0 |
0 |
|
OpenSMT
|
0
|
3794
|
2155.86 |
2626.33 |
3794 |
1621 |
2173 |
0 |
27 |
0 |
0 |
|
cvc5
|
0
|
3787
|
1941.64 |
2407.95 |
3787 |
1621 |
2166 |
0 |
34 |
0 |
0 |
|
SMTInterpol
|
0
|
3708
|
19481.10 |
8844.64 |
3708 |
1620 |
2088 |
0 |
113 |
0 |
0 |