116.06/30.17	MAYBE
116.06/30.17	
116.06/30.17	Proof:
116.06/30.17	ConCon could not decide confluence of the system.
116.06/30.17	\cite{ALS94}, Theorem 4.1 does not apply.
116.06/30.17	This system is of type 3 or smaller.
116.06/30.17	This system is strongly deterministic.
116.06/30.17	This system is of type 3 or smaller.
116.06/30.17	This system is deterministic.
116.06/30.17	ConCon could not decide if this system is quasi-decreasing.
116.06/30.17	\cite{O02}, p. 214, Proposition 7.2.50 does not apply.
116.06/30.17	This system is of type 3 or smaller.
116.06/30.17	This system is deterministic.
116.06/30.17	System R transformed to U(R).
116.06/30.17	The external tool could not decide termination of the system.
116.06/30.17	Call external tool:
116.06/30.17	./ttt2.sh
116.06/30.17	Input:
116.06/30.17	  lt(x, 0) -> false
116.06/30.17	  lt(0, s(y)) -> true
116.06/30.17	  lt(s(x), s(y)) -> lt(x, y)
116.06/30.17	  ?1(true, x, y, ys) -> cons(y, cons(x, ys))
116.06/30.17	  cons(x, cons(y, ys)) -> ?1(lt(x, y), x, y, ys)
116.06/30.17	
116.06/30.17	
116.06/30.19	EOF