Download

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

Sources

The examples used in this evaluation are from the following collections. They have been translated to binary applicative form.

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.

The body of these examples was later accepted into the Termination Problem Data Base (TPDB) as the TRS/currying category.

Results

Example AProVE 1.2 AProVE 1.1d
TRS/currying/AG01/#4.2.trs (Submit) *0.16 *0.49
TRS/currying/AG01/#4.3.trs (Submit) *0.9 *0.36
TRS/currying/AG01/#4.5.trs (Submit) *0.8 *0.34
TRS/currying/AG01/#4.7.trs (Submit) *0.11 *0.46
TRS/currying/AG01/#4.8.trs (Submit) *0.36 &infty;
TRS/currying/AG01/#4.10.trs (Submit) *0.6 *0.39
TRS/currying/AG01/#4.13.trs (Submit) *0.14 *0.38
TRS/currying/AG01/#4.15.trs (Submit) *0.22 &infty;
TRS/currying/AG01/#4.17.trs (Submit) *0.25 &infty;
TRS/currying/AG01/#4.19.trs (Submit) *0.45 &infty;
TRS/currying/AG01/#4.22.trs (Submit) *0.36 -22.91
TRS/currying/AG01/#4.24.trs (Submit) *0.72 *1.64
TRS/currying/AG01/#4.26.trs (Submit) *6.85 &infty;
TRS/currying/AG01/#4.28.trs (Submit) *0.50 -31.76
TRS/currying/AG01/#4.34.trs (Submit) *0.59 &infty;
TRS/currying/AG01/#4.36.trs (Submit) *3.18 &infty;
TRS/currying/AG01/#3.2.trs (Submit) *0.49 &infty;
TRS/currying/AG01/#3.6.trs (Submit) *1.7 &infty;
TRS/currying/AG01/#3.8.trs (Submit) *0.81 &infty;
TRS/currying/AG01/#3.10.trs (Submit) *4.70 &infty;
TRS/currying/AG01/#3.13.trs (Submit) *3.79 &infty;
TRS/currying/AG01/#3.16.trs (Submit) *0.39 -13.39
TRS/currying/AG01/#3.18.trs (Submit) *0.68 &infty;
TRS/currying/AG01/#3.22.trs (Submit) *0.58 &infty;
TRS/currying/AG01/#3.25.trs (Submit) *0.33 -27.56
TRS/currying/AG01/#3.27.trs (Submit) *0.11 *0.36
TRS/currying/AG01/#3.32.trs (Submit) *0.11 *0.37
TRS/currying/AG01/#3.36.trs (Submit) *0.62 &infty;
TRS/currying/AG01/#3.38.trs (Submit) *0.72 &infty;
TRS/currying/AG01/#3.40.trs (Submit) *1.16 &infty;
TRS/currying/AG01/#3.45.trs (Submit) *0.22 *0.48
TRS/currying/AG01/#3.48.trs (Submit) *0.43 &infty;
TRS/currying/AG01/#3.52.trs (Submit) *0.25 *10.95
TRS/currying/AG01/#3.55.trs (Submit) *3.35 &infty;
TRS/currying/AG01/#3.57.trs (Submit) *1.44 &infty;
TRS/currying/D33/01.trs (Submit) *0.17 *0.41
TRS/currying/D33/02.trs (Submit) *0.15 *0.4
TRS/currying/D33/06.trs (Submit) *0.22 *0.46
TRS/currying/D33/08.trs (Submit) *0.60 *0.86
TRS/currying/D33/11.trs (Submit) *3.49 *3.39
TRS/currying/D33/12.trs (Submit) *0.47 &infty;
TRS/currying/D33/13.trs (Submit) *6.87 -29.08
TRS/currying/D33/17.trs (Submit) *0.35 *24.33
TRS/currying/D33/18.trs (Submit) *0.23 *0.74
TRS/currying/D33/21.trs (Submit) *0.47 &infty;
TRS/currying/D33/29.trs (Submit) *0.34 *15.45
TRS/currying/D33/30.trs (Submit) *0.83 &infty;
TRS/currying/D33/31.trs (Submit) *0.42 &infty;
TRS/currying/D33/33.trs (Submit) -60.29 &infty;
TRS/currying/Ste92/motivation.trs (Submit) *0.28 *0.6
TRS/currying/Ste92/perfect.trs (Submit) *0.91 &infty;
TRS/currying/Ste92/minsort.trs (Submit) -60.1 &infty;
TRS/currying/Ste92/hydra.trs (Submit) *0.31 *34.6
TRS/currying/Ste92/perfect2.trs (Submit) *2.5 &infty;

Statistics

AProVE 1.2 AProVE 1.1d
Yes () 52 21
Failure () 2 5
No () 0 0
Timeout () 0 28
Error () 0 0
Total 54 54