5.09/2.20	YES
5.09/2.20	
5.09/2.20	Proof:
5.09/2.20	This system is confluent.
5.09/2.20	By \cite{ALS94}, Theorem 4.1.
5.09/2.20	This system is of type 3 or smaller.
5.09/2.20	This system is strongly deterministic.
5.09/2.20	This system is quasi-decreasing.
5.09/2.20	By \cite{O02}, p. 214, Proposition 7.2.50.
5.09/2.20	This system is of type 3 or smaller.
5.09/2.20	This system is deterministic.
5.09/2.20	System R transformed to optimized U(R).
5.09/2.20	This system is terminating.
5.09/2.20	Call external tool:
5.09/2.20	./ttt2.sh
5.09/2.20	Input:
5.09/2.20	(VAR x y)
5.09/2.20	(RULES
5.09/2.20	  pin(a) -> pout(b)
5.09/2.20	  pin(b) -> pout(c)
5.09/2.20	  tc(x) -> x
5.09/2.20	  tc(x) -> ?1(pin(x), x)
5.09/2.20	  ?1(pout(z), x) -> ?2(tc(z), x)
5.09/2.20	  ?2(y, x) -> y
5.09/2.20	)
5.09/2.20	
5.09/2.20	 Matrix Interpretation Processor: dim=1
5.09/2.20	  
5.09/2.20	  interpretation:
5.09/2.20	   [?2](x0, x1) = x0 + x1 + 2,
5.09/2.20	   
5.09/2.20	   [z] = 0,
5.09/2.20	   
5.09/2.20	   [?1](x0, x1) = x0 + x1 + 4,
5.09/2.20	   
5.09/2.20	   [tc](x0) = 5x0 + 6,
5.09/2.20	   
5.09/2.20	   [c] = 6,
5.09/2.20	   
5.09/2.20	   [pout](x0) = 3x0 + 4,
5.09/2.20	   
5.09/2.20	   [b] = 5,
5.09/2.20	   
5.09/2.20	   [pin](x0) = 4x0 + 2,
5.09/2.20	   
5.09/2.20	   [a] = 5
5.09/2.20	  orientation:
5.09/2.20	   pin(a()) = 22 >= 19 = pout(b())
5.09/2.20	   
5.09/2.20	   pin(b()) = 22 >= 22 = pout(c())
5.09/2.20	   
5.09/2.20	   tc(x) = 5x + 6 >= x = x
5.09/2.20	   
5.09/2.20	   tc(x) = 5x + 6 >= 5x + 6 = ?1(pin(x),x)
5.09/2.20	   
5.09/2.20	   ?1(pout(z()),x) = x + 8 >= x + 8 = ?2(tc(z()),x)
5.09/2.20	   
5.09/2.20	   ?2(y,x) = x + y + 2 >= y = y
5.09/2.20	  problem:
5.09/2.20	   pin(b()) -> pout(c())
5.09/2.20	   tc(x) -> ?1(pin(x),x)
5.09/2.20	   ?1(pout(z()),x) -> ?2(tc(z()),x)
5.09/2.20	  Matrix Interpretation Processor: dim=1
5.09/2.20	   
5.09/2.20	   interpretation:
5.09/2.20	    [?2](x0, x1) = x0 + 3x1,
5.09/2.20	    
5.09/2.21	    [z] = 0,
5.09/2.21	    
5.09/2.21	    [?1](x0, x1) = 4x0 + 3x1,
5.09/2.21	    
5.09/2.21	    [tc](x0) = 7x0,
5.09/2.21	    
5.09/2.21	    [c] = 0,
5.09/2.21	    
5.09/2.21	    [pout](x0) = 2x0 + 2,
5.09/2.21	    
5.09/2.21	    [b] = 2,
5.09/2.21	    
5.09/2.21	    [pin](x0) = x0
5.09/2.21	   orientation:
5.09/2.21	    pin(b()) = 2 >= 2 = pout(c())
5.09/2.21	    
5.09/2.21	    tc(x) = 7x >= 7x = ?1(pin(x),x)
5.09/2.21	    
5.09/2.21	    ?1(pout(z()),x) = 3x + 8 >= 3x = ?2(tc(z()),x)
5.09/2.21	   problem:
5.09/2.21	    pin(b()) -> pout(c())
5.09/2.21	    tc(x) -> ?1(pin(x),x)
5.09/2.21	   Matrix Interpretation Processor: dim=1
5.09/2.21	    
5.09/2.21	    interpretation:
5.09/2.21	     [?1](x0, x1) = x0 + 5x1,
5.09/2.21	     
5.09/2.21	     [tc](x0) = 6x0 + 1,
5.09/2.21	     
5.09/2.21	     [c] = 4,
5.09/2.21	     
5.09/2.21	     [pout](x0) = x0,
5.09/2.21	     
5.09/2.21	     [b] = 4,
5.09/2.21	     
5.09/2.21	     [pin](x0) = x0
5.09/2.21	    orientation:
5.09/2.21	     pin(b()) = 4 >= 4 = pout(c())
5.09/2.21	     
5.09/2.21	     tc(x) = 6x + 1 >= 6x = ?1(pin(x),x)
5.09/2.21	    problem:
5.09/2.21	     pin(b()) -> pout(c())
5.09/2.21	    Matrix Interpretation Processor: dim=3
5.09/2.21	     
5.09/2.21	     interpretation:
5.09/2.21	            [0]
5.09/2.21	      [c] = [0]
5.09/2.21	            [0],
5.09/2.21	      
5.09/2.21	                   [1 0 0]  
5.09/2.21	      [pout](x0) = [0 0 0]x0
5.09/2.21	                   [0 0 0]  ,
5.09/2.21	      
5.09/2.21	            [0]
5.09/2.21	      [b] = [0]
5.09/2.21	            [0],
5.09/2.21	      
5.09/2.21	                  [1 0 0]     [1]
5.09/2.21	      [pin](x0) = [0 0 0]x0 + [0]
5.09/2.21	                  [0 0 0]     [0]
5.09/2.21	     orientation:
5.09/2.21	                 [1]    [0]            
5.09/2.21	      pin(b()) = [0] >= [0] = pout(c())
5.09/2.21	                 [0]    [0]            
5.09/2.21	     problem:
5.09/2.21	      
5.09/2.21	     Qed
5.09/2.21	All 2 critical pairs are joinable.
5.09/2.21	Overlap: (rule1: tc(x') -> y' <= pin(x') = pout(z), tc(z) = y', rule2: tc(y) -> y, pos: ε, mgu: {(x',y)})
5.09/2.21	CP: y = y' <= pin(y) = pout(z), tc(z) = y'
5.09/2.21	This critical pair is infeasible.
5.09/2.21	This critical pair is conditional.
5.09/2.21	This critical pair has some non-trivial conditions.
5.09/2.21	'\Sigma(pin(y)) \cap (->^*_R)[\Sigma(REN(pout(z)))]' is empty by ETAC.
5.09/2.21	Overlap: (rule1: tc(y) -> y, rule2: tc(x') -> y' <= pin(x') = pout(z), tc(z) = y', pos: ε, mgu: {(y,x')})
5.09/2.21	CP: y' = x' <= pin(x') = pout(z), tc(z) = y'
5.09/2.21	This critical pair is infeasible.
5.09/2.21	This critical pair is conditional.
5.09/2.21	This critical pair has some non-trivial conditions.
5.09/2.21	'\Sigma(pin(x')) \cap (->^*_R)[\Sigma(REN(pout(z)))]' is empty by ETAC.
5.09/2.21	
5.09/2.24	EOF