1.27/1.14	YES
1.27/1.14	
1.27/1.14	Proof:
1.27/1.14	This system is confluent.
1.27/1.14	By \cite{ALS94}, Theorem 4.1.
1.27/1.14	This system is of type 3 or smaller.
1.27/1.14	This system is strongly deterministic.
1.27/1.14	This system is quasi-decreasing.
1.27/1.14	By \cite{A14}, Theorem 11.5.9.
1.27/1.14	This system is of type 3 or smaller.
1.27/1.14	This system is deterministic.
1.27/1.14	System R transformed to V(R) + Emb.
1.27/1.14	This system is terminating.
1.27/1.14	Call external tool:
1.27/1.14	./ttt2.sh
1.27/1.14	Input:
1.27/1.14	  f(x, x) -> a
1.27/1.14	  f(x, x) -> g(x)
1.27/1.14	  g(x) -> x
1.27/1.14	  f(x, y) -> x
1.27/1.14	  f(x, y) -> y
1.27/1.14	
1.27/1.14	 Polynomial Interpretation Processor:
1.27/1.14	  dimension: 1
1.27/1.14	  interpretation:
1.27/1.14	   [g](x0) = 4x0 + 2x0x0 + 4,
1.27/1.14	   
1.27/1.14	   [a] = 0,
1.27/1.14	   
1.27/1.14	   [f](x0, x1) = 4x0 + x1 + 2x1x1 + 5
1.27/1.14	  orientation:
1.27/1.14	   f(x,x) = 5x + 2x*x + 5 >= 0 = a()
1.27/1.14	   
1.27/1.14	   f(x,x) = 5x + 2x*x + 5 >= 4x + 2x*x + 4 = g(x)
1.27/1.14	   
1.27/1.14	   g(x) = 4x + 2x*x + 4 >= x = x
1.27/1.14	   
1.27/1.14	   f(x,y) = 4x + y + 2y*y + 5 >= x = x
1.27/1.14	   
1.27/1.14	   f(x,y) = 4x + y + 2y*y + 5 >= y = y
1.27/1.14	  problem:
1.27/1.14	   
1.27/1.14	  Qed
1.27/1.14	All 0 critical pairs are joinable.
1.27/1.14	
1.27/1.17	EOF