5.41/2.01	MAYBE
5.41/2.01	
5.41/2.01	Problem:
5.41/2.01	s(p(x)) -> x
5.41/2.01	p(s(x)) -> x
5.41/2.01	pos(0()) -> false()
5.41/2.01	pos(s(0())) -> true()
5.41/2.01	pos(s(x)) -> true() <= pos(x) = true()
5.41/2.01	pos(p(x)) -> false() <= pos(x) = false()
5.41/2.01	
5.41/2.01	Proof:
5.41/2.01	ConCon could not decide confluence of the system.
5.41/2.01	\cite{ALS94}, Theorem 4.1 does not apply.
5.41/2.01	ConCon could not decide whether all 6 critical pairs are joinable or not.
5.41/2.01	CP: pos(x) = false() <= pos(s(x)) = false():
5.41/2.01	ConCon could not decide infeasibility of this critical pair.
5.41/2.01	
5.41/2.04	EOF