| %------------------------------------------------------------------------------ |
| % 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. |
| %------------------------------------------------------------------------------ |
