MAYBE
TRS:
 {      permute(x, y, a()) -> permute(isZero(x), x, b()),
        permute(y, x, c()) -> s(s(permute(x, y, a()))),
  permute(false(), x, b()) -> permute(ack(x, x), p(x), c()),
   permute(true(), x, b()) -> 0(),
                 double(x) -> permute(x, x, a()),
               isZero(0()) -> true(),
              isZero(s(x)) -> false(),
               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)),
                    p(0()) -> 0(),
                   p(s(x)) -> x,
              plus(x, 0()) -> x,
           plus(x, s(0())) -> s(x),
          plus(x, s(s(y))) -> s(plus(s(x), y)),
              plus(0(), y) -> y,
             plus(s(x), y) -> plus(x, s(y))}
 DP:
  Strict:
   {      permute#(x, y, a()) -> permute#(isZero(x), x, b()),
          permute#(x, y, a()) -> isZero#(x),
          permute#(y, x, c()) -> permute#(x, y, a()),
    permute#(false(), x, b()) -> permute#(ack(x, x), p(x), c()),
    permute#(false(), x, b()) -> ack#(x, x),
    permute#(false(), x, b()) -> p#(x),
                   double#(x) -> permute#(x, x, a()),
                 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),
            plus#(x, s(s(y))) -> plus#(s(x), y),
               plus#(s(x), y) -> plus#(x, s(y))}
  Weak:
  {      permute(x, y, a()) -> permute(isZero(x), x, b()),
         permute(y, x, c()) -> s(s(permute(x, y, a()))),
   permute(false(), x, b()) -> permute(ack(x, x), p(x), c()),
    permute(true(), x, b()) -> 0(),
                  double(x) -> permute(x, x, a()),
                isZero(0()) -> true(),
               isZero(s(x)) -> false(),
                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)),
                     p(0()) -> 0(),
                    p(s(x)) -> x,
               plus(x, 0()) -> x,
            plus(x, s(0())) -> s(x),
           plus(x, s(s(y))) -> s(plus(s(x), y)),
               plus(0(), y) -> y,
              plus(s(x), y) -> plus(x, 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, ack(s(x), y)))
    (ack#(s(x), 0()) -> ack#(x, s(0())), ack#(0(), x) -> plus#(x, s(0())))
    (plus#(x, s(s(y))) -> plus#(s(x), y), plus#(s(x), y) -> plus#(x, s(y)))
    (plus#(x, s(s(y))) -> plus#(s(x), y), plus#(x, s(s(y))) -> plus#(s(x), y))
    (permute#(y, x, c()) -> permute#(x, y, a()), permute#(x, y, a()) -> isZero#(x))
    (permute#(y, x, c()) -> permute#(x, y, a()), permute#(x, y, a()) -> permute#(isZero(x), x, b()))
    (double#(x) -> permute#(x, x, a()), permute#(x, y, a()) -> isZero#(x))
    (double#(x) -> permute#(x, x, a()), permute#(x, y, a()) -> permute#(isZero(x), x, b()))
    (permute#(false(), x, b()) -> ack#(x, x), ack#(s(x), s(y)) -> ack#(s(x), y))
    (permute#(false(), x, b()) -> ack#(x, x), ack#(s(x), s(y)) -> ack#(x, ack(s(x), y)))
    (permute#(false(), x, b()) -> ack#(x, x), ack#(s(x), 0()) -> ack#(x, s(0())))
    (permute#(false(), x, b()) -> ack#(x, x), ack#(0(), x) -> plus#(x, s(0())))
    (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))
    (plus#(s(x), y) -> plus#(x, s(y)), plus#(x, s(s(y))) -> plus#(s(x), y))
    (plus#(s(x), y) -> plus#(x, s(y)), plus#(s(x), y) -> plus#(x, s(y)))
    (permute#(false(), x, b()) -> permute#(ack(x, x), p(x), c()), permute#(y, x, c()) -> permute#(x, y, a()))
    (permute#(x, y, a()) -> permute#(isZero(x), x, b()), permute#(false(), x, b()) -> permute#(ack(x, x), p(x), c()))
    (permute#(x, y, a()) -> permute#(isZero(x), x, b()), permute#(false(), x, b()) -> ack#(x, x))
    (permute#(x, y, a()) -> permute#(isZero(x), x, b()), permute#(false(), x, b()) -> p#(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))
    (ack#(0(), x) -> plus#(x, s(0())), plus#(s(x), y) -> plus#(x, s(y)))}
   SCCS:
    Scc:
     {plus#(x, s(s(y))) -> plus#(s(x), y),
         plus#(s(x), y) -> plus#(x, s(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:
     {      permute#(x, y, a()) -> permute#(isZero(x), x, b()),
            permute#(y, x, c()) -> permute#(x, y, a()),
      permute#(false(), x, b()) -> permute#(ack(x, x), p(x), c())}
    SCC:
     Strict:
      {plus#(x, s(s(y))) -> plus#(s(x), y),
          plus#(s(x), y) -> plus#(x, s(y))}
     Weak:
     {      permute(x, y, a()) -> permute(isZero(x), x, b()),
            permute(y, x, c()) -> s(s(permute(x, y, a()))),
      permute(false(), x, b()) -> permute(ack(x, x), p(x), c()),
       permute(true(), x, b()) -> 0(),
                     double(x) -> permute(x, x, a()),
                   isZero(0()) -> true(),
                  isZero(s(x)) -> false(),
                   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)),
                        p(0()) -> 0(),
                       p(s(x)) -> x,
                  plus(x, 0()) -> x,
               plus(x, s(0())) -> s(x),
              plus(x, s(s(y))) -> s(plus(s(x), y)),
                  plus(0(), y) -> y,
                 plus(s(x), y) -> plus(x, s(y))}
     POLY:
      Argument Filtering:
       pi(plus#) = [0,1], pi(plus) = [], pi(s) = [0], pi(true) = [], pi(0) = [], pi(false) = [], pi(c) = [], pi(p) = [], pi(ack) = [], pi(b) = [], pi(isZero) = [], pi(double) = [], pi(a) = [], pi(permute) = []
      Usable Rules:
       {}
      Interpretation:
       [plus#](x0, x1) = x0 + x1,
       [s](x0) = x0 + 1
      Strict:
       {plus#(s(x), y) -> plus#(x, s(y))}
      Weak:
       {      permute(x, y, a()) -> permute(isZero(x), x, b()),
              permute(y, x, c()) -> s(s(permute(x, y, a()))),
        permute(false(), x, b()) -> permute(ack(x, x), p(x), c()),
         permute(true(), x, b()) -> 0(),
                       double(x) -> permute(x, x, a()),
                     isZero(0()) -> true(),
                    isZero(s(x)) -> false(),
                     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)),
                          p(0()) -> 0(),
                         p(s(x)) -> x,
                    plus(x, 0()) -> x,
                 plus(x, s(0())) -> s(x),
                plus(x, s(s(y))) -> s(plus(s(x), y)),
                    plus(0(), y) -> y,
                   plus(s(x), y) -> plus(x, s(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:
         {      permute(x, y, a()) -> permute(isZero(x), x, b()),
                permute(y, x, c()) -> s(s(permute(x, y, a()))),
          permute(false(), x, b()) -> permute(ack(x, x), p(x), c()),
           permute(true(), x, b()) -> 0(),
                         double(x) -> permute(x, x, a()),
                       isZero(0()) -> true(),
                      isZero(s(x)) -> false(),
                       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)),
                            p(0()) -> 0(),
                           p(s(x)) -> x,
                      plus(x, 0()) -> x,
                   plus(x, s(0())) -> s(x),
                  plus(x, s(s(y))) -> s(plus(s(x), y)),
                      plus(0(), y) -> y,
                     plus(s(x), y) -> plus(x, s(y))}
         SPSC:
          Simple Projection:
           pi(plus#) = 0
          Strict:
           {}
          Qed
    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:
     {      permute(x, y, a()) -> permute(isZero(x), x, b()),
            permute(y, x, c()) -> s(s(permute(x, y, a()))),
      permute(false(), x, b()) -> permute(ack(x, x), p(x), c()),
       permute(true(), x, b()) -> 0(),
                     double(x) -> permute(x, x, a()),
                   isZero(0()) -> true(),
                  isZero(s(x)) -> false(),
                   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)),
                        p(0()) -> 0(),
                       p(s(x)) -> x,
                  plus(x, 0()) -> x,
               plus(x, s(0())) -> s(x),
              plus(x, s(s(y))) -> s(plus(s(x), y)),
                  plus(0(), y) -> y,
                 plus(s(x), y) -> plus(x, s(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:
         {      permute(x, y, a()) -> permute(isZero(x), x, b()),
                permute(y, x, c()) -> s(s(permute(x, y, a()))),
          permute(false(), x, b()) -> permute(ack(x, x), p(x), c()),
           permute(true(), x, b()) -> 0(),
                         double(x) -> permute(x, x, a()),
                       isZero(0()) -> true(),
                      isZero(s(x)) -> false(),
                       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)),
                            p(0()) -> 0(),
                           p(s(x)) -> x,
                      plus(x, 0()) -> x,
                   plus(x, s(0())) -> s(x),
                  plus(x, s(s(y))) -> s(plus(s(x), y)),
                      plus(0(), y) -> y,
                     plus(s(x), y) -> plus(x, 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:
            Scc:
             {ack#(s(x), s(y)) -> ack#(s(x), y)}
            SCC:
             Strict:
              {ack#(s(x), s(y)) -> ack#(s(x), y)}
             Weak:
             {      permute(x, y, a()) -> permute(isZero(x), x, b()),
                    permute(y, x, c()) -> s(s(permute(x, y, a()))),
              permute(false(), x, b()) -> permute(ack(x, x), p(x), c()),
               permute(true(), x, b()) -> 0(),
                             double(x) -> permute(x, x, a()),
                           isZero(0()) -> true(),
                          isZero(s(x)) -> false(),
                           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)),
                                p(0()) -> 0(),
                               p(s(x)) -> x,
                          plus(x, 0()) -> x,
                       plus(x, s(0())) -> s(x),
                      plus(x, s(s(y))) -> s(plus(s(x), y)),
                          plus(0(), y) -> y,
                         plus(s(x), y) -> plus(x, s(y))}
             SPSC:
              Simple Projection:
               pi(ack#) = 1
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {      permute#(x, y, a()) -> permute#(isZero(x), x, b()),
             permute#(y, x, c()) -> permute#(x, y, a()),
       permute#(false(), x, b()) -> permute#(ack(x, x), p(x), c())}
     Weak:
     {      permute(x, y, a()) -> permute(isZero(x), x, b()),
            permute(y, x, c()) -> s(s(permute(x, y, a()))),
      permute(false(), x, b()) -> permute(ack(x, x), p(x), c()),
       permute(true(), x, b()) -> 0(),
                     double(x) -> permute(x, x, a()),
                   isZero(0()) -> true(),
                  isZero(s(x)) -> false(),
                   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)),
                        p(0()) -> 0(),
                       p(s(x)) -> x,
                  plus(x, 0()) -> x,
               plus(x, s(0())) -> s(x),
              plus(x, s(s(y))) -> s(plus(s(x), y)),
                  plus(0(), y) -> y,
                 plus(s(x), y) -> plus(x, s(y))}
     Fail