YES

proof:
The input problem is infeasible because

[1] the following set of Horn clauses is satisfiable:

	le(s(x), s(y)) = le(x, y)
	le(s(x), 0) = false
	le(0, y) = true
	split(x, cons(y, ys)) = tp2(cons(y, zs1), zs2)
	split(x, cons(y, ys)) = tp2(zs1, cons(y, zs2))
	split(x, nil) = tp2(nil, nil)
	split(x1, x3) = tp2(zs1, zs2) & le(x1, x2) = true & split(x1, x3) = tp2(x4, x5) & le(x1, x2) = false ==> true__ = false__
	true__ = false__ ==> \bottom

This holds because

[2] the following E does not entail the following G (Claessen-Smallbone's transformation (2018)):

E:
	le(0, y) = true
	le(s(x), 0) = false
	le(s(x), s(y)) = le(x, y)
	split(x, cons(y, ys)) = tp2(cons(y, zs1), zs2)
	split(x, cons(y, ys)) = tp2(zs1, cons(y, zs2))
	split(x, nil) = tp2(nil, nil)
	t1(split(x1, x3), le(x1, x2), split(x1, x3), le(x1, x2), zs1, zs2, x4, x5) = true__
	t1(tp2(zs1, zs2), true, tp2(x4, x5), false, zs1, zs2, x4, x5) = false__
	t2(false__) = true__
	t2(true__) = false__
G:
	true__ = false__

This holds because

[3] the following ground-complete ordered TRS entails E but does not entail G:

	le(0, X0) -> true
	le(s(X0), 0) -> false
	le(s(X0), s(X1)) -> le(X0, X1)
	split(X0, cons(X1, X2)) -> g1
	split(X0, nil) -> tp2(nil, nil)
	t1(Z1, Z2, Z1, Z2, X3, X4, X5, X6) -> true__
	t1(Z1, false, Z1, false, X2, X3, X4, X5) -> true__
	t1(Z1, true, Z1, true, X1, X2, X3, X4) -> true__
	t1(Z1, true, Z2, false, X0, X1, X2, X3) -> false__
	t1(Z1, true, g1, false, X0, X1, true__, cons(X2, true__)) -> false__
	t1(g1, true, Z1, false, true__, cons(X2, true__), X0, X1) -> false__
	t1(tp2(nil, nil), Z1, tp2(nil, nil), Z1, X2, X3, X4, X5) -> true__
	t1(tp2(nil, nil), true, tp2(nil, nil), true, X0, X1, X2, X3) -> true__
	t2(false__) -> true__
	t2(true__) -> false__
	tp2(X0, cons(X1, X2)) -> g1
	tp2(cons(X0, X1), X2) -> g1
with the LPO induced by
	cons > g1 > split > tp2 > t1 > nil > s > false > 0 > true > le > t2 > false__ > true__