MAYBE Time: 0.080889 TRS: { mark f(X1, X2, X3) -> active f(X1, mark X2, X3), 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(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b()} DP: DP: { mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), 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(b(), X, c()) -> mark# f(X, c(), X), active# f(b(), X, c()) -> f#(X, c(), X), active# c() -> mark# b()} TRS: { mark f(X1, X2, X3) -> active f(X1, mark X2, X3), 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(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b()} UR: { mark f(X1, X2, X3) -> active f(X1, mark X2, X3), 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(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b(), a(x, y) -> x, a(x, y) -> y} EDG: {(active# f(b(), X, c()) -> mark# f(X, c(), X), mark# b() -> active# b()) (active# f(b(), X, c()) -> mark# f(X, c(), X), mark# c() -> active# c()) (active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> mark# X2) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(active 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, 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#(X1, mark X2, 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, X2, mark 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, 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#(X1, active 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, 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, X2, mark X3) -> f#(X1, X2, X3)) (f#(mark 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#(mark X1, 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#(X1, mark X2, 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, X2, mark X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (mark# c() -> active# c(), active# c() -> mark# b()) (mark# c() -> active# c(), active# f(b(), X, c()) -> f#(X, c(), X)) (mark# c() -> active# c(), active# f(b(), X, c()) -> mark# f(X, c(), X)) (active# c() -> mark# b(), mark# b() -> active# b()) (active# c() -> mark# b(), mark# c() -> active# c()) (active# c() -> mark# b(), mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (active# c() -> mark# b(), mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (active# c() -> mark# b(), mark# f(X1, X2, X3) -> mark# X2) (mark# b() -> active# b(), active# f(b(), X, c()) -> mark# f(X, c(), X)) (mark# b() -> active# b(), active# f(b(), X, c()) -> f#(X, c(), X)) (mark# b() -> active# b(), active# c() -> mark# b()) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> mark# X2) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# c() -> active# c()) (mark# f(X1, X2, X3) -> mark# X2, mark# b() -> active# b()) (f#(active 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), f#(X1, X2, active 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, active 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#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, active 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, active 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, active 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#(active X1, X2, 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, 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, mark 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#(mark 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)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(b(), X, c()) -> mark# f(X, c(), X)) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(b(), X, c()) -> f#(X, c(), X)) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# c() -> mark# b())} EDG: {(active# f(b(), X, c()) -> mark# f(X, c(), X), mark# b() -> active# b()) (active# f(b(), X, c()) -> mark# f(X, c(), X), mark# c() -> active# c()) (active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> mark# X2) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(active 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, 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#(X1, mark X2, 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, X2, mark 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, 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#(X1, active 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, 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, X2, mark X3) -> f#(X1, X2, X3)) (f#(mark 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#(mark X1, 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#(X1, mark X2, 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, X2, mark X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (mark# c() -> active# c(), active# c() -> mark# b()) (active# c() -> mark# b(), mark# b() -> active# b()) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> mark# X2) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# c() -> active# c()) (mark# f(X1, X2, X3) -> mark# X2, mark# b() -> active# b()) (f#(active 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), f#(X1, X2, active 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, active 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#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, active 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, active 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, active 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#(active X1, X2, 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, 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, mark 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#(mark 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)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(b(), X, c()) -> mark# f(X, c(), X)) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(b(), X, c()) -> f#(X, c(), X)) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# c() -> mark# b())} EDG: {(active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> mark# X2) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(active 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, 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#(X1, mark X2, 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, X2, mark 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, 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#(X1, active 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, 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, X2, mark X3) -> f#(X1, X2, X3)) (f#(mark 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#(mark X1, 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#(X1, mark X2, 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, X2, mark X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (mark# c() -> active# c(), active# c() -> mark# b()) (active# c() -> mark# b(), mark# b() -> active# b()) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> mark# X2) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# c() -> active# c()) (mark# f(X1, X2, X3) -> mark# X2, mark# b() -> active# b()) (f#(active 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), f#(X1, X2, active 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, active 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#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, active 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, active 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, active 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#(active X1, X2, 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, 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, mark 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#(mark 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)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(b(), X, c()) -> mark# f(X, c(), X)) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(b(), X, c()) -> f#(X, c(), X))} EDG: {(active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (active# f(b(), X, c()) -> mark# f(X, c(), X), mark# f(X1, X2, X3) -> mark# X2) (f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(active 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, 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#(X1, mark X2, 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, X2, mark 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, 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#(X1, active 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, 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, X2, mark X3) -> f#(X1, X2, X3)) (f#(mark 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#(mark X1, 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#(X1, mark X2, 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, X2, mark X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (active# f(b(), X, c()) -> f#(X, c(), X), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (mark# c() -> active# c(), active# c() -> mark# b()) (active# c() -> mark# b(), mark# b() -> active# b()) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> mark# X2) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> f#(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3)) (mark# f(X1, X2, X3) -> mark# X2, mark# c() -> active# c()) (mark# f(X1, X2, X3) -> mark# X2, mark# b() -> active# b()) (f#(active 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), f#(X1, X2, active 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, active 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#(active X1, X2, X3) -> f#(X1, X2, X3)) (f#(X1, active 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, active 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, active 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#(active X1, X2, 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, 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, mark 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#(mark 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)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, X2, mark X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, X2, active X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(X1, active X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> f#(X1, mark X2, X3), f#(active X1, X2, X3) -> f#(X1, X2, X3)) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(b(), X, c()) -> mark# f(X, c(), X)) (mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(b(), X, c()) -> f#(X, c(), X))} STATUS: arrows: 0.704082 SCCS (2): Scc: { mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(b(), X, c()) -> mark# f(X, c(), 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 (3): Strict: { mark# f(X1, X2, X3) -> mark# X2, mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(b(), X, c()) -> mark# f(X, c(), X)} Weak: { mark f(X1, X2, X3) -> active f(X1, mark X2, X3), 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(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = x0 + 1, [mark](x0) = x0 + 1, [active](x0) = x0, [c] = 0, [b] = 0, [mark#](x0) = x0, [active#](x0) = 1 Strict: active# f(b(), X, c()) -> mark# f(X, c(), X) 1 + 0X >= 1 + 0X mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 mark# f(X1, X2, X3) -> mark# X2 1 + 0X1 + 1X2 + 0X3 >= 0 + 1X2 Weak: active c() -> mark b() 0 >= 1 active f(b(), X, c()) -> mark f(X, c(), X) 1 + 1X >= 2 + 0X 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) 1 + 0X1 + 1X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 2 + 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() 1 >= 0 mark c() -> active c() 1 >= 0 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 2 + 0X1 + 1X2 + 0X3 >= 2 + 0X1 + 1X2 + 0X3 SCCS (1): Scc: { mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(b(), X, c()) -> mark# f(X, c(), X)} SCC (2): Strict: { mark# f(X1, X2, X3) -> active# f(X1, mark X2, X3), active# f(b(), X, c()) -> mark# f(X, c(), X)} Weak: { mark f(X1, X2, X3) -> active f(X1, mark X2, X3), 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(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b()} Fail 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, mark X2, X3), 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(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b()} 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 + 1, [c] = 0, [b] = 1, [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: active c() -> mark b() 1 >= 1 active f(b(), X, c()) -> mark f(X, c(), X) 1 + 0X >= 0 + 0X 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 >= 2 mark c() -> active c() 0 >= 1 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 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, mark X2, X3), 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(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b()} 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 + 1, [c] = 0, [b] = 1, [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: active c() -> mark b() 1 >= 1 active f(b(), X, c()) -> mark f(X, c(), X) 1 + 0X >= 0 + 0X 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 >= 2 mark c() -> active c() 0 >= 1 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 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#(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, mark X2, X3), 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(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b()} 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 + 1, [c] = 0, [b] = 1, [f#](x0, x1, x2) = x0 Strict: f#(mark X1, X2, X3) -> f#(X1, X2, X3) 0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 f#(X1, mark X2, X3) -> f#(X1, X2, X3) 0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 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: active c() -> mark b() 1 >= 1 active f(b(), X, c()) -> mark f(X, c(), X) 1 + 0X >= 0 + 0X 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 >= 2 mark c() -> active c() 0 >= 1 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: {f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(mark X1, X2, X3) -> f#(X1, X2, X3)} SCC (3): Strict: {f#(X1, X2, mark 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, mark X2, X3), 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(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b()} 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, [c] = 1, [b] = 0, [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, mark X3) -> f#(X1, X2, X3) 0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3 Weak: active c() -> mark b() 1 >= 1 active f(b(), X, c()) -> mark f(X, c(), X) 1 + 1X >= 3 + 1X f(active X1, X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 f(mark X1, X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 f(X1, active X2, X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 f(X1, mark X2, X3) -> f(X1, X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 f(X1, X2, active X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 f(X1, X2, mark X3) -> f(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 1 + 1X1 + 1X2 + 0X3 mark b() -> active b() 1 >= 0 mark c() -> active c() 2 >= 1 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3 SCCS (1): Scc: {f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)} SCC (2): Strict: {f#(X1, X2, mark X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)} Weak: { mark f(X1, X2, X3) -> active f(X1, mark X2, X3), 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(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b()} 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, [c] = 1, [b] = 0, [f#](x0, x1, x2) = x0 Strict: f#(X1, mark X2, X3) -> f#(X1, X2, X3) 0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 f#(X1, X2, mark X3) -> f#(X1, X2, X3) 1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 Weak: active c() -> mark b() 1 >= 1 active f(b(), X, c()) -> mark f(X, c(), X) 2 + 1X >= 3 + 2X f(active X1, X2, X3) -> f(X1, X2, X3) 1 + 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) 1 + 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) 1 + 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() 1 >= 0 mark c() -> active c() 2 >= 1 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 SCCS (1): Scc: {f#(X1, mark X2, X3) -> f#(X1, X2, X3)} SCC (1): Strict: {f#(X1, mark X2, X3) -> f#(X1, X2, X3)} Weak: { mark f(X1, X2, X3) -> active f(X1, mark X2, X3), 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(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b()} 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, [c] = 1, [b] = 0, [f#](x0, x1, x2) = x0 Strict: f#(X1, mark X2, X3) -> f#(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 Weak: active c() -> mark b() 1 >= 1 active f(b(), X, c()) -> mark f(X, c(), X) 2 + 1X >= 3 + 2X f(active X1, X2, X3) -> f(X1, X2, X3) 1 + 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) 1 + 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) 1 + 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() 1 >= 0 mark c() -> active c() 2 >= 1 mark f(X1, X2, X3) -> active f(X1, mark X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 Qed