MAYBE Time: 1.563984 TRS: { f(x, y, mark z) -> mark f(x, y, z), f(ok x, ok y, ok z) -> ok f(x, y, z), active f(x, y, z) -> f(x, y, active z), active f(b(), c(), x) -> mark f(x, x, x), active d() -> mark c(), active d() -> m b(), proper f(x, y, z) -> f(proper x, proper y, proper z), proper b() -> ok b(), proper c() -> ok c(), proper d() -> ok d(), top mark x -> top proper x, top ok x -> top active x} DP: DP: { f#(x, y, mark z) -> f#(x, y, z), f#(ok x, ok y, ok z) -> f#(x, y, z), active# f(x, y, z) -> f#(x, y, active z), active# f(x, y, z) -> active# z, active# f(b(), c(), x) -> f#(x, x, x), proper# f(x, y, z) -> f#(proper x, proper y, proper z), proper# f(x, y, z) -> proper# x, proper# f(x, y, z) -> proper# y, proper# f(x, y, z) -> proper# z, top# mark x -> proper# x, top# mark x -> top# proper x, top# ok x -> active# x, top# ok x -> top# active x} TRS: { f(x, y, mark z) -> mark f(x, y, z), f(ok x, ok y, ok z) -> ok f(x, y, z), active f(x, y, z) -> f(x, y, active z), active f(b(), c(), x) -> mark f(x, x, x), active d() -> mark c(), active d() -> m b(), proper f(x, y, z) -> f(proper x, proper y, proper z), proper b() -> ok b(), proper c() -> ok c(), proper d() -> ok d(), top mark x -> top proper x, top ok x -> top active x} UR: { f(x, y, mark z) -> mark f(x, y, z), f(ok x, ok y, ok z) -> ok f(x, y, z), active f(x, y, z) -> f(x, y, active z), active f(b(), c(), x) -> mark f(x, x, x), active d() -> mark c(), active d() -> m b(), proper f(x, y, z) -> f(proper x, proper y, proper z), proper b() -> ok b(), proper c() -> ok c(), proper d() -> ok d(), a(w, v) -> w, a(w, v) -> v} EDG: {(active# f(x, y, z) -> f#(x, y, active z), f#(ok x, ok y, ok z) -> f#(x, y, z)) (active# f(x, y, z) -> f#(x, y, active z), f#(x, y, mark z) -> f#(x, y, z)) (proper# f(x, y, z) -> proper# x, proper# f(x, y, z) -> proper# z) (proper# f(x, y, z) -> proper# x, proper# f(x, y, z) -> proper# y) (proper# f(x, y, z) -> proper# x, proper# f(x, y, z) -> proper# x) (proper# f(x, y, z) -> proper# x, proper# f(x, y, z) -> f#(proper x, proper y, proper z)) (top# ok x -> active# x, active# f(b(), c(), x) -> f#(x, x, x)) (top# ok x -> active# x, active# f(x, y, z) -> active# z) (top# ok x -> active# x, active# f(x, y, z) -> f#(x, y, active z)) (f#(x, y, mark z) -> f#(x, y, z), f#(ok x, ok y, ok z) -> f#(x, y, z)) (f#(x, y, mark z) -> f#(x, y, z), f#(x, y, mark z) -> f#(x, y, z)) (active# f(x, y, z) -> active# z, active# f(b(), c(), x) -> f#(x, x, x)) (active# f(x, y, z) -> active# z, active# f(x, y, z) -> active# z) (active# f(x, y, z) -> active# z, active# f(x, y, z) -> f#(x, y, active z)) (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) (proper# f(x, y, z) -> proper# z, proper# f(x, y, z) -> f#(proper x, proper y, proper z)) (proper# f(x, y, z) -> proper# z, proper# f(x, y, z) -> proper# x) (proper# f(x, y, z) -> proper# z, proper# f(x, y, z) -> proper# y) (proper# f(x, y, z) -> proper# z, proper# f(x, y, z) -> proper# z) (f#(ok x, ok y, ok z) -> f#(x, y, z), f#(x, y, mark z) -> f#(x, y, z)) (f#(ok x, ok y, ok z) -> f#(x, y, z), f#(ok x, ok y, ok z) -> f#(x, y, z)) (proper# f(x, y, z) -> proper# y, proper# f(x, y, z) -> f#(proper x, proper y, proper z)) (proper# f(x, y, z) -> proper# y, proper# f(x, y, z) -> proper# x) (proper# f(x, y, z) -> proper# y, proper# f(x, y, z) -> proper# y) (proper# f(x, y, z) -> proper# y, proper# f(x, y, z) -> proper# z) (top# mark x -> proper# x, proper# f(x, y, z) -> f#(proper x, proper y, proper z)) (top# mark x -> proper# x, proper# f(x, y, z) -> proper# x) (top# mark x -> proper# x, proper# f(x, y, z) -> proper# y) (top# mark x -> proper# x, proper# f(x, y, z) -> proper# z) (proper# f(x, y, z) -> f#(proper x, proper y, proper z), f#(x, y, mark z) -> f#(x, y, z)) (proper# f(x, y, z) -> f#(proper x, proper y, proper z), f#(ok x, ok y, ok z) -> f#(x, y, z)) (active# f(b(), c(), x) -> f#(x, x, x), f#(x, y, mark z) -> f#(x, y, z)) (active# f(b(), c(), x) -> f#(x, x, x), f#(ok x, ok y, ok z) -> f#(x, y, z))} STATUS: arrows: 0.763314 SCCS (4): Scc: {top# mark x -> top# proper x, top# ok x -> top# active x} Scc: {active# f(x, y, z) -> active# z} Scc: {proper# f(x, y, z) -> proper# x, proper# f(x, y, z) -> proper# y, proper# f(x, y, z) -> proper# z} Scc: { f#(x, y, mark z) -> f#(x, y, z), f#(ok x, ok y, ok z) -> f#(x, y, z)} SCC (2): Strict: {top# mark x -> top# proper x, top# ok x -> top# active x} Weak: { f(x, y, mark z) -> mark f(x, y, z), f(ok x, ok y, ok z) -> ok f(x, y, z), active f(x, y, z) -> f(x, y, active z), active f(b(), c(), x) -> mark f(x, x, x), active d() -> mark c(), active d() -> m b(), proper f(x, y, z) -> f(proper x, proper y, proper z), proper b() -> ok b(), proper c() -> ok c(), proper d() -> ok d(), top mark x -> top proper x, top ok x -> top active x} Fail SCC (1): Strict: {active# f(x, y, z) -> active# z} Weak: { f(x, y, mark z) -> mark f(x, y, z), f(ok x, ok y, ok z) -> ok f(x, y, z), active f(x, y, z) -> f(x, y, active z), active f(b(), c(), x) -> mark f(x, x, x), active d() -> mark c(), active d() -> m b(), proper f(x, y, z) -> f(proper x, proper y, proper z), proper b() -> ok b(), proper c() -> ok c(), proper d() -> ok d(), 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, [m](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = 0, [top](x0) = x0 + 1, [b] = 1, [c] = 0, [d] = 1, [active#](x0) = x0 Strict: active# f(x, y, z) -> active# z 1 + 0x + 0y + 1z >= 0 + 1z Weak: top ok x -> top active x 2 + 1x >= 2 + 1x top mark x -> top proper x 2 + 1x >= 1 + 0x proper d() -> ok d() 0 >= 2 proper c() -> ok c() 0 >= 1 proper b() -> ok b() 0 >= 2 proper f(x, y, z) -> f(proper x, proper y, proper z) 0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z active d() -> m b() 2 >= 0 active d() -> mark c() 2 >= 1 active f(b(), c(), x) -> mark f(x, x, x) 2 + 1x >= 2 + 1x active f(x, y, z) -> f(x, y, active z) 2 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z f(ok x, ok y, ok z) -> ok f(x, y, z) 2 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z f(x, y, mark z) -> mark f(x, y, z) 2 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z Qed SCC (3): Strict: {proper# f(x, y, z) -> proper# x, proper# f(x, y, z) -> proper# y, proper# f(x, y, z) -> proper# z} Weak: { f(x, y, mark z) -> mark f(x, y, z), f(ok x, ok y, ok z) -> ok f(x, y, z), active f(x, y, z) -> f(x, y, active z), active f(b(), c(), x) -> mark f(x, x, x), active d() -> mark c(), active d() -> m b(), proper f(x, y, z) -> f(proper x, proper y, proper z), proper b() -> ok b(), proper c() -> ok c(), proper d() -> ok d(), 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, [m](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = 0, [top](x0) = 0, [b] = 1, [c] = 1, [d] = 1, [proper#](x0) = x0 + 1 Strict: proper# f(x, y, z) -> proper# z 2 + 1x + 1y + 1z >= 1 + 1z proper# f(x, y, z) -> proper# y 2 + 1x + 1y + 1z >= 1 + 1y proper# f(x, y, z) -> proper# x 2 + 1x + 1y + 1z >= 1 + 1x Weak: top ok x -> top active x 0 + 0x >= 0 + 0x top mark x -> top proper x 0 + 0x >= 0 + 0x proper d() -> ok d() 0 >= 2 proper c() -> ok c() 0 >= 2 proper b() -> ok b() 0 >= 2 proper f(x, y, z) -> f(proper x, proper y, proper z) 0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z active d() -> m b() 2 >= 0 active d() -> mark c() 2 >= 2 active f(b(), c(), x) -> mark f(x, x, x) 4 + 1x >= 2 + 3x active f(x, y, z) -> f(x, y, active z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z f(ok x, ok y, ok z) -> ok f(x, y, z) 4 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z f(x, y, mark z) -> mark f(x, y, z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z Qed SCC (2): Strict: { f#(x, y, mark z) -> f#(x, y, z), f#(ok x, ok y, ok z) -> f#(x, y, z)} Weak: { f(x, y, mark z) -> mark f(x, y, z), f(ok x, ok y, ok z) -> ok f(x, y, z), active f(x, y, z) -> f(x, y, active z), active f(b(), c(), x) -> mark f(x, x, x), active d() -> mark c(), active d() -> m b(), proper f(x, y, z) -> f(proper x, proper y, proper z), proper b() -> ok b(), proper c() -> ok c(), proper d() -> ok d(), 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, [m](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = 0, [top](x0) = 0, [b] = 1, [c] = 1, [d] = 1, [f#](x0, x1, x2) = x0 Strict: f#(ok x, ok y, ok z) -> f#(x, y, z) 1 + 0x + 1y + 0z >= 0 + 0x + 1y + 0z f#(x, y, mark z) -> f#(x, y, z) 0 + 0x + 1y + 0z >= 0 + 0x + 1y + 0z Weak: top ok x -> top active x 0 + 0x >= 0 + 0x top mark x -> top proper x 0 + 0x >= 0 + 0x proper d() -> ok d() 0 >= 2 proper c() -> ok c() 0 >= 2 proper b() -> ok b() 0 >= 2 proper f(x, y, z) -> f(proper x, proper y, proper z) 0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z active d() -> m b() 2 >= 0 active d() -> mark c() 2 >= 2 active f(b(), c(), x) -> mark f(x, x, x) 2 + 1x >= 2 + 1x active f(x, y, z) -> f(x, y, active z) 2 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z f(ok x, ok y, ok z) -> ok f(x, y, z) 2 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z f(x, y, mark z) -> mark f(x, y, z) 2 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z SCCS (1): Scc: {f#(x, y, mark z) -> f#(x, y, z)} SCC (1): Strict: {f#(x, y, mark z) -> f#(x, y, z)} Weak: { f(x, y, mark z) -> mark f(x, y, z), f(ok x, ok y, ok z) -> ok f(x, y, z), active f(x, y, z) -> f(x, y, active z), active f(b(), c(), x) -> mark f(x, x, x), active d() -> mark c(), active d() -> m b(), proper f(x, y, z) -> f(proper x, proper y, proper z), proper b() -> ok b(), proper c() -> ok c(), proper d() -> ok d(), 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, [m](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = 0, [top](x0) = x0 + 1, [b] = 1, [c] = 0, [d] = 1, [f#](x0, x1, x2) = x0 Strict: f#(x, y, mark z) -> f#(x, y, z) 1 + 0x + 0y + 1z >= 0 + 0x + 0y + 1z Weak: top ok x -> top active x 2 + 1x >= 2 + 1x top mark x -> top proper x 2 + 1x >= 1 + 0x proper d() -> ok d() 0 >= 2 proper c() -> ok c() 0 >= 1 proper b() -> ok b() 0 >= 2 proper f(x, y, z) -> f(proper x, proper y, proper z) 0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z active d() -> m b() 2 >= 0 active d() -> mark c() 2 >= 1 active f(b(), c(), x) -> mark f(x, x, x) 2 + 1x >= 2 + 1x active f(x, y, z) -> f(x, y, active z) 2 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z f(ok x, ok y, ok z) -> ok f(x, y, z) 2 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z f(x, y, mark z) -> mark f(x, y, z) 2 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z Qed