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