MAYBE
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:
  Strict:
   {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)}
  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))}
  EDG:
   {(ack#(0(), x) -> plus#(x, s(0())), plus#(s(x), y) -> plus#(y, x))
    (ack#(0(), x) -> plus#(x, s(0())), plus#(s(x), y) -> plus#(x, s(y)))
    (minus#(minus(x, y), z) -> minus#(x, 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))
    (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
    (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)))
    (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))
    (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) -> 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) -> minus#(p(ack(0(), 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), 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())))
    (div#(x, y) -> quot#(x, y, 0()), quot#(s(x), s(y), z) -> 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) -> p#(ack(0(), x)))
    (div#(x, y) -> quot#(x, y, 0()), quot#(s(x), s(y), z) -> minus#(p(ack(0(), x)), y))
    (plus#(s(x), y) -> plus#(x, s(y)), plus#(s(x), y) -> plus#(x, s(y)))
    (plus#(s(x), y) -> plus#(x, s(y)), plus#(s(x), y) -> plus#(y, x))
    (quot#(s(x), s(y), z) -> ack#(0(), x), ack#(0(), x) -> plus#(x, s(0())))
    (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))
    (minus#(minus(x, y), z) -> plus#(y, z), plus#(s(x), y) -> plus#(x, s(y)))
    (minus#(minus(x, y), z) -> plus#(y, z), plus#(s(x), y) -> plus#(y, x))
    (ack#(s(x), s(y)) -> ack#(x, ack(s(x), y)), ack#(0(), x) -> plus#(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#(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))
    (ack#(s(x), 0()) -> ack#(x, s(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), 0()) -> ack#(x, s(0())), ack#(s(x), s(y)) -> ack#(s(x), y))
    (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))}
   SCCS:
    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:
     {quot#(s(x), s(y), z) -> quot#(minus(p(ack(0(), x)), y), s(y), s(z))}
    Scc:
     {plus#(s(x), y) -> plus#(x, s(y)),
      plus#(s(x), y) -> plus#(y, x)}
    Scc:
     {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
          minus#(s(x), s(y)) -> minus#(x, y)}
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(ack#) = 0
      Strict:
       { ack#(s(x), 0()) -> ack#(x, s(0())),
        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), 0()) -> ack#(x, s(0())))
        (ack#(s(x), 0()) -> ack#(x, s(0())), ack#(s(x), s(y)) -> ack#(s(x), y))}
       SCCS:
        Scc:
         { ack#(s(x), 0()) -> ack#(x, s(0())),
          ack#(s(x), s(y)) -> ack#(s(x), y)}
        SCC:
         Strict:
          { ack#(s(x), 0()) -> ack#(x, s(0())),
           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))}
         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:
            Scc:
             {ack#(s(x), s(y)) -> ack#(s(x), y)}
            SCC:
             Strict:
              {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))}
             SPSC:
              Simple Projection:
               pi(ack#) = 1
              Strict:
               {}
              Qed
    SCC:
     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))}
     Fail
    SCC:
     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))}
     POLY:
      Argument Filtering:
       pi(ack) = [], pi(div) = [], pi(quot) = [], pi(p) = [], pi(true) = [], pi(zero) = [], pi(false) = [], pi(s) = [0], pi(0) = [], pi(plus#) = [0,1], pi(plus) = [], pi(minus) = []
      Usable Rules:
       {}
      Interpretation:
       [plus#](x0, x1) = x0 + x1,
       [s](x0) = x0 + 1
      Strict:
       {plus#(s(x), y) -> plus#(x, s(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))}
      EDG:
       {(plus#(s(x), y) -> plus#(x, s(y)), plus#(s(x), y) -> plus#(x, s(y)))}
       SCCS:
        Scc:
         {plus#(s(x), y) -> plus#(x, s(y))}
        SCC:
         Strict:
          {plus#(s(x), y) -> plus#(x, s(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))}
         SPSC:
          Simple Projection:
           pi(plus#) = 0
          Strict:
           {}
          Qed
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {minus#(s(x), s(y)) -> minus#(x, y)}
      EDG:
       {(minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))}
       SCCS:
        Scc:
         {minus#(s(x), s(y)) -> minus#(x, y)}
        SCC:
         Strict:
          {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))}
         SPSC:
          Simple Projection:
           pi(minus#) = 0
          Strict:
           {}
          Qed