QF_UFNIA (Single Query Track)
Competition results for the QF_UFNIA
logic
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 339
Time Limit: 1200 seconds
Memory Limit: 30720 GB
Winners
Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
---|
Yices2 | Yices2 | Yices2 | cvc5 | 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 | 264 | 11704.61 | 11739.34 | 264 | 228 | 36 | 75 | 0 | 73 | 2 |
cvc5 | 0 | 171 | 10974.49 | 10997.23 | 171 | 125 | 46 | 168 | 0 | 168 | 0 |
SMTInterpol | 0 | 134 | 22361.16 | 20265.99 | 134 | 103 | 31 | 205 | 0 | 86 | 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 | 264 | 11704.61 | 11739.34 | 264 | 228 | 36 | 75 | 0 | 73 | 2 |
cvc5 | 0 | 171 | 10974.49 | 10997.23 | 171 | 125 | 46 | 168 | 0 | 168 | 0 |
SMTInterpol | 0 | 134 | 22361.16 | 20265.99 | 134 | 103 | 31 | 205 | 0 | 86 | 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 | 228 | 9951.02 | 9980.99 | 228 | 228 | 0 | 5 | 106 | 3 | 2 |
cvc5 | 0 | 125 | 10515.55 | 10532.46 | 125 | 125 | 0 | 108 | 106 | 108 | 0 |
SMTInterpol | 0 | 103 | 20307.17 | 18493.16 | 103 | 103 | 0 | 130 | 106 | 41 | 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 | 46 | 458.95 | 464.76 | 46 | 0 | 46 | 9 | 284 | 9 | 0 |
Yices2 | 0 | 36 | 1753.60 | 1758.35 | 36 | 0 | 36 | 19 | 284 | 19 | 0 |
SMTInterpol | 0 | 31 | 2053.98 | 1772.82 | 31 | 0 | 31 | 24 | 284 | 6 | 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 | 203 | 575.98 | 601.34 | 203 | 171 | 32 | 0 | 136 | 0 | 0 |
cvc5 | 0 | 133 | 237.71 | 254.22 | 133 | 92 | 41 | 0 | 206 | 0 | 0 |
SMTInterpol | 0 | 58 | 266.61 | 143.46 | 58 | 37 | 21 | 97 | 184 | 0 | 0 |