MAYBE
885.42/297.15	MAYBE
885.42/297.15	
885.42/297.15	We are left with following problem, upon which TcT provides the
885.42/297.15	certificate MAYBE.
885.42/297.15	
885.42/297.15	Strict Trs:
885.42/297.15	  { le(s(x), s(y)) -> le(x, y)
885.42/297.15	  , le(s(x), 0()) -> false()
885.42/297.15	  , le(0(), y) -> true()
885.42/297.15	  , double(s(x)) -> s(s(double(x)))
885.42/297.15	  , double(0()) -> 0()
885.42/297.15	  , log(s(x)) -> loop(s(x), s(0()), 0())
885.42/297.15	  , log(0()) -> logError()
885.42/297.15	  , loop(x, s(y), z) -> if(le(x, s(y)), x, s(y), z)
885.42/297.15	  , if(false(), x, y, z) -> loop(x, double(y), s(z))
885.42/297.15	  , if(true(), x, y, z) -> z }
885.42/297.15	Obligation:
885.42/297.15	  innermost runtime complexity
885.42/297.15	Answer:
885.42/297.15	  MAYBE
885.42/297.15	
885.42/297.15	None of the processors succeeded.
885.42/297.15	
885.42/297.15	Details of failed attempt(s):
885.42/297.15	-----------------------------
885.42/297.15	1) 'empty' failed due to the following reason:
885.42/297.15	   
885.42/297.15	   Empty strict component of the problem is NOT empty.
885.42/297.15	
885.42/297.15	2) 'Best' failed due to the following reason:
885.42/297.15	   
885.42/297.15	   None of the processors succeeded.
885.42/297.15	   
885.42/297.15	   Details of failed attempt(s):
885.42/297.15	   -----------------------------
885.42/297.15	   1) 'With Problem ... (timeout of 297 seconds)' failed due to the
885.42/297.15	      following reason:
885.42/297.15	      
885.42/297.15	      Computation stopped due to timeout after 297.0 seconds.
885.42/297.15	   
885.42/297.15	   2) 'Best' failed due to the following reason:
885.42/297.15	      
885.42/297.15	      None of the processors succeeded.
885.42/297.15	      
885.42/297.15	      Details of failed attempt(s):
885.42/297.15	      -----------------------------
885.42/297.15	      1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
885.42/297.15	         seconds)' failed due to the following reason:
885.42/297.15	         
885.42/297.15	         Computation stopped due to timeout after 148.0 seconds.
885.42/297.15	      
885.42/297.15	      2) 'Best' failed due to the following reason:
885.42/297.15	         
885.42/297.15	         None of the processors succeeded.
885.42/297.15	         
885.42/297.15	         Details of failed attempt(s):
885.42/297.15	         -----------------------------
885.42/297.15	         1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
885.42/297.15	            following reason:
885.42/297.15	            
885.42/297.15	            The input cannot be shown compatible
885.42/297.15	         
885.42/297.15	         2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
885.42/297.15	            to the following reason:
885.42/297.15	            
885.42/297.15	            The input cannot be shown compatible
885.42/297.15	         
885.42/297.15	      
885.42/297.15	      3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
885.42/297.15	         failed due to the following reason:
885.42/297.15	         
885.42/297.15	         None of the processors succeeded.
885.42/297.15	         
885.42/297.15	         Details of failed attempt(s):
885.42/297.15	         -----------------------------
885.42/297.15	         1) 'Bounds with minimal-enrichment and initial automaton 'match''
885.42/297.15	            failed due to the following reason:
885.42/297.15	            
885.42/297.15	            match-boundness of the problem could not be verified.
885.42/297.15	         
885.42/297.15	         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
885.42/297.15	            failed due to the following reason:
885.42/297.15	            
885.42/297.15	            match-boundness of the problem could not be verified.
885.42/297.15	         
885.42/297.15	      
885.42/297.15	   
885.42/297.15	
885.42/297.15	
885.42/297.15	Arrrr..
885.66/297.20	EOF