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