Equality_NonLinearArith (Single Query Track)
Competition results for the Equality_NonLinearArith
division
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 9696
Time Limit: 1200 seconds
Memory Limit: 20480 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 | 6278 | 224359.348865 | 225034.625913 | 6278 | 765 | 5513 | 3418 | 0 | 3078 | 0 |
| iProver v3.9 | 0 | 3694 | 320834.988839 | 84955.24662 | 4132 | 0 | 4132 | 5564 | 0 | 5564 | 0 |
| SMTInterpol | 0 | 2873 | 27058.020967 | 17958.931411 | 2873 | 84 | 2789 | 6823 | 0 | 3819 | 86 |
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 | 6278 | 224359.348865 | 225034.625913 | 6278 | 765 | 5513 | 3418 | 0 | 3078 | 0 |
| SMTInterpol | 0 | 2873 | 27058.020967 | 17958.931411 | 2873 | 84 | 2789 | 6823 | 0 | 3819 | 86 |
| iProver v3.9 | 2 | 4130 | 1.536612437244e+06 | 392088.466758 | 4132 | 0 | 4132 | 5564 | 0 | 5564 | 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 | 765 | 30616.308149 | 30699.250066 | 765 | 765 | 0 | 84 | 8847 | 6 | 0 |
| SMTInterpol | 0 | 84 | 261.599769 | 211.705303 | 84 | 84 | 0 | 765 | 8847 | 62 | 0 |
| iProver v3.9 | 2 | 0 | 4668.448944 | 1181.564623 | 2 | 0 | 2 | 847 | 8847 | 847 | 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 | 5513 | 193743.040716 | 194335.375847 | 5513 | 0 | 5513 | 215 | 3968 | 151 | 0 |
| iProver v3.9 | 0 | 4080 | 1.453706433695e+06 | 371125.151524 | 4080 | 0 | 4080 | 1648 | 3968 | 1648 | 0 |
| SMTInterpol | 0 | 2789 | 26796.421197 | 17747.226108 | 2789 | 0 | 2789 | 2939 | 3968 | 1806 | 45 |
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 | 5543 | 3473.24676 | 4027.185312 | 5543 | 696 | 4847 | 337 | 3816 | 0 | 0 |
| iProver v3.9 | 0 | 2962 | 35841.348949 | 11356.967563 | 2962 | 0 | 2962 | 0 | 6734 | 0 | 0 |
| SMTInterpol | 0 | 2813 | 11700.055022 | 4725.257097 | 2813 | 83 | 2730 | 2475 | 4408 | 0 | 0 |