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