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