MAYBE
754.16/297.12	MAYBE
754.16/297.12	
754.16/297.12	We are left with following problem, upon which TcT provides the
754.16/297.12	certificate MAYBE.
754.16/297.12	
754.16/297.12	Strict Trs:
754.16/297.12	  { sel(X1, X2) -> n__sel(X1, X2)
754.16/297.12	  , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
754.16/297.12	  , sel(0(), cons(X, Z)) -> X
754.16/297.12	  , s(X) -> n__s(X)
754.16/297.12	  , cons(X1, X2) -> n__cons(X1, X2)
754.16/297.12	  , activate(X) -> X
754.16/297.12	  , activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))
754.16/297.12	  , activate(n__from(X)) -> from(activate(X))
754.16/297.12	  , activate(n__s(X)) -> s(activate(X))
754.16/297.12	  , activate(n__0()) -> 0()
754.16/297.12	  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
754.16/297.12	  , activate(n__nil()) -> nil()
754.16/297.12	  , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2))
754.16/297.12	  , 0() -> n__0()
754.16/297.12	  , first(X1, X2) -> n__first(X1, X2)
754.16/297.12	  , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
754.16/297.12	  , first(0(), Z) -> nil()
754.16/297.12	  , nil() -> n__nil()
754.16/297.12	  , from(X) -> cons(X, n__from(n__s(X)))
754.16/297.12	  , from(X) -> n__from(X)
754.16/297.12	  , sel1(s(X), cons(Y, Z)) -> sel1(X, activate(Z))
754.16/297.12	  , sel1(0(), cons(X, Z)) -> quote(X)
754.16/297.12	  , quote(n__s(X)) -> s1(quote(activate(X)))
754.16/297.12	  , quote(n__0()) -> 01()
754.16/297.12	  , quote(n__sel(X, Z)) -> sel1(activate(X), activate(Z))
754.16/297.12	  , first1(s(X), cons(Y, Z)) ->
754.16/297.12	    cons1(quote(Y), first1(X, activate(Z)))
754.16/297.12	  , first1(0(), Z) -> nil1()
754.16/297.12	  , quote1(n__first(X, Z)) -> first1(activate(X), activate(Z))
754.16/297.12	  , quote1(n__cons(X, Z)) ->
754.16/297.12	    cons1(quote(activate(X)), quote1(activate(Z)))
754.16/297.12	  , quote1(n__nil()) -> nil1()
754.16/297.12	  , unquote(01()) -> 0()
754.16/297.12	  , unquote(s1(X)) -> s(unquote(X))
754.16/297.12	  , unquote1(nil1()) -> nil()
754.16/297.12	  , unquote1(cons1(X, Z)) -> fcons(unquote(X), unquote1(Z))
754.16/297.12	  , fcons(X, Z) -> cons(X, Z) }
754.16/297.12	Obligation:
754.16/297.12	  runtime complexity
754.16/297.12	Answer:
754.16/297.12	  MAYBE
754.16/297.12	
754.16/297.12	None of the processors succeeded.
754.16/297.12	
754.16/297.12	Details of failed attempt(s):
754.16/297.12	-----------------------------
754.16/297.12	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
754.16/297.12	   following reason:
754.16/297.12	   
754.16/297.12	   Computation stopped due to timeout after 297.0 seconds.
754.16/297.12	
754.16/297.12	2) 'Best' failed due to the following reason:
754.16/297.12	   
754.16/297.12	   None of the processors succeeded.
754.16/297.12	   
754.16/297.12	   Details of failed attempt(s):
754.16/297.12	   -----------------------------
754.16/297.12	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
754.16/297.12	      seconds)' failed due to the following reason:
754.16/297.12	      
754.16/297.12	      None of the processors succeeded.
754.16/297.12	      
754.16/297.12	      Details of failed attempt(s):
754.16/297.12	      -----------------------------
754.16/297.12	      1) 'empty' failed due to the following reason:
754.16/297.12	         
754.16/297.12	         Empty strict component of the problem is NOT empty.
754.16/297.12	      
754.16/297.12	      2) 'With Problem ...' failed due to the following reason:
754.16/297.12	         
754.16/297.12	         None of the processors succeeded.
754.16/297.12	         
754.16/297.12	         Details of failed attempt(s):
754.16/297.12	         -----------------------------
754.16/297.12	         1) 'empty' failed due to the following reason:
754.16/297.12	            
754.16/297.12	            Empty strict component of the problem is NOT empty.
754.16/297.12	         
754.16/297.12	         2) 'Fastest' failed due to the following reason:
754.16/297.12	            
754.16/297.12	            None of the processors succeeded.
754.16/297.12	            
754.16/297.12	            Details of failed attempt(s):
754.16/297.12	            -----------------------------
754.16/297.12	            1) 'With Problem ...' failed due to the following reason:
754.16/297.12	               
754.16/297.12	               None of the processors succeeded.
754.16/297.12	               
754.16/297.12	               Details of failed attempt(s):
754.16/297.12	               -----------------------------
754.16/297.12	               1) 'empty' failed due to the following reason:
754.16/297.12	                  
754.16/297.12	                  Empty strict component of the problem is NOT empty.
754.16/297.12	               
754.16/297.12	               2) 'With Problem ...' failed due to the following reason:
754.16/297.12	                  
754.16/297.12	                  None of the processors succeeded.
754.16/297.12	                  
754.16/297.12	                  Details of failed attempt(s):
754.16/297.12	                  -----------------------------
754.16/297.12	                  1) 'empty' failed due to the following reason:
754.16/297.12	                     
754.16/297.12	                     Empty strict component of the problem is NOT empty.
754.16/297.12	                  
754.16/297.12	                  2) 'With Problem ...' failed due to the following reason:
754.16/297.12	                     
754.16/297.12	                     None of the processors succeeded.
754.16/297.12	                     
754.16/297.12	                     Details of failed attempt(s):
754.16/297.12	                     -----------------------------
754.16/297.12	                     1) 'empty' failed due to the following reason:
754.16/297.12	                        
754.16/297.12	                        Empty strict component of the problem is NOT empty.
754.16/297.12	                     
754.16/297.12	                     2) 'With Problem ...' failed due to the following reason:
754.16/297.12	                        
754.16/297.12	                        Empty strict component of the problem is NOT empty.
754.16/297.12	                     
754.16/297.12	                  
754.16/297.12	               
754.16/297.12	            
754.16/297.12	            2) 'With Problem ...' failed due to the following reason:
754.16/297.12	               
754.16/297.12	               None of the processors succeeded.
754.16/297.12	               
754.16/297.12	               Details of failed attempt(s):
754.16/297.12	               -----------------------------
754.16/297.12	               1) 'empty' failed due to the following reason:
754.16/297.12	                  
754.16/297.12	                  Empty strict component of the problem is NOT empty.
754.16/297.12	               
754.16/297.12	               2) 'With Problem ...' failed due to the following reason:
754.16/297.12	                  
754.16/297.12	                  Empty strict component of the problem is NOT empty.
754.16/297.12	               
754.16/297.12	            
754.16/297.12	         
754.16/297.12	      
754.16/297.12	   
754.16/297.12	   2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
754.16/297.12	      failed due to the following reason:
754.16/297.12	      
754.16/297.12	      None of the processors succeeded.
754.16/297.12	      
754.16/297.12	      Details of failed attempt(s):
754.16/297.12	      -----------------------------
754.16/297.12	      1) 'Bounds with perSymbol-enrichment and initial automaton 'match''
754.16/297.12	         failed due to the following reason:
754.16/297.12	         
754.16/297.12	         match-boundness of the problem could not be verified.
754.16/297.12	      
754.16/297.12	      2) 'Bounds with minimal-enrichment and initial automaton 'match''
754.16/297.12	         failed due to the following reason:
754.16/297.12	         
754.16/297.12	         match-boundness of the problem could not be verified.
754.16/297.12	      
754.16/297.12	   
754.16/297.12	   3) 'Best' failed due to the following reason:
754.16/297.12	      
754.16/297.12	      None of the processors succeeded.
754.16/297.12	      
754.16/297.12	      Details of failed attempt(s):
754.16/297.12	      -----------------------------
754.16/297.12	      1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
754.16/297.12	         to the following reason:
754.16/297.12	         
754.16/297.12	         The processor is inapplicable, reason:
754.16/297.12	           Processor only applicable for innermost runtime complexity analysis
754.16/297.12	      
754.16/297.12	      2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
754.16/297.12	         following reason:
754.16/297.12	         
754.16/297.12	         The processor is inapplicable, reason:
754.16/297.12	           Processor only applicable for innermost runtime complexity analysis
754.16/297.12	      
754.16/297.12	   
754.16/297.12	
754.16/297.12	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
754.16/297.12	   the following reason:
754.16/297.12	   
754.16/297.12	   We add the following weak dependency pairs:
754.16/297.12	   
754.16/297.12	   Strict DPs:
754.16/297.12	     { sel^#(X1, X2) -> c_1(X1, X2)
754.16/297.12	     , sel^#(s(X), cons(Y, Z)) -> c_2(sel^#(X, activate(Z)))
754.16/297.12	     , sel^#(0(), cons(X, Z)) -> c_3(X)
754.16/297.12	     , s^#(X) -> c_4(X)
754.16/297.12	     , cons^#(X1, X2) -> c_5(X1, X2)
754.16/297.12	     , activate^#(X) -> c_6(X)
754.16/297.12	     , activate^#(n__first(X1, X2)) ->
754.16/297.12	       c_7(first^#(activate(X1), activate(X2)))
754.16/297.12	     , activate^#(n__from(X)) -> c_8(from^#(activate(X)))
754.16/297.12	     , activate^#(n__s(X)) -> c_9(s^#(activate(X)))
754.16/297.12	     , activate^#(n__0()) -> c_10(0^#())
754.16/297.12	     , activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2))
754.16/297.12	     , activate^#(n__nil()) -> c_12(nil^#())
754.16/297.12	     , activate^#(n__sel(X1, X2)) ->
754.16/297.12	       c_13(sel^#(activate(X1), activate(X2)))
754.16/297.12	     , first^#(X1, X2) -> c_15(X1, X2)
754.16/297.12	     , first^#(s(X), cons(Y, Z)) ->
754.16/297.12	       c_16(cons^#(Y, n__first(X, activate(Z))))
754.16/297.12	     , first^#(0(), Z) -> c_17(nil^#())
754.16/297.12	     , from^#(X) -> c_19(cons^#(X, n__from(n__s(X))))
754.16/297.12	     , from^#(X) -> c_20(X)
754.16/297.12	     , 0^#() -> c_14()
754.16/297.12	     , nil^#() -> c_18()
754.16/297.12	     , sel1^#(s(X), cons(Y, Z)) -> c_21(sel1^#(X, activate(Z)))
754.16/297.12	     , sel1^#(0(), cons(X, Z)) -> c_22(quote^#(X))
754.16/297.12	     , quote^#(n__s(X)) -> c_23(quote^#(activate(X)))
754.16/297.12	     , quote^#(n__0()) -> c_24()
754.16/297.12	     , quote^#(n__sel(X, Z)) -> c_25(sel1^#(activate(X), activate(Z)))
754.16/297.12	     , first1^#(s(X), cons(Y, Z)) ->
754.16/297.12	       c_26(quote^#(Y), first1^#(X, activate(Z)))
754.16/297.12	     , first1^#(0(), Z) -> c_27()
754.16/297.12	     , quote1^#(n__first(X, Z)) ->
754.16/297.12	       c_28(first1^#(activate(X), activate(Z)))
754.16/297.12	     , quote1^#(n__cons(X, Z)) ->
754.16/297.12	       c_29(quote^#(activate(X)), quote1^#(activate(Z)))
754.16/297.12	     , quote1^#(n__nil()) -> c_30()
754.16/297.12	     , unquote^#(01()) -> c_31(0^#())
754.16/297.12	     , unquote^#(s1(X)) -> c_32(s^#(unquote(X)))
754.16/297.12	     , unquote1^#(nil1()) -> c_33(nil^#())
754.16/297.12	     , unquote1^#(cons1(X, Z)) -> c_34(fcons^#(unquote(X), unquote1(Z)))
754.16/297.12	     , fcons^#(X, Z) -> c_35(cons^#(X, Z)) }
754.16/297.12	   
754.16/297.12	   and mark the set of starting terms.
754.16/297.12	   
754.16/297.12	   We are left with following problem, upon which TcT provides the
754.16/297.12	   certificate MAYBE.
754.16/297.12	   
754.16/297.12	   Strict DPs:
754.16/297.12	     { sel^#(X1, X2) -> c_1(X1, X2)
754.16/297.12	     , sel^#(s(X), cons(Y, Z)) -> c_2(sel^#(X, activate(Z)))
754.16/297.12	     , sel^#(0(), cons(X, Z)) -> c_3(X)
754.16/297.12	     , s^#(X) -> c_4(X)
754.16/297.12	     , cons^#(X1, X2) -> c_5(X1, X2)
754.16/297.12	     , activate^#(X) -> c_6(X)
754.16/297.12	     , activate^#(n__first(X1, X2)) ->
754.16/297.12	       c_7(first^#(activate(X1), activate(X2)))
754.16/297.12	     , activate^#(n__from(X)) -> c_8(from^#(activate(X)))
754.16/297.12	     , activate^#(n__s(X)) -> c_9(s^#(activate(X)))
754.16/297.12	     , activate^#(n__0()) -> c_10(0^#())
754.16/297.12	     , activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2))
754.16/297.12	     , activate^#(n__nil()) -> c_12(nil^#())
754.16/297.12	     , activate^#(n__sel(X1, X2)) ->
754.16/297.12	       c_13(sel^#(activate(X1), activate(X2)))
754.16/297.12	     , first^#(X1, X2) -> c_15(X1, X2)
754.16/297.12	     , first^#(s(X), cons(Y, Z)) ->
754.16/297.12	       c_16(cons^#(Y, n__first(X, activate(Z))))
754.16/297.12	     , first^#(0(), Z) -> c_17(nil^#())
754.16/297.12	     , from^#(X) -> c_19(cons^#(X, n__from(n__s(X))))
754.16/297.12	     , from^#(X) -> c_20(X)
754.16/297.12	     , 0^#() -> c_14()
754.16/297.12	     , nil^#() -> c_18()
754.16/297.12	     , sel1^#(s(X), cons(Y, Z)) -> c_21(sel1^#(X, activate(Z)))
754.16/297.12	     , sel1^#(0(), cons(X, Z)) -> c_22(quote^#(X))
754.16/297.12	     , quote^#(n__s(X)) -> c_23(quote^#(activate(X)))
754.16/297.12	     , quote^#(n__0()) -> c_24()
754.16/297.12	     , quote^#(n__sel(X, Z)) -> c_25(sel1^#(activate(X), activate(Z)))
754.16/297.12	     , first1^#(s(X), cons(Y, Z)) ->
754.16/297.12	       c_26(quote^#(Y), first1^#(X, activate(Z)))
754.16/297.12	     , first1^#(0(), Z) -> c_27()
754.16/297.12	     , quote1^#(n__first(X, Z)) ->
754.16/297.12	       c_28(first1^#(activate(X), activate(Z)))
754.16/297.12	     , quote1^#(n__cons(X, Z)) ->
754.16/297.12	       c_29(quote^#(activate(X)), quote1^#(activate(Z)))
754.16/297.12	     , quote1^#(n__nil()) -> c_30()
754.16/297.12	     , unquote^#(01()) -> c_31(0^#())
754.16/297.12	     , unquote^#(s1(X)) -> c_32(s^#(unquote(X)))
754.16/297.12	     , unquote1^#(nil1()) -> c_33(nil^#())
754.16/297.12	     , unquote1^#(cons1(X, Z)) -> c_34(fcons^#(unquote(X), unquote1(Z)))
754.16/297.12	     , fcons^#(X, Z) -> c_35(cons^#(X, Z)) }
754.16/297.12	   Strict Trs:
754.16/297.12	     { sel(X1, X2) -> n__sel(X1, X2)
754.16/297.12	     , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
754.16/297.12	     , sel(0(), cons(X, Z)) -> X
754.16/297.12	     , s(X) -> n__s(X)
754.16/297.12	     , cons(X1, X2) -> n__cons(X1, X2)
754.16/297.12	     , activate(X) -> X
754.16/297.12	     , activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))
754.16/297.12	     , activate(n__from(X)) -> from(activate(X))
754.16/297.12	     , activate(n__s(X)) -> s(activate(X))
754.16/297.12	     , activate(n__0()) -> 0()
754.16/297.12	     , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
754.16/297.12	     , activate(n__nil()) -> nil()
754.16/297.12	     , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2))
754.16/297.12	     , 0() -> n__0()
754.16/297.12	     , first(X1, X2) -> n__first(X1, X2)
754.16/297.12	     , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
754.16/297.12	     , first(0(), Z) -> nil()
754.16/297.12	     , nil() -> n__nil()
754.16/297.12	     , from(X) -> cons(X, n__from(n__s(X)))
754.16/297.12	     , from(X) -> n__from(X)
754.16/297.12	     , sel1(s(X), cons(Y, Z)) -> sel1(X, activate(Z))
754.16/297.12	     , sel1(0(), cons(X, Z)) -> quote(X)
754.16/297.12	     , quote(n__s(X)) -> s1(quote(activate(X)))
754.16/297.12	     , quote(n__0()) -> 01()
754.16/297.12	     , quote(n__sel(X, Z)) -> sel1(activate(X), activate(Z))
754.16/297.12	     , first1(s(X), cons(Y, Z)) ->
754.16/297.12	       cons1(quote(Y), first1(X, activate(Z)))
754.16/297.12	     , first1(0(), Z) -> nil1()
754.16/297.12	     , quote1(n__first(X, Z)) -> first1(activate(X), activate(Z))
754.16/297.12	     , quote1(n__cons(X, Z)) ->
754.16/297.12	       cons1(quote(activate(X)), quote1(activate(Z)))
754.16/297.12	     , quote1(n__nil()) -> nil1()
754.16/297.12	     , unquote(01()) -> 0()
754.16/297.12	     , unquote(s1(X)) -> s(unquote(X))
754.16/297.12	     , unquote1(nil1()) -> nil()
754.16/297.12	     , unquote1(cons1(X, Z)) -> fcons(unquote(X), unquote1(Z))
754.16/297.12	     , fcons(X, Z) -> cons(X, Z) }
754.16/297.12	   Obligation:
754.16/297.12	     runtime complexity
754.16/297.12	   Answer:
754.16/297.12	     MAYBE
754.16/297.12	   
754.16/297.12	   We estimate the number of application of {19,20,24,27,30} by
754.16/297.12	   applications of Pre({19,20,24,27,30}) =
754.16/297.12	   {1,3,4,5,6,10,12,14,16,18,22,23,26,28,29,31,33}. Here rules are
754.16/297.12	   labeled as follows:
754.16/297.12	   
754.16/297.12	     DPs:
754.16/297.12	       { 1: sel^#(X1, X2) -> c_1(X1, X2)
754.16/297.12	       , 2: sel^#(s(X), cons(Y, Z)) -> c_2(sel^#(X, activate(Z)))
754.16/297.12	       , 3: sel^#(0(), cons(X, Z)) -> c_3(X)
754.16/297.12	       , 4: s^#(X) -> c_4(X)
754.16/297.12	       , 5: cons^#(X1, X2) -> c_5(X1, X2)
754.16/297.12	       , 6: activate^#(X) -> c_6(X)
754.16/297.12	       , 7: activate^#(n__first(X1, X2)) ->
754.16/297.12	            c_7(first^#(activate(X1), activate(X2)))
754.16/297.12	       , 8: activate^#(n__from(X)) -> c_8(from^#(activate(X)))
754.16/297.12	       , 9: activate^#(n__s(X)) -> c_9(s^#(activate(X)))
754.16/297.12	       , 10: activate^#(n__0()) -> c_10(0^#())
754.16/297.12	       , 11: activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2))
754.16/297.12	       , 12: activate^#(n__nil()) -> c_12(nil^#())
754.16/297.12	       , 13: activate^#(n__sel(X1, X2)) ->
754.16/297.12	             c_13(sel^#(activate(X1), activate(X2)))
754.16/297.12	       , 14: first^#(X1, X2) -> c_15(X1, X2)
754.16/297.12	       , 15: first^#(s(X), cons(Y, Z)) ->
754.16/297.12	             c_16(cons^#(Y, n__first(X, activate(Z))))
754.16/297.12	       , 16: first^#(0(), Z) -> c_17(nil^#())
754.16/297.12	       , 17: from^#(X) -> c_19(cons^#(X, n__from(n__s(X))))
754.16/297.12	       , 18: from^#(X) -> c_20(X)
754.16/297.12	       , 19: 0^#() -> c_14()
754.16/297.12	       , 20: nil^#() -> c_18()
754.16/297.12	       , 21: sel1^#(s(X), cons(Y, Z)) -> c_21(sel1^#(X, activate(Z)))
754.16/297.12	       , 22: sel1^#(0(), cons(X, Z)) -> c_22(quote^#(X))
754.16/297.12	       , 23: quote^#(n__s(X)) -> c_23(quote^#(activate(X)))
754.16/297.12	       , 24: quote^#(n__0()) -> c_24()
754.16/297.12	       , 25: quote^#(n__sel(X, Z)) ->
754.16/297.12	             c_25(sel1^#(activate(X), activate(Z)))
754.16/297.12	       , 26: first1^#(s(X), cons(Y, Z)) ->
754.16/297.12	             c_26(quote^#(Y), first1^#(X, activate(Z)))
754.16/297.12	       , 27: first1^#(0(), Z) -> c_27()
754.16/297.12	       , 28: quote1^#(n__first(X, Z)) ->
754.16/297.12	             c_28(first1^#(activate(X), activate(Z)))
754.16/297.12	       , 29: quote1^#(n__cons(X, Z)) ->
754.16/297.12	             c_29(quote^#(activate(X)), quote1^#(activate(Z)))
754.16/297.12	       , 30: quote1^#(n__nil()) -> c_30()
754.16/297.12	       , 31: unquote^#(01()) -> c_31(0^#())
754.16/297.12	       , 32: unquote^#(s1(X)) -> c_32(s^#(unquote(X)))
754.16/297.12	       , 33: unquote1^#(nil1()) -> c_33(nil^#())
754.16/297.12	       , 34: unquote1^#(cons1(X, Z)) ->
754.16/297.12	             c_34(fcons^#(unquote(X), unquote1(Z)))
754.16/297.12	       , 35: fcons^#(X, Z) -> c_35(cons^#(X, Z)) }
754.16/297.12	   
754.16/297.12	   We are left with following problem, upon which TcT provides the
754.16/297.12	   certificate MAYBE.
754.16/297.12	   
754.16/297.12	   Strict DPs:
754.16/297.12	     { sel^#(X1, X2) -> c_1(X1, X2)
754.16/297.12	     , sel^#(s(X), cons(Y, Z)) -> c_2(sel^#(X, activate(Z)))
754.16/297.12	     , sel^#(0(), cons(X, Z)) -> c_3(X)
754.16/297.12	     , s^#(X) -> c_4(X)
754.16/297.12	     , cons^#(X1, X2) -> c_5(X1, X2)
754.16/297.12	     , activate^#(X) -> c_6(X)
754.16/297.12	     , activate^#(n__first(X1, X2)) ->
754.16/297.12	       c_7(first^#(activate(X1), activate(X2)))
754.16/297.12	     , activate^#(n__from(X)) -> c_8(from^#(activate(X)))
754.16/297.12	     , activate^#(n__s(X)) -> c_9(s^#(activate(X)))
754.16/297.12	     , activate^#(n__0()) -> c_10(0^#())
754.16/297.12	     , activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2))
754.16/297.12	     , activate^#(n__nil()) -> c_12(nil^#())
754.16/297.12	     , activate^#(n__sel(X1, X2)) ->
754.16/297.12	       c_13(sel^#(activate(X1), activate(X2)))
754.16/297.12	     , first^#(X1, X2) -> c_15(X1, X2)
754.16/297.12	     , first^#(s(X), cons(Y, Z)) ->
754.16/297.12	       c_16(cons^#(Y, n__first(X, activate(Z))))
754.16/297.12	     , first^#(0(), Z) -> c_17(nil^#())
754.16/297.12	     , from^#(X) -> c_19(cons^#(X, n__from(n__s(X))))
754.16/297.12	     , from^#(X) -> c_20(X)
754.16/297.12	     , sel1^#(s(X), cons(Y, Z)) -> c_21(sel1^#(X, activate(Z)))
754.16/297.12	     , sel1^#(0(), cons(X, Z)) -> c_22(quote^#(X))
754.16/297.12	     , quote^#(n__s(X)) -> c_23(quote^#(activate(X)))
754.16/297.12	     , quote^#(n__sel(X, Z)) -> c_25(sel1^#(activate(X), activate(Z)))
754.16/297.12	     , first1^#(s(X), cons(Y, Z)) ->
754.16/297.12	       c_26(quote^#(Y), first1^#(X, activate(Z)))
754.16/297.12	     , quote1^#(n__first(X, Z)) ->
754.16/297.12	       c_28(first1^#(activate(X), activate(Z)))
754.16/297.12	     , quote1^#(n__cons(X, Z)) ->
754.16/297.12	       c_29(quote^#(activate(X)), quote1^#(activate(Z)))
754.16/297.12	     , unquote^#(01()) -> c_31(0^#())
754.16/297.12	     , unquote^#(s1(X)) -> c_32(s^#(unquote(X)))
754.16/297.12	     , unquote1^#(nil1()) -> c_33(nil^#())
754.16/297.12	     , unquote1^#(cons1(X, Z)) -> c_34(fcons^#(unquote(X), unquote1(Z)))
754.16/297.12	     , fcons^#(X, Z) -> c_35(cons^#(X, Z)) }
754.16/297.12	   Strict Trs:
754.16/297.12	     { sel(X1, X2) -> n__sel(X1, X2)
754.16/297.12	     , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
754.16/297.12	     , sel(0(), cons(X, Z)) -> X
754.16/297.12	     , s(X) -> n__s(X)
754.16/297.12	     , cons(X1, X2) -> n__cons(X1, X2)
754.16/297.12	     , activate(X) -> X
754.16/297.12	     , activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))
754.16/297.12	     , activate(n__from(X)) -> from(activate(X))
754.16/297.12	     , activate(n__s(X)) -> s(activate(X))
754.16/297.12	     , activate(n__0()) -> 0()
754.16/297.12	     , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
754.16/297.12	     , activate(n__nil()) -> nil()
754.16/297.12	     , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2))
754.16/297.12	     , 0() -> n__0()
754.16/297.12	     , first(X1, X2) -> n__first(X1, X2)
754.16/297.12	     , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
754.16/297.12	     , first(0(), Z) -> nil()
754.16/297.12	     , nil() -> n__nil()
754.16/297.12	     , from(X) -> cons(X, n__from(n__s(X)))
754.16/297.12	     , from(X) -> n__from(X)
754.16/297.12	     , sel1(s(X), cons(Y, Z)) -> sel1(X, activate(Z))
754.16/297.12	     , sel1(0(), cons(X, Z)) -> quote(X)
754.16/297.12	     , quote(n__s(X)) -> s1(quote(activate(X)))
754.16/297.12	     , quote(n__0()) -> 01()
754.16/297.12	     , quote(n__sel(X, Z)) -> sel1(activate(X), activate(Z))
754.16/297.12	     , first1(s(X), cons(Y, Z)) ->
754.16/297.12	       cons1(quote(Y), first1(X, activate(Z)))
754.16/297.12	     , first1(0(), Z) -> nil1()
754.16/297.12	     , quote1(n__first(X, Z)) -> first1(activate(X), activate(Z))
754.16/297.12	     , quote1(n__cons(X, Z)) ->
754.16/297.12	       cons1(quote(activate(X)), quote1(activate(Z)))
754.16/297.12	     , quote1(n__nil()) -> nil1()
754.16/297.12	     , unquote(01()) -> 0()
754.16/297.12	     , unquote(s1(X)) -> s(unquote(X))
754.16/297.12	     , unquote1(nil1()) -> nil()
754.16/297.12	     , unquote1(cons1(X, Z)) -> fcons(unquote(X), unquote1(Z))
754.16/297.12	     , fcons(X, Z) -> cons(X, Z) }
754.16/297.12	   Weak DPs:
754.16/297.12	     { 0^#() -> c_14()
754.16/297.12	     , nil^#() -> c_18()
754.16/297.12	     , quote^#(n__0()) -> c_24()
754.16/297.12	     , first1^#(0(), Z) -> c_27()
754.16/297.12	     , quote1^#(n__nil()) -> c_30() }
754.16/297.12	   Obligation:
754.16/297.12	     runtime complexity
754.16/297.12	   Answer:
754.16/297.12	     MAYBE
754.16/297.12	   
754.16/297.12	   We estimate the number of application of {10,12,16,26,28} by
754.16/297.12	   applications of Pre({10,12,16,26,28}) = {1,3,4,5,6,7,14,18}. Here
754.16/297.12	   rules are labeled as follows:
754.16/297.12	   
754.16/297.12	     DPs:
754.16/297.12	       { 1: sel^#(X1, X2) -> c_1(X1, X2)
754.16/297.12	       , 2: sel^#(s(X), cons(Y, Z)) -> c_2(sel^#(X, activate(Z)))
754.16/297.12	       , 3: sel^#(0(), cons(X, Z)) -> c_3(X)
754.16/297.12	       , 4: s^#(X) -> c_4(X)
754.16/297.12	       , 5: cons^#(X1, X2) -> c_5(X1, X2)
754.16/297.12	       , 6: activate^#(X) -> c_6(X)
754.16/297.12	       , 7: activate^#(n__first(X1, X2)) ->
754.16/297.12	            c_7(first^#(activate(X1), activate(X2)))
754.16/297.12	       , 8: activate^#(n__from(X)) -> c_8(from^#(activate(X)))
754.16/297.12	       , 9: activate^#(n__s(X)) -> c_9(s^#(activate(X)))
754.16/297.12	       , 10: activate^#(n__0()) -> c_10(0^#())
754.16/297.12	       , 11: activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2))
754.16/297.12	       , 12: activate^#(n__nil()) -> c_12(nil^#())
754.16/297.12	       , 13: activate^#(n__sel(X1, X2)) ->
754.16/297.12	             c_13(sel^#(activate(X1), activate(X2)))
754.16/297.12	       , 14: first^#(X1, X2) -> c_15(X1, X2)
754.16/297.12	       , 15: first^#(s(X), cons(Y, Z)) ->
754.16/297.12	             c_16(cons^#(Y, n__first(X, activate(Z))))
754.16/297.12	       , 16: first^#(0(), Z) -> c_17(nil^#())
754.16/297.12	       , 17: from^#(X) -> c_19(cons^#(X, n__from(n__s(X))))
754.16/297.12	       , 18: from^#(X) -> c_20(X)
754.16/297.12	       , 19: sel1^#(s(X), cons(Y, Z)) -> c_21(sel1^#(X, activate(Z)))
754.16/297.12	       , 20: sel1^#(0(), cons(X, Z)) -> c_22(quote^#(X))
754.16/297.12	       , 21: quote^#(n__s(X)) -> c_23(quote^#(activate(X)))
754.16/297.12	       , 22: quote^#(n__sel(X, Z)) ->
754.16/297.12	             c_25(sel1^#(activate(X), activate(Z)))
754.16/297.12	       , 23: first1^#(s(X), cons(Y, Z)) ->
754.16/297.12	             c_26(quote^#(Y), first1^#(X, activate(Z)))
754.16/297.12	       , 24: quote1^#(n__first(X, Z)) ->
754.16/297.12	             c_28(first1^#(activate(X), activate(Z)))
754.16/297.12	       , 25: quote1^#(n__cons(X, Z)) ->
754.16/297.12	             c_29(quote^#(activate(X)), quote1^#(activate(Z)))
754.16/297.12	       , 26: unquote^#(01()) -> c_31(0^#())
754.16/297.12	       , 27: unquote^#(s1(X)) -> c_32(s^#(unquote(X)))
754.16/297.12	       , 28: unquote1^#(nil1()) -> c_33(nil^#())
754.16/297.12	       , 29: unquote1^#(cons1(X, Z)) ->
754.16/297.12	             c_34(fcons^#(unquote(X), unquote1(Z)))
754.16/297.12	       , 30: fcons^#(X, Z) -> c_35(cons^#(X, Z))
754.16/297.12	       , 31: 0^#() -> c_14()
754.16/297.12	       , 32: nil^#() -> c_18()
754.16/297.12	       , 33: quote^#(n__0()) -> c_24()
754.16/297.12	       , 34: first1^#(0(), Z) -> c_27()
754.16/297.12	       , 35: quote1^#(n__nil()) -> c_30() }
754.16/297.12	   
754.16/297.12	   We are left with following problem, upon which TcT provides the
754.16/297.12	   certificate MAYBE.
754.16/297.12	   
754.16/297.12	   Strict DPs:
754.16/297.12	     { sel^#(X1, X2) -> c_1(X1, X2)
754.16/297.12	     , sel^#(s(X), cons(Y, Z)) -> c_2(sel^#(X, activate(Z)))
754.16/297.12	     , sel^#(0(), cons(X, Z)) -> c_3(X)
754.16/297.12	     , s^#(X) -> c_4(X)
754.16/297.12	     , cons^#(X1, X2) -> c_5(X1, X2)
754.16/297.12	     , activate^#(X) -> c_6(X)
754.16/297.12	     , activate^#(n__first(X1, X2)) ->
754.16/297.12	       c_7(first^#(activate(X1), activate(X2)))
754.16/297.12	     , activate^#(n__from(X)) -> c_8(from^#(activate(X)))
754.16/297.12	     , activate^#(n__s(X)) -> c_9(s^#(activate(X)))
754.16/297.12	     , activate^#(n__cons(X1, X2)) -> c_11(cons^#(activate(X1), X2))
754.16/297.12	     , activate^#(n__sel(X1, X2)) ->
754.16/297.12	       c_13(sel^#(activate(X1), activate(X2)))
754.16/297.12	     , first^#(X1, X2) -> c_15(X1, X2)
754.16/297.12	     , first^#(s(X), cons(Y, Z)) ->
754.16/297.12	       c_16(cons^#(Y, n__first(X, activate(Z))))
754.16/297.12	     , from^#(X) -> c_19(cons^#(X, n__from(n__s(X))))
754.16/297.12	     , from^#(X) -> c_20(X)
754.16/297.12	     , sel1^#(s(X), cons(Y, Z)) -> c_21(sel1^#(X, activate(Z)))
754.16/297.12	     , sel1^#(0(), cons(X, Z)) -> c_22(quote^#(X))
754.16/297.12	     , quote^#(n__s(X)) -> c_23(quote^#(activate(X)))
754.16/297.12	     , quote^#(n__sel(X, Z)) -> c_25(sel1^#(activate(X), activate(Z)))
754.16/297.12	     , first1^#(s(X), cons(Y, Z)) ->
754.16/297.12	       c_26(quote^#(Y), first1^#(X, activate(Z)))
754.16/297.12	     , quote1^#(n__first(X, Z)) ->
754.16/297.12	       c_28(first1^#(activate(X), activate(Z)))
754.16/297.12	     , quote1^#(n__cons(X, Z)) ->
754.16/297.12	       c_29(quote^#(activate(X)), quote1^#(activate(Z)))
754.16/297.12	     , unquote^#(s1(X)) -> c_32(s^#(unquote(X)))
754.16/297.12	     , unquote1^#(cons1(X, Z)) -> c_34(fcons^#(unquote(X), unquote1(Z)))
754.16/297.12	     , fcons^#(X, Z) -> c_35(cons^#(X, Z)) }
754.16/297.12	   Strict Trs:
754.16/297.12	     { sel(X1, X2) -> n__sel(X1, X2)
754.16/297.12	     , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
754.16/297.12	     , sel(0(), cons(X, Z)) -> X
754.16/297.12	     , s(X) -> n__s(X)
754.16/297.12	     , cons(X1, X2) -> n__cons(X1, X2)
754.16/297.12	     , activate(X) -> X
754.16/297.12	     , activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))
754.16/297.12	     , activate(n__from(X)) -> from(activate(X))
754.16/297.12	     , activate(n__s(X)) -> s(activate(X))
754.16/297.12	     , activate(n__0()) -> 0()
754.16/297.12	     , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
754.16/297.12	     , activate(n__nil()) -> nil()
754.16/297.12	     , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2))
754.16/297.12	     , 0() -> n__0()
754.16/297.12	     , first(X1, X2) -> n__first(X1, X2)
754.16/297.12	     , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
754.16/297.12	     , first(0(), Z) -> nil()
754.16/297.12	     , nil() -> n__nil()
754.16/297.12	     , from(X) -> cons(X, n__from(n__s(X)))
754.16/297.12	     , from(X) -> n__from(X)
754.16/297.12	     , sel1(s(X), cons(Y, Z)) -> sel1(X, activate(Z))
754.16/297.12	     , sel1(0(), cons(X, Z)) -> quote(X)
754.16/297.12	     , quote(n__s(X)) -> s1(quote(activate(X)))
754.16/297.12	     , quote(n__0()) -> 01()
754.16/297.12	     , quote(n__sel(X, Z)) -> sel1(activate(X), activate(Z))
754.16/297.12	     , first1(s(X), cons(Y, Z)) ->
754.16/297.12	       cons1(quote(Y), first1(X, activate(Z)))
754.16/297.12	     , first1(0(), Z) -> nil1()
754.16/297.12	     , quote1(n__first(X, Z)) -> first1(activate(X), activate(Z))
754.16/297.12	     , quote1(n__cons(X, Z)) ->
754.16/297.12	       cons1(quote(activate(X)), quote1(activate(Z)))
754.16/297.12	     , quote1(n__nil()) -> nil1()
754.16/297.12	     , unquote(01()) -> 0()
754.16/297.12	     , unquote(s1(X)) -> s(unquote(X))
754.16/297.12	     , unquote1(nil1()) -> nil()
754.16/297.12	     , unquote1(cons1(X, Z)) -> fcons(unquote(X), unquote1(Z))
754.16/297.12	     , fcons(X, Z) -> cons(X, Z) }
754.16/297.12	   Weak DPs:
754.16/297.12	     { activate^#(n__0()) -> c_10(0^#())
754.16/297.12	     , activate^#(n__nil()) -> c_12(nil^#())
754.16/297.12	     , first^#(0(), Z) -> c_17(nil^#())
754.16/297.12	     , 0^#() -> c_14()
754.16/297.12	     , nil^#() -> c_18()
754.16/297.12	     , quote^#(n__0()) -> c_24()
754.16/297.12	     , first1^#(0(), Z) -> c_27()
754.16/297.12	     , quote1^#(n__nil()) -> c_30()
754.16/297.12	     , unquote^#(01()) -> c_31(0^#())
754.16/297.12	     , unquote1^#(nil1()) -> c_33(nil^#()) }
754.16/297.12	   Obligation:
754.16/297.12	     runtime complexity
754.16/297.12	   Answer:
754.16/297.12	     MAYBE
754.16/297.12	   
754.16/297.12	   Empty strict component of the problem is NOT empty.
754.16/297.12	
754.16/297.12	
754.16/297.12	Arrrr..
754.29/297.24	EOF