op(400, xfx, [*,+,^,v,/,\,#]).  % infix operators
op(300,yf,@).                   % postfix operator

list(usable).
x * (y + z) = (x * y) + (x * z).
x + x@ = 1.
(x * y@) + ((x * x) + (y@ * x)) = x.
(x * x@) + ((x * z) + (x@ * z)) = z.
(x * y@) + ((x * y) + (y@ * y)) = x.
A + A != A.
end_of_list.
