YES

proof:
The input problem is infeasible because

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

	even(x) = true ==> odd(s(x)) = true
	even(x) = false ==> odd(s(x)) = false
	odd(0) = false
	odd(x) = true ==> even(s(x)) = true
	odd(x) = false ==> even(s(x)) = false
	even(0) = true
	odd(x1) = false & odd(x1) = true ==> true__ = false__
	true__ = false__ ==> \bottom

This holds because

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

E:
	even(0) = true
	g1(even(x), x) = odd(s(x))
	g1(false, x) = false
	g1(true, x) = true
	g2(false, x) = false
	g2(odd(x), x) = even(s(x))
	g2(true, x) = true
	odd(0) = false
	t1(false, true) = false__
	t1(odd(x1), odd(x1)) = true__
	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:

	even(0) -> true
	even(s(X0)) -> g2(odd(X0), X0)
	false -> odd(0)
	g1(odd(0), X0) -> odd(0)
	g1(true, X0) -> true
	g2(odd(0), X0) -> odd(0)
	g2(true, X0) -> true
	odd(s(X0)) -> g1(even(X0), X0)
	t1(Z1, Z1) -> true__
	t1(g1(Z1, X0), g1(Z1, X0)) -> true__
	t1(odd(0), true) -> false__
	t1(true, true) -> true__
	t2(false__) -> true__
	t2(true__) -> false__
with the LPO induced by
	t1 > s > false > odd > g1 > even > g2 > true > 0 > t2 > false__ > true__