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