MAYBE
Time: 0.010362
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:
  DP:
   {      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)}
  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)}
  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()))
    (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()))
    (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#(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))
    (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))
    (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#(0(), x) -> plus#(x, s 0()), 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()))
     (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()))
     (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#(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))
     (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))
     (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#(0(), x) -> plus#(x, s 0()), 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()))
      (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()))
      (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#(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))
      (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))
      (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#(0(), x) -> plus#(x, s 0()), plus#(s x, y) -> plus#(x, s y))}
     STATUS:
      arrows: 0.840237
      SCCS (3):
       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:
        {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#(x, s s y) -> plus#(s x, y),
           plus#(s x, y) -> plus#(x, s y)}
       
       
       SCC (3):
        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)}
        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:
        {      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)}
        Open
       
       SCC (2):
        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)}
        Open