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