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
	even(x1) = false & even(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(even(x1), even(x1)) = true__
	t1(false, true) = 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:

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