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