MAYBE Time: 0.087435 TRS: {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g X -> g active X, active g b() -> mark c(), active b() -> mark c(), g mark X -> mark g X, g ok X -> ok g X, proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), proper g X -> g proper X, proper c() -> ok c(), proper b() -> ok b(), top mark X -> top proper X, top ok X -> top active X} DP: DP: {f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), active# f(X, g X, Y) -> f#(Y, Y, Y), active# g X -> active# X, active# g X -> g# active X, g# mark X -> g# X, g# ok X -> g# X, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X3, proper# g X -> g# proper X, proper# g X -> proper# X, top# mark X -> proper# X, top# mark X -> top# proper X, top# ok X -> active# X, top# ok X -> top# active X} TRS: {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g X -> g active X, active g b() -> mark c(), active b() -> mark c(), g mark X -> mark g X, g ok X -> ok g X, proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), proper g X -> g proper X, proper c() -> ok c(), proper b() -> ok b(), top mark X -> top proper X, top ok X -> top active X} EDG: {(active# g X -> g# active X, g# ok X -> g# X) (active# g X -> g# active X, g# mark X -> g# X) (top# mark X -> top# proper X, top# ok X -> top# active X) (top# mark X -> top# proper X, top# ok X -> active# X) (top# mark X -> top# proper X, top# mark X -> top# proper X) (top# mark X -> top# proper X, top# mark X -> proper# X) (proper# f(X1, X2, X3) -> proper# X3, proper# g X -> proper# X) (proper# f(X1, X2, X3) -> proper# X3, proper# g X -> g# proper X) (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X3) (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X2) (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> proper# X1) (proper# f(X1, X2, X3) -> proper# X3, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3)) (g# mark X -> g# X, g# ok X -> g# X) (g# mark X -> g# X, g# mark X -> g# X) (proper# g X -> proper# X, proper# g X -> proper# X) (proper# g X -> proper# X, proper# g X -> g# proper X) (proper# g X -> proper# X, proper# f(X1, X2, X3) -> proper# X3) (proper# g X -> proper# X, proper# f(X1, X2, X3) -> proper# X2) (proper# g X -> proper# X, proper# f(X1, X2, X3) -> proper# X1) (proper# g X -> proper# X, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3)) (top# ok X -> active# X, active# g X -> g# active X) (top# ok X -> active# X, active# g X -> active# X) (top# ok X -> active# X, active# f(X, g X, Y) -> f#(Y, Y, Y)) (proper# f(X1, X2, X3) -> proper# X1, proper# g X -> proper# X) (proper# f(X1, X2, X3) -> proper# X1, proper# g X -> g# proper X) (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X3) (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X2) (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X1) (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3)) (proper# f(X1, X2, X3) -> proper# X2, proper# g X -> proper# X) (proper# f(X1, X2, X3) -> proper# X2, proper# g X -> g# proper X) (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X3) (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X2) (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X1) (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3)) (f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)) (proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)) (top# mark X -> proper# X, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3)) (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X1) (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X2) (top# mark X -> proper# X, proper# f(X1, X2, X3) -> proper# X3) (top# mark X -> proper# X, proper# g X -> g# proper X) (top# mark X -> proper# X, proper# g X -> proper# X) (g# ok X -> g# X, g# mark X -> g# X) (g# ok X -> g# X, g# ok X -> g# X) (active# g X -> active# X, active# f(X, g X, Y) -> f#(Y, Y, Y)) (active# g X -> active# X, active# g X -> active# X) (active# g X -> active# X, active# g X -> g# active X) (top# ok X -> top# active X, top# mark X -> proper# X) (top# ok X -> top# active X, top# mark X -> top# proper X) (top# ok X -> top# active X, top# ok X -> active# X) (top# ok X -> top# active X, top# ok X -> top# active X) (proper# g X -> g# proper X, g# mark X -> g# X) (proper# g X -> g# proper X, g# ok X -> g# X) (active# f(X, g X, Y) -> f#(Y, Y, Y), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3))} STATUS: arrows: 0.785156 SCCS (5): Scc: {top# mark X -> top# proper X, top# ok X -> top# active X} Scc: {active# g X -> active# X} Scc: {proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X3, proper# g X -> proper# X} Scc: {g# mark X -> g# X, g# ok X -> g# X} Scc: {f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)} SCC (2): Strict: {top# mark X -> top# proper X, top# ok X -> top# active X} Weak: {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g X -> g active X, active g b() -> mark c(), active b() -> mark c(), g mark X -> mark g X, g ok X -> ok g X, proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), proper g X -> g proper X, proper c() -> ok c(), proper b() -> ok b(), top mark X -> top proper X, top ok X -> top active X} Fail SCC (1): Strict: {active# g X -> active# X} Weak: {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g X -> g active X, active g b() -> mark c(), active b() -> mark c(), g mark X -> mark g X, g ok X -> ok g X, proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), proper g X -> g proper X, proper c() -> ok c(), proper b() -> ok b(), top mark X -> top proper X, top ok X -> top active X} 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 + 1, [g](x0) = x0 + 1, [proper](x0) = 0, [ok](x0) = x0 + 1, [top](x0) = x0 + 1, [c] = 1, [b] = 0, [active#](x0) = x0 Strict: active# g X -> active# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 1 + 0X proper b() -> ok b() 0 >= 1 proper c() -> ok c() 0 >= 2 proper g X -> g proper X 0 + 0X >= 1 + 0X proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 g ok X -> ok g X 2 + 1X >= 2 + 1X g mark X -> mark g X 2 + 1X >= 2 + 1X active b() -> mark c() 1 >= 2 active g b() -> mark c() 2 >= 2 active g X -> g active X 2 + 1X >= 2 + 1X active f(X, g X, Y) -> mark f(Y, Y, Y) 2 + 1Y + 0X >= 2 + 1Y f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3) 2 + 0X1 + 0X2 + 1X3 >= 2 + 0X1 + 0X2 + 1X3 Qed SCC (4): Strict: {proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X3, proper# g X -> proper# X} Weak: {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g X -> g active X, active g b() -> mark c(), active b() -> mark c(), g mark X -> mark g X, g ok X -> ok g X, proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), proper g X -> g proper X, proper c() -> ok c(), proper b() -> ok b(), top mark X -> top proper X, top ok X -> top active X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2) = x0 + x1 + x2, [mark](x0) = 0, [active](x0) = x0 + 1, [g](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = 0, [top](x0) = 0, [c] = 1, [b] = 0, [proper#](x0) = x0 Strict: proper# g X -> proper# X 1 + 1X >= 0 + 1X proper# f(X1, X2, X3) -> proper# X3 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X3 proper# f(X1, X2, X3) -> proper# X2 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X2 proper# f(X1, X2, X3) -> proper# X1 0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper b() -> ok b() 1 >= 0 proper c() -> ok c() 2 >= 0 proper g X -> g proper X 2 + 1X >= 2 + 1X proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3) 1 + 1X1 + 1X2 + 1X3 >= 3 + 1X1 + 1X2 + 1X3 g ok X -> ok g X 1 + 0X >= 0 + 0X g mark X -> mark g X 1 + 0X >= 0 + 0X active b() -> mark c() 1 >= 0 active g b() -> mark c() 2 >= 0 active g X -> g active X 2 + 1X >= 2 + 1X active f(X, g X, Y) -> mark f(Y, Y, Y) 2 + 1Y + 2X >= 0 + 0Y f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 SCCS (1): Scc: {proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X3} SCC (3): Strict: {proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X3} Weak: {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g X -> g active X, active g b() -> mark c(), active b() -> mark c(), g mark X -> mark g X, g ok X -> ok g X, proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), proper g X -> g proper X, proper c() -> ok c(), proper b() -> ok b(), top mark X -> top proper X, top ok X -> top active 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) = 0, [g](x0) = x0 + 1, [proper](x0) = 0, [ok](x0) = x0 + 1, [top](x0) = 0, [c] = 1, [b] = 1, [proper#](x0) = x0 + 1 Strict: proper# f(X1, X2, X3) -> proper# X3 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X3 proper# f(X1, X2, X3) -> proper# X2 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X2 proper# f(X1, X2, X3) -> proper# X1 2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper b() -> ok b() 0 >= 2 proper c() -> ok c() 0 >= 2 proper g X -> g proper X 0 + 0X >= 1 + 0X proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 g ok X -> ok g X 2 + 1X >= 2 + 1X g mark X -> mark g X 2 + 1X >= 2 + 1X active b() -> mark c() 0 >= 2 active g b() -> mark c() 0 >= 2 active g X -> g active X 0 + 0X >= 1 + 0X active f(X, g X, Y) -> mark f(Y, Y, Y) 0 + 0Y + 0X >= 2 + 3Y f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3) 4 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 Qed SCC (2): Strict: {g# mark X -> g# X, g# ok X -> g# X} Weak: {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g X -> g active X, active g b() -> mark c(), active b() -> mark c(), g mark X -> mark g X, g ok X -> ok g X, proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), proper g X -> g proper X, proper c() -> ok c(), proper b() -> ok b(), top mark X -> top proper X, top ok X -> top active 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) = x0 + 1, [proper](x0) = 0, [ok](x0) = x0 + 1, [top](x0) = 0, [c] = 0, [b] = 0, [g#](x0) = x0 Strict: g# ok X -> g# X 1 + 1X >= 0 + 1X g# mark X -> g# X 0 + 1X >= 0 + 1X Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper b() -> ok b() 0 >= 1 proper c() -> ok c() 0 >= 1 proper g X -> g proper X 0 + 0X >= 1 + 0X proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 g ok X -> ok g X 2 + 1X >= 2 + 1X g mark X -> mark g X 1 + 1X >= 1 + 1X active b() -> mark c() 1 >= 0 active g b() -> mark c() 2 >= 0 active g X -> g active X 2 + 1X >= 2 + 1X active f(X, g X, Y) -> mark f(Y, Y, Y) 2 + 1Y + 0X >= 1 + 1Y f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3) 2 + 0X1 + 0X2 + 1X3 >= 2 + 0X1 + 0X2 + 1X3 SCCS (1): Scc: {g# mark X -> g# X} SCC (1): Strict: {g# mark X -> g# X} Weak: {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g X -> g active X, active g b() -> mark c(), active b() -> mark c(), g mark X -> mark g X, g ok X -> ok g X, proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), proper g X -> g proper X, proper c() -> ok c(), proper b() -> ok b(), top mark X -> top proper X, top ok X -> top active X} 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 + 1, [g](x0) = x0 + 1, [proper](x0) = 0, [ok](x0) = x0 + 1, [top](x0) = x0 + 1, [c] = 1, [b] = 0, [g#](x0) = x0 Strict: g# mark X -> g# X 1 + 1X >= 0 + 1X Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 1 + 0X proper b() -> ok b() 0 >= 1 proper c() -> ok c() 0 >= 2 proper g X -> g proper X 0 + 0X >= 1 + 0X proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 g ok X -> ok g X 2 + 1X >= 2 + 1X g mark X -> mark g X 2 + 1X >= 2 + 1X active b() -> mark c() 1 >= 2 active g b() -> mark c() 2 >= 2 active g X -> g active X 2 + 1X >= 2 + 1X active f(X, g X, Y) -> mark f(Y, Y, Y) 2 + 1Y + 0X >= 2 + 1Y f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3) 2 + 0X1 + 0X2 + 1X3 >= 2 + 0X1 + 0X2 + 1X3 Qed SCC (1): Strict: {f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)} Weak: {f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X, g X, Y) -> mark f(Y, Y, Y), active g X -> g active X, active g b() -> mark c(), active b() -> mark c(), g mark X -> mark g X, g ok X -> ok g X, proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), proper g X -> g proper X, proper c() -> ok c(), proper b() -> ok b(), top mark X -> top proper X, top ok X -> top active 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) = 0, [g](x0) = x0 + 1, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = 0, [c] = 1, [b] = 1, [f#](x0, x1, x2) = x0 Strict: f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3) 1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3 Weak: top ok X -> top active X 0 + 0X >= 0 + 0X top mark X -> top proper X 0 + 0X >= 0 + 0X proper b() -> ok b() 2 >= 2 proper c() -> ok c() 2 >= 2 proper g X -> g proper X 2 + 1X >= 2 + 1X proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3) 2 + 1X1 + 1X2 + 1X3 >= 4 + 1X1 + 1X2 + 1X3 g ok X -> ok g X 2 + 1X >= 2 + 1X g mark X -> mark g X 2 + 1X >= 2 + 1X active b() -> mark c() 0 >= 2 active g b() -> mark c() 0 >= 2 active g X -> g active X 0 + 0X >= 1 + 0X active f(X, g X, Y) -> mark f(Y, Y, Y) 0 + 0Y + 0X >= 2 + 3Y f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3) 4 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 Qed