%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEU170+1 : 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 : n017.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:53 AM UTC 2026
% Result : Theorem 81.95s 19.67s
% Output : Refutation 83.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 35
% Syntax : Number of formulae : 533 ( 171 unt; 0 typ; 12 def)
% Number of atoms : 1505 ( 542 equ; 0 cnn)
% Maximal formula atoms : 26 ( 2 avg)
% Number of connectives : 5922 ( 647 ~; 556 |; 72 &;4581 @)
% ( 5 <=>; 61 =>; 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 : 25 ( 22 usr; 8 con; 0-3 aty)
% Number of variables : 735 ( 13 ^; 687 !; 23 ?; 735 :)
% ( 0 !>; 0 ?*; 0 @-; 12 @+)
% Comments :
%------------------------------------------------------------------------------
thf(element_decl,type,
element: $i > $i > $o ).
thf(powerset_decl,type,
powerset: $i > $i ).
thf(disjoint_decl,type,
disjoint: $i > $i > $o ).
thf(subset_decl,type,
subset: $i > $i > $o ).
thf(subset_complement_decl,type,
subset_complement: $i > $i > $i ).
thf(empty_decl,type,
empty: $i > $o ).
thf(empty_set_decl,type,
empty_set: $i ).
thf(set_difference_decl,type,
set_difference: $i > $i > $i ).
thf(in_decl,type,
in: $i > $i > $o ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk5_decl,type,
sk5: $i ).
thf(sk6_decl,type,
sk6: $i > $i > $i > $o ).
thf(sk7_decl,type,
sk7: $i > $i > $i > $i ).
thf(sk8_decl,type,
sk8: $i > $i > $i > $i ).
thf(sk9_decl,type,
sk9: $i > $i ).
thf(sk10_decl,type,
sk10: $i > $i > $i ).
thf(sk11_decl,type,
sk11: $i > $i > $i ).
thf(sk12_decl,type,
sk12: $i > $i ).
thf(sk13_decl,type,
sk13: $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i] :
( ( A @ powerset @ ( B @ element ) )
=> ! [C: $i] :
( ( A @ powerset @ ( C @ element ) )
=> ( ( ( C @ ( A @ subset_complement ) @ ( B @ subset ) )
=> ( C @ ( B @ disjoint ) ) )
& ( ( C @ ( B @ disjoint ) )
=> ( C @ ( A @ subset_complement ) @ ( B @ subset ) ) ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ( ( sk1 @ powerset @ ( A @ element ) )
=> ! [B: $i] :
( ( sk1 @ powerset @ ( B @ element ) )
=> ( ( ( B @ ( sk1 @ subset_complement ) @ ( A @ subset ) )
=> ( B @ ( A @ disjoint ) ) )
& ( ( B @ ( A @ disjoint ) )
=> ( B @ ( sk1 @ subset_complement ) @ ( A @ subset ) ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ( sk1 @ powerset @ ( A @ element ) )
=> ( ( ( A @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) )
=> ( A @ ( sk2 @ disjoint ) ) )
& ( ( A @ ( sk2 @ disjoint ) )
=> ( A @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] : ( A @ empty ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: $i] :
~ ( A @ empty ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
~ ( ( A @ ( D @ in ) )
=> ( ~ ( B @ ( D @ in ) )
& ( C @ ( D @ in ) ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
~ ( ( ~ ( B @ ( D @ in ) )
& ( C @ ( D @ in ) ) )
=> ( A @ ( D @ in ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( ^ [A: $i] :
@+[B: $i] :
( ~ ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( B @ ( C @ in ) )
=> ( A @ ( C @ in ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
( ( A @ ( C @ in ) )
& ( B @ ( C @ in ) ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( ^ [A: $i] :
@+[B: $i] :
( ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( ^ [A: $i] :
@+[B: $i] : ( A @ ( B @ element ) ) ) ) ).
thf(1,conjecture,
! [A: $i,B: $i] :
( ( A @ powerset @ ( B @ element ) )
=> ! [C: $i] :
( ( A @ powerset @ ( C @ element ) )
=> ( ( C @ ( B @ disjoint ) )
<=> ( C @ ( A @ subset_complement ) @ ( B @ subset ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t43_subset_1) ).
thf(2,negated_conjecture,
~ ! [A: $i,B: $i] :
( ( A @ powerset @ ( B @ element ) )
=> ! [C: $i] :
( ( A @ powerset @ ( C @ element ) )
=> ( ( C @ ( B @ disjoint ) )
<=> ( C @ ( A @ subset_complement ) @ ( B @ subset ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(25,plain,
~ ! [A: $i,B: $i] :
( ( A @ powerset @ ( B @ element ) )
=> ! [C: $i] :
( ( A @ powerset @ ( C @ element ) )
=> ( ( ( C @ ( A @ subset_complement ) @ ( B @ subset ) )
=> ( C @ ( B @ disjoint ) ) )
& ( ( C @ ( B @ disjoint ) )
=> ( C @ ( A @ subset_complement ) @ ( B @ subset ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(26,plain,
( ( ~ ( sk3 @ ( sk2 @ disjoint ) )
| ~ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) ) )
& ( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) )
| ~ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) ) )
& ( ~ ( sk3 @ ( sk2 @ disjoint ) )
| ( sk3 @ ( sk2 @ disjoint ) ) )
& ( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) )
| ( sk3 @ ( sk2 @ disjoint ) ) )
& ( sk1 @ powerset @ ( sk3 @ element ) )
& ( sk1 @ powerset @ ( sk2 @ element ) ) ),
inference(cnf,[status(esa)],[25]) ).
thf(28,plain,
sk1 @ powerset @ ( sk2 @ element ),
inference(cnfConj,[status(thm)],[26]) ).
thf(20,axiom,
! [A: $i,B: $i] :
( ( A @ powerset @ ( B @ element ) )
=> ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',involutiveness_k3_subset_1) ).
thf(112,plain,
! [A: $i,B: $i] :
( ( A @ powerset @ ( B @ element ) )
=> ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(113,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B )
| ~ ( A @ powerset @ ( B @ element ) ) ),
inference(cnf,[status(esa)],[112]) ).
thf(114,plain,
! [B: $i,A: $i] :
( ~ ( A @ powerset @ ( B @ element ) )
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(lifteq,[status(thm)],[113]) ).
thf(10523,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[28,114]) ).
thf(10524,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(simp,[status(thm)],[10523]) ).
thf(10525,plain,
( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
= sk2 ),
inference(pattern_uni,[status(thm)],[10524:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(12,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(57,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)],[12]) ).
thf(58,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ! [D: $i] :
( ( ~ ( B @ ( D @ in ) )
& ( A @ ( D @ in ) ) )
=> ( C @ ( D @ in ) ) )
& ! [D: $i] :
( ( C @ ( D @ in ) )
=> ( ~ ( B @ ( D @ in ) )
& ( A @ ( D @ in ) ) ) ) )
=> ( C
= ( B @ ( A @ set_difference ) ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( C
= ( B @ ( A @ set_difference ) ) )
=> ( ! [D: $i] :
( ( ~ ( B @ ( D @ in ) )
& ( A @ ( D @ in ) ) )
=> ( C @ ( D @ in ) ) )
& ! [D: $i] :
( ( C @ ( D @ in ) )
=> ( ~ ( B @ ( D @ in ) )
& ( A @ ( D @ in ) ) ) ) ) ) ),
inference(miniscope,[status(thm)],[57]) ).
thf(59,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( H
= ( G @ ( F @ set_difference ) ) )
| ~ ( H @ ( F @ ( G @ ( H @ sk8 ) ) @ in ) )
| ( H @ ( G @ ( F @ sk6 ) ) ) )
& ( ( H
= ( G @ ( F @ set_difference ) ) )
| ~ ( G @ ( F @ ( G @ ( H @ sk8 ) ) @ in ) )
| ( H @ ( G @ ( F @ sk6 ) ) ) )
& ( ( H
= ( G @ ( F @ set_difference ) ) )
| ( F @ ( F @ ( G @ ( H @ sk8 ) ) @ in ) )
| ( H @ ( G @ ( F @ sk6 ) ) ) )
& ( ( H
= ( G @ ( F @ set_difference ) ) )
| ~ ( H @ ( G @ ( F @ sk6 ) ) )
| ( G @ ( F @ ( G @ ( H @ sk7 ) ) @ in ) )
| ~ ( F @ ( F @ ( G @ ( H @ sk7 ) ) @ in ) ) )
& ( ( H
= ( G @ ( F @ set_difference ) ) )
| ~ ( H @ ( G @ ( F @ sk6 ) ) )
| ( H @ ( F @ ( G @ ( H @ sk7 ) ) @ in ) ) )
& ( ( C @ ( E @ in ) )
| ( B @ ( E @ in ) )
| ~ ( A @ ( E @ in ) )
| ( C
!= ( B @ ( A @ set_difference ) ) ) )
& ( ~ ( B @ ( D @ in ) )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ set_difference ) ) ) )
& ( ( A @ ( D @ in ) )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ set_difference ) ) ) ) ),
inference(cnf,[status(esa)],[58]) ).
thf(61,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( B @ ( A @ set_difference ) ) )
| ( A @ ( A @ ( B @ ( C @ sk8 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk6 ) ) ) ),
inference(cnfConj,[status(thm)],[59]) ).
thf(68,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( A @ ( B @ ( C @ sk8 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk6 ) ) )
| ( C
= ( B @ ( A @ set_difference ) ) ) ),
inference(lifteq,[status(thm)],[61]) ).
thf(69,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( A @ ( B @ ( C @ sk8 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk6 ) ) )
| ( C
= ( B @ ( A @ set_difference ) ) ) ),
inference(simp,[status(thm)],[68]) ).
thf(14,axiom,
! [A: $i,B: $i] :
( ( A @ powerset @ ( B @ element ) )
=> ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_subset_1) ).
thf(88,plain,
! [A: $i,B: $i] :
( ( A @ powerset @ ( B @ element ) )
=> ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(89,plain,
! [B: $i,A: $i] :
( ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ ( A @ powerset @ ( B @ element ) ) ),
inference(cnf,[status(esa)],[88]) ).
thf(3592,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[28,89]) ).
thf(3593,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[3592]) ).
thf(3594,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[3593:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(3702,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3594,89]) ).
thf(3703,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[3702]) ).
thf(3704,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[3703:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) ))]]) ).
thf(3860,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3704,89]) ).
thf(3861,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[3860]) ).
thf(3862,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[3861:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(10551,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[3862,114]) ).
thf(10552,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(simp,[status(thm)],[10551]) ).
thf(10553,plain,
( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
= ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[10552:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(15526,plain,
( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
= ( sk2 @ ( sk1 @ subset_complement ) ) ),
inference(rewrite,[status(thm)],[10553,10525]) ).
thf(21,axiom,
! [A: $i] :
? [B: $i] :
( ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_subset_1) ).
thf(115,plain,
! [A: $i] :
? [B: $i] :
( ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(4078,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3862,89]) ).
thf(4079,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[4078]) ).
thf(4080,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[4079:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(4463,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4080,89]) ).
thf(4464,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[4463]) ).
thf(4465,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[4464:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(5269,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4465,89]) ).
thf(5270,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[5269]) ).
thf(5271,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[5270:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(5985,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5271,89]) ).
thf(5986,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[5985]) ).
thf(5987,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[5986:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(6449,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5987,89]) ).
thf(6450,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[6449]) ).
thf(6451,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[6450:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(10857,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[6451,10525]) ).
thf(14753,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[10857,10525]) ).
thf(23,axiom,
! [A: $i,B: $i] :
( ( A @ powerset @ ( B @ element ) )
=> ( ( B @ ( A @ subset_complement ) )
= ( B @ ( A @ set_difference ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_subset_1) ).
thf(121,plain,
! [A: $i,B: $i] :
( ( A @ powerset @ ( B @ element ) )
=> ( ( B @ ( A @ subset_complement ) )
= ( B @ ( A @ set_difference ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(122,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subset_complement ) )
= ( B @ ( A @ set_difference ) ) )
| ~ ( A @ powerset @ ( B @ element ) ) ),
inference(cnf,[status(esa)],[121]) ).
thf(123,plain,
! [B: $i,A: $i] :
( ~ ( A @ powerset @ ( B @ element ) )
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(lifteq,[status(thm)],[122]) ).
thf(14860,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(paramod_ordered,[status(thm)],[14753,123]) ).
thf(14861,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(simp,[status(thm)],[14860]) ).
thf(14862,plain,
( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
= ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[14861:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(10537,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[4080,114]) ).
thf(10538,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(simp,[status(thm)],[10537]) ).
thf(10539,plain,
( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
= ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[10538:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(21374,plain,
( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
= ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(rewrite,[status(thm)],[10539,15526]) ).
thf(22384,plain,
( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
= ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(rewrite,[status(thm)],[14862,21374]) ).
thf(6,axiom,
empty_set @ empty,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_xboole_0) ).
thf(42,plain,
empty_set @ empty,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(7,axiom,
! [A: $i] :
( ( A @ empty )
=> ( A = empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
thf(43,plain,
! [A: $i] :
( ( A @ empty )
=> ( A = empty_set ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(44,plain,
! [A: $i] :
( ( A = empty_set )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[43]) ).
thf(45,plain,
! [A: $i] :
( ~ ( A @ empty )
| ( A = empty_set ) ),
inference(lifteq,[status(thm)],[44]) ).
thf(19,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(105,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)],[19]) ).
thf(106,plain,
( ~ ? [A: $i,B: $i] :
( ( B @ ( A @ disjoint ) )
& ? [C: $i] :
( ( B @ ( C @ in ) )
& ( A @ ( C @ in ) ) ) )
& ~ ? [A: $i,B: $i] :
( ~ ? [C: $i] :
( ( B @ ( C @ in ) )
& ( A @ ( C @ in ) ) )
& ~ ( B @ ( A @ disjoint ) ) ) ),
inference(miniscope,[status(thm)],[105]) ).
thf(107,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ~ ( D @ ( C @ disjoint ) )
| ~ ( D @ ( E @ in ) )
| ~ ( C @ ( E @ in ) ) )
& ( ( B @ ( A @ ( B @ sk11 ) @ in ) )
| ( B @ ( A @ disjoint ) ) )
& ( ( A @ ( A @ ( B @ sk11 ) @ in ) )
| ( B @ ( A @ disjoint ) ) ) ),
inference(cnf,[status(esa)],[106]) ).
thf(108,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ ( B @ sk11 ) @ in ) )
| ( B @ ( A @ disjoint ) ) ),
inference(cnfConj,[status(thm)],[107]) ).
thf(9,axiom,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( B @ ( A @ in ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
thf(49,plain,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( B @ ( A @ in ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(50,plain,
~ ? [A: $i,B: $i] :
( ( B @ empty )
& ( B @ ( A @ in ) ) ),
inference(miniscope,[status(thm)],[49]) ).
thf(51,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[50]) ).
thf(147,plain,
! [B: $i,A: $i] :
( ( ( empty_set @ empty )
!= ( B @ empty ) )
| ~ $true
| ~ ( B @ ( A @ in ) ) ),
inference(paramod_ordered,[status(thm)],[42,51]) ).
thf(148,plain,
! [B: $i,A: $i] :
( ( ( empty_set @ empty )
!= ( B @ empty ) )
| ~ ( B @ ( A @ in ) ) ),
inference(simp,[status(thm)],[147]) ).
thf(149,plain,
! [A: $i] :
~ ( empty_set @ ( A @ in ) ),
inference(pattern_uni,[status(thm)],[148:[bind(A,$thf( A )),bind(B,$thf( empty_set ))]]) ).
thf(8172,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk11 ) @ in ) )
!= ( empty_set @ ( C @ in ) ) )
| ~ $true
| ( B @ ( A @ disjoint ) ) ),
inference(paramod_ordered,[status(thm)],[108,149]) ).
thf(8173,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk11 ) @ in ) )
!= ( empty_set @ ( C @ in ) ) )
| ( B @ ( A @ disjoint ) ) ),
inference(simp,[status(thm)],[8172]) ).
thf(8174,plain,
! [A: $i] : ( A @ ( empty_set @ disjoint ) ),
inference(pattern_uni,[status(thm)],[8173:[bind(A,$thf( empty_set )),bind(B,$thf( D )),bind(C,$thf( empty_set @ ( D @ sk11 ) ))]]) ).
thf(8231,plain,
! [A: $i] : ( A @ ( empty_set @ disjoint ) ),
inference(simp,[status(thm)],[8174]) ).
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(93,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ disjoint ) )
=> ( A @ ( B @ disjoint ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(94,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ disjoint ) )
| ~ ( B @ ( A @ disjoint ) ) ),
inference(cnf,[status(esa)],[93]) ).
thf(8294,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( empty_set @ disjoint ) )
!= ( C @ ( B @ disjoint ) ) )
| ( B @ ( C @ disjoint ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8231,94]) ).
thf(8295,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( empty_set @ disjoint ) )
!= ( C @ ( B @ disjoint ) ) )
| ( B @ ( C @ disjoint ) ) ),
inference(simp,[status(thm)],[8294]) ).
thf(8296,plain,
! [A: $i] : ( empty_set @ ( A @ disjoint ) ),
inference(pattern_uni,[status(thm)],[8295:[bind(A,$thf( A )),bind(B,$thf( empty_set )),bind(C,$thf( A ))]]) ).
thf(22,axiom,
! [A: $i,B: $i] : ( A @ ( A @ subset ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
thf(119,plain,
! [A: $i] : ( A @ ( A @ subset ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(120,plain,
! [A: $i] : ( A @ ( A @ subset ) ),
inference(cnf,[status(esa)],[119]) ).
thf(30,plain,
( ~ ( sk3 @ ( sk2 @ disjoint ) )
| ~ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) ) ),
inference(cnfConj,[status(thm)],[26]) ).
thf(355,plain,
! [A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) ) )
| ~ ( sk3 @ ( sk2 @ disjoint ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[120,30]) ).
thf(356,plain,
! [A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) ) )
| ~ ( sk3 @ ( sk2 @ disjoint ) ) ),
inference(simp,[status(thm)],[355]) ).
thf(357,plain,
! [A: $i] :
( ( A
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ( A != sk2 )
| ~ ( sk3 @ ( sk2 @ disjoint ) ) ),
inference(simp,[status(thm)],[356]) ).
thf(358,plain,
( ( ( sk3 @ ( sk1 @ subset_complement ) )
!= sk2 )
| ~ ( sk3 @ ( sk2 @ disjoint ) ) ),
inference(simp,[status(thm)],[357]) ).
thf(8392,plain,
! [A: $i] :
( ( ( empty_set @ ( A @ disjoint ) )
!= ( sk3 @ ( sk2 @ disjoint ) ) )
| ( ( sk3 @ ( sk1 @ subset_complement ) )
!= sk2 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8296,358]) ).
thf(8393,plain,
! [A: $i] :
( ( ( empty_set @ ( A @ disjoint ) )
!= ( sk3 @ ( sk2 @ disjoint ) ) )
| ( ( sk3 @ ( sk1 @ subset_complement ) )
!= sk2 ) ),
inference(simp,[status(thm)],[8392]) ).
thf(8397,plain,
! [A: $i] :
( ( sk3 != empty_set )
| ( A != sk2 )
| ( ( sk3 @ ( sk1 @ subset_complement ) )
!= sk2 ) ),
inference(simp,[status(thm)],[8393]) ).
thf(8403,plain,
( ( sk3 != empty_set )
| ( ( sk3 @ ( sk1 @ subset_complement ) )
!= sk2 ) ),
inference(simp,[status(thm)],[8397]) ).
thf(12561,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ( sk3 != empty_set )
| ( sk2 != sk2 ) ),
inference(paramod_ordered,[status(thm)],[10525,8403]) ).
thf(12562,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[12561]) ).
thf(12606,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) )
!= sk3 )
| ( sk1 != sk1 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[12562]) ).
thf(12619,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) )
!= sk3 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[12606]) ).
thf(14482,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ subset_complement ) ) )
| ( sk3 != empty_set )
| ( sk3 != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[45,12619]) ).
thf(14483,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ subset_complement ) ) )
| ( sk3 != empty_set )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[14482]) ).
thf(14484,plain,
( ( sk3 != empty_set )
| ~ ( sk2 @ ( sk1 @ subset_complement ) @ empty ) ),
inference(pattern_uni,[status(thm)],[14483:[bind(A,$thf( sk2 @ ( sk1 @ subset_complement ) ))]]) ).
thf(20465,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) @ empty )
!= ( empty_set @ empty ) )
| ( sk3 != empty_set )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,14484]) ).
thf(20466,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) @ empty )
!= ( empty_set @ empty ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[20465]) ).
thf(20534,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) )
!= empty_set )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[20466]) ).
thf(11,axiom,
! [A: $i] :
( ( A @ ( empty_set @ set_difference ) )
= empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_boole) ).
thf(54,plain,
! [A: $i] :
( ( A @ ( empty_set @ set_difference ) )
= empty_set ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(55,plain,
! [A: $i] :
( ( A @ ( empty_set @ set_difference ) )
= empty_set ),
inference(cnf,[status(esa)],[54]) ).
thf(56,plain,
! [A: $i] :
( ( A @ ( empty_set @ set_difference ) )
= empty_set ),
inference(lifteq,[status(thm)],[55]) ).
thf(8,axiom,
! [A: $i] :
( ( empty_set @ ( A @ set_difference ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_boole) ).
thf(46,plain,
! [A: $i] :
( ( empty_set @ ( A @ set_difference ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(47,plain,
! [A: $i] :
( ( empty_set @ ( A @ set_difference ) )
= A ),
inference(cnf,[status(esa)],[46]) ).
thf(48,plain,
! [A: $i] :
( ( empty_set @ ( A @ set_difference ) )
= A ),
inference(lifteq,[status(thm)],[47]) ).
thf(31,plain,
sk1 @ powerset @ ( sk3 @ element ),
inference(cnfConj,[status(thm)],[26]) ).
thf(11462,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(paramod_ordered,[status(thm)],[31,123]) ).
thf(11463,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(simp,[status(thm)],[11462]) ).
thf(11464,plain,
( ( sk3 @ ( sk1 @ set_difference ) )
= ( sk3 @ ( sk1 @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[11463:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 ))]]) ).
thf(11688,plain,
! [A: $i] :
( ( ( empty_set @ ( A @ set_difference ) )
!= ( sk3 @ ( sk1 @ set_difference ) ) )
| ( A
= ( sk3 @ ( sk1 @ subset_complement ) ) ) ),
inference(paramod_ordered,[status(thm)],[48,11464]) ).
thf(11719,plain,
! [A: $i] :
( ( sk3 != empty_set )
| ( A != sk1 )
| ( A
= ( sk3 @ ( sk1 @ subset_complement ) ) ) ),
inference(simp,[status(thm)],[11688]) ).
thf(11728,plain,
( ( sk3 != empty_set )
| ( ( sk3 @ ( sk1 @ subset_complement ) )
= sk1 ) ),
inference(simp,[status(thm)],[11719]) ).
thf(116,plain,
! [A: $i] :
( ( A @ sk12 @ empty )
& ( A @ powerset @ ( A @ sk12 @ element ) ) ),
inference(cnf,[status(esa)],[115]) ).
thf(117,plain,
! [A: $i] : ( A @ powerset @ ( A @ sk12 @ element ) ),
inference(cnfConj,[status(thm)],[116]) ).
thf(118,plain,
! [A: $i] : ( A @ sk12 @ empty ),
inference(cnfConj,[status(thm)],[116]) ).
thf(573,plain,
! [B: $i,A: $i] :
( ( ( A @ sk12 @ empty )
!= ( B @ empty ) )
| ~ $true
| ( B = empty_set ) ),
inference(paramod_ordered,[status(thm)],[118,45]) ).
thf(574,plain,
! [B: $i,A: $i] :
( ( ( A @ sk12 @ empty )
!= ( B @ empty ) )
| ( B = empty_set ) ),
inference(simp,[status(thm)],[573]) ).
thf(575,plain,
! [A: $i] :
( ( A @ sk12 )
= empty_set ),
inference(pattern_uni,[status(thm)],[574:[bind(A,$thf( C )),bind(B,$thf( C @ sk12 ))]]) ).
thf(619,plain,
! [A: $i] :
( ( A @ sk12 )
= empty_set ),
inference(simp,[status(thm)],[575]) ).
thf(639,plain,
! [A: $i] : ( A @ powerset @ ( empty_set @ element ) ),
inference(rewrite,[status(thm)],[117,619]) ).
thf(10751,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ~ $true
| ( ( C @ ( B @ subset_complement ) @ ( B @ subset_complement ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[639,114]) ).
thf(10752,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ( ( C @ ( B @ subset_complement ) @ ( B @ subset_complement ) )
= C ) ),
inference(simp,[status(thm)],[10751]) ).
thf(10753,plain,
! [A: $i] :
( ( empty_set @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= empty_set ),
inference(pattern_uni,[status(thm)],[10752:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( empty_set ))]]) ).
thf(11494,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ~ $true
| ( ( C @ ( B @ set_difference ) )
= ( C @ ( B @ subset_complement ) ) ) ),
inference(paramod_ordered,[status(thm)],[639,123]) ).
thf(11495,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ( ( C @ ( B @ set_difference ) )
= ( C @ ( B @ subset_complement ) ) ) ),
inference(simp,[status(thm)],[11494]) ).
thf(11496,plain,
! [A: $i] :
( ( empty_set @ ( A @ set_difference ) )
= ( empty_set @ ( A @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[11495:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( empty_set ))]]) ).
thf(12336,plain,
! [A: $i] :
( ( empty_set @ ( A @ subset_complement ) )
= A ),
inference(rewrite,[status(thm)],[11496,48]) ).
thf(12338,plain,
! [A: $i] :
( ( A @ ( A @ subset_complement ) )
= empty_set ),
inference(rewrite,[status(thm)],[10753,12336]) ).
thf(12910,plain,
! [A: $i] :
( ( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
!= ( A @ ( A @ subset_complement ) ) )
| ( sk2 = empty_set ) ),
inference(paramod_ordered,[status(thm)],[10525,12338]) ).
thf(12945,plain,
! [A: $i] :
( ( ( sk2 @ ( sk1 @ subset_complement ) )
!= A )
| ( sk1 != A )
| ( sk2 = empty_set ) ),
inference(simp,[status(thm)],[12910]) ).
thf(12975,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) )
!= sk1 )
| ( sk2 = empty_set ) ),
inference(simp,[status(thm)],[12945]) ).
thf(18,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(97,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)],[18]) ).
thf(98,plain,
( ! [A: $i,B: $i] :
( ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( B @ ( C @ in ) ) )
=> ( B @ ( A @ subset ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
=> ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( B @ ( C @ in ) ) ) ) ),
inference(miniscope,[status(thm)],[97]) ).
thf(99,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( D @ subset ) )
| ~ ( E @ ( D @ ( E @ sk10 ) @ in ) ) )
& ( ( E @ ( D @ subset ) )
| ( D @ ( D @ ( E @ sk10 ) @ in ) ) )
& ( ( B @ ( C @ in ) )
| ~ ( A @ ( C @ in ) )
| ~ ( B @ ( A @ subset ) ) ) ),
inference(cnf,[status(esa)],[98]) ).
thf(101,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ( A @ ( A @ ( B @ sk10 ) @ in ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(103,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ( A @ ( A @ ( B @ sk10 ) @ in ) ) ),
inference(simp,[status(thm)],[101]) ).
thf(753,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk10 ) @ in ) )
!= ( empty_set @ ( C @ in ) ) )
| ~ $true
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[103,149]) ).
thf(754,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk10 ) @ in ) )
!= ( empty_set @ ( C @ in ) ) )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[753]) ).
thf(755,plain,
! [A: $i] : ( A @ ( empty_set @ subset ) ),
inference(pattern_uni,[status(thm)],[754:[bind(A,$thf( empty_set )),bind(B,$thf( D )),bind(C,$thf( empty_set @ ( D @ sk10 ) ))]]) ).
thf(765,plain,
! [A: $i] : ( A @ ( empty_set @ subset ) ),
inference(simp,[status(thm)],[755]) ).
thf(906,plain,
! [A: $i] :
( ( ( A @ ( empty_set @ subset ) )
!= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) ) )
| ~ ( sk3 @ ( sk2 @ disjoint ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[765,30]) ).
thf(907,plain,
! [A: $i] :
( ( ( A @ ( empty_set @ subset ) )
!= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) ) )
| ~ ( sk3 @ ( sk2 @ disjoint ) ) ),
inference(simp,[status(thm)],[906]) ).
thf(908,plain,
! [A: $i] :
( ( A
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ( sk2 != empty_set )
| ~ ( sk3 @ ( sk2 @ disjoint ) ) ),
inference(simp,[status(thm)],[907]) ).
thf(912,plain,
( ( sk2 != empty_set )
| ~ ( sk3 @ ( sk2 @ disjoint ) ) ),
inference(simp,[status(thm)],[908]) ).
thf(920,plain,
! [A: $i] :
( ( A != sk2 )
| ( empty_set != empty_set )
| ~ ( sk3 @ ( sk2 @ disjoint ) )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[45,912]) ).
thf(921,plain,
! [A: $i] :
( ( A != sk2 )
| ~ ( sk3 @ ( sk2 @ disjoint ) )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[920]) ).
thf(922,plain,
( ~ ( sk3 @ ( sk2 @ disjoint ) )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[921:[bind(A,$thf( sk2 ))]]) ).
thf(946,plain,
! [A: $i] :
( ( A != sk2 )
| ~ ( sk3 @ ( empty_set @ disjoint ) )
| ~ ( sk2 @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[45,922]) ).
thf(947,plain,
( ~ ( sk3 @ ( empty_set @ disjoint ) )
| ~ ( sk2 @ empty )
| ~ ( sk2 @ empty ) ),
inference(pattern_uni,[status(thm)],[946:[bind(A,$thf( sk2 ))]]) ).
thf(966,plain,
( ~ ( sk3 @ ( empty_set @ disjoint ) )
| ~ ( sk2 @ empty ) ),
inference(simp,[status(thm)],[947]) ).
thf(973,plain,
( ( ( sk2 @ empty )
!= ( empty_set @ empty ) )
| ~ ( sk3 @ ( empty_set @ disjoint ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,966]) ).
thf(974,plain,
( ( ( sk2 @ empty )
!= ( empty_set @ empty ) )
| ~ ( sk3 @ ( empty_set @ disjoint ) ) ),
inference(simp,[status(thm)],[973]) ).
thf(997,plain,
( ( sk2 != empty_set )
| ~ ( sk3 @ ( empty_set @ disjoint ) ) ),
inference(simp,[status(thm)],[974]) ).
thf(8245,plain,
( ( sk2 != empty_set )
| ~ $true ),
inference(rewrite,[status(thm)],[997,8231]) ).
thf(8246,plain,
sk2 != empty_set,
inference(simp,[status(thm)],[8245]) ).
thf(25181,plain,
( ( sk2 @ ( sk1 @ subset_complement ) )
!= sk1 ),
inference(simplifyReflect,[status(thm)],[12975,8246]) ).
thf(25187,plain,
( ( ( sk3 @ ( sk1 @ subset_complement ) )
!= ( sk2 @ ( sk1 @ subset_complement ) ) )
| ( sk1 != sk1 )
| ( sk3 != empty_set ) ),
inference(paramod_ordered,[status(thm)],[11728,25181]) ).
thf(25188,plain,
( ( ( sk3 @ ( sk1 @ subset_complement ) )
!= ( sk2 @ ( sk1 @ subset_complement ) ) )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[25187]) ).
thf(25247,plain,
( ( sk3 != sk2 )
| ( sk1 != sk1 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[25188]) ).
thf(25268,plain,
( ( sk3 != sk2 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[25247]) ).
thf(10864,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[5987,10525]) ).
thf(13613,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[10864,10525]) ).
thf(13698,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(paramod_ordered,[status(thm)],[13613,123]) ).
thf(13699,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(simp,[status(thm)],[13698]) ).
thf(13700,plain,
( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
= ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[13699:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(17756,plain,
( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
= ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(rewrite,[status(thm)],[13700,15526]) ).
thf(843,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ ( C @ sk8 ) ) @ in ) )
!= ( empty_set @ ( D @ in ) ) )
| ~ $true
| ( C @ ( B @ ( A @ sk6 ) ) )
| ( C
= ( B @ ( A @ set_difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[69,149]) ).
thf(844,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ ( C @ sk8 ) ) @ in ) )
!= ( empty_set @ ( D @ in ) ) )
| ( C @ ( B @ ( A @ sk6 ) ) )
| ( C
= ( B @ ( A @ set_difference ) ) ) ),
inference(simp,[status(thm)],[843]) ).
thf(845,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( empty_set @ sk6 ) ) )
| ( A
= ( B @ ( empty_set @ set_difference ) ) ) ),
inference(pattern_uni,[status(thm)],[844:[bind(A,$thf( empty_set )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( empty_set @ ( F @ ( E @ sk8 ) ) ))]]) ).
thf(876,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( empty_set @ sk6 ) ) )
| ( A
= ( B @ ( empty_set @ set_difference ) ) ) ),
inference(simp,[status(thm)],[845]) ).
thf(1029,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( empty_set @ sk6 ) ) )
| ( A = empty_set ) ),
inference(rewrite,[status(thm)],[876,56]) ).
thf(1122,plain,
! [B: $i,A: $i] :
( ( A != sk2 )
| ( empty_set != empty_set )
| ~ ( sk3 @ ( empty_set @ disjoint ) )
| ( A @ ( B @ ( empty_set @ sk6 ) ) ) ),
inference(paramod_ordered,[status(thm)],[1029,997]) ).
thf(1123,plain,
! [B: $i,A: $i] :
( ( A != sk2 )
| ~ ( sk3 @ ( empty_set @ disjoint ) )
| ( A @ ( B @ ( empty_set @ sk6 ) ) ) ),
inference(simp,[status(thm)],[1122]) ).
thf(1124,plain,
! [A: $i] :
( ~ ( sk3 @ ( empty_set @ disjoint ) )
| ( sk2 @ ( A @ ( empty_set @ sk6 ) ) ) ),
inference(pattern_uni,[status(thm)],[1123:[bind(A,$thf( sk2 ))]]) ).
thf(1252,plain,
! [A: $i] :
( ~ ( sk3 @ ( empty_set @ disjoint ) )
| ( sk2 @ ( A @ ( empty_set @ sk6 ) ) ) ),
inference(simp,[status(thm)],[1124]) ).
thf(8255,plain,
! [A: $i] :
( ~ $true
| ( sk2 @ ( A @ ( empty_set @ sk6 ) ) ) ),
inference(rewrite,[status(thm)],[1252,8231]) ).
thf(8256,plain,
! [A: $i] : ( sk2 @ ( A @ ( empty_set @ sk6 ) ) ),
inference(simp,[status(thm)],[8255]) ).
thf(4,axiom,
? [A: $i] : ( A @ empty ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_xboole_0) ).
thf(37,plain,
? [A: $i] : ( A @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(11431,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(paramod_ordered,[status(thm)],[3594,123]) ).
thf(11432,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(simp,[status(thm)],[11431]) ).
thf(11433,plain,
( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
= ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[11432:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) ))]]) ).
thf(12008,plain,
( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
= sk2 ),
inference(rewrite,[status(thm)],[11433,10525]) ).
thf(12020,plain,
! [A: $i] :
( ( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
!= ( A @ ( empty_set @ set_difference ) ) )
| ( sk2 = empty_set ) ),
inference(paramod_ordered,[status(thm)],[12008,56]) ).
thf(12127,plain,
! [A: $i] :
( ( ( sk2 @ ( sk1 @ subset_complement ) )
!= A )
| ( sk1 != empty_set )
| ( sk2 = empty_set ) ),
inference(simp,[status(thm)],[12020]) ).
thf(12159,plain,
( ( sk1 != empty_set )
| ( sk2 = empty_set ) ),
inference(simp,[status(thm)],[12127]) ).
thf(13330,plain,
sk1 != empty_set,
inference(simplifyReflect,[status(thm)],[12159,8246]) ).
thf(13337,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( empty_set != empty_set )
| ( A @ ( B @ ( empty_set @ sk6 ) ) ) ),
inference(paramod_ordered,[status(thm)],[1029,13330]) ).
thf(13338,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( A @ ( B @ ( empty_set @ sk6 ) ) ) ),
inference(simp,[status(thm)],[13337]) ).
thf(13339,plain,
! [A: $i] : ( sk1 @ ( A @ ( empty_set @ sk6 ) ) ),
inference(pattern_uni,[status(thm)],[13338:[bind(A,$thf( sk1 ))]]) ).
thf(13346,plain,
! [A: $i] : ( sk1 @ ( A @ ( empty_set @ sk6 ) ) ),
inference(simp,[status(thm)],[13339]) ).
thf(10,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ~ ( A @ ( B @ in ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
thf(52,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ~ ( A @ ( B @ in ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(3,axiom,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( A != B )
& ( A @ empty ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_boole) ).
thf(33,plain,
! [A: $i,B: $i] :
~ ( ( B @ empty )
& ( A != B )
& ( A @ empty ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(34,plain,
~ ? [A: $i] :
( ? [B: $i] :
( ( B @ empty )
& ( A != B ) )
& ( A @ empty ) ),
inference(miniscope,[status(thm)],[33]) ).
thf(35,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ( A = B )
| ~ ( A @ empty ) ),
inference(cnf,[status(esa)],[34]) ).
thf(36,plain,
! [B: $i,A: $i] :
( ~ ( B @ empty )
| ~ ( A @ empty )
| ( A = B ) ),
inference(lifteq,[status(thm)],[35]) ).
thf(29,plain,
( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) )
| ( sk3 @ ( sk2 @ disjoint ) ) ),
inference(cnfConj,[status(thm)],[26]) ).
thf(183,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ( A @ ( sk2 @ subset ) )
| ( sk3 @ ( sk2 @ disjoint ) )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[36,29]) ).
thf(184,plain,
! [A: $i] :
( ( A @ ( sk2 @ subset ) )
| ( sk3 @ ( sk2 @ disjoint ) )
| ~ ( sk3 @ ( sk1 @ subset_complement ) @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[183:[bind(A,$thf( A )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) ))]]) ).
thf(14646,plain,
! [A: $i] :
( ( ( A @ ( A @ subset_complement ) )
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ( sk3 != empty_set )
| ( sk1 = empty_set ) ),
inference(paramod_ordered,[status(thm)],[12338,11728]) ).
thf(14682,plain,
! [A: $i] :
( ( A != sk3 )
| ( A != sk1 )
| ( sk3 != empty_set )
| ( sk1 = empty_set ) ),
inference(simp,[status(thm)],[14646]) ).
thf(14725,plain,
( ( sk3 != sk1 )
| ( sk3 != empty_set )
| ( sk1 = empty_set ) ),
inference(simp,[status(thm)],[14682]) ).
thf(30258,plain,
( ( sk3 != sk1 )
| ( sk3 != empty_set ) ),
inference(simplifyReflect,[status(thm)],[14725,13330]) ).
thf(53,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ in ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[52]) ).
thf(700,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( A @ ( B @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( B @ ( A @ in ) ) ),
inference(eqfactor_ordered,[status(thm)],[53]) ).
thf(701,plain,
! [A: $i] :
~ ( A @ ( A @ in ) ),
inference(pattern_uni,[status(thm)],[700:[bind(A,$thf( B ))]]) ).
thf(702,plain,
! [A: $i] :
~ ( A @ ( A @ in ) ),
inference(simp,[status(thm)],[701]) ).
thf(24,axiom,
! [A: $i] :
? [B: $i] : ( A @ ( B @ element ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_subset_1) ).
thf(124,plain,
! [A: $i] :
? [B: $i] : ( A @ ( B @ element ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(125,plain,
! [A: $i] : ( A @ ( A @ sk13 @ element ) ),
inference(cnf,[status(esa)],[124]) ).
thf(3598,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[31,89]) ).
thf(3599,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[3598]) ).
thf(3600,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[3599:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 ))]]) ).
thf(3780,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3600,89]) ).
thf(3781,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[3780]) ).
thf(3782,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[3781:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) ))]]) ).
thf(3968,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3782,89]) ).
thf(3969,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[3968]) ).
thf(3970,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[3969:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(4255,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3970,89]) ).
thf(4256,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[4255]) ).
thf(4257,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[4256:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(4631,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4257,89]) ).
thf(4632,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[4631]) ).
thf(4633,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[4632:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(5471,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4633,89]) ).
thf(5472,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[5471]) ).
thf(5473,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[5472:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(10665,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[31,114]) ).
thf(10666,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(simp,[status(thm)],[10665]) ).
thf(10667,plain,
( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
= sk3 ),
inference(pattern_uni,[status(thm)],[10666:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 ))]]) ).
thf(11192,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[5473,10667]) ).
thf(12993,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[11192,10667]) ).
thf(599,plain,
! [A: $i] :
( ( A != sk3 )
| ( ( sk3 @ ( sk1 @ subset_complement ) )
!= sk2 )
| ~ ( empty_set @ ( sk2 @ disjoint ) )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[45,358]) ).
thf(600,plain,
( ( ( sk3 @ ( sk1 @ subset_complement ) )
!= sk2 )
| ~ ( empty_set @ ( sk2 @ disjoint ) )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[599:[bind(A,$thf( sk3 ))]]) ).
thf(8366,plain,
( ( ( sk3 @ ( sk1 @ subset_complement ) )
!= sk2 )
| ~ $true
| ~ ( sk3 @ empty ) ),
inference(rewrite,[status(thm)],[600,8296]) ).
thf(8367,plain,
( ( ( sk3 @ ( sk1 @ subset_complement ) )
!= sk2 )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[8366]) ).
thf(12480,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ( sk2 != sk2 )
| ~ ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[10525,8367]) ).
thf(12481,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[12480]) ).
thf(12521,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) )
!= sk3 )
| ( sk1 != sk1 )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[12481]) ).
thf(12531,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) )
!= sk3 )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[12521]) ).
thf(6217,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5473,89]) ).
thf(6218,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[6217]) ).
thf(6219,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[6218:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(11185,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[6219,10667]) ).
thf(13884,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[11185,10667]) ).
thf(13968,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(paramod_ordered,[status(thm)],[13884,123]) ).
thf(13969,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(simp,[status(thm)],[13968]) ).
thf(13970,plain,
( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[13969:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(10673,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[3970,114]) ).
thf(10674,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(simp,[status(thm)],[10673]) ).
thf(10675,plain,
( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[10674:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(15832,plain,
( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
= ( sk3 @ ( sk1 @ subset_complement ) ) ),
inference(rewrite,[status(thm)],[10675,10667]) ).
thf(17955,plain,
( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(rewrite,[status(thm)],[13970,15832]) ).
thf(12920,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
!= ( A @ ( A @ subset_complement ) ) )
| ( sk3 = empty_set ) ),
inference(paramod_ordered,[status(thm)],[10667,12338]) ).
thf(12932,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ subset_complement ) )
!= A )
| ( sk1 != A )
| ( sk3 = empty_set ) ),
inference(simp,[status(thm)],[12920]) ).
thf(12961,plain,
( ( ( sk3 @ ( sk1 @ subset_complement ) )
!= sk1 )
| ( sk3 = empty_set ) ),
inference(simp,[status(thm)],[12932]) ).
thf(11412,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(paramod_ordered,[status(thm)],[3600,123]) ).
thf(11413,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(simp,[status(thm)],[11412]) ).
thf(11414,plain,
( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[11413:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) ))]]) ).
thf(11851,plain,
( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
= sk3 ),
inference(rewrite,[status(thm)],[11414,10667]) ).
thf(11918,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
!= ( empty_set @ ( A @ set_difference ) ) )
| ( sk3 = A ) ),
inference(paramod_ordered,[status(thm)],[11851,48]) ).
thf(11966,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ subset_complement ) )
!= empty_set )
| ( sk1 != A )
| ( sk3 = A ) ),
inference(simp,[status(thm)],[11918]) ).
thf(11991,plain,
( ( ( sk3 @ ( sk1 @ subset_complement ) )
!= empty_set )
| ( sk3 = sk1 ) ),
inference(simp,[status(thm)],[11966]) ).
thf(10862,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[5271,10525]) ).
thf(12621,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[10862,10525]) ).
thf(13,axiom,
! [A: $i] :
( ~ ( A @ empty )
=> ? [B: $i] :
( ~ ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_subset_1) ).
thf(84,plain,
! [A: $i] :
( ~ ( A @ empty )
=> ? [B: $i] :
( ~ ( B @ empty )
& ( A @ powerset @ ( B @ element ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(159,plain,
! [C: $i,B: $i,A: $i] :
( ( A != empty_set )
| ( ( C @ ( B @ set_difference ) )
= empty_set )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[36,56]) ).
thf(160,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ set_difference ) )
= empty_set )
| ~ ( A @ empty )
| ~ ( empty_set @ empty ) ),
inference(pattern_uni,[status(thm)],[159:[bind(A,$thf( empty_set ))]]) ).
thf(319,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ set_difference ) )
= empty_set )
| ~ ( A @ empty )
| ~ ( empty_set @ empty ) ),
inference(simp,[status(thm)],[160]) ).
thf(25740,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ set_difference ) )
= empty_set )
| ~ ( A @ empty )
| ~ $true ),
inference(rewrite,[status(thm)],[319,42]) ).
thf(25741,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ set_difference ) )
= empty_set )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[25740]) ).
thf(25655,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk3 != sk2 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[45,25268]) ).
thf(25656,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk3 != sk2 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[25655]) ).
thf(25657,plain,
( ( sk3 != sk2 )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[25656:[bind(A,$thf( sk3 ))]]) ).
thf(12546,plain,
! [A: $i] :
( ( ( empty_set @ ( A @ subset_complement ) )
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ( sk3 != empty_set )
| ( A != sk2 ) ),
inference(paramod_ordered,[status(thm)],[12336,8403]) ).
thf(12603,plain,
( ( sk3 != empty_set )
| ( sk2 != sk1 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[12546]) ).
thf(12616,plain,
( ( sk2 != sk1 )
| ( sk3 != empty_set ) ),
inference(simp,[status(thm)],[12603]) ).
thf(13146,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk2 != sk1 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[45,12616]) ).
thf(13147,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk2 != sk1 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[13146]) ).
thf(13148,plain,
( ( sk2 != sk1 )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[13147:[bind(A,$thf( sk3 ))]]) ).
thf(7436,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6451,89]) ).
thf(7437,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[7436]) ).
thf(7438,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[7437:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(8563,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7438,89]) ).
thf(8564,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[8563]) ).
thf(8565,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[8564:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(9673,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8565,89]) ).
thf(9674,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[9673]) ).
thf(9675,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[9674:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(23994,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[9675,21374]) ).
thf(23998,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
!= ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) )
| ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) ) ),
inference(paramod_ordered,[status(thm)],[10525,23994]) ).
thf(23999,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[23998:[]]) ).
thf(24737,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[23999,21374]) ).
thf(24763,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24737,89]) ).
thf(24764,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[24763]) ).
thf(24765,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[24764:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(25288,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[24765,21374]) ).
thf(3604,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk13 @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ( B @ powerset @ ( C @ ( B @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[125,89]) ).
thf(3605,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk13 @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ( B @ powerset @ ( C @ ( B @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[3604]) ).
thf(3606,plain,
! [A: $i] : ( A @ powerset @ ( A @ powerset @ sk13 @ ( A @ subset_complement ) @ element ) ),
inference(pattern_uni,[status(thm)],[3605:[bind(A,$thf( E @ powerset )),bind(B,$thf( E )),bind(C,$thf( E @ powerset @ sk13 ))]]) ).
thf(3679,plain,
! [A: $i] : ( A @ powerset @ ( A @ powerset @ sk13 @ ( A @ subset_complement ) @ element ) ),
inference(simp,[status(thm)],[3606]) ).
thf(13333,plain,
! [A: $i] :
( ( A != sk1 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[45,13330]) ).
thf(13334,plain,
! [A: $i] :
( ( A != sk1 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[13333]) ).
thf(13335,plain,
~ ( sk1 @ empty ),
inference(pattern_uni,[status(thm)],[13334:[bind(A,$thf( sk1 ))]]) ).
thf(11400,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk13 @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ~ $true
| ( ( C @ ( B @ set_difference ) )
= ( C @ ( B @ subset_complement ) ) ) ),
inference(paramod_ordered,[status(thm)],[125,123]) ).
thf(11401,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk13 @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ( ( C @ ( B @ set_difference ) )
= ( C @ ( B @ subset_complement ) ) ) ),
inference(simp,[status(thm)],[11400]) ).
thf(11402,plain,
! [A: $i] :
( ( A @ powerset @ sk13 @ ( A @ set_difference ) )
= ( A @ powerset @ sk13 @ ( A @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[11401:[bind(A,$thf( E @ powerset )),bind(B,$thf( E )),bind(C,$thf( E @ powerset @ sk13 ))]]) ).
thf(11498,plain,
! [A: $i] :
( ( A @ powerset @ sk13 @ ( A @ set_difference ) )
= ( A @ powerset @ sk13 @ ( A @ subset_complement ) ) ),
inference(simp,[status(thm)],[11402]) ).
thf(18976,plain,
! [B: $i,A: $i] :
( ( ( A @ powerset @ sk13 @ ( A @ set_difference ) )
!= ( B @ ( empty_set @ set_difference ) ) )
| ( ( A @ powerset @ sk13 @ ( A @ subset_complement ) )
= empty_set ) ),
inference(paramod_ordered,[status(thm)],[11498,56]) ).
thf(18977,plain,
( ( empty_set @ powerset @ sk13 @ ( empty_set @ subset_complement ) )
= empty_set ),
inference(pattern_uni,[status(thm)],[18976:[bind(A,$thf( empty_set )),bind(B,$thf( empty_set @ powerset @ sk13 ))]]) ).
thf(10443,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk13 @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ~ $true
| ( ( C @ ( B @ subset_complement ) @ ( B @ subset_complement ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[125,114]) ).
thf(10444,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ sk13 @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ( ( C @ ( B @ subset_complement ) @ ( B @ subset_complement ) )
= C ) ),
inference(simp,[status(thm)],[10443]) ).
thf(10445,plain,
! [A: $i] :
( ( A @ powerset @ sk13 @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= ( A @ powerset @ sk13 ) ),
inference(pattern_uni,[status(thm)],[10444:[bind(A,$thf( E @ powerset )),bind(B,$thf( E )),bind(C,$thf( E @ powerset @ sk13 ))]]) ).
thf(10841,plain,
! [A: $i] :
( ( A @ powerset @ sk13 @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= ( A @ powerset @ sk13 ) ),
inference(simp,[status(thm)],[10445]) ).
thf(19143,plain,
! [A: $i] :
( ( ( empty_set @ powerset @ sk13 @ ( empty_set @ subset_complement ) )
!= ( A @ powerset @ sk13 @ ( A @ subset_complement ) ) )
| ( ( empty_set @ ( A @ subset_complement ) )
= ( A @ powerset @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[18977,10841]) ).
thf(19144,plain,
( ( empty_set @ ( empty_set @ subset_complement ) )
= ( empty_set @ powerset @ sk13 ) ),
inference(pattern_uni,[status(thm)],[19143:[bind(A,$thf( empty_set ))]]) ).
thf(19396,plain,
( ( empty_set @ powerset @ sk13 )
= empty_set ),
inference(rewrite,[status(thm)],[19144,12336]) ).
thf(15,axiom,
! [A: $i] :
~ ( A @ powerset @ empty ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
thf(90,plain,
! [A: $i] :
~ ( A @ powerset @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(91,plain,
~ ? [A: $i] : ( A @ powerset @ empty ),
inference(miniscope,[status(thm)],[90]) ).
thf(92,plain,
! [A: $i] :
~ ( A @ powerset @ empty ),
inference(cnf,[status(esa)],[91]) ).
thf(19422,plain,
! [A: $i] :
( ( ( empty_set @ powerset @ sk13 )
!= ( A @ powerset @ sk13 ) )
| ( ( empty_set @ ( A @ set_difference ) )
= ( A @ powerset @ sk13 @ ( A @ subset_complement ) ) ) ),
inference(paramod_ordered,[status(thm)],[19396,11498]) ).
thf(19423,plain,
( ( empty_set @ ( empty_set @ set_difference ) )
= ( empty_set @ powerset @ sk13 @ ( empty_set @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[19422:[bind(A,$thf( empty_set ))]]) ).
thf(19748,plain,
( ( empty_set @ ( empty_set @ subset_complement ) )
= empty_set ),
inference(rewrite,[status(thm)],[19423,48,19396]) ).
thf(8237,plain,
( ~ $true
| ~ ( sk2 @ empty ) ),
inference(rewrite,[status(thm)],[966,8231]) ).
thf(8238,plain,
~ ( sk2 @ empty ),
inference(simp,[status(thm)],[8237]) ).
thf(6711,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6219,89]) ).
thf(6712,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[6711]) ).
thf(6713,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[6712:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(7728,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[6713,89]) ).
thf(7729,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[7728]) ).
thf(7730,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[7729:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(8885,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7730,89]) ).
thf(8886,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[8885]) ).
thf(8887,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[8886:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(10025,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8887,89]) ).
thf(10026,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[10025]) ).
thf(10027,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[10026:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(10705,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[4257,114]) ).
thf(10706,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(simp,[status(thm)],[10705]) ).
thf(10707,plain,
( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[10706:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(21862,plain,
( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(rewrite,[status(thm)],[10707,15832]) ).
thf(26546,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[10027,21862]) ).
thf(10429,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[4633,114]) ).
thf(10430,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(simp,[status(thm)],[10429]) ).
thf(10431,plain,
( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[10430:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(29553,plain,
( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(rewrite,[status(thm)],[10431,21862]) ).
thf(29556,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[26546,29553]) ).
thf(30359,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[29556,29553]) ).
thf(187,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ( A @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) )
| ( sk3 @ ( sk2 @ disjoint ) )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[36,29]) ).
thf(188,plain,
! [A: $i] :
( ( A @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) )
| ( sk3 @ ( sk2 @ disjoint ) )
| ~ ( sk3 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[187:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(109,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ sk11 ) @ in ) )
| ( B @ ( A @ disjoint ) ) ),
inference(cnfConj,[status(thm)],[107]) ).
thf(66,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( B @ ( A @ set_difference ) ) )
| ~ ( C @ ( B @ ( A @ sk6 ) ) )
| ( B @ ( A @ ( B @ ( C @ sk7 ) ) @ in ) )
| ~ ( A @ ( A @ ( B @ ( C @ sk7 ) ) @ in ) ) ),
inference(cnfConj,[status(thm)],[59]) ).
thf(76,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ sk6 ) ) )
| ( B @ ( A @ ( B @ ( C @ sk7 ) ) @ in ) )
| ~ ( A @ ( A @ ( B @ ( C @ sk7 ) ) @ in ) )
| ( C
= ( B @ ( A @ set_difference ) ) ) ),
inference(lifteq,[status(thm)],[66]) ).
thf(77,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ sk6 ) ) )
| ( B @ ( A @ ( B @ ( C @ sk7 ) ) @ in ) )
| ~ ( A @ ( A @ ( B @ ( C @ sk7 ) ) @ in ) )
| ( C
= ( B @ ( A @ set_difference ) ) ) ),
inference(simp,[status(thm)],[76]) ).
thf(38,plain,
sk4 @ empty,
inference(cnf,[status(esa)],[37]) ).
thf(552,plain,
! [A: $i] :
( ( ( sk4 @ empty )
!= ( A @ empty ) )
| ~ $true
| ( A = empty_set ) ),
inference(paramod_ordered,[status(thm)],[38,45]) ).
thf(553,plain,
! [A: $i] :
( ( ( sk4 @ empty )
!= ( A @ empty ) )
| ( A = empty_set ) ),
inference(simp,[status(thm)],[552]) ).
thf(554,plain,
sk4 = empty_set,
inference(pattern_uni,[status(thm)],[553:[bind(A,$thf( sk4 ))]]) ).
thf(17,axiom,
! [A: $i,B: $i] :
( ( A @ powerset @ ( B @ element ) )
=> ! [C: $i] :
( ( B @ ( C @ in ) )
=> ( A @ ( C @ in ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l3_subset_1) ).
thf(95,plain,
! [A: $i,B: $i] :
( ( A @ powerset @ ( B @ element ) )
=> ! [C: $i] :
( ( B @ ( C @ in ) )
=> ( A @ ( C @ in ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(96,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ in ) )
| ~ ( B @ ( C @ in ) )
| ~ ( A @ powerset @ ( B @ element ) ) ),
inference(cnf,[status(esa)],[95]) ).
thf(85,plain,
! [A: $i] :
( ( ~ ( A @ sk9 @ empty )
| ( A @ empty ) )
& ( ( A @ powerset @ ( A @ sk9 @ element ) )
| ( A @ empty ) ) ),
inference(cnf,[status(esa)],[84]) ).
thf(87,plain,
! [A: $i] :
( ~ ( A @ sk9 @ empty )
| ( A @ empty ) ),
inference(cnfConj,[status(thm)],[85]) ).
thf(3521,plain,
! [A: $i] :
( ( ( A @ sk9 @ empty )
!= ( empty_set @ empty ) )
| ~ $true
| ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[42,87]) ).
thf(3522,plain,
! [A: $i] :
( ( ( A @ sk9 @ empty )
!= ( empty_set @ empty ) )
| ( A @ empty ) ),
inference(simp,[status(thm)],[3521]) ).
thf(3541,plain,
! [A: $i] :
( ( ( A @ sk9 )
!= empty_set )
| ( A @ empty ) ),
inference(simp,[status(thm)],[3522]) ).
thf(5,axiom,
? [A: $i] :
~ ( A @ empty ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
thf(39,plain,
? [A: $i] :
~ ( A @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(40,plain,
~ ! [A: $i] : ( A @ empty ),
inference(miniscope,[status(thm)],[39]) ).
thf(41,plain,
~ ( sk5 @ empty ),
inference(cnf,[status(esa)],[40]) ).
thf(65,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ in ) )
| ( B @ ( D @ in ) )
| ~ ( A @ ( D @ in ) )
| ( C
!= ( B @ ( A @ set_difference ) ) ) ),
inference(cnfConj,[status(thm)],[59]) ).
thf(72,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ in ) )
| ( B @ ( D @ in ) )
| ~ ( A @ ( D @ in ) )
| ( C
!= ( B @ ( A @ set_difference ) ) ) ),
inference(lifteq,[status(thm)],[65]) ).
thf(73,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ set_difference ) @ ( C @ in ) )
| ( B @ ( C @ in ) )
| ~ ( A @ ( C @ in ) ) ),
inference(simp,[status(thm)],[72]) ).
thf(14626,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( empty_set != empty_set )
| ( ( sk3 @ ( sk1 @ subset_complement ) )
= sk1 )
| ( A @ ( B @ ( empty_set @ sk6 ) ) ) ),
inference(paramod_ordered,[status(thm)],[1029,11728]) ).
thf(14627,plain,
! [B: $i,A: $i] :
( ( A != sk3 )
| ( ( sk3 @ ( sk1 @ subset_complement ) )
= sk1 )
| ( A @ ( B @ ( empty_set @ sk6 ) ) ) ),
inference(simp,[status(thm)],[14626]) ).
thf(14628,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ subset_complement ) )
= sk1 )
| ( sk3 @ ( A @ ( empty_set @ sk6 ) ) ) ),
inference(pattern_uni,[status(thm)],[14627:[bind(A,$thf( sk3 ))]]) ).
thf(14713,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ subset_complement ) )
= sk1 )
| ( sk3 @ ( A @ ( empty_set @ sk6 ) ) ) ),
inference(simp,[status(thm)],[14628]) ).
thf(129,plain,
( ( ( sk5 @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,41]) ).
thf(130,plain,
( ( sk5 @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[129]) ).
thf(131,plain,
sk5 != empty_set,
inference(simp,[status(thm)],[130]) ).
thf(1087,plain,
! [B: $i,A: $i] :
( ( A != sk5 )
| ( empty_set != empty_set )
| ( A @ ( B @ ( empty_set @ sk6 ) ) ) ),
inference(paramod_ordered,[status(thm)],[1029,131]) ).
thf(1088,plain,
! [B: $i,A: $i] :
( ( A != sk5 )
| ( A @ ( B @ ( empty_set @ sk6 ) ) ) ),
inference(simp,[status(thm)],[1087]) ).
thf(1089,plain,
! [A: $i] : ( sk5 @ ( A @ ( empty_set @ sk6 ) ) ),
inference(pattern_uni,[status(thm)],[1088:[bind(A,$thf( sk5 ))]]) ).
thf(1241,plain,
! [A: $i] : ( sk5 @ ( A @ ( empty_set @ sk6 ) ) ),
inference(simp,[status(thm)],[1089]) ).
thf(3664,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ( B @ powerset @ ( C @ ( B @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[639,89]) ).
thf(3665,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( empty_set @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ( B @ powerset @ ( C @ ( B @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[3664]) ).
thf(3666,plain,
! [A: $i] : ( A @ powerset @ ( empty_set @ ( A @ subset_complement ) @ element ) ),
inference(pattern_uni,[status(thm)],[3665:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( empty_set ))]]) ).
thf(12337,plain,
! [A: $i] : ( A @ powerset @ ( A @ element ) ),
inference(rewrite,[status(thm)],[3666,12336]) ).
thf(12842,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ( B @ powerset @ ( C @ ( B @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[12337,89]) ).
thf(12843,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ( B @ powerset @ ( C @ ( B @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[12842]) ).
thf(12844,plain,
! [A: $i] : ( A @ powerset @ ( A @ ( A @ subset_complement ) @ element ) ),
inference(pattern_uni,[status(thm)],[12843:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(13553,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ ( A @ subset_complement ) @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ~ $true
| ( ( C @ ( B @ set_difference ) )
= ( C @ ( B @ subset_complement ) ) ) ),
inference(paramod_ordered,[status(thm)],[12844,123]) ).
thf(13554,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ ( A @ subset_complement ) @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ( ( C @ ( B @ set_difference ) )
= ( C @ ( B @ subset_complement ) ) ) ),
inference(simp,[status(thm)],[13553]) ).
thf(13555,plain,
! [A: $i] :
( ( A @ ( A @ subset_complement ) @ ( A @ set_difference ) )
= ( A @ ( A @ subset_complement ) @ ( A @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[13554:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ ( E @ subset_complement ) ))]]) ).
thf(13598,plain,
! [A: $i] :
( ( A @ ( A @ subset_complement ) @ ( A @ set_difference ) )
= ( A @ ( A @ subset_complement ) @ ( A @ subset_complement ) ) ),
inference(simp,[status(thm)],[13555]) ).
thf(12839,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ~ $true
| ( ( C @ ( B @ subset_complement ) @ ( B @ subset_complement ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[12337,114]) ).
thf(12840,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ( ( C @ ( B @ subset_complement ) @ ( B @ subset_complement ) )
= C ) ),
inference(simp,[status(thm)],[12839]) ).
thf(12841,plain,
! [A: $i] :
( ( A @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= A ),
inference(pattern_uni,[status(thm)],[12840:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(23661,plain,
! [A: $i] :
( ( A @ ( A @ subset_complement ) @ ( A @ set_difference ) )
= A ),
inference(rewrite,[status(thm)],[13598,12841]) ).
thf(295,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ~ ( sk3 @ ( sk2 @ disjoint ) )
| ~ ( A @ ( sk2 @ subset ) )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[36,30]) ).
thf(296,plain,
! [A: $i] :
( ~ ( sk3 @ ( sk2 @ disjoint ) )
| ~ ( A @ ( sk2 @ subset ) )
| ~ ( sk3 @ ( sk1 @ subset_complement ) @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[295:[bind(A,$thf( A )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) ))]]) ).
thf(60,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( D @ in ) )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ set_difference ) ) ) ),
inference(cnfConj,[status(thm)],[59]) ).
thf(70,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( D @ in ) )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ set_difference ) ) ) ),
inference(lifteq,[status(thm)],[60]) ).
thf(71,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ in ) )
| ~ ( B @ ( A @ set_difference ) @ ( C @ in ) ) ),
inference(simp,[status(thm)],[70]) ).
thf(132,plain,
! [A: $i] :
( ( ( A @ powerset @ empty )
!= ( empty_set @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,92]) ).
thf(133,plain,
! [A: $i] :
( ( A @ powerset @ empty )
!= ( empty_set @ empty ) ),
inference(simp,[status(thm)],[132]) ).
thf(136,plain,
! [A: $i] :
( ( A @ powerset )
!= empty_set ),
inference(simp,[status(thm)],[133]) ).
thf(1184,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ powerset ) )
| ( empty_set != empty_set )
| ( A @ ( B @ ( empty_set @ sk6 ) ) ) ),
inference(paramod_ordered,[status(thm)],[1029,136]) ).
thf(1185,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ powerset ) )
| ( A @ ( B @ ( empty_set @ sk6 ) ) ) ),
inference(simp,[status(thm)],[1184]) ).
thf(1186,plain,
! [B: $i,A: $i] : ( B @ powerset @ ( A @ ( empty_set @ sk6 ) ) ),
inference(pattern_uni,[status(thm)],[1185:[bind(A,$thf( D @ powerset )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(1224,plain,
! [B: $i,A: $i] : ( B @ powerset @ ( A @ ( empty_set @ sk6 ) ) ),
inference(simp,[status(thm)],[1186]) ).
thf(86,plain,
! [A: $i] :
( ( A @ powerset @ ( A @ sk9 @ element ) )
| ( A @ empty ) ),
inference(cnfConj,[status(thm)],[85]) ).
thf(67,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( B @ ( A @ set_difference ) ) )
| ~ ( B @ ( A @ ( B @ ( C @ sk8 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk6 ) ) ) ),
inference(cnfConj,[status(thm)],[59]) ).
thf(80,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ ( C @ sk8 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk6 ) ) )
| ( C
= ( B @ ( A @ set_difference ) ) ) ),
inference(lifteq,[status(thm)],[67]) ).
thf(81,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ ( C @ sk8 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk6 ) ) )
| ( C
= ( B @ ( A @ set_difference ) ) ) ),
inference(simp,[status(thm)],[80]) ).
thf(239,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ( sk1 @ powerset @ ( A @ element ) )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[36,31]) ).
thf(240,plain,
! [A: $i] :
( ( sk1 @ powerset @ ( A @ element ) )
| ~ ( sk3 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[239:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(11373,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,123]) ).
thf(11374,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(simp,[status(thm)],[11373]) ).
thf(11375,plain,
( ( sk2 @ ( sk1 @ set_difference ) )
= ( sk2 @ ( sk1 @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[11374:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(305,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ~ ( A @ ( sk2 @ disjoint ) )
| ~ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[36,30]) ).
thf(306,plain,
! [A: $i] :
( ~ ( A @ ( sk2 @ disjoint ) )
| ~ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) )
| ~ ( sk3 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[305:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(12077,plain,
! [A: $i] :
( ( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
!= ( empty_set @ ( A @ set_difference ) ) )
| ( sk2 = A ) ),
inference(paramod_ordered,[status(thm)],[12008,48]) ).
thf(12124,plain,
! [A: $i] :
( ( ( sk2 @ ( sk1 @ subset_complement ) )
!= empty_set )
| ( sk1 != A )
| ( sk2 = A ) ),
inference(simp,[status(thm)],[12077]) ).
thf(12156,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) )
!= empty_set )
| ( sk2 = sk1 ) ),
inference(simp,[status(thm)],[12124]) ).
thf(14605,plain,
! [A: $i] :
( ( A != sk3 )
| ( empty_set != empty_set )
| ( ( sk3 @ ( sk1 @ subset_complement ) )
= sk1 )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[45,11728]) ).
thf(14606,plain,
! [A: $i] :
( ( A != sk3 )
| ( ( sk3 @ ( sk1 @ subset_complement ) )
= sk1 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[14605]) ).
thf(14607,plain,
( ( ( sk3 @ ( sk1 @ subset_complement ) )
= sk1 )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[14606:[bind(A,$thf( sk3 ))]]) ).
thf(28253,plain,
( ( ( sk3 @ ( sk1 @ subset_complement ) )
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ( sk1 != sk1 )
| ( sk3 = empty_set )
| ~ ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[14607,12961]) ).
thf(28254,plain,
( ( ( sk3 @ ( sk1 @ subset_complement ) )
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ( sk3 = empty_set )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[28253]) ).
thf(28255,plain,
( ( sk3 = empty_set )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[28254:[]]) ).
thf(12856,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ~ $true
| ( ( C @ ( B @ set_difference ) )
= ( C @ ( B @ subset_complement ) ) ) ),
inference(paramod_ordered,[status(thm)],[12337,123]) ).
thf(12857,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ powerset @ ( A @ element ) )
!= ( B @ powerset @ ( C @ element ) ) )
| ( ( C @ ( B @ set_difference ) )
= ( C @ ( B @ subset_complement ) ) ) ),
inference(simp,[status(thm)],[12856]) ).
thf(12858,plain,
! [A: $i] :
( ( A @ ( A @ set_difference ) )
= ( A @ ( A @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[12857:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(20481,plain,
! [A: $i] :
( ( A != sk3 )
| ( empty_set != empty_set )
| ~ ( sk2 @ ( sk1 @ subset_complement ) @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[45,14484]) ).
thf(20482,plain,
! [A: $i] :
( ( A != sk3 )
| ~ ( sk2 @ ( sk1 @ subset_complement ) @ empty )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[20481]) ).
thf(20483,plain,
( ~ ( sk2 @ ( sk1 @ subset_complement ) @ empty )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[20482:[bind(A,$thf( sk3 ))]]) ).
thf(23328,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) @ empty )
!= ( empty_set @ empty ) )
| ~ $true
| ~ ( sk3 @ empty ) ),
inference(paramod_ordered,[status(thm)],[42,20483]) ).
thf(23329,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) @ empty )
!= ( empty_set @ empty ) )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[23328]) ).
thf(23409,plain,
( ( ( sk2 @ ( sk1 @ subset_complement ) )
!= empty_set )
| ~ ( sk3 @ empty ) ),
inference(simp,[status(thm)],[23329]) ).
thf(26637,plain,
( ( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
!= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) )
| ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) ) ),
inference(paramod_ordered,[status(thm)],[21862,26546]) ).
thf(26638,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[26637:[]]) ).
thf(27289,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[26638,21862]) ).
thf(27308,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[27289,89]) ).
thf(27309,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( A @ powerset @ ( B @ ( A @ subset_complement ) @ element ) ) ),
inference(simp,[status(thm)],[27308]) ).
thf(27310,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(pattern_uni,[status(thm)],[27309:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(27861,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[27310,21862]) ).
thf(30263,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk3 != sk1 )
| ( empty_set != empty_set )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[45,30258]) ).
thf(30264,plain,
! [A: $i] :
( ( A != sk3 )
| ( sk3 != sk1 )
| ~ ( A @ empty ) ),
inference(simp,[status(thm)],[30263]) ).
thf(30265,plain,
( ( sk3 != sk1 )
| ~ ( sk3 @ empty ) ),
inference(pattern_uni,[status(thm)],[30264:[bind(A,$thf( sk3 ))]]) ).
thf(15343,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ subset_complement ) )
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ( ( sk1 @ ( sk1 @ set_difference ) )
= sk3 )
| ( sk3 @ ( A @ ( empty_set @ sk6 ) ) ) ),
inference(paramod_ordered,[status(thm)],[14713,11851]) ).
thf(15344,plain,
! [A: $i] :
( ( ( sk1 @ ( sk1 @ set_difference ) )
= sk3 )
| ( sk3 @ ( A @ ( empty_set @ sk6 ) ) ) ),
inference(pattern_uni,[status(thm)],[15343:[]]) ).
thf(18495,plain,
! [A: $i] :
( ( ( sk1 @ ( sk1 @ subset_complement ) )
= sk3 )
| ( sk3 @ ( A @ ( empty_set @ sk6 ) ) ) ),
inference(rewrite,[status(thm)],[15344,12858]) ).
thf(18614,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ subset_complement ) )
!= ( B @ ( B @ subset_complement ) ) )
| ( sk3 = empty_set )
| ( sk3 @ ( A @ ( empty_set @ sk6 ) ) ) ),
inference(paramod_ordered,[status(thm)],[18495,12338]) ).
thf(18615,plain,
! [A: $i] :
( ( sk3 = empty_set )
| ( sk3 @ ( A @ ( empty_set @ sk6 ) ) ) ),
inference(pattern_uni,[status(thm)],[18614:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(10581,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[4465,114]) ).
thf(10582,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ subset_complement ) @ ( A @ subset_complement ) )
= B ) ),
inference(simp,[status(thm)],[10581]) ).
thf(10583,plain,
( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
= ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[10582:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(30835,plain,
( ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) )
= ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(rewrite,[status(thm)],[10583,21374]) ).
thf(30837,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[23994,30835]) ).
thf(31518,plain,
sk1 @ powerset @ ( sk2 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[30837,30835]) ).
thf(11187,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[6713,10667]) ).
thf(15013,plain,
sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ),
inference(rewrite,[status(thm)],[11187,10667]) ).
thf(15120,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ~ $true
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(paramod_ordered,[status(thm)],[15013,123]) ).
thf(15121,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ powerset @ ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ element ) )
!= ( A @ powerset @ ( B @ element ) ) )
| ( ( B @ ( A @ set_difference ) )
= ( B @ ( A @ subset_complement ) ) ) ),
inference(simp,[status(thm)],[15120]) ).
thf(15122,plain,
( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(pattern_uni,[status(thm)],[15121:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ))]]) ).
thf(23014,plain,
( ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ set_difference ) )
= ( sk3 @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) @ ( sk1 @ subset_complement ) ) ),
inference(rewrite,[status(thm)],[15122,21862]) ).
thf(12367,plain,
! [A: $i] :
( ( ( empty_set @ ( A @ subset_complement ) )
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ( ( A @ ( sk1 @ set_difference ) )
= sk3 ) ),
inference(paramod_ordered,[status(thm)],[12336,11851]) ).
thf(12422,plain,
! [A: $i] :
( ( sk3 != empty_set )
| ( A != sk1 )
| ( ( A @ ( sk1 @ set_difference ) )
= sk3 ) ),
inference(simp,[status(thm)],[12367]) ).
thf(12431,plain,
( ( sk3 != empty_set )
| ( ( sk1 @ ( sk1 @ set_difference ) )
= sk3 ) ),
inference(simp,[status(thm)],[12422]) ).
thf(19456,plain,
( ( sk3 != empty_set )
| ( ( sk1 @ ( sk1 @ subset_complement ) )
= sk3 ) ),
inference(rewrite,[status(thm)],[12431,12858]) ).
thf(102,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ~ ( B @ ( A @ ( B @ sk10 ) @ in ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(104,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ~ ( B @ ( A @ ( B @ sk10 ) @ in ) ) ),
inference(simp,[status(thm)],[102]) ).
thf(64,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( D @ in ) )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ set_difference ) ) ) ),
inference(cnfConj,[status(thm)],[59]) ).
thf(74,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( D @ in ) )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ set_difference ) ) ) ),
inference(lifteq,[status(thm)],[64]) ).
thf(75,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ in ) )
| ~ ( B @ ( A @ set_difference ) @ ( C @ in ) ) ),
inference(simp,[status(thm)],[74]) ).
thf(299,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ~ ( sk3 @ ( sk2 @ disjoint ) )
| ~ ( A @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) )
| ~ ( B @ empty )
| ~ ( A @ empty ) ),
inference(paramod_ordered,[status(thm)],[36,30]) ).
thf(300,plain,
! [A: $i] :
( ~ ( sk3 @ ( sk2 @ disjoint ) )
| ~ ( A @ ( sk1 @ subset_complement ) @ ( sk2 @ subset ) )
| ~ ( sk3 @ empty )
| ~ ( A @ empty ) ),
inference(pattern_uni,[status(thm)],[299:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(17238,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ subset_complement ) ) )
| ( empty_set != empty_set )
| ( sk2 = sk1 )
| ( A @ ( B @ ( empty_set @ sk6 ) ) ) ),
inference(paramod_ordered,[status(thm)],[1029,12156]) ).
thf(17239,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ subset_complement ) ) )
| ( sk2 = sk1 )
| ( A @ ( B @ ( empty_set @ sk6 ) ) ) ),
inference(simp,[status(thm)],[17238]) ).
thf(17240,plain,
! [A: $i] :
( ( sk2 = sk1 )
| ( sk2 @ ( sk1 @ subset_complement ) @ ( A @ ( empty_set @ sk6 ) ) ) ),
inference(pattern_uni,[status(thm)],[17239:[bind(A,$thf( sk2 @ ( sk1 @ subset_complement ) )),bind(B,$thf( B ))]]) ).
thf(17284,plain,
! [A: $i] :
( ( sk2 = sk1 )
| ( sk2 @ ( sk1 @ subset_complement ) @ ( A @ ( empty_set @ sk6 ) ) ) ),
inference(simp,[status(thm)],[17240]) ).
thf(63,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( B @ ( A @ set_difference ) ) )
| ~ ( C @ ( B @ ( A @ sk6 ) ) )
| ( C @ ( A @ ( B @ ( C @ sk7 ) ) @ in ) ) ),
inference(cnfConj,[status(thm)],[59]) ).
thf(78,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ sk6 ) ) )
| ( C @ ( A @ ( B @ ( C @ sk7 ) ) @ in ) )
| ( C
= ( B @ ( A @ set_difference ) ) ) ),
inference(lifteq,[status(thm)],[63]) ).
thf(79,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ sk6 ) ) )
| ( C @ ( A @ ( B @ ( C @ sk7 ) ) @ in ) )
| ( C
= ( B @ ( A @ set_difference ) ) ) ),
inference(simp,[status(thm)],[78]) ).
thf(16509,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ( empty_set != empty_set )
| ( sk3 = sk1 )
| ( A @ ( B @ ( empty_set @ sk6 ) ) ) ),
inference(paramod_ordered,[status(thm)],[1029,11991]) ).
thf(16510,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk3 @ ( sk1 @ subset_complement ) ) )
| ( sk3 = sk1 )
| ( A @ ( B @ ( empty_set @ sk6 ) ) ) ),
inference(simp,[status(thm)],[16509]) ).
thf(16511,plain,
! [A: $i] :
( ( sk3 = sk1 )
| ( sk3 @ ( sk1 @ subset_complement ) @ ( A @ ( empty_set @ sk6 ) ) ) ),
inference(pattern_uni,[status(thm)],[16510:[bind(A,$thf( sk3 @ ( sk1 @ subset_complement ) )),bind(B,$thf( B ))]]) ).
thf(16563,plain,
! [A: $i] :
( ( sk3 = sk1 )
| ( sk3 @ ( sk1 @ subset_complement ) @ ( A @ ( empty_set @ sk6 ) ) ) ),
inference(simp,[status(thm)],[16511]) ).
thf(62,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( B @ ( A @ set_difference ) ) )
| ~ ( C @ ( A @ ( B @ ( C @ sk8 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk6 ) ) ) ),
inference(cnfConj,[status(thm)],[59]) ).
thf(82,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ ( B @ ( C @ sk8 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk6 ) ) )
| ( C
= ( B @ ( A @ set_difference ) ) ) ),
inference(lifteq,[status(thm)],[62]) ).
thf(83,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ ( B @ ( C @ sk8 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk6 ) ) )
| ( C
= ( B @ ( A @ set_difference ) ) ) ),
inference(simp,[status(thm)],[82]) ).
thf(100,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ in ) )
| ~ ( A @ ( C @ in ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(110,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ disjoint ) )
| ~ ( B @ ( C @ in ) )
| ~ ( A @ ( C @ in ) ) ),
inference(cnfConj,[status(thm)],[107]) ).
thf(111,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ disjoint ) )
| ~ ( B @ ( C @ in ) )
| ~ ( A @ ( C @ in ) ) ),
inference(simp,[status(thm)],[110]) ).
thf(38848,plain,
$false,
inference(e,[status(thm)],[10525,69,88,15526,115,22384,20534,120,56,25268,42,17756,8256,37,13346,25,52,184,30258,619,702,125,12993,12531,17955,12961,46,93,11991,57,29,12621,8367,121,8246,84,89,11728,25741,25657,13148,25288,3679,13335,28,14484,19396,33,92,19748,97,3600,21374,8403,8238,30359,188,53,109,124,77,554,96,3541,41,21862,73,14713,105,1241,765,23661,45,11464,296,149,71,54,3594,49,1224,86,12337,39,81,12619,103,11498,240,1029,108,11375,12336,306,13330,25181,12156,112,123,12616,48,28255,95,12858,10667,12841,23409,27861,8231,30265,31,18615,20483,10841,43,14607,31518,30835,23014,87,19456,29553,104,15832,18495,114,75,119,12338,300,17284,36,8296,30,51,136,94,358,79,12844,131,16563,83,639,100,90,111]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU170+1 : 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.13/0.40 % Computer : n017.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sat Sep 26 08:39:18 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 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.86/0.98 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.25/1.19 % [INFO] Parsing done (205ms).
% 1.42/1.20 % [INFO] Running in sequential loop mode.
% 2.12/1.62 % [INFO] eprover registered as external prover.
% 2.12/1.63 % [INFO] Scanning for conjecture ...
% 2.33/1.74 % [INFO] Found a conjecture (or negated_conjecture) and 26 axioms. Running axiom selection ...
% 2.52/1.81 % [INFO] Axiom selection finished. Selected 22 axioms (removed 4 axioms).
% 2.52/1.85 % [INFO] Problem is first-order (TPTP FOF).
% 2.52/1.86 % [INFO] Type checking passed.
% 2.52/1.87 % [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 ...
% 81.95/19.66 % External prover 'e' found a proof!
% 81.95/19.66 % [INFO] Killing All external provers ...
% 81.95/19.67 % Time passed: 19124ms (effective reasoning time: 18453ms)
% 81.95/19.67 % 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)>
% 81.95/19.67 % Axioms used in derivation (22): fc1_xboole_0, l3_subset_1, involutiveness_k3_subset_1, t4_boole, rc1_subset_1, existence_m1_subset_1, d5_subset_1, d4_xboole_0, symmetry_r1_xboole_0, rc2_xboole_0, t6_boole, rc2_subset_1, t7_boole, fc1_subset_1, d3_tarski, reflexivity_r1_tarski, t8_boole, rc1_xboole_0, t3_xboole_0, t3_boole, dt_k3_subset_1, antisymmetry_r2_hidden
% 81.95/19.67 % No. of inferences in proof: 521
% 81.95/19.67 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 19124 ms resp. 18453 ms w/o parsing
% 83.20/19.90 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 83.20/19.91 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------