assign(max_seconds, 30).

%------------------------------------------------------------------------------
% File     : SET668+3 : TPTP v3.0.1. Released v2.2.0.
% Domain   : Set Theory (Relations)
% Problem  : Id on X subset of R  => X is domain R & X subset of range R
% Version  : [Wor89] axioms : Reduced > Incomplete.
% English  : If the identity relation on X is a subset of a relation R from 
%            X to Y then X is the domain of R and X is a subset of the range 
%            of R.

% Refs     : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int
%          : [Wor89] Woronowicz (1989), Relations Defined on Sets
% Source   : [ILF]
% Names    : RELSET_1 (31) [Wor89]

% Status   : Theorem
% Rating   : 0.22 v2.7.0, 0.17 v2.6.0, 0.14 v2.5.0, 0.12 v2.4.0, 0.25 v2.3.0, 0.33 v2.2.1
% Syntax   : Number of formulae    :   33 (   2 unit)
%            Number of atoms       :  130 (   7 equality)
%            Maximal formula depth :   11 (   6 average)
%            Number of connectives :  101 (   4 ~  ;   0  |;  13  &)
%                                         (  10 <=>;  74 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    6 (   0 propositional; 1-2 arity)
%            Number of functors    :   13 (   2 constant; 0-3 arity)
%            Number of variables   :   74 (   0 singleton;  68 !;   6 ?)
%            Maximal term depth    :    3 (   1 average)

% Comments :
%          : tptp2X -f mace4 SET668+3.p 
%------------------------------------------------------------------------------
%----NOTE WELL: conjecture has been negated
set(prolog_style_variables).
formulas(assumptions).

% p1, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( ( subset(B,C)
               & subset(C,B) )
            -> B = C ) ) ) ) ).

% p2, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( all D 
              ( ilf_type(D,set_type)
              -> ( all E 
                  ( ilf_type(E,relation_type(B,C))
                  -> ( subset(identity_relation_of(D),E)
                    -> ( subset(D,domain(B,C,E))
                       & subset(D,range(B,C,E)) ) ) ) ) ) ) ) ) ) ).

% p3, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( all D 
              ( ilf_type(D,set_type)
              -> ( member(ordered_pair(C,D),identity_relation_of(B))
               <-> ( member(C,B)
                   & C = D ) ) ) ) ) ) ) ).

% p4, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ilf_type(identity_relation_of(B),binary_relation_type) ) ).

% p5, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( ( all D 
                ( ilf_type(D,subset_type(cross_product(B,C)))
                -> ilf_type(D,relation_type(B,C)) ) )
             & ( all E 
                ( ilf_type(E,relation_type(B,C))
                -> ilf_type(E,subset_type(cross_product(B,C))) ) ) ) ) ) ) ).

% p6, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( exists D ilf_type(D,relation_type(C,B)) ) ) ) ) ).

% p7, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( subset(B,C)
           <-> ( all D 
                ( ilf_type(D,set_type)
                -> ( member(D,B)
                  -> member(D,C) ) ) ) ) ) ) ) ).

% p8, axiom.
    ( all B 
      ( ilf_type(B,binary_relation_type)
      -> ( all C 
          ( ilf_type(C,binary_relation_type)
          -> ( subset(B,C)
           <-> ( all D 
                ( ilf_type(D,set_type)
                -> ( all E 
                    ( ilf_type(E,set_type)
                    -> ( member(ordered_pair(D,E),B)
                      -> member(ordered_pair(D,E),C) ) ) ) ) ) ) ) ) ) ).

% p9, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( B = C
           <-> ( subset(B,C)
               & subset(C,B) ) ) ) ) ) ).

% p10, axiom.
    ( all B 
      ( ilf_type(B,binary_relation_type)
      -> ilf_type(domain_of(B),set_type) ) ).

% p11, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ilf_type(cross_product(B,C),set_type) ) ) ) ).

% p12, axiom.
    ( all B 
      ( ilf_type(B,binary_relation_type)
      -> ilf_type(range_of(B),set_type) ) ).

% p13, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ilf_type(ordered_pair(B,C),set_type) ) ) ) ).

% p14, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( ilf_type(B,binary_relation_type)
       <-> ( relation_like(B)
           & ilf_type(B,set_type) ) ) ) ).

% p15, axiom.
    ( exists B ilf_type(B,binary_relation_type) ).

% p16, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( ilf_type(C,subset_type(B))
           <-> ilf_type(C,member_type(power_set(B))) ) ) ) ) ).

% p17, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( exists C ilf_type(C,subset_type(B)) ) ) ).

% p18, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> subset(B,B) ) ).

% p19, axiom.
    ( all B 
      ( ilf_type(B,binary_relation_type)
      -> subset(B,B) ) ).

% p20, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( member(B,power_set(C))
           <-> ( all D 
                ( ilf_type(D,set_type)
                -> ( member(D,B)
                  -> member(D,C) ) ) ) ) ) ) ) ).

% p21, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( -(empty(power_set(B)))
         & ilf_type(power_set(B),set_type) ) ) ).

% p22, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ( -(empty(C))
             & ilf_type(C,set_type) )
          -> ( ilf_type(B,member_type(C))
           <-> member(B,C) ) ) ) ) ).

% p23, axiom.
    ( all B 
      ( ( -(empty(B))
         & ilf_type(B,set_type) )
      -> ( exists C ilf_type(C,member_type(B)) ) ) ).

% p24, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( relation_like(B)
       <-> ( all C 
            ( ilf_type(C,set_type)
            -> ( member(C,B)
              -> ( exists D 
                  ( ilf_type(D,set_type)
                   & ( exists E 
                      ( ilf_type(E,set_type)
                       & C = ordered_pair(D,E) ) ) ) ) ) ) ) ) ) ).

% p25, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( all D 
              ( ilf_type(D,subset_type(cross_product(B,C)))
              -> relation_like(D) ) ) ) ) ) ).

% p26, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( empty(B)
       <-> ( all C 
            ( ilf_type(C,set_type)
            -> -(member(C,B)) ) ) ) ) ).

% p27, axiom.
    ( all B 
      ( ( empty(B)
         & ilf_type(B,set_type) )
      -> relation_like(B) ) ).

% p28, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( all D 
              ( ilf_type(D,relation_type(B,C))
              -> domain(B,C,D) = domain_of(D) ) ) ) ) ) ).

% p29, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( all D 
              ( ilf_type(D,relation_type(B,C))
              -> ilf_type(domain(B,C,D),subset_type(B)) ) ) ) ) ) ).

% p30, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( all D 
              ( ilf_type(D,relation_type(B,C))
              -> range(B,C,D) = range_of(D) ) ) ) ) ) ).

% p31, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( all D 
              ( ilf_type(D,relation_type(B,C))
              -> ilf_type(range(B,C,D),subset_type(C)) ) ) ) ) ) ).

% p32, axiom.
    ( all B ilf_type(B,set_type) ).

% prove_relset_1_31, negated_conjecture.
    -(( ( all B 
          ( ilf_type(B,set_type)
          -> ( all C 
              ( ilf_type(C,set_type)
              -> ( all D 
                  ( ilf_type(D,relation_type(C,B))
                  -> ( subset(identity_relation_of(C),D)
                    -> ( C = domain(C,B,D)
                       & subset(C,range(C,B,D)) ) ) ) ) ) ) ) ) )).
end_of_list.

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