MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__app(X1,X2)) -> app(X1,X2) activate(n__from(X)) -> from(X) activate(n__nil()) -> nil() activate(n__zWadr(X1,X2)) -> zWadr(X1,X2) app(X1,X2) -> n__app(X1,X2) app(cons(X,XS),YS) -> cons(X,n__app(activate(XS),YS)) app(nil(),YS) -> YS from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) nil() -> n__nil() prefix(L) -> cons(nil(),n__zWadr(L,prefix(L))) zWadr(X1,X2) -> n__zWadr(X1,X2) zWadr(XS,nil()) -> nil() zWadr(cons(X,XS),cons(Y,YS)) -> cons(app(Y,cons(X,n__nil())),n__zWadr(activate(XS),activate(YS))) zWadr(nil(),YS) -> nil() - Signature: {activate/1,app/2,from/1,nil/0,prefix/1,zWadr/2} / {cons/2,n__app/2,n__from/1,n__nil/0,n__zWadr/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,app,from,nil,prefix ,zWadr} and constructors {cons,n__app,n__from,n__nil,n__zWadr,s} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = MiniSMT} + Details: The input can not be schown compatible. MAYBE