blob: f0b1a6d1b1445e428f61f4c967ca992470793085 [file] [log] [blame]
 %------------------------------------------------------------------------------ % 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. %------------------------------------------------------------------------------