twee-0.1: tests/and-or.p

cnf(a, axiom, '+'(X, Y) = '+'(Y, X)).
cnf(a, axiom, '+'(X, '+'(Y, Z)) = '+'('+'(X, Y), Z)).
cnf(a, axiom, '*'(X, Y) = '*'(Y, X)).
cnf(a, axiom, '*'(X, '*'(Y, Z)) = '*'('*'(X, Y), Z)).
cnf(a, axiom, '+'(X, '0') = X).
cnf(a, axiom, '*'(X, '0') = '0').
cnf(a, axiom, '*'(X, '+'(Y, Z)) = '+'('*'(X, Y), '*'(X, Z))).
cnf(a, axiom, '+'(X, '*'(Y, Z)) = '*'('+'(X, Y), '+'(X, Z))).
cnf(a, axiom, not(not(X)) = X).
cnf(a, axiom, not('+'(X, Y)) = '*'(not(X), not(Y))).
cnf(a, axiom, '+'(X, not(X)) = '1').
cnf(a, axiom, '*'(X, not(X)) = '0').