MAYBE 402.99/297.19 MAYBE 402.99/297.19 402.99/297.19 We are left with following problem, upon which TcT provides the 402.99/297.19 certificate MAYBE. 402.99/297.19 402.99/297.19 Strict Trs: 402.99/297.19 { a__h(X) -> a__g(mark(X), X) 402.99/297.19 , a__h(X) -> h(X) 402.99/297.19 , a__g(X1, X2) -> g(X1, X2) 402.99/297.19 , a__g(a(), X) -> a__f(b(), X) 402.99/297.19 , mark(a()) -> a__a() 402.99/297.19 , mark(b()) -> b() 402.99/297.19 , mark(h(X)) -> a__h(mark(X)) 402.99/297.19 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 402.99/297.19 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 402.99/297.19 , a__f(X, X) -> a__h(a__a()) 402.99/297.19 , a__f(X1, X2) -> f(X1, X2) 402.99/297.19 , a__a() -> a() 402.99/297.19 , a__a() -> b() } 402.99/297.19 Obligation: 402.99/297.19 innermost runtime complexity 402.99/297.19 Answer: 402.99/297.19 MAYBE 402.99/297.19 402.99/297.19 None of the processors succeeded. 402.99/297.19 402.99/297.19 Details of failed attempt(s): 402.99/297.19 ----------------------------- 402.99/297.19 1) 'empty' failed due to the following reason: 402.99/297.19 402.99/297.19 Empty strict component of the problem is NOT empty. 402.99/297.19 402.99/297.19 2) 'Best' failed due to the following reason: 402.99/297.19 402.99/297.19 None of the processors succeeded. 402.99/297.19 402.99/297.19 Details of failed attempt(s): 402.99/297.19 ----------------------------- 402.99/297.19 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 402.99/297.19 following reason: 402.99/297.19 402.99/297.19 Computation stopped due to timeout after 297.0 seconds. 402.99/297.19 402.99/297.19 2) 'Best' failed due to the following reason: 402.99/297.19 402.99/297.19 None of the processors succeeded. 402.99/297.19 402.99/297.19 Details of failed attempt(s): 402.99/297.19 ----------------------------- 402.99/297.19 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 402.99/297.19 seconds)' failed due to the following reason: 402.99/297.19 402.99/297.19 The weightgap principle applies (using the following nonconstant 402.99/297.19 growth matrix-interpretation) 402.99/297.19 402.99/297.19 The following argument positions are usable: 402.99/297.19 Uargs(a__h) = {1}, Uargs(a__g) = {1}, Uargs(a__f) = {1} 402.99/297.19 402.99/297.19 TcT has computed the following matrix interpretation satisfying 402.99/297.19 not(EDA) and not(IDA(1)). 402.99/297.19 402.99/297.19 [a__h](x1) = [1] x1 + [4] 402.99/297.19 402.99/297.19 [a__g](x1, x2) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [mark](x1) = [0] 402.99/297.19 402.99/297.19 [a] = [0] 402.99/297.19 402.99/297.19 [a__f](x1, x2) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [b] = [0] 402.99/297.19 402.99/297.19 [a__a] = [0] 402.99/297.19 402.99/297.19 [h](x1) = [1] x1 + [7] 402.99/297.19 402.99/297.19 [g](x1, x2) = [1] x1 + [7] 402.99/297.19 402.99/297.19 [f](x1, x2) = [1] x1 + [7] 402.99/297.19 402.99/297.19 The order satisfies the following ordering constraints: 402.99/297.19 402.99/297.19 [a__h(X)] = [1] X + [4] 402.99/297.19 > [0] 402.99/297.19 = [a__g(mark(X), X)] 402.99/297.19 402.99/297.19 [a__h(X)] = [1] X + [4] 402.99/297.19 ? [1] X + [7] 402.99/297.19 = [h(X)] 402.99/297.19 402.99/297.19 [a__g(X1, X2)] = [1] X1 + [0] 402.99/297.19 ? [1] X1 + [7] 402.99/297.19 = [g(X1, X2)] 402.99/297.19 402.99/297.19 [a__g(a(), X)] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__f(b(), X)] 402.99/297.19 402.99/297.19 [mark(a())] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__a()] 402.99/297.19 402.99/297.19 [mark(b())] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [b()] 402.99/297.19 402.99/297.19 [mark(h(X))] = [0] 402.99/297.19 ? [4] 402.99/297.19 = [a__h(mark(X))] 402.99/297.19 402.99/297.19 [mark(g(X1, X2))] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__g(mark(X1), X2)] 402.99/297.19 402.99/297.19 [mark(f(X1, X2))] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__f(mark(X1), X2)] 402.99/297.19 402.99/297.19 [a__f(X, X)] = [1] X + [0] 402.99/297.19 ? [4] 402.99/297.19 = [a__h(a__a())] 402.99/297.19 402.99/297.19 [a__f(X1, X2)] = [1] X1 + [0] 402.99/297.19 ? [1] X1 + [7] 402.99/297.19 = [f(X1, X2)] 402.99/297.19 402.99/297.19 [a__a()] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a()] 402.99/297.19 402.99/297.19 [a__a()] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [b()] 402.99/297.19 402.99/297.19 402.99/297.19 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 402.99/297.19 402.99/297.19 We are left with following problem, upon which TcT provides the 402.99/297.19 certificate MAYBE. 402.99/297.19 402.99/297.19 Strict Trs: 402.99/297.19 { a__h(X) -> h(X) 402.99/297.19 , a__g(X1, X2) -> g(X1, X2) 402.99/297.19 , a__g(a(), X) -> a__f(b(), X) 402.99/297.19 , mark(a()) -> a__a() 402.99/297.19 , mark(b()) -> b() 402.99/297.19 , mark(h(X)) -> a__h(mark(X)) 402.99/297.19 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 402.99/297.19 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 402.99/297.19 , a__f(X, X) -> a__h(a__a()) 402.99/297.19 , a__f(X1, X2) -> f(X1, X2) 402.99/297.19 , a__a() -> a() 402.99/297.19 , a__a() -> b() } 402.99/297.19 Weak Trs: { a__h(X) -> a__g(mark(X), X) } 402.99/297.19 Obligation: 402.99/297.19 innermost runtime complexity 402.99/297.19 Answer: 402.99/297.19 MAYBE 402.99/297.19 402.99/297.19 The weightgap principle applies (using the following nonconstant 402.99/297.19 growth matrix-interpretation) 402.99/297.19 402.99/297.19 The following argument positions are usable: 402.99/297.19 Uargs(a__h) = {1}, Uargs(a__g) = {1}, Uargs(a__f) = {1} 402.99/297.19 402.99/297.19 TcT has computed the following matrix interpretation satisfying 402.99/297.19 not(EDA) and not(IDA(1)). 402.99/297.19 402.99/297.19 [a__h](x1) = [1] x1 + [1] 402.99/297.19 402.99/297.19 [a__g](x1, x2) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [mark](x1) = [0] 402.99/297.19 402.99/297.19 [a] = [0] 402.99/297.19 402.99/297.19 [a__f](x1, x2) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [b] = [0] 402.99/297.19 402.99/297.19 [a__a] = [0] 402.99/297.19 402.99/297.19 [h](x1) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [g](x1, x2) = [1] x1 + [7] 402.99/297.19 402.99/297.19 [f](x1, x2) = [1] x1 + [7] 402.99/297.19 402.99/297.19 The order satisfies the following ordering constraints: 402.99/297.19 402.99/297.19 [a__h(X)] = [1] X + [1] 402.99/297.19 > [0] 402.99/297.19 = [a__g(mark(X), X)] 402.99/297.19 402.99/297.19 [a__h(X)] = [1] X + [1] 402.99/297.19 > [1] X + [0] 402.99/297.19 = [h(X)] 402.99/297.19 402.99/297.19 [a__g(X1, X2)] = [1] X1 + [0] 402.99/297.19 ? [1] X1 + [7] 402.99/297.19 = [g(X1, X2)] 402.99/297.19 402.99/297.19 [a__g(a(), X)] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__f(b(), X)] 402.99/297.19 402.99/297.19 [mark(a())] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__a()] 402.99/297.19 402.99/297.19 [mark(b())] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [b()] 402.99/297.19 402.99/297.19 [mark(h(X))] = [0] 402.99/297.19 ? [1] 402.99/297.19 = [a__h(mark(X))] 402.99/297.19 402.99/297.19 [mark(g(X1, X2))] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__g(mark(X1), X2)] 402.99/297.19 402.99/297.19 [mark(f(X1, X2))] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__f(mark(X1), X2)] 402.99/297.19 402.99/297.19 [a__f(X, X)] = [1] X + [0] 402.99/297.19 ? [1] 402.99/297.19 = [a__h(a__a())] 402.99/297.19 402.99/297.19 [a__f(X1, X2)] = [1] X1 + [0] 402.99/297.19 ? [1] X1 + [7] 402.99/297.19 = [f(X1, X2)] 402.99/297.19 402.99/297.19 [a__a()] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a()] 402.99/297.19 402.99/297.19 [a__a()] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [b()] 402.99/297.19 402.99/297.19 402.99/297.19 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 402.99/297.19 402.99/297.19 We are left with following problem, upon which TcT provides the 402.99/297.19 certificate MAYBE. 402.99/297.19 402.99/297.19 Strict Trs: 402.99/297.19 { a__g(X1, X2) -> g(X1, X2) 402.99/297.19 , a__g(a(), X) -> a__f(b(), X) 402.99/297.19 , mark(a()) -> a__a() 402.99/297.19 , mark(b()) -> b() 402.99/297.19 , mark(h(X)) -> a__h(mark(X)) 402.99/297.19 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 402.99/297.19 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 402.99/297.19 , a__f(X, X) -> a__h(a__a()) 402.99/297.19 , a__f(X1, X2) -> f(X1, X2) 402.99/297.19 , a__a() -> a() 402.99/297.19 , a__a() -> b() } 402.99/297.19 Weak Trs: 402.99/297.19 { a__h(X) -> a__g(mark(X), X) 402.99/297.19 , a__h(X) -> h(X) } 402.99/297.19 Obligation: 402.99/297.19 innermost runtime complexity 402.99/297.19 Answer: 402.99/297.19 MAYBE 402.99/297.19 402.99/297.19 The weightgap principle applies (using the following nonconstant 402.99/297.19 growth matrix-interpretation) 402.99/297.19 402.99/297.19 The following argument positions are usable: 402.99/297.19 Uargs(a__h) = {1}, Uargs(a__g) = {1}, Uargs(a__f) = {1} 402.99/297.19 402.99/297.19 TcT has computed the following matrix interpretation satisfying 402.99/297.19 not(EDA) and not(IDA(1)). 402.99/297.19 402.99/297.19 [a__h](x1) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [a__g](x1, x2) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [mark](x1) = [0] 402.99/297.19 402.99/297.19 [a] = [0] 402.99/297.19 402.99/297.19 [a__f](x1, x2) = [1] x1 + [4] 402.99/297.19 402.99/297.19 [b] = [0] 402.99/297.19 402.99/297.19 [a__a] = [0] 402.99/297.19 402.99/297.19 [h](x1) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [g](x1, x2) = [1] x1 + [7] 402.99/297.19 402.99/297.19 [f](x1, x2) = [1] x1 + [7] 402.99/297.19 402.99/297.19 The order satisfies the following ordering constraints: 402.99/297.19 402.99/297.19 [a__h(X)] = [1] X + [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__g(mark(X), X)] 402.99/297.19 402.99/297.19 [a__h(X)] = [1] X + [0] 402.99/297.19 >= [1] X + [0] 402.99/297.19 = [h(X)] 402.99/297.19 402.99/297.19 [a__g(X1, X2)] = [1] X1 + [0] 402.99/297.19 ? [1] X1 + [7] 402.99/297.19 = [g(X1, X2)] 402.99/297.19 402.99/297.19 [a__g(a(), X)] = [0] 402.99/297.19 ? [4] 402.99/297.19 = [a__f(b(), X)] 402.99/297.19 402.99/297.19 [mark(a())] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__a()] 402.99/297.19 402.99/297.19 [mark(b())] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [b()] 402.99/297.19 402.99/297.19 [mark(h(X))] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__h(mark(X))] 402.99/297.19 402.99/297.19 [mark(g(X1, X2))] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__g(mark(X1), X2)] 402.99/297.19 402.99/297.19 [mark(f(X1, X2))] = [0] 402.99/297.19 ? [4] 402.99/297.19 = [a__f(mark(X1), X2)] 402.99/297.19 402.99/297.19 [a__f(X, X)] = [1] X + [4] 402.99/297.19 > [0] 402.99/297.19 = [a__h(a__a())] 402.99/297.19 402.99/297.19 [a__f(X1, X2)] = [1] X1 + [4] 402.99/297.19 ? [1] X1 + [7] 402.99/297.19 = [f(X1, X2)] 402.99/297.19 402.99/297.19 [a__a()] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a()] 402.99/297.19 402.99/297.19 [a__a()] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [b()] 402.99/297.19 402.99/297.19 402.99/297.19 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 402.99/297.19 402.99/297.19 We are left with following problem, upon which TcT provides the 402.99/297.19 certificate MAYBE. 402.99/297.19 402.99/297.19 Strict Trs: 402.99/297.19 { a__g(X1, X2) -> g(X1, X2) 402.99/297.19 , a__g(a(), X) -> a__f(b(), X) 402.99/297.19 , mark(a()) -> a__a() 402.99/297.19 , mark(b()) -> b() 402.99/297.19 , mark(h(X)) -> a__h(mark(X)) 402.99/297.19 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 402.99/297.19 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 402.99/297.19 , a__f(X1, X2) -> f(X1, X2) 402.99/297.19 , a__a() -> a() 402.99/297.19 , a__a() -> b() } 402.99/297.19 Weak Trs: 402.99/297.19 { a__h(X) -> a__g(mark(X), X) 402.99/297.19 , a__h(X) -> h(X) 402.99/297.19 , a__f(X, X) -> a__h(a__a()) } 402.99/297.19 Obligation: 402.99/297.19 innermost runtime complexity 402.99/297.19 Answer: 402.99/297.19 MAYBE 402.99/297.19 402.99/297.19 The weightgap principle applies (using the following nonconstant 402.99/297.19 growth matrix-interpretation) 402.99/297.19 402.99/297.19 The following argument positions are usable: 402.99/297.19 Uargs(a__h) = {1}, Uargs(a__g) = {1}, Uargs(a__f) = {1} 402.99/297.19 402.99/297.19 TcT has computed the following matrix interpretation satisfying 402.99/297.19 not(EDA) and not(IDA(1)). 402.99/297.19 402.99/297.19 [a__h](x1) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [a__g](x1, x2) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [mark](x1) = [0] 402.99/297.19 402.99/297.19 [a] = [4] 402.99/297.19 402.99/297.19 [a__f](x1, x2) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [b] = [0] 402.99/297.19 402.99/297.19 [a__a] = [0] 402.99/297.19 402.99/297.19 [h](x1) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [g](x1, x2) = [1] x1 + [7] 402.99/297.19 402.99/297.19 [f](x1, x2) = [1] x1 + [7] 402.99/297.19 402.99/297.19 The order satisfies the following ordering constraints: 402.99/297.19 402.99/297.19 [a__h(X)] = [1] X + [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__g(mark(X), X)] 402.99/297.19 402.99/297.19 [a__h(X)] = [1] X + [0] 402.99/297.19 >= [1] X + [0] 402.99/297.19 = [h(X)] 402.99/297.19 402.99/297.19 [a__g(X1, X2)] = [1] X1 + [0] 402.99/297.19 ? [1] X1 + [7] 402.99/297.19 = [g(X1, X2)] 402.99/297.19 402.99/297.19 [a__g(a(), X)] = [4] 402.99/297.19 > [0] 402.99/297.19 = [a__f(b(), X)] 402.99/297.19 402.99/297.19 [mark(a())] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__a()] 402.99/297.19 402.99/297.19 [mark(b())] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [b()] 402.99/297.19 402.99/297.19 [mark(h(X))] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__h(mark(X))] 402.99/297.19 402.99/297.19 [mark(g(X1, X2))] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__g(mark(X1), X2)] 402.99/297.19 402.99/297.19 [mark(f(X1, X2))] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__f(mark(X1), X2)] 402.99/297.19 402.99/297.19 [a__f(X, X)] = [1] X + [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__h(a__a())] 402.99/297.19 402.99/297.19 [a__f(X1, X2)] = [1] X1 + [0] 402.99/297.19 ? [1] X1 + [7] 402.99/297.19 = [f(X1, X2)] 402.99/297.19 402.99/297.19 [a__a()] = [0] 402.99/297.19 ? [4] 402.99/297.19 = [a()] 402.99/297.19 402.99/297.19 [a__a()] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [b()] 402.99/297.19 402.99/297.19 402.99/297.19 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 402.99/297.19 402.99/297.19 We are left with following problem, upon which TcT provides the 402.99/297.19 certificate MAYBE. 402.99/297.19 402.99/297.19 Strict Trs: 402.99/297.19 { a__g(X1, X2) -> g(X1, X2) 402.99/297.19 , mark(a()) -> a__a() 402.99/297.19 , mark(b()) -> b() 402.99/297.19 , mark(h(X)) -> a__h(mark(X)) 402.99/297.19 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 402.99/297.19 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 402.99/297.19 , a__f(X1, X2) -> f(X1, X2) 402.99/297.19 , a__a() -> a() 402.99/297.19 , a__a() -> b() } 402.99/297.19 Weak Trs: 402.99/297.19 { a__h(X) -> a__g(mark(X), X) 402.99/297.19 , a__h(X) -> h(X) 402.99/297.19 , a__g(a(), X) -> a__f(b(), X) 402.99/297.19 , a__f(X, X) -> a__h(a__a()) } 402.99/297.19 Obligation: 402.99/297.19 innermost runtime complexity 402.99/297.19 Answer: 402.99/297.19 MAYBE 402.99/297.19 402.99/297.19 The weightgap principle applies (using the following nonconstant 402.99/297.19 growth matrix-interpretation) 402.99/297.19 402.99/297.19 The following argument positions are usable: 402.99/297.19 Uargs(a__h) = {1}, Uargs(a__g) = {1}, Uargs(a__f) = {1} 402.99/297.19 402.99/297.19 TcT has computed the following matrix interpretation satisfying 402.99/297.19 not(EDA) and not(IDA(1)). 402.99/297.19 402.99/297.19 [a__h](x1) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [a__g](x1, x2) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [mark](x1) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [a] = [4] 402.99/297.19 402.99/297.19 [a__f](x1, x2) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [b] = [0] 402.99/297.19 402.99/297.19 [a__a] = [0] 402.99/297.19 402.99/297.19 [h](x1) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [g](x1, x2) = [1] x1 + [0] 402.99/297.19 402.99/297.19 [f](x1, x2) = [1] x1 + [0] 402.99/297.19 402.99/297.19 The order satisfies the following ordering constraints: 402.99/297.19 402.99/297.19 [a__h(X)] = [1] X + [0] 402.99/297.19 >= [1] X + [0] 402.99/297.19 = [a__g(mark(X), X)] 402.99/297.19 402.99/297.19 [a__h(X)] = [1] X + [0] 402.99/297.19 >= [1] X + [0] 402.99/297.19 = [h(X)] 402.99/297.19 402.99/297.19 [a__g(X1, X2)] = [1] X1 + [0] 402.99/297.19 >= [1] X1 + [0] 402.99/297.19 = [g(X1, X2)] 402.99/297.19 402.99/297.19 [a__g(a(), X)] = [4] 402.99/297.19 > [0] 402.99/297.19 = [a__f(b(), X)] 402.99/297.19 402.99/297.19 [mark(a())] = [4] 402.99/297.19 > [0] 402.99/297.19 = [a__a()] 402.99/297.19 402.99/297.19 [mark(b())] = [0] 402.99/297.19 >= [0] 402.99/297.19 = [b()] 402.99/297.19 402.99/297.19 [mark(h(X))] = [1] X + [0] 402.99/297.19 >= [1] X + [0] 402.99/297.19 = [a__h(mark(X))] 402.99/297.19 402.99/297.19 [mark(g(X1, X2))] = [1] X1 + [0] 402.99/297.19 >= [1] X1 + [0] 402.99/297.19 = [a__g(mark(X1), X2)] 402.99/297.19 402.99/297.19 [mark(f(X1, X2))] = [1] X1 + [0] 402.99/297.19 >= [1] X1 + [0] 402.99/297.19 = [a__f(mark(X1), X2)] 402.99/297.19 402.99/297.19 [a__f(X, X)] = [1] X + [0] 402.99/297.19 >= [0] 402.99/297.19 = [a__h(a__a())] 402.99/297.19 402.99/297.19 [a__f(X1, X2)] = [1] X1 + [0] 402.99/297.19 >= [1] X1 + [0] 403.37/297.20 = [f(X1, X2)] 403.37/297.20 403.37/297.20 [a__a()] = [0] 403.37/297.20 ? [4] 403.37/297.20 = [a()] 403.37/297.20 403.37/297.20 [a__a()] = [0] 403.37/297.20 >= [0] 403.37/297.20 = [b()] 403.37/297.20 403.37/297.20 403.37/297.20 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 403.37/297.20 403.37/297.20 We are left with following problem, upon which TcT provides the 403.37/297.20 certificate MAYBE. 403.37/297.20 403.37/297.20 Strict Trs: 403.37/297.20 { a__g(X1, X2) -> g(X1, X2) 403.37/297.20 , mark(b()) -> b() 403.37/297.20 , mark(h(X)) -> a__h(mark(X)) 403.37/297.20 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 403.37/297.20 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 403.37/297.20 , a__f(X1, X2) -> f(X1, X2) 403.37/297.20 , a__a() -> a() 403.37/297.20 , a__a() -> b() } 403.37/297.20 Weak Trs: 403.37/297.20 { a__h(X) -> a__g(mark(X), X) 403.37/297.20 , a__h(X) -> h(X) 403.37/297.20 , a__g(a(), X) -> a__f(b(), X) 403.37/297.20 , mark(a()) -> a__a() 403.37/297.20 , a__f(X, X) -> a__h(a__a()) } 403.37/297.20 Obligation: 403.37/297.20 innermost runtime complexity 403.37/297.20 Answer: 403.37/297.20 MAYBE 403.37/297.20 403.37/297.20 The weightgap principle applies (using the following nonconstant 403.37/297.20 growth matrix-interpretation) 403.37/297.20 403.37/297.20 The following argument positions are usable: 403.37/297.20 Uargs(a__h) = {1}, Uargs(a__g) = {1}, Uargs(a__f) = {1} 403.37/297.20 403.37/297.20 TcT has computed the following matrix interpretation satisfying 403.37/297.20 not(EDA) and not(IDA(1)). 403.37/297.20 403.37/297.20 [a__h](x1) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [a__g](x1, x2) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [mark](x1) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [a] = [0] 403.37/297.20 403.37/297.20 [a__f](x1, x2) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [b] = [0] 403.37/297.20 403.37/297.20 [a__a] = [0] 403.37/297.20 403.37/297.20 [h](x1) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [g](x1, x2) = [1] x1 + [4] 403.37/297.20 403.37/297.20 [f](x1, x2) = [1] x1 + [0] 403.37/297.20 403.37/297.20 The order satisfies the following ordering constraints: 403.37/297.20 403.37/297.20 [a__h(X)] = [1] X + [0] 403.37/297.20 >= [1] X + [0] 403.37/297.20 = [a__g(mark(X), X)] 403.37/297.20 403.37/297.20 [a__h(X)] = [1] X + [0] 403.37/297.20 >= [1] X + [0] 403.37/297.20 = [h(X)] 403.37/297.20 403.37/297.20 [a__g(X1, X2)] = [1] X1 + [0] 403.37/297.20 ? [1] X1 + [4] 403.37/297.20 = [g(X1, X2)] 403.37/297.20 403.37/297.20 [a__g(a(), X)] = [0] 403.37/297.20 >= [0] 403.37/297.20 = [a__f(b(), X)] 403.37/297.20 403.37/297.20 [mark(a())] = [0] 403.37/297.20 >= [0] 403.37/297.20 = [a__a()] 403.37/297.20 403.37/297.20 [mark(b())] = [0] 403.37/297.20 >= [0] 403.37/297.20 = [b()] 403.37/297.20 403.37/297.20 [mark(h(X))] = [1] X + [0] 403.37/297.20 >= [1] X + [0] 403.37/297.20 = [a__h(mark(X))] 403.37/297.20 403.37/297.20 [mark(g(X1, X2))] = [1] X1 + [4] 403.37/297.20 > [1] X1 + [0] 403.37/297.20 = [a__g(mark(X1), X2)] 403.37/297.20 403.37/297.20 [mark(f(X1, X2))] = [1] X1 + [0] 403.37/297.20 >= [1] X1 + [0] 403.37/297.20 = [a__f(mark(X1), X2)] 403.37/297.20 403.37/297.20 [a__f(X, X)] = [1] X + [0] 403.37/297.20 >= [0] 403.37/297.20 = [a__h(a__a())] 403.37/297.20 403.37/297.20 [a__f(X1, X2)] = [1] X1 + [0] 403.37/297.20 >= [1] X1 + [0] 403.37/297.20 = [f(X1, X2)] 403.37/297.20 403.37/297.20 [a__a()] = [0] 403.37/297.20 >= [0] 403.37/297.20 = [a()] 403.37/297.20 403.37/297.20 [a__a()] = [0] 403.37/297.20 >= [0] 403.37/297.20 = [b()] 403.37/297.20 403.37/297.20 403.37/297.20 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 403.37/297.20 403.37/297.20 We are left with following problem, upon which TcT provides the 403.37/297.20 certificate MAYBE. 403.37/297.20 403.37/297.20 Strict Trs: 403.37/297.20 { a__g(X1, X2) -> g(X1, X2) 403.37/297.20 , mark(b()) -> b() 403.37/297.20 , mark(h(X)) -> a__h(mark(X)) 403.37/297.20 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 403.37/297.20 , a__f(X1, X2) -> f(X1, X2) 403.37/297.20 , a__a() -> a() 403.37/297.20 , a__a() -> b() } 403.37/297.20 Weak Trs: 403.37/297.20 { a__h(X) -> a__g(mark(X), X) 403.37/297.20 , a__h(X) -> h(X) 403.37/297.20 , a__g(a(), X) -> a__f(b(), X) 403.37/297.20 , mark(a()) -> a__a() 403.37/297.20 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 403.37/297.20 , a__f(X, X) -> a__h(a__a()) } 403.37/297.20 Obligation: 403.37/297.20 innermost runtime complexity 403.37/297.20 Answer: 403.37/297.20 MAYBE 403.37/297.20 403.37/297.20 The weightgap principle applies (using the following nonconstant 403.37/297.20 growth matrix-interpretation) 403.37/297.20 403.37/297.20 The following argument positions are usable: 403.37/297.20 Uargs(a__h) = {1}, Uargs(a__g) = {1}, Uargs(a__f) = {1} 403.37/297.20 403.37/297.20 TcT has computed the following matrix interpretation satisfying 403.37/297.20 not(EDA) and not(IDA(1)). 403.37/297.20 403.37/297.20 [a__h](x1) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [a__g](x1, x2) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [mark](x1) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [a] = [0] 403.37/297.20 403.37/297.20 [a__f](x1, x2) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [b] = [0] 403.37/297.20 403.37/297.20 [a__a] = [0] 403.37/297.20 403.37/297.20 [h](x1) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [g](x1, x2) = [1] x1 + [4] 403.37/297.20 403.37/297.20 [f](x1, x2) = [1] x1 + [1] 403.37/297.20 403.37/297.20 The order satisfies the following ordering constraints: 403.37/297.20 403.37/297.20 [a__h(X)] = [1] X + [0] 403.37/297.20 >= [1] X + [0] 403.37/297.20 = [a__g(mark(X), X)] 403.37/297.20 403.37/297.20 [a__h(X)] = [1] X + [0] 403.37/297.20 >= [1] X + [0] 403.37/297.20 = [h(X)] 403.37/297.20 403.37/297.20 [a__g(X1, X2)] = [1] X1 + [0] 403.37/297.20 ? [1] X1 + [4] 403.37/297.20 = [g(X1, X2)] 403.37/297.20 403.37/297.20 [a__g(a(), X)] = [0] 403.37/297.20 >= [0] 403.37/297.20 = [a__f(b(), X)] 403.37/297.20 403.37/297.20 [mark(a())] = [0] 403.37/297.20 >= [0] 403.37/297.20 = [a__a()] 403.37/297.20 403.37/297.20 [mark(b())] = [0] 403.37/297.20 >= [0] 403.37/297.20 = [b()] 403.37/297.20 403.37/297.20 [mark(h(X))] = [1] X + [0] 403.37/297.20 >= [1] X + [0] 403.37/297.20 = [a__h(mark(X))] 403.37/297.20 403.37/297.20 [mark(g(X1, X2))] = [1] X1 + [4] 403.37/297.20 > [1] X1 + [0] 403.37/297.20 = [a__g(mark(X1), X2)] 403.37/297.20 403.37/297.20 [mark(f(X1, X2))] = [1] X1 + [1] 403.37/297.20 > [1] X1 + [0] 403.37/297.20 = [a__f(mark(X1), X2)] 403.37/297.20 403.37/297.20 [a__f(X, X)] = [1] X + [0] 403.37/297.20 >= [0] 403.37/297.20 = [a__h(a__a())] 403.37/297.20 403.37/297.20 [a__f(X1, X2)] = [1] X1 + [0] 403.37/297.20 ? [1] X1 + [1] 403.37/297.20 = [f(X1, X2)] 403.37/297.20 403.37/297.20 [a__a()] = [0] 403.37/297.20 >= [0] 403.37/297.20 = [a()] 403.37/297.20 403.37/297.20 [a__a()] = [0] 403.37/297.20 >= [0] 403.37/297.20 = [b()] 403.37/297.20 403.37/297.20 403.37/297.20 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 403.37/297.20 403.37/297.20 We are left with following problem, upon which TcT provides the 403.37/297.20 certificate MAYBE. 403.37/297.20 403.37/297.20 Strict Trs: 403.37/297.20 { a__g(X1, X2) -> g(X1, X2) 403.37/297.20 , mark(b()) -> b() 403.37/297.20 , mark(h(X)) -> a__h(mark(X)) 403.37/297.20 , a__f(X1, X2) -> f(X1, X2) 403.37/297.20 , a__a() -> a() 403.37/297.20 , a__a() -> b() } 403.37/297.20 Weak Trs: 403.37/297.20 { a__h(X) -> a__g(mark(X), X) 403.37/297.20 , a__h(X) -> h(X) 403.37/297.20 , a__g(a(), X) -> a__f(b(), X) 403.37/297.20 , mark(a()) -> a__a() 403.37/297.20 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 403.37/297.20 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 403.37/297.20 , a__f(X, X) -> a__h(a__a()) } 403.37/297.20 Obligation: 403.37/297.20 innermost runtime complexity 403.37/297.20 Answer: 403.37/297.20 MAYBE 403.37/297.20 403.37/297.20 The weightgap principle applies (using the following nonconstant 403.37/297.20 growth matrix-interpretation) 403.37/297.20 403.37/297.20 The following argument positions are usable: 403.37/297.20 Uargs(a__h) = {1}, Uargs(a__g) = {1}, Uargs(a__f) = {1} 403.37/297.20 403.37/297.20 TcT has computed the following matrix interpretation satisfying 403.37/297.20 not(EDA) and not(IDA(1)). 403.37/297.20 403.37/297.20 [a__h](x1) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [a__g](x1, x2) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [mark](x1) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [a] = [1] 403.37/297.20 403.37/297.20 [a__f](x1, x2) = [1] x1 + [1] 403.37/297.20 403.37/297.20 [b] = [0] 403.37/297.20 403.37/297.20 [a__a] = [1] 403.37/297.20 403.37/297.20 [h](x1) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [g](x1, x2) = [1] x1 + [4] 403.37/297.20 403.37/297.20 [f](x1, x2) = [1] x1 + [4] 403.37/297.20 403.37/297.20 The order satisfies the following ordering constraints: 403.37/297.20 403.37/297.20 [a__h(X)] = [1] X + [0] 403.37/297.20 >= [1] X + [0] 403.37/297.20 = [a__g(mark(X), X)] 403.37/297.20 403.37/297.20 [a__h(X)] = [1] X + [0] 403.37/297.20 >= [1] X + [0] 403.37/297.20 = [h(X)] 403.37/297.20 403.37/297.20 [a__g(X1, X2)] = [1] X1 + [0] 403.37/297.20 ? [1] X1 + [4] 403.37/297.20 = [g(X1, X2)] 403.37/297.20 403.37/297.20 [a__g(a(), X)] = [1] 403.37/297.20 >= [1] 403.37/297.20 = [a__f(b(), X)] 403.37/297.20 403.37/297.20 [mark(a())] = [1] 403.37/297.20 >= [1] 403.37/297.20 = [a__a()] 403.37/297.20 403.37/297.20 [mark(b())] = [0] 403.37/297.20 >= [0] 403.37/297.20 = [b()] 403.37/297.20 403.37/297.20 [mark(h(X))] = [1] X + [0] 403.37/297.20 >= [1] X + [0] 403.37/297.20 = [a__h(mark(X))] 403.37/297.20 403.37/297.20 [mark(g(X1, X2))] = [1] X1 + [4] 403.37/297.20 > [1] X1 + [0] 403.37/297.20 = [a__g(mark(X1), X2)] 403.37/297.20 403.37/297.20 [mark(f(X1, X2))] = [1] X1 + [4] 403.37/297.20 > [1] X1 + [1] 403.37/297.20 = [a__f(mark(X1), X2)] 403.37/297.20 403.37/297.20 [a__f(X, X)] = [1] X + [1] 403.37/297.20 >= [1] 403.37/297.20 = [a__h(a__a())] 403.37/297.20 403.37/297.20 [a__f(X1, X2)] = [1] X1 + [1] 403.37/297.20 ? [1] X1 + [4] 403.37/297.20 = [f(X1, X2)] 403.37/297.20 403.37/297.20 [a__a()] = [1] 403.37/297.20 >= [1] 403.37/297.20 = [a()] 403.37/297.20 403.37/297.20 [a__a()] = [1] 403.37/297.20 > [0] 403.37/297.20 = [b()] 403.37/297.20 403.37/297.20 403.37/297.20 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 403.37/297.20 403.37/297.20 We are left with following problem, upon which TcT provides the 403.37/297.20 certificate MAYBE. 403.37/297.20 403.37/297.20 Strict Trs: 403.37/297.20 { a__g(X1, X2) -> g(X1, X2) 403.37/297.20 , mark(b()) -> b() 403.37/297.20 , mark(h(X)) -> a__h(mark(X)) 403.37/297.20 , a__f(X1, X2) -> f(X1, X2) 403.37/297.20 , a__a() -> a() } 403.37/297.20 Weak Trs: 403.37/297.20 { a__h(X) -> a__g(mark(X), X) 403.37/297.20 , a__h(X) -> h(X) 403.37/297.20 , a__g(a(), X) -> a__f(b(), X) 403.37/297.20 , mark(a()) -> a__a() 403.37/297.20 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 403.37/297.20 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 403.37/297.20 , a__f(X, X) -> a__h(a__a()) 403.37/297.20 , a__a() -> b() } 403.37/297.20 Obligation: 403.37/297.20 innermost runtime complexity 403.37/297.20 Answer: 403.37/297.20 MAYBE 403.37/297.20 403.37/297.20 The weightgap principle applies (using the following nonconstant 403.37/297.20 growth matrix-interpretation) 403.37/297.20 403.37/297.20 The following argument positions are usable: 403.37/297.20 Uargs(a__h) = {1}, Uargs(a__g) = {1}, Uargs(a__f) = {1} 403.37/297.20 403.37/297.20 TcT has computed the following matrix interpretation satisfying 403.37/297.20 not(EDA) and not(IDA(1)). 403.37/297.20 403.37/297.20 [a__h](x1) = [1] x1 + [4] 403.37/297.20 403.37/297.20 [a__g](x1, x2) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [mark](x1) = [1] x1 + [1] 403.37/297.20 403.37/297.20 [a] = [4] 403.37/297.20 403.37/297.20 [a__f](x1, x2) = [1] x1 + [4] 403.37/297.20 403.37/297.20 [b] = [0] 403.37/297.20 403.37/297.20 [a__a] = [0] 403.37/297.20 403.37/297.20 [h](x1) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [g](x1, x2) = [1] x1 + [0] 403.37/297.20 403.37/297.20 [f](x1, x2) = [1] x1 + [7] 403.37/297.20 403.37/297.20 The order satisfies the following ordering constraints: 403.37/297.20 403.37/297.20 [a__h(X)] = [1] X + [4] 403.37/297.20 > [1] X + [1] 403.37/297.20 = [a__g(mark(X), X)] 403.37/297.20 403.37/297.20 [a__h(X)] = [1] X + [4] 403.37/297.20 > [1] X + [0] 403.37/297.20 = [h(X)] 403.37/297.20 403.37/297.20 [a__g(X1, X2)] = [1] X1 + [0] 403.37/297.20 >= [1] X1 + [0] 403.37/297.20 = [g(X1, X2)] 403.37/297.20 403.37/297.20 [a__g(a(), X)] = [4] 403.37/297.20 >= [4] 403.37/297.20 = [a__f(b(), X)] 403.37/297.20 403.37/297.20 [mark(a())] = [5] 403.37/297.20 > [0] 403.37/297.20 = [a__a()] 403.37/297.20 403.37/297.20 [mark(b())] = [1] 403.37/297.20 > [0] 403.37/297.20 = [b()] 403.37/297.20 403.37/297.20 [mark(h(X))] = [1] X + [1] 403.37/297.20 ? [1] X + [5] 403.37/297.20 = [a__h(mark(X))] 403.37/297.20 403.37/297.20 [mark(g(X1, X2))] = [1] X1 + [1] 403.37/297.20 >= [1] X1 + [1] 403.37/297.20 = [a__g(mark(X1), X2)] 403.37/297.20 403.37/297.20 [mark(f(X1, X2))] = [1] X1 + [8] 403.37/297.20 > [1] X1 + [5] 403.37/297.20 = [a__f(mark(X1), X2)] 403.37/297.20 403.37/297.20 [a__f(X, X)] = [1] X + [4] 403.37/297.20 >= [4] 403.37/297.20 = [a__h(a__a())] 403.37/297.20 403.37/297.20 [a__f(X1, X2)] = [1] X1 + [4] 403.37/297.20 ? [1] X1 + [7] 403.37/297.20 = [f(X1, X2)] 403.37/297.20 403.37/297.20 [a__a()] = [0] 403.37/297.20 ? [4] 403.37/297.20 = [a()] 403.37/297.20 403.37/297.20 [a__a()] = [0] 403.37/297.20 >= [0] 403.37/297.20 = [b()] 403.37/297.20 403.37/297.20 403.37/297.20 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 403.37/297.20 403.37/297.20 We are left with following problem, upon which TcT provides the 403.37/297.20 certificate MAYBE. 403.37/297.20 403.37/297.20 Strict Trs: 403.37/297.20 { a__g(X1, X2) -> g(X1, X2) 403.37/297.20 , mark(h(X)) -> a__h(mark(X)) 403.37/297.20 , a__f(X1, X2) -> f(X1, X2) 403.37/297.20 , a__a() -> a() } 403.37/297.20 Weak Trs: 403.37/297.20 { a__h(X) -> a__g(mark(X), X) 403.37/297.20 , a__h(X) -> h(X) 403.37/297.20 , a__g(a(), X) -> a__f(b(), X) 403.37/297.20 , mark(a()) -> a__a() 403.37/297.20 , mark(b()) -> b() 403.37/297.20 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 403.37/297.20 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 403.37/297.20 , a__f(X, X) -> a__h(a__a()) 403.37/297.20 , a__a() -> b() } 403.37/297.20 Obligation: 403.37/297.20 innermost runtime complexity 403.37/297.20 Answer: 403.37/297.20 MAYBE 403.37/297.20 403.37/297.20 None of the processors succeeded. 403.37/297.20 403.37/297.20 Details of failed attempt(s): 403.37/297.20 ----------------------------- 403.37/297.20 1) 'empty' failed due to the following reason: 403.37/297.20 403.37/297.20 Empty strict component of the problem is NOT empty. 403.37/297.20 403.37/297.20 2) 'With Problem ...' failed due to the following reason: 403.37/297.20 403.37/297.20 None of the processors succeeded. 403.37/297.20 403.37/297.20 Details of failed attempt(s): 403.37/297.20 ----------------------------- 403.37/297.20 1) 'empty' failed due to the following reason: 403.37/297.20 403.37/297.20 Empty strict component of the problem is NOT empty. 403.37/297.20 403.37/297.20 2) 'Fastest' failed due to the following reason: 403.37/297.20 403.37/297.20 None of the processors succeeded. 403.37/297.20 403.37/297.20 Details of failed attempt(s): 403.37/297.20 ----------------------------- 403.37/297.20 1) 'With Problem ...' failed due to the following reason: 403.37/297.20 403.37/297.20 None of the processors succeeded. 403.37/297.20 403.37/297.20 Details of failed attempt(s): 403.37/297.20 ----------------------------- 403.37/297.20 1) 'empty' failed due to the following reason: 403.37/297.20 403.37/297.20 Empty strict component of the problem is NOT empty. 403.37/297.20 403.37/297.20 2) 'With Problem ...' failed due to the following reason: 403.37/297.20 403.37/297.20 We use the processor 'matrix interpretation of dimension 2' to 403.37/297.20 orient following rules strictly. 403.37/297.20 403.37/297.20 Trs: { mark(h(X)) -> a__h(mark(X)) } 403.37/297.20 403.37/297.20 The induced complexity on above rules (modulo remaining rules) is 403.37/297.20 YES(?,O(n^2)) . These rules are moved into the corresponding weak 403.37/297.20 component(s). 403.37/297.20 403.37/297.20 Sub-proof: 403.37/297.20 ---------- 403.37/297.20 The following argument positions are usable: 403.37/297.20 Uargs(a__h) = {1}, Uargs(a__g) = {1}, Uargs(a__f) = {1} 403.37/297.20 403.37/297.20 TcT has computed the following constructor-based matrix 403.37/297.20 interpretation satisfying not(EDA). 403.37/297.20 403.37/297.20 [a__h](x1) = [1 7] x1 + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 403.37/297.20 [a__g](x1, x2) = [1 0] x1 + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 403.37/297.20 [mark](x1) = [1 1] x1 + [0] 403.37/297.20 [0 1] [0] 403.37/297.20 403.37/297.20 [a] = [0] 403.37/297.20 [0] 403.37/297.20 403.37/297.20 [a__f](x1, x2) = [1 0] x1 + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 403.37/297.20 [b] = [0] 403.37/297.20 [0] 403.37/297.20 403.37/297.20 [a__a] = [0] 403.37/297.20 [0] 403.37/297.20 403.37/297.20 [h](x1) = [1 7] x1 + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 403.37/297.20 [g](x1, x2) = [1 0] x1 + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 403.37/297.20 [f](x1, x2) = [1 0] x1 + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 403.37/297.20 The order satisfies the following ordering constraints: 403.37/297.20 403.37/297.20 [a__h(X)] = [1 7] X + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 >= [1 1] X + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 = [a__g(mark(X), X)] 403.37/297.20 403.37/297.20 [a__h(X)] = [1 7] X + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 >= [1 7] X + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 = [h(X)] 403.37/297.20 403.37/297.20 [a__g(X1, X2)] = [1 0] X1 + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 >= [1 0] X1 + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 = [g(X1, X2)] 403.37/297.20 403.37/297.20 [a__g(a(), X)] = [0] 403.37/297.20 [1] 403.37/297.20 >= [0] 403.37/297.20 [1] 403.37/297.20 = [a__f(b(), X)] 403.37/297.20 403.37/297.20 [mark(a())] = [0] 403.37/297.20 [0] 403.37/297.20 >= [0] 403.37/297.20 [0] 403.37/297.20 = [a__a()] 403.37/297.20 403.37/297.20 [mark(b())] = [0] 403.37/297.20 [0] 403.37/297.20 >= [0] 403.37/297.20 [0] 403.37/297.20 = [b()] 403.37/297.20 403.37/297.20 [mark(h(X))] = [1 8] X + [1] 403.37/297.20 [0 1] [1] 403.37/297.20 > [1 8] X + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 = [a__h(mark(X))] 403.37/297.20 403.37/297.20 [mark(g(X1, X2))] = [1 1] X1 + [1] 403.37/297.20 [0 1] [1] 403.37/297.20 > [1 1] X1 + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 = [a__g(mark(X1), X2)] 403.37/297.20 403.37/297.20 [mark(f(X1, X2))] = [1 1] X1 + [1] 403.37/297.20 [0 1] [1] 403.37/297.20 > [1 1] X1 + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 = [a__f(mark(X1), X2)] 403.37/297.20 403.37/297.20 [a__f(X, X)] = [1 0] X + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 >= [0] 403.37/297.20 [1] 403.37/297.20 = [a__h(a__a())] 403.37/297.20 403.37/297.20 [a__f(X1, X2)] = [1 0] X1 + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 >= [1 0] X1 + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 = [f(X1, X2)] 403.37/297.20 403.37/297.20 [a__a()] = [0] 403.37/297.20 [0] 403.37/297.20 >= [0] 403.37/297.20 [0] 403.37/297.20 = [a()] 403.37/297.20 403.37/297.20 [a__a()] = [0] 403.37/297.20 [0] 403.37/297.20 >= [0] 403.37/297.20 [0] 403.37/297.20 = [b()] 403.37/297.20 403.37/297.20 403.37/297.20 We return to the main proof. 403.37/297.20 403.37/297.20 We are left with following problem, upon which TcT provides the 403.37/297.20 certificate MAYBE. 403.37/297.20 403.37/297.20 Strict Trs: 403.37/297.20 { a__g(X1, X2) -> g(X1, X2) 403.37/297.20 , a__f(X1, X2) -> f(X1, X2) 403.37/297.20 , a__a() -> a() } 403.37/297.20 Weak Trs: 403.37/297.20 { a__h(X) -> a__g(mark(X), X) 403.37/297.20 , a__h(X) -> h(X) 403.37/297.20 , a__g(a(), X) -> a__f(b(), X) 403.37/297.20 , mark(a()) -> a__a() 403.37/297.20 , mark(b()) -> b() 403.37/297.20 , mark(h(X)) -> a__h(mark(X)) 403.37/297.20 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 403.37/297.20 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 403.37/297.20 , a__f(X, X) -> a__h(a__a()) 403.37/297.20 , a__a() -> b() } 403.37/297.20 Obligation: 403.37/297.20 innermost runtime complexity 403.37/297.20 Answer: 403.37/297.20 MAYBE 403.37/297.20 403.37/297.20 We use the processor 'matrix interpretation of dimension 2' to 403.37/297.20 orient following rules strictly. 403.37/297.20 403.37/297.20 Trs: { a__f(X1, X2) -> f(X1, X2) } 403.37/297.20 403.37/297.20 The induced complexity on above rules (modulo remaining rules) is 403.37/297.20 YES(?,O(n^2)) . These rules are moved into the corresponding weak 403.37/297.20 component(s). 403.37/297.20 403.37/297.20 Sub-proof: 403.37/297.20 ---------- 403.37/297.20 The following argument positions are usable: 403.37/297.20 Uargs(a__h) = {1}, Uargs(a__g) = {1}, Uargs(a__f) = {1} 403.37/297.20 403.37/297.20 TcT has computed the following constructor-based matrix 403.37/297.20 interpretation satisfying not(EDA). 403.37/297.20 403.37/297.20 [a__h](x1) = [1 4] x1 + [0] 403.37/297.20 [0 1] [1] 403.37/297.20 403.37/297.20 [a__g](x1, x2) = [1 0] x1 + [0] 403.37/297.21 [0 1] [1] 403.37/297.21 403.37/297.21 [mark](x1) = [1 2] x1 + [0] 403.37/297.21 [0 1] [0] 403.37/297.21 403.37/297.21 [a] = [1] 403.37/297.21 [0] 403.37/297.21 403.37/297.21 [a__f](x1, x2) = [1 0] x1 + [1] 403.37/297.21 [0 1] [1] 403.37/297.21 403.37/297.21 [b] = [0] 403.37/297.21 [0] 403.37/297.21 403.37/297.21 [a__a] = [1] 403.37/297.21 [0] 403.37/297.21 403.37/297.21 [h](x1) = [1 4] x1 + [0] 403.37/297.21 [0 1] [1] 403.37/297.21 403.37/297.21 [g](x1, x2) = [1 0] x1 + [0] 403.37/297.21 [0 1] [1] 403.37/297.21 403.37/297.21 [f](x1, x2) = [1 0] x1 + [0] 403.37/297.21 [0 1] [1] 403.37/297.21 403.37/297.21 The order satisfies the following ordering constraints: 403.37/297.21 403.37/297.21 [a__h(X)] = [1 4] X + [0] 403.37/297.21 [0 1] [1] 403.37/297.21 >= [1 2] X + [0] 403.37/297.21 [0 1] [1] 403.37/297.21 = [a__g(mark(X), X)] 403.37/297.21 403.37/297.21 [a__h(X)] = [1 4] X + [0] 403.37/297.21 [0 1] [1] 403.37/297.21 >= [1 4] X + [0] 403.37/297.21 [0 1] [1] 403.37/297.21 = [h(X)] 403.37/297.21 403.37/297.21 [a__g(X1, X2)] = [1 0] X1 + [0] 403.37/297.21 [0 1] [1] 403.37/297.21 >= [1 0] X1 + [0] 403.37/297.21 [0 1] [1] 403.37/297.21 = [g(X1, X2)] 403.37/297.21 403.37/297.21 [a__g(a(), X)] = [1] 403.37/297.21 [1] 403.37/297.21 >= [1] 403.37/297.21 [1] 403.37/297.21 = [a__f(b(), X)] 403.37/297.21 403.37/297.21 [mark(a())] = [1] 403.37/297.21 [0] 403.37/297.21 >= [1] 403.37/297.21 [0] 403.37/297.21 = [a__a()] 403.37/297.21 403.37/297.21 [mark(b())] = [0] 403.37/297.21 [0] 403.37/297.21 >= [0] 403.37/297.21 [0] 403.37/297.21 = [b()] 403.37/297.21 403.37/297.21 [mark(h(X))] = [1 6] X + [2] 403.37/297.21 [0 1] [1] 403.37/297.21 > [1 6] X + [0] 403.37/297.21 [0 1] [1] 403.37/297.21 = [a__h(mark(X))] 403.37/297.21 403.37/297.21 [mark(g(X1, X2))] = [1 2] X1 + [2] 403.37/297.21 [0 1] [1] 403.37/297.21 > [1 2] X1 + [0] 403.37/297.21 [0 1] [1] 403.37/297.21 = [a__g(mark(X1), X2)] 403.37/297.21 403.37/297.21 [mark(f(X1, X2))] = [1 2] X1 + [2] 403.37/297.21 [0 1] [1] 403.37/297.21 > [1 2] X1 + [1] 403.37/297.21 [0 1] [1] 403.37/297.21 = [a__f(mark(X1), X2)] 403.37/297.21 403.37/297.21 [a__f(X, X)] = [1 0] X + [1] 403.37/297.21 [0 1] [1] 403.37/297.21 >= [1] 403.37/297.21 [1] 403.37/297.21 = [a__h(a__a())] 403.37/297.21 403.37/297.21 [a__f(X1, X2)] = [1 0] X1 + [1] 403.37/297.21 [0 1] [1] 403.37/297.21 > [1 0] X1 + [0] 403.37/297.21 [0 1] [1] 403.37/297.21 = [f(X1, X2)] 403.37/297.21 403.37/297.21 [a__a()] = [1] 403.37/297.21 [0] 403.37/297.21 >= [1] 403.37/297.21 [0] 403.37/297.21 = [a()] 403.37/297.21 403.37/297.21 [a__a()] = [1] 403.37/297.21 [0] 403.37/297.21 > [0] 403.37/297.21 [0] 403.37/297.21 = [b()] 403.37/297.21 403.37/297.21 403.37/297.21 We return to the main proof. 403.37/297.21 403.37/297.21 We are left with following problem, upon which TcT provides the 403.37/297.21 certificate MAYBE. 403.37/297.21 403.37/297.21 Strict Trs: 403.37/297.21 { a__g(X1, X2) -> g(X1, X2) 403.37/297.21 , a__a() -> a() } 403.37/297.21 Weak Trs: 403.37/297.21 { a__h(X) -> a__g(mark(X), X) 403.37/297.21 , a__h(X) -> h(X) 403.37/297.21 , a__g(a(), X) -> a__f(b(), X) 403.37/297.21 , mark(a()) -> a__a() 403.37/297.21 , mark(b()) -> b() 403.37/297.21 , mark(h(X)) -> a__h(mark(X)) 403.37/297.21 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 403.37/297.21 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 403.37/297.21 , a__f(X, X) -> a__h(a__a()) 403.37/297.21 , a__f(X1, X2) -> f(X1, X2) 403.37/297.21 , a__a() -> b() } 403.37/297.21 Obligation: 403.37/297.21 innermost runtime complexity 403.37/297.21 Answer: 403.37/297.21 MAYBE 403.37/297.21 403.37/297.21 We use the processor 'matrix interpretation of dimension 2' to 403.37/297.21 orient following rules strictly. 403.37/297.21 403.37/297.21 Trs: { a__g(X1, X2) -> g(X1, X2) } 403.37/297.21 403.37/297.21 The induced complexity on above rules (modulo remaining rules) is 403.37/297.21 YES(?,O(n^2)) . These rules are moved into the corresponding weak 403.37/297.21 component(s). 403.37/297.21 403.37/297.21 Sub-proof: 403.37/297.21 ---------- 403.37/297.21 The following argument positions are usable: 403.37/297.21 Uargs(a__h) = {1}, Uargs(a__g) = {1}, Uargs(a__f) = {1} 403.37/297.21 403.37/297.21 TcT has computed the following constructor-based matrix 403.37/297.21 interpretation satisfying not(EDA). 403.37/297.21 403.37/297.21 [a__h](x1) = [1 1] x1 + [1] 403.37/297.21 [0 1] [4] 403.37/297.21 403.37/297.21 [a__g](x1, x2) = [1 0] x1 + [1] 403.37/297.21 [0 1] [4] 403.37/297.21 403.37/297.21 [mark](x1) = [1 1] x1 + [0] 403.37/297.21 [0 1] [0] 403.37/297.21 403.37/297.21 [a] = [0] 403.37/297.21 [0] 403.37/297.21 403.37/297.21 [a__f](x1, x2) = [1 0] x1 + [1] 403.37/297.21 [0 1] [4] 403.37/297.21 403.37/297.21 [b] = [0] 403.37/297.21 [0] 403.37/297.21 403.37/297.21 [a__a] = [0] 403.37/297.21 [0] 403.37/297.21 403.37/297.21 [h](x1) = [1 1] x1 + [0] 403.37/297.21 [0 1] [4] 403.37/297.21 403.37/297.21 [g](x1, x2) = [1 0] x1 + [0] 403.37/297.21 [0 1] [4] 403.37/297.21 403.37/297.21 [f](x1, x2) = [1 0] x1 + [0] 403.37/297.21 [0 1] [4] 403.37/297.21 403.37/297.21 The order satisfies the following ordering constraints: 403.37/297.21 403.37/297.21 [a__h(X)] = [1 1] X + [1] 403.37/297.21 [0 1] [4] 403.37/297.21 >= [1 1] X + [1] 403.37/297.21 [0 1] [4] 403.37/297.21 = [a__g(mark(X), X)] 403.37/297.21 403.37/297.21 [a__h(X)] = [1 1] X + [1] 403.37/297.21 [0 1] [4] 403.37/297.21 > [1 1] X + [0] 403.37/297.21 [0 1] [4] 403.37/297.21 = [h(X)] 403.37/297.21 403.37/297.21 [a__g(X1, X2)] = [1 0] X1 + [1] 403.37/297.21 [0 1] [4] 403.37/297.21 > [1 0] X1 + [0] 403.37/297.21 [0 1] [4] 403.37/297.21 = [g(X1, X2)] 403.37/297.21 403.37/297.21 [a__g(a(), X)] = [1] 403.37/297.21 [4] 403.37/297.21 >= [1] 403.37/297.21 [4] 403.37/297.21 = [a__f(b(), X)] 403.37/297.21 403.37/297.21 [mark(a())] = [0] 403.37/297.21 [0] 403.37/297.21 >= [0] 403.37/297.21 [0] 403.37/297.21 = [a__a()] 403.37/297.21 403.37/297.21 [mark(b())] = [0] 403.37/297.21 [0] 403.37/297.21 >= [0] 403.37/297.21 [0] 403.37/297.21 = [b()] 403.37/297.21 403.37/297.21 [mark(h(X))] = [1 2] X + [4] 403.37/297.21 [0 1] [4] 403.37/297.21 > [1 2] X + [1] 403.37/297.21 [0 1] [4] 403.37/297.21 = [a__h(mark(X))] 403.37/297.21 403.37/297.21 [mark(g(X1, X2))] = [1 1] X1 + [4] 403.37/297.21 [0 1] [4] 403.37/297.21 > [1 1] X1 + [1] 403.37/297.21 [0 1] [4] 403.37/297.21 = [a__g(mark(X1), X2)] 403.37/297.21 403.37/297.21 [mark(f(X1, X2))] = [1 1] X1 + [4] 403.37/297.21 [0 1] [4] 403.37/297.21 > [1 1] X1 + [1] 403.37/297.21 [0 1] [4] 403.37/297.21 = [a__f(mark(X1), X2)] 403.37/297.21 403.37/297.21 [a__f(X, X)] = [1 0] X + [1] 403.37/297.21 [0 1] [4] 403.37/297.21 >= [1] 403.37/297.21 [4] 403.37/297.21 = [a__h(a__a())] 403.37/297.21 403.37/297.21 [a__f(X1, X2)] = [1 0] X1 + [1] 403.37/297.21 [0 1] [4] 403.37/297.21 > [1 0] X1 + [0] 403.37/297.21 [0 1] [4] 403.37/297.21 = [f(X1, X2)] 403.37/297.21 403.37/297.21 [a__a()] = [0] 403.37/297.21 [0] 403.37/297.21 >= [0] 403.37/297.21 [0] 403.37/297.21 = [a()] 403.37/297.21 403.37/297.21 [a__a()] = [0] 403.37/297.21 [0] 403.37/297.21 >= [0] 403.37/297.21 [0] 403.37/297.21 = [b()] 403.37/297.21 403.37/297.21 403.37/297.21 We return to the main proof. 403.37/297.21 403.37/297.21 We are left with following problem, upon which TcT provides the 403.37/297.21 certificate MAYBE. 403.37/297.21 403.37/297.21 Strict Trs: { a__a() -> a() } 403.37/297.21 Weak Trs: 403.37/297.21 { a__h(X) -> a__g(mark(X), X) 403.37/297.21 , a__h(X) -> h(X) 403.37/297.21 , a__g(X1, X2) -> g(X1, X2) 403.37/297.21 , a__g(a(), X) -> a__f(b(), X) 403.37/297.21 , mark(a()) -> a__a() 403.37/297.21 , mark(b()) -> b() 403.37/297.21 , mark(h(X)) -> a__h(mark(X)) 403.37/297.21 , mark(g(X1, X2)) -> a__g(mark(X1), X2) 403.37/297.21 , mark(f(X1, X2)) -> a__f(mark(X1), X2) 403.37/297.21 , a__f(X, X) -> a__h(a__a()) 403.37/297.21 , a__f(X1, X2) -> f(X1, X2) 403.37/297.21 , a__a() -> b() } 403.37/297.21 Obligation: 403.37/297.21 innermost runtime complexity 403.37/297.21 Answer: 403.37/297.21 MAYBE 403.37/297.21 403.37/297.21 None of the processors succeeded. 403.37/297.21 403.37/297.21 Details of failed attempt(s): 403.37/297.21 ----------------------------- 403.37/297.21 1) 'empty' failed due to the following reason: 403.37/297.21 403.37/297.21 Empty strict component of the problem is NOT empty. 403.37/297.21 403.37/297.21 2) 'With Problem ...' failed due to the following reason: 403.37/297.21 403.37/297.21 None of the processors succeeded. 403.37/297.21 403.37/297.21 Details of failed attempt(s): 403.37/297.21 ----------------------------- 403.37/297.21 1) 'empty' failed due to the following reason: 403.37/297.21 403.37/297.21 Empty strict component of the problem is NOT empty. 403.37/297.21 403.37/297.21 2) 'With Problem ...' failed due to the following reason: 403.37/297.21 403.37/297.21 Empty strict component of the problem is NOT empty. 403.37/297.21 403.37/297.21 403.37/297.21 403.37/297.21 403.37/297.21 2) 'With Problem ...' failed due to the following reason: 403.37/297.21 403.37/297.21 None of the processors succeeded. 403.37/297.21 403.37/297.21 Details of failed attempt(s): 403.37/297.21 ----------------------------- 403.37/297.21 1) 'empty' failed due to the following reason: 403.37/297.21 403.37/297.21 Empty strict component of the problem is NOT empty. 403.37/297.21 403.37/297.21 2) 'With Problem ...' failed due to the following reason: 403.37/297.21 403.37/297.21 Empty strict component of the problem is NOT empty. 403.37/297.21 403.37/297.21 403.37/297.21 403.37/297.21 403.37/297.21 403.37/297.21 2) 'Best' failed due to the following reason: 403.37/297.21 403.37/297.21 None of the processors succeeded. 403.37/297.21 403.37/297.21 Details of failed attempt(s): 403.37/297.21 ----------------------------- 403.37/297.21 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 403.37/297.21 following reason: 403.37/297.21 403.37/297.21 The input cannot be shown compatible 403.37/297.21 403.37/297.21 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 403.37/297.21 to the following reason: 403.37/297.21 403.37/297.21 The input cannot be shown compatible 403.37/297.21 403.37/297.21 403.37/297.21 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 403.37/297.21 failed due to the following reason: 403.37/297.21 403.37/297.21 None of the processors succeeded. 403.37/297.21 403.37/297.21 Details of failed attempt(s): 403.37/297.21 ----------------------------- 403.37/297.21 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 403.37/297.21 failed due to the following reason: 403.37/297.21 403.37/297.21 match-boundness of the problem could not be verified. 403.37/297.21 403.37/297.21 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 403.37/297.21 failed due to the following reason: 403.37/297.21 403.37/297.21 match-boundness of the problem could not be verified. 403.37/297.21 403.37/297.21 403.37/297.21 403.37/297.21 403.37/297.21 403.37/297.21 Arrrr.. 403.37/297.26 EOF