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