2.97/1.69	YES
2.97/1.69	
2.97/1.69	Proof:
2.97/1.69	This system is confluent.
2.97/1.69	Removed infeasible rules from system R.
2.97/1.69	By \cite{ALS94}, Theorem 4.1.
3.33/1.70	This system is of type 3 or smaller.
3.33/1.70	This system is strongly deterministic.
3.33/1.70	This system is quasi-decreasing.
3.33/1.70	By \cite{O02}, p. 214, Proposition 7.2.50.
3.33/1.70	This system is of type 3 or smaller.
3.33/1.70	This system is deterministic.
3.33/1.70	System R transformed to U(R).
3.33/1.70	This system is terminating.
3.33/1.70	Call external tool:
3.33/1.70	./ttt2.sh
3.33/1.70	Input:
3.33/1.70	(VAR n r)
3.33/1.70	(RULES
3.33/1.70	  filter(n, r, nil) -> pair(mo, nil)
3.33/1.70	)
3.33/1.70	
3.33/1.70	 Matrix Interpretation Processor: dim=3
3.33/1.70	  
3.33/1.70	  interpretation:
3.33/1.70	                    [1 0 0]     [1 0 0]     [0]
3.33/1.70	   [pair](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1]
3.33/1.70	                    [0 0 0]     [0 0 0]     [0],
3.33/1.70	   
3.33/1.70	          [0]
3.33/1.70	   [mo] = [0]
3.33/1.70	          [0],
3.33/1.70	   
3.33/1.70	                          [1 0 0]     [1 0 0]     [1 0 0]     [1]
3.33/1.70	   [filter](x0, x1, x2) = [0 0 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [1]
3.33/1.70	                          [0 0 0]     [0 0 0]     [0 0 0]     [0],
3.33/1.70	   
3.33/1.70	           [0]
3.33/1.70	   [nil] = [0]
3.33/1.70	           [0]
3.33/1.70	  orientation:
3.33/1.70	                       [1 0 0]    [1 0 0]    [1]    [0]                   
3.33/1.70	   filter(n,r,nil()) = [0 0 0]n + [0 0 0]r + [1] >= [1] = pair(mo(),nil())
3.33/1.70	                       [0 0 0]    [0 0 0]    [0]    [0]                   
3.33/1.70	  problem:
3.33/1.70	   
3.33/1.70	  Qed
3.33/1.70	All 0 critical pairs are joinable.
3.33/1.70	
3.33/1.72	EOF