53.25/14.43	MAYBE
53.25/14.43	
53.25/14.43	Problem:
53.25/14.43	lt(x, 0()) -> false()
53.25/14.43	lt(0(), s(y)) -> true()
53.25/14.43	lt(s(x), s(y)) -> lt(x, y)
53.25/14.43	cons(x, cons(y, ys)) -> cons(y, cons(x, ys)) <= lt(x, y) = true()
53.25/14.43	
53.25/14.43	Proof:
53.25/14.43	ConCon could not decide confluence of the system.
53.25/14.43	\cite{ALS94}, Theorem 4.1 does not apply.
53.25/14.43	ConCon could not decide whether all 1 critical pairs are joinable or not.
53.25/14.43	CP: cons(x, cons(y, cons(y', z'))) = cons(y', cons(x, cons(y, z'))) <= lt(x, y') = true(), lt(y', y) = true():
53.25/14.43	ConCon could not decide infeasibility of this critical pair.
53.25/14.43	ConCon could not decide if this system is quasi-decreasing.
53.25/14.43	\cite{O02}, p. 214, Proposition 7.2.50 does not apply.
53.25/14.43	System R transformed to optimized U(R).
53.25/14.43	The external tool could not decide termination of the system.
53.25/14.43	Call external tool:
53.25/14.43	./ttt2.sh
53.25/14.43	Input:
53.25/14.43	  lt(x, 0()) -> false()
53.25/14.43	  lt(0(), s(y)) -> true()
53.25/14.43	  lt(s(x), s(y)) -> lt(x, y)
53.25/14.43	  ?1(true(), x, y, ys) -> cons(y, cons(x, ys))
53.25/14.43	  cons(x, cons(y, ys)) -> ?1(lt(x, y), x, y, ys)
53.25/14.43	
53.25/14.43	
53.25/14.45	EOF