UFLIA (Single Query Track)
Competition results for the UFLIA
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 2849
Time Limit: 1200 seconds
Memory Limit: 20480 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 | 1628 | 32420.34317 | 32590.471577 | 1628 | 3 | 1625 | 1221 | 0 | 1200 | 0 |
| iProver v3.9 | 0 | 652 | 94254.87376 | 25067.156344 | 773 | 0 | 773 | 2076 | 0 | 2076 | 0 |
| SMTInterpol | 0 | 384 | 27332.603997 | 21903.12971 | 386 | 6 | 380 | 2463 | 0 | 2146 | 71 |
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 | 1628 | 32420.34317 | 32590.471577 | 1628 | 3 | 1625 | 1221 | 0 | 1200 | 0 |
| iProver v3.9 | 0 | 773 | 430115.386276 | 110249.352584 | 773 | 0 | 773 | 2076 | 0 | 2076 | 0 |
| SMTInterpol | 0 | 386 | 29836.74144 | 24226.770412 | 386 | 6 | 380 | 2463 | 0 | 2146 | 71 |
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 | 6 | 4.39797 | 3.195005 | 6 | 6 | 0 | 5 | 2838 | 1 | 0 |
| cvc5 | 0 | 3 | 1081.101342 | 1081.605131 | 3 | 3 | 0 | 8 | 2838 | 3 | 0 |
| iProver v3.9 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 11 | 2838 | 11 | 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 | 1625 | 31339.241828 | 31508.866446 | 1625 | 0 | 1625 | 43 | 1181 | 43 | 0 |
| iProver v3.9 | 0 | 773 | 430115.386276 | 110249.352584 | 773 | 0 | 773 | 895 | 1181 | 895 | 0 |
| SMTInterpol | 0 | 380 | 29832.34347 | 24223.575407 | 380 | 0 | 380 | 1288 | 1181 | 1225 | 18 |
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 | 1453 | 2333.66038 | 2479.773498 | 1453 | 1 | 1452 | 0 | 1396 | 0 | 0 |
| iProver v3.9 | 0 | 390 | 11297.193192 | 3385.024396 | 390 | 0 | 390 | 0 | 2459 | 0 | 0 |
| SMTInterpol | 0 | 303 | 2693.577564 | 1109.334287 | 303 | 6 | 297 | 71 | 2475 | 0 | 0 |