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