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