MAYBE
Time: 0.001536
TRS:
 {  ack(s x, y) -> f(x, x),
  ack(s x, s y) -> ack(x, ack(s x, y)),
  ack(s x, 0()) -> ack(x, s 0()),
    ack(0(), y) -> s y,
        f(x, y) -> ack(x, y),
      f(x, s y) -> f(y, x),
      f(s x, y) -> f(x, s x)}
 DP:
  DP:
   {  ack#(s x, y) -> f#(x, x),
    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()),
          f#(x, y) -> ack#(x, y),
        f#(x, s y) -> f#(y, x),
        f#(s x, y) -> f#(x, s x)}
  TRS:
  {  ack(s x, y) -> f(x, x),
   ack(s x, s y) -> ack(x, ack(s x, y)),
   ack(s x, 0()) -> ack(x, s 0()),
     ack(0(), y) -> s y,
         f(x, y) -> ack(x, y),
       f(x, s y) -> f(y, x),
       f(s x, y) -> f(x, s x)}
  UR:
   {  ack(s x, y) -> f(x, x),
    ack(s x, s y) -> ack(x, ack(s x, y)),
    ack(s x, 0()) -> ack(x, s 0()),
      ack(0(), y) -> s y,
          f(x, y) -> ack(x, y),
        f(x, s y) -> f(y, x),
        f(s x, y) -> f(x, s x),
          a(z, w) -> z,
          a(z, w) -> w}
   EDG:
    {(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, 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, y) -> f#(x, x))
     (f#(s x, y) -> f#(x, s x), f#(s x, y) -> f#(x, s x))
     (f#(s x, y) -> f#(x, s x), f#(x, s y) -> f#(y, x))
     (f#(s x, y) -> f#(x, s x), f#(x, y) -> ack#(x, y))
     (f#(x, s y) -> f#(y, x), f#(s x, y) -> f#(x, s x))
     (f#(x, s y) -> f#(y, x), f#(x, s y) -> f#(y, x))
     (f#(x, s y) -> f#(y, x), f#(x, y) -> ack#(x, y))
     (ack#(s x, s y) -> ack#(s x, y), ack#(s x, y) -> f#(x, x))
     (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#(s x, y), ack#(s x, s 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, y) -> f#(x, x), f#(x, y) -> ack#(x, y))
     (ack#(s x, y) -> f#(x, x), f#(x, s y) -> f#(y, x))
     (ack#(s x, y) -> f#(x, x), f#(s x, y) -> f#(x, s x))
     (f#(x, y) -> ack#(x, y), ack#(s x, y) -> f#(x, x))
     (f#(x, y) -> ack#(x, y), ack#(s x, s y) -> ack#(x, ack(s x, y)))
     (f#(x, y) -> ack#(x, y), ack#(s x, s y) -> ack#(s x, y))
     (f#(x, y) -> ack#(x, y), ack#(s x, 0()) -> ack#(x, s 0()))
     (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, y) -> f#(x, x))
     (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, 0()) -> ack#(x, s 0()), ack#(s x, 0()) -> ack#(x, s 0()))}
    STATUS:
     arrows: 0.489796
     SCCS (1):
      Scc:
       {  ack#(s x, y) -> f#(x, x),
        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()),
              f#(x, y) -> ack#(x, y),
            f#(x, s y) -> f#(y, x),
            f#(s x, y) -> f#(x, s x)}
      
      SCC (7):
       Strict:
        {  ack#(s x, y) -> f#(x, x),
         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()),
               f#(x, y) -> ack#(x, y),
             f#(x, s y) -> f#(y, x),
             f#(s x, y) -> f#(x, s x)}
       Weak:
       {  ack(s x, y) -> f(x, x),
        ack(s x, s y) -> ack(x, ack(s x, y)),
        ack(s x, 0()) -> ack(x, s 0()),
          ack(0(), y) -> s y,
              f(x, y) -> ack(x, y),
            f(x, s y) -> f(y, x),
            f(s x, y) -> f(x, s x)}
       Open