MAYBE 'Pop* with parameter subtitution (timeout of 60.0 seconds)' ----------------------------------------------------------- Answer: MAYBE Input Problem: innermost runtime-complexity with respect to Rules: { a__terms(N) -> cons(recip(a__sqr(mark(N))), terms(s(N))) , a__sqr(0()) -> 0() , a__sqr(s(X)) -> s(a__add(a__sqr(mark(X)), a__dbl(mark(X)))) , a__dbl(0()) -> 0() , a__dbl(s(X)) -> s(s(a__dbl(mark(X)))) , a__add(0(), X) -> mark(X) , a__add(s(X), Y) -> s(a__add(mark(X), mark(Y))) , a__first(0(), X) -> nil() , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)) , mark(terms(X)) -> a__terms(mark(X)) , mark(sqr(X)) -> a__sqr(mark(X)) , mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)) , mark(dbl(X)) -> a__dbl(mark(X)) , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(recip(X)) -> recip(mark(X)) , mark(s(X)) -> s(mark(X)) , mark(0()) -> 0() , mark(nil()) -> nil() , a__terms(X) -> terms(X) , a__sqr(X) -> sqr(X) , a__add(X1, X2) -> add(X1, X2) , a__dbl(X) -> dbl(X) , a__first(X1, X2) -> first(X1, X2)} Proof Output: The input cannot be shown compatible