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