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