MAYBE TRS: {g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b()))), g(e(), g(e(), x)) -> g(d(), g(c(), x)), g(d(), g(d(), x)) -> g(c(), g(e(), x)), g(c(), g(c(), x)) -> g(e(), g(d(), x)), f(g(x, y)) -> g(y, g(f(f(x)), a()))} DP: Strict: {g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(x, g(y, g(x, y))) -> g#(y, b()), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(e(), g(e(), x)) -> g#(c(), x), g#(d(), g(d(), x)) -> g#(e(), x), g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(c(), g(c(), x)) -> g#(d(), x), f#(g(x, y)) -> g#(y, g(f(f(x)), a())), f#(g(x, y)) -> g#(f(f(x)), a()), f#(g(x, y)) -> f#(x), f#(g(x, y)) -> f#(f(x))} Weak: {g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b()))), g(e(), g(e(), x)) -> g(d(), g(c(), x)), g(d(), g(d(), x)) -> g(c(), g(e(), x)), g(c(), g(c(), x)) -> g(e(), g(d(), x)), f(g(x, y)) -> g(y, g(f(f(x)), a()))} EDG: {(g#(e(), g(e(), x)) -> g#(c(), x), g#(c(), g(c(), x)) -> g#(d(), x)) (g#(e(), g(e(), x)) -> g#(c(), x), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))) (g#(e(), g(e(), x)) -> g#(c(), x), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(e(), g(e(), x)) -> g#(c(), x), g#(x, g(y, g(x, y))) -> g#(y, b())) (g#(e(), g(e(), x)) -> g#(c(), x), g#(x, g(y, g(x, y))) -> g#(x, g(y, b()))) (g#(c(), g(c(), x)) -> g#(d(), x), g#(d(), g(d(), x)) -> g#(c(), g(e(), x))) (g#(c(), g(c(), x)) -> g#(d(), x), g#(d(), g(d(), x)) -> g#(e(), x)) (g#(c(), g(c(), x)) -> g#(d(), x), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(c(), g(c(), x)) -> g#(d(), x), g#(x, g(y, g(x, y))) -> g#(y, b())) (g#(c(), g(c(), x)) -> g#(d(), x), g#(x, g(y, g(x, y))) -> g#(x, g(y, b()))) (g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(c(), g(c(), x)) -> g#(d(), x)) (g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))) (g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(d(), g(d(), x)) -> g#(c(), g(e(), x))) (g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(d(), g(d(), x)) -> g#(e(), x)) (g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(e(), g(e(), x)) -> g#(c(), x)) (g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(e(), g(e(), x)) -> g#(d(), g(c(), x))) (g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(d(), g(d(), x)) -> g#(c(), g(e(), x))) (g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(d(), g(d(), x)) -> g#(e(), x)) (g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(x, g(y, g(x, y))) -> g#(y, b())) (g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(x, g(y, g(x, y))) -> g#(x, g(y, b()))) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(e(), g(e(), x)) -> g#(c(), x)) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(e(), g(e(), x)) -> g#(d(), g(c(), x))) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(x, g(y, g(x, y))) -> g#(y, b())) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(x, g(y, g(x, y))) -> g#(x, g(y, b()))) (f#(g(x, y)) -> f#(f(x)), f#(g(x, y)) -> g#(y, g(f(f(x)), a()))) (f#(g(x, y)) -> f#(f(x)), f#(g(x, y)) -> g#(f(f(x)), a())) (f#(g(x, y)) -> f#(f(x)), f#(g(x, y)) -> f#(x)) (f#(g(x, y)) -> f#(f(x)), f#(g(x, y)) -> f#(f(x))) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(x, g(y, g(x, y))) -> g#(x, g(y, b()))) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(x, g(y, g(x, y))) -> g#(y, b())) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(d(), x)) (f#(g(x, y)) -> g#(y, g(f(f(x)), a())), g#(e(), g(e(), x)) -> g#(d(), g(c(), x))) (f#(g(x, y)) -> g#(y, g(f(f(x)), a())), g#(e(), g(e(), x)) -> g#(c(), x)) (f#(g(x, y)) -> g#(y, g(f(f(x)), a())), g#(d(), g(d(), x)) -> g#(e(), x)) (f#(g(x, y)) -> g#(y, g(f(f(x)), a())), g#(d(), g(d(), x)) -> g#(c(), g(e(), x))) (f#(g(x, y)) -> g#(y, g(f(f(x)), a())), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))) (f#(g(x, y)) -> g#(y, g(f(f(x)), a())), g#(c(), g(c(), x)) -> g#(d(), x)) (f#(g(x, y)) -> f#(x), f#(g(x, y)) -> g#(y, g(f(f(x)), a()))) (f#(g(x, y)) -> f#(x), f#(g(x, y)) -> g#(f(f(x)), a())) (f#(g(x, y)) -> f#(x), f#(g(x, y)) -> f#(x)) (f#(g(x, y)) -> f#(x), f#(g(x, y)) -> f#(f(x))) (g#(d(), g(d(), x)) -> g#(e(), x), g#(x, g(y, g(x, y))) -> g#(x, g(y, b()))) (g#(d(), g(d(), x)) -> g#(e(), x), g#(x, g(y, g(x, y))) -> g#(y, b())) (g#(d(), g(d(), x)) -> g#(e(), x), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(d(), g(d(), x)) -> g#(e(), x), g#(e(), g(e(), x)) -> g#(d(), g(c(), x))) (g#(d(), g(d(), x)) -> g#(e(), x), g#(e(), g(e(), x)) -> g#(c(), x)) (g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(x, g(y, g(x, y))) -> g#(x, g(y, b()))) (g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(x, g(y, g(x, y))) -> g#(y, b())) (g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))))} SCCS: Scc: {f#(g(x, y)) -> f#(x), f#(g(x, y)) -> f#(f(x))} Scc: {g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(e(), g(e(), x)) -> g#(c(), x), g#(d(), g(d(), x)) -> g#(e(), x), g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(c(), g(c(), x)) -> g#(d(), x)} SCC: Strict: {f#(g(x, y)) -> f#(x), f#(g(x, y)) -> f#(f(x))} Weak: {g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b()))), g(e(), g(e(), x)) -> g(d(), g(c(), x)), g(d(), g(d(), x)) -> g(c(), g(e(), x)), g(c(), g(c(), x)) -> g(e(), g(d(), x)), f(g(x, y)) -> g(y, g(f(f(x)), a()))} Fail SCC: Strict: {g#(x, g(y, g(x, y))) -> g#(x, g(y, b())), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(e(), g(e(), x)) -> g#(c(), x), g#(d(), g(d(), x)) -> g#(e(), x), g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(c(), g(c(), x)) -> g#(d(), x)} Weak: {g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b()))), g(e(), g(e(), x)) -> g(d(), g(c(), x)), g(d(), g(d(), x)) -> g(c(), g(e(), x)), g(c(), g(c(), x)) -> g(e(), g(d(), x)), f(g(x, y)) -> g(y, g(f(f(x)), a()))} POLY: Argument Filtering: pi(b) = [], pi(a) = [], pi(f) = [], pi(c) = [], pi(d) = [], pi(e) = [], pi(g#) = 1, pi(g) = [1] Usable Rules: {} Interpretation: [g](x0) = x0 + 1, [b] = 0 Strict: {g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))} Weak: {g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b()))), g(e(), g(e(), x)) -> g(d(), g(c(), x)), g(d(), g(d(), x)) -> g(c(), g(e(), x)), g(c(), g(c(), x)) -> g(e(), g(d(), x)), f(g(x, y)) -> g(y, g(f(f(x)), a()))} EDG: {(g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(d(), g(d(), x)) -> g#(c(), g(e(), x))) (g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(e(), g(e(), x)) -> g#(d(), g(c(), x))) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))) (g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))), g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b()))))} SCCS: Scc: {g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))} Scc: {g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))} SCC: Strict: {g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(e(), g(d(), x))} Weak: {g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b()))), g(e(), g(e(), x)) -> g(d(), g(c(), x)), g(d(), g(d(), x)) -> g(c(), g(e(), x)), g(c(), g(c(), x)) -> g(e(), g(d(), x)), f(g(x, y)) -> g(y, g(f(f(x)), a()))} Fail SCC: Strict: {g#(x, g(y, g(x, y))) -> g#(a(), g(x, g(y, b())))} Weak: {g(x, g(y, g(x, y))) -> g(a(), g(x, g(y, b()))), g(e(), g(e(), x)) -> g(d(), g(c(), x)), g(d(), g(d(), x)) -> g(c(), g(e(), x)), g(c(), g(c(), x)) -> g(e(), g(d(), x)), f(g(x, y)) -> g(y, g(f(f(x)), a()))} Fail