MAYBE
Time: 0.553876
TRS:
 {                        mark nil() -> nil(),
                   mark cons(X1, X2) -> cons(mark X1, X2),
                    mark app(X1, X2) -> a__app(mark X1, mark X2),
                         mark from X -> a__from mark X,
                            mark s X -> s mark X,
                  mark zWadr(X1, X2) -> a__zWadr(mark X1, mark X2),
                       mark prefix X -> a__prefix mark X,
                      a__app(X1, X2) -> app(X1, X2),
                   a__app(nil(), YS) -> mark YS,
             a__app(cons(X, XS), YS) -> cons(mark X, app(XS, YS)),
                           a__from X -> cons(mark X, from s X),
                           a__from X -> from X,
                 a__zWadr(XS, nil()) -> nil(),
                    a__zWadr(X1, X2) -> zWadr(X1, X2),
                 a__zWadr(nil(), YS) -> nil(),
  a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark Y, cons(mark X, nil())), zWadr(XS, YS)),
                         a__prefix X -> prefix X,
                         a__prefix L -> cons(nil(), zWadr(L, prefix L))}
 DP:
  DP:
   {                 mark# cons(X1, X2) -> mark# X1,
                      mark# app(X1, X2) -> mark# X1,
                      mark# app(X1, X2) -> mark# X2,
                      mark# app(X1, X2) -> a__app#(mark X1, mark X2),
                           mark# from X -> mark# X,
                           mark# from X -> a__from# mark X,
                              mark# s X -> mark# X,
                    mark# zWadr(X1, X2) -> mark# X1,
                    mark# zWadr(X1, X2) -> mark# X2,
                    mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2),
                         mark# prefix X -> mark# X,
                         mark# prefix X -> a__prefix# mark X,
                     a__app#(nil(), YS) -> mark# YS,
               a__app#(cons(X, XS), YS) -> mark# X,
                             a__from# X -> mark# X,
    a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X,
    a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y,
    a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil()))}
  TRS:
  {                        mark nil() -> nil(),
                    mark cons(X1, X2) -> cons(mark X1, X2),
                     mark app(X1, X2) -> a__app(mark X1, mark X2),
                          mark from X -> a__from mark X,
                             mark s X -> s mark X,
                   mark zWadr(X1, X2) -> a__zWadr(mark X1, mark X2),
                        mark prefix X -> a__prefix mark X,
                       a__app(X1, X2) -> app(X1, X2),
                    a__app(nil(), YS) -> mark YS,
              a__app(cons(X, XS), YS) -> cons(mark X, app(XS, YS)),
                            a__from X -> cons(mark X, from s X),
                            a__from X -> from X,
                  a__zWadr(XS, nil()) -> nil(),
                     a__zWadr(X1, X2) -> zWadr(X1, X2),
                  a__zWadr(nil(), YS) -> nil(),
   a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark Y, cons(mark X, nil())), zWadr(XS, YS)),
                          a__prefix X -> prefix X,
                          a__prefix L -> cons(nil(), zWadr(L, prefix L))}
  UR:
   {                        mark nil() -> nil(),
                     mark cons(X1, X2) -> cons(mark X1, X2),
                      mark app(X1, X2) -> a__app(mark X1, mark X2),
                           mark from X -> a__from mark X,
                              mark s X -> s mark X,
                    mark zWadr(X1, X2) -> a__zWadr(mark X1, mark X2),
                         mark prefix X -> a__prefix mark X,
                        a__app(X1, X2) -> app(X1, X2),
                     a__app(nil(), YS) -> mark YS,
               a__app(cons(X, XS), YS) -> cons(mark X, app(XS, YS)),
                             a__from X -> cons(mark X, from s X),
                             a__from X -> from X,
                   a__zWadr(XS, nil()) -> nil(),
                      a__zWadr(X1, X2) -> zWadr(X1, X2),
                   a__zWadr(nil(), YS) -> nil(),
    a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark Y, cons(mark X, nil())), zWadr(XS, YS)),
                           a__prefix X -> prefix X,
                           a__prefix L -> cons(nil(), zWadr(L, prefix L))}
   EDG:
    {
     (mark# from X -> mark# X, mark# prefix X -> a__prefix# mark X)
     (mark# from X -> mark# X, mark# prefix X -> mark# X)
     (mark# from X -> mark# X, mark# zWadr(X1, X2) -> a__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 -> mark# X)
     (mark# from X -> mark# X, mark# from X -> a__from# mark X)
     (mark# from X -> mark# X, mark# from X -> mark# X)
     (mark# from X -> mark# X, mark# app(X1, X2) -> a__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# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# prefix X -> mark# X, mark# prefix X -> a__prefix# mark X)
     (mark# prefix X -> mark# X, mark# prefix X -> mark# X)
     (mark# prefix X -> mark# X, mark# zWadr(X1, X2) -> a__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 -> mark# X)
     (mark# prefix X -> mark# X, mark# from X -> a__from# mark X)
     (mark# prefix X -> mark# X, mark# from X -> mark# X)
     (mark# prefix X -> mark# X, mark# app(X1, X2) -> a__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)
     (mark# prefix X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__from# X -> mark# X, mark# prefix X -> a__prefix# mark X)
     (a__from# X -> mark# X, mark# prefix X -> mark# X)
     (a__from# X -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
     (a__from# X -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
     (a__from# X -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
     (a__from# X -> mark# X, mark# s X -> mark# X)
     (a__from# X -> mark# X, mark# from X -> a__from# mark X)
     (a__from# X -> mark# X, mark# from X -> mark# X)
     (a__from# X -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
     (a__from# X -> mark# X, mark# app(X1, X2) -> mark# X2)
     (a__from# X -> mark# X, mark# app(X1, X2) -> mark# X1)
     (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# app(X1, X2) -> mark# X2, mark# prefix X -> a__prefix# mark X)
     (mark# app(X1, X2) -> mark# X2, mark# prefix X -> mark# X)
     (mark# app(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> a__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 -> mark# X)
     (mark# app(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
     (mark# app(X1, X2) -> mark# X2, mark# from X -> mark# X)
     (mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> a__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)
     (mark# app(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (mark# app(X1, X2) -> a__app#(mark X1, mark X2), a__app#(cons(X, XS), YS) -> mark# X)
     (mark# app(X1, X2) -> a__app#(mark X1, mark X2), a__app#(nil(), YS) -> mark# YS)
     (a__app#(nil(), YS) -> mark# YS, mark# prefix X -> a__prefix# mark X)
     (a__app#(nil(), YS) -> mark# YS, mark# prefix X -> mark# X)
     (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
     (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> mark# X2)
     (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> mark# X1)
     (a__app#(nil(), YS) -> mark# YS, mark# s X -> mark# X)
     (a__app#(nil(), YS) -> mark# YS, mark# from X -> a__from# mark X)
     (a__app#(nil(), YS) -> mark# YS, mark# from X -> mark# X)
     (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
     (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> mark# X2)
     (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> mark# X1)
     (a__app#(nil(), YS) -> mark# YS, mark# cons(X1, X2) -> mark# X1)
     (mark# app(X1, X2) -> mark# X1, mark# prefix X -> a__prefix# mark X)
     (mark# app(X1, X2) -> mark# X1, mark# prefix X -> mark# X)
     (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
     (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2)
     (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X1)
     (mark# app(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# app(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
     (mark# app(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
     (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2)
     (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1)
     (mark# app(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# prefix X -> a__prefix# mark X)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# prefix X -> mark# X)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> mark# X2)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> mark# X1)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# s X -> mark# X)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# from X -> a__from# mark X)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# from X -> mark# X)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> mark# X2)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> mark# X1)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# cons(X1, X2) -> mark# X1)
     (mark# zWadr(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (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) -> a__app#(mark X1, mark X2))
     (mark# zWadr(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# zWadr(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
     (mark# zWadr(X1, X2) -> mark# X1, mark# s X -> 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) -> a__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 -> a__prefix# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# prefix X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# prefix X -> a__prefix# mark X)
     (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X)
     (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y)
     (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())))
     (mark# zWadr(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (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) -> a__app#(mark X1, mark X2))
     (mark# zWadr(X1, X2) -> mark# X2, mark# from X -> mark# X)
     (mark# zWadr(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
     (mark# zWadr(X1, X2) -> mark# X2, mark# s X -> 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) -> a__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 -> a__prefix# mark X)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> mark# X1)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> mark# X2)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# from X -> mark# X)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# from X -> a__from# mark X)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# s X -> mark# X)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# prefix X -> mark# X)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# prefix X -> a__prefix# mark X)
     (a__app#(cons(X, XS), YS) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> mark# X1)
     (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> mark# X2)
     (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
     (a__app#(cons(X, XS), YS) -> mark# X, mark# from X -> mark# X)
     (a__app#(cons(X, XS), YS) -> mark# X, mark# from X -> a__from# mark X)
     (a__app#(cons(X, XS), YS) -> mark# X, mark# s X -> mark# X)
     (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
     (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
     (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
     (a__app#(cons(X, XS), YS) -> mark# X, mark# prefix X -> mark# X)
     (a__app#(cons(X, XS), YS) -> mark# X, mark# prefix X -> a__prefix# mark X)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (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) -> a__app#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# from X -> mark# X)
     (mark# s X -> mark# X, mark# from X -> a__from# mark X)
     (mark# s X -> mark# X, mark# s X -> 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) -> a__zWadr#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# prefix X -> mark# X)
     (mark# s X -> mark# X, mark# prefix X -> a__prefix# mark X)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())), a__app#(nil(), YS) -> mark# YS)
     (a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())), a__app#(cons(X, XS), YS) -> mark# X)
     (mark# from X -> a__from# mark X, a__from# X -> mark# X)
    }
    EDG:
     {
      (mark# from X -> mark# X, mark# prefix X -> a__prefix# mark X)
      (mark# from X -> mark# X, mark# prefix X -> mark# X)
      (mark# from X -> mark# X, mark# zWadr(X1, X2) -> a__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 -> mark# X)
      (mark# from X -> mark# X, mark# from X -> a__from# mark X)
      (mark# from X -> mark# X, mark# from X -> mark# X)
      (mark# from X -> mark# X, mark# app(X1, X2) -> a__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# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# prefix X -> mark# X, mark# prefix X -> a__prefix# mark X)
      (mark# prefix X -> mark# X, mark# prefix X -> mark# X)
      (mark# prefix X -> mark# X, mark# zWadr(X1, X2) -> a__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 -> mark# X)
      (mark# prefix X -> mark# X, mark# from X -> a__from# mark X)
      (mark# prefix X -> mark# X, mark# from X -> mark# X)
      (mark# prefix X -> mark# X, mark# app(X1, X2) -> a__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)
      (mark# prefix X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (a__from# X -> mark# X, mark# prefix X -> a__prefix# mark X)
      (a__from# X -> mark# X, mark# prefix X -> mark# X)
      (a__from# X -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
      (a__from# X -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
      (a__from# X -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
      (a__from# X -> mark# X, mark# s X -> mark# X)
      (a__from# X -> mark# X, mark# from X -> a__from# mark X)
      (a__from# X -> mark# X, mark# from X -> mark# X)
      (a__from# X -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
      (a__from# X -> mark# X, mark# app(X1, X2) -> mark# X2)
      (a__from# X -> mark# X, mark# app(X1, X2) -> mark# X1)
      (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# app(X1, X2) -> mark# X2, mark# prefix X -> a__prefix# mark X)
      (mark# app(X1, X2) -> mark# X2, mark# prefix X -> mark# X)
      (mark# app(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> a__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 -> mark# X)
      (mark# app(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
      (mark# app(X1, X2) -> mark# X2, mark# from X -> mark# X)
      (mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> a__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)
      (mark# app(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
      (mark# app(X1, X2) -> a__app#(mark X1, mark X2), a__app#(cons(X, XS), YS) -> mark# X)
      (mark# app(X1, X2) -> a__app#(mark X1, mark X2), a__app#(nil(), YS) -> mark# YS)
      (a__app#(nil(), YS) -> mark# YS, mark# prefix X -> a__prefix# mark X)
      (a__app#(nil(), YS) -> mark# YS, mark# prefix X -> mark# X)
      (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
      (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> mark# X2)
      (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> mark# X1)
      (a__app#(nil(), YS) -> mark# YS, mark# s X -> mark# X)
      (a__app#(nil(), YS) -> mark# YS, mark# from X -> a__from# mark X)
      (a__app#(nil(), YS) -> mark# YS, mark# from X -> mark# X)
      (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
      (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> mark# X2)
      (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> mark# X1)
      (a__app#(nil(), YS) -> mark# YS, mark# cons(X1, X2) -> mark# X1)
      (mark# app(X1, X2) -> mark# X1, mark# prefix X -> a__prefix# mark X)
      (mark# app(X1, X2) -> mark# X1, mark# prefix X -> mark# X)
      (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
      (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2)
      (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X1)
      (mark# app(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# app(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
      (mark# app(X1, X2) -> mark# X1, mark# from X -> mark# X)
      (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
      (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2)
      (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1)
      (mark# app(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# prefix X -> a__prefix# mark X)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# prefix X -> mark# X)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> mark# X2)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> mark# X1)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# s X -> mark# X)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# from X -> a__from# mark X)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# from X -> mark# X)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> mark# X2)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> mark# X1)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# cons(X1, X2) -> mark# X1)
      (mark# zWadr(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (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) -> a__app#(mark X1, mark X2))
      (mark# zWadr(X1, X2) -> mark# X1, mark# from X -> mark# X)
      (mark# zWadr(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
      (mark# zWadr(X1, X2) -> mark# X1, mark# s X -> 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) -> a__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 -> a__prefix# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2)
      (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
      (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2)
      (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
      (mark# cons(X1, X2) -> mark# X1, mark# prefix X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# prefix X -> a__prefix# mark X)
      (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X)
      (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y)
      (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())))
      (mark# zWadr(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
      (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) -> a__app#(mark X1, mark X2))
      (mark# zWadr(X1, X2) -> mark# X2, mark# from X -> mark# X)
      (mark# zWadr(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
      (mark# zWadr(X1, X2) -> mark# X2, mark# s X -> 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) -> a__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 -> a__prefix# mark X)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> mark# X1)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> mark# X2)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# from X -> mark# X)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# from X -> a__from# mark X)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# s X -> mark# X)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# prefix X -> mark# X)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# prefix X -> a__prefix# mark X)
      (a__app#(cons(X, XS), YS) -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> mark# X1)
      (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> mark# X2)
      (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
      (a__app#(cons(X, XS), YS) -> mark# X, mark# from X -> mark# X)
      (a__app#(cons(X, XS), YS) -> mark# X, mark# from X -> a__from# mark X)
      (a__app#(cons(X, XS), YS) -> mark# X, mark# s X -> mark# X)
      (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
      (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
      (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
      (a__app#(cons(X, XS), YS) -> mark# X, mark# prefix X -> mark# X)
      (a__app#(cons(X, XS), YS) -> mark# X, mark# prefix X -> a__prefix# mark X)
      (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (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) -> a__app#(mark X1, mark X2))
      (mark# s X -> mark# X, mark# from X -> mark# X)
      (mark# s X -> mark# X, mark# from X -> a__from# mark X)
      (mark# s X -> mark# X, mark# s X -> 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) -> a__zWadr#(mark X1, mark X2))
      (mark# s X -> mark# X, mark# prefix X -> mark# X)
      (mark# s X -> mark# X, mark# prefix X -> a__prefix# mark X)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())), a__app#(nil(), YS) -> mark# YS)
      (a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())), a__app#(cons(X, XS), YS) -> mark# X)
      (mark# from X -> a__from# mark X, a__from# X -> mark# X)
     }
     EDG:
      {
       (mark# from X -> mark# X, mark# prefix X -> a__prefix# mark X)
       (mark# from X -> mark# X, mark# prefix X -> mark# X)
       (mark# from X -> mark# X, mark# zWadr(X1, X2) -> a__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 -> mark# X)
       (mark# from X -> mark# X, mark# from X -> a__from# mark X)
       (mark# from X -> mark# X, mark# from X -> mark# X)
       (mark# from X -> mark# X, mark# app(X1, X2) -> a__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# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# prefix X -> mark# X, mark# prefix X -> a__prefix# mark X)
       (mark# prefix X -> mark# X, mark# prefix X -> mark# X)
       (mark# prefix X -> mark# X, mark# zWadr(X1, X2) -> a__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 -> mark# X)
       (mark# prefix X -> mark# X, mark# from X -> a__from# mark X)
       (mark# prefix X -> mark# X, mark# from X -> mark# X)
       (mark# prefix X -> mark# X, mark# app(X1, X2) -> a__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)
       (mark# prefix X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (a__from# X -> mark# X, mark# prefix X -> a__prefix# mark X)
       (a__from# X -> mark# X, mark# prefix X -> mark# X)
       (a__from# X -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
       (a__from# X -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
       (a__from# X -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
       (a__from# X -> mark# X, mark# s X -> mark# X)
       (a__from# X -> mark# X, mark# from X -> a__from# mark X)
       (a__from# X -> mark# X, mark# from X -> mark# X)
       (a__from# X -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
       (a__from# X -> mark# X, mark# app(X1, X2) -> mark# X2)
       (a__from# X -> mark# X, mark# app(X1, X2) -> mark# X1)
       (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# app(X1, X2) -> mark# X2, mark# prefix X -> a__prefix# mark X)
       (mark# app(X1, X2) -> mark# X2, mark# prefix X -> mark# X)
       (mark# app(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> a__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 -> mark# X)
       (mark# app(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
       (mark# app(X1, X2) -> mark# X2, mark# from X -> mark# X)
       (mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> a__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)
       (mark# app(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
       (mark# app(X1, X2) -> a__app#(mark X1, mark X2), a__app#(cons(X, XS), YS) -> mark# X)
       (mark# app(X1, X2) -> a__app#(mark X1, mark X2), a__app#(nil(), YS) -> mark# YS)
       (a__app#(nil(), YS) -> mark# YS, mark# prefix X -> a__prefix# mark X)
       (a__app#(nil(), YS) -> mark# YS, mark# prefix X -> mark# X)
       (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
       (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> mark# X2)
       (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> mark# X1)
       (a__app#(nil(), YS) -> mark# YS, mark# s X -> mark# X)
       (a__app#(nil(), YS) -> mark# YS, mark# from X -> a__from# mark X)
       (a__app#(nil(), YS) -> mark# YS, mark# from X -> mark# X)
       (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
       (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> mark# X2)
       (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> mark# X1)
       (a__app#(nil(), YS) -> mark# YS, mark# cons(X1, X2) -> mark# X1)
       (mark# app(X1, X2) -> mark# X1, mark# prefix X -> a__prefix# mark X)
       (mark# app(X1, X2) -> mark# X1, mark# prefix X -> mark# X)
       (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
       (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2)
       (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X1)
       (mark# app(X1, X2) -> mark# X1, mark# s X -> mark# X)
       (mark# app(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
       (mark# app(X1, X2) -> mark# X1, mark# from X -> mark# X)
       (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
       (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2)
       (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1)
       (mark# app(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# prefix X -> a__prefix# mark X)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# prefix X -> mark# X)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> mark# X2)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> mark# X1)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# s X -> mark# X)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# from X -> a__from# mark X)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# from X -> mark# X)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> mark# X2)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> mark# X1)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# cons(X1, X2) -> mark# X1)
       (mark# zWadr(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
       (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) -> a__app#(mark X1, mark X2))
       (mark# zWadr(X1, X2) -> mark# X1, mark# from X -> mark# X)
       (mark# zWadr(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
       (mark# zWadr(X1, X2) -> mark# X1, mark# s X -> 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) -> a__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 -> a__prefix# mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
       (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1)
       (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2)
       (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
       (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X1)
       (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2)
       (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
       (mark# cons(X1, X2) -> mark# X1, mark# prefix X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# prefix X -> a__prefix# mark X)
       (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X)
       (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y)
       (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())))
       (mark# zWadr(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
       (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) -> a__app#(mark X1, mark X2))
       (mark# zWadr(X1, X2) -> mark# X2, mark# from X -> mark# X)
       (mark# zWadr(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
       (mark# zWadr(X1, X2) -> mark# X2, mark# s X -> 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) -> a__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 -> a__prefix# mark X)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> mark# X1)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> mark# X2)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# from X -> mark# X)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# from X -> a__from# mark X)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# s X -> mark# X)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# prefix X -> mark# X)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# prefix X -> a__prefix# mark X)
       (a__app#(cons(X, XS), YS) -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> mark# X1)
       (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> mark# X2)
       (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
       (a__app#(cons(X, XS), YS) -> mark# X, mark# from X -> mark# X)
       (a__app#(cons(X, XS), YS) -> mark# X, mark# from X -> a__from# mark X)
       (a__app#(cons(X, XS), YS) -> mark# X, mark# s X -> mark# X)
       (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
       (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
       (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
       (a__app#(cons(X, XS), YS) -> mark# X, mark# prefix X -> mark# X)
       (a__app#(cons(X, XS), YS) -> mark# X, mark# prefix X -> a__prefix# mark X)
       (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (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) -> a__app#(mark X1, mark X2))
       (mark# s X -> mark# X, mark# from X -> mark# X)
       (mark# s X -> mark# X, mark# from X -> a__from# mark X)
       (mark# s X -> mark# X, mark# s X -> 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) -> a__zWadr#(mark X1, mark X2))
       (mark# s X -> mark# X, mark# prefix X -> mark# X)
       (mark# s X -> mark# X, mark# prefix X -> a__prefix# mark X)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())), a__app#(nil(), YS) -> mark# YS)
       (a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())), a__app#(cons(X, XS), YS) -> mark# X)
       (mark# from X -> a__from# mark X, a__from# X -> mark# X)
      }
      EDG:
       {
        (mark# from X -> mark# X, mark# prefix X -> a__prefix# mark X)
        (mark# from X -> mark# X, mark# prefix X -> mark# X)
        (mark# from X -> mark# X, mark# zWadr(X1, X2) -> a__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 -> mark# X)
        (mark# from X -> mark# X, mark# from X -> a__from# mark X)
        (mark# from X -> mark# X, mark# from X -> mark# X)
        (mark# from X -> mark# X, mark# app(X1, X2) -> a__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# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (mark# prefix X -> mark# X, mark# prefix X -> a__prefix# mark X)
        (mark# prefix X -> mark# X, mark# prefix X -> mark# X)
        (mark# prefix X -> mark# X, mark# zWadr(X1, X2) -> a__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 -> mark# X)
        (mark# prefix X -> mark# X, mark# from X -> a__from# mark X)
        (mark# prefix X -> mark# X, mark# from X -> mark# X)
        (mark# prefix X -> mark# X, mark# app(X1, X2) -> a__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)
        (mark# prefix X -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (a__from# X -> mark# X, mark# prefix X -> a__prefix# mark X)
        (a__from# X -> mark# X, mark# prefix X -> mark# X)
        (a__from# X -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
        (a__from# X -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
        (a__from# X -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
        (a__from# X -> mark# X, mark# s X -> mark# X)
        (a__from# X -> mark# X, mark# from X -> a__from# mark X)
        (a__from# X -> mark# X, mark# from X -> mark# X)
        (a__from# X -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
        (a__from# X -> mark# X, mark# app(X1, X2) -> mark# X2)
        (a__from# X -> mark# X, mark# app(X1, X2) -> mark# X1)
        (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (mark# app(X1, X2) -> mark# X2, mark# prefix X -> a__prefix# mark X)
        (mark# app(X1, X2) -> mark# X2, mark# prefix X -> mark# X)
        (mark# app(X1, X2) -> mark# X2, mark# zWadr(X1, X2) -> a__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 -> mark# X)
        (mark# app(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
        (mark# app(X1, X2) -> mark# X2, mark# from X -> mark# X)
        (mark# app(X1, X2) -> mark# X2, mark# app(X1, X2) -> a__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)
        (mark# app(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
        (mark# app(X1, X2) -> a__app#(mark X1, mark X2), a__app#(cons(X, XS), YS) -> mark# X)
        (mark# app(X1, X2) -> a__app#(mark X1, mark X2), a__app#(nil(), YS) -> mark# YS)
        (a__app#(nil(), YS) -> mark# YS, mark# prefix X -> a__prefix# mark X)
        (a__app#(nil(), YS) -> mark# YS, mark# prefix X -> mark# X)
        (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
        (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> mark# X2)
        (a__app#(nil(), YS) -> mark# YS, mark# zWadr(X1, X2) -> mark# X1)
        (a__app#(nil(), YS) -> mark# YS, mark# s X -> mark# X)
        (a__app#(nil(), YS) -> mark# YS, mark# from X -> a__from# mark X)
        (a__app#(nil(), YS) -> mark# YS, mark# from X -> mark# X)
        (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
        (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> mark# X2)
        (a__app#(nil(), YS) -> mark# YS, mark# app(X1, X2) -> mark# X1)
        (a__app#(nil(), YS) -> mark# YS, mark# cons(X1, X2) -> mark# X1)
        (mark# app(X1, X2) -> mark# X1, mark# prefix X -> a__prefix# mark X)
        (mark# app(X1, X2) -> mark# X1, mark# prefix X -> mark# X)
        (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
        (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2)
        (mark# app(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X1)
        (mark# app(X1, X2) -> mark# X1, mark# s X -> mark# X)
        (mark# app(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
        (mark# app(X1, X2) -> mark# X1, mark# from X -> mark# X)
        (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
        (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2)
        (mark# app(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1)
        (mark# app(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# prefix X -> a__prefix# mark X)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# prefix X -> mark# X)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> mark# X2)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWadr(X1, X2) -> mark# X1)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# s X -> mark# X)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# from X -> a__from# mark X)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# from X -> mark# X)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> mark# X2)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# app(X1, X2) -> mark# X1)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# cons(X1, X2) -> mark# X1)
        (mark# zWadr(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
        (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) -> a__app#(mark X1, mark X2))
        (mark# zWadr(X1, X2) -> mark# X1, mark# from X -> mark# X)
        (mark# zWadr(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
        (mark# zWadr(X1, X2) -> mark# X1, mark# s X -> 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) -> a__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 -> a__prefix# mark X)
        (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
        (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X1)
        (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> mark# X2)
        (mark# cons(X1, X2) -> mark# X1, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
        (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
        (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X)
        (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
        (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X1)
        (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> mark# X2)
        (mark# cons(X1, X2) -> mark# X1, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
        (mark# cons(X1, X2) -> mark# X1, mark# prefix X -> mark# X)
        (mark# cons(X1, X2) -> mark# X1, mark# prefix X -> a__prefix# mark X)
        (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X)
        (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y)
        (mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2), a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())))
        (mark# zWadr(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
        (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) -> a__app#(mark X1, mark X2))
        (mark# zWadr(X1, X2) -> mark# X2, mark# from X -> mark# X)
        (mark# zWadr(X1, X2) -> mark# X2, mark# from X -> a__from# mark X)
        (mark# zWadr(X1, X2) -> mark# X2, mark# s X -> 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) -> a__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 -> a__prefix# mark X)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> mark# X1)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> mark# X2)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# from X -> mark# X)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# from X -> a__from# mark X)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# s X -> mark# X)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# prefix X -> mark# X)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# prefix X -> a__prefix# mark X)
        (a__app#(cons(X, XS), YS) -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> mark# X1)
        (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> mark# X2)
        (a__app#(cons(X, XS), YS) -> mark# X, mark# app(X1, X2) -> a__app#(mark X1, mark X2))
        (a__app#(cons(X, XS), YS) -> mark# X, mark# from X -> mark# X)
        (a__app#(cons(X, XS), YS) -> mark# X, mark# from X -> a__from# mark X)
        (a__app#(cons(X, XS), YS) -> mark# X, mark# s X -> mark# X)
        (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> mark# X1)
        (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> mark# X2)
        (a__app#(cons(X, XS), YS) -> mark# X, mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2))
        (a__app#(cons(X, XS), YS) -> mark# X, mark# prefix X -> mark# X)
        (a__app#(cons(X, XS), YS) -> mark# X, mark# prefix X -> a__prefix# mark X)
        (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (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) -> a__app#(mark X1, mark X2))
        (mark# s X -> mark# X, mark# from X -> mark# X)
        (mark# s X -> mark# X, mark# from X -> a__from# mark X)
        (mark# s X -> mark# X, mark# s X -> 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) -> a__zWadr#(mark X1, mark X2))
        (mark# s X -> mark# X, mark# prefix X -> mark# X)
        (mark# s X -> mark# X, mark# prefix X -> a__prefix# mark X)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())), a__app#(nil(), YS) -> mark# YS)
        (a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil())), a__app#(cons(X, XS), YS) -> mark# X)
        (mark# from X -> a__from# mark X, a__from# X -> mark# X)
       }
       STATUS:
        arrows: 0.493827
        SCCS (1):
         Scc:
          {                 mark# cons(X1, X2) -> mark# X1,
                             mark# app(X1, X2) -> mark# X1,
                             mark# app(X1, X2) -> mark# X2,
                             mark# app(X1, X2) -> a__app#(mark X1, mark X2),
                                  mark# from X -> mark# X,
                                  mark# from X -> a__from# mark X,
                                     mark# s X -> mark# X,
                           mark# zWadr(X1, X2) -> mark# X1,
                           mark# zWadr(X1, X2) -> mark# X2,
                           mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2),
                                mark# prefix X -> mark# X,
                            a__app#(nil(), YS) -> mark# YS,
                      a__app#(cons(X, XS), YS) -> mark# X,
                                    a__from# X -> mark# X,
           a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X,
           a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y,
           a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil()))}
         
         SCC (17):
          Strict:
           {                 mark# cons(X1, X2) -> mark# X1,
                              mark# app(X1, X2) -> mark# X1,
                              mark# app(X1, X2) -> mark# X2,
                              mark# app(X1, X2) -> a__app#(mark X1, mark X2),
                                   mark# from X -> mark# X,
                                   mark# from X -> a__from# mark X,
                                      mark# s X -> mark# X,
                            mark# zWadr(X1, X2) -> mark# X1,
                            mark# zWadr(X1, X2) -> mark# X2,
                            mark# zWadr(X1, X2) -> a__zWadr#(mark X1, mark X2),
                                 mark# prefix X -> mark# X,
                             a__app#(nil(), YS) -> mark# YS,
                       a__app#(cons(X, XS), YS) -> mark# X,
                                     a__from# X -> mark# X,
            a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# X,
            a__zWadr#(cons(X, XS), cons(Y, YS)) -> mark# Y,
            a__zWadr#(cons(X, XS), cons(Y, YS)) -> a__app#(mark Y, cons(mark X, nil()))}
          Weak:
          {                        mark nil() -> nil(),
                            mark cons(X1, X2) -> cons(mark X1, X2),
                             mark app(X1, X2) -> a__app(mark X1, mark X2),
                                  mark from X -> a__from mark X,
                                     mark s X -> s mark X,
                           mark zWadr(X1, X2) -> a__zWadr(mark X1, mark X2),
                                mark prefix X -> a__prefix mark X,
                               a__app(X1, X2) -> app(X1, X2),
                            a__app(nil(), YS) -> mark YS,
                      a__app(cons(X, XS), YS) -> cons(mark X, app(XS, YS)),
                                    a__from X -> cons(mark X, from s X),
                                    a__from X -> from X,
                          a__zWadr(XS, nil()) -> nil(),
                             a__zWadr(X1, X2) -> zWadr(X1, X2),
                          a__zWadr(nil(), YS) -> nil(),
           a__zWadr(cons(X, XS), cons(Y, YS)) -> cons(a__app(mark Y, cons(mark X, nil())), zWadr(XS, YS)),
                                  a__prefix X -> prefix X,
                                  a__prefix L -> cons(nil(), zWadr(L, prefix L))}
          Open