%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYO222^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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:45:25 AM UTC 2026
% Result : Theorem 75.02s 18.90s
% Output : Refutation 91.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 2
% Syntax : Number of formulae : 730 ( 299 unt; 0 typ; 1 def)
% Number of atoms : 2572 ( 851 equ; 216 cnn)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 4977 (1093 ~; 660 |; 12 &;3202 @)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 475 ( 475 >; 0 *; 0 +; 0 <<)
% Number of symbols : 36 ( 32 usr; 31 con; 0-2 aty)
% Number of variables : 1251 ( 544 ^; 700 !; 6 ?;1251 :)
% ( 0 !>; 0 ?*; 0 @-; 1 @+)
% Comments :
%------------------------------------------------------------------------------
thf(f_decl,type,
f: $i > $i ).
thf(a_decl,type,
a: $i ).
thf(cP_decl,type,
cP: $i > $o ).
thf(sk1_decl,type,
sk1: ( $i > $o ) > $o ).
thf(sk2_decl,type,
sk2: ( $i > $o ) > $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk5_decl,type,
sk5: $i ).
thf(sk6_decl,type,
sk6: $i ).
thf(sk7_decl,type,
sk7: $i ).
thf(sk8_decl,type,
sk8: $i ).
thf(sk9_decl,type,
sk9: $i ).
thf(sk12_decl,type,
sk12: $i ).
thf(sk13_decl,type,
sk13: $i ).
thf(sk14_decl,type,
sk14: $i ).
thf(sk15_decl,type,
sk15: $i ).
thf(sk16_decl,type,
sk16: $i ).
thf(sk17_decl,type,
sk17: $i ).
thf(sk18_decl,type,
sk18: $i ).
thf(sk19_decl,type,
sk19: $i ).
thf(sk20_decl,type,
sk20: $i ).
thf(sk21_decl,type,
sk21: $i ).
thf(sk22_decl,type,
sk22: $i ).
thf(sk26_decl,type,
sk26: $i ).
thf(sk27_decl,type,
sk27: $i ).
thf(sk28_decl,type,
sk28: $i ).
thf(sk29_decl,type,
sk29: $i ).
thf(sk30_decl,type,
sk30: $i ).
thf(sk31_decl,type,
sk31: $i ).
thf(sk33_decl,type,
sk33: $i ).
thf(sk34_decl,type,
sk34: $i ).
thf(sk35_decl,type,
sk35: $i ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: $i > $o] :
@+[B: $i] :
~ ( ( A @ ( f @ B ) )
=> ( cP @ B ) ) ) ) ).
thf(1,conjecture,
? [A: $i > $o] :
( ! [B: $i] :
( ( A @ ( f @ B ) )
=> ( cP @ B ) )
& ( ( ( cP @ a )
& ! [B: $i,C: $i] :
( ( ( f @ B )
= ( f @ C ) )
=> ( B = C ) ) )
=> ? [B: $i] : ( A @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM115A) ).
thf(2,negated_conjecture,
~ ? [A: $i > $o] :
( ! [B: $i] :
( ( A @ ( f @ B ) )
=> ( cP @ B ) )
& ( ( ( cP @ a )
& ! [B: $i,C: $i] :
( ( ( f @ B )
= ( f @ C ) )
=> ( B = C ) ) )
=> ? [B: $i] : ( A @ B ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ? [A: $i > $o] :
( ! [B: $i] :
( ( A @ ( f @ B ) )
=> ( cP @ B ) )
& ( ( ( cP @ a )
& ! [B: $i,C: $i] :
( ( ( f @ B )
= ( f @ C ) )
=> ( B = C ) ) )
=> ? [B: $i] : ( A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
! [D: $i,C: $i,B: $i,A: $i > $o] :
( ( ( A @ ( f @ ( sk2 @ A ) ) )
| ~ ( sk1 @ A ) )
& ( ~ ( cP @ ( sk2 @ A ) )
| ~ ( sk1 @ A ) )
& ( ( sk1 @ A )
| ( cP @ a ) )
& ( ( sk1 @ A )
| ( ( f @ B )
!= ( f @ C ) )
| ( B = C ) )
& ( ( sk1 @ A )
| ~ ( A @ D ) ) ),
inference(cnf,[status(esa)],[3]) ).
thf(9,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A )
| ~ ( A @ B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(11,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A )
| ~ ( A @ B ) ),
inference(simp,[status(thm)],[9]) ).
thf(29,plain,
! [B: $i > $o,A: $i] :
( ( sk1
@ ^ [C: $i] :
~ ( B @ C ) )
| ~ ~ ( B @ A ) ),
inference(prim_subst,[status(thm)],[11:[bind(A,$thf( ^ [D: $i] : ~ ( C @ D ) ))]]) ).
thf(42,plain,
! [B: $i > $o,A: $i] :
( ( sk1
@ ^ [C: $i] :
~ ( B @ C ) )
| ( B @ A ) ),
inference(cnf,[status(esa)],[29]) ).
thf(43,plain,
! [B: $i > $o,A: $i] :
( ( sk1
@ ^ [C: $i] :
~ ( B @ C ) )
| ( B @ A ) ),
inference(simp,[status(thm)],[42]) ).
thf(5,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ~ ( sk1 @ A ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(15,plain,
! [C: $i > $o,B: $i,A: $i > $o] :
( ~ ( A @ B )
| ~ ( cP @ ( sk2 @ C ) )
| ~ $true
| ( ( sk1 @ A )
!= ( sk1 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[11,5]) ).
thf(16,plain,
! [C: $i > $o,B: $i,A: $i > $o] :
( ~ ( A @ B )
| ~ ( cP @ ( sk2 @ C ) )
| ( ( sk1 @ A )
!= ( sk1 @ C ) ) ),
inference(simp,[status(thm)],[15]) ).
thf(17,plain,
! [B: $i,A: $i > $o] :
( ~ ( A @ B )
| ~ ( cP @ ( sk2 @ A ) ) ),
inference(pattern_uni,[status(thm)],[16:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A ))]]) ).
thf(50,plain,
! [B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( ( cP @ ( sk2 @ A ) )
!= ( A @ B ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[17]) ).
thf(58,plain,
~ ( cP @ ( sk2 @ cP ) ),
inference(pre_uni,[status(thm)],[50:[bind(A,$thf( cP )),bind(B,$thf( sk2 @ cP ))]]) ).
thf(1088,plain,
! [B: $i > $o,A: $i] :
( ( sk1
@ ^ [C: $i] :
~ ( B @ C ) )
| ~ $true
| ( ( B @ A )
!= ( cP @ ( sk2 @ cP ) ) ) ),
inference(paramod_ordered,[status(thm)],[43,58]) ).
thf(1089,plain,
! [B: $i > $o,A: $i] :
( ( sk1
@ ^ [C: $i] :
~ ( B @ C ) )
| ( ( B @ A )
!= ( cP @ ( sk2 @ cP ) ) ) ),
inference(simp,[status(thm)],[1088]) ).
thf(1109,plain,
( sk1
@ ^ [A: $i] :
~ ( cP @ A ) ),
inference(pre_uni,[status(thm)],[1089:[bind(A,$thf( sk2 @ cP )),bind(B,$thf( cP ))]]) ).
thf(1188,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ~ $true
| ( ( sk1
@ ^ [B: $i] :
~ ( cP @ B ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1109,5]) ).
thf(1189,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1
@ ^ [B: $i] :
~ ( cP @ B ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[1188]) ).
thf(1190,plain,
~ ( cP
@ ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) ) ),
inference(pattern_uni,[status(thm)],[1189:[bind(A,$thf( ^ [B: $i] : ~ ( cP @ B ) ))]]) ).
thf(8,plain,
! [A: $i > $o] :
( ( sk1 @ A )
| ( cP @ a ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(7,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ~ ( sk1 @ A ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(117,plain,
( $false
| ~ ( sk1
@ ^ [A: $i] : $false ) ),
inference(prim_subst,[status(thm)],[7:[bind(A,$thf( ^ [B: $i] : $false ))]]) ).
thf(141,plain,
~ ( sk1
@ ^ [A: $i] : $false ),
inference(simp,[status(thm)],[117]) ).
thf(157,plain,
! [A: $i > $o] :
( ( cP @ a )
| ~ $true
| ( ( sk1 @ A )
!= ( sk1
@ ^ [B: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[8,141]) ).
thf(158,plain,
! [A: $i > $o] :
( ( cP @ a )
| ( ( sk1 @ A )
!= ( sk1
@ ^ [B: $i] : $false ) ) ),
inference(simp,[status(thm)],[157]) ).
thf(159,plain,
cP @ a,
inference(pattern_uni,[status(thm)],[158:[bind(A,$thf( ^ [B: $i] : $false ))]]) ).
thf(171,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A )
| ~ $true
| ( ( cP @ a )
!= ( A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[159,11]) ).
thf(172,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A )
| ( ( cP @ a )
!= ( A @ B ) ) ),
inference(simp,[status(thm)],[171]) ).
thf(180,plain,
sk1 @ cP,
inference(pre_uni,[status(thm)],[172:[bind(A,$thf( cP )),bind(B,$thf( a ))]]) ).
thf(188,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ~ $true
| ( ( sk1 @ cP )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[180,7]) ).
thf(189,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ( ( sk1 @ cP )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[188]) ).
thf(190,plain,
cP @ ( f @ ( sk2 @ cP ) ),
inference(pattern_uni,[status(thm)],[189:[bind(A,$thf( cP ))]]) ).
thf(20,plain,
! [D: $i,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( sk1 @ C )
| ~ $true
| ( ( sk1 @ A )
!= ( C @ D ) ) ),
inference(paramod_ordered,[status(thm)],[11,11]) ).
thf(21,plain,
! [D: $i,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( sk1 @ C )
| ( ( sk1 @ A )
!= ( C @ D ) ) ),
inference(simp,[status(thm)],[20]) ).
thf(31,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ~ ( C @ B @ A )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) ) ),
inference(pre_uni,[status(thm)],[21:[bind(A,$thf( E @ D )),bind(B,$thf( B )),bind(C,$thf( ^ [F: $i] : ( sk1 @ ( E @ F ) ) ))]]) ).
thf(45,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ~ ( C @ B @ A )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) ) ),
inference(simp,[status(thm)],[31]) ).
thf(1346,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ~ $true
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( ( cP @ ( f @ ( sk2 @ cP ) ) )
!= ( C @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[190,45]) ).
thf(1347,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( ( cP @ ( f @ ( sk2 @ cP ) ) )
!= ( C @ B @ A ) ) ),
inference(simp,[status(thm)],[1346]) ).
thf(1359,plain,
( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ ( f @ A ) ) ) ),
inference(pre_uni,[status(thm)],[1347:[bind(A,$thf( A )),bind(B,$thf( sk2 @ cP )),bind(C,$thf( ^ [D: $i] : ^ [E: $i] : ( cP @ ( f @ D ) ) ))]]) ).
thf(1995,plain,
( ~ $true
| ( ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ ( f @ A ) ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[1359,141]) ).
thf(1996,plain,
( ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ ( f @ A ) ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[1995]) ).
thf(2024,plain,
( ( ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ ( f @ A ) ) ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[1996]) ).
thf(2771,plain,
( sk1
@ ^ [A: $i] : ( cP @ ( f @ sk8 ) ) ),
inference(func_ext,[status(esa)],[2024]) ).
thf(2809,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ~ $true
| ( ( sk1
@ ^ [B: $i] : ( cP @ ( f @ sk8 ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2771,7]) ).
thf(2810,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ( ( sk1
@ ^ [B: $i] : ( cP @ ( f @ sk8 ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[2809]) ).
thf(2811,plain,
cP @ ( f @ sk8 ),
inference(pattern_uni,[status(thm)],[2810:[bind(A,$thf( ^ [B: $i] : ( cP @ ( f @ sk8 ) ) ))]]) ).
thf(1198,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ~ $true
| ( ( sk1
@ ^ [B: $i] :
~ ( cP @ B ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1109,7]) ).
thf(1199,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ( ( sk1
@ ^ [B: $i] :
~ ( cP @ B ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[1198]) ).
thf(1200,plain,
~ ( cP
@ ( f
@ ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[1199:[bind(A,$thf( ^ [B: $i] : ~ ( cP @ B ) ))]]) ).
thf(1212,plain,
~ ( cP
@ ( f
@ ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) ) ) ),
inference(cnf,[status(esa)],[1200]) ).
thf(5232,plain,
! [B: $i > $o,A: $i] :
( ( sk1
@ ^ [C: $i] :
~ ( B @ C ) )
| ~ $true
| ( ( B @ A )
!= ( cP
@ ( f
@ ( sk2
@ ^ [C: $i] :
~ ( cP @ C ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[43,1212]) ).
thf(5233,plain,
! [B: $i > $o,A: $i] :
( ( sk1
@ ^ [C: $i] :
~ ( B @ C ) )
| ( ( B @ A )
!= ( cP
@ ( f
@ ( sk2
@ ^ [C: $i] :
~ ( cP @ C ) ) ) ) ) ),
inference(simp,[status(thm)],[5232]) ).
thf(5256,plain,
( sk1
@ ^ [A: $i] :
~ ( cP @ ( f @ A ) ) ),
inference(pre_uni,[status(thm)],[5233:[bind(A,$thf( sk2 @ ^ [C: $i] : ~ ( cP @ C ) )),bind(B,$thf( ^ [C: $i] : ( cP @ ( f @ C ) ) ))]]) ).
thf(5265,plain,
( ~ $true
| ( ( sk1
@ ^ [A: $i] :
~ ( cP @ ( f @ A ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[5256,141]) ).
thf(5266,plain,
( ( sk1
@ ^ [A: $i] :
~ ( cP @ ( f @ A ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[5265]) ).
thf(5318,plain,
( ( ^ [A: $i] :
~ ( cP @ ( f @ A ) ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[5266]) ).
thf(5345,plain,
~ ( cP @ ( f @ sk12 ) ),
inference(func_ext,[status(esa)],[5318]) ).
thf(5346,plain,
~ ( cP @ ( f @ sk12 ) ),
inference(cnf,[status(esa)],[5345]) ).
thf(5369,plain,
( ~ $true
| ( ( cP @ ( f @ sk12 ) )
!= ( cP @ ( f @ sk8 ) ) ) ),
inference(paramod_ordered,[status(thm)],[2811,5346]) ).
thf(5370,plain,
( ( cP @ ( f @ sk12 ) )
!= ( cP @ ( f @ sk8 ) ) ),
inference(simp,[status(thm)],[5369]) ).
thf(5378,plain,
( ( f @ sk12 )
!= ( f @ sk8 ) ),
inference(simp,[status(thm)],[5370]) ).
thf(6014,plain,
sk12 != sk8,
inference(simp,[status(thm)],[5378]) ).
thf(1357,plain,
( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) ),
inference(pre_uni,[status(thm)],[1347:[bind(A,$thf( A )),bind(B,$thf( f @ ( sk2 @ cP ) )),bind(C,$thf( ^ [D: $i] : ^ [E: $i] : ( cP @ D ) ))]]) ).
thf(1429,plain,
( ~ $true
| ( ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[1357,141]) ).
thf(1430,plain,
( ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[1429]) ).
thf(1455,plain,
( ( ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[1430]) ).
thf(1468,plain,
( sk1
@ ^ [A: $i] : ( cP @ sk7 ) ),
inference(func_ext,[status(esa)],[1455]) ).
thf(1582,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ~ $true
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( ( sk1
@ ^ [D: $i] : ( cP @ sk7 ) )
!= ( C @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1468,45]) ).
thf(1583,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( ( sk1
@ ^ [D: $i] : ( cP @ sk7 ) )
!= ( C @ B @ A ) ) ),
inference(simp,[status(thm)],[1582]) ).
thf(1615,plain,
( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ A ) ) ) ),
inference(pre_uni,[status(thm)],[1583:[bind(A,$thf( A )),bind(B,$thf( sk7 )),bind(C,$thf( ^ [D: $i] : ^ [E: $i] : ( sk1 @ ^ [F: $i] : ( cP @ D ) ) ))]]) ).
thf(2330,plain,
( ~ $true
| ( ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ A ) ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[1615,141]) ).
thf(2331,plain,
( ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ A ) ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[2330]) ).
thf(2358,plain,
( ( ^ [A: $i] :
( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ A ) ) ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[2331]) ).
thf(2774,plain,
( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ sk9 ) ) ),
inference(func_ext,[status(esa)],[2358]) ).
thf(3351,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ~ $true
| ( ( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ sk9 ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2774,7]) ).
thf(3352,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ( ( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ sk9 ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[3351]) ).
thf(3353,plain,
( sk1
@ ^ [A: $i] : ( cP @ sk9 ) ),
inference(pattern_uni,[status(thm)],[3352:[bind(A,$thf( ^ [B: $i] : ( sk1 @ ^ [C: $i] : ( cP @ sk9 ) ) ))]]) ).
thf(3485,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ~ $true
| ( ( sk1
@ ^ [B: $i] : ( cP @ sk9 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3353,7]) ).
thf(3486,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ( ( sk1
@ ^ [B: $i] : ( cP @ sk9 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[3485]) ).
thf(3487,plain,
cP @ sk9,
inference(pattern_uni,[status(thm)],[3486:[bind(A,$thf( ^ [B: $i] : ( cP @ sk9 ) ))]]) ).
thf(22,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A )
| ( ( A @ B )
!= ( ~ ( sk1 @ A ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[11]) ).
thf(32,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A )
| ( ( A @ B )
!= ( ~ ( sk1 @ A ) ) ) ),
inference(simp,[status(thm)],[22]) ).
thf(300,plain,
! [D: $i,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( sk1 @ C )
| ( ( ~ $true )
!= ( C @ D ) )
| ( ( sk1 @ A )
!= ( sk1 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[11,32]) ).
thf(301,plain,
! [D: $i,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( sk1 @ C )
| ( C @ D )
| ( ( sk1 @ A )
!= ( sk1 @ C ) ) ),
inference(simp,[status(thm)],[300]) ).
thf(302,plain,
! [C: $i,B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( sk1 @ A )
| ( A @ C ) ),
inference(pattern_uni,[status(thm)],[301:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A ))]]) ).
thf(327,plain,
! [B: $i,A: $i] :
( ( A != A )
| ( sk1 @ ( (=) @ $i @ A ) )
| ( A = B ) ),
inference(replace_leibeq,[status(thm)],[302:[bind(A,$thf( (=) @ $i @ A ))]]) ).
thf(328,plain,
! [B: $i,A: $i] :
( ( A != A )
| ( A = B )
| ( sk1 @ ( (=) @ $i @ A ) ) ),
inference(lifteq,[status(thm)],[327]) ).
thf(331,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A = B ) ),
inference(pattern_uni,[status(thm)],[328:[]]) ).
thf(352,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A = B ) ),
inference(simp,[status(thm)],[331]) ).
thf(10354,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A != sk8 )
| ( B != sk12 ) ),
inference(paramod_ordered,[status(thm)],[352,6014]) ).
thf(10355,plain,
! [A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A != sk8 ) ),
inference(pattern_uni,[status(thm)],[10354:[bind(A,$thf( A )),bind(B,$thf( sk12 ))]]) ).
thf(11171,plain,
sk1 @ ( (=) @ $i @ sk8 ),
inference(simp,[status(thm)],[10355]) ).
thf(11806,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk8 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11171,5]) ).
thf(11807,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1 @ ( (=) @ $i @ sk8 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[11806]) ).
thf(11808,plain,
~ ( cP @ ( sk2 @ ( (=) @ $i @ sk8 ) ) ),
inference(pattern_uni,[status(thm)],[11807:[bind(A,$thf( (=) @ $i @ sk8 ))]]) ).
thf(16457,plain,
( ~ $true
| ( ( cP @ ( sk2 @ ( (=) @ $i @ sk8 ) ) )
!= ( cP @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[3487,11808]) ).
thf(16458,plain,
( ( cP @ ( sk2 @ ( (=) @ $i @ sk8 ) ) )
!= ( cP @ sk9 ) ),
inference(simp,[status(thm)],[16457]) ).
thf(16501,plain,
( ( sk2 @ ( (=) @ $i @ sk8 ) )
!= sk9 ),
inference(simp,[status(thm)],[16458]) ).
thf(255,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A )
| ~ $true
| ( ( cP @ ( f @ ( sk2 @ cP ) ) )
!= ( A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[190,11]) ).
thf(256,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A )
| ( ( cP @ ( f @ ( sk2 @ cP ) ) )
!= ( A @ B ) ) ),
inference(simp,[status(thm)],[255]) ).
thf(268,plain,
( sk1
@ ^ [A: $i] : ( cP @ ( f @ A ) ) ),
inference(pre_uni,[status(thm)],[256:[bind(A,$thf( ^ [C: $i] : ( cP @ ( f @ C ) ) )),bind(B,$thf( sk2 @ cP ))]]) ).
thf(276,plain,
( ~ $true
| ( ( sk1
@ ^ [A: $i] : ( cP @ ( f @ A ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[268,141]) ).
thf(277,plain,
( ( sk1
@ ^ [A: $i] : ( cP @ ( f @ A ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[276]) ).
thf(287,plain,
( ( ^ [A: $i] : ( cP @ ( f @ A ) ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[277]) ).
thf(288,plain,
cP @ ( f @ sk4 ),
inference(func_ext,[status(esa)],[287]) ).
thf(5347,plain,
( ~ $true
| ( ( cP @ ( f @ sk12 ) )
!= ( cP @ ( f @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[288,5346]) ).
thf(5348,plain,
( ( cP @ ( f @ sk12 ) )
!= ( cP @ ( f @ sk4 ) ) ),
inference(simp,[status(thm)],[5347]) ).
thf(5375,plain,
( ( f @ sk12 )
!= ( f @ sk4 ) ),
inference(simp,[status(thm)],[5348]) ).
thf(186,plain,
( ~ $true
| ( ( sk1 @ cP )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[180,141]) ).
thf(187,plain,
( ( sk1 @ cP )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[186]) ).
thf(196,plain,
( cP
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[187]) ).
thf(198,plain,
cP @ sk3,
inference(func_ext,[status(esa)],[196]) ).
thf(5365,plain,
( ~ $true
| ( ( cP @ ( f @ sk12 ) )
!= ( cP @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[198,5346]) ).
thf(5366,plain,
( ( cP @ ( f @ sk12 ) )
!= ( cP @ sk3 ) ),
inference(simp,[status(thm)],[5365]) ).
thf(5379,plain,
( ( f @ sk12 )
!= sk3 ),
inference(simp,[status(thm)],[5366]) ).
thf(10432,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( B != sk3 )
| ( A
!= ( f @ sk12 ) ) ),
inference(paramod_ordered,[status(thm)],[352,5379]) ).
thf(10433,plain,
! [A: $i] :
( ( sk1 @ ( (=) @ $i @ ( f @ sk12 ) ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[10432:[bind(A,$thf( f @ sk12 )),bind(B,$thf( B ))]]) ).
thf(11198,plain,
sk1 @ ( (=) @ $i @ ( f @ sk12 ) ),
inference(simp,[status(thm)],[10433]) ).
thf(15624,plain,
( ~ $true
| ( ( sk1 @ ( (=) @ $i @ ( f @ sk12 ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[11198,141]) ).
thf(15625,plain,
( ( sk1 @ ( (=) @ $i @ ( f @ sk12 ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[15624]) ).
thf(15785,plain,
( ( (=) @ $i @ ( f @ sk12 ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[15625]) ).
thf(20897,plain,
( ( f @ sk12 )
= sk26 ),
inference(func_ext,[status(esa)],[15785]) ).
thf(20901,plain,
( ( f @ sk12 )
= sk26 ),
inference(lifteq,[status(thm)],[20897]) ).
thf(20904,plain,
( ( f @ sk4 )
!= sk26 ),
inference(rewrite,[status(thm)],[5375,20901]) ).
thf(10472,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A
!= ( f @ sk4 ) )
| ( B
!= ( f @ sk12 ) ) ),
inference(paramod_ordered,[status(thm)],[352,5375]) ).
thf(10473,plain,
! [A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A
!= ( f @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[10472:[bind(A,$thf( A )),bind(B,$thf( f @ sk12 ))]]) ).
thf(11215,plain,
sk1 @ ( (=) @ $i @ ( f @ sk4 ) ),
inference(simp,[status(thm)],[10473]) ).
thf(16243,plain,
( ~ $true
| ( ( sk1 @ ( (=) @ $i @ ( f @ sk4 ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[11215,141]) ).
thf(16244,plain,
( ( sk1 @ ( (=) @ $i @ ( f @ sk4 ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[16243]) ).
thf(16334,plain,
( ( (=) @ $i @ ( f @ sk4 ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[16244]) ).
thf(23241,plain,
( ( f @ sk4 )
= sk31 ),
inference(func_ext,[status(esa)],[16334]) ).
thf(23246,plain,
( ( f @ sk4 )
= sk31 ),
inference(lifteq,[status(thm)],[23241]) ).
thf(23897,plain,
sk31 != sk26,
inference(rewrite,[status(thm)],[20904,23246]) ).
thf(2945,plain,
( ~ $true
| ( ( cP @ ( sk2 @ cP ) )
!= ( cP @ ( f @ sk8 ) ) ) ),
inference(paramod_ordered,[status(thm)],[2811,58]) ).
thf(2946,plain,
( ( cP @ ( sk2 @ cP ) )
!= ( cP @ ( f @ sk8 ) ) ),
inference(simp,[status(thm)],[2945]) ).
thf(2982,plain,
( ( sk2 @ cP )
!= ( f @ sk8 ) ),
inference(simp,[status(thm)],[2946]) ).
thf(10458,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A
!= ( f @ sk8 ) )
| ( B
!= ( sk2 @ cP ) ) ),
inference(paramod_ordered,[status(thm)],[352,2982]) ).
thf(10459,plain,
! [A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A
!= ( f @ sk8 ) ) ),
inference(pattern_uni,[status(thm)],[10458:[bind(A,$thf( A )),bind(B,$thf( sk2 @ cP ))]]) ).
thf(11208,plain,
sk1 @ ( (=) @ $i @ ( f @ sk8 ) ),
inference(simp,[status(thm)],[10459]) ).
thf(16014,plain,
( ~ $true
| ( ( sk1 @ ( (=) @ $i @ ( f @ sk8 ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[11208,141]) ).
thf(16015,plain,
( ( sk1 @ ( (=) @ $i @ ( f @ sk8 ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[16014]) ).
thf(16148,plain,
( ( (=) @ $i @ ( f @ sk8 ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[16015]) ).
thf(23233,plain,
( ( f @ sk8 )
= sk30 ),
inference(func_ext,[status(esa)],[16148]) ).
thf(23238,plain,
( ( f @ sk8 )
= sk30 ),
inference(lifteq,[status(thm)],[23233]) ).
thf(23255,plain,
( ( (=) @ $i @ sk30 )
!= ( ^ [A: $i] : $false ) ),
inference(rewrite,[status(thm)],[16148,23238]) ).
thf(23896,plain,
( ( (=) @ $i @ sk31 )
!= ( ^ [A: $i] : $false ) ),
inference(rewrite,[status(thm)],[16334,23246]) ).
thf(24964,plain,
sk31 = sk34,
inference(func_ext,[status(esa)],[23896]) ).
thf(24966,plain,
sk34 = sk31,
inference(lifteq,[status(thm)],[24964]) ).
thf(1182,plain,
( ~ $true
| ( ( sk1
@ ^ [A: $i] :
~ ( cP @ A ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[1109,141]) ).
thf(1183,plain,
( ( sk1
@ ^ [A: $i] :
~ ( cP @ A ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[1182]) ).
thf(1205,plain,
( ( ^ [A: $i] :
~ ( cP @ A ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[1183]) ).
thf(1220,plain,
~ ( cP @ sk6 ),
inference(func_ext,[status(esa)],[1205]) ).
thf(1221,plain,
~ ( cP @ sk6 ),
inference(cnf,[status(esa)],[1220]) ).
thf(3619,plain,
( ~ $true
| ( ( cP @ sk9 )
!= ( cP @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[3487,1221]) ).
thf(3620,plain,
( ( cP @ sk9 )
!= ( cP @ sk6 ) ),
inference(simp,[status(thm)],[3619]) ).
thf(3644,plain,
sk9 != sk6,
inference(simp,[status(thm)],[3620]) ).
thf(10398,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A != sk6 )
| ( B != sk9 ) ),
inference(paramod_ordered,[status(thm)],[352,3644]) ).
thf(10399,plain,
! [A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A != sk6 ) ),
inference(pattern_uni,[status(thm)],[10398:[bind(A,$thf( A )),bind(B,$thf( sk9 ))]]) ).
thf(11186,plain,
sk1 @ ( (=) @ $i @ sk6 ),
inference(simp,[status(thm)],[10399]) ).
thf(12332,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk6 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11186,5]) ).
thf(12333,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1 @ ( (=) @ $i @ sk6 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[12332]) ).
thf(12334,plain,
~ ( cP @ ( sk2 @ ( (=) @ $i @ sk6 ) ) ),
inference(pattern_uni,[status(thm)],[12333:[bind(A,$thf( (=) @ $i @ sk6 ))]]) ).
thf(101,plain,
! [C: $i > $o,B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( C @ ( f @ ( sk2 @ C ) ) )
| ~ $true
| ( ( sk1 @ A )
!= ( sk1 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[11,7]) ).
thf(102,plain,
! [C: $i > $o,B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( C @ ( f @ ( sk2 @ C ) ) )
| ( ( sk1 @ A )
!= ( sk1 @ C ) ) ),
inference(simp,[status(thm)],[101]) ).
thf(103,plain,
! [B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( A @ ( f @ ( sk2 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[102:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A ))]]) ).
thf(120,plain,
! [A: $i] :
( ( A != A )
| ( A
= ( f @ ( sk2 @ ( (=) @ $i @ A ) ) ) ) ),
inference(replace_leibeq,[status(thm)],[103:[bind(A,$thf( (=) @ $i @ B ))]]) ).
thf(121,plain,
! [A: $i] :
( ( A != A )
| ( A
= ( f @ ( sk2 @ ( (=) @ $i @ A ) ) ) ) ),
inference(lifteq,[status(thm)],[120]) ).
thf(123,plain,
! [A: $i] :
( A
= ( f @ ( sk2 @ ( (=) @ $i @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[121:[]]) ).
thf(146,plain,
! [A: $i] :
( A
= ( f @ ( sk2 @ ( (=) @ $i @ A ) ) ) ),
inference(simp,[status(thm)],[123]) ).
thf(2935,plain,
( ~ $true
| ( ( cP @ ( f @ sk8 ) )
!= ( cP @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[2811,1221]) ).
thf(2936,plain,
( ( cP @ ( f @ sk8 ) )
!= ( cP @ sk6 ) ),
inference(simp,[status(thm)],[2935]) ).
thf(2955,plain,
( ( f @ sk8 )
!= sk6 ),
inference(simp,[status(thm)],[2936]) ).
thf(6697,plain,
! [A: $i] :
( ( A != sk6 )
| ( ( f @ ( sk2 @ ( (=) @ $i @ A ) ) )
!= ( f @ sk8 ) ) ),
inference(paramod_ordered,[status(thm)],[146,2955]) ).
thf(6868,plain,
( ( sk2 @ ( (=) @ $i @ sk6 ) )
!= sk8 ),
inference(simp,[status(thm)],[6697]) ).
thf(282,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ~ $true
| ( ( sk1
@ ^ [B: $i] : ( cP @ ( f @ B ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[268,7]) ).
thf(283,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ( ( sk1
@ ^ [B: $i] : ( cP @ ( f @ B ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[282]) ).
thf(284,plain,
( cP
@ ( f
@ ( f
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ A ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[283:[bind(A,$thf( ^ [B: $i] : ( cP @ ( f @ B ) ) ))]]) ).
thf(723,plain,
! [B: $i,A: $i > $o] :
( ~ $true
| ~ ( cP @ ( sk2 @ A ) )
| ( ( cP
@ ( f
@ ( f
@ ( sk2
@ ^ [C: $i] : ( cP @ ( f @ C ) ) ) ) ) )
!= ( A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[284,17]) ).
thf(724,plain,
! [B: $i,A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( cP
@ ( f
@ ( f
@ ( sk2
@ ^ [C: $i] : ( cP @ ( f @ C ) ) ) ) ) )
!= ( A @ B ) ) ),
inference(simp,[status(thm)],[723]) ).
thf(741,plain,
~ ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) ) ),
inference(pre_uni,[status(thm)],[724:[bind(A,$thf( ^ [C: $i] : ( cP @ ( f @ ( f @ C ) ) ) )),bind(B,$thf( sk2 @ ^ [C: $i] : ( cP @ ( f @ C ) ) ))]]) ).
thf(1261,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) ) )
!= ( cP @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[198,1190]) ).
thf(1262,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) ) )
!= ( cP @ sk3 ) ),
inference(simp,[status(thm)],[1261]) ).
thf(1275,plain,
( ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) )
!= sk3 ),
inference(simp,[status(thm)],[1262]) ).
thf(10335,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A != sk3 )
| ( B
!= ( sk2
@ ^ [C: $i] :
~ ( cP @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[352,1275]) ).
thf(10336,plain,
! [A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A != sk3 ) ),
inference(pattern_uni,[status(thm)],[10335:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ^ [C: $i] : ~ ( cP @ C ) ))]]) ).
thf(11165,plain,
sk1 @ ( (=) @ $i @ sk3 ),
inference(simp,[status(thm)],[10336]) ).
thf(11483,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( sk1 @ ( (=) @ $i @ A ) )
| ( B != sk3 ) ),
inference(paramod_ordered,[status(thm)],[352,11165]) ).
thf(11484,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( B != sk3 ) ),
inference(simp,[status(thm)],[11483]) ).
thf(11485,plain,
! [A: $i] : ( sk1 @ ( (=) @ $i @ A ) ),
inference(pattern_uni,[status(thm)],[11484:[bind(A,$thf( A )),bind(B,$thf( sk3 ))]]) ).
thf(259,plain,
! [B: $i,A: $i > $o] :
( ~ $true
| ~ ( cP @ ( sk2 @ A ) )
| ( ( cP @ ( f @ ( sk2 @ cP ) ) )
!= ( A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[190,17]) ).
thf(260,plain,
! [B: $i,A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( cP @ ( f @ ( sk2 @ cP ) ) )
!= ( A @ B ) ) ),
inference(simp,[status(thm)],[259]) ).
thf(264,plain,
~ ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ A ) ) ) ),
inference(pre_uni,[status(thm)],[260:[bind(A,$thf( ^ [C: $i] : ( cP @ ( f @ C ) ) )),bind(B,$thf( sk2 @ cP ))]]) ).
thf(441,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ A ) ) ) )
!= ( cP @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[198,264]) ).
thf(442,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ A ) ) ) )
!= ( cP @ sk3 ) ),
inference(simp,[status(thm)],[441]) ).
thf(449,plain,
( ( sk2
@ ^ [A: $i] : ( cP @ ( f @ A ) ) )
!= sk3 ),
inference(simp,[status(thm)],[442]) ).
thf(25,plain,
! [B: $i > $i,A: $i] :
( ( sk1
@ ^ [C: $i] : ( cP @ ( B @ C ) ) )
| ~ ( cP @ ( B @ A ) ) ),
inference(prim_subst,[status(thm)],[11:[bind(A,$thf( ^ [D: $i] : ( cP @ ( C @ D ) ) ))]]) ).
thf(34,plain,
! [B: $i > $i,A: $i] :
( ( sk1
@ ^ [C: $i] : ( cP @ ( B @ C ) ) )
| ~ ( cP @ ( B @ A ) ) ),
inference(simp,[status(thm)],[25]) ).
thf(465,plain,
! [D: $i,C: $i > $o,B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ( sk1 @ C )
| ~ $true
| ( ( sk1
@ ^ [E: $i] : ( cP @ ( B @ E ) ) )
!= ( C @ D ) ) ),
inference(paramod_ordered,[status(thm)],[34,11]) ).
thf(466,plain,
! [D: $i,C: $i > $o,B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ( sk1 @ C )
| ( ( sk1
@ ^ [E: $i] : ( cP @ ( B @ E ) ) )
!= ( C @ D ) ) ),
inference(simp,[status(thm)],[465]) ).
thf(489,plain,
! [C: $i > $i > $i,B: $i,A: $i] :
( ~ ( cP @ ( C @ B @ A ) )
| ( sk1
@ ^ [D: $i] :
( sk1
@ ^ [E: $i] : ( cP @ ( C @ D @ E ) ) ) ) ),
inference(pre_uni,[status(thm)],[466:[bind(A,$thf( A )),bind(B,$thf( F @ D )),bind(C,$thf( ^ [F: $i] : ( sk1 @ ^ [G: $i] : ( cP @ ( F @ F @ G ) ) ) )),bind(D,$thf( D ))]]) ).
thf(500,plain,
! [C: $i > $i > $i,B: $i,A: $i] :
( ~ ( cP @ ( C @ B @ A ) )
| ( sk1
@ ^ [D: $i] :
( sk1
@ ^ [E: $i] : ( cP @ ( C @ D @ E ) ) ) ) ),
inference(simp,[status(thm)],[489]) ).
thf(437,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ A ) ) ) )
!= ( cP @ a ) ) ),
inference(paramod_ordered,[status(thm)],[159,264]) ).
thf(438,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ A ) ) ) )
!= ( cP @ a ) ),
inference(simp,[status(thm)],[437]) ).
thf(448,plain,
( ( sk2
@ ^ [A: $i] : ( cP @ ( f @ A ) ) )
!= a ),
inference(simp,[status(thm)],[438]) ).
thf(10414,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A != a )
| ( B
!= ( sk2
@ ^ [C: $i] : ( cP @ ( f @ C ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[352,448]) ).
thf(10415,plain,
! [A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A != a ) ),
inference(pattern_uni,[status(thm)],[10414:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ^ [C: $i] : ( cP @ ( f @ C ) ) ))]]) ).
thf(11191,plain,
sk1 @ ( (=) @ $i @ a ),
inference(simp,[status(thm)],[10415]) ).
thf(12492,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ~ $true
| ( ( sk1 @ ( (=) @ $i @ a ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11191,5]) ).
thf(12493,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1 @ ( (=) @ $i @ a ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[12492]) ).
thf(12494,plain,
~ ( cP @ ( sk2 @ ( (=) @ $i @ a ) ) ),
inference(pattern_uni,[status(thm)],[12493:[bind(A,$thf( (=) @ $i @ a ))]]) ).
thf(28,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
| ~ ( ( B @ A )
| ( C @ A ) ) ),
inference(prim_subst,[status(thm)],[11:[bind(A,$thf( ^ [E: $i] : ( ( C @ E ) | ( D @ E ) ) ))]]) ).
thf(37,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
| ~ ( B @ A ) )
& ( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
| ~ ( C @ A ) ) ),
inference(cnf,[status(esa)],[28]) ).
thf(38,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
| ~ ( B @ A ) ),
inference(cnfConj,[status(thm)],[37]) ).
thf(40,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
| ~ ( B @ A ) ),
inference(simp,[status(thm)],[38]) ).
thf(640,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] :
( ~ ( C @ D )
| ( B @ D ) ) )
| ~ ~ ( C @ A ) ),
inference(prim_subst,[status(thm)],[40:[bind(A,$thf( A )),bind(B,$thf( ^ [E: $i] : ~ ( D @ E ) ))]]) ).
thf(669,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] :
( ~ ( C @ D )
| ( B @ D ) ) )
| ( C @ A ) ),
inference(cnf,[status(esa)],[640]) ).
thf(670,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] :
( ~ ( C @ D )
| ( B @ D ) ) )
| ( C @ A ) ),
inference(simp,[status(thm)],[669]) ).
thf(10456,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( B
!= ( f @ sk8 ) )
| ( A
!= ( sk2 @ cP ) ) ),
inference(paramod_ordered,[status(thm)],[352,2982]) ).
thf(10457,plain,
! [A: $i] :
( ( sk1 @ ( (=) @ $i @ ( sk2 @ cP ) ) )
| ( A
!= ( f @ sk8 ) ) ),
inference(pattern_uni,[status(thm)],[10456:[bind(A,$thf( sk2 @ cP )),bind(B,$thf( B ))]]) ).
thf(11207,plain,
sk1 @ ( (=) @ $i @ ( sk2 @ cP ) ),
inference(simp,[status(thm)],[10457]) ).
thf(15831,plain,
( ~ $true
| ( ( sk1 @ ( (=) @ $i @ ( sk2 @ cP ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[11207,141]) ).
thf(15832,plain,
( ( sk1 @ ( (=) @ $i @ ( sk2 @ cP ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[15831]) ).
thf(15971,plain,
( ( (=) @ $i @ ( sk2 @ cP ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[15832]) ).
thf(21441,plain,
( ( sk2 @ cP )
= sk28 ),
inference(func_ext,[status(esa)],[15971]) ).
thf(21443,plain,
( ( sk2 @ cP )
= sk28 ),
inference(lifteq,[status(thm)],[21441]) ).
thf(21445,plain,
( ( f @ sk8 )
!= sk28 ),
inference(rewrite,[status(thm)],[2982,21443]) ).
thf(23251,plain,
sk30 != sk28,
inference(rewrite,[status(thm)],[21445,23238]) ).
thf(20908,plain,
( ( (=) @ $i @ sk26 )
!= ( ^ [A: $i] : $false ) ),
inference(rewrite,[status(thm)],[15785,20901]) ).
thf(21396,plain,
sk26 = sk27,
inference(func_ext,[status(esa)],[20908]) ).
thf(21398,plain,
sk27 = sk26,
inference(lifteq,[status(thm)],[21396]) ).
thf(26,plain,
! [B: $i > $i > $o,A: $i] :
( ( sk1
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) )
| ~ ( sk1 @ ( B @ A ) ) ),
inference(prim_subst,[status(thm)],[11:[bind(A,$thf( ^ [D: $i] : ( sk1 @ ( C @ D ) ) ))]]) ).
thf(35,plain,
! [B: $i > $i > $o,A: $i] :
( ( sk1
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) )
| ~ ( sk1 @ ( B @ A ) ) ),
inference(simp,[status(thm)],[26]) ).
thf(543,plain,
! [C: $i > $o,B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ( C @ ( f @ ( sk2 @ C ) ) )
| ~ $true
| ( ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) ) )
!= ( sk1 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[35,7]) ).
thf(544,plain,
! [C: $i > $o,B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ( C @ ( f @ ( sk2 @ C ) ) )
| ( ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) ) )
!= ( sk1 @ C ) ) ),
inference(simp,[status(thm)],[543]) ).
thf(545,plain,
! [B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ( sk1
@ ( B
@ ( f
@ ( sk2
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[544:[bind(A,$thf( A )),bind(B,$thf( D )),bind(C,$thf( ^ [E: $i] : ( sk1 @ ( D @ E ) ) ))]]) ).
thf(565,plain,
! [B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ( sk1
@ ( B
@ ( f
@ ( sk2
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[545]) ).
thf(11486,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk3 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11165,5]) ).
thf(11487,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1 @ ( (=) @ $i @ sk3 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[11486]) ).
thf(11488,plain,
~ ( cP @ ( sk2 @ ( (=) @ $i @ sk3 ) ) ),
inference(pattern_uni,[status(thm)],[11487:[bind(A,$thf( (=) @ $i @ sk3 ))]]) ).
thf(14516,plain,
( ~ $true
| ( ( cP @ ( sk2 @ ( (=) @ $i @ sk3 ) ) )
!= ( cP @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[3487,11488]) ).
thf(14517,plain,
( ( cP @ ( sk2 @ ( (=) @ $i @ sk3 ) ) )
!= ( cP @ sk9 ) ),
inference(simp,[status(thm)],[14516]) ).
thf(14553,plain,
( ( sk2 @ ( (=) @ $i @ sk3 ) )
!= sk9 ),
inference(simp,[status(thm)],[14517]) ).
thf(2326,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ~ $true
| ( ( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] :
( sk1
@ ^ [D: $i] : ( cP @ B ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1615,5]) ).
thf(2327,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] :
( sk1
@ ^ [D: $i] : ( cP @ B ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[2326]) ).
thf(2328,plain,
~ ( cP
@ ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ A ) ) ) ) ),
inference(pattern_uni,[status(thm)],[2327:[bind(A,$thf( ^ [B: $i] : ( sk1 @ ^ [C: $i] : ( sk1 @ ^ [D: $i] : ( cP @ B ) ) ) ))]]) ).
thf(1321,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ~ $true
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( ( cP @ a )
!= ( C @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[159,45]) ).
thf(1322,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( ( cP @ a )
!= ( C @ B @ A ) ) ),
inference(simp,[status(thm)],[1321]) ).
thf(1369,plain,
( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ a ) ) ),
inference(pre_uni,[status(thm)],[1322:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( ^ [D: $i] : ^ [E: $i] : ( cP @ a ) ))]]) ).
thf(2039,plain,
( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : $true ) ),
inference(rewrite,[status(thm)],[1369,159]) ).
thf(471,plain,
! [D: $i,C: $i > $o,B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ( sk1 @ C )
| ( ( ~ $true )
!= ( C @ D ) )
| ( ( sk1
@ ^ [E: $i] : ( cP @ ( B @ E ) ) )
!= ( sk1 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[34,32]) ).
thf(472,plain,
! [D: $i,C: $i > $o,B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ( sk1 @ C )
| ( C @ D )
| ( ( sk1
@ ^ [E: $i] : ( cP @ ( B @ E ) ) )
!= ( sk1 @ C ) ) ),
inference(simp,[status(thm)],[471]) ).
thf(473,plain,
! [C: $i > $i,B: $i,A: $i] :
( ~ ( cP @ ( C @ A ) )
| ( sk1
@ ^ [D: $i] : ( cP @ ( C @ D ) ) )
| ( cP @ ( C @ B ) ) ),
inference(pattern_uni,[status(thm)],[472:[bind(A,$thf( A )),bind(B,$thf( E )),bind(C,$thf( ^ [F: $i] : ( cP @ ( E @ F ) ) ))]]) ).
thf(504,plain,
! [C: $i > $i,B: $i,A: $i] :
( ~ ( cP @ ( C @ A ) )
| ( sk1
@ ^ [D: $i] : ( cP @ ( C @ D ) ) )
| ( cP @ ( C @ B ) ) ),
inference(simp,[status(thm)],[473]) ).
thf(56,plain,
( ~ $true
| ~ ( cP
@ ( sk2
@ ^ [A: $i] : $true ) ) ),
inference(prim_subst,[status(thm)],[17:[bind(A,$thf( ^ [C: $i] : $true ))]]) ).
thf(69,plain,
~ ( cP
@ ( sk2
@ ^ [A: $i] : $true ) ),
inference(simp,[status(thm)],[56]) ).
thf(2898,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] : $true ) )
!= ( cP @ ( f @ sk8 ) ) ) ),
inference(paramod_ordered,[status(thm)],[2811,69]) ).
thf(2899,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] : $true ) )
!= ( cP @ ( f @ sk8 ) ) ),
inference(simp,[status(thm)],[2898]) ).
thf(2990,plain,
( ( sk2
@ ^ [A: $i] : $true )
!= ( f @ sk8 ) ),
inference(simp,[status(thm)],[2899]) ).
thf(10544,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( B
!= ( f @ sk8 ) )
| ( A
!= ( sk2
@ ^ [C: $i] : $true ) ) ),
inference(paramod_ordered,[status(thm)],[352,2990]) ).
thf(10545,plain,
! [A: $i] :
( ( sk1
@ ( (=) @ $i
@ ( sk2
@ ^ [B: $i] : $true ) ) )
| ( A
!= ( f @ sk8 ) ) ),
inference(pattern_uni,[status(thm)],[10544:[bind(A,$thf( sk2 @ ^ [C: $i] : $true )),bind(B,$thf( B ))]]) ).
thf(11242,plain,
( sk1
@ ( (=) @ $i
@ ( sk2
@ ^ [A: $i] : $true ) ) ),
inference(simp,[status(thm)],[10545]) ).
thf(16549,plain,
( ~ $true
| ( ( sk1
@ ( (=) @ $i
@ ( sk2
@ ^ [A: $i] : $true ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[11242,141]) ).
thf(16550,plain,
( ( sk1
@ ( (=) @ $i
@ ( sk2
@ ^ [A: $i] : $true ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[16549]) ).
thf(16656,plain,
( ( (=) @ $i
@ ( sk2
@ ^ [A: $i] : $true ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[16550]) ).
thf(25061,plain,
( ( sk2
@ ^ [A: $i] : $true )
= sk35 ),
inference(func_ext,[status(esa)],[16656]) ).
thf(25073,plain,
( ( sk2
@ ^ [A: $i] : $true )
= sk35 ),
inference(lifteq,[status(thm)],[25061]) ).
thf(25090,plain,
~ ( cP @ sk35 ),
inference(rewrite,[status(thm)],[69,25073]) ).
thf(1593,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ~ $true
| ( ( sk1
@ ^ [B: $i] : ( cP @ sk7 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1468,7]) ).
thf(1594,plain,
! [A: $i > $o] :
( ( A @ ( f @ ( sk2 @ A ) ) )
| ( ( sk1
@ ^ [B: $i] : ( cP @ sk7 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[1593]) ).
thf(1595,plain,
cP @ sk7,
inference(pattern_uni,[status(thm)],[1594:[bind(A,$thf( ^ [B: $i] : ( cP @ sk7 ) ))]]) ).
thf(1433,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ~ $true
| ( ( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ B ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1357,5]) ).
thf(1434,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ B ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[1433]) ).
thf(1435,plain,
~ ( cP
@ ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[1434:[bind(A,$thf( ^ [B: $i] : ( sk1 @ ^ [C: $i] : ( cP @ B ) ) ))]]) ).
thf(1761,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) ) )
!= ( cP @ sk7 ) ) ),
inference(paramod_ordered,[status(thm)],[1595,1435]) ).
thf(1762,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) ) )
!= ( cP @ sk7 ) ),
inference(simp,[status(thm)],[1761]) ).
thf(1792,plain,
( ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) )
!= sk7 ),
inference(simp,[status(thm)],[1762]) ).
thf(39,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
| ~ ( C @ A ) ),
inference(cnfConj,[status(thm)],[37]) ).
thf(41,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
| ~ ( C @ A ) ),
inference(simp,[status(thm)],[39]) ).
thf(796,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
| ~ $true
| ( ( cP @ ( f @ sk4 ) )
!= ( C @ A ) ) ),
inference(paramod_ordered,[status(thm)],[288,41]) ).
thf(797,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
| ( ( cP @ ( f @ sk4 ) )
!= ( C @ A ) ) ),
inference(simp,[status(thm)],[796]) ).
thf(856,plain,
! [A: $i > $o] :
( sk1
@ ^ [B: $i] :
( ( A @ B )
| ( cP @ B ) ) ),
inference(pre_uni,[status(thm)],[797:[bind(A,$thf( f @ sk4 )),bind(B,$thf( B )),bind(C,$thf( cP ))]]) ).
thf(902,plain,
! [A: $i > $o] :
( sk1
@ ^ [B: $i] :
( ( A @ B )
| ( cP @ B ) ) ),
inference(simp,[status(thm)],[856]) ).
thf(257,plain,
( ~ $true
| ( ( cP @ ( f @ ( sk2 @ cP ) ) )
!= ( cP @ ( sk2 @ cP ) ) ) ),
inference(paramod_ordered,[status(thm)],[190,58]) ).
thf(258,plain,
( ( cP @ ( f @ ( sk2 @ cP ) ) )
!= ( cP @ ( sk2 @ cP ) ) ),
inference(simp,[status(thm)],[257]) ).
thf(270,plain,
( ( f @ ( sk2 @ cP ) )
!= ( sk2 @ cP ) ),
inference(simp,[status(thm)],[258]) ).
thf(21447,plain,
( ( f @ sk28 )
!= sk28 ),
inference(rewrite,[status(thm)],[270,21443]) ).
thf(97,plain,
! [B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ( B @ ( f @ ( sk2 @ B ) ) )
| ~ $true
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( sk1 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[7,7]) ).
thf(98,plain,
! [B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ( B @ ( f @ ( sk2 @ B ) ) )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( sk1 @ B ) ) ),
inference(simp,[status(thm)],[97]) ).
thf(132,plain,
! [A: $i > $i > $o] :
( ~ ( sk1
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) )
| ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) )
@ ( f
@ ( sk2
@ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[98:[bind(A,$thf( ^ [D: $i] : ( sk1 @ ( C @ D ) ) )),bind(B,$thf( C @ ( f @ ( sk2 @ ^ [D: $i] : ( sk1 @ ( C @ D ) ) ) ) ))]]) ).
thf(136,plain,
! [A: $i > $i > $o] :
( ~ ( sk1
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) )
| ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) )
@ ( f
@ ( sk2
@ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[132]) ).
thf(4263,plain,
! [A: $i > $i > $o] :
( ~ $true
| ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) )
@ ( f
@ ( sk2
@ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) ) ) ) ) )
| ( ( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ B ) ) )
!= ( sk1
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1357,136]) ).
thf(4264,plain,
! [A: $i > $i > $o] :
( ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) )
@ ( f
@ ( sk2
@ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) ) ) ) ) )
| ( ( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ B ) ) )
!= ( sk1
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) ) ),
inference(simp,[status(thm)],[4263]) ).
thf(4265,plain,
( cP
@ ( f
@ ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) ) ) ),
inference(pattern_uni,[status(thm)],[4264:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ( cP @ B ) ))]]) ).
thf(1749,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ A ) ) ) )
!= ( cP @ sk7 ) ) ),
inference(paramod_ordered,[status(thm)],[1595,264]) ).
thf(1750,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ A ) ) ) )
!= ( cP @ sk7 ) ),
inference(simp,[status(thm)],[1749]) ).
thf(1773,plain,
( ( sk2
@ ^ [A: $i] : ( cP @ ( f @ A ) ) )
!= sk7 ),
inference(simp,[status(thm)],[1750]) ).
thf(3582,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) ) )
!= ( cP @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[3487,1190]) ).
thf(3583,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) ) )
!= ( cP @ sk9 ) ),
inference(simp,[status(thm)],[3582]) ).
thf(3670,plain,
( ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) )
!= sk9 ),
inference(simp,[status(thm)],[3583]) ).
thf(633,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
| ( ( B @ A )
!= ( ~ ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[40]) ).
thf(646,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
| ( ( B @ A )
!= ( ~ ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) ) ) ) ),
inference(simp,[status(thm)],[633]) ).
thf(12500,plain,
( ~ $true
| ( ( sk1 @ ( (=) @ $i @ a ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[11191,141]) ).
thf(12501,plain,
( ( sk1 @ ( (=) @ $i @ a ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[12500]) ).
thf(12610,plain,
( ( (=) @ $i @ a )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[12501]) ).
thf(21459,plain,
cP @ ( f @ sk28 ),
inference(rewrite,[status(thm)],[190,21443]) ).
thf(202,plain,
! [A: $i > $o] :
( ~ $true
| ~ ( sk1 @ A )
| ( ( cP @ ( sk2 @ A ) )
!= ( cP @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[198,5]) ).
thf(203,plain,
! [A: $i > $o] :
( ~ ( sk1 @ A )
| ( ( cP @ ( sk2 @ A ) )
!= ( cP @ sk3 ) ) ),
inference(simp,[status(thm)],[202]) ).
thf(218,plain,
! [A: $i > $o] :
( ~ ( sk1 @ A )
| ( ( sk2 @ A )
!= sk3 ) ),
inference(simp,[status(thm)],[203]) ).
thf(11478,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk3 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11165,218]) ).
thf(11479,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk3 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[11478]) ).
thf(11480,plain,
( ( sk2 @ ( (=) @ $i @ sk3 ) )
!= sk3 ),
inference(pattern_uni,[status(thm)],[11479:[bind(A,$thf( (=) @ $i @ sk3 ))]]) ).
thf(51,plain,
! [B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ~ ( cP
@ ( sk2
@ ^ [C: $i] : ( cP @ ( B @ C ) ) ) ) ),
inference(prim_subst,[status(thm)],[17:[bind(A,$thf( ^ [D: $i] : ( cP @ ( C @ D ) ) ))]]) ).
thf(61,plain,
! [B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ~ ( cP
@ ( sk2
@ ^ [C: $i] : ( cP @ ( B @ C ) ) ) ) ),
inference(simp,[status(thm)],[51]) ).
thf(1614,plain,
( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ sk7 ) ) ) ),
inference(pre_uni,[status(thm)],[1583:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( ^ [D: $i] : ^ [E: $i] : ( sk1 @ ^ [F: $i] : ( cP @ sk7 ) ) ))]]) ).
thf(6932,plain,
( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : $true ) ) ),
inference(rewrite,[status(thm)],[1614,1595]) ).
thf(6,plain,
! [C: $i,B: $i,A: $i > $o] :
( ( sk1 @ A )
| ( ( f @ B )
!= ( f @ C ) )
| ( B = C ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(10,plain,
! [C: $i,B: $i,A: $i > $o] :
( ( ( f @ B )
!= ( f @ C ) )
| ( B = C )
| ( sk1 @ A ) ),
inference(lifteq,[status(thm)],[6]) ).
thf(228,plain,
! [C: $i,B: $i,A: $i > $o] :
( ( ( f @ B )
!= ( f @ C ) )
| ( B = C )
| ~ $true
| ( ( sk1 @ A )
!= ( sk1
@ ^ [D: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[10,141]) ).
thf(229,plain,
! [C: $i,B: $i,A: $i > $o] :
( ( ( f @ B )
!= ( f @ C ) )
| ( B = C )
| ( ( sk1 @ A )
!= ( sk1
@ ^ [D: $i] : $false ) ) ),
inference(simp,[status(thm)],[228]) ).
thf(230,plain,
! [B: $i,A: $i] :
( ( ( f @ A )
!= ( f @ B ) )
| ( A = B ) ),
inference(pattern_uni,[status(thm)],[229:[bind(A,$thf( ^ [D: $i] : $false ))]]) ).
thf(243,plain,
! [B: $i,A: $i] :
( ( ( f @ A )
!= ( f @ B ) )
| ( A = B ) ),
inference(simp,[status(thm)],[230]) ).
thf(5357,plain,
( ~ $true
| ( ( cP @ ( f @ sk12 ) )
!= ( cP @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[3487,5346]) ).
thf(5358,plain,
( ( cP @ ( f @ sk12 ) )
!= ( cP @ sk9 ) ),
inference(simp,[status(thm)],[5357]) ).
thf(5384,plain,
( ( f @ sk12 )
!= sk9 ),
inference(simp,[status(thm)],[5358]) ).
thf(20905,plain,
sk26 != sk9,
inference(rewrite,[status(thm)],[5384,20901]) ).
thf(20903,plain,
sk26 != sk3,
inference(rewrite,[status(thm)],[5379,20901]) ).
thf(21444,plain,
( ( (=) @ $i @ sk28 )
!= ( ^ [A: $i] : $false ) ),
inference(rewrite,[status(thm)],[15971,21443]) ).
thf(22384,plain,
sk28 = sk29,
inference(func_ext,[status(esa)],[21444]) ).
thf(22386,plain,
sk29 = sk28,
inference(lifteq,[status(thm)],[22384]) ).
thf(11532,plain,
! [B: $i > $i > $o,A: $i] :
( ( sk1
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) )
| ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk3 ) )
!= ( sk1 @ ( B @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[11165,35]) ).
thf(11533,plain,
! [B: $i > $i > $o,A: $i] :
( ( sk1
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) )
| ( ( sk1 @ ( (=) @ $i @ sk3 ) )
!= ( sk1 @ ( B @ A ) ) ) ),
inference(simp,[status(thm)],[11532]) ).
thf(11593,plain,
( sk1
@ ^ [A: $i] : ( sk1 @ ( (=) @ $i @ A ) ) ),
inference(pre_uni,[status(thm)],[11533:[bind(A,$thf( sk3 )),bind(B,$thf( (=) @ $i ))]]) ).
thf(15130,plain,
( ~ $true
| ( ( sk1
@ ^ [A: $i] : ( sk1 @ ( (=) @ $i @ A ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[11593,141]) ).
thf(15131,plain,
( ( sk1
@ ^ [A: $i] : ( sk1 @ ( (=) @ $i @ A ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[15130]) ).
thf(15248,plain,
( ( ^ [A: $i] : ( sk1 @ ( (=) @ $i @ A ) ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[15131]) ).
thf(15263,plain,
sk1 @ ( (=) @ $i @ sk21 ),
inference(func_ext,[status(esa)],[15248]) ).
thf(15400,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk21 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[15263,218]) ).
thf(15401,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk21 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[15400]) ).
thf(15402,plain,
( ( sk2 @ ( (=) @ $i @ sk21 ) )
!= sk3 ),
inference(pattern_uni,[status(thm)],[15401:[bind(A,$thf( (=) @ $i @ sk21 ))]]) ).
thf(1222,plain,
( ~ $true
| ( ( cP @ ( f @ sk4 ) )
!= ( cP @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[288,1221]) ).
thf(1223,plain,
( ( cP @ ( f @ sk4 ) )
!= ( cP @ sk6 ) ),
inference(simp,[status(thm)],[1222]) ).
thf(1240,plain,
( ( f @ sk4 )
!= sk6 ),
inference(simp,[status(thm)],[1223]) ).
thf(6746,plain,
! [A: $i] :
( ( A != sk6 )
| ( ( f @ ( sk2 @ ( (=) @ $i @ A ) ) )
!= ( f @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[146,1240]) ).
thf(6852,plain,
( ( sk2 @ ( (=) @ $i @ sk6 ) )
!= sk4 ),
inference(simp,[status(thm)],[6746]) ).
thf(10528,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A != sk4 )
| ( B
!= ( sk2 @ ( (=) @ $i @ sk6 ) ) ) ),
inference(paramod_ordered,[status(thm)],[352,6852]) ).
thf(10529,plain,
! [A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A != sk4 ) ),
inference(pattern_uni,[status(thm)],[10528:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ( (=) @ $i @ sk6 ) ))]]) ).
thf(11236,plain,
sk1 @ ( (=) @ $i @ sk4 ),
inference(simp,[status(thm)],[10529]) ).
thf(14272,plain,
( ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk4 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[11236,141]) ).
thf(14273,plain,
( ( sk1 @ ( (=) @ $i @ sk4 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[14272]) ).
thf(14375,plain,
( ( (=) @ $i @ sk4 )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[14273]) ).
thf(14439,plain,
sk4 = sk20,
inference(func_ext,[status(esa)],[14375]) ).
thf(14445,plain,
sk20 = sk4,
inference(lifteq,[status(thm)],[14439]) ).
thf(5351,plain,
( ~ $true
| ( ( cP @ ( f @ sk12 ) )
!= ( cP @ sk7 ) ) ),
inference(paramod_ordered,[status(thm)],[1595,5346]) ).
thf(5352,plain,
( ( cP @ ( f @ sk12 ) )
!= ( cP @ sk7 ) ),
inference(simp,[status(thm)],[5351]) ).
thf(5376,plain,
( ( f @ sk12 )
!= sk7 ),
inference(simp,[status(thm)],[5352]) ).
thf(6799,plain,
! [A: $i] :
( ( A != sk7 )
| ( ( f @ ( sk2 @ ( (=) @ $i @ A ) ) )
!= ( f @ sk12 ) ) ),
inference(paramod_ordered,[status(thm)],[146,5376]) ).
thf(6865,plain,
( ( sk2 @ ( (=) @ $i @ sk7 ) )
!= sk12 ),
inference(simp,[status(thm)],[6799]) ).
thf(10352,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( B != sk8 )
| ( A != sk12 ) ),
inference(paramod_ordered,[status(thm)],[352,6014]) ).
thf(10353,plain,
! [A: $i] :
( ( sk1 @ ( (=) @ $i @ sk12 ) )
| ( A != sk8 ) ),
inference(pattern_uni,[status(thm)],[10352:[bind(A,$thf( sk12 ))]]) ).
thf(11170,plain,
sk1 @ ( (=) @ $i @ sk12 ),
inference(simp,[status(thm)],[10353]) ).
thf(165,plain,
! [A: $i > $o] :
( ~ $true
| ~ ( sk1 @ A )
| ( ( cP @ ( sk2 @ A ) )
!= ( cP @ a ) ) ),
inference(paramod_ordered,[status(thm)],[159,5]) ).
thf(166,plain,
! [A: $i > $o] :
( ~ ( sk1 @ A )
| ( ( cP @ ( sk2 @ A ) )
!= ( cP @ a ) ) ),
inference(simp,[status(thm)],[165]) ).
thf(178,plain,
! [A: $i > $o] :
( ~ ( sk1 @ A )
| ( ( sk2 @ A )
!= a ) ),
inference(simp,[status(thm)],[166]) ).
thf(11728,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk12 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11170,178]) ).
thf(11729,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk12 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[11728]) ).
thf(11730,plain,
( ( sk2 @ ( (=) @ $i @ sk12 ) )
!= a ),
inference(pattern_uni,[status(thm)],[11729:[bind(A,$thf( (=) @ $i @ sk12 ))]]) ).
thf(12574,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ a ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11191,178]) ).
thf(12575,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ a ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[12574]) ).
thf(12576,plain,
( ( sk2 @ ( (=) @ $i @ a ) )
!= a ),
inference(pattern_uni,[status(thm)],[12575:[bind(A,$thf( (=) @ $i @ a ))]]) ).
thf(89,plain,
! [B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ~ ( cP @ ( sk2 @ B ) )
| ~ $true
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( sk1 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[7,5]) ).
thf(90,plain,
! [B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ~ ( cP @ ( sk2 @ B ) )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( sk1 @ B ) ) ),
inference(simp,[status(thm)],[89]) ).
thf(133,plain,
! [A: $i > $i > $o] :
( ~ ( sk1
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) )
| ~ ( cP
@ ( sk2
@ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[90:[bind(A,$thf( ^ [D: $i] : ( sk1 @ ( C @ D ) ) )),bind(B,$thf( C @ ( f @ ( sk2 @ ^ [D: $i] : ( sk1 @ ( C @ D ) ) ) ) ))]]) ).
thf(137,plain,
! [A: $i > $i > $o] :
( ~ ( sk1
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) )
| ~ ( cP
@ ( sk2
@ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[133]) ).
thf(24,plain,
! [A: $i] :
( ( sk1 @ cP )
| ~ ( cP @ A ) ),
inference(prim_subst,[status(thm)],[11:[bind(A,$thf( cP ))]]) ).
thf(33,plain,
! [A: $i] :
( ( sk1 @ cP )
| ~ ( cP @ A ) ),
inference(simp,[status(thm)],[24]) ).
thf(11814,plain,
( ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk8 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[11171,141]) ).
thf(11815,plain,
( ( sk1 @ ( (=) @ $i @ sk8 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[11814]) ).
thf(11906,plain,
( ( (=) @ $i @ sk8 )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[11815]) ).
thf(12644,plain,
sk8 = sk15,
inference(func_ext,[status(esa)],[11906]) ).
thf(12650,plain,
sk15 = sk8,
inference(lifteq,[status(thm)],[12644]) ).
thf(163,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] : $true ) )
!= ( cP @ a ) ) ),
inference(paramod_ordered,[status(thm)],[159,69]) ).
thf(164,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] : $true ) )
!= ( cP @ a ) ),
inference(simp,[status(thm)],[163]) ).
thf(177,plain,
( ( sk2
@ ^ [A: $i] : $true )
!= a ),
inference(simp,[status(thm)],[164]) ).
thf(25095,plain,
sk35 != a,
inference(rewrite,[status(thm)],[177,25073]) ).
thf(3331,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ~ $true
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( ( sk1
@ ^ [D: $i] :
( sk1
@ ^ [E: $i] : ( cP @ sk9 ) ) )
!= ( C @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2774,45]) ).
thf(3332,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( ( sk1
@ ^ [D: $i] :
( sk1
@ ^ [E: $i] : ( cP @ sk9 ) ) )
!= ( C @ B @ A ) ) ),
inference(simp,[status(thm)],[3331]) ).
thf(3403,plain,
( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] :
( sk1
@ ^ [D: $i] : ( cP @ A ) ) ) ) ),
inference(pre_uni,[status(thm)],[3332:[bind(A,$thf( A )),bind(B,$thf( sk9 )),bind(C,$thf( ^ [D: $i] : ^ [E: $i] : ( sk1 @ ^ [F: $i] : ( sk1 @ ^ [G: $i] : ( cP @ D ) ) ) ))]]) ).
thf(12340,plain,
( ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk6 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[11186,141]) ).
thf(12341,plain,
( ( sk1 @ ( (=) @ $i @ sk6 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[12340]) ).
thf(12461,plain,
( ( (=) @ $i @ sk6 )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[12341]) ).
thf(6642,plain,
! [A: $i] :
( ( A != sk9 )
| ( ( f @ ( sk2 @ ( (=) @ $i @ A ) ) )
!= ( f @ sk12 ) ) ),
inference(paramod_ordered,[status(thm)],[146,5384]) ).
thf(6833,plain,
( ( sk2 @ ( (=) @ $i @ sk9 ) )
!= sk12 ),
inference(simp,[status(thm)],[6642]) ).
thf(10396,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( B != sk6 )
| ( A != sk9 ) ),
inference(paramod_ordered,[status(thm)],[352,3644]) ).
thf(10397,plain,
! [A: $i] :
( ( sk1 @ ( (=) @ $i @ sk9 ) )
| ( A != sk6 ) ),
inference(pattern_uni,[status(thm)],[10396:[bind(A,$thf( sk9 ))]]) ).
thf(11185,plain,
sk1 @ ( (=) @ $i @ sk9 ),
inference(simp,[status(thm)],[10397]) ).
thf(12180,plain,
( ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk9 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[11185,141]) ).
thf(12181,plain,
( ( sk1 @ ( (=) @ $i @ sk9 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[12180]) ).
thf(12304,plain,
( ( (=) @ $i @ sk9 )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[12181]) ).
thf(11568,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk3 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11165,178]) ).
thf(11569,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk3 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[11568]) ).
thf(11570,plain,
( ( sk2 @ ( (=) @ $i @ sk3 ) )
!= a ),
inference(pattern_uni,[status(thm)],[11569:[bind(A,$thf( (=) @ $i @ sk3 ))]]) ).
thf(20906,plain,
~ ( cP @ sk26 ),
inference(rewrite,[status(thm)],[5346,20901]) ).
thf(22574,plain,
( ~ $true
| ( ( cP @ ( f @ sk28 ) )
!= ( cP @ sk26 ) ) ),
inference(paramod_ordered,[status(thm)],[21459,20906]) ).
thf(22575,plain,
( ( cP @ ( f @ sk28 ) )
!= ( cP @ sk26 ) ),
inference(simp,[status(thm)],[22574]) ).
thf(22705,plain,
( ( f @ sk28 )
!= sk26 ),
inference(simp,[status(thm)],[22575]) ).
thf(3593,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ A ) ) ) )
!= ( cP @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[3487,264]) ).
thf(3594,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ A ) ) ) )
!= ( cP @ sk9 ) ),
inference(simp,[status(thm)],[3593]) ).
thf(3667,plain,
( ( sk2
@ ^ [A: $i] : ( cP @ ( f @ A ) ) )
!= sk9 ),
inference(simp,[status(thm)],[3594]) ).
thf(23254,plain,
sk30 != sk6,
inference(rewrite,[status(thm)],[2955,23238]) ).
thf(1763,plain,
( ~ $true
| ( ( cP @ sk7 )
!= ( cP @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[1595,1221]) ).
thf(1764,plain,
( ( cP @ sk7 )
!= ( cP @ sk6 ) ),
inference(simp,[status(thm)],[1763]) ).
thf(1794,plain,
sk7 != sk6,
inference(simp,[status(thm)],[1764]) ).
thf(10394,plain,
! [B: $i,A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A != sk7 )
| ( B
!= ( sk2
@ ^ [C: $i] :
( sk1
@ ^ [D: $i] : ( cP @ C ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[352,1792]) ).
thf(10395,plain,
! [A: $i] :
( ( sk1 @ ( (=) @ $i @ A ) )
| ( A != sk7 ) ),
inference(pattern_uni,[status(thm)],[10394:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ^ [C: $i] : ( sk1 @ ^ [D: $i] : ( cP @ C ) ) ))]]) ).
thf(11184,plain,
sk1 @ ( (=) @ $i @ sk7 ),
inference(simp,[status(thm)],[10395]) ).
thf(12020,plain,
( ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk7 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[11184,141]) ).
thf(12021,plain,
( ( sk1 @ ( (=) @ $i @ sk7 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[12020]) ).
thf(12142,plain,
( ( (=) @ $i @ sk7 )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[12021]) ).
thf(467,plain,
! [D: $i,C: $i > $o,B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ~ $true
| ~ ( cP @ ( sk2 @ C ) )
| ( ( sk1
@ ^ [E: $i] : ( cP @ ( B @ E ) ) )
!= ( C @ D ) ) ),
inference(paramod_ordered,[status(thm)],[34,17]) ).
thf(468,plain,
! [D: $i,C: $i > $o,B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ~ ( cP @ ( sk2 @ C ) )
| ( ( sk1
@ ^ [E: $i] : ( cP @ ( B @ E ) ) )
!= ( C @ D ) ) ),
inference(simp,[status(thm)],[467]) ).
thf(483,plain,
! [C: $i > $i > $i,B: $i,A: $i] :
( ~ ( cP @ ( C @ B @ A ) )
| ~ ( cP
@ ( sk2
@ ^ [D: $i] :
( sk1
@ ^ [E: $i] : ( cP @ ( C @ D @ E ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[468:[bind(A,$thf( A )),bind(B,$thf( F @ D )),bind(C,$thf( ^ [F: $i] : ( sk1 @ ^ [G: $i] : ( cP @ ( F @ F @ G ) ) ) )),bind(D,$thf( D ))]]) ).
thf(499,plain,
! [C: $i > $i > $i,B: $i,A: $i] :
( ~ ( cP @ ( C @ B @ A ) )
| ~ ( cP
@ ( sk2
@ ^ [D: $i] :
( sk1
@ ^ [E: $i] : ( cP @ ( C @ D @ E ) ) ) ) ) ),
inference(simp,[status(thm)],[483]) ).
thf(14431,plain,
a = sk19,
inference(func_ext,[status(esa)],[12610]) ).
thf(14437,plain,
sk19 = a,
inference(lifteq,[status(thm)],[14431]) ).
thf(15408,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk21 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[15263,5]) ).
thf(15409,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1 @ ( (=) @ $i @ sk21 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[15408]) ).
thf(15410,plain,
~ ( cP @ ( sk2 @ ( (=) @ $i @ sk21 ) ) ),
inference(pattern_uni,[status(thm)],[15409:[bind(A,$thf( (=) @ $i @ sk21 ))]]) ).
thf(3584,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) ) )
!= ( cP @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[3487,741]) ).
thf(3585,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) ) )
!= ( cP @ sk9 ) ),
inference(simp,[status(thm)],[3584]) ).
thf(3671,plain,
( ( sk2
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) )
!= sk9 ),
inference(simp,[status(thm)],[3585]) ).
thf(210,plain,
! [B: $i,A: $i > $o] :
( ~ ( A @ B )
| ~ $true
| ( ( cP @ ( sk2 @ A ) )
!= ( cP @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[198,17]) ).
thf(211,plain,
! [B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( ( cP @ ( sk2 @ A ) )
!= ( cP @ sk3 ) ) ),
inference(simp,[status(thm)],[210]) ).
thf(212,plain,
! [B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( ( sk2 @ A )
!= sk3 ) ),
inference(simp,[status(thm)],[211]) ).
thf(1740,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) ) )
!= ( cP @ sk7 ) ) ),
inference(paramod_ordered,[status(thm)],[1595,741]) ).
thf(1741,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) ) )
!= ( cP @ sk7 ) ),
inference(simp,[status(thm)],[1740]) ).
thf(1776,plain,
( ( sk2
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) )
!= sk7 ),
inference(simp,[status(thm)],[1741]) ).
thf(11494,plain,
( ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk3 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[11165,141]) ).
thf(11495,plain,
( ( sk1 @ ( (=) @ $i @ sk3 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[11494]) ).
thf(11591,plain,
( ( (=) @ $i @ sk3 )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[11495]) ).
thf(11959,plain,
sk3 = sk13,
inference(func_ext,[status(esa)],[11591]) ).
thf(11965,plain,
sk13 = sk3,
inference(lifteq,[status(thm)],[11959]) ).
thf(11646,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk12 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11170,5]) ).
thf(11647,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1 @ ( (=) @ $i @ sk12 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[11646]) ).
thf(11648,plain,
~ ( cP @ ( sk2 @ ( (=) @ $i @ sk12 ) ) ),
inference(pattern_uni,[status(thm)],[11647:[bind(A,$thf( (=) @ $i @ sk12 ))]]) ).
thf(15299,plain,
( ~ $true
| ( ( cP @ ( sk2 @ ( (=) @ $i @ sk12 ) ) )
!= ( cP @ sk7 ) ) ),
inference(paramod_ordered,[status(thm)],[1595,11648]) ).
thf(15300,plain,
( ( cP @ ( sk2 @ ( (=) @ $i @ sk12 ) ) )
!= ( cP @ sk7 ) ),
inference(simp,[status(thm)],[15299]) ).
thf(15354,plain,
( ( sk2 @ ( (=) @ $i @ sk12 ) )
!= sk7 ),
inference(simp,[status(thm)],[15300]) ).
thf(1228,plain,
( ~ $true
| ( ( cP @ sk6 )
!= ( cP @ a ) ) ),
inference(paramod_ordered,[status(thm)],[159,1221]) ).
thf(1229,plain,
( ( cP @ sk6 )
!= ( cP @ a ) ),
inference(simp,[status(thm)],[1228]) ).
thf(1246,plain,
sk6 != a,
inference(simp,[status(thm)],[1229]) ).
thf(14350,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk4 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11236,178]) ).
thf(14351,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk4 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[14350]) ).
thf(14352,plain,
( ( sk2 @ ( (=) @ $i @ sk4 ) )
!= a ),
inference(pattern_uni,[status(thm)],[14351:[bind(A,$thf( (=) @ $i @ sk4 ))]]) ).
thf(477,plain,
! [C: $i > $i,B: $i,A: $i > $o] :
( ~ ( sk1 @ A )
| ( sk1
@ ^ [D: $i] : ( cP @ ( C @ D ) ) )
| ~ $true
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( cP @ ( C @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[7,34]) ).
thf(478,plain,
! [C: $i > $i,B: $i,A: $i > $o] :
( ~ ( sk1 @ A )
| ( sk1
@ ^ [D: $i] : ( cP @ ( C @ D ) ) )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( cP @ ( C @ B ) ) ) ),
inference(simp,[status(thm)],[477]) ).
thf(495,plain,
! [C: $i > $i,B: $i > $i,A: $i] :
( ~ ( sk1
@ ^ [D: $i] : ( cP @ ( C @ D ) ) )
| ( sk1
@ ^ [D: $i] : ( cP @ ( B @ D ) ) )
| ( ( C
@ ( f
@ ( sk2
@ ^ [D: $i] : ( cP @ ( C @ D ) ) ) ) )
!= ( B @ A ) ) ),
inference(pre_uni,[status(thm)],[478:[bind(A,$thf( ^ [E: $i] : ( cP @ ( D @ E ) ) ))]]) ).
thf(496,plain,
! [C: $i > $i,B: $i > $i,A: $i] :
( ( sk1
@ ^ [D: $i] : ( cP @ ( B @ D ) ) )
| ~ ( sk1
@ ^ [D: $i] : ( cP @ ( C @ D ) ) )
| ( ( C
@ ( f
@ ( sk2
@ ^ [D: $i] : ( cP @ ( C @ D ) ) ) ) )
!= ( B @ A ) ) ),
inference(pre_uni,[status(thm)],[495:[]]) ).
thf(503,plain,
! [C: $i > $i,B: $i > $i,A: $i] :
( ( sk1
@ ^ [D: $i] : ( cP @ ( B @ D ) ) )
| ~ ( sk1
@ ^ [D: $i] : ( cP @ ( C @ D ) ) )
| ( ( C
@ ( f
@ ( sk2
@ ^ [D: $i] : ( cP @ ( C @ D ) ) ) ) )
!= ( B @ A ) ) ),
inference(simp,[status(thm)],[496]) ).
thf(729,plain,
! [B: $i > $i,A: $i] :
( ( sk1
@ ^ [C: $i] : ( cP @ ( B @ C ) ) )
| ~ $true
| ( ( cP
@ ( f
@ ( f
@ ( sk2
@ ^ [C: $i] : ( cP @ ( f @ C ) ) ) ) ) )
!= ( cP @ ( B @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[284,34]) ).
thf(730,plain,
! [B: $i > $i,A: $i] :
( ( sk1
@ ^ [C: $i] : ( cP @ ( B @ C ) ) )
| ( ( cP
@ ( f
@ ( f
@ ( sk2
@ ^ [C: $i] : ( cP @ ( f @ C ) ) ) ) ) )
!= ( cP @ ( B @ A ) ) ) ),
inference(simp,[status(thm)],[729]) ).
thf(737,plain,
( sk1
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) ),
inference(pre_uni,[status(thm)],[730:[bind(A,$thf( sk2 @ ^ [C: $i] : ( cP @ ( f @ C ) ) )),bind(B,$thf( ^ [C: $i] : ( f @ ( f @ C ) ) ))]]) ).
thf(764,plain,
( ~ $true
| ( ( sk1
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[737,141]) ).
thf(765,plain,
( ( sk1
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[764]) ).
thf(786,plain,
( ( ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[765]) ).
thf(936,plain,
cP @ ( f @ ( f @ sk5 ) ),
inference(func_ext,[status(esa)],[786]) ).
thf(1226,plain,
( ~ $true
| ( ( cP @ ( f @ ( f @ sk5 ) ) )
!= ( cP @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[936,1221]) ).
thf(1227,plain,
( ( cP @ ( f @ ( f @ sk5 ) ) )
!= ( cP @ sk6 ) ),
inference(simp,[status(thm)],[1226]) ).
thf(1241,plain,
( ( f @ ( f @ sk5 ) )
!= sk6 ),
inference(simp,[status(thm)],[1227]) ).
thf(1738,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) ) )
!= ( cP @ sk7 ) ) ),
inference(paramod_ordered,[status(thm)],[1595,1190]) ).
thf(1739,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) ) )
!= ( cP @ sk7 ) ),
inference(simp,[status(thm)],[1738]) ).
thf(1779,plain,
( ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) )
!= sk7 ),
inference(simp,[status(thm)],[1739]) ).
thf(5359,plain,
( ~ $true
| ( ( cP @ ( f @ sk12 ) )
!= ( cP @ a ) ) ),
inference(paramod_ordered,[status(thm)],[159,5346]) ).
thf(5360,plain,
( ( cP @ ( f @ sk12 ) )
!= ( cP @ a ) ),
inference(simp,[status(thm)],[5359]) ).
thf(5377,plain,
( ( f @ sk12 )
!= a ),
inference(simp,[status(thm)],[5360]) ).
thf(6726,plain,
! [A: $i] :
( ( A != a )
| ( ( f @ ( sk2 @ ( (=) @ $i @ A ) ) )
!= ( f @ sk12 ) ) ),
inference(paramod_ordered,[status(thm)],[146,5377]) ).
thf(6859,plain,
( ( sk2 @ ( (=) @ $i @ a ) )
!= sk12 ),
inference(simp,[status(thm)],[6726]) ).
thf(1556,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) ) )
!= ( cP @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[198,1435]) ).
thf(1557,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) ) )
!= ( cP @ sk3 ) ),
inference(simp,[status(thm)],[1556]) ).
thf(1563,plain,
( ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) )
!= sk3 ),
inference(simp,[status(thm)],[1557]) ).
thf(12484,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ a ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11191,218]) ).
thf(12485,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ a ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[12484]) ).
thf(12486,plain,
( ( sk2 @ ( (=) @ $i @ a ) )
!= sk3 ),
inference(pattern_uni,[status(thm)],[12485:[bind(A,$thf( (=) @ $i @ a ))]]) ).
thf(1236,plain,
( ~ $true
| ( ( cP @ ( f @ ( sk2 @ cP ) ) )
!= ( cP @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[190,1221]) ).
thf(1237,plain,
( ( cP @ ( f @ ( sk2 @ cP ) ) )
!= ( cP @ sk6 ) ),
inference(simp,[status(thm)],[1236]) ).
thf(1238,plain,
( ( f @ ( sk2 @ cP ) )
!= sk6 ),
inference(simp,[status(thm)],[1237]) ).
thf(21448,plain,
( ( f @ sk28 )
!= sk6 ),
inference(rewrite,[status(thm)],[1238,21443]) ).
thf(13597,plain,
sk6 = sk18,
inference(func_ext,[status(esa)],[12461]) ).
thf(13603,plain,
sk18 = sk6,
inference(lifteq,[status(thm)],[13597]) ).
thf(1257,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) ) )
!= ( cP @ a ) ) ),
inference(paramod_ordered,[status(thm)],[159,1190]) ).
thf(1258,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) ) )
!= ( cP @ a ) ),
inference(simp,[status(thm)],[1257]) ).
thf(1273,plain,
( ( sk2
@ ^ [A: $i] :
~ ( cP @ A ) )
!= a ),
inference(simp,[status(thm)],[1258]) ).
thf(95,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ~ ( B @ C )
| ~ $true
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( cP @ ( sk2 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[7,17]) ).
thf(96,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ~ ( B @ C )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( cP @ ( sk2 @ B ) ) ) ),
inference(simp,[status(thm)],[95]) ).
thf(125,plain,
! [B: $i > $i > $o,A: $i] :
( ~ ( sk1
@ ^ [C: $i] : ( cP @ ( sk2 @ ( B @ C ) ) ) )
| ~ ( B
@ ( f
@ ( sk2
@ ^ [C: $i] : ( cP @ ( sk2 @ ( B @ C ) ) ) ) )
@ A ) ),
inference(pre_uni,[status(thm)],[96:[bind(A,$thf( ^ [E: $i] : ( cP @ ( sk2 @ ( E @ E ) ) ) )),bind(B,$thf( E @ ( f @ ( sk2 @ ^ [E: $i] : ( cP @ ( sk2 @ ( E @ E ) ) ) ) ) )),bind(C,$thf( C ))]]) ).
thf(148,plain,
! [B: $i > $i > $o,A: $i] :
( ~ ( sk1
@ ^ [C: $i] : ( cP @ ( sk2 @ ( B @ C ) ) ) )
| ~ ( B
@ ( f
@ ( sk2
@ ^ [C: $i] : ( cP @ ( sk2 @ ( B @ C ) ) ) ) )
@ A ) ),
inference(simp,[status(thm)],[125]) ).
thf(519,plain,
! [B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ~ $true
| ( ( sk1
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) )
!= ( sk1
@ ^ [C: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[35,141]) ).
thf(520,plain,
! [B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ( ( sk1
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) )
!= ( sk1
@ ^ [C: $i] : $false ) ) ),
inference(simp,[status(thm)],[519]) ).
thf(562,plain,
! [B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ( ( ^ [C: $i] : ( sk1 @ ( B @ C ) ) )
!= ( ^ [C: $i] : $false ) ) ),
inference(simp,[status(thm)],[520]) ).
thf(2796,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ~ $true
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( ( sk1
@ ^ [D: $i] : ( cP @ ( f @ sk8 ) ) )
!= ( C @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2771,45]) ).
thf(2797,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( ( sk1
@ ^ [D: $i] : ( cP @ ( f @ sk8 ) ) )
!= ( C @ B @ A ) ) ),
inference(simp,[status(thm)],[2796]) ).
thf(2849,plain,
( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ ( f @ A ) ) ) ) ),
inference(pre_uni,[status(thm)],[2797:[bind(A,$thf( A )),bind(B,$thf( sk8 )),bind(C,$thf( ^ [D: $i] : ^ [E: $i] : ( sk1 @ ^ [F: $i] : ( cP @ ( f @ D ) ) ) ))]]) ).
thf(57,plain,
! [B: $i > $o,A: $i] :
( ~ ~ ( B @ A )
| ~ ( cP
@ ( sk2
@ ^ [C: $i] :
~ ( B @ C ) ) ) ),
inference(prim_subst,[status(thm)],[17:[bind(A,$thf( ^ [D: $i] : ~ ( C @ D ) ))]]) ).
thf(70,plain,
! [B: $i > $o,A: $i] :
( ( B @ A )
| ~ ( cP
@ ( sk2
@ ^ [C: $i] :
~ ( B @ C ) ) ) ),
inference(cnf,[status(esa)],[57]) ).
thf(71,plain,
! [B: $i > $o,A: $i] :
( ( B @ A )
| ~ ( cP
@ ( sk2
@ ^ [C: $i] :
~ ( B @ C ) ) ) ),
inference(simp,[status(thm)],[70]) ).
thf(534,plain,
! [D: $i,C: $i > $o,B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ~ $true
| ~ ( cP @ ( sk2 @ C ) )
| ( ( sk1
@ ^ [E: $i] : ( sk1 @ ( B @ E ) ) )
!= ( C @ D ) ) ),
inference(paramod_ordered,[status(thm)],[35,17]) ).
thf(535,plain,
! [D: $i,C: $i > $o,B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ~ ( cP @ ( sk2 @ C ) )
| ( ( sk1
@ ^ [E: $i] : ( sk1 @ ( B @ E ) ) )
!= ( C @ D ) ) ),
inference(simp,[status(thm)],[534]) ).
thf(561,plain,
! [C: $i > $i > $i > $o,B: $i,A: $i] :
( ~ ( sk1 @ ( C @ B @ A ) )
| ~ ( cP
@ ( sk2
@ ^ [D: $i] :
( sk1
@ ^ [E: $i] : ( sk1 @ ( C @ D @ E ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[535:[bind(A,$thf( A )),bind(B,$thf( F @ D )),bind(C,$thf( ^ [F: $i] : ( sk1 @ ^ [G: $i] : ( sk1 @ ( F @ F @ G ) ) ) )),bind(D,$thf( D ))]]) ).
thf(572,plain,
! [C: $i > $i > $i > $o,B: $i,A: $i] :
( ~ ( sk1 @ ( C @ B @ A ) )
| ~ ( cP
@ ( sk2
@ ^ [D: $i] :
( sk1
@ ^ [E: $i] : ( sk1 @ ( C @ D @ E ) ) ) ) ) ),
inference(simp,[status(thm)],[561]) ).
thf(119,plain,
! [A: $i > $i] :
( ( cP
@ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( cP @ ( A @ B ) ) ) ) ) )
| ~ ( sk1
@ ^ [B: $i] : ( cP @ ( A @ B ) ) ) ),
inference(prim_subst,[status(thm)],[7:[bind(A,$thf( ^ [C: $i] : ( cP @ ( B @ C ) ) ))]]) ).
thf(144,plain,
! [A: $i > $i] :
( ( cP
@ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( cP @ ( A @ B ) ) ) ) ) )
| ~ ( sk1
@ ^ [B: $i] : ( cP @ ( A @ B ) ) ) ),
inference(simp,[status(thm)],[119]) ).
thf(1232,plain,
( ~ $true
| ( ( cP @ sk6 )
!= ( cP @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[198,1221]) ).
thf(1233,plain,
( ( cP @ sk6 )
!= ( cP @ sk3 ) ),
inference(simp,[status(thm)],[1232]) ).
thf(1239,plain,
sk6 != sk3,
inference(simp,[status(thm)],[1233]) ).
thf(11654,plain,
( ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk12 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[11170,141]) ).
thf(11655,plain,
( ( sk1 @ ( (=) @ $i @ sk12 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[11654]) ).
thf(11759,plain,
( ( (=) @ $i @ sk12 )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[11655]) ).
thf(11967,plain,
sk12 = sk14,
inference(func_ext,[status(esa)],[11759]) ).
thf(11973,plain,
sk14 = sk12,
inference(lifteq,[status(thm)],[11967]) ).
thf(16449,plain,
( ~ $true
| ( ( cP @ ( sk2 @ ( (=) @ $i @ sk8 ) ) )
!= ( cP @ sk7 ) ) ),
inference(paramod_ordered,[status(thm)],[1595,11808]) ).
thf(16450,plain,
( ( cP @ ( sk2 @ ( (=) @ $i @ sk8 ) ) )
!= ( cP @ sk7 ) ),
inference(simp,[status(thm)],[16449]) ).
thf(16500,plain,
( ( sk2 @ ( (=) @ $i @ sk8 ) )
!= sk7 ),
inference(simp,[status(thm)],[16450]) ).
thf(14256,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk4 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11236,218]) ).
thf(14257,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk4 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[14256]) ).
thf(14258,plain,
( ( sk2 @ ( (=) @ $i @ sk4 ) )
!= sk3 ),
inference(pattern_uni,[status(thm)],[14257:[bind(A,$thf( (=) @ $i @ sk4 ))]]) ).
thf(627,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
| ~ $true
| ( ( cP @ sk3 )
!= ( B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[198,40]) ).
thf(628,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
| ( ( cP @ sk3 )
!= ( B @ A ) ) ),
inference(simp,[status(thm)],[627]) ).
thf(642,plain,
! [A: $i > $o] :
( sk1
@ ^ [B: $i] :
( ( cP @ B )
| ( A @ B ) ) ),
inference(pre_uni,[status(thm)],[628:[bind(A,$thf( sk3 )),bind(B,$thf( cP )),bind(C,$thf( C ))]]) ).
thf(672,plain,
! [A: $i > $o] :
( sk1
@ ^ [B: $i] :
( ( cP @ B )
| ( A @ B ) ) ),
inference(simp,[status(thm)],[642]) ).
thf(12094,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk7 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11184,178]) ).
thf(12095,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk7 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[12094]) ).
thf(12096,plain,
( ( sk2 @ ( (=) @ $i @ sk7 ) )
!= a ),
inference(pattern_uni,[status(thm)],[12095:[bind(A,$thf( (=) @ $i @ sk7 ))]]) ).
thf(521,plain,
! [D: $i > $i > $o,C: $i,B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ( sk1
@ ^ [E: $i] : ( sk1 @ ( D @ E ) ) )
| ~ $true
| ( ( sk1
@ ^ [E: $i] : ( sk1 @ ( B @ E ) ) )
!= ( sk1 @ ( D @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[35,35]) ).
thf(522,plain,
! [D: $i > $i > $o,C: $i,B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ( sk1
@ ^ [E: $i] : ( sk1 @ ( D @ E ) ) )
| ( ( sk1
@ ^ [E: $i] : ( sk1 @ ( B @ E ) ) )
!= ( sk1 @ ( D @ C ) ) ) ),
inference(simp,[status(thm)],[521]) ).
thf(553,plain,
! [C: $i > $i > $i > $o,B: $i,A: $i] :
( ~ ( sk1 @ ( C @ B @ A ) )
| ( sk1
@ ^ [D: $i] :
( sk1
@ ^ [E: $i] : ( sk1 @ ( C @ D @ E ) ) ) ) ),
inference(pre_uni,[status(thm)],[522:[bind(A,$thf( A )),bind(B,$thf( E @ C )),bind(C,$thf( C )),bind(D,$thf( ^ [F: $i] : ^ [G: $i] : ( sk1 @ ( E @ F @ G ) ) ))]]) ).
thf(567,plain,
! [C: $i > $i > $i > $o,B: $i,A: $i] :
( ~ ( sk1 @ ( C @ B @ A ) )
| ( sk1
@ ^ [D: $i] :
( sk1
@ ^ [E: $i] : ( sk1 @ ( C @ D @ E ) ) ) ) ),
inference(simp,[status(thm)],[553]) ).
thf(15307,plain,
( ~ $true
| ( ( cP @ ( sk2 @ ( (=) @ $i @ sk12 ) ) )
!= ( cP @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[3487,11648]) ).
thf(15308,plain,
( ( cP @ ( sk2 @ ( (=) @ $i @ sk12 ) ) )
!= ( cP @ sk9 ) ),
inference(simp,[status(thm)],[15307]) ).
thf(15352,plain,
( ( sk2 @ ( (=) @ $i @ sk12 ) )
!= sk9 ),
inference(simp,[status(thm)],[15308]) ).
thf(21456,plain,
~ ( cP @ sk28 ),
inference(rewrite,[status(thm)],[58,21443]) ).
thf(116,plain,
! [A: $i > $i > $o] :
( ( sk1
@ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) ) ) )
| ~ ( sk1
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) ),
inference(prim_subst,[status(thm)],[7:[bind(A,$thf( ^ [C: $i] : ( sk1 @ ( B @ C ) ) ))]]) ).
thf(140,plain,
! [A: $i > $i > $o] :
( ( sk1
@ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) ) ) )
| ~ ( sk1
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) ),
inference(simp,[status(thm)],[116]) ).
thf(23899,plain,
sk31 != sk6,
inference(rewrite,[status(thm)],[1240,23246]) ).
thf(24708,plain,
sk30 = sk33,
inference(func_ext,[status(esa)],[23255]) ).
thf(24710,plain,
sk33 = sk30,
inference(lifteq,[status(thm)],[24708]) ).
thf(54,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ~ ( ( B @ A )
| ( C @ A ) )
| ~ ( cP
@ ( sk2
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) ) ) ),
inference(prim_subst,[status(thm)],[17:[bind(A,$thf( ^ [E: $i] : ( ( C @ E ) | ( D @ E ) ) ))]]) ).
thf(63,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ( ~ ( B @ A )
| ~ ( cP
@ ( sk2
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) ) ) )
& ( ~ ( C @ A )
| ~ ( cP
@ ( sk2
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) ) ) ) ),
inference(cnf,[status(esa)],[54]) ).
thf(64,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ~ ( B @ A )
| ~ ( cP
@ ( sk2
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) ) ) ),
inference(cnfConj,[status(thm)],[63]) ).
thf(66,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ~ ( B @ A )
| ~ ( cP
@ ( sk2
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) ) ) ),
inference(simp,[status(thm)],[64]) ).
thf(11638,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk12 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11170,218]) ).
thf(11639,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk12 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[11638]) ).
thf(11640,plain,
( ( sk2 @ ( (=) @ $i @ sk12 ) )
!= sk3 ),
inference(pattern_uni,[status(thm)],[11639:[bind(A,$thf( (=) @ $i @ sk12 ))]]) ).
thf(20909,plain,
( ( f @ sk8 )
!= sk26 ),
inference(rewrite,[status(thm)],[5378,20901]) ).
thf(23249,plain,
sk30 != sk26,
inference(rewrite,[status(thm)],[20909,23238]) ).
thf(371,plain,
( ~ $true
| ( ( cP @ ( sk2 @ cP ) )
!= ( cP @ ( f @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[288,58]) ).
thf(372,plain,
( ( cP @ ( sk2 @ cP ) )
!= ( cP @ ( f @ sk4 ) ) ),
inference(simp,[status(thm)],[371]) ).
thf(373,plain,
( ( sk2 @ cP )
!= ( f @ sk4 ) ),
inference(simp,[status(thm)],[372]) ).
thf(21458,plain,
( ( f @ sk4 )
!= sk28 ),
inference(rewrite,[status(thm)],[373,21443]) ).
thf(23902,plain,
sk31 != sk28,
inference(rewrite,[status(thm)],[21458,23246]) ).
thf(93,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ~ $true
| ~ ( cP @ ( sk2 @ B ) )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[7,17]) ).
thf(94,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ~ ( cP @ ( sk2 @ B ) )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( B @ C ) ) ),
inference(simp,[status(thm)],[93]) ).
thf(129,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ~ ( cP @ ( sk2 @ B ) )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( B @ C ) ) ),
inference(pre_uni,[status(thm)],[94:[]]) ).
thf(130,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( cP @ ( sk2 @ B ) )
| ~ ( sk1 @ A )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( B @ C ) ) ),
inference(pre_uni,[status(thm)],[129:[]]) ).
thf(12004,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk7 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11184,218]) ).
thf(12005,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk7 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[12004]) ).
thf(12006,plain,
( ( sk2 @ ( (=) @ $i @ sk7 ) )
!= sk3 ),
inference(pattern_uni,[status(thm)],[12005:[bind(A,$thf( (=) @ $i @ sk7 ))]]) ).
thf(99,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ( sk1 @ B )
| ~ $true
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[7,11]) ).
thf(100,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ( sk1 @ B )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( B @ C ) ) ),
inference(simp,[status(thm)],[99]) ).
thf(134,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ( sk1 @ B )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( B @ C ) ) ),
inference(pre_uni,[status(thm)],[100:[]]) ).
thf(135,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ( sk1 @ B )
| ~ ( sk1 @ A )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( B @ C ) ) ),
inference(pre_uni,[status(thm)],[134:[]]) ).
thf(474,plain,
! [C: $i > $o,B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ( C @ ( f @ ( sk2 @ C ) ) )
| ~ $true
| ( ( sk1
@ ^ [D: $i] : ( cP @ ( B @ D ) ) )
!= ( sk1 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[34,7]) ).
thf(475,plain,
! [C: $i > $o,B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ( C @ ( f @ ( sk2 @ C ) ) )
| ( ( sk1
@ ^ [D: $i] : ( cP @ ( B @ D ) ) )
!= ( sk1 @ C ) ) ),
inference(simp,[status(thm)],[474]) ).
thf(476,plain,
! [B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ( cP
@ ( B
@ ( f
@ ( sk2
@ ^ [C: $i] : ( cP @ ( B @ C ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[475:[bind(A,$thf( A )),bind(B,$thf( D )),bind(C,$thf( ^ [E: $i] : ( cP @ ( D @ E ) ) ))]]) ).
thf(505,plain,
! [B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ( cP
@ ( B
@ ( f
@ ( sk2
@ ^ [C: $i] : ( cP @ ( B @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[476]) ).
thf(20907,plain,
sk26 != a,
inference(rewrite,[status(thm)],[5377,20901]) ).
thf(206,plain,
( ~ $true
| ( ( cP @ ( sk2 @ cP ) )
!= ( cP @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[198,58]) ).
thf(207,plain,
( ( cP @ ( sk2 @ cP ) )
!= ( cP @ sk3 ) ),
inference(simp,[status(thm)],[206]) ).
thf(219,plain,
( ( sk2 @ cP )
!= sk3 ),
inference(simp,[status(thm)],[207]) ).
thf(21452,plain,
sk28 != sk3,
inference(rewrite,[status(thm)],[219,21443]) ).
thf(1009,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) ) )
!= ( cP @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[198,741]) ).
thf(1010,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) ) )
!= ( cP @ sk3 ) ),
inference(simp,[status(thm)],[1009]) ).
thf(1018,plain,
( ( sk2
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) )
!= sk3 ),
inference(simp,[status(thm)],[1010]) ).
thf(315,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ( sk1 @ B )
| ~ ( B @ C )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( ~ ( sk1 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[7,32]) ).
thf(335,plain,
! [B: $i > $i > $o,A: $i] :
( ~ ( sk1
@ ^ [C: $i] :
~ ( sk1 @ ( B @ C ) ) )
| ( sk1
@ ( B
@ ( f
@ ( sk2
@ ^ [C: $i] :
~ ( sk1 @ ( B @ C ) ) ) ) ) )
| ~ ( B
@ ( f
@ ( sk2
@ ^ [C: $i] :
~ ( sk1 @ ( B @ C ) ) ) )
@ A ) ),
inference(pre_uni,[status(thm)],[315:[bind(A,$thf( ^ [E: $i] : ~ ( sk1 @ ( E @ E ) ) )),bind(B,$thf( E @ ( f @ ( sk2 @ ^ [E: $i] : ~ ( sk1 @ ( E @ E ) ) ) ) )),bind(C,$thf( C ))]]) ).
thf(355,plain,
! [B: $i > $i > $o,A: $i] :
( ~ ( sk1
@ ^ [C: $i] :
~ ( sk1 @ ( B @ C ) ) )
| ( sk1
@ ( B
@ ( f
@ ( sk2
@ ^ [C: $i] :
~ ( sk1 @ ( B @ C ) ) ) ) ) )
| ~ ( B
@ ( f
@ ( sk2
@ ^ [C: $i] :
~ ( sk1 @ ( B @ C ) ) ) )
@ A ) ),
inference(simp,[status(thm)],[335]) ).
thf(87,plain,
! [B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ~ $true
| ~ ( sk1 @ B )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( cP @ ( sk2 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[7,5]) ).
thf(88,plain,
! [B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ~ ( sk1 @ B )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( cP @ ( sk2 @ B ) ) ) ),
inference(simp,[status(thm)],[87]) ).
thf(122,plain,
! [A: $i > $i > $o] :
( ~ ( sk1
@ ^ [B: $i] : ( cP @ ( sk2 @ ( A @ B ) ) ) )
| ~ ( sk1
@ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( cP @ ( sk2 @ ( A @ B ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[88:[bind(A,$thf( ^ [D: $i] : ( cP @ ( sk2 @ ( D @ D ) ) ) )),bind(B,$thf( D @ ( f @ ( sk2 @ ^ [D: $i] : ( cP @ ( sk2 @ ( D @ D ) ) ) ) ) ))]]) ).
thf(145,plain,
! [A: $i > $i > $o] :
( ~ ( sk1
@ ^ [B: $i] : ( cP @ ( sk2 @ ( A @ B ) ) ) )
| ~ ( sk1
@ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( cP @ ( sk2 @ ( A @ B ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[122]) ).
thf(461,plain,
! [B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ~ $true
| ( ( sk1
@ ^ [C: $i] : ( cP @ ( B @ C ) ) )
!= ( sk1
@ ^ [C: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[34,141]) ).
thf(462,plain,
! [B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ( ( sk1
@ ^ [C: $i] : ( cP @ ( B @ C ) ) )
!= ( sk1
@ ^ [C: $i] : $false ) ) ),
inference(simp,[status(thm)],[461]) ).
thf(490,plain,
! [B: $i > $i,A: $i] :
( ~ ( cP @ ( B @ A ) )
| ( ( ^ [C: $i] : ( cP @ ( B @ C ) ) )
!= ( ^ [C: $i] : $false ) ) ),
inference(simp,[status(thm)],[462]) ).
thf(604,plain,
! [F: $i > $o,E: $i > $o,D: $i,C: $i > $o,B: $i > $o,A: $i] :
( ~ ( B @ A )
| ( sk1
@ ^ [G: $i] :
( ( E @ G )
| ( F @ G ) ) )
| ~ $true
| ( ( sk1
@ ^ [G: $i] :
( ( B @ G )
| ( C @ G ) ) )
!= ( E @ D ) ) ),
inference(paramod_ordered,[status(thm)],[40,40]) ).
thf(605,plain,
! [F: $i > $o,E: $i > $o,D: $i,C: $i > $o,B: $i > $o,A: $i] :
( ~ ( B @ A )
| ( sk1
@ ^ [G: $i] :
( ( E @ G )
| ( F @ G ) ) )
| ( ( sk1
@ ^ [G: $i] :
( ( B @ G )
| ( C @ G ) ) )
!= ( E @ D ) ) ),
inference(simp,[status(thm)],[604]) ).
thf(645,plain,
! [E: $i > $i > $o,D: $i > $i > $o,C: $i > $o,B: $i,A: $i] :
( ~ ( D @ B @ A )
| ( sk1
@ ^ [F: $i] :
( ( sk1
@ ^ [G: $i] :
( ( D @ F @ G )
| ( E @ F @ G ) ) )
| ( C @ F ) ) ) ),
inference(pre_uni,[status(thm)],[605:[bind(A,$thf( A )),bind(B,$thf( H @ D )),bind(C,$thf( I @ D )),bind(D,$thf( D )),bind(E,$thf( ^ [I: $i] : ( sk1 @ ^ [J: $i] : ( ( H @ I @ J ) | ( I @ I @ J ) ) ) )),bind(F,$thf( F ))]]) ).
thf(675,plain,
! [E: $i > $i > $o,D: $i > $i > $o,C: $i > $o,B: $i,A: $i] :
( ~ ( D @ B @ A )
| ( sk1
@ ^ [F: $i] :
( ( sk1
@ ^ [G: $i] :
( ( D @ F @ G )
| ( E @ F @ G ) ) )
| ( C @ F ) ) ) ),
inference(simp,[status(thm)],[645]) ).
thf(12324,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk6 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11186,218]) ).
thf(12325,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk6 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[12324]) ).
thf(12326,plain,
( ( sk2 @ ( (=) @ $i @ sk6 ) )
!= sk3 ),
inference(pattern_uni,[status(thm)],[12325:[bind(A,$thf( (=) @ $i @ sk6 ))]]) ).
thf(6012,plain,
sk12 != sk4,
inference(simp,[status(thm)],[5375]) ).
thf(12172,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk9 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11185,5]) ).
thf(12173,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1 @ ( (=) @ $i @ sk9 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[12172]) ).
thf(12174,plain,
~ ( cP @ ( sk2 @ ( (=) @ $i @ sk9 ) ) ),
inference(pattern_uni,[status(thm)],[12173:[bind(A,$thf( (=) @ $i @ sk9 ))]]) ).
thf(1552,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) ) )
!= ( cP @ a ) ) ),
inference(paramod_ordered,[status(thm)],[159,1435]) ).
thf(1553,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) ) )
!= ( cP @ a ) ),
inference(simp,[status(thm)],[1552]) ).
thf(1566,plain,
( ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) )
!= a ),
inference(simp,[status(thm)],[1553]) ).
thf(12254,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk9 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11185,178]) ).
thf(12255,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk9 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[12254]) ).
thf(12256,plain,
( ( sk2 @ ( (=) @ $i @ sk9 ) )
!= a ),
inference(pattern_uni,[status(thm)],[12255:[bind(A,$thf( (=) @ $i @ sk9 ))]]) ).
thf(65,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ~ ( C @ A )
| ~ ( cP
@ ( sk2
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) ) ) ),
inference(cnfConj,[status(thm)],[63]) ).
thf(67,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ~ ( C @ A )
| ~ ( cP
@ ( sk2
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) ) ) ),
inference(simp,[status(thm)],[65]) ).
thf(4233,plain,
! [A: $i > $i > $o] :
( ~ ( sk1
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) )
| ~ $true
| ( ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) )
@ ( f
@ ( sk2
@ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) ) ) ) ) )
!= ( cP @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[136,1221]) ).
thf(4234,plain,
! [A: $i > $i > $o] :
( ~ ( sk1
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) )
| ( ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) )
@ ( f
@ ( sk2
@ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] : ( sk1 @ ( A @ B ) ) ) ) ) ) ) )
!= ( cP @ sk6 ) ) ),
inference(simp,[status(thm)],[4233]) ).
thf(4292,plain,
~ ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ sk6 ) ) ),
inference(pre_uni,[status(thm)],[4234:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ( cP @ sk6 ) ))]]) ).
thf(4398,plain,
~ ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : $false ) ),
inference(rewrite,[status(thm)],[4292,1221]) ).
thf(15418,plain,
( ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk21 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[15263,141]) ).
thf(15419,plain,
( ( sk1 @ ( (=) @ $i @ sk21 ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[15418]) ).
thf(15556,plain,
( ( (=) @ $i @ sk21 )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[15419]) ).
thf(23894,plain,
cP @ sk31,
inference(rewrite,[status(thm)],[288,23246]) ).
thf(3326,plain,
( ~ $true
| ( ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ sk9 ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[2774,141]) ).
thf(3327,plain,
( ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ sk9 ) ) )
!= ( sk1
@ ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[3326]) ).
thf(3390,plain,
( ( ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ sk9 ) ) )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[3327]) ).
thf(3715,plain,
( ( ^ [A: $i] :
( sk1
@ ^ [B: $i] : $true ) )
!= ( ^ [A: $i] : $false ) ),
inference(rewrite,[status(thm)],[3390,3487]) ).
thf(12414,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk6 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11186,178]) ).
thf(12415,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk6 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[12414]) ).
thf(12416,plain,
( ( sk2 @ ( (=) @ $i @ sk6 ) )
!= a ),
inference(pattern_uni,[status(thm)],[12415:[bind(A,$thf( (=) @ $i @ sk6 ))]]) ).
thf(23256,plain,
cP @ sk30,
inference(rewrite,[status(thm)],[2811,23238]) ).
thf(3629,plain,
( ~ $true
| ( ( cP @ ( sk2 @ cP ) )
!= ( cP @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[3487,58]) ).
thf(3630,plain,
( ( cP @ ( sk2 @ cP ) )
!= ( cP @ sk9 ) ),
inference(simp,[status(thm)],[3629]) ).
thf(3645,plain,
( ( sk2 @ cP )
!= sk9 ),
inference(simp,[status(thm)],[3630]) ).
thf(21455,plain,
sk28 != sk9,
inference(rewrite,[status(thm)],[3645,21443]) ).
thf(12012,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk7 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11184,5]) ).
thf(12013,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1 @ ( (=) @ $i @ sk7 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[12012]) ).
thf(12014,plain,
~ ( cP @ ( sk2 @ ( (=) @ $i @ sk7 ) ) ),
inference(pattern_uni,[status(thm)],[12013:[bind(A,$thf( (=) @ $i @ sk7 ))]]) ).
thf(169,plain,
! [B: $i,A: $i > $o] :
( ~ ( A @ B )
| ~ $true
| ( ( cP @ ( sk2 @ A ) )
!= ( cP @ a ) ) ),
inference(paramod_ordered,[status(thm)],[159,17]) ).
thf(170,plain,
! [B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( ( cP @ ( sk2 @ A ) )
!= ( cP @ a ) ) ),
inference(simp,[status(thm)],[169]) ).
thf(175,plain,
! [B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( ( sk2 @ A )
!= a ) ),
inference(simp,[status(thm)],[170]) ).
thf(546,plain,
! [C: $i > $i > $o,B: $i,A: $i > $o] :
( ~ ( sk1 @ A )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ~ $true
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( sk1 @ ( C @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[7,35]) ).
thf(547,plain,
! [C: $i > $i > $o,B: $i,A: $i > $o] :
( ~ ( sk1 @ A )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( sk1 @ ( C @ B ) ) ) ),
inference(simp,[status(thm)],[546]) ).
thf(559,plain,
! [C: $i > $i > $o,B: $i > $i > $o,A: $i] :
( ~ ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) ) )
| ( ( C
@ ( f
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) ) ) )
!= ( B @ A ) ) ),
inference(pre_uni,[status(thm)],[547:[bind(A,$thf( ^ [E: $i] : ( sk1 @ ( D @ E ) ) ))]]) ).
thf(560,plain,
! [C: $i > $i > $o,B: $i > $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) ) )
| ~ ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( ( C
@ ( f
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) ) ) )
!= ( B @ A ) ) ),
inference(pre_uni,[status(thm)],[559:[]]) ).
thf(571,plain,
! [C: $i > $i > $o,B: $i > $i > $o,A: $i] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) ) )
| ~ ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( ( C
@ ( f
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) ) ) )
!= ( B @ A ) ) ),
inference(simp,[status(thm)],[560]) ).
thf(13589,plain,
sk9 = sk17,
inference(func_ext,[status(esa)],[12304]) ).
thf(13595,plain,
sk17 = sk9,
inference(lifteq,[status(thm)],[13589]) ).
thf(200,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] : $true ) )
!= ( cP @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[198,69]) ).
thf(201,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] : $true ) )
!= ( cP @ sk3 ) ),
inference(simp,[status(thm)],[200]) ).
thf(213,plain,
( ( sk2
@ ^ [A: $i] : $true )
!= sk3 ),
inference(simp,[status(thm)],[201]) ).
thf(25093,plain,
sk35 != sk3,
inference(rewrite,[status(thm)],[213,25073]) ).
thf(46,plain,
! [D: $i,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( A @ B )
| ~ $true
| ~ ( cP @ ( sk2 @ C ) )
| ( ( sk1 @ A )
!= ( C @ D ) ) ),
inference(paramod_ordered,[status(thm)],[11,17]) ).
thf(47,plain,
! [D: $i,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( A @ B )
| ~ ( cP @ ( sk2 @ C ) )
| ( ( sk1 @ A )
!= ( C @ D ) ) ),
inference(simp,[status(thm)],[46]) ).
thf(59,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ~ ( C @ B @ A )
| ~ ( cP
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) ) ) ),
inference(pre_uni,[status(thm)],[47:[bind(A,$thf( E @ D )),bind(B,$thf( B )),bind(C,$thf( ^ [F: $i] : ( sk1 @ ( E @ F ) ) ))]]) ).
thf(72,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ~ ( C @ B @ A )
| ~ ( cP
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) ) ) ),
inference(simp,[status(thm)],[59]) ).
thf(118,plain,
! [B: $i > $o,A: $i > $o] :
( ( A
@ ( f
@ ( sk2
@ ^ [C: $i] :
( ( A @ C )
| ( B @ C ) ) ) ) )
| ( B
@ ( f
@ ( sk2
@ ^ [C: $i] :
( ( A @ C )
| ( B @ C ) ) ) ) )
| ~ ( sk1
@ ^ [C: $i] :
( ( A @ C )
| ( B @ C ) ) ) ),
inference(prim_subst,[status(thm)],[7:[bind(A,$thf( ^ [D: $i] : ( ( B @ D ) | ( C @ D ) ) ))]]) ).
thf(142,plain,
! [B: $i > $o,A: $i > $o] :
( ( A
@ ( f
@ ( sk2
@ ^ [C: $i] :
( ( A @ C )
| ( B @ C ) ) ) ) )
| ( B
@ ( f
@ ( sk2
@ ^ [C: $i] :
( ( A @ C )
| ( B @ C ) ) ) ) )
| ~ ( sk1
@ ^ [C: $i] :
( ( A @ C )
| ( B @ C ) ) ) ),
inference(cnf,[status(esa)],[118]) ).
thf(143,plain,
! [B: $i > $o,A: $i > $o] :
( ( A
@ ( f
@ ( sk2
@ ^ [C: $i] :
( ( A @ C )
| ( B @ C ) ) ) ) )
| ( B
@ ( f
@ ( sk2
@ ^ [C: $i] :
( ( A @ C )
| ( B @ C ) ) ) ) )
| ~ ( sk1
@ ^ [C: $i] :
( ( A @ C )
| ( B @ C ) ) ) ),
inference(simp,[status(thm)],[142]) ).
thf(15499,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk21 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[15263,178]) ).
thf(15500,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk21 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[15499]) ).
thf(15501,plain,
( ( sk2 @ ( (=) @ $i @ sk21 ) )
!= a ),
inference(pattern_uni,[status(thm)],[15500:[bind(A,$thf( (=) @ $i @ sk21 ))]]) ).
thf(1769,plain,
( ~ $true
| ( ( cP @ ( sk2 @ cP ) )
!= ( cP @ sk7 ) ) ),
inference(paramod_ordered,[status(thm)],[1595,58]) ).
thf(1770,plain,
( ( cP @ ( sk2 @ cP ) )
!= ( cP @ sk7 ) ),
inference(simp,[status(thm)],[1769]) ).
thf(1799,plain,
( ( sk2 @ cP )
!= sk7 ),
inference(simp,[status(thm)],[1770]) ).
thf(21449,plain,
sk28 != sk7,
inference(rewrite,[status(thm)],[1799,21443]) ).
thf(173,plain,
( ~ $true
| ( ( cP @ ( sk2 @ cP ) )
!= ( cP @ a ) ) ),
inference(paramod_ordered,[status(thm)],[159,58]) ).
thf(174,plain,
( ( cP @ ( sk2 @ cP ) )
!= ( cP @ a ) ),
inference(simp,[status(thm)],[173]) ).
thf(176,plain,
( ( sk2 @ cP )
!= a ),
inference(simp,[status(thm)],[174]) ).
thf(21451,plain,
sk28 != a,
inference(rewrite,[status(thm)],[176,21443]) ).
thf(23224,plain,
( ( sk26 != sk26 )
| ( ( f @ sk28 )
!= ( f @ sk12 ) ) ),
inference(paramod_ordered,[status(thm)],[20901,22705]) ).
thf(23225,plain,
( ( f @ sk28 )
!= ( f @ sk12 ) ),
inference(simp,[status(thm)],[23224]) ).
thf(23229,plain,
sk28 != sk12,
inference(simp,[status(thm)],[23225]) ).
thf(316,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ( sk1 @ B )
| ( ( ~ $true )
!= ( B @ C ) )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( sk1 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[7,32]) ).
thf(317,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A )
| ( sk1 @ B )
| ( B @ C )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( sk1 @ B ) ) ),
inference(simp,[status(thm)],[316]) ).
thf(330,plain,
! [B: $i > $i > $o,A: $i] :
( ~ ( sk1
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) )
| ( sk1
@ ( B
@ ( f
@ ( sk2
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) ) ) ) )
| ( B
@ ( f
@ ( sk2
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) ) )
@ A ) ),
inference(pre_uni,[status(thm)],[317:[bind(A,$thf( ^ [E: $i] : ( sk1 @ ( D @ E ) ) )),bind(B,$thf( D @ ( f @ ( sk2 @ ^ [E: $i] : ( sk1 @ ( D @ E ) ) ) ) ))]]) ).
thf(351,plain,
! [B: $i > $i > $o,A: $i] :
( ~ ( sk1
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) )
| ( sk1
@ ( B
@ ( f
@ ( sk2
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) ) ) ) )
| ( B
@ ( f
@ ( sk2
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) ) )
@ A ) ),
inference(simp,[status(thm)],[330]) ).
thf(11798,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk8 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11171,218]) ).
thf(11799,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk8 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[11798]) ).
thf(11800,plain,
( ( sk2 @ ( (=) @ $i @ sk8 ) )
!= sk3 ),
inference(pattern_uni,[status(thm)],[11799:[bind(A,$thf( (=) @ $i @ sk8 ))]]) ).
thf(114,plain,
! [A: $i > $o] :
( ~ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] :
~ ( A @ B ) ) ) )
| ~ ( sk1
@ ^ [B: $i] :
~ ( A @ B ) ) ),
inference(prim_subst,[status(thm)],[7:[bind(A,$thf( ^ [C: $i] : ~ ( B @ C ) ))]]) ).
thf(138,plain,
! [A: $i > $o] :
( ~ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] :
~ ( A @ B ) ) ) )
| ~ ( sk1
@ ^ [B: $i] :
~ ( A @ B ) ) ),
inference(cnf,[status(esa)],[114]) ).
thf(139,plain,
! [A: $i > $o] :
( ~ ( A
@ ( f
@ ( sk2
@ ^ [B: $i] :
~ ( A @ B ) ) ) )
| ~ ( sk1
@ ^ [B: $i] :
~ ( A @ B ) ) ),
inference(simp,[status(thm)],[138]) ).
thf(12164,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk9 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11185,218]) ).
thf(12165,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= sk3 )
| ( ( sk1 @ ( (=) @ $i @ sk9 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[12164]) ).
thf(12166,plain,
( ( sk2 @ ( (=) @ $i @ sk9 ) )
!= sk3 ),
inference(pattern_uni,[status(thm)],[12165:[bind(A,$thf( (=) @ $i @ sk9 ))]]) ).
thf(20910,plain,
sk26 != sk7,
inference(rewrite,[status(thm)],[5376,20901]) ).
thf(1992,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ~ $true
| ( ( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ ( f @ B ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1359,5]) ).
thf(1993,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : ( cP @ ( f @ B ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[1992]) ).
thf(1994,plain,
~ ( cP
@ ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ ( f @ A ) ) ) ) ),
inference(pattern_uni,[status(thm)],[1993:[bind(A,$thf( ^ [B: $i] : ( sk1 @ ^ [C: $i] : ( cP @ ( f @ B ) ) ) ))]]) ).
thf(12652,plain,
sk7 = sk16,
inference(func_ext,[status(esa)],[12142]) ).
thf(12658,plain,
sk16 = sk7,
inference(lifteq,[status(thm)],[12652]) ).
thf(6631,plain,
! [A: $i] :
( ( A != sk3 )
| ( ( f @ ( sk2 @ ( (=) @ $i @ A ) ) )
!= ( f @ sk12 ) ) ),
inference(paramod_ordered,[status(thm)],[146,5379]) ).
thf(6822,plain,
( ( sk2 @ ( (=) @ $i @ sk3 ) )
!= sk12 ),
inference(simp,[status(thm)],[6631]) ).
thf(27,plain,
( ( sk1
@ ^ [A: $i] : $true )
| ~ $true ),
inference(prim_subst,[status(thm)],[11:[bind(A,$thf( ^ [C: $i] : $true ))]]) ).
thf(36,plain,
( sk1
@ ^ [A: $i] : $true ),
inference(simp,[status(thm)],[27]) ).
thf(14508,plain,
( ~ $true
| ( ( cP @ ( sk2 @ ( (=) @ $i @ sk3 ) ) )
!= ( cP @ sk7 ) ) ),
inference(paramod_ordered,[status(thm)],[1595,11488]) ).
thf(14509,plain,
( ( cP @ ( sk2 @ ( (=) @ $i @ sk3 ) ) )
!= ( cP @ sk7 ) ),
inference(simp,[status(thm)],[14508]) ).
thf(14551,plain,
( ( sk2 @ ( (=) @ $i @ sk3 ) )
!= sk7 ),
inference(simp,[status(thm)],[14509]) ).
thf(15579,plain,
sk21 = sk22,
inference(func_ext,[status(esa)],[15556]) ).
thf(15585,plain,
sk22 = sk21,
inference(lifteq,[status(thm)],[15579]) ).
thf(14264,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ~ $true
| ( ( sk1 @ ( (=) @ $i @ sk4 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11236,5]) ).
thf(14265,plain,
! [A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1 @ ( (=) @ $i @ sk4 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[14264]) ).
thf(14266,plain,
~ ( cP @ ( sk2 @ ( (=) @ $i @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[14265:[bind(A,$thf( (=) @ $i @ sk4 ))]]) ).
thf(625,plain,
! [D: $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( sk1 @ A )
| ( sk1
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) ) )
| ~ $true
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[7,40]) ).
thf(626,plain,
! [D: $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( sk1 @ A )
| ( sk1
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) ) )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( C @ B ) ) ),
inference(simp,[status(thm)],[625]) ).
thf(663,plain,
! [D: $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( sk1 @ A )
| ( sk1
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) ) )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( C @ B ) ) ),
inference(pre_uni,[status(thm)],[626:[]]) ).
thf(664,plain,
! [D: $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ( sk1
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) ) )
| ~ ( sk1 @ A )
| ( ( A @ ( f @ ( sk2 @ A ) ) )
!= ( C @ B ) ) ),
inference(pre_uni,[status(thm)],[663:[]]) ).
thf(11888,plain,
! [A: $i > $o] :
( ~ $true
| ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk8 ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11171,178]) ).
thf(11889,plain,
! [A: $i > $o] :
( ( ( sk2 @ A )
!= a )
| ( ( sk1 @ ( (=) @ $i @ sk8 ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[11888]) ).
thf(11890,plain,
( ( sk2 @ ( (=) @ $i @ sk8 ) )
!= a ),
inference(pattern_uni,[status(thm)],[11889:[bind(A,$thf( (=) @ $i @ sk8 ))]]) ).
thf(538,plain,
! [D: $i,C: $i > $o,B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ( sk1 @ C )
| ( ( ~ $true )
!= ( C @ D ) )
| ( ( sk1
@ ^ [E: $i] : ( sk1 @ ( B @ E ) ) )
!= ( sk1 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[35,32]) ).
thf(539,plain,
! [D: $i,C: $i > $o,B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ( sk1 @ C )
| ( C @ D )
| ( ( sk1
@ ^ [E: $i] : ( sk1 @ ( B @ E ) ) )
!= ( sk1 @ C ) ) ),
inference(simp,[status(thm)],[538]) ).
thf(540,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ~ ( sk1 @ ( C @ A ) )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( sk1 @ ( C @ B ) ) ),
inference(pattern_uni,[status(thm)],[539:[bind(A,$thf( A )),bind(B,$thf( E )),bind(C,$thf( ^ [F: $i] : ( sk1 @ ( E @ F ) ) ))]]) ).
thf(575,plain,
! [C: $i > $i > $o,B: $i,A: $i] :
( ~ ( sk1 @ ( C @ A ) )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( C @ D ) ) )
| ( sk1 @ ( C @ B ) ) ),
inference(simp,[status(thm)],[540]) ).
thf(52,plain,
! [B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ~ ( cP
@ ( sk2
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) ) ) ),
inference(prim_subst,[status(thm)],[17:[bind(A,$thf( ^ [D: $i] : ( sk1 @ ( C @ D ) ) ))]]) ).
thf(62,plain,
! [B: $i > $i > $o,A: $i] :
( ~ ( sk1 @ ( B @ A ) )
| ~ ( cP
@ ( sk2
@ ^ [C: $i] : ( sk1 @ ( B @ C ) ) ) ) ),
inference(simp,[status(thm)],[52]) ).
thf(1584,plain,
! [B: $i,A: $i > $o] :
( ~ $true
| ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1
@ ^ [C: $i] : ( cP @ sk7 ) )
!= ( A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[1468,17]) ).
thf(1585,plain,
! [B: $i,A: $i > $o] :
( ~ ( cP @ ( sk2 @ A ) )
| ( ( sk1
@ ^ [C: $i] : ( cP @ sk7 ) )
!= ( A @ B ) ) ),
inference(simp,[status(thm)],[1584]) ).
thf(1619,plain,
~ ( cP
@ ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ sk7 ) ) ) ),
inference(pre_uni,[status(thm)],[1585:[bind(A,$thf( ^ [C: $i] : ( sk1 @ ^ [D: $i] : ( cP @ sk7 ) ) )),bind(B,$thf( B ))]]) ).
thf(7181,plain,
~ ( cP
@ ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : $true ) ) ),
inference(rewrite,[status(thm)],[1619,1595]) ).
thf(354,plain,
! [C: $i,B: $i,A: $i > $o] :
( ~ ( A @ B )
| ( sk1 @ A )
| ( A @ C ) ),
inference(simp,[status(thm)],[302]) ).
thf(592,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ~ ( B @ A )
| ~ $true
| ( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
!= ( sk1
@ ^ [D: $i] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[40,141]) ).
thf(593,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ~ ( B @ A )
| ( ( sk1
@ ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
!= ( sk1
@ ^ [D: $i] : $false ) ) ),
inference(simp,[status(thm)],[592]) ).
thf(659,plain,
! [C: $i > $o,B: $i > $o,A: $i] :
( ~ ( B @ A )
| ( ( ^ [D: $i] :
( ( B @ D )
| ( C @ D ) ) )
!= ( ^ [D: $i] : $false ) ) ),
inference(simp,[status(thm)],[593]) ).
thf(1005,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) ) )
!= ( cP @ a ) ) ),
inference(paramod_ordered,[status(thm)],[159,741]) ).
thf(1006,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) ) )
!= ( cP @ a ) ),
inference(simp,[status(thm)],[1005]) ).
thf(1014,plain,
( ( sk2
@ ^ [A: $i] : ( cP @ ( f @ ( f @ A ) ) ) )
!= a ),
inference(simp,[status(thm)],[1006]) ).
thf(3613,plain,
( ~ $true
| ( ( cP
@ ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) ) )
!= ( cP @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[3487,1435]) ).
thf(3614,plain,
( ( cP
@ ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) ) )
!= ( cP @ sk9 ) ),
inference(simp,[status(thm)],[3613]) ).
thf(3669,plain,
( ( sk2
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : ( cP @ A ) ) )
!= sk9 ),
inference(simp,[status(thm)],[3614]) ).
thf(27582,plain,
$false,
inference(e,[status(thm)],[1190,6014,16501,23897,23255,24966,12334,6868,741,5,11485,1205,449,500,12494,670,23251,1275,21398,565,14553,1359,2328,2039,504,23896,1455,25090,196,1792,3644,902,5256,21447,284,2024,448,4265,1773,1109,3670,646,12610,21459,11480,61,6932,243,20905,20903,22386,15402,14445,6865,21444,11730,12576,137,33,12650,25095,3403,12461,6833,12304,11570,6852,22705,3667,23254,11488,1794,12142,141,499,14437,15410,20908,3671,212,1776,11965,15354,1246,41,14352,503,1241,1779,6859,1563,12486,21448,13603,11591,264,45,1595,180,17,32,34,1273,148,562,1615,2849,71,572,144,1239,3487,11973,2358,16500,14258,936,159,672,12096,23238,567,7,15352,737,103,21456,140,23899,24710,66,5318,11640,23249,198,23902,130,12006,135,1435,3,505,20907,35,21452,1018,355,145,490,675,12326,6012,11808,12174,1566,12256,67,4398,23246,15556,23894,3715,12416,23256,21455,1221,12014,11,175,571,11906,13595,25093,72,143,43,20901,15501,20906,218,21449,21451,23229,351,11800,139,786,40,12166,20910,1212,1994,287,12658,6822,36,146,14551,14375,15585,14266,136,268,11759,664,25073,11890,575,1357,62,178,7181,21443,354,659,11648,1014,3669]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO222^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.11/0.20 % Computer : n017.cluster.edu
% 0.11/0.20 % Model : x86_64 x86_64
% 0.11/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.20 % Memory : 8046.5625MB
% 0.11/0.20 % OS : Linux 6.8.0-71-generic
% 0.11/0.20 % CPULimit : 300
% 0.11/0.20 % WCLimit : 300
% 0.11/0.20 % DateTime : Tue Sep 29 16:35:22 UTC 2026
% 0.11/0.20 % CPUTime :
% 0.11/0.20 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.90/0.79 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.25/0.98 % [INFO] Parsing done (187ms).
% 1.25/0.99 % [INFO] Running in sequential loop mode.
% 2.04/1.41 % [INFO] eprover registered as external prover.
% 2.04/1.41 % [INFO] Scanning for conjecture ...
% 2.22/1.51 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.22/1.54 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.22/1.54 % [INFO] Problem is higher-order (TPTP THF).
% 2.22/1.55 % [INFO] Type checking passed.
% 2.22/1.55 % [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 ...
% 88.95/18.89 % External prover 'e' found a proof!
% 88.95/18.89 % [INFO] Killing All external provers ...
% 88.95/18.89 % Time passed: 18550ms (effective reasoning time: 17896ms)
% 88.95/18.90 % 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)>
% 75.02/18.90 % Axioms used in derivation (0):
% 75.02/18.90 % No. of inferences in proof: 729
% 75.02/18.90 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 18550 ms resp. 17896 ms w/o parsing
% 91.19/19.18 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 91.19/19.18 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------