MAYBE

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

Strict Trs:
  { rec[mapL_0][2](NilL()) -> NilL()
  , rec[mapL_0][2](ConsL(x2, x1)) ->
    ConsL(rec[dc_0][1](x2), rec[mapL_0][2](x1))
  , rec[dc_0][1](Nil()) -> Nil()
  , rec[dc_0][1](Cons(x77, Nil())) -> Cons(x77, Nil())
  , rec[dc_0][1](Cons(x3, Cons(x2, x1))) ->
    const_f[2](Cons(x3, Cons(x2, x1)),
               rec[mapL_0][2](ConsL(Cons(x3,
                                         rec[take_0][2](rec[halve_0][1](rec[length_0][1](x1)),
                                                        Cons(x2, x1))),
                                    ConsL(rec[drop_0][2](rec[halve_0][1](rec[length_0][1](x1)),
                                                         Cons(x2, x1)),
                                          NilL()))))
  , rec[length_0][1](Nil()) -> 0()
  , rec[length_0][1](Cons(x13, x17)) -> S(rec[length_0][1](x17))
  , rec[halve_0][1](0()) -> 0()
  , rec[halve_0][1](S(0())) -> S(0())
  , rec[halve_0][1](S(S(x17))) -> S(rec[halve_0][1](x17))
  , rec[take_0][2](0(), x26) -> Nil()
  , rec[take_0][2](S(x14), Cons(x10, x6)) ->
    Cons(x10, rec[take_0][2](x14, x6))
  , rec[take_0][2](S(0()), Nil()) ->
    Cons(Head_error_empty_list(), Nil())
  , rec[drop_0][2](0(), x26) -> x26
  , rec[drop_0][2](S(x14), Cons(x10, x6)) -> rec[drop_0][2](x14, x6)
  , rec[drop_0][2](S(0()), Nil()) -> Tail_error_empty_list()
  , const_f[2](Cons(x4, Cons(x5, x6)), ConsL(x3, ConsL(x2, x1))) ->
    rec[merge_0][2](x3, x2)
  , rec[merge_0][2](Nil(), x58) -> x58
  , rec[merge_0][2](Cons(x66, x74), Nil()) -> Cons(x66, x74)
  , rec[merge_0][2](Cons(x18, x14), Cons(x10, x6)) ->
    merge_cond_2(rec[leq_0][2](x18, x10),
                 Cons(x18, x14),
                 Cons(x10, x6),
                 x18,
                 x14,
                 x10,
                 x6)
  , merge_cond_2(True(),
                 Cons(x15, x17),
                 Cons(x11, x13),
                 x9,
                 x7,
                 x5,
                 x3)
    -> Cons(x9, rec[merge_0][2](x7, Cons(x11, x13)))
  , merge_cond_2(False(),
                 Cons(x15, x17),
                 Cons(x11, x13),
                 x9,
                 x7,
                 x5,
                 x3)
    -> Cons(x5, rec[merge_0][2](Cons(x15, x17), x3))
  , rec[leq_0][2](0(), x106) -> True()
  , rec[leq_0][2](S(x114), 0()) -> False()
  , rec[leq_0][2](S(x10), S(x6)) -> rec[leq_0][2](x10, x6)
  , main(x43) -> rec[dc_0][1](x43) }
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) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
            following reason:
            
            The input cannot be shown compatible
         
         2) 'Polynomial Path Order (PS) (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..