YES weighted path orer with linear polynomial on natural numbers: g_A(x1) = x1 + 1 f_A(x1) = x1 h_A(x1) = x1 precedence: f > h > g status: g: [1] f: [1] h: [1] the condition f(x) ->> f(h(x)) is unsatisfiable for all substitutions.