MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ f1() -> g1()
, f1() -> g2()
, g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, f2() -> g1()
, f2() -> g2()
, h1() -> i()
, h2() -> i()
, e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e2(x, x, y, z, z) -> e6(x, y, z)
, e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z)
, e2(i(), x, y, z, i()) -> e6(x, y, z)
, e5(i(), x, y, z) -> e6(x, y, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
, e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
, e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
e1(x1, x1, x, y, z)
, e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
e5(x1, x, y, z) }
Obligation:
runtime complexity
Answer:
MAYBE
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 60 seconds)' failed due to the
following reason:
Computation stopped due to timeout after 60.0 seconds.
2) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
failed due to the following reason:
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
none
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[f1] = [7]
[g1] = [7]
[g2] = [7]
[f2] = [7]
[h1] = [7]
[h2] = [7]
[i] = [0]
[e1](x1, x2, x3, x4, x5) = [1] x5 + [7]
[e2](x1, x2, x3, x4, x5) = [1] x4 + [7]
[e5](x1, x2, x3, x4) = [1] x4 + [7]
[e3](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1] x11 + [6]
[e6](x1, x2, x3) = [1] x3 + [4]
[e4](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1] x11 + [7]
The following symbols are considered usable
{f1, g1, g2, f2, h1, h2, e1, e2, e5, e3, e4}
The order satisfies the following ordering constraints:
[f1()] = [7]
>= [7]
= [g1()]
[f1()] = [7]
>= [7]
= [g2()]
[g1()] = [7]
>= [7]
= [h1()]
[g1()] = [7]
>= [7]
= [h2()]
[g2()] = [7]
>= [7]
= [h1()]
[g2()] = [7]
>= [7]
= [h2()]
[f2()] = [7]
>= [7]
= [g1()]
[f2()] = [7]
>= [7]
= [g2()]
[h1()] = [7]
> [0]
= [i()]
[h2()] = [7]
> [0]
= [i()]
[e1(x1, x1, x, y, z)] = [1] z + [7]
>= [1] z + [7]
= [e5(x1, x, y, z)]
[e1(h1(), h2(), x, y, z)] = [1] z + [7]
>= [1] z + [7]
= [e2(x, x, y, z, z)]
[e2(x, x, y, z, z)] = [1] z + [7]
> [1] z + [4]
= [e6(x, y, z)]
[e2(f1(), x, y, z, f2())] = [1] z + [7]
> [1] z + [6]
= [e3(x, y, x, y, y, z, y, z, x, y, z)]
[e2(i(), x, y, z, i())] = [1] z + [7]
> [1] z + [4]
= [e6(x, y, z)]
[e5(i(), x, y, z)] = [1] z + [7]
> [1] z + [4]
= [e6(x, y, z)]
[e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)] = [1] z + [6]
? [1] z + [7]
= [e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)]
[e3(x, y, x, y, y, z, y, z, x, y, z)] = [1] z + [6]
> [1] z + [4]
= [e6(x, y, z)]
[e4(x, x, x, x, x, x, x, x, x, x, x)] = [1] x + [7]
> [1] x + [4]
= [e6(x, x, x)]
[e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z)] = [1] z + [7]
>= [1] z + [7]
= [e1(x1, x1, x, y, z)]
[e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z)] = [1] z + [7]
>= [1] z + [7]
= [e5(x1, x, y, z)]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ f1() -> g1()
, f1() -> g2()
, g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, f2() -> g1()
, f2() -> g2()
, e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
e1(x1, x1, x, y, z)
, e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
e5(x1, x, y, z) }
Weak Trs:
{ h1() -> i()
, h2() -> i()
, e2(x, x, y, z, z) -> e6(x, y, z)
, e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z)
, e2(i(), x, y, z, i()) -> e6(x, y, z)
, e5(i(), x, y, z) -> e6(x, y, z)
, e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
, e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x) }
Obligation:
runtime complexity
Answer:
MAYBE
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
none
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[f1] = [7]
[g1] = [7]
[g2] = [7]
[f2] = [7]
[h1] = [7]
[h2] = [7]
[i] = [0]
[e1](x1, x2, x3, x4, x5) = [1] x5 + [7]
[e2](x1, x2, x3, x4, x5) = [1] x4 + [6]
[e5](x1, x2, x3, x4) = [1] x4 + [6]
[e3](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1] x11 + [6]
[e6](x1, x2, x3) = [1] x3 + [5]
[e4](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1] x11 + [7]
The following symbols are considered usable
{f1, g1, g2, f2, h1, h2, e1, e2, e5, e3, e4}
The order satisfies the following ordering constraints:
[f1()] = [7]
>= [7]
= [g1()]
[f1()] = [7]
>= [7]
= [g2()]
[g1()] = [7]
>= [7]
= [h1()]
[g1()] = [7]
>= [7]
= [h2()]
[g2()] = [7]
>= [7]
= [h1()]
[g2()] = [7]
>= [7]
= [h2()]
[f2()] = [7]
>= [7]
= [g1()]
[f2()] = [7]
>= [7]
= [g2()]
[h1()] = [7]
> [0]
= [i()]
[h2()] = [7]
> [0]
= [i()]
[e1(x1, x1, x, y, z)] = [1] z + [7]
> [1] z + [6]
= [e5(x1, x, y, z)]
[e1(h1(), h2(), x, y, z)] = [1] z + [7]
> [1] z + [6]
= [e2(x, x, y, z, z)]
[e2(x, x, y, z, z)] = [1] z + [6]
> [1] z + [5]
= [e6(x, y, z)]
[e2(f1(), x, y, z, f2())] = [1] z + [6]
>= [1] z + [6]
= [e3(x, y, x, y, y, z, y, z, x, y, z)]
[e2(i(), x, y, z, i())] = [1] z + [6]
> [1] z + [5]
= [e6(x, y, z)]
[e5(i(), x, y, z)] = [1] z + [6]
> [1] z + [5]
= [e6(x, y, z)]
[e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)] = [1] z + [6]
? [1] z + [7]
= [e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)]
[e3(x, y, x, y, y, z, y, z, x, y, z)] = [1] z + [6]
> [1] z + [5]
= [e6(x, y, z)]
[e4(x, x, x, x, x, x, x, x, x, x, x)] = [1] x + [7]
> [1] x + [5]
= [e6(x, x, x)]
[e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z)] = [1] z + [7]
>= [1] z + [7]
= [e1(x1, x1, x, y, z)]
[e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z)] = [1] z + [7]
> [1] z + [6]
= [e5(x1, x, y, z)]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ f1() -> g1()
, f1() -> g2()
, g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, f2() -> g1()
, f2() -> g2()
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
e1(x1, x1, x, y, z) }
Weak Trs:
{ h1() -> i()
, h2() -> i()
, e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e2(x, x, y, z, z) -> e6(x, y, z)
, e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z)
, e2(i(), x, y, z, i()) -> e6(x, y, z)
, e5(i(), x, y, z) -> e6(x, y, z)
, e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
, e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
, e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
e5(x1, x, y, z) }
Obligation:
runtime complexity
Answer:
MAYBE
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
none
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[f1] = [7]
[g1] = [0]
[g2] = [0]
[f2] = [7]
[h1] = [4]
[h2] = [4]
[i] = [0]
[e1](x1, x2, x3, x4, x5) = [1] x5 + [5]
[e2](x1, x2, x3, x4, x5) = [1] x4 + [4]
[e5](x1, x2, x3, x4) = [1] x4 + [0]
[e3](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1] x11 + [3]
[e6](x1, x2, x3) = [1] x3 + [0]
[e4](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1] x11 + [0]
The following symbols are considered usable
{f1, g1, g2, f2, h1, h2, e1, e2, e5, e3, e4}
The order satisfies the following ordering constraints:
[f1()] = [7]
> [0]
= [g1()]
[f1()] = [7]
> [0]
= [g2()]
[g1()] = [0]
? [4]
= [h1()]
[g1()] = [0]
? [4]
= [h2()]
[g2()] = [0]
? [4]
= [h1()]
[g2()] = [0]
? [4]
= [h2()]
[f2()] = [7]
> [0]
= [g1()]
[f2()] = [7]
> [0]
= [g2()]
[h1()] = [4]
> [0]
= [i()]
[h2()] = [4]
> [0]
= [i()]
[e1(x1, x1, x, y, z)] = [1] z + [5]
> [1] z + [0]
= [e5(x1, x, y, z)]
[e1(h1(), h2(), x, y, z)] = [1] z + [5]
> [1] z + [4]
= [e2(x, x, y, z, z)]
[e2(x, x, y, z, z)] = [1] z + [4]
> [1] z + [0]
= [e6(x, y, z)]
[e2(f1(), x, y, z, f2())] = [1] z + [4]
> [1] z + [3]
= [e3(x, y, x, y, y, z, y, z, x, y, z)]
[e2(i(), x, y, z, i())] = [1] z + [4]
> [1] z + [0]
= [e6(x, y, z)]
[e5(i(), x, y, z)] = [1] z + [0]
>= [1] z + [0]
= [e6(x, y, z)]
[e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)] = [1] z + [3]
> [1] z + [0]
= [e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)]
[e3(x, y, x, y, y, z, y, z, x, y, z)] = [1] z + [3]
> [1] z + [0]
= [e6(x, y, z)]
[e4(x, x, x, x, x, x, x, x, x, x, x)] = [1] x + [0]
>= [1] x + [0]
= [e6(x, x, x)]
[e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z)] = [1] z + [0]
? [1] z + [5]
= [e1(x1, x1, x, y, z)]
[e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z)] = [1] z + [0]
>= [1] z + [0]
= [e5(x1, x, y, z)]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
e1(x1, x1, x, y, z) }
Weak Trs:
{ f1() -> g1()
, f1() -> g2()
, f2() -> g1()
, f2() -> g2()
, h1() -> i()
, h2() -> i()
, e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e2(x, x, y, z, z) -> e6(x, y, z)
, e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z)
, e2(i(), x, y, z, i()) -> e6(x, y, z)
, e5(i(), x, y, z) -> e6(x, y, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
, e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
, e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
e5(x1, x, y, z) }
Obligation:
runtime complexity
Answer:
MAYBE
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
none
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[f1] = [7]
[g1] = [6]
[g2] = [0]
[f2] = [7]
[h1] = [4]
[h2] = [4]
[i] = [0]
[e1](x1, x2, x3, x4, x5) = [1] x5 + [5]
[e2](x1, x2, x3, x4, x5) = [1] x4 + [0]
[e5](x1, x2, x3, x4) = [1] x4 + [0]
[e3](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1] x11 + [0]
[e6](x1, x2, x3) = [1] x3 + [0]
[e4](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1] x11 + [0]
The following symbols are considered usable
{f1, g1, g2, f2, h1, h2, e1, e2, e5, e3, e4}
The order satisfies the following ordering constraints:
[f1()] = [7]
> [6]
= [g1()]
[f1()] = [7]
> [0]
= [g2()]
[g1()] = [6]
> [4]
= [h1()]
[g1()] = [6]
> [4]
= [h2()]
[g2()] = [0]
? [4]
= [h1()]
[g2()] = [0]
? [4]
= [h2()]
[f2()] = [7]
> [6]
= [g1()]
[f2()] = [7]
> [0]
= [g2()]
[h1()] = [4]
> [0]
= [i()]
[h2()] = [4]
> [0]
= [i()]
[e1(x1, x1, x, y, z)] = [1] z + [5]
> [1] z + [0]
= [e5(x1, x, y, z)]
[e1(h1(), h2(), x, y, z)] = [1] z + [5]
> [1] z + [0]
= [e2(x, x, y, z, z)]
[e2(x, x, y, z, z)] = [1] z + [0]
>= [1] z + [0]
= [e6(x, y, z)]
[e2(f1(), x, y, z, f2())] = [1] z + [0]
>= [1] z + [0]
= [e3(x, y, x, y, y, z, y, z, x, y, z)]
[e2(i(), x, y, z, i())] = [1] z + [0]
>= [1] z + [0]
= [e6(x, y, z)]
[e5(i(), x, y, z)] = [1] z + [0]
>= [1] z + [0]
= [e6(x, y, z)]
[e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)] = [1] z + [0]
>= [1] z + [0]
= [e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)]
[e3(x, y, x, y, y, z, y, z, x, y, z)] = [1] z + [0]
>= [1] z + [0]
= [e6(x, y, z)]
[e4(x, x, x, x, x, x, x, x, x, x, x)] = [1] x + [0]
>= [1] x + [0]
= [e6(x, x, x)]
[e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z)] = [1] z + [0]
? [1] z + [5]
= [e1(x1, x1, x, y, z)]
[e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z)] = [1] z + [0]
>= [1] z + [0]
= [e5(x1, x, y, z)]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ g2() -> h1()
, g2() -> h2()
, e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
e1(x1, x1, x, y, z) }
Weak Trs:
{ f1() -> g1()
, f1() -> g2()
, g1() -> h1()
, g1() -> h2()
, f2() -> g1()
, f2() -> g2()
, h1() -> i()
, h2() -> i()
, e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e2(x, x, y, z, z) -> e6(x, y, z)
, e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z)
, e2(i(), x, y, z, i()) -> e6(x, y, z)
, e5(i(), x, y, z) -> e6(x, y, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
, e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
, e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
e5(x1, x, y, z) }
Obligation:
runtime complexity
Answer:
MAYBE
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
none
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[f1] = [7]
[g1] = [7]
[g2] = [7]
[f2] = [7]
[h1] = [6]
[h2] = [5]
[i] = [5]
[e1](x1, x2, x3, x4, x5) = [1] x3 + [1] x4 + [1] x5 + [7]
[e2](x1, x2, x3, x4, x5) = [1] x2 + [1] x3 + [1] x4 + [7]
[e5](x1, x2, x3, x4) = [1] x2 + [1] x3 + [1] x4 + [7]
[e3](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1] x9 + [1] x10 + [1] x11 + [7]
[e6](x1, x2, x3) = [1] x1 + [1] x3 + [7]
[e4](x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = [1] x9 + [1] x10 + [1] x11 + [7]
The following symbols are considered usable
{f1, g1, g2, f2, h1, h2, e1, e2, e5, e3, e4}
The order satisfies the following ordering constraints:
[f1()] = [7]
>= [7]
= [g1()]
[f1()] = [7]
>= [7]
= [g2()]
[g1()] = [7]
> [6]
= [h1()]
[g1()] = [7]
> [5]
= [h2()]
[g2()] = [7]
> [6]
= [h1()]
[g2()] = [7]
> [5]
= [h2()]
[f2()] = [7]
>= [7]
= [g1()]
[f2()] = [7]
>= [7]
= [g2()]
[h1()] = [6]
> [5]
= [i()]
[h2()] = [5]
>= [5]
= [i()]
[e1(x1, x1, x, y, z)] = [1] x + [1] y + [1] z + [7]
>= [1] x + [1] y + [1] z + [7]
= [e5(x1, x, y, z)]
[e1(h1(), h2(), x, y, z)] = [1] x + [1] y + [1] z + [7]
>= [1] x + [1] y + [1] z + [7]
= [e2(x, x, y, z, z)]
[e2(x, x, y, z, z)] = [1] x + [1] y + [1] z + [7]
>= [1] x + [1] z + [7]
= [e6(x, y, z)]
[e2(f1(), x, y, z, f2())] = [1] x + [1] y + [1] z + [7]
>= [1] x + [1] y + [1] z + [7]
= [e3(x, y, x, y, y, z, y, z, x, y, z)]
[e2(i(), x, y, z, i())] = [1] x + [1] y + [1] z + [7]
>= [1] x + [1] z + [7]
= [e6(x, y, z)]
[e5(i(), x, y, z)] = [1] x + [1] y + [1] z + [7]
>= [1] x + [1] z + [7]
= [e6(x, y, z)]
[e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)] = [1] x + [1] y + [1] z + [7]
>= [1] x + [1] y + [1] z + [7]
= [e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)]
[e3(x, y, x, y, y, z, y, z, x, y, z)] = [1] x + [1] y + [1] z + [7]
>= [1] x + [1] z + [7]
= [e6(x, y, z)]
[e4(x, x, x, x, x, x, x, x, x, x, x)] = [3] x + [7]
>= [2] x + [7]
= [e6(x, x, x)]
[e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z)] = [1] x + [1] y + [1] z + [7]
>= [1] x + [1] y + [1] z + [7]
= [e1(x1, x1, x, y, z)]
[e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z)] = [1] x + [1] y + [1] z + [7]
>= [1] x + [1] y + [1] z + [7]
= [e5(x1, x, y, z)]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
e1(x1, x1, x, y, z) }
Weak Trs:
{ f1() -> g1()
, f1() -> g2()
, g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, f2() -> g1()
, f2() -> g2()
, h1() -> i()
, h2() -> i()
, e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e2(x, x, y, z, z) -> e6(x, y, z)
, e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z)
, e2(i(), x, y, z, i()) -> e6(x, y, z)
, e5(i(), x, y, z) -> e6(x, y, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
, e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
, e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
e5(x1, x, y, z) }
Obligation:
runtime complexity
Answer:
MAYBE
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'WithProblem' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'WithProblem' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'WithProblem' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'WithProblem' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'WithProblem' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'WithProblem' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
following reason:
The processor is inapplicable, reason:
Processor only applicable for innermost runtime complexity analysis
2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
to the following reason:
The processor is inapplicable, reason:
Processor only applicable for innermost runtime complexity analysis
3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Bounds with perSymbol-enrichment and initial automaton 'match''
failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'Bounds with minimal-enrichment and initial automaton 'match''
failed due to the following reason:
match-boundness of the problem could not be verified.
3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
due to the following reason:
We add the following weak dependency pairs:
Strict DPs:
{ f1^#() -> c_1(g1^#())
, f1^#() -> c_2(g2^#())
, g1^#() -> c_3(h1^#())
, g1^#() -> c_4(h2^#())
, g2^#() -> c_5(h1^#())
, g2^#() -> c_6(h2^#())
, h1^#() -> c_9()
, h2^#() -> c_10()
, f2^#() -> c_7(g1^#())
, f2^#() -> c_8(g2^#())
, e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, e1^#(h1(), h2(), x, y, z) -> c_12(e2^#(x, x, y, z, z))
, e5^#(i(), x, y, z) -> c_16(x, y, z)
, e2^#(x, x, y, z, z) -> c_13(x, y, z)
, e2^#(f1(), x, y, z, f2()) ->
c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z))
, e2^#(i(), x, y, z, i()) -> c_15(x, y, z)
, e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_18(x, y, z)
, e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_19(x, x, x)
, e4^#(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
c_20(e1^#(x1, x1, x, y, z))
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_21(e5^#(x1, x, y, z)) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ f1^#() -> c_1(g1^#())
, f1^#() -> c_2(g2^#())
, g1^#() -> c_3(h1^#())
, g1^#() -> c_4(h2^#())
, g2^#() -> c_5(h1^#())
, g2^#() -> c_6(h2^#())
, h1^#() -> c_9()
, h2^#() -> c_10()
, f2^#() -> c_7(g1^#())
, f2^#() -> c_8(g2^#())
, e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, e1^#(h1(), h2(), x, y, z) -> c_12(e2^#(x, x, y, z, z))
, e5^#(i(), x, y, z) -> c_16(x, y, z)
, e2^#(x, x, y, z, z) -> c_13(x, y, z)
, e2^#(f1(), x, y, z, f2()) ->
c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z))
, e2^#(i(), x, y, z, i()) -> c_15(x, y, z)
, e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_18(x, y, z)
, e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_19(x, x, x)
, e4^#(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
c_20(e1^#(x1, x1, x, y, z))
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_21(e5^#(x1, x, y, z)) }
Strict Trs:
{ f1() -> g1()
, f1() -> g2()
, g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, f2() -> g1()
, f2() -> g2()
, h1() -> i()
, h2() -> i()
, e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e2(x, x, y, z, z) -> e6(x, y, z)
, e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z)
, e2(i(), x, y, z, i()) -> e6(x, y, z)
, e5(i(), x, y, z) -> e6(x, y, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
, e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
, e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
e1(x1, x1, x, y, z)
, e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
e5(x1, x, y, z) }
Obligation:
runtime complexity
Answer:
MAYBE
We estimate the number of application of {7,8} by applications of
Pre({7,8}) = {3,4,5,6,13,14,16,18,19}. Here rules are labeled as
follows:
DPs:
{ 1: f1^#() -> c_1(g1^#())
, 2: f1^#() -> c_2(g2^#())
, 3: g1^#() -> c_3(h1^#())
, 4: g1^#() -> c_4(h2^#())
, 5: g2^#() -> c_5(h1^#())
, 6: g2^#() -> c_6(h2^#())
, 7: h1^#() -> c_9()
, 8: h2^#() -> c_10()
, 9: f2^#() -> c_7(g1^#())
, 10: f2^#() -> c_8(g2^#())
, 11: e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, 12: e1^#(h1(), h2(), x, y, z) -> c_12(e2^#(x, x, y, z, z))
, 13: e5^#(i(), x, y, z) -> c_16(x, y, z)
, 14: e2^#(x, x, y, z, z) -> c_13(x, y, z)
, 15: e2^#(f1(), x, y, z, f2()) ->
c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z))
, 16: e2^#(i(), x, y, z, i()) -> c_15(x, y, z)
, 17: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, 18: e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_18(x, y, z)
, 19: e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_19(x, x, x)
, 20: e4^#(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
c_20(e1^#(x1, x1, x, y, z))
, 21: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_21(e5^#(x1, x, y, z)) }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ f1^#() -> c_1(g1^#())
, f1^#() -> c_2(g2^#())
, g1^#() -> c_3(h1^#())
, g1^#() -> c_4(h2^#())
, g2^#() -> c_5(h1^#())
, g2^#() -> c_6(h2^#())
, f2^#() -> c_7(g1^#())
, f2^#() -> c_8(g2^#())
, e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, e1^#(h1(), h2(), x, y, z) -> c_12(e2^#(x, x, y, z, z))
, e5^#(i(), x, y, z) -> c_16(x, y, z)
, e2^#(x, x, y, z, z) -> c_13(x, y, z)
, e2^#(f1(), x, y, z, f2()) ->
c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z))
, e2^#(i(), x, y, z, i()) -> c_15(x, y, z)
, e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_18(x, y, z)
, e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_19(x, x, x)
, e4^#(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
c_20(e1^#(x1, x1, x, y, z))
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_21(e5^#(x1, x, y, z)) }
Strict Trs:
{ f1() -> g1()
, f1() -> g2()
, g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, f2() -> g1()
, f2() -> g2()
, h1() -> i()
, h2() -> i()
, e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e2(x, x, y, z, z) -> e6(x, y, z)
, e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z)
, e2(i(), x, y, z, i()) -> e6(x, y, z)
, e5(i(), x, y, z) -> e6(x, y, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
, e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
, e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
e1(x1, x1, x, y, z)
, e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
e5(x1, x, y, z) }
Weak DPs:
{ h1^#() -> c_9()
, h2^#() -> c_10() }
Obligation:
runtime complexity
Answer:
MAYBE
We estimate the number of application of {3,4,5,6} by applications
of Pre({3,4,5,6}) = {1,2,7,8,11,12,14,16,17}. Here rules are
labeled as follows:
DPs:
{ 1: f1^#() -> c_1(g1^#())
, 2: f1^#() -> c_2(g2^#())
, 3: g1^#() -> c_3(h1^#())
, 4: g1^#() -> c_4(h2^#())
, 5: g2^#() -> c_5(h1^#())
, 6: g2^#() -> c_6(h2^#())
, 7: f2^#() -> c_7(g1^#())
, 8: f2^#() -> c_8(g2^#())
, 9: e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, 10: e1^#(h1(), h2(), x, y, z) -> c_12(e2^#(x, x, y, z, z))
, 11: e5^#(i(), x, y, z) -> c_16(x, y, z)
, 12: e2^#(x, x, y, z, z) -> c_13(x, y, z)
, 13: e2^#(f1(), x, y, z, f2()) ->
c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z))
, 14: e2^#(i(), x, y, z, i()) -> c_15(x, y, z)
, 15: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, 16: e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_18(x, y, z)
, 17: e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_19(x, x, x)
, 18: e4^#(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
c_20(e1^#(x1, x1, x, y, z))
, 19: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_21(e5^#(x1, x, y, z))
, 20: h1^#() -> c_9()
, 21: h2^#() -> c_10() }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ f1^#() -> c_1(g1^#())
, f1^#() -> c_2(g2^#())
, f2^#() -> c_7(g1^#())
, f2^#() -> c_8(g2^#())
, e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, e1^#(h1(), h2(), x, y, z) -> c_12(e2^#(x, x, y, z, z))
, e5^#(i(), x, y, z) -> c_16(x, y, z)
, e2^#(x, x, y, z, z) -> c_13(x, y, z)
, e2^#(f1(), x, y, z, f2()) ->
c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z))
, e2^#(i(), x, y, z, i()) -> c_15(x, y, z)
, e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_18(x, y, z)
, e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_19(x, x, x)
, e4^#(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
c_20(e1^#(x1, x1, x, y, z))
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_21(e5^#(x1, x, y, z)) }
Strict Trs:
{ f1() -> g1()
, f1() -> g2()
, g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, f2() -> g1()
, f2() -> g2()
, h1() -> i()
, h2() -> i()
, e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e2(x, x, y, z, z) -> e6(x, y, z)
, e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z)
, e2(i(), x, y, z, i()) -> e6(x, y, z)
, e5(i(), x, y, z) -> e6(x, y, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
, e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
, e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
e1(x1, x1, x, y, z)
, e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
e5(x1, x, y, z) }
Weak DPs:
{ g1^#() -> c_3(h1^#())
, g1^#() -> c_4(h2^#())
, g2^#() -> c_5(h1^#())
, g2^#() -> c_6(h2^#())
, h1^#() -> c_9()
, h2^#() -> c_10() }
Obligation:
runtime complexity
Answer:
MAYBE
We estimate the number of application of {1,2,3,4} by applications
of Pre({1,2,3,4}) = {7,8,10,12,13}. Here rules are labeled as
follows:
DPs:
{ 1: f1^#() -> c_1(g1^#())
, 2: f1^#() -> c_2(g2^#())
, 3: f2^#() -> c_7(g1^#())
, 4: f2^#() -> c_8(g2^#())
, 5: e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, 6: e1^#(h1(), h2(), x, y, z) -> c_12(e2^#(x, x, y, z, z))
, 7: e5^#(i(), x, y, z) -> c_16(x, y, z)
, 8: e2^#(x, x, y, z, z) -> c_13(x, y, z)
, 9: e2^#(f1(), x, y, z, f2()) ->
c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z))
, 10: e2^#(i(), x, y, z, i()) -> c_15(x, y, z)
, 11: e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, 12: e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_18(x, y, z)
, 13: e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_19(x, x, x)
, 14: e4^#(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
c_20(e1^#(x1, x1, x, y, z))
, 15: e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_21(e5^#(x1, x, y, z))
, 16: g1^#() -> c_3(h1^#())
, 17: g1^#() -> c_4(h2^#())
, 18: g2^#() -> c_5(h1^#())
, 19: g2^#() -> c_6(h2^#())
, 20: h1^#() -> c_9()
, 21: h2^#() -> c_10() }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ e1^#(x1, x1, x, y, z) -> c_11(e5^#(x1, x, y, z))
, e1^#(h1(), h2(), x, y, z) -> c_12(e2^#(x, x, y, z, z))
, e5^#(i(), x, y, z) -> c_16(x, y, z)
, e2^#(x, x, y, z, z) -> c_13(x, y, z)
, e2^#(f1(), x, y, z, f2()) ->
c_14(e3^#(x, y, x, y, y, z, y, z, x, y, z))
, e2^#(i(), x, y, z, i()) -> c_15(x, y, z)
, e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
c_17(e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z))
, e3^#(x, y, x, y, y, z, y, z, x, y, z) -> c_18(x, y, z)
, e4^#(x, x, x, x, x, x, x, x, x, x, x) -> c_19(x, x, x)
, e4^#(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
c_20(e1^#(x1, x1, x, y, z))
, e4^#(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
c_21(e5^#(x1, x, y, z)) }
Strict Trs:
{ f1() -> g1()
, f1() -> g2()
, g1() -> h1()
, g1() -> h2()
, g2() -> h1()
, g2() -> h2()
, f2() -> g1()
, f2() -> g2()
, h1() -> i()
, h2() -> i()
, e1(x1, x1, x, y, z) -> e5(x1, x, y, z)
, e1(h1(), h2(), x, y, z) -> e2(x, x, y, z, z)
, e2(x, x, y, z, z) -> e6(x, y, z)
, e2(f1(), x, y, z, f2()) -> e3(x, y, x, y, y, z, y, z, x, y, z)
, e2(i(), x, y, z, i()) -> e6(x, y, z)
, e5(i(), x, y, z) -> e6(x, y, z)
, e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) ->
e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
, e3(x, y, x, y, y, z, y, z, x, y, z) -> e6(x, y, z)
, e4(x, x, x, x, x, x, x, x, x, x, x) -> e6(x, x, x)
, e4(g1(), x1, g2(), x1, g1(), x1, g2(), x1, x, y, z) ->
e1(x1, x1, x, y, z)
, e4(i(), x1, i(), x1, i(), x1, i(), x1, x, y, z) ->
e5(x1, x, y, z) }
Weak DPs:
{ f1^#() -> c_1(g1^#())
, f1^#() -> c_2(g2^#())
, g1^#() -> c_3(h1^#())
, g1^#() -> c_4(h2^#())
, g2^#() -> c_5(h1^#())
, g2^#() -> c_6(h2^#())
, h1^#() -> c_9()
, h2^#() -> c_10()
, f2^#() -> c_7(g1^#())
, f2^#() -> c_8(g2^#()) }
Obligation:
runtime complexity
Answer:
MAYBE
Empty strict component of the problem is NOT empty.
Arrrr..