Introduction
We tested all 2795 TRSs of TPDB 8.0 using AProVE with two strategies that are similar to the ones which have been used during the termination competition 2010.
- no_semlab is like the competition strategy, but where semantic labeling has been removed.
- with_semlab is like the competition strategy, but where semantic labeling has been extended. (the competition strategy did not use quasi-models, but with_semlab does.)
In the result table one can click on the execution times to see the proofs and answers of CeTA (version 1.17).
Links
Color codes
| Success (Proof) |
| Success (Disproof) |
| Failure |
| Timeout |
| Accept |
| Reject |
Summary
| no_semlab | with_semlab | Total | |
|---|---|---|---|
| Examples | 2795 | 2795 | |
| Successes | 1628 (1403 YES, 225 NO) | 1677 (1459 YES, 218 NO) | 1698 (1471 YES, 227 NO) |
| Failures | 1167 (1018 timeouts) | 1118 (1042 timeouts) | |
| Time (termination tool) | 19h 48m 50s | 20h 24m 26s | |
| Accepted | 1628 | 1677 | 1698 |
| Rejected | 0 | 0 | |
| Unsupported | 0 | 0 | |
| Time (certification) | 0h 1m 32s | 0h 3m 9s |