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