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