%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEV204^5 : TPTP v9.3.1. Released 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 : n015.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:37:00 AM UTC 2026
% Result : Theorem 251.37s 87.46s
% Output : Refutation 243.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 6
% Syntax : Number of formulae : 354 ( 90 unt; 0 typ; 5 def)
% Number of atoms : 1593 ( 658 equ; 98 cnn)
% Maximal formula atoms : 18 ( 4 avg)
% Number of connectives : 6805 ( 675 ~; 578 |; 66 &;5458 @)
% ( 0 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 7 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 167 ( 167 >; 0 *; 0 +; 0 <<)
% Number of symbols : 14 ( 10 usr; 7 con; 0-3 aty)
% Number of variables : 1134 ( 577 ^; 518 !; 34 ?;1134 :)
% ( 0 !>; 0 ?*; 0 @-; 5 @+)
% Comments :
%------------------------------------------------------------------------------
thf(iS_type,type,
iS: $tType ).
thf(y_decl,type,
y: iS ).
thf(x_decl,type,
x: iS ).
thf(cP_decl,type,
cP: iS > iS > iS ).
thf(c0_decl,type,
c0: iS ).
thf(sk1_decl,type,
sk1: ( iS > $o ) > iS ).
thf(sk2_decl,type,
sk2: ( iS > $o ) > iS ).
thf(sk3_decl,type,
sk3: iS > iS > iS > $o ).
thf(sk4_decl,type,
sk4: iS > iS > iS ).
thf(sk5_decl,type,
sk5: iS > iS > iS ).
thf(sk7_decl,type,
sk7: iS ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: iS > $o] :
@+[B: iS] :
~ ! [C: iS] :
( ( ( A @ B )
& ( A @ C ) )
=> ( A @ ( cP @ B @ C ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: iS > $o] :
@+[B: iS] :
~ ( ( ( A @ ( sk1 @ A ) )
& ( A @ B ) )
=> ( A @ ( cP @ ( sk1 @ A ) @ B ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: iS > iS > iS > $o] :
~ ( ! [B: iS,C: iS,D: iS] :
( ( ( ( B = c0 )
& ( C = D ) )
| ( ( C = c0 )
& ( B = D ) )
| ? [E: iS,F: iS] :
( ( B
= ( cP @ E @ F ) )
& ? [G: iS,H: iS] :
( ( C
= ( cP @ G @ H ) )
& ? [I: iS,J: iS] :
( ( D
= ( cP @ I @ J ) )
& ( A @ E @ G @ I )
& ( A @ F @ H @ J ) ) ) ) )
=> ( A @ B @ C @ D ) )
=> ( A @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: iS > iS > iS] :
! [B: iS,C: iS] :
( ( A @ C @ ( cP @ B @ C ) )
= B ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: iS > iS > iS] :
! [B: iS,C: iS] :
( ( A @ B @ ( cP @ B @ C ) )
= C ) ) ) ).
thf(1,conjecture,
( ( ! [A: iS,B: iS] :
( ( cP @ A @ B )
!= c0 )
& ! [A: iS,B: iS,C: iS,D: iS] :
( ( ( cP @ A @ C )
= ( cP @ B @ D ) )
=> ( ( A = B )
& ( C = D ) ) )
& ! [A: iS > $o] :
( ( ( A @ c0 )
& ! [B: iS,C: iS] :
( ( ( A @ B )
& ( A @ C ) )
=> ( A @ ( cP @ B @ C ) ) ) )
=> ! [B: iS] : ( A @ B ) ) )
=> ! [A: iS > iS > iS > $o] :
( ( $true
& ! [B: iS,C: iS,D: iS] :
( ( ( ( B = c0 )
& ( C = D ) )
| ( ( C = c0 )
& ( B = D ) )
| ? [E: iS,F: iS,G: iS,H: iS,I: iS,J: iS] :
( ( B
= ( cP @ E @ F ) )
& ( C
= ( cP @ G @ H ) )
& ( D
= ( cP @ I @ J ) )
& ( A @ E @ G @ I )
& ( A @ F @ H @ J ) ) )
=> ( A @ B @ C @ D ) ) )
=> ( A @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cS_INCL_LEM4_pme) ).
thf(2,negated_conjecture,
~ ( ( ! [A: iS,B: iS] :
( ( cP @ A @ B )
!= c0 )
& ! [A: iS,B: iS,C: iS,D: iS] :
( ( ( cP @ A @ C )
= ( cP @ B @ D ) )
=> ( ( A = B )
& ( C = D ) ) )
& ! [A: iS > $o] :
( ( ( A @ c0 )
& ! [B: iS,C: iS] :
( ( ( A @ B )
& ( A @ C ) )
=> ( A @ ( cP @ B @ C ) ) ) )
=> ! [B: iS] : ( A @ B ) ) )
=> ! [A: iS > iS > iS > $o] :
( ( $true
& ! [B: iS,C: iS,D: iS] :
( ( ( ( B = c0 )
& ( C = D ) )
| ( ( C = c0 )
& ( B = D ) )
| ? [E: iS,F: iS,G: iS,H: iS,I: iS,J: iS] :
( ( B
= ( cP @ E @ F ) )
& ( C
= ( cP @ G @ H ) )
& ( D
= ( cP @ I @ J ) )
& ( A @ E @ G @ I )
& ( A @ F @ H @ J ) ) )
=> ( A @ B @ C @ D ) ) )
=> ( A @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ( ( ! [A: iS,B: iS] :
( ( cP @ A @ B )
!= c0 )
& ! [A: iS,B: iS,C: iS,D: iS] :
( ( ( cP @ A @ C )
= ( cP @ B @ D ) )
=> ( ( A = B )
& ( C = D ) ) )
& ! [A: iS > $o] :
( ( ( A @ c0 )
& ! [B: iS,C: iS] :
( ( ( A @ B )
& ( A @ C ) )
=> ( A @ ( cP @ B @ C ) ) ) )
=> ! [B: iS] : ( A @ B ) ) )
=> ! [A: iS > iS > iS > $o] :
( ! [B: iS,C: iS,D: iS] :
( ( ( ( B = c0 )
& ( C = D ) )
| ( ( C = c0 )
& ( B = D ) )
| ? [E: iS,F: iS,G: iS,H: iS,I: iS,J: iS] :
( ( B
= ( cP @ E @ F ) )
& ( C
= ( cP @ G @ H ) )
& ( D
= ( cP @ I @ J ) )
& ( A @ E @ G @ I )
& ( A @ F @ H @ J ) ) )
=> ( A @ B @ C @ D ) )
=> ( A @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
~ ( ( ~ ? [A: iS,B: iS] :
( ( cP @ A @ B )
= c0 )
& ! [A: iS,B: iS,C: iS,D: iS] :
( ( ( cP @ A @ C )
= ( cP @ B @ D ) )
=> ( ( A = B )
& ( C = D ) ) )
& ! [A: iS > $o] :
( ( ( A @ c0 )
& ! [B: iS,C: iS] :
( ( ( A @ B )
& ( A @ C ) )
=> ( A @ ( cP @ B @ C ) ) ) )
=> ! [B: iS] : ( A @ B ) ) )
=> ! [A: iS > iS > iS > $o] :
( ! [B: iS,C: iS,D: iS] :
( ( ( ( B = c0 )
& ( C = D ) )
| ( ( C = c0 )
& ( B = D ) )
| ? [E: iS,F: iS] :
( ( B
= ( cP @ E @ F ) )
& ? [G: iS,H: iS] :
( ( C
= ( cP @ G @ H ) )
& ? [I: iS,J: iS] :
( ( D
= ( cP @ I @ J ) )
& ( A @ E @ G @ I )
& ( A @ F @ H @ J ) ) ) ) )
=> ( A @ B @ C @ D ) )
=> ( A @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ),
inference(miniscope,[status(thm)],[3]) ).
thf(5,plain,
! [Q: iS,P: iS,O: iS,N: iS,M: iS,L: iS,K: iS,J: iS,I: iS,H: iS,G: iS > $o,F: iS,E: iS,D: iS,C: iS,B: iS,A: iS] :
( ( ( cP @ A @ B )
!= c0 )
& ( ( ( cP @ C @ E )
!= ( cP @ D @ F ) )
| ( C = D ) )
& ( ( ( cP @ C @ E )
!= ( cP @ D @ F ) )
| ( E = F ) )
& ( ~ ( G @ c0 )
| ( G @ ( sk1 @ G ) )
| ( G @ H ) )
& ( ~ ( G @ c0 )
| ( G @ ( sk2 @ G ) )
| ( G @ H ) )
& ( ~ ( G @ c0 )
| ~ ( G @ ( cP @ ( sk1 @ G ) @ ( sk2 @ G ) ) )
| ( G @ H ) )
& ( ( I != c0 )
| ( J != K )
| ( sk3 @ I @ J @ K ) )
& ( ( J != c0 )
| ( I != K )
| ( sk3 @ I @ J @ K ) )
& ( ( I
!= ( cP @ L @ M ) )
| ( J
!= ( cP @ N @ O ) )
| ( K
!= ( cP @ P @ Q ) )
| ~ ( sk3 @ L @ N @ P )
| ~ ( sk3 @ M @ O @ Q )
| ( sk3 @ I @ J @ K ) )
& ~ ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ),
inference(cnf,[status(esa)],[4]) ).
thf(6,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk1 @ A ) )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(17,plain,
! [A: iS] :
( ( c0 != c0 )
| ( c0
= ( sk1 @ ( (=) @ iS @ c0 ) ) )
| ( c0 = A ) ),
inference(replace_leibeq,[status(thm)],[6:[bind(A,$thf( (=) @ iS @ c0 ))]]) ).
thf(28,plain,
! [A: iS] :
( ( c0 != c0 )
| ( ( sk1 @ ( (=) @ iS @ c0 ) )
= c0 )
| ( c0 = A ) ),
inference(lifteq,[status(thm)],[17]) ).
thf(29,plain,
! [A: iS] :
( ( ( sk1 @ ( (=) @ iS @ c0 ) )
= c0 )
| ( c0 = A ) ),
inference(simp,[status(thm)],[28]) ).
thf(13,plain,
! [B: iS,A: iS] :
( ( cP @ A @ B )
!= c0 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(27,plain,
! [B: iS,A: iS] :
( ( cP @ A @ B )
!= c0 ),
inference(lifteq,[status(thm)],[13]) ).
thf(61,plain,
! [C: iS,B: iS,A: iS] :
( ( ( sk1 @ ( (=) @ iS @ c0 ) )
= c0 )
| ( c0 != c0 )
| ( A
!= ( cP @ B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[29,27]) ).
thf(62,plain,
! [C: iS,B: iS,A: iS] :
( ( ( sk1 @ ( (=) @ iS @ c0 ) )
= c0 )
| ( A
!= ( cP @ B @ C ) ) ),
inference(simp,[status(thm)],[61]) ).
thf(63,plain,
( ( sk1 @ ( (=) @ iS @ c0 ) )
= c0 ),
inference(pattern_uni,[status(thm)],[62:[bind(A,$thf( cP @ D @ E )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(11,plain,
! [C: iS,B: iS,A: iS] :
( ( B != c0 )
| ( A != C )
| ( sk3 @ A @ B @ C ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(39,plain,
! [C: iS,B: iS,A: iS] :
( ( B != c0 )
| ( A != C )
| ( sk3 @ A @ B @ C ) ),
inference(lifteq,[status(thm)],[11]) ).
thf(40,plain,
! [A: iS] : ( sk3 @ A @ c0 @ A ),
inference(simp,[status(thm)],[39]) ).
thf(10,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(19,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( A @ B ) ),
inference(simp,[status(thm)],[10]) ).
thf(100,plain,
! [C: iS,B: iS > $o,A: iS] :
( ~ ( B @ c0 )
| ~ $true
| ( B @ C )
| ( ( sk3 @ A @ c0 @ A )
!= ( B @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,19]) ).
thf(101,plain,
! [C: iS,B: iS > $o,A: iS] :
( ~ ( B @ c0 )
| ( B @ C )
| ( ( sk3 @ A @ c0 @ A )
!= ( B @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ) ) ),
inference(simp,[status(thm)],[100]) ).
thf(133,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ~ ( sk3 @ ( B @ c0 ) @ c0 @ ( C @ c0 ) )
| ( sk3 @ ( B @ A ) @ c0 @ ( C @ A ) )
| ( ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) ) ) )
!= ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[101:[bind(A,$thf( D @ ( cP @ ( sk1 @ ^ [F: iS] : ( sk3 @ ( D @ F ) @ c0 @ ( F @ F ) ) ) @ ( sk2 @ ^ [F: iS] : ( sk3 @ ( D @ F ) @ c0 @ ( F @ F ) ) ) ) )),bind(B,$thf( ^ [F: iS] : ( sk3 @ ( D @ F ) @ c0 @ ( F @ F ) ) )),bind(C,$thf( C ))]]) ).
thf(134,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ( sk3 @ ( B @ A ) @ c0 @ ( C @ A ) )
| ~ ( sk3 @ ( B @ c0 ) @ c0 @ ( C @ c0 ) )
| ( ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) ) ) )
!= ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[133:[]]) ).
thf(159,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ( sk3 @ ( B @ A ) @ c0 @ ( C @ A ) )
| ~ ( sk3 @ ( B @ c0 ) @ c0 @ ( C @ c0 ) )
| ( ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) ) ) )
!= ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) ) ) ) ) ),
inference(simp,[status(thm)],[134]) ).
thf(9931,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ( sk3 @ ( B @ A ) @ c0 @ c0 )
| ~ ( sk3 @ ( B @ c0 ) @ c0 @ ( C @ c0 ) )
| ( ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) ) ) )
!= ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) ) ) ) )
| ( ( sk1 @ ( (=) @ iS @ c0 ) )
!= ( C @ A ) ) ),
inference(paramod_ordered,[status(thm)],[63,159]) ).
thf(10031,plain,
! [A: iS > iS] :
( ( sk3 @ ( A @ ( sk1 @ ( (=) @ iS @ c0 ) ) ) @ c0 @ c0 )
| ~ ( sk3 @ ( A @ c0 ) @ c0 @ c0 )
| ( ( A
@ ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ ( A @ B ) @ c0 @ B ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ ( A @ B ) @ c0 @ B ) ) ) )
!= ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ ( A @ B ) @ c0 @ B ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ ( A @ B ) @ c0 @ B ) ) ) ) ),
inference(pre_uni,[status(thm)],[9931:[bind(A,$thf( sk1 @ ( (=) @ iS @ c0 ) )),bind(B,$thf( B )),bind(C,$thf( ^ [D: iS] : D ))]]) ).
thf(10034,plain,
( ~ ( sk3 @ c0 @ c0 @ c0 )
| ( sk3 @ ( sk1 @ ( (=) @ iS @ c0 ) ) @ c0 @ c0 ) ),
inference(pre_uni,[status(thm)],[10031:[bind(A,$thf( ^ [B: iS] : B ))]]) ).
thf(10429,plain,
( ~ $true
| ( sk3 @ c0 @ c0 @ c0 ) ),
inference(rewrite,[status(thm)],[10034,40,63]) ).
thf(10430,plain,
sk3 @ c0 @ c0 @ c0,
inference(simp,[status(thm)],[10429]) ).
thf(24,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk1 @ A ) )
| ( A @ B ) ),
inference(simp,[status(thm)],[6]) ).
thf(10477,plain,
! [B: iS,A: iS > $o] :
( ~ $true
| ( A @ ( sk1 @ A ) )
| ( A @ B )
| ( ( sk3 @ c0 @ c0 @ c0 )
!= ( A @ c0 ) ) ),
inference(paramod_ordered,[status(thm)],[10430,24]) ).
thf(10478,plain,
! [B: iS,A: iS > $o] :
( ( A @ ( sk1 @ A ) )
| ( A @ B )
| ( ( sk3 @ c0 @ c0 @ c0 )
!= ( A @ c0 ) ) ),
inference(simp,[status(thm)],[10477]) ).
thf(10606,plain,
! [A: iS] :
( ( sk3
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) )
@ c0
@ c0 )
| ( sk3 @ A @ c0 @ c0 ) ),
inference(pre_uni,[status(thm)],[10478:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ c0 @ c0 ) )),bind(B,$thf( B ))]]) ).
thf(10705,plain,
! [A: iS] :
( ( sk3
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) )
@ c0
@ c0 )
| ( sk3 @ A @ c0 @ c0 ) ),
inference(simp,[status(thm)],[10606]) ).
thf(13580,plain,
! [A: iS] :
( ( sk3
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) )
@ c0
@ c0 )
| ( ( sk3 @ A @ c0 @ c0 )
!= ( sk3
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) )
@ c0
@ c0 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[10705]) ).
thf(13650,plain,
( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ c0 @ c0 ) )
@ c0
@ c0 ),
inference(pattern_uni,[status(thm)],[13580:[bind(A,$thf( sk1 @ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) ))]]) ).
thf(110,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( ( A @ B )
!= ( ~ ( A @ c0 ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[19]) ).
thf(147,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( ( A @ B )
!= ( ~ ( A @ c0 ) ) ) ),
inference(simp,[status(thm)],[110]) ).
thf(98,plain,
! [C: iS,B: iS > $o,A: iS] :
( ~ $true
| ~ ( B @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) )
| ( B @ C )
| ( ( sk3 @ A @ c0 @ A )
!= ( B @ c0 ) ) ),
inference(paramod_ordered,[status(thm)],[40,19]) ).
thf(99,plain,
! [C: iS,B: iS > $o,A: iS] :
( ~ ( B @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) )
| ( B @ C )
| ( ( sk3 @ A @ c0 @ A )
!= ( B @ c0 ) ) ),
inference(simp,[status(thm)],[98]) ).
thf(121,plain,
! [C: iS,B: iS > $o,A: iS] :
( ( ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) )
!= ( cP @ ( sk1 @ ( (=) @ iS @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ) ) @ ( sk2 @ ( (=) @ iS @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ) ) ) )
| ( ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) )
= C )
| ( ( sk3 @ A @ c0 @ A )
!= ( ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) )
= c0 ) ) ),
inference(replace_leibeq,[status(thm)],[99:[bind(A,$thf( A )),bind(B,$thf( (=) @ iS @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ))]]) ).
thf(124,plain,
! [C: iS,B: iS > $o,A: iS] :
( ( ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) )
!= ( cP @ ( sk1 @ ( (=) @ iS @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ) ) @ ( sk2 @ ( (=) @ iS @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ) ) ) )
| ( ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) )
= C )
| ( ( sk3 @ A @ c0 @ A )
!= ( ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) )
= c0 ) ) ),
inference(lifteq,[status(thm)],[121]) ).
thf(400,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ B )
| ~ $true
| ( C @ ( sk1 @ C ) )
| ( C @ D )
| ( ( A @ ( sk1 @ A ) )
!= ( C @ c0 ) ) ),
inference(paramod_ordered,[status(thm)],[24,24]) ).
thf(401,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ B )
| ( C @ ( sk1 @ C ) )
| ( C @ D )
| ( ( A @ ( sk1 @ A ) )
!= ( C @ c0 ) ) ),
inference(simp,[status(thm)],[400]) ).
thf(435,plain,
! [C: iS,B: iS > $o,A: iS] :
( ( c0 != c0 )
| ( c0 = A )
| ( B @ ( sk1 @ B ) )
| ( B @ C )
| ( ( c0
= ( sk1 @ ( (=) @ iS @ c0 ) ) )
!= ( B @ c0 ) ) ),
inference(replace_leibeq,[status(thm)],[401:[bind(A,$thf( (=) @ iS @ c0 ))]]) ).
thf(449,plain,
! [C: iS,B: iS > $o,A: iS] :
( ( c0 != c0 )
| ( c0 = A )
| ( B @ ( sk1 @ B ) )
| ( B @ C )
| ( ( c0
= ( sk1 @ ( (=) @ iS @ c0 ) ) )
!= ( B @ c0 ) ) ),
inference(lifteq,[status(thm)],[435]) ).
thf(464,plain,
! [B: iS,A: iS] :
( ( c0
= ( sk1 @ ( (=) @ iS @ B ) ) )
| ( c0
= ( sk1
@ ( (=) @ iS
@ ( sk1
@ ^ [C: iS] :
( c0
= ( sk1 @ ( (=) @ iS @ C ) ) ) ) ) ) )
| ( c0 = A ) ),
inference(pre_uni,[status(thm)],[449:[bind(A,$thf( A )),bind(B,$thf( ^ [D: iS] : ( c0 = ( sk1 @ ( (=) @ iS @ D ) ) ) )),bind(C,$thf( C ))]]) ).
thf(515,plain,
! [B: iS,A: iS] :
( ( ( sk1 @ ( (=) @ iS @ B ) )
= c0 )
| ( ( sk1
@ ( (=) @ iS
@ ( sk1
@ ^ [C: iS] :
( c0
= ( sk1 @ ( (=) @ iS @ C ) ) ) ) ) )
= c0 )
| ( c0 = A ) ),
inference(lifteq,[status(thm)],[464]) ).
thf(516,plain,
! [B: iS,A: iS] :
( ( ( sk1 @ ( (=) @ iS @ B ) )
= c0 )
| ( ( sk1
@ ( (=) @ iS
@ ( sk1
@ ^ [C: iS] :
( c0
= ( sk1 @ ( (=) @ iS @ C ) ) ) ) ) )
= c0 )
| ( c0 = A ) ),
inference(simp,[status(thm)],[515]) ).
thf(1403,plain,
! [B: iS,A: iS] :
( ( ( sk1 @ ( (=) @ iS @ B ) )
= c0 )
| ( c0 = A )
| ( ( sk1
@ ( (=) @ iS
@ ( sk1
@ ^ [C: iS] :
( c0
= ( sk1 @ ( (=) @ iS @ C ) ) ) ) ) )
!= ( sk1 @ ( (=) @ iS @ B ) ) )
| ( c0 != c0 ) ),
inference(eqfactor_ordered,[status(thm)],[516]) ).
thf(1442,plain,
! [A: iS] :
( ( ( sk1
@ ( (=) @ iS
@ ( sk1
@ ^ [B: iS] :
( c0
= ( sk1 @ ( (=) @ iS @ B ) ) ) ) ) )
= c0 )
| ( c0 = A ) ),
inference(pattern_uni,[status(thm)],[1403:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ^ [C: iS] : ( c0 = ( sk1 @ ( (=) @ iS @ C ) ) ) ))]]) ).
thf(1651,plain,
! [C: iS,B: iS,A: iS] :
( ( ( sk1
@ ( (=) @ iS
@ ( sk1
@ ^ [D: iS] :
( c0
= ( sk1 @ ( (=) @ iS @ D ) ) ) ) ) )
= c0 )
| ( c0 != c0 )
| ( A
!= ( cP @ B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[1442,27]) ).
thf(1652,plain,
! [C: iS,B: iS,A: iS] :
( ( ( sk1
@ ( (=) @ iS
@ ( sk1
@ ^ [D: iS] :
( c0
= ( sk1 @ ( (=) @ iS @ D ) ) ) ) ) )
= c0 )
| ( A
!= ( cP @ B @ C ) ) ),
inference(simp,[status(thm)],[1651]) ).
thf(1653,plain,
( ( sk1
@ ( (=) @ iS
@ ( sk1
@ ^ [A: iS] :
( c0
= ( sk1 @ ( (=) @ iS @ A ) ) ) ) ) )
= c0 ),
inference(pattern_uni,[status(thm)],[1652:[bind(A,$thf( cP @ D @ E )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(9,plain,
! [I: iS,H: iS,G: iS,F: iS,E: iS,D: iS,C: iS,B: iS,A: iS] :
( ( A
!= ( cP @ D @ E ) )
| ( B
!= ( cP @ F @ G ) )
| ( C
!= ( cP @ H @ I ) )
| ~ ( sk3 @ D @ F @ H )
| ~ ( sk3 @ E @ G @ I )
| ( sk3 @ A @ B @ C ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(25,plain,
! [I: iS,H: iS,G: iS,F: iS,E: iS,D: iS,C: iS,B: iS,A: iS] :
( ( A
!= ( cP @ D @ E ) )
| ( B
!= ( cP @ F @ G ) )
| ( C
!= ( cP @ H @ I ) )
| ~ ( sk3 @ D @ F @ H )
| ~ ( sk3 @ E @ G @ I )
| ( sk3 @ A @ B @ C ) ),
inference(lifteq,[status(thm)],[9]) ).
thf(26,plain,
! [F: iS,E: iS,D: iS,C: iS,B: iS,A: iS] :
( ~ ( sk3 @ A @ C @ E )
| ~ ( sk3 @ B @ D @ F )
| ( sk3 @ ( cP @ A @ B ) @ ( cP @ C @ D ) @ ( cP @ E @ F ) ) ),
inference(simp,[status(thm)],[25]) ).
thf(8,plain,
~ ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(555,plain,
! [F: iS,E: iS,D: iS,C: iS,B: iS,A: iS] :
( ~ ( sk3 @ A @ C @ E )
| ~ ( sk3 @ B @ D @ F )
| ~ $true
| ( ( sk3 @ ( cP @ A @ B ) @ ( cP @ C @ D ) @ ( cP @ E @ F ) )
!= ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ),
inference(paramod_ordered,[status(thm)],[26,8]) ).
thf(556,plain,
! [F: iS,E: iS,D: iS,C: iS,B: iS,A: iS] :
( ~ ( sk3 @ A @ C @ E )
| ~ ( sk3 @ B @ D @ F )
| ( ( sk3 @ ( cP @ A @ B ) @ ( cP @ C @ D ) @ ( cP @ E @ F ) )
!= ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ),
inference(simp,[status(thm)],[555]) ).
thf(557,plain,
( ~ ( sk3 @ x @ x @ x )
| ~ ( sk3 @ c0 @ y @ y ) ),
inference(pattern_uni,[status(thm)],[556:[bind(A,$thf( x )),bind(B,$thf( c0 )),bind(C,$thf( x )),bind(D,$thf( y )),bind(E,$thf( x )),bind(F,$thf( y ))]]) ).
thf(15,plain,
! [C: iS,B: iS,A: iS] :
( ( A != c0 )
| ( B != C )
| ( sk3 @ A @ B @ C ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(41,plain,
! [C: iS,B: iS,A: iS] :
( ( A != c0 )
| ( B != C )
| ( sk3 @ A @ B @ C ) ),
inference(lifteq,[status(thm)],[15]) ).
thf(42,plain,
! [A: iS] : ( sk3 @ c0 @ A @ A ),
inference(simp,[status(thm)],[41]) ).
thf(647,plain,
( ~ ( sk3 @ x @ x @ x )
| ~ $true ),
inference(rewrite,[status(thm)],[557,42]) ).
thf(648,plain,
~ ( sk3 @ x @ x @ x ),
inference(simp,[status(thm)],[647]) ).
thf(653,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk1 @ A ) )
| ~ $true
| ( ( A @ B )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[24,648]) ).
thf(654,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk1 @ A ) )
| ( ( A @ B )
!= ( sk3 @ x @ x @ x ) ) ),
inference(simp,[status(thm)],[653]) ).
thf(672,plain,
( ~ ( sk3 @ c0 @ x @ x )
| ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ) ),
inference(pre_uni,[status(thm)],[654:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ x @ x ) )),bind(B,$thf( x ))]]) ).
thf(727,plain,
( ~ $true
| ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ) ),
inference(rewrite,[status(thm)],[672,42]) ).
thf(728,plain,
( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ),
inference(simp,[status(thm)],[727]) ).
thf(730,plain,
( ~ $true
| ( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x )
!= ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ),
inference(paramod_ordered,[status(thm)],[728,8]) ).
thf(731,plain,
( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x )
!= ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ),
inference(simp,[status(thm)],[730]) ).
thf(756,plain,
( ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
!= ( cP @ x @ c0 ) )
| ( ( cP @ x @ y )
!= x )
| ( ( cP @ x @ y )
!= x ) ),
inference(simp,[status(thm)],[731]) ).
thf(762,plain,
( ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
!= ( cP @ x @ c0 ) )
| ( ( cP @ x @ y )
!= x ) ),
inference(simp,[status(thm)],[756]) ).
thf(7,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk2 @ A ) )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(18,plain,
! [A: iS] :
( ( c0 != c0 )
| ( c0
= ( sk2 @ ( (=) @ iS @ c0 ) ) )
| ( c0 = A ) ),
inference(replace_leibeq,[status(thm)],[7:[bind(A,$thf( (=) @ iS @ c0 ))]]) ).
thf(35,plain,
! [A: iS] :
( ( c0 != c0 )
| ( ( sk2 @ ( (=) @ iS @ c0 ) )
= c0 )
| ( c0 = A ) ),
inference(lifteq,[status(thm)],[18]) ).
thf(36,plain,
! [A: iS] :
( ( ( sk2 @ ( (=) @ iS @ c0 ) )
= c0 )
| ( c0 = A ) ),
inference(simp,[status(thm)],[35]) ).
thf(192,plain,
! [C: iS,B: iS,A: iS] :
( ( ( sk2 @ ( (=) @ iS @ c0 ) )
= c0 )
| ( c0 != c0 )
| ( A
!= ( cP @ B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[36,27]) ).
thf(193,plain,
! [C: iS,B: iS,A: iS] :
( ( ( sk2 @ ( (=) @ iS @ c0 ) )
= c0 )
| ( A
!= ( cP @ B @ C ) ) ),
inference(simp,[status(thm)],[192]) ).
thf(194,plain,
( ( sk2 @ ( (=) @ iS @ c0 ) )
= c0 ),
inference(pattern_uni,[status(thm)],[193:[bind(A,$thf( cP @ D @ E )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(659,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ~ $true
| ( ( A @ B )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[19,648]) ).
thf(660,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( ( A @ B )
!= ( sk3 @ x @ x @ x ) ) ),
inference(simp,[status(thm)],[659]) ).
thf(666,plain,
( ~ ( sk3 @ x @ c0 @ x )
| ~ ( sk3 @ x
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
@ x ) ),
inference(pre_uni,[status(thm)],[660:[bind(A,$thf( ^ [C: iS] : ( sk3 @ x @ C @ x ) )),bind(B,$thf( x ))]]) ).
thf(2041,plain,
( ~ $true
| ~ ( sk3 @ x
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
@ x ) ),
inference(rewrite,[status(thm)],[666,40]) ).
thf(2042,plain,
~ ( sk3 @ x
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
@ x ),
inference(simp,[status(thm)],[2041]) ).
thf(2047,plain,
( ~ ( sk3 @ x
@ ( cP @ c0
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
@ x )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( sk1 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[63,2042]) ).
thf(2079,plain,
( ~ ( sk3 @ x
@ ( cP @ c0
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
@ x )
| ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[2047]) ).
thf(7402,plain,
( ~ ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x )
| ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( sk2 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[194,2079]) ).
thf(7461,plain,
( ~ ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x )
| ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) )
| ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[7402]) ).
thf(7476,plain,
( ~ ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x )
| ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[7461]) ).
thf(7477,plain,
( ( ( sk3 @ x @ sk7 @ x )
!= ( c0 = sk7 ) )
| ~ ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x ) ),
inference(func_ext,[status(esa)],[7476]) ).
thf(671,plain,
( ~ ( sk3 @ x @ c0 @ x )
| ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ),
inference(pre_uni,[status(thm)],[654:[bind(A,$thf( ^ [C: iS] : ( sk3 @ x @ C @ x ) )),bind(B,$thf( x ))]]) ).
thf(682,plain,
( ~ $true
| ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ),
inference(rewrite,[status(thm)],[671,40]) ).
thf(683,plain,
( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ),
inference(simp,[status(thm)],[682]) ).
thf(655,plain,
! [A: iS] :
( ~ $true
| ( ( sk3 @ A @ c0 @ A )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[40,648]) ).
thf(656,plain,
! [A: iS] :
( ( sk3 @ A @ c0 @ A )
!= ( sk3 @ x @ x @ x ) ),
inference(simp,[status(thm)],[655]) ).
thf(675,plain,
! [A: iS] :
( ( A != x )
| ( c0 != x )
| ( A != x ) ),
inference(simp,[status(thm)],[656]) ).
thf(677,plain,
c0 != x,
inference(simp,[status(thm)],[675]) ).
thf(34,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk2 @ A ) )
| ( A @ B ) ),
inference(simp,[status(thm)],[7]) ).
thf(10444,plain,
! [B: iS,A: iS > $o] :
( ~ $true
| ( A @ ( sk2 @ A ) )
| ( A @ B )
| ( ( sk3 @ c0 @ c0 @ c0 )
!= ( A @ c0 ) ) ),
inference(paramod_ordered,[status(thm)],[10430,34]) ).
thf(10445,plain,
! [B: iS,A: iS > $o] :
( ( A @ ( sk2 @ A ) )
| ( A @ B )
| ( ( sk3 @ c0 @ c0 @ c0 )
!= ( A @ c0 ) ) ),
inference(simp,[status(thm)],[10444]) ).
thf(10625,plain,
! [A: iS] :
( ( sk3 @ c0
@ ( sk2
@ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) )
@ c0 )
| ( sk3 @ c0 @ A @ c0 ) ),
inference(pre_uni,[status(thm)],[10445:[bind(A,$thf( ^ [C: iS] : ( sk3 @ c0 @ C @ c0 ) )),bind(B,$thf( B ))]]) ).
thf(10717,plain,
! [A: iS] :
( ( sk3 @ c0
@ ( sk2
@ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) )
@ c0 )
| ( sk3 @ c0 @ A @ c0 ) ),
inference(simp,[status(thm)],[10625]) ).
thf(17408,plain,
! [A: iS] :
( ( sk3 @ c0
@ ( sk2
@ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) )
@ c0 )
| ( ( sk3 @ c0 @ A @ c0 )
!= ( sk3 @ c0
@ ( sk2
@ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) )
@ c0 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[10717]) ).
thf(17577,plain,
( sk3 @ c0
@ ( sk2
@ ^ [A: iS] : ( sk3 @ c0 @ A @ c0 ) )
@ c0 ),
inference(pattern_uni,[status(thm)],[17408:[bind(A,$thf( sk2 @ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) ))]]) ).
thf(799,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk2 @ A ) )
| ~ $true
| ( ( A @ B )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[34,648]) ).
thf(800,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk2 @ A ) )
| ( ( A @ B )
!= ( sk3 @ x @ x @ x ) ) ),
inference(simp,[status(thm)],[799]) ).
thf(952,plain,
( ~ ( sk3 @ x @ c0 @ x )
| ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ),
inference(pre_uni,[status(thm)],[800:[bind(A,$thf( ^ [C: iS] : ( sk3 @ x @ C @ x ) )),bind(B,$thf( x ))]]) ).
thf(1062,plain,
( ~ $true
| ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ),
inference(rewrite,[status(thm)],[952,40]) ).
thf(1063,plain,
( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ),
inference(simp,[status(thm)],[1062]) ).
thf(108,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ B )
| ( ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
!= ( A @ c0 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[19]) ).
thf(152,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ B )
| ( ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
!= ( A @ c0 ) ) ),
inference(pre_uni,[status(thm)],[108:[]]) ).
thf(153,plain,
! [B: iS,A: iS > $o] :
( ( A @ B )
| ~ ( A @ c0 )
| ( ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
!= ( A @ c0 ) ) ),
inference(pre_uni,[status(thm)],[152:[]]) ).
thf(92,plain,
! [C: iS,B: iS > $o,A: iS] :
( ~ $true
| ~ ( B @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) )
| ( B @ C )
| ( ( sk3 @ c0 @ A @ A )
!= ( B @ c0 ) ) ),
inference(paramod_ordered,[status(thm)],[42,19]) ).
thf(93,plain,
! [C: iS,B: iS > $o,A: iS] :
( ~ ( B @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) )
| ( B @ C )
| ( ( sk3 @ c0 @ A @ A )
!= ( B @ c0 ) ) ),
inference(simp,[status(thm)],[92]) ).
thf(136,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ~ ( sk3
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) )
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) ) )
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) ) ) )
| ( sk3 @ A @ ( B @ A ) @ ( C @ A ) )
| ( ( B @ c0 )
!= ( C @ c0 ) ) ),
inference(pre_uni,[status(thm)],[93:[bind(A,$thf( E @ c0 )),bind(B,$thf( ^ [F: iS] : ( sk3 @ F @ ( E @ F ) @ ( F @ F ) ) )),bind(C,$thf( C ))]]) ).
thf(138,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ( sk3 @ A @ ( B @ A ) @ ( C @ A ) )
| ~ ( sk3
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) )
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) ) )
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) ) ) )
| ( ( B @ c0 )
!= ( C @ c0 ) ) ),
inference(pre_uni,[status(thm)],[136:[]]) ).
thf(161,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ( sk3 @ A @ ( B @ A ) @ ( C @ A ) )
| ~ ( sk3
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) )
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) ) )
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) ) ) )
| ( ( B @ c0 )
!= ( C @ c0 ) ) ),
inference(simp,[status(thm)],[138]) ).
thf(12405,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ~ ( sk3
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) )
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) ) )
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) ) ) )
| ( ( B @ c0 )
!= ( C @ c0 ) )
| ~ $true
| ( ( sk3 @ A @ ( B @ A ) @ ( C @ A ) )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[161,648]) ).
thf(12406,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ~ ( sk3
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) )
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) ) )
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) ) ) )
| ( ( B @ c0 )
!= ( C @ c0 ) )
| ( ( sk3 @ A @ ( B @ A ) @ ( C @ A ) )
!= ( sk3 @ x @ x @ x ) ) ),
inference(simp,[status(thm)],[12405]) ).
thf(12830,plain,
( ~ ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) )
| ( c0 != c0 ) ),
inference(pre_uni,[status(thm)],[12406:[bind(A,$thf( x )),bind(B,$thf( ^ [D: iS] : D )),bind(C,$thf( ^ [D: iS] : D ))]]) ).
thf(12832,plain,
~ ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[12830:[]]) ).
thf(14803,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk1 @ A ) )
| ~ $true
| ( ( A @ B )
!= ( sk3
@ ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) )
@ ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) )
@ ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[24,12832]) ).
thf(14804,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk1 @ A ) )
| ( ( A @ B )
!= ( sk3
@ ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) )
@ ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) )
@ ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) ) ) ) ),
inference(simp,[status(thm)],[14803]) ).
thf(14912,plain,
( ~ ( sk3 @ c0 @ c0 @ c0 )
| ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) ),
inference(pre_uni,[status(thm)],[14804:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ C @ C ) )),bind(B,$thf( cP @ ( sk1 @ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) @ ( sk2 @ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) ))]]) ).
thf(21931,plain,
( ~ $true
| ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) ),
inference(rewrite,[status(thm)],[14912,10430]) ).
thf(21932,plain,
( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ),
inference(simp,[status(thm)],[21931]) ).
thf(21963,plain,
( ~ $true
| ( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ),
inference(paramod_ordered,[status(thm)],[21932,8]) ).
thf(21964,plain,
( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ),
inference(simp,[status(thm)],[21963]) ).
thf(22137,plain,
( ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( cP @ x @ c0 ) )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( cP @ x @ y ) )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( cP @ x @ y ) ) ),
inference(simp,[status(thm)],[21964]) ).
thf(22165,plain,
( ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( cP @ x @ c0 ) )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( cP @ x @ y ) ) ),
inference(simp,[status(thm)],[22137]) ).
thf(22023,plain,
( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0 )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( sk1 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[63,21932]) ).
thf(22120,plain,
( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0 )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[22023]) ).
thf(22308,plain,
( ( sk3 @ c0
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0 )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( sk1 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[63,22120]) ).
thf(22420,plain,
( ( sk3 @ c0
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0 )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[22308]) ).
thf(22429,plain,
( ( sk3 @ c0
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0 )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[22420]) ).
thf(94,plain,
! [C: iS,B: iS > $o,A: iS] :
( ~ ( B @ c0 )
| ~ $true
| ( B @ C )
| ( ( sk3 @ c0 @ A @ A )
!= ( B @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,19]) ).
thf(95,plain,
! [C: iS,B: iS > $o,A: iS] :
( ~ ( B @ c0 )
| ( B @ C )
| ( ( sk3 @ c0 @ A @ A )
!= ( B @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ) ) ),
inference(simp,[status(thm)],[94]) ).
thf(120,plain,
! [B: iS,A: iS] :
( ( c0 != c0 )
| ( c0 = B )
| ( ( sk3 @ c0 @ A @ A )
!= ( c0
= ( cP @ ( sk1 @ ( (=) @ iS @ c0 ) ) @ ( sk2 @ ( (=) @ iS @ c0 ) ) ) ) ) ),
inference(replace_leibeq,[status(thm)],[95:[bind(A,$thf( A )),bind(B,$thf( (=) @ iS @ c0 ))]]) ).
thf(130,plain,
! [B: iS,A: iS] :
( ( c0 != c0 )
| ( c0 = B )
| ( ( sk3 @ c0 @ A @ A )
!= ( c0
= ( cP @ ( sk1 @ ( (=) @ iS @ c0 ) ) @ ( sk2 @ ( (=) @ iS @ c0 ) ) ) ) ) ),
inference(lifteq,[status(thm)],[120]) ).
thf(157,plain,
! [B: iS,A: iS] :
( ( c0 = B )
| ( ( sk3 @ c0 @ A @ A )
!= ( c0
= ( cP @ ( sk1 @ ( (=) @ iS @ c0 ) ) @ ( sk2 @ ( (=) @ iS @ c0 ) ) ) ) ) ),
inference(simp,[status(thm)],[130]) ).
thf(8573,plain,
! [B: iS,A: iS] :
( ( c0 = B )
| ( ( sk3 @ c0 @ A @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) ) ),
inference(rewrite,[status(thm)],[157,194,63]) ).
thf(8676,plain,
! [D: iS,C: iS,B: iS,A: iS] :
( ( ( sk3 @ c0 @ A @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) )
| ( c0 != c0 )
| ( B
!= ( cP @ C @ D ) ) ),
inference(paramod_ordered,[status(thm)],[8573,27]) ).
thf(8677,plain,
! [D: iS,C: iS,B: iS,A: iS] :
( ( ( sk3 @ c0 @ A @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) )
| ( B
!= ( cP @ C @ D ) ) ),
inference(simp,[status(thm)],[8676]) ).
thf(8678,plain,
! [A: iS] :
( ( sk3 @ c0 @ A @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) ),
inference(pattern_uni,[status(thm)],[8677:[bind(A,$thf( A )),bind(B,$thf( cP @ E @ F )),bind(C,$thf( E )),bind(D,$thf( F ))]]) ).
thf(12,plain,
! [D: iS,C: iS,B: iS,A: iS] :
( ( ( cP @ A @ C )
!= ( cP @ B @ D ) )
| ( C = D ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(30,plain,
! [D: iS,C: iS,B: iS,A: iS] :
( ( ( cP @ A @ C )
!= ( cP @ B @ D ) )
| ( C = D ) ),
inference(lifteq,[status(thm)],[12]) ).
thf(31,plain,
! [D: iS,C: iS,B: iS,A: iS] :
( ( ( cP @ A @ C )
!= ( cP @ B @ D ) )
| ( C = D ) ),
inference(simp,[status(thm)],[30]) ).
thf(32,plain,
? [A: iS > iS > iS] :
! [B: iS,C: iS] :
( ( A @ B @ ( cP @ B @ C ) )
= C ),
inference(detectInverse,[status(thm)],[31]) ).
thf(33,plain,
! [B: iS,A: iS] :
( ( sk5 @ A @ ( cP @ A @ B ) )
= B ),
inference(cnf,[status(esa)],[32]) ).
thf(184,plain,
! [B: iS,A: iS] :
( ( sk5 @ A @ ( cP @ A @ B ) )
= B ),
inference(lifteq,[status(thm)],[33]) ).
thf(140,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ~ ( sk3 @ c0 @ ( B @ c0 ) @ ( C @ c0 ) )
| ( sk3 @ c0 @ ( B @ A ) @ ( C @ A ) )
| ( ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) ) ) )
!= ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[95:[bind(A,$thf( E @ ( cP @ ( sk1 @ ^ [F: iS] : ( sk3 @ c0 @ ( E @ F ) @ ( F @ F ) ) ) @ ( sk2 @ ^ [F: iS] : ( sk3 @ c0 @ ( E @ F ) @ ( F @ F ) ) ) ) )),bind(B,$thf( ^ [F: iS] : ( sk3 @ c0 @ ( E @ F ) @ ( F @ F ) ) )),bind(C,$thf( C ))]]) ).
thf(141,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ( sk3 @ c0 @ ( B @ A ) @ ( C @ A ) )
| ~ ( sk3 @ c0 @ ( B @ c0 ) @ ( C @ c0 ) )
| ( ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) ) ) )
!= ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[140:[]]) ).
thf(164,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ( sk3 @ c0 @ ( B @ A ) @ ( C @ A ) )
| ~ ( sk3 @ c0 @ ( B @ c0 ) @ ( C @ c0 ) )
| ( ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) ) ) )
!= ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) ) ) ) ) ),
inference(simp,[status(thm)],[141]) ).
thf(12309,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ~ ( sk3
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) )
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) ) )
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) ) ) )
| ( ( B @ c0 )
!= ( C @ c0 ) )
| ~ $true
| ( ( sk3 @ A @ ( B @ A ) @ ( C @ A ) )
!= ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ),
inference(paramod_ordered,[status(thm)],[161,8]) ).
thf(12310,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ~ ( sk3
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) )
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) ) )
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ D @ ( B @ D ) @ ( C @ D ) ) ) ) ) )
| ( ( B @ c0 )
!= ( C @ c0 ) )
| ( ( sk3 @ A @ ( B @ A ) @ ( C @ A ) )
!= ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ),
inference(simp,[status(thm)],[12309]) ).
thf(12672,plain,
( ~ ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) )
@ ( cP @ x @ y )
@ ( cP @ x @ y ) )
| ( ( cP @ x @ y )
!= ( cP @ x @ y ) ) ),
inference(pre_uni,[status(thm)],[12310:[bind(A,$thf( cP @ x @ c0 )),bind(B,$thf( ^ [D: iS] : ( cP @ x @ y ) )),bind(C,$thf( ^ [D: iS] : ( cP @ x @ y ) ))]]) ).
thf(12673,plain,
~ ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) )
@ ( cP @ x @ y )
@ ( cP @ x @ y ) ),
inference(pattern_uni,[status(thm)],[12672:[]]) ).
thf(15944,plain,
! [A: iS] :
( ~ $true
| ( ( sk3 @ c0 @ A @ A )
!= ( sk3
@ ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) )
@ ( cP @ x @ y )
@ ( cP @ x @ y ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,12673]) ).
thf(15945,plain,
! [A: iS] :
( ( sk3 @ c0 @ A @ A )
!= ( sk3
@ ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) )
@ ( cP @ x @ y )
@ ( cP @ x @ y ) ) ),
inference(simp,[status(thm)],[15944]) ).
thf(16122,plain,
! [A: iS] :
( ( ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) )
!= c0 )
| ( A
!= ( cP @ x @ y ) )
| ( A
!= ( cP @ x @ y ) ) ),
inference(simp,[status(thm)],[15945]) ).
thf(16141,plain,
( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) )
!= c0 ),
inference(simp,[status(thm)],[16122]) ).
thf(2053,plain,
( ~ $true
| ( ( sk3 @ x
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
@ x )
!= ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ) ),
inference(paramod_ordered,[status(thm)],[1063,2042]) ).
thf(2054,plain,
( ( sk3 @ x
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
@ x )
!= ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ),
inference(simp,[status(thm)],[2053]) ).
thf(2082,plain,
( ( x != x )
| ( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
| ( x != x ) ),
inference(simp,[status(thm)],[2054]) ).
thf(2093,plain,
( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) ),
inference(simp,[status(thm)],[2082]) ).
thf(14837,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk2 @ A ) )
| ~ $true
| ( ( A @ B )
!= ( sk3
@ ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) )
@ ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) )
@ ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[34,12832]) ).
thf(14838,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk2 @ A ) )
| ( ( A @ B )
!= ( sk3
@ ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) )
@ ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) )
@ ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) ) ) ) ),
inference(simp,[status(thm)],[14837]) ).
thf(14924,plain,
( ~ ( sk3 @ c0 @ c0 @ c0 )
| ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) ),
inference(pre_uni,[status(thm)],[14838:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ C @ C ) )),bind(B,$thf( cP @ ( sk1 @ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) @ ( sk2 @ ^ [C: iS] : ( sk3 @ C @ C @ C ) ) ))]]) ).
thf(27241,plain,
( ~ $true
| ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) ),
inference(rewrite,[status(thm)],[14924,10430]) ).
thf(27242,plain,
( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ),
inference(simp,[status(thm)],[27241]) ).
thf(27268,plain,
( ~ $true
| ( ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) )
!= ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[27242,12832]) ).
thf(27269,plain,
( ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) )
!= ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) ),
inference(simp,[status(thm)],[27268]) ).
thf(27451,plain,
( ( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) ),
inference(simp,[status(thm)],[27269]) ).
thf(27479,plain,
( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ),
inference(simp,[status(thm)],[27451]) ).
thf(953,plain,
( ~ ( sk3 @ c0 @ x @ x )
| ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ) ),
inference(pre_uni,[status(thm)],[800:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ x @ x ) )),bind(B,$thf( x ))]]) ).
thf(1518,plain,
( ~ $true
| ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ) ),
inference(rewrite,[status(thm)],[953,42]) ).
thf(1519,plain,
( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ),
inference(simp,[status(thm)],[1518]) ).
thf(12827,plain,
( ~ ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
@ x
@ x )
| ( x != x ) ),
inference(pre_uni,[status(thm)],[12406:[bind(A,$thf( x )),bind(B,$thf( ^ [D: iS] : x )),bind(C,$thf( ^ [D: iS] : x ))]]) ).
thf(12831,plain,
~ ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
@ x
@ x ),
inference(pattern_uni,[status(thm)],[12827:[]]) ).
thf(13075,plain,
( ~ $true
| ( ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
@ x
@ x )
!= ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ) ) ),
inference(paramod_ordered,[status(thm)],[1519,12831]) ).
thf(13076,plain,
( ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
@ x
@ x )
!= ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ) ),
inference(simp,[status(thm)],[13075]) ).
thf(13165,plain,
( ( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
| ( x != x )
| ( x != x ) ),
inference(simp,[status(thm)],[13076]) ).
thf(13186,plain,
( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) ),
inference(simp,[status(thm)],[13165]) ).
thf(135,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ~ ( sk3 @ c0
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) ) ) )
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) ) ) ) )
| ( sk3 @ c0 @ ( B @ A ) @ ( C @ A ) )
| ( ( B @ c0 )
!= ( C @ c0 ) ) ),
inference(pre_uni,[status(thm)],[93:[bind(A,$thf( E @ c0 )),bind(B,$thf( ^ [F: iS] : ( sk3 @ c0 @ ( E @ F ) @ ( F @ F ) ) )),bind(C,$thf( C ))]]) ).
thf(137,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ( sk3 @ c0 @ ( B @ A ) @ ( C @ A ) )
| ~ ( sk3 @ c0
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) ) ) )
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) ) ) ) )
| ( ( B @ c0 )
!= ( C @ c0 ) ) ),
inference(pre_uni,[status(thm)],[135:[]]) ).
thf(160,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ( sk3 @ c0 @ ( B @ A ) @ ( C @ A ) )
| ~ ( sk3 @ c0
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) ) ) )
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ c0 @ ( B @ D ) @ ( C @ D ) ) ) ) ) )
| ( ( B @ c0 )
!= ( C @ c0 ) ) ),
inference(simp,[status(thm)],[137]) ).
thf(14,plain,
! [D: iS,C: iS,B: iS,A: iS] :
( ( ( cP @ A @ C )
!= ( cP @ B @ D ) )
| ( A = B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(20,plain,
! [D: iS,C: iS,B: iS,A: iS] :
( ( ( cP @ A @ C )
!= ( cP @ B @ D ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[14]) ).
thf(21,plain,
! [D: iS,C: iS,B: iS,A: iS] :
( ( ( cP @ A @ C )
!= ( cP @ B @ D ) )
| ( A = B ) ),
inference(simp,[status(thm)],[20]) ).
thf(142,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ~ ( sk3
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) ) ) )
@ c0
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) ) ) ) )
| ( sk3 @ ( B @ A ) @ c0 @ ( C @ A ) )
| ( ( B @ c0 )
!= ( C @ c0 ) ) ),
inference(pre_uni,[status(thm)],[99:[bind(A,$thf( D @ c0 )),bind(B,$thf( ^ [F: iS] : ( sk3 @ ( D @ F ) @ c0 @ ( F @ F ) ) )),bind(C,$thf( C ))]]) ).
thf(144,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ( sk3 @ ( B @ A ) @ c0 @ ( C @ A ) )
| ~ ( sk3
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) ) ) )
@ c0
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) ) ) ) )
| ( ( B @ c0 )
!= ( C @ c0 ) ) ),
inference(pre_uni,[status(thm)],[142:[]]) ).
thf(165,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ( sk3 @ ( B @ A ) @ c0 @ ( C @ A ) )
| ~ ( sk3
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) ) ) )
@ c0
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ c0 @ ( C @ D ) ) ) ) ) )
| ( ( B @ c0 )
!= ( C @ c0 ) ) ),
inference(simp,[status(thm)],[144]) ).
thf(954,plain,
( ~ ( sk3 @ c0 @ c0 @ x )
| ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
@ x ) ),
inference(pre_uni,[status(thm)],[800:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ C @ x ) )),bind(B,$thf( x ))]]) ).
thf(3873,plain,
( ~ ( sk3 @ c0 @ c0 @ x )
| ~ $true
| ( ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
@ x )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[954,648]) ).
thf(3874,plain,
( ~ ( sk3 @ c0 @ c0 @ x )
| ( ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
@ x )
!= ( sk3 @ x @ x @ x ) ) ),
inference(simp,[status(thm)],[3873]) ).
thf(3956,plain,
( ~ ( sk3 @ c0 @ c0 @ x )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
!= x )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
!= x )
| ( x != x ) ),
inference(simp,[status(thm)],[3874]) ).
thf(3980,plain,
( ~ ( sk3 @ c0 @ c0 @ x )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
!= x ) ),
inference(simp,[status(thm)],[3956]) ).
thf(685,plain,
( ~ $true
| ( ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) )
!= ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ) ),
inference(paramod_ordered,[status(thm)],[683,8]) ).
thf(686,plain,
( ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) )
!= ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ),
inference(simp,[status(thm)],[685]) ).
thf(710,plain,
( ( ( cP @ x @ c0 )
!= x )
| ( ( cP @ x @ y )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
| ( ( cP @ x @ y )
!= x ) ),
inference(simp,[status(thm)],[686]) ).
thf(7494,plain,
( ~ $true
| ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x ) ) ),
inference(paramod_ordered,[status(thm)],[1063,7476]) ).
thf(7495,plain,
( ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x ) ) ),
inference(simp,[status(thm)],[7494]) ).
thf(7545,plain,
( ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) )
| ( x != x )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( cP @ c0 @ c0 ) )
| ( x != x ) ),
inference(simp,[status(thm)],[7495]) ).
thf(7593,plain,
( ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( cP @ c0 @ c0 ) ) ),
inference(simp,[status(thm)],[7545]) ).
thf(112,plain,
! [B: iS > $o,A: iS] :
( ~ ~ ( B @ c0 )
| ~ ~ ( B
@ ( cP
@ ( sk1
@ ^ [C: iS] :
~ ( B @ C ) )
@ ( sk2
@ ^ [C: iS] :
~ ( B @ C ) ) ) )
| ~ ( B @ A ) ),
inference(prim_subst,[status(thm)],[19:[bind(A,$thf( ^ [D: iS] : ~ ( C @ D ) ))]]) ).
thf(168,plain,
! [B: iS > $o,A: iS] :
( ( B @ c0 )
| ( B
@ ( cP
@ ( sk1
@ ^ [C: iS] :
~ ( B @ C ) )
@ ( sk2
@ ^ [C: iS] :
~ ( B @ C ) ) ) )
| ~ ( B @ A ) ),
inference(cnf,[status(esa)],[112]) ).
thf(169,plain,
! [B: iS > $o,A: iS] :
( ( B @ c0 )
| ( B
@ ( cP
@ ( sk1
@ ^ [C: iS] :
~ ( B @ C ) )
@ ( sk2
@ ^ [C: iS] :
~ ( B @ C ) ) ) )
| ~ ( B @ A ) ),
inference(simp,[status(thm)],[168]) ).
thf(1070,plain,
( ~ $true
| ( ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[1063,648]) ).
thf(1071,plain,
( ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ x @ x ) ),
inference(simp,[status(thm)],[1070]) ).
thf(1095,plain,
( ( x != x )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= x )
| ( x != x ) ),
inference(simp,[status(thm)],[1071]) ).
thf(1099,plain,
( ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= x ),
inference(simp,[status(thm)],[1095]) ).
thf(14799,plain,
! [A: iS] :
( ~ $true
| ( ( sk3 @ c0 @ A @ A )
!= ( sk3
@ ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) ) )
@ ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) ) )
@ ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,12832]) ).
thf(14800,plain,
! [A: iS] :
( ( sk3 @ c0 @ A @ A )
!= ( sk3
@ ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) ) )
@ ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) ) )
@ ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) ) ) ) ),
inference(simp,[status(thm)],[14799]) ).
thf(14921,plain,
! [A: iS] :
( ( ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) ) )
!= c0 )
| ( A
!= ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) ) ) )
| ( A
!= ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) ) ) ) ),
inference(simp,[status(thm)],[14800]) ).
thf(14950,plain,
( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= c0 ),
inference(simp,[status(thm)],[14921]) ).
thf(1046,plain,
( ( ( cP @ x @ y )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
| ( ( cP @ x @ y )
!= x )
| ( ( cP @ x @ c0 )
!= ( cP @ x @ y ) )
| ( x != x ) ),
inference(eqfactor_ordered,[status(thm)],[710]) ).
thf(1049,plain,
( ( ( cP @ x @ y )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
| ( ( cP @ x @ y )
!= x )
| ( x != x )
| ( c0 != y ) ),
inference(simp,[status(thm)],[1046]) ).
thf(1050,plain,
( ( ( cP @ x @ y )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
| ( ( cP @ x @ y )
!= x )
| ( c0 != y ) ),
inference(simp,[status(thm)],[1049]) ).
thf(104,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ~ $true
| ~ ( C @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) )
| ( C @ D )
| ( ( A @ B )
!= ( C @ c0 ) ) ),
inference(paramod_ordered,[status(thm)],[19,19]) ).
thf(105,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ~ ( C @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) )
| ( C @ D )
| ( ( A @ B )
!= ( C @ c0 ) ) ),
inference(simp,[status(thm)],[104]) ).
thf(119,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) )
!= ( cP @ ( sk1 @ ( (=) @ iS @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) ) ) @ ( sk2 @ ( (=) @ iS @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) ) ) ) )
| ( ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) )
= D )
| ( ( A @ B )
!= ( ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) )
= c0 ) ) ),
inference(replace_leibeq,[status(thm)],[105:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( (=) @ iS @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) ))]]) ).
thf(129,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ( ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) )
!= ( cP @ ( sk1 @ ( (=) @ iS @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) ) ) @ ( sk2 @ ( (=) @ iS @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) ) ) ) )
| ( ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) )
= D )
| ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( ( A @ B )
!= ( ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) )
= c0 ) ) ),
inference(lifteq,[status(thm)],[119]) ).
thf(1526,plain,
( ~ $true
| ( ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[1519,648]) ).
thf(1527,plain,
( ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x )
!= ( sk3 @ x @ x @ x ) ),
inference(simp,[status(thm)],[1526]) ).
thf(1557,plain,
( ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
!= x )
| ( x != x )
| ( x != x ) ),
inference(simp,[status(thm)],[1527]) ).
thf(1563,plain,
( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
!= x ),
inference(simp,[status(thm)],[1557]) ).
thf(734,plain,
( ~ $true
| ( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[728,648]) ).
thf(735,plain,
( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x )
!= ( sk3 @ x @ x @ x ) ),
inference(simp,[status(thm)],[734]) ).
thf(758,plain,
( ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
!= x )
| ( x != x )
| ( x != x ) ),
inference(simp,[status(thm)],[735]) ).
thf(765,plain,
( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
!= x ),
inference(simp,[status(thm)],[758]) ).
thf(9526,plain,
! [B: iS,A: iS] :
( ( c0
!= ( cP @ c0 @ c0 ) )
| ( ( sk3 @ c0 @ A @ A )
!= ( sk3 @ c0 @ B @ B ) ) ),
inference(paramod_ordered,[status(thm)],[42,8678]) ).
thf(9527,plain,
( c0
!= ( cP @ c0 @ c0 ) ),
inference(pattern_uni,[status(thm)],[9526:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(9562,plain,
( ( cP @ c0 @ c0 )
!= c0 ),
inference(lifteq,[status(thm)],[9527]) ).
thf(143,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ~ ( sk3
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) ) ) )
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) ) )
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) ) ) ) )
| ( sk3 @ ( B @ A ) @ A @ ( C @ A ) )
| ( ( B @ c0 )
!= ( C @ c0 ) ) ),
inference(pre_uni,[status(thm)],[99:[bind(A,$thf( D @ c0 )),bind(B,$thf( ^ [F: iS] : ( sk3 @ ( D @ F ) @ F @ ( F @ F ) ) )),bind(C,$thf( C ))]]) ).
thf(145,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ( sk3 @ ( B @ A ) @ A @ ( C @ A ) )
| ~ ( sk3
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) ) ) )
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) ) )
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) ) ) ) )
| ( ( B @ c0 )
!= ( C @ c0 ) ) ),
inference(pre_uni,[status(thm)],[143:[]]) ).
thf(166,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ( sk3 @ ( B @ A ) @ A @ ( C @ A ) )
| ~ ( sk3
@ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) ) ) )
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) ) )
@ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] : ( sk3 @ ( B @ D ) @ D @ ( C @ D ) ) ) ) ) )
| ( ( B @ c0 )
!= ( C @ c0 ) ) ),
inference(simp,[status(thm)],[145]) ).
thf(115,plain,
! [C: iS > $o,B: iS > $o,A: iS] :
( ~ ( ( B @ c0 )
| ( C @ c0 ) )
| ~ ( ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) ) ) )
| ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) ) ) ) )
| ( B @ A )
| ( C @ A ) ),
inference(prim_subst,[status(thm)],[19:[bind(A,$thf( ^ [E: iS] : ( ( C @ E ) | ( D @ E ) ) ))]]) ).
thf(170,plain,
! [C: iS > $o,B: iS > $o,A: iS] :
( ( ~ ( B @ c0 )
| ~ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) ) ) )
| ( B @ A )
| ( C @ A ) )
& ( ~ ( B @ c0 )
| ~ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) ) ) )
| ( B @ A )
| ( C @ A ) )
& ( ~ ( C @ c0 )
| ~ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) ) ) )
| ( B @ A )
| ( C @ A ) )
& ( ~ ( C @ c0 )
| ~ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) ) ) )
| ( B @ A )
| ( C @ A ) ) ),
inference(cnf,[status(esa)],[115]) ).
thf(172,plain,
! [C: iS > $o,B: iS > $o,A: iS] :
( ~ ( B @ c0 )
| ~ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) ) ) )
| ( B @ A )
| ( C @ A ) ),
inference(cnfConj,[status(thm)],[170]) ).
thf(176,plain,
! [C: iS > $o,B: iS > $o,A: iS] :
( ~ ( B @ c0 )
| ~ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) ) ) )
| ( B @ A )
| ( C @ A ) ),
inference(simp,[status(thm)],[172]) ).
thf(22019,plain,
( ~ $true
| ( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[21932,648]) ).
thf(22020,plain,
( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk3 @ x @ x @ x ) ),
inference(simp,[status(thm)],[22019]) ).
thf(22123,plain,
( ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= x )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= x )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= x ) ),
inference(simp,[status(thm)],[22020]) ).
thf(22155,plain,
( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= x ),
inference(simp,[status(thm)],[22123]) ).
thf(27150,plain,
( ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( cP @ x @ y ) )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( cP @ x @ c0 )
!= ( cP @ x @ y ) ) ),
inference(eqfactor_ordered,[status(thm)],[22165]) ).
thf(27165,plain,
( ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( cP @ x @ y ) )
| ( x != x )
| ( c0 != y ) ),
inference(simp,[status(thm)],[27150]) ).
thf(27181,plain,
( ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( cP @ x @ y ) )
| ( c0 != y ) ),
inference(simp,[status(thm)],[27165]) ).
thf(45,plain,
! [A: iS] :
( ~ $true
| ( ( sk3 @ c0 @ A @ A )
!= ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,8]) ).
thf(46,plain,
! [A: iS] :
( ( sk3 @ c0 @ A @ A )
!= ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ),
inference(simp,[status(thm)],[45]) ).
thf(48,plain,
! [A: iS] :
( ( ( cP @ x @ c0 )
!= c0 )
| ( A
!= ( cP @ x @ y ) )
| ( A
!= ( cP @ x @ y ) ) ),
inference(simp,[status(thm)],[46]) ).
thf(49,plain,
( ( cP @ x @ c0 )
!= c0 ),
inference(simp,[status(thm)],[48]) ).
thf(1066,plain,
( ~ $true
| ( ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) )
!= ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ) ),
inference(paramod_ordered,[status(thm)],[1063,8]) ).
thf(1067,plain,
( ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) )
!= ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ),
inference(simp,[status(thm)],[1066]) ).
thf(1092,plain,
( ( ( cP @ x @ c0 )
!= x )
| ( ( cP @ x @ y )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
| ( ( cP @ x @ y )
!= x ) ),
inference(simp,[status(thm)],[1067]) ).
thf(116,plain,
! [B: iS,A: iS] :
( ( c0 != c0 )
| ( c0 = B )
| ( ( sk3 @ A @ c0 @ A )
!= ( c0
= ( cP @ ( sk1 @ ( (=) @ iS @ c0 ) ) @ ( sk2 @ ( (=) @ iS @ c0 ) ) ) ) ) ),
inference(replace_leibeq,[status(thm)],[101:[bind(A,$thf( A )),bind(B,$thf( (=) @ iS @ c0 ))]]) ).
thf(125,plain,
! [B: iS,A: iS] :
( ( c0 != c0 )
| ( c0 = B )
| ( ( sk3 @ A @ c0 @ A )
!= ( c0
= ( cP @ ( sk1 @ ( (=) @ iS @ c0 ) ) @ ( sk2 @ ( (=) @ iS @ c0 ) ) ) ) ) ),
inference(lifteq,[status(thm)],[116]) ).
thf(179,plain,
! [B: iS,A: iS] :
( ( c0 = B )
| ( ( sk3 @ A @ c0 @ A )
!= ( c0
= ( cP @ ( sk1 @ ( (=) @ iS @ c0 ) ) @ ( sk2 @ ( (=) @ iS @ c0 ) ) ) ) ) ),
inference(simp,[status(thm)],[125]) ).
thf(25001,plain,
! [B: iS,A: iS] :
( ( c0 = B )
| ( ( sk3 @ A @ c0 @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) ) ),
inference(rewrite,[status(thm)],[179,194,63]) ).
thf(25275,plain,
! [B: iS,A: iS] :
( ( ( sk3 @ A @ c0 @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) )
| ( c0 != c0 )
| ( B
!= ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[25001,16141]) ).
thf(25276,plain,
! [B: iS,A: iS] :
( ( ( sk3 @ A @ c0 @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) )
| ( B
!= ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ) ) ),
inference(simp,[status(thm)],[25275]) ).
thf(25277,plain,
! [A: iS] :
( ( sk3 @ A @ c0 @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) ),
inference(pattern_uni,[status(thm)],[25276:[bind(A,$thf( A )),bind(B,$thf( cP @ ( sk1 @ ^ [C: iS] : ( sk3 @ C @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) @ ( sk2 @ ^ [C: iS] : ( sk3 @ C @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ))]]) ).
thf(21978,plain,
( ~ $true
| ( ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) )
!= ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[21932,12832]) ).
thf(21979,plain,
( ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) )
!= ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) ),
inference(simp,[status(thm)],[21978]) ).
thf(22124,plain,
( ( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ) ),
inference(simp,[status(thm)],[21979]) ).
thf(22156,plain,
( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) ),
inference(simp,[status(thm)],[22124]) ).
thf(22202,plain,
( ( ( cP @ c0
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( sk1 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[63,22156]) ).
thf(22212,plain,
( ( ( cP @ c0
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[22202]) ).
thf(106,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ~ ( C @ c0 )
| ~ $true
| ( C @ D )
| ( ( A @ B )
!= ( C @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,19]) ).
thf(107,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ~ ( C @ c0 )
| ( C @ D )
| ( ( A @ B )
!= ( C @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) ) ) ),
inference(simp,[status(thm)],[106]) ).
thf(154,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ~ ( C @ c0 )
| ( C @ D )
| ( ( A @ B )
!= ( C @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) ) ) ),
inference(pre_uni,[status(thm)],[107:[]]) ).
thf(155,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ( C @ D )
| ~ ( C @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ~ ( A @ c0 )
| ( ( A @ B )
!= ( C @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) ) ) ),
inference(pre_uni,[status(thm)],[154:[]]) ).
thf(22309,plain,
( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0
@ c0 )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( sk1 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[63,22120]) ).
thf(22410,plain,
( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0
@ c0 )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[22309]) ).
thf(22427,plain,
( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0
@ c0 )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[22410]) ).
thf(10605,plain,
! [A: iS] :
( ( sk3 @ c0
@ ( sk1
@ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) )
@ c0 )
| ( sk3 @ c0 @ A @ c0 ) ),
inference(pre_uni,[status(thm)],[10478:[bind(A,$thf( ^ [C: iS] : ( sk3 @ c0 @ C @ c0 ) )),bind(B,$thf( B ))]]) ).
thf(10704,plain,
! [A: iS] :
( ( sk3 @ c0
@ ( sk1
@ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) )
@ c0 )
| ( sk3 @ c0 @ A @ c0 ) ),
inference(simp,[status(thm)],[10605]) ).
thf(10959,plain,
! [A: iS] :
( ( sk3 @ c0
@ ( sk1
@ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) )
@ c0 )
| ( ( sk3 @ c0 @ A @ c0 )
!= ( sk3 @ c0
@ ( sk1
@ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) )
@ c0 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[10704]) ).
thf(11012,plain,
( sk3 @ c0
@ ( sk1
@ ^ [A: iS] : ( sk3 @ c0 @ A @ c0 ) )
@ c0 ),
inference(pattern_uni,[status(thm)],[10959:[bind(A,$thf( sk1 @ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) ))]]) ).
thf(22201,plain,
( ( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0 )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( sk2 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[194,22156]) ).
thf(22211,plain,
( ( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0 )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[22201]) ).
thf(26924,plain,
( ( ( cP @ c0 @ c0 )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( sk1 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[63,22211]) ).
thf(26943,plain,
( ( ( cP @ c0 @ c0 )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[26924]) ).
thf(26953,plain,
( ( ( cP @ c0 @ c0 )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[26943]) ).
thf(149,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ~ ( C @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) )
| ( C @ D )
| ( ( A @ B )
!= ( C @ c0 ) ) ),
inference(pre_uni,[status(thm)],[105:[]]) ).
thf(150,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ( C @ D )
| ~ ( C @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ~ ( A @ c0 )
| ( ( A @ B )
!= ( C @ c0 ) ) ),
inference(pre_uni,[status(thm)],[149:[]]) ).
thf(689,plain,
( ~ $true
| ( ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[683,648]) ).
thf(690,plain,
( ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ x @ x ) ),
inference(simp,[status(thm)],[689]) ).
thf(713,plain,
( ( x != x )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= x )
| ( x != x ) ),
inference(simp,[status(thm)],[690]) ).
thf(717,plain,
( ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= x ),
inference(simp,[status(thm)],[713]) ).
thf(27325,plain,
( ~ $true
| ( ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[27242,648]) ).
thf(27326,plain,
( ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk3 @ x @ x @ x ) ),
inference(simp,[status(thm)],[27325]) ).
thf(27457,plain,
( ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= x )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= x )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= x ) ),
inference(simp,[status(thm)],[27326]) ).
thf(27481,plain,
( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= x ),
inference(simp,[status(thm)],[27457]) ).
thf(673,plain,
( ~ ( sk3 @ c0 @ c0 @ x )
| ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
@ x ) ),
inference(pre_uni,[status(thm)],[654:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ C @ x ) )),bind(B,$thf( x ))]]) ).
thf(2064,plain,
! [A: iS] :
( ~ $true
| ( ( sk3 @ A @ c0 @ A )
!= ( sk3 @ x
@ ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ x @ B @ x ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ x @ B @ x ) ) )
@ x ) ) ),
inference(paramod_ordered,[status(thm)],[40,2042]) ).
thf(2065,plain,
! [A: iS] :
( ( sk3 @ A @ c0 @ A )
!= ( sk3 @ x
@ ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ x @ B @ x ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ x @ B @ x ) ) )
@ x ) ),
inference(simp,[status(thm)],[2064]) ).
thf(2081,plain,
! [A: iS] :
( ( A != x )
| ( ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ x @ B @ x ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ x @ B @ x ) ) )
!= c0 )
| ( A != x ) ),
inference(simp,[status(thm)],[2065]) ).
thf(2092,plain,
( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
!= c0 ),
inference(simp,[status(thm)],[2081]) ).
thf(173,plain,
! [C: iS > $o,B: iS > $o,A: iS] :
( ~ ( C @ c0 )
| ~ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) ) ) )
| ( B @ A )
| ( C @ A ) ),
inference(cnfConj,[status(thm)],[170]) ).
thf(177,plain,
! [C: iS > $o,B: iS > $o,A: iS] :
( ~ ( C @ c0 )
| ~ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) ) ) )
| ( B @ A )
| ( C @ A ) ),
inference(simp,[status(thm)],[173]) ).
thf(2835,plain,
( ~ ( sk3 @ c0 @ c0 @ x )
| ~ $true
| ( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
@ x )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[673,648]) ).
thf(2836,plain,
( ~ ( sk3 @ c0 @ c0 @ x )
| ( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
@ x )
!= ( sk3 @ x @ x @ x ) ) ),
inference(simp,[status(thm)],[2835]) ).
thf(2875,plain,
( ~ ( sk3 @ c0 @ c0 @ x )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
!= x )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
!= x )
| ( x != x ) ),
inference(simp,[status(thm)],[2836]) ).
thf(2920,plain,
( ~ ( sk3 @ c0 @ c0 @ x )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
!= x ) ),
inference(simp,[status(thm)],[2875]) ).
thf(7492,plain,
( ~ $true
| ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x ) ) ),
inference(paramod_ordered,[status(thm)],[683,7476]) ).
thf(7493,plain,
( ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x ) ) ),
inference(simp,[status(thm)],[7492]) ).
thf(7577,plain,
( ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) )
| ( x != x )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( cP @ c0 @ c0 ) )
| ( x != x ) ),
inference(simp,[status(thm)],[7493]) ).
thf(7585,plain,
( ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( cP @ c0 @ c0 ) ) ),
inference(simp,[status(thm)],[7577]) ).
thf(13069,plain,
! [A: iS] :
( ~ $true
| ( ( sk3 @ c0 @ A @ A )
!= ( sk3
@ ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ x @ x ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ x @ x ) ) )
@ x
@ x ) ) ),
inference(paramod_ordered,[status(thm)],[42,12831]) ).
thf(13070,plain,
! [A: iS] :
( ( sk3 @ c0 @ A @ A )
!= ( sk3
@ ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ x @ x ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ x @ x ) ) )
@ x
@ x ) ),
inference(simp,[status(thm)],[13069]) ).
thf(13142,plain,
! [A: iS] :
( ( ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ x @ x ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ x @ x ) ) )
!= c0 )
| ( A != x )
| ( A != x ) ),
inference(simp,[status(thm)],[13070]) ).
thf(13175,plain,
( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
!= c0 ),
inference(simp,[status(thm)],[13142]) ).
thf(171,plain,
! [C: iS > $o,B: iS > $o,A: iS] :
( ~ ( B @ c0 )
| ~ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) ) ) )
| ( B @ A )
| ( C @ A ) ),
inference(cnfConj,[status(thm)],[170]) ).
thf(175,plain,
! [C: iS > $o,B: iS > $o,A: iS] :
( ~ ( B @ c0 )
| ~ ( B
@ ( cP
@ ( sk1
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) ) ) )
| ( B @ A )
| ( C @ A ) ),
inference(simp,[status(thm)],[171]) ).
thf(13060,plain,
( ~ $true
| ( ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
@ x
@ x )
!= ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ) ) ),
inference(paramod_ordered,[status(thm)],[728,12831]) ).
thf(13061,plain,
( ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
@ x
@ x )
!= ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ) ),
inference(simp,[status(thm)],[13060]) ).
thf(13145,plain,
( ( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
| ( x != x )
| ( x != x ) ),
inference(simp,[status(thm)],[13061]) ).
thf(13178,plain,
( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) ),
inference(simp,[status(thm)],[13145]) ).
thf(1104,plain,
( ( ( cP @ x @ y )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
| ( ( cP @ x @ y )
!= x )
| ( ( cP @ x @ c0 )
!= ( cP @ x @ y ) )
| ( x != x ) ),
inference(eqfactor_ordered,[status(thm)],[1092]) ).
thf(1107,plain,
( ( ( cP @ x @ y )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
| ( ( cP @ x @ y )
!= x )
| ( x != x )
| ( c0 != y ) ),
inference(simp,[status(thm)],[1104]) ).
thf(1108,plain,
( ( ( cP @ x @ y )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
| ( ( cP @ x @ y )
!= x )
| ( c0 != y ) ),
inference(simp,[status(thm)],[1107]) ).
thf(10626,plain,
! [A: iS] :
( ( sk3
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) )
@ c0
@ c0 )
| ( sk3 @ A @ c0 @ c0 ) ),
inference(pre_uni,[status(thm)],[10445:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ c0 @ c0 ) )),bind(B,$thf( B ))]]) ).
thf(10718,plain,
! [A: iS] :
( ( sk3
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) )
@ c0
@ c0 )
| ( sk3 @ A @ c0 @ c0 ) ),
inference(simp,[status(thm)],[10626]) ).
thf(24354,plain,
! [A: iS] :
( ( sk3
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) )
@ c0
@ c0 )
| ( ( sk3 @ A @ c0 @ c0 )
!= ( sk3
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) )
@ c0
@ c0 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[10718]) ).
thf(24504,plain,
( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ c0 @ c0 ) )
@ c0
@ c0 ),
inference(pattern_uni,[status(thm)],[24354:[bind(A,$thf( sk2 @ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) ))]]) ).
thf(102,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ~ $true
| ( ( A @ B )
!= ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,8]) ).
thf(103,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( ( A @ B )
!= ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ),
inference(simp,[status(thm)],[102]) ).
thf(151,plain,
( ~ ( sk3 @ ( cP @ x @ c0 ) @ c0 @ c0 )
| ~ ( sk3 @ ( cP @ x @ c0 )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ ( cP @ x @ c0 ) @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ ( cP @ x @ c0 ) @ A @ A ) ) )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ ( cP @ x @ c0 ) @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ ( cP @ x @ c0 ) @ A @ A ) ) ) ) ),
inference(pre_uni,[status(thm)],[103:[bind(A,$thf( ^ [C: iS] : ( sk3 @ ( cP @ x @ c0 ) @ C @ C ) )),bind(B,$thf( cP @ x @ y ))]]) ).
thf(111,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( ( A @ B )
!= ( ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[19]) ).
thf(146,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( ( A @ B )
!= ( ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) ) ) ) ),
inference(simp,[status(thm)],[111]) ).
thf(22,plain,
? [A: iS > iS > iS] :
! [B: iS,C: iS] :
( ( A @ C @ ( cP @ B @ C ) )
= B ),
inference(detectInverse,[status(thm)],[21]) ).
thf(23,plain,
! [B: iS,A: iS] :
( ( sk4 @ B @ ( cP @ A @ B ) )
= A ),
inference(cnf,[status(esa)],[22]) ).
thf(183,plain,
! [B: iS,A: iS] :
( ( sk4 @ B @ ( cP @ A @ B ) )
= A ),
inference(lifteq,[status(thm)],[23]) ).
thf(117,plain,
! [C: iS,B: iS > $o,A: iS] :
( ( ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) )
!= ( cP @ ( sk1 @ ( (=) @ iS @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ) ) @ ( sk2 @ ( (=) @ iS @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ) ) ) )
| ( ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) )
= C )
| ( ( sk3 @ c0 @ A @ A )
!= ( ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) )
= c0 ) ) ),
inference(replace_leibeq,[status(thm)],[93:[bind(A,$thf( A )),bind(B,$thf( (=) @ iS @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ))]]) ).
thf(126,plain,
! [C: iS,B: iS > $o,A: iS] :
( ( ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) )
!= ( cP @ ( sk1 @ ( (=) @ iS @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ) ) @ ( sk2 @ ( (=) @ iS @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ) ) ) )
| ( ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) )
= C )
| ( ( sk3 @ c0 @ A @ A )
!= ( ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) )
= c0 ) ) ),
inference(lifteq,[status(thm)],[117]) ).
thf(1522,plain,
( ~ $true
| ( ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x )
!= ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ) ),
inference(paramod_ordered,[status(thm)],[1519,8]) ).
thf(1523,plain,
( ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x )
!= ( sk3 @ ( cP @ x @ c0 ) @ ( cP @ x @ y ) @ ( cP @ x @ y ) ) ),
inference(simp,[status(thm)],[1522]) ).
thf(1555,plain,
( ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
!= ( cP @ x @ c0 ) )
| ( ( cP @ x @ y )
!= x )
| ( ( cP @ x @ y )
!= x ) ),
inference(simp,[status(thm)],[1523]) ).
thf(1561,plain,
( ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
!= ( cP @ x @ c0 ) )
| ( ( cP @ x @ y )
!= x ) ),
inference(simp,[status(thm)],[1555]) ).
thf(2051,plain,
( ~ $true
| ( ( sk3 @ x
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
@ x )
!= ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ) ),
inference(paramod_ordered,[status(thm)],[683,2042]) ).
thf(2052,plain,
( ( sk3 @ x
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
@ x )
!= ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ),
inference(simp,[status(thm)],[2051]) ).
thf(2080,plain,
( ( x != x )
| ( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
| ( x != x ) ),
inference(simp,[status(thm)],[2052]) ).
thf(2091,plain,
( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) ),
inference(simp,[status(thm)],[2080]) ).
thf(174,plain,
! [C: iS > $o,B: iS > $o,A: iS] :
( ~ ( C @ c0 )
| ~ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) ) ) )
| ( B @ A )
| ( C @ A ) ),
inference(cnfConj,[status(thm)],[170]) ).
thf(178,plain,
! [C: iS > $o,B: iS > $o,A: iS] :
( ~ ( C @ c0 )
| ~ ( C
@ ( cP
@ ( sk1
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) )
@ ( sk2
@ ^ [D: iS] :
( ( B @ D )
| ( C @ D ) ) ) ) )
| ( B @ A )
| ( C @ A ) ),
inference(simp,[status(thm)],[174]) ).
thf(27792,plain,
$false,
inference(e,[status(thm)],[13650,147,124,1653,762,7477,683,677,17577,1063,2042,153,22165,42,24,22429,8678,184,12832,164,16141,2093,27479,12673,1519,13186,160,21,165,3980,710,7593,169,10430,1099,14950,1050,129,12831,1563,765,7476,9562,166,34,161,176,27,22155,27181,49,1092,25277,159,2079,27242,22120,22212,155,8573,22427,3,11012,648,194,26953,63,150,954,25001,717,27481,22156,31,673,2092,177,2920,7585,13175,175,22211,13178,1108,40,26,8,24504,151,21932,146,183,19,126,1561,2091,728,178]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV204^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % 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.10/0.21 % Computer : n015.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 15:24:31 UTC 2026
% 0.10/0.21 % CPUTime :
% 0.10/0.21 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.88/0.79 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.22/0.99 % [INFO] Parsing done (189ms).
% 1.22/1.00 % [INFO] Running in sequential loop mode.
% 2.01/1.41 % [INFO] eprover registered as external prover.
% 2.01/1.41 % [INFO] Scanning for conjecture ...
% 2.21/1.54 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.21/1.58 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.21/1.58 % [INFO] Problem is higher-order (TPTP THF).
% 2.21/1.59 % [INFO] Type checking passed.
% 2.21/1.59 % [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 ...
% 251.37/87.45 % External prover 'e' found a proof!
% 251.37/87.45 % [INFO] Killing All external provers ...
% 251.37/87.46 % Time passed: 87103ms (effective reasoning time: 86451ms)
% 251.37/87.46 % 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)>
% 251.37/87.46 % Axioms used in derivation (0):
% 251.37/87.46 % No. of inferences in proof: 349
% 251.37/87.46 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 87103 ms resp. 86451 ms w/o parsing
% 243.85/87.59 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 243.85/87.59 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------