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