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