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__