% The (infinitely) Many-Valued sentential calculus (MV).
% 
% {MV-1,MV-2,MV-3,MV-5} axiomatizes MV.
% 

set(auto).

list(usable).

-P(i(x,y)) | -P(x) | P(y).      % condensed detachment

P(i(x,i(y,x))).                 % MV-1
P(i(i(x,y),i(i(y,z),i(x,z)))).  % MV-2
P(i(i(i(x,y),y),i(i(y,x),x))).  % MV-3
P(i(i(n(x),n(y)),i(y,x))).      % MV-5

% -P(i(n(n(a)),a)) | $ANS(MV_24).
-P(i(i(a,b),i(i(c,a),i(c,b)))) | $ANS(MV_25).
% -P(i(a,n(n(a)))) | $ANS(MV_29).

end_of_list.

