 % Query: cequiv(g)
cequiv(X) :- cnfequiv(X,Y), write(Y). 

cnfequiv(X,Y) :- transform(X,Z), cnfequiv(Z,Y).
cnfequiv(X,X).

transform(n(n(X)),X).  % eliminate double negation

transform(n(a(X,Y)),o(n(X),n(Y))).  % De Morgan
transform(n(o(X,Y)),a(n(X),n(Y))).  %

transform(o(X,a(Y,Z)),a(o(X,Y),o(X,Z))).   % distribution
transform(o(a(X,Y),Z),a(o(X,Z),o(Y,Z))).   %

transform(o(X1,Y),o(X2,Y)) :- transform(X1,X2).  %
transform(o(X,Y1),o(X,Y2)) :- transform(Y1,Y2).  %
                                                 % transform subterms
transform(a(X1,Y),a(X2,Y)) :- transform(X1,X2).  %
transform(a(X,Y1),a(X,Y2)) :- transform(Y1,Y2).  %
                                                 %
transform(n(X1),n(X2)) :- transform(X1,X2).      %