YES

TRS:

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

max/plus interpretations on N:

  and_A(x1,x2,x3) = max{4, 1 + x1, 2 + x2, 3 + x3}
  and#_A(x1,x2,x3) = max{4, 1 + x1, 2 + x2, 3 + x3}
  not_A(x1) = max{4, 2 + x1}
  not#_A(x1) = max{4, 2 + x1}
  band_A(x1,x2) = max{1, 2 + x1, 2 + x2}
  band#_A(x1,x2) = max{1, 2 + x1, 2 + x2}

precedence:

  and > not = band