exists(X,exists(Y,~(X=Y) and all(Z,Z=X or Z=Y))).

%a=b -> [].
%X=a, X=b.


/*
goal ~(exists(Z,all(X, (exists(W,all(Y,f(X,Y)<=> Y=W)) <=> X=Z)))
        <=> 
       exists(Z,all(X, (exists(W,all(Y,f(Y,X)<=> Y=W)) <=> X=Z)))).

*/
goal ~(exists(Z,all(X, (exists(W,all(Y,(f(X,Y)<=> Y=W) <=> X=Z)))))
        <=> 
       exists(Z,all(X, (exists(W,all(Y,(f(Y,X)<=> Y=W) <=> X=Z)))))).


%:-saci([2]).