%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SET071+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n013.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:13 AM UTC 2026
% Result : Theorem 64.00s 18.73s
% Output : Refutation 80.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 52
% Syntax : Number of formulae : 974 ( 286 unt; 0 typ; 8 def)
% Number of atoms : 2873 ( 976 equ; 0 cnn)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 8874 (1488 ~; 970 |; 199 &;6095 @)
% ( 19 <=>; 103 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 42 ( 39 usr; 11 con; 0-3 aty)
% Number of variables : 1219 ( 7 ^;1187 !; 17 ?;1219 :)
% ( 0 !>; 0 ?*; 0 @-; 8 @+)
% Comments :
%------------------------------------------------------------------------------
thf(member_decl,type,
member: $i > $i > $o ).
thf(universal_class_decl,type,
universal_class: $i ).
thf(unordered_pair_decl,type,
unordered_pair: $i > $i > $i ).
thf(null_class_decl,type,
null_class: $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(subclass_decl,type,
subclass: $i > $i > $o ).
thf(restrict_decl,type,
restrict: $i > $i > $i > $i ).
thf(intersection_decl,type,
intersection: $i > $i > $i ).
thf(cross_product_decl,type,
cross_product: $i > $i > $i ).
thf(range_of_decl,type,
range_of: $i > $i ).
thf(domain_of_decl,type,
domain_of: $i > $i ).
thf(inverse_decl,type,
inverse: $i > $i ).
thf(flip_decl,type,
flip: $i > $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 > $i > $i ).
thf(sk4_decl,type,
sk4: $i > $i > $i ).
thf(sk5_decl,type,
sk5: $i > $i ).
thf(sk6_decl,type,
sk6: $i > $i > $i ).
thf(sk7_decl,type,
sk7: $i ).
thf(sk8_decl,type,
sk8: $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i] :
( ( ~ ( universal_class @ ( B @ member ) )
& ~ ( universal_class @ ( A @ member ) ) )
=> ( ( B @ ( A @ unordered_pair ) )
= null_class ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ( ( ~ ( universal_class @ ( A @ member ) )
& ~ ( universal_class @ ( sk1 @ member ) ) )
=> ( ( A @ ( sk1 @ unordered_pair ) )
= null_class ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( ( A @ ( C @ member ) )
& ( C @ ( B @ member ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( B @ ( C @ member ) )
=> ( A @ ( C @ member ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: $i] :
@+[B: $i] :
( ( A @ ( B @ disjoint ) )
& ( A @ ( B @ member ) )
& ( universal_class @ ( B @ member ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( ( A @ ( C @ member ) )
& ( B @ ( C @ member ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( @+[A: $i] :
( ! [B: $i] :
( ( B @ inductive )
=> ( B @ ( A @ subclass ) ) )
& ( A @ inductive )
& ( universal_class @ ( A @ member ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( @+[A: $i] :
( ! [B: $i] :
( ( universal_class @ ( B @ member ) )
=> ( ( B @ ( B @ ( A @ apply ) @ member ) )
| ( B = null_class ) ) )
& ( A @ function ) ) ) ) ).
thf(5,axiom,
! [A: $i,B: $i] :
( ( A = B )
<=> ( ( A @ ( B @ subclass ) )
& ( B @ ( A @ subclass ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',extensionality) ).
thf(58,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)],[5]) ).
thf(59,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)],[58]) ).
thf(60,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)],[59]) ).
thf(63,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ subclass ) )
| ~ ( B @ ( A @ subclass ) ) ),
inference(cnfConj,[status(thm)],[60]) ).
thf(68,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ subclass ) )
| ~ ( B @ ( A @ subclass ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[63]) ).
thf(69,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ subclass ) )
| ~ ( B @ ( A @ subclass ) )
| ( A = B ) ),
inference(simp,[status(thm)],[68]) ).
thf(17,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ intersection ) @ ( C @ member ) )
<=> ( ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection) ).
thf(134,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)],[17]) ).
thf(135,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)],[134]) ).
thf(136,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)],[135]) ).
thf(138,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ~ ( B @ ( A @ intersection ) @ ( C @ member ) ) ),
inference(cnfConj,[status(thm)],[136]) ).
thf(10,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ subclass ) )
<=> ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_defn) ).
thf(92,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)],[10]) ).
thf(93,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)],[92]) ).
thf(94,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( D @ subclass ) )
| ~ ( E @ ( D @ ( E @ sk4 ) @ member ) ) )
& ( ( E @ ( D @ subclass ) )
| ( D @ ( D @ ( E @ sk4 ) @ member ) ) )
& ( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ subclass ) ) ) ),
inference(cnf,[status(esa)],[93]) ).
thf(96,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subclass ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(98,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subclass ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[96]) ).
thf(29,axiom,
? [A: $i] :
( ! [B: $i] :
( ( B @ inductive )
=> ( B @ ( A @ subclass ) ) )
& ( A @ inductive )
& ( universal_class @ ( A @ member ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',infinity) ).
thf(207,plain,
? [A: $i] :
( ! [B: $i] :
( ( B @ inductive )
=> ( B @ ( A @ subclass ) ) )
& ( A @ inductive )
& ( universal_class @ ( A @ member ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(208,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ subclass ) )
| ~ ( A @ inductive ) )
& ( sk7 @ inductive )
& ( universal_class @ ( sk7 @ member ) ) ),
inference(cnf,[status(esa)],[207]) ).
thf(210,plain,
sk7 @ inductive,
inference(cnfConj,[status(thm)],[208]) ).
thf(13,axiom,
! [A: $i] :
( ( A @ inductive )
<=> ( ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
& ( A @ ( null_class @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inductive_defn) ).
thf(110,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)],[13]) ).
thf(111,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)],[110]) ).
thf(112,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)],[111]) ).
thf(113,plain,
! [A: $i] :
( ( A @ ( null_class @ member ) )
| ~ ( A @ inductive ) ),
inference(cnfConj,[status(thm)],[112]) ).
thf(30,axiom,
! [A: $i] :
~ ( null_class @ ( A @ member ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',null_class_defn) ).
thf(212,plain,
! [A: $i] :
~ ( null_class @ ( A @ member ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(213,plain,
~ ? [A: $i] : ( null_class @ ( A @ member ) ),
inference(miniscope,[status(thm)],[212]) ).
thf(214,plain,
! [A: $i] :
~ ( null_class @ ( A @ member ) ),
inference(cnf,[status(esa)],[213]) ).
thf(356,plain,
! [B: $i,A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( null_class @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[113,214]) ).
thf(357,plain,
! [B: $i,A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( null_class @ ( B @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[356]) ).
thf(358,plain,
~ ( null_class @ inductive ),
inference(pattern_uni,[status(thm)],[357:[bind(A,$thf( null_class )),bind(B,$thf( null_class ))]]) ).
thf(728,plain,
( ( ( sk7 @ inductive )
!= ( null_class @ inductive ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[210,358]) ).
thf(729,plain,
( ( sk7 @ inductive )
!= ( null_class @ inductive ) ),
inference(simp,[status(thm)],[728]) ).
thf(730,plain,
sk7 != null_class,
inference(simp,[status(thm)],[729]) ).
thf(732,plain,
! [B: $i,A: $i] :
( ( A != sk7 )
| ( B != null_class )
| ~ ( A @ ( B @ subclass ) )
| ~ ( B @ ( A @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[69,730]) ).
thf(733,plain,
! [A: $i] :
( ( A != null_class )
| ~ ( sk7 @ ( A @ subclass ) )
| ~ ( A @ ( sk7 @ subclass ) ) ),
inference(pattern_uni,[status(thm)],[732:[bind(A,$thf( sk7 ))]]) ).
thf(736,plain,
( ~ ( sk7 @ ( null_class @ subclass ) )
| ~ ( null_class @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[733]) ).
thf(3572,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ~ $true
| ( B @ ( A @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[98,214]) ).
thf(3573,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ( B @ ( A @ subclass ) ) ),
inference(simp,[status(thm)],[3572]) ).
thf(3574,plain,
! [A: $i] : ( A @ ( null_class @ subclass ) ),
inference(pattern_uni,[status(thm)],[3573:[bind(A,$thf( null_class )),bind(B,$thf( D )),bind(C,$thf( null_class @ ( D @ sk4 ) ))]]) ).
thf(3615,plain,
! [A: $i] : ( A @ ( null_class @ subclass ) ),
inference(simp,[status(thm)],[3574]) ).
thf(11139,plain,
( ~ $true
| ~ ( null_class @ ( sk7 @ subclass ) ) ),
inference(rewrite,[status(thm)],[736,3615]) ).
thf(11140,plain,
~ ( null_class @ ( sk7 @ subclass ) ),
inference(simp,[status(thm)],[11139]) ).
thf(11184,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( sk7 @ subclass ) ) )
| ~ $true
| ( A @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[98,11140]) ).
thf(11185,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( sk7 @ subclass ) ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[11184]) ).
thf(11186,plain,
sk7 @ ( sk7 @ ( null_class @ sk4 ) @ member ),
inference(pattern_uni,[status(thm)],[11185:[bind(A,$thf( sk7 )),bind(B,$thf( null_class ))]]) ).
thf(359,plain,
! [A: $i] :
( ( ( sk7 @ inductive )
!= ( A @ inductive ) )
| ( A @ ( null_class @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[210,113]) ).
thf(360,plain,
! [A: $i] :
( ( ( sk7 @ inductive )
!= ( A @ inductive ) )
| ( A @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[359]) ).
thf(361,plain,
sk7 @ ( null_class @ member ),
inference(pattern_uni,[status(thm)],[360:[bind(A,$thf( sk7 ))]]) ).
thf(8,axiom,
! [A: $i,B: $i] :
( ( B @ sum_class @ ( A @ member ) )
<=> ? [C: $i] :
( ( B @ ( C @ member ) )
& ( C @ ( A @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_class_defn) ).
thf(76,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)],[8]) ).
thf(77,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)],[76]) ).
thf(78,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 @ sk3 ) @ member ) )
| ~ ( B @ sum_class @ ( A @ member ) ) )
& ( ( A @ ( B @ sk3 ) @ ( A @ member ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ) ),
inference(cnf,[status(esa)],[77]) ).
thf(80,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ sk3 ) @ member ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[78]) ).
thf(1609,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[80,214]) ).
thf(1610,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[1609]) ).
thf(1611,plain,
! [A: $i] :
~ ( null_class @ sum_class @ ( A @ member ) ),
inference(pattern_uni,[status(thm)],[1610:[bind(A,$thf( E )),bind(B,$thf( null_class )),bind(C,$thf( E @ ( null_class @ sk3 ) ))]]) ).
thf(1638,plain,
! [A: $i] :
~ ( null_class @ sum_class @ ( A @ member ) ),
inference(simp,[status(thm)],[1611]) ).
thf(2505,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ member ) )
!= ( null_class @ sum_class @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[80,1638]) ).
thf(2506,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ member ) )
!= ( null_class @ sum_class @ ( C @ member ) ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[2505]) ).
thf(2507,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(pattern_uni,[status(thm)],[2506:[bind(A,$thf( E )),bind(B,$thf( null_class @ sum_class )),bind(C,$thf( E @ ( null_class @ sum_class @ sk3 ) ))]]) ).
thf(2543,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(simp,[status(thm)],[2507]) ).
thf(2989,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[80,2543]) ).
thf(2990,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[2989]) ).
thf(2991,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(pattern_uni,[status(thm)],[2990:[bind(A,$thf( E )),bind(B,$thf( null_class @ sum_class @ sum_class )),bind(C,$thf( E @ ( null_class @ sum_class @ sum_class @ sk3 ) ))]]) ).
thf(3039,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(simp,[status(thm)],[2991]) ).
thf(3825,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[80,3039]) ).
thf(3826,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[3825]) ).
thf(3827,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(pattern_uni,[status(thm)],[3826:[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 @ sk3 ) ))]]) ).
thf(3891,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(simp,[status(thm)],[3827]) ).
thf(5162,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[80,3891]) ).
thf(5163,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[5162]) ).
thf(5164,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(pattern_uni,[status(thm)],[5163:[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 @ sk3 ) ))]]) ).
thf(5233,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(simp,[status(thm)],[5164]) ).
thf(6608,plain,
! [A: $i] :
( ( ( sk7 @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[361,5233]) ).
thf(6609,plain,
! [A: $i] :
( ( sk7 @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[6608]) ).
thf(6680,plain,
! [A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk7 )
| ( null_class != A ) ),
inference(simp,[status(thm)],[6609]) ).
thf(6705,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk7 ),
inference(simp,[status(thm)],[6680]) ).
thf(18,axiom,
! [A: $i] :
( ( A != null_class )
=> ? [B: $i] :
( ( A @ ( B @ disjoint ) )
& ( A @ ( B @ member ) )
& ( universal_class @ ( B @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity) ).
thf(141,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)],[18]) ).
thf(142,plain,
! [A: $i] :
( ( ( A @ ( A @ sk5 @ disjoint ) )
| ( A = null_class ) )
& ( ( A @ ( A @ sk5 @ member ) )
| ( A = null_class ) )
& ( ( universal_class @ ( A @ sk5 @ member ) )
| ( A = null_class ) ) ),
inference(cnf,[status(esa)],[141]) ).
thf(144,plain,
! [A: $i] :
( ( A @ ( A @ sk5 @ member ) )
| ( A = null_class ) ),
inference(cnfConj,[status(thm)],[142]) ).
thf(147,plain,
! [A: $i] :
( ( A @ ( A @ sk5 @ member ) )
| ( A = null_class ) ),
inference(lifteq,[status(thm)],[144]) ).
thf(12970,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk5 @ member ) )
!= ( null_class @ sum_class @ ( B @ member ) ) )
| ~ $true
| ( A = null_class ) ),
inference(paramod_ordered,[status(thm)],[147,1638]) ).
thf(12971,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk5 @ member ) )
!= ( null_class @ sum_class @ ( B @ member ) ) )
| ( A = null_class ) ),
inference(simp,[status(thm)],[12970]) ).
thf(12972,plain,
( ( null_class @ sum_class )
= null_class ),
inference(pattern_uni,[status(thm)],[12971:[bind(A,$thf( null_class @ sum_class )),bind(B,$thf( null_class @ sum_class @ sk5 ))]]) ).
thf(13821,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk7 ),
inference(rewrite,[status(thm)],[6705,12972]) ).
thf(13332,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk5 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ~ $true
| ( A = null_class ) ),
inference(paramod_ordered,[status(thm)],[147,3039]) ).
thf(13333,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk5 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ( A = null_class ) ),
inference(simp,[status(thm)],[13332]) ).
thf(13334,plain,
( ( null_class @ sum_class @ sum_class @ sum_class )
= null_class ),
inference(pattern_uni,[status(thm)],[13333:[bind(A,$thf( null_class @ sum_class @ sum_class @ sum_class )),bind(B,$thf( null_class @ sum_class @ sum_class @ sum_class @ sk5 ))]]) ).
thf(15425,plain,
( ( null_class @ sum_class @ sum_class )
= null_class ),
inference(rewrite,[status(thm)],[13334,12972]) ).
thf(16444,plain,
( ( null_class @ sum_class @ sum_class )
!= sk7 ),
inference(rewrite,[status(thm)],[13821,15425]) ).
thf(34,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ union ) @ ( C @ member ) )
<=> ( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',union_defn) ).
thf(231,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)],[34]) ).
thf(232,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) ) )
=> ( B @ ( A @ union ) @ ( C @ member ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ union ) @ ( C @ member ) )
=> ( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[231]) ).
thf(233,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( D @ union ) @ ( F @ member ) )
| ~ ( E @ ( F @ member ) ) )
& ( ( E @ ( D @ union ) @ ( F @ member ) )
| ~ ( D @ ( F @ member ) ) )
& ( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) )
| ~ ( B @ ( A @ union ) @ ( C @ member ) ) ) ),
inference(cnf,[status(esa)],[232]) ).
thf(234,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) )
| ~ ( B @ ( A @ union ) @ ( C @ member ) ) ),
inference(cnfConj,[status(thm)],[233]) ).
thf(14,axiom,
! [A: $i,B: $i] :
( ( B @ power_class @ ( A @ member ) )
<=> ( ( B @ ( A @ subclass ) )
& ( universal_class @ ( A @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',power_class_defn) ).
thf(117,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)],[14]) ).
thf(118,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)],[117]) ).
thf(119,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)],[118]) ).
thf(121,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subclass ) )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[119]) ).
thf(209,plain,
universal_class @ ( sk7 @ member ),
inference(cnfConj,[status(thm)],[208]) ).
thf(1,conjecture,
! [A: $i,B: $i] :
( ( ~ ( universal_class @ ( B @ member ) )
& ~ ( universal_class @ ( A @ member ) ) )
=> ( ( B @ ( A @ unordered_pair ) )
= null_class ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',null_unordered_pair) ).
thf(2,negated_conjecture,
~ ! [A: $i,B: $i] :
( ( ~ ( universal_class @ ( B @ member ) )
& ~ ( universal_class @ ( A @ member ) ) )
=> ( ( B @ ( A @ unordered_pair ) )
= null_class ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(46,plain,
~ ! [A: $i,B: $i] :
( ( ~ ( universal_class @ ( B @ member ) )
& ~ ( universal_class @ ( A @ member ) ) )
=> ( ( B @ ( A @ unordered_pair ) )
= null_class ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(47,plain,
( ( ( sk2 @ ( sk1 @ unordered_pair ) )
!= null_class )
& ~ ( universal_class @ ( sk2 @ member ) )
& ~ ( universal_class @ ( sk1 @ member ) ) ),
inference(cnf,[status(esa)],[46]) ).
thf(49,plain,
~ ( universal_class @ ( sk2 @ member ) ),
inference(cnfConj,[status(thm)],[47]) ).
thf(277,plain,
( ( ( universal_class @ ( sk7 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[209,49]) ).
thf(278,plain,
( ( universal_class @ ( sk7 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[277]) ).
thf(283,plain,
( ( universal_class != universal_class )
| ( sk7 != sk2 ) ),
inference(simp,[status(thm)],[278]) ).
thf(286,plain,
sk7 != sk2,
inference(simp,[status(thm)],[283]) ).
thf(422,plain,
! [B: $i,A: $i] :
( ( A != sk7 )
| ( B != sk2 )
| ~ ( A @ ( B @ subclass ) )
| ~ ( B @ ( A @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[69,286]) ).
thf(423,plain,
! [A: $i] :
( ( A != sk2 )
| ~ ( sk7 @ ( A @ subclass ) )
| ~ ( A @ ( sk7 @ subclass ) ) ),
inference(pattern_uni,[status(thm)],[422:[bind(A,$thf( sk7 ))]]) ).
thf(697,plain,
( ~ ( sk7 @ ( sk2 @ subclass ) )
| ~ ( sk2 @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[423]) ).
thf(3632,plain,
! [A: $i] :
( ( ( A @ ( null_class @ subclass ) )
!= ( sk7 @ ( sk2 @ subclass ) ) )
| ~ $true
| ~ ( sk2 @ ( sk7 @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[3615,697]) ).
thf(3633,plain,
! [A: $i] :
( ( ( A @ ( null_class @ subclass ) )
!= ( sk7 @ ( sk2 @ subclass ) ) )
| ~ ( sk2 @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[3632]) ).
thf(3654,plain,
! [A: $i] :
( ( A != sk7 )
| ( sk2 != null_class )
| ~ ( sk2 @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[3633]) ).
thf(3660,plain,
( ( sk2 != null_class )
| ~ ( sk2 @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[3654]) ).
thf(7070,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk2 @ ( sk7 @ subclass ) ) )
| ( sk2 != null_class )
| ~ $true
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[121,3660]) ).
thf(7071,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk2 @ ( sk7 @ subclass ) ) )
| ( sk2 != null_class )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[7070]) ).
thf(7072,plain,
( ( sk2 != null_class )
| ~ ( sk2 @ power_class @ ( sk7 @ member ) ) ),
inference(pattern_uni,[status(thm)],[7071:[bind(A,$thf( sk7 )),bind(B,$thf( sk2 ))]]) ).
thf(11314,plain,
( ( ( sk7 @ ( sk7 @ ( null_class @ sk4 ) @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11186,49]) ).
thf(11315,plain,
( ( sk7 @ ( sk7 @ ( null_class @ sk4 ) @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[11314]) ).
thf(11385,plain,
( ( sk7 != universal_class )
| ( ( sk7 @ ( null_class @ sk4 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[11315]) ).
thf(143,plain,
! [A: $i] :
( ( universal_class @ ( A @ sk5 @ member ) )
| ( A = null_class ) ),
inference(cnfConj,[status(thm)],[142]) ).
thf(146,plain,
! [A: $i] :
( ( universal_class @ ( A @ sk5 @ member ) )
| ( A = null_class ) ),
inference(lifteq,[status(thm)],[143]) ).
thf(1182,plain,
! [A: $i] :
( ( A != sk7 )
| ( null_class != null_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,730]) ).
thf(1183,plain,
! [A: $i] :
( ( A != sk7 )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[1182]) ).
thf(1184,plain,
universal_class @ ( sk7 @ sk5 @ member ),
inference(pattern_uni,[status(thm)],[1183:[bind(A,$thf( sk7 ))]]) ).
thf(39,axiom,
! [A: $i,B: $i] :
( ( A @ complement @ ( B @ member ) )
<=> ( ~ ( A @ ( B @ member ) )
& ( universal_class @ ( B @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement) ).
thf(248,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(249,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)],[248]) ).
thf(250,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)],[249]) ).
thf(252,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ member ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(cnfConj,[status(thm)],[250]) ).
thf(1684,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk7 @ sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[1184,252]) ).
thf(1685,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk7 @ sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[1684]) ).
thf(1686,plain,
~ ( universal_class @ complement @ ( sk7 @ sk5 @ member ) ),
inference(pattern_uni,[status(thm)],[1685:[bind(A,$thf( universal_class )),bind(B,$thf( sk7 @ sk5 ))]]) ).
thf(22,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/sandbox2/benchmark/theBenchmark.p',rotate_defn) ).
thf(167,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)],[22]) ).
thf(168,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)],[167]) ).
thf(169,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)],[168]) ).
thf(170,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)],[169]) ).
thf(23760,plain,
( ( ( sk2 @ power_class @ ( sk7 @ member ) )
!= ( universal_class @ ( sk7 @ member ) ) )
| ( sk2 != null_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[209,7072]) ).
thf(23761,plain,
( ( ( sk2 @ power_class @ ( sk7 @ member ) )
!= ( universal_class @ ( sk7 @ member ) ) )
| ( sk2 != null_class ) ),
inference(simp,[status(thm)],[23760]) ).
thf(23846,plain,
( ( ( sk2 @ power_class )
!= universal_class )
| ( sk7 != sk7 )
| ( sk2 != null_class ) ),
inference(simp,[status(thm)],[23761]) ).
thf(23865,plain,
( ( ( sk2 @ power_class )
!= universal_class )
| ( sk2 != null_class ) ),
inference(simp,[status(thm)],[23846]) ).
thf(281,plain,
! [A: $i] :
( ( ( universal_class @ ( sk7 @ member ) )
!= ( null_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[209,214]) ).
thf(282,plain,
! [A: $i] :
( ( universal_class @ ( sk7 @ member ) )
!= ( null_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[281]) ).
thf(285,plain,
! [A: $i] :
( ( null_class != universal_class )
| ( sk7 != A ) ),
inference(simp,[status(thm)],[282]) ).
thf(288,plain,
null_class != universal_class,
inference(simp,[status(thm)],[285]) ).
thf(1248,plain,
! [A: $i] :
( ( null_class != null_class )
| ( A != universal_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,288]) ).
thf(1249,plain,
! [A: $i] :
( ( A != universal_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[1248:[]]) ).
thf(1458,plain,
universal_class @ ( universal_class @ sk5 @ member ),
inference(simp,[status(thm)],[1249]) ).
thf(1777,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( universal_class @ sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[1458,252]) ).
thf(1778,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( universal_class @ sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[1777]) ).
thf(1779,plain,
~ ( universal_class @ complement @ ( universal_class @ sk5 @ member ) ),
inference(pattern_uni,[status(thm)],[1778:[bind(A,$thf( universal_class )),bind(B,$thf( universal_class @ sk5 ))]]) ).
thf(2214,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( universal_class @ complement @ ( universal_class @ sk5 @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[113,1779]) ).
thf(2215,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( universal_class @ complement @ ( universal_class @ sk5 @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[2214]) ).
thf(2245,plain,
! [A: $i] :
( ( A
!= ( universal_class @ complement ) )
| ( ( universal_class @ sk5 )
!= null_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[2215]) ).
thf(2248,plain,
( ( ( universal_class @ sk5 )
!= null_class )
| ~ ( universal_class @ complement @ inductive ) ),
inference(simp,[status(thm)],[2245]) ).
thf(120,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( A @ member ) )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[119]) ).
thf(28,axiom,
universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_relation_defn1) ).
thf(206,plain,
universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(466,plain,
! [B: $i,A: $i] :
( ( A != null_class )
| ( B != universal_class )
| ~ ( A @ ( B @ subclass ) )
| ~ ( B @ ( A @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[69,288]) ).
thf(467,plain,
! [A: $i] :
( ( A != universal_class )
| ~ ( null_class @ ( A @ subclass ) )
| ~ ( A @ ( null_class @ subclass ) ) ),
inference(pattern_uni,[status(thm)],[466:[bind(A,$thf( null_class ))]]) ).
thf(712,plain,
( ~ ( null_class @ ( universal_class @ subclass ) )
| ~ ( universal_class @ ( null_class @ subclass ) ) ),
inference(simp,[status(thm)],[467]) ).
thf(9050,plain,
( ~ ( null_class @ ( universal_class @ subclass ) )
| ~ $true ),
inference(rewrite,[status(thm)],[712,3615]) ).
thf(9051,plain,
~ ( null_class @ ( universal_class @ subclass ) ),
inference(simp,[status(thm)],[9050]) ).
thf(9073,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[206,9051]) ).
thf(9074,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( successor_relation @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) ),
inference(simp,[status(thm)],[9073]) ).
thf(9135,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( successor_relation != universal_class ) ),
inference(simp,[status(thm)],[9074]) ).
thf(32,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/sandbox2/benchmark/theBenchmark.p',flip_defn) ).
thf(217,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)],[32]) ).
thf(15,axiom,
! [A: $i] :
( ( A @ singleton )
= ( A @ ( A @ unordered_pair ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set_defn) ).
thf(124,plain,
! [A: $i] :
( ( A @ singleton )
= ( A @ ( A @ unordered_pair ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(125,plain,
! [A: $i] :
( ( A @ singleton )
= ( A @ ( A @ unordered_pair ) ) ),
inference(cnf,[status(esa)],[124]) ).
thf(126,plain,
! [A: $i] :
( ( A @ ( A @ unordered_pair ) )
= ( A @ singleton ) ),
inference(lifteq,[status(thm)],[125]) ).
thf(27,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
<=> ( ( ( A = C )
| ( A = B ) )
& ( universal_class @ ( A @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair_defn) ).
thf(194,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)],[27]) ).
thf(195,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)],[194]) ).
thf(196,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)],[195]) ).
thf(199,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
| ( A != B )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[196]) ).
thf(202,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
| ~ ( universal_class @ ( A @ member ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[199]) ).
thf(203,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( A @ member ) )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[202]) ).
thf(35216,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk7 @ member ) )
!= ( universal_class @ ( A @ member ) ) )
| ( B @ ( A @ unordered_pair ) @ ( A @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[209,203]) ).
thf(35217,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk7 @ member ) )
!= ( universal_class @ ( A @ member ) ) )
| ( B @ ( A @ unordered_pair ) @ ( A @ member ) ) ),
inference(simp,[status(thm)],[35216]) ).
thf(35218,plain,
! [A: $i] : ( A @ ( sk7 @ unordered_pair ) @ ( sk7 @ member ) ),
inference(pattern_uni,[status(thm)],[35217:[bind(A,$thf( sk7 ))]]) ).
thf(35495,plain,
! [A: $i] : ( A @ ( sk7 @ unordered_pair ) @ ( sk7 @ member ) ),
inference(simp,[status(thm)],[35218]) ).
thf(35733,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ unordered_pair ) )
!= ( B @ ( sk7 @ unordered_pair ) ) )
| ( A @ singleton @ ( sk7 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[126,35495]) ).
thf(35734,plain,
sk7 @ singleton @ ( sk7 @ member ),
inference(pattern_uni,[status(thm)],[35733:[bind(A,$thf( sk7 )),bind(B,$thf( sk7 ))]]) ).
thf(36071,plain,
! [A: $i] :
( ( ( sk7 @ singleton @ ( sk7 @ member ) )
!= ( null_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35734,214]) ).
thf(36072,plain,
! [A: $i] :
( ( sk7 @ singleton @ ( sk7 @ member ) )
!= ( null_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[36071]) ).
thf(36101,plain,
! [A: $i] :
( ( ( sk7 @ singleton )
!= null_class )
| ( sk7 != A ) ),
inference(simp,[status(thm)],[36072]) ).
thf(36158,plain,
( ( sk7 @ singleton )
!= null_class ),
inference(simp,[status(thm)],[36101]) ).
thf(36244,plain,
! [A: $i] :
( ( A
!= ( sk7 @ singleton ) )
| ( null_class != null_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,36158]) ).
thf(36245,plain,
! [A: $i] :
( ( A
!= ( sk7 @ singleton ) )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[36244]) ).
thf(36246,plain,
universal_class @ ( sk7 @ singleton @ sk5 @ member ),
inference(pattern_uni,[status(thm)],[36245:[bind(A,$thf( sk7 @ singleton ))]]) ).
thf(36485,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk7 @ singleton @ sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[36246,252]) ).
thf(36486,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk7 @ singleton @ sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[36485]) ).
thf(36487,plain,
~ ( universal_class @ complement @ ( sk7 @ singleton @ sk5 @ member ) ),
inference(pattern_uni,[status(thm)],[36486:[bind(A,$thf( universal_class )),bind(B,$thf( sk7 @ singleton @ sk5 ))]]) ).
thf(35968,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ singleton @ ( sk7 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[35734,252]) ).
thf(35969,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ singleton @ ( sk7 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[35968]) ).
thf(35970,plain,
~ ( sk7 @ singleton @ complement @ ( sk7 @ member ) ),
inference(pattern_uni,[status(thm)],[35969:[bind(A,$thf( sk7 @ singleton )),bind(B,$thf( sk7 ))]]) ).
thf(37522,plain,
( ( ( sk7 @ singleton @ complement @ ( sk7 @ member ) )
!= ( sk7 @ singleton @ ( sk7 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35734,35970]) ).
thf(37523,plain,
( ( sk7 @ singleton @ complement @ ( sk7 @ member ) )
!= ( sk7 @ singleton @ ( sk7 @ member ) ) ),
inference(simp,[status(thm)],[37522]) ).
thf(37618,plain,
( ( ( sk7 @ singleton @ complement )
!= ( sk7 @ singleton ) )
| ( sk7 != sk7 ) ),
inference(simp,[status(thm)],[37523]) ).
thf(37685,plain,
( ( sk7 @ singleton @ complement )
!= ( sk7 @ singleton ) ),
inference(simp,[status(thm)],[37618]) ).
thf(48,plain,
~ ( universal_class @ ( sk1 @ member ) ),
inference(cnfConj,[status(thm)],[47]) ).
thf(342,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[113,48]) ).
thf(343,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[342]) ).
thf(362,plain,
! [A: $i] :
( ( A != universal_class )
| ( sk1 != null_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[343]) ).
thf(367,plain,
( ( sk1 != null_class )
| ~ ( universal_class @ inductive ) ),
inference(simp,[status(thm)],[362]) ).
thf(1326,plain,
! [A: $i] :
( ( A != sk1 )
| ( null_class != null_class )
| ~ ( universal_class @ inductive )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,367]) ).
thf(1327,plain,
! [A: $i] :
( ( A != sk1 )
| ~ ( universal_class @ inductive )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[1326]) ).
thf(1328,plain,
( ~ ( universal_class @ inductive )
| ( universal_class @ ( sk1 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[1327:[bind(A,$thf( sk1 ))]]) ).
thf(8127,plain,
( ( ( universal_class @ ( sk1 @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true
| ~ ( universal_class @ inductive ) ),
inference(paramod_ordered,[status(thm)],[1328,49]) ).
thf(8128,plain,
( ( ( universal_class @ ( sk1 @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ ( universal_class @ inductive ) ),
inference(simp,[status(thm)],[8127]) ).
thf(8198,plain,
( ( universal_class != universal_class )
| ( ( sk1 @ sk5 )
!= sk2 )
| ~ ( universal_class @ inductive ) ),
inference(simp,[status(thm)],[8128]) ).
thf(8204,plain,
( ( ( sk1 @ sk5 )
!= sk2 )
| ~ ( universal_class @ inductive ) ),
inference(simp,[status(thm)],[8198]) ).
thf(25,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/sandbox2/benchmark/theBenchmark.p',successor_relation_defn2) ).
thf(182,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)],[25]) ).
thf(183,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)],[182]) ).
thf(184,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)],[183]) ).
thf(185,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( A @ member ) )
| ~ ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[184]) ).
thf(50,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) )
!= null_class ),
inference(cnfConj,[status(thm)],[47]) ).
thf(51,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) )
!= null_class ),
inference(lifteq,[status(thm)],[50]) ).
thf(13467,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( null_class != null_class )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[147,51]) ).
thf(13468,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[13467]) ).
thf(13469,plain,
sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ),
inference(pattern_uni,[status(thm)],[13468:[bind(A,$thf( sk2 @ ( sk1 @ unordered_pair ) ))]]) ).
thf(35723,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk7 @ unordered_pair ) @ ( sk7 @ member ) )
!= ( null_class @ ( B @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35495,214]) ).
thf(35724,plain,
! [B: $i,A: $i] :
( ( A @ ( sk7 @ unordered_pair ) @ ( sk7 @ member ) )
!= ( null_class @ ( B @ member ) ) ),
inference(simp,[status(thm)],[35723]) ).
thf(35768,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk7 @ unordered_pair ) )
!= null_class )
| ( sk7 != B ) ),
inference(simp,[status(thm)],[35724]) ).
thf(35849,plain,
! [A: $i] :
( ( A @ ( sk7 @ unordered_pair ) )
!= null_class ),
inference(simp,[status(thm)],[35768]) ).
thf(39816,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( sk7 @ unordered_pair ) ) )
| ( null_class != null_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,35849]) ).
thf(39817,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( sk7 @ unordered_pair ) ) )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[39816]) ).
thf(39818,plain,
! [A: $i] : ( universal_class @ ( A @ ( sk7 @ unordered_pair ) @ sk5 @ member ) ),
inference(pattern_uni,[status(thm)],[39817:[bind(A,$thf( D @ ( sk7 @ unordered_pair ) )),bind(B,$thf( D ))]]) ).
thf(39831,plain,
! [A: $i] : ( universal_class @ ( A @ ( sk7 @ unordered_pair ) @ sk5 @ member ) ),
inference(simp,[status(thm)],[39818]) ).
thf(279,plain,
( ( ( universal_class @ ( sk7 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[209,48]) ).
thf(280,plain,
( ( universal_class @ ( sk7 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[279]) ).
thf(284,plain,
( ( universal_class != universal_class )
| ( sk7 != sk1 ) ),
inference(simp,[status(thm)],[280]) ).
thf(287,plain,
sk7 != sk1,
inference(simp,[status(thm)],[284]) ).
thf(608,plain,
! [B: $i,A: $i] :
( ( A != sk7 )
| ( B != sk1 )
| ~ ( A @ ( B @ subclass ) )
| ~ ( B @ ( A @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[69,287]) ).
thf(609,plain,
! [A: $i] :
( ( A != sk1 )
| ~ ( sk7 @ ( A @ subclass ) )
| ~ ( A @ ( sk7 @ subclass ) ) ),
inference(pattern_uni,[status(thm)],[608:[bind(A,$thf( sk7 ))]]) ).
thf(673,plain,
( ~ ( sk7 @ ( sk1 @ subclass ) )
| ~ ( sk1 @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[609]) ).
thf(3641,plain,
! [A: $i] :
( ( ( A @ ( null_class @ subclass ) )
!= ( sk7 @ ( sk1 @ subclass ) ) )
| ~ $true
| ~ ( sk1 @ ( sk7 @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[3615,673]) ).
thf(3642,plain,
! [A: $i] :
( ( ( A @ ( null_class @ subclass ) )
!= ( sk7 @ ( sk1 @ subclass ) ) )
| ~ ( sk1 @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[3641]) ).
thf(3653,plain,
! [A: $i] :
( ( A != sk7 )
| ( sk1 != null_class )
| ~ ( sk1 @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[3642]) ).
thf(3659,plain,
( ( sk1 != null_class )
| ~ ( sk1 @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[3653]) ).
thf(7097,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk1 @ ( sk7 @ subclass ) ) )
| ( sk1 != null_class )
| ~ $true
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[121,3659]) ).
thf(7098,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk1 @ ( sk7 @ subclass ) ) )
| ( sk1 != null_class )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[7097]) ).
thf(7099,plain,
( ( sk1 != null_class )
| ~ ( sk1 @ power_class @ ( sk7 @ member ) ) ),
inference(pattern_uni,[status(thm)],[7098:[bind(A,$thf( sk7 )),bind(B,$thf( sk1 ))]]) ).
thf(26088,plain,
( ( ( sk1 @ power_class @ ( sk7 @ member ) )
!= ( universal_class @ ( sk7 @ member ) ) )
| ( sk1 != null_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[209,7099]) ).
thf(26089,plain,
( ( ( sk1 @ power_class @ ( sk7 @ member ) )
!= ( universal_class @ ( sk7 @ member ) ) )
| ( sk1 != null_class ) ),
inference(simp,[status(thm)],[26088]) ).
thf(26144,plain,
( ( ( sk1 @ power_class )
!= universal_class )
| ( sk7 != sk7 )
| ( sk1 != null_class ) ),
inference(simp,[status(thm)],[26089]) ).
thf(26186,plain,
( ( ( sk1 @ power_class )
!= universal_class )
| ( sk1 != null_class ) ),
inference(simp,[status(thm)],[26144]) ).
thf(40,axiom,
? [A: $i] :
( ! [B: $i] :
( ( universal_class @ ( B @ member ) )
=> ( ( B @ ( B @ ( A @ apply ) @ member ) )
| ( B = null_class ) ) )
& ( A @ function ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',choice) ).
thf(255,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(256,plain,
! [A: $i] :
( ( ( A @ ( A @ ( sk8 @ apply ) @ member ) )
| ( A = null_class )
| ~ ( universal_class @ ( A @ member ) ) )
& ( sk8 @ function ) ),
inference(cnf,[status(esa)],[255]) ).
thf(257,plain,
sk8 @ function,
inference(cnfConj,[status(thm)],[256]) ).
thf(1697,plain,
! [A: $i] :
( ( A
!= ( sk7 @ sk5 ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,1184]) ).
thf(1698,plain,
( ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( sk7 @ sk5 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[1697:[bind(A,$thf( sk7 @ sk5 ))]]) ).
thf(3368,plain,
! [A: $i] :
( ( A
!= ( sk7 @ sk5 @ sk5 ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,1698]) ).
thf(3369,plain,
! [A: $i] :
( ( A
!= ( sk7 @ sk5 @ sk5 ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[3368]) ).
thf(3370,plain,
( ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( sk7 @ sk5 @ sk5 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[3369:[bind(A,$thf( sk7 @ sk5 @ sk5 ))]]) ).
thf(26,axiom,
! [A: $i,B: $i] : ( universal_class @ ( B @ ( A @ unordered_pair ) @ member ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair) ).
thf(192,plain,
! [A: $i,B: $i] : ( universal_class @ ( B @ ( A @ unordered_pair ) @ member ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(193,plain,
! [B: $i,A: $i] : ( universal_class @ ( B @ ( A @ unordered_pair ) @ member ) ),
inference(cnf,[status(esa)],[192]) ).
thf(975,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)],[126,193]) ).
thf(976,plain,
! [A: $i] : ( universal_class @ ( A @ singleton @ member ) ),
inference(pattern_uni,[status(thm)],[975:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(6629,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ 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)],[80,5233]) ).
thf(6630,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[6629]) ).
thf(6631,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(pattern_uni,[status(thm)],[6630:[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 @ sk3 ) ))]]) ).
thf(6709,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(simp,[status(thm)],[6631]) ).
thf(7925,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ 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)],[80,6709]) ).
thf(7926,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ 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)],[7925]) ).
thf(7927,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)],[7926:[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 @ sk3 ) ))]]) ).
thf(8031,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)],[7927]) ).
thf(10550,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( A @ singleton @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[976,8031]) ).
thf(10551,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( A @ singleton @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) ),
inference(simp,[status(thm)],[10550]) ).
thf(10588,plain,
! [B: $i,A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= universal_class )
| ( ( A @ singleton )
!= B ) ),
inference(simp,[status(thm)],[10551]) ).
thf(10629,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= universal_class ),
inference(simp,[status(thm)],[10588]) ).
thf(13818,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= universal_class ),
inference(rewrite,[status(thm)],[10629,12972]) ).
thf(12694,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk5 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ~ $true
| ( A = null_class ) ),
inference(paramod_ordered,[status(thm)],[147,5233]) ).
thf(12695,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk5 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ( A = null_class ) ),
inference(simp,[status(thm)],[12694]) ).
thf(12696,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
= null_class ),
inference(pattern_uni,[status(thm)],[12695:[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 @ sk5 ))]]) ).
thf(16945,plain,
( ( null_class @ sum_class @ sum_class @ sum_class )
= null_class ),
inference(rewrite,[status(thm)],[12696,15425]) ).
thf(17924,plain,
( ( null_class @ sum_class @ sum_class @ sum_class )
!= universal_class ),
inference(rewrite,[status(thm)],[13818,16945]) ).
thf(23,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/sandbox2/benchmark/theBenchmark.p',first_second) ).
thf(174,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)],[23]) ).
thf(3,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ apply ) )
= ( B @ singleton @ ( A @ image ) @ sum_class ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',apply_defn) ).
thf(52,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ apply ) )
= ( B @ singleton @ ( A @ image ) @ sum_class ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(211,plain,
! [A: $i] :
( ( A @ ( sk7 @ subclass ) )
| ~ ( A @ inductive ) ),
inference(cnfConj,[status(thm)],[208]) ).
thf(36,axiom,
! [A: $i] : ( universal_class @ ( A @ subclass ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',class_elements_are_sets) ).
thf(241,plain,
! [A: $i] : ( universal_class @ ( A @ subclass ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(242,plain,
! [A: $i] : ( universal_class @ ( A @ subclass ) ),
inference(cnf,[status(esa)],[241]) ).
thf(1537,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ subclass ) )
!= ( sk7 @ ( sk1 @ subclass ) ) )
| ~ $true
| ~ ( sk1 @ ( sk7 @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[242,673]) ).
thf(1538,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ subclass ) )
!= ( sk7 @ ( sk1 @ subclass ) ) )
| ~ ( sk1 @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[1537]) ).
thf(1545,plain,
! [A: $i] :
( ( sk7 != universal_class )
| ( A != sk1 )
| ~ ( sk1 @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[1538]) ).
thf(1556,plain,
( ( sk7 != universal_class )
| ~ ( sk1 @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[1545]) ).
thf(38550,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ subclass ) )
!= ( sk1 @ ( sk7 @ subclass ) ) )
| ( sk7 != universal_class )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[211,1556]) ).
thf(38551,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ subclass ) )
!= ( sk1 @ ( sk7 @ subclass ) ) )
| ( sk7 != universal_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[38550]) ).
thf(38552,plain,
( ( sk7 != universal_class )
| ~ ( sk1 @ inductive ) ),
inference(pattern_uni,[status(thm)],[38551:[bind(A,$thf( sk1 ))]]) ).
thf(1250,plain,
! [A: $i] :
( ( A != sk8 )
| ( null_class @ function )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,257]) ).
thf(1251,plain,
( ( null_class @ function )
| ( universal_class @ ( sk8 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[1250:[bind(A,$thf( sk8 ))]]) ).
thf(1874,plain,
( ( ( universal_class @ ( sk8 @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true
| ( null_class @ function ) ),
inference(paramod_ordered,[status(thm)],[1251,49]) ).
thf(1875,plain,
( ( ( universal_class @ ( sk8 @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ( null_class @ function ) ),
inference(simp,[status(thm)],[1874]) ).
thf(1887,plain,
( ( universal_class != universal_class )
| ( ( sk8 @ sk5 )
!= sk2 )
| ( null_class @ function ) ),
inference(simp,[status(thm)],[1875]) ).
thf(1907,plain,
( ( ( sk8 @ sk5 )
!= sk2 )
| ( null_class @ function ) ),
inference(simp,[status(thm)],[1887]) ).
thf(754,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ ( null_class @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[361,252]) ).
thf(755,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ ( null_class @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[754]) ).
thf(756,plain,
~ ( sk7 @ complement @ ( null_class @ member ) ),
inference(pattern_uni,[status(thm)],[755:[bind(A,$thf( sk7 )),bind(B,$thf( null_class ))]]) ).
thf(791,plain,
( ( ( sk7 @ complement @ ( null_class @ member ) )
!= ( sk7 @ ( null_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[361,756]) ).
thf(792,plain,
( ( sk7 @ complement @ ( null_class @ member ) )
!= ( sk7 @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[791]) ).
thf(796,plain,
( ( ( sk7 @ complement )
!= sk7 )
| ( null_class != null_class ) ),
inference(simp,[status(thm)],[792]) ).
thf(802,plain,
( ( sk7 @ complement )
!= sk7 ),
inference(simp,[status(thm)],[796]) ).
thf(35619,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk7 @ unordered_pair ) @ ( sk7 @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ complement @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[35495,252]) ).
thf(35620,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk7 @ unordered_pair ) @ ( sk7 @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ ( B @ complement @ ( C @ member ) ) ),
inference(simp,[status(thm)],[35619]) ).
thf(35621,plain,
! [A: $i] :
~ ( A @ ( sk7 @ unordered_pair ) @ complement @ ( sk7 @ member ) ),
inference(pattern_uni,[status(thm)],[35620:[bind(A,$thf( E )),bind(B,$thf( E @ ( sk7 @ unordered_pair ) )),bind(C,$thf( sk7 ))]]) ).
thf(35819,plain,
! [A: $i] :
~ ( A @ ( sk7 @ unordered_pair ) @ complement @ ( sk7 @ member ) ),
inference(simp,[status(thm)],[35621]) ).
thf(13810,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(rewrite,[status(thm)],[8031,12972]) ).
thf(12620,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk5 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ~ $true
| ( A = null_class ) ),
inference(paramod_ordered,[status(thm)],[147,8031]) ).
thf(12621,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk5 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ( A = null_class ) ),
inference(simp,[status(thm)],[12620]) ).
thf(12622,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
= null_class ),
inference(pattern_uni,[status(thm)],[12621:[bind(A,$thf( null_class @ sum_class @ sum_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 @ sum_class @ sum_class @ sk5 ))]]) ).
thf(19977,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class )
= null_class ),
inference(rewrite,[status(thm)],[12622,16945]) ).
thf(22254,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(rewrite,[status(thm)],[13810,19977]) ).
thf(20,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ disjoint ) )
<=> ! [C: $i] :
~ ( ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',disjoint_defn) ).
thf(152,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)],[20]) ).
thf(33,axiom,
! [A: $i,B: $i] :
( ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
<=> ( ( B @ ( A @ member ) )
& ( universal_class @ ( B @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_relation_defn) ).
thf(224,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)],[33]) ).
thf(225,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)],[224]) ).
thf(226,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)],[225]) ).
thf(228,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ member ) )
| ~ ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[226]) ).
thf(4,axiom,
! [A: $i] :
( ( A @ successor )
= ( A @ singleton @ ( A @ union ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor_defn) ).
thf(55,plain,
! [A: $i] :
( ( A @ successor )
= ( A @ singleton @ ( A @ union ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(56,plain,
! [A: $i] :
( ( A @ successor )
= ( A @ singleton @ ( A @ union ) ) ),
inference(cnf,[status(esa)],[55]) ).
thf(57,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ union ) )
= ( A @ successor ) ),
inference(lifteq,[status(thm)],[56]) ).
thf(354,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[113,49]) ).
thf(355,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[354]) ).
thf(364,plain,
! [A: $i] :
( ( A != universal_class )
| ( sk2 != null_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[355]) ).
thf(370,plain,
( ( sk2 != null_class )
| ~ ( universal_class @ inductive ) ),
inference(simp,[status(thm)],[364]) ).
thf(1238,plain,
! [A: $i] :
( ( A != sk2 )
| ( null_class != null_class )
| ~ ( universal_class @ inductive )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,370]) ).
thf(1239,plain,
! [A: $i] :
( ( A != sk2 )
| ~ ( universal_class @ inductive )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[1238]) ).
thf(1240,plain,
( ~ ( universal_class @ inductive )
| ( universal_class @ ( sk2 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[1239:[bind(A,$thf( sk2 ))]]) ).
thf(6413,plain,
( ( ( universal_class @ ( sk2 @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true
| ~ ( universal_class @ inductive ) ),
inference(paramod_ordered,[status(thm)],[1240,48]) ).
thf(6414,plain,
( ( ( universal_class @ ( sk2 @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ ( universal_class @ inductive ) ),
inference(simp,[status(thm)],[6413]) ).
thf(6461,plain,
( ( universal_class != universal_class )
| ( ( sk2 @ sk5 )
!= sk1 )
| ~ ( universal_class @ inductive ) ),
inference(simp,[status(thm)],[6414]) ).
thf(6487,plain,
( ( ( sk2 @ sk5 )
!= sk1 )
| ~ ( universal_class @ inductive ) ),
inference(simp,[status(thm)],[6461]) ).
thf(42,axiom,
! [A: $i] : ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( A @ flip @ subclass ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',flip) ).
thf(261,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(11157,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( sk7 @ subclass ) ) )
| ~ $true
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[121,11140]) ).
thf(11158,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( sk7 @ subclass ) ) )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[11157]) ).
thf(11159,plain,
~ ( null_class @ power_class @ ( sk7 @ member ) ),
inference(pattern_uni,[status(thm)],[11158:[bind(A,$thf( sk7 )),bind(B,$thf( null_class ))]]) ).
thf(11911,plain,
( ( ( null_class @ power_class @ ( sk7 @ member ) )
!= ( universal_class @ ( sk7 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[209,11159]) ).
thf(11912,plain,
( ( null_class @ power_class @ ( sk7 @ member ) )
!= ( universal_class @ ( sk7 @ member ) ) ),
inference(simp,[status(thm)],[11911]) ).
thf(11960,plain,
( ( ( null_class @ power_class )
!= universal_class )
| ( sk7 != sk7 ) ),
inference(simp,[status(thm)],[11912]) ).
thf(11986,plain,
( ( null_class @ power_class )
!= universal_class ),
inference(simp,[status(thm)],[11960]) ).
thf(1535,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ subclass ) )
!= ( sk1 @ ( sk7 @ subclass ) ) )
| ~ ( sk7 @ ( sk1 @ subclass ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[242,673]) ).
thf(1536,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ subclass ) )
!= ( sk1 @ ( sk7 @ subclass ) ) )
| ~ ( sk7 @ ( sk1 @ subclass ) ) ),
inference(simp,[status(thm)],[1535]) ).
thf(1553,plain,
! [A: $i] :
( ( sk1 != universal_class )
| ( A != sk7 )
| ~ ( sk7 @ ( sk1 @ subclass ) ) ),
inference(simp,[status(thm)],[1536]) ).
thf(1561,plain,
( ( sk1 != universal_class )
| ~ ( sk7 @ ( sk1 @ subclass ) ) ),
inference(simp,[status(thm)],[1553]) ).
thf(3647,plain,
! [A: $i] :
( ( ( A @ ( null_class @ subclass ) )
!= ( sk7 @ ( sk1 @ subclass ) ) )
| ( sk1 != universal_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3615,1561]) ).
thf(3648,plain,
! [A: $i] :
( ( ( A @ ( null_class @ subclass ) )
!= ( sk7 @ ( sk1 @ subclass ) ) )
| ( sk1 != universal_class ) ),
inference(simp,[status(thm)],[3647]) ).
thf(3649,plain,
! [A: $i] :
( ( A != sk7 )
| ( sk1 != null_class )
| ( sk1 != universal_class ) ),
inference(simp,[status(thm)],[3648]) ).
thf(3655,plain,
( ( sk1 != null_class )
| ( sk1 != universal_class ) ),
inference(simp,[status(thm)],[3649]) ).
thf(3905,plain,
! [A: $i] :
( ( A != sk1 )
| ( null_class != null_class )
| ( sk1 != universal_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,3655]) ).
thf(3906,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk1 != universal_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[3905]) ).
thf(3907,plain,
( ( sk1 != universal_class )
| ( universal_class @ ( sk1 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[3906:[bind(A,$thf( sk1 ))]]) ).
thf(16611,plain,
( ( ( universal_class @ ( sk1 @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true
| ( sk1 != universal_class ) ),
inference(paramod_ordered,[status(thm)],[3907,49]) ).
thf(16612,plain,
( ( ( universal_class @ ( sk1 @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ( sk1 != universal_class ) ),
inference(simp,[status(thm)],[16611]) ).
thf(16690,plain,
( ( universal_class != universal_class )
| ( ( sk1 @ sk5 )
!= sk2 )
| ( sk1 != universal_class ) ),
inference(simp,[status(thm)],[16612]) ).
thf(16721,plain,
( ( ( sk1 @ sk5 )
!= sk2 )
| ( sk1 != universal_class ) ),
inference(simp,[status(thm)],[16690]) ).
thf(3810,plain,
! [A: $i] :
( ( ( sk7 @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[361,3039]) ).
thf(3811,plain,
! [A: $i] :
( ( sk7 @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[3810]) ).
thf(3857,plain,
! [A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class )
!= sk7 )
| ( null_class != A ) ),
inference(simp,[status(thm)],[3811]) ).
thf(3875,plain,
( ( null_class @ sum_class @ sum_class @ sum_class )
!= sk7 ),
inference(simp,[status(thm)],[3857]) ).
thf(13836,plain,
( ( null_class @ sum_class @ sum_class )
!= sk7 ),
inference(rewrite,[status(thm)],[3875,12972]) ).
thf(15028,plain,
( ( null_class @ sum_class )
!= sk7 ),
inference(rewrite,[status(thm)],[13836,12972]) ).
thf(187,plain,
! [B: $i,A: $i] :
( ( ( A @ successor )
= B )
| ~ ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[184]) ).
thf(189,plain,
! [B: $i,A: $i] :
( ~ ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
| ( ( A @ successor )
= B ) ),
inference(lifteq,[status(thm)],[187]) ).
thf(11,axiom,
! [A: $i] :
( ( A @ inverse )
= ( universal_class @ ( A @ cross_product ) @ flip @ domain_of ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inverse_defn) ).
thf(100,plain,
! [A: $i] :
( ( A @ inverse )
= ( universal_class @ ( A @ cross_product ) @ flip @ domain_of ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(101,plain,
! [A: $i] :
( ( A @ inverse )
= ( universal_class @ ( A @ cross_product ) @ flip @ domain_of ) ),
inference(cnf,[status(esa)],[100]) ).
thf(102,plain,
! [A: $i] :
( ( A @ inverse )
= ( universal_class @ ( A @ cross_product ) @ flip @ domain_of ) ),
inference(lifteq,[status(thm)],[101]) ).
thf(7,axiom,
! [A: $i] :
( ( A @ range_of )
= ( A @ inverse @ domain_of ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',range_of_defn) ).
thf(73,plain,
! [A: $i] :
( ( A @ range_of )
= ( A @ inverse @ domain_of ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(74,plain,
! [A: $i] :
( ( A @ range_of )
= ( A @ inverse @ domain_of ) ),
inference(cnf,[status(esa)],[73]) ).
thf(75,plain,
! [A: $i] :
( ( A @ inverse @ domain_of )
= ( A @ range_of ) ),
inference(lifteq,[status(thm)],[74]) ).
thf(923,plain,
! [B: $i,A: $i] :
( ( ( A @ inverse )
!= ( B @ inverse ) )
| ( ( universal_class @ ( A @ cross_product ) @ flip @ domain_of @ domain_of )
= ( B @ range_of ) ) ),
inference(paramod_ordered,[status(thm)],[102,75]) ).
thf(924,plain,
! [A: $i] :
( ( universal_class @ ( A @ cross_product ) @ flip @ domain_of @ domain_of )
= ( A @ range_of ) ),
inference(pattern_uni,[status(thm)],[923:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(21,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/sandbox2/benchmark/theBenchmark.p',cross_product_defn) ).
thf(160,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)],[21]) ).
thf(161,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)],[160]) ).
thf(162,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)],[161]) ).
thf(164,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)],[162]) ).
thf(291,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk7 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[209,252]) ).
thf(292,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk7 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[291]) ).
thf(293,plain,
~ ( universal_class @ complement @ ( sk7 @ member ) ),
inference(pattern_uni,[status(thm)],[292:[bind(A,$thf( universal_class )),bind(B,$thf( sk7 ))]]) ).
thf(35926,plain,
( ( ( universal_class @ complement @ ( sk7 @ member ) )
!= ( sk7 @ singleton @ ( sk7 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35734,293]) ).
thf(35927,plain,
( ( universal_class @ complement @ ( sk7 @ member ) )
!= ( sk7 @ singleton @ ( sk7 @ member ) ) ),
inference(simp,[status(thm)],[35926]) ).
thf(36138,plain,
( ( ( universal_class @ complement )
!= ( sk7 @ singleton ) )
| ( sk7 != sk7 ) ),
inference(simp,[status(thm)],[35927]) ).
thf(36180,plain,
( ( universal_class @ complement )
!= ( sk7 @ singleton ) ),
inference(simp,[status(thm)],[36138]) ).
thf(12,axiom,
! [A: $i] :
( ( A @ function )
<=> ( ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
& ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',function_defn) ).
thf(103,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)],[12]) ).
thf(104,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)],[103]) ).
thf(105,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)],[104]) ).
thf(106,plain,
! [A: $i] :
( ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
| ~ ( A @ function ) ),
inference(cnfConj,[status(thm)],[105]) ).
thf(114,plain,
! [A: $i] :
( ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
| ~ ( A @ inductive ) ),
inference(cnfConj,[status(thm)],[112]) ).
thf(5680,plain,
! [A: $i] :
( ( ( sk7 @ inductive )
!= ( A @ inductive ) )
| ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[210,114]) ).
thf(5681,plain,
! [A: $i] :
( ( ( sk7 @ inductive )
!= ( A @ inductive ) )
| ( A @ ( A @ ( successor_relation @ image ) @ subclass ) ) ),
inference(simp,[status(thm)],[5680]) ).
thf(5682,plain,
sk7 @ ( sk7 @ ( successor_relation @ image ) @ subclass ),
inference(pattern_uni,[status(thm)],[5681:[bind(A,$thf( sk7 ))]]) ).
thf(31,axiom,
! [A: $i,B: $i] :
( ( ( B @ function )
& ( universal_class @ ( A @ member ) ) )
=> ( universal_class @ ( A @ ( B @ image ) @ member ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',replacement) ).
thf(215,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)],[31]) ).
thf(216,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( A @ ( B @ image ) @ member ) )
| ~ ( B @ function )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(cnf,[status(esa)],[215]) ).
thf(1784,plain,
( ( ( universal_class @ ( universal_class @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1458,49]) ).
thf(1785,plain,
( ( universal_class @ ( universal_class @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[1784]) ).
thf(1800,plain,
( ( universal_class != universal_class )
| ( ( universal_class @ sk5 )
!= sk2 ) ),
inference(simp,[status(thm)],[1785]) ).
thf(1811,plain,
( ( universal_class @ sk5 )
!= sk2 ),
inference(simp,[status(thm)],[1800]) ).
thf(175,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)],[174]) ).
thf(177,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ordered_pair ) @ second )
= B )
| ~ ( universal_class @ ( B @ member ) )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[175]) ).
thf(179,plain,
! [B: $i,A: $i] :
( ~ ( universal_class @ ( B @ member ) )
| ~ ( universal_class @ ( A @ member ) )
| ( ( B @ ( A @ ordered_pair ) @ second )
= B ) ),
inference(lifteq,[status(thm)],[177]) ).
thf(1375,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( null_class != null_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,51]) ).
thf(1376,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[1375]) ).
thf(1377,plain,
universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ),
inference(pattern_uni,[status(thm)],[1376:[bind(A,$thf( sk2 @ ( sk1 @ unordered_pair ) ))]]) ).
thf(41,axiom,
universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_relation) ).
thf(260,plain,
universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(1214,plain,
! [A: $i] :
( ( A
!= ( universal_class @ ( universal_class @ cross_product ) ) )
| ( null_class @ ( element_relation @ subclass ) )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,260]) ).
thf(1215,plain,
( ( null_class @ ( element_relation @ subclass ) )
| ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[1214:[bind(A,$thf( universal_class @ ( universal_class @ cross_product ) ))]]) ).
thf(218,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)],[217]) ).
thf(219,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)],[218]) ).
thf(221,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)],[219]) ).
thf(4362,plain,
! [A: $i] :
( ( ( sk8 @ function )
!= ( A @ function ) )
| ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[257,106]) ).
thf(4363,plain,
! [A: $i] :
( ( ( sk8 @ function )
!= ( A @ function ) )
| ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) ) ),
inference(simp,[status(thm)],[4362]) ).
thf(4364,plain,
universal_class @ ( universal_class @ cross_product ) @ ( sk8 @ subclass ),
inference(pattern_uni,[status(thm)],[4363:[bind(A,$thf( sk8 ))]]) ).
thf(3461,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ subclass ) )
!= ( sk2 @ ( sk7 @ subclass ) ) )
| ~ ( sk7 @ ( sk2 @ subclass ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[242,697]) ).
thf(3462,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ subclass ) )
!= ( sk2 @ ( sk7 @ subclass ) ) )
| ~ ( sk7 @ ( sk2 @ subclass ) ) ),
inference(simp,[status(thm)],[3461]) ).
thf(3471,plain,
! [A: $i] :
( ( sk2 != universal_class )
| ( A != sk7 )
| ~ ( sk7 @ ( sk2 @ subclass ) ) ),
inference(simp,[status(thm)],[3462]) ).
thf(3484,plain,
( ( sk2 != universal_class )
| ~ ( sk7 @ ( sk2 @ subclass ) ) ),
inference(simp,[status(thm)],[3471]) ).
thf(3933,plain,
! [A: $i] :
( ( ( A @ ( null_class @ subclass ) )
!= ( sk7 @ ( sk2 @ subclass ) ) )
| ( sk2 != universal_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3615,3484]) ).
thf(3934,plain,
! [A: $i] :
( ( ( A @ ( null_class @ subclass ) )
!= ( sk7 @ ( sk2 @ subclass ) ) )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[3933]) ).
thf(3956,plain,
! [A: $i] :
( ( A != sk7 )
| ( sk2 != null_class )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[3934]) ).
thf(3967,plain,
( ( sk2 != null_class )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[3956]) ).
thf(4200,plain,
! [A: $i] :
( ( A != sk2 )
| ( null_class != null_class )
| ( sk2 != universal_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,3967]) ).
thf(4201,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk2 != universal_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[4200]) ).
thf(4202,plain,
( ( sk2 != universal_class )
| ( universal_class @ ( sk2 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[4201:[bind(A,$thf( sk2 ))]]) ).
thf(17393,plain,
( ( ( universal_class @ ( sk2 @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true
| ( sk2 != universal_class ) ),
inference(paramod_ordered,[status(thm)],[4202,48]) ).
thf(17394,plain,
( ( ( universal_class @ ( sk2 @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[17393]) ).
thf(17437,plain,
( ( universal_class != universal_class )
| ( ( sk2 @ sk5 )
!= sk1 )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[17394]) ).
thf(17470,plain,
( ( ( sk2 @ sk5 )
!= sk1 )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[17437]) ).
thf(16,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/sandbox2/benchmark/theBenchmark.p',compose_defn2) ).
thf(127,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)],[16]) ).
thf(128,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)],[127]) ).
thf(129,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)],[128]) ).
thf(132,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)],[129]) ).
thf(133,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)],[132]) ).
thf(17717,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[13469,252]) ).
thf(17718,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[17717]) ).
thf(17719,plain,
~ ( sk2 @ ( sk1 @ unordered_pair ) @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) ),
inference(pattern_uni,[status(thm)],[17718:[bind(A,$thf( sk2 @ ( sk1 @ unordered_pair ) )),bind(B,$thf( sk2 @ ( sk1 @ unordered_pair ) @ sk5 ))]]) ).
thf(200,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
| ( A != C )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[196]) ).
thf(204,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
| ~ ( universal_class @ ( A @ member ) )
| ( A != C ) ),
inference(lifteq,[status(thm)],[200]) ).
thf(205,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( B @ member ) )
| ~ ( universal_class @ ( B @ member ) ) ),
inference(simp,[status(thm)],[204]) ).
thf(37083,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk7 @ member ) )
!= ( universal_class @ ( B @ member ) ) )
| ( B @ ( A @ unordered_pair ) @ ( B @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[209,205]) ).
thf(37084,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk7 @ member ) )
!= ( universal_class @ ( B @ member ) ) )
| ( B @ ( A @ unordered_pair ) @ ( B @ member ) ) ),
inference(simp,[status(thm)],[37083]) ).
thf(37085,plain,
! [A: $i] : ( sk7 @ ( A @ unordered_pair ) @ ( sk7 @ member ) ),
inference(pattern_uni,[status(thm)],[37084:[bind(A,$thf( A )),bind(B,$thf( sk7 ))]]) ).
thf(41956,plain,
! [A: $i] :
( ( ( sk7 @ ( A @ unordered_pair ) @ ( sk7 @ member ) )
!= ( sk7 @ singleton @ complement @ ( sk7 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37085,35970]) ).
thf(41957,plain,
! [A: $i] :
( ( sk7 @ ( A @ unordered_pair ) @ ( sk7 @ member ) )
!= ( sk7 @ singleton @ complement @ ( sk7 @ member ) ) ),
inference(simp,[status(thm)],[41956]) ).
thf(42155,plain,
! [A: $i] :
( ( ( sk7 @ ( A @ unordered_pair ) )
!= ( sk7 @ singleton @ complement ) )
| ( sk7 != sk7 ) ),
inference(simp,[status(thm)],[41957]) ).
thf(42246,plain,
! [A: $i] :
( ( sk7 @ ( A @ unordered_pair ) )
!= ( sk7 @ singleton @ complement ) ),
inference(simp,[status(thm)],[42155]) ).
thf(36218,plain,
! [A: $i] :
( ( A
!= ( sk7 @ singleton ) )
| ( null_class != null_class )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[147,36158]) ).
thf(36219,plain,
! [A: $i] :
( ( A
!= ( sk7 @ singleton ) )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[36218]) ).
thf(36220,plain,
sk7 @ singleton @ ( sk7 @ singleton @ sk5 @ member ),
inference(pattern_uni,[status(thm)],[36219:[bind(A,$thf( sk7 @ singleton ))]]) ).
thf(37891,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ singleton @ ( sk7 @ singleton @ sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[36220,252]) ).
thf(37892,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ singleton @ ( sk7 @ singleton @ sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[37891]) ).
thf(37893,plain,
~ ( sk7 @ singleton @ complement @ ( sk7 @ singleton @ sk5 @ member ) ),
inference(pattern_uni,[status(thm)],[37892:[bind(A,$thf( sk7 @ singleton )),bind(B,$thf( sk7 @ singleton @ sk5 ))]]) ).
thf(115,plain,
! [A: $i] :
( ( A @ inductive )
| ~ ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
| ~ ( A @ ( null_class @ member ) ) ),
inference(cnfConj,[status(thm)],[112]) ).
thf(116,plain,
! [A: $i] :
( ( A @ inductive )
| ~ ( A @ ( A @ ( successor_relation @ image ) @ subclass ) )
| ~ ( A @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[115]) ).
thf(37,axiom,
! [A: $i] :
( ( universal_class @ ( A @ member ) )
=> ( universal_class @ ( A @ power_class @ member ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',power_class) ).
thf(243,plain,
! [A: $i] :
( ( universal_class @ ( A @ member ) )
=> ( universal_class @ ( A @ power_class @ member ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(373,plain,
( ( ( sk7 @ inductive )
!= ( universal_class @ inductive ) )
| ( sk1 != null_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[210,367]) ).
thf(374,plain,
( ( ( sk7 @ inductive )
!= ( universal_class @ inductive ) )
| ( sk1 != null_class ) ),
inference(simp,[status(thm)],[373]) ).
thf(375,plain,
( ( sk7 != universal_class )
| ( sk1 != null_class ) ),
inference(simp,[status(thm)],[374]) ).
thf(12896,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk7 != universal_class )
| ( null_class != null_class )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[147,375]) ).
thf(12897,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk7 != universal_class )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[12896]) ).
thf(12898,plain,
( ( sk7 != universal_class )
| ( sk1 @ ( sk1 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[12897:[bind(A,$thf( sk1 ))]]) ).
thf(198,plain,
! [C: $i,B: $i,A: $i] :
( ( A = C )
| ( A = B )
| ~ ( C @ ( B @ unordered_pair ) @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[196]) ).
thf(201,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ unordered_pair ) @ ( A @ member ) )
| ( A = C )
| ( A = B ) ),
inference(lifteq,[status(thm)],[198]) ).
thf(107,plain,
! [A: $i] :
( ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
| ~ ( A @ function ) ),
inference(cnfConj,[status(thm)],[105]) ).
thf(4555,plain,
! [A: $i] :
( ( ( sk8 @ function )
!= ( A @ function ) )
| ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[257,107]) ).
thf(4556,plain,
! [A: $i] :
( ( ( sk8 @ function )
!= ( A @ function ) )
| ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) ) ),
inference(simp,[status(thm)],[4555]) ).
thf(4557,plain,
identity_relation @ ( sk8 @ inverse @ ( sk8 @ compose ) @ subclass ),
inference(pattern_uni,[status(thm)],[4556:[bind(A,$thf( sk8 ))]]) ).
thf(220,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)],[219]) ).
thf(6623,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)],[113,5233]) ).
thf(6624,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)],[6623]) ).
thf(6625,plain,
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ inductive ),
inference(pattern_uni,[status(thm)],[6624:[bind(A,$thf( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )),bind(B,$thf( null_class ))]]) ).
thf(13815,plain,
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ inductive ),
inference(rewrite,[status(thm)],[6625,12972]) ).
thf(16168,plain,
~ ( null_class @ sum_class @ sum_class @ inductive ),
inference(rewrite,[status(thm)],[13815,15425]) ).
thf(13000,plain,
! [A: $i] :
( ( A != sk1 )
| ( null_class != null_class )
| ~ ( universal_class @ inductive )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[147,367]) ).
thf(13001,plain,
! [A: $i] :
( ( A != sk1 )
| ~ ( universal_class @ inductive )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[13000]) ).
thf(13002,plain,
( ~ ( universal_class @ inductive )
| ( sk1 @ ( sk1 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[13001:[bind(A,$thf( sk1 ))]]) ).
thf(6,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( A @ ( B @ restrict ) ) )
= ( C @ ( A @ cross_product ) @ ( B @ intersection ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',restrict_defn) ).
thf(70,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)],[6]) ).
thf(20177,plain,
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[13469,17719]) ).
thf(20178,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[20177]) ).
thf(20342,plain,
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ complement )
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 )
!= ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 ) ) ),
inference(simp,[status(thm)],[20178]) ).
thf(20367,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ complement )
!= ( sk2 @ ( sk1 @ unordered_pair ) ) ),
inference(simp,[status(thm)],[20342]) ).
thf(9071,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( sk8 @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4364,9051]) ).
thf(9072,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( sk8 @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) ),
inference(simp,[status(thm)],[9071]) ).
thf(9126,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( sk8 != universal_class ) ),
inference(simp,[status(thm)],[9072]) ).
thf(45,axiom,
! [A: $i] :
( ( universal_class @ ( A @ member ) )
=> ( universal_class @ ( A @ sum_class @ member ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_class) ).
thf(275,plain,
! [A: $i] :
( ( universal_class @ ( A @ member ) )
=> ( universal_class @ ( A @ sum_class @ member ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(137,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ member ) )
| ~ ( B @ ( A @ intersection ) @ ( C @ member ) ) ),
inference(cnfConj,[status(thm)],[136]) ).
thf(197,plain,
! [C: $i,B: $i,A: $i] :
( ( universal_class @ ( A @ member ) )
| ~ ( C @ ( B @ unordered_pair ) @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[196]) ).
thf(289,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk7 @ member ) )
!= ( A @ complement @ ( B @ member ) ) )
| ~ ( A @ ( B @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[209,252]) ).
thf(290,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk7 @ member ) )
!= ( A @ complement @ ( B @ member ) ) )
| ~ ( A @ ( B @ member ) ) ),
inference(simp,[status(thm)],[289]) ).
thf(295,plain,
! [B: $i,A: $i] :
( ( ( A @ complement )
!= universal_class )
| ( sk7 != B )
| ~ ( A @ ( B @ member ) ) ),
inference(simp,[status(thm)],[290]) ).
thf(298,plain,
! [A: $i] :
( ( ( A @ complement )
!= universal_class )
| ~ ( A @ ( sk7 @ member ) ) ),
inference(simp,[status(thm)],[295]) ).
thf(35643,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk7 @ unordered_pair ) @ ( sk7 @ member ) )
!= ( B @ ( sk7 @ member ) ) )
| ( ( B @ complement )
!= universal_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35495,298]) ).
thf(35644,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk7 @ unordered_pair ) @ ( sk7 @ member ) )
!= ( B @ ( sk7 @ member ) ) )
| ( ( B @ complement )
!= universal_class ) ),
inference(simp,[status(thm)],[35643]) ).
thf(35645,plain,
! [A: $i] :
( ( A @ ( sk7 @ unordered_pair ) @ complement )
!= universal_class ),
inference(pattern_uni,[status(thm)],[35644:[bind(A,$thf( D )),bind(B,$thf( D @ ( sk7 @ unordered_pair ) ))]]) ).
thf(35820,plain,
! [A: $i] :
( ( A @ ( sk7 @ unordered_pair ) @ complement )
!= universal_class ),
inference(simp,[status(thm)],[35645]) ).
thf(310,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)],[193,252]) ).
thf(311,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)],[310]) ).
thf(312,plain,
! [B: $i,A: $i] :
~ ( universal_class @ complement @ ( B @ ( A @ unordered_pair ) @ member ) ),
inference(pattern_uni,[status(thm)],[311:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( universal_class )),bind(D,$thf( F @ ( E @ unordered_pair ) ))]]) ).
thf(324,plain,
! [B: $i,A: $i] :
~ ( universal_class @ complement @ ( B @ ( A @ unordered_pair ) @ member ) ),
inference(simp,[status(thm)],[312]) ).
thf(61,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subclass ) )
| ( A != B ) ),
inference(cnfConj,[status(thm)],[60]) ).
thf(64,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subclass ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[61]) ).
thf(65,plain,
! [A: $i] : ( A @ ( A @ subclass ) ),
inference(simp,[status(thm)],[64]) ).
thf(979,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)],[126,324]) ).
thf(980,plain,
! [A: $i] :
~ ( universal_class @ complement @ ( A @ singleton @ member ) ),
inference(pattern_uni,[status(thm)],[979:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(38562,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ subclass ) )
!= ( sk1 @ ( sk7 @ subclass ) ) )
| ~ ( sk7 @ ( sk1 @ subclass ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[211,673]) ).
thf(38563,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ subclass ) )
!= ( sk1 @ ( sk7 @ subclass ) ) )
| ~ ( sk7 @ ( sk1 @ subclass ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[38562]) ).
thf(38564,plain,
( ~ ( sk7 @ ( sk1 @ subclass ) )
| ~ ( sk1 @ inductive ) ),
inference(pattern_uni,[status(thm)],[38563:[bind(A,$thf( sk1 ))]]) ).
thf(108,plain,
! [A: $i] :
( ( A @ function )
| ~ ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
| ~ ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) ) ),
inference(cnfConj,[status(thm)],[105]) ).
thf(109,plain,
! [A: $i] :
( ( A @ function )
| ~ ( identity_relation @ ( A @ inverse @ ( A @ compose ) @ subclass ) )
| ~ ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) ) ),
inference(simp,[status(thm)],[108]) ).
thf(36559,plain,
( ( ( universal_class @ ( sk7 @ singleton @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[36246,48]) ).
thf(36560,plain,
( ( universal_class @ ( sk7 @ singleton @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[36559]) ).
thf(36666,plain,
( ( universal_class != universal_class )
| ( ( sk7 @ singleton @ sk5 )
!= sk1 ) ),
inference(simp,[status(thm)],[36560]) ).
thf(36696,plain,
( ( sk7 @ singleton @ sk5 )
!= sk1 ),
inference(simp,[status(thm)],[36666]) ).
thf(1790,plain,
! [A: $i] :
( ( A
!= ( universal_class @ sk5 ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,1458]) ).
thf(1791,plain,
( ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( universal_class @ sk5 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[1790:[bind(A,$thf( universal_class @ sk5 ))]]) ).
thf(44935,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ ( sk7 @ unordered_pair ) @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[39831,49]) ).
thf(44936,plain,
! [A: $i] :
( ( universal_class @ ( A @ ( sk7 @ unordered_pair ) @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[44935]) ).
thf(45083,plain,
! [A: $i] :
( ( universal_class != universal_class )
| ( ( A @ ( sk7 @ unordered_pair ) @ sk5 )
!= sk2 ) ),
inference(simp,[status(thm)],[44936]) ).
thf(45107,plain,
! [A: $i] :
( ( A @ ( sk7 @ unordered_pair ) @ sk5 )
!= sk2 ),
inference(simp,[status(thm)],[45083]) ).
thf(12793,plain,
! [A: $i] :
( ( A != sk2 )
| ( null_class != null_class )
| ( sk2 != universal_class )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[147,3967]) ).
thf(12794,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk2 != universal_class )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[12793]) ).
thf(12795,plain,
( ( sk2 != universal_class )
| ( sk2 @ ( sk2 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[12794:[bind(A,$thf( sk2 ))]]) ).
thf(6401,plain,
( ( ( universal_class @ ( sk2 @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true
| ~ ( universal_class @ inductive ) ),
inference(paramod_ordered,[status(thm)],[1240,49]) ).
thf(6402,plain,
( ( ( universal_class @ ( sk2 @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ ( universal_class @ inductive ) ),
inference(simp,[status(thm)],[6401]) ).
thf(6460,plain,
( ( universal_class != universal_class )
| ( ( sk2 @ sk5 )
!= sk2 )
| ~ ( universal_class @ inductive ) ),
inference(simp,[status(thm)],[6402]) ).
thf(6486,plain,
( ( ( sk2 @ sk5 )
!= sk2 )
| ~ ( universal_class @ inductive ) ),
inference(simp,[status(thm)],[6460]) ).
thf(6997,plain,
( ( ( sk7 @ inductive )
!= ( universal_class @ inductive ) )
| ( ( sk2 @ sk5 )
!= sk2 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[210,6486]) ).
thf(6998,plain,
( ( ( sk7 @ inductive )
!= ( universal_class @ inductive ) )
| ( ( sk2 @ sk5 )
!= sk2 ) ),
inference(simp,[status(thm)],[6997]) ).
thf(6999,plain,
( ( sk7 != universal_class )
| ( ( sk2 @ sk5 )
!= sk2 ) ),
inference(simp,[status(thm)],[6998]) ).
thf(3463,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ subclass ) )
!= ( sk7 @ ( sk2 @ subclass ) ) )
| ~ $true
| ~ ( sk2 @ ( sk7 @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[242,697]) ).
thf(3464,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ subclass ) )
!= ( sk7 @ ( sk2 @ subclass ) ) )
| ~ ( sk2 @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[3463]) ).
thf(3476,plain,
! [A: $i] :
( ( sk7 != universal_class )
| ( A != sk2 )
| ~ ( sk2 @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[3464]) ).
thf(3486,plain,
( ( sk7 != universal_class )
| ~ ( sk2 @ ( sk7 @ subclass ) ) ),
inference(simp,[status(thm)],[3476]) ).
thf(7067,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk2 @ ( sk7 @ subclass ) ) )
| ( sk7 != universal_class )
| ~ $true
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[121,3486]) ).
thf(7068,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk2 @ ( sk7 @ subclass ) ) )
| ( sk7 != universal_class )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[7067]) ).
thf(7069,plain,
( ( sk7 != universal_class )
| ~ ( sk2 @ power_class @ ( sk7 @ member ) ) ),
inference(pattern_uni,[status(thm)],[7068:[bind(A,$thf( sk7 )),bind(B,$thf( sk2 ))]]) ).
thf(172,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)],[169]) ).
thf(173,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)],[172]) ).
thf(1938,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ subclass ) )
!= ( sk1 @ ( sk7 @ subclass ) ) )
| ( sk7 != universal_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[242,1556]) ).
thf(1939,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ subclass ) )
!= ( sk1 @ ( sk7 @ subclass ) ) )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[1938]) ).
thf(1940,plain,
! [A: $i] :
( ( sk1 != universal_class )
| ( A != sk7 )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[1939]) ).
thf(1947,plain,
( ( sk1 != universal_class )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[1940]) ).
thf(35936,plain,
( ( ( null_class @ power_class @ ( sk7 @ member ) )
!= ( sk7 @ singleton @ ( sk7 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35734,11159]) ).
thf(35937,plain,
( ( null_class @ power_class @ ( sk7 @ member ) )
!= ( sk7 @ singleton @ ( sk7 @ member ) ) ),
inference(simp,[status(thm)],[35936]) ).
thf(36141,plain,
( ( ( null_class @ power_class )
!= ( sk7 @ singleton ) )
| ( sk7 != sk7 ) ),
inference(simp,[status(thm)],[35937]) ).
thf(36183,plain,
( ( null_class @ power_class )
!= ( sk7 @ singleton ) ),
inference(simp,[status(thm)],[36141]) ).
thf(7121,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk7 @ ( sk1 @ subclass ) ) )
| ( sk1 != universal_class )
| ~ $true
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[121,1561]) ).
thf(7122,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk7 @ ( sk1 @ subclass ) ) )
| ( sk1 != universal_class )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[7121]) ).
thf(7123,plain,
( ( sk1 != universal_class )
| ~ ( sk7 @ power_class @ ( sk1 @ member ) ) ),
inference(pattern_uni,[status(thm)],[7122:[bind(A,$thf( sk1 )),bind(B,$thf( sk7 ))]]) ).
thf(9066,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ $true
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[121,9051]) ).
thf(9067,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[9066]) ).
thf(9068,plain,
~ ( null_class @ power_class @ ( universal_class @ member ) ),
inference(pattern_uni,[status(thm)],[9067:[bind(A,$thf( universal_class )),bind(B,$thf( null_class ))]]) ).
thf(981,plain,
! [A: $i] :
( ( ( A @ ( A @ unordered_pair ) )
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( ( A @ singleton )
!= null_class ) ),
inference(paramod_ordered,[status(thm)],[126,51]) ).
thf(984,plain,
! [A: $i] :
( ( A != sk2 )
| ( A != sk1 )
| ( ( A @ singleton )
!= null_class ) ),
inference(simp,[status(thm)],[981]) ).
thf(985,plain,
( ( sk2 != sk1 )
| ( ( sk1 @ singleton )
!= null_class ) ),
inference(simp,[status(thm)],[984]) ).
thf(10532,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ member ) )
!= ( null_class @ sum_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)],[80,8031]) ).
thf(10533,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk3 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[10532]) ).
thf(10534,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(pattern_uni,[status(thm)],[10533:[bind(A,$thf( E )),bind(B,$thf( null_class @ sum_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 @ sum_class @ sk3 ) ))]]) ).
thf(10615,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(simp,[status(thm)],[10534]) ).
thf(23337,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(rewrite,[status(thm)],[10615,19977]) ).
thf(5765,plain,
! [A: $i] :
( ( A != successor_relation )
| ( sk7 @ ( sk7 @ ( null_class @ image ) @ subclass ) )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,5682]) ).
thf(5766,plain,
( ( sk7 @ ( sk7 @ ( null_class @ image ) @ subclass ) )
| ( universal_class @ ( successor_relation @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[5765:[bind(A,$thf( successor_relation ))]]) ).
thf(1771,plain,
( ( ( universal_class @ ( universal_class @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1458,48]) ).
thf(1772,plain,
( ( universal_class @ ( universal_class @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[1771]) ).
thf(1806,plain,
( ( universal_class != universal_class )
| ( ( universal_class @ sk5 )
!= sk1 ) ),
inference(simp,[status(thm)],[1772]) ).
thf(1814,plain,
( ( universal_class @ sk5 )
!= sk1 ),
inference(simp,[status(thm)],[1806]) ).
thf(6664,plain,
! [A: $i] :
( ( ( universal_class @ ( sk7 @ sk5 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1184,5233]) ).
thf(6665,plain,
! [A: $i] :
( ( universal_class @ ( sk7 @ sk5 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[6664]) ).
thf(6669,plain,
! [A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= universal_class )
| ( ( sk7 @ sk5 )
!= A ) ),
inference(simp,[status(thm)],[6665]) ).
thf(6695,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= universal_class ),
inference(simp,[status(thm)],[6669]) ).
thf(13803,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= universal_class ),
inference(rewrite,[status(thm)],[6695,12972]) ).
thf(16115,plain,
( ( null_class @ sum_class @ sum_class )
!= universal_class ),
inference(rewrite,[status(thm)],[13803,15425]) ).
thf(2296,plain,
( ( ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1377,49]) ).
thf(2297,plain,
( ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[2296]) ).
thf(2325,plain,
( ( universal_class != universal_class )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 )
!= sk2 ) ),
inference(simp,[status(thm)],[2297]) ).
thf(2338,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 )
!= sk2 ),
inference(simp,[status(thm)],[2325]) ).
thf(11330,plain,
( ( ( sk7 @ ( sk7 @ ( null_class @ sk4 ) @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11186,48]) ).
thf(11331,plain,
( ( sk7 @ ( sk7 @ ( null_class @ sk4 ) @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[11330]) ).
thf(11379,plain,
( ( sk7 != universal_class )
| ( ( sk7 @ ( null_class @ sk4 ) )
!= sk1 ) ),
inference(simp,[status(thm)],[11331]) ).
thf(145,plain,
! [A: $i] :
( ( A @ ( A @ sk5 @ disjoint ) )
| ( A = null_class ) ),
inference(cnfConj,[status(thm)],[142]) ).
thf(148,plain,
! [A: $i] :
( ( A @ ( A @ sk5 @ disjoint ) )
| ( A = null_class ) ),
inference(lifteq,[status(thm)],[145]) ).
thf(14156,plain,
! [A: $i] :
( ( A != sk8 )
| ( null_class @ function )
| ( A @ ( A @ sk5 @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[148,257]) ).
thf(14157,plain,
( ( null_class @ function )
| ( sk8 @ ( sk8 @ sk5 @ disjoint ) ) ),
inference(pattern_uni,[status(thm)],[14156:[bind(A,$thf( sk8 ))]]) ).
thf(165,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)],[162]) ).
thf(166,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)],[165]) ).
thf(24,axiom,
! [A: $i] : ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( A @ rotate @ subclass ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rotate) ).
thf(180,plain,
! [A: $i] : ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( A @ rotate @ subclass ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(19,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ cross_product ) @ ( C @ member ) )
=> ( C
= ( C @ second @ ( C @ first @ ordered_pair ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cross_product) ).
thf(149,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)],[19]) ).
thf(16638,plain,
( ( ( universal_class @ ( sk1 @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true
| ( sk1 != universal_class ) ),
inference(paramod_ordered,[status(thm)],[3907,48]) ).
thf(16639,plain,
( ( ( universal_class @ ( sk1 @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ( sk1 != universal_class ) ),
inference(simp,[status(thm)],[16638]) ).
thf(16698,plain,
( ( universal_class != universal_class )
| ( ( sk1 @ sk5 )
!= sk1 )
| ( sk1 != universal_class ) ),
inference(simp,[status(thm)],[16639]) ).
thf(16726,plain,
( ( ( sk1 @ sk5 )
!= sk1 )
| ( sk1 != universal_class ) ),
inference(simp,[status(thm)],[16698]) ).
thf(42125,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ ( A @ unordered_pair ) @ ( sk7 @ member ) )
!= ( null_class @ ( B @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37085,214]) ).
thf(42126,plain,
! [B: $i,A: $i] :
( ( sk7 @ ( A @ unordered_pair ) @ ( sk7 @ member ) )
!= ( null_class @ ( B @ member ) ) ),
inference(simp,[status(thm)],[42125]) ).
thf(42164,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ ( A @ unordered_pair ) )
!= null_class )
| ( sk7 != B ) ),
inference(simp,[status(thm)],[42126]) ).
thf(42252,plain,
! [A: $i] :
( ( sk7 @ ( A @ unordered_pair ) )
!= null_class ),
inference(simp,[status(thm)],[42164]) ).
thf(42328,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk7 @ ( B @ unordered_pair ) ) )
| ( null_class != null_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,42252]) ).
thf(42329,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk7 @ ( B @ unordered_pair ) ) )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[42328]) ).
thf(42330,plain,
! [A: $i] : ( universal_class @ ( sk7 @ ( A @ unordered_pair ) @ sk5 @ member ) ),
inference(pattern_uni,[status(thm)],[42329:[bind(A,$thf( sk7 @ ( C @ unordered_pair ) )),bind(B,$thf( C ))]]) ).
thf(42351,plain,
! [A: $i] : ( universal_class @ ( sk7 @ ( A @ unordered_pair ) @ sk5 @ member ) ),
inference(simp,[status(thm)],[42330]) ).
thf(10505,plain,
! [A: $i] :
( ( ( sk7 @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[361,8031]) ).
thf(10506,plain,
! [A: $i] :
( ( sk7 @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[10505]) ).
thf(10591,plain,
! [A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk7 )
| ( null_class != A ) ),
inference(simp,[status(thm)],[10506]) ).
thf(10631,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk7 ),
inference(simp,[status(thm)],[10591]) ).
thf(13834,plain,
( ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )
!= sk7 ),
inference(rewrite,[status(thm)],[10631,12972]) ).
thf(18663,plain,
( ( null_class @ sum_class @ sum_class @ sum_class )
!= sk7 ),
inference(rewrite,[status(thm)],[13834,16945]) ).
thf(188,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)],[184]) ).
thf(190,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)],[188]) ).
thf(191,plain,
! [A: $i] :
( ( successor_relation @ ( A @ successor @ ( A @ ordered_pair ) @ member ) )
| ~ ( universal_class @ ( A @ successor @ member ) )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[190]) ).
thf(9077,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[260,9051]) ).
thf(9078,plain,
( ( universal_class @ ( universal_class @ cross_product ) @ ( element_relation @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) ),
inference(simp,[status(thm)],[9077]) ).
thf(9142,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( element_relation != universal_class ) ),
inference(simp,[status(thm)],[9078]) ).
thf(12321,plain,
! [A: $i] :
( ( A != sk7 )
| ( null_class != null_class )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[147,730]) ).
thf(12322,plain,
! [A: $i] :
( ( A != sk7 )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[12321]) ).
thf(12323,plain,
sk7 @ ( sk7 @ sk5 @ member ),
inference(pattern_uni,[status(thm)],[12322:[bind(A,$thf( sk7 ))]]) ).
thf(13950,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ ( sk7 @ sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[12323,252]) ).
thf(13951,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ ( sk7 @ sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[13950]) ).
thf(13952,plain,
~ ( sk7 @ complement @ ( sk7 @ sk5 @ member ) ),
inference(pattern_uni,[status(thm)],[13951:[bind(A,$thf( sk7 )),bind(B,$thf( sk7 @ sk5 ))]]) ).
thf(15602,plain,
( ( ( sk7 @ complement @ ( sk7 @ sk5 @ member ) )
!= ( universal_class @ ( sk7 @ sk5 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1184,13952]) ).
thf(15603,plain,
( ( sk7 @ complement @ ( sk7 @ sk5 @ member ) )
!= ( universal_class @ ( sk7 @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[15602]) ).
thf(15630,plain,
( ( ( sk7 @ complement )
!= universal_class )
| ( ( sk7 @ sk5 )
!= ( sk7 @ sk5 ) ) ),
inference(simp,[status(thm)],[15603]) ).
thf(15641,plain,
( ( sk7 @ complement )
!= universal_class ),
inference(simp,[status(thm)],[15630]) ).
thf(53,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ apply ) )
= ( B @ singleton @ ( A @ image ) @ sum_class ) ),
inference(cnf,[status(esa)],[52]) ).
thf(54,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ apply ) )
= ( B @ singleton @ ( A @ image ) @ sum_class ) ),
inference(lifteq,[status(thm)],[53]) ).
thf(41984,plain,
! [A: $i] :
( ( ( sk7 @ ( A @ unordered_pair ) @ ( sk7 @ member ) )
!= ( null_class @ power_class @ ( sk7 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37085,11159]) ).
thf(41985,plain,
! [A: $i] :
( ( sk7 @ ( A @ unordered_pair ) @ ( sk7 @ member ) )
!= ( null_class @ power_class @ ( sk7 @ member ) ) ),
inference(simp,[status(thm)],[41984]) ).
thf(42206,plain,
! [A: $i] :
( ( ( sk7 @ ( A @ unordered_pair ) )
!= ( null_class @ power_class ) )
| ( sk7 != sk7 ) ),
inference(simp,[status(thm)],[41985]) ).
thf(42285,plain,
! [A: $i] :
( ( sk7 @ ( A @ unordered_pair ) )
!= ( null_class @ power_class ) ),
inference(simp,[status(thm)],[42206]) ).
thf(181,plain,
! [A: $i] : ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( A @ rotate @ subclass ) ),
inference(cnf,[status(esa)],[180]) ).
thf(8142,plain,
( ( ( universal_class @ ( sk1 @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true
| ~ ( universal_class @ inductive ) ),
inference(paramod_ordered,[status(thm)],[1328,48]) ).
thf(8143,plain,
( ( ( universal_class @ ( sk1 @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ ( universal_class @ inductive ) ),
inference(simp,[status(thm)],[8142]) ).
thf(8196,plain,
( ( universal_class != universal_class )
| ( ( sk1 @ sk5 )
!= sk1 )
| ~ ( universal_class @ inductive ) ),
inference(simp,[status(thm)],[8143]) ).
thf(8202,plain,
( ( ( sk1 @ sk5 )
!= sk1 )
| ~ ( universal_class @ inductive ) ),
inference(simp,[status(thm)],[8196]) ).
thf(13174,plain,
! [A: $i] :
( ( A != sk2 )
| ( null_class != null_class )
| ~ ( universal_class @ inductive )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[147,370]) ).
thf(13175,plain,
! [A: $i] :
( ( A != sk2 )
| ~ ( universal_class @ inductive )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[13174]) ).
thf(13176,plain,
( ~ ( universal_class @ inductive )
| ( sk2 @ ( sk2 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[13175:[bind(A,$thf( sk2 ))]]) ).
thf(36239,plain,
! [A: $i] :
( ( A
!= ( sk7 @ singleton ) )
| ( null_class != null_class )
| ( A @ ( A @ sk5 @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[148,36158]) ).
thf(36240,plain,
! [A: $i] :
( ( A
!= ( sk7 @ singleton ) )
| ( A @ ( A @ sk5 @ disjoint ) ) ),
inference(simp,[status(thm)],[36239]) ).
thf(36241,plain,
sk7 @ singleton @ ( sk7 @ singleton @ sk5 @ disjoint ),
inference(pattern_uni,[status(thm)],[36240:[bind(A,$thf( sk7 @ singleton ))]]) ).
thf(9,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/sandbox2/benchmark/theBenchmark.p',domain_of) ).
thf(83,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)],[9]) ).
thf(84,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)],[83]) ).
thf(85,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)],[84]) ).
thf(86,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( B @ member ) )
| ~ ( A @ domain_of @ ( B @ member ) ) ),
inference(cnfConj,[status(thm)],[85]) ).
thf(153,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)],[152]) ).
thf(154,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( D @ disjoint ) )
| ( E @ ( D @ ( E @ sk6 ) @ member ) ) )
& ( ( E @ ( D @ disjoint ) )
| ( D @ ( D @ ( E @ sk6 ) @ member ) ) )
& ( ~ ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ disjoint ) ) ) ),
inference(cnf,[status(esa)],[153]) ).
thf(157,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ disjoint ) )
| ( B @ ( A @ ( B @ sk6 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[154]) ).
thf(159,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ disjoint ) )
| ( B @ ( A @ ( B @ sk6 ) @ member ) ) ),
inference(simp,[status(thm)],[157]) ).
thf(7083,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk1 @ ( sk7 @ subclass ) ) )
| ( sk7 != universal_class )
| ~ $true
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[121,1556]) ).
thf(7084,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk1 @ ( sk7 @ subclass ) ) )
| ( sk7 != universal_class )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[7083]) ).
thf(7085,plain,
( ( sk7 != universal_class )
| ~ ( sk1 @ power_class @ ( sk7 @ member ) ) ),
inference(pattern_uni,[status(thm)],[7084:[bind(A,$thf( sk7 )),bind(B,$thf( sk1 ))]]) ).
thf(25154,plain,
( ( ( sk1 @ power_class @ ( sk7 @ member ) )
!= ( universal_class @ ( sk7 @ member ) ) )
| ( sk7 != universal_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[209,7085]) ).
thf(25155,plain,
( ( ( sk1 @ power_class @ ( sk7 @ member ) )
!= ( universal_class @ ( sk7 @ member ) ) )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[25154]) ).
thf(25235,plain,
( ( ( sk1 @ power_class )
!= universal_class )
| ( sk7 != sk7 )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[25155]) ).
thf(25248,plain,
( ( ( sk1 @ power_class )
!= universal_class )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[25235]) ).
thf(2257,plain,
( ( ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1377,48]) ).
thf(2258,plain,
( ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[2257]) ).
thf(2333,plain,
( ( universal_class != universal_class )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 )
!= sk1 ) ),
inference(simp,[status(thm)],[2258]) ).
thf(2346,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 )
!= sk1 ),
inference(simp,[status(thm)],[2333]) ).
thf(229,plain,
! [B: $i,A: $i] :
( ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
| ~ ( B @ ( A @ member ) )
| ~ ( universal_class @ ( B @ member ) ) ),
inference(cnfConj,[status(thm)],[226]) ).
thf(230,plain,
! [B: $i,A: $i] :
( ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) )
| ~ ( B @ ( A @ member ) )
| ~ ( universal_class @ ( B @ member ) ) ),
inference(simp,[status(thm)],[229]) ).
thf(1678,plain,
( ( ( universal_class @ ( sk7 @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1184,48]) ).
thf(1679,plain,
( ( universal_class @ ( sk7 @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[1678]) ).
thf(1710,plain,
( ( universal_class != universal_class )
| ( ( sk7 @ sk5 )
!= sk1 ) ),
inference(simp,[status(thm)],[1679]) ).
thf(1722,plain,
( ( sk7 @ sk5 )
!= sk1 ),
inference(simp,[status(thm)],[1710]) ).
thf(38,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ image ) )
= ( universal_class @ ( A @ ( B @ restrict ) ) @ range_of ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',image_defn) ).
thf(245,plain,
! [A: $i,B: $i] :
( ( A @ ( B @ image ) )
= ( universal_class @ ( A @ ( B @ restrict ) ) @ range_of ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(300,plain,
( ( ( universal_class @ complement @ ( sk7 @ member ) )
!= ( universal_class @ ( sk7 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[209,293]) ).
thf(301,plain,
( ( universal_class @ complement @ ( sk7 @ member ) )
!= ( universal_class @ ( sk7 @ member ) ) ),
inference(simp,[status(thm)],[300]) ).
thf(302,plain,
( ( ( universal_class @ complement )
!= universal_class )
| ( sk7 != sk7 ) ),
inference(simp,[status(thm)],[301]) ).
thf(303,plain,
( ( universal_class @ complement )
!= universal_class ),
inference(simp,[status(thm)],[302]) ).
thf(139,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ intersection ) @ ( C @ member ) )
| ~ ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(cnfConj,[status(thm)],[136]) ).
thf(140,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ intersection ) @ ( C @ member ) )
| ~ ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[139]) ).
thf(35,axiom,
! [A: $i,B: $i] : ( universal_class @ ( universal_class @ cross_product ) @ ( A @ ( B @ compose ) @ subclass ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',compose_defn1) ).
thf(239,plain,
! [A: $i,B: $i] : ( universal_class @ ( universal_class @ cross_product ) @ ( A @ ( B @ compose ) @ subclass ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(240,plain,
! [B: $i,A: $i] : ( universal_class @ ( universal_class @ cross_product ) @ ( A @ ( B @ compose ) @ subclass ) ),
inference(cnf,[status(esa)],[239]) ).
thf(42019,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk7 @ ( A @ unordered_pair ) @ ( sk7 @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ complement @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[37085,252]) ).
thf(42020,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk7 @ ( A @ unordered_pair ) @ ( sk7 @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ ( B @ complement @ ( C @ member ) ) ),
inference(simp,[status(thm)],[42019]) ).
thf(42021,plain,
! [A: $i] :
~ ( sk7 @ ( A @ unordered_pair ) @ complement @ ( sk7 @ member ) ),
inference(pattern_uni,[status(thm)],[42020:[bind(A,$thf( D )),bind(B,$thf( sk7 @ ( D @ unordered_pair ) )),bind(C,$thf( sk7 ))]]) ).
thf(42228,plain,
! [A: $i] :
~ ( sk7 @ ( A @ unordered_pair ) @ complement @ ( sk7 @ member ) ),
inference(simp,[status(thm)],[42021]) ).
thf(13811,plain,
! [A: $i] :
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ),
inference(rewrite,[status(thm)],[6709,12972]) ).
thf(21259,plain,
! [A: $i] :
~ ( null_class @ sum_class @ ( A @ member ) ),
inference(rewrite,[status(thm)],[13811,19977]) ).
thf(2287,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[1377,252]) ).
thf(2288,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[2287]) ).
thf(2289,plain,
~ ( universal_class @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) ),
inference(pattern_uni,[status(thm)],[2288:[bind(A,$thf( universal_class )),bind(B,$thf( sk2 @ ( sk1 @ unordered_pair ) @ sk5 ))]]) ).
thf(1291,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk7 != universal_class )
| ( null_class != null_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,375]) ).
thf(1292,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk7 != universal_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[1291]) ).
thf(1293,plain,
( ( sk7 != universal_class )
| ( universal_class @ ( sk1 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[1292:[bind(A,$thf( sk1 ))]]) ).
thf(7021,plain,
( ( ( sk7 @ inductive )
!= ( universal_class @ inductive ) )
| ( ( sk2 @ sk5 )
!= sk1 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[210,6487]) ).
thf(7022,plain,
( ( ( sk7 @ inductive )
!= ( universal_class @ inductive ) )
| ( ( sk2 @ sk5 )
!= sk1 ) ),
inference(simp,[status(thm)],[7021]) ).
thf(7023,plain,
( ( sk7 != universal_class )
| ( ( sk2 @ sk5 )
!= sk1 ) ),
inference(simp,[status(thm)],[7022]) ).
thf(155,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ disjoint ) ) ),
inference(cnfConj,[status(thm)],[154]) ).
thf(313,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( B @ ( A @ unordered_pair ) @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[193,49]) ).
thf(314,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( B @ ( A @ unordered_pair ) @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[313]) ).
thf(319,plain,
! [B: $i,A: $i] :
( ( universal_class != universal_class )
| ( ( B @ ( A @ unordered_pair ) )
!= sk2 ) ),
inference(simp,[status(thm)],[314]) ).
thf(326,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) )
!= sk2 ),
inference(simp,[status(thm)],[319]) ).
thf(982,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ unordered_pair ) )
!= ( C @ ( B @ unordered_pair ) ) )
| ( ( A @ singleton )
!= sk2 ) ),
inference(paramod_ordered,[status(thm)],[126,326]) ).
thf(983,plain,
! [A: $i] :
( ( A @ singleton )
!= sk2 ),
inference(pattern_uni,[status(thm)],[982:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(130,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)],[129]) ).
thf(35586,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ unordered_pair ) @ ( sk7 @ member ) )
!= ( null_class @ power_class @ ( sk7 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35495,11159]) ).
thf(35587,plain,
! [A: $i] :
( ( A @ ( sk7 @ unordered_pair ) @ ( sk7 @ member ) )
!= ( null_class @ power_class @ ( sk7 @ member ) ) ),
inference(simp,[status(thm)],[35586]) ).
thf(35776,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ unordered_pair ) )
!= ( null_class @ power_class ) )
| ( sk7 != sk7 ) ),
inference(simp,[status(thm)],[35587]) ).
thf(35853,plain,
! [A: $i] :
( ( A @ ( sk7 @ unordered_pair ) )
!= ( null_class @ power_class ) ),
inference(simp,[status(thm)],[35776]) ).
thf(222,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)],[219]) ).
thf(223,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)],[222]) ).
thf(17756,plain,
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( universal_class @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[13469,2289]) ).
thf(17757,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( universal_class @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[17756]) ).
thf(17851,plain,
( ( ( sk2 @ ( sk1 @ unordered_pair ) )
!= ( universal_class @ complement ) )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 )
!= ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 ) ) ),
inference(simp,[status(thm)],[17757]) ).
thf(17874,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) )
!= ( universal_class @ complement ) ),
inference(simp,[status(thm)],[17851]) ).
thf(87,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) )
!= null_class )
| ~ ( A @ domain_of @ ( B @ member ) ) ),
inference(cnfConj,[status(thm)],[85]) ).
thf(89,plain,
! [B: $i,A: $i] :
( ~ ( A @ domain_of @ ( B @ member ) )
| ( ( universal_class @ ( B @ singleton @ ( A @ restrict ) ) )
!= null_class ) ),
inference(lifteq,[status(thm)],[87]) ).
thf(71,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ restrict ) ) )
= ( C @ ( A @ cross_product ) @ ( B @ intersection ) ) ),
inference(cnf,[status(esa)],[70]) ).
thf(72,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ restrict ) ) )
= ( C @ ( A @ cross_product ) @ ( B @ intersection ) ) ),
inference(lifteq,[status(thm)],[71]) ).
thf(2614,plain,
! [B: $i,A: $i] :
( ~ ( A @ domain_of @ ( B @ member ) )
| ( ( universal_class @ ( B @ singleton @ cross_product ) @ ( A @ intersection ) )
!= null_class ) ),
inference(rewrite,[status(thm)],[89,72]) ).
thf(793,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( sk7 @ complement @ ( null_class @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[113,756]) ).
thf(794,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( sk7 @ complement @ ( null_class @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[793]) ).
thf(795,plain,
~ ( sk7 @ complement @ inductive ),
inference(pattern_uni,[status(thm)],[794:[bind(A,$thf( sk7 @ complement ))]]) ).
thf(5771,plain,
( ( ( sk7 @ ( sk7 @ ( successor_relation @ image ) @ subclass ) )
!= ( sk7 @ ( sk1 @ subclass ) ) )
| ( sk1 != universal_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5682,1561]) ).
thf(5772,plain,
( ( ( sk7 @ ( sk7 @ ( successor_relation @ image ) @ subclass ) )
!= ( sk7 @ ( sk1 @ subclass ) ) )
| ( sk1 != universal_class ) ),
inference(simp,[status(thm)],[5771]) ).
thf(5773,plain,
( ( sk7 != sk7 )
| ( ( sk7 @ ( successor_relation @ image ) )
!= sk1 )
| ( sk1 != universal_class ) ),
inference(simp,[status(thm)],[5772]) ).
thf(5785,plain,
( ( ( sk7 @ ( successor_relation @ image ) )
!= sk1 )
| ( sk1 != universal_class ) ),
inference(simp,[status(thm)],[5773]) ).
thf(122,plain,
! [B: $i,A: $i] :
( ( B @ power_class @ ( A @ member ) )
| ~ ( B @ ( A @ subclass ) )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[119]) ).
thf(123,plain,
! [B: $i,A: $i] :
( ( B @ power_class @ ( A @ member ) )
| ~ ( B @ ( A @ subclass ) )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[122]) ).
thf(10524,plain,
! [B: $i,A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[113,8031]) ).
thf(10525,plain,
! [B: $i,A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( B @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[10524]) ).
thf(10526,plain,
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ inductive ),
inference(pattern_uni,[status(thm)],[10525:[bind(A,$thf( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class )),bind(B,$thf( null_class ))]]) ).
thf(13831,plain,
~ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ inductive ),
inference(rewrite,[status(thm)],[10526,12972]) ).
thf(18000,plain,
~ ( null_class @ sum_class @ sum_class @ sum_class @ inductive ),
inference(rewrite,[status(thm)],[13831,16945]) ).
thf(95,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ subclass ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(4516,plain,
! [A: $i] :
( ( A
!= ( universal_class @ ( universal_class @ cross_product ) ) )
| ( null_class @ ( sk8 @ subclass ) )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,4364]) ).
thf(4517,plain,
( ( null_class @ ( sk8 @ subclass ) )
| ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[4516:[bind(A,$thf( universal_class @ ( universal_class @ cross_product ) ))]]) ).
thf(4629,plain,
! [A: $i] :
( ( ( A @ inverse )
!= ( sk8 @ inverse ) )
| ( identity_relation @ ( universal_class @ ( A @ cross_product ) @ flip @ domain_of @ ( sk8 @ compose ) @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[102,4557]) ).
thf(4630,plain,
identity_relation @ ( universal_class @ ( sk8 @ cross_product ) @ flip @ domain_of @ ( sk8 @ compose ) @ subclass ),
inference(pattern_uni,[status(thm)],[4629:[bind(A,$thf( sk8 ))]]) ).
thf(43,axiom,
! [A: $i] :
( ( identity_relation @ ( A @ member ) )
<=> ? [B: $i] :
( ( A
= ( B @ ( B @ ordered_pair ) ) )
& ( universal_class @ ( B @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_relation) ).
thf(263,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(156,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ disjoint ) )
| ( A @ ( A @ ( B @ sk6 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[154]) ).
thf(158,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ disjoint ) )
| ( A @ ( A @ ( B @ sk6 ) @ member ) ) ),
inference(simp,[status(thm)],[156]) ).
thf(16337,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk6 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ~ $true
| ( B @ ( A @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[158,214]) ).
thf(16338,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk6 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ( B @ ( A @ disjoint ) ) ),
inference(simp,[status(thm)],[16337]) ).
thf(16339,plain,
! [A: $i] : ( A @ ( null_class @ disjoint ) ),
inference(pattern_uni,[status(thm)],[16338:[bind(A,$thf( null_class )),bind(B,$thf( D )),bind(C,$thf( null_class @ ( D @ sk6 ) ))]]) ).
thf(16389,plain,
! [A: $i] : ( A @ ( null_class @ disjoint ) ),
inference(simp,[status(thm)],[16339]) ).
thf(38559,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ subclass ) )
!= ( sk1 @ ( sk7 @ subclass ) ) )
| ( sk1 != null_class )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[211,3659]) ).
thf(38560,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ subclass ) )
!= ( sk1 @ ( sk7 @ subclass ) ) )
| ( sk1 != null_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[38559]) ).
thf(38561,plain,
( ( sk1 != null_class )
| ~ ( sk1 @ inductive ) ),
inference(pattern_uni,[status(thm)],[38560:[bind(A,$thf( sk1 ))]]) ).
thf(22930,plain,
( ( ( sk2 @ power_class @ ( sk7 @ member ) )
!= ( universal_class @ ( sk7 @ member ) ) )
| ( sk7 != universal_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[209,7069]) ).
thf(22931,plain,
( ( ( sk2 @ power_class @ ( sk7 @ member ) )
!= ( universal_class @ ( sk7 @ member ) ) )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[22930]) ).
thf(22995,plain,
( ( ( sk2 @ power_class )
!= universal_class )
| ( sk7 != sk7 )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[22931]) ).
thf(23031,plain,
( ( ( sk2 @ power_class )
!= universal_class )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[22995]) ).
thf(11295,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ ( sk7 @ ( null_class @ sk4 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[11186,252]) ).
thf(11296,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ ( sk7 @ ( null_class @ sk4 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[11295]) ).
thf(11297,plain,
~ ( sk7 @ complement @ ( sk7 @ ( null_class @ sk4 ) @ member ) ),
inference(pattern_uni,[status(thm)],[11296:[bind(A,$thf( sk7 )),bind(B,$thf( sk7 @ ( null_class @ sk4 ) ))]]) ).
thf(10527,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ~ $true
| ( B @ ( A @ subclass ) ) ),
inference(paramod_ordered,[status(thm)],[98,8031]) ).
thf(10528,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ( B @ ( A @ subclass ) ) ),
inference(simp,[status(thm)],[10527]) ).
thf(10529,plain,
! [A: $i] : ( A @ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ subclass ) ),
inference(pattern_uni,[status(thm)],[10528:[bind(A,$thf( null_class @ sum_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 @ sum_class @ ( D @ sk4 ) ))]]) ).
thf(10614,plain,
! [A: $i] : ( A @ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ subclass ) ),
inference(simp,[status(thm)],[10529]) ).
thf(22680,plain,
! [A: $i] : ( A @ ( null_class @ sum_class @ sum_class @ sum_class @ subclass ) ),
inference(rewrite,[status(thm)],[10614,19977]) ).
thf(9091,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ $true
| ( A @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[98,9051]) ).
thf(9092,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[9091]) ).
thf(9093,plain,
universal_class @ ( universal_class @ ( null_class @ sk4 ) @ member ),
inference(pattern_uni,[status(thm)],[9092:[bind(A,$thf( universal_class )),bind(B,$thf( null_class ))]]) ).
thf(14128,plain,
! [A: $i] :
( ( A != sk7 )
| ( null_class != null_class )
| ( A @ ( A @ sk5 @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[148,730]) ).
thf(14129,plain,
! [A: $i] :
( ( A != sk7 )
| ( A @ ( A @ sk5 @ disjoint ) ) ),
inference(simp,[status(thm)],[14128]) ).
thf(14130,plain,
sk7 @ ( sk7 @ sk5 @ disjoint ),
inference(pattern_uni,[status(thm)],[14129:[bind(A,$thf( sk7 ))]]) ).
thf(1261,plain,
! [A: $i] :
( ( A
!= ( universal_class @ ( universal_class @ cross_product ) ) )
| ( null_class @ ( successor_relation @ subclass ) )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,206]) ).
thf(1262,plain,
( ( null_class @ ( successor_relation @ subclass ) )
| ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[1261:[bind(A,$thf( universal_class @ ( universal_class @ cross_product ) ))]]) ).
thf(1691,plain,
( ( ( universal_class @ ( sk7 @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1184,49]) ).
thf(1692,plain,
( ( universal_class @ ( sk7 @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[1691]) ).
thf(1704,plain,
( ( universal_class != universal_class )
| ( ( sk7 @ sk5 )
!= sk2 ) ),
inference(simp,[status(thm)],[1692]) ).
thf(1717,plain,
( ( sk7 @ sk5 )
!= sk2 ),
inference(simp,[status(thm)],[1704]) ).
thf(38542,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ subclass ) )
!= ( sk2 @ ( sk7 @ subclass ) ) )
| ( sk7 != universal_class )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[211,3486]) ).
thf(38543,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ subclass ) )
!= ( sk2 @ ( sk7 @ subclass ) ) )
| ( sk7 != universal_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[38542]) ).
thf(38544,plain,
( ( sk7 != universal_class )
| ~ ( sk2 @ inductive ) ),
inference(pattern_uni,[status(thm)],[38543:[bind(A,$thf( sk2 ))]]) ).
thf(3952,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ subclass ) )
!= ( sk7 @ ( sk2 @ subclass ) ) )
| ( sk2 != universal_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[242,3484]) ).
thf(3953,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ subclass ) )
!= ( sk7 @ ( sk2 @ subclass ) ) )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[3952]) ).
thf(3959,plain,
! [A: $i] :
( ( sk7 != universal_class )
| ( A != sk2 )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[3953]) ).
thf(3970,plain,
( ( sk7 != universal_class )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[3959]) ).
thf(14154,plain,
! [A: $i] :
( ( null_class != null_class )
| ( A != universal_class )
| ( A @ ( A @ sk5 @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[148,288]) ).
thf(14155,plain,
! [A: $i] :
( ( A != universal_class )
| ( A @ ( A @ sk5 @ disjoint ) ) ),
inference(pattern_uni,[status(thm)],[14154:[]]) ).
thf(14960,plain,
universal_class @ ( universal_class @ sk5 @ disjoint ),
inference(simp,[status(thm)],[14155]) ).
thf(304,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( B @ ( A @ unordered_pair ) @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[193,48]) ).
thf(305,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( B @ ( A @ unordered_pair ) @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[304]) ).
thf(320,plain,
! [B: $i,A: $i] :
( ( universal_class != universal_class )
| ( ( B @ ( A @ unordered_pair ) )
!= sk1 ) ),
inference(simp,[status(thm)],[305]) ).
thf(322,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) )
!= sk1 ),
inference(simp,[status(thm)],[320]) ).
thf(977,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ unordered_pair ) )
!= ( C @ ( B @ unordered_pair ) ) )
| ( ( A @ singleton )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[126,322]) ).
thf(978,plain,
! [A: $i] :
( ( A @ singleton )
!= sk1 ),
inference(pattern_uni,[status(thm)],[977:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(44968,plain,
! [A: $i] :
( ( ( universal_class @ ( A @ ( sk7 @ unordered_pair ) @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[39831,48]) ).
thf(44969,plain,
! [A: $i] :
( ( universal_class @ ( A @ ( sk7 @ unordered_pair ) @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[44968]) ).
thf(45082,plain,
! [A: $i] :
( ( universal_class != universal_class )
| ( ( A @ ( sk7 @ unordered_pair ) @ sk5 )
!= sk1 ) ),
inference(simp,[status(thm)],[44969]) ).
thf(45106,plain,
! [A: $i] :
( ( A @ ( sk7 @ unordered_pair ) @ sk5 )
!= sk1 ),
inference(simp,[status(thm)],[45082]) ).
thf(9312,plain,
( ( ( universal_class @ ( universal_class @ ( null_class @ sk4 ) @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9093,49]) ).
thf(9313,plain,
( ( universal_class @ ( universal_class @ ( null_class @ sk4 ) @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[9312]) ).
thf(9382,plain,
( ( universal_class != universal_class )
| ( ( universal_class @ ( null_class @ sk4 ) )
!= sk2 ) ),
inference(simp,[status(thm)],[9313]) ).
thf(9406,plain,
( ( universal_class @ ( null_class @ sk4 ) )
!= sk2 ),
inference(simp,[status(thm)],[9382]) ).
thf(37488,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ unordered_pair ) @ ( sk7 @ member ) )
!= ( sk7 @ singleton @ complement @ ( sk7 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35495,35970]) ).
thf(37489,plain,
! [A: $i] :
( ( A @ ( sk7 @ unordered_pair ) @ ( sk7 @ member ) )
!= ( sk7 @ singleton @ complement @ ( sk7 @ member ) ) ),
inference(simp,[status(thm)],[37488]) ).
thf(37622,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ unordered_pair ) )
!= ( sk7 @ singleton @ complement ) )
| ( sk7 != sk7 ) ),
inference(simp,[status(thm)],[37489]) ).
thf(37688,plain,
! [A: $i] :
( ( A @ ( sk7 @ unordered_pair ) )
!= ( sk7 @ singleton @ complement ) ),
inference(simp,[status(thm)],[37622]) ).
thf(38532,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ subclass ) )
!= ( sk2 @ ( sk7 @ subclass ) ) )
| ~ ( sk7 @ ( sk2 @ subclass ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[211,697]) ).
thf(38533,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ subclass ) )
!= ( sk2 @ ( sk7 @ subclass ) ) )
| ~ ( sk7 @ ( sk2 @ subclass ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[38532]) ).
thf(38534,plain,
( ~ ( sk7 @ ( sk2 @ subclass ) )
| ~ ( sk2 @ inductive ) ),
inference(pattern_uni,[status(thm)],[38533:[bind(A,$thf( sk2 ))]]) ).
thf(4276,plain,
! [A: $i] :
( ( A
!= ( universal_class @ sk5 @ sk5 ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,1791]) ).
thf(4277,plain,
! [A: $i] :
( ( A
!= ( universal_class @ sk5 @ sk5 ) )
| ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[4276]) ).
thf(4278,plain,
( ( universal_class @ ( null_class @ member ) )
| ( universal_class @ ( universal_class @ sk5 @ sk5 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[4277:[bind(A,$thf( universal_class @ sk5 @ sk5 ))]]) ).
thf(97,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subclass ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[94]) ).
thf(99,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subclass ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[97]) ).
thf(13209,plain,
! [A: $i] :
( ( A != sk1 )
| ( null_class != null_class )
| ( sk1 != universal_class )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[147,3655]) ).
thf(13210,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk1 != universal_class )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[13209]) ).
thf(13211,plain,
( ( sk1 != universal_class )
| ( sk1 @ ( sk1 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[13210:[bind(A,$thf( sk1 ))]]) ).
thf(36530,plain,
( ( ( universal_class @ ( sk7 @ singleton @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[36246,49]) ).
thf(36531,plain,
( ( universal_class @ ( sk7 @ singleton @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) ),
inference(simp,[status(thm)],[36530]) ).
thf(36669,plain,
( ( universal_class != universal_class )
| ( ( sk7 @ singleton @ sk5 )
!= sk2 ) ),
inference(simp,[status(thm)],[36531]) ).
thf(36699,plain,
( ( sk7 @ singleton @ sk5 )
!= sk2 ),
inference(simp,[status(thm)],[36669]) ).
thf(35991,plain,
! [A: $i] :
( ( ( sk7 @ singleton @ ( sk7 @ member ) )
!= ( A @ ( sk7 @ member ) ) )
| ( ( A @ complement )
!= universal_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35734,298]) ).
thf(35992,plain,
! [A: $i] :
( ( ( sk7 @ singleton @ ( sk7 @ member ) )
!= ( A @ ( sk7 @ member ) ) )
| ( ( A @ complement )
!= universal_class ) ),
inference(simp,[status(thm)],[35991]) ).
thf(35993,plain,
( ( sk7 @ singleton @ complement )
!= universal_class ),
inference(pattern_uni,[status(thm)],[35992:[bind(A,$thf( sk7 @ singleton ))]]) ).
thf(14800,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( null_class != null_class )
| ( A @ ( A @ sk5 @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[148,51]) ).
thf(14801,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( A @ ( A @ sk5 @ disjoint ) ) ),
inference(simp,[status(thm)],[14800]) ).
thf(14802,plain,
sk2 @ ( sk1 @ unordered_pair ) @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ disjoint ),
inference(pattern_uni,[status(thm)],[14801:[bind(A,$thf( sk2 @ ( sk1 @ unordered_pair ) ))]]) ).
thf(7478,plain,
( ( ( universal_class @ ( sk1 @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true
| ( sk7 != universal_class ) ),
inference(paramod_ordered,[status(thm)],[1293,48]) ).
thf(7479,plain,
( ( ( universal_class @ ( sk1 @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[7478]) ).
thf(7528,plain,
( ( universal_class != universal_class )
| ( ( sk1 @ sk5 )
!= sk1 )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[7479]) ).
thf(7552,plain,
( ( ( sk1 @ sk5 )
!= sk1 )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[7528]) ).
thf(7466,plain,
( ( ( universal_class @ ( sk1 @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true
| ( sk7 != universal_class ) ),
inference(paramod_ordered,[status(thm)],[1293,49]) ).
thf(7467,plain,
( ( ( universal_class @ ( sk1 @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[7466]) ).
thf(7521,plain,
( ( universal_class != universal_class )
| ( ( sk1 @ sk5 )
!= sk2 )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[7467]) ).
thf(7547,plain,
( ( ( sk1 @ sk5 )
!= sk2 )
| ( sk7 != universal_class ) ),
inference(simp,[status(thm)],[7521]) ).
thf(186,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( B @ member ) )
| ~ ( successor_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[184]) ).
thf(7920,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk4 ) @ 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)],[98,6709]) ).
thf(7921,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk4 ) @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ ( C @ member ) ) )
| ( B @ ( A @ subclass ) ) ),
inference(simp,[status(thm)],[7920]) ).
thf(7922,plain,
! [A: $i] : ( A @ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ subclass ) ),
inference(pattern_uni,[status(thm)],[7921:[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 @ sk4 ) ))]]) ).
thf(8030,plain,
! [A: $i] : ( A @ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ subclass ) ),
inference(simp,[status(thm)],[7922]) ).
thf(13802,plain,
! [A: $i] : ( A @ ( null_class @ sum_class @ sum_class @ sum_class @ sum_class @ sum_class @ subclass ) ),
inference(rewrite,[status(thm)],[8030,12972]) ).
thf(21140,plain,
! [A: $i] : ( A @ ( null_class @ sum_class @ subclass ) ),
inference(rewrite,[status(thm)],[13802,19977]) ).
thf(171,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)],[169]) ).
thf(7112,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk7 @ ( sk2 @ subclass ) ) )
| ( sk2 != universal_class )
| ~ $true
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(paramod_ordered,[status(thm)],[121,3484]) ).
thf(7113,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subclass ) )
!= ( sk7 @ ( sk2 @ subclass ) ) )
| ( sk2 != universal_class )
| ~ ( B @ power_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[7112]) ).
thf(7114,plain,
( ( sk2 != universal_class )
| ~ ( sk7 @ power_class @ ( sk2 @ member ) ) ),
inference(pattern_uni,[status(thm)],[7113:[bind(A,$thf( sk2 )),bind(B,$thf( sk7 ))]]) ).
thf(2473,plain,
! [A: $i] :
( ( ( A @ ( A @ unordered_pair ) )
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( ( A @ singleton @ sk5 )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[126,2346]) ).
thf(2474,plain,
! [A: $i] :
( ( A != sk2 )
| ( A != sk1 )
| ( ( A @ singleton @ sk5 )
!= sk1 ) ),
inference(simp,[status(thm)],[2473]) ).
thf(2475,plain,
( ( sk2 != sk1 )
| ( ( sk1 @ singleton @ sk5 )
!= sk1 ) ),
inference(simp,[status(thm)],[2474]) ).
thf(19783,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ ordered_pair ) @ ordered_pair ) @ member ) )
!= ( null_class @ ( E @ member ) ) )
| ~ $true
| ~ ( A @ rotate @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[171,214]) ).
thf(19784,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ ordered_pair ) @ ordered_pair ) @ member ) )
!= ( null_class @ ( E @ member ) ) )
| ~ ( A @ rotate @ ( D @ ( C @ ( B @ ordered_pair ) @ ordered_pair ) @ member ) ) ),
inference(simp,[status(thm)],[19783]) ).
thf(19785,plain,
! [C: $i,B: $i,A: $i] :
~ ( null_class @ rotate @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ),
inference(pattern_uni,[status(thm)],[19784:[bind(A,$thf( null_class )),bind(B,$thf( G )),bind(C,$thf( H )),bind(D,$thf( I )),bind(E,$thf( G @ ( I @ ( H @ ordered_pair ) @ ordered_pair ) ))]]) ).
thf(19901,plain,
! [C: $i,B: $i,A: $i] :
~ ( null_class @ rotate @ ( C @ ( B @ ( A @ ordered_pair ) @ ordered_pair ) @ member ) ),
inference(simp,[status(thm)],[19785]) ).
thf(88,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)],[85]) ).
thf(90,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)],[88]) ).
thf(91,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)],[90]) ).
thf(2779,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)],[91,72]) ).
thf(81,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ sum_class @ ( A @ member ) )
| ~ ( B @ ( C @ member ) )
| ~ ( C @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[78]) ).
thf(82,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ sum_class @ ( A @ member ) )
| ~ ( B @ ( C @ member ) )
| ~ ( C @ ( A @ member ) ) ),
inference(simp,[status(thm)],[81]) ).
thf(17366,plain,
( ( ( universal_class @ ( sk2 @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ~ $true
| ( sk2 != universal_class ) ),
inference(paramod_ordered,[status(thm)],[4202,49]) ).
thf(17367,plain,
( ( ( universal_class @ ( sk2 @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ member ) ) )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[17366]) ).
thf(17448,plain,
( ( universal_class != universal_class )
| ( ( sk2 @ sk5 )
!= sk2 )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[17367]) ).
thf(17476,plain,
( ( ( sk2 @ sk5 )
!= sk2 )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[17448]) ).
thf(759,plain,
( ( ( universal_class @ ( sk2 @ member ) )
!= ( sk7 @ ( null_class @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[361,49]) ).
thf(760,plain,
( ( universal_class @ ( sk2 @ member ) )
!= ( sk7 @ ( null_class @ member ) ) ),
inference(simp,[status(thm)],[759]) ).
thf(763,plain,
( ( sk7 != universal_class )
| ( sk2 != null_class ) ),
inference(simp,[status(thm)],[760]) ).
thf(44,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( B @ singleton @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair_defn) ).
thf(272,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(12366,plain,
! [A: $i] :
( ( A != sk8 )
| ( null_class @ function )
| ( A @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[147,257]) ).
thf(12367,plain,
( ( null_class @ function )
| ( sk8 @ ( sk8 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[12366:[bind(A,$thf( sk8 ))]]) ).
thf(150,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( C @ second @ ( C @ first @ ordered_pair ) ) )
| ~ ( B @ ( A @ cross_product ) @ ( C @ member ) ) ),
inference(cnf,[status(esa)],[149]) ).
thf(151,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ cross_product ) @ ( C @ member ) )
| ( ( C @ second @ ( C @ first @ ordered_pair ) )
= C ) ),
inference(lifteq,[status(thm)],[150]) ).
thf(2372,plain,
! [A: $i] :
( ( ( A @ ( A @ unordered_pair ) )
!= ( sk2 @ ( sk1 @ unordered_pair ) ) )
| ( ( A @ singleton @ sk5 )
!= sk2 ) ),
inference(paramod_ordered,[status(thm)],[126,2338]) ).
thf(2373,plain,
! [A: $i] :
( ( A != sk2 )
| ( A != sk1 )
| ( ( A @ singleton @ sk5 )
!= sk2 ) ),
inference(simp,[status(thm)],[2372]) ).
thf(2374,plain,
( ( sk2 != sk1 )
| ( ( sk1 @ singleton @ sk5 )
!= sk2 ) ),
inference(simp,[status(thm)],[2373]) ).
thf(3808,plain,
! [A: $i] :
( ( ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1377,3039]) ).
thf(3809,plain,
! [A: $i] :
( ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( null_class @ sum_class @ sum_class @ sum_class @ ( A @ member ) ) ),
inference(simp,[status(thm)],[3808]) ).
thf(3855,plain,
! [A: $i] :
( ( ( null_class @ sum_class @ sum_class @ sum_class )
!= universal_class )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 )
!= A ) ),
inference(simp,[status(thm)],[3809]) ).
thf(3872,plain,
( ( null_class @ sum_class @ sum_class @ sum_class )
!= universal_class ),
inference(simp,[status(thm)],[3855]) ).
thf(13826,plain,
( ( null_class @ sum_class @ sum_class )
!= universal_class ),
inference(rewrite,[status(thm)],[3872,12972]) ).
thf(14070,plain,
( ( null_class @ sum_class )
!= universal_class ),
inference(rewrite,[status(thm)],[13826,12972]) ).
thf(41972,plain,
! [A: $i] :
( ( ( sk7 @ ( A @ unordered_pair ) @ ( sk7 @ member ) )
!= ( universal_class @ complement @ ( sk7 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37085,293]) ).
thf(41973,plain,
! [A: $i] :
( ( sk7 @ ( A @ unordered_pair ) @ ( sk7 @ member ) )
!= ( universal_class @ complement @ ( sk7 @ member ) ) ),
inference(simp,[status(thm)],[41972]) ).
thf(42176,plain,
! [A: $i] :
( ( ( sk7 @ ( A @ unordered_pair ) )
!= ( universal_class @ complement ) )
| ( sk7 != sk7 ) ),
inference(simp,[status(thm)],[41973]) ).
thf(42262,plain,
! [A: $i] :
( ( sk7 @ ( A @ unordered_pair ) )
!= ( universal_class @ complement ) ),
inference(simp,[status(thm)],[42176]) ).
thf(262,plain,
! [A: $i] : ( universal_class @ ( universal_class @ ( universal_class @ cross_product ) @ cross_product ) @ ( A @ flip @ subclass ) ),
inference(cnf,[status(esa)],[261]) ).
thf(9064,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ $true
| ~ ( A @ function ) ),
inference(paramod_ordered,[status(thm)],[106,9051]) ).
thf(9065,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) @ ( A @ subclass ) )
!= ( null_class @ ( universal_class @ subclass ) ) )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[9064]) ).
thf(9139,plain,
! [A: $i] :
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ( A != universal_class )
| ~ ( A @ function ) ),
inference(simp,[status(thm)],[9065]) ).
thf(9156,plain,
( ( ( universal_class @ ( universal_class @ cross_product ) )
!= null_class )
| ~ ( universal_class @ function ) ),
inference(simp,[status(thm)],[9139]) ).
thf(2146,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( universal_class @ complement @ ( sk7 @ sk5 @ member ) ) )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[113,1686]) ).
thf(2147,plain,
! [A: $i] :
( ( ( A @ ( null_class @ member ) )
!= ( universal_class @ complement @ ( sk7 @ sk5 @ member ) ) )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[2146]) ).
thf(2173,plain,
! [A: $i] :
( ( A
!= ( universal_class @ complement ) )
| ( ( sk7 @ sk5 )
!= null_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[2147]) ).
thf(2186,plain,
( ( ( sk7 @ sk5 )
!= null_class )
| ~ ( universal_class @ complement @ inductive ) ),
inference(simp,[status(thm)],[2173]) ).
thf(35576,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ unordered_pair ) @ ( sk7 @ member ) )
!= ( universal_class @ complement @ ( sk7 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35495,293]) ).
thf(35577,plain,
! [A: $i] :
( ( A @ ( sk7 @ unordered_pair ) @ ( sk7 @ member ) )
!= ( universal_class @ complement @ ( sk7 @ member ) ) ),
inference(simp,[status(thm)],[35576]) ).
thf(35779,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ unordered_pair ) )
!= ( universal_class @ complement ) )
| ( sk7 != sk7 ) ),
inference(simp,[status(thm)],[35577]) ).
thf(35854,plain,
! [A: $i] :
( ( A @ ( sk7 @ unordered_pair ) )
!= ( universal_class @ complement ) ),
inference(simp,[status(thm)],[35779]) ).
thf(38545,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ subclass ) )
!= ( sk2 @ ( sk7 @ subclass ) ) )
| ( sk2 != null_class )
| ~ $true
| ~ ( A @ inductive ) ),
inference(paramod_ordered,[status(thm)],[211,3660]) ).
thf(38546,plain,
! [A: $i] :
( ( ( A @ ( sk7 @ subclass ) )
!= ( sk2 @ ( sk7 @ subclass ) ) )
| ( sk2 != null_class )
| ~ ( A @ inductive ) ),
inference(simp,[status(thm)],[38545]) ).
thf(38547,plain,
( ( sk2 != null_class )
| ~ ( sk2 @ inductive ) ),
inference(pattern_uni,[status(thm)],[38546:[bind(A,$thf( sk2 ))]]) ).
thf(79,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk3 ) @ ( A @ member ) )
| ~ ( B @ sum_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[78]) ).
thf(16838,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk6 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ~ $true
| ( B @ ( A @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[159,214]) ).
thf(16839,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ sk6 ) @ member ) )
!= ( null_class @ ( C @ member ) ) )
| ( B @ ( A @ disjoint ) ) ),
inference(simp,[status(thm)],[16838]) ).
thf(16840,plain,
! [A: $i] : ( null_class @ ( A @ disjoint ) ),
inference(pattern_uni,[status(thm)],[16839:[bind(A,$thf( E )),bind(B,$thf( null_class )),bind(C,$thf( E @ ( null_class @ sk6 ) ))]]) ).
thf(16888,plain,
! [A: $i] : ( null_class @ ( A @ disjoint ) ),
inference(simp,[status(thm)],[16840]) ).
thf(3819,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)],[113,3039]) ).
thf(3820,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)],[3819]) ).
thf(3821,plain,
~ ( null_class @ sum_class @ sum_class @ sum_class @ inductive ),
inference(pattern_uni,[status(thm)],[3820:[bind(A,$thf( null_class @ sum_class @ sum_class @ sum_class )),bind(B,$thf( null_class ))]]) ).
thf(13805,plain,
~ ( null_class @ sum_class @ sum_class @ inductive ),
inference(rewrite,[status(thm)],[3821,12972]) ).
thf(13877,plain,
~ ( null_class @ sum_class @ inductive ),
inference(rewrite,[status(thm)],[13805,12972]) ).
thf(1350,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk7 != universal_class )
| ( null_class != null_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(paramod_ordered,[status(thm)],[146,763]) ).
thf(1351,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk7 != universal_class )
| ( universal_class @ ( A @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[1350]) ).
thf(1352,plain,
( ( sk7 != universal_class )
| ( universal_class @ ( sk2 @ sk5 @ member ) ) ),
inference(pattern_uni,[status(thm)],[1351:[bind(A,$thf( sk2 ))]]) ).
thf(42045,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ ( A @ unordered_pair ) @ ( sk7 @ member ) )
!= ( B @ ( sk7 @ member ) ) )
| ( ( B @ complement )
!= universal_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37085,298]) ).
thf(42046,plain,
! [B: $i,A: $i] :
( ( ( sk7 @ ( A @ unordered_pair ) @ ( sk7 @ member ) )
!= ( B @ ( sk7 @ member ) ) )
| ( ( B @ complement )
!= universal_class ) ),
inference(simp,[status(thm)],[42045]) ).
thf(42047,plain,
! [A: $i] :
( ( sk7 @ ( A @ unordered_pair ) @ complement )
!= universal_class ),
inference(pattern_uni,[status(thm)],[42046:[bind(A,$thf( C )),bind(B,$thf( sk7 @ ( C @ unordered_pair ) ))]]) ).
thf(42229,plain,
! [A: $i] :
( ( sk7 @ ( A @ unordered_pair ) @ complement )
!= universal_class ),
inference(simp,[status(thm)],[42047]) ).
thf(9329,plain,
( ( ( universal_class @ ( universal_class @ ( null_class @ sk4 ) @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9093,48]) ).
thf(9330,plain,
( ( universal_class @ ( universal_class @ ( null_class @ sk4 ) @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) ),
inference(simp,[status(thm)],[9329]) ).
thf(9374,plain,
( ( universal_class != universal_class )
| ( ( universal_class @ ( null_class @ sk4 ) )
!= sk1 ) ),
inference(simp,[status(thm)],[9330]) ).
thf(9402,plain,
( ( universal_class @ ( null_class @ sk4 ) )
!= sk1 ),
inference(simp,[status(thm)],[9374]) ).
thf(131,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)],[129]) ).
thf(163,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)],[162]) ).
thf(176,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ordered_pair ) @ first )
= A )
| ~ ( universal_class @ ( B @ member ) )
| ~ ( universal_class @ ( A @ member ) ) ),
inference(cnfConj,[status(thm)],[175]) ).
thf(178,plain,
! [B: $i,A: $i] :
( ~ ( universal_class @ ( B @ member ) )
| ~ ( universal_class @ ( A @ member ) )
| ( ( B @ ( A @ ordered_pair ) @ first )
= A ) ),
inference(lifteq,[status(thm)],[176]) ).
thf(1859,plain,
( ( ( universal_class @ ( sk8 @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ~ $true
| ( null_class @ function ) ),
inference(paramod_ordered,[status(thm)],[1251,48]) ).
thf(1860,plain,
( ( ( universal_class @ ( sk8 @ sk5 @ member ) )
!= ( universal_class @ ( sk1 @ member ) ) )
| ( null_class @ function ) ),
inference(simp,[status(thm)],[1859]) ).
thf(1893,plain,
( ( universal_class != universal_class )
| ( ( sk8 @ sk5 )
!= sk1 )
| ( null_class @ function ) ),
inference(simp,[status(thm)],[1860]) ).
thf(1902,plain,
( ( ( sk8 @ sk5 )
!= sk1 )
| ( null_class @ function ) ),
inference(simp,[status(thm)],[1893]) ).
thf(227,plain,
! [B: $i,A: $i] :
( ( universal_class @ ( B @ member ) )
| ~ ( element_relation @ ( B @ ( A @ ordered_pair ) @ member ) ) ),
inference(cnfConj,[status(thm)],[226]) ).
thf(5761,plain,
( ( ( sk7 @ ( sk7 @ ( successor_relation @ image ) @ subclass ) )
!= ( sk7 @ ( sk2 @ subclass ) ) )
| ( sk2 != universal_class )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5682,3484]) ).
thf(5762,plain,
( ( ( sk7 @ ( sk7 @ ( successor_relation @ image ) @ subclass ) )
!= ( sk7 @ ( sk2 @ subclass ) ) )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[5761]) ).
thf(5782,plain,
( ( sk7 != sk7 )
| ( ( sk7 @ ( successor_relation @ image ) )
!= sk2 )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[5762]) ).
thf(5788,plain,
( ( ( sk7 @ ( successor_relation @ image ) )
!= sk2 )
| ( sk2 != universal_class ) ),
inference(simp,[status(thm)],[5782]) ).
thf(9295,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( universal_class @ ( null_class @ sk4 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ $true
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(paramod_ordered,[status(thm)],[9093,252]) ).
thf(9296,plain,
! [B: $i,A: $i] :
( ( ( universal_class @ ( universal_class @ ( null_class @ sk4 ) @ member ) )
!= ( A @ ( B @ member ) ) )
| ~ ( A @ complement @ ( B @ member ) ) ),
inference(simp,[status(thm)],[9295]) ).
thf(9297,plain,
~ ( universal_class @ complement @ ( universal_class @ ( null_class @ sk4 ) @ member ) ),
inference(pattern_uni,[status(thm)],[9296:[bind(A,$thf( universal_class )),bind(B,$thf( universal_class @ ( null_class @ sk4 ) ))]]) ).
thf(13922,plain,
( ( ( universal_class @ complement @ ( sk7 @ sk5 @ member ) )
!= ( sk7 @ ( sk7 @ sk5 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[12323,1686]) ).
thf(13923,plain,
( ( universal_class @ complement @ ( sk7 @ sk5 @ member ) )
!= ( sk7 @ ( sk7 @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[13922]) ).
thf(14026,plain,
( ( ( universal_class @ complement )
!= sk7 )
| ( ( sk7 @ sk5 )
!= ( sk7 @ sk5 ) ) ),
inference(simp,[status(thm)],[13923]) ).
thf(14055,plain,
( ( universal_class @ complement )
!= sk7 ),
inference(simp,[status(thm)],[14026]) ).
thf(20199,plain,
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1377,17719]) ).
thf(20200,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ complement @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) )
!= ( universal_class @ ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 @ member ) ) ),
inference(simp,[status(thm)],[20199]) ).
thf(20311,plain,
( ( ( sk2 @ ( sk1 @ unordered_pair ) @ complement )
!= universal_class )
| ( ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 )
!= ( sk2 @ ( sk1 @ unordered_pair ) @ sk5 ) ) ),
inference(simp,[status(thm)],[20200]) ).
thf(20357,plain,
( ( sk2 @ ( sk1 @ unordered_pair ) @ complement )
!= universal_class ),
inference(simp,[status(thm)],[20311]) ).
thf(50895,plain,
$false,
inference(e,[status(thm)],[69,138,11186,16444,234,7072,11385,1686,170,23865,2248,120,9135,730,217,36487,37685,8204,1458,185,13469,39831,288,26186,257,3370,17924,174,52,38552,110,1907,802,35819,22254,46,152,228,57,6487,261,11986,16721,15028,189,924,164,756,36180,211,106,121,35970,5682,216,1811,179,147,1377,1215,221,293,4364,17470,133,17719,35495,42246,37893,206,116,243,11159,12898,248,117,201,4557,220,102,16168,13002,260,160,35734,70,20367,192,9126,275,137,92,252,197,36220,35820,324,224,361,65,1328,980,141,38564,697,3615,109,36696,124,193,1791,212,45107,12795,6999,7069,173,1947,36183,3967,7123,9068,3486,985,23337,5766,134,73,1814,1779,205,16115,36246,2338,11379,19977,6486,14157,298,3660,1251,1698,166,148,180,149,16726,42351,375,18663,191,9142,36158,286,13952,15641,54,42285,16945,49,181,8202,13176,36241,86,159,25248,2346,113,230,76,1722,245,98,303,367,103,140,240,42228,21259,1556,2289,1293,7023,155,983,130,35853,223,167,241,17874,80,37085,2614,795,5785,209,123,194,18000,255,48,7085,95,3659,4517,4630,263,16389,38561,673,182,23031,11297,127,22680,9093,14130,370,3655,1262,72,1717,38544,1240,3970,14960,4202,978,45106,9406,37688,38534,4278,99,13211,36699,203,35993,14802,7552,7099,231,976,7547,3484,158,186,21140,171,7114,55,114,75,2475,58,19901,2779,82,207,12323,17476,763,272,214,287,12367,15425,151,2374,3907,146,12972,51,14070,42252,42262,11140,262,9051,9156,210,126,2186,1561,35854,38547,326,107,239,242,358,79,16888,13877,1352,35849,42229,9402,131,163,178,1902,227,322,83,1184,5788,215,9297,14055,20357,100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET071+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.14/0.41 % Computer : n013.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sat Sep 26 07:01:52 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.88/0.99 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.45/1.23 % [INFO] Parsing done (240ms).
% 1.45/1.25 % [INFO] Running in sequential loop mode.
% 2.20/1.65 % [INFO] eprover registered as external prover.
% 2.20/1.66 % [INFO] Scanning for conjecture ...
% 2.42/1.77 % [INFO] Found a conjecture (or negated_conjecture) and 43 axioms. Running axiom selection ...
% 2.59/1.86 % [INFO] Axiom selection finished. Selected 43 axioms (removed 0 axioms).
% 2.83/1.94 % [INFO] Problem is first-order (TPTP FOF).
% 2.83/1.95 % [INFO] Type checking passed.
% 2.83/1.95 % [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 ...
% 64.00/18.72 % External prover 'e' found a proof!
% 64.00/18.72 % [INFO] Killing All external provers ...
% 64.00/18.73 % Time passed: 18176ms (effective reasoning time: 17477ms)
% 64.00/18.73 % 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)>
% 64.00/18.73 % 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
% 64.00/18.73 % No. of inferences in proof: 966
% 64.00/18.73 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 18176 ms resp. 17477 ms w/o parsing
% 80.04/19.01 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 80.04/19.02 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------