(VAR x y z) (RULES or(0, x) -> x or(x, 0) -> x or(1, x) -> 1 or(x, 1) -> 1 or(x, not(x)) -> 1 or(not(x), x) -> 1 and(0, x) -> 0 and(x, 0) -> 0 and(1, x) -> x and(x, 1) -> x and(x, not(x)) -> 0 and(not(x), x) -> 0 not(1) -> 0 not(0) -> 1 implies(x, y) -> 1 | not(x) -> 1 implies(x, y) -> 1 | y -> 1 implies(x, y) -> 0 | x -> 1, y -> 0 f(x) -> f(0) | implies(implies(x, implies(x, 0)), 0) -> 1 )