MAYBE

Problem:
 plus(0(),x) -> x
 plus(s(x),y) -> s(plus(p(s(x)),y))
 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))
 p(s(0())) -> 0()
 p(s(s(x))) -> s(p(s(x)))
 tower(x,y) -> towerIter(x,y,s(0()))
 towerIter(0(),y,z) -> z
 towerIter(s(x),y,z) -> towerIter(p(s(x)),y,exp(y,z))

Proof:
 DP Processor:
  DPs:
   plus#(s(x),y) -> p#(s(x))
   plus#(s(x),y) -> plus#(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))
   exp#(x,s(y)) -> exp#(x,y)
   exp#(x,s(y)) -> times#(x,exp(x,y))
   p#(s(s(x))) -> p#(s(x))
   tower#(x,y) -> towerIter#(x,y,s(0()))
   towerIter#(s(x),y,z) -> exp#(y,z)
   towerIter#(s(x),y,z) -> p#(s(x))
   towerIter#(s(x),y,z) -> towerIter#(p(s(x)),y,exp(y,z))
  TRS:
   plus(0(),x) -> x
   plus(s(x),y) -> s(plus(p(s(x)),y))
   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))
   p(s(0())) -> 0()
   p(s(s(x))) -> s(p(s(x)))
   tower(x,y) -> towerIter(x,y,s(0()))
   towerIter(0(),y,z) -> z
   towerIter(s(x),y,z) -> towerIter(p(s(x)),y,exp(y,z))
  Usable Rule Processor:
   DPs:
    plus#(s(x),y) -> p#(s(x))
    plus#(s(x),y) -> plus#(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))
    exp#(x,s(y)) -> exp#(x,y)
    exp#(x,s(y)) -> times#(x,exp(x,y))
    p#(s(s(x))) -> p#(s(x))
    tower#(x,y) -> towerIter#(x,y,s(0()))
    towerIter#(s(x),y,z) -> exp#(y,z)
    towerIter#(s(x),y,z) -> p#(s(x))
    towerIter#(s(x),y,z) -> towerIter#(p(s(x)),y,exp(y,z))
   TRS:
    f14(x,y) -> x
    f14(x,y) -> 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))
    plus(0(),x) -> x
    plus(s(x),y) -> s(plus(p(s(x)),y))
    exp(x,0()) -> s(0())
    exp(x,s(y)) -> times(x,exp(x,y))
   ADG Processor:
    DPs:
     plus#(s(x),y) -> p#(s(x))
     plus#(s(x),y) -> plus#(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))
     exp#(x,s(y)) -> exp#(x,y)
     exp#(x,s(y)) -> times#(x,exp(x,y))
     p#(s(s(x))) -> p#(s(x))
     tower#(x,y) -> towerIter#(x,y,s(0()))
     towerIter#(s(x),y,z) -> exp#(y,z)
     towerIter#(s(x),y,z) -> p#(s(x))
     towerIter#(s(x),y,z) -> towerIter#(p(s(x)),y,exp(y,z))
    TRS:
     f14(x,y) -> x
     f14(x,y) -> 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))
     plus(0(),x) -> x
     plus(s(x),y) -> s(plus(p(s(x)),y))
     exp(x,0()) -> s(0())
     exp(x,s(y)) -> times(x,exp(x,y))
    graph:
     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))
     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) ->
     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) -> p#(s(x)) ->
     p#(s(s(x))) -> 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) -> p#(s(x))
     tower#(x,y) -> towerIter#(x,y,s(0())) ->
     towerIter#(s(x),y,z) -> towerIter#(p(s(x)),y,exp(y,z))
     exp#(x,s(y)) -> 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))
     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)
     exp#(x,s(y)) -> times#(x,exp(x,y)) ->
     times#(s(x),y) -> plus#(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) -> times#(p(s(x)),y)
     times#(s(x),y) -> times#(p(s(x)),y) ->
     times#(s(x),y) -> plus#(y,times(p(s(x)),y))
     times#(s(x),y) -> p#(s(x)) ->
     p#(s(s(x))) -> p#(s(x))
     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)
     p#(s(s(x))) -> 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) -> p#(s(x))
     plus#(s(x),y) -> plus#(p(s(x)),y) -> plus#(s(x),y) -> plus#(p(s(x)),y)
    Restore Modifier:
     DPs:
      plus#(s(x),y) -> p#(s(x))
      plus#(s(x),y) -> plus#(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))
      exp#(x,s(y)) -> exp#(x,y)
      exp#(x,s(y)) -> times#(x,exp(x,y))
      p#(s(s(x))) -> p#(s(x))
      tower#(x,y) -> towerIter#(x,y,s(0()))
      towerIter#(s(x),y,z) -> exp#(y,z)
      towerIter#(s(x),y,z) -> p#(s(x))
      towerIter#(s(x),y,z) -> towerIter#(p(s(x)),y,exp(y,z))
     TRS:
      plus(0(),x) -> x
      plus(s(x),y) -> s(plus(p(s(x)),y))
      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))
      p(s(0())) -> 0()
      p(s(s(x))) -> s(p(s(x)))
      tower(x,y) -> towerIter(x,y,s(0()))
      towerIter(0(),y,z) -> z
      towerIter(s(x),y,z) -> towerIter(p(s(x)),y,exp(y,z))
     SCC Processor:
      #sccs: 5
      #rules: 5
      #arcs: 24/144
      DPs:
       towerIter#(s(x),y,z) -> towerIter#(p(s(x)),y,exp(y,z))
      TRS:
       plus(0(),x) -> x
       plus(s(x),y) -> s(plus(p(s(x)),y))
       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))
       p(s(0())) -> 0()
       p(s(s(x))) -> s(p(s(x)))
       tower(x,y) -> towerIter(x,y,s(0()))
       towerIter(0(),y,z) -> z
       towerIter(s(x),y,z) -> towerIter(p(s(x)),y,exp(y,z))
      Open
      
      DPs:
       exp#(x,s(y)) -> exp#(x,y)
      TRS:
       plus(0(),x) -> x
       plus(s(x),y) -> s(plus(p(s(x)),y))
       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))
       p(s(0())) -> 0()
       p(s(s(x))) -> s(p(s(x)))
       tower(x,y) -> towerIter(x,y,s(0()))
       towerIter(0(),y,z) -> z
       towerIter(s(x),y,z) -> towerIter(p(s(x)),y,exp(y,z))
      Open
      
      DPs:
       times#(s(x),y) -> times#(p(s(x)),y)
      TRS:
       plus(0(),x) -> x
       plus(s(x),y) -> s(plus(p(s(x)),y))
       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))
       p(s(0())) -> 0()
       p(s(s(x))) -> s(p(s(x)))
       tower(x,y) -> towerIter(x,y,s(0()))
       towerIter(0(),y,z) -> z
       towerIter(s(x),y,z) -> towerIter(p(s(x)),y,exp(y,z))
      Open
      
      DPs:
       plus#(s(x),y) -> plus#(p(s(x)),y)
      TRS:
       plus(0(),x) -> x
       plus(s(x),y) -> s(plus(p(s(x)),y))
       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))
       p(s(0())) -> 0()
       p(s(s(x))) -> s(p(s(x)))
       tower(x,y) -> towerIter(x,y,s(0()))
       towerIter(0(),y,z) -> z
       towerIter(s(x),y,z) -> towerIter(p(s(x)),y,exp(y,z))
      Open
      
      DPs:
       p#(s(s(x))) -> p#(s(x))
      TRS:
       plus(0(),x) -> x
       plus(s(x),y) -> s(plus(p(s(x)),y))
       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))
       p(s(0())) -> 0()
       p(s(s(x))) -> s(p(s(x)))
       tower(x,y) -> towerIter(x,y,s(0()))
       towerIter(0(),y,z) -> z
       towerIter(s(x),y,z) -> towerIter(p(s(x)),y,exp(y,z))
      Open