(VAR x y z) (RULES 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)) ) (COMMENT Example 2.32 in \cite{SK90})