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