3.22/1.72	YES
3.22/1.72	
3.22/1.72	Proof:
3.22/1.72	This system is confluent.
3.22/1.72	By \cite{ALS94}, Theorem 4.1.
3.22/1.72	This system is of type 3 or smaller.
3.22/1.72	This system is strongly deterministic.
3.22/1.72	This system is quasi-decreasing.
3.22/1.72	By \cite{O02}, p. 214, Proposition 7.2.50.
3.22/1.72	This system is of type 3 or smaller.
3.22/1.72	This system is deterministic.
3.22/1.72	System R transformed to U(R).
3.22/1.72	This system is terminating.
3.22/1.72	Call external tool:
3.22/1.72	./ttt2.sh
3.22/1.72	Input:
3.22/1.72	(VAR x y)
3.22/1.72	(RULES
3.22/1.72	  ?1(a, x) -> x
3.22/1.72	  f(x) -> ?1(x, x)
3.22/1.72	  g(x) -> h(x, x)
3.22/1.72	  h(x, y) -> i(x)
3.22/1.72	)
3.22/1.72	
3.22/1.72	 Polynomial Interpretation Processor:
3.22/1.72	  dimension: 1
3.22/1.72	  interpretation:
3.22/1.72	   [i](x0) = x0x0,
3.22/1.72	   
3.22/1.72	   [h](x0, x1) = x0x0 + 2x1x1 + 1,
3.22/1.72	   
3.22/1.72	   [g](x0) = 6x0x0 + 2,
3.22/1.72	   
3.22/1.72	   [f](x0) = 4x0 + 6x0x0 + 4,
3.22/1.72	   
3.22/1.72	   [?1](x0, x1) = 4x1 + x0x0 + 2,
3.22/1.72	   
3.22/1.72	   [a] = 0
3.22/1.72	  orientation:
3.22/1.72	   ?1(a(),x) = 4x + 2 >= x = x
3.22/1.72	   
3.22/1.72	   f(x) = 4x + 6x*x + 4 >= 4x + x*x + 2 = ?1(x,x)
3.22/1.72	   
3.22/1.72	   g(x) = 6x*x + 2 >= 3x*x + 1 = h(x,x)
3.22/1.72	   
3.22/1.72	   h(x,y) = x*x + 2y*y + 1 >= x*x = i(x)
3.22/1.72	  problem:
3.22/1.72	   
3.22/1.72	  Qed
3.22/1.72	All 0 critical pairs are joinable.
3.22/1.72	
3.26/1.75	EOF