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