3.10/1.64	YES
3.10/1.64	
3.10/1.64	Proof:
3.10/1.64	This system is confluent.
3.10/1.64	Inlined conditions in System R.
3.10/1.64	By \cite{ALS94}, Theorem 4.1.
3.10/1.64	This system is of type 3 or smaller.
3.10/1.64	This system is strongly deterministic.
3.10/1.64	This system is quasi-decreasing.
3.10/1.64	By \cite{O02}, p. 214, Proposition 7.2.50.
3.10/1.64	This system is of type 3 or smaller.
3.10/1.64	This system is deterministic.
3.10/1.64	System R transformed to U(R).
3.10/1.64	This system is terminating.
3.10/1.64	Call external tool:
3.10/1.64	./ttt2.sh
3.10/1.64	Input:
3.10/1.64	(VAR x)
3.10/1.64	(RULES
3.10/1.64	  f(x) -> x
3.10/1.64	  a -> b
3.10/1.64	  b -> c
3.10/1.64	)
3.10/1.64	
3.10/1.64	 Polynomial Interpretation Processor:
3.10/1.64	  dimension: 1
3.10/1.64	  interpretation:
3.10/1.64	   [c] = 0,
3.10/1.64	   
3.10/1.64	   [b] = 4,
3.10/1.64	   
3.10/1.64	   [a] = 5,
3.10/1.64	   
3.10/1.64	   [f](x0) = x0 + 4
3.10/1.64	  orientation:
3.10/1.64	   f(x) = x + 4 >= x = x
3.10/1.64	   
3.10/1.64	   a() = 5 >= 4 = b()
3.10/1.65	   
3.10/1.65	   b() = 4 >= 0 = c()
3.10/1.65	  problem:
3.10/1.65	   
3.10/1.65	  Qed
3.10/1.65	All 0 critical pairs are joinable.
3.10/1.65	
3.10/1.67	EOF