Download

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

Sources

For this evaluation we took all examples from the Termination Problem Database '04 with a strategy annotation and deleted the strategy information (i.e., now one had to prove or disprove full termination instead of "innermost"' or "context-sensitive" termination).

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

Results

Example AProVE 1.2 AProVE 1.1d
TRS/nontermin/AG01/#4.12a.trs (Submit) !0.35 !0.8
TRS/nontermin/AG01/#4.2.trs (Submit) !0.29 !0.61
TRS/nontermin/AG01/#4.3.trs (Submit) !0.24 !0.45
TRS/nontermin/AG01/#4.4.trs (Submit) !0.33 !0.46
TRS/nontermin/AG01/#4.7.trs (Submit) !0.27 !0.52
TRS/nontermin/AG01/#4.20a.trs (Submit) *0.31 *0.31
TRS/nontermin/AG01/#4.30a.trs (Submit) *0.45 *0.63
TRS/nontermin/AG01/#4.30b.trs (Submit) *7.4 *11.05
TRS/nontermin/AG01/#4.30c.trs (Submit) *7.57 &infty;
TRS/nontermin/AG01/#4.37a.trs (Submit) *0.27 *0.55
TRS/nontermin/AG01/#4.13.trs (Submit) -20.70 -10.52
TRS/nontermin/AG01/#4.14.trs (Submit) !0.26 !0.57
TRS/nontermin/AG01/#4.15.trs (Submit) !0.38 !0.65
TRS/nontermin/AG01/#4.16.trs (Submit) !0.24 !0.46
TRS/nontermin/AG01/#4.17.trs (Submit) !0.41 !0.63
TRS/nontermin/AG01/#4.18.trs (Submit) !2.12 !1.06
TRS/nontermin/AG01/#4.19.trs (Submit) -21.13 -13.95
TRS/nontermin/AG01/#4.20.trs (Submit) *0.24 *0.31
TRS/nontermin/AG01/#4.21.trs (Submit) *0.29 *0.32
TRS/nontermin/AG01/#4.22.trs (Submit) *0.23 *0.5
TRS/nontermin/AG01/#4.23.trs (Submit) *0.45 *0.62
TRS/nontermin/AG01/#4.25.trs (Submit) *0.16 *0.4
TRS/nontermin/AG01/#4.26.trs (Submit) *6.70 *10.98
TRS/nontermin/AG01/#4.27.trs (Submit) *0.44 *0.62
TRS/nontermin/AG01/#4.28.trs (Submit) *1.28 *0.84
TRS/nontermin/AG01/#4.29.trs (Submit) *7.27 *11.13
TRS/nontermin/AG01/#4.30.trs (Submit) *6.80 *10.85
TRS/nontermin/AG01/#4.31.trs (Submit) *15.96 *10.91
TRS/nontermin/AG01/#4.32.trs (Submit) *0.21 *0.5
TRS/nontermin/AG01/#4.33.trs (Submit) *0.54 *0.76
TRS/nontermin/AG01/#4.34.trs (Submit) *0.46 *0.68
TRS/nontermin/AG01/#4.35.trs (Submit) *3.16 *2.48
TRS/nontermin/AG01/#4.36.trs (Submit) *1.95 *1.67
TRS/nontermin/AG01/#4.37.trs (Submit) *0.22 *0.5
TRS/nontermin/CSR/Ex49_GM04.trs (Submit) *0.44 *0.64
TRS/nontermin/CSR/Ex5_7_Luc97.trs (Submit) !1.82 !0.83
TRS/nontermin/CSR/ExIntrod_Zan97.trs (Submit) !1.59 !0.65
TRS/nontermin/CSR/Ex1_2_Luc02c.trs (Submit) !1.25 !0.44
TRS/nontermin/CSR/ExIntrod_GM01.trs (Submit) !4.5 !0.59
TRS/nontermin/CSR/ExIntrod_GM04.trs (Submit) !3.92 !0.54
TRS/nontermin/CSR/Ex5_Zan97.trs (Submit) !1.22 !0.46
TRS/nontermin/CSR/Ex1_Zan97.trs (Submit) !0.91 !0.8
TRS/nontermin/CSR/ExConc_Zan97.trs (Submit) !0.59 !0.63
TRS/nontermin/CSR/Ex4_7_15_Bor03.trs (Submit) !2.12 !0.53
TRS/nontermin/CSR/Ex24_GM04.trs (Submit) !0.27 !0.5
TRS/nontermin/CSR/ExIntrod_GM99.trs (Submit) !1.88 !0.73
TRS/nontermin/CSR/Ex6_Luc98.trs (Submit) !1.33 !0.47
TRS/nontermin/CSR/Ex4_Zan97.trs (Submit) !0.64 !0.54
TRS/nontermin/CSR/Ex4_7_77_Bor03.trs (Submit) !3.60 !0.41
TRS/nontermin/CSR/Ex9_BLR02.trs (Submit) !1.53 !0.65
TRS/nontermin/CSR/Ex4_7_56_Bor03.trs (Submit) !1.27 !0.46
TRS/nontermin/CSR/Ex26_Luc03b.trs (Submit) !1.63 !0.66
TRS/nontermin/CSR/Ex15_Luc98.trs (Submit) !1.47 !0.57
TRS/nontermin/CSR/Ex1_GL02a.trs (Submit) !1.42 !0.59
TRS/nontermin/CSR/Ex1_Luc02b.trs (Submit) !1.33 !0.52
TRS/nontermin/CSR/Ex6_9_Luc02c.trs (Submit) !1.29 !0.47
TRS/nontermin/CSR/ExAppendixB_AEL03.trs (Submit) !1.77 !0.87
TRS/nontermin/CSR/Ex3_3_25_Bor03.trs (Submit) !1.44 !0.59
TRS/nontermin/CSR/Ex1_2_AEL03.trs (Submit) !1.67 !0.73
TRS/nontermin/CSR/Ex3_12_Luc96a.trs (Submit) !1.27 !0.46
TRS/nontermin/CSR/Ex8_BLR02.trs (Submit) !0.41 !0.58
TRS/nontermin/CSR/Ex1_GM03.trs (Submit) !0.44 !0.6
TRS/nontermin/CSR/Ex14_AEGL02.trs (Submit) !1.29 !0.48
TRS/nontermin/CSR/Ex2_Luc03b.trs (Submit) !1.43 !0.54
TRS/nontermin/CSR/Ex1_GM99.trs (Submit) !0.21 !0.44
TRS/nontermin/CSR/Ex6_15_AEL02.trs (Submit) !2.14 !1.01
TRS/nontermin/CSR/Ex3_2_Luc97.trs (Submit) !1.52 !0.62
TRS/nontermin/CSR/Ex4_4_Luc96b.trs (Submit) !0.29 !0.52
TRS/nontermin/CSR/Ex6_GM04.trs (Submit) !0.75 !0.63
TRS/nontermin/CSR/Ex7_BLR02.trs (Submit) !1.37 !0.54
TRS/nontermin/CSR/Ex4_7_37_Bor03.trs (Submit) !1.62 !0.7
TRS/nontermin/HM/n001.trs (Submit) !1.76 !1.18
TRS/nontermin/Rubio-inn/test830.trs (Submit) *0.18 *0.42
TRS/nontermin/Rubio-inn/test10.trs (Submit) !0.51 !0.59
TRS/nontermin/Rubio-inn/bn111.trs (Submit) -7.23 -10.67
TRS/nontermin/Rubio-inn/muladd.trs (Submit) !0.38 !0.57
TRS/nontermin/Rubio-inn/test75.trs (Submit) !0.29 !0.79
TRS/nontermin/Rubio-inn/test76.trs (Submit) !2.82 -11.45
TRS/nontermin/Rubio-inn/test77.trs (Submit) -60.4 -10.82
TRS/nontermin/Rubio-inn/gkg.trs (Submit) !0.25 !0.47
TRS/nontermin/Rubio-inn/toyama.trs (Submit) !0.22 !0.47
TRS/nontermin/Rubio-inn/test9.trs (Submit) !0.38 !0.94
TRS/nontermin/TRCSR/ExSec11_1_Luc02a.trs (Submit) !1.74 !0.77
TRS/nontermin/cariboo/ex1.trs (Submit) !1.7 !0.79
TRS/nontermin/cariboo/ex2.trs (Submit) !1.27 !0.48
TRS/nontermin/cariboo/ex3.trs (Submit) !0.78 !0.7
TRS/nontermin/cariboo/ex4.trs (Submit) !1.42 !0.84
TRS/nontermin/cariboo/ex5.trs (Submit) !0.92 !0.45
TRS/nontermin/cariboo/ex6.trs (Submit) !0.32 !0.56
TRS/nontermin/cariboo/tricky1.trs (Submit) *0.19 *24.05

Statistics

AProVE 1.2 AProVE 1.1d
Yes () 25 24
Failure () 4 5
No () 61 60
Timeout () 0 1
Error () 0 0
Total 90 90