%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SET655+3 : TPTP v9.3.1. Released v2.2.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 : Sun Sep 27 08:30:39 AM UTC 2026
% Result : Theorem 254.88s 74.13s
% Output : Refutation 244.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 34
% Syntax : Number of formulae : 611 ( 84 unt; 0 typ; 14 def)
% Number of atoms : 2429 ( 429 equ; 0 cnn)
% Maximal formula atoms : 26 ( 3 avg)
% Number of connectives : 7281 (1120 ~;1067 |; 63 &;4873 @)
% ( 6 <=>; 152 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 7 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 29 ( 26 usr; 8 con; 0-2 aty)
% Number of variables : 1110 ( 14 ^;1067 !; 15 ?;1110 :)
% ( 0 !>; 0 ?*; 0 @-; 14 @+)
% Comments :
%------------------------------------------------------------------------------
thf(ilf_type_decl,type,
ilf_type: $i > $i > $o ).
thf(set_type_decl,type,
set_type: $i ).
thf(relation_type_decl,type,
relation_type: $i > $i > $i ).
thf(subset_decl,type,
subset: $i > $i > $o ).
thf(empty_decl,type,
empty: $i > $o ).
thf(member_decl,type,
member: $i > $i > $o ).
thf(power_set_decl,type,
power_set: $i > $i ).
thf(subset_type_decl,type,
subset_type: $i > $i ).
thf(cross_product_decl,type,
cross_product: $i > $i > $i ).
thf(relation_like_decl,type,
relation_like: $i > $o ).
thf(member_type_decl,type,
member_type: $i > $i ).
thf(ordered_pair_decl,type,
ordered_pair: $i > $i > $i ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk5_decl,type,
sk5: $i ).
thf(sk6_decl,type,
sk6: $i > $i > $i ).
thf(sk7_decl,type,
sk7: $i > $i ).
thf(sk8_decl,type,
sk8: $i > $i > $i ).
thf(sk9_decl,type,
sk9: $i > $i ).
thf(sk10_decl,type,
sk10: $i > $i > $i ).
thf(sk11_decl,type,
sk11: $i > $i > $i ).
thf(sk12_decl,type,
sk12: $i > $i ).
thf(sk13_decl,type,
sk13: $i > $i ).
thf(sk14_decl,type,
sk14: $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ! [D: $i] :
( ( set_type @ ( D @ ilf_type ) )
=> ! [E: $i] :
( ( C @ ( A @ relation_type ) @ ( E @ ilf_type ) )
=> ( ( ( D @ ( C @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( D @ ( B @ relation_type ) @ ( E @ ilf_type ) ) ) ) ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ! [D: $i] :
( ( B @ ( sk1 @ relation_type ) @ ( D @ ilf_type ) )
=> ( ( ( C @ ( B @ subset ) )
& ( A @ ( sk1 @ subset ) ) )
=> ( C @ ( A @ relation_type ) @ ( D @ ilf_type ) ) ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ! [C: $i] :
( ( A @ ( sk1 @ relation_type ) @ ( C @ ilf_type ) )
=> ( ( ( B @ ( A @ subset ) )
& ( sk2 @ ( sk1 @ subset ) ) )
=> ( B @ ( sk2 @ relation_type ) @ ( C @ ilf_type ) ) ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
~ ( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( sk3 @ ( sk1 @ relation_type ) @ ( B @ ilf_type ) )
=> ( ( ( A @ ( sk3 @ subset ) )
& ( sk2 @ ( sk1 @ subset ) ) )
=> ( A @ ( sk2 @ relation_type ) @ ( B @ ilf_type ) ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: $i] :
~ ( ( sk3 @ ( sk1 @ relation_type ) @ ( A @ ilf_type ) )
=> ( ( ( sk4 @ ( sk3 @ subset ) )
& ( sk2 @ ( sk1 @ subset ) ) )
=> ( sk4 @ ( sk2 @ relation_type ) @ ( A @ ilf_type ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: $i,B: $i] :
@+[C: $i] : ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( set_type @ ( B @ ilf_type ) )
=> ~ ( A @ ( B @ member ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( set_type @ ( C @ ilf_type ) )
=> ( ( B @ ( C @ member ) )
=> ( A @ ( C @ member ) ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( ^ [A: $i] :
@+[B: $i] : ( A @ member_type @ ( B @ ilf_type ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( ? [D: $i] :
( ( A
= ( D @ ( C @ ordered_pair ) ) )
& ( set_type @ ( D @ ilf_type ) ) )
& ( set_type @ ( C @ ilf_type ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( ( A
= ( C @ ( B @ ( A @ sk10 ) @ ordered_pair ) ) )
& ( set_type @ ( C @ ilf_type ) ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( set_type @ ( B @ ilf_type ) )
=> ( ( A @ ( B @ member ) )
=> ? [C: $i] :
( ? [D: $i] :
( ( B
= ( D @ ( C @ ordered_pair ) ) )
& ( set_type @ ( D @ ilf_type ) ) )
& ( set_type @ ( C @ ilf_type ) ) ) ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( ^ [A: $i] :
@+[B: $i] : ( A @ subset_type @ ( B @ ilf_type ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( set_type @ ( C @ ilf_type ) )
=> ( ( B @ ( C @ member ) )
=> ( A @ ( C @ member ) ) ) ) ) ) ).
thf(1,conjecture,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ! [D: $i] :
( ( set_type @ ( D @ ilf_type ) )
=> ! [E: $i] :
( ( C @ ( A @ relation_type ) @ ( E @ ilf_type ) )
=> ( ( ( D @ ( C @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( D @ ( B @ relation_type ) @ ( E @ ilf_type ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_relset_1_17) ).
thf(2,negated_conjecture,
~ ! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ! [D: $i] :
( ( set_type @ ( D @ ilf_type ) )
=> ! [E: $i] :
( ( C @ ( A @ relation_type ) @ ( E @ ilf_type ) )
=> ( ( ( D @ ( C @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( D @ ( B @ relation_type ) @ ( E @ ilf_type ) ) ) ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(22,plain,
~ ! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ! [D: $i] :
( ( set_type @ ( D @ ilf_type ) )
=> ! [E: $i] :
( ( C @ ( A @ relation_type ) @ ( E @ ilf_type ) )
=> ( ( ( D @ ( C @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( D @ ( B @ relation_type ) @ ( E @ ilf_type ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(23,plain,
( ~ ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) )
& ( sk4 @ ( sk3 @ subset ) )
& ( sk2 @ ( sk1 @ subset ) )
& ( sk3 @ ( sk1 @ relation_type ) @ ( sk5 @ ilf_type ) )
& ( set_type @ ( sk4 @ ilf_type ) )
& ( set_type @ ( sk3 @ ilf_type ) )
& ( set_type @ ( sk2 @ ilf_type ) )
& ( set_type @ ( sk1 @ ilf_type ) ) ),
inference(cnf,[status(esa)],[22]) ).
thf(28,plain,
sk3 @ ( sk1 @ relation_type ) @ ( sk5 @ ilf_type ),
inference(cnfConj,[status(thm)],[23]) ).
thf(11,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( ! [C: $i] :
( ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) )
=> ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) ) )
& ! [C: $i] :
( ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) )
=> ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3) ).
thf(57,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( ! [C: $i] :
( ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) )
=> ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) ) )
& ! [C: $i] :
( ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) )
=> ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(58,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ cross_product ) @ subset_type @ ( D @ ilf_type ) )
| ~ ( B @ ( A @ relation_type ) @ ( D @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) )
| ~ ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ) ),
inference(cnf,[status(esa)],[57]) ).
thf(60,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) )
| ~ ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[58]) ).
thf(61,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) )
| ~ ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(simp,[status(thm)],[60]) ).
thf(4,axiom,
! [A: $i] : ( set_type @ ( A @ ilf_type ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p19) ).
thf(34,plain,
! [A: $i] : ( set_type @ ( A @ ilf_type ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(35,plain,
! [A: $i] : ( set_type @ ( A @ ilf_type ) ),
inference(cnf,[status(esa)],[34]) ).
thf(1421,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) )
| ~ ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[61,35]) ).
thf(1422,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) )
| ~ ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) ) ),
inference(simp,[status(thm)],[1421]) ).
thf(1423,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ relation_type ) @ ( sk5 @ ilf_type ) )
!= ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) ) )
| ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[28,1422]) ).
thf(1424,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ relation_type ) @ ( sk5 @ ilf_type ) )
!= ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) ) )
| ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) ) ),
inference(simp,[status(thm)],[1423]) ).
thf(1425,plain,
sk3 @ ( sk1 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ),
inference(pattern_uni,[status(thm)],[1424:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 )),bind(C,$thf( sk5 ))]]) ).
thf(13,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( ( A @ subset_type @ ( B @ ilf_type ) )
<=> ( A @ power_set @ member_type @ ( B @ ilf_type ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p7) ).
thf(64,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( ( ( A @ power_set @ member_type @ ( B @ ilf_type ) )
=> ( A @ subset_type @ ( B @ ilf_type ) ) )
& ( ( A @ subset_type @ ( B @ ilf_type ) )
=> ( A @ power_set @ member_type @ ( B @ ilf_type ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(65,plain,
! [B: $i,A: $i] :
( ( ( A @ subset_type @ ( B @ ilf_type ) )
| ~ ( A @ power_set @ member_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( A @ power_set @ member_type @ ( B @ ilf_type ) )
| ~ ( A @ subset_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ) ),
inference(cnf,[status(esa)],[64]) ).
thf(66,plain,
! [B: $i,A: $i] :
( ( A @ power_set @ member_type @ ( B @ ilf_type ) )
| ~ ( A @ subset_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[65]) ).
thf(1506,plain,
! [B: $i,A: $i] :
( ( A @ power_set @ member_type @ ( B @ ilf_type ) )
| ~ ( A @ subset_type @ ( B @ ilf_type ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[66,35]) ).
thf(1507,plain,
! [B: $i,A: $i] :
( ( A @ power_set @ member_type @ ( B @ ilf_type ) )
| ~ ( A @ subset_type @ ( B @ ilf_type ) ) ),
inference(simp,[status(thm)],[1506]) ).
thf(1527,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) )
!= ( A @ subset_type @ ( B @ ilf_type ) ) )
| ( A @ power_set @ member_type @ ( B @ ilf_type ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1425,1507]) ).
thf(1528,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) )
!= ( A @ subset_type @ ( B @ ilf_type ) ) )
| ( A @ power_set @ member_type @ ( B @ ilf_type ) ) ),
inference(simp,[status(thm)],[1527]) ).
thf(1529,plain,
sk3 @ ( sk1 @ cross_product ) @ power_set @ member_type @ ( sk5 @ ilf_type ),
inference(pattern_uni,[status(thm)],[1528:[bind(A,$thf( sk3 @ ( sk1 @ cross_product ) )),bind(B,$thf( sk5 ))]]) ).
thf(14,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( ( set_type @ ( B @ ilf_type ) )
& ~ ( B @ empty ) )
=> ( ( B @ member_type @ ( A @ ilf_type ) )
<=> ( B @ ( A @ member ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p12) ).
thf(68,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( ( set_type @ ( B @ ilf_type ) )
& ~ ( B @ empty ) )
=> ( ( ( B @ ( A @ member ) )
=> ( B @ member_type @ ( A @ ilf_type ) ) )
& ( ( B @ member_type @ ( A @ ilf_type ) )
=> ( B @ ( A @ member ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(69,plain,
! [B: $i,A: $i] :
( ( ( B @ member_type @ ( A @ ilf_type ) )
| ~ ( B @ ( A @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ( B @ empty )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( B @ ( A @ member ) )
| ~ ( B @ member_type @ ( A @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ( B @ empty )
| ~ ( set_type @ ( A @ ilf_type ) ) ) ),
inference(cnf,[status(esa)],[68]) ).
thf(70,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ member ) )
| ~ ( B @ member_type @ ( A @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ( B @ empty )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[69]) ).
thf(1761,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ member ) )
| ~ ( B @ member_type @ ( A @ ilf_type ) )
| ~ $true
| ( B @ empty )
| ~ $true ),
inference(rewrite,[status(thm)],[70,35]) ).
thf(1762,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ member ) )
| ~ ( B @ member_type @ ( A @ ilf_type ) )
| ( B @ empty ) ),
inference(simp,[status(thm)],[1761]) ).
thf(1779,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ member_type @ ( sk5 @ ilf_type ) )
!= ( B @ member_type @ ( A @ ilf_type ) ) )
| ( B @ ( A @ member ) )
| ~ $true
| ( B @ empty ) ),
inference(paramod_ordered,[status(thm)],[1529,1762]) ).
thf(1780,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ member_type @ ( sk5 @ ilf_type ) )
!= ( B @ member_type @ ( A @ ilf_type ) ) )
| ( B @ ( A @ member ) )
| ( B @ empty ) ),
inference(simp,[status(thm)],[1779]) ).
thf(1781,plain,
( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
| ( sk3 @ ( sk1 @ cross_product ) @ power_set @ empty ) ),
inference(pattern_uni,[status(thm)],[1780:[bind(A,$thf( sk5 )),bind(B,$thf( sk3 @ ( sk1 @ cross_product ) @ power_set ))]]) ).
thf(7,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ( ( set_type @ ( A @ power_set @ ilf_type ) )
& ~ ( A @ power_set @ empty ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p11) ).
thf(43,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ( ( set_type @ ( A @ power_set @ ilf_type ) )
& ~ ( A @ power_set @ empty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(44,plain,
! [A: $i] :
( ( ( set_type @ ( A @ power_set @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ~ ( A @ power_set @ empty )
| ~ ( set_type @ ( A @ ilf_type ) ) ) ),
inference(cnf,[status(esa)],[43]) ).
thf(45,plain,
! [A: $i] :
( ~ ( A @ power_set @ empty )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(152,plain,
! [A: $i] :
( ~ ( A @ power_set @ empty )
| ~ $true ),
inference(rewrite,[status(thm)],[45,35]) ).
thf(153,plain,
! [A: $i] :
~ ( A @ power_set @ empty ),
inference(simp,[status(thm)],[152]) ).
thf(1955,plain,
( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
| $false ),
inference(rewrite,[status(thm)],[1781,153]) ).
thf(1956,plain,
sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ),
inference(simp,[status(thm)],[1955]) ).
thf(29,plain,
sk2 @ ( sk1 @ subset ),
inference(cnfConj,[status(thm)],[23]) ).
thf(21,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( ( B @ ( A @ subset ) )
<=> ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p5) ).
thf(93,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( ( ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) )
=> ( B @ ( A @ subset ) ) )
& ( ( B @ ( A @ subset ) )
=> ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(94,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ subset ) )
| ~ ( B @ ( A @ ( B @ sk14 ) @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( B @ ( A @ subset ) )
| ( A @ ( A @ ( B @ sk14 ) @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( B @ ( A @ subset ) )
| ( set_type @ ( A @ ( B @ sk14 ) @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( set_type @ ( C @ ilf_type ) )
| ~ ( B @ ( A @ subset ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ) ),
inference(cnf,[status(esa)],[93]) ).
thf(95,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( set_type @ ( C @ ilf_type ) )
| ~ ( B @ ( A @ subset ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(376,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ $true
| ~ ( B @ ( A @ subset ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[95,35]) ).
thf(377,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[376]) ).
thf(378,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[29,377]) ).
thf(379,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[378]) ).
thf(380,plain,
! [A: $i] :
( ( sk2 @ ( A @ member ) )
| ~ ( sk1 @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[379:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(418,plain,
! [A: $i] :
( ( sk2 @ ( A @ member ) )
| ~ ( sk1 @ ( A @ member ) ) ),
inference(simp,[status(thm)],[380]) ).
thf(2351,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk1 @ ( A @ member ) ) )
| ( sk2 @ ( A @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1956,418]) ).
thf(2352,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk1 @ ( A @ member ) ) )
| ( sk2 @ ( A @ member ) ) ),
inference(simp,[status(thm)],[2351]) ).
thf(2439,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk1 )
| ( sk5 != A )
| ( sk2 @ ( A @ member ) ) ),
inference(simp,[status(thm)],[2352]) ).
thf(2452,plain,
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk1 )
| ( sk2 @ ( sk5 @ member ) ) ),
inference(simp,[status(thm)],[2439]) ).
thf(6,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ( ( A @ empty )
<=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ~ ( A @ ( B @ member ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p14) ).
thf(38,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ( ( ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ~ ( A @ ( B @ member ) ) )
=> ( A @ empty ) )
& ( ( A @ empty )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ~ ( A @ ( B @ member ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(39,plain,
! [B: $i,A: $i] :
( ( ( A @ empty )
| ( A @ ( A @ sk7 @ member ) )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( A @ empty )
| ( set_type @ ( A @ sk7 @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ~ ( A @ ( B @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( A @ empty )
| ~ ( set_type @ ( A @ ilf_type ) ) ) ),
inference(cnf,[status(esa)],[38]) ).
thf(40,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( A @ empty )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(160,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ member ) )
| ~ $true
| ~ ( A @ empty )
| ~ $true ),
inference(rewrite,[status(thm)],[40,35]) ).
thf(161,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ member ) )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[160]) ).
thf(384,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ member ) )
!= ( D @ ( E @ member ) ) )
| ~ $true
| ~ ( D @ empty )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[377,161]) ).
thf(385,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ member ) )
!= ( D @ ( E @ member ) ) )
| ~ ( D @ empty )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[384]) ).
thf(386,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ empty )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(pattern_uni,[status(thm)],[385:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( B )),bind(E,$thf( C ))]]) ).
thf(420,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ~ ( B @ empty )
| ~ ( A @ ( C @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[29,386]) ).
thf(421,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ~ ( B @ empty )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[420]) ).
thf(422,plain,
! [A: $i] :
( ~ ( sk2 @ empty )
| ~ ( sk1 @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[421:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(453,plain,
! [A: $i] :
( ~ ( sk2 @ empty )
| ~ ( sk1 @ ( A @ member ) ) ),
inference(simp,[status(thm)],[422]) ).
thf(1957,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk1 @ ( A @ member ) ) )
| ~ ( sk2 @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1956,453]) ).
thf(1958,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk1 @ ( A @ member ) ) )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[1957]) ).
thf(1988,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk1 )
| ( sk5 != A )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[1958]) ).
thf(1995,plain,
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk1 )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[1988]) ).
thf(9,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( ( B @ power_set @ ( A @ member ) )
<=> ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p10) ).
thf(49,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( ( ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) )
=> ( B @ power_set @ ( A @ member ) ) )
& ( ( B @ power_set @ ( A @ member ) )
=> ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(50,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ power_set @ ( A @ member ) )
| ~ ( B @ ( A @ ( B @ sk8 ) @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( B @ power_set @ ( A @ member ) )
| ( A @ ( A @ ( B @ sk8 ) @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( B @ power_set @ ( A @ member ) )
| ( set_type @ ( A @ ( B @ sk8 ) @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( set_type @ ( C @ ilf_type ) )
| ~ ( B @ power_set @ ( A @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ) ),
inference(cnf,[status(esa)],[49]) ).
thf(53,plain,
! [B: $i,A: $i] :
( ( B @ power_set @ ( A @ member ) )
| ( A @ ( A @ ( B @ sk8 ) @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[50]) ).
thf(854,plain,
! [B: $i,A: $i] :
( ( B @ power_set @ ( A @ member ) )
| ( A @ ( A @ ( B @ sk8 ) @ member ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[53,35]) ).
thf(855,plain,
! [B: $i,A: $i] :
( ( B @ power_set @ ( A @ member ) )
| ( A @ ( A @ ( B @ sk8 ) @ member ) ) ),
inference(simp,[status(thm)],[854]) ).
thf(874,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk8 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ~ $true
| ~ ( C @ empty )
| ( B @ power_set @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[855,161]) ).
thf(875,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk8 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ~ ( C @ empty )
| ( B @ power_set @ ( A @ member ) ) ),
inference(simp,[status(thm)],[874]) ).
thf(876,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ( A @ power_set @ ( B @ member ) ) ),
inference(pattern_uni,[status(thm)],[875:[bind(A,$thf( F )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ sk8 ) ))]]) ).
thf(893,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ( A @ power_set @ ( B @ member ) ) ),
inference(simp,[status(thm)],[876]) ).
thf(10,axiom,
! [A: $i] :
( ( ( set_type @ ( A @ ilf_type ) )
& ~ ( A @ empty ) )
=> ? [B: $i] : ( A @ member_type @ ( B @ ilf_type ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p13) ).
thf(55,plain,
! [A: $i] :
( ( ( set_type @ ( A @ ilf_type ) )
& ~ ( A @ empty ) )
=> ? [B: $i] : ( A @ member_type @ ( B @ ilf_type ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(56,plain,
! [A: $i] :
( ( A @ member_type @ ( A @ sk9 @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) )
| ( A @ empty ) ),
inference(cnf,[status(esa)],[55]) ).
thf(608,plain,
! [A: $i] :
( ( A @ member_type @ ( A @ sk9 @ ilf_type ) )
| ~ $true
| ( A @ empty ) ),
inference(rewrite,[status(thm)],[56,35]) ).
thf(609,plain,
! [A: $i] :
( ( A @ member_type @ ( A @ sk9 @ ilf_type ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[608]) ).
thf(1811,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ member_type @ ( A @ sk9 @ ilf_type ) )
!= ( C @ member_type @ ( B @ ilf_type ) ) )
| ( C @ ( B @ member ) )
| ~ $true
| ( C @ empty )
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[609,1762]) ).
thf(1812,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ member_type @ ( A @ sk9 @ ilf_type ) )
!= ( C @ member_type @ ( B @ ilf_type ) ) )
| ( C @ ( B @ member ) )
| ( C @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[1811]) ).
thf(1813,plain,
! [A: $i] :
( ( A @ ( A @ sk9 @ member ) )
| ( A @ empty )
| ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[1812:[bind(A,$thf( D )),bind(B,$thf( D @ sk9 )),bind(C,$thf( D ))]]) ).
thf(1845,plain,
! [A: $i] :
( ( A @ ( A @ sk9 @ member ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[1813]) ).
thf(27,plain,
sk4 @ ( sk3 @ subset ),
inference(cnfConj,[status(thm)],[23]) ).
thf(390,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27,377]) ).
thf(391,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[390]) ).
thf(392,plain,
! [A: $i] :
( ( sk4 @ ( A @ member ) )
| ~ ( sk3 @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[391:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(415,plain,
! [A: $i] :
( ( sk4 @ ( A @ member ) )
| ~ ( sk3 @ ( A @ member ) ) ),
inference(simp,[status(thm)],[392]) ).
thf(3828,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk9 @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ( sk4 @ ( B @ member ) )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[1845,415]) ).
thf(3829,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk9 @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ( sk4 @ ( B @ member ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[3828]) ).
thf(3830,plain,
( ( sk4 @ ( sk3 @ sk9 @ member ) )
| ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[3829:[bind(A,$thf( sk3 )),bind(B,$thf( sk3 @ sk9 ))]]) ).
thf(12,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ( ( ( C @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( C @ ( A @ subset ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p1) ).
thf(62,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ( ( ( C @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( C @ ( A @ subset ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(63,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ subset ) )
| ~ ( C @ ( B @ subset ) )
| ~ ( B @ ( A @ subset ) )
| ~ ( set_type @ ( C @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnf,[status(esa)],[62]) ).
thf(202,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ subset ) )
| ~ ( C @ ( B @ subset ) )
| ~ ( B @ ( A @ subset ) )
| ~ $true
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[63,35]) ).
thf(203,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ subset ) )
| ~ ( C @ ( B @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[202]) ).
thf(213,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( C @ ( A @ subset ) )
| ~ $true
| ~ ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[27,203]) ).
thf(214,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( C @ ( A @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[213]) ).
thf(215,plain,
! [A: $i] :
( ( sk4 @ ( A @ subset ) )
| ~ ( sk3 @ ( A @ subset ) ) ),
inference(pattern_uni,[status(thm)],[214:[bind(A,$thf( A )),bind(B,$thf( sk3 )),bind(C,$thf( sk4 ))]]) ).
thf(447,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( A @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ~ ( C @ empty )
| ~ ( B @ ( D @ member ) )
| ~ $true
| ~ ( sk3 @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[215,386]) ).
thf(448,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( A @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ~ ( C @ empty )
| ~ ( B @ ( D @ member ) )
| ~ ( sk3 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[447]) ).
thf(449,plain,
! [B: $i,A: $i] :
( ~ ( sk4 @ empty )
| ~ ( A @ ( B @ member ) )
| ~ ( sk3 @ ( A @ subset ) ) ),
inference(pattern_uni,[status(thm)],[448:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk4 ))]]) ).
thf(450,plain,
! [B: $i,A: $i] :
( ~ ( sk4 @ empty )
| ~ ( A @ ( B @ member ) )
| ~ ( sk3 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[449]) ).
thf(1980,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ~ ( sk3 @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[1956,450]) ).
thf(1981,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ~ ( sk3 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[1980]) ).
thf(1982,plain,
( ~ ( sk4 @ empty )
| ~ ( sk3 @ ( sk3 @ ( sk1 @ cross_product ) @ power_set @ subset ) ) ),
inference(pattern_uni,[status(thm)],[1981:[bind(A,$thf( sk3 @ ( sk1 @ cross_product ) @ power_set )),bind(B,$thf( sk5 ))]]) ).
thf(18,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ( ( A @ relation_like )
<=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( ( A @ ( B @ member ) )
=> ? [C: $i] :
( ? [D: $i] :
( ( B
= ( D @ ( C @ ordered_pair ) ) )
& ( set_type @ ( D @ ilf_type ) ) )
& ( set_type @ ( C @ ilf_type ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p15) ).
thf(78,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ( ( ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( ( A @ ( B @ member ) )
=> ? [C: $i] :
( ? [D: $i] :
( ( B
= ( D @ ( C @ ordered_pair ) ) )
& ( set_type @ ( D @ ilf_type ) ) )
& ( set_type @ ( C @ ilf_type ) ) ) ) )
=> ( A @ relation_like ) )
& ( ( A @ relation_like )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( ( A @ ( B @ member ) )
=> ? [C: $i] :
( ? [D: $i] :
( ( B
= ( D @ ( C @ ordered_pair ) ) )
& ( set_type @ ( D @ ilf_type ) ) )
& ( set_type @ ( C @ ilf_type ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(79,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ relation_like )
| ( ( A @ sk12 )
!= ( D @ ( C @ ordered_pair ) ) )
| ~ ( set_type @ ( D @ ilf_type ) )
| ~ ( set_type @ ( C @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( A @ relation_like )
| ( A @ ( A @ sk12 @ member ) )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( A @ relation_like )
| ( set_type @ ( A @ sk12 @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( B
= ( A @ ( B @ sk11 ) @ ( A @ ( B @ sk10 ) @ ordered_pair ) ) )
| ~ ( A @ ( B @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( A @ relation_like )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( set_type @ ( A @ ( B @ sk11 ) @ ilf_type ) )
| ~ ( A @ ( B @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( A @ relation_like )
| ~ ( set_type @ ( A @ ilf_type ) ) )
& ( ( set_type @ ( A @ ( B @ sk10 ) @ ilf_type ) )
| ~ ( A @ ( B @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( A @ relation_like )
| ~ ( set_type @ ( A @ ilf_type ) ) ) ),
inference(cnf,[status(esa)],[78]) ).
thf(81,plain,
! [A: $i] :
( ( A @ relation_like )
| ( A @ ( A @ sk12 @ member ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[79]) ).
thf(460,plain,
! [A: $i] :
( ( A @ relation_like )
| ( A @ ( A @ sk12 @ member ) )
| ~ $true ),
inference(rewrite,[status(thm)],[81,35]) ).
thf(461,plain,
! [A: $i] :
( ( A @ relation_like )
| ( A @ ( A @ sk12 @ member ) ) ),
inference(simp,[status(thm)],[460]) ).
thf(207,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( C @ ( A @ subset ) )
| ~ $true
| ~ ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[29,203]) ).
thf(208,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( C @ ( A @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[207]) ).
thf(209,plain,
! [A: $i] :
( ( sk2 @ ( A @ subset ) )
| ~ ( sk1 @ ( A @ subset ) ) ),
inference(pattern_uni,[status(thm)],[208:[bind(A,$thf( A )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 ))]]) ).
thf(256,plain,
! [A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( sk1 @ ( A @ subset ) ) )
| ( sk2 @ ( A @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27,209]) ).
thf(257,plain,
! [A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( sk1 @ ( A @ subset ) ) )
| ( sk2 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[256]) ).
thf(280,plain,
! [A: $i] :
( ( sk4 != sk1 )
| ( sk3 != A )
| ( sk2 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[257]) ).
thf(286,plain,
( ( sk4 != sk1 )
| ( sk2 @ ( sk3 @ subset ) ) ),
inference(simp,[status(thm)],[280]) ).
thf(426,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk3 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ~ ( B @ empty )
| ~ ( A @ ( C @ member ) )
| ~ $true
| ( sk4 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[286,386]) ).
thf(427,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk3 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ~ ( B @ empty )
| ~ ( A @ ( C @ member ) )
| ( sk4 != sk1 ) ),
inference(simp,[status(thm)],[426]) ).
thf(428,plain,
! [A: $i] :
( ~ ( sk2 @ empty )
| ~ ( sk3 @ ( A @ member ) )
| ( sk4 != sk1 ) ),
inference(pattern_uni,[status(thm)],[427:[bind(A,$thf( sk3 )),bind(B,$thf( sk2 ))]]) ).
thf(457,plain,
! [A: $i] :
( ~ ( sk2 @ empty )
| ~ ( sk3 @ ( A @ member ) )
| ( sk4 != sk1 ) ),
inference(simp,[status(thm)],[428]) ).
thf(580,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk12 @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ~ ( sk2 @ empty )
| ~ $true
| ( sk4 != sk1 )
| ( A @ relation_like ) ),
inference(paramod_ordered,[status(thm)],[461,457]) ).
thf(581,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk12 @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ~ ( sk2 @ empty )
| ( sk4 != sk1 )
| ( A @ relation_like ) ),
inference(simp,[status(thm)],[580]) ).
thf(582,plain,
( ~ ( sk2 @ empty )
| ( sk4 != sk1 )
| ( sk3 @ relation_like ) ),
inference(pattern_uni,[status(thm)],[581:[bind(A,$thf( sk3 )),bind(B,$thf( sk3 @ sk12 ))]]) ).
thf(59,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) )
| ~ ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[58]) ).
thf(1282,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) )
| ~ ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[59,35]) ).
thf(1283,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) )
| ~ ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) ) ),
inference(simp,[status(thm)],[1282]) ).
thf(24,plain,
~ ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(1288,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) )
!= ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) ) )
| ~ $true
| ~ ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) ) ),
inference(paramod_ordered,[status(thm)],[1283,24]) ).
thf(1289,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ relation_type ) @ ( C @ ilf_type ) )
!= ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) ) )
| ~ ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) ) ),
inference(simp,[status(thm)],[1288]) ).
thf(1290,plain,
~ ( sk4 @ ( sk2 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) ),
inference(pattern_uni,[status(thm)],[1289:[bind(A,$thf( sk2 )),bind(B,$thf( sk4 )),bind(C,$thf( sk5 ))]]) ).
thf(54,plain,
! [B: $i,A: $i] :
( ( B @ power_set @ ( A @ member ) )
| ~ ( B @ ( A @ ( B @ sk8 ) @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[50]) ).
thf(1098,plain,
! [B: $i,A: $i] :
( ( B @ power_set @ ( A @ member ) )
| ~ ( B @ ( A @ ( B @ sk8 ) @ member ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[54,35]) ).
thf(1099,plain,
! [B: $i,A: $i] :
( ( B @ power_set @ ( A @ member ) )
| ~ ( B @ ( A @ ( B @ sk8 ) @ member ) ) ),
inference(simp,[status(thm)],[1098]) ).
thf(1100,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk8 ) @ member ) )
!= ( D @ ( C @ ( D @ sk8 ) @ member ) ) )
| ( D @ power_set @ ( C @ member ) )
| ~ $true
| ( B @ power_set @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[855,1099]) ).
thf(1101,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk8 ) @ member ) )
!= ( D @ ( C @ ( D @ sk8 ) @ member ) ) )
| ( D @ power_set @ ( C @ member ) )
| ( B @ power_set @ ( A @ member ) ) ),
inference(simp,[status(thm)],[1100]) ).
thf(1102,plain,
! [A: $i] :
( ( A @ power_set @ ( A @ member ) )
| ( A @ power_set @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[1101:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A )),bind(D,$thf( A ))]]) ).
thf(1139,plain,
! [A: $i] : ( A @ power_set @ ( A @ member ) ),
inference(simp,[status(thm)],[1102]) ).
thf(2131,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set @ ( A @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ( sk4 @ ( B @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1139,415]) ).
thf(2132,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set @ ( A @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ( sk4 @ ( B @ member ) ) ),
inference(simp,[status(thm)],[2131]) ).
thf(2213,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set )
!= sk3 )
| ( A != B )
| ( sk4 @ ( B @ member ) ) ),
inference(simp,[status(thm)],[2132]) ).
thf(2231,plain,
! [A: $i] :
( ( ( A @ power_set )
!= sk3 )
| ( sk4 @ ( A @ member ) ) ),
inference(simp,[status(thm)],[2213]) ).
thf(17,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ! [D: $i] :
( ( set_type @ ( D @ ilf_type ) )
=> ( ( ( D @ ( C @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( D @ ( B @ cross_product ) @ ( C @ ( A @ cross_product ) @ subset ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2) ).
thf(76,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ! [C: $i] :
( ( set_type @ ( C @ ilf_type ) )
=> ! [D: $i] :
( ( set_type @ ( D @ ilf_type ) )
=> ( ( ( D @ ( C @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( D @ ( B @ cross_product ) @ ( C @ ( A @ cross_product ) @ subset ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(77,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ cross_product ) @ ( C @ ( A @ cross_product ) @ subset ) )
| ~ ( D @ ( C @ subset ) )
| ~ ( B @ ( A @ subset ) )
| ~ ( set_type @ ( D @ ilf_type ) )
| ~ ( set_type @ ( C @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnf,[status(esa)],[76]) ).
thf(171,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ cross_product ) @ ( C @ ( A @ cross_product ) @ subset ) )
| ~ ( D @ ( C @ subset ) )
| ~ ( B @ ( A @ subset ) )
| ~ $true
| ~ $true
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[77,35]) ).
thf(172,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ cross_product ) @ ( C @ ( A @ cross_product ) @ subset ) )
| ~ ( D @ ( C @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[171]) ).
thf(182,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( D @ ( C @ subset ) ) )
| ( D @ ( B @ cross_product ) @ ( C @ ( A @ cross_product ) @ subset ) )
| ~ $true
| ~ ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[27,172]) ).
thf(183,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( D @ ( C @ subset ) ) )
| ( D @ ( B @ cross_product ) @ ( C @ ( A @ cross_product ) @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[182]) ).
thf(184,plain,
! [B: $i,A: $i] :
( ( sk4 @ ( B @ cross_product ) @ ( sk3 @ ( A @ cross_product ) @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(pattern_uni,[status(thm)],[183:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( sk3 )),bind(D,$thf( sk4 ))]]) ).
thf(5623,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk4 @ ( B @ cross_product ) @ ( sk3 @ ( A @ cross_product ) @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[29,184]) ).
thf(5624,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk4 @ ( B @ cross_product ) @ ( sk3 @ ( A @ cross_product ) @ subset ) ) ),
inference(simp,[status(thm)],[5623]) ).
thf(5625,plain,
sk4 @ ( sk2 @ cross_product ) @ ( sk3 @ ( sk1 @ cross_product ) @ subset ),
inference(pattern_uni,[status(thm)],[5624:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(98,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ~ ( B @ ( A @ ( B @ sk14 ) @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(4531,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ~ ( B @ ( A @ ( B @ sk14 ) @ member ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[98,35]) ).
thf(4532,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ~ ( B @ ( A @ ( B @ sk14 ) @ member ) ) ),
inference(simp,[status(thm)],[4531]) ).
thf(5,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ? [C: $i] : ( A @ ( B @ relation_type ) @ ( C @ ilf_type ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p4) ).
thf(36,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ? [C: $i] : ( A @ ( B @ relation_type ) @ ( C @ ilf_type ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(37,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ relation_type ) @ ( A @ ( B @ sk6 ) @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnf,[status(esa)],[36]) ).
thf(141,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ relation_type ) @ ( A @ ( B @ sk6 ) @ ilf_type ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[37,35]) ).
thf(142,plain,
! [B: $i,A: $i] : ( A @ ( B @ relation_type ) @ ( A @ ( B @ sk6 ) @ ilf_type ) ),
inference(simp,[status(thm)],[141]) ).
thf(856,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk8 ) @ member ) )
!= ( sk1 @ ( C @ member ) ) )
| ~ ( sk2 @ empty )
| ~ $true
| ( B @ power_set @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[855,453]) ).
thf(857,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk8 ) @ member ) )
!= ( sk1 @ ( C @ member ) ) )
| ~ ( sk2 @ empty )
| ( B @ power_set @ ( A @ member ) ) ),
inference(simp,[status(thm)],[856]) ).
thf(858,plain,
! [A: $i] :
( ~ ( sk2 @ empty )
| ( A @ power_set @ ( sk1 @ member ) ) ),
inference(pattern_uni,[status(thm)],[857:[bind(A,$thf( sk1 )),bind(B,$thf( D )),bind(C,$thf( sk1 @ ( D @ sk8 ) ))]]) ).
thf(898,plain,
! [A: $i] :
( ~ ( sk2 @ empty )
| ( A @ power_set @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[858]) ).
thf(5650,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk4 @ ( B @ cross_product ) @ ( sk3 @ ( A @ cross_product ) @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27,184]) ).
thf(5651,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk4 @ ( B @ cross_product ) @ ( sk3 @ ( A @ cross_product ) @ subset ) ) ),
inference(simp,[status(thm)],[5650]) ).
thf(5652,plain,
sk4 @ ( sk4 @ cross_product ) @ ( sk3 @ ( sk3 @ cross_product ) @ subset ),
inference(pattern_uni,[status(thm)],[5651:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(176,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( D @ ( C @ subset ) ) )
| ( D @ ( B @ cross_product ) @ ( C @ ( A @ cross_product ) @ subset ) )
| ~ $true
| ~ ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[29,172]) ).
thf(177,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( D @ ( C @ subset ) ) )
| ( D @ ( B @ cross_product ) @ ( C @ ( A @ cross_product ) @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[176]) ).
thf(178,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( B @ cross_product ) @ ( sk1 @ ( A @ cross_product ) @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(pattern_uni,[status(thm)],[177:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( sk1 )),bind(D,$thf( sk2 ))]]) ).
thf(5933,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk4 @ cross_product ) @ ( sk3 @ ( sk3 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk2 @ ( B @ cross_product ) @ ( sk1 @ ( A @ cross_product ) @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5652,178]) ).
thf(5934,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk4 @ cross_product ) @ ( sk3 @ ( sk3 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk2 @ ( B @ cross_product ) @ ( sk1 @ ( A @ cross_product ) @ subset ) ) ),
inference(simp,[status(thm)],[5933]) ).
thf(5935,plain,
sk2 @ ( sk4 @ ( sk4 @ cross_product ) @ cross_product ) @ ( sk1 @ ( sk3 @ ( sk3 @ cross_product ) @ cross_product ) @ subset ),
inference(pattern_uni,[status(thm)],[5934:[bind(A,$thf( sk3 @ ( sk3 @ cross_product ) )),bind(B,$thf( sk4 @ ( sk4 @ cross_product ) ))]]) ).
thf(97,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ( A @ ( A @ ( B @ sk14 ) @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(4065,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ( A @ ( A @ ( B @ sk14 ) @ member ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[97,35]) ).
thf(4066,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ( A @ ( A @ ( B @ sk14 ) @ member ) ) ),
inference(simp,[status(thm)],[4065]) ).
thf(4067,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk14 ) @ member ) )
!= ( sk1 @ ( C @ member ) ) )
| ~ ( sk2 @ empty )
| ~ $true
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[4066,453]) ).
thf(4068,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk14 ) @ member ) )
!= ( sk1 @ ( C @ member ) ) )
| ~ ( sk2 @ empty )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[4067]) ).
thf(4069,plain,
! [A: $i] :
( ~ ( sk2 @ empty )
| ( A @ ( sk1 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[4068:[bind(A,$thf( sk1 )),bind(B,$thf( D )),bind(C,$thf( sk1 @ ( D @ sk14 ) ))]]) ).
thf(4119,plain,
! [A: $i] :
( ~ ( sk2 @ empty )
| ( A @ ( sk1 @ subset ) ) ),
inference(simp,[status(thm)],[4069]) ).
thf(4196,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk1 @ subset ) )
!= ( sk3 @ ( B @ subset ) ) )
| ( sk4 @ ( B @ subset ) )
| ~ $true
| ~ ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[4119,215]) ).
thf(4197,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk1 @ subset ) )
!= ( sk3 @ ( B @ subset ) ) )
| ( sk4 @ ( B @ subset ) )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[4196]) ).
thf(4198,plain,
( ( sk4 @ ( sk1 @ subset ) )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[4197:[bind(A,$thf( sk3 )),bind(B,$thf( sk1 ))]]) ).
thf(1470,plain,
( ( ( sk3 @ ( sk1 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) )
!= ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1425,24]) ).
thf(1471,plain,
( ( sk3 @ ( sk1 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) )
!= ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) ) ),
inference(simp,[status(thm)],[1470]) ).
thf(1479,plain,
( ( ( sk3 @ ( sk1 @ cross_product ) @ subset_type )
!= ( sk4 @ ( sk2 @ relation_type ) ) )
| ( sk5 != sk5 ) ),
inference(simp,[status(thm)],[1471]) ).
thf(1482,plain,
( ( sk3 @ ( sk1 @ cross_product ) @ subset_type )
!= ( sk4 @ ( sk2 @ relation_type ) ) ),
inference(simp,[status(thm)],[1479]) ).
thf(429,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ~ ( B @ empty )
| ~ ( A @ ( C @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27,386]) ).
thf(430,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ~ ( B @ empty )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[429]) ).
thf(431,plain,
! [A: $i] :
( ~ ( sk4 @ empty )
| ~ ( sk3 @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[430:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(459,plain,
! [A: $i] :
( ~ ( sk4 @ empty )
| ~ ( sk3 @ ( A @ member ) ) ),
inference(simp,[status(thm)],[431]) ).
thf(883,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk8 ) @ member ) )
!= ( sk3 @ ( C @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ( B @ power_set @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[855,459]) ).
thf(884,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk8 ) @ member ) )
!= ( sk3 @ ( C @ member ) ) )
| ~ ( sk4 @ empty )
| ( B @ power_set @ ( A @ member ) ) ),
inference(simp,[status(thm)],[883]) ).
thf(885,plain,
! [A: $i] :
( ~ ( sk4 @ empty )
| ( A @ power_set @ ( sk3 @ member ) ) ),
inference(pattern_uni,[status(thm)],[884:[bind(A,$thf( sk3 )),bind(B,$thf( D )),bind(C,$thf( sk3 @ ( D @ sk8 ) ))]]) ).
thf(896,plain,
! [A: $i] :
( ~ ( sk4 @ empty )
| ( A @ power_set @ ( sk3 @ member ) ) ),
inference(simp,[status(thm)],[885]) ).
thf(999,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ power_set @ ( sk3 @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ~ ( sk3 @ ( B @ subset ) )
| ~ ( sk4 @ empty ) ),
inference(paramod_ordered,[status(thm)],[896,450]) ).
thf(1000,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ power_set @ ( sk3 @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ ( sk3 @ ( B @ subset ) )
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[999]) ).
thf(1001,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ power_set @ subset ) )
| ~ ( sk4 @ empty ) ),
inference(pattern_uni,[status(thm)],[1000:[bind(A,$thf( D )),bind(B,$thf( D @ power_set )),bind(C,$thf( sk3 ))]]) ).
thf(1013,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ power_set @ subset ) )
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[1001]) ).
thf(1035,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ subset ) )
!= ( sk3 @ ( B @ power_set @ subset ) ) )
| ~ $true
| ~ ( sk4 @ empty )
| ~ ( sk1 @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[209,1013]) ).
thf(1036,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ subset ) )
!= ( sk3 @ ( B @ power_set @ subset ) ) )
| ~ ( sk4 @ empty )
| ~ ( sk1 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[1035]) ).
thf(1050,plain,
! [B: $i,A: $i] :
( ( sk3 != sk2 )
| ( A
!= ( B @ power_set ) )
| ~ ( sk4 @ empty )
| ~ ( sk1 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[1036]) ).
thf(1055,plain,
! [A: $i] :
( ( sk3 != sk2 )
| ~ ( sk4 @ empty )
| ~ ( sk1 @ ( A @ power_set @ subset ) ) ),
inference(simp,[status(thm)],[1050]) ).
thf(3,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ( A @ ( A @ subset ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p9) ).
thf(32,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ( A @ ( A @ subset ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(33,plain,
! [A: $i] :
( ( A @ ( A @ subset ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnf,[status(esa)],[32]) ).
thf(135,plain,
! [A: $i] :
( ( A @ ( A @ subset ) )
| ~ $true ),
inference(rewrite,[status(thm)],[33,35]) ).
thf(136,plain,
! [A: $i] : ( A @ ( A @ subset ) ),
inference(simp,[status(thm)],[135]) ).
thf(194,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( E @ ( D @ subset ) ) )
| ( E @ ( C @ cross_product ) @ ( D @ ( B @ cross_product ) @ subset ) )
| ~ $true
| ~ ( C @ ( B @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[136,172]) ).
thf(195,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( E @ ( D @ subset ) ) )
| ( E @ ( C @ cross_product ) @ ( D @ ( B @ cross_product ) @ subset ) )
| ~ ( C @ ( B @ subset ) ) ),
inference(simp,[status(thm)],[194]) ).
thf(196,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ cross_product ) @ ( A @ ( B @ cross_product ) @ subset ) )
| ~ ( C @ ( B @ subset ) ) ),
inference(pattern_uni,[status(thm)],[195:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( A ))]]) ).
thf(85,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ ( B @ sk11 ) @ ( A @ ( B @ sk10 ) @ ordered_pair ) ) )
| ~ ( A @ ( B @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( A @ relation_like )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[79]) ).
thf(86,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( A @ relation_like )
| ~ ( set_type @ ( A @ ilf_type ) )
| ( ( A @ ( B @ sk11 ) @ ( A @ ( B @ sk10 ) @ ordered_pair ) )
= B ) ),
inference(lifteq,[status(thm)],[85]) ).
thf(3267,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ member ) )
| ~ $true
| ~ ( A @ relation_like )
| ~ $true
| ( ( A @ ( B @ sk11 ) @ ( A @ ( B @ sk10 ) @ ordered_pair ) )
= B ) ),
inference(rewrite,[status(thm)],[86,35]) ).
thf(3268,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ member ) )
| ~ ( A @ relation_like )
| ( ( A @ ( B @ sk11 ) @ ( A @ ( B @ sk10 ) @ ordered_pair ) )
= B ) ),
inference(simp,[status(thm)],[3267]) ).
thf(42,plain,
! [A: $i] :
( ( A @ empty )
| ( A @ ( A @ sk7 @ member ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(249,plain,
! [A: $i] :
( ( A @ empty )
| ( A @ ( A @ sk7 @ member ) )
| ~ $true ),
inference(rewrite,[status(thm)],[42,35]) ).
thf(250,plain,
! [A: $i] :
( ( A @ empty )
| ( A @ ( A @ sk7 @ member ) ) ),
inference(simp,[status(thm)],[249]) ).
thf(589,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ~ ( sk2 @ empty )
| ~ $true
| ( sk4 != sk1 )
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[250,457]) ).
thf(590,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ~ ( sk2 @ empty )
| ( sk4 != sk1 )
| ( A @ empty ) ),
inference(simp,[status(thm)],[589]) ).
thf(591,plain,
( ~ ( sk2 @ empty )
| ( sk4 != sk1 )
| ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[590:[bind(A,$thf( sk3 )),bind(B,$thf( sk3 @ sk7 ))]]) ).
thf(1315,plain,
( ( ( sk3 @ ( sk1 @ relation_type ) @ ( sk5 @ ilf_type ) )
!= ( sk4 @ ( sk2 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[28,1290]) ).
thf(1316,plain,
( ( sk3 @ ( sk1 @ relation_type ) @ ( sk5 @ ilf_type ) )
!= ( sk4 @ ( sk2 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) ) ),
inference(simp,[status(thm)],[1315]) ).
thf(1330,plain,
( ( ( sk3 @ ( sk1 @ relation_type ) )
!= ( sk4 @ ( sk2 @ cross_product ) @ subset_type ) )
| ( sk5 != sk5 ) ),
inference(simp,[status(thm)],[1316]) ).
thf(1334,plain,
( ( sk3 @ ( sk1 @ relation_type ) )
!= ( sk4 @ ( sk2 @ cross_product ) @ subset_type ) ),
inference(simp,[status(thm)],[1330]) ).
thf(71,plain,
! [B: $i,A: $i] :
( ( B @ member_type @ ( A @ ilf_type ) )
| ~ ( B @ ( A @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ( B @ empty )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[69]) ).
thf(2032,plain,
! [B: $i,A: $i] :
( ( B @ member_type @ ( A @ ilf_type ) )
| ~ ( B @ ( A @ member ) )
| ~ $true
| ( B @ empty )
| ~ $true ),
inference(rewrite,[status(thm)],[71,35]) ).
thf(2033,plain,
! [B: $i,A: $i] :
( ( B @ member_type @ ( A @ ilf_type ) )
| ~ ( B @ ( A @ member ) )
| ( B @ empty ) ),
inference(simp,[status(thm)],[2032]) ).
thf(3921,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ sk9 @ member ) )
!= ( B @ ( A @ member ) ) )
| ( B @ member_type @ ( A @ ilf_type ) )
| ~ $true
| ( B @ empty )
| ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[3830,2033]) ).
thf(3922,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ sk9 @ member ) )
!= ( B @ ( A @ member ) ) )
| ( B @ member_type @ ( A @ ilf_type ) )
| ( B @ empty )
| ( sk3 @ empty ) ),
inference(simp,[status(thm)],[3921]) ).
thf(3923,plain,
( ( sk4 @ member_type @ ( sk3 @ sk9 @ ilf_type ) )
| ( sk4 @ empty )
| ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[3922:[bind(A,$thf( sk3 @ sk9 )),bind(B,$thf( sk4 ))]]) ).
thf(19,axiom,
! [A: $i] :
( ( ( set_type @ ( A @ ilf_type ) )
& ( A @ empty ) )
=> ( A @ relation_like ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p16) ).
thf(89,plain,
! [A: $i] :
( ( ( set_type @ ( A @ ilf_type ) )
& ( A @ empty ) )
=> ( A @ relation_like ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(16,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( set_type @ ( B @ ( A @ cross_product ) @ ilf_type ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6) ).
thf(74,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( set_type @ ( B @ ( A @ cross_product ) @ ilf_type ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(51,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( set_type @ ( C @ ilf_type ) )
| ~ ( B @ power_set @ ( A @ member ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[50]) ).
thf(514,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ $true
| ~ ( B @ power_set @ ( A @ member ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[51,35]) ).
thf(515,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ power_set @ ( A @ member ) ) ),
inference(simp,[status(thm)],[514]) ).
thf(1966,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( B @ power_set @ ( A @ member ) ) )
| ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1956,515]) ).
thf(1967,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( B @ power_set @ ( A @ member ) ) )
| ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[1966]) ).
thf(1968,plain,
! [A: $i] :
( ( sk3 @ ( sk1 @ cross_product ) @ ( A @ member ) )
| ~ ( sk5 @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[1967:[bind(A,$thf( sk5 )),bind(B,$thf( sk3 @ ( sk1 @ cross_product ) )),bind(C,$thf( C ))]]) ).
thf(1990,plain,
! [A: $i] :
( ( sk3 @ ( sk1 @ cross_product ) @ ( A @ member ) )
| ~ ( sk5 @ ( A @ member ) ) ),
inference(simp,[status(thm)],[1968]) ).
thf(2758,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ ( A @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ empty )
| ~ ( sk5 @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[1990,161]) ).
thf(2759,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ ( A @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ ( B @ empty )
| ~ ( sk5 @ ( A @ member ) ) ),
inference(simp,[status(thm)],[2758]) ).
thf(2760,plain,
! [A: $i] :
( ~ ( sk3 @ ( sk1 @ cross_product ) @ empty )
| ~ ( sk5 @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[2759:[bind(A,$thf( A )),bind(B,$thf( sk3 @ ( sk1 @ cross_product ) )),bind(C,$thf( A ))]]) ).
thf(2969,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk8 ) @ member ) )
!= ( sk5 @ ( C @ member ) ) )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty )
| ~ $true
| ( B @ power_set @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[855,2760]) ).
thf(2970,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk8 ) @ member ) )
!= ( sk5 @ ( C @ member ) ) )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty )
| ( B @ power_set @ ( A @ member ) ) ),
inference(simp,[status(thm)],[2969]) ).
thf(2971,plain,
! [A: $i] :
( ~ ( sk3 @ ( sk1 @ cross_product ) @ empty )
| ( A @ power_set @ ( sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[2970:[bind(A,$thf( sk5 )),bind(B,$thf( D )),bind(C,$thf( sk5 @ ( D @ sk8 ) ))]]) ).
thf(3011,plain,
! [A: $i] :
( ~ ( sk3 @ ( sk1 @ cross_product ) @ empty )
| ( A @ power_set @ ( sk5 @ member ) ) ),
inference(simp,[status(thm)],[2971]) ).
thf(204,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( C @ ( A @ subset ) )
| ~ ( C @ ( B @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[29,203]) ).
thf(205,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( C @ ( A @ subset ) )
| ~ ( C @ ( B @ subset ) ) ),
inference(simp,[status(thm)],[204]) ).
thf(206,plain,
! [A: $i] :
( ( A @ ( sk1 @ subset ) )
| ~ ( A @ ( sk2 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[205:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(248,plain,
! [A: $i] :
( ( A @ ( sk1 @ subset ) )
| ~ ( A @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[206]) ).
thf(5837,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk2 @ cross_product ) @ ( sk3 @ ( sk1 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk2 @ ( B @ cross_product ) @ ( sk1 @ ( A @ cross_product ) @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5625,178]) ).
thf(5838,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk2 @ cross_product ) @ ( sk3 @ ( sk1 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk2 @ ( B @ cross_product ) @ ( sk1 @ ( A @ cross_product ) @ subset ) ) ),
inference(simp,[status(thm)],[5837]) ).
thf(5839,plain,
sk2 @ ( sk4 @ ( sk2 @ cross_product ) @ cross_product ) @ ( sk1 @ ( sk3 @ ( sk1 @ cross_product ) @ cross_product ) @ subset ),
inference(pattern_uni,[status(thm)],[5838:[bind(A,$thf( sk3 @ ( sk1 @ cross_product ) )),bind(B,$thf( sk4 @ ( sk2 @ cross_product ) ))]]) ).
thf(2355,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk12 @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ( sk2 @ ( B @ member ) )
| ~ $true
| ( A @ relation_like ) ),
inference(paramod_ordered,[status(thm)],[461,418]) ).
thf(2356,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk12 @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ( sk2 @ ( B @ member ) )
| ( A @ relation_like ) ),
inference(simp,[status(thm)],[2355]) ).
thf(2357,plain,
( ( sk2 @ ( sk1 @ sk12 @ member ) )
| ( sk1 @ relation_like ) ),
inference(pattern_uni,[status(thm)],[2356:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ sk12 ))]]) ).
thf(2494,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ sk12 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ~ ( sk3 @ ( A @ subset ) )
| ( sk1 @ relation_like ) ),
inference(paramod_ordered,[status(thm)],[2357,450]) ).
thf(2495,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ sk12 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ~ ( sk3 @ ( A @ subset ) )
| ( sk1 @ relation_like ) ),
inference(simp,[status(thm)],[2494]) ).
thf(2496,plain,
( ~ ( sk4 @ empty )
| ~ ( sk3 @ ( sk2 @ subset ) )
| ( sk1 @ relation_like ) ),
inference(pattern_uni,[status(thm)],[2495:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 @ sk12 ))]]) ).
thf(510,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ~ ( sk2 @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[250,453]) ).
thf(511,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ~ ( sk2 @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[510]) ).
thf(512,plain,
( ~ ( sk2 @ empty )
| ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[511:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ sk7 ))]]) ).
thf(5781,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk2 @ cross_product ) @ ( sk3 @ ( sk1 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk4 @ ( B @ cross_product ) @ ( sk3 @ ( A @ cross_product ) @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5625,184]) ).
thf(5782,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk2 @ cross_product ) @ ( sk3 @ ( sk1 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk4 @ ( B @ cross_product ) @ ( sk3 @ ( A @ cross_product ) @ subset ) ) ),
inference(simp,[status(thm)],[5781]) ).
thf(5783,plain,
sk4 @ ( sk4 @ ( sk2 @ cross_product ) @ cross_product ) @ ( sk3 @ ( sk3 @ ( sk1 @ cross_product ) @ cross_product ) @ subset ),
inference(pattern_uni,[status(thm)],[5782:[bind(A,$thf( sk3 @ ( sk1 @ cross_product ) )),bind(B,$thf( sk4 @ ( sk2 @ cross_product ) ))]]) ).
thf(3825,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk9 @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ( sk2 @ ( B @ member ) )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[1845,418]) ).
thf(3826,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk9 @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ( sk2 @ ( B @ member ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[3825]) ).
thf(3827,plain,
( ( sk2 @ ( sk1 @ sk9 @ member ) )
| ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[3826:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ sk9 ))]]) ).
thf(67,plain,
! [B: $i,A: $i] :
( ( A @ subset_type @ ( B @ ilf_type ) )
| ~ ( A @ power_set @ member_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[65]) ).
thf(1618,plain,
! [B: $i,A: $i] :
( ( A @ subset_type @ ( B @ ilf_type ) )
| ~ ( A @ power_set @ member_type @ ( B @ ilf_type ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[67,35]) ).
thf(1619,plain,
! [B: $i,A: $i] :
( ( A @ subset_type @ ( B @ ilf_type ) )
| ~ ( A @ power_set @ member_type @ ( B @ ilf_type ) ) ),
inference(simp,[status(thm)],[1618]) ).
thf(2931,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk5 @ ( A @ member ) ) )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1956,2760]) ).
thf(2932,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk5 @ ( A @ member ) ) )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty ) ),
inference(simp,[status(thm)],[2931]) ).
thf(3000,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk5 )
| ( sk5 != A )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty ) ),
inference(simp,[status(thm)],[2932]) ).
thf(3022,plain,
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk5 )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty ) ),
inference(simp,[status(thm)],[3000]) ).
thf(1431,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ relation_type ) @ ( A @ ( B @ sk6 ) @ ilf_type ) )
!= ( D @ ( C @ relation_type ) @ ( E @ ilf_type ) ) )
| ( D @ ( C @ cross_product ) @ subset_type @ ( E @ ilf_type ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[142,1422]) ).
thf(1432,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ relation_type ) @ ( A @ ( B @ sk6 ) @ ilf_type ) )
!= ( D @ ( C @ relation_type ) @ ( E @ ilf_type ) ) )
| ( D @ ( C @ cross_product ) @ subset_type @ ( E @ ilf_type ) ) ),
inference(simp,[status(thm)],[1431]) ).
thf(1433,plain,
! [B: $i,A: $i] : ( B @ ( A @ cross_product ) @ subset_type @ ( B @ ( A @ sk6 ) @ ilf_type ) ),
inference(pattern_uni,[status(thm)],[1432:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( F )),bind(D,$thf( G )),bind(E,$thf( G @ ( F @ sk6 ) ))]]) ).
thf(1463,plain,
! [B: $i,A: $i] : ( B @ ( A @ cross_product ) @ subset_type @ ( B @ ( A @ sk6 ) @ ilf_type ) ),
inference(simp,[status(thm)],[1433]) ).
thf(8,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ! [C: $i] :
( ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) )
=> ( C @ relation_like ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p17) ).
thf(47,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ! [C: $i] :
( ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) )
=> ( C @ relation_like ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(48,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ relation_like )
| ~ ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnf,[status(esa)],[47]) ).
thf(308,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ relation_like )
| ~ ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) )
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[48,35]) ).
thf(309,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ relation_like )
| ~ ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) ) ),
inference(simp,[status(thm)],[308]) ).
thf(1495,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ cross_product ) @ subset_type @ ( B @ ( A @ sk6 ) @ ilf_type ) )
!= ( D @ ( C @ cross_product ) @ subset_type @ ( E @ ilf_type ) ) )
| ( E @ relation_like )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1463,309]) ).
thf(1496,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ cross_product ) @ subset_type @ ( B @ ( A @ sk6 ) @ ilf_type ) )
!= ( D @ ( C @ cross_product ) @ subset_type @ ( E @ ilf_type ) ) )
| ( E @ relation_like ) ),
inference(simp,[status(thm)],[1495]) ).
thf(1497,plain,
! [B: $i,A: $i] : ( B @ ( A @ sk6 ) @ relation_like ),
inference(pattern_uni,[status(thm)],[1496:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( F )),bind(D,$thf( G )),bind(E,$thf( G @ ( F @ sk6 ) ))]]) ).
thf(1502,plain,
! [B: $i,A: $i] : ( B @ ( A @ sk6 ) @ relation_like ),
inference(simp,[status(thm)],[1497]) ).
thf(191,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( E @ ( C @ cross_product ) @ ( D @ ( B @ cross_product ) @ subset ) )
| ~ ( E @ ( D @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[136,172]) ).
thf(192,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( E @ ( C @ cross_product ) @ ( D @ ( B @ cross_product ) @ subset ) )
| ~ ( E @ ( D @ subset ) ) ),
inference(simp,[status(thm)],[191]) ).
thf(193,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ cross_product ) @ ( B @ ( A @ cross_product ) @ subset ) )
| ~ ( C @ ( B @ subset ) ) ),
inference(pattern_uni,[status(thm)],[192:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(197,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ cross_product ) @ ( B @ ( A @ cross_product ) @ subset ) )
| ~ ( C @ ( B @ subset ) ) ),
inference(simp,[status(thm)],[193]) ).
thf(20,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ? [B: $i] : ( A @ subset_type @ ( B @ ilf_type ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p8) ).
thf(91,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ? [B: $i] : ( A @ subset_type @ ( B @ ilf_type ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(92,plain,
! [A: $i] :
( ( A @ subset_type @ ( A @ sk13 @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnf,[status(esa)],[91]) ).
thf(162,plain,
! [A: $i] :
( ( A @ subset_type @ ( A @ sk13 @ ilf_type ) )
| ~ $true ),
inference(rewrite,[status(thm)],[92,35]) ).
thf(163,plain,
! [A: $i] : ( A @ subset_type @ ( A @ sk13 @ ilf_type ) ),
inference(simp,[status(thm)],[162]) ).
thf(314,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ subset_type @ ( A @ sk13 @ ilf_type ) )
!= ( C @ ( B @ cross_product ) @ subset_type @ ( D @ ilf_type ) ) )
| ( D @ relation_like )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[163,309]) ).
thf(315,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ subset_type @ ( A @ sk13 @ ilf_type ) )
!= ( C @ ( B @ cross_product ) @ subset_type @ ( D @ ilf_type ) ) )
| ( D @ relation_like ) ),
inference(simp,[status(thm)],[314]) ).
thf(316,plain,
! [B: $i,A: $i] : ( B @ ( A @ cross_product ) @ sk13 @ relation_like ),
inference(pattern_uni,[status(thm)],[315:[bind(A,$thf( G @ ( F @ cross_product ) )),bind(B,$thf( F )),bind(C,$thf( G )),bind(D,$thf( G @ ( F @ cross_product ) @ sk13 ))]]) ).
thf(324,plain,
! [B: $i,A: $i] : ( B @ ( A @ cross_product ) @ sk13 @ relation_like ),
inference(simp,[status(thm)],[316]) ).
thf(819,plain,
! [A: $i] :
( ( ( A @ power_set @ empty )
!= ( sk3 @ empty ) )
| ~ $true
| ~ ( sk2 @ empty )
| ( sk4 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[591,153]) ).
thf(820,plain,
! [A: $i] :
( ( ( A @ power_set @ empty )
!= ( sk3 @ empty ) )
| ~ ( sk2 @ empty )
| ( sk4 != sk1 ) ),
inference(simp,[status(thm)],[819]) ).
thf(847,plain,
! [A: $i] :
( ( ( A @ power_set )
!= sk3 )
| ~ ( sk2 @ empty )
| ( sk4 != sk1 ) ),
inference(simp,[status(thm)],[820]) ).
thf(5877,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk4 @ cross_product ) @ ( sk3 @ ( sk3 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk4 @ ( B @ cross_product ) @ ( sk3 @ ( A @ cross_product ) @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5652,184]) ).
thf(5878,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk4 @ cross_product ) @ ( sk3 @ ( sk3 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk4 @ ( B @ cross_product ) @ ( sk3 @ ( A @ cross_product ) @ subset ) ) ),
inference(simp,[status(thm)],[5877]) ).
thf(5879,plain,
sk4 @ ( sk4 @ ( sk4 @ cross_product ) @ cross_product ) @ ( sk3 @ ( sk3 @ ( sk3 @ cross_product ) @ cross_product ) @ subset ),
inference(pattern_uni,[status(thm)],[5878:[bind(A,$thf( sk3 @ ( sk3 @ cross_product ) )),bind(B,$thf( sk4 @ ( sk4 @ cross_product ) ))]]) ).
thf(1577,plain,
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ member_type @ ( sk5 @ ilf_type ) )
!= ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1529,24]) ).
thf(1578,plain,
( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ member_type @ ( sk5 @ ilf_type ) )
!= ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) ) ),
inference(simp,[status(thm)],[1577]) ).
thf(1587,plain,
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ member_type )
!= ( sk4 @ ( sk2 @ relation_type ) ) )
| ( sk5 != sk5 ) ),
inference(simp,[status(thm)],[1578]) ).
thf(1592,plain,
( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ member_type )
!= ( sk4 @ ( sk2 @ relation_type ) ) ),
inference(simp,[status(thm)],[1587]) ).
thf(327,plain,
! [A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( sk3 @ ( A @ subset ) ) )
| ( sk4 @ ( A @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[29,215]) ).
thf(328,plain,
! [A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( sk3 @ ( A @ subset ) ) )
| ( sk4 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[327]) ).
thf(363,plain,
! [A: $i] :
( ( sk3 != sk2 )
| ( sk1 != A )
| ( sk4 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[328]) ).
thf(371,plain,
( ( sk3 != sk2 )
| ( sk4 @ ( sk1 @ subset ) ) ),
inference(simp,[status(thm)],[363]) ).
thf(474,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( sk1 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ~ ( B @ empty )
| ~ ( A @ ( C @ member ) )
| ~ $true
| ( sk3 != sk2 ) ),
inference(paramod_ordered,[status(thm)],[371,386]) ).
thf(475,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( sk1 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ~ ( B @ empty )
| ~ ( A @ ( C @ member ) )
| ( sk3 != sk2 ) ),
inference(simp,[status(thm)],[474]) ).
thf(476,plain,
! [A: $i] :
( ~ ( sk4 @ empty )
| ~ ( sk1 @ ( A @ member ) )
| ( sk3 != sk2 ) ),
inference(pattern_uni,[status(thm)],[475:[bind(A,$thf( sk1 )),bind(B,$thf( sk4 ))]]) ).
thf(502,plain,
! [A: $i] :
( ~ ( sk4 @ empty )
| ~ ( sk1 @ ( A @ member ) )
| ( sk3 != sk2 ) ),
inference(simp,[status(thm)],[476]) ).
thf(980,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set @ ( sk3 @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ( sk3 != sk2 )
| ~ ( sk4 @ empty ) ),
inference(paramod_ordered,[status(thm)],[896,502]) ).
thf(981,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set @ ( sk3 @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ( sk3 != sk2 )
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[980]) ).
thf(1006,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set )
!= sk1 )
| ( sk3 != B )
| ( sk3 != sk2 )
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[981]) ).
thf(1017,plain,
! [A: $i] :
( ( ( A @ power_set )
!= sk1 )
| ( sk3 != sk2 )
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[1006]) ).
thf(1717,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( A @ subset ) )
!= ( B @ ( sk2 @ subset ) ) )
| ( B @ ( sk1 @ subset ) )
| ~ $true
| ~ ( sk3 @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[215,248]) ).
thf(1718,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( A @ subset ) )
!= ( B @ ( sk2 @ subset ) ) )
| ( B @ ( sk1 @ subset ) )
| ~ ( sk3 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[1717]) ).
thf(1719,plain,
( ( sk4 @ ( sk1 @ subset ) )
| ~ ( sk3 @ ( sk2 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[1718:[bind(A,$thf( sk2 )),bind(B,$thf( sk4 ))]]) ).
thf(1636,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ member_type @ ( A @ sk9 @ ilf_type ) )
!= ( B @ power_set @ member_type @ ( C @ ilf_type ) ) )
| ( B @ subset_type @ ( C @ ilf_type ) )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[609,1619]) ).
thf(1637,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ member_type @ ( A @ sk9 @ ilf_type ) )
!= ( B @ power_set @ member_type @ ( C @ ilf_type ) ) )
| ( B @ subset_type @ ( C @ ilf_type ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[1636]) ).
thf(1638,plain,
! [A: $i] :
( ( A @ subset_type @ ( A @ power_set @ sk9 @ ilf_type ) )
| ( A @ power_set @ empty ) ),
inference(pattern_uni,[status(thm)],[1637:[bind(A,$thf( E @ power_set )),bind(B,$thf( E )),bind(C,$thf( E @ power_set @ sk9 ))]]) ).
thf(1659,plain,
! [A: $i] :
( ( A @ subset_type @ ( A @ power_set @ sk9 @ ilf_type ) )
| ( A @ power_set @ empty ) ),
inference(simp,[status(thm)],[1638]) ).
thf(1731,plain,
! [A: $i] :
( ( A @ subset_type @ ( A @ power_set @ sk9 @ ilf_type ) )
| $false ),
inference(rewrite,[status(thm)],[1659,153]) ).
thf(1732,plain,
! [A: $i] : ( A @ subset_type @ ( A @ power_set @ sk9 @ ilf_type ) ),
inference(simp,[status(thm)],[1731]) ).
thf(1747,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ subset_type @ ( A @ power_set @ sk9 @ ilf_type ) )
!= ( C @ ( B @ cross_product ) @ subset_type @ ( D @ ilf_type ) ) )
| ( D @ relation_like )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1732,309]) ).
thf(1748,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ subset_type @ ( A @ power_set @ sk9 @ ilf_type ) )
!= ( C @ ( B @ cross_product ) @ subset_type @ ( D @ ilf_type ) ) )
| ( D @ relation_like ) ),
inference(simp,[status(thm)],[1747]) ).
thf(1749,plain,
! [B: $i,A: $i] : ( B @ ( A @ cross_product ) @ power_set @ sk9 @ relation_like ),
inference(pattern_uni,[status(thm)],[1748:[bind(A,$thf( H @ ( G @ cross_product ) )),bind(B,$thf( G )),bind(C,$thf( H )),bind(D,$thf( H @ ( G @ cross_product ) @ power_set @ sk9 ))]]) ).
thf(1755,plain,
! [B: $i,A: $i] : ( B @ ( A @ cross_product ) @ power_set @ sk9 @ relation_like ),
inference(simp,[status(thm)],[1749]) ).
thf(5122,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk2 @ ( B @ cross_product ) @ ( sk1 @ ( A @ cross_product ) @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27,178]) ).
thf(5123,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk2 @ ( B @ cross_product ) @ ( sk1 @ ( A @ cross_product ) @ subset ) ) ),
inference(simp,[status(thm)],[5122]) ).
thf(5124,plain,
sk2 @ ( sk4 @ cross_product ) @ ( sk1 @ ( sk3 @ cross_product ) @ subset ),
inference(pattern_uni,[status(thm)],[5123:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(5385,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk4 @ cross_product ) @ ( sk1 @ ( sk3 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk2 @ ( B @ cross_product ) @ ( sk1 @ ( A @ cross_product ) @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5124,178]) ).
thf(5386,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk4 @ cross_product ) @ ( sk1 @ ( sk3 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk2 @ ( B @ cross_product ) @ ( sk1 @ ( A @ cross_product ) @ subset ) ) ),
inference(simp,[status(thm)],[5385]) ).
thf(5387,plain,
sk2 @ ( sk2 @ ( sk4 @ cross_product ) @ cross_product ) @ ( sk1 @ ( sk1 @ ( sk3 @ cross_product ) @ cross_product ) @ subset ),
inference(pattern_uni,[status(thm)],[5386:[bind(A,$thf( sk1 @ ( sk3 @ cross_product ) )),bind(B,$thf( sk2 @ ( sk4 @ cross_product ) ))]]) ).
thf(4102,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk14 ) @ member ) )
!= ( sk5 @ ( C @ member ) ) )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty )
| ~ $true
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[4066,2760]) ).
thf(4103,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk14 ) @ member ) )
!= ( sk5 @ ( C @ member ) ) )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[4102]) ).
thf(4104,plain,
! [A: $i] :
( ~ ( sk3 @ ( sk1 @ cross_product ) @ empty )
| ( A @ ( sk5 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[4103:[bind(A,$thf( sk5 )),bind(B,$thf( D )),bind(C,$thf( sk5 @ ( D @ sk14 ) ))]]) ).
thf(4122,plain,
! [A: $i] :
( ~ ( sk3 @ ( sk1 @ cross_product ) @ empty )
| ( A @ ( sk5 @ subset ) ) ),
inference(simp,[status(thm)],[4104]) ).
thf(4734,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk5 @ subset ) )
!= ( sk3 @ ( B @ subset ) ) )
| ( sk4 @ ( B @ subset ) )
| ~ $true
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty ) ),
inference(paramod_ordered,[status(thm)],[4122,215]) ).
thf(4735,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk5 @ subset ) )
!= ( sk3 @ ( B @ subset ) ) )
| ( sk4 @ ( B @ subset ) )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty ) ),
inference(simp,[status(thm)],[4734]) ).
thf(4736,plain,
( ( sk4 @ ( sk5 @ subset ) )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty ) ),
inference(pattern_uni,[status(thm)],[4735:[bind(A,$thf( sk3 )),bind(B,$thf( sk5 ))]]) ).
thf(402,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ member ) )
!= ( B @ ( D @ member ) ) )
| ( C @ ( D @ member ) )
| ~ $true
| ~ ( C @ ( B @ subset ) )
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[250,377]) ).
thf(403,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ member ) )
!= ( B @ ( D @ member ) ) )
| ( C @ ( D @ member ) )
| ~ ( C @ ( B @ subset ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[402]) ).
thf(404,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk7 @ member ) )
| ~ ( A @ ( B @ subset ) )
| ( B @ empty ) ),
inference(pattern_uni,[status(thm)],[403:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( C )),bind(D,$thf( E @ sk7 ))]]) ).
thf(412,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk7 @ member ) )
| ~ ( A @ ( B @ subset ) )
| ( B @ empty ) ),
inference(simp,[status(thm)],[404]) ).
thf(736,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( A @ ( B @ subset ) ) )
| ( A @ ( B @ sk7 @ member ) )
| ~ $true
| ( B @ empty ) ),
inference(paramod_ordered,[status(thm)],[29,412]) ).
thf(737,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( A @ ( B @ subset ) ) )
| ( A @ ( B @ sk7 @ member ) )
| ( B @ empty ) ),
inference(simp,[status(thm)],[736]) ).
thf(738,plain,
( ( sk2 @ ( sk1 @ sk7 @ member ) )
| ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[737:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 ))]]) ).
thf(2721,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk5 @ ( A @ member ) ) )
| ( sk3 @ ( sk1 @ cross_product ) @ ( A @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1956,1990]) ).
thf(2722,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk5 @ ( A @ member ) ) )
| ( sk3 @ ( sk1 @ cross_product ) @ ( A @ member ) ) ),
inference(simp,[status(thm)],[2721]) ).
thf(2827,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk5 )
| ( sk5 != A )
| ( sk3 @ ( sk1 @ cross_product ) @ ( A @ member ) ) ),
inference(simp,[status(thm)],[2722]) ).
thf(2845,plain,
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk5 )
| ( sk3 @ ( sk1 @ cross_product ) @ ( sk5 @ member ) ) ),
inference(simp,[status(thm)],[2827]) ).
thf(2480,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ sk12 @ member ) )
!= ( B @ ( A @ member ) ) )
| ( B @ member_type @ ( A @ ilf_type ) )
| ~ $true
| ( B @ empty )
| ( sk1 @ relation_like ) ),
inference(paramod_ordered,[status(thm)],[2357,2033]) ).
thf(2481,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ sk12 @ member ) )
!= ( B @ ( A @ member ) ) )
| ( B @ member_type @ ( A @ ilf_type ) )
| ( B @ empty )
| ( sk1 @ relation_like ) ),
inference(simp,[status(thm)],[2480]) ).
thf(2482,plain,
( ( sk2 @ member_type @ ( sk1 @ sk12 @ ilf_type ) )
| ( sk2 @ empty )
| ( sk1 @ relation_like ) ),
inference(pattern_uni,[status(thm)],[2481:[bind(A,$thf( sk1 @ sk12 )),bind(B,$thf( sk2 ))]]) ).
thf(603,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ( sk3 != sk2 )
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[250,502]) ).
thf(604,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ( sk3 != sk2 )
| ( A @ empty ) ),
inference(simp,[status(thm)],[603]) ).
thf(605,plain,
( ~ ( sk4 @ empty )
| ( sk3 != sk2 )
| ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[604:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ sk7 ))]]) ).
thf(2107,plain,
! [A: $i] :
( ( ( sk2 @ ( A @ subset ) )
!= ( sk3 @ ( sk3 @ ( sk1 @ cross_product ) @ power_set @ subset ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ~ ( sk1 @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[209,1982]) ).
thf(2108,plain,
! [A: $i] :
( ( ( sk2 @ ( A @ subset ) )
!= ( sk3 @ ( sk3 @ ( sk1 @ cross_product ) @ power_set @ subset ) ) )
| ~ ( sk4 @ empty )
| ~ ( sk1 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[2107]) ).
thf(2117,plain,
! [A: $i] :
( ( sk3 != sk2 )
| ( A
!= ( sk3 @ ( sk1 @ cross_product ) @ power_set ) )
| ~ ( sk4 @ empty )
| ~ ( sk1 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[2108]) ).
thf(2125,plain,
( ( sk3 != sk2 )
| ~ ( sk4 @ empty )
| ~ ( sk1 @ ( sk3 @ ( sk1 @ cross_product ) @ power_set @ subset ) ) ),
inference(simp,[status(thm)],[2117]) ).
thf(1323,plain,
! [A: $i] :
( ( ( set_type @ ( A @ ilf_type ) )
!= ( sk4 @ ( sk2 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,1290]) ).
thf(1324,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
!= ( sk4 @ ( sk2 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) ) ),
inference(simp,[status(thm)],[1323]) ).
thf(1328,plain,
! [A: $i] :
( ( ( sk4 @ ( sk2 @ cross_product ) @ subset_type )
!= set_type )
| ( A != sk5 ) ),
inference(simp,[status(thm)],[1324]) ).
thf(1333,plain,
( ( sk4 @ ( sk2 @ cross_product ) @ subset_type )
!= set_type ),
inference(simp,[status(thm)],[1328]) ).
thf(2786,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ member ) )
!= ( sk5 @ ( B @ member ) ) )
| ( sk3 @ ( sk1 @ cross_product ) @ ( B @ member ) )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[250,1990]) ).
thf(2787,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ member ) )
!= ( sk5 @ ( B @ member ) ) )
| ( sk3 @ ( sk1 @ cross_product ) @ ( B @ member ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[2786]) ).
thf(2788,plain,
( ( sk3 @ ( sk1 @ cross_product ) @ ( sk5 @ sk7 @ member ) )
| ( sk5 @ empty ) ),
inference(pattern_uni,[status(thm)],[2787:[bind(A,$thf( sk5 )),bind(B,$thf( sk5 @ sk7 ))]]) ).
thf(2881,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ ( sk5 @ sk7 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ empty )
| ( sk5 @ empty ) ),
inference(paramod_ordered,[status(thm)],[2788,161]) ).
thf(2882,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ ( sk5 @ sk7 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ empty )
| ( sk5 @ empty ) ),
inference(simp,[status(thm)],[2881]) ).
thf(2883,plain,
( ~ ( sk3 @ ( sk1 @ cross_product ) @ empty )
| ( sk5 @ empty ) ),
inference(pattern_uni,[status(thm)],[2882:[bind(A,$thf( sk3 @ ( sk1 @ cross_product ) )),bind(B,$thf( sk5 @ sk7 ))]]) ).
thf(763,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk3 @ subset ) )
!= ( A @ ( B @ subset ) ) )
| ( A @ ( B @ sk7 @ member ) )
| ~ $true
| ( B @ empty )
| ( sk4 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[286,412]) ).
thf(764,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk3 @ subset ) )
!= ( A @ ( B @ subset ) ) )
| ( A @ ( B @ sk7 @ member ) )
| ( B @ empty )
| ( sk4 != sk1 ) ),
inference(simp,[status(thm)],[763]) ).
thf(765,plain,
( ( sk2 @ ( sk3 @ sk7 @ member ) )
| ( sk3 @ empty )
| ( sk4 != sk1 ) ),
inference(pattern_uni,[status(thm)],[764:[bind(A,$thf( sk2 )),bind(B,$thf( sk3 ))]]) ).
thf(1983,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk3 @ ( A @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1956,459]) ).
thf(1984,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk3 @ ( A @ member ) ) )
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[1983]) ).
thf(1989,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk3 )
| ( sk5 != A )
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[1984]) ).
thf(1996,plain,
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk3 )
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[1989]) ).
thf(1959,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk1 @ ( A @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ( sk3 != sk2 ) ),
inference(paramod_ordered,[status(thm)],[1956,502]) ).
thf(1960,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk1 @ ( A @ member ) ) )
| ~ ( sk4 @ empty )
| ( sk3 != sk2 ) ),
inference(simp,[status(thm)],[1959]) ).
thf(1985,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk1 )
| ( sk5 != A )
| ~ ( sk4 @ empty )
| ( sk3 != sk2 ) ),
inference(simp,[status(thm)],[1960]) ).
thf(1991,plain,
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk1 )
| ~ ( sk4 @ empty )
| ( sk3 != sk2 ) ),
inference(simp,[status(thm)],[1985]) ).
thf(2142,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk12 @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ( sk4 @ ( B @ member ) )
| ~ $true
| ( A @ relation_like ) ),
inference(paramod_ordered,[status(thm)],[461,415]) ).
thf(2143,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk12 @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ( sk4 @ ( B @ member ) )
| ( A @ relation_like ) ),
inference(simp,[status(thm)],[2142]) ).
thf(2144,plain,
( ( sk4 @ ( sk3 @ sk12 @ member ) )
| ( sk3 @ relation_like ) ),
inference(pattern_uni,[status(thm)],[2143:[bind(A,$thf( sk3 )),bind(B,$thf( sk3 @ sk12 ))]]) ).
thf(5101,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk2 @ ( B @ cross_product ) @ ( sk1 @ ( A @ cross_product ) @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[29,178]) ).
thf(5102,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk2 @ ( B @ cross_product ) @ ( sk1 @ ( A @ cross_product ) @ subset ) ) ),
inference(simp,[status(thm)],[5101]) ).
thf(5103,plain,
sk2 @ ( sk2 @ cross_product ) @ ( sk1 @ ( sk1 @ cross_product ) @ subset ),
inference(pattern_uni,[status(thm)],[5102:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(5664,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ cross_product ) @ ( sk1 @ ( sk1 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk4 @ ( B @ cross_product ) @ ( sk3 @ ( A @ cross_product ) @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5103,184]) ).
thf(5665,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ cross_product ) @ ( sk1 @ ( sk1 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk4 @ ( B @ cross_product ) @ ( sk3 @ ( A @ cross_product ) @ subset ) ) ),
inference(simp,[status(thm)],[5664]) ).
thf(5666,plain,
sk4 @ ( sk2 @ ( sk2 @ cross_product ) @ cross_product ) @ ( sk3 @ ( sk1 @ ( sk1 @ cross_product ) @ cross_product ) @ subset ),
inference(pattern_uni,[status(thm)],[5665:[bind(A,$thf( sk1 @ ( sk1 @ cross_product ) )),bind(B,$thf( sk2 @ ( sk2 @ cross_product ) ))]]) ).
thf(1742,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ subset_type @ ( A @ power_set @ sk9 @ ilf_type ) )
!= ( C @ ( B @ cross_product ) @ subset_type @ ( D @ ilf_type ) ) )
| ( C @ ( B @ relation_type ) @ ( D @ ilf_type ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1732,1283]) ).
thf(1743,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ subset_type @ ( A @ power_set @ sk9 @ ilf_type ) )
!= ( C @ ( B @ cross_product ) @ subset_type @ ( D @ ilf_type ) ) )
| ( C @ ( B @ relation_type ) @ ( D @ ilf_type ) ) ),
inference(simp,[status(thm)],[1742]) ).
thf(1744,plain,
! [B: $i,A: $i] : ( B @ ( A @ relation_type ) @ ( B @ ( A @ cross_product ) @ power_set @ sk9 @ ilf_type ) ),
inference(pattern_uni,[status(thm)],[1743:[bind(A,$thf( H @ ( G @ cross_product ) )),bind(B,$thf( G )),bind(C,$thf( H )),bind(D,$thf( H @ ( G @ cross_product ) @ power_set @ sk9 ))]]) ).
thf(1754,plain,
! [B: $i,A: $i] : ( B @ ( A @ relation_type ) @ ( B @ ( A @ cross_product ) @ power_set @ sk9 @ ilf_type ) ),
inference(simp,[status(thm)],[1744]) ).
thf(164,plain,
! [A: $i] :
( ( ( A @ subset_type @ ( A @ sk13 @ ilf_type ) )
!= ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[163,24]) ).
thf(165,plain,
! [A: $i] :
( ( A @ subset_type @ ( A @ sk13 @ ilf_type ) )
!= ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) ) ),
inference(simp,[status(thm)],[164]) ).
thf(166,plain,
! [A: $i] :
( ( ( A @ subset_type )
!= ( sk4 @ ( sk2 @ relation_type ) ) )
| ( ( A @ sk13 )
!= sk5 ) ),
inference(simp,[status(thm)],[165]) ).
thf(1466,plain,
( ( ( sk4 @ ( sk2 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) )
!= ( sk3 @ ( sk1 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1425,1290]) ).
thf(1467,plain,
( ( sk4 @ ( sk2 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) )
!= ( sk3 @ ( sk1 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) ) ),
inference(simp,[status(thm)],[1466]) ).
thf(1480,plain,
( ( ( sk4 @ ( sk2 @ cross_product ) @ subset_type )
!= ( sk3 @ ( sk1 @ cross_product ) @ subset_type ) )
| ( sk5 != sk5 ) ),
inference(simp,[status(thm)],[1467]) ).
thf(1483,plain,
( ( sk4 @ ( sk2 @ cross_product ) @ subset_type )
!= ( sk3 @ ( sk1 @ cross_product ) @ subset_type ) ),
inference(simp,[status(thm)],[1480]) ).
thf(575,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[250,459]) ).
thf(576,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk7 @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[575]) ).
thf(577,plain,
( ~ ( sk4 @ empty )
| ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[576:[bind(A,$thf( sk3 )),bind(B,$thf( sk3 @ sk7 ))]]) ).
thf(1961,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( A @ ( C @ member ) ) )
| ~ ( B @ empty )
| ~ $true
| ~ ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[1956,386]) ).
thf(1962,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( A @ ( C @ member ) ) )
| ~ ( B @ empty )
| ~ ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[1961]) ).
thf(1963,plain,
! [A: $i] :
( ~ ( A @ empty )
| ~ ( A @ ( sk3 @ ( sk1 @ cross_product ) @ power_set @ subset ) ) ),
inference(pattern_uni,[status(thm)],[1962:[bind(A,$thf( sk3 @ ( sk1 @ cross_product ) @ power_set )),bind(B,$thf( B )),bind(C,$thf( sk5 ))]]) ).
thf(1997,plain,
! [A: $i] :
( ~ ( A @ empty )
| ~ ( A @ ( sk3 @ ( sk1 @ cross_product ) @ power_set @ subset ) ) ),
inference(simp,[status(thm)],[1963]) ).
thf(210,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( C @ ( A @ subset ) )
| ~ ( C @ ( B @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27,203]) ).
thf(211,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( C @ ( A @ subset ) )
| ~ ( C @ ( B @ subset ) ) ),
inference(simp,[status(thm)],[210]) ).
thf(212,plain,
! [A: $i] :
( ( A @ ( sk3 @ subset ) )
| ~ ( A @ ( sk4 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[211:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(245,plain,
! [A: $i] :
( ( A @ ( sk3 @ subset ) )
| ~ ( A @ ( sk4 @ subset ) ) ),
inference(simp,[status(thm)],[212]) ).
thf(1144,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ power_set @ ( A @ member ) )
!= ( B @ ( D @ member ) ) )
| ~ ( C @ empty )
| ~ $true
| ~ ( C @ ( B @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[1139,386]) ).
thf(1145,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ power_set @ ( A @ member ) )
!= ( B @ ( D @ member ) ) )
| ~ ( C @ empty )
| ~ ( C @ ( B @ subset ) ) ),
inference(simp,[status(thm)],[1144]) ).
thf(1146,plain,
! [B: $i,A: $i] :
( ~ ( A @ empty )
| ~ ( A @ ( B @ power_set @ subset ) ) ),
inference(pattern_uni,[status(thm)],[1145:[bind(A,$thf( E )),bind(B,$thf( E @ power_set )),bind(C,$thf( C )),bind(D,$thf( E ))]]) ).
thf(1180,plain,
! [B: $i,A: $i] :
( ~ ( A @ empty )
| ~ ( A @ ( B @ power_set @ subset ) ) ),
inference(simp,[status(thm)],[1146]) ).
thf(3687,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ subset ) )
!= ( B @ ( C @ power_set @ subset ) ) )
| ~ ( B @ empty )
| ~ $true
| ~ ( sk1 @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[209,1180]) ).
thf(3688,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ subset ) )
!= ( B @ ( C @ power_set @ subset ) ) )
| ~ ( B @ empty )
| ~ ( sk1 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[3687]) ).
thf(3689,plain,
! [A: $i] :
( ~ ( sk2 @ empty )
| ~ ( sk1 @ ( A @ power_set @ subset ) ) ),
inference(pattern_uni,[status(thm)],[3688:[bind(A,$thf( D @ power_set )),bind(B,$thf( sk2 )),bind(C,$thf( D ))]]) ).
thf(3710,plain,
! [A: $i] :
( ~ ( sk2 @ empty )
| ~ ( sk1 @ ( A @ power_set @ subset ) ) ),
inference(simp,[status(thm)],[3689]) ).
thf(1571,plain,
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ member_type @ ( sk5 @ ilf_type ) )
!= ( sk4 @ ( sk2 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1529,1290]) ).
thf(1572,plain,
( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ member_type @ ( sk5 @ ilf_type ) )
!= ( sk4 @ ( sk2 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) ) ),
inference(simp,[status(thm)],[1571]) ).
thf(1584,plain,
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ member_type )
!= ( sk4 @ ( sk2 @ cross_product ) @ subset_type ) )
| ( sk5 != sk5 ) ),
inference(simp,[status(thm)],[1572]) ).
thf(1589,plain,
( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ member_type )
!= ( sk4 @ ( sk2 @ cross_product ) @ subset_type ) ),
inference(simp,[status(thm)],[1584]) ).
thf(629,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ subset ) )
!= ( B @ ( sk4 @ subset ) ) )
| ( B @ ( sk3 @ subset ) )
| ~ $true
| ~ ( sk1 @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[209,245]) ).
thf(630,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ subset ) )
!= ( B @ ( sk4 @ subset ) ) )
| ( B @ ( sk3 @ subset ) )
| ~ ( sk1 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[629]) ).
thf(631,plain,
( ( sk2 @ ( sk3 @ subset ) )
| ~ ( sk1 @ ( sk4 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[630:[bind(A,$thf( sk4 )),bind(B,$thf( sk2 ))]]) ).
thf(1541,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ cross_product ) @ subset_type @ ( B @ ( A @ sk6 ) @ ilf_type ) )
!= ( C @ subset_type @ ( D @ ilf_type ) ) )
| ( C @ power_set @ member_type @ ( D @ ilf_type ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1463,1507]) ).
thf(1542,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ cross_product ) @ subset_type @ ( B @ ( A @ sk6 ) @ ilf_type ) )
!= ( C @ subset_type @ ( D @ ilf_type ) ) )
| ( C @ power_set @ member_type @ ( D @ ilf_type ) ) ),
inference(simp,[status(thm)],[1541]) ).
thf(1543,plain,
! [B: $i,A: $i] : ( B @ ( A @ cross_product ) @ power_set @ member_type @ ( B @ ( A @ sk6 ) @ ilf_type ) ),
inference(pattern_uni,[status(thm)],[1542:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( H @ ( G @ cross_product ) )),bind(D,$thf( H @ ( G @ sk6 ) ))]]) ).
thf(1557,plain,
! [B: $i,A: $i] : ( B @ ( A @ cross_product ) @ power_set @ member_type @ ( B @ ( A @ sk6 ) @ ilf_type ) ),
inference(simp,[status(thm)],[1543]) ).
thf(137,plain,
! [A: $i] :
( ( ( set_type @ ( A @ ilf_type ) )
!= ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,24]) ).
thf(138,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
!= ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) ) ),
inference(simp,[status(thm)],[137]) ).
thf(139,plain,
! [A: $i] :
( ( ( sk4 @ ( sk2 @ relation_type ) )
!= set_type )
| ( A != sk5 ) ),
inference(simp,[status(thm)],[138]) ).
thf(140,plain,
( ( sk4 @ ( sk2 @ relation_type ) )
!= set_type ),
inference(simp,[status(thm)],[139]) ).
thf(143,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ relation_type ) @ ( A @ ( B @ sk6 ) @ ilf_type ) )
!= ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[142,24]) ).
thf(144,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ relation_type ) @ ( A @ ( B @ sk6 ) @ ilf_type ) )
!= ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) ) ),
inference(simp,[status(thm)],[143]) ).
thf(145,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ relation_type ) )
!= ( sk4 @ ( sk2 @ relation_type ) ) )
| ( ( A @ ( B @ sk6 ) )
!= sk5 ) ),
inference(simp,[status(thm)],[144]) ).
thf(154,plain,
! [B: $i,A: $i] :
( ( A != sk4 )
| ( B != sk2 )
| ( ( A @ ( B @ sk6 ) )
!= sk5 ) ),
inference(simp,[status(thm)],[145]) ).
thf(155,plain,
( ( sk4 @ ( sk2 @ sk6 ) )
!= sk5 ),
inference(simp,[status(thm)],[154]) ).
thf(1140,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set @ ( A @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ~ ( sk2 @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1139,453]) ).
thf(1141,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set @ ( A @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[1140]) ).
thf(1171,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set )
!= sk1 )
| ( A != B )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[1141]) ).
thf(1177,plain,
! [A: $i] :
( ( ( A @ power_set )
!= sk1 )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[1171]) ).
thf(917,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ sk7 @ member ) )
!= ( A @ ( C @ member ) ) )
| ( B @ ( C @ member ) )
| ~ $true
| ~ ( B @ ( A @ subset ) )
| ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[738,377]) ).
thf(918,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ sk7 @ member ) )
!= ( A @ ( C @ member ) ) )
| ( B @ ( C @ member ) )
| ~ ( B @ ( A @ subset ) )
| ( sk1 @ empty ) ),
inference(simp,[status(thm)],[917]) ).
thf(919,plain,
! [A: $i] :
( ( A @ ( sk1 @ sk7 @ member ) )
| ~ ( A @ ( sk2 @ subset ) )
| ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[918:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( sk1 @ sk7 ))]]) ).
thf(932,plain,
! [A: $i] :
( ( A @ ( sk1 @ sk7 @ member ) )
| ~ ( A @ ( sk2 @ subset ) )
| ( sk1 @ empty ) ),
inference(simp,[status(thm)],[919]) ).
thf(1536,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ subset_type @ ( A @ sk13 @ ilf_type ) )
!= ( B @ subset_type @ ( C @ ilf_type ) ) )
| ( B @ power_set @ member_type @ ( C @ ilf_type ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[163,1507]) ).
thf(1537,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ subset_type @ ( A @ sk13 @ ilf_type ) )
!= ( B @ subset_type @ ( C @ ilf_type ) ) )
| ( B @ power_set @ member_type @ ( C @ ilf_type ) ) ),
inference(simp,[status(thm)],[1536]) ).
thf(1538,plain,
! [A: $i] : ( A @ power_set @ member_type @ ( A @ sk13 @ ilf_type ) ),
inference(pattern_uni,[status(thm)],[1537:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ sk13 ))]]) ).
thf(1556,plain,
! [A: $i] : ( A @ power_set @ member_type @ ( A @ sk13 @ ilf_type ) ),
inference(simp,[status(thm)],[1538]) ).
thf(5178,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( sk2 @ ( C @ cross_product ) @ ( sk1 @ ( B @ cross_product ) @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[136,178]) ).
thf(5179,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( sk2 @ ( C @ cross_product ) @ ( sk1 @ ( B @ cross_product ) @ subset ) ) ),
inference(simp,[status(thm)],[5178]) ).
thf(5180,plain,
! [A: $i] : ( sk2 @ ( A @ cross_product ) @ ( sk1 @ ( A @ cross_product ) @ subset ) ),
inference(pattern_uni,[status(thm)],[5179:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(766,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( A @ ( B @ subset ) ) )
| ( A @ ( B @ sk7 @ member ) )
| ~ $true
| ( B @ empty ) ),
inference(paramod_ordered,[status(thm)],[27,412]) ).
thf(767,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ subset ) )
!= ( A @ ( B @ subset ) ) )
| ( A @ ( B @ sk7 @ member ) )
| ( B @ empty ) ),
inference(simp,[status(thm)],[766]) ).
thf(768,plain,
( ( sk4 @ ( sk3 @ sk7 @ member ) )
| ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[767:[bind(A,$thf( sk4 )),bind(B,$thf( sk3 ))]]) ).
thf(1002,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set @ ( sk3 @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ~ ( sk4 @ empty ) ),
inference(paramod_ordered,[status(thm)],[896,459]) ).
thf(1003,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set @ ( sk3 @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[1002]) ).
thf(1005,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set )
!= sk3 )
| ( sk3 != B )
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[1003]) ).
thf(1015,plain,
! [A: $i] :
( ( ( A @ power_set )
!= sk3 )
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[1005]) ).
thf(1475,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) )
!= ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) ) )
| ( C @ relation_like )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1425,309]) ).
thf(1476,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ subset_type @ ( sk5 @ ilf_type ) )
!= ( B @ ( A @ cross_product ) @ subset_type @ ( C @ ilf_type ) ) )
| ( C @ relation_like ) ),
inference(simp,[status(thm)],[1475]) ).
thf(1477,plain,
sk5 @ relation_like,
inference(pattern_uni,[status(thm)],[1476:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 )),bind(C,$thf( sk5 ))]]) ).
thf(920,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ sk7 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ~ ( sk3 @ ( A @ subset ) )
| ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[738,450]) ).
thf(921,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ sk7 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ~ ( sk3 @ ( A @ subset ) )
| ( sk1 @ empty ) ),
inference(simp,[status(thm)],[920]) ).
thf(922,plain,
( ~ ( sk4 @ empty )
| ~ ( sk3 @ ( sk2 @ subset ) )
| ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[921:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 @ sk7 ))]]) ).
thf(2067,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ sk7 @ member ) )
!= ( B @ ( A @ member ) ) )
| ( B @ member_type @ ( A @ ilf_type ) )
| ~ $true
| ( B @ empty )
| ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[768,2033]) ).
thf(2068,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ sk7 @ member ) )
!= ( B @ ( A @ member ) ) )
| ( B @ member_type @ ( A @ ilf_type ) )
| ( B @ empty )
| ( sk3 @ empty ) ),
inference(simp,[status(thm)],[2067]) ).
thf(2069,plain,
( ( sk4 @ member_type @ ( sk3 @ sk7 @ ilf_type ) )
| ( sk4 @ empty )
| ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[2068:[bind(A,$thf( sk3 @ sk7 )),bind(B,$thf( sk4 ))]]) ).
thf(2052,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ sk7 @ member ) )
!= ( B @ ( A @ member ) ) )
| ( B @ member_type @ ( A @ ilf_type ) )
| ~ $true
| ( B @ empty )
| ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[738,2033]) ).
thf(2053,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ sk7 @ member ) )
!= ( B @ ( A @ member ) ) )
| ( B @ member_type @ ( A @ ilf_type ) )
| ( B @ empty )
| ( sk1 @ empty ) ),
inference(simp,[status(thm)],[2052]) ).
thf(2054,plain,
( ( sk2 @ member_type @ ( sk1 @ sk7 @ ilf_type ) )
| ( sk2 @ empty )
| ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[2053:[bind(A,$thf( sk1 @ sk7 )),bind(B,$thf( sk2 ))]]) ).
thf(1737,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ subset_type @ ( A @ power_set @ sk9 @ ilf_type ) )
!= ( B @ subset_type @ ( C @ ilf_type ) ) )
| ( B @ power_set @ member_type @ ( C @ ilf_type ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1732,1507]) ).
thf(1738,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ subset_type @ ( A @ power_set @ sk9 @ ilf_type ) )
!= ( B @ subset_type @ ( C @ ilf_type ) ) )
| ( B @ power_set @ member_type @ ( C @ ilf_type ) ) ),
inference(simp,[status(thm)],[1737]) ).
thf(1739,plain,
! [A: $i] : ( A @ power_set @ member_type @ ( A @ power_set @ sk9 @ ilf_type ) ),
inference(pattern_uni,[status(thm)],[1738:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ power_set @ sk9 ))]]) ).
thf(1758,plain,
! [A: $i] : ( A @ power_set @ member_type @ ( A @ power_set @ sk9 @ ilf_type ) ),
inference(simp,[status(thm)],[1739]) ).
thf(5292,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ cross_product ) @ ( sk1 @ ( sk1 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk2 @ ( B @ cross_product ) @ ( sk1 @ ( A @ cross_product ) @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5103,178]) ).
thf(5293,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ cross_product ) @ ( sk1 @ ( sk1 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk2 @ ( B @ cross_product ) @ ( sk1 @ ( A @ cross_product ) @ subset ) ) ),
inference(simp,[status(thm)],[5292]) ).
thf(5294,plain,
sk2 @ ( sk2 @ ( sk2 @ cross_product ) @ cross_product ) @ ( sk1 @ ( sk1 @ ( sk1 @ cross_product ) @ cross_product ) @ subset ),
inference(pattern_uni,[status(thm)],[5293:[bind(A,$thf( sk1 @ ( sk1 @ cross_product ) )),bind(B,$thf( sk2 @ ( sk2 @ cross_product ) ))]]) ).
thf(1484,plain,
( ( sk4 @ ( sk2 @ cross_product ) )
!= ( sk3 @ ( sk1 @ cross_product ) ) ),
inference(simp,[status(thm)],[1483]) ).
thf(2138,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk3 @ ( A @ member ) ) )
| ( sk4 @ ( A @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1956,415]) ).
thf(2139,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk3 @ ( A @ member ) ) )
| ( sk4 @ ( A @ member ) ) ),
inference(simp,[status(thm)],[2138]) ).
thf(2206,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk3 )
| ( sk5 != A )
| ( sk4 @ ( A @ member ) ) ),
inference(simp,[status(thm)],[2139]) ).
thf(2224,plain,
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk3 )
| ( sk4 @ ( sk5 @ member ) ) ),
inference(simp,[status(thm)],[2206]) ).
thf(4087,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk14 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ~ $true
| ~ ( C @ empty )
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[4066,161]) ).
thf(4088,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk14 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ~ ( C @ empty )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[4087]) ).
thf(4089,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ( A @ ( B @ subset ) ) ),
inference(pattern_uni,[status(thm)],[4088:[bind(A,$thf( F )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ sk14 ) ))]]) ).
thf(4132,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ( A @ ( B @ subset ) ) ),
inference(simp,[status(thm)],[4089]) ).
thf(15,axiom,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( set_type @ ( B @ ( A @ ordered_pair ) @ ilf_type ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p18) ).
thf(72,plain,
! [A: $i] :
( ( set_type @ ( A @ ilf_type ) )
=> ! [B: $i] :
( ( set_type @ ( B @ ilf_type ) )
=> ( set_type @ ( B @ ( A @ ordered_pair ) @ ilf_type ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(757,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk1 @ subset ) )
!= ( A @ ( B @ subset ) ) )
| ( A @ ( B @ sk7 @ member ) )
| ~ $true
| ( B @ empty )
| ( sk3 != sk2 ) ),
inference(paramod_ordered,[status(thm)],[371,412]) ).
thf(758,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk1 @ subset ) )
!= ( A @ ( B @ subset ) ) )
| ( A @ ( B @ sk7 @ member ) )
| ( B @ empty )
| ( sk3 != sk2 ) ),
inference(simp,[status(thm)],[757]) ).
thf(759,plain,
( ( sk4 @ ( sk1 @ sk7 @ member ) )
| ( sk1 @ empty )
| ( sk3 != sk2 ) ),
inference(pattern_uni,[status(thm)],[758:[bind(A,$thf( sk4 )),bind(B,$thf( sk1 ))]]) ).
thf(3398,plain,
! [A: $i] :
( ( ( sk3 @ empty )
!= ( A @ empty ) )
| ~ $true
| ~ ( A @ ( sk3 @ ( sk1 @ cross_product ) @ power_set @ subset ) )
| ~ ( sk2 @ empty )
| ( sk4 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[591,1997]) ).
thf(3399,plain,
! [A: $i] :
( ( ( sk3 @ empty )
!= ( A @ empty ) )
| ~ ( A @ ( sk3 @ ( sk1 @ cross_product ) @ power_set @ subset ) )
| ~ ( sk2 @ empty )
| ( sk4 != sk1 ) ),
inference(simp,[status(thm)],[3398]) ).
thf(3400,plain,
( ~ ( sk3 @ ( sk3 @ ( sk1 @ cross_product ) @ power_set @ subset ) )
| ~ ( sk2 @ empty )
| ( sk4 != sk1 ) ),
inference(pattern_uni,[status(thm)],[3399:[bind(A,$thf( sk3 ))]]) ).
thf(3857,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ sk9 @ member ) )
!= ( B @ ( A @ member ) ) )
| ( B @ member_type @ ( A @ ilf_type ) )
| ~ $true
| ( B @ empty )
| ( sk1 @ empty ) ),
inference(paramod_ordered,[status(thm)],[3827,2033]) ).
thf(3858,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ sk9 @ member ) )
!= ( B @ ( A @ member ) ) )
| ( B @ member_type @ ( A @ ilf_type ) )
| ( B @ empty )
| ( sk1 @ empty ) ),
inference(simp,[status(thm)],[3857]) ).
thf(3859,plain,
( ( sk2 @ member_type @ ( sk1 @ sk9 @ ilf_type ) )
| ( sk2 @ empty )
| ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[3858:[bind(A,$thf( sk1 @ sk9 )),bind(B,$thf( sk2 ))]]) ).
thf(2260,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ sk12 @ member ) )
!= ( B @ ( A @ member ) ) )
| ( B @ member_type @ ( A @ ilf_type ) )
| ~ $true
| ( B @ empty )
| ( sk3 @ relation_like ) ),
inference(paramod_ordered,[status(thm)],[2144,2033]) ).
thf(2261,plain,
! [B: $i,A: $i] :
( ( ( sk4 @ ( sk3 @ sk12 @ member ) )
!= ( B @ ( A @ member ) ) )
| ( B @ member_type @ ( A @ ilf_type ) )
| ( B @ empty )
| ( sk3 @ relation_like ) ),
inference(simp,[status(thm)],[2260]) ).
thf(2262,plain,
( ( sk4 @ member_type @ ( sk3 @ sk12 @ ilf_type ) )
| ( sk4 @ empty )
| ( sk3 @ relation_like ) ),
inference(pattern_uni,[status(thm)],[2261:[bind(A,$thf( sk3 @ sk12 )),bind(B,$thf( sk4 ))]]) ).
thf(111,plain,
( ( ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) )
!= ( sk3 @ ( sk1 @ relation_type ) @ ( sk5 @ ilf_type ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[28,24]) ).
thf(112,plain,
( ( sk4 @ ( sk2 @ relation_type ) @ ( sk5 @ ilf_type ) )
!= ( sk3 @ ( sk1 @ relation_type ) @ ( sk5 @ ilf_type ) ) ),
inference(simp,[status(thm)],[111]) ).
thf(113,plain,
( ( ( sk4 @ ( sk2 @ relation_type ) )
!= ( sk3 @ ( sk1 @ relation_type ) ) )
| ( sk5 != sk5 ) ),
inference(simp,[status(thm)],[112]) ).
thf(114,plain,
( ( sk4 @ ( sk2 @ relation_type ) )
!= ( sk3 @ ( sk1 @ relation_type ) ) ),
inference(simp,[status(thm)],[113]) ).
thf(566,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk12 @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ( A @ relation_like ) ),
inference(paramod_ordered,[status(thm)],[461,459]) ).
thf(567,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk12 @ member ) )
!= ( sk3 @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ( A @ relation_like ) ),
inference(simp,[status(thm)],[566]) ).
thf(568,plain,
( ~ ( sk4 @ empty )
| ( sk3 @ relation_like ) ),
inference(pattern_uni,[status(thm)],[567:[bind(A,$thf( sk3 )),bind(B,$thf( sk3 @ sk12 ))]]) ).
thf(82,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ relation_like )
| ( ( A @ sk12 )
!= ( C @ ( B @ ordered_pair ) ) )
| ~ ( set_type @ ( C @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) ) ),
inference(cnfConj,[status(thm)],[79]) ).
thf(87,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ relation_like )
| ~ ( set_type @ ( C @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) )
| ( ( A @ sk12 )
!= ( C @ ( B @ ordered_pair ) ) ) ),
inference(lifteq,[status(thm)],[82]) ).
thf(88,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ relation_like )
| ~ ( set_type @ ( C @ ilf_type ) )
| ~ ( set_type @ ( B @ ilf_type ) )
| ~ ( set_type @ ( A @ ilf_type ) )
| ( ( A @ sk12 )
!= ( C @ ( B @ ordered_pair ) ) ) ),
inference(simp,[status(thm)],[87]) ).
thf(3597,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ relation_like )
| ~ $true
| ~ $true
| ~ $true
| ( ( A @ sk12 )
!= ( C @ ( B @ ordered_pair ) ) ) ),
inference(rewrite,[status(thm)],[88,35]) ).
thf(3598,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ relation_like )
| ( ( A @ sk12 )
!= ( C @ ( B @ ordered_pair ) ) ) ),
inference(simp,[status(thm)],[3597]) ).
thf(1297,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ subset_type @ ( A @ sk13 @ ilf_type ) )
!= ( C @ ( B @ cross_product ) @ subset_type @ ( D @ ilf_type ) ) )
| ( C @ ( B @ relation_type ) @ ( D @ ilf_type ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[163,1283]) ).
thf(1298,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ subset_type @ ( A @ sk13 @ ilf_type ) )
!= ( C @ ( B @ cross_product ) @ subset_type @ ( D @ ilf_type ) ) )
| ( C @ ( B @ relation_type ) @ ( D @ ilf_type ) ) ),
inference(simp,[status(thm)],[1297]) ).
thf(1299,plain,
! [B: $i,A: $i] : ( B @ ( A @ relation_type ) @ ( B @ ( A @ cross_product ) @ sk13 @ ilf_type ) ),
inference(pattern_uni,[status(thm)],[1298:[bind(A,$thf( G @ ( F @ cross_product ) )),bind(B,$thf( F )),bind(C,$thf( G )),bind(D,$thf( G @ ( F @ cross_product ) @ sk13 ))]]) ).
thf(1308,plain,
! [B: $i,A: $i] : ( B @ ( A @ relation_type ) @ ( B @ ( A @ cross_product ) @ sk13 @ ilf_type ) ),
inference(simp,[status(thm)],[1299]) ).
thf(4114,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk14 ) @ member ) )
!= ( sk3 @ ( C @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[4066,459]) ).
thf(4115,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk14 ) @ member ) )
!= ( sk3 @ ( C @ member ) ) )
| ~ ( sk4 @ empty )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[4114]) ).
thf(4116,plain,
! [A: $i] :
( ~ ( sk4 @ empty )
| ( A @ ( sk3 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[4115:[bind(A,$thf( sk3 )),bind(B,$thf( D )),bind(C,$thf( sk3 @ ( D @ sk14 ) ))]]) ).
thf(4129,plain,
! [A: $i] :
( ~ ( sk4 @ empty )
| ( A @ ( sk3 @ subset ) ) ),
inference(simp,[status(thm)],[4116]) ).
thf(4370,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk3 @ subset ) )
!= ( sk1 @ ( B @ subset ) ) )
| ( sk2 @ ( B @ subset ) )
| ~ $true
| ~ ( sk4 @ empty ) ),
inference(paramod_ordered,[status(thm)],[4129,209]) ).
thf(4371,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk3 @ subset ) )
!= ( sk1 @ ( B @ subset ) ) )
| ( sk2 @ ( B @ subset ) )
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[4370]) ).
thf(4372,plain,
( ( sk2 @ ( sk3 @ subset ) )
| ~ ( sk4 @ empty ) ),
inference(pattern_uni,[status(thm)],[4371:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 ))]]) ).
thf(1972,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk3 @ ( A @ member ) ) )
| ~ ( sk2 @ empty )
| ~ $true
| ( sk4 != sk1 ) ),
inference(paramod_ordered,[status(thm)],[1956,457]) ).
thf(1973,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set @ ( sk5 @ member ) )
!= ( sk3 @ ( A @ member ) ) )
| ~ ( sk2 @ empty )
| ( sk4 != sk1 ) ),
inference(simp,[status(thm)],[1972]) ).
thf(1987,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk3 )
| ( sk5 != A )
| ~ ( sk2 @ empty )
| ( sk4 != sk1 ) ),
inference(simp,[status(thm)],[1973]) ).
thf(1994,plain,
( ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk3 )
| ~ ( sk2 @ empty )
| ( sk4 != sk1 ) ),
inference(simp,[status(thm)],[1987]) ).
thf(90,plain,
! [A: $i] :
( ( A @ relation_like )
| ~ ( set_type @ ( A @ ilf_type ) )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[89]) ).
thf(167,plain,
! [A: $i] :
( ( A @ relation_like )
| ~ $true
| ~ ( A @ empty ) ),
inference(rewrite,[status(thm)],[90,35]) ).
thf(168,plain,
! [A: $i] :
( ( A @ relation_like )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[167]) ).
thf(146,plain,
( ( sk4 != sk3 )
| ( sk2 != sk1 ) ),
inference(simp,[status(thm)],[114]) ).
thf(2927,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set @ ( A @ member ) )
!= ( sk5 @ ( B @ member ) ) )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1139,2760]) ).
thf(2928,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set @ ( A @ member ) )
!= ( sk5 @ ( B @ member ) ) )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty ) ),
inference(simp,[status(thm)],[2927]) ).
thf(2993,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set )
!= sk5 )
| ( A != B )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty ) ),
inference(simp,[status(thm)],[2928]) ).
thf(3015,plain,
! [A: $i] :
( ( ( A @ power_set )
!= sk5 )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty ) ),
inference(simp,[status(thm)],[2993]) ).
thf(5707,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk4 @ cross_product ) @ ( sk1 @ ( sk3 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk4 @ ( B @ cross_product ) @ ( sk3 @ ( A @ cross_product ) @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5124,184]) ).
thf(5708,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk4 @ cross_product ) @ ( sk1 @ ( sk3 @ cross_product ) @ subset ) )
!= ( B @ ( A @ subset ) ) )
| ( sk4 @ ( B @ cross_product ) @ ( sk3 @ ( A @ cross_product ) @ subset ) ) ),
inference(simp,[status(thm)],[5707]) ).
thf(5709,plain,
sk4 @ ( sk2 @ ( sk4 @ cross_product ) @ cross_product ) @ ( sk3 @ ( sk1 @ ( sk3 @ cross_product ) @ cross_product ) @ subset ),
inference(pattern_uni,[status(thm)],[5708:[bind(A,$thf( sk1 @ ( sk3 @ cross_product ) )),bind(B,$thf( sk2 @ ( sk4 @ cross_product ) ))]]) ).
thf(504,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk12 @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ~ ( sk2 @ empty )
| ~ $true
| ( A @ relation_like ) ),
inference(paramod_ordered,[status(thm)],[461,453]) ).
thf(505,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk12 @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ~ ( sk2 @ empty )
| ( A @ relation_like ) ),
inference(simp,[status(thm)],[504]) ).
thf(506,plain,
( ~ ( sk2 @ empty )
| ( sk1 @ relation_like ) ),
inference(pattern_uni,[status(thm)],[505:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ sk12 ))]]) ).
thf(2547,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ~ ( sk3 @ ( A @ subset ) )
| ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[2452,450]) ).
thf(2548,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ~ ( sk3 @ ( A @ subset ) )
| ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk1 ) ),
inference(simp,[status(thm)],[2547]) ).
thf(2549,plain,
( ~ ( sk4 @ empty )
| ~ ( sk3 @ ( sk2 @ subset ) )
| ( ( sk3 @ ( sk1 @ cross_product ) @ power_set )
!= sk1 ) ),
inference(pattern_uni,[status(thm)],[2548:[bind(A,$thf( sk2 )),bind(B,$thf( sk5 ))]]) ).
thf(3409,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ subset ) )
!= ( B @ ( sk3 @ ( sk1 @ cross_product ) @ power_set @ subset ) ) )
| ~ ( B @ empty )
| ~ $true
| ~ ( sk1 @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[209,1997]) ).
thf(3410,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ subset ) )
!= ( B @ ( sk3 @ ( sk1 @ cross_product ) @ power_set @ subset ) ) )
| ~ ( B @ empty )
| ~ ( sk1 @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[3409]) ).
thf(3411,plain,
( ~ ( sk2 @ empty )
| ~ ( sk1 @ ( sk3 @ ( sk1 @ cross_product ) @ power_set @ subset ) ) ),
inference(pattern_uni,[status(thm)],[3410:[bind(A,$thf( sk3 @ ( sk1 @ cross_product ) @ power_set )),bind(B,$thf( sk2 ))]]) ).
thf(594,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk12 @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ~ $true
| ( sk3 != sk2 )
| ( A @ relation_like ) ),
inference(paramod_ordered,[status(thm)],[461,502]) ).
thf(595,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk12 @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ~ ( sk4 @ empty )
| ( sk3 != sk2 )
| ( A @ relation_like ) ),
inference(simp,[status(thm)],[594]) ).
thf(596,plain,
( ~ ( sk4 @ empty )
| ( sk3 != sk2 )
| ( sk1 @ relation_like ) ),
inference(pattern_uni,[status(thm)],[595:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ sk12 ))]]) ).
thf(4711,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk5 @ subset ) )
!= ( sk1 @ ( B @ subset ) ) )
| ( sk2 @ ( B @ subset ) )
| ~ $true
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty ) ),
inference(paramod_ordered,[status(thm)],[4122,209]) ).
thf(4712,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk5 @ subset ) )
!= ( sk1 @ ( B @ subset ) ) )
| ( sk2 @ ( B @ subset ) )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty ) ),
inference(simp,[status(thm)],[4711]) ).
thf(4713,plain,
( ( sk2 @ ( sk5 @ subset ) )
| ~ ( sk3 @ ( sk1 @ cross_product ) @ empty ) ),
inference(pattern_uni,[status(thm)],[4712:[bind(A,$thf( sk1 )),bind(B,$thf( sk5 ))]]) ).
thf(3810,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk9 @ member ) )
!= ( sk5 @ ( B @ member ) ) )
| ( sk3 @ ( sk1 @ cross_product ) @ ( B @ member ) )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[1845,1990]) ).
thf(3811,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk9 @ member ) )
!= ( sk5 @ ( B @ member ) ) )
| ( sk3 @ ( sk1 @ cross_product ) @ ( B @ member ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[3810]) ).
thf(3812,plain,
( ( sk3 @ ( sk1 @ cross_product ) @ ( sk5 @ sk9 @ member ) )
| ( sk5 @ empty ) ),
inference(pattern_uni,[status(thm)],[3811:[bind(A,$thf( sk5 )),bind(B,$thf( sk5 @ sk9 ))]]) ).
thf(2717,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set @ ( A @ member ) )
!= ( sk5 @ ( B @ member ) ) )
| ( sk3 @ ( sk1 @ cross_product ) @ ( B @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1139,1990]) ).
thf(2718,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set @ ( A @ member ) )
!= ( sk5 @ ( B @ member ) ) )
| ( sk3 @ ( sk1 @ cross_product ) @ ( B @ member ) ) ),
inference(simp,[status(thm)],[2717]) ).
thf(2816,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set )
!= sk5 )
| ( A != B )
| ( sk3 @ ( sk1 @ cross_product ) @ ( B @ member ) ) ),
inference(simp,[status(thm)],[2718]) ).
thf(2832,plain,
! [A: $i] :
( ( ( A @ power_set )
!= sk5 )
| ( sk3 @ ( sk1 @ cross_product ) @ ( A @ member ) ) ),
inference(simp,[status(thm)],[2816]) ).
thf(2346,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set @ ( A @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ( sk2 @ ( B @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1139,418]) ).
thf(2347,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set @ ( A @ member ) )
!= ( sk1 @ ( B @ member ) ) )
| ( sk2 @ ( B @ member ) ) ),
inference(simp,[status(thm)],[2346]) ).
thf(2440,plain,
! [B: $i,A: $i] :
( ( ( A @ power_set )
!= sk1 )
| ( A != B )
| ( sk2 @ ( B @ member ) ) ),
inference(simp,[status(thm)],[2347]) ).
thf(2453,plain,
! [A: $i] :
( ( ( A @ power_set )
!= sk1 )
| ( sk2 @ ( A @ member ) ) ),
inference(simp,[status(thm)],[2440]) ).
thf(217290,plain,
$false,
inference(e,[status(thm)],[2452,1995,893,3830,1982,1956,582,1290,2231,1422,5625,4532,142,153,1507,898,5935,24,4198,1529,1482,1055,184,196,4119,93,1013,57,78,3268,29,591,1334,3923,1283,453,89,74,3011,248,5839,2496,512,5783,3827,1619,28,38,3022,1502,197,461,324,847,5879,1592,1762,1017,1425,1719,1755,5387,4736,515,738,2845,457,2482,371,605,2125,1099,1333,2883,765,1996,1732,1991,2788,2144,412,5666,1754,2033,166,161,64,34,1483,32,22,286,4122,577,27,1139,1997,49,172,5103,76,245,3710,377,1589,631,1557,609,140,91,155,1177,932,1556,5180,768,1015,1477,922,35,2069,2054,1758,209,1990,5652,145,1845,855,5294,1484,2224,502,4132,2357,72,386,43,2760,450,1180,203,759,5124,3400,250,896,3859,418,2262,55,114,568,3598,1308,4372,1994,36,168,146,3015,136,5709,506,2549,415,4129,3411,596,47,4713,163,68,62,178,3812,459,4066,2832,215,2453,309,1463]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SET655+3 : TPTP v9.3.1. Released v2.2.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.05/0.32 % Computer : n012.cluster.edu
% 0.05/0.32 % Model : x86_64 x86_64
% 0.05/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.32 % Memory : 8046.5625MB
% 0.05/0.32 % OS : Linux 6.8.0-71-generic
% 0.05/0.32 % CPULimit : 300
% 0.05/0.32 % WCLimit : 300
% 0.05/0.32 % DateTime : Sat Sep 26 08:03:19 UTC 2026
% 0.05/0.32 % CPUTime :
% 0.05/0.32 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.61/0.77 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.94/0.94 % [INFO] Parsing done (172ms).
% 0.94/0.96 % [INFO] Running in sequential loop mode.
% 1.51/1.28 % [INFO] eprover registered as external prover.
% 1.51/1.29 % [INFO] Scanning for conjecture ...
% 1.72/1.38 % [INFO] Found a conjecture (or negated_conjecture) and 19 axioms. Running axiom selection ...
% 1.93/1.44 % [INFO] Axiom selection finished. Selected 19 axioms (removed 0 axioms).
% 1.93/1.49 % [INFO] Problem is first-order (TPTP FOF).
% 2.17/1.50 % [INFO] Type checking passed.
% 2.17/1.50 % [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 ...
% 254.88/74.13 % External prover 'e' found a proof!
% 254.88/74.13 % [INFO] Killing All external provers ...
% 254.88/74.13 % Time passed: 73710ms (effective reasoning time: 73170ms)
% 254.88/74.13 % 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)>
% 254.88/74.13 % Axioms used in derivation (19): p16, p12, p18, p15, p3, p11, p2, p14, p17, p9, p1, p13, p10, p19, p4, p7, p5, p6, p8
% 254.88/74.13 % No. of inferences in proof: 597
% 254.88/74.13 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 73710 ms resp. 73170 ms w/o parsing
% 244.63/74.26 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 244.63/74.26 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------