MAYBE
255.39/119.53	MAYBE
255.39/119.53	
255.39/119.53	We are left with following problem, upon which TcT provides the
255.39/119.53	certificate MAYBE.
255.39/119.53	
255.39/119.53	Strict Trs:
255.39/119.53	  { le(0(), y) -> true()
255.39/119.53	  , le(s(x), 0()) -> false()
255.39/119.53	  , le(s(x), s(y)) -> le(x, y)
255.39/119.53	  , minus(0(), y) -> 0()
255.39/119.53	  , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y)
255.39/119.53	  , if_minus(true(), s(x), y) -> 0()
255.39/119.53	  , if_minus(false(), s(x), y) -> s(minus(x, y))
255.39/119.53	  , mod(0(), y) -> 0()
255.39/119.53	  , mod(s(x), 0()) -> 0()
255.39/119.53	  , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
255.39/119.53	  , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
255.39/119.53	  , if_mod(false(), s(x), s(y)) -> s(x) }
255.39/119.53	Obligation:
255.39/119.53	  runtime complexity
255.39/119.53	Answer:
255.39/119.53	  MAYBE
255.39/119.53	
255.39/119.53	None of the processors succeeded.
255.39/119.53	
255.39/119.53	Details of failed attempt(s):
255.39/119.53	-----------------------------
255.39/119.53	1) 'Best' failed due to the following reason:
255.39/119.53	   
255.39/119.53	   None of the processors succeeded.
255.39/119.53	   
255.39/119.53	   Details of failed attempt(s):
255.39/119.53	   -----------------------------
255.39/119.53	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
255.39/119.53	      seconds)' failed due to the following reason:
255.39/119.53	      
255.39/119.53	      None of the processors succeeded.
255.39/119.53	      
255.39/119.53	      Details of failed attempt(s):
255.39/119.53	      -----------------------------
255.39/119.53	      1) 'empty' failed due to the following reason:
255.39/119.53	         
255.39/119.53	         Empty strict component of the problem is NOT empty.
255.39/119.53	      
255.39/119.53	      2) 'With Problem ...' failed due to the following reason:
255.39/119.53	         
255.39/119.53	         None of the processors succeeded.
255.39/119.53	         
255.39/119.53	         Details of failed attempt(s):
255.39/119.53	         -----------------------------
255.39/119.53	         1) 'empty' failed due to the following reason:
255.39/119.53	            
255.39/119.53	            Empty strict component of the problem is NOT empty.
255.39/119.53	         
255.39/119.53	         2) 'Fastest' failed due to the following reason:
255.39/119.53	            
255.39/119.53	            None of the processors succeeded.
255.39/119.53	            
255.39/119.53	            Details of failed attempt(s):
255.39/119.53	            -----------------------------
255.39/119.53	            1) 'With Problem ...' failed due to the following reason:
255.39/119.53	               
255.39/119.53	               None of the processors succeeded.
255.39/119.53	               
255.39/119.53	               Details of failed attempt(s):
255.39/119.53	               -----------------------------
255.39/119.53	               1) 'empty' failed due to the following reason:
255.39/119.53	                  
255.39/119.53	                  Empty strict component of the problem is NOT empty.
255.39/119.53	               
255.39/119.53	               2) 'With Problem ...' failed due to the following reason:
255.39/119.53	                  
255.39/119.53	                  Empty strict component of the problem is NOT empty.
255.39/119.53	               
255.39/119.53	            
255.39/119.53	            2) 'With Problem ...' failed due to the following reason:
255.39/119.53	               
255.39/119.53	               None of the processors succeeded.
255.39/119.53	               
255.39/119.53	               Details of failed attempt(s):
255.39/119.53	               -----------------------------
255.39/119.53	               1) 'empty' failed due to the following reason:
255.39/119.53	                  
255.39/119.53	                  Empty strict component of the problem is NOT empty.
255.39/119.53	               
255.39/119.53	               2) 'With Problem ...' failed due to the following reason:
255.39/119.53	                  
255.39/119.53	                  None of the processors succeeded.
255.39/119.53	                  
255.39/119.53	                  Details of failed attempt(s):
255.39/119.53	                  -----------------------------
255.39/119.53	                  1) 'empty' failed due to the following reason:
255.39/119.53	                     
255.39/119.53	                     Empty strict component of the problem is NOT empty.
255.39/119.53	                  
255.39/119.53	                  2) 'With Problem ...' failed due to the following reason:
255.39/119.53	                     
255.39/119.53	                     None of the processors succeeded.
255.39/119.53	                     
255.39/119.53	                     Details of failed attempt(s):
255.39/119.53	                     -----------------------------
255.39/119.53	                     1) 'empty' failed due to the following reason:
255.39/119.53	                        
255.39/119.53	                        Empty strict component of the problem is NOT empty.
255.39/119.53	                     
255.39/119.53	                     2) 'With Problem ...' failed due to the following reason:
255.39/119.53	                        
255.39/119.53	                        Empty strict component of the problem is NOT empty.
255.39/119.53	                     
255.39/119.53	                  
255.39/119.53	               
255.39/119.53	            
255.39/119.53	         
255.39/119.53	      
255.39/119.53	   
255.39/119.53	   2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
255.39/119.53	      failed due to the following reason:
255.39/119.53	      
255.39/119.53	      None of the processors succeeded.
255.39/119.53	      
255.39/119.53	      Details of failed attempt(s):
255.39/119.53	      -----------------------------
255.39/119.53	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
255.39/119.53	         failed due to the following reason:
255.39/119.53	         
255.39/119.53	         match-boundness of the problem could not be verified.
255.39/119.53	      
255.39/119.53	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
255.39/119.53	         failed due to the following reason:
255.39/119.53	         
255.39/119.53	         match-boundness of the problem could not be verified.
255.39/119.53	      
255.39/119.53	   
255.39/119.53	   3) 'Best' failed due to the following reason:
255.39/119.53	      
255.39/119.53	      None of the processors succeeded.
255.39/119.53	      
255.39/119.53	      Details of failed attempt(s):
255.39/119.53	      -----------------------------
255.39/119.53	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
255.39/119.53	         following reason:
255.39/119.53	         
255.39/119.53	         The processor is inapplicable, reason:
255.39/119.53	           Processor only applicable for innermost runtime complexity analysis
255.39/119.53	      
255.39/119.53	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
255.39/119.53	         to the following reason:
255.39/119.53	         
255.39/119.53	         The processor is inapplicable, reason:
255.39/119.53	           Processor only applicable for innermost runtime complexity analysis
255.39/119.53	      
255.39/119.53	   
255.39/119.53	
255.39/119.53	2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
255.39/119.53	   the following reason:
255.39/119.53	   
255.39/119.53	   We add the following weak dependency pairs:
255.39/119.53	   
255.39/119.53	   Strict DPs:
255.39/119.53	     { le^#(0(), y) -> c_1()
255.39/119.53	     , le^#(s(x), 0()) -> c_2()
255.39/119.53	     , le^#(s(x), s(y)) -> c_3(le^#(x, y))
255.39/119.53	     , minus^#(0(), y) -> c_4()
255.39/119.53	     , minus^#(s(x), y) -> c_5(if_minus^#(le(s(x), y), s(x), y))
255.39/119.53	     , if_minus^#(true(), s(x), y) -> c_6()
255.39/119.53	     , if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y))
255.39/119.53	     , mod^#(0(), y) -> c_8()
255.39/119.53	     , mod^#(s(x), 0()) -> c_9()
255.39/119.53	     , mod^#(s(x), s(y)) -> c_10(if_mod^#(le(y, x), s(x), s(y)))
255.39/119.53	     , if_mod^#(true(), s(x), s(y)) -> c_11(mod^#(minus(x, y), s(y)))
255.39/119.53	     , if_mod^#(false(), s(x), s(y)) -> c_12(x) }
255.39/119.53	   
255.39/119.53	   and mark the set of starting terms.
255.39/119.53	   
255.39/119.53	   We are left with following problem, upon which TcT provides the
255.39/119.53	   certificate MAYBE.
255.39/119.53	   
255.39/119.53	   Strict DPs:
255.39/119.53	     { le^#(0(), y) -> c_1()
255.39/119.53	     , le^#(s(x), 0()) -> c_2()
255.39/119.53	     , le^#(s(x), s(y)) -> c_3(le^#(x, y))
255.39/119.53	     , minus^#(0(), y) -> c_4()
255.39/119.53	     , minus^#(s(x), y) -> c_5(if_minus^#(le(s(x), y), s(x), y))
255.39/119.53	     , if_minus^#(true(), s(x), y) -> c_6()
255.39/119.53	     , if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y))
255.39/119.53	     , mod^#(0(), y) -> c_8()
255.39/119.53	     , mod^#(s(x), 0()) -> c_9()
255.39/119.53	     , mod^#(s(x), s(y)) -> c_10(if_mod^#(le(y, x), s(x), s(y)))
255.39/119.53	     , if_mod^#(true(), s(x), s(y)) -> c_11(mod^#(minus(x, y), s(y)))
255.39/119.53	     , if_mod^#(false(), s(x), s(y)) -> c_12(x) }
255.39/119.53	   Strict Trs:
255.39/119.53	     { le(0(), y) -> true()
255.39/119.53	     , le(s(x), 0()) -> false()
255.39/119.53	     , le(s(x), s(y)) -> le(x, y)
255.39/119.53	     , minus(0(), y) -> 0()
255.39/119.53	     , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y)
255.39/119.53	     , if_minus(true(), s(x), y) -> 0()
255.39/119.53	     , if_minus(false(), s(x), y) -> s(minus(x, y))
255.39/119.53	     , mod(0(), y) -> 0()
255.39/119.53	     , mod(s(x), 0()) -> 0()
255.39/119.53	     , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
255.39/119.53	     , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
255.39/119.53	     , if_mod(false(), s(x), s(y)) -> s(x) }
255.39/119.53	   Obligation:
255.39/119.53	     runtime complexity
255.39/119.53	   Answer:
255.39/119.53	     MAYBE
255.39/119.53	   
255.39/119.53	   We estimate the number of application of {1,2,4,6,8,9} by
255.39/119.53	   applications of Pre({1,2,4,6,8,9}) = {3,5,7,11,12}. Here rules are
255.39/119.53	   labeled as follows:
255.39/119.53	   
255.39/119.53	     DPs:
255.39/119.53	       { 1: le^#(0(), y) -> c_1()
255.39/119.53	       , 2: le^#(s(x), 0()) -> c_2()
255.39/119.53	       , 3: le^#(s(x), s(y)) -> c_3(le^#(x, y))
255.39/119.53	       , 4: minus^#(0(), y) -> c_4()
255.39/119.53	       , 5: minus^#(s(x), y) -> c_5(if_minus^#(le(s(x), y), s(x), y))
255.39/119.53	       , 6: if_minus^#(true(), s(x), y) -> c_6()
255.39/119.53	       , 7: if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y))
255.39/119.53	       , 8: mod^#(0(), y) -> c_8()
255.39/119.53	       , 9: mod^#(s(x), 0()) -> c_9()
255.39/119.53	       , 10: mod^#(s(x), s(y)) -> c_10(if_mod^#(le(y, x), s(x), s(y)))
255.39/119.53	       , 11: if_mod^#(true(), s(x), s(y)) ->
255.39/119.53	             c_11(mod^#(minus(x, y), s(y)))
255.39/119.53	       , 12: if_mod^#(false(), s(x), s(y)) -> c_12(x) }
255.39/119.53	   
255.39/119.53	   We are left with following problem, upon which TcT provides the
255.39/119.53	   certificate MAYBE.
255.39/119.53	   
255.39/119.53	   Strict DPs:
255.39/119.53	     { le^#(s(x), s(y)) -> c_3(le^#(x, y))
255.39/119.53	     , minus^#(s(x), y) -> c_5(if_minus^#(le(s(x), y), s(x), y))
255.39/119.53	     , if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y))
255.39/119.53	     , mod^#(s(x), s(y)) -> c_10(if_mod^#(le(y, x), s(x), s(y)))
255.39/119.53	     , if_mod^#(true(), s(x), s(y)) -> c_11(mod^#(minus(x, y), s(y)))
255.39/119.53	     , if_mod^#(false(), s(x), s(y)) -> c_12(x) }
255.39/119.53	   Strict Trs:
255.39/119.53	     { le(0(), y) -> true()
255.39/119.53	     , le(s(x), 0()) -> false()
255.39/119.53	     , le(s(x), s(y)) -> le(x, y)
255.39/119.53	     , minus(0(), y) -> 0()
255.39/119.53	     , minus(s(x), y) -> if_minus(le(s(x), y), s(x), y)
255.39/119.53	     , if_minus(true(), s(x), y) -> 0()
255.39/119.53	     , if_minus(false(), s(x), y) -> s(minus(x, y))
255.39/119.53	     , mod(0(), y) -> 0()
255.39/119.53	     , mod(s(x), 0()) -> 0()
255.39/119.53	     , mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
255.39/119.53	     , if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
255.39/119.53	     , if_mod(false(), s(x), s(y)) -> s(x) }
255.39/119.53	   Weak DPs:
255.39/119.53	     { le^#(0(), y) -> c_1()
255.39/119.53	     , le^#(s(x), 0()) -> c_2()
255.39/119.53	     , minus^#(0(), y) -> c_4()
255.39/119.53	     , if_minus^#(true(), s(x), y) -> c_6()
255.39/119.53	     , mod^#(0(), y) -> c_8()
255.39/119.53	     , mod^#(s(x), 0()) -> c_9() }
255.39/119.53	   Obligation:
255.39/119.53	     runtime complexity
255.39/119.53	   Answer:
255.39/119.53	     MAYBE
255.39/119.53	   
255.39/119.53	   Empty strict component of the problem is NOT empty.
255.39/119.53	
255.39/119.53	
255.39/119.53	Arrrr..
255.61/119.73	EOF