YES
TRS:
 {plus(x, s(s(y))) -> s(plus(s(x), y)),
  plus(s(s(x)), y) -> s(plus(x, s(y))),
   plus(s(0()), y) -> s(y),
      plus(0(), y) -> y,
   ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y))),
    ack(s(x), 0()) -> ack(x, s(0())),
       ack(0(), y) -> s(y)}
 DP:
  Strict:
   {plus#(x, s(s(y))) -> plus#(s(x), y),
    plus#(s(s(x)), y) -> plus#(x, s(y)),
     ack#(s(x), s(y)) -> plus#(y, ack(s(x), y)),
     ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))),
     ack#(s(x), s(y)) -> ack#(s(x), y),
      ack#(s(x), 0()) -> ack#(x, s(0()))}
  Weak:
  {plus(x, s(s(y))) -> s(plus(s(x), y)),
   plus(s(s(x)), y) -> s(plus(x, s(y))),
    plus(s(0()), y) -> s(y),
       plus(0(), y) -> y,
    ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y))),
     ack(s(x), 0()) -> ack(x, s(0())),
        ack(0(), y) -> s(y)}
  EDG:
   {(ack#(s(x), 0()) -> ack#(x, s(0())), ack#(s(x), s(y)) -> ack#(s(x), y))
    (ack#(s(x), 0()) -> ack#(x, s(0())), ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))))
    (ack#(s(x), 0()) -> ack#(x, s(0())), ack#(s(x), s(y)) -> plus#(y, ack(s(x), y)))
    (ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))), ack#(s(x), 0()) -> ack#(x, s(0())))
    (ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))), ack#(s(x), s(y)) -> ack#(s(x), y))
    (ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))), ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))))
    (ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))), ack#(s(x), s(y)) -> plus#(y, ack(s(x), y)))
    (ack#(s(x), s(y)) -> ack#(s(x), y), ack#(s(x), 0()) -> ack#(x, s(0())))
    (ack#(s(x), s(y)) -> ack#(s(x), y), ack#(s(x), s(y)) -> ack#(s(x), y))
    (ack#(s(x), s(y)) -> ack#(s(x), y), ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))))
    (ack#(s(x), s(y)) -> ack#(s(x), y), ack#(s(x), s(y)) -> plus#(y, ack(s(x), y)))
    (plus#(x, s(s(y))) -> plus#(s(x), y), plus#(x, s(s(y))) -> plus#(s(x), y))
    (plus#(x, s(s(y))) -> plus#(s(x), y), plus#(s(s(x)), y) -> plus#(x, s(y)))
    (plus#(s(s(x)), y) -> plus#(x, s(y)), plus#(x, s(s(y))) -> plus#(s(x), y))
    (plus#(s(s(x)), y) -> plus#(x, s(y)), plus#(s(s(x)), y) -> plus#(x, s(y)))
    (ack#(s(x), s(y)) -> plus#(y, ack(s(x), y)), plus#(x, s(s(y))) -> plus#(s(x), y))
    (ack#(s(x), s(y)) -> plus#(y, ack(s(x), y)), plus#(s(s(x)), y) -> plus#(x, s(y)))}
   SCCS:
    Scc:
     {ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))),
      ack#(s(x), s(y)) -> ack#(s(x), y),
       ack#(s(x), 0()) -> ack#(x, s(0()))}
    Scc:
     {plus#(x, s(s(y))) -> plus#(s(x), y),
      plus#(s(s(x)), y) -> plus#(x, s(y))}
    SCC:
     Strict:
      {ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))),
       ack#(s(x), s(y)) -> ack#(s(x), y),
        ack#(s(x), 0()) -> ack#(x, s(0()))}
     Weak:
     {plus(x, s(s(y))) -> s(plus(s(x), y)),
      plus(s(s(x)), y) -> s(plus(x, s(y))),
       plus(s(0()), y) -> s(y),
          plus(0(), y) -> y,
       ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y))),
        ack(s(x), 0()) -> ack(x, s(0())),
           ack(0(), y) -> s(y)}
     SPSC:
      Simple Projection:
       pi(ack#) = 0
      Strict:
       {ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))),
        ack#(s(x), s(y)) -> ack#(s(x), y)}
      EDG:
       {(ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))), ack#(s(x), s(y)) -> ack#(s(x), y))
        (ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))), ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))))
        (ack#(s(x), s(y)) -> ack#(s(x), y), ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))))
        (ack#(s(x), s(y)) -> ack#(s(x), y), ack#(s(x), s(y)) -> ack#(s(x), y))}
       SCCS:
        Scc:
         {ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))),
          ack#(s(x), s(y)) -> ack#(s(x), y)}
        SCC:
         Strict:
          {ack#(s(x), s(y)) -> ack#(x, plus(y, ack(s(x), y))),
           ack#(s(x), s(y)) -> ack#(s(x), y)}
         Weak:
         {plus(x, s(s(y))) -> s(plus(s(x), y)),
          plus(s(s(x)), y) -> s(plus(x, s(y))),
           plus(s(0()), y) -> s(y),
              plus(0(), y) -> y,
           ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y))),
            ack(s(x), 0()) -> ack(x, s(0())),
               ack(0(), y) -> s(y)}
         SPSC:
          Simple Projection:
           pi(ack#) = 0
          Strict:
           {ack#(s(x), s(y)) -> ack#(s(x), y)}
          EDG:
           {(ack#(s(x), s(y)) -> ack#(s(x), y), ack#(s(x), s(y)) -> ack#(s(x), y))}
           SCCS:
            Scc:
             {ack#(s(x), s(y)) -> ack#(s(x), y)}
            SCC:
             Strict:
              {ack#(s(x), s(y)) -> ack#(s(x), y)}
             Weak:
             {plus(x, s(s(y))) -> s(plus(s(x), y)),
              plus(s(s(x)), y) -> s(plus(x, s(y))),
               plus(s(0()), y) -> s(y),
                  plus(0(), y) -> y,
               ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y))),
                ack(s(x), 0()) -> ack(x, s(0())),
                   ack(0(), y) -> s(y)}
             SPSC:
              Simple Projection:
               pi(ack#) = 1
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {plus#(x, s(s(y))) -> plus#(s(x), y),
       plus#(s(s(x)), y) -> plus#(x, s(y))}
     Weak:
     {plus(x, s(s(y))) -> s(plus(s(x), y)),
      plus(s(s(x)), y) -> s(plus(x, s(y))),
       plus(s(0()), y) -> s(y),
          plus(0(), y) -> y,
       ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y))),
        ack(s(x), 0()) -> ack(x, s(0())),
           ack(0(), y) -> s(y)}
     POLY:
      Argument Filtering:
       pi(ack) = [], pi(0) = [], pi(plus#) = [0,1], pi(plus) = [], pi(s) = [0]
      Usable Rules:
       {}
      Interpretation:
       [plus#](x0, x1) = x0 + x1,
       [s](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {plus(x, s(s(y))) -> s(plus(s(x), y)),
        plus(s(s(x)), y) -> s(plus(x, s(y))),
         plus(s(0()), y) -> s(y),
            plus(0(), y) -> y,
         ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y))),
          ack(s(x), 0()) -> ack(x, s(0())),
             ack(0(), y) -> s(y)}
      Qed