%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEU216+3 : TPTP v9.3.1. Released v3.2.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 : n008.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:38:03 AM UTC 2026
% Result : Theorem 158.06s 43.74s
% Output : Refutation 161.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 57
% Syntax : Number of formulae : 979 ( 286 unt; 0 typ; 16 def)
% Number of atoms : 3085 (1061 equ; 0 cnn)
% Maximal formula atoms : 34 ( 3 avg)
% Number of connectives : 9117 (1554 ~;1355 |; 141 &;5971 @)
% ( 8 <=>; 88 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 37 ( 34 usr; 13 con; 0-2 aty)
% Number of variables : 1431 ( 11 ^;1373 !; 31 ?;1431 :)
% ( 0 !>; 0 ?*; 0 @-; 16 @+)
% Comments :
%------------------------------------------------------------------------------
thf(relation_decl,type,
relation: $i > $o ).
thf(function_decl,type,
function: $i > $o ).
thf(identity_relation_decl,type,
identity_relation: $i > $i ).
thf(relation_dom_decl,type,
relation_dom: $i > $i ).
thf(in_decl,type,
in: $i > $i > $o ).
thf(apply_decl,type,
apply: $i > $i > $i ).
thf(unordered_pair_decl,type,
unordered_pair: $i > $i > $i ).
thf(subset_decl,type,
subset: $i > $i > $o ).
thf(empty_decl,type,
empty: $i > $o ).
thf(singleton_decl,type,
singleton: $i > $i ).
thf(empty_set_decl,type,
empty_set: $i ).
thf(element_decl,type,
element: $i > $i > $o ).
thf(powerset_decl,type,
powerset: $i > $i ).
thf(ordered_pair_decl,type,
ordered_pair: $i > $i > $i ).
thf(relation_empty_yielding_decl,type,
relation_empty_yielding: $i > $o ).
thf(relation_rng_decl,type,
relation_rng: $i > $i ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $o ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk5_decl,type,
sk5: $i ).
thf(sk6_decl,type,
sk6: $i ).
thf(sk7_decl,type,
sk7: $i > $i ).
thf(sk8_decl,type,
sk8: $i > $i ).
thf(sk9_decl,type,
sk9: $i > $i ).
thf(sk10_decl,type,
sk10: $i ).
thf(sk11_decl,type,
sk11: $i ).
thf(sk12_decl,type,
sk12: $i ).
thf(sk13_decl,type,
sk13: $i > $i > $o ).
thf(sk14_decl,type,
sk14: $i > $i > $i ).
thf(sk15_decl,type,
sk15: $i > $i > $i ).
thf(sk16_decl,type,
sk16: $i > $i > $i ).
thf(sk17_decl,type,
sk17: $i > $i > $i ).
thf(sk18_decl,type,
sk18: $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( ( ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( ( C @ ( B @ apply ) )
= C ) )
& ( ( B @ relation_dom )
= A ) )
=> ( B
= ( A @ identity_relation ) ) )
& ( ( B
= ( A @ identity_relation ) )
=> ( ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( ( C @ ( B @ apply ) )
= C ) )
& ( ( B @ relation_dom )
= A ) ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ( ( ( A @ function )
& ( A @ relation ) )
=> ( ( ( ! [B: $i] :
( ( sk1 @ ( B @ in ) )
=> ( ( B @ ( A @ apply ) )
= B ) )
& ( ( A @ relation_dom )
= sk1 ) )
=> ( A
= ( sk1 @ identity_relation ) ) )
& ( ( A
= ( sk1 @ identity_relation ) )
=> ( ! [B: $i] :
( ( sk1 @ ( B @ in ) )
=> ( ( B @ ( A @ apply ) )
= B ) )
& ( ( A @ relation_dom )
= sk1 ) ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
~ ( ( sk1 @ ( A @ in ) )
=> ( ( A @ ( sk2 @ apply ) )
= A ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: $i] : ( A @ empty ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: $i] :
~ ( A @ empty ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: $i] :
@+[B: $i] :
( ~ ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: $i] :
@+[B: $i] :
( ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( ^ [A: $i] :
@+[B: $i] : ( A @ ( B @ element ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( @+[A: $i] :
( ( A @ relation_empty_yielding )
& ( A @ relation ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( @+[A: $i] :
( ( A @ relation )
& ( A @ empty ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( @+[A: $i] :
( ( A @ relation )
& ~ ( A @ empty ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ! [D: $i] :
( ( A @ ( D @ ( C @ ordered_pair ) @ in ) )
=> ( ( C = D )
& ( B @ ( C @ in ) ) ) ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( A @ ( C @ ( B @ ( A @ sk14 ) @ ordered_pair ) @ in ) )
=> ( ( ( B @ ( A @ sk14 ) )
= C )
& ( B @ ( B @ ( A @ sk14 ) @ in ) ) ) ) ) ) ).
thf(sk16_def,definition,
( sk16
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ! [D: $i] :
( ( ( C = D )
& ( B @ ( C @ in ) ) )
=> ( A @ ( D @ ( C @ ordered_pair ) @ in ) ) ) ) ) ).
thf(sk17_def,definition,
( sk17
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( ( ( B @ ( A @ sk16 ) )
= C )
& ( B @ ( B @ ( A @ sk16 ) @ in ) ) )
=> ( A @ ( C @ ( B @ ( A @ sk16 ) @ ordered_pair ) @ in ) ) ) ) ) ).
thf(sk18_def,definition,
( sk18
= ( @+[A: $i] :
( ( A @ function )
& ( A @ relation ) ) ) ) ).
thf(1,conjecture,
! [A: $i,B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( B
= ( A @ identity_relation ) )
<=> ( ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( ( C @ ( B @ apply ) )
= C ) )
& ( ( B @ relation_dom )
= A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t34_funct_1) ).
thf(2,negated_conjecture,
~ ! [A: $i,B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( B
= ( A @ identity_relation ) )
<=> ( ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( ( C @ ( B @ apply ) )
= C ) )
& ( ( B @ relation_dom )
= A ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(43,plain,
~ ! [A: $i,B: $i] :
( ( ( B @ function )
& ( B @ relation ) )
=> ( ( ( ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( ( C @ ( B @ apply ) )
= C ) )
& ( ( B @ relation_dom )
= A ) )
=> ( B
= ( A @ identity_relation ) ) )
& ( ( B
= ( A @ identity_relation ) )
=> ( ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( ( C @ ( B @ apply ) )
= C ) )
& ( ( B @ relation_dom )
= A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(44,plain,
! [A: $i] :
( ( ( sk2
!= ( sk1 @ identity_relation ) )
| sk3 )
& ( ( ( A @ ( sk2 @ apply ) )
= A )
| ~ ( sk1 @ ( A @ in ) )
| sk3 )
& ( ( ( sk2 @ relation_dom )
= sk1 )
| sk3 )
& ( ~ sk3
| ( ( sk4 @ ( sk2 @ apply ) )
!= sk4 )
| ( ( sk2 @ relation_dom )
!= sk1 ) )
& ( ~ sk3
| ( sk1 @ ( sk4 @ in ) )
| ( ( sk2 @ relation_dom )
!= sk1 ) )
& ( ~ sk3
| ( sk2
= ( sk1 @ identity_relation ) ) )
& ( sk2 @ function )
& ( sk2 @ relation ) ),
inference(cnf,[status(esa)],[43]) ).
thf(48,plain,
( ( ( sk2 @ relation_dom )
= sk1 )
| sk3 ),
inference(cnfConj,[status(thm)],[44]) ).
thf(56,plain,
( sk3
| ( ( sk2 @ relation_dom )
= sk1 ) ),
inference(lifteq,[status(thm)],[48]) ).
thf(9,axiom,
empty_set @ empty,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_xboole_0) ).
thf(76,plain,
empty_set @ empty,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(35,axiom,
! [A: $i] :
( ( A @ empty )
=> ( ( A @ relation_dom @ relation )
& ( A @ relation_dom @ empty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc7_relat_1) ).
thf(195,plain,
! [A: $i] :
( ( A @ empty )
=> ( ( A @ relation_dom @ relation )
& ( A @ relation_dom @ empty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(196,plain,
! [A: $i] :
( ( ( A @ relation_dom @ relation )
| ~ ( A @ empty ) )
& ( ( A @ relation_dom @ empty )
| ~ ( A @ empty ) ) ),
inference(cnf,[status(esa)],[195]) ).
thf(197,plain,
! [A: $i] :
( ( A @ relation_dom @ empty )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[196]) ).
thf(13516,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,197]) ).
thf(13517,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty ) ),
inference(simp,[status(thm)],[13516]) ).
thf(13518,plain,
empty_set @ relation_dom @ empty,
inference(pattern_uni,[status(thm)],[13517:[bind(A,$thf( empty_set ))]]) ).
thf(13619,plain,
( ( ( sk2 @ relation_dom )
!= ( empty_set @ relation_dom ) )
| ( sk1 @ empty )
| sk3 ),
inference(paramod_ordered,[status(thm)],[56,13518]) ).
thf(13751,plain,
( ( sk2 != empty_set )
| ( sk1 @ empty )
| sk3 ),
inference(simp,[status(thm)],[13619]) ).
thf(7,axiom,
? [A: $i] :
~ ( A @ empty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
thf(70,plain,
? [A: $i] :
~ ( A @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(71,plain,
~ ! [A: $i] : ( A @ empty ),
inference(miniscope,[status(thm)],[70]) ).
thf(72,plain,
~ ( sk6 @ empty ),
inference(cnf,[status(esa)],[71]) ).
thf(14570,plain,
( ( ( sk6 @ empty )
!= ( sk1 @ empty ) )
| ~ $true
| ( sk2 != empty_set )
| sk3 ),
inference(paramod_ordered,[status(thm)],[13751,72]) ).
thf(14571,plain,
( ( ( sk6 @ empty )
!= ( sk1 @ empty ) )
| ( sk2 != empty_set )
| sk3 ),
inference(simp,[status(thm)],[14570]) ).
thf(14606,plain,
( ( sk6 != sk1 )
| ( sk2 != empty_set )
| sk3 ),
inference(simp,[status(thm)],[14571]) ).
thf(4,axiom,
! [A: $i,B: $i] : ( A @ ( A @ subset ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
thf(62,plain,
! [A: $i] : ( A @ ( A @ subset ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(63,plain,
! [A: $i] : ( A @ ( A @ subset ) ),
inference(cnf,[status(esa)],[62]) ).
thf(10,axiom,
! [A: $i,B: $i] :
( ( B @ powerset @ ( A @ element ) )
<=> ( B @ ( A @ subset ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
thf(77,plain,
! [A: $i,B: $i] :
( ( ( B @ ( A @ subset ) )
=> ( B @ powerset @ ( A @ element ) ) )
& ( ( B @ powerset @ ( A @ element ) )
=> ( B @ ( A @ subset ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(78,plain,
( ! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
=> ( B @ powerset @ ( A @ element ) ) )
& ! [A: $i,B: $i] :
( ( B @ powerset @ ( A @ element ) )
=> ( B @ ( A @ subset ) ) ) ),
inference(miniscope,[status(thm)],[77]) ).
thf(79,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ powerset @ ( C @ element ) )
| ~ ( D @ ( C @ subset ) ) )
& ( ( B @ ( A @ subset ) )
| ~ ( B @ powerset @ ( A @ element ) ) ) ),
inference(cnf,[status(esa)],[78]) ).
thf(81,plain,
! [B: $i,A: $i] :
( ( B @ powerset @ ( A @ element ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnfConj,[status(thm)],[79]) ).
thf(82,plain,
! [B: $i,A: $i] :
( ( B @ powerset @ ( A @ element ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[81]) ).
thf(869,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( C @ powerset @ ( B @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[63,82]) ).
thf(870,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( C @ powerset @ ( B @ element ) ) ),
inference(simp,[status(thm)],[869]) ).
thf(871,plain,
! [A: $i] : ( A @ powerset @ ( A @ element ) ),
inference(pattern_uni,[status(thm)],[870:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(32,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ element ) )
=> ( ( B @ ( A @ in ) )
| ( B @ empty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
thf(185,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ element ) )
=> ( ( B @ ( A @ in ) )
| ( B @ empty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(186,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ in ) )
| ( B @ empty )
| ~ ( B @ ( A @ element ) ) ),
inference(cnf,[status(esa)],[185]) ).
thf(12547,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[871,186]) ).
thf(12548,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty ) ),
inference(simp,[status(thm)],[12547]) ).
thf(12549,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ in ) )
| ( A @ powerset @ empty ) ),
inference(pattern_uni,[status(thm)],[12548:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ powerset ))]]) ).
thf(12552,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ in ) )
| ( A @ powerset @ empty ) ),
inference(simp,[status(thm)],[12549]) ).
thf(13,axiom,
! [A: $i] :
~ ( A @ powerset @ empty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
thf(90,plain,
! [A: $i] :
~ ( A @ powerset @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(91,plain,
~ ? [A: $i] : ( A @ powerset @ empty ),
inference(miniscope,[status(thm)],[90]) ).
thf(92,plain,
! [A: $i] :
~ ( A @ powerset @ empty ),
inference(cnf,[status(esa)],[91]) ).
thf(32607,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ in ) )
| $false ),
inference(rewrite,[status(thm)],[12552,92]) ).
thf(32608,plain,
! [A: $i] : ( A @ powerset @ ( A @ in ) ),
inference(simp,[status(thm)],[32607]) ).
thf(3,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ unordered_pair ) )
= ( A @ ( B @ unordered_pair ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
thf(59,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ unordered_pair ) )
= ( A @ ( B @ unordered_pair ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(60,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) )
= ( A @ ( B @ unordered_pair ) ) ),
inference(cnf,[status(esa)],[59]) ).
thf(61,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) )
= ( A @ ( B @ unordered_pair ) ) ),
inference(lifteq,[status(thm)],[60]) ).
thf(30,axiom,
! [A: $i,B: $i] :
( ( B @ relation )
=> ( ( B
= ( A @ identity_relation ) )
<=> ! [C: $i,D: $i] :
( ( B @ ( D @ ( C @ ordered_pair ) @ in ) )
<=> ( ( C = D )
& ( A @ ( C @ in ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_relat_1) ).
thf(159,plain,
! [A: $i,B: $i] :
( ( B @ relation )
=> ( ( ! [C: $i,D: $i] :
( ( ( ( C = D )
& ( A @ ( C @ in ) ) )
=> ( B @ ( D @ ( C @ ordered_pair ) @ in ) ) )
& ( ( B @ ( D @ ( C @ ordered_pair ) @ in ) )
=> ( ( C = D )
& ( A @ ( C @ in ) ) ) ) )
=> ( B
= ( A @ identity_relation ) ) )
& ( ( B
= ( A @ identity_relation ) )
=> ! [C: $i,D: $i] :
( ( ( ( C = D )
& ( A @ ( C @ in ) ) )
=> ( B @ ( D @ ( C @ ordered_pair ) @ in ) ) )
& ( ( B @ ( D @ ( C @ ordered_pair ) @ in ) )
=> ( ( C = D )
& ( A @ ( C @ in ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(160,plain,
! [A: $i,B: $i] :
( ( B @ relation )
=> ( ( ( ! [C: $i,D: $i] :
( ( ( C = D )
& ( A @ ( C @ in ) ) )
=> ( B @ ( D @ ( C @ ordered_pair ) @ in ) ) )
& ! [C: $i,D: $i] :
( ( B @ ( D @ ( C @ ordered_pair ) @ in ) )
=> ( ( C = D )
& ( A @ ( C @ in ) ) ) ) )
=> ( B
= ( A @ identity_relation ) ) )
& ( ( B
= ( A @ identity_relation ) )
=> ( ! [C: $i,D: $i] :
( ( ( C = D )
& ( A @ ( C @ in ) ) )
=> ( B @ ( D @ ( C @ ordered_pair ) @ in ) ) )
& ! [C: $i,D: $i] :
( ( B @ ( D @ ( C @ ordered_pair ) @ in ) )
=> ( ( C = D )
& ( A @ ( C @ in ) ) ) ) ) ) ) ),
inference(miniscope,[status(thm)],[159]) ).
thf(161,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B
= ( A @ identity_relation ) )
| ~ ( B @ ( A @ ( B @ sk17 ) @ ( A @ ( B @ sk16 ) @ ordered_pair ) @ in ) )
| ( B @ ( A @ sk13 ) )
| ~ ( B @ relation ) )
& ( ( B
= ( A @ identity_relation ) )
| ( ( A @ ( B @ sk16 ) )
= ( A @ ( B @ sk17 ) ) )
| ( B @ ( A @ sk13 ) )
| ~ ( B @ relation ) )
& ( ( B
= ( A @ identity_relation ) )
| ( A @ ( A @ ( B @ sk16 ) @ in ) )
| ( B @ ( A @ sk13 ) )
| ~ ( B @ relation ) )
& ( ( B
= ( A @ identity_relation ) )
| ~ ( B @ ( A @ sk13 ) )
| ( ( A @ ( B @ sk14 ) )
!= ( A @ ( B @ sk15 ) ) )
| ~ ( A @ ( A @ ( B @ sk14 ) @ in ) )
| ~ ( B @ relation ) )
& ( ( B
= ( A @ identity_relation ) )
| ~ ( B @ ( A @ sk13 ) )
| ( B @ ( A @ ( B @ sk15 ) @ ( A @ ( B @ sk14 ) @ ordered_pair ) @ in ) )
| ~ ( B @ relation ) )
& ( ( B @ ( F @ ( E @ ordered_pair ) @ in ) )
| ( E != F )
| ~ ( A @ ( E @ in ) )
| ( B
!= ( A @ identity_relation ) )
| ~ ( B @ relation ) )
& ( ( C = D )
| ~ ( B @ ( D @ ( C @ ordered_pair ) @ in ) )
| ( B
!= ( A @ identity_relation ) )
| ~ ( B @ relation ) )
& ( ( A @ ( C @ in ) )
| ~ ( B @ ( D @ ( C @ ordered_pair ) @ in ) )
| ( B
!= ( A @ identity_relation ) )
| ~ ( B @ relation ) ) ),
inference(cnf,[status(esa)],[160]) ).
thf(166,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C = D )
| ~ ( B @ ( D @ ( C @ ordered_pair ) @ in ) )
| ( B
!= ( A @ identity_relation ) )
| ~ ( B @ relation ) ),
inference(cnfConj,[status(thm)],[161]) ).
thf(175,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( D @ ( C @ ordered_pair ) @ in ) )
| ~ ( B @ relation )
| ( C = D )
| ( B
!= ( A @ identity_relation ) ) ),
inference(lifteq,[status(thm)],[166]) ).
thf(176,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ identity_relation @ ( C @ ( B @ ordered_pair ) @ in ) )
| ~ ( A @ identity_relation @ relation )
| ( B = C ) ),
inference(simp,[status(thm)],[175]) ).
thf(34,axiom,
! [A: $i] :
( ( A @ identity_relation @ function )
& ( A @ identity_relation @ relation ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_funct_1) ).
thf(189,plain,
! [A: $i] :
( ( A @ identity_relation @ function )
& ( A @ identity_relation @ relation ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(190,plain,
( ! [A: $i] : ( A @ identity_relation @ function )
& ! [A: $i] : ( A @ identity_relation @ relation ) ),
inference(miniscope,[status(thm)],[189]) ).
thf(191,plain,
! [B: $i,A: $i] :
( ( B @ identity_relation @ function )
& ( A @ identity_relation @ relation ) ),
inference(cnf,[status(esa)],[190]) ).
thf(192,plain,
! [A: $i] : ( A @ identity_relation @ relation ),
inference(cnfConj,[status(thm)],[191]) ).
thf(12,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
thf(87,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(88,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) ) ),
inference(cnf,[status(esa)],[87]) ).
thf(89,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) ) ),
inference(lifteq,[status(thm)],[88]) ).
thf(6099,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) )
| ~ $true
| ( B = C ) ),
inference(rewrite,[status(thm)],[176,192,89]) ).
thf(6100,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) )
| ( B = C ) ),
inference(simp,[status(thm)],[6099]) ).
thf(232,plain,
( ( ( sk6 @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,72]) ).
thf(233,plain,
( ( sk6 @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[232]) ).
thf(235,plain,
sk6 != empty_set,
inference(simp,[status(thm)],[233]) ).
thf(7020,plain,
! [C: $i,B: $i,A: $i] :
( ( B != sk6 )
| ( C != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[6100,235]) ).
thf(7021,plain,
! [B: $i,A: $i] :
( ( B != empty_set )
| ~ ( A @ identity_relation @ ( sk6 @ singleton @ ( B @ ( sk6 @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[7020:[bind(A,$thf( A )),bind(B,$thf( sk6 ))]]) ).
thf(7443,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( sk6 @ singleton @ ( empty_set @ ( sk6 @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[7021]) ).
thf(7873,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( sk6 @ singleton @ ( empty_set @ ( sk6 @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7443]) ).
thf(7874,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( empty_set @ ( sk6 @ unordered_pair ) @ ( sk6 @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[7873:[bind(A,$thf( empty_set @ ( sk6 @ unordered_pair ) )),bind(B,$thf( sk6 @ singleton )),bind(C,$thf( C ))]]) ).
thf(8033,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( empty_set @ ( sk6 @ unordered_pair ) @ ( sk6 @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[7874]) ).
thf(32634,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ ( sk6 @ unordered_pair ) @ ( sk6 @ singleton @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,8033]) ).
thf(32635,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ ( sk6 @ unordered_pair ) @ ( sk6 @ singleton @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32634]) ).
thf(32778,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( empty_set @ ( sk6 @ unordered_pair ) @ ( sk6 @ singleton @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32635]) ).
thf(32819,plain,
! [A: $i] :
( ( empty_set @ ( sk6 @ unordered_pair ) @ ( sk6 @ singleton @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32778]) ).
thf(28,axiom,
? [A: $i] :
( ( A @ relation )
& ~ ( A @ empty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_relat_1) ).
thf(153,plain,
? [A: $i] :
( ( A @ relation )
& ~ ( A @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(154,plain,
( ( sk12 @ relation )
& ~ ( sk12 @ empty ) ),
inference(cnf,[status(esa)],[153]) ).
thf(155,plain,
~ ( sk12 @ empty ),
inference(cnfConj,[status(thm)],[154]) ).
thf(230,plain,
( ( ( sk12 @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,155]) ).
thf(231,plain,
( ( sk12 @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[230]) ).
thf(234,plain,
sk12 != empty_set,
inference(simp,[status(thm)],[231]) ).
thf(16,axiom,
! [A: $i] :
? [B: $i] :
( ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_subset_1) ).
thf(99,plain,
! [A: $i] :
? [B: $i] :
( ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(100,plain,
! [A: $i] :
( ( A @ sk8 @ empty )
& ( A @ powerset @ ( A @ sk8 @ element ) ) ),
inference(cnf,[status(esa)],[99]) ).
thf(102,plain,
! [A: $i] : ( A @ sk8 @ empty ),
inference(cnfConj,[status(thm)],[100]) ).
thf(18,axiom,
! [A: $i,B: $i] :
~ ( B @ ( A @ ordered_pair ) @ empty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
thf(105,plain,
! [A: $i,B: $i] :
~ ( B @ ( A @ ordered_pair ) @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(106,plain,
~ ? [A: $i,B: $i] : ( B @ ( A @ ordered_pair ) @ empty ),
inference(miniscope,[status(thm)],[105]) ).
thf(107,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ ordered_pair ) @ empty ),
inference(cnf,[status(esa)],[106]) ).
thf(659,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ sk8 @ empty )
!= ( C @ ( B @ ordered_pair ) @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,107]) ).
thf(660,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ sk8 @ empty )
!= ( C @ ( B @ ordered_pair ) @ empty ) ),
inference(simp,[status(thm)],[659]) ).
thf(673,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ sk8 )
!= ( C @ ( B @ ordered_pair ) ) ),
inference(simp,[status(thm)],[660]) ).
thf(1224,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ sk8 )
!= ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) ) ),
inference(rewrite,[status(thm)],[673,89]) ).
thf(15,axiom,
! [A: $i] :
( ( A @ empty )
=> ( A = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
thf(96,plain,
! [A: $i] :
( ( A @ empty )
=> ( A = empty_set ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(97,plain,
! [A: $i] :
( ( A = empty_set )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[96]) ).
thf(98,plain,
! [A: $i] :
( ~ ( A @ empty )
| ( A = empty_set ) ),
inference(lifteq,[status(thm)],[97]) ).
thf(1777,plain,
! [B: $i,A: $i] :
( ( ( A @ sk8 @ empty )
!= ( B @ empty ) )
| ~ $true
| ( B = empty_set ) ),
inference(paramod_ordered,[status(thm)],[102,98]) ).
thf(1778,plain,
! [B: $i,A: $i] :
( ( ( A @ sk8 @ empty )
!= ( B @ empty ) )
| ( B = empty_set ) ),
inference(simp,[status(thm)],[1777]) ).
thf(1779,plain,
! [A: $i] :
( ( A @ sk8 )
= empty_set ),
inference(pattern_uni,[status(thm)],[1778:[bind(A,$thf( C )),bind(B,$thf( C @ sk8 ))]]) ).
thf(2009,plain,
! [A: $i] :
( ( A @ sk8 )
= empty_set ),
inference(simp,[status(thm)],[1779]) ).
thf(4992,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) )
!= empty_set ),
inference(rewrite,[status(thm)],[1224,2009]) ).
thf(27,axiom,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ! [B: $i,C: $i] :
( ( ~ ( A @ relation_dom @ ( B @ in ) )
=> ( ( C
= ( B @ ( A @ apply ) ) )
<=> ( C = empty_set ) ) )
& ( ( A @ relation_dom @ ( B @ in ) )
=> ( ( C
= ( B @ ( A @ apply ) ) )
<=> ( A @ ( C @ ( B @ ordered_pair ) @ in ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_funct_1) ).
thf(138,plain,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ! [B: $i,C: $i] :
( ( ~ ( A @ relation_dom @ ( B @ in ) )
=> ( ( ( C = empty_set )
=> ( C
= ( B @ ( A @ apply ) ) ) )
& ( ( C
= ( B @ ( A @ apply ) ) )
=> ( C = empty_set ) ) ) )
& ( ( A @ relation_dom @ ( B @ in ) )
=> ( ( ( A @ ( C @ ( B @ ordered_pair ) @ in ) )
=> ( C
= ( B @ ( A @ apply ) ) ) )
& ( ( C
= ( B @ ( A @ apply ) ) )
=> ( A @ ( C @ ( B @ ordered_pair ) @ in ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(47,plain,
( ~ sk3
| ( sk2
= ( sk1 @ identity_relation ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(58,plain,
( ~ sk3
| ( ( sk1 @ identity_relation )
= sk2 ) ),
inference(lifteq,[status(thm)],[47]) ).
thf(36,axiom,
! [A: $i] :
( ( ( A @ identity_relation @ relation_rng )
= A )
& ( ( A @ identity_relation @ relation_dom )
= A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t71_relat_1) ).
thf(199,plain,
! [A: $i] :
( ( ( A @ identity_relation @ relation_rng )
= A )
& ( ( A @ identity_relation @ relation_dom )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(200,plain,
( ! [A: $i] :
( ( A @ identity_relation @ relation_rng )
= A )
& ! [A: $i] :
( ( A @ identity_relation @ relation_dom )
= A ) ),
inference(miniscope,[status(thm)],[199]) ).
thf(201,plain,
! [B: $i,A: $i] :
( ( ( B @ identity_relation @ relation_rng )
= B )
& ( ( A @ identity_relation @ relation_dom )
= A ) ),
inference(cnf,[status(esa)],[200]) ).
thf(202,plain,
! [A: $i] :
( ( A @ identity_relation @ relation_dom )
= A ),
inference(cnfConj,[status(thm)],[201]) ).
thf(204,plain,
! [A: $i] :
( ( A @ identity_relation @ relation_dom )
= A ),
inference(lifteq,[status(thm)],[202]) ).
thf(691,plain,
! [A: $i] :
( ( ( sk1 @ identity_relation )
!= ( A @ identity_relation ) )
| ( ( sk2 @ relation_dom )
= A )
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[58,204]) ).
thf(692,plain,
( ( ( sk2 @ relation_dom )
= sk1 )
| ~ sk3 ),
inference(pattern_uni,[status(thm)],[691:[bind(A,$thf( sk1 ))]]) ).
thf(49,plain,
( ~ sk3
| ( sk1 @ ( sk4 @ in ) )
| ( ( sk2 @ relation_dom )
!= sk1 ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(55,plain,
( ~ sk3
| ( sk1 @ ( sk4 @ in ) )
| ( ( sk2 @ relation_dom )
!= sk1 ) ),
inference(lifteq,[status(thm)],[49]) ).
thf(744,plain,
( ( ( sk2 @ relation_dom )
!= ( sk2 @ relation_dom ) )
| ~ sk3
| ( sk1 @ ( sk4 @ in ) )
| ( sk1 != sk1 )
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[692,55]) ).
thf(745,plain,
( ( ( sk2 @ relation_dom )
!= ( sk2 @ relation_dom ) )
| ( sk1 @ ( sk4 @ in ) )
| ~ sk3 ),
inference(simp,[status(thm)],[744]) ).
thf(746,plain,
( ( sk1 @ ( sk4 @ in ) )
| ~ sk3 ),
inference(pattern_uni,[status(thm)],[745:[]]) ).
thf(23,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ( B @ ( A @ element ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
thf(122,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ( B @ ( A @ element ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(123,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ element ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[122]) ).
thf(2887,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk4 @ in ) )
!= ( B @ ( A @ in ) ) )
| ( B @ ( A @ element ) )
| ~ $true
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[746,123]) ).
thf(2888,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk4 @ in ) )
!= ( B @ ( A @ in ) ) )
| ( B @ ( A @ element ) )
| ~ sk3 ),
inference(simp,[status(thm)],[2887]) ).
thf(2889,plain,
( ( sk1 @ ( sk4 @ element ) )
| ~ sk3 ),
inference(pattern_uni,[status(thm)],[2888:[bind(A,$thf( sk4 )),bind(B,$thf( sk1 ))]]) ).
thf(7871,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ ( sk6 @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( sk6 @ singleton @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7443]) ).
thf(7872,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( sk6 @ singleton @ ( sk6 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[7871:[bind(A,$thf( sk6 )),bind(B,$thf( empty_set ))]]) ).
thf(8030,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( sk6 @ singleton @ ( sk6 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[7872]) ).
thf(5,axiom,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( A != B )
& ( A @ empty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_boole) ).
thf(64,plain,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( A != B )
& ( A @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(65,plain,
~ ? [A: $i] :
( ? [B: $i] :
( ( B @ empty )
& ( A != B ) )
& ( A @ empty ) ),
inference(miniscope,[status(thm)],[64]) ).
thf(66,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ( A = B )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[65]) ).
thf(67,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ~ ( A @ empty )
| ( A = B ) ),
inference(lifteq,[status(thm)],[66]) ).
thf(50,plain,
( ( sk2
!= ( sk1 @ identity_relation ) )
| sk3 ),
inference(cnfConj,[status(thm)],[44]) ).
thf(57,plain,
( sk3
| ( ( sk1 @ identity_relation )
!= sk2 ) ),
inference(lifteq,[status(thm)],[50]) ).
thf(412,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk1 @ identity_relation ) )
| sk3
| ( B != sk2 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[67,57]) ).
thf(413,plain,
! [A: $i] :
( sk3
| ( A != sk2 )
| ~ ( A @ empty )
| ~ ( sk1 @ identity_relation @ empty ) ),
inference(pattern_uni,[status(thm)],[412:[bind(A,$thf( sk1 @ identity_relation )),bind(B,$thf( B ))]]) ).
thf(596,plain,
( sk3
| ~ ( sk2 @ empty )
| ~ ( sk1 @ identity_relation @ empty ) ),
inference(simp,[status(thm)],[413]) ).
thf(932,plain,
( ( ( sk1 @ identity_relation @ empty )
!= ( empty_set @ empty ) )
| sk3
| ~ ( sk2 @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,596]) ).
thf(933,plain,
( ( ( sk1 @ identity_relation @ empty )
!= ( empty_set @ empty ) )
| sk3
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[932]) ).
thf(962,plain,
( ( ( sk1 @ identity_relation )
!= empty_set )
| ~ ( sk2 @ empty )
| sk3 ),
inference(simp,[status(thm)],[933]) ).
thf(164,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ identity_relation ) )
| ~ ( B @ ( A @ sk13 ) )
| ( ( A @ ( B @ sk14 ) )
!= ( A @ ( B @ sk15 ) ) )
| ~ ( A @ ( A @ ( B @ sk14 ) @ in ) )
| ~ ( B @ relation ) ),
inference(cnfConj,[status(thm)],[161]) ).
thf(170,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sk13 ) )
| ~ ( A @ ( A @ ( B @ sk14 ) @ in ) )
| ~ ( B @ relation )
| ( B
= ( A @ identity_relation ) )
| ( ( A @ ( B @ sk15 ) )
!= ( A @ ( B @ sk14 ) ) ) ),
inference(lifteq,[status(thm)],[164]) ).
thf(20,axiom,
! [A: $i] :
( ( A @ empty )
=> ( ( A @ relation_rng @ relation )
& ( A @ relation_rng @ empty ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc8_relat_1) ).
thf(112,plain,
! [A: $i] :
( ( A @ empty )
=> ( ( A @ relation_rng @ relation )
& ( A @ relation_rng @ empty ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(113,plain,
! [A: $i] :
( ( ( A @ relation_rng @ relation )
| ~ ( A @ empty ) )
& ( ( A @ relation_rng @ empty )
| ~ ( A @ empty ) ) ),
inference(cnf,[status(esa)],[112]) ).
thf(114,plain,
! [A: $i] :
( ( A @ relation_rng @ empty )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[113]) ).
thf(2165,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,114]) ).
thf(2166,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty ) ),
inference(simp,[status(thm)],[2165]) ).
thf(2167,plain,
empty_set @ relation_rng @ empty,
inference(pattern_uni,[status(thm)],[2166:[bind(A,$thf( empty_set ))]]) ).
thf(2230,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[2167,98]) ).
thf(2231,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[2230]) ).
thf(2232,plain,
( ( empty_set @ relation_rng )
= empty_set ),
inference(pattern_uni,[status(thm)],[2231:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(46,plain,
sk2 @ relation,
inference(cnfConj,[status(thm)],[44]) ).
thf(38,axiom,
! [A: $i] :
( ( ( A @ relation )
& ~ ( A @ empty ) )
=> ~ ( A @ relation_rng @ empty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_relat_1) ).
thf(209,plain,
! [A: $i] :
( ( ( A @ relation )
& ~ ( A @ empty ) )
=> ~ ( A @ relation_rng @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(210,plain,
! [A: $i] :
( ~ ( A @ relation_rng @ empty )
| ~ ( A @ relation )
| ( A @ empty ) ),
inference(cnf,[status(esa)],[209]) ).
thf(14120,plain,
! [A: $i] :
( ( ( sk2 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_rng @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[46,210]) ).
thf(14121,plain,
! [A: $i] :
( ( ( sk2 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_rng @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[14120]) ).
thf(14122,plain,
( ~ ( sk2 @ relation_rng @ empty )
| ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[14121:[bind(A,$thf( sk2 ))]]) ).
thf(19696,plain,
( ( ( sk2 @ relation_rng @ empty )
!= ( empty_set @ empty ) )
| ~ $true
| ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[76,14122]) ).
thf(19697,plain,
( ( ( sk2 @ relation_rng @ empty )
!= ( empty_set @ empty ) )
| ( sk2 @ empty ) ),
inference(simp,[status(thm)],[19696]) ).
thf(19736,plain,
( ( ( sk2 @ relation_rng )
!= empty_set )
| ( sk2 @ empty ) ),
inference(simp,[status(thm)],[19697]) ).
thf(21751,plain,
( ( ( sk2 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( empty_set != empty_set )
| ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[2232,19736]) ).
thf(21752,plain,
( ( ( sk2 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( sk2 @ empty ) ),
inference(simp,[status(thm)],[21751]) ).
thf(21792,plain,
( ( sk2 != empty_set )
| ( sk2 @ empty ) ),
inference(simp,[status(thm)],[21752]) ).
thf(22612,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[21792,197]) ).
thf(22613,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[22612]) ).
thf(22614,plain,
( ( sk2 @ relation_dom @ empty )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[22613:[bind(A,$thf( sk2 ))]]) ).
thf(115,plain,
! [A: $i] :
( ( A @ relation_rng @ relation )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[113]) ).
thf(101,plain,
! [A: $i] : ( A @ powerset @ ( A @ sk8 @ element ) ),
inference(cnfConj,[status(thm)],[100]) ).
thf(2054,plain,
! [A: $i] : ( A @ powerset @ ( empty_set @ element ) ),
inference(rewrite,[status(thm)],[101,2009]) ).
thf(12532,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2054,186]) ).
thf(12533,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty ) ),
inference(simp,[status(thm)],[12532]) ).
thf(12534,plain,
! [A: $i] :
( ( A @ powerset @ ( empty_set @ in ) )
| ( A @ powerset @ empty ) ),
inference(pattern_uni,[status(thm)],[12533:[bind(A,$thf( D )),bind(B,$thf( empty_set )),bind(C,$thf( D @ powerset ))]]) ).
thf(12553,plain,
! [A: $i] :
( ( A @ powerset @ ( empty_set @ in ) )
| ( A @ powerset @ empty ) ),
inference(simp,[status(thm)],[12534]) ).
thf(22361,plain,
! [A: $i] :
( ( A @ powerset @ ( empty_set @ in ) )
| $false ),
inference(rewrite,[status(thm)],[12553,92]) ).
thf(22362,plain,
! [A: $i] : ( A @ powerset @ ( empty_set @ in ) ),
inference(simp,[status(thm)],[22361]) ).
thf(169,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ ( C @ ordered_pair ) @ in ) )
| ( C != D )
| ~ ( A @ ( C @ in ) )
| ( B
!= ( A @ identity_relation ) )
| ~ ( B @ relation ) ),
inference(cnfConj,[status(thm)],[161]) ).
thf(173,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ ( C @ ordered_pair ) @ in ) )
| ~ ( A @ ( C @ in ) )
| ~ ( B @ relation )
| ( C != D )
| ( B
!= ( A @ identity_relation ) ) ),
inference(lifteq,[status(thm)],[169]) ).
thf(174,plain,
! [B: $i,A: $i] :
( ( A @ identity_relation @ ( B @ ( B @ ordered_pair ) @ in ) )
| ~ ( A @ ( B @ in ) )
| ~ ( A @ identity_relation @ relation ) ),
inference(simp,[status(thm)],[173]) ).
thf(5702,plain,
! [B: $i,A: $i] :
( ( A @ identity_relation @ ( B @ singleton @ ( B @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) )
| ~ ( A @ ( B @ in ) )
| ~ $true ),
inference(rewrite,[status(thm)],[174,192,89]) ).
thf(5703,plain,
! [B: $i,A: $i] :
( ( A @ identity_relation @ ( B @ singleton @ ( B @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) )
| ~ ( A @ ( B @ in ) ) ),
inference(simp,[status(thm)],[5702]) ).
thf(22431,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ in ) )
!= ( B @ ( C @ in ) ) )
| ( B @ identity_relation @ ( C @ singleton @ ( C @ ( C @ unordered_pair ) @ unordered_pair ) @ in ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22362,5703]) ).
thf(22432,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ in ) )
!= ( B @ ( C @ in ) ) )
| ( B @ identity_relation @ ( C @ singleton @ ( C @ ( C @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[22431]) ).
thf(22433,plain,
! [A: $i] : ( A @ powerset @ identity_relation @ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[22432:[bind(A,$thf( D )),bind(B,$thf( D @ powerset )),bind(C,$thf( empty_set ))]]) ).
thf(22553,plain,
! [A: $i] : ( A @ powerset @ identity_relation @ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[22433]) ).
thf(22,axiom,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( B @ ( A @ in ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
thf(119,plain,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( B @ ( A @ in ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(120,plain,
~ ? [A: $i,B: $i] :
( ( B @ empty )
& ( B @ ( A @ in ) ) ),
inference(miniscope,[status(thm)],[119]) ).
thf(121,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[120]) ).
thf(2736,plain,
! [B: $i,A: $i] :
( ( ( empty_set @ empty )
!= ( B @ empty ) )
| ~ $true
| ~ ( B @ ( A @ in ) ) ),
inference(paramod_ordered,[status(thm)],[76,121]) ).
thf(2737,plain,
! [B: $i,A: $i] :
( ( ( empty_set @ empty )
!= ( B @ empty ) )
| ~ ( B @ ( A @ in ) ) ),
inference(simp,[status(thm)],[2736]) ).
thf(2738,plain,
! [A: $i] :
~ ( empty_set @ ( A @ in ) ),
inference(pattern_uni,[status(thm)],[2737:[bind(A,$thf( A )),bind(B,$thf( empty_set ))]]) ).
thf(22882,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation @ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) )
!= ( empty_set @ ( B @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22553,2738]) ).
thf(22883,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ identity_relation @ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) )
!= ( empty_set @ ( B @ in ) ) ),
inference(simp,[status(thm)],[22882]) ).
thf(23049,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation )
!= empty_set )
| ( ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) )
!= B ) ),
inference(simp,[status(thm)],[22883]) ).
thf(23095,plain,
! [A: $i] :
( ( A @ powerset @ identity_relation )
!= empty_set ),
inference(simp,[status(thm)],[23049]) ).
thf(272,plain,
! [A: $i] :
( ( ( A @ powerset @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,92]) ).
thf(273,plain,
! [A: $i] :
( ( A @ powerset @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[272]) ).
thf(276,plain,
! [A: $i] :
( ( A @ powerset )
!= empty_set ),
inference(simp,[status(thm)],[273]) ).
thf(22800,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) )
| ( C @ powerset @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,22553]) ).
thf(22801,plain,
! [A: $i] : ( A @ powerset @ identity_relation @ ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[22800:[bind(A,$thf( empty_set @ ( empty_set @ unordered_pair ) )),bind(B,$thf( empty_set @ singleton )),bind(C,$thf( C ))]]) ).
thf(23101,plain,
! [A: $i] : ( A @ powerset @ identity_relation @ ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[22801]) ).
thf(33,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ~ ( A @ ( B @ in ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
thf(187,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ~ ( A @ ( B @ in ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(188,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ in ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[187]) ).
thf(13084,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( A @ ( B @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( B @ ( A @ in ) ) ),
inference(eqfactor_ordered,[status(thm)],[188]) ).
thf(13085,plain,
! [A: $i] :
~ ( A @ ( A @ in ) ),
inference(pattern_uni,[status(thm)],[13084:[bind(A,$thf( B ))]]) ).
thf(13102,plain,
! [A: $i] :
~ ( A @ ( A @ in ) ),
inference(simp,[status(thm)],[13085]) ).
thf(23359,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation @ ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) )
!= ( B @ ( B @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[23101,13102]) ).
thf(23360,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ identity_relation @ ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) )
!= ( B @ ( B @ in ) ) ),
inference(simp,[status(thm)],[23359]) ).
thf(23657,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation )
!= B )
| ( ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) )
!= B ) ),
inference(simp,[status(thm)],[23360]) ).
thf(23704,plain,
! [A: $i] :
( ( A @ powerset @ identity_relation )
!= ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) ) ),
inference(simp,[status(thm)],[23657]) ).
thf(19,axiom,
? [A: $i] :
( ( A @ relation_empty_yielding )
& ( A @ relation ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc3_relat_1) ).
thf(108,plain,
? [A: $i] :
( ( A @ relation_empty_yielding )
& ( A @ relation ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(109,plain,
( ( sk10 @ relation_empty_yielding )
& ( sk10 @ relation ) ),
inference(cnf,[status(esa)],[108]) ).
thf(110,plain,
sk10 @ relation,
inference(cnfConj,[status(thm)],[109]) ).
thf(163,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ identity_relation ) )
| ( A @ ( A @ ( B @ sk16 ) @ in ) )
| ( B @ ( A @ sk13 ) )
| ~ ( B @ relation ) ),
inference(cnfConj,[status(thm)],[161]) ).
thf(180,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ ( B @ sk16 ) @ in ) )
| ( B @ ( A @ sk13 ) )
| ~ ( B @ relation )
| ( B
= ( A @ identity_relation ) ) ),
inference(lifteq,[status(thm)],[163]) ).
thf(1359,plain,
! [B: $i,A: $i] :
( ( ( sk10 @ relation )
!= ( B @ relation ) )
| ( A @ ( A @ ( B @ sk16 ) @ in ) )
| ( B @ ( A @ sk13 ) )
| ~ $true
| ( B
= ( A @ identity_relation ) ) ),
inference(paramod_ordered,[status(thm)],[110,180]) ).
thf(1360,plain,
! [B: $i,A: $i] :
( ( ( sk10 @ relation )
!= ( B @ relation ) )
| ( A @ ( A @ ( B @ sk16 ) @ in ) )
| ( B @ ( A @ sk13 ) )
| ( B
= ( A @ identity_relation ) ) ),
inference(simp,[status(thm)],[1359]) ).
thf(1361,plain,
! [A: $i] :
( ( A @ ( A @ ( sk10 @ sk16 ) @ in ) )
| ( sk10 @ ( A @ sk13 ) )
| ( ( A @ identity_relation )
= sk10 ) ),
inference(pattern_uni,[status(thm)],[1360:[bind(A,$thf( A )),bind(B,$thf( sk10 ))]]) ).
thf(5601,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( sk10 @ sk16 ) @ in ) )
!= ( empty_set @ ( B @ in ) ) )
| ~ $true
| ( sk10 @ ( A @ sk13 ) )
| ( ( A @ identity_relation )
= sk10 ) ),
inference(paramod_ordered,[status(thm)],[1361,2738]) ).
thf(5602,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( sk10 @ sk16 ) @ in ) )
!= ( empty_set @ ( B @ in ) ) )
| ( sk10 @ ( A @ sk13 ) )
| ( ( A @ identity_relation )
= sk10 ) ),
inference(simp,[status(thm)],[5601]) ).
thf(5603,plain,
( ( sk10 @ ( empty_set @ sk13 ) )
| ( ( empty_set @ identity_relation )
= sk10 ) ),
inference(pattern_uni,[status(thm)],[5602:[bind(A,$thf( empty_set )),bind(B,$thf( empty_set @ ( sk10 @ sk16 ) ))]]) ).
thf(31,axiom,
( ( empty_set @ relation )
& ( empty_set @ empty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_relat_1) ).
thf(181,plain,
( ( empty_set @ relation )
& ( empty_set @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(182,plain,
( ( empty_set @ relation )
& ( empty_set @ empty ) ),
inference(cnf,[status(esa)],[181]) ).
thf(184,plain,
empty_set @ relation,
inference(cnfConj,[status(thm)],[182]) ).
thf(1355,plain,
! [B: $i,A: $i] :
( ( ( empty_set @ relation )
!= ( B @ relation ) )
| ( A @ ( A @ ( B @ sk16 ) @ in ) )
| ( B @ ( A @ sk13 ) )
| ~ $true
| ( B
= ( A @ identity_relation ) ) ),
inference(paramod_ordered,[status(thm)],[184,180]) ).
thf(1356,plain,
! [B: $i,A: $i] :
( ( ( empty_set @ relation )
!= ( B @ relation ) )
| ( A @ ( A @ ( B @ sk16 ) @ in ) )
| ( B @ ( A @ sk13 ) )
| ( B
= ( A @ identity_relation ) ) ),
inference(simp,[status(thm)],[1355]) ).
thf(1357,plain,
! [A: $i] :
( ( A @ ( A @ ( empty_set @ sk16 ) @ in ) )
| ( empty_set @ ( A @ sk13 ) )
| ( ( A @ identity_relation )
= empty_set ) ),
inference(pattern_uni,[status(thm)],[1356:[bind(A,$thf( A )),bind(B,$thf( empty_set ))]]) ).
thf(2762,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( empty_set @ sk16 ) @ in ) )
!= ( empty_set @ ( B @ in ) ) )
| ~ $true
| ( empty_set @ ( A @ sk13 ) )
| ( ( A @ identity_relation )
= empty_set ) ),
inference(paramod_ordered,[status(thm)],[1357,2738]) ).
thf(2763,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( empty_set @ sk16 ) @ in ) )
!= ( empty_set @ ( B @ in ) ) )
| ( empty_set @ ( A @ sk13 ) )
| ( ( A @ identity_relation )
= empty_set ) ),
inference(simp,[status(thm)],[2762]) ).
thf(2764,plain,
( ( empty_set @ ( empty_set @ sk13 ) )
| ( ( empty_set @ identity_relation )
= empty_set ) ),
inference(pattern_uni,[status(thm)],[2763:[bind(A,$thf( empty_set )),bind(B,$thf( empty_set @ ( empty_set @ sk16 ) ))]]) ).
thf(5980,plain,
( ( ( empty_set @ identity_relation )
!= ( empty_set @ identity_relation ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 = empty_set )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[5603,2764]) ).
thf(5981,plain,
( ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 = empty_set )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[5980:[]]) ).
thf(52,plain,
! [A: $i] :
( ( ( A @ ( sk2 @ apply ) )
= A )
| ~ ( sk1 @ ( A @ in ) )
| sk3 ),
inference(cnfConj,[status(thm)],[44]) ).
thf(53,plain,
! [A: $i] :
( ~ ( sk1 @ ( A @ in ) )
| sk3
| ( ( A @ ( sk2 @ apply ) )
= A ) ),
inference(lifteq,[status(thm)],[52]) ).
thf(5578,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( sk10 @ sk16 ) @ in ) )
!= ( sk1 @ ( B @ in ) ) )
| ~ $true
| sk3
| ( ( B @ ( sk2 @ apply ) )
= B )
| ( sk10 @ ( A @ sk13 ) )
| ( ( A @ identity_relation )
= sk10 ) ),
inference(paramod_ordered,[status(thm)],[1361,53]) ).
thf(5579,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( sk10 @ sk16 ) @ in ) )
!= ( sk1 @ ( B @ in ) ) )
| sk3
| ( ( B @ ( sk2 @ apply ) )
= B )
| ( sk10 @ ( A @ sk13 ) )
| ( ( A @ identity_relation )
= sk10 ) ),
inference(simp,[status(thm)],[5578]) ).
thf(5580,plain,
( sk3
| ( ( sk1 @ ( sk10 @ sk16 ) @ ( sk2 @ apply ) )
= ( sk1 @ ( sk10 @ sk16 ) ) )
| ( sk10 @ ( sk1 @ sk13 ) )
| ( ( sk1 @ identity_relation )
= sk10 ) ),
inference(pattern_uni,[status(thm)],[5579:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ ( sk10 @ sk16 ) ))]]) ).
thf(21696,plain,
( ( sk10 != sk10 )
| sk3
| ( ( sk1 @ ( sk10 @ sk16 ) )
= ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) ) )
| ( sk10 @ ( sk1 @ sk13 ) )
| ( ( sk1 @ identity_relation )
= sk10 )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[5981,5580]) ).
thf(21697,plain,
( sk3
| ( ( sk1 @ ( sk10 @ sk16 ) )
= ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) ) )
| ( sk10 @ ( sk1 @ sk13 ) )
| ( ( sk1 @ identity_relation )
= sk10 )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[21696:[]]) ).
thf(22701,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[21792,114]) ).
thf(22702,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[22701]) ).
thf(22703,plain,
( ( sk2 @ relation_rng @ empty )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[22702:[bind(A,$thf( sk2 ))]]) ).
thf(35365,plain,
( ( ( sk2 @ relation_rng @ empty )
!= ( sk6 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[22703,72]) ).
thf(35366,plain,
( ( ( sk2 @ relation_rng @ empty )
!= ( sk6 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[35365]) ).
thf(35424,plain,
( ( ( sk2 @ relation_rng )
!= sk6 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[35366]) ).
thf(39508,plain,
! [A: $i] :
( ( A != sk2 )
| ( ( sk2 @ relation_rng )
!= sk6 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,35424]) ).
thf(39509,plain,
! [A: $i] :
( ( A != sk2 )
| ( ( sk2 @ relation_rng )
!= sk6 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[39508]) ).
thf(39510,plain,
( ( ( sk2 @ relation_rng )
!= sk6 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[39509:[bind(A,$thf( sk2 ))]]) ).
thf(23531,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation @ ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) )
!= ( C @ ( B @ in ) ) )
| ( C @ ( B @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[23101,123]) ).
thf(23532,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation @ ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) )
!= ( C @ ( B @ in ) ) )
| ( C @ ( B @ element ) ) ),
inference(simp,[status(thm)],[23531]) ).
thf(23533,plain,
! [A: $i] : ( A @ powerset @ identity_relation @ ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ element ) ),
inference(pattern_uni,[status(thm)],[23532:[bind(A,$thf( J )),bind(B,$thf( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) )),bind(C,$thf( J @ powerset @ identity_relation ))]]) ).
thf(23745,plain,
! [A: $i] : ( A @ powerset @ identity_relation @ ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ element ) ),
inference(simp,[status(thm)],[23533]) ).
thf(8,axiom,
! [A: $i] :
~ ( A @ singleton @ empty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_subset_1) ).
thf(73,plain,
! [A: $i] :
~ ( A @ singleton @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(74,plain,
~ ? [A: $i] : ( A @ singleton @ empty ),
inference(miniscope,[status(thm)],[73]) ).
thf(75,plain,
! [A: $i] :
~ ( A @ singleton @ empty ),
inference(cnf,[status(esa)],[74]) ).
thf(263,plain,
! [A: $i] :
( ( ( A @ singleton @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,75]) ).
thf(264,plain,
! [A: $i] :
( ( A @ singleton @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[263]) ).
thf(267,plain,
! [A: $i] :
( ( A @ singleton )
!= empty_set ),
inference(simp,[status(thm)],[264]) ).
thf(6831,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C
!= ( D @ singleton ) )
| ( B != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[6100,267]) ).
thf(6832,plain,
! [C: $i,B: $i,A: $i] :
( ( B != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ singleton @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[6831:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( E @ singleton )),bind(D,$thf( E ))]]) ).
thf(7363,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( empty_set @ singleton @ ( B @ singleton @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[6832]) ).
thf(16109,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ singleton @ ( D @ singleton @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7363]) ).
thf(16110,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ singleton @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[16109:[bind(A,$thf( G @ singleton @ ( empty_set @ unordered_pair ) )),bind(B,$thf( empty_set @ singleton )),bind(C,$thf( C )),bind(D,$thf( G ))]]) ).
thf(16336,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ singleton @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[16110]) ).
thf(23209,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C
!= ( D @ powerset @ identity_relation ) )
| ( B != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[6100,23095]) ).
thf(23210,plain,
! [C: $i,B: $i,A: $i] :
( ( B != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ powerset @ identity_relation @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[23209:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( F @ powerset @ identity_relation )),bind(D,$thf( F ))]]) ).
thf(23253,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( empty_set @ singleton @ ( B @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[23210]) ).
thf(32712,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ singleton @ ( C @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,23253]) ).
thf(32713,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ singleton @ ( C @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32712]) ).
thf(32781,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( empty_set @ singleton @ ( C @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32713]) ).
thf(32823,plain,
! [B: $i,A: $i] :
( ( empty_set @ singleton @ ( B @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32781]) ).
thf(23205,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ powerset @ identity_relation ) )
| ( C != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[6100,23095]) ).
thf(23206,plain,
! [C: $i,B: $i,A: $i] :
( ( B != empty_set )
| ~ ( A @ identity_relation @ ( C @ powerset @ identity_relation @ singleton @ ( B @ ( C @ powerset @ identity_relation @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[23205:[bind(A,$thf( A )),bind(B,$thf( F @ powerset @ identity_relation )),bind(C,$thf( C )),bind(D,$thf( F ))]]) ).
thf(23251,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ powerset @ identity_relation @ singleton @ ( empty_set @ ( B @ powerset @ identity_relation @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[23206]) ).
thf(17,axiom,
! [A: $i] :
? [B: $i] : ( A @ ( B @ element ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_m1_subset_1) ).
thf(103,plain,
! [A: $i] :
? [B: $i] : ( A @ ( B @ element ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(104,plain,
! [A: $i] : ( A @ ( A @ sk9 @ element ) ),
inference(cnf,[status(esa)],[103]) ).
thf(12538,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk9 @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,186]) ).
thf(12539,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk9 @ element ) )
!= ( C @ ( B @ element ) ) )
| ( C @ ( B @ in ) )
| ( C @ empty ) ),
inference(simp,[status(thm)],[12538]) ).
thf(12540,plain,
! [A: $i] :
( ( A @ ( A @ sk9 @ in ) )
| ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[12539:[bind(A,$thf( D )),bind(B,$thf( D @ sk9 )),bind(C,$thf( D ))]]) ).
thf(12554,plain,
! [A: $i] :
( ( A @ ( A @ sk9 @ in ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[12540]) ).
thf(27269,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk9 @ in ) )
!= ( C @ ( B @ in ) ) )
| ( C @ ( B @ element ) )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[12554,123]) ).
thf(27270,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk9 @ in ) )
!= ( C @ ( B @ in ) ) )
| ( C @ ( B @ element ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[27269]) ).
thf(27271,plain,
! [A: $i] :
( ( A @ ( A @ sk9 @ element ) )
| ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[27270:[bind(A,$thf( D )),bind(B,$thf( D @ sk9 )),bind(C,$thf( D ))]]) ).
thf(27355,plain,
! [A: $i] :
( ( A @ ( A @ sk9 @ element ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[27271]) ).
thf(27557,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( D @ powerset @ identity_relation @ singleton @ ( empty_set @ ( D @ powerset @ identity_relation @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,23251]) ).
thf(27558,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( empty_set @ ( B @ powerset @ identity_relation @ unordered_pair ) @ ( B @ powerset @ identity_relation @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[27557:[bind(A,$thf( empty_set @ ( K @ powerset @ identity_relation @ unordered_pair ) )),bind(B,$thf( K @ powerset @ identity_relation @ singleton )),bind(C,$thf( C )),bind(D,$thf( K ))]]) ).
thf(27885,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( empty_set @ ( B @ powerset @ identity_relation @ unordered_pair ) @ ( B @ powerset @ identity_relation @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[27558]) ).
thf(35112,plain,
! [A: $i] :
( ( ( sk1 @ ( sk10 @ sk16 ) )
!= ( A @ ( sk10 @ sk16 ) ) )
| ( A @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| ( sk10 @ ( A @ sk13 ) )
| ( ( A @ identity_relation )
= sk10 )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( ( sk1 @ identity_relation )
= sk10 )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[21697,1361]) ).
thf(35113,plain,
( ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| ( sk10 @ ( sk1 @ sk13 ) )
| ( ( sk1 @ identity_relation )
= sk10 )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( ( sk1 @ identity_relation )
= sk10 )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[35112:[bind(A,$thf( sk1 ))]]) ).
thf(35192,plain,
( ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( ( sk1 @ identity_relation )
= sk10 )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(simp,[status(thm)],[35113]) ).
thf(203,plain,
! [A: $i] :
( ( A @ identity_relation @ relation_rng )
= A ),
inference(cnfConj,[status(thm)],[201]) ).
thf(205,plain,
! [A: $i] :
( ( A @ identity_relation @ relation_rng )
= A ),
inference(lifteq,[status(thm)],[203]) ).
thf(206,plain,
! [A: $i] :
( ( A @ identity_relation @ relation_rng )
= A ),
inference(simp,[status(thm)],[205]) ).
thf(36608,plain,
! [A: $i] :
( ( ( sk1 @ identity_relation )
!= ( A @ identity_relation ) )
| ( ( sk10 @ relation_rng )
= A )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[35192,206]) ).
thf(36609,plain,
( ( ( sk10 @ relation_rng )
= sk1 )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[36608:[bind(A,$thf( sk1 ))]]) ).
thf(5927,plain,
! [A: $i] :
( ( ( empty_set @ identity_relation )
!= ( A @ identity_relation ) )
| ( ( sk10 @ relation_rng )
= A )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[5603,206]) ).
thf(5928,plain,
( ( ( sk10 @ relation_rng )
= empty_set )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[5927:[bind(A,$thf( empty_set ))]]) ).
thf(39015,plain,
( ( ( sk10 @ relation_rng )
!= ( sk10 @ relation_rng ) )
| ( sk1 = empty_set )
| ( sk10 @ ( empty_set @ sk13 ) )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[36609,5928]) ).
thf(39016,plain,
( ( ( sk10 @ relation_rng )
!= ( sk10 @ relation_rng ) )
| ( sk1 = empty_set )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(simp,[status(thm)],[39015]) ).
thf(39017,plain,
( ( sk1 = empty_set )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[39016:[]]) ).
thf(39,axiom,
! [A: $i] :
( ( ( A @ relation )
& ~ ( A @ empty ) )
=> ~ ( A @ relation_dom @ empty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_relat_1) ).
thf(211,plain,
! [A: $i] :
( ( ( A @ relation )
& ~ ( A @ empty ) )
=> ~ ( A @ relation_dom @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(212,plain,
! [A: $i] :
( ~ ( A @ relation_dom @ empty )
| ~ ( A @ relation )
| ( A @ empty ) ),
inference(cnf,[status(esa)],[211]) ).
thf(14389,plain,
! [A: $i] :
( ( ( sk2 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[46,212]) ).
thf(14390,plain,
! [A: $i] :
( ( ( sk2 @ relation )
!= ( A @ relation ) )
| ~ ( A @ relation_dom @ empty )
| ( A @ empty ) ),
inference(simp,[status(thm)],[14389]) ).
thf(14391,plain,
( ~ ( sk2 @ relation_dom @ empty )
| ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[14390:[bind(A,$thf( sk2 ))]]) ).
thf(20674,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( empty_set @ empty ) )
| ~ $true
| ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[76,14391]) ).
thf(20675,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( empty_set @ empty ) )
| ( sk2 @ empty ) ),
inference(simp,[status(thm)],[20674]) ).
thf(20707,plain,
( ( ( sk2 @ relation_dom )
!= empty_set )
| ( sk2 @ empty ) ),
inference(simp,[status(thm)],[20675]) ).
thf(45,plain,
( ~ sk3
| ( ( sk4 @ ( sk2 @ apply ) )
!= sk4 )
| ( ( sk2 @ relation_dom )
!= sk1 ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(54,plain,
( ~ sk3
| ( ( sk4 @ ( sk2 @ apply ) )
!= sk4 )
| ( ( sk2 @ relation_dom )
!= sk1 ) ),
inference(lifteq,[status(thm)],[45]) ).
thf(741,plain,
( ( ( sk2 @ relation_dom )
!= ( sk2 @ relation_dom ) )
| ~ sk3
| ( ( sk4 @ ( sk2 @ apply ) )
!= sk4 )
| ( sk1 != sk1 )
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[692,54]) ).
thf(742,plain,
( ( ( sk2 @ relation_dom )
!= ( sk2 @ relation_dom ) )
| ( ( sk4 @ ( sk2 @ apply ) )
!= sk4 )
| ~ sk3 ),
inference(simp,[status(thm)],[741]) ).
thf(743,plain,
( ( ( sk4 @ ( sk2 @ apply ) )
!= sk4 )
| ~ sk3 ),
inference(pattern_uni,[status(thm)],[742:[]]) ).
thf(847,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk4 @ ( sk2 @ apply ) ) )
| ( B != sk4 )
| ~ sk3
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[67,743]) ).
thf(848,plain,
! [A: $i] :
( ( A != sk4 )
| ~ sk3
| ~ ( A @ empty )
| ~ ( sk4 @ ( sk2 @ apply ) @ empty ) ),
inference(pattern_uni,[status(thm)],[847:[bind(A,$thf( sk4 @ ( sk2 @ apply ) )),bind(B,$thf( B ))]]) ).
thf(859,plain,
( ~ sk3
| ~ ( sk4 @ empty )
| ~ ( sk4 @ ( sk2 @ apply ) @ empty ) ),
inference(simp,[status(thm)],[848]) ).
thf(4390,plain,
( ( ( sk4 @ ( sk2 @ apply ) @ empty )
!= ( empty_set @ empty ) )
| ~ sk3
| ~ ( sk4 @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,859]) ).
thf(4391,plain,
( ( ( sk4 @ ( sk2 @ apply ) @ empty )
!= ( empty_set @ empty ) )
| ~ sk3
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[4390]) ).
thf(4439,plain,
( ( ( sk4 @ ( sk2 @ apply ) )
!= empty_set )
| ~ sk3
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[4391]) ).
thf(6,axiom,
? [A: $i] : ( A @ empty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_xboole_0) ).
thf(68,plain,
? [A: $i] : ( A @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(69,plain,
sk5 @ empty,
inference(cnf,[status(esa)],[68]) ).
thf(1707,plain,
! [A: $i] :
( ( ( sk5 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[69,98]) ).
thf(1708,plain,
! [A: $i] :
( ( ( sk5 @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[1707]) ).
thf(1709,plain,
sk5 = empty_set,
inference(pattern_uni,[status(thm)],[1708:[bind(A,$thf( sk5 ))]]) ).
thf(6189,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ powerset ) )
| ( C != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[6100,276]) ).
thf(6190,plain,
! [C: $i,B: $i,A: $i] :
( ( B != empty_set )
| ~ ( A @ identity_relation @ ( C @ powerset @ singleton @ ( B @ ( C @ powerset @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[6189:[bind(A,$thf( A )),bind(B,$thf( E @ powerset )),bind(C,$thf( C )),bind(D,$thf( E ))]]) ).
thf(7112,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ powerset @ singleton @ ( empty_set @ ( B @ powerset @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[6190]) ).
thf(16879,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( D @ powerset @ singleton @ ( empty_set @ ( D @ powerset @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7112]) ).
thf(16880,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( empty_set @ ( B @ powerset @ unordered_pair ) @ ( B @ powerset @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[16879:[bind(A,$thf( empty_set @ ( I @ powerset @ unordered_pair ) )),bind(B,$thf( I @ powerset @ singleton )),bind(C,$thf( C )),bind(D,$thf( I ))]]) ).
thf(17118,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( empty_set @ ( B @ powerset @ unordered_pair ) @ ( B @ powerset @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[16880]) ).
thf(17799,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ ( D @ powerset @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ ( D @ powerset @ singleton @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,17118]) ).
thf(17800,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ powerset @ ( empty_set @ unordered_pair ) @ ( B @ powerset @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[17799:[bind(A,$thf( E @ powerset )),bind(B,$thf( empty_set )),bind(C,$thf( C )),bind(D,$thf( E ))]]) ).
thf(17972,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ powerset @ ( empty_set @ unordered_pair ) @ ( B @ powerset @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[17800]) ).
thf(29,axiom,
! [A: $i] :
( ( A @ empty )
=> ( A @ relation ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relat_1) ).
thf(157,plain,
! [A: $i] :
( ( A @ empty )
=> ( A @ relation ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(14,axiom,
! [A: $i,B: $i] :
~ ( B @ ( A @ unordered_pair ) @ empty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_subset_1) ).
thf(93,plain,
! [A: $i,B: $i] :
~ ( B @ ( A @ unordered_pair ) @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(94,plain,
~ ? [A: $i,B: $i] : ( B @ ( A @ unordered_pair ) @ empty ),
inference(miniscope,[status(thm)],[93]) ).
thf(95,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ unordered_pair ) @ empty ),
inference(cnf,[status(esa)],[94]) ).
thf(645,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,95]) ).
thf(646,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[645]) ).
thf(654,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) )
!= empty_set ),
inference(simp,[status(thm)],[646]) ).
thf(6473,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( E @ ( D @ unordered_pair ) ) )
| ( C != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[6100,654]) ).
thf(6474,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B != empty_set )
| ~ ( A @ identity_relation @ ( D @ ( C @ unordered_pair ) @ singleton @ ( B @ ( D @ ( C @ unordered_pair ) @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[6473:[bind(A,$thf( A )),bind(B,$thf( G @ ( F @ unordered_pair ) )),bind(C,$thf( C )),bind(D,$thf( F )),bind(E,$thf( G ))]]) ).
thf(7222,plain,
! [C: $i,B: $i,A: $i] :
~ ( A @ identity_relation @ ( C @ ( B @ unordered_pair ) @ singleton @ ( empty_set @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[6474]) ).
thf(21003,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ ( E @ ( D @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( E @ ( D @ unordered_pair ) @ singleton @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7222]) ).
thf(21004,plain,
! [C: $i,B: $i,A: $i] :
~ ( A @ identity_relation @ ( C @ ( B @ unordered_pair ) @ singleton @ ( C @ ( B @ unordered_pair ) @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[21003:[bind(A,$thf( G @ ( F @ unordered_pair ) )),bind(B,$thf( empty_set )),bind(C,$thf( C )),bind(D,$thf( F )),bind(E,$thf( G ))]]) ).
thf(21188,plain,
! [C: $i,B: $i,A: $i] :
~ ( A @ identity_relation @ ( C @ ( B @ unordered_pair ) @ singleton @ ( C @ ( B @ unordered_pair ) @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[21004]) ).
thf(6191,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C
!= ( D @ powerset ) )
| ( B != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[6100,276]) ).
thf(6192,plain,
! [C: $i,B: $i,A: $i] :
( ( B != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ powerset @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[6191:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( E @ powerset )),bind(D,$thf( E ))]]) ).
thf(7113,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( empty_set @ singleton @ ( B @ powerset @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[6192]) ).
thf(32700,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ singleton @ ( C @ powerset @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,7113]) ).
thf(32701,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ singleton @ ( C @ powerset @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32700]) ).
thf(32803,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( empty_set @ singleton @ ( C @ powerset @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32701]) ).
thf(32848,plain,
! [B: $i,A: $i] :
( ( empty_set @ singleton @ ( B @ powerset @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32803]) ).
thf(24,axiom,
? [A: $i] :
( ( A @ relation )
& ( A @ empty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_relat_1) ).
thf(124,plain,
? [A: $i] :
( ( A @ relation )
& ( A @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(125,plain,
( ( sk11 @ relation )
& ( sk11 @ empty ) ),
inference(cnf,[status(esa)],[124]) ).
thf(126,plain,
sk11 @ empty,
inference(cnfConj,[status(thm)],[125]) ).
thf(1929,plain,
! [A: $i] :
( ( ( sk11 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[126,98]) ).
thf(1930,plain,
! [A: $i] :
( ( ( sk11 @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[1929]) ).
thf(1931,plain,
sk11 = empty_set,
inference(pattern_uni,[status(thm)],[1930:[bind(A,$thf( sk11 ))]]) ).
thf(934,plain,
( ( ( sk2 @ empty )
!= ( empty_set @ empty ) )
| sk3
| ~ $true
| ~ ( sk1 @ identity_relation @ empty ) ),
inference(paramod_ordered,[status(thm)],[76,596]) ).
thf(935,plain,
( ( ( sk2 @ empty )
!= ( empty_set @ empty ) )
| sk3
| ~ ( sk1 @ identity_relation @ empty ) ),
inference(simp,[status(thm)],[934]) ).
thf(969,plain,
( ( sk2 != empty_set )
| ~ ( sk1 @ identity_relation @ empty )
| sk3 ),
inference(simp,[status(thm)],[935]) ).
thf(21750,plain,
! [A: $i] :
( ( ( A @ identity_relation @ relation_rng )
!= ( sk2 @ relation_rng ) )
| ( A != empty_set )
| ( sk2 @ empty ) ),
inference(paramod_ordered,[status(thm)],[206,19736]) ).
thf(21791,plain,
( ( ( empty_set @ identity_relation )
!= sk2 )
| ( sk2 @ empty ) ),
inference(simp,[status(thm)],[21750]) ).
thf(193,plain,
! [A: $i] : ( A @ identity_relation @ function ),
inference(cnfConj,[status(thm)],[191]) ).
thf(194,plain,
! [A: $i] : ( A @ identity_relation @ function ),
inference(simp,[status(thm)],[193]) ).
thf(5956,plain,
! [A: $i] :
( ( ( empty_set @ identity_relation )
!= ( A @ identity_relation ) )
| ( sk10 @ function )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[5603,194]) ).
thf(5957,plain,
( ( sk10 @ function )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[5956:[bind(A,$thf( empty_set ))]]) ).
thf(168,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ identity_relation ) )
| ~ ( B @ ( A @ sk13 ) )
| ( B @ ( A @ ( B @ sk15 ) @ ( A @ ( B @ sk14 ) @ ordered_pair ) @ in ) )
| ~ ( B @ relation ) ),
inference(cnfConj,[status(thm)],[161]) ).
thf(179,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sk13 ) )
| ( B @ ( A @ ( B @ sk15 ) @ ( A @ ( B @ sk14 ) @ ordered_pair ) @ in ) )
| ~ ( B @ relation )
| ( B
= ( A @ identity_relation ) ) ),
inference(lifteq,[status(thm)],[168]) ).
thf(10950,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sk13 ) )
| ( B @ ( A @ ( B @ sk14 ) @ singleton @ ( A @ ( B @ sk15 ) @ ( A @ ( B @ sk14 ) @ unordered_pair ) @ unordered_pair ) @ in ) )
| ~ ( B @ relation )
| ( B
= ( A @ identity_relation ) ) ),
inference(rewrite,[status(thm)],[179,89]) ).
thf(661,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ordered_pair ) @ empty )
!= ( sk5 @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[69,107]) ).
thf(662,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) @ empty )
!= ( sk5 @ empty ) ),
inference(simp,[status(thm)],[661]) ).
thf(674,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) )
!= sk5 ),
inference(simp,[status(thm)],[662]) ).
thf(1222,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) )
!= sk5 ),
inference(rewrite,[status(thm)],[674,89]) ).
thf(1253,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( D @ ( C @ unordered_pair ) ) )
| ( ( C @ singleton @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) )
!= sk5 ) ),
inference(paramod_ordered,[status(thm)],[61,1222]) ).
thf(1254,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) )
!= sk5 ),
inference(pattern_uni,[status(thm)],[1253:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(2955,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) )
!= empty_set ),
inference(rewrite,[status(thm)],[1254,1709]) ).
thf(2970,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( C @ singleton @ ( C @ ( D @ unordered_pair ) @ unordered_pair ) ) )
| ( ( A @ ( B @ unordered_pair ) )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[61,2955]) ).
thf(2971,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( B @ singleton @ unordered_pair ) )
!= empty_set ),
inference(pattern_uni,[status(thm)],[2970:[bind(A,$thf( G @ ( E @ unordered_pair ) )),bind(B,$thf( G @ singleton )),bind(C,$thf( G )),bind(D,$thf( E ))]]) ).
thf(3001,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( B @ singleton @ unordered_pair ) )
!= empty_set ),
inference(simp,[status(thm)],[2971]) ).
thf(4328,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ unordered_pair ) )
!= ( D @ ( C @ unordered_pair ) ) )
| ( ( B @ ( A @ unordered_pair ) @ ( D @ singleton @ unordered_pair ) )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[61,3001]) ).
thf(4329,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) )
!= empty_set ),
inference(pattern_uni,[status(thm)],[4328:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(22831,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation @ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) )
!= ( C @ ( B @ in ) ) )
| ~ ( B @ ( C @ in ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22553,188]) ).
thf(22832,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation @ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) )
!= ( C @ ( B @ in ) ) )
| ~ ( B @ ( C @ in ) ) ),
inference(simp,[status(thm)],[22831]) ).
thf(22833,plain,
! [A: $i] :
~ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ ( A @ powerset @ identity_relation @ in ) ),
inference(pattern_uni,[status(thm)],[22832:[bind(A,$thf( J )),bind(B,$thf( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) )),bind(C,$thf( J @ powerset @ identity_relation ))]]) ).
thf(23115,plain,
! [A: $i] :
~ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ ( A @ powerset @ identity_relation @ in ) ),
inference(simp,[status(thm)],[22833]) ).
thf(2244,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2167,114]) ).
thf(2245,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ empty ) ),
inference(simp,[status(thm)],[2244]) ).
thf(2246,plain,
empty_set @ relation_rng @ relation_rng @ empty,
inference(pattern_uni,[status(thm)],[2245:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(2304,plain,
empty_set @ relation_rng @ empty,
inference(rewrite,[status(thm)],[2246,2232]) ).
thf(2422,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2304,115]) ).
thf(2423,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation ) ),
inference(simp,[status(thm)],[2422]) ).
thf(2424,plain,
empty_set @ relation_rng @ relation_rng @ relation,
inference(pattern_uni,[status(thm)],[2423:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(2451,plain,
empty_set @ relation_rng @ relation,
inference(rewrite,[status(thm)],[2424,2232]) ).
thf(39908,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
!= ( B @ ( A @ in ) ) )
| ( B @ ( A @ element ) )
| ~ $true
| ( sk1 = empty_set )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[39017,123]) ).
thf(39909,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
!= ( B @ ( A @ in ) ) )
| ( B @ ( A @ element ) )
| ( sk1 = empty_set )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(simp,[status(thm)],[39908]) ).
thf(39910,plain,
( ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ element ) )
| ( sk1 = empty_set )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[39909:[bind(A,$thf( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) )),bind(B,$thf( sk1 ))]]) ).
thf(1827,plain,
! [A: $i] :
( ( A != sk4 )
| ( ( empty_set @ ( sk2 @ apply ) )
!= sk4 )
| ~ sk3
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,743]) ).
thf(1828,plain,
( ( ( empty_set @ ( sk2 @ apply ) )
!= sk4 )
| ~ sk3
| ~ ( sk4 @ empty ) ),
inference(pattern_uni,[status(thm)],[1827:[bind(A,$thf( sk4 ))]]) ).
thf(7022,plain,
! [C: $i,B: $i,A: $i] :
( ( C != sk6 )
| ( B != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[6100,235]) ).
thf(7023,plain,
! [B: $i,A: $i] :
( ( B != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( sk6 @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[7022:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( sk6 ))]]) ).
thf(7444,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( empty_set @ singleton @ ( sk6 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[7023]) ).
thf(8064,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ unordered_pair ) )
!= ( empty_set @ singleton @ ( sk6 @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( B @ ( A @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7444]) ).
thf(8065,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( sk6 @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[8064:[bind(A,$thf( empty_set @ singleton )),bind(B,$thf( sk6 @ ( empty_set @ unordered_pair ) )),bind(C,$thf( C ))]]) ).
thf(8194,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( sk6 @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[8065]) ).
thf(32719,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk6 @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,8194]) ).
thf(32720,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk6 @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32719]) ).
thf(32788,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( sk6 @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32720]) ).
thf(32831,plain,
! [A: $i] :
( ( sk6 @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32788]) ).
thf(33457,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk12 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[22614,155]) ).
thf(33458,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk12 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[33457]) ).
thf(33567,plain,
( ( ( sk2 @ relation_dom )
!= sk12 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[33458]) ).
thf(38710,plain,
! [A: $i] :
( ( A != sk2 )
| ( ( sk2 @ relation_dom )
!= sk12 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,33567]) ).
thf(38711,plain,
! [A: $i] :
( ( A != sk2 )
| ( ( sk2 @ relation_dom )
!= sk12 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[38710]) ).
thf(38712,plain,
( ( ( sk2 @ relation_dom )
!= sk12 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[38711:[bind(A,$thf( sk2 ))]]) ).
thf(198,plain,
! [A: $i] :
( ( A @ relation_dom @ relation )
| ~ ( A @ empty ) ),
inference(cnfConj,[status(thm)],[196]) ).
thf(22661,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[21792,198]) ).
thf(22662,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[22661]) ).
thf(22663,plain,
( ( sk2 @ relation_dom @ relation )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[22662:[bind(A,$thf( sk2 ))]]) ).
thf(11,axiom,
! [A: $i] :
( ~ ( A @ empty )
=> ? [B: $i] :
( ~ ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_subset_1) ).
thf(83,plain,
! [A: $i] :
( ~ ( A @ empty )
=> ? [B: $i] :
( ~ ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(84,plain,
! [A: $i] :
( ( ~ ( A @ sk7 @ empty )
| ( A @ empty ) )
& ( ( A @ powerset @ ( A @ sk7 @ element ) )
| ( A @ empty ) ) ),
inference(cnf,[status(esa)],[83]) ).
thf(85,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ sk7 @ element ) )
| ( A @ empty ) ),
inference(cnfConj,[status(thm)],[84]) ).
thf(80,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ~ ( B @ powerset @ ( A @ element ) ) ),
inference(cnfConj,[status(thm)],[79]) ).
thf(973,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk7 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[85,80]) ).
thf(974,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk7 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[973]) ).
thf(975,plain,
! [A: $i] :
( ( A @ ( A @ sk7 @ subset ) )
| ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[974:[bind(A,$thf( D )),bind(B,$thf( D @ sk7 )),bind(C,$thf( D ))]]) ).
thf(988,plain,
! [A: $i] :
( ( A @ ( A @ sk7 @ subset ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[975]) ).
thf(21,axiom,
! [A: $i,B: $i,C: $i] :
~ ( ( C @ empty )
& ( C @ powerset @ ( B @ element ) )
& ( B @ ( A @ in ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
thf(116,plain,
! [A: $i,B: $i,C: $i] :
~ ( ( C @ empty )
& ( C @ powerset @ ( B @ element ) )
& ( B @ ( A @ in ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(711,plain,
! [A: $i] :
( ( ( sk1 @ identity_relation )
!= ( A @ identity_relation ) )
| ( ( sk2 @ relation_rng )
= A )
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[58,206]) ).
thf(712,plain,
( ( ( sk2 @ relation_rng )
= sk1 )
| ~ sk3 ),
inference(pattern_uni,[status(thm)],[711:[bind(A,$thf( sk1 ))]]) ).
thf(2241,plain,
( ( ( sk2 @ relation_rng )
!= ( empty_set @ relation_rng ) )
| ( sk1 @ empty )
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[712,2167]) ).
thf(2258,plain,
( ( sk2 != empty_set )
| ~ sk3
| ( sk1 @ empty ) ),
inference(simp,[status(thm)],[2241]) ).
thf(2727,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk4 @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( B @ empty )
| ~ $true
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[746,121]) ).
thf(2728,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk4 @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( B @ empty )
| ~ sk3 ),
inference(simp,[status(thm)],[2727]) ).
thf(2729,plain,
( ~ ( sk1 @ empty )
| ~ sk3 ),
inference(pattern_uni,[status(thm)],[2728:[bind(A,$thf( sk4 )),bind(B,$thf( sk1 ))]]) ).
thf(2789,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ~ $true
| ~ sk3
| ( sk2 != empty_set )
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[2258,2729]) ).
thf(2790,plain,
( ( ( sk1 @ empty )
!= ( sk1 @ empty ) )
| ( sk2 != empty_set )
| ~ sk3 ),
inference(simp,[status(thm)],[2789]) ).
thf(2791,plain,
( ( sk2 != empty_set )
| ~ sk3 ),
inference(pattern_uni,[status(thm)],[2790:[]]) ).
thf(2882,plain,
! [A: $i] :
( ( A != sk2 )
| ( empty_set != empty_set )
| ~ sk3
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,2791]) ).
thf(2883,plain,
! [A: $i] :
( ( A != sk2 )
| ~ sk3
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[2882]) ).
thf(2884,plain,
( ~ sk3
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[2883:[bind(A,$thf( sk2 ))]]) ).
thf(306,plain,
! [B: $i,A: $i] :
( ( B != sk2 )
| sk3
| ( ( A @ relation_dom )
= sk1 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[67,56]) ).
thf(307,plain,
! [A: $i] :
( sk3
| ( ( A @ relation_dom )
= sk1 )
| ~ ( sk2 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[306:[bind(A,$thf( A )),bind(B,$thf( sk2 ))]]) ).
thf(20997,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( E @ ( D @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( E @ ( D @ unordered_pair ) @ singleton @ ( empty_set @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7222]) ).
thf(20998,plain,
! [C: $i,B: $i,A: $i] :
~ ( C @ identity_relation @ ( B @ ( A @ unordered_pair ) @ singleton @ ( empty_set @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[20997:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( B ))]]) ).
thf(42,axiom,
? [A: $i] :
( ( A @ function )
& ( A @ relation ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_funct_1) ).
thf(220,plain,
? [A: $i] :
( ( A @ function )
& ( A @ relation ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(41,axiom,
( ( empty_set @ relation_empty_yielding )
& ( empty_set @ relation )
& ( empty_set @ empty ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc12_relat_1) ).
thf(215,plain,
( ( empty_set @ relation_empty_yielding )
& ( empty_set @ relation )
& ( empty_set @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(216,plain,
( ( empty_set @ relation_empty_yielding )
& ( empty_set @ relation )
& ( empty_set @ empty ) ),
inference(cnf,[status(esa)],[215]) ).
thf(219,plain,
empty_set @ relation_empty_yielding,
inference(cnfConj,[status(thm)],[216]) ).
thf(472,plain,
! [B: $i,A: $i] :
( ( B != empty_set )
| ( A @ relation_empty_yielding )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[67,219]) ).
thf(473,plain,
! [A: $i] :
( ( A @ relation_empty_yielding )
| ~ ( empty_set @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[472:[bind(A,$thf( A )),bind(B,$thf( empty_set ))]]) ).
thf(25141,plain,
! [A: $i] :
( ( A @ relation_empty_yielding )
| ~ $true
| ~ ( A @ empty ) ),
inference(rewrite,[status(thm)],[473,76]) ).
thf(25142,plain,
! [A: $i] :
( ( A @ relation_empty_yielding )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[25141]) ).
thf(25149,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_empty_yielding )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[21792,25142]) ).
thf(25150,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_empty_yielding )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[25149]) ).
thf(25151,plain,
( ( sk2 @ relation_empty_yielding )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[25150:[bind(A,$thf( sk2 ))]]) ).
thf(32613,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ singleton @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,16336]) ).
thf(32614,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ singleton @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32613]) ).
thf(32763,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( C @ singleton @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32614]) ).
thf(32872,plain,
! [B: $i,A: $i] :
( ( B @ singleton @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32763]) ).
thf(528,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk1 @ identity_relation ) )
| ~ sk3
| ( A = sk2 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[67,58]) ).
thf(529,plain,
! [A: $i] :
( ~ sk3
| ( A = sk2 )
| ~ ( sk1 @ identity_relation @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[528:[bind(A,$thf( A )),bind(B,$thf( sk1 @ identity_relation ))]]) ).
thf(6829,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ singleton ) )
| ( C != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[6100,267]) ).
thf(6830,plain,
! [C: $i,B: $i,A: $i] :
( ( B != empty_set )
| ~ ( A @ identity_relation @ ( C @ singleton @ singleton @ ( B @ ( C @ singleton @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[6829:[bind(A,$thf( A )),bind(B,$thf( E @ singleton )),bind(C,$thf( C )),bind(D,$thf( E ))]]) ).
thf(7362,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ singleton @ singleton @ ( empty_set @ ( B @ singleton @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[6830]) ).
thf(17527,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ ( D @ singleton @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( D @ singleton @ singleton @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7362]) ).
thf(17528,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ singleton @ singleton @ ( B @ singleton @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[17527:[bind(A,$thf( E @ singleton )),bind(B,$thf( empty_set )),bind(C,$thf( C )),bind(D,$thf( E ))]]) ).
thf(17773,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ singleton @ singleton @ ( B @ singleton @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[17528]) ).
thf(2968,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( C @ ( D @ unordered_pair ) ) )
| ( ( C @ singleton @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[61,2955]) ).
thf(2969,plain,
! [B: $i,A: $i] :
( ( B @ singleton @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) )
!= empty_set ),
inference(pattern_uni,[status(thm)],[2968:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(1823,plain,
! [A: $i] :
( ( A
!= ( sk4 @ ( sk2 @ apply ) ) )
| ( sk4 != empty_set )
| ~ sk3
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,743]) ).
thf(1824,plain,
( ( sk4 != empty_set )
| ~ sk3
| ~ ( sk4 @ ( sk2 @ apply ) @ empty ) ),
inference(pattern_uni,[status(thm)],[1823:[bind(A,$thf( sk4 @ ( sk2 @ apply ) ))]]) ).
thf(13674,plain,
! [A: $i] :
( ( ( empty_set @ relation_dom @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[13518,98]) ).
thf(13675,plain,
! [A: $i] :
( ( ( empty_set @ relation_dom @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[13674]) ).
thf(13676,plain,
( ( empty_set @ relation_dom )
= empty_set ),
inference(pattern_uni,[status(thm)],[13675:[bind(A,$thf( empty_set @ relation_dom ))]]) ).
thf(13775,plain,
( ( ( sk2 @ relation_dom )
!= ( empty_set @ relation_dom ) )
| sk3
| ( sk1 = empty_set ) ),
inference(paramod_ordered,[status(thm)],[13676,56]) ).
thf(13833,plain,
( ( sk2 != empty_set )
| sk3
| ( sk1 = empty_set ) ),
inference(simp,[status(thm)],[13775]) ).
thf(17175,plain,
( ( sk3 != sk3 )
| ( sk2 != empty_set )
| ~ $true
| ( sk2 != empty_set )
| ( sk1 = empty_set ) ),
inference(paramod_ordered,[status(thm)],[13833,2791]) ).
thf(17176,plain,
( ( sk3 != sk3 )
| ( sk2 != empty_set )
| ( sk1 = empty_set ) ),
inference(simp,[status(thm)],[17175]) ).
thf(17177,plain,
( ( sk2 != empty_set )
| ( sk1 = empty_set ) ),
inference(pattern_uni,[status(thm)],[17176:[]]) ).
thf(17230,plain,
! [A: $i] :
( ( A != sk2 )
| ( empty_set != empty_set )
| ( sk1 = empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,17177]) ).
thf(17231,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk1 = empty_set )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[17230]) ).
thf(17232,plain,
( ( sk1 = empty_set )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[17231:[bind(A,$thf( sk2 ))]]) ).
thf(26180,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 = empty_set )
| ~ $true
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[20707,17232]) ).
thf(26181,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk1 = empty_set )
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(simp,[status(thm)],[26180]) ).
thf(26182,plain,
( ( sk1 = empty_set )
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[26181:[]]) ).
thf(162,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ identity_relation ) )
| ~ ( B @ ( A @ ( B @ sk17 ) @ ( A @ ( B @ sk16 ) @ ordered_pair ) @ in ) )
| ( B @ ( A @ sk13 ) )
| ~ ( B @ relation ) ),
inference(cnfConj,[status(thm)],[161]) ).
thf(178,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk17 ) @ ( A @ ( B @ sk16 ) @ ordered_pair ) @ in ) )
| ( B @ ( A @ sk13 ) )
| ~ ( B @ relation )
| ( B
= ( A @ identity_relation ) ) ),
inference(lifteq,[status(thm)],[162]) ).
thf(9105,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk16 ) @ singleton @ ( A @ ( B @ sk17 ) @ ( A @ ( B @ sk16 ) @ unordered_pair ) @ unordered_pair ) @ in ) )
| ( B @ ( A @ sk13 ) )
| ~ ( B @ relation )
| ( B
= ( A @ identity_relation ) ) ),
inference(rewrite,[status(thm)],[178,89]) ).
thf(32629,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ ( B @ powerset @ identity_relation @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,23115]) ).
thf(32630,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ ( B @ powerset @ identity_relation @ in ) ) ),
inference(simp,[status(thm)],[32629]) ).
thf(32796,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) )
| ( A
!= ( B @ powerset @ identity_relation ) ) ),
inference(simp,[status(thm)],[32630]) ).
thf(32840,plain,
! [A: $i] :
( ( A @ powerset @ identity_relation @ powerset )
!= ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) ),
inference(simp,[status(thm)],[32796]) ).
thf(1757,plain,
! [A: $i] :
( ( A
!= ( sk2 @ relation_dom ) )
| ( sk1 = empty_set )
| ~ sk3
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,692]) ).
thf(1758,plain,
( ( sk1 = empty_set )
| ~ sk3
| ~ ( sk2 @ relation_dom @ empty ) ),
inference(pattern_uni,[status(thm)],[1757:[bind(A,$thf( sk2 @ relation_dom ))]]) ).
thf(2752,plain,
! [A: $i] :
( ( ( sk1 @ ( sk4 @ in ) )
!= ( empty_set @ ( A @ in ) ) )
| ~ $true
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[746,2738]) ).
thf(2753,plain,
! [A: $i] :
( ( ( sk1 @ ( sk4 @ in ) )
!= ( empty_set @ ( A @ in ) ) )
| ~ sk3 ),
inference(simp,[status(thm)],[2752]) ).
thf(2765,plain,
! [A: $i] :
( ( sk1 != empty_set )
| ( sk4 != A )
| ~ sk3 ),
inference(simp,[status(thm)],[2753]) ).
thf(2769,plain,
( ( sk1 != empty_set )
| ~ sk3 ),
inference(simp,[status(thm)],[2765]) ).
thf(10806,plain,
( ( sk1 != sk1 )
| ( empty_set != empty_set )
| ~ sk3
| ~ sk3
| ~ ( sk2 @ relation_dom @ empty ) ),
inference(paramod_ordered,[status(thm)],[1758,2769]) ).
thf(10807,plain,
( ( sk1 != sk1 )
| ~ sk3
| ~ ( sk2 @ relation_dom @ empty ) ),
inference(simp,[status(thm)],[10806]) ).
thf(10808,plain,
( ~ sk3
| ~ ( sk2 @ relation_dom @ empty ) ),
inference(pattern_uni,[status(thm)],[10807:[]]) ).
thf(22692,plain,
( ( ( sk6 @ empty )
!= ( sk2 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[21792,72]) ).
thf(22693,plain,
( ( ( sk6 @ empty )
!= ( sk2 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[22692]) ).
thf(22748,plain,
( ( sk6 != sk2 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[22693]) ).
thf(23269,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk6 != sk2 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,22748]) ).
thf(23270,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk6 != sk2 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[23269]) ).
thf(23271,plain,
( ( sk6 != sk2 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[23270:[bind(A,$thf( sk2 ))]]) ).
thf(26198,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk6 != sk2 )
| ~ $true
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[20707,23271]) ).
thf(26199,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk6 != sk2 )
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(simp,[status(thm)],[26198]) ).
thf(26200,plain,
( ( sk6 != sk2 )
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[26199:[]]) ).
thf(27038,plain,
! [A: $i] :
( ( ( A @ identity_relation @ relation_dom )
!= ( sk2 @ relation_dom ) )
| ( sk6 != sk2 )
| ( A != empty_set ) ),
inference(paramod_ordered,[status(thm)],[204,26200]) ).
thf(27082,plain,
( ( ( empty_set @ identity_relation )
!= sk2 )
| ( sk6 != sk2 ) ),
inference(simp,[status(thm)],[27038]) ).
thf(41578,plain,
( ( sk10 != sk10 )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ element ) )
| ( sk1 = empty_set )
| sk3
| ( empty_set @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[5981,39910]) ).
thf(41579,plain,
( ( sk10 != sk10 )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ element ) )
| ( sk1 = empty_set )
| sk3
| ( empty_set @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(simp,[status(thm)],[41578]) ).
thf(41580,plain,
( ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ element ) )
| ( sk1 = empty_set )
| sk3
| ( empty_set @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[41579:[]]) ).
thf(1786,plain,
! [A: $i] :
( ( A != sk4 )
| ( sk1 @ ( empty_set @ in ) )
| ~ sk3
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,746]) ).
thf(1787,plain,
( ( sk1 @ ( empty_set @ in ) )
| ~ sk3
| ~ ( sk4 @ empty ) ),
inference(pattern_uni,[status(thm)],[1786:[bind(A,$thf( sk4 ))]]) ).
thf(22659,plain,
( ( ( sk12 @ empty )
!= ( sk2 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[21792,155]) ).
thf(22660,plain,
( ( ( sk12 @ empty )
!= ( sk2 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[22659]) ).
thf(22754,plain,
( ( sk12 != sk2 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[22660]) ).
thf(32625,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ powerset @ singleton @ ( empty_set @ ( C @ powerset @ unordered_pair ) @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,7112]) ).
thf(32626,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ powerset @ singleton @ ( empty_set @ ( C @ powerset @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32625]) ).
thf(32779,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( C @ powerset @ singleton @ ( empty_set @ ( C @ powerset @ unordered_pair ) @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32626]) ).
thf(32820,plain,
! [B: $i,A: $i] :
( ( B @ powerset @ singleton @ ( empty_set @ ( B @ powerset @ unordered_pair ) @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32779]) ).
thf(8263,plain,
! [A: $i] :
( ( A != sk4 )
| ( ( empty_set @ ( sk2 @ apply ) )
!= empty_set )
| ~ sk3
| ~ ( sk4 @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,4439]) ).
thf(8264,plain,
( ( ( empty_set @ ( sk2 @ apply ) )
!= empty_set )
| ~ sk3
| ~ ( sk4 @ empty )
| ~ ( sk4 @ empty ) ),
inference(pattern_uni,[status(thm)],[8263:[bind(A,$thf( sk4 ))]]) ).
thf(8314,plain,
( ( ( empty_set @ ( sk2 @ apply ) )
!= empty_set )
| ~ sk3
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[8264]) ).
thf(27559,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ ( D @ powerset @ identity_relation @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( D @ powerset @ identity_relation @ singleton @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,23251]) ).
thf(27560,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ powerset @ identity_relation @ singleton @ ( B @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[27559:[bind(A,$thf( F @ powerset @ identity_relation )),bind(B,$thf( empty_set )),bind(C,$thf( C )),bind(D,$thf( F ))]]) ).
thf(27886,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ powerset @ identity_relation @ singleton @ ( B @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[27560]) ).
thf(156,plain,
sk12 @ relation,
inference(cnfConj,[status(thm)],[154]) ).
thf(21289,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( D @ ( C @ unordered_pair ) @ singleton @ ( empty_set @ ( C @ ( D @ unordered_pair ) @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( E @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,20998]) ).
thf(21290,plain,
! [C: $i,B: $i,A: $i] :
~ ( A @ identity_relation @ ( empty_set @ ( B @ ( C @ unordered_pair ) @ unordered_pair ) @ ( C @ ( B @ unordered_pair ) @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[21289:[bind(A,$thf( empty_set @ ( K @ ( L @ unordered_pair ) @ unordered_pair ) )),bind(B,$thf( L @ ( K @ unordered_pair ) @ singleton )),bind(C,$thf( K )),bind(D,$thf( L )),bind(E,$thf( E ))]]) ).
thf(21498,plain,
! [C: $i,B: $i,A: $i] :
~ ( A @ identity_relation @ ( empty_set @ ( B @ ( C @ unordered_pair ) @ unordered_pair ) @ ( C @ ( B @ unordered_pair ) @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[21290]) ).
thf(20649,plain,
( ( ( sk2 @ relation_dom )
!= ( sk2 @ relation_dom ) )
| ~ ( sk1 @ empty )
| ( sk2 @ empty )
| sk3 ),
inference(paramod_ordered,[status(thm)],[56,14391]) ).
thf(20650,plain,
( ~ ( sk1 @ empty )
| ( sk2 @ empty )
| sk3 ),
inference(pattern_uni,[status(thm)],[20649:[]]) ).
thf(25004,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ~ $true
| ( sk2 @ empty )
| sk3 ),
inference(paramod_ordered,[status(thm)],[76,20650]) ).
thf(25005,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk2 @ empty )
| sk3 ),
inference(simp,[status(thm)],[25004]) ).
thf(25127,plain,
( ( sk1 != empty_set )
| ( sk2 @ empty )
| sk3 ),
inference(simp,[status(thm)],[25005]) ).
thf(13457,plain,
! [A: $i] :
( ( ( sk2 @ relation_dom )
!= ( A @ relation_dom ) )
| ( sk1 @ empty )
| ~ ( A @ empty )
| sk3 ),
inference(paramod_ordered,[status(thm)],[56,197]) ).
thf(13458,plain,
( ( sk1 @ empty )
| ~ ( sk2 @ empty )
| sk3 ),
inference(pattern_uni,[status(thm)],[13457:[bind(A,$thf( sk2 ))]]) ).
thf(23311,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk12 != sk2 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,22754]) ).
thf(23312,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk12 != sk2 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[23311]) ).
thf(23313,plain,
( ( sk12 != sk2 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[23312:[bind(A,$thf( sk2 ))]]) ).
thf(26293,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk12 != sk2 )
| ~ $true
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[20707,23313]) ).
thf(26294,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk12 != sk2 )
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(simp,[status(thm)],[26293]) ).
thf(26295,plain,
( ( sk12 != sk2 )
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[26294:[]]) ).
thf(27117,plain,
! [A: $i] :
( ( ( A @ identity_relation @ relation_dom )
!= ( sk2 @ relation_dom ) )
| ( sk12 != sk2 )
| ( A != empty_set ) ),
inference(paramod_ordered,[status(thm)],[204,26295]) ).
thf(27161,plain,
( ( ( empty_set @ identity_relation )
!= sk2 )
| ( sk12 != sk2 ) ),
inference(simp,[status(thm)],[27117]) ).
thf(25731,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk2 @ relation_empty_yielding )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,25151]) ).
thf(25732,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk2 @ relation_empty_yielding )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[25731]) ).
thf(25733,plain,
( ( sk2 @ relation_empty_yielding )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[25732:[bind(A,$thf( sk2 ))]]) ).
thf(773,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk9 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,80]) ).
thf(774,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk9 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) ) ),
inference(simp,[status(thm)],[773]) ).
thf(775,plain,
! [A: $i] : ( A @ ( A @ powerset @ sk9 @ subset ) ),
inference(pattern_uni,[status(thm)],[774:[bind(A,$thf( E @ powerset )),bind(B,$thf( E @ powerset @ sk9 )),bind(C,$thf( E ))]]) ).
thf(783,plain,
! [A: $i] : ( A @ ( A @ powerset @ sk9 @ subset ) ),
inference(simp,[status(thm)],[775]) ).
thf(5940,plain,
! [A: $i] :
( ( ( empty_set @ identity_relation )
!= ( A @ identity_relation ) )
| ( ( sk10 @ relation_dom )
= A )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[5603,204]) ).
thf(5941,plain,
( ( ( sk10 @ relation_dom )
= empty_set )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[5940:[bind(A,$thf( empty_set ))]]) ).
thf(15853,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ singleton @ ( D @ powerset @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7113]) ).
thf(15854,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ powerset @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[15853:[bind(A,$thf( G @ powerset @ ( empty_set @ unordered_pair ) )),bind(B,$thf( empty_set @ singleton )),bind(C,$thf( C )),bind(D,$thf( G ))]]) ).
thf(16078,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ powerset @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[15854]) ).
thf(32752,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ powerset @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,16078]) ).
thf(32753,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ powerset @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32752]) ).
thf(32784,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( C @ powerset @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32753]) ).
thf(32827,plain,
! [B: $i,A: $i] :
( ( B @ powerset @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32784]) ).
thf(6163,plain,
! [C: $i,B: $i,A: $i] :
( ( C != sk12 )
| ( B != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[6100,234]) ).
thf(6164,plain,
! [B: $i,A: $i] :
( ( B != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( sk12 @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[6163:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( sk12 ))]]) ).
thf(7099,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( empty_set @ singleton @ ( sk12 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[6164]) ).
thf(7685,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ singleton @ ( sk12 @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7099]) ).
thf(7686,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( sk12 @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[7685:[bind(A,$thf( sk12 @ ( empty_set @ unordered_pair ) )),bind(B,$thf( empty_set @ singleton )),bind(C,$thf( C ))]]) ).
thf(7821,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( sk12 @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[7686]) ).
thf(6161,plain,
! [C: $i,B: $i,A: $i] :
( ( B != sk12 )
| ( C != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[6100,234]) ).
thf(6162,plain,
! [B: $i,A: $i] :
( ( B != empty_set )
| ~ ( A @ identity_relation @ ( sk12 @ singleton @ ( B @ ( sk12 @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[6161:[bind(A,$thf( A )),bind(B,$thf( sk12 ))]]) ).
thf(7098,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( sk12 @ singleton @ ( empty_set @ ( sk12 @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[6162]) ).
thf(7495,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ ( sk12 @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( sk12 @ singleton @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7098]) ).
thf(7496,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( sk12 @ singleton @ ( sk12 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[7495:[bind(A,$thf( sk12 )),bind(B,$thf( empty_set ))]]) ).
thf(7658,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( sk12 @ singleton @ ( sk12 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[7496]) ).
thf(32692,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk12 @ singleton @ ( sk12 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,7658]) ).
thf(32693,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk12 @ singleton @ ( sk12 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32692]) ).
thf(32782,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( sk12 @ singleton @ ( sk12 @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32693]) ).
thf(32824,plain,
! [A: $i] :
( ( sk12 @ singleton @ ( sk12 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32782]) ).
thf(27211,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk9 @ in ) )
!= ( sk1 @ ( B @ in ) ) )
| ~ $true
| sk3
| ( ( B @ ( sk2 @ apply ) )
= B )
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[12554,53]) ).
thf(27212,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ sk9 @ in ) )
!= ( sk1 @ ( B @ in ) ) )
| sk3
| ( ( B @ ( sk2 @ apply ) )
= B )
| ( A @ empty ) ),
inference(simp,[status(thm)],[27211]) ).
thf(27213,plain,
( sk3
| ( ( sk1 @ sk9 @ ( sk2 @ apply ) )
= ( sk1 @ sk9 ) )
| ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[27212:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ sk9 ))]]) ).
thf(25068,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk12 != sk2 )
| ~ $true
| ~ ( sk1 @ empty )
| sk3 ),
inference(paramod_ordered,[status(thm)],[20650,23313]) ).
thf(25069,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk12 != sk2 )
| ~ ( sk1 @ empty )
| sk3 ),
inference(simp,[status(thm)],[25068]) ).
thf(25070,plain,
( ( sk12 != sk2 )
| ~ ( sk1 @ empty )
| sk3 ),
inference(pattern_uni,[status(thm)],[25069:[]]) ).
thf(10212,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( sk6 @ singleton @ ( sk6 @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,8030]) ).
thf(10213,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( sk6 @ ( empty_set @ unordered_pair ) @ ( sk6 @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[10212:[bind(A,$thf( sk6 @ ( empty_set @ unordered_pair ) )),bind(B,$thf( sk6 @ singleton )),bind(C,$thf( C ))]]) ).
thf(10401,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( sk6 @ ( empty_set @ unordered_pair ) @ ( sk6 @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[10213]) ).
thf(25,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ powerset @ ( B @ element ) )
& ( B @ ( A @ in ) ) )
=> ( C @ ( A @ element ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
thf(128,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ powerset @ ( B @ element ) )
& ( B @ ( A @ in ) ) )
=> ( C @ ( A @ element ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(129,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ element ) )
| ~ ( C @ powerset @ ( B @ element ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[128]) ).
thf(7497,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( sk12 @ singleton @ ( empty_set @ ( sk12 @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7098]) ).
thf(7498,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( empty_set @ ( sk12 @ unordered_pair ) @ ( sk12 @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[7497:[bind(A,$thf( empty_set @ ( sk12 @ unordered_pair ) )),bind(B,$thf( sk12 @ singleton )),bind(C,$thf( C ))]]) ).
thf(7661,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( empty_set @ ( sk12 @ unordered_pair ) @ ( sk12 @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[7498]) ).
thf(26,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ function )
& ( C @ relation ) )
=> ( ( C @ ( B @ ( A @ ordered_pair ) @ in ) )
<=> ( ( B
= ( A @ ( C @ apply ) ) )
& ( C @ relation_dom @ ( A @ in ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_funct_1) ).
thf(130,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ function )
& ( C @ relation ) )
=> ( ( ( ( B
= ( A @ ( C @ apply ) ) )
& ( C @ relation_dom @ ( A @ in ) ) )
=> ( C @ ( B @ ( A @ ordered_pair ) @ in ) ) )
& ( ( C @ ( B @ ( A @ ordered_pair ) @ in ) )
=> ( ( B
= ( A @ ( C @ apply ) ) )
& ( C @ relation_dom @ ( A @ in ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(131,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ ordered_pair ) @ in ) )
| ( B
!= ( A @ ( C @ apply ) ) )
| ~ ( C @ relation_dom @ ( A @ in ) )
| ~ ( C @ function )
| ~ ( C @ relation ) )
& ( ( B
= ( A @ ( C @ apply ) ) )
| ~ ( C @ ( B @ ( A @ ordered_pair ) @ in ) )
| ~ ( C @ function )
| ~ ( C @ relation ) )
& ( ( C @ relation_dom @ ( A @ in ) )
| ~ ( C @ ( B @ ( A @ ordered_pair ) @ in ) )
| ~ ( C @ function )
| ~ ( C @ relation ) ) ),
inference(cnf,[status(esa)],[130]) ).
thf(132,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ relation_dom @ ( A @ in ) )
| ~ ( C @ ( B @ ( A @ ordered_pair ) @ in ) )
| ~ ( C @ function )
| ~ ( C @ relation ) ),
inference(cnfConj,[status(thm)],[131]) ).
thf(3225,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ relation_dom @ ( A @ in ) )
| ~ ( C @ ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) @ in ) )
| ~ ( C @ function )
| ~ ( C @ relation ) ),
inference(rewrite,[status(thm)],[132,89]) ).
thf(1251,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( C @ singleton @ ( D @ ( C @ unordered_pair ) @ unordered_pair ) ) )
| ( ( A @ ( B @ unordered_pair ) )
!= sk5 ) ),
inference(paramod_ordered,[status(thm)],[61,1222]) ).
thf(1252,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ unordered_pair ) @ ( B @ singleton @ unordered_pair ) )
!= sk5 ),
inference(pattern_uni,[status(thm)],[1251:[bind(A,$thf( F @ ( G @ unordered_pair ) )),bind(B,$thf( G @ singleton )),bind(C,$thf( G )),bind(D,$thf( F ))]]) ).
thf(1273,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ unordered_pair ) @ ( B @ singleton @ unordered_pair ) )
!= sk5 ),
inference(simp,[status(thm)],[1252]) ).
thf(3158,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ unordered_pair ) @ ( B @ singleton @ unordered_pair ) )
!= empty_set ),
inference(rewrite,[status(thm)],[1273,1709]) ).
thf(3172,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( C @ ( D @ unordered_pair ) ) )
| ( ( A @ ( B @ unordered_pair ) @ ( D @ singleton @ unordered_pair ) )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[61,3158]) ).
thf(3173,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ unordered_pair ) @ ( A @ singleton @ unordered_pair ) )
!= empty_set ),
inference(pattern_uni,[status(thm)],[3172:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(23408,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation @ ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) )
!= ( C @ ( B @ in ) ) )
| ~ ( B @ ( C @ in ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[23101,188]) ).
thf(23409,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation @ ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) )
!= ( C @ ( B @ in ) ) )
| ~ ( B @ ( C @ in ) ) ),
inference(simp,[status(thm)],[23408]) ).
thf(23410,plain,
! [A: $i] :
~ ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ ( A @ powerset @ identity_relation @ in ) ),
inference(pattern_uni,[status(thm)],[23409:[bind(A,$thf( J )),bind(B,$thf( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) )),bind(C,$thf( J @ powerset @ identity_relation ))]]) ).
thf(23709,plain,
! [A: $i] :
~ ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ ( A @ powerset @ identity_relation @ in ) ),
inference(simp,[status(thm)],[23410]) ).
thf(32717,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ ( B @ powerset @ identity_relation @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,23709]) ).
thf(32718,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ ( B @ powerset @ identity_relation @ in ) ) ),
inference(simp,[status(thm)],[32717]) ).
thf(32766,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) ) )
| ( A
!= ( B @ powerset @ identity_relation ) ) ),
inference(simp,[status(thm)],[32718]) ).
thf(32875,plain,
! [A: $i] :
( ( A @ powerset @ identity_relation @ powerset )
!= ( empty_set @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) ) ),
inference(simp,[status(thm)],[32766]) ).
thf(2660,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( empty_set @ sk16 ) @ in ) )
!= ( sk1 @ ( B @ in ) ) )
| ~ $true
| sk3
| ( ( B @ ( sk2 @ apply ) )
= B )
| ( empty_set @ ( A @ sk13 ) )
| ( ( A @ identity_relation )
= empty_set ) ),
inference(paramod_ordered,[status(thm)],[1357,53]) ).
thf(2661,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( empty_set @ sk16 ) @ in ) )
!= ( sk1 @ ( B @ in ) ) )
| sk3
| ( ( B @ ( sk2 @ apply ) )
= B )
| ( empty_set @ ( A @ sk13 ) )
| ( ( A @ identity_relation )
= empty_set ) ),
inference(simp,[status(thm)],[2660]) ).
thf(2662,plain,
( sk3
| ( ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) )
= ( sk1 @ ( empty_set @ sk16 ) ) )
| ( empty_set @ ( sk1 @ sk13 ) )
| ( ( sk1 @ identity_relation )
= empty_set ) ),
inference(pattern_uni,[status(thm)],[2661:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ ( empty_set @ sk16 ) ))]]) ).
thf(1731,plain,
! [A: $i] :
( ( A
!= ( sk2 @ relation_dom ) )
| sk3
| ( sk1 = empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,56]) ).
thf(1732,plain,
( sk3
| ( sk1 = empty_set )
| ~ ( sk2 @ relation_dom @ empty ) ),
inference(pattern_uni,[status(thm)],[1731:[bind(A,$thf( sk2 @ relation_dom ))]]) ).
thf(22797,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation @ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) )
!= ( C @ ( B @ in ) ) )
| ~ ( C @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22553,121]) ).
thf(22798,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation @ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) )
!= ( C @ ( B @ in ) ) )
| ~ ( C @ empty ) ),
inference(simp,[status(thm)],[22797]) ).
thf(22799,plain,
! [A: $i] :
~ ( A @ powerset @ identity_relation @ empty ),
inference(pattern_uni,[status(thm)],[22798:[bind(A,$thf( J )),bind(B,$thf( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) )),bind(C,$thf( J @ powerset @ identity_relation ))]]) ).
thf(23099,plain,
! [A: $i] :
~ ( A @ powerset @ identity_relation @ empty ),
inference(simp,[status(thm)],[22799]) ).
thf(37,axiom,
! [A: $i] :
( ( A @ empty )
=> ( A @ function ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_funct_1) ).
thf(207,plain,
! [A: $i] :
( ( A @ empty )
=> ( A @ function ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(208,plain,
! [A: $i] :
( ( A @ function )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[207]) ).
thf(14532,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ $true
| ( sk2 != empty_set )
| sk3 ),
inference(paramod_ordered,[status(thm)],[13751,208]) ).
thf(14533,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ( sk2 != empty_set )
| sk3 ),
inference(simp,[status(thm)],[14532]) ).
thf(14534,plain,
( ( sk1 @ function )
| ( sk2 != empty_set )
| sk3 ),
inference(pattern_uni,[status(thm)],[14533:[bind(A,$thf( sk1 ))]]) ).
thf(4560,plain,
( ( ( sk4 @ ( sk2 @ apply ) @ empty )
!= ( empty_set @ empty ) )
| ( sk4 != empty_set )
| ~ sk3
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,1824]) ).
thf(4561,plain,
( ( ( sk4 @ ( sk2 @ apply ) @ empty )
!= ( empty_set @ empty ) )
| ( sk4 != empty_set )
| ~ sk3 ),
inference(simp,[status(thm)],[4560]) ).
thf(4599,plain,
( ( ( sk4 @ ( sk2 @ apply ) )
!= empty_set )
| ( sk4 != empty_set )
| ~ sk3 ),
inference(simp,[status(thm)],[4561]) ).
thf(14539,plain,
( ( ( sk12 @ empty )
!= ( sk1 @ empty ) )
| ~ $true
| ( sk2 != empty_set )
| sk3 ),
inference(paramod_ordered,[status(thm)],[13751,155]) ).
thf(14540,plain,
( ( ( sk12 @ empty )
!= ( sk1 @ empty ) )
| ( sk2 != empty_set )
| sk3 ),
inference(simp,[status(thm)],[14539]) ).
thf(14603,plain,
( ( sk12 != sk1 )
| ( sk2 != empty_set )
| sk3 ),
inference(simp,[status(thm)],[14540]) ).
thf(20897,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk12 != sk1 )
| ( empty_set != empty_set )
| sk3
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,14603]) ).
thf(20898,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk12 != sk1 )
| sk3
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[20897]) ).
thf(20899,plain,
( ( sk12 != sk1 )
| sk3
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[20898:[bind(A,$thf( sk2 ))]]) ).
thf(21694,plain,
( ( sk10 != sk10 )
| sk3
| ( ( sk1 @ ( sk10 @ sk16 ) @ ( sk2 @ apply ) )
= ( sk1 @ ( sk10 @ sk16 ) ) )
| ( empty_set @ ( sk1 @ sk13 ) )
| ( ( sk1 @ identity_relation )
= sk10 )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[5981,5580]) ).
thf(21695,plain,
( sk3
| ( ( sk1 @ ( sk10 @ sk16 ) @ ( sk2 @ apply ) )
= ( sk1 @ ( sk10 @ sk16 ) ) )
| ( empty_set @ ( sk1 @ sk13 ) )
| ( ( sk1 @ identity_relation )
= sk10 )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[21694:[]]) ).
thf(32650,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( C @ ( B @ in ) ) )
| ~ ( B @ ( C @ in ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,188]) ).
thf(32651,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( C @ ( B @ in ) ) )
| ~ ( B @ ( C @ in ) ) ),
inference(simp,[status(thm)],[32650]) ).
thf(32652,plain,
! [A: $i] :
~ ( A @ ( A @ powerset @ in ) ),
inference(pattern_uni,[status(thm)],[32651:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ powerset ))]]) ).
thf(32821,plain,
! [A: $i] :
~ ( A @ ( A @ powerset @ in ) ),
inference(simp,[status(thm)],[32652]) ).
thf(33001,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( B @ powerset @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,32821]) ).
thf(33002,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( B @ powerset @ in ) ) ),
inference(simp,[status(thm)],[33001]) ).
thf(33024,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= B )
| ( A
!= ( B @ powerset ) ) ),
inference(simp,[status(thm)],[33002]) ).
thf(33032,plain,
! [A: $i] :
( ( A @ powerset @ powerset )
!= A ),
inference(simp,[status(thm)],[33024]) ).
thf(13497,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2304,197]) ).
thf(13498,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ empty ) ),
inference(simp,[status(thm)],[13497]) ).
thf(13499,plain,
empty_set @ relation_rng @ relation_dom @ empty,
inference(pattern_uni,[status(thm)],[13498:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(13847,plain,
empty_set @ relation_dom @ empty,
inference(rewrite,[status(thm)],[13499,2232]) ).
thf(663,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ordered_pair ) @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,107]) ).
thf(664,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[663]) ).
thf(676,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) )
!= empty_set ),
inference(simp,[status(thm)],[664]) ).
thf(1226,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) )
!= empty_set ),
inference(rewrite,[status(thm)],[676,89]) ).
thf(6475,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C
!= ( E @ ( D @ unordered_pair ) ) )
| ( B != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[6100,654]) ).
thf(6476,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B != empty_set )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( D @ ( C @ unordered_pair ) @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[6475:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( G @ ( F @ unordered_pair ) )),bind(D,$thf( F )),bind(E,$thf( G ))]]) ).
thf(7223,plain,
! [C: $i,B: $i,A: $i] :
~ ( A @ identity_relation @ ( empty_set @ singleton @ ( C @ ( B @ unordered_pair ) @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[6476]) ).
thf(1751,plain,
! [A: $i] :
( ( A != sk1 )
| sk3
| ( ( empty_set @ identity_relation )
!= sk2 )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,57]) ).
thf(1752,plain,
( sk3
| ( ( empty_set @ identity_relation )
!= sk2 )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[1751:[bind(A,$thf( sk1 ))]]) ).
thf(117,plain,
~ ? [A: $i,B: $i] :
( ? [C: $i] :
( ( C @ empty )
& ( C @ powerset @ ( B @ element ) ) )
& ( B @ ( A @ in ) ) ),
inference(miniscope,[status(thm)],[116]) ).
thf(118,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ empty )
| ~ ( C @ powerset @ ( B @ element ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[117]) ).
thf(27947,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ ( D @ powerset @ identity_relation @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ ( D @ powerset @ identity_relation @ singleton @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,27885]) ).
thf(27948,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ ( B @ powerset @ identity_relation @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[27947:[bind(A,$thf( F @ powerset @ identity_relation )),bind(B,$thf( empty_set )),bind(C,$thf( C )),bind(D,$thf( F ))]]) ).
thf(28219,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ ( B @ powerset @ identity_relation @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[27948]) ).
thf(25143,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_empty_yielding )
| ~ $true
| ( sk2 != empty_set )
| sk3 ),
inference(paramod_ordered,[status(thm)],[13751,25142]) ).
thf(25144,plain,
! [A: $i] :
( ( ( sk1 @ empty )
!= ( A @ empty ) )
| ( A @ relation_empty_yielding )
| ( sk2 != empty_set )
| sk3 ),
inference(simp,[status(thm)],[25143]) ).
thf(25145,plain,
( ( sk1 @ relation_empty_yielding )
| ( sk2 != empty_set )
| sk3 ),
inference(pattern_uni,[status(thm)],[25144:[bind(A,$thf( sk1 ))]]) ).
thf(21001,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( E @ ( D @ unordered_pair ) @ singleton @ ( empty_set @ ( E @ ( D @ unordered_pair ) @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7222]) ).
thf(21002,plain,
! [C: $i,B: $i,A: $i] :
~ ( A @ identity_relation @ ( empty_set @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ ( C @ ( B @ unordered_pair ) @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[21001:[bind(A,$thf( empty_set @ ( L @ ( K @ unordered_pair ) @ unordered_pair ) )),bind(B,$thf( L @ ( K @ unordered_pair ) @ singleton )),bind(C,$thf( C )),bind(D,$thf( K )),bind(E,$thf( L ))]]) ).
thf(21186,plain,
! [C: $i,B: $i,A: $i] :
~ ( A @ identity_relation @ ( empty_set @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ ( C @ ( B @ unordered_pair ) @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[21002]) ).
thf(32619,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ powerset @ ( empty_set @ unordered_pair ) @ ( C @ powerset @ singleton @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,17972]) ).
thf(32620,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ powerset @ ( empty_set @ unordered_pair ) @ ( C @ powerset @ singleton @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32619]) ).
thf(32794,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( C @ powerset @ ( empty_set @ unordered_pair ) @ ( C @ powerset @ singleton @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32620]) ).
thf(32837,plain,
! [B: $i,A: $i] :
( ( B @ powerset @ ( empty_set @ unordered_pair ) @ ( B @ powerset @ singleton @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32794]) ).
thf(86,plain,
! [A: $i] :
( ~ ( A @ sk7 @ empty )
| ( A @ empty ) ),
inference(cnfConj,[status(thm)],[84]) ).
thf(32704,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk12 @ singleton @ ( empty_set @ ( sk12 @ unordered_pair ) @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,7098]) ).
thf(32705,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk12 @ singleton @ ( empty_set @ ( sk12 @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32704]) ).
thf(32787,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( sk12 @ singleton @ ( empty_set @ ( sk12 @ unordered_pair ) @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32705]) ).
thf(32830,plain,
! [A: $i] :
( ( sk12 @ singleton @ ( empty_set @ ( sk12 @ unordered_pair ) @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32787]) ).
thf(26399,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ singleton @ ( D @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,23253]) ).
thf(26400,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[26399:[bind(A,$thf( H @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) )),bind(B,$thf( empty_set @ singleton )),bind(C,$thf( C )),bind(D,$thf( H ))]]) ).
thf(26616,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[26400]) ).
thf(32738,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,26616]) ).
thf(32739,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32738]) ).
thf(32760,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( C @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32739]) ).
thf(32868,plain,
! [B: $i,A: $i] :
( ( B @ powerset @ identity_relation @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32760]) ).
thf(418,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| sk3
| ( ( A @ identity_relation )
!= sk2 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[67,57]) ).
thf(419,plain,
! [A: $i] :
( sk3
| ( ( A @ identity_relation )
!= sk2 )
| ~ ( sk1 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[418:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(14002,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2304,198]) ).
thf(14003,plain,
! [A: $i] :
( ( ( empty_set @ relation_rng @ empty )
!= ( A @ empty ) )
| ( A @ relation_dom @ relation ) ),
inference(simp,[status(thm)],[14002]) ).
thf(14004,plain,
empty_set @ relation_rng @ relation_dom @ relation,
inference(pattern_uni,[status(thm)],[14003:[bind(A,$thf( empty_set @ relation_rng ))]]) ).
thf(14193,plain,
empty_set @ relation_dom @ relation,
inference(rewrite,[status(thm)],[14004,2232]) ).
thf(20831,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk1 @ function )
| ( empty_set != empty_set )
| sk3
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,14534]) ).
thf(20832,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk1 @ function )
| sk3
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[20831]) ).
thf(20833,plain,
( ( sk1 @ function )
| sk3
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[20832:[bind(A,$thf( sk2 ))]]) ).
thf(879,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( D @ ( C @ unordered_pair ) ) )
| ( ( A @ ( B @ unordered_pair ) )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[61,654]) ).
thf(880,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ unordered_pair ) )
!= empty_set ),
inference(pattern_uni,[status(thm)],[879:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(33507,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk6 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[22614,72]) ).
thf(33508,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( sk6 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[33507]) ).
thf(33579,plain,
( ( ( sk2 @ relation_dom )
!= sk6 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[33508]) ).
thf(13030,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk4 @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( A @ ( B @ in ) )
| ~ $true
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[746,188]) ).
thf(13031,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk4 @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( A @ ( B @ in ) )
| ~ sk3 ),
inference(simp,[status(thm)],[13030]) ).
thf(13032,plain,
( ~ ( sk4 @ ( sk1 @ in ) )
| ~ sk3 ),
inference(pattern_uni,[status(thm)],[13031:[bind(A,$thf( sk4 )),bind(B,$thf( sk1 ))]]) ).
thf(32732,plain,
! [A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( sk4 @ ( sk1 @ in ) ) )
| ~ $true
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[32608,13032]) ).
thf(32733,plain,
! [A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( sk4 @ ( sk1 @ in ) ) )
| ~ sk3 ),
inference(simp,[status(thm)],[32732]) ).
thf(32798,plain,
! [A: $i] :
( ( ( A @ powerset )
!= sk4 )
| ( A != sk1 )
| ~ sk3 ),
inference(simp,[status(thm)],[32733]) ).
thf(32842,plain,
( ( ( sk1 @ powerset )
!= sk4 )
| ~ sk3 ),
inference(simp,[status(thm)],[32798]) ).
thf(26218,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[20707,98]) ).
thf(26219,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(simp,[status(thm)],[26218]) ).
thf(26220,plain,
( ( sk2 = empty_set )
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[26219:[bind(A,$thf( sk2 ))]]) ).
thf(32664,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk6 @ ( empty_set @ unordered_pair ) @ ( sk6 @ singleton @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,10401]) ).
thf(32665,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk6 @ ( empty_set @ unordered_pair ) @ ( sk6 @ singleton @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32664]) ).
thf(32805,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( sk6 @ ( empty_set @ unordered_pair ) @ ( sk6 @ singleton @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32665]) ).
thf(32851,plain,
! [A: $i] :
( ( sk6 @ ( empty_set @ unordered_pair ) @ ( sk6 @ singleton @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32805]) ).
thf(32609,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk6 @ singleton @ ( sk6 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,8030]) ).
thf(32610,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk6 @ singleton @ ( sk6 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32609]) ).
thf(32793,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( sk6 @ singleton @ ( sk6 @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32610]) ).
thf(32836,plain,
! [A: $i] :
( ( sk6 @ singleton @ ( sk6 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32793]) ).
thf(134,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ ordered_pair ) @ in ) )
| ( B
!= ( A @ ( C @ apply ) ) )
| ~ ( C @ relation_dom @ ( A @ in ) )
| ~ ( C @ function )
| ~ ( C @ relation ) ),
inference(cnfConj,[status(thm)],[131]) ).
thf(136,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ ordered_pair ) @ in ) )
| ~ ( C @ relation_dom @ ( A @ in ) )
| ~ ( C @ function )
| ~ ( C @ relation )
| ( B
!= ( A @ ( C @ apply ) ) ) ),
inference(lifteq,[status(thm)],[134]) ).
thf(137,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ apply ) @ ( A @ ordered_pair ) @ in ) )
| ~ ( B @ relation_dom @ ( A @ in ) )
| ~ ( B @ function )
| ~ ( B @ relation ) ),
inference(simp,[status(thm)],[136]) ).
thf(3747,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ singleton @ ( A @ ( B @ apply ) @ ( A @ unordered_pair ) @ unordered_pair ) @ in ) )
| ~ ( B @ relation_dom @ ( A @ in ) )
| ~ ( B @ function )
| ~ ( B @ relation ) ),
inference(rewrite,[status(thm)],[137,89]) ).
thf(4398,plain,
! [A: $i] :
( ( A != sk4 )
| ~ sk3
| ~ ( sk4 @ empty )
| ~ ( empty_set @ ( sk2 @ apply ) @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,859]) ).
thf(4399,plain,
( ~ sk3
| ~ ( sk4 @ empty )
| ~ ( empty_set @ ( sk2 @ apply ) @ empty )
| ~ ( sk4 @ empty ) ),
inference(pattern_uni,[status(thm)],[4398:[bind(A,$thf( sk4 ))]]) ).
thf(4445,plain,
( ~ sk3
| ~ ( empty_set @ ( sk2 @ apply ) @ empty )
| ~ ( sk4 @ empty ) ),
inference(simp,[status(thm)],[4399]) ).
thf(40,axiom,
! [A: $i] : ( A @ identity_relation @ relation ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_relat_1) ).
thf(213,plain,
! [A: $i] : ( A @ identity_relation @ relation ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(18891,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( D @ singleton @ singleton @ ( D @ singleton @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,17773]) ).
thf(18892,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ singleton @ ( empty_set @ unordered_pair ) @ ( B @ singleton @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[18891:[bind(A,$thf( I @ singleton @ ( empty_set @ unordered_pair ) )),bind(B,$thf( I @ singleton @ singleton )),bind(C,$thf( C )),bind(D,$thf( I ))]]) ).
thf(19103,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ singleton @ ( empty_set @ unordered_pair ) @ ( B @ singleton @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[18892]) ).
thf(38805,plain,
! [A: $i] :
( ( A != sk2 )
| ( ( sk2 @ relation_dom )
!= sk6 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,33579]) ).
thf(38806,plain,
! [A: $i] :
( ( A != sk2 )
| ( ( sk2 @ relation_dom )
!= sk6 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[38805]) ).
thf(38807,plain,
( ( ( sk2 @ relation_dom )
!= sk6 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[38806:[bind(A,$thf( sk2 ))]]) ).
thf(32702,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ singleton @ ( empty_set @ unordered_pair ) @ ( C @ singleton @ singleton @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,19103]) ).
thf(32703,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ singleton @ ( empty_set @ unordered_pair ) @ ( C @ singleton @ singleton @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32702]) ).
thf(32772,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( C @ singleton @ ( empty_set @ unordered_pair ) @ ( C @ singleton @ singleton @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32703]) ).
thf(32813,plain,
! [B: $i,A: $i] :
( ( B @ singleton @ ( empty_set @ unordered_pair ) @ ( B @ singleton @ singleton @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32772]) ).
thf(221,plain,
( ( sk18 @ function )
& ( sk18 @ relation ) ),
inference(cnf,[status(esa)],[220]) ).
thf(223,plain,
sk18 @ function,
inference(cnfConj,[status(thm)],[221]) ).
thf(1257,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ unordered_pair ) )
!= ( D @ ( C @ unordered_pair ) ) )
| ( ( C @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) )
!= sk5 ) ),
inference(paramod_ordered,[status(thm)],[61,1222]) ).
thf(1258,plain,
! [B: $i,A: $i] :
( ( B @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) )
!= sk5 ),
inference(pattern_uni,[status(thm)],[1257:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(3110,plain,
! [B: $i,A: $i] :
( ( B @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) )
!= empty_set ),
inference(rewrite,[status(thm)],[1258,1709]) ).
thf(16881,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ ( D @ powerset @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( D @ powerset @ singleton @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7112]) ).
thf(16882,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ powerset @ singleton @ ( B @ powerset @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[16881:[bind(A,$thf( E @ powerset )),bind(B,$thf( empty_set )),bind(C,$thf( C )),bind(D,$thf( E ))]]) ).
thf(17120,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ powerset @ singleton @ ( B @ powerset @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[16882]) ).
thf(32740,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ powerset @ singleton @ ( C @ powerset @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,17120]) ).
thf(32741,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ powerset @ singleton @ ( C @ powerset @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32740]) ).
thf(32801,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( C @ powerset @ singleton @ ( C @ powerset @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32741]) ).
thf(32846,plain,
! [B: $i,A: $i] :
( ( B @ powerset @ singleton @ ( B @ powerset @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32801]) ).
thf(41365,plain,
( ( sk1 != sk1 )
| ( empty_set != empty_set )
| ( sk2 @ empty )
| sk3
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ element ) )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[39910,25127]) ).
thf(41366,plain,
( ( sk1 != sk1 )
| ( sk2 @ empty )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ element ) )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(simp,[status(thm)],[41365]) ).
thf(41367,plain,
( ( sk2 @ empty )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ element ) )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[41366:[]]) ).
thf(35314,plain,
( ( ( sk2 @ relation_rng @ empty )
!= ( sk12 @ empty ) )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[22703,155]) ).
thf(35315,plain,
( ( ( sk2 @ relation_rng @ empty )
!= ( sk12 @ empty ) )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[35314]) ).
thf(35450,plain,
( ( ( sk2 @ relation_rng )
!= sk12 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[35315]) ).
thf(38709,plain,
! [A: $i] :
( ( ( A @ identity_relation @ relation_dom )
!= ( sk2 @ relation_dom ) )
| ( A != sk12 )
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[204,33567]) ).
thf(38757,plain,
( ( ( sk12 @ identity_relation )
!= sk2 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[38709]) ).
thf(32660,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ ( C @ powerset @ unordered_pair ) @ ( C @ powerset @ singleton @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,17118]) ).
thf(32661,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ ( C @ powerset @ unordered_pair ) @ ( C @ powerset @ singleton @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32660]) ).
thf(32783,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( empty_set @ ( C @ powerset @ unordered_pair ) @ ( C @ powerset @ singleton @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32661]) ).
thf(32826,plain,
! [B: $i,A: $i] :
( ( empty_set @ ( B @ powerset @ unordered_pair ) @ ( B @ powerset @ singleton @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32783]) ).
thf(165,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( C @ in ) )
| ~ ( B @ ( D @ ( C @ ordered_pair ) @ in ) )
| ( B
!= ( A @ identity_relation ) )
| ~ ( B @ relation ) ),
inference(cnfConj,[status(thm)],[161]) ).
thf(171,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( C @ in ) )
| ~ ( B @ ( D @ ( C @ ordered_pair ) @ in ) )
| ~ ( B @ relation )
| ( B
!= ( A @ identity_relation ) ) ),
inference(lifteq,[status(thm)],[165]) ).
thf(172,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ in ) )
| ~ ( A @ identity_relation @ ( C @ ( B @ ordered_pair ) @ in ) )
| ~ ( A @ identity_relation @ relation ) ),
inference(simp,[status(thm)],[171]) ).
thf(5445,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ in ) )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) )
| ~ $true ),
inference(rewrite,[status(thm)],[172,192,89]) ).
thf(5446,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ in ) )
| ~ ( A @ identity_relation @ ( B @ singleton @ ( C @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[5445]) ).
thf(8841,plain,
( ( ( sk4 @ empty )
!= ( empty_set @ empty ) )
| ~ sk3
| ~ ( empty_set @ ( sk2 @ apply ) @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,4445]) ).
thf(8842,plain,
( ( ( sk4 @ empty )
!= ( empty_set @ empty ) )
| ~ sk3
| ~ ( empty_set @ ( sk2 @ apply ) @ empty ) ),
inference(simp,[status(thm)],[8841]) ).
thf(8905,plain,
( ( sk4 != empty_set )
| ~ sk3
| ~ ( empty_set @ ( sk2 @ apply ) @ empty ) ),
inference(simp,[status(thm)],[8842]) ).
thf(22780,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation @ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) )
!= ( B @ ( B @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22553,13102]) ).
thf(22781,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ identity_relation @ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) )
!= ( B @ ( B @ in ) ) ),
inference(simp,[status(thm)],[22780]) ).
thf(23063,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation )
!= B )
| ( ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) )
!= B ) ),
inference(simp,[status(thm)],[22781]) ).
thf(23106,plain,
! [A: $i] :
( ( A @ powerset @ identity_relation )
!= ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) ),
inference(simp,[status(thm)],[23063]) ).
thf(39980,plain,
( ( sk10 != sk10 )
| ( sk1 = empty_set )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( empty_set @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[5981,39017]) ).
thf(39981,plain,
( ( sk10 != sk10 )
| ( sk1 = empty_set )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( empty_set @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(simp,[status(thm)],[39980]) ).
thf(39982,plain,
( ( sk1 = empty_set )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( empty_set @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[39981:[]]) ).
thf(139,plain,
! [A: $i] :
( ( ( A @ function )
& ( A @ relation ) )
=> ( ! [B: $i] :
( ~ ( A @ relation_dom @ ( B @ in ) )
=> ( ! [C: $i] :
( ( C = empty_set )
=> ( C
= ( B @ ( A @ apply ) ) ) )
& ! [C: $i] :
( ( C
= ( B @ ( A @ apply ) ) )
=> ( C = empty_set ) ) ) )
& ! [B: $i] :
( ( A @ relation_dom @ ( B @ in ) )
=> ( ! [C: $i] :
( ( A @ ( C @ ( B @ ordered_pair ) @ in ) )
=> ( C
= ( B @ ( A @ apply ) ) ) )
& ! [C: $i] :
( ( C
= ( B @ ( A @ apply ) ) )
=> ( A @ ( C @ ( B @ ordered_pair ) @ in ) ) ) ) ) ) ),
inference(miniscope,[status(thm)],[138]) ).
thf(140,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( G
= ( E @ ( A @ apply ) ) )
| ( G != empty_set )
| ( A @ relation_dom @ ( E @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( F = empty_set )
| ( F
!= ( E @ ( A @ apply ) ) )
| ( A @ relation_dom @ ( E @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( D
= ( B @ ( A @ apply ) ) )
| ~ ( A @ ( D @ ( B @ ordered_pair ) @ in ) )
| ~ ( A @ relation_dom @ ( B @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) )
& ( ( A @ ( C @ ( B @ ordered_pair ) @ in ) )
| ( C
!= ( B @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( B @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ) ),
inference(cnf,[status(esa)],[139]) ).
thf(143,plain,
! [C: $i,B: $i,A: $i] :
( ( C = empty_set )
| ( C
!= ( B @ ( A @ apply ) ) )
| ( A @ relation_dom @ ( B @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[140]) ).
thf(149,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ relation_dom @ ( B @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( C = empty_set )
| ( C
!= ( B @ ( A @ apply ) ) ) ),
inference(lifteq,[status(thm)],[143]) ).
thf(150,plain,
! [B: $i,A: $i] :
( ( A @ relation_dom @ ( B @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( ( B @ ( A @ apply ) )
= empty_set ) ),
inference(simp,[status(thm)],[149]) ).
thf(776,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk8 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[101,80]) ).
thf(777,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ sk8 @ element ) )
!= ( C @ powerset @ ( B @ element ) ) )
| ( C @ ( B @ subset ) ) ),
inference(simp,[status(thm)],[776]) ).
thf(778,plain,
! [A: $i] : ( A @ ( A @ sk8 @ subset ) ),
inference(pattern_uni,[status(thm)],[777:[bind(A,$thf( D )),bind(B,$thf( D @ sk8 )),bind(C,$thf( D ))]]) ).
thf(784,plain,
! [A: $i] : ( A @ ( A @ sk8 @ subset ) ),
inference(simp,[status(thm)],[778]) ).
thf(2060,plain,
! [A: $i] : ( A @ ( empty_set @ subset ) ),
inference(rewrite,[status(thm)],[784,2009]) ).
thf(167,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ identity_relation ) )
| ( ( A @ ( B @ sk16 ) )
= ( A @ ( B @ sk17 ) ) )
| ( B @ ( A @ sk13 ) )
| ~ ( B @ relation ) ),
inference(cnfConj,[status(thm)],[161]) ).
thf(177,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ sk13 ) )
| ~ ( B @ relation )
| ( B
= ( A @ identity_relation ) )
| ( ( A @ ( B @ sk17 ) )
= ( A @ ( B @ sk16 ) ) ) ),
inference(lifteq,[status(thm)],[167]) ).
thf(32744,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ singleton @ ( sk12 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,7099]) ).
thf(32745,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ singleton @ ( sk12 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32744]) ).
thf(32790,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( empty_set @ singleton @ ( sk12 @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32745]) ).
thf(32833,plain,
! [A: $i] :
( ( empty_set @ singleton @ ( sk12 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32790]) ).
thf(17265,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ singleton @ ( E @ ( D @ unordered_pair ) @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7223]) ).
thf(17266,plain,
! [C: $i,B: $i,A: $i] :
~ ( A @ identity_relation @ ( C @ ( B @ unordered_pair ) @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[17265:[bind(A,$thf( I @ ( H @ unordered_pair ) @ ( empty_set @ unordered_pair ) )),bind(B,$thf( empty_set @ singleton )),bind(C,$thf( C )),bind(D,$thf( H )),bind(E,$thf( I ))]]) ).
thf(17500,plain,
! [C: $i,B: $i,A: $i] :
~ ( A @ identity_relation @ ( C @ ( B @ unordered_pair ) @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[17266]) ).
thf(27039,plain,
! [A: $i] :
( ( A
!= ( sk2 @ relation_dom ) )
| ( sk6 != sk2 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,26200]) ).
thf(27040,plain,
! [A: $i] :
( ( A
!= ( sk2 @ relation_dom ) )
| ( sk6 != sk2 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[27039]) ).
thf(27041,plain,
( ( sk6 != sk2 )
| ~ ( sk2 @ relation_dom @ empty ) ),
inference(pattern_uni,[status(thm)],[27040:[bind(A,$thf( sk2 @ relation_dom ))]]) ).
thf(10911,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( empty_set @ empty ) )
| ~ sk3
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,10808]) ).
thf(10912,plain,
( ( ( sk2 @ relation_dom @ empty )
!= ( empty_set @ empty ) )
| ~ sk3 ),
inference(simp,[status(thm)],[10911]) ).
thf(10941,plain,
( ( ( sk2 @ relation_dom )
!= empty_set )
| ~ sk3 ),
inference(simp,[status(thm)],[10912]) ).
thf(12316,plain,
! [A: $i] :
( ( ( A @ identity_relation @ relation_dom )
!= ( sk2 @ relation_dom ) )
| ( A != empty_set )
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[204,10941]) ).
thf(12345,plain,
( ( ( empty_set @ identity_relation )
!= sk2 )
| ~ sk3 ),
inference(simp,[status(thm)],[12316]) ).
thf(26175,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk2 @ relation_empty_yielding )
| ~ $true
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[20707,25733]) ).
thf(26176,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk2 @ relation_empty_yielding )
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(simp,[status(thm)],[26175]) ).
thf(26177,plain,
( ( sk2 @ relation_empty_yielding )
| ( ( sk2 @ relation_dom )
!= empty_set ) ),
inference(pattern_uni,[status(thm)],[26176:[]]) ).
thf(133,plain,
! [C: $i,B: $i,A: $i] :
( ( B
= ( A @ ( C @ apply ) ) )
| ~ ( C @ ( B @ ( A @ ordered_pair ) @ in ) )
| ~ ( C @ function )
| ~ ( C @ relation ) ),
inference(cnfConj,[status(thm)],[131]) ).
thf(135,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ ordered_pair ) @ in ) )
| ~ ( C @ function )
| ~ ( C @ relation )
| ( B
= ( A @ ( C @ apply ) ) ) ),
inference(lifteq,[status(thm)],[133]) ).
thf(3334,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) @ in ) )
| ~ ( C @ function )
| ~ ( C @ relation )
| ( B
= ( A @ ( C @ apply ) ) ) ),
inference(rewrite,[status(thm)],[135,89]) ).
thf(32644,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ singleton @ singleton @ ( C @ singleton @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,17773]) ).
thf(32645,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( C @ singleton @ singleton @ ( C @ singleton @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32644]) ).
thf(32795,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( C @ singleton @ singleton @ ( C @ singleton @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32645]) ).
thf(32838,plain,
! [B: $i,A: $i] :
( ( B @ singleton @ singleton @ ( B @ singleton @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32795]) ).
thf(38804,plain,
! [A: $i] :
( ( ( A @ identity_relation @ relation_dom )
!= ( sk2 @ relation_dom ) )
| ( A != sk6 )
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[204,33579]) ).
thf(38852,plain,
( ( ( sk6 @ identity_relation )
!= sk2 )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[38804]) ).
thf(40198,plain,
! [A: $i] :
( ( A != sk2 )
| ( ( sk2 @ relation_rng )
!= sk12 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,35450]) ).
thf(40199,plain,
! [A: $i] :
( ( A != sk2 )
| ( ( sk2 @ relation_rng )
!= sk12 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[40198]) ).
thf(40200,plain,
( ( ( sk2 @ relation_rng )
!= sk12 )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[40199:[bind(A,$thf( sk2 ))]]) ).
thf(22581,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ~ $true
| ( sk2 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[21792,115]) ).
thf(22582,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_rng @ relation )
| ( sk2 != empty_set ) ),
inference(simp,[status(thm)],[22581]) ).
thf(22583,plain,
( ( sk2 @ relation_rng @ relation )
| ( sk2 != empty_set ) ),
inference(pattern_uni,[status(thm)],[22582:[bind(A,$thf( sk2 ))]]) ).
thf(32674,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ singleton @ ( sk6 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,7444]) ).
thf(32675,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ singleton @ ( sk6 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32674]) ).
thf(32775,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( empty_set @ singleton @ ( sk6 @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32675]) ).
thf(32816,plain,
! [A: $i] :
( ( empty_set @ singleton @ ( sk6 @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32775]) ).
thf(14194,plain,
( ( ( sk2 @ relation_dom )
!= ( empty_set @ relation_dom ) )
| ( sk1 @ relation )
| sk3 ),
inference(paramod_ordered,[status(thm)],[56,14193]) ).
thf(14269,plain,
( ( sk2 != empty_set )
| ( sk1 @ relation )
| sk3 ),
inference(simp,[status(thm)],[14194]) ).
thf(20319,plain,
! [A: $i] :
( ( A != sk2 )
| ( empty_set != empty_set )
| ( sk1 @ relation )
| sk3
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,14269]) ).
thf(20320,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk1 @ relation )
| sk3
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[20319]) ).
thf(20321,plain,
( ( sk1 @ relation )
| sk3
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[20320:[bind(A,$thf( sk2 ))]]) ).
thf(32623,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( B @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,13102]) ).
thf(32624,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ ( B @ in ) ) ),
inference(simp,[status(thm)],[32623]) ).
thf(32807,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= B )
| ( A != B ) ),
inference(simp,[status(thm)],[32624]) ).
thf(32853,plain,
! [A: $i] :
( ( A @ powerset )
!= A ),
inference(simp,[status(thm)],[32807]) ).
thf(42679,plain,
( ( sk1 != sk1 )
| ( empty_set != empty_set )
| ( sk2 @ empty )
| sk3
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( empty_set @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[39982,25127]) ).
thf(42680,plain,
( ( sk1 != sk1 )
| ( sk2 @ empty )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( empty_set @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(simp,[status(thm)],[42679]) ).
thf(42681,plain,
( ( sk2 @ empty )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( empty_set @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[42680:[]]) ).
thf(32742,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ singleton @ ( C @ singleton @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,7363]) ).
thf(32743,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ singleton @ ( C @ singleton @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32742]) ).
thf(32777,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( empty_set @ singleton @ ( C @ singleton @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32743]) ).
thf(32818,plain,
! [B: $i,A: $i] :
( ( empty_set @ singleton @ ( B @ singleton @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32777]) ).
thf(158,plain,
! [A: $i] :
( ( A @ relation )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[157]) ).
thf(17529,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( D @ singleton @ singleton @ ( empty_set @ ( D @ singleton @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7362]) ).
thf(17530,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( empty_set @ ( B @ singleton @ unordered_pair ) @ ( B @ singleton @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[17529:[bind(A,$thf( empty_set @ ( I @ singleton @ unordered_pair ) )),bind(B,$thf( I @ singleton @ singleton )),bind(C,$thf( C )),bind(D,$thf( I ))]]) ).
thf(17775,plain,
! [B: $i,A: $i] :
~ ( A @ identity_relation @ ( empty_set @ ( B @ singleton @ unordered_pair ) @ ( B @ singleton @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[17530]) ).
thf(955,plain,
( ( ( sk1 @ identity_relation @ empty )
!= ( sk11 @ empty ) )
| sk3
| ~ ( sk2 @ empty )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[126,596]) ).
thf(956,plain,
( ( ( sk1 @ identity_relation @ empty )
!= ( sk11 @ empty ) )
| sk3
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[955]) ).
thf(960,plain,
( ( ( sk1 @ identity_relation )
!= sk11 )
| ~ ( sk2 @ empty )
| sk3 ),
inference(simp,[status(thm)],[956]) ).
thf(1067,plain,
( ( ( sk11 @ empty )
!= ( sk2 @ empty ) )
| ( ( sk1 @ identity_relation )
!= sk11 )
| ~ $true
| sk3 ),
inference(paramod_ordered,[status(thm)],[126,960]) ).
thf(1068,plain,
( ( ( sk11 @ empty )
!= ( sk2 @ empty ) )
| ( ( sk1 @ identity_relation )
!= sk11 )
| sk3 ),
inference(simp,[status(thm)],[1067]) ).
thf(1069,plain,
( ( sk11 != sk2 )
| ( ( sk1 @ identity_relation )
!= sk11 )
| sk3 ),
inference(simp,[status(thm)],[1068]) ).
thf(4451,plain,
( ( sk2 != empty_set )
| ( ( sk1 @ identity_relation )
!= empty_set )
| sk3 ),
inference(rewrite,[status(thm)],[1069,1931]) ).
thf(20940,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk6 != sk1 )
| ( empty_set != empty_set )
| sk3
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,14606]) ).
thf(20941,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk6 != sk1 )
| sk3
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[20940]) ).
thf(20942,plain,
( ( sk6 != sk1 )
| sk3
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[20941:[bind(A,$thf( sk2 ))]]) ).
thf(141,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ ordered_pair ) @ in ) )
| ( C
!= ( B @ ( A @ apply ) ) )
| ~ ( A @ relation_dom @ ( B @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(cnfConj,[status(thm)],[140]) ).
thf(145,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ ordered_pair ) @ in ) )
| ~ ( A @ relation_dom @ ( B @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation )
| ( C
!= ( B @ ( A @ apply ) ) ) ),
inference(lifteq,[status(thm)],[141]) ).
thf(146,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ apply ) @ ( B @ ordered_pair ) @ in ) )
| ~ ( A @ relation_dom @ ( B @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(simp,[status(thm)],[145]) ).
thf(4121,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ singleton @ ( B @ ( A @ apply ) @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) )
| ~ ( A @ relation_dom @ ( B @ in ) )
| ~ ( A @ function )
| ~ ( A @ relation ) ),
inference(rewrite,[status(thm)],[146,89]) ).
thf(40269,plain,
( ( sk1 != sk1 )
| ( empty_set != empty_set )
| ( sk2 @ empty )
| sk3
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[39017,25127]) ).
thf(40270,plain,
( ( sk1 != sk1 )
| ( sk2 @ empty )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(simp,[status(thm)],[40269]) ).
thf(40271,plain,
( ( sk2 @ empty )
| ( sk1 @ ( sk1 @ ( empty_set @ sk16 ) @ ( sk2 @ apply ) @ in ) )
| sk3
| ( sk10 @ ( sk1 @ sk13 ) )
| ( empty_set @ ( empty_set @ sk13 ) )
| ( sk10 @ ( empty_set @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[40270:[]]) ).
thf(32736,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( D @ ( C @ unordered_pair ) @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,17500]) ).
thf(32737,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( D @ ( C @ unordered_pair ) @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32736]) ).
thf(32797,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( D @ ( C @ unordered_pair ) @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32737]) ).
thf(32841,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unordered_pair ) @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32797]) ).
thf(25161,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_empty_yielding )
| ~ $true
| ~ ( sk1 @ empty )
| sk3 ),
inference(paramod_ordered,[status(thm)],[20650,25142]) ).
thf(25162,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A @ relation_empty_yielding )
| ~ ( sk1 @ empty )
| sk3 ),
inference(simp,[status(thm)],[25161]) ).
thf(25163,plain,
( ( sk2 @ relation_empty_yielding )
| ~ ( sk1 @ empty )
| sk3 ),
inference(pattern_uni,[status(thm)],[25162:[bind(A,$thf( sk2 ))]]) ).
thf(20095,plain,
( ( ( sk4 @ empty )
!= ( empty_set @ empty ) )
| ( ( empty_set @ ( sk2 @ apply ) )
!= empty_set )
| ~ sk3
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,8314]) ).
thf(20096,plain,
( ( ( sk4 @ empty )
!= ( empty_set @ empty ) )
| ( ( empty_set @ ( sk2 @ apply ) )
!= empty_set )
| ~ sk3 ),
inference(simp,[status(thm)],[20095]) ).
thf(20163,plain,
( ( sk4 != empty_set )
| ( ( empty_set @ ( sk2 @ apply ) )
!= empty_set )
| ~ sk3 ),
inference(simp,[status(thm)],[20096]) ).
thf(13105,plain,
! [A: $i] :
( ( ( sk1 @ ( sk4 @ in ) )
!= ( A @ ( A @ in ) ) )
| ~ $true
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[746,13102]) ).
thf(13106,plain,
! [A: $i] :
( ( ( sk1 @ ( sk4 @ in ) )
!= ( A @ ( A @ in ) ) )
| ~ sk3 ),
inference(simp,[status(thm)],[13105]) ).
thf(13123,plain,
! [A: $i] :
( ( sk1 != A )
| ( sk4 != A )
| ~ sk3 ),
inference(simp,[status(thm)],[13106]) ).
thf(13133,plain,
( ( sk4 != sk1 )
| ~ sk3 ),
inference(simp,[status(thm)],[13123]) ).
thf(51,plain,
sk2 @ function,
inference(cnfConj,[status(thm)],[44]) ).
thf(22956,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation @ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) )
!= ( C @ ( B @ in ) ) )
| ( C @ ( B @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22553,123]) ).
thf(22957,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ identity_relation @ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) )
!= ( C @ ( B @ in ) ) )
| ( C @ ( B @ element ) ) ),
inference(simp,[status(thm)],[22956]) ).
thf(22958,plain,
! [A: $i] : ( A @ powerset @ identity_relation @ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ element ) ),
inference(pattern_uni,[status(thm)],[22957:[bind(A,$thf( J )),bind(B,$thf( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) )),bind(C,$thf( J @ powerset @ identity_relation ))]]) ).
thf(23152,plain,
! [A: $i] : ( A @ powerset @ identity_relation @ ( empty_set @ singleton @ ( empty_set @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ element ) ),
inference(simp,[status(thm)],[22958]) ).
thf(4842,plain,
( ( ( sk4 @ empty )
!= ( empty_set @ empty ) )
| ( ( empty_set @ ( sk2 @ apply ) )
!= sk4 )
| ~ sk3
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,1828]) ).
thf(4843,plain,
( ( ( sk4 @ empty )
!= ( empty_set @ empty ) )
| ( ( empty_set @ ( sk2 @ apply ) )
!= sk4 )
| ~ sk3 ),
inference(simp,[status(thm)],[4842]) ).
thf(4885,plain,
( ( sk4 != empty_set )
| ( ( empty_set @ ( sk2 @ apply ) )
!= sk4 )
| ~ sk3 ),
inference(simp,[status(thm)],[4843]) ).
thf(304,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk2 @ relation_dom ) )
| sk3
| ( A = sk1 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[67,56]) ).
thf(305,plain,
! [A: $i] :
( sk3
| ( A = sk1 )
| ~ ( sk2 @ relation_dom @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[304:[bind(A,$thf( A )),bind(B,$thf( sk2 @ relation_dom ))]]) ).
thf(24985,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk6 != sk2 )
| ~ $true
| ~ ( sk1 @ empty )
| sk3 ),
inference(paramod_ordered,[status(thm)],[20650,23271]) ).
thf(24986,plain,
( ( ( sk2 @ empty )
!= ( sk2 @ empty ) )
| ( sk6 != sk2 )
| ~ ( sk1 @ empty )
| sk3 ),
inference(simp,[status(thm)],[24985]) ).
thf(24987,plain,
( ( sk6 != sk2 )
| ~ ( sk1 @ empty )
| sk3 ),
inference(pattern_uni,[status(thm)],[24986:[]]) ).
thf(32662,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk12 @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,7821]) ).
thf(32663,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk12 @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32662]) ).
thf(32764,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( sk12 @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32663]) ).
thf(32873,plain,
! [A: $i] :
( ( sk12 @ ( empty_set @ unordered_pair ) @ ( empty_set @ singleton @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32764]) ).
thf(340,plain,
! [B: $i,A: $i] :
( ( B != sk4 )
| ~ sk3
| ( ( A @ ( sk2 @ apply ) )
!= sk4 )
| ( ( sk2 @ relation_dom )
!= sk1 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[67,54]) ).
thf(341,plain,
! [A: $i] :
( ~ sk3
| ( ( A @ ( sk2 @ apply ) )
!= sk4 )
| ( ( sk2 @ relation_dom )
!= sk1 )
| ~ ( sk4 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[340:[bind(A,$thf( A )),bind(B,$thf( sk4 ))]]) ).
thf(32669,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ ( sk12 @ unordered_pair ) @ ( sk12 @ singleton @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,7661]) ).
thf(32670,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( empty_set @ ( sk12 @ unordered_pair ) @ ( sk12 @ singleton @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32669]) ).
thf(32791,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( empty_set @ ( sk12 @ unordered_pair ) @ ( sk12 @ singleton @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32670]) ).
thf(32834,plain,
! [A: $i] :
( ( empty_set @ ( sk12 @ unordered_pair ) @ ( sk12 @ singleton @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32791]) ).
thf(33016,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ in ) )
!= ( B @ ( B @ powerset @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22362,32821]) ).
thf(33017,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( empty_set @ in ) )
!= ( B @ ( B @ powerset @ in ) ) ),
inference(simp,[status(thm)],[33016]) ).
thf(33029,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= B )
| ( ( B @ powerset )
!= empty_set ) ),
inference(simp,[status(thm)],[33017]) ).
thf(33037,plain,
! [A: $i] :
( ( A @ powerset @ powerset )
!= empty_set ),
inference(simp,[status(thm)],[33029]) ).
thf(21291,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ ( C @ ( D @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( E @ identity_relation @ ( D @ ( C @ unordered_pair ) @ singleton @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,20998]) ).
thf(21292,plain,
! [C: $i,B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ ( C @ unordered_pair ) @ singleton @ ( C @ ( B @ unordered_pair ) @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[21291:[bind(A,$thf( G @ ( F @ unordered_pair ) )),bind(B,$thf( empty_set )),bind(C,$thf( G )),bind(D,$thf( F ))]]) ).
thf(21500,plain,
! [C: $i,B: $i,A: $i] :
~ ( A @ identity_relation @ ( B @ ( C @ unordered_pair ) @ singleton @ ( C @ ( B @ unordered_pair ) @ ( empty_set @ unordered_pair ) @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[21292]) ).
thf(32734,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk6 @ singleton @ ( empty_set @ ( sk6 @ unordered_pair ) @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,7443]) ).
thf(32735,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk6 @ singleton @ ( empty_set @ ( sk6 @ unordered_pair ) @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32734]) ).
thf(32771,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( sk6 @ singleton @ ( empty_set @ ( sk6 @ unordered_pair ) @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32735]) ).
thf(32812,plain,
! [A: $i] :
( ( sk6 @ singleton @ ( empty_set @ ( sk6 @ unordered_pair ) @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32771]) ).
thf(368,plain,
! [B: $i,A: $i] :
( ( B != sk4 )
| ~ sk3
| ( sk1 @ ( A @ in ) )
| ( ( sk2 @ relation_dom )
!= sk1 )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[67,55]) ).
thf(369,plain,
! [A: $i] :
( ~ sk3
| ( sk1 @ ( A @ in ) )
| ( ( sk2 @ relation_dom )
!= sk1 )
| ~ ( sk4 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[368:[bind(A,$thf( A )),bind(B,$thf( sk4 ))]]) ).
thf(25006,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set )
| ~ ( sk1 @ empty )
| sk3 ),
inference(paramod_ordered,[status(thm)],[20650,98]) ).
thf(25007,plain,
! [A: $i] :
( ( ( sk2 @ empty )
!= ( A @ empty ) )
| ( A = empty_set )
| ~ ( sk1 @ empty )
| sk3 ),
inference(simp,[status(thm)],[25006]) ).
thf(25008,plain,
( ( sk2 = empty_set )
| ~ ( sk1 @ empty )
| sk3 ),
inference(pattern_uni,[status(thm)],[25007:[bind(A,$thf( sk2 ))]]) ).
thf(27118,plain,
! [A: $i] :
( ( A
!= ( sk2 @ relation_dom ) )
| ( sk12 != sk2 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[98,26295]) ).
thf(27119,plain,
! [A: $i] :
( ( A
!= ( sk2 @ relation_dom ) )
| ( sk12 != sk2 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[27118]) ).
thf(27120,plain,
( ( sk12 != sk2 )
| ~ ( sk2 @ relation_dom @ empty ) ),
inference(pattern_uni,[status(thm)],[27119:[bind(A,$thf( sk2 @ relation_dom ))]]) ).
thf(8461,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( sk12 @ singleton @ ( sk12 @ ( empty_set @ unordered_pair ) @ unordered_pair ) ) )
| ~ ( C @ identity_relation @ ( A @ ( B @ unordered_pair ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[61,7658]) ).
thf(8462,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( sk12 @ ( empty_set @ unordered_pair ) @ ( sk12 @ singleton @ unordered_pair ) @ in ) ),
inference(pattern_uni,[status(thm)],[8461:[bind(A,$thf( sk12 @ ( empty_set @ unordered_pair ) )),bind(B,$thf( sk12 @ singleton )),bind(C,$thf( C ))]]) ).
thf(8596,plain,
! [A: $i] :
~ ( A @ identity_relation @ ( sk12 @ ( empty_set @ unordered_pair ) @ ( sk12 @ singleton @ unordered_pair ) @ in ) ),
inference(simp,[status(thm)],[8462]) ).
thf(111,plain,
sk10 @ relation_empty_yielding,
inference(cnfConj,[status(thm)],[109]) ).
thf(32756,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk12 @ ( empty_set @ unordered_pair ) @ ( sk12 @ singleton @ unordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[32608,8596]) ).
thf(32757,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( A @ in ) )
!= ( B @ identity_relation @ ( sk12 @ ( empty_set @ unordered_pair ) @ ( sk12 @ singleton @ unordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[32756]) ).
thf(32789,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset )
!= ( B @ identity_relation ) )
| ( A
!= ( sk12 @ ( empty_set @ unordered_pair ) @ ( sk12 @ singleton @ unordered_pair ) ) ) ),
inference(simp,[status(thm)],[32757]) ).
thf(32832,plain,
! [A: $i] :
( ( sk12 @ ( empty_set @ unordered_pair ) @ ( sk12 @ singleton @ unordered_pair ) @ powerset )
!= ( A @ identity_relation ) ),
inference(simp,[status(thm)],[32789]) ).
thf(14031,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ function )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[76,208]) ).
thf(14032,plain,
! [A: $i] :
( ( ( empty_set @ empty )
!= ( A @ empty ) )
| ( A @ function ) ),
inference(simp,[status(thm)],[14031]) ).
thf(14033,plain,
empty_set @ function,
inference(pattern_uni,[status(thm)],[14032:[bind(A,$thf( empty_set ))]]) ).
thf(222,plain,
sk18 @ relation,
inference(cnfConj,[status(thm)],[221]) ).
thf(66377,plain,
$false,
inference(e,[status(thm)],[14606,32819,234,4992,138,2889,8030,962,170,22614,115,23095,276,23704,21697,39510,23745,56,16336,32823,23251,153,27355,185,13751,27885,39017,20707,4439,1709,110,35424,17972,14391,157,21188,184,189,32848,1931,19736,46,969,93,13102,57,22703,21791,7112,5957,10950,4329,23115,2451,211,39910,1828,121,32831,38712,61,692,22663,12554,89,988,116,8033,206,2884,307,20998,85,220,2232,25151,32872,529,746,17773,70,2969,192,1824,26182,9105,32840,92,197,10808,27082,41580,1787,22754,2769,32820,8314,27886,17232,156,21498,25127,188,53,13676,13458,3001,27161,25733,783,7222,5941,1361,124,32827,77,21792,17118,7821,212,96,33567,32824,2304,654,27213,25070,5603,10401,129,7661,73,128,105,3225,3173,32875,2662,1732,7444,23099,2729,14534,23271,64,5928,180,4599,20899,21695,3158,2791,743,33032,13847,204,1226,7223,1752,59,118,28219,25145,21186,2738,32837,5703,7658,181,5580,86,159,32830,32868,419,14193,20833,2955,76,880,33579,98,32842,187,26220,219,7362,208,32851,35192,32836,3747,4445,7113,103,213,19103,7098,38807,155,198,108,32813,14122,130,26200,223,6100,267,80,3110,32846,25142,41367,2054,35450,38757,20650,112,123,23709,32826,8194,194,209,23253,5446,8905,712,63,23106,95,39982,150,2060,67,177,32608,13032,32821,7443,32833,17500,27041,199,12345,26177,3334,32838,23101,38852,40200,22583,72,859,43,32816,5981,20321,99,26616,87,23313,32853,7363,7099,17120,42681,32818,104,158,186,17775,114,2764,4451,20942,4121,75,40271,207,32841,82,2009,25163,119,58,235,20163,22553,13133,51,23152,4885,305,210,36609,24987,195,32873,10941,341,16078,26295,32834,596,33037,21500,14269,32812,14603,68,62,871,369,1357,17177,25008,83,22362,27120,8596,90,111,32832,122,14033,215,222,22748]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU216+3 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.07 % 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.15/0.40 % Computer : n008.cluster.edu
% 0.15/0.40 % Model : x86_64 x86_64
% 0.15/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.40 % Memory : 8046.5625MB
% 0.15/0.40 % OS : Linux 6.8.0-71-generic
% 0.15/0.40 % CPULimit : 300
% 0.15/0.40 % WCLimit : 300
% 0.15/0.40 % DateTime : Sat Sep 26 08:52:45 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.15/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.84/1.00 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.33/1.22 % [INFO] Parsing done (213ms).
% 1.33/1.23 % [INFO] Running in sequential loop mode.
% 2.01/1.63 % [INFO] eprover registered as external prover.
% 2.01/1.64 % [INFO] Scanning for conjecture ...
% 2.19/1.75 % [INFO] Found a conjecture (or negated_conjecture) and 40 axioms. Running axiom selection ...
% 2.34/1.83 % [INFO] Axiom selection finished. Selected 40 axioms (removed 0 axioms).
% 2.34/1.88 % [INFO] Problem is first-order (TPTP FOF).
% 2.34/1.89 % [INFO] Type checking passed.
% 2.34/1.89 % [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 ...
% 158.06/43.73 % External prover 'e' found a proof!
% 158.06/43.73 % [INFO] Killing All external provers ...
% 158.06/43.73 % Time passed: 43177ms (effective reasoning time: 42497ms)
% 158.06/43.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)>
% 158.06/43.74 % Axioms used in derivation (40): cc1_relat_1, rc1_funct_1, fc2_subset_1, t4_subset, rc1_subset_1, fc5_relat_1, rc2_relat_1, rc2_xboole_0, fc1_zfmisc_1, d4_funct_1, fc1_xboole_0, d5_tarski, fc4_relat_1, t1_subset, rc3_relat_1, t6_boole, rc2_subset_1, fc3_subset_1, t5_subset, fc2_funct_1, t8_funct_1, t7_boole, cc1_funct_1, d10_relat_1, fc1_subset_1, t3_subset, existence_m1_subset_1, commutativity_k2_tarski, rc1_relat_1, reflexivity_r1_tarski, dt_k6_relat_1, fc6_relat_1, t8_boole, rc1_xboole_0, t2_subset, fc7_relat_1, fc12_relat_1, fc8_relat_1, t71_relat_1, antisymmetry_r2_hidden
% 158.06/43.74 % No. of inferences in proof: 963
% 158.06/43.74 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 43177 ms resp. 42497 ms w/o parsing
% 161.46/44.20 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 161.46/44.21 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------