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