YES(?,POLY) 'Pop* with parameter subtitution (timeout of 60.0 seconds)' ----------------------------------------------------------- Answer: YES(?,POLY) Input Problem: innermost runtime-complexity with respect to Rules: { app(nil(), YS) -> YS , app(cons(X), YS) -> cons(X) , from(X) -> cons(X) , zWadr(nil(), YS) -> nil() , zWadr(XS, nil()) -> nil() , zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X))) , prefix(L) -> cons(nil())} Proof Output: The input was oriented with the instance of POP* as induced by the precedence app ~ from, app ~ zWadr, app ~ prefix, from ~ zWadr, from ~ prefix, zWadr ~ prefix and safe mapping safe(app) = {1, 2}, safe(nil) = {}, safe(cons) = {1}, safe(from) = {}, safe(zWadr) = {1}, safe(prefix) = {} . For your convenience, here is the input in predicative notation: Rules: { app(; nil(), YS) -> YS , app(; cons(; X), YS) -> cons(; X) , from(X;) -> cons(; X) , zWadr(YS; nil()) -> nil() , zWadr(nil(); XS) -> nil() , zWadr(cons(; Y); cons(; X)) -> cons(; app(; Y, cons(; X))) , prefix(L;) -> cons(; nil())}