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