MAYBE Time: 0.223051 TRS: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} DP: DP: { mark# f(X1, X2, X3) -> active# f(X1, X2, X3), mark# g X -> mark# X, mark# g X -> active# g mark X, mark# g X -> g# mark X, mark# c() -> active# c(), mark# b() -> active# b(), f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3), active# f(X, g X, Y) -> mark# f(Y, Y, Y), active# f(X, g X, Y) -> f#(Y, Y, Y), active# g b() -> mark# c(), active# b() -> mark# c(), g# mark X -> g# X, g# active X -> g# X} TRS: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} UR: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X, a(x, y) -> x, a(x, y) -> y} EDG: {(f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(active X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (active# f(X, g X, Y) -> f#(Y, Y, Y), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (active# f(X, g X, Y) -> f#(Y, Y, Y), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (active# f(X, g X, Y) -> f#(Y, Y, Y), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (active# f(X, g X, Y) -> f#(Y, Y, Y), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (active# f(X, g X, Y) -> f#(Y, Y, Y), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (active# f(X, g X, Y) -> f#(Y, Y, Y), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (mark# b() -> active# b(), active# b() -> mark# c()) (mark# b() -> active# b(), active# g b() -> mark# c()) (mark# b() -> active# b(), active# f(X, g X, Y) -> f#(Y, Y, Y)) (mark# b() -> active# b(), active# f(X, g X, Y) -> mark# f(Y, Y, Y)) (active# b() -> mark# c(), mark# b() -> active# b()) (active# b() -> mark# c(), mark# c() -> active# c()) (active# b() -> mark# c(), mark# g X -> g# mark X) (active# b() -> mark# c(), mark# g X -> active# g mark X) (active# b() -> mark# c(), mark# g X -> mark# X) (active# b() -> mark# c(), mark# f(X1, X2, X3) -> active# f(X1, X2, X3)) (g# mark X -> g# X, g# active X -> g# X) (g# mark X -> g# X, g# mark X -> g# X) (mark# g X -> active# g mark X, active# b() -> mark# c()) (mark# g X -> active# g mark X, active# g b() -> mark# c()) (mark# g X -> active# g mark X, active# f(X, g X, Y) -> f#(Y, Y, Y)) (mark# g X -> active# g mark X, active# f(X, g X, Y) -> mark# f(Y, Y, Y)) (active# f(X, g X, Y) -> mark# f(Y, Y, Y), mark# b() -> active# b()) (active# f(X, g X, Y) -> mark# f(Y, Y, Y), mark# c() -> active# c()) (active# f(X, g X, Y) -> mark# f(Y, Y, Y), mark# g X -> g# mark X) (active# f(X, g X, Y) -> mark# f(Y, Y, Y), mark# g X -> active# g mark X) (active# f(X, g X, Y) -> mark# f(Y, Y, Y), mark# g X -> mark# X) (active# f(X, g X, Y) -> mark# f(Y, Y, Y), mark# f(X1, X2, X3) -> active# f(X1, X2, X3)) (mark# f(X1, X2, X3) -> active# f(X1, X2, X3), active# f(X, g X, Y) -> mark# f(Y, Y, Y)) (mark# f(X1, X2, X3) -> active# f(X1, X2, X3), active# f(X, g X, Y) -> f#(Y, Y, Y)) (mark# f(X1, X2, X3) -> active# f(X1, X2, X3), active# g b() -> mark# c()) (mark# f(X1, X2, X3) -> active# f(X1, X2, X3), active# b() -> mark# c()) (g# active X -> g# X, g# mark X -> g# X) (g# active X -> g# X, g# active X -> g# X) (mark# g X -> mark# X, mark# f(X1, X2, X3) -> active# f(X1, X2, X3)) (mark# g X -> mark# X, mark# g X -> mark# X) (mark# g X -> mark# X, mark# g X -> active# g mark X) (mark# g X -> mark# X, mark# g X -> g# mark X) (mark# g X -> mark# X, mark# c() -> active# c()) (mark# g X -> mark# X, mark# b() -> active# b()) (active# g b() -> mark# c(), mark# f(X1, X2, X3) -> active# f(X1, X2, X3)) (active# g b() -> mark# c(), mark# g X -> mark# X) (active# g b() -> mark# c(), mark# g X -> active# g mark X) (active# g b() -> mark# c(), mark# g X -> g# mark X) (active# g b() -> mark# c(), mark# c() -> active# c()) (active# g b() -> mark# c(), mark# b() -> active# b()) (mark# c() -> active# c(), active# f(X, g X, Y) -> mark# f(Y, Y, Y)) (mark# c() -> active# c(), active# f(X, g X, Y) -> f#(Y, Y, Y)) (mark# c() -> active# c(), active# g b() -> mark# c()) (mark# c() -> active# c(), active# b() -> mark# c()) (mark# g X -> g# mark X, g# mark X -> g# X) (mark# g X -> g# mark X, g# active X -> g# X) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3))} STATUS: arrows: 0.728395 SCCS (3): Scc: { mark# f(X1, X2, X3) -> active# f(X1, X2, X3), mark# g X -> mark# X, mark# g X -> active# g mark X, mark# c() -> active# c(), mark# b() -> active# b(), active# f(X, g X, Y) -> mark# f(Y, Y, Y), active# g b() -> mark# c(), active# b() -> mark# c()} Scc: { g# mark X -> g# X, g# active X -> g# X} Scc: { f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)} SCC (8): Strict: { mark# f(X1, X2, X3) -> active# f(X1, X2, X3), mark# g X -> mark# X, mark# g X -> active# g mark X, mark# c() -> active# c(), mark# b() -> active# b(), active# f(X, g X, Y) -> mark# f(Y, Y, Y), active# g b() -> mark# c(), active# b() -> mark# c()} Weak: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = 0, [mark](x0) = x0, [active](x0) = x0, [g](x0) = x0, [c] = 0, [b] = 1, [mark#](x0) = x0, [active#](x0) = x0 Strict: active# b() -> mark# c() 1 >= 0 active# g b() -> mark# c() 1 >= 0 active# f(X, g X, Y) -> mark# f(Y, Y, Y) 0 + 0Y + 0X >= 0 + 0Y mark# b() -> active# b() 1 >= 1 mark# c() -> active# c() 0 >= 0 mark# g X -> active# g mark X 0 + 1X >= 0 + 1X mark# g X -> mark# X 0 + 1X >= 0 + 1X mark# f(X1, X2, X3) -> active# f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 Weak: g active X -> g X 0 + 1X >= 0 + 1X g mark X -> g X 0 + 1X >= 0 + 1X active b() -> mark c() 1 >= 0 active g b() -> mark c() 1 >= 0 active f(X, g X, Y) -> mark f(Y, Y, Y) 0 + 0Y + 0X >= 0 + 0Y f(active X1, X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, active X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, X2, active X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark b() -> active b() 1 >= 1 mark c() -> active c() 0 >= 0 mark g X -> active g mark X 0 + 1X >= 0 + 1X mark f(X1, X2, X3) -> active f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: { mark# f(X1, X2, X3) -> active# f(X1, X2, X3), mark# g X -> mark# X, mark# g X -> active# g mark X, mark# c() -> active# c(), mark# b() -> active# b(), active# f(X, g X, Y) -> mark# f(Y, Y, Y)} SCC (6): Strict: { mark# f(X1, X2, X3) -> active# f(X1, X2, X3), mark# g X -> mark# X, mark# g X -> active# g mark X, mark# c() -> active# c(), mark# b() -> active# b(), active# f(X, g X, Y) -> mark# f(Y, Y, Y)} Weak: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = 0, [mark](x0) = 0, [active](x0) = 0, [g](x0) = x0, [c] = 0, [b] = 1, [mark#](x0) = x0, [active#](x0) = 0 Strict: active# f(X, g X, Y) -> mark# f(Y, Y, Y) 0 + 0Y + 0X >= 0 + 0Y mark# b() -> active# b() 1 >= 0 mark# c() -> active# c() 0 >= 0 mark# g X -> active# g mark X 0 + 1X >= 0 + 0X mark# g X -> mark# X 0 + 1X >= 0 + 1X mark# f(X1, X2, X3) -> active# f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 Weak: g active X -> g X 0 + 0X >= 0 + 1X g mark X -> g X 0 + 0X >= 0 + 1X active b() -> mark c() 0 >= 0 active g b() -> mark c() 0 >= 0 active f(X, g X, Y) -> mark f(Y, Y, Y) 0 + 0Y + 0X >= 0 + 0Y f(active X1, X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, active X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, X2, active X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark b() -> active b() 0 >= 0 mark c() -> active c() 0 >= 0 mark g X -> active g mark X 0 + 0X >= 0 + 0X mark f(X1, X2, X3) -> active f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: { mark# f(X1, X2, X3) -> active# f(X1, X2, X3), mark# g X -> mark# X, mark# g X -> active# g mark X, mark# c() -> active# c(), active# f(X, g X, Y) -> mark# f(Y, Y, Y)} SCC (5): Strict: { mark# f(X1, X2, X3) -> active# f(X1, X2, X3), mark# g X -> mark# X, mark# g X -> active# g mark X, mark# c() -> active# c(), active# f(X, g X, Y) -> mark# f(Y, Y, Y)} Weak: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = 0, [mark](x0) = 0, [active](x0) = 0, [g](x0) = x0, [c] = 1, [b] = 0, [mark#](x0) = x0, [active#](x0) = 0 Strict: active# f(X, g X, Y) -> mark# f(Y, Y, Y) 0 + 0Y + 0X >= 0 + 0Y mark# c() -> active# c() 1 >= 0 mark# g X -> active# g mark X 0 + 1X >= 0 + 0X mark# g X -> mark# X 0 + 1X >= 0 + 1X mark# f(X1, X2, X3) -> active# f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 Weak: g active X -> g X 0 + 0X >= 0 + 1X g mark X -> g X 0 + 0X >= 0 + 1X active b() -> mark c() 0 >= 0 active g b() -> mark c() 0 >= 0 active f(X, g X, Y) -> mark f(Y, Y, Y) 0 + 0Y + 0X >= 0 + 0Y f(active X1, X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, active X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, X2, active X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark b() -> active b() 0 >= 0 mark c() -> active c() 0 >= 0 mark g X -> active g mark X 0 + 0X >= 0 + 0X mark f(X1, X2, X3) -> active f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: { mark# f(X1, X2, X3) -> active# f(X1, X2, X3), mark# g X -> mark# X, mark# g X -> active# g mark X, active# f(X, g X, Y) -> mark# f(Y, Y, Y)} SCC (4): Strict: { mark# f(X1, X2, X3) -> active# f(X1, X2, X3), mark# g X -> mark# X, mark# g X -> active# g mark X, active# f(X, g X, Y) -> mark# f(Y, Y, Y)} Weak: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [g](x0) = 0, [c] = 1, [b] = 1, [mark#](x0) = 1, [active#](x0) = x0 Strict: active# f(X, g X, Y) -> mark# f(Y, Y, Y) 1 + 0Y + 0X >= 1 + 0Y mark# g X -> active# g mark X 1 + 0X >= 0 + 0X mark# g X -> mark# X 1 + 0X >= 1 + 0X mark# f(X1, X2, X3) -> active# f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 Weak: g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X active b() -> mark c() 2 >= 2 active g b() -> mark c() 1 >= 2 active f(X, g X, Y) -> mark f(Y, Y, Y) 2 + 0Y + 0X >= 2 + 0Y f(active X1, X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, active X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, X2, active X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark b() -> active b() 2 >= 2 mark c() -> active c() 2 >= 2 mark g X -> active g mark X 1 + 0X >= 1 + 0X mark f(X1, X2, X3) -> active f(X1, X2, X3) 2 + 0X1 + 0X2 + 0X3 >= 2 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: { mark# f(X1, X2, X3) -> active# f(X1, X2, X3), mark# g X -> mark# X, active# f(X, g X, Y) -> mark# f(Y, Y, Y)} SCC (3): Strict: { mark# f(X1, X2, X3) -> active# f(X1, X2, X3), mark# g X -> mark# X, active# f(X, g X, Y) -> mark# f(Y, Y, Y)} Weak: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = 0, [mark](x0) = x0 + 1, [active](x0) = x0, [g](x0) = x0 + 1, [c] = 0, [b] = 1, [mark#](x0) = x0, [active#](x0) = 0 Strict: active# f(X, g X, Y) -> mark# f(Y, Y, Y) 0 + 0Y + 0X >= 0 + 0Y mark# g X -> mark# X 1 + 1X >= 0 + 1X mark# f(X1, X2, X3) -> active# f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 Weak: g active X -> g X 1 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X active b() -> mark c() 1 >= 1 active g b() -> mark c() 2 >= 1 active f(X, g X, Y) -> mark f(Y, Y, Y) 0 + 0Y + 0X >= 1 + 0Y f(active X1, X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, active X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, X2, active X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark b() -> active b() 2 >= 1 mark c() -> active c() 1 >= 0 mark g X -> active g mark X 2 + 1X >= 2 + 1X mark f(X1, X2, X3) -> active f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: { mark# f(X1, X2, X3) -> active# f(X1, X2, X3), active# f(X, g X, Y) -> mark# f(Y, Y, Y)} SCC (2): Strict: { mark# f(X1, X2, X3) -> active# f(X1, X2, X3), active# f(X, g X, Y) -> mark# f(Y, Y, Y)} Weak: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} Fail SCC (2): Strict: { g# mark X -> g# X, g# active X -> g# X} Weak: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = 1, [mark](x0) = x0, [active](x0) = x0 + 1, [g](x0) = 0, [c] = 1, [b] = 0, [g#](x0) = x0 Strict: g# active X -> g# X 1 + 1X >= 0 + 1X g# mark X -> g# X 0 + 1X >= 0 + 1X Weak: g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X active b() -> mark c() 1 >= 1 active g b() -> mark c() 1 >= 1 active f(X, g X, Y) -> mark f(Y, Y, Y) 2 + 0Y + 0X >= 1 + 0Y f(active X1, X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, active X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, X2, active X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark b() -> active b() 0 >= 1 mark c() -> active c() 1 >= 2 mark g X -> active g mark X 0 + 0X >= 1 + 0X mark f(X1, X2, X3) -> active f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 2 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: {g# mark X -> g# X} SCC (1): Strict: {g# mark X -> g# X} Weak: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = x0 + x1 + 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [g](x0) = x0 + 1, [c] = 1, [b] = 1, [g#](x0) = x0 Strict: g# mark X -> g# X 1 + 1X >= 0 + 1X Weak: g active X -> g X 2 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X active b() -> mark c() 2 >= 2 active g b() -> mark c() 3 >= 2 active f(X, g X, Y) -> mark f(Y, Y, Y) 2 + 1Y + 1X >= 2 + 2Y f(active X1, X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 f(X1, active X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 f(X1, X2, active X3) -> f(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 mark b() -> active b() 2 >= 2 mark c() -> active c() 2 >= 2 mark g X -> active g mark X 2 + 1X >= 3 + 1X mark f(X1, X2, X3) -> active f(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 2 + 1X1 + 0X2 + 1X3 Qed SCC (6): Strict: { f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)} Weak: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = 1, [mark](x0) = x0, [active](x0) = x0 + 1, [g](x0) = 0, [c] = 1, [b] = 0, [f#](x0, x1, x2) = x0 Strict: f#(active X1, X2, X3) -> f#(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(mark X1, X2, X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(X1, active X2, X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(X1, mark X2, X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(X1, X2, active X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(X1, X2, mark X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 Weak: g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X active b() -> mark c() 1 >= 1 active g b() -> mark c() 1 >= 1 active f(X, g X, Y) -> mark f(Y, Y, Y) 2 + 0Y + 0X >= 1 + 0Y f(active X1, X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, active X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, X2, active X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark b() -> active b() 0 >= 1 mark c() -> active c() 1 >= 2 mark g X -> active g mark X 0 + 0X >= 1 + 0X mark f(X1, X2, X3) -> active f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 2 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: { f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)} SCC (5): Strict: { f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)} Weak: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = x0 + 1, [mark](x0) = x0, [active](x0) = x0 + 1, [g](x0) = 1, [c] = 1, [b] = 0, [f#](x0, x1, x2) = x0 Strict: f#(mark X1, X2, X3) -> f#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 f#(X1, active X2, X3) -> f#(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 f#(X1, mark X2, X3) -> f#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 f#(X1, X2, active X3) -> f#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 f#(X1, X2, mark X3) -> f#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 Weak: g active X -> g X 1 + 0X >= 1 + 0X g mark X -> g X 1 + 0X >= 1 + 0X active b() -> mark c() 1 >= 1 active g b() -> mark c() 2 >= 1 active f(X, g X, Y) -> mark f(Y, Y, Y) 3 + 0Y + 0X >= 1 + 1Y f(active X1, X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3 f(X1, active X2, X3) -> f(X1, X2, X3) 2 + 0X1 + 1X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3 f(X1, X2, active X3) -> f(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3 mark b() -> active b() 0 >= 1 mark c() -> active c() 1 >= 2 mark g X -> active g mark X 1 + 0X >= 2 + 0X mark f(X1, X2, X3) -> active f(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 2 + 0X1 + 1X2 + 0X3 SCCS (1): Scc: { f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)} SCC (4): Strict: { f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)} Weak: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = 0, [mark](x0) = x0 + 1, [active](x0) = 0, [g](x0) = 0, [c] = 0, [b] = 1, [f#](x0, x1, x2) = x0 Strict: f#(mark X1, X2, X3) -> f#(X1, X2, X3) 1 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(X1, mark X2, X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(X1, X2, active X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 f#(X1, X2, mark X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 Weak: g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X active b() -> mark c() 0 >= 1 active g b() -> mark c() 0 >= 1 active f(X, g X, Y) -> mark f(Y, Y, Y) 0 + 0Y + 0X >= 1 + 0Y f(active X1, X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, active X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, X2, active X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark b() -> active b() 2 >= 0 mark c() -> active c() 1 >= 0 mark g X -> active g mark X 1 + 0X >= 0 + 0X mark f(X1, X2, X3) -> active f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: { f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)} SCC (3): Strict: { f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)} Weak: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = x0 + x1 + x2 + 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [g](x0) = 0, [c] = 1, [b] = 1, [f#](x0, x1, x2) = x0 Strict: f#(X1, mark X2, X3) -> f#(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 f#(X1, X2, active X3) -> f#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 f#(X1, X2, mark X3) -> f#(X1, X2, X3) 0 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 Weak: g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X active b() -> mark c() 2 >= 2 active g b() -> mark c() 1 >= 2 active f(X, g X, Y) -> mark f(Y, Y, Y) 2 + 1Y + 1X >= 2 + 3Y f(active X1, X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, active X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, X2, active X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3 mark b() -> active b() 2 >= 2 mark c() -> active c() 2 >= 2 mark g X -> active g mark X 1 + 0X >= 1 + 0X mark f(X1, X2, X3) -> active f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 SCCS (1): Scc: { f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)} SCC (2): Strict: { f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)} Weak: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = 1, [mark](x0) = x0, [active](x0) = x0 + 1, [g](x0) = 0, [c] = 1, [b] = 0, [f#](x0, x1, x2) = x0 Strict: f#(X1, X2, active X3) -> f#(X1, X2, X3) 1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 f#(X1, X2, mark X3) -> f#(X1, X2, X3) 0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 Weak: g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X active b() -> mark c() 1 >= 1 active g b() -> mark c() 1 >= 1 active f(X, g X, Y) -> mark f(Y, Y, Y) 2 + 0Y + 0X >= 1 + 0Y f(active X1, X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, active X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, X2, active X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark b() -> active b() 0 >= 1 mark c() -> active c() 1 >= 2 mark g X -> active g mark X 0 + 0X >= 1 + 0X mark f(X1, X2, X3) -> active f(X1, X2, X3) 1 + 0X1 + 0X2 + 0X3 >= 2 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: {f#(X1, X2, mark X3) -> f#(X1, X2, X3)} SCC (1): Strict: {f#(X1, X2, mark X3) -> f#(X1, X2, X3)} Weak: { mark f(X1, X2, X3) -> active f(X1, X2, X3), mark g X -> active g mark X, mark c() -> active c(), mark b() -> active b(), f(X1, X2, mark X3) -> f(X1, X2, X3), f(X1, X2, active X3) -> f(X1, X2, X3), f(X1, mark X2, X3) -> f(X1, X2, X3), f(X1, active X2, X3) -> f(X1, X2, X3), f(mark X1, X2, X3) -> f(X1, X2, X3), f(active X1, X2, X3) -> f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g b() -> mark c(), active b() -> mark c(), g mark X -> g X, g active X -> g X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = x0 + x1 + 1, [mark](x0) = x0 + 1, [active](x0) = x0 + 1, [g](x0) = x0 + 1, [c] = 1, [b] = 1, [f#](x0, x1, x2) = x0 Strict: f#(X1, X2, mark X3) -> f#(X1, X2, X3) 1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 Weak: g active X -> g X 2 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X active b() -> mark c() 2 >= 2 active g b() -> mark c() 3 >= 2 active f(X, g X, Y) -> mark f(Y, Y, Y) 2 + 1Y + 1X >= 2 + 2Y f(active X1, X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 f(X1, active X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 f(X1, X2, active X3) -> f(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 1 + 1X1 + 0X2 + 1X3 mark b() -> active b() 2 >= 2 mark c() -> active c() 2 >= 2 mark g X -> active g mark X 2 + 1X >= 3 + 1X mark f(X1, X2, X3) -> active f(X1, X2, X3) 2 + 1X1 + 0X2 + 1X3 >= 2 + 1X1 + 0X2 + 1X3 Qed