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{7, 1 + x1} not#_A(x1) = max{7, 1 + x1} if_A(x1,x2,x3) = max{7, x1, 2 + x2, 2 + x3} if#_A(x1,x2,x3) = max{7, x1, 2 + x2, 2 + x3} false_A = 5 false#_A = 5 true_A = 5 true#_A = 5 and_A(x1,x2) = max{7, 1 + x1, 3 + x2} and#_A(x1,x2) = max{7, 1 + x1, 3 + x2} or_A(x1,x2) = max{6, 4 + x1, 7 + x2} or#_A(x1,x2) = max{6, 4 + x1, 7 + x2} implies_A(x1,x2) = max{7, 1 + x1, 4 + x2} implies#_A(x1,x2) = max{7, 1 + x1, 4 + x2} =_A(x1,x2) = max{5, 9 + x1, 4 + x2} =#_A(x1,x2) = max{5, 9 + x1, 4 + x2} precedence: = > not = and > false = or = implies > true > if