2.02/1.03	MAYBE
2.02/1.03	
2.02/1.03	Proof:
2.02/1.03	ConCon could not decide confluence of the system.
2.02/1.03	\cite{ALS94}, Theorem 4.1 does not apply.
2.02/1.03	This system is of type 3 or smaller.
2.02/1.03	This system is strongly deterministic.
2.02/1.03	This system is of type 3 or smaller.
2.02/1.03	This system is deterministic.
2.02/1.03	This system is non-terminating.
2.02/1.03	Call external tool:
2.02/1.03	./ttt2.sh
2.02/1.03	Input:
2.02/1.03	  up(x) -> x
2.02/1.03	  down(x) -> x
2.02/1.03	  up(x) -> up(s(x))
2.02/1.03	  down(s(x)) -> down(x)
2.02/1.03	  between(x, y, z) -> true
2.02/1.03	  between(x, y, z) -> down(z)
2.02/1.03	  between(x, y, z) -> up(x)
2.02/1.03	  s(x) -> x
2.02/1.03	  between(x, y, z) -> x
2.02/1.03	  between(x, y, z) -> y
2.02/1.03	  between(x, y, z) -> z
2.02/1.03	  up(x) -> x
2.02/1.03	  down(x) -> x
2.02/1.03	
2.02/1.03	 Containment Processor: loop length: 1
2.02/1.03	                        terms:
2.02/1.03	                         up(x)
2.02/1.04	                        context: []
2.02/1.04	                        substitution:
2.02/1.04	                         x -> s(x)
2.02/1.04	  Qed
2.02/1.04	ConCon could not decide if this system is quasi-decreasing.
2.02/1.04	\cite{A14}, Theorem 11.5.9 does not apply.
2.02/1.04	This system is of type 3 or smaller.
2.02/1.04	This system is deterministic.
2.02/1.04	This system is non-terminating.
2.02/1.04	Call external tool:
2.02/1.04	./ttt2.sh
2.02/1.04	Input:
2.02/1.04	  up(x) -> x
2.02/1.04	  down(x) -> x
2.02/1.04	  up(x) -> up(s(x))
2.02/1.04	  down(s(x)) -> down(x)
2.02/1.04	  between(x, y, z) -> true
2.02/1.04	  between(x, y, z) -> down(z)
2.02/1.04	  between(x, y, z) -> up(x)
2.02/1.04	  s(x) -> x
2.02/1.04	  between(x, y, z) -> x
2.02/1.04	  between(x, y, z) -> y
2.02/1.04	  between(x, y, z) -> z
2.02/1.04	  up(x) -> x
2.02/1.04	  down(x) -> x
2.02/1.04	
2.02/1.04	 Containment Processor: loop length: 1
2.02/1.04	                        terms:
2.02/1.04	                         up(x)
2.02/1.04	                        context: []
2.02/1.04	                        substitution:
2.02/1.04	                         x -> s(x)
2.02/1.04	  Qed
2.02/1.04	
2.02/1.07	EOF