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..