YES

proof:
The input problem is infeasible because

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

	min(xs) = y & le(x, y) = false ==> min(cons(x, xs)) = y
	min(xs) = y & le(x, y) = true ==> min(cons(x, xs)) = x
	min(cons(x, nil)) = x
	le(s(x), s(y)) = le(x, y)
	le(0, s(y)) = true
	le(x, 0) = false
	min(x2) = y & le(x1, y) = true & min(x2) = x3 & le(x1, x3) = 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:
	g1(false, x, xs) = min(xs)
	g1(le(x, min(xs)), x, xs) = min(cons(x, xs))
	g1(true, x, xs) = x
	le(0, s(y)) = true
	le(s(x), s(y)) = le(x, y)
	le(x, 0) = false
	min(cons(x, nil)) = x
	t1(le(x1, min(x2)), le(x1, min(x2))) = true__
	t1(true, false) = 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:

	g1(false, X0, X1) -> min(X1)
	g1(le(X0, min(nil)), X0, nil) -> X0
	g1(true, X0, X1) -> X0
	le(0, s(X0)) -> true
	le(X0, 0) -> false
	le(s(X0), s(X1)) -> le(X0, X1)
	min(cons(X0, X1)) -> g1(le(X0, min(X1)), X0, X1)
	t1(Z1, Z1) -> true__
	t1(false, false) -> true__
	t1(true, false) -> false__
	t2(false__) -> true__
	t2(true__) -> false__
with the LPO induced by
	0 > true > cons > le > nil > false > g1 > min > s > t2 > t1 > false__ > true__