MAYBE
Time: 1.584787
TRS:
 {        plus(0(), x) -> x,
          plus(s x, y) -> s plus(p s x, y),
               p s 0() -> 0(),
               p s s x -> s p s x,
         times(0(), y) -> 0(),
         times(s x, y) -> plus(y, times(p s x, y)),
           exp(x, 0()) -> s 0(),
           exp(x, s y) -> times(x, exp(x, y)),
  towerIter(0(), y, z) -> z,
  towerIter(s x, y, z) -> towerIter(p s x, y, exp(y, z)),
           tower(x, y) -> towerIter(x, y, s 0())}
 DP:
  DP:
   {        plus#(s x, y) -> plus#(p s x, y),
            plus#(s x, y) -> p# s x,
                 p# s s x -> p# s x,
           times#(s x, y) -> plus#(y, times(p s x, y)),
           times#(s x, y) -> p# s x,
           times#(s x, y) -> times#(p s x, y),
             exp#(x, s y) -> times#(x, exp(x, y)),
             exp#(x, s y) -> exp#(x, y),
    towerIter#(s x, y, z) -> p# s x,
    towerIter#(s x, y, z) -> exp#(y, z),
    towerIter#(s x, y, z) -> towerIter#(p s x, y, exp(y, z)),
             tower#(x, y) -> towerIter#(x, y, s 0())}
  TRS:
  {        plus(0(), x) -> x,
           plus(s x, y) -> s plus(p s x, y),
                p s 0() -> 0(),
                p s s x -> s p s x,
          times(0(), y) -> 0(),
          times(s x, y) -> plus(y, times(p s x, y)),
            exp(x, 0()) -> s 0(),
            exp(x, s y) -> times(x, exp(x, y)),
   towerIter(0(), y, z) -> z,
   towerIter(s x, y, z) -> towerIter(p s x, y, exp(y, z)),
            tower(x, y) -> towerIter(x, y, s 0())}
  UR:
   { plus(0(), x) -> x,
     plus(s x, y) -> s plus(p s x, y),
          p s 0() -> 0(),
          p s s x -> s p s x,
    times(0(), y) -> 0(),
    times(s x, y) -> plus(y, times(p s x, y)),
      exp(x, 0()) -> s 0(),
      exp(x, s y) -> times(x, exp(x, y)),
          a(w, v) -> w,
          a(w, v) -> v}
   EDG:
    {(times#(s x, y) -> plus#(y, times(p s x, y)), plus#(s x, y) -> p# s x)
     (times#(s x, y) -> plus#(y, times(p s x, y)), plus#(s x, y) -> plus#(p s x, y))
     (towerIter#(s x, y, z) -> exp#(y, z), exp#(x, s y) -> exp#(x, y))
     (towerIter#(s x, y, z) -> exp#(y, z), exp#(x, s y) -> times#(x, exp(x, y)))
     (towerIter#(s x, y, z) -> towerIter#(p s x, y, exp(y, z)), towerIter#(s x, y, z) -> towerIter#(p s x, y, exp(y, z)))
     (towerIter#(s x, y, z) -> towerIter#(p s x, y, exp(y, z)), towerIter#(s x, y, z) -> exp#(y, z))
     (towerIter#(s x, y, z) -> towerIter#(p s x, y, exp(y, z)), towerIter#(s x, y, z) -> p# s x)
     (times#(s x, y) -> times#(p s x, y), times#(s x, y) -> times#(p s x, y))
     (times#(s x, y) -> times#(p s x, y), times#(s x, y) -> p# s x)
     (times#(s x, y) -> times#(p s x, y), times#(s x, y) -> plus#(y, times(p s x, y)))
     (p# s s x -> p# s x, p# s s x -> p# s x)
     (towerIter#(s x, y, z) -> p# s x, p# s s x -> p# s x)
     (times#(s x, y) -> p# s x, p# s s x -> p# s x)
     (plus#(s x, y) -> p# s x, p# s s x -> p# s x)
     (plus#(s x, y) -> plus#(p s x, y), plus#(s x, y) -> plus#(p s x, y))
     (plus#(s x, y) -> plus#(p s x, y), plus#(s x, y) -> p# s x)
     (exp#(x, s y) -> exp#(x, y), exp#(x, s y) -> times#(x, exp(x, y)))
     (exp#(x, s y) -> exp#(x, y), exp#(x, s y) -> exp#(x, y))
     (exp#(x, s y) -> times#(x, exp(x, y)), times#(s x, y) -> plus#(y, times(p s x, y)))
     (exp#(x, s y) -> times#(x, exp(x, y)), times#(s x, y) -> p# s x)
     (exp#(x, s y) -> times#(x, exp(x, y)), times#(s x, y) -> times#(p s x, y))
     (tower#(x, y) -> towerIter#(x, y, s 0()), towerIter#(s x, y, z) -> p# s x)
     (tower#(x, y) -> towerIter#(x, y, s 0()), towerIter#(s x, y, z) -> exp#(y, z))
     (tower#(x, y) -> towerIter#(x, y, s 0()), towerIter#(s x, y, z) -> towerIter#(p s x, y, exp(y, z)))}
    STATUS:
     arrows: 0.833333
     SCCS (5):
      Scc:
       {towerIter#(s x, y, z) -> towerIter#(p s x, y, exp(y, z))}
      Scc:
       {exp#(x, s y) -> exp#(x, y)}
      Scc:
       {times#(s x, y) -> times#(p s x, y)}
      Scc:
       {plus#(s x, y) -> plus#(p s x, y)}
      Scc:
       {p# s s x -> p# s x}
      
      
      SCC (1):
       Strict:
        {towerIter#(s x, y, z) -> towerIter#(p s x, y, exp(y, z))}
       Weak:
       {        plus(0(), x) -> x,
                plus(s x, y) -> s plus(p s x, y),
                     p s 0() -> 0(),
                     p s s x -> s p s x,
               times(0(), y) -> 0(),
               times(s x, y) -> plus(y, times(p s x, y)),
                 exp(x, 0()) -> s 0(),
                 exp(x, s y) -> times(x, exp(x, y)),
        towerIter(0(), y, z) -> z,
        towerIter(s x, y, z) -> towerIter(p s x, y, exp(y, z)),
                 tower(x, y) -> towerIter(x, y, s 0())}
       Open
      
      SCC (1):
       Strict:
        {exp#(x, s y) -> exp#(x, y)}
       Weak:
       {        plus(0(), x) -> x,
                plus(s x, y) -> s plus(p s x, y),
                     p s 0() -> 0(),
                     p s s x -> s p s x,
               times(0(), y) -> 0(),
               times(s x, y) -> plus(y, times(p s x, y)),
                 exp(x, 0()) -> s 0(),
                 exp(x, s y) -> times(x, exp(x, y)),
        towerIter(0(), y, z) -> z,
        towerIter(s x, y, z) -> towerIter(p s x, y, exp(y, z)),
                 tower(x, y) -> towerIter(x, y, s 0())}
       Open
      
      SCC (1):
       Strict:
        {times#(s x, y) -> times#(p s x, y)}
       Weak:
       {        plus(0(), x) -> x,
                plus(s x, y) -> s plus(p s x, y),
                     p s 0() -> 0(),
                     p s s x -> s p s x,
               times(0(), y) -> 0(),
               times(s x, y) -> plus(y, times(p s x, y)),
                 exp(x, 0()) -> s 0(),
                 exp(x, s y) -> times(x, exp(x, y)),
        towerIter(0(), y, z) -> z,
        towerIter(s x, y, z) -> towerIter(p s x, y, exp(y, z)),
                 tower(x, y) -> towerIter(x, y, s 0())}
       Open
      
      
      SCC (1):
       Strict:
        {plus#(s x, y) -> plus#(p s x, y)}
       Weak:
       {        plus(0(), x) -> x,
                plus(s x, y) -> s plus(p s x, y),
                     p s 0() -> 0(),
                     p s s x -> s p s x,
               times(0(), y) -> 0(),
               times(s x, y) -> plus(y, times(p s x, y)),
                 exp(x, 0()) -> s 0(),
                 exp(x, s y) -> times(x, exp(x, y)),
        towerIter(0(), y, z) -> z,
        towerIter(s x, y, z) -> towerIter(p s x, y, exp(y, z)),
                 tower(x, y) -> towerIter(x, y, s 0())}
       Open
      
      
      SCC (1):
       Strict:
        {p# s s x -> p# s x}
       Weak:
       {        plus(0(), x) -> x,
                plus(s x, y) -> s plus(p s x, y),
                     p s 0() -> 0(),
                     p s s x -> s p s x,
               times(0(), y) -> 0(),
               times(s x, y) -> plus(y, times(p s x, y)),
                 exp(x, 0()) -> s 0(),
                 exp(x, s y) -> times(x, exp(x, y)),
        towerIter(0(), y, z) -> z,
        towerIter(s x, y, z) -> towerIter(p s x, y, exp(y, z)),
                 tower(x, y) -> towerIter(x, y, s 0())}
       Open