YES

TRS:

  and(x,or(y,z)) -> or(and(x,y),and(x,z))
  and(x,and(y,y)) -> and(x,y)
  or(or(x,y),and(y,z)) -> or(x,y)
  or(x,and(x,y)) -> x
  or(true(),y) -> true()
  or(x,false()) -> x
  or(x,x) -> x
  or(x,or(y,y)) -> or(x,y)
  and(x,true()) -> x
  and(false(),y) -> false()
  and(x,x) -> x

linear polynomial interpretations on N:

  and_A(x1,x2) = x1 + x2 + 1
  and#_A(x1,x2) = 2
  or_A(x1,x2) = x1 + 1
  or#_A(x1,x2) = 1
  true_A = 1
  true#_A = 0
  false_A = 1
  false#_A = 1

precedence:

  and > or = false > true