UF (Single Query Track)
Competition results for the UF
logic
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 2857
Time Limit: 1200 seconds
Memory Limit: 30720 GB
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
|
1158
|
235762.40 |
235935.66 |
1158 |
394 |
764 |
1699 |
0 |
1699 |
0 |
|
iProver v3.9.3
|
0
|
748
|
62316.17 |
16352.74 |
790 |
235 |
555 |
2067 |
0 |
2065 |
2 |
|
Yices2
|
0
|
323
|
17347.38 |
17389.88 |
323 |
33 |
290 |
2534 |
0 |
2532 |
0 |
|
SMTInterpol
|
0
|
195
|
17193.27 |
13907.63 |
195 |
7 |
188 |
2662 |
0 |
1328 |
0 |
|
UltimateEliminator+MathSAT
|
0
|
0
|
0.00 |
0.00 |
0 |
0 |
0 |
2857 |
0 |
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
|
1158
|
235762.40 |
235935.66 |
1158 |
394 |
764 |
1699 |
0 |
1699 |
0 |
|
iProver v3.9.3
|
0
|
790
|
163354.72 |
41803.54 |
790 |
235 |
555 |
2067 |
0 |
2065 |
2 |
|
Yices2
|
0
|
323
|
17347.38 |
17389.88 |
323 |
33 |
290 |
2534 |
0 |
2532 |
0 |
|
SMTInterpol
|
0
|
195
|
17193.27 |
13907.63 |
195 |
7 |
188 |
2662 |
0 |
1328 |
0 |
|
UltimateEliminator+MathSAT
|
0
|
0
|
0.00 |
0.00 |
0 |
0 |
0 |
2857 |
0 |
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
|
394
|
206953.45 |
207028.42 |
394 |
394 |
0 |
23 |
2440 |
23 |
0 |
|
iProver v3.9.3
|
0
|
235
|
29214.12 |
7517.25 |
235 |
235 |
0 |
182 |
2440 |
182 |
0 |
|
Yices2
|
0
|
33
|
342.53 |
346.73 |
33 |
33 |
0 |
384 |
2440 |
384 |
0 |
|
SMTInterpol
|
0
|
7
|
48.76 |
29.60 |
7 |
7 |
0 |
410 |
2440 |
171 |
0 |
|
UltimateEliminator+MathSAT
|
0
|
0
|
0.00 |
0.00 |
0 |
0 |
0 |
417 |
2440 |
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
|
764
|
28808.95 |
28907.24 |
764 |
0 |
764 |
23 |
2070 |
23 |
0 |
|
iProver v3.9.3
|
0
|
555
|
134140.60 |
34286.29 |
555 |
0 |
555 |
232 |
2070 |
232 |
0 |
|
Yices2
|
0
|
290
|
17004.85 |
17043.15 |
290 |
0 |
290 |
497 |
2070 |
496 |
0 |
|
SMTInterpol
|
0
|
188
|
17144.51 |
13878.03 |
188 |
0 |
188 |
599 |
2070 |
345 |
0 |
|
UltimateEliminator+MathSAT
|
0
|
0
|
0.00 |
0.00 |
0 |
0 |
0 |
787 |
2070 |
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
|
630
|
531.08 |
609.13 |
630 |
10 |
620 |
0 |
2227 |
0 |
0 |
|
iProver v3.9.3
|
0
|
596
|
5792.39 |
1831.58 |
596 |
199 |
397 |
0 |
2261 |
0 |
0 |
|
Yices2
|
0
|
264
|
411.87 |
444.42 |
264 |
30 |
234 |
2 |
2591 |
0 |
0 |
|
SMTInterpol
|
0
|
134
|
1171.29 |
576.43 |
134 |
6 |
128 |
10 |
2713 |
0 |
0 |
|
UltimateEliminator+MathSAT
|
0
|
0
|
0.00 |
0.00 |
0 |
0 |
0 |
2857 |
0 |
0 |
0 |