YES TRS: or(x,x) -> x and(x,x) -> x not(not(x)) -> x not(and(x,y)) -> or(not(x),not(y)) not(or(x,y)) -> and(not(x),not(y)) max/plus interpretations on N: or_A(x1,x2) = max{10, 4 + x1, 8 + x2} or#_A(x1,x2) = max{0, 2, -6} and_A(x1,x2) = max{3, 4 + x1, 8 + x2} and#_A(x1,x2) = max{4, 4, 4} not_A(x1) = max{2, 2 + x1} not#_A(x1) = max{1, -5 + x1} precedence: and > not > or