YES linear polynomial interpretations on natural numbers: f_A(x1) = x1 g_A(x1) = 2 a_A = 1 b_A = 0 F_A(x1) = x1 the condition F(a()) ->> F(g(a())) is unsatisfiable for all substitutions.