MAYBE Time: 0.475410 TRS: { g(x, x) -> g(a(), 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: DP: { g#(x, x) -> g#(a(), 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} TRS: { g(x, x) -> g(a(), 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#(x, x) -> g#(a(), b()), g#(x, x) -> g#(a(), b())) (g#(d(), g(d(), x)) -> g#(c(), g(e(), x)), g#(c(), g(c(), x)) -> g#(d(), x)) (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#(x, x) -> g#(a(), b())) (f# g(x, y) -> g#(f f x, a()), g#(x, x) -> g#(a(), b())) (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, x) -> g#(a(), 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, x) -> g#(a(), 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#(e(), x), g#(x, x) -> g#(a(), 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)) (f# g(x, y) -> g#(y, g(f f x, a())), g#(x, x) -> g#(a(), b())) (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)) (g#(c(), g(c(), x)) -> g#(e(), g(d(), x)), g#(x, x) -> g#(a(), 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#(e(), g(e(), x)) -> g#(c(), x)) (g#(e(), g(e(), x)) -> g#(d(), g(c(), x)), g#(x, x) -> g#(a(), b())) (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#(d(), g(d(), x)) -> g#(c(), g(e(), 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)} STATUS: arrows: 0.710744 SCCS (3): Scc: {f# g(x, y) -> f# x, f# g(x, y) -> f# f x} Scc: {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: {g#(x, x) -> g#(a(), b())} SCC (2): Strict: {f# g(x, y) -> f# x, f# g(x, y) -> f# f x} Weak: { g(x, x) -> g(a(), 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 (6): Strict: {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, x) -> g(a(), 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: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [g](x0, x1) = x0 + 1, [f](x0) = 0, [a] = 1, [b] = 0, [e] = 0, [d] = 0, [c] = 0, [g#](x0, x1) = x0 Strict: g#(c(), g(c(), x)) -> g#(d(), x) 1 + 1x >= 0 + 1x g#(c(), g(c(), x)) -> g#(e(), g(d(), x)) 1 + 1x >= 1 + 1x g#(d(), g(d(), x)) -> g#(c(), g(e(), x)) 1 + 1x >= 1 + 1x g#(d(), g(d(), x)) -> g#(e(), x) 1 + 1x >= 0 + 1x g#(e(), g(e(), x)) -> g#(c(), x) 1 + 1x >= 0 + 1x g#(e(), g(e(), x)) -> g#(d(), g(c(), x)) 1 + 1x >= 1 + 1x Weak: f g(x, y) -> g(y, g(f f x, a())) 0 + 0x + 0y >= 3 + 0x + 0y g(c(), g(c(), x)) -> g(e(), g(d(), x)) 2 + 1x >= 2 + 1x g(d(), g(d(), x)) -> g(c(), g(e(), x)) 2 + 1x >= 2 + 1x g(e(), g(e(), x)) -> g(d(), g(c(), x)) 2 + 1x >= 2 + 1x g(x, x) -> g(a(), b()) 1 + 1x >= 1 SCCS (1): 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 (3): 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, x) -> g(a(), 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 (1): Strict: {g#(x, x) -> g#(a(), b())} Weak: { g(x, x) -> g(a(), 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