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