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