YES linear polynomial interpretations on natural numbers: -_A(x1,x2) = x1 s_A(x1) = x1 + 1 0_A = 0 the condition -(x,x) ->> s(x) is unsatisfiable for all substitutions.