MAYBE 768.73/297.11 MAYBE 768.73/297.11 768.73/297.11 We are left with following problem, upon which TcT provides the 768.73/297.11 certificate MAYBE. 768.73/297.11 768.73/297.11 Strict Trs: 768.73/297.11 { minus(x, 0()) -> x 768.73/297.11 , minus(s(x), s(y)) -> minus(x, y) 768.73/297.11 , quot(0(), s(y)) -> 0() 768.73/297.11 , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) 768.73/297.11 , le(0(), y) -> true() 768.73/297.11 , le(s(x), 0()) -> false() 768.73/297.11 , le(s(x), s(y)) -> le(x, y) 768.73/297.11 , inc(0()) -> s(0()) 768.73/297.11 , inc(s(x)) -> s(inc(x)) 768.73/297.11 , log(x) -> logIter(x, 0()) 768.73/297.11 , logIter(x, y) -> 768.73/297.11 if(le(s(0()), x), le(s(s(0())), x), quot(x, s(s(0()))), inc(y)) 768.73/297.11 , if(true(), true(), x, y) -> logIter(x, y) 768.73/297.11 , if(true(), false(), x, s(y)) -> y 768.73/297.11 , if(false(), b, x, y) -> logZeroError() } 768.73/297.11 Obligation: 768.73/297.11 innermost runtime complexity 768.73/297.11 Answer: 768.73/297.11 MAYBE 768.73/297.11 768.73/297.11 None of the processors succeeded. 768.73/297.11 768.73/297.11 Details of failed attempt(s): 768.73/297.11 ----------------------------- 768.73/297.11 1) 'empty' failed due to the following reason: 768.73/297.11 768.73/297.11 Empty strict component of the problem is NOT empty. 768.73/297.11 768.73/297.11 2) 'Best' failed due to the following reason: 768.73/297.11 768.73/297.11 None of the processors succeeded. 768.73/297.11 768.73/297.11 Details of failed attempt(s): 768.73/297.11 ----------------------------- 768.73/297.11 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 768.73/297.11 following reason: 768.73/297.11 768.73/297.11 Computation stopped due to timeout after 297.0 seconds. 768.73/297.11 768.73/297.11 2) 'Best' failed due to the following reason: 768.73/297.11 768.73/297.11 None of the processors succeeded. 768.73/297.11 768.73/297.11 Details of failed attempt(s): 768.73/297.11 ----------------------------- 768.73/297.11 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 768.73/297.11 seconds)' failed due to the following reason: 768.73/297.11 768.73/297.11 Computation stopped due to timeout after 148.0 seconds. 768.73/297.11 768.73/297.11 2) 'Best' failed due to the following reason: 768.73/297.11 768.73/297.11 None of the processors succeeded. 768.73/297.11 768.73/297.11 Details of failed attempt(s): 768.73/297.11 ----------------------------- 768.73/297.11 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 768.73/297.11 to the following reason: 768.73/297.11 768.73/297.11 The input cannot be shown compatible 768.73/297.11 768.73/297.11 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 768.73/297.11 following reason: 768.73/297.11 768.73/297.11 The input cannot be shown compatible 768.73/297.11 768.73/297.11 768.73/297.11 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 768.73/297.11 failed due to the following reason: 768.73/297.11 768.73/297.11 None of the processors succeeded. 768.73/297.11 768.73/297.11 Details of failed attempt(s): 768.73/297.11 ----------------------------- 768.73/297.11 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 768.73/297.11 failed due to the following reason: 768.73/297.11 768.73/297.11 match-boundness of the problem could not be verified. 768.73/297.11 768.73/297.11 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 768.73/297.11 failed due to the following reason: 768.73/297.11 768.73/297.11 match-boundness of the problem could not be verified. 768.73/297.11 768.73/297.11 768.73/297.11 768.73/297.11 768.73/297.11 768.73/297.11 Arrrr.. 768.73/297.13 EOF