MAYBE
342.82/190.55	MAYBE
342.82/190.55	
342.82/190.55	We are left with following problem, upon which TcT provides the
342.82/190.55	certificate MAYBE.
342.82/190.55	
342.82/190.55	Strict Trs:
342.82/190.55	  { plus(0(), Y) -> Y
342.82/190.55	  , plus(s(X), Y) -> s(plus(X, Y))
342.82/190.55	  , min(X, 0()) -> X
342.82/190.55	  , min(s(X), s(Y)) -> min(X, Y)
342.82/190.55	  , min(min(X, Y), Z()) -> min(X, plus(Y, Z()))
342.82/190.55	  , quot(0(), s(Y)) -> 0()
342.82/190.55	  , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) }
342.82/190.55	Obligation:
342.82/190.55	  runtime complexity
342.82/190.55	Answer:
342.82/190.55	  MAYBE
342.82/190.55	
342.82/190.55	None of the processors succeeded.
342.82/190.55	
342.82/190.55	Details of failed attempt(s):
342.82/190.55	-----------------------------
342.82/190.55	1) 'Best' failed due to the following reason:
342.82/190.55	   
342.82/190.55	   None of the processors succeeded.
342.82/190.55	   
342.82/190.55	   Details of failed attempt(s):
342.82/190.55	   -----------------------------
342.82/190.55	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
342.82/190.55	      seconds)' failed due to the following reason:
342.82/190.55	      
342.82/190.55	      None of the processors succeeded.
342.82/190.55	      
342.82/190.55	      Details of failed attempt(s):
342.82/190.55	      -----------------------------
342.82/190.55	      1) 'empty' failed due to the following reason:
342.82/190.55	         
342.82/190.55	         Empty strict component of the problem is NOT empty.
342.82/190.55	      
342.82/190.55	      2) 'With Problem ...' failed due to the following reason:
342.82/190.55	         
342.82/190.55	         None of the processors succeeded.
342.82/190.55	         
342.82/190.55	         Details of failed attempt(s):
342.82/190.55	         -----------------------------
342.82/190.55	         1) 'empty' failed due to the following reason:
342.82/190.55	            
342.82/190.55	            Empty strict component of the problem is NOT empty.
342.82/190.55	         
342.82/190.55	         2) 'Fastest' failed due to the following reason:
342.82/190.55	            
342.82/190.55	            None of the processors succeeded.
342.82/190.55	            
342.82/190.55	            Details of failed attempt(s):
342.82/190.55	            -----------------------------
342.82/190.55	            1) 'With Problem ...' failed due to the following reason:
342.82/190.55	               
342.82/190.55	               None of the processors succeeded.
342.82/190.55	               
342.82/190.55	               Details of failed attempt(s):
342.82/190.55	               -----------------------------
342.82/190.55	               1) 'empty' failed due to the following reason:
342.82/190.55	                  
342.82/190.55	                  Empty strict component of the problem is NOT empty.
342.82/190.55	               
342.82/190.55	               2) 'With Problem ...' failed due to the following reason:
342.82/190.55	                  
342.82/190.55	                  Empty strict component of the problem is NOT empty.
342.82/190.55	               
342.82/190.55	            
342.82/190.55	            2) 'With Problem ...' failed due to the following reason:
342.82/190.55	               
342.82/190.55	               None of the processors succeeded.
342.82/190.55	               
342.82/190.55	               Details of failed attempt(s):
342.82/190.55	               -----------------------------
342.82/190.55	               1) 'empty' failed due to the following reason:
342.82/190.55	                  
342.82/190.55	                  Empty strict component of the problem is NOT empty.
342.82/190.55	               
342.82/190.55	               2) 'With Problem ...' failed due to the following reason:
342.82/190.55	                  
342.82/190.55	                  None of the processors succeeded.
342.82/190.55	                  
342.82/190.55	                  Details of failed attempt(s):
342.82/190.55	                  -----------------------------
342.82/190.55	                  1) 'empty' failed due to the following reason:
342.82/190.55	                     
342.82/190.55	                     Empty strict component of the problem is NOT empty.
342.82/190.55	                  
342.82/190.55	                  2) 'With Problem ...' failed due to the following reason:
342.82/190.55	                     
342.82/190.55	                     None of the processors succeeded.
342.82/190.55	                     
342.82/190.55	                     Details of failed attempt(s):
342.82/190.55	                     -----------------------------
342.82/190.55	                     1) 'empty' failed due to the following reason:
342.82/190.55	                        
342.82/190.55	                        Empty strict component of the problem is NOT empty.
342.82/190.55	                     
342.82/190.55	                     2) 'With Problem ...' failed due to the following reason:
342.82/190.55	                        
342.82/190.55	                        Empty strict component of the problem is NOT empty.
342.82/190.55	                     
342.82/190.55	                  
342.82/190.55	               
342.82/190.55	            
342.82/190.55	         
342.82/190.55	      
342.82/190.55	   
342.82/190.55	   2) 'Best' failed due to the following reason:
342.82/190.55	      
342.82/190.55	      None of the processors succeeded.
342.82/190.55	      
342.82/190.55	      Details of failed attempt(s):
342.82/190.55	      -----------------------------
342.82/190.55	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
342.82/190.55	         following reason:
342.82/190.55	         
342.82/190.55	         The processor is inapplicable, reason:
342.82/190.55	           Processor only applicable for innermost runtime complexity analysis
342.82/190.55	      
342.82/190.55	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
342.82/190.55	         to the following reason:
342.82/190.55	         
342.82/190.55	         The processor is inapplicable, reason:
342.82/190.55	           Processor only applicable for innermost runtime complexity analysis
342.82/190.55	      
342.82/190.55	   
342.82/190.55	   3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
342.82/190.55	      failed due to the following reason:
342.82/190.55	      
342.82/190.55	      None of the processors succeeded.
342.82/190.55	      
342.82/190.55	      Details of failed attempt(s):
342.82/190.55	      -----------------------------
342.82/190.55	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
342.82/190.55	         failed due to the following reason:
342.82/190.55	         
342.82/190.55	         match-boundness of the problem could not be verified.
342.82/190.55	      
342.82/190.55	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
342.82/190.55	         failed due to the following reason:
342.82/190.55	         
342.82/190.55	         match-boundness of the problem could not be verified.
342.82/190.55	      
342.82/190.55	   
342.82/190.55	
342.82/190.55	2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
342.82/190.55	   the following reason:
342.82/190.55	   
342.82/190.55	   We add the following weak dependency pairs:
342.82/190.55	   
342.82/190.55	   Strict DPs:
342.82/190.55	     { plus^#(0(), Y) -> c_1(Y)
342.82/190.55	     , plus^#(s(X), Y) -> c_2(plus^#(X, Y))
342.82/190.55	     , min^#(X, 0()) -> c_3(X)
342.82/190.55	     , min^#(s(X), s(Y)) -> c_4(min^#(X, Y))
342.82/190.55	     , min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())))
342.82/190.55	     , quot^#(0(), s(Y)) -> c_6()
342.82/190.55	     , quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y))) }
342.82/190.55	   
342.82/190.55	   and mark the set of starting terms.
342.82/190.55	   
342.82/190.55	   We are left with following problem, upon which TcT provides the
342.82/190.55	   certificate MAYBE.
342.82/190.55	   
342.82/190.55	   Strict DPs:
342.82/190.55	     { plus^#(0(), Y) -> c_1(Y)
342.82/190.55	     , plus^#(s(X), Y) -> c_2(plus^#(X, Y))
342.82/190.55	     , min^#(X, 0()) -> c_3(X)
342.82/190.55	     , min^#(s(X), s(Y)) -> c_4(min^#(X, Y))
342.82/190.55	     , min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())))
342.82/190.55	     , quot^#(0(), s(Y)) -> c_6()
342.82/190.55	     , quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y))) }
342.82/190.55	   Strict Trs:
342.82/190.55	     { plus(0(), Y) -> Y
342.82/190.55	     , plus(s(X), Y) -> s(plus(X, Y))
342.82/190.55	     , min(X, 0()) -> X
342.82/190.55	     , min(s(X), s(Y)) -> min(X, Y)
342.82/190.55	     , min(min(X, Y), Z()) -> min(X, plus(Y, Z()))
342.82/190.55	     , quot(0(), s(Y)) -> 0()
342.82/190.55	     , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) }
342.82/190.55	   Obligation:
342.82/190.55	     runtime complexity
342.82/190.55	   Answer:
342.82/190.55	     MAYBE
342.82/190.55	   
342.82/190.55	   We estimate the number of application of {6} by applications of
342.82/190.55	   Pre({6}) = {1,3,7}. Here rules are labeled as follows:
342.82/190.55	   
342.82/190.55	     DPs:
342.82/190.55	       { 1: plus^#(0(), Y) -> c_1(Y)
342.82/190.55	       , 2: plus^#(s(X), Y) -> c_2(plus^#(X, Y))
342.82/190.55	       , 3: min^#(X, 0()) -> c_3(X)
342.82/190.55	       , 4: min^#(s(X), s(Y)) -> c_4(min^#(X, Y))
342.82/190.55	       , 5: min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())))
342.82/190.55	       , 6: quot^#(0(), s(Y)) -> c_6()
342.82/190.55	       , 7: quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y))) }
342.82/190.55	   
342.82/190.55	   We are left with following problem, upon which TcT provides the
342.82/190.55	   certificate MAYBE.
342.82/190.55	   
342.82/190.55	   Strict DPs:
342.82/190.55	     { plus^#(0(), Y) -> c_1(Y)
342.82/190.55	     , plus^#(s(X), Y) -> c_2(plus^#(X, Y))
342.82/190.55	     , min^#(X, 0()) -> c_3(X)
342.82/190.55	     , min^#(s(X), s(Y)) -> c_4(min^#(X, Y))
342.82/190.55	     , min^#(min(X, Y), Z()) -> c_5(min^#(X, plus(Y, Z())))
342.82/190.55	     , quot^#(s(X), s(Y)) -> c_7(quot^#(min(X, Y), s(Y))) }
342.82/190.55	   Strict Trs:
342.82/190.55	     { plus(0(), Y) -> Y
342.82/190.55	     , plus(s(X), Y) -> s(plus(X, Y))
342.82/190.55	     , min(X, 0()) -> X
342.82/190.55	     , min(s(X), s(Y)) -> min(X, Y)
342.82/190.55	     , min(min(X, Y), Z()) -> min(X, plus(Y, Z()))
342.82/190.55	     , quot(0(), s(Y)) -> 0()
342.82/190.55	     , quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) }
342.82/190.55	   Weak DPs: { quot^#(0(), s(Y)) -> c_6() }
342.82/190.55	   Obligation:
342.82/190.55	     runtime complexity
342.82/190.55	   Answer:
342.82/190.55	     MAYBE
342.82/190.55	   
342.82/190.55	   Empty strict component of the problem is NOT empty.
342.82/190.55	
342.82/190.55	
342.82/190.55	Arrrr..
343.04/190.71	EOF