MAYBE 'Pop* with parameter subtitution (timeout of 60.0 seconds)' ----------------------------------------------------------- Answer: MAYBE Input Problem: innermost runtime-complexity with respect to Rules: { average(x, y) -> if(ge(x, y), x, y) , if(true(), x, y) -> averIter(y, x, y) , if(false(), x, y) -> averIter(x, y, x) , averIter(x, y, z) -> ifIter(ge(x, y), x, y, z) , ifIter(true(), x, y, z) -> z , ifIter(false(), x, y, z) -> averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0()))) , append(nil(), y) -> y , append(cons(n, x), y) -> cons(n, app(x, y)) , low(n, nil()) -> nil() , low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x)) , if_low(false(), n, cons(m, x)) -> cons(m, low(n, x)) , if_low(true(), n, cons(m, x)) -> low(n, x) , high(n, nil()) -> nil() , high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x)) , if_high(false(), n, cons(m, x)) -> high(n, x) , if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x)) , quicksort(x) -> ifquick(isempty(x), x) , ifquick(true(), x) -> nil() , ifquick(false(), x) -> append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x))))) , plus(0(), y) -> y , plus(s(x), y) -> s(plus(x, y)) , isempty(nil()) -> true() , isempty(cons(n, x)) -> false() , head(nil()) -> error() , head(cons(n, x)) -> n , tail(nil()) -> nil() , tail(cons(n, x)) -> x , ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , a() -> b() , a() -> c()} Proof Output: The input cannot be shown compatible