YES

proof:
The input problem is infeasible because

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

	process(store, m) = process(sndsplit(m, app(map_f(self, nil), store)), m)
	process(store, m) = process(app(map_f(self, nil), sndsplit(m, store)), m)
	map_f(pid, cons(h, t)) = app(f(pid, h), map_f(pid, t))
	map_f(pid, nil) = nil
	app(cons(h, t), x) = cons(h, app(t, x))
	app(nil, x) = x
	length(cons(h, t)) = s(length(t))
	length(nil) = 0
	leq(s(n), s(m)) = leq(n, m)
	leq(s(n), 0) = false
	leq(0, m) = true
	empty(cons(h, t)) = false
	empty(nil) = true
	sndsplit(s(n), cons(h, t)) = sndsplit(n, t)
	sndsplit(s(n), nil) = nil
	sndsplit(0, x) = x
	fstsplit(s(n), cons(h, t)) = cons(h, fstsplit(n, t))
	fstsplit(s(n), nil) = nil
	fstsplit(0, x) = nil
	leq(x2, length(x1)) = true & empty(fstsplit(x2, x1)) = false & leq(x2, length(x1)) = false & empty(fstsplit(x2, app(map_f(self, nil), x1))) = false ==> true__ = false__
	true__ = false__ ==> \bottom

This holds because

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

E:
	app(cons(h, t), x) = cons(h, app(t, x))
	app(nil, x) = x
	empty(cons(h, t)) = false
	empty(nil) = true
	fstsplit(0, x) = nil
	fstsplit(s(n), cons(h, t)) = cons(h, fstsplit(n, t))
	fstsplit(s(n), nil) = nil
	length(cons(h, t)) = s(length(t))
	length(nil) = 0
	leq(0, m) = true
	leq(s(n), 0) = false
	leq(s(n), s(m)) = leq(n, m)
	map_f(pid, cons(h, t)) = app(f(pid, h), map_f(pid, t))
	map_f(pid, nil) = nil
	sndsplit(0, x) = x
	sndsplit(s(n), cons(h, t)) = sndsplit(n, t)
	sndsplit(s(n), nil) = nil
	t1(leq(x2, length(x1)), empty(fstsplit(x2, x1)), leq(x2, length(x1)), empty(fstsplit(x2, app(map_f(self, nil), x1)))) = true__
	t1(true, false, false, false) = 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:

	0 -> length(nil)
	app(cons(X0, X1), X2) -> cons(X0, app(X1, X2))
	app(nil, X0) -> X0
	empty(cons(X0, X1)) -> false
	fstsplit(length(nil), X0) -> nil
	fstsplit(s(X0), cons(X1, X2)) -> cons(X1, fstsplit(X0, X2))
	fstsplit(s(X0), nil) -> nil
	length(cons(X0, X1)) -> s(length(X1))
	leq(length(nil), X0) -> empty(nil)
	leq(s(X0), length(nil)) -> false
	leq(s(X0), s(X1)) -> leq(X0, X1)
	map_f(X0, cons(X1, X2)) -> app(f(X0, X1), map_f(X0, X2))
	map_f(X0, nil) -> nil
	sndsplit(length(nil), X0) -> X0
	sndsplit(s(X0), cons(X1, X2)) -> sndsplit(X0, X2)
	sndsplit(s(X0), nil) -> nil
	t1(Z1, empty(Z3), Z1, empty(Z3)) -> true__
	t1(Z1, false, Z1, false) -> true__
	t1(empty(nil), empty(nil), empty(nil), empty(nil)) -> true__
	t1(empty(nil), false, empty(nil), false) -> true__
	t1(empty(nil), false, false, false) -> false__
	t1(false, empty(nil), false, empty(nil)) -> true__
	t1(false, false, false, false) -> true__
	t2(false__) -> true__
	t2(true__) -> false__
	true -> empty(nil)
with the LPO induced by
	self > map_f > f > t1 > app > 0 > length > s > true > empty > nil > fstsplit > cons > false > t2 > sndsplit > leq > false__ > true__