MAYBE
Time: 0.005028
TRS:
 {                    app(X1, X2) -> n__app(X1, X2),
                   app(nil(), YS) -> YS,
             app(cons(X, XS), YS) -> cons(X, n__app(activate XS, YS)),
                            nil() -> n__nil(),
                       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),
                           from X -> cons(X, n__from s X),
                           from X -> n__from X,
                 zWadr(XS, nil()) -> nil(),
                    zWadr(X1, X2) -> n__zWadr(X1, X2),
                 zWadr(nil(), YS) -> nil(),
  zWadr(cons(X, XS), cons(Y, YS)) -> cons(app(Y, cons(X, n__nil())), n__zWadr(activate XS, activate YS)),
                         prefix L -> cons(nil(), n__zWadr(L, prefix L))}
 DP:
  DP:
   {           app#(cons(X, XS), YS) -> activate# XS,
            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),
    zWadr#(cons(X, XS), cons(Y, YS)) -> app#(Y, cons(X, n__nil())),
    zWadr#(cons(X, XS), cons(Y, YS)) -> activate# YS,
    zWadr#(cons(X, XS), cons(Y, YS)) -> activate# XS,
                           prefix# L -> nil#(),
                           prefix# L -> prefix# L}
  TRS:
  {                    app(X1, X2) -> n__app(X1, X2),
                    app(nil(), YS) -> YS,
              app(cons(X, XS), YS) -> cons(X, n__app(activate XS, YS)),
                             nil() -> n__nil(),
                        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),
                            from X -> cons(X, n__from s X),
                            from X -> n__from X,
                  zWadr(XS, nil()) -> nil(),
                     zWadr(X1, X2) -> n__zWadr(X1, X2),
                  zWadr(nil(), YS) -> nil(),
   zWadr(cons(X, XS), cons(Y, YS)) -> cons(app(Y, cons(X, n__nil())), n__zWadr(activate XS, activate YS)),
                          prefix L -> cons(nil(), n__zWadr(L, prefix L))}
  UR:
   {}
   EDG:
    {(app#(cons(X, XS), YS) -> activate# XS, activate# n__nil() -> nil#())
     (prefix# L -> prefix# L, prefix# L -> prefix# L)
     (prefix# L -> prefix# L, prefix# L -> nil#())
     (zWadr#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__nil() -> nil#())
     (activate# n__app(X1, X2) -> app#(X1, X2), app#(cons(X, XS), YS) -> activate# XS)
     (zWadr#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__nil() -> nil#())}
    STATUS:
     arrows: 0.940000
     SCCS (1):
      Scc:
       {prefix# L -> prefix# L}
      
      
      
      
      
      SCC (1):
       Strict:
        {prefix# L -> prefix# L}
       Weak:
       {                    app(X1, X2) -> n__app(X1, X2),
                         app(nil(), YS) -> YS,
                   app(cons(X, XS), YS) -> cons(X, n__app(activate XS, YS)),
                                  nil() -> n__nil(),
                             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),
                                 from X -> cons(X, n__from s X),
                                 from X -> n__from X,
                       zWadr(XS, nil()) -> nil(),
                          zWadr(X1, X2) -> n__zWadr(X1, X2),
                       zWadr(nil(), YS) -> nil(),
        zWadr(cons(X, XS), cons(Y, YS)) -> cons(app(Y, cons(X, n__nil())), n__zWadr(activate XS, activate YS)),
                               prefix L -> cons(nil(), n__zWadr(L, prefix L))}
       Open