YES Time: 0.001801 TRS: {f(x, f(a(), a())) -> f(f(f(f(a(), a()), a()), x), a())} DP: DP: {f#(x, f(a(), a())) -> f#(f(f(f(a(), a()), a()), x), a()), f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), x), f#(x, f(a(), a())) -> f#(f(a(), a()), a())} TRS: {f(x, f(a(), a())) -> f(f(f(f(a(), a()), a()), x), a())} EDG: {(f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), x), f#(x, f(a(), a())) -> f#(f(f(f(a(), a()), a()), x), a())) (f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), x), f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), x)) (f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), x), f#(x, f(a(), a())) -> f#(f(a(), a()), a()))} EDG: {} EDG: {} STATUS: arrows: 1.000000 SCCS (0):