MAYBE

Problem:
 app(nil(),YS) -> YS
 app(cons(X,XS),YS) -> cons(X,app(XS,YS))
 from(X) -> cons(X,from(s(X)))
 zWadr(nil(),YS) -> nil()
 zWadr(XS,nil()) -> nil()
 zWadr(cons(X,XS),cons(Y,YS)) -> cons(app(Y,cons(X,nil())),zWadr(XS,YS))
 prefix(L) -> cons(nil(),zWadr(L,prefix(L)))

Proof:
 DP Processor:
  DPs:
   app#(cons(X,XS),YS) -> app#(XS,YS)
   from#(X) -> from#(s(X))
   zWadr#(cons(X,XS),cons(Y,YS)) -> zWadr#(XS,YS)
   zWadr#(cons(X,XS),cons(Y,YS)) -> app#(Y,cons(X,nil()))
   prefix#(L) -> prefix#(L)
   prefix#(L) -> zWadr#(L,prefix(L))
  TRS:
   app(nil(),YS) -> YS
   app(cons(X,XS),YS) -> cons(X,app(XS,YS))
   from(X) -> cons(X,from(s(X)))
   zWadr(nil(),YS) -> nil()
   zWadr(XS,nil()) -> nil()
   zWadr(cons(X,XS),cons(Y,YS)) -> cons(app(Y,cons(X,nil())),zWadr(XS,YS))
   prefix(L) -> cons(nil(),zWadr(L,prefix(L)))
  CDG Processor:
   DPs:
    app#(cons(X,XS),YS) -> app#(XS,YS)
    from#(X) -> from#(s(X))
    zWadr#(cons(X,XS),cons(Y,YS)) -> zWadr#(XS,YS)
    zWadr#(cons(X,XS),cons(Y,YS)) -> app#(Y,cons(X,nil()))
    prefix#(L) -> prefix#(L)
    prefix#(L) -> zWadr#(L,prefix(L))
   TRS:
    app(nil(),YS) -> YS
    app(cons(X,XS),YS) -> cons(X,app(XS,YS))
    from(X) -> cons(X,from(s(X)))
    zWadr(nil(),YS) -> nil()
    zWadr(XS,nil()) -> nil()
    zWadr(cons(X,XS),cons(Y,YS)) -> cons(app(Y,cons(X,nil())),zWadr(XS,YS))
    prefix(L) -> cons(nil(),zWadr(L,prefix(L)))
   graph:
    prefix#(L) -> prefix#(L) -> prefix#(L) -> prefix#(L)
    prefix#(L) -> prefix#(L) -> prefix#(L) -> zWadr#(L,prefix(L))
    prefix#(L) -> zWadr#(L,prefix(L)) ->
    zWadr#(cons(X,XS),cons(Y,YS)) -> zWadr#(XS,YS)
    prefix#(L) -> zWadr#(L,prefix(L)) ->
    zWadr#(cons(X,XS),cons(Y,YS)) -> app#(Y,cons(X,nil()))
    zWadr#(cons(X,XS),cons(Y,YS)) -> zWadr#(XS,YS) ->
    zWadr#(cons(X,XS),cons(Y,YS)) -> zWadr#(XS,YS)
    zWadr#(cons(X,XS),cons(Y,YS)) -> zWadr#(XS,YS) ->
    zWadr#(cons(X,XS),cons(Y,YS)) -> app#(Y,cons(X,nil()))
    zWadr#(cons(X,XS),cons(Y,YS)) -> app#(Y,cons(X,nil())) ->
    app#(cons(X,XS),YS) -> app#(XS,YS)
    from#(X) -> from#(s(X)) -> from#(X) -> from#(s(X))
    app#(cons(X,XS),YS) -> app#(XS,YS) -> app#(cons(X,XS),YS) -> app#(XS,YS)
   SCC Processor:
    #sccs: 4
    #rules: 4
    #arcs: 9/36
    DPs:
     from#(X) -> from#(s(X))
    TRS:
     app(nil(),YS) -> YS
     app(cons(X,XS),YS) -> cons(X,app(XS,YS))
     from(X) -> cons(X,from(s(X)))
     zWadr(nil(),YS) -> nil()
     zWadr(XS,nil()) -> nil()
     zWadr(cons(X,XS),cons(Y,YS)) -> cons(app(Y,cons(X,nil())),zWadr(XS,YS))
     prefix(L) -> cons(nil(),zWadr(L,prefix(L)))
    Open
    
    DPs:
     prefix#(L) -> prefix#(L)
    TRS:
     app(nil(),YS) -> YS
     app(cons(X,XS),YS) -> cons(X,app(XS,YS))
     from(X) -> cons(X,from(s(X)))
     zWadr(nil(),YS) -> nil()
     zWadr(XS,nil()) -> nil()
     zWadr(cons(X,XS),cons(Y,YS)) -> cons(app(Y,cons(X,nil())),zWadr(XS,YS))
     prefix(L) -> cons(nil(),zWadr(L,prefix(L)))
    Open
    
    DPs:
     zWadr#(cons(X,XS),cons(Y,YS)) -> zWadr#(XS,YS)
    TRS:
     app(nil(),YS) -> YS
     app(cons(X,XS),YS) -> cons(X,app(XS,YS))
     from(X) -> cons(X,from(s(X)))
     zWadr(nil(),YS) -> nil()
     zWadr(XS,nil()) -> nil()
     zWadr(cons(X,XS),cons(Y,YS)) -> cons(app(Y,cons(X,nil())),zWadr(XS,YS))
     prefix(L) -> cons(nil(),zWadr(L,prefix(L)))
    Open
    
    DPs:
     app#(cons(X,XS),YS) -> app#(XS,YS)
    TRS:
     app(nil(),YS) -> YS
     app(cons(X,XS),YS) -> cons(X,app(XS,YS))
     from(X) -> cons(X,from(s(X)))
     zWadr(nil(),YS) -> nil()
     zWadr(XS,nil()) -> nil()
     zWadr(cons(X,XS),cons(Y,YS)) -> cons(app(Y,cons(X,nil())),zWadr(XS,YS))
     prefix(L) -> cons(nil(),zWadr(L,prefix(L)))
    Open