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