0.00/0.68	YES
0.00/0.68	
0.00/0.68	Problem:
0.00/0.69	split(x, nil()) -> tp2(nil(), nil())
0.00/0.69	split(x, cons(y, ys)) -> tp2(zs1, cons(y, zs2)) <= split(x, ys) = tp2(zs1, zs2), le(x, y) = true()
0.00/0.69	split(x, cons(y, ys)) -> tp2(cons(y, zs1), zs2) <= split(x, ys) = tp2(zs1, zs2), le(x, y) = false()
0.00/0.69	le(0(), y) -> true()
0.00/0.69	le(s(x), 0()) -> false()
0.00/0.69	le(s(x), s(y)) -> le(x, y)
0.00/0.69	
0.00/0.69	Proof:
0.00/0.69	This system is confluent.
0.00/0.69	By \cite{GNG13}, Theorem 9.
0.00/0.69	This system is of type 3 or smaller.
0.00/0.69	This system is deterministic.
0.00/0.69	This system is weakly left-linear.
0.00/0.69	System R transformed to optimized U(R).
0.00/0.69	This system is orthogonal.
0.00/0.69	
0.00/0.99	EOF