MAYBE
Time: 0.060064
TRS:
 {                      mark app(X1, X2) -> active app(mark X1, mark X2),
                              mark nil() -> active nil(),
                       mark cons(X1, X2) -> active cons(mark X1, X2),
                             mark from X -> active from mark X,
                                mark s X -> active s mark X,
                      mark zWadr(X1, X2) -> active zWadr(mark X1, mark X2),
                           mark prefix X -> active prefix mark X,
                   active app(nil(), YS) -> mark YS,
             active app(cons(X, XS), YS) -> mark cons(X, app(XS, YS)),
                           active from X -> mark cons(X, from s X),
                 active zWadr(XS, nil()) -> mark nil(),
                 active zWadr(nil(), YS) -> mark nil(),
  active zWadr(cons(X, XS), cons(Y, YS)) -> mark cons(app(Y, cons(X, nil())), zWadr(XS, YS)),
                         active prefix L -> mark cons(nil(), zWadr(L, prefix L)),
                        app(X1, mark X2) -> app(X1, X2),
                      app(X1, active X2) -> app(X1, X2),
                        app(mark X1, X2) -> app(X1, X2),
                      app(active X1, X2) -> app(X1, X2),
                       cons(X1, mark X2) -> cons(X1, X2),
                     cons(X1, active X2) -> cons(X1, X2),
                       cons(mark X1, X2) -> cons(X1, X2),
                     cons(active X1, X2) -> cons(X1, X2),
                             from mark X -> from X,
                           from active X -> from X,
                                s mark X -> s X,
                              s active X -> s X,
                      zWadr(X1, mark X2) -> zWadr(X1, X2),
                    zWadr(X1, active X2) -> zWadr(X1, X2),
                      zWadr(mark X1, X2) -> zWadr(X1, X2),
                    zWadr(active X1, X2) -> zWadr(X1, X2),
                           prefix mark X -> prefix X,
                         prefix active X -> prefix X}
 DP:
  DP:
   {                      mark# app(X1, X2) -> mark# X1,
                          mark# app(X1, X2) -> mark# X2,
                          mark# app(X1, X2) -> active# app(mark X1, mark X2),
                          mark# app(X1, X2) -> app#(mark X1, mark X2),
                                mark# nil() -> active# nil(),
                         mark# cons(X1, X2) -> mark# X1,
                         mark# cons(X1, X2) -> active# cons(mark X1, X2),
                         mark# cons(X1, X2) -> cons#(mark X1, X2),
                               mark# from X -> mark# X,
                               mark# from X -> active# from mark X,
                               mark# from X -> from# mark X,
                                  mark# s X -> mark# X,
                                  mark# s X -> active# s mark X,
                                  mark# s X -> s# mark X,
                        mark# zWadr(X1, X2) -> mark# X1,
                        mark# zWadr(X1, X2) -> mark# X2,
                        mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2),
                        mark# zWadr(X1, X2) -> zWadr#(mark X1, mark X2),
                             mark# prefix X -> mark# X,
                             mark# prefix X -> active# prefix mark X,
                             mark# prefix X -> prefix# mark X,
                     active# app(nil(), YS) -> mark# YS,
               active# app(cons(X, XS), YS) -> mark# cons(X, app(XS, YS)),
               active# app(cons(X, XS), YS) -> app#(XS, YS),
               active# app(cons(X, XS), YS) -> cons#(X, app(XS, YS)),
                             active# from X -> mark# cons(X, from s X),
                             active# from X -> cons#(X, from s X),
                             active# from X -> from# s X,
                             active# from X -> s# X,
                   active# zWadr(XS, nil()) -> mark# nil(),
                   active# zWadr(nil(), YS) -> mark# nil(),
    active# zWadr(cons(X, XS), cons(Y, YS)) -> mark# cons(app(Y, cons(X, nil())), zWadr(XS, YS)),
    active# zWadr(cons(X, XS), cons(Y, YS)) -> app#(Y, cons(X, nil())),
    active# zWadr(cons(X, XS), cons(Y, YS)) -> cons#(X, nil()),
    active# zWadr(cons(X, XS), cons(Y, YS)) -> cons#(app(Y, cons(X, nil())), zWadr(XS, YS)),
    active# zWadr(cons(X, XS), cons(Y, YS)) -> zWadr#(XS, YS),
                           active# prefix L -> mark# cons(nil(), zWadr(L, prefix L)),
                           active# prefix L -> cons#(nil(), zWadr(L, prefix L)),
                           active# prefix L -> zWadr#(L, prefix L),
                          app#(X1, mark X2) -> app#(X1, X2),
                        app#(X1, active X2) -> app#(X1, X2),
                          app#(mark X1, X2) -> app#(X1, X2),
                        app#(active X1, X2) -> app#(X1, X2),
                         cons#(X1, mark X2) -> cons#(X1, X2),
                       cons#(X1, active X2) -> cons#(X1, X2),
                         cons#(mark X1, X2) -> cons#(X1, X2),
                       cons#(active X1, X2) -> cons#(X1, X2),
                               from# mark X -> from# X,
                             from# active X -> from# X,
                                  s# mark X -> s# X,
                                s# active X -> s# X,
                        zWadr#(X1, mark X2) -> zWadr#(X1, X2),
                      zWadr#(X1, active X2) -> zWadr#(X1, X2),
                        zWadr#(mark X1, X2) -> zWadr#(X1, X2),
                      zWadr#(active X1, X2) -> zWadr#(X1, X2),
                             prefix# mark X -> prefix# X,
                           prefix# active X -> prefix# X}
  TRS:
  {                      mark app(X1, X2) -> active app(mark X1, mark X2),
                               mark nil() -> active nil(),
                        mark cons(X1, X2) -> active cons(mark X1, X2),
                              mark from X -> active from mark X,
                                 mark s X -> active s mark X,
                       mark zWadr(X1, X2) -> active zWadr(mark X1, mark X2),
                            mark prefix X -> active prefix mark X,
                    active app(nil(), YS) -> mark YS,
              active app(cons(X, XS), YS) -> mark cons(X, app(XS, YS)),
                            active from X -> mark cons(X, from s X),
                  active zWadr(XS, nil()) -> mark nil(),
                  active zWadr(nil(), YS) -> mark nil(),
   active zWadr(cons(X, XS), cons(Y, YS)) -> mark cons(app(Y, cons(X, nil())), zWadr(XS, YS)),
                          active prefix L -> mark cons(nil(), zWadr(L, prefix L)),
                         app(X1, mark X2) -> app(X1, X2),
                       app(X1, active X2) -> app(X1, X2),
                         app(mark X1, X2) -> app(X1, X2),
                       app(active X1, X2) -> app(X1, X2),
                        cons(X1, mark X2) -> cons(X1, X2),
                      cons(X1, active X2) -> cons(X1, X2),
                        cons(mark X1, X2) -> cons(X1, X2),
                      cons(active X1, X2) -> cons(X1, X2),
                              from mark X -> from X,
                            from active X -> from X,
                                 s mark X -> s X,
                               s active X -> s X,
                       zWadr(X1, mark X2) -> zWadr(X1, X2),
                     zWadr(X1, active X2) -> zWadr(X1, X2),
                       zWadr(mark X1, X2) -> zWadr(X1, X2),
                     zWadr(active X1, X2) -> zWadr(X1, X2),
                            prefix mark X -> prefix X,
                          prefix active X -> prefix X}
  UR:
   {                      mark app(X1, X2) -> active app(mark X1, mark X2),
                                mark nil() -> active nil(),
                         mark cons(X1, X2) -> active cons(mark X1, X2),
                               mark from X -> active from mark X,
                                  mark s X -> active s mark X,
                        mark zWadr(X1, X2) -> active zWadr(mark X1, mark X2),
                             mark prefix X -> active prefix mark X,
                     active app(nil(), YS) -> mark YS,
               active app(cons(X, XS), YS) -> mark cons(X, app(XS, YS)),
                             active from X -> mark cons(X, from s X),
                   active zWadr(XS, nil()) -> mark nil(),
                   active zWadr(nil(), YS) -> mark nil(),
    active zWadr(cons(X, XS), cons(Y, YS)) -> mark cons(app(Y, cons(X, nil())), zWadr(XS, YS)),
                           active prefix L -> mark cons(nil(), zWadr(L, prefix L)),
                          app(X1, mark X2) -> app(X1, X2),
                        app(X1, active X2) -> app(X1, X2),
                          app(mark X1, X2) -> app(X1, X2),
                        app(active X1, X2) -> app(X1, X2),
                         cons(X1, mark X2) -> cons(X1, X2),
                       cons(X1, active X2) -> cons(X1, X2),
                         cons(mark X1, X2) -> cons(X1, X2),
                       cons(active X1, X2) -> cons(X1, X2),
                               from mark X -> from X,
                             from active X -> from X,
                                  s mark X -> s X,
                                s active X -> s X,
                        zWadr(X1, mark X2) -> zWadr(X1, X2),
                      zWadr(X1, active X2) -> zWadr(X1, X2),
                        zWadr(mark X1, X2) -> zWadr(X1, X2),
                      zWadr(active X1, X2) -> zWadr(X1, X2),
                             prefix mark X -> prefix X,
                           prefix active X -> prefix X,
                                   a(x, y) -> x,
                                   a(x, y) -> y}
   EDG:
    {
     (active# zWadr(cons(X, XS), cons(Y, YS)) -> zWadr#(XS, YS), zWadr#(active X1, X2) -> zWadr#(X1, X2))
     (active# zWadr(cons(X, XS), cons(Y, YS)) -> zWadr#(XS, YS), zWadr#(mark X1, X2) -> zWadr#(X1, X2))
     (active# zWadr(cons(X, XS), cons(Y, YS)) -> zWadr#(XS, YS), zWadr#(X1, active X2) -> zWadr#(X1, X2))
     (active# zWadr(cons(X, XS), cons(Y, YS)) -> zWadr#(XS, YS), zWadr#(X1, mark X2) -> zWadr#(X1, X2))
     (app#(X1, active X2) -> app#(X1, X2), app#(active X1, X2) -> app#(X1, X2))
     (app#(X1, active X2) -> app#(X1, X2), app#(mark X1, X2) -> app#(X1, X2))
     (app#(X1, active X2) -> app#(X1, X2), app#(X1, active X2) -> app#(X1, X2))
     (app#(X1, active X2) -> app#(X1, X2), app#(X1, mark X2) -> app#(X1, X2))
     (app#(active X1, X2) -> app#(X1, X2), app#(active X1, X2) -> app#(X1, X2))
     (app#(active X1, X2) -> app#(X1, X2), app#(mark X1, X2) -> app#(X1, X2))
     (app#(active X1, X2) -> app#(X1, X2), app#(X1, active X2) -> app#(X1, X2))
     (app#(active X1, X2) -> app#(X1, X2), app#(X1, mark X2) -> app#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (zWadr#(X1, active X2) -> zWadr#(X1, X2), zWadr#(active X1, X2) -> zWadr#(X1, X2))
     (zWadr#(X1, active X2) -> zWadr#(X1, X2), zWadr#(mark X1, X2) -> zWadr#(X1, X2))
     (zWadr#(X1, active X2) -> zWadr#(X1, X2), zWadr#(X1, active X2) -> zWadr#(X1, X2))
     (zWadr#(X1, active X2) -> zWadr#(X1, X2), zWadr#(X1, mark X2) -> zWadr#(X1, X2))
     (zWadr#(active X1, X2) -> zWadr#(X1, X2), zWadr#(active X1, X2) -> zWadr#(X1, X2))
     (zWadr#(active X1, X2) -> zWadr#(X1, X2), zWadr#(mark X1, X2) -> zWadr#(X1, X2))
     (zWadr#(active X1, X2) -> zWadr#(X1, X2), zWadr#(X1, active X2) -> zWadr#(X1, X2))
     (zWadr#(active X1, X2) -> zWadr#(X1, X2), zWadr#(X1, mark X2) -> zWadr#(X1, X2))
     (mark# zWadr(X1, X2) -> zWadr#(mark X1, mark X2), zWadr#(active X1, X2) -> zWadr#(X1, X2))
     (mark# zWadr(X1, X2) -> zWadr#(mark X1, mark X2), zWadr#(mark X1, X2) -> zWadr#(X1, X2))
     (mark# zWadr(X1, X2) -> zWadr#(mark X1, mark X2), zWadr#(X1, active X2) -> zWadr#(X1, X2))
     (mark# zWadr(X1, X2) -> zWadr#(mark X1, mark X2), zWadr#(X1, mark X2) -> zWadr#(X1, X2))
     (mark# app(X1, X2) -> mark# X2, mark# prefix X -> prefix# mark X)
     (mark# app(X1, X2) -> mark# X2, mark# prefix X -> active# prefix mark X)
     (mark# app(X1, X2) -> mark# X2, mark# prefix X -> mark# X)
     (mark# app(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> zWadr#(mark X1, mark X2))
     (mark# app(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2))
     (mark# app(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> mark# X2)
     (mark# app(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> mark# X1)
     (mark# app(X1, X2) -> mark# X2, mark# s X -> s# mark X)
     (mark# app(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
     (mark# app(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# app(X1, X2) -> mark# X2, mark# from X -> from# mark X)
     (mark# app(X1, X2) -> mark# X2, mark# from X -> active# from mark X)
     (mark# app(X1, X2) -> mark# X2, mark# from X -> mark# X)
     (mark# app(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# app(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# app(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (mark# app(X1, X2) -> mark# X2, mark# nil() -> active# nil())
     (mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> app#(mark X1, mark X2))
     (mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> active# app(mark X1, mark X2))
     (mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> mark# X2)
     (mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> mark# X1)
     (active# app(nil(), YS) -> mark# YS, mark# prefix X -> prefix# mark X)
     (active# app(nil(), YS) -> mark# YS, mark# prefix X -> active# prefix mark X)
     (active# app(nil(), YS) -> mark# YS, mark# prefix X -> mark# X)
     (active# app(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> zWadr#(mark X1, mark X2))
     (active# app(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2))
     (active# app(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> mark# X2)
     (active# app(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> mark# X1)
     (active# app(nil(), YS) -> mark# YS, mark# s X -> s# mark X)
     (active# app(nil(), YS) -> mark# YS, mark# s X -> active# s mark X)
     (active# app(nil(), YS) -> mark# YS, mark# s X -> mark# X)
     (active# app(nil(), YS) -> mark# YS, mark# from X -> from# mark X)
     (active# app(nil(), YS) -> mark# YS, mark# from X -> active# from mark X)
     (active# app(nil(), YS) -> mark# YS, mark# from X -> mark# X)
     (active# app(nil(), YS) -> mark# YS, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# app(nil(), YS) -> mark# YS, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# app(nil(), YS) -> mark# YS, mark# cons(X1, X2) -> mark# X1)
     (active# app(nil(), YS) -> mark# YS, mark# nil() -> active# nil())
     (active# app(nil(), YS) -> mark# YS, mark# app(X1, X2) -> app#(mark X1, mark X2))
     (active# app(nil(), YS) -> mark# YS, mark# app(X1, X2) -> active# app(mark X1, mark X2))
     (active# app(nil(), YS) -> mark# YS, mark# app(X1, X2) -> mark# X2)
     (active# app(nil(), YS) -> mark# YS, mark# app(X1, X2) -> mark# X1)
     (mark# from X -> active# from mark X, active# from X -> s# X)
     (mark# from X -> active# from mark X, active# from X -> from# s X)
     (mark# from X -> active# from mark X, active# from X -> cons#(X, from s X))
     (mark# from X -> active# from mark X, active# from X -> mark# cons(X, from s X))
     (mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2), active# zWadr(cons(X, XS), cons(Y, YS)) -> zWadr#(XS, YS))
     (mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2), active# zWadr(cons(X, XS), cons(Y, YS)) -> cons#(app(Y, cons(X, nil())), zWadr(XS, YS)))
     (mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2), active# zWadr(cons(X, XS), cons(Y, YS)) -> cons#(X, nil()))
     (mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2), active# zWadr(cons(X, XS), cons(Y, YS)) -> app#(Y, cons(X, nil())))
     (mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2), active# zWadr(cons(X, XS), cons(Y, YS)) -> mark# cons(app(Y, cons(X, nil())), zWadr(XS, YS)))
     (mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2), active# zWadr(nil(), YS) -> mark# nil())
     (mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2), active# zWadr(XS, nil()) -> mark# nil())
     (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# prefix X -> prefix# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# prefix X -> active# prefix mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# prefix X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> zWadr#(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> from# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil())
     (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> app#(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> active# app(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1)
     (active# zWadr(nil(), YS) -> mark# nil(), mark# nil() -> active# nil())
     (active# zWadr(cons(X, XS), cons(Y, YS)) -> cons#(X, nil()), cons#(active X1, X2) -> cons#(X1, X2))
     (active# zWadr(cons(X, XS), cons(Y, YS)) -> cons#(X, nil()), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# zWadr(cons(X, XS), cons(Y, YS)) -> mark# cons(app(Y, cons(X, nil())), zWadr(XS, YS)), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# zWadr(cons(X, XS), cons(Y, YS)) -> mark# cons(app(Y, cons(X, nil())), zWadr(XS, YS)), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# zWadr(cons(X, XS), cons(Y, YS)) -> mark# cons(app(Y, cons(X, nil())), zWadr(XS, YS)), mark# cons(X1, X2) -> mark# X1)
     (active# zWadr(cons(X, XS), cons(Y, YS)) -> app#(Y, cons(X, nil())), app#(active X1, X2) -> app#(X1, X2))
     (active# zWadr(cons(X, XS), cons(Y, YS)) -> app#(Y, cons(X, nil())), app#(mark X1, X2) -> app#(X1, X2))
     (mark# from X -> from# mark X, from# active X -> from# X)
     (mark# from X -> from# mark X, from# mark X -> from# X)
     (mark# prefix X -> prefix# mark X, prefix# active X -> prefix# X)
     (mark# prefix X -> prefix# mark X, prefix# mark X -> prefix# X)
     (active# app(cons(X, XS), YS) -> cons#(X, app(XS, YS)), cons#(active X1, X2) -> cons#(X1, X2))
     (active# app(cons(X, XS), YS) -> cons#(X, app(XS, YS)), cons#(mark X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (mark# from X -> mark# X, mark# prefix X -> prefix# mark X)
     (mark# from X -> mark# X, mark# prefix X -> active# prefix mark X)
     (mark# from X -> mark# X, mark# prefix X -> mark# X)
     (mark# from X -> mark# X, mark# zWadr(X1, X2) -> zWadr#(mark X1, mark X2))
     (mark# from X -> mark# X, mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2))
     (mark# from X -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
     (mark# from X -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
     (mark# from X -> mark# X, mark# s X -> s# mark X)
     (mark# from X -> mark# X, mark# s X -> active# s mark X)
     (mark# from X -> mark# X, mark# s X -> mark# X)
     (mark# from X -> mark# X, mark# from X -> from# mark X)
     (mark# from X -> mark# X, mark# from X -> active# from mark X)
     (mark# from X -> mark# X, mark# from X -> mark# X)
     (mark# from X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# from X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# from X -> mark# X, mark# nil() -> active# nil())
     (mark# from X -> mark# X, mark# app(X1, X2) -> app#(mark X1, mark X2))
     (mark# from X -> mark# X, mark# app(X1, X2) -> active# app(mark X1, mark X2))
     (mark# from X -> mark# X, mark# app(X1, X2) -> mark# X2)
     (mark# from X -> mark# X, mark# app(X1, X2) -> mark# X1)
     (mark# prefix X -> mark# X, mark# prefix X -> prefix# mark X)
     (mark# prefix X -> mark# X, mark# prefix X -> active# prefix mark X)
     (mark# prefix X -> mark# X, mark# prefix X -> mark# X)
     (mark# prefix X -> mark# X, mark# zWadr(X1, X2) -> zWadr#(mark X1, mark X2))
     (mark# prefix X -> mark# X, mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2))
     (mark# prefix X -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
     (mark# prefix X -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
     (mark# prefix X -> mark# X, mark# s X -> s# mark X)
     (mark# prefix X -> mark# X, mark# s X -> active# s mark X)
     (mark# prefix X -> mark# X, mark# s X -> mark# X)
     (mark# prefix X -> mark# X, mark# from X -> from# mark X)
     (mark# prefix X -> mark# X, mark# from X -> active# from mark X)
     (mark# prefix X -> mark# X, mark# from X -> mark# X)
     (mark# prefix X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# prefix X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# prefix X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# prefix X -> mark# X, mark# nil() -> active# nil())
     (mark# prefix X -> mark# X, mark# app(X1, X2) -> app#(mark X1, mark X2))
     (mark# prefix X -> mark# X, mark# app(X1, X2) -> active# app(mark X1, mark X2))
     (mark# prefix X -> mark# X, mark# app(X1, X2) -> mark# X2)
     (mark# prefix X -> mark# X, mark# app(X1, X2) -> mark# X1)
     (from# mark X -> from# X, from# active X -> from# X)
     (from# mark X -> from# X, from# mark X -> from# X)
     (s# mark X -> s# X, s# active X -> s# X)
     (s# mark X -> s# X, s# mark X -> s# X)
     (prefix# mark X -> prefix# X, prefix# active X -> prefix# X)
     (prefix# mark X -> prefix# X, prefix# mark X -> prefix# X)
     (prefix# active X -> prefix# X, prefix# mark X -> prefix# X)
     (prefix# active X -> prefix# X, prefix# active X -> prefix# X)
     (s# active X -> s# X, s# mark X -> s# X)
     (s# active X -> s# X, s# active X -> s# X)
     (from# active X -> from# X, from# mark X -> from# X)
     (from# active X -> from# X, from# active X -> from# X)
     (active# from X -> s# X, s# mark X -> s# X)
     (active# from X -> s# X, s# active X -> s# X)
     (mark# s X -> mark# X, mark# app(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# app(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# app(X1, X2) -> active# app(mark X1, mark X2))
     (mark# s X -> mark# X, mark# app(X1, X2) -> app#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# nil() -> active# nil())
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# s X -> mark# X, mark# from X -> mark# X)
     (mark# s X -> mark# X, mark# from X -> active# from mark X)
     (mark# s X -> mark# X, mark# from X -> from# mark X)
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# s X -> active# s mark X)
     (mark# s X -> mark# X, mark# s X -> s# mark X)
     (mark# s X -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2))
     (mark# s X -> mark# X, mark# zWadr(X1, X2) -> zWadr#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# prefix X -> mark# X)
     (mark# s X -> mark# X, mark# prefix X -> active# prefix mark X)
     (mark# s X -> mark# X, mark# prefix X -> prefix# mark X)
     (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# from X -> cons#(X, from s X), cons#(active X1, X2) -> cons#(X1, X2))
     (mark# s X -> s# mark X, s# mark X -> s# X)
     (mark# s X -> s# mark X, s# active X -> s# X)
     (active# prefix L -> mark# cons(nil(), zWadr(L, prefix L)), mark# cons(X1, X2) -> mark# X1)
     (active# prefix L -> mark# cons(nil(), zWadr(L, prefix L)), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# prefix L -> mark# cons(nil(), zWadr(L, prefix L)), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# app(cons(X, XS), YS) -> mark# cons(X, app(XS, YS)), mark# cons(X1, X2) -> mark# X1)
     (active# app(cons(X, XS), YS) -> mark# cons(X, app(XS, YS)), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# app(cons(X, XS), YS) -> mark# cons(X, app(XS, YS)), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# zWadr(XS, nil()) -> mark# nil(), mark# nil() -> active# nil())
     (mark# zWadr(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1)
     (mark# zWadr(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2)
     (mark# zWadr(X1, X2) -> mark# X1, mark# app(X1, X2) -> active# app(mark X1, mark X2))
     (mark# zWadr(X1, X2) -> mark# X1, mark# app(X1, X2) -> app#(mark X1, mark X2))
     (mark# zWadr(X1, X2) -> mark# X1, mark# nil() -> active# nil())
     (mark# zWadr(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# zWadr(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# zWadr(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# zWadr(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# zWadr(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
     (mark# zWadr(X1, X2) -> mark# X1, mark# from X -> from# mark X)
     (mark# zWadr(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# zWadr(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# zWadr(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# zWadr(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X1)
     (mark# zWadr(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2)
     (mark# zWadr(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2))
     (mark# zWadr(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> zWadr#(mark X1, mark X2))
     (mark# zWadr(X1, X2) -> mark# X1, mark# prefix X -> mark# X)
     (mark# zWadr(X1, X2) -> mark# X1, mark# prefix X -> active# prefix mark X)
     (mark# zWadr(X1, X2) -> mark# X1, mark# prefix X -> prefix# mark X)
     (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1)
     (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2)
     (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> active# app(mark X1, mark X2))
     (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> app#(mark X1, mark X2))
     (mark# app(X1, X2) -> mark# X1, mark# nil() -> active# nil())
     (mark# app(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# app(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# app(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# app(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# app(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
     (mark# app(X1, X2) -> mark# X1, mark# from X -> from# mark X)
     (mark# app(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# app(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# app(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X1)
     (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2)
     (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2))
     (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> zWadr#(mark X1, mark X2))
     (mark# app(X1, X2) -> mark# X1, mark# prefix X -> mark# X)
     (mark# app(X1, X2) -> mark# X1, mark# prefix X -> active# prefix mark X)
     (mark# app(X1, X2) -> mark# X1, mark# prefix X -> prefix# mark X)
     (mark# prefix X -> active# prefix mark X, active# prefix L -> mark# cons(nil(), zWadr(L, prefix L)))
     (mark# prefix X -> active# prefix mark X, active# prefix L -> cons#(nil(), zWadr(L, prefix L)))
     (mark# prefix X -> active# prefix mark X, active# prefix L -> zWadr#(L, prefix L))
     (mark# app(X1, X2) -> active# app(mark X1, mark X2), active# app(nil(), YS) -> mark# YS)
     (mark# app(X1, X2) -> active# app(mark X1, mark X2), active# app(cons(X, XS), YS) -> mark# cons(X, app(XS, YS)))
     (mark# app(X1, X2) -> active# app(mark X1, mark X2), active# app(cons(X, XS), YS) -> app#(XS, YS))
     (mark# app(X1, X2) -> active# app(mark X1, mark X2), active# app(cons(X, XS), YS) -> cons#(X, app(XS, YS)))
     (mark# zWadr(X1, X2) -> mark# X2, mark# app(X1, X2) -> mark# X1)
     (mark# zWadr(X1, X2) -> mark# X2, mark# app(X1, X2) -> mark# X2)
     (mark# zWadr(X1, X2) -> mark# X2, mark# app(X1, X2) -> active# app(mark X1, mark X2))
     (mark# zWadr(X1, X2) -> mark# X2, mark# app(X1, X2) -> app#(mark X1, mark X2))
     (mark# zWadr(X1, X2) -> mark# X2, mark# nil() -> active# nil())
     (mark# zWadr(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (mark# zWadr(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# zWadr(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# zWadr(X1, X2) -> mark# X2, mark# from X -> mark# X)
     (mark# zWadr(X1, X2) -> mark# X2, mark# from X -> active# from mark X)
     (mark# zWadr(X1, X2) -> mark# X2, mark# from X -> from# mark X)
     (mark# zWadr(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# zWadr(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
     (mark# zWadr(X1, X2) -> mark# X2, mark# s X -> s# mark X)
     (mark# zWadr(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> mark# X1)
     (mark# zWadr(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> mark# X2)
     (mark# zWadr(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2))
     (mark# zWadr(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> zWadr#(mark X1, mark X2))
     (mark# zWadr(X1, X2) -> mark# X2, mark# prefix X -> mark# X)
     (mark# zWadr(X1, X2) -> mark# X2, mark# prefix X -> active# prefix mark X)
     (mark# zWadr(X1, X2) -> mark# X2, mark# prefix X -> prefix# mark X)
     (active# prefix L -> zWadr#(L, prefix L), zWadr#(mark X1, X2) -> zWadr#(X1, X2))
     (active# prefix L -> zWadr#(L, prefix L), zWadr#(active X1, X2) -> zWadr#(X1, X2))
     (mark# app(X1, X2) -> app#(mark X1, mark X2), app#(X1, mark X2) -> app#(X1, X2))
     (mark# app(X1, X2) -> app#(mark X1, mark X2), app#(X1, active X2) -> app#(X1, X2))
     (mark# app(X1, X2) -> app#(mark X1, mark X2), app#(mark X1, X2) -> app#(X1, X2))
     (mark# app(X1, X2) -> app#(mark X1, mark X2), app#(active X1, X2) -> app#(X1, X2))
     (zWadr#(mark X1, X2) -> zWadr#(X1, X2), zWadr#(X1, mark X2) -> zWadr#(X1, X2))
     (zWadr#(mark X1, X2) -> zWadr#(X1, X2), zWadr#(X1, active X2) -> zWadr#(X1, X2))
     (zWadr#(mark X1, X2) -> zWadr#(X1, X2), zWadr#(mark X1, X2) -> zWadr#(X1, X2))
     (zWadr#(mark X1, X2) -> zWadr#(X1, X2), zWadr#(active X1, X2) -> zWadr#(X1, X2))
     (zWadr#(X1, mark X2) -> zWadr#(X1, X2), zWadr#(X1, mark X2) -> zWadr#(X1, X2))
     (zWadr#(X1, mark X2) -> zWadr#(X1, X2), zWadr#(X1, active X2) -> zWadr#(X1, X2))
     (zWadr#(X1, mark X2) -> zWadr#(X1, X2), zWadr#(mark X1, X2) -> zWadr#(X1, X2))
     (zWadr#(X1, mark X2) -> zWadr#(X1, X2), zWadr#(active X1, X2) -> zWadr#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (app#(mark X1, X2) -> app#(X1, X2), app#(X1, mark X2) -> app#(X1, X2))
     (app#(mark X1, X2) -> app#(X1, X2), app#(X1, active X2) -> app#(X1, X2))
     (app#(mark X1, X2) -> app#(X1, X2), app#(mark X1, X2) -> app#(X1, X2))
     (app#(mark X1, X2) -> app#(X1, X2), app#(active X1, X2) -> app#(X1, X2))
     (app#(X1, mark X2) -> app#(X1, X2), app#(X1, mark X2) -> app#(X1, X2))
     (app#(X1, mark X2) -> app#(X1, X2), app#(X1, active X2) -> app#(X1, X2))
     (app#(X1, mark X2) -> app#(X1, X2), app#(mark X1, X2) -> app#(X1, X2))
     (app#(X1, mark X2) -> app#(X1, X2), app#(active X1, X2) -> app#(X1, X2))
     (active# app(cons(X, XS), YS) -> app#(XS, YS), app#(X1, mark X2) -> app#(X1, X2))
     (active# app(cons(X, XS), YS) -> app#(XS, YS), app#(X1, active X2) -> app#(X1, X2))
     (active# app(cons(X, XS), YS) -> app#(XS, YS), app#(mark X1, X2) -> app#(X1, X2))
     (active# app(cons(X, XS), YS) -> app#(XS, YS), app#(active X1, X2) -> app#(X1, X2))
    }
    STATUS:
     arrows: 0.901816
     SCCS (7):
      Scc:
       {                      mark# app(X1, X2) -> mark# X1,
                              mark# app(X1, X2) -> mark# X2,
                              mark# app(X1, X2) -> active# app(mark X1, mark X2),
                             mark# cons(X1, X2) -> mark# X1,
                                   mark# from X -> mark# X,
                                   mark# from X -> active# from mark X,
                                      mark# s X -> mark# X,
                            mark# zWadr(X1, X2) -> mark# X1,
                            mark# zWadr(X1, X2) -> mark# X2,
                            mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2),
                                 mark# prefix X -> mark# X,
                                 mark# prefix X -> active# prefix mark X,
                         active# app(nil(), YS) -> mark# YS,
                   active# app(cons(X, XS), YS) -> mark# cons(X, app(XS, YS)),
                                 active# from X -> mark# cons(X, from s X),
        active# zWadr(cons(X, XS), cons(Y, YS)) -> mark# cons(app(Y, cons(X, nil())), zWadr(XS, YS)),
                               active# prefix L -> mark# cons(nil(), zWadr(L, prefix L))}
      Scc:
       {  prefix# mark X -> prefix# X,
        prefix# active X -> prefix# X}
      Scc:
       {  from# mark X -> from# X,
        from# active X -> from# X}
      Scc:
       {  s# mark X -> s# X,
        s# active X -> s# X}
      Scc:
       {  cons#(X1, mark X2) -> cons#(X1, X2),
        cons#(X1, active X2) -> cons#(X1, X2),
          cons#(mark X1, X2) -> cons#(X1, X2),
        cons#(active X1, X2) -> cons#(X1, X2)}
      Scc:
       {  zWadr#(X1, mark X2) -> zWadr#(X1, X2),
        zWadr#(X1, active X2) -> zWadr#(X1, X2),
          zWadr#(mark X1, X2) -> zWadr#(X1, X2),
        zWadr#(active X1, X2) -> zWadr#(X1, X2)}
      Scc:
       {  app#(X1, mark X2) -> app#(X1, X2),
        app#(X1, active X2) -> app#(X1, X2),
          app#(mark X1, X2) -> app#(X1, X2),
        app#(active X1, X2) -> app#(X1, X2)}
      
      SCC (17):
       Strict:
        {                      mark# app(X1, X2) -> mark# X1,
                               mark# app(X1, X2) -> mark# X2,
                               mark# app(X1, X2) -> active# app(mark X1, mark X2),
                              mark# cons(X1, X2) -> mark# X1,
                                    mark# from X -> mark# X,
                                    mark# from X -> active# from mark X,
                                       mark# s X -> mark# X,
                             mark# zWadr(X1, X2) -> mark# X1,
                             mark# zWadr(X1, X2) -> mark# X2,
                             mark# zWadr(X1, X2) -> active# zWadr(mark X1, mark X2),
                                  mark# prefix X -> mark# X,
                                  mark# prefix X -> active# prefix mark X,
                          active# app(nil(), YS) -> mark# YS,
                    active# app(cons(X, XS), YS) -> mark# cons(X, app(XS, YS)),
                                  active# from X -> mark# cons(X, from s X),
         active# zWadr(cons(X, XS), cons(Y, YS)) -> mark# cons(app(Y, cons(X, nil())), zWadr(XS, YS)),
                                active# prefix L -> mark# cons(nil(), zWadr(L, prefix L))}
       Weak:
       {                      mark app(X1, X2) -> active app(mark X1, mark X2),
                                    mark nil() -> active nil(),
                             mark cons(X1, X2) -> active cons(mark X1, X2),
                                   mark from X -> active from mark X,
                                      mark s X -> active s mark X,
                            mark zWadr(X1, X2) -> active zWadr(mark X1, mark X2),
                                 mark prefix X -> active prefix mark X,
                         active app(nil(), YS) -> mark YS,
                   active app(cons(X, XS), YS) -> mark cons(X, app(XS, YS)),
                                 active from X -> mark cons(X, from s X),
                       active zWadr(XS, nil()) -> mark nil(),
                       active zWadr(nil(), YS) -> mark nil(),
        active zWadr(cons(X, XS), cons(Y, YS)) -> mark cons(app(Y, cons(X, nil())), zWadr(XS, YS)),
                               active prefix L -> mark cons(nil(), zWadr(L, prefix L)),
                              app(X1, mark X2) -> app(X1, X2),
                            app(X1, active X2) -> app(X1, X2),
                              app(mark X1, X2) -> app(X1, X2),
                            app(active X1, X2) -> app(X1, X2),
                             cons(X1, mark X2) -> cons(X1, X2),
                           cons(X1, active X2) -> cons(X1, X2),
                             cons(mark X1, X2) -> cons(X1, X2),
                           cons(active X1, X2) -> cons(X1, X2),
                                   from mark X -> from X,
                                 from active X -> from X,
                                      s mark X -> s X,
                                    s active X -> s X,
                            zWadr(X1, mark X2) -> zWadr(X1, X2),
                          zWadr(X1, active X2) -> zWadr(X1, X2),
                            zWadr(mark X1, X2) -> zWadr(X1, X2),
                          zWadr(active X1, X2) -> zWadr(X1, X2),
                                 prefix mark X -> prefix X,
                               prefix active X -> prefix X}
       Open
      
      
      SCC (2):
       Strict:
        {  prefix# mark X -> prefix# X,
         prefix# active X -> prefix# X}
       Weak:
       {                      mark app(X1, X2) -> active app(mark X1, mark X2),
                                    mark nil() -> active nil(),
                             mark cons(X1, X2) -> active cons(mark X1, X2),
                                   mark from X -> active from mark X,
                                      mark s X -> active s mark X,
                            mark zWadr(X1, X2) -> active zWadr(mark X1, mark X2),
                                 mark prefix X -> active prefix mark X,
                         active app(nil(), YS) -> mark YS,
                   active app(cons(X, XS), YS) -> mark cons(X, app(XS, YS)),
                                 active from X -> mark cons(X, from s X),
                       active zWadr(XS, nil()) -> mark nil(),
                       active zWadr(nil(), YS) -> mark nil(),
        active zWadr(cons(X, XS), cons(Y, YS)) -> mark cons(app(Y, cons(X, nil())), zWadr(XS, YS)),
                               active prefix L -> mark cons(nil(), zWadr(L, prefix L)),
                              app(X1, mark X2) -> app(X1, X2),
                            app(X1, active X2) -> app(X1, X2),
                              app(mark X1, X2) -> app(X1, X2),
                            app(active X1, X2) -> app(X1, X2),
                             cons(X1, mark X2) -> cons(X1, X2),
                           cons(X1, active X2) -> cons(X1, X2),
                             cons(mark X1, X2) -> cons(X1, X2),
                           cons(active X1, X2) -> cons(X1, X2),
                                   from mark X -> from X,
                                 from active X -> from X,
                                      s mark X -> s X,
                                    s active X -> s X,
                            zWadr(X1, mark X2) -> zWadr(X1, X2),
                          zWadr(X1, active X2) -> zWadr(X1, X2),
                            zWadr(mark X1, X2) -> zWadr(X1, X2),
                          zWadr(active X1, X2) -> zWadr(X1, X2),
                                 prefix mark X -> prefix X,
                               prefix active X -> prefix X}
       Open
      
      
      
      
      
      
      
      
      
      SCC (2):
       Strict:
        {  from# mark X -> from# X,
         from# active X -> from# X}
       Weak:
       {                      mark app(X1, X2) -> active app(mark X1, mark X2),
                                    mark nil() -> active nil(),
                             mark cons(X1, X2) -> active cons(mark X1, X2),
                                   mark from X -> active from mark X,
                                      mark s X -> active s mark X,
                            mark zWadr(X1, X2) -> active zWadr(mark X1, mark X2),
                                 mark prefix X -> active prefix mark X,
                         active app(nil(), YS) -> mark YS,
                   active app(cons(X, XS), YS) -> mark cons(X, app(XS, YS)),
                                 active from X -> mark cons(X, from s X),
                       active zWadr(XS, nil()) -> mark nil(),
                       active zWadr(nil(), YS) -> mark nil(),
        active zWadr(cons(X, XS), cons(Y, YS)) -> mark cons(app(Y, cons(X, nil())), zWadr(XS, YS)),
                               active prefix L -> mark cons(nil(), zWadr(L, prefix L)),
                              app(X1, mark X2) -> app(X1, X2),
                            app(X1, active X2) -> app(X1, X2),
                              app(mark X1, X2) -> app(X1, X2),
                            app(active X1, X2) -> app(X1, X2),
                             cons(X1, mark X2) -> cons(X1, X2),
                           cons(X1, active X2) -> cons(X1, X2),
                             cons(mark X1, X2) -> cons(X1, X2),
                           cons(active X1, X2) -> cons(X1, X2),
                                   from mark X -> from X,
                                 from active X -> from X,
                                      s mark X -> s X,
                                    s active X -> s X,
                            zWadr(X1, mark X2) -> zWadr(X1, X2),
                          zWadr(X1, active X2) -> zWadr(X1, X2),
                            zWadr(mark X1, X2) -> zWadr(X1, X2),
                          zWadr(active X1, X2) -> zWadr(X1, X2),
                                 prefix mark X -> prefix X,
                               prefix active X -> prefix X}
       Open
      
      SCC (2):
       Strict:
        {  s# mark X -> s# X,
         s# active X -> s# X}
       Weak:
       {                      mark app(X1, X2) -> active app(mark X1, mark X2),
                                    mark nil() -> active nil(),
                             mark cons(X1, X2) -> active cons(mark X1, X2),
                                   mark from X -> active from mark X,
                                      mark s X -> active s mark X,
                            mark zWadr(X1, X2) -> active zWadr(mark X1, mark X2),
                                 mark prefix X -> active prefix mark X,
                         active app(nil(), YS) -> mark YS,
                   active app(cons(X, XS), YS) -> mark cons(X, app(XS, YS)),
                                 active from X -> mark cons(X, from s X),
                       active zWadr(XS, nil()) -> mark nil(),
                       active zWadr(nil(), YS) -> mark nil(),
        active zWadr(cons(X, XS), cons(Y, YS)) -> mark cons(app(Y, cons(X, nil())), zWadr(XS, YS)),
                               active prefix L -> mark cons(nil(), zWadr(L, prefix L)),
                              app(X1, mark X2) -> app(X1, X2),
                            app(X1, active X2) -> app(X1, X2),
                              app(mark X1, X2) -> app(X1, X2),
                            app(active X1, X2) -> app(X1, X2),
                             cons(X1, mark X2) -> cons(X1, X2),
                           cons(X1, active X2) -> cons(X1, X2),
                             cons(mark X1, X2) -> cons(X1, X2),
                           cons(active X1, X2) -> cons(X1, X2),
                                   from mark X -> from X,
                                 from active X -> from X,
                                      s mark X -> s X,
                                    s active X -> s X,
                            zWadr(X1, mark X2) -> zWadr(X1, X2),
                          zWadr(X1, active X2) -> zWadr(X1, X2),
                            zWadr(mark X1, X2) -> zWadr(X1, X2),
                          zWadr(active X1, X2) -> zWadr(X1, X2),
                                 prefix mark X -> prefix X,
                               prefix active X -> prefix X}
       Open
      
      
      
      
      
      
      
      
      SCC (4):
       Strict:
        {  cons#(X1, mark X2) -> cons#(X1, X2),
         cons#(X1, active X2) -> cons#(X1, X2),
           cons#(mark X1, X2) -> cons#(X1, X2),
         cons#(active X1, X2) -> cons#(X1, X2)}
       Weak:
       {                      mark app(X1, X2) -> active app(mark X1, mark X2),
                                    mark nil() -> active nil(),
                             mark cons(X1, X2) -> active cons(mark X1, X2),
                                   mark from X -> active from mark X,
                                      mark s X -> active s mark X,
                            mark zWadr(X1, X2) -> active zWadr(mark X1, mark X2),
                                 mark prefix X -> active prefix mark X,
                         active app(nil(), YS) -> mark YS,
                   active app(cons(X, XS), YS) -> mark cons(X, app(XS, YS)),
                                 active from X -> mark cons(X, from s X),
                       active zWadr(XS, nil()) -> mark nil(),
                       active zWadr(nil(), YS) -> mark nil(),
        active zWadr(cons(X, XS), cons(Y, YS)) -> mark cons(app(Y, cons(X, nil())), zWadr(XS, YS)),
                               active prefix L -> mark cons(nil(), zWadr(L, prefix L)),
                              app(X1, mark X2) -> app(X1, X2),
                            app(X1, active X2) -> app(X1, X2),
                              app(mark X1, X2) -> app(X1, X2),
                            app(active X1, X2) -> app(X1, X2),
                             cons(X1, mark X2) -> cons(X1, X2),
                           cons(X1, active X2) -> cons(X1, X2),
                             cons(mark X1, X2) -> cons(X1, X2),
                           cons(active X1, X2) -> cons(X1, X2),
                                   from mark X -> from X,
                                 from active X -> from X,
                                      s mark X -> s X,
                                    s active X -> s X,
                            zWadr(X1, mark X2) -> zWadr(X1, X2),
                          zWadr(X1, active X2) -> zWadr(X1, X2),
                            zWadr(mark X1, X2) -> zWadr(X1, X2),
                          zWadr(active X1, X2) -> zWadr(X1, X2),
                                 prefix mark X -> prefix X,
                               prefix active X -> prefix X}
       Open
      
      SCC (4):
       Strict:
        {  zWadr#(X1, mark X2) -> zWadr#(X1, X2),
         zWadr#(X1, active X2) -> zWadr#(X1, X2),
           zWadr#(mark X1, X2) -> zWadr#(X1, X2),
         zWadr#(active X1, X2) -> zWadr#(X1, X2)}
       Weak:
       {                      mark app(X1, X2) -> active app(mark X1, mark X2),
                                    mark nil() -> active nil(),
                             mark cons(X1, X2) -> active cons(mark X1, X2),
                                   mark from X -> active from mark X,
                                      mark s X -> active s mark X,
                            mark zWadr(X1, X2) -> active zWadr(mark X1, mark X2),
                                 mark prefix X -> active prefix mark X,
                         active app(nil(), YS) -> mark YS,
                   active app(cons(X, XS), YS) -> mark cons(X, app(XS, YS)),
                                 active from X -> mark cons(X, from s X),
                       active zWadr(XS, nil()) -> mark nil(),
                       active zWadr(nil(), YS) -> mark nil(),
        active zWadr(cons(X, XS), cons(Y, YS)) -> mark cons(app(Y, cons(X, nil())), zWadr(XS, YS)),
                               active prefix L -> mark cons(nil(), zWadr(L, prefix L)),
                              app(X1, mark X2) -> app(X1, X2),
                            app(X1, active X2) -> app(X1, X2),
                              app(mark X1, X2) -> app(X1, X2),
                            app(active X1, X2) -> app(X1, X2),
                             cons(X1, mark X2) -> cons(X1, X2),
                           cons(X1, active X2) -> cons(X1, X2),
                             cons(mark X1, X2) -> cons(X1, X2),
                           cons(active X1, X2) -> cons(X1, X2),
                                   from mark X -> from X,
                                 from active X -> from X,
                                      s mark X -> s X,
                                    s active X -> s X,
                            zWadr(X1, mark X2) -> zWadr(X1, X2),
                          zWadr(X1, active X2) -> zWadr(X1, X2),
                            zWadr(mark X1, X2) -> zWadr(X1, X2),
                          zWadr(active X1, X2) -> zWadr(X1, X2),
                                 prefix mark X -> prefix X,
                               prefix active X -> prefix X}
       Open
      
      SCC (4):
       Strict:
        {  app#(X1, mark X2) -> app#(X1, X2),
         app#(X1, active X2) -> app#(X1, X2),
           app#(mark X1, X2) -> app#(X1, X2),
         app#(active X1, X2) -> app#(X1, X2)}
       Weak:
       {                      mark app(X1, X2) -> active app(mark X1, mark X2),
                                    mark nil() -> active nil(),
                             mark cons(X1, X2) -> active cons(mark X1, X2),
                                   mark from X -> active from mark X,
                                      mark s X -> active s mark X,
                            mark zWadr(X1, X2) -> active zWadr(mark X1, mark X2),
                                 mark prefix X -> active prefix mark X,
                         active app(nil(), YS) -> mark YS,
                   active app(cons(X, XS), YS) -> mark cons(X, app(XS, YS)),
                                 active from X -> mark cons(X, from s X),
                       active zWadr(XS, nil()) -> mark nil(),
                       active zWadr(nil(), YS) -> mark nil(),
        active zWadr(cons(X, XS), cons(Y, YS)) -> mark cons(app(Y, cons(X, nil())), zWadr(XS, YS)),
                               active prefix L -> mark cons(nil(), zWadr(L, prefix L)),
                              app(X1, mark X2) -> app(X1, X2),
                            app(X1, active X2) -> app(X1, X2),
                              app(mark X1, X2) -> app(X1, X2),
                            app(active X1, X2) -> app(X1, X2),
                             cons(X1, mark X2) -> cons(X1, X2),
                           cons(X1, active X2) -> cons(X1, X2),
                             cons(mark X1, X2) -> cons(X1, X2),
                           cons(active X1, X2) -> cons(X1, X2),
                                   from mark X -> from X,
                                 from active X -> from X,
                                      s mark X -> s X,
                                    s active X -> s X,
                            zWadr(X1, mark X2) -> zWadr(X1, X2),
                          zWadr(X1, active X2) -> zWadr(X1, X2),
                            zWadr(mark X1, X2) -> zWadr(X1, X2),
                          zWadr(active X1, X2) -> zWadr(X1, X2),
                                 prefix mark X -> prefix X,
                               prefix active X -> prefix X}
       Open