YES

proof:
The input problem is infeasible because

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

	f(f(x, y), x) = x
	f(f(x, y), f(z, w)) = f(f(x, z), f(y, w))
	f(b, a) = f(a, b) ==> true__ = false__
	true__ = false__ ==> \bottom

This holds because

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

E:
	f(f(x, y), f(z, w)) = f(f(x, z), f(y, w))
	f(f(x, y), x) = x
	t1(f(a, b)) = false__
	t1(f(b, a)) = 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:
	f(f(x, y), w) = f(f(x, z), w)
	f(Y2, f(Y1, Y3)) -> f(Y2, Y3)
	f(f(f(Y1, X1), Y3), Y2) -> f(Y1, Y2)
	f(f(x, y), x) -> x
	t1(f(a, b)) -> false__
	t1(f(b, a)) -> true__
	t2(false__) -> true__
	t2(true__) -> false__
with the LPO induced by
	a > b > f > t1 > t2 > false__ > true__