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