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