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