%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SET607+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : 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:30:26 AM UTC 2026
% Result : Theorem 254.04s 73.07s
% Output : Refutation 248.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 13
% Syntax : Number of formulae : 546 ( 167 unt; 0 typ; 5 def)
% Number of atoms : 1615 ( 513 equ; 0 cnn)
% Maximal formula atoms : 18 ( 2 avg)
% Number of connectives : 6898 ( 840 ~; 625 |; 37 &;5354 @)
% ( 6 <=>; 36 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 8 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 12 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 1660 ( 6 ^;1649 !; 0 ?;1660 :)
% ( 0 !>; 0 ?*; 0 @-; 5 @+)
% Comments :
%------------------------------------------------------------------------------
thf(union_decl,type,
union: $i > $i > $i ).
thf(difference_decl,type,
difference: $i > $i > $i ).
thf(member_decl,type,
member: $i > $i > $o ).
thf(subset_decl,type,
subset: $i > $i > $o ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i > $i > $i ).
thf(sk4_decl,type,
sk4: $i > $i > $i ).
thf(sk5_decl,type,
sk5: $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i] :
( ( A @ ( B @ difference ) @ ( A @ union ) )
= ( B @ ( A @ union ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
( ( sk1 @ ( A @ difference ) @ ( sk1 @ union ) )
!= ( A @ ( sk1 @ union ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( B @ ( C @ member ) )
=> ( A @ ( C @ member ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( B @ ( C @ member ) )
=> ( A @ ( C @ member ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ) ) ).
thf(6,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ union ) )
= ( A @ ( B @ union ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_union) ).
thf(40,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ union ) )
= ( A @ ( B @ union ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(41,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ union ) )
= ( A @ ( B @ union ) ) ),
inference(cnf,[status(esa)],[40]) ).
thf(42,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ union ) )
= ( A @ ( B @ union ) ) ),
inference(lifteq,[status(thm)],[41]) ).
thf(7,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
<=> ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subset_defn) ).
thf(43,plain,
! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) )
=> ( B @ ( A @ subset ) ) )
& ( ( B @ ( A @ subset ) )
=> ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(44,plain,
( ! [A: $i,B: $i] :
( ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) )
=> ( B @ ( A @ subset ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ subset ) )
=> ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[43]) ).
thf(45,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( D @ subset ) )
| ~ ( E @ ( D @ ( E @ sk3 ) @ member ) ) )
& ( ( E @ ( D @ subset ) )
| ( D @ ( D @ ( E @ sk3 ) @ member ) ) )
& ( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ subset ) ) ) ),
inference(cnf,[status(esa)],[44]) ).
thf(47,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ( A @ ( A @ ( B @ sk3 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[45]) ).
thf(49,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ( A @ ( A @ ( B @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[47]) ).
thf(3,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ union ) @ ( C @ member ) )
<=> ( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',union_defn) ).
thf(13,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) ) )
=> ( B @ ( A @ union ) @ ( C @ member ) ) )
& ( ( B @ ( A @ union ) @ ( C @ member ) )
=> ( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(14,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) ) )
=> ( B @ ( A @ union ) @ ( C @ member ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ union ) @ ( C @ member ) )
=> ( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[13]) ).
thf(15,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( D @ union ) @ ( F @ member ) )
| ~ ( E @ ( F @ member ) ) )
& ( ( E @ ( D @ union ) @ ( F @ member ) )
| ~ ( D @ ( F @ member ) ) )
& ( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) )
| ~ ( B @ ( A @ union ) @ ( C @ member ) ) ) ),
inference(cnf,[status(esa)],[14]) ).
thf(17,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ union ) @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(cnfConj,[status(thm)],[15]) ).
thf(19,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ union ) @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[17]) ).
thf(160,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( C @ ( E @ member ) ) )
| ( D @ ( C @ union ) @ ( E @ member ) )
| ~ $true
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[49,19]) ).
thf(161,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( C @ ( E @ member ) ) )
| ( D @ ( C @ union ) @ ( E @ member ) )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[160]) ).
thf(162,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ union ) @ ( C @ ( B @ sk3 ) @ member ) )
| ( B @ ( C @ subset ) ) ),
inference(pattern_uni,[status(thm)],[161:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( G )),bind(D,$thf( D )),bind(E,$thf( G @ ( F @ sk3 ) ))]]) ).
thf(175,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ union ) @ ( C @ ( B @ sk3 ) @ member ) )
| ( B @ ( C @ subset ) ) ),
inference(simp,[status(thm)],[162]) ).
thf(5,axiom,
! [A: $i,B: $i] :
( ( A = B )
<=> ( ( A @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equal_defn) ).
thf(28,plain,
! [A: $i,B: $i] :
( ( ( ( A @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( A = B ) )
& ( ( A = B )
=> ( ( A @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(29,plain,
( ! [A: $i,B: $i] :
( ( ( A @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) )
=> ( A = B ) )
& ! [A: $i,B: $i] :
( ( A = B )
=> ( ( A @ ( B @ subset ) )
& ( B @ ( A @ subset ) ) ) ) ),
inference(miniscope,[status(thm)],[28]) ).
thf(30,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C = D )
| ~ ( C @ ( D @ subset ) )
| ~ ( D @ ( C @ subset ) ) )
& ( ( A @ ( B @ subset ) )
| ( A != B ) )
& ( ( B @ ( A @ subset ) )
| ( A != B ) ) ),
inference(cnf,[status(esa)],[29]) ).
thf(33,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnfConj,[status(thm)],[30]) ).
thf(38,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ subset ) )
| ~ ( B @ ( A @ subset ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[33]) ).
thf(39,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ subset ) )
| ~ ( B @ ( A @ subset ) )
| ( A = B ) ),
inference(simp,[status(thm)],[38]) ).
thf(1,conjecture,
! [A: $i,B: $i] :
( ( A @ ( B @ difference ) @ ( A @ union ) )
= ( B @ ( A @ union ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_th79) ).
thf(2,negated_conjecture,
~ ! [A: $i,B: $i] :
( ( A @ ( B @ difference ) @ ( A @ union ) )
= ( B @ ( A @ union ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(10,plain,
~ ! [A: $i,B: $i] :
( ( A @ ( B @ difference ) @ ( A @ union ) )
= ( B @ ( A @ union ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(11,plain,
( ( sk1 @ ( sk2 @ difference ) @ ( sk1 @ union ) )
!= ( sk2 @ ( sk1 @ union ) ) ),
inference(cnf,[status(esa)],[10]) ).
thf(12,plain,
( ( sk1 @ ( sk2 @ difference ) @ ( sk1 @ union ) )
!= ( sk2 @ ( sk1 @ union ) ) ),
inference(lifteq,[status(thm)],[11]) ).
thf(74,plain,
( ( ( sk1 @ ( sk2 @ difference ) )
!= sk2 )
| ( sk1 != sk1 ) ),
inference(simp,[status(thm)],[12]) ).
thf(75,plain,
( ( sk1 @ ( sk2 @ difference ) )
!= sk2 ),
inference(simp,[status(thm)],[74]) ).
thf(604,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk1 @ ( sk2 @ difference ) ) )
| ( B != sk2 )
| ~ ( A @ ( B @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[39,75]) ).
thf(605,plain,
! [A: $i] :
( ( A != sk2 )
| ~ ( sk1 @ ( sk2 @ difference ) @ ( A @ subset ) )
| ~ ( A @ ( sk1 @ ( sk2 @ difference ) @ subset ) ) ),
inference(pattern_uni,[status(thm)],[604:[bind(A,$thf( sk1 @ ( sk2 @ difference ) )),bind(B,$thf( B ))]]) ).
thf(804,plain,
( ~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) )
| ~ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ subset ) ) ),
inference(simp,[status(thm)],[605]) ).
thf(857,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subset ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ subset ) ) )
| ~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) )
| ~ $true
| ( A @ ( A @ ( B @ sk3 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[49,804]) ).
thf(858,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subset ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ subset ) ) )
| ~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) )
| ( A @ ( A @ ( B @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[857]) ).
thf(859,plain,
( ~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) )
| ( sk1 @ ( sk2 @ difference ) @ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ sk3 ) @ member ) ) ),
inference(pattern_uni,[status(thm)],[858:[bind(A,$thf( sk1 @ ( sk2 @ difference ) )),bind(B,$thf( sk2 ))]]) ).
thf(4,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ difference ) @ ( C @ member ) )
<=> ( ~ ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',difference_defn) ).
thf(21,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ~ ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) )
=> ( B @ ( A @ difference ) @ ( C @ member ) ) )
& ( ( B @ ( A @ difference ) @ ( C @ member ) )
=> ( ~ ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(22,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ~ ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) )
=> ( B @ ( A @ difference ) @ ( C @ member ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ difference ) @ ( C @ member ) )
=> ( ~ ( B @ ( C @ member ) )
& ( A @ ( C @ member ) ) ) ) ),
inference(miniscope,[status(thm)],[21]) ).
thf(23,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( D @ difference ) @ ( F @ member ) )
| ( E @ ( F @ member ) )
| ~ ( D @ ( F @ member ) ) )
& ( ~ ( B @ ( C @ member ) )
| ~ ( B @ ( A @ difference ) @ ( C @ member ) ) )
& ( ( A @ ( C @ member ) )
| ~ ( B @ ( A @ difference ) @ ( C @ member ) ) ) ),
inference(cnf,[status(esa)],[22]) ).
thf(24,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ member ) )
| ~ ( B @ ( A @ difference ) @ ( C @ member ) ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(8542,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ difference ) @ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ sk3 ) @ member ) )
!= ( B @ ( A @ difference ) @ ( C @ member ) ) )
| ( A @ ( C @ member ) )
| ~ $true
| ~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[859,24]) ).
thf(8543,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ difference ) @ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ sk3 ) @ member ) )
!= ( B @ ( A @ difference ) @ ( C @ member ) ) )
| ( A @ ( C @ member ) )
| ~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[8542]) ).
thf(8544,plain,
( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ sk3 ) @ member ) )
| ~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[8543:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 )),bind(C,$thf( sk1 @ ( sk2 @ difference ) @ ( sk2 @ sk3 ) ))]]) ).
thf(48,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ~ ( B @ ( A @ ( B @ sk3 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[45]) ).
thf(50,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ~ ( B @ ( A @ ( B @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[48]) ).
thf(899,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subset ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ subset ) ) )
| ~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) )
| ~ $true
| ~ ( B @ ( A @ ( B @ sk3 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[50,804]) ).
thf(900,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subset ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ subset ) ) )
| ~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) )
| ~ ( B @ ( A @ ( B @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[899]) ).
thf(901,plain,
( ~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) )
| ~ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ sk3 ) @ member ) ) ),
inference(pattern_uni,[status(thm)],[900:[bind(A,$thf( sk1 @ ( sk2 @ difference ) )),bind(B,$thf( sk2 ))]]) ).
thf(9026,plain,
( ( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ sk3 ) @ member ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ sk3 ) @ member ) ) )
| ~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) )
| ~ $true
| ~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[8544,901]) ).
thf(9027,plain,
( ( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ sk3 ) @ member ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ sk3 ) @ member ) ) )
| ~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[9026]) ).
thf(9028,plain,
~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ),
inference(pattern_uni,[status(thm)],[9027:[]]) ).
thf(9379,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true
| ( A @ ( C @ union ) @ ( C @ ( B @ sk3 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[175,9028]) ).
thf(9380,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ( A @ ( C @ union ) @ ( C @ ( B @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[9379]) ).
thf(9381,plain,
! [A: $i] : ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(pattern_uni,[status(thm)],[9380:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ( sk2 @ difference ) )),bind(C,$thf( sk2 ))]]) ).
thf(9339,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true
| ( A @ ( A @ ( B @ sk3 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[49,9028]) ).
thf(9340,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ( A @ ( A @ ( B @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[9339]) ).
thf(9341,plain,
sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ),
inference(pattern_uni,[status(thm)],[9340:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 @ ( sk2 @ difference ) ))]]) ).
thf(25,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ member ) )
| ~ ( B @ ( A @ difference ) @ ( C @ member ) ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(94,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( F @ member ) ) )
| ~ $true
| ~ ( E @ ( D @ difference ) @ ( F @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[19,25]) ).
thf(95,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( F @ member ) ) )
| ~ ( E @ ( D @ difference ) @ ( F @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[94]) ).
thf(96,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( C @ union ) @ ( B @ difference ) @ ( A @ member ) )
| ~ ( C @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[95:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( H @ ( G @ union ) )),bind(F,$thf( C ))]]) ).
thf(98,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( C @ union ) @ ( B @ difference ) @ ( A @ member ) )
| ~ ( C @ ( A @ member ) ) ),
inference(simp,[status(thm)],[96]) ).
thf(9862,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( A @ member ) ) )
| ~ ( D @ ( C @ union ) @ ( B @ difference ) @ ( A @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9341,98]) ).
thf(9863,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( A @ member ) ) )
| ~ ( D @ ( C @ union ) @ ( B @ difference ) @ ( A @ member ) ) ),
inference(simp,[status(thm)],[9862]) ).
thf(9864,plain,
! [B: $i,A: $i] :
~ ( B @ ( sk2 @ union ) @ ( A @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(pattern_uni,[status(thm)],[9863:[bind(A,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )),bind(B,$thf( B )),bind(C,$thf( sk2 )),bind(D,$thf( D ))]]) ).
thf(9919,plain,
! [B: $i,A: $i] :
~ ( B @ ( sk2 @ union ) @ ( A @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(simp,[status(thm)],[9864]) ).
thf(14720,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( sk2 @ union ) @ ( B @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9381,9919]) ).
thf(14721,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( sk2 @ union ) @ ( B @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[14720]) ).
thf(14765,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ union ) )
!= ( C @ ( sk2 @ union ) @ ( B @ difference ) ) )
| ( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ) ) ),
inference(simp,[status(thm)],[14721]) ).
thf(14846,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ union ) )
!= ( C @ ( sk2 @ union ) @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[14765]) ).
thf(14913,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( E @ ( sk2 @ union ) ) )
| ( ( A @ ( B @ union ) @ ( D @ difference ) )
!= ( C @ ( sk2 @ union ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,14846]) ).
thf(14914,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( C @ difference ) )
!= ( B @ ( sk2 @ union ) ) ),
inference(pattern_uni,[status(thm)],[14913:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( B ))]]) ).
thf(15002,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( C @ difference ) )
!= ( B @ ( sk2 @ union ) ) ),
inference(simp,[status(thm)],[14914]) ).
thf(18,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ union ) @ ( C @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(cnfConj,[status(thm)],[15]) ).
thf(20,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ union ) @ ( C @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[18]) ).
thf(154,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( D @ ( E @ member ) ) )
| ( D @ ( C @ union ) @ ( E @ member ) )
| ~ $true
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[49,20]) ).
thf(155,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( D @ ( E @ member ) ) )
| ( D @ ( C @ union ) @ ( E @ member ) )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[154]) ).
thf(156,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ union ) @ ( C @ ( B @ sk3 ) @ member ) )
| ( B @ ( C @ subset ) ) ),
inference(pattern_uni,[status(thm)],[155:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( C )),bind(D,$thf( G )),bind(E,$thf( G @ ( F @ sk3 ) ))]]) ).
thf(179,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ union ) @ ( C @ ( B @ sk3 ) @ member ) )
| ( B @ ( C @ subset ) ) ),
inference(simp,[status(thm)],[156]) ).
thf(9281,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true
| ( C @ ( A @ union ) @ ( C @ ( B @ sk3 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[179,9028]) ).
thf(9282,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ( C @ ( A @ union ) @ ( C @ ( B @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[9281]) ).
thf(9283,plain,
! [A: $i] : ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(pattern_uni,[status(thm)],[9282:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ( sk2 @ difference ) )),bind(C,$thf( sk2 ))]]) ).
thf(14639,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( sk2 @ union ) @ ( B @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9283,9919]) ).
thf(14640,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( sk2 @ union ) @ ( B @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[14639]) ).
thf(14774,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ union ) )
!= ( C @ ( sk2 @ union ) @ ( B @ difference ) ) )
| ( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ) ) ),
inference(simp,[status(thm)],[14640]) ).
thf(14852,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ union ) )
!= ( C @ ( sk2 @ union ) @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[14774]) ).
thf(128,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( D @ ( C @ union ) ) )
| ( A @ ( B @ union ) @ ( E @ member ) )
| ~ ( D @ ( E @ member ) ) ),
inference(paramod_ordered,[status(thm)],[42,20]) ).
thf(129,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ union ) @ ( C @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(pattern_uni,[status(thm)],[128:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(138,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ union ) @ ( C @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[129]) ).
thf(76,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ( ( B @ ( A @ difference ) @ ( C @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ ( B @ ( C @ member ) ) ),
inference(eqfactor_ordered,[status(thm)],[25]) ).
thf(78,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) )
!= B )
| ( C != C )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[76]) ).
thf(79,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) )
!= B )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[78]) ).
thf(85,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( F @ member ) ) )
| ( ( E @ ( D @ difference ) )
!= E )
| ~ $true
| ~ ( A @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[19,79]) ).
thf(86,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( F @ member ) ) )
| ( ( E @ ( D @ difference ) )
!= E )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[85]) ).
thf(87,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ union ) @ ( B @ difference ) )
!= ( D @ ( C @ union ) ) )
| ~ ( C @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[86:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( H @ ( G @ union ) )),bind(F,$thf( C ))]]) ).
thf(101,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ union ) @ ( B @ difference ) )
!= ( D @ ( C @ union ) ) )
| ~ ( C @ ( A @ member ) ) ),
inference(simp,[status(thm)],[87]) ).
thf(10805,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ( ( C @ ( B @ difference ) )
!= C )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9283,79]) ).
thf(10806,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ( ( C @ ( B @ difference ) )
!= C ) ),
inference(simp,[status(thm)],[10805]) ).
thf(10807,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( B @ union ) @ ( A @ difference ) )
!= ( sk2 @ ( B @ union ) ) ),
inference(pattern_uni,[status(thm)],[10806:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( sk2 @ ( I @ union ) )),bind(D,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ))]]) ).
thf(10862,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( B @ union ) @ ( A @ difference ) )
!= ( sk2 @ ( B @ union ) ) ),
inference(simp,[status(thm)],[10807]) ).
thf(12884,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( sk2 @ ( D @ union ) ) )
| ( ( A @ ( B @ union ) @ ( C @ difference ) )
!= ( sk2 @ ( D @ union ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,10862]) ).
thf(12885,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( B @ difference ) )
!= ( sk2 @ ( A @ union ) ) ),
inference(pattern_uni,[status(thm)],[12884:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(12934,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( B @ difference ) )
!= ( sk2 @ ( A @ union ) ) ),
inference(simp,[status(thm)],[12885]) ).
thf(202,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( D @ ( C @ union ) @ ( B @ difference ) @ ( A @ member ) )
!= ( C @ ( A @ member ) ) )
| ~ ( C @ ( A @ member ) ) ),
inference(eqfactor_ordered,[status(thm)],[98]) ).
thf(204,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ union ) @ ( B @ difference ) )
!= C )
| ( A != A )
| ~ ( C @ ( A @ member ) ) ),
inference(simp,[status(thm)],[202]) ).
thf(210,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ union ) @ ( B @ difference ) )
!= C )
| ~ ( C @ ( A @ member ) ) ),
inference(simp,[status(thm)],[204]) ).
thf(222,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ union ) )
!= ( F @ ( E @ union ) ) )
| ( ( B @ ( A @ union ) @ ( D @ difference ) )
!= E )
| ~ ( E @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[42,210]) ).
thf(223,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( D @ difference ) )
!= B )
| ~ ( B @ ( C @ member ) ) ),
inference(pattern_uni,[status(thm)],[222:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( B )),bind(F,$thf( A ))]]) ).
thf(9867,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ( ( B @ ( A @ union ) @ ( D @ difference ) )
!= B )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9341,223]) ).
thf(9868,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ( ( B @ ( A @ union ) @ ( D @ difference ) )
!= B ) ),
inference(simp,[status(thm)],[9867]) ).
thf(9869,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( B @ difference ) )
!= sk2 ),
inference(pattern_uni,[status(thm)],[9868:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )),bind(D,$thf( D ))]]) ).
thf(9921,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( B @ difference ) )
!= sk2 ),
inference(simp,[status(thm)],[9869]) ).
thf(10436,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( sk2 @ ( C @ union ) ) )
| ( ( A @ ( B @ union ) @ ( D @ difference ) )
!= sk2 ) ),
inference(paramod_ordered,[status(thm)],[42,9921]) ).
thf(10437,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( B @ difference ) )
!= sk2 ),
inference(pattern_uni,[status(thm)],[10436:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( A ))]]) ).
thf(10478,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( B @ difference ) )
!= sk2 ),
inference(simp,[status(thm)],[10437]) ).
thf(10799,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( B @ ( D @ member ) ) )
| ( C @ ( B @ union ) @ ( D @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9283,19]) ).
thf(10800,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( B @ ( D @ member ) ) )
| ( C @ ( B @ union ) @ ( D @ member ) ) ),
inference(simp,[status(thm)],[10799]) ).
thf(10801,plain,
! [B: $i,A: $i] : ( A @ ( sk2 @ ( B @ union ) @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(pattern_uni,[status(thm)],[10800:[bind(A,$thf( I )),bind(B,$thf( sk2 @ ( I @ union ) )),bind(C,$thf( C )),bind(D,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ))]]) ).
thf(10858,plain,
! [B: $i,A: $i] : ( A @ ( sk2 @ ( B @ union ) @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(simp,[status(thm)],[10801]) ).
thf(9360,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true
| ~ ( B @ ( A @ ( B @ sk3 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[50,9028]) ).
thf(9361,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ ( B @ ( A @ ( B @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[9360]) ).
thf(9362,plain,
~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(pattern_uni,[status(thm)],[9361:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 @ ( sk2 @ difference ) ))]]) ).
thf(19537,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk2 @ ( B @ union ) @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[10858,9362]) ).
thf(19538,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ ( B @ union ) @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[19537]) ).
thf(19755,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk2 @ ( B @ union ) @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) )
| ( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ) ) ),
inference(simp,[status(thm)],[19538]) ).
thf(19793,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ ( B @ union ) @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(simp,[status(thm)],[19755]) ).
thf(19908,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( C @ ( sk2 @ ( D @ union ) @ union ) ) )
| ( ( A @ ( B @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,19793]) ).
thf(19909,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( B @ union ) @ ( A @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(pattern_uni,[status(thm)],[19908:[bind(A,$thf( sk2 @ ( E @ union ) )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( E ))]]) ).
thf(20046,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( B @ union ) @ ( A @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(simp,[status(thm)],[19909]) ).
thf(172,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( D @ ( E @ member ) ) )
| ~ $true
| ~ ( D @ ( C @ difference ) @ ( E @ member ) )
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[49,25]) ).
thf(173,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( D @ ( E @ member ) ) )
| ~ ( D @ ( C @ difference ) @ ( E @ member ) )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[172]) ).
thf(174,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ difference ) @ ( C @ ( B @ sk3 ) @ member ) )
| ( B @ ( C @ subset ) ) ),
inference(pattern_uni,[status(thm)],[173:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( C )),bind(D,$thf( G )),bind(E,$thf( G @ ( F @ sk3 ) ))]]) ).
thf(180,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ difference ) @ ( C @ ( B @ sk3 ) @ member ) )
| ( B @ ( C @ subset ) ) ),
inference(simp,[status(thm)],[174]) ).
thf(166,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( D @ ( C @ difference ) @ ( E @ member ) ) )
| ( C @ ( E @ member ) )
| ~ $true
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[49,24]) ).
thf(167,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( D @ ( C @ difference ) @ ( E @ member ) ) )
| ( C @ ( E @ member ) )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[166]) ).
thf(168,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( B @ difference ) @ ( A @ sk3 ) @ member ) )
| ( A @ ( C @ ( B @ difference ) @ subset ) ) ),
inference(pattern_uni,[status(thm)],[167:[bind(A,$thf( I @ ( H @ difference ) )),bind(B,$thf( F )),bind(C,$thf( H )),bind(D,$thf( I )),bind(E,$thf( I @ ( H @ difference ) @ ( F @ sk3 ) ))]]) ).
thf(177,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( B @ difference ) @ ( A @ sk3 ) @ member ) )
| ( A @ ( C @ ( B @ difference ) @ subset ) ) ),
inference(simp,[status(thm)],[168]) ).
thf(23693,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ ( B @ difference ) @ ( A @ sk3 ) @ member ) )
!= ( E @ ( D @ ( E @ sk3 ) @ member ) ) )
| ( E @ ( D @ subset ) )
| ~ $true
| ( A @ ( C @ ( B @ difference ) @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[177,50]) ).
thf(23694,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ ( B @ difference ) @ ( A @ sk3 ) @ member ) )
!= ( E @ ( D @ ( E @ sk3 ) @ member ) ) )
| ( E @ ( D @ subset ) )
| ( A @ ( C @ ( B @ difference ) @ subset ) ) ),
inference(simp,[status(thm)],[23693]) ).
thf(23695,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ difference ) @ subset ) )
| ( A @ ( B @ ( A @ difference ) @ subset ) ) ),
inference(pattern_uni,[status(thm)],[23694:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( G )),bind(D,$thf( G @ ( F @ difference ) )),bind(E,$thf( F ))]]) ).
thf(23772,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ difference ) @ subset ) ),
inference(simp,[status(thm)],[23695]) ).
thf(163,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( D @ ( E @ member ) ) )
| ( ( D @ ( C @ difference ) )
!= D )
| ~ $true
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[49,79]) ).
thf(164,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( D @ ( E @ member ) ) )
| ( ( D @ ( C @ difference ) )
!= D )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[163]) ).
thf(165,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ difference ) )
!= C )
| ( B @ ( C @ subset ) ) ),
inference(pattern_uni,[status(thm)],[164:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( C )),bind(D,$thf( G )),bind(E,$thf( G @ ( F @ sk3 ) ))]]) ).
thf(176,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ difference ) )
!= C )
| ( B @ ( C @ subset ) ) ),
inference(simp,[status(thm)],[165]) ).
thf(9320,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true
| ( ( C @ ( A @ difference ) )
!= C ) ),
inference(paramod_ordered,[status(thm)],[176,9028]) ).
thf(9321,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ( ( C @ ( A @ difference ) )
!= C ) ),
inference(simp,[status(thm)],[9320]) ).
thf(9322,plain,
! [A: $i] :
( ( sk2 @ ( A @ difference ) )
!= sk2 ),
inference(pattern_uni,[status(thm)],[9321:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ( sk2 @ difference ) )),bind(C,$thf( sk2 ))]]) ).
thf(9440,plain,
! [C: $i,B: $i,A: $i] :
( ( B
!= ( sk2 @ ( C @ difference ) ) )
| ( A != sk2 )
| ~ ( A @ ( B @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[39,9322]) ).
thf(9441,plain,
! [B: $i,A: $i] :
( ( A != sk2 )
| ~ ( A @ ( sk2 @ ( B @ difference ) @ subset ) )
| ~ ( sk2 @ ( B @ difference ) @ ( A @ subset ) ) ),
inference(pattern_uni,[status(thm)],[9440:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ( D @ difference ) )),bind(C,$thf( D ))]]) ).
thf(9452,plain,
! [A: $i] :
( ~ ( sk2 @ ( sk2 @ ( A @ difference ) @ subset ) )
| ~ ( sk2 @ ( A @ difference ) @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[9441]) ).
thf(29012,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ difference ) @ subset ) )
!= ( sk2 @ ( sk2 @ ( C @ difference ) @ subset ) ) )
| ~ $true
| ~ ( sk2 @ ( C @ difference ) @ ( sk2 @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[23772,9452]) ).
thf(29013,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ difference ) @ subset ) )
!= ( sk2 @ ( sk2 @ ( C @ difference ) @ subset ) ) )
| ~ ( sk2 @ ( C @ difference ) @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[29012]) ).
thf(29014,plain,
~ ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ),
inference(pattern_uni,[status(thm)],[29013:[bind(A,$thf( sk2 )),bind(B,$thf( sk2 )),bind(C,$thf( sk2 ))]]) ).
thf(29315,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true
| ~ ( C @ ( A @ difference ) @ ( C @ ( B @ sk3 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[180,29014]) ).
thf(29316,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ ( C @ ( A @ difference ) @ ( C @ ( B @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[29315]) ).
thf(29317,plain,
! [A: $i] :
~ ( sk2 @ ( A @ difference ) @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(pattern_uni,[status(thm)],[29316:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ( sk2 @ difference ) )),bind(C,$thf( sk2 ))]]) ).
thf(9,axiom,
! [A: $i,B: $i] :
( ( A = B )
<=> ! [C: $i] :
( ( A @ ( C @ member ) )
<=> ( B @ ( C @ member ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equal_member_defn) ).
thf(53,plain,
! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( ( B @ ( C @ member ) )
=> ( A @ ( C @ member ) ) )
& ( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) )
=> ( A = B ) )
& ( ( A = B )
=> ! [C: $i] :
( ( ( B @ ( C @ member ) )
=> ( A @ ( C @ member ) ) )
& ( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(54,plain,
( ! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( B @ ( C @ member ) )
=> ( A @ ( C @ member ) ) )
& ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) )
=> ( A = B ) )
& ! [A: $i,B: $i] :
( ( A = B )
=> ( ! [C: $i] :
( ( B @ ( C @ member ) )
=> ( A @ ( C @ member ) ) )
& ! [C: $i] :
( ( A @ ( C @ member ) )
=> ( B @ ( C @ member ) ) ) ) ) ),
inference(miniscope,[status(thm)],[53]) ).
thf(55,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E = F )
| ~ ( E @ ( E @ ( F @ sk5 ) @ member ) )
| ~ ( F @ ( E @ ( F @ sk4 ) @ member ) ) )
& ( ( E = F )
| ( F @ ( E @ ( F @ sk5 ) @ member ) )
| ~ ( F @ ( E @ ( F @ sk4 ) @ member ) ) )
& ( ( E = F )
| ~ ( E @ ( E @ ( F @ sk5 ) @ member ) )
| ( E @ ( E @ ( F @ sk4 ) @ member ) ) )
& ( ( E = F )
| ( F @ ( E @ ( F @ sk5 ) @ member ) )
| ( E @ ( E @ ( F @ sk4 ) @ member ) ) )
& ( ( A @ ( D @ member ) )
| ~ ( B @ ( D @ member ) )
| ( A != B ) )
& ( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ( A != B ) ) ),
inference(cnf,[status(esa)],[54]) ).
thf(59,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( B @ ( A @ ( B @ sk5 ) @ member ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[55]) ).
thf(70,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ sk5 ) @ member ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[59]) ).
thf(71,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ sk5 ) @ member ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) )
| ( A = B ) ),
inference(simp,[status(thm)],[70]) ).
thf(31,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ( A != B ) ),
inference(cnfConj,[status(thm)],[30]) ).
thf(34,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ subset ) )
| ( A != B ) ),
inference(lifteq,[status(thm)],[31]) ).
thf(35,plain,
! [A: $i] : ( A @ ( A @ subset ) ),
inference(simp,[status(thm)],[34]) ).
thf(29358,plain,
! [A: $i] :
( ( ( A @ ( A @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,29014]) ).
thf(29359,plain,
! [A: $i] :
( ( A @ ( A @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[29358]) ).
thf(29393,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk2 @ difference ) ) )
| ( A != sk2 ) ),
inference(simp,[status(thm)],[29359]) ).
thf(29414,plain,
( ( sk2 @ ( sk2 @ difference ) )
!= sk2 ),
inference(simp,[status(thm)],[29393]) ).
thf(29799,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk2 @ ( sk2 @ difference ) ) )
| ( B != sk2 )
| ( B @ ( A @ ( B @ sk5 ) @ member ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[71,29414]) ).
thf(29800,plain,
! [A: $i] :
( ( A != sk2 )
| ( A @ ( sk2 @ ( sk2 @ difference ) @ ( A @ sk5 ) @ member ) )
| ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ ( sk2 @ difference ) @ ( A @ sk4 ) @ member ) ) ),
inference(pattern_uni,[status(thm)],[29799:[bind(A,$thf( sk2 @ ( sk2 @ difference ) )),bind(B,$thf( B ))]]) ).
thf(29847,plain,
( ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ sk5 ) @ member ) )
| ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[29800]) ).
thf(148,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( D @ difference ) @ ( F @ member ) ) )
| ( D @ ( F @ member ) )
| ~ $true
| ~ ( A @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[19,24]) ).
thf(149,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( D @ difference ) @ ( F @ member ) ) )
| ( D @ ( F @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[148]) ).
thf(151,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( E @ ( D @ difference ) ) )
| ( C != F )
| ~ ( A @ ( C @ member ) )
| ( D @ ( F @ member ) ) ),
inference(simp,[status(thm)],[149]) ).
thf(153,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( D @ ( C @ difference ) ) )
| ~ ( A @ ( E @ member ) )
| ( C @ ( E @ member ) ) ),
inference(simp,[status(thm)],[151]) ).
thf(119,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( D @ ( F @ member ) ) )
| ( E @ ( D @ union ) @ ( F @ member ) )
| ~ $true
| ~ ( B @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[20,19]) ).
thf(120,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( D @ ( F @ member ) ) )
| ( E @ ( D @ union ) @ ( F @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[119]) ).
thf(121,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ ( C @ union ) @ union ) @ ( A @ member ) )
| ~ ( D @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[120:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ union ) )),bind(E,$thf( E )),bind(F,$thf( C ))]]) ).
thf(142,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ ( C @ union ) @ union ) @ ( A @ member ) )
| ~ ( D @ ( A @ member ) ) ),
inference(simp,[status(thm)],[121]) ).
thf(29337,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true
| ( A @ ( A @ ( B @ sk3 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[49,29014]) ).
thf(29338,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ( A @ ( A @ ( B @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[29337]) ).
thf(29339,plain,
sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk3 ) @ member ),
inference(pattern_uni,[status(thm)],[29338:[bind(A,$thf( sk2 )),bind(B,$thf( sk2 @ ( sk2 @ difference ) ))]]) ).
thf(15075,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( E @ ( sk2 @ union ) ) )
| ( ( A @ ( B @ union ) @ ( D @ difference ) )
!= ( sk2 @ ( C @ union ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,14852]) ).
thf(15076,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( C @ difference ) )
!= ( sk2 @ ( B @ union ) ) ),
inference(pattern_uni,[status(thm)],[15075:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( B ))]]) ).
thf(15181,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( C @ difference ) )
!= ( sk2 @ ( B @ union ) ) ),
inference(simp,[status(thm)],[15076]) ).
thf(15968,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( sk2 @ ( C @ union ) ) )
| ( ( A @ ( B @ union ) @ ( E @ difference ) )
!= ( sk2 @ ( D @ union ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,15181]) ).
thf(15969,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( C @ difference ) )
!= ( sk2 @ ( B @ union ) ) ),
inference(pattern_uni,[status(thm)],[15968:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( A ))]]) ).
thf(16074,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( C @ difference ) )
!= ( sk2 @ ( B @ union ) ) ),
inference(simp,[status(thm)],[15969]) ).
thf(18264,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( sk2 @ ( D @ union ) ) )
| ( ( A @ ( B @ union ) )
!= ( C @ ( sk2 @ union ) @ ( E @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,16074]) ).
thf(18265,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ union ) )
!= ( B @ ( sk2 @ union ) @ ( C @ difference ) ) ),
inference(pattern_uni,[status(thm)],[18264:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(18384,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ union ) )
!= ( B @ ( sk2 @ union ) @ ( C @ difference ) ) ),
inference(simp,[status(thm)],[18265]) ).
thf(279,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ union ) @ ( C @ ( B @ sk3 ) @ member ) )
!= ( E @ ( D @ ( E @ sk3 ) @ member ) ) )
| ( E @ ( D @ subset ) )
| ~ $true
| ( B @ ( C @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[175,50]) ).
thf(280,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ union ) @ ( C @ ( B @ sk3 ) @ member ) )
!= ( E @ ( D @ ( E @ sk3 ) @ member ) ) )
| ( E @ ( D @ subset ) )
| ( B @ ( C @ subset ) ) ),
inference(simp,[status(thm)],[279]) ).
thf(281,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ union ) @ ( A @ subset ) )
| ( B @ ( A @ union ) @ ( A @ subset ) ) ),
inference(pattern_uni,[status(thm)],[280:[bind(A,$thf( G )),bind(B,$thf( G @ ( F @ union ) )),bind(C,$thf( F )),bind(D,$thf( F )),bind(E,$thf( G @ ( F @ union ) ))]]) ).
thf(289,plain,
! [B: $i,A: $i] : ( B @ ( A @ union ) @ ( A @ subset ) ),
inference(simp,[status(thm)],[281]) ).
thf(292,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( D @ ( C @ union ) ) )
| ( A @ ( B @ union ) @ ( C @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[42,289]) ).
thf(293,plain,
! [B: $i,A: $i] : ( A @ ( B @ union ) @ ( A @ subset ) ),
inference(pattern_uni,[status(thm)],[292:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(9318,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ union ) @ ( A @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[293,9028]) ).
thf(9319,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ union ) @ ( A @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[9318]) ).
thf(9385,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) )
| ( A != sk2 ) ),
inference(simp,[status(thm)],[9319]) ).
thf(9396,plain,
! [A: $i] :
( ( sk2 @ ( A @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(simp,[status(thm)],[9385]) ).
thf(9794,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ ( A @ difference ) @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[9341,25]) ).
thf(9795,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ ( B @ ( A @ difference ) @ ( C @ member ) ) ),
inference(simp,[status(thm)],[9794]) ).
thf(9796,plain,
! [A: $i] :
~ ( sk2 @ ( A @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(pattern_uni,[status(thm)],[9795:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ))]]) ).
thf(11638,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( B @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9381,9796]) ).
thf(11639,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( B @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[11638]) ).
thf(11683,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk2 @ union ) )
!= ( sk2 @ ( B @ difference ) ) )
| ( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ) ) ),
inference(simp,[status(thm)],[11639]) ).
thf(11720,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ union ) )
!= ( sk2 @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[11683]) ).
thf(11385,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( B @ ( D @ member ) ) )
| ( C @ ( B @ union ) @ ( D @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9381,19]) ).
thf(11386,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( B @ ( D @ member ) ) )
| ( C @ ( B @ union ) @ ( D @ member ) ) ),
inference(simp,[status(thm)],[11385]) ).
thf(11387,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( sk2 @ union ) @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(pattern_uni,[status(thm)],[11386:[bind(A,$thf( J )),bind(B,$thf( J @ ( sk2 @ union ) )),bind(C,$thf( C )),bind(D,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ))]]) ).
thf(11453,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( sk2 @ union ) @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(simp,[status(thm)],[11387]) ).
thf(46,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(cnfConj,[status(thm)],[45]) ).
thf(20100,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( sk2 @ ( D @ union ) ) )
| ( ( A @ ( B @ union ) @ ( C @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,20046]) ).
thf(20101,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( B @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(pattern_uni,[status(thm)],[20100:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(20206,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( B @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(simp,[status(thm)],[20101]) ).
thf(146,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( D @ difference ) @ ( F @ member ) ) )
| ( D @ ( F @ member ) )
| ~ $true
| ~ ( B @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[20,24]) ).
thf(147,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( D @ difference ) @ ( F @ member ) ) )
| ( D @ ( F @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[146]) ).
thf(150,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( E @ ( D @ difference ) ) )
| ( C != F )
| ~ ( B @ ( C @ member ) )
| ( D @ ( F @ member ) ) ),
inference(simp,[status(thm)],[147]) ).
thf(152,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( D @ ( C @ difference ) ) )
| ~ ( B @ ( E @ member ) )
| ( C @ ( E @ member ) ) ),
inference(simp,[status(thm)],[150]) ).
thf(187,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( F @ ( D @ member ) ) )
| ~ ( G @ ( F @ union ) @ ( E @ difference ) @ ( D @ member ) )
| ~ $true
| ~ ( A @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[19,98]) ).
thf(188,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( F @ ( D @ member ) ) )
| ~ ( G @ ( F @ union ) @ ( E @ difference ) @ ( D @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[187]) ).
thf(189,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( E @ ( D @ union ) @ union ) @ ( B @ difference ) @ ( A @ member ) )
| ~ ( D @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[188:[bind(A,$thf( H )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( C )),bind(E,$thf( E )),bind(F,$thf( I @ ( H @ union ) ))]]) ).
thf(211,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( E @ ( D @ union ) @ union ) @ ( B @ difference ) @ ( A @ member ) )
| ~ ( D @ ( A @ member ) ) ),
inference(simp,[status(thm)],[189]) ).
thf(29805,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk2 @ ( sk2 @ difference ) ) )
| ( A != sk2 )
| ( B @ ( A @ ( B @ sk5 ) @ member ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[71,29414]) ).
thf(29806,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk2 @ ( sk2 @ difference ) @ ( A @ ( sk2 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
| ( A @ ( A @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(pattern_uni,[status(thm)],[29805:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ( sk2 @ difference ) ))]]) ).
thf(29850,plain,
( ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
| ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[29806]) ).
thf(36079,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
!= ( B @ ( A @ difference ) @ ( C @ member ) ) )
| ( A @ ( C @ member ) )
| ~ $true
| ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[29850,24]) ).
thf(36080,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
!= ( B @ ( A @ difference ) @ ( C @ member ) ) )
| ( A @ ( C @ member ) )
| ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[36079]) ).
thf(36081,plain,
( ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
| ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(pattern_uni,[status(thm)],[36080:[bind(A,$thf( sk2 )),bind(B,$thf( sk2 )),bind(C,$thf( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk5 ) ))]]) ).
thf(61,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( A @ ( B @ sk5 ) @ member ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[55]) ).
thf(66,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( A @ ( B @ sk5 ) @ member ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[61]) ).
thf(67,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( A @ ( B @ sk5 ) @ member ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) )
| ( A = B ) ),
inference(simp,[status(thm)],[66]) ).
thf(37635,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
!= ( A @ ( A @ ( B @ sk5 ) @ member ) ) )
| ~ $true
| ( A @ ( A @ ( B @ sk4 ) @ member ) )
| ( A = B )
| ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[36081,67]) ).
thf(37636,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
!= ( A @ ( A @ ( B @ sk5 ) @ member ) ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) )
| ( A = B )
| ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[37635]) ).
thf(37637,plain,
( ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
| ( ( sk2 @ ( sk2 @ difference ) )
= sk2 )
| ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(pattern_uni,[status(thm)],[37636:[bind(A,$thf( sk2 )),bind(B,$thf( sk2 @ ( sk2 @ difference ) ))]]) ).
thf(37753,plain,
( ( ( sk2 @ ( sk2 @ difference ) )
= sk2 )
| ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[37637]) ).
thf(37829,plain,
sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ),
inference(simplifyReflect,[status(thm)],[37753,9322]) ).
thf(37848,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ ( A @ difference ) @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[37829,25]) ).
thf(37849,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ ( B @ ( A @ difference ) @ ( C @ member ) ) ),
inference(simp,[status(thm)],[37848]) ).
thf(37850,plain,
! [A: $i] :
~ ( sk2 @ ( A @ difference ) @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) ),
inference(pattern_uni,[status(thm)],[37849:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) ))]]) ).
thf(19539,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ ( B @ union ) @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( C @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[10858,9796]) ).
thf(19540,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ ( B @ union ) @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( C @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[19539]) ).
thf(19744,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ ( B @ union ) @ union ) )
!= ( sk2 @ ( C @ difference ) ) )
| ( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ) ) ),
inference(simp,[status(thm)],[19540]) ).
thf(19779,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ ( B @ union ) @ union ) )
!= ( sk2 @ ( C @ difference ) ) ),
inference(simp,[status(thm)],[19744]) ).
thf(21920,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( sk2 @ ( D @ union ) ) )
| ( ( C @ ( A @ ( B @ union ) @ union ) )
!= ( sk2 @ ( E @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,19779]) ).
thf(21921,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( sk2 @ union ) @ union ) )
!= ( sk2 @ ( C @ difference ) ) ),
inference(pattern_uni,[status(thm)],[21920:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(22032,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( sk2 @ union ) @ union ) )
!= ( sk2 @ ( C @ difference ) ) ),
inference(simp,[status(thm)],[21921]) ).
thf(22587,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( C @ ( sk2 @ union ) ) )
| ( ( D @ ( A @ ( B @ union ) @ union ) )
!= ( sk2 @ ( E @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,22032]) ).
thf(22588,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( sk2 @ ( A @ union ) @ union ) )
!= ( sk2 @ ( C @ difference ) ) ),
inference(pattern_uni,[status(thm)],[22587:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(22713,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( sk2 @ ( A @ union ) @ union ) )
!= ( sk2 @ ( C @ difference ) ) ),
inference(simp,[status(thm)],[22588]) ).
thf(220,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( F @ ( E @ union ) ) )
| ( ( A @ ( B @ union ) @ ( D @ difference ) )
!= E )
| ~ ( E @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[42,210]) ).
thf(221,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ union ) @ ( D @ difference ) )
!= A )
| ~ ( A @ ( C @ member ) ) ),
inference(pattern_uni,[status(thm)],[220:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( B ))]]) ).
thf(5199,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk1 @ ( sk2 @ difference ) ) )
| ( A != sk2 )
| ( B @ ( A @ ( B @ sk5 ) @ member ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[71,75]) ).
thf(5200,plain,
! [A: $i] :
( ( A != sk2 )
| ( sk1 @ ( sk2 @ difference ) @ ( A @ ( sk1 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
| ( A @ ( A @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(pattern_uni,[status(thm)],[5199:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ( sk2 @ difference ) ))]]) ).
thf(5851,plain,
( ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
| ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[5200]) ).
thf(13982,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
!= ( B @ ( A @ difference ) @ ( C @ member ) ) )
| ( A @ ( C @ member ) )
| ~ $true
| ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[5851,24]) ).
thf(13983,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
!= ( B @ ( A @ difference ) @ ( C @ member ) ) )
| ( A @ ( C @ member ) )
| ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[13982]) ).
thf(13984,plain,
( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
| ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(pattern_uni,[status(thm)],[13983:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk5 ) ))]]) ).
thf(15355,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
!= ( A @ ( A @ ( B @ sk5 ) @ member ) ) )
| ~ $true
| ( A @ ( A @ ( B @ sk4 ) @ member ) )
| ( A = B )
| ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[13984,67]) ).
thf(15356,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
!= ( A @ ( A @ ( B @ sk5 ) @ member ) ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) )
| ( A = B )
| ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[15355]) ).
thf(15357,plain,
( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
| ( ( sk1 @ ( sk2 @ difference ) )
= sk2 )
| ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(pattern_uni,[status(thm)],[15356:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 @ ( sk2 @ difference ) ))]]) ).
thf(15474,plain,
( ( ( sk1 @ ( sk2 @ difference ) )
= sk2 )
| ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[15357]) ).
thf(16253,plain,
sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ),
inference(simplifyReflect,[status(thm)],[15474,75]) ).
thf(16314,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ( A @ ( B @ union ) @ ( C @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[16253,138]) ).
thf(16315,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ( A @ ( B @ union ) @ ( C @ member ) ) ),
inference(simp,[status(thm)],[16314]) ).
thf(16316,plain,
! [A: $i] : ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ),
inference(pattern_uni,[status(thm)],[16315:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) ))]]) ).
thf(16623,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ( C @ ( B @ union ) @ ( D @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[16316,20]) ).
thf(16624,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ( C @ ( B @ union ) @ ( D @ member ) ) ),
inference(simp,[status(thm)],[16623]) ).
thf(16625,plain,
! [B: $i,A: $i] : ( B @ ( sk2 @ union ) @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ),
inference(pattern_uni,[status(thm)],[16624:[bind(A,$thf( J )),bind(B,$thf( B )),bind(C,$thf( J @ ( sk2 @ union ) )),bind(D,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) ))]]) ).
thf(16885,plain,
! [B: $i,A: $i] : ( B @ ( sk2 @ union ) @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ),
inference(simp,[status(thm)],[16625]) ).
thf(15516,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( sk2 @ ( C @ union ) ) )
| ( ( A @ ( B @ union ) @ ( E @ difference ) )
!= ( D @ ( sk2 @ union ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,15002]) ).
thf(15517,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( C @ difference ) )
!= ( B @ ( sk2 @ union ) ) ),
inference(pattern_uni,[status(thm)],[15516:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( A ))]]) ).
thf(15598,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( C @ difference ) )
!= ( B @ ( sk2 @ union ) ) ),
inference(simp,[status(thm)],[15517]) ).
thf(16132,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( D @ ( sk2 @ union ) ) )
| ( ( A @ ( B @ union ) )
!= ( C @ ( sk2 @ union ) @ ( E @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,15598]) ).
thf(16133,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ union ) )
!= ( B @ ( sk2 @ union ) @ ( C @ difference ) ) ),
inference(pattern_uni,[status(thm)],[16132:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( B ))]]) ).
thf(16200,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ union ) )
!= ( B @ ( sk2 @ union ) @ ( C @ difference ) ) ),
inference(simp,[status(thm)],[16133]) ).
thf(88,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( D @ ( C @ union ) ) )
| ( A @ ( B @ union ) @ ( E @ member ) )
| ~ ( C @ ( E @ member ) ) ),
inference(paramod_ordered,[status(thm)],[42,19]) ).
thf(89,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ union ) @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(pattern_uni,[status(thm)],[88:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(102,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ union ) @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[89]) ).
thf(57,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( A @ ( B @ sk5 ) @ member ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[55]) ).
thf(64,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( A @ ( B @ sk5 ) @ member ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ member ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[57]) ).
thf(65,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( A @ ( B @ sk5 ) @ member ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ member ) )
| ( A = B ) ),
inference(simp,[status(thm)],[64]) ).
thf(1916,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk1 @ ( sk2 @ difference ) ) )
| ( B != sk2 )
| ~ ( A @ ( A @ ( B @ sk5 ) @ member ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[65,75]) ).
thf(1917,plain,
! [A: $i] :
( ( A != sk2 )
| ~ ( sk1 @ ( sk2 @ difference ) @ ( sk1 @ ( sk2 @ difference ) @ ( A @ sk5 ) @ member ) )
| ~ ( A @ ( sk1 @ ( sk2 @ difference ) @ ( A @ sk4 ) @ member ) ) ),
inference(pattern_uni,[status(thm)],[1916:[bind(A,$thf( sk1 @ ( sk2 @ difference ) )),bind(B,$thf( B ))]]) ).
thf(2382,plain,
( ~ ( sk1 @ ( sk2 @ difference ) @ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ sk5 ) @ member ) )
| ~ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[1917]) ).
thf(10686,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ( C @ ( B @ union ) @ ( D @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9283,20]) ).
thf(10687,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ( C @ ( B @ union ) @ ( D @ member ) ) ),
inference(simp,[status(thm)],[10686]) ).
thf(10688,plain,
! [B: $i,A: $i] : ( sk2 @ ( B @ union ) @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(pattern_uni,[status(thm)],[10687:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( sk2 @ ( I @ union ) )),bind(D,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ))]]) ).
thf(10872,plain,
! [B: $i,A: $i] : ( sk2 @ ( B @ union ) @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(simp,[status(thm)],[10688]) ).
thf(25197,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( B @ union ) @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( C @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[10872,9796]) ).
thf(25198,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( B @ union ) @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( C @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[25197]) ).
thf(25463,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( B @ union ) @ ( A @ union ) )
!= ( sk2 @ ( C @ difference ) ) )
| ( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ) ) ),
inference(simp,[status(thm)],[25198]) ).
thf(25530,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( B @ union ) @ ( A @ union ) )
!= ( sk2 @ ( C @ difference ) ) ),
inference(simp,[status(thm)],[25463]) ).
thf(13076,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( C @ ( sk2 @ union ) ) )
| ( ( A @ ( B @ union ) @ ( D @ difference ) )
!= ( sk2 @ ( C @ union ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,12934]) ).
thf(13077,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( B @ difference ) )
!= ( sk2 @ ( A @ union ) ) ),
inference(pattern_uni,[status(thm)],[13076:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(13126,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( B @ difference ) )
!= ( sk2 @ ( A @ union ) ) ),
inference(simp,[status(thm)],[13077]) ).
thf(682,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk1 @ ( sk2 @ difference ) @ ( sk1 @ union ) ) )
| ( B
!= ( sk2 @ ( sk1 @ union ) ) )
| ~ ( A @ ( B @ subset ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[39,12]) ).
thf(683,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ union ) ) )
| ~ ( sk1 @ ( sk2 @ difference ) @ ( sk1 @ union ) @ ( A @ subset ) )
| ~ ( A @ ( sk1 @ ( sk2 @ difference ) @ ( sk1 @ union ) @ subset ) ) ),
inference(pattern_uni,[status(thm)],[682:[bind(A,$thf( sk1 @ ( sk2 @ difference ) @ ( sk1 @ union ) )),bind(B,$thf( B ))]]) ).
thf(778,plain,
( ~ ( sk1 @ ( sk2 @ difference ) @ ( sk1 @ union ) @ ( sk2 @ ( sk1 @ union ) @ subset ) )
| ~ ( sk2 @ ( sk1 @ union ) @ ( sk1 @ ( sk2 @ difference ) @ ( sk1 @ union ) @ subset ) ) ),
inference(simp,[status(thm)],[683]) ).
thf(19910,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( sk2 @ ( D @ union ) ) )
| ( ( C @ ( A @ ( B @ union ) @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,19793]) ).
thf(19911,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( sk2 @ union ) @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(pattern_uni,[status(thm)],[19910:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(20047,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( sk2 @ union ) @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(simp,[status(thm)],[19911]) ).
thf(82,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( D @ ( F @ member ) ) )
| ( E @ ( D @ union ) @ ( F @ member ) )
| ~ $true
| ~ ( A @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[19,19]) ).
thf(83,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( D @ ( F @ member ) ) )
| ( E @ ( D @ union ) @ ( F @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[82]) ).
thf(84,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ ( C @ union ) @ union ) @ ( A @ member ) )
| ~ ( C @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[83:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ union ) )),bind(E,$thf( E )),bind(F,$thf( C ))]]) ).
thf(100,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ ( C @ union ) @ union ) @ ( A @ member ) )
| ~ ( C @ ( A @ member ) ) ),
inference(simp,[status(thm)],[84]) ).
thf(16461,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( C @ ( A @ member ) ) )
| ( B @ ( D @ ( C @ union ) @ union ) @ ( A @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[16253,100]) ).
thf(16462,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( C @ ( A @ member ) ) )
| ( B @ ( D @ ( C @ union ) @ union ) @ ( A @ member ) ) ),
inference(simp,[status(thm)],[16461]) ).
thf(16463,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( sk2 @ union ) @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ),
inference(pattern_uni,[status(thm)],[16462:[bind(A,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) )),bind(B,$thf( B )),bind(C,$thf( sk2 )),bind(D,$thf( D ))]]) ).
thf(16497,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( sk2 @ union ) @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ),
inference(simp,[status(thm)],[16463]) ).
thf(134,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( F @ member ) ) )
| ~ $true
| ~ ( E @ ( D @ difference ) @ ( F @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[20,25]) ).
thf(135,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( F @ member ) ) )
| ~ ( E @ ( D @ difference ) @ ( F @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[134]) ).
thf(136,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( C @ union ) @ ( B @ difference ) @ ( A @ member ) )
| ~ ( D @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[135:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( H @ ( G @ union ) )),bind(F,$thf( C ))]]) ).
thf(141,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( C @ union ) @ ( B @ difference ) @ ( A @ member ) )
| ~ ( D @ ( A @ member ) ) ),
inference(simp,[status(thm)],[136]) ).
thf(29297,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ difference ) @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[23772,29014]) ).
thf(29298,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ difference ) @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[29297]) ).
thf(29396,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk2 @ ( sk2 @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= sk2 ) ),
inference(simp,[status(thm)],[29298]) ).
thf(29417,plain,
! [A: $i] :
( ( A @ ( sk2 @ ( sk2 @ difference ) @ difference ) )
!= sk2 ),
inference(simp,[status(thm)],[29396]) ).
thf(15518,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( D @ ( sk2 @ union ) ) )
| ( ( A @ ( B @ union ) )
!= ( sk2 @ ( C @ union ) @ ( E @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,15002]) ).
thf(15519,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ union ) )
!= ( sk2 @ ( B @ union ) @ ( C @ difference ) ) ),
inference(pattern_uni,[status(thm)],[15518:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( B ))]]) ).
thf(15599,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ union ) )
!= ( sk2 @ ( B @ union ) @ ( C @ difference ) ) ),
inference(simp,[status(thm)],[15519]) ).
thf(21918,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( C @ ( sk2 @ ( D @ union ) @ union ) ) )
| ( ( A @ ( B @ union ) )
!= ( sk2 @ ( E @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,19779]) ).
thf(21919,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( C @ union ) @ ( A @ union ) )
!= ( sk2 @ ( B @ difference ) ) ),
inference(pattern_uni,[status(thm)],[21918:[bind(A,$thf( sk2 @ ( F @ union ) )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( F )),bind(E,$thf( E ))]]) ).
thf(22031,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( C @ union ) @ ( A @ union ) )
!= ( sk2 @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[21919]) ).
thf(22423,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( sk2 @ ( E @ union ) @ ( C @ union ) ) )
| ( ( A @ ( B @ union ) )
!= ( sk2 @ ( D @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,22031]) ).
thf(22424,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ ( C @ union ) @ union ) )
!= ( sk2 @ ( B @ difference ) ) ),
inference(pattern_uni,[status(thm)],[22423:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ( F @ union ) )),bind(C,$thf( A )),bind(D,$thf( D )),bind(E,$thf( F ))]]) ).
thf(22533,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ ( C @ union ) @ union ) )
!= ( sk2 @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[22424]) ).
thf(77,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ difference ) @ ( C @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[76]) ).
thf(192,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( F @ ( E @ union ) ) )
| ~ ( A @ ( B @ union ) @ ( D @ difference ) @ ( C @ member ) )
| ~ ( E @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[42,98]) ).
thf(193,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( A @ ( B @ union ) @ ( D @ difference ) @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(pattern_uni,[status(thm)],[192:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( B ))]]) ).
thf(11391,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ( ( C @ ( B @ difference ) )
!= C )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9381,79]) ).
thf(11392,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ( ( C @ ( B @ difference ) )
!= C ) ),
inference(simp,[status(thm)],[11391]) ).
thf(11393,plain,
! [B: $i,A: $i] :
( ( B @ ( sk2 @ union ) @ ( A @ difference ) )
!= ( B @ ( sk2 @ union ) ) ),
inference(pattern_uni,[status(thm)],[11392:[bind(A,$thf( J )),bind(B,$thf( B )),bind(C,$thf( J @ ( sk2 @ union ) )),bind(D,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ))]]) ).
thf(11455,plain,
! [B: $i,A: $i] :
( ( B @ ( sk2 @ union ) @ ( A @ difference ) )
!= ( B @ ( sk2 @ union ) ) ),
inference(simp,[status(thm)],[11393]) ).
thf(12980,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( D @ ( sk2 @ union ) ) )
| ( ( A @ ( B @ union ) @ ( C @ difference ) )
!= ( D @ ( sk2 @ union ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,11455]) ).
thf(12981,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( B @ difference ) )
!= ( A @ ( sk2 @ union ) ) ),
inference(pattern_uni,[status(thm)],[12980:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( B ))]]) ).
thf(13046,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( B @ difference ) )
!= ( A @ ( sk2 @ union ) ) ),
inference(simp,[status(thm)],[12981]) ).
thf(20623,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( C @ ( sk2 @ union ) @ ( D @ union ) ) )
| ( ( A @ ( B @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,20206]) ).
thf(20624,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( sk2 @ union ) @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(pattern_uni,[status(thm)],[20623:[bind(A,$thf( A )),bind(B,$thf( F @ ( sk2 @ union ) )),bind(C,$thf( F )),bind(D,$thf( A ))]]) ).
thf(20757,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( sk2 @ union ) @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(simp,[status(thm)],[20624]) ).
thf(190,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( G @ ( F @ union ) @ ( E @ difference ) @ ( D @ member ) ) )
| ~ $true
| ~ ( F @ ( D @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[19,98]) ).
thf(191,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( G @ ( F @ union ) @ ( E @ difference ) @ ( D @ member ) ) )
| ~ ( F @ ( D @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[190]) ).
thf(205,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( G @ ( F @ union ) @ ( E @ difference ) ) )
| ( C != D )
| ~ ( F @ ( D @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[191]) ).
thf(212,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( F @ ( E @ union ) @ ( D @ difference ) ) )
| ~ ( E @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[205]) ).
thf(58,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( B @ ( A @ ( B @ sk5 ) @ member ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(cnfConj,[status(thm)],[55]) ).
thf(72,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ sk5 ) @ member ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ member ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[58]) ).
thf(73,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ sk5 ) @ member ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ member ) )
| ( A = B ) ),
inference(simp,[status(thm)],[72]) ).
thf(10683,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ~ $true
| ~ ( C @ ( B @ difference ) @ ( D @ member ) ) ),
inference(paramod_ordered,[status(thm)],[9283,25]) ).
thf(10684,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ~ ( C @ ( B @ difference ) @ ( D @ member ) ) ),
inference(simp,[status(thm)],[10683]) ).
thf(10685,plain,
! [B: $i,A: $i] :
~ ( sk2 @ ( B @ union ) @ ( A @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(pattern_uni,[status(thm)],[10684:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( sk2 @ ( I @ union ) )),bind(D,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ))]]) ).
thf(10868,plain,
! [B: $i,A: $i] :
~ ( sk2 @ ( B @ union ) @ ( A @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(simp,[status(thm)],[10685]) ).
thf(26504,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( C @ union ) @ ( B @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9381,10868]) ).
thf(26505,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( C @ union ) @ ( B @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[26504]) ).
thf(26567,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ union ) )
!= ( sk2 @ ( C @ union ) @ ( B @ difference ) ) )
| ( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ) ) ),
inference(simp,[status(thm)],[26505]) ).
thf(26665,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ union ) )
!= ( sk2 @ ( C @ union ) @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[26567]) ).
thf(16327,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ( B @ ( A @ union ) @ ( C @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[16253,20]) ).
thf(16328,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ( B @ ( A @ union ) @ ( C @ member ) ) ),
inference(simp,[status(thm)],[16327]) ).
thf(16329,plain,
! [A: $i] : ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ),
inference(pattern_uni,[status(thm)],[16328:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) ))]]) ).
thf(26349,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( B @ union ) @ ( A @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9341,10868]) ).
thf(26350,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( B @ union ) @ ( A @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[26349]) ).
thf(26555,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( B @ union ) @ ( A @ difference ) )
!= sk2 )
| ( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ) ) ),
inference(simp,[status(thm)],[26350]) ).
thf(26655,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( B @ union ) @ ( A @ difference ) )
!= sk2 ),
inference(simp,[status(thm)],[26555]) ).
thf(16403,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( C @ ( A @ member ) ) )
| ~ ( D @ ( C @ union ) @ ( B @ difference ) @ ( A @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[16253,98]) ).
thf(16404,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( C @ ( A @ member ) ) )
| ~ ( D @ ( C @ union ) @ ( B @ difference ) @ ( A @ member ) ) ),
inference(simp,[status(thm)],[16403]) ).
thf(16405,plain,
! [B: $i,A: $i] :
~ ( B @ ( sk2 @ union ) @ ( A @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ),
inference(pattern_uni,[status(thm)],[16404:[bind(A,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) )),bind(B,$thf( B )),bind(C,$thf( sk2 )),bind(D,$thf( D ))]]) ).
thf(16486,plain,
! [B: $i,A: $i] :
~ ( B @ ( sk2 @ union ) @ ( A @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ),
inference(simp,[status(thm)],[16405]) ).
thf(15970,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( sk2 @ ( D @ union ) ) )
| ( ( A @ ( B @ union ) )
!= ( sk2 @ ( C @ union ) @ ( E @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,15181]) ).
thf(15971,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ union ) )
!= ( sk2 @ ( B @ union ) @ ( C @ difference ) ) ),
inference(pattern_uni,[status(thm)],[15970:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(16075,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ union ) )
!= ( sk2 @ ( B @ union ) @ ( C @ difference ) ) ),
inference(simp,[status(thm)],[15971]) ).
thf(22425,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( sk2 @ ( E @ union ) ) )
| ( ( A @ ( B @ union ) @ ( C @ union ) )
!= ( sk2 @ ( D @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,22031]) ).
thf(22426,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( B @ union ) )
!= ( sk2 @ ( C @ difference ) ) ),
inference(pattern_uni,[status(thm)],[22425:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A ))]]) ).
thf(22534,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( B @ union ) )
!= ( sk2 @ ( C @ difference ) ) ),
inference(simp,[status(thm)],[22426]) ).
thf(23384,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( C @ ( sk2 @ union ) ) )
| ( ( A @ ( B @ union ) @ ( D @ union ) )
!= ( sk2 @ ( E @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,22534]) ).
thf(23385,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( B @ union ) )
!= ( sk2 @ ( C @ difference ) ) ),
inference(pattern_uni,[status(thm)],[23384:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(23526,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( B @ union ) )
!= ( sk2 @ ( C @ difference ) ) ),
inference(simp,[status(thm)],[23385]) ).
thf(26,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ difference ) @ ( C @ member ) )
| ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(27,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ difference ) @ ( C @ member ) )
| ( B @ ( C @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[26]) ).
thf(29279,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ union ) @ ( A @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[293,29014]) ).
thf(29280,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ union ) @ ( A @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[29279]) ).
thf(29397,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ union ) )
!= ( sk2 @ ( sk2 @ difference ) ) )
| ( A != sk2 ) ),
inference(simp,[status(thm)],[29280]) ).
thf(29418,plain,
! [A: $i] :
( ( sk2 @ ( A @ union ) )
!= ( sk2 @ ( sk2 @ difference ) ) ),
inference(simp,[status(thm)],[29397]) ).
thf(16,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) )
| ~ ( B @ ( A @ union ) @ ( C @ member ) ) ),
inference(cnfConj,[status(thm)],[15]) ).
thf(157,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( D @ ( C @ union ) @ ( E @ member ) ) )
| ( D @ ( E @ member ) )
| ( C @ ( E @ member ) )
| ~ $true
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[49,16]) ).
thf(158,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( D @ ( C @ union ) @ ( E @ member ) ) )
| ( D @ ( E @ member ) )
| ( C @ ( E @ member ) )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[157]) ).
thf(159,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( C @ ( B @ union ) @ ( A @ sk3 ) @ member ) )
| ( B @ ( C @ ( B @ union ) @ ( A @ sk3 ) @ member ) )
| ( A @ ( C @ ( B @ union ) @ subset ) ) ),
inference(pattern_uni,[status(thm)],[158:[bind(A,$thf( I @ ( H @ union ) )),bind(B,$thf( F )),bind(C,$thf( H )),bind(D,$thf( I )),bind(E,$thf( I @ ( H @ union ) @ ( F @ sk3 ) ))]]) ).
thf(181,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( C @ ( B @ union ) @ ( A @ sk3 ) @ member ) )
| ( B @ ( C @ ( B @ union ) @ ( A @ sk3 ) @ member ) )
| ( A @ ( C @ ( B @ union ) @ subset ) ) ),
inference(simp,[status(thm)],[159]) ).
thf(26345,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( C @ union ) @ ( B @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9283,10868]) ).
thf(26346,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( C @ union ) @ ( B @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[26345]) ).
thf(26559,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ union ) )
!= ( sk2 @ ( C @ union ) @ ( B @ difference ) ) )
| ( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ) ) ),
inference(simp,[status(thm)],[26346]) ).
thf(26659,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ union ) )
!= ( sk2 @ ( C @ union ) @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[26559]) ).
thf(122,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( F @ member ) ) )
| ( E @ ( D @ union ) @ ( F @ member ) )
| ~ $true
| ~ ( A @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[19,20]) ).
thf(123,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( F @ member ) ) )
| ( E @ ( D @ union ) @ ( F @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[122]) ).
thf(124,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ union ) @ ( B @ union ) @ ( A @ member ) )
| ~ ( C @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[123:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( H @ ( G @ union ) )),bind(F,$thf( C ))]]) ).
thf(144,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ union ) @ ( B @ union ) @ ( A @ member ) )
| ~ ( C @ ( A @ member ) ) ),
inference(simp,[status(thm)],[124]) ).
thf(5193,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk1 @ ( sk2 @ difference ) ) )
| ( B != sk2 )
| ( B @ ( A @ ( B @ sk5 ) @ member ) )
| ( A @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[71,75]) ).
thf(5194,plain,
! [A: $i] :
( ( A != sk2 )
| ( A @ ( sk1 @ ( sk2 @ difference ) @ ( A @ sk5 ) @ member ) )
| ( sk1 @ ( sk2 @ difference ) @ ( sk1 @ ( sk2 @ difference ) @ ( A @ sk4 ) @ member ) ) ),
inference(pattern_uni,[status(thm)],[5193:[bind(A,$thf( sk1 @ ( sk2 @ difference ) )),bind(B,$thf( B ))]]) ).
thf(5848,plain,
( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ sk5 ) @ member ) )
| ( sk1 @ ( sk2 @ difference ) @ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[5194]) ).
thf(182,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( F @ ( D @ member ) ) )
| ~ ( G @ ( F @ union ) @ ( E @ difference ) @ ( D @ member ) )
| ~ $true
| ~ ( B @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[20,98]) ).
thf(183,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( F @ ( D @ member ) ) )
| ~ ( G @ ( F @ union ) @ ( E @ difference ) @ ( D @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[182]) ).
thf(184,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( E @ ( D @ union ) @ union ) @ ( B @ difference ) @ ( A @ member ) )
| ~ ( E @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[183:[bind(A,$thf( H )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( C )),bind(E,$thf( E )),bind(F,$thf( I @ ( H @ union ) ))]]) ).
thf(208,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( E @ ( D @ union ) @ union ) @ ( B @ difference ) @ ( A @ member ) )
| ~ ( E @ ( A @ member ) ) ),
inference(simp,[status(thm)],[184]) ).
thf(37830,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ( A @ ( B @ union ) @ ( C @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37829,138]) ).
thf(37831,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ( A @ ( B @ union ) @ ( C @ member ) ) ),
inference(simp,[status(thm)],[37830]) ).
thf(37832,plain,
! [A: $i] : ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) ),
inference(pattern_uni,[status(thm)],[37831:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) ))]]) ).
thf(185,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( G @ ( F @ union ) @ ( E @ difference ) @ ( D @ member ) ) )
| ~ $true
| ~ ( F @ ( D @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[20,98]) ).
thf(186,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( G @ ( F @ union ) @ ( E @ difference ) @ ( D @ member ) ) )
| ~ ( F @ ( D @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[185]) ).
thf(206,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( G @ ( F @ union ) @ ( E @ difference ) ) )
| ( C != D )
| ~ ( F @ ( D @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[186]) ).
thf(213,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( F @ ( E @ union ) @ ( D @ difference ) ) )
| ~ ( E @ ( C @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[206]) ).
thf(28074,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( sk2 @ union ) @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( C @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11453,9796]) ).
thf(28075,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( sk2 @ union ) @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( C @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[28074]) ).
thf(28347,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( sk2 @ union ) @ union ) )
!= ( sk2 @ ( C @ difference ) ) )
| ( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ) ) ),
inference(simp,[status(thm)],[28075]) ).
thf(28449,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( sk2 @ union ) @ union ) )
!= ( sk2 @ ( C @ difference ) ) ),
inference(simp,[status(thm)],[28347]) ).
thf(29274,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( A @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[289,29014]) ).
thf(29275,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ union ) @ ( A @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[29274]) ).
thf(29394,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( sk2 @ ( sk2 @ difference ) ) )
| ( A != sk2 ) ),
inference(simp,[status(thm)],[29275]) ).
thf(29415,plain,
! [A: $i] :
( ( A @ ( sk2 @ union ) )
!= ( sk2 @ ( sk2 @ difference ) ) ),
inference(simp,[status(thm)],[29394]) ).
thf(9316,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( A @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[289,9028]) ).
thf(9317,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ union ) @ ( A @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[9316]) ).
thf(9387,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) )
| ( A != sk2 ) ),
inference(simp,[status(thm)],[9317]) ).
thf(9398,plain,
! [A: $i] :
( ( A @ ( sk2 @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(simp,[status(thm)],[9387]) ).
thf(29381,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true
| ( A @ ( C @ union ) @ ( C @ ( B @ sk3 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[175,29014]) ).
thf(29382,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ( A @ ( C @ union ) @ ( C @ ( B @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[29381]) ).
thf(29383,plain,
! [A: $i] : ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(pattern_uni,[status(thm)],[29382:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ( sk2 @ difference ) )),bind(C,$thf( sk2 ))]]) ).
thf(199,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( F @ ( E @ union ) @ ( D @ difference ) @ ( C @ member ) ) )
| ~ $true
| ~ ( E @ ( C @ member ) )
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[49,98]) ).
thf(200,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( F @ ( E @ union ) @ ( D @ difference ) @ ( C @ member ) ) )
| ~ ( E @ ( C @ member ) )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[199]) ).
thf(201,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( D @ ( C @ union ) @ ( B @ difference ) @ ( A @ sk3 ) @ member ) )
| ( A @ ( D @ ( C @ union ) @ ( B @ difference ) @ subset ) ) ),
inference(pattern_uni,[status(thm)],[200:[bind(A,$thf( L @ ( K @ union ) @ ( I @ difference ) )),bind(B,$thf( G )),bind(C,$thf( L @ ( K @ union ) @ ( I @ difference ) @ ( G @ sk3 ) )),bind(D,$thf( I )),bind(E,$thf( K )),bind(F,$thf( L ))]]) ).
thf(209,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( D @ ( C @ union ) @ ( B @ difference ) @ ( A @ sk3 ) @ member ) )
| ( A @ ( D @ ( C @ union ) @ ( B @ difference ) @ subset ) ) ),
inference(simp,[status(thm)],[201]) ).
thf(125,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( F @ member ) ) )
| ( ( E @ ( D @ difference ) )
!= E )
| ~ $true
| ~ ( B @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[20,79]) ).
thf(126,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( F @ member ) ) )
| ( ( E @ ( D @ difference ) )
!= E )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[125]) ).
thf(127,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ union ) @ ( B @ difference ) )
!= ( D @ ( C @ union ) ) )
| ~ ( D @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[126:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( H @ ( G @ union ) )),bind(F,$thf( C ))]]) ).
thf(145,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ union ) @ ( B @ difference ) )
!= ( D @ ( C @ union ) ) )
| ~ ( D @ ( A @ member ) ) ),
inference(simp,[status(thm)],[127]) ).
thf(29775,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk2 @ ( sk2 @ difference ) ) )
| ( B != sk2 )
| ~ ( A @ ( A @ ( B @ sk5 ) @ member ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[65,29414]) ).
thf(29776,plain,
! [A: $i] :
( ( A != sk2 )
| ~ ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ ( sk2 @ difference ) @ ( A @ sk5 ) @ member ) )
| ~ ( A @ ( sk2 @ ( sk2 @ difference ) @ ( A @ sk4 ) @ member ) ) ),
inference(pattern_uni,[status(thm)],[29775:[bind(A,$thf( sk2 @ ( sk2 @ difference ) )),bind(B,$thf( B ))]]) ).
thf(29839,plain,
( ~ ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ sk5 ) @ member ) )
| ~ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[29776]) ).
thf(11272,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ( C @ ( B @ union ) @ ( D @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9381,20]) ).
thf(11273,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( D @ member ) ) )
| ( C @ ( B @ union ) @ ( D @ member ) ) ),
inference(simp,[status(thm)],[11272]) ).
thf(11274,plain,
! [B: $i,A: $i] : ( B @ ( sk2 @ union ) @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(pattern_uni,[status(thm)],[11273:[bind(A,$thf( J )),bind(B,$thf( B )),bind(C,$thf( J @ ( sk2 @ union ) )),bind(D,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ))]]) ).
thf(11405,plain,
! [B: $i,A: $i] : ( B @ ( sk2 @ union ) @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(simp,[status(thm)],[11274]) ).
thf(27459,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( sk2 @ union ) @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( C @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11405,9796]) ).
thf(27460,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( sk2 @ union ) @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( C @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[27459]) ).
thf(27715,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( sk2 @ union ) @ ( A @ union ) )
!= ( sk2 @ ( C @ difference ) ) )
| ( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ) ) ),
inference(simp,[status(thm)],[27460]) ).
thf(27774,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( sk2 @ union ) @ ( A @ union ) )
!= ( sk2 @ ( C @ difference ) ) ),
inference(simp,[status(thm)],[27715]) ).
thf(20269,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( D @ ( C @ ( sk2 @ union ) @ union ) ) )
| ( ( A @ ( B @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,20047]) ).
thf(20270,plain,
! [B: $i,A: $i] :
( ( B @ ( sk2 @ union ) @ ( A @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(pattern_uni,[status(thm)],[20269:[bind(A,$thf( F @ ( sk2 @ union ) )),bind(B,$thf( B )),bind(C,$thf( F )),bind(D,$thf( B ))]]) ).
thf(20420,plain,
! [B: $i,A: $i] :
( ( B @ ( sk2 @ union ) @ ( A @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(simp,[status(thm)],[20270]) ).
thf(22585,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( D @ ( C @ ( sk2 @ union ) @ union ) ) )
| ( ( A @ ( B @ union ) )
!= ( sk2 @ ( E @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,22032]) ).
thf(22586,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( sk2 @ union ) @ ( A @ union ) )
!= ( sk2 @ ( B @ difference ) ) ),
inference(pattern_uni,[status(thm)],[22585:[bind(A,$thf( G @ ( sk2 @ union ) )),bind(B,$thf( B )),bind(C,$thf( G )),bind(D,$thf( B )),bind(E,$thf( E ))]]) ).
thf(22712,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( sk2 @ union ) @ ( A @ union ) )
!= ( sk2 @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[22586]) ).
thf(20271,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( C @ ( sk2 @ union ) ) )
| ( ( D @ ( A @ ( B @ union ) @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,20047]) ).
thf(20272,plain,
! [B: $i,A: $i] :
( ( B @ ( sk2 @ ( A @ union ) @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(pattern_uni,[status(thm)],[20271:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(20421,plain,
! [B: $i,A: $i] :
( ( B @ ( sk2 @ ( A @ union ) @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(simp,[status(thm)],[20272]) ).
thf(29276,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true
| ( C @ ( A @ union ) @ ( C @ ( B @ sk3 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[179,29014]) ).
thf(29277,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ subset ) )
!= ( sk2 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ( C @ ( A @ union ) @ ( C @ ( B @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[29276]) ).
thf(29278,plain,
! [A: $i] : ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk3 ) @ member ) ),
inference(pattern_uni,[status(thm)],[29277:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ( sk2 @ difference ) )),bind(C,$thf( sk2 ))]]) ).
thf(132,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( D @ difference ) @ ( F @ member ) ) )
| ~ ( E @ ( F @ member ) )
| ~ $true
| ~ ( B @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[20,25]) ).
thf(133,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( D @ difference ) @ ( F @ member ) ) )
| ~ ( E @ ( F @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[132]) ).
thf(137,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( E @ ( D @ difference ) ) )
| ( C != F )
| ~ ( E @ ( F @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[133]) ).
thf(143,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( D @ ( C @ difference ) ) )
| ~ ( D @ ( E @ member ) )
| ~ ( B @ ( E @ member ) ) ),
inference(simp,[status(thm)],[137]) ).
thf(92,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( D @ difference ) @ ( F @ member ) ) )
| ~ ( E @ ( F @ member ) )
| ~ $true
| ~ ( A @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[19,25]) ).
thf(93,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( D @ difference ) @ ( F @ member ) ) )
| ~ ( E @ ( F @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[92]) ).
thf(97,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( E @ ( D @ difference ) ) )
| ( C != F )
| ~ ( E @ ( F @ member ) )
| ~ ( A @ ( C @ member ) ) ),
inference(simp,[status(thm)],[93]) ).
thf(99,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( D @ ( C @ difference ) ) )
| ~ ( D @ ( E @ member ) )
| ~ ( A @ ( E @ member ) ) ),
inference(simp,[status(thm)],[97]) ).
thf(203,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ union ) @ ( B @ difference ) @ ( A @ member ) )
!= ( C @ ( A @ member ) ) )
| ~ ( C @ ( A @ member ) ) ),
inference(simp,[status(thm)],[202]) ).
thf(113,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( F @ member ) ) )
| ( E @ ( D @ union ) @ ( F @ member ) )
| ~ $true
| ~ ( B @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[20,20]) ).
thf(114,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) @ ( C @ member ) )
!= ( E @ ( F @ member ) ) )
| ( E @ ( D @ union ) @ ( F @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(simp,[status(thm)],[113]) ).
thf(115,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ union ) @ ( B @ union ) @ ( A @ member ) )
| ~ ( D @ ( A @ member ) ) ),
inference(pattern_uni,[status(thm)],[114:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( H @ ( G @ union ) )),bind(F,$thf( C ))]]) ).
thf(139,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ union ) @ ( B @ union ) @ ( A @ member ) )
| ~ ( D @ ( A @ member ) ) ),
inference(simp,[status(thm)],[115]) ).
thf(23877,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ difference ) @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[23772,9028]) ).
thf(23878,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ difference ) @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[23877]) ).
thf(23879,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk1 @ ( sk2 @ difference ) ) )
| ( ( B @ ( A @ difference ) )
!= sk2 ) ),
inference(simp,[status(thm)],[23878]) ).
thf(23886,plain,
! [A: $i] :
( ( A @ ( sk1 @ ( sk2 @ difference ) @ difference ) )
!= sk2 ),
inference(simp,[status(thm)],[23879]) ).
thf(9800,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( A @ ( C @ member ) ) )
| ( B @ ( C @ member ) )
| ~ $true
| ~ ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[9341,46]) ).
thf(9801,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( A @ ( C @ member ) ) )
| ( B @ ( C @ member ) )
| ~ ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[9800]) ).
thf(9802,plain,
! [A: $i] :
( ( A @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
| ~ ( A @ ( sk2 @ subset ) ) ),
inference(pattern_uni,[status(thm)],[9801:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ))]]) ).
thf(9951,plain,
! [A: $i] :
( ( A @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
| ~ ( A @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[9802]) ).
thf(9903,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( A @ member ) ) )
| ( ( D @ ( C @ union ) @ ( B @ difference ) )
!= C )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9341,210]) ).
thf(9904,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( C @ ( A @ member ) ) )
| ( ( D @ ( C @ union ) @ ( B @ difference ) )
!= C ) ),
inference(simp,[status(thm)],[9903]) ).
thf(9905,plain,
! [B: $i,A: $i] :
( ( B @ ( sk2 @ union ) @ ( A @ difference ) )
!= sk2 ),
inference(pattern_uni,[status(thm)],[9904:[bind(A,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )),bind(B,$thf( B )),bind(C,$thf( sk2 )),bind(D,$thf( D ))]]) ).
thf(9940,plain,
! [B: $i,A: $i] :
( ( B @ ( sk2 @ union ) @ ( A @ difference ) )
!= sk2 ),
inference(simp,[status(thm)],[9905]) ).
thf(13734,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( sk2 @ ( C @ union ) ) )
| ( ( A @ ( B @ union ) @ ( D @ difference ) )
!= ( C @ ( sk2 @ union ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,13046]) ).
thf(13735,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( B @ difference ) )
!= ( A @ ( sk2 @ union ) ) ),
inference(pattern_uni,[status(thm)],[13734:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( A ))]]) ).
thf(13793,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ union ) @ ( B @ difference ) )
!= ( A @ ( sk2 @ union ) ) ),
inference(simp,[status(thm)],[13735]) ).
thf(196,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( E @ ( C @ member ) ) )
| ~ ( F @ ( E @ union ) @ ( D @ difference ) @ ( C @ member ) )
| ~ $true
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[49,98]) ).
thf(197,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( E @ ( C @ member ) ) )
| ~ ( F @ ( E @ union ) @ ( D @ difference ) @ ( C @ member ) )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[196]) ).
thf(198,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( D @ union ) @ ( A @ difference ) @ ( D @ ( C @ sk3 ) @ member ) )
| ( C @ ( D @ subset ) ) ),
inference(pattern_uni,[status(thm)],[197:[bind(A,$thf( H )),bind(B,$thf( G )),bind(C,$thf( H @ ( G @ sk3 ) )),bind(D,$thf( D )),bind(E,$thf( H ))]]) ).
thf(207,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( D @ union ) @ ( A @ difference ) @ ( D @ ( C @ sk3 ) @ member ) )
| ( C @ ( D @ subset ) ) ),
inference(simp,[status(thm)],[198]) ).
thf(23386,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( C @ ( sk2 @ union ) @ ( D @ union ) ) )
| ( ( A @ ( B @ union ) )
!= ( sk2 @ ( E @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,22534]) ).
thf(23387,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( sk2 @ union ) @ union ) )
!= ( sk2 @ ( B @ difference ) ) ),
inference(pattern_uni,[status(thm)],[23386:[bind(A,$thf( A )),bind(B,$thf( G @ ( sk2 @ union ) )),bind(C,$thf( G )),bind(D,$thf( A )),bind(E,$thf( E ))]]) ).
thf(23527,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( sk2 @ union ) @ union ) )
!= ( sk2 @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[23387]) ).
thf(1922,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk1 @ ( sk2 @ difference ) ) )
| ( A != sk2 )
| ~ ( A @ ( A @ ( B @ sk5 ) @ member ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ member ) ) ),
inference(paramod_ordered,[status(thm)],[65,75]) ).
thf(1923,plain,
! [A: $i] :
( ( A != sk2 )
| ~ ( A @ ( A @ ( sk1 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
| ~ ( sk1 @ ( sk2 @ difference ) @ ( A @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(pattern_uni,[status(thm)],[1922:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ( sk2 @ difference ) ))]]) ).
thf(2385,plain,
( ~ ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk5 ) @ member ) )
| ~ ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ) ),
inference(simp,[status(thm)],[1923]) ).
thf(37851,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ( B @ ( A @ union ) @ ( C @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[37829,20]) ).
thf(37852,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ( B @ ( A @ union ) @ ( C @ member ) ) ),
inference(simp,[status(thm)],[37851]) ).
thf(37853,plain,
! [A: $i] : ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) @ member ) ),
inference(pattern_uni,[status(thm)],[37852:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk2 @ ( sk2 @ ( sk2 @ difference ) @ sk4 ) ))]]) ).
thf(8,axiom,
! [A: $i] : ( A @ ( A @ subset ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_of_subset) ).
thf(51,plain,
! [A: $i] : ( A @ ( A @ subset ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(244,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( C @ ( E @ union ) ) )
| ( A @ ( B @ union ) @ ( E @ ( D @ sk3 ) @ member ) )
| ( D @ ( E @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[42,175]) ).
thf(245,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ union ) @ ( A @ ( C @ sk3 ) @ member ) )
| ( C @ ( A @ subset ) ) ),
inference(pattern_uni,[status(thm)],[244:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( D )),bind(E,$thf( A ))]]) ).
thf(273,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ union ) @ ( A @ ( C @ sk3 ) @ member ) )
| ( C @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[245]) ).
thf(169,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( D @ ( C @ difference ) @ ( E @ member ) ) )
| ~ ( D @ ( E @ member ) )
| ~ $true
| ( B @ ( A @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[49,25]) ).
thf(170,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( B @ sk3 ) @ member ) )
!= ( D @ ( C @ difference ) @ ( E @ member ) ) )
| ~ ( D @ ( E @ member ) )
| ( B @ ( A @ subset ) ) ),
inference(simp,[status(thm)],[169]) ).
thf(171,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( C @ ( B @ difference ) @ ( A @ sk3 ) @ member ) )
| ( A @ ( C @ ( B @ difference ) @ subset ) ) ),
inference(pattern_uni,[status(thm)],[170:[bind(A,$thf( I @ ( H @ difference ) )),bind(B,$thf( F )),bind(C,$thf( H )),bind(D,$thf( I )),bind(E,$thf( I @ ( H @ difference ) @ ( F @ sk3 ) ))]]) ).
thf(178,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( C @ ( B @ difference ) @ ( A @ sk3 ) @ member ) )
| ( A @ ( C @ ( B @ difference ) @ subset ) ) ),
inference(simp,[status(thm)],[171]) ).
thf(24467,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ ( B @ difference ) @ ( A @ sk3 ) @ member ) )
!= ( F @ ( F @ ( E @ difference ) @ ( D @ sk3 ) @ member ) ) )
| ~ $true
| ( D @ ( F @ ( E @ difference ) @ subset ) )
| ( A @ ( C @ ( B @ difference ) @ subset ) ) ),
inference(paramod_ordered,[status(thm)],[177,178]) ).
thf(24468,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ ( B @ difference ) @ ( A @ sk3 ) @ member ) )
!= ( F @ ( F @ ( E @ difference ) @ ( D @ sk3 ) @ member ) ) )
| ( D @ ( F @ ( E @ difference ) @ subset ) )
| ( A @ ( C @ ( B @ difference ) @ subset ) ) ),
inference(simp,[status(thm)],[24467]) ).
thf(24469,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ difference ) @ subset ) )
| ( A @ ( B @ ( B @ difference ) @ subset ) ) ),
inference(pattern_uni,[status(thm)],[24468:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A )),bind(E,$thf( B )),bind(F,$thf( B ))]]) ).
thf(24510,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ difference ) @ subset ) ),
inference(simp,[status(thm)],[24469]) ).
thf(16441,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( D @ ( A @ member ) ) )
| ( D @ ( C @ union ) @ ( B @ union ) @ ( A @ member ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[16253,139]) ).
thf(16442,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( D @ ( A @ member ) ) )
| ( D @ ( C @ union ) @ ( B @ union ) @ ( A @ member ) ) ),
inference(simp,[status(thm)],[16441]) ).
thf(16443,plain,
! [B: $i,A: $i] : ( sk2 @ ( B @ union ) @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ),
inference(pattern_uni,[status(thm)],[16442:[bind(A,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( sk2 ))]]) ).
thf(16494,plain,
! [B: $i,A: $i] : ( sk2 @ ( B @ union ) @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ),
inference(simp,[status(thm)],[16443]) ).
thf(16324,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ $true
| ~ ( B @ ( A @ difference ) @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[16253,25]) ).
thf(16325,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) )
!= ( B @ ( C @ member ) ) )
| ~ ( B @ ( A @ difference ) @ ( C @ member ) ) ),
inference(simp,[status(thm)],[16324]) ).
thf(16326,plain,
! [A: $i] :
~ ( sk2 @ ( A @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) @ member ) ),
inference(pattern_uni,[status(thm)],[16325:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk4 ) ))]]) ).
thf(194,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ union ) )
!= ( F @ ( E @ union ) ) )
| ~ ( B @ ( A @ union ) @ ( D @ difference ) @ ( C @ member ) )
| ~ ( E @ ( C @ member ) ) ),
inference(paramod_ordered,[status(thm)],[42,98]) ).
thf(195,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ union ) @ ( D @ difference ) @ ( C @ member ) )
| ~ ( B @ ( C @ member ) ) ),
inference(pattern_uni,[status(thm)],[194:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( B )),bind(F,$thf( A ))]]) ).
thf(20621,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( C @ ( sk2 @ union ) ) )
| ( ( A @ ( B @ union ) @ ( D @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,20206]) ).
thf(20622,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( B @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(pattern_uni,[status(thm)],[20621:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(20756,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( B @ union ) )
!= ( sk1 @ ( sk2 @ difference ) ) ),
inference(simp,[status(thm)],[20622]) ).
thf(24598,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ difference ) @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[24510,9028]) ).
thf(24599,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ difference ) @ subset ) )
!= ( sk1 @ ( sk2 @ difference ) @ ( sk2 @ subset ) ) ),
inference(simp,[status(thm)],[24598]) ).
thf(24601,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk1 @ ( sk2 @ difference ) ) )
| ( ( B @ ( B @ difference ) )
!= sk2 ) ),
inference(simp,[status(thm)],[24599]) ).
thf(24615,plain,
! [A: $i] :
( ( A @ ( A @ difference ) )
!= sk2 ),
inference(simp,[status(thm)],[24601]) ).
thf(11567,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( B @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9283,9796]) ).
thf(11568,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( A @ union ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) )
!= ( sk2 @ ( B @ difference ) @ ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) @ member ) ) ),
inference(simp,[status(thm)],[11567]) ).
thf(11672,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ union ) )
!= ( sk2 @ ( B @ difference ) ) )
| ( ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ difference ) @ sk3 ) ) ) ),
inference(simp,[status(thm)],[11568]) ).
thf(11707,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( A @ union ) )
!= ( sk2 @ ( B @ difference ) ) ),
inference(simp,[status(thm)],[11672]) ).
thf(107,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ union ) )
!= ( D @ ( C @ union ) ) )
| ( D @ ( E @ member ) )
| ( C @ ( E @ member ) )
| ~ ( A @ ( B @ union ) @ ( E @ member ) ) ),
inference(paramod_ordered,[status(thm)],[42,16]) ).
thf(108,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) )
| ~ ( A @ ( B @ union ) @ ( C @ member ) ) ),
inference(pattern_uni,[status(thm)],[107:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(111,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ member ) )
| ( A @ ( C @ member ) )
| ~ ( A @ ( B @ union ) @ ( C @ member ) ) ),
inference(simp,[status(thm)],[108]) ).
thf(227323,plain,
$false,
inference(e,[status(thm)],[15002,14852,138,101,12934,10478,20046,29317,10,29847,153,142,29339,18384,42,24,9396,25,11720,11453,20,46,289,20206,9362,152,9283,179,211,37850,22713,221,293,9452,16885,9796,37829,9341,16200,102,2382,25530,13126,778,21,10858,28,20047,65,16497,53,141,29417,15599,22533,77,193,13046,23772,20757,212,16316,13,73,26665,16329,10862,22032,26655,180,10872,176,11455,16486,29014,16075,23526,27,71,12,29418,49,181,26659,144,5848,9322,39,98,208,37832,213,28449,9381,223,29415,9921,9398,35,16253,29383,22534,209,145,29839,27774,19793,50,67,177,16,20420,22712,15598,20421,22031,175,29278,143,43,99,203,139,23886,40,9951,9940,9028,9919,75,13793,16074,207,23527,11405,2385,37853,51,273,10868,24510,16494,19,16326,210,79,195,20756,14846,24615,11707,178,111,29414,15181,19779,100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET607+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.12/0.39 % Computer : n017.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sat Sep 26 07:55:03 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.87/0.98 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.25/1.18 % [INFO] Parsing done (191ms).
% 1.25/1.19 % [INFO] Running in sequential loop mode.
% 2.06/1.60 % [INFO] eprover registered as external prover.
% 2.06/1.61 % [INFO] Scanning for conjecture ...
% 2.25/1.70 % [INFO] Found a conjecture (or negated_conjecture) and 7 axioms. Running axiom selection ...
% 2.25/1.74 % [INFO] Axiom selection finished. Selected 7 axioms (removed 0 axioms).
% 2.25/1.76 % [INFO] Problem is first-order (TPTP FOF).
% 2.25/1.76 % [INFO] Type checking passed.
% 2.25/1.77 % [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 ...
% 254.04/73.06 % External prover 'e' found a proof!
% 254.04/73.07 % [INFO] Killing All external provers ...
% 254.04/73.07 % Time passed: 72527ms (effective reasoning time: 71870ms)
% 254.04/73.07 % 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)>
% 254.04/73.07 % Axioms used in derivation (7): reflexivity_of_subset, equal_member_defn, equal_defn, difference_defn, commutativity_of_union, union_defn, subset_defn
% 254.04/73.07 % No. of inferences in proof: 541
% 254.04/73.07 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 72527 ms resp. 71870 ms w/o parsing
% 248.58/73.29 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 248.58/73.29 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------