MAYBE
Time: 0.317421
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}
  UR:
   {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,
           a(z, w) -> z,
           a(z, w) -> w}
   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))}
    STATUS:
     arrows: 0.527778
     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}
       Open
      
      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}
       Open