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