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