MAYBE 1089.70/297.77 MAYBE 1089.70/297.77 1089.70/297.77 We are left with following problem, upon which TcT provides the 1089.70/297.77 certificate MAYBE. 1089.70/297.77 1089.70/297.77 Strict Trs: 1089.70/297.77 { times(x, y) -> sum(generate(x, y)) 1089.70/297.77 , sum(xs) -> sum2(xs, 0()) 1089.70/297.77 , generate(x, y) -> gen(x, y, 0()) 1089.70/297.77 , gen(x, y, z) -> if(ge(z, x), x, y, z) 1089.70/297.77 , if(true(), x, y, z) -> nil() 1089.70/297.77 , if(false(), x, y, z) -> cons(y, gen(x, y, s(z))) 1089.70/297.77 , ge(x, 0()) -> true() 1089.70/297.77 , ge(0(), s(y)) -> false() 1089.70/297.77 , ge(s(x), s(y)) -> ge(x, y) 1089.70/297.77 , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y) 1089.70/297.77 , ifsum(true(), b, xs, y) -> y 1089.70/297.77 , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y) 1089.70/297.77 , isNil(nil()) -> true() 1089.70/297.77 , isNil(cons(x, xs)) -> false() 1089.70/297.77 , isZero(0()) -> true() 1089.70/297.77 , isZero(s(0())) -> false() 1089.70/297.77 , isZero(s(s(x))) -> isZero(s(x)) 1089.70/297.77 , head(nil()) -> error() 1089.70/297.77 , head(cons(x, xs)) -> x 1089.70/297.77 , ifsum2(true(), xs, y) -> sum2(tail(xs), y) 1089.70/297.77 , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y)) 1089.70/297.77 , tail(nil()) -> nil() 1089.70/297.77 , tail(cons(x, xs)) -> xs 1089.70/297.77 , p(0()) -> s(s(0())) 1089.70/297.77 , p(s(0())) -> 0() 1089.70/297.77 , p(s(s(x))) -> s(p(s(x))) 1089.70/297.77 , a() -> c() 1089.70/297.77 , a() -> d() } 1089.70/297.77 Obligation: 1089.70/297.77 innermost runtime complexity 1089.70/297.77 Answer: 1089.70/297.77 MAYBE 1089.70/297.77 1089.70/297.77 None of the processors succeeded. 1089.70/297.77 1089.70/297.77 Details of failed attempt(s): 1089.70/297.77 ----------------------------- 1089.70/297.77 1) 'empty' failed due to the following reason: 1089.70/297.77 1089.70/297.77 Empty strict component of the problem is NOT empty. 1089.70/297.77 1089.70/297.77 2) 'Best' failed due to the following reason: 1089.70/297.77 1089.70/297.77 None of the processors succeeded. 1089.70/297.77 1089.70/297.77 Details of failed attempt(s): 1089.70/297.77 ----------------------------- 1089.70/297.77 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1089.70/297.77 following reason: 1089.70/297.77 1089.70/297.77 Computation stopped due to timeout after 297.0 seconds. 1089.70/297.77 1089.70/297.77 2) 'Best' failed due to the following reason: 1089.70/297.77 1089.70/297.77 None of the processors succeeded. 1089.70/297.77 1089.70/297.77 Details of failed attempt(s): 1089.70/297.77 ----------------------------- 1089.70/297.77 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1089.70/297.77 seconds)' failed due to the following reason: 1089.70/297.77 1089.70/297.77 Computation stopped due to timeout after 148.0 seconds. 1089.70/297.77 1089.70/297.77 2) 'Best' failed due to the following reason: 1089.70/297.77 1089.70/297.77 None of the processors succeeded. 1089.70/297.77 1089.70/297.77 Details of failed attempt(s): 1089.70/297.77 ----------------------------- 1089.70/297.77 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1089.70/297.77 following reason: 1089.70/297.77 1089.70/297.77 The input cannot be shown compatible 1089.70/297.77 1089.70/297.77 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1089.70/297.77 to the following reason: 1089.70/297.77 1089.70/297.77 The input cannot be shown compatible 1089.70/297.77 1089.70/297.77 1089.70/297.77 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1089.70/297.77 failed due to the following reason: 1089.70/297.77 1089.70/297.77 None of the processors succeeded. 1089.70/297.77 1089.70/297.77 Details of failed attempt(s): 1089.70/297.77 ----------------------------- 1089.70/297.77 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1089.70/297.77 failed due to the following reason: 1089.70/297.77 1089.70/297.77 match-boundness of the problem could not be verified. 1089.70/297.77 1089.70/297.77 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1089.70/297.77 failed due to the following reason: 1089.70/297.77 1089.70/297.77 match-boundness of the problem could not be verified. 1089.70/297.77 1089.70/297.77 1089.70/297.77 1089.70/297.77 1089.70/297.77 1089.70/297.77 Arrrr.. 1090.23/298.05 EOF