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