YES
Time: 0.001606
TRS:
 {ack(s x, s y) -> ack(x, ack(s x, y)),
  ack(s x, 0()) -> ack(x, s 0()),
    ack(0(), y) -> s y}
 DP:
  DP:
   {ack#(s x, s y) -> ack#(x, ack(s x, y)),
    ack#(s x, s y) -> ack#(s x, y),
    ack#(s x, 0()) -> ack#(x, s 0())}
  TRS:
  {ack(s x, s y) -> ack(x, ack(s x, y)),
   ack(s x, 0()) -> ack(x, s 0()),
     ack(0(), y) -> s y}
  EDG:
   {(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, ack(s x, y)))
    (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(x, 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#(x, ack(s x, y)), ack#(s x, s y) -> ack#(x, ack(s x, y)))
    (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(s x, y))}
   SCCS (1):
    Scc:
     {ack#(s x, s y) -> ack#(x, ack(s x, y)),
      ack#(s x, s y) -> ack#(s x, y),
      ack#(s x, 0()) -> ack#(x, s 0())}
    SCC (3):
     Strict:
      {ack#(s x, s y) -> ack#(x, ack(s x, y)),
       ack#(s x, s y) -> ack#(s x, y),
       ack#(s x, 0()) -> ack#(x, s 0())}
     Weak:
     {ack(s x, s y) -> ack(x, 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, ack(s x, y)),
        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))
        (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(x, ack(s x, y)))
        (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(x, ack(s x, y)))
        (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(s x, y))}
       SCCS (1):
        Scc:
         {ack#(s x, s y) -> ack#(x, ack(s x, y)),
          ack#(s x, s y) -> ack#(s x, y)}
        SCC (2):
         Strict:
          {ack#(s x, s y) -> ack#(x, ack(s x, y)),
           ack#(s x, s y) -> ack#(s x, y)}
         Weak:
         {ack(s x, s y) -> ack(x, 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 (1):
            Scc:
             {ack#(s x, s y) -> ack#(s x, y)}
            SCC (1):
             Strict:
              {ack#(s x, s y) -> ack#(s x, y)}
             Weak:
             {ack(s x, s y) -> ack(x, 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