(VAR x y )
(RULES 
        and(x,false) -> false
        and(x,not(false)) -> x
        not(not(x)) -> x
        implies(false,y) -> not(false)
        implies(x,false) -> not(x)
        implies(not(x),not(y)) -> implies(y,and(x,y))
        
)