YES weighted path orer with linear polynomial on natural numbers: isnoc_A(x1) = x1 + 1 cons_A(x1,x2) = x1 + 4 tp2_A(x1,x2) = 3 nil_A = 1 precedence: tp2 > isnoc > nil > cons status: isnoc: [1] cons: [1] tp2: [] nil: [] the condition isnoc(nil()) ->> tp2(x3,x4) is unsatisfiable for all substitutions.