MAYBE Time: 0.679160 TRS: { a__g(X1, X2) -> g(X1, X2), a__g(a(), X) -> a__f(b(), X), mark b() -> b(), mark a() -> a__a(), mark h X -> a__h mark X, mark g(X1, X2) -> a__g(mark X1, X2), mark f(X1, X2) -> a__f(mark X1, X2), a__h X -> a__g(mark X, X), a__h X -> h X, a__f(X, X) -> a__h a__a(), a__f(X1, X2) -> f(X1, X2), a__a() -> b(), a__a() -> a()} DP: DP: { a__g#(a(), X) -> a__f#(b(), X), mark# a() -> a__a#(), mark# h X -> mark# X, mark# h X -> a__h# mark X, mark# g(X1, X2) -> a__g#(mark X1, X2), mark# g(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> a__f#(mark X1, X2), a__h# X -> a__g#(mark X, X), a__h# X -> mark# X, a__f#(X, X) -> a__h# a__a(), a__f#(X, X) -> a__a#()} TRS: { a__g(X1, X2) -> g(X1, X2), a__g(a(), X) -> a__f(b(), X), mark b() -> b(), mark a() -> a__a(), mark h X -> a__h mark X, mark g(X1, X2) -> a__g(mark X1, X2), mark f(X1, X2) -> a__f(mark X1, X2), a__h X -> a__g(mark X, X), a__h X -> h X, a__f(X, X) -> a__h a__a(), a__f(X1, X2) -> f(X1, X2), a__a() -> b(), a__a() -> a()} EDG: {(mark# g(X1, X2) -> mark# X1, mark# f(X1, X2) -> a__f#(mark X1, X2)) (mark# g(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1) (mark# g(X1, X2) -> mark# X1, mark# g(X1, X2) -> mark# X1) (mark# g(X1, X2) -> mark# X1, mark# g(X1, X2) -> a__g#(mark X1, X2)) (mark# g(X1, X2) -> mark# X1, mark# h X -> a__h# mark X) (mark# g(X1, X2) -> mark# X1, mark# h X -> mark# X) (mark# g(X1, X2) -> mark# X1, mark# a() -> a__a#()) (mark# g(X1, X2) -> a__g#(mark X1, X2), a__g#(a(), X) -> a__f#(b(), X)) (mark# h X -> mark# X, mark# f(X1, X2) -> a__f#(mark X1, X2)) (mark# h X -> mark# X, mark# f(X1, X2) -> mark# X1) (mark# h X -> mark# X, mark# g(X1, X2) -> mark# X1) (mark# h X -> mark# X, mark# g(X1, X2) -> a__g#(mark X1, X2)) (mark# h X -> mark# X, mark# h X -> a__h# mark X) (mark# h X -> mark# X, mark# h X -> mark# X) (mark# h X -> mark# X, mark# a() -> a__a#()) (a__h# X -> a__g#(mark X, X), a__g#(a(), X) -> a__f#(b(), X)) (a__f#(X, X) -> a__h# a__a(), a__h# X -> mark# X) (a__f#(X, X) -> a__h# a__a(), a__h# X -> a__g#(mark X, X)) (mark# h X -> a__h# mark X, a__h# X -> a__g#(mark X, X)) (mark# h X -> a__h# mark X, a__h# X -> mark# X) (a__h# X -> mark# X, mark# a() -> a__a#()) (a__h# X -> mark# X, mark# h X -> mark# X) (a__h# X -> mark# X, mark# h X -> a__h# mark X) (a__h# X -> mark# X, mark# g(X1, X2) -> a__g#(mark X1, X2)) (a__h# X -> mark# X, mark# g(X1, X2) -> mark# X1) (a__h# X -> mark# X, mark# f(X1, X2) -> mark# X1) (a__h# X -> mark# X, mark# f(X1, X2) -> a__f#(mark X1, X2)) (mark# f(X1, X2) -> a__f#(mark X1, X2), a__f#(X, X) -> a__h# a__a()) (mark# f(X1, X2) -> a__f#(mark X1, X2), a__f#(X, X) -> a__a#()) (mark# f(X1, X2) -> mark# X1, mark# a() -> a__a#()) (mark# f(X1, X2) -> mark# X1, mark# h X -> mark# X) (mark# f(X1, X2) -> mark# X1, mark# h X -> a__h# mark X) (mark# f(X1, X2) -> mark# X1, mark# g(X1, X2) -> a__g#(mark X1, X2)) (mark# f(X1, X2) -> mark# X1, mark# g(X1, X2) -> mark# X1) (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1) (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> a__f#(mark X1, X2)) (a__g#(a(), X) -> a__f#(b(), X), a__f#(X, X) -> a__h# a__a()) (a__g#(a(), X) -> a__f#(b(), X), a__f#(X, X) -> a__a#())} EDG: {(mark# g(X1, X2) -> mark# X1, mark# f(X1, X2) -> a__f#(mark X1, X2)) (mark# g(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1) (mark# g(X1, X2) -> mark# X1, mark# g(X1, X2) -> mark# X1) (mark# g(X1, X2) -> mark# X1, mark# g(X1, X2) -> a__g#(mark X1, X2)) (mark# g(X1, X2) -> mark# X1, mark# h X -> a__h# mark X) (mark# g(X1, X2) -> mark# X1, mark# h X -> mark# X) (mark# g(X1, X2) -> mark# X1, mark# a() -> a__a#()) (mark# g(X1, X2) -> a__g#(mark X1, X2), a__g#(a(), X) -> a__f#(b(), X)) (mark# h X -> mark# X, mark# f(X1, X2) -> a__f#(mark X1, X2)) (mark# h X -> mark# X, mark# f(X1, X2) -> mark# X1) (mark# h X -> mark# X, mark# g(X1, X2) -> mark# X1) (mark# h X -> mark# X, mark# g(X1, X2) -> a__g#(mark X1, X2)) (mark# h X -> mark# X, mark# h X -> a__h# mark X) (mark# h X -> mark# X, mark# h X -> mark# X) (mark# h X -> mark# X, mark# a() -> a__a#()) (a__h# X -> a__g#(mark X, X), a__g#(a(), X) -> a__f#(b(), X)) (a__f#(X, X) -> a__h# a__a(), a__h# X -> mark# X) (a__f#(X, X) -> a__h# a__a(), a__h# X -> a__g#(mark X, X)) (mark# h X -> a__h# mark X, a__h# X -> a__g#(mark X, X)) (mark# h X -> a__h# mark X, a__h# X -> mark# X) (a__h# X -> mark# X, mark# a() -> a__a#()) (a__h# X -> mark# X, mark# h X -> mark# X) (a__h# X -> mark# X, mark# h X -> a__h# mark X) (a__h# X -> mark# X, mark# g(X1, X2) -> a__g#(mark X1, X2)) (a__h# X -> mark# X, mark# g(X1, X2) -> mark# X1) (a__h# X -> mark# X, mark# f(X1, X2) -> mark# X1) (a__h# X -> mark# X, mark# f(X1, X2) -> a__f#(mark X1, X2)) (mark# f(X1, X2) -> a__f#(mark X1, X2), a__f#(X, X) -> a__h# a__a()) (mark# f(X1, X2) -> a__f#(mark X1, X2), a__f#(X, X) -> a__a#()) (mark# f(X1, X2) -> mark# X1, mark# a() -> a__a#()) (mark# f(X1, X2) -> mark# X1, mark# h X -> mark# X) (mark# f(X1, X2) -> mark# X1, mark# h X -> a__h# mark X) (mark# f(X1, X2) -> mark# X1, mark# g(X1, X2) -> a__g#(mark X1, X2)) (mark# f(X1, X2) -> mark# X1, mark# g(X1, X2) -> mark# X1) (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1) (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> a__f#(mark X1, X2)) (a__g#(a(), X) -> a__f#(b(), X), a__f#(X, X) -> a__h# a__a()) (a__g#(a(), X) -> a__f#(b(), X), a__f#(X, X) -> a__a#())} EDG: {(mark# g(X1, X2) -> mark# X1, mark# f(X1, X2) -> a__f#(mark X1, X2)) (mark# g(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1) (mark# g(X1, X2) -> mark# X1, mark# g(X1, X2) -> mark# X1) (mark# g(X1, X2) -> mark# X1, mark# g(X1, X2) -> a__g#(mark X1, X2)) (mark# g(X1, X2) -> mark# X1, mark# h X -> a__h# mark X) (mark# g(X1, X2) -> mark# X1, mark# h X -> mark# X) (mark# g(X1, X2) -> mark# X1, mark# a() -> a__a#()) (mark# g(X1, X2) -> a__g#(mark X1, X2), a__g#(a(), X) -> a__f#(b(), X)) (mark# h X -> mark# X, mark# f(X1, X2) -> a__f#(mark X1, X2)) (mark# h X -> mark# X, mark# f(X1, X2) -> mark# X1) (mark# h X -> mark# X, mark# g(X1, X2) -> mark# X1) (mark# h X -> mark# X, mark# g(X1, X2) -> a__g#(mark X1, X2)) (mark# h X -> mark# X, mark# h X -> a__h# mark X) (mark# h X -> mark# X, mark# h X -> mark# X) (mark# h X -> mark# X, mark# a() -> a__a#()) (a__h# X -> a__g#(mark X, X), a__g#(a(), X) -> a__f#(b(), X)) (a__f#(X, X) -> a__h# a__a(), a__h# X -> mark# X) (a__f#(X, X) -> a__h# a__a(), a__h# X -> a__g#(mark X, X)) (mark# h X -> a__h# mark X, a__h# X -> a__g#(mark X, X)) (mark# h X -> a__h# mark X, a__h# X -> mark# X) (a__h# X -> mark# X, mark# a() -> a__a#()) (a__h# X -> mark# X, mark# h X -> mark# X) (a__h# X -> mark# X, mark# h X -> a__h# mark X) (a__h# X -> mark# X, mark# g(X1, X2) -> a__g#(mark X1, X2)) (a__h# X -> mark# X, mark# g(X1, X2) -> mark# X1) (a__h# X -> mark# X, mark# f(X1, X2) -> mark# X1) (a__h# X -> mark# X, mark# f(X1, X2) -> a__f#(mark X1, X2)) (mark# f(X1, X2) -> a__f#(mark X1, X2), a__f#(X, X) -> a__h# a__a()) (mark# f(X1, X2) -> a__f#(mark X1, X2), a__f#(X, X) -> a__a#()) (mark# f(X1, X2) -> mark# X1, mark# a() -> a__a#()) (mark# f(X1, X2) -> mark# X1, mark# h X -> mark# X) (mark# f(X1, X2) -> mark# X1, mark# h X -> a__h# mark X) (mark# f(X1, X2) -> mark# X1, mark# g(X1, X2) -> a__g#(mark X1, X2)) (mark# f(X1, X2) -> mark# X1, mark# g(X1, X2) -> mark# X1) (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1) (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> a__f#(mark X1, X2)) (a__g#(a(), X) -> a__f#(b(), X), a__f#(X, X) -> a__h# a__a()) (a__g#(a(), X) -> a__f#(b(), X), a__f#(X, X) -> a__a#())} EDG: {(mark# g(X1, X2) -> mark# X1, mark# f(X1, X2) -> a__f#(mark X1, X2)) (mark# g(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1) (mark# g(X1, X2) -> mark# X1, mark# g(X1, X2) -> mark# X1) (mark# g(X1, X2) -> mark# X1, mark# g(X1, X2) -> a__g#(mark X1, X2)) (mark# g(X1, X2) -> mark# X1, mark# h X -> a__h# mark X) (mark# g(X1, X2) -> mark# X1, mark# h X -> mark# X) (mark# g(X1, X2) -> mark# X1, mark# a() -> a__a#()) (mark# g(X1, X2) -> a__g#(mark X1, X2), a__g#(a(), X) -> a__f#(b(), X)) (mark# h X -> mark# X, mark# f(X1, X2) -> a__f#(mark X1, X2)) (mark# h X -> mark# X, mark# f(X1, X2) -> mark# X1) (mark# h X -> mark# X, mark# g(X1, X2) -> mark# X1) (mark# h X -> mark# X, mark# g(X1, X2) -> a__g#(mark X1, X2)) (mark# h X -> mark# X, mark# h X -> a__h# mark X) (mark# h X -> mark# X, mark# h X -> mark# X) (mark# h X -> mark# X, mark# a() -> a__a#()) (a__h# X -> a__g#(mark X, X), a__g#(a(), X) -> a__f#(b(), X)) (a__f#(X, X) -> a__h# a__a(), a__h# X -> mark# X) (a__f#(X, X) -> a__h# a__a(), a__h# X -> a__g#(mark X, X)) (mark# h X -> a__h# mark X, a__h# X -> a__g#(mark X, X)) (mark# h X -> a__h# mark X, a__h# X -> mark# X) (a__h# X -> mark# X, mark# a() -> a__a#()) (a__h# X -> mark# X, mark# h X -> mark# X) (a__h# X -> mark# X, mark# h X -> a__h# mark X) (a__h# X -> mark# X, mark# g(X1, X2) -> a__g#(mark X1, X2)) (a__h# X -> mark# X, mark# g(X1, X2) -> mark# X1) (a__h# X -> mark# X, mark# f(X1, X2) -> mark# X1) (a__h# X -> mark# X, mark# f(X1, X2) -> a__f#(mark X1, X2)) (mark# f(X1, X2) -> a__f#(mark X1, X2), a__f#(X, X) -> a__h# a__a()) (mark# f(X1, X2) -> a__f#(mark X1, X2), a__f#(X, X) -> a__a#()) (mark# f(X1, X2) -> mark# X1, mark# a() -> a__a#()) (mark# f(X1, X2) -> mark# X1, mark# h X -> mark# X) (mark# f(X1, X2) -> mark# X1, mark# h X -> a__h# mark X) (mark# f(X1, X2) -> mark# X1, mark# g(X1, X2) -> a__g#(mark X1, X2)) (mark# f(X1, X2) -> mark# X1, mark# g(X1, X2) -> mark# X1) (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1) (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> a__f#(mark X1, X2)) (a__g#(a(), X) -> a__f#(b(), X), a__f#(X, X) -> a__h# a__a()) (a__g#(a(), X) -> a__f#(b(), X), a__f#(X, X) -> a__a#())} STATUS: arrows: 0.736111 SCCS (1): Scc: { a__g#(a(), X) -> a__f#(b(), X), mark# h X -> mark# X, mark# h X -> a__h# mark X, mark# g(X1, X2) -> a__g#(mark X1, X2), mark# g(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> a__f#(mark X1, X2), a__h# X -> a__g#(mark X, X), a__h# X -> mark# X, a__f#(X, X) -> a__h# a__a()} SCC (10): Strict: { a__g#(a(), X) -> a__f#(b(), X), mark# h X -> mark# X, mark# h X -> a__h# mark X, mark# g(X1, X2) -> a__g#(mark X1, X2), mark# g(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> a__f#(mark X1, X2), a__h# X -> a__g#(mark X, X), a__h# X -> mark# X, a__f#(X, X) -> a__h# a__a()} Weak: { a__g(X1, X2) -> g(X1, X2), a__g(a(), X) -> a__f(b(), X), mark b() -> b(), mark a() -> a__a(), mark h X -> a__h mark X, mark g(X1, X2) -> a__g(mark X1, X2), mark f(X1, X2) -> a__f(mark X1, X2), a__h X -> a__g(mark X, X), a__h X -> h X, a__f(X, X) -> a__h a__a(), a__f(X1, X2) -> f(X1, X2), a__a() -> b(), a__a() -> a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__g](x0, x1) = x0 + 1, [a__f](x0, x1) = x0 + 1, [g](x0, x1) = x0 + 1, [f](x0, x1) = x0 + 1, [mark](x0) = x0, [a__h](x0) = x0 + 1, [h](x0) = x0 + 1, [b] = 0, [a] = 0, [a__a] = 0, [a__g#](x0, x1) = 0, [a__f#](x0, x1) = x0, [mark#](x0) = x0, [a__h#](x0) = x0 Strict: a__f#(X, X) -> a__h# a__a() 0 + 1X >= 0 a__h# X -> mark# X 0 + 1X >= 0 + 1X a__h# X -> a__g#(mark X, X) 0 + 1X >= 0 + 0X mark# f(X1, X2) -> a__f#(mark X1, X2) 1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 mark# f(X1, X2) -> mark# X1 1 + 1X1 + 0X2 >= 0 + 1X1 mark# g(X1, X2) -> mark# X1 1 + 1X1 + 0X2 >= 0 + 1X1 mark# g(X1, X2) -> a__g#(mark X1, X2) 1 + 1X1 + 0X2 >= 0 + 0X1 + 0X2 mark# h X -> a__h# mark X 1 + 1X >= 0 + 1X mark# h X -> mark# X 1 + 1X >= 0 + 1X a__g#(a(), X) -> a__f#(b(), X) 0 + 0X >= 0 + 0X Weak: a__a() -> a() 0 >= 0 a__a() -> b() 0 >= 0 a__f(X1, X2) -> f(X1, X2) 1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2 a__f(X, X) -> a__h a__a() 1 + 1X >= 1 a__h X -> h X 1 + 1X >= 1 + 1X a__h X -> a__g(mark X, X) 1 + 1X >= 1 + 1X mark f(X1, X2) -> a__f(mark X1, X2) 1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2 mark g(X1, X2) -> a__g(mark X1, X2) 1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2 mark h X -> a__h mark X 1 + 1X >= 1 + 1X mark a() -> a__a() 0 >= 0 mark b() -> b() 0 >= 0 a__g(a(), X) -> a__f(b(), X) 1 + 0X >= 1 + 0X a__g(X1, X2) -> g(X1, X2) 1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2 SCCS (1): Scc: {a__g#(a(), X) -> a__f#(b(), X), a__h# X -> a__g#(mark X, X), a__f#(X, X) -> a__h# a__a()} SCC (3): Strict: {a__g#(a(), X) -> a__f#(b(), X), a__h# X -> a__g#(mark X, X), a__f#(X, X) -> a__h# a__a()} Weak: { a__g(X1, X2) -> g(X1, X2), a__g(a(), X) -> a__f(b(), X), mark b() -> b(), mark a() -> a__a(), mark h X -> a__h mark X, mark g(X1, X2) -> a__g(mark X1, X2), mark f(X1, X2) -> a__f(mark X1, X2), a__h X -> a__g(mark X, X), a__h X -> h X, a__f(X, X) -> a__h a__a(), a__f(X1, X2) -> f(X1, X2), a__a() -> b(), a__a() -> a()} Fail