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.

%------------------------------------------------------------------------------