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