MAYBE
1184.70/297.16	MAYBE
1184.70/297.16	
1184.70/297.16	We are left with following problem, upon which TcT provides the
1184.70/297.16	certificate MAYBE.
1184.70/297.16	
1184.70/297.16	Strict Trs:
1184.70/297.16	  { dbl(X) -> n__dbl(X)
1184.70/297.16	  , dbl(0()) -> 0()
1184.70/297.16	  , dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
1184.70/297.16	  , s(X) -> n__s(X)
1184.70/297.16	  , activate(X) -> X
1184.70/297.16	  , activate(n__s(X)) -> s(X)
1184.70/297.16	  , activate(n__dbl(X)) -> dbl(activate(X))
1184.70/297.16	  , activate(n__dbls(X)) -> dbls(activate(X))
1184.70/297.16	  , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2))
1184.70/297.16	  , activate(n__indx(X1, X2)) -> indx(activate(X1), X2)
1184.70/297.16	  , activate(n__from(X)) -> from(X)
1184.70/297.16	  , dbls(X) -> n__dbls(X)
1184.70/297.16	  , dbls(nil()) -> nil()
1184.70/297.16	  , dbls(cons(X, Y)) ->
1184.70/297.16	    cons(n__dbl(activate(X)), n__dbls(activate(Y)))
1184.70/297.16	  , sel(X1, X2) -> n__sel(X1, X2)
1184.70/297.16	  , sel(0(), cons(X, Y)) -> activate(X)
1184.70/297.16	  , sel(s(X), cons(Y, Z)) -> sel(activate(X), activate(Z))
1184.70/297.16	  , indx(X1, X2) -> n__indx(X1, X2)
1184.70/297.16	  , indx(nil(), X) -> nil()
1184.70/297.16	  , indx(cons(X, Y), Z) ->
1184.70/297.16	    cons(n__sel(activate(X), activate(Z)),
1184.70/297.16	         n__indx(activate(Y), activate(Z)))
1184.70/297.16	  , from(X) -> cons(activate(X), n__from(n__s(activate(X))))
1184.70/297.16	  , from(X) -> n__from(X) }
1184.70/297.16	Obligation:
1184.70/297.16	  runtime complexity
1184.70/297.16	Answer:
1184.70/297.16	  MAYBE
1184.70/297.16	
1184.70/297.16	None of the processors succeeded.
1184.70/297.16	
1184.70/297.16	Details of failed attempt(s):
1184.70/297.16	-----------------------------
1184.70/297.16	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
1184.70/297.16	   following reason:
1184.70/297.16	   
1184.70/297.16	   Computation stopped due to timeout after 297.0 seconds.
1184.70/297.16	
1184.70/297.16	2) 'Best' failed due to the following reason:
1184.70/297.16	   
1184.70/297.16	   None of the processors succeeded.
1184.70/297.16	   
1184.70/297.16	   Details of failed attempt(s):
1184.70/297.16	   -----------------------------
1184.70/297.16	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
1184.70/297.16	      seconds)' failed due to the following reason:
1184.70/297.16	      
1184.70/297.16	      None of the processors succeeded.
1184.70/297.16	      
1184.70/297.16	      Details of failed attempt(s):
1184.70/297.16	      -----------------------------
1184.70/297.16	      1) 'empty' failed due to the following reason:
1184.70/297.16	         
1184.70/297.16	         Empty strict component of the problem is NOT empty.
1184.70/297.16	      
1184.70/297.16	      2) 'With Problem ...' failed due to the following reason:
1184.70/297.16	         
1184.70/297.16	         None of the processors succeeded.
1184.70/297.16	         
1184.70/297.16	         Details of failed attempt(s):
1184.70/297.16	         -----------------------------
1184.70/297.16	         1) 'empty' failed due to the following reason:
1184.70/297.16	            
1184.70/297.16	            Empty strict component of the problem is NOT empty.
1184.70/297.16	         
1184.70/297.16	         2) 'Fastest' failed due to the following reason:
1184.70/297.16	            
1184.70/297.16	            None of the processors succeeded.
1184.70/297.16	            
1184.70/297.16	            Details of failed attempt(s):
1184.70/297.16	            -----------------------------
1184.70/297.16	            1) 'With Problem ...' failed due to the following reason:
1184.70/297.16	               
1184.70/297.16	               None of the processors succeeded.
1184.70/297.16	               
1184.70/297.16	               Details of failed attempt(s):
1184.70/297.16	               -----------------------------
1184.70/297.16	               1) 'empty' failed due to the following reason:
1184.70/297.16	                  
1184.70/297.16	                  Empty strict component of the problem is NOT empty.
1184.70/297.16	               
1184.70/297.16	               2) 'With Problem ...' failed due to the following reason:
1184.70/297.16	                  
1184.70/297.16	                  None of the processors succeeded.
1184.70/297.16	                  
1184.70/297.16	                  Details of failed attempt(s):
1184.70/297.16	                  -----------------------------
1184.70/297.16	                  1) 'empty' failed due to the following reason:
1184.70/297.16	                     
1184.70/297.16	                     Empty strict component of the problem is NOT empty.
1184.70/297.16	                  
1184.70/297.16	                  2) 'With Problem ...' failed due to the following reason:
1184.70/297.16	                     
1184.70/297.16	                     None of the processors succeeded.
1184.70/297.16	                     
1184.70/297.16	                     Details of failed attempt(s):
1184.70/297.16	                     -----------------------------
1184.70/297.16	                     1) 'empty' failed due to the following reason:
1184.70/297.16	                        
1184.70/297.16	                        Empty strict component of the problem is NOT empty.
1184.70/297.16	                     
1184.70/297.16	                     2) 'With Problem ...' failed due to the following reason:
1184.70/297.16	                        
1184.70/297.16	                        Empty strict component of the problem is NOT empty.
1184.70/297.16	                     
1184.70/297.16	                  
1184.70/297.16	               
1184.70/297.16	            
1184.70/297.16	            2) 'With Problem ...' failed due to the following reason:
1184.70/297.16	               
1184.70/297.16	               None of the processors succeeded.
1184.70/297.16	               
1184.70/297.16	               Details of failed attempt(s):
1184.70/297.16	               -----------------------------
1184.70/297.16	               1) 'empty' failed due to the following reason:
1184.70/297.16	                  
1184.70/297.16	                  Empty strict component of the problem is NOT empty.
1184.70/297.16	               
1184.70/297.16	               2) 'With Problem ...' failed due to the following reason:
1184.70/297.16	                  
1184.70/297.16	                  Empty strict component of the problem is NOT empty.
1184.70/297.16	               
1184.70/297.16	            
1184.70/297.16	         
1184.70/297.16	      
1184.70/297.16	   
1184.70/297.16	   2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
1184.70/297.16	      failed due to the following reason:
1184.70/297.16	      
1184.70/297.16	      None of the processors succeeded.
1184.70/297.16	      
1184.70/297.16	      Details of failed attempt(s):
1184.70/297.16	      -----------------------------
1184.70/297.16	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
1184.70/297.16	         failed due to the following reason:
1184.70/297.16	         
1184.70/297.16	         match-boundness of the problem could not be verified.
1184.70/297.16	      
1184.70/297.16	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
1184.70/297.16	         failed due to the following reason:
1184.70/297.16	         
1184.70/297.16	         match-boundness of the problem could not be verified.
1184.70/297.16	      
1184.70/297.16	   
1184.70/297.16	   3) 'Best' failed due to the following reason:
1184.70/297.16	      
1184.70/297.16	      None of the processors succeeded.
1184.70/297.16	      
1184.70/297.16	      Details of failed attempt(s):
1184.70/297.16	      -----------------------------
1184.70/297.16	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
1184.70/297.16	         following reason:
1184.70/297.16	         
1184.70/297.16	         The processor is inapplicable, reason:
1184.70/297.16	           Processor only applicable for innermost runtime complexity analysis
1184.70/297.16	      
1184.70/297.16	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
1184.70/297.16	         to the following reason:
1184.70/297.16	         
1184.70/297.16	         The processor is inapplicable, reason:
1184.70/297.16	           Processor only applicable for innermost runtime complexity analysis
1184.70/297.16	      
1184.70/297.16	   
1184.70/297.16	
1184.70/297.16	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
1184.70/297.16	   the following reason:
1184.70/297.16	   
1184.70/297.16	   We add the following weak dependency pairs:
1184.70/297.16	   
1184.70/297.16	   Strict DPs:
1184.70/297.16	     { dbl^#(X) -> c_1(X)
1184.70/297.16	     , dbl^#(0()) -> c_2()
1184.70/297.16	     , dbl^#(s(X)) -> c_3(s^#(n__s(n__dbl(activate(X)))))
1184.70/297.16	     , s^#(X) -> c_4(X)
1184.70/297.16	     , activate^#(X) -> c_5(X)
1184.70/297.16	     , activate^#(n__s(X)) -> c_6(s^#(X))
1184.70/297.16	     , activate^#(n__dbl(X)) -> c_7(dbl^#(activate(X)))
1184.70/297.16	     , activate^#(n__dbls(X)) -> c_8(dbls^#(activate(X)))
1184.70/297.16	     , activate^#(n__sel(X1, X2)) ->
1184.70/297.16	       c_9(sel^#(activate(X1), activate(X2)))
1184.70/297.16	     , activate^#(n__indx(X1, X2)) -> c_10(indx^#(activate(X1), X2))
1184.70/297.16	     , activate^#(n__from(X)) -> c_11(from^#(X))
1184.70/297.16	     , dbls^#(X) -> c_12(X)
1184.70/297.16	     , dbls^#(nil()) -> c_13()
1184.70/297.16	     , dbls^#(cons(X, Y)) -> c_14(activate^#(X), activate^#(Y))
1184.70/297.16	     , sel^#(X1, X2) -> c_15(X1, X2)
1184.70/297.16	     , sel^#(0(), cons(X, Y)) -> c_16(activate^#(X))
1184.70/297.16	     , sel^#(s(X), cons(Y, Z)) -> c_17(sel^#(activate(X), activate(Z)))
1184.70/297.16	     , indx^#(X1, X2) -> c_18(X1, X2)
1184.70/297.16	     , indx^#(nil(), X) -> c_19()
1184.70/297.16	     , indx^#(cons(X, Y), Z) ->
1184.70/297.16	       c_20(activate^#(X), activate^#(Z), activate^#(Y), activate^#(Z))
1184.70/297.16	     , from^#(X) -> c_21(activate^#(X), activate^#(X))
1184.70/297.16	     , from^#(X) -> c_22(X) }
1184.70/297.16	   
1184.70/297.16	   and mark the set of starting terms.
1184.70/297.16	   
1184.70/297.16	   We are left with following problem, upon which TcT provides the
1184.70/297.16	   certificate MAYBE.
1184.70/297.16	   
1184.70/297.16	   Strict DPs:
1184.70/297.16	     { dbl^#(X) -> c_1(X)
1184.70/297.16	     , dbl^#(0()) -> c_2()
1184.70/297.16	     , dbl^#(s(X)) -> c_3(s^#(n__s(n__dbl(activate(X)))))
1184.70/297.16	     , s^#(X) -> c_4(X)
1184.70/297.16	     , activate^#(X) -> c_5(X)
1184.70/297.16	     , activate^#(n__s(X)) -> c_6(s^#(X))
1184.70/297.16	     , activate^#(n__dbl(X)) -> c_7(dbl^#(activate(X)))
1184.70/297.16	     , activate^#(n__dbls(X)) -> c_8(dbls^#(activate(X)))
1184.70/297.16	     , activate^#(n__sel(X1, X2)) ->
1184.70/297.16	       c_9(sel^#(activate(X1), activate(X2)))
1184.70/297.16	     , activate^#(n__indx(X1, X2)) -> c_10(indx^#(activate(X1), X2))
1184.70/297.16	     , activate^#(n__from(X)) -> c_11(from^#(X))
1184.70/297.16	     , dbls^#(X) -> c_12(X)
1184.70/297.16	     , dbls^#(nil()) -> c_13()
1184.70/297.16	     , dbls^#(cons(X, Y)) -> c_14(activate^#(X), activate^#(Y))
1184.70/297.16	     , sel^#(X1, X2) -> c_15(X1, X2)
1184.70/297.16	     , sel^#(0(), cons(X, Y)) -> c_16(activate^#(X))
1184.70/297.16	     , sel^#(s(X), cons(Y, Z)) -> c_17(sel^#(activate(X), activate(Z)))
1184.70/297.16	     , indx^#(X1, X2) -> c_18(X1, X2)
1184.70/297.16	     , indx^#(nil(), X) -> c_19()
1184.70/297.16	     , indx^#(cons(X, Y), Z) ->
1184.70/297.16	       c_20(activate^#(X), activate^#(Z), activate^#(Y), activate^#(Z))
1184.70/297.16	     , from^#(X) -> c_21(activate^#(X), activate^#(X))
1184.70/297.16	     , from^#(X) -> c_22(X) }
1184.70/297.16	   Strict Trs:
1184.70/297.16	     { dbl(X) -> n__dbl(X)
1184.70/297.16	     , dbl(0()) -> 0()
1184.70/297.16	     , dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
1184.70/297.16	     , s(X) -> n__s(X)
1184.70/297.16	     , activate(X) -> X
1184.70/297.16	     , activate(n__s(X)) -> s(X)
1184.70/297.16	     , activate(n__dbl(X)) -> dbl(activate(X))
1184.70/297.16	     , activate(n__dbls(X)) -> dbls(activate(X))
1184.70/297.16	     , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2))
1184.70/297.16	     , activate(n__indx(X1, X2)) -> indx(activate(X1), X2)
1184.70/297.16	     , activate(n__from(X)) -> from(X)
1184.70/297.16	     , dbls(X) -> n__dbls(X)
1184.70/297.16	     , dbls(nil()) -> nil()
1184.70/297.16	     , dbls(cons(X, Y)) ->
1184.70/297.16	       cons(n__dbl(activate(X)), n__dbls(activate(Y)))
1184.70/297.16	     , sel(X1, X2) -> n__sel(X1, X2)
1184.70/297.16	     , sel(0(), cons(X, Y)) -> activate(X)
1184.70/297.16	     , sel(s(X), cons(Y, Z)) -> sel(activate(X), activate(Z))
1184.70/297.16	     , indx(X1, X2) -> n__indx(X1, X2)
1184.70/297.16	     , indx(nil(), X) -> nil()
1184.70/297.16	     , indx(cons(X, Y), Z) ->
1184.70/297.16	       cons(n__sel(activate(X), activate(Z)),
1184.70/297.16	            n__indx(activate(Y), activate(Z)))
1184.70/297.16	     , from(X) -> cons(activate(X), n__from(n__s(activate(X))))
1184.70/297.16	     , from(X) -> n__from(X) }
1184.70/297.16	   Obligation:
1184.70/297.16	     runtime complexity
1184.70/297.16	   Answer:
1184.70/297.16	     MAYBE
1184.70/297.16	   
1184.70/297.16	   We estimate the number of application of {2,13,19} by applications
1184.70/297.16	   of Pre({2,13,19}) = {1,4,5,7,8,10,12,15,18,22}. Here rules are
1184.70/297.16	   labeled as follows:
1184.70/297.16	   
1184.70/297.16	     DPs:
1184.70/297.16	       { 1: dbl^#(X) -> c_1(X)
1184.70/297.16	       , 2: dbl^#(0()) -> c_2()
1184.70/297.16	       , 3: dbl^#(s(X)) -> c_3(s^#(n__s(n__dbl(activate(X)))))
1184.70/297.16	       , 4: s^#(X) -> c_4(X)
1184.70/297.16	       , 5: activate^#(X) -> c_5(X)
1184.70/297.16	       , 6: activate^#(n__s(X)) -> c_6(s^#(X))
1184.70/297.16	       , 7: activate^#(n__dbl(X)) -> c_7(dbl^#(activate(X)))
1184.70/297.16	       , 8: activate^#(n__dbls(X)) -> c_8(dbls^#(activate(X)))
1184.70/297.16	       , 9: activate^#(n__sel(X1, X2)) ->
1184.70/297.16	            c_9(sel^#(activate(X1), activate(X2)))
1184.70/297.16	       , 10: activate^#(n__indx(X1, X2)) -> c_10(indx^#(activate(X1), X2))
1184.70/297.16	       , 11: activate^#(n__from(X)) -> c_11(from^#(X))
1184.70/297.16	       , 12: dbls^#(X) -> c_12(X)
1184.70/297.16	       , 13: dbls^#(nil()) -> c_13()
1184.70/297.16	       , 14: dbls^#(cons(X, Y)) -> c_14(activate^#(X), activate^#(Y))
1184.70/297.16	       , 15: sel^#(X1, X2) -> c_15(X1, X2)
1184.70/297.16	       , 16: sel^#(0(), cons(X, Y)) -> c_16(activate^#(X))
1184.70/297.16	       , 17: sel^#(s(X), cons(Y, Z)) ->
1184.70/297.16	             c_17(sel^#(activate(X), activate(Z)))
1184.70/297.16	       , 18: indx^#(X1, X2) -> c_18(X1, X2)
1184.70/297.16	       , 19: indx^#(nil(), X) -> c_19()
1184.70/297.16	       , 20: indx^#(cons(X, Y), Z) ->
1184.70/297.16	             c_20(activate^#(X), activate^#(Z), activate^#(Y), activate^#(Z))
1184.70/297.16	       , 21: from^#(X) -> c_21(activate^#(X), activate^#(X))
1184.70/297.16	       , 22: from^#(X) -> c_22(X) }
1184.70/297.16	   
1184.70/297.16	   We are left with following problem, upon which TcT provides the
1184.70/297.16	   certificate MAYBE.
1184.70/297.16	   
1184.70/297.16	   Strict DPs:
1184.70/297.16	     { dbl^#(X) -> c_1(X)
1184.70/297.16	     , dbl^#(s(X)) -> c_3(s^#(n__s(n__dbl(activate(X)))))
1184.70/297.16	     , s^#(X) -> c_4(X)
1184.70/297.16	     , activate^#(X) -> c_5(X)
1184.70/297.16	     , activate^#(n__s(X)) -> c_6(s^#(X))
1184.70/297.16	     , activate^#(n__dbl(X)) -> c_7(dbl^#(activate(X)))
1184.70/297.16	     , activate^#(n__dbls(X)) -> c_8(dbls^#(activate(X)))
1184.70/297.16	     , activate^#(n__sel(X1, X2)) ->
1184.70/297.16	       c_9(sel^#(activate(X1), activate(X2)))
1184.70/297.16	     , activate^#(n__indx(X1, X2)) -> c_10(indx^#(activate(X1), X2))
1184.70/297.16	     , activate^#(n__from(X)) -> c_11(from^#(X))
1184.70/297.16	     , dbls^#(X) -> c_12(X)
1184.70/297.16	     , dbls^#(cons(X, Y)) -> c_14(activate^#(X), activate^#(Y))
1184.70/297.16	     , sel^#(X1, X2) -> c_15(X1, X2)
1184.70/297.16	     , sel^#(0(), cons(X, Y)) -> c_16(activate^#(X))
1184.70/297.16	     , sel^#(s(X), cons(Y, Z)) -> c_17(sel^#(activate(X), activate(Z)))
1184.70/297.16	     , indx^#(X1, X2) -> c_18(X1, X2)
1184.70/297.16	     , indx^#(cons(X, Y), Z) ->
1184.70/297.16	       c_20(activate^#(X), activate^#(Z), activate^#(Y), activate^#(Z))
1184.70/297.16	     , from^#(X) -> c_21(activate^#(X), activate^#(X))
1184.70/297.16	     , from^#(X) -> c_22(X) }
1184.70/297.16	   Strict Trs:
1184.70/297.16	     { dbl(X) -> n__dbl(X)
1184.70/297.16	     , dbl(0()) -> 0()
1184.70/297.16	     , dbl(s(X)) -> s(n__s(n__dbl(activate(X))))
1184.70/297.16	     , s(X) -> n__s(X)
1184.70/297.16	     , activate(X) -> X
1184.70/297.16	     , activate(n__s(X)) -> s(X)
1184.70/297.16	     , activate(n__dbl(X)) -> dbl(activate(X))
1184.70/297.16	     , activate(n__dbls(X)) -> dbls(activate(X))
1184.70/297.16	     , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2))
1184.70/297.16	     , activate(n__indx(X1, X2)) -> indx(activate(X1), X2)
1184.70/297.16	     , activate(n__from(X)) -> from(X)
1184.70/297.16	     , dbls(X) -> n__dbls(X)
1184.70/297.16	     , dbls(nil()) -> nil()
1184.70/297.16	     , dbls(cons(X, Y)) ->
1184.70/297.16	       cons(n__dbl(activate(X)), n__dbls(activate(Y)))
1184.70/297.16	     , sel(X1, X2) -> n__sel(X1, X2)
1184.70/297.16	     , sel(0(), cons(X, Y)) -> activate(X)
1184.70/297.16	     , sel(s(X), cons(Y, Z)) -> sel(activate(X), activate(Z))
1184.70/297.16	     , indx(X1, X2) -> n__indx(X1, X2)
1184.70/297.16	     , indx(nil(), X) -> nil()
1184.70/297.16	     , indx(cons(X, Y), Z) ->
1184.70/297.16	       cons(n__sel(activate(X), activate(Z)),
1184.70/297.16	            n__indx(activate(Y), activate(Z)))
1184.70/297.16	     , from(X) -> cons(activate(X), n__from(n__s(activate(X))))
1184.70/297.16	     , from(X) -> n__from(X) }
1184.70/297.16	   Weak DPs:
1184.70/297.16	     { dbl^#(0()) -> c_2()
1184.70/297.16	     , dbls^#(nil()) -> c_13()
1184.70/297.16	     , indx^#(nil(), X) -> c_19() }
1184.70/297.16	   Obligation:
1184.70/297.16	     runtime complexity
1184.70/297.16	   Answer:
1184.70/297.16	     MAYBE
1184.70/297.16	   
1184.70/297.16	   Empty strict component of the problem is NOT empty.
1184.70/297.16	
1184.70/297.16	
1184.70/297.16	Arrrr..
1185.80/298.08	EOF