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