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