YES
Time: 0.010543
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:
  DP:
   {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())}
  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}
  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 (2):
    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 (3):
     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#(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#(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) -> ack#(s x, y))}
       SCCS (1):
        Scc:
         {ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))),
          ack#(s x, s y) -> ack#(s x, y)}
        SCC (2):
         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 (1):
            Scc:
             {ack#(s x, s y) -> ack#(s x, y)}
            SCC (1):
             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 (2):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [plus](x0, x1) = 0,
       
       [ack](x0, x1) = 0,
       
       [s](x0) = x0 + 1,
       
       [0] = 1,
       
       [plus#](x0, x1) = x0 + x1 + 1
      Strict:
       plus#(s s x, y) -> plus#(x, s y)
       3 + 1x + 1y >= 2 + 1x + 1y
       plus#(x, s s y) -> plus#(s x, y)
       3 + 1x + 1y >= 2 + 1x + 1y
      Weak:
       
     Qed