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 max/plus interpretations on N: and_A(x1,x2) = max{1, 1 + x1, 2} and#_A(x1,x2) = max{1, 2, 5} or_A(x1,x2) = max{2, x1, 2} or#_A(x1,x2) = max{3, 4, 5} true_A = 1 true#_A = 2 false_A = 1 false#_A = 0 precedence: and > or = false > true