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