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