3.67/1.76	YES
3.67/1.76	
3.67/1.76	Proof:
3.67/1.76	This system is confluent.
3.67/1.76	Removed infeasible rules from system R.
3.67/1.76	By \cite{ALS94}, Theorem 4.1.
3.67/1.76	This system is of type 3 or smaller.
3.67/1.76	This system is strongly deterministic.
3.67/1.76	This system is quasi-decreasing.
3.67/1.76	By \cite{O02}, p. 214, Proposition 7.2.50.
3.67/1.76	This system is of type 3 or smaller.
3.67/1.76	This system is deterministic.
3.67/1.76	System R transformed to optimized U(R).
3.67/1.76	This system is terminating.
3.67/1.76	Call external tool:
3.67/1.76	./ttt2.sh
3.67/1.76	Input:
3.67/1.76	(VAR x)
3.67/1.76	(RULES
3.67/1.76	  h(x, x) -> A
3.67/1.76	)
3.67/1.76	
3.67/1.76	 Polynomial Interpretation Processor:
3.67/1.76	  dimension: 1
3.67/1.76	  interpretation:
3.67/1.76	   [A] = 0,
3.67/1.76	   
3.67/1.76	   [h](x0, x1) = 3x0 + -3x1 + 5x1x1 + 1
3.67/1.76	  orientation:
3.67/1.76	   h(x,x) = 5x*x + 1 >= 0 = A()
3.67/1.76	  problem:
3.67/1.76	   
3.67/1.76	  Qed
3.67/1.76	All 0 critical pairs are joinable.
3.67/1.76	
4.97/2.11	EOF