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