%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEU711^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:29:06 AM UTC 2026
% Result : Theorem 92.79s 21.72s
% Output : Refutation 89.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 8
% Syntax : Number of formulae : 941 ( 59 unt; 0 typ; 7 def)
% Number of atoms : 3582 (1240 equ; 0 cnn)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 12269 (1819 ~;1719 |; 9 &;8669 @)
% ( 0 <=>; 53 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 7 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 13 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 1398 ( 2 ^;1392 !; 0 ?;1398 :)
% ( 0 !>; 0 ?*; 0 @-; 4 @+)
% Comments :
%------------------------------------------------------------------------------
thf(in_decl,type,
in: $i > $i > $o ).
thf(powerset_decl,type,
powerset: $i > $i ).
thf(powersetI_decl,type,
powersetI: $o ).
thf(powersetE_decl,type,
powersetE: $o ).
thf(binunion_decl,type,
binunion: $i > $i > $i ).
thf(binunionEcases_decl,type,
binunionEcases: $o ).
thf(sk1_decl,type,
sk1: $i > $i > $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(powersetI_def,definition,
( powersetI
= ( ! [A: $i,B: $i] :
( ! [C: $i] :
( ( in @ C @ B )
=> ( in @ C @ A ) )
=> ( in @ B @ ( powerset @ A ) ) ) ) ) ).
thf(powersetE_def,definition,
( powersetE
= ( ! [A: $i,B: $i,C: $i] :
( ( in @ B @ ( powerset @ A ) )
=> ( ( in @ C @ B )
=> ( in @ C @ A ) ) ) ) ) ).
thf(binunionEcases_def,definition,
( binunionEcases
= ( ! [A: $i,B: $i,C: $i,D: $o] :
( ( in @ C @ ( binunion @ A @ B ) )
=> ( ( ( in @ C @ A )
=> D )
=> ( ( ( in @ C @ B )
=> D )
=> D ) ) ) ) ) ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( in @ C @ A )
=> ( in @ C @ B ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ! [B: $i] :
( ( in @ B @ ( powerset @ A ) )
=> ! [C: $i] :
( ( in @ C @ ( powerset @ A ) )
=> ( in @ ( binunion @ B @ C ) @ ( powerset @ A ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ( in @ A @ ( powerset @ sk2 ) )
=> ! [B: $i] :
( ( in @ B @ ( powerset @ sk2 ) )
=> ( in @ ( binunion @ A @ B ) @ ( powerset @ sk2 ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
~ ( ( in @ A @ ( powerset @ sk2 ) )
=> ( in @ ( binunion @ sk3 @ A ) @ ( powerset @ sk2 ) ) ) ) ) ).
thf(1,conjecture,
( powersetI
=> ( powersetE
=> ( binunionEcases
=> ! [A: $i,B: $i] :
( ( in @ B @ ( powerset @ A ) )
=> ! [C: $i] :
( ( in @ C @ ( powerset @ A ) )
=> ( in @ ( binunion @ B @ C ) @ ( powerset @ A ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',binunionT_lem) ).
thf(2,negated_conjecture,
~ ( powersetI
=> ( powersetE
=> ( binunionEcases
=> ! [A: $i,B: $i] :
( ( in @ B @ ( powerset @ A ) )
=> ! [C: $i] :
( ( in @ C @ ( powerset @ A ) )
=> ( in @ ( binunion @ B @ C ) @ ( powerset @ A ) ) ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ( ! [A: $i,B: $i] :
( ! [C: $i] :
( ( in @ C @ B )
=> ( in @ C @ A ) )
=> ( in @ B @ ( powerset @ A ) ) )
=> ( ! [A: $i,B: $i,C: $i] :
( ( in @ B @ ( powerset @ A ) )
=> ( ( in @ C @ B )
=> ( in @ C @ A ) ) )
=> ( ! [A: $i,B: $i,C: $i,D: $o] :
( ( in @ C @ ( binunion @ A @ B ) )
=> ( ( ( in @ C @ A )
=> D )
=> ( ( ( in @ C @ B )
=> D )
=> D ) ) )
=> ! [A: $i,B: $i] :
( ( in @ B @ ( powerset @ A ) )
=> ! [C: $i] :
( ( in @ C @ ( powerset @ A ) )
=> ( in @ ( binunion @ B @ C ) @ ( powerset @ A ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
~ ( ! [A: $i,B: $i] :
( ! [C: $i] :
( ( in @ C @ B )
=> ( in @ C @ A ) )
=> ( in @ B @ ( powerset @ A ) ) )
=> ( ! [A: $i,B: $i] :
( ( in @ B @ ( powerset @ A ) )
=> ! [C: $i] :
( ( in @ C @ B )
=> ( in @ C @ A ) ) )
=> ( ! [A: $i,B: $i,C: $i] :
( ( in @ C @ ( binunion @ A @ B ) )
=> ! [D: $o] :
( ( ( in @ C @ A )
=> D )
=> ( ( ( in @ C @ B )
=> D )
=> D ) ) )
=> ! [A: $i,B: $i] :
( ( in @ B @ ( powerset @ A ) )
=> ! [C: $i] :
( ( in @ C @ ( powerset @ A ) )
=> ( in @ ( binunion @ B @ C ) @ ( powerset @ A ) ) ) ) ) ) ),
inference(miniscope,[status(thm)],[3]) ).
thf(5,plain,
! [I: $o,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( in @ ( sk1 @ B @ A ) @ B )
| ( in @ B @ ( powerset @ A ) ) )
& ( ~ ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ B @ ( powerset @ A ) ) )
& ( ~ ( in @ D @ ( powerset @ C ) )
| ~ ( in @ E @ D )
| ( in @ E @ C ) )
& ( ~ ( in @ H @ ( binunion @ F @ G ) )
| ( in @ H @ F )
| ( in @ H @ G )
| I )
& ( ~ ( in @ H @ ( binunion @ F @ G ) )
| ( in @ H @ F )
| ~ I
| I )
& ( ~ ( in @ H @ ( binunion @ F @ G ) )
| ~ I
| ( in @ H @ G )
| I )
& ( ~ ( in @ H @ ( binunion @ F @ G ) )
| ~ I
| ~ I
| I )
& ( in @ sk3 @ ( powerset @ sk2 ) )
& ( in @ sk4 @ ( powerset @ sk2 ) )
& ~ ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ),
inference(cnf,[status(esa)],[4]) ).
thf(9,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ B )
| ( in @ B @ ( powerset @ A ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(8,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ( in @ C @ A ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(20,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ( in @ C @ A ) ),
inference(simp,[status(thm)],[8]) ).
thf(62,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ~ ( in @ D @ ( powerset @ C ) )
| ~ $true
| ( in @ E @ C )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ E @ D ) ) ),
inference(paramod_ordered,[status(thm)],[9,20]) ).
thf(63,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ~ ( in @ D @ ( powerset @ C ) )
| ( in @ E @ C )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ E @ D ) ) ),
inference(simp,[status(thm)],[62]) ).
thf(64,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ C ) )
| ~ ( in @ B @ ( powerset @ A ) )
| ( in @ ( sk1 @ B @ C ) @ A ) ),
inference(pattern_uni,[status(thm)],[63:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( C )),bind(D,$thf( F )),bind(E,$thf( sk1 @ F @ G ))]]) ).
thf(69,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ C ) )
| ~ ( in @ B @ ( powerset @ A ) )
| ( in @ ( sk1 @ B @ C ) @ A ) ),
inference(simp,[status(thm)],[64]) ).
thf(12,plain,
in @ sk4 @ ( powerset @ sk2 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(13,plain,
! [B: $i,A: $i] :
( ~ ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ B @ ( powerset @ A ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(103,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ~ $true
| ( in @ E @ ( powerset @ D ) )
| ( ( in @ C @ A )
!= ( in @ ( sk1 @ E @ D ) @ D ) ) ),
inference(paramod_ordered,[status(thm)],[20,13]) ).
thf(104,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ( in @ E @ ( powerset @ D ) )
| ( ( in @ C @ A )
!= ( in @ ( sk1 @ E @ D ) @ D ) ) ),
inference(simp,[status(thm)],[103]) ).
thf(105,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ ( sk1 @ C @ A ) @ B )
| ( in @ C @ ( powerset @ A ) ) ),
inference(pattern_uni,[status(thm)],[104:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( sk1 @ F @ A )),bind(D,$thf( A )),bind(E,$thf( F ))]]) ).
thf(121,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ ( sk1 @ C @ A ) @ B )
| ( in @ C @ ( powerset @ A ) ) ),
inference(simp,[status(thm)],[105]) ).
thf(8062,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ~ ( in @ ( sk1 @ C @ A ) @ B )
| ( in @ C @ ( powerset @ A ) )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[12,121]) ).
thf(8063,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ ( sk1 @ C @ A ) @ B )
| ( in @ C @ ( powerset @ A ) )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(simp,[status(thm)],[8062]) ).
thf(8064,plain,
! [A: $i] :
( ~ ( in @ ( sk1 @ A @ sk2 ) @ sk4 )
| ( in @ A @ ( powerset @ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[8063:[bind(A,$thf( sk2 )),bind(B,$thf( sk4 ))]]) ).
thf(8334,plain,
! [A: $i] :
( ~ ( in @ ( sk1 @ A @ sk2 ) @ sk4 )
| ( in @ A @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[8064]) ).
thf(40065,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ C ) )
| ~ ( in @ B @ ( powerset @ A ) )
| ~ $true
| ( in @ D @ ( powerset @ sk2 ) )
| ( ( in @ ( sk1 @ B @ C ) @ A )
!= ( in @ ( sk1 @ D @ sk2 ) @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[69,8334]) ).
thf(40066,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ C ) )
| ~ ( in @ B @ ( powerset @ A ) )
| ( in @ D @ ( powerset @ sk2 ) )
| ( ( in @ ( sk1 @ B @ C ) @ A )
!= ( in @ ( sk1 @ D @ sk2 ) @ sk4 ) ) ),
inference(simp,[status(thm)],[40065]) ).
thf(40067,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ sk2 ) )
| ~ ( in @ A @ ( powerset @ sk4 ) )
| ( in @ A @ ( powerset @ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[40066:[bind(A,$thf( sk4 )),bind(B,$thf( B )),bind(C,$thf( sk2 )),bind(D,$thf( B ))]]) ).
thf(40457,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ sk2 ) )
| ~ ( in @ A @ ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[40067]) ).
thf(40608,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( in @ C @ ( powerset @ sk2 ) )
| ~ $true
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ C @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,40457]) ).
thf(40609,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( in @ C @ ( powerset @ sk2 ) )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ C @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[40608]) ).
thf(40610,plain,
! [A: $i] :
( ( in @ ( powerset @ sk4 ) @ ( powerset @ A ) )
| ( in @ ( sk1 @ ( powerset @ sk4 ) @ A ) @ ( powerset @ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[40609:[bind(A,$thf( E )),bind(B,$thf( powerset @ sk4 )),bind(C,$thf( sk1 @ ( powerset @ sk4 ) @ E ))]]) ).
thf(40968,plain,
! [A: $i] :
( ( in @ ( powerset @ sk4 ) @ ( powerset @ A ) )
| ( in @ ( sk1 @ ( powerset @ sk4 ) @ A ) @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[40610]) ).
thf(45589,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ ( powerset @ sk4 ) @ ( powerset @ A ) )
| ~ $true
| ( in @ C @ ( powerset @ B ) )
| ( ( in @ ( sk1 @ ( powerset @ sk4 ) @ A ) @ ( powerset @ sk2 ) )
!= ( in @ ( sk1 @ C @ B ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[40968,13]) ).
thf(45590,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ ( powerset @ sk4 ) @ ( powerset @ A ) )
| ( in @ C @ ( powerset @ B ) )
| ( ( in @ ( sk1 @ ( powerset @ sk4 ) @ A ) @ ( powerset @ sk2 ) )
!= ( in @ ( sk1 @ C @ B ) @ B ) ) ),
inference(simp,[status(thm)],[45589]) ).
thf(45591,plain,
( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
| ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(pattern_uni,[status(thm)],[45590:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( powerset @ sk2 )),bind(C,$thf( powerset @ sk4 ))]]) ).
thf(45771,plain,
in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ),
inference(simp,[status(thm)],[45591]) ).
thf(38,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ~ ( in @ C @ B )
| ( in @ C @ A )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[12,20]) ).
thf(39,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ C @ B )
| ( in @ C @ A )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(simp,[status(thm)],[38]) ).
thf(40,plain,
! [A: $i] :
( ~ ( in @ A @ sk4 )
| ( in @ A @ sk2 ) ),
inference(pattern_uni,[status(thm)],[39:[bind(A,$thf( sk2 )),bind(B,$thf( sk4 ))]]) ).
thf(54,plain,
! [A: $i] :
( ~ ( in @ A @ sk4 )
| ( in @ A @ sk2 ) ),
inference(simp,[status(thm)],[40]) ).
thf(73,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ~ $true
| ( in @ D @ sk2 )
| ( ( in @ C @ A )
!= ( in @ D @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[20,54]) ).
thf(74,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ( in @ D @ sk2 )
| ( ( in @ C @ A )
!= ( in @ D @ sk4 ) ) ),
inference(simp,[status(thm)],[73]) ).
thf(75,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk4 ) )
| ~ ( in @ B @ A )
| ( in @ B @ sk2 ) ),
inference(pattern_uni,[status(thm)],[74:[bind(A,$thf( sk4 )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(87,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk4 ) )
| ~ ( in @ B @ A )
| ( in @ B @ sk2 ) ),
inference(simp,[status(thm)],[75]) ).
thf(4358,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk4 ) )
| ( in @ B @ sk2 )
| ( ( in @ B @ A )
!= ( in @ A @ ( powerset @ sk4 ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[87]) ).
thf(4370,plain,
( ~ ( in @ ( powerset @ sk4 ) @ ( powerset @ sk4 ) )
| ( in @ ( powerset @ sk4 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[4358:[bind(A,$thf( powerset @ sk4 )),bind(B,$thf( powerset @ sk4 ))]]) ).
thf(45893,plain,
( ~ $true
| ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ ( powerset @ sk4 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[45771,4370]) ).
thf(45894,plain,
( ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ ( powerset @ sk4 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[45893]) ).
thf(46010,plain,
( ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( powerset @ sk4 )
!= ( powerset @ sk4 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[45894]) ).
thf(46107,plain,
( ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[46010]) ).
thf(52505,plain,
( ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( powerset @ sk2 )
!= sk4 ) ),
inference(simp,[status(thm)],[46107]) ).
thf(108,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ~ $true
| ( in @ D @ ( powerset @ C ) )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ ( sk1 @ D @ C ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[9,13]) ).
thf(109,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( in @ D @ ( powerset @ C ) )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ ( sk1 @ D @ C ) @ C ) ) ),
inference(simp,[status(thm)],[108]) ).
thf(110,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ A ) )
| ( in @ A @ ( powerset @ A ) ) ),
inference(pattern_uni,[status(thm)],[109:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( B ))]]) ).
thf(122,plain,
! [A: $i] : ( in @ A @ ( powerset @ A ) ),
inference(simp,[status(thm)],[110]) ).
thf(128,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ C @ ( powerset @ B ) )
| ~ $true
| ( in @ D @ B )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ D @ C ) ) ),
inference(paramod_ordered,[status(thm)],[122,20]) ).
thf(129,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ C @ ( powerset @ B ) )
| ( in @ D @ B )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ D @ C ) ) ),
inference(simp,[status(thm)],[128]) ).
thf(130,plain,
! [B: $i,A: $i] :
( ~ ( in @ ( powerset @ B ) @ ( powerset @ A ) )
| ( in @ B @ A ) ),
inference(pattern_uni,[status(thm)],[129:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( powerset @ E )),bind(D,$thf( E ))]]) ).
thf(138,plain,
! [B: $i,A: $i] :
( ~ ( in @ ( powerset @ B ) @ ( powerset @ A ) )
| ( in @ B @ A ) ),
inference(simp,[status(thm)],[130]) ).
thf(15,plain,
in @ sk3 @ ( powerset @ sk2 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(79,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ A @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[15,54]) ).
thf(80,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ A @ sk4 ) ) ),
inference(simp,[status(thm)],[79]) ).
thf(83,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( sk3 != A )
| ( ( powerset @ sk2 )
!= sk4 ) ),
inference(simp,[status(thm)],[80]) ).
thf(85,plain,
( ( in @ sk3 @ sk2 )
| ( ( powerset @ sk2 )
!= sk4 ) ),
inference(simp,[status(thm)],[83]) ).
thf(91,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ $true
| ~ ( in @ C @ B )
| ( in @ C @ A )
| ( ( in @ sk3 @ sk2 )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[85,20]) ).
thf(92,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ C @ B )
| ( in @ C @ A )
| ( ( in @ sk3 @ sk2 )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(simp,[status(thm)],[91]) ).
thf(99,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ C @ A )
| ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ C @ B )
| ( sk3 != B )
| ( ( powerset @ A )
!= sk2 ) ),
inference(simp,[status(thm)],[92]) ).
thf(101,plain,
! [B: $i,A: $i] :
( ( in @ B @ A )
| ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ B @ sk3 )
| ( ( powerset @ A )
!= sk2 ) ),
inference(simp,[status(thm)],[99]) ).
thf(133,plain,
! [B: $i,A: $i] :
( ~ $true
| ( in @ B @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ B @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[122,54]) ).
thf(134,plain,
! [B: $i,A: $i] :
( ( in @ B @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ B @ sk4 ) ) ),
inference(simp,[status(thm)],[133]) ).
thf(137,plain,
! [B: $i,A: $i] :
( ( in @ B @ sk2 )
| ( A != B )
| ( ( powerset @ A )
!= sk4 ) ),
inference(simp,[status(thm)],[134]) ).
thf(141,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( powerset @ A )
!= sk4 ) ),
inference(simp,[status(thm)],[137]) ).
thf(14,plain,
~ ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(29,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ~ $true
| ( ( in @ C @ A )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,14]) ).
thf(30,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ( ( in @ C @ A )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[29]) ).
thf(31,plain,
! [A: $i] :
( ~ ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A ) ),
inference(pattern_uni,[status(thm)],[30:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( B )),bind(C,$thf( binunion @ sk3 @ sk4 ))]]) ).
thf(56,plain,
! [A: $i] :
( ~ ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A ) ),
inference(simp,[status(thm)],[31]) ).
thf(844,plain,
! [B: $i,A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ~ ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[141,56]) ).
thf(845,plain,
! [B: $i,A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ~ ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ B ) ) ),
inference(simp,[status(thm)],[844]) ).
thf(846,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ~ ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(pattern_uni,[status(thm)],[845:[bind(A,$thf( binunion @ sk3 @ sk4 )),bind(B,$thf( sk2 ))]]) ).
thf(131,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ( in @ C @ ( powerset @ B ) )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( sk1 @ C @ B ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[122,13]) ).
thf(132,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ C @ ( powerset @ B ) )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( sk1 @ C @ B ) @ B ) ) ),
inference(simp,[status(thm)],[131]) ).
thf(135,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ C @ ( powerset @ B ) )
| ( A
!= ( sk1 @ C @ B ) )
| ( ( powerset @ A )
!= B ) ),
inference(simp,[status(thm)],[132]) ).
thf(139,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( ( powerset @ ( sk1 @ B @ A ) )
!= A ) ),
inference(simp,[status(thm)],[135]) ).
thf(44,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ~ ( in @ C @ B )
| ( in @ C @ A )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[15,20]) ).
thf(45,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ C @ B )
| ( in @ C @ A )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(simp,[status(thm)],[44]) ).
thf(46,plain,
! [A: $i] :
( ~ ( in @ A @ sk3 )
| ( in @ A @ sk2 ) ),
inference(pattern_uni,[status(thm)],[45:[bind(A,$thf( sk2 )),bind(B,$thf( sk3 ))]]) ).
thf(55,plain,
! [A: $i] :
( ~ ( in @ A @ sk3 )
| ( in @ A @ sk2 ) ),
inference(simp,[status(thm)],[46]) ).
thf(185,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ~ $true
| ( in @ D @ sk2 )
| ( ( in @ C @ A )
!= ( in @ D @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[20,55]) ).
thf(186,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ( in @ D @ sk2 )
| ( ( in @ C @ A )
!= ( in @ D @ sk3 ) ) ),
inference(simp,[status(thm)],[185]) ).
thf(187,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk3 ) )
| ~ ( in @ B @ A )
| ( in @ B @ sk2 ) ),
inference(pattern_uni,[status(thm)],[186:[bind(A,$thf( sk3 )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(210,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk3 ) )
| ~ ( in @ B @ A )
| ( in @ B @ sk2 ) ),
inference(simp,[status(thm)],[187]) ).
thf(21287,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk3 ) )
| ( in @ B @ sk2 )
| ( ( in @ B @ A )
!= ( in @ A @ ( powerset @ sk3 ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[210]) ).
thf(21361,plain,
( ~ ( in @ ( powerset @ sk3 ) @ ( powerset @ sk3 ) )
| ( in @ ( powerset @ sk3 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[21287:[bind(A,$thf( powerset @ sk3 )),bind(B,$thf( powerset @ sk3 ))]]) ).
thf(23103,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( in @ ( powerset @ sk3 ) @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk3 ) @ ( powerset @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,21361]) ).
thf(23104,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( in @ ( powerset @ sk3 ) @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk3 ) @ ( powerset @ sk3 ) ) ) ),
inference(simp,[status(thm)],[23103]) ).
thf(23105,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk3 ) @ sk3 ) )
!= sk3 )
| ( in @ ( powerset @ sk3 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[23104:[bind(A,$thf( sk3 )),bind(B,$thf( powerset @ sk3 ))]]) ).
thf(197,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ A @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[12,55]) ).
thf(198,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ A @ sk3 ) ) ),
inference(simp,[status(thm)],[197]) ).
thf(202,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( sk4 != A )
| ( ( powerset @ sk2 )
!= sk3 ) ),
inference(simp,[status(thm)],[198]) ).
thf(209,plain,
( ( in @ sk4 @ sk2 )
| ( ( powerset @ sk2 )
!= sk3 ) ),
inference(simp,[status(thm)],[202]) ).
thf(222,plain,
! [B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ $true
| ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ A )
!= ( in @ sk4 @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[209,13]) ).
thf(223,plain,
! [B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ A )
!= ( in @ sk4 @ sk2 ) ) ),
inference(simp,[status(thm)],[222]) ).
thf(230,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( ( powerset @ sk2 )
!= sk3 )
| ( ( sk1 @ B @ A )
!= sk4 )
| ( A != sk2 ) ),
inference(simp,[status(thm)],[223]) ).
thf(234,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ sk2 ) )
| ( ( powerset @ sk2 )
!= sk3 )
| ( ( sk1 @ A @ sk2 )
!= sk4 ) ),
inference(simp,[status(thm)],[230]) ).
thf(834,plain,
! [B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) )
| ~ $true
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[122,56]) ).
thf(835,plain,
! [B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ B ) ) ),
inference(simp,[status(thm)],[834]) ).
thf(836,plain,
~ ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[835:[bind(A,$thf( binunion @ sk3 @ sk4 )),bind(B,$thf( powerset @ ( binunion @ sk3 @ sk4 ) ))]]) ).
thf(9862,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,836]) ).
thf(9863,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[9862]) ).
thf(9864,plain,
( ( powerset @ ( sk1 @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ sk2 ) ) )
!= ( powerset @ sk2 ) ),
inference(pattern_uni,[status(thm)],[9863:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( powerset @ ( binunion @ sk3 @ sk4 ) ))]]) ).
thf(76,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ~ $true
| ( in @ C @ sk2 )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ C @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[9,54]) ).
thf(77,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( in @ C @ sk2 )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ C @ sk4 ) ) ),
inference(simp,[status(thm)],[76]) ).
thf(78,plain,
! [A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ( in @ ( sk1 @ sk4 @ A ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[77:[bind(A,$thf( E )),bind(B,$thf( sk4 )),bind(C,$thf( sk1 @ sk4 @ E ))]]) ).
thf(88,plain,
! [A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ( in @ ( sk1 @ sk4 @ A ) @ sk2 ) ),
inference(simp,[status(thm)],[78]) ).
thf(10,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ C @ ( binunion @ A @ B ) )
| ( in @ C @ A )
| ( in @ C @ B )
| D ),
inference(cnfConj,[status(thm)],[5]) ).
thf(16,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ C @ ( binunion @ A @ B ) )
| ( in @ C @ A )
| ( in @ C @ B )
| D ),
inference(simp,[status(thm)],[10]) ).
thf(253,plain,
! [F: $o,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ~ $true
| ( in @ E @ C )
| ( in @ E @ D )
| F
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ E @ ( binunion @ C @ D ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,16]) ).
thf(254,plain,
! [F: $o,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( in @ E @ C )
| ( in @ E @ D )
| F
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ E @ ( binunion @ C @ D ) ) ) ),
inference(simp,[status(thm)],[253]) ).
thf(255,plain,
! [D: $i,C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ C @ D ) @ ( powerset @ B ) )
| ( in @ ( sk1 @ ( binunion @ C @ D ) @ B ) @ C )
| ( in @ ( sk1 @ ( binunion @ C @ D ) @ B ) @ D )
| A ),
inference(pattern_uni,[status(thm)],[254:[bind(A,$thf( H )),bind(B,$thf( binunion @ I @ J )),bind(C,$thf( I )),bind(D,$thf( J )),bind(E,$thf( sk1 @ ( binunion @ I @ J ) @ H )),bind(F,$thf( F ))]]) ).
thf(318,plain,
! [D: $i,C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ C @ D ) @ ( powerset @ B ) )
| ( in @ ( sk1 @ ( binunion @ C @ D ) @ B ) @ C )
| ( in @ ( sk1 @ ( binunion @ C @ D ) @ B ) @ D )
| A ),
inference(simp,[status(thm)],[255]) ).
thf(1037,plain,
! [D: $i,C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ C @ D ) @ ( powerset @ B ) )
| ( in @ ( sk1 @ ( binunion @ C @ D ) @ B ) @ C )
| A
| ( ( in @ ( sk1 @ ( binunion @ C @ D ) @ B ) @ D )
!= ( in @ ( sk1 @ ( binunion @ C @ D ) @ B ) @ C ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[318]) ).
thf(1060,plain,
! [C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ C @ C ) @ ( powerset @ B ) )
| ( in @ ( sk1 @ ( binunion @ C @ C ) @ B ) @ C )
| A ),
inference(pattern_uni,[status(thm)],[1037:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(1088,plain,
! [C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ C @ C ) @ ( powerset @ B ) )
| ( in @ ( sk1 @ ( binunion @ C @ C ) @ B ) @ C )
| A ),
inference(simp,[status(thm)],[1060]) ).
thf(1781,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ C @ C ) @ ( powerset @ B ) )
| A
| ~ $true
| ( in @ E @ ( powerset @ D ) )
| ( ( in @ ( sk1 @ ( binunion @ C @ C ) @ B ) @ C )
!= ( in @ ( sk1 @ E @ D ) @ D ) ) ),
inference(paramod_ordered,[status(thm)],[1088,13]) ).
thf(1782,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ C @ C ) @ ( powerset @ B ) )
| A
| ( in @ E @ ( powerset @ D ) )
| ( ( in @ ( sk1 @ ( binunion @ C @ C ) @ B ) @ C )
!= ( in @ ( sk1 @ E @ D ) @ D ) ) ),
inference(simp,[status(thm)],[1781]) ).
thf(1783,plain,
! [B: $i,A: $o] :
( ( in @ ( binunion @ B @ B ) @ ( powerset @ B ) )
| A
| ( in @ ( binunion @ B @ B ) @ ( powerset @ B ) ) ),
inference(pattern_uni,[status(thm)],[1782:[bind(A,$thf( A )),bind(B,$thf( G )),bind(C,$thf( G )),bind(D,$thf( G )),bind(E,$thf( binunion @ G @ G ))]]) ).
thf(1931,plain,
! [B: $i,A: $o] :
( ( in @ ( binunion @ B @ B ) @ ( powerset @ B ) )
| A ),
inference(simp,[status(thm)],[1783]) ).
thf(41,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ $true
| ( in @ C @ A )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[12,20]) ).
thf(42,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ( in @ C @ A )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ C @ B ) ) ),
inference(simp,[status(thm)],[41]) ).
thf(43,plain,
! [A: $i] :
( ~ ( in @ ( powerset @ sk2 ) @ ( powerset @ A ) )
| ( in @ sk4 @ A ) ),
inference(pattern_uni,[status(thm)],[42:[bind(A,$thf( A )),bind(B,$thf( powerset @ sk2 )),bind(C,$thf( sk4 ))]]) ).
thf(2470,plain,
! [C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ B @ B ) @ ( powerset @ B ) )
| ~ $true
| ( in @ sk4 @ C )
| ( A
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[1931,43]) ).
thf(2471,plain,
! [C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ B @ B ) @ ( powerset @ B ) )
| ( in @ sk4 @ C )
| ( A
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ C ) ) ) ),
inference(simp,[status(thm)],[2470]) ).
thf(2472,plain,
! [B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ sk4 @ B ) ),
inference(pattern_uni,[status(thm)],[2471:[bind(A,$thf( in @ ( powerset @ sk2 ) @ ( powerset @ G ) )),bind(B,$thf( B )),bind(C,$thf( G ))]]) ).
thf(2612,plain,
! [B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ sk4 @ B ) ),
inference(simp,[status(thm)],[2472]) ).
thf(1425,plain,
( ( ( powerset @ sk2 )
!= sk4 )
| ~ $true
| ( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk3 @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[85,836]) ).
thf(1426,plain,
( ( ( powerset @ sk2 )
!= sk4 )
| ( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk3 @ sk2 ) ) ),
inference(simp,[status(thm)],[1425]) ).
thf(1469,plain,
( ( ( powerset @ sk2 )
!= sk4 )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[1426]) ).
thf(353,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ~ $true
| ( in @ C @ ( powerset @ B ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( sk1 @ C @ B ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[141,13]) ).
thf(354,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ( in @ C @ ( powerset @ B ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( sk1 @ C @ B ) @ B ) ) ),
inference(simp,[status(thm)],[353]) ).
thf(355,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ( in @ A @ ( powerset @ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[354:[bind(A,$thf( sk1 @ D @ sk2 )),bind(B,$thf( sk2 )),bind(C,$thf( D ))]]) ).
thf(367,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ( in @ A @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[355]) ).
thf(1451,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ~ $true
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[367,836]) ).
thf(1452,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[1451]) ).
thf(1465,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ( A
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[1452]) ).
thf(1480,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ sk2 ) )
!= sk4 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[1465]) ).
thf(18107,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ sk2 ) )
!= sk4 )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[1480]) ).
thf(2564,plain,
! [A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| $false ),
inference(prim_subst,[status(thm)],[1931:[bind(A,$thf( $false ))]]) ).
thf(2593,plain,
! [A: $i] : ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) ),
inference(simp,[status(thm)],[2564]) ).
thf(4265,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ~ ( in @ C @ B )
| ( in @ C @ sk2 )
| ( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
!= ( in @ B @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[2593,87]) ).
thf(4266,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ C @ B )
| ( in @ C @ sk2 )
| ( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
!= ( in @ B @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[4265]) ).
thf(4267,plain,
! [A: $i] :
( ~ ( in @ A @ ( binunion @ sk4 @ sk4 ) )
| ( in @ A @ sk2 ) ),
inference(pattern_uni,[status(thm)],[4266:[bind(A,$thf( sk4 )),bind(B,$thf( binunion @ sk4 @ sk4 )),bind(C,$thf( C ))]]) ).
thf(4471,plain,
! [A: $i] :
( ~ ( in @ A @ ( binunion @ sk4 @ sk4 ) )
| ( in @ A @ sk2 ) ),
inference(simp,[status(thm)],[4267]) ).
thf(8874,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ~ $true
| ( in @ C @ sk2 )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ C @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,4471]) ).
thf(8875,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( in @ C @ sk2 )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ C @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[8874]) ).
thf(8876,plain,
! [A: $i] :
( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ A ) )
| ( in @ ( sk1 @ ( binunion @ sk4 @ sk4 ) @ A ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[8875:[bind(A,$thf( E )),bind(B,$thf( binunion @ sk4 @ sk4 )),bind(C,$thf( sk1 @ ( binunion @ sk4 @ sk4 ) @ E ))]]) ).
thf(8997,plain,
! [A: $i] :
( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ A ) )
| ( in @ ( sk1 @ ( binunion @ sk4 @ sk4 ) @ A ) @ sk2 ) ),
inference(simp,[status(thm)],[8876]) ).
thf(18179,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ A ) )
| ~ $true
| ( in @ C @ ( powerset @ B ) )
| ( ( in @ ( sk1 @ ( binunion @ sk4 @ sk4 ) @ A ) @ sk2 )
!= ( in @ ( sk1 @ C @ B ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[8997,13]) ).
thf(18180,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ A ) )
| ( in @ C @ ( powerset @ B ) )
| ( ( in @ ( sk1 @ ( binunion @ sk4 @ sk4 ) @ A ) @ sk2 )
!= ( in @ ( sk1 @ C @ B ) @ B ) ) ),
inference(simp,[status(thm)],[18179]) ).
thf(18181,plain,
( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
| ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[18180:[bind(A,$thf( sk2 )),bind(B,$thf( sk2 )),bind(C,$thf( binunion @ sk4 @ sk4 ))]]) ).
thf(18318,plain,
in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ),
inference(simp,[status(thm)],[18181]) ).
thf(18460,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk4 ) )
| ~ $true
| ( in @ B @ sk2 )
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[18318,87]) ).
thf(18461,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk4 ) )
| ( in @ B @ sk2 )
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(simp,[status(thm)],[18460]) ).
thf(18462,plain,
( ~ ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) )
| ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[18461:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( binunion @ sk4 @ sk4 ))]]) ).
thf(20012,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,18462]) ).
thf(20013,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[20012]) ).
thf(20014,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk2 ) @ sk4 ) )
!= sk4 )
| ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[20013:[bind(A,$thf( sk4 )),bind(B,$thf( powerset @ sk2 ))]]) ).
thf(9965,plain,
( ( sk1 @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ sk2 ) )
!= sk2 ),
inference(simp,[status(thm)],[9864]) ).
thf(21169,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk3 ) )
| ~ $true
| ( in @ B @ sk2 )
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[18318,210]) ).
thf(21170,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk3 ) )
| ( in @ B @ sk2 )
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(simp,[status(thm)],[21169]) ).
thf(21171,plain,
( ~ ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) )
| ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[21170:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( binunion @ sk4 @ sk4 ))]]) ).
thf(26586,plain,
! [A: $i] :
( ~ $true
| ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,21171]) ).
thf(26587,plain,
! [A: $i] :
( ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(simp,[status(thm)],[26586]) ).
thf(26766,plain,
! [A: $i] :
( ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( A
!= ( powerset @ sk2 ) )
| ( ( powerset @ A )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[26587]) ).
thf(26810,plain,
( ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[26766]) ).
thf(45865,plain,
( ~ $true
| ( ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[45771,14]) ).
thf(45866,plain,
( ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[45865]) ).
thf(46086,plain,
( ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ sk4 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[45866]) ).
thf(56176,plain,
( ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ sk4 ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[46086]) ).
thf(9789,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ~ $true
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,846]) ).
thf(9790,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[9789]) ).
thf(9791,plain,
( ( ( powerset @ ( sk1 @ sk2 @ ( powerset @ sk2 ) ) )
!= ( powerset @ sk2 ) )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 ) ),
inference(pattern_uni,[status(thm)],[9790:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk2 ))]]) ).
thf(4337,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk4 ) )
| ~ $true
| ( in @ B @ sk2 )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[15,87]) ).
thf(4338,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk4 ) )
| ( in @ B @ sk2 )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(simp,[status(thm)],[4337]) ).
thf(4339,plain,
( ~ ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) )
| ( in @ sk3 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[4338:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk3 ))]]) ).
thf(1866,plain,
! [D: $i,C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ C @ C ) @ ( powerset @ B ) )
| A
| ~ $true
| ( in @ D @ sk2 )
| ( ( in @ ( sk1 @ ( binunion @ C @ C ) @ B ) @ C )
!= ( in @ D @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[1088,55]) ).
thf(1867,plain,
! [D: $i,C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ C @ C ) @ ( powerset @ B ) )
| A
| ( in @ D @ sk2 )
| ( ( in @ ( sk1 @ ( binunion @ C @ C ) @ B ) @ C )
!= ( in @ D @ sk3 ) ) ),
inference(simp,[status(thm)],[1866]) ).
thf(1868,plain,
! [B: $i,A: $o] :
( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ B ) )
| A
| ( in @ ( sk1 @ ( binunion @ sk3 @ sk3 ) @ B ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[1867:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( sk3 )),bind(D,$thf( sk1 @ ( binunion @ sk3 @ sk3 ) @ F ))]]) ).
thf(1896,plain,
! [B: $i,A: $o] :
( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ B ) )
| A
| ( in @ ( sk1 @ ( binunion @ sk3 @ sk3 ) @ B ) @ sk2 ) ),
inference(simp,[status(thm)],[1868]) ).
thf(5142,plain,
! [D: $i,C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ B ) )
| A
| ~ $true
| ( in @ D @ ( powerset @ C ) )
| ( ( in @ ( sk1 @ ( binunion @ sk3 @ sk3 ) @ B ) @ sk2 )
!= ( in @ ( sk1 @ D @ C ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[1896,13]) ).
thf(5143,plain,
! [D: $i,C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ B ) )
| A
| ( in @ D @ ( powerset @ C ) )
| ( ( in @ ( sk1 @ ( binunion @ sk3 @ sk3 ) @ B ) @ sk2 )
!= ( in @ ( sk1 @ D @ C ) @ C ) ) ),
inference(simp,[status(thm)],[5142]) ).
thf(5144,plain,
! [A: $o] :
( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
| A
| ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[5143:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk2 )),bind(D,$thf( binunion @ sk3 @ sk3 ))]]) ).
thf(5325,plain,
! [A: $o] :
( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
| A ),
inference(simp,[status(thm)],[5144]) ).
thf(6185,plain,
! [A: $o] :
( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
| ~ $true
| ( A
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[5325,14]) ).
thf(6186,plain,
! [A: $o] :
( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
| ( A
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[6185]) ).
thf(6187,plain,
in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ),
inference(pattern_uni,[status(thm)],[6186:[bind(A,$thf( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ))]]) ).
thf(6416,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[6187,54]) ).
thf(6417,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ sk4 ) ) ),
inference(simp,[status(thm)],[6416]) ).
thf(6457,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( binunion @ sk3 @ sk3 )
!= A )
| ( ( powerset @ sk2 )
!= sk4 ) ),
inference(simp,[status(thm)],[6417]) ).
thf(6495,plain,
( ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( ( powerset @ sk2 )
!= sk4 ) ),
inference(simp,[status(thm)],[6457]) ).
thf(9276,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ~ $true
| ( in @ C @ B )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ C ) @ ( powerset @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[367,138]) ).
thf(9277,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ( in @ C @ B )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ C ) @ ( powerset @ B ) ) ) ),
inference(simp,[status(thm)],[9276]) ).
thf(9278,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ ( powerset @ A ) @ sk2 ) )
!= sk4 )
| ( in @ A @ sk2 ) ),
inference(pattern_uni,[status(thm)],[9277:[bind(A,$thf( powerset @ D )),bind(B,$thf( sk2 )),bind(C,$thf( D ))]]) ).
thf(9377,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ ( powerset @ A ) @ sk2 ) )
!= sk4 )
| ( in @ A @ sk2 ) ),
inference(simp,[status(thm)],[9278]) ).
thf(44346,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ ( powerset @ A ) @ sk2 ) )
!= sk4 )
| ~ ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[9377,56]) ).
thf(44347,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ ( powerset @ A ) @ sk2 ) )
!= sk4 )
| ~ ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ B ) ) ),
inference(simp,[status(thm)],[44346]) ).
thf(44348,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ sk2 ) )
!= sk4 )
| ~ ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(pattern_uni,[status(thm)],[44347:[bind(A,$thf( binunion @ sk3 @ sk4 )),bind(B,$thf( sk2 ))]]) ).
thf(6439,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk4 ) )
| ~ $true
| ( in @ B @ sk2 )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[6187,87]) ).
thf(6440,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk4 ) )
| ( in @ B @ sk2 )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(simp,[status(thm)],[6439]) ).
thf(6441,plain,
( ~ ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) )
| ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[6440:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( binunion @ sk3 @ sk3 ))]]) ).
thf(7969,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ~ ( in @ C @ ( powerset @ B ) )
| ~ $true
| ( in @ D @ ( powerset @ B ) )
| ( ( in @ ( sk1 @ sk4 @ A ) @ sk2 )
!= ( in @ ( sk1 @ D @ B ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[88,121]) ).
thf(7970,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ~ ( in @ C @ ( powerset @ B ) )
| ( in @ D @ ( powerset @ B ) )
| ( ( in @ ( sk1 @ sk4 @ A ) @ sk2 )
!= ( in @ ( sk1 @ D @ B ) @ C ) ) ),
inference(simp,[status(thm)],[7969]) ).
thf(7971,plain,
! [A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ~ ( in @ sk2 @ ( powerset @ A ) )
| ( in @ sk4 @ ( powerset @ A ) ) ),
inference(pattern_uni,[status(thm)],[7970:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 )),bind(D,$thf( sk4 ))]]) ).
thf(8293,plain,
! [A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ~ ( in @ sk2 @ ( powerset @ A ) ) ),
inference(simp,[status(thm)],[7971]) ).
thf(12024,plain,
! [B: $i,A: $i] :
( ~ ( in @ sk2 @ ( powerset @ A ) )
| ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ B )
| ( ( in @ sk4 @ ( powerset @ A ) )
!= ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[8293,56]) ).
thf(12025,plain,
! [B: $i,A: $i] :
( ~ ( in @ sk2 @ ( powerset @ A ) )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ B )
| ( ( in @ sk4 @ ( powerset @ A ) )
!= ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[12024]) ).
thf(12026,plain,
( ~ ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 ) ),
inference(pattern_uni,[status(thm)],[12025:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk4 ))]]) ).
thf(12583,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,12026]) ).
thf(12584,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[12583]) ).
thf(12585,plain,
( ( ( powerset @ ( sk1 @ sk2 @ ( powerset @ sk2 ) ) )
!= ( powerset @ sk2 ) )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 ) ),
inference(pattern_uni,[status(thm)],[12584:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk2 ))]]) ).
thf(12774,plain,
( ( ( sk1 @ sk2 @ ( powerset @ sk2 ) )
!= sk2 )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 ) ),
inference(simp,[status(thm)],[12585]) ).
thf(106,plain,
! [B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ $true
| ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ A )
!= ( in @ sk3 @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[85,13]) ).
thf(107,plain,
! [B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ A )
!= ( in @ sk3 @ sk2 ) ) ),
inference(simp,[status(thm)],[106]) ).
thf(117,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( ( powerset @ sk2 )
!= sk4 )
| ( ( sk1 @ B @ A )
!= sk3 )
| ( A != sk2 ) ),
inference(simp,[status(thm)],[107]) ).
thf(120,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ sk2 ) )
| ( ( powerset @ sk2 )
!= sk4 )
| ( ( sk1 @ A @ sk2 )
!= sk3 ) ),
inference(simp,[status(thm)],[117]) ).
thf(195,plain,
! [B: $i,A: $i] :
( ~ $true
| ( in @ B @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ B @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[122,55]) ).
thf(196,plain,
! [B: $i,A: $i] :
( ( in @ B @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ B @ sk3 ) ) ),
inference(simp,[status(thm)],[195]) ).
thf(206,plain,
! [B: $i,A: $i] :
( ( in @ B @ sk2 )
| ( A != B )
| ( ( powerset @ A )
!= sk3 ) ),
inference(simp,[status(thm)],[196]) ).
thf(214,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( powerset @ A )
!= sk3 ) ),
inference(simp,[status(thm)],[206]) ).
thf(4248,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk4 ) )
| ~ $true
| ( in @ B @ sk2 )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[12,87]) ).
thf(4249,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk4 ) )
| ( in @ B @ sk2 )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(simp,[status(thm)],[4248]) ).
thf(4250,plain,
( ~ ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) )
| ( in @ sk4 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[4249:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk4 ))]]) ).
thf(4552,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ~ $true
| ( in @ sk4 @ sk2 )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[214,4250]) ).
thf(4553,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ( in @ sk4 @ sk2 )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[4552]) ).
thf(4564,plain,
! [A: $i] :
( ( in @ sk4 @ sk2 )
| ( ( powerset @ A )
!= sk3 )
| ( A
!= ( powerset @ sk2 ) )
| ( ( powerset @ sk4 )
!= sk2 ) ),
inference(simp,[status(thm)],[4553]) ).
thf(4592,plain,
( ( in @ sk4 @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk3 )
| ( ( powerset @ sk4 )
!= sk2 ) ),
inference(simp,[status(thm)],[4564]) ).
thf(4343,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ sk4 ) )
| ~ $true
| ( in @ C @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[122,87]) ).
thf(4344,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ sk4 ) )
| ( in @ C @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ C @ B ) ) ),
inference(simp,[status(thm)],[4343]) ).
thf(4345,plain,
! [A: $i] :
( ~ ( in @ ( powerset @ A ) @ ( powerset @ sk4 ) )
| ( in @ A @ sk2 ) ),
inference(pattern_uni,[status(thm)],[4344:[bind(A,$thf( D )),bind(B,$thf( powerset @ D )),bind(C,$thf( D ))]]) ).
thf(4479,plain,
! [A: $i] :
( ~ ( in @ ( powerset @ A ) @ ( powerset @ sk4 ) )
| ( in @ A @ sk2 ) ),
inference(simp,[status(thm)],[4345]) ).
thf(18358,plain,
! [A: $i] :
( ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[18318,56]) ).
thf(18359,plain,
! [A: $i] :
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[18358]) ).
thf(18493,plain,
! [A: $i] :
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( binunion @ sk4 @ sk4 )
!= A )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[18359]) ).
thf(18549,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ sk4 @ sk4 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[18493]) ).
thf(6406,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ~ ( in @ C @ B )
| ( in @ C @ A )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[6187,20]) ).
thf(6407,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ C @ B )
| ( in @ C @ A )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(simp,[status(thm)],[6406]) ).
thf(6408,plain,
! [A: $i] :
( ~ ( in @ A @ ( binunion @ sk3 @ sk3 ) )
| ( in @ A @ sk2 ) ),
inference(pattern_uni,[status(thm)],[6407:[bind(A,$thf( sk2 )),bind(B,$thf( binunion @ sk3 @ sk3 )),bind(C,$thf( C ))]]) ).
thf(6485,plain,
! [A: $i] :
( ~ ( in @ A @ ( binunion @ sk3 @ sk3 ) )
| ( in @ A @ sk2 ) ),
inference(simp,[status(thm)],[6408]) ).
thf(9677,plain,
! [B: $i,A: $i] :
( ~ $true
| ( in @ B @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ B @ ( binunion @ sk3 @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,6485]) ).
thf(9678,plain,
! [B: $i,A: $i] :
( ( in @ B @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ B @ ( binunion @ sk3 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[9677]) ).
thf(9720,plain,
! [B: $i,A: $i] :
( ( in @ B @ sk2 )
| ( A != B )
| ( ( powerset @ A )
!= ( binunion @ sk3 @ sk3 ) ) ),
inference(simp,[status(thm)],[9678]) ).
thf(9769,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( powerset @ A )
!= ( binunion @ sk3 @ sk3 ) ) ),
inference(simp,[status(thm)],[9720]) ).
thf(20890,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk3 ) )
| ~ $true
| ( in @ B @ sk2 )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[6187,210]) ).
thf(20891,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk3 ) )
| ( in @ B @ sk2 )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(simp,[status(thm)],[20890]) ).
thf(20892,plain,
( ~ ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) )
| ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[20891:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( binunion @ sk3 @ sk3 ))]]) ).
thf(25995,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,20892]) ).
thf(25996,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(simp,[status(thm)],[25995]) ).
thf(25997,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk2 ) @ sk3 ) )
!= sk3 )
| ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[25996:[bind(A,$thf( sk3 )),bind(B,$thf( powerset @ sk2 ))]]) ).
thf(21032,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk3 ) )
| ~ $true
| ( in @ B @ sk2 )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[12,210]) ).
thf(21033,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk3 ) )
| ( in @ B @ sk2 )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(simp,[status(thm)],[21032]) ).
thf(21034,plain,
( ~ ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) )
| ( in @ sk4 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[21033:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk4 ))]]) ).
thf(21746,plain,
! [A: $i] :
( ~ $true
| ( in @ sk4 @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,21034]) ).
thf(21747,plain,
! [A: $i] :
( ( in @ sk4 @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(simp,[status(thm)],[21746]) ).
thf(21780,plain,
! [A: $i] :
( ( in @ sk4 @ sk2 )
| ( A
!= ( powerset @ sk2 ) )
| ( ( powerset @ A )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[21747]) ).
thf(21839,plain,
( ( in @ sk4 @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[21780]) ).
thf(123,plain,
! [A: $i] :
( ~ $true
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,14]) ).
thf(124,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[123]) ).
thf(136,plain,
! [A: $i] :
( ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( powerset @ A )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[124]) ).
thf(140,plain,
( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= ( powerset @ sk2 ) ),
inference(simp,[status(thm)],[136]) ).
thf(142,plain,
( ( binunion @ sk3 @ sk4 )
!= sk2 ),
inference(simp,[status(thm)],[140]) ).
thf(21263,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ sk3 ) )
| ~ $true
| ( in @ C @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[122,210]) ).
thf(21264,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ sk3 ) )
| ( in @ C @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ C @ B ) ) ),
inference(simp,[status(thm)],[21263]) ).
thf(21265,plain,
! [A: $i] :
( ~ ( in @ ( powerset @ A ) @ ( powerset @ sk3 ) )
| ( in @ A @ sk2 ) ),
inference(pattern_uni,[status(thm)],[21264:[bind(A,$thf( D )),bind(B,$thf( powerset @ D )),bind(C,$thf( D ))]]) ).
thf(21445,plain,
! [A: $i] :
( ~ ( in @ ( powerset @ A ) @ ( powerset @ sk3 ) )
| ( in @ A @ sk2 ) ),
inference(simp,[status(thm)],[21265]) ).
thf(32041,plain,
! [B: $i,A: $i] :
( ~ $true
| ( in @ B @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ B ) @ ( powerset @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,21445]) ).
thf(32042,plain,
! [B: $i,A: $i] :
( ( in @ B @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ B ) @ ( powerset @ sk3 ) ) ) ),
inference(simp,[status(thm)],[32041]) ).
thf(32052,plain,
! [B: $i,A: $i] :
( ( in @ B @ sk2 )
| ( A
!= ( powerset @ B ) )
| ( ( powerset @ A )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[32042]) ).
thf(32165,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[32052]) ).
thf(2530,plain,
! [C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ B @ B ) @ ( powerset @ B ) )
| ~ $true
| ( in @ C @ sk2 )
| ( A
!= ( in @ C @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[1931,54]) ).
thf(2531,plain,
! [C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ B @ B ) @ ( powerset @ B ) )
| ( in @ C @ sk2 )
| ( A
!= ( in @ C @ sk4 ) ) ),
inference(simp,[status(thm)],[2530]) ).
thf(2532,plain,
! [B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ B @ sk2 ) ),
inference(pattern_uni,[status(thm)],[2531:[bind(A,$thf( in @ D @ sk4 )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(2627,plain,
! [B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ B @ sk2 ) ),
inference(simp,[status(thm)],[2532]) ).
thf(45816,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ~ $true
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[45771,846]) ).
thf(45817,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[45816]) ).
thf(46083,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ( ( powerset @ sk4 )
!= sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[45817]) ).
thf(46091,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ( ( powerset @ sk4 )
!= sk2 ) ),
inference(simp,[status(thm)],[46083]) ).
thf(8159,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ~ ( in @ ( sk1 @ C @ A ) @ B )
| ( in @ C @ ( powerset @ A ) )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[15,121]) ).
thf(8160,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ ( sk1 @ C @ A ) @ B )
| ( in @ C @ ( powerset @ A ) )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(simp,[status(thm)],[8159]) ).
thf(8161,plain,
! [A: $i] :
( ~ ( in @ ( sk1 @ A @ sk2 ) @ sk3 )
| ( in @ A @ ( powerset @ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[8160:[bind(A,$thf( sk2 )),bind(B,$thf( sk3 ))]]) ).
thf(8351,plain,
! [A: $i] :
( ~ ( in @ ( sk1 @ A @ sk2 ) @ sk3 )
| ( in @ A @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[8161]) ).
thf(41302,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ C ) )
| ~ ( in @ B @ ( powerset @ A ) )
| ~ $true
| ( in @ D @ ( powerset @ sk2 ) )
| ( ( in @ ( sk1 @ B @ C ) @ A )
!= ( in @ ( sk1 @ D @ sk2 ) @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[69,8351]) ).
thf(41303,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ C ) )
| ~ ( in @ B @ ( powerset @ A ) )
| ( in @ D @ ( powerset @ sk2 ) )
| ( ( in @ ( sk1 @ B @ C ) @ A )
!= ( in @ ( sk1 @ D @ sk2 ) @ sk3 ) ) ),
inference(simp,[status(thm)],[41302]) ).
thf(41304,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ sk2 ) )
| ~ ( in @ A @ ( powerset @ sk3 ) )
| ( in @ A @ ( powerset @ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[41303:[bind(A,$thf( sk3 )),bind(B,$thf( B )),bind(C,$thf( sk2 )),bind(D,$thf( B ))]]) ).
thf(41691,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ sk2 ) )
| ~ ( in @ A @ ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[41304]) ).
thf(41847,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( in @ C @ ( powerset @ sk2 ) )
| ~ $true
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ C @ ( powerset @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,41691]) ).
thf(41848,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( in @ C @ ( powerset @ sk2 ) )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ C @ ( powerset @ sk3 ) ) ) ),
inference(simp,[status(thm)],[41847]) ).
thf(41849,plain,
! [A: $i] :
( ( in @ ( powerset @ sk3 ) @ ( powerset @ A ) )
| ( in @ ( sk1 @ ( powerset @ sk3 ) @ A ) @ ( powerset @ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[41848:[bind(A,$thf( E )),bind(B,$thf( powerset @ sk3 )),bind(C,$thf( sk1 @ ( powerset @ sk3 ) @ E ))]]) ).
thf(42202,plain,
! [A: $i] :
( ( in @ ( powerset @ sk3 ) @ ( powerset @ A ) )
| ( in @ ( sk1 @ ( powerset @ sk3 ) @ A ) @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[41849]) ).
thf(47123,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ ( powerset @ sk3 ) @ ( powerset @ A ) )
| ~ $true
| ( in @ C @ ( powerset @ B ) )
| ( ( in @ ( sk1 @ ( powerset @ sk3 ) @ A ) @ ( powerset @ sk2 ) )
!= ( in @ ( sk1 @ C @ B ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[42202,13]) ).
thf(47124,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ ( powerset @ sk3 ) @ ( powerset @ A ) )
| ( in @ C @ ( powerset @ B ) )
| ( ( in @ ( sk1 @ ( powerset @ sk3 ) @ A ) @ ( powerset @ sk2 ) )
!= ( in @ ( sk1 @ C @ B ) @ B ) ) ),
inference(simp,[status(thm)],[47123]) ).
thf(47125,plain,
( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
| ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(pattern_uni,[status(thm)],[47124:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( powerset @ sk2 )),bind(C,$thf( powerset @ sk3 ))]]) ).
thf(47309,plain,
in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ),
inference(simp,[status(thm)],[47125]) ).
thf(47370,plain,
! [A: $i] :
( ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[47309,56]) ).
thf(47371,plain,
! [A: $i] :
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[47370]) ).
thf(47372,plain,
~ ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk3 ) ),
inference(pattern_uni,[status(thm)],[47371:[bind(A,$thf( powerset @ sk3 ))]]) ).
thf(23120,plain,
! [A: $i] :
( ~ $true
| ( in @ ( powerset @ sk3 ) @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk3 ) @ ( powerset @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,21361]) ).
thf(23121,plain,
! [A: $i] :
( ( in @ ( powerset @ sk3 ) @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk3 ) @ ( powerset @ sk3 ) ) ) ),
inference(simp,[status(thm)],[23120]) ).
thf(23198,plain,
! [A: $i] :
( ( in @ ( powerset @ sk3 ) @ sk2 )
| ( A
!= ( powerset @ sk3 ) )
| ( ( powerset @ A )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[23121]) ).
thf(23217,plain,
( ( in @ ( powerset @ sk3 ) @ sk2 )
| ( ( powerset @ ( powerset @ sk3 ) )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[23198]) ).
thf(23783,plain,
( ( ( powerset @ ( powerset @ sk3 ) )
!= ( powerset @ sk3 ) )
| ~ $true
| ( ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ sk3 ) @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[23217,14]) ).
thf(23784,plain,
( ( ( powerset @ ( powerset @ sk3 ) )
!= ( powerset @ sk3 ) )
| ( ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ sk3 ) @ sk2 ) ) ),
inference(simp,[status(thm)],[23783]) ).
thf(23956,plain,
( ( ( powerset @ sk3 )
!= sk3 )
| ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ sk3 ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[23784]) ).
thf(193,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ A @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[15,55]) ).
thf(194,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ A @ sk3 ) ) ),
inference(simp,[status(thm)],[193]) ).
thf(203,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( sk3 != A )
| ( ( powerset @ sk2 )
!= sk3 ) ),
inference(simp,[status(thm)],[194]) ).
thf(211,plain,
( ( in @ sk3 @ sk2 )
| ( ( powerset @ sk2 )
!= sk3 ) ),
inference(simp,[status(thm)],[203]) ).
thf(809,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ sk3 @ sk2 )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[211,56]) ).
thf(810,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ sk3 @ sk2 )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[809]) ).
thf(873,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( sk3 != A )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[810]) ).
thf(898,plain,
( ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[873]) ).
thf(259,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ $true
| ( in @ C @ A )
| ( in @ C @ B )
| D
| ( ( in @ sk4 @ sk2 )
!= ( in @ C @ ( binunion @ A @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[209,16]) ).
thf(260,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ( in @ C @ A )
| ( in @ C @ B )
| D
| ( ( in @ sk4 @ sk2 )
!= ( in @ C @ ( binunion @ A @ B ) ) ) ),
inference(simp,[status(thm)],[259]) ).
thf(292,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( in @ C @ A )
| ( in @ C @ B )
| D
| ( ( powerset @ sk2 )
!= sk3 )
| ( sk4 != C )
| ( ( binunion @ A @ B )
!= sk2 ) ),
inference(simp,[status(thm)],[260]) ).
thf(301,plain,
! [C: $o,B: $i,A: $i] :
( ( in @ sk4 @ A )
| ( in @ sk4 @ B )
| C
| ( ( powerset @ sk2 )
!= sk3 )
| ( ( binunion @ A @ B )
!= sk2 ) ),
inference(simp,[status(thm)],[292]) ).
thf(45947,plain,
( ~ $true
| ( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[45771,836]) ).
thf(45948,plain,
( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[45947]) ).
thf(46065,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= ( powerset @ sk4 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[45948]) ).
thf(46130,plain,
( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= ( powerset @ sk4 ) ),
inference(simp,[status(thm)],[46065]) ).
thf(47354,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ~ $true
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[47309,846]) ).
thf(47355,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[47354]) ).
thf(47548,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ( ( powerset @ sk3 )
!= sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[47355]) ).
thf(47650,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ( ( powerset @ sk3 )
!= sk2 ) ),
inference(simp,[status(thm)],[47548]) ).
thf(35,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ~ ( in @ E @ ( powerset @ D ) )
| ~ $true
| ( in @ F @ D )
| ( ( in @ C @ A )
!= ( in @ F @ E ) ) ),
inference(paramod_ordered,[status(thm)],[20,20]) ).
thf(36,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ~ ( in @ E @ ( powerset @ D ) )
| ( in @ F @ D )
| ( ( in @ C @ A )
!= ( in @ F @ E ) ) ),
inference(simp,[status(thm)],[35]) ).
thf(37,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ~ ( in @ A @ ( powerset @ D ) )
| ( in @ C @ D ) ),
inference(pattern_uni,[status(thm)],[36:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( C ))]]) ).
thf(32,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ~ $true
| ~ ( in @ F @ E )
| ( in @ F @ D )
| ( ( in @ C @ A )
!= ( in @ E @ ( powerset @ D ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,20]) ).
thf(33,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ~ ( in @ F @ E )
| ( in @ F @ D )
| ( ( in @ C @ A )
!= ( in @ E @ ( powerset @ D ) ) ) ),
inference(simp,[status(thm)],[32]) ).
thf(34,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ ( powerset @ D ) ) )
| ~ ( in @ B @ A )
| ~ ( in @ C @ B )
| ( in @ C @ D ) ),
inference(pattern_uni,[status(thm)],[33:[bind(A,$thf( powerset @ G )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( G )),bind(E,$thf( C ))]]) ).
thf(52,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ ( powerset @ D ) ) )
| ~ ( in @ B @ A )
| ~ ( in @ C @ B )
| ( in @ C @ D ) ),
inference(simp,[status(thm)],[34]) ).
thf(346,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[141,14]) ).
thf(347,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[346]) ).
thf(366,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[347]) ).
thf(372,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[366]) ).
thf(322,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ $true
| ~ ( in @ C @ B )
| ( in @ C @ A )
| ( ( in @ sk3 @ sk2 )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[211,20]) ).
thf(323,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ C @ B )
| ( in @ C @ A )
| ( ( in @ sk3 @ sk2 )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(simp,[status(thm)],[322]) ).
thf(339,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ C @ A )
| ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ C @ B )
| ( sk3 != B )
| ( ( powerset @ A )
!= sk2 ) ),
inference(simp,[status(thm)],[323]) ).
thf(344,plain,
! [B: $i,A: $i] :
( ( in @ B @ A )
| ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ B @ sk3 )
| ( ( powerset @ A )
!= sk2 ) ),
inference(simp,[status(thm)],[339]) ).
thf(8926,plain,
! [B: $i,A: $i] :
( ~ $true
| ( in @ B @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ B @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,4471]) ).
thf(8927,plain,
! [B: $i,A: $i] :
( ( in @ B @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ B @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[8926]) ).
thf(8951,plain,
! [B: $i,A: $i] :
( ( in @ B @ sk2 )
| ( A != B )
| ( ( powerset @ A )
!= ( binunion @ sk4 @ sk4 ) ) ),
inference(simp,[status(thm)],[8927]) ).
thf(9018,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( powerset @ A )
!= ( binunion @ sk4 @ sk4 ) ) ),
inference(simp,[status(thm)],[8951]) ).
thf(2694,plain,
! [B: $i,A: $i] :
( ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ B )
| ( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
!= ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[2593,56]) ).
thf(2695,plain,
! [B: $i,A: $i] :
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ B )
| ( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
!= ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[2694]) ).
thf(2696,plain,
~ ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[2695:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ))]]) ).
thf(14801,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk4 @ sk4 ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[9018,2696]) ).
thf(14802,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk4 @ sk4 ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[14801]) ).
thf(14883,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk4 @ sk4 ) )
| ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[14802]) ).
thf(14923,plain,
( ( ( binunion @ sk4 @ sk4 )
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[14883]) ).
thf(33552,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk3 ) )
| ~ ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[32165,56]) ).
thf(33553,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk3 ) )
| ~ ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ B ) ) ),
inference(simp,[status(thm)],[33552]) ).
thf(33554,plain,
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk3 ) )
| ~ ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(pattern_uni,[status(thm)],[33553:[bind(A,$thf( binunion @ sk3 @ sk4 )),bind(B,$thf( sk2 ))]]) ).
thf(2822,plain,
! [A: $i] :
( ~ $true
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,2696]) ).
thf(2823,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[2822]) ).
thf(2845,plain,
! [A: $i] :
( ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( powerset @ A )
!= ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[2823]) ).
thf(2857,plain,
( ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) )
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) ),
inference(simp,[status(thm)],[2845]) ).
thf(45982,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ A @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[45771,55]) ).
thf(45983,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ A @ sk3 ) ) ),
inference(simp,[status(thm)],[45982]) ).
thf(46024,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( powerset @ sk4 )
!= A )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk3 ) ),
inference(simp,[status(thm)],[45983]) ).
thf(46115,plain,
( ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk3 ) ),
inference(simp,[status(thm)],[46024]) ).
thf(7409,plain,
! [A: $i] :
( ~ $true
| ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,6441]) ).
thf(7410,plain,
! [A: $i] :
( ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[7409]) ).
thf(7447,plain,
! [A: $i] :
( ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( A
!= ( powerset @ sk2 ) )
| ( ( powerset @ A )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[7410]) ).
thf(7509,plain,
( ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[7447]) ).
thf(866,plain,
! [B: $i,A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ~ ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[214,56]) ).
thf(867,plain,
! [B: $i,A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ~ ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ B ) ) ),
inference(simp,[status(thm)],[866]) ).
thf(868,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ~ ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(pattern_uni,[status(thm)],[867:[bind(A,$thf( binunion @ sk3 @ sk4 )),bind(B,$thf( sk2 ))]]) ).
thf(47481,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ~ $true
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[47309,868]) ).
thf(47482,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[47481]) ).
thf(47560,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ( ( powerset @ sk3 )
!= sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[47482]) ).
thf(47657,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ( ( powerset @ sk3 )
!= sk2 ) ),
inference(simp,[status(thm)],[47560]) ).
thf(1438,plain,
! [A: $i] :
( ~ $true
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,836]) ).
thf(1439,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[1438]) ).
thf(1464,plain,
! [A: $i] :
( ( A
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( powerset @ A )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[1439]) ).
thf(1479,plain,
( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[1464]) ).
thf(47489,plain,
( ~ $true
| ( in @ ( powerset @ sk3 ) @ sk2 )
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ ( powerset @ sk3 ) @ ( powerset @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[47309,21361]) ).
thf(47490,plain,
( ( in @ ( powerset @ sk3 ) @ sk2 )
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ ( powerset @ sk3 ) @ ( powerset @ sk3 ) ) ) ),
inference(simp,[status(thm)],[47489]) ).
thf(47617,plain,
( ( in @ ( powerset @ sk3 ) @ sk2 )
| ( ( powerset @ sk3 )
!= ( powerset @ sk3 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[47490]) ).
thf(47635,plain,
( ( in @ ( powerset @ sk3 ) @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[47617]) ).
thf(54305,plain,
( ( in @ ( powerset @ sk3 ) @ sk2 )
| ( ( powerset @ sk2 )
!= sk3 ) ),
inference(simp,[status(thm)],[47635]) ).
thf(45990,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk3 ) )
| ~ $true
| ( in @ B @ sk2 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[45771,210]) ).
thf(45991,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk3 ) )
| ( in @ B @ sk2 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ B @ A ) ) ),
inference(simp,[status(thm)],[45990]) ).
thf(45992,plain,
( ~ ( in @ ( powerset @ ( powerset @ sk2 ) ) @ ( powerset @ sk3 ) )
| ( in @ ( powerset @ sk4 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[45991:[bind(A,$thf( powerset @ ( powerset @ sk2 ) )),bind(B,$thf( powerset @ sk4 ))]]) ).
thf(55966,plain,
( ~ $true
| ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( in @ ( powerset @ ( powerset @ sk2 ) ) @ ( powerset @ sk3 ) )
!= ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[47309,45992]) ).
thf(55967,plain,
( ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( in @ ( powerset @ ( powerset @ sk2 ) ) @ ( powerset @ sk3 ) )
!= ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[55966]) ).
thf(56000,plain,
( ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk3 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[55967]) ).
thf(56155,plain,
( ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[56000]) ).
thf(56177,plain,
( ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( powerset @ sk2 )
!= sk3 ) ),
inference(simp,[status(thm)],[56155]) ).
thf(6404,plain,
( ~ $true
| ( ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[6187,14]) ).
thf(6405,plain,
( ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[6404]) ).
thf(6450,plain,
( ( ( binunion @ sk3 @ sk4 )
!= ( binunion @ sk3 @ sk3 ) )
| ( ( powerset @ sk2 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[6405]) ).
thf(6493,plain,
( ( binunion @ sk3 @ sk4 )
!= ( binunion @ sk3 @ sk3 ) ),
inference(simp,[status(thm)],[6450]) ).
thf(6808,plain,
( ( sk3 != sk3 )
| ( sk4 != sk3 ) ),
inference(simp,[status(thm)],[6493]) ).
thf(6809,plain,
sk4 != sk3,
inference(simp,[status(thm)],[6808]) ).
thf(219,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ B @ ( powerset @ A ) )
| ~ $true
| ( in @ C @ A )
| ( ( in @ sk4 @ sk2 )
!= ( in @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[209,20]) ).
thf(220,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ B @ ( powerset @ A ) )
| ( in @ C @ A )
| ( ( in @ sk4 @ sk2 )
!= ( in @ C @ B ) ) ),
inference(simp,[status(thm)],[219]) ).
thf(221,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ sk2 @ ( powerset @ A ) )
| ( in @ sk4 @ A ) ),
inference(pattern_uni,[status(thm)],[220:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk4 ))]]) ).
thf(47,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ $true
| ( in @ C @ A )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[15,20]) ).
thf(48,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ( in @ C @ A )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ C @ B ) ) ),
inference(simp,[status(thm)],[47]) ).
thf(49,plain,
! [A: $i] :
( ~ ( in @ ( powerset @ sk2 ) @ ( powerset @ A ) )
| ( in @ sk3 @ A ) ),
inference(pattern_uni,[status(thm)],[48:[bind(A,$thf( A )),bind(B,$thf( powerset @ sk2 )),bind(C,$thf( sk3 ))]]) ).
thf(2535,plain,
! [C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ B @ B ) @ ( powerset @ B ) )
| ~ $true
| ( in @ sk3 @ C )
| ( A
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[1931,49]) ).
thf(2536,plain,
! [C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ B @ B ) @ ( powerset @ B ) )
| ( in @ sk3 @ C )
| ( A
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ C ) ) ) ),
inference(simp,[status(thm)],[2535]) ).
thf(2537,plain,
! [B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ sk3 @ B ) ),
inference(pattern_uni,[status(thm)],[2536:[bind(A,$thf( in @ ( powerset @ sk2 ) @ ( powerset @ G ) )),bind(B,$thf( B )),bind(C,$thf( G ))]]) ).
thf(2628,plain,
! [B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ sk3 @ B ) ),
inference(simp,[status(thm)],[2537]) ).
thf(8821,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ~ $true
| ( in @ C @ sk2 )
| ( ( in @ sk3 @ B )
!= ( in @ C @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[2628,4471]) ).
thf(8822,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ C @ sk2 )
| ( ( in @ sk3 @ B )
!= ( in @ C @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[8821]) ).
thf(8823,plain,
! [A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ sk3 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[8822:[bind(A,$thf( A )),bind(B,$thf( binunion @ sk4 @ sk4 )),bind(C,$thf( sk3 ))]]) ).
thf(9489,plain,
! [B: $i,A: $i] :
( ~ $true
| ( in @ B @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ B ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,4479]) ).
thf(9490,plain,
! [B: $i,A: $i] :
( ( in @ B @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ B ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[9489]) ).
thf(9498,plain,
! [B: $i,A: $i] :
( ( in @ B @ sk2 )
| ( A
!= ( powerset @ B ) )
| ( ( powerset @ A )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[9490]) ).
thf(9549,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[9498]) ).
thf(15038,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk4 ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[9549,836]) ).
thf(15039,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk4 ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[15038]) ).
thf(15202,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk4 ) )
| ( A
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[15039]) ).
thf(15321,plain,
( ( ( powerset @ ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) ) )
!= ( powerset @ sk4 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[15202]) ).
thf(5278,plain,
! [A: $i] :
( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ A ) )
| $false
| ( in @ ( sk1 @ ( binunion @ sk3 @ sk3 ) @ A ) @ sk2 ) ),
inference(prim_subst,[status(thm)],[1896:[bind(A,$thf( $false ))]]) ).
thf(5328,plain,
! [A: $i] :
( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ A ) )
| ( in @ ( sk1 @ ( binunion @ sk3 @ sk3 ) @ A ) @ sk2 ) ),
inference(simp,[status(thm)],[5278]) ).
thf(248,plain,
! [G: $o,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ~ $true
| ( in @ F @ D )
| ( in @ F @ E )
| G
| ( ( in @ C @ A )
!= ( in @ F @ ( binunion @ D @ E ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,16]) ).
thf(249,plain,
! [G: $o,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ~ ( in @ C @ B )
| ( in @ F @ D )
| ( in @ F @ E )
| G
| ( ( in @ C @ A )
!= ( in @ F @ ( binunion @ D @ E ) ) ) ),
inference(simp,[status(thm)],[248]) ).
thf(250,plain,
! [E: $i,D: $i,C: $o,B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ ( binunion @ D @ E ) ) )
| ~ ( in @ B @ A )
| ( in @ B @ D )
| ( in @ B @ E )
| C ),
inference(pattern_uni,[status(thm)],[249:[bind(A,$thf( binunion @ H @ I )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( H )),bind(E,$thf( I )),bind(F,$thf( C ))]]) ).
thf(312,plain,
! [E: $i,D: $i,C: $o,B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ ( binunion @ D @ E ) ) )
| ~ ( in @ B @ A )
| ( in @ B @ D )
| ( in @ B @ E )
| C ),
inference(simp,[status(thm)],[250]) ).
thf(50,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( powerset @ A ) )
| ( in @ C @ A )
| ( ( in @ C @ B )
!= ( in @ B @ ( powerset @ A ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[20]) ).
thf(51,plain,
! [A: $i] :
( ~ ( in @ ( powerset @ A ) @ ( powerset @ A ) )
| ( in @ ( powerset @ A ) @ A ) ),
inference(pattern_uni,[status(thm)],[50:[bind(A,$thf( D )),bind(B,$thf( powerset @ D )),bind(C,$thf( powerset @ D ))]]) ).
thf(53,plain,
! [A: $i] :
( ~ ( in @ ( powerset @ A ) @ ( powerset @ A ) )
| ( in @ ( powerset @ A ) @ A ) ),
inference(simp,[status(thm)],[51]) ).
thf(1973,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ~ $true
| ( in @ ( powerset @ B ) @ B )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ B ) @ ( powerset @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[367,53]) ).
thf(1974,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ( in @ ( powerset @ B ) @ B )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ B ) @ ( powerset @ B ) ) ) ),
inference(simp,[status(thm)],[1973]) ).
thf(1975,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk2 ) @ sk2 ) )
!= sk4 )
| ( in @ ( powerset @ sk2 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[1974:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk2 ))]]) ).
thf(18387,plain,
( ~ $true
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[18318,14]) ).
thf(18388,plain,
( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[18387]) ).
thf(18494,plain,
( ( ( binunion @ sk4 @ sk4 )
!= ( binunion @ sk3 @ sk4 ) )
| ( ( powerset @ sk2 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[18388]) ).
thf(18550,plain,
( ( binunion @ sk4 @ sk4 )
!= ( binunion @ sk3 @ sk4 ) ),
inference(simp,[status(thm)],[18494]) ).
thf(378,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ~ $true
| ( in @ C @ ( powerset @ B ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( sk1 @ C @ B ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[214,13]) ).
thf(379,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ( in @ C @ ( powerset @ B ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( sk1 @ C @ B ) @ B ) ) ),
inference(simp,[status(thm)],[378]) ).
thf(380,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk3 )
| ( in @ A @ ( powerset @ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[379:[bind(A,$thf( sk1 @ D @ sk2 )),bind(B,$thf( sk2 )),bind(C,$thf( D ))]]) ).
thf(399,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk3 )
| ( in @ A @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[380]) ).
thf(38154,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk3 )
| ~ $true
| ( in @ ( powerset @ B ) @ B )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ B ) @ ( powerset @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[399,53]) ).
thf(38155,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk3 )
| ( in @ ( powerset @ B ) @ B )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ B ) @ ( powerset @ B ) ) ) ),
inference(simp,[status(thm)],[38154]) ).
thf(38156,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk2 ) @ sk2 ) )
!= sk3 )
| ( in @ ( powerset @ sk2 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[38155:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk2 ))]]) ).
thf(9795,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,6441]) ).
thf(9796,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[9795]) ).
thf(9797,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk2 ) @ sk4 ) )
!= sk4 )
| ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[9796:[bind(A,$thf( sk4 )),bind(B,$thf( powerset @ sk2 ))]]) ).
thf(14969,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk4 ) )
| ~ ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[9549,56]) ).
thf(14970,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk4 ) )
| ~ ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ B ) ) ),
inference(simp,[status(thm)],[14969]) ).
thf(14971,plain,
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk4 ) )
| ~ ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(pattern_uni,[status(thm)],[14970:[bind(A,$thf( binunion @ sk3 @ sk4 )),bind(B,$thf( sk2 ))]]) ).
thf(15722,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk4 ) )
| ~ $true
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,14971]) ).
thf(15723,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk4 ) )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[15722]) ).
thf(15771,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk4 ) )
| ( A != sk2 )
| ( ( powerset @ A )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[15723]) ).
thf(15920,plain,
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk4 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[15771]) ).
thf(21257,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk3 ) )
| ~ $true
| ( in @ B @ sk2 )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[15,210]) ).
thf(21258,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk3 ) )
| ( in @ B @ sk2 )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ B @ A ) ) ),
inference(simp,[status(thm)],[21257]) ).
thf(21259,plain,
( ~ ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) )
| ( in @ sk3 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[21258:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk3 ))]]) ).
thf(21996,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( in @ sk3 @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,21259]) ).
thf(21997,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( in @ sk3 @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(simp,[status(thm)],[21996]) ).
thf(21998,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk2 ) @ sk3 ) )
!= sk3 )
| ( in @ sk3 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[21997:[bind(A,$thf( sk3 )),bind(B,$thf( powerset @ sk2 ))]]) ).
thf(817,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ sk4 @ sk2 )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[209,56]) ).
thf(818,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ sk4 @ sk2 )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[817]) ).
thf(886,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( sk4 != A )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[818]) ).
thf(910,plain,
( ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[886]) ).
thf(3427,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ~ $true
| ( in @ D @ ( powerset @ C ) )
| ( ( in @ B @ sk2 )
!= ( in @ ( sk1 @ D @ C ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[2627,13]) ).
thf(3428,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ D @ ( powerset @ C ) )
| ( ( in @ B @ sk2 )
!= ( in @ ( sk1 @ D @ C ) @ C ) ) ),
inference(simp,[status(thm)],[3427]) ).
thf(3429,plain,
! [B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ B @ ( powerset @ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[3428:[bind(A,$thf( A )),bind(B,$thf( sk1 @ E @ sk2 )),bind(C,$thf( sk2 )),bind(D,$thf( E ))]]) ).
thf(3603,plain,
! [B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ B @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[3429]) ).
thf(251,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ $true
| ( in @ C @ A )
| ( in @ C @ B )
| D
| ( ( in @ sk3 @ sk2 )
!= ( in @ C @ ( binunion @ A @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[85,16]) ).
thf(252,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ( in @ C @ A )
| ( in @ C @ B )
| D
| ( ( in @ sk3 @ sk2 )
!= ( in @ C @ ( binunion @ A @ B ) ) ) ),
inference(simp,[status(thm)],[251]) ).
thf(293,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( in @ C @ A )
| ( in @ C @ B )
| D
| ( ( powerset @ sk2 )
!= sk4 )
| ( sk3 != C )
| ( ( binunion @ A @ B )
!= sk2 ) ),
inference(simp,[status(thm)],[252]) ).
thf(302,plain,
! [C: $o,B: $i,A: $i] :
( ( in @ sk3 @ A )
| ( in @ sk3 @ B )
| C
| ( ( powerset @ sk2 )
!= sk4 )
| ( ( binunion @ A @ B )
!= sk2 ) ),
inference(simp,[status(thm)],[293]) ).
thf(23,plain,
( ~ $true
| ( ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ sk3 @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[15,14]) ).
thf(24,plain,
( ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ sk3 @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[23]) ).
thf(26,plain,
( ( ( binunion @ sk3 @ sk4 )
!= sk3 )
| ( ( powerset @ sk2 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[24]) ).
thf(28,plain,
( ( binunion @ sk3 @ sk4 )
!= sk3 ),
inference(simp,[status(thm)],[26]) ).
thf(81,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ A @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[12,54]) ).
thf(82,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ A @ sk4 ) ) ),
inference(simp,[status(thm)],[81]) ).
thf(84,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( sk4 != A )
| ( ( powerset @ sk2 )
!= sk4 ) ),
inference(simp,[status(thm)],[82]) ).
thf(86,plain,
( ( in @ sk4 @ sk2 )
| ( ( powerset @ sk2 )
!= sk4 ) ),
inference(simp,[status(thm)],[84]) ).
thf(145,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ $true
| ~ ( in @ C @ B )
| ( in @ C @ A )
| ( ( in @ sk4 @ sk2 )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[86,20]) ).
thf(146,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ C @ B )
| ( in @ C @ A )
| ( ( in @ sk4 @ sk2 )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(simp,[status(thm)],[145]) ).
thf(157,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ C @ A )
| ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ C @ B )
| ( sk4 != B )
| ( ( powerset @ A )
!= sk2 ) ),
inference(simp,[status(thm)],[146]) ).
thf(160,plain,
! [B: $i,A: $i] :
( ( in @ B @ A )
| ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ B @ sk4 )
| ( ( powerset @ A )
!= sk2 ) ),
inference(simp,[status(thm)],[157]) ).
thf(47465,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ A @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[47309,54]) ).
thf(47466,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ A @ sk4 ) ) ),
inference(simp,[status(thm)],[47465]) ).
thf(47546,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( powerset @ sk3 )
!= A )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk4 ) ),
inference(simp,[status(thm)],[47466]) ).
thf(47649,plain,
( ( in @ ( powerset @ sk3 ) @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk4 ) ),
inference(simp,[status(thm)],[47546]) ).
thf(869,plain,
! [A: $i] :
( ~ ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) )
| ( ( in @ ( binunion @ sk3 @ sk4 ) @ A )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[56]) ).
thf(876,plain,
! [A: $i] :
( ~ ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) )
| ( ( binunion @ sk3 @ sk4 )
!= A )
| ( A
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[869]) ).
thf(900,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
| ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[876]) ).
thf(18009,plain,
! [A: $i] :
( ~ $true
| ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ ( powerset @ sk2 ) ) )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,900]) ).
thf(18010,plain,
! [A: $i] :
( ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ ( powerset @ sk2 ) ) )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[18009]) ).
thf(18075,plain,
! [A: $i] :
( ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ ( powerset @ sk2 ) ) )
| ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( powerset @ A )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[18010]) ).
thf(18091,plain,
( ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ ( powerset @ sk2 ) ) )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[18075]) ).
thf(190,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ~ $true
| ( in @ C @ sk2 )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ C @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[9,55]) ).
thf(191,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( in @ C @ sk2 )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ C @ sk3 ) ) ),
inference(simp,[status(thm)],[190]) ).
thf(192,plain,
! [A: $i] :
( ( in @ sk3 @ ( powerset @ A ) )
| ( in @ ( sk1 @ sk3 @ A ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[191:[bind(A,$thf( E )),bind(B,$thf( sk3 )),bind(C,$thf( sk1 @ sk3 @ E ))]]) ).
thf(207,plain,
! [A: $i] :
( ( in @ sk3 @ ( powerset @ A ) )
| ( in @ ( sk1 @ sk3 @ A ) @ sk2 ) ),
inference(simp,[status(thm)],[192]) ).
thf(8151,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ sk3 @ ( powerset @ A ) )
| ~ ( in @ C @ ( powerset @ B ) )
| ~ $true
| ( in @ D @ ( powerset @ B ) )
| ( ( in @ ( sk1 @ sk3 @ A ) @ sk2 )
!= ( in @ ( sk1 @ D @ B ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[207,121]) ).
thf(8152,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ sk3 @ ( powerset @ A ) )
| ~ ( in @ C @ ( powerset @ B ) )
| ( in @ D @ ( powerset @ B ) )
| ( ( in @ ( sk1 @ sk3 @ A ) @ sk2 )
!= ( in @ ( sk1 @ D @ B ) @ C ) ) ),
inference(simp,[status(thm)],[8151]) ).
thf(8153,plain,
! [A: $i] :
( ( in @ sk3 @ ( powerset @ A ) )
| ~ ( in @ sk2 @ ( powerset @ A ) )
| ( in @ sk3 @ ( powerset @ A ) ) ),
inference(pattern_uni,[status(thm)],[8152:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 )),bind(D,$thf( sk3 ))]]) ).
thf(8349,plain,
! [A: $i] :
( ( in @ sk3 @ ( powerset @ A ) )
| ~ ( in @ sk2 @ ( powerset @ A ) ) ),
inference(simp,[status(thm)],[8153]) ).
thf(13398,plain,
! [B: $i,A: $i] :
( ~ ( in @ sk2 @ ( powerset @ A ) )
| ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ B )
| ( ( in @ sk3 @ ( powerset @ A ) )
!= ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[8349,56]) ).
thf(13399,plain,
! [B: $i,A: $i] :
( ~ ( in @ sk2 @ ( powerset @ A ) )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ B )
| ( ( in @ sk3 @ ( powerset @ A ) )
!= ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[13398]) ).
thf(13400,plain,
( ~ ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 ) ),
inference(pattern_uni,[status(thm)],[13399:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk3 ))]]) ).
thf(45997,plain,
( ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[45771,13400]) ).
thf(45998,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[45997]) ).
thf(46033,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 )
| ( ( powerset @ sk4 )
!= sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[45998]) ).
thf(46118,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 )
| ( ( powerset @ sk4 )
!= sk2 ) ),
inference(simp,[status(thm)],[46033]) ).
thf(279,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ C @ ( binunion @ A @ B ) )
| ( in @ C @ A )
| ( in @ C @ B )
| ( D
!= ( in @ C @ A ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[16]) ).
thf(289,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( binunion @ C @ A ) )
| ( in @ B @ C )
| ( in @ B @ A ) ),
inference(pattern_uni,[status(thm)],[279:[bind(A,$thf( F )),bind(B,$thf( B )),bind(C,$thf( E )),bind(D,$thf( in @ E @ F ))]]) ).
thf(297,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( binunion @ C @ A ) )
| ( in @ B @ C )
| ( in @ B @ A ) ),
inference(simp,[status(thm)],[289]) ).
thf(57,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ~ $true
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,14]) ).
thf(58,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[57]) ).
thf(66,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( ( sk1 @ B @ A )
!= ( binunion @ sk3 @ sk4 ) )
| ( B
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[58]) ).
thf(70,plain,
! [A: $i] :
( ( in @ ( powerset @ sk2 ) @ ( powerset @ A ) )
| ( ( sk1 @ ( powerset @ sk2 ) @ A )
!= ( binunion @ sk3 @ sk4 ) ) ),
inference(simp,[status(thm)],[66]) ).
thf(38212,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk3 )
| ~ $true
| ( in @ sk4 @ B )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[399,43]) ).
thf(38213,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk3 )
| ( in @ sk4 @ B )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ B ) ) ) ),
inference(simp,[status(thm)],[38212]) ).
thf(38214,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk2 ) @ sk2 ) )
!= sk3 )
| ( in @ sk4 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[38213:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk2 ))]]) ).
thf(26561,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,21171]) ).
thf(26562,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(simp,[status(thm)],[26561]) ).
thf(26563,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk2 ) @ sk3 ) )
!= sk3 )
| ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[26562:[bind(A,$thf( sk3 )),bind(B,$thf( powerset @ sk2 ))]]) ).
thf(22013,plain,
! [A: $i] :
( ~ $true
| ( in @ sk3 @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,21259]) ).
thf(22014,plain,
! [A: $i] :
( ( in @ sk3 @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(simp,[status(thm)],[22013]) ).
thf(22077,plain,
! [A: $i] :
( ( in @ sk3 @ sk2 )
| ( A
!= ( powerset @ sk2 ) )
| ( ( powerset @ A )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[22014]) ).
thf(22117,plain,
( ( in @ sk3 @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[22077]) ).
thf(45841,plain,
( ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[45771,12026]) ).
thf(45842,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[45841]) ).
thf(46062,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 )
| ( ( powerset @ sk4 )
!= sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[45842]) ).
thf(46128,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 )
| ( ( powerset @ sk4 )
!= sk2 ) ),
inference(simp,[status(thm)],[46062]) ).
thf(4677,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ~ $true
| ( in @ sk3 @ sk2 )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[214,4339]) ).
thf(4678,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ( in @ sk3 @ sk2 )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[4677]) ).
thf(4715,plain,
! [A: $i] :
( ( in @ sk3 @ sk2 )
| ( ( powerset @ A )
!= sk3 )
| ( A
!= ( powerset @ sk2 ) )
| ( ( powerset @ sk4 )
!= sk2 ) ),
inference(simp,[status(thm)],[4678]) ).
thf(4732,plain,
( ( in @ sk3 @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk3 )
| ( ( powerset @ sk4 )
!= sk2 ) ),
inference(simp,[status(thm)],[4715]) ).
thf(9827,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,14]) ).
thf(9828,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[9827]) ).
thf(9829,plain,
( ( powerset @ ( sk1 @ ( binunion @ sk3 @ sk4 ) @ sk2 ) )
!= sk2 ),
inference(pattern_uni,[status(thm)],[9828:[bind(A,$thf( sk2 )),bind(B,$thf( binunion @ sk3 @ sk4 ))]]) ).
thf(18436,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk3 @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[18318,6485]) ).
thf(18437,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk3 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[18436]) ).
thf(18497,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( binunion @ sk4 @ sk4 )
!= A )
| ( ( binunion @ sk3 @ sk3 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[18437]) ).
thf(18552,plain,
( ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( ( binunion @ sk3 @ sk3 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[18497]) ).
thf(13979,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,13400]) ).
thf(13980,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[13979]) ).
thf(13981,plain,
( ( ( powerset @ ( sk1 @ sk2 @ ( powerset @ sk2 ) ) )
!= ( powerset @ sk2 ) )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 ) ),
inference(pattern_uni,[status(thm)],[13980:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk2 ))]]) ).
thf(18469,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[18318,55]) ).
thf(18470,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ sk3 ) ) ),
inference(simp,[status(thm)],[18469]) ).
thf(18539,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( binunion @ sk4 @ sk4 )
!= A )
| ( ( powerset @ sk2 )
!= sk3 ) ),
inference(simp,[status(thm)],[18470]) ).
thf(18569,plain,
( ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( ( powerset @ sk2 )
!= sk3 ) ),
inference(simp,[status(thm)],[18539]) ).
thf(237,plain,
! [E: $o,D: $i,C: $i,B: $i,A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ~ $true
| ( in @ D @ B )
| ( in @ D @ C )
| E
| ( ( in @ ( sk1 @ sk4 @ A ) @ sk2 )
!= ( in @ D @ ( binunion @ B @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[88,16]) ).
thf(238,plain,
! [E: $o,D: $i,C: $i,B: $i,A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ( in @ D @ B )
| ( in @ D @ C )
| E
| ( ( in @ ( sk1 @ sk4 @ A ) @ sk2 )
!= ( in @ D @ ( binunion @ B @ C ) ) ) ),
inference(simp,[status(thm)],[237]) ).
thf(286,plain,
! [E: $o,D: $i,C: $i,B: $i,A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ( in @ D @ B )
| ( in @ D @ C )
| E
| ( ( sk1 @ sk4 @ A )
!= D )
| ( ( binunion @ B @ C )
!= sk2 ) ),
inference(simp,[status(thm)],[238]) ).
thf(317,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ( in @ ( sk1 @ sk4 @ A ) @ B )
| ( in @ ( sk1 @ sk4 @ A ) @ C )
| D
| ( ( binunion @ B @ C )
!= sk2 ) ),
inference(simp,[status(thm)],[286]) ).
thf(44456,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ ( powerset @ A ) @ sk2 ) )
!= sk4 )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[9377,836]) ).
thf(44457,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ ( powerset @ A ) @ sk2 ) )
!= sk4 )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[44456]) ).
thf(44519,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ ( powerset @ A ) @ sk2 ) )
!= sk4 )
| ( A
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[44457]) ).
thf(44674,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) ) @ sk2 ) )
!= sk4 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[44519]) ).
thf(28400,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ~ $true
| ( in @ D @ ( powerset @ C ) )
| ( ( in @ B @ ( powerset @ sk2 ) )
!= ( in @ ( sk1 @ D @ C ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[3603,13]) ).
thf(28401,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ D @ ( powerset @ C ) )
| ( ( in @ B @ ( powerset @ sk2 ) )
!= ( in @ ( sk1 @ D @ C ) @ C ) ) ),
inference(simp,[status(thm)],[28400]) ).
thf(28402,plain,
! [B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(pattern_uni,[status(thm)],[28401:[bind(A,$thf( A )),bind(B,$thf( sk1 @ E @ ( powerset @ sk2 ) )),bind(C,$thf( powerset @ sk2 )),bind(D,$thf( E ))]]) ).
thf(28767,plain,
! [B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[28402]) ).
thf(847,plain,
! [A: $i] :
( ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[12,56]) ).
thf(848,plain,
! [A: $i] :
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[847]) ).
thf(884,plain,
! [A: $i] :
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( sk4 != A )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[848]) ).
thf(908,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[884]) ).
thf(2023,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[908]) ).
thf(1449,plain,
( ( ( powerset @ sk2 )
!= sk4 )
| ~ $true
| ( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk4 @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[86,836]) ).
thf(1450,plain,
( ( ( powerset @ sk2 )
!= sk4 )
| ( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk4 @ sk2 ) ) ),
inference(simp,[status(thm)],[1449]) ).
thf(1461,plain,
( ( ( powerset @ sk2 )
!= sk4 )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[1450]) ).
thf(20035,plain,
! [A: $i] :
( ~ $true
| ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,18462]) ).
thf(20036,plain,
! [A: $i] :
( ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[20035]) ).
thf(20131,plain,
! [A: $i] :
( ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( A
!= ( powerset @ sk2 ) )
| ( ( powerset @ A )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[20036]) ).
thf(20224,plain,
( ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[20131]) ).
thf(45818,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ sk2 ) )
| ~ $true
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ A @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[45771,40457]) ).
thf(45819,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ sk2 ) )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ A @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[45818]) ).
thf(46082,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ sk2 ) )
| ( ( powerset @ sk4 )
!= A )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[45819]) ).
thf(46090,plain,
( ( in @ ( powerset @ sk4 ) @ ( powerset @ sk2 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[46082]) ).
thf(57162,plain,
( ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk4 ) )
| ~ $true
| ( ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[46090,14]) ).
thf(57163,plain,
( ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk4 ) )
| ( ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[57162]) ).
thf(57593,plain,
( ( ( powerset @ sk2 )
!= sk4 )
| ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ sk4 ) )
| ( ( powerset @ sk2 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[57163]) ).
thf(57673,plain,
( ( ( powerset @ sk2 )
!= sk4 )
| ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[57593]) ).
thf(2567,plain,
! [C: $o,B: $o,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| B
| C ),
inference(prim_subst,[status(thm)],[1931:[bind(A,$thf( C | D ))]]) ).
thf(2597,plain,
! [C: $o,B: $o,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| B
| C ),
inference(cnf,[status(esa)],[2567]) ).
thf(2598,plain,
! [C: $o,B: $o,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| B
| C ),
inference(simp,[status(thm)],[2597]) ).
thf(14781,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk4 @ sk4 ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[9018,836]) ).
thf(14782,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk4 @ sk4 ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[14781]) ).
thf(14826,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk4 @ sk4 ) )
| ( A
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[14782]) ).
thf(14929,plain,
( ( ( binunion @ sk4 @ sk4 )
!= ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[14826]) ).
thf(9844,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk4 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,4370]) ).
thf(9845,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk4 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[9844]) ).
thf(9846,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk4 ) @ sk4 ) )
!= sk4 )
| ( in @ ( powerset @ sk4 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[9845:[bind(A,$thf( sk4 )),bind(B,$thf( powerset @ sk4 ))]]) ).
thf(8924,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[15,4471]) ).
thf(8925,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[8924]) ).
thf(8940,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( sk3 != A )
| ( ( binunion @ sk4 @ sk4 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[8925]) ).
thf(9008,plain,
( ( in @ sk3 @ sk2 )
| ( ( binunion @ sk4 @ sk4 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[8940]) ).
thf(1447,plain,
( ~ $true
| ( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk4 @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[12,836]) ).
thf(1448,plain,
( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk4 @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[1447]) ).
thf(1466,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[1448]) ).
thf(385,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[214,14]) ).
thf(386,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[385]) ).
thf(393,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[386]) ).
thf(398,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[393]) ).
thf(9675,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk3 @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[15,6485]) ).
thf(9676,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk3 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[9675]) ).
thf(9700,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( sk3 != A )
| ( ( binunion @ sk3 @ sk3 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[9676]) ).
thf(9750,plain,
( ( in @ sk3 @ sk2 )
| ( ( binunion @ sk3 @ sk3 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[9700]) ).
thf(15948,plain,
( ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) )
| ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk2 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk4 ) ) ),
inference(eqfactor_ordered,[status(thm)],[15920]) ).
thf(15955,plain,
( ( ( powerset @ sk2 )
!= sk2 )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk2 )
| ( ( powerset @ sk2 )
!= sk4 ) ),
inference(simp,[status(thm)],[15948]) ).
thf(9857,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ~ $true
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,868]) ).
thf(9858,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[9857]) ).
thf(9859,plain,
( ( ( powerset @ ( sk1 @ sk2 @ ( powerset @ sk2 ) ) )
!= ( powerset @ sk2 ) )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 ) ),
inference(pattern_uni,[status(thm)],[9858:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk2 ))]]) ).
thf(11591,plain,
( ( ( sk1 @ sk2 @ ( powerset @ sk2 ) )
!= sk2 )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 ) ),
inference(simp,[status(thm)],[9859]) ).
thf(147,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ B @ ( powerset @ A ) )
| ~ $true
| ( in @ C @ A )
| ( ( in @ sk4 @ sk2 )
!= ( in @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[86,20]) ).
thf(148,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ B @ ( powerset @ A ) )
| ( in @ C @ A )
| ( ( in @ sk4 @ sk2 )
!= ( in @ C @ B ) ) ),
inference(simp,[status(thm)],[147]) ).
thf(149,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ sk2 @ ( powerset @ A ) )
| ( in @ sk4 @ A ) ),
inference(pattern_uni,[status(thm)],[148:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk4 ))]]) ).
thf(165,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ~ ( in @ C @ ( powerset @ B ) )
| ~ $true
| ( in @ D @ B )
| ( ( in @ ( sk1 @ sk4 @ A ) @ sk2 )
!= ( in @ D @ C ) ) ),
inference(paramod_ordered,[status(thm)],[88,20]) ).
thf(166,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ~ ( in @ C @ ( powerset @ B ) )
| ( in @ D @ B )
| ( ( in @ ( sk1 @ sk4 @ A ) @ sk2 )
!= ( in @ D @ C ) ) ),
inference(simp,[status(thm)],[165]) ).
thf(167,plain,
! [B: $i,A: $i] :
( ( in @ sk4 @ ( powerset @ B ) )
| ~ ( in @ sk2 @ ( powerset @ A ) )
| ( in @ ( sk1 @ sk4 @ B ) @ A ) ),
inference(pattern_uni,[status(thm)],[166:[bind(A,$thf( F )),bind(B,$thf( B )),bind(C,$thf( sk2 )),bind(D,$thf( sk1 @ sk4 @ F ))]]) ).
thf(180,plain,
! [B: $i,A: $i] :
( ( in @ sk4 @ ( powerset @ B ) )
| ~ ( in @ sk2 @ ( powerset @ A ) )
| ( in @ ( sk1 @ sk4 @ B ) @ A ) ),
inference(simp,[status(thm)],[167]) ).
thf(269,plain,
! [E: $o,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( in @ D @ B )
| ( in @ D @ C )
| E
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ D @ ( binunion @ B @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,16]) ).
thf(270,plain,
! [E: $o,D: $i,C: $i,B: $i,A: $i] :
( ( in @ D @ B )
| ( in @ D @ C )
| E
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ D @ ( binunion @ B @ C ) ) ) ),
inference(simp,[status(thm)],[269]) ).
thf(288,plain,
! [E: $o,D: $i,C: $i,B: $i,A: $i] :
( ( in @ D @ B )
| ( in @ D @ C )
| E
| ( A != D )
| ( ( powerset @ A )
!= ( binunion @ B @ C ) ) ),
inference(simp,[status(thm)],[270]) ).
thf(296,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( in @ C @ A )
| ( in @ C @ B )
| D
| ( ( powerset @ C )
!= ( binunion @ A @ B ) ) ),
inference(simp,[status(thm)],[288]) ).
thf(173,plain,
! [A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ sk4 @ A ) @ sk2 )
!= ( in @ sk4 @ ( powerset @ A ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[88]) ).
thf(176,plain,
! [A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ( ( sk1 @ sk4 @ A )
!= sk4 )
| ( ( powerset @ A )
!= sk2 ) ),
inference(simp,[status(thm)],[173]) ).
thf(14738,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk4 @ sk4 ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[9018,14]) ).
thf(14739,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk4 @ sk4 ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[14738]) ).
thf(14875,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk4 @ sk4 ) )
| ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[14739]) ).
thf(14915,plain,
( ( ( binunion @ sk4 @ sk4 )
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[14875]) ).
thf(111,plain,
! [B: $i,A: $i] :
( ~ $true
| ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ A )
!= ( in @ sk3 @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[15,13]) ).
thf(112,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ A )
!= ( in @ sk3 @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[111]) ).
thf(115,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( ( sk1 @ B @ A )
!= sk3 )
| ( A
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[112]) ).
thf(118,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) )
| ( ( sk1 @ A @ ( powerset @ sk2 ) )
!= sk3 ) ),
inference(simp,[status(thm)],[115]) ).
thf(9798,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( in @ C @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ C ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,4479]) ).
thf(9799,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( in @ C @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ C ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[9798]) ).
thf(9800,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ ( powerset @ A ) @ sk4 ) )
!= sk4 )
| ( in @ A @ sk2 ) ),
inference(pattern_uni,[status(thm)],[9799:[bind(A,$thf( sk4 )),bind(B,$thf( powerset @ D )),bind(C,$thf( D ))]]) ).
thf(9952,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ ( powerset @ A ) @ sk4 ) )
!= sk4 )
| ( in @ A @ sk2 ) ),
inference(simp,[status(thm)],[9800]) ).
thf(21,plain,
( ~ $true
| ( ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ sk4 @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[12,14]) ).
thf(22,plain,
( ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ sk4 @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[21]) ).
thf(25,plain,
( ( ( binunion @ sk3 @ sk4 )
!= sk4 )
| ( ( powerset @ sk2 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[22]) ).
thf(27,plain,
( ( binunion @ sk3 @ sk4 )
!= sk4 ),
inference(simp,[status(thm)],[25]) ).
thf(4526,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ~ $true
| ( in @ sk4 @ sk2 )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[141,4250]) ).
thf(4527,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ( in @ sk4 @ sk2 )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[4526]) ).
thf(4587,plain,
! [A: $i] :
( ( in @ sk4 @ sk2 )
| ( ( powerset @ A )
!= sk4 )
| ( A
!= ( powerset @ sk2 ) )
| ( ( powerset @ sk4 )
!= sk2 ) ),
inference(simp,[status(thm)],[4527]) ).
thf(4605,plain,
( ( in @ sk4 @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk4 )
| ( ( powerset @ sk4 )
!= sk2 ) ),
inference(simp,[status(thm)],[4587]) ).
thf(65,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ B @ ( powerset @ A ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[9]) ).
thf(68,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( ( sk1 @ B @ A )
!= B )
| ( B
!= ( powerset @ A ) ) ),
inference(simp,[status(thm)],[65]) ).
thf(71,plain,
! [A: $i] :
( ( in @ ( powerset @ A ) @ ( powerset @ A ) )
| ( ( sk1 @ ( powerset @ A ) @ A )
!= ( powerset @ A ) ) ),
inference(simp,[status(thm)],[68]) ).
thf(9614,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk3 @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[6187,6485]) ).
thf(9615,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk3 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[9614]) ).
thf(9727,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( binunion @ sk3 @ sk3 )
!= A )
| ( ( binunion @ sk3 @ sk3 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[9615]) ).
thf(9776,plain,
( ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( ( binunion @ sk3 @ sk3 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[9727]) ).
thf(13452,plain,
! [C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ B @ B ) @ ( powerset @ B ) )
| ( in @ sk3 @ ( powerset @ C ) )
| ~ $true
| ( A
!= ( in @ sk2 @ ( powerset @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[1931,8349]) ).
thf(13453,plain,
! [C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ B @ B ) @ ( powerset @ B ) )
| ( in @ sk3 @ ( powerset @ C ) )
| ( A
!= ( in @ sk2 @ ( powerset @ C ) ) ) ),
inference(simp,[status(thm)],[13452]) ).
thf(13454,plain,
! [B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ sk3 @ ( powerset @ B ) ) ),
inference(pattern_uni,[status(thm)],[13453:[bind(A,$thf( in @ sk2 @ ( powerset @ F ) )),bind(B,$thf( B )),bind(C,$thf( F ))]]) ).
thf(13762,plain,
! [B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ sk3 @ ( powerset @ B ) ) ),
inference(simp,[status(thm)],[13454]) ).
thf(150,plain,
! [B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ $true
| ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ A )
!= ( in @ sk4 @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[86,13]) ).
thf(151,plain,
! [B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ A )
!= ( in @ sk4 @ sk2 ) ) ),
inference(simp,[status(thm)],[150]) ).
thf(156,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( ( powerset @ sk2 )
!= sk4 )
| ( ( sk1 @ B @ A )
!= sk4 )
| ( A != sk2 ) ),
inference(simp,[status(thm)],[151]) ).
thf(159,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ sk2 ) )
| ( ( powerset @ sk2 )
!= sk4 )
| ( ( sk1 @ A @ sk2 )
!= sk4 ) ),
inference(simp,[status(thm)],[156]) ).
thf(4681,plain,
! [A: $i] :
( ~ $true
| ( in @ sk3 @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,4339]) ).
thf(4682,plain,
! [A: $i] :
( ( in @ sk3 @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[4681]) ).
thf(4687,plain,
! [A: $i] :
( ( in @ sk3 @ sk2 )
| ( A
!= ( powerset @ sk2 ) )
| ( ( powerset @ A )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[4682]) ).
thf(4716,plain,
( ( in @ sk3 @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[4687]) ).
thf(6422,plain,
( ~ $true
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[6187,836]) ).
thf(6423,plain,
( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[6422]) ).
thf(6461,plain,
( ( ( binunion @ sk3 @ sk3 )
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[6423]) ).
thf(47539,plain,
( ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 )
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[47309,13400]) ).
thf(47540,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 )
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[47539]) ).
thf(47633,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 )
| ( ( powerset @ sk3 )
!= sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[47540]) ).
thf(47639,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 )
| ( ( powerset @ sk3 )
!= sk2 ) ),
inference(simp,[status(thm)],[47633]) ).
thf(8829,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ~ $true
| ( in @ C @ sk2 )
| ( ( in @ sk4 @ B )
!= ( in @ C @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[2612,4471]) ).
thf(8830,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ C @ sk2 )
| ( ( in @ sk4 @ B )
!= ( in @ C @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[8829]) ).
thf(8831,plain,
! [A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ sk4 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[8830:[bind(A,$thf( A )),bind(B,$thf( binunion @ sk4 @ sk4 )),bind(C,$thf( sk4 ))]]) ).
thf(15981,plain,
! [B: $i,A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk3 @ sk3 ) )
| ~ ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[9769,56]) ).
thf(15982,plain,
! [B: $i,A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk3 @ sk3 ) )
| ~ ( in @ B @ ( powerset @ ( powerset @ sk2 ) ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ B ) ) ),
inference(simp,[status(thm)],[15981]) ).
thf(15983,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= ( binunion @ sk3 @ sk3 ) )
| ~ ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(pattern_uni,[status(thm)],[15982:[bind(A,$thf( binunion @ sk3 @ sk4 )),bind(B,$thf( sk2 ))]]) ).
thf(12072,plain,
! [C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ B @ B ) @ ( powerset @ B ) )
| ( in @ sk4 @ ( powerset @ C ) )
| ~ $true
| ( A
!= ( in @ sk2 @ ( powerset @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[1931,8293]) ).
thf(12073,plain,
! [C: $i,B: $i,A: $o] :
( ( in @ ( binunion @ B @ B ) @ ( powerset @ B ) )
| ( in @ sk4 @ ( powerset @ C ) )
| ( A
!= ( in @ sk2 @ ( powerset @ C ) ) ) ),
inference(simp,[status(thm)],[12072]) ).
thf(12074,plain,
! [B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ sk4 @ ( powerset @ B ) ) ),
inference(pattern_uni,[status(thm)],[12073:[bind(A,$thf( in @ sk2 @ ( powerset @ F ) )),bind(B,$thf( B )),bind(C,$thf( F ))]]) ).
thf(12354,plain,
! [B: $i,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| ( in @ sk4 @ ( powerset @ B ) ) ),
inference(simp,[status(thm)],[12074]) ).
thf(278,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ C @ ( binunion @ A @ B ) )
| ( in @ C @ A )
| ( in @ C @ B )
| ( D
!= ( ~ ( in @ C @ ( binunion @ A @ B ) ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[16]) ).
thf(294,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( binunion @ B @ C ) )
| ( in @ A @ B )
| ( in @ A @ C ) ),
inference(pattern_uni,[status(thm)],[278:[bind(A,$thf( H )),bind(B,$thf( I )),bind(C,$thf( F )),bind(D,$thf( ~ ( in @ F @ ( binunion @ H @ I ) ) ))]]) ).
thf(303,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( binunion @ B @ C ) )
| ( in @ A @ B )
| ( in @ A @ C ) ),
inference(simp,[status(thm)],[294]) ).
thf(7933,plain,
( ( ( binunion @ sk3 @ sk3 )
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[6461]) ).
thf(21729,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( in @ sk4 @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,21034]) ).
thf(21730,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( in @ sk4 @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(simp,[status(thm)],[21729]) ).
thf(21731,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk2 ) @ sk3 ) )
!= sk3 )
| ( in @ sk4 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[21730:[bind(A,$thf( sk3 )),bind(B,$thf( powerset @ sk2 ))]]) ).
thf(29956,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ sk4 @ sk4 ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[18549]) ).
thf(4651,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ~ $true
| ( in @ sk3 @ sk2 )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[141,4339]) ).
thf(4652,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ( in @ sk3 @ sk2 )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[4651]) ).
thf(4707,plain,
! [A: $i] :
( ( in @ sk3 @ sk2 )
| ( ( powerset @ A )
!= sk4 )
| ( A
!= ( powerset @ sk2 ) )
| ( ( powerset @ sk4 )
!= sk2 ) ),
inference(simp,[status(thm)],[4652]) ).
thf(4726,plain,
( ( in @ sk3 @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk4 )
| ( ( powerset @ sk4 )
!= sk2 ) ),
inference(simp,[status(thm)],[4707]) ).
thf(5731,plain,
! [A: $i] :
( ~ $true
| ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk4 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,4370]) ).
thf(5732,plain,
! [A: $i] :
( ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk4 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[5731]) ).
thf(5773,plain,
! [A: $i] :
( ( in @ ( powerset @ sk4 ) @ sk2 )
| ( A
!= ( powerset @ sk4 ) )
| ( ( powerset @ A )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[5732]) ).
thf(5780,plain,
( ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( powerset @ ( powerset @ sk4 ) )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[5773]) ).
thf(1423,plain,
( ( ( powerset @ sk2 )
!= sk3 )
| ~ $true
| ( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk3 @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[211,836]) ).
thf(1424,plain,
( ( ( powerset @ sk2 )
!= sk3 )
| ( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk3 @ sk2 ) ) ),
inference(simp,[status(thm)],[1423]) ).
thf(1471,plain,
( ( ( powerset @ sk2 )
!= sk3 )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[1424]) ).
thf(1445,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[141,836]) ).
thf(1446,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[1445]) ).
thf(1472,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ( A
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[1446]) ).
thf(1474,plain,
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= sk4 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[1472]) ).
thf(47487,plain,
( ~ $true
| ( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[47309,836]) ).
thf(47488,plain,
( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[47487]) ).
thf(47566,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= ( powerset @ sk3 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[47488]) ).
thf(47659,plain,
( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= ( powerset @ sk3 ) ),
inference(simp,[status(thm)],[47566]) ).
thf(23734,plain,
( ( in @ ( powerset @ sk3 ) @ sk2 )
| ( ( powerset @ sk3 )
!= sk3 ) ),
inference(simp,[status(thm)],[23217]) ).
thf(11590,plain,
( ( ( sk1 @ sk2 @ ( powerset @ sk2 ) )
!= sk2 )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 ) ),
inference(simp,[status(thm)],[9791]) ).
thf(45925,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ A @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[45771,54]) ).
thf(45926,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ A @ sk4 ) ) ),
inference(simp,[status(thm)],[45925]) ).
thf(46074,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( powerset @ sk4 )
!= A )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk4 ) ),
inference(simp,[status(thm)],[45926]) ).
thf(46132,plain,
( ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk4 ) ),
inference(simp,[status(thm)],[46074]) ).
thf(239,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ C @ ( binunion @ A @ B ) )
| ( in @ C @ A )
| ( in @ C @ B )
| ~ $true
| ( D
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[16,14]) ).
thf(240,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ C @ ( binunion @ A @ B ) )
| ( in @ C @ A )
| ( in @ C @ B )
| ( D
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[239]) ).
thf(241,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ C @ ( binunion @ A @ B ) )
| ( in @ C @ A )
| ( in @ C @ B ) ),
inference(pattern_uni,[status(thm)],[240:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ))]]) ).
thf(38177,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk3 )
| ~ $true
| ( in @ sk3 @ B )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[399,49]) ).
thf(38178,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk3 )
| ( in @ sk3 @ B )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ B ) ) ) ),
inference(simp,[status(thm)],[38177]) ).
thf(38179,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk2 ) @ sk2 ) )
!= sk3 )
| ( in @ sk3 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[38178:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk2 ))]]) ).
thf(36626,plain,
( ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ ( powerset @ sk2 ) ) )
| ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[18091]) ).
thf(37484,plain,
( ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ sk2 ) )
| ( ( binunion @ sk3 @ sk4 )
!= ( binunion @ sk3 @ sk4 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(eqfactor_ordered,[status(thm)],[36626]) ).
thf(37486,plain,
( ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ sk2 ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[37484]) ).
thf(271,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ~ $true
| ( in @ C @ A )
| ( in @ C @ B )
| D
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ C @ ( binunion @ A @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[12,16]) ).
thf(272,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( in @ C @ A )
| ( in @ C @ B )
| D
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ C @ ( binunion @ A @ B ) ) ) ),
inference(simp,[status(thm)],[271]) ).
thf(290,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( in @ C @ A )
| ( in @ C @ B )
| D
| ( sk4 != C )
| ( ( binunion @ A @ B )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[272]) ).
thf(299,plain,
! [C: $o,B: $i,A: $i] :
( ( in @ sk4 @ A )
| ( in @ sk4 @ B )
| C
| ( ( binunion @ A @ B )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[290]) ).
thf(4556,plain,
! [A: $i] :
( ~ $true
| ( in @ sk4 @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,4250]) ).
thf(4557,plain,
! [A: $i] :
( ( in @ sk4 @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[4556]) ).
thf(4577,plain,
! [A: $i] :
( ( in @ sk4 @ sk2 )
| ( A
!= ( powerset @ sk2 ) )
| ( ( powerset @ A )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[4557]) ).
thf(4598,plain,
( ( in @ sk4 @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk4 ) ) ),
inference(simp,[status(thm)],[4577]) ).
thf(327,plain,
! [B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ $true
| ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ A )
!= ( in @ sk3 @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[211,13]) ).
thf(328,plain,
! [B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ A )
!= ( in @ sk3 @ sk2 ) ) ),
inference(simp,[status(thm)],[327]) ).
thf(337,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( ( powerset @ sk2 )
!= sk3 )
| ( ( sk1 @ B @ A )
!= sk3 )
| ( A != sk2 ) ),
inference(simp,[status(thm)],[328]) ).
thf(342,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ sk2 ) )
| ( ( powerset @ sk2 )
!= sk3 )
| ( ( sk1 @ A @ sk2 )
!= sk3 ) ),
inference(simp,[status(thm)],[337]) ).
thf(774,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ~ $true
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[367,14]) ).
thf(775,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[774]) ).
thf(776,plain,
( ( powerset @ ( sk1 @ ( binunion @ sk3 @ sk4 ) @ sk2 ) )
!= sk4 ),
inference(pattern_uni,[status(thm)],[775:[bind(A,$thf( binunion @ sk3 @ sk4 ))]]) ).
thf(9792,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( in @ sk3 @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,4339]) ).
thf(9793,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( in @ sk3 @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[9792]) ).
thf(9794,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk2 ) @ sk4 ) )
!= sk4 )
| ( in @ sk3 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[9793:[bind(A,$thf( sk4 )),bind(B,$thf( powerset @ sk2 ))]]) ).
thf(18395,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[18318,4471]) ).
thf(18396,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[18395]) ).
thf(18512,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( binunion @ sk4 @ sk4 )
!= A )
| ( ( binunion @ sk4 @ sk4 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[18396]) ).
thf(18561,plain,
( ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( ( binunion @ sk4 @ sk4 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[18512]) ).
thf(93,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ B @ ( powerset @ A ) )
| ~ $true
| ( in @ C @ A )
| ( ( in @ sk3 @ sk2 )
!= ( in @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[85,20]) ).
thf(94,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ B @ ( powerset @ A ) )
| ( in @ C @ A )
| ( ( in @ sk3 @ sk2 )
!= ( in @ C @ B ) ) ),
inference(simp,[status(thm)],[93]) ).
thf(95,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ sk2 @ ( powerset @ A ) )
| ( in @ sk3 @ A ) ),
inference(pattern_uni,[status(thm)],[94:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk3 ))]]) ).
thf(6444,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[6187,55]) ).
thf(6445,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ sk3 ) ) ),
inference(simp,[status(thm)],[6444]) ).
thf(6466,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( binunion @ sk3 @ sk3 )
!= A )
| ( ( powerset @ sk2 )
!= sk3 ) ),
inference(simp,[status(thm)],[6445]) ).
thf(6481,plain,
( ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( ( powerset @ sk2 )
!= sk3 ) ),
inference(simp,[status(thm)],[6466]) ).
thf(6392,plain,
! [A: $i] :
( ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[6187,56]) ).
thf(6393,plain,
! [A: $i] :
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[6392]) ).
thf(6478,plain,
! [A: $i] :
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( binunion @ sk3 @ sk3 )
!= A )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[6393]) ).
thf(6489,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ sk3 @ sk3 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[6478]) ).
thf(8364,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ sk3 @ sk3 ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[6489]) ).
thf(67,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(simp,[status(thm)],[65]) ).
thf(163,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ~ $true
| ~ ( in @ D @ C )
| ( in @ D @ B )
| ( ( in @ ( sk1 @ sk4 @ A ) @ sk2 )
!= ( in @ C @ ( powerset @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[88,20]) ).
thf(164,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ~ ( in @ D @ C )
| ( in @ D @ B )
| ( ( in @ ( sk1 @ sk4 @ A ) @ sk2 )
!= ( in @ C @ ( powerset @ B ) ) ) ),
inference(simp,[status(thm)],[163]) ).
thf(174,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ( in @ D @ B )
| ~ ( in @ D @ C )
| ( ( sk1 @ sk4 @ A )
!= C )
| ( ( powerset @ B )
!= sk2 ) ),
inference(simp,[status(thm)],[164]) ).
thf(182,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ( in @ C @ B )
| ~ ( in @ C @ ( sk1 @ sk4 @ A ) )
| ( ( powerset @ B )
!= sk2 ) ),
inference(simp,[status(thm)],[174]) ).
thf(59,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ~ $true
| ~ ( in @ E @ D )
| ( in @ E @ C )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ D @ ( powerset @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,20]) ).
thf(60,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ~ ( in @ E @ D )
| ( in @ E @ C )
| ( ( in @ ( sk1 @ B @ A ) @ B )
!= ( in @ D @ ( powerset @ C ) ) ) ),
inference(simp,[status(thm)],[59]) ).
thf(61,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ ( powerset @ C ) @ ( powerset @ B ) )
| ~ ( in @ A @ ( sk1 @ ( powerset @ C ) @ B ) )
| ( in @ A @ C ) ),
inference(pattern_uni,[status(thm)],[60:[bind(A,$thf( G )),bind(B,$thf( powerset @ H )),bind(C,$thf( H )),bind(D,$thf( sk1 @ ( powerset @ H ) @ G )),bind(E,$thf( E ))]]) ).
thf(72,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ ( powerset @ C ) @ ( powerset @ B ) )
| ~ ( in @ A @ ( sk1 @ ( powerset @ C ) @ B ) )
| ( in @ A @ C ) ),
inference(simp,[status(thm)],[61]) ).
thf(175,plain,
! [A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ sk4 @ A ) @ sk2 )
!= ( in @ sk4 @ ( powerset @ A ) ) ) ),
inference(simp,[status(thm)],[173]) ).
thf(35927,plain,
! [C: $o,B: $o,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| B
| ~ $true
| ( C
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[2598,14]) ).
thf(35928,plain,
! [C: $o,B: $o,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| B
| ( C
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[35927]) ).
thf(35929,plain,
! [B: $o,A: $i] :
( ( in @ ( binunion @ A @ A ) @ ( powerset @ A ) )
| B ),
inference(pattern_uni,[status(thm)],[35928:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ))]]) ).
thf(9630,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk3 @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[12,6485]) ).
thf(9631,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk3 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[9630]) ).
thf(9721,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( sk4 != A )
| ( ( binunion @ sk3 @ sk3 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[9631]) ).
thf(9770,plain,
( ( in @ sk4 @ sk2 )
| ( ( binunion @ sk3 @ sk3 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[9721]) ).
thf(45162,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ ( powerset @ A ) @ sk4 ) )
!= sk4 )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[9952,14]) ).
thf(45163,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ ( powerset @ A ) @ sk4 ) )
!= sk4 )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[45162]) ).
thf(45339,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ ( powerset @ A ) @ sk4 ) )
!= sk4 )
| ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[45163]) ).
thf(45418,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ sk4 ) )
!= sk4 )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[45339]) ).
thf(45832,plain,
! [A: $i] :
( ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[45771,56]) ).
thf(45833,plain,
! [A: $i] :
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[45832]) ).
thf(45834,plain,
~ ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk4 ) ),
inference(pattern_uni,[status(thm)],[45833:[bind(A,$thf( powerset @ sk4 ))]]) ).
thf(46370,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,45834]) ).
thf(46371,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[46370]) ).
thf(46372,plain,
( ( powerset @ ( sk1 @ ( binunion @ sk3 @ sk4 ) @ sk4 ) )
!= sk4 ),
inference(pattern_uni,[status(thm)],[46371:[bind(A,$thf( sk4 )),bind(B,$thf( binunion @ sk3 @ sk4 ))]]) ).
thf(1453,plain,
( ( ( powerset @ sk2 )
!= sk3 )
| ~ $true
| ( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk4 @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[209,836]) ).
thf(1454,plain,
( ( ( powerset @ sk2 )
!= sk3 )
| ( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk4 @ sk2 ) ) ),
inference(simp,[status(thm)],[1453]) ).
thf(1459,plain,
( ( ( powerset @ sk2 )
!= sk3 )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[1454]) ).
thf(851,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ sk4 @ sk2 )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[86,56]) ).
thf(852,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ sk4 @ sk2 )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[851]) ).
thf(879,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( sk4 != A )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[852]) ).
thf(903,plain,
( ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[879]) ).
thf(827,plain,
! [A: $i] :
( ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[15,56]) ).
thf(828,plain,
! [A: $i] :
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[827]) ).
thf(889,plain,
! [A: $i] :
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( sk3 != A )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[828]) ).
thf(914,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[889]) ).
thf(2226,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[914]) ).
thf(769,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ~ $true
| ( in @ sk4 @ B )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[367,43]) ).
thf(770,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ( in @ sk4 @ B )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ B ) ) ) ),
inference(simp,[status(thm)],[769]) ).
thf(771,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk2 ) @ sk2 ) )
!= sk4 )
| ( in @ sk4 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[770:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk2 ))]]) ).
thf(47916,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,47372]) ).
thf(47917,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk3 ) ) ) ),
inference(simp,[status(thm)],[47916]) ).
thf(47918,plain,
( ( powerset @ ( sk1 @ ( binunion @ sk3 @ sk4 ) @ sk3 ) )
!= sk3 ),
inference(pattern_uni,[status(thm)],[47917:[bind(A,$thf( sk3 )),bind(B,$thf( binunion @ sk3 @ sk4 ))]]) ).
thf(14172,plain,
( ( ( sk1 @ sk2 @ ( powerset @ sk2 ) )
!= sk2 )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 ) ),
inference(simp,[status(thm)],[13981]) ).
thf(8879,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[12,4471]) ).
thf(8880,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ sk4 @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[8879]) ).
thf(8946,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( sk4 != A )
| ( ( binunion @ sk4 @ sk4 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[8880]) ).
thf(9014,plain,
( ( in @ sk4 @ sk2 )
| ( ( binunion @ sk4 @ sk4 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[8946]) ).
thf(280,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ C @ ( binunion @ A @ B ) )
| ( in @ C @ A )
| ( in @ C @ B )
| ( D
!= ( in @ C @ B ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[16]) ).
thf(287,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( binunion @ A @ C ) )
| ( in @ B @ A )
| ( in @ B @ C ) ),
inference(pattern_uni,[status(thm)],[280:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( in @ E @ F ))]]) ).
thf(319,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ ( binunion @ A @ C ) )
| ( in @ B @ A )
| ( in @ B @ C ) ),
inference(simp,[status(thm)],[287]) ).
thf(813,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ sk3 @ sk2 )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[85,56]) ).
thf(814,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( ( in @ sk3 @ sk2 )
!= ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[813]) ).
thf(871,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ A )
| ( sk3 != A )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[814]) ).
thf(896,plain,
( ( ( powerset @ sk2 )
!= sk4 )
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk3 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[871]) ).
thf(2797,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[141,2696]) ).
thf(2798,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[2797]) ).
thf(2839,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk4 )
| ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[2798]) ).
thf(2855,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk4 )
| ( ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[2839]) ).
thf(1457,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[214,836]) ).
thf(1458,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[1457]) ).
thf(1470,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ( A
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[1458]) ).
thf(1481,plain,
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= sk3 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[1470]) ).
thf(15058,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk4 ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[9549,2696]) ).
thf(15059,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk4 ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[15058]) ).
thf(15254,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk4 ) )
| ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[15059]) ).
thf(15358,plain,
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk4 ) )
| ( ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[15254]) ).
thf(47379,plain,
( ~ $true
| ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 )
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[47309,12026]) ).
thf(47380,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 )
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[47379]) ).
thf(47631,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 )
| ( ( powerset @ sk3 )
!= sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[47380]) ).
thf(47638,plain,
( ~ ( in @ ( binunion @ sk3 @ sk4 ) @ sk4 )
| ( ( powerset @ sk3 )
!= sk2 ) ),
inference(simp,[status(thm)],[47631]) ).
thf(2818,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[214,2696]) ).
thf(2819,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[2818]) ).
thf(2836,plain,
! [A: $i] :
( ( ( powerset @ A )
!= sk3 )
| ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[2819]) ).
thf(2853,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ( ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[2836]) ).
thf(34297,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk3 ) )
| ~ $true
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,33554]) ).
thf(34298,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk3 ) )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[34297]) ).
thf(34566,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk3 ) )
| ( A != sk2 )
| ( ( powerset @ A )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[34298]) ).
thf(34668,plain,
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk3 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[34566]) ).
thf(38196,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk3 )
| ~ $true
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[399,836]) ).
thf(38197,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk3 )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[38196]) ).
thf(38318,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk3 )
| ( A
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[38197]) ).
thf(38383,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ sk2 ) )
!= sk3 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[38318]) ).
thf(779,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ~ $true
| ( in @ sk3 @ B )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[367,49]) ).
thf(780,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk4 )
| ( in @ sk3 @ B )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ B ) ) ) ),
inference(simp,[status(thm)],[779]) ).
thf(781,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk2 ) @ sk2 ) )
!= sk4 )
| ( in @ sk3 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[780:[bind(A,$thf( powerset @ sk2 )),bind(B,$thf( sk2 ))]]) ).
thf(217,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ $true
| ~ ( in @ C @ B )
| ( in @ C @ A )
| ( ( in @ sk4 @ sk2 )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[209,20]) ).
thf(218,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ C @ B )
| ( in @ C @ A )
| ( ( in @ sk4 @ sk2 )
!= ( in @ B @ ( powerset @ A ) ) ) ),
inference(simp,[status(thm)],[217]) ).
thf(231,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ C @ A )
| ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ C @ B )
| ( sk4 != B )
| ( ( powerset @ A )
!= sk2 ) ),
inference(simp,[status(thm)],[218]) ).
thf(235,plain,
! [B: $i,A: $i] :
( ( in @ B @ A )
| ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ B @ sk4 )
| ( ( powerset @ A )
!= sk2 ) ),
inference(simp,[status(thm)],[231]) ).
thf(35732,plain,
( ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) )
| ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk2 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk3 ) ) ),
inference(eqfactor_ordered,[status(thm)],[34668]) ).
thf(35746,plain,
( ( ( powerset @ sk2 )
!= sk2 )
| ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk2 )
| ( ( powerset @ sk2 )
!= sk3 ) ),
inference(simp,[status(thm)],[35732]) ).
thf(47522,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ A @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[47309,55]) ).
thf(47523,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ ( powerset @ sk3 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ A @ sk3 ) ) ),
inference(simp,[status(thm)],[47522]) ).
thf(47592,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( powerset @ sk3 )
!= A )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk3 ) ),
inference(simp,[status(thm)],[47523]) ).
thf(47666,plain,
( ( in @ ( powerset @ sk3 ) @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk3 ) ),
inference(simp,[status(thm)],[47592]) ).
thf(33669,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk3 ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[32165,2696]) ).
thf(33670,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk3 ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[33669]) ).
thf(33865,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk3 ) )
| ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[33670]) ).
thf(33977,plain,
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk3 ) )
| ( ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[33865]) ).
thf(113,plain,
! [B: $i,A: $i] :
( ~ $true
| ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ A )
!= ( in @ sk4 @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[12,13]) ).
thf(114,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ B @ A ) @ A )
!= ( in @ sk4 @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[113]) ).
thf(116,plain,
! [B: $i,A: $i] :
( ( in @ B @ ( powerset @ A ) )
| ( ( sk1 @ B @ A )
!= sk4 )
| ( A
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[114]) ).
thf(119,plain,
! [A: $i] :
( ( in @ A @ ( powerset @ ( powerset @ sk2 ) ) )
| ( ( sk1 @ A @ ( powerset @ sk2 ) )
!= sk4 ) ),
inference(simp,[status(thm)],[116]) ).
thf(18438,plain,
( ~ $true
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[18318,836]) ).
thf(18439,plain,
( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[18438]) ).
thf(18491,plain,
( ( ( binunion @ sk4 @ sk4 )
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[18439]) ).
thf(276,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ~ $true
| ( in @ C @ A )
| ( in @ C @ B )
| D
| ( ( in @ sk4 @ sk2 )
!= ( in @ C @ ( binunion @ A @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[86,16]) ).
thf(277,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk4 )
| ( in @ C @ A )
| ( in @ C @ B )
| D
| ( ( in @ sk4 @ sk2 )
!= ( in @ C @ ( binunion @ A @ B ) ) ) ),
inference(simp,[status(thm)],[276]) ).
thf(291,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( in @ C @ A )
| ( in @ C @ B )
| D
| ( ( powerset @ sk2 )
!= sk4 )
| ( sk4 != C )
| ( ( binunion @ A @ B )
!= sk2 ) ),
inference(simp,[status(thm)],[277]) ).
thf(300,plain,
! [C: $o,B: $i,A: $i] :
( ( in @ sk4 @ A )
| ( in @ sk4 @ B )
| C
| ( ( powerset @ sk2 )
!= sk4 )
| ( ( binunion @ A @ B )
!= sk2 ) ),
inference(simp,[status(thm)],[291]) ).
thf(16052,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk3 @ sk3 ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[9769,836]) ).
thf(16053,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk3 @ sk3 ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[16052]) ).
thf(16151,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk3 @ sk3 ) )
| ( A
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[16053]) ).
thf(16186,plain,
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( binunion @ sk3 @ sk3 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[16151]) ).
thf(18426,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[18318,54]) ).
thf(18427,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk4 @ sk4 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ sk4 ) ) ),
inference(simp,[status(thm)],[18426]) ).
thf(18523,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( binunion @ sk4 @ sk4 )
!= A )
| ( ( powerset @ sk2 )
!= sk4 ) ),
inference(simp,[status(thm)],[18427]) ).
thf(18566,plain,
( ( in @ ( binunion @ sk4 @ sk4 ) @ sk2 )
| ( ( powerset @ sk2 )
!= sk4 ) ),
inference(simp,[status(thm)],[18523]) ).
thf(57104,plain,
( ( in @ ( powerset @ sk4 ) @ ( powerset @ sk2 ) )
| ( ( powerset @ sk2 )
!= sk4 ) ),
inference(simp,[status(thm)],[46090]) ).
thf(38115,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk3 )
| ~ $true
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[399,14]) ).
thf(38116,plain,
! [A: $i] :
( ( ( powerset @ ( sk1 @ A @ sk2 ) )
!= sk3 )
| ( ( in @ A @ ( powerset @ sk2 ) )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[38115]) ).
thf(38117,plain,
( ( powerset @ ( sk1 @ ( binunion @ sk3 @ sk4 ) @ sk2 ) )
!= sk3 ),
inference(pattern_uni,[status(thm)],[38116:[bind(A,$thf( binunion @ sk3 @ sk4 ))]]) ).
thf(45941,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ~ $true
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[45771,868]) ).
thf(45942,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk2 @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[45941]) ).
thf(46007,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ( ( powerset @ sk4 )
!= sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[45942]) ).
thf(46104,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ( ( powerset @ sk4 )
!= sk2 ) ),
inference(simp,[status(thm)],[46007]) ).
thf(267,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ~ $true
| ( in @ C @ A )
| ( in @ C @ B )
| D
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ C @ ( binunion @ A @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[15,16]) ).
thf(268,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( in @ C @ A )
| ( in @ C @ B )
| D
| ( ( in @ sk3 @ ( powerset @ sk2 ) )
!= ( in @ C @ ( binunion @ A @ B ) ) ) ),
inference(simp,[status(thm)],[267]) ).
thf(295,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ( in @ C @ A )
| ( in @ C @ B )
| D
| ( sk3 != C )
| ( ( binunion @ A @ B )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[268]) ).
thf(305,plain,
! [C: $o,B: $i,A: $i] :
( ( in @ sk3 @ A )
| ( in @ sk3 @ B )
| C
| ( ( binunion @ A @ B )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[295]) ).
thf(33647,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk3 ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[32165,836]) ).
thf(33648,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk3 ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[33647]) ).
thf(33746,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk3 ) )
| ( A
!= ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[33648]) ).
thf(34058,plain,
( ( ( powerset @ ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) ) )
!= ( powerset @ sk3 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[33746]) ).
thf(324,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ B @ ( powerset @ A ) )
| ~ $true
| ( in @ C @ A )
| ( ( in @ sk3 @ sk2 )
!= ( in @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[211,20]) ).
thf(325,plain,
! [C: $i,B: $i,A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ B @ ( powerset @ A ) )
| ( in @ C @ A )
| ( ( in @ sk3 @ sk2 )
!= ( in @ C @ B ) ) ),
inference(simp,[status(thm)],[324]) ).
thf(326,plain,
! [A: $i] :
( ( ( powerset @ sk2 )
!= sk3 )
| ~ ( in @ sk2 @ ( powerset @ A ) )
| ( in @ sk3 @ A ) ),
inference(pattern_uni,[status(thm)],[325:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk3 ))]]) ).
thf(37485,plain,
( ( ( binunion @ sk3 @ sk4 )
!= ( powerset @ sk2 ) )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[37484]) ).
thf(16072,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk3 @ sk3 ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[9769,2696]) ).
thf(16073,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk3 @ sk3 ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) ) ) ) ),
inference(simp,[status(thm)],[16072]) ).
thf(16155,plain,
! [A: $i] :
( ( ( powerset @ A )
!= ( binunion @ sk3 @ sk3 ) )
| ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[16073]) ).
thf(16190,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= ( binunion @ sk3 @ sk3 ) )
| ( ( binunion @ ( powerset @ sk2 ) @ ( powerset @ sk2 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[16155]) ).
thf(33580,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk3 ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[32165,14]) ).
thf(33581,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk3 ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[33580]) ).
thf(33728,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk3 ) )
| ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[33581]) ).
thf(34046,plain,
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk3 ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[33728]) ).
thf(161,plain,
! [A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ~ $true
| ( ( in @ ( sk1 @ sk4 @ A ) @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[88,14]) ).
thf(162,plain,
! [A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ( ( in @ ( sk1 @ sk4 @ A ) @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[161]) ).
thf(178,plain,
! [A: $i] :
( ( in @ sk4 @ ( powerset @ A ) )
| ( ( sk1 @ sk4 @ A )
!= ( binunion @ sk3 @ sk4 ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[162]) ).
thf(45971,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk4 ) )
| ~ $true
| ( in @ B @ sk2 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[45771,87]) ).
thf(45972,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( powerset @ sk4 ) )
| ( in @ B @ sk2 )
| ( ( in @ ( powerset @ sk4 ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ B @ A ) ) ),
inference(simp,[status(thm)],[45971]) ).
thf(45973,plain,
( ~ ( in @ ( powerset @ ( powerset @ sk2 ) ) @ ( powerset @ sk4 ) )
| ( in @ ( powerset @ sk4 ) @ sk2 ) ),
inference(pattern_uni,[status(thm)],[45972:[bind(A,$thf( powerset @ ( powerset @ sk2 ) )),bind(B,$thf( powerset @ sk4 ))]]) ).
thf(8863,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[6187,4471]) ).
thf(8864,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( in @ ( binunion @ sk3 @ sk3 ) @ ( powerset @ sk2 ) )
!= ( in @ A @ ( binunion @ sk4 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[8863]) ).
thf(8961,plain,
! [A: $i] :
( ( in @ A @ sk2 )
| ( ( binunion @ sk3 @ sk3 )
!= A )
| ( ( binunion @ sk4 @ sk4 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[8864]) ).
thf(8978,plain,
( ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( ( binunion @ sk4 @ sk4 )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[8961]) ).
thf(39548,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ sk2 ) )
!= sk3 )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[38383]) ).
thf(9893,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ~ $true
| ( in @ sk4 @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,4250]) ).
thf(9894,plain,
! [B: $i,A: $i] :
( ( ( powerset @ ( sk1 @ B @ A ) )
!= A )
| ( in @ sk4 @ sk2 )
| ( ( in @ B @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk4 ) ) ) ),
inference(simp,[status(thm)],[9893]) ).
thf(9895,plain,
( ( ( powerset @ ( sk1 @ ( powerset @ sk2 ) @ sk4 ) )
!= sk4 )
| ( in @ sk4 @ sk2 ) ),
inference(pattern_uni,[status(thm)],[9894:[bind(A,$thf( sk4 )),bind(B,$thf( powerset @ sk2 ))]]) ).
thf(14995,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk4 ) )
| ~ $true
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[9549,14]) ).
thf(14996,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk4 ) )
| ( ( in @ A @ sk2 )
!= ( in @ ( binunion @ sk3 @ sk4 ) @ ( powerset @ sk2 ) ) ) ),
inference(simp,[status(thm)],[14995]) ).
thf(15126,plain,
! [A: $i] :
( ( ( powerset @ ( powerset @ A ) )
!= ( powerset @ sk4 ) )
| ( A
!= ( binunion @ sk3 @ sk4 ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[14996]) ).
thf(15273,plain,
( ( ( powerset @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) )
!= ( powerset @ sk4 ) )
| ( ( powerset @ sk2 )
!= sk2 ) ),
inference(simp,[status(thm)],[15126]) ).
thf(1436,plain,
( ~ $true
| ( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk3 @ ( powerset @ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[15,836]) ).
thf(1437,plain,
( ( in @ ( powerset @ ( binunion @ sk3 @ sk4 ) ) @ ( powerset @ ( powerset @ sk2 ) ) )
!= ( in @ sk3 @ ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[1436]) ).
thf(1468,plain,
( ( ( powerset @ ( binunion @ sk3 @ sk4 ) )
!= sk3 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk2 ) ) ),
inference(simp,[status(thm)],[1437]) ).
thf(26020,plain,
! [A: $i] :
( ~ $true
| ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[122,20892]) ).
thf(26021,plain,
! [A: $i] :
( ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( ( in @ A @ ( powerset @ A ) )
!= ( in @ ( powerset @ sk2 ) @ ( powerset @ sk3 ) ) ) ),
inference(simp,[status(thm)],[26020]) ).
thf(26069,plain,
! [A: $i] :
( ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( A
!= ( powerset @ sk2 ) )
| ( ( powerset @ A )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[26021]) ).
thf(26244,plain,
( ( in @ ( binunion @ sk3 @ sk3 ) @ sk2 )
| ( ( powerset @ ( powerset @ sk2 ) )
!= ( powerset @ sk3 ) ) ),
inference(simp,[status(thm)],[26069]) ).
thf(5789,plain,
( ( in @ ( powerset @ sk4 ) @ sk2 )
| ( ( powerset @ sk4 )
!= sk4 ) ),
inference(simp,[status(thm)],[5780]) ).
thf(85269,plain,
$false,
inference(e,[status(thm)],[69,52505,138,101,846,23105,234,40457,9864,88,2612,1469,18107,20014,9965,26810,56176,9791,4339,6495,44348,6441,12774,120,4592,4479,18549,9769,25997,56,21839,142,21171,32165,2627,12585,46091,47372,12026,23956,898,301,46130,47650,37,52,14,372,344,14923,33554,2857,20,46115,1931,4471,7509,47657,1479,54305,8293,211,6187,121,56177,6809,221,8823,15321,5328,312,1975,18550,38156,21445,85,9797,15920,4370,42202,21998,9549,910,46086,3603,302,28,160,47649,18091,46118,297,70,38214,8334,26563,2628,22117,46128,4732,9829,18552,13981,18569,317,9,53,141,21034,44674,28767,2023,1461,20224,57673,8351,2598,14929,13,9846,9008,1466,18462,398,9750,45992,15955,11591,149,180,296,176,6493,8349,14915,118,9952,27,4605,14971,71,12,54,9776,49,13762,86,159,4716,900,9377,6461,47639,8831,15983,12354,318,303,45771,7933,21731,367,29956,2593,4726,5780,21259,1471,20892,40968,140,399,1474,868,47659,47635,23734,11590,46132,3,241,6485,9018,38179,37486,299,4598,209,342,836,776,9794,18561,21361,95,6481,8364,67,182,18318,72,175,43,35929,9770,45418,46107,46372,1459,903,2226,771,47918,2696,87,14172,9014,319,896,2855,1481,4250,15358,56155,139,47638,2853,6489,34668,55,38383,781,235,46090,207,35746,47666,33977,214,119,914,8997,18491,300,16186,47309,18566,57104,1480,38117,23217,46104,305,210,34058,45834,326,37485,9859,36626,16190,908,15,34046,178,45973,8978,39548,9895,122,1088,15273,1468,41691,13400,26244,5789]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU711^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.20 % Computer : n011.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Tue Sep 29 14:13:31 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.65/0.51 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.86/0.61 % [INFO] Parsing done (98ms).
% 0.86/0.62 % [INFO] Running in sequential loop mode.
% 1.42/0.81 % [INFO] eprover registered as external prover.
% 1.42/0.81 % [INFO] Scanning for conjecture ...
% 1.42/0.87 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 1.42/0.89 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 1.42/0.89 % [INFO] Problem is higher-order (TPTP THF).
% 1.42/0.89 % [INFO] Type checking passed.
% 1.42/0.90 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 92.79/21.71 % External prover 'e' found a proof!
% 92.79/21.71 % [INFO] Killing All external provers ...
% 92.79/21.71 % Time passed: 21407ms (effective reasoning time: 21087ms)
% 92.79/21.71 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 92.79/21.71 % Axioms used in derivation (0):
% 92.79/21.71 % No. of inferences in proof: 934
% 92.79/21.72 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 21407 ms resp. 21087 ms w/o parsing
% 89.68/22.02 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 89.68/22.03 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------