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