% problem-set/pelletier/p42.in
% created : 07/25/86
% revised : 08/17/89

% description:
%
% Full Predicate Logic (without Identity and Functions).
% A set is 'circular' if it is a member of another set which in turn is.
% a member of the original. Intuitively all sets are non-circular. .
% Prove there is no set of noncircular sets..
% -(Ey)(Ax)(Fxy <-> -(Ez)(Fxz & Fzx))..

% representation:
%
% declare_predicate(2,F).
% declare_variables([x,y,z]).

set(hyper_res).
set(ur_res).
set(simplify_fol).


formula_list(sos).

% denial of the statement
(exists y all x (F(x,y) <-> -(exists z (F(x,z) & F(z,x))))).

end_of_list.
