assign(max_seconds, 30). %------------------------------------------------------------------------------ % File : SET593+3 : TPTP v3.0.1. Released v2.2.0. % Domain : Set Theory (Boolean properties) % Problem : If X (= Y U Z, then X \ Y (= Z and X \ Z (= Y % Version : [Try89] axioms : Reduced > Incomplete. % English : If X is a subset of the union of Y and Z, then the difference % of X and Y is a subset of Z and the difference of X and Z is % a subset of Y. % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % : [Try89] Trybulec (1989), Tarski Grothendieck Set Theory % : [TS89] Trybulec & Swieczkowska (1989), Boolean Properties of % Source : [ILF] % Names : BOOLE (52) [TS89] % Status : Theorem % Rating : 0.67 v2.7.0, 0.50 v2.6.0, 0.71 v2.5.0, 0.75 v2.4.0, 0.25 v2.3.0, 0.00 v2.2.1 % Syntax : Number of formulae : 7 ( 2 unit) % Number of atoms : 17 ( 2 equality) % Maximal formula depth : 7 ( 5 average) % Number of connectives : 11 ( 1 ~ ; 1 |; 2 &) % ( 5 <=>; 2 =>; 0 <=) % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 3 ( 0 propositional; 2-2 arity) % Number of functors : 2 ( 0 constant; 2-2 arity) % Number of variables : 18 ( 0 singleton; 18 !; 0 ?) % Maximal term depth : 2 ( 1 average) % Comments : % : tptp2X -f mace4 SET593+3.p %------------------------------------------------------------------------------ %----NOTE WELL: conjecture has been negated set(prolog_style_variables). formulas(assumptions). % union_defn, axiom. ( all B ( all C ( all D ( member(D,union(B,C)) <-> ( member(D,B) | member(D,C) ) ) ) ) ). % difference_defn, axiom. ( all B ( all C ( all D ( member(D,difference(B,C)) <-> ( member(D,B) & -(member(D,C)) ) ) ) ) ). % subset_defn, axiom. ( all B ( all C ( subset(B,C) <-> ( all D ( member(D,B) -> member(D,C) ) ) ) ) ). % commutativity_of_union, axiom. ( all B ( all C union(B,C) = union(C,B) ) ). % reflexivity_of_subset, axiom. ( all B subset(B,B) ). % equal_member_defn, axiom. ( all B ( all C ( B = C <-> ( all D ( member(D,B) <-> member(D,C) ) ) ) ) ). % prove_th52, negated_conjecture. -(( ( all B ( all C ( all D ( subset(B,union(C,D)) -> ( subset(difference(B,C),D) & subset(difference(B,D),C) ) ) ) ) ) )). end_of_list. %------------------------------------------------------------------------------