5.00/2.12	YES
5.00/2.12	
5.00/2.12	Proof:
5.00/2.12	This system is confluent.
5.00/2.12	By \cite{ALS94}, Theorem 4.1.
5.00/2.12	This system is of type 3 or smaller.
5.00/2.12	This system is strongly deterministic.
5.00/2.12	This system is quasi-decreasing.
5.00/2.12	By \cite{O02}, p. 214, Proposition 7.2.50.
5.00/2.12	This system is of type 3 or smaller.
5.00/2.12	This system is deterministic.
5.00/2.12	System R transformed to U(R).
5.00/2.12	This system is terminating.
5.00/2.12	Call external tool:
5.00/2.12	./ttt2.sh
5.00/2.12	Input:
5.00/2.12	(VAR z x y)
5.00/2.12	(RULES
5.00/2.12	  ?2(i(z), x, y) -> g(x, y, z)
5.00/2.12	  ?1(i(y), x) -> ?2(h(a, y), x, y)
5.00/2.12	  f(x) -> ?1(h(a, x), x)
5.00/2.12	  h(a, a) -> i(b)
5.00/2.12	  h(a, b) -> i(c)
5.00/2.12	  h(b, b) -> i(d)
5.00/2.12	)
5.00/2.12	
5.00/2.12	 Matrix Interpretation Processor: dim=1
5.00/2.12	  
5.00/2.12	  interpretation:
5.00/2.12	   [d] = 0,
5.00/2.12	   
5.00/2.12	   [c] = 0,
5.00/2.12	   
5.00/2.12	   [b] = 0,
5.00/2.12	   
5.00/2.12	   [f](x0) = 5x0 + 6,
5.00/2.12	   
5.00/2.12	   [h](x0, x1) = 2x0 + x1,
5.00/2.12	   
5.00/2.12	   [a] = 0,
5.00/2.12	   
5.00/2.12	   [?1](x0, x1) = 4x0 + x1 + 4,
5.00/2.12	   
5.00/2.12	   [g](x0, x1, x2) = x0 + x1 + 4x2,
5.00/2.12	   
5.00/2.12	   [?2](x0, x1, x2) = 2x0 + x1 + 2x2,
5.00/2.12	   
5.00/2.14	   [i](x0) = 4x0
5.00/2.14	  orientation:
5.00/2.14	   ?2(i(z),x,y) = x + 2y + 8z >= x + y + 4z = g(x,y,z)
5.00/2.14	   
5.00/2.14	   ?1(i(y),x) = x + 16y + 4 >= x + 4y = ?2(h(a(),y),x,y)
5.00/2.14	   
5.00/2.14	   f(x) = 5x + 6 >= 5x + 4 = ?1(h(a(),x),x)
5.00/2.14	   
5.00/2.14	   h(a(),a()) = 0 >= 0 = i(b())
5.00/2.14	   
5.00/2.14	   h(a(),b()) = 0 >= 0 = i(c())
5.00/2.14	   
5.00/2.14	   h(b(),b()) = 0 >= 0 = i(d())
5.00/2.14	  problem:
5.00/2.14	   ?2(i(z),x,y) -> g(x,y,z)
5.00/2.14	   h(a(),a()) -> i(b())
5.00/2.14	   h(a(),b()) -> i(c())
5.00/2.14	   h(b(),b()) -> i(d())
5.00/2.14	  Matrix Interpretation Processor: dim=3
5.00/2.14	   
5.00/2.14	   interpretation:
5.00/2.14	          [0]
5.00/2.14	    [d] = [0]
5.00/2.14	          [0],
5.00/2.14	    
5.00/2.14	          [0]
5.00/2.14	    [c] = [0]
5.00/2.14	          [0],
5.00/2.14	    
5.00/2.14	          [0]
5.00/2.14	    [b] = [0]
5.00/2.14	          [1],
5.00/2.14	    
5.00/2.14	                  [1 0 0]     [1 0 0]     [1]
5.00/2.14	    [h](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
5.00/2.14	                  [0 0 0]     [0 1 0]     [0],
5.00/2.14	    
5.00/2.14	          [0]
5.00/2.14	    [a] = [1]
5.00/2.14	          [0],
5.00/2.14	    
5.00/2.14	                      [1 0 0]     [1 0 0]     [1 0 0]  
5.00/2.14	    [g](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2
5.00/2.14	                      [0 0 0]     [0 0 0]     [0 0 0]  ,
5.00/2.14	    
5.00/2.14	                       [1 0 0]     [1 0 0]     [1 0 0]     [1]
5.00/2.14	    [?2](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [0]
5.00/2.14	                       [0 0 0]     [0 0 0]     [0 0 0]     [0],
5.00/2.14	    
5.00/2.14	              [1 0 0]  
5.00/2.14	    [i](x0) = [0 0 0]x0
5.00/2.14	              [0 0 1]  
5.00/2.14	   orientation:
5.00/2.14	                   [1 0 0]    [1 0 0]    [1 0 0]    [1]    [1 0 0]    [1 0 0]    [1 0 0]            
5.00/2.14	    ?2(i(z),x,y) = [0 0 0]x + [0 0 0]y + [0 0 0]z + [0] >= [0 0 0]x + [0 0 0]y + [0 0 0]z = g(x,y,z)
5.00/2.14	                   [0 0 0]    [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0 0 0]            
5.00/2.14	    
5.00/2.14	                 [1]    [0]         
5.00/2.14	    h(a(),a()) = [0] >= [0] = i(b())
5.00/2.14	                 [1]    [1]         
5.00/2.14	    
5.00/2.14	                 [1]    [0]         
5.00/2.14	    h(a(),b()) = [0] >= [0] = i(c())
5.00/2.14	                 [0]    [0]         
5.00/2.14	    
5.00/2.14	                 [1]    [0]         
5.00/2.14	    h(b(),b()) = [0] >= [0] = i(d())
5.00/2.14	                 [0]    [0]         
5.00/2.14	   problem:
5.00/2.14	    
5.00/2.14	   Qed
5.00/2.14	All 0 critical pairs are joinable.
5.00/2.14	
5.37/2.25	EOF