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)
  , 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) }
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:
     { 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))
     , a__indx^#(X1, X2) -> c_19(X1, X2)
     , a__indx^#(nil(), X) -> c_20()
     , a__indx^#(cons(X, Y), Z) -> c_21(X, Z, Y, Z)
     , a__from^#(X) -> c_22(X, X)
     , a__from^#(X) -> c_23(X) }
   
   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))
     , a__indx^#(X1, X2) -> c_19(X1, X2)
     , a__indx^#(nil(), X) -> c_20()
     , a__indx^#(cons(X, Y), Z) -> c_21(X, Z, Y, Z)
     , a__from^#(X) -> c_22(X, X)
     , a__from^#(X) -> c_23(X) }
   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)
     , 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) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {2,5,10,13,20} by
   applications of Pre({2,5,10,13,20}) =
   {1,3,4,6,7,8,11,12,14,15,17,19,21,22,23}. 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: a__indx^#(X1, X2) -> c_19(X1, X2)
       , 20: a__indx^#(nil(), X) -> c_20()
       , 21: a__indx^#(cons(X, Y), Z) -> c_21(X, Z, Y, Z)
       , 22: a__from^#(X) -> c_22(X, X)
       , 23: a__from^#(X) -> c_23(X) }
   
   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))
     , a__indx^#(X1, X2) -> c_19(X1, X2)
     , a__indx^#(cons(X, Y), Z) -> c_21(X, Z, Y, Z)
     , a__from^#(X) -> c_22(X, X)
     , a__from^#(X) -> c_23(X) }
   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)
     , 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) }
   Weak DPs:
     { a__dbl^#(0()) -> c_2()
     , a__dbls^#(nil()) -> c_5()
     , mark^#(0()) -> c_10()
     , mark^#(nil()) -> c_13()
     , a__indx^#(nil(), X) -> c_20() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..