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