%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SET894+1 : TPTP v9.3.1. Bugfixed v4.0.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 : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:31:16 AM UTC 2026
% Result : Theorem 166.05s 42.83s
% Output : Refutation 161.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 25
% Syntax : Number of formulae : 452 ( 143 unt; 0 typ; 14 def)
% Number of atoms : 1204 ( 542 equ; 0 cnn)
% Maximal formula atoms : 34 ( 2 avg)
% Number of connectives : 5666 ( 757 ~; 497 |; 68 &;4295 @)
% ( 6 <=>; 43 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 7 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 24 ( 21 usr; 6 con; 0-4 aty)
% Number of variables : 931 ( 28 ^; 859 !; 30 ?; 931 :)
% ( 0 !>; 0 ?*; 0 @-; 14 @+)
% Comments :
%------------------------------------------------------------------------------
thf(cartesian_product2_decl,type,
cartesian_product2: $i > $i > $i ).
thf(singleton_decl,type,
singleton: $i > $i ).
thf(ordered_pair_decl,type,
ordered_pair: $i > $i > $i ).
thf(in_decl,type,
in: $i > $i > $o ).
thf(unordered_pair_decl,type,
unordered_pair: $i > $i > $i ).
thf(empty_decl,type,
empty: $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 > $i > $i ).
thf(sk6_decl,type,
sk6: $i > $i > $i > $i > $i ).
thf(sk7_decl,type,
sk7: $i > $i > $i > $o ).
thf(sk8_decl,type,
sk8: $i > $i > $i > $i ).
thf(sk9_decl,type,
sk9: $i > $i > $i > $i ).
thf(sk10_decl,type,
sk10: $i > $i > $i > $i ).
thf(sk11_decl,type,
sk11: $i > $i > $i > $i ).
thf(sk12_decl,type,
sk12: $i ).
thf(sk13_decl,type,
sk13: $i ).
thf(sk14_decl,type,
sk14: $i > $i > $i ).
thf(sk15_decl,type,
sk15: $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i] :
( ( B @ singleton @ ( A @ singleton @ cartesian_product2 ) )
= ( B @ ( A @ ordered_pair ) @ singleton ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
( ( A @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( A @ ( sk1 @ ordered_pair ) @ singleton ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( A @ ( C @ in ) )
=> ( C = B ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( C = B )
=> ( A @ ( C @ in ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: $i,B: $i,C: $i,D: $i] :
@+[E: $i] :
( ? [F: $i] :
( ( A
= ( F @ ( E @ ordered_pair ) ) )
& ( C @ ( F @ in ) ) )
& ( D @ ( E @ in ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: $i,B: $i,C: $i,D: $i] :
@+[E: $i] :
( ( A
= ( E @ ( D @ ( C @ ( B @ ( A @ sk5 ) ) ) @ ordered_pair ) ) )
& ( C @ ( E @ in ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
~ ( ( A @ ( D @ in ) )
=> ? [E: $i] :
( ? [F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) ) )
& ( C @ ( E @ in ) ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
~ ( ? [E: $i] :
( ? [F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) ) )
& ( C @ ( E @ in ) ) )
=> ( A @ ( D @ in ) ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
( ? [E: $i] :
( ( ( C @ ( B @ ( A @ sk9 ) ) )
= ( E @ ( D @ ordered_pair ) ) )
& ( B @ ( E @ in ) ) )
& ( C @ ( D @ in ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [A: $i,B: $i,C: $i] :
@+[D: $i] :
( ( ( C @ ( B @ ( A @ sk9 ) ) )
= ( D @ ( C @ ( B @ ( A @ sk10 ) ) @ ordered_pair ) ) )
& ( B @ ( D @ in ) ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( @+[A: $i] : ( A @ empty ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( @+[A: $i] :
~ ( A @ empty ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( B @ ( C @ in ) )
=> ( A @ ( C @ in ) ) ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( ^ [A: $i,B: $i] :
@+[C: $i] :
~ ( ( A @ ( C @ in ) )
=> ( B @ ( C @ in ) ) ) ) ) ).
thf(5,axiom,
! [A: $i,B: $i] :
( ( B
= ( A @ singleton ) )
<=> ! [C: $i] :
( ( B @ ( C @ in ) )
<=> ( C = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_tarski) ).
thf(21,plain,
! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( ( C = A )
=> ( B @ ( C @ in ) ) )
& ( ( B @ ( C @ in ) )
=> ( C = A ) ) )
=> ( B
= ( A @ singleton ) ) )
& ( ( B
= ( A @ singleton ) )
=> ! [C: $i] :
( ( ( C = A )
=> ( B @ ( C @ in ) ) )
& ( ( B @ ( C @ in ) )
=> ( C = A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(22,plain,
( ! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( C = A )
=> ( B @ ( C @ in ) ) )
& ! [C: $i] :
( ( B @ ( C @ in ) )
=> ( C = A ) ) )
=> ( B
= ( A @ singleton ) ) )
& ! [A: $i,B: $i] :
( ( B
= ( A @ singleton ) )
=> ( ! [C: $i] :
( ( C = A )
=> ( B @ ( C @ in ) ) )
& ! [C: $i] :
( ( B @ ( C @ in ) )
=> ( C = A ) ) ) ) ),
inference(miniscope,[status(thm)],[21]) ).
thf(23,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F
= ( E @ singleton ) )
| ~ ( F @ ( E @ ( F @ sk4 ) @ in ) )
| ( ( E @ ( F @ sk3 ) )
!= E ) )
& ( ( F
= ( E @ singleton ) )
| ( ( E @ ( F @ sk4 ) )
= E )
| ( ( E @ ( F @ sk3 ) )
!= E ) )
& ( ( F
= ( E @ singleton ) )
| ~ ( F @ ( E @ ( F @ sk4 ) @ in ) )
| ( F @ ( E @ ( F @ sk3 ) @ in ) ) )
& ( ( F
= ( E @ singleton ) )
| ( ( E @ ( F @ sk4 ) )
= E )
| ( F @ ( E @ ( F @ sk3 ) @ in ) ) )
& ( ( B @ ( D @ in ) )
| ( D != A )
| ( B
!= ( A @ singleton ) ) )
& ( ( C = A )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ singleton ) ) ) ),
inference(cnf,[status(esa)],[22]) ).
thf(28,plain,
! [C: $i,B: $i,A: $i] :
( ( C = A )
| ~ ( B @ ( C @ in ) )
| ( B
!= ( A @ singleton ) ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(32,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ in ) )
| ( C = A )
| ( B
!= ( A @ singleton ) ) ),
inference(lifteq,[status(thm)],[28]) ).
thf(33,plain,
! [B: $i,A: $i] :
( ~ ( A @ singleton @ ( B @ in ) )
| ( B = A ) ),
inference(simp,[status(thm)],[32]) ).
thf(1,conjecture,
! [A: $i,B: $i] :
( ( B @ singleton @ ( A @ singleton @ cartesian_product2 ) )
= ( B @ ( A @ ordered_pair ) @ singleton ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t35_zfmisc_1) ).
thf(2,negated_conjecture,
~ ! [A: $i,B: $i] :
( ( B @ singleton @ ( A @ singleton @ cartesian_product2 ) )
= ( B @ ( A @ ordered_pair ) @ singleton ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(13,plain,
~ ! [A: $i,B: $i] :
( ( B @ singleton @ ( A @ singleton @ cartesian_product2 ) )
= ( B @ ( A @ ordered_pair ) @ singleton ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(14,plain,
( ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) ),
inference(cnf,[status(esa)],[13]) ).
thf(15,plain,
( ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) ),
inference(lifteq,[status(thm)],[14]) ).
thf(350,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ( A
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(351,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[350:[bind(A,$thf( A )),bind(B,$thf( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ))]]) ).
thf(519,plain,
~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) ),
inference(simp,[status(thm)],[351]) ).
thf(835,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton ) )
| ~ ( A @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,519]) ).
thf(836,plain,
! [A: $i] :
( ~ ( A @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) )
| ~ ( A @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[835:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton ))]]) ).
thf(27,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ in ) )
| ( C != A )
| ( B
!= ( A @ singleton ) ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(34,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ in ) )
| ( C != A )
| ( B
!= ( A @ singleton ) ) ),
inference(lifteq,[status(thm)],[27]) ).
thf(35,plain,
! [A: $i] : ( A @ singleton @ ( A @ in ) ),
inference(simp,[status(thm)],[34]) ).
thf(3,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ~ ( A @ ( B @ in ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
thf(16,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ in ) )
=> ~ ( A @ ( B @ in ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(17,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ in ) )
| ~ ( B @ ( A @ in ) ) ),
inference(cnf,[status(esa)],[16]) ).
thf(110,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( C @ ( B @ in ) ) )
| ~ ( B @ ( C @ in ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,17]) ).
thf(111,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( C @ ( B @ in ) ) )
| ~ ( B @ ( C @ in ) ) ),
inference(simp,[status(thm)],[110]) ).
thf(112,plain,
! [A: $i] :
~ ( A @ ( A @ singleton @ in ) ),
inference(pattern_uni,[status(thm)],[111:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ singleton ))]]) ).
thf(118,plain,
! [A: $i] :
~ ( A @ ( A @ singleton @ in ) ),
inference(simp,[status(thm)],[112]) ).
thf(185,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( B @ ( B @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,118]) ).
thf(186,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( B @ ( B @ singleton @ in ) ) ),
inference(simp,[status(thm)],[185]) ).
thf(187,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton )
!= B )
| ( A
!= ( B @ singleton ) ) ),
inference(simp,[status(thm)],[186]) ).
thf(189,plain,
! [A: $i] :
( ( A @ singleton @ singleton )
!= A ),
inference(simp,[status(thm)],[187]) ).
thf(384,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ singleton @ singleton ) )
| ( B != C )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,189]) ).
thf(385,plain,
! [B: $i,A: $i] :
( ( A != B )
| ~ ( B @ singleton @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[384:[bind(A,$thf( E @ singleton @ singleton )),bind(B,$thf( B )),bind(C,$thf( E ))]]) ).
thf(532,plain,
! [A: $i] :
~ ( A @ singleton @ singleton @ singleton @ ( A @ in ) ),
inference(simp,[status(thm)],[385]) ).
thf(1697,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( B @ singleton @ singleton @ singleton @ ( B @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,532]) ).
thf(1698,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( B @ singleton @ singleton @ singleton @ ( B @ in ) ) ),
inference(simp,[status(thm)],[1697]) ).
thf(1711,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton )
!= ( B @ singleton @ singleton @ singleton ) )
| ( A != B ) ),
inference(simp,[status(thm)],[1698]) ).
thf(1718,plain,
! [A: $i] :
( ( A @ singleton @ singleton @ singleton )
!= ( A @ singleton ) ),
inference(simp,[status(thm)],[1711]) ).
thf(10,axiom,
? [A: $i] : ( A @ empty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_xboole_0) ).
thf(88,plain,
? [A: $i] : ( A @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(89,plain,
sk12 @ empty,
inference(cnf,[status(esa)],[88]) ).
thf(8,axiom,
! [A: $i,B: $i] :
~ ( B @ ( A @ ordered_pair ) @ empty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
thf(78,plain,
! [A: $i,B: $i] :
~ ( B @ ( A @ ordered_pair ) @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(79,plain,
~ ? [A: $i,B: $i] : ( B @ ( A @ ordered_pair ) @ empty ),
inference(miniscope,[status(thm)],[78]) ).
thf(80,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ ordered_pair ) @ empty ),
inference(cnf,[status(esa)],[79]) ).
thf(107,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ordered_pair ) @ empty )
!= ( sk12 @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[89,80]) ).
thf(108,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) @ empty )
!= ( sk12 @ empty ) ),
inference(simp,[status(thm)],[107]) ).
thf(109,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) )
!= sk12 ),
inference(simp,[status(thm)],[108]) ).
thf(476,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ordered_pair ) ) )
| ( A != sk12 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,109]) ).
thf(477,plain,
! [C: $i,B: $i,A: $i] :
( ( A != sk12 )
| ~ ( A @ singleton @ ( C @ ( B @ ordered_pair ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[476:[bind(A,$thf( A )),bind(B,$thf( F @ ( E @ ordered_pair ) )),bind(C,$thf( E )),bind(D,$thf( F ))]]) ).
thf(578,plain,
! [B: $i,A: $i] :
~ ( sk12 @ singleton @ ( B @ ( A @ ordered_pair ) @ in ) ),
inference(simp,[status(thm)],[477]) ).
thf(2510,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ ( C @ ( B @ ordered_pair ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,578]) ).
thf(2511,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ ( C @ ( B @ ordered_pair ) @ in ) ) ),
inference(simp,[status(thm)],[2510]) ).
thf(2519,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton )
!= ( sk12 @ singleton ) )
| ( A
!= ( C @ ( B @ ordered_pair ) ) ) ),
inference(simp,[status(thm)],[2511]) ).
thf(2530,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) @ singleton )
!= ( sk12 @ singleton ) ),
inference(simp,[status(thm)],[2519]) ).
thf(3247,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ordered_pair ) @ singleton ) )
| ( A
!= ( sk12 @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,2530]) ).
thf(3248,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton ) )
| ~ ( A @ singleton @ ( C @ ( B @ ordered_pair ) @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[3247:[bind(A,$thf( A )),bind(B,$thf( G @ ( F @ ordered_pair ) @ singleton )),bind(C,$thf( F )),bind(D,$thf( G ))]]) ).
thf(3261,plain,
! [B: $i,A: $i] :
~ ( sk12 @ singleton @ singleton @ ( B @ ( A @ ordered_pair ) @ singleton @ in ) ),
inference(simp,[status(thm)],[3248]) ).
thf(6916,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ ( C @ ( B @ ordered_pair ) @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,3261]) ).
thf(6917,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ ( C @ ( B @ ordered_pair ) @ singleton @ in ) ) ),
inference(simp,[status(thm)],[6916]) ).
thf(6945,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton )
!= ( sk12 @ singleton @ singleton ) )
| ( A
!= ( C @ ( B @ ordered_pair ) @ singleton ) ) ),
inference(simp,[status(thm)],[6917]) ).
thf(6960,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) @ singleton @ singleton )
!= ( sk12 @ singleton @ singleton ) ),
inference(simp,[status(thm)],[6945]) ).
thf(7103,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A
!= ( D @ ( C @ ordered_pair ) @ singleton @ singleton ) )
| ( B
!= ( sk12 @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,6960]) ).
thf(7104,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton ) )
| ~ ( C @ ( B @ ordered_pair ) @ singleton @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[7103:[bind(A,$thf( H @ ( G @ ordered_pair ) @ singleton @ singleton )),bind(B,$thf( B )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(7127,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ ordered_pair ) @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[7104]) ).
thf(9335,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( C @ ( B @ ordered_pair ) @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,7127]) ).
thf(9336,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( C @ ( B @ ordered_pair ) @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ in ) ) ),
inference(simp,[status(thm)],[9335]) ).
thf(9376,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton )
!= ( C @ ( B @ ordered_pair ) @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk12 @ singleton @ singleton ) ) ),
inference(simp,[status(thm)],[9336]) ).
thf(9407,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) @ singleton @ singleton @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton ) ),
inference(simp,[status(thm)],[9376]) ).
thf(9590,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ordered_pair ) @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk12 @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,9407]) ).
thf(9591,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( C @ ( B @ ordered_pair ) @ singleton @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[9590:[bind(A,$thf( A )),bind(B,$thf( I @ ( H @ ordered_pair ) @ singleton @ singleton @ singleton )),bind(C,$thf( H )),bind(D,$thf( I ))]]) ).
thf(9653,plain,
! [B: $i,A: $i] :
~ ( sk12 @ singleton @ singleton @ singleton @ singleton @ ( B @ ( A @ ordered_pair ) @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[9591]) ).
thf(12,axiom,
! [A: $i,B: $i] :
( ! [C: $i] :
( ( A @ ( C @ in ) )
<=> ( B @ ( C @ in ) ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_tarski) ).
thf(93,plain,
! [A: $i,B: $i] :
( ! [C: $i] :
( ( ( B @ ( C @ in ) )
=> ( A @ ( C @ in ) ) )
& ( ( A @ ( C @ in ) )
=> ( B @ ( C @ in ) ) ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(94,plain,
! [A: $i,B: $i] :
( ( ! [C: $i] :
( ( B @ ( C @ in ) )
=> ( A @ ( C @ in ) ) )
& ! [C: $i] :
( ( A @ ( C @ in ) )
=> ( B @ ( C @ in ) ) ) )
=> ( A = B ) ),
inference(miniscope,[status(thm)],[93]) ).
thf(95,plain,
! [B: $i,A: $i] :
( ( ( A = B )
| ~ ( A @ ( A @ ( B @ sk15 ) @ in ) )
| ~ ( B @ ( A @ ( B @ sk14 ) @ in ) ) )
& ( ( A = B )
| ( B @ ( A @ ( B @ sk15 ) @ in ) )
| ~ ( B @ ( A @ ( B @ sk14 ) @ in ) ) )
& ( ( A = B )
| ~ ( A @ ( A @ ( B @ sk15 ) @ in ) )
| ( A @ ( A @ ( B @ sk14 ) @ in ) ) )
& ( ( A = B )
| ( B @ ( A @ ( B @ sk15 ) @ in ) )
| ( A @ ( A @ ( B @ sk14 ) @ in ) ) ) ),
inference(cnf,[status(esa)],[94]) ).
thf(97,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( A @ ( B @ sk15 ) @ in ) )
| ( A @ ( A @ ( B @ sk14 ) @ in ) ) ),
inference(cnfConj,[status(thm)],[95]) ).
thf(101,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( A @ ( B @ sk15 ) @ in ) )
| ( A @ ( A @ ( B @ sk14 ) @ in ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[97]) ).
thf(346,plain,
! [B: $i,A: $i] :
( ( B != sk2 )
| ( ( A @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(347,plain,
! [A: $i] :
( ( ( A @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( sk2 @ in ) ) ),
inference(pattern_uni,[status(thm)],[346:[bind(A,$thf( A )),bind(B,$thf( sk2 ))]]) ).
thf(845,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ ( sk2 @ singleton @ ( A @ singleton @ cartesian_product2 ) @ in ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,519]) ).
thf(846,plain,
! [A: $i] :
( ~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ ( sk2 @ singleton @ ( A @ singleton @ cartesian_product2 ) @ in ) )
| ~ ( A @ singleton @ ( sk1 @ in ) ) ),
inference(pattern_uni,[status(thm)],[845:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(875,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,519]) ).
thf(876,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) ) ),
inference(simp,[status(thm)],[875]) ).
thf(877,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton ) )
| ( A
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) ) ),
inference(simp,[status(thm)],[876]) ).
thf(890,plain,
( ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton ) ),
inference(simp,[status(thm)],[877]) ).
thf(1599,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton ) )
| ( B
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,890]) ).
thf(1600,plain,
! [A: $i] :
( ( A
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton ) )
| ~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[1599:[bind(A,$thf( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton )),bind(B,$thf( B ))]]) ).
thf(1637,plain,
~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ in ) ),
inference(simp,[status(thm)],[1600]) ).
thf(1986,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,1637]) ).
thf(1987,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ in ) ) ),
inference(simp,[status(thm)],[1986]) ).
thf(2020,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton ) ) ),
inference(simp,[status(thm)],[1987]) ).
thf(2028,plain,
( ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton ) ),
inference(simp,[status(thm)],[2020]) ).
thf(3333,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton ) )
| ( B
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,2028]) ).
thf(3334,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton ) )
| ~ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[3333:[bind(A,$thf( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton )),bind(B,$thf( B ))]]) ).
thf(3386,plain,
~ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[3334]) ).
thf(8259,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,3386]) ).
thf(8260,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ in ) ) ),
inference(simp,[status(thm)],[8259]) ).
thf(8333,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton ) ) ),
inference(simp,[status(thm)],[8260]) ).
thf(8340,plain,
( ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton ) ),
inference(simp,[status(thm)],[8333]) ).
thf(11422,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,8340]) ).
thf(11423,plain,
! [A: $i] :
( ( A
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[11422:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton ))]]) ).
thf(11581,plain,
~ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[11423]) ).
thf(4,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ unordered_pair ) )
= ( A @ ( B @ unordered_pair ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
thf(18,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ unordered_pair ) )
= ( A @ ( B @ unordered_pair ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(19,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) )
= ( A @ ( B @ unordered_pair ) ) ),
inference(cnf,[status(esa)],[18]) ).
thf(20,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) )
= ( A @ ( B @ unordered_pair ) ) ),
inference(lifteq,[status(thm)],[19]) ).
thf(7,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
thf(75,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(76,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) )
= ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) ) ),
inference(cnf,[status(esa)],[75]) ).
thf(77,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) )
= ( B @ ( A @ ordered_pair ) ) ),
inference(lifteq,[status(thm)],[76]) ).
thf(233,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( D @ ( C @ unordered_pair ) ) )
| ( ( C @ singleton @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) )
= ( D @ ( C @ ordered_pair ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,77]) ).
thf(234,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( A @ ( B @ unordered_pair ) @ unordered_pair ) )
= ( B @ ( A @ ordered_pair ) ) ),
inference(pattern_uni,[status(thm)],[233:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(366,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( ( sk2 @ singleton @ ( B @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(367,plain,
! [A: $i] :
( ( ( sk2 @ singleton @ ( A @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( sk1 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[366:[bind(A,$thf( sk1 ))]]) ).
thf(523,plain,
! [A: $i] :
( ( ( sk2 @ singleton @ ( A @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( sk1 @ singleton @ ( A @ in ) ) ),
inference(simp,[status(thm)],[367]) ).
thf(6,axiom,
! [A: $i,B: $i,C: $i] :
( ( C
= ( B @ ( A @ cartesian_product2 ) ) )
<=> ! [D: $i] :
( ( C @ ( D @ in ) )
<=> ? [E: $i,F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) )
& ( A @ ( E @ in ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_zfmisc_1) ).
thf(42,plain,
! [A: $i,B: $i,C: $i] :
( ( ! [D: $i] :
( ( ? [E: $i,F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) )
& ( A @ ( E @ in ) ) )
=> ( C @ ( D @ in ) ) )
& ( ( C @ ( D @ in ) )
=> ? [E: $i,F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) )
& ( A @ ( E @ in ) ) ) ) )
=> ( C
= ( B @ ( A @ cartesian_product2 ) ) ) )
& ( ( C
= ( B @ ( A @ cartesian_product2 ) ) )
=> ! [D: $i] :
( ( ? [E: $i,F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) )
& ( A @ ( E @ in ) ) )
=> ( C @ ( D @ in ) ) )
& ( ( C @ ( D @ in ) )
=> ? [E: $i,F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) )
& ( A @ ( E @ in ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(43,plain,
( ! [A: $i,B: $i,C: $i] :
( ( ! [D: $i] :
( ? [E: $i] :
( ? [F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) ) )
& ( A @ ( E @ in ) ) )
=> ( C @ ( D @ in ) ) )
& ! [D: $i] :
( ( C @ ( D @ in ) )
=> ? [E: $i] :
( ? [F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) ) )
& ( A @ ( E @ in ) ) ) ) )
=> ( C
= ( B @ ( A @ cartesian_product2 ) ) ) )
& ! [A: $i,B: $i,C: $i] :
( ( C
= ( B @ ( A @ cartesian_product2 ) ) )
=> ( ! [D: $i] :
( ? [E: $i] :
( ? [F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) ) )
& ( A @ ( E @ in ) ) )
=> ( C @ ( D @ in ) ) )
& ! [D: $i] :
( ( C @ ( D @ in ) )
=> ? [E: $i] :
( ? [F: $i] :
( ( D
= ( F @ ( E @ ordered_pair ) ) )
& ( B @ ( F @ in ) ) )
& ( A @ ( E @ in ) ) ) ) ) ) ),
inference(miniscope,[status(thm)],[42]) ).
thf(44,plain,
! [L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( J
= ( I @ ( H @ cartesian_product2 ) ) )
| ~ ( J @ ( H @ ( I @ ( J @ sk9 ) ) @ in ) )
| ( J @ ( I @ ( H @ sk7 ) ) ) )
& ( ( J
= ( I @ ( H @ cartesian_product2 ) ) )
| ( ( H @ ( I @ ( J @ sk9 ) ) )
= ( H @ ( I @ ( J @ sk11 ) ) @ ( H @ ( I @ ( J @ sk10 ) ) @ ordered_pair ) ) )
| ( J @ ( I @ ( H @ sk7 ) ) ) )
& ( ( J
= ( I @ ( H @ cartesian_product2 ) ) )
| ( I @ ( H @ ( I @ ( J @ sk11 ) ) @ in ) )
| ( J @ ( I @ ( H @ sk7 ) ) ) )
& ( ( J
= ( I @ ( H @ cartesian_product2 ) ) )
| ( H @ ( H @ ( I @ ( J @ sk10 ) ) @ in ) )
| ( J @ ( I @ ( H @ sk7 ) ) ) )
& ( ( J
= ( I @ ( H @ cartesian_product2 ) ) )
| ~ ( J @ ( I @ ( H @ sk7 ) ) )
| ( ( H @ ( I @ ( J @ sk8 ) ) )
!= ( L @ ( K @ ordered_pair ) ) )
| ~ ( I @ ( L @ in ) )
| ~ ( H @ ( K @ in ) ) )
& ( ( J
= ( I @ ( H @ cartesian_product2 ) ) )
| ~ ( J @ ( I @ ( H @ sk7 ) ) )
| ( J @ ( H @ ( I @ ( J @ sk8 ) ) @ in ) ) )
& ( ( C @ ( E @ in ) )
| ( E
!= ( G @ ( F @ ordered_pair ) ) )
| ~ ( B @ ( G @ in ) )
| ~ ( A @ ( F @ in ) )
| ( C
!= ( B @ ( A @ cartesian_product2 ) ) ) )
& ( ( D
= ( A @ ( B @ ( C @ ( D @ sk6 ) ) ) @ ( A @ ( B @ ( C @ ( D @ sk5 ) ) ) @ ordered_pair ) ) )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ cartesian_product2 ) ) ) )
& ( ( B @ ( A @ ( B @ ( C @ ( D @ sk6 ) ) ) @ in ) )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ cartesian_product2 ) ) ) )
& ( ( A @ ( A @ ( B @ ( C @ ( D @ sk5 ) ) ) @ in ) )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ cartesian_product2 ) ) ) ) ),
inference(cnf,[status(esa)],[43]) ).
thf(53,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D
= ( A @ ( B @ ( C @ ( D @ sk6 ) ) ) @ ( A @ ( B @ ( C @ ( D @ sk5 ) ) ) @ ordered_pair ) ) )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(59,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( D @ in ) )
| ( ( A @ ( B @ ( C @ ( D @ sk6 ) ) ) @ ( A @ ( B @ ( C @ ( D @ sk5 ) ) ) @ ordered_pair ) )
= D )
| ( C
!= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(lifteq,[status(thm)],[53]) ).
thf(60,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ cartesian_product2 ) @ ( C @ in ) )
| ( ( A @ ( B @ ( B @ ( A @ cartesian_product2 ) @ ( C @ sk6 ) ) ) @ ( A @ ( B @ ( B @ ( A @ cartesian_product2 ) @ ( C @ sk5 ) ) ) @ ordered_pair ) )
= C ) ),
inference(simp,[status(thm)],[59]) ).
thf(3677,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ ( A @ cartesian_product2 ) @ ( C @ sk6 ) ) ) @ ( A @ ( B @ ( B @ ( A @ cartesian_product2 ) @ ( C @ sk5 ) ) ) @ ordered_pair ) )
!= ( E @ ( D @ ordered_pair ) ) )
| ( C != sk12 )
| ~ ( B @ ( A @ cartesian_product2 ) @ ( C @ in ) ) ),
inference(paramod_ordered,[status(thm)],[60,109]) ).
thf(3678,plain,
! [C: $i,B: $i,A: $i] :
( ( A != sk12 )
| ~ ( B @ ( C @ cartesian_product2 ) @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[3677:[bind(A,$thf( O )),bind(B,$thf( N )),bind(C,$thf( L )),bind(D,$thf( O @ ( N @ ( N @ ( O @ cartesian_product2 ) @ ( L @ sk5 ) ) ) )),bind(E,$thf( O @ ( N @ ( N @ ( O @ cartesian_product2 ) @ ( L @ sk6 ) ) ) ))]]) ).
thf(3758,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ cartesian_product2 ) @ ( sk12 @ in ) ),
inference(simp,[status(thm)],[3678]) ).
thf(3787,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( B @ ( C @ cartesian_product2 ) @ ( sk12 @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,3758]) ).
thf(3788,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( B @ ( C @ cartesian_product2 ) @ ( sk12 @ in ) ) ),
inference(simp,[status(thm)],[3787]) ).
thf(3793,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton )
!= ( B @ ( C @ cartesian_product2 ) ) )
| ( A != sk12 ) ),
inference(simp,[status(thm)],[3788]) ).
thf(3796,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ cartesian_product2 ) )
!= ( sk12 @ singleton ) ),
inference(simp,[status(thm)],[3793]) ).
thf(3808,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( C @ ( D @ cartesian_product2 ) ) )
| ( A
!= ( sk12 @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,3796]) ).
thf(3809,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton ) )
| ~ ( A @ singleton @ ( C @ ( B @ cartesian_product2 ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[3808:[bind(A,$thf( A )),bind(B,$thf( F @ ( E @ cartesian_product2 ) )),bind(C,$thf( F )),bind(D,$thf( E ))]]) ).
thf(3814,plain,
! [B: $i,A: $i] :
~ ( sk12 @ singleton @ singleton @ ( B @ ( A @ cartesian_product2 ) @ in ) ),
inference(simp,[status(thm)],[3809]) ).
thf(3848,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ ( C @ ( B @ cartesian_product2 ) @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,3814]) ).
thf(3849,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ ( C @ ( B @ cartesian_product2 ) @ in ) ) ),
inference(simp,[status(thm)],[3848]) ).
thf(3862,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton )
!= ( sk12 @ singleton @ singleton ) )
| ( A
!= ( C @ ( B @ cartesian_product2 ) ) ) ),
inference(simp,[status(thm)],[3849]) ).
thf(3875,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ cartesian_product2 ) @ singleton )
!= ( sk12 @ singleton @ singleton ) ),
inference(simp,[status(thm)],[3862]) ).
thf(5067,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ cartesian_product2 ) @ singleton ) )
| ( A
!= ( sk12 @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,3875]) ).
thf(5068,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( C @ ( B @ cartesian_product2 ) @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[5067:[bind(A,$thf( A )),bind(B,$thf( G @ ( F @ cartesian_product2 ) @ singleton )),bind(C,$thf( F )),bind(D,$thf( G ))]]) ).
thf(5089,plain,
! [B: $i,A: $i] :
~ ( sk12 @ singleton @ singleton @ singleton @ ( B @ ( A @ cartesian_product2 ) @ singleton @ in ) ),
inference(simp,[status(thm)],[5068]) ).
thf(7875,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ singleton @ ( C @ ( B @ cartesian_product2 ) @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,5089]) ).
thf(7876,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ singleton @ ( C @ ( B @ cartesian_product2 ) @ singleton @ in ) ) ),
inference(simp,[status(thm)],[7875]) ).
thf(7910,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton ) )
| ( A
!= ( C @ ( B @ cartesian_product2 ) @ singleton ) ) ),
inference(simp,[status(thm)],[7876]) ).
thf(7935,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ cartesian_product2 ) @ singleton @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton ) ),
inference(simp,[status(thm)],[7910]) ).
thf(116,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( A @ ( B @ in ) )
!= ( B @ ( A @ in ) ) )
| ~ ( B @ ( A @ in ) ) ),
inference(eqfactor_ordered,[status(thm)],[17]) ).
thf(117,plain,
! [A: $i] :
~ ( A @ ( A @ in ) ),
inference(pattern_uni,[status(thm)],[116:[bind(A,$thf( B ))]]) ).
thf(120,plain,
! [A: $i] :
~ ( A @ ( A @ in ) ),
inference(simp,[status(thm)],[117]) ).
thf(11,axiom,
? [A: $i] :
~ ( A @ empty ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
thf(90,plain,
? [A: $i] :
~ ( A @ empty ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(91,plain,
~ ! [A: $i] : ( A @ empty ),
inference(miniscope,[status(thm)],[90]) ).
thf(92,plain,
~ ( sk13 @ empty ),
inference(cnf,[status(esa)],[91]) ).
thf(104,plain,
( ( ( sk13 @ empty )
!= ( sk12 @ empty ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[89,92]) ).
thf(105,plain,
( ( sk13 @ empty )
!= ( sk12 @ empty ) ),
inference(simp,[status(thm)],[104]) ).
thf(106,plain,
sk13 != sk12,
inference(simp,[status(thm)],[105]) ).
thf(432,plain,
! [B: $i,A: $i] :
( ( B != sk13 )
| ( A != sk12 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,106]) ).
thf(433,plain,
! [A: $i] :
( ( A != sk12 )
| ~ ( A @ singleton @ ( sk13 @ in ) ) ),
inference(pattern_uni,[status(thm)],[432:[bind(A,$thf( A )),bind(B,$thf( sk13 ))]]) ).
thf(556,plain,
~ ( sk12 @ singleton @ ( sk13 @ in ) ),
inference(simp,[status(thm)],[433]) ).
thf(604,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton ) )
| ~ ( B @ ( sk13 @ in ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,556]) ).
thf(605,plain,
! [A: $i] :
( ~ ( A @ ( sk13 @ in ) )
| ~ ( sk12 @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[604:[bind(A,$thf( sk12 @ singleton )),bind(B,$thf( B ))]]) ).
thf(614,plain,
! [A: $i] :
( ~ ( A @ ( sk13 @ in ) )
| ~ ( sk12 @ singleton @ singleton @ ( A @ in ) ) ),
inference(simp,[status(thm)],[605]) ).
thf(596,plain,
! [B: $i,A: $i] :
( ( B != sk13 )
| ~ ( sk12 @ singleton @ ( A @ in ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,556]) ).
thf(597,plain,
! [A: $i] :
( ~ ( sk12 @ singleton @ ( A @ in ) )
| ~ ( A @ singleton @ ( sk13 @ in ) ) ),
inference(pattern_uni,[status(thm)],[596:[bind(A,$thf( A )),bind(B,$thf( sk13 ))]]) ).
thf(52,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( B @ ( A @ cartesian_product2 ) ) )
| ( A @ ( A @ ( B @ ( C @ sk10 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk7 ) ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(55,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( A @ ( B @ ( C @ sk10 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk7 ) ) )
| ( C
= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(lifteq,[status(thm)],[52]) ).
thf(56,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( A @ ( B @ ( C @ sk10 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk7 ) ) )
| ( C
= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(simp,[status(thm)],[55]) ).
thf(14290,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ ( C @ ( B @ ordered_pair ) @ singleton @ singleton @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,9653]) ).
thf(14291,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ ( C @ ( B @ ordered_pair ) @ singleton @ singleton @ singleton @ in ) ) ),
inference(simp,[status(thm)],[14290]) ).
thf(14346,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton ) )
| ( A
!= ( C @ ( B @ ordered_pair ) @ singleton @ singleton @ singleton ) ) ),
inference(simp,[status(thm)],[14291]) ).
thf(14354,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton ) ),
inference(simp,[status(thm)],[14346]) ).
thf(171,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( B @ ( B @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,120]) ).
thf(172,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( B @ ( B @ in ) ) ),
inference(simp,[status(thm)],[171]) ).
thf(173,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton )
!= B )
| ( A != B ) ),
inference(simp,[status(thm)],[172]) ).
thf(174,plain,
! [A: $i] :
( ( A @ singleton )
!= A ),
inference(simp,[status(thm)],[173]) ).
thf(9598,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A
!= ( D @ ( C @ ordered_pair ) @ singleton @ singleton @ singleton ) )
| ( B
!= ( sk12 @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,9407]) ).
thf(9599,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton @ singleton ) )
| ~ ( C @ ( B @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[9598:[bind(A,$thf( I @ ( H @ ordered_pair ) @ singleton @ singleton @ singleton )),bind(B,$thf( B )),bind(C,$thf( H )),bind(D,$thf( I ))]]) ).
thf(9657,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[9599]) ).
thf(26,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk4 ) )
= A )
| ( B @ ( A @ ( B @ sk3 ) @ in ) ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(36,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ sk3 ) @ in ) )
| ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk4 ) )
= A ) ),
inference(lifteq,[status(thm)],[26]) ).
thf(37,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ sk3 ) @ in ) )
| ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk4 ) )
= A ) ),
inference(simp,[status(thm)],[36]) ).
thf(3251,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A
!= ( D @ ( C @ ordered_pair ) @ singleton ) )
| ( B
!= ( sk12 @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,2530]) ).
thf(3252,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton ) )
| ~ ( C @ ( B @ ordered_pair ) @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[3251:[bind(A,$thf( G @ ( F @ ordered_pair ) @ singleton )),bind(B,$thf( B )),bind(C,$thf( F )),bind(D,$thf( G ))]]) ).
thf(3263,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ ordered_pair ) @ singleton @ singleton @ ( sk12 @ singleton @ in ) ),
inference(simp,[status(thm)],[3252]) ).
thf(310,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ singleton ) )
| ( B != C )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,174]) ).
thf(311,plain,
! [B: $i,A: $i] :
( ( A != B )
| ~ ( B @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[310:[bind(A,$thf( D @ singleton )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(504,plain,
! [A: $i] :
~ ( A @ singleton @ singleton @ ( A @ in ) ),
inference(simp,[status(thm)],[311]) ).
thf(837,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk1 @ singleton ) )
| ~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ ( sk2 @ singleton @ ( A @ cartesian_product2 ) @ in ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,519]) ).
thf(838,plain,
! [A: $i] :
( ~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ ( sk2 @ singleton @ ( A @ cartesian_product2 ) @ in ) )
| ~ ( A @ singleton @ ( sk1 @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[837:[bind(A,$thf( A )),bind(B,$thf( sk1 @ singleton ))]]) ).
thf(356,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk2 @ ( sk1 @ ordered_pair ) ) )
| ( ( A @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(357,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( A @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[356:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ( sk1 @ ordered_pair ) ))]]) ).
thf(5071,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A
!= ( D @ ( C @ cartesian_product2 ) @ singleton ) )
| ( B
!= ( sk12 @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,3875]) ).
thf(5072,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton ) )
| ~ ( C @ ( B @ cartesian_product2 ) @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[5071:[bind(A,$thf( G @ ( F @ cartesian_product2 ) @ singleton )),bind(B,$thf( B )),bind(C,$thf( F )),bind(D,$thf( G ))]]) ).
thf(5091,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ cartesian_product2 ) @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[5072]) ).
thf(608,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ ( sk13 @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,556]) ).
thf(609,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ ( sk13 @ in ) ) ),
inference(simp,[status(thm)],[608]) ).
thf(610,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk12 @ singleton ) )
| ( A != sk13 ) ),
inference(simp,[status(thm)],[609]) ).
thf(611,plain,
( ( sk13 @ singleton )
!= ( sk12 @ singleton ) ),
inference(simp,[status(thm)],[610]) ).
thf(648,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk13 @ singleton ) )
| ( A
!= ( sk12 @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,611]) ).
thf(649,plain,
! [A: $i] :
( ( A
!= ( sk12 @ singleton ) )
| ~ ( A @ singleton @ ( sk13 @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[648:[bind(A,$thf( A )),bind(B,$thf( sk13 @ singleton ))]]) ).
thf(657,plain,
~ ( sk12 @ singleton @ singleton @ ( sk13 @ singleton @ in ) ),
inference(simp,[status(thm)],[649]) ).
thf(694,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ ( sk13 @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,657]) ).
thf(695,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ ( sk13 @ singleton @ in ) ) ),
inference(simp,[status(thm)],[694]) ).
thf(696,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk12 @ singleton @ singleton ) )
| ( A
!= ( sk13 @ singleton ) ) ),
inference(simp,[status(thm)],[695]) ).
thf(703,plain,
( ( sk13 @ singleton @ singleton )
!= ( sk12 @ singleton @ singleton ) ),
inference(simp,[status(thm)],[696]) ).
thf(1010,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk13 @ singleton @ singleton ) )
| ( B
!= ( sk12 @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,703]) ).
thf(1011,plain,
! [A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton ) )
| ~ ( sk13 @ singleton @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[1010:[bind(A,$thf( sk13 @ singleton @ singleton )),bind(B,$thf( B ))]]) ).
thf(1016,plain,
~ ( sk13 @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[1011]) ).
thf(1072,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk13 @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,1016]) ).
thf(1073,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk13 @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ in ) ) ),
inference(simp,[status(thm)],[1072]) ).
thf(1074,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk13 @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk12 @ singleton @ singleton ) ) ),
inference(simp,[status(thm)],[1073]) ).
thf(1087,plain,
( ( sk13 @ singleton @ singleton @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton ) ),
inference(simp,[status(thm)],[1074]) ).
thf(1168,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk13 @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk12 @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,1087]) ).
thf(1169,plain,
! [A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( sk13 @ singleton @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[1168:[bind(A,$thf( A )),bind(B,$thf( sk13 @ singleton @ singleton @ singleton ))]]) ).
thf(1187,plain,
~ ( sk12 @ singleton @ singleton @ singleton @ singleton @ ( sk13 @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[1169]) ).
thf(1346,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ ( sk13 @ singleton @ singleton @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,1187]) ).
thf(1347,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ ( sk13 @ singleton @ singleton @ singleton @ in ) ) ),
inference(simp,[status(thm)],[1346]) ).
thf(1348,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk13 @ singleton @ singleton @ singleton ) ) ),
inference(simp,[status(thm)],[1347]) ).
thf(1350,plain,
( ( sk13 @ singleton @ singleton @ singleton @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton ) ),
inference(simp,[status(thm)],[1348]) ).
thf(1457,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk13 @ singleton @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk12 @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,1350]) ).
thf(1458,plain,
! [A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( sk13 @ singleton @ singleton @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[1457:[bind(A,$thf( A )),bind(B,$thf( sk13 @ singleton @ singleton @ singleton @ singleton ))]]) ).
thf(1495,plain,
~ ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ ( sk13 @ singleton @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[1458]) ).
thf(1768,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ ( sk13 @ singleton @ singleton @ singleton @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,1495]) ).
thf(1769,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ ( sk13 @ singleton @ singleton @ singleton @ singleton @ in ) ) ),
inference(simp,[status(thm)],[1768]) ).
thf(1808,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk13 @ singleton @ singleton @ singleton @ singleton ) ) ),
inference(simp,[status(thm)],[1769]) ).
thf(1817,plain,
( ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton ) ),
inference(simp,[status(thm)],[1808]) ).
thf(2632,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,1817]) ).
thf(2633,plain,
! [A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[2632:[bind(A,$thf( A )),bind(B,$thf( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton ))]]) ).
thf(2674,plain,
~ ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[2633]) ).
thf(5191,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,2674]) ).
thf(5192,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ in ) ) ),
inference(simp,[status(thm)],[5191]) ).
thf(5255,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton ) ) ),
inference(simp,[status(thm)],[5192]) ).
thf(5259,plain,
( ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton ) ),
inference(simp,[status(thm)],[5255]) ).
thf(7162,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,5259]) ).
thf(7163,plain,
! [A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[7162:[bind(A,$thf( A )),bind(B,$thf( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton ))]]) ).
thf(7236,plain,
~ ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[7163]) ).
thf(7176,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ( B
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,5259]) ).
thf(7177,plain,
! [A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[7176:[bind(A,$thf( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton )),bind(B,$thf( B ))]]) ).
thf(7226,plain,
~ ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[7177]) ).
thf(29,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ singleton ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ in ) )
| ( B @ ( A @ ( B @ sk3 ) @ in ) ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(30,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk4 ) @ in ) )
| ( B @ ( A @ ( B @ sk3 ) @ in ) )
| ( B
= ( A @ singleton ) ) ),
inference(lifteq,[status(thm)],[29]) ).
thf(31,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk4 ) @ in ) )
| ( B @ ( A @ ( B @ sk3 ) @ in ) )
| ( B
= ( A @ singleton ) ) ),
inference(simp,[status(thm)],[30]) ).
thf(146,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton )
!= ( sk1 @ singleton ) )
| ( ( sk2 @ singleton @ ( B @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ in ) )
| ( B @ ( A @ ( B @ sk3 ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[31,15]) ).
thf(147,plain,
! [A: $i] :
( ( ( sk2 @ singleton @ ( A @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ ( sk1 @ ( A @ sk4 ) @ in ) )
| ( A @ ( sk1 @ ( A @ sk3 ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[146:[bind(A,$thf( sk1 ))]]) ).
thf(164,plain,
! [A: $i] :
( ( ( sk2 @ singleton @ ( A @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ ( sk1 @ ( A @ sk4 ) @ in ) )
| ( A @ ( sk1 @ ( A @ sk3 ) @ in ) ) ),
inference(simp,[status(thm)],[147]) ).
thf(15998,plain,
! [A: $i] :
( ~ $true
| ( ( A @ ( sk13 @ in ) )
!= ( sk12 @ singleton @ singleton @ ( A @ in ) ) )
| ~ ( sk12 @ singleton @ singleton @ ( A @ in ) ) ),
inference(eqfactor_ordered,[status(thm)],[614]) ).
thf(16004,plain,
! [A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton ) )
| ( sk13 != A )
| ~ ( sk12 @ singleton @ singleton @ ( A @ in ) ) ),
inference(simp,[status(thm)],[15998]) ).
thf(16018,plain,
( ( ( sk12 @ singleton @ singleton )
!= sk13 )
| ~ ( sk12 @ singleton @ singleton @ ( sk13 @ in ) ) ),
inference(simp,[status(thm)],[16004]) ).
thf(9,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ cartesian_product2 ) @ ( B @ ( A @ ordered_pair ) @ in ) )
<=> ( ( D @ ( B @ in ) )
& ( C @ ( A @ in ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l55_zfmisc_1) ).
thf(81,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( ( D @ ( B @ in ) )
& ( C @ ( A @ in ) ) )
=> ( D @ ( C @ cartesian_product2 ) @ ( B @ ( A @ ordered_pair ) @ in ) ) )
& ( ( D @ ( C @ cartesian_product2 ) @ ( B @ ( A @ ordered_pair ) @ in ) )
=> ( ( D @ ( B @ in ) )
& ( C @ ( A @ in ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(82,plain,
( ! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( B @ in ) )
& ( C @ ( A @ in ) ) )
=> ( D @ ( C @ cartesian_product2 ) @ ( B @ ( A @ ordered_pair ) @ in ) ) )
& ! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ cartesian_product2 ) @ ( B @ ( A @ ordered_pair ) @ in ) )
=> ( ( D @ ( B @ in ) )
& ( C @ ( A @ in ) ) ) ) ),
inference(miniscope,[status(thm)],[81]) ).
thf(83,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( H @ ( G @ cartesian_product2 ) @ ( F @ ( E @ ordered_pair ) @ in ) )
| ~ ( H @ ( F @ in ) )
| ~ ( G @ ( E @ in ) ) )
& ( ( D @ ( B @ in ) )
| ~ ( D @ ( C @ cartesian_product2 ) @ ( B @ ( A @ ordered_pair ) @ in ) ) )
& ( ( C @ ( A @ in ) )
| ~ ( D @ ( C @ cartesian_product2 ) @ ( B @ ( A @ ordered_pair ) @ in ) ) ) ),
inference(cnf,[status(esa)],[82]) ).
thf(84,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( A @ in ) )
| ~ ( D @ ( C @ cartesian_product2 ) @ ( B @ ( A @ ordered_pair ) @ in ) ) ),
inference(cnfConj,[status(thm)],[83]) ).
thf(352,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk2 @ singleton ) )
| ( ( A @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(353,plain,
! [A: $i] :
( ( ( A @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( sk2 @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[352:[bind(A,$thf( A )),bind(B,$thf( sk2 @ singleton ))]]) ).
thf(374,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ ordered_pair ) ) )
| ( ( B @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(375,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[374:[bind(A,$thf( sk2 @ ( sk1 @ ordered_pair ) )),bind(B,$thf( B ))]]) ).
thf(527,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ ( A @ in ) ) ),
inference(simp,[status(thm)],[375]) ).
thf(49,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( B @ ( A @ cartesian_product2 ) ) )
| ( ( A @ ( B @ ( C @ sk9 ) ) )
= ( A @ ( B @ ( C @ sk11 ) ) @ ( A @ ( B @ ( C @ sk10 ) ) @ ordered_pair ) ) )
| ( C @ ( B @ ( A @ sk7 ) ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(73,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ sk7 ) ) )
| ( C
= ( B @ ( A @ cartesian_product2 ) ) )
| ( ( A @ ( B @ ( C @ sk9 ) ) )
= ( A @ ( B @ ( C @ sk11 ) ) @ ( A @ ( B @ ( C @ sk10 ) ) @ ordered_pair ) ) ) ),
inference(lifteq,[status(thm)],[49]) ).
thf(74,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ sk7 ) ) )
| ( C
= ( B @ ( A @ cartesian_product2 ) ) )
| ( ( A @ ( B @ ( C @ sk9 ) ) )
= ( A @ ( B @ ( C @ sk11 ) ) @ ( A @ ( B @ ( C @ sk10 ) ) @ ordered_pair ) ) ) ),
inference(simp,[status(thm)],[73]) ).
thf(378,plain,
! [B: $i,A: $i] :
( ( A != sk2 )
| ( ( B @ ( sk1 @ ordered_pair ) @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(379,plain,
! [A: $i] :
( ( ( A @ ( sk1 @ ordered_pair ) @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( sk2 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[378:[bind(A,$thf( sk2 ))]]) ).
thf(529,plain,
! [A: $i] :
( ( ( A @ ( sk1 @ ordered_pair ) @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( sk2 @ singleton @ ( A @ in ) ) ),
inference(simp,[status(thm)],[379]) ).
thf(85,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ in ) )
| ~ ( D @ ( C @ cartesian_product2 ) @ ( B @ ( A @ ordered_pair ) @ in ) ) ),
inference(cnfConj,[status(thm)],[83]) ).
thf(1004,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk13 @ singleton @ singleton ) )
| ( A
!= ( sk12 @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,703]) ).
thf(1005,plain,
! [A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( sk13 @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[1004:[bind(A,$thf( A )),bind(B,$thf( sk13 @ singleton @ singleton ))]]) ).
thf(1021,plain,
~ ( sk12 @ singleton @ singleton @ singleton @ ( sk13 @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[1005]) ).
thf(1245,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( B @ singleton @ singleton @ ( B @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,504]) ).
thf(1246,plain,
! [B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( B @ singleton @ singleton @ ( B @ in ) ) ),
inference(simp,[status(thm)],[1245]) ).
thf(1247,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton )
!= ( B @ singleton @ singleton ) )
| ( A != B ) ),
inference(simp,[status(thm)],[1246]) ).
thf(1255,plain,
! [A: $i] :
( ( A @ singleton @ singleton )
!= ( A @ singleton ) ),
inference(simp,[status(thm)],[1247]) ).
thf(348,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ( ( sk2 @ singleton @ ( A @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(349,plain,
! [A: $i] :
( ( ( sk2 @ singleton @ ( A @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( sk1 @ in ) ) ),
inference(pattern_uni,[status(thm)],[348:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(47,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( B @ ( A @ cartesian_product2 ) ) )
| ~ ( C @ ( B @ ( A @ sk7 ) ) )
| ( C @ ( A @ ( B @ ( C @ sk8 ) ) @ in ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(69,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ sk7 ) ) )
| ( C @ ( A @ ( B @ ( C @ sk8 ) ) @ in ) )
| ( C
= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(lifteq,[status(thm)],[47]) ).
thf(70,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ sk7 ) ) )
| ( C @ ( A @ ( B @ ( C @ sk8 ) ) @ in ) )
| ( C
= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(simp,[status(thm)],[69]) ).
thf(11432,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,8340]) ).
thf(11433,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[11432:[bind(A,$thf( A )),bind(B,$thf( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton ))]]) ).
thf(11582,plain,
~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[11433]) ).
thf(148,plain,
! [B: $i,A: $i] :
( ( ( A @ singleton )
!= ( sk2 @ singleton ) )
| ( ( B @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ in ) )
| ( B @ ( A @ ( B @ sk3 ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[31,15]) ).
thf(149,plain,
! [A: $i] :
( ( ( A @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ ( sk2 @ ( A @ sk4 ) @ in ) )
| ( A @ ( sk2 @ ( A @ sk3 ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[148:[bind(A,$thf( sk2 ))]]) ).
thf(165,plain,
! [A: $i] :
( ( ( A @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ ( sk2 @ ( A @ sk4 ) @ in ) )
| ( A @ ( sk2 @ ( A @ sk3 ) @ in ) ) ),
inference(simp,[status(thm)],[149]) ).
thf(360,plain,
! [B: $i,A: $i] :
( ( B != sk2 )
| ( ( A @ ( sk1 @ ordered_pair ) @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(361,plain,
! [A: $i] :
( ( ( A @ ( sk1 @ ordered_pair ) @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( A @ singleton @ ( sk2 @ in ) ) ),
inference(pattern_uni,[status(thm)],[360:[bind(A,$thf( A )),bind(B,$thf( sk2 ))]]) ).
thf(364,plain,
! [B: $i,A: $i] :
( ( A != sk2 )
| ( ( B @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(365,plain,
! [A: $i] :
( ( ( A @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( sk2 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[364:[bind(A,$thf( sk2 ))]]) ).
thf(522,plain,
! [A: $i] :
( ( ( A @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( sk2 @ singleton @ ( A @ in ) ) ),
inference(simp,[status(thm)],[365]) ).
thf(841,plain,
! [B: $i,A: $i] :
( ( B != sk2 )
| ~ ( A @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,519]) ).
thf(842,plain,
! [A: $i] :
( ~ ( A @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) )
| ~ ( A @ singleton @ ( sk2 @ in ) ) ),
inference(pattern_uni,[status(thm)],[841:[bind(A,$thf( A )),bind(B,$thf( sk2 ))]]) ).
thf(316,plain,
! [B: $i,A: $i] :
( ( B != sk13 )
| ~ ( A @ empty )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,92]) ).
thf(317,plain,
! [A: $i] :
( ~ ( A @ empty )
| ~ ( A @ singleton @ ( sk13 @ in ) ) ),
inference(pattern_uni,[status(thm)],[316:[bind(A,$thf( A )),bind(B,$thf( sk13 ))]]) ).
thf(45,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( B @ ( A @ cartesian_product2 ) ) )
| ( B @ ( A @ ( B @ ( C @ sk11 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk7 ) ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(61,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( B @ ( C @ sk11 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk7 ) ) )
| ( C
= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(lifteq,[status(thm)],[45]) ).
thf(62,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( B @ ( C @ sk11 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk7 ) ) )
| ( C
= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(simp,[status(thm)],[61]) ).
thf(4875,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ cartesian_product2 ) )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ( C
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ( B @ ( A @ ( B @ ( C @ sk11 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk7 ) ) ) ),
inference(paramod_ordered,[status(thm)],[62,15]) ).
thf(4876,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ( sk2 @ singleton @ ( sk1 @ singleton @ ( sk2 @ singleton @ ( A @ sk11 ) ) @ in ) )
| ( A @ ( sk2 @ singleton @ ( sk1 @ singleton @ sk7 ) ) ) ),
inference(pattern_uni,[status(thm)],[4875:[bind(A,$thf( sk1 @ singleton )),bind(B,$thf( sk2 @ singleton )),bind(C,$thf( C ))]]) ).
thf(4977,plain,
( ( sk2 @ singleton @ ( sk1 @ singleton @ ( sk2 @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ sk11 ) ) @ in ) )
| ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ sk7 ) ) ) ),
inference(simp,[status(thm)],[4876]) ).
thf(5500,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ singleton @ ( sk1 @ singleton @ ( sk2 @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ sk11 ) ) @ in ) )
!= ( A @ singleton @ ( B @ in ) ) )
| ~ $true
| ( B = A )
| ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ sk7 ) ) ) ),
inference(paramod_ordered,[status(thm)],[4977,33]) ).
thf(5501,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ singleton @ ( sk1 @ singleton @ ( sk2 @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ sk11 ) ) @ in ) )
!= ( A @ singleton @ ( B @ in ) ) )
| ( B = A )
| ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ sk7 ) ) ) ),
inference(simp,[status(thm)],[5500]) ).
thf(5502,plain,
( ( ( sk1 @ singleton @ ( sk2 @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ sk11 ) ) )
= sk2 )
| ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ sk7 ) ) ) ),
inference(pattern_uni,[status(thm)],[5501:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 @ singleton @ ( sk2 @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ sk11 ) ) ))]]) ).
thf(1467,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk13 @ singleton @ singleton @ singleton @ singleton ) )
| ( B
!= ( sk12 @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,1350]) ).
thf(1468,plain,
! [A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[1467:[bind(A,$thf( sk13 @ singleton @ singleton @ singleton @ singleton )),bind(B,$thf( B ))]]) ).
thf(1498,plain,
~ ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[1468]) ).
thf(15782,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,11581]) ).
thf(15783,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton @ in ) ) ),
inference(simp,[status(thm)],[15782]) ).
thf(15870,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton ) ) ),
inference(simp,[status(thm)],[15783]) ).
thf(15912,plain,
( ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ singleton @ singleton ) ),
inference(simp,[status(thm)],[15870]) ).
thf(2644,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ( B
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,1817]) ).
thf(2645,plain,
! [A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[2644:[bind(A,$thf( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton )),bind(B,$thf( B ))]]) ).
thf(2681,plain,
~ ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[2645]) ).
thf(25,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ singleton ) )
| ~ ( B @ ( A @ ( B @ sk4 ) @ in ) )
| ( ( A @ ( B @ sk3 ) )
!= A ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(40,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk4 ) @ in ) )
| ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk3 ) )
!= A ) ),
inference(lifteq,[status(thm)],[25]) ).
thf(41,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ sk4 ) @ in ) )
| ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk3 ) )
!= A ) ),
inference(simp,[status(thm)],[40]) ).
thf(8086,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ cartesian_product2 ) @ singleton @ singleton ) )
| ( A
!= ( sk12 @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,7935]) ).
thf(8087,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( C @ ( B @ cartesian_product2 ) @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[8086:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ cartesian_product2 ) @ singleton @ singleton )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(8127,plain,
! [B: $i,A: $i] :
~ ( sk12 @ singleton @ singleton @ singleton @ singleton @ ( B @ ( A @ cartesian_product2 ) @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[8087]) ).
thf(227,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ singleton @ ( B @ ( A @ unordered_pair ) @ unordered_pair ) )
!= ( D @ ( C @ unordered_pair ) ) )
| ( ( B @ ( A @ ordered_pair ) )
= ( C @ ( D @ unordered_pair ) ) ) ),
inference(paramod_ordered,[status(thm)],[77,20]) ).
thf(228,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ unordered_pair ) @ ( B @ singleton @ unordered_pair ) )
= ( A @ ( B @ ordered_pair ) ) ),
inference(pattern_uni,[status(thm)],[227:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( F @ ( G @ unordered_pair ) )),bind(D,$thf( G @ singleton ))]]) ).
thf(244,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ unordered_pair ) @ ( B @ singleton @ unordered_pair ) )
= ( A @ ( B @ ordered_pair ) ) ),
inference(simp,[status(thm)],[228]) ).
thf(768,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unordered_pair ) )
!= ( C @ singleton @ ( C @ ( D @ unordered_pair ) @ unordered_pair ) ) )
| ( ( A @ ( B @ unordered_pair ) )
= ( D @ ( C @ ordered_pair ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,234]) ).
thf(769,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( B @ singleton @ unordered_pair ) )
= ( A @ ( B @ ordered_pair ) ) ),
inference(pattern_uni,[status(thm)],[768:[bind(A,$thf( G @ ( E @ unordered_pair ) )),bind(B,$thf( G @ singleton )),bind(C,$thf( G )),bind(D,$thf( E ))]]) ).
thf(794,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unordered_pair ) @ ( B @ singleton @ unordered_pair ) )
= ( A @ ( B @ ordered_pair ) ) ),
inference(simp,[status(thm)],[769]) ).
thf(96,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( B @ ( A @ ( B @ sk15 ) @ in ) )
| ( A @ ( A @ ( B @ sk14 ) @ in ) ) ),
inference(cnfConj,[status(thm)],[95]) ).
thf(100,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ sk15 ) @ in ) )
| ( A @ ( A @ ( B @ sk14 ) @ in ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[96]) ).
thf(19201,plain,
! [B: $i,A: $i] :
( ( A != sk13 )
| ( B != sk12 )
| ( B @ ( A @ ( B @ sk15 ) @ in ) )
| ( A @ ( A @ ( B @ sk14 ) @ in ) ) ),
inference(paramod_ordered,[status(thm)],[100,106]) ).
thf(19202,plain,
! [A: $i] :
( ( A != sk12 )
| ( A @ ( sk13 @ ( A @ sk15 ) @ in ) )
| ( sk13 @ ( sk13 @ ( A @ sk14 ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[19201:[bind(A,$thf( sk13 ))]]) ).
thf(22980,plain,
( ( sk12 @ ( sk13 @ ( sk12 @ sk15 ) @ in ) )
| ( sk13 @ ( sk13 @ ( sk12 @ sk14 ) @ in ) ) ),
inference(simp,[status(thm)],[19202]) ).
thf(1577,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton ) )
| ( A
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,890]) ).
thf(1578,plain,
! [A: $i] :
( ( A
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton ) )
| ~ ( A @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[1577:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton ))]]) ).
thf(1648,plain,
~ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[1578]) ).
thf(48,plain,
! [C: $i,B: $i,A: $i] :
( ( C
= ( B @ ( A @ cartesian_product2 ) ) )
| ~ ( C @ ( A @ ( B @ ( C @ sk9 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk7 ) ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(63,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ ( B @ ( C @ sk9 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk7 ) ) )
| ( C
= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(lifteq,[status(thm)],[48]) ).
thf(64,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ ( B @ ( C @ sk9 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk7 ) ) )
| ( C
= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(simp,[status(thm)],[63]) ).
thf(600,plain,
! [B: $i,A: $i] :
( ( B != sk12 )
| ~ ( A @ singleton @ ( sk13 @ in ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,556]) ).
thf(601,plain,
! [A: $i] :
( ~ ( A @ singleton @ ( sk13 @ in ) )
| ~ ( A @ singleton @ ( sk12 @ in ) ) ),
inference(pattern_uni,[status(thm)],[600:[bind(A,$thf( A )),bind(B,$thf( sk12 ))]]) ).
thf(478,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A
!= ( D @ ( C @ ordered_pair ) ) )
| ( B != sk12 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,109]) ).
thf(479,plain,
! [C: $i,B: $i,A: $i] :
( ( A != sk12 )
| ~ ( C @ ( B @ ordered_pair ) @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[478:[bind(A,$thf( F @ ( E @ ordered_pair ) )),bind(B,$thf( B )),bind(C,$thf( E )),bind(D,$thf( F ))]]) ).
thf(579,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ ordered_pair ) @ singleton @ ( sk12 @ in ) ),
inference(simp,[status(thm)],[479]) ).
thf(11684,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ ( C @ ( B @ cartesian_product2 ) @ singleton @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,8127]) ).
thf(11685,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ ( C @ ( B @ cartesian_product2 ) @ singleton @ singleton @ in ) ) ),
inference(simp,[status(thm)],[11684]) ).
thf(11738,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton ) )
| ( A
!= ( C @ ( B @ cartesian_product2 ) @ singleton @ singleton ) ) ),
inference(simp,[status(thm)],[11685]) ).
thf(11775,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ cartesian_product2 ) @ singleton @ singleton @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton ) ),
inference(simp,[status(thm)],[11738]) ).
thf(12772,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A
!= ( D @ ( C @ cartesian_product2 ) @ singleton @ singleton @ singleton ) )
| ( B
!= ( sk12 @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,11775]) ).
thf(12773,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( C @ ( B @ cartesian_product2 ) @ singleton @ singleton @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[12772:[bind(A,$thf( I @ ( H @ cartesian_product2 ) @ singleton @ singleton @ singleton )),bind(B,$thf( B )),bind(C,$thf( H )),bind(D,$thf( I ))]]) ).
thf(12830,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ cartesian_product2 ) @ singleton @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[12773]) ).
thf(7097,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ordered_pair ) @ singleton @ singleton ) )
| ( A
!= ( sk12 @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,6960]) ).
thf(7098,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( C @ ( B @ ordered_pair ) @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[7097:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ordered_pair ) @ singleton @ singleton )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(7145,plain,
! [B: $i,A: $i] :
~ ( sk12 @ singleton @ singleton @ singleton @ ( B @ ( A @ ordered_pair ) @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[7098]) ).
thf(2103,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ cartesian_product2 ) )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ( C
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ( A @ ( A @ ( B @ ( C @ sk10 ) ) @ in ) )
| ( C @ ( B @ ( A @ sk7 ) ) ) ),
inference(paramod_ordered,[status(thm)],[56,15]) ).
thf(2104,plain,
! [A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ( sk1 @ singleton @ ( sk1 @ singleton @ ( sk2 @ singleton @ ( A @ sk10 ) ) @ in ) )
| ( A @ ( sk2 @ singleton @ ( sk1 @ singleton @ sk7 ) ) ) ),
inference(pattern_uni,[status(thm)],[2103:[bind(A,$thf( sk1 @ singleton )),bind(B,$thf( sk2 @ singleton )),bind(C,$thf( C ))]]) ).
thf(2425,plain,
( ( sk1 @ singleton @ ( sk1 @ singleton @ ( sk2 @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ sk10 ) ) @ in ) )
| ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ sk7 ) ) ) ),
inference(simp,[status(thm)],[2104]) ).
thf(3810,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( D @ cartesian_product2 ) ) )
| ( B
!= ( sk12 @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,3796]) ).
thf(3811,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton ) )
| ~ ( C @ ( B @ cartesian_product2 ) @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[3810:[bind(A,$thf( F @ ( E @ cartesian_product2 ) )),bind(B,$thf( B )),bind(C,$thf( F )),bind(D,$thf( E ))]]) ).
thf(3815,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ cartesian_product2 ) @ singleton @ ( sk12 @ singleton @ in ) ),
inference(simp,[status(thm)],[3811]) ).
thf(12958,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,7226]) ).
thf(12959,plain,
! [A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ in ) ) ),
inference(simp,[status(thm)],[12958]) ).
thf(13037,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton ) ) ),
inference(simp,[status(thm)],[12959]) ).
thf(13064,plain,
( ( sk13 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton @ singleton ) ),
inference(simp,[status(thm)],[13037]) ).
thf(24,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk4 ) )
= A )
| ( ( A @ ( B @ sk3 ) )
!= A ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(38,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk4 ) )
= A )
| ( ( A @ ( B @ sk3 ) )
!= A ) ),
inference(lifteq,[status(thm)],[24]) ).
thf(39,plain,
! [B: $i,A: $i] :
( ( B
= ( A @ singleton ) )
| ( ( A @ ( B @ sk4 ) )
= A )
| ( ( A @ ( B @ sk3 ) )
!= A ) ),
inference(simp,[status(thm)],[38]) ).
thf(598,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk12 @ singleton ) )
| ~ ( A @ ( sk13 @ in ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,556]) ).
thf(599,plain,
! [A: $i] :
( ~ ( A @ ( sk13 @ in ) )
| ~ ( A @ singleton @ ( sk12 @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[598:[bind(A,$thf( A )),bind(B,$thf( sk12 @ singleton ))]]) ).
thf(344,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk1 @ singleton ) )
| ( ( sk2 @ singleton @ ( A @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(345,plain,
! [A: $i] :
( ( ( sk2 @ singleton @ ( A @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( sk1 @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[344:[bind(A,$thf( A )),bind(B,$thf( sk1 @ singleton ))]]) ).
thf(847,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ~ ( sk2 @ ( A @ ordered_pair ) @ singleton @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,519]) ).
thf(848,plain,
! [A: $i] :
( ~ ( sk2 @ ( A @ ordered_pair ) @ singleton @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) )
| ~ ( A @ singleton @ ( sk1 @ in ) ) ),
inference(pattern_uni,[status(thm)],[847:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(354,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ( A
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(355,plain,
! [A: $i] :
( ( A
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( A @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[354:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ( sk1 @ ordered_pair ) @ singleton ))]]) ).
thf(520,plain,
~ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ in ) ),
inference(simp,[status(thm)],[355]) ).
thf(50,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( B @ ( C @ ( D @ sk6 ) ) ) @ in ) )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(65,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( B @ ( C @ ( D @ sk6 ) ) ) @ in ) )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(lifteq,[status(thm)],[50]) ).
thf(66,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( B @ ( B @ ( A @ cartesian_product2 ) @ ( C @ sk6 ) ) ) @ in ) )
| ~ ( B @ ( A @ cartesian_product2 ) @ ( C @ in ) ) ),
inference(simp,[status(thm)],[65]) ).
thf(362,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk1 @ singleton ) )
| ( ( sk2 @ singleton @ ( B @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(363,plain,
! [A: $i] :
( ( ( sk2 @ singleton @ ( A @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( sk1 @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[362:[bind(A,$thf( sk1 @ singleton )),bind(B,$thf( B ))]]) ).
thf(521,plain,
! [A: $i] :
( ( ( sk2 @ singleton @ ( A @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( sk1 @ singleton @ singleton @ ( A @ in ) ) ),
inference(simp,[status(thm)],[363]) ).
thf(652,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk13 @ singleton ) )
| ( B
!= ( sk12 @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,611]) ).
thf(653,plain,
! [A: $i] :
( ( A
!= ( sk12 @ singleton ) )
| ~ ( sk13 @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[652:[bind(A,$thf( sk13 @ singleton )),bind(B,$thf( B ))]]) ).
thf(658,plain,
~ ( sk13 @ singleton @ singleton @ ( sk12 @ singleton @ in ) ),
inference(simp,[status(thm)],[653]) ).
thf(370,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk2 @ singleton ) )
| ( ( B @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(371,plain,
! [A: $i] :
( ( ( A @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( sk2 @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[370:[bind(A,$thf( sk2 @ singleton )),bind(B,$thf( B ))]]) ).
thf(525,plain,
! [A: $i] :
( ( ( A @ ( sk1 @ singleton @ cartesian_product2 ) )
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( sk2 @ singleton @ singleton @ ( A @ in ) ) ),
inference(simp,[status(thm)],[371]) ).
thf(434,plain,
! [B: $i,A: $i] :
( ( A != sk13 )
| ( B != sk12 )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,106]) ).
thf(435,plain,
! [A: $i] :
( ( A != sk12 )
| ~ ( sk13 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[434:[bind(A,$thf( sk13 ))]]) ).
thf(557,plain,
~ ( sk13 @ singleton @ ( sk12 @ in ) ),
inference(simp,[status(thm)],[435]) ).
thf(1176,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk13 @ singleton @ singleton @ singleton ) )
| ( B
!= ( sk12 @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,1087]) ).
thf(1177,plain,
! [A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton @ singleton ) )
| ~ ( sk13 @ singleton @ singleton @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[1176:[bind(A,$thf( sk13 @ singleton @ singleton @ singleton )),bind(B,$thf( B ))]]) ).
thf(1188,plain,
~ ( sk13 @ singleton @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[1177]) ).
thf(12764,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ cartesian_product2 ) @ singleton @ singleton @ singleton ) )
| ( A
!= ( sk12 @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,11775]) ).
thf(12765,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( C @ ( B @ cartesian_product2 ) @ singleton @ singleton @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[12764:[bind(A,$thf( A )),bind(B,$thf( I @ ( H @ cartesian_product2 ) @ singleton @ singleton @ singleton )),bind(C,$thf( H )),bind(D,$thf( I ))]]) ).
thf(12826,plain,
! [B: $i,A: $i] :
~ ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ ( B @ ( A @ cartesian_product2 ) @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[12765]) ).
thf(839,plain,
! [B: $i,A: $i] :
( ( B != sk2 )
| ~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ ( A @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,519]) ).
thf(840,plain,
! [A: $i] :
( ~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ ( A @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) )
| ~ ( A @ singleton @ ( sk2 @ in ) ) ),
inference(pattern_uni,[status(thm)],[839:[bind(A,$thf( A )),bind(B,$thf( sk2 ))]]) ).
thf(358,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ( ( sk2 @ ( A @ ordered_pair ) @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(359,plain,
! [A: $i] :
( ( ( sk2 @ ( A @ ordered_pair ) @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( A @ singleton @ ( sk1 @ in ) ) ),
inference(pattern_uni,[status(thm)],[358:[bind(A,$thf( A )),bind(B,$thf( sk1 ))]]) ).
thf(602,plain,
! [B: $i,A: $i] :
( ( A != sk13 )
| ~ ( sk12 @ singleton @ ( B @ in ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,556]) ).
thf(603,plain,
! [A: $i] :
( ~ ( sk12 @ singleton @ ( A @ in ) )
| ~ ( sk13 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[602:[bind(A,$thf( sk13 ))]]) ).
thf(613,plain,
! [A: $i] :
( ~ ( sk12 @ singleton @ ( A @ in ) )
| ~ ( sk13 @ singleton @ ( A @ in ) ) ),
inference(simp,[status(thm)],[603]) ).
thf(3337,plain,
! [B: $i,A: $i] :
( ( A
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton ) )
| ( B
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,2028]) ).
thf(3338,plain,
! [A: $i] :
( ( A
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton ) )
| ~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[3337:[bind(A,$thf( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton )),bind(B,$thf( B ))]]) ).
thf(3388,plain,
~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ singleton @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[3338]) ).
thf(54,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C
= ( B @ ( A @ cartesian_product2 ) ) )
| ~ ( C @ ( B @ ( A @ sk7 ) ) )
| ( ( A @ ( B @ ( C @ sk8 ) ) )
!= ( E @ ( D @ ordered_pair ) ) )
| ~ ( B @ ( E @ in ) )
| ~ ( A @ ( D @ in ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(71,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ sk7 ) ) )
| ~ ( B @ ( E @ in ) )
| ~ ( A @ ( D @ in ) )
| ( C
= ( B @ ( A @ cartesian_product2 ) ) )
| ( ( A @ ( B @ ( C @ sk8 ) ) )
!= ( E @ ( D @ ordered_pair ) ) ) ),
inference(lifteq,[status(thm)],[54]) ).
thf(72,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ ( A @ sk7 ) ) )
| ~ ( B @ ( E @ in ) )
| ~ ( A @ ( D @ in ) )
| ( C
= ( B @ ( A @ cartesian_product2 ) ) )
| ( ( A @ ( B @ ( C @ sk8 ) ) )
!= ( E @ ( D @ ordered_pair ) ) ) ),
inference(simp,[status(thm)],[71]) ).
thf(86,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ cartesian_product2 ) @ ( B @ ( A @ ordered_pair ) @ in ) )
| ~ ( D @ ( B @ in ) )
| ~ ( C @ ( A @ in ) ) ),
inference(cnfConj,[status(thm)],[83]) ).
thf(87,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ cartesian_product2 ) @ ( B @ ( A @ ordered_pair ) @ in ) )
| ~ ( D @ ( B @ in ) )
| ~ ( C @ ( A @ in ) ) ),
inference(simp,[status(thm)],[86]) ).
thf(17679,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ ( sk13 @ in ) ) )
| ( ( sk12 @ singleton @ singleton )
!= sk13 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,16018]) ).
thf(17680,plain,
! [A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ ( sk13 @ in ) ) )
| ( ( sk12 @ singleton @ singleton )
!= sk13 ) ),
inference(simp,[status(thm)],[17679]) ).
thf(17723,plain,
! [A: $i] :
( ( ( A @ singleton )
!= ( sk12 @ singleton @ singleton ) )
| ( A != sk13 )
| ( ( sk12 @ singleton @ singleton )
!= sk13 ) ),
inference(simp,[status(thm)],[17680]) ).
thf(17740,plain,
( ( ( sk12 @ singleton @ singleton )
!= ( sk13 @ singleton ) )
| ( ( sk12 @ singleton @ singleton )
!= sk13 ) ),
inference(simp,[status(thm)],[17723]) ).
thf(17743,plain,
( ( ( sk12 @ singleton )
!= sk13 )
| ( ( sk12 @ singleton @ singleton )
!= sk13 ) ),
inference(simp,[status(thm)],[17740]) ).
thf(843,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk2 @ ( sk1 @ ordered_pair ) @ singleton ) )
| ~ ( A @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,519]) ).
thf(844,plain,
! [A: $i] :
( ~ ( A @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) )
| ~ ( A @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ in ) ) ),
inference(pattern_uni,[status(thm)],[843:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ( sk1 @ ordered_pair ) @ singleton ))]]) ).
thf(46,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ in ) )
| ( D
!= ( F @ ( E @ ordered_pair ) ) )
| ~ ( B @ ( F @ in ) )
| ~ ( A @ ( E @ in ) )
| ( C
!= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(57,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( D @ in ) )
| ~ ( B @ ( F @ in ) )
| ~ ( A @ ( E @ in ) )
| ( D
!= ( F @ ( E @ ordered_pair ) ) )
| ( C
!= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(lifteq,[status(thm)],[46]) ).
thf(58,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ cartesian_product2 ) @ ( D @ ( C @ ordered_pair ) @ in ) )
| ~ ( B @ ( D @ in ) )
| ~ ( A @ ( C @ in ) ) ),
inference(simp,[status(thm)],[57]) ).
thf(23534,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ ( C @ ( B @ cartesian_product2 ) @ singleton @ singleton @ singleton @ in ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[35,12826]) ).
thf(23535,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ singleton @ ( A @ in ) )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton @ ( C @ ( B @ cartesian_product2 ) @ singleton @ singleton @ singleton @ in ) ) ),
inference(simp,[status(thm)],[23534]) ).
thf(23648,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton ) )
| ( A
!= ( C @ ( B @ cartesian_product2 ) @ singleton @ singleton @ singleton ) ) ),
inference(simp,[status(thm)],[23535]) ).
thf(23718,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ cartesian_product2 ) @ singleton @ singleton @ singleton @ singleton )
!= ( sk12 @ singleton @ singleton @ singleton @ singleton @ singleton ) ),
inference(simp,[status(thm)],[23648]) ).
thf(318,plain,
! [B: $i,A: $i] :
( ( A != sk13 )
| ~ ( B @ empty )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,92]) ).
thf(319,plain,
! [A: $i] :
( ~ ( A @ empty )
| ~ ( sk13 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[318:[bind(A,$thf( sk13 ))]]) ).
thf(506,plain,
! [A: $i] :
( ~ ( A @ empty )
| ~ ( sk13 @ singleton @ ( A @ in ) ) ),
inference(simp,[status(thm)],[319]) ).
thf(2729,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ singleton @ ( sk1 @ singleton @ ( sk2 @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ sk10 ) ) @ in ) )
!= ( A @ singleton @ ( B @ in ) ) )
| ~ $true
| ( B = A )
| ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ sk7 ) ) ) ),
inference(paramod_ordered,[status(thm)],[2425,33]) ).
thf(2730,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ singleton @ ( sk1 @ singleton @ ( sk2 @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ sk10 ) ) @ in ) )
!= ( A @ singleton @ ( B @ in ) ) )
| ( B = A )
| ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ sk7 ) ) ) ),
inference(simp,[status(thm)],[2729]) ).
thf(2731,plain,
( ( ( sk1 @ singleton @ ( sk2 @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ sk10 ) ) )
= sk1 )
| ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ sk7 ) ) ) ),
inference(pattern_uni,[status(thm)],[2730:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ singleton @ ( sk2 @ singleton @ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ sk10 ) ) ))]]) ).
thf(376,plain,
! [B: $i,A: $i] :
( ( A != sk1 )
| ( ( sk2 @ ( B @ ordered_pair ) @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,15]) ).
thf(377,plain,
! [A: $i] :
( ( ( sk2 @ ( A @ ordered_pair ) @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( sk1 @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[376:[bind(A,$thf( sk1 ))]]) ).
thf(528,plain,
! [A: $i] :
( ( ( sk2 @ ( A @ ordered_pair ) @ singleton )
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( sk1 @ singleton @ ( A @ in ) ) ),
inference(simp,[status(thm)],[377]) ).
thf(5060,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ cartesian_product2 ) )
!= ( sk12 @ singleton ) ),
inference(simp,[status(thm)],[3875]) ).
thf(849,plain,
! [B: $i,A: $i] :
( ( B
!= ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ) )
| ~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ ( A @ in ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,519]) ).
thf(850,plain,
! [A: $i] :
( ~ ( sk2 @ ( sk1 @ ordered_pair ) @ singleton @ singleton @ ( A @ in ) )
| ~ ( A @ singleton @ ( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) @ in ) ) ),
inference(pattern_uni,[status(thm)],[849:[bind(A,$thf( A )),bind(B,$thf( sk2 @ singleton @ ( sk1 @ singleton @ cartesian_product2 ) ))]]) ).
thf(51,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( A @ ( B @ ( C @ ( D @ sk5 ) ) ) @ in ) )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(67,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( A @ ( B @ ( C @ ( D @ sk5 ) ) ) @ in ) )
| ~ ( C @ ( D @ in ) )
| ( C
!= ( B @ ( A @ cartesian_product2 ) ) ) ),
inference(lifteq,[status(thm)],[51]) ).
thf(68,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( A @ ( B @ ( B @ ( A @ cartesian_product2 ) @ ( C @ sk5 ) ) ) @ in ) )
| ~ ( B @ ( A @ cartesian_product2 ) @ ( C @ in ) ) ),
inference(simp,[status(thm)],[67]) ).
thf(8092,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A
!= ( D @ ( C @ cartesian_product2 ) @ singleton @ singleton ) )
| ( B
!= ( sk12 @ singleton @ singleton @ singleton ) )
| ~ ( A @ singleton @ ( B @ in ) ) ),
inference(paramod_ordered,[status(thm)],[33,7935]) ).
thf(8093,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk12 @ singleton @ singleton @ singleton ) )
| ~ ( C @ ( B @ cartesian_product2 ) @ singleton @ singleton @ singleton @ ( A @ in ) ) ),
inference(pattern_uni,[status(thm)],[8092:[bind(A,$thf( H @ ( G @ cartesian_product2 ) @ singleton @ singleton )),bind(B,$thf( B )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(8130,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ cartesian_product2 ) @ singleton @ singleton @ singleton @ ( sk12 @ singleton @ singleton @ singleton @ in ) ),
inference(simp,[status(thm)],[8093]) ).
thf(78099,plain,
$false,
inference(e,[status(thm)],[836,1718,9653,101,347,846,11581,234,88,523,7935,120,614,597,56,14354,174,42,9657,37,3263,504,838,357,20,93,5091,78,1087,189,7236,7226,164,16018,106,84,353,5259,2530,89,527,74,60,529,85,1021,1255,349,70,21,33,3261,11582,165,3814,92,361,522,842,1350,317,5502,1498,3386,519,578,109,77,15912,1016,2681,13,41,8127,244,657,1187,794,22980,1648,64,2028,17,601,3758,2674,579,118,3796,611,12830,7145,2425,3815,13064,81,39,599,345,8340,890,9407,848,520,66,521,11775,5089,80,35,658,525,557,18,1637,1188,16,12826,840,31,7127,359,703,613,6960,3388,72,556,87,1817,17743,844,75,17740,58,23718,1495,506,3875,532,2731,528,5060,15,62,850,68,90,8130,4977,100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SET894+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% 0.00/0.12 % 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.27/0.50 % Computer : n004.cluster.edu
% 0.27/0.50 % Model : x86_64 x86_64
% 0.27/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.27/0.50 % Memory : 8046.5625MB
% 0.27/0.50 % OS : Linux 6.8.0-71-generic
% 0.27/0.50 % CPULimit : 300
% 0.27/0.51 % WCLimit : 300
% 0.27/0.51 % DateTime : Sat Sep 26 08:24:37 UTC 2026
% 0.27/0.51 % CPUTime :
% 0.27/0.51 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
% 1.40/1.37 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.92/1.66 % [INFO] Parsing done (281ms).
% 1.92/1.68 % [INFO] Running in sequential loop mode.
% 3.13/2.31 % [INFO] eprover registered as external prover.
% 3.13/2.32 % [INFO] Scanning for conjecture ...
% 3.34/2.47 % [INFO] Found a conjecture (or negated_conjecture) and 10 axioms. Running axiom selection ...
% 3.50/2.52 % [INFO] Axiom selection finished. Selected 10 axioms (removed 0 axioms).
% 3.50/2.56 % [INFO] Problem is first-order (TPTP FOF).
% 3.50/2.57 % [INFO] Type checking passed.
% 3.50/2.58 % [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 ...
% 166.05/42.82 % External prover 'e' found a proof!
% 166.05/42.82 % [INFO] Killing All external provers ...
% 166.05/42.83 % Time passed: 42099ms (effective reasoning time: 41134ms)
% 166.05/42.83 % 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)>
% 166.05/42.83 % Axioms used in derivation (10): d5_tarski, t2_tarski, l55_zfmisc_1, rc1_xboole_0, rc2_xboole_0, antisymmetry_r2_hidden, fc1_zfmisc_1, d1_tarski, d2_zfmisc_1, commutativity_k2_tarski
% 166.05/42.83 % No. of inferences in proof: 438
% 166.05/42.83 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 42099 ms resp. 41134 ms w/o parsing
% 161.55/43.05 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 161.55/43.06 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------