MAYBE

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

Strict Trs:
  { h(e(x), y) -> h(d(x, y), s(y))
  , d(g(x, y), z) -> g(d(x, z), e(y))
  , d(g(g(0(), x), y), s(z)) -> g(e(x), d(g(g(0(), x), y), z))
  , d(g(g(0(), x), y), 0()) -> e(y)
  , d(g(0(), x), y) -> e(x)
  , g(e(x), e(y)) -> e(g(x, y)) }
Obligation:
  runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 60 seconds)' failed due to the
   following reason:
   
   Computation stopped due to timeout after 60.0 seconds.

2) 'Best' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
      failed due to the following reason:
      
      Computation stopped due to timeout after 30.0 seconds.
   
   2) 'Best' failed due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
         following reason:
         
         The processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
      2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
         to the following reason:
         
         The processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
   
   3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
      due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'Bounds with perSymbol-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
      2) 'Bounds with minimal-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
   

3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
   due to the following reason:
   
   We add the following weak dependency pairs:
   
   Strict DPs:
     { h^#(e(x), y) -> c_1(h^#(d(x, y), s(y)))
     , d^#(g(x, y), z) -> c_2(g^#(d(x, z), e(y)))
     , d^#(g(g(0(), x), y), s(z)) ->
       c_3(g^#(e(x), d(g(g(0(), x), y), z)))
     , d^#(g(g(0(), x), y), 0()) -> c_4(y)
     , d^#(g(0(), x), y) -> c_5(x)
     , g^#(e(x), e(y)) -> c_6(g^#(x, y)) }
   
   and mark the set of starting terms.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { h^#(e(x), y) -> c_1(h^#(d(x, y), s(y)))
     , d^#(g(x, y), z) -> c_2(g^#(d(x, z), e(y)))
     , d^#(g(g(0(), x), y), s(z)) ->
       c_3(g^#(e(x), d(g(g(0(), x), y), z)))
     , d^#(g(g(0(), x), y), 0()) -> c_4(y)
     , d^#(g(0(), x), y) -> c_5(x)
     , g^#(e(x), e(y)) -> c_6(g^#(x, y)) }
   Strict Trs:
     { h(e(x), y) -> h(d(x, y), s(y))
     , d(g(x, y), z) -> g(d(x, z), e(y))
     , d(g(g(0(), x), y), s(z)) -> g(e(x), d(g(g(0(), x), y), z))
     , d(g(g(0(), x), y), 0()) -> e(y)
     , d(g(0(), x), y) -> e(x)
     , g(e(x), e(y)) -> e(g(x, y)) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Consider the dependency graph:
   
     1: h^#(e(x), y) -> c_1(h^#(d(x, y), s(y)))
        -->_1 h^#(e(x), y) -> c_1(h^#(d(x, y), s(y))) :1
     
     2: d^#(g(x, y), z) -> c_2(g^#(d(x, z), e(y)))
        -->_1 g^#(e(x), e(y)) -> c_6(g^#(x, y)) :6
     
     3: d^#(g(g(0(), x), y), s(z)) ->
        c_3(g^#(e(x), d(g(g(0(), x), y), z)))
        -->_1 g^#(e(x), e(y)) -> c_6(g^#(x, y)) :6
     
     4: d^#(g(g(0(), x), y), 0()) -> c_4(y)
        -->_1 g^#(e(x), e(y)) -> c_6(g^#(x, y)) :6
        -->_1 d^#(g(0(), x), y) -> c_5(x) :5
        -->_1 d^#(g(g(0(), x), y), 0()) -> c_4(y) :4
        -->_1 d^#(g(g(0(), x), y), s(z)) ->
              c_3(g^#(e(x), d(g(g(0(), x), y), z))) :3
        -->_1 d^#(g(x, y), z) -> c_2(g^#(d(x, z), e(y))) :2
        -->_1 h^#(e(x), y) -> c_1(h^#(d(x, y), s(y))) :1
     
     5: d^#(g(0(), x), y) -> c_5(x)
        -->_1 g^#(e(x), e(y)) -> c_6(g^#(x, y)) :6
        -->_1 d^#(g(0(), x), y) -> c_5(x) :5
        -->_1 d^#(g(g(0(), x), y), 0()) -> c_4(y) :4
        -->_1 d^#(g(g(0(), x), y), s(z)) ->
              c_3(g^#(e(x), d(g(g(0(), x), y), z))) :3
        -->_1 d^#(g(x, y), z) -> c_2(g^#(d(x, z), e(y))) :2
        -->_1 h^#(e(x), y) -> c_1(h^#(d(x, y), s(y))) :1
     
     6: g^#(e(x), e(y)) -> c_6(g^#(x, y))
        -->_1 g^#(e(x), e(y)) -> c_6(g^#(x, y)) :6
     
   
   Only the nodes {1,6} are reachable from nodes {1,6} that start
   derivation from marked basic terms. The nodes not reachable are
   removed from the problem.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { h^#(e(x), y) -> c_1(h^#(d(x, y), s(y)))
     , g^#(e(x), e(y)) -> c_6(g^#(x, y)) }
   Strict Trs:
     { h(e(x), y) -> h(d(x, y), s(y))
     , d(g(x, y), z) -> g(d(x, z), e(y))
     , d(g(g(0(), x), y), s(z)) -> g(e(x), d(g(g(0(), x), y), z))
     , d(g(g(0(), x), y), 0()) -> e(y)
     , d(g(0(), x), y) -> e(x)
     , g(e(x), e(y)) -> e(g(x, y)) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..