MAYBE
Time: 0.007205
TRS:
 {        minus(x, 0()) -> x,
  minus(minus(x, y), z) -> minus(x, plus(y, z)),
          minus(0(), y) -> 0(),
        minus(s x, s y) -> minus(x, y),
           plus(0(), y) -> y,
           plus(s x, y) -> plus(x, s y),
           plus(s x, y) -> s plus(y, x),
               zero 0() -> true(),
               zero s x -> false(),
                  p 0() -> 0(),
                  p s x -> x,
      quot(0(), s y, z) -> z,
      quot(s x, s y, z) -> quot(minus(p ack(0(), x), y), s y, s z),
              div(x, y) -> quot(x, y, 0()),
            ack(0(), x) -> plus(x, s 0()),
            ack(0(), x) -> s x,
          ack(s x, 0()) -> ack(x, s 0()),
          ack(s x, s y) -> ack(x, ack(s x, y))}
 DP:
  DP:
   {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
    minus#(minus(x, y), z) -> plus#(y, z),
          minus#(s x, s y) -> minus#(x, y),
             plus#(s x, y) -> plus#(x, s y),
             plus#(s x, y) -> plus#(y, x),
        quot#(s x, s y, z) -> minus#(p ack(0(), x), y),
        quot#(s x, s y, z) -> p# ack(0(), x),
        quot#(s x, s y, z) -> quot#(minus(p ack(0(), x), y), s y, s z),
        quot#(s x, s y, z) -> ack#(0(), x),
                div#(x, y) -> quot#(x, y, 0()),
              ack#(0(), x) -> plus#(x, s 0()),
            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)}
  TRS:
  {        minus(x, 0()) -> x,
   minus(minus(x, y), z) -> minus(x, plus(y, z)),
           minus(0(), y) -> 0(),
         minus(s x, s y) -> minus(x, y),
            plus(0(), y) -> y,
            plus(s x, y) -> plus(x, s y),
            plus(s x, y) -> s plus(y, x),
                zero 0() -> true(),
                zero s x -> false(),
                   p 0() -> 0(),
                   p s x -> x,
       quot(0(), s y, z) -> z,
       quot(s x, s y, z) -> quot(minus(p ack(0(), x), y), s y, s z),
               div(x, y) -> quot(x, y, 0()),
             ack(0(), x) -> plus(x, s 0()),
             ack(0(), x) -> s x,
           ack(s x, 0()) -> ack(x, s 0()),
           ack(s x, s y) -> ack(x, ack(s x, 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, ack(s x, y)))
    (ack#(s x, 0()) -> ack#(x, s 0()), ack#(0(), x) -> plus#(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, 0()) -> ack#(x, s 0()))
    (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(0(), x) -> plus#(x, s 0()))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> plus#(y, z))
    (minus#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
    (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, y) -> plus#(y, x))
    (minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, y) -> plus#(x, s y))
    (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(y, x))
    (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(x, s y))
    (quot#(s x, s y, z) -> ack#(0(), x), ack#(0(), x) -> plus#(x, s 0()))
    (div#(x, y) -> quot#(x, y, 0()), quot#(s x, s y, z) -> minus#(p ack(0(), x), y))
    (div#(x, y) -> quot#(x, y, 0()), quot#(s x, s y, z) -> p# ack(0(), x))
    (div#(x, y) -> quot#(x, y, 0()), quot#(s x, s y, z) -> quot#(minus(p ack(0(), x), y), s y, s z))
    (div#(x, y) -> quot#(x, y, 0()), quot#(s x, s y, z) -> ack#(0(), x))
    (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#(x, ack(s x, y)))
    (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(s x, y))
    (quot#(s x, s y, z) -> minus#(p ack(0(), x), y), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
    (quot#(s x, s y, z) -> minus#(p ack(0(), x), y), minus#(minus(x, y), z) -> plus#(y, z))
    (quot#(s x, s y, z) -> minus#(p ack(0(), x), y), minus#(s x, s y) -> minus#(x, y))
    (quot#(s x, s y, z) -> quot#(minus(p ack(0(), x), y), s y, s z), quot#(s x, s y, z) -> minus#(p ack(0(), x), y))
    (quot#(s x, s y, z) -> quot#(minus(p ack(0(), x), y), s y, s z), quot#(s x, s y, z) -> p# ack(0(), x))
    (quot#(s x, s y, z) -> quot#(minus(p ack(0(), x), y), s y, s z), quot#(s x, s y, z) -> quot#(minus(p ack(0(), x), y), s y, s z))
    (quot#(s x, s y, z) -> quot#(minus(p ack(0(), x), y), s y, s z), quot#(s x, s y, z) -> ack#(0(), x))
    (plus#(s x, y) -> plus#(y, x), plus#(s x, y) -> plus#(x, s y))
    (plus#(s x, y) -> plus#(y, x), plus#(s x, y) -> plus#(y, x))
    (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
    (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(minus(x, y), z) -> plus#(y, z))
    (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(s x, s y) -> minus#(x, y))
    (ack#(0(), x) -> plus#(x, s 0()), plus#(s x, y) -> plus#(x, s y))
    (ack#(0(), x) -> plus#(x, s 0()), plus#(s x, y) -> plus#(y, x))}
   STATUS:
    arrows: 0.816327
    SCCS (4):
     Scc:
      {quot#(s x, s y, z) -> quot#(minus(p ack(0(), x), y), s y, s z)}
     Scc:
      {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
             minus#(s x, s y) -> minus#(x, y)}
     Scc:
      {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)}
     Scc:
      {plus#(s x, y) -> plus#(x, s y),
       plus#(s x, y) -> plus#(y, x)}
     
     
     SCC (1):
      Strict:
       {quot#(s x, s y, z) -> quot#(minus(p ack(0(), x), y), s y, s z)}
      Weak:
      {        minus(x, 0()) -> x,
       minus(minus(x, y), z) -> minus(x, plus(y, z)),
               minus(0(), y) -> 0(),
             minus(s x, s y) -> minus(x, y),
                plus(0(), y) -> y,
                plus(s x, y) -> plus(x, s y),
                plus(s x, y) -> s plus(y, x),
                    zero 0() -> true(),
                    zero s x -> false(),
                       p 0() -> 0(),
                       p s x -> x,
           quot(0(), s y, z) -> z,
           quot(s x, s y, z) -> quot(minus(p ack(0(), x), y), s y, s z),
                   div(x, y) -> quot(x, y, 0()),
                 ack(0(), x) -> plus(x, s 0()),
                 ack(0(), x) -> s x,
               ack(s x, 0()) -> ack(x, s 0()),
               ack(s x, s y) -> ack(x, ack(s x, y))}
      Open
     
     
     
     SCC (2):
      Strict:
       {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
              minus#(s x, s y) -> minus#(x, y)}
      Weak:
      {        minus(x, 0()) -> x,
       minus(minus(x, y), z) -> minus(x, plus(y, z)),
               minus(0(), y) -> 0(),
             minus(s x, s y) -> minus(x, y),
                plus(0(), y) -> y,
                plus(s x, y) -> plus(x, s y),
                plus(s x, y) -> s plus(y, x),
                    zero 0() -> true(),
                    zero s x -> false(),
                       p 0() -> 0(),
                       p s x -> x,
           quot(0(), s y, z) -> z,
           quot(s x, s y, z) -> quot(minus(p ack(0(), x), y), s y, s z),
                   div(x, y) -> quot(x, y, 0()),
                 ack(0(), x) -> plus(x, s 0()),
                 ack(0(), x) -> s x,
               ack(s x, 0()) -> ack(x, s 0()),
               ack(s x, s y) -> ack(x, ack(s x, y))}
      Open
     
     SCC (3):
      Strict:
       {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)}
      Weak:
      {        minus(x, 0()) -> x,
       minus(minus(x, y), z) -> minus(x, plus(y, z)),
               minus(0(), y) -> 0(),
             minus(s x, s y) -> minus(x, y),
                plus(0(), y) -> y,
                plus(s x, y) -> plus(x, s y),
                plus(s x, y) -> s plus(y, x),
                    zero 0() -> true(),
                    zero s x -> false(),
                       p 0() -> 0(),
                       p s x -> x,
           quot(0(), s y, z) -> z,
           quot(s x, s y, z) -> quot(minus(p ack(0(), x), y), s y, s z),
                   div(x, y) -> quot(x, y, 0()),
                 ack(0(), x) -> plus(x, s 0()),
                 ack(0(), x) -> s x,
               ack(s x, 0()) -> ack(x, s 0()),
               ack(s x, s y) -> ack(x, ack(s x, y))}
      Open
     
     SCC (2):
      Strict:
       {plus#(s x, y) -> plus#(x, s y),
        plus#(s x, y) -> plus#(y, x)}
      Weak:
      {        minus(x, 0()) -> x,
       minus(minus(x, y), z) -> minus(x, plus(y, z)),
               minus(0(), y) -> 0(),
             minus(s x, s y) -> minus(x, y),
                plus(0(), y) -> y,
                plus(s x, y) -> plus(x, s y),
                plus(s x, y) -> s plus(y, x),
                    zero 0() -> true(),
                    zero s x -> false(),
                       p 0() -> 0(),
                       p s x -> x,
           quot(0(), s y, z) -> z,
           quot(s x, s y, z) -> quot(minus(p ack(0(), x), y), s y, s z),
                   div(x, y) -> quot(x, y, 0()),
                 ack(0(), x) -> plus(x, s 0()),
                 ack(0(), x) -> s x,
               ack(s x, 0()) -> ack(x, s 0()),
               ack(s x, s y) -> ack(x, ack(s x, y))}
      Open