%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEU703^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 : n012.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:04 AM UTC 2026
% Result : Theorem 152.42s 41.39s
% Output : Refutation 149.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 13
% Syntax : Number of formulae : 630 ( 109 unt; 0 typ; 12 def)
% Number of atoms : 2587 (1174 equ; 0 cnn)
% Maximal formula atoms : 29 ( 4 avg)
% Number of connectives : 8217 (1328 ~; 963 |; 177 &;5685 @)
% ( 0 <=>; 64 =>; 0 <=; 0 <~>)
% Maximal formula depth : 36 ( 8 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 65 ( 65 >; 0 *; 0 +; 0 <<)
% Number of symbols : 24 ( 21 usr; 18 con; 0-2 aty)
% Number of variables : 1821 ( 659 ^;1156 !; 0 ?;1821 :)
% ( 0 !>; 0 ?*; 0 @-; 6 @+)
% Comments :
%------------------------------------------------------------------------------
thf(in_decl,type,
in: $i > $i > $o ).
thf(emptyset_decl,type,
emptyset: $i ).
thf(setadjoin_decl,type,
setadjoin: $i > $i > $i ).
thf(dsetconstr_decl,type,
dsetconstr: $i > ( $i > $o ) > $i ).
thf(dsetconstrER_decl,type,
dsetconstrER: $o ).
thf(setext_decl,type,
setext: $o ).
thf(uniqinunit_decl,type,
uniqinunit: $o ).
thf(eqinunit_decl,type,
eqinunit: $o ).
thf(in__Cong_decl,type,
in__Cong: $o ).
thf(iftrueProp1_decl,type,
iftrueProp1: $o ).
thf(sk1_decl,type,
sk1: $i > $i > $i ).
thf(sk2_decl,type,
sk2: $i > $i > $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $o ).
thf(sk5_decl,type,
sk5: $i ).
thf(sk6_decl,type,
sk6: $i ).
thf(sk8_decl,type,
sk8: $i ).
thf(sk9_decl,type,
sk9: $i ).
thf(sk11_decl,type,
sk11: $i ).
thf(sk14_decl,type,
sk14: $i ).
thf(sk17_decl,type,
sk17: $i ).
thf(dsetconstrER_def,definition,
( dsetconstrER
= ( ! [A: $i,B: $i > $o,C: $i] :
( ( in @ C @ ( dsetconstr @ A @ B ) )
=> ( B @ C ) ) ) ) ).
thf(setext_def,definition,
( setext
= ( ! [A: $i,B: $i] :
( ! [C: $i] :
( ( in @ C @ A )
=> ( in @ C @ B ) )
=> ( ! [C: $i] :
( ( in @ C @ B )
=> ( in @ C @ A ) )
=> ( A = B ) ) ) ) ) ).
thf(uniqinunit_def,definition,
( uniqinunit
= ( ! [A: $i,B: $i] :
( ( in @ A @ ( setadjoin @ B @ emptyset ) )
=> ( A = B ) ) ) ) ).
thf(eqinunit_def,definition,
( eqinunit
= ( ! [A: $i,B: $i] :
( ( A = B )
=> ( in @ A @ ( setadjoin @ B @ emptyset ) ) ) ) ) ).
thf(in__Cong_def,definition,
( in__Cong
= ( ! [A: $i,B: $i] :
( ( A = B )
=> ! [C: $i,D: $i] :
( ( C = D )
=> ( ( in @ C @ A )
= ( in @ D @ B ) ) ) ) ) ) ).
thf(iftrueProp1_def,definition,
( iftrueProp1
= ( ! [A: $i,B: $o,C: $i] :
( ( in @ C @ A )
=> ! [D: $i] :
( ( in @ D @ A )
=> ( B
=> ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) ) ) ) ) ) ) ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( in @ C @ B )
=> ( in @ C @ A ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( in @ C @ A )
=> ( in @ C @ B ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ! [B: $o,C: $i] :
( ( in @ C @ A )
=> ! [D: $i] :
( ( in @ D @ A )
=> ( B
=> ( ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) )
= ( setadjoin @ C @ emptyset ) ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $o] :
~ ! [B: $i] :
( ( in @ B @ sk3 )
=> ! [C: $i] :
( ( in @ C @ sk3 )
=> ( A
=> ( ( dsetconstr @ sk3
@ ^ [D: $i] :
( ( A
& ( D = B ) )
| ( ~ A
& ( D = C ) ) ) )
= ( setadjoin @ B @ emptyset ) ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: $i] :
~ ( ( in @ A @ sk3 )
=> ! [B: $i] :
( ( in @ B @ sk3 )
=> ( sk4
=> ( ( dsetconstr @ sk3
@ ^ [C: $i] :
( ( sk4
& ( C = A ) )
| ( ~ sk4
& ( C = B ) ) ) )
= ( setadjoin @ A @ emptyset ) ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: $i] :
~ ( ( in @ A @ sk3 )
=> ( sk4
=> ( ( dsetconstr @ sk3
@ ^ [B: $i] :
( ( sk4
& ( B = sk5 ) )
| ( ~ sk4
& ( B = A ) ) ) )
= ( setadjoin @ sk5 @ emptyset ) ) ) ) ) ) ).
thf(1,conjecture,
( dsetconstrER
=> ( setext
=> ( uniqinunit
=> ( eqinunit
=> ( in__Cong
=> ( iftrueProp1
=> ! [A: $i,B: $o,C: $i] :
( ( in @ C @ A )
=> ! [D: $i] :
( ( in @ D @ A )
=> ( B
=> ( ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) )
= ( setadjoin @ C @ emptyset ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',iftrueProp2) ).
thf(2,negated_conjecture,
~ ( dsetconstrER
=> ( setext
=> ( uniqinunit
=> ( eqinunit
=> ( in__Cong
=> ( iftrueProp1
=> ! [A: $i,B: $o,C: $i] :
( ( in @ C @ A )
=> ! [D: $i] :
( ( in @ D @ A )
=> ( B
=> ( ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) )
= ( setadjoin @ C @ emptyset ) ) ) ) ) ) ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ( ! [A: $i,B: $i > $o,C: $i] :
( ( in @ C @ ( dsetconstr @ A @ B ) )
=> ( B @ C ) )
=> ( ! [A: $i,B: $i] :
( ! [C: $i] :
( ( in @ C @ A )
=> ( in @ C @ B ) )
=> ( ! [C: $i] :
( ( in @ C @ B )
=> ( in @ C @ A ) )
=> ( A = B ) ) )
=> ( ! [A: $i,B: $i] :
( ( in @ A @ ( setadjoin @ B @ emptyset ) )
=> ( A = B ) )
=> ( ! [A: $i,B: $i] :
( ( A = B )
=> ( in @ A @ ( setadjoin @ B @ emptyset ) ) )
=> ( ! [A: $i,B: $i] :
( ( A = B )
=> ! [C: $i,D: $i] :
( ( C = D )
=> ( ( in @ C @ A )
= ( in @ D @ B ) ) ) )
=> ( ! [A: $i,B: $o,C: $i] :
( ( in @ C @ A )
=> ! [D: $i] :
( ( in @ D @ A )
=> ( B
=> ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) ) ) ) )
=> ! [A: $i,B: $o,C: $i] :
( ( in @ C @ A )
=> ! [D: $i] :
( ( in @ D @ A )
=> ( B
=> ( ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) )
= ( setadjoin @ C @ emptyset ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
! [Q: $i,P: $i,O: $o,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i > $o,A: $i] :
( ( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ( B @ C ) )
& ( ( in @ ( sk1 @ E @ D ) @ D )
| ( in @ ( sk2 @ E @ D ) @ E )
| ( D = E ) )
& ( ( in @ ( sk1 @ E @ D ) @ D )
| ~ ( in @ ( sk2 @ E @ D ) @ D )
| ( D = E ) )
& ( ~ ( in @ ( sk1 @ E @ D ) @ E )
| ( in @ ( sk2 @ E @ D ) @ E )
| ( D = E ) )
& ( ~ ( in @ ( sk1 @ E @ D ) @ E )
| ~ ( in @ ( sk2 @ E @ D ) @ D )
| ( D = E ) )
& ( ~ ( in @ F @ ( setadjoin @ G @ emptyset ) )
| ( F = G ) )
& ( ( H != I )
| ( in @ H @ ( setadjoin @ I @ emptyset ) ) )
& ( ( J != K )
| ( L != M )
| ( ( in @ L @ J )
= ( in @ M @ K ) ) )
& ( ~ ( in @ P @ N )
| ~ ( in @ Q @ N )
| ~ O
| ( in @ P
@ ( dsetconstr @ N
@ ^ [R: $i] :
( ( O
& ( R = P ) )
| ( ~ O
& ( R = Q ) ) ) ) ) )
& ( in @ sk5 @ sk3 )
& ( in @ sk6 @ sk3 )
& sk4
& ( ( dsetconstr @ sk3
@ ^ [R: $i] :
( ( sk4
& ( R = sk5 ) )
| ( ~ sk4
& ( R = sk6 ) ) ) )
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(cnf,[status(esa)],[3]) ).
thf(16,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( in @ A @ ( setadjoin @ B @ emptyset ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(27,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( in @ A @ ( setadjoin @ B @ emptyset ) ) ),
inference(lifteq,[status(thm)],[16]) ).
thf(28,plain,
! [A: $i] : ( in @ A @ ( setadjoin @ A @ emptyset ) ),
inference(simp,[status(thm)],[27]) ).
thf(5,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A = B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(18,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( in @ A @ ( setadjoin @ B @ emptyset ) ) ),
inference(lifteq,[status(thm)],[5]) ).
thf(19,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( in @ A @ ( setadjoin @ B @ emptyset ) ) ),
inference(simp,[status(thm)],[18]) ).
thf(9,plain,
in @ sk6 @ sk3,
inference(cnfConj,[status(thm)],[4]) ).
thf(14,plain,
! [D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ ( in @ D @ A )
| ~ B
| ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(22,plain,
! [D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ ( in @ D @ A )
| ~ B
| ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) ) ),
inference(simp,[status(thm)],[14]) ).
thf(65,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ A )
| ~ ( in @ C @ A )
| ~ $true
| ( in @ B
@ ( dsetconstr @ A
@ ^ [D: $i] :
( ( $true
& ( D = B ) )
| ( ~ $true
& ( D = C ) ) ) ) ) ),
inference(prim_subst,[status(thm)],[22:[bind(A,$thf( A )),bind(B,$thf( $true ))]]) ).
thf(72,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ A )
| ~ ( in @ C @ A )
| ( in @ B
@ ( dsetconstr @ A
@ ^ [D: $i] : ( D = B ) ) ) ),
inference(simp,[status(thm)],[65]) ).
thf(6022,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ~ ( in @ C @ A )
| ( in @ B
@ ( dsetconstr @ A
@ ^ [D: $i] : ( D = B ) ) )
| ( ( in @ sk6 @ sk3 )
!= ( in @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[9,72]) ).
thf(6023,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ C @ A )
| ( in @ B
@ ( dsetconstr @ A
@ ^ [D: $i] : ( D = B ) ) )
| ( ( in @ sk6 @ sk3 )
!= ( in @ B @ A ) ) ),
inference(simp,[status(thm)],[6022]) ).
thf(6024,plain,
! [A: $i] :
( ~ ( in @ A @ sk3 )
| ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk6 ) ) ) ),
inference(pattern_uni,[status(thm)],[6023:[bind(A,$thf( sk3 )),bind(B,$thf( sk6 ))]]) ).
thf(6121,plain,
! [A: $i] :
( ~ ( in @ A @ sk3 )
| ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk6 ) ) ) ),
inference(simp,[status(thm)],[6024]) ).
thf(30503,plain,
! [A: $i] :
( ~ $true
| ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk6 ) ) )
| ( ( in @ sk6 @ sk3 )
!= ( in @ A @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[9,6121]) ).
thf(30504,plain,
! [A: $i] :
( ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk6 ) ) )
| ( ( in @ sk6 @ sk3 )
!= ( in @ A @ sk3 ) ) ),
inference(simp,[status(thm)],[30503]) ).
thf(30505,plain,
( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk6 ) ) ),
inference(pattern_uni,[status(thm)],[30504:[bind(A,$thf( sk6 ))]]) ).
thf(17,plain,
! [C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ( B @ C ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(329,plain,
! [B: $i,A: $i] :
( ~ ( in @ B
@ ( dsetconstr @ A
@ ^ [C: $i] : $false ) )
| $false ),
inference(prim_subst,[status(thm)],[17:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : $false ))]]) ).
thf(349,plain,
! [B: $i,A: $i] :
~ ( in @ B
@ ( dsetconstr @ A
@ ^ [C: $i] : $false ) ),
inference(simp,[status(thm)],[329]) ).
thf(31858,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk6 ) ) )
!= ( in @ B
@ ( dsetconstr @ A
@ ^ [C: $i] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[30505,349]) ).
thf(31859,plain,
! [B: $i,A: $i] :
( ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk6 ) ) )
!= ( in @ B
@ ( dsetconstr @ A
@ ^ [C: $i] : $false ) ) ),
inference(simp,[status(thm)],[31858]) ).
thf(32090,plain,
! [B: $i,A: $i] :
( ( sk6 != B )
| ( ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk6 ) )
!= ( dsetconstr @ A
@ ^ [C: $i] : $false ) ) ),
inference(simp,[status(thm)],[31859]) ).
thf(32157,plain,
! [A: $i] :
( ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk6 ) )
!= ( dsetconstr @ A
@ ^ [B: $i] : $false ) ),
inference(simp,[status(thm)],[32090]) ).
thf(32265,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B
!= ( dsetconstr @ C
@ ^ [D: $i] : $false ) )
| ( A
!= ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk6 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,32157]) ).
thf(32266,plain,
! [B: $i,A: $i] :
( ~ ( in
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk6 ) )
@ ( setadjoin @ A @ emptyset ) )
| ( A
!= ( dsetconstr @ B
@ ^ [C: $i] : $false ) ) ),
inference(pattern_uni,[status(thm)],[32265:[bind(A,$thf( dsetconstr @ sk3 @ ^ [D: $i] : ( D = sk6 ) )),bind(B,$thf( B )),bind(C,$thf( C ))]]) ).
thf(32293,plain,
! [A: $i] :
~ ( in
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk6 ) )
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset ) ),
inference(simp,[status(thm)],[32266]) ).
thf(35093,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk6 ) )
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,32293]) ).
thf(35094,plain,
! [B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk6 ) )
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset ) ) ),
inference(simp,[status(thm)],[35093]) ).
thf(35280,plain,
! [B: $i,A: $i] :
( ( A
!= ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk6 ) ) )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset ) ) ),
inference(simp,[status(thm)],[35094]) ).
thf(35381,plain,
! [A: $i] :
( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk6 ) )
@ emptyset )
!= ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset ) ),
inference(simp,[status(thm)],[35280]) ).
thf(7,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B )
| ( A = B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(25,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B ) ),
inference(lifteq,[status(thm)],[7]) ).
thf(26,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B ) ),
inference(simp,[status(thm)],[25]) ).
thf(15,plain,
( ( dsetconstr @ sk3
@ ^ [A: $i] :
( ( sk4
& ( A = sk5 ) )
| ( ~ sk4
& ( A = sk6 ) ) ) )
!= ( setadjoin @ sk5 @ emptyset ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(33,plain,
( ( dsetconstr @ sk3
@ ^ [A: $i] :
( ( sk4
& ( A = sk5 ) )
| ( ~ sk4
& ( A = sk6 ) ) ) )
!= ( setadjoin @ sk5 @ emptyset ) ),
inference(lifteq,[status(thm)],[15]) ).
thf(12,plain,
sk4,
inference(cnfConj,[status(thm)],[4]) ).
thf(34,plain,
( ( dsetconstr @ sk3
@ ^ [A: $i] :
( ( $true
& ( A = sk5 ) )
| ( ~ $true
& ( A = sk6 ) ) ) )
!= ( setadjoin @ sk5 @ emptyset ) ),
inference(rewrite,[status(thm)],[33,12]) ).
thf(35,plain,
( ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
!= ( setadjoin @ sk5 @ emptyset ) ),
inference(simp,[status(thm)],[34]) ).
thf(137,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B )
| ( ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = A ) )
!= ( setadjoin @ sk5 @ emptyset ) )
| ( B != sk5 ) ),
inference(paramod_ordered,[status(thm)],[26,35]) ).
thf(138,plain,
! [A: $i] :
( ( in @ ( sk1 @ sk5 @ A ) @ A )
| ( in @ ( sk2 @ sk5 @ A ) @ sk5 )
| ( ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = A ) )
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(pattern_uni,[status(thm)],[137:[bind(A,$thf( A )),bind(B,$thf( sk5 ))]]) ).
thf(296,plain,
! [C: $i,B: $i > $o,A: $i] :
( ~ $true
| ( B @ C )
| ( ( in @ sk6 @ sk3 )
!= ( in @ C @ ( dsetconstr @ A @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,17]) ).
thf(297,plain,
! [C: $i,B: $i > $o,A: $i] :
( ( B @ C )
| ( ( in @ sk6 @ sk3 )
!= ( in @ C @ ( dsetconstr @ A @ B ) ) ) ),
inference(simp,[status(thm)],[296]) ).
thf(333,plain,
! [C: $i,B: $i > $o,A: $i] :
( ( B @ C )
| ( sk6 != C )
| ( ( dsetconstr @ A @ B )
!= sk3 ) ),
inference(simp,[status(thm)],[297]) ).
thf(353,plain,
! [B: $i > $o,A: $i] :
( ( B @ sk6 )
| ( ( dsetconstr @ A @ B )
!= sk3 ) ),
inference(simp,[status(thm)],[333]) ).
thf(1978,plain,
! [B: $i > $o,A: $i] :
( ~ ( B @ sk6 )
| ( ( dsetconstr @ A
@ ^ [C: $i] :
~ ( B @ C ) )
!= sk3 ) ),
inference(prim_subst,[status(thm)],[353:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : ~ ( C @ D ) ))]]) ).
thf(2023,plain,
! [B: $i > $o,A: $i] :
( ~ ( B @ sk6 )
| ( ( dsetconstr @ A
@ ^ [C: $i] :
~ ( B @ C ) )
!= sk3 ) ),
inference(cnf,[status(esa)],[1978]) ).
thf(2024,plain,
! [B: $i > $o,A: $i] :
( ~ ( B @ sk6 )
| ( ( dsetconstr @ A
@ ^ [C: $i] :
~ ( B @ C ) )
!= sk3 ) ),
inference(simp,[status(thm)],[2023]) ).
thf(26379,plain,
! [B: $i > $o,A: $i] :
( ~ $true
| ( ( dsetconstr @ A
@ ^ [C: $i] :
~ ( B @ C ) )
!= sk3 )
| ( ( in @ sk6 @ sk3 )
!= ( B @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[9,2024]) ).
thf(26380,plain,
! [B: $i > $o,A: $i] :
( ( ( dsetconstr @ A
@ ^ [C: $i] :
~ ( B @ C ) )
!= sk3 )
| ( ( in @ sk6 @ sk3 )
!= ( B @ sk6 ) ) ),
inference(simp,[status(thm)],[26379]) ).
thf(26480,plain,
! [A: $i] :
( ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B @ sk3 ) )
!= sk3 ),
inference(pre_uni,[status(thm)],[26380:[bind(A,$thf( A )),bind(B,$thf( ^ [C: $i] : ( in @ C @ sk3 ) ))]]) ).
thf(27384,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B != sk3 )
| ( A
!= ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ D @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,26480]) ).
thf(27385,plain,
! [B: $i,A: $i] :
( ~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ sk3 ) )
@ ( setadjoin @ A @ emptyset ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[27384:[bind(A,$thf( dsetconstr @ D @ ^ [E: $i] : ~ ( in @ E @ sk3 ) )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(27405,plain,
! [A: $i] :
~ ( in
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B @ sk3 ) )
@ ( setadjoin @ sk3 @ emptyset ) ),
inference(simp,[status(thm)],[27385]) ).
thf(27449,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ sk3 ) )
@ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,27405]) ).
thf(27450,plain,
! [B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ sk3 ) )
@ ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[27449]) ).
thf(27597,plain,
! [B: $i,A: $i] :
( ( A
!= ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ sk3 ) ) )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[27450]) ).
thf(27664,plain,
! [A: $i] :
( ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B @ sk3 ) )
@ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ),
inference(simp,[status(thm)],[27597]) ).
thf(31830,plain,
! [B: $i > $o,A: $i] :
( ~ $true
| ( ( dsetconstr @ A
@ ^ [C: $i] :
~ ( B @ C ) )
!= sk3 )
| ( ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk6 ) ) )
!= ( B @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[30505,2024]) ).
thf(31831,plain,
! [B: $i > $o,A: $i] :
( ( ( dsetconstr @ A
@ ^ [C: $i] :
~ ( B @ C ) )
!= sk3 )
| ( ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk6 ) ) )
!= ( B @ sk6 ) ) ),
inference(simp,[status(thm)],[31830]) ).
thf(32098,plain,
! [A: $i] :
( ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = B ) ) ) )
!= sk3 ),
inference(pre_uni,[status(thm)],[31831:[bind(A,$thf( A )),bind(B,$thf( ^ [C: $i] : ( in @ sk6 @ ( dsetconstr @ sk3 @ ^ [D: $i] : ( D = C ) ) ) ))]]) ).
thf(46,plain,
! [D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ $true
| ~ B
| ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) )
| ( ( in @ sk6 @ sk3 )
!= ( in @ D @ A ) ) ),
inference(paramod_ordered,[status(thm)],[9,22]) ).
thf(47,plain,
! [D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ B
| ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) )
| ( ( in @ sk6 @ sk3 )
!= ( in @ D @ A ) ) ),
inference(simp,[status(thm)],[46]) ).
thf(48,plain,
! [B: $i,A: $o] :
( ~ ( in @ B @ sk3 )
| ~ A
| ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] :
( ( A
& ( C = B ) )
| ( ~ A
& ( C = sk6 ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[47:[bind(A,$thf( sk3 )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( sk6 ))]]) ).
thf(88,plain,
! [B: $i,A: $o] :
( ~ ( in @ B @ sk3 )
| ~ A
| ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] :
( ( A
& ( C = B ) )
| ( ~ A
& ( C = sk6 ) ) ) ) ) ),
inference(simp,[status(thm)],[48]) ).
thf(32100,plain,
! [A: $i] :
( ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = B ) ) ) )
!= sk3 ),
inference(pre_uni,[status(thm)],[31831:[bind(A,$thf( A )),bind(B,$thf( ^ [C: $i] : ( in @ C @ ( dsetconstr @ sk3 @ ^ [D: $i] : ( D = C ) ) ) ))]]) ).
thf(32387,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B != sk3 )
| ( A
!= ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ D
@ ( dsetconstr @ sk3
@ ^ [E: $i] : ( E = D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,32100]) ).
thf(32388,plain,
! [B: $i,A: $i] :
( ~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) )
@ ( setadjoin @ A @ emptyset ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[32387:[bind(A,$thf( dsetconstr @ D @ ^ [E: $i] : ~ ( in @ E @ ( dsetconstr @ sk3 @ ^ [F: $i] : ( F = E ) ) ) )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(32398,plain,
! [A: $i] :
~ ( in
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = B ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ),
inference(simp,[status(thm)],[32388]) ).
thf(375,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( in @ sk6 @ sk3 )
!= ( in @ B
@ ( dsetconstr @ A
@ ^ [C: $i] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,349]) ).
thf(376,plain,
! [B: $i,A: $i] :
( ( in @ sk6 @ sk3 )
!= ( in @ B
@ ( dsetconstr @ A
@ ^ [C: $i] : $false ) ) ),
inference(simp,[status(thm)],[375]) ).
thf(397,plain,
! [B: $i,A: $i] :
( ( sk6 != B )
| ( ( dsetconstr @ A
@ ^ [C: $i] : $false )
!= sk3 ) ),
inference(simp,[status(thm)],[376]) ).
thf(410,plain,
! [A: $i] :
( ( dsetconstr @ A
@ ^ [B: $i] : $false )
!= sk3 ),
inference(simp,[status(thm)],[397]) ).
thf(425,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A != sk3 )
| ( B
!= ( dsetconstr @ C
@ ^ [D: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[19,410]) ).
thf(426,plain,
! [B: $i,A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[425:[bind(A,$thf( A )),bind(B,$thf( dsetconstr @ D @ ^ [E: $i] : $false )),bind(C,$thf( D ))]]) ).
thf(431,plain,
! [A: $i] :
~ ( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset ) ),
inference(simp,[status(thm)],[426]) ).
thf(1352,plain,
! [D: $i,C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ~ $true
| ( ( B @ C )
!= ( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ D
@ ^ [E: $i] : $false )
@ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,431]) ).
thf(1353,plain,
! [D: $i,C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ( ( B @ C )
!= ( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ D
@ ^ [E: $i] : $false )
@ emptyset ) ) ) ),
inference(simp,[status(thm)],[1352]) ).
thf(1378,plain,
! [B: $i > $i,A: $i] :
~ ( in @ emptyset
@ ( dsetconstr @ A
@ ^ [C: $i] :
( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ ( B @ C )
@ ^ [D: $i] : $false )
@ C ) ) ) ),
inference(pre_uni,[status(thm)],[1353:[bind(A,$thf( A )),bind(B,$thf( ^ [F: $i] : ( in @ sk3 @ ( setadjoin @ ( dsetconstr @ ( I @ F ) @ ^ [G: $i] : $false ) @ F ) ) )),bind(C,$thf( emptyset )),bind(D,$thf( I @ emptyset ))]]) ).
thf(1401,plain,
! [B: $i > $i,A: $i] :
~ ( in @ emptyset
@ ( dsetconstr @ A
@ ^ [C: $i] :
( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ ( B @ C )
@ ^ [D: $i] : $false )
@ C ) ) ) ),
inference(simp,[status(thm)],[1378]) ).
thf(11235,plain,
! [C: $i > $i,B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ emptyset
@ ( dsetconstr @ B
@ ^ [D: $i] :
( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ ( C @ D )
@ ^ [E: $i] : $false )
@ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,1401]) ).
thf(11236,plain,
! [C: $i > $i,B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ emptyset
@ ( dsetconstr @ B
@ ^ [D: $i] :
( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ ( C @ D )
@ ^ [E: $i] : $false )
@ D ) ) ) ) ),
inference(simp,[status(thm)],[11235]) ).
thf(11326,plain,
! [C: $i > $i,B: $i,A: $i] :
( ( A != emptyset )
| ( ( setadjoin @ A @ emptyset )
!= ( dsetconstr @ B
@ ^ [D: $i] :
( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ ( C @ D )
@ ^ [E: $i] : $false )
@ D ) ) ) ) ),
inference(simp,[status(thm)],[11236]) ).
thf(11352,plain,
! [B: $i > $i,A: $i] :
( ( dsetconstr @ A
@ ^ [C: $i] :
( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ ( B @ C )
@ ^ [D: $i] : $false )
@ C ) ) )
!= ( setadjoin @ emptyset @ emptyset ) ),
inference(simp,[status(thm)],[11326]) ).
thf(32196,plain,
! [A: $i] :
( ( sk3 != A )
| ( ( ^ [B: $i] : ( B = sk6 ) )
!= ( ^ [B: $i] : $false ) ) ),
inference(simp,[status(thm)],[32157]) ).
thf(32286,plain,
( ( ^ [A: $i] : ( A = sk6 ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[32196]) ).
thf(32328,plain,
sk8 = sk6,
inference(func_ext,[status(esa)],[32286]) ).
thf(32349,plain,
sk8 = sk6,
inference(lifteq,[status(thm)],[32328]) ).
thf(32521,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B = sk6 )
| ( A != sk8 ) ),
inference(paramod_ordered,[status(thm)],[19,32349]) ).
thf(32522,plain,
! [A: $i] :
( ~ ( in @ sk8 @ ( setadjoin @ A @ emptyset ) )
| ( A = sk6 ) ),
inference(pattern_uni,[status(thm)],[32521:[bind(A,$thf( sk8 ))]]) ).
thf(32528,plain,
! [A: $i] :
( ~ ( in @ sk8 @ ( setadjoin @ A @ emptyset ) )
| ( A = sk6 ) ),
inference(simp,[status(thm)],[32522]) ).
thf(35807,plain,
! [A: $i] :
( ~ ( in @ sk6 @ ( setadjoin @ A @ emptyset ) )
| ( A = sk6 ) ),
inference(rewrite,[status(thm)],[32528,32349]) ).
thf(36653,plain,
! [A: $i] :
( ~ ( in @ sk6 @ ( setadjoin @ A @ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk6 )
| ( A
!= ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) ) ) ),
inference(paramod_ordered,[status(thm)],[35807,35]) ).
thf(36654,plain,
( ~ ( in @ sk6
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk6 ) ),
inference(pattern_uni,[status(thm)],[36653:[bind(A,$thf( dsetconstr @ sk3 @ ^ [B: $i] : ( B = sk5 ) ))]]) ).
thf(13,plain,
in @ sk5 @ sk3,
inference(cnfConj,[status(thm)],[4]) ).
thf(5976,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ~ ( in @ C @ A )
| ( in @ B
@ ( dsetconstr @ A
@ ^ [D: $i] : ( D = B ) ) )
| ( ( in @ sk5 @ sk3 )
!= ( in @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[13,72]) ).
thf(5977,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ C @ A )
| ( in @ B
@ ( dsetconstr @ A
@ ^ [D: $i] : ( D = B ) ) )
| ( ( in @ sk5 @ sk3 )
!= ( in @ B @ A ) ) ),
inference(simp,[status(thm)],[5976]) ).
thf(5978,plain,
! [A: $i] :
( ~ ( in @ A @ sk3 )
| ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) ) ) ),
inference(pattern_uni,[status(thm)],[5977:[bind(A,$thf( sk3 )),bind(B,$thf( sk5 ))]]) ).
thf(6152,plain,
! [A: $i] :
( ~ ( in @ A @ sk3 )
| ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) ) ) ),
inference(simp,[status(thm)],[5978]) ).
thf(53196,plain,
! [A: $i] :
( ~ $true
| ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) ) )
| ( ( in @ sk6 @ sk3 )
!= ( in @ A @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[9,6152]) ).
thf(53197,plain,
! [A: $i] :
( ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) ) )
| ( ( in @ sk6 @ sk3 )
!= ( in @ A @ sk3 ) ) ),
inference(simp,[status(thm)],[53196]) ).
thf(53198,plain,
( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) ) ),
inference(pattern_uni,[status(thm)],[53197:[bind(A,$thf( sk6 ))]]) ).
thf(54423,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) )
!= ( in @ B
@ ( dsetconstr @ A
@ ^ [C: $i] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[53198,349]) ).
thf(54424,plain,
! [B: $i,A: $i] :
( ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) )
!= ( in @ B
@ ( dsetconstr @ A
@ ^ [C: $i] : $false ) ) ),
inference(simp,[status(thm)],[54423]) ).
thf(54750,plain,
! [B: $i,A: $i] :
( ( sk5 != B )
| ( ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
!= ( dsetconstr @ A
@ ^ [C: $i] : $false ) ) ),
inference(simp,[status(thm)],[54424]) ).
thf(54836,plain,
! [A: $i] :
( ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
!= ( dsetconstr @ A
@ ^ [B: $i] : $false ) ),
inference(simp,[status(thm)],[54750]) ).
thf(188,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( in @ sk5 @ B )
| ( A != sk3 ) ),
inference(paramod_ordered,[status(thm)],[19,13]) ).
thf(189,plain,
! [A: $i] :
( ~ ( in @ sk3 @ ( setadjoin @ A @ emptyset ) )
| ( in @ sk5 @ A ) ),
inference(pattern_uni,[status(thm)],[188:[bind(A,$thf( sk3 ))]]) ).
thf(269,plain,
! [A: $i] :
( ~ ( in @ sk3 @ ( setadjoin @ A @ emptyset ) )
| ( in @ sk5 @ A ) ),
inference(simp,[status(thm)],[189]) ).
thf(32523,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A = sk6 )
| ( B != sk8 ) ),
inference(paramod_ordered,[status(thm)],[19,32349]) ).
thf(32524,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ sk8 @ emptyset ) )
| ( A = sk6 ) ),
inference(pattern_uni,[status(thm)],[32523:[bind(A,$thf( A )),bind(B,$thf( sk8 ))]]) ).
thf(32530,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ sk6 @ emptyset ) )
| ( A = sk6 ) ),
inference(rewrite,[status(thm)],[32524,32349]) ).
thf(32556,plain,
! [B: $i,A: $i] :
( ~ ( in @ sk3 @ ( setadjoin @ A @ emptyset ) )
| ~ $true
| ( B = sk6 )
| ( ( in @ sk5 @ A )
!= ( in @ B @ ( setadjoin @ sk6 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[269,32530]) ).
thf(32557,plain,
! [B: $i,A: $i] :
( ~ ( in @ sk3 @ ( setadjoin @ A @ emptyset ) )
| ( B = sk6 )
| ( ( in @ sk5 @ A )
!= ( in @ B @ ( setadjoin @ sk6 @ emptyset ) ) ) ),
inference(simp,[status(thm)],[32556]) ).
thf(32558,plain,
( ~ ( in @ sk3 @ ( setadjoin @ ( setadjoin @ sk6 @ emptyset ) @ emptyset ) )
| ( sk6 = sk5 ) ),
inference(pattern_uni,[status(thm)],[32557:[bind(A,$thf( setadjoin @ sk6 @ emptyset )),bind(B,$thf( sk5 ))]]) ).
thf(298,plain,
! [C: $i,B: $i > $o,A: $i] :
( ~ $true
| ( B @ C )
| ( ( in @ sk5 @ sk3 )
!= ( in @ C @ ( dsetconstr @ A @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[13,17]) ).
thf(299,plain,
! [C: $i,B: $i > $o,A: $i] :
( ( B @ C )
| ( ( in @ sk5 @ sk3 )
!= ( in @ C @ ( dsetconstr @ A @ B ) ) ) ),
inference(simp,[status(thm)],[298]) ).
thf(335,plain,
! [C: $i,B: $i > $o,A: $i] :
( ( B @ C )
| ( sk5 != C )
| ( ( dsetconstr @ A @ B )
!= sk3 ) ),
inference(simp,[status(thm)],[299]) ).
thf(355,plain,
! [B: $i > $o,A: $i] :
( ( B @ sk5 )
| ( ( dsetconstr @ A @ B )
!= sk3 ) ),
inference(simp,[status(thm)],[335]) ).
thf(2085,plain,
! [B: $i > $o,A: $i] :
( ~ ( B @ sk5 )
| ( ( dsetconstr @ A
@ ^ [C: $i] :
~ ( B @ C ) )
!= sk3 ) ),
inference(prim_subst,[status(thm)],[355:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : ~ ( C @ D ) ))]]) ).
thf(2113,plain,
! [B: $i > $o,A: $i] :
( ~ ( B @ sk5 )
| ( ( dsetconstr @ A
@ ^ [C: $i] :
~ ( B @ C ) )
!= sk3 ) ),
inference(cnf,[status(esa)],[2085]) ).
thf(2114,plain,
! [B: $i > $o,A: $i] :
( ~ ( B @ sk5 )
| ( ( dsetconstr @ A
@ ^ [C: $i] :
~ ( B @ C ) )
!= sk3 ) ),
inference(simp,[status(thm)],[2113]) ).
thf(202,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B
!= ( setadjoin @ sk5 @ emptyset ) )
| ( A
!= ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,35]) ).
thf(203,plain,
! [A: $i] :
( ~ ( in
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ ( setadjoin @ A @ emptyset ) )
| ( A
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(pattern_uni,[status(thm)],[202:[bind(A,$thf( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) )),bind(B,$thf( B ))]]) ).
thf(243,plain,
~ ( in
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ),
inference(simp,[status(thm)],[203]) ).
thf(556,plain,
! [C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ~ $true
| ( ( B @ C )
!= ( in
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) )
@ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,243]) ).
thf(557,plain,
! [C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ( ( B @ C )
!= ( in
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) )
@ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ) ) ),
inference(simp,[status(thm)],[556]) ).
thf(597,plain,
! [A: $i] :
~ ( in @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
@ ( dsetconstr @ A
@ ( in
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) ) ) ) ),
inference(pre_uni,[status(thm)],[557:[bind(A,$thf( A )),bind(B,$thf( in @ ( dsetconstr @ sk3 @ ^ [D: $i] : ( D = sk5 ) ) )),bind(C,$thf( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ))]]) ).
thf(54928,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B
!= ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) ) )
| ( A
!= ( dsetconstr @ C
@ ^ [D: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[19,54836]) ).
thf(54929,plain,
! [B: $i,A: $i] :
( ~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ ( setadjoin @ A @ emptyset ) )
| ( A
!= ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) ) ),
inference(pattern_uni,[status(thm)],[54928:[bind(A,$thf( dsetconstr @ D @ ^ [E: $i] : $false )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(54955,plain,
! [A: $i] :
~ ( in
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset ) ),
inference(simp,[status(thm)],[54929]) ).
thf(208,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A
!= ( setadjoin @ sk5 @ emptyset ) )
| ( B
!= ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,35]) ).
thf(209,plain,
! [A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset ) )
| ( A
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(pattern_uni,[status(thm)],[208:[bind(A,$thf( A )),bind(B,$thf( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) ))]]) ).
thf(246,plain,
~ ( in @ ( setadjoin @ sk5 @ emptyset )
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset ) ),
inference(simp,[status(thm)],[209]) ).
thf(660,plain,
! [C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ~ $true
| ( ( B @ C )
!= ( in @ ( setadjoin @ sk5 @ emptyset )
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) )
@ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,246]) ).
thf(661,plain,
! [C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ( ( B @ C )
!= ( in @ ( setadjoin @ sk5 @ emptyset )
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) )
@ emptyset ) ) ) ),
inference(simp,[status(thm)],[660]) ).
thf(698,plain,
! [A: $i] :
~ ( in
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ ( dsetconstr @ A
@ ^ [B: $i] : ( in @ ( setadjoin @ sk5 @ emptyset ) @ ( setadjoin @ B @ emptyset ) ) ) ),
inference(pre_uni,[status(thm)],[661:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : ( in @ ( setadjoin @ sk5 @ emptyset ) @ ( setadjoin @ D @ emptyset ) ) )),bind(C,$thf( dsetconstr @ sk3 @ ^ [D: $i] : ( D = sk5 ) ))]]) ).
thf(324,plain,
! [C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ( ( B @ C )
!= ( ~ ( in @ C @ ( dsetconstr @ A @ B ) ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[17]) ).
thf(340,plain,
! [A: $i] :
~ ( in
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B @ B ) )
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B @ B ) ) ),
inference(pre_uni,[status(thm)],[324:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : ~ ( in @ D @ D ) )),bind(C,$thf( dsetconstr @ A @ ^ [D: $i] : ~ ( in @ D @ D ) ))]]) ).
thf(54333,plain,
! [B: $i > $o,A: $i] :
( ~ $true
| ( ( dsetconstr @ A
@ ^ [C: $i] :
~ ( B @ C ) )
!= sk3 )
| ( ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) )
!= ( B @ sk5 ) ) ),
inference(paramod_ordered,[status(thm)],[53198,2114]) ).
thf(54334,plain,
! [B: $i > $o,A: $i] :
( ( ( dsetconstr @ A
@ ^ [C: $i] :
~ ( B @ C ) )
!= sk3 )
| ( ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) )
!= ( B @ sk5 ) ) ),
inference(simp,[status(thm)],[54333]) ).
thf(54733,plain,
! [A: $i] :
( ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) ) )
!= sk3 ),
inference(pre_uni,[status(thm)],[54334:[bind(A,$thf( A )),bind(B,$thf( ^ [C: $i] : ( in @ C @ ( dsetconstr @ sk3 @ ^ [D: $i] : ( D = sk5 ) ) ) ))]]) ).
thf(6,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ A )
| ~ ( in @ ( sk2 @ B @ A ) @ A )
| ( A = B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(23,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( in @ ( sk1 @ B @ A ) @ A )
| ~ ( in @ ( sk2 @ B @ A ) @ A ) ),
inference(lifteq,[status(thm)],[6]) ).
thf(24,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( in @ ( sk1 @ B @ A ) @ A )
| ~ ( in @ ( sk2 @ B @ A ) @ A ) ),
inference(simp,[status(thm)],[23]) ).
thf(192,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( in @ sk5 @ A )
| ( B != sk3 ) ),
inference(paramod_ordered,[status(thm)],[19,13]) ).
thf(193,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ sk3 @ emptyset ) )
| ( in @ sk5 @ A ) ),
inference(pattern_uni,[status(thm)],[192:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(12692,plain,
! [A: $i] :
( ~ $true
| ( in @ sk5 @ A )
| ( ( in @ sk5 @ sk3 )
!= ( in @ A @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[13,193]) ).
thf(12693,plain,
! [A: $i] :
( ( in @ sk5 @ A )
| ( ( in @ sk5 @ sk3 )
!= ( in @ A @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(simp,[status(thm)],[12692]) ).
thf(12896,plain,
! [A: $i] :
( ( in @ sk5 @ A )
| ( sk5 != A )
| ( ( setadjoin @ sk3 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[12693]) ).
thf(12960,plain,
( ( in @ sk5 @ sk5 )
| ( ( setadjoin @ sk3 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[12896]) ).
thf(54732,plain,
! [A: $i] :
( ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = B ) ) ) )
!= sk3 ),
inference(pre_uni,[status(thm)],[54334:[bind(A,$thf( A )),bind(B,$thf( ^ [C: $i] : ( in @ sk5 @ ( dsetconstr @ sk3 @ ^ [D: $i] : ( D = C ) ) ) ))]]) ).
thf(56185,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A != sk3 )
| ( B
!= ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [E: $i] : ( E = D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,54732]) ).
thf(56186,plain,
! [B: $i,A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) )
@ emptyset ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[56185:[bind(A,$thf( A )),bind(B,$thf( dsetconstr @ D @ ^ [E: $i] : ~ ( in @ sk5 @ ( dsetconstr @ sk3 @ ^ [F: $i] : ( F = E ) ) ) )),bind(C,$thf( D ))]]) ).
thf(56221,plain,
! [A: $i] :
~ ( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = B ) ) ) )
@ emptyset ) ),
inference(simp,[status(thm)],[56186]) ).
thf(32930,plain,
! [A: $i] :
( ~ $true
| ( A = sk6 )
| ( ( in @ sk5 @ sk3 )
!= ( in @ A @ ( setadjoin @ sk6 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[13,32530]) ).
thf(32931,plain,
! [A: $i] :
( ( A = sk6 )
| ( ( in @ sk5 @ sk3 )
!= ( in @ A @ ( setadjoin @ sk6 @ emptyset ) ) ) ),
inference(simp,[status(thm)],[32930]) ).
thf(33737,plain,
! [A: $i] :
( ( A = sk6 )
| ( sk5 != A )
| ( ( setadjoin @ sk6 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[32931]) ).
thf(33969,plain,
( ( sk6 = sk5 )
| ( ( setadjoin @ sk6 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[33737]) ).
thf(34058,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( sk6 = sk5 )
| ( B != sk3 )
| ( A
!= ( setadjoin @ sk6 @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,33969]) ).
thf(34059,plain,
! [A: $i] :
( ~ ( in @ ( setadjoin @ sk6 @ emptyset ) @ ( setadjoin @ A @ emptyset ) )
| ( sk6 = sk5 )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[34058:[bind(A,$thf( setadjoin @ sk6 @ emptyset )),bind(B,$thf( B ))]]) ).
thf(34080,plain,
( ~ ( in @ ( setadjoin @ sk6 @ emptyset ) @ ( setadjoin @ sk3 @ emptyset ) )
| ( sk6 = sk5 ) ),
inference(simp,[status(thm)],[34059]) ).
thf(42403,plain,
( ~ ( in @ ( setadjoin @ sk6 @ emptyset ) @ ( setadjoin @ sk3 @ emptyset ) )
| ( ( ^ [A: $i] : ( A = sk5 ) )
!= ( ^ [A: $i] : $false ) )
| ( sk6 != sk6 ) ),
inference(paramod_ordered,[status(thm)],[34080,32286]) ).
thf(42404,plain,
( ~ ( in @ ( setadjoin @ sk6 @ emptyset ) @ ( setadjoin @ sk3 @ emptyset ) )
| ( ( ^ [A: $i] : ( A = sk5 ) )
!= ( ^ [A: $i] : $false ) ) ),
inference(pattern_uni,[status(thm)],[42403:[]]) ).
thf(45385,plain,
( ( sk11 = sk5 )
| ~ ( in @ ( setadjoin @ sk6 @ emptyset ) @ ( setadjoin @ sk3 @ emptyset ) ) ),
inference(func_ext,[status(esa)],[42404]) ).
thf(45634,plain,
( ( sk11 = sk5 )
| ~ ( in @ ( setadjoin @ sk6 @ emptyset ) @ ( setadjoin @ sk3 @ emptyset ) ) ),
inference(lifteq,[status(thm)],[45385]) ).
thf(176,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( in @ B @ sk3 )
| ( A != sk6 ) ),
inference(paramod_ordered,[status(thm)],[19,9]) ).
thf(177,plain,
! [A: $i] :
( ~ ( in @ sk6 @ ( setadjoin @ A @ emptyset ) )
| ( in @ A @ sk3 ) ),
inference(pattern_uni,[status(thm)],[176:[bind(A,$thf( sk6 ))]]) ).
thf(266,plain,
! [A: $i] :
( ~ ( in @ sk6 @ ( setadjoin @ A @ emptyset ) )
| ( in @ A @ sk3 ) ),
inference(simp,[status(thm)],[177]) ).
thf(17111,plain,
! [A: $i] :
( ~ $true
| ( in @ A @ sk3 )
| ( ( in @ sk6 @ ( setadjoin @ A @ emptyset ) )
!= ( in @ sk6 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[9,266]) ).
thf(17112,plain,
! [A: $i] :
( ( in @ A @ sk3 )
| ( ( in @ sk6 @ ( setadjoin @ A @ emptyset ) )
!= ( in @ sk6 @ sk3 ) ) ),
inference(simp,[status(thm)],[17111]) ).
thf(17321,plain,
! [A: $i] :
( ( in @ A @ sk3 )
| ( sk6 != sk6 )
| ( ( setadjoin @ A @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[17112]) ).
thf(17415,plain,
! [A: $i] :
( ( in @ A @ sk3 )
| ( ( setadjoin @ A @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[17321]) ).
thf(391,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ C
@ ( dsetconstr @ B
@ ^ [D: $i] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,349]) ).
thf(392,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ C
@ ( dsetconstr @ B
@ ^ [D: $i] : $false ) ) ),
inference(simp,[status(thm)],[391]) ).
thf(398,plain,
! [C: $i,B: $i,A: $i] :
( ( A != C )
| ( ( setadjoin @ A @ emptyset )
!= ( dsetconstr @ B
@ ^ [D: $i] : $false ) ) ),
inference(simp,[status(thm)],[392]) ).
thf(411,plain,
! [B: $i,A: $i] :
( ( setadjoin @ B @ emptyset )
!= ( dsetconstr @ A
@ ^ [C: $i] : $false ) ),
inference(simp,[status(thm)],[398]) ).
thf(900,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A
!= ( setadjoin @ D @ emptyset ) )
| ( B
!= ( dsetconstr @ C
@ ^ [E: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[19,411]) ).
thf(901,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ emptyset ) )
| ( A
!= ( setadjoin @ B @ emptyset ) ) ),
inference(pattern_uni,[status(thm)],[900:[bind(A,$thf( A )),bind(B,$thf( dsetconstr @ E @ ^ [F: $i] : $false )),bind(C,$thf( E )),bind(D,$thf( D ))]]) ).
thf(905,plain,
! [B: $i,A: $i] :
~ ( in @ ( setadjoin @ A @ emptyset )
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset ) ),
inference(simp,[status(thm)],[901]) ).
thf(5132,plain,
! [E: $i,D: $i,C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ~ $true
| ( ( B @ C )
!= ( in @ ( setadjoin @ D @ emptyset )
@ ( setadjoin
@ ( dsetconstr @ E
@ ^ [F: $i] : $false )
@ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,905]) ).
thf(5133,plain,
! [E: $i,D: $i,C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ( ( B @ C )
!= ( in @ ( setadjoin @ D @ emptyset )
@ ( setadjoin
@ ( dsetconstr @ E
@ ^ [F: $i] : $false )
@ emptyset ) ) ) ),
inference(simp,[status(thm)],[5132]) ).
thf(5159,plain,
! [B: $i,A: $i] :
~ ( in
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset )
@ ( dsetconstr @ A
@ ^ [C: $i] : ( in @ C @ C ) ) ),
inference(pre_uni,[status(thm)],[5133:[bind(A,$thf( A )),bind(B,$thf( ^ [F: $i] : ( in @ F @ F ) )),bind(C,$thf( setadjoin @ ( dsetconstr @ E @ ^ [F: $i] : $false ) @ emptyset )),bind(D,$thf( dsetconstr @ E @ ^ [F: $i] : $false )),bind(E,$thf( E ))]]) ).
thf(5190,plain,
! [B: $i,A: $i] :
~ ( in
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset )
@ ( dsetconstr @ A
@ ^ [C: $i] : ( in @ C @ C ) ) ),
inference(simp,[status(thm)],[5159]) ).
thf(6318,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( setadjoin
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ emptyset )
@ ( dsetconstr @ B
@ ^ [D: $i] : ( in @ D @ D ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,5190]) ).
thf(6319,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( setadjoin
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ emptyset )
@ ( dsetconstr @ B
@ ^ [D: $i] : ( in @ D @ D ) ) ) ),
inference(simp,[status(thm)],[6318]) ).
thf(6409,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( setadjoin
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ emptyset ) )
| ( ( setadjoin @ A @ emptyset )
!= ( dsetconstr @ B
@ ^ [D: $i] : ( in @ D @ D ) ) ) ),
inference(simp,[status(thm)],[6319]) ).
thf(6423,plain,
! [B: $i,A: $i] :
( ( setadjoin
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset )
@ emptyset )
!= ( dsetconstr @ A
@ ^ [C: $i] : ( in @ C @ C ) ) ),
inference(simp,[status(thm)],[6409]) ).
thf(32465,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B != sk3 )
| ( A
!= ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [E: $i] : ( E = D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,32098]) ).
thf(32466,plain,
! [B: $i,A: $i] :
( ~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) )
@ ( setadjoin @ A @ emptyset ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[32465:[bind(A,$thf( dsetconstr @ D @ ^ [E: $i] : ~ ( in @ sk6 @ ( dsetconstr @ sk3 @ ^ [F: $i] : ( F = E ) ) ) )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(32484,plain,
! [A: $i] :
~ ( in
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = B ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ),
inference(simp,[status(thm)],[32466]) ).
thf(41365,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,32484]) ).
thf(41366,plain,
! [B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[41365]) ).
thf(41546,plain,
! [B: $i,A: $i] :
( ( A
!= ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) ) )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[41366]) ).
thf(41613,plain,
! [A: $i] :
( ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = B ) ) ) )
@ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ),
inference(simp,[status(thm)],[41546]) ).
thf(423,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B != sk3 )
| ( A
!= ( dsetconstr @ C
@ ^ [D: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[19,410]) ).
thf(424,plain,
! [B: $i,A: $i] :
( ~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ ( setadjoin @ A @ emptyset ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[423:[bind(A,$thf( dsetconstr @ D @ ^ [E: $i] : $false )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(430,plain,
! [A: $i] :
~ ( in
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ ( setadjoin @ sk3 @ emptyset ) ),
inference(simp,[status(thm)],[424]) ).
thf(459,plain,
! [D: $i,C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ~ $true
| ( ( B @ C )
!= ( in
@ ( dsetconstr @ D
@ ^ [E: $i] : $false )
@ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,430]) ).
thf(460,plain,
! [D: $i,C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ( ( B @ C )
!= ( in
@ ( dsetconstr @ D
@ ^ [E: $i] : $false )
@ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(simp,[status(thm)],[459]) ).
thf(480,plain,
! [B: $i,A: $i] :
~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ ( dsetconstr @ A
@ ^ [C: $i] : ( in @ C @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(pre_uni,[status(thm)],[460:[bind(A,$thf( A )),bind(B,$thf( ^ [E: $i] : ( in @ E @ ( setadjoin @ sk3 @ emptyset ) ) )),bind(C,$thf( dsetconstr @ D @ ^ [E: $i] : $false )),bind(D,$thf( D ))]]) ).
thf(502,plain,
! [B: $i,A: $i] :
~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ ( dsetconstr @ A
@ ^ [C: $i] : ( in @ C @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(simp,[status(thm)],[480]) ).
thf(8742,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ ( dsetconstr @ B
@ ^ [D: $i] : ( in @ D @ ( setadjoin @ sk3 @ emptyset ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,502]) ).
thf(8743,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ ( dsetconstr @ B
@ ^ [D: $i] : ( in @ D @ ( setadjoin @ sk3 @ emptyset ) ) ) ) ),
inference(simp,[status(thm)],[8742]) ).
thf(8853,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( dsetconstr @ C
@ ^ [D: $i] : $false ) )
| ( ( setadjoin @ A @ emptyset )
!= ( dsetconstr @ B
@ ^ [D: $i] : ( in @ D @ ( setadjoin @ sk3 @ emptyset ) ) ) ) ),
inference(simp,[status(thm)],[8743]) ).
thf(8880,plain,
! [B: $i,A: $i] :
( ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset )
!= ( dsetconstr @ A
@ ^ [C: $i] : ( in @ C @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(simp,[status(thm)],[8853]) ).
thf(482,plain,
! [B: $i > $i,A: $i] :
~ ( in @ emptyset
@ ( dsetconstr @ A
@ ^ [C: $i] :
( in
@ ( dsetconstr @ ( B @ C )
@ ^ [D: $i] : $false )
@ ( setadjoin @ sk3 @ C ) ) ) ),
inference(pre_uni,[status(thm)],[460:[bind(A,$thf( A )),bind(B,$thf( ^ [F: $i] : ( in @ ( dsetconstr @ ( I @ F ) @ ^ [G: $i] : $false ) @ ( setadjoin @ sk3 @ F ) ) )),bind(C,$thf( emptyset )),bind(D,$thf( I @ emptyset ))]]) ).
thf(504,plain,
! [B: $i > $i,A: $i] :
~ ( in @ emptyset
@ ( dsetconstr @ A
@ ^ [C: $i] :
( in
@ ( dsetconstr @ ( B @ C )
@ ^ [D: $i] : $false )
@ ( setadjoin @ sk3 @ C ) ) ) ),
inference(simp,[status(thm)],[482]) ).
thf(54847,plain,
! [A: $i] :
( ( sk3 != A )
| ( ( ^ [B: $i] : ( B = sk5 ) )
!= ( ^ [B: $i] : $false ) ) ),
inference(simp,[status(thm)],[54836]) ).
thf(54965,plain,
( ( ^ [A: $i] : ( A = sk5 ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[54847]) ).
thf(54995,plain,
sk17 = sk5,
inference(func_ext,[status(esa)],[54965]) ).
thf(55018,plain,
sk17 = sk5,
inference(lifteq,[status(thm)],[54995]) ).
thf(55032,plain,
! [A: $i] :
( ~ ( in @ sk6 @ ( setadjoin @ A @ emptyset ) )
| ( sk6 = sk5 )
| ( A != sk17 ) ),
inference(paramod_ordered,[status(thm)],[35807,55018]) ).
thf(55033,plain,
( ~ ( in @ sk6 @ ( setadjoin @ sk17 @ emptyset ) )
| ( sk6 = sk5 ) ),
inference(pattern_uni,[status(thm)],[55032:[bind(A,$thf( sk17 ))]]) ).
thf(55053,plain,
( ~ ( in @ sk6 @ ( setadjoin @ sk5 @ emptyset ) )
| ( sk6 = sk5 ) ),
inference(rewrite,[status(thm)],[55033,55018]) ).
thf(1309,plain,
! [A: $i] :
( ~ $true
| ( ( in @ sk6 @ sk3 )
!= ( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,431]) ).
thf(1310,plain,
! [A: $i] :
( ( in @ sk6 @ sk3 )
!= ( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset ) ) ),
inference(simp,[status(thm)],[1309]) ).
thf(1379,plain,
! [A: $i] :
( ( sk6 != sk3 )
| ( ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[1310]) ).
thf(1375,plain,
! [B: $i,A: $i] :
~ ( in
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset )
@ ( dsetconstr @ A @ ( in @ sk3 ) ) ),
inference(pre_uni,[status(thm)],[1353:[bind(A,$thf( A )),bind(B,$thf( in @ sk3 )),bind(C,$thf( setadjoin @ ( dsetconstr @ D @ ^ [E: $i] : $false ) @ emptyset )),bind(D,$thf( D ))]]) ).
thf(1398,plain,
! [B: $i,A: $i] :
~ ( in
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset )
@ ( dsetconstr @ A @ ( in @ sk3 ) ) ),
inference(simp,[status(thm)],[1375]) ).
thf(54922,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B
!= ( dsetconstr @ C
@ ^ [D: $i] : $false ) )
| ( A
!= ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,54836]) ).
thf(54923,plain,
! [B: $i,A: $i] :
( ~ ( in
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
@ ( setadjoin @ A @ emptyset ) )
| ( A
!= ( dsetconstr @ B
@ ^ [C: $i] : $false ) ) ),
inference(pattern_uni,[status(thm)],[54922:[bind(A,$thf( dsetconstr @ sk3 @ ^ [D: $i] : ( D = sk5 ) )),bind(B,$thf( B )),bind(C,$thf( C ))]]) ).
thf(54952,plain,
! [A: $i] :
~ ( in
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset ) ),
inference(simp,[status(thm)],[54923]) ).
thf(39499,plain,
( ~ ( in @ sk3 @ ( setadjoin @ ( setadjoin @ sk6 @ emptyset ) @ emptyset ) )
| ( ( ^ [A: $i] : ( A = sk5 ) )
!= ( ^ [A: $i] : $false ) )
| ( sk6 != sk6 ) ),
inference(paramod_ordered,[status(thm)],[32558,32286]) ).
thf(39500,plain,
( ~ ( in @ sk3 @ ( setadjoin @ ( setadjoin @ sk6 @ emptyset ) @ emptyset ) )
| ( ( ^ [A: $i] : ( A = sk5 ) )
!= ( ^ [A: $i] : $false ) ) ),
inference(pattern_uni,[status(thm)],[39499:[]]) ).
thf(41741,plain,
! [A: $i] :
( ~ $true
| ( ( ^ [B: $i] : ( B = sk5 ) )
!= ( ^ [B: $i] : $false ) )
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ sk3 @ ( setadjoin @ ( setadjoin @ sk6 @ emptyset ) @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,39500]) ).
thf(41742,plain,
! [A: $i] :
( ( ( ^ [B: $i] : ( B = sk5 ) )
!= ( ^ [B: $i] : $false ) )
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ sk3 @ ( setadjoin @ ( setadjoin @ sk6 @ emptyset ) @ emptyset ) ) ) ),
inference(simp,[status(thm)],[41741]) ).
thf(41941,plain,
! [A: $i] :
( ( ( ^ [B: $i] : ( B = sk5 ) )
!= ( ^ [B: $i] : $false ) )
| ( A != sk3 )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin @ ( setadjoin @ sk6 @ emptyset ) @ emptyset ) ) ),
inference(simp,[status(thm)],[41742]) ).
thf(42024,plain,
( ( ( ^ [A: $i] : ( A = sk5 ) )
!= ( ^ [A: $i] : $false ) )
| ( ( setadjoin @ ( setadjoin @ sk6 @ emptyset ) @ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[41941]) ).
thf(50405,plain,
( ( ( ^ [A: $i] : ( A = sk5 ) )
!= ( ^ [A: $i] : $false ) )
| ( ( setadjoin @ sk6 @ emptyset )
!= sk3 )
| ( emptyset != emptyset ) ),
inference(simp,[status(thm)],[42024]) ).
thf(50581,plain,
( ( ( ^ [A: $i] : ( A = sk5 ) )
!= ( ^ [A: $i] : $false ) )
| ( ( setadjoin @ sk6 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[50405]) ).
thf(50590,plain,
( ( sk14 = sk5 )
| ( ( setadjoin @ sk6 @ emptyset )
!= sk3 ) ),
inference(func_ext,[status(esa)],[50581]) ).
thf(50691,plain,
( ( sk14 = sk5 )
| ( ( setadjoin @ sk6 @ emptyset )
!= sk3 ) ),
inference(lifteq,[status(thm)],[50590]) ).
thf(50783,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( sk14 = sk5 )
| ( A != sk3 )
| ( B
!= ( setadjoin @ sk6 @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,50691]) ).
thf(50784,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ ( setadjoin @ sk6 @ emptyset ) @ emptyset ) )
| ( sk14 = sk5 )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[50783:[bind(A,$thf( A )),bind(B,$thf( setadjoin @ sk6 @ emptyset ))]]) ).
thf(50807,plain,
( ~ ( in @ sk3 @ ( setadjoin @ ( setadjoin @ sk6 @ emptyset ) @ emptyset ) )
| ( sk14 = sk5 ) ),
inference(simp,[status(thm)],[50784]) ).
thf(57402,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,54952]) ).
thf(57403,plain,
! [B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset ) ) ),
inference(simp,[status(thm)],[57402]) ).
thf(57641,plain,
! [B: $i,A: $i] :
( ( A
!= ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset ) ) ),
inference(simp,[status(thm)],[57403]) ).
thf(57688,plain,
! [A: $i] :
( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset )
!= ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset ) ),
inference(simp,[status(thm)],[57641]) ).
thf(37,plain,
! [E: $i,D: $i,C: $o,B: $i,A: $i] :
( ~ $true
| ~ ( in @ E @ B )
| ~ C
| ( in @ D
@ ( dsetconstr @ B
@ ^ [F: $i] :
( ( C
& ( F = D ) )
| ( ~ C
& ( F = E ) ) ) ) )
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ D @ B ) ) ),
inference(paramod_ordered,[status(thm)],[28,22]) ).
thf(38,plain,
! [E: $i,D: $i,C: $o,B: $i,A: $i] :
( ~ ( in @ E @ B )
| ~ C
| ( in @ D
@ ( dsetconstr @ B
@ ^ [F: $i] :
( ( C
& ( F = D ) )
| ( ~ C
& ( F = E ) ) ) ) )
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ D @ B ) ) ),
inference(simp,[status(thm)],[37]) ).
thf(39,plain,
! [C: $i,B: $i,A: $o] :
( ~ ( in @ B @ ( setadjoin @ C @ emptyset ) )
| ~ A
| ( in @ C
@ ( dsetconstr @ ( setadjoin @ C @ emptyset )
@ ^ [D: $i] :
( ( A
& ( D = C ) )
| ( ~ A
& ( D = B ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[38:[bind(A,$thf( F )),bind(B,$thf( setadjoin @ F @ emptyset )),bind(C,$thf( C )),bind(D,$thf( F )),bind(E,$thf( E ))]]) ).
thf(84,plain,
! [C: $i,B: $i,A: $o] :
( ~ ( in @ B @ ( setadjoin @ C @ emptyset ) )
| ~ A
| ( in @ C
@ ( dsetconstr @ ( setadjoin @ C @ emptyset )
@ ^ [D: $i] :
( ( A
& ( D = C ) )
| ( ~ A
& ( D = B ) ) ) ) ) ),
inference(simp,[status(thm)],[39]) ).
thf(105,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B )
| ( in @ A @ sk3 )
| ( B != sk6 ) ),
inference(paramod_ordered,[status(thm)],[26,9]) ).
thf(106,plain,
! [A: $i] :
( ( in @ ( sk1 @ sk6 @ A ) @ A )
| ( in @ ( sk2 @ sk6 @ A ) @ sk6 )
| ( in @ A @ sk3 ) ),
inference(pattern_uni,[status(thm)],[105:[bind(A,$thf( A )),bind(B,$thf( sk6 ))]]) ).
thf(129,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B )
| ( ( dsetconstr @ B
@ ^ [C: $i] : ( C = sk5 ) )
!= ( setadjoin @ sk5 @ emptyset ) )
| ( A != sk3 ) ),
inference(paramod_ordered,[status(thm)],[26,35]) ).
thf(130,plain,
! [A: $i] :
( ( in @ ( sk1 @ A @ sk3 ) @ sk3 )
| ( in @ ( sk2 @ A @ sk3 ) @ A )
| ( ( dsetconstr @ A
@ ^ [B: $i] : ( B = sk5 ) )
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(pattern_uni,[status(thm)],[129:[bind(A,$thf( sk3 ))]]) ).
thf(147,plain,
! [A: $i] :
( ( in @ ( sk1 @ A @ sk3 ) @ sk3 )
| ( in @ ( sk2 @ A @ sk3 ) @ A )
| ( ( dsetconstr @ A
@ ^ [B: $i] : ( B = sk5 ) )
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(simp,[status(thm)],[130]) ).
thf(49,plain,
! [D: $i,C: $i,B: $o,A: $i] :
( ~ $true
| ~ ( in @ D @ A )
| ~ B
| ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) )
| ( ( in @ sk5 @ sk3 )
!= ( in @ C @ A ) ) ),
inference(paramod_ordered,[status(thm)],[13,22]) ).
thf(50,plain,
! [D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ D @ A )
| ~ B
| ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) )
| ( ( in @ sk5 @ sk3 )
!= ( in @ C @ A ) ) ),
inference(simp,[status(thm)],[49]) ).
thf(51,plain,
! [B: $i,A: $o] :
( ~ ( in @ B @ sk3 )
| ~ A
| ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [C: $i] :
( ( A
& ( C = sk5 ) )
| ( ~ A
& ( C = B ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[50:[bind(A,$thf( sk3 )),bind(B,$thf( B )),bind(C,$thf( sk5 ))]]) ).
thf(89,plain,
! [B: $i,A: $o] :
( ~ ( in @ B @ sk3 )
| ~ A
| ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [C: $i] :
( ( A
& ( C = sk5 ) )
| ( ~ A
& ( C = B ) ) ) ) ) ),
inference(simp,[status(thm)],[51]) ).
thf(194,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ $true
| ( ( in @ sk5 @ sk3 )
!= ( in @ A @ ( setadjoin @ B @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[13,19]) ).
thf(195,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( ( in @ sk5 @ sk3 )
!= ( in @ A @ ( setadjoin @ B @ emptyset ) ) ) ),
inference(simp,[status(thm)],[194]) ).
thf(240,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( sk5 != A )
| ( ( setadjoin @ B @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[195]) ).
thf(265,plain,
! [A: $i] :
( ( sk5 = A )
| ( ( setadjoin @ A @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[240]) ).
thf(66,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ A )
| ~ ( in @ C @ A )
| ~ ~ D
| ( in @ B
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( ~ D
& ( E = B ) )
| ( ~ ~ D
& ( E = C ) ) ) ) ) ),
inference(prim_subst,[status(thm)],[22:[bind(A,$thf( A )),bind(B,$thf( ~ ( E ) ))]]) ).
thf(73,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ A )
| ~ ( in @ C @ A )
| D
| ( in @ B
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( ~ D
& ( E = B ) )
| ( ~ ~ D
& ( E = C ) ) ) ) ) ),
inference(cnf,[status(esa)],[66]) ).
thf(74,plain,
! [D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ A )
| ~ ( in @ C @ A )
| D
| ( in @ B
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( ~ D
& ( E = B ) )
| ( D
& ( E = C ) ) ) ) ) ),
inference(simp,[status(thm)],[73]) ).
thf(115,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B )
| ( in @ sk5 @ A )
| ( B != sk3 ) ),
inference(paramod_ordered,[status(thm)],[26,13]) ).
thf(116,plain,
! [A: $i] :
( ( in @ ( sk1 @ sk3 @ A ) @ A )
| ( in @ ( sk2 @ sk3 @ A ) @ sk3 )
| ( in @ sk5 @ A ) ),
inference(pattern_uni,[status(thm)],[115:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(620,plain,
( ~ $true
| ( ( in @ ( setadjoin @ sk5 @ emptyset )
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset ) )
!= ( in @ sk5 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[13,246]) ).
thf(621,plain,
( ( in @ ( setadjoin @ sk5 @ emptyset )
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset ) )
!= ( in @ sk5 @ sk3 ) ),
inference(simp,[status(thm)],[620]) ).
thf(700,plain,
( ( ( setadjoin @ sk5 @ emptyset )
!= sk5 )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[621]) ).
thf(3546,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A != sk5 )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
@ emptyset )
!= sk3 )
| ( B
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,700]) ).
thf(3547,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) )
| ( A != sk5 )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset )
!= sk3 ) ),
inference(pattern_uni,[status(thm)],[3546:[bind(A,$thf( A )),bind(B,$thf( setadjoin @ sk5 @ emptyset ))]]) ).
thf(3591,plain,
( ~ ( in @ sk5 @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[3547]) ).
thf(62,plain,
! [D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ ( in @ D @ A )
| ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) )
| ( B
!= ( in @ C @ A ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[22]) ).
thf(71,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ C )
| ~ ( in @ A @ C )
| ( in @ B
@ ( dsetconstr @ C
@ ^ [D: $i] :
( ( ( in @ B @ C )
& ( D = B ) )
| ( ~ ( in @ B @ C )
& ( D = A ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[62:[bind(A,$thf( F )),bind(B,$thf( in @ E @ F )),bind(C,$thf( E ))]]) ).
thf(85,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ B @ C )
| ~ ( in @ A @ C )
| ( in @ B
@ ( dsetconstr @ C
@ ^ [D: $i] :
( ( ( in @ B @ C )
& ( D = B ) )
| ( ~ ( in @ B @ C )
& ( D = A ) ) ) ) ) ),
inference(simp,[status(thm)],[71]) ).
thf(55134,plain,
! [A: $i] :
( ~ $true
| ( sk6 = sk5 )
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ sk6 @ ( setadjoin @ sk5 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,55053]) ).
thf(55135,plain,
! [A: $i] :
( ( sk6 = sk5 )
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ sk6 @ ( setadjoin @ sk5 @ emptyset ) ) ) ),
inference(simp,[status(thm)],[55134]) ).
thf(55404,plain,
! [A: $i] :
( ( sk6 = sk5 )
| ( A != sk6 )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(simp,[status(thm)],[55135]) ).
thf(55465,plain,
( ( sk6 = sk5 )
| ( ( setadjoin @ sk6 @ emptyset )
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(simp,[status(thm)],[55404]) ).
thf(5085,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ ( setadjoin @ B @ emptyset )
@ ( setadjoin
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,905]) ).
thf(5086,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ ( setadjoin @ B @ emptyset )
@ ( setadjoin
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ emptyset ) ) ),
inference(simp,[status(thm)],[5085]) ).
thf(5172,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( setadjoin @ B @ emptyset ) )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ emptyset ) ) ),
inference(simp,[status(thm)],[5086]) ).
thf(5206,plain,
! [B: $i,A: $i] :
( ( setadjoin @ ( setadjoin @ A @ emptyset ) @ emptyset )
!= ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset ) ),
inference(simp,[status(thm)],[5172]) ).
thf(3210,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ C ) )
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ C ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,340]) ).
thf(3211,plain,
! [B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ C ) )
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ C ) ) ) ),
inference(simp,[status(thm)],[3210]) ).
thf(3243,plain,
! [B: $i,A: $i] :
( ( A
!= ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ C ) ) )
| ( ( setadjoin @ A @ emptyset )
!= ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ C ) ) ) ),
inference(simp,[status(thm)],[3211]) ).
thf(3261,plain,
! [A: $i] :
( ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B @ B ) )
@ emptyset )
!= ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B @ B ) ) ),
inference(simp,[status(thm)],[3243]) ).
thf(10,plain,
! [B: $i,A: $i] :
( ~ ( in @ ( sk1 @ B @ A ) @ B )
| ~ ( in @ ( sk2 @ B @ A ) @ A )
| ( A = B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(20,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( in @ ( sk1 @ B @ A ) @ B )
| ~ ( in @ ( sk2 @ B @ A ) @ A ) ),
inference(lifteq,[status(thm)],[10]) ).
thf(21,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( in @ ( sk1 @ B @ A ) @ B )
| ~ ( in @ ( sk2 @ B @ A ) @ A ) ),
inference(simp,[status(thm)],[20]) ).
thf(32099,plain,
! [A: $i] :
( ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk6 ) ) ) )
!= sk3 ),
inference(pre_uni,[status(thm)],[31831:[bind(A,$thf( A )),bind(B,$thf( ^ [C: $i] : ( in @ C @ ( dsetconstr @ sk3 @ ^ [D: $i] : ( D = sk6 ) ) ) ))]]) ).
thf(34986,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B != sk3 )
| ( A
!= ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ D
@ ( dsetconstr @ sk3
@ ^ [E: $i] : ( E = sk6 ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,32099]) ).
thf(34987,plain,
! [B: $i,A: $i] :
( ~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk6 ) ) ) )
@ ( setadjoin @ A @ emptyset ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[34986:[bind(A,$thf( dsetconstr @ D @ ^ [E: $i] : ~ ( in @ E @ ( dsetconstr @ sk3 @ ^ [F: $i] : ( F = sk6 ) ) ) )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(35030,plain,
! [A: $i] :
~ ( in
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk6 ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ),
inference(simp,[status(thm)],[34987]) ).
thf(58,plain,
! [H: $i,G: $i,F: $o,E: $i,D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ ( in @ D @ A )
| ~ B
| ~ ( in @ G @ E )
| ~ $true
| ~ F
| ( in @ G
@ ( dsetconstr @ E
@ ^ [I: $i] :
( ( F
& ( I = G ) )
| ( ~ F
& ( I = H ) ) ) ) )
| ( ( in @ C
@ ( dsetconstr @ A
@ ^ [I: $i] :
( ( B
& ( I = C ) )
| ( ~ B
& ( I = D ) ) ) ) )
!= ( in @ H @ E ) ) ),
inference(paramod_ordered,[status(thm)],[22,22]) ).
thf(59,plain,
! [H: $i,G: $i,F: $o,E: $i,D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ ( in @ D @ A )
| ~ B
| ~ ( in @ G @ E )
| ~ F
| ( in @ G
@ ( dsetconstr @ E
@ ^ [I: $i] :
( ( F
& ( I = G ) )
| ( ~ F
& ( I = H ) ) ) ) )
| ( ( in @ C
@ ( dsetconstr @ A
@ ^ [I: $i] :
( ( B
& ( I = C ) )
| ( ~ B
& ( I = D ) ) ) ) )
!= ( in @ H @ E ) ) ),
inference(simp,[status(thm)],[58]) ).
thf(60,plain,
! [F: $i,E: $i,D: $o,C: $i,B: $i,A: $o] :
( ~ ( in @ B @ F )
| ~ ( in @ C @ F )
| ~ A
| ~ ( in @ E
@ ( dsetconstr @ F
@ ^ [G: $i] :
( ( A
& ( G = B ) )
| ( ~ A
& ( G = C ) ) ) ) )
| ~ D
| ( in @ E
@ ( dsetconstr
@ ( dsetconstr @ F
@ ^ [G: $i] :
( ( A
& ( G = B ) )
| ( ~ A
& ( G = C ) ) ) )
@ ^ [G: $i] :
( ( D
& ( G = E ) )
| ( ~ D
& ( G = B ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[59:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( dsetconstr @ I @ ^ [J: $i] : ( ( B & ( J = C ) ) | ( ~ ( B ) & ( J = D ) ) ) )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( C ))]]) ).
thf(92,plain,
! [F: $i,E: $i,D: $o,C: $i,B: $i,A: $o] :
( ~ ( in @ B @ F )
| ~ ( in @ C @ F )
| ~ A
| ~ ( in @ E
@ ( dsetconstr @ F
@ ^ [G: $i] :
( ( A
& ( G = B ) )
| ( ~ A
& ( G = C ) ) ) ) )
| ~ D
| ( in @ E
@ ( dsetconstr
@ ( dsetconstr @ F
@ ^ [G: $i] :
( ( A
& ( G = B ) )
| ( ~ A
& ( G = C ) ) ) )
@ ^ [G: $i] :
( ( D
& ( G = E ) )
| ( ~ D
& ( G = B ) ) ) ) ) ),
inference(simp,[status(thm)],[60]) ).
thf(554,plain,
! [A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,243]) ).
thf(555,plain,
! [A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ) ),
inference(simp,[status(thm)],[554]) ).
thf(590,plain,
! [A: $i] :
( ( A
!= ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) ) )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ) ),
inference(simp,[status(thm)],[555]) ).
thf(601,plain,
( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
!= ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ),
inference(simp,[status(thm)],[590]) ).
thf(1529,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A
!= ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) )
| ( B
!= ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
@ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,601]) ).
thf(1530,plain,
! [A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset )
@ emptyset ) )
| ( A
!= ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ) ),
inference(pattern_uni,[status(thm)],[1529:[bind(A,$thf( A )),bind(B,$thf( setadjoin @ ( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) ) @ emptyset ))]]) ).
thf(1555,plain,
~ ( in @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
@ ( setadjoin
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
@ emptyset ) ),
inference(simp,[status(thm)],[1530]) ).
thf(32471,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A != sk3 )
| ( B
!= ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [E: $i] : ( E = D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,32098]) ).
thf(32472,plain,
! [B: $i,A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) )
@ emptyset ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[32471:[bind(A,$thf( A )),bind(B,$thf( dsetconstr @ D @ ^ [E: $i] : ~ ( in @ sk6 @ ( dsetconstr @ sk3 @ ^ [F: $i] : ( F = E ) ) ) )),bind(C,$thf( D ))]]) ).
thf(32487,plain,
! [A: $i] :
~ ( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = B ) ) ) )
@ emptyset ) ),
inference(simp,[status(thm)],[32472]) ).
thf(618,plain,
( ~ $true
| ( ( in @ ( setadjoin @ sk5 @ emptyset )
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset ) )
!= ( in @ sk6 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[9,246]) ).
thf(619,plain,
( ( in @ ( setadjoin @ sk5 @ emptyset )
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset ) )
!= ( in @ sk6 @ sk3 ) ),
inference(simp,[status(thm)],[618]) ).
thf(694,plain,
( ( ( setadjoin @ sk5 @ emptyset )
!= sk6 )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[619]) ).
thf(3370,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk6 )
| ( B != sk3 )
| ( A
!= ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
@ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,694]) ).
thf(3371,plain,
! [A: $i] :
( ~ ( in
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset )
@ ( setadjoin @ A @ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk6 )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[3370:[bind(A,$thf( setadjoin @ ( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) ) @ emptyset )),bind(B,$thf( B ))]]) ).
thf(3408,plain,
( ~ ( in
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
@ ( setadjoin @ sk3 @ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk6 ) ),
inference(simp,[status(thm)],[3371]) ).
thf(457,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,430]) ).
thf(458,plain,
! [B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[457]) ).
thf(488,plain,
! [B: $i,A: $i] :
( ( A
!= ( dsetconstr @ B
@ ^ [C: $i] : $false ) )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[458]) ).
thf(509,plain,
! [A: $i] :
( ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ),
inference(simp,[status(thm)],[488]) ).
thf(1443,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B
!= ( setadjoin @ sk3 @ emptyset ) )
| ( A
!= ( setadjoin
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,509]) ).
thf(1444,plain,
! [B: $i,A: $i] :
( ~ ( in
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset )
@ ( setadjoin @ A @ emptyset ) )
| ( A
!= ( setadjoin @ sk3 @ emptyset ) ) ),
inference(pattern_uni,[status(thm)],[1443:[bind(A,$thf( setadjoin @ ( dsetconstr @ F @ ^ [E: $i] : $false ) @ emptyset )),bind(B,$thf( B )),bind(C,$thf( F ))]]) ).
thf(1457,plain,
! [A: $i] :
~ ( in
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset )
@ ( setadjoin @ ( setadjoin @ sk3 @ emptyset ) @ emptyset ) ),
inference(simp,[status(thm)],[1444]) ).
thf(29432,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B
!= ( setadjoin @ sk3 @ emptyset ) )
| ( A
!= ( setadjoin
@ ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ D @ sk3 ) )
@ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,27664]) ).
thf(29433,plain,
! [B: $i,A: $i] :
( ~ ( in
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ sk3 ) )
@ emptyset )
@ ( setadjoin @ A @ emptyset ) )
| ( A
!= ( setadjoin @ sk3 @ emptyset ) ) ),
inference(pattern_uni,[status(thm)],[29432:[bind(A,$thf( setadjoin @ ( dsetconstr @ F @ ^ [E: $i] : ~ ( in @ E @ sk3 ) ) @ emptyset )),bind(B,$thf( B )),bind(C,$thf( F ))]]) ).
thf(29480,plain,
! [A: $i] :
~ ( in
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B @ sk3 ) )
@ emptyset )
@ ( setadjoin @ ( setadjoin @ sk3 @ emptyset ) @ emptyset ) ),
inference(simp,[status(thm)],[29433]) ).
thf(697,plain,
! [A: $i] :
~ ( in
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset )
@ ( dsetconstr @ A @ ( in @ ( setadjoin @ sk5 @ emptyset ) ) ) ),
inference(pre_uni,[status(thm)],[661:[bind(A,$thf( A )),bind(B,$thf( in @ ( setadjoin @ sk5 @ emptyset ) )),bind(C,$thf( setadjoin @ ( dsetconstr @ sk3 @ ^ [D: $i] : ( D = sk5 ) ) @ emptyset ))]]) ).
thf(3386,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk6 )
| ( A != sk3 )
| ( B
!= ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
@ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,694]) ).
thf(3387,plain,
! [A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset )
@ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk6 )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[3386:[bind(A,$thf( A )),bind(B,$thf( setadjoin @ ( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) ) @ emptyset ))]]) ).
thf(3413,plain,
( ~ ( in @ sk3
@ ( setadjoin
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
@ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk6 ) ),
inference(simp,[status(thm)],[3387]) ).
thf(516,plain,
( ~ $true
| ( ( in
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) )
!= ( in @ sk5 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[13,243]) ).
thf(517,plain,
( ( in
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) )
!= ( in @ sk5 @ sk3 ) ),
inference(simp,[status(thm)],[516]) ).
thf(593,plain,
( ( ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
!= sk5 )
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[517]) ).
thf(1620,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B != sk5 )
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 )
| ( A
!= ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,593]) ).
thf(1621,plain,
! [A: $i] :
( ~ ( in
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ ( setadjoin @ A @ emptyset ) )
| ( A != sk5 )
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 ) ),
inference(pattern_uni,[status(thm)],[1620:[bind(A,$thf( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) )),bind(B,$thf( B ))]]) ).
thf(1672,plain,
( ~ ( in
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ sk5 @ emptyset ) )
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[1621]) ).
thf(182,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( in @ sk6 @ A )
| ( B != sk3 ) ),
inference(paramod_ordered,[status(thm)],[19,9]) ).
thf(183,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ sk3 @ emptyset ) )
| ( in @ sk6 @ A ) ),
inference(pattern_uni,[status(thm)],[182:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(7728,plain,
! [A: $i] :
( ~ $true
| ( in @ sk6 @ A )
| ( ( in @ sk6 @ sk3 )
!= ( in @ A @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,183]) ).
thf(7729,plain,
! [A: $i] :
( ( in @ sk6 @ A )
| ( ( in @ sk6 @ sk3 )
!= ( in @ A @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(simp,[status(thm)],[7728]) ).
thf(7832,plain,
! [A: $i] :
( ( in @ sk6 @ A )
| ( sk6 != A )
| ( ( setadjoin @ sk3 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[7729]) ).
thf(7875,plain,
( ( in @ sk6 @ sk6 )
| ( ( setadjoin @ sk3 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[7832]) ).
thf(9994,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B )
| ( in @ sk6 @ sk6 )
| ( B != sk3 )
| ( A
!= ( setadjoin @ sk3 @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[26,7875]) ).
thf(9995,plain,
! [A: $i] :
( ( in @ ( sk1 @ A @ ( setadjoin @ sk3 @ emptyset ) ) @ ( setadjoin @ sk3 @ emptyset ) )
| ( in @ ( sk2 @ A @ ( setadjoin @ sk3 @ emptyset ) ) @ A )
| ( in @ sk6 @ sk6 )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[9994:[bind(A,$thf( setadjoin @ sk3 @ emptyset )),bind(B,$thf( B ))]]) ).
thf(10021,plain,
( ( in @ ( sk1 @ sk3 @ ( setadjoin @ sk3 @ emptyset ) ) @ ( setadjoin @ sk3 @ emptyset ) )
| ( in @ ( sk2 @ sk3 @ ( setadjoin @ sk3 @ emptyset ) ) @ sk3 )
| ( in @ sk6 @ sk6 ) ),
inference(simp,[status(thm)],[9995]) ).
thf(55044,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A = sk5 )
| ( B != sk17 ) ),
inference(paramod_ordered,[status(thm)],[19,55018]) ).
thf(55045,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ sk17 @ emptyset ) )
| ( A = sk5 ) ),
inference(pattern_uni,[status(thm)],[55044:[bind(A,$thf( A )),bind(B,$thf( sk17 ))]]) ).
thf(63446,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ sk5 @ emptyset ) )
| ( A = sk5 ) ),
inference(rewrite,[status(thm)],[55045,55018]) ).
thf(1449,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A
!= ( setadjoin @ sk3 @ emptyset ) )
| ( B
!= ( setadjoin
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,509]) ).
thf(1450,plain,
! [B: $i,A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset )
@ emptyset ) )
| ( A
!= ( setadjoin @ sk3 @ emptyset ) ) ),
inference(pattern_uni,[status(thm)],[1449:[bind(A,$thf( A )),bind(B,$thf( setadjoin @ ( dsetconstr @ F @ ^ [E: $i] : $false ) @ emptyset )),bind(C,$thf( F ))]]) ).
thf(1461,plain,
! [A: $i] :
~ ( in @ ( setadjoin @ sk3 @ emptyset )
@ ( setadjoin
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset )
@ emptyset ) ),
inference(simp,[status(thm)],[1450]) ).
thf(27388,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A != sk3 )
| ( B
!= ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ D @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,26480]) ).
thf(27389,plain,
! [B: $i,A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ sk3 ) )
@ emptyset ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[27388:[bind(A,$thf( A )),bind(B,$thf( dsetconstr @ D @ ^ [E: $i] : ~ ( in @ E @ sk3 ) )),bind(C,$thf( D ))]]) ).
thf(27409,plain,
! [A: $i] :
~ ( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B @ sk3 ) )
@ emptyset ) ),
inference(simp,[status(thm)],[27389]) ).
thf(896,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A
!= ( dsetconstr @ C
@ ^ [E: $i] : $false ) )
| ( B
!= ( setadjoin @ D @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,411]) ).
thf(897,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ ( setadjoin @ C @ emptyset ) @ emptyset ) )
| ( A
!= ( dsetconstr @ B
@ ^ [D: $i] : $false ) ) ),
inference(pattern_uni,[status(thm)],[896:[bind(A,$thf( A )),bind(B,$thf( setadjoin @ E @ emptyset )),bind(C,$thf( C )),bind(D,$thf( E ))]]) ).
thf(903,plain,
! [B: $i,A: $i] :
~ ( in
@ ( dsetconstr @ A
@ ^ [C: $i] : $false )
@ ( setadjoin @ ( setadjoin @ B @ emptyset ) @ emptyset ) ),
inference(simp,[status(thm)],[897]) ).
thf(4881,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [D: $i] : $false )
@ ( setadjoin @ ( setadjoin @ C @ emptyset ) @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,903]) ).
thf(4882,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [D: $i] : $false )
@ ( setadjoin @ ( setadjoin @ C @ emptyset ) @ emptyset ) ) ),
inference(simp,[status(thm)],[4881]) ).
thf(4968,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( dsetconstr @ B
@ ^ [D: $i] : $false ) )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin @ ( setadjoin @ C @ emptyset ) @ emptyset ) ) ),
inference(simp,[status(thm)],[4882]) ).
thf(5026,plain,
! [B: $i,A: $i] :
( ( setadjoin
@ ( dsetconstr @ A
@ ^ [C: $i] : $false )
@ emptyset )
!= ( setadjoin @ ( setadjoin @ B @ emptyset ) @ emptyset ) ),
inference(simp,[status(thm)],[4968]) ).
thf(479,plain,
! [B: $i > $i,A: $i] :
~ ( in @ ( setadjoin @ sk3 @ emptyset )
@ ( dsetconstr @ A
@ ^ [C: $i] :
( in
@ ( dsetconstr @ ( B @ C )
@ ^ [D: $i] : $false )
@ C ) ) ),
inference(pre_uni,[status(thm)],[460:[bind(A,$thf( A )),bind(B,$thf( ^ [F: $i] : ( in @ ( dsetconstr @ ( K @ F ) @ ^ [G: $i] : $false ) @ F ) )),bind(C,$thf( setadjoin @ sk3 @ emptyset )),bind(D,$thf( K @ ( setadjoin @ sk3 @ emptyset ) ))]]) ).
thf(501,plain,
! [B: $i > $i,A: $i] :
~ ( in @ ( setadjoin @ sk3 @ emptyset )
@ ( dsetconstr @ A
@ ^ [C: $i] :
( in
@ ( dsetconstr @ ( B @ C )
@ ^ [D: $i] : $false )
@ C ) ) ),
inference(simp,[status(thm)],[479]) ).
thf(8552,plain,
! [C: $i > $i,B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ ( setadjoin @ sk3 @ emptyset )
@ ( dsetconstr @ B
@ ^ [D: $i] :
( in
@ ( dsetconstr @ ( C @ D )
@ ^ [E: $i] : $false )
@ D ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,501]) ).
thf(8553,plain,
! [C: $i > $i,B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ ( setadjoin @ sk3 @ emptyset )
@ ( dsetconstr @ B
@ ^ [D: $i] :
( in
@ ( dsetconstr @ ( C @ D )
@ ^ [E: $i] : $false )
@ D ) ) ) ),
inference(simp,[status(thm)],[8552]) ).
thf(8654,plain,
! [C: $i > $i,B: $i,A: $i] :
( ( A
!= ( setadjoin @ sk3 @ emptyset ) )
| ( ( setadjoin @ A @ emptyset )
!= ( dsetconstr @ B
@ ^ [D: $i] :
( in
@ ( dsetconstr @ ( C @ D )
@ ^ [E: $i] : $false )
@ D ) ) ) ),
inference(simp,[status(thm)],[8553]) ).
thf(8690,plain,
! [B: $i > $i,A: $i] :
( ( dsetconstr @ A
@ ^ [C: $i] :
( in
@ ( dsetconstr @ ( B @ C )
@ ^ [D: $i] : $false )
@ C ) )
!= ( setadjoin @ ( setadjoin @ sk3 @ emptyset ) @ emptyset ) ),
inference(simp,[status(thm)],[8654]) ).
thf(34994,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A != sk3 )
| ( B
!= ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ D
@ ( dsetconstr @ sk3
@ ^ [E: $i] : ( E = sk6 ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,32099]) ).
thf(34995,plain,
! [B: $i,A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk6 ) ) ) )
@ emptyset ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[34994:[bind(A,$thf( A )),bind(B,$thf( dsetconstr @ D @ ^ [E: $i] : ~ ( in @ E @ ( dsetconstr @ sk3 @ ^ [F: $i] : ( F = sk6 ) ) ) )),bind(C,$thf( D ))]]) ).
thf(35038,plain,
! [A: $i] :
~ ( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk6 ) ) ) )
@ emptyset ) ),
inference(simp,[status(thm)],[34995]) ).
thf(3538,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk5 )
| ( B != sk3 )
| ( A
!= ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
@ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,700]) ).
thf(3539,plain,
! [A: $i] :
( ~ ( in
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset )
@ ( setadjoin @ A @ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk5 )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[3538:[bind(A,$thf( setadjoin @ ( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) ) @ emptyset )),bind(B,$thf( B ))]]) ).
thf(3587,plain,
( ~ ( in
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
@ ( setadjoin @ sk3 @ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk5 ) ),
inference(simp,[status(thm)],[3539]) ).
thf(3554,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk5 )
| ( A != sk3 )
| ( B
!= ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
@ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,700]) ).
thf(3555,plain,
! [A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset )
@ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk5 )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[3554:[bind(A,$thf( A )),bind(B,$thf( setadjoin @ ( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) ) @ emptyset ))]]) ).
thf(3592,plain,
( ~ ( in @ sk3
@ ( setadjoin
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
@ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk5 ) ),
inference(simp,[status(thm)],[3555]) ).
thf(2792,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset )
@ ( setadjoin @ ( setadjoin @ sk3 @ emptyset ) @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,1457]) ).
thf(2793,plain,
! [B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset )
@ ( setadjoin @ ( setadjoin @ sk3 @ emptyset ) @ emptyset ) ) ),
inference(simp,[status(thm)],[2792]) ).
thf(2869,plain,
! [B: $i,A: $i] :
( ( A
!= ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset ) )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin @ ( setadjoin @ sk3 @ emptyset ) @ emptyset ) ) ),
inference(simp,[status(thm)],[2793]) ).
thf(2915,plain,
! [A: $i] :
( ( setadjoin
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset )
@ emptyset )
!= ( setadjoin @ ( setadjoin @ sk3 @ emptyset ) @ emptyset ) ),
inference(simp,[status(thm)],[2869]) ).
thf(33317,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ sk6 @ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk6 )
| ( A
!= ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) ) ) ),
inference(paramod_ordered,[status(thm)],[32530,35]) ).
thf(33318,plain,
( ~ ( in
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ sk6 @ emptyset ) )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk6 ) ),
inference(pattern_uni,[status(thm)],[33317:[bind(A,$thf( dsetconstr @ sk3 @ ^ [B: $i] : ( B = sk5 ) ))]]) ).
thf(379,plain,
! [E: $i,D: $i,C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ~ $true
| ( ( B @ C )
!= ( in @ E
@ ( dsetconstr @ D
@ ^ [F: $i] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,349]) ).
thf(380,plain,
! [E: $i,D: $i,C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ( ( B @ C )
!= ( in @ E
@ ( dsetconstr @ D
@ ^ [F: $i] : $false ) ) ) ),
inference(simp,[status(thm)],[379]) ).
thf(399,plain,
! [C: $i > $i,B: $i,A: $i] :
~ ( in
@ ( dsetconstr @ B
@ ^ [D: $i] : $false )
@ ( dsetconstr @ A
@ ^ [D: $i] : ( in @ ( C @ D ) @ D ) ) ),
inference(pre_uni,[status(thm)],[380:[bind(A,$thf( A )),bind(B,$thf( ^ [G: $i] : ( in @ ( F @ G ) @ G ) )),bind(C,$thf( dsetconstr @ D @ ^ [F: $i] : $false )),bind(D,$thf( D )),bind(E,$thf( F @ ( dsetconstr @ D @ ^ [G: $i] : $false ) ))]]) ).
thf(412,plain,
! [C: $i > $i,B: $i,A: $i] :
~ ( in
@ ( dsetconstr @ B
@ ^ [D: $i] : $false )
@ ( dsetconstr @ A
@ ^ [D: $i] : ( in @ ( C @ D ) @ D ) ) ),
inference(simp,[status(thm)],[399]) ).
thf(1636,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A != sk5 )
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 )
| ( B
!= ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,593]) ).
thf(1637,plain,
! [A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset ) )
| ( A != sk5 )
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 ) ),
inference(pattern_uni,[status(thm)],[1636:[bind(A,$thf( A )),bind(B,$thf( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) ))]]) ).
thf(1680,plain,
( ~ ( in @ sk5
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset ) )
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[1637]) ).
thf(8,plain,
! [B: $i,A: $i] :
( ~ ( in @ ( sk1 @ B @ A ) @ B )
| ( in @ ( sk2 @ B @ A ) @ B )
| ( A = B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(31,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( in @ ( sk1 @ B @ A ) @ B )
| ( in @ ( sk2 @ B @ A ) @ B ) ),
inference(lifteq,[status(thm)],[8]) ).
thf(32,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( in @ ( sk1 @ B @ A ) @ B )
| ( in @ ( sk2 @ B @ A ) @ B ) ),
inference(simp,[status(thm)],[31]) ).
thf(10829,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( setadjoin
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ emptyset )
@ ( dsetconstr @ B @ ( in @ sk3 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,1398]) ).
thf(10830,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( setadjoin
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ emptyset )
@ ( dsetconstr @ B @ ( in @ sk3 ) ) ) ),
inference(simp,[status(thm)],[10829]) ).
thf(10945,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( setadjoin
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ emptyset ) )
| ( ( setadjoin @ A @ emptyset )
!= ( dsetconstr @ B @ ( in @ sk3 ) ) ) ),
inference(simp,[status(thm)],[10830]) ).
thf(10993,plain,
! [B: $i,A: $i] :
( ( setadjoin
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset )
@ emptyset )
!= ( dsetconstr @ A @ ( in @ sk3 ) ) ),
inference(simp,[status(thm)],[10945]) ).
thf(7689,plain,
! [A: $i] :
( ~ $true
| ( in @ sk6 @ A )
| ( ( in @ sk5 @ sk3 )
!= ( in @ A @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[13,183]) ).
thf(7690,plain,
! [A: $i] :
( ( in @ sk6 @ A )
| ( ( in @ sk5 @ sk3 )
!= ( in @ A @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(simp,[status(thm)],[7689]) ).
thf(7859,plain,
! [A: $i] :
( ( in @ sk6 @ A )
| ( sk5 != A )
| ( ( setadjoin @ sk3 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[7690]) ).
thf(7910,plain,
( ( in @ sk6 @ sk5 )
| ( ( setadjoin @ sk3 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[7859]) ).
thf(133,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B )
| ( A
!= ( setadjoin @ sk5 @ emptyset ) )
| ( B
!= ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) ) ),
inference(paramod_ordered,[status(thm)],[26,35]) ).
thf(134,plain,
! [A: $i] :
( ( in
@ ( sk1
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ A )
@ A )
| ( in
@ ( sk2
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ A )
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) ) )
| ( A
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(pattern_uni,[status(thm)],[133:[bind(A,$thf( A )),bind(B,$thf( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) ))]]) ).
thf(149,plain,
( ( in
@ ( sk1
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ sk5 @ emptyset ) )
@ ( setadjoin @ sk5 @ emptyset ) )
| ( in
@ ( sk2
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ sk5 @ emptyset ) )
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) ) ) ),
inference(simp,[status(thm)],[134]) ).
thf(44461,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk6 ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,35030]) ).
thf(44462,plain,
! [B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk6 ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[44461]) ).
thf(44696,plain,
! [B: $i,A: $i] :
( ( A
!= ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk6 ) ) ) ) )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[44462]) ).
thf(44777,plain,
! [A: $i] :
( ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk6 ) ) ) )
@ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ),
inference(simp,[status(thm)],[44696]) ).
thf(190,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( in @ A @ sk3 )
| ( B != sk5 ) ),
inference(paramod_ordered,[status(thm)],[19,13]) ).
thf(191,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ sk5 @ emptyset ) )
| ( in @ A @ sk3 ) ),
inference(pattern_uni,[status(thm)],[190:[bind(A,$thf( A )),bind(B,$thf( sk5 ))]]) ).
thf(16166,plain,
! [D: $i > $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ C
@ ^ [E: $i] : $false )
@ ( dsetconstr @ B
@ ^ [E: $i] : ( in @ ( D @ E ) @ E ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,412]) ).
thf(16167,plain,
! [D: $i > $i,C: $i,B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ C
@ ^ [E: $i] : $false )
@ ( dsetconstr @ B
@ ^ [E: $i] : ( in @ ( D @ E ) @ E ) ) ) ),
inference(simp,[status(thm)],[16166]) ).
thf(16249,plain,
! [D: $i > $i,C: $i,B: $i,A: $i] :
( ( A
!= ( dsetconstr @ C
@ ^ [E: $i] : $false ) )
| ( ( setadjoin @ A @ emptyset )
!= ( dsetconstr @ B
@ ^ [E: $i] : ( in @ ( D @ E ) @ E ) ) ) ),
inference(simp,[status(thm)],[16167]) ).
thf(16302,plain,
! [C: $i > $i,B: $i,A: $i] :
( ( setadjoin
@ ( dsetconstr @ B
@ ^ [D: $i] : $false )
@ emptyset )
!= ( dsetconstr @ A
@ ^ [D: $i] : ( in @ ( C @ D ) @ D ) ) ),
inference(simp,[status(thm)],[16249]) ).
thf(56297,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B != sk3 )
| ( A
!= ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ D
@ ( dsetconstr @ sk3
@ ^ [E: $i] : ( E = sk5 ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,54733]) ).
thf(56298,plain,
! [B: $i,A: $i] :
( ~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) ) ) )
@ ( setadjoin @ A @ emptyset ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[56297:[bind(A,$thf( dsetconstr @ D @ ^ [E: $i] : ~ ( in @ E @ ( dsetconstr @ sk3 @ ^ [F: $i] : ( F = sk5 ) ) ) )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(56342,plain,
! [A: $i] :
~ ( in
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ),
inference(simp,[status(thm)],[56298]) ).
thf(3362,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B != sk6 )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
@ emptyset )
!= sk3 )
| ( A
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,694]) ).
thf(3363,plain,
! [A: $i] :
( ~ ( in @ ( setadjoin @ sk5 @ emptyset ) @ ( setadjoin @ A @ emptyset ) )
| ( A != sk6 )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset )
!= sk3 ) ),
inference(pattern_uni,[status(thm)],[3362:[bind(A,$thf( setadjoin @ sk5 @ emptyset )),bind(B,$thf( B ))]]) ).
thf(3404,plain,
( ~ ( in @ ( setadjoin @ sk5 @ emptyset ) @ ( setadjoin @ sk6 @ emptyset ) )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[3363]) ).
thf(54649,plain,
! [A: $i] :
( ~ $true
| ( A = sk6 )
| ( ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) ) )
!= ( in @ A @ ( setadjoin @ sk6 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[53198,32530]) ).
thf(54650,plain,
! [A: $i] :
( ( A = sk6 )
| ( ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) ) )
!= ( in @ A @ ( setadjoin @ sk6 @ emptyset ) ) ) ),
inference(simp,[status(thm)],[54649]) ).
thf(54704,plain,
! [A: $i] :
( ( A = sk6 )
| ( sk5 != A )
| ( ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
!= ( setadjoin @ sk6 @ emptyset ) ) ),
inference(simp,[status(thm)],[54650]) ).
thf(54819,plain,
( ( sk6 = sk5 )
| ( ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
!= ( setadjoin @ sk6 @ emptyset ) ) ),
inference(simp,[status(thm)],[54704]) ).
thf(143,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( in @ ( sk1 @ B @ A ) @ A )
| ( ( in @ ( sk2 @ B @ A ) @ B )
!= ( in @ ( sk1 @ B @ A ) @ A ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[26]) ).
thf(144,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( in @ ( sk1 @ B @ A ) @ A )
| ( ( in @ ( sk2 @ B @ A ) @ B )
!= ( in @ ( sk1 @ B @ A ) @ A ) ) ),
inference(simp,[status(thm)],[143]) ).
thf(1626,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
!= sk5 )
| ( B != sk3 )
| ( A
!= ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,593]) ).
thf(1627,plain,
! [A: $i] :
( ~ ( in @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) @ ( setadjoin @ A @ emptyset ) )
| ( ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
!= sk5 )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[1626:[bind(A,$thf( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )),bind(B,$thf( B ))]]) ).
thf(1675,plain,
( ~ ( in @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) @ ( setadjoin @ sk3 @ emptyset ) )
| ( ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
!= sk5 ) ),
inference(simp,[status(thm)],[1627]) ).
thf(40,plain,
! [E: $i,D: $i,C: $o,B: $i,A: $i] :
( ~ ( in @ D @ B )
| ~ $true
| ~ C
| ( in @ D
@ ( dsetconstr @ B
@ ^ [F: $i] :
( ( C
& ( F = D ) )
| ( ~ C
& ( F = E ) ) ) ) )
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ E @ B ) ) ),
inference(paramod_ordered,[status(thm)],[28,22]) ).
thf(41,plain,
! [E: $i,D: $i,C: $o,B: $i,A: $i] :
( ~ ( in @ D @ B )
| ~ C
| ( in @ D
@ ( dsetconstr @ B
@ ^ [F: $i] :
( ( C
& ( F = D ) )
| ( ~ C
& ( F = E ) ) ) ) )
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ E @ B ) ) ),
inference(simp,[status(thm)],[40]) ).
thf(42,plain,
! [C: $i,B: $i,A: $o] :
( ~ ( in @ B @ ( setadjoin @ C @ emptyset ) )
| ~ A
| ( in @ B
@ ( dsetconstr @ ( setadjoin @ C @ emptyset )
@ ^ [D: $i] :
( ( A
& ( D = B ) )
| ( ~ A
& ( D = C ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[41:[bind(A,$thf( F )),bind(B,$thf( setadjoin @ F @ emptyset )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( F ))]]) ).
thf(86,plain,
! [C: $i,B: $i,A: $o] :
( ~ ( in @ B @ ( setadjoin @ C @ emptyset ) )
| ~ A
| ( in @ B
@ ( dsetconstr @ ( setadjoin @ C @ emptyset )
@ ^ [D: $i] :
( ( A
& ( D = B ) )
| ( ~ A
& ( D = C ) ) ) ) ) ),
inference(simp,[status(thm)],[42]) ).
thf(180,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( in @ A @ sk3 )
| ( B != sk6 ) ),
inference(paramod_ordered,[status(thm)],[19,9]) ).
thf(181,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ sk6 @ emptyset ) )
| ( in @ A @ sk3 ) ),
inference(pattern_uni,[status(thm)],[180:[bind(A,$thf( A )),bind(B,$thf( sk6 ))]]) ).
thf(10000,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B )
| ( in @ sk6 @ sk6 )
| ( A != sk3 )
| ( B
!= ( setadjoin @ sk3 @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[26,7875]) ).
thf(10001,plain,
! [A: $i] :
( ( in @ ( sk1 @ ( setadjoin @ sk3 @ emptyset ) @ A ) @ A )
| ( in @ ( sk2 @ ( setadjoin @ sk3 @ emptyset ) @ A ) @ ( setadjoin @ sk3 @ emptyset ) )
| ( in @ sk6 @ sk6 )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[10000:[bind(A,$thf( A )),bind(B,$thf( setadjoin @ sk3 @ emptyset ))]]) ).
thf(10024,plain,
( ( in @ ( sk1 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ sk3 )
| ( in @ ( sk2 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ ( setadjoin @ sk3 @ emptyset ) )
| ( in @ sk6 @ sk6 ) ),
inference(simp,[status(thm)],[10001]) ).
thf(514,plain,
( ~ $true
| ( ( in
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) )
!= ( in @ sk6 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[9,243]) ).
thf(515,plain,
( ( in
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) )
!= ( in @ sk6 @ sk3 ) ),
inference(simp,[status(thm)],[514]) ).
thf(594,plain,
( ( ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
!= sk6 )
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[515]) ).
thf(1762,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A != sk6 )
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 )
| ( B
!= ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,594]) ).
thf(1763,plain,
! [A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset ) )
| ( A != sk6 )
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 ) ),
inference(pattern_uni,[status(thm)],[1762:[bind(A,$thf( A )),bind(B,$thf( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) ))]]) ).
thf(1806,plain,
( ~ ( in @ sk6
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset ) )
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[1763]) ).
thf(68,plain,
! [E: $o,D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ A )
| ~ ( in @ C @ A )
| ~ ( D
| E )
| ( in @ B
@ ( dsetconstr @ A
@ ^ [F: $i] :
( ( ( D
| E )
& ( F = B ) )
| ( ~ ( D
| E )
& ( F = C ) ) ) ) ) ),
inference(prim_subst,[status(thm)],[22:[bind(A,$thf( A )),bind(B,$thf( E | F ))]]) ).
thf(77,plain,
! [E: $o,D: $o,C: $i,B: $i,A: $i] :
( ( ~ ( in @ B @ A )
| ~ ( in @ C @ A )
| ~ D
| ( in @ B
@ ( dsetconstr @ A
@ ^ [F: $i] :
( ( ( D
| E )
& ( F = B ) )
| ( ~ ( D
| E )
& ( F = C ) ) ) ) ) )
& ( ~ ( in @ B @ A )
| ~ ( in @ C @ A )
| ~ E
| ( in @ B
@ ( dsetconstr @ A
@ ^ [F: $i] :
( ( ( D
| E )
& ( F = B ) )
| ( ~ ( D
| E )
& ( F = C ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[68]) ).
thf(79,plain,
! [E: $o,D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ A )
| ~ ( in @ C @ A )
| ~ E
| ( in @ B
@ ( dsetconstr @ A
@ ^ [F: $i] :
( ( ( D
| E )
& ( F = B ) )
| ( ~ ( D
| E )
& ( F = C ) ) ) ) ) ),
inference(cnfConj,[status(thm)],[77]) ).
thf(81,plain,
! [E: $o,D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ A )
| ~ ( in @ C @ A )
| ~ E
| ( in @ B
@ ( dsetconstr @ A
@ ^ [F: $i] :
( ( ( D
| E )
& ( F = B ) )
| ( ~ ( D
| E )
& ( F = C ) ) ) ) ) ),
inference(simp,[status(thm)],[79]) ).
thf(1752,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
!= sk6 )
| ( B != sk3 )
| ( A
!= ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,594]) ).
thf(1753,plain,
! [A: $i] :
( ~ ( in @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) @ ( setadjoin @ A @ emptyset ) )
| ( ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
!= sk6 )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[1752:[bind(A,$thf( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )),bind(B,$thf( B ))]]) ).
thf(1801,plain,
( ~ ( in @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) @ ( setadjoin @ sk3 @ emptyset ) )
| ( ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
!= sk6 ) ),
inference(simp,[status(thm)],[1753]) ).
thf(29440,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A
!= ( setadjoin @ sk3 @ emptyset ) )
| ( B
!= ( setadjoin
@ ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ D @ sk3 ) )
@ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,27664]) ).
thf(29441,plain,
! [B: $i,A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ sk3 ) )
@ emptyset )
@ emptyset ) )
| ( A
!= ( setadjoin @ sk3 @ emptyset ) ) ),
inference(pattern_uni,[status(thm)],[29440:[bind(A,$thf( A )),bind(B,$thf( setadjoin @ ( dsetconstr @ F @ ^ [E: $i] : ~ ( in @ E @ sk3 ) ) @ emptyset )),bind(C,$thf( F ))]]) ).
thf(29447,plain,
! [A: $i] :
~ ( in @ ( setadjoin @ sk3 @ emptyset )
@ ( setadjoin
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B @ sk3 ) )
@ emptyset )
@ emptyset ) ),
inference(simp,[status(thm)],[29441]) ).
thf(55,plain,
! [H: $i,G: $i,F: $o,E: $i,D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ ( in @ D @ A )
| ~ B
| ~ $true
| ~ ( in @ H @ E )
| ~ F
| ( in @ G
@ ( dsetconstr @ E
@ ^ [I: $i] :
( ( F
& ( I = G ) )
| ( ~ F
& ( I = H ) ) ) ) )
| ( ( in @ C
@ ( dsetconstr @ A
@ ^ [I: $i] :
( ( B
& ( I = C ) )
| ( ~ B
& ( I = D ) ) ) ) )
!= ( in @ G @ E ) ) ),
inference(paramod_ordered,[status(thm)],[22,22]) ).
thf(56,plain,
! [H: $i,G: $i,F: $o,E: $i,D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ ( in @ D @ A )
| ~ B
| ~ ( in @ H @ E )
| ~ F
| ( in @ G
@ ( dsetconstr @ E
@ ^ [I: $i] :
( ( F
& ( I = G ) )
| ( ~ F
& ( I = H ) ) ) ) )
| ( ( in @ C
@ ( dsetconstr @ A
@ ^ [I: $i] :
( ( B
& ( I = C ) )
| ( ~ B
& ( I = D ) ) ) ) )
!= ( in @ G @ E ) ) ),
inference(simp,[status(thm)],[55]) ).
thf(57,plain,
! [F: $i,E: $i,D: $o,C: $i,B: $i,A: $o] :
( ~ ( in @ B @ F )
| ~ ( in @ C @ F )
| ~ A
| ~ ( in @ E
@ ( dsetconstr @ F
@ ^ [G: $i] :
( ( A
& ( G = B ) )
| ( ~ A
& ( G = C ) ) ) ) )
| ~ D
| ( in @ B
@ ( dsetconstr
@ ( dsetconstr @ F
@ ^ [G: $i] :
( ( A
& ( G = B ) )
| ( ~ A
& ( G = C ) ) ) )
@ ^ [G: $i] :
( ( D
& ( G = B ) )
| ( ~ D
& ( G = E ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[56:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( dsetconstr @ I @ ^ [J: $i] : ( ( B & ( J = C ) ) | ( ~ ( B ) & ( J = D ) ) ) )),bind(F,$thf( F )),bind(G,$thf( C )),bind(H,$thf( H ))]]) ).
thf(91,plain,
! [F: $i,E: $i,D: $o,C: $i,B: $i,A: $o] :
( ~ ( in @ B @ F )
| ~ ( in @ C @ F )
| ~ A
| ~ ( in @ E
@ ( dsetconstr @ F
@ ^ [G: $i] :
( ( A
& ( G = B ) )
| ( ~ A
& ( G = C ) ) ) ) )
| ~ D
| ( in @ B
@ ( dsetconstr
@ ( dsetconstr @ F
@ ^ [G: $i] :
( ( A
& ( G = B ) )
| ( ~ A
& ( G = C ) ) ) )
@ ^ [G: $i] :
( ( D
& ( G = B ) )
| ( ~ D
& ( G = E ) ) ) ) ) ),
inference(simp,[status(thm)],[57]) ).
thf(433,plain,
! [A: $i] :
( ~ $true
| ( ( in
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ ( setadjoin @ sk3 @ emptyset ) )
!= ( in @ sk6 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[9,430]) ).
thf(434,plain,
! [A: $i] :
( ( in
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ ( setadjoin @ sk3 @ emptyset ) )
!= ( in @ sk6 @ sk3 ) ),
inference(simp,[status(thm)],[433]) ).
thf(483,plain,
! [A: $i] :
( ( ( dsetconstr @ A
@ ^ [B: $i] : $false )
!= sk6 )
| ( ( setadjoin @ sk3 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[434]) ).
thf(3530,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B != sk5 )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
@ emptyset )
!= sk3 )
| ( A
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,700]) ).
thf(3531,plain,
! [A: $i] :
( ~ ( in @ ( setadjoin @ sk5 @ emptyset ) @ ( setadjoin @ A @ emptyset ) )
| ( A != sk5 )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset )
!= sk3 ) ),
inference(pattern_uni,[status(thm)],[3530:[bind(A,$thf( setadjoin @ sk5 @ emptyset )),bind(B,$thf( B ))]]) ).
thf(3583,plain,
( ~ ( in @ ( setadjoin @ sk5 @ emptyset ) @ ( setadjoin @ sk5 @ emptyset ) )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[3531]) ).
thf(107,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B )
| ( in @ sk6 @ A )
| ( B != sk3 ) ),
inference(paramod_ordered,[status(thm)],[26,9]) ).
thf(108,plain,
! [A: $i] :
( ( in @ ( sk1 @ sk3 @ A ) @ A )
| ( in @ ( sk2 @ sk3 @ A ) @ sk3 )
| ( in @ sk6 @ A ) ),
inference(pattern_uni,[status(thm)],[107:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(10660,plain,
! [C: $i > $i,B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ emptyset
@ ( dsetconstr @ B
@ ^ [D: $i] :
( in
@ ( dsetconstr @ ( C @ D )
@ ^ [E: $i] : $false )
@ ( setadjoin @ sk3 @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,504]) ).
thf(10661,plain,
! [C: $i > $i,B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in @ emptyset
@ ( dsetconstr @ B
@ ^ [D: $i] :
( in
@ ( dsetconstr @ ( C @ D )
@ ^ [E: $i] : $false )
@ ( setadjoin @ sk3 @ D ) ) ) ) ),
inference(simp,[status(thm)],[10660]) ).
thf(10745,plain,
! [C: $i > $i,B: $i,A: $i] :
( ( A != emptyset )
| ( ( setadjoin @ A @ emptyset )
!= ( dsetconstr @ B
@ ^ [D: $i] :
( in
@ ( dsetconstr @ ( C @ D )
@ ^ [E: $i] : $false )
@ ( setadjoin @ sk3 @ D ) ) ) ) ),
inference(simp,[status(thm)],[10661]) ).
thf(10792,plain,
! [B: $i > $i,A: $i] :
( ( dsetconstr @ A
@ ^ [C: $i] :
( in
@ ( dsetconstr @ ( B @ C )
@ ^ [D: $i] : $false )
@ ( setadjoin @ sk3 @ C ) ) )
!= ( setadjoin @ emptyset @ emptyset ) ),
inference(simp,[status(thm)],[10745]) ).
thf(1376,plain,
! [B: $i,A: $i] :
~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ ( dsetconstr @ A
@ ^ [C: $i] : ( in @ sk3 @ ( setadjoin @ C @ emptyset ) ) ) ),
inference(pre_uni,[status(thm)],[1353:[bind(A,$thf( A )),bind(B,$thf( ^ [E: $i] : ( in @ sk3 @ ( setadjoin @ E @ emptyset ) ) )),bind(C,$thf( dsetconstr @ D @ ^ [E: $i] : $false )),bind(D,$thf( D ))]]) ).
thf(1399,plain,
! [B: $i,A: $i] :
~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ ( dsetconstr @ A
@ ^ [C: $i] : ( in @ sk3 @ ( setadjoin @ C @ emptyset ) ) ) ),
inference(simp,[status(thm)],[1376]) ).
thf(11048,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ ( dsetconstr @ B
@ ^ [D: $i] : ( in @ sk3 @ ( setadjoin @ D @ emptyset ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,1399]) ).
thf(11049,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ C
@ ^ [D: $i] : $false )
@ ( dsetconstr @ B
@ ^ [D: $i] : ( in @ sk3 @ ( setadjoin @ D @ emptyset ) ) ) ) ),
inference(simp,[status(thm)],[11048]) ).
thf(11155,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( dsetconstr @ C
@ ^ [D: $i] : $false ) )
| ( ( setadjoin @ A @ emptyset )
!= ( dsetconstr @ B
@ ^ [D: $i] : ( in @ sk3 @ ( setadjoin @ D @ emptyset ) ) ) ) ),
inference(simp,[status(thm)],[11049]) ).
thf(11173,plain,
! [B: $i,A: $i] :
( ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ emptyset )
!= ( dsetconstr @ A
@ ^ [C: $i] : ( in @ sk3 @ ( setadjoin @ C @ emptyset ) ) ) ),
inference(simp,[status(thm)],[11155]) ).
thf(56305,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A != sk3 )
| ( B
!= ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ D
@ ( dsetconstr @ sk3
@ ^ [E: $i] : ( E = sk5 ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,54733]) ).
thf(56306,plain,
! [B: $i,A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) ) ) )
@ emptyset ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[56305:[bind(A,$thf( A )),bind(B,$thf( dsetconstr @ D @ ^ [E: $i] : ~ ( in @ E @ ( dsetconstr @ sk3 @ ^ [F: $i] : ( F = sk5 ) ) ) )),bind(C,$thf( D ))]]) ).
thf(56350,plain,
! [A: $i] :
~ ( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) ) )
@ emptyset ) ),
inference(simp,[status(thm)],[56306]) ).
thf(127,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B )
| ( B
!= ( setadjoin @ sk5 @ emptyset ) )
| ( A
!= ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) ) ),
inference(paramod_ordered,[status(thm)],[26,35]) ).
thf(128,plain,
! [A: $i] :
( ( in
@ ( sk1 @ A
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) ) )
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) ) )
| ( in
@ ( sk2 @ A
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) ) )
@ A )
| ( A
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(pattern_uni,[status(thm)],[127:[bind(A,$thf( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) )),bind(B,$thf( B ))]]) ).
thf(146,plain,
( ( in
@ ( sk1 @ ( setadjoin @ sk5 @ emptyset )
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) ) )
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) ) )
| ( in
@ ( sk2 @ ( setadjoin @ sk5 @ emptyset )
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) ) )
@ ( setadjoin @ sk5 @ emptyset ) ) ),
inference(simp,[status(thm)],[128]) ).
thf(778,plain,
! [B: $i,A: $i] :
( ( in
@ ( sk1 @ ( setadjoin @ sk5 @ emptyset )
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) )
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) )
| ( A = B )
| ~ $true
| ( ( in
@ ( sk2 @ ( setadjoin @ sk5 @ emptyset )
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) )
@ ( setadjoin @ sk5 @ emptyset ) )
!= ( in @ A @ ( setadjoin @ B @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[146,19]) ).
thf(779,plain,
! [B: $i,A: $i] :
( ( in
@ ( sk1 @ ( setadjoin @ sk5 @ emptyset )
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) )
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) )
| ( A = B )
| ( ( in
@ ( sk2 @ ( setadjoin @ sk5 @ emptyset )
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) )
@ ( setadjoin @ sk5 @ emptyset ) )
!= ( in @ A @ ( setadjoin @ B @ emptyset ) ) ) ),
inference(simp,[status(thm)],[778]) ).
thf(780,plain,
( ( in
@ ( sk1 @ ( setadjoin @ sk5 @ emptyset )
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) ) )
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) ) )
| ( ( sk2 @ ( setadjoin @ sk5 @ emptyset )
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) ) )
= sk5 ) ),
inference(pattern_uni,[status(thm)],[779:[bind(A,$thf( sk2 @ ( setadjoin @ sk5 @ emptyset ) @ ( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) ) )),bind(B,$thf( sk5 ))]]) ).
thf(178,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( in @ sk6 @ B )
| ( A != sk3 ) ),
inference(paramod_ordered,[status(thm)],[19,9]) ).
thf(179,plain,
! [A: $i] :
( ~ ( in @ sk3 @ ( setadjoin @ A @ emptyset ) )
| ( in @ sk6 @ A ) ),
inference(pattern_uni,[status(thm)],[178:[bind(A,$thf( sk3 ))]]) ).
thf(267,plain,
! [A: $i] :
( ~ ( in @ sk3 @ ( setadjoin @ A @ emptyset ) )
| ( in @ sk6 @ A ) ),
inference(simp,[status(thm)],[179]) ).
thf(78,plain,
! [E: $o,D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ A )
| ~ ( in @ C @ A )
| ~ D
| ( in @ B
@ ( dsetconstr @ A
@ ^ [F: $i] :
( ( ( D
| E )
& ( F = B ) )
| ( ~ ( D
| E )
& ( F = C ) ) ) ) ) ),
inference(cnfConj,[status(thm)],[77]) ).
thf(80,plain,
! [E: $o,D: $o,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ A )
| ~ ( in @ C @ A )
| ~ D
| ( in @ B
@ ( dsetconstr @ A
@ ^ [F: $i] :
( ( ( D
| E )
& ( F = B ) )
| ( ~ ( D
| E )
& ( F = C ) ) ) ) ) ),
inference(simp,[status(thm)],[78]) ).
thf(50777,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( sk14 = sk5 )
| ( B != sk3 )
| ( A
!= ( setadjoin @ sk6 @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,50691]) ).
thf(50778,plain,
! [A: $i] :
( ~ ( in @ ( setadjoin @ sk6 @ emptyset ) @ ( setadjoin @ A @ emptyset ) )
| ( sk14 = sk5 )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[50777:[bind(A,$thf( setadjoin @ sk6 @ emptyset )),bind(B,$thf( B ))]]) ).
thf(50804,plain,
( ~ ( in @ ( setadjoin @ sk6 @ emptyset ) @ ( setadjoin @ sk3 @ emptyset ) )
| ( sk14 = sk5 ) ),
inference(simp,[status(thm)],[50778]) ).
thf(34052,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B )
| ( sk6 = sk5 )
| ( A != sk3 )
| ( B
!= ( setadjoin @ sk6 @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[26,33969]) ).
thf(34053,plain,
! [A: $i] :
( ( in @ ( sk1 @ ( setadjoin @ sk6 @ emptyset ) @ A ) @ A )
| ( in @ ( sk2 @ ( setadjoin @ sk6 @ emptyset ) @ A ) @ ( setadjoin @ sk6 @ emptyset ) )
| ( sk6 = sk5 )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[34052:[bind(A,$thf( A )),bind(B,$thf( setadjoin @ sk6 @ emptyset ))]]) ).
thf(34079,plain,
( ( in @ ( sk1 @ ( setadjoin @ sk6 @ emptyset ) @ sk3 ) @ sk3 )
| ( in @ ( sk2 @ ( setadjoin @ sk6 @ emptyset ) @ sk3 ) @ ( setadjoin @ sk6 @ emptyset ) )
| ( sk6 = sk5 ) ),
inference(simp,[status(thm)],[34053]) ).
thf(1519,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B
!= ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) )
| ( A
!= ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
@ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,601]) ).
thf(1520,plain,
! [A: $i] :
( ~ ( in
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset )
@ ( setadjoin @ A @ emptyset ) )
| ( A
!= ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ) ),
inference(pattern_uni,[status(thm)],[1519:[bind(A,$thf( setadjoin @ ( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) ) @ emptyset )),bind(B,$thf( B ))]]) ).
thf(1551,plain,
~ ( in
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
@ ( setadjoin @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) @ emptyset ) ),
inference(simp,[status(thm)],[1520]) ).
thf(1746,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B != sk6 )
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 )
| ( A
!= ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,594]) ).
thf(1747,plain,
! [A: $i] :
( ~ ( in
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ ( setadjoin @ A @ emptyset ) )
| ( A != sk6 )
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 ) ),
inference(pattern_uni,[status(thm)],[1746:[bind(A,$thf( dsetconstr @ sk3 @ ^ [C: $i] : ( C = sk5 ) )),bind(B,$thf( B ))]]) ).
thf(1798,plain,
( ~ ( in
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ sk6 @ emptyset ) )
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[1747]) ).
thf(56179,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B != sk3 )
| ( A
!= ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [E: $i] : ( E = D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,54732]) ).
thf(56180,plain,
! [B: $i,A: $i] :
( ~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) )
@ ( setadjoin @ A @ emptyset ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[56179:[bind(A,$thf( dsetconstr @ D @ ^ [E: $i] : ~ ( in @ sk5 @ ( dsetconstr @ sk3 @ ^ [F: $i] : ( F = E ) ) ) )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(56218,plain,
! [A: $i] :
~ ( in
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = B ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ),
inference(simp,[status(thm)],[56180]) ).
thf(59199,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,56218]) ).
thf(59200,plain,
! [B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[59199]) ).
thf(59415,plain,
! [B: $i,A: $i] :
( ( A
!= ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) ) )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[59200]) ).
thf(59461,plain,
! [A: $i] :
( ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ sk5
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = B ) ) ) )
@ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ),
inference(simp,[status(thm)],[59415]) ).
thf(13854,plain,
! [B: $i,A: $i] :
( ( ( setadjoin @ A @ emptyset )
!= ( dsetconstr @ B
@ ^ [C: $i] : $false ) )
| ( emptyset != emptyset ) ),
inference(simp,[status(thm)],[5206]) ).
thf(14017,plain,
! [B: $i,A: $i] :
( ( setadjoin @ A @ emptyset )
!= ( dsetconstr @ B
@ ^ [C: $i] : $false ) ),
inference(simp,[status(thm)],[13854]) ).
thf(3378,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A != sk6 )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
@ emptyset )
!= sk3 )
| ( B
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,694]) ).
thf(3379,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) )
| ( A != sk6 )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset )
!= sk3 ) ),
inference(pattern_uni,[status(thm)],[3378:[bind(A,$thf( A )),bind(B,$thf( setadjoin @ sk5 @ emptyset ))]]) ).
thf(3412,plain,
( ~ ( in @ sk6 @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[3379]) ).
thf(32391,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( A != sk3 )
| ( B
!= ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ D
@ ( dsetconstr @ sk3
@ ^ [E: $i] : ( E = D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,32100]) ).
thf(32392,plain,
! [B: $i,A: $i] :
( ~ ( in @ A
@ ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) )
@ emptyset ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[32391:[bind(A,$thf( A )),bind(B,$thf( dsetconstr @ D @ ^ [E: $i] : ~ ( in @ E @ ( dsetconstr @ sk3 @ ^ [F: $i] : ( F = E ) ) ) )),bind(C,$thf( D ))]]) ).
thf(32402,plain,
! [A: $i] :
~ ( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = B ) ) ) )
@ emptyset ) ),
inference(simp,[status(thm)],[32392]) ).
thf(3222,plain,
! [D: $i,C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ~ $true
| ( ( B @ C )
!= ( in
@ ( dsetconstr @ D
@ ^ [E: $i] :
~ ( in @ E @ E ) )
@ ( dsetconstr @ D
@ ^ [E: $i] :
~ ( in @ E @ E ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,340]) ).
thf(3223,plain,
! [D: $i,C: $i,B: $i > $o,A: $i] :
( ~ ( in @ C @ ( dsetconstr @ A @ B ) )
| ( ( B @ C )
!= ( in
@ ( dsetconstr @ D
@ ^ [E: $i] :
~ ( in @ E @ E ) )
@ ( dsetconstr @ D
@ ^ [E: $i] :
~ ( in @ E @ E ) ) ) ) ),
inference(simp,[status(thm)],[3222]) ).
thf(3235,plain,
! [B: $i,A: $i] :
~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ C ) )
@ ( dsetconstr @ A
@ ^ [C: $i] : ( in @ C @ C ) ) ),
inference(pre_uni,[status(thm)],[3223:[bind(A,$thf( A )),bind(B,$thf( ^ [E: $i] : ( in @ E @ E ) )),bind(C,$thf( dsetconstr @ D @ ^ [E: $i] : ~ ( in @ E @ E ) )),bind(D,$thf( D ))]]) ).
thf(3256,plain,
! [B: $i,A: $i] :
~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ C ) )
@ ( dsetconstr @ A
@ ^ [C: $i] : ( in @ C @ C ) ) ),
inference(simp,[status(thm)],[3235]) ).
thf(38678,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,32398]) ).
thf(38679,plain,
! [B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[38678]) ).
thf(38835,plain,
! [B: $i,A: $i] :
( ( A
!= ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = C ) ) ) ) )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[38679]) ).
thf(38929,plain,
! [A: $i] :
( ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = B ) ) ) )
@ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ),
inference(simp,[status(thm)],[38835]) ).
thf(43,plain,
! [D: $i,C: $i,B: $o,A: $i] :
( ~ $true
| ~ ( in @ D @ A )
| ~ B
| ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) )
| ( ( in @ sk6 @ sk3 )
!= ( in @ C @ A ) ) ),
inference(paramod_ordered,[status(thm)],[9,22]) ).
thf(44,plain,
! [D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ D @ A )
| ~ B
| ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) )
| ( ( in @ sk6 @ sk3 )
!= ( in @ C @ A ) ) ),
inference(simp,[status(thm)],[43]) ).
thf(45,plain,
! [B: $i,A: $o] :
( ~ ( in @ B @ sk3 )
| ~ A
| ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [C: $i] :
( ( A
& ( C = sk6 ) )
| ( ~ A
& ( C = B ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[44:[bind(A,$thf( sk3 )),bind(B,$thf( B )),bind(C,$thf( sk6 ))]]) ).
thf(87,plain,
! [B: $i,A: $o] :
( ~ ( in @ B @ sk3 )
| ~ A
| ( in @ sk6
@ ( dsetconstr @ sk3
@ ^ [C: $i] :
( ( A
& ( C = sk6 ) )
| ( ~ A
& ( C = B ) ) ) ) ) ),
inference(simp,[status(thm)],[45]) ).
thf(35505,plain,
( ~ $true
| ( ( setadjoin @ sk5 @ emptyset )
!= sk6 )
| ( ( in
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ sk6 @ emptyset ) )
!= ( in @ sk5 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[13,33318]) ).
thf(35506,plain,
( ( ( setadjoin @ sk5 @ emptyset )
!= sk6 )
| ( ( in
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ sk6 @ emptyset ) )
!= ( in @ sk5 @ sk3 ) ) ),
inference(simp,[status(thm)],[35505]) ).
thf(35690,plain,
( ( ( setadjoin @ sk5 @ emptyset )
!= sk6 )
| ( ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
!= sk5 )
| ( ( setadjoin @ sk6 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[35506]) ).
thf(1768,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
!= sk6 )
| ( A != sk3 )
| ( B
!= ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,594]) ).
thf(1769,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) @ emptyset ) )
| ( ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
!= sk6 )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[1768:[bind(A,$thf( A )),bind(B,$thf( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ))]]) ).
thf(1807,plain,
( ~ ( in @ sk3 @ ( setadjoin @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) @ emptyset ) )
| ( ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
!= sk6 ) ),
inference(simp,[status(thm)],[1769]) ).
thf(4758,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ D @ D ) )
@ ( dsetconstr @ B
@ ^ [D: $i] : ( in @ D @ D ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,3256]) ).
thf(4759,plain,
! [C: $i,B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ D @ D ) )
@ ( dsetconstr @ B
@ ^ [D: $i] : ( in @ D @ D ) ) ) ),
inference(simp,[status(thm)],[4758]) ).
thf(4802,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( dsetconstr @ C
@ ^ [D: $i] :
~ ( in @ D @ D ) ) )
| ( ( setadjoin @ A @ emptyset )
!= ( dsetconstr @ B
@ ^ [D: $i] : ( in @ D @ D ) ) ) ),
inference(simp,[status(thm)],[4759]) ).
thf(4806,plain,
! [B: $i,A: $i] :
( ( setadjoin
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C @ C ) )
@ emptyset )
!= ( dsetconstr @ A
@ ^ [C: $i] : ( in @ C @ C ) ) ),
inference(simp,[status(thm)],[4802]) ).
thf(113,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B )
| ( in @ A @ sk3 )
| ( B != sk5 ) ),
inference(paramod_ordered,[status(thm)],[26,13]) ).
thf(114,plain,
! [A: $i] :
( ( in @ ( sk1 @ sk5 @ A ) @ A )
| ( in @ ( sk2 @ sk5 @ A ) @ sk5 )
| ( in @ A @ sk3 ) ),
inference(pattern_uni,[status(thm)],[113:[bind(A,$thf( A )),bind(B,$thf( sk5 ))]]) ).
thf(67,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ A )
| ~ ( in @ C @ A )
| ~ ( in @ D @ E )
| ( in @ B
@ ( dsetconstr @ A
@ ^ [F: $i] :
( ( ( in @ D @ E )
& ( F = B ) )
| ( ~ ( in @ D @ E )
& ( F = C ) ) ) ) ) ),
inference(prim_subst,[status(thm)],[22:[bind(A,$thf( A )),bind(B,$thf( in @ E @ F ))]]) ).
thf(75,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( in @ B @ A )
| ~ ( in @ C @ A )
| ~ ( in @ D @ E )
| ( in @ B
@ ( dsetconstr @ A
@ ^ [F: $i] :
( ( ( in @ D @ E )
& ( F = B ) )
| ( ~ ( in @ D @ E )
& ( F = C ) ) ) ) ) ),
inference(simp,[status(thm)],[67]) ).
thf(435,plain,
! [A: $i] :
( ~ $true
| ( ( in
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ ( setadjoin @ sk3 @ emptyset ) )
!= ( in @ sk5 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[13,430]) ).
thf(436,plain,
! [A: $i] :
( ( in
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ ( setadjoin @ sk3 @ emptyset ) )
!= ( in @ sk5 @ sk3 ) ),
inference(simp,[status(thm)],[435]) ).
thf(478,plain,
! [A: $i] :
( ( ( dsetconstr @ A
@ ^ [B: $i] : $false )
!= sk5 )
| ( ( setadjoin @ sk3 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[436]) ).
thf(23415,plain,
! [A: $i] :
( ( in @ ( sk1 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ sk3 )
| ( in @ sk6 @ sk6 )
| ~ $true
| ( in @ sk6 @ A )
| ( ( in @ ( sk2 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ ( setadjoin @ sk3 @ emptyset ) )
!= ( in @ A @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[10024,183]) ).
thf(23416,plain,
! [A: $i] :
( ( in @ ( sk1 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ sk3 )
| ( in @ sk6 @ sk6 )
| ( in @ sk6 @ A )
| ( ( in @ ( sk2 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ ( setadjoin @ sk3 @ emptyset ) )
!= ( in @ A @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(simp,[status(thm)],[23415]) ).
thf(23417,plain,
( ( in @ ( sk1 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ sk3 )
| ( in @ sk6 @ sk6 )
| ( in @ sk6 @ ( sk2 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) ) ),
inference(pattern_uni,[status(thm)],[23416:[bind(A,$thf( sk2 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ))]]) ).
thf(61,plain,
! [D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ B
| ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) )
| ( ( in @ D @ A )
!= ( in @ C @ A ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[22]) ).
thf(69,plain,
! [C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ B
| ( in @ C
@ ( dsetconstr @ A
@ ^ [D: $i] :
( ( B
& ( D = C ) )
| ( ~ B
& ( D = C ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[61:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(82,plain,
! [C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ B
| ( in @ C
@ ( dsetconstr @ A
@ ^ [D: $i] :
( ( B
& ( D = C ) )
| ( ~ B
& ( D = C ) ) ) ) ) ),
inference(simp,[status(thm)],[69]) ).
thf(9302,plain,
( ~ $true
| ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 )
| ( ( in @ sk5
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset ) )
!= ( in @ sk5 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[13,1680]) ).
thf(9303,plain,
( ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 )
| ( ( in @ sk5
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset ) )
!= ( in @ sk5 @ sk3 ) ) ),
inference(simp,[status(thm)],[9302]) ).
thf(9521,plain,
( ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 )
| ( sk5 != sk5 )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[9303]) ).
thf(9542,plain,
( ( ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset )
!= sk3 )
| ( ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[9521]) ).
thf(60469,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ ( setadjoin @ sk6 @ emptyset ) @ sk3 ) @ sk3 )
| ( sk6 = sk5 )
| ( A = B )
| ~ $true
| ( ( in @ ( sk2 @ ( setadjoin @ sk6 @ emptyset ) @ sk3 ) @ ( setadjoin @ sk6 @ emptyset ) )
!= ( in @ A @ ( setadjoin @ B @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[34079,19]) ).
thf(60470,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ ( setadjoin @ sk6 @ emptyset ) @ sk3 ) @ sk3 )
| ( sk6 = sk5 )
| ( A = B )
| ( ( in @ ( sk2 @ ( setadjoin @ sk6 @ emptyset ) @ sk3 ) @ ( setadjoin @ sk6 @ emptyset ) )
!= ( in @ A @ ( setadjoin @ B @ emptyset ) ) ) ),
inference(simp,[status(thm)],[60469]) ).
thf(60471,plain,
( ( in @ ( sk1 @ ( setadjoin @ sk6 @ emptyset ) @ sk3 ) @ sk3 )
| ( sk6 = sk5 )
| ( ( sk2 @ ( setadjoin @ sk6 @ emptyset ) @ sk3 )
= sk6 ) ),
inference(pattern_uni,[status(thm)],[60470:[bind(A,$thf( sk2 @ ( setadjoin @ sk6 @ emptyset ) @ sk3 )),bind(B,$thf( sk6 ))]]) ).
thf(184,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ $true
| ( ( in @ sk6 @ sk3 )
!= ( in @ A @ ( setadjoin @ B @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,19]) ).
thf(185,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( ( in @ sk6 @ sk3 )
!= ( in @ A @ ( setadjoin @ B @ emptyset ) ) ) ),
inference(simp,[status(thm)],[184]) ).
thf(237,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( sk6 != A )
| ( ( setadjoin @ B @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[185]) ).
thf(262,plain,
! [A: $i] :
( ( sk6 = A )
| ( ( setadjoin @ A @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[237]) ).
thf(12750,plain,
! [A: $i] :
( ~ $true
| ( in @ sk5 @ A )
| ( ( in @ sk6 @ sk3 )
!= ( in @ A @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,193]) ).
thf(12751,plain,
! [A: $i] :
( ( in @ sk5 @ A )
| ( ( in @ sk6 @ sk3 )
!= ( in @ A @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(simp,[status(thm)],[12750]) ).
thf(12908,plain,
! [A: $i] :
( ( in @ sk5 @ A )
| ( sk6 != A )
| ( ( setadjoin @ sk3 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[12751]) ).
thf(12972,plain,
( ( in @ sk5 @ sk6 )
| ( ( setadjoin @ sk3 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[12908]) ).
thf(1311,plain,
! [A: $i] :
( ~ $true
| ( ( in @ sk5 @ sk3 )
!= ( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[13,431]) ).
thf(1312,plain,
! [A: $i] :
( ( in @ sk5 @ sk3 )
!= ( in @ sk3
@ ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset ) ) ),
inference(simp,[status(thm)],[1311]) ).
thf(1380,plain,
! [A: $i] :
( ( sk5 != sk3 )
| ( ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[1312]) ).
thf(33540,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ sk6 @ emptyset ) )
| ( sk6 != sk3 )
| ( A
!= ( dsetconstr @ B
@ ^ [C: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[32530,410]) ).
thf(33541,plain,
! [A: $i] :
( ~ ( in
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ ( setadjoin @ sk6 @ emptyset ) )
| ( sk6 != sk3 ) ),
inference(pattern_uni,[status(thm)],[33540:[bind(A,$thf( dsetconstr @ C @ ^ [D: $i] : $false )),bind(B,$thf( C ))]]) ).
thf(33871,plain,
! [A: $i] :
( ~ ( in
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ ( setadjoin @ sk6 @ emptyset ) )
| ( sk6 != sk3 ) ),
inference(simp,[status(thm)],[33541]) ).
thf(135,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ B @ A ) @ A )
| ( in @ ( sk2 @ B @ A ) @ B )
| ( ( dsetconstr @ A
@ ^ [C: $i] : ( C = sk5 ) )
!= ( setadjoin @ sk5 @ emptyset ) )
| ( B != sk3 ) ),
inference(paramod_ordered,[status(thm)],[26,35]) ).
thf(136,plain,
! [A: $i] :
( ( in @ ( sk1 @ sk3 @ A ) @ A )
| ( in @ ( sk2 @ sk3 @ A ) @ sk3 )
| ( ( dsetconstr @ A
@ ^ [B: $i] : ( B = sk5 ) )
!= ( setadjoin @ sk5 @ emptyset ) ) ),
inference(pattern_uni,[status(thm)],[135:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(55046,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ sk6 @ emptyset ) )
| ( sk6 = sk5 )
| ( A != sk17 ) ),
inference(paramod_ordered,[status(thm)],[32530,55018]) ).
thf(55047,plain,
( ~ ( in @ sk17 @ ( setadjoin @ sk6 @ emptyset ) )
| ( sk6 = sk5 ) ),
inference(pattern_uni,[status(thm)],[55046:[bind(A,$thf( sk17 ))]]) ).
thf(56366,plain,
( ~ ( in @ sk5 @ ( setadjoin @ sk6 @ emptyset ) )
| ( sk6 = sk5 ) ),
inference(rewrite,[status(thm)],[55047,55018]) ).
thf(186,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( in @ B @ sk3 )
| ( A != sk5 ) ),
inference(paramod_ordered,[status(thm)],[19,13]) ).
thf(187,plain,
! [A: $i] :
( ~ ( in @ sk5 @ ( setadjoin @ A @ emptyset ) )
| ( in @ A @ sk3 ) ),
inference(pattern_uni,[status(thm)],[186:[bind(A,$thf( sk5 ))]]) ).
thf(268,plain,
! [A: $i] :
( ~ ( in @ sk5 @ ( setadjoin @ A @ emptyset ) )
| ( in @ A @ sk3 ) ),
inference(simp,[status(thm)],[187]) ).
thf(5684,plain,
! [C: $i,B: $i > $o,A: $i] :
( ( in
@ ( sk1
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) )
@ ( setadjoin @ sk5 @ emptyset ) )
@ ( setadjoin @ sk5 @ emptyset ) )
| ~ $true
| ( B @ C )
| ( ( in
@ ( sk2
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) )
@ ( setadjoin @ sk5 @ emptyset ) )
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) ) )
!= ( in @ C @ ( dsetconstr @ A @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[149,17]) ).
thf(5685,plain,
! [C: $i,B: $i > $o,A: $i] :
( ( in
@ ( sk1
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) )
@ ( setadjoin @ sk5 @ emptyset ) )
@ ( setadjoin @ sk5 @ emptyset ) )
| ( B @ C )
| ( ( in
@ ( sk2
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) )
@ ( setadjoin @ sk5 @ emptyset ) )
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) ) )
!= ( in @ C @ ( dsetconstr @ A @ B ) ) ) ),
inference(simp,[status(thm)],[5684]) ).
thf(5686,plain,
( ( in
@ ( sk1
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ sk5 @ emptyset ) )
@ ( setadjoin @ sk5 @ emptyset ) )
| ( ( sk2
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ sk5 @ emptyset ) )
= sk5 ) ),
inference(pattern_uni,[status(thm)],[5685:[bind(A,$thf( sk3 )),bind(B,$thf( ^ [D: $i] : ( D = sk5 ) )),bind(C,$thf( sk2 @ ( dsetconstr @ sk3 @ ^ [D: $i] : ( D = sk5 ) ) @ ( setadjoin @ sk5 @ emptyset ) ))]]) ).
thf(5741,plain,
( ( ( sk2
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ sk5 @ emptyset ) )
= sk5 )
| ( in
@ ( sk1
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ ( setadjoin @ sk5 @ emptyset ) )
@ ( setadjoin @ sk5 @ emptyset ) ) ),
inference(lifteq,[status(thm)],[5686]) ).
thf(596,plain,
! [A: $i] :
~ ( in
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ ( dsetconstr @ A
@ ^ [B: $i] : ( in @ B @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ) ) ),
inference(pre_uni,[status(thm)],[557:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : ( in @ D @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ) )),bind(C,$thf( dsetconstr @ sk3 @ ^ [D: $i] : ( D = sk5 ) ))]]) ).
thf(52,plain,
! [D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ $true
| ~ B
| ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) )
| ( ( in @ sk5 @ sk3 )
!= ( in @ D @ A ) ) ),
inference(paramod_ordered,[status(thm)],[13,22]) ).
thf(53,plain,
! [D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ B
| ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) )
| ( ( in @ sk5 @ sk3 )
!= ( in @ D @ A ) ) ),
inference(simp,[status(thm)],[52]) ).
thf(54,plain,
! [B: $i,A: $o] :
( ~ ( in @ B @ sk3 )
| ~ A
| ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] :
( ( A
& ( C = B ) )
| ( ~ A
& ( C = sk5 ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[53:[bind(A,$thf( sk3 )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( sk5 ))]]) ).
thf(90,plain,
! [B: $i,A: $o] :
( ~ ( in @ B @ sk3 )
| ~ A
| ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] :
( ( A
& ( C = B ) )
| ( ~ A
& ( C = sk5 ) ) ) ) ) ),
inference(simp,[status(thm)],[54]) ).
thf(55182,plain,
( ~ $true
| ( sk6 = sk5 )
| ( ( in @ sk6 @ ( setadjoin @ sk5 @ emptyset ) )
!= ( in @ sk6 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[9,55053]) ).
thf(55183,plain,
( ( sk6 = sk5 )
| ( ( in @ sk6 @ ( setadjoin @ sk5 @ emptyset ) )
!= ( in @ sk6 @ sk3 ) ) ),
inference(simp,[status(thm)],[55182]) ).
thf(55432,plain,
( ( sk6 = sk5 )
| ( sk6 != sk6 )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[55183]) ).
thf(55490,plain,
( ( sk6 = sk5 )
| ( ( setadjoin @ sk5 @ emptyset )
!= sk3 ) ),
inference(simp,[status(thm)],[55432]) ).
thf(41694,plain,
( ( sk9 = sk5 )
| ~ ( in @ sk3 @ ( setadjoin @ ( setadjoin @ sk6 @ emptyset ) @ emptyset ) ) ),
inference(func_ext,[status(esa)],[39500]) ).
thf(41939,plain,
( ( sk9 = sk5 )
| ~ ( in @ sk3 @ ( setadjoin @ ( setadjoin @ sk6 @ emptyset ) @ emptyset ) ) ),
inference(lifteq,[status(thm)],[41694]) ).
thf(23418,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ sk3 )
| ( in @ sk6 @ sk6 )
| ( A = B )
| ~ $true
| ( ( in @ ( sk2 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ ( setadjoin @ sk3 @ emptyset ) )
!= ( in @ A @ ( setadjoin @ B @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[10024,19]) ).
thf(23419,plain,
! [B: $i,A: $i] :
( ( in @ ( sk1 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ sk3 )
| ( in @ sk6 @ sk6 )
| ( A = B )
| ( ( in @ ( sk2 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ ( setadjoin @ sk3 @ emptyset ) )
!= ( in @ A @ ( setadjoin @ B @ emptyset ) ) ) ),
inference(simp,[status(thm)],[23418]) ).
thf(23420,plain,
( ( in @ ( sk1 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ sk3 )
| ( in @ sk6 @ sk6 )
| ( ( sk2 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 )
= sk3 ) ),
inference(pattern_uni,[status(thm)],[23419:[bind(A,$thf( sk2 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 )),bind(B,$thf( sk3 ))]]) ).
thf(63,plain,
! [D: $i,C: $i,B: $o,A: $i] :
( ~ ( in @ C @ A )
| ~ ( in @ D @ A )
| ( in @ C
@ ( dsetconstr @ A
@ ^ [E: $i] :
( ( B
& ( E = C ) )
| ( ~ B
& ( E = D ) ) ) ) )
| ( B
!= ( in @ D @ A ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[22]) ).
thf(70,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ C )
| ~ ( in @ B @ C )
| ( in @ A
@ ( dsetconstr @ C
@ ^ [D: $i] :
( ( ( in @ B @ C )
& ( D = A ) )
| ( ~ ( in @ B @ C )
& ( D = B ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[63:[bind(A,$thf( F )),bind(B,$thf( in @ E @ F )),bind(C,$thf( C )),bind(D,$thf( E ))]]) ).
thf(83,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ C )
| ~ ( in @ B @ C )
| ( in @ A
@ ( dsetconstr @ C
@ ^ [D: $i] :
( ( ( in @ B @ C )
& ( D = A ) )
| ( ~ ( in @ B @ C )
& ( D = B ) ) ) ) ) ),
inference(simp,[status(thm)],[70]) ).
thf(1642,plain,
! [B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) )
!= sk5 )
| ( A != sk3 )
| ( B
!= ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) ) ),
inference(paramod_ordered,[status(thm)],[19,593]) ).
thf(1643,plain,
! [A: $i] :
( ~ ( in @ A @ ( setadjoin @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) @ emptyset ) )
| ( ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
!= sk5 )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[1642:[bind(A,$thf( A )),bind(B,$thf( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ))]]) ).
thf(1681,plain,
( ~ ( in @ sk3 @ ( setadjoin @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) @ emptyset ) )
| ( ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
!= sk5 ) ),
inference(simp,[status(thm)],[1643]) ).
thf(61529,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,56342]) ).
thf(61530,plain,
! [B: $i,A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) ) ) )
@ ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[61529]) ).
thf(61762,plain,
! [B: $i,A: $i] :
( ( A
!= ( dsetconstr @ B
@ ^ [C: $i] :
~ ( in @ C
@ ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk5 ) ) ) ) )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ) ),
inference(simp,[status(thm)],[61530]) ).
thf(61834,plain,
! [A: $i] :
( ( setadjoin
@ ( dsetconstr @ A
@ ^ [B: $i] :
~ ( in @ B
@ ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk5 ) ) ) )
@ emptyset )
!= ( setadjoin @ sk3 @ emptyset ) ),
inference(simp,[status(thm)],[61762]) ).
thf(6519,plain,
! [A: $i] :
( ~ $true
| ( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset )
@ ( setadjoin @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,1551]) ).
thf(6520,plain,
! [A: $i] :
( ( in @ A @ ( setadjoin @ A @ emptyset ) )
!= ( in
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset )
@ ( setadjoin @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) @ emptyset ) ) ),
inference(simp,[status(thm)],[6519]) ).
thf(6740,plain,
! [A: $i] :
( ( A
!= ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk5 ) )
@ emptyset ) )
| ( ( setadjoin @ A @ emptyset )
!= ( setadjoin @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) @ emptyset ) ) ),
inference(simp,[status(thm)],[6520]) ).
thf(6767,plain,
( ( setadjoin
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [A: $i] : ( A = sk5 ) )
@ emptyset )
@ emptyset )
!= ( setadjoin @ ( setadjoin @ ( setadjoin @ sk5 @ emptyset ) @ emptyset ) @ emptyset ) ),
inference(simp,[status(thm)],[6740]) ).
thf(32271,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( in @ A @ ( setadjoin @ B @ emptyset ) )
| ( B
!= ( dsetconstr @ sk3
@ ^ [D: $i] : ( D = sk6 ) ) )
| ( A
!= ( dsetconstr @ C
@ ^ [D: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[19,32157]) ).
thf(32272,plain,
! [B: $i,A: $i] :
( ~ ( in
@ ( dsetconstr @ B
@ ^ [C: $i] : $false )
@ ( setadjoin @ A @ emptyset ) )
| ( A
!= ( dsetconstr @ sk3
@ ^ [C: $i] : ( C = sk6 ) ) ) ),
inference(pattern_uni,[status(thm)],[32271:[bind(A,$thf( dsetconstr @ D @ ^ [E: $i] : $false )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(32299,plain,
! [A: $i] :
~ ( in
@ ( dsetconstr @ A
@ ^ [B: $i] : $false )
@ ( setadjoin
@ ( dsetconstr @ sk3
@ ^ [B: $i] : ( B = sk6 ) )
@ emptyset ) ),
inference(simp,[status(thm)],[32272]) ).
thf(23255,plain,
! [A: $i] :
( ( in @ ( sk1 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ sk3 )
| ( in @ sk6 @ sk6 )
| ~ $true
| ( in @ sk5 @ A )
| ( ( in @ ( sk2 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ ( setadjoin @ sk3 @ emptyset ) )
!= ( in @ A @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(paramod_ordered,[status(thm)],[10024,193]) ).
thf(23256,plain,
! [A: $i] :
( ( in @ ( sk1 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ sk3 )
| ( in @ sk6 @ sk6 )
| ( in @ sk5 @ A )
| ( ( in @ ( sk2 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ ( setadjoin @ sk3 @ emptyset ) )
!= ( in @ A @ ( setadjoin @ sk3 @ emptyset ) ) ) ),
inference(simp,[status(thm)],[23255]) ).
thf(23257,plain,
( ( in @ ( sk1 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) @ sk3 )
| ( in @ sk6 @ sk6 )
| ( in @ sk5 @ ( sk2 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ) ) ),
inference(pattern_uni,[status(thm)],[23256:[bind(A,$thf( sk2 @ ( setadjoin @ sk3 @ emptyset ) @ sk3 ))]]) ).
thf(107838,plain,
$false,
inference(e,[status(thm)],[35381,138,27664,32098,88,32398,11352,36654,54836,1401,32558,2114,269,597,53198,54955,698,340,54733,24,12960,56221,45634,17415,6423,41613,8880,504,55053,1379,1398,2024,54952,50807,57688,84,353,905,32293,106,32484,147,89,411,265,74,116,243,3591,85,55465,5206,3261,28,21,349,35030,92,1555,35807,32487,3408,1457,29480,697,3413,1672,10021,593,63446,9,32286,32349,54732,34080,193,1461,27409,13,5026,8690,35038,266,3587,3592,2915,33318,412,430,1680,32,10993,17,7910,149,601,44777,191,22,16302,56342,3404,54819,694,33969,12,144,7875,5190,1675,86,181,10024,1806,81,509,1801,29447,594,91,483,700,3583,108,10792,11173,50691,32099,26480,56350,780,267,431,80,35,50804,54965,3,27405,34079,355,1551,1798,59461,14017,32157,502,3412,55018,72,32402,3256,38929,87,903,35690,1807,4806,26,114,75,30505,478,23417,82,9542,60471,246,410,262,146,12972,1380,33871,183,19,136,56366,268,5741,32100,56218,596,501,1399,32530,90,55490,41939,23420,83,1681,61834,6767,32299,23257]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU703^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.04 % 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.06/0.11 % Computer : n012.cluster.edu
% 0.06/0.11 % Model : x86_64 x86_64
% 0.06/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.11 % Memory : 8046.5625MB
% 0.06/0.11 % OS : Linux 6.8.0-71-generic
% 0.06/0.11 % CPULimit : 300
% 0.06/0.11 % WCLimit : 300
% 0.06/0.11 % DateTime : Tue Sep 29 14:12:03 UTC 2026
% 0.06/0.12 % CPUTime :
% 0.06/0.12 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.39/0.39 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.55/0.48 % [INFO] Parsing done (94ms).
% 0.55/0.49 % [INFO] Running in sequential loop mode.
% 0.91/0.67 % [INFO] eprover registered as external prover.
% 0.91/0.67 % [INFO] Scanning for conjecture ...
% 1.08/0.74 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 1.08/0.76 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 1.08/0.76 % [INFO] Problem is higher-order (TPTP THF).
% 1.08/0.76 % [INFO] Type checking passed.
% 1.08/0.76 % [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 ...
% 152.42/41.39 % External prover 'e' found a proof!
% 152.42/41.39 % [INFO] Killing All external provers ...
% 152.42/41.39 % Time passed: 41200ms (effective reasoning time: 40898ms)
% 152.42/41.39 % 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)>
% 152.42/41.39 % Axioms used in derivation (0):
% 152.42/41.39 % No. of inferences in proof: 618
% 152.42/41.39 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 41200 ms resp. 40898 ms w/o parsing
% 149.09/41.62 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 149.09/41.63 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------