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