assign(max_seconds, 120).

%------------------------------------------------------------------------------
% File     : SET660+3 : TPTP v3.0.1. Released v2.2.0.
% Domain   : Set Theory (Relations)
% Problem  : For every y in Y ? x : <x,y> in R (X to Y) iff range of R is Y
% Version  : [Wor89] axioms : Reduced > Incomplete.
% English  : For every y in Y there exists x such that <x,y> is in a 
%            relation R from X to Y iff the range of R is Y.

% 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 (23) [Wor89]

% Status   : Theorem
% Rating   : 0.78 v2.7.0, 0.67 v2.6.0, 0.71 v2.5.0, 0.75 v2.4.0, 0.75 v2.3.0, 0.67 v2.2.1
% Syntax   : Number of formulae    :   35 (   2 unit)
%            Number of atoms       :  141 (  10 equality)
%            Maximal formula depth :   13 (   6 average)
%            Number of connectives :  110 (   4 ~  ;   0  |;  12  &)
%                                         (  14 <=>;  80 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    6 (   0 propositional; 1-2 arity)
%            Number of functors    :   14 (   2 constant; 0-3 arity)
%            Number of variables   :   83 (   0 singleton;  75 !;   8 ?)
%            Maximal term depth    :    3 (   1 average)

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

% p1, axiom.
    ( all B 
      ( ilf_type(B,binary_relation_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( member(C,range_of(B))
           <-> ( exists D 
                ( ilf_type(D,set_type)
                 & member(ordered_pair(D,C),B) ) ) ) ) ) ) ).

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

% p3, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> ( all D 
              ( ilf_type(D,binary_relation_type)
              -> ( member(ordered_pair(B,C),D)
                -> ( member(B,domain_of(D))
                   & member(C,range_of(D)) ) ) ) ) ) ) ) ).

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

% p5, 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,set_type)
                  -> ( all F 
                      ( ilf_type(F,set_type)
                      -> ( F = ordered_pair(D,E)
                       <-> F = unordered_pair(unordered_pair(D,E),singleton(D)) ) ) ) ) ) ) ) ) ) ) ).

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

% p7, 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))) ) ) ) ) ) ) ).

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

% 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)
      -> ilf_type(singleton(B),set_type) ) ).

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

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

% p14, axiom.
    ( all B 
      ( ilf_type(B,set_type)
      -> ( all C 
          ( ilf_type(C,set_type)
          -> unordered_pair(B,C) = unordered_pair(C,B) ) ) ) ).

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

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

% p17, 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))) ) ) ) ) ).

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

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

% p20, 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) ) ) ) ) ) ) ) ).

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

% p22, 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) ) ) ) ) ) ) ) ).

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

% p24, 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) ) ) ) ) ).

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

% p26, 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) ) ) ) ) ) ) ) ) ) ).

% p27, 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) ) ) ) ) ) ).

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

% p29, axiom.
    ( all B 
      ( ( empty(B)
         & ilf_type(B,set_type) )
      -> relation_like(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))
              -> domain(B,C,D) = domain_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(domain(B,C,D),subset_type(B)) ) ) ) ) ) ).

% p32, 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) ) ) ) ) ) ).

% p33, 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)) ) ) ) ) ) ).

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

% prove_relset_1_23, negated_conjecture.
    -(( ( all B 
          ( ilf_type(B,set_type)
          -> ( all C 
              ( ilf_type(C,set_type)
              -> ( all D 
                  ( ilf_type(D,relation_type(B,C))
                  -> ( ( all E 
                        ( ilf_type(E,set_type)
                        -> ( member(E,C)
                          -> ( exists F 
                              ( ilf_type(F,set_type)
                               & member(ordered_pair(F,E),D) ) ) ) ) )
                   <-> range(B,C,D) = C ) ) ) ) ) ) ) )).
end_of_list.

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