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