%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SET076+1 : TPTP v9.3.1. Bugfixed v5.4.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 : n018.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:29:16 AM UTC 2026
% Result : Theorem 83.50s 19.48s
% Output : Refutation 70.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 53
% Syntax : Number of formulae : 1032 ( 348 unt; 0 typ; 9 def)
% Number of atoms : 2927 ( 902 equ; 0 cnn)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 9603 (1408 ~; 880 |; 197 &;6997 @)
% ( 19 <=>; 102 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 43 ( 40 usr; 12 con; 0-3 aty)
% Number of variables : 1233 ( 7 ^;1200 !; 17 ?;1233 :)
% ( 0 !>; 0 ?*; 0 @-; 9 @+)
% Comments :
%------------------------------------------------------------------------------
thf(member_decl,type,
member: $i > $i > $o ).
thf(subclass_decl,type,
subclass: $i > $i > $o ).
thf(unordered_pair_decl,type,
unordered_pair: $i > $i > $i ).
thf(apply_decl,type,
apply: $i > $i > $i ).
thf(sum_class_decl,type,
sum_class: $i > $i ).
thf(image_decl,type,
image: $i > $i > $i ).
thf(singleton_decl,type,
singleton: $i > $i ).
thf(successor_decl,type,
successor: $i > $i ).
thf(union_decl,type,
union: $i > $i > $i ).
thf(inverse_decl,type,
inverse: $i > $i ).
thf(domain_of_decl,type,
domain_of: $i > $i ).
thf(flip_decl,type,
flip: $i > $i ).
thf(cross_product_decl,type,
cross_product: $i > $i > $i ).
thf(universal_class_decl,type,
universal_class: $i ).
thf(range_of_decl,type,
range_of: $i > $i ).
thf(restrict_decl,type,
restrict: $i > $i > $i > $i ).
thf(intersection_decl,type,
intersection: $i > $i > $i ).
thf(null_class_decl,type,
null_class: $i ).
thf(function_decl,type,
function: $i > $o ).
thf(compose_decl,type,
compose: $i > $i > $i ).
thf(identity_relation_decl,type,
identity_relation: $i ).
thf(inductive_decl,type,
inductive: $i > $o ).
thf(successor_relation_decl,type,
successor_relation: $i ).
thf(power_class_decl,type,
power_class: $i > $i ).
thf(ordered_pair_decl,type,
ordered_pair: $i > $i > $i ).
thf(disjoint_decl,type,
disjoint: $i > $i > $o ).
thf(first_decl,type,
first: $i > $i ).
thf(second_decl,type,
second: $i > $i ).
thf(rotate_decl,type,
rotate: $i > $i ).
thf(element_relation_decl,type,
element_relation: $i ).
thf(complement_decl,type,
complement: $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 > $i > $i ).
thf(sk5_decl,type,
sk5: $i > $i > $i ).
thf(sk6_decl,type,
sk6: $i > $i ).
thf(sk7_decl,type,
sk7: $i > $i > $i ).
thf(sk8_decl,type,
sk8: $i ).
thf(sk9_decl,type,
sk9: $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i,C: $i] :
( ( ( C @ ( B @ member ) )
& ( C @ ( A @ member ) ) )
=> ( C @ ( B @ ( A @ unordered_pair ) @ subclass ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ! [B: $i] :
( ( ( B @ ( A @ member ) )
& ( B @ ( sk1 @ member ) ) )
=> ( B @ ( A @ ( sk1 @ unordered_pair ) @ subclass ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ( ( A @ ( sk2 @ member ) )
& ( A @ ( sk1 @ member ) ) )
=> ( A @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( ( A @ ( C @ member ) )
& ( C @ ( B @ member ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( B @ ( C @ member ) )
=> ( A @ ( C @ member ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: $i] :
@+[B: $i] :
( ( A @ ( B @ disjoint ) )
& ( A @ ( B @ member ) )
& ( universal_class @ ( B @ member ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( ( A @ ( C @ member ) )
& ( B @ ( C @ member ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( @+[A: $i] :
( ! [B: $i] :
( ( B @ inductive )
=> ( B @ ( A @ subclass ) ) )
& ( A @ inductive )
& ( universal_class @ ( A @ member ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( @+[A: $i] :
( ! [B: $i] :
( ( universal_class @ ( B @ member ) )
=> ( ( B @ ( B @ ( A @ apply ) @ member ) )
| ( B = null_class ) ) )
& ( A @ function ) ) ) ) ).
thf(9,axiom,
! [A: $i,B: $i] :
( ( B @ sum_class @ ( A @ member ) )
<=> ? [C: $i] :
( ( B @ ( C @ member ) )
& ( C @ ( A @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_class_defn) ).
thf(69,plain,
! [A: $i,B: $i] :
( ( ? [C: $i] :
( ( B @ ( C @ member ) )
& ( C @ ( A @ member ) ) )
=> ( B @ sum_class @ ( A @ member ) ) )
& ( ( B @ sum_class @ ( A @ member ) )
=> ? [C: $i] :
( ( B @ ( C @ member ) )
& ( C @ ( A @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(41,axiom,
universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_relation) ).
thf(259,plain,
universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(11,axiom,
! [A: $i,B: $i] :
( ( A = B )
<=> ( ( A @ ( B @ subclass ) )
& ( B @ ( A @ subclass ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',extensionality) ).
thf(85,plain,
! [A: $i,B: $i] :
( ( ( ( A @ ( B @ subclass ) )
& ( B @ ( A @ subclass ) ) )
=> ( A = B ) )
& ( ( A = B )
=> ( ( A @ ( B @ subclass ) )
& ( B @ ( A @ subclass ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(86,plain,
( ! [A: $i,B: $i] :
( ( ( A @ ( B @ subclass ) )
& ( B @ ( A @ subclass ) ) )
=> ( A = B ) )
& ! [A: $i,B: $i] :
( ( A = B )
=> ( ( A @ ( B @ subclass ) )
& ( B @ ( A @ subclass ) ) ) ) ),
inference(miniscope,[status(thm)],[85]) ).
thf(87,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C = D )
| ~ ( C @ ( D @ subclass ) )
| ~ ( D @ ( C @ subclass ) ) )
& ( ( A @ ( B @ subclass ) )
| ( A != B ) )
& ( ( B @ ( A @ subclass ) )
| ( A != B ) ) ),
inference(cnf,[status(esa)],[86]) ).
thf(90,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ subclass ) )
| ~ ( B @ ( A @ subclass ) ) ),
inference(cnfConj,[status(thm)],[87]) ).
thf(95,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ subclass ) )
| ~ ( B @ ( A @ subclass ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[90]) ).
thf(96,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ subclass ) )
| ~ ( B @ ( A @ subclass ) )
| ( A = B ) ),
inference(simp,[status(thm)],[95]) ).
thf(30,axiom,
? [A: $i] :
( ! [B: $i] :
( ( B @ inductive )
=> ( B @ ( A @ subclass ) ) )
& ( A @ inductive )
& ( universal_class @ ( A @ member ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',infinity) ).
thf(209,plain,
? [A: $i] :
( ! [B: $i] :
( ( B @ inductive )
=> ( B @ ( A @ subclass ) ) )
& ( A @ inductive )
& ( universal_class @ ( A @ member ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(210,plain,
! [A: $i] :
( ( ( A @ ( sk8 @ subclass ) )
| ~ ( A @ inductive ) )
& ( sk8 @ inductive )
& ( universal_class @ ( sk8 @ member ) ) ),
inference(cnf,[status(esa)],[209]) ).
thf(211,plain,
universal_class @ ( sk8 @ member ),
inference(cnfConj,[status(thm)],[210]) ).
thf(31,axiom,
! [A: $i] :
~ ( null_class @ ( A @ member ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',null_class_defn) ).
thf(214,plain,
! [A: $i] :
~ ( null_class @ ( A @ member ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(215,plain,
~ ? [A: $i] : ( null_class @ ( A @ member ) ),
inference(miniscope,[status(thm)],[214]) ).
thf(216,plain,
! [A: $i] :
~ ( null_class @ ( A @ member ) ),
inference(cnf,[status(esa)],[215]) ).
thf(284,plain,
! [A: $i] :
( ( ( universal_class @ ( sk8 @ member ) )
!= ( null_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[211,216]) ).
thf(285,plain,
! [A: $i] :
( ( universal_class @ ( sk8 @ member ) )
!= ( null_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[284]) ).
thf(286,plain,
! [A: $i] :
( ( null_class != universal_class )
| ( sk8 != A ) ),
inference(simp,[status(thm)],[285]) ).
thf(287,plain,
null_class != universal_class,
inference(simp,[status(thm)],[286]) ).
thf(3329,plain,
! [B: $i,A: $i] :
( ( A != null_class )
| ( B != universal_class )
| ~ ( A @ ( B @ subclass ) )
| ~ ( B @ ( A @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[96,287]) ).
thf(3330,plain,
! [A: $i] :
( ( A != universal_class )
| ~ ( null_class @ ( A @ subclass ) )
| ~ ( A @ ( null_class @ subclass ) ) ),
inference(pattern_uni,[status(thm)],[3329:[bind(A,$thf( null_class ))]]) ).
thf(3630,plain,
( ~ ( null_class @ ( universal_class @ subclass ) )
| ~ ( universal_class @ ( null_class @ subclass ) ) ),
inference(simp,[status(thm)],[3330]) ).
thf(37,axiom,
! [A: $i] : ( universal_class @ ( A @ subclass ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',class_elements_are_sets) ).
thf(243,plain,
! [A: $i] : ( universal_class @ ( A @ subclass ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(244,plain,
! [A: $i] : ( universal_class @ ( A @ subclass ) ),
inference(cnf,[status(esa)],[243]) ).
thf(5377,plain,
( ~ ( null_class @ ( universal_class @ subclass ) )
| ~ $true ),
inference(rewrite,[status(thm)],[3630,244]) ).
thf(5378,plain,
~ ( null_class @ ( universal_class @ subclass ) ),
inference(simp,[status(thm)],[5377]) ).
thf(5398,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[259,5378]) ).
thf(5399,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) ),
inference(simp,[status(thm)],[5398]) ).
thf(5422,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( element_relation != universal_class ) ),
inference(simp,[status(thm)],[5399]) ).
thf(12,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ subclass ) )
<=> ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_defn) ).
thf(97,plain,
! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) )
=> ( B @ ( A @ subclass ) ) )
& ( ( B @ ( A @ subclass ) )
=> ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(98,plain,
( ! [A: $i,B: $i] :
( ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) )
=> ( B @ ( A @ subclass ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ subclass ) )
=> ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[97]) ).
thf(99,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( D @ subclass ) )
| ~ ( E @ ( D @ ( E @ sk5 ) @ member ) ) )
& ( ( E @ ( D @ subclass ) )
| ( D @ ( D @ ( E @ sk5 ) @ member ) ) )
& ( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ subclass ) ) ) ),
inference(cnf,[status(esa)],[98]) ).
thf(101,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subclass ) )
| ( A @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(103,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subclass ) )
| ( A @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(simp,[status(thm)],[101]) ).
thf(5404,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ $true
| ( A @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[103,5378]) ).
thf(5405,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ( A @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(simp,[status(thm)],[5404]) ).
thf(5406,plain,
universal_class @ ( universal_class @ ( null_class @ sk5 ) @ member ),
inference(pattern_uni,[status(thm)],[5405:[bind(A,$thf( universal_class )),bind(B,$thf( null_class ))]]) ).
thf(70,plain,
( ! [A: $i,B: $i] :
( ? [C: $i] :
( ( B @ ( C @ member ) )
& ( C @ ( A @ member ) ) )
=> ( B @ sum_class @ ( A @ member ) ) )
& ! [A: $i,B: $i] :
( ( B @ sum_class @ ( A @ member ) )
=> ? [C: $i] :
( ( B @ ( C @ member ) )
& ( C @ ( A @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[69]) ).
thf(71,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ sum_class @ ( C @ member ) )
| ~ ( D @ ( E @ member ) )
| ~ ( E @ ( C @ member ) ) )
& ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
| ~ ( B @ sum_class @ ( A @ member ) ) )
& ( ( A @ ( B @ sk4 ) @ ( A @ member ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ) ),
inference(cnf,[status(esa)],[70]) ).
thf(73,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ sk4 ) @ member ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[71]) ).
thf(1203,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[73,216]) ).
thf(1204,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[1203]) ).
thf(1205,plain,
! [A: $i] :
~ ( null_class @ sum_class @ ( A @ member ) ),
inference(pattern_uni,[status(thm)],[1204:[bind(A,$thf( E )),bind(B,$thf( null_class )),bind(C,$thf( E @ ( null_class @ sk4 ) ))]]) ).
thf(1295,plain,
! [A: $i] :
~ ( null_class @ sum_class @ ( A @ member ) ),
inference(simp,[status(thm)],[1205]) ).
thf(1313,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[73,1295]) ).
thf(1314,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ ( C @ member ) ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[1313]) ).
thf(1315,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(pattern_uni,[status(thm)],[1314:[bind(A,$thf( E )),bind(B,$thf( null_class @ sum_class )),bind(C,$thf( E @ ( null_class @ sum_class @ sk4 ) ))]]) ).
thf(1346,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(simp,[status(thm)],[1315]) ).
thf(1625,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[73,1346]) ).
thf(1626,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[1625]) ).
thf(1627,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(pattern_uni,[status(thm)],[1626:[bind(A,$thf( E )),bind(B,$thf( null_class @ sum_class @ sum_class )),bind(C,$thf( E @ ( null_class @ sum_class @ sum_class @ sk4 ) ))]]) ).
thf(1679,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(simp,[status(thm)],[1627]) ).
thf(1810,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[73,1679]) ).
thf(1811,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[1810]) ).
thf(1812,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(pattern_uni,[status(thm)],[1811:[bind(A,$thf( E )),bind(B,$thf( null_class @ sum_class @ sum_class @ sum_class )),bind(C,$thf( E @ ( null_class @ sum_class @ sum_class @ sum_class @ sk4 ) ))]]) ).
thf(1857,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(simp,[status(thm)],[1812]) ).
thf(2103,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[73,1857]) ).
thf(2104,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[2103]) ).
thf(2105,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(pattern_uni,[status(thm)],[2104:[bind(A,$thf( E )),bind(B,$thf( null_class @ sum_class @ sum_class @ sum_class @ sum_class )),bind(C,$thf( E @ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sk4 ) ))]]) ).
thf(2169,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(simp,[status(thm)],[2105]) ).
thf(4012,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[73,2169]) ).
thf(4013,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[4012]) ).
thf(4014,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(pattern_uni,[status(thm)],[4013:[bind(A,$thf( E )),bind(B,$thf( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )),bind(C,$thf( E @ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sk4 ) ))]]) ).
thf(4089,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(simp,[status(thm)],[4014]) ).
thf(12976,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ ( null_class @ sk5 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5406,4089]) ).
thf(12977,plain,
! [A: $i] :
( ( universal_class @ ( universal_class @ ( null_class @ sk5 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[12976]) ).
thf(13096,plain,
! [A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= universal_class )
| ( ( universal_class @ ( null_class @ sk5 ) )
!= A ) ),
inference(simp,[status(thm)],[12977]) ).
thf(13137,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= universal_class ),
inference(simp,[status(thm)],[13096]) ).
thf(19,axiom,
! [A: $i] :
( ( A != null_class )
=> ? [B: $i] :
( ( A @ ( B @ disjoint ) )
& ( A @ ( B @ member ) )
& ( universal_class @ ( B @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regularity) ).
thf(143,plain,
! [A: $i] :
( ( A != null_class )
=> ? [B: $i] :
( ( A @ ( B @ disjoint ) )
& ( A @ ( B @ member ) )
& ( universal_class @ ( B @ member ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(144,plain,
! [A: $i] :
( ( ( A @ ( A @ sk6 @ disjoint ) )
| ( A = null_class ) )
& ( ( A @ ( A @ sk6 @ member ) )
| ( A = null_class ) )
& ( ( universal_class @ ( A @ sk6 @ member ) )
| ( A = null_class ) ) ),
inference(cnf,[status(esa)],[143]) ).
thf(146,plain,
! [A: $i] :
( ( A @ ( A @ sk6 @ member ) )
| ( A = null_class ) ),
inference(cnfConj,[status(thm)],[144]) ).
thf(149,plain,
! [A: $i] :
( ( A @ ( A @ sk6 @ member ) )
| ( A = null_class ) ),
inference(lifteq,[status(thm)],[146]) ).
thf(15131,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk6 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ~ $true
| ( A = null_class ) ),
inference(paramod_ordered,[status(thm)],[149,2169]) ).
thf(15132,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk6 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ( A = null_class ) ),
inference(simp,[status(thm)],[15131]) ).
thf(15133,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
= null_class ),
inference(pattern_uni,[status(thm)],[15132:[bind(A,$thf( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )),bind(B,$thf( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sk6 ))]]) ).
thf(16027,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk6 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ~ $true
| ( A = null_class ) ),
inference(paramod_ordered,[status(thm)],[149,1679]) ).
thf(16028,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk6 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ( A = null_class ) ),
inference(simp,[status(thm)],[16027]) ).
thf(16029,plain,
( ( null_class @ sum_class @ sum_class @ sum_class )
= null_class ),
inference(pattern_uni,[status(thm)],[16028:[bind(A,$thf( null_class @ sum_class @ sum_class @ sum_class )),bind(B,$thf( null_class @ sum_class @ sum_class @ sum_class @ sk6 ))]]) ).
thf(14937,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk6 @ member ) )
!= ( null_class @ sum_class @ ( B @ member ) ) )
| ~ $true
| ( A = null_class ) ),
inference(paramod_ordered,[status(thm)],[149,1295]) ).
thf(14938,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk6 @ member ) )
!= ( null_class @ sum_class @ ( B @ member ) ) )
| ( A = null_class ) ),
inference(simp,[status(thm)],[14937]) ).
thf(14939,plain,
( ( null_class @ sum_class )
= null_class ),
inference(pattern_uni,[status(thm)],[14938:[bind(A,$thf( null_class @ sum_class )),bind(B,$thf( null_class @ sum_class @ sk6 ))]]) ).
thf(19211,plain,
( ( null_class @ sum_class @ sum_class )
= null_class ),
inference(rewrite,[status(thm)],[16029,14939]) ).
thf(21467,plain,
( ( null_class @ sum_class @ sum_class @ sum_class )
= null_class ),
inference(rewrite,[status(thm)],[15133,19211]) ).
thf(22966,plain,
( ( null_class @ sum_class @ sum_class @ sum_class )
!= universal_class ),
inference(rewrite,[status(thm)],[13137,21467]) ).
thf(145,plain,
! [A: $i] :
( ( universal_class @ ( A @ sk6 @ member ) )
| ( A = null_class ) ),
inference(cnfConj,[status(thm)],[144]) ).
thf(148,plain,
! [A: $i] :
( ( universal_class @ ( A @ sk6 @ member ) )
| ( A = null_class ) ),
inference(lifteq,[status(thm)],[145]) ).
thf(1,conjecture,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ member ) )
& ( C @ ( A @ member ) ) )
=> ( C @ ( B @ ( A @ unordered_pair ) @ subclass ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_is_subset) ).
thf(2,negated_conjecture,
~ ! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ member ) )
& ( C @ ( A @ member ) ) )
=> ( C @ ( B @ ( A @ unordered_pair ) @ subclass ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(46,plain,
~ ! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ member ) )
& ( C @ ( A @ member ) ) )
=> ( C @ ( B @ ( A @ unordered_pair ) @ subclass ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(47,plain,
( ~ ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) )
& ( sk3 @ ( sk2 @ member ) )
& ( sk3 @ ( sk1 @ member ) ) ),
inference(cnf,[status(esa)],[46]) ).
thf(49,plain,
sk3 @ ( sk2 @ member ),
inference(cnfConj,[status(thm)],[47]) ).
thf(276,plain,
! [A: $i] :
( ( ( sk3 @ ( sk2 @ member ) )
!= ( null_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,216]) ).
thf(277,plain,
! [A: $i] :
( ( sk3 @ ( sk2 @ member ) )
!= ( null_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[276]) ).
thf(280,plain,
! [A: $i] :
( ( sk3 != null_class )
| ( sk2 != A ) ),
inference(simp,[status(thm)],[277]) ).
thf(282,plain,
sk3 != null_class,
inference(simp,[status(thm)],[280]) ).
thf(3193,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( B != null_class )
| ~ ( A @ ( B @ subclass ) )
| ~ ( B @ ( A @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[96,282]) ).
thf(3194,plain,
! [A: $i] :
( ( A != null_class )
| ~ ( sk3 @ ( A @ subclass ) )
| ~ ( A @ ( sk3 @ subclass ) ) ),
inference(pattern_uni,[status(thm)],[3193:[bind(A,$thf( sk3 ))]]) ).
thf(3575,plain,
( ~ ( sk3 @ ( null_class @ subclass ) )
| ~ ( null_class @ ( sk3 @ subclass ) ) ),
inference(simp,[status(thm)],[3194]) ).
thf(4608,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk5 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ~ $true
| ( B @ ( A @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[103,216]) ).
thf(4609,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk5 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ( B @ ( A @ subclass ) ) ),
inference(simp,[status(thm)],[4608]) ).
thf(4610,plain,
! [A: $i] : ( A @ ( null_class @ subclass ) ),
inference(pattern_uni,[status(thm)],[4609:[bind(A,$thf( null_class )),bind(B,$thf( D )),bind(C,$thf( null_class @ ( D @ sk5 ) ))]]) ).
thf(4694,plain,
! [A: $i] : ( A @ ( null_class @ subclass ) ),
inference(simp,[status(thm)],[4610]) ).
thf(4720,plain,
( ~ $true
| ~ ( null_class @ ( sk3 @ subclass ) ) ),
inference(rewrite,[status(thm)],[3575,4694]) ).
thf(4721,plain,
~ ( null_class @ ( sk3 @ subclass ) ),
inference(simp,[status(thm)],[4720]) ).
thf(4777,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( sk3 @ subclass ) ) )
| ~ $true
| ( A @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[103,4721]) ).
thf(4778,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( sk3 @ subclass ) ) )
| ( A @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(simp,[status(thm)],[4777]) ).
thf(4779,plain,
sk3 @ ( sk3 @ ( null_class @ sk5 ) @ member ),
inference(pattern_uni,[status(thm)],[4778:[bind(A,$thf( sk3 )),bind(B,$thf( null_class ))]]) ).
thf(4823,plain,
! [A: $i] :
( ( A
!= ( sk3 @ ( null_class @ sk5 ) ) )
| ( sk3 @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,4779]) ).
thf(4824,plain,
( ( sk3 @ ( null_class @ member ) )
| ( universal_class @ ( sk3 @ ( null_class @ sk5 ) @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[4823:[bind(A,$thf( sk3 @ ( null_class @ sk5 ) ))]]) ).
thf(39,axiom,
! [A: $i,B: $i] :
( ( A @ complement @ ( B @ member ) )
<=> ( ~ ( A @ ( B @ member ) )
& ( universal_class @ ( B @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement) ).
thf(247,plain,
! [A: $i,B: $i] :
( ( ( ~ ( A @ ( B @ member ) )
& ( universal_class @ ( B @ member ) ) )
=> ( A @ complement @ ( B @ member ) ) )
& ( ( A @ complement @ ( B @ member ) )
=> ( ~ ( A @ ( B @ member ) )
& ( universal_class @ ( B @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(248,plain,
( ! [A: $i,B: $i] :
( ( ~ ( A @ ( B @ member ) )
& ( universal_class @ ( B @ member ) ) )
=> ( A @ complement @ ( B @ member ) ) )
& ! [A: $i,B: $i] :
( ( A @ complement @ ( B @ member ) )
=> ( ~ ( A @ ( B @ member ) )
& ( universal_class @ ( B @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[247]) ).
thf(249,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ complement @ ( D @ member ) )
| ( C @ ( D @ member ) )
| ~ ( universal_class @ ( D @ member ) ) )
& ( ~ ( A @ ( B @ member ) )
| ~ ( A @ complement @ ( B @ member ) ) )
& ( ( universal_class @ ( B @ member ) )
| ~ ( A @ complement @ ( B @ member ) ) ) ),
inference(cnf,[status(esa)],[248]) ).
thf(251,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ member ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(cnfConj,[status(thm)],[249]) ).
thf(4875,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk3 @ ( null_class @ sk5 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[4779,251]) ).
thf(4876,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk3 @ ( null_class @ sk5 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[4875]) ).
thf(4877,plain,
~ ( sk3 @ complement @ ( sk3 @ ( null_class @ sk5 ) @ member ) ),
inference(pattern_uni,[status(thm)],[4876:[bind(A,$thf( sk3 )),bind(B,$thf( sk3 @ ( null_class @ sk5 ) ))]]) ).
thf(14,axiom,
! [A: $i] :
( ( A @ inductive )
<=> ( ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
& ( A @ ( null_class @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inductive_defn) ).
thf(112,plain,
! [A: $i] :
( ( ( ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
& ( A @ ( null_class @ member ) ) )
=> ( A @ inductive ) )
& ( ( A @ inductive )
=> ( ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
& ( A @ ( null_class @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(113,plain,
( ! [A: $i] :
( ( ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
& ( A @ ( null_class @ member ) ) )
=> ( A @ inductive ) )
& ! [A: $i] :
( ( A @ inductive )
=> ( ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
& ( A @ ( null_class @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[112]) ).
thf(114,plain,
! [B: $i,A: $i] :
( ( ( B @ inductive )
| ~ ( B @ ( B @ ( successor_relation @ image ) @ subclass ) )
| ~ ( B @ ( null_class @ member ) ) )
& ( ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
| ~ ( A @ inductive ) )
& ( ( A @ ( null_class @ member ) )
| ~ ( A @ inductive ) ) ),
inference(cnf,[status(esa)],[113]) ).
thf(115,plain,
! [A: $i] :
( ( A @ ( null_class @ member ) )
| ~ ( A @ inductive ) ),
inference(cnfConj,[status(thm)],[114]) ).
thf(212,plain,
sk8 @ inductive,
inference(cnfConj,[status(thm)],[210]) ).
thf(7313,plain,
! [A: $i] :
( ( ( sk8 @ inductive )
!= ( A @ inductive ) )
| ( A @ ( null_class @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[212,115]) ).
thf(7314,plain,
! [A: $i] :
( ( ( sk8 @ inductive )
!= ( A @ inductive ) )
| ( A @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[7313]) ).
thf(7315,plain,
sk8 @ ( null_class @ member ),
inference(pattern_uni,[status(thm)],[7314:[bind(A,$thf( sk8 ))]]) ).
thf(7505,plain,
! [B: $i,A: $i] :
( ( ( sk8 @ ( null_class @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[7315,251]) ).
thf(7506,plain,
! [B: $i,A: $i] :
( ( ( sk8 @ ( null_class @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[7505]) ).
thf(7507,plain,
~ ( sk8 @ complement @ ( null_class @ member ) ),
inference(pattern_uni,[status(thm)],[7506:[bind(A,$thf( sk8 )),bind(B,$thf( null_class ))]]) ).
thf(7884,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( sk8 @ complement @ ( null_class @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[115,7507]) ).
thf(7885,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( sk8 @ complement @ ( null_class @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7884]) ).
thf(7886,plain,
~ ( sk8 @ complement @ inductive ),
inference(pattern_uni,[status(thm)],[7885:[bind(A,$thf( sk8 @ complement ))]]) ).
thf(32,axiom,
! [A: $i,B: $i] :
( ( ( B @ function )
& ( universal_class @ ( A @ member ) ) )
=> ( universal_class @ ( A @ ( B @ image ) @ member ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',replacement) ).
thf(217,plain,
! [A: $i,B: $i] :
( ( ( B @ function )
& ( universal_class @ ( A @ member ) ) )
=> ( universal_class @ ( A @ ( B @ image ) @ member ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(25,axiom,
! [A: $i] : ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( A @ rotate @ subclass ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rotate) ).
thf(182,plain,
! [A: $i] : ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( A @ rotate @ subclass ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(183,plain,
! [A: $i] : ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( A @ rotate @ subclass ) ),
inference(cnf,[status(esa)],[182]) ).
thf(50,plain,
~ ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ),
inference(cnfConj,[status(thm)],[47]) ).
thf(306,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( A @ rotate @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[183,50]) ).
thf(307,plain,
! [A: $i] :
( ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( A @ rotate @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) ),
inference(simp,[status(thm)],[306]) ).
thf(308,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) )
!= sk3 )
| ( ( A @ rotate )
!= ( sk2 @ ( sk1 @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[307]) ).
thf(48,plain,
sk3 @ ( sk1 @ member ),
inference(cnfConj,[status(thm)],[47]) ).
thf(102,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subclass ) )
| ~ ( B @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(104,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subclass ) )
| ~ ( B @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(simp,[status(thm)],[102]) ).
thf(294,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[244,50]) ).
thf(295,plain,
! [A: $i] :
( ( universal_class @ ( A @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) ),
inference(simp,[status(thm)],[294]) ).
thf(296,plain,
! [A: $i] :
( ( sk3 != universal_class )
| ( A
!= ( sk2 @ ( sk1 @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[295]) ).
thf(297,plain,
sk3 != universal_class,
inference(simp,[status(thm)],[296]) ).
thf(2769,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( B != universal_class )
| ~ ( A @ ( B @ subclass ) )
| ~ ( B @ ( A @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[96,297]) ).
thf(2770,plain,
! [A: $i] :
( ( A != universal_class )
| ~ ( sk3 @ ( A @ subclass ) )
| ~ ( A @ ( sk3 @ subclass ) ) ),
inference(pattern_uni,[status(thm)],[2769:[bind(A,$thf( sk3 ))]]) ).
thf(3845,plain,
( ~ ( sk3 @ ( universal_class @ subclass ) )
| ~ ( universal_class @ ( sk3 @ subclass ) ) ),
inference(simp,[status(thm)],[2770]) ).
thf(5549,plain,
( ~ ( sk3 @ ( universal_class @ subclass ) )
| ~ $true ),
inference(rewrite,[status(thm)],[3845,244]) ).
thf(5550,plain,
~ ( sk3 @ ( universal_class @ subclass ) ),
inference(simp,[status(thm)],[5549]) ).
thf(5577,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ $true
| ~ ( B @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[104,5550]) ).
thf(5578,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ ( B @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(simp,[status(thm)],[5577]) ).
thf(5579,plain,
~ ( sk3 @ ( universal_class @ ( sk3 @ sk5 ) @ member ) ),
inference(pattern_uni,[status(thm)],[5578:[bind(A,$thf( universal_class )),bind(B,$thf( sk3 ))]]) ).
thf(5821,plain,
( ( ( sk3 @ ( universal_class @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,5579]) ).
thf(5822,plain,
( ( sk3 @ ( universal_class @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[5821]) ).
thf(5864,plain,
( ( sk3 != sk3 )
| ( ( universal_class @ ( sk3 @ sk5 ) )
!= sk1 ) ),
inference(simp,[status(thm)],[5822]) ).
thf(5878,plain,
( ( universal_class @ ( sk3 @ sk5 ) )
!= sk1 ),
inference(simp,[status(thm)],[5864]) ).
thf(13039,plain,
! [A: $i] :
( ( ( sk3 @ ( sk2 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,4089]) ).
thf(13040,plain,
! [A: $i] :
( ( sk3 @ ( sk2 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[13039]) ).
thf(13109,plain,
! [A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk3 )
| ( sk2 != A ) ),
inference(simp,[status(thm)],[13040]) ).
thf(13147,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk3 ),
inference(simp,[status(thm)],[13109]) ).
thf(23810,plain,
( ( null_class @ sum_class @ sum_class @ sum_class )
!= sk3 ),
inference(rewrite,[status(thm)],[13147,21467]) ).
thf(40,axiom,
? [A: $i] :
( ! [B: $i] :
( ( universal_class @ ( B @ member ) )
=> ( ( B @ ( B @ ( A @ apply ) @ member ) )
| ( B = null_class ) ) )
& ( A @ function ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',choice) ).
thf(254,plain,
? [A: $i] :
( ! [B: $i] :
( ( universal_class @ ( B @ member ) )
=> ( ( B @ ( B @ ( A @ apply ) @ member ) )
| ( B = null_class ) ) )
& ( A @ function ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(255,plain,
! [A: $i] :
( ( ( A @ ( A @ ( sk9 @ apply ) @ member ) )
| ( A = null_class )
| ~ ( universal_class @ ( A @ member ) ) )
& ( sk9 @ function ) ),
inference(cnf,[status(esa)],[254]) ).
thf(256,plain,
sk9 @ function,
inference(cnfConj,[status(thm)],[255]) ).
thf(510,plain,
! [A: $i] :
( ( A != sk9 )
| ( null_class @ function )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,256]) ).
thf(511,plain,
( ( null_class @ function )
| ( universal_class @ ( sk9 @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[510:[bind(A,$thf( sk9 ))]]) ).
thf(4738,plain,
! [A: $i] :
( ( ( A @ ( null_class @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4694,50]) ).
thf(4739,plain,
! [A: $i] :
( ( A @ ( null_class @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) ),
inference(simp,[status(thm)],[4738]) ).
thf(4743,plain,
! [A: $i] :
( ( A != sk3 )
| ( ( sk2 @ ( sk1 @ unordered_pair ) )
!= null_class ) ),
inference(simp,[status(thm)],[4739]) ).
thf(4747,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) )
!= null_class ),
inference(simp,[status(thm)],[4743]) ).
thf(15,axiom,
! [A: $i,B: $i] :
( ( B @ power_class @ ( A @ member ) )
<=> ( ( B @ ( A @ subclass ) )
& ( universal_class @ ( A @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',power_class_defn) ).
thf(119,plain,
! [A: $i,B: $i] :
( ( ( ( B @ ( A @ subclass ) )
& ( universal_class @ ( A @ member ) ) )
=> ( B @ power_class @ ( A @ member ) ) )
& ( ( B @ power_class @ ( A @ member ) )
=> ( ( B @ ( A @ subclass ) )
& ( universal_class @ ( A @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(120,plain,
( ! [A: $i,B: $i] :
( ( ( B @ ( A @ subclass ) )
& ( universal_class @ ( A @ member ) ) )
=> ( B @ power_class @ ( A @ member ) ) )
& ! [A: $i,B: $i] :
( ( B @ power_class @ ( A @ member ) )
=> ( ( B @ ( A @ subclass ) )
& ( universal_class @ ( A @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[119]) ).
thf(121,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ power_class @ ( C @ member ) )
| ~ ( D @ ( C @ subclass ) )
| ~ ( universal_class @ ( C @ member ) ) )
& ( ( B @ ( A @ subclass ) )
| ~ ( B @ power_class @ ( A @ member ) ) )
& ( ( universal_class @ ( A @ member ) )
| ~ ( B @ power_class @ ( A @ member ) ) ) ),
inference(cnf,[status(esa)],[120]) ).
thf(123,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subclass ) )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[121]) ).
thf(8844,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ $true
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[123,5550]) ).
thf(8845,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[8844]) ).
thf(8846,plain,
~ ( sk3 @ power_class @ ( universal_class @ member ) ),
inference(pattern_uni,[status(thm)],[8845:[bind(A,$thf( universal_class )),bind(B,$thf( sk3 ))]]) ).
thf(9031,plain,
( ( ( sk3 @ ( sk2 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,8846]) ).
thf(9032,plain,
( ( sk3 @ ( sk2 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) ),
inference(simp,[status(thm)],[9031]) ).
thf(9059,plain,
( ( ( sk3 @ power_class )
!= sk3 )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[9032]) ).
thf(4,axiom,
! [A: $i] :
( ( A @ successor )
= ( A @ singleton @ ( A @ union ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_defn) ).
thf(54,plain,
! [A: $i] :
( ( A @ successor )
= ( A @ singleton @ ( A @ union ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(55,plain,
! [A: $i] :
( ( A @ successor )
= ( A @ singleton @ ( A @ union ) ) ),
inference(cnf,[status(esa)],[54]) ).
thf(56,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ union ) )
= ( A @ successor ) ),
inference(lifteq,[status(thm)],[55]) ).
thf(490,plain,
! [A: $i] :
( ( A != sk8 )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,211]) ).
thf(491,plain,
( ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( sk8 @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[490:[bind(A,$thf( sk8 ))]]) ).
thf(1135,plain,
! [A: $i] :
( ( A
!= ( sk8 @ sk6 ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,491]) ).
thf(1136,plain,
! [A: $i] :
( ( A
!= ( sk8 @ sk6 ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[1135]) ).
thf(1137,plain,
( ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( sk8 @ sk6 @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[1136:[bind(A,$thf( sk8 @ sk6 ))]]) ).
thf(18,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ intersection ) @ ( C @ member ) )
<=> ( ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection) ).
thf(136,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) )
=> ( B @ ( A @ intersection ) @ ( C @ member ) ) )
& ( ( B @ ( A @ intersection ) @ ( C @ member ) )
=> ( ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(137,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) )
=> ( B @ ( A @ intersection ) @ ( C @ member ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ intersection ) @ ( C @ member ) )
=> ( ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[136]) ).
thf(138,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( D @ intersection ) @ ( F @ member ) )
| ~ ( E @ ( F @ member ) )
| ~ ( D @ ( F @ member ) ) )
& ( ( B @ ( C @ member ) )
| ~ ( B @ ( A @ intersection ) @ ( C @ member ) ) )
& ( ( A @ ( C @ member ) )
| ~ ( B @ ( A @ intersection ) @ ( C @ member ) ) ) ),
inference(cnf,[status(esa)],[137]) ).
thf(141,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ intersection ) @ ( C @ member ) )
| ~ ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(cnfConj,[status(thm)],[138]) ).
thf(142,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ intersection ) @ ( C @ member ) )
| ~ ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[141]) ).
thf(20,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ cross_product ) @ ( C @ member ) )
=> ( C
= ( C @ second @ ( C @ first @ ordered_pair ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cross_product) ).
thf(151,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ cross_product ) @ ( C @ member ) )
=> ( C
= ( C @ second @ ( C @ first @ ordered_pair ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(152,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( C @ second @ ( C @ first @ ordered_pair ) ) )
| ~ ( B @ ( A @ cross_product ) @ ( C @ member ) ) ),
inference(cnf,[status(esa)],[151]) ).
thf(153,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ cross_product ) @ ( C @ member ) )
| ( ( C @ second @ ( C @ first @ ordered_pair ) )
= C ) ),
inference(lifteq,[status(thm)],[152]) ).
thf(44,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair_defn) ).
thf(271,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(272,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) ) ),
inference(cnf,[status(esa)],[271]) ).
thf(273,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) ) ),
inference(lifteq,[status(thm)],[272]) ).
thf(18824,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ cross_product ) @ ( C @ member ) )
| ( ( C @ second @ singleton @ ( C @ first @ unordered_pair ) @ ( C @ first @ singleton @ unordered_pair ) )
= C ) ),
inference(rewrite,[status(thm)],[153,273]) ).
thf(10,axiom,
! [A: $i,B: $i] :
( ( A @ domain_of @ ( B @ member ) )
<=> ( ( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) )
!= null_class )
& ( universal_class @ ( B @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain_of) ).
thf(76,plain,
! [A: $i,B: $i] :
( ( ( ( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) )
!= null_class )
& ( universal_class @ ( B @ member ) ) )
=> ( A @ domain_of @ ( B @ member ) ) )
& ( ( A @ domain_of @ ( B @ member ) )
=> ( ( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) )
!= null_class )
& ( universal_class @ ( B @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(77,plain,
( ! [A: $i,B: $i] :
( ( ( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) )
!= null_class )
& ( universal_class @ ( B @ member ) ) )
=> ( A @ domain_of @ ( B @ member ) ) )
& ! [A: $i,B: $i] :
( ( A @ domain_of @ ( B @ member ) )
=> ( ( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) )
!= null_class )
& ( universal_class @ ( B @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[76]) ).
thf(78,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ domain_of @ ( D @ member ) )
| ( ( universal_class @ ( D @ singleton @ ( C @ restrict ) ) )
= null_class )
| ~ ( universal_class @ ( D @ member ) ) )
& ( ( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) )
!= null_class )
| ~ ( A @ domain_of @ ( B @ member ) ) )
& ( ( universal_class @ ( B @ member ) )
| ~ ( A @ domain_of @ ( B @ member ) ) ) ),
inference(cnf,[status(esa)],[77]) ).
thf(80,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) )
!= null_class )
| ~ ( A @ domain_of @ ( B @ member ) ) ),
inference(cnfConj,[status(thm)],[78]) ).
thf(82,plain,
! [B: $i,A: $i] :
( ~ ( A @ domain_of @ ( B @ member ) )
| ( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) )
!= null_class ) ),
inference(lifteq,[status(thm)],[80]) ).
thf(7,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( A @ ( B @ restrict ) ) )
= ( C @ ( A @ cross_product ) @ ( B @ intersection ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',restrict_defn) ).
thf(63,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( A @ ( B @ restrict ) ) )
= ( C @ ( A @ cross_product ) @ ( B @ intersection ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(64,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ restrict ) ) )
= ( C @ ( A @ cross_product ) @ ( B @ intersection ) ) ),
inference(cnf,[status(esa)],[63]) ).
thf(65,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ restrict ) ) )
= ( C @ ( A @ cross_product ) @ ( B @ intersection ) ) ),
inference(lifteq,[status(thm)],[64]) ).
thf(1988,plain,
! [B: $i,A: $i] :
( ~ ( A @ domain_of @ ( B @ member ) )
| ( ( universal_class @ ( B @ singleton @ cross_product ) @ ( A @ intersection ) )
!= null_class ) ),
inference(rewrite,[status(thm)],[82,65]) ).
thf(33,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ flip @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) )
<=> ( ( D @ ( C @ ( A @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
& ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',flip_defn) ).
thf(219,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( ( D @ ( C @ ( A @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
& ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ) )
=> ( D @ flip @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ) )
& ( ( D @ flip @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) )
=> ( ( D @ ( C @ ( A @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
& ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(220,plain,
( ! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( C @ ( A @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
& ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ) )
=> ( D @ flip @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ) )
& ! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ flip @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) )
=> ( ( D @ ( C @ ( A @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
& ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[219]) ).
thf(221,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( H @ flip @ ( G @ ( F @ ( E @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( H @ ( G @ ( E @ ( F @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( G @ ( F @ ( E @ ordered_pair ) @ ordered_pair ) @ member ) ) )
& ( ( D @ ( C @ ( A @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( D @ flip @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ) )
& ( ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( D @ flip @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ) ) ),
inference(cnf,[status(esa)],[220]) ).
thf(222,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( D @ flip @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[221]) ).
thf(47546,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( C @ singleton @ ( B @ ( A @ ordered_pair ) @ unordered_pair ) @ ( B @ ( A @ ordered_pair ) @ singleton @ unordered_pair ) @ member ) )
| ~ ( D @ flip @ ( C @ singleton @ ( B @ ( A @ ordered_pair ) @ unordered_pair ) @ ( B @ ( A @ ordered_pair ) @ singleton @ unordered_pair ) @ member ) ) ),
inference(rewrite,[status(thm)],[222,273]) ).
thf(15951,plain,
! [A: $i] :
( ( A != sk3 )
| ( null_class != null_class )
| ( A @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[149,282]) ).
thf(15952,plain,
! [A: $i] :
( ( A != sk3 )
| ( A @ ( A @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[15951]) ).
thf(15953,plain,
sk3 @ ( sk3 @ sk6 @ member ),
inference(pattern_uni,[status(thm)],[15952:[bind(A,$thf( sk3 ))]]) ).
thf(5126,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) )
| ~ $true
| ~ ( B @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[104,50]) ).
thf(5127,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) )
| ~ ( B @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(simp,[status(thm)],[5126]) ).
thf(5128,plain,
~ ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) ),
inference(pattern_uni,[status(thm)],[5127:[bind(A,$thf( sk2 @ ( sk1 @ unordered_pair ) )),bind(B,$thf( sk3 ))]]) ).
thf(17186,plain,
( ( ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk3 @ sk6 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15953,5128]) ).
thf(17187,plain,
( ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk3 @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[17186]) ).
thf(17233,plain,
( ( sk3 != sk3 )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) )
!= ( sk3 @ sk6 ) ) ),
inference(simp,[status(thm)],[17187]) ).
thf(17258,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) )
!= ( sk3 @ sk6 ) ),
inference(simp,[status(thm)],[17233]) ).
thf(7512,plain,
! [A: $i] :
( ( ( sk8 @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7315,1679]) ).
thf(7513,plain,
! [A: $i] :
( ( sk8 @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[7512]) ).
thf(7548,plain,
! [A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class )
!= sk8 )
| ( null_class != A ) ),
inference(simp,[status(thm)],[7513]) ).
thf(7576,plain,
( ( null_class @ sum_class @ sum_class @ sum_class )
!= sk8 ),
inference(simp,[status(thm)],[7548]) ).
thf(16824,plain,
( ( null_class @ sum_class @ sum_class )
!= sk8 ),
inference(rewrite,[status(thm)],[7576,14939]) ).
thf(18595,plain,
( ( null_class @ sum_class )
!= sk8 ),
inference(rewrite,[status(thm)],[16824,14939]) ).
thf(17113,plain,
( ( ( sk3 @ ( universal_class @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk3 @ sk6 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15953,5579]) ).
thf(17114,plain,
( ( sk3 @ ( universal_class @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk3 @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[17113]) ).
thf(17220,plain,
( ( sk3 != sk3 )
| ( ( universal_class @ ( sk3 @ sk5 ) )
!= ( sk3 @ sk6 ) ) ),
inference(simp,[status(thm)],[17114]) ).
thf(17253,plain,
( ( universal_class @ ( sk3 @ sk5 ) )
!= ( sk3 @ sk6 ) ),
inference(simp,[status(thm)],[17220]) ).
thf(6914,plain,
( ( ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,5128]) ).
thf(6915,plain,
( ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[6914]) ).
thf(6946,plain,
( ( sk3 != sk3 )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[6915]) ).
thf(6971,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) )
!= sk2 ),
inference(simp,[status(thm)],[6946]) ).
thf(8911,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ $true
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[123,5378]) ).
thf(8912,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[8911]) ).
thf(8913,plain,
~ ( null_class @ power_class @ ( universal_class @ member ) ),
inference(pattern_uni,[status(thm)],[8912:[bind(A,$thf( universal_class )),bind(B,$thf( null_class ))]]) ).
thf(15933,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk3 @ ( null_class @ member ) )
| ( A @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[149,48]) ).
thf(15934,plain,
( ( sk3 @ ( null_class @ member ) )
| ( sk1 @ ( sk1 @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[15933:[bind(A,$thf( sk1 ))]]) ).
thf(25980,plain,
! [A: $i] :
( ( ( sk1 @ ( sk1 @ sk6 @ member ) )
!= ( null_class @ ( A @ member ) ) )
| ~ $true
| ( sk3 @ ( null_class @ member ) ) ),
inference(paramod_ordered,[status(thm)],[15934,216]) ).
thf(25981,plain,
! [A: $i] :
( ( ( sk1 @ ( sk1 @ sk6 @ member ) )
!= ( null_class @ ( A @ member ) ) )
| ( sk3 @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[25980]) ).
thf(26154,plain,
! [A: $i] :
( ( sk1 != null_class )
| ( ( sk1 @ sk6 )
!= A )
| ( sk3 @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[25981]) ).
thf(26176,plain,
( ( sk1 != null_class )
| ( sk3 @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[26154]) ).
thf(5484,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( universal_class @ ( null_class @ sk5 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[5406,251]) ).
thf(5485,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( universal_class @ ( null_class @ sk5 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[5484]) ).
thf(5486,plain,
~ ( universal_class @ complement @ ( universal_class @ ( null_class @ sk5 ) @ member ) ),
inference(pattern_uni,[status(thm)],[5485:[bind(A,$thf( universal_class )),bind(B,$thf( universal_class @ ( null_class @ sk5 ) ))]]) ).
thf(7304,plain,
! [B: $i,A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( null_class @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[115,216]) ).
thf(7305,plain,
! [B: $i,A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( null_class @ ( B @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7304]) ).
thf(7306,plain,
~ ( null_class @ inductive ),
inference(pattern_uni,[status(thm)],[7305:[bind(A,$thf( null_class )),bind(B,$thf( null_class ))]]) ).
thf(7419,plain,
( ( ( sk8 @ inductive )
!= ( null_class @ inductive ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[212,7306]) ).
thf(7420,plain,
( ( sk8 @ inductive )
!= ( null_class @ inductive ) ),
inference(simp,[status(thm)],[7419]) ).
thf(7425,plain,
sk8 != null_class,
inference(simp,[status(thm)],[7420]) ).
thf(7430,plain,
! [B: $i,A: $i] :
( ( A != sk8 )
| ( B != null_class )
| ~ ( A @ ( B @ subclass ) )
| ~ ( B @ ( A @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[96,7425]) ).
thf(7431,plain,
! [A: $i] :
( ( A != null_class )
| ~ ( sk8 @ ( A @ subclass ) )
| ~ ( A @ ( sk8 @ subclass ) ) ),
inference(pattern_uni,[status(thm)],[7430:[bind(A,$thf( sk8 ))]]) ).
thf(7434,plain,
( ~ ( sk8 @ ( null_class @ subclass ) )
| ~ ( null_class @ ( sk8 @ subclass ) ) ),
inference(simp,[status(thm)],[7431]) ).
thf(14387,plain,
( ~ $true
| ~ ( null_class @ ( sk8 @ subclass ) ) ),
inference(rewrite,[status(thm)],[7434,4694]) ).
thf(14388,plain,
~ ( null_class @ ( sk8 @ subclass ) ),
inference(simp,[status(thm)],[14387]) ).
thf(14434,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( sk8 @ subclass ) ) )
| ~ $true
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[123,14388]) ).
thf(14435,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( sk8 @ subclass ) ) )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[14434]) ).
thf(14436,plain,
~ ( null_class @ power_class @ ( sk8 @ member ) ),
inference(pattern_uni,[status(thm)],[14435:[bind(A,$thf( sk8 )),bind(B,$thf( null_class ))]]) ).
thf(14985,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( null_class != null_class )
| ( A @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[149,4747]) ).
thf(14986,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( A @ ( A @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[14985]) ).
thf(14987,plain,
sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ),
inference(pattern_uni,[status(thm)],[14986:[bind(A,$thf( sk2 @ ( sk1 @ unordered_pair ) ))]]) ).
thf(4797,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( null_class != null_class )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,4747]) ).
thf(4798,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[4797]) ).
thf(4799,plain,
universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ),
inference(pattern_uni,[status(thm)],[4798:[bind(A,$thf( sk2 @ ( sk1 @ unordered_pair ) ))]]) ).
thf(5016,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[4799,251]) ).
thf(5017,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[5016]) ).
thf(5018,plain,
~ ( universal_class @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ) ),
inference(pattern_uni,[status(thm)],[5017:[bind(A,$thf( universal_class )),bind(B,$thf( sk2 @ ( sk1 @ unordered_pair ) @ sk6 ))]]) ).
thf(24668,plain,
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ) )
!= ( universal_class @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[14987,5018]) ).
thf(24669,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ) )
!= ( universal_class @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[24668]) ).
thf(24708,plain,
( ( ( sk2 @ ( sk1 @ unordered_pair ) )
!= ( universal_class @ complement ) )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 )
!= ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 ) ) ),
inference(simp,[status(thm)],[24669]) ).
thf(24755,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) )
!= ( universal_class @ complement ) ),
inference(simp,[status(thm)],[24708]) ).
thf(16,axiom,
! [A: $i] :
( ( A @ singleton )
= ( A @ ( A @ unordered_pair ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_set_defn) ).
thf(126,plain,
! [A: $i] :
( ( A @ singleton )
= ( A @ ( A @ unordered_pair ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(127,plain,
! [A: $i] :
( ( A @ singleton )
= ( A @ ( A @ unordered_pair ) ) ),
inference(cnf,[status(esa)],[126]) ).
thf(128,plain,
! [A: $i] :
( ( A @ ( A @ unordered_pair ) )
= ( A @ singleton ) ),
inference(lifteq,[status(thm)],[127]) ).
thf(88,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subclass ) )
| ( A != B ) ),
inference(cnfConj,[status(thm)],[87]) ).
thf(91,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subclass ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[88]) ).
thf(92,plain,
! [A: $i] : ( A @ ( A @ subclass ) ),
inference(simp,[status(thm)],[91]) ).
thf(298,plain,
! [A: $i] :
( ( ( A @ ( A @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[92,50]) ).
thf(299,plain,
! [A: $i] :
( ( A @ ( A @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) ),
inference(simp,[status(thm)],[298]) ).
thf(300,plain,
! [A: $i] :
( ( A != sk3 )
| ( A
!= ( sk2 @ ( sk1 @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[299]) ).
thf(301,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) )
!= sk3 ),
inference(simp,[status(thm)],[300]) ).
thf(821,plain,
! [A: $i] :
( ( ( A @ ( A @ unordered_pair ) )
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( ( A @ singleton )
!= sk3 ) ),
inference(paramod_ordered,[status(thm)],[128,301]) ).
thf(831,plain,
! [A: $i] :
( ( A != sk2 )
| ( A != sk1 )
| ( ( A @ singleton )
!= sk3 ) ),
inference(simp,[status(thm)],[821]) ).
thf(841,plain,
( ( sk2 != sk1 )
| ( ( sk1 @ singleton )
!= sk3 ) ),
inference(simp,[status(thm)],[831]) ).
thf(13,axiom,
! [A: $i] :
( ( A @ function )
<=> ( ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
& ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',function_defn) ).
thf(105,plain,
! [A: $i] :
( ( ( ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
& ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) ) )
=> ( A @ function ) )
& ( ( A @ function )
=> ( ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
& ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(106,plain,
( ! [A: $i] :
( ( ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
& ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) ) )
=> ( A @ function ) )
& ! [A: $i] :
( ( A @ function )
=> ( ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
& ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) ) ) ) ),
inference(miniscope,[status(thm)],[105]) ).
thf(107,plain,
! [B: $i,A: $i] :
( ( ( B @ function )
| ~ ( identity_relation @ ( B @ inverse @ ( B @ compose ) @ subclass ) )
| ~ ( universal_class @ ( universal_class @ cross_product ) @ ( B @ subclass ) ) )
& ( ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
| ~ ( A @ function ) )
& ( ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
| ~ ( A @ function ) ) ),
inference(cnf,[status(esa)],[106]) ).
thf(108,plain,
! [A: $i] :
( ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
| ~ ( A @ function ) ),
inference(cnfConj,[status(thm)],[107]) ).
thf(14429,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
!= ( null_class @ ( sk8 @ subclass ) ) )
| ~ $true
| ~ ( A @ function ) ),
inference(paramod_ordered,[status(thm)],[108,14388]) ).
thf(14430,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
!= ( null_class @ ( sk8 @ subclass ) ) )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[14429]) ).
thf(14459,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( A != sk8 )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[14430]) ).
thf(14488,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ~ ( sk8 @ function ) ),
inference(simp,[status(thm)],[14459]) ).
thf(147,plain,
! [A: $i] :
( ( A @ ( A @ sk6 @ disjoint ) )
| ( A = null_class ) ),
inference(cnfConj,[status(thm)],[144]) ).
thf(150,plain,
! [A: $i] :
( ( A @ ( A @ sk6 @ disjoint ) )
| ( A = null_class ) ),
inference(lifteq,[status(thm)],[147]) ).
thf(28,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
<=> ( ( ( A = C )
| ( A = B ) )
& ( universal_class @ ( A @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_defn) ).
thf(196,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ( ( A = C )
| ( A = B ) )
& ( universal_class @ ( A @ member ) ) )
=> ( C @ ( B @ unordered_pair ) @ ( A @ member ) ) )
& ( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
=> ( ( ( A = C )
| ( A = B ) )
& ( universal_class @ ( A @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(197,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ( ( A = C )
| ( A = B ) )
& ( universal_class @ ( A @ member ) ) )
=> ( C @ ( B @ unordered_pair ) @ ( A @ member ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
=> ( ( ( A = C )
| ( A = B ) )
& ( universal_class @ ( A @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[196]) ).
thf(198,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ unordered_pair ) @ ( D @ member ) )
| ( D != F )
| ~ ( universal_class @ ( D @ member ) ) )
& ( ( F @ ( E @ unordered_pair ) @ ( D @ member ) )
| ( D != E )
| ~ ( universal_class @ ( D @ member ) ) )
& ( ( A = C )
| ( A = B )
| ~ ( C @ ( B @ unordered_pair ) @ ( A @ member ) ) )
& ( ( universal_class @ ( A @ member ) )
| ~ ( C @ ( B @ unordered_pair ) @ ( A @ member ) ) ) ),
inference(cnf,[status(esa)],[197]) ).
thf(201,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
| ( A != B )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[198]) ).
thf(204,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
| ~ ( universal_class @ ( A @ member ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[201]) ).
thf(205,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( A @ member ) )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[204]) ).
thf(43003,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk8 @ member ) )
!= ( universal_class @ ( A @ member ) ) )
| ( B @ ( A @ unordered_pair ) @ ( A @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[211,205]) ).
thf(43004,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk8 @ member ) )
!= ( universal_class @ ( A @ member ) ) )
| ( B @ ( A @ unordered_pair ) @ ( A @ member ) ) ),
inference(simp,[status(thm)],[43003]) ).
thf(43005,plain,
! [A: $i] : ( A @ ( sk8 @ unordered_pair ) @ ( sk8 @ member ) ),
inference(pattern_uni,[status(thm)],[43004:[bind(A,$thf( sk8 ))]]) ).
thf(43493,plain,
! [A: $i] : ( A @ ( sk8 @ unordered_pair ) @ ( sk8 @ member ) ),
inference(simp,[status(thm)],[43005]) ).
thf(44553,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ unordered_pair ) )
!= ( B @ ( sk8 @ unordered_pair ) ) )
| ( A @ singleton @ ( sk8 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[128,43493]) ).
thf(44554,plain,
sk8 @ singleton @ ( sk8 @ member ),
inference(pattern_uni,[status(thm)],[44553:[bind(A,$thf( sk8 )),bind(B,$thf( sk8 ))]]) ).
thf(44857,plain,
! [A: $i] :
( ( ( sk8 @ singleton @ ( sk8 @ member ) )
!= ( null_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[44554,216]) ).
thf(44858,plain,
! [A: $i] :
( ( sk8 @ singleton @ ( sk8 @ member ) )
!= ( null_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[44857]) ).
thf(45086,plain,
! [A: $i] :
( ( ( sk8 @ singleton )
!= null_class )
| ( sk8 != A ) ),
inference(simp,[status(thm)],[44858]) ).
thf(45117,plain,
( ( sk8 @ singleton )
!= null_class ),
inference(simp,[status(thm)],[45086]) ).
thf(45454,plain,
! [A: $i] :
( ( A
!= ( sk8 @ singleton ) )
| ( null_class != null_class )
| ( A @ ( A @ sk6 @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[150,45117]) ).
thf(45455,plain,
! [A: $i] :
( ( A
!= ( sk8 @ singleton ) )
| ( A @ ( A @ sk6 @ disjoint ) ) ),
inference(simp,[status(thm)],[45454]) ).
thf(45456,plain,
sk8 @ singleton @ ( sk8 @ singleton @ sk6 @ disjoint ),
inference(pattern_uni,[status(thm)],[45455:[bind(A,$thf( sk8 @ singleton ))]]) ).
thf(13047,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk5 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ $true
| ( B @ ( A @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[103,4089]) ).
thf(13048,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk5 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ( B @ ( A @ subclass ) ) ),
inference(simp,[status(thm)],[13047]) ).
thf(13049,plain,
! [A: $i] : ( A @ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ subclass ) ),
inference(pattern_uni,[status(thm)],[13048:[bind(A,$thf( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )),bind(B,$thf( D )),bind(C,$thf( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( D @ sk5 ) ))]]) ).
thf(13164,plain,
! [A: $i] : ( A @ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ subclass ) ),
inference(simp,[status(thm)],[13049]) ).
thf(30722,plain,
! [A: $i] : ( A @ ( null_class @ sum_class @ sum_class @ sum_class @ subclass ) ),
inference(rewrite,[status(thm)],[13164,21467]) ).
thf(26,axiom,
! [A: $i,B: $i] :
( ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
<=> ( ( ( A @ successor )
= B )
& ( universal_class @ ( B @ member ) )
& ( universal_class @ ( A @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_relation_defn2) ).
thf(184,plain,
! [A: $i,B: $i] :
( ( ( ( ( A @ successor )
= B )
& ( universal_class @ ( B @ member ) )
& ( universal_class @ ( A @ member ) ) )
=> ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) )
& ( ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
=> ( ( ( A @ successor )
= B )
& ( universal_class @ ( B @ member ) )
& ( universal_class @ ( A @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(185,plain,
( ! [A: $i,B: $i] :
( ( ( ( A @ successor )
= B )
& ( universal_class @ ( B @ member ) )
& ( universal_class @ ( A @ member ) ) )
=> ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) )
& ! [A: $i,B: $i] :
( ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
=> ( ( ( A @ successor )
= B )
& ( universal_class @ ( B @ member ) )
& ( universal_class @ ( A @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[184]) ).
thf(186,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( successor_relation @ ( D @ ( C @ ordered_pair ) @ member ) )
| ( ( C @ successor )
!= D )
| ~ ( universal_class @ ( D @ member ) )
| ~ ( universal_class @ ( C @ member ) ) )
& ( ( ( A @ successor )
= B )
| ~ ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) )
& ( ( universal_class @ ( B @ member ) )
| ~ ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) )
& ( ( universal_class @ ( A @ member ) )
| ~ ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) ) ),
inference(cnf,[status(esa)],[185]) ).
thf(190,plain,
! [B: $i,A: $i] :
( ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
| ( ( A @ successor )
!= B )
| ~ ( universal_class @ ( B @ member ) )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[186]) ).
thf(192,plain,
! [B: $i,A: $i] :
( ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
| ~ ( universal_class @ ( B @ member ) )
| ~ ( universal_class @ ( A @ member ) )
| ( ( A @ successor )
!= B ) ),
inference(lifteq,[status(thm)],[190]) ).
thf(193,plain,
! [A: $i] :
( ( successor_relation @ ( A @ successor @ ( A @ ordered_pair ) @ member ) )
| ~ ( universal_class @ ( A @ successor @ member ) )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[192]) ).
thf(31203,plain,
! [A: $i] :
( ( successor_relation @ ( A @ successor @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) @ member ) )
| ~ ( universal_class @ ( A @ successor @ member ) )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(rewrite,[status(thm)],[193,273]) ).
thf(21,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ disjoint ) )
<=> ! [C: $i] :
~ ( ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',disjoint_defn) ).
thf(154,plain,
! [A: $i,B: $i] :
( ( ! [C: $i] :
~ ( ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) )
=> ( B @ ( A @ disjoint ) ) )
& ( ( B @ ( A @ disjoint ) )
=> ! [C: $i] :
~ ( ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(155,plain,
( ! [A: $i,B: $i] :
( ~ ? [C: $i] :
( ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) )
=> ( B @ ( A @ disjoint ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ disjoint ) )
=> ~ ? [C: $i] :
( ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[154]) ).
thf(156,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( D @ disjoint ) )
| ( E @ ( D @ ( E @ sk7 ) @ member ) ) )
& ( ( E @ ( D @ disjoint ) )
| ( D @ ( D @ ( E @ sk7 ) @ member ) ) )
& ( ~ ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ disjoint ) ) ) ),
inference(cnf,[status(esa)],[155]) ).
thf(159,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ disjoint ) )
| ( B @ ( A @ ( B @ sk7 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(161,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ disjoint ) )
| ( B @ ( A @ ( B @ sk7 ) @ member ) ) ),
inference(simp,[status(thm)],[159]) ).
thf(20764,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk7 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ~ $true
| ( B @ ( A @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[161,216]) ).
thf(20765,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk7 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ( B @ ( A @ disjoint ) ) ),
inference(simp,[status(thm)],[20764]) ).
thf(20766,plain,
! [A: $i] : ( null_class @ ( A @ disjoint ) ),
inference(pattern_uni,[status(thm)],[20765:[bind(A,$thf( E )),bind(B,$thf( null_class )),bind(C,$thf( E @ ( null_class @ sk7 ) ))]]) ).
thf(20926,plain,
! [A: $i] : ( null_class @ ( A @ disjoint ) ),
inference(simp,[status(thm)],[20766]) ).
thf(500,plain,
! [A: $i] :
( ( A != sk8 )
| ( null_class @ inductive )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,212]) ).
thf(501,plain,
( ( null_class @ inductive )
| ( universal_class @ ( sk8 @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[500:[bind(A,$thf( sk8 ))]]) ).
thf(7413,plain,
( $false
| ( universal_class @ ( sk8 @ sk6 @ member ) ) ),
inference(rewrite,[status(thm)],[501,7306]) ).
thf(7414,plain,
universal_class @ ( sk8 @ sk6 @ member ),
inference(simp,[status(thm)],[7413]) ).
thf(9027,plain,
( ( ( universal_class @ ( sk8 @ sk6 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7414,8846]) ).
thf(9028,plain,
( ( universal_class @ ( sk8 @ sk6 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) ),
inference(simp,[status(thm)],[9027]) ).
thf(9084,plain,
( ( ( sk3 @ power_class )
!= universal_class )
| ( ( sk8 @ sk6 )
!= universal_class ) ),
inference(simp,[status(thm)],[9028]) ).
thf(7650,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk8 @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[7414,251]) ).
thf(7651,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk8 @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[7650]) ).
thf(7652,plain,
~ ( universal_class @ complement @ ( sk8 @ sk6 @ member ) ),
inference(pattern_uni,[status(thm)],[7651:[bind(A,$thf( universal_class )),bind(B,$thf( sk8 @ sk6 ))]]) ).
thf(124,plain,
! [B: $i,A: $i] :
( ( B @ power_class @ ( A @ member ) )
| ~ ( B @ ( A @ subclass ) )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[121]) ).
thf(125,plain,
! [B: $i,A: $i] :
( ( B @ power_class @ ( A @ member ) )
| ~ ( B @ ( A @ subclass ) )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[124]) ).
thf(4650,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) )
| ~ $true
| ( A @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[103,50]) ).
thf(4651,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) )
| ( A @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(simp,[status(thm)],[4650]) ).
thf(4652,plain,
sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ),
inference(pattern_uni,[status(thm)],[4651:[bind(A,$thf( sk2 @ ( sk1 @ unordered_pair ) )),bind(B,$thf( sk3 ))]]) ).
thf(13045,plain,
! [A: $i] :
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4652,4089]) ).
thf(13046,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[13045]) ).
thf(13095,plain,
! [A: $i] :
( ( ( sk2 @ ( sk1 @ unordered_pair ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class ) )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) )
!= A ) ),
inference(simp,[status(thm)],[13046]) ).
thf(13136,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class ) ),
inference(simp,[status(thm)],[13095]) ).
thf(28448,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) )
!= ( null_class @ sum_class @ sum_class @ sum_class ) ),
inference(rewrite,[status(thm)],[13136,21467]) ).
thf(34,axiom,
! [A: $i,B: $i] :
( ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
<=> ( ( B @ ( A @ member ) )
& ( universal_class @ ( B @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_relation_defn) ).
thf(226,plain,
! [A: $i,B: $i] :
( ( ( ( B @ ( A @ member ) )
& ( universal_class @ ( B @ member ) ) )
=> ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) )
& ( ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
=> ( ( B @ ( A @ member ) )
& ( universal_class @ ( B @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(227,plain,
( ! [A: $i,B: $i] :
( ( ( B @ ( A @ member ) )
& ( universal_class @ ( B @ member ) ) )
=> ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) )
& ! [A: $i,B: $i] :
( ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
=> ( ( B @ ( A @ member ) )
& ( universal_class @ ( B @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[226]) ).
thf(228,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( element_relation @ ( D @ ( C @ ordered_pair ) @ member ) )
| ~ ( D @ ( C @ member ) )
| ~ ( universal_class @ ( D @ member ) ) )
& ( ( B @ ( A @ member ) )
| ~ ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) )
& ( ( universal_class @ ( B @ member ) )
| ~ ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) ) ),
inference(cnf,[status(esa)],[227]) ).
thf(230,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ member ) )
| ~ ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[228]) ).
thf(53905,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ member ) )
| ~ ( element_relation @ ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) @ member ) ) ),
inference(rewrite,[status(thm)],[230,273]) ).
thf(311,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk2 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[49,251]) ).
thf(312,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk2 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[311]) ).
thf(313,plain,
~ ( sk3 @ complement @ ( sk2 @ member ) ),
inference(pattern_uni,[status(thm)],[312:[bind(A,$thf( sk3 )),bind(B,$thf( sk2 ))]]) ).
thf(349,plain,
( ( ( sk3 @ complement @ ( sk2 @ member ) )
!= ( sk3 @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,313]) ).
thf(350,plain,
( ( sk3 @ complement @ ( sk2 @ member ) )
!= ( sk3 @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[349]) ).
thf(355,plain,
( ( ( sk3 @ complement )
!= sk3 )
| ( sk2 != sk2 ) ),
inference(simp,[status(thm)],[350]) ).
thf(357,plain,
( ( sk3 @ complement )
!= sk3 ),
inference(simp,[status(thm)],[355]) ).
thf(157,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ disjoint ) ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(5742,plain,
! [A: $i] :
( ( ( sk9 @ function )
!= ( A @ function ) )
| ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[256,108]) ).
thf(5743,plain,
! [A: $i] :
( ( ( sk9 @ function )
!= ( A @ function ) )
| ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) ) ),
inference(simp,[status(thm)],[5742]) ).
thf(5744,plain,
universal_class @ ( universal_class @ cross_product ) @ ( sk9 @ subclass ),
inference(pattern_uni,[status(thm)],[5743:[bind(A,$thf( sk9 ))]]) ).
thf(5835,plain,
( ( ( sk3 @ ( universal_class @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk3 @ ( null_class @ sk5 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4779,5579]) ).
thf(5836,plain,
( ( sk3 @ ( universal_class @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk3 @ ( null_class @ sk5 ) @ member ) ) ),
inference(simp,[status(thm)],[5835]) ).
thf(5846,plain,
( ( sk3 != sk3 )
| ( ( universal_class @ ( sk3 @ sk5 ) )
!= ( sk3 @ ( null_class @ sk5 ) ) ) ),
inference(simp,[status(thm)],[5836]) ).
thf(5868,plain,
( ( universal_class @ ( sk3 @ sk5 ) )
!= ( sk3 @ ( null_class @ sk5 ) ) ),
inference(simp,[status(thm)],[5846]) ).
thf(11098,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[4652,251]) ).
thf(11099,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[11098]) ).
thf(11100,plain,
~ ( sk2 @ ( sk1 @ unordered_pair ) @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) ),
inference(pattern_uni,[status(thm)],[11099:[bind(A,$thf( sk2 @ ( sk1 @ unordered_pair ) )),bind(B,$thf( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) ))]]) ).
thf(23,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( A @ rotate @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
<=> ( ( A @ ( B @ ( D @ ( C @ ordered_pair ) @ ordered_pair ) @ member ) )
& ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rotate_defn) ).
thf(169,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( ( A @ ( B @ ( D @ ( C @ ordered_pair ) @ ordered_pair ) @ member ) )
& ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) )
=> ( A @ rotate @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) )
& ( ( A @ rotate @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
=> ( ( A @ ( B @ ( D @ ( C @ ordered_pair ) @ ordered_pair ) @ member ) )
& ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(170,plain,
( ! [A: $i,B: $i,C: $i,D: $i] :
( ( ( A @ ( B @ ( D @ ( C @ ordered_pair ) @ ordered_pair ) @ member ) )
& ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) )
=> ( A @ rotate @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) )
& ! [A: $i,B: $i,C: $i,D: $i] :
( ( A @ rotate @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
=> ( ( A @ ( B @ ( D @ ( C @ ordered_pair ) @ ordered_pair ) @ member ) )
& ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[169]) ).
thf(171,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ rotate @ ( H @ ( G @ ( F @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( E @ ( F @ ( H @ ( G @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( H @ ( G @ ( F @ ordered_pair ) @ ordered_pair ) @ member ) ) )
& ( ( A @ ( B @ ( D @ ( C @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( A @ rotate @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) )
& ( ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( A @ rotate @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) ) ),
inference(cnf,[status(esa)],[170]) ).
thf(172,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( A @ rotate @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[171]) ).
thf(23098,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( D @ singleton @ ( C @ ( B @ ordered_pair ) @ unordered_pair ) @ ( C @ ( B @ ordered_pair ) @ singleton @ unordered_pair ) @ member ) )
| ~ ( A @ rotate @ ( D @ singleton @ ( C @ ( B @ ordered_pair ) @ unordered_pair ) @ ( C @ ( B @ ordered_pair ) @ singleton @ unordered_pair ) @ member ) ) ),
inference(rewrite,[status(thm)],[172,273]) ).
thf(5,axiom,
! [A: $i] :
( ( A @ inverse )
= ( universal_class @ ( A @ cross_product ) @ flip @ domain_of ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inverse_defn) ).
thf(57,plain,
! [A: $i] :
( ( A @ inverse )
= ( universal_class @ ( A @ cross_product ) @ flip @ domain_of ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(42,axiom,
! [A: $i] : ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( A @ flip @ subclass ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',flip) ).
thf(260,plain,
! [A: $i] : ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( A @ flip @ subclass ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(261,plain,
! [A: $i] : ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( A @ flip @ subclass ) ),
inference(cnf,[status(esa)],[260]) ).
thf(17,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( A @ ( B @ compose ) @ ( D @ ( C @ ordered_pair ) @ member ) )
<=> ( ( C @ singleton @ ( A @ image ) @ ( B @ image ) @ ( D @ member ) )
& ( universal_class @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compose_defn2) ).
thf(129,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( ( C @ singleton @ ( A @ image ) @ ( B @ image ) @ ( D @ member ) )
& ( universal_class @ ( C @ member ) ) )
=> ( A @ ( B @ compose ) @ ( D @ ( C @ ordered_pair ) @ member ) ) )
& ( ( A @ ( B @ compose ) @ ( D @ ( C @ ordered_pair ) @ member ) )
=> ( ( C @ singleton @ ( A @ image ) @ ( B @ image ) @ ( D @ member ) )
& ( universal_class @ ( C @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(130,plain,
( ! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ singleton @ ( A @ image ) @ ( B @ image ) @ ( D @ member ) )
& ( universal_class @ ( C @ member ) ) )
=> ( A @ ( B @ compose ) @ ( D @ ( C @ ordered_pair ) @ member ) ) )
& ! [A: $i,B: $i,C: $i,D: $i] :
( ( A @ ( B @ compose ) @ ( D @ ( C @ ordered_pair ) @ member ) )
=> ( ( C @ singleton @ ( A @ image ) @ ( B @ image ) @ ( D @ member ) )
& ( universal_class @ ( C @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[129]) ).
thf(131,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( F @ compose ) @ ( H @ ( G @ ordered_pair ) @ member ) )
| ~ ( G @ singleton @ ( E @ image ) @ ( F @ image ) @ ( H @ member ) )
| ~ ( universal_class @ ( G @ member ) ) )
& ( ( C @ singleton @ ( A @ image ) @ ( B @ image ) @ ( D @ member ) )
| ~ ( A @ ( B @ compose ) @ ( D @ ( C @ ordered_pair ) @ member ) ) )
& ( ( universal_class @ ( C @ member ) )
| ~ ( A @ ( B @ compose ) @ ( D @ ( C @ ordered_pair ) @ member ) ) ) ),
inference(cnf,[status(esa)],[130]) ).
thf(133,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ singleton @ ( A @ image ) @ ( B @ image ) @ ( D @ member ) )
| ~ ( A @ ( B @ compose ) @ ( D @ ( C @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[131]) ).
thf(10497,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ singleton @ ( A @ image ) @ ( B @ image ) @ ( D @ member ) )
| ~ ( A @ ( B @ compose ) @ ( D @ singleton @ ( C @ unordered_pair ) @ ( C @ singleton @ unordered_pair ) @ member ) ) ),
inference(rewrite,[status(thm)],[133,273]) ).
thf(134,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( B @ compose ) @ ( D @ ( C @ ordered_pair ) @ member ) )
| ~ ( C @ singleton @ ( A @ image ) @ ( B @ image ) @ ( D @ member ) )
| ~ ( universal_class @ ( C @ member ) ) ),
inference(cnfConj,[status(thm)],[131]) ).
thf(135,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( B @ compose ) @ ( D @ ( C @ ordered_pair ) @ member ) )
| ~ ( C @ singleton @ ( A @ image ) @ ( B @ image ) @ ( D @ member ) )
| ~ ( universal_class @ ( C @ member ) ) ),
inference(simp,[status(thm)],[134]) ).
thf(11441,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( B @ compose ) @ ( D @ singleton @ ( C @ unordered_pair ) @ ( C @ singleton @ unordered_pair ) @ member ) )
| ~ ( C @ singleton @ ( A @ image ) @ ( B @ image ) @ ( D @ member ) )
| ~ ( universal_class @ ( C @ member ) ) ),
inference(rewrite,[status(thm)],[135,273]) ).
thf(132,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( universal_class @ ( C @ member ) )
| ~ ( A @ ( B @ compose ) @ ( D @ ( C @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[131]) ).
thf(9882,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( universal_class @ ( C @ member ) )
| ~ ( A @ ( B @ compose ) @ ( D @ singleton @ ( C @ unordered_pair ) @ ( C @ singleton @ unordered_pair ) @ member ) ) ),
inference(rewrite,[status(thm)],[132,273]) ).
thf(321,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk8 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[211,251]) ).
thf(322,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk8 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[321]) ).
thf(323,plain,
~ ( universal_class @ complement @ ( sk8 @ member ) ),
inference(pattern_uni,[status(thm)],[322:[bind(A,$thf( universal_class )),bind(B,$thf( sk8 ))]]) ).
thf(44583,plain,
! [A: $i] :
( ( ( A @ ( sk8 @ unordered_pair ) @ ( sk8 @ member ) )
!= ( universal_class @ complement @ ( sk8 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43493,323]) ).
thf(44584,plain,
! [A: $i] :
( ( A @ ( sk8 @ unordered_pair ) @ ( sk8 @ member ) )
!= ( universal_class @ complement @ ( sk8 @ member ) ) ),
inference(simp,[status(thm)],[44583]) ).
thf(44710,plain,
! [A: $i] :
( ( ( A @ ( sk8 @ unordered_pair ) )
!= ( universal_class @ complement ) )
| ( sk8 != sk8 ) ),
inference(simp,[status(thm)],[44584]) ).
thf(44789,plain,
! [A: $i] :
( ( A @ ( sk8 @ unordered_pair ) )
!= ( universal_class @ complement ) ),
inference(simp,[status(thm)],[44710]) ).
thf(15711,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk3 @ ( null_class @ member ) )
| ( A @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[149,49]) ).
thf(15712,plain,
( ( sk3 @ ( null_class @ member ) )
| ( sk2 @ ( sk2 @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[15711:[bind(A,$thf( sk2 ))]]) ).
thf(44944,plain,
! [B: $i,A: $i] :
( ( ( sk8 @ singleton @ ( sk8 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[44554,251]) ).
thf(44945,plain,
! [B: $i,A: $i] :
( ( ( sk8 @ singleton @ ( sk8 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[44944]) ).
thf(44946,plain,
~ ( sk8 @ singleton @ complement @ ( sk8 @ member ) ),
inference(pattern_uni,[status(thm)],[44945:[bind(A,$thf( sk8 @ singleton )),bind(B,$thf( sk8 ))]]) ).
thf(291,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[259,50]) ).
thf(292,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) ),
inference(simp,[status(thm)],[291]) ).
thf(293,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= sk3 )
| ( ( sk2 @ ( sk1 @ unordered_pair ) )
!= element_relation ) ),
inference(simp,[status(thm)],[292]) ).
thf(22,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ cross_product ) @ ( B @ ( A @ ordered_pair ) @ member ) )
<=> ( ( D @ ( B @ member ) )
& ( C @ ( A @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cross_product_defn) ).
thf(162,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( ( D @ ( B @ member ) )
& ( C @ ( A @ member ) ) )
=> ( D @ ( C @ cross_product ) @ ( B @ ( A @ ordered_pair ) @ member ) ) )
& ( ( D @ ( C @ cross_product ) @ ( B @ ( A @ ordered_pair ) @ member ) )
=> ( ( D @ ( B @ member ) )
& ( C @ ( A @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(163,plain,
( ! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( B @ member ) )
& ( C @ ( A @ member ) ) )
=> ( D @ ( C @ cross_product ) @ ( B @ ( A @ ordered_pair ) @ member ) ) )
& ! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ cross_product ) @ ( B @ ( A @ ordered_pair ) @ member ) )
=> ( ( D @ ( B @ member ) )
& ( C @ ( A @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[162]) ).
thf(164,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( H @ ( G @ cross_product ) @ ( F @ ( E @ ordered_pair ) @ member ) )
| ~ ( H @ ( F @ member ) )
| ~ ( G @ ( E @ member ) ) )
& ( ( D @ ( B @ member ) )
| ~ ( D @ ( C @ cross_product ) @ ( B @ ( A @ ordered_pair ) @ member ) ) )
& ( ( C @ ( A @ member ) )
| ~ ( D @ ( C @ cross_product ) @ ( B @ ( A @ ordered_pair ) @ member ) ) ) ),
inference(cnf,[status(esa)],[163]) ).
thf(167,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ cross_product ) @ ( B @ ( A @ ordered_pair ) @ member ) )
| ~ ( D @ ( B @ member ) )
| ~ ( C @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[164]) ).
thf(168,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ cross_product ) @ ( B @ ( A @ ordered_pair ) @ member ) )
| ~ ( D @ ( B @ member ) )
| ~ ( C @ ( A @ member ) ) ),
inference(simp,[status(thm)],[167]) ).
thf(22271,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ cross_product ) @ ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) @ member ) )
| ~ ( D @ ( B @ member ) )
| ~ ( C @ ( A @ member ) ) ),
inference(rewrite,[status(thm)],[168,273]) ).
thf(11030,plain,
! [A: $i] :
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4652,2169]) ).
thf(11031,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[11030]) ).
thf(11159,plain,
! [A: $i] :
( ( ( sk2 @ ( sk1 @ unordered_pair ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class ) )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) )
!= A ) ),
inference(simp,[status(thm)],[11031]) ).
thf(11190,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class ) ),
inference(simp,[status(thm)],[11159]) ).
thf(16833,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class ) ),
inference(rewrite,[status(thm)],[11190,14939]) ).
thf(25813,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) )
!= ( null_class @ sum_class ) ),
inference(rewrite,[status(thm)],[16833,21467]) ).
thf(18063,plain,
! [A: $i] :
( ( A != sk3 )
| ( null_class != null_class )
| ( A @ ( A @ sk6 @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[150,282]) ).
thf(18064,plain,
! [A: $i] :
( ( A != sk3 )
| ( A @ ( A @ sk6 @ disjoint ) ) ),
inference(simp,[status(thm)],[18063]) ).
thf(18065,plain,
sk3 @ ( sk3 @ sk6 @ disjoint ),
inference(pattern_uni,[status(thm)],[18064:[bind(A,$thf( sk3 ))]]) ).
thf(116,plain,
! [A: $i] :
( ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
| ~ ( A @ inductive ) ),
inference(cnfConj,[status(thm)],[114]) ).
thf(35,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ union ) @ ( C @ member ) )
<=> ( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',union_defn) ).
thf(233,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) ) )
=> ( B @ ( A @ union ) @ ( C @ member ) ) )
& ( ( B @ ( A @ union ) @ ( C @ member ) )
=> ( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(6,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ image ) )
= ( universal_class @ ( A @ ( B @ restrict ) ) @ range_of ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',image_defn) ).
thf(60,plain,
! [A: $i,B: $i] :
( ( A @ ( B @ image ) )
= ( universal_class @ ( A @ ( B @ restrict ) ) @ range_of ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(13036,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[73,4089]) ).
thf(13037,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[13036]) ).
thf(13038,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(pattern_uni,[status(thm)],[13037:[bind(A,$thf( E )),bind(B,$thf( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )),bind(C,$thf( E @ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sk4 ) ))]]) ).
thf(13163,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(simp,[status(thm)],[13038]) ).
thf(30872,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(rewrite,[status(thm)],[13163,21467]) ).
thf(44951,plain,
! [A: $i] :
( ( ( sk8 @ singleton @ ( sk8 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[44554,30872]) ).
thf(44952,plain,
! [A: $i] :
( ( sk8 @ singleton @ ( sk8 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[44951]) ).
thf(45057,plain,
! [A: $i] :
( ( ( sk8 @ singleton )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class ) )
| ( sk8 != A ) ),
inference(simp,[status(thm)],[44952]) ).
thf(45105,plain,
( ( sk8 @ singleton )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class ) ),
inference(simp,[status(thm)],[45057]) ).
thf(50500,plain,
( ( sk8 @ singleton )
!= ( null_class @ sum_class ) ),
inference(rewrite,[status(thm)],[45105,21467]) ).
thf(533,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk3 @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,49]) ).
thf(534,plain,
( ( sk3 @ ( null_class @ member ) )
| ( universal_class @ ( sk2 @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[533:[bind(A,$thf( sk2 ))]]) ).
thf(189,plain,
! [B: $i,A: $i] :
( ( ( A @ successor )
= B )
| ~ ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[186]) ).
thf(191,plain,
! [B: $i,A: $i] :
( ~ ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
| ( ( A @ successor )
= B ) ),
inference(lifteq,[status(thm)],[189]) ).
thf(29073,plain,
! [B: $i,A: $i] :
( ~ ( successor_relation @ ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) @ member ) )
| ( ( A @ successor )
= B ) ),
inference(rewrite,[status(thm)],[191,273]) ).
thf(15700,plain,
! [A: $i] :
( ( A != sk8 )
| ( null_class != null_class )
| ( A @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[149,7425]) ).
thf(15701,plain,
! [A: $i] :
( ( A != sk8 )
| ( A @ ( A @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[15700]) ).
thf(15702,plain,
sk8 @ ( sk8 @ sk6 @ member ),
inference(pattern_uni,[status(thm)],[15701:[bind(A,$thf( sk8 ))]]) ).
thf(16915,plain,
( ( ( universal_class @ complement @ ( sk8 @ sk6 @ member ) )
!= ( sk8 @ ( sk8 @ sk6 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15702,7652]) ).
thf(16916,plain,
( ( universal_class @ complement @ ( sk8 @ sk6 @ member ) )
!= ( sk8 @ ( sk8 @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[16915]) ).
thf(17030,plain,
( ( ( universal_class @ complement )
!= sk8 )
| ( ( sk8 @ sk6 )
!= ( sk8 @ sk6 ) ) ),
inference(simp,[status(thm)],[16916]) ).
thf(17061,plain,
( ( universal_class @ complement )
!= sk8 ),
inference(simp,[status(thm)],[17030]) ).
thf(24,axiom,
! [A: $i,B: $i] :
( ( ( universal_class @ ( B @ member ) )
& ( universal_class @ ( A @ member ) ) )
=> ( ( ( B @ ( A @ ordered_pair ) @ second )
= B )
& ( ( B @ ( A @ ordered_pair ) @ first )
= A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',first_second) ).
thf(176,plain,
! [A: $i,B: $i] :
( ( ( universal_class @ ( B @ member ) )
& ( universal_class @ ( A @ member ) ) )
=> ( ( ( B @ ( A @ ordered_pair ) @ second )
= B )
& ( ( B @ ( A @ ordered_pair ) @ first )
= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(177,plain,
! [B: $i,A: $i] :
( ( ( ( B @ ( A @ ordered_pair ) @ second )
= B )
| ~ ( universal_class @ ( B @ member ) )
| ~ ( universal_class @ ( A @ member ) ) )
& ( ( ( B @ ( A @ ordered_pair ) @ first )
= A )
| ~ ( universal_class @ ( B @ member ) )
| ~ ( universal_class @ ( A @ member ) ) ) ),
inference(cnf,[status(esa)],[176]) ).
thf(179,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ordered_pair ) @ second )
= B )
| ~ ( universal_class @ ( B @ member ) )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[177]) ).
thf(181,plain,
! [B: $i,A: $i] :
( ~ ( universal_class @ ( B @ member ) )
| ~ ( universal_class @ ( A @ member ) )
| ( ( B @ ( A @ ordered_pair ) @ second )
= B ) ),
inference(lifteq,[status(thm)],[179]) ).
thf(27547,plain,
! [B: $i,A: $i] :
( ~ ( universal_class @ ( B @ member ) )
| ~ ( universal_class @ ( A @ member ) )
| ( ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) @ second )
= B ) ),
inference(rewrite,[status(thm)],[181,273]) ).
thf(158,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ disjoint ) )
| ( A @ ( A @ ( B @ sk7 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[156]) ).
thf(160,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ disjoint ) )
| ( A @ ( A @ ( B @ sk7 ) @ member ) ) ),
inference(simp,[status(thm)],[158]) ).
thf(224,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ flip @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( D @ ( C @ ( A @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[221]) ).
thf(225,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ flip @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( D @ ( C @ ( A @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ) ),
inference(simp,[status(thm)],[224]) ).
thf(50893,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ flip @ ( C @ singleton @ ( B @ ( A @ ordered_pair ) @ unordered_pair ) @ ( B @ ( A @ ordered_pair ) @ singleton @ unordered_pair ) @ member ) )
| ~ ( D @ ( C @ singleton @ ( A @ ( B @ ordered_pair ) @ unordered_pair ) @ ( A @ ( B @ ordered_pair ) @ singleton @ unordered_pair ) @ member ) )
| ~ ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( C @ singleton @ ( B @ ( A @ ordered_pair ) @ unordered_pair ) @ ( B @ ( A @ ordered_pair ) @ singleton @ unordered_pair ) @ member ) ) ),
inference(rewrite,[status(thm)],[225,273]) ).
thf(46644,plain,
( ( ( sk8 @ singleton @ complement @ ( sk8 @ member ) )
!= ( universal_class @ ( sk8 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[211,44946]) ).
thf(46645,plain,
( ( sk8 @ singleton @ complement @ ( sk8 @ member ) )
!= ( universal_class @ ( sk8 @ member ) ) ),
inference(simp,[status(thm)],[46644]) ).
thf(46852,plain,
( ( ( sk8 @ singleton @ complement )
!= universal_class )
| ( sk8 != sk8 ) ),
inference(simp,[status(thm)],[46645]) ).
thf(46879,plain,
( ( sk8 @ singleton @ complement )
!= universal_class ),
inference(simp,[status(thm)],[46852]) ).
thf(29,axiom,
universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_relation_defn1) ).
thf(208,plain,
universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(5570,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[208,5550]) ).
thf(5571,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) ),
inference(simp,[status(thm)],[5570]) ).
thf(5594,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= sk3 )
| ( successor_relation != universal_class ) ),
inference(simp,[status(thm)],[5571]) ).
thf(166,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ member ) )
| ~ ( D @ ( C @ cross_product ) @ ( B @ ( A @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[164]) ).
thf(21596,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ member ) )
| ~ ( D @ ( C @ cross_product ) @ ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) @ member ) ) ),
inference(rewrite,[status(thm)],[166,273]) ).
thf(16820,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(rewrite,[status(thm)],[2169,14939]) ).
thf(27248,plain,
! [A: $i] :
~ ( null_class @ sum_class @ ( A @ member ) ),
inference(rewrite,[status(thm)],[16820,21467]) ).
thf(24641,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[14987,251]) ).
thf(24642,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[24641]) ).
thf(24643,plain,
~ ( sk2 @ ( sk1 @ unordered_pair ) @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ) ),
inference(pattern_uni,[status(thm)],[24642:[bind(A,$thf( sk2 @ ( sk1 @ unordered_pair ) )),bind(B,$thf( sk2 @ ( sk1 @ unordered_pair ) @ sk6 ))]]) ).
thf(581,plain,
! [A: $i] :
( ( null_class != null_class )
| ( A != universal_class )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,287]) ).
thf(582,plain,
! [A: $i] :
( ( A != universal_class )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[581:[]]) ).
thf(609,plain,
universal_class @ ( universal_class @ sk6 @ member ),
inference(simp,[status(thm)],[582]) ).
thf(691,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( universal_class @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[609,251]) ).
thf(692,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( universal_class @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[691]) ).
thf(693,plain,
~ ( universal_class @ complement @ ( universal_class @ sk6 @ member ) ),
inference(pattern_uni,[status(thm)],[692:[bind(A,$thf( universal_class )),bind(B,$thf( universal_class @ sk6 ))]]) ).
thf(17351,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( null_class != null_class )
| ( A @ ( A @ sk6 @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[150,4747]) ).
thf(17352,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( A @ ( A @ sk6 @ disjoint ) ) ),
inference(simp,[status(thm)],[17351]) ).
thf(17353,plain,
sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ disjoint ),
inference(pattern_uni,[status(thm)],[17352:[bind(A,$thf( sk2 @ ( sk1 @ unordered_pair ) ))]]) ).
thf(14425,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ) )
!= ( null_class @ ( sk8 @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[208,14388]) ).
thf(14426,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ) )
!= ( null_class @ ( sk8 @ subclass ) ) ),
inference(simp,[status(thm)],[14425]) ).
thf(14477,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( sk8 != successor_relation ) ),
inference(simp,[status(thm)],[14426]) ).
thf(460,plain,
! [A: $i] :
( ( A
!= ( universal_class @ ( universal_class @ cross_product ) ) )
| ( null_class @ ( successor_relation @ subclass ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,208]) ).
thf(461,plain,
( ( null_class @ ( successor_relation @ subclass ) )
| ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[460:[bind(A,$thf( universal_class @ ( universal_class @ cross_product ) ))]]) ).
thf(16953,plain,
( ( ( sk8 @ ( sk8 @ sk6 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15702,8846]) ).
thf(16954,plain,
( ( sk8 @ ( sk8 @ sk6 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) ),
inference(simp,[status(thm)],[16953]) ).
thf(17032,plain,
( ( ( sk3 @ power_class )
!= sk8 )
| ( ( sk8 @ sk6 )
!= universal_class ) ),
inference(simp,[status(thm)],[16954]) ).
thf(521,plain,
! [A: $i] :
( ( A
!= ( universal_class @ ( universal_class @ cross_product ) ) )
| ( null_class @ ( element_relation @ subclass ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,259]) ).
thf(522,plain,
( ( null_class @ ( element_relation @ subclass ) )
| ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[521:[bind(A,$thf( universal_class @ ( universal_class @ cross_product ) ))]]) ).
thf(27,axiom,
! [A: $i,B: $i] : ( universal_class @ ( B @ ( A @ unordered_pair ) @ member ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair) ).
thf(194,plain,
! [A: $i,B: $i] : ( universal_class @ ( B @ ( A @ unordered_pair ) @ member ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(195,plain,
! [B: $i,A: $i] : ( universal_class @ ( B @ ( A @ unordered_pair ) @ member ) ),
inference(cnf,[status(esa)],[194]) ).
thf(829,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ unordered_pair ) )
!= ( C @ ( B @ unordered_pair ) ) )
| ( universal_class @ ( A @ singleton @ member ) ) ),
inference(paramod_ordered,[status(thm)],[128,195]) ).
thf(830,plain,
! [A: $i] : ( universal_class @ ( A @ singleton @ member ) ),
inference(pattern_uni,[status(thm)],[829:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(7785,plain,
! [A: $i] :
( ( ( sk8 @ inductive )
!= ( A @ inductive ) )
| ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[212,116]) ).
thf(7786,plain,
! [A: $i] :
( ( ( sk8 @ inductive )
!= ( A @ inductive ) )
| ( A @ ( A @ ( successor_relation @ image ) @ subclass ) ) ),
inference(simp,[status(thm)],[7785]) ).
thf(7787,plain,
sk8 @ ( sk8 @ ( successor_relation @ image ) @ subclass ),
inference(pattern_uni,[status(thm)],[7786:[bind(A,$thf( sk8 ))]]) ).
thf(8022,plain,
( ( ( sk8 @ ( sk8 @ ( successor_relation @ image ) @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7787,5550]) ).
thf(8023,plain,
( ( sk8 @ ( sk8 @ ( successor_relation @ image ) @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) ),
inference(simp,[status(thm)],[8022]) ).
thf(8068,plain,
( ( sk8 != sk3 )
| ( ( sk8 @ ( successor_relation @ image ) )
!= universal_class ) ),
inference(simp,[status(thm)],[8023]) ).
thf(8869,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( sk3 @ subclass ) ) )
| ~ $true
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[123,4721]) ).
thf(8870,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( sk3 @ subclass ) ) )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[8869]) ).
thf(8871,plain,
~ ( null_class @ power_class @ ( sk3 @ member ) ),
inference(pattern_uni,[status(thm)],[8870:[bind(A,$thf( sk3 )),bind(B,$thf( null_class ))]]) ).
thf(17133,plain,
( ( ( sk3 @ ( sk3 @ sk6 @ member ) )
!= ( null_class @ power_class @ ( sk3 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15953,8871]) ).
thf(17134,plain,
( ( sk3 @ ( sk3 @ sk6 @ member ) )
!= ( null_class @ power_class @ ( sk3 @ member ) ) ),
inference(simp,[status(thm)],[17133]) ).
thf(17232,plain,
( ( ( null_class @ power_class )
!= sk3 )
| ( ( sk3 @ sk6 )
!= sk3 ) ),
inference(simp,[status(thm)],[17134]) ).
thf(675,plain,
! [A: $i] :
( ( A
!= ( universal_class @ sk6 ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,609]) ).
thf(676,plain,
( ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( universal_class @ sk6 @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[675:[bind(A,$thf( universal_class @ sk6 ))]]) ).
thf(4484,plain,
! [A: $i] :
( ( A
!= ( universal_class @ sk6 @ sk6 ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,676]) ).
thf(4485,plain,
! [A: $i] :
( ( A
!= ( universal_class @ sk6 @ sk6 ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[4484]) ).
thf(4486,plain,
( ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( universal_class @ sk6 @ sk6 @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[4485:[bind(A,$thf( universal_class @ sk6 @ sk6 ))]]) ).
thf(3,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ apply ) )
= ( B @ singleton @ ( A @ image ) @ sum_class ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',apply_defn) ).
thf(51,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ apply ) )
= ( B @ singleton @ ( A @ image ) @ sum_class ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(52,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ apply ) )
= ( B @ singleton @ ( A @ image ) @ sum_class ) ),
inference(cnf,[status(esa)],[51]) ).
thf(53,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ apply ) )
= ( B @ singleton @ ( A @ image ) @ sum_class ) ),
inference(lifteq,[status(thm)],[52]) ).
thf(14564,plain,
( ( ( null_class @ power_class @ ( sk8 @ member ) )
!= ( sk3 @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,14436]) ).
thf(14565,plain,
( ( null_class @ power_class @ ( sk8 @ member ) )
!= ( sk3 @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[14564]) ).
thf(14601,plain,
( ( ( null_class @ power_class )
!= sk3 )
| ( sk8 != sk1 ) ),
inference(simp,[status(thm)],[14565]) ).
thf(9149,plain,
( ( ( null_class @ power_class @ ( sk3 @ member ) )
!= ( sk3 @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,8871]) ).
thf(9150,plain,
( ( null_class @ power_class @ ( sk3 @ member ) )
!= ( sk3 @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[9149]) ).
thf(9186,plain,
( ( ( null_class @ power_class )
!= sk3 )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[9150]) ).
thf(316,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( universal_class @ ( B @ ( A @ unordered_pair ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ~ $true
| ~ ( C @ complement @ ( D @ member ) ) ),
inference(paramod_ordered,[status(thm)],[195,251]) ).
thf(317,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( universal_class @ ( B @ ( A @ unordered_pair ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ~ ( C @ complement @ ( D @ member ) ) ),
inference(simp,[status(thm)],[316]) ).
thf(318,plain,
! [B: $i,A: $i] :
~ ( universal_class @ complement @ ( B @ ( A @ unordered_pair ) @ member ) ),
inference(pattern_uni,[status(thm)],[317:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( universal_class )),bind(D,$thf( F @ ( E @ unordered_pair ) ))]]) ).
thf(339,plain,
! [B: $i,A: $i] :
~ ( universal_class @ complement @ ( B @ ( A @ unordered_pair ) @ member ) ),
inference(simp,[status(thm)],[318]) ).
thf(14423,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ) )
!= ( null_class @ ( sk8 @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[259,14388]) ).
thf(14424,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ) )
!= ( null_class @ ( sk8 @ subclass ) ) ),
inference(simp,[status(thm)],[14423]) ).
thf(14473,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( sk8 != element_relation ) ),
inference(simp,[status(thm)],[14424]) ).
thf(17163,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk3 @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[15953,251]) ).
thf(17164,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk3 @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[17163]) ).
thf(17165,plain,
~ ( sk3 @ complement @ ( sk3 @ sk6 @ member ) ),
inference(pattern_uni,[status(thm)],[17164:[bind(A,$thf( sk3 )),bind(B,$thf( sk3 @ sk6 ))]]) ).
thf(14431,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( sk8 @ subclass ) ) )
| ~ $true
| ( A @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[103,14388]) ).
thf(14432,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( sk8 @ subclass ) ) )
| ( A @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(simp,[status(thm)],[14431]) ).
thf(14433,plain,
sk8 @ ( sk8 @ ( null_class @ sk5 ) @ member ),
inference(pattern_uni,[status(thm)],[14432:[bind(A,$thf( sk8 )),bind(B,$thf( null_class ))]]) ).
thf(14717,plain,
! [B: $i,A: $i] :
( ( ( sk8 @ ( sk8 @ ( null_class @ sk5 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[14433,251]) ).
thf(14718,plain,
! [B: $i,A: $i] :
( ( ( sk8 @ ( sk8 @ ( null_class @ sk5 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[14717]) ).
thf(14719,plain,
~ ( sk8 @ complement @ ( sk8 @ ( null_class @ sk5 ) @ member ) ),
inference(pattern_uni,[status(thm)],[14718:[bind(A,$thf( sk8 )),bind(B,$thf( sk8 @ ( null_class @ sk5 ) ))]]) ).
thf(7330,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( sk3 @ complement @ ( sk2 @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[115,313]) ).
thf(7331,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( sk3 @ complement @ ( sk2 @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7330]) ).
thf(7385,plain,
! [A: $i] :
( ( A
!= ( sk3 @ complement ) )
| ( sk2 != null_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7331]) ).
thf(7404,plain,
( ( sk2 != null_class )
| ~ ( sk3 @ complement @ inductive ) ),
inference(simp,[status(thm)],[7385]) ).
thf(17166,plain,
( ( ( sk3 @ ( sk3 @ sk6 @ member ) )
!= ( sk8 @ complement @ ( null_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15953,7507]) ).
thf(17167,plain,
( ( sk3 @ ( sk3 @ sk6 @ member ) )
!= ( sk8 @ complement @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[17166]) ).
thf(17239,plain,
( ( ( sk8 @ complement )
!= sk3 )
| ( ( sk3 @ sk6 )
!= null_class ) ),
inference(simp,[status(thm)],[17167]) ).
thf(109,plain,
! [A: $i] :
( ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
| ~ ( A @ function ) ),
inference(cnfConj,[status(thm)],[107]) ).
thf(326,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[48,251]) ).
thf(327,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[326]) ).
thf(328,plain,
~ ( sk3 @ complement @ ( sk1 @ member ) ),
inference(pattern_uni,[status(thm)],[327:[bind(A,$thf( sk3 )),bind(B,$thf( sk1 ))]]) ).
thf(7923,plain,
( ( ( sk8 @ complement @ ( null_class @ member ) )
!= ( sk8 @ ( null_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7315,7507]) ).
thf(7924,plain,
( ( sk8 @ complement @ ( null_class @ member ) )
!= ( sk8 @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[7923]) ).
thf(7971,plain,
( ( ( sk8 @ complement )
!= sk8 )
| ( null_class != null_class ) ),
inference(simp,[status(thm)],[7924]) ).
thf(7981,plain,
( ( sk8 @ complement )
!= sk8 ),
inference(simp,[status(thm)],[7971]) ).
thf(5574,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ $true
| ( A @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[103,5550]) ).
thf(5575,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ( A @ ( A @ ( B @ sk5 ) @ member ) ) ),
inference(simp,[status(thm)],[5574]) ).
thf(5576,plain,
universal_class @ ( universal_class @ ( sk3 @ sk5 ) @ member ),
inference(pattern_uni,[status(thm)],[5575:[bind(A,$thf( universal_class )),bind(B,$thf( sk3 ))]]) ).
thf(16981,plain,
! [B: $i,A: $i] :
( ( ( sk8 @ ( sk8 @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[15702,251]) ).
thf(16982,plain,
! [B: $i,A: $i] :
( ( ( sk8 @ ( sk8 @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[16981]) ).
thf(16983,plain,
~ ( sk8 @ complement @ ( sk8 @ sk6 @ member ) ),
inference(pattern_uni,[status(thm)],[16982:[bind(A,$thf( sk8 )),bind(B,$thf( sk8 @ sk6 ))]]) ).
thf(19870,plain,
( ( ( sk8 @ complement @ ( sk8 @ sk6 @ member ) )
!= ( sk3 @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,16983]) ).
thf(19871,plain,
( ( sk8 @ complement @ ( sk8 @ sk6 @ member ) )
!= ( sk3 @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[19870]) ).
thf(19911,plain,
( ( ( sk8 @ complement )
!= sk3 )
| ( ( sk8 @ sk6 )
!= sk2 ) ),
inference(simp,[status(thm)],[19871]) ).
thf(202,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
| ( A != C )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[198]) ).
thf(206,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
| ~ ( universal_class @ ( A @ member ) )
| ( A != C ) ),
inference(lifteq,[status(thm)],[202]) ).
thf(207,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( B @ member ) )
| ~ ( universal_class @ ( B @ member ) ) ),
inference(simp,[status(thm)],[206]) ).
thf(43573,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk8 @ member ) )
!= ( universal_class @ ( B @ member ) ) )
| ( B @ ( A @ unordered_pair ) @ ( B @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[211,207]) ).
thf(43574,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk8 @ member ) )
!= ( universal_class @ ( B @ member ) ) )
| ( B @ ( A @ unordered_pair ) @ ( B @ member ) ) ),
inference(simp,[status(thm)],[43573]) ).
thf(43575,plain,
! [A: $i] : ( sk8 @ ( A @ unordered_pair ) @ ( sk8 @ member ) ),
inference(pattern_uni,[status(thm)],[43574:[bind(A,$thf( A )),bind(B,$thf( sk8 ))]]) ).
thf(555,plain,
! [A: $i] :
( ( A != sk3 )
| ( null_class != null_class )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,282]) ).
thf(556,plain,
! [A: $i] :
( ( A != sk3 )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[555]) ).
thf(557,plain,
universal_class @ ( sk3 @ sk6 @ member ),
inference(pattern_uni,[status(thm)],[556:[bind(A,$thf( sk3 ))]]) ).
thf(621,plain,
! [A: $i] :
( ( A
!= ( sk3 @ sk6 ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,557]) ).
thf(622,plain,
( ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( sk3 @ sk6 @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[621:[bind(A,$thf( sk3 @ sk6 ))]]) ).
thf(827,plain,
! [A: $i] :
( ( ( A @ ( A @ unordered_pair ) )
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ~ ( sk3 @ ( A @ singleton @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[128,50]) ).
thf(833,plain,
! [A: $i] :
( ( A != sk2 )
| ( A != sk1 )
| ~ ( sk3 @ ( A @ singleton @ subclass ) ) ),
inference(simp,[status(thm)],[827]) ).
thf(837,plain,
( ( sk2 != sk1 )
| ~ ( sk3 @ ( sk1 @ singleton @ subclass ) ) ),
inference(simp,[status(thm)],[833]) ).
thf(2368,plain,
! [A: $i] :
( ( A
!= ( sk3 @ sk6 @ sk6 ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,622]) ).
thf(2369,plain,
! [A: $i] :
( ( A
!= ( sk3 @ sk6 @ sk6 ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[2368]) ).
thf(2370,plain,
( ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( sk3 @ sk6 @ sk6 @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[2369:[bind(A,$thf( sk3 @ sk6 @ sk6 ))]]) ).
thf(9001,plain,
( ( ( universal_class @ ( sk8 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[211,8846]) ).
thf(9002,plain,
( ( universal_class @ ( sk8 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) ),
inference(simp,[status(thm)],[9001]) ).
thf(9068,plain,
( ( ( sk3 @ power_class )
!= universal_class )
| ( sk8 != universal_class ) ),
inference(simp,[status(thm)],[9002]) ).
thf(19296,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( sk3 @ complement @ ( sk3 @ sk6 @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[115,17165]) ).
thf(19297,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( sk3 @ complement @ ( sk3 @ sk6 @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[19296]) ).
thf(19438,plain,
! [A: $i] :
( ( A
!= ( sk3 @ complement ) )
| ( ( sk3 @ sk6 )
!= null_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[19297]) ).
thf(19459,plain,
( ( ( sk3 @ sk6 )
!= null_class )
| ~ ( sk3 @ complement @ inductive ) ),
inference(simp,[status(thm)],[19438]) ).
thf(46727,plain,
( ( ( sk8 @ singleton @ complement @ ( sk8 @ member ) )
!= ( sk8 @ singleton @ ( sk8 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[44554,44946]) ).
thf(46728,plain,
( ( sk8 @ singleton @ complement @ ( sk8 @ member ) )
!= ( sk8 @ singleton @ ( sk8 @ member ) ) ),
inference(simp,[status(thm)],[46727]) ).
thf(46854,plain,
( ( ( sk8 @ singleton @ complement )
!= ( sk8 @ singleton ) )
| ( sk8 != sk8 ) ),
inference(simp,[status(thm)],[46728]) ).
thf(46880,plain,
( ( sk8 @ singleton @ complement )
!= ( sk8 @ singleton ) ),
inference(simp,[status(thm)],[46854]) ).
thf(61,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ image ) )
= ( universal_class @ ( A @ ( B @ restrict ) ) @ range_of ) ),
inference(cnf,[status(esa)],[60]) ).
thf(62,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ image ) )
= ( universal_class @ ( A @ ( B @ restrict ) ) @ range_of ) ),
inference(lifteq,[status(thm)],[61]) ).
thf(8,axiom,
! [A: $i] :
( ( A @ range_of )
= ( A @ inverse @ domain_of ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',range_of_defn) ).
thf(66,plain,
! [A: $i] :
( ( A @ range_of )
= ( A @ inverse @ domain_of ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(67,plain,
! [A: $i] :
( ( A @ range_of )
= ( A @ inverse @ domain_of ) ),
inference(cnf,[status(esa)],[66]) ).
thf(68,plain,
! [A: $i] :
( ( A @ range_of )
= ( A @ inverse @ domain_of ) ),
inference(lifteq,[status(thm)],[67]) ).
thf(654,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ image ) )
= ( universal_class @ ( A @ ( B @ restrict ) ) @ inverse @ domain_of ) ),
inference(rewrite,[status(thm)],[62,68]) ).
thf(655,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ image ) )
!= ( D @ singleton @ ( C @ image ) ) )
| ( ( universal_class @ ( A @ ( B @ restrict ) ) @ inverse @ domain_of @ sum_class )
= ( D @ ( C @ apply ) ) ) ),
inference(paramod_ordered,[status(thm)],[654,53]) ).
thf(656,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) @ inverse @ domain_of @ sum_class )
= ( B @ ( A @ apply ) ) ),
inference(pattern_uni,[status(thm)],[655:[bind(A,$thf( E @ singleton )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( E ))]]) ).
thf(670,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) @ inverse @ domain_of @ sum_class )
= ( B @ ( A @ apply ) ) ),
inference(simp,[status(thm)],[656]) ).
thf(1086,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( B @ singleton @ cross_product ) @ ( A @ intersection ) @ inverse @ domain_of @ sum_class )
= ( B @ ( A @ apply ) ) ),
inference(rewrite,[status(thm)],[670,65]) ).
thf(44499,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk8 @ unordered_pair ) @ ( sk8 @ member ) )
!= ( null_class @ ( B @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43493,216]) ).
thf(44500,plain,
! [B: $i,A: $i] :
( ( A @ ( sk8 @ unordered_pair ) @ ( sk8 @ member ) )
!= ( null_class @ ( B @ member ) ) ),
inference(simp,[status(thm)],[44499]) ).
thf(44712,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk8 @ unordered_pair ) )
!= null_class )
| ( sk8 != B ) ),
inference(simp,[status(thm)],[44500]) ).
thf(44790,plain,
! [A: $i] :
( ( A @ ( sk8 @ unordered_pair ) )
!= null_class ),
inference(simp,[status(thm)],[44712]) ).
thf(52425,plain,
! [B: $i,A: $i] :
( ( ( sk8 @ ( A @ unordered_pair ) @ ( sk8 @ member ) )
!= ( null_class @ ( B @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43575,216]) ).
thf(52426,plain,
! [B: $i,A: $i] :
( ( sk8 @ ( A @ unordered_pair ) @ ( sk8 @ member ) )
!= ( null_class @ ( B @ member ) ) ),
inference(simp,[status(thm)],[52425]) ).
thf(52665,plain,
! [B: $i,A: $i] :
( ( ( sk8 @ ( A @ unordered_pair ) )
!= null_class )
| ( sk8 != B ) ),
inference(simp,[status(thm)],[52426]) ).
thf(52747,plain,
! [A: $i] :
( ( sk8 @ ( A @ unordered_pair ) )
!= null_class ),
inference(simp,[status(thm)],[52665]) ).
thf(213,plain,
! [A: $i] :
( ( A @ ( sk8 @ subclass ) )
| ~ ( A @ inductive ) ),
inference(cnfConj,[status(thm)],[210]) ).
thf(45356,plain,
! [A: $i] :
( ( ( A @ ( sk8 @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[213,5550]) ).
thf(45357,plain,
! [A: $i] :
( ( ( A @ ( sk8 @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[45356]) ).
thf(45413,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk8 != universal_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[45357]) ).
thf(45421,plain,
( ( sk8 != universal_class )
| ~ ( sk3 @ inductive ) ),
inference(simp,[status(thm)],[45413]) ).
thf(45941,plain,
( ( ( sk8 @ inductive )
!= ( sk3 @ inductive ) )
| ( sk8 != universal_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[212,45421]) ).
thf(45942,plain,
( ( ( sk8 @ inductive )
!= ( sk3 @ inductive ) )
| ( sk8 != universal_class ) ),
inference(simp,[status(thm)],[45941]) ).
thf(45979,plain,
( ( sk8 != sk3 )
| ( sk8 != universal_class ) ),
inference(simp,[status(thm)],[45942]) ).
thf(9041,plain,
( ( ( sk3 @ ( sk1 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,8846]) ).
thf(9042,plain,
( ( sk3 @ ( sk1 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) ),
inference(simp,[status(thm)],[9041]) ).
thf(9081,plain,
( ( ( sk3 @ power_class )
!= sk3 )
| ( sk1 != universal_class ) ),
inference(simp,[status(thm)],[9042]) ).
thf(18261,plain,
! [A: $i] :
( ( null_class != null_class )
| ( A != universal_class )
| ( A @ ( A @ sk6 @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[150,287]) ).
thf(18262,plain,
! [A: $i] :
( ( A != universal_class )
| ( A @ ( A @ sk6 @ disjoint ) ) ),
inference(pattern_uni,[status(thm)],[18261:[]]) ).
thf(18508,plain,
universal_class @ ( universal_class @ sk6 @ disjoint ),
inference(simp,[status(thm)],[18262]) ).
thf(45449,plain,
! [A: $i] :
( ( A
!= ( sk8 @ singleton ) )
| ( null_class != null_class )
| ( A @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[149,45117]) ).
thf(45450,plain,
! [A: $i] :
( ( A
!= ( sk8 @ singleton ) )
| ( A @ ( A @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[45449]) ).
thf(45451,plain,
sk8 @ singleton @ ( sk8 @ singleton @ sk6 @ member ),
inference(pattern_uni,[status(thm)],[45450:[bind(A,$thf( sk8 @ singleton ))]]) ).
thf(47201,plain,
! [B: $i,A: $i] :
( ( ( sk8 @ singleton @ ( sk8 @ singleton @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[45451,251]) ).
thf(47202,plain,
! [B: $i,A: $i] :
( ( ( sk8 @ singleton @ ( sk8 @ singleton @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[47201]) ).
thf(47203,plain,
~ ( sk8 @ singleton @ complement @ ( sk8 @ singleton @ sk6 @ member ) ),
inference(pattern_uni,[status(thm)],[47202:[bind(A,$thf( sk8 @ singleton )),bind(B,$thf( sk8 @ singleton @ sk6 ))]]) ).
thf(18047,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk3 @ ( null_class @ member ) )
| ( A @ ( A @ sk6 @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[150,48]) ).
thf(18048,plain,
( ( sk3 @ ( null_class @ member ) )
| ( sk1 @ ( sk1 @ sk6 @ disjoint ) ) ),
inference(pattern_uni,[status(thm)],[18047:[bind(A,$thf( sk1 ))]]) ).
thf(14389,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( sk9 @ subclass ) )
!= ( null_class @ ( sk8 @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5744,14388]) ).
thf(14390,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( sk9 @ subclass ) )
!= ( null_class @ ( sk8 @ subclass ) ) ),
inference(simp,[status(thm)],[14389]) ).
thf(14469,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( sk9 != sk8 ) ),
inference(simp,[status(thm)],[14390]) ).
thf(44835,plain,
( ( ( null_class @ power_class @ ( sk8 @ member ) )
!= ( sk8 @ singleton @ ( sk8 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[44554,14436]) ).
thf(44836,plain,
( ( null_class @ power_class @ ( sk8 @ member ) )
!= ( sk8 @ singleton @ ( sk8 @ member ) ) ),
inference(simp,[status(thm)],[44835]) ).
thf(45084,plain,
( ( ( null_class @ power_class )
!= ( sk8 @ singleton ) )
| ( sk8 != sk8 ) ),
inference(simp,[status(thm)],[44836]) ).
thf(45116,plain,
( ( null_class @ power_class )
!= ( sk8 @ singleton ) ),
inference(simp,[status(thm)],[45084]) ).
thf(5929,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( sk9 @ subclass ) )
!= ( null_class @ ( sk3 @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5744,4721]) ).
thf(5930,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( sk9 @ subclass ) )
!= ( null_class @ ( sk3 @ subclass ) ) ),
inference(simp,[status(thm)],[5929]) ).
thf(5962,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( sk9 != sk3 ) ),
inference(simp,[status(thm)],[5930]) ).
thf(825,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ unordered_pair ) )
!= ( C @ ( B @ unordered_pair ) ) )
| ~ ( universal_class @ complement @ ( A @ singleton @ member ) ) ),
inference(paramod_ordered,[status(thm)],[128,339]) ).
thf(826,plain,
! [A: $i] :
~ ( universal_class @ complement @ ( A @ singleton @ member ) ),
inference(pattern_uni,[status(thm)],[825:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(12716,plain,
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4652,11100]) ).
thf(12717,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) ) ),
inference(simp,[status(thm)],[12716]) ).
thf(12774,plain,
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ complement )
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) )
!= ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) ) ) ),
inference(simp,[status(thm)],[12717]) ).
thf(12787,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ complement )
!= ( sk2 @ ( sk1 @ unordered_pair ) ) ),
inference(simp,[status(thm)],[12774]) ).
thf(16843,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(rewrite,[status(thm)],[4089,14939]) ).
thf(28489,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(rewrite,[status(thm)],[16843,21467]) ).
thf(58,plain,
! [A: $i] :
( ( A @ inverse )
= ( universal_class @ ( A @ cross_product ) @ flip @ domain_of ) ),
inference(cnf,[status(esa)],[57]) ).
thf(59,plain,
! [A: $i] :
( ( universal_class @ ( A @ cross_product ) @ flip @ domain_of )
= ( A @ inverse ) ),
inference(lifteq,[status(thm)],[58]) ).
thf(117,plain,
! [A: $i] :
( ( A @ inductive )
| ~ ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
| ~ ( A @ ( null_class @ member ) ) ),
inference(cnfConj,[status(thm)],[114]) ).
thf(118,plain,
! [A: $i] :
( ( A @ inductive )
| ~ ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
| ~ ( A @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[117]) ).
thf(5957,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( sk9 @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5744,5378]) ).
thf(5958,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( sk9 @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) ),
inference(simp,[status(thm)],[5957]) ).
thf(5965,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( sk9 != universal_class ) ),
inference(simp,[status(thm)],[5958]) ).
thf(4021,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,2169]) ).
thf(4022,plain,
! [A: $i] :
( ( sk3 @ ( sk1 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[4021]) ).
thf(4044,plain,
! [A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk3 )
| ( sk1 != A ) ),
inference(simp,[status(thm)],[4022]) ).
thf(4067,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk3 ),
inference(simp,[status(thm)],[4044]) ).
thf(16834,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk3 ),
inference(rewrite,[status(thm)],[4067,14939]) ).
thf(20975,plain,
( ( null_class @ sum_class @ sum_class )
!= sk3 ),
inference(rewrite,[status(thm)],[16834,19211]) ).
thf(231,plain,
! [B: $i,A: $i] :
( ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
| ~ ( B @ ( A @ member ) )
| ~ ( universal_class @ ( B @ member ) ) ),
inference(cnfConj,[status(thm)],[228]) ).
thf(232,plain,
! [B: $i,A: $i] :
( ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
| ~ ( B @ ( A @ member ) )
| ~ ( universal_class @ ( B @ member ) ) ),
inference(simp,[status(thm)],[231]) ).
thf(54721,plain,
! [B: $i,A: $i] :
( ( element_relation @ ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) @ member ) )
| ~ ( B @ ( A @ member ) )
| ~ ( universal_class @ ( B @ member ) ) ),
inference(rewrite,[status(thm)],[232,273]) ).
thf(16951,plain,
( ( ( sk8 @ ( sk8 @ sk6 @ member ) )
!= ( null_class @ power_class @ ( sk3 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15702,8871]) ).
thf(16952,plain,
( ( sk8 @ ( sk8 @ sk6 @ member ) )
!= ( null_class @ power_class @ ( sk3 @ member ) ) ),
inference(simp,[status(thm)],[16951]) ).
thf(17041,plain,
( ( ( null_class @ power_class )
!= sk8 )
| ( ( sk8 @ sk6 )
!= sk3 ) ),
inference(simp,[status(thm)],[16952]) ).
thf(7307,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( sk3 @ ( universal_class @ ( sk3 @ sk5 ) @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[115,5579]) ).
thf(7308,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( sk3 @ ( universal_class @ ( sk3 @ sk5 ) @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7307]) ).
thf(7377,plain,
! [A: $i] :
( ( A != sk3 )
| ( ( universal_class @ ( sk3 @ sk5 ) )
!= null_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7308]) ).
thf(7394,plain,
( ( ( universal_class @ ( sk3 @ sk5 ) )
!= null_class )
| ~ ( sk3 @ inductive ) ),
inference(simp,[status(thm)],[7377]) ).
thf(4773,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ) )
!= ( null_class @ ( sk3 @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[208,4721]) ).
thf(4774,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ) )
!= ( null_class @ ( sk3 @ subclass ) ) ),
inference(simp,[status(thm)],[4773]) ).
thf(4790,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( sk3 != successor_relation ) ),
inference(simp,[status(thm)],[4774]) ).
thf(45,axiom,
! [A: $i] :
( ( universal_class @ ( A @ member ) )
=> ( universal_class @ ( A @ sum_class @ member ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_class) ).
thf(274,plain,
! [A: $i] :
( ( universal_class @ ( A @ member ) )
=> ( universal_class @ ( A @ sum_class @ member ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(15451,plain,
! [A: $i] :
( ( A != sk9 )
| ( null_class @ function )
| ( A @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[149,256]) ).
thf(15452,plain,
( ( null_class @ function )
| ( sk9 @ ( sk9 @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[15451:[bind(A,$thf( sk9 ))]]) ).
thf(19374,plain,
( ( ( sk3 @ complement @ ( sk3 @ sk6 @ member ) )
!= ( sk8 @ ( null_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7315,17165]) ).
thf(19375,plain,
( ( sk3 @ complement @ ( sk3 @ sk6 @ member ) )
!= ( sk8 @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[19374]) ).
thf(19444,plain,
( ( ( sk3 @ complement )
!= sk8 )
| ( ( sk3 @ sk6 )
!= null_class ) ),
inference(simp,[status(thm)],[19375]) ).
thf(14552,plain,
( ( ( null_class @ power_class @ ( sk8 @ member ) )
!= ( sk3 @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,14436]) ).
thf(14553,plain,
( ( null_class @ power_class @ ( sk8 @ member ) )
!= ( sk3 @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[14552]) ).
thf(14595,plain,
( ( ( null_class @ power_class )
!= sk3 )
| ( sk8 != sk2 ) ),
inference(simp,[status(thm)],[14553]) ).
thf(38,axiom,
! [A: $i] :
( ( universal_class @ ( A @ member ) )
=> ( universal_class @ ( A @ power_class @ member ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',power_class) ).
thf(245,plain,
! [A: $i] :
( ( universal_class @ ( A @ member ) )
=> ( universal_class @ ( A @ power_class @ member ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(551,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk3 @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,48]) ).
thf(552,plain,
( ( sk3 @ ( null_class @ member ) )
| ( universal_class @ ( sk1 @ sk6 @ member ) ) ),
inference(pattern_uni,[status(thm)],[551:[bind(A,$thf( sk1 ))]]) ).
thf(13041,plain,
! [A: $i] :
( ( ( sk8 @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7315,4089]) ).
thf(13042,plain,
! [A: $i] :
( ( sk8 @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[13041]) ).
thf(13105,plain,
! [A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk8 )
| ( null_class != A ) ),
inference(simp,[status(thm)],[13042]) ).
thf(13144,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk8 ),
inference(simp,[status(thm)],[13105]) ).
thf(23728,plain,
( ( null_class @ sum_class @ sum_class @ sum_class )
!= sk8 ),
inference(rewrite,[status(thm)],[13144,21467]) ).
thf(140,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ~ ( B @ ( A @ intersection ) @ ( C @ member ) ) ),
inference(cnfConj,[status(thm)],[138]) ).
thf(19882,plain,
( ( ( sk8 @ complement @ ( sk8 @ sk6 @ member ) )
!= ( sk3 @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,16983]) ).
thf(19883,plain,
( ( sk8 @ complement @ ( sk8 @ sk6 @ member ) )
!= ( sk3 @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[19882]) ).
thf(19917,plain,
( ( ( sk8 @ complement )
!= sk3 )
| ( ( sk8 @ sk6 )
!= sk1 ) ),
inference(simp,[status(thm)],[19883]) ).
thf(7344,plain,
! [B: $i,A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[115,1679]) ).
thf(7345,plain,
! [B: $i,A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7344]) ).
thf(7346,plain,
~ ( null_class @ sum_class @ sum_class @ sum_class @ inductive ),
inference(pattern_uni,[status(thm)],[7345:[bind(A,$thf( null_class @ sum_class @ sum_class @ sum_class )),bind(B,$thf( null_class ))]]) ).
thf(16825,plain,
~ ( null_class @ sum_class @ sum_class @ inductive ),
inference(rewrite,[status(thm)],[7346,14939]) ).
thf(18631,plain,
~ ( null_class @ sum_class @ inductive ),
inference(rewrite,[status(thm)],[16825,14939]) ).
thf(7477,plain,
( ( ( sk3 @ ( universal_class @ ( sk3 @ sk5 ) @ member ) )
!= ( sk8 @ ( null_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7315,5579]) ).
thf(7478,plain,
( ( sk3 @ ( universal_class @ ( sk3 @ sk5 ) @ member ) )
!= ( sk8 @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[7477]) ).
thf(7561,plain,
( ( sk8 != sk3 )
| ( ( universal_class @ ( sk3 @ sk5 ) )
!= null_class ) ),
inference(simp,[status(thm)],[7478]) ).
thf(816,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ image ) )
= ( universal_class @ ( A @ cross_product ) @ ( B @ intersection ) @ inverse @ domain_of ) ),
inference(rewrite,[status(thm)],[654,65]) ).
thf(9043,plain,
( ( ( universal_class @ ( sk3 @ sk6 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[557,8846]) ).
thf(9044,plain,
( ( universal_class @ ( sk3 @ sk6 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) ),
inference(simp,[status(thm)],[9043]) ).
thf(9079,plain,
( ( ( sk3 @ power_class )
!= universal_class )
| ( ( sk3 @ sk6 )
!= universal_class ) ),
inference(simp,[status(thm)],[9044]) ).
thf(9139,plain,
( ( ( null_class @ power_class @ ( sk3 @ member ) )
!= ( sk3 @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,8871]) ).
thf(9140,plain,
( ( null_class @ power_class @ ( sk3 @ member ) )
!= ( sk3 @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[9139]) ).
thf(9174,plain,
( ( ( null_class @ power_class )
!= sk3 )
| ( sk3 != sk2 ) ),
inference(simp,[status(thm)],[9140]) ).
thf(17678,plain,
! [A: $i] :
( ( A != sk9 )
| ( null_class @ function )
| ( A @ ( A @ sk6 @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[150,256]) ).
thf(17679,plain,
( ( null_class @ function )
| ( sk9 @ ( sk9 @ sk6 @ disjoint ) ) ),
inference(pattern_uni,[status(thm)],[17678:[bind(A,$thf( sk9 ))]]) ).
thf(17095,plain,
( ( ( sk3 @ ( sk3 @ sk6 @ member ) )
!= ( null_class @ power_class @ ( sk8 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15953,14436]) ).
thf(17096,plain,
( ( sk3 @ ( sk3 @ sk6 @ member ) )
!= ( null_class @ power_class @ ( sk8 @ member ) ) ),
inference(simp,[status(thm)],[17095]) ).
thf(17223,plain,
( ( ( null_class @ power_class )
!= sk3 )
| ( ( sk3 @ sk6 )
!= sk8 ) ),
inference(simp,[status(thm)],[17096]) ).
thf(9256,plain,
( ( ( sk3 @ ( sk1 @ member ) )
!= ( null_class @ power_class @ ( universal_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,8913]) ).
thf(9257,plain,
( ( sk3 @ ( sk1 @ member ) )
!= ( null_class @ power_class @ ( universal_class @ member ) ) ),
inference(simp,[status(thm)],[9256]) ).
thf(9294,plain,
( ( ( null_class @ power_class )
!= sk3 )
| ( sk1 != universal_class ) ),
inference(simp,[status(thm)],[9257]) ).
thf(165,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( A @ member ) )
| ~ ( D @ ( C @ cross_product ) @ ( B @ ( A @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[164]) ).
thf(21183,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( A @ member ) )
| ~ ( D @ ( C @ cross_product ) @ ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) @ member ) ) ),
inference(rewrite,[status(thm)],[165,273]) ).
thf(45444,plain,
! [A: $i] :
( ( A
!= ( sk8 @ singleton ) )
| ( null_class != null_class )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[148,45117]) ).
thf(45445,plain,
! [A: $i] :
( ( A
!= ( sk8 @ singleton ) )
| ( universal_class @ ( A @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[45444]) ).
thf(45446,plain,
universal_class @ ( sk8 @ singleton @ sk6 @ member ),
inference(pattern_uni,[status(thm)],[45445:[bind(A,$thf( sk8 @ singleton ))]]) ).
thf(45728,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk8 @ singleton @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[45446,251]) ).
thf(45729,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk8 @ singleton @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[45728]) ).
thf(45730,plain,
~ ( universal_class @ complement @ ( sk8 @ singleton @ sk6 @ member ) ),
inference(pattern_uni,[status(thm)],[45729:[bind(A,$thf( universal_class )),bind(B,$thf( sk8 @ singleton @ sk6 ))]]) ).
thf(199,plain,
! [C: $i,B: $i,A: $i] :
( ( universal_class @ ( A @ member ) )
| ~ ( C @ ( B @ unordered_pair ) @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[198]) ).
thf(32123,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( C @ ( B @ unordered_pair ) @ ( A @ member ) ) )
| ( universal_class @ ( A @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4652,199]) ).
thf(32124,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( C @ ( B @ unordered_pair ) @ ( A @ member ) ) )
| ( universal_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[32123]) ).
thf(32125,plain,
universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ),
inference(pattern_uni,[status(thm)],[32124:[bind(A,$thf( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 ))]]) ).
thf(44215,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[32125,251]) ).
thf(44216,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[44215]) ).
thf(44217,plain,
~ ( universal_class @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) ),
inference(pattern_uni,[status(thm)],[44216:[bind(A,$thf( universal_class )),bind(B,$thf( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) ))]]) ).
thf(16913,plain,
( ( ( sk8 @ ( sk8 @ sk6 @ member ) )
!= ( null_class @ power_class @ ( sk8 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15702,14436]) ).
thf(16914,plain,
( ( sk8 @ ( sk8 @ sk6 @ member ) )
!= ( null_class @ power_class @ ( sk8 @ member ) ) ),
inference(simp,[status(thm)],[16913]) ).
thf(17051,plain,
( ( ( null_class @ power_class )
!= sk8 )
| ( ( sk8 @ sk6 )
!= sk8 ) ),
inference(simp,[status(thm)],[16914]) ).
thf(36,axiom,
! [A: $i,B: $i] : ( universal_class @ ( universal_class @ cross_product ) @ ( A @ ( B @ compose ) @ subclass ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',compose_defn1) ).
thf(241,plain,
! [A: $i,B: $i] : ( universal_class @ ( universal_class @ cross_product ) @ ( A @ ( B @ compose ) @ subclass ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(21861,plain,
! [A: $i] :
( ( ( sk2 @ ( sk2 @ sk6 @ member ) )
!= ( null_class @ ( A @ member ) ) )
| ~ $true
| ( sk3 @ ( null_class @ member ) ) ),
inference(paramod_ordered,[status(thm)],[15712,216]) ).
thf(21862,plain,
! [A: $i] :
( ( ( sk2 @ ( sk2 @ sk6 @ member ) )
!= ( null_class @ ( A @ member ) ) )
| ( sk3 @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[21861]) ).
thf(21977,plain,
! [A: $i] :
( ( sk2 != null_class )
| ( ( sk2 @ sk6 )
!= A )
| ( sk3 @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[21862]) ).
thf(22026,plain,
( ( sk2 != null_class )
| ( sk3 @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[21977]) ).
thf(638,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk3 @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[557,251]) ).
thf(639,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk3 @ sk6 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[638]) ).
thf(640,plain,
~ ( universal_class @ complement @ ( sk3 @ sk6 @ member ) ),
inference(pattern_uni,[status(thm)],[639:[bind(A,$thf( universal_class )),bind(B,$thf( sk3 @ sk6 ))]]) ).
thf(17170,plain,
( ( ( universal_class @ complement @ ( sk3 @ sk6 @ member ) )
!= ( sk3 @ ( sk3 @ sk6 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15953,640]) ).
thf(17171,plain,
( ( universal_class @ complement @ ( sk3 @ sk6 @ member ) )
!= ( sk3 @ ( sk3 @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[17170]) ).
thf(17216,plain,
( ( ( universal_class @ complement )
!= sk3 )
| ( ( sk3 @ sk6 )
!= ( sk3 @ sk6 ) ) ),
inference(simp,[status(thm)],[17171]) ).
thf(17251,plain,
( ( universal_class @ complement )
!= sk3 ),
inference(simp,[status(thm)],[17216]) ).
thf(9037,plain,
( ( ( universal_class @ ( universal_class @ sk6 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[609,8846]) ).
thf(9038,plain,
( ( universal_class @ ( universal_class @ sk6 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) ),
inference(simp,[status(thm)],[9037]) ).
thf(9069,plain,
( ( ( sk3 @ power_class )
!= universal_class )
| ( ( universal_class @ sk6 )
!= universal_class ) ),
inference(simp,[status(thm)],[9038]) ).
thf(6936,plain,
( ( ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk3 @ ( null_class @ sk5 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4779,5128]) ).
thf(6937,plain,
( ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk3 @ ( null_class @ sk5 ) @ member ) ) ),
inference(simp,[status(thm)],[6936]) ).
thf(6949,plain,
( ( sk3 != sk3 )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) )
!= ( sk3 @ ( null_class @ sk5 ) ) ) ),
inference(simp,[status(thm)],[6937]) ).
thf(6973,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) )
!= ( sk3 @ ( null_class @ sk5 ) ) ),
inference(simp,[status(thm)],[6949]) ).
thf(7491,plain,
( ( ( sk3 @ complement @ ( sk1 @ member ) )
!= ( sk8 @ ( null_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7315,328]) ).
thf(7492,plain,
( ( sk3 @ complement @ ( sk1 @ member ) )
!= ( sk8 @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[7491]) ).
thf(7539,plain,
( ( ( sk3 @ complement )
!= sk8 )
| ( sk1 != null_class ) ),
inference(simp,[status(thm)],[7492]) ).
thf(52517,plain,
! [A: $i] :
( ( ( sk8 @ ( A @ unordered_pair ) @ ( sk8 @ member ) )
!= ( universal_class @ complement @ ( sk8 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43575,323]) ).
thf(52518,plain,
! [A: $i] :
( ( sk8 @ ( A @ unordered_pair ) @ ( sk8 @ member ) )
!= ( universal_class @ complement @ ( sk8 @ member ) ) ),
inference(simp,[status(thm)],[52517]) ).
thf(52661,plain,
! [A: $i] :
( ( ( sk8 @ ( A @ unordered_pair ) )
!= ( universal_class @ complement ) )
| ( sk8 != sk8 ) ),
inference(simp,[status(thm)],[52518]) ).
thf(52744,plain,
! [A: $i] :
( ( sk8 @ ( A @ unordered_pair ) )
!= ( universal_class @ complement ) ),
inference(simp,[status(thm)],[52661]) ).
thf(7931,plain,
( ( ( sk3 @ ( sk1 @ member ) )
!= ( sk8 @ complement @ ( null_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,7507]) ).
thf(7932,plain,
( ( sk3 @ ( sk1 @ member ) )
!= ( sk8 @ complement @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[7931]) ).
thf(7956,plain,
( ( ( sk8 @ complement )
!= sk3 )
| ( sk1 != null_class ) ),
inference(simp,[status(thm)],[7932]) ).
thf(14504,plain,
( ( ( null_class @ power_class @ ( sk8 @ member ) )
!= ( universal_class @ ( sk8 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[211,14436]) ).
thf(14505,plain,
( ( null_class @ power_class @ ( sk8 @ member ) )
!= ( universal_class @ ( sk8 @ member ) ) ),
inference(simp,[status(thm)],[14504]) ).
thf(14585,plain,
( ( ( null_class @ power_class )
!= universal_class )
| ( sk8 != sk8 ) ),
inference(simp,[status(thm)],[14505]) ).
thf(14624,plain,
( ( null_class @ power_class )
!= universal_class ),
inference(simp,[status(thm)],[14585]) ).
thf(19844,plain,
( ( ( sk8 @ complement @ ( sk8 @ sk6 @ member ) )
!= ( universal_class @ ( sk8 @ sk6 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7414,16983]) ).
thf(19845,plain,
( ( sk8 @ complement @ ( sk8 @ sk6 @ member ) )
!= ( universal_class @ ( sk8 @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[19844]) ).
thf(19924,plain,
( ( ( sk8 @ complement )
!= universal_class )
| ( ( sk8 @ sk6 )
!= ( sk8 @ sk6 ) ) ),
inference(simp,[status(thm)],[19845]) ).
thf(19954,plain,
( ( sk8 @ complement )
!= universal_class ),
inference(simp,[status(thm)],[19924]) ).
thf(16907,plain,
( ( ( sk8 @ ( sk8 @ sk6 @ member ) )
!= ( null_class @ power_class @ ( universal_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15702,8913]) ).
thf(16908,plain,
( ( sk8 @ ( sk8 @ sk6 @ member ) )
!= ( null_class @ power_class @ ( universal_class @ member ) ) ),
inference(simp,[status(thm)],[16907]) ).
thf(17055,plain,
( ( ( null_class @ power_class )
!= sk8 )
| ( ( sk8 @ sk6 )
!= universal_class ) ),
inference(simp,[status(thm)],[16908]) ).
thf(8902,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) )
| ~ $true
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[123,50]) ).
thf(8903,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[8902]) ).
thf(8904,plain,
~ ( sk3 @ power_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ member ) ),
inference(pattern_uni,[status(thm)],[8903:[bind(A,$thf( sk2 @ ( sk1 @ unordered_pair ) )),bind(B,$thf( sk3 ))]]) ).
thf(17089,plain,
( ( ( sk3 @ ( sk3 @ sk6 @ member ) )
!= ( null_class @ power_class @ ( universal_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15953,8913]) ).
thf(17090,plain,
( ( sk3 @ ( sk3 @ sk6 @ member ) )
!= ( null_class @ power_class @ ( universal_class @ member ) ) ),
inference(simp,[status(thm)],[17089]) ).
thf(17217,plain,
( ( ( null_class @ power_class )
!= sk3 )
| ( ( sk3 @ sk6 )
!= universal_class ) ),
inference(simp,[status(thm)],[17090]) ).
thf(5722,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
!= ( null_class @ ( sk3 @ subclass ) ) )
| ~ $true
| ~ ( A @ function ) ),
inference(paramod_ordered,[status(thm)],[108,4721]) ).
thf(5723,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
!= ( null_class @ ( sk3 @ subclass ) ) )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[5722]) ).
thf(5754,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( A != sk3 )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[5723]) ).
thf(5767,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ~ ( sk3 @ function ) ),
inference(simp,[status(thm)],[5754]) ).
thf(5400,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[208,5378]) ).
thf(5401,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) ),
inference(simp,[status(thm)],[5400]) ).
thf(5418,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( successor_relation != universal_class ) ),
inference(simp,[status(thm)],[5401]) ).
thf(1822,plain,
! [A: $i] :
( ( ( universal_class @ ( sk3 @ sk6 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[557,1679]) ).
thf(1823,plain,
! [A: $i] :
( ( universal_class @ ( sk3 @ sk6 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[1822]) ).
thf(1835,plain,
! [A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class )
!= universal_class )
| ( ( sk3 @ sk6 )
!= A ) ),
inference(simp,[status(thm)],[1823]) ).
thf(1859,plain,
( ( null_class @ sum_class @ sum_class @ sum_class )
!= universal_class ),
inference(simp,[status(thm)],[1835]) ).
thf(16850,plain,
( ( null_class @ sum_class @ sum_class )
!= universal_class ),
inference(rewrite,[status(thm)],[1859,14939]) ).
thf(18669,plain,
( ( null_class @ sum_class )
!= universal_class ),
inference(rewrite,[status(thm)],[16850,14939]) ).
thf(17875,plain,
! [A: $i] :
( ( A != sk8 )
| ( null_class != null_class )
| ( A @ ( A @ sk6 @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[150,7425]) ).
thf(17876,plain,
! [A: $i] :
( ( A != sk8 )
| ( A @ ( A @ sk6 @ disjoint ) ) ),
inference(simp,[status(thm)],[17875]) ).
thf(17877,plain,
sk8 @ ( sk8 @ sk6 @ disjoint ),
inference(pattern_uni,[status(thm)],[17876:[bind(A,$thf( sk8 ))]]) ).
thf(16973,plain,
( ( ( sk8 @ ( sk8 @ sk6 @ member ) )
!= ( sk3 @ complement @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15702,313]) ).
thf(16974,plain,
( ( sk8 @ ( sk8 @ sk6 @ member ) )
!= ( sk3 @ complement @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[16973]) ).
thf(17045,plain,
( ( ( sk3 @ complement )
!= sk8 )
| ( ( sk8 @ sk6 )
!= sk2 ) ),
inference(simp,[status(thm)],[16974]) ).
thf(360,plain,
( ( ( universal_class @ complement @ ( sk8 @ member ) )
!= ( universal_class @ ( sk8 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[211,323]) ).
thf(361,plain,
( ( universal_class @ complement @ ( sk8 @ member ) )
!= ( universal_class @ ( sk8 @ member ) ) ),
inference(simp,[status(thm)],[360]) ).
thf(367,plain,
( ( ( universal_class @ complement )
!= universal_class )
| ( sk8 != sk8 ) ),
inference(simp,[status(thm)],[361]) ).
thf(370,plain,
( ( universal_class @ complement )
!= universal_class ),
inference(simp,[status(thm)],[367]) ).
thf(6186,plain,
! [A: $i] :
( ( ( sk9 @ function )
!= ( A @ function ) )
| ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[256,109]) ).
thf(6187,plain,
! [A: $i] :
( ( ( sk9 @ function )
!= ( A @ function ) )
| ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) ) ),
inference(simp,[status(thm)],[6186]) ).
thf(6188,plain,
identity_relation @ ( sk9 @ inverse @ ( sk9 @ compose ) @ subclass ),
inference(pattern_uni,[status(thm)],[6187:[bind(A,$thf( sk9 ))]]) ).
thf(4736,plain,
! [A: $i] :
( ( ( A @ ( null_class @ subclass ) )
!= ( sk3 @ ( sk1 @ singleton @ subclass ) ) )
| ( sk2 != sk1 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4694,837]) ).
thf(4737,plain,
! [A: $i] :
( ( ( A @ ( null_class @ subclass ) )
!= ( sk3 @ ( sk1 @ singleton @ subclass ) ) )
| ( sk2 != sk1 ) ),
inference(simp,[status(thm)],[4736]) ).
thf(4744,plain,
! [A: $i] :
( ( A != sk3 )
| ( ( sk1 @ singleton )
!= null_class )
| ( sk2 != sk1 ) ),
inference(simp,[status(thm)],[4737]) ).
thf(4748,plain,
( ( ( sk1 @ singleton )
!= null_class )
| ( sk2 != sk1 ) ),
inference(simp,[status(thm)],[4744]) ).
thf(7340,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( universal_class @ complement @ ( sk3 @ sk6 @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[115,640]) ).
thf(7341,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( universal_class @ complement @ ( sk3 @ sk6 @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7340]) ).
thf(7374,plain,
! [A: $i] :
( ( A
!= ( universal_class @ complement ) )
| ( ( sk3 @ sk6 )
!= null_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7341]) ).
thf(7391,plain,
( ( ( sk3 @ sk6 )
!= null_class )
| ~ ( universal_class @ complement @ inductive ) ),
inference(simp,[status(thm)],[7374]) ).
thf(72,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk4 ) @ ( A @ member ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[71]) ).
thf(44938,plain,
( ( ( universal_class @ complement @ ( sk8 @ member ) )
!= ( sk8 @ singleton @ ( sk8 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[44554,323]) ).
thf(44939,plain,
( ( universal_class @ complement @ ( sk8 @ member ) )
!= ( sk8 @ singleton @ ( sk8 @ member ) ) ),
inference(simp,[status(thm)],[44938]) ).
thf(45060,plain,
( ( ( universal_class @ complement )
!= ( sk8 @ singleton ) )
| ( sk8 != sk8 ) ),
inference(simp,[status(thm)],[44939]) ).
thf(45106,plain,
( ( universal_class @ complement )
!= ( sk8 @ singleton ) ),
inference(simp,[status(thm)],[45060]) ).
thf(17135,plain,
( ( ( sk3 @ ( sk3 @ sk6 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15953,8846]) ).
thf(17136,plain,
( ( sk3 @ ( sk3 @ sk6 @ member ) )
!= ( sk3 @ power_class @ ( universal_class @ member ) ) ),
inference(simp,[status(thm)],[17135]) ).
thf(17215,plain,
( ( ( sk3 @ power_class )
!= sk3 )
| ( ( sk3 @ sk6 )
!= universal_class ) ),
inference(simp,[status(thm)],[17136]) ).
thf(16949,plain,
( ( ( sk8 @ ( sk8 @ sk6 @ member ) )
!= ( sk3 @ complement @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15702,328]) ).
thf(16950,plain,
( ( sk8 @ ( sk8 @ sk6 @ member ) )
!= ( sk3 @ complement @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[16949]) ).
thf(17025,plain,
( ( ( sk3 @ complement )
!= sk8 )
| ( ( sk8 @ sk6 )
!= sk1 ) ),
inference(simp,[status(thm)],[16950]) ).
thf(5720,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ $true
| ~ ( A @ function ) ),
inference(paramod_ordered,[status(thm)],[108,5550]) ).
thf(5721,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[5720]) ).
thf(5758,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= sk3 )
| ( A != universal_class )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[5721]) ).
thf(5771,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= sk3 )
| ~ ( universal_class @ function ) ),
inference(simp,[status(thm)],[5758]) ).
thf(5813,plain,
( ( ( sk3 @ ( universal_class @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,5579]) ).
thf(5814,plain,
( ( sk3 @ ( universal_class @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[5813]) ).
thf(5853,plain,
( ( sk3 != sk3 )
| ( ( universal_class @ ( sk3 @ sk5 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[5814]) ).
thf(5873,plain,
( ( universal_class @ ( sk3 @ sk5 ) )
!= sk2 ),
inference(simp,[status(thm)],[5853]) ).
thf(5651,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( universal_class @ ( sk3 @ sk5 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[5576,251]) ).
thf(5652,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( universal_class @ ( sk3 @ sk5 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[5651]) ).
thf(5653,plain,
~ ( universal_class @ complement @ ( universal_class @ ( sk3 @ sk5 ) @ member ) ),
inference(pattern_uni,[status(thm)],[5652:[bind(A,$thf( universal_class )),bind(B,$thf( universal_class @ ( sk3 @ sk5 ) ))]]) ).
thf(200,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ( A = B )
| ~ ( C @ ( B @ unordered_pair ) @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[198]) ).
thf(203,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
| ( A = C )
| ( A = B ) ),
inference(lifteq,[status(thm)],[200]) ).
thf(218,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( A @ ( B @ image ) @ member ) )
| ~ ( B @ function )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(cnf,[status(esa)],[217]) ).
thf(81,plain,
! [B: $i,A: $i] :
( ( A @ domain_of @ ( B @ member ) )
| ( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) )
= null_class )
| ~ ( universal_class @ ( B @ member ) ) ),
inference(cnfConj,[status(thm)],[78]) ).
thf(83,plain,
! [B: $i,A: $i] :
( ( A @ domain_of @ ( B @ member ) )
| ~ ( universal_class @ ( B @ member ) )
| ( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) )
= null_class ) ),
inference(lifteq,[status(thm)],[81]) ).
thf(84,plain,
! [B: $i,A: $i] :
( ( A @ domain_of @ ( B @ member ) )
| ~ ( universal_class @ ( B @ member ) )
| ( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) )
= null_class ) ),
inference(simp,[status(thm)],[83]) ).
thf(2226,plain,
! [B: $i,A: $i] :
( ( A @ domain_of @ ( B @ member ) )
| ~ ( universal_class @ ( B @ member ) )
| ( ( universal_class @ ( B @ singleton @ cross_product ) @ ( A @ intersection ) )
= null_class ) ),
inference(rewrite,[status(thm)],[84,65]) ).
thf(6922,plain,
( ( ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,5128]) ).
thf(6923,plain,
( ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) @ member ) )
!= ( sk3 @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[6922]) ).
thf(6945,plain,
( ( sk3 != sk3 )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) )
!= sk1 ) ),
inference(simp,[status(thm)],[6923]) ).
thf(6970,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk3 @ sk5 ) )
!= sk1 ),
inference(simp,[status(thm)],[6945]) ).
thf(7499,plain,
( ( ( sk3 @ complement @ ( sk2 @ member ) )
!= ( sk8 @ ( null_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7315,313]) ).
thf(7500,plain,
( ( sk3 @ complement @ ( sk2 @ member ) )
!= ( sk8 @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[7499]) ).
thf(7547,plain,
( ( ( sk3 @ complement )
!= sk8 )
| ( sk2 != null_class ) ),
inference(simp,[status(thm)],[7500]) ).
thf(52403,plain,
! [A: $i] :
( ( ( sk8 @ ( A @ unordered_pair ) @ ( sk8 @ member ) )
!= ( null_class @ power_class @ ( sk8 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43575,14436]) ).
thf(52404,plain,
! [A: $i] :
( ( sk8 @ ( A @ unordered_pair ) @ ( sk8 @ member ) )
!= ( null_class @ power_class @ ( sk8 @ member ) ) ),
inference(simp,[status(thm)],[52403]) ).
thf(52671,plain,
! [A: $i] :
( ( ( sk8 @ ( A @ unordered_pair ) )
!= ( null_class @ power_class ) )
| ( sk8 != sk8 ) ),
inference(simp,[status(thm)],[52404]) ).
thf(52752,plain,
! [A: $i] :
( ( sk8 @ ( A @ unordered_pair ) )
!= ( null_class @ power_class ) ),
inference(simp,[status(thm)],[52671]) ).
thf(139,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ member ) )
| ~ ( B @ ( A @ intersection ) @ ( C @ member ) ) ),
inference(cnfConj,[status(thm)],[138]) ).
thf(7301,plain,
! [B: $i,A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[115,2169]) ).
thf(7302,plain,
! [B: $i,A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7301]) ).
thf(7303,plain,
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ inductive ),
inference(pattern_uni,[status(thm)],[7302:[bind(A,$thf( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )),bind(B,$thf( null_class ))]]) ).
thf(16840,plain,
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ inductive ),
inference(rewrite,[status(thm)],[7303,14939]) ).
thf(21032,plain,
~ ( null_class @ sum_class @ sum_class @ inductive ),
inference(rewrite,[status(thm)],[16840,19211]) ).
thf(3975,plain,
! [A: $i] :
( ( ( universal_class @ ( sk8 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[211,2169]) ).
thf(3976,plain,
! [A: $i] :
( ( universal_class @ ( sk8 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[3975]) ).
thf(4036,plain,
! [A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= universal_class )
| ( sk8 != A ) ),
inference(simp,[status(thm)],[3976]) ).
thf(4062,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= universal_class ),
inference(simp,[status(thm)],[4036]) ).
thf(16816,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= universal_class ),
inference(rewrite,[status(thm)],[4062,14939]) ).
thf(20663,plain,
( ( null_class @ sum_class @ sum_class )
!= universal_class ),
inference(rewrite,[status(thm)],[16816,19211]) ).
thf(7921,plain,
( ( ( sk3 @ ( sk2 @ member ) )
!= ( sk8 @ complement @ ( null_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,7507]) ).
thf(7922,plain,
( ( sk3 @ ( sk2 @ member ) )
!= ( sk8 @ complement @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[7921]) ).
thf(7959,plain,
( ( ( sk8 @ complement )
!= sk3 )
| ( sk2 != null_class ) ),
inference(simp,[status(thm)],[7922]) ).
thf(187,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( A @ member ) )
| ~ ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[186]) ).
thf(28100,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( A @ member ) )
| ~ ( successor_relation @ ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) @ member ) ) ),
inference(rewrite,[status(thm)],[187,273]) ).
thf(174,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ rotate @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( A @ ( B @ ( D @ ( C @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[171]) ).
thf(175,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ rotate @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( A @ ( B @ ( D @ ( C @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) ),
inference(simp,[status(thm)],[174]) ).
thf(24868,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ rotate @ ( D @ singleton @ ( C @ ( B @ ordered_pair ) @ unordered_pair ) @ ( C @ ( B @ ordered_pair ) @ singleton @ unordered_pair ) @ member ) )
| ~ ( A @ ( B @ singleton @ ( D @ ( C @ ordered_pair ) @ unordered_pair ) @ ( D @ ( C @ ordered_pair ) @ singleton @ unordered_pair ) @ member ) )
| ~ ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( D @ singleton @ ( C @ ( B @ ordered_pair ) @ unordered_pair ) @ ( C @ ( B @ ordered_pair ) @ singleton @ unordered_pair ) @ member ) ) ),
inference(rewrite,[status(thm)],[175,273]) ).
thf(20262,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk7 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ~ $true
| ( B @ ( A @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[160,216]) ).
thf(20263,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk7 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ( B @ ( A @ disjoint ) ) ),
inference(simp,[status(thm)],[20262]) ).
thf(20264,plain,
! [A: $i] : ( A @ ( null_class @ disjoint ) ),
inference(pattern_uni,[status(thm)],[20263:[bind(A,$thf( null_class )),bind(B,$thf( D )),bind(C,$thf( null_class @ ( D @ sk7 ) ))]]) ).
thf(20425,plain,
! [A: $i] : ( A @ ( null_class @ disjoint ) ),
inference(simp,[status(thm)],[20264]) ).
thf(17884,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk3 @ ( null_class @ member ) )
| ( A @ ( A @ sk6 @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[150,49]) ).
thf(17885,plain,
( ( sk3 @ ( null_class @ member ) )
| ( sk2 @ ( sk2 @ sk6 @ disjoint ) ) ),
inference(pattern_uni,[status(thm)],[17884:[bind(A,$thf( sk2 ))]]) ).
thf(229,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( B @ member ) )
| ~ ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[228]) ).
thf(53304,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( B @ member ) )
| ~ ( element_relation @ ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) @ member ) ) ),
inference(rewrite,[status(thm)],[229,273]) ).
thf(7309,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( universal_class @ complement @ ( universal_class @ sk6 @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[115,693]) ).
thf(7310,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( universal_class @ complement @ ( universal_class @ sk6 @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7309]) ).
thf(7387,plain,
! [A: $i] :
( ( A
!= ( universal_class @ complement ) )
| ( ( universal_class @ sk6 )
!= null_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7310]) ).
thf(7406,plain,
( ( ( universal_class @ sk6 )
!= null_class )
| ~ ( universal_class @ complement @ inductive ) ),
inference(simp,[status(thm)],[7387]) ).
thf(74,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ sum_class @ ( A @ member ) )
| ~ ( B @ ( C @ member ) )
| ~ ( C @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[71]) ).
thf(75,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ sum_class @ ( A @ member ) )
| ~ ( B @ ( C @ member ) )
| ~ ( C @ ( A @ member ) ) ),
inference(simp,[status(thm)],[74]) ).
thf(5927,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( sk9 @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5744,5550]) ).
thf(5928,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( sk9 @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) ),
inference(simp,[status(thm)],[5927]) ).
thf(5963,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= sk3 )
| ( sk9 != universal_class ) ),
inference(simp,[status(thm)],[5928]) ).
thf(288,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[208,50]) ).
thf(289,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ) )
!= ( sk3 @ ( sk2 @ ( sk1 @ unordered_pair ) @ subclass ) ) ),
inference(simp,[status(thm)],[288]) ).
thf(290,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= sk3 )
| ( ( sk2 @ ( sk1 @ unordered_pair ) )
!= successor_relation ) ),
inference(simp,[status(thm)],[289]) ).
thf(7473,plain,
! [A: $i] :
( ( ( sk8 @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7315,2169]) ).
thf(7474,plain,
! [A: $i] :
( ( sk8 @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[7473]) ).
thf(7545,plain,
! [A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk8 )
| ( null_class != A ) ),
inference(simp,[status(thm)],[7474]) ).
thf(7574,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk8 ),
inference(simp,[status(thm)],[7545]) ).
thf(16846,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk8 ),
inference(rewrite,[status(thm)],[7574,14939]) ).
thf(21408,plain,
( ( null_class @ sum_class @ sum_class )
!= sk8 ),
inference(rewrite,[status(thm)],[16846,19211]) ).
thf(4771,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ) )
!= ( null_class @ ( sk3 @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[259,4721]) ).
thf(4772,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ) )
!= ( null_class @ ( sk3 @ subclass ) ) ),
inference(simp,[status(thm)],[4771]) ).
thf(4787,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( sk3 != element_relation ) ),
inference(simp,[status(thm)],[4772]) ).
thf(43,axiom,
! [A: $i] :
( ( identity_relation @ ( A @ member ) )
<=> ? [B: $i] :
( ( A
= ( B @ ( B @ ordered_pair ) ) )
& ( universal_class @ ( B @ member ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_relation) ).
thf(262,plain,
! [A: $i] :
( ( ? [B: $i] :
( ( A
= ( B @ ( B @ ordered_pair ) ) )
& ( universal_class @ ( B @ member ) ) )
=> ( identity_relation @ ( A @ member ) ) )
& ( ( identity_relation @ ( A @ member ) )
=> ? [B: $i] :
( ( A
= ( B @ ( B @ ordered_pair ) ) )
& ( universal_class @ ( B @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(79,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( B @ member ) )
| ~ ( A @ domain_of @ ( B @ member ) ) ),
inference(cnfConj,[status(thm)],[78]) ).
thf(7781,plain,
! [A: $i] :
( ( ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[116,5550]) ).
thf(7782,plain,
! [A: $i] :
( ( ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7781]) ).
thf(7820,plain,
! [A: $i] :
( ( A != sk3 )
| ( ( A @ ( successor_relation @ image ) )
!= universal_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7782]) ).
thf(7829,plain,
( ( ( sk3 @ ( successor_relation @ image ) )
!= universal_class )
| ~ ( sk3 @ inductive ) ),
inference(simp,[status(thm)],[7820]) ).
thf(21133,plain,
( ( ( sk8 @ inductive )
!= ( sk3 @ inductive ) )
| ( ( sk3 @ ( successor_relation @ image ) )
!= universal_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[212,7829]) ).
thf(21134,plain,
( ( ( sk8 @ inductive )
!= ( sk3 @ inductive ) )
| ( ( sk3 @ ( successor_relation @ image ) )
!= universal_class ) ),
inference(simp,[status(thm)],[21133]) ).
thf(21177,plain,
( ( sk8 != sk3 )
| ( ( sk3 @ ( successor_relation @ image ) )
!= universal_class ) ),
inference(simp,[status(thm)],[21134]) ).
thf(8050,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ image ) )
!= ( sk8 @ ( successor_relation @ image ) ) )
| ( sk8 @ ( universal_class @ ( A @ cross_product ) @ ( B @ intersection ) @ inverse @ domain_of @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[816,7787]) ).
thf(8051,plain,
sk8 @ ( universal_class @ ( sk8 @ cross_product ) @ ( successor_relation @ intersection ) @ inverse @ domain_of @ subclass ),
inference(pattern_uni,[status(thm)],[8050:[bind(A,$thf( sk8 )),bind(B,$thf( successor_relation ))]]) ).
thf(188,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( B @ member ) )
| ~ ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[186]) ).
thf(28814,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( B @ member ) )
| ~ ( successor_relation @ ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) @ member ) ) ),
inference(rewrite,[status(thm)],[188,273]) ).
thf(9246,plain,
( ( ( sk3 @ ( sk2 @ member ) )
!= ( null_class @ power_class @ ( universal_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,8913]) ).
thf(9247,plain,
( ( sk3 @ ( sk2 @ member ) )
!= ( null_class @ power_class @ ( universal_class @ member ) ) ),
inference(simp,[status(thm)],[9246]) ).
thf(9293,plain,
( ( ( null_class @ power_class )
!= sk3 )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[9247]) ).
thf(27113,plain,
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ) )
!= ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4799,24643]) ).
thf(27114,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ) )
!= ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[27113]) ).
thf(27152,plain,
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ complement )
!= universal_class )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 )
!= ( sk2 @ ( sk1 @ unordered_pair ) @ sk6 ) ) ),
inference(simp,[status(thm)],[27114]) ).
thf(27180,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ complement )
!= universal_class ),
inference(simp,[status(thm)],[27152]) ).
thf(173,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( D @ ( C @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( A @ rotate @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[171]) ).
thf(23895,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( B @ singleton @ ( D @ ( C @ ordered_pair ) @ unordered_pair ) @ ( D @ ( C @ ordered_pair ) @ singleton @ unordered_pair ) @ member ) )
| ~ ( A @ rotate @ ( D @ singleton @ ( C @ ( B @ ordered_pair ) @ unordered_pair ) @ ( C @ ( B @ ordered_pair ) @ singleton @ unordered_pair ) @ member ) ) ),
inference(rewrite,[status(thm)],[173,273]) ).
thf(242,plain,
! [B: $i,A: $i] : ( universal_class @ ( universal_class @ cross_product ) @ ( A @ ( B @ compose ) @ subclass ) ),
inference(cnf,[status(esa)],[241]) ).
thf(8574,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( universal_class @ complement @ ( sk8 @ sk6 @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[115,7652]) ).
thf(8575,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( universal_class @ complement @ ( sk8 @ sk6 @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[8574]) ).
thf(8660,plain,
! [A: $i] :
( ( A
!= ( universal_class @ complement ) )
| ( ( sk8 @ sk6 )
!= null_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[8575]) ).
thf(8675,plain,
( ( ( sk8 @ sk6 )
!= null_class )
| ~ ( universal_class @ complement @ inductive ) ),
inference(simp,[status(thm)],[8660]) ).
thf(4605,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk5 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ $true
| ( B @ ( A @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[103,2169]) ).
thf(4606,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk5 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ( B @ ( A @ subclass ) ) ),
inference(simp,[status(thm)],[4605]) ).
thf(4607,plain,
! [A: $i] : ( A @ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ subclass ) ),
inference(pattern_uni,[status(thm)],[4606:[bind(A,$thf( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )),bind(B,$thf( D )),bind(C,$thf( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( D @ sk5 ) ))]]) ).
thf(4719,plain,
! [A: $i] : ( A @ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ subclass ) ),
inference(simp,[status(thm)],[4607]) ).
thf(16849,plain,
! [A: $i] : ( A @ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ subclass ) ),
inference(rewrite,[status(thm)],[4719,14939]) ).
thf(28353,plain,
! [A: $i] : ( A @ ( null_class @ sum_class @ subclass ) ),
inference(rewrite,[status(thm)],[16849,21467]) ).
thf(223,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( A @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) )
| ~ ( D @ flip @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[221]) ).
thf(49488,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ singleton @ ( A @ ( B @ ordered_pair ) @ unordered_pair ) @ ( A @ ( B @ ordered_pair ) @ singleton @ unordered_pair ) @ member ) )
| ~ ( D @ flip @ ( C @ singleton @ ( B @ ( A @ ordered_pair ) @ unordered_pair ) @ ( B @ ( A @ ordered_pair ) @ singleton @ unordered_pair ) @ member ) ) ),
inference(rewrite,[status(thm)],[223,273]) ).
thf(7320,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( sk3 @ complement @ ( sk1 @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[115,328]) ).
thf(7321,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( sk3 @ complement @ ( sk1 @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7320]) ).
thf(7375,plain,
! [A: $i] :
( ( A
!= ( sk3 @ complement ) )
| ( sk1 != null_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[7321]) ).
thf(7392,plain,
( ( sk1 != null_class )
| ~ ( sk3 @ complement @ inductive ) ),
inference(simp,[status(thm)],[7375]) ).
thf(19386,plain,
( ( ( sk3 @ complement @ ( sk3 @ sk6 @ member ) )
!= ( universal_class @ ( sk3 @ sk6 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[557,17165]) ).
thf(19387,plain,
( ( sk3 @ complement @ ( sk3 @ sk6 @ member ) )
!= ( universal_class @ ( sk3 @ sk6 @ member ) ) ),
inference(simp,[status(thm)],[19386]) ).
thf(19414,plain,
( ( ( sk3 @ complement )
!= universal_class )
| ( ( sk3 @ sk6 )
!= ( sk3 @ sk6 ) ) ),
inference(simp,[status(thm)],[19387]) ).
thf(19452,plain,
( ( sk3 @ complement )
!= universal_class ),
inference(simp,[status(thm)],[19414]) ).
thf(5749,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ $true
| ~ ( A @ function ) ),
inference(paramod_ordered,[status(thm)],[108,5378]) ).
thf(5750,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[5749]) ).
thf(5755,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( A != universal_class )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[5750]) ).
thf(5768,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ~ ( universal_class @ function ) ),
inference(simp,[status(thm)],[5755]) ).
thf(110,plain,
! [A: $i] :
( ( A @ function )
| ~ ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
| ~ ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) ) ),
inference(cnfConj,[status(thm)],[107]) ).
thf(111,plain,
! [A: $i] :
( ( A @ function )
| ~ ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
| ~ ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) ) ),
inference(simp,[status(thm)],[110]) ).
thf(5568,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[259,5550]) ).
thf(5569,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ) )
!= ( sk3 @ ( universal_class @ subclass ) ) ),
inference(simp,[status(thm)],[5568]) ).
thf(5591,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= sk3 )
| ( element_relation != universal_class ) ),
inference(simp,[status(thm)],[5569]) ).
thf(122,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( A @ member ) )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[121]) ).
thf(1820,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,1679]) ).
thf(1821,plain,
! [A: $i] :
( ( sk3 @ ( sk1 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[1820]) ).
thf(1842,plain,
! [A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class )
!= sk3 )
| ( sk1 != A ) ),
inference(simp,[status(thm)],[1821]) ).
thf(1863,plain,
( ( null_class @ sum_class @ sum_class @ sum_class )
!= sk3 ),
inference(simp,[status(thm)],[1842]) ).
thf(16823,plain,
( ( null_class @ sum_class @ sum_class )
!= sk3 ),
inference(rewrite,[status(thm)],[1863,14939]) ).
thf(18559,plain,
( ( null_class @ sum_class )
!= sk3 ),
inference(rewrite,[status(thm)],[16823,14939]) ).
thf(44477,plain,
! [A: $i] :
( ( ( A @ ( sk8 @ unordered_pair ) @ ( sk8 @ member ) )
!= ( null_class @ power_class @ ( sk8 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[43493,14436]) ).
thf(44478,plain,
! [A: $i] :
( ( A @ ( sk8 @ unordered_pair ) @ ( sk8 @ member ) )
!= ( null_class @ power_class @ ( sk8 @ member ) ) ),
inference(simp,[status(thm)],[44477]) ).
thf(44704,plain,
! [A: $i] :
( ( ( A @ ( sk8 @ unordered_pair ) )
!= ( null_class @ power_class ) )
| ( sk8 != sk8 ) ),
inference(simp,[status(thm)],[44478]) ).
thf(44787,plain,
! [A: $i] :
( ( A @ ( sk8 @ unordered_pair ) )
!= ( null_class @ power_class ) ),
inference(simp,[status(thm)],[44704]) ).
thf(178,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ordered_pair ) @ first )
= A )
| ~ ( universal_class @ ( B @ member ) )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[177]) ).
thf(180,plain,
! [B: $i,A: $i] :
( ~ ( universal_class @ ( B @ member ) )
| ~ ( universal_class @ ( A @ member ) )
| ( ( B @ ( A @ ordered_pair ) @ first )
= A ) ),
inference(lifteq,[status(thm)],[178]) ).
thf(26430,plain,
! [B: $i,A: $i] :
( ~ ( universal_class @ ( B @ member ) )
| ~ ( universal_class @ ( A @ member ) )
| ( ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) @ first )
= A ) ),
inference(rewrite,[status(thm)],[180,273]) ).
thf(100,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ subclass ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(62283,plain,
$false,
inference(e,[status(thm)],[69,5422,22966,4824,4877,7886,115,217,308,5878,23810,511,4747,9059,247,5550,56,1137,142,18824,1988,47546,17258,18595,17253,6971,8913,26176,21467,5486,14436,24755,841,14488,301,45456,30722,31203,20926,184,9084,7652,125,28448,53905,357,196,157,5744,5868,11100,46,23098,57,261,10497,216,11441,9882,211,44789,15712,14987,44946,293,22271,25813,18065,116,243,233,5406,60,85,50500,534,29073,17061,27547,160,297,50893,46879,5594,21596,27248,24643,260,5579,693,17353,92,65,14477,97,461,17032,522,830,15702,8068,17232,4486,53,169,14601,9186,339,14473,17165,14719,7404,17239,212,96,256,109,328,4721,7981,5576,19911,43575,129,15934,622,837,2370,9068,19459,46880,128,1086,205,44790,52747,8871,7414,45979,14433,8846,73,9081,105,244,18508,47203,14388,18048,148,14469,161,149,176,45116,5962,826,12787,28489,259,59,118,5965,54,313,44554,49,20975,54721,7425,17041,7315,7394,4790,219,274,15452,19444,14595,76,245,271,208,4694,552,323,23728,140,213,66,251,4652,19917,18631,108,7561,816,103,9079,9174,609,17679,17223,9294,21183,45730,45446,44217,45421,226,17051,7507,241,22026,17251,162,9069,209,112,30872,123,6973,194,7539,52744,48,63,640,282,150,7956,14624,19954,17055,8904,19211,5018,557,17217,50,5767,199,5418,18669,17877,182,17045,32125,370,6188,154,4748,7391,72,45106,143,17215,17025,5771,5873,5653,203,43493,16983,218,104,2226,6970,7306,7547,52752,45117,139,21032,20663,7959,28100,24868,20425,17885,207,53304,5128,7406,75,5963,290,119,214,287,151,45451,21408,15953,51,7787,4787,183,273,14939,262,79,195,21177,8051,28814,5378,9293,27180,23895,242,126,136,8675,28353,4799,7829,68,49488,7392,19452,5768,111,254,4779,5591,122,18559,676,44787,26430,100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET076+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.13/0.39 % Computer : n018.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sat Sep 26 07:05:36 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 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.89/0.97 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.53/1.21 % [INFO] Parsing done (239ms).
% 1.53/1.23 % [INFO] Running in sequential loop mode.
% 2.16/1.62 % [INFO] eprover registered as external prover.
% 2.16/1.63 % [INFO] Scanning for conjecture ...
% 2.34/1.75 % [INFO] Found a conjecture (or negated_conjecture) and 43 axioms. Running axiom selection ...
% 2.51/1.83 % [INFO] Axiom selection finished. Selected 43 axioms (removed 0 axioms).
% 2.73/1.92 % [INFO] Problem is first-order (TPTP FOF).
% 2.73/1.93 % [INFO] Type checking passed.
% 2.73/1.94 % [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 ...
% 83.50/19.48 % External prover 'e' found a proof!
% 83.50/19.48 % [INFO] Killing All external provers ...
% 83.50/19.48 % Time passed: 18953ms (effective reasoning time: 18249ms)
% 83.50/19.48 % 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)>
% 83.50/19.48 % Axioms used in derivation (43): sum_class_defn, image_defn, cross_product_defn, extensionality, infinity, first_second, rotate, null_class_defn, sum_class, restrict_defn, compose_defn1, inductive_defn, unordered_pair, cross_product, flip_defn, function_defn, element_relation_defn, identity_relation, unordered_pair_defn, successor_relation_defn1, power_class_defn, intersection, inverse_defn, replacement, element_relation, singleton_set_defn, subclass_defn, domain_of, power_class, flip, compose_defn2, choice, complement, disjoint_defn, apply_defn, regularity, successor_defn, ordered_pair_defn, class_elements_are_sets, range_of_defn, union_defn, successor_relation_defn2, rotate_defn
% 83.50/19.48 % No. of inferences in proof: 1023
% 83.50/19.48 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 18953 ms resp. 18249 ms w/o parsing
% 70.31/19.77 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 70.31/19.78 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------