2.27/1.59	YES
2.27/1.59	
2.27/1.59	Proof:
2.27/1.60	This system is confluent.
2.27/1.60	Removed infeasible rules from system R.
2.27/1.60	By \cite{ALS94}, Theorem 4.1.
2.27/1.60	This system is of type 3 or smaller.
2.27/1.60	This system is strongly deterministic.
2.27/1.60	This system is quasi-decreasing.
2.27/1.60	By \cite{A14}, Theorem 11.5.9.
2.27/1.60	This system is of type 3 or smaller.
2.27/1.60	This system is deterministic.
2.27/1.60	System R transformed to V(R) + Emb.
2.27/1.60	This system is terminating.
2.27/1.60	Call external tool:
2.27/1.60	./ttt2.sh
2.27/1.60	Input:
2.27/1.60	(VAR x y)
2.27/1.60	(RULES
2.27/1.60	  h(x, x) -> A
2.27/1.60	  h(x, y) -> x
2.27/1.60	  h(x, y) -> y
2.27/1.60	)
2.27/1.60	
2.27/1.60	 LPO Processor:
2.27/1.60	  precedence:
2.27/1.60	   h > A
2.27/1.60	  problem:
2.27/1.60	   
2.27/1.60	  Qed
2.27/1.60	All 0 critical pairs are joinable.
2.27/1.60	
2.27/1.61	EOF