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