2.87/1.31	YES
2.87/1.31	
2.87/1.31	Proof:
2.87/1.31	This system is confluent.
2.87/1.31	By \cite{ALS94}, Theorem 4.1.
2.87/1.31	This system is of type 3 or smaller.
2.87/1.31	This system is strongly deterministic.
2.87/1.31	This system is quasi-decreasing.
2.87/1.31	By \cite{O02}, p. 214, Proposition 7.2.50.
2.87/1.31	This system is of type 3 or smaller.
2.87/1.31	This system is deterministic.
2.87/1.31	System R transformed to optimized U(R).
2.87/1.31	This system is terminating.
2.87/1.31	Call external tool:
2.87/1.31	./ttt2.sh
2.87/1.31	Input:
2.87/1.31	  even(0) -> true
2.87/1.31	  even(s(x)) -> ?1(odd(x), x)
2.87/1.31	  ?1(true, x) -> true
2.87/1.31	  odd(s(x)) -> ?2(even(x), x)
2.87/1.31	  ?2(true, x) -> true
2.87/1.31	
2.87/1.31	 Matrix Interpretation Processor: dim=1
2.87/1.31	  
2.87/1.31	  interpretation:
2.87/1.31	   [?2](x0, x1) = 2x0 + 2x1 + 1,
2.87/1.31	   
2.87/1.31	   [?1](x0, x1) = 6x0 + 2x1,
2.87/1.31	   
2.87/1.31	   [odd](x0) = 3x0 + 3,
2.87/1.32	   
2.87/1.32	   [s](x0) = 5x0 + 4,
2.87/1.32	   
2.87/1.32	   [true] = 0,
2.87/1.32	   
2.87/1.32	   [even](x0) = 4x0 + 2,
2.87/1.32	   
2.87/1.32	   [0] = 2
2.87/1.32	  orientation:
2.87/1.32	   even(0()) = 10 >= 0 = true()
2.87/1.32	   
2.87/1.32	   even(s(x)) = 20x + 18 >= 20x + 18 = ?1(odd(x),x)
2.87/1.32	   
2.87/1.32	   ?1(true(),x) = 2x >= 0 = true()
2.87/1.32	   
2.87/1.32	   odd(s(x)) = 15x + 15 >= 10x + 5 = ?2(even(x),x)
2.87/1.32	   
2.87/1.32	   ?2(true(),x) = 2x + 1 >= 0 = true()
2.87/1.32	  problem:
2.87/1.32	   even(s(x)) -> ?1(odd(x),x)
2.87/1.32	   ?1(true(),x) -> true()
2.87/1.32	  Matrix Interpretation Processor: dim=1
2.87/1.32	   
2.87/1.32	   interpretation:
2.87/1.32	    [?1](x0, x1) = x0 + 4x1 + 4,
2.87/1.32	    
2.87/1.32	    [odd](x0) = x0,
2.87/1.32	    
2.87/1.32	    [s](x0) = x0 + 4,
2.87/1.32	    
2.87/1.32	    [true] = 0,
2.87/1.32	    
2.87/1.32	    [even](x0) = 5x0 + 4
2.87/1.32	   orientation:
2.87/1.32	    even(s(x)) = 5x + 24 >= 5x + 4 = ?1(odd(x),x)
2.87/1.32	    
2.87/1.32	    ?1(true(),x) = 4x + 4 >= 0 = true()
2.87/1.32	   problem:
2.87/1.32	    
2.87/1.32	   Qed
2.87/1.32	All 0 critical pairs are joinable.
2.87/1.32	
3.18/1.35	EOF