%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEU162+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n004.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:37:50 AM UTC 2026
% Result : Theorem 99.74s 24.89s
% Output : Refutation 102.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 99
% Syntax : Number of formulae : 857 ( 251 unt; 0 typ; 17 def)
% Number of atoms : 2355 (1023 equ; 0 cnn)
% Maximal formula atoms : 26 ( 2 avg)
% Number of connectives : 6703 (1257 ~; 861 |; 182 &;4187 @)
% ( 33 <=>; 183 =>; 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; 9 con; 0-3 aty)
% Number of variables : 1451 ( 24 ^;1367 !; 43 ?;1451 :)
% ( 0 !>; 0 ?*; 0 @-; 17 @+)
% Comments :
%------------------------------------------------------------------------------
thf(set_difference_decl,type,
set_difference: $i > $i > $i ).
thf(singleton_decl,type,
singleton: $i > $i ).
thf(in_decl,type,
in: $i > $i > $o ).
thf(proper_subset_decl,type,
proper_subset: $i > $i > $o ).
thf(empty_decl,type,
empty: $i > $o ).
thf(subset_decl,type,
subset: $i > $i > $o ).
thf(set_union2_decl,type,
set_union2: $i > $i > $i ).
thf(empty_set_decl,type,
empty_set: $i ).
thf(set_intersection2_decl,type,
set_intersection2: $i > $i > $i ).
thf(disjoint_decl,type,
disjoint: $i > $i > $o ).
thf(unordered_pair_decl,type,
unordered_pair: $i > $i > $i ).
thf(ordered_pair_decl,type,
ordered_pair: $i > $i > $i ).
thf(union_decl,type,
union: $i > $i ).
thf(cartesian_product2_decl,type,
cartesian_product2: $i > $i > $i ).
thf(powerset_decl,type,
powerset: $i > $i ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk5_decl,type,
sk5: $i ).
thf(sk6_decl,type,
sk6: $i ).
thf(sk9_decl,type,
sk9: $i > $i > $i ).
thf(sk10_decl,type,
sk10: $i > $i > $i ).
thf(sk11_decl,type,
sk11: $i > $i > $i ).
thf(sk12_decl,type,
sk12: $i > $i > $i ).
thf(sk13_decl,type,
sk13: $i > $i > $i > $i ).
thf(sk14_decl,type,
sk14: $i > $i > $o ).
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 > $i > $i > $o ).
thf(sk19_decl,type,
sk19: $i > $i > $i > $i ).
thf(sk20_decl,type,
sk20: $i > $i > $i > $i ).
thf(sk21_decl,type,
sk21: $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i] :
( ( ( B @ singleton @ ( A @ set_difference ) )
= A )
=> ~ ( A @ ( B @ in ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ( ( ( A @ singleton @ ( sk1 @ set_difference ) )
= sk1 )
=> ~ ( sk1 @ ( A @ in ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ! [B: $i] :
( ~ ( A @ ( B @ in ) )
=> ( ( B @ singleton @ ( A @ set_difference ) )
= A ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
~ ( ~ ( sk3 @ ( A @ in ) )
=> ( ( A @ singleton @ ( sk3 @ set_difference ) )
= sk3 ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: $i] : ( A @ empty ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: $i] :
~ ( A @ empty ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( A @ ( C @ in ) )
=> ( C = B ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( C = B )
=> ( A @ ( C @ in ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( B @ ( C @ in ) )
=> ( A @ ( C @ in ) ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( A @ ( C @ in ) )
=> ( B @ ( C @ in ) ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
( ( C @ ( D @ in ) )
& ( D @ ( A @ in ) ) ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( A @ ( C @ in ) )
=> ? [D: $i] :
( ( B @ ( D @ in ) )
& ( D @ ( C @ in ) ) ) ) ) ) ).
thf(sk16_def,definition,
( sk16
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ? [D: $i] :
( ( B @ ( D @ in ) )
& ( D @ ( C @ in ) ) )
=> ( A @ ( C @ in ) ) ) ) ) ).
thf(sk17_def,definition,
( sk17
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( ( B @ ( C @ in ) )
& ( C @ ( B @ ( A @ sk16 ) @ in ) ) ) ) ) ).
thf(sk19_def,definition,
( sk19
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
~ ( ( A @ ( D @ in ) )
=> ( ( D = B )
| ( D = C ) ) ) ) ) ).
thf(sk20_def,definition,
( sk20
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
~ ( ( ( D = B )
| ( D = C ) )
=> ( A @ ( D @ in ) ) ) ) ) ).
thf(sk21_def,definition,
( sk21
= ( ^ [A: $i] :
@+[B: $i] : ( A @ ( B @ in ) ) ) ) ).
thf(39,axiom,
! [A: $i,B: $i] :
( ( B
= ( A @ singleton ) )
<=> ! [C: $i] :
( ( B @ ( C @ in ) )
<=> ( C = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_tarski) ).
thf(219,plain,
! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( ( C = A )
=> ( B @ ( C @ in ) ) )
& ( ( B @ ( C @ in ) )
=> ( C = A ) ) )
=> ( B
= ( A @ singleton ) ) )
& ( ( B
= ( A @ singleton ) )
=> ! [C: $i] :
( ( ( C = A )
=> ( B @ ( C @ in ) ) )
& ( ( B @ ( C @ in ) )
=> ( C = A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(220,plain,
( ! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( C = A )
=> ( B @ ( C @ in ) ) )
& ! [C: $i] :
( ( B @ ( C @ in ) )
=> ( C = A ) ) )
=> ( B
= ( A @ singleton ) ) )
& ! [A: $i,B: $i] :
( ( B
= ( A @ singleton ) )
=> ( ! [C: $i] :
( ( C = A )
=> ( B @ ( C @ in ) ) )
& ! [C: $i] :
( ( B @ ( C @ in ) )
=> ( C = A ) ) ) ) ),
inference(miniscope,[status(thm)],[219]) ).
thf(221,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F
= ( E @ singleton ) )
| ~ ( F @ ( E @ ( F @ sk10 ) @ in ) )
| ( ( E @ ( F @ sk9 ) )
!= E ) )
& ( ( F
= ( E @ singleton ) )
| ( ( E @ ( F @ sk10 ) )
= E )
| ( ( E @ ( F @ sk9 ) )
!= E ) )
& ( ( F
= ( E @ singleton ) )
| ~ ( F @ ( E @ ( F @ sk10 ) @ in ) )
| ( F @ ( E @ ( F @ sk9 ) @ in ) ) )
& ( ( F
= ( E @ singleton ) )
| ( ( E @ ( F @ sk10 ) )
= E )
| ( F @ ( E @ ( F @ sk9 ) @ in ) ) )
& ( ( B @ ( D @ in ) )
| ( D != A )
| ( B
!= ( A @ singleton ) ) )
& ( ( C = A )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ singleton ) ) ) ),
inference(cnf,[status(esa)],[220]) ).
thf(227,plain,
! [C: $i,B: $i,A: $i] :
( ( C = A )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ singleton ) ) ),
inference(cnfConj,[status(thm)],[221]) ).
thf(236,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ in ) )
| ( C = A )
| ( B
!= ( A @ singleton ) ) ),
inference(lifteq,[status(thm)],[227]) ).
thf(237,plain,
! [B: $i,A: $i] :
( ~ ( A @ singleton @ ( B @ in ) )
| ( B = A ) ),
inference(simp,[status(thm)],[236]) ).
thf(5,axiom,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( A != B )
& ( A @ empty ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_boole) ).
thf(99,plain,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( A != B )
& ( A @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(100,plain,
~ ? [A: $i] :
( ? [B: $i] :
( ( B @ empty )
& ( A != B ) )
& ( A @ empty ) ),
inference(miniscope,[status(thm)],[99]) ).
thf(101,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ( A = B )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[100]) ).
thf(102,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ~ ( A @ empty )
| ( A = B ) ),
inference(lifteq,[status(thm)],[101]) ).
thf(66,axiom,
! [A: $i] :
( ( A @ ( empty_set @ set_difference ) )
= empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_boole) ).
thf(483,plain,
! [A: $i] :
( ( A @ ( empty_set @ set_difference ) )
= empty_set ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(484,plain,
! [A: $i] :
( ( A @ ( empty_set @ set_difference ) )
= empty_set ),
inference(cnf,[status(esa)],[483]) ).
thf(485,plain,
! [A: $i] :
( ( A @ ( empty_set @ set_difference ) )
= empty_set ),
inference(lifteq,[status(thm)],[484]) ).
thf(1,conjecture,
! [A: $i,B: $i] :
( ( ( B @ singleton @ ( A @ set_difference ) )
= A )
<=> ~ ( A @ ( B @ in ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t65_zfmisc_1) ).
thf(2,negated_conjecture,
~ ! [A: $i,B: $i] :
( ( ( B @ singleton @ ( A @ set_difference ) )
= A )
<=> ~ ( A @ ( B @ in ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(84,plain,
~ ! [A: $i,B: $i] :
( ( ~ ( A @ ( B @ in ) )
=> ( ( B @ singleton @ ( A @ set_difference ) )
= A ) )
& ( ( ( B @ singleton @ ( A @ set_difference ) )
= A )
=> ~ ( A @ ( B @ in ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(85,plain,
~ ( ! [A: $i,B: $i] :
( ~ ( A @ ( B @ in ) )
=> ( ( B @ singleton @ ( A @ set_difference ) )
= A ) )
& ! [A: $i,B: $i] :
( ( ( B @ singleton @ ( A @ set_difference ) )
= A )
=> ~ ( A @ ( B @ in ) ) ) ),
inference(miniscope,[status(thm)],[84]) ).
thf(86,plain,
( ( ( ( sk4 @ singleton @ ( sk3 @ set_difference ) )
!= sk3 )
| ( sk1 @ ( sk2 @ in ) ) )
& ( ~ ( sk3 @ ( sk4 @ in ) )
| ( sk1 @ ( sk2 @ in ) ) )
& ( ( ( sk4 @ singleton @ ( sk3 @ set_difference ) )
!= sk3 )
| ( ( sk2 @ singleton @ ( sk1 @ set_difference ) )
= sk1 ) )
& ( ~ ( sk3 @ ( sk4 @ in ) )
| ( ( sk2 @ singleton @ ( sk1 @ set_difference ) )
= sk1 ) ) ),
inference(cnf,[status(esa)],[85]) ).
thf(90,plain,
( ( ( sk4 @ singleton @ ( sk3 @ set_difference ) )
!= sk3 )
| ( sk1 @ ( sk2 @ in ) ) ),
inference(cnfConj,[status(thm)],[86]) ).
thf(93,plain,
( ( sk1 @ ( sk2 @ in ) )
| ( ( sk4 @ singleton @ ( sk3 @ set_difference ) )
!= sk3 ) ),
inference(lifteq,[status(thm)],[90]) ).
thf(48,axiom,
! [A: $i] :
( ( A = empty_set )
<=> ! [B: $i] :
~ ( A @ ( B @ in ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_xboole_0) ).
thf(330,plain,
! [A: $i] :
( ( ! [B: $i] :
~ ( A @ ( B @ in ) )
=> ( A = empty_set ) )
& ( ( A = empty_set )
=> ! [B: $i] :
~ ( A @ ( B @ in ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(331,plain,
( ! [A: $i] :
( ~ ? [B: $i] : ( A @ ( B @ in ) )
=> ( A = empty_set ) )
& ! [A: $i] :
( ( A = empty_set )
=> ~ ? [B: $i] : ( A @ ( B @ in ) ) ) ),
inference(miniscope,[status(thm)],[330]) ).
thf(332,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C = empty_set )
| ( C @ ( C @ sk21 @ in ) ) )
& ( ~ ( A @ ( B @ in ) )
| ( A != empty_set ) ) ),
inference(cnf,[status(esa)],[331]) ).
thf(333,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ in ) )
| ( A != empty_set ) ),
inference(cnfConj,[status(thm)],[332]) ).
thf(335,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ in ) )
| ( A != empty_set ) ),
inference(lifteq,[status(thm)],[333]) ).
thf(336,plain,
! [A: $i] :
~ ( empty_set @ ( A @ in ) ),
inference(simp,[status(thm)],[335]) ).
thf(624,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ in ) )
!= ( empty_set @ ( A @ in ) ) )
| ~ $true
| ( ( sk4 @ singleton @ ( sk3 @ set_difference ) )
!= sk3 ) ),
inference(paramod_ordered,[status(thm)],[93,336]) ).
thf(625,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ in ) )
!= ( empty_set @ ( A @ in ) ) )
| ( ( sk4 @ singleton @ ( sk3 @ set_difference ) )
!= sk3 ) ),
inference(simp,[status(thm)],[624]) ).
thf(629,plain,
! [A: $i] :
( ( sk1 != empty_set )
| ( sk2 != A )
| ( ( sk4 @ singleton @ ( sk3 @ set_difference ) )
!= sk3 ) ),
inference(simp,[status(thm)],[625]) ).
thf(631,plain,
( ( sk1 != empty_set )
| ( ( sk4 @ singleton @ ( sk3 @ set_difference ) )
!= sk3 ) ),
inference(simp,[status(thm)],[629]) ).
thf(640,plain,
! [A: $i] :
( ( ( A @ ( empty_set @ set_difference ) )
!= ( sk4 @ singleton @ ( sk3 @ set_difference ) ) )
| ( sk1 != empty_set )
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[485,631]) ).
thf(646,plain,
! [A: $i] :
( ( A
!= ( sk4 @ singleton ) )
| ( sk3 != empty_set )
| ( sk1 != empty_set )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[640]) ).
thf(651,plain,
( ( sk1 != empty_set )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[646]) ).
thf(699,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( sk1 != empty_set )
| ( B != empty_set )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[102,651]) ).
thf(700,plain,
! [A: $i] :
( ( sk1 != empty_set )
| ( A != empty_set )
| ~ ( A @ empty )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[699:[bind(A,$thf( sk3 ))]]) ).
thf(987,plain,
( ( sk1 != empty_set )
| ~ ( empty_set @ empty )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[700]) ).
thf(14,axiom,
empty_set @ empty,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_xboole_0) ).
thf(134,plain,
empty_set @ empty,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(1103,plain,
( ( sk1 != empty_set )
| ~ $true
| ~ ( sk3 @ empty ) ),
inference(rewrite,[status(thm)],[987,134]) ).
thf(1104,plain,
( ( sk1 != empty_set )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[1103]) ).
thf(12342,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ( A != empty_set )
| ~ ( sk3 @ empty )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,1104]) ).
thf(12343,plain,
! [A: $i] :
( ( A != empty_set )
| ~ ( sk3 @ empty )
| ~ ( A @ singleton @ ( sk1 @ in ) ) ),
inference(pattern_uni,[status(thm)],[12342:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(13199,plain,
( ~ ( sk3 @ empty )
| ~ ( empty_set @ singleton @ ( sk1 @ in ) ) ),
inference(simp,[status(thm)],[12343]) ).
thf(21,axiom,
! [A: $i] :
( ( A @ empty )
=> ( A = empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
thf(152,plain,
! [A: $i] :
( ( A @ empty )
=> ( A = empty_set ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(153,plain,
! [A: $i] :
( ( A = empty_set )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[152]) ).
thf(154,plain,
! [A: $i] :
( ~ ( A @ empty )
| ( A = empty_set ) ),
inference(lifteq,[status(thm)],[153]) ).
thf(638,plain,
! [A: $i] :
( ( ( A @ ( empty_set @ set_difference ) )
!= ( sk4 @ singleton @ ( sk3 @ set_difference ) ) )
| ( sk1 @ ( sk2 @ in ) )
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[485,93]) ).
thf(643,plain,
! [A: $i] :
( ( A
!= ( sk4 @ singleton ) )
| ( sk3 != empty_set )
| ( sk3 != empty_set )
| ( sk1 @ ( sk2 @ in ) ) ),
inference(simp,[status(thm)],[638]) ).
thf(648,plain,
( ( sk3 != empty_set )
| ( sk1 @ ( sk2 @ in ) ) ),
inference(simp,[status(thm)],[643]) ).
thf(4274,plain,
! [A: $i] :
( ( A != sk3 )
| ( empty_set != empty_set )
| ( sk1 @ ( sk2 @ in ) )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[154,648]) ).
thf(4275,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk1 @ ( sk2 @ in ) )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[4274]) ).
thf(4276,plain,
( ( sk1 @ ( sk2 @ in ) )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[4275:[bind(A,$thf( sk3 ))]]) ).
thf(43,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ~ ( A @ ( B @ in ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
thf(281,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ~ ( A @ ( B @ in ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(282,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ in ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[281]) ).
thf(39609,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( A @ ( B @ in ) )
| ~ $true
| ~ ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[4276,282]) ).
thf(39610,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( A @ ( B @ in ) )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[39609]) ).
thf(39611,plain,
( ~ ( sk2 @ ( sk1 @ in ) )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[39610:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 ))]]) ).
thf(46,axiom,
! [A: $i,B: $i,C: $i] :
( ( C
= ( B @ ( A @ unordered_pair ) ) )
<=> ! [D: $i] :
( ( C @ ( D @ in ) )
<=> ( ( D = B )
| ( D = A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_tarski) ).
thf(292,plain,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i] :
( ( ( ( D = B )
| ( D = A ) )
=> ( C @ ( D @ in ) ) )
& ( ( C @ ( D @ in ) )
=> ( ( D = B )
| ( D = A ) ) ) )
=> ( C
= ( B @ ( A @ unordered_pair ) ) ) )
& ( ( C
= ( B @ ( A @ unordered_pair ) ) )
=> ! [D: $i] :
( ( ( ( D = B )
| ( D = A ) )
=> ( C @ ( D @ in ) ) )
& ( ( C @ ( D @ in ) )
=> ( ( D = B )
| ( D = A ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(293,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ! [D: $i] :
( ( ( D = B )
| ( D = A ) )
=> ( C @ ( D @ in ) ) )
& ! [D: $i] :
( ( C @ ( D @ in ) )
=> ( ( D = B )
| ( D = A ) ) ) )
=> ( C
= ( B @ ( A @ unordered_pair ) ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( C
= ( B @ ( A @ unordered_pair ) ) )
=> ( ! [D: $i] :
( ( ( D = B )
| ( D = A ) )
=> ( C @ ( D @ in ) ) )
& ! [D: $i] :
( ( C @ ( D @ in ) )
=> ( ( D = B )
| ( D = A ) ) ) ) ) ),
inference(miniscope,[status(thm)],[292]) ).
thf(294,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( H
= ( G @ ( F @ unordered_pair ) ) )
| ~ ( H @ ( F @ ( G @ ( H @ sk20 ) ) @ in ) )
| ( H @ ( G @ ( F @ sk18 ) ) ) )
& ( ( H
= ( G @ ( F @ unordered_pair ) ) )
| ( ( F @ ( G @ ( H @ sk20 ) ) )
= G )
| ( ( F @ ( G @ ( H @ sk20 ) ) )
= F )
| ( H @ ( G @ ( F @ sk18 ) ) ) )
& ( ( H
= ( G @ ( F @ unordered_pair ) ) )
| ~ ( H @ ( G @ ( F @ sk18 ) ) )
| ( ( F @ ( G @ ( H @ sk19 ) ) )
!= G ) )
& ( ( H
= ( G @ ( F @ unordered_pair ) ) )
| ~ ( H @ ( G @ ( F @ sk18 ) ) )
| ( ( F @ ( G @ ( H @ sk19 ) ) )
!= F ) )
& ( ( H
= ( G @ ( F @ unordered_pair ) ) )
| ~ ( H @ ( G @ ( F @ sk18 ) ) )
| ( H @ ( F @ ( G @ ( H @ sk19 ) ) @ in ) ) )
& ( ( C @ ( E @ in ) )
| ( E != B )
| ( C
!= ( B @ ( A @ unordered_pair ) ) ) )
& ( ( C @ ( E @ in ) )
| ( E != A )
| ( C
!= ( B @ ( A @ unordered_pair ) ) ) )
& ( ( D = B )
| ( D = A )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ unordered_pair ) ) ) ) ),
inference(cnf,[status(esa)],[293]) ).
thf(298,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ in ) )
| ( D != B )
| ( C
!= ( B @ ( A @ unordered_pair ) ) ) ),
inference(cnfConj,[status(thm)],[294]) ).
thf(315,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ in ) )
| ( D != B )
| ( C
!= ( B @ ( A @ unordered_pair ) ) ) ),
inference(lifteq,[status(thm)],[298]) ).
thf(316,plain,
! [B: $i,A: $i] : ( B @ ( A @ unordered_pair ) @ ( B @ in ) ),
inference(simp,[status(thm)],[315]) ).
thf(2733,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) @ ( B @ in ) )
!= ( empty_set @ ( C @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[316,336]) ).
thf(2734,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( B @ in ) )
!= ( empty_set @ ( C @ in ) ) ),
inference(simp,[status(thm)],[2733]) ).
thf(2738,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= empty_set )
| ( B != C ) ),
inference(simp,[status(thm)],[2734]) ).
thf(2744,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) )
!= empty_set ),
inference(simp,[status(thm)],[2738]) ).
thf(16,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ disjoint ) )
=> ( A @ ( B @ disjoint ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_r1_xboole_0) ).
thf(138,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ disjoint ) )
=> ( A @ ( B @ disjoint ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(59,axiom,
! [A: $i] :
( ( A @ singleton )
!= empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l1_zfmisc_1) ).
thf(411,plain,
! [A: $i] :
( ( A @ singleton )
!= empty_set ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(412,plain,
~ ? [A: $i] :
( ( A @ singleton )
= empty_set ),
inference(miniscope,[status(thm)],[411]) ).
thf(413,plain,
! [A: $i] :
( ( A @ singleton )
!= empty_set ),
inference(cnf,[status(esa)],[412]) ).
thf(414,plain,
! [A: $i] :
( ( A @ singleton )
!= empty_set ),
inference(lifteq,[status(thm)],[413]) ).
thf(12883,plain,
! [C: $i,B: $i,A: $i] :
( ( B
!= ( C @ singleton ) )
| ( A != empty_set )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,414]) ).
thf(12884,plain,
! [B: $i,A: $i] :
( ( A != empty_set )
| ~ ( A @ singleton @ ( B @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[12883:[bind(A,$thf( A )),bind(B,$thf( D @ singleton )),bind(C,$thf( D ))]]) ).
thf(13410,plain,
! [A: $i] :
~ ( empty_set @ singleton @ ( A @ singleton @ in ) ),
inference(simp,[status(thm)],[12884]) ).
thf(70,axiom,
! [A: $i,B: $i] :
( ( ( B @ ( A @ set_difference ) )
= empty_set )
<=> ( B @ ( A @ subset ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t37_xboole_1) ).
thf(518,plain,
! [A: $i,B: $i] :
( ( ( B @ ( A @ subset ) )
=> ( ( B @ ( A @ set_difference ) )
= empty_set ) )
& ( ( ( B @ ( A @ set_difference ) )
= empty_set )
=> ( B @ ( A @ subset ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(27,axiom,
! [A: $i] : ( A @ ( empty_set @ subset ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_xboole_1) ).
thf(182,plain,
! [A: $i] : ( A @ ( empty_set @ subset ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(183,plain,
! [A: $i] : ( A @ ( empty_set @ subset ) ),
inference(cnf,[status(esa)],[182]) ).
thf(23,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ proper_subset ) )
<=> ( ( A != B )
& ( B @ ( A @ subset ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_xboole_0) ).
thf(158,plain,
! [A: $i,B: $i] :
( ( ( ( A != B )
& ( B @ ( A @ subset ) ) )
=> ( B @ ( A @ proper_subset ) ) )
& ( ( B @ ( A @ proper_subset ) )
=> ( ( A != B )
& ( B @ ( A @ subset ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(159,plain,
( ! [A: $i,B: $i] :
( ( ( A != B )
& ( B @ ( A @ subset ) ) )
=> ( B @ ( A @ proper_subset ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ proper_subset ) )
=> ( ( A != B )
& ( B @ ( A @ subset ) ) ) ) ),
inference(miniscope,[status(thm)],[158]) ).
thf(160,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ proper_subset ) )
| ( C = D )
| ~ ( D @ ( C @ subset ) ) )
& ( ( A != B )
| ~ ( B @ ( A @ proper_subset ) ) )
& ( ( B @ ( A @ subset ) )
| ~ ( B @ ( A @ proper_subset ) ) ) ),
inference(cnf,[status(esa)],[159]) ).
thf(163,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ proper_subset ) )
| ( A = B )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnfConj,[status(thm)],[160]) ).
thf(166,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ proper_subset ) )
| ~ ( B @ ( A @ subset ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[163]) ).
thf(167,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ proper_subset ) )
| ~ ( B @ ( A @ subset ) )
| ( A = B ) ),
inference(simp,[status(thm)],[166]) ).
thf(5818,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( empty_set @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( C @ ( B @ proper_subset ) )
| ~ $true
| ( B = C ) ),
inference(paramod_ordered,[status(thm)],[183,167]) ).
thf(5819,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( empty_set @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ( C @ ( B @ proper_subset ) )
| ( B = C ) ),
inference(simp,[status(thm)],[5818]) ).
thf(5820,plain,
! [A: $i] :
( ( A @ ( empty_set @ proper_subset ) )
| ( empty_set = A ) ),
inference(pattern_uni,[status(thm)],[5819:[bind(A,$thf( A )),bind(B,$thf( empty_set )),bind(C,$thf( A ))]]) ).
thf(42,axiom,
! [A: $i,B: $i] :
( ( B
= ( A @ union ) )
<=> ! [C: $i] :
( ( B @ ( C @ in ) )
<=> ? [D: $i] :
( ( A @ ( D @ in ) )
& ( D @ ( C @ in ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_tarski) ).
thf(254,plain,
! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( ? [D: $i] :
( ( A @ ( D @ in ) )
& ( D @ ( C @ in ) ) )
=> ( B @ ( C @ in ) ) )
& ( ( B @ ( C @ in ) )
=> ? [D: $i] :
( ( A @ ( D @ in ) )
& ( D @ ( C @ in ) ) ) ) )
=> ( B
= ( A @ union ) ) )
& ( ( B
= ( A @ union ) )
=> ! [C: $i] :
( ( ? [D: $i] :
( ( A @ ( D @ in ) )
& ( D @ ( C @ in ) ) )
=> ( B @ ( C @ in ) ) )
& ( ( B @ ( C @ in ) )
=> ? [D: $i] :
( ( A @ ( D @ in ) )
& ( D @ ( C @ in ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(255,plain,
( ! [A: $i,B: $i] :
( ( ! [C: $i] :
( ? [D: $i] :
( ( A @ ( D @ in ) )
& ( D @ ( C @ in ) ) )
=> ( B @ ( C @ in ) ) )
& ! [C: $i] :
( ( B @ ( C @ in ) )
=> ? [D: $i] :
( ( A @ ( D @ in ) )
& ( D @ ( C @ in ) ) ) ) )
=> ( B
= ( A @ union ) ) )
& ! [A: $i,B: $i] :
( ( B
= ( A @ union ) )
=> ( ! [C: $i] :
( ? [D: $i] :
( ( A @ ( D @ in ) )
& ( D @ ( C @ in ) ) )
=> ( B @ ( C @ in ) ) )
& ! [C: $i] :
( ( B @ ( C @ in ) )
=> ? [D: $i] :
( ( A @ ( D @ in ) )
& ( D @ ( C @ in ) ) ) ) ) ) ),
inference(miniscope,[status(thm)],[254]) ).
thf(256,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( G
= ( F @ union ) )
| ~ ( G @ ( F @ ( G @ sk16 ) @ in ) )
| ( G @ ( F @ sk14 ) ) )
& ( ( G
= ( F @ union ) )
| ( F @ ( F @ ( G @ sk17 ) @ in ) )
| ( G @ ( F @ sk14 ) ) )
& ( ( G
= ( F @ union ) )
| ( F @ ( G @ sk17 ) @ ( F @ ( G @ sk16 ) @ in ) )
| ( G @ ( F @ sk14 ) ) )
& ( ( G
= ( F @ union ) )
| ~ ( G @ ( F @ sk14 ) )
| ~ ( F @ ( H @ in ) )
| ~ ( H @ ( F @ ( G @ sk15 ) @ in ) ) )
& ( ( G
= ( F @ union ) )
| ~ ( G @ ( F @ sk14 ) )
| ( G @ ( F @ ( G @ sk15 ) @ in ) ) )
& ( ( B @ ( D @ in ) )
| ~ ( A @ ( E @ in ) )
| ~ ( E @ ( D @ in ) )
| ( B
!= ( A @ union ) ) )
& ( ( A @ ( A @ ( B @ ( C @ sk13 ) ) @ in ) )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ union ) ) )
& ( ( A @ ( B @ ( C @ sk13 ) ) @ ( C @ in ) )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ union ) ) ) ),
inference(cnf,[status(esa)],[255]) ).
thf(263,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ union ) )
| ~ ( B @ ( A @ sk14 ) )
| ( B @ ( A @ ( B @ sk15 ) @ in ) ) ),
inference(cnfConj,[status(thm)],[256]) ).
thf(275,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sk14 ) )
| ( B @ ( A @ ( B @ sk15 ) @ in ) )
| ( B
= ( A @ union ) ) ),
inference(lifteq,[status(thm)],[263]) ).
thf(276,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ sk14 ) )
| ( B @ ( A @ ( B @ sk15 ) @ in ) )
| ( B
= ( A @ union ) ) ),
inference(simp,[status(thm)],[275]) ).
thf(223,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ in ) )
| ( C != A )
| ( B
!= ( A @ singleton ) ) ),
inference(cnfConj,[status(thm)],[221]) ).
thf(232,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ in ) )
| ( C != A )
| ( B
!= ( A @ singleton ) ) ),
inference(lifteq,[status(thm)],[223]) ).
thf(233,plain,
! [A: $i] : ( A @ singleton @ ( A @ in ) ),
inference(simp,[status(thm)],[232]) ).
thf(41,axiom,
! [A: $i,B: $i] :
( ! [C: $i] :
( ( A @ ( C @ in ) )
<=> ( B @ ( C @ in ) ) )
=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tarski) ).
thf(243,plain,
! [A: $i,B: $i] :
( ! [C: $i] :
( ( ( B @ ( C @ in ) )
=> ( A @ ( C @ in ) ) )
& ( ( A @ ( C @ in ) )
=> ( B @ ( C @ in ) ) ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(244,plain,
! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( B @ ( C @ in ) )
=> ( A @ ( C @ in ) ) )
& ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( B @ ( C @ in ) ) ) )
=> ( A = B ) ),
inference(miniscope,[status(thm)],[243]) ).
thf(245,plain,
! [B: $i,A: $i] :
( ( ( A = B )
| ~ ( A @ ( A @ ( B @ sk12 ) @ in ) )
| ~ ( B @ ( A @ ( B @ sk11 ) @ in ) ) )
& ( ( A = B )
| ( B @ ( A @ ( B @ sk12 ) @ in ) )
| ~ ( B @ ( A @ ( B @ sk11 ) @ in ) ) )
& ( ( A = B )
| ~ ( A @ ( A @ ( B @ sk12 ) @ in ) )
| ( A @ ( A @ ( B @ sk11 ) @ in ) ) )
& ( ( A = B )
| ( B @ ( A @ ( B @ sk12 ) @ in ) )
| ( A @ ( A @ ( B @ sk11 ) @ in ) ) ) ),
inference(cnf,[status(esa)],[244]) ).
thf(246,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( B @ ( A @ ( B @ sk12 ) @ in ) )
| ( A @ ( A @ ( B @ sk11 ) @ in ) ) ),
inference(cnfConj,[status(thm)],[245]) ).
thf(250,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ sk12 ) @ in ) )
| ( A @ ( A @ ( B @ sk11 ) @ in ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[246]) ).
thf(12,axiom,
? [A: $i] :
~ ( A @ empty ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
thf(119,plain,
? [A: $i] :
~ ( A @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(120,plain,
~ ! [A: $i] : ( A @ empty ),
inference(miniscope,[status(thm)],[119]) ).
thf(121,plain,
~ ( sk6 @ empty ),
inference(cnf,[status(esa)],[120]) ).
thf(611,plain,
( ( ( sk6 @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[134,121]) ).
thf(612,plain,
( ( sk6 @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[611]) ).
thf(613,plain,
sk6 != empty_set,
inference(simp,[status(thm)],[612]) ).
thf(15809,plain,
! [B: $i,A: $i] :
( ( A != sk6 )
| ( B != empty_set )
| ( B @ ( A @ ( B @ sk12 ) @ in ) )
| ( A @ ( A @ ( B @ sk11 ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[250,613]) ).
thf(15810,plain,
! [A: $i] :
( ( A != empty_set )
| ( A @ ( sk6 @ ( A @ sk12 ) @ in ) )
| ( sk6 @ ( sk6 @ ( A @ sk11 ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[15809:[bind(A,$thf( sk6 ))]]) ).
thf(16251,plain,
( ( empty_set @ ( sk6 @ ( empty_set @ sk12 ) @ in ) )
| ( sk6 @ ( sk6 @ ( empty_set @ sk11 ) @ in ) ) ),
inference(simp,[status(thm)],[15810]) ).
thf(31082,plain,
( $false
| ( sk6 @ ( sk6 @ ( empty_set @ sk11 ) @ in ) ) ),
inference(rewrite,[status(thm)],[16251,336]) ).
thf(31083,plain,
sk6 @ ( sk6 @ ( empty_set @ sk11 ) @ in ),
inference(simp,[status(thm)],[31082]) ).
thf(259,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( A @ ( B @ ( C @ sk13 ) ) @ in ) )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ union ) ) ),
inference(cnfConj,[status(thm)],[256]) ).
thf(273,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( A @ ( B @ ( C @ sk13 ) ) @ in ) )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ union ) ) ),
inference(lifteq,[status(thm)],[259]) ).
thf(274,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ ( A @ union @ ( B @ sk13 ) ) @ in ) )
| ~ ( A @ union @ ( B @ in ) ) ),
inference(simp,[status(thm)],[273]) ).
thf(32127,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ union @ ( B @ sk13 ) ) @ in ) )
!= ( empty_set @ ( C @ in ) ) )
| ~ $true
| ~ ( A @ union @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[274,336]) ).
thf(32128,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ union @ ( B @ sk13 ) ) @ in ) )
!= ( empty_set @ ( C @ in ) ) )
| ~ ( A @ union @ ( B @ in ) ) ),
inference(simp,[status(thm)],[32127]) ).
thf(32129,plain,
! [A: $i] :
~ ( empty_set @ union @ ( A @ in ) ),
inference(pattern_uni,[status(thm)],[32128:[bind(A,$thf( empty_set )),bind(B,$thf( D )),bind(C,$thf( empty_set @ ( empty_set @ union @ ( D @ sk13 ) ) ))]]) ).
thf(32284,plain,
! [A: $i] :
~ ( empty_set @ union @ ( A @ in ) ),
inference(simp,[status(thm)],[32129]) ).
thf(32405,plain,
! [A: $i] :
( ( ( sk6 @ ( sk6 @ ( empty_set @ sk11 ) @ in ) )
!= ( empty_set @ union @ ( A @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[31083,32284]) ).
thf(32406,plain,
! [A: $i] :
( ( sk6 @ ( sk6 @ ( empty_set @ sk11 ) @ in ) )
!= ( empty_set @ union @ ( A @ in ) ) ),
inference(simp,[status(thm)],[32405]) ).
thf(32506,plain,
! [A: $i] :
( ( ( empty_set @ union )
!= sk6 )
| ( ( sk6 @ ( empty_set @ sk11 ) )
!= A ) ),
inference(simp,[status(thm)],[32406]) ).
thf(32563,plain,
( ( empty_set @ union )
!= sk6 ),
inference(simp,[status(thm)],[32506]) ).
thf(32606,plain,
! [B: $i,A: $i] :
( ( B
!= ( empty_set @ union ) )
| ( A != sk6 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,32563]) ).
thf(32607,plain,
! [A: $i] :
( ( A != sk6 )
| ~ ( A @ singleton @ ( empty_set @ union @ in ) ) ),
inference(pattern_uni,[status(thm)],[32606:[bind(A,$thf( A )),bind(B,$thf( empty_set @ union ))]]) ).
thf(32686,plain,
~ ( sk6 @ singleton @ ( empty_set @ union @ in ) ),
inference(simp,[status(thm)],[32607]) ).
thf(32742,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk6 @ singleton @ ( empty_set @ union @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[233,32686]) ).
thf(32743,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk6 @ singleton @ ( empty_set @ union @ in ) ) ),
inference(simp,[status(thm)],[32742]) ).
thf(32916,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk6 @ singleton ) )
| ( A
!= ( empty_set @ union ) ) ),
inference(simp,[status(thm)],[32743]) ).
thf(32950,plain,
( ( empty_set @ union @ singleton )
!= ( sk6 @ singleton ) ),
inference(simp,[status(thm)],[32916]) ).
thf(12941,plain,
! [B: $i,A: $i] :
( ( A != sk6 )
| ( B != empty_set )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,613]) ).
thf(12942,plain,
! [A: $i] :
( ( A != empty_set )
| ~ ( sk6 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[12941:[bind(A,$thf( sk6 ))]]) ).
thf(13437,plain,
~ ( sk6 @ singleton @ ( empty_set @ in ) ),
inference(simp,[status(thm)],[12942]) ).
thf(1112,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( B != empty_set )
| ~ ( sk3 @ empty )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[102,1104]) ).
thf(1113,plain,
! [A: $i] :
( ( A != empty_set )
| ~ ( sk3 @ empty )
| ~ ( A @ empty )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[1112:[bind(A,$thf( sk1 ))]]) ).
thf(1122,plain,
( ~ ( sk3 @ empty )
| ~ ( empty_set @ empty )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[1113]) ).
thf(2939,plain,
( ~ ( sk3 @ empty )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(rewrite,[status(thm)],[1122,134]) ).
thf(2940,plain,
( ~ ( sk3 @ empty )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[2939]) ).
thf(10,axiom,
! [A: $i,B: $i] : ( B @ ( A @ set_union2 ) @ ( A @ subset ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_xboole_1) ).
thf(114,plain,
! [A: $i,B: $i] : ( B @ ( A @ set_union2 ) @ ( A @ subset ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(115,plain,
! [B: $i,A: $i] : ( B @ ( A @ set_union2 ) @ ( A @ subset ) ),
inference(cnf,[status(esa)],[114]) ).
thf(9,axiom,
! [A: $i] :
( ( empty_set @ ( A @ subset ) )
=> ( A = empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_xboole_1) ).
thf(111,plain,
! [A: $i] :
( ( empty_set @ ( A @ subset ) )
=> ( A = empty_set ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(112,plain,
! [A: $i] :
( ( A = empty_set )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(cnf,[status(esa)],[111]) ).
thf(113,plain,
! [A: $i] :
( ~ ( empty_set @ ( A @ subset ) )
| ( A = empty_set ) ),
inference(lifteq,[status(thm)],[112]) ).
thf(1357,plain,
! [A: $i] :
( ( A != sk6 )
| ( empty_set != empty_set )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[113,613]) ).
thf(1358,plain,
! [A: $i] :
( ( A != sk6 )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[1357]) ).
thf(1359,plain,
~ ( empty_set @ ( sk6 @ subset ) ),
inference(pattern_uni,[status(thm)],[1358:[bind(A,$thf( sk6 ))]]) ).
thf(1495,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ set_union2 ) @ ( A @ subset ) )
!= ( empty_set @ ( sk6 @ subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,1359]) ).
thf(1496,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ set_union2 ) @ ( A @ subset ) )
!= ( empty_set @ ( sk6 @ subset ) ) ),
inference(simp,[status(thm)],[1495]) ).
thf(1514,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ set_union2 ) )
!= empty_set )
| ( A != sk6 ) ),
inference(simp,[status(thm)],[1496]) ).
thf(1522,plain,
! [A: $i] :
( ( A @ ( sk6 @ set_union2 ) )
!= empty_set ),
inference(simp,[status(thm)],[1514]) ).
thf(37,axiom,
! [A: $i,B: $i] : ( A @ ( B @ ( A @ set_intersection2 ) @ subset ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t17_xboole_1) ).
thf(214,plain,
! [A: $i,B: $i] : ( A @ ( B @ ( A @ set_intersection2 ) @ subset ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(215,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ set_intersection2 ) @ subset ) ),
inference(cnf,[status(esa)],[214]) ).
thf(1251,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ singleton ) )
| ( empty_set != empty_set )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[113,414]) ).
thf(1252,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ singleton ) )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[1251]) ).
thf(1253,plain,
! [A: $i] :
~ ( empty_set @ ( A @ singleton @ subset ) ),
inference(pattern_uni,[status(thm)],[1252:[bind(A,$thf( C @ singleton )),bind(B,$thf( C ))]]) ).
thf(1409,plain,
! [A: $i] :
~ ( empty_set @ ( A @ singleton @ subset ) ),
inference(simp,[status(thm)],[1253]) ).
thf(1586,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ set_intersection2 ) @ subset ) )
!= ( empty_set @ ( C @ singleton @ subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[215,1409]) ).
thf(1587,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( A @ set_intersection2 ) @ subset ) )
!= ( empty_set @ ( C @ singleton @ subset ) ) ),
inference(simp,[status(thm)],[1586]) ).
thf(1604,plain,
! [C: $i,B: $i,A: $i] :
( ( A != empty_set )
| ( ( B @ ( A @ set_intersection2 ) )
!= ( C @ singleton ) ) ),
inference(simp,[status(thm)],[1587]) ).
thf(1608,plain,
! [B: $i,A: $i] :
( ( A @ ( empty_set @ set_intersection2 ) )
!= ( B @ singleton ) ),
inference(simp,[status(thm)],[1604]) ).
thf(1592,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ set_intersection2 ) @ subset ) )
!= ( empty_set @ ( C @ subset ) ) )
| ~ $true
| ( C = empty_set ) ),
inference(paramod_ordered,[status(thm)],[215,113]) ).
thf(1593,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ set_intersection2 ) @ subset ) )
!= ( empty_set @ ( C @ subset ) ) )
| ( C = empty_set ) ),
inference(simp,[status(thm)],[1592]) ).
thf(1594,plain,
! [A: $i] :
( ( A @ ( empty_set @ set_intersection2 ) )
= empty_set ),
inference(pattern_uni,[status(thm)],[1593:[bind(A,$thf( empty_set )),bind(B,$thf( E )),bind(C,$thf( E @ ( empty_set @ set_intersection2 ) ))]]) ).
thf(1613,plain,
! [A: $i] :
( ( A @ ( empty_set @ set_intersection2 ) )
= empty_set ),
inference(simp,[status(thm)],[1594]) ).
thf(2644,plain,
! [A: $i] :
( ( A @ singleton )
!= empty_set ),
inference(rewrite,[status(thm)],[1608,1613]) ).
thf(81,axiom,
( ( empty_set @ powerset )
= ( empty_set @ singleton ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_zfmisc_1) ).
thf(600,plain,
( ( empty_set @ powerset )
= ( empty_set @ singleton ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(601,plain,
( ( empty_set @ powerset )
= ( empty_set @ singleton ) ),
inference(lifteq,[status(thm)],[600]) ).
thf(6458,plain,
! [A: $i] :
( ( A
!= ( empty_set @ powerset ) )
| ( ( empty_set @ singleton )
= empty_set )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,601]) ).
thf(6459,plain,
( ( ( empty_set @ singleton )
= empty_set )
| ( empty_set @ powerset @ ( empty_set @ proper_subset ) ) ),
inference(pattern_uni,[status(thm)],[6458:[bind(A,$thf( empty_set @ powerset ))]]) ).
thf(9900,plain,
( ( ( empty_set @ singleton )
= empty_set )
| ( empty_set @ singleton @ ( empty_set @ proper_subset ) ) ),
inference(rewrite,[status(thm)],[6459,601]) ).
thf(9901,plain,
empty_set @ singleton @ ( empty_set @ proper_subset ),
inference(simplifyReflect,[status(thm)],[9900,414]) ).
thf(2973,plain,
( ~ $true
| ( ( sk3 @ empty )
!= ( sk1 @ empty ) )
| ~ ( sk1 @ empty ) ),
inference(eqfactor_ordered,[status(thm)],[2940]) ).
thf(2979,plain,
( ( sk3 != sk1 )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[2973]) ).
thf(3177,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk3 != sk1 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[134,2979]) ).
thf(3178,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[3177]) ).
thf(3203,plain,
( ( sk1 != empty_set )
| ( sk3 != sk1 ) ),
inference(simp,[status(thm)],[3178]) ).
thf(3283,plain,
! [A: $i] :
( ( A != sk1 )
| ( empty_set != empty_set )
| ( sk3 != sk1 )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[113,3203]) ).
thf(3284,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk3 != sk1 )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[3283]) ).
thf(3285,plain,
( ( sk3 != sk1 )
| ~ ( empty_set @ ( sk1 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[3284:[bind(A,$thf( sk1 ))]]) ).
thf(32442,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ union @ ( B @ sk13 ) ) @ in ) )
!= ( empty_set @ union @ ( C @ in ) ) )
| ~ $true
| ~ ( A @ union @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[274,32284]) ).
thf(32443,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ union @ ( B @ sk13 ) ) @ in ) )
!= ( empty_set @ union @ ( C @ in ) ) )
| ~ ( A @ union @ ( B @ in ) ) ),
inference(simp,[status(thm)],[32442]) ).
thf(32444,plain,
! [A: $i] :
~ ( empty_set @ union @ union @ ( A @ in ) ),
inference(pattern_uni,[status(thm)],[32443:[bind(A,$thf( empty_set @ union )),bind(B,$thf( D )),bind(C,$thf( empty_set @ union @ ( empty_set @ union @ union @ ( D @ sk13 ) ) ))]]) ).
thf(32532,plain,
! [A: $i] :
~ ( empty_set @ union @ union @ ( A @ in ) ),
inference(simp,[status(thm)],[32444]) ).
thf(37455,plain,
! [A: $i] :
( ( ( sk6 @ ( sk6 @ ( empty_set @ sk11 ) @ in ) )
!= ( empty_set @ union @ union @ ( A @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[31083,32532]) ).
thf(37456,plain,
! [A: $i] :
( ( sk6 @ ( sk6 @ ( empty_set @ sk11 ) @ in ) )
!= ( empty_set @ union @ union @ ( A @ in ) ) ),
inference(simp,[status(thm)],[37455]) ).
thf(37598,plain,
! [A: $i] :
( ( ( empty_set @ union @ union )
!= sk6 )
| ( ( sk6 @ ( empty_set @ sk11 ) )
!= A ) ),
inference(simp,[status(thm)],[37456]) ).
thf(37692,plain,
( ( empty_set @ union @ union )
!= sk6 ),
inference(simp,[status(thm)],[37598]) ).
thf(37765,plain,
! [B: $i,A: $i] :
( ( B
!= ( empty_set @ union @ union ) )
| ( A != sk6 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,37692]) ).
thf(37766,plain,
! [A: $i] :
( ( A != sk6 )
| ~ ( A @ singleton @ ( empty_set @ union @ union @ in ) ) ),
inference(pattern_uni,[status(thm)],[37765:[bind(A,$thf( A )),bind(B,$thf( empty_set @ union @ union ))]]) ).
thf(37871,plain,
~ ( sk6 @ singleton @ ( empty_set @ union @ union @ in ) ),
inference(simp,[status(thm)],[37766]) ).
thf(6,axiom,
? [A: $i] : ( A @ empty ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_xboole_0) ).
thf(103,plain,
? [A: $i] : ( A @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(104,plain,
sk5 @ empty,
inference(cnf,[status(esa)],[103]) ).
thf(4621,plain,
! [A: $i] :
( ( ( sk5 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[104,154]) ).
thf(4622,plain,
! [A: $i] :
( ( ( sk5 @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[4621]) ).
thf(4623,plain,
sk5 = empty_set,
inference(pattern_uni,[status(thm)],[4622:[bind(A,$thf( sk5 ))]]) ).
thf(54,axiom,
! [A: $i] :
( ( empty_set @ ( A @ set_difference ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_boole) ).
thf(384,plain,
! [A: $i] :
( ( empty_set @ ( A @ set_difference ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(1308,plain,
! [A: $i] :
( ( A != sk1 )
| ( empty_set != empty_set )
| ~ ( sk3 @ empty )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[113,1104]) ).
thf(1309,plain,
! [A: $i] :
( ( A != sk1 )
| ~ ( sk3 @ empty )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[1308]) ).
thf(1310,plain,
( ~ ( sk3 @ empty )
| ~ ( empty_set @ ( sk1 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[1309:[bind(A,$thf( sk1 ))]]) ).
thf(18,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
=> ( ( B @ ( A @ set_intersection2 ) )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t28_xboole_1) ).
thf(142,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
=> ( ( B @ ( A @ set_intersection2 ) )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(12218,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( B != empty_set )
| ( sk3 != empty_set )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,651]) ).
thf(12219,plain,
! [A: $i] :
( ( A != empty_set )
| ( sk3 != empty_set )
| ~ ( sk1 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[12218:[bind(A,$thf( sk1 ))]]) ).
thf(13596,plain,
( ( sk3 != empty_set )
| ~ ( sk1 @ singleton @ ( empty_set @ in ) ) ),
inference(simp,[status(thm)],[12219]) ).
thf(7,axiom,
! [A: $i,B: $i] :
~ ( ( A @ ( B @ proper_subset ) )
& ( B @ ( A @ subset ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t60_xboole_1) ).
thf(105,plain,
! [A: $i,B: $i] :
~ ( ( A @ ( B @ proper_subset ) )
& ( B @ ( A @ subset ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(106,plain,
~ ? [A: $i,B: $i] :
( ( A @ ( B @ proper_subset ) )
& ( B @ ( A @ subset ) ) ),
inference(miniscope,[status(thm)],[105]) ).
thf(107,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ proper_subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnf,[status(esa)],[106]) ).
thf(1127,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( empty_set @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ~ ( B @ ( C @ proper_subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[183,107]) ).
thf(1128,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( empty_set @ subset ) )
!= ( C @ ( B @ subset ) ) )
| ~ ( B @ ( C @ proper_subset ) ) ),
inference(simp,[status(thm)],[1127]) ).
thf(1129,plain,
! [A: $i] :
~ ( empty_set @ ( A @ proper_subset ) ),
inference(pattern_uni,[status(thm)],[1128:[bind(A,$thf( A )),bind(B,$thf( empty_set )),bind(C,$thf( A ))]]) ).
thf(9984,plain,
! [A: $i] :
( ( ( empty_set @ singleton @ ( empty_set @ proper_subset ) )
!= ( empty_set @ ( A @ proper_subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9901,1129]) ).
thf(9985,plain,
! [A: $i] :
( ( empty_set @ singleton @ ( empty_set @ proper_subset ) )
!= ( empty_set @ ( A @ proper_subset ) ) ),
inference(simp,[status(thm)],[9984]) ).
thf(9986,plain,
! [A: $i] :
( ( ( empty_set @ singleton )
!= empty_set )
| ( empty_set != A ) ),
inference(simp,[status(thm)],[9985]) ).
thf(9989,plain,
( ( empty_set @ singleton )
!= empty_set ),
inference(simp,[status(thm)],[9986]) ).
thf(12228,plain,
! [B: $i,A: $i] :
( ( B
!= ( empty_set @ singleton ) )
| ( A != empty_set )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,9989]) ).
thf(12229,plain,
! [A: $i] :
( ( A != empty_set )
| ~ ( A @ singleton @ ( empty_set @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[12228:[bind(A,$thf( A )),bind(B,$thf( empty_set @ singleton ))]]) ).
thf(13601,plain,
~ ( empty_set @ singleton @ ( empty_set @ singleton @ in ) ),
inference(simp,[status(thm)],[12229]) ).
thf(13951,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( empty_set @ singleton @ ( empty_set @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[233,13601]) ).
thf(13952,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( empty_set @ singleton @ ( empty_set @ singleton @ in ) ) ),
inference(simp,[status(thm)],[13951]) ).
thf(14048,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( empty_set @ singleton ) )
| ( A
!= ( empty_set @ singleton ) ) ),
inference(simp,[status(thm)],[13952]) ).
thf(14065,plain,
( ( empty_set @ singleton @ singleton )
!= ( empty_set @ singleton ) ),
inference(simp,[status(thm)],[14048]) ).
thf(14307,plain,
! [B: $i,A: $i] :
( ( B
!= ( empty_set @ singleton @ singleton ) )
| ( A
!= ( empty_set @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,14065]) ).
thf(14308,plain,
! [A: $i] :
( ( A
!= ( empty_set @ singleton ) )
| ~ ( A @ singleton @ ( empty_set @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[14307:[bind(A,$thf( A )),bind(B,$thf( empty_set @ singleton @ singleton ))]]) ).
thf(14368,plain,
~ ( empty_set @ singleton @ singleton @ ( empty_set @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[14308]) ).
thf(16597,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( empty_set @ singleton @ singleton @ ( empty_set @ singleton @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[233,14368]) ).
thf(16598,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( empty_set @ singleton @ singleton @ ( empty_set @ singleton @ singleton @ in ) ) ),
inference(simp,[status(thm)],[16597]) ).
thf(16755,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( empty_set @ singleton @ singleton ) )
| ( A
!= ( empty_set @ singleton @ singleton ) ) ),
inference(simp,[status(thm)],[16598]) ).
thf(16784,plain,
( ( empty_set @ singleton @ singleton @ singleton )
!= ( empty_set @ singleton @ singleton ) ),
inference(simp,[status(thm)],[16755]) ).
thf(1737,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( sk6 @ set_union2 ) ) )
| ( empty_set != empty_set )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[113,1522]) ).
thf(1738,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( sk6 @ set_union2 ) ) )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[1737]) ).
thf(1739,plain,
! [A: $i] :
~ ( empty_set @ ( A @ ( sk6 @ set_union2 ) @ subset ) ),
inference(pattern_uni,[status(thm)],[1738:[bind(A,$thf( D @ ( sk6 @ set_union2 ) )),bind(B,$thf( D ))]]) ).
thf(1746,plain,
! [A: $i] :
~ ( empty_set @ ( A @ ( sk6 @ set_union2 ) @ subset ) ),
inference(simp,[status(thm)],[1739]) ).
thf(2526,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ set_union2 ) @ ( A @ subset ) )
!= ( empty_set @ ( C @ ( sk6 @ set_union2 ) @ subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,1746]) ).
thf(2527,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ set_union2 ) @ ( A @ subset ) )
!= ( empty_set @ ( C @ ( sk6 @ set_union2 ) @ subset ) ) ),
inference(simp,[status(thm)],[2526]) ).
thf(2568,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ set_union2 ) )
!= empty_set )
| ( A
!= ( C @ ( sk6 @ set_union2 ) ) ) ),
inference(simp,[status(thm)],[2527]) ).
thf(2575,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( sk6 @ set_union2 ) @ set_union2 ) )
!= empty_set ),
inference(simp,[status(thm)],[2568]) ).
thf(89,plain,
( ~ ( sk3 @ ( sk4 @ in ) )
| ( sk1 @ ( sk2 @ in ) ) ),
inference(cnfConj,[status(thm)],[86]) ).
thf(1029,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk3 @ ( sk4 @ in ) ) )
| ~ $true
| ( sk1 @ ( sk2 @ in ) ) ),
inference(paramod_ordered,[status(thm)],[233,89]) ).
thf(1030,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk3 @ ( sk4 @ in ) ) )
| ( sk1 @ ( sk2 @ in ) ) ),
inference(simp,[status(thm)],[1029]) ).
thf(1044,plain,
! [A: $i] :
( ( ( A @ singleton )
!= sk3 )
| ( A != sk4 )
| ( sk1 @ ( sk2 @ in ) ) ),
inference(simp,[status(thm)],[1030]) ).
thf(1048,plain,
( ( ( sk4 @ singleton )
!= sk3 )
| ( sk1 @ ( sk2 @ in ) ) ),
inference(simp,[status(thm)],[1044]) ).
thf(3864,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ in ) )
!= ( empty_set @ ( A @ in ) ) )
| ~ $true
| ( ( sk4 @ singleton )
!= sk3 ) ),
inference(paramod_ordered,[status(thm)],[1048,336]) ).
thf(3865,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ in ) )
!= ( empty_set @ ( A @ in ) ) )
| ( ( sk4 @ singleton )
!= sk3 ) ),
inference(simp,[status(thm)],[3864]) ).
thf(3868,plain,
! [A: $i] :
( ( sk1 != empty_set )
| ( sk2 != A )
| ( ( sk4 @ singleton )
!= sk3 ) ),
inference(simp,[status(thm)],[3865]) ).
thf(3878,plain,
( ( sk1 != empty_set )
| ( ( sk4 @ singleton )
!= sk3 ) ),
inference(simp,[status(thm)],[3868]) ).
thf(12939,plain,
! [B: $i,A: $i] :
( ( B != sk6 )
| ( A != empty_set )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,613]) ).
thf(12940,plain,
! [A: $i] :
( ( A != empty_set )
| ~ ( A @ singleton @ ( sk6 @ in ) ) ),
inference(pattern_uni,[status(thm)],[12939:[bind(A,$thf( A )),bind(B,$thf( sk6 ))]]) ).
thf(13436,plain,
~ ( empty_set @ singleton @ ( sk6 @ in ) ),
inference(simp,[status(thm)],[12940]) ).
thf(13647,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( empty_set @ singleton @ ( sk6 @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[233,13436]) ).
thf(13648,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( empty_set @ singleton @ ( sk6 @ in ) ) ),
inference(simp,[status(thm)],[13647]) ).
thf(13719,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( empty_set @ singleton ) )
| ( A != sk6 ) ),
inference(simp,[status(thm)],[13648]) ).
thf(13730,plain,
( ( sk6 @ singleton )
!= ( empty_set @ singleton ) ),
inference(simp,[status(thm)],[13719]) ).
thf(13875,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk6 @ singleton ) )
| ( A
!= ( empty_set @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,13730]) ).
thf(13876,plain,
! [A: $i] :
( ( A
!= ( empty_set @ singleton ) )
| ~ ( A @ singleton @ ( sk6 @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[13875:[bind(A,$thf( A )),bind(B,$thf( sk6 @ singleton ))]]) ).
thf(13916,plain,
~ ( empty_set @ singleton @ singleton @ ( sk6 @ singleton @ in ) ),
inference(simp,[status(thm)],[13876]) ).
thf(14464,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( empty_set @ singleton @ singleton @ ( sk6 @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[233,13916]) ).
thf(14465,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( empty_set @ singleton @ singleton @ ( sk6 @ singleton @ in ) ) ),
inference(simp,[status(thm)],[14464]) ).
thf(14575,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( empty_set @ singleton @ singleton ) )
| ( A
!= ( sk6 @ singleton ) ) ),
inference(simp,[status(thm)],[14465]) ).
thf(14599,plain,
( ( sk6 @ singleton @ singleton )
!= ( empty_set @ singleton @ singleton ) ),
inference(simp,[status(thm)],[14575]) ).
thf(14814,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk6 @ singleton @ singleton ) )
| ( A
!= ( empty_set @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,14599]) ).
thf(14815,plain,
! [A: $i] :
( ( A
!= ( empty_set @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( sk6 @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[14814:[bind(A,$thf( A )),bind(B,$thf( sk6 @ singleton @ singleton ))]]) ).
thf(14871,plain,
~ ( empty_set @ singleton @ singleton @ singleton @ ( sk6 @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[14815]) ).
thf(32610,plain,
! [B: $i,A: $i] :
( ( A
!= ( empty_set @ union ) )
| ( B != sk6 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,32563]) ).
thf(32611,plain,
! [A: $i] :
( ( A != sk6 )
| ~ ( empty_set @ union @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[32610:[bind(A,$thf( empty_set @ union )),bind(B,$thf( B ))]]) ).
thf(32687,plain,
~ ( empty_set @ union @ singleton @ ( sk6 @ in ) ),
inference(simp,[status(thm)],[32611]) ).
thf(28,axiom,
! [A: $i,B: $i] :
( ~ ( A @ empty )
=> ~ ( B @ ( A @ set_union2 ) @ empty ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_xboole_0) ).
thf(184,plain,
! [A: $i,B: $i] :
( ~ ( A @ empty )
=> ~ ( B @ ( A @ set_union2 ) @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(8,axiom,
! [A: $i] :
( ( empty_set @ ( A @ set_union2 ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_boole) ).
thf(108,plain,
! [A: $i] :
( ( empty_set @ ( A @ set_union2 ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(109,plain,
! [A: $i] :
( ( empty_set @ ( A @ set_union2 ) )
= A ),
inference(cnf,[status(esa)],[108]) ).
thf(110,plain,
! [A: $i] :
( ( empty_set @ ( A @ set_union2 ) )
= A ),
inference(lifteq,[status(thm)],[109]) ).
thf(79,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ singleton @ subset ) )
<=> ( B @ ( A @ in ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l2_zfmisc_1) ).
thf(587,plain,
! [A: $i,B: $i] :
( ( ( B @ ( A @ in ) )
=> ( B @ ( A @ singleton @ subset ) ) )
& ( ( B @ ( A @ singleton @ subset ) )
=> ( B @ ( A @ in ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(34961,plain,
! [B: $i,A: $i] :
( ( B
!= ( empty_set @ union @ singleton ) )
| ( A
!= ( sk6 @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,32950]) ).
thf(34962,plain,
! [A: $i] :
( ( A
!= ( sk6 @ singleton ) )
| ~ ( A @ singleton @ ( empty_set @ union @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[34961:[bind(A,$thf( A )),bind(B,$thf( empty_set @ union @ singleton ))]]) ).
thf(35058,plain,
~ ( sk6 @ singleton @ singleton @ ( empty_set @ union @ singleton @ in ) ),
inference(simp,[status(thm)],[34962]) ).
thf(35397,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk6 @ singleton @ singleton @ ( empty_set @ union @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[233,35058]) ).
thf(35398,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk6 @ singleton @ singleton @ ( empty_set @ union @ singleton @ in ) ) ),
inference(simp,[status(thm)],[35397]) ).
thf(35648,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk6 @ singleton @ singleton ) )
| ( A
!= ( empty_set @ union @ singleton ) ) ),
inference(simp,[status(thm)],[35398]) ).
thf(35682,plain,
( ( empty_set @ union @ singleton @ singleton )
!= ( sk6 @ singleton @ singleton ) ),
inference(simp,[status(thm)],[35648]) ).
thf(301,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ in ) )
| ( D != A )
| ( C
!= ( B @ ( A @ unordered_pair ) ) ) ),
inference(cnfConj,[status(thm)],[294]) ).
thf(303,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ in ) )
| ( D != A )
| ( C
!= ( B @ ( A @ unordered_pair ) ) ) ),
inference(lifteq,[status(thm)],[301]) ).
thf(304,plain,
! [B: $i,A: $i] : ( B @ ( A @ unordered_pair ) @ ( A @ in ) ),
inference(simp,[status(thm)],[303]) ).
thf(1821,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) @ ( A @ in ) )
!= ( empty_set @ ( C @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[304,336]) ).
thf(1822,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( A @ in ) )
!= ( empty_set @ ( C @ in ) ) ),
inference(simp,[status(thm)],[1821]) ).
thf(1827,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= empty_set )
| ( A != C ) ),
inference(simp,[status(thm)],[1822]) ).
thf(1832,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ unordered_pair ) )
!= empty_set ),
inference(simp,[status(thm)],[1827]) ).
thf(32,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ disjoint ) )
<=> ( ( B @ ( A @ set_intersection2 ) )
= empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d7_xboole_0) ).
thf(196,plain,
! [A: $i,B: $i] :
( ( ( ( B @ ( A @ set_intersection2 ) )
= empty_set )
=> ( B @ ( A @ disjoint ) ) )
& ( ( B @ ( A @ disjoint ) )
=> ( ( B @ ( A @ set_intersection2 ) )
= empty_set ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(64,axiom,
! [A: $i,B: $i] :
( ~ ( B @ ( A @ in ) )
=> ( B @ ( A @ singleton @ disjoint ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l28_zfmisc_1) ).
thf(460,plain,
! [A: $i,B: $i] :
( ~ ( B @ ( A @ in ) )
=> ( B @ ( A @ singleton @ disjoint ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(22,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ unordered_pair ) )
= ( A @ ( B @ unordered_pair ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
thf(155,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ unordered_pair ) )
= ( A @ ( B @ unordered_pair ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(156,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) )
= ( A @ ( B @ unordered_pair ) ) ),
inference(cnf,[status(esa)],[155]) ).
thf(157,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) )
= ( A @ ( B @ unordered_pair ) ) ),
inference(lifteq,[status(thm)],[156]) ).
thf(6609,plain,
! [A: $i] :
( ( A != sk1 )
| ( empty_set != empty_set )
| ( sk3 != sk1 )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,3203]) ).
thf(6610,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk3 != sk1 )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6609]) ).
thf(6611,plain,
( ( sk3 != sk1 )
| ( sk1 @ ( empty_set @ proper_subset ) ) ),
inference(pattern_uni,[status(thm)],[6610:[bind(A,$thf( sk1 ))]]) ).
thf(39597,plain,
! [B: $i,A: $i] :
( ( ( sk6 @ ( sk6 @ ( empty_set @ sk11 ) @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( A @ ( B @ in ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[31083,282]) ).
thf(39598,plain,
! [B: $i,A: $i] :
( ( ( sk6 @ ( sk6 @ ( empty_set @ sk11 ) @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( A @ ( B @ in ) ) ),
inference(simp,[status(thm)],[39597]) ).
thf(39599,plain,
~ ( sk6 @ ( empty_set @ sk11 ) @ ( sk6 @ in ) ),
inference(pattern_uni,[status(thm)],[39598:[bind(A,$thf( sk6 @ ( empty_set @ sk11 ) )),bind(B,$thf( sk6 ))]]) ).
thf(39757,plain,
( ( ( sk6 @ ( sk6 @ ( empty_set @ sk11 ) @ in ) )
!= ( sk6 @ ( empty_set @ sk11 ) @ ( sk6 @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[31083,39599]) ).
thf(39758,plain,
( ( sk6 @ ( sk6 @ ( empty_set @ sk11 ) @ in ) )
!= ( sk6 @ ( empty_set @ sk11 ) @ ( sk6 @ in ) ) ),
inference(simp,[status(thm)],[39757]) ).
thf(39913,plain,
( ( ( sk6 @ ( empty_set @ sk11 ) )
!= sk6 )
| ( ( sk6 @ ( empty_set @ sk11 ) )
!= sk6 ) ),
inference(simp,[status(thm)],[39758]) ).
thf(39960,plain,
( ( sk6 @ ( empty_set @ sk11 ) )
!= sk6 ),
inference(simp,[status(thm)],[39913]) ).
thf(40022,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk6 @ ( empty_set @ sk11 ) ) )
| ( A != sk6 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,39960]) ).
thf(40023,plain,
! [A: $i] :
( ( A != sk6 )
| ~ ( A @ singleton @ ( sk6 @ ( empty_set @ sk11 ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[40022:[bind(A,$thf( A )),bind(B,$thf( sk6 @ ( empty_set @ sk11 ) ))]]) ).
thf(40130,plain,
~ ( sk6 @ singleton @ ( sk6 @ ( empty_set @ sk11 ) @ in ) ),
inference(simp,[status(thm)],[40023]) ).
thf(45,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ singleton @ subset ) )
<=> ( B @ ( A @ in ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t37_zfmisc_1) ).
thf(286,plain,
! [A: $i,B: $i] :
( ( ( B @ ( A @ in ) )
=> ( B @ ( A @ singleton @ subset ) ) )
& ( ( B @ ( A @ singleton @ subset ) )
=> ( B @ ( A @ in ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(287,plain,
( ! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ( B @ ( A @ singleton @ subset ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ singleton @ subset ) )
=> ( B @ ( A @ in ) ) ) ),
inference(miniscope,[status(thm)],[286]) ).
thf(288,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ singleton @ subset ) )
| ~ ( D @ ( C @ in ) ) )
& ( ( B @ ( A @ in ) )
| ~ ( B @ ( A @ singleton @ subset ) ) ) ),
inference(cnf,[status(esa)],[287]) ).
thf(289,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ in ) )
| ~ ( B @ ( A @ singleton @ subset ) ) ),
inference(cnfConj,[status(thm)],[288]) ).
thf(38,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ set_union2 ) )
= ( A @ ( B @ set_union2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_xboole_0) ).
thf(216,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ set_union2 ) )
= ( A @ ( B @ set_union2 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(36,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
=> ( ( B @ ( A @ set_union2 ) )
= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_xboole_1) ).
thf(211,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
=> ( ( B @ ( A @ set_union2 ) )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(249,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( A @ ( B @ sk12 ) @ in ) )
| ~ ( B @ ( A @ ( B @ sk11 ) @ in ) ) ),
inference(cnfConj,[status(thm)],[245]) ).
thf(253,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( A @ ( B @ sk12 ) @ in ) )
| ~ ( B @ ( A @ ( B @ sk11 ) @ in ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[249]) ).
thf(57,axiom,
! [A: $i,B: $i] :
( ( B @ singleton @ ( A @ singleton @ subset ) )
=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_zfmisc_1) ).
thf(397,plain,
! [A: $i,B: $i] :
( ( B @ singleton @ ( A @ singleton @ subset ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(262,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( C @ in ) )
| ~ ( A @ ( D @ in ) )
| ~ ( D @ ( C @ in ) )
| ( B
!= ( A @ union ) ) ),
inference(cnfConj,[status(thm)],[256]) ).
thf(279,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( C @ in ) )
| ~ ( A @ ( D @ in ) )
| ~ ( D @ ( C @ in ) )
| ( B
!= ( A @ union ) ) ),
inference(lifteq,[status(thm)],[262]) ).
thf(280,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ union @ ( B @ in ) )
| ~ ( A @ ( C @ in ) )
| ~ ( C @ ( B @ in ) ) ),
inference(simp,[status(thm)],[279]) ).
thf(6231,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ singleton ) )
| ( empty_set != empty_set )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,2644]) ).
thf(6232,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ singleton ) )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6231]) ).
thf(6233,plain,
! [A: $i] : ( A @ singleton @ ( empty_set @ proper_subset ) ),
inference(pattern_uni,[status(thm)],[6232:[bind(A,$thf( C @ singleton )),bind(B,$thf( C ))]]) ).
thf(6646,plain,
! [A: $i] : ( A @ singleton @ ( empty_set @ proper_subset ) ),
inference(simp,[status(thm)],[6233]) ).
thf(1492,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ set_union2 ) @ ( A @ subset ) )
!= ( D @ ( C @ subset ) ) )
| ~ ( C @ ( D @ proper_subset ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,107]) ).
thf(1493,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ set_union2 ) @ ( A @ subset ) )
!= ( D @ ( C @ subset ) ) )
| ~ ( C @ ( D @ proper_subset ) ) ),
inference(simp,[status(thm)],[1492]) ).
thf(1494,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ ( A @ set_union2 ) @ proper_subset ) ),
inference(pattern_uni,[status(thm)],[1493:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ set_union2 ) ))]]) ).
thf(1519,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ ( A @ set_union2 ) @ proper_subset ) ),
inference(simp,[status(thm)],[1494]) ).
thf(7334,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton @ ( empty_set @ proper_subset ) )
!= ( B @ ( C @ ( B @ set_union2 ) @ proper_subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6646,1519]) ).
thf(7335,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ singleton @ ( empty_set @ proper_subset ) )
!= ( B @ ( C @ ( B @ set_union2 ) @ proper_subset ) ) ),
inference(simp,[status(thm)],[7334]) ).
thf(7374,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton )
!= B )
| ( ( C @ ( B @ set_union2 ) )
!= empty_set ) ),
inference(simp,[status(thm)],[7335]) ).
thf(7381,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ singleton @ set_union2 ) )
!= empty_set ),
inference(simp,[status(thm)],[7374]) ).
thf(1497,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ set_union2 ) @ ( A @ subset ) )
!= ( empty_set @ ( C @ singleton @ subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[115,1409]) ).
thf(1498,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ set_union2 ) @ ( A @ subset ) )
!= ( empty_set @ ( C @ singleton @ subset ) ) ),
inference(simp,[status(thm)],[1497]) ).
thf(1513,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ set_union2 ) )
!= empty_set )
| ( A
!= ( C @ singleton ) ) ),
inference(simp,[status(thm)],[1498]) ).
thf(1521,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ singleton @ set_union2 ) )
!= empty_set ),
inference(simp,[status(thm)],[1513]) ).
thf(33,axiom,
! [A: $i,B: $i] :
( ( A @ ( A @ set_union2 ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_k2_xboole_0) ).
thf(204,plain,
! [A: $i] :
( ( A @ ( A @ set_union2 ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(205,plain,
! [A: $i] :
( ( A @ ( A @ set_union2 ) )
= A ),
inference(cnf,[status(esa)],[204]) ).
thf(206,plain,
! [A: $i] :
( ( A @ ( A @ set_union2 ) )
= A ),
inference(lifteq,[status(thm)],[205]) ).
thf(1202,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk1 != empty_set )
| ( empty_set != empty_set )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[113,651]) ).
thf(1203,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk1 != empty_set )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[1202]) ).
thf(1204,plain,
( ( sk1 != empty_set )
| ~ ( empty_set @ ( sk3 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[1203:[bind(A,$thf( sk3 ))]]) ).
thf(1562,plain,
! [A: $i] :
( ( A != sk1 )
| ( empty_set != empty_set )
| ~ ( empty_set @ ( sk3 @ subset ) )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[113,1204]) ).
thf(1563,plain,
! [A: $i] :
( ( A != sk1 )
| ~ ( empty_set @ ( sk3 @ subset ) )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[1562]) ).
thf(1564,plain,
( ~ ( empty_set @ ( sk3 @ subset ) )
| ~ ( empty_set @ ( sk1 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[1563:[bind(A,$thf( sk1 ))]]) ).
thf(82,axiom,
! [A: $i,B: $i] :
~ ( ( B @ ( A @ in ) )
& ( B @ ( A @ singleton @ disjoint ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l25_zfmisc_1) ).
thf(602,plain,
! [A: $i,B: $i] :
~ ( ( B @ ( A @ in ) )
& ( B @ ( A @ singleton @ disjoint ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(38378,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk6 @ singleton @ ( empty_set @ union @ union @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[233,37871]) ).
thf(38379,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk6 @ singleton @ ( empty_set @ union @ union @ in ) ) ),
inference(simp,[status(thm)],[38378]) ).
thf(38614,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk6 @ singleton ) )
| ( A
!= ( empty_set @ union @ union ) ) ),
inference(simp,[status(thm)],[38379]) ).
thf(38667,plain,
( ( empty_set @ union @ union @ singleton )
!= ( sk6 @ singleton ) ),
inference(simp,[status(thm)],[38614]) ).
thf(13,axiom,
! [A: $i,B: $i] :
( ( A = B )
<=> ( ( A @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
thf(122,plain,
! [A: $i,B: $i] :
( ( ( ( A @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( A = B ) )
& ( ( A = B )
=> ( ( A @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(123,plain,
( ! [A: $i,B: $i] :
( ( ( A @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( A = B ) )
& ! [A: $i,B: $i] :
( ( A = B )
=> ( ( A @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) ) ) ),
inference(miniscope,[status(thm)],[122]) ).
thf(124,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C = D )
| ~ ( C @ ( D @ subset ) )
| ~ ( D @ ( C @ subset ) ) )
& ( ( A @ ( B @ subset ) )
| ( A != B ) )
& ( ( B @ ( A @ subset ) )
| ( A != B ) ) ),
inference(cnf,[status(esa)],[123]) ).
thf(127,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnfConj,[status(thm)],[124]) ).
thf(132,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ subset ) )
| ~ ( B @ ( A @ subset ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[127]) ).
thf(133,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ subset ) )
| ~ ( B @ ( A @ subset ) )
| ( A = B ) ),
inference(simp,[status(thm)],[132]) ).
thf(11,axiom,
! [A: $i,B: $i] :
( ~ ( A @ empty )
=> ~ ( A @ ( B @ set_union2 ) @ empty ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_xboole_0) ).
thf(116,plain,
! [A: $i,B: $i] :
( ~ ( A @ empty )
=> ~ ( A @ ( B @ set_union2 ) @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(75,axiom,
! [A: $i,B: $i,C: $i] :
( ( C
= ( B @ ( A @ cartesian_product2 ) ) )
<=> ! [D: $i] :
( ( C @ ( D @ in ) )
<=> ? [E: $i,F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) )
& ( A @ ( E @ in ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_zfmisc_1) ).
thf(546,plain,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i] :
( ( ? [E: $i,F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) )
& ( A @ ( E @ in ) ) )
=> ( C @ ( D @ in ) ) )
& ( ( C @ ( D @ in ) )
=> ? [E: $i,F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) )
& ( A @ ( E @ in ) ) ) ) )
=> ( C
= ( B @ ( A @ cartesian_product2 ) ) ) )
& ( ( C
= ( B @ ( A @ cartesian_product2 ) ) )
=> ! [D: $i] :
( ( ? [E: $i,F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) )
& ( A @ ( E @ in ) ) )
=> ( C @ ( D @ in ) ) )
& ( ( C @ ( D @ in ) )
=> ? [E: $i,F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) )
& ( A @ ( E @ in ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(197,plain,
( ! [A: $i,B: $i] :
( ( ( B @ ( A @ set_intersection2 ) )
= empty_set )
=> ( B @ ( A @ disjoint ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ disjoint ) )
=> ( ( B @ ( A @ set_intersection2 ) )
= empty_set ) ) ),
inference(miniscope,[status(thm)],[196]) ).
thf(198,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ disjoint ) )
| ( ( D @ ( C @ set_intersection2 ) )
!= empty_set ) )
& ( ( ( B @ ( A @ set_intersection2 ) )
= empty_set )
| ~ ( B @ ( A @ disjoint ) ) ) ),
inference(cnf,[status(esa)],[197]) ).
thf(199,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ set_intersection2 ) )
= empty_set )
| ~ ( B @ ( A @ disjoint ) ) ),
inference(cnfConj,[status(thm)],[198]) ).
thf(201,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ disjoint ) )
| ( ( B @ ( A @ set_intersection2 ) )
= empty_set ) ),
inference(lifteq,[status(thm)],[199]) ).
thf(53,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ set_difference ) @ ( A @ set_difference ) )
= ( B @ ( A @ set_intersection2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_xboole_1) ).
thf(381,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ set_difference ) @ ( A @ set_difference ) )
= ( B @ ( A @ set_intersection2 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(6280,plain,
! [A: $i] :
( ( A != sk1 )
| ( empty_set != empty_set )
| ( sk3 != empty_set )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,651]) ).
thf(6281,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk3 != empty_set )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6280]) ).
thf(6282,plain,
( ( sk3 != empty_set )
| ( sk1 @ ( empty_set @ proper_subset ) ) ),
inference(pattern_uni,[status(thm)],[6281:[bind(A,$thf( sk1 ))]]) ).
thf(4411,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ singleton @ set_union2 ) ) )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[154,1521]) ).
thf(4412,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ singleton @ set_union2 ) ) )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[4411]) ).
thf(4413,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ singleton @ set_union2 ) @ empty ),
inference(pattern_uni,[status(thm)],[4412:[bind(A,$thf( E @ ( F @ singleton @ set_union2 ) )),bind(B,$thf( E )),bind(C,$thf( F ))]]) ).
thf(4700,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ singleton @ set_union2 ) @ empty ),
inference(simp,[status(thm)],[4413]) ).
thf(260,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ sk13 ) ) @ ( C @ in ) )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ union ) ) ),
inference(cnfConj,[status(thm)],[256]) ).
thf(269,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ sk13 ) ) @ ( C @ in ) )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ union ) ) ),
inference(lifteq,[status(thm)],[260]) ).
thf(270,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ union @ ( B @ sk13 ) ) @ ( B @ in ) )
| ~ ( A @ union @ ( B @ in ) ) ),
inference(simp,[status(thm)],[269]) ).
thf(72,axiom,
! [A: $i,B: $i] :
( ( ( B @ ( A @ set_difference ) )
= empty_set )
<=> ( B @ ( A @ subset ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l32_xboole_1) ).
thf(529,plain,
! [A: $i,B: $i] :
( ( ( B @ ( A @ subset ) )
=> ( ( B @ ( A @ set_difference ) )
= empty_set ) )
& ( ( ( B @ ( A @ set_difference ) )
= empty_set )
=> ( B @ ( A @ subset ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(41564,plain,
( ( ( sk6 @ singleton @ ( sk6 @ ( empty_set @ sk11 ) @ in ) )
!= ( sk6 @ ( sk6 @ ( empty_set @ sk11 ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[31083,40130]) ).
thf(41565,plain,
( ( sk6 @ singleton @ ( sk6 @ ( empty_set @ sk11 ) @ in ) )
!= ( sk6 @ ( sk6 @ ( empty_set @ sk11 ) @ in ) ) ),
inference(simp,[status(thm)],[41564]) ).
thf(41747,plain,
( ( ( sk6 @ singleton )
!= sk6 )
| ( ( sk6 @ ( empty_set @ sk11 ) )
!= ( sk6 @ ( empty_set @ sk11 ) ) ) ),
inference(simp,[status(thm)],[41565]) ).
thf(41762,plain,
( ( sk6 @ singleton )
!= sk6 ),
inference(simp,[status(thm)],[41747]) ).
thf(13879,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk6 @ singleton ) )
| ( B
!= ( empty_set @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,13730]) ).
thf(13880,plain,
! [A: $i] :
( ( A
!= ( empty_set @ singleton ) )
| ~ ( sk6 @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[13879:[bind(A,$thf( sk6 @ singleton )),bind(B,$thf( B ))]]) ).
thf(13917,plain,
~ ( sk6 @ singleton @ singleton @ ( empty_set @ singleton @ in ) ),
inference(simp,[status(thm)],[13880]) ).
thf(217,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ set_union2 ) )
= ( A @ ( B @ set_union2 ) ) ),
inference(cnf,[status(esa)],[216]) ).
thf(218,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ set_union2 ) )
= ( A @ ( B @ set_union2 ) ) ),
inference(lifteq,[status(thm)],[217]) ).
thf(10228,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ set_union2 ) )
!= ( C @ ( sk6 @ set_union2 ) ) )
| ( ( B @ ( A @ set_union2 ) )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[218,1522]) ).
thf(10229,plain,
! [A: $i] :
( ( sk6 @ ( A @ set_union2 ) )
!= empty_set ),
inference(pattern_uni,[status(thm)],[10228:[bind(A,$thf( A )),bind(B,$thf( sk6 )),bind(C,$thf( A ))]]) ).
thf(37771,plain,
! [B: $i,A: $i] :
( ( A
!= ( empty_set @ union @ union ) )
| ( B != sk6 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,37692]) ).
thf(37772,plain,
! [A: $i] :
( ( A != sk6 )
| ~ ( empty_set @ union @ union @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[37771:[bind(A,$thf( empty_set @ union @ union )),bind(B,$thf( B ))]]) ).
thf(37872,plain,
~ ( empty_set @ union @ union @ singleton @ ( sk6 @ in ) ),
inference(simp,[status(thm)],[37772]) ).
thf(30,axiom,
! [A: $i] :
( ( empty_set @ ( A @ set_intersection2 ) )
= empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_boole) ).
thf(190,plain,
! [A: $i] :
( ( empty_set @ ( A @ set_intersection2 ) )
= empty_set ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(191,plain,
! [A: $i] :
( ( empty_set @ ( A @ set_intersection2 ) )
= empty_set ),
inference(cnf,[status(esa)],[190]) ).
thf(192,plain,
! [A: $i] :
( ( empty_set @ ( A @ set_intersection2 ) )
= empty_set ),
inference(lifteq,[status(thm)],[191]) ).
thf(2599,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ unordered_pair ) ) )
| ( empty_set != empty_set )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[113,1832]) ).
thf(2600,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ unordered_pair ) ) )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[2599]) ).
thf(2601,plain,
! [B: $i,A: $i] :
~ ( empty_set @ ( B @ ( A @ unordered_pair ) @ subset ) ),
inference(pattern_uni,[status(thm)],[2600:[bind(A,$thf( E @ ( D @ unordered_pair ) )),bind(B,$thf( E )),bind(C,$thf( D ))]]) ).
thf(2606,plain,
! [B: $i,A: $i] :
~ ( empty_set @ ( B @ ( A @ unordered_pair ) @ subset ) ),
inference(simp,[status(thm)],[2601]) ).
thf(701,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( B != empty_set )
| ( sk3 != empty_set )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[102,651]) ).
thf(702,plain,
! [A: $i] :
( ( A != empty_set )
| ( sk3 != empty_set )
| ~ ( A @ empty )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[701:[bind(A,$thf( sk1 ))]]) ).
thf(988,plain,
( ( sk3 != empty_set )
| ~ ( empty_set @ empty )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[702]) ).
thf(1179,plain,
( ( sk3 != empty_set )
| ~ $true
| ~ ( sk1 @ empty ) ),
inference(rewrite,[status(thm)],[988,134]) ).
thf(1180,plain,
( ( sk3 != empty_set )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[1179]) ).
thf(1368,plain,
! [A: $i] :
( ( A != sk3 )
| ( empty_set != empty_set )
| ~ ( sk1 @ empty )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[113,1180]) ).
thf(1369,plain,
! [A: $i] :
( ( A != sk3 )
| ~ ( sk1 @ empty )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[1368]) ).
thf(1370,plain,
( ~ ( sk1 @ empty )
| ~ ( empty_set @ ( sk3 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[1369:[bind(A,$thf( sk3 ))]]) ).
thf(15,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ set_intersection2 ) )
= ( A @ ( B @ set_intersection2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
thf(135,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ set_intersection2 ) )
= ( A @ ( B @ set_intersection2 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(136,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ set_intersection2 ) )
= ( A @ ( B @ set_intersection2 ) ) ),
inference(cnf,[status(esa)],[135]) ).
thf(137,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ set_intersection2 ) )
= ( A @ ( B @ set_intersection2 ) ) ),
inference(lifteq,[status(thm)],[136]) ).
thf(88,plain,
( ( ( sk4 @ singleton @ ( sk3 @ set_difference ) )
!= sk3 )
| ( ( sk2 @ singleton @ ( sk1 @ set_difference ) )
= sk1 ) ),
inference(cnfConj,[status(thm)],[86]) ).
thf(92,plain,
( ( ( sk4 @ singleton @ ( sk3 @ set_difference ) )
!= sk3 )
| ( ( sk2 @ singleton @ ( sk1 @ set_difference ) )
= sk1 ) ),
inference(lifteq,[status(thm)],[88]) ).
thf(224,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ singleton ) )
| ~ ( B @ ( A @ ( B @ sk10 ) @ in ) )
| ( ( A @ ( B @ sk9 ) )
!= A ) ),
inference(cnfConj,[status(thm)],[221]) ).
thf(228,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk10 ) @ in ) )
| ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk9 ) )
!= A ) ),
inference(lifteq,[status(thm)],[224]) ).
thf(229,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk10 ) @ in ) )
| ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk9 ) )
!= A ) ),
inference(simp,[status(thm)],[228]) ).
thf(248,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( B @ ( A @ ( B @ sk12 ) @ in ) )
| ~ ( B @ ( A @ ( B @ sk11 ) @ in ) ) ),
inference(cnfConj,[status(thm)],[245]) ).
thf(252,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ sk12 ) @ in ) )
| ~ ( B @ ( A @ ( B @ sk11 ) @ in ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[248]) ).
thf(2797,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ set_intersection2 ) )
!= ( D @ ( C @ set_intersection2 ) ) )
| ( C @ ( A @ ( B @ set_intersection2 ) @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[137,215]) ).
thf(2798,plain,
! [B: $i,A: $i] : ( A @ ( A @ ( B @ set_intersection2 ) @ subset ) ),
inference(pattern_uni,[status(thm)],[2797:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(3749,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ set_intersection2 ) )
!= ( C @ ( D @ set_intersection2 ) ) )
| ( C @ ( A @ ( B @ set_intersection2 ) @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[137,2798]) ).
thf(3750,plain,
! [B: $i,A: $i] : ( B @ ( A @ ( B @ set_intersection2 ) @ subset ) ),
inference(pattern_uni,[status(thm)],[3749:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(12885,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ singleton ) )
| ( B != empty_set )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,414]) ).
thf(12886,plain,
! [B: $i,A: $i] :
( ( A != empty_set )
| ~ ( B @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[12885:[bind(A,$thf( D @ singleton )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(13411,plain,
! [A: $i] :
~ ( A @ singleton @ singleton @ ( empty_set @ in ) ),
inference(simp,[status(thm)],[12886]) ).
thf(9936,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ set_union2 ) @ proper_subset ) )
!= ( empty_set @ singleton @ ( empty_set @ proper_subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9901,1519]) ).
thf(9937,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ set_union2 ) @ proper_subset ) )
!= ( empty_set @ singleton @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[9936]) ).
thf(9988,plain,
! [B: $i,A: $i] :
( ( A
!= ( empty_set @ singleton ) )
| ( ( B @ ( A @ set_union2 ) )
!= empty_set ) ),
inference(simp,[status(thm)],[9937]) ).
thf(9991,plain,
! [A: $i] :
( ( A @ ( empty_set @ singleton @ set_union2 ) )
!= empty_set ),
inference(simp,[status(thm)],[9988]) ).
thf(10807,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ set_union2 ) )
!= ( C @ ( empty_set @ singleton @ set_union2 ) ) )
| ( ( B @ ( A @ set_union2 ) )
!= empty_set ) ),
inference(paramod_ordered,[status(thm)],[218,9991]) ).
thf(10808,plain,
! [A: $i] :
( ( empty_set @ singleton @ ( A @ set_union2 ) )
!= empty_set ),
inference(pattern_uni,[status(thm)],[10807:[bind(A,$thf( A )),bind(B,$thf( empty_set @ singleton )),bind(C,$thf( A ))]]) ).
thf(39633,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( A @ ( B @ in ) )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[648,282]) ).
thf(39634,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( A @ ( B @ in ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[39633]) ).
thf(39635,plain,
( ~ ( sk2 @ ( sk1 @ in ) )
| ( sk3 != empty_set ) ),
inference(pattern_uni,[status(thm)],[39634:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 ))]]) ).
thf(4,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ proper_subset ) )
=> ~ ( A @ ( B @ proper_subset ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_xboole_0) ).
thf(97,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ proper_subset ) )
=> ~ ( A @ ( B @ proper_subset ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(2566,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ set_intersection2 ) @ subset ) )
!= ( empty_set @ ( C @ ( sk6 @ set_union2 ) @ subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[215,1746]) ).
thf(2567,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( A @ set_intersection2 ) @ subset ) )
!= ( empty_set @ ( C @ ( sk6 @ set_union2 ) @ subset ) ) ),
inference(simp,[status(thm)],[2566]) ).
thf(2570,plain,
! [C: $i,B: $i,A: $i] :
( ( A != empty_set )
| ( ( B @ ( A @ set_intersection2 ) )
!= ( C @ ( sk6 @ set_union2 ) ) ) ),
inference(simp,[status(thm)],[2567]) ).
thf(2578,plain,
! [B: $i,A: $i] :
( ( A @ ( empty_set @ set_intersection2 ) )
!= ( B @ ( sk6 @ set_union2 ) ) ),
inference(simp,[status(thm)],[2570]) ).
thf(3141,plain,
! [A: $i] :
( ( A @ ( sk6 @ set_union2 ) )
!= empty_set ),
inference(rewrite,[status(thm)],[2578,1613]) ).
thf(4475,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( sk6 @ set_union2 ) ) )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[154,3141]) ).
thf(4476,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( sk6 @ set_union2 ) ) )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[4475]) ).
thf(4477,plain,
! [A: $i] :
~ ( A @ ( sk6 @ set_union2 ) @ empty ),
inference(pattern_uni,[status(thm)],[4476:[bind(A,$thf( D @ ( sk6 @ set_union2 ) )),bind(B,$thf( D ))]]) ).
thf(4719,plain,
! [A: $i] :
~ ( A @ ( sk6 @ set_union2 ) @ empty ),
inference(simp,[status(thm)],[4477]) ).
thf(10368,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ set_union2 ) )
!= ( C @ ( sk6 @ set_union2 ) ) )
| ~ ( B @ ( A @ set_union2 ) @ empty ) ),
inference(paramod_ordered,[status(thm)],[218,4719]) ).
thf(10369,plain,
! [A: $i] :
~ ( sk6 @ ( A @ set_union2 ) @ empty ),
inference(pattern_uni,[status(thm)],[10368:[bind(A,$thf( A )),bind(B,$thf( sk6 )),bind(C,$thf( A ))]]) ).
thf(44,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
=> ( B
= ( A @ ( B @ set_difference ) @ ( A @ set_union2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t45_xboole_1) ).
thf(283,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
=> ( B
= ( A @ ( B @ set_difference ) @ ( A @ set_union2 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(284,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ ( B @ set_difference ) @ ( A @ set_union2 ) ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnf,[status(esa)],[283]) ).
thf(285,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ subset ) )
| ( ( A @ ( B @ set_difference ) @ ( A @ set_union2 ) )
= B ) ),
inference(lifteq,[status(thm)],[284]) ).
thf(200,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ disjoint ) )
| ( ( B @ ( A @ set_intersection2 ) )
!= empty_set ) ),
inference(cnfConj,[status(thm)],[198]) ).
thf(202,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ disjoint ) )
| ( ( B @ ( A @ set_intersection2 ) )
!= empty_set ) ),
inference(lifteq,[status(thm)],[200]) ).
thf(203,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ disjoint ) )
| ( ( B @ ( A @ set_intersection2 ) )
!= empty_set ) ),
inference(simp,[status(thm)],[202]) ).
thf(9093,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( empty_set @ set_intersection2 ) )
!= ( C @ ( B @ set_intersection2 ) ) )
| ( C @ ( B @ disjoint ) )
| ( empty_set != empty_set ) ),
inference(paramod_ordered,[status(thm)],[1613,203]) ).
thf(9094,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( empty_set @ set_intersection2 ) )
!= ( C @ ( B @ set_intersection2 ) ) )
| ( C @ ( B @ disjoint ) ) ),
inference(simp,[status(thm)],[9093]) ).
thf(9095,plain,
! [A: $i] : ( A @ ( empty_set @ disjoint ) ),
inference(pattern_uni,[status(thm)],[9094:[bind(A,$thf( A )),bind(B,$thf( empty_set )),bind(C,$thf( A ))]]) ).
thf(6333,plain,
! [A: $i] :
( ( A != sk1 )
| ( empty_set != empty_set )
| ~ ( sk3 @ empty )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,1104]) ).
thf(6334,plain,
! [A: $i] :
( ( A != sk1 )
| ~ ( sk3 @ empty )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6333]) ).
thf(6335,plain,
( ~ ( sk3 @ empty )
| ( sk1 @ ( empty_set @ proper_subset ) ) ),
inference(pattern_uni,[status(thm)],[6334:[bind(A,$thf( sk1 ))]]) ).
thf(41852,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk6 @ singleton ) )
| ( B != sk6 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,41762]) ).
thf(41853,plain,
! [A: $i] :
( ( A != sk6 )
| ~ ( sk6 @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[41852:[bind(A,$thf( sk6 @ singleton )),bind(B,$thf( B ))]]) ).
thf(41924,plain,
~ ( sk6 @ singleton @ singleton @ ( sk6 @ in ) ),
inference(simp,[status(thm)],[41853]) ).
thf(80,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ unordered_pair ) @ subset ) )
<=> ( ( C @ ( B @ in ) )
& ( C @ ( A @ in ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t38_zfmisc_1) ).
thf(593,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ( C @ ( B @ in ) )
& ( C @ ( A @ in ) ) )
=> ( C @ ( B @ ( A @ unordered_pair ) @ subset ) ) )
& ( ( C @ ( B @ ( A @ unordered_pair ) @ subset ) )
=> ( ( C @ ( B @ in ) )
& ( C @ ( A @ in ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(2978,plain,
( ( ( sk3 @ empty )
!= ( sk1 @ empty ) )
| ~ ( sk1 @ empty ) ),
inference(simp,[status(thm)],[2973]) ).
thf(9058,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( ( sk3 @ empty )
!= ( sk1 @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[134,2978]) ).
thf(9059,plain,
( ( ( sk1 @ empty )
!= ( empty_set @ empty ) )
| ( ( sk3 @ empty )
!= ( sk1 @ empty ) ) ),
inference(simp,[status(thm)],[9058]) ).
thf(9079,plain,
( ( sk1 != empty_set )
| ( ( sk3 @ empty )
!= ( sk1 @ empty ) ) ),
inference(simp,[status(thm)],[9059]) ).
thf(21502,plain,
( ( sk1 @ empty )
| ( sk3 @ empty )
| ( sk1 != empty_set ) ),
inference(bool_ext,[status(thm)],[9079]) ).
thf(39369,plain,
( ( ( sk3 @ empty )
!= ( sk3 @ empty ) )
| ( sk1 != empty_set )
| ~ $true
| ( sk1 @ empty )
| ( sk1 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[21502,1104]) ).
thf(39370,plain,
( ( ( sk3 @ empty )
!= ( sk3 @ empty ) )
| ( sk1 @ empty )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[39369]) ).
thf(39371,plain,
( ( sk1 @ empty )
| ( sk1 != empty_set ) ),
inference(pattern_uni,[status(thm)],[39370:[]]) ).
thf(40822,plain,
( ( ( sk6 @ empty )
!= ( sk1 @ empty ) )
| ~ $true
| ( sk1 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[39371,121]) ).
thf(40823,plain,
( ( ( sk6 @ empty )
!= ( sk1 @ empty ) )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[40822]) ).
thf(40988,plain,
( ( sk6 != sk1 )
| ( sk1 != empty_set ) ),
inference(simp,[status(thm)],[40823]) ).
thf(17,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( A @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( C @ ( B @ set_intersection2 ) @ ( A @ subset ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t19_xboole_1) ).
thf(140,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( A @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( C @ ( B @ set_intersection2 ) @ ( A @ subset ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(141,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ set_intersection2 ) @ ( A @ subset ) )
| ~ ( C @ ( A @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnf,[status(esa)],[140]) ).
thf(13091,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( sk1 != empty_set )
| ( B != sk1 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,3203]) ).
thf(13092,plain,
! [A: $i] :
( ( sk1 != empty_set )
| ( A != sk1 )
| ~ ( sk3 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[13091:[bind(A,$thf( sk3 ))]]) ).
thf(13504,plain,
( ( sk1 != empty_set )
| ~ ( sk3 @ singleton @ ( sk1 @ in ) ) ),
inference(simp,[status(thm)],[13092]) ).
thf(49,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( A @ singleton )
= ( C @ ( B @ unordered_pair ) ) )
=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_zfmisc_1) ).
thf(339,plain,
! [A: $i,B: $i,C: $i] :
( ( ( A @ singleton )
= ( C @ ( B @ unordered_pair ) ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(71,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ( ( B @ ( A @ singleton @ set_union2 ) )
= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l23_zfmisc_1) ).
thf(526,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ( ( B @ ( A @ singleton @ set_union2 ) )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(68,axiom,
! [A: $i,B: $i,C: $i] :
( ( C
= ( B @ ( A @ set_difference ) ) )
<=> ! [D: $i] :
( ( C @ ( D @ in ) )
<=> ( ~ ( B @ ( D @ in ) )
& ( A @ ( D @ in ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_xboole_0) ).
thf(489,plain,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i] :
( ( ( ~ ( B @ ( D @ in ) )
& ( A @ ( D @ in ) ) )
=> ( C @ ( D @ in ) ) )
& ( ( C @ ( D @ in ) )
=> ( ~ ( B @ ( D @ in ) )
& ( A @ ( D @ in ) ) ) ) )
=> ( C
= ( B @ ( A @ set_difference ) ) ) )
& ( ( C
= ( B @ ( A @ set_difference ) ) )
=> ! [D: $i] :
( ( ( ~ ( B @ ( D @ in ) )
& ( A @ ( D @ in ) ) )
=> ( C @ ( D @ in ) ) )
& ( ( C @ ( D @ in ) )
=> ( ~ ( B @ ( D @ in ) )
& ( A @ ( D @ in ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(1205,plain,
! [A: $i] :
( ( A != sk1 )
| ( empty_set != empty_set )
| ( sk3 != empty_set )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[113,651]) ).
thf(1206,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk3 != empty_set )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[1205]) ).
thf(1207,plain,
( ( sk3 != empty_set )
| ~ ( empty_set @ ( sk1 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[1206:[bind(A,$thf( sk1 ))]]) ).
thf(40028,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk6 @ ( empty_set @ sk11 ) ) )
| ( B != sk6 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,39960]) ).
thf(40029,plain,
! [A: $i] :
( ( A != sk6 )
| ~ ( sk6 @ ( empty_set @ sk11 ) @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[40028:[bind(A,$thf( sk6 @ ( empty_set @ sk11 ) )),bind(B,$thf( B ))]]) ).
thf(40131,plain,
~ ( sk6 @ ( empty_set @ sk11 ) @ singleton @ ( sk6 @ in ) ),
inference(simp,[status(thm)],[40029]) ).
thf(4301,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ singleton ) )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[154,2644]) ).
thf(4302,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ singleton ) )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[4301]) ).
thf(4303,plain,
! [A: $i] :
~ ( A @ singleton @ empty ),
inference(pattern_uni,[status(thm)],[4302:[bind(A,$thf( C @ singleton )),bind(B,$thf( C ))]]) ).
thf(4736,plain,
! [A: $i] :
~ ( A @ singleton @ empty ),
inference(simp,[status(thm)],[4303]) ).
thf(3,axiom,
! [A: $i,B: $i] :
~ ( A @ ( A @ proper_subset ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',irreflexivity_r2_xboole_0) ).
thf(94,plain,
! [A: $i] :
~ ( A @ ( A @ proper_subset ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(95,plain,
~ ? [A: $i] : ( A @ ( A @ proper_subset ) ),
inference(miniscope,[status(thm)],[94]) ).
thf(96,plain,
! [A: $i] :
~ ( A @ ( A @ proper_subset ) ),
inference(cnf,[status(esa)],[95]) ).
thf(31,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ subset ) )
=> ( C @ ( B @ set_intersection2 ) @ ( C @ ( A @ set_intersection2 ) @ subset ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t26_xboole_1) ).
thf(193,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ subset ) )
=> ( C @ ( B @ set_intersection2 ) @ ( C @ ( A @ set_intersection2 ) @ subset ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(73,axiom,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( B @ ( A @ in ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
thf(537,plain,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( B @ ( A @ in ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(32463,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ in ) )
!= ( empty_set @ union @ ( A @ in ) ) )
| ~ $true
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[648,32284]) ).
thf(32464,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ in ) )
!= ( empty_set @ union @ ( A @ in ) ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[32463]) ).
thf(32503,plain,
! [A: $i] :
( ( ( empty_set @ union )
!= sk1 )
| ( sk2 != A )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[32464]) ).
thf(32559,plain,
( ( ( empty_set @ union )
!= sk1 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[32503]) ).
thf(14313,plain,
! [B: $i,A: $i] :
( ( A
!= ( empty_set @ singleton @ singleton ) )
| ( B
!= ( empty_set @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,14065]) ).
thf(14314,plain,
! [A: $i] :
( ( A
!= ( empty_set @ singleton ) )
| ~ ( empty_set @ singleton @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[14313:[bind(A,$thf( empty_set @ singleton @ singleton )),bind(B,$thf( B ))]]) ).
thf(14369,plain,
~ ( empty_set @ singleton @ singleton @ singleton @ ( empty_set @ singleton @ in ) ),
inference(simp,[status(thm)],[14314]) ).
thf(13748,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) @ ( B @ in ) )
!= ( sk6 @ singleton @ ( empty_set @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[316,13437]) ).
thf(13749,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( B @ in ) )
!= ( sk6 @ singleton @ ( empty_set @ in ) ) ),
inference(simp,[status(thm)],[13748]) ).
thf(13830,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( sk6 @ singleton ) )
| ( B != empty_set ) ),
inference(simp,[status(thm)],[13749]) ).
thf(13839,plain,
! [A: $i] :
( ( empty_set @ ( A @ unordered_pair ) )
!= ( sk6 @ singleton ) ),
inference(simp,[status(thm)],[13830]) ).
thf(12214,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ( A != empty_set )
| ( sk3 != empty_set )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,651]) ).
thf(12215,plain,
! [A: $i] :
( ( A != empty_set )
| ( sk3 != empty_set )
| ~ ( A @ singleton @ ( sk1 @ in ) ) ),
inference(pattern_uni,[status(thm)],[12214:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(13594,plain,
( ( sk3 != empty_set )
| ~ ( empty_set @ singleton @ ( sk1 @ in ) ) ),
inference(simp,[status(thm)],[12215]) ).
thf(9110,plain,
! [C: $i,B: $i,A: $i] :
( ( ( empty_set @ ( A @ set_intersection2 ) )
!= ( C @ ( B @ set_intersection2 ) ) )
| ( C @ ( B @ disjoint ) )
| ( empty_set != empty_set ) ),
inference(paramod_ordered,[status(thm)],[192,203]) ).
thf(9111,plain,
! [C: $i,B: $i,A: $i] :
( ( ( empty_set @ ( A @ set_intersection2 ) )
!= ( C @ ( B @ set_intersection2 ) ) )
| ( C @ ( B @ disjoint ) ) ),
inference(simp,[status(thm)],[9110]) ).
thf(9112,plain,
! [A: $i] : ( empty_set @ ( A @ disjoint ) ),
inference(pattern_uni,[status(thm)],[9111:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( empty_set ))]]) ).
thf(125,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ( A != B ) ),
inference(cnfConj,[status(thm)],[124]) ).
thf(128,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[125]) ).
thf(129,plain,
! [A: $i] : ( A @ ( A @ subset ) ),
inference(simp,[status(thm)],[128]) ).
thf(13633,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) @ ( B @ in ) )
!= ( empty_set @ singleton @ ( sk6 @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[316,13436]) ).
thf(13634,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( B @ in ) )
!= ( empty_set @ singleton @ ( sk6 @ in ) ) ),
inference(simp,[status(thm)],[13633]) ).
thf(13720,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ singleton ) )
| ( B != sk6 ) ),
inference(simp,[status(thm)],[13634]) ).
thf(13731,plain,
! [A: $i] :
( ( sk6 @ ( A @ unordered_pair ) )
!= ( empty_set @ singleton ) ),
inference(simp,[status(thm)],[13720]) ).
thf(83,axiom,
! [A: $i] :
( ( A @ ( A @ unordered_pair ) )
= ( A @ singleton ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t69_enumset1) ).
thf(605,plain,
! [A: $i] :
( ( A @ ( A @ unordered_pair ) )
= ( A @ singleton ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(2627,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ singleton @ set_union2 ) ) )
| ( empty_set != empty_set )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[113,1521]) ).
thf(2628,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ singleton @ set_union2 ) ) )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[2627]) ).
thf(2629,plain,
! [B: $i,A: $i] :
~ ( empty_set @ ( A @ ( B @ singleton @ set_union2 ) @ subset ) ),
inference(pattern_uni,[status(thm)],[2628:[bind(A,$thf( E @ ( F @ singleton @ set_union2 ) )),bind(B,$thf( E )),bind(C,$thf( F ))]]) ).
thf(2634,plain,
! [B: $i,A: $i] :
~ ( empty_set @ ( A @ ( B @ singleton @ set_union2 ) @ subset ) ),
inference(simp,[status(thm)],[2629]) ).
thf(257,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ union ) )
| ( A @ ( A @ ( B @ sk17 ) @ in ) )
| ( B @ ( A @ sk14 ) ) ),
inference(cnfConj,[status(thm)],[256]) ).
thf(265,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ ( B @ sk17 ) @ in ) )
| ( B @ ( A @ sk14 ) )
| ( B
= ( A @ union ) ) ),
inference(lifteq,[status(thm)],[257]) ).
thf(266,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ ( B @ sk17 ) @ in ) )
| ( B @ ( A @ sk14 ) )
| ( B
= ( A @ union ) ) ),
inference(simp,[status(thm)],[265]) ).
thf(6226,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( sk6 @ set_union2 ) ) )
| ( empty_set != empty_set )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,1522]) ).
thf(6227,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( sk6 @ set_union2 ) ) )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6226]) ).
thf(6228,plain,
! [A: $i] : ( A @ ( sk6 @ set_union2 ) @ ( empty_set @ proper_subset ) ),
inference(pattern_uni,[status(thm)],[6227:[bind(A,$thf( D @ ( sk6 @ set_union2 ) )),bind(B,$thf( D ))]]) ).
thf(6644,plain,
! [A: $i] : ( A @ ( sk6 @ set_union2 ) @ ( empty_set @ proper_subset ) ),
inference(simp,[status(thm)],[6228]) ).
thf(10376,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ set_union2 ) )
!= ( C @ ( sk6 @ set_union2 ) ) )
| ( B @ ( A @ set_union2 ) @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[218,6644]) ).
thf(10377,plain,
! [A: $i] : ( sk6 @ ( A @ set_union2 ) @ ( empty_set @ proper_subset ) ),
inference(pattern_uni,[status(thm)],[10376:[bind(A,$thf( A )),bind(B,$thf( sk6 )),bind(C,$thf( A ))]]) ).
thf(6277,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk1 != empty_set )
| ( empty_set != empty_set )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,651]) ).
thf(6278,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk1 != empty_set )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6277]) ).
thf(6279,plain,
( ( sk1 != empty_set )
| ( sk3 @ ( empty_set @ proper_subset ) ) ),
inference(pattern_uni,[status(thm)],[6278:[bind(A,$thf( sk3 ))]]) ).
thf(6242,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ ( sk6 @ set_union2 ) @ set_union2 ) ) )
| ( empty_set != empty_set )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,2575]) ).
thf(6243,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ ( sk6 @ set_union2 ) @ set_union2 ) ) )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6242]) ).
thf(6244,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( sk6 @ set_union2 ) @ set_union2 ) @ ( empty_set @ proper_subset ) ),
inference(pattern_uni,[status(thm)],[6243:[bind(A,$thf( E @ ( G @ ( sk6 @ set_union2 ) @ set_union2 ) )),bind(B,$thf( E )),bind(C,$thf( G ))]]) ).
thf(6647,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( sk6 @ set_union2 ) @ set_union2 ) @ ( empty_set @ proper_subset ) ),
inference(simp,[status(thm)],[6244]) ).
thf(40395,plain,
( ( ( sk1 @ ( sk2 @ in ) )
!= ( sk2 @ ( sk1 @ in ) ) )
| ~ $true
| ~ ( sk3 @ empty )
| ~ ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[4276,39611]) ).
thf(40396,plain,
( ( ( sk1 @ ( sk2 @ in ) )
!= ( sk2 @ ( sk1 @ in ) ) )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[40395]) ).
thf(40499,plain,
( ( sk2 != sk1 )
| ( sk2 != sk1 )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[40396]) ).
thf(40526,plain,
( ( sk2 != sk1 )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[40499]) ).
thf(50,axiom,
! [A: $i,B: $i,C: $i] :
( ( C
= ( B @ ( A @ set_union2 ) ) )
<=> ! [D: $i] :
( ( C @ ( D @ in ) )
<=> ( ( B @ ( D @ in ) )
| ( A @ ( D @ in ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_xboole_0) ).
thf(343,plain,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i] :
( ( ( ( B @ ( D @ in ) )
| ( A @ ( D @ in ) ) )
=> ( C @ ( D @ in ) ) )
& ( ( C @ ( D @ in ) )
=> ( ( B @ ( D @ in ) )
| ( A @ ( D @ in ) ) ) ) )
=> ( C
= ( B @ ( A @ set_union2 ) ) ) )
& ( ( C
= ( B @ ( A @ set_union2 ) ) )
=> ! [D: $i] :
( ( ( ( B @ ( D @ in ) )
| ( A @ ( D @ in ) ) )
=> ( C @ ( D @ in ) ) )
& ( ( C @ ( D @ in ) )
=> ( ( B @ ( D @ in ) )
| ( A @ ( D @ in ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(4364,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ unordered_pair ) ) )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[154,1832]) ).
thf(4365,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ unordered_pair ) ) )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[4364]) ).
thf(4366,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ unordered_pair ) @ empty ),
inference(pattern_uni,[status(thm)],[4365:[bind(A,$thf( E @ ( D @ unordered_pair ) )),bind(B,$thf( E )),bind(C,$thf( D ))]]) ).
thf(4685,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ unordered_pair ) @ empty ),
inference(simp,[status(thm)],[4366]) ).
thf(12346,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( B != empty_set )
| ~ ( sk3 @ empty )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,1104]) ).
thf(12347,plain,
! [A: $i] :
( ( A != empty_set )
| ~ ( sk3 @ empty )
| ~ ( sk1 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[12346:[bind(A,$thf( sk1 ))]]) ).
thf(13201,plain,
( ~ ( sk3 @ empty )
| ~ ( sk1 @ singleton @ ( empty_set @ in ) ) ),
inference(simp,[status(thm)],[12347]) ).
thf(161,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ~ ( B @ ( A @ proper_subset ) ) ),
inference(cnfConj,[status(thm)],[160]) ).
thf(20,axiom,
! [A: $i,B: $i] :
( ( A @ ( A @ set_intersection2 ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_k3_xboole_0) ).
thf(149,plain,
! [A: $i] :
( ( A @ ( A @ set_intersection2 ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(40800,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk1 @ empty )
| ( empty_set != empty_set )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,39371]) ).
thf(40801,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk1 @ empty )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[40800]) ).
thf(40802,plain,
( ( sk1 @ empty )
| ( sk1 @ ( empty_set @ proper_subset ) ) ),
inference(pattern_uni,[status(thm)],[40801:[bind(A,$thf( sk1 ))]]) ).
thf(19,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
~ ( ( A != D )
& ( A != C )
& ( ( B @ ( A @ unordered_pair ) )
= ( D @ ( C @ unordered_pair ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_zfmisc_1) ).
thf(145,plain,
! [A: $i,B: $i,C: $i,D: $i] :
~ ( ( A != D )
& ( A != C )
& ( ( B @ ( A @ unordered_pair ) )
= ( D @ ( C @ unordered_pair ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(146,plain,
~ ? [A: $i,B: $i,C: $i,D: $i] :
( ( A != D )
& ( A != C )
& ( ( B @ ( A @ unordered_pair ) )
= ( D @ ( C @ unordered_pair ) ) ) ),
inference(miniscope,[status(thm)],[145]) ).
thf(147,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A = D )
| ( A = C )
| ( ( B @ ( A @ unordered_pair ) )
!= ( D @ ( C @ unordered_pair ) ) ) ),
inference(cnf,[status(esa)],[146]) ).
thf(148,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A = D )
| ( A = C )
| ( ( B @ ( A @ unordered_pair ) )
!= ( D @ ( C @ unordered_pair ) ) ) ),
inference(lifteq,[status(thm)],[147]) ).
thf(26,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ disjoint ) )
& ( B @ ( A @ subset ) ) )
=> ( C @ ( A @ disjoint ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_xboole_1) ).
thf(180,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ disjoint ) )
& ( B @ ( A @ subset ) ) )
=> ( C @ ( A @ disjoint ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(78,axiom,
! [A: $i,B: $i] :
( ( B @ ( B @ ( A @ set_union2 ) @ set_difference ) )
= ( B @ ( A @ set_difference ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t40_xboole_1) ).
thf(584,plain,
! [A: $i,B: $i] :
( ( B @ ( B @ ( A @ set_union2 ) @ set_difference ) )
= ( B @ ( A @ set_difference ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(61,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ set_difference ) @ ( A @ set_union2 ) )
= ( B @ ( A @ set_union2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t39_xboole_1) ).
thf(423,plain,
! [A: $i,B: $i] :
( ( A @ ( B @ set_difference ) @ ( A @ set_union2 ) )
= ( B @ ( A @ set_union2 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(7666,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk6 @ set_union2 ) @ ( empty_set @ proper_subset ) )
!= ( B @ ( C @ ( B @ set_union2 ) @ proper_subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6644,1519]) ).
thf(7667,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk6 @ set_union2 ) @ ( empty_set @ proper_subset ) )
!= ( B @ ( C @ ( B @ set_union2 ) @ proper_subset ) ) ),
inference(simp,[status(thm)],[7666]) ).
thf(7714,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk6 @ set_union2 ) )
!= B )
| ( ( C @ ( B @ set_union2 ) )
!= empty_set ) ),
inference(simp,[status(thm)],[7667]) ).
thf(7736,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( sk6 @ set_union2 ) @ set_union2 ) )
!= empty_set ),
inference(simp,[status(thm)],[7714]) ).
thf(117,plain,
! [A: $i] :
( ~ ( A @ empty )
=> ~ ? [B: $i] : ( A @ ( B @ set_union2 ) @ empty ) ),
inference(miniscope,[status(thm)],[116]) ).
thf(118,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ set_union2 ) @ empty )
| ( A @ empty ) ),
inference(cnf,[status(esa)],[117]) ).
thf(19220,plain,
! [B: $i,A: $i] :
( ( A
!= ( empty_set @ singleton @ ( B @ set_union2 ) ) )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[154,10808]) ).
thf(19221,plain,
! [B: $i,A: $i] :
( ( A
!= ( empty_set @ singleton @ ( B @ set_union2 ) ) )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[19220]) ).
thf(19222,plain,
! [A: $i] :
~ ( empty_set @ singleton @ ( A @ set_union2 ) @ empty ),
inference(pattern_uni,[status(thm)],[19221:[bind(A,$thf( empty_set @ singleton @ ( C @ set_union2 ) )),bind(B,$thf( C ))]]) ).
thf(19264,plain,
! [A: $i] :
~ ( empty_set @ singleton @ ( A @ set_union2 ) @ empty ),
inference(simp,[status(thm)],[19222]) ).
thf(41848,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk6 @ singleton ) )
| ( A != sk6 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,41762]) ).
thf(41849,plain,
! [A: $i] :
( ( A != sk6 )
| ~ ( A @ singleton @ ( sk6 @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[41848:[bind(A,$thf( A )),bind(B,$thf( sk6 @ singleton ))]]) ).
thf(41923,plain,
~ ( sk6 @ singleton @ ( sk6 @ singleton @ in ) ),
inference(simp,[status(thm)],[41849]) ).
thf(32418,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ in ) )
!= ( empty_set @ union @ ( A @ in ) ) )
| ~ $true
| ~ ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[4276,32284]) ).
thf(32419,plain,
! [A: $i] :
( ( ( sk1 @ ( sk2 @ in ) )
!= ( empty_set @ union @ ( A @ in ) ) )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[32418]) ).
thf(32500,plain,
! [A: $i] :
( ( ( empty_set @ union )
!= sk1 )
| ( sk2 != A )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[32419]) ).
thf(32556,plain,
( ( ( empty_set @ union )
!= sk1 )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[32500]) ).
thf(76,axiom,
! [A: $i,B: $i] : ( A @ ( B @ ( A @ set_difference ) @ subset ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t36_xboole_1) ).
thf(579,plain,
! [A: $i,B: $i] : ( A @ ( B @ ( A @ set_difference ) @ subset ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(290,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ singleton @ subset ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnfConj,[status(thm)],[288]) ).
thf(291,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ singleton @ subset ) )
| ~ ( B @ ( A @ in ) ) ),
inference(simp,[status(thm)],[290]) ).
thf(143,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ set_intersection2 ) )
= A )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnf,[status(esa)],[142]) ).
thf(144,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ subset ) )
| ( ( B @ ( A @ set_intersection2 ) )
= A ) ),
inference(lifteq,[status(thm)],[143]) ).
thf(6183,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ unordered_pair ) ) )
| ( empty_set != empty_set )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,2744]) ).
thf(6184,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ unordered_pair ) ) )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6183]) ).
thf(6185,plain,
! [B: $i,A: $i] : ( B @ ( A @ unordered_pair ) @ ( empty_set @ proper_subset ) ),
inference(pattern_uni,[status(thm)],[6184:[bind(A,$thf( E @ ( D @ unordered_pair ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(6638,plain,
! [B: $i,A: $i] : ( B @ ( A @ unordered_pair ) @ ( empty_set @ proper_subset ) ),
inference(simp,[status(thm)],[6185]) ).
thf(6634,plain,
! [A: $i] :
( ( A != sk1 )
| ( empty_set != empty_set )
| ~ ( empty_set @ ( sk3 @ subset ) )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,1204]) ).
thf(6635,plain,
! [A: $i] :
( ( A != sk1 )
| ~ ( empty_set @ ( sk3 @ subset ) )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6634]) ).
thf(6636,plain,
( ~ ( empty_set @ ( sk3 @ subset ) )
| ( sk1 @ ( empty_set @ proper_subset ) ) ),
inference(pattern_uni,[status(thm)],[6635:[bind(A,$thf( sk1 ))]]) ).
thf(181,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ disjoint ) )
| ~ ( C @ ( B @ disjoint ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnf,[status(esa)],[180]) ).
thf(6547,plain,
! [A: $i] :
( ( A != sk6 )
| ( empty_set != empty_set )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,613]) ).
thf(6548,plain,
! [A: $i] :
( ( A != sk6 )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6547]) ).
thf(6549,plain,
sk6 @ ( empty_set @ proper_subset ),
inference(pattern_uni,[status(thm)],[6548:[bind(A,$thf( sk6 ))]]) ).
thf(74,axiom,
! [A: $i,B: $i] :
( ~ ( ( B @ ( A @ disjoint ) )
& ? [C: $i] : ( B @ ( A @ set_intersection2 ) @ ( C @ in ) ) )
& ~ ( ! [C: $i] :
~ ( B @ ( A @ set_intersection2 ) @ ( C @ in ) )
& ~ ( B @ ( A @ disjoint ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_xboole_0) ).
thf(540,plain,
! [A: $i,B: $i] :
( ~ ( ( B @ ( A @ disjoint ) )
& ? [C: $i] : ( B @ ( A @ set_intersection2 ) @ ( C @ in ) ) )
& ~ ( ! [C: $i] :
~ ( B @ ( A @ set_intersection2 ) @ ( C @ in ) )
& ~ ( B @ ( A @ disjoint ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(12987,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ( A != empty_set )
| ~ ( sk1 @ empty )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,1180]) ).
thf(12988,plain,
! [A: $i] :
( ( A != empty_set )
| ~ ( sk1 @ empty )
| ~ ( A @ singleton @ ( sk3 @ in ) ) ),
inference(pattern_uni,[status(thm)],[12987:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(13459,plain,
( ~ ( sk1 @ empty )
| ~ ( empty_set @ singleton @ ( sk3 @ in ) ) ),
inference(simp,[status(thm)],[12988]) ).
thf(13089,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ( A != empty_set )
| ( sk3 != sk1 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,3203]) ).
thf(13090,plain,
! [A: $i] :
( ( A != empty_set )
| ( sk3 != sk1 )
| ~ ( A @ singleton @ ( sk1 @ in ) ) ),
inference(pattern_uni,[status(thm)],[13089:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(13503,plain,
( ( sk3 != sk1 )
| ~ ( empty_set @ singleton @ ( sk1 @ in ) ) ),
inference(simp,[status(thm)],[13090]) ).
thf(29,axiom,
! [A: $i,B: $i] :
~ ( B @ ( A @ ordered_pair ) @ empty ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
thf(187,plain,
! [A: $i,B: $i] :
~ ( B @ ( A @ ordered_pair ) @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(6570,plain,
! [A: $i] :
( ( A != sk3 )
| ( empty_set != empty_set )
| ~ ( sk1 @ empty )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,1180]) ).
thf(6571,plain,
! [A: $i] :
( ( A != sk3 )
| ~ ( sk1 @ empty )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6570]) ).
thf(6572,plain,
( ~ ( sk1 @ empty )
| ( sk3 @ ( empty_set @ proper_subset ) ) ),
inference(pattern_uni,[status(thm)],[6571:[bind(A,$thf( sk3 ))]]) ).
thf(32393,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( empty_set @ union @ ( B @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[233,32284]) ).
thf(32394,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( empty_set @ union @ ( B @ in ) ) ),
inference(simp,[status(thm)],[32393]) ).
thf(32504,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton )
!= ( empty_set @ union ) )
| ( A != B ) ),
inference(simp,[status(thm)],[32394]) ).
thf(32560,plain,
! [A: $i] :
( ( A @ singleton )
!= ( empty_set @ union ) ),
inference(simp,[status(thm)],[32504]) ).
thf(98,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ proper_subset ) )
| ~ ( B @ ( A @ proper_subset ) ) ),
inference(cnf,[status(esa)],[97]) ).
thf(34,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( C @ ( A @ subset ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_xboole_1) ).
thf(207,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( C @ ( A @ subset ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(208,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ subset ) )
| ~ ( C @ ( B @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnf,[status(esa)],[207]) ).
thf(55,axiom,
! [A: $i,B: $i] :
( ~ ( ( B @ ( A @ disjoint ) )
& ? [C: $i] :
( ( B @ ( C @ in ) )
& ( A @ ( C @ in ) ) ) )
& ~ ( ! [C: $i] :
~ ( ( B @ ( C @ in ) )
& ( A @ ( C @ in ) ) )
& ~ ( B @ ( A @ disjoint ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_xboole_0) ).
thf(387,plain,
! [A: $i,B: $i] :
( ~ ( ( B @ ( A @ disjoint ) )
& ? [C: $i] :
( ( B @ ( C @ in ) )
& ( A @ ( C @ in ) ) ) )
& ~ ( ! [C: $i] :
~ ( ( B @ ( C @ in ) )
& ( A @ ( C @ in ) ) )
& ~ ( B @ ( A @ disjoint ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(34967,plain,
! [B: $i,A: $i] :
( ( A
!= ( empty_set @ union @ singleton ) )
| ( B
!= ( sk6 @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,32950]) ).
thf(34968,plain,
! [A: $i] :
( ( A
!= ( sk6 @ singleton ) )
| ~ ( empty_set @ union @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[34967:[bind(A,$thf( empty_set @ union @ singleton )),bind(B,$thf( B ))]]) ).
thf(35059,plain,
~ ( empty_set @ union @ singleton @ singleton @ ( sk6 @ singleton @ in ) ),
inference(simp,[status(thm)],[34968]) ).
thf(212,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ set_union2 ) )
= B )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnf,[status(esa)],[211]) ).
thf(213,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ subset ) )
| ( ( B @ ( A @ set_union2 ) )
= B ) ),
inference(lifteq,[status(thm)],[212]) ).
thf(87,plain,
( ~ ( sk3 @ ( sk4 @ in ) )
| ( ( sk2 @ singleton @ ( sk1 @ set_difference ) )
= sk1 ) ),
inference(cnfConj,[status(thm)],[86]) ).
thf(91,plain,
( ~ ( sk3 @ ( sk4 @ in ) )
| ( ( sk2 @ singleton @ ( sk1 @ set_difference ) )
= sk1 ) ),
inference(lifteq,[status(thm)],[87]) ).
thf(6427,plain,
! [A: $i] :
( ( A != sk3 )
| ( empty_set != empty_set )
| ~ ( empty_set @ ( sk1 @ subset ) )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,1207]) ).
thf(6428,plain,
! [A: $i] :
( ( A != sk3 )
| ~ ( empty_set @ ( sk1 @ subset ) )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6427]) ).
thf(6429,plain,
( ~ ( empty_set @ ( sk1 @ subset ) )
| ( sk3 @ ( empty_set @ proper_subset ) ) ),
inference(pattern_uni,[status(thm)],[6428:[bind(A,$thf( sk3 ))]]) ).
thf(65,axiom,
! [A: $i,B: $i] :
( ( B
= ( A @ powerset ) )
<=> ! [C: $i] :
( ( B @ ( C @ in ) )
<=> ( A @ ( C @ subset ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_zfmisc_1) ).
thf(462,plain,
! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( ( A @ ( C @ subset ) )
=> ( B @ ( C @ in ) ) )
& ( ( B @ ( C @ in ) )
=> ( A @ ( C @ subset ) ) ) )
=> ( B
= ( A @ powerset ) ) )
& ( ( B
= ( A @ powerset ) )
=> ! [C: $i] :
( ( ( A @ ( C @ subset ) )
=> ( B @ ( C @ in ) ) )
& ( ( B @ ( C @ in ) )
=> ( A @ ( C @ subset ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(40,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_tarski) ).
thf(240,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)],[40]) ).
thf(247,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( A @ ( B @ sk12 ) @ in ) )
| ( A @ ( A @ ( B @ sk11 ) @ in ) ) ),
inference(cnfConj,[status(thm)],[245]) ).
thf(251,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( A @ ( B @ sk12 ) @ in ) )
| ( A @ ( A @ ( B @ sk11 ) @ in ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[247]) ).
thf(42274,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk6 != sk1 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[154,40988]) ).
thf(42275,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk6 != sk1 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[42274]) ).
thf(42276,plain,
( ( sk6 != sk1 )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[42275:[bind(A,$thf( sk1 ))]]) ).
thf(12212,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ( sk1 != empty_set )
| ( A != empty_set )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,651]) ).
thf(12213,plain,
! [A: $i] :
( ( sk1 != empty_set )
| ( A != empty_set )
| ~ ( A @ singleton @ ( sk3 @ in ) ) ),
inference(pattern_uni,[status(thm)],[12212:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(13593,plain,
( ( sk1 != empty_set )
| ~ ( empty_set @ singleton @ ( sk3 @ in ) ) ),
inference(simp,[status(thm)],[12213]) ).
thf(258,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ union ) )
| ~ ( B @ ( A @ ( B @ sk16 ) @ in ) )
| ( B @ ( A @ sk14 ) ) ),
inference(cnfConj,[status(thm)],[256]) ).
thf(277,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk16 ) @ in ) )
| ( B @ ( A @ sk14 ) )
| ( B
= ( A @ union ) ) ),
inference(lifteq,[status(thm)],[258]) ).
thf(278,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk16 ) @ in ) )
| ( B @ ( A @ sk14 ) )
| ( B
= ( A @ union ) ) ),
inference(simp,[status(thm)],[277]) ).
thf(56,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ subset ) )
=> ( C @ ( B @ set_difference ) @ ( C @ ( A @ set_difference ) @ subset ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t33_xboole_1) ).
thf(394,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ subset ) )
=> ( C @ ( B @ set_difference ) @ ( C @ ( A @ set_difference ) @ subset ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(1248,plain,
! [A: $i] :
( ( A != sk3 )
| ( empty_set != empty_set )
| ( sk1 @ ( sk2 @ in ) )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[113,648]) ).
thf(1249,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk1 @ ( sk2 @ in ) )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[1248]) ).
thf(1250,plain,
( ( sk1 @ ( sk2 @ in ) )
| ~ ( empty_set @ ( sk3 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[1249:[bind(A,$thf( sk3 ))]]) ).
thf(6734,plain,
! [A: $i] :
( ( A != sk1 )
| ( empty_set != empty_set )
| ( sk3 @ ( empty_set @ proper_subset ) )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,6279]) ).
thf(6735,plain,
! [A: $i] :
( ( A != sk1 )
| ( sk3 @ ( empty_set @ proper_subset ) )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6734]) ).
thf(6736,plain,
( ( sk3 @ ( empty_set @ proper_subset ) )
| ( sk1 @ ( empty_set @ proper_subset ) ) ),
inference(pattern_uni,[status(thm)],[6735:[bind(A,$thf( sk1 ))]]) ).
thf(62,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ cartesian_product2 ) @ ( B @ ( A @ ordered_pair ) @ in ) )
<=> ( ( D @ ( B @ in ) )
& ( C @ ( A @ in ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l55_zfmisc_1) ).
thf(426,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( ( D @ ( B @ in ) )
& ( C @ ( A @ in ) ) )
=> ( D @ ( C @ cartesian_product2 ) @ ( B @ ( A @ ordered_pair ) @ in ) ) )
& ( ( D @ ( C @ cartesian_product2 ) @ ( B @ ( A @ ordered_pair ) @ in ) )
=> ( ( D @ ( B @ in ) )
& ( C @ ( A @ in ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(6274,plain,
! [A: $i] :
( ( A != sk1 )
| ( empty_set != empty_set )
| ( ( sk4 @ singleton )
!= sk3 )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,3878]) ).
thf(6275,plain,
! [A: $i] :
( ( A != sk1 )
| ( ( sk4 @ singleton )
!= sk3 )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6274]) ).
thf(6276,plain,
( ( ( sk4 @ singleton )
!= sk3 )
| ( sk1 @ ( empty_set @ proper_subset ) ) ),
inference(pattern_uni,[status(thm)],[6275:[bind(A,$thf( sk1 ))]]) ).
thf(3979,plain,
! [A: $i] :
( ( A != sk1 )
| ( empty_set != empty_set )
| ( ( sk4 @ singleton )
!= sk3 )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[113,3878]) ).
thf(3980,plain,
! [A: $i] :
( ( A != sk1 )
| ( ( sk4 @ singleton )
!= sk3 )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[3979]) ).
thf(3981,plain,
( ( ( sk4 @ singleton )
!= sk3 )
| ~ ( empty_set @ ( sk1 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[3980:[bind(A,$thf( sk1 ))]]) ).
thf(69,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ( B @ union @ ( A @ subset ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l50_zfmisc_1) ).
thf(516,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ( B @ union @ ( A @ subset ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(6336,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ singleton @ set_union2 ) ) )
| ( empty_set != empty_set )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,1521]) ).
thf(6337,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ singleton @ set_union2 ) ) )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6336]) ).
thf(6338,plain,
! [B: $i,A: $i] : ( A @ ( B @ singleton @ set_union2 ) @ ( empty_set @ proper_subset ) ),
inference(pattern_uni,[status(thm)],[6337:[bind(A,$thf( E @ ( F @ singleton @ set_union2 ) )),bind(B,$thf( E )),bind(C,$thf( F ))]]) ).
thf(6664,plain,
! [B: $i,A: $i] : ( A @ ( B @ singleton @ set_union2 ) @ ( empty_set @ proper_subset ) ),
inference(simp,[status(thm)],[6338]) ).
thf(35,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( C @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( B @ ( C @ ( A @ set_union2 ) @ subset ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_xboole_1) ).
thf(209,plain,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( C @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( B @ ( C @ ( A @ set_union2 ) @ subset ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(580,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ set_difference ) @ subset ) ),
inference(cnf,[status(esa)],[579]) ).
thf(13822,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) @ ( A @ in ) )
!= ( sk6 @ singleton @ ( empty_set @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[304,13437]) ).
thf(13823,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( A @ in ) )
!= ( sk6 @ singleton @ ( empty_set @ in ) ) ),
inference(simp,[status(thm)],[13822]) ).
thf(13836,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( sk6 @ singleton ) )
| ( A != empty_set ) ),
inference(simp,[status(thm)],[13823]) ).
thf(13843,plain,
! [A: $i] :
( ( A @ ( empty_set @ unordered_pair ) )
!= ( sk6 @ singleton ) ),
inference(simp,[status(thm)],[13836]) ).
thf(51,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
<=> ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( B @ ( C @ in ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
thf(370,plain,
! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( B @ ( C @ in ) ) )
=> ( B @ ( A @ subset ) ) )
& ( ( B @ ( A @ subset ) )
=> ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( B @ ( C @ in ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(4349,plain,
! [A: $i] :
( ( A != sk1 )
| ( empty_set != empty_set )
| ( ( sk4 @ singleton )
!= sk3 )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[154,3878]) ).
thf(4350,plain,
! [A: $i] :
( ( A != sk1 )
| ( ( sk4 @ singleton )
!= sk3 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[4349]) ).
thf(4351,plain,
( ( ( sk4 @ singleton )
!= sk3 )
| ~ ( sk1 @ empty ) ),
inference(pattern_uni,[status(thm)],[4350:[bind(A,$thf( sk1 ))]]) ).
thf(4312,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ ( sk6 @ set_union2 ) @ set_union2 ) ) )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[154,2575]) ).
thf(4313,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ ( sk6 @ set_union2 ) @ set_union2 ) ) )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[4312]) ).
thf(4314,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ ( sk6 @ set_union2 ) @ set_union2 ) @ empty ),
inference(pattern_uni,[status(thm)],[4313:[bind(A,$thf( E @ ( G @ ( sk6 @ set_union2 ) @ set_union2 ) )),bind(B,$thf( E )),bind(C,$thf( G ))]]) ).
thf(4737,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ ( sk6 @ set_union2 ) @ set_union2 ) @ empty ),
inference(simp,[status(thm)],[4314]) ).
thf(12991,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( B != empty_set )
| ~ ( sk1 @ empty )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,1180]) ).
thf(12992,plain,
! [A: $i] :
( ( A != empty_set )
| ~ ( sk1 @ empty )
| ~ ( sk3 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[12991:[bind(A,$thf( sk3 ))]]) ).
thf(13461,plain,
( ~ ( sk1 @ empty )
| ~ ( sk3 @ singleton @ ( empty_set @ in ) ) ),
inference(simp,[status(thm)],[12992]) ).
thf(13707,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) @ ( A @ in ) )
!= ( empty_set @ singleton @ ( sk6 @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[304,13436]) ).
thf(13708,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( A @ in ) )
!= ( empty_set @ singleton @ ( sk6 @ in ) ) ),
inference(simp,[status(thm)],[13707]) ).
thf(13718,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( empty_set @ singleton ) )
| ( A != sk6 ) ),
inference(simp,[status(thm)],[13708]) ).
thf(13729,plain,
! [A: $i] :
( ( A @ ( sk6 @ unordered_pair ) )
!= ( empty_set @ singleton ) ),
inference(simp,[status(thm)],[13718]) ).
thf(385,plain,
! [A: $i] :
( ( empty_set @ ( A @ set_difference ) )
= A ),
inference(cnf,[status(esa)],[384]) ).
thf(386,plain,
! [A: $i] :
( ( empty_set @ ( A @ set_difference ) )
= A ),
inference(lifteq,[status(thm)],[385]) ).
thf(41978,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk6 @ singleton @ ( sk6 @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[233,41923]) ).
thf(41979,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk6 @ singleton @ ( sk6 @ singleton @ in ) ) ),
inference(simp,[status(thm)],[41978]) ).
thf(42146,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk6 @ singleton ) )
| ( A
!= ( sk6 @ singleton ) ) ),
inference(simp,[status(thm)],[41979]) ).
thf(42184,plain,
( ( sk6 @ singleton @ singleton )
!= ( sk6 @ singleton ) ),
inference(simp,[status(thm)],[42146]) ).
thf(12216,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( sk1 != empty_set )
| ( B != empty_set )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,651]) ).
thf(12217,plain,
! [A: $i] :
( ( sk1 != empty_set )
| ( A != empty_set )
| ~ ( sk3 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[12216:[bind(A,$thf( sk3 ))]]) ).
thf(13595,plain,
( ( sk1 != empty_set )
| ~ ( sk3 @ singleton @ ( empty_set @ in ) ) ),
inference(simp,[status(thm)],[12217]) ).
thf(10240,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ set_union2 ) )
!= ( C @ ( sk6 @ set_union2 ) ) )
| ~ ( empty_set @ ( B @ ( A @ set_union2 ) @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[218,1746]) ).
thf(10241,plain,
! [A: $i] :
~ ( empty_set @ ( sk6 @ ( A @ set_union2 ) @ subset ) ),
inference(pattern_uni,[status(thm)],[10240:[bind(A,$thf( A )),bind(B,$thf( sk6 )),bind(C,$thf( A ))]]) ).
thf(77,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ subset ) )
=> ( ( C @ singleton @ ( B @ set_difference ) @ ( A @ subset ) )
| ( A @ ( C @ in ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l3_zfmisc_1) ).
thf(581,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ subset ) )
=> ( ( C @ singleton @ ( B @ set_difference ) @ ( A @ subset ) )
| ( A @ ( C @ in ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(2911,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ ( sk6 @ set_union2 ) @ set_union2 ) ) )
| ( empty_set != empty_set )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[113,2575]) ).
thf(2912,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ ( sk6 @ set_union2 ) @ set_union2 ) ) )
| ~ ( empty_set @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[2911]) ).
thf(2913,plain,
! [B: $i,A: $i] :
~ ( empty_set @ ( A @ ( B @ ( sk6 @ set_union2 ) @ set_union2 ) @ subset ) ),
inference(pattern_uni,[status(thm)],[2912:[bind(A,$thf( E @ ( G @ ( sk6 @ set_union2 ) @ set_union2 ) )),bind(B,$thf( E )),bind(C,$thf( G ))]]) ).
thf(2919,plain,
! [B: $i,A: $i] :
~ ( empty_set @ ( A @ ( B @ ( sk6 @ set_union2 ) @ set_union2 ) @ subset ) ),
inference(simp,[status(thm)],[2913]) ).
thf(225,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk10 ) )
= A )
| ( ( A @ ( B @ sk9 ) )
!= A ) ),
inference(cnfConj,[status(thm)],[221]) ).
thf(230,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk10 ) )
= A )
| ( ( A @ ( B @ sk9 ) )
!= A ) ),
inference(lifteq,[status(thm)],[225]) ).
thf(231,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk10 ) )
= A )
| ( ( A @ ( B @ sk9 ) )
!= A ) ),
inference(simp,[status(thm)],[230]) ).
thf(47,axiom,
! [A: $i,B: $i] :
( ( B @ singleton @ ( A @ subset ) )
<=> ( ( A
= ( B @ singleton ) )
| ( A = empty_set ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t39_zfmisc_1) ).
thf(319,plain,
! [A: $i,B: $i] :
( ( ( ( A
= ( B @ singleton ) )
| ( A = empty_set ) )
=> ( B @ singleton @ ( A @ subset ) ) )
& ( ( B @ singleton @ ( A @ subset ) )
=> ( ( A
= ( B @ singleton ) )
| ( A = empty_set ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(185,plain,
! [A: $i] :
( ~ ( A @ empty )
=> ~ ? [B: $i] : ( B @ ( A @ set_union2 ) @ empty ) ),
inference(miniscope,[status(thm)],[184]) ).
thf(186,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ set_union2 ) @ empty )
| ( A @ empty ) ),
inference(cnf,[status(esa)],[185]) ).
thf(139,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ disjoint ) )
| ~ ( B @ ( A @ disjoint ) ) ),
inference(cnf,[status(esa)],[138]) ).
thf(639,plain,
! [A: $i] :
( ( ( A @ ( empty_set @ set_difference ) )
!= ( sk4 @ singleton @ ( sk3 @ set_difference ) ) )
| ( sk3 != empty_set )
| ( ( sk2 @ singleton @ ( sk1 @ set_difference ) )
= sk1 ) ),
inference(paramod_ordered,[status(thm)],[485,92]) ).
thf(647,plain,
! [A: $i] :
( ( A
!= ( sk4 @ singleton ) )
| ( sk3 != empty_set )
| ( sk3 != empty_set )
| ( ( sk2 @ singleton @ ( sk1 @ set_difference ) )
= sk1 ) ),
inference(simp,[status(thm)],[639]) ).
thf(652,plain,
( ( sk3 != empty_set )
| ( ( sk2 @ singleton @ ( sk1 @ set_difference ) )
= sk1 ) ),
inference(simp,[status(thm)],[647]) ).
thf(13087,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ( sk1 != empty_set )
| ( A != sk1 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,3203]) ).
thf(13088,plain,
! [A: $i] :
( ( sk1 != empty_set )
| ( A != sk1 )
| ~ ( A @ singleton @ ( sk3 @ in ) ) ),
inference(pattern_uni,[status(thm)],[13087:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(13502,plain,
( ( sk1 != empty_set )
| ~ ( sk1 @ singleton @ ( sk3 @ in ) ) ),
inference(simp,[status(thm)],[13088]) ).
thf(226,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ singleton ) )
| ~ ( B @ ( A @ ( B @ sk10 ) @ in ) )
| ( B @ ( A @ ( B @ sk9 ) @ in ) ) ),
inference(cnfConj,[status(thm)],[221]) ).
thf(234,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk10 ) @ in ) )
| ( B @ ( A @ ( B @ sk9 ) @ in ) )
| ( B
= ( A @ singleton ) ) ),
inference(lifteq,[status(thm)],[226]) ).
thf(235,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk10 ) @ in ) )
| ( B @ ( A @ ( B @ sk9 ) @ in ) )
| ( B
= ( A @ singleton ) ) ),
inference(simp,[status(thm)],[234]) ).
thf(63,axiom,
! [A: $i,B: $i,C: $i] :
( ( C
= ( B @ ( A @ set_intersection2 ) ) )
<=> ! [D: $i] :
( ( C @ ( D @ in ) )
<=> ( ( B @ ( D @ in ) )
& ( A @ ( D @ in ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_xboole_0) ).
thf(433,plain,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i] :
( ( ( ( B @ ( D @ in ) )
& ( A @ ( D @ in ) ) )
=> ( C @ ( D @ in ) ) )
& ( ( C @ ( D @ in ) )
=> ( ( B @ ( D @ in ) )
& ( A @ ( D @ in ) ) ) ) )
=> ( C
= ( B @ ( A @ set_intersection2 ) ) ) )
& ( ( C
= ( B @ ( A @ set_intersection2 ) ) )
=> ! [D: $i] :
( ( ( ( B @ ( D @ in ) )
& ( A @ ( D @ in ) ) )
=> ( C @ ( D @ in ) ) )
& ( ( C @ ( D @ in ) )
=> ( ( B @ ( D @ in ) )
& ( A @ ( D @ in ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(23582,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( empty_set @ singleton @ ( B @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[233,13410]) ).
thf(23583,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( empty_set @ singleton @ ( B @ singleton @ in ) ) ),
inference(simp,[status(thm)],[23582]) ).
thf(23701,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton )
!= ( empty_set @ singleton ) )
| ( A
!= ( B @ singleton ) ) ),
inference(simp,[status(thm)],[23583]) ).
thf(23718,plain,
! [A: $i] :
( ( A @ singleton @ singleton )
!= ( empty_set @ singleton ) ),
inference(simp,[status(thm)],[23701]) ).
thf(264,plain,
! [C: $i,B: $i,A: $i] :
( ( B
= ( A @ union ) )
| ~ ( B @ ( A @ sk14 ) )
| ~ ( A @ ( C @ in ) )
| ~ ( C @ ( A @ ( B @ sk15 ) @ in ) ) ),
inference(cnfConj,[status(thm)],[256]) ).
thf(271,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ sk14 ) )
| ~ ( A @ ( C @ in ) )
| ~ ( C @ ( A @ ( B @ sk15 ) @ in ) )
| ( B
= ( A @ union ) ) ),
inference(lifteq,[status(thm)],[264]) ).
thf(272,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ sk14 ) )
| ~ ( A @ ( C @ in ) )
| ~ ( C @ ( A @ ( B @ sk15 ) @ in ) )
| ( B
= ( A @ union ) ) ),
inference(simp,[status(thm)],[271]) ).
thf(6196,plain,
! [A: $i] :
( ( A != sk3 )
| ( empty_set != empty_set )
| ( sk1 @ ( sk2 @ in ) )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,648]) ).
thf(6197,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk1 @ ( sk2 @ in ) )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6196]) ).
thf(6198,plain,
( ( sk1 @ ( sk2 @ in ) )
| ( sk3 @ ( empty_set @ proper_subset ) ) ),
inference(pattern_uni,[status(thm)],[6197:[bind(A,$thf( sk3 ))]]) ).
thf(52,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ( ( B @ ( A @ singleton @ set_union2 ) )
= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t46_zfmisc_1) ).
thf(378,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ( ( B @ ( A @ singleton @ set_union2 ) )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(150,plain,
! [A: $i] :
( ( A @ ( A @ set_intersection2 ) )
= A ),
inference(cnf,[status(esa)],[149]) ).
thf(151,plain,
! [A: $i] :
( ( A @ ( A @ set_intersection2 ) )
= A ),
inference(lifteq,[status(thm)],[150]) ).
thf(24,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( A @ ordered_pair ) )
= ( D @ ( C @ ordered_pair ) ) )
=> ( ( B = D )
& ( A = C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t33_zfmisc_1) ).
thf(168,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( A @ ordered_pair ) )
= ( D @ ( C @ ordered_pair ) ) )
=> ( ( B = D )
& ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(12326,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ( A != sk1 )
| ~ ( sk1 @ empty )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,2979]) ).
thf(12327,plain,
! [A: $i] :
( ( A != sk1 )
| ~ ( sk1 @ empty )
| ~ ( A @ singleton @ ( sk3 @ in ) ) ),
inference(pattern_uni,[status(thm)],[12326:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(13192,plain,
( ~ ( sk1 @ empty )
| ~ ( sk1 @ singleton @ ( sk3 @ in ) ) ),
inference(simp,[status(thm)],[12327]) ).
thf(31090,plain,
! [A: $i] :
( ( A
!= ( sk6 @ ( empty_set @ sk11 ) ) )
| ( sk6 @ ( empty_set @ in ) )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,31083]) ).
thf(31091,plain,
( ( sk6 @ ( empty_set @ in ) )
| ( sk6 @ ( empty_set @ sk11 ) @ ( empty_set @ proper_subset ) ) ),
inference(pattern_uni,[status(thm)],[31090:[bind(A,$thf( sk6 @ ( empty_set @ sk11 ) ))]]) ).
thf(40586,plain,
( ( ( sk3 @ empty )
!= ( empty_set @ empty ) )
| ( sk2 != sk1 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[134,40526]) ).
thf(40587,plain,
( ( ( sk3 @ empty )
!= ( empty_set @ empty ) )
| ( sk2 != sk1 ) ),
inference(simp,[status(thm)],[40586]) ).
thf(40638,plain,
( ( sk3 != empty_set )
| ( sk2 != sk1 ) ),
inference(simp,[status(thm)],[40587]) ).
thf(40358,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk2 @ ( sk1 @ in ) ) )
| ~ $true
| ~ ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[233,39611]) ).
thf(40359,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk2 @ ( sk1 @ in ) ) )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[40358]) ).
thf(40488,plain,
! [A: $i] :
( ( ( A @ singleton )
!= sk2 )
| ( A != sk1 )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[40359]) ).
thf(40514,plain,
( ( ( sk1 @ singleton )
!= sk2 )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[40488]) ).
thf(210,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ set_union2 ) @ subset ) )
| ~ ( B @ ( C @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnf,[status(esa)],[209]) ).
thf(261,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ union ) )
| ( A @ ( B @ sk17 ) @ ( A @ ( B @ sk16 ) @ in ) )
| ( B @ ( A @ sk14 ) ) ),
inference(cnfConj,[status(thm)],[256]) ).
thf(267,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk17 ) @ ( A @ ( B @ sk16 ) @ in ) )
| ( B @ ( A @ sk14 ) )
| ( B
= ( A @ union ) ) ),
inference(lifteq,[status(thm)],[261]) ).
thf(268,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ sk17 ) @ ( A @ ( B @ sk16 ) @ in ) )
| ( B @ ( A @ sk14 ) )
| ( B
= ( A @ union ) ) ),
inference(simp,[status(thm)],[267]) ).
thf(194,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
=> ! [C: $i] : ( C @ ( B @ set_intersection2 ) @ ( C @ ( A @ set_intersection2 ) @ subset ) ) ),
inference(miniscope,[status(thm)],[193]) ).
thf(195,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ set_intersection2 ) @ ( C @ ( A @ set_intersection2 ) @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnf,[status(esa)],[194]) ).
thf(58,axiom,
! [A: $i,B: $i] :
( ( B @ singleton @ ( A @ subset ) )
<=> ( ( A
= ( B @ singleton ) )
| ( A = empty_set ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l4_zfmisc_1) ).
thf(400,plain,
! [A: $i,B: $i] :
( ( ( ( A
= ( B @ singleton ) )
| ( A = empty_set ) )
=> ( B @ singleton @ ( A @ subset ) ) )
& ( ( B @ singleton @ ( A @ subset ) )
=> ( ( A
= ( B @ singleton ) )
| ( A = empty_set ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(39737,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk6 @ ( empty_set @ sk11 ) @ ( sk6 @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[233,39599]) ).
thf(39738,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk6 @ ( empty_set @ sk11 ) @ ( sk6 @ in ) ) ),
inference(simp,[status(thm)],[39737]) ).
thf(39906,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk6 @ ( empty_set @ sk11 ) ) )
| ( A != sk6 ) ),
inference(simp,[status(thm)],[39738]) ).
thf(39954,plain,
( ( sk6 @ ( empty_set @ sk11 ) )
!= ( sk6 @ singleton ) ),
inference(simp,[status(thm)],[39906]) ).
thf(12330,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( B != sk1 )
| ~ ( sk1 @ empty )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,2979]) ).
thf(12331,plain,
! [A: $i] :
( ( A != sk1 )
| ~ ( sk1 @ empty )
| ~ ( sk3 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[12330:[bind(A,$thf( sk3 ))]]) ).
thf(13194,plain,
( ~ ( sk1 @ empty )
| ~ ( sk3 @ singleton @ ( sk1 @ in ) ) ),
inference(simp,[status(thm)],[12331]) ).
thf(60,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ disjoint ) )
<=> ( ( B @ ( A @ set_difference ) )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t83_xboole_1) ).
thf(415,plain,
! [A: $i,B: $i] :
( ( ( ( B @ ( A @ set_difference ) )
= A )
=> ( B @ ( A @ disjoint ) ) )
& ( ( B @ ( A @ disjoint ) )
=> ( ( B @ ( A @ set_difference ) )
= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(2799,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ set_intersection2 ) )
!= ( D @ ( C @ set_intersection2 ) ) )
| ( C @ ( B @ ( A @ set_intersection2 ) @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[137,215]) ).
thf(2800,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( A @ set_intersection2 ) @ subset ) ),
inference(pattern_uni,[status(thm)],[2799:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(222,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk10 ) )
= A )
| ( B @ ( A @ ( B @ sk9 ) @ in ) ) ),
inference(cnfConj,[status(thm)],[221]) ).
thf(238,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ sk9 ) @ in ) )
| ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk10 ) )
= A ) ),
inference(lifteq,[status(thm)],[222]) ).
thf(239,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ sk9 ) @ in ) )
| ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk10 ) )
= A ) ),
inference(simp,[status(thm)],[238]) ).
thf(241,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) ) ),
inference(cnf,[status(esa)],[240]) ).
thf(242,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) ) ),
inference(lifteq,[status(thm)],[241]) ).
thf(6593,plain,
! [A: $i] :
( ( A != sk3 )
| ( empty_set != empty_set )
| ( ( sk2 @ singleton @ ( sk1 @ set_difference ) )
= sk1 )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(paramod_ordered,[status(thm)],[5820,652]) ).
thf(6594,plain,
! [A: $i] :
( ( A != sk3 )
| ( ( sk2 @ singleton @ ( sk1 @ set_difference ) )
= sk1 )
| ( A @ ( empty_set @ proper_subset ) ) ),
inference(simp,[status(thm)],[6593]) ).
thf(6595,plain,
( ( ( sk2 @ singleton @ ( sk1 @ set_difference ) )
= sk1 )
| ( sk3 @ ( empty_set @ proper_subset ) ) ),
inference(pattern_uni,[status(thm)],[6594:[bind(A,$thf( sk3 ))]]) ).
thf(25,axiom,
! [A: $i,B: $i] : ( A @ ( A @ subset ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
thf(178,plain,
! [A: $i] : ( A @ ( A @ subset ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(606,plain,
! [A: $i] :
( ( A @ ( A @ unordered_pair ) )
= ( A @ singleton ) ),
inference(cnf,[status(esa)],[605]) ).
thf(607,plain,
! [A: $i] :
( ( A @ ( A @ unordered_pair ) )
= ( A @ singleton ) ),
inference(lifteq,[status(thm)],[606]) ).
thf(67,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( A @ singleton )
= ( C @ ( B @ unordered_pair ) ) )
=> ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t9_zfmisc_1) ).
thf(486,plain,
! [A: $i,B: $i,C: $i] :
( ( ( A @ singleton )
= ( C @ ( B @ unordered_pair ) ) )
=> ( B = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(13093,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( B != empty_set )
| ( sk3 != sk1 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[237,3203]) ).
thf(13094,plain,
! [A: $i] :
( ( A != empty_set )
| ( sk3 != sk1 )
| ~ ( sk1 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[13093:[bind(A,$thf( sk1 ))]]) ).
thf(13505,plain,
( ( sk3 != sk1 )
| ~ ( sk1 @ singleton @ ( empty_set @ in ) ) ),
inference(simp,[status(thm)],[13094]) ).
thf(73557,plain,
$false,
inference(e,[status(thm)],[13199,39611,2744,138,13410,518,5820,276,32950,13437,2940,115,1522,2644,9901,3285,37871,4623,384,1310,142,13596,16784,2575,1746,1613,1359,651,3878,14871,1409,32687,9989,184,110,587,35682,1832,196,460,157,6611,40130,93,152,289,316,216,485,121,84,211,253,397,280,7381,2979,411,1104,1521,206,1564,602,38667,89,133,116,243,292,233,546,201,381,6282,4700,270,529,41762,102,31083,13917,1519,10229,37872,192,2606,1370,137,92,6646,229,252,3750,13411,10808,39635,97,10369,285,9095,6335,41924,593,40988,141,13504,2798,3141,4276,339,526,489,1207,40131,2978,4736,96,193,537,32559,14369,13839,13594,9112,129,39599,13731,32532,605,134,2634,266,10377,6279,6647,40526,343,237,105,13436,4685,13201,161,149,40802,601,32686,148,35058,180,584,423,7736,286,118,19264,41923,32556,579,291,281,204,13730,144,6638,6636,181,6549,540,13459,13503,187,6572,113,219,274,32560,1048,98,208,387,631,35059,140,213,91,483,6429,155,462,103,9079,240,251,330,108,42276,13593,32563,278,394,135,1250,167,6736,14599,39960,426,6276,3981,516,6664,145,648,209,580,282,414,13916,13843,9991,182,370,4351,4737,13461,336,13729,613,154,600,386,42184,13595,10241,99,1180,203,581,218,2919,250,231,37692,319,304,186,114,139,158,652,13502,14368,235,433,207,23718,272,6198,214,119,378,151,14065,168,13192,31091,190,40638,39371,3203,4719,32284,40514,183,210,268,195,6644,400,39954,13194,94,283,415,2800,107,239,242,1129,6595,178,607,111,254,486,13505,122,215,1204]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU162+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.14/0.60 % Computer : n004.cluster.edu
% 0.14/0.60 % Model : x86_64 x86_64
% 0.14/0.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.60 % Memory : 8046.5625MB
% 0.14/0.60 % OS : Linux 6.8.0-71-generic
% 0.14/0.60 % CPULimit : 300
% 0.14/0.60 % WCLimit : 300
% 0.14/0.60 % DateTime : Sat Sep 26 08:42:37 UTC 2026
% 0.14/0.61 % CPUTime :
% 0.14/0.61 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.90/1.19 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.41/1.44 % [INFO] Parsing done (248ms).
% 1.41/1.46 % [INFO] Running in sequential loop mode.
% 2.38/1.86 % [INFO] eprover registered as external prover.
% 2.38/1.87 % [INFO] Scanning for conjecture ...
% 2.61/1.99 % [INFO] Found a conjecture (or negated_conjecture) and 91 axioms. Running axiom selection ...
% 2.82/2.08 % [INFO] Axiom selection finished. Selected 81 axioms (removed 10 axioms).
% 3.07/2.19 % [INFO] Problem is first-order (TPTP FOF).
% 3.24/2.21 % [INFO] Type checking passed.
% 3.24/2.21 % [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 ...
% 99.74/24.88 % External prover 'e' found a proof!
% 99.74/24.88 % [INFO] Killing All external provers ...
% 99.74/24.89 % Time passed: 24137ms (effective reasoning time: 23421ms)
% 99.74/24.89 % 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)>
% 99.74/24.89 % Axioms used in derivation (81): t2_boole, t9_zfmisc_1, l2_zfmisc_1, t19_xboole_1, t17_xboole_1, fc1_zfmisc_1, d1_tarski, idempotence_k3_xboole_0, t1_boole, t3_xboole_1, fc1_xboole_0, d5_tarski, t37_xboole_1, commutativity_k3_xboole_0, d2_tarski, fc2_xboole_0, d1_xboole_0, l50_zfmisc_1, t46_zfmisc_1, t6_boole, t1_xboole_1, commutativity_k2_xboole_0, t4_xboole_0, l25_zfmisc_1, t1_zfmisc_1, d8_xboole_0, t2_tarski, t33_xboole_1, l32_xboole_1, t8_zfmisc_1, t4_boole, fc3_xboole_0, d2_xboole_0, d4_tarski, t7_boole, t33_zfmisc_1, t48_xboole_1, d7_xboole_0, t83_xboole_1, l28_zfmisc_1, l4_zfmisc_1, antisymmetry_r2_xboole_0, d2_zfmisc_1, l3_zfmisc_1, commutativity_k2_tarski, d1_zfmisc_1, t69_enumset1, t38_zfmisc_1, l55_zfmisc_1, t26_xboole_1, t63_xboole_1, t8_xboole_1, t28_xboole_1, d3_tarski, t39_zfmisc_1, reflexivity_r1_tarski, t6_zfmisc_1, t2_xboole_1, d4_xboole_0, t36_xboole_1, l23_zfmisc_1, t8_boole, rc1_xboole_0, t12_xboole_1, t10_zfmisc_1, t37_zfmisc_1, symmetry_r1_xboole_0, idempotence_k2_xboole_0, d10_xboole_0, t7_xboole_1, t60_xboole_1, t3_xboole_0, t3_boole, rc2_xboole_0, t45_xboole_1, t40_xboole_1, l1_zfmisc_1, irreflexivity_r2_xboole_0, d3_xboole_0, t39_xboole_1, antisymmetry_r2_hidden
% 99.74/24.89 % No. of inferences in proof: 840
% 99.74/24.89 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 24137 ms resp. 23421 ms w/o parsing
% 102.48/25.30 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 102.48/25.31 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------