MAYBE
Time: 0.030175
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())}
  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)))}
   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:
     {p# s s x -> p# s x}
    Scc:
     {plus#(s x, y) -> plus#(p s x, y)}
    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())}
     Fail
    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())}
     SPSC:
      Simple Projection:
       pi(exp#) = 1
      Strict:
       {}
      Qed
    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())}
     Fail
    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())}
     SPSC:
      Simple Projection:
       pi(p#) = 0
      Strict:
       {}
      Qed
    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())}
     Fail