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