MAYBE
211.30/60.04	MAYBE
211.30/60.04	
211.30/60.04	We are left with following problem, upon which TcT provides the
211.30/60.04	certificate MAYBE.
211.30/60.04	
211.30/60.04	Strict Trs:
211.30/60.04	  { ap(ap(g(), x), y) -> y
211.30/60.04	  , ap(f(), x) -> ap(f(), app(g(), x)) }
211.30/60.04	Obligation:
211.30/60.04	  derivational complexity
211.30/60.04	Answer:
211.30/60.04	  MAYBE
211.30/60.04	
211.30/60.04	None of the processors succeeded.
211.30/60.04	
211.30/60.04	Details of failed attempt(s):
211.30/60.04	-----------------------------
211.30/60.04	1) 'Fastest (timeout of 60 seconds)' failed due to the following
211.30/60.04	   reason:
211.30/60.04	   
211.30/60.04	   Computation stopped due to timeout after 60.0 seconds.
211.30/60.04	
211.30/60.04	2) 'Inspecting Problem... (timeout of 297 seconds)' failed due to
211.30/60.04	   the following reason:
211.30/60.04	   
211.30/60.04	   We use the processor 'matrix interpretation of dimension 1' to
211.30/60.04	   orient following rules strictly.
211.30/60.04	   
211.30/60.04	   Trs: { ap(ap(g(), x), y) -> y }
211.30/60.04	   
211.30/60.04	   The induced complexity on above rules (modulo remaining rules) is
211.30/60.04	   YES(?,O(n^1)) . These rules are moved into the corresponding weak
211.30/60.04	   component(s).
211.30/60.04	   
211.30/60.04	   Sub-proof:
211.30/60.04	   ----------
211.30/60.04	     TcT has computed the following triangular matrix interpretation.
211.30/60.04	     
211.30/60.04	        [ap](x1, x2) = [1] x1 + [1] x2 + [2]
211.30/60.04	                                            
211.30/60.04	                 [g] = [0]                  
211.30/60.04	                                            
211.30/60.04	                 [f] = [2]                  
211.30/60.04	                                            
211.30/60.04	       [app](x1, x2) = [1] x1 + [1] x2 + [0]
211.30/60.04	     
211.30/60.04	     The order satisfies the following ordering constraints:
211.30/60.04	     
211.30/60.04	       [ap(ap(g(), x), y)] =  [1] x + [1] y + [4]   
211.30/60.04	                           >  [1] y + [0]           
211.30/60.04	                           =  [y]                   
211.30/60.04	                                                    
211.30/60.04	              [ap(f(), x)] =  [1] x + [4]           
211.30/60.04	                           >= [1] x + [4]           
211.30/60.04	                           =  [ap(f(), app(g(), x))]
211.30/60.04	                                                    
211.30/60.04	   
211.30/60.04	   We return to the main proof.
211.30/60.04	   
211.30/60.04	   We are left with following problem, upon which TcT provides the
211.30/60.04	   certificate MAYBE.
211.30/60.04	   
211.30/60.04	   Strict Trs: { ap(f(), x) -> ap(f(), app(g(), x)) }
211.30/60.04	   Weak Trs: { ap(ap(g(), x), y) -> y }
211.30/60.04	   Obligation:
211.30/60.04	     derivational complexity
211.30/60.04	   Answer:
211.30/60.04	     MAYBE
211.30/60.04	   
211.30/60.04	   None of the processors succeeded.
211.30/60.04	   
211.30/60.04	   Details of failed attempt(s):
211.30/60.04	   -----------------------------
211.30/60.04	   1) 'empty' failed due to the following reason:
211.30/60.04	      
211.30/60.04	      Empty strict component of the problem is NOT empty.
211.30/60.04	   
211.30/60.04	   2) 'Fastest' failed due to the following reason:
211.30/60.04	      
211.30/60.04	      None of the processors succeeded.
211.30/60.04	      
211.30/60.04	      Details of failed attempt(s):
211.30/60.04	      -----------------------------
211.30/60.04	      1) 'Fastest (timeout of 30 seconds)' failed due to the following
211.30/60.04	         reason:
211.30/60.04	         
211.30/60.04	         Computation stopped due to timeout after 30.0 seconds.
211.30/60.04	      
211.30/60.04	      2) 'Fastest' failed due to the following reason:
211.30/60.04	         
211.30/60.04	         None of the processors succeeded.
211.30/60.04	         
211.30/60.04	         Details of failed attempt(s):
211.30/60.04	         -----------------------------
211.30/60.04	         1) 'matrix interpretation of dimension 6' failed due to the
211.30/60.04	            following reason:
211.30/60.04	            
211.30/60.04	            The input cannot be shown compatible
211.30/60.04	         
211.30/60.04	         2) 'matrix interpretation of dimension 5' failed due to the
211.30/60.04	            following reason:
211.30/60.04	            
211.30/60.04	            The input cannot be shown compatible
211.30/60.04	         
211.30/60.04	         3) 'matrix interpretation of dimension 4' failed due to the
211.30/60.04	            following reason:
211.30/60.04	            
211.30/60.04	            The input cannot be shown compatible
211.30/60.04	         
211.30/60.04	         4) 'matrix interpretation of dimension 3' failed due to the
211.30/60.04	            following reason:
211.30/60.04	            
211.30/60.04	            The input cannot be shown compatible
211.30/60.04	         
211.30/60.04	         5) 'matrix interpretation of dimension 2' failed due to the
211.30/60.04	            following reason:
211.30/60.04	            
211.30/60.04	            The input cannot be shown compatible
211.30/60.04	         
211.30/60.04	         6) 'matrix interpretation of dimension 1' failed due to the
211.30/60.04	            following reason:
211.30/60.04	            
211.30/60.04	            The input cannot be shown compatible
211.30/60.04	         
211.30/60.04	      
211.30/60.04	      3) 'iteProgress' failed due to the following reason:
211.30/60.04	         
211.30/60.04	         Fail
211.30/60.04	      
211.30/60.04	      4) 'bsearch-matrix' failed due to the following reason:
211.30/60.04	         
211.30/60.04	         The input cannot be shown compatible
211.30/60.04	      
211.30/60.04	   
211.30/60.04	
211.30/60.04	3) 'iteProgress (timeout of 297 seconds)' failed due to the
211.30/60.04	   following reason:
211.30/60.04	   
211.30/60.04	   Fail
211.30/60.04	
211.30/60.04	4) 'bsearch-matrix (timeout of 297 seconds)' failed due to the
211.30/60.04	   following reason:
211.30/60.04	   
211.30/60.04	   The input cannot be shown compatible
211.30/60.04	
211.30/60.04	
211.30/60.04	Arrrr..
211.30/60.04	EOF