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 | 1362 (1137 YES, 225 NO) | 1425 (1207 YES, 218 NO) | 1454 (1227 YES, 227 NO) |
| Failures | 1433 (1020 timeouts) | 1370 (1038 timeouts) | |
| Time (termination tool) | 19h 46m 7s | 20h 19m 19s | |
| Accepted | 1361 | 1424 | 1453 |
| Rejected | 1 | 1 | |
| Unsupported | 0 | 0 | |
| Time (certification) | 0h 0m 56s | 0h 2m 35s |