MAYBE TRS: {f(x, f(a(), a())) -> f(f(f(a(), a()), a()), f(a(), x))} DP: Strict: {f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), f(a(), x)), f#(x, f(a(), a())) -> f#(f(a(), a()), a()), f#(x, f(a(), a())) -> f#(a(), x)} Weak: {f(x, f(a(), a())) -> f(f(f(a(), a()), a()), f(a(), x))} EDG: {(f#(x, f(a(), a())) -> f#(a(), x), f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), f(a(), x))) (f#(x, f(a(), a())) -> f#(a(), x), f#(x, f(a(), a())) -> f#(f(a(), a()), a())) (f#(x, f(a(), a())) -> f#(a(), x), f#(x, f(a(), a())) -> f#(a(), x)) (f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), f(a(), x)), f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), f(a(), x))) (f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), f(a(), x)), f#(x, f(a(), a())) -> f#(f(a(), a()), a())) (f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), f(a(), x)), f#(x, f(a(), a())) -> f#(a(), x))} SCCS: Scc: {f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), f(a(), x)), f#(x, f(a(), a())) -> f#(a(), x)} SCC: Strict: {f#(x, f(a(), a())) -> f#(f(f(a(), a()), a()), f(a(), x)), f#(x, f(a(), a())) -> f#(a(), x)} Weak: {f(x, f(a(), a())) -> f(f(f(a(), a()), a()), f(a(), x))} Fail