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