%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEV199^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n008.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:36:59 AM UTC 2026
% Result : Theorem 270.24s 99.09s
% Output : Refutation 270.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 6
% Syntax : Number of formulae : 350 ( 83 unt; 0 typ; 5 def)
% Number of atoms : 1598 ( 681 equ; 119 cnn)
% Maximal formula atoms : 18 ( 4 avg)
% Number of connectives : 6503 ( 689 ~; 608 |; 66 &;5112 @)
% ( 0 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 8 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 172 ( 172 >; 0 *; 0 +; 0 <<)
% Number of symbols : 13 ( 9 usr; 6 con; 0-3 aty)
% Number of variables : 1115 ( 569 ^; 507 !; 34 ?;1115 :)
% ( 0 !>; 0 ?*; 0 @-; 5 @+)
% Comments :
%------------------------------------------------------------------------------
thf(iS_type,type,
iS: $tType ).
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 @ x @ x @ x ) ) ) ) ).
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 @ x @ x @ x ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cS_INCL_LEM3_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 @ x @ x @ x ) ) ),
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 @ x @ x @ x ) ) ),
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 @ x @ x @ x ) ) ),
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 @ x @ x @ x ) ),
inference(cnf,[status(esa)],[4]) ).
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(8,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk2 @ A ) )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(40,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk2 @ A ) )
| ( A @ B ) ),
inference(simp,[status(thm)],[8]) ).
thf(13,plain,
~ ( sk3 @ x @ x @ x ),
inference(cnfConj,[status(thm)],[5]) ).
thf(461,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk2 @ A ) )
| ~ $true
| ( ( A @ B )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[40,13]) ).
thf(462,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk2 @ A ) )
| ( ( A @ B )
!= ( sk3 @ x @ x @ x ) ) ),
inference(simp,[status(thm)],[461]) ).
thf(578,plain,
( ~ ( sk3 @ c0 @ x @ x )
| ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ) ),
inference(pre_uni,[status(thm)],[462:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ x @ x ) )),bind(B,$thf( x ))]]) ).
thf(12,plain,
! [C: iS,B: iS,A: iS] :
( ( A != c0 )
| ( B != C )
| ( sk3 @ A @ B @ C ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(29,plain,
! [C: iS,B: iS,A: iS] :
( ( A != c0 )
| ( B != C )
| ( sk3 @ A @ B @ C ) ),
inference(lifteq,[status(thm)],[12]) ).
thf(30,plain,
! [A: iS] : ( sk3 @ c0 @ A @ A ),
inference(simp,[status(thm)],[29]) ).
thf(3871,plain,
( ~ $true
| ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ) ),
inference(rewrite,[status(thm)],[578,30]) ).
thf(3872,plain,
( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ),
inference(simp,[status(thm)],[3871]) ).
thf(11,plain,
! [D: iS,C: iS,B: iS,A: iS] :
( ( ( cP @ A @ C )
!= ( cP @ B @ D ) )
| ( C = D ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(36,plain,
! [D: iS,C: iS,B: iS,A: iS] :
( ( ( cP @ A @ C )
!= ( cP @ B @ D ) )
| ( C = D ) ),
inference(lifteq,[status(thm)],[11]) ).
thf(37,plain,
! [D: iS,C: iS,B: iS,A: iS] :
( ( ( cP @ A @ C )
!= ( cP @ B @ D ) )
| ( C = D ) ),
inference(simp,[status(thm)],[36]) ).
thf(38,plain,
? [A: iS > iS > iS] :
! [B: iS,C: iS] :
( ( A @ B @ ( cP @ B @ C ) )
= C ),
inference(detectInverse,[status(thm)],[37]) ).
thf(39,plain,
! [B: iS,A: iS] :
( ( sk5 @ A @ ( cP @ A @ B ) )
= B ),
inference(cnf,[status(esa)],[38]) ).
thf(336,plain,
! [B: iS,A: iS] :
( ( sk5 @ A @ ( cP @ A @ B ) )
= B ),
inference(lifteq,[status(thm)],[39]) ).
thf(10,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk1 @ A ) )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(19,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk1 @ A ) )
| ( A @ B ) ),
inference(simp,[status(thm)],[10]) ).
thf(205,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk1 @ A ) )
| ~ $true
| ( ( A @ B )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[19,13]) ).
thf(206,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk1 @ A ) )
| ( ( A @ B )
!= ( sk3 @ x @ x @ x ) ) ),
inference(simp,[status(thm)],[205]) ).
thf(270,plain,
( ~ ( sk3 @ x @ c0 @ x )
| ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ),
inference(pre_uni,[status(thm)],[206:[bind(A,$thf( ^ [C: iS] : ( sk3 @ x @ C @ x ) )),bind(B,$thf( x ))]]) ).
thf(6,plain,
! [C: iS,B: iS,A: iS] :
( ( B != c0 )
| ( A != C )
| ( sk3 @ A @ B @ C ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(24,plain,
! [C: iS,B: iS,A: iS] :
( ( B != c0 )
| ( A != C )
| ( sk3 @ A @ B @ C ) ),
inference(lifteq,[status(thm)],[6]) ).
thf(25,plain,
! [A: iS] : ( sk3 @ A @ c0 @ A ),
inference(simp,[status(thm)],[24]) ).
thf(390,plain,
( ~ $true
| ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ),
inference(rewrite,[status(thm)],[270,25]) ).
thf(391,plain,
( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ),
inference(simp,[status(thm)],[390]) ).
thf(225,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ ( sk1 @ A ) )
| ( ( A @ B )
!= ( A @ ( sk1 @ A ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[19]) ).
thf(237,plain,
! [A: iS] :
( ( c0 != c0 )
| ( c0
= ( sk1 @ ( (=) @ iS @ c0 ) ) )
| ( ( c0 = A )
!= ( c0
= ( sk1 @ ( (=) @ iS @ c0 ) ) ) )
| ~ $true ),
inference(replace_leibeq,[status(thm)],[225:[bind(A,$thf( (=) @ iS @ c0 ))]]) ).
thf(244,plain,
! [A: iS] :
( ( c0 != c0 )
| ( ( sk1 @ ( (=) @ iS @ c0 ) )
= c0 )
| ( ( c0 = A )
!= ( c0
= ( sk1 @ ( (=) @ iS @ c0 ) ) ) )
| ~ $true ),
inference(lifteq,[status(thm)],[237]) ).
thf(255,plain,
( ~ $true
| ( ( sk1 @ ( (=) @ iS @ c0 ) )
= c0 ) ),
inference(pattern_uni,[status(thm)],[244:[bind(A,$thf( sk1 @ ( (=) @ iS @ c0 ) ))]]) ).
thf(325,plain,
( ( sk1 @ ( (=) @ iS @ c0 ) )
= c0 ),
inference(simp,[status(thm)],[255]) ).
thf(18,plain,
! [A: iS] :
( ( c0 != c0 )
| ( c0
= ( sk2 @ ( (=) @ iS @ c0 ) ) )
| ( c0 = A ) ),
inference(replace_leibeq,[status(thm)],[8:[bind(A,$thf( (=) @ iS @ c0 ))]]) ).
thf(32,plain,
! [A: iS] :
( ( c0 != c0 )
| ( ( sk2 @ ( (=) @ iS @ c0 ) )
= c0 )
| ( c0 = A ) ),
inference(lifteq,[status(thm)],[18]) ).
thf(33,plain,
! [A: iS] :
( ( ( sk2 @ ( (=) @ iS @ c0 ) )
= c0 )
| ( c0 = A ) ),
inference(simp,[status(thm)],[32]) ).
thf(7,plain,
! [B: iS,A: iS] :
( ( cP @ A @ B )
!= c0 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(31,plain,
! [B: iS,A: iS] :
( ( cP @ A @ B )
!= c0 ),
inference(lifteq,[status(thm)],[7]) ).
thf(156,plain,
! [C: iS,B: iS,A: iS] :
( ( ( sk2 @ ( (=) @ iS @ c0 ) )
= c0 )
| ( c0 != c0 )
| ( A
!= ( cP @ B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[33,31]) ).
thf(157,plain,
! [C: iS,B: iS,A: iS] :
( ( ( sk2 @ ( (=) @ iS @ c0 ) )
= c0 )
| ( A
!= ( cP @ B @ C ) ) ),
inference(simp,[status(thm)],[156]) ).
thf(158,plain,
( ( sk2 @ ( (=) @ iS @ c0 ) )
= c0 ),
inference(pattern_uni,[status(thm)],[157:[bind(A,$thf( cP @ D @ E )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(9,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(26,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( A @ B ) ),
inference(simp,[status(thm)],[9]) ).
thf(55,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)],[26,13]) ).
thf(56,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( ( A @ B )
!= ( sk3 @ x @ x @ x ) ) ),
inference(simp,[status(thm)],[55]) ).
thf(90,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)],[56:[bind(A,$thf( ^ [C: iS] : ( sk3 @ x @ C @ x ) )),bind(B,$thf( x ))]]) ).
thf(337,plain,
( ~ $true
| ~ ( sk3 @ x
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
@ x ) ),
inference(rewrite,[status(thm)],[90,25]) ).
thf(338,plain,
~ ( sk3 @ x
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
@ x ),
inference(simp,[status(thm)],[337]) ).
thf(344,plain,
( ~ ( sk3 @ x
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ c0 )
@ x )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( sk2 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[158,338]) ).
thf(356,plain,
( ~ ( sk3 @ x
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ c0 )
@ x )
| ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[344]) ).
thf(422,plain,
( ~ ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x )
| ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( sk1 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[325,356]) ).
thf(444,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)],[422]) ).
thf(450,plain,
( ~ ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x )
| ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[444]) ).
thf(679,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)],[391,450]) ).
thf(680,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)],[679]) ).
thf(711,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)],[680]) ).
thf(720,plain,
( ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( cP @ c0 @ c0 ) ) ),
inference(simp,[status(thm)],[711]) ).
thf(51,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)],[25,26]) ).
thf(52,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)],[51]) ).
thf(93,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)],[52:[bind(A,$thf( D @ c0 )),bind(B,$thf( ^ [F: iS] : ( sk3 @ ( D @ F ) @ c0 @ ( F @ F ) ) )),bind(C,$thf( C ))]]) ).
thf(95,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)],[93:[]]) ).
thf(131,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)],[95]) ).
thf(61,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)],[30,26]) ).
thf(62,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)],[61]) ).
thf(111,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)],[62:[bind(A,$thf( E @ c0 )),bind(B,$thf( ^ [F: iS] : ( sk3 @ c0 @ ( E @ F ) @ ( F @ F ) ) )),bind(C,$thf( C ))]]) ).
thf(113,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)],[111:[]]) ).
thf(138,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)],[113]) ).
thf(577,plain,
( ~ ( sk3 @ x @ c0 @ x )
| ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ),
inference(pre_uni,[status(thm)],[462:[bind(A,$thf( ^ [C: iS] : ( sk3 @ x @ C @ x ) )),bind(B,$thf( x ))]]) ).
thf(1881,plain,
( ~ $true
| ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ) ),
inference(rewrite,[status(thm)],[577,25]) ).
thf(1882,plain,
( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x ),
inference(simp,[status(thm)],[1881]) ).
thf(676,plain,
( ( ( sk3 @ x @ sk7 @ x )
!= ( c0 = sk7 ) )
| ~ ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x ) ),
inference(func_ext,[status(esa)],[450]) ).
thf(9198,plain,
( ~ ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x )
| ~ ( sk3 @ x @ sk7 @ x )
| ( c0 != sk7 ) ),
inference(bool_ext,[status(thm)],[676]) ).
thf(9324,plain,
( ( sk7 != c0 )
| ~ ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x )
| ~ ( sk3 @ x @ sk7 @ x ) ),
inference(lifteq,[status(thm)],[9198]) ).
thf(10266,plain,
! [A: iS] :
( ( sk7 != c0 )
| ~ ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x )
| ~ $true
| ( ( sk3 @ A @ c0 @ A )
!= ( sk3 @ x @ sk7 @ x ) ) ),
inference(paramod_ordered,[status(thm)],[25,9324]) ).
thf(10267,plain,
! [A: iS] :
( ( sk7 != c0 )
| ~ ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x )
| ( ( sk3 @ A @ c0 @ A )
!= ( sk3 @ x @ sk7 @ x ) ) ),
inference(simp,[status(thm)],[10266]) ).
thf(10382,plain,
! [A: iS] :
( ( sk7 != c0 )
| ~ ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x )
| ( A != x )
| ( sk7 != c0 )
| ( A != x ) ),
inference(simp,[status(thm)],[10267]) ).
thf(10483,plain,
( ( sk7 != c0 )
| ~ ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x ) ),
inference(simp,[status(thm)],[10382]) ).
thf(10524,plain,
( ( sk7 != c0 )
| ~ $true
| ( ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x ) ) ),
inference(paramod_ordered,[status(thm)],[1882,10483]) ).
thf(10525,plain,
( ( sk7 != c0 )
| ( ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x ) ) ),
inference(simp,[status(thm)],[10524]) ).
thf(10628,plain,
( ( sk7 != c0 )
| ( x != x )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( cP @ c0 @ c0 ) )
| ( x != x ) ),
inference(simp,[status(thm)],[10525]) ).
thf(10638,plain,
( ( sk7 != c0 )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( cP @ c0 @ c0 ) ) ),
inference(simp,[status(thm)],[10628]) ).
thf(94,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)],[52:[bind(A,$thf( D @ c0 )),bind(B,$thf( ^ [F: iS] : ( sk3 @ ( D @ F ) @ F @ ( F @ F ) ) )),bind(C,$thf( C ))]]) ).
thf(96,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)],[94:[]]) ).
thf(132,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)],[96]) ).
thf(16322,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 ) ) ) ) ) )
| ( ( B @ c0 )
!= ( C @ c0 ) )
| ~ $true
| ( ( sk3 @ ( B @ A ) @ A @ ( C @ A ) )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[132,13]) ).
thf(16323,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 ) ) ) ) ) )
| ( ( B @ c0 )
!= ( C @ c0 ) )
| ( ( sk3 @ ( B @ A ) @ A @ ( C @ A ) )
!= ( sk3 @ x @ x @ x ) ) ),
inference(simp,[status(thm)],[16322]) ).
thf(16713,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)],[16323:[bind(A,$thf( x )),bind(B,$thf( ^ [D: iS] : D )),bind(C,$thf( ^ [D: iS] : D ))]]) ).
thf(16715,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)],[16713:[]]) ).
thf(17278,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)],[40,16715]) ).
thf(17279,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)],[17278]) ).
thf(17343,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)],[17279:[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(63,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)],[30,26]) ).
thf(64,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)],[63]) ).
thf(99,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)],[64:[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(100,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)],[99:[]]) ).
thf(133,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)],[100]) ).
thf(17481,plain,
! [C: iS > iS,B: iS > iS,A: iS] :
( ( sk3 @ c0 @ c0 @ ( 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 ) ) ) ) ) )
| ( ( sk1 @ ( (=) @ iS @ c0 ) )
!= ( B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[325,133]) ).
thf(17782,plain,
! [A: iS > iS] :
( ( sk3 @ c0 @ c0 @ ( A @ ( sk1 @ ( (=) @ iS @ c0 ) ) ) )
| ~ ( sk3 @ c0 @ c0 @ ( A @ c0 ) )
| ( ( A
@ ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ c0 @ B @ ( A @ B ) ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ c0 @ B @ ( A @ B ) ) ) ) )
!= ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ c0 @ B @ ( A @ B ) ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ c0 @ B @ ( A @ B ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[17481:[bind(A,$thf( sk1 @ ( (=) @ iS @ c0 ) )),bind(B,$thf( ^ [D: iS] : D ))]]) ).
thf(17785,plain,
( ~ ( sk3 @ c0 @ c0 @ c0 )
| ( sk3 @ c0 @ c0 @ ( sk1 @ ( (=) @ iS @ c0 ) ) ) ),
inference(pre_uni,[status(thm)],[17782:[bind(A,$thf( ^ [B: iS] : B ))]]) ).
thf(18295,plain,
( ~ $true
| ( sk3 @ c0 @ c0 @ c0 ) ),
inference(rewrite,[status(thm)],[17785,325,25]) ).
thf(18296,plain,
sk3 @ c0 @ c0 @ c0,
inference(simp,[status(thm)],[18295]) ).
thf(24888,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)],[17343,18296]) ).
thf(24889,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)],[24888]) ).
thf(25021,plain,
( ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0 )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( sk2 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[158,24889]) ).
thf(25091,plain,
( ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0 )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[25021]) ).
thf(25432,plain,
( ( sk3 @ c0
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0 )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( sk2 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[158,25091]) ).
thf(25512,plain,
( ( sk3 @ c0
@ ( sk2
@ ^ [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)],[25432]) ).
thf(25531,plain,
( ( sk3 @ c0
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0 )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[25512]) ).
thf(76,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)],[64:[bind(A,$thf( A )),bind(B,$thf( (=) @ iS @ c0 ))]]) ).
thf(85,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)],[76]) ).
thf(127,plain,
! [B: iS,A: iS] :
( ( c0 = B )
| ( ( sk3 @ c0 @ A @ A )
!= ( c0
= ( cP @ ( sk1 @ ( (=) @ iS @ c0 ) ) @ ( sk2 @ ( (=) @ iS @ c0 ) ) ) ) ) ),
inference(simp,[status(thm)],[85]) ).
thf(12822,plain,
! [B: iS,A: iS] :
( ( c0 = B )
| ( ( sk3 @ c0 @ A @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) ) ),
inference(rewrite,[status(thm)],[127,325,158]) ).
thf(91,plain,
( ~ ( sk3 @ c0 @ x @ x )
| ~ ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
@ x
@ x ) ),
inference(pre_uni,[status(thm)],[56:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ x @ x ) )),bind(B,$thf( x ))]]) ).
thf(4007,plain,
( ~ $true
| ~ ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
@ x
@ x ) ),
inference(rewrite,[status(thm)],[91,30]) ).
thf(4008,plain,
~ ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
@ x
@ x ),
inference(simp,[status(thm)],[4007]) ).
thf(4072,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)],[30,4008]) ).
thf(4073,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)],[4072]) ).
thf(4090,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)],[4073]) ).
thf(4107,plain,
( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) ) )
!= c0 ),
inference(simp,[status(thm)],[4090]) ).
thf(13368,plain,
! [B: iS,A: iS] :
( ( ( sk3 @ c0 @ A @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) )
| ( c0 != c0 )
| ( B
!= ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ x @ x ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ x @ x ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[12822,4107]) ).
thf(13369,plain,
! [B: iS,A: iS] :
( ( ( sk3 @ c0 @ A @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) )
| ( B
!= ( cP
@ ( sk1
@ ^ [C: iS] : ( sk3 @ C @ x @ x ) )
@ ( sk2
@ ^ [C: iS] : ( sk3 @ C @ x @ x ) ) ) ) ),
inference(simp,[status(thm)],[13368]) ).
thf(13370,plain,
! [A: iS] :
( ( sk3 @ c0 @ A @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) ),
inference(pattern_uni,[status(thm)],[13369:[bind(A,$thf( A )),bind(B,$thf( cP @ ( sk1 @ ^ [C: iS] : ( sk3 @ C @ x @ x ) ) @ ( sk2 @ ^ [C: iS] : ( sk3 @ C @ x @ x ) ) ))]]) ).
thf(13885,plain,
! [B: iS,A: iS] :
( ( c0
!= ( cP @ c0 @ c0 ) )
| ( ( sk3 @ A @ c0 @ A )
!= ( sk3 @ c0 @ B @ B ) ) ),
inference(paramod_ordered,[status(thm)],[25,13370]) ).
thf(13886,plain,
( c0
!= ( cP @ c0 @ c0 ) ),
inference(pattern_uni,[status(thm)],[13885:[bind(A,$thf( c0 )),bind(B,$thf( c0 ))]]) ).
thf(13933,plain,
( ( cP @ c0 @ c0 )
!= c0 ),
inference(lifteq,[status(thm)],[13886]) ).
thf(1912,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)],[1882,450]) ).
thf(1913,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)],[1912]) ).
thf(1932,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)],[1913]) ).
thf(1939,plain,
( ( ( ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( cP @ c0 @ c0 ) ) ),
inference(simp,[status(thm)],[1932]) ).
thf(4037,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)],[3872,4008]) ).
thf(4038,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)],[4037]) ).
thf(4094,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)],[4038]) ).
thf(4110,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)],[4094]) ).
thf(579,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)],[462:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ C @ x ) )),bind(B,$thf( x ))]]) ).
thf(5018,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)],[579,13]) ).
thf(5019,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)],[5018]) ).
thf(5132,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)],[5019]) ).
thf(5146,plain,
( ~ ( sk3 @ c0 @ c0 @ x )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
!= x ) ),
inference(simp,[status(thm)],[5132]) ).
thf(17291,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)],[19,16715]) ).
thf(17292,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)],[17291]) ).
thf(17329,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)],[17292:[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(22699,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)],[17329,18296]) ).
thf(22700,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)],[22699]) ).
thf(22783,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)],[22700,16715]) ).
thf(22784,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)],[22783]) ).
thf(22898,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)],[22784]) ).
thf(22941,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)],[22898]) ).
thf(22963,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)],[325,22941]) ).
thf(23002,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)],[22963]) ).
thf(223,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ B )
| ( ( A @ ( sk1 @ A ) )
!= ( ~ ( A @ c0 ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[19]) ).
thf(257,plain,
! [B: iS,A: iS > $o] :
( ( A @ B )
| ~ ( A @ c0 )
| ( ( A @ ( sk1 @ A ) )
!= ( ~ ( A @ c0 ) ) ) ),
inference(simp,[status(thm)],[223]) ).
thf(22741,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)],[325,22700]) ).
thf(22902,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)],[22741]) ).
thf(23160,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)],[325,22902]) ).
thf(23339,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)],[23160]) ).
thf(23356,plain,
( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0
@ c0 )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[23339]) ).
thf(15,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(41,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)],[15]) ).
thf(42,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)],[41]) ).
thf(68,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)],[26]) ).
thf(110,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)],[68]) ).
thf(72,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)],[26:[bind(A,$thf( ^ [E: iS] : ( ( C @ E ) | ( D @ E ) ) ))]]) ).
thf(117,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)],[72]) ).
thf(121,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)],[117]) ).
thf(125,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)],[121]) ).
thf(23043,plain,
( ( ( cP @ c0 @ c0 )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( sk2 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[158,23002]) ).
thf(23044,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)],[23043]) ).
thf(23057,plain,
( ( ( cP @ c0 @ c0 )
!= ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[23044]) ).
thf(43,plain,
! [A: iS] :
( ~ $true
| ( ( sk3 @ A @ c0 @ A )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[25,13]) ).
thf(44,plain,
! [A: iS] :
( ( sk3 @ A @ c0 @ A )
!= ( sk3 @ x @ x @ x ) ),
inference(simp,[status(thm)],[43]) ).
thf(45,plain,
! [A: iS] :
( ( A != x )
| ( c0 != x )
| ( A != x ) ),
inference(simp,[status(thm)],[44]) ).
thf(46,plain,
c0 != x,
inference(simp,[status(thm)],[45]) ).
thf(272,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)],[206:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ C @ x ) )),bind(B,$thf( x ))]]) ).
thf(4510,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)],[272,13]) ).
thf(4511,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)],[4510]) ).
thf(4579,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)],[4511]) ).
thf(4622,plain,
( ~ ( sk3 @ c0 @ c0 @ x )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
!= x ) ),
inference(simp,[status(thm)],[4579]) ).
thf(73,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)],[52:[bind(A,$thf( A )),bind(B,$thf( (=) @ iS @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ))]]) ).
thf(84,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)],[73]) ).
thf(10340,plain,
( ( sk7 != c0 )
| ~ ( sk3 @ x @ sk7 @ x )
| ( ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x )
!= ( sk3 @ x @ sk7 @ x ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[9324]) ).
thf(10458,plain,
( ( sk7 != c0 )
| ~ ( sk3 @ x @ sk7 @ x )
| ( x != x )
| ( ( cP @ c0 @ c0 )
!= sk7 )
| ( x != x ) ),
inference(simp,[status(thm)],[10340]) ).
thf(10508,plain,
( ( sk7 != c0 )
| ~ ( sk3 @ x @ sk7 @ x )
| ( ( cP @ c0 @ c0 )
!= sk7 ) ),
inference(simp,[status(thm)],[10458]) ).
thf(11741,plain,
! [A: iS] :
( ( sk7 != c0 )
| ~ $true
| ( ( cP @ c0 @ c0 )
!= sk7 )
| ( ( sk3 @ A @ c0 @ A )
!= ( sk3 @ x @ sk7 @ x ) ) ),
inference(paramod_ordered,[status(thm)],[25,10508]) ).
thf(11742,plain,
! [A: iS] :
( ( sk7 != c0 )
| ( ( cP @ c0 @ c0 )
!= sk7 )
| ( ( sk3 @ A @ c0 @ A )
!= ( sk3 @ x @ sk7 @ x ) ) ),
inference(simp,[status(thm)],[11741]) ).
thf(11812,plain,
! [A: iS] :
( ( sk7 != c0 )
| ( ( cP @ c0 @ c0 )
!= sk7 )
| ( A != x )
| ( sk7 != c0 )
| ( A != x ) ),
inference(simp,[status(thm)],[11742]) ).
thf(11870,plain,
( ( sk7 != c0 )
| ( ( cP @ c0 @ c0 )
!= sk7 ) ),
inference(simp,[status(thm)],[11812]) ).
thf(395,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)],[391,338]) ).
thf(396,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)],[395]) ).
thf(407,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)],[396]) ).
thf(411,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)],[407]) ).
thf(69,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)],[26:[bind(A,$thf( ^ [D: iS] : ~ ( C @ D ) ))]]) ).
thf(115,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)],[69]) ).
thf(116,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)],[115]) ).
thf(24963,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)],[24889,16715]) ).
thf(24964,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)],[24963]) ).
thf(25088,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)],[24964]) ).
thf(25107,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)],[25088]) ).
thf(25144,plain,
( ( ( cP @ c0
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( sk1 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[325,25107]) ).
thf(25183,plain,
( ( ( cP @ c0
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[25144]) ).
thf(53,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)],[25,26]) ).
thf(54,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)],[53]) ).
thf(79,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)],[54:[bind(A,$thf( A )),bind(B,$thf( (=) @ iS @ c0 ))]]) ).
thf(87,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)],[79]) ).
thf(128,plain,
! [B: iS,A: iS] :
( ( c0 = B )
| ( ( sk3 @ A @ c0 @ A )
!= ( c0
= ( cP @ ( sk1 @ ( (=) @ iS @ c0 ) ) @ ( sk2 @ ( (=) @ iS @ c0 ) ) ) ) ) ),
inference(simp,[status(thm)],[87]) ).
thf(13995,plain,
! [B: iS,A: iS] :
( ( c0 = B )
| ( ( sk3 @ A @ c0 @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) ) ),
inference(rewrite,[status(thm)],[128,325,158]) ).
thf(14094,plain,
! [B: iS,A: iS] :
( ( ( sk3 @ A @ c0 @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) )
| ( c0 != c0 )
| ( B
!= ( cP @ c0 @ c0 ) ) ),
inference(paramod_ordered,[status(thm)],[13995,13933]) ).
thf(14095,plain,
! [B: iS,A: iS] :
( ( ( sk3 @ A @ c0 @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) )
| ( B
!= ( cP @ c0 @ c0 ) ) ),
inference(simp,[status(thm)],[14094]) ).
thf(14096,plain,
! [A: iS] :
( ( sk3 @ A @ c0 @ A )
!= ( c0
= ( cP @ c0 @ c0 ) ) ),
inference(pattern_uni,[status(thm)],[14095:[bind(A,$thf( A )),bind(B,$thf( cP @ c0 @ c0 ))]]) ).
thf(67,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( ( A @ B )
!= ( ~ ( A @ c0 ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[26]) ).
thf(102,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ~ ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
| ( ( A @ B )
!= ( ~ ( A @ c0 ) ) ) ),
inference(simp,[status(thm)],[67]) ).
thf(92,plain,
( ~ ( sk3 @ c0 @ c0 @ x )
| ~ ( sk3
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) ) )
@ ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ x ) ) )
@ x ) ),
inference(pre_uni,[status(thm)],[56:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ C @ x ) )),bind(B,$thf( x ))]]) ).
thf(1910,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)],[1882,338]) ).
thf(1911,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)],[1910]) ).
thf(1928,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)],[1911]) ).
thf(1936,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)],[1928]) ).
thf(271,plain,
( ~ ( sk3 @ c0 @ x @ x )
| ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ) ),
inference(pre_uni,[status(thm)],[206:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ x @ x ) )),bind(B,$thf( x ))]]) ).
thf(868,plain,
( ~ $true
| ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ) ),
inference(rewrite,[status(thm)],[271,30]) ).
thf(869,plain,
( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x ),
inference(simp,[status(thm)],[868]) ).
thf(4046,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)],[869,4008]) ).
thf(4047,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)],[4046]) ).
thf(4092,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)],[4047]) ).
thf(4108,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)],[4092]) ).
thf(3899,plain,
( ~ $true
| ( ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[3872,13]) ).
thf(3900,plain,
( ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x )
!= ( sk3 @ x @ x @ x ) ),
inference(simp,[status(thm)],[3899]) ).
thf(3933,plain,
( ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
!= x )
| ( x != x )
| ( x != x ) ),
inference(simp,[status(thm)],[3900]) ).
thf(3941,plain,
( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
!= x ),
inference(simp,[status(thm)],[3933]) ).
thf(120,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)],[117]) ).
thf(124,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)],[120]) ).
thf(1883,plain,
( ~ $true
| ( ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[1882,13]) ).
thf(1884,plain,
( ( sk3 @ x
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ x @ x ) ),
inference(simp,[status(thm)],[1883]) ).
thf(1930,plain,
( ( x != x )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= x )
| ( x != x ) ),
inference(simp,[status(thm)],[1884]) ).
thf(1937,plain,
( ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= x ),
inference(simp,[status(thm)],[1930]) ).
thf(219,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)],[19,19]) ).
thf(220,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)],[219]) ).
thf(232,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)],[220:[bind(A,$thf( (=) @ iS @ c0 ))]]) ).
thf(254,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)],[232]) ).
thf(291,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)],[254:[bind(A,$thf( A )),bind(B,$thf( ^ [D: iS] : ( c0 = ( sk1 @ ( (=) @ iS @ D ) ) ) )),bind(C,$thf( C ))]]) ).
thf(307,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)],[291]) ).
thf(308,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)],[307]) ).
thf(1110,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)],[308]) ).
thf(1136,plain,
! [A: iS] :
( ( ( sk1
@ ( (=) @ iS
@ ( sk1
@ ^ [B: iS] :
( c0
= ( sk1 @ ( (=) @ iS @ B ) ) ) ) ) )
= c0 )
| ( c0 = A ) ),
inference(pattern_uni,[status(thm)],[1110:[bind(A,$thf( A )),bind(B,$thf( sk1 @ ^ [C: iS] : ( c0 = ( sk1 @ ( (=) @ iS @ C ) ) ) ))]]) ).
thf(2241,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)],[1136,31]) ).
thf(2242,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)],[2241]) ).
thf(2243,plain,
( ( sk1
@ ( (=) @ iS
@ ( sk1
@ ^ [A: iS] :
( c0
= ( sk1 @ ( (=) @ iS @ A ) ) ) ) ) )
= c0 ),
inference(pattern_uni,[status(thm)],[2242:[bind(A,$thf( cP @ D @ E )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(392,plain,
( ~ $true
| ( ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[391,13]) ).
thf(393,plain,
( ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ x @ x ) ),
inference(simp,[status(thm)],[392]) ).
thf(408,plain,
( ( x != x )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= x )
| ( x != x ) ),
inference(simp,[status(thm)],[393]) ).
thf(412,plain,
( ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= x ),
inference(simp,[status(thm)],[408]) ).
thf(23159,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)],[325,22902]) ).
thf(23317,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)],[23159]) ).
thf(23348,plain,
( ( sk3 @ c0
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0 )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[23317]) ).
thf(870,plain,
( ~ $true
| ( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x )
!= ( sk3 @ x @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[869,13]) ).
thf(871,plain,
( ( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
@ x
@ x )
!= ( sk3 @ x @ x @ x ) ),
inference(simp,[status(thm)],[870]) ).
thf(900,plain,
( ( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
!= x )
| ( x != x )
| ( x != x ) ),
inference(simp,[status(thm)],[871]) ).
thf(904,plain,
( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ x @ x ) )
!= x ),
inference(simp,[status(thm)],[900]) ).
thf(209,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ B )
| ~ ( C @ c0 )
| ~ $true
| ( C @ D )
| ( ( A @ ( sk1 @ A ) )
!= ( C @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,26]) ).
thf(210,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ B )
| ~ ( C @ c0 )
| ( C @ D )
| ( ( A @ ( sk1 @ A ) )
!= ( C @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) ) ) ),
inference(simp,[status(thm)],[209]) ).
thf(258,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ B )
| ~ ( C @ c0 )
| ( C @ D )
| ( ( A @ ( sk1 @ A ) )
!= ( C @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) ) ) ),
inference(pre_uni,[status(thm)],[210:[]]) ).
thf(259,plain,
! [D: iS,C: iS > $o,B: iS,A: iS > $o] :
( ( C @ D )
| ~ ( C @ c0 )
| ( A @ B )
| ~ ( A @ c0 )
| ( ( A @ ( sk1 @ A ) )
!= ( C @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) ) ) ),
inference(pre_uni,[status(thm)],[258:[]]) ).
thf(24965,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)],[24889,13]) ).
thf(24966,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)],[24965]) ).
thf(25082,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)],[24966]) ).
thf(25128,plain,
( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= x ),
inference(simp,[status(thm)],[25082]) ).
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(335,plain,
! [B: iS,A: iS] :
( ( sk4 @ B @ ( cP @ A @ B ) )
= A ),
inference(lifteq,[status(thm)],[23]) ).
thf(18425,plain,
! [B: iS,A: iS > $o] :
( ~ $true
| ( A @ ( sk2 @ A ) )
| ( A @ B )
| ( ( sk3 @ c0 @ c0 @ c0 )
!= ( A @ c0 ) ) ),
inference(paramod_ordered,[status(thm)],[18296,40]) ).
thf(18426,plain,
! [B: iS,A: iS > $o] :
( ( A @ ( sk2 @ A ) )
| ( A @ B )
| ( ( sk3 @ c0 @ c0 @ c0 )
!= ( A @ c0 ) ) ),
inference(simp,[status(thm)],[18425]) ).
thf(18621,plain,
! [A: iS] :
( ( sk3
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) )
@ c0
@ c0 )
| ( sk3 @ A @ c0 @ c0 ) ),
inference(pre_uni,[status(thm)],[18426:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ c0 @ c0 ) )),bind(B,$thf( B ))]]) ).
thf(18717,plain,
! [A: iS] :
( ( sk3
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) )
@ c0
@ c0 )
| ( sk3 @ A @ c0 @ c0 ) ),
inference(simp,[status(thm)],[18621]) ).
thf(28115,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)],[18717]) ).
thf(28236,plain,
( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ c0 @ c0 ) )
@ c0
@ c0 ),
inference(pattern_uni,[status(thm)],[28115:[bind(A,$thf( sk2 @ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) ))]]) ).
thf(80,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)],[62:[bind(A,$thf( A )),bind(B,$thf( (=) @ iS @ ( cP @ ( sk1 @ B ) @ ( sk2 @ B ) ) ))]]) ).
thf(86,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)],[80]) ).
thf(57,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)],[26,26]) ).
thf(58,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)],[57]) ).
thf(78,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)],[58:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( (=) @ iS @ ( cP @ ( sk1 @ C ) @ ( sk2 @ C ) ) ))]]) ).
thf(81,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)],[78]) ).
thf(65,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ B )
| ( ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
!= ( A @ c0 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[26]) ).
thf(97,plain,
! [B: iS,A: iS > $o] :
( ~ ( A @ c0 )
| ( A @ B )
| ( ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
!= ( A @ c0 ) ) ),
inference(pre_uni,[status(thm)],[65:[]]) ).
thf(98,plain,
! [B: iS,A: iS > $o] :
( ( A @ B )
| ~ ( A @ c0 )
| ( ( A @ ( cP @ ( sk1 @ A ) @ ( sk2 @ A ) ) )
!= ( A @ c0 ) ) ),
inference(pre_uni,[status(thm)],[97:[]]) ).
thf(23001,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)],[158,22941]) ).
thf(23004,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)],[23001]) ).
thf(25182,plain,
( ( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0 )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( sk2 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[158,25107]) ).
thf(25184,plain,
( ( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0 )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[25182]) ).
thf(107,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)],[58:[]]) ).
thf(108,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)],[107:[]]) ).
thf(105,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)],[54:[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(106,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)],[105:[]]) ).
thf(135,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)],[106]) ).
thf(119,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)],[117]) ).
thf(123,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)],[119]) ).
thf(25224,plain,
( ( ( cP @ c0 @ c0 )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( sk2 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[158,25183]) ).
thf(25233,plain,
( ( ( cP @ c0 @ c0 )
!= ( sk2
@ ^ [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)],[25224]) ).
thf(25238,plain,
( ( ( cP @ c0 @ c0 )
!= ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[25233]) ).
thf(17142,plain,
! [A: iS] :
( ~ $true
| ( ( sk3 @ A @ c0 @ 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)],[25,16715]) ).
thf(17143,plain,
! [A: iS] :
( ( sk3 @ A @ c0 @ 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)],[17142]) ).
thf(17314,plain,
! [A: iS] :
( ( A
!= ( 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 ) ) )
!= c0 )
| ( A
!= ( cP
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) )
@ ( sk2
@ ^ [B: iS] : ( sk3 @ B @ B @ B ) ) ) ) ),
inference(simp,[status(thm)],[17143]) ).
thf(17356,plain,
( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) ) )
!= c0 ),
inference(simp,[status(thm)],[17314]) ).
thf(339,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)],[25,338]) ).
thf(340,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)],[339]) ).
thf(355,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)],[340]) ).
thf(363,plain,
( ( cP
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ ( sk2
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) ) )
!= c0 ),
inference(simp,[status(thm)],[355]) ).
thf(59,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)],[26,26]) ).
thf(60,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)],[59]) ).
thf(103,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)],[60:[]]) ).
thf(104,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)],[103:[]]) ).
thf(18435,plain,
! [B: iS,A: iS > $o] :
( ~ $true
| ( A @ ( sk1 @ A ) )
| ( A @ B )
| ( ( sk3 @ c0 @ c0 @ c0 )
!= ( A @ c0 ) ) ),
inference(paramod_ordered,[status(thm)],[18296,19]) ).
thf(18436,plain,
! [B: iS,A: iS > $o] :
( ( A @ ( sk1 @ A ) )
| ( A @ B )
| ( ( sk3 @ c0 @ c0 @ c0 )
!= ( A @ c0 ) ) ),
inference(simp,[status(thm)],[18435]) ).
thf(18528,plain,
! [A: iS] :
( ( sk3 @ c0
@ ( sk1
@ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) )
@ c0 )
| ( sk3 @ c0 @ A @ c0 ) ),
inference(pre_uni,[status(thm)],[18436:[bind(A,$thf( ^ [C: iS] : ( sk3 @ c0 @ C @ c0 ) )),bind(B,$thf( B ))]]) ).
thf(18661,plain,
! [A: iS] :
( ( sk3 @ c0
@ ( sk1
@ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) )
@ c0 )
| ( sk3 @ c0 @ A @ c0 ) ),
inference(simp,[status(thm)],[18528]) ).
thf(19891,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)],[18661]) ).
thf(20126,plain,
( sk3 @ c0
@ ( sk1
@ ^ [A: iS] : ( sk3 @ c0 @ A @ c0 ) )
@ c0 ),
inference(pattern_uni,[status(thm)],[19891:[bind(A,$thf( sk1 @ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) ))]]) ).
thf(10536,plain,
( ( sk7 != c0 )
| ~ $true
| ( ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x ) ) ),
inference(paramod_ordered,[status(thm)],[391,10483]) ).
thf(10537,plain,
( ( sk7 != c0 )
| ( ( sk3 @ x
@ ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
@ x )
!= ( sk3 @ x @ ( cP @ c0 @ c0 ) @ x ) ) ),
inference(simp,[status(thm)],[10536]) ).
thf(10610,plain,
( ( sk7 != c0 )
| ( x != x )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( cP @ c0 @ c0 ) )
| ( x != x ) ),
inference(simp,[status(thm)],[10537]) ).
thf(10659,plain,
( ( sk7 != c0 )
| ( ( sk1
@ ^ [A: iS] : ( sk3 @ x @ A @ x ) )
!= ( cP @ c0 @ c0 ) ) ),
inference(simp,[status(thm)],[10610]) ).
thf(112,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)],[62:[bind(A,$thf( E @ c0 )),bind(B,$thf( ^ [F: iS] : ( sk3 @ F @ ( E @ F ) @ ( F @ F ) ) )),bind(C,$thf( C ))]]) ).
thf(114,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)],[112:[]]) ).
thf(139,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)],[114]) ).
thf(18529,plain,
! [A: iS] :
( ( sk3
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) )
@ c0
@ c0 )
| ( sk3 @ A @ c0 @ c0 ) ),
inference(pre_uni,[status(thm)],[18436:[bind(A,$thf( ^ [C: iS] : ( sk3 @ C @ c0 @ c0 ) )),bind(B,$thf( B ))]]) ).
thf(18662,plain,
! [A: iS] :
( ( sk3
@ ( sk1
@ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) )
@ c0
@ c0 )
| ( sk3 @ A @ c0 @ c0 ) ),
inference(simp,[status(thm)],[18529]) ).
thf(24153,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)],[18662]) ).
thf(24333,plain,
( sk3
@ ( sk1
@ ^ [A: iS] : ( sk3 @ A @ c0 @ c0 ) )
@ c0
@ c0 ),
inference(pattern_uni,[status(thm)],[24153:[bind(A,$thf( sk1 @ ^ [B: iS] : ( sk3 @ B @ c0 @ c0 ) ))]]) ).
thf(25433,plain,
( ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0
@ c0 )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) )
| ( ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( sk2 @ ( (=) @ iS @ c0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[158,25091]) ).
thf(25513,plain,
( ( sk3
@ ( sk2
@ ^ [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)],[25433]) ).
thf(25532,plain,
( ( sk3
@ ( sk2
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
@ c0
@ c0 )
| ( ( ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= ( (=) @ iS @ c0 ) ) ),
inference(simp,[status(thm)],[25513]) ).
thf(22788,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)],[22700,13]) ).
thf(22789,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)],[22788]) ).
thf(22915,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)],[22789]) ).
thf(22924,plain,
( ( sk1
@ ^ [A: iS] : ( sk3 @ A @ A @ A ) )
!= x ),
inference(simp,[status(thm)],[22915]) ).
thf(18620,plain,
! [A: iS] :
( ( sk3 @ c0
@ ( sk2
@ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) )
@ c0 )
| ( sk3 @ c0 @ A @ c0 ) ),
inference(pre_uni,[status(thm)],[18426:[bind(A,$thf( ^ [C: iS] : ( sk3 @ c0 @ C @ c0 ) )),bind(B,$thf( B ))]]) ).
thf(18716,plain,
! [A: iS] :
( ( sk3 @ c0
@ ( sk2
@ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) )
@ c0 )
| ( sk3 @ c0 @ A @ c0 ) ),
inference(simp,[status(thm)],[18620]) ).
thf(26384,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)],[18716]) ).
thf(26587,plain,
( sk3 @ c0
@ ( sk2
@ ^ [A: iS] : ( sk3 @ c0 @ A @ c0 ) )
@ c0 ),
inference(pattern_uni,[status(thm)],[26384:[bind(A,$thf( sk2 @ ^ [B: iS] : ( sk3 @ c0 @ B @ c0 ) ))]]) ).
thf(118,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)],[117]) ).
thf(122,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)],[118]) ).
thf(32215,plain,
$false,
inference(e,[status(thm)],[21,3872,336,720,131,138,10638,25531,13933,1882,1939,4110,5146,23002,37,25,257,23356,42,110,125,23057,46,325,4008,22902,4622,84,11870,132,133,411,18296,116,25183,14096,102,92,12822,1936,4108,22941,356,869,24889,3941,124,16715,1937,2243,13,412,23348,25091,13370,904,579,259,25128,391,25107,335,28236,86,81,98,4107,13995,22700,23004,25184,108,135,3,123,25238,17356,338,31,450,363,104,20126,40,26,158,10659,139,272,10483,24333,25532,30,22924,19,26587,122,676]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV199^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21 % Computer : n008.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:21:29 UTC 2026
% 0.10/0.21 % CPUTime :
% 0.10/0.21 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.85/0.79 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.16/0.98 % [INFO] Parsing done (183ms).
% 1.16/0.99 % [INFO] Running in sequential loop mode.
% 1.79/1.39 % [INFO] eprover registered as external prover.
% 1.79/1.40 % [INFO] Scanning for conjecture ...
% 2.21/1.52 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.21/1.57 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.21/1.57 % [INFO] Problem is higher-order (TPTP THF).
% 2.21/1.57 % [INFO] Type checking passed.
% 2.21/1.58 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 270.24/99.09 % External prover 'e' found a proof!
% 270.24/99.09 % [INFO] Killing All external provers ...
% 270.24/99.09 % Time passed: 98730ms (effective reasoning time: 98087ms)
% 270.24/99.09 % 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)>
% 270.24/99.09 % Axioms used in derivation (0):
% 270.24/99.09 % No. of inferences in proof: 345
% 270.24/99.09 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 98730 ms resp. 98087 ms w/o parsing
% 270.82/99.21 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 270.82/99.22 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------