MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict 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))
  , 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)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { plus^#(0(), x) -> c_1()
  , plus^#(s(x), y) -> c_2(plus^#(p(s(x)), y), p^#(s(x)))
  , p^#(s(0())) -> c_3()
  , p^#(s(s(x))) -> c_4(p^#(s(x)))
  , times^#(0(), y) -> c_5()
  , times^#(s(x), y) ->
    c_6(plus^#(y, times(p(s(x)), y)), times^#(p(s(x)), y), p^#(s(x)))
  , exp^#(x, 0()) -> c_7()
  , exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y))
  , tower^#(x, y) -> c_9(towerIter^#(x, y, s(0())))
  , towerIter^#(0(), y, z) -> c_10()
  , towerIter^#(s(x), y, z) ->
    c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { plus^#(0(), x) -> c_1()
  , plus^#(s(x), y) -> c_2(plus^#(p(s(x)), y), p^#(s(x)))
  , p^#(s(0())) -> c_3()
  , p^#(s(s(x))) -> c_4(p^#(s(x)))
  , times^#(0(), y) -> c_5()
  , times^#(s(x), y) ->
    c_6(plus^#(y, times(p(s(x)), y)), times^#(p(s(x)), y), p^#(s(x)))
  , exp^#(x, 0()) -> c_7()
  , exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y))
  , tower^#(x, y) -> c_9(towerIter^#(x, y, s(0())))
  , towerIter^#(0(), y, z) -> c_10()
  , towerIter^#(s(x), y, z) ->
    c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) }
Weak 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))
  , 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)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {1,3,5,7,10} by
applications of Pre({1,3,5,7,10}) = {2,4,6,8,9,11}. Here rules are
labeled as follows:

  DPs:
    { 1: plus^#(0(), x) -> c_1()
    , 2: plus^#(s(x), y) -> c_2(plus^#(p(s(x)), y), p^#(s(x)))
    , 3: p^#(s(0())) -> c_3()
    , 4: p^#(s(s(x))) -> c_4(p^#(s(x)))
    , 5: times^#(0(), y) -> c_5()
    , 6: times^#(s(x), y) ->
         c_6(plus^#(y, times(p(s(x)), y)), times^#(p(s(x)), y), p^#(s(x)))
    , 7: exp^#(x, 0()) -> c_7()
    , 8: exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y))
    , 9: tower^#(x, y) -> c_9(towerIter^#(x, y, s(0())))
    , 10: towerIter^#(0(), y, z) -> c_10()
    , 11: towerIter^#(s(x), y, z) ->
          c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { plus^#(s(x), y) -> c_2(plus^#(p(s(x)), y), p^#(s(x)))
  , p^#(s(s(x))) -> c_4(p^#(s(x)))
  , times^#(s(x), y) ->
    c_6(plus^#(y, times(p(s(x)), y)), times^#(p(s(x)), y), p^#(s(x)))
  , exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y))
  , tower^#(x, y) -> c_9(towerIter^#(x, y, s(0())))
  , towerIter^#(s(x), y, z) ->
    c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) }
Weak DPs:
  { plus^#(0(), x) -> c_1()
  , p^#(s(0())) -> c_3()
  , times^#(0(), y) -> c_5()
  , exp^#(x, 0()) -> c_7()
  , towerIter^#(0(), y, z) -> c_10() }
Weak 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))
  , 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)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ plus^#(0(), x) -> c_1()
, p^#(s(0())) -> c_3()
, times^#(0(), y) -> c_5()
, exp^#(x, 0()) -> c_7()
, towerIter^#(0(), y, z) -> c_10() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { plus^#(s(x), y) -> c_2(plus^#(p(s(x)), y), p^#(s(x)))
  , p^#(s(s(x))) -> c_4(p^#(s(x)))
  , times^#(s(x), y) ->
    c_6(plus^#(y, times(p(s(x)), y)), times^#(p(s(x)), y), p^#(s(x)))
  , exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y))
  , tower^#(x, y) -> c_9(towerIter^#(x, y, s(0())))
  , towerIter^#(s(x), y, z) ->
    c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) }
Weak 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))
  , 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)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: plus^#(s(x), y) -> c_2(plus^#(p(s(x)), y), p^#(s(x)))
     -->_2 p^#(s(s(x))) -> c_4(p^#(s(x))) :2
     -->_1 plus^#(s(x), y) -> c_2(plus^#(p(s(x)), y), p^#(s(x))) :1
  
  2: p^#(s(s(x))) -> c_4(p^#(s(x)))
     -->_1 p^#(s(s(x))) -> c_4(p^#(s(x))) :2
  
  3: times^#(s(x), y) ->
     c_6(plus^#(y, times(p(s(x)), y)), times^#(p(s(x)), y), p^#(s(x)))
     -->_2 times^#(s(x), y) ->
           c_6(plus^#(y, times(p(s(x)), y)),
               times^#(p(s(x)), y),
               p^#(s(x))) :3
     -->_3 p^#(s(s(x))) -> c_4(p^#(s(x))) :2
     -->_1 plus^#(s(x), y) -> c_2(plus^#(p(s(x)), y), p^#(s(x))) :1
  
  4: exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y))
     -->_2 exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y)) :4
     -->_1 times^#(s(x), y) ->
           c_6(plus^#(y, times(p(s(x)), y)),
               times^#(p(s(x)), y),
               p^#(s(x))) :3
  
  5: tower^#(x, y) -> c_9(towerIter^#(x, y, s(0())))
     -->_1 towerIter^#(s(x), y, z) ->
           c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) :6
  
  6: towerIter^#(s(x), y, z) ->
     c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z))
     -->_1 towerIter^#(s(x), y, z) ->
           c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) :6
     -->_3 exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y)) :4
     -->_2 p^#(s(s(x))) -> c_4(p^#(s(x))) :2
  

Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).

  { tower^#(x, y) -> c_9(towerIter^#(x, y, s(0()))) }


We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { plus^#(s(x), y) -> c_2(plus^#(p(s(x)), y), p^#(s(x)))
  , p^#(s(s(x))) -> c_4(p^#(s(x)))
  , times^#(s(x), y) ->
    c_6(plus^#(y, times(p(s(x)), y)), times^#(p(s(x)), y), p^#(s(x)))
  , exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y))
  , towerIter^#(s(x), y, z) ->
    c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) }
Weak 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))
  , 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)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { 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)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { plus^#(s(x), y) -> c_2(plus^#(p(s(x)), y), p^#(s(x)))
  , p^#(s(s(x))) -> c_4(p^#(s(x)))
  , times^#(s(x), y) ->
    c_6(plus^#(y, times(p(s(x)), y)), times^#(p(s(x)), y), p^#(s(x)))
  , exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y))
  , towerIter^#(s(x), y, z) ->
    c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) }
Weak 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)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'matrices' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'matrix interpretation of dimension 4' failed due to the
      following reason:
      
      Following exception was raised:
        stack overflow
   
   2) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   4) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   5) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   6) 'matrix interpretation of dimension 1' failed due to the
      following reason:
      
      The input cannot be shown compatible
   

2) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.


Arrrr..