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