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