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