MAYBE Time: 0.054754 TRS: { f(X1, mark X2, X3) -> mark f(X1, X2, X3), f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X1, X2, X3) -> f(X1, active X2, X3), active f(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b(), proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), proper c() -> ok c(), proper b() -> ok b(), top mark X -> top proper X, top ok X -> top active X} DP: DP: { f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), active# f(X1, X2, X3) -> f#(X1, active X2, X3), active# f(X1, X2, X3) -> active# X2, active# f(b(), X, c()) -> f#(X, c(), 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, top# mark X -> proper# X, top# mark X -> top# proper X, top# ok X -> active# X, top# ok X -> top# active X} TRS: { f(X1, mark X2, X3) -> mark f(X1, X2, X3), f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X1, X2, X3) -> f(X1, active X2, X3), active f(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b(), proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), proper c() -> ok c(), proper b() -> ok b(), top mark X -> top proper X, top ok X -> top active X} UR: { f(X1, mark X2, X3) -> mark f(X1, X2, X3), f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X1, X2, X3) -> f(X1, active X2, X3), active f(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b(), proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), proper c() -> ok c(), proper b() -> ok b(), a(x, y) -> x, a(x, y) -> y} EDG: {(proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper 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#(X1, mark X2, X3) -> f#(X1, X2, X3)) (top# ok X -> active# X, active# f(b(), X, c()) -> f#(X, c(), X)) (top# ok X -> active# X, active# f(X1, X2, X3) -> active# X2) (top# ok X -> active# X, active# f(X1, X2, X3) -> f#(X1, active X2, X3)) (active# f(X1, X2, X3) -> active# X2, active# f(b(), X, c()) -> f#(X, c(), X)) (active# f(X1, X2, X3) -> active# X2, active# f(X1, X2, X3) -> active# X2) (active# f(X1, X2, X3) -> active# X2, active# f(X1, X2, X3) -> f#(X1, active X2, X3)) (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)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)) (f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (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) (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) (f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)) (active# f(X1, X2, X3) -> f#(X1, active X2, X3), f#(X1, mark X2, X3) -> f#(X1, X2, X3)) (active# f(X1, X2, X3) -> f#(X1, active X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)) (proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> f#(proper X1, proper X2, proper X3)) (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) -> proper# X2) (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) -> f#(proper X1, proper X2, proper X3)) (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) -> proper# X2) (proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# 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)} STATUS: arrows: 0.775148 SCCS (4): Scc: {top# mark X -> top# proper X, top# ok X -> top# active X} Scc: {active# f(X1, X2, X3) -> active# X2} Scc: {proper# f(X1, X2, X3) -> proper# X1, proper# f(X1, X2, X3) -> proper# X2, proper# f(X1, X2, X3) -> proper# X3} Scc: { f#(X1, mark X2, X3) -> f#(X1, X2, X3), 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(X1, mark X2, X3) -> mark f(X1, X2, X3), f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X1, X2, X3) -> f(X1, active X2, X3), active f(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b(), proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), 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# f(X1, X2, X3) -> active# X2} Weak: { f(X1, mark X2, X3) -> mark f(X1, X2, X3), f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X1, X2, X3) -> f(X1, active X2, X3), active f(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b(), proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), 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, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = x0 + 1, [c] = 1, [b] = 1, [active#](x0) = x0 Strict: active# f(X1, X2, X3) -> active# X2 1 + 0X1 + 1X2 + 0X3 >= 0 + 1X2 Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 2 + 1X proper b() -> ok b() 2 >= 2 proper c() -> ok c() 2 >= 2 proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3) 2 + 0X1 + 1X2 + 0X3 >= 2 + 0X1 + 1X2 + 0X3 active c() -> mark b() 2 >= 2 active f(b(), X, c()) -> mark f(X, c(), X) 2 + 1X >= 3 + 0X active f(X1, X2, X3) -> f(X1, active X2, X3) 2 + 0X1 + 1X2 + 0X3 >= 2 + 0X1 + 1X2 + 0X3 f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3) 2 + 0X1 + 1X2 + 0X3 >= 2 + 0X1 + 1X2 + 0X3 f(X1, mark X2, X3) -> mark f(X1, X2, X3) 2 + 0X1 + 1X2 + 0X3 >= 2 + 0X1 + 1X2 + 0X3 Qed 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(X1, mark X2, X3) -> mark f(X1, X2, X3), f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X1, X2, X3) -> f(X1, active X2, X3), active f(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b(), proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), 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) = 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 f(X1, X2, X3) -> f(proper X1, proper X2, proper X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3 active c() -> mark b() 2 >= 2 active f(b(), X, c()) -> mark f(X, c(), X) 4 + 1X >= 3 + 2X active f(X1, X2, X3) -> f(X1, active X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3) 4 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 f(X1, mark X2, X3) -> mark f(X1, X2, X3) 2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3 Qed SCC (2): Strict: { f#(X1, mark X2, X3) -> f#(X1, X2, X3), f#(ok X1, ok X2, ok X3) -> f#(X1, X2, X3)} Weak: { f(X1, mark X2, X3) -> mark f(X1, X2, X3), f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X1, X2, X3) -> f(X1, active X2, X3), active f(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b(), proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), 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, [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 f#(X1, mark X2, X3) -> f#(X1, X2, X3) 0 + 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 f(X1, X2, X3) -> f(proper X1, proper X2, proper X3) 2 + 0X1 + 1X2 + 0X3 >= 2 + 0X1 + 1X2 + 0X3 active c() -> mark b() 2 >= 2 active f(b(), X, c()) -> mark f(X, c(), X) 2 + 1X >= 3 + 0X active f(X1, X2, X3) -> f(X1, active X2, X3) 2 + 0X1 + 1X2 + 0X3 >= 2 + 0X1 + 1X2 + 0X3 f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3) 2 + 0X1 + 1X2 + 0X3 >= 2 + 0X1 + 1X2 + 0X3 f(X1, mark X2, X3) -> mark f(X1, X2, X3) 2 + 0X1 + 1X2 + 0X3 >= 2 + 0X1 + 1X2 + 0X3 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: { f(X1, mark X2, X3) -> mark f(X1, X2, X3), f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3), active f(X1, X2, X3) -> f(X1, active X2, X3), active f(b(), X, c()) -> mark f(X, c(), X), active c() -> mark b(), proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3), 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, [proper](x0) = x0 + 1, [ok](x0) = x0 + 1, [top](x0) = x0 + 1, [c] = 1, [b] = 1, [f#](x0, x1, x2) = x0 Strict: f#(X1, mark X2, X3) -> f#(X1, X2, X3) 1 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3 Weak: top ok X -> top active X 2 + 1X >= 2 + 1X top mark X -> top proper X 2 + 1X >= 2 + 1X proper b() -> ok b() 2 >= 2 proper c() -> ok c() 2 >= 2 proper f(X1, X2, X3) -> f(proper X1, proper X2, proper X3) 2 + 0X1 + 1X2 + 0X3 >= 2 + 0X1 + 1X2 + 0X3 active c() -> mark b() 2 >= 2 active f(b(), X, c()) -> mark f(X, c(), X) 2 + 1X >= 3 + 0X active f(X1, X2, X3) -> f(X1, active X2, X3) 2 + 0X1 + 1X2 + 0X3 >= 2 + 0X1 + 1X2 + 0X3 f(ok X1, ok X2, ok X3) -> ok f(X1, X2, X3) 2 + 0X1 + 1X2 + 0X3 >= 2 + 0X1 + 1X2 + 0X3 f(X1, mark X2, X3) -> mark f(X1, X2, X3) 2 + 0X1 + 1X2 + 0X3 >= 2 + 0X1 + 1X2 + 0X3 Qed