Download

You can download the example collection used below as an archive.

Sources

The following table lists the origin of the examples.

Directory name Source
D33 Nachum Dershowitz, 33 Examples of Termination, Proc. French Spring School of Theoretical Computer Science, Lecture Notes in Computer Science 909, 1995.
AG01 Thomas Arts and Jürgen Giesl, A Collection of Examples for Termination of Term Rewriting Using Dependency Pairs, Technical Report AIB-2001-09, RWTH Aachen, Germany.
Ste92 Joachim Steinbach, Automatic Termination Proofs With Transformation Orderings Proc. of the 6th RTA, LNCS 914, 1995.

Results

Example AProVE 1.2 AProVE 1.1d
TRS/uncurried/AG01/#4.2.trs (Submit) *0.12 *0.44
TRS/uncurried/AG01/#4.3.trs (Submit) *0.9 *0.36
TRS/uncurried/AG01/#4.5.trs (Submit) *0.22 *0.64
TRS/uncurried/AG01/#4.7.trs (Submit) *0.10 *0.37
TRS/uncurried/AG01/#4.8.trs (Submit) *0.29 *0.46
TRS/uncurried/AG01/#4.10.trs (Submit) *0.5 *0.35
TRS/uncurried/AG01/#4.13.trs (Submit) *0.14 *0.41
TRS/uncurried/AG01/#4.15.trs (Submit) *0.13 *0.43
TRS/uncurried/AG01/#4.17.trs (Submit) *0.16 *0.47
TRS/uncurried/AG01/#4.19.trs (Submit) *0.29 *0.56
TRS/uncurried/AG01/#4.22.trs (Submit) *0.24 *0.55
TRS/uncurried/AG01/#4.24.trs (Submit) *0.52 *0.73
TRS/uncurried/AG01/#4.26.trs (Submit) *6.70 *11.26
TRS/uncurried/AG01/#4.28.trs (Submit) *1.26 *0.89
TRS/uncurried/AG01/#4.34.trs (Submit) *0.46 *0.69
TRS/uncurried/AG01/#4.36.trs (Submit) *1.95 *1.69
TRS/uncurried/AG01/#3.2.trs (Submit) *0.36 *0.58
TRS/uncurried/AG01/#3.6.trs (Submit) *0.79 *0.97
TRS/uncurried/AG01/#3.8.trs (Submit) *0.51 *0.71
TRS/uncurried/AG01/#3.10.trs (Submit) *2.56 *2.55
TRS/uncurried/AG01/#3.13.trs (Submit) *1.73 *1.54
TRS/uncurried/AG01/#3.16.trs (Submit) *0.26 *0.56
TRS/uncurried/AG01/#3.18.trs (Submit) *0.47 *0.69
TRS/uncurried/AG01/#3.22.trs (Submit) *0.43 *10.96
TRS/uncurried/AG01/#3.25.trs (Submit) *0.79 *0.49
TRS/uncurried/AG01/#3.27.trs (Submit) *1.75 *2.91
TRS/uncurried/AG01/#3.32.trs (Submit) *0.24 *0.31
TRS/uncurried/AG01/#3.36.trs (Submit) *0.52 *0.79
TRS/uncurried/AG01/#3.38.trs (Submit) *0.49 *0.71
TRS/uncurried/AG01/#3.40.trs (Submit) *0.78 *1.06
TRS/uncurried/AG01/#3.45.trs (Submit) *0.17 *0.44
TRS/uncurried/AG01/#3.48.trs (Submit) *0.28 *0.69
TRS/uncurried/AG01/#3.52.trs (Submit) *0.16 *0.5
TRS/uncurried/AG01/#3.55.trs (Submit) *2.0 *1.61
TRS/uncurried/AG01/#3.57.trs (Submit) *0.91 *1.09
TRS/uncurried/D33/01.trs (Submit) *0.15 *0.4
TRS/uncurried/D33/02.trs (Submit) *0.12 *0.39
TRS/uncurried/D33/06.trs (Submit) *0.41 *0.33
TRS/uncurried/D33/08.trs (Submit) *0.34 *0.7
TRS/uncurried/D33/11.trs (Submit) *0.93 *1.21
TRS/uncurried/D33/12.trs (Submit) *0.31 *0.65
TRS/uncurried/D33/13.trs (Submit) *6.71 *10.86
TRS/uncurried/D33/17.trs (Submit) *0.17 *0.47
TRS/uncurried/D33/18.trs (Submit) *0.18 *0.44
TRS/uncurried/D33/21.trs (Submit) *0.37 *0.58
TRS/uncurried/D33/29.trs (Submit) *0.21 *0.58
TRS/uncurried/D33/30.trs (Submit) *0.33 &infty;
TRS/uncurried/D33/31.trs (Submit) *0.23 *0.55
TRS/uncurried/D33/33.trs (Submit) -60.2 &infty;
TRS/uncurried/Ste92/motivation.trs (Submit) *0.24 *0.52
TRS/uncurried/Ste92/perfect.trs (Submit) *0.31 *0.71
TRS/uncurried/Ste92/minsort.trs (Submit) &infty; &infty;
TRS/uncurried/Ste92/hydra.trs (Submit) *0.21 *0.56
TRS/uncurried/Ste92/perfect2.trs (Submit) *0.78 *1.07

Statistics

AProVE 1.2 AProVE 1.1d
Yes () 52 51
Failure () 1 0
No () 0 0
Timeout () 1 3
Error () 0 0
Total 54 54