MAYBE
Time: 0.267344
TRS:
 {                 app(nil(), YS) -> YS,
             app(cons(X, XS), YS) -> cons(X, app(XS, YS)),
                           from X -> cons(X, from s X),
                 zWadr(XS, nil()) -> nil(),
                 zWadr(nil(), YS) -> 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))}
 DP:
  DP:
   {           app#(cons(X, XS), YS) -> app#(XS, YS),
                             from# X -> from# s X,
    zWadr#(cons(X, XS), cons(Y, YS)) -> app#(Y, cons(X, nil())),
    zWadr#(cons(X, XS), cons(Y, YS)) -> zWadr#(XS, YS),
                           prefix# L -> zWadr#(L, prefix L),
                           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(XS, nil()) -> nil(),
                  zWadr(nil(), YS) -> 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))}
  UR:
   {                 app(nil(), YS) -> YS,
               app(cons(X, XS), YS) -> cons(X, app(XS, YS)),
                   zWadr(XS, nil()) -> nil(),
                   zWadr(nil(), YS) -> 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)),
                            a(x, y) -> x,
                            a(x, y) -> y}
   EDG:
    {(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())))
     (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)) -> app#(Y, cons(X, nil())), app#(cons(X, XS), YS) -> app#(XS, YS))
     (from# X -> from# s X, from# X -> from# s X)
     (prefix# L -> prefix# L, prefix# L -> zWadr#(L, prefix L))
     (prefix# L -> prefix# L, prefix# L -> prefix# L)
     (app#(cons(X, XS), YS) -> app#(XS, YS), app#(cons(X, XS), YS) -> app#(XS, YS))}
    STATUS:
     arrows: 0.750000
     SCCS (4):
      Scc:
       {from# X -> from# s X}
      Scc:
       {prefix# L -> prefix# L}
      Scc:
       {zWadr#(cons(X, XS), cons(Y, YS)) -> zWadr#(XS, YS)}
      Scc:
       {app#(cons(X, XS), YS) -> app#(XS, YS)}
      
      SCC (1):
       Strict:
        {from# X -> from# s X}
       Weak:
       {                 app(nil(), YS) -> YS,
                   app(cons(X, XS), YS) -> cons(X, app(XS, YS)),
                                 from X -> cons(X, from s X),
                       zWadr(XS, nil()) -> nil(),
                       zWadr(nil(), YS) -> 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
      SCC (1):
       Strict:
        {prefix# L -> prefix# L}
       Weak:
       {                 app(nil(), YS) -> YS,
                   app(cons(X, XS), YS) -> cons(X, app(XS, YS)),
                                 from X -> cons(X, from s X),
                       zWadr(XS, nil()) -> nil(),
                       zWadr(nil(), YS) -> 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
      
      SCC (1):
       Strict:
        {zWadr#(cons(X, XS), cons(Y, YS)) -> zWadr#(XS, YS)}
       Weak:
       {                 app(nil(), YS) -> YS,
                   app(cons(X, XS), YS) -> cons(X, app(XS, YS)),
                                 from X -> cons(X, from s X),
                       zWadr(XS, nil()) -> nil(),
                       zWadr(nil(), YS) -> 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
      
      SCC (1):
       Strict:
        {app#(cons(X, XS), YS) -> app#(XS, YS)}
       Weak:
       {                 app(nil(), YS) -> YS,
                   app(cons(X, XS), YS) -> cons(X, app(XS, YS)),
                                 from X -> cons(X, from s X),
                       zWadr(XS, nil()) -> nil(),
                       zWadr(nil(), YS) -> 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