YES

proof:
The input problem is infeasible because

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

	ring(st_1, in_2, st_2, in_3, st_3, m) = ring(st_1, in_2, st_2, tail(in_3), st_3, m)
	ring(st_1, in_2, st_2, in_3, st_3, m) = ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
	ring(st_1, in_2, st_2, in_3, st_3, m) = ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
	ring(st_1, in_2, st_2, in_3, st_3, m) = ring(st_1, tail(in_2), st_2, in_3, st_3, m)
	ring(st_1, in_2, st_2, in_3, st_3, m) = ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
	ring(st_1, in_2, st_2, in_3, st_3, m) = ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
	ring(st_1, in_2, st_2, in_3, st_3, m) = ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
	tail(cons(h, t)) = t
	head(cons(h, t)) = h
	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(x6, length(x3)) = true & empty(fstsplit(x6, x3)) = false & leq(x6, length(x3)) = false & empty(fstsplit(x6, app(map_f(two, head(x2)), x3))) = 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
	head(cons(h, t)) = h
	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(x6, length(x3)), empty(fstsplit(x6, x3)), leq(x6, length(x3)), empty(fstsplit(x6, app(map_f(two, head(x2)), x3)))) = true__
	t1(true, false, false, false) = false__
	t2(false__) = true__
	t2(true__) = false__
	tail(cons(h, t)) = t
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(f(X0, X1), map_f(X0, X2)) -> map_f(X0, cons(X1, X2))
	app(f(Y0, Y1), nil) -> map_f(Y0, cons(Y1, nil))
	app(nil, X0) -> X0
	empty(cons(X0, X1)) -> false
	fstsplit(length(nil), Y0) -> nil
	fstsplit(s(X0), cons(X1, X2)) -> cons(X1, fstsplit(X0, X2))
	fstsplit(s(X0), nil) -> nil
	head(cons(X0, X1)) -> X0
	length(cons(X0, X1)) -> s(length(X1))
	leq(length(nil), Y0) -> empty(nil)
	leq(s(X0), s(X1)) -> leq(X0, X1)
	leq(s(Y0), length(nil)) -> false
	map_f(X0, nil) -> nil
	sndsplit(length(nil), Y0) -> Y0
	sndsplit(s(X0), cons(X1, X2)) -> sndsplit(X0, X2)
	sndsplit(s(X0), nil) -> nil
	t1(Y0, empty(fstsplit(Y1, Y2)), Y0, empty(fstsplit(Y1, Y2))) -> true__
	t1(Y0, empty(fstsplit(Y1, Y2)), Y0, empty(fstsplit(Y1, app(map_f(two, X0), Y2)))) -> true__
	t1(Y0, empty(nil), Y0, empty(fstsplit(s(Y1), app(map_f(two, X0), nil)))) -> true__
	t1(Y0, empty(nil), Y0, empty(nil)) -> true__
	t1(Y0, false, Y0, empty(fstsplit(s(X0), app(map_f(two, Y3), cons(X1, X2))))) -> true__
	t1(Y0, false, Y0, false) -> true__
	t1(empty(nil), false, false, false) -> false__
	t2(false__) -> true__
	t2(true__) -> false__
	tail(cons(X0, X1)) -> X1
	true -> empty(nil)
with the LPO induced by
	two > leq > app > tail > fstsplit > sndsplit > true > empty > false > t1 > f > cons > s > head > map_f > 0 > length > nil > t2 > false__ > true__