9.15/8.30	MAYBE
9.15/8.30	
9.15/8.30	Problem:
9.15/8.30	up(x) -> x
9.15/8.30	down(x) -> x
9.15/8.30	up(x) -> up(s(x))
9.15/8.30	down(s(x)) -> down(x)
9.15/8.31	between(x, y, z) -> true() <= up(x) = y, down(z) = y
9.15/8.31	
9.15/8.31	Proof:
9.15/8.31	ConCon could not decide confluence of the system.
9.15/8.31	\cite{ALS94}, Theorem 4.1 does not apply.
9.15/8.31	ConCon could not decide whether all 4 critical pairs are joinable or not.
9.15/8.31	CP: x = up(s(x)):
9.15/8.31	
9.15/8.32	EOF