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

list(usable).

% L1, L3, B1:

y + (x * (y * z)) = y.
((x * y) + (y * z)) + y = y.
(x + y) * (x + y@) = x.

% y * (x + (y + z)) = y.         % L 2
% ((x + y) * (y + z)) * y = y.   % L 4
% (x * y) + (x * y@) = x.        % B 2

 ((x * z) + x) * (x + z) = x.
 ((x * x) + y) * (x + x) = x.
 ((y * x) + x) * (y + x) = x.

% ((x + z) * x) + (x * z) = x.
% ((x + x) * y) + (x * x) = x.
% ((y + x) * x) + (y * x) = x.

A@ @ != A.
 
end_of_list.