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