MAYBE

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

Strict Trs:
  { evalState_cond(Pair(x9, x11)) -> x11
  , rec[plus_0][2](0(), x50) -> x50
  , rec[plus_0][2](S(x10), x6) -> S(rec[plus_0][2](x10, x6))
  , find_cond_2(True(), x15, x21, x25) -> Some(x25)
  , find_cond_2(False(), x58, x4, x7) -> find_key[1](x58, x4)
  , find_key[1](x29, Nil()) -> None()
  , find_key[1](x9, Cons(Pair(x7, x5), x3)) ->
    find_cond_2(rec[equal_0][2](x7, x9), x9, x3, x5)
  , rec[equal_0][2](0(), 0()) -> True()
  , rec[equal_0][2](0(), S(x122)) -> False()
  , rec[equal_0][2](S(x122), 0()) -> False()
  , rec[equal_0][2](S(x10), S(x6)) -> rec[equal_0][2](x10, x6)
  , bind_cond(Pair(x337, x152), memoM_1(x209)) ->
    Pair(Cons(Pair(x209, x152), x337), x152)
  , bind_cond(Pair(x2, x4),
              liftM2_0(bind_m_f(bind_m_f(get(), liftM_0(find_key(x8))),
                                memoM_0(x6))))
    ->
    bind_cond(bind_cond(Pair(x2, find_key[1](x8, x2)), memoM_0(x6)),
              liftM2_1(x4))
  , bind_cond(Pair(x3, x2), liftM2_1(x1)) ->
    Pair(x3, rec[plus_0][2](x1, x2))
  , bind_cond(Pair(x84, Some(x76)), memoM_0(x22)) -> Pair(x84, x76)
  , bind_cond(Pair(x9, None()), memoM_0(0())) ->
    bind_m_f[1](memoM_1(0()), x9)
  , bind_cond(Pair(x9, None()), memoM_0(S(0()))) ->
    bind_m_f[1](memoM_1(S(0())), x9)
  , bind_cond(Pair(x2, None()), memoM_0(S(S(x1)))) ->
    bind_cond(bind_cond(bind_cond(Pair(x2, find_key[1](S(x1), x2)),
                                  memoM_0(S(x1))),
                        liftM2_0(bind_m_f(bind_m_f(get(), liftM_0(find_key(x1))),
                                          memoM_0(x1)))),
              memoM_1(S(S(x1))))
  , bind_m_f[1](x2, x1) -> bind_cond(Pair(x1, S(0())), x2)
  , main(0()) -> S(0())
  , main(S(0())) -> S(0())
  , main(S(S(x1))) ->
    evalState_cond(bind_cond(bind_cond(Pair(Nil(), None()),
                                       memoM_0(S(x1))),
                             liftM2_0(bind_m_f(bind_m_f(get(), liftM_0(find_key(x1))),
                                               memoM_0(x1))))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.

2) 'Best' failed due to the following reason:
   
   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) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
            to the following reason:
            
            The input cannot be shown compatible
         
         2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
            following reason:
            
            The input cannot be shown compatible
         
      
      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 minimal-enrichment and initial automaton 'match''
            failed due to the following reason:
            
            match-boundness of the problem could not be verified.
         
         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
            failed due to the following reason:
            
            match-boundness of the problem could not be verified.
         
      
   


Arrrr..