DOMAINS   
	EXPR=con(EXPR,EXPR);       % конъюнкция        
	impl(EXPR,EXPR);      % импликация
	no(EXPR);             % отрицание
	var(symbol).          % переменная

PREDICATES
   nondeterm reduce(EXPR,EXPR,integer)

CLAUSES
   reduce(var(X),var(X),_).   
   reduce(con(P,con(Q,R)),con(con(P1,Q1),R1),N):-N<>2,             %2
            reduce(P,P1,0),reduce(Q,Q1,0),reduce(R,R1,0). 
   reduce(con(P,impl(P,Q)),Q1,N):-N<>3,                            %3
            reduce(Q,Q1,0).
   reduce(con(no(Q),impl(P,Q)),P1,N):-N<>4,                    %4
            reduce(no(P),P1,0).
   reduce(con(no(no(Q)),impl(P,no(no(no(Q))))),no(P1),N):-N<>4,    %4.1
            reduce(P,P1,0).
   reduce(no(no(P)),P1,N):-N<>5,
            reduce(P,P1,6).                                   %5
   reduce(con(P,Q),X,N):-N<>1,
	    reduce(con(Q,P),X,1).
%            reduce(P,P1,0),reduce(Q,Q1,0),reduce(con(Q1,P1),X,1). %1   
   reduce(P,no(no(P)),N):-N<>6.                                %6
%   reduce(P,P,_).

GOAL
%  reduce(con(var(t), impl(var(s), no(var(t)))),X,0),
%  reduce(con(var(t),impl(var(t),var(s))),X,0),
 reduce(con(no(no(con(impl(var(p),var(q)),var(p)))),
         impl(no(var(r)),no(con(impl(var(p),var(q)),var(p))))),X,0),
%  reduce(con(no(no(var(q))),impl(no(con(impl(var(p),var(q)),var(p))),
%          no(var(q)))),X,0),
  write(X),nl,X=no(var(s)).
