YES linear polynomial interpretations on natural numbers: c_A = 0 g_A(x1,x2) = 0 a_A = 1 d_A = 0 f_A(x1,x2) = x1 b_A = 2 the condition f(a(),b()) ->> b() is unsatisfiable for all substitutions.