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