YES
TRS:
 {           a__f(X) -> f(X),
           a__f(0()) -> cons(0(), f(s(0()))),
        a__f(s(0())) -> a__f(a__p(s(0()))),
             a__p(X) -> p(X),
        a__p(s(0())) -> 0(),
  mark(cons(X1, X2)) -> cons(mark(X1), X2),
           mark(0()) -> 0(),
          mark(f(X)) -> a__f(mark(X)),
          mark(s(X)) -> s(mark(X)),
          mark(p(X)) -> a__p(mark(X))}
 DP:
  Strict:
   {      a__f#(s(0())) -> a__f#(a__p(s(0()))),
          a__f#(s(0())) -> a__p#(s(0())),
    mark#(cons(X1, X2)) -> mark#(X1),
            mark#(f(X)) -> a__f#(mark(X)),
            mark#(f(X)) -> mark#(X),
            mark#(s(X)) -> mark#(X),
            mark#(p(X)) -> a__p#(mark(X)),
            mark#(p(X)) -> mark#(X)}
  Weak:
  {           a__f(X) -> f(X),
            a__f(0()) -> cons(0(), f(s(0()))),
         a__f(s(0())) -> a__f(a__p(s(0()))),
              a__p(X) -> p(X),
         a__p(s(0())) -> 0(),
   mark(cons(X1, X2)) -> cons(mark(X1), X2),
            mark(0()) -> 0(),
           mark(f(X)) -> a__f(mark(X)),
           mark(s(X)) -> s(mark(X)),
           mark(p(X)) -> a__p(mark(X))}
  EDG:
   {(mark#(cons(X1, X2)) -> mark#(X1), mark#(p(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(f(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(f(X)) -> a__f#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(f(X)) -> a__f#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (a__f#(s(0())) -> a__f#(a__p(s(0()))), a__f#(s(0())) -> a__p#(s(0())))
    (a__f#(s(0())) -> a__f#(a__p(s(0()))), a__f#(s(0())) -> a__f#(a__p(s(0()))))
    (mark#(p(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(p(X)) -> mark#(X), mark#(f(X)) -> a__f#(mark(X)))
    (mark#(p(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
    (mark#(p(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(p(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(p(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (mark#(f(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(f(X)) -> mark#(X), mark#(f(X)) -> a__f#(mark(X)))
    (mark#(f(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
    (mark#(f(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(f(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(f(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (mark#(f(X)) -> a__f#(mark(X)), a__f#(s(0())) -> a__f#(a__p(s(0()))))
    (mark#(f(X)) -> a__f#(mark(X)), a__f#(s(0())) -> a__p#(s(0())))}
   SCCS:
    Scc:
     {mark#(cons(X1, X2)) -> mark#(X1),
              mark#(f(X)) -> mark#(X),
              mark#(s(X)) -> mark#(X),
              mark#(p(X)) -> mark#(X)}
    Scc:
     {a__f#(s(0())) -> a__f#(a__p(s(0())))}
    SCC:
     Strict:
      {mark#(cons(X1, X2)) -> mark#(X1),
               mark#(f(X)) -> mark#(X),
               mark#(s(X)) -> mark#(X),
               mark#(p(X)) -> mark#(X)}
     Weak:
     {           a__f(X) -> f(X),
               a__f(0()) -> cons(0(), f(s(0()))),
            a__f(s(0())) -> a__f(a__p(s(0()))),
                 a__p(X) -> p(X),
            a__p(s(0())) -> 0(),
      mark(cons(X1, X2)) -> cons(mark(X1), X2),
               mark(0()) -> 0(),
              mark(f(X)) -> a__f(mark(X)),
              mark(s(X)) -> s(mark(X)),
              mark(p(X)) -> a__p(mark(X))}
     SPSC:
      Simple Projection:
       pi(mark#) = 0
      Strict:
       {mark#(cons(X1, X2)) -> mark#(X1),
                mark#(f(X)) -> mark#(X),
                mark#(p(X)) -> mark#(X)}
      EDG:
       {(mark#(f(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
        (mark#(f(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
        (mark#(f(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(p(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(p(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
        (mark#(p(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(f(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(p(X)) -> mark#(X))}
       SCCS:
        Scc:
         {mark#(cons(X1, X2)) -> mark#(X1),
                  mark#(f(X)) -> mark#(X),
                  mark#(p(X)) -> mark#(X)}
        SCC:
         Strict:
          {mark#(cons(X1, X2)) -> mark#(X1),
                   mark#(f(X)) -> mark#(X),
                   mark#(p(X)) -> mark#(X)}
         Weak:
         {           a__f(X) -> f(X),
                   a__f(0()) -> cons(0(), f(s(0()))),
                a__f(s(0())) -> a__f(a__p(s(0()))),
                     a__p(X) -> p(X),
                a__p(s(0())) -> 0(),
          mark(cons(X1, X2)) -> cons(mark(X1), X2),
                   mark(0()) -> 0(),
                  mark(f(X)) -> a__f(mark(X)),
                  mark(s(X)) -> s(mark(X)),
                  mark(p(X)) -> a__p(mark(X))}
         SPSC:
          Simple Projection:
           pi(mark#) = 0
          Strict:
           {mark#(cons(X1, X2)) -> mark#(X1),
                    mark#(f(X)) -> mark#(X)}
          EDG:
           {(mark#(cons(X1, X2)) -> mark#(X1), mark#(f(X)) -> mark#(X))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(f(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(f(X)) -> mark#(X), mark#(f(X)) -> mark#(X))}
           SCCS:
            Scc:
             {mark#(cons(X1, X2)) -> mark#(X1),
                      mark#(f(X)) -> mark#(X)}
            SCC:
             Strict:
              {mark#(cons(X1, X2)) -> mark#(X1),
                       mark#(f(X)) -> mark#(X)}
             Weak:
             {           a__f(X) -> f(X),
                       a__f(0()) -> cons(0(), f(s(0()))),
                    a__f(s(0())) -> a__f(a__p(s(0()))),
                         a__p(X) -> p(X),
                    a__p(s(0())) -> 0(),
              mark(cons(X1, X2)) -> cons(mark(X1), X2),
                       mark(0()) -> 0(),
                      mark(f(X)) -> a__f(mark(X)),
                      mark(s(X)) -> s(mark(X)),
                      mark(p(X)) -> a__p(mark(X))}
             SPSC:
              Simple Projection:
               pi(mark#) = 0
              Strict:
               {mark#(f(X)) -> mark#(X)}
              EDG:
               {(mark#(f(X)) -> mark#(X), mark#(f(X)) -> mark#(X))}
               SCCS:
                Scc:
                 {mark#(f(X)) -> mark#(X)}
                SCC:
                 Strict:
                  {mark#(f(X)) -> mark#(X)}
                 Weak:
                 {           a__f(X) -> f(X),
                           a__f(0()) -> cons(0(), f(s(0()))),
                        a__f(s(0())) -> a__f(a__p(s(0()))),
                             a__p(X) -> p(X),
                        a__p(s(0())) -> 0(),
                  mark(cons(X1, X2)) -> cons(mark(X1), X2),
                           mark(0()) -> 0(),
                          mark(f(X)) -> a__f(mark(X)),
                          mark(s(X)) -> s(mark(X)),
                          mark(p(X)) -> a__p(mark(X))}
                 SPSC:
                  Simple Projection:
                   pi(mark#) = 0
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {a__f#(s(0())) -> a__f#(a__p(s(0())))}
     Weak:
     {           a__f(X) -> f(X),
               a__f(0()) -> cons(0(), f(s(0()))),
            a__f(s(0())) -> a__f(a__p(s(0()))),
                 a__p(X) -> p(X),
            a__p(s(0())) -> 0(),
      mark(cons(X1, X2)) -> cons(mark(X1), X2),
               mark(0()) -> 0(),
              mark(f(X)) -> a__f(mark(X)),
              mark(s(X)) -> s(mark(X)),
              mark(p(X)) -> a__p(mark(X))}
     POLY:
      Argument Filtering:
       pi(p) = [], pi(mark) = [], pi(a__p) = [], pi(a__f#) = 0, pi(a__f) = [], pi(s) = [], pi(f) = [], pi(0) = [], pi(cons) = []
      Usable Rules:
       {}
      Interpretation:
       [a__p] = 0,
       [s] = 1
      Strict:
       {}
      Weak:
       {           a__f(X) -> f(X),
                 a__f(0()) -> cons(0(), f(s(0()))),
              a__f(s(0())) -> a__f(a__p(s(0()))),
                   a__p(X) -> p(X),
              a__p(s(0())) -> 0(),
        mark(cons(X1, X2)) -> cons(mark(X1), X2),
                 mark(0()) -> 0(),
                mark(f(X)) -> a__f(mark(X)),
                mark(s(X)) -> s(mark(X)),
                mark(p(X)) -> a__p(mark(X))}
      Qed