YES TRS: not(x) -> if(x,false(),true()) and(x,y) -> if(x,y,false()) or(x,y) -> if(x,true(),y) implies(x,y) -> if(x,y,true()) =(x,x) -> true() =(x,y) -> if(x,y,not(y)) if(true(),x,y) -> x if(false(),x,y) -> y if(x,x,if(x,false(),true())) -> true() =(x,y) -> if(x,y,if(y,false(),true())) max/plus interpretations on N: not_A(x1) = max{0, x1} not#_A(x1) = max{0, x1} if_A(x1,x2,x3) = max{0, x1, x2, x3} if#_A(x1,x2,x3) = max{0, x1, x2, x3} false_A = 0 false#_A = 0 true_A = 0 true#_A = 0 and_A(x1,x2) = max{0, x1, x2} and#_A(x1,x2) = max{0, x1, x2} or_A(x1,x2) = max{0, x1, x2} or#_A(x1,x2) = max{0, x1, x2} implies_A(x1,x2) = max{0, x1, x2} implies#_A(x1,x2) = max{0, x1, x2} =_A(x1,x2) = max{0, x1, x2} =#_A(x1,x2) = max{0, x1, x2} precedence: = > not = and = or = implies > if = false > true