MAYBE

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

Strict Trs:
  { a__dbl(X) -> dbl(X)
  , a__dbl(0()) -> 0()
  , a__dbl(s(X)) -> s(s(dbl(X)))
  , a__dbls(X) -> dbls(X)
  , a__dbls(nil()) -> nil()
  , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
  , a__sel(X1, X2) -> sel(X1, X2)
  , a__sel(0(), cons(X, Y)) -> mark(X)
  , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z))
  , mark(0()) -> 0()
  , mark(s(X)) -> s(X)
  , mark(dbl(X)) -> a__dbl(mark(X))
  , mark(nil()) -> nil()
  , mark(cons(X1, X2)) -> cons(X1, X2)
  , mark(dbls(X)) -> a__dbls(mark(X))
  , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2))
  , mark(indx(X1, X2)) -> a__indx(mark(X1), X2)
  , mark(from(X)) -> a__from(X)
  , mark(01()) -> 01()
  , mark(s1(X)) -> s1(mark(X))
  , mark(dbl1(X)) -> a__dbl1(mark(X))
  , mark(sel1(X1, X2)) -> a__sel1(mark(X1), mark(X2))
  , mark(quote(X)) -> a__quote(mark(X))
  , a__indx(X1, X2) -> indx(X1, X2)
  , a__indx(nil(), X) -> nil()
  , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
  , a__from(X) -> cons(X, from(s(X)))
  , a__from(X) -> from(X)
  , a__dbl1(X) -> dbl1(X)
  , a__dbl1(0()) -> 01()
  , a__dbl1(s(X)) -> s1(s1(a__dbl1(mark(X))))
  , a__sel1(X1, X2) -> sel1(X1, X2)
  , a__sel1(0(), cons(X, Y)) -> mark(X)
  , a__sel1(s(X), cons(Y, Z)) -> a__sel1(mark(X), mark(Z))
  , a__quote(X) -> quote(X)
  , a__quote(0()) -> 01()
  , a__quote(s(X)) -> s1(a__quote(mark(X)))
  , a__quote(dbl(X)) -> a__dbl1(mark(X))
  , a__quote(sel(X, Y)) -> a__sel1(mark(X), mark(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) '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) '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 processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
      2) '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
      
   

3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
   due to the following reason:
   
   We add the following weak dependency pairs:
   
   Strict DPs:
     { a__dbl^#(X) -> c_1(X)
     , a__dbl^#(0()) -> c_2()
     , a__dbl^#(s(X)) -> c_3(X)
     , a__dbls^#(X) -> c_4(X)
     , a__dbls^#(nil()) -> c_5()
     , a__dbls^#(cons(X, Y)) -> c_6(X, Y)
     , a__sel^#(X1, X2) -> c_7(X1, X2)
     , a__sel^#(0(), cons(X, Y)) -> c_8(mark^#(X))
     , a__sel^#(s(X), cons(Y, Z)) -> c_9(a__sel^#(mark(X), mark(Z)))
     , mark^#(0()) -> c_10()
     , mark^#(s(X)) -> c_11(X)
     , mark^#(dbl(X)) -> c_12(a__dbl^#(mark(X)))
     , mark^#(nil()) -> c_13()
     , mark^#(cons(X1, X2)) -> c_14(X1, X2)
     , mark^#(dbls(X)) -> c_15(a__dbls^#(mark(X)))
     , mark^#(sel(X1, X2)) -> c_16(a__sel^#(mark(X1), mark(X2)))
     , mark^#(indx(X1, X2)) -> c_17(a__indx^#(mark(X1), X2))
     , mark^#(from(X)) -> c_18(a__from^#(X))
     , mark^#(01()) -> c_19()
     , mark^#(s1(X)) -> c_20(mark^#(X))
     , mark^#(dbl1(X)) -> c_21(a__dbl1^#(mark(X)))
     , mark^#(sel1(X1, X2)) -> c_22(a__sel1^#(mark(X1), mark(X2)))
     , mark^#(quote(X)) -> c_23(a__quote^#(mark(X)))
     , a__indx^#(X1, X2) -> c_24(X1, X2)
     , a__indx^#(nil(), X) -> c_25()
     , a__indx^#(cons(X, Y), Z) -> c_26(X, Z, Y, Z)
     , a__from^#(X) -> c_27(X, X)
     , a__from^#(X) -> c_28(X)
     , a__dbl1^#(X) -> c_29(X)
     , a__dbl1^#(0()) -> c_30()
     , a__dbl1^#(s(X)) -> c_31(a__dbl1^#(mark(X)))
     , a__sel1^#(X1, X2) -> c_32(X1, X2)
     , a__sel1^#(0(), cons(X, Y)) -> c_33(mark^#(X))
     , a__sel1^#(s(X), cons(Y, Z)) -> c_34(a__sel1^#(mark(X), mark(Z)))
     , a__quote^#(X) -> c_35(X)
     , a__quote^#(0()) -> c_36()
     , a__quote^#(s(X)) -> c_37(a__quote^#(mark(X)))
     , a__quote^#(dbl(X)) -> c_38(a__dbl1^#(mark(X)))
     , a__quote^#(sel(X, Y)) -> c_39(a__sel1^#(mark(X), mark(Y))) }
   
   and mark the set of starting terms.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { a__dbl^#(X) -> c_1(X)
     , a__dbl^#(0()) -> c_2()
     , a__dbl^#(s(X)) -> c_3(X)
     , a__dbls^#(X) -> c_4(X)
     , a__dbls^#(nil()) -> c_5()
     , a__dbls^#(cons(X, Y)) -> c_6(X, Y)
     , a__sel^#(X1, X2) -> c_7(X1, X2)
     , a__sel^#(0(), cons(X, Y)) -> c_8(mark^#(X))
     , a__sel^#(s(X), cons(Y, Z)) -> c_9(a__sel^#(mark(X), mark(Z)))
     , mark^#(0()) -> c_10()
     , mark^#(s(X)) -> c_11(X)
     , mark^#(dbl(X)) -> c_12(a__dbl^#(mark(X)))
     , mark^#(nil()) -> c_13()
     , mark^#(cons(X1, X2)) -> c_14(X1, X2)
     , mark^#(dbls(X)) -> c_15(a__dbls^#(mark(X)))
     , mark^#(sel(X1, X2)) -> c_16(a__sel^#(mark(X1), mark(X2)))
     , mark^#(indx(X1, X2)) -> c_17(a__indx^#(mark(X1), X2))
     , mark^#(from(X)) -> c_18(a__from^#(X))
     , mark^#(01()) -> c_19()
     , mark^#(s1(X)) -> c_20(mark^#(X))
     , mark^#(dbl1(X)) -> c_21(a__dbl1^#(mark(X)))
     , mark^#(sel1(X1, X2)) -> c_22(a__sel1^#(mark(X1), mark(X2)))
     , mark^#(quote(X)) -> c_23(a__quote^#(mark(X)))
     , a__indx^#(X1, X2) -> c_24(X1, X2)
     , a__indx^#(nil(), X) -> c_25()
     , a__indx^#(cons(X, Y), Z) -> c_26(X, Z, Y, Z)
     , a__from^#(X) -> c_27(X, X)
     , a__from^#(X) -> c_28(X)
     , a__dbl1^#(X) -> c_29(X)
     , a__dbl1^#(0()) -> c_30()
     , a__dbl1^#(s(X)) -> c_31(a__dbl1^#(mark(X)))
     , a__sel1^#(X1, X2) -> c_32(X1, X2)
     , a__sel1^#(0(), cons(X, Y)) -> c_33(mark^#(X))
     , a__sel1^#(s(X), cons(Y, Z)) -> c_34(a__sel1^#(mark(X), mark(Z)))
     , a__quote^#(X) -> c_35(X)
     , a__quote^#(0()) -> c_36()
     , a__quote^#(s(X)) -> c_37(a__quote^#(mark(X)))
     , a__quote^#(dbl(X)) -> c_38(a__dbl1^#(mark(X)))
     , a__quote^#(sel(X, Y)) -> c_39(a__sel1^#(mark(X), mark(Y))) }
   Strict Trs:
     { a__dbl(X) -> dbl(X)
     , a__dbl(0()) -> 0()
     , a__dbl(s(X)) -> s(s(dbl(X)))
     , a__dbls(X) -> dbls(X)
     , a__dbls(nil()) -> nil()
     , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
     , a__sel(X1, X2) -> sel(X1, X2)
     , a__sel(0(), cons(X, Y)) -> mark(X)
     , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z))
     , mark(0()) -> 0()
     , mark(s(X)) -> s(X)
     , mark(dbl(X)) -> a__dbl(mark(X))
     , mark(nil()) -> nil()
     , mark(cons(X1, X2)) -> cons(X1, X2)
     , mark(dbls(X)) -> a__dbls(mark(X))
     , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2))
     , mark(indx(X1, X2)) -> a__indx(mark(X1), X2)
     , mark(from(X)) -> a__from(X)
     , mark(01()) -> 01()
     , mark(s1(X)) -> s1(mark(X))
     , mark(dbl1(X)) -> a__dbl1(mark(X))
     , mark(sel1(X1, X2)) -> a__sel1(mark(X1), mark(X2))
     , mark(quote(X)) -> a__quote(mark(X))
     , a__indx(X1, X2) -> indx(X1, X2)
     , a__indx(nil(), X) -> nil()
     , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
     , a__from(X) -> cons(X, from(s(X)))
     , a__from(X) -> from(X)
     , a__dbl1(X) -> dbl1(X)
     , a__dbl1(0()) -> 01()
     , a__dbl1(s(X)) -> s1(s1(a__dbl1(mark(X))))
     , a__sel1(X1, X2) -> sel1(X1, X2)
     , a__sel1(0(), cons(X, Y)) -> mark(X)
     , a__sel1(s(X), cons(Y, Z)) -> a__sel1(mark(X), mark(Z))
     , a__quote(X) -> quote(X)
     , a__quote(0()) -> 01()
     , a__quote(s(X)) -> s1(a__quote(mark(X)))
     , a__quote(dbl(X)) -> a__dbl1(mark(X))
     , a__quote(sel(X, Y)) -> a__sel1(mark(X), mark(Y)) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {2,5,10,13,19,25,30,36} by
   applications of Pre({2,5,10,13,19,25,30,36}) =
   {1,3,4,6,7,8,11,12,14,15,17,20,21,23,24,26,27,28,29,31,32,33,35,37,38}.
   Here rules are labeled as follows:
   
     DPs:
       { 1: a__dbl^#(X) -> c_1(X)
       , 2: a__dbl^#(0()) -> c_2()
       , 3: a__dbl^#(s(X)) -> c_3(X)
       , 4: a__dbls^#(X) -> c_4(X)
       , 5: a__dbls^#(nil()) -> c_5()
       , 6: a__dbls^#(cons(X, Y)) -> c_6(X, Y)
       , 7: a__sel^#(X1, X2) -> c_7(X1, X2)
       , 8: a__sel^#(0(), cons(X, Y)) -> c_8(mark^#(X))
       , 9: a__sel^#(s(X), cons(Y, Z)) -> c_9(a__sel^#(mark(X), mark(Z)))
       , 10: mark^#(0()) -> c_10()
       , 11: mark^#(s(X)) -> c_11(X)
       , 12: mark^#(dbl(X)) -> c_12(a__dbl^#(mark(X)))
       , 13: mark^#(nil()) -> c_13()
       , 14: mark^#(cons(X1, X2)) -> c_14(X1, X2)
       , 15: mark^#(dbls(X)) -> c_15(a__dbls^#(mark(X)))
       , 16: mark^#(sel(X1, X2)) -> c_16(a__sel^#(mark(X1), mark(X2)))
       , 17: mark^#(indx(X1, X2)) -> c_17(a__indx^#(mark(X1), X2))
       , 18: mark^#(from(X)) -> c_18(a__from^#(X))
       , 19: mark^#(01()) -> c_19()
       , 20: mark^#(s1(X)) -> c_20(mark^#(X))
       , 21: mark^#(dbl1(X)) -> c_21(a__dbl1^#(mark(X)))
       , 22: mark^#(sel1(X1, X2)) -> c_22(a__sel1^#(mark(X1), mark(X2)))
       , 23: mark^#(quote(X)) -> c_23(a__quote^#(mark(X)))
       , 24: a__indx^#(X1, X2) -> c_24(X1, X2)
       , 25: a__indx^#(nil(), X) -> c_25()
       , 26: a__indx^#(cons(X, Y), Z) -> c_26(X, Z, Y, Z)
       , 27: a__from^#(X) -> c_27(X, X)
       , 28: a__from^#(X) -> c_28(X)
       , 29: a__dbl1^#(X) -> c_29(X)
       , 30: a__dbl1^#(0()) -> c_30()
       , 31: a__dbl1^#(s(X)) -> c_31(a__dbl1^#(mark(X)))
       , 32: a__sel1^#(X1, X2) -> c_32(X1, X2)
       , 33: a__sel1^#(0(), cons(X, Y)) -> c_33(mark^#(X))
       , 34: a__sel1^#(s(X), cons(Y, Z)) ->
             c_34(a__sel1^#(mark(X), mark(Z)))
       , 35: a__quote^#(X) -> c_35(X)
       , 36: a__quote^#(0()) -> c_36()
       , 37: a__quote^#(s(X)) -> c_37(a__quote^#(mark(X)))
       , 38: a__quote^#(dbl(X)) -> c_38(a__dbl1^#(mark(X)))
       , 39: a__quote^#(sel(X, Y)) -> c_39(a__sel1^#(mark(X), mark(Y))) }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { a__dbl^#(X) -> c_1(X)
     , a__dbl^#(s(X)) -> c_3(X)
     , a__dbls^#(X) -> c_4(X)
     , a__dbls^#(cons(X, Y)) -> c_6(X, Y)
     , a__sel^#(X1, X2) -> c_7(X1, X2)
     , a__sel^#(0(), cons(X, Y)) -> c_8(mark^#(X))
     , a__sel^#(s(X), cons(Y, Z)) -> c_9(a__sel^#(mark(X), mark(Z)))
     , mark^#(s(X)) -> c_11(X)
     , mark^#(dbl(X)) -> c_12(a__dbl^#(mark(X)))
     , mark^#(cons(X1, X2)) -> c_14(X1, X2)
     , mark^#(dbls(X)) -> c_15(a__dbls^#(mark(X)))
     , mark^#(sel(X1, X2)) -> c_16(a__sel^#(mark(X1), mark(X2)))
     , mark^#(indx(X1, X2)) -> c_17(a__indx^#(mark(X1), X2))
     , mark^#(from(X)) -> c_18(a__from^#(X))
     , mark^#(s1(X)) -> c_20(mark^#(X))
     , mark^#(dbl1(X)) -> c_21(a__dbl1^#(mark(X)))
     , mark^#(sel1(X1, X2)) -> c_22(a__sel1^#(mark(X1), mark(X2)))
     , mark^#(quote(X)) -> c_23(a__quote^#(mark(X)))
     , a__indx^#(X1, X2) -> c_24(X1, X2)
     , a__indx^#(cons(X, Y), Z) -> c_26(X, Z, Y, Z)
     , a__from^#(X) -> c_27(X, X)
     , a__from^#(X) -> c_28(X)
     , a__dbl1^#(X) -> c_29(X)
     , a__dbl1^#(s(X)) -> c_31(a__dbl1^#(mark(X)))
     , a__sel1^#(X1, X2) -> c_32(X1, X2)
     , a__sel1^#(0(), cons(X, Y)) -> c_33(mark^#(X))
     , a__sel1^#(s(X), cons(Y, Z)) -> c_34(a__sel1^#(mark(X), mark(Z)))
     , a__quote^#(X) -> c_35(X)
     , a__quote^#(s(X)) -> c_37(a__quote^#(mark(X)))
     , a__quote^#(dbl(X)) -> c_38(a__dbl1^#(mark(X)))
     , a__quote^#(sel(X, Y)) -> c_39(a__sel1^#(mark(X), mark(Y))) }
   Strict Trs:
     { a__dbl(X) -> dbl(X)
     , a__dbl(0()) -> 0()
     , a__dbl(s(X)) -> s(s(dbl(X)))
     , a__dbls(X) -> dbls(X)
     , a__dbls(nil()) -> nil()
     , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
     , a__sel(X1, X2) -> sel(X1, X2)
     , a__sel(0(), cons(X, Y)) -> mark(X)
     , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z))
     , mark(0()) -> 0()
     , mark(s(X)) -> s(X)
     , mark(dbl(X)) -> a__dbl(mark(X))
     , mark(nil()) -> nil()
     , mark(cons(X1, X2)) -> cons(X1, X2)
     , mark(dbls(X)) -> a__dbls(mark(X))
     , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2))
     , mark(indx(X1, X2)) -> a__indx(mark(X1), X2)
     , mark(from(X)) -> a__from(X)
     , mark(01()) -> 01()
     , mark(s1(X)) -> s1(mark(X))
     , mark(dbl1(X)) -> a__dbl1(mark(X))
     , mark(sel1(X1, X2)) -> a__sel1(mark(X1), mark(X2))
     , mark(quote(X)) -> a__quote(mark(X))
     , a__indx(X1, X2) -> indx(X1, X2)
     , a__indx(nil(), X) -> nil()
     , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
     , a__from(X) -> cons(X, from(s(X)))
     , a__from(X) -> from(X)
     , a__dbl1(X) -> dbl1(X)
     , a__dbl1(0()) -> 01()
     , a__dbl1(s(X)) -> s1(s1(a__dbl1(mark(X))))
     , a__sel1(X1, X2) -> sel1(X1, X2)
     , a__sel1(0(), cons(X, Y)) -> mark(X)
     , a__sel1(s(X), cons(Y, Z)) -> a__sel1(mark(X), mark(Z))
     , a__quote(X) -> quote(X)
     , a__quote(0()) -> 01()
     , a__quote(s(X)) -> s1(a__quote(mark(X)))
     , a__quote(dbl(X)) -> a__dbl1(mark(X))
     , a__quote(sel(X, Y)) -> a__sel1(mark(X), mark(Y)) }
   Weak DPs:
     { a__dbl^#(0()) -> c_2()
     , a__dbls^#(nil()) -> c_5()
     , mark^#(0()) -> c_10()
     , mark^#(nil()) -> c_13()
     , mark^#(01()) -> c_19()
     , a__indx^#(nil(), X) -> c_25()
     , a__dbl1^#(0()) -> c_30()
     , a__quote^#(0()) -> c_36() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..