Equality_NonLinearArith (Single Query Track)
Competition results for the Equality_NonLinearArith
division
in the Single Query Track. Chart
Results were generated on 2025-08-11
Benchmarks: 10232
Time Limit: 1200 seconds
Memory Limit: 30720 GB
Logics: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 | 6722 | 268105.11 | 268967.71 | 6722 | 712 | 6010 | 3510 | 0 | 3136 | 1 |
iProver v3.9.3 | 0 | 3992 | 393224.91 | 103781.36 | 4511 | 0 | 4511 | 5721 | 0 | 5682 | 39 |
SMTInterpol | 0 | 2924 | 22955.33 | 15345.68 | 2924 | 80 | 2844 | 7308 | 0 | 3404 | 0 |
UltimateEliminator+MathSAT | 0 | 619 | 9612.56 | 8253.36 | 619 | 434 | 185 | 6341 | 3272 | 476 | 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 | 6722 | 268105.11 | 268967.71 | 6722 | 712 | 6010 | 3510 | 0 | 3136 | 1 |
iProver v3.9.3 | 0 | 4511 | 1893686.16 | 481584.81 | 4511 | 0 | 4511 | 5721 | 0 | 5682 | 39 |
SMTInterpol | 0 | 2924 | 22955.33 | 15345.68 | 2924 | 80 | 2844 | 7308 | 0 | 3404 | 0 |
UltimateEliminator+MathSAT | 0 | 619 | 9612.56 | 8253.36 | 619 | 434 | 185 | 6341 | 3272 | 476 | 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 | 712 | 31881.73 | 31973.82 | 712 | 712 | 0 | 81 | 9439 | 5 | 0 |
UltimateEliminator+MathSAT | 0 | 434 | 8600.11 | 7645.99 | 434 | 434 | 0 | 359 | 9439 | 236 | 0 |
SMTInterpol | 0 | 80 | 56.08 | 45.04 | 80 | 80 | 0 | 713 | 9439 | 59 | 0 |
iProver v3.9.3 | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 793 | 9439 | 793 | 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 | 6010 | 236223.38 | 236993.89 | 6010 | 0 | 6010 | 371 | 3851 | 297 | 1 |
iProver v3.9.3 | 0 | 4511 | 1893686.16 | 481584.81 | 4511 | 0 | 4511 | 1870 | 3851 | 1831 | 39 |
SMTInterpol | 0 | 2844 | 22899.25 | 15300.64 | 2844 | 0 | 2844 | 3537 | 3851 | 1762 | 0 |
UltimateEliminator+MathSAT | 0 | 185 | 1012.45 | 607.37 | 185 | 0 | 185 | 3244 | 6803 | 148 | 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 | 5875 | 4500.96 | 5224.86 | 5875 | 642 | 5233 | 362 | 3995 | 0 | 0 |
iProver v3.9.3 | 0 | 3116 | 39898.25 | 12635.10 | 3116 | 0 | 3116 | 0 | 7116 | 0 | 0 |
SMTInterpol | 0 | 2876 | 9704.94 | 4353.16 | 2876 | 80 | 2796 | 2700 | 4656 | 0 | 0 |
UltimateEliminator+MathSAT | 0 | 590 | 3617.73 | 2332.73 | 590 | 407 | 183 | 5806 | 3836 | 0 | 0 |