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