5.77/2.32	YES
5.77/2.32	
5.77/2.32	Proof:
5.77/2.32	This system is confluent.
5.77/2.32	By \cite{SMI95}, Corollary 4.7 or 5.3.
5.77/2.32	This system is oriented.
5.77/2.32	This system is of type 3 or smaller.
5.77/2.32	This system is right-stable.
5.77/2.33	This system is properly oriented.
5.77/2.33	This is an overlay system.
5.77/2.33	This system is left-linear.
5.77/2.33	All 2 critical pairs are trivial or infeasible.
5.77/2.33	Overlap: (rule1: pos(s(y)) -> true <= pos(y) = true, rule2: pos(s(0)) -> true, pos: ε, mgu: {(y,0)})
5.77/2.33	CP: true = true <= pos(0) = true
5.77/2.33	This critical pair is trivial.
5.77/2.33	Overlap: (rule1: pos(s(0)) -> true, rule2: pos(s(y)) -> true <= pos(y) = true, pos: ε, mgu: {(y,0)})
5.77/2.33	CP: true = true <= pos(0) = true
5.77/2.33	This critical pair is infeasible.
5.77/2.33	This critical pair is conditional.
5.77/2.33	This critical pair has some non-trivial conditions.
5.77/2.33	Call external tool:
5.77/2.33	./waldmeister
5.77/2.33	Input:
5.77/2.33	  pos(s(0)) -> true
5.77/2.33	  pos(0) -> false
5.77/2.33	  pos(s(x)) -> true <= pos(x) = true
5.77/2.33	  pos(p(x)) -> false <= pos(x) = false
5.77/2.33	
5.77/2.33	By Waldmeister.
5.77/2.33	
6.27/2.37	EOF