MAYBE 972.23/297.02 MAYBE 972.23/297.02 972.23/297.02 We are left with following problem, upon which TcT provides the 972.23/297.02 certificate MAYBE. 972.23/297.02 972.23/297.02 Strict Trs: 972.23/297.02 { U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)) 972.23/297.02 , U12(tt(), M, N) -> s(plus(activate(N), activate(M))) 972.23/297.02 , activate(X) -> X 972.23/297.02 , plus(N, s(M)) -> U11(tt(), M, N) 972.23/297.02 , plus(N, 0()) -> N 972.23/297.02 , U21(tt(), M, N) -> U22(tt(), activate(M), activate(N)) 972.23/297.02 , U22(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 972.23/297.02 , x(N, s(M)) -> U21(tt(), M, N) 972.23/297.02 , x(N, 0()) -> 0() } 972.23/297.02 Obligation: 972.23/297.02 runtime complexity 972.23/297.02 Answer: 972.23/297.02 MAYBE 972.23/297.02 972.23/297.02 None of the processors succeeded. 972.23/297.02 972.23/297.02 Details of failed attempt(s): 972.23/297.02 ----------------------------- 972.23/297.02 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 972.23/297.02 following reason: 972.23/297.02 972.23/297.02 Computation stopped due to timeout after 297.0 seconds. 972.23/297.02 972.23/297.02 2) 'Best' failed due to the following reason: 972.23/297.02 972.23/297.02 None of the processors succeeded. 972.23/297.02 972.23/297.02 Details of failed attempt(s): 972.23/297.02 ----------------------------- 972.23/297.02 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 972.23/297.02 seconds)' failed due to the following reason: 972.23/297.02 972.23/297.02 Computation stopped due to timeout after 148.0 seconds. 972.23/297.02 972.23/297.02 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 972.23/297.02 failed due to the following reason: 972.23/297.02 972.23/297.02 None of the processors succeeded. 972.23/297.02 972.23/297.02 Details of failed attempt(s): 972.23/297.02 ----------------------------- 972.23/297.02 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 972.23/297.02 failed due to the following reason: 972.23/297.02 972.23/297.02 match-boundness of the problem could not be verified. 972.23/297.02 972.23/297.02 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 972.23/297.02 failed due to the following reason: 972.23/297.02 972.23/297.02 match-boundness of the problem could not be verified. 972.23/297.02 972.23/297.02 972.23/297.02 3) 'Best' failed due to the following reason: 972.23/297.02 972.23/297.02 None of the processors succeeded. 972.23/297.02 972.23/297.02 Details of failed attempt(s): 972.23/297.02 ----------------------------- 972.23/297.02 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 972.23/297.02 following reason: 972.23/297.02 972.23/297.02 The processor is inapplicable, reason: 972.23/297.02 Processor only applicable for innermost runtime complexity analysis 972.23/297.02 972.23/297.02 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 972.23/297.02 to the following reason: 972.23/297.02 972.23/297.02 The processor is inapplicable, reason: 972.23/297.02 Processor only applicable for innermost runtime complexity analysis 972.23/297.02 972.23/297.02 972.23/297.02 972.23/297.02 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 972.23/297.02 the following reason: 972.23/297.02 972.23/297.02 We add the following weak dependency pairs: 972.23/297.02 972.23/297.02 Strict DPs: 972.23/297.02 { U11^#(tt(), M, N) -> c_1(U12^#(tt(), activate(M), activate(N))) 972.23/297.02 , U12^#(tt(), M, N) -> c_2(plus^#(activate(N), activate(M))) 972.23/297.02 , plus^#(N, s(M)) -> c_4(U11^#(tt(), M, N)) 972.23/297.02 , plus^#(N, 0()) -> c_5(N) 972.23/297.02 , activate^#(X) -> c_3(X) 972.23/297.02 , U21^#(tt(), M, N) -> c_6(U22^#(tt(), activate(M), activate(N))) 972.23/297.02 , U22^#(tt(), M, N) -> 972.23/297.02 c_7(plus^#(x(activate(N), activate(M)), activate(N))) 972.23/297.02 , x^#(N, s(M)) -> c_8(U21^#(tt(), M, N)) 972.23/297.02 , x^#(N, 0()) -> c_9() } 972.23/297.02 972.23/297.02 and mark the set of starting terms. 972.23/297.02 972.23/297.02 We are left with following problem, upon which TcT provides the 972.23/297.02 certificate MAYBE. 972.23/297.02 972.23/297.02 Strict DPs: 972.23/297.02 { U11^#(tt(), M, N) -> c_1(U12^#(tt(), activate(M), activate(N))) 972.23/297.02 , U12^#(tt(), M, N) -> c_2(plus^#(activate(N), activate(M))) 972.23/297.02 , plus^#(N, s(M)) -> c_4(U11^#(tt(), M, N)) 972.23/297.02 , plus^#(N, 0()) -> c_5(N) 972.23/297.02 , activate^#(X) -> c_3(X) 972.23/297.02 , U21^#(tt(), M, N) -> c_6(U22^#(tt(), activate(M), activate(N))) 972.23/297.02 , U22^#(tt(), M, N) -> 972.23/297.02 c_7(plus^#(x(activate(N), activate(M)), activate(N))) 972.23/297.02 , x^#(N, s(M)) -> c_8(U21^#(tt(), M, N)) 972.23/297.02 , x^#(N, 0()) -> c_9() } 972.23/297.02 Strict Trs: 972.23/297.02 { U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)) 972.23/297.02 , U12(tt(), M, N) -> s(plus(activate(N), activate(M))) 972.23/297.02 , activate(X) -> X 972.23/297.02 , plus(N, s(M)) -> U11(tt(), M, N) 972.23/297.02 , plus(N, 0()) -> N 972.23/297.02 , U21(tt(), M, N) -> U22(tt(), activate(M), activate(N)) 972.23/297.02 , U22(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 972.23/297.02 , x(N, s(M)) -> U21(tt(), M, N) 972.23/297.02 , x(N, 0()) -> 0() } 972.23/297.02 Obligation: 972.23/297.02 runtime complexity 972.23/297.02 Answer: 972.23/297.02 MAYBE 972.23/297.02 972.23/297.02 We estimate the number of application of {9} by applications of 972.23/297.02 Pre({9}) = {4,5}. Here rules are labeled as follows: 972.23/297.02 972.23/297.02 DPs: 972.23/297.02 { 1: U11^#(tt(), M, N) -> 972.23/297.02 c_1(U12^#(tt(), activate(M), activate(N))) 972.23/297.02 , 2: U12^#(tt(), M, N) -> c_2(plus^#(activate(N), activate(M))) 972.23/297.02 , 3: plus^#(N, s(M)) -> c_4(U11^#(tt(), M, N)) 972.23/297.02 , 4: plus^#(N, 0()) -> c_5(N) 972.23/297.02 , 5: activate^#(X) -> c_3(X) 972.23/297.02 , 6: U21^#(tt(), M, N) -> 972.23/297.02 c_6(U22^#(tt(), activate(M), activate(N))) 972.23/297.02 , 7: U22^#(tt(), M, N) -> 972.23/297.02 c_7(plus^#(x(activate(N), activate(M)), activate(N))) 972.23/297.02 , 8: x^#(N, s(M)) -> c_8(U21^#(tt(), M, N)) 972.23/297.02 , 9: x^#(N, 0()) -> c_9() } 972.23/297.02 972.23/297.02 We are left with following problem, upon which TcT provides the 972.23/297.02 certificate MAYBE. 972.23/297.02 972.23/297.02 Strict DPs: 972.23/297.02 { U11^#(tt(), M, N) -> c_1(U12^#(tt(), activate(M), activate(N))) 972.23/297.02 , U12^#(tt(), M, N) -> c_2(plus^#(activate(N), activate(M))) 972.23/297.02 , plus^#(N, s(M)) -> c_4(U11^#(tt(), M, N)) 972.23/297.02 , plus^#(N, 0()) -> c_5(N) 972.23/297.02 , activate^#(X) -> c_3(X) 972.23/297.02 , U21^#(tt(), M, N) -> c_6(U22^#(tt(), activate(M), activate(N))) 972.23/297.02 , U22^#(tt(), M, N) -> 972.23/297.02 c_7(plus^#(x(activate(N), activate(M)), activate(N))) 972.23/297.02 , x^#(N, s(M)) -> c_8(U21^#(tt(), M, N)) } 972.23/297.02 Strict Trs: 972.23/297.02 { U11(tt(), M, N) -> U12(tt(), activate(M), activate(N)) 972.23/297.02 , U12(tt(), M, N) -> s(plus(activate(N), activate(M))) 972.23/297.02 , activate(X) -> X 972.23/297.02 , plus(N, s(M)) -> U11(tt(), M, N) 972.23/297.02 , plus(N, 0()) -> N 972.23/297.02 , U21(tt(), M, N) -> U22(tt(), activate(M), activate(N)) 972.23/297.02 , U22(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N)) 972.23/297.02 , x(N, s(M)) -> U21(tt(), M, N) 972.23/297.02 , x(N, 0()) -> 0() } 972.23/297.02 Weak DPs: { x^#(N, 0()) -> c_9() } 972.23/297.02 Obligation: 972.23/297.02 runtime complexity 972.23/297.02 Answer: 972.23/297.02 MAYBE 972.23/297.02 972.23/297.02 Empty strict component of the problem is NOT empty. 972.23/297.02 972.23/297.02 972.23/297.02 Arrrr.. 972.64/297.46 EOF