YES proof: The input problem is infeasible because [1] the following set of Horn clauses is satisfiable: e(x) = true ==> e(s(x)) = false e(x) = false ==> e(s(x)) = true e(0) = true e(x1) = false & e(x1) = true ==> true__ = false__ true__ = false__ ==> \bottom This holds because [2] the following E does not entail the following G (Claessen-Smallbone's transformation (2018)): E: e(0) = true g1(e(x), x) = e(s(x)) g1(false, x) = true g1(true, x) = false t1(e(x1), e(x1)) = true__ t1(false, true) = 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: e(0) -> true e(s(X0)) -> g1(e(X0), X0) g1(false, X0) -> true g1(g2, X0) -> true g1(true, X0) -> false g2 -> false t1(Z1, Z1) -> true__ t1(false, true) -> false__ t1(g1(Z1, X0), g1(Z1, X0)) -> true__ t1(g1(g1(Z1, X0), s(X0)), g1(g1(Z1, X0), s(X0))) -> true__ t1(g2, e(0)) -> false__ t1(g2, g2) -> true__ t2(false__) -> true__ t2(true__) -> false__ with the LPO induced by g2 > e > g1 > t2 > false > true > 0 > s > t1 > true__ > false__