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