%------------------------------------------------------------------------------
% File     : SET002+4 : TPTP v3.1.0. Released v2.2.0.
% Domain   : Set Theory (Naive)
% Problem  : Idempotency of union
% Version  : [Pas99] axioms.
% English  :

% Refs     : [Pas99] Pastre (1999), Email to G. Sutcliffe
% Source   : [Pas99]
% Names    :

% Status   : Theorem
% Rating   : 0.36 v3.1.0, 0.56 v2.7.0, 0.33 v2.6.0, 0.57 v2.5.0, 0.50 v2.4.0, 0.25 v2.3.0, 0.00 v2.2.1
% Syntax   : Number of formulae    :   12 (   2 unit)
%            Number of atoms       :   30 (   3 equality)
%            Maximal formula depth :    7 (   5 average)
%            Number of connectives :   20 (   2 ~  ;   2  |;   4  &)
%                                         (  10 <=>;   2 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    4 (   0 propositional; 2-2 arity)
%            Number of functors    :    9 (   1 constant; 0-2 arity)
%            Number of variables   :   29 (   0 singleton;  28 !;   1 ?)
%            Maximal term depth    :    2 (   1 average)

% Comments : 
%          : tptp2X -f dfg -t rm_equality:rstfp SET002+4.p 
%------------------------------------------------------------------------------

begin_problem(TPTP_Problem).

list_of_descriptions.
name({*[ File     : SET002+4 : TPTP v3.1.0. Released v2.2.0.],[ Names    :]*}).
author({*[ Source   : [Pas99]]*}).
status(unknown).
description({*[ Refs     : [Pas99] Pastre (1999), Email to G. Sutcliffe]*}).
end_of_list.

list_of_symbols.
functions[(difference,2), (empty_set,0), (intersection,2), (power_set,1), (product,1), (singleton,1), (sum,1), (union,2), (unordered_pair,2)].
predicates[(equal_set,2), (member,2), (subset,2)].
end_of_list.

list_of_formulae(axioms).

formula(
 forall([A,B],
  equiv(
   subset(A,B),
   forall([X],
    implies(
     member(X,A),
     member(X,B))))),
subset ).

formula(
 forall([A,B],
  equiv(
   equal_set(A,B),
   and(
    subset(A,B),
    subset(B,A)))),
equal_set ).

formula(
 forall([X,A],
  equiv(
   member(X,power_set(A)),
   subset(X,A))),
power_set ).

formula(
 forall([X,A,B],
  equiv(
   member(X,intersection(A,B)),
   and(
    member(X,A),
    member(X,B)))),
intersection ).

formula(
 forall([X,A,B],
  equiv(
   member(X,union(A,B)),
   or(
    member(X,A),
    member(X,B)))),
union ).

formula(
 forall([X],
  not(
   member(X,empty_set))),
empty_set ).

formula(
 forall([B,A,E],
  equiv(
   member(B,difference(E,A)),
   and(
    member(B,E),
    not(
     member(B,A))))),
difference ).

formula(
 forall([X,A],
  equiv(
   member(X,singleton(A)),
   equal(X,A))),
singleton ).

formula(
 forall([X,A,B],
  equiv(
   member(X,unordered_pair(A,B)),
   or(
    equal(X,A),
    equal(X,B)))),
unordered_pair ).

formula(
 forall([X,A],
  equiv(
   member(X,sum(A)),
   exists([Y],
    and(
     member(Y,A),
     member(X,Y))))),
sum ).

formula(
 forall([X,A],
  equiv(
   member(X,product(A)),
   forall([Y],
    implies(
     member(Y,A),
     member(X,Y))))),
product ).

end_of_list.

%----NOTE WELL: conjecture has been negated
list_of_formulae(conjectures).

formula(  %(conjecture)
 forall([A],
  equal_set(union(A,A),A)),
thI14 ).

end_of_list.

end_problem.
%------------------------------------------------------------------------------