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