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