%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEU795^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n003.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 : Wed Sep 30 08:29:20 AM UTC 2026
% Result : Theorem 87.83s 22.63s
% Output : Refutation 88.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 21
% Syntax : Number of formulae : 197 ( 51 unt; 0 typ; 20 def)
% Number of atoms : 1333 ( 691 equ; 80 cnn)
% Maximal formula atoms : 8 ( 6 avg)
% Number of connectives : 3013 ( 259 ~; 232 |; 221 &;2281 @)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 5 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 47 ( 47 >; 0 *; 0 +; 0 <<)
% Number of symbols : 29 ( 25 usr; 19 con; 0-3 aty)
% Number of variables : 640 ( 136 ^; 290 !; 199 ?; 640 :)
% ( 0 !>; 0 ?*; 0 @-; 15 @+)
% Comments :
%------------------------------------------------------------------------------
thf(in_decl,type,
in: $i > $i > $o ).
thf(exu_decl,type,
exu: ( $i > $o ) > $o ).
thf(descr_decl,type,
descr: ( $i > $o ) > $i ).
thf(descrp_decl,type,
descrp: $o ).
thf(in__Cong_decl,type,
in__Cong: $o ).
thf(image1Ex1_decl,type,
image1Ex1: $o ).
thf(image1_decl,type,
image1: $i > ( $i > $i ) > $i ).
thf(sk1_decl,type,
sk1: $i > ( $i > $o ) > $i ).
thf(sk2_decl,type,
sk2: ( $i > $i ) > $i > $i ).
thf(sk3_decl,type,
sk3: $i > ( $i > $i ) > $i > $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk5_decl,type,
sk5: $i > $i ).
thf(sk6_decl,type,
sk6: $i ).
thf(sk7_decl,type,
sk7: $i ).
thf(sk8_decl,type,
sk8: $i > ( $i > $i ) > $i > $i ).
thf(sk27_decl,type,
sk27: $i ).
thf(sk28_decl,type,
sk28: $i ).
thf(sk100_decl,type,
sk100: $i ).
thf(sk105_decl,type,
sk105: $i ).
thf(sk119_decl,type,
sk119: $i ).
thf(sk121_decl,type,
sk121: $i ).
thf(sk137_decl,type,
sk137: $i ).
thf(sk141_decl,type,
sk141: $i ).
thf(sk149_decl,type,
sk149: $i ).
thf(sk167_decl,type,
sk167: $i ).
thf(exu_def,definition,
( exu
= ( ^ [A: $i > $o] :
? [B: $i] :
( ( A @ B )
& ! [C: $i] :
( ( A @ C )
=> ( B = C ) ) ) ) ) ).
thf(descrp_def,definition,
( descrp
= ( ! [A: $i > $o] :
( ( exu @ A )
=> ( A @ ( descr @ A ) ) ) ) ) ).
thf(in__Cong_def,definition,
( in__Cong
= ( ! [A: $i,B: $i] :
( ( A = B )
=> ! [C: $i,D: $i] :
( ( C = D )
=> ( ( in @ C @ A )
= ( in @ D @ B ) ) ) ) ) ) ).
thf(image1Ex1_def,definition,
( image1Ex1
= ( ! [A: $i,B: $i > $i] :
( exu
@ ^ [C: $i] :
! [D: $i] :
( ( in @ D @ C )
= ( ? [E: $i] :
( ( in @ E @ A )
& ( D
= ( B @ E ) ) ) ) ) ) ) ) ).
thf(image1_def,definition,
( image1
= ( ^ [A: $i,B: $i > $i] :
( descr
@ ^ [C: $i] :
! [D: $i] :
( ( in @ D @ C )
= ( ? [E: $i] :
( ( in @ E @ A )
& ( D
= ( B @ E ) ) ) ) ) ) ) ) ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: $i,B: $i > $o] :
@+[C: $i] :
~ ( ( B @ C )
=> ( A = C ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: $i > $i,B: $i] :
@+[C: $i] :
( ! [D: $i] :
( ( in @ D @ C )
= ( ? [E: $i] :
( ( in @ E @ B )
& ( D
= ( A @ E ) ) ) ) )
& ! [D: $i] :
( ! [E: $i] :
( ( in @ E @ D )
= ( ? [F: $i] :
( ( in @ F @ B )
& ( E
= ( A @ F ) ) ) ) )
=> ( C = D ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: $i,B: $i > $i,C: $i] :
@+[D: $i] :
( ( in @ D @ A )
!= ( ? [E: $i] :
( ( in @ E @ C )
& ( D
= ( B @ E ) ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
~ ! [B: $i > $i,C: $i] :
( ( in @ C
@ ( descr
@ ^ [D: $i] :
! [E: $i] :
( ( in @ E @ D )
= ( ? [F: $i] :
( ( in @ F @ A )
& ( E
= ( B @ F ) ) ) ) ) ) )
= ( ? [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: $i > $i] :
~ ! [B: $i] :
( ( in @ B
@ ( descr
@ ^ [C: $i] :
! [D: $i] :
( ( in @ D @ C )
= ( ? [E: $i] :
( ( in @ E @ sk4 )
& ( D
= ( A @ E ) ) ) ) ) ) )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( A @ C ) ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: $i] :
( ( in @ A
@ ( descr
@ ^ [B: $i] :
! [C: $i] :
( ( in @ C @ B )
= ( ? [D: $i] :
( ( in @ D @ sk4 )
& ( C
= ( sk5 @ D ) ) ) ) ) ) )
!= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( A
= ( sk5 @ B ) ) ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( @+[A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: $i,B: $i > $i,C: $i] :
@+[D: $i] :
( ( in @ D @ C )
& ( A
= ( B @ D ) ) ) ) ) ).
thf(sk27_def,definition,
( sk27
= ( @+[A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) ) ) ) ).
thf(sk28_def,definition,
( sk28
= ( @+[A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) ) ) ) ).
thf(sk105_def,definition,
( sk105
= ( @+[A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) ) ) ) ).
thf(sk121_def,definition,
( sk121
= ( @+[A: $i] :
( ( in @ A @ sk100 )
!= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( A
= ( sk5 @ B ) ) ) ) ) ) ) ).
thf(sk137_def,definition,
( sk137
= ( @+[A: $i] :
( ( in @ A @ sk4 )
& ( ( sk3 @ sk100 @ sk5 @ sk4 )
= ( sk5 @ A ) ) ) ) ) ).
thf(sk141_def,definition,
( sk141
= ( @+[A: $i] :
( ( in @ A @ sk119 )
!= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( A
= ( sk5 @ B ) ) ) ) ) ) ) ).
thf(sk167_def,definition,
( sk167
= ( @+[A: $i] :
( ( in @ A @ sk4 )
& ( ( sk3 @ sk119 @ sk5 @ sk4 )
= ( sk5 @ A ) ) ) ) ) ).
thf(1,conjecture,
( descrp
=> ( in__Cong
=> ( image1Ex1
=> ! [A: $i,B: $i > $i,C: $i] :
( ( in @ C @ ( image1 @ A @ B ) )
= ( ? [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',image1Equiv) ).
thf(2,negated_conjecture,
~ ( descrp
=> ( in__Cong
=> ( image1Ex1
=> ! [A: $i,B: $i > $i,C: $i] :
( ( in @ C @ ( image1 @ A @ B ) )
= ( ? [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) ) ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ( ! [A: $i > $o] :
( ? [B: $i] :
( ( A @ B )
& ! [C: $i] :
( ( A @ C )
=> ( B = C ) ) )
=> ( A @ ( descr @ A ) ) )
=> ( ! [A: $i,B: $i] :
( ( A = B )
=> ! [C: $i,D: $i] :
( ( C = D )
=> ( ( in @ C @ A )
= ( in @ D @ B ) ) ) )
=> ( ! [A: $i,B: $i > $i] :
? [C: $i] :
( ! [D: $i] :
( ( in @ D @ C )
= ( ? [E: $i] :
( ( in @ E @ A )
& ( D
= ( B @ E ) ) ) ) )
& ! [D: $i] :
( ! [E: $i] :
( ( in @ E @ D )
= ( ? [F: $i] :
( ( in @ F @ A )
& ( E
= ( B @ F ) ) ) ) )
=> ( C = D ) ) )
=> ! [A: $i,B: $i > $i,C: $i] :
( ( in @ C
@ ( descr
@ ^ [D: $i] :
! [E: $i] :
( ( in @ E @ D )
= ( ? [F: $i] :
( ( in @ F @ A )
& ( E
= ( B @ F ) ) ) ) ) ) )
= ( ? [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
! [J: $i,I: $i,H: $i > $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i > $o] :
( ( ~ ( A @ B )
| ( A @ ( sk1 @ B @ A ) )
| ( A @ ( descr @ A ) ) )
& ( ~ ( A @ B )
| ( B
!= ( sk1 @ B @ A ) )
| ( A @ ( descr @ A ) ) )
& ( ( C != D )
| ( E != F )
| ( ( in @ E @ C )
= ( in @ F @ D ) ) )
& ( ( in @ I @ ( sk2 @ H @ G ) )
= ( ? [K: $i] :
( ( in @ K @ G )
& ( I
= ( H @ K ) ) ) ) )
& ( ( ( in @ ( sk3 @ J @ H @ G ) @ J )
!= ( ? [K: $i] :
( ( in @ K @ G )
& ( ( sk3 @ J @ H @ G )
= ( H @ K ) ) ) ) )
| ( ( sk2 @ H @ G )
= J ) )
& ( ( in @ sk6
@ ( descr
@ ^ [K: $i] :
! [L: $i] :
( ( in @ L @ K )
= ( ? [M: $i] :
( ( in @ M @ sk4 )
& ( L
= ( sk5 @ M ) ) ) ) ) ) )
!= ( ? [K: $i] :
( ( in @ K @ sk4 )
& ( sk6
= ( sk5 @ K ) ) ) ) ) ),
inference(cnf,[status(esa)],[3]) ).
thf(5,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( in @ C @ ( sk2 @ B @ A ) )
= ( ? [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(13,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( in @ C @ ( sk2 @ B @ A ) )
= ( ? [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) ) ) ),
inference(lifteq,[status(thm)],[5]) ).
thf(14,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( in @ C @ ( sk2 @ B @ A ) )
= ( ? [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) ) ) ),
inference(simp,[status(thm)],[13]) ).
thf(10,plain,
! [B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( A @ ( sk1 @ B @ A ) )
| ( A @ ( descr @ A ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(11,plain,
! [A: $i] :
( ( A != A )
| ( A
= ( sk1 @ A @ ( (=) @ $i @ A ) ) )
| ( A
= ( descr @ ( (=) @ $i @ A ) ) ) ),
inference(replace_leibeq,[status(thm)],[10:[bind(A,$thf( (=) @ $i @ B ))]]) ).
thf(21,plain,
! [A: $i] :
( ( A != A )
| ( ( sk1 @ A @ ( (=) @ $i @ A ) )
= A )
| ( A
= ( descr @ ( (=) @ $i @ A ) ) ) ),
inference(lifteq,[status(thm)],[11]) ).
thf(22,plain,
! [A: $i] :
( ( ( sk1 @ A @ ( (=) @ $i @ A ) )
= A )
| ( A
= ( descr @ ( (=) @ $i @ A ) ) ) ),
inference(simp,[status(thm)],[21]) ).
thf(7,plain,
! [B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( B
!= ( sk1 @ B @ A ) )
| ( A @ ( descr @ A ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(12,plain,
! [A: $i] :
( ( A != A )
| ( A
!= ( sk1 @ A @ ( (=) @ $i @ A ) ) )
| ( A
= ( descr @ ( (=) @ $i @ A ) ) ) ),
inference(replace_leibeq,[status(thm)],[7:[bind(A,$thf( (=) @ $i @ B ))]]) ).
thf(18,plain,
! [A: $i] :
( ( A != A )
| ( ( sk1 @ A @ ( (=) @ $i @ A ) )
!= A )
| ( A
= ( descr @ ( (=) @ $i @ A ) ) ) ),
inference(lifteq,[status(thm)],[12]) ).
thf(19,plain,
! [A: $i] :
( ( ( sk1 @ A @ ( (=) @ $i @ A ) )
!= A )
| ( A
= ( descr @ ( (=) @ $i @ A ) ) ) ),
inference(simp,[status(thm)],[18]) ).
thf(2011,plain,
! [B: $i,A: $i] :
( ( A
= ( descr @ ( (=) @ $i @ A ) ) )
| ( A != B )
| ( B
= ( descr @ ( (=) @ $i @ B ) ) )
| ( ( sk1 @ A @ ( (=) @ $i @ A ) )
!= ( sk1 @ B @ ( (=) @ $i @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,19]) ).
thf(2012,plain,
! [A: $i] :
( ( A
= ( descr @ ( (=) @ $i @ A ) ) )
| ( A != A )
| ( A
= ( descr @ ( (=) @ $i @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[2011:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(2018,plain,
! [A: $i] :
( A
= ( descr @ ( (=) @ $i @ A ) ) ),
inference(simp,[status(thm)],[2012]) ).
thf(2060,plain,
! [D: $i,C: $i > $i,B: $i,A: $i] :
( ( ( in @ D @ ( descr @ ( (=) @ $i @ A ) ) )
= ( ? [E: $i] :
( ( in @ E @ B )
& ( D
= ( C @ E ) ) ) ) )
| ( A
!= ( sk2 @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[2018,14]) ).
thf(2061,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( in @ A @ ( descr @ ( (=) @ $i @ ( sk2 @ B @ C ) ) ) )
= ( ? [D: $i] :
( ( in @ D @ C )
& ( A
= ( B @ D ) ) ) ) ),
inference(pattern_uni,[status(thm)],[2060:[bind(A,$thf( sk2 @ E @ F )),bind(B,$thf( F )),bind(C,$thf( E ))]]) ).
thf(2185,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( in @ A @ ( descr @ ( (=) @ $i @ ( sk2 @ B @ C ) ) ) )
= ( ? [D: $i] :
( ( in @ D @ C )
& ( A
= ( B @ D ) ) ) ) ),
inference(simp,[status(thm)],[2061]) ).
thf(9,plain,
( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(17,plain,
( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) ) ) ),
inference(lifteq,[status(thm)],[9]) ).
thf(2248,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( ( in @ A @ ( descr @ ( (=) @ $i @ ( sk2 @ B @ C ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [D: $i] :
! [E: $i] :
( ( in @ E @ D )
= ( ? [F: $i] :
( ( in @ F @ sk4 )
& ( E
= ( sk5 @ F ) ) ) ) ) ) ) )
| ( ( ? [D: $i] :
( ( in @ D @ C )
& ( A
= ( B @ D ) ) ) )
!= ( ? [D: $i] :
( ( in @ D @ sk4 )
& ( sk6
= ( sk5 @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[2185,17]) ).
thf(2249,plain,
( ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[2248:[bind(A,$thf( sk6 )),bind(B,$thf( sk5 )),bind(C,$thf( sk4 ))]]) ).
thf(2740,plain,
! [A: $i] :
( ( ( in @ sk6 @ A )
!= ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) )
| ( ( descr @ ( (=) @ $i @ A ) )
!= ( descr
@ ^ [B: $i] :
! [C: $i] :
( ( in @ C @ B )
= ( ? [D: $i] :
( ( in @ D @ sk4 )
& ( C
= ( sk5 @ D ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[2018,2249]) ).
thf(2787,plain,
! [A: $i] :
( ( sk6 != sk6 )
| ( A
!= ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) )
| ( ( (=) @ $i @ A )
!= ( ^ [B: $i] :
! [C: $i] :
( ( in @ C @ B )
= ( ? [D: $i] :
( ( in @ D @ sk4 )
& ( C
= ( sk5 @ D ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[2740]) ).
thf(2814,plain,
( ( (=) @ $i @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) )
!= ( ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[2787]) ).
thf(3891,plain,
( ( ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) )
= sk119 )
!= ( ! [A: $i] :
( ( in @ A @ sk119 )
= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( A
= ( sk5 @ B ) ) ) ) ) ) ),
inference(func_ext,[status(esa)],[2814]) ).
thf(5070,plain,
! [A: $i] :
( ( ( A = sk119 )
!= ( ! [B: $i] :
( ( in @ B @ sk119 )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( ( descr @ ( (=) @ $i @ A ) )
!= ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[2018,3891]) ).
thf(5071,plain,
( ( ( sk2 @ sk5 @ sk4 )
= sk119 )
!= ( ! [A: $i] :
( ( in @ A @ sk119 )
= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( A
= ( sk5 @ B ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[5070:[bind(A,$thf( sk2 @ sk5 @ sk4 ))]]) ).
thf(5089,plain,
( ( ( sk2 @ sk5 @ sk4 )
!= sk119 )
| ~ ! [A: $i] :
( ( in @ A @ sk119 )
= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( A
= ( sk5 @ B ) ) ) ) ) ),
inference(bool_ext,[status(thm)],[5071]) ).
thf(5115,plain,
( ( ( sk2 @ sk5 @ sk4 )
!= sk119 )
| ~ ! [A: $i] :
( ( in @ A @ sk119 )
= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( A
= ( sk5 @ B ) ) ) ) ) ),
inference(lifteq,[status(thm)],[5089]) ).
thf(5125,plain,
( ( ( sk2 @ sk5 @ sk4 )
!= sk119 )
| ( ( in @ sk141 @ sk119 )
!= ( ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk141
= ( sk5 @ A ) ) ) ) ) ),
inference(cnf,[status(esa)],[5115]) ).
thf(5126,plain,
( ( ( in @ sk141 @ sk119 )
!= ( ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk141
= ( sk5 @ A ) ) ) ) )
| ( ( sk2 @ sk5 @ sk4 )
!= sk119 ) ),
inference(lifteq,[status(thm)],[5125]) ).
thf(6041,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( ( in @ C @ ( sk2 @ B @ A ) )
!= ( in @ sk141 @ sk119 ) )
| ( ( sk2 @ sk5 @ sk4 )
!= sk119 )
| ( ( ? [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) ) )
!= ( ? [D: $i] :
( ( in @ D @ sk4 )
& ( sk141
= ( sk5 @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[14,5126]) ).
thf(6042,plain,
( ( ( in @ sk141 @ ( sk2 @ sk5 @ sk4 ) )
!= ( in @ sk141 @ sk119 ) )
| ( ( sk2 @ sk5 @ sk4 )
!= sk119 ) ),
inference(pattern_uni,[status(thm)],[6041:[bind(A,$thf( sk4 )),bind(B,$thf( sk5 )),bind(C,$thf( sk141 ))]]) ).
thf(6181,plain,
( ( sk141 != sk141 )
| ( ( sk2 @ sk5 @ sk4 )
!= sk119 )
| ( ( sk2 @ sk5 @ sk4 )
!= sk119 ) ),
inference(simp,[status(thm)],[6042]) ).
thf(6263,plain,
( ( sk2 @ sk5 @ sk4 )
!= sk119 ),
inference(simp,[status(thm)],[6181]) ).
thf(36,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( ( in @ C @ ( sk2 @ B @ A ) )
!= ( in @ sk6
@ ( descr
@ ^ [D: $i] :
! [E: $i] :
( ( in @ E @ D )
= ( ? [F: $i] :
( ( in @ F @ sk4 )
& ( E
= ( sk5 @ F ) ) ) ) ) ) ) )
| ( ( ? [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) ) )
!= ( ? [D: $i] :
( ( in @ D @ sk4 )
& ( sk6
= ( sk5 @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[14,17]) ).
thf(37,plain,
( ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[36:[bind(A,$thf( sk4 )),bind(B,$thf( sk5 )),bind(C,$thf( sk6 ))]]) ).
thf(52,plain,
( ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ),
inference(bool_ext,[status(thm)],[37]) ).
thf(521,plain,
! [C: $i,B: $i > $i,A: $i] :
( ? [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) )
| ( in @ sk6
@ ( descr
@ ^ [D: $i] :
! [E: $i] :
( ( in @ E @ D )
= ( ? [F: $i] :
( ( in @ F @ sk4 )
& ( E
= ( sk5 @ F ) ) ) ) ) ) )
| ( ( in @ C @ ( sk2 @ B @ A ) )
!= ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[14,52]) ).
thf(522,plain,
( ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) )
| ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[521:[bind(A,$thf( sk4 )),bind(B,$thf( sk5 )),bind(C,$thf( sk6 ))]]) ).
thf(550,plain,
( ( ( in @ sk28 @ sk4 )
| ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) )
& ( ( sk6
= ( sk5 @ sk28 ) )
| ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[522]) ).
thf(551,plain,
( ( in @ sk28 @ sk4 )
| ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ),
inference(cnfConj,[status(thm)],[550]) ).
thf(519,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( in @ sk6
@ ( descr
@ ^ [D: $i] :
! [E: $i] :
( ( in @ E @ D )
= ( ? [F: $i] :
( ( in @ F @ sk4 )
& ( E
= ( sk5 @ F ) ) ) ) ) ) )
| ? [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) )
| ( ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
!= ( in @ C @ ( sk2 @ B @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[52,14]) ).
thf(520,plain,
( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[519:[bind(A,$thf( sk4 )),bind(B,$thf( sk5 )),bind(C,$thf( sk6 ))]]) ).
thf(546,plain,
( ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( in @ sk27 @ sk4 ) )
& ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( sk6
= ( sk5 @ sk27 ) ) ) ),
inference(cnf,[status(esa)],[520]) ).
thf(547,plain,
( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( in @ sk27 @ sk4 ) ),
inference(cnfConj,[status(thm)],[546]) ).
thf(2723,plain,
( ( in @ sk27 @ sk4 )
| ~ ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[547,2249]) ).
thf(2724,plain,
( ( in @ sk27 @ sk4 )
| ~ ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) ),
inference(pattern_uni,[status(thm)],[2723:[]]) ).
thf(26,plain,
( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) ) ),
inference(bool_ext,[status(thm)],[17]) ).
thf(29,plain,
( ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( in @ sk7 @ sk4 ) )
& ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( sk6
= ( sk5 @ sk7 ) ) ) ),
inference(cnf,[status(esa)],[26]) ).
thf(30,plain,
( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( in @ sk7 @ sk4 ) ),
inference(cnfConj,[status(thm)],[29]) ).
thf(75,plain,
( ( in @ sk7 @ sk4 )
| ~ ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[30,17]) ).
thf(76,plain,
( ( in @ sk7 @ sk4 )
| ~ ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[75:[]]) ).
thf(104,plain,
! [A: $i] :
( ( in @ sk7 @ sk4 )
| ~ ( in @ A @ sk4 )
| ( sk6
!= ( sk5 @ A ) ) ),
inference(cnf,[status(esa)],[76]) ).
thf(105,plain,
! [A: $i] :
( ( ( sk5 @ A )
!= sk6 )
| ( in @ sk7 @ sk4 )
| ~ ( in @ A @ sk4 ) ),
inference(lifteq,[status(thm)],[104]) ).
thf(33,plain,
! [C: $i,B: $i > $i,A: $i] :
( ~ ( in @ C @ ( sk2 @ B @ A ) )
| ? [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) ) ),
inference(bool_ext,[status(thm)],[14]) ).
thf(41,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( ~ ( in @ C @ ( sk2 @ B @ A ) )
| ( in @ ( sk8 @ C @ B @ A ) @ A ) )
& ( ~ ( in @ C @ ( sk2 @ B @ A ) )
| ( C
= ( B @ ( sk8 @ C @ B @ A ) ) ) ) ),
inference(cnf,[status(esa)],[33]) ).
thf(43,plain,
! [C: $i,B: $i > $i,A: $i] :
( ~ ( in @ C @ ( sk2 @ B @ A ) )
| ( C
= ( B @ ( sk8 @ C @ B @ A ) ) ) ),
inference(cnfConj,[status(thm)],[41]) ).
thf(44,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( ( B @ ( sk8 @ C @ B @ A ) )
= C )
| ~ ( in @ C @ ( sk2 @ B @ A ) ) ),
inference(lifteq,[status(thm)],[43]) ).
thf(8,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( ( in @ ( sk3 @ C @ B @ A ) @ C )
!= ( ? [D: $i] :
( ( in @ D @ A )
& ( ( sk3 @ C @ B @ A )
= ( B @ D ) ) ) ) )
| ( ( sk2 @ B @ A )
= C ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(23,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( ( in @ ( sk3 @ C @ B @ A ) @ C )
!= ( ? [D: $i] :
( ( in @ D @ A )
& ( ( sk3 @ C @ B @ A )
= ( B @ D ) ) ) ) )
| ( ( sk2 @ B @ A )
= C ) ),
inference(lifteq,[status(thm)],[8]) ).
thf(24,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( ( in @ ( sk3 @ C @ B @ A ) @ C )
!= ( ? [D: $i] :
( ( in @ D @ A )
& ( ( sk3 @ C @ B @ A )
= ( B @ D ) ) ) ) )
| ( ( sk2 @ B @ A )
= C ) ),
inference(simp,[status(thm)],[23]) ).
thf(6440,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( ( in @ ( sk3 @ C @ B @ A ) @ C )
!= ( ? [D: $i] :
( ( in @ D @ A )
& ( ( sk3 @ C @ B @ A )
= ( B @ D ) ) ) ) )
| ( C != sk119 )
| ( ( sk2 @ B @ A )
!= ( sk2 @ sk5 @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[24,6263]) ).
thf(6441,plain,
! [A: $i] :
( ( ( in @ ( sk3 @ A @ sk5 @ sk4 ) @ A )
!= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( ( sk3 @ A @ sk5 @ sk4 )
= ( sk5 @ B ) ) ) ) )
| ( A != sk119 ) ),
inference(pattern_uni,[status(thm)],[6440:[bind(A,$thf( sk4 )),bind(B,$thf( sk5 )),bind(C,$thf( C ))]]) ).
thf(6447,plain,
( ( in @ ( sk3 @ sk119 @ sk5 @ sk4 ) @ sk119 )
!= ( ? [A: $i] :
( ( in @ A @ sk4 )
& ( ( sk3 @ sk119 @ sk5 @ sk4 )
= ( sk5 @ A ) ) ) ) ),
inference(simp,[status(thm)],[6441]) ).
thf(6977,plain,
( ( in @ ( sk3 @ sk119 @ sk5 @ sk4 ) @ sk119 )
| ? [A: $i] :
( ( in @ A @ sk4 )
& ( ( sk3 @ sk119 @ sk5 @ sk4 )
= ( sk5 @ A ) ) ) ),
inference(bool_ext,[status(thm)],[6447]) ).
thf(7061,plain,
( ( ( in @ ( sk3 @ sk119 @ sk5 @ sk4 ) @ sk119 )
| ( in @ sk167 @ sk4 ) )
& ( ( in @ ( sk3 @ sk119 @ sk5 @ sk4 ) @ sk119 )
| ( ( sk3 @ sk119 @ sk5 @ sk4 )
= ( sk5 @ sk167 ) ) ) ),
inference(cnf,[status(esa)],[6977]) ).
thf(7062,plain,
( ( in @ ( sk3 @ sk119 @ sk5 @ sk4 ) @ sk119 )
| ( in @ sk167 @ sk4 ) ),
inference(cnfConj,[status(thm)],[7061]) ).
thf(2712,plain,
( ( sk6 != sk6 )
| ( ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) )
!= ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[2249]) ).
thf(2807,plain,
( ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) )
!= ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[2712]) ).
thf(2785,plain,
! [A: $i] :
( ( sk6 != sk6 )
| ( A
!= ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) )
| ( ( descr @ ( (=) @ $i @ A ) )
!= ( descr
@ ^ [B: $i] :
! [C: $i] :
( ( in @ C @ B )
= ( ? [D: $i] :
( ( in @ D @ sk4 )
& ( C
= ( sk5 @ D ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[2740]) ).
thf(2813,plain,
( ( descr @ ( (=) @ $i @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) )
!= ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[2785]) ).
thf(3972,plain,
! [A: $i] :
( ( A
!= ( descr @ ( (=) @ $i @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) ) )
| ( ( descr @ ( (=) @ $i @ A ) )
!= ( descr
@ ^ [B: $i] :
! [C: $i] :
( ( in @ C @ B )
= ( ? [D: $i] :
( ( in @ D @ sk4 )
& ( C
= ( sk5 @ D ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[2018,2813]) ).
thf(3974,plain,
( ( (=) @ $i @ ( descr @ ( (=) @ $i @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) ) )
!= ( ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3972]) ).
thf(42,plain,
! [C: $i,B: $i > $i,A: $i] :
( ~ ( in @ C @ ( sk2 @ B @ A ) )
| ( in @ ( sk8 @ C @ B @ A ) @ A ) ),
inference(cnfConj,[status(thm)],[41]) ).
thf(20,plain,
! [B: $i,A: $i > $o] :
( ( ( sk1 @ B @ A )
!= B )
| ~ ( A @ B )
| ( A @ ( descr @ A ) ) ),
inference(lifteq,[status(thm)],[7]) ).
thf(548,plain,
( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( sk6
= ( sk5 @ sk27 ) ) ),
inference(cnfConj,[status(thm)],[546]) ).
thf(549,plain,
( ( ( sk5 @ sk27 )
= sk6 )
| ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ),
inference(lifteq,[status(thm)],[548]) ).
thf(2766,plain,
( ( ( sk5 @ sk27 )
= sk6 )
| ~ ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[549,2249]) ).
thf(2767,plain,
( ( ( sk5 @ sk27 )
= sk6 )
| ~ ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) ),
inference(pattern_uni,[status(thm)],[2766:[]]) ).
thf(51,plain,
( ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ~ ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ),
inference(bool_ext,[status(thm)],[37]) ).
thf(961,plain,
( ( in @ sk28 @ sk4 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ~ $true
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[551,51]) ).
thf(962,plain,
( ( in @ sk28 @ sk4 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[961]) ).
thf(963,plain,
( ( in @ sk28 @ sk4 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[962:[]]) ).
thf(1084,plain,
( ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ~ $true
| ( ( in @ sk28 @ sk4 )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[963,51]) ).
thf(1085,plain,
( ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ( ( in @ sk28 @ sk4 )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[1084]) ).
thf(1115,plain,
( ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ( sk28 != sk6 )
| ( ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) )
!= sk4 ) ),
inference(simp,[status(thm)],[1085]) ).
thf(31,plain,
( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( sk6
= ( sk5 @ sk7 ) ) ),
inference(cnfConj,[status(thm)],[29]) ).
thf(32,plain,
( ( ( sk5 @ sk7 )
= sk6 )
| ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ),
inference(lifteq,[status(thm)],[31]) ).
thf(412,plain,
( ( ( sk5 @ sk7 )
= sk6 )
| ~ ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[32,17]) ).
thf(413,plain,
( ( ( sk5 @ sk7 )
= sk6 )
| ~ ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[412:[]]) ).
thf(442,plain,
! [A: $i] :
( ( ( sk5 @ sk7 )
= sk6 )
| ~ ( in @ A @ sk4 )
| ( sk6
!= ( sk5 @ A ) ) ),
inference(cnf,[status(esa)],[413]) ).
thf(443,plain,
! [A: $i] :
( ( ( sk5 @ A )
!= sk6 )
| ( ( sk5 @ sk7 )
= sk6 )
| ~ ( in @ A @ sk4 ) ),
inference(lifteq,[status(thm)],[442]) ).
thf(2823,plain,
( ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) )
!= ( ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[2807]) ).
thf(2834,plain,
( ( ( sk2 @ sk5 @ sk4 )
= sk100 )
!= ( ! [A: $i] :
( ( in @ A @ sk100 )
= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( A
= ( sk5 @ B ) ) ) ) ) ) ),
inference(func_ext,[status(esa)],[2823]) ).
thf(3907,plain,
( ( ( sk2 @ sk5 @ sk4 )
!= sk100 )
| ~ ! [A: $i] :
( ( in @ A @ sk100 )
= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( A
= ( sk5 @ B ) ) ) ) ) ),
inference(bool_ext,[status(thm)],[2834]) ).
thf(3932,plain,
( ( ( sk2 @ sk5 @ sk4 )
!= sk100 )
| ~ ! [A: $i] :
( ( in @ A @ sk100 )
= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( A
= ( sk5 @ B ) ) ) ) ) ),
inference(lifteq,[status(thm)],[3907]) ).
thf(3943,plain,
( ( ( sk2 @ sk5 @ sk4 )
!= sk100 )
| ( ( in @ sk121 @ sk100 )
!= ( ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk121
= ( sk5 @ A ) ) ) ) ) ),
inference(cnf,[status(esa)],[3932]) ).
thf(3944,plain,
( ( ( in @ sk121 @ sk100 )
!= ( ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk121
= ( sk5 @ A ) ) ) ) )
| ( ( sk2 @ sk5 @ sk4 )
!= sk100 ) ),
inference(lifteq,[status(thm)],[3943]) ).
thf(4001,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( ( in @ C @ ( sk2 @ B @ A ) )
!= ( in @ sk121 @ sk100 ) )
| ( ( sk2 @ sk5 @ sk4 )
!= sk100 )
| ( ( ? [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) ) )
!= ( ? [D: $i] :
( ( in @ D @ sk4 )
& ( sk121
= ( sk5 @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[14,3944]) ).
thf(4002,plain,
( ( ( in @ sk121 @ ( sk2 @ sk5 @ sk4 ) )
!= ( in @ sk121 @ sk100 ) )
| ( ( sk2 @ sk5 @ sk4 )
!= sk100 ) ),
inference(pattern_uni,[status(thm)],[4001:[bind(A,$thf( sk4 )),bind(B,$thf( sk5 )),bind(C,$thf( sk121 ))]]) ).
thf(4120,plain,
( ( sk121 != sk121 )
| ( ( sk2 @ sk5 @ sk4 )
!= sk100 )
| ( ( sk2 @ sk5 @ sk4 )
!= sk100 ) ),
inference(simp,[status(thm)],[4002]) ).
thf(4193,plain,
( ( sk2 @ sk5 @ sk4 )
!= sk100 ),
inference(simp,[status(thm)],[4120]) ).
thf(4447,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( ( in @ ( sk3 @ C @ B @ A ) @ C )
!= ( ? [D: $i] :
( ( in @ D @ A )
& ( ( sk3 @ C @ B @ A )
= ( B @ D ) ) ) ) )
| ( C != sk100 )
| ( ( sk2 @ B @ A )
!= ( sk2 @ sk5 @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[24,4193]) ).
thf(4448,plain,
! [A: $i] :
( ( ( in @ ( sk3 @ A @ sk5 @ sk4 ) @ A )
!= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( ( sk3 @ A @ sk5 @ sk4 )
= ( sk5 @ B ) ) ) ) )
| ( A != sk100 ) ),
inference(pattern_uni,[status(thm)],[4447:[bind(A,$thf( sk4 )),bind(B,$thf( sk5 )),bind(C,$thf( C ))]]) ).
thf(4454,plain,
( ( in @ ( sk3 @ sk100 @ sk5 @ sk4 ) @ sk100 )
!= ( ? [A: $i] :
( ( in @ A @ sk4 )
& ( ( sk3 @ sk100 @ sk5 @ sk4 )
= ( sk5 @ A ) ) ) ) ),
inference(simp,[status(thm)],[4448]) ).
thf(3973,plain,
( ( descr @ ( (=) @ $i @ ( descr @ ( (=) @ $i @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) ) ) )
!= ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3972]) ).
thf(772,plain,
( ( ( sk5 @ sk27 )
= sk6 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ~ $true
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[549,51]) ).
thf(773,plain,
( ( ( sk5 @ sk27 )
= sk6 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[772]) ).
thf(774,plain,
( ( ( sk5 @ sk27 )
= sk6 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[773:[]]) ).
thf(2771,plain,
( ( in @ sk7 @ sk4 )
| ~ ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[30,2249]) ).
thf(2772,plain,
( ( in @ sk7 @ sk4 )
| ~ ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) ),
inference(pattern_uni,[status(thm)],[2771:[]]) ).
thf(25,plain,
( ~ ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ~ ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) ) ),
inference(bool_ext,[status(thm)],[17]) ).
thf(27,plain,
! [A: $i] :
( ~ ( in @ sk6
@ ( descr
@ ^ [B: $i] :
! [C: $i] :
( ( in @ C @ B )
= ( ? [D: $i] :
( ( in @ D @ sk4 )
& ( C
= ( sk5 @ D ) ) ) ) ) ) )
| ~ ( in @ A @ sk4 )
| ( sk6
!= ( sk5 @ A ) ) ),
inference(cnf,[status(esa)],[25]) ).
thf(28,plain,
! [A: $i] :
( ( ( sk5 @ A )
!= sk6 )
| ~ ( in @ sk6
@ ( descr
@ ^ [B: $i] :
! [C: $i] :
( ( in @ C @ B )
= ( ? [D: $i] :
( ( in @ D @ sk4 )
& ( C
= ( sk5 @ D ) ) ) ) ) ) )
| ~ ( in @ A @ sk4 ) ),
inference(lifteq,[status(thm)],[27]) ).
thf(35,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( ( ? [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) ) )
!= ( ? [D: $i] :
( ( in @ D @ sk4 )
& ( sk6
= ( sk5 @ D ) ) ) ) )
| ( ( in @ C @ ( sk2 @ B @ A ) )
!= ( in @ sk6
@ ( descr
@ ^ [D: $i] :
! [E: $i] :
( ( in @ E @ D )
= ( ? [F: $i] :
( ( in @ F @ sk4 )
& ( E
= ( sk5 @ F ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[14,17]) ).
thf(38,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( ( ^ [D: $i] :
( ( in @ D @ A )
& ( C
= ( B @ D ) ) ) )
!= ( ^ [D: $i] :
( ( in @ D @ sk4 )
& ( sk6
= ( sk5 @ D ) ) ) ) )
| ( ( in @ C @ ( sk2 @ B @ A ) )
!= ( in @ sk6
@ ( descr
@ ^ [D: $i] :
! [E: $i] :
( ( in @ E @ D )
= ( ? [F: $i] :
( ( in @ F @ sk4 )
& ( E
= ( sk5 @ F ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[35]) ).
thf(4910,plain,
( ( in @ ( sk3 @ sk100 @ sk5 @ sk4 ) @ sk100 )
| ? [A: $i] :
( ( in @ A @ sk4 )
& ( ( sk3 @ sk100 @ sk5 @ sk4 )
= ( sk5 @ A ) ) ) ),
inference(bool_ext,[status(thm)],[4454]) ).
thf(5028,plain,
( ( ( in @ ( sk3 @ sk100 @ sk5 @ sk4 ) @ sk100 )
| ( in @ sk137 @ sk4 ) )
& ( ( in @ ( sk3 @ sk100 @ sk5 @ sk4 ) @ sk100 )
| ( ( sk3 @ sk100 @ sk5 @ sk4 )
= ( sk5 @ sk137 ) ) ) ),
inference(cnf,[status(esa)],[4910]) ).
thf(5030,plain,
( ( in @ ( sk3 @ sk100 @ sk5 @ sk4 ) @ sk100 )
| ( ( sk3 @ sk100 @ sk5 @ sk4 )
= ( sk5 @ sk137 ) ) ),
inference(cnfConj,[status(thm)],[5028]) ).
thf(5031,plain,
( ( ( sk3 @ sk100 @ sk5 @ sk4 )
= ( sk5 @ sk137 ) )
| ( in @ ( sk3 @ sk100 @ sk5 @ sk4 ) @ sk100 ) ),
inference(lifteq,[status(thm)],[5030]) ).
thf(5930,plain,
! [A: $i] :
( ( A
!= ( descr @ ( (=) @ $i @ ( descr @ ( (=) @ $i @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) ) ) ) )
| ( ( descr @ ( (=) @ $i @ A ) )
!= ( descr
@ ^ [B: $i] :
! [C: $i] :
( ( in @ C @ B )
= ( ? [D: $i] :
( ( in @ D @ sk4 )
& ( C
= ( sk5 @ D ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[2018,3973]) ).
thf(5932,plain,
( ( (=) @ $i @ ( descr @ ( (=) @ $i @ ( descr @ ( (=) @ $i @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) ) ) ) )
!= ( ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5930]) ).
thf(583,plain,
( ( in @ sk27 @ sk4 )
| ~ ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[547,17]) ).
thf(584,plain,
( ( in @ sk27 @ sk4 )
| ~ ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[583:[]]) ).
thf(621,plain,
! [A: $i] :
( ( in @ sk27 @ sk4 )
| ~ ( in @ A @ sk4 )
| ( sk6
!= ( sk5 @ A ) ) ),
inference(cnf,[status(esa)],[584]) ).
thf(622,plain,
! [A: $i] :
( ( ( sk5 @ A )
!= sk6 )
| ( in @ sk27 @ sk4 )
| ~ ( in @ A @ sk4 ) ),
inference(lifteq,[status(thm)],[621]) ).
thf(592,plain,
( ( in @ sk27 @ sk4 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ~ $true
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[547,51]) ).
thf(593,plain,
( ( in @ sk27 @ sk4 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[592]) ).
thf(594,plain,
( ( in @ sk27 @ sk4 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[593:[]]) ).
thf(696,plain,
( ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ~ $true
| ( ( in @ sk27 @ sk4 )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[594,51]) ).
thf(697,plain,
( ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ( ( in @ sk27 @ sk4 )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[696]) ).
thf(701,plain,
( ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ( sk27 != sk6 )
| ( ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) )
!= sk4 ) ),
inference(simp,[status(thm)],[697]) ).
thf(80,plain,
( ( in @ sk7 @ sk4 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ~ $true
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[30,51]) ).
thf(81,plain,
( ( in @ sk7 @ sk4 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[80]) ).
thf(82,plain,
( ( in @ sk7 @ sk4 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[81:[]]) ).
thf(142,plain,
( ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ~ $true
| ( ( in @ sk7 @ sk4 )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[82,51]) ).
thf(143,plain,
( ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ( ( in @ sk7 @ sk4 )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[142]) ).
thf(148,plain,
( ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ( sk7 != sk6 )
| ( ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) )
!= sk4 ) ),
inference(simp,[status(thm)],[143]) ).
thf(5882,plain,
( ( ( descr @ ( (=) @ $i @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) )
= sk149 )
!= ( ! [A: $i] :
( ( in @ A @ sk149 )
= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( A
= ( sk5 @ B ) ) ) ) ) ) ),
inference(func_ext,[status(esa)],[3974]) ).
thf(5959,plain,
! [A: $i] :
( ( ( A = sk149 )
!= ( ! [B: $i] :
( ( in @ B @ sk149 )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( ( descr @ ( (=) @ $i @ A ) )
!= ( descr @ ( (=) @ $i @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[2018,5882]) ).
thf(5960,plain,
( ( ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) )
= sk149 )
!= ( ! [A: $i] :
( ( in @ A @ sk149 )
= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( A
= ( sk5 @ B ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[5959:[bind(A,$thf( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ))]]) ).
thf(2720,plain,
( ( in @ sk28 @ sk4 )
| ~ ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[551,2249]) ).
thf(2721,plain,
( ( in @ sk28 @ sk4 )
| ~ ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) ),
inference(pattern_uni,[status(thm)],[2720:[]]) ).
thf(552,plain,
( ( sk6
= ( sk5 @ sk28 ) )
| ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ),
inference(cnfConj,[status(thm)],[550]) ).
thf(553,plain,
( ( ( sk5 @ sk28 )
= sk6 )
| ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ),
inference(lifteq,[status(thm)],[552]) ).
thf(2756,plain,
( ( ( sk5 @ sk28 )
= sk6 )
| ~ ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[553,2249]) ).
thf(2757,plain,
( ( ( sk5 @ sk28 )
= sk6 )
| ~ ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) ),
inference(pattern_uni,[status(thm)],[2756:[]]) ).
thf(2714,plain,
( ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) )
| ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ),
inference(bool_ext,[status(thm)],[2249]) ).
thf(2880,plain,
! [C: $i,B: $i > $i,A: $i] :
( ( in @ sk6
@ ( descr
@ ^ [D: $i] :
! [E: $i] :
( ( in @ E @ D )
= ( ? [F: $i] :
( ( in @ F @ sk4 )
& ( E
= ( sk5 @ F ) ) ) ) ) ) )
| ? [D: $i] :
( ( in @ D @ C )
& ( A
= ( B @ D ) ) )
| ( ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) )
!= ( in @ A @ ( descr @ ( (=) @ $i @ ( sk2 @ B @ C ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[2714,2185]) ).
thf(2881,plain,
( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ? [A: $i] :
( ( in @ A @ sk4 )
& ( sk6
= ( sk5 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[2880:[bind(A,$thf( sk6 )),bind(B,$thf( sk5 )),bind(C,$thf( sk4 ))]]) ).
thf(3029,plain,
( ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( in @ sk105 @ sk4 ) )
& ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( sk6
= ( sk5 @ sk105 ) ) ) ),
inference(cnf,[status(esa)],[2881]) ).
thf(3030,plain,
( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( in @ sk105 @ sk4 ) ),
inference(cnfConj,[status(thm)],[3029]) ).
thf(4294,plain,
( ( in @ sk105 @ sk4 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ~ $true
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3030,51]) ).
thf(4295,plain,
( ( in @ sk105 @ sk4 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[4294]) ).
thf(4296,plain,
( ( in @ sk105 @ sk4 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[4295:[]]) ).
thf(1470,plain,
( ( ( sk5 @ sk28 )
= sk6 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ~ $true
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[553,51]) ).
thf(1471,plain,
( ( ( sk5 @ sk28 )
= sk6 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[1470]) ).
thf(1472,plain,
( ( ( sk5 @ sk28 )
= sk6 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[1471:[]]) ).
thf(240,plain,
! [B: $i,A: $i > $o] :
( ( in @ sk6
@ ( descr
@ ^ [C: $i] :
! [D: $i] :
( ( in @ D @ C )
= ( ? [E: $i] :
( ( in @ E @ sk4 )
& ( D
= ( sk5 @ E ) ) ) ) ) ) )
| ~ $true
| ( A @ ( sk1 @ B @ A ) )
| ( A @ ( descr @ A ) )
| ( ( in @ sk7 @ sk4 )
!= ( A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[30,10]) ).
thf(241,plain,
! [B: $i,A: $i > $o] :
( ( in @ sk6
@ ( descr
@ ^ [C: $i] :
! [D: $i] :
( ( in @ D @ C )
= ( ? [E: $i] :
( ( in @ E @ sk4 )
& ( D
= ( sk5 @ E ) ) ) ) ) ) )
| ( A @ ( sk1 @ B @ A ) )
| ( A @ ( descr @ A ) )
| ( ( in @ sk7 @ sk4 )
!= ( A @ B ) ) ),
inference(simp,[status(thm)],[240]) ).
thf(304,plain,
( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( in
@ ( sk1 @ sk7
@ ^ [A: $i] : ( in @ A @ sk4 ) )
@ sk4 )
| ( in
@ ( descr
@ ^ [A: $i] : ( in @ A @ sk4 ) )
@ sk4 ) ),
inference(pre_uni,[status(thm)],[241:[bind(A,$thf( ^ [C: $i] : ( in @ C @ sk4 ) )),bind(B,$thf( sk7 ))]]) ).
thf(6002,plain,
! [A: $i] :
( ( ( A = sk149 )
!= ( ! [B: $i] :
( ( in @ B @ sk149 )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
| ( ( descr @ ( (=) @ $i @ A ) )
!= ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[2018,5960]) ).
thf(6003,plain,
( ( ( sk2 @ sk5 @ sk4 )
= sk149 )
!= ( ! [A: $i] :
( ( in @ A @ sk149 )
= ( ? [B: $i] :
( ( in @ B @ sk4 )
& ( A
= ( sk5 @ B ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[6002:[bind(A,$thf( sk2 @ sk5 @ sk4 ))]]) ).
thf(50,plain,
( ( sk6 != sk6 )
| ( ( sk2 @ sk5 @ sk4 )
!= ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[37]) ).
thf(55,plain,
( ( sk2 @ sk5 @ sk4 )
!= ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[50]) ).
thf(416,plain,
( ( ( sk5 @ sk7 )
= sk6 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ~ $true
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[32,51]) ).
thf(417,plain,
( ( ( sk5 @ sk7 )
= sk6 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[416]) ).
thf(418,plain,
( ( ( sk5 @ sk7 )
= sk6 )
| ~ ( in @ sk6 @ ( sk2 @ sk5 @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[417:[]]) ).
thf(2753,plain,
( ( ( sk5 @ sk7 )
= sk6 )
| ~ ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) )
| ( ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) )
!= ( in @ sk6
@ ( descr
@ ^ [A: $i] :
! [B: $i] :
( ( in @ B @ A )
= ( ? [C: $i] :
( ( in @ C @ sk4 )
& ( B
= ( sk5 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[32,2249]) ).
thf(2754,plain,
( ( ( sk5 @ sk7 )
= sk6 )
| ~ ( in @ sk6 @ ( descr @ ( (=) @ $i @ ( sk2 @ sk5 @ sk4 ) ) ) ) ),
inference(pattern_uni,[status(thm)],[2753:[]]) ).
thf(5029,plain,
( ( in @ ( sk3 @ sk100 @ sk5 @ sk4 ) @ sk100 )
| ( in @ sk137 @ sk4 ) ),
inference(cnfConj,[status(thm)],[5028]) ).
thf(15367,plain,
$false,
inference(e,[status(thm)],[6263,10,551,2724,105,44,7062,3,2807,6447,3974,42,24,37,3891,52,14,2814,2185,20,2767,1115,443,4454,3973,774,2772,2249,28,38,5031,5932,547,622,701,2813,32,148,5960,5882,17,2721,5071,594,2757,4296,1472,553,963,304,2823,6003,55,418,549,82,30,51,2714,3030,4193,2754,5029,2018,2834]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU795^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21 % Computer : n003.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Tue Sep 29 14:32:35 UTC 2026
% 0.10/0.21 % CPUTime :
% 0.10/0.21 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.65/0.50 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.07/0.63 % [INFO] Parsing done (128ms).
% 1.07/0.64 % [INFO] Running in sequential loop mode.
% 1.78/1.05 % [INFO] eprover registered as external prover.
% 1.78/1.06 % [INFO] Scanning for conjecture ...
% 1.96/1.19 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.11/1.23 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.11/1.23 % [INFO] Problem is higher-order (TPTP THF).
% 2.11/1.23 % [INFO] Type checking passed.
% 2.11/1.24 % [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 ...
% 87.83/22.62 % External prover 'e' found a proof!
% 87.83/22.62 % [INFO] Killing All external provers ...
% 87.83/22.62 % Time passed: 22332ms (effective reasoning time: 21976ms)
% 87.83/22.62 % 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)>
% 87.83/22.63 % Axioms used in derivation (0):
% 87.83/22.63 % No. of inferences in proof: 177
% 87.83/22.63 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 22332 ms resp. 21976 ms w/o parsing
% 88.76/22.82 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 88.76/22.82 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------