YES

proof:
The input problem is infeasible because

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

	isnoc(cons(x, ys)) = tp2(cons(x, xs), y)
	isnoc(cons(y, nil)) = tp2(nil, y)
	isnoc(nil) = tp2(x3, x4) ==> true__ = false__
	true__ = false__ ==> \bottom

This holds because

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

E:
	isnoc(cons(x, ys)) = tp2(cons(x, xs), y)
	isnoc(cons(y, nil)) = tp2(nil, y)
	t1(isnoc(nil)) = true__
	t1(tp2(x3, x4)) = 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:
	isnoc(cons(Y0, X3)) = isnoc(cons(Y0, Y3))
	isnoc(cons(x, ys)) = tp2(cons(x, xs), y)
	t1(isnoc(cons(X0, X3))) -> false__
	t1(isnoc(nil)) -> true__
	t1(tp2(x3, x4)) -> false__
	t2(false__) -> true__
	t2(true__) -> false__
	tp2(nil, y) -> isnoc(cons(y, nil))
with the LPO induced by
	tp2 > cons > isnoc > nil > t2 > t1 > false__ > true__