4.72/2.12	YES
4.72/2.12	
4.72/2.12	Proof:
4.72/2.12	This system is confluent.
4.72/2.12	By \cite{ALS94}, Theorem 4.1.
4.72/2.12	This system is of type 3 or smaller.
4.72/2.12	This system is strongly deterministic.
4.72/2.12	This system is quasi-decreasing.
4.72/2.12	By \cite{O02}, p. 214, Proposition 7.2.50.
4.72/2.12	This system is of type 3 or smaller.
4.72/2.12	This system is deterministic.
4.72/2.12	System R transformed to optimized U(R).
4.72/2.12	This system is terminating.
4.72/2.12	Call external tool:
4.72/2.12	./ttt2.sh
4.72/2.12	Input:
4.72/2.12	(VAR x)
4.72/2.12	(RULES
4.72/2.12	  e(0) -> true
4.72/2.12	  e(s(x)) -> ?1(e(x), x)
4.72/2.12	  ?1(false, x) -> true
4.72/2.12	  e(s(x)) -> ?1(e(x), x)
4.72/2.12	  ?1(true, x) -> false
4.72/2.12	)
4.72/2.12	
4.72/2.12	 Matrix Interpretation Processor: dim=1
4.72/2.12	  
4.72/2.12	  interpretation:
4.72/2.12	   [false] = 0,
4.72/2.12	   
4.72/2.12	   [?1](x0, x1) = x0 + 4x1,
4.72/2.12	   
4.72/2.12	   [s](x0) = 5x0,
4.72/2.12	   
4.72/2.12	   [true] = 0,
4.72/2.12	   
4.72/2.12	   [e](x0) = x0 + 4,
4.72/2.12	   
4.72/2.12	   [0] = 4
4.72/2.12	  orientation:
4.72/2.12	   e(0()) = 8 >= 0 = true()
4.72/2.12	   
4.72/2.12	   e(s(x)) = 5x + 4 >= 5x + 4 = ?1(e(x),x)
4.72/2.12	   
4.72/2.12	   ?1(false(),x) = 4x >= 0 = true()
4.72/2.12	   
4.72/2.12	   ?1(true(),x) = 4x >= 0 = false()
4.72/2.12	  problem:
4.72/2.12	   e(s(x)) -> ?1(e(x),x)
4.92/2.13	   ?1(false(),x) -> true()
4.92/2.13	   ?1(true(),x) -> false()
4.92/2.13	  Matrix Interpretation Processor: dim=1
4.92/2.13	   
4.92/2.13	   interpretation:
4.92/2.13	    [false] = 2,
4.92/2.13	    
4.92/2.13	    [?1](x0, x1) = x0 + 4x1 + 3,
4.92/2.13	    
4.92/2.13	    [s](x0) = 3x0 + 5,
4.92/2.13	    
4.92/2.13	    [true] = 1,
4.92/2.13	    
4.92/2.13	    [e](x0) = 4x0
4.92/2.13	   orientation:
4.92/2.13	    e(s(x)) = 12x + 20 >= 8x + 3 = ?1(e(x),x)
4.92/2.13	    
4.92/2.13	    ?1(false(),x) = 4x + 5 >= 1 = true()
4.92/2.13	    
4.92/2.13	    ?1(true(),x) = 4x + 4 >= 2 = false()
4.92/2.13	   problem:
4.92/2.13	    
4.92/2.13	   Qed
4.92/2.13	All 2 critical pairs are joinable.
4.92/2.13	Overlap: (rule1: e(s(y)) -> false <= e(y) = true, rule2: e(s(z)) -> true <= e(z) = false, pos: ε, mgu: {(y,z)})
4.92/2.13	CP: true = false <= e(z) = true, e(z) = false
4.92/2.13	This critical pair is unfeasible.
4.92/2.13	Overlap: (rule1: e(s(y)) -> true <= e(y) = false, rule2: e(s(z)) -> false <= e(z) = true, pos: ε, mgu: {(y,z)})
4.92/2.13	CP: false = true <= e(z) = false, e(z) = true
4.92/2.13	This critical pair is unfeasible.
4.92/2.13	
5.01/2.17	EOF