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