MAYBE

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

Strict Trs:
  { sel(X1, X2) -> n__sel(X1, X2)
  , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
  , sel(0(), cons(X, Z)) -> X
  , s(X) -> n__s(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , activate(X) -> X
  , activate(n__first(X1, X2)) -> first(X1, X2)
  , activate(n__from(X)) -> from(X)
  , activate(n__0()) -> 0()
  , activate(n__cons(X1, X2)) -> cons(X1, X2)
  , activate(n__nil()) -> nil()
  , activate(n__s(X)) -> s(X)
  , activate(n__sel(X1, X2)) -> sel(X1, X2)
  , 0() -> n__0()
  , first(X1, X2) -> n__first(X1, X2)
  , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
  , first(0(), Z) -> nil()
  , nil() -> n__nil()
  , from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , sel1(s(X), cons(Y, Z)) -> sel1(X, activate(Z))
  , sel1(0(), cons(X, Z)) -> quote(X)
  , quote(n__0()) -> 01()
  , quote(n__s(X)) -> s1(quote(activate(X)))
  , quote(n__sel(X, Z)) -> sel1(activate(X), activate(Z))
  , first1(s(X), cons(Y, Z)) ->
    cons1(quote(Y), first1(X, activate(Z)))
  , first1(0(), Z) -> nil1()
  , quote1(n__first(X, Z)) -> first1(activate(X), activate(Z))
  , quote1(n__cons(X, Z)) ->
    cons1(quote(activate(X)), quote1(activate(Z)))
  , quote1(n__nil()) -> nil1()
  , unquote(01()) -> 0()
  , unquote(s1(X)) -> s(unquote(X))
  , unquote1(nil1()) -> nil()
  , unquote1(cons1(X, Z)) -> fcons(unquote(X), unquote1(Z))
  , fcons(X, Z) -> cons(X, Z) }
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:
     { sel^#(X1, X2) -> c_1(X1, X2)
     , sel^#(s(X), cons(Y, Z)) -> c_2(sel^#(X, activate(Z)))
     , sel^#(0(), cons(X, Z)) -> c_3(X)
     , s^#(X) -> c_4(X)
     , cons^#(X1, X2) -> c_5(X1, X2)
     , activate^#(X) -> c_6(X)
     , activate^#(n__first(X1, X2)) -> c_7(first^#(X1, X2))
     , activate^#(n__from(X)) -> c_8(from^#(X))
     , activate^#(n__0()) -> c_9(0^#())
     , activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2))
     , activate^#(n__nil()) -> c_11(nil^#())
     , activate^#(n__s(X)) -> c_12(s^#(X))
     , activate^#(n__sel(X1, X2)) -> c_13(sel^#(X1, X2))
     , first^#(X1, X2) -> c_15(X1, X2)
     , first^#(s(X), cons(Y, Z)) ->
       c_16(cons^#(Y, n__first(X, activate(Z))))
     , first^#(0(), Z) -> c_17(nil^#())
     , from^#(X) -> c_19(cons^#(X, n__from(s(X))))
     , from^#(X) -> c_20(X)
     , 0^#() -> c_14()
     , nil^#() -> c_18()
     , sel1^#(s(X), cons(Y, Z)) -> c_21(sel1^#(X, activate(Z)))
     , sel1^#(0(), cons(X, Z)) -> c_22(quote^#(X))
     , quote^#(n__0()) -> c_23()
     , quote^#(n__s(X)) -> c_24(quote^#(activate(X)))
     , quote^#(n__sel(X, Z)) -> c_25(sel1^#(activate(X), activate(Z)))
     , first1^#(s(X), cons(Y, Z)) ->
       c_26(quote^#(Y), first1^#(X, activate(Z)))
     , first1^#(0(), Z) -> c_27()
     , quote1^#(n__first(X, Z)) ->
       c_28(first1^#(activate(X), activate(Z)))
     , quote1^#(n__cons(X, Z)) ->
       c_29(quote^#(activate(X)), quote1^#(activate(Z)))
     , quote1^#(n__nil()) -> c_30()
     , unquote^#(01()) -> c_31(0^#())
     , unquote^#(s1(X)) -> c_32(s^#(unquote(X)))
     , unquote1^#(nil1()) -> c_33(nil^#())
     , unquote1^#(cons1(X, Z)) -> c_34(fcons^#(unquote(X), unquote1(Z)))
     , fcons^#(X, Z) -> c_35(cons^#(X, Z)) }
   
   and mark the set of starting terms.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { sel^#(X1, X2) -> c_1(X1, X2)
     , sel^#(s(X), cons(Y, Z)) -> c_2(sel^#(X, activate(Z)))
     , sel^#(0(), cons(X, Z)) -> c_3(X)
     , s^#(X) -> c_4(X)
     , cons^#(X1, X2) -> c_5(X1, X2)
     , activate^#(X) -> c_6(X)
     , activate^#(n__first(X1, X2)) -> c_7(first^#(X1, X2))
     , activate^#(n__from(X)) -> c_8(from^#(X))
     , activate^#(n__0()) -> c_9(0^#())
     , activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2))
     , activate^#(n__nil()) -> c_11(nil^#())
     , activate^#(n__s(X)) -> c_12(s^#(X))
     , activate^#(n__sel(X1, X2)) -> c_13(sel^#(X1, X2))
     , first^#(X1, X2) -> c_15(X1, X2)
     , first^#(s(X), cons(Y, Z)) ->
       c_16(cons^#(Y, n__first(X, activate(Z))))
     , first^#(0(), Z) -> c_17(nil^#())
     , from^#(X) -> c_19(cons^#(X, n__from(s(X))))
     , from^#(X) -> c_20(X)
     , 0^#() -> c_14()
     , nil^#() -> c_18()
     , sel1^#(s(X), cons(Y, Z)) -> c_21(sel1^#(X, activate(Z)))
     , sel1^#(0(), cons(X, Z)) -> c_22(quote^#(X))
     , quote^#(n__0()) -> c_23()
     , quote^#(n__s(X)) -> c_24(quote^#(activate(X)))
     , quote^#(n__sel(X, Z)) -> c_25(sel1^#(activate(X), activate(Z)))
     , first1^#(s(X), cons(Y, Z)) ->
       c_26(quote^#(Y), first1^#(X, activate(Z)))
     , first1^#(0(), Z) -> c_27()
     , quote1^#(n__first(X, Z)) ->
       c_28(first1^#(activate(X), activate(Z)))
     , quote1^#(n__cons(X, Z)) ->
       c_29(quote^#(activate(X)), quote1^#(activate(Z)))
     , quote1^#(n__nil()) -> c_30()
     , unquote^#(01()) -> c_31(0^#())
     , unquote^#(s1(X)) -> c_32(s^#(unquote(X)))
     , unquote1^#(nil1()) -> c_33(nil^#())
     , unquote1^#(cons1(X, Z)) -> c_34(fcons^#(unquote(X), unquote1(Z)))
     , fcons^#(X, Z) -> c_35(cons^#(X, Z)) }
   Strict Trs:
     { sel(X1, X2) -> n__sel(X1, X2)
     , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
     , sel(0(), cons(X, Z)) -> X
     , s(X) -> n__s(X)
     , cons(X1, X2) -> n__cons(X1, X2)
     , activate(X) -> X
     , activate(n__first(X1, X2)) -> first(X1, X2)
     , activate(n__from(X)) -> from(X)
     , activate(n__0()) -> 0()
     , activate(n__cons(X1, X2)) -> cons(X1, X2)
     , activate(n__nil()) -> nil()
     , activate(n__s(X)) -> s(X)
     , activate(n__sel(X1, X2)) -> sel(X1, X2)
     , 0() -> n__0()
     , first(X1, X2) -> n__first(X1, X2)
     , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
     , first(0(), Z) -> nil()
     , nil() -> n__nil()
     , from(X) -> cons(X, n__from(s(X)))
     , from(X) -> n__from(X)
     , sel1(s(X), cons(Y, Z)) -> sel1(X, activate(Z))
     , sel1(0(), cons(X, Z)) -> quote(X)
     , quote(n__0()) -> 01()
     , quote(n__s(X)) -> s1(quote(activate(X)))
     , quote(n__sel(X, Z)) -> sel1(activate(X), activate(Z))
     , first1(s(X), cons(Y, Z)) ->
       cons1(quote(Y), first1(X, activate(Z)))
     , first1(0(), Z) -> nil1()
     , quote1(n__first(X, Z)) -> first1(activate(X), activate(Z))
     , quote1(n__cons(X, Z)) ->
       cons1(quote(activate(X)), quote1(activate(Z)))
     , quote1(n__nil()) -> nil1()
     , unquote(01()) -> 0()
     , unquote(s1(X)) -> s(unquote(X))
     , unquote1(nil1()) -> nil()
     , unquote1(cons1(X, Z)) -> fcons(unquote(X), unquote1(Z))
     , fcons(X, Z) -> cons(X, Z) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {19,20,23,27,30} by
   applications of Pre({19,20,23,27,30}) =
   {1,3,4,5,6,9,11,14,16,18,22,24,26,28,29,31,33}. Here rules are
   labeled as follows:
   
     DPs:
       { 1: sel^#(X1, X2) -> c_1(X1, X2)
       , 2: sel^#(s(X), cons(Y, Z)) -> c_2(sel^#(X, activate(Z)))
       , 3: sel^#(0(), cons(X, Z)) -> c_3(X)
       , 4: s^#(X) -> c_4(X)
       , 5: cons^#(X1, X2) -> c_5(X1, X2)
       , 6: activate^#(X) -> c_6(X)
       , 7: activate^#(n__first(X1, X2)) -> c_7(first^#(X1, X2))
       , 8: activate^#(n__from(X)) -> c_8(from^#(X))
       , 9: activate^#(n__0()) -> c_9(0^#())
       , 10: activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2))
       , 11: activate^#(n__nil()) -> c_11(nil^#())
       , 12: activate^#(n__s(X)) -> c_12(s^#(X))
       , 13: activate^#(n__sel(X1, X2)) -> c_13(sel^#(X1, X2))
       , 14: first^#(X1, X2) -> c_15(X1, X2)
       , 15: first^#(s(X), cons(Y, Z)) ->
             c_16(cons^#(Y, n__first(X, activate(Z))))
       , 16: first^#(0(), Z) -> c_17(nil^#())
       , 17: from^#(X) -> c_19(cons^#(X, n__from(s(X))))
       , 18: from^#(X) -> c_20(X)
       , 19: 0^#() -> c_14()
       , 20: nil^#() -> c_18()
       , 21: sel1^#(s(X), cons(Y, Z)) -> c_21(sel1^#(X, activate(Z)))
       , 22: sel1^#(0(), cons(X, Z)) -> c_22(quote^#(X))
       , 23: quote^#(n__0()) -> c_23()
       , 24: quote^#(n__s(X)) -> c_24(quote^#(activate(X)))
       , 25: quote^#(n__sel(X, Z)) ->
             c_25(sel1^#(activate(X), activate(Z)))
       , 26: first1^#(s(X), cons(Y, Z)) ->
             c_26(quote^#(Y), first1^#(X, activate(Z)))
       , 27: first1^#(0(), Z) -> c_27()
       , 28: quote1^#(n__first(X, Z)) ->
             c_28(first1^#(activate(X), activate(Z)))
       , 29: quote1^#(n__cons(X, Z)) ->
             c_29(quote^#(activate(X)), quote1^#(activate(Z)))
       , 30: quote1^#(n__nil()) -> c_30()
       , 31: unquote^#(01()) -> c_31(0^#())
       , 32: unquote^#(s1(X)) -> c_32(s^#(unquote(X)))
       , 33: unquote1^#(nil1()) -> c_33(nil^#())
       , 34: unquote1^#(cons1(X, Z)) ->
             c_34(fcons^#(unquote(X), unquote1(Z)))
       , 35: fcons^#(X, Z) -> c_35(cons^#(X, Z)) }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { sel^#(X1, X2) -> c_1(X1, X2)
     , sel^#(s(X), cons(Y, Z)) -> c_2(sel^#(X, activate(Z)))
     , sel^#(0(), cons(X, Z)) -> c_3(X)
     , s^#(X) -> c_4(X)
     , cons^#(X1, X2) -> c_5(X1, X2)
     , activate^#(X) -> c_6(X)
     , activate^#(n__first(X1, X2)) -> c_7(first^#(X1, X2))
     , activate^#(n__from(X)) -> c_8(from^#(X))
     , activate^#(n__0()) -> c_9(0^#())
     , activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2))
     , activate^#(n__nil()) -> c_11(nil^#())
     , activate^#(n__s(X)) -> c_12(s^#(X))
     , activate^#(n__sel(X1, X2)) -> c_13(sel^#(X1, X2))
     , first^#(X1, X2) -> c_15(X1, X2)
     , first^#(s(X), cons(Y, Z)) ->
       c_16(cons^#(Y, n__first(X, activate(Z))))
     , first^#(0(), Z) -> c_17(nil^#())
     , from^#(X) -> c_19(cons^#(X, n__from(s(X))))
     , from^#(X) -> c_20(X)
     , sel1^#(s(X), cons(Y, Z)) -> c_21(sel1^#(X, activate(Z)))
     , sel1^#(0(), cons(X, Z)) -> c_22(quote^#(X))
     , quote^#(n__s(X)) -> c_24(quote^#(activate(X)))
     , quote^#(n__sel(X, Z)) -> c_25(sel1^#(activate(X), activate(Z)))
     , first1^#(s(X), cons(Y, Z)) ->
       c_26(quote^#(Y), first1^#(X, activate(Z)))
     , quote1^#(n__first(X, Z)) ->
       c_28(first1^#(activate(X), activate(Z)))
     , quote1^#(n__cons(X, Z)) ->
       c_29(quote^#(activate(X)), quote1^#(activate(Z)))
     , unquote^#(01()) -> c_31(0^#())
     , unquote^#(s1(X)) -> c_32(s^#(unquote(X)))
     , unquote1^#(nil1()) -> c_33(nil^#())
     , unquote1^#(cons1(X, Z)) -> c_34(fcons^#(unquote(X), unquote1(Z)))
     , fcons^#(X, Z) -> c_35(cons^#(X, Z)) }
   Strict Trs:
     { sel(X1, X2) -> n__sel(X1, X2)
     , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
     , sel(0(), cons(X, Z)) -> X
     , s(X) -> n__s(X)
     , cons(X1, X2) -> n__cons(X1, X2)
     , activate(X) -> X
     , activate(n__first(X1, X2)) -> first(X1, X2)
     , activate(n__from(X)) -> from(X)
     , activate(n__0()) -> 0()
     , activate(n__cons(X1, X2)) -> cons(X1, X2)
     , activate(n__nil()) -> nil()
     , activate(n__s(X)) -> s(X)
     , activate(n__sel(X1, X2)) -> sel(X1, X2)
     , 0() -> n__0()
     , first(X1, X2) -> n__first(X1, X2)
     , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
     , first(0(), Z) -> nil()
     , nil() -> n__nil()
     , from(X) -> cons(X, n__from(s(X)))
     , from(X) -> n__from(X)
     , sel1(s(X), cons(Y, Z)) -> sel1(X, activate(Z))
     , sel1(0(), cons(X, Z)) -> quote(X)
     , quote(n__0()) -> 01()
     , quote(n__s(X)) -> s1(quote(activate(X)))
     , quote(n__sel(X, Z)) -> sel1(activate(X), activate(Z))
     , first1(s(X), cons(Y, Z)) ->
       cons1(quote(Y), first1(X, activate(Z)))
     , first1(0(), Z) -> nil1()
     , quote1(n__first(X, Z)) -> first1(activate(X), activate(Z))
     , quote1(n__cons(X, Z)) ->
       cons1(quote(activate(X)), quote1(activate(Z)))
     , quote1(n__nil()) -> nil1()
     , unquote(01()) -> 0()
     , unquote(s1(X)) -> s(unquote(X))
     , unquote1(nil1()) -> nil()
     , unquote1(cons1(X, Z)) -> fcons(unquote(X), unquote1(Z))
     , fcons(X, Z) -> cons(X, Z) }
   Weak DPs:
     { 0^#() -> c_14()
     , nil^#() -> c_18()
     , quote^#(n__0()) -> c_23()
     , first1^#(0(), Z) -> c_27()
     , quote1^#(n__nil()) -> c_30() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {9,11,16,26,28} by
   applications of Pre({9,11,16,26,28}) = {1,3,4,5,6,7,14,18}. Here
   rules are labeled as follows:
   
     DPs:
       { 1: sel^#(X1, X2) -> c_1(X1, X2)
       , 2: sel^#(s(X), cons(Y, Z)) -> c_2(sel^#(X, activate(Z)))
       , 3: sel^#(0(), cons(X, Z)) -> c_3(X)
       , 4: s^#(X) -> c_4(X)
       , 5: cons^#(X1, X2) -> c_5(X1, X2)
       , 6: activate^#(X) -> c_6(X)
       , 7: activate^#(n__first(X1, X2)) -> c_7(first^#(X1, X2))
       , 8: activate^#(n__from(X)) -> c_8(from^#(X))
       , 9: activate^#(n__0()) -> c_9(0^#())
       , 10: activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2))
       , 11: activate^#(n__nil()) -> c_11(nil^#())
       , 12: activate^#(n__s(X)) -> c_12(s^#(X))
       , 13: activate^#(n__sel(X1, X2)) -> c_13(sel^#(X1, X2))
       , 14: first^#(X1, X2) -> c_15(X1, X2)
       , 15: first^#(s(X), cons(Y, Z)) ->
             c_16(cons^#(Y, n__first(X, activate(Z))))
       , 16: first^#(0(), Z) -> c_17(nil^#())
       , 17: from^#(X) -> c_19(cons^#(X, n__from(s(X))))
       , 18: from^#(X) -> c_20(X)
       , 19: sel1^#(s(X), cons(Y, Z)) -> c_21(sel1^#(X, activate(Z)))
       , 20: sel1^#(0(), cons(X, Z)) -> c_22(quote^#(X))
       , 21: quote^#(n__s(X)) -> c_24(quote^#(activate(X)))
       , 22: quote^#(n__sel(X, Z)) ->
             c_25(sel1^#(activate(X), activate(Z)))
       , 23: first1^#(s(X), cons(Y, Z)) ->
             c_26(quote^#(Y), first1^#(X, activate(Z)))
       , 24: quote1^#(n__first(X, Z)) ->
             c_28(first1^#(activate(X), activate(Z)))
       , 25: quote1^#(n__cons(X, Z)) ->
             c_29(quote^#(activate(X)), quote1^#(activate(Z)))
       , 26: unquote^#(01()) -> c_31(0^#())
       , 27: unquote^#(s1(X)) -> c_32(s^#(unquote(X)))
       , 28: unquote1^#(nil1()) -> c_33(nil^#())
       , 29: unquote1^#(cons1(X, Z)) ->
             c_34(fcons^#(unquote(X), unquote1(Z)))
       , 30: fcons^#(X, Z) -> c_35(cons^#(X, Z))
       , 31: 0^#() -> c_14()
       , 32: nil^#() -> c_18()
       , 33: quote^#(n__0()) -> c_23()
       , 34: first1^#(0(), Z) -> c_27()
       , 35: quote1^#(n__nil()) -> c_30() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { sel^#(X1, X2) -> c_1(X1, X2)
     , sel^#(s(X), cons(Y, Z)) -> c_2(sel^#(X, activate(Z)))
     , sel^#(0(), cons(X, Z)) -> c_3(X)
     , s^#(X) -> c_4(X)
     , cons^#(X1, X2) -> c_5(X1, X2)
     , activate^#(X) -> c_6(X)
     , activate^#(n__first(X1, X2)) -> c_7(first^#(X1, X2))
     , activate^#(n__from(X)) -> c_8(from^#(X))
     , activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2))
     , activate^#(n__s(X)) -> c_12(s^#(X))
     , activate^#(n__sel(X1, X2)) -> c_13(sel^#(X1, X2))
     , first^#(X1, X2) -> c_15(X1, X2)
     , first^#(s(X), cons(Y, Z)) ->
       c_16(cons^#(Y, n__first(X, activate(Z))))
     , from^#(X) -> c_19(cons^#(X, n__from(s(X))))
     , from^#(X) -> c_20(X)
     , sel1^#(s(X), cons(Y, Z)) -> c_21(sel1^#(X, activate(Z)))
     , sel1^#(0(), cons(X, Z)) -> c_22(quote^#(X))
     , quote^#(n__s(X)) -> c_24(quote^#(activate(X)))
     , quote^#(n__sel(X, Z)) -> c_25(sel1^#(activate(X), activate(Z)))
     , first1^#(s(X), cons(Y, Z)) ->
       c_26(quote^#(Y), first1^#(X, activate(Z)))
     , quote1^#(n__first(X, Z)) ->
       c_28(first1^#(activate(X), activate(Z)))
     , quote1^#(n__cons(X, Z)) ->
       c_29(quote^#(activate(X)), quote1^#(activate(Z)))
     , unquote^#(s1(X)) -> c_32(s^#(unquote(X)))
     , unquote1^#(cons1(X, Z)) -> c_34(fcons^#(unquote(X), unquote1(Z)))
     , fcons^#(X, Z) -> c_35(cons^#(X, Z)) }
   Strict Trs:
     { sel(X1, X2) -> n__sel(X1, X2)
     , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
     , sel(0(), cons(X, Z)) -> X
     , s(X) -> n__s(X)
     , cons(X1, X2) -> n__cons(X1, X2)
     , activate(X) -> X
     , activate(n__first(X1, X2)) -> first(X1, X2)
     , activate(n__from(X)) -> from(X)
     , activate(n__0()) -> 0()
     , activate(n__cons(X1, X2)) -> cons(X1, X2)
     , activate(n__nil()) -> nil()
     , activate(n__s(X)) -> s(X)
     , activate(n__sel(X1, X2)) -> sel(X1, X2)
     , 0() -> n__0()
     , first(X1, X2) -> n__first(X1, X2)
     , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
     , first(0(), Z) -> nil()
     , nil() -> n__nil()
     , from(X) -> cons(X, n__from(s(X)))
     , from(X) -> n__from(X)
     , sel1(s(X), cons(Y, Z)) -> sel1(X, activate(Z))
     , sel1(0(), cons(X, Z)) -> quote(X)
     , quote(n__0()) -> 01()
     , quote(n__s(X)) -> s1(quote(activate(X)))
     , quote(n__sel(X, Z)) -> sel1(activate(X), activate(Z))
     , first1(s(X), cons(Y, Z)) ->
       cons1(quote(Y), first1(X, activate(Z)))
     , first1(0(), Z) -> nil1()
     , quote1(n__first(X, Z)) -> first1(activate(X), activate(Z))
     , quote1(n__cons(X, Z)) ->
       cons1(quote(activate(X)), quote1(activate(Z)))
     , quote1(n__nil()) -> nil1()
     , unquote(01()) -> 0()
     , unquote(s1(X)) -> s(unquote(X))
     , unquote1(nil1()) -> nil()
     , unquote1(cons1(X, Z)) -> fcons(unquote(X), unquote1(Z))
     , fcons(X, Z) -> cons(X, Z) }
   Weak DPs:
     { activate^#(n__0()) -> c_9(0^#())
     , activate^#(n__nil()) -> c_11(nil^#())
     , first^#(0(), Z) -> c_17(nil^#())
     , 0^#() -> c_14()
     , nil^#() -> c_18()
     , quote^#(n__0()) -> c_23()
     , first1^#(0(), Z) -> c_27()
     , quote1^#(n__nil()) -> c_30()
     , unquote^#(01()) -> c_31(0^#())
     , unquote1^#(nil1()) -> c_33(nil^#()) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..