Reducing Relative Termination to Dependency Pair Problems

This page suppliments the experimental results of this paper. Please scroll down to 'Details' for the used benchmark files and execution logs (i.e., proofs).

Please choose a benchmark set:

Summary

counting...

Details

Problem TC2014 MAT2b MAT3b Basic Extension Removal Usable WithMAT3b WithMAT3b+Usable AProVE ttt2
Mixed_relative_TRS/abp.trs MAYBE 0.23 3.58 0.07 18.72 18.95 18.67 60.01 60.01 66.49 59.63
Mixed_relative_TRS/abp2.trs MAYBE 0.22 4.28 0.00 1.69 1.91 1.91 13.33 13.30 66.95 59.28
Mixed_relative_TRS/assoc.trs NO 0.01 0.01 0.00 0.06 0.08 0.08 0.11 0.11 2.21 59.28
Mixed_relative_TRS/carbridge.trs YES 0.26 0.96 0.00 0.48 0.27 0.27 0.27 0.27 3.18 59.26
Mixed_relative_TRS/gcd.trs MAYBE 0.07 0.37 0.00 0.04 0.11 0.11 0.48 0.48 64.56 59.25
Mixed_relative_TRS/gcd_list.trs MAYBE 0.16 0.94 0.59 0.45 0.61 0.61 60.03 60.02 60.67 59.25
Mixed_relative_TRS/gcd_many.trs NO 0.07 0.20 0.00 0.14 0.22 0.22 0.64 0.64 1.96 0.27
Mixed_relative_TRS/ijcar2006.trs YES 0.01 0.02 0.00 0.05 0.02 0.02 0.02 0.02 2.65 1.03
Mixed_relative_TRS/relsubst.trs MAYBE 0.01 0.03 0.00 0.08 0.10 0.10 0.12 0.12 64.27 59.22
Mixed_relative_TRS/rt-rw4.trs YES 4.16 49.63 0.00 7.40 1.20 1.19 1.19 1.20 9.70 59.27
Mixed_relative_TRS/trafic.trs YES 2.26 2.03 0.00 1.62 0.78 0.77 0.78 0.78 12.34 59.28
Relative_05/rt1-1.trs YES 0.01 0.01 0.01 0.00 0.01 0.01 0.01 0.01 2.16 0.45
Relative_05/rt1-2.trs YES 0.01 0.01 0.00 0.03 0.01 0.01 0.01 0.01 2.22 0.46
Relative_05/rt1-3.trs YES 0.02 0.06 0.00 0.00 0.01 0.01 0.01 0.01 1.83 1.58
Relative_05/rt1-4.trs YES 0.02 0.06 0.00 0.06 0.03 0.03 0.03 0.03 2.10 1.51
Relative_05/rt1-5.trs YES 0.02 0.09 0.00 0.07 0.01 0.01 0.01 0.01 2.29 3.05
Relative_05/rt2-1.trs YES 0.01 0.02 0.00 0.04 0.01 0.01 0.01 0.01 2.07 0.71
Relative_05/rt2-2.trs YES 0.01 0.01 0.00 0.02 0.01 0.01 0.01 0.01 2.10 0.45
Relative_05/rt2-3.trs YES 0.02 0.03 0.00 0.02 0.03 0.03 0.03 0.03 1.98 0.63
Relative_05/rt2-4.trs YES 0.01 0.03 0.00 0.02 0.02 0.02 0.02 0.02 2.26 0.78
Relative_05/rt2-5.trs YES 0.02 0.05 0.00 0.03 0.02 0.02 0.02 0.02 2.22 1.27
Relative_05/rt2-7.trs YES 0.02 0.05 0.01 0.01 0.03 0.03 0.07 0.07 3.30 1.82
Relative_05/rt2-8.trs NO 0.07 0.14 0.00 0.02 0.10 0.10 0.14 0.14 2.04 59.25
Relative_05/rt3-1.trs YES 0.01 0.03 0.00 0.10 0.02 0.02 0.02 0.02 2.59 0.67
Relative_05/rt3-2.trs YES 0.02 0.05 0.00 0.04 0.02 0.02 0.02 0.02 2.23 1.23
Relative_05/rt3-3.trs NO 0.02 0.05 0.00 0.03 0.04 0.04 0.07 0.07 1.93 59.24
Relative_05/rt3-4.trs YES 0.01 0.02 0.00 0.08 0.10 0.10 0.12 0.12 22.37 59.29
Relative_05/rt3-5.trs YES 0.03 0.08 0.00 0.08 0.11 0.11 0.11 0.11 5.69 3.94
Relative_05/rt3-6.trs NO 0.01 0.03 0.00 0.03 0.05 0.05 0.10 0.11 1.97 0.27
Relative_05/rt3-7.trs YES 0.02 0.05 0.00 0.06 0.03 0.03 0.03 0.03 2.61 1.46
Relative_05/rt3-8.trs NO 0.02 0.05 0.00 0.33 0.35 0.35 0.42 0.42 2.00 0.27
Relative_05/rt3-9.trs YES 0.04 0.08 0.00 0.02 0.05 0.05 0.05 0.05 2.61 3.30
Relative_05/rtL-cbn1.trs YES 0.41 2.04 0.00 0.43 0.68 0.68 6.24 6.24 12.47 59.23
Relative_05/rtL-cbn5.trs YES 0.90 60.01 0.00 2.00 2.91 2.91 60.00 60.04 10.69 59.25
Relative_05/rtL-cbo.trs MAYBE 0.17 0.45 0.00 0.22 0.28 0.28 0.52 0.52 62.02 59.31
Relative_05/rtL-evnz.trs NO 0.93 60.00 0.00 0.52 1.43 1.43 60.04 60.00 31.13 59.25
Relative_05/rtL-evo.trs NO 0.61 55.70 0.00 0.23 0.53 0.53 60.00 60.02 2.55 0.60
Relative_05/rtL-me2.trs YES 0.02 0.03 0.00 0.10 0.01 0.01 0.01 0.01 2.80 3.68
Relative_05/rtL-me3.trs YES 0.08 0.18 0.00 0.38 0.01 0.01 0.01 0.01 3.37 59.26
Relative_05/rtL-pwl.trs YES 0.51 44.20 0.00 1.13 1.21 1.21 60.00 60.03 11.12 59.26
Relative_05/rtL-rw2.trs MAYBE 2.29 60.03 0.00 0.87 5.69 5.69 60.04 60.03 62.22 59.26
Relative_05/rtL-rw5.trs MAYBE 3.71 60.01 0.00 0.04 3.76 3.75 60.01 60.00 69.41 59.26
Relative_05/rtL-wl1nz.trs YES 0.04 0.26 0.08 0.08 0.11 0.11 0.12 0.12 2.92 3.15
Relative_05/rtL-wl1o.trs MAYBE 0.05 0.09 0.05 0.05 0.08 0.08 0.23 0.23 60.41 59.23
MAT2b MAT3b Basic Extension Removal Usable WithMAT3b WithMAT3b+Usable AProVE ttt2
YES # 21 23 4 6 24 24 25 25 27 19
time 7.07 53.82 0.1 1.86 4.72 4.7 16.31 16.29 133.87 31.17
avr. 0.337 2.34 0.025 0.31 0.197 0.196 0.652 0.652 4.958 1.641
NO # 0 0 0 0 0 0 0 0 8 4
time 45.79 1.41
avr. 5.724 0.353
MAYBE # 23 17 40 38 20 20 11 11 0 21
time 10.53 112.18 0.71 36.01 37.29 37 9.07 9.08 1244.81
avr. 0.458 6.599 0.018 0.948 1.865 1.85 0.825 0.825 59.277
TIMEOUT # 0 4 0 0 0 0 8 8 9 0
time 240.05 480.13 480.15 577
avr. 60.013 60.016 60.019 64.111
NEWS # 0 0 0 2 2 2 2 2 0 0
Total # 44 44 44 44 44 44 44 44 44 44
time 17.6 406.05 0.81 37.87 42.01 41.7 505.51 505.52 756.66 1277.39
avr. 0.4 9.228 0.018 0.861 0.955 0.948 11.489 11.489 17.197 29.032