MAYBE
Time: 0.007548
TRS:
 {             plus(0(), x) -> x,
               plus(s x, y) -> s plus(x, y),
              times(0(), y) -> 0(),
              times(s x, y) -> plus(y, times(x, y)),
                exp(x, 0()) -> s 0(),
                exp(x, s y) -> times(x, exp(x, y)),
                 ge(x, 0()) -> true(),
               ge(0(), s x) -> false(),
               ge(s x, s y) -> ge(x, y),
      towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z),
                tower(x, y) -> towerIter(0(), x, y, s 0()),
   help(true(), c, x, y, z) -> z,
  help(false(), c, x, y, z) -> towerIter(s c, x, y, exp(y, z))}
 DP:
  DP:
   {             plus#(s x, y) -> plus#(x, y),
                times#(s x, y) -> plus#(y, times(x, y)),
                times#(s x, y) -> times#(x, y),
                  exp#(x, s y) -> times#(x, exp(x, y)),
                  exp#(x, s y) -> exp#(x, y),
                 ge#(s x, s y) -> ge#(x, y),
        towerIter#(c, x, y, z) -> ge#(c, x),
        towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z),
                  tower#(x, y) -> towerIter#(0(), x, y, s 0()),
    help#(false(), c, x, y, z) -> exp#(y, z),
    help#(false(), c, x, y, z) -> towerIter#(s c, x, y, exp(y, z))}
  TRS:
  {             plus(0(), x) -> x,
                plus(s x, y) -> s plus(x, y),
               times(0(), y) -> 0(),
               times(s x, y) -> plus(y, times(x, y)),
                 exp(x, 0()) -> s 0(),
                 exp(x, s y) -> times(x, exp(x, y)),
                  ge(x, 0()) -> true(),
                ge(0(), s x) -> false(),
                ge(s x, s y) -> ge(x, y),
       towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z),
                 tower(x, y) -> towerIter(0(), x, y, s 0()),
    help(true(), c, x, y, z) -> z,
   help(false(), c, x, y, z) -> towerIter(s c, x, y, exp(y, z))}
  EDG:
   {(times#(s x, y) -> times#(x, y), times#(s x, y) -> times#(x, y))
    (times#(s x, y) -> times#(x, y), times#(s x, y) -> plus#(y, times(x, y)))
    (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
    (exp#(x, s y) -> times#(x, exp(x, y)), times#(s x, y) -> times#(x, y))
    (exp#(x, s y) -> times#(x, exp(x, y)), times#(s x, y) -> plus#(y, times(x, y)))
    (towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z), help#(false(), c, x, y, z) -> towerIter#(s c, x, y, exp(y, z)))
    (towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z), help#(false(), c, x, y, z) -> exp#(y, z))
    (help#(false(), c, x, y, z) -> towerIter#(s c, x, y, exp(y, z)), towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z))
    (help#(false(), c, x, y, z) -> towerIter#(s c, x, y, exp(y, z)), towerIter#(c, x, y, z) -> ge#(c, x))
    (towerIter#(c, x, y, z) -> ge#(c, x), ge#(s x, s y) -> ge#(x, y))
    (tower#(x, y) -> towerIter#(0(), x, y, s 0()), towerIter#(c, x, y, z) -> ge#(c, x))
    (tower#(x, y) -> towerIter#(0(), x, y, s 0()), towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z))
    (help#(false(), c, x, y, z) -> exp#(y, z), exp#(x, s y) -> times#(x, exp(x, y)))
    (help#(false(), c, x, y, z) -> exp#(y, z), exp#(x, s y) -> exp#(x, y))
    (times#(s x, y) -> plus#(y, times(x, y)), plus#(s x, y) -> plus#(x, y))
    (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))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))}
   EDG:
    {(times#(s x, y) -> times#(x, y), times#(s x, y) -> times#(x, y))
     (times#(s x, y) -> times#(x, y), times#(s x, y) -> plus#(y, times(x, y)))
     (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
     (exp#(x, s y) -> times#(x, exp(x, y)), times#(s x, y) -> times#(x, y))
     (exp#(x, s y) -> times#(x, exp(x, y)), times#(s x, y) -> plus#(y, times(x, y)))
     (towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z), help#(false(), c, x, y, z) -> towerIter#(s c, x, y, exp(y, z)))
     (towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z), help#(false(), c, x, y, z) -> exp#(y, z))
     (help#(false(), c, x, y, z) -> towerIter#(s c, x, y, exp(y, z)), towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z))
     (help#(false(), c, x, y, z) -> towerIter#(s c, x, y, exp(y, z)), towerIter#(c, x, y, z) -> ge#(c, x))
     (towerIter#(c, x, y, z) -> ge#(c, x), ge#(s x, s y) -> ge#(x, y))
     (tower#(x, y) -> towerIter#(0(), x, y, s 0()), towerIter#(c, x, y, z) -> ge#(c, x))
     (tower#(x, y) -> towerIter#(0(), x, y, s 0()), towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z))
     (help#(false(), c, x, y, z) -> exp#(y, z), exp#(x, s y) -> times#(x, exp(x, y)))
     (help#(false(), c, x, y, z) -> exp#(y, z), exp#(x, s y) -> exp#(x, y))
     (times#(s x, y) -> plus#(y, times(x, y)), plus#(s x, y) -> plus#(x, y))
     (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))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))}
    EDG:
     {(times#(s x, y) -> times#(x, y), times#(s x, y) -> times#(x, y))
      (times#(s x, y) -> times#(x, y), times#(s x, y) -> plus#(y, times(x, y)))
      (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
      (exp#(x, s y) -> times#(x, exp(x, y)), times#(s x, y) -> times#(x, y))
      (exp#(x, s y) -> times#(x, exp(x, y)), times#(s x, y) -> plus#(y, times(x, y)))
      (towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z), help#(false(), c, x, y, z) -> towerIter#(s c, x, y, exp(y, z)))
      (towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z), help#(false(), c, x, y, z) -> exp#(y, z))
      (help#(false(), c, x, y, z) -> towerIter#(s c, x, y, exp(y, z)), towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z))
      (help#(false(), c, x, y, z) -> towerIter#(s c, x, y, exp(y, z)), towerIter#(c, x, y, z) -> ge#(c, x))
      (towerIter#(c, x, y, z) -> ge#(c, x), ge#(s x, s y) -> ge#(x, y))
      (tower#(x, y) -> towerIter#(0(), x, y, s 0()), towerIter#(c, x, y, z) -> ge#(c, x))
      (tower#(x, y) -> towerIter#(0(), x, y, s 0()), towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z))
      (help#(false(), c, x, y, z) -> exp#(y, z), exp#(x, s y) -> times#(x, exp(x, y)))
      (help#(false(), c, x, y, z) -> exp#(y, z), exp#(x, s y) -> exp#(x, y))
      (times#(s x, y) -> plus#(y, times(x, y)), plus#(s x, y) -> plus#(x, y))
      (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))
      (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))}
     STATUS:
      arrows: 0.851240
      SCCS (5):
       Scc:
        {    towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z),
         help#(false(), c, x, y, z) -> towerIter#(s c, x, y, exp(y, z))}
       Scc:
        {ge#(s x, s y) -> ge#(x, y)}
       Scc:
        {exp#(x, s y) -> exp#(x, y)}
       Scc:
        {times#(s x, y) -> times#(x, y)}
       Scc:
        {plus#(s x, y) -> plus#(x, y)}
       
       
       SCC (2):
        Strict:
         {    towerIter#(c, x, y, z) -> help#(ge(c, x), c, x, y, z),
          help#(false(), c, x, y, z) -> towerIter#(s c, x, y, exp(y, z))}
        Weak:
        {             plus(0(), x) -> x,
                      plus(s x, y) -> s plus(x, y),
                     times(0(), y) -> 0(),
                     times(s x, y) -> plus(y, times(x, y)),
                       exp(x, 0()) -> s 0(),
                       exp(x, s y) -> times(x, exp(x, y)),
                        ge(x, 0()) -> true(),
                      ge(0(), s x) -> false(),
                      ge(s x, s y) -> ge(x, y),
             towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z),
                       tower(x, y) -> towerIter(0(), x, y, s 0()),
          help(true(), c, x, y, z) -> z,
         help(false(), c, x, y, z) -> towerIter(s c, x, y, exp(y, z))}
        Open
       
       
       SCC (1):
        Strict:
         {ge#(s x, s y) -> ge#(x, y)}
        Weak:
        {             plus(0(), x) -> x,
                      plus(s x, y) -> s plus(x, y),
                     times(0(), y) -> 0(),
                     times(s x, y) -> plus(y, times(x, y)),
                       exp(x, 0()) -> s 0(),
                       exp(x, s y) -> times(x, exp(x, y)),
                        ge(x, 0()) -> true(),
                      ge(0(), s x) -> false(),
                      ge(s x, s y) -> ge(x, y),
             towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z),
                       tower(x, y) -> towerIter(0(), x, y, s 0()),
          help(true(), c, x, y, z) -> z,
         help(false(), c, x, y, z) -> towerIter(s c, x, y, exp(y, z))}
        Open
       SCC (1):
        Strict:
         {exp#(x, s y) -> exp#(x, y)}
        Weak:
        {             plus(0(), x) -> x,
                      plus(s x, y) -> s plus(x, y),
                     times(0(), y) -> 0(),
                     times(s x, y) -> plus(y, times(x, y)),
                       exp(x, 0()) -> s 0(),
                       exp(x, s y) -> times(x, exp(x, y)),
                        ge(x, 0()) -> true(),
                      ge(0(), s x) -> false(),
                      ge(s x, s y) -> ge(x, y),
             towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z),
                       tower(x, y) -> towerIter(0(), x, y, s 0()),
          help(true(), c, x, y, z) -> z,
         help(false(), c, x, y, z) -> towerIter(s c, x, y, exp(y, z))}
        Open
       
       SCC (1):
        Strict:
         {times#(s x, y) -> times#(x, y)}
        Weak:
        {             plus(0(), x) -> x,
                      plus(s x, y) -> s plus(x, y),
                     times(0(), y) -> 0(),
                     times(s x, y) -> plus(y, times(x, y)),
                       exp(x, 0()) -> s 0(),
                       exp(x, s y) -> times(x, exp(x, y)),
                        ge(x, 0()) -> true(),
                      ge(0(), s x) -> false(),
                      ge(s x, s y) -> ge(x, y),
             towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z),
                       tower(x, y) -> towerIter(0(), x, y, s 0()),
          help(true(), c, x, y, z) -> z,
         help(false(), c, x, y, z) -> towerIter(s c, x, y, exp(y, z))}
        Open
       
       SCC (1):
        Strict:
         {plus#(s x, y) -> plus#(x, y)}
        Weak:
        {             plus(0(), x) -> x,
                      plus(s x, y) -> s plus(x, y),
                     times(0(), y) -> 0(),
                     times(s x, y) -> plus(y, times(x, y)),
                       exp(x, 0()) -> s 0(),
                       exp(x, s y) -> times(x, exp(x, y)),
                        ge(x, 0()) -> true(),
                      ge(0(), s x) -> false(),
                      ge(s x, s y) -> ge(x, y),
             towerIter(c, x, y, z) -> help(ge(c, x), c, x, y, z),
                       tower(x, y) -> towerIter(0(), x, y, s 0()),
          help(true(), c, x, y, z) -> z,
         help(false(), c, x, y, z) -> towerIter(s c, x, y, exp(y, z))}
        Open