YES proof: The input problem is infeasible because [1] the following set of Horn clauses is satisfiable: h(x, x) = g(a) g(g(a)) = f(b) f(a) = g(h(a, b)) G(h(a, b)) = G(g(a)) ==> true__ = false__ true__ = false__ ==> \bottom This holds because [2] the following E does not entail the following G (Claessen-Smallbone's transformation (2018)): E: f(a) = g(h(a, b)) g(g(a)) = f(b) h(x, x) = g(a) t1(G(g(a))) = false__ t1(G(h(a, b))) = true__ 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: g(g(a)) -> f(b) g(h(a, b)) -> f(a) h(x, x) -> g(a) t1(G(g(a))) -> false__ t1(G(h(a, b))) -> true__ t2(false__) -> true__ t2(true__) -> false__ with the LPO induced by t2 > G > t1 > h > g > f > b > a > false__ > true__