MAYBE 860.26/297.56 MAYBE 860.26/297.56 860.26/297.56 We are left with following problem, upon which TcT provides the 860.26/297.56 certificate MAYBE. 860.26/297.56 860.26/297.56 Strict Trs: 860.26/297.56 { a__and(X1, X2) -> and(X1, X2) 860.26/297.56 , a__and(tt(), X) -> mark(X) 860.26/297.56 , mark(tt()) -> tt() 860.26/297.56 , mark(0()) -> 0() 860.26/297.56 , mark(s(X)) -> s(mark(X)) 860.26/297.56 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 860.26/297.56 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) 860.26/297.56 , a__plus(X1, X2) -> plus(X1, X2) 860.26/297.56 , a__plus(N, 0()) -> mark(N) 860.26/297.56 , a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) } 860.26/297.56 Obligation: 860.26/297.56 runtime complexity 860.26/297.56 Answer: 860.26/297.56 MAYBE 860.26/297.56 860.26/297.56 The input is overlay and right-linear. Switching to innermost 860.26/297.56 rewriting. 860.26/297.56 860.26/297.56 We are left with following problem, upon which TcT provides the 860.26/297.56 certificate MAYBE. 860.26/297.56 860.26/297.56 Strict Trs: 860.26/297.56 { a__and(X1, X2) -> and(X1, X2) 860.26/297.56 , a__and(tt(), X) -> mark(X) 860.26/297.56 , mark(tt()) -> tt() 860.26/297.56 , mark(0()) -> 0() 860.26/297.56 , mark(s(X)) -> s(mark(X)) 860.26/297.56 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 860.26/297.56 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) 860.26/297.56 , a__plus(X1, X2) -> plus(X1, X2) 860.26/297.56 , a__plus(N, 0()) -> mark(N) 860.26/297.56 , a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) } 860.26/297.56 Obligation: 860.26/297.56 innermost runtime complexity 860.26/297.56 Answer: 860.26/297.56 MAYBE 860.26/297.56 860.26/297.56 None of the processors succeeded. 860.26/297.56 860.26/297.56 Details of failed attempt(s): 860.26/297.56 ----------------------------- 860.26/297.56 1) 'empty' failed due to the following reason: 860.26/297.56 860.26/297.56 Empty strict component of the problem is NOT empty. 860.26/297.56 860.26/297.56 2) 'Best' failed due to the following reason: 860.26/297.56 860.26/297.56 None of the processors succeeded. 860.26/297.56 860.26/297.56 Details of failed attempt(s): 860.26/297.56 ----------------------------- 860.26/297.56 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 860.26/297.56 following reason: 860.26/297.56 860.26/297.56 Computation stopped due to timeout after 297.0 seconds. 860.26/297.56 860.26/297.56 2) 'Best' failed due to the following reason: 860.26/297.56 860.26/297.56 None of the processors succeeded. 860.26/297.56 860.26/297.56 Details of failed attempt(s): 860.26/297.56 ----------------------------- 860.26/297.56 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 860.26/297.56 seconds)' failed due to the following reason: 860.26/297.56 860.26/297.56 We use the processor 'matrix interpretation of dimension 1' to 860.26/297.56 orient following rules strictly. 860.26/297.56 860.26/297.56 Trs: { a__plus(N, 0()) -> mark(N) } 860.26/297.56 860.26/297.56 The induced complexity on above rules (modulo remaining rules) is 860.26/297.56 YES(?,O(n^1)) . These rules are moved into the corresponding weak 860.26/297.56 component(s). 860.26/297.56 860.26/297.56 Sub-proof: 860.26/297.56 ---------- 860.26/297.56 The following argument positions are usable: 860.26/297.56 Uargs(a__and) = {1}, Uargs(a__plus) = {1, 2}, Uargs(s) = {1} 860.26/297.56 860.26/297.56 TcT has computed the following constructor-based matrix 860.26/297.56 interpretation satisfying not(EDA). 860.26/297.56 860.26/297.56 [a__and](x1, x2) = [1] x1 + [1] x2 + [0] 860.26/297.56 860.26/297.56 [tt] = [0] 860.26/297.56 860.26/297.56 [mark](x1) = [1] x1 + [0] 860.26/297.56 860.26/297.56 [a__plus](x1, x2) = [1] x1 + [1] x2 + [0] 860.26/297.56 860.26/297.56 [0] = [4] 860.26/297.56 860.26/297.56 [s](x1) = [1] x1 + [0] 860.26/297.56 860.26/297.56 [and](x1, x2) = [1] x1 + [1] x2 + [0] 860.26/297.56 860.26/297.56 [plus](x1, x2) = [1] x1 + [1] x2 + [0] 860.26/297.56 860.26/297.56 The order satisfies the following ordering constraints: 860.26/297.56 860.26/297.56 [a__and(X1, X2)] = [1] X1 + [1] X2 + [0] 860.26/297.56 >= [1] X1 + [1] X2 + [0] 860.26/297.56 = [and(X1, X2)] 860.26/297.56 860.26/297.56 [a__and(tt(), X)] = [1] X + [0] 860.26/297.56 >= [1] X + [0] 860.26/297.56 = [mark(X)] 860.26/297.56 860.26/297.56 [mark(tt())] = [0] 860.26/297.56 >= [0] 860.26/297.56 = [tt()] 860.26/297.56 860.26/297.56 [mark(0())] = [4] 860.26/297.56 >= [4] 860.26/297.56 = [0()] 860.26/297.56 860.26/297.56 [mark(s(X))] = [1] X + [0] 860.26/297.56 >= [1] X + [0] 860.26/297.56 = [s(mark(X))] 860.26/297.56 860.26/297.56 [mark(and(X1, X2))] = [1] X1 + [1] X2 + [0] 860.26/297.56 >= [1] X1 + [1] X2 + [0] 860.26/297.56 = [a__and(mark(X1), X2)] 860.26/297.56 860.26/297.56 [mark(plus(X1, X2))] = [1] X1 + [1] X2 + [0] 860.26/297.56 >= [1] X1 + [1] X2 + [0] 860.26/297.56 = [a__plus(mark(X1), mark(X2))] 860.26/297.56 860.26/297.56 [a__plus(X1, X2)] = [1] X1 + [1] X2 + [0] 860.26/297.56 >= [1] X1 + [1] X2 + [0] 860.26/297.56 = [plus(X1, X2)] 860.26/297.56 860.26/297.56 [a__plus(N, 0())] = [1] N + [4] 860.26/297.56 > [1] N + [0] 860.26/297.56 = [mark(N)] 860.26/297.56 860.26/297.56 [a__plus(N, s(M))] = [1] N + [1] M + [0] 860.26/297.56 >= [1] N + [1] M + [0] 860.26/297.56 = [s(a__plus(mark(N), mark(M)))] 860.26/297.56 860.26/297.56 860.26/297.56 We return to the main proof. 860.26/297.56 860.26/297.56 We are left with following problem, upon which TcT provides the 860.26/297.56 certificate MAYBE. 860.26/297.56 860.26/297.56 Strict Trs: 860.26/297.56 { a__and(X1, X2) -> and(X1, X2) 860.26/297.56 , a__and(tt(), X) -> mark(X) 860.26/297.56 , mark(tt()) -> tt() 860.26/297.56 , mark(0()) -> 0() 860.26/297.56 , mark(s(X)) -> s(mark(X)) 860.26/297.56 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 860.26/297.56 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) 860.26/297.56 , a__plus(X1, X2) -> plus(X1, X2) 860.26/297.56 , a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) } 860.26/297.56 Weak Trs: { a__plus(N, 0()) -> mark(N) } 860.26/297.56 Obligation: 860.26/297.56 innermost runtime complexity 860.26/297.56 Answer: 860.26/297.56 MAYBE 860.26/297.56 860.26/297.56 The weightgap principle applies (using the following nonconstant 860.26/297.56 growth matrix-interpretation) 860.26/297.56 860.26/297.56 The following argument positions are usable: 860.26/297.56 Uargs(a__and) = {1}, Uargs(a__plus) = {1, 2}, Uargs(s) = {1} 860.26/297.56 860.26/297.56 TcT has computed the following matrix interpretation satisfying 860.26/297.56 not(EDA) and not(IDA(1)). 860.26/297.56 860.26/297.56 [a__and](x1, x2) = [1] x1 + [1] 860.26/297.56 860.26/297.56 [tt] = [0] 860.26/297.56 860.26/297.56 [mark](x1) = [0] 860.26/297.56 860.26/297.56 [a__plus](x1, x2) = [1] x1 + [1] x2 + [0] 860.26/297.56 860.26/297.56 [0] = [4] 860.26/297.56 860.26/297.56 [s](x1) = [1] x1 + [0] 860.26/297.56 860.26/297.56 [and](x1, x2) = [1] x1 + [0] 860.26/297.56 860.26/297.56 [plus](x1, x2) = [1] x1 + [1] x2 + [7] 860.26/297.56 860.26/297.56 The order satisfies the following ordering constraints: 860.26/297.56 860.26/297.56 [a__and(X1, X2)] = [1] X1 + [1] 860.26/297.56 > [1] X1 + [0] 860.26/297.56 = [and(X1, X2)] 860.26/297.56 860.26/297.56 [a__and(tt(), X)] = [1] 860.26/297.56 > [0] 860.26/297.56 = [mark(X)] 860.26/297.56 860.26/297.56 [mark(tt())] = [0] 860.26/297.56 >= [0] 860.26/297.56 = [tt()] 860.26/297.56 860.26/297.56 [mark(0())] = [0] 860.26/297.56 ? [4] 860.26/297.56 = [0()] 860.26/297.56 860.26/297.56 [mark(s(X))] = [0] 860.26/297.56 >= [0] 860.26/297.56 = [s(mark(X))] 860.26/297.56 860.26/297.56 [mark(and(X1, X2))] = [0] 860.26/297.56 ? [1] 860.26/297.56 = [a__and(mark(X1), X2)] 860.26/297.56 860.26/297.56 [mark(plus(X1, X2))] = [0] 860.26/297.56 >= [0] 860.26/297.56 = [a__plus(mark(X1), mark(X2))] 860.26/297.56 860.26/297.56 [a__plus(X1, X2)] = [1] X1 + [1] X2 + [0] 860.26/297.56 ? [1] X1 + [1] X2 + [7] 860.26/297.56 = [plus(X1, X2)] 860.26/297.56 860.26/297.56 [a__plus(N, 0())] = [1] N + [4] 860.26/297.56 > [0] 860.26/297.56 = [mark(N)] 860.26/297.56 860.26/297.56 [a__plus(N, s(M))] = [1] N + [1] M + [0] 860.26/297.56 >= [0] 860.26/297.56 = [s(a__plus(mark(N), mark(M)))] 860.26/297.56 860.26/297.56 860.26/297.56 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 860.26/297.56 860.26/297.56 We are left with following problem, upon which TcT provides the 860.26/297.56 certificate MAYBE. 860.26/297.56 860.26/297.56 Strict Trs: 860.26/297.56 { mark(tt()) -> tt() 860.26/297.56 , mark(0()) -> 0() 860.26/297.56 , mark(s(X)) -> s(mark(X)) 860.26/297.56 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 860.26/297.56 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) 860.26/297.56 , a__plus(X1, X2) -> plus(X1, X2) 860.26/297.56 , a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) } 860.26/297.56 Weak Trs: 860.26/297.56 { a__and(X1, X2) -> and(X1, X2) 860.26/297.56 , a__and(tt(), X) -> mark(X) 860.26/297.56 , a__plus(N, 0()) -> mark(N) } 860.26/297.56 Obligation: 860.26/297.56 innermost runtime complexity 860.26/297.56 Answer: 860.26/297.56 MAYBE 860.26/297.56 860.26/297.56 The weightgap principle applies (using the following nonconstant 860.26/297.56 growth matrix-interpretation) 860.26/297.56 860.26/297.56 The following argument positions are usable: 860.26/297.56 Uargs(a__and) = {1}, Uargs(a__plus) = {1, 2}, Uargs(s) = {1} 860.26/297.56 860.26/297.56 TcT has computed the following matrix interpretation satisfying 860.26/297.56 not(EDA) and not(IDA(1)). 860.26/297.56 860.26/297.56 [a__and](x1, x2) = [1] x1 + [1] x2 + [4] 860.26/297.56 860.26/297.56 [tt] = [4] 860.26/297.56 860.26/297.56 [mark](x1) = [1] x1 + [0] 860.26/297.56 860.26/297.56 [a__plus](x1, x2) = [1] x1 + [1] x2 + [0] 860.26/297.56 860.26/297.56 [0] = [4] 860.26/297.56 860.26/297.56 [s](x1) = [1] x1 + [0] 860.26/297.56 860.26/297.56 [and](x1, x2) = [1] x1 + [1] x2 + [0] 860.26/297.56 860.26/297.56 [plus](x1, x2) = [1] x1 + [1] x2 + [1] 860.26/297.56 860.26/297.56 The order satisfies the following ordering constraints: 860.26/297.56 860.26/297.56 [a__and(X1, X2)] = [1] X1 + [1] X2 + [4] 860.26/297.56 > [1] X1 + [1] X2 + [0] 860.26/297.56 = [and(X1, X2)] 860.26/297.56 860.26/297.56 [a__and(tt(), X)] = [1] X + [8] 860.26/297.56 > [1] X + [0] 860.26/297.56 = [mark(X)] 860.26/297.56 860.26/297.56 [mark(tt())] = [4] 860.26/297.56 >= [4] 860.26/297.56 = [tt()] 860.26/297.56 860.26/297.56 [mark(0())] = [4] 860.26/297.56 >= [4] 860.26/297.56 = [0()] 860.26/297.56 860.26/297.56 [mark(s(X))] = [1] X + [0] 860.26/297.56 >= [1] X + [0] 860.26/297.56 = [s(mark(X))] 860.26/297.56 860.26/297.56 [mark(and(X1, X2))] = [1] X1 + [1] X2 + [0] 860.26/297.56 ? [1] X1 + [1] X2 + [4] 860.26/297.56 = [a__and(mark(X1), X2)] 860.26/297.56 860.26/297.56 [mark(plus(X1, X2))] = [1] X1 + [1] X2 + [1] 860.26/297.56 > [1] X1 + [1] X2 + [0] 860.26/297.56 = [a__plus(mark(X1), mark(X2))] 860.26/297.56 860.26/297.56 [a__plus(X1, X2)] = [1] X1 + [1] X2 + [0] 860.26/297.56 ? [1] X1 + [1] X2 + [1] 860.26/297.56 = [plus(X1, X2)] 860.26/297.56 860.26/297.56 [a__plus(N, 0())] = [1] N + [4] 860.26/297.56 > [1] N + [0] 860.26/297.56 = [mark(N)] 860.26/297.56 860.26/297.56 [a__plus(N, s(M))] = [1] N + [1] M + [0] 860.26/297.56 >= [1] N + [1] M + [0] 860.26/297.56 = [s(a__plus(mark(N), mark(M)))] 860.26/297.56 860.26/297.56 860.26/297.56 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 860.26/297.56 860.26/297.56 We are left with following problem, upon which TcT provides the 860.26/297.56 certificate MAYBE. 860.26/297.56 860.26/297.56 Strict Trs: 860.26/297.56 { mark(tt()) -> tt() 860.26/297.56 , mark(0()) -> 0() 860.26/297.56 , mark(s(X)) -> s(mark(X)) 860.26/297.56 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 860.26/297.56 , a__plus(X1, X2) -> plus(X1, X2) 860.26/297.56 , a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) } 860.26/297.56 Weak Trs: 860.26/297.56 { a__and(X1, X2) -> and(X1, X2) 860.26/297.56 , a__and(tt(), X) -> mark(X) 860.26/297.56 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) 860.26/297.56 , a__plus(N, 0()) -> mark(N) } 860.26/297.56 Obligation: 860.26/297.56 innermost runtime complexity 860.26/297.56 Answer: 860.26/297.56 MAYBE 860.26/297.56 860.26/297.56 The weightgap principle applies (using the following nonconstant 860.26/297.56 growth matrix-interpretation) 860.26/297.56 860.26/297.56 The following argument positions are usable: 860.26/297.56 Uargs(a__and) = {1}, Uargs(a__plus) = {1, 2}, Uargs(s) = {1} 860.26/297.56 860.26/297.56 TcT has computed the following matrix interpretation satisfying 860.26/297.56 not(EDA) and not(IDA(1)). 860.26/297.56 860.26/297.56 [a__and](x1, x2) = [1] x1 + [1] x2 + [7] 860.26/297.56 860.26/297.56 [tt] = [4] 860.26/297.56 860.26/297.56 [mark](x1) = [1] x1 + [1] 860.26/297.56 860.26/297.56 [a__plus](x1, x2) = [1] x1 + [1] x2 + [0] 860.26/297.56 860.26/297.56 [0] = [4] 860.26/297.56 860.26/297.56 [s](x1) = [1] x1 + [0] 860.26/297.56 860.26/297.56 [and](x1, x2) = [1] x1 + [1] x2 + [0] 860.26/297.56 860.26/297.56 [plus](x1, x2) = [1] x1 + [1] x2 + [2] 860.26/297.56 860.26/297.56 The order satisfies the following ordering constraints: 860.26/297.56 860.26/297.56 [a__and(X1, X2)] = [1] X1 + [1] X2 + [7] 860.26/297.56 > [1] X1 + [1] X2 + [0] 860.26/297.56 = [and(X1, X2)] 860.26/297.56 860.26/297.56 [a__and(tt(), X)] = [1] X + [11] 860.26/297.56 > [1] X + [1] 860.26/297.56 = [mark(X)] 860.26/297.56 860.26/297.56 [mark(tt())] = [5] 860.26/297.56 > [4] 860.26/297.56 = [tt()] 860.26/297.56 860.26/297.56 [mark(0())] = [5] 860.26/297.56 > [4] 860.26/297.56 = [0()] 860.26/297.56 860.26/297.56 [mark(s(X))] = [1] X + [1] 860.26/297.56 >= [1] X + [1] 860.26/297.56 = [s(mark(X))] 860.26/297.56 860.26/297.56 [mark(and(X1, X2))] = [1] X1 + [1] X2 + [1] 860.26/297.56 ? [1] X1 + [1] X2 + [8] 860.26/297.56 = [a__and(mark(X1), X2)] 860.26/297.56 860.26/297.56 [mark(plus(X1, X2))] = [1] X1 + [1] X2 + [3] 860.26/297.56 > [1] X1 + [1] X2 + [2] 860.26/297.56 = [a__plus(mark(X1), mark(X2))] 860.26/297.56 860.26/297.56 [a__plus(X1, X2)] = [1] X1 + [1] X2 + [0] 860.26/297.56 ? [1] X1 + [1] X2 + [2] 860.26/297.56 = [plus(X1, X2)] 860.26/297.56 860.26/297.56 [a__plus(N, 0())] = [1] N + [4] 860.26/297.56 > [1] N + [1] 860.26/297.56 = [mark(N)] 860.26/297.56 860.26/297.56 [a__plus(N, s(M))] = [1] N + [1] M + [0] 860.26/297.56 ? [1] N + [1] M + [2] 860.26/297.56 = [s(a__plus(mark(N), mark(M)))] 860.26/297.56 860.26/297.56 860.26/297.56 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 860.26/297.56 860.26/297.56 We are left with following problem, upon which TcT provides the 860.26/297.56 certificate MAYBE. 860.26/297.56 860.26/297.56 Strict Trs: 860.26/297.56 { mark(s(X)) -> s(mark(X)) 860.26/297.56 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 860.26/297.56 , a__plus(X1, X2) -> plus(X1, X2) 860.26/297.56 , a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) } 860.26/297.56 Weak Trs: 860.26/297.56 { a__and(X1, X2) -> and(X1, X2) 860.26/297.56 , a__and(tt(), X) -> mark(X) 860.26/297.56 , mark(tt()) -> tt() 860.26/297.56 , mark(0()) -> 0() 860.26/297.56 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) 860.26/297.56 , a__plus(N, 0()) -> mark(N) } 860.26/297.56 Obligation: 860.26/297.56 innermost runtime complexity 860.26/297.56 Answer: 860.26/297.56 MAYBE 860.26/297.56 860.26/297.56 None of the processors succeeded. 860.26/297.56 860.26/297.56 Details of failed attempt(s): 860.26/297.56 ----------------------------- 860.26/297.56 1) 'empty' failed due to the following reason: 860.26/297.56 860.26/297.56 Empty strict component of the problem is NOT empty. 860.26/297.56 860.26/297.56 2) 'With Problem ...' failed due to the following reason: 860.26/297.56 860.26/297.56 None of the processors succeeded. 860.26/297.56 860.26/297.56 Details of failed attempt(s): 860.26/297.56 ----------------------------- 860.26/297.56 1) 'empty' failed due to the following reason: 860.26/297.56 860.26/297.56 Empty strict component of the problem is NOT empty. 860.26/297.56 860.26/297.56 2) 'Fastest' failed due to the following reason: 860.26/297.56 860.26/297.56 None of the processors succeeded. 860.26/297.56 860.26/297.56 Details of failed attempt(s): 860.26/297.56 ----------------------------- 860.26/297.56 1) 'With Problem ...' failed due to the following reason: 860.26/297.56 860.26/297.56 None of the processors succeeded. 860.26/297.56 860.26/297.56 Details of failed attempt(s): 860.26/297.56 ----------------------------- 860.26/297.56 1) 'empty' failed due to the following reason: 860.26/297.56 860.26/297.56 Empty strict component of the problem is NOT empty. 860.26/297.56 860.26/297.56 2) 'With Problem ...' failed due to the following reason: 860.26/297.56 860.26/297.56 We use the processor 'matrix interpretation of dimension 2' to 860.26/297.56 orient following rules strictly. 860.26/297.56 860.26/297.56 Trs: { a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) } 860.26/297.56 860.26/297.56 The induced complexity on above rules (modulo remaining rules) is 860.26/297.56 YES(?,O(n^2)) . These rules are moved into the corresponding weak 860.26/297.56 component(s). 860.26/297.56 860.26/297.56 Sub-proof: 860.26/297.56 ---------- 860.26/297.56 The following argument positions are usable: 860.26/297.56 Uargs(a__and) = {1}, Uargs(a__plus) = {1, 2}, Uargs(s) = {1} 860.26/297.56 860.26/297.56 TcT has computed the following constructor-based matrix 860.26/297.56 interpretation satisfying not(EDA). 860.26/297.56 860.26/297.56 [a__and](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 860.26/297.56 [0 0] [0 1] [0] 860.26/297.56 860.26/297.56 [tt] = [0] 860.26/297.56 [0] 860.26/297.56 860.26/297.56 [mark](x1) = [1 0] x1 + [0] 860.26/297.56 [0 1] [0] 860.26/297.56 860.26/297.56 [a__plus](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 860.26/297.56 [0 1] [0 1] [0] 860.26/297.56 860.26/297.56 [0] = [0] 860.26/297.56 [0] 860.26/297.56 860.26/297.56 [s](x1) = [1 0] x1 + [0] 860.26/297.56 [0 1] [1] 860.26/297.56 860.26/297.56 [and](x1, x2) = [1 0] x1 + [1 0] x2 + [0] 860.26/297.56 [0 0] [0 1] [0] 860.26/297.56 860.26/297.56 [plus](x1, x2) = [1 0] x1 + [1 1] x2 + [0] 860.26/297.56 [0 1] [0 1] [0] 860.26/297.56 860.26/297.56 The order satisfies the following ordering constraints: 860.26/297.56 860.26/297.56 [a__and(X1, X2)] = [1 0] X1 + [1 0] X2 + [0] 860.26/297.56 [0 0] [0 1] [0] 860.26/297.56 >= [1 0] X1 + [1 0] X2 + [0] 860.26/297.56 [0 0] [0 1] [0] 860.26/297.56 = [and(X1, X2)] 860.26/297.56 860.26/297.56 [a__and(tt(), X)] = [1 0] X + [0] 860.26/297.56 [0 1] [0] 860.26/297.56 >= [1 0] X + [0] 860.26/297.56 [0 1] [0] 860.26/297.56 = [mark(X)] 860.26/297.56 860.26/297.56 [mark(tt())] = [0] 860.26/297.56 [0] 860.26/297.56 >= [0] 860.26/297.56 [0] 860.26/297.56 = [tt()] 860.26/297.56 860.26/297.56 [mark(0())] = [0] 860.26/297.56 [0] 860.26/297.56 >= [0] 860.26/297.56 [0] 860.26/297.56 = [0()] 860.26/297.56 860.26/297.56 [mark(s(X))] = [1 0] X + [0] 860.26/297.56 [0 1] [1] 860.26/297.56 >= [1 0] X + [0] 860.26/297.56 [0 1] [1] 860.26/297.56 = [s(mark(X))] 860.26/297.56 860.26/297.56 [mark(and(X1, X2))] = [1 0] X1 + [1 0] X2 + [0] 860.26/297.56 [0 0] [0 1] [0] 860.26/297.56 >= [1 0] X1 + [1 0] X2 + [0] 860.26/297.56 [0 0] [0 1] [0] 860.26/297.56 = [a__and(mark(X1), X2)] 860.26/297.56 860.26/297.56 [mark(plus(X1, X2))] = [1 0] X1 + [1 1] X2 + [0] 860.26/297.56 [0 1] [0 1] [0] 860.26/297.56 >= [1 0] X1 + [1 1] X2 + [0] 860.26/297.56 [0 1] [0 1] [0] 860.26/297.56 = [a__plus(mark(X1), mark(X2))] 860.26/297.56 860.26/297.56 [a__plus(X1, X2)] = [1 0] X1 + [1 1] X2 + [0] 860.26/297.56 [0 1] [0 1] [0] 860.26/297.56 >= [1 0] X1 + [1 1] X2 + [0] 860.26/297.56 [0 1] [0 1] [0] 860.26/297.56 = [plus(X1, X2)] 860.26/297.56 860.26/297.56 [a__plus(N, 0())] = [1 0] N + [0] 860.26/297.56 [0 1] [0] 860.26/297.56 >= [1 0] N + [0] 860.26/297.56 [0 1] [0] 860.26/297.56 = [mark(N)] 860.26/297.56 860.26/297.56 [a__plus(N, s(M))] = [1 0] N + [1 1] M + [1] 860.26/297.56 [0 1] [0 1] [1] 860.26/297.56 > [1 0] N + [1 1] M + [0] 860.26/297.56 [0 1] [0 1] [1] 860.26/297.56 = [s(a__plus(mark(N), mark(M)))] 860.26/297.56 860.26/297.56 860.26/297.56 We return to the main proof. 860.26/297.56 860.26/297.56 We are left with following problem, upon which TcT provides the 860.26/297.56 certificate MAYBE. 860.26/297.56 860.26/297.56 Strict Trs: 860.26/297.56 { mark(s(X)) -> s(mark(X)) 860.26/297.56 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 860.26/297.56 , a__plus(X1, X2) -> plus(X1, X2) } 860.26/297.56 Weak Trs: 860.26/297.56 { a__and(X1, X2) -> and(X1, X2) 860.26/297.56 , a__and(tt(), X) -> mark(X) 860.26/297.56 , mark(tt()) -> tt() 860.26/297.56 , mark(0()) -> 0() 860.26/297.56 , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)) 860.26/297.56 , a__plus(N, 0()) -> mark(N) 860.26/297.56 , a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) } 860.26/297.56 Obligation: 860.26/297.56 innermost runtime complexity 860.26/297.56 Answer: 860.26/297.56 MAYBE 860.26/297.56 860.26/297.56 None of the processors succeeded. 860.26/297.56 860.26/297.56 Details of failed attempt(s): 860.26/297.56 ----------------------------- 860.26/297.56 1) 'empty' failed due to the following reason: 860.26/297.56 860.26/297.56 Empty strict component of the problem is NOT empty. 860.26/297.56 860.26/297.56 2) 'With Problem ...' failed due to the following reason: 860.26/297.56 860.26/297.56 None of the processors succeeded. 860.26/297.56 860.26/297.56 Details of failed attempt(s): 860.26/297.56 ----------------------------- 860.26/297.56 1) 'empty' failed due to the following reason: 860.26/297.56 860.26/297.56 Empty strict component of the problem is NOT empty. 860.26/297.56 860.26/297.56 2) 'With Problem ...' failed due to the following reason: 860.26/297.56 860.26/297.56 Empty strict component of the problem is NOT empty. 860.26/297.56 860.26/297.56 860.26/297.56 860.26/297.56 860.26/297.56 2) 'With Problem ...' failed due to the following reason: 860.26/297.56 860.26/297.56 None of the processors succeeded. 860.26/297.56 860.26/297.56 Details of failed attempt(s): 860.26/297.56 ----------------------------- 860.26/297.56 1) 'empty' failed due to the following reason: 860.26/297.56 860.26/297.56 Empty strict component of the problem is NOT empty. 860.26/297.56 860.26/297.56 2) 'With Problem ...' failed due to the following reason: 860.26/297.56 860.26/297.56 Empty strict component of the problem is NOT empty. 860.26/297.56 860.26/297.56 860.26/297.56 860.26/297.56 860.26/297.56 860.26/297.56 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 860.26/297.56 failed due to the following reason: 860.26/297.56 860.26/297.56 Computation stopped due to timeout after 24.0 seconds. 860.26/297.56 860.26/297.56 3) 'Best' failed due to the following reason: 860.26/297.56 860.26/297.56 None of the processors succeeded. 860.26/297.56 860.26/297.56 Details of failed attempt(s): 860.26/297.56 ----------------------------- 860.26/297.56 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 860.26/297.56 following reason: 860.26/297.56 860.26/297.56 The input cannot be shown compatible 860.26/297.56 860.26/297.56 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 860.26/297.56 to the following reason: 860.26/297.56 860.26/297.56 The input cannot be shown compatible 860.26/297.56 860.26/297.56 860.26/297.56 860.26/297.56 860.26/297.56 860.26/297.56 Arrrr.. 860.64/297.77 EOF