Benchmarks on Context-Sensitive TRSs

Table 1 shows a summary of results of VMTL on a set of conditional TRSs, some of which are particularly challenging. All conditional TRS from the termination problem database are included in this collection of examples. Note that in this section non-termination means non-termination of the transformed TRS obtained by the conditional TRS through a transformation. A time limit of 60 seconds was used.

Number of TRSsProved Terminating Proved Non-terminatingMaybe Timeout
27 17 3 4 3
Table 1: VMTL Benchmark Summary.

Table 2 provides details on these experiments.

Last Update: January 31, 2009
Contact: vmtl@logic.at