YES

proof:
The input problem is infeasible because

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

	pos(p(x)) = false
	pos(s(x)) = true
	pos(0) = false
	pos(s(0)) = true
	pos(0) = 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:
	pos(0) = false
	pos(p(x)) = false
	pos(s(0)) = true
	pos(s(x)) = true
	t1(pos(0)) = true__
	t1(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:

	false -> pos(0)
	pos(p(x)) -> pos(0)
	pos(s(x)) -> true
	t1(pos(0)) -> true__
	t1(true) -> false__
	t2(false__) -> true__
	t2(true__) -> false__
with the LPO induced by
	t2 > t1 > p > false > 0 > s > true > pos > false__ > true__