MAYBE 'Pop* with parameter subtitution (timeout of 60.0 seconds)' ----------------------------------------------------------- Answer: MAYBE Input Problem: innermost runtime-complexity with respect to Rules: { times(x, y) -> sum(generate(x, y)) , generate(x, y) -> gen(x, y, 0()) , gen(x, y, z) -> if(ge(z, x), x, y, z) , if(true(), x, y, z) -> nil() , if(false(), x, y, z) -> cons(y, gen(x, y, s(z))) , sum(xs) -> sum2(xs, 0()) , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y) , ifsum(true(), b, xs, y) -> y , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y) , ifsum2(true(), xs, y) -> sum2(tail(xs), y) , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y)) , isNil(nil()) -> true() , isNil(cons(x, xs)) -> false() , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , head(cons(x, xs)) -> x , head(nil()) -> error() , isZero(0()) -> true() , isZero(s(0())) -> false() , isZero(s(s(x))) -> isZero(s(x)) , p(0()) -> s(s(0())) , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , a() -> c() , a() -> d()} Proof Output: The input cannot be shown compatible