YES Time: 0.260214 TRS: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g mark X, mark a() -> active a(), c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark c f g f a()} DP: DP: { mark# c X -> active# c X, mark# f X -> mark# X, mark# f X -> f# mark X, mark# f X -> active# f mark X, mark# g X -> mark# X, mark# g X -> g# mark X, mark# g X -> active# g mark X, mark# a() -> active# a(), c# mark X -> c# X, c# active X -> c# X, f# mark X -> f# X, f# active X -> f# X, g# mark X -> g# X, g# active X -> g# X, active# f f a() -> mark# c f g f a(), active# f f a() -> c# f g f a(), active# f f a() -> f# g f a(), active# f f a() -> g# f a()} TRS: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g mark X, mark a() -> active a(), c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark c f g f a()} UR: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g mark X, mark a() -> active a(), c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark c f g f a()} EDG: {(mark# f X -> f# mark X, f# active X -> f# X) (mark# f X -> f# mark X, f# mark X -> f# X) (mark# g X -> mark# X, mark# a() -> active# a()) (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# g X -> mark# X) (mark# g X -> mark# X, mark# f X -> active# f mark X) (mark# g X -> mark# X, mark# f X -> f# mark X) (mark# g X -> mark# X, mark# f X -> mark# X) (mark# g X -> mark# X, mark# c X -> active# c X) (c# active X -> c# X, c# active X -> c# X) (c# active X -> c# X, c# mark X -> c# X) (f# active X -> f# X, f# active X -> f# X) (f# active X -> f# X, f# mark X -> f# X) (g# active X -> g# X, g# active X -> g# X) (g# active X -> g# X, g# mark X -> g# X) (mark# f X -> active# f mark X, active# f f a() -> g# f a()) (mark# f X -> active# f mark X, active# f f a() -> f# g f a()) (mark# f X -> active# f mark X, active# f f a() -> c# f g f a()) (mark# f X -> active# f mark X, active# f f a() -> mark# c f g f a()) (active# f f a() -> mark# c f g f a(), mark# c X -> active# c X) (g# mark X -> g# X, g# mark X -> g# X) (g# mark X -> g# X, g# active X -> g# X) (f# mark X -> f# X, f# mark X -> f# X) (f# mark X -> f# X, f# active X -> f# X) (c# mark X -> c# X, c# mark X -> c# X) (c# mark X -> c# X, c# active X -> c# X) (mark# f X -> mark# X, mark# c X -> active# c X) (mark# f X -> mark# X, mark# f X -> mark# X) (mark# f X -> mark# X, mark# f X -> f# mark X) (mark# f X -> mark# X, mark# f X -> active# f mark X) (mark# f X -> mark# X, mark# g X -> mark# X) (mark# f X -> mark# X, mark# g X -> g# mark X) (mark# f X -> mark# X, mark# g X -> active# g mark X) (mark# f X -> mark# X, mark# a() -> active# a()) (mark# g X -> g# mark X, g# mark X -> g# X) (mark# g X -> g# mark X, g# active X -> g# X)} STATUS: arrows: 0.885802 SCCS (4): Scc: { c# mark X -> c# X, c# active X -> c# X} Scc: {mark# f X -> mark# X, mark# g X -> mark# X} Scc: { g# mark X -> g# X, g# active X -> g# X} Scc: { f# mark X -> f# X, f# active X -> f# X} SCC (2): Strict: { c# mark X -> c# X, c# active X -> c# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g mark X, mark a() -> active a(), c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark c f g f a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0, [c](x0) = 0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [a] = 0, [c#](x0) = x0 Strict: c# active X -> c# X 1 + 1X >= 0 + 1X c# mark X -> c# X 0 + 1X >= 0 + 1X Weak: active f f a() -> mark c f g f a() 1 >= 0 g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X c active X -> c X 0 + 0X >= 0 + 0X c mark X -> c X 0 + 0X >= 0 + 0X mark a() -> active a() 0 >= 1 mark g X -> active g mark X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark c X -> active c X 0 + 0X >= 1 + 0X SCCS (1): Scc: {c# mark X -> c# X} SCC (1): Strict: {c# mark X -> c# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g mark X, mark a() -> active a(), c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark c f g f a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [c](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0 + 1, [a] = 1, [c#](x0) = x0 Strict: c# mark X -> c# X 1 + 1X >= 0 + 1X Weak: active f f a() -> mark c f g f a() 4 >= 6 g active X -> g X 2 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X f active X -> f X 2 + 1X >= 1 + 1X f mark X -> f X 2 + 1X >= 1 + 1X c active X -> c X 2 + 1X >= 1 + 1X c mark X -> c X 2 + 1X >= 1 + 1X mark a() -> active a() 2 >= 2 mark g X -> active g mark X 2 + 1X >= 3 + 1X mark f X -> active f mark X 2 + 1X >= 3 + 1X mark c X -> active c X 2 + 1X >= 2 + 1X Qed SCC (2): Strict: {mark# f X -> mark# X, mark# g X -> mark# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g mark X, mark a() -> active a(), c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark c f g f a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = 0, [c](x0) = x0 + 1, [f](x0) = x0, [g](x0) = x0 + 1, [active](x0) = x0 + 1, [a] = 1, [mark#](x0) = x0 Strict: mark# g X -> mark# X 1 + 1X >= 0 + 1X mark# f X -> mark# X 0 + 1X >= 0 + 1X Weak: active f f a() -> mark c f g f a() 2 >= 0 g active X -> g X 2 + 1X >= 1 + 1X g mark X -> g X 1 + 0X >= 1 + 1X f active X -> f X 1 + 1X >= 0 + 1X f mark X -> f X 0 + 0X >= 0 + 1X c active X -> c X 2 + 1X >= 1 + 1X c mark X -> c X 1 + 0X >= 1 + 1X mark a() -> active a() 0 >= 2 mark g X -> active g mark X 0 + 0X >= 2 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark c X -> active c X 0 + 0X >= 2 + 1X SCCS (1): Scc: {mark# f X -> mark# X} SCC (1): Strict: {mark# f X -> mark# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g mark X, mark a() -> active a(), c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark c f g f a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [c](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0 + 1, [a] = 1, [mark#](x0) = x0 Strict: mark# f X -> mark# X 1 + 1X >= 0 + 1X Weak: active f f a() -> mark c f g f a() 4 >= 6 g active X -> g X 2 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X f active X -> f X 2 + 1X >= 1 + 1X f mark X -> f X 2 + 1X >= 1 + 1X c active X -> c X 2 + 1X >= 1 + 1X c mark X -> c X 2 + 1X >= 1 + 1X mark a() -> active a() 2 >= 2 mark g X -> active g mark X 2 + 1X >= 3 + 1X mark f X -> active f mark X 2 + 1X >= 3 + 1X mark c X -> active c X 2 + 1X >= 2 + 1X Qed SCC (2): Strict: { g# mark X -> g# X, g# active X -> g# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g mark X, mark a() -> active a(), c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark c f g f a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0, [c](x0) = 0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [a] = 0, [g#](x0) = x0 Strict: g# active X -> g# X 1 + 1X >= 0 + 1X g# mark X -> g# X 0 + 1X >= 0 + 1X Weak: active f f a() -> mark c f g f a() 1 >= 0 g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X c active X -> c X 0 + 0X >= 0 + 0X c mark X -> c X 0 + 0X >= 0 + 0X mark a() -> active a() 0 >= 1 mark g X -> active g mark X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark c X -> active c X 0 + 0X >= 1 + 0X SCCS (1): Scc: {g# mark X -> g# X} SCC (1): Strict: {g# mark X -> g# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g mark X, mark a() -> active a(), c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark c f g f a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [c](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0 + 1, [a] = 1, [g#](x0) = x0 Strict: g# mark X -> g# X 1 + 1X >= 0 + 1X Weak: active f f a() -> mark c f g f a() 4 >= 6 g active X -> g X 2 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X f active X -> f X 2 + 1X >= 1 + 1X f mark X -> f X 2 + 1X >= 1 + 1X c active X -> c X 2 + 1X >= 1 + 1X c mark X -> c X 2 + 1X >= 1 + 1X mark a() -> active a() 2 >= 2 mark g X -> active g mark X 2 + 1X >= 3 + 1X mark f X -> active f mark X 2 + 1X >= 3 + 1X mark c X -> active c X 2 + 1X >= 2 + 1X Qed SCC (2): Strict: { f# mark X -> f# X, f# active X -> f# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g mark X, mark a() -> active a(), c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark c f g f a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0, [c](x0) = 0, [f](x0) = 0, [g](x0) = 0, [active](x0) = x0 + 1, [a] = 0, [f#](x0) = x0 Strict: f# active X -> f# X 1 + 1X >= 0 + 1X f# mark X -> f# X 0 + 1X >= 0 + 1X Weak: active f f a() -> mark c f g f a() 1 >= 0 g active X -> g X 0 + 0X >= 0 + 0X g mark X -> g X 0 + 0X >= 0 + 0X f active X -> f X 0 + 0X >= 0 + 0X f mark X -> f X 0 + 0X >= 0 + 0X c active X -> c X 0 + 0X >= 0 + 0X c mark X -> c X 0 + 0X >= 0 + 0X mark a() -> active a() 0 >= 1 mark g X -> active g mark X 0 + 0X >= 1 + 0X mark f X -> active f mark X 0 + 0X >= 1 + 0X mark c X -> active c X 0 + 0X >= 1 + 0X SCCS (1): Scc: {f# mark X -> f# X} SCC (1): Strict: {f# mark X -> f# X} Weak: { mark c X -> active c X, mark f X -> active f mark X, mark g X -> active g mark X, mark a() -> active a(), c mark X -> c X, c active X -> c X, f mark X -> f X, f active X -> f X, g mark X -> g X, g active X -> g X, active f f a() -> mark c f g f a()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [mark](x0) = x0 + 1, [c](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0 + 1, [active](x0) = x0 + 1, [a] = 1, [f#](x0) = x0 Strict: f# mark X -> f# X 1 + 1X >= 0 + 1X Weak: active f f a() -> mark c f g f a() 4 >= 6 g active X -> g X 2 + 1X >= 1 + 1X g mark X -> g X 2 + 1X >= 1 + 1X f active X -> f X 2 + 1X >= 1 + 1X f mark X -> f X 2 + 1X >= 1 + 1X c active X -> c X 2 + 1X >= 1 + 1X c mark X -> c X 2 + 1X >= 1 + 1X mark a() -> active a() 2 >= 2 mark g X -> active g mark X 2 + 1X >= 3 + 1X mark f X -> active f mark X 2 + 1X >= 3 + 1X mark c X -> active c X 2 + 1X >= 2 + 1X Qed