YES

TRS:

  and(not(not(x)),y,not(z)) -> and(y,band(x,z),x)

linear polynomial interpretations on N:

  and_A(x1,x2,x3) = 0
  and#_A(x1,x2,x3) = x1 + x2 + x3
  not_A(x1) = x1 + 1
  not#_A(x1) = 0
  band_A(x1,x2) = 1
  band#_A(x1,x2) = x2

precedence:

  and > not = band