UFLIA (Single Query Track)
Competition results for the UFLIA
logic
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 2849
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 | SMTInterpol | 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 | 1656 | 33743.71 | 33950.87 | 1656 | 2 | 1654 | 1193 | 0 | 1176 | 0 |
iProver v3.9.3 | 0 | 664 | 81662.42 | 21773.15 | 786 | 0 | 786 | 2063 | 0 | 2063 | 0 |
SMTInterpol | 0 | 381 | 28140.69 | 22980.50 | 382 | 4 | 378 | 2467 | 0 | 1754 | 0 |
UltimateEliminator+MathSAT | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 2849 | 0 | 1 | 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 | 1656 | 33743.71 | 33950.87 | 1656 | 2 | 1654 | 1193 | 0 | 1176 | 0 |
iProver v3.9.3 | 0 | 786 | 436647.04 | 111469.05 | 786 | 0 | 786 | 2063 | 0 | 2063 | 0 |
SMTInterpol | 0 | 382 | 29636.45 | 23994.28 | 382 | 4 | 378 | 2467 | 0 | 1754 | 0 |
UltimateEliminator+MathSAT | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 2849 | 0 | 1 | 0 |
SAT Performance Performance
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
---|
SMTInterpol | 0 | 4 | 2.72 | 2.16 | 4 | 4 | 0 | 5 | 2840 | 0 | 0 |
cvc5 | 0 | 2 | 1081.38 | 1081.81 | 2 | 2 | 0 | 7 | 2840 | 3 | 0 |
UltimateEliminator+MathSAT | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 9 | 2840 | 0 | 0 |
iProver v3.9.3 | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 9 | 2840 | 9 | 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 | 1654 | 32662.33 | 32869.06 | 1654 | 0 | 1654 | 52 | 1143 | 52 | 0 |
iProver v3.9.3 | 0 | 786 | 436647.04 | 111469.05 | 786 | 0 | 786 | 920 | 1143 | 920 | 0 |
SMTInterpol | 0 | 378 | 29633.73 | 23992.12 | 378 | 0 | 378 | 1328 | 1143 | 1140 | 0 |
UltimateEliminator+MathSAT | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 1706 | 1143 | 1 | 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 | 1505 | 1896.97 | 2081.17 | 1505 | 0 | 1505 | 0 | 1344 | 0 | 0 |
iProver v3.9.3 | 0 | 424 | 11855.72 | 3543.22 | 424 | 0 | 424 | 0 | 2425 | 0 | 0 |
SMTInterpol | 0 | 296 | 2107.51 | 941.41 | 296 | 4 | 292 | 72 | 2481 | 0 | 0 |
UltimateEliminator+MathSAT | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 2843 | 6 | 0 | 0 |