2.96/1.63	YES
2.96/1.63	
2.96/1.63	Proof:
2.96/1.64	This system is confluent.
2.96/1.64	Removed infeasible rules from system R.
2.96/1.64	By \cite{ALS94}, Theorem 4.1.
2.96/1.64	This system is of type 3 or smaller.
2.96/1.64	This system is strongly deterministic.
2.96/1.64	This system is quasi-decreasing.
2.96/1.64	By \cite{O02}, p. 214, Proposition 7.2.50.
2.96/1.64	This system is of type 3 or smaller.
2.96/1.64	This system is deterministic.
2.96/1.64	System R transformed to optimized U(R).
2.96/1.64	This system is terminating.
2.96/1.64	Call external tool:
2.96/1.64	./ttt2.sh
2.96/1.64	Input:
2.96/1.64	(VAR )
2.96/1.64	(RULES
2.96/1.64	  
2.96/1.64	)
2.96/1.64	
2.96/1.64	 Bounds Processor:
2.96/1.64	  bound: 0
2.96/1.64	  enrichment: match
2.96/1.64	  automaton:
2.96/1.64	   final states: {2}
2.96/1.64	   transitions:
2.96/1.64	    f20() -> 2*
2.96/1.64	  problem:
2.96/1.64	   
2.96/1.64	  Qed
2.96/1.64	All 0 critical pairs are joinable.
2.96/1.64	
2.96/1.72	EOF