YES Time: 0.002065 TRS: {f(x, f(a(), a())) -> f(a(), f(f(f(a(), a()), a()), x))} DP: DP: {f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), x), f#(x, f(a(), a())) -> f#(f(a(), a()), a()), f#(x, f(a(), a())) -> f#(a(), f(f(f(a(), a()), a()), x))} TRS: {f(x, f(a(), a())) -> f(a(), f(f(f(a(), a()), a()), x))} UR: {f(x, f(a(), a())) -> f(a(), f(f(f(a(), a()), a()), x))} EDG: {(f#(x, f(a(), a())) -> f#(a(), f(f(f(a(), a()), a()), x)), f#(x, f(a(), a())) -> f#(a(), f(f(f(a(), a()), a()), x))) (f#(x, f(a(), a())) -> f#(a(), f(f(f(a(), a()), a()), x)), f#(x, f(a(), a())) -> f#(f(a(), a()), a())) (f#(x, f(a(), a())) -> f#(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(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())) (f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), x), f#(x, f(a(), a())) -> f#(a(), f(f(f(a(), a()), a()), x))) (f#(x, f(a(), a())) -> f#(f(a(), a()), a()), f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), x)) (f#(x, f(a(), a())) -> f#(f(a(), a()), a()), f#(x, f(a(), a())) -> f#(f(a(), a()), a())) (f#(x, f(a(), a())) -> f#(f(a(), a()), a()), f#(x, f(a(), a())) -> f#(a(), f(f(f(a(), a()), a()), x)))} EDG: {(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())) (f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), x), f#(x, f(a(), a())) -> f#(a(), f(f(f(a(), a()), a()), x)))} EDG: {} EDG: {} STATUS: arrows: 1.000000 SCCS (0):