YES

proof:
The input problem is infeasible because

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

	f(f(x, y), z) = f(x, f(y, z))
	f(x, unit) = x
	x = a ==> f(x, x) = unit
	a = f(a, a) ==> 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(a, a) = unit
	f(f(x, y), z) = f(x, f(y, z))
	f(x, unit) = x
	t1(a) = true__
	t1(f(a, a)) = 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:

	f(Y0, f(a, a)) -> Y0
	f(Y0, f(a, f(a, Y2))) -> f(Y0, Y2)
	f(f(x, y), z) -> f(x, f(y, z))
	t1(a) -> true__
	t1(f(a, a)) -> false__
	t2(false__) -> true__
	t2(true__) -> false__
	unit -> f(a, a)
with the LPO induced by
	t1 > unit > a > f > t2 > false__ > true__