MAYBE 785.76/297.05 MAYBE 785.76/297.05 785.76/297.05 We are left with following problem, upon which TcT provides the 785.76/297.05 certificate MAYBE. 785.76/297.05 785.76/297.05 Strict Trs: 785.76/297.05 { a__U11(X1, X2, X3) -> U11(X1, X2, X3) 785.76/297.05 , a__U11(tt(), M, N) -> a__U12(tt(), M, N) 785.76/297.05 , a__U12(X1, X2, X3) -> U12(X1, X2, X3) 785.76/297.05 , a__U12(tt(), M, N) -> s(a__plus(mark(N), mark(M))) 785.76/297.05 , a__plus(X1, X2) -> plus(X1, X2) 785.76/297.05 , a__plus(N, s(M)) -> a__U11(tt(), M, N) 785.76/297.05 , a__plus(N, 0()) -> mark(N) 785.76/297.05 , mark(tt()) -> tt() 785.76/297.05 , mark(s(X)) -> s(mark(X)) 785.76/297.05 , mark(0()) -> 0() 785.76/297.05 , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3) 785.76/297.05 , mark(U12(X1, X2, X3)) -> a__U12(mark(X1), X2, X3) 785.76/297.05 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) } 785.76/297.05 Obligation: 785.76/297.05 innermost runtime complexity 785.76/297.05 Answer: 785.76/297.05 MAYBE 785.76/297.05 785.76/297.05 None of the processors succeeded. 785.76/297.05 785.76/297.05 Details of failed attempt(s): 785.76/297.05 ----------------------------- 785.76/297.05 1) 'empty' failed due to the following reason: 785.76/297.05 785.76/297.05 Empty strict component of the problem is NOT empty. 785.76/297.05 785.76/297.05 2) 'Best' failed due to the following reason: 785.76/297.05 785.76/297.05 None of the processors succeeded. 785.76/297.05 785.76/297.05 Details of failed attempt(s): 785.76/297.05 ----------------------------- 785.76/297.05 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 785.76/297.05 following reason: 785.76/297.05 785.76/297.05 Computation stopped due to timeout after 297.0 seconds. 785.76/297.05 785.76/297.05 2) 'Best' failed due to the following reason: 785.76/297.05 785.76/297.05 None of the processors succeeded. 785.76/297.05 785.76/297.05 Details of failed attempt(s): 785.76/297.05 ----------------------------- 785.76/297.05 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 785.76/297.05 seconds)' failed due to the following reason: 785.76/297.05 785.76/297.05 The weightgap principle applies (using the following nonconstant 785.76/297.05 growth matrix-interpretation) 785.76/297.05 785.76/297.05 The following argument positions are usable: 785.76/297.05 Uargs(a__U11) = {1}, Uargs(a__U12) = {1}, Uargs(s) = {1}, 785.76/297.05 Uargs(a__plus) = {1, 2} 785.76/297.05 785.76/297.05 TcT has computed the following matrix interpretation satisfying 785.76/297.05 not(EDA) and not(IDA(1)). 785.76/297.05 785.76/297.05 [a__U11](x1, x2, x3) = [1] x1 + [4] 785.76/297.05 785.76/297.05 [tt] = [0] 785.76/297.05 785.76/297.05 [a__U12](x1, x2, x3) = [1] x1 + [0] 785.76/297.05 785.76/297.05 [s](x1) = [1] x1 + [0] 785.76/297.05 785.76/297.05 [a__plus](x1, x2) = [1] x1 + [1] x2 + [0] 785.76/297.05 785.76/297.05 [mark](x1) = [0] 785.76/297.05 785.76/297.05 [0] = [0] 785.76/297.05 785.76/297.05 [U11](x1, x2, x3) = [1] x1 + [3] 785.76/297.05 785.76/297.05 [U12](x1, x2, x3) = [1] x1 + [7] 785.76/297.05 785.76/297.05 [plus](x1, x2) = [1] x1 + [1] x2 + [7] 785.76/297.05 785.76/297.05 The order satisfies the following ordering constraints: 785.76/297.05 785.76/297.05 [a__U11(X1, X2, X3)] = [1] X1 + [4] 785.76/297.05 > [1] X1 + [3] 785.76/297.05 = [U11(X1, X2, X3)] 785.76/297.05 785.76/297.05 [a__U11(tt(), M, N)] = [4] 785.76/297.05 > [0] 785.76/297.05 = [a__U12(tt(), M, N)] 785.76/297.05 785.76/297.05 [a__U12(X1, X2, X3)] = [1] X1 + [0] 785.76/297.05 ? [1] X1 + [7] 785.76/297.05 = [U12(X1, X2, X3)] 785.76/297.05 785.76/297.05 [a__U12(tt(), M, N)] = [0] 785.76/297.05 >= [0] 785.76/297.05 = [s(a__plus(mark(N), mark(M)))] 785.76/297.05 785.76/297.05 [a__plus(X1, X2)] = [1] X1 + [1] X2 + [0] 785.76/297.05 ? [1] X1 + [1] X2 + [7] 785.76/297.05 = [plus(X1, X2)] 785.76/297.05 785.76/297.05 [a__plus(N, s(M))] = [1] M + [1] N + [0] 785.76/297.05 ? [4] 785.76/297.05 = [a__U11(tt(), M, N)] 785.76/297.05 785.76/297.05 [a__plus(N, 0())] = [1] N + [0] 785.76/297.05 >= [0] 785.76/297.05 = [mark(N)] 785.76/297.05 785.76/297.05 [mark(tt())] = [0] 785.76/297.05 >= [0] 785.76/297.05 = [tt()] 785.76/297.05 785.76/297.05 [mark(s(X))] = [0] 785.76/297.05 >= [0] 785.76/297.05 = [s(mark(X))] 785.76/297.05 785.76/297.05 [mark(0())] = [0] 785.76/297.05 >= [0] 785.76/297.05 = [0()] 785.76/297.05 785.76/297.05 [mark(U11(X1, X2, X3))] = [0] 785.76/297.05 ? [4] 785.76/297.05 = [a__U11(mark(X1), X2, X3)] 785.76/297.05 785.76/297.05 [mark(U12(X1, X2, X3))] = [0] 785.76/297.05 >= [0] 785.76/297.05 = [a__U12(mark(X1), X2, X3)] 785.76/297.05 785.76/297.05 [mark(plus(X1, X2))] = [0] 785.76/297.05 >= [0] 785.76/297.05 = [a__plus(mark(X1), mark(X2))] 785.76/297.05 785.76/297.05 785.76/297.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 785.76/297.05 785.76/297.05 We are left with following problem, upon which TcT provides the 785.76/297.05 certificate MAYBE. 785.76/297.05 785.76/297.05 Strict Trs: 785.76/297.05 { a__U12(X1, X2, X3) -> U12(X1, X2, X3) 785.76/297.05 , a__U12(tt(), M, N) -> s(a__plus(mark(N), mark(M))) 785.76/297.05 , a__plus(X1, X2) -> plus(X1, X2) 785.76/297.05 , a__plus(N, s(M)) -> a__U11(tt(), M, N) 785.76/297.05 , a__plus(N, 0()) -> mark(N) 785.76/297.05 , mark(tt()) -> tt() 785.76/297.05 , mark(s(X)) -> s(mark(X)) 785.76/297.05 , mark(0()) -> 0() 785.76/297.05 , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3) 785.76/297.05 , mark(U12(X1, X2, X3)) -> a__U12(mark(X1), X2, X3) 785.76/297.05 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) } 785.76/297.05 Weak Trs: 785.76/297.05 { a__U11(X1, X2, X3) -> U11(X1, X2, X3) 785.76/297.05 , a__U11(tt(), M, N) -> a__U12(tt(), M, N) } 785.76/297.05 Obligation: 785.76/297.05 innermost runtime complexity 785.76/297.05 Answer: 785.76/297.05 MAYBE 785.76/297.05 785.76/297.05 The weightgap principle applies (using the following nonconstant 785.76/297.05 growth matrix-interpretation) 785.76/297.05 785.76/297.05 The following argument positions are usable: 785.76/297.05 Uargs(a__U11) = {1}, Uargs(a__U12) = {1}, Uargs(s) = {1}, 785.76/297.05 Uargs(a__plus) = {1, 2} 785.76/297.05 785.76/297.05 TcT has computed the following matrix interpretation satisfying 785.76/297.05 not(EDA) and not(IDA(1)). 785.76/297.05 785.76/297.05 [a__U11](x1, x2, x3) = [1] x1 + [4] 785.76/297.05 785.76/297.05 [tt] = [4] 785.76/297.05 785.76/297.05 [a__U12](x1, x2, x3) = [1] x1 + [1] 785.76/297.05 785.76/297.05 [s](x1) = [1] x1 + [0] 785.76/297.05 785.76/297.05 [a__plus](x1, x2) = [1] x1 + [1] x2 + [0] 785.76/297.05 785.76/297.05 [mark](x1) = [0] 785.76/297.05 785.76/297.05 [0] = [0] 785.76/297.05 785.76/297.05 [U11](x1, x2, x3) = [1] x1 + [3] 785.76/297.05 785.76/297.05 [U12](x1, x2, x3) = [1] x1 + [0] 785.76/297.05 785.76/297.05 [plus](x1, x2) = [1] x1 + [1] x2 + [7] 785.76/297.05 785.76/297.05 The order satisfies the following ordering constraints: 785.76/297.05 785.76/297.05 [a__U11(X1, X2, X3)] = [1] X1 + [4] 785.76/297.05 > [1] X1 + [3] 785.76/297.05 = [U11(X1, X2, X3)] 785.76/297.05 785.76/297.05 [a__U11(tt(), M, N)] = [8] 785.76/297.05 > [5] 785.76/297.05 = [a__U12(tt(), M, N)] 785.76/297.05 785.76/297.05 [a__U12(X1, X2, X3)] = [1] X1 + [1] 785.76/297.05 > [1] X1 + [0] 785.76/297.05 = [U12(X1, X2, X3)] 785.76/297.05 785.76/297.05 [a__U12(tt(), M, N)] = [5] 785.76/297.05 > [0] 785.76/297.05 = [s(a__plus(mark(N), mark(M)))] 785.76/297.05 785.76/297.05 [a__plus(X1, X2)] = [1] X1 + [1] X2 + [0] 785.76/297.05 ? [1] X1 + [1] X2 + [7] 785.76/297.05 = [plus(X1, X2)] 785.76/297.05 785.76/297.05 [a__plus(N, s(M))] = [1] M + [1] N + [0] 785.76/297.05 ? [8] 785.76/297.05 = [a__U11(tt(), M, N)] 785.76/297.05 785.76/297.05 [a__plus(N, 0())] = [1] N + [0] 785.76/297.05 >= [0] 785.76/297.05 = [mark(N)] 785.76/297.05 785.76/297.05 [mark(tt())] = [0] 785.76/297.05 ? [4] 785.76/297.05 = [tt()] 785.76/297.05 785.76/297.05 [mark(s(X))] = [0] 785.76/297.05 >= [0] 785.76/297.05 = [s(mark(X))] 785.76/297.05 785.76/297.05 [mark(0())] = [0] 785.76/297.05 >= [0] 785.76/297.05 = [0()] 785.76/297.05 785.76/297.05 [mark(U11(X1, X2, X3))] = [0] 785.76/297.05 ? [4] 785.76/297.05 = [a__U11(mark(X1), X2, X3)] 785.76/297.05 785.76/297.05 [mark(U12(X1, X2, X3))] = [0] 785.76/297.05 ? [1] 785.76/297.05 = [a__U12(mark(X1), X2, X3)] 785.76/297.05 785.76/297.05 [mark(plus(X1, X2))] = [0] 785.76/297.05 >= [0] 785.76/297.05 = [a__plus(mark(X1), mark(X2))] 785.76/297.05 785.76/297.05 785.76/297.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 785.76/297.05 785.76/297.05 We are left with following problem, upon which TcT provides the 785.76/297.05 certificate MAYBE. 785.76/297.05 785.76/297.05 Strict Trs: 785.76/297.05 { a__plus(X1, X2) -> plus(X1, X2) 785.76/297.05 , a__plus(N, s(M)) -> a__U11(tt(), M, N) 785.76/297.05 , a__plus(N, 0()) -> mark(N) 785.76/297.05 , mark(tt()) -> tt() 785.76/297.05 , mark(s(X)) -> s(mark(X)) 785.76/297.05 , mark(0()) -> 0() 785.76/297.05 , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3) 785.76/297.05 , mark(U12(X1, X2, X3)) -> a__U12(mark(X1), X2, X3) 785.76/297.05 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) } 785.76/297.05 Weak Trs: 785.76/297.05 { a__U11(X1, X2, X3) -> U11(X1, X2, X3) 785.76/297.05 , a__U11(tt(), M, N) -> a__U12(tt(), M, N) 785.76/297.05 , a__U12(X1, X2, X3) -> U12(X1, X2, X3) 785.76/297.05 , a__U12(tt(), M, N) -> s(a__plus(mark(N), mark(M))) } 785.76/297.05 Obligation: 785.76/297.05 innermost runtime complexity 785.76/297.05 Answer: 785.76/297.05 MAYBE 785.76/297.05 785.76/297.05 The weightgap principle applies (using the following nonconstant 785.76/297.05 growth matrix-interpretation) 785.76/297.05 785.76/297.05 The following argument positions are usable: 785.76/297.05 Uargs(a__U11) = {1}, Uargs(a__U12) = {1}, Uargs(s) = {1}, 785.76/297.05 Uargs(a__plus) = {1, 2} 785.76/297.05 785.76/297.05 TcT has computed the following matrix interpretation satisfying 785.76/297.05 not(EDA) and not(IDA(1)). 785.76/297.05 785.76/297.05 [a__U11](x1, x2, x3) = [1] x1 + [1] 785.76/297.05 785.76/297.05 [tt] = [7] 785.76/297.05 785.76/297.05 [a__U12](x1, x2, x3) = [1] x1 + [1] 785.76/297.05 785.76/297.05 [s](x1) = [1] x1 + [0] 785.76/297.05 785.76/297.05 [a__plus](x1, x2) = [1] x1 + [1] x2 + [4] 785.76/297.05 785.76/297.05 [mark](x1) = [0] 785.76/297.05 785.76/297.05 [0] = [0] 785.76/297.05 785.76/297.05 [U11](x1, x2, x3) = [1] x1 + [1] 785.76/297.05 785.76/297.05 [U12](x1, x2, x3) = [1] x1 + [1] 785.76/297.05 785.76/297.05 [plus](x1, x2) = [1] x1 + [1] x2 + [3] 785.76/297.05 785.76/297.05 The order satisfies the following ordering constraints: 785.76/297.05 785.76/297.05 [a__U11(X1, X2, X3)] = [1] X1 + [1] 785.76/297.05 >= [1] X1 + [1] 785.76/297.05 = [U11(X1, X2, X3)] 785.76/297.05 785.76/297.05 [a__U11(tt(), M, N)] = [8] 785.76/297.05 >= [8] 785.76/297.05 = [a__U12(tt(), M, N)] 785.76/297.05 785.76/297.05 [a__U12(X1, X2, X3)] = [1] X1 + [1] 785.76/297.05 >= [1] X1 + [1] 785.76/297.05 = [U12(X1, X2, X3)] 785.76/297.06 785.76/297.06 [a__U12(tt(), M, N)] = [8] 785.76/297.06 > [4] 785.76/297.06 = [s(a__plus(mark(N), mark(M)))] 785.76/297.06 785.76/297.06 [a__plus(X1, X2)] = [1] X1 + [1] X2 + [4] 785.76/297.06 > [1] X1 + [1] X2 + [3] 785.76/297.06 = [plus(X1, X2)] 785.76/297.06 785.76/297.06 [a__plus(N, s(M))] = [1] M + [1] N + [4] 785.76/297.06 ? [8] 785.76/297.06 = [a__U11(tt(), M, N)] 785.76/297.06 785.76/297.06 [a__plus(N, 0())] = [1] N + [4] 785.76/297.06 > [0] 785.76/297.06 = [mark(N)] 785.76/297.06 785.76/297.06 [mark(tt())] = [0] 785.76/297.06 ? [7] 785.76/297.06 = [tt()] 785.76/297.06 785.76/297.06 [mark(s(X))] = [0] 785.76/297.06 >= [0] 785.76/297.06 = [s(mark(X))] 785.76/297.06 785.76/297.06 [mark(0())] = [0] 785.76/297.06 >= [0] 785.76/297.06 = [0()] 785.76/297.06 785.76/297.06 [mark(U11(X1, X2, X3))] = [0] 785.76/297.06 ? [1] 785.76/297.06 = [a__U11(mark(X1), X2, X3)] 785.76/297.06 785.76/297.06 [mark(U12(X1, X2, X3))] = [0] 785.76/297.06 ? [1] 785.76/297.06 = [a__U12(mark(X1), X2, X3)] 785.76/297.06 785.76/297.06 [mark(plus(X1, X2))] = [0] 785.76/297.06 ? [4] 785.76/297.06 = [a__plus(mark(X1), mark(X2))] 785.76/297.06 785.76/297.06 785.76/297.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 785.76/297.06 785.76/297.06 We are left with following problem, upon which TcT provides the 785.76/297.06 certificate MAYBE. 785.76/297.06 785.76/297.06 Strict Trs: 785.76/297.06 { a__plus(N, s(M)) -> a__U11(tt(), M, N) 785.76/297.06 , mark(tt()) -> tt() 785.76/297.06 , mark(s(X)) -> s(mark(X)) 785.76/297.06 , mark(0()) -> 0() 785.76/297.06 , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3) 785.76/297.06 , mark(U12(X1, X2, X3)) -> a__U12(mark(X1), X2, X3) 785.76/297.06 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) } 785.76/297.06 Weak Trs: 785.76/297.06 { a__U11(X1, X2, X3) -> U11(X1, X2, X3) 785.76/297.06 , a__U11(tt(), M, N) -> a__U12(tt(), M, N) 785.76/297.06 , a__U12(X1, X2, X3) -> U12(X1, X2, X3) 785.76/297.06 , a__U12(tt(), M, N) -> s(a__plus(mark(N), mark(M))) 785.76/297.06 , a__plus(X1, X2) -> plus(X1, X2) 785.76/297.06 , a__plus(N, 0()) -> mark(N) } 785.76/297.06 Obligation: 785.76/297.06 innermost runtime complexity 785.76/297.06 Answer: 785.76/297.06 MAYBE 785.76/297.06 785.76/297.06 The weightgap principle applies (using the following nonconstant 785.76/297.06 growth matrix-interpretation) 785.76/297.06 785.76/297.06 The following argument positions are usable: 785.76/297.06 Uargs(a__U11) = {1}, Uargs(a__U12) = {1}, Uargs(s) = {1}, 785.76/297.06 Uargs(a__plus) = {1, 2} 785.76/297.06 785.76/297.06 TcT has computed the following matrix interpretation satisfying 785.76/297.06 not(EDA) and not(IDA(1)). 785.76/297.06 785.76/297.06 [a__U11](x1, x2, x3) = [1] x1 + [6] 785.76/297.06 785.76/297.06 [tt] = [7] 785.76/297.06 785.76/297.06 [a__U12](x1, x2, x3) = [1] x1 + [6] 785.76/297.06 785.76/297.06 [s](x1) = [1] x1 + [4] 785.76/297.06 785.76/297.06 [a__plus](x1, x2) = [1] x1 + [1] x2 + [1] 785.76/297.06 785.76/297.06 [mark](x1) = [4] 785.76/297.06 785.76/297.06 [0] = [3] 785.76/297.06 785.76/297.06 [U11](x1, x2, x3) = [1] x1 + [3] 785.76/297.06 785.76/297.06 [U12](x1, x2, x3) = [1] x1 + [3] 785.76/297.06 785.76/297.06 [plus](x1, x2) = [1] x1 + [1] x2 + [1] 785.76/297.06 785.76/297.06 The order satisfies the following ordering constraints: 785.76/297.06 785.76/297.06 [a__U11(X1, X2, X3)] = [1] X1 + [6] 785.76/297.06 > [1] X1 + [3] 785.76/297.06 = [U11(X1, X2, X3)] 785.76/297.06 785.76/297.06 [a__U11(tt(), M, N)] = [13] 785.76/297.06 >= [13] 785.76/297.06 = [a__U12(tt(), M, N)] 785.76/297.06 785.76/297.06 [a__U12(X1, X2, X3)] = [1] X1 + [6] 785.76/297.06 > [1] X1 + [3] 785.76/297.06 = [U12(X1, X2, X3)] 785.76/297.06 785.76/297.06 [a__U12(tt(), M, N)] = [13] 785.76/297.06 >= [13] 785.76/297.06 = [s(a__plus(mark(N), mark(M)))] 785.76/297.06 785.76/297.06 [a__plus(X1, X2)] = [1] X1 + [1] X2 + [1] 785.76/297.06 >= [1] X1 + [1] X2 + [1] 785.76/297.06 = [plus(X1, X2)] 785.76/297.06 785.76/297.06 [a__plus(N, s(M))] = [1] M + [1] N + [5] 785.76/297.06 ? [13] 785.76/297.06 = [a__U11(tt(), M, N)] 785.76/297.06 785.76/297.06 [a__plus(N, 0())] = [1] N + [4] 785.76/297.06 >= [4] 785.76/297.06 = [mark(N)] 785.76/297.06 785.76/297.06 [mark(tt())] = [4] 785.76/297.06 ? [7] 785.76/297.06 = [tt()] 785.76/297.06 785.76/297.06 [mark(s(X))] = [4] 785.76/297.06 ? [8] 785.76/297.06 = [s(mark(X))] 785.76/297.06 785.76/297.06 [mark(0())] = [4] 785.76/297.06 > [3] 785.76/297.06 = [0()] 785.76/297.06 785.76/297.06 [mark(U11(X1, X2, X3))] = [4] 785.76/297.06 ? [10] 785.76/297.06 = [a__U11(mark(X1), X2, X3)] 785.76/297.06 785.76/297.06 [mark(U12(X1, X2, X3))] = [4] 785.76/297.06 ? [10] 785.76/297.06 = [a__U12(mark(X1), X2, X3)] 785.76/297.06 785.76/297.06 [mark(plus(X1, X2))] = [4] 785.76/297.06 ? [9] 785.76/297.06 = [a__plus(mark(X1), mark(X2))] 785.76/297.06 785.76/297.06 785.76/297.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 785.76/297.06 785.76/297.06 We are left with following problem, upon which TcT provides the 785.76/297.06 certificate MAYBE. 785.76/297.06 785.76/297.06 Strict Trs: 785.76/297.06 { a__plus(N, s(M)) -> a__U11(tt(), M, N) 785.76/297.06 , mark(tt()) -> tt() 785.76/297.06 , mark(s(X)) -> s(mark(X)) 785.76/297.06 , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3) 785.76/297.06 , mark(U12(X1, X2, X3)) -> a__U12(mark(X1), X2, X3) 785.76/297.06 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) } 785.76/297.06 Weak Trs: 785.76/297.06 { a__U11(X1, X2, X3) -> U11(X1, X2, X3) 785.76/297.06 , a__U11(tt(), M, N) -> a__U12(tt(), M, N) 785.76/297.06 , a__U12(X1, X2, X3) -> U12(X1, X2, X3) 785.76/297.06 , a__U12(tt(), M, N) -> s(a__plus(mark(N), mark(M))) 785.76/297.06 , a__plus(X1, X2) -> plus(X1, X2) 785.76/297.06 , a__plus(N, 0()) -> mark(N) 785.76/297.06 , mark(0()) -> 0() } 785.76/297.06 Obligation: 785.76/297.06 innermost runtime complexity 785.76/297.06 Answer: 785.76/297.06 MAYBE 785.76/297.06 785.76/297.06 The weightgap principle applies (using the following nonconstant 785.76/297.06 growth matrix-interpretation) 785.76/297.06 785.76/297.06 The following argument positions are usable: 785.76/297.06 Uargs(a__U11) = {1}, Uargs(a__U12) = {1}, Uargs(s) = {1}, 785.76/297.06 Uargs(a__plus) = {1, 2} 785.76/297.06 785.76/297.06 TcT has computed the following matrix interpretation satisfying 785.76/297.06 not(EDA) and not(IDA(1)). 785.76/297.06 785.76/297.06 [a__U11](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 785.76/297.06 785.76/297.06 [tt] = [3] 785.76/297.06 785.76/297.06 [a__U12](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 785.76/297.06 785.76/297.06 [s](x1) = [1] x1 + [0] 785.76/297.06 785.76/297.06 [a__plus](x1, x2) = [1] x1 + [1] x2 + [0] 785.76/297.06 785.76/297.06 [mark](x1) = [1] x1 + [1] 785.76/297.06 785.76/297.06 [0] = [4] 785.76/297.06 785.76/297.06 [U11](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 785.76/297.06 785.76/297.06 [U12](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] 785.76/297.06 785.76/297.06 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 785.76/297.06 785.76/297.06 The order satisfies the following ordering constraints: 785.76/297.06 785.76/297.06 [a__U11(X1, X2, X3)] = [1] X1 + [1] X2 + [1] X3 + [0] 785.76/297.06 >= [1] X1 + [1] X2 + [1] X3 + [0] 785.76/297.06 = [U11(X1, X2, X3)] 785.76/297.06 785.76/297.06 [a__U11(tt(), M, N)] = [1] M + [1] N + [3] 785.76/297.06 >= [1] M + [1] N + [3] 785.76/297.06 = [a__U12(tt(), M, N)] 785.76/297.06 785.76/297.06 [a__U12(X1, X2, X3)] = [1] X1 + [1] X2 + [1] X3 + [0] 785.76/297.06 >= [1] X1 + [1] X2 + [1] X3 + [0] 785.76/297.06 = [U12(X1, X2, X3)] 785.76/297.06 785.76/297.06 [a__U12(tt(), M, N)] = [1] M + [1] N + [3] 785.76/297.06 > [1] M + [1] N + [2] 785.76/297.06 = [s(a__plus(mark(N), mark(M)))] 785.76/297.06 785.76/297.06 [a__plus(X1, X2)] = [1] X1 + [1] X2 + [0] 785.76/297.06 >= [1] X1 + [1] X2 + [0] 785.76/297.06 = [plus(X1, X2)] 785.76/297.06 785.76/297.06 [a__plus(N, s(M))] = [1] M + [1] N + [0] 785.76/297.06 ? [1] M + [1] N + [3] 785.76/297.06 = [a__U11(tt(), M, N)] 785.76/297.06 785.76/297.06 [a__plus(N, 0())] = [1] N + [4] 785.76/297.06 > [1] N + [1] 785.76/297.06 = [mark(N)] 785.76/297.06 785.76/297.06 [mark(tt())] = [4] 785.76/297.06 > [3] 785.76/297.06 = [tt()] 785.76/297.06 785.76/297.06 [mark(s(X))] = [1] X + [1] 785.76/297.06 >= [1] X + [1] 785.76/297.06 = [s(mark(X))] 785.76/297.06 785.76/297.06 [mark(0())] = [5] 785.76/297.06 > [4] 785.76/297.06 = [0()] 785.76/297.06 785.76/297.06 [mark(U11(X1, X2, X3))] = [1] X1 + [1] X2 + [1] X3 + [1] 785.76/297.06 >= [1] X1 + [1] X2 + [1] X3 + [1] 785.76/297.06 = [a__U11(mark(X1), X2, X3)] 785.76/297.06 785.76/297.06 [mark(U12(X1, X2, X3))] = [1] X1 + [1] X2 + [1] X3 + [1] 785.76/297.06 >= [1] X1 + [1] X2 + [1] X3 + [1] 785.76/297.06 = [a__U12(mark(X1), X2, X3)] 785.76/297.06 785.76/297.06 [mark(plus(X1, X2))] = [1] X1 + [1] X2 + [1] 785.76/297.06 ? [1] X1 + [1] X2 + [2] 785.76/297.06 = [a__plus(mark(X1), mark(X2))] 785.76/297.06 785.76/297.06 785.76/297.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 785.76/297.06 785.76/297.06 We are left with following problem, upon which TcT provides the 785.76/297.06 certificate MAYBE. 785.76/297.06 785.76/297.06 Strict Trs: 785.76/297.06 { a__plus(N, s(M)) -> a__U11(tt(), M, N) 785.76/297.06 , mark(s(X)) -> s(mark(X)) 785.76/297.06 , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3) 785.76/297.06 , mark(U12(X1, X2, X3)) -> a__U12(mark(X1), X2, X3) 785.76/297.06 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) } 785.76/297.06 Weak Trs: 785.76/297.06 { a__U11(X1, X2, X3) -> U11(X1, X2, X3) 785.76/297.06 , a__U11(tt(), M, N) -> a__U12(tt(), M, N) 785.76/297.06 , a__U12(X1, X2, X3) -> U12(X1, X2, X3) 785.76/297.06 , a__U12(tt(), M, N) -> s(a__plus(mark(N), mark(M))) 785.76/297.06 , a__plus(X1, X2) -> plus(X1, X2) 785.76/297.06 , a__plus(N, 0()) -> mark(N) 785.76/297.06 , mark(tt()) -> tt() 785.76/297.06 , mark(0()) -> 0() } 785.76/297.06 Obligation: 785.76/297.06 innermost runtime complexity 785.76/297.06 Answer: 785.76/297.06 MAYBE 785.76/297.06 785.76/297.06 None of the processors succeeded. 785.76/297.06 785.76/297.06 Details of failed attempt(s): 785.76/297.06 ----------------------------- 785.76/297.06 1) 'empty' failed due to the following reason: 785.76/297.06 785.76/297.06 Empty strict component of the problem is NOT empty. 785.76/297.06 785.76/297.06 2) 'With Problem ...' failed due to the following reason: 785.76/297.06 785.76/297.06 None of the processors succeeded. 785.76/297.06 785.76/297.06 Details of failed attempt(s): 785.76/297.06 ----------------------------- 785.76/297.06 1) 'empty' failed due to the following reason: 785.76/297.06 785.76/297.06 Empty strict component of the problem is NOT empty. 785.76/297.06 785.76/297.06 2) 'Fastest' failed due to the following reason: 785.76/297.06 785.76/297.06 None of the processors succeeded. 785.76/297.06 785.76/297.06 Details of failed attempt(s): 785.76/297.06 ----------------------------- 785.76/297.06 1) 'With Problem ...' failed due to the following reason: 785.76/297.06 785.76/297.06 None of the processors succeeded. 785.76/297.06 785.76/297.06 Details of failed attempt(s): 785.76/297.06 ----------------------------- 785.76/297.06 1) 'empty' failed due to the following reason: 785.76/297.06 785.76/297.06 Empty strict component of the problem is NOT empty. 785.76/297.06 785.76/297.06 2) 'With Problem ...' failed due to the following reason: 785.76/297.06 785.76/297.06 The weightgap principle applies (using the following nonconstant 785.76/297.06 growth matrix-interpretation) 785.76/297.06 785.76/297.06 The following argument positions are usable: 785.76/297.06 Uargs(a__U11) = {1}, Uargs(a__U12) = {1}, Uargs(s) = {1}, 785.76/297.06 Uargs(a__plus) = {1, 2} 785.76/297.06 785.76/297.06 TcT has computed the following matrix interpretation satisfying 785.76/297.06 not(EDA) and not(IDA(1)). 785.76/297.06 785.76/297.06 [a__U11](x1, x2, x3) = [1 0] x1 + [0] 785.76/297.06 [0 0] [4] 785.76/297.06 785.76/297.06 [tt] = [0] 785.76/297.06 [0] 785.76/297.06 785.76/297.06 [a__U12](x1, x2, x3) = [1 0] x1 + [0] 785.76/297.06 [0 0] [4] 785.76/297.06 785.76/297.06 [s](x1) = [1 0] x1 + [0] 785.76/297.06 [0 0] [2] 785.76/297.06 785.76/297.06 [a__plus](x1, x2) = [1 0] x1 + [1 2] x2 + [0] 785.76/297.06 [0 0] [0 0] [4] 785.76/297.06 785.76/297.06 [mark](x1) = [0] 785.76/297.06 [0] 785.76/297.06 785.76/297.06 [0] = [0] 785.76/297.06 [0] 785.76/297.06 785.76/297.06 [U11](x1, x2, x3) = [0] 785.76/297.06 [0] 785.76/297.06 785.76/297.06 [U12](x1, x2, x3) = [0] 785.76/297.06 [0] 785.76/297.06 785.76/297.06 [plus](x1, x2) = [0] 785.76/297.06 [0] 785.76/297.06 785.76/297.06 The order satisfies the following ordering constraints: 785.76/297.06 785.76/297.06 [a__U11(X1, X2, X3)] = [1 0] X1 + [0] 785.76/297.06 [0 0] [4] 785.76/297.06 >= [0] 785.76/297.06 [0] 785.76/297.06 = [U11(X1, X2, X3)] 785.76/297.06 785.76/297.06 [a__U11(tt(), M, N)] = [0] 785.76/297.06 [4] 785.76/297.06 >= [0] 785.76/297.06 [4] 785.76/297.06 = [a__U12(tt(), M, N)] 785.76/297.06 785.76/297.06 [a__U12(X1, X2, X3)] = [1 0] X1 + [0] 785.76/297.06 [0 0] [4] 785.76/297.06 >= [0] 785.76/297.06 [0] 785.76/297.06 = [U12(X1, X2, X3)] 785.76/297.06 785.76/297.06 [a__U12(tt(), M, N)] = [0] 785.76/297.06 [4] 785.76/297.06 >= [0] 785.76/297.06 [2] 785.76/297.06 = [s(a__plus(mark(N), mark(M)))] 785.76/297.06 785.76/297.06 [a__plus(X1, X2)] = [1 0] X1 + [1 2] X2 + [0] 785.76/297.06 [0 0] [0 0] [4] 785.76/297.06 >= [0] 785.76/297.06 [0] 785.76/297.06 = [plus(X1, X2)] 785.76/297.06 785.76/297.06 [a__plus(N, s(M))] = [1 0] M + [1 0] N + [4] 785.76/297.06 [0 0] [0 0] [4] 785.76/297.06 > [0] 785.76/297.06 [4] 785.76/297.06 = [a__U11(tt(), M, N)] 785.76/297.06 785.76/297.06 [a__plus(N, 0())] = [1 0] N + [0] 785.76/297.06 [0 0] [4] 785.76/297.06 >= [0] 785.76/297.06 [0] 785.76/297.06 = [mark(N)] 785.76/297.06 785.76/297.06 [mark(tt())] = [0] 785.76/297.06 [0] 785.76/297.06 >= [0] 785.76/297.06 [0] 785.76/297.06 = [tt()] 785.76/297.06 785.76/297.06 [mark(s(X))] = [0] 785.76/297.06 [0] 785.76/297.06 ? [0] 785.76/297.06 [2] 785.76/297.06 = [s(mark(X))] 785.76/297.06 785.76/297.06 [mark(0())] = [0] 785.76/297.06 [0] 785.76/297.06 >= [0] 785.76/297.06 [0] 785.76/297.06 = [0()] 785.76/297.06 785.76/297.06 [mark(U11(X1, X2, X3))] = [0] 785.76/297.06 [0] 785.76/297.06 ? [0] 785.76/297.06 [4] 785.76/297.06 = [a__U11(mark(X1), X2, X3)] 785.76/297.06 785.76/297.06 [mark(U12(X1, X2, X3))] = [0] 785.76/297.06 [0] 785.76/297.06 ? [0] 785.76/297.06 [4] 785.76/297.06 = [a__U12(mark(X1), X2, X3)] 785.76/297.06 785.76/297.06 [mark(plus(X1, X2))] = [0] 785.76/297.06 [0] 785.76/297.06 ? [0] 785.76/297.06 [4] 785.76/297.06 = [a__plus(mark(X1), mark(X2))] 785.76/297.06 785.76/297.06 785.76/297.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 785.76/297.06 785.76/297.06 We are left with following problem, upon which TcT provides the 785.76/297.06 certificate MAYBE. 785.76/297.06 785.76/297.06 Strict Trs: 785.76/297.06 { mark(s(X)) -> s(mark(X)) 785.76/297.06 , mark(U11(X1, X2, X3)) -> a__U11(mark(X1), X2, X3) 785.76/297.06 , mark(U12(X1, X2, X3)) -> a__U12(mark(X1), X2, X3) 785.76/297.06 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) } 785.76/297.06 Weak Trs: 785.76/297.06 { a__U11(X1, X2, X3) -> U11(X1, X2, X3) 785.76/297.06 , a__U11(tt(), M, N) -> a__U12(tt(), M, N) 785.76/297.06 , a__U12(X1, X2, X3) -> U12(X1, X2, X3) 785.76/297.06 , a__U12(tt(), M, N) -> s(a__plus(mark(N), mark(M))) 785.76/297.06 , a__plus(X1, X2) -> plus(X1, X2) 785.76/297.06 , a__plus(N, s(M)) -> a__U11(tt(), M, N) 785.76/297.06 , a__plus(N, 0()) -> mark(N) 785.76/297.06 , mark(tt()) -> tt() 785.76/297.06 , mark(0()) -> 0() } 785.76/297.06 Obligation: 785.76/297.06 innermost runtime complexity 785.76/297.06 Answer: 785.76/297.06 MAYBE 785.76/297.06 785.76/297.06 None of the processors succeeded. 785.76/297.06 785.76/297.06 Details of failed attempt(s): 785.76/297.06 ----------------------------- 785.76/297.06 1) 'empty' failed due to the following reason: 785.76/297.06 785.76/297.06 Empty strict component of the problem is NOT empty. 785.76/297.06 785.76/297.06 2) 'With Problem ...' failed due to the following reason: 785.76/297.06 785.76/297.06 None of the processors succeeded. 785.76/297.06 785.76/297.06 Details of failed attempt(s): 785.76/297.06 ----------------------------- 785.76/297.06 1) 'empty' failed due to the following reason: 785.76/297.06 785.76/297.06 Empty strict component of the problem is NOT empty. 785.76/297.06 785.76/297.06 2) 'With Problem ...' failed due to the following reason: 785.76/297.06 785.76/297.06 Empty strict component of the problem is NOT empty. 785.76/297.06 785.76/297.06 785.76/297.06 785.76/297.06 785.76/297.06 2) 'With Problem ...' failed due to the following reason: 785.76/297.06 785.76/297.06 None of the processors succeeded. 785.76/297.06 785.76/297.06 Details of failed attempt(s): 785.76/297.06 ----------------------------- 785.76/297.06 1) 'empty' failed due to the following reason: 785.76/297.06 785.76/297.06 Empty strict component of the problem is NOT empty. 785.76/297.06 785.76/297.06 2) 'With Problem ...' failed due to the following reason: 785.76/297.06 785.76/297.06 Empty strict component of the problem is NOT empty. 785.76/297.06 785.76/297.06 785.76/297.06 785.76/297.06 785.76/297.06 785.76/297.06 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 785.76/297.06 failed due to the following reason: 785.76/297.06 785.76/297.06 Computation stopped due to timeout after 24.0 seconds. 785.76/297.06 785.76/297.06 3) 'Best' failed due to the following reason: 785.76/297.06 785.76/297.06 None of the processors succeeded. 785.76/297.06 785.76/297.06 Details of failed attempt(s): 785.76/297.06 ----------------------------- 785.76/297.06 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 785.76/297.06 to the following reason: 785.76/297.06 785.76/297.06 The input cannot be shown compatible 785.76/297.06 785.76/297.06 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 785.76/297.06 following reason: 785.76/297.06 785.76/297.06 The input cannot be shown compatible 785.76/297.06 785.76/297.06 785.76/297.06 785.76/297.06 785.76/297.06 785.76/297.06 Arrrr.. 786.30/297.58 EOF