%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEU875^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:29:30 AM UTC 2026
% Result : Theorem 86.79s 17.90s
% Output : Refutation 88.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 6
% Syntax : Number of formulae : 614 ( 30 unt; 0 typ; 5 def)
% Number of atoms : 3879 (1140 equ; 82 cnn)
% Maximal formula atoms : 49 ( 6 avg)
% Number of connectives : 6907 (1372 ~;1840 |; 58 &;3599 @)
% ( 0 <=>; 38 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 7 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 438 ( 438 >; 0 *; 0 +; 0 <<)
% Number of symbols : 36 ( 32 usr; 15 con; 0-2 aty)
% Number of variables : 1645 ( 904 ^; 732 !; 4 ?;1645 :)
% ( 0 !>; 0 ?*; 0 @-; 5 @+)
% Comments :
%------------------------------------------------------------------------------
thf(a_type,type,
a: $tType ).
thf(t_decl,type,
t: a ).
thf(cA_decl,type,
cA: ( a > $o ) > $o ).
thf(sk1_decl,type,
sk1: $o ).
thf(sk2_decl,type,
sk2: a > $o ).
thf(sk3_decl,type,
sk3: a > $o ).
thf(sk4_decl,type,
sk4: ( a > $o ) > $o ).
thf(sk5_decl,type,
sk5: ( a > $o ) > ( a > $o ) > $o ).
thf(sk6_decl,type,
sk6: ( a > $o ) > $o ).
thf(sk7_decl,type,
sk7: ( a > $o ) > a ).
thf(sk8_decl,type,
sk8: ( a > $o ) > a > $o ).
thf(sk9_decl,type,
sk9: a ).
thf(sk10_decl,type,
sk10: a ).
thf(sk13_decl,type,
sk13: a > a ).
thf(sk15_decl,type,
sk15: a ).
thf(sk16_decl,type,
sk16: a ).
thf(sk17_decl,type,
sk17: a ).
thf(sk18_decl,type,
sk18: a > a ).
thf(sk19_decl,type,
sk19: a > a ).
thf(sk21_decl,type,
sk21: a > a ).
thf(sk22_decl,type,
sk22: a > a > a ).
thf(sk23_decl,type,
sk23: a ).
thf(sk25_decl,type,
sk25: a ).
thf(sk26_decl,type,
sk26: a > a ).
thf(sk27_decl,type,
sk27: a > a ).
thf(sk28_decl,type,
sk28: a > a ).
thf(sk30_decl,type,
sk30: a > a ).
thf(sk33_decl,type,
sk33: a ).
thf(sk35_decl,type,
sk35: a ).
thf(sk36_decl,type,
sk36: a ).
thf(sk37_decl,type,
sk37: a > a ).
thf(sk43_decl,type,
sk43: a > a ).
thf(sk44_decl,type,
sk44: a > a ).
thf(sk2_def,definition,
( sk2
= ( @+[A: a > $o] :
~ ( ( ( cA @ A )
& ( A @ t ) )
=> ( cA @ A ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: a > $o] :
~ ( ( ( cA @ A )
& ( A @ t ) )
=> ? [B: a > $o] :
( ! [C: ( a > $o ) > $o] :
( ( ( C
@ ^ [D: a] : $false )
& ! [D: a > $o] :
( ( C @ D )
=> ! [E: a] :
( ( B @ E )
=> ( C
@ ^ [F: a] :
( ( D @ F )
| ( E = F ) ) ) ) ) )
=> ( C @ B ) )
& ! [C: a] :
( ( B @ C )
=> ( A @ C ) )
& ! [C: a > $o] :
( ( ( cA @ C )
& ! [D: a] :
( ( B @ D )
=> ( C @ D ) ) )
=> ( ( cA @ C )
& ( C @ t ) ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: a > $o] :
@+[B: ( a > $o ) > $o] :
~ ( ( ( B
@ ^ [C: a] : $false )
& ! [C: a > $o] :
( ( B @ C )
=> ! [D: a] :
( ( A @ D )
=> ( B
@ ^ [E: a] :
( ( C @ E )
| ( D = E ) ) ) ) ) )
=> ( B @ A ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: a > $o] :
@+[B: a] :
~ ( ( A @ B )
=> ( sk3 @ B ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: a > $o] :
@+[B: a > $o] :
~ ( ( ( cA @ B )
& ! [C: a] :
( ( A @ C )
=> ( B @ C ) ) )
=> ( ( cA @ B )
& ( B @ t ) ) ) ) ) ).
thf(1,conjecture,
( ! [A: a > $o] :
( ( ( cA @ A )
& ( A @ t ) )
=> ( cA @ A ) )
& ! [A: a > $o] :
( ( ( cA @ A )
& ( A @ t ) )
=> ? [B: a > $o] :
( ! [C: ( a > $o ) > $o] :
( ( ( C
@ ^ [D: a] : $false )
& ! [D: a > $o] :
( ( C @ D )
=> ! [E: a] :
( ( B @ E )
=> ( C
@ ^ [F: a] :
( ( D @ F )
| ( E = F ) ) ) ) ) )
=> ( C @ B ) )
& ! [C: a] :
( ( B @ C )
=> ( A @ C ) )
& ! [C: a > $o] :
( ( ( cA @ C )
& ! [D: a] :
( ( B @ D )
=> ( C @ D ) ) )
=> ( ( cA @ C )
& ( C @ t ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cDOMLEMMA5_pme) ).
thf(2,negated_conjecture,
~ ( ! [A: a > $o] :
( ( ( cA @ A )
& ( A @ t ) )
=> ( cA @ A ) )
& ! [A: a > $o] :
( ( ( cA @ A )
& ( A @ t ) )
=> ? [B: a > $o] :
( ! [C: ( a > $o ) > $o] :
( ( ( C
@ ^ [D: a] : $false )
& ! [D: a > $o] :
( ( C @ D )
=> ! [E: a] :
( ( B @ E )
=> ( C
@ ^ [F: a] :
( ( D @ F )
| ( E = F ) ) ) ) ) )
=> ( C @ B ) )
& ! [C: a] :
( ( B @ C )
=> ( A @ C ) )
& ! [C: a > $o] :
( ( ( cA @ C )
& ! [D: a] :
( ( B @ D )
=> ( C @ D ) ) )
=> ( ( cA @ C )
& ( C @ t ) ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ( ! [A: a > $o] :
( ( ( cA @ A )
& ( A @ t ) )
=> ( cA @ A ) )
& ! [A: a > $o] :
( ( ( cA @ A )
& ( A @ t ) )
=> ? [B: a > $o] :
( ! [C: ( a > $o ) > $o] :
( ( ( C
@ ^ [D: a] : $false )
& ! [D: a > $o] :
( ( C @ D )
=> ! [E: a] :
( ( B @ E )
=> ( C
@ ^ [F: a] :
( ( D @ F )
| ( E = F ) ) ) ) ) )
=> ( C @ B ) )
& ! [C: a] :
( ( B @ C )
=> ( A @ C ) )
& ! [C: a > $o] :
( ( ( cA @ C )
& ! [D: a] :
( ( B @ D )
=> ( C @ D ) ) )
=> ( ( cA @ C )
& ( C @ t ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
! [D: a,C: a,B: a > $o,A: a > $o] :
( ( ( cA @ sk2 )
| ~ sk1 )
& ( ( sk2 @ t )
| ~ sk1 )
& ( ~ ( cA @ sk2 )
| ~ sk1 )
& ( sk1
| ( cA @ sk3 ) )
& ( sk1
| ( sk3 @ t ) )
& ( sk1
| ( sk5 @ A
@ ^ [E: a] : $false )
| ~ ( sk4 @ A ) )
& ( sk1
| ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ( sk5 @ A
@ ^ [E: a] :
( ( B @ E )
| ( C = E ) ) )
| ~ ( sk4 @ A ) )
& ( sk1
| ~ ( sk5 @ A @ A )
| ~ ( sk4 @ A ) )
& ( sk1
| ( sk4 @ A )
| ( A @ ( sk7 @ A ) )
| ~ ( sk6 @ A ) )
& ( sk1
| ( sk4 @ A )
| ~ ( sk3 @ ( sk7 @ A ) )
| ~ ( sk6 @ A ) )
& ( sk1
| ( sk4 @ A )
| ( sk6 @ A )
| ( cA @ ( sk8 @ A ) ) )
& ( sk1
| ( sk4 @ A )
| ( sk6 @ A )
| ~ ( A @ D )
| ( sk8 @ A @ D ) )
& ( sk1
| ( sk4 @ A )
| ( sk6 @ A )
| ~ ( cA @ ( sk8 @ A ) )
| ~ ( sk8 @ A @ t ) ) ),
inference(cnf,[status(esa)],[3]) ).
thf(6,plain,
( sk1
| ( sk3 @ t ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(17,plain,
( ( cA @ sk2 )
| ~ sk1 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(14,plain,
( ~ ( cA @ sk2 )
| ~ sk1 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(88,plain,
( ~ sk1
| ~ $true
| ~ sk1
| ( ( cA @ sk2 )
!= ( cA @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[17,14]) ).
thf(89,plain,
( ~ sk1
| ( ( cA @ sk2 )
!= ( cA @ sk2 ) ) ),
inference(simp,[status(thm)],[88]) ).
thf(90,plain,
~ sk1,
inference(pattern_uni,[status(thm)],[89:[]]) ).
thf(93,plain,
( $false
| ( sk3 @ t ) ),
inference(rewrite,[status(thm)],[6,90]) ).
thf(94,plain,
sk3 @ t,
inference(simp,[status(thm)],[93]) ).
thf(9,plain,
! [B: a,A: a > $o] :
( sk1
| ( sk4 @ A )
| ( sk6 @ A )
| ~ ( A @ B )
| ( sk8 @ A @ B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(18,plain,
! [B: a,A: a > $o] :
( sk1
| ( sk4 @ A )
| ( sk6 @ A )
| ~ ( A @ B )
| ( sk8 @ A @ B ) ),
inference(simp,[status(thm)],[9]) ).
thf(446,plain,
! [B: a,A: a > $o] :
( $false
| ( sk4 @ A )
| ( sk6 @ A )
| ~ ( A @ B )
| ( sk8 @ A @ B ) ),
inference(rewrite,[status(thm)],[18,90]) ).
thf(447,plain,
! [B: a,A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ~ ( A @ B )
| ( sk8 @ A @ B ) ),
inference(simp,[status(thm)],[446]) ).
thf(478,plain,
! [B: a,A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ~ $true
| ( sk8 @ A @ B )
| ( ( sk3 @ t )
!= ( A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[94,447]) ).
thf(479,plain,
! [B: a,A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ( sk8 @ A @ B )
| ( ( sk3 @ t )
!= ( A @ B ) ) ),
inference(simp,[status(thm)],[478]) ).
thf(520,plain,
( ( sk4 @ sk3 )
| ( sk6 @ sk3 )
| ( sk8 @ sk3 @ t ) ),
inference(pre_uni,[status(thm)],[479:[bind(A,$thf( sk3 )),bind(B,$thf( t ))]]) ).
thf(12,plain,
! [A: a > $o] :
( sk1
| ( sk4 @ A )
| ( sk6 @ A )
| ( cA @ ( sk8 @ A ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(97,plain,
! [A: a > $o] :
( $false
| ( sk4 @ A )
| ( sk6 @ A )
| ( cA @ ( sk8 @ A ) ) ),
inference(rewrite,[status(thm)],[12,90]) ).
thf(98,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ( cA @ ( sk8 @ A ) ) ),
inference(simp,[status(thm)],[97]) ).
thf(7,plain,
! [A: a > $o] :
( sk1
| ( sk4 @ A )
| ( A @ ( sk7 @ A ) )
| ~ ( sk6 @ A ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(174,plain,
! [A: a > $o] :
( $false
| ( sk4 @ A )
| ( A @ ( sk7 @ A ) )
| ~ ( sk6 @ A ) ),
inference(rewrite,[status(thm)],[7,90]) ).
thf(175,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( A @ ( sk7 @ A ) )
| ~ ( sk6 @ A ) ),
inference(simp,[status(thm)],[174]) ).
thf(11,plain,
! [A: a > $o] :
( sk1
| ( sk4 @ A )
| ~ ( sk3 @ ( sk7 @ A ) )
| ~ ( sk6 @ A ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(161,plain,
! [A: a > $o] :
( $false
| ( sk4 @ A )
| ~ ( sk3 @ ( sk7 @ A ) )
| ~ ( sk6 @ A ) ),
inference(rewrite,[status(thm)],[11,90]) ).
thf(162,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ~ ( sk3 @ ( sk7 @ A ) )
| ~ ( sk6 @ A ) ),
inference(simp,[status(thm)],[161]) ).
thf(199,plain,
! [B: a > $o,A: a > $o] :
( ( sk4 @ A )
| ~ ( sk6 @ A )
| ( sk4 @ B )
| ~ $true
| ~ ( sk6 @ B )
| ( ( A @ ( sk7 @ A ) )
!= ( sk3 @ ( sk7 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,162]) ).
thf(200,plain,
! [B: a > $o,A: a > $o] :
( ( sk4 @ A )
| ~ ( sk6 @ A )
| ( sk4 @ B )
| ~ ( sk6 @ B )
| ( ( A @ ( sk7 @ A ) )
!= ( sk3 @ ( sk7 @ B ) ) ) ),
inference(simp,[status(thm)],[199]) ).
thf(236,plain,
( ( sk4 @ sk3 )
| ~ ( sk6 @ sk3 )
| ( sk4 @ sk3 )
| ~ ( sk6 @ sk3 ) ),
inference(pre_uni,[status(thm)],[200:[bind(A,$thf( sk3 )),bind(B,$thf( sk3 ))]]) ).
thf(263,plain,
( ( sk4 @ sk3 )
| ~ ( sk6 @ sk3 ) ),
inference(simp,[status(thm)],[236]) ).
thf(287,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( cA @ ( sk8 @ A ) )
| ( sk4 @ sk3 )
| ~ $true
| ( ( sk6 @ A )
!= ( sk6 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[98,263]) ).
thf(288,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( cA @ ( sk8 @ A ) )
| ( sk4 @ sk3 )
| ( ( sk6 @ A )
!= ( sk6 @ sk3 ) ) ),
inference(simp,[status(thm)],[287]) ).
thf(289,plain,
( ( sk4 @ sk3 )
| ( cA @ ( sk8 @ sk3 ) )
| ( sk4 @ sk3 ) ),
inference(pattern_uni,[status(thm)],[288:[bind(A,$thf( sk3 ))]]) ).
thf(293,plain,
( ( sk4 @ sk3 )
| ( cA @ ( sk8 @ sk3 ) ) ),
inference(simp,[status(thm)],[289]) ).
thf(10,plain,
! [A: a > $o] :
( sk1
| ( sk4 @ A )
| ( sk6 @ A )
| ~ ( cA @ ( sk8 @ A ) )
| ~ ( sk8 @ A @ t ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(346,plain,
! [A: a > $o] :
( $false
| ( sk4 @ A )
| ( sk6 @ A )
| ~ ( cA @ ( sk8 @ A ) )
| ~ ( sk8 @ A @ t ) ),
inference(rewrite,[status(thm)],[10,90]) ).
thf(347,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ~ ( cA @ ( sk8 @ A ) )
| ~ ( sk8 @ A @ t ) ),
inference(simp,[status(thm)],[346]) ).
thf(350,plain,
! [A: a > $o] :
( ( sk4 @ sk3 )
| ( sk4 @ A )
| ( sk6 @ A )
| ~ $true
| ~ ( sk8 @ A @ t )
| ( ( cA @ ( sk8 @ sk3 ) )
!= ( cA @ ( sk8 @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[293,347]) ).
thf(351,plain,
! [A: a > $o] :
( ( sk4 @ sk3 )
| ( sk4 @ A )
| ( sk6 @ A )
| ~ ( sk8 @ A @ t )
| ( ( cA @ ( sk8 @ sk3 ) )
!= ( cA @ ( sk8 @ A ) ) ) ),
inference(simp,[status(thm)],[350]) ).
thf(352,plain,
( ( sk4 @ sk3 )
| ( sk4 @ sk3 )
| ( sk6 @ sk3 )
| ~ ( sk8 @ sk3 @ t ) ),
inference(pattern_uni,[status(thm)],[351:[bind(A,$thf( sk3 ))]]) ).
thf(383,plain,
( ( sk4 @ sk3 )
| ( sk6 @ sk3 )
| ~ ( sk8 @ sk3 @ t ) ),
inference(simp,[status(thm)],[352]) ).
thf(3714,plain,
( ( sk4 @ sk3 )
| ( sk6 @ sk3 )
| ( sk4 @ sk3 )
| ( sk6 @ sk3 )
| ~ $true
| ( ( sk8 @ sk3 @ t )
!= ( sk8 @ sk3 @ t ) ) ),
inference(paramod_ordered,[status(thm)],[520,383]) ).
thf(3715,plain,
( ( sk4 @ sk3 )
| ( sk6 @ sk3 )
| ( ( sk8 @ sk3 @ t )
!= ( sk8 @ sk3 @ t ) ) ),
inference(simp,[status(thm)],[3714]) ).
thf(3716,plain,
( ( sk4 @ sk3 )
| ( sk6 @ sk3 ) ),
inference(pattern_uni,[status(thm)],[3715:[]]) ).
thf(3957,plain,
( ( sk4 @ sk3 )
| ( sk4 @ sk3 )
| ~ $true
| ( ( sk6 @ sk3 )
!= ( sk6 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[3716,263]) ).
thf(3958,plain,
( ( sk4 @ sk3 )
| ( ( sk6 @ sk3 )
!= ( sk6 @ sk3 ) ) ),
inference(simp,[status(thm)],[3957]) ).
thf(3959,plain,
sk4 @ sk3,
inference(pattern_uni,[status(thm)],[3958:[]]) ).
thf(5,plain,
! [A: a > $o] :
( sk1
| ( sk5 @ A
@ ^ [B: a] : $false )
| ~ ( sk4 @ A ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(103,plain,
! [A: a > $o] :
( $false
| ( sk5 @ A
@ ^ [B: a] : $false )
| ~ ( sk4 @ A ) ),
inference(rewrite,[status(thm)],[5,90]) ).
thf(104,plain,
! [A: a > $o] :
( ( sk5 @ A
@ ^ [B: a] : $false )
| ~ ( sk4 @ A ) ),
inference(simp,[status(thm)],[103]) ).
thf(4039,plain,
! [A: a > $o] :
( ( sk5 @ A
@ ^ [B: a] : $false )
| ~ $true
| ( ( sk4 @ sk3 )
!= ( sk4 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3959,104]) ).
thf(4040,plain,
! [A: a > $o] :
( ( sk5 @ A
@ ^ [B: a] : $false )
| ( ( sk4 @ sk3 )
!= ( sk4 @ A ) ) ),
inference(simp,[status(thm)],[4039]) ).
thf(4041,plain,
( sk5 @ sk3
@ ^ [A: a] : $false ),
inference(pattern_uni,[status(thm)],[4040:[bind(A,$thf( sk3 ))]]) ).
thf(16,plain,
! [C: a,B: a > $o,A: a > $o] :
( sk1
| ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ( sk5 @ A
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ~ ( sk4 @ A ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(37,plain,
! [C: a,B: a > $o,A: a > $o] :
( sk1
| ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ( sk5 @ A
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ( ( sk4 @ A )
!= ( A @ C ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[16]) ).
thf(47,plain,
! [C: a,B: a > $o,A: a > $o] :
( sk1
| ( sk5 @ A
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ( ( sk4 @ A )
!= ( A @ C ) ) ),
inference(simp,[status(thm)],[37]) ).
thf(785,plain,
! [C: a,B: a > $o,A: a > $o] :
( $false
| ( sk5 @ A
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ( ( sk4 @ A )
!= ( A @ C ) ) ),
inference(rewrite,[status(thm)],[47,90]) ).
thf(786,plain,
! [C: a,B: a > $o,A: a > $o] :
( ( sk5 @ A
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ( ( sk4 @ A )
!= ( A @ C ) ) ),
inference(simp,[status(thm)],[785]) ).
thf(13,plain,
! [A: a > $o] :
( sk1
| ~ ( sk5 @ A @ A )
| ~ ( sk4 @ A ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(95,plain,
! [A: a > $o] :
( $false
| ~ ( sk5 @ A @ A )
| ~ ( sk4 @ A ) ),
inference(rewrite,[status(thm)],[13,90]) ).
thf(96,plain,
! [A: a > $o] :
( ~ ( sk5 @ A @ A )
| ~ ( sk4 @ A ) ),
inference(simp,[status(thm)],[95]) ).
thf(850,plain,
! [D: a > $o,C: a,B: a > $o,A: a > $o] :
( ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ( ( sk4 @ A )
!= ( A @ C ) )
| ~ $true
| ~ ( sk4 @ D )
| ( ( sk5 @ A
@ ^ [E: a] :
( ( B @ E )
| ( C = E ) ) )
!= ( sk5 @ D @ D ) ) ),
inference(paramod_ordered,[status(thm)],[786,96]) ).
thf(851,plain,
! [D: a > $o,C: a,B: a > $o,A: a > $o] :
( ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ( ( sk4 @ A )
!= ( A @ C ) )
| ~ ( sk4 @ D )
| ( ( sk5 @ A
@ ^ [E: a] :
( ( B @ E )
| ( C = E ) ) )
!= ( sk5 @ D @ D ) ) ),
inference(simp,[status(thm)],[850]) ).
thf(852,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( ( B @ A )
| ( A = A ) )
| ( ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
!= ( ( B @ A )
| ( A = A ) ) )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) ),
inference(pattern_uni,[status(thm)],[851:[bind(A,$thf( ^ [F: a] : ( ( E @ F ) | ( C = F ) ) )),bind(B,$thf( E )),bind(C,$thf( C )),bind(D,$thf( ^ [F: a] : ( ( E @ F ) | ( C = F ) ) ))]]) ).
thf(1028,plain,
! [B: a > $o,A: a] :
( ( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( B @ A )
| ( ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
!= ( ( B @ A )
| ( A = A ) ) )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) )
& ( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ( A != A )
| ( ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
!= ( ( B @ A )
| ( A = A ) ) )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) ) ),
inference(cnf,[status(esa)],[852]) ).
thf(1030,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ( A != A )
| ( ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
!= ( ( B @ A )
| ( A = A ) ) )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) ),
inference(cnfConj,[status(thm)],[1028]) ).
thf(1032,plain,
! [B: a > $o,A: a] :
( ( A != A )
| ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ( ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
!= ( ( B @ A )
| ( A = A ) ) )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) ),
inference(lifteq,[status(thm)],[1030]) ).
thf(1033,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) ),
inference(simp,[status(thm)],[1032]) ).
thf(1059,plain,
! [C: a > $o,B: a,A: a > $o] :
( ~ ( sk4 @ A )
| ~ $true
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( B = D ) ) )
| ( ( sk5 @ A
@ ^ [D: a] : $false )
!= ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( B = D ) )
@ C ) ) ),
inference(paramod_ordered,[status(thm)],[104,1033]) ).
thf(1060,plain,
! [C: a > $o,B: a,A: a > $o] :
( ~ ( sk4 @ A )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( B = D ) ) )
| ( ( sk5 @ A
@ ^ [D: a] : $false )
!= ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( B = D ) )
@ C ) ) ),
inference(simp,[status(thm)],[1059]) ).
thf(1061,plain,
! [A: a] :
( ~ ( sk4
@ ^ [B: a] :
( $false
| ( A = B ) ) )
| ~ ( sk4
@ ^ [B: a] :
( $false
| ( A = B ) ) ) ),
inference(pattern_uni,[status(thm)],[1060:[bind(A,$thf( ^ [D: a] : ( $false | ( B = D ) ) )),bind(B,$thf( B )),bind(C,$thf( ^ [D: a] : $false ))]]) ).
thf(1080,plain,
! [A: a] :
~ ( sk4 @ ( (=) @ a @ A ) ),
inference(simp,[status(thm)],[1061]) ).
thf(4025,plain,
! [A: a] :
( ~ $true
| ( ( sk4 @ sk3 )
!= ( sk4 @ ( (=) @ a @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[3959,1080]) ).
thf(4026,plain,
! [A: a] :
( ( sk4 @ sk3 )
!= ( sk4 @ ( (=) @ a @ A ) ) ),
inference(simp,[status(thm)],[4025]) ).
thf(4048,plain,
! [A: a] :
( sk3
!= ( (=) @ a @ A ) ),
inference(simp,[status(thm)],[4026]) ).
thf(4237,plain,
! [A: a] :
( ( sk3 @ ( sk21 @ A ) )
!= ( A
= ( sk21 @ A ) ) ),
inference(func_ext,[status(esa)],[4048]) ).
thf(4441,plain,
! [A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( A
= ( sk21 @ A ) ) ),
inference(bool_ext,[status(thm)],[4237]) ).
thf(4451,plain,
! [A: a] :
( ( ( sk21 @ A )
= A )
| ( sk3 @ ( sk21 @ A ) ) ),
inference(lifteq,[status(thm)],[4441]) ).
thf(21,plain,
! [C: a,B: a > $o,A: a > $o] :
( sk1
| sk1
| ~ ( sk5 @ A @ B )
| ~ $true
| ( sk5 @ A
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ~ ( sk4 @ A )
| ( ( sk3 @ t )
!= ( A @ C ) ) ),
inference(paramod_ordered,[status(thm)],[6,16]) ).
thf(22,plain,
! [C: a,B: a > $o,A: a > $o] :
( sk1
| ~ ( sk5 @ A @ B )
| ( sk5 @ A
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ~ ( sk4 @ A )
| ( ( sk3 @ t )
!= ( A @ C ) ) ),
inference(simp,[status(thm)],[21]) ).
thf(50,plain,
! [A: a > $o] :
( sk1
| ~ ( sk5 @ sk3 @ A )
| ( sk5 @ sk3
@ ^ [B: a] :
( ( A @ B )
| ( t = B ) ) )
| ~ ( sk4 @ sk3 ) ),
inference(pre_uni,[status(thm)],[22:[bind(A,$thf( sk3 )),bind(B,$thf( B )),bind(C,$thf( t ))]]) ).
thf(68,plain,
! [A: a > $o] :
( sk1
| ~ ( sk5 @ sk3 @ A )
| ( sk5 @ sk3
@ ^ [B: a] :
( ( A @ B )
| ( t = B ) ) )
| ~ ( sk4 @ sk3 ) ),
inference(simp,[status(thm)],[50]) ).
thf(5180,plain,
! [A: a > $o] :
( $false
| ~ ( sk5 @ sk3 @ A )
| ( sk5 @ sk3
@ ^ [B: a] :
( ( A @ B )
| ( t = B ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[68,3959,90]) ).
thf(5181,plain,
! [A: a > $o] :
( ~ ( sk5 @ sk3 @ A )
| ( sk5 @ sk3
@ ^ [B: a] :
( ( A @ B )
| ( t = B ) ) ) ),
inference(simp,[status(thm)],[5180]) ).
thf(5186,plain,
! [A: a > $o] :
( ~ $true
| ( sk5 @ sk3
@ ^ [B: a] :
( ( A @ B )
| ( t = B ) ) )
| ( ( sk5 @ sk3
@ ^ [B: a] : $false )
!= ( sk5 @ sk3 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[4041,5181]) ).
thf(5187,plain,
! [A: a > $o] :
( ( sk5 @ sk3
@ ^ [B: a] :
( ( A @ B )
| ( t = B ) ) )
| ( ( sk5 @ sk3
@ ^ [B: a] : $false )
!= ( sk5 @ sk3 @ A ) ) ),
inference(simp,[status(thm)],[5186]) ).
thf(5188,plain,
( sk5 @ sk3
@ ^ [A: a] :
( $false
| ( t = A ) ) ),
inference(pattern_uni,[status(thm)],[5187:[bind(A,$thf( ^ [B: a] : $false ))]]) ).
thf(5356,plain,
sk5 @ sk3 @ ( (=) @ a @ t ),
inference(simp,[status(thm)],[5188]) ).
thf(3993,plain,
! [A: a > $o] :
( ~ ( sk5 @ A @ A )
| ~ $true
| ( ( sk4 @ sk3 )
!= ( sk4 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3959,96]) ).
thf(3994,plain,
! [A: a > $o] :
( ~ ( sk5 @ A @ A )
| ( ( sk4 @ sk3 )
!= ( sk4 @ A ) ) ),
inference(simp,[status(thm)],[3993]) ).
thf(3995,plain,
~ ( sk5 @ sk3 @ sk3 ),
inference(pattern_uni,[status(thm)],[3994:[bind(A,$thf( sk3 ))]]) ).
thf(5395,plain,
( ~ $true
| ( ( sk5 @ sk3 @ sk3 )
!= ( sk5 @ sk3 @ ( (=) @ a @ t ) ) ) ),
inference(paramod_ordered,[status(thm)],[5356,3995]) ).
thf(5396,plain,
( ( sk5 @ sk3 @ sk3 )
!= ( sk5 @ sk3 @ ( (=) @ a @ t ) ) ),
inference(simp,[status(thm)],[5395]) ).
thf(5445,plain,
( ( sk3 != sk3 )
| ( sk3
!= ( (=) @ a @ t ) ) ),
inference(simp,[status(thm)],[5396]) ).
thf(5483,plain,
( sk3
!= ( (=) @ a @ t ) ),
inference(simp,[status(thm)],[5445]) ).
thf(5513,plain,
( ( sk3 @ sk33 )
!= ( t = sk33 ) ),
inference(func_ext,[status(esa)],[5483]) ).
thf(5515,plain,
( ( sk3 @ sk33 )
| ( t = sk33 ) ),
inference(bool_ext,[status(thm)],[5513]) ).
thf(5523,plain,
( ( sk33 = t )
| ( sk3 @ sk33 ) ),
inference(lifteq,[status(thm)],[5515]) ).
thf(5514,plain,
( ~ ( sk3 @ sk33 )
| ( t != sk33 ) ),
inference(bool_ext,[status(thm)],[5513]) ).
thf(5526,plain,
( ( sk33 != t )
| ~ ( sk3 @ sk33 ) ),
inference(lifteq,[status(thm)],[5514]) ).
thf(5602,plain,
( ( sk33 != t )
| ~ $true
| ( ( sk3 @ sk33 )
!= ( sk3 @ t ) ) ),
inference(paramod_ordered,[status(thm)],[94,5526]) ).
thf(5603,plain,
( ( sk33 != t )
| ( ( sk3 @ sk33 )
!= ( sk3 @ t ) ) ),
inference(simp,[status(thm)],[5602]) ).
thf(5605,plain,
( ( sk33 != t )
| ( sk33 != t ) ),
inference(simp,[status(thm)],[5603]) ).
thf(5610,plain,
sk33 != t,
inference(simp,[status(thm)],[5605]) ).
thf(5611,plain,
sk3 @ sk33,
inference(simplifyReflect,[status(thm)],[5523,5610]) ).
thf(4440,plain,
! [A: a] :
( ~ ( sk3 @ ( sk21 @ A ) )
| ( A
!= ( sk21 @ A ) ) ),
inference(bool_ext,[status(thm)],[4237]) ).
thf(4447,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ~ ( sk3 @ ( sk21 @ A ) ) ),
inference(lifteq,[status(thm)],[4440]) ).
thf(12432,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ~ $true
| ( ( sk3 @ ( sk21 @ A ) )
!= ( sk3 @ sk33 ) ) ),
inference(paramod_ordered,[status(thm)],[5611,4447]) ).
thf(12433,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ( ( sk3 @ ( sk21 @ A ) )
!= ( sk3 @ sk33 ) ) ),
inference(simp,[status(thm)],[12432]) ).
thf(12451,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ( ( sk21 @ A )
!= sk33 ) ),
inference(simp,[status(thm)],[12433]) ).
thf(14501,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ( ( sk21 @ A )
!= ( sk21 @ A ) )
| ( sk33 != A ) ),
inference(eqfactor_ordered,[status(thm)],[12451]) ).
thf(14502,plain,
( ( sk21 @ sk33 )
!= sk33 ),
inference(pattern_uni,[status(thm)],[14501:[bind(A,$thf( sk33 ))]]) ).
thf(14505,plain,
! [A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( A != sk33 )
| ( ( sk21 @ A )
!= ( sk21 @ sk33 ) ) ),
inference(paramod_ordered,[status(thm)],[4451,14502]) ).
thf(14506,plain,
( ( sk3 @ ( sk21 @ sk33 ) )
| ( sk33 != sk33 ) ),
inference(pattern_uni,[status(thm)],[14505:[bind(A,$thf( sk33 ))]]) ).
thf(14507,plain,
sk3 @ ( sk21 @ sk33 ),
inference(simp,[status(thm)],[14506]) ).
thf(44,plain,
! [B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [C: a] : $true
@ A )
| ~ $true
| ( sk5
@ ^ [C: a] : $true
@ ^ [C: a] :
( ( A @ C )
| ( B = C ) ) )
| ~ ( sk4
@ ^ [C: a] : $true ) ),
inference(prim_subst,[status(thm)],[16:[bind(A,$thf( ^ [D: a] : $true ))]]) ).
thf(63,plain,
! [B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [C: a] : $true
@ A )
| ( sk5
@ ^ [C: a] : $true
@ ^ [C: a] :
( ( A @ C )
| ( B = C ) ) )
| ~ ( sk4
@ ^ [C: a] : $true ) ),
inference(simp,[status(thm)],[44]) ).
thf(3734,plain,
! [B: a,A: a > $o] :
( $false
| ~ ( sk5
@ ^ [C: a] : $true
@ A )
| ( sk5
@ ^ [C: a] : $true
@ ^ [C: a] :
( ( A @ C )
| ( B = C ) ) )
| ~ ( sk4
@ ^ [C: a] : $true ) ),
inference(rewrite,[status(thm)],[63,90]) ).
thf(3735,plain,
! [B: a,A: a > $o] :
( ~ ( sk5
@ ^ [C: a] : $true
@ A )
| ( sk5
@ ^ [C: a] : $true
@ ^ [C: a] :
( ( A @ C )
| ( B = C ) ) )
| ~ ( sk4
@ ^ [C: a] : $true ) ),
inference(simp,[status(thm)],[3734]) ).
thf(3817,plain,
! [C: a,B: a > $o,A: a > $o] :
( ~ ( sk4 @ A )
| ~ $true
| ( sk5
@ ^ [D: a] : $true
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ~ ( sk4
@ ^ [D: a] : $true )
| ( ( sk5 @ A
@ ^ [D: a] : $false )
!= ( sk5
@ ^ [D: a] : $true
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[104,3735]) ).
thf(3818,plain,
! [C: a,B: a > $o,A: a > $o] :
( ~ ( sk4 @ A )
| ( sk5
@ ^ [D: a] : $true
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ~ ( sk4
@ ^ [D: a] : $true )
| ( ( sk5 @ A
@ ^ [D: a] : $false )
!= ( sk5
@ ^ [D: a] : $true
@ B ) ) ),
inference(simp,[status(thm)],[3817]) ).
thf(3819,plain,
! [A: a] :
( ~ ( sk4
@ ^ [B: a] : $true )
| ( sk5
@ ^ [B: a] : $true
@ ^ [B: a] :
( $false
| ( A = B ) ) )
| ~ ( sk4
@ ^ [B: a] : $true ) ),
inference(pattern_uni,[status(thm)],[3818:[bind(A,$thf( ^ [D: a] : $true )),bind(B,$thf( ^ [D: a] : $false ))]]) ).
thf(3937,plain,
! [A: a] :
( ~ ( sk4
@ ^ [B: a] : $true )
| ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) ) ),
inference(simp,[status(thm)],[3819]) ).
thf(4796,plain,
! [A: a] :
( ~ $true
| ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk4 @ sk3 )
!= ( sk4
@ ^ [B: a] : $true ) ) ),
inference(paramod_ordered,[status(thm)],[3959,3937]) ).
thf(4797,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk4 @ sk3 )
!= ( sk4
@ ^ [B: a] : $true ) ) ),
inference(simp,[status(thm)],[4796]) ).
thf(4876,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( sk3
!= ( ^ [B: a] : $true ) ) ),
inference(simp,[status(thm)],[4797]) ).
thf(5274,plain,
! [B: a > $o,A: a] :
( ( sk3
!= ( ^ [C: a] : $true ) )
| ~ $true
| ( sk5 @ sk3
@ ^ [C: a] :
( ( B @ C )
| ( t = C ) ) )
| ( ( sk5
@ ^ [C: a] : $true
@ ( (=) @ a @ A ) )
!= ( sk5 @ sk3 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[4876,5181]) ).
thf(5275,plain,
! [B: a > $o,A: a] :
( ( sk3
!= ( ^ [C: a] : $true ) )
| ( sk5 @ sk3
@ ^ [C: a] :
( ( B @ C )
| ( t = C ) ) )
| ( ( sk5
@ ^ [C: a] : $true
@ ( (=) @ a @ A ) )
!= ( sk5 @ sk3 @ B ) ) ),
inference(simp,[status(thm)],[5274]) ).
thf(5325,plain,
! [B: a > $o,A: a] :
( ( sk5 @ sk3
@ ^ [C: a] :
( ( B @ C )
| ( t = C ) ) )
| ( sk3
!= ( ^ [C: a] : $true ) )
| ( sk3
!= ( ^ [C: a] : $true ) )
| ( ( (=) @ a @ A )
!= B ) ),
inference(simp,[status(thm)],[5275]) ).
thf(5364,plain,
! [A: a] :
( ( sk5 @ sk3
@ ^ [B: a] :
( ( A = B )
| ( t = B ) ) )
| ( sk3
!= ( ^ [B: a] : $true ) ) ),
inference(simp,[status(thm)],[5325]) ).
thf(23,plain,
! [D: a > $o,C: a,B: a > $o,A: a > $o] :
( sk1
| ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ~ ( sk4 @ A )
| sk1
| ~ $true
| ~ ( sk4 @ D )
| ( ( sk5 @ A
@ ^ [E: a] :
( ( B @ E )
| ( C = E ) ) )
!= ( sk5 @ D @ D ) ) ),
inference(paramod_ordered,[status(thm)],[16,13]) ).
thf(24,plain,
! [D: a > $o,C: a,B: a > $o,A: a > $o] :
( sk1
| ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ~ ( sk4 @ A )
| ~ ( sk4 @ D )
| ( ( sk5 @ A
@ ^ [E: a] :
( ( B @ E )
| ( C = E ) ) )
!= ( sk5 @ D @ D ) ) ),
inference(simp,[status(thm)],[23]) ).
thf(25,plain,
! [B: a > $o,A: a] :
( sk1
| ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( ( B @ A )
| ( A = A ) )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) ),
inference(pattern_uni,[status(thm)],[24:[bind(A,$thf( ^ [F: a] : ( ( E @ F ) | ( C = F ) ) )),bind(B,$thf( E )),bind(C,$thf( C )),bind(D,$thf( ^ [F: a] : ( ( E @ F ) | ( C = F ) ) ))]]) ).
thf(70,plain,
! [B: a > $o,A: a] :
( ( sk1
| ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( B @ A )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) )
& ( sk1
| ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ( A != A )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) ) ),
inference(cnf,[status(esa)],[25]) ).
thf(71,plain,
! [B: a > $o,A: a] :
( sk1
| ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( B @ A )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) ),
inference(cnfConj,[status(thm)],[70]) ).
thf(73,plain,
! [B: a > $o,A: a] :
( sk1
| ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( B @ A )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) ),
inference(simp,[status(thm)],[71]) ).
thf(109,plain,
! [B: a > $o,A: a] :
( $false
| ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( B @ A )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) ),
inference(rewrite,[status(thm)],[73,90]) ).
thf(110,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( B @ A )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) ),
inference(simp,[status(thm)],[109]) ).
thf(125,plain,
! [A: a] :
( ~ ( sk5
@ ^ [B: a] :
( $true
| ( A = B ) )
@ ^ [B: a] : $true )
| ~ $true
| ~ ( sk4
@ ^ [B: a] :
( $true
| ( A = B ) ) ) ),
inference(prim_subst,[status(thm)],[110:[bind(A,$thf( A )),bind(B,$thf( ^ [C: a] : $true ))]]) ).
thf(141,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ~ ( sk4
@ ^ [A: a] : $true ) ),
inference(simp,[status(thm)],[125]) ).
thf(4015,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ~ $true
| ( ( sk4 @ sk3 )
!= ( sk4
@ ^ [A: a] : $true ) ) ),
inference(paramod_ordered,[status(thm)],[3959,141]) ).
thf(4016,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk4 @ sk3 )
!= ( sk4
@ ^ [A: a] : $true ) ) ),
inference(simp,[status(thm)],[4015]) ).
thf(4050,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( sk3
!= ( ^ [A: a] : $true ) ) ),
inference(simp,[status(thm)],[4016]) ).
thf(10586,plain,
! [A: a] :
( ( sk3
!= ( ^ [B: a] : $true ) )
| ~ $true
| ( sk3
!= ( ^ [B: a] : $true ) )
| ( ( sk5 @ sk3
@ ^ [B: a] :
( ( A = B )
| ( t = B ) ) )
!= ( sk5
@ ^ [B: a] : $true
@ ^ [B: a] : $true ) ) ),
inference(paramod_ordered,[status(thm)],[5364,4050]) ).
thf(10587,plain,
! [A: a] :
( ( sk3
!= ( ^ [B: a] : $true ) )
| ( ( sk5 @ sk3
@ ^ [B: a] :
( ( A = B )
| ( t = B ) ) )
!= ( sk5
@ ^ [B: a] : $true
@ ^ [B: a] : $true ) ) ),
inference(simp,[status(thm)],[10586]) ).
thf(10689,plain,
! [A: a] :
( ( sk3
!= ( ^ [B: a] : $true ) )
| ( sk3
!= ( ^ [B: a] : $true ) )
| ( ( ^ [B: a] :
( ( A = B )
| ( t = B ) ) )
!= ( ^ [B: a] : $true ) ) ),
inference(simp,[status(thm)],[10587]) ).
thf(10715,plain,
! [A: a] :
( ( sk3
!= ( ^ [B: a] : $true ) )
| ( ( ^ [B: a] :
( ( A = B )
| ( t = B ) ) )
!= ( ^ [B: a] : $true ) ) ),
inference(simp,[status(thm)],[10689]) ).
thf(10763,plain,
! [A: a] :
( ~ ( sk3 @ ( sk43 @ A ) )
| ~ ( ( A
= ( sk44 @ A ) )
| ( t
= ( sk44 @ A ) ) ) ),
inference(func_ext,[status(esa)],[10715]) ).
thf(10764,plain,
! [A: a] :
( ( ~ ( sk3 @ ( sk43 @ A ) )
| ( A
!= ( sk44 @ A ) ) )
& ( ~ ( sk3 @ ( sk43 @ A ) )
| ( t
!= ( sk44 @ A ) ) ) ),
inference(cnf,[status(esa)],[10763]) ).
thf(10766,plain,
! [A: a] :
( ~ ( sk3 @ ( sk43 @ A ) )
| ( t
!= ( sk44 @ A ) ) ),
inference(cnfConj,[status(thm)],[10764]) ).
thf(10768,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ~ ( sk3 @ ( sk43 @ A ) ) ),
inference(lifteq,[status(thm)],[10766]) ).
thf(14555,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ~ $true
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ ( sk21 @ sk33 ) ) ) ),
inference(paramod_ordered,[status(thm)],[14507,10768]) ).
thf(14556,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ ( sk21 @ sk33 ) ) ) ),
inference(simp,[status(thm)],[14555]) ).
thf(14567,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk43 @ A )
!= ( sk21 @ sk33 ) ) ),
inference(simp,[status(thm)],[14556]) ).
thf(508,plain,
! [A: a] :
( ( sk4
@ ^ [B: a] : $true )
| ( sk6
@ ^ [B: a] : $true )
| ~ $true
| ( sk8
@ ^ [B: a] : $true
@ A ) ),
inference(prim_subst,[status(thm)],[447:[bind(A,$thf( ^ [C: a] : $true ))]]) ).
thf(571,plain,
! [A: a] :
( ( sk4
@ ^ [B: a] : $true )
| ( sk6
@ ^ [B: a] : $true )
| ( sk8
@ ^ [B: a] : $true
@ A ) ),
inference(simp,[status(thm)],[508]) ).
thf(3122,plain,
! [B: a > $o,A: a] :
( ( sk4
@ ^ [C: a] : $true )
| ( sk6
@ ^ [C: a] : $true )
| ( sk4 @ B )
| ( sk6 @ B )
| ~ ( cA @ ( sk8 @ B ) )
| ~ $true
| ( ( sk8
@ ^ [C: a] : $true
@ A )
!= ( sk8 @ B @ t ) ) ),
inference(paramod_ordered,[status(thm)],[571,347]) ).
thf(3123,plain,
! [B: a > $o,A: a] :
( ( sk4
@ ^ [C: a] : $true )
| ( sk6
@ ^ [C: a] : $true )
| ( sk4 @ B )
| ( sk6 @ B )
| ~ ( cA @ ( sk8 @ B ) )
| ( ( sk8
@ ^ [C: a] : $true
@ A )
!= ( sk8 @ B @ t ) ) ),
inference(simp,[status(thm)],[3122]) ).
thf(3124,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( sk6
@ ^ [A: a] : $true )
| ( sk4
@ ^ [A: a] : $true )
| ( sk6
@ ^ [A: a] : $true )
| ~ ( cA
@ ( sk8
@ ^ [A: a] : $true ) ) ),
inference(pattern_uni,[status(thm)],[3123:[bind(A,$thf( t )),bind(B,$thf( ^ [C: a] : $true ))]]) ).
thf(3149,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( sk6
@ ^ [A: a] : $true )
| ~ ( cA
@ ( sk8
@ ^ [A: a] : $true ) ) ),
inference(simp,[status(thm)],[3124]) ).
thf(15707,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ( sk4
@ ^ [B: a] : $true )
| ( sk6
@ ^ [B: a] : $true )
| ~ $true
| ( ( cA @ ( sk8 @ A ) )
!= ( cA
@ ( sk8
@ ^ [B: a] : $true ) ) ) ),
inference(paramod_ordered,[status(thm)],[98,3149]) ).
thf(15708,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ( sk4
@ ^ [B: a] : $true )
| ( sk6
@ ^ [B: a] : $true )
| ( ( cA @ ( sk8 @ A ) )
!= ( cA
@ ( sk8
@ ^ [B: a] : $true ) ) ) ),
inference(simp,[status(thm)],[15707]) ).
thf(15709,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( sk6
@ ^ [A: a] : $true )
| ( sk4
@ ^ [A: a] : $true )
| ( sk6
@ ^ [A: a] : $true ) ),
inference(pattern_uni,[status(thm)],[15708:[bind(A,$thf( ^ [B: a] : $true ))]]) ).
thf(15796,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( sk6
@ ^ [A: a] : $true ) ),
inference(simp,[status(thm)],[15709]) ).
thf(166,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ~ $true
| ~ ( sk6 @ A )
| ( ( sk3 @ ( sk7 @ A ) )
!= ( sk3 @ t ) ) ),
inference(paramod_ordered,[status(thm)],[94,162]) ).
thf(167,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ~ ( sk6 @ A )
| ( ( sk3 @ ( sk7 @ A ) )
!= ( sk3 @ t ) ) ),
inference(simp,[status(thm)],[166]) ).
thf(168,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ~ ( sk6 @ A )
| ( ( sk7 @ A )
!= t ) ),
inference(simp,[status(thm)],[167]) ).
thf(15830,plain,
! [A: a > $o] :
( ( sk4
@ ^ [B: a] : $true )
| ( sk4 @ A )
| ~ $true
| ( ( sk7 @ A )
!= t )
| ( ( sk6
@ ^ [B: a] : $true )
!= ( sk6 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[15796,168]) ).
thf(15831,plain,
! [A: a > $o] :
( ( sk4
@ ^ [B: a] : $true )
| ( sk4 @ A )
| ( ( sk7 @ A )
!= t )
| ( ( sk6
@ ^ [B: a] : $true )
!= ( sk6 @ A ) ) ),
inference(simp,[status(thm)],[15830]) ).
thf(15832,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( sk4
@ ^ [A: a] : $true )
| ( ( sk7
@ ^ [A: a] : $true )
!= t ) ),
inference(pattern_uni,[status(thm)],[15831:[bind(A,$thf( ^ [B: a] : $true ))]]) ).
thf(15874,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk7
@ ^ [A: a] : $true )
!= t ) ),
inference(simp,[status(thm)],[15832]) ).
thf(15816,plain,
! [A: a > $o] :
( ( sk4
@ ^ [B: a] : $true )
| ( sk4 @ A )
| ~ ( sk3 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk6
@ ^ [B: a] : $true )
!= ( sk6 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[15796,162]) ).
thf(15817,plain,
! [A: a > $o] :
( ( sk4
@ ^ [B: a] : $true )
| ( sk4 @ A )
| ~ ( sk3 @ ( sk7 @ A ) )
| ( ( sk6
@ ^ [B: a] : $true )
!= ( sk6 @ A ) ) ),
inference(simp,[status(thm)],[15816]) ).
thf(15818,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( sk4
@ ^ [A: a] : $true )
| ~ ( sk3
@ ( sk7
@ ^ [A: a] : $true ) ) ),
inference(pattern_uni,[status(thm)],[15817:[bind(A,$thf( ^ [B: a] : $true ))]]) ).
thf(15865,plain,
( ( sk4
@ ^ [A: a] : $true )
| ~ ( sk3
@ ( sk7
@ ^ [A: a] : $true ) ) ),
inference(simp,[status(thm)],[15818]) ).
thf(16011,plain,
( ~ ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ~ $true
| ( ( sk4
@ ^ [A: a] : $true )
!= ( sk4
@ ^ [A: a] : $true ) ) ),
inference(paramod_ordered,[status(thm)],[15865,141]) ).
thf(16012,plain,
( ~ ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk4
@ ^ [A: a] : $true )
!= ( sk4
@ ^ [A: a] : $true ) ) ),
inference(simp,[status(thm)],[16011]) ).
thf(16013,plain,
( ~ ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true ) ),
inference(pattern_uni,[status(thm)],[16012:[]]) ).
thf(163,plain,
! [B: a > $o,A: a > $o] :
( ( sk4 @ A )
| ( cA @ ( sk8 @ A ) )
| ( sk4 @ B )
| ~ ( sk3 @ ( sk7 @ B ) )
| ~ $true
| ( ( sk6 @ A )
!= ( sk6 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[98,162]) ).
thf(164,plain,
! [B: a > $o,A: a > $o] :
( ( sk4 @ A )
| ( cA @ ( sk8 @ A ) )
| ( sk4 @ B )
| ~ ( sk3 @ ( sk7 @ B ) )
| ( ( sk6 @ A )
!= ( sk6 @ B ) ) ),
inference(simp,[status(thm)],[163]) ).
thf(165,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( cA @ ( sk8 @ A ) )
| ( sk4 @ A )
| ~ ( sk3 @ ( sk7 @ A ) ) ),
inference(pattern_uni,[status(thm)],[164:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(169,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( cA @ ( sk8 @ A ) )
| ~ ( sk3 @ ( sk7 @ A ) ) ),
inference(simp,[status(thm)],[165]) ).
thf(14728,plain,
! [B: a,A: a > $o] :
( ( cA @ ( sk8 @ A ) )
| ~ ( sk3 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk4 @ A )
!= ( sk4 @ ( (=) @ a @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[169,1080]) ).
thf(14729,plain,
! [B: a,A: a > $o] :
( ( cA @ ( sk8 @ A ) )
| ~ ( sk3 @ ( sk7 @ A ) )
| ( ( sk4 @ A )
!= ( sk4 @ ( (=) @ a @ B ) ) ) ),
inference(simp,[status(thm)],[14728]) ).
thf(14730,plain,
! [A: a] :
( ( cA @ ( sk8 @ ( (=) @ a @ A ) ) )
| ~ ( sk3 @ ( sk7 @ ( (=) @ a @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[14729:[bind(A,$thf( (=) @ a @ B )),bind(B,$thf( B ))]]) ).
thf(14912,plain,
! [A: a] :
( ( cA @ ( sk8 @ ( (=) @ a @ A ) ) )
| ~ ( sk3 @ ( sk7 @ ( (=) @ a @ A ) ) ) ),
inference(simp,[status(thm)],[14730]) ).
thf(210,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ~ ( sk6 @ A )
| ~ $true
| ( ( A @ ( sk7 @ A ) )
!= sk1 ) ),
inference(paramod_ordered,[status(thm)],[175,90]) ).
thf(211,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ~ ( sk6 @ A )
| ( ( A @ ( sk7 @ A ) )
!= sk1 ) ),
inference(simp,[status(thm)],[210]) ).
thf(240,plain,
( ( sk4
@ ^ [A: a] : sk1 )
| ~ ( sk6
@ ^ [A: a] : sk1 ) ),
inference(pre_uni,[status(thm)],[211:[bind(A,$thf( ^ [B: a] : sk1 ))]]) ).
thf(266,plain,
( ( sk4
@ ^ [A: a] : $false )
| ~ ( sk6
@ ^ [A: a] : $false ) ),
inference(rewrite,[status(thm)],[240,90]) ).
thf(267,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( cA @ ( sk8 @ A ) )
| ( sk4
@ ^ [B: a] : $false )
| ~ $true
| ( ( sk6 @ A )
!= ( sk6
@ ^ [B: a] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[98,266]) ).
thf(268,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( cA @ ( sk8 @ A ) )
| ( sk4
@ ^ [B: a] : $false )
| ( ( sk6 @ A )
!= ( sk6
@ ^ [B: a] : $false ) ) ),
inference(simp,[status(thm)],[267]) ).
thf(269,plain,
( ( sk4
@ ^ [A: a] : $false )
| ( cA
@ ( sk8
@ ^ [A: a] : $false ) )
| ( sk4
@ ^ [A: a] : $false ) ),
inference(pattern_uni,[status(thm)],[268:[bind(A,$thf( ^ [B: a] : $false ))]]) ).
thf(276,plain,
( ( sk4
@ ^ [A: a] : $false )
| ( cA
@ ( sk8
@ ^ [A: a] : $false ) ) ),
inference(simp,[status(thm)],[269]) ).
thf(105,plain,
! [B: a > $o,A: a > $o] :
( ~ ( sk4 @ A )
| ~ $true
| ~ ( sk4 @ B )
| ( ( sk5 @ A
@ ^ [C: a] : $false )
!= ( sk5 @ B @ B ) ) ),
inference(paramod_ordered,[status(thm)],[104,96]) ).
thf(106,plain,
! [B: a > $o,A: a > $o] :
( ~ ( sk4 @ A )
| ~ ( sk4 @ B )
| ( ( sk5 @ A
@ ^ [C: a] : $false )
!= ( sk5 @ B @ B ) ) ),
inference(simp,[status(thm)],[105]) ).
thf(107,plain,
( ~ ( sk4
@ ^ [A: a] : $false )
| ~ ( sk4
@ ^ [A: a] : $false ) ),
inference(pattern_uni,[status(thm)],[106:[bind(A,$thf( ^ [C: a] : $false )),bind(B,$thf( ^ [C: a] : $false ))]]) ).
thf(108,plain,
~ ( sk4
@ ^ [A: a] : $false ),
inference(simp,[status(thm)],[107]) ).
thf(294,plain,
( $false
| ( cA
@ ( sk8
@ ^ [A: a] : $false ) ) ),
inference(rewrite,[status(thm)],[276,108]) ).
thf(295,plain,
( cA
@ ( sk8
@ ^ [A: a] : $false ) ),
inference(simp,[status(thm)],[294]) ).
thf(373,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ~ $true
| ~ ( sk8 @ A @ t )
| ( ( cA
@ ( sk8
@ ^ [B: a] : $false ) )
!= ( cA @ ( sk8 @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[295,347]) ).
thf(374,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ~ ( sk8 @ A @ t )
| ( ( cA
@ ( sk8
@ ^ [B: a] : $false ) )
!= ( cA @ ( sk8 @ A ) ) ) ),
inference(simp,[status(thm)],[373]) ).
thf(375,plain,
( ( sk4
@ ^ [A: a] : $false )
| ( sk6
@ ^ [A: a] : $false )
| ~ ( sk8
@ ^ [A: a] : $false
@ t ) ),
inference(pattern_uni,[status(thm)],[374:[bind(A,$thf( ^ [B: a] : $false ))]]) ).
thf(219,plain,
( ( sk4
@ ^ [A: a] : $false )
| $false
| ~ ( sk6
@ ^ [A: a] : $false ) ),
inference(prim_subst,[status(thm)],[175:[bind(A,$thf( ^ [B: a] : $false ))]]) ).
thf(252,plain,
( ( sk4
@ ^ [A: a] : $false )
| ~ ( sk6
@ ^ [A: a] : $false ) ),
inference(simp,[status(thm)],[219]) ).
thf(277,plain,
( $false
| ~ ( sk6
@ ^ [A: a] : $false ) ),
inference(rewrite,[status(thm)],[252,108]) ).
thf(278,plain,
~ ( sk6
@ ^ [A: a] : $false ),
inference(simp,[status(thm)],[277]) ).
thf(1202,plain,
( $false
| $false
| ~ ( sk8
@ ^ [A: a] : $false
@ t ) ),
inference(rewrite,[status(thm)],[375,278,108]) ).
thf(1203,plain,
~ ( sk8
@ ^ [A: a] : $false
@ t ),
inference(simp,[status(thm)],[1202]) ).
thf(1204,plain,
( ( sk4 @ sk3 )
| ( sk6 @ sk3 )
| ~ $true
| ( ( sk8 @ sk3 @ t )
!= ( sk8
@ ^ [A: a] : $false
@ t ) ) ),
inference(paramod_ordered,[status(thm)],[520,1203]) ).
thf(1205,plain,
( ( sk4 @ sk3 )
| ( sk6 @ sk3 )
| ( ( sk8 @ sk3 @ t )
!= ( sk8
@ ^ [A: a] : $false
@ t ) ) ),
inference(simp,[status(thm)],[1204]) ).
thf(1212,plain,
( ( sk4 @ sk3 )
| ( sk6 @ sk3 )
| ( sk3
!= ( ^ [A: a] : $false ) )
| ( t != t ) ),
inference(simp,[status(thm)],[1205]) ).
thf(1215,plain,
( ( sk4 @ sk3 )
| ( sk6 @ sk3 )
| ( sk3
!= ( ^ [A: a] : $false ) ) ),
inference(simp,[status(thm)],[1212]) ).
thf(1227,plain,
( ( sk4 @ sk3 )
| ( sk3
!= ( ^ [A: a] : $false ) )
| ( sk4 @ sk3 )
| ~ $true
| ( ( sk6 @ sk3 )
!= ( sk6 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[1215,263]) ).
thf(1228,plain,
( ( sk4 @ sk3 )
| ( sk3
!= ( ^ [A: a] : $false ) )
| ( ( sk6 @ sk3 )
!= ( sk6 @ sk3 ) ) ),
inference(simp,[status(thm)],[1227]) ).
thf(1229,plain,
( ( sk4 @ sk3 )
| ( sk3
!= ( ^ [A: a] : $false ) ) ),
inference(pattern_uni,[status(thm)],[1228:[]]) ).
thf(1494,plain,
( ( sk3
!= ( ^ [A: a] : $false ) )
| ~ $true
| ( ( sk4 @ sk3 )
!= ( sk4
@ ^ [A: a] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[1229,108]) ).
thf(1495,plain,
( ( sk3
!= ( ^ [A: a] : $false ) )
| ( ( sk4 @ sk3 )
!= ( sk4
@ ^ [A: a] : $false ) ) ),
inference(simp,[status(thm)],[1494]) ).
thf(1515,plain,
( ( sk3
!= ( ^ [A: a] : $false ) )
| ( sk3
!= ( ^ [A: a] : $false ) ) ),
inference(simp,[status(thm)],[1495]) ).
thf(1521,plain,
( sk3
!= ( ^ [A: a] : $false ) ),
inference(simp,[status(thm)],[1515]) ).
thf(1524,plain,
sk3 @ sk17,
inference(func_ext,[status(esa)],[1521]) ).
thf(12436,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ~ $true
| ( ( sk3 @ ( sk21 @ A ) )
!= ( sk3 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[1524,4447]) ).
thf(12437,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ( ( sk3 @ ( sk21 @ A ) )
!= ( sk3 @ sk17 ) ) ),
inference(simp,[status(thm)],[12436]) ).
thf(12448,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ( ( sk21 @ A )
!= sk17 ) ),
inference(simp,[status(thm)],[12437]) ).
thf(12664,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ( ( sk21 @ A )
!= ( sk21 @ A ) )
| ( sk17 != A ) ),
inference(eqfactor_ordered,[status(thm)],[12448]) ).
thf(12665,plain,
( ( sk21 @ sk17 )
!= sk17 ),
inference(pattern_uni,[status(thm)],[12664:[bind(A,$thf( sk17 ))]]) ).
thf(12668,plain,
! [A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( A != sk17 )
| ( ( sk21 @ A )
!= ( sk21 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[4451,12665]) ).
thf(12669,plain,
( ( sk3 @ ( sk21 @ sk17 ) )
| ( sk17 != sk17 ) ),
inference(pattern_uni,[status(thm)],[12668:[bind(A,$thf( sk17 ))]]) ).
thf(12670,plain,
sk3 @ ( sk21 @ sk17 ),
inference(simp,[status(thm)],[12669]) ).
thf(12718,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ~ $true
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ ( sk21 @ sk17 ) ) ) ),
inference(paramod_ordered,[status(thm)],[12670,10768]) ).
thf(12719,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ ( sk21 @ sk17 ) ) ) ),
inference(simp,[status(thm)],[12718]) ).
thf(12738,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk43 @ A )
!= ( sk21 @ sk17 ) ) ),
inference(simp,[status(thm)],[12719]) ).
thf(4823,plain,
! [A: a] :
( ~ ( sk4
@ ^ [B: a] : $true )
| ~ $true
| ~ ( sk4
@ ^ [B: a] : $true )
| ( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
!= ( sk5
@ ^ [B: a] : $true
@ ^ [B: a] : $true ) ) ),
inference(paramod_ordered,[status(thm)],[3937,141]) ).
thf(4824,plain,
! [A: a] :
( ~ ( sk4
@ ^ [B: a] : $true )
| ( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
!= ( sk5
@ ^ [B: a] : $true
@ ^ [B: a] : $true ) ) ),
inference(simp,[status(thm)],[4823]) ).
thf(4884,plain,
! [A: a] :
( ~ ( sk4
@ ^ [B: a] : $true )
| ( ( ^ [B: a] : $true )
!= ( ^ [B: a] : $true ) )
| ( ( (=) @ a @ A )
!= ( ^ [B: a] : $true ) ) ),
inference(simp,[status(thm)],[4824]) ).
thf(4923,plain,
! [A: a] :
( ~ ( sk4
@ ^ [B: a] : $true )
| ( ( (=) @ a @ A )
!= ( ^ [B: a] : $true ) ) ),
inference(simp,[status(thm)],[4884]) ).
thf(4947,plain,
! [A: a] :
( ( A
!= ( sk26 @ A ) )
| ~ ( sk4
@ ^ [B: a] : $true ) ),
inference(func_ext,[status(esa)],[4923]) ).
thf(4956,plain,
! [A: a] :
( ( ( sk26 @ A )
!= A )
| ~ ( sk4
@ ^ [B: a] : $true ) ),
inference(lifteq,[status(thm)],[4947]) ).
thf(5159,plain,
! [A: a] :
( ( ( sk26 @ A )
!= A )
| ~ $true
| ( ( sk4 @ sk3 )
!= ( sk4
@ ^ [B: a] : $true ) ) ),
inference(paramod_ordered,[status(thm)],[3959,4956]) ).
thf(5160,plain,
! [A: a] :
( ( ( sk26 @ A )
!= A )
| ( ( sk4 @ sk3 )
!= ( sk4
@ ^ [B: a] : $true ) ) ),
inference(simp,[status(thm)],[5159]) ).
thf(5168,plain,
! [A: a] :
( ( ( sk26 @ A )
!= A )
| ( sk3
!= ( ^ [B: a] : $true ) ) ),
inference(simp,[status(thm)],[5160]) ).
thf(12660,plain,
! [B: a,A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( A != B )
| ( ( sk21 @ B )
!= sk17 )
| ( ( sk21 @ A )
!= ( sk21 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[4451,12448]) ).
thf(12661,plain,
! [A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( A != A )
| ( ( sk21 @ A )
!= sk17 ) ),
inference(pattern_uni,[status(thm)],[12660:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(12666,plain,
! [A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( ( sk21 @ A )
!= sk17 ) ),
inference(simp,[status(thm)],[12661]) ).
thf(118,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ $true
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ( ( sk3 @ t )
!= ( B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[94,110]) ).
thf(119,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ( ( sk3 @ t )
!= ( B @ A ) ) ),
inference(simp,[status(thm)],[118]) ).
thf(134,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) )
@ sk3 )
| ~ ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) ) ) ),
inference(pre_uni,[status(thm)],[119:[bind(A,$thf( t )),bind(B,$thf( sk3 ))]]) ).
thf(305,plain,
! [A: a > $o] :
( ~ ( sk4 @ A )
| ~ $true
| ~ ( sk4
@ ^ [B: a] :
( ( sk3 @ B )
| ( t = B ) ) )
| ( ( sk5 @ A
@ ^ [B: a] : $false )
!= ( sk5
@ ^ [B: a] :
( ( sk3 @ B )
| ( t = B ) )
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[104,134]) ).
thf(306,plain,
! [A: a > $o] :
( ~ ( sk4 @ A )
| ~ ( sk4
@ ^ [B: a] :
( ( sk3 @ B )
| ( t = B ) ) )
| ( ( sk5 @ A
@ ^ [B: a] : $false )
!= ( sk5
@ ^ [B: a] :
( ( sk3 @ B )
| ( t = B ) )
@ sk3 ) ) ),
inference(simp,[status(thm)],[305]) ).
thf(308,plain,
! [A: a > $o] :
( ~ ( sk4 @ A )
| ~ ( sk4
@ ^ [B: a] :
( ( sk3 @ B )
| ( t = B ) ) )
| ( A
!= ( ^ [B: a] :
( ( sk3 @ B )
| ( t = B ) ) ) )
| ( sk3
!= ( ^ [B: a] : $false ) ) ),
inference(simp,[status(thm)],[306]) ).
thf(309,plain,
( ~ ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) ) )
| ~ ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) ) )
| ( sk3
!= ( ^ [A: a] : $false ) ) ),
inference(simp,[status(thm)],[308]) ).
thf(310,plain,
( ~ ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) ) )
| ( sk3
!= ( ^ [A: a] : $false ) ) ),
inference(simp,[status(thm)],[309]) ).
thf(311,plain,
( ( sk3 @ sk9 )
| ~ ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) ) ) ),
inference(func_ext,[status(esa)],[310]) ).
thf(4019,plain,
( ( sk3 @ sk9 )
| ~ $true
| ( ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) ) )
!= ( sk4 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[3959,311]) ).
thf(4020,plain,
( ( sk3 @ sk9 )
| ( ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) ) )
!= ( sk4 @ sk3 ) ) ),
inference(simp,[status(thm)],[4019]) ).
thf(4054,plain,
( ( sk3 @ sk9 )
| ( ( ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) ) )
!= sk3 ) ),
inference(simp,[status(thm)],[4020]) ).
thf(4794,plain,
( ( ( ( sk3 @ sk25 )
| ( t = sk25 ) )
!= ( sk3 @ sk25 ) )
| ( sk3 @ sk9 ) ),
inference(func_ext,[status(esa)],[4054]) ).
thf(7388,plain,
( ( sk3 @ sk9 )
| ( sk3 @ sk25 )
| ( t = sk25 )
| ( sk3 @ sk25 ) ),
inference(bool_ext,[status(thm)],[4794]) ).
thf(7428,plain,
( ( sk3 @ sk9 )
| ( sk3 @ sk25 )
| ( t = sk25 )
| ( sk3 @ sk25 ) ),
inference(cnf,[status(esa)],[7388]) ).
thf(7429,plain,
( ( sk25 = t )
| ( sk3 @ sk9 )
| ( sk3 @ sk25 )
| ( sk3 @ sk25 ) ),
inference(lifteq,[status(thm)],[7428]) ).
thf(7430,plain,
( ( sk25 = t )
| ( sk3 @ sk9 )
| ( sk3 @ sk25 ) ),
inference(simp,[status(thm)],[7429]) ).
thf(7387,plain,
( ( sk3 @ sk9 )
| ~ ( ( sk3 @ sk25 )
| ( t = sk25 ) )
| ~ ( sk3 @ sk25 ) ),
inference(bool_ext,[status(thm)],[4794]) ).
thf(7423,plain,
( ( ( sk3 @ sk9 )
| ~ ( sk3 @ sk25 )
| ~ ( sk3 @ sk25 ) )
& ( ( sk3 @ sk9 )
| ( t != sk25 )
| ~ ( sk3 @ sk25 ) ) ),
inference(cnf,[status(esa)],[7387]) ).
thf(7424,plain,
( ( sk3 @ sk9 )
| ~ ( sk3 @ sk25 )
| ~ ( sk3 @ sk25 ) ),
inference(cnfConj,[status(thm)],[7423]) ).
thf(7426,plain,
( ( sk3 @ sk9 )
| ~ ( sk3 @ sk25 ) ),
inference(simp,[status(thm)],[7424]) ).
thf(7557,plain,
( ( sk25 = t )
| ( sk3 @ sk9 )
| ( sk3 @ sk9 )
| ~ $true
| ( ( sk3 @ sk25 )
!= ( sk3 @ sk25 ) ) ),
inference(paramod_ordered,[status(thm)],[7430,7426]) ).
thf(7558,plain,
( ( sk25 = t )
| ( sk3 @ sk9 )
| ( ( sk3 @ sk25 )
!= ( sk3 @ sk25 ) ) ),
inference(simp,[status(thm)],[7557]) ).
thf(7559,plain,
( ( sk25 = t )
| ( sk3 @ sk9 ) ),
inference(pattern_uni,[status(thm)],[7558:[]]) ).
thf(7441,plain,
( ( sk3 @ sk9 )
| ~ $true
| ( ( sk3 @ sk25 )
!= ( sk3 @ t ) ) ),
inference(paramod_ordered,[status(thm)],[94,7426]) ).
thf(7442,plain,
( ( sk3 @ sk9 )
| ( ( sk3 @ sk25 )
!= ( sk3 @ t ) ) ),
inference(simp,[status(thm)],[7441]) ).
thf(7449,plain,
( ( sk3 @ sk9 )
| ( sk25 != t ) ),
inference(simp,[status(thm)],[7442]) ).
thf(8290,plain,
( ( sk3 @ sk9 )
| ( sk3 @ sk9 )
| ( t != t )
| ( sk25 != sk25 ) ),
inference(paramod_ordered,[status(thm)],[7559,7449]) ).
thf(8291,plain,
( ( sk3 @ sk9 )
| ( sk25 != sk25 ) ),
inference(simp,[status(thm)],[8290]) ).
thf(8292,plain,
sk3 @ sk9,
inference(pattern_uni,[status(thm)],[8291:[]]) ).
thf(16073,plain,
( ( sk4
@ ^ [A: a] : $true )
| ~ $true
| ( ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
!= ( sk3 @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[8292,15865]) ).
thf(16074,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
!= ( sk3 @ sk9 ) ) ),
inference(simp,[status(thm)],[16073]) ).
thf(16184,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk7
@ ^ [A: a] : $true )
!= sk9 ) ),
inference(simp,[status(thm)],[16074]) ).
thf(16007,plain,
( ( sk4
@ ^ [A: a] : $true )
| ~ $true
| ( ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
!= ( sk3 @ sk33 ) ) ),
inference(paramod_ordered,[status(thm)],[5611,15865]) ).
thf(16008,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
!= ( sk3 @ sk33 ) ) ),
inference(simp,[status(thm)],[16007]) ).
thf(16156,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk7
@ ^ [A: a] : $true )
!= sk33 ) ),
inference(simp,[status(thm)],[16008]) ).
thf(12440,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ~ $true
| ( ( sk3 @ ( sk21 @ A ) )
!= ( sk3 @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[8292,4447]) ).
thf(12441,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ( ( sk3 @ ( sk21 @ A ) )
!= ( sk3 @ sk9 ) ) ),
inference(simp,[status(thm)],[12440]) ).
thf(12449,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ( ( sk21 @ A )
!= sk9 ) ),
inference(simp,[status(thm)],[12441]) ).
thf(13264,plain,
! [B: a,A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( A != B )
| ( ( sk21 @ B )
!= sk9 )
| ( ( sk21 @ A )
!= ( sk21 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[4451,12449]) ).
thf(13265,plain,
! [A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( A != A )
| ( ( sk21 @ A )
!= sk9 ) ),
inference(pattern_uni,[status(thm)],[13264:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(13270,plain,
! [A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( ( sk21 @ A )
!= sk9 ) ),
inference(simp,[status(thm)],[13265]) ).
thf(5393,plain,
( ~ $true
| ( sk3
!= ( ^ [A: a] : $true ) )
| ( ( sk5 @ sk3 @ ( (=) @ a @ t ) )
!= ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true ) ) ),
inference(paramod_ordered,[status(thm)],[5356,4050]) ).
thf(5394,plain,
( ( sk3
!= ( ^ [A: a] : $true ) )
| ( ( sk5 @ sk3 @ ( (=) @ a @ t ) )
!= ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true ) ) ),
inference(simp,[status(thm)],[5393]) ).
thf(5479,plain,
( ( sk3
!= ( ^ [A: a] : $true ) )
| ( sk3
!= ( ^ [A: a] : $true ) )
| ( ( (=) @ a @ t )
!= ( ^ [A: a] : $true ) ) ),
inference(simp,[status(thm)],[5394]) ).
thf(5510,plain,
( ( sk3
!= ( ^ [A: a] : $true ) )
| ( ( (=) @ a @ t )
!= ( ^ [A: a] : $true ) ) ),
inference(simp,[status(thm)],[5479]) ).
thf(6220,plain,
( ~ ( sk3 @ sk35 )
| ( t != sk36 ) ),
inference(func_ext,[status(esa)],[5510]) ).
thf(6221,plain,
( ( sk36 != t )
| ~ ( sk3 @ sk35 ) ),
inference(lifteq,[status(thm)],[6220]) ).
thf(6226,plain,
( ( sk36 != t )
| ~ $true
| ( ( sk3 @ sk35 )
!= ( sk3 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[1524,6221]) ).
thf(6227,plain,
( ( sk36 != t )
| ( ( sk3 @ sk35 )
!= ( sk3 @ sk17 ) ) ),
inference(simp,[status(thm)],[6226]) ).
thf(6236,plain,
( ( sk36 != t )
| ( sk35 != sk17 ) ),
inference(simp,[status(thm)],[6227]) ).
thf(8392,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ $true
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ( ( sk3 @ sk9 )
!= ( B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[8292,110]) ).
thf(8393,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ( ( sk3 @ sk9 )
!= ( B @ A ) ) ),
inference(simp,[status(thm)],[8392]) ).
thf(8451,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk9 = A ) )
@ sk3 )
| ~ ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk9 = A ) ) ) ),
inference(pre_uni,[status(thm)],[8393:[bind(A,$thf( sk9 )),bind(B,$thf( sk3 ))]]) ).
thf(9003,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk9 = A ) )
@ sk3 )
| ~ $true
| ( ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk9 = A ) ) )
!= ( sk4 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[3959,8451]) ).
thf(9004,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk9 = A ) )
@ sk3 )
| ( ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk9 = A ) ) )
!= ( sk4 @ sk3 ) ) ),
inference(simp,[status(thm)],[9003]) ).
thf(9064,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk9 = A ) )
@ sk3 )
| ( ( ^ [A: a] :
( ( sk3 @ A )
| ( sk9 = A ) ) )
!= sk3 ) ),
inference(simp,[status(thm)],[9004]) ).
thf(7386,plain,
! [A: a] :
( ~ ( sk3 @ ( sk37 @ A ) )
| ( ( sk26 @ A )
!= A ) ),
inference(func_ext,[status(esa)],[5168]) ).
thf(1062,plain,
! [E: a > $o,D: a,C: a,B: a > $o,A: a > $o] :
( ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ( ( sk4 @ A )
!= ( A @ C ) )
| ~ $true
| ~ ( sk4
@ ^ [F: a] :
( ( E @ F )
| ( D = F ) ) )
| ( ( sk5 @ A
@ ^ [F: a] :
( ( B @ F )
| ( C = F ) ) )
!= ( sk5
@ ^ [F: a] :
( ( E @ F )
| ( D = F ) )
@ E ) ) ),
inference(paramod_ordered,[status(thm)],[786,1033]) ).
thf(1063,plain,
! [E: a > $o,D: a,C: a,B: a > $o,A: a > $o] :
( ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ( ( sk4 @ A )
!= ( A @ C ) )
| ~ ( sk4
@ ^ [F: a] :
( ( E @ F )
| ( D = F ) ) )
| ( ( sk5 @ A
@ ^ [F: a] :
( ( B @ F )
| ( C = F ) ) )
!= ( sk5
@ ^ [F: a] :
( ( E @ F )
| ( D = F ) )
@ E ) ) ),
inference(simp,[status(thm)],[1062]) ).
thf(1064,plain,
! [C: a > $o,B: a,A: a] :
( ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ~ ( ( C @ A )
| ( A = A )
| ( B = A ) )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) ),
inference(pattern_uni,[status(thm)],[1063:[bind(A,$thf( ^ [G: a] : ( ( J @ G ) | ( C = G ) | ( D = G ) ) )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( ^ [G: a] : ( ( J @ G ) | ( C = G ) ) ))]]) ).
thf(1081,plain,
! [C: a > $o,B: a,A: a] :
( ( ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ~ ( C @ A )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) )
& ( ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ( A != A )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) )
& ( ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ( B != A )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) ) ),
inference(cnf,[status(esa)],[1064]) ).
thf(1083,plain,
! [C: a > $o,B: a,A: a] :
( ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ( A != A )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) ),
inference(cnfConj,[status(thm)],[1081]) ).
thf(1086,plain,
! [C: a > $o,B: a,A: a] :
( ( A != A )
| ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) ),
inference(lifteq,[status(thm)],[1083]) ).
thf(1087,plain,
! [C: a > $o,B: a,A: a] :
( ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) ),
inference(simp,[status(thm)],[1086]) ).
thf(3629,plain,
! [D: a > $o,C: a,B: a,A: a > $o] :
( ~ ( sk4 @ A )
| ~ $true
| ~ ( sk4
@ ^ [E: a] :
( ( D @ E )
| ( B = E )
| ( C = E ) ) )
| ( ( sk5 @ A
@ ^ [E: a] : $false )
!= ( sk5
@ ^ [E: a] :
( ( D @ E )
| ( B = E )
| ( C = E ) )
@ D ) ) ),
inference(paramod_ordered,[status(thm)],[104,1087]) ).
thf(3630,plain,
! [D: a > $o,C: a,B: a,A: a > $o] :
( ~ ( sk4 @ A )
| ~ ( sk4
@ ^ [E: a] :
( ( D @ E )
| ( B = E )
| ( C = E ) ) )
| ( ( sk5 @ A
@ ^ [E: a] : $false )
!= ( sk5
@ ^ [E: a] :
( ( D @ E )
| ( B = E )
| ( C = E ) )
@ D ) ) ),
inference(simp,[status(thm)],[3629]) ).
thf(3631,plain,
! [B: a,A: a] :
( ~ ( sk4
@ ^ [C: a] :
( $false
| ( A = C )
| ( B = C ) ) )
| ~ ( sk4
@ ^ [C: a] :
( $false
| ( A = C )
| ( B = C ) ) ) ),
inference(pattern_uni,[status(thm)],[3630:[bind(A,$thf( ^ [E: a] : ( $false | ( B = E ) | ( C = E ) ) )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( ^ [E: a] : $false ))]]) ).
thf(3670,plain,
! [B: a,A: a] :
~ ( sk4
@ ^ [C: a] :
( ( A = C )
| ( B = C ) ) ),
inference(simp,[status(thm)],[3631]) ).
thf(3989,plain,
! [B: a,A: a] :
( ~ $true
| ( ( sk4
@ ^ [C: a] :
( ( A = C )
| ( B = C ) ) )
!= ( sk4 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[3959,3670]) ).
thf(3990,plain,
! [B: a,A: a] :
( ( sk4
@ ^ [C: a] :
( ( A = C )
| ( B = C ) ) )
!= ( sk4 @ sk3 ) ),
inference(simp,[status(thm)],[3989]) ).
thf(4060,plain,
! [B: a,A: a] :
( ( ^ [C: a] :
( ( A = C )
| ( B = C ) ) )
!= sk3 ),
inference(simp,[status(thm)],[3990]) ).
thf(4439,plain,
! [B: a,A: a] :
( ( ( A
= ( sk22 @ B @ A ) )
| ( B
= ( sk22 @ B @ A ) ) )
!= ( sk3 @ ( sk22 @ B @ A ) ) ),
inference(func_ext,[status(esa)],[4060]) ).
thf(5616,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ $true
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ( ( sk3 @ sk33 )
!= ( B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[5611,110]) ).
thf(5617,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ( ( sk3 @ sk33 )
!= ( B @ A ) ) ),
inference(simp,[status(thm)],[5616]) ).
thf(5640,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk33 = A ) )
@ sk3 )
| ~ ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk33 = A ) ) ) ),
inference(pre_uni,[status(thm)],[5617:[bind(A,$thf( sk33 )),bind(B,$thf( sk3 ))]]) ).
thf(6232,plain,
( ( sk36 != t )
| ~ $true
| ( ( sk3 @ sk35 )
!= ( sk3 @ t ) ) ),
inference(paramod_ordered,[status(thm)],[94,6221]) ).
thf(6233,plain,
( ( sk36 != t )
| ( ( sk3 @ sk35 )
!= ( sk3 @ t ) ) ),
inference(simp,[status(thm)],[6232]) ).
thf(6240,plain,
( ( sk36 != t )
| ( sk35 != t ) ),
inference(simp,[status(thm)],[6233]) ).
thf(4506,plain,
( ~ ( sk3 @ sk23 )
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true ) ),
inference(func_ext,[status(esa)],[4050]) ).
thf(4597,plain,
( ~ $true
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ sk23 )
!= ( sk3 @ t ) ) ),
inference(paramod_ordered,[status(thm)],[94,4506]) ).
thf(4598,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ sk23 )
!= ( sk3 @ t ) ) ),
inference(simp,[status(thm)],[4597]) ).
thf(4622,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( sk23 != t ) ),
inference(simp,[status(thm)],[4598]) ).
thf(13268,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ( ( sk21 @ A )
!= ( sk21 @ A ) )
| ( sk9 != A ) ),
inference(eqfactor_ordered,[status(thm)],[12449]) ).
thf(13269,plain,
( ( sk21 @ sk9 )
!= sk9 ),
inference(pattern_uni,[status(thm)],[13268:[bind(A,$thf( sk9 ))]]) ).
thf(13272,plain,
! [A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( A != sk9 )
| ( ( sk21 @ A )
!= ( sk21 @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[4451,13269]) ).
thf(13273,plain,
( ( sk3 @ ( sk21 @ sk9 ) )
| ( sk9 != sk9 ) ),
inference(pattern_uni,[status(thm)],[13272:[bind(A,$thf( sk9 ))]]) ).
thf(13274,plain,
sk3 @ ( sk21 @ sk9 ),
inference(simp,[status(thm)],[13273]) ).
thf(13318,plain,
( ~ $true
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ ( sk21 @ sk9 ) )
!= ( sk3 @ sk23 ) ) ),
inference(paramod_ordered,[status(thm)],[13274,4506]) ).
thf(13319,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ ( sk21 @ sk9 ) )
!= ( sk3 @ sk23 ) ) ),
inference(simp,[status(thm)],[13318]) ).
thf(13365,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk21 @ sk9 )
!= sk23 ) ),
inference(simp,[status(thm)],[13319]) ).
thf(4948,plain,
! [A: a] :
( ~ $true
| ( ( (=) @ a @ A )
!= ( ^ [B: a] : $true ) )
| ( ( sk4 @ sk3 )
!= ( sk4
@ ^ [B: a] : $true ) ) ),
inference(paramod_ordered,[status(thm)],[3959,4923]) ).
thf(4949,plain,
! [A: a] :
( ( ( (=) @ a @ A )
!= ( ^ [B: a] : $true ) )
| ( ( sk4 @ sk3 )
!= ( sk4
@ ^ [B: a] : $true ) ) ),
inference(simp,[status(thm)],[4948]) ).
thf(4961,plain,
! [A: a] :
( ( ( (=) @ a @ A )
!= ( ^ [B: a] : $true ) )
| ( sk3
!= ( ^ [B: a] : $true ) ) ),
inference(simp,[status(thm)],[4949]) ).
thf(4966,plain,
! [A: a] :
( ( A
!= ( sk27 @ A ) )
| ~ ( sk3 @ ( sk28 @ A ) ) ),
inference(func_ext,[status(esa)],[4961]) ).
thf(4967,plain,
! [A: a] :
( ( ( sk27 @ A )
!= A )
| ~ ( sk3 @ ( sk28 @ A ) ) ),
inference(lifteq,[status(thm)],[4966]) ).
thf(16318,plain,
( ~ $true
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
!= ( sk3 @ t ) ) ),
inference(paramod_ordered,[status(thm)],[94,16013]) ).
thf(16319,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
!= ( sk3 @ t ) ) ),
inference(simp,[status(thm)],[16318]) ).
thf(16344,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk7
@ ^ [A: a] : $true )
!= t ) ),
inference(simp,[status(thm)],[16319]) ).
thf(12714,plain,
( ~ $true
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ ( sk21 @ sk17 ) )
!= ( sk3 @ sk23 ) ) ),
inference(paramod_ordered,[status(thm)],[12670,4506]) ).
thf(12715,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ ( sk21 @ sk17 ) )
!= ( sk3 @ sk23 ) ) ),
inference(simp,[status(thm)],[12714]) ).
thf(12750,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk21 @ sk17 )
!= sk23 ) ),
inference(simp,[status(thm)],[12715]) ).
thf(11154,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ~ $true
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ t ) ) ),
inference(paramod_ordered,[status(thm)],[94,10768]) ).
thf(11155,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ t ) ) ),
inference(simp,[status(thm)],[11154]) ).
thf(11163,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk43 @ A )
!= t ) ),
inference(simp,[status(thm)],[11155]) ).
thf(13284,plain,
( ( sk36 != t )
| ~ $true
| ( ( sk3 @ ( sk21 @ sk9 ) )
!= ( sk3 @ sk35 ) ) ),
inference(paramod_ordered,[status(thm)],[13274,6221]) ).
thf(13285,plain,
( ( sk36 != t )
| ( ( sk3 @ ( sk21 @ sk9 ) )
!= ( sk3 @ sk35 ) ) ),
inference(simp,[status(thm)],[13284]) ).
thf(13356,plain,
( ( sk36 != t )
| ( ( sk21 @ sk9 )
!= sk35 ) ),
inference(simp,[status(thm)],[13285]) ).
thf(8908,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk33 = A ) )
@ sk3 )
| ~ $true
| ( ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk33 = A ) ) )
!= ( sk4 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[3959,5640]) ).
thf(8909,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk33 = A ) )
@ sk3 )
| ( ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk33 = A ) ) )
!= ( sk4 @ sk3 ) ) ),
inference(simp,[status(thm)],[8908]) ).
thf(8975,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk33 = A ) )
@ sk3 )
| ( ( ^ [A: a] :
( ( sk3 @ A )
| ( sk33 = A ) ) )
!= sk3 ) ),
inference(simp,[status(thm)],[8909]) ).
thf(12444,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ~ $true
| ( ( sk3 @ ( sk21 @ A ) )
!= ( sk3 @ t ) ) ),
inference(paramod_ordered,[status(thm)],[94,4447]) ).
thf(12445,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ( ( sk3 @ ( sk21 @ A ) )
!= ( sk3 @ t ) ) ),
inference(simp,[status(thm)],[12444]) ).
thf(12450,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ( ( sk21 @ A )
!= t ) ),
inference(simp,[status(thm)],[12445]) ).
thf(13882,plain,
! [A: a] :
( ( ( sk21 @ A )
!= A )
| ( ( sk21 @ A )
!= ( sk21 @ A ) )
| ( t != A ) ),
inference(eqfactor_ordered,[status(thm)],[12450]) ).
thf(13883,plain,
( ( sk21 @ t )
!= t ),
inference(pattern_uni,[status(thm)],[13882:[bind(A,$thf( t ))]]) ).
thf(13886,plain,
! [A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( A != t )
| ( ( sk21 @ A )
!= ( sk21 @ t ) ) ),
inference(paramod_ordered,[status(thm)],[4451,13883]) ).
thf(13887,plain,
( ( sk3 @ ( sk21 @ t ) )
| ( t != t ) ),
inference(pattern_uni,[status(thm)],[13886:[bind(A,$thf( t ))]]) ).
thf(13888,plain,
sk3 @ ( sk21 @ t ),
inference(simp,[status(thm)],[13887]) ).
thf(16035,plain,
( ( sk4
@ ^ [A: a] : $true )
| ~ $true
| ( ( sk3 @ ( sk21 @ t ) )
!= ( sk3
@ ( sk7
@ ^ [A: a] : $true ) ) ) ),
inference(paramod_ordered,[status(thm)],[13888,15865]) ).
thf(16036,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk3 @ ( sk21 @ t ) )
!= ( sk3
@ ( sk7
@ ^ [A: a] : $true ) ) ) ),
inference(simp,[status(thm)],[16035]) ).
thf(16155,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk21 @ t )
!= ( sk7
@ ^ [A: a] : $true ) ) ),
inference(simp,[status(thm)],[16036]) ).
thf(16295,plain,
( ~ $true
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
!= ( sk3 @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[8292,16013]) ).
thf(16296,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
!= ( sk3 @ sk9 ) ) ),
inference(simp,[status(thm)],[16295]) ).
thf(16356,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk7
@ ^ [A: a] : $true )
!= sk9 ) ),
inference(simp,[status(thm)],[16296]) ).
thf(8,plain,
( sk1
| ( cA @ sk3 ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(101,plain,
( $false
| ( cA @ sk3 ) ),
inference(rewrite,[status(thm)],[8,90]) ).
thf(102,plain,
cA @ sk3,
inference(simp,[status(thm)],[101]) ).
thf(16033,plain,
( ( sk4
@ ^ [A: a] : $true )
| ~ $true
| ( ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
!= ( sk3 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[1524,15865]) ).
thf(16034,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
!= ( sk3 @ sk17 ) ) ),
inference(simp,[status(thm)],[16033]) ).
thf(16183,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk7
@ ^ [A: a] : $true )
!= sk17 ) ),
inference(simp,[status(thm)],[16034]) ).
thf(5025,plain,
! [A: a] :
( ~ ( sk3 @ ( sk30 @ A ) )
| ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) ) ),
inference(func_ext,[status(esa)],[4876]) ).
thf(11268,plain,
! [A: a] :
( ~ $true
| ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ t ) ) ),
inference(paramod_ordered,[status(thm)],[94,5025]) ).
thf(11269,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ t ) ) ),
inference(simp,[status(thm)],[11268]) ).
thf(11339,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk30 @ A )
!= t ) ),
inference(simp,[status(thm)],[11269]) ).
thf(16070,plain,
! [A: a > $o] :
( ~ ( sk3
@ ( sk7
@ ^ [B: a] : $true ) )
| ( sk5 @ A
@ ^ [B: a] : $false )
| ~ $true
| ( ( sk4
@ ^ [B: a] : $true )
!= ( sk4 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[15865,104]) ).
thf(16071,plain,
! [A: a > $o] :
( ~ ( sk3
@ ( sk7
@ ^ [B: a] : $true ) )
| ( sk5 @ A
@ ^ [B: a] : $false )
| ( ( sk4
@ ^ [B: a] : $true )
!= ( sk4 @ A ) ) ),
inference(simp,[status(thm)],[16070]) ).
thf(16072,plain,
( ~ ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
| ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $false ) ),
inference(pattern_uni,[status(thm)],[16071:[bind(A,$thf( ^ [B: a] : $true ))]]) ).
thf(12695,plain,
! [A: a] :
( ~ $true
| ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ ( sk21 @ sk17 ) ) ) ),
inference(paramod_ordered,[status(thm)],[12670,5025]) ).
thf(12696,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ ( sk21 @ sk17 ) ) ) ),
inference(simp,[status(thm)],[12695]) ).
thf(12764,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk30 @ A )
!= ( sk21 @ sk17 ) ) ),
inference(simp,[status(thm)],[12696]) ).
thf(79,plain,
! [D: a,C: a > $o,B: a > $o,A: a > $o] :
( sk1
| ( sk4 @ A )
| ( cA @ ( sk8 @ A ) )
| sk1
| ~ ( sk5 @ B @ C )
| ~ $true
| ( sk5 @ B
@ ^ [E: a] :
( ( C @ E )
| ( D = E ) ) )
| ~ ( sk4 @ B )
| ( ( sk6 @ A )
!= ( B @ D ) ) ),
inference(paramod_ordered,[status(thm)],[12,16]) ).
thf(80,plain,
! [D: a,C: a > $o,B: a > $o,A: a > $o] :
( sk1
| ( sk4 @ A )
| ( cA @ ( sk8 @ A ) )
| ~ ( sk5 @ B @ C )
| ( sk5 @ B
@ ^ [E: a] :
( ( C @ E )
| ( D = E ) ) )
| ~ ( sk4 @ B )
| ( ( sk6 @ A )
!= ( B @ D ) ) ),
inference(simp,[status(thm)],[79]) ).
thf(83,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( sk1
| ( sk4 @ ( C @ B ) )
| ( cA @ ( sk8 @ ( C @ B ) ) )
| ~ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ A )
| ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ),
inference(pre_uni,[status(thm)],[80:[bind(A,$thf( E @ D )),bind(B,$thf( ^ [F: a] : ( sk6 @ ( E @ F ) ) ))]]) ).
thf(86,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( sk1
| ( sk4 @ ( C @ B ) )
| ( cA @ ( sk8 @ ( C @ B ) ) )
| ~ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ A )
| ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ),
inference(simp,[status(thm)],[83]) ).
thf(7798,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( $false
| ( sk4 @ ( C @ B ) )
| ( cA @ ( sk8 @ ( C @ B ) ) )
| ~ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ A )
| ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ),
inference(rewrite,[status(thm)],[86,90]) ).
thf(7799,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( ( sk4 @ ( C @ B ) )
| ( cA @ ( sk8 @ ( C @ B ) ) )
| ~ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ A )
| ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ),
inference(simp,[status(thm)],[7798]) ).
thf(8419,plain,
( ~ $true
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ sk23 )
!= ( sk3 @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[8292,4506]) ).
thf(8420,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ sk23 )
!= ( sk3 @ sk9 ) ) ),
inference(simp,[status(thm)],[8419]) ).
thf(8446,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( sk23 != sk9 ) ),
inference(simp,[status(thm)],[8420]) ).
thf(15520,plain,
! [A: a] :
( ( cA @ ( sk8 @ ( (=) @ a @ A ) ) )
| ~ $true
| ( ( sk3 @ ( sk7 @ ( (=) @ a @ A ) ) )
!= ( sk3 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[1524,14912]) ).
thf(15521,plain,
! [A: a] :
( ( cA @ ( sk8 @ ( (=) @ a @ A ) ) )
| ( ( sk3 @ ( sk7 @ ( (=) @ a @ A ) ) )
!= ( sk3 @ sk17 ) ) ),
inference(simp,[status(thm)],[15520]) ).
thf(15578,plain,
! [A: a] :
( ( cA @ ( sk8 @ ( (=) @ a @ A ) ) )
| ( ( sk7 @ ( (=) @ a @ A ) )
!= sk17 ) ),
inference(simp,[status(thm)],[15521]) ).
thf(16002,plain,
( ( sk4
@ ^ [A: a] : $true )
| ~ $true
| ( ( sk3 @ ( sk21 @ sk17 ) )
!= ( sk3
@ ( sk7
@ ^ [A: a] : $true ) ) ) ),
inference(paramod_ordered,[status(thm)],[12670,15865]) ).
thf(16003,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk3 @ ( sk21 @ sk17 ) )
!= ( sk3
@ ( sk7
@ ^ [A: a] : $true ) ) ) ),
inference(simp,[status(thm)],[16002]) ).
thf(16144,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk21 @ sk17 )
!= ( sk7
@ ^ [A: a] : $true ) ) ),
inference(simp,[status(thm)],[16003]) ).
thf(1525,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ $true
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ( ( sk3 @ sk17 )
!= ( B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1524,110]) ).
thf(1526,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ( ( sk3 @ sk17 )
!= ( B @ A ) ) ),
inference(simp,[status(thm)],[1525]) ).
thf(1540,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk17 = A ) )
@ sk3 )
| ~ ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk17 = A ) ) ) ),
inference(pre_uni,[status(thm)],[1526:[bind(A,$thf( sk17 )),bind(B,$thf( sk3 ))]]) ).
thf(4017,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) )
@ sk3 )
| ~ $true
| ( ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) ) )
!= ( sk4 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[3959,134]) ).
thf(4018,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) )
@ sk3 )
| ( ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) ) )
!= ( sk4 @ sk3 ) ) ),
inference(simp,[status(thm)],[4017]) ).
thf(4049,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) )
@ sk3 )
| ( ( ^ [A: a] :
( ( sk3 @ A )
| ( t = A ) ) )
!= sk3 ) ),
inference(simp,[status(thm)],[4018]) ).
thf(11142,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ~ $true
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ sk33 ) ) ),
inference(paramod_ordered,[status(thm)],[5611,10768]) ).
thf(11143,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ sk33 ) ) ),
inference(simp,[status(thm)],[11142]) ).
thf(11157,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk43 @ A )
!= sk33 ) ),
inference(simp,[status(thm)],[11143]) ).
thf(81,plain,
! [D: a,C: a > $o,B: a > $o,A: a > $o] :
( sk1
| ( sk4 @ A )
| ( sk6 @ A )
| sk1
| ~ ( sk5 @ B @ C )
| ~ $true
| ( sk5 @ B
@ ^ [E: a] :
( ( C @ E )
| ( D = E ) ) )
| ~ ( sk4 @ B )
| ( ( cA @ ( sk8 @ A ) )
!= ( B @ D ) ) ),
inference(paramod_ordered,[status(thm)],[12,16]) ).
thf(82,plain,
! [D: a,C: a > $o,B: a > $o,A: a > $o] :
( sk1
| ( sk4 @ A )
| ( sk6 @ A )
| ~ ( sk5 @ B @ C )
| ( sk5 @ B
@ ^ [E: a] :
( ( C @ E )
| ( D = E ) ) )
| ~ ( sk4 @ B )
| ( ( cA @ ( sk8 @ A ) )
!= ( B @ D ) ) ),
inference(simp,[status(thm)],[81]) ).
thf(84,plain,
! [D: a > a > a > $o,C: a,B: a > $o,A: a > $o] :
( sk1
| ( sk4 @ A )
| ( sk6 @ A )
| ~ ( sk5
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) )
@ B )
| ( sk5
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) )
@ ^ [E: a] :
( ( B @ E )
| ( C = E ) ) )
| ~ ( sk4
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) ) )
| ( ( ^ [E: a] : A )
!= ( D @ C ) ) ),
inference(pre_uni,[status(thm)],[82:[bind(A,$thf( A )),bind(B,$thf( ^ [F: a] : ( cA @ ^ [G: a] : ( sk8 @ ( F @ F @ G ) @ G ) ) )),bind(C,$thf( C )),bind(D,$thf( D ))]]) ).
thf(85,plain,
! [D: a > a > a > $o,C: a,B: a > $o,A: a > $o] :
( ~ ( sk4
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) ) )
| ( sk5
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) )
@ ^ [E: a] :
( ( B @ E )
| ( C = E ) ) )
| ~ ( sk5
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) )
@ B )
| ( sk6 @ A )
| ( sk4 @ A )
| sk1
| ( ( ^ [E: a] : A )
!= ( D @ C ) ) ),
inference(pre_uni,[status(thm)],[84:[]]) ).
thf(87,plain,
! [D: a > a > a > $o,C: a,B: a > $o,A: a > $o] :
( ~ ( sk4
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) ) )
| ( sk5
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) )
@ ^ [E: a] :
( ( B @ E )
| ( C = E ) ) )
| ~ ( sk5
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) )
@ B )
| ( sk6 @ A )
| ( sk4 @ A )
| sk1
| ( ( ^ [E: a] : A )
!= ( D @ C ) ) ),
inference(simp,[status(thm)],[85]) ).
thf(8554,plain,
! [D: a > a > a > $o,C: a,B: a > $o,A: a > $o] :
( ~ ( sk4
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) ) )
| ( sk5
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) )
@ ^ [E: a] :
( ( B @ E )
| ( C = E ) ) )
| ~ ( sk5
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) )
@ B )
| ( sk6 @ A )
| ( sk4 @ A )
| $false
| ( ( ^ [E: a] : A )
!= ( D @ C ) ) ),
inference(rewrite,[status(thm)],[87,90]) ).
thf(8555,plain,
! [D: a > a > a > $o,C: a,B: a > $o,A: a > $o] :
( ~ ( sk4
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) ) )
| ( sk5
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) )
@ ^ [E: a] :
( ( B @ E )
| ( C = E ) ) )
| ~ ( sk5
@ ^ [E: a] :
( cA
@ ^ [F: a] : ( sk8 @ ( D @ E @ F ) @ F ) )
@ B )
| ( sk6 @ A )
| ( sk4 @ A )
| ( ( ^ [E: a] : A )
!= ( D @ C ) ) ),
inference(simp,[status(thm)],[8554]) ).
thf(13299,plain,
! [A: a] :
( ~ $true
| ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ ( sk21 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[13274,5025]) ).
thf(13300,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ ( sk21 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[13299]) ).
thf(13366,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk30 @ A )
!= ( sk21 @ sk9 ) ) ),
inference(simp,[status(thm)],[13300]) ).
thf(170,plain,
! [B: a > $o,A: a > $o] :
( ( sk4 @ A )
| ( cA @ ( sk8 @ A ) )
| ( sk4 @ B )
| ~ $true
| ( ( sk7 @ B )
!= t )
| ( ( sk6 @ A )
!= ( sk6 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[98,168]) ).
thf(171,plain,
! [B: a > $o,A: a > $o] :
( ( sk4 @ A )
| ( cA @ ( sk8 @ A ) )
| ( sk4 @ B )
| ( ( sk7 @ B )
!= t )
| ( ( sk6 @ A )
!= ( sk6 @ B ) ) ),
inference(simp,[status(thm)],[170]) ).
thf(172,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( cA @ ( sk8 @ A ) )
| ( sk4 @ A )
| ( ( sk7 @ A )
!= t ) ),
inference(pattern_uni,[status(thm)],[171:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(173,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ( cA @ ( sk8 @ A ) )
| ( ( sk7 @ A )
!= t ) ),
inference(simp,[status(thm)],[172]) ).
thf(13310,plain,
! [B: a,A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ~ $true
| ( sk8 @ A @ B )
| ( ( sk3 @ ( sk21 @ sk9 ) )
!= ( A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[13274,447]) ).
thf(13311,plain,
! [B: a,A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ( sk8 @ A @ B )
| ( ( sk3 @ ( sk21 @ sk9 ) )
!= ( A @ B ) ) ),
inference(simp,[status(thm)],[13310]) ).
thf(13383,plain,
( ( sk4
@ ^ [A: a] : ( sk3 @ ( sk21 @ A ) ) )
| ( sk6
@ ^ [A: a] : ( sk3 @ ( sk21 @ A ) ) )
| ( sk8
@ ^ [A: a] : ( sk3 @ ( sk21 @ A ) )
@ sk9 ) ),
inference(pre_uni,[status(thm)],[13311:[bind(A,$thf( ^ [C: a] : ( sk3 @ ( sk21 @ C ) ) )),bind(B,$thf( sk9 ))]]) ).
thf(4573,plain,
( ~ $true
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ sk23 )
!= ( sk3 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[1524,4506]) ).
thf(4574,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ sk23 )
!= ( sk3 @ sk17 ) ) ),
inference(simp,[status(thm)],[4573]) ).
thf(4613,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( sk23 != sk17 ) ),
inference(simp,[status(thm)],[4574]) ).
thf(36,plain,
! [C: a,B: a > $o,A: a > $o] :
( sk1
| ~ ( sk5 @ A @ B )
| ( sk5 @ A
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ~ ( sk4 @ A )
| ( ( A @ C )
!= ( sk5 @ A @ B ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[16]) ).
thf(51,plain,
! [C: a,B: a > $o,A: a > $o] :
( sk1
| ( sk5 @ A
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ~ ( sk5 @ A @ B )
| ~ ( sk4 @ A )
| ( ( A @ C )
!= ( sk5 @ A @ B ) ) ),
inference(simp,[status(thm)],[36]) ).
thf(1250,plain,
! [C: a,B: a > $o,A: a > $o] :
( $false
| ( sk5 @ A
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ~ ( sk5 @ A @ B )
| ~ ( sk4 @ A )
| ( ( A @ C )
!= ( sk5 @ A @ B ) ) ),
inference(rewrite,[status(thm)],[51,90]) ).
thf(1251,plain,
! [C: a,B: a > $o,A: a > $o] :
( ( sk5 @ A
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ~ ( sk5 @ A @ B )
| ~ ( sk4 @ A )
| ( ( A @ C )
!= ( sk5 @ A @ B ) ) ),
inference(simp,[status(thm)],[1250]) ).
thf(11196,plain,
! [A: a] :
( ~ $true
| ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ sk33 ) ) ),
inference(paramod_ordered,[status(thm)],[5611,5025]) ).
thf(11197,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ sk33 ) ) ),
inference(simp,[status(thm)],[11196]) ).
thf(11301,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk30 @ A )
!= sk33 ) ),
inference(simp,[status(thm)],[11197]) ).
thf(1216,plain,
( ( sk3 @ sk15 )
| ( sk4 @ sk3 )
| ( sk6 @ sk3 ) ),
inference(func_ext,[status(esa)],[1215]) ).
thf(2005,plain,
( ( sk3 @ sk15 )
| ( sk4 @ sk3 )
| ( sk4 @ sk3 )
| ~ $true
| ( ( sk6 @ sk3 )
!= ( sk6 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[1216,263]) ).
thf(2006,plain,
( ( sk3 @ sk15 )
| ( sk4 @ sk3 )
| ( ( sk6 @ sk3 )
!= ( sk6 @ sk3 ) ) ),
inference(simp,[status(thm)],[2005]) ).
thf(2007,plain,
( ( sk3 @ sk15 )
| ( sk4 @ sk3 ) ),
inference(pattern_uni,[status(thm)],[2006:[]]) ).
thf(2056,plain,
! [A: a] :
( ( sk3 @ sk15 )
| ~ $true
| ( ( sk4 @ sk3 )
!= ( sk4 @ ( (=) @ a @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[2007,1080]) ).
thf(2057,plain,
! [A: a] :
( ( sk3 @ sk15 )
| ( ( sk4 @ sk3 )
!= ( sk4 @ ( (=) @ a @ A ) ) ) ),
inference(simp,[status(thm)],[2056]) ).
thf(2070,plain,
! [A: a] :
( ( sk3 @ sk15 )
| ( sk3
!= ( (=) @ a @ A ) ) ),
inference(simp,[status(thm)],[2057]) ).
thf(2557,plain,
! [A: a] :
( ( ( sk3 @ ( sk19 @ A ) )
!= ( A
= ( sk19 @ A ) ) )
| ( sk3 @ sk15 ) ),
inference(func_ext,[status(esa)],[2070]) ).
thf(332,plain,
( ( cA @ ( sk8 @ sk3 ) )
| ~ $true
| ( ( sk4 @ sk3 )
!= ( sk4
@ ^ [A: a] : $false ) ) ),
inference(paramod_ordered,[status(thm)],[293,108]) ).
thf(333,plain,
( ( cA @ ( sk8 @ sk3 ) )
| ( ( sk4 @ sk3 )
!= ( sk4
@ ^ [A: a] : $false ) ) ),
inference(simp,[status(thm)],[332]) ).
thf(339,plain,
( ( cA @ ( sk8 @ sk3 ) )
| ( sk3
!= ( ^ [A: a] : $false ) ) ),
inference(simp,[status(thm)],[333]) ).
thf(391,plain,
( ( sk3 @ sk10 )
| ( cA @ ( sk8 @ sk3 ) ) ),
inference(func_ext,[status(esa)],[339]) ).
thf(13913,plain,
! [A: a] :
( ~ $true
| ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ ( sk21 @ t ) ) ) ),
inference(paramod_ordered,[status(thm)],[13888,5025]) ).
thf(13914,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ ( sk21 @ t ) ) ) ),
inference(simp,[status(thm)],[13913]) ).
thf(13952,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk30 @ A )
!= ( sk21 @ t ) ) ),
inference(simp,[status(thm)],[13914]) ).
thf(5431,plain,
! [B: a,A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ~ $true
| ( sk8 @ A @ B )
| ( ( sk5 @ sk3 @ ( (=) @ a @ t ) )
!= ( A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[5356,447]) ).
thf(5432,plain,
! [B: a,A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ( sk8 @ A @ B )
| ( ( sk5 @ sk3 @ ( (=) @ a @ t ) )
!= ( A @ B ) ) ),
inference(simp,[status(thm)],[5431]) ).
thf(5449,plain,
( ( sk4
@ ^ [A: a] : ( sk5 @ sk3 @ ( (=) @ a @ A ) ) )
| ( sk6
@ ^ [A: a] : ( sk5 @ sk3 @ ( (=) @ a @ A ) ) )
| ( sk8
@ ^ [A: a] : ( sk5 @ sk3 @ ( (=) @ a @ A ) )
@ t ) ),
inference(pre_uni,[status(thm)],[5432:[bind(A,$thf( ^ [C: a] : ( sk5 @ sk3 @ ( (=) @ a @ C ) ) )),bind(B,$thf( t ))]]) ).
thf(8394,plain,
( ( sk36 != t )
| ~ $true
| ( ( sk3 @ sk35 )
!= ( sk3 @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[8292,6221]) ).
thf(8395,plain,
( ( sk36 != t )
| ( ( sk3 @ sk35 )
!= ( sk3 @ sk9 ) ) ),
inference(simp,[status(thm)],[8394]) ).
thf(8452,plain,
( ( sk36 != t )
| ( sk35 != sk9 ) ),
inference(simp,[status(thm)],[8395]) ).
thf(14517,plain,
( ( sk36 != t )
| ~ $true
| ( ( sk3 @ ( sk21 @ sk33 ) )
!= ( sk3 @ sk35 ) ) ),
inference(paramod_ordered,[status(thm)],[14507,6221]) ).
thf(14518,plain,
( ( sk36 != t )
| ( ( sk3 @ ( sk21 @ sk33 ) )
!= ( sk3 @ sk35 ) ) ),
inference(simp,[status(thm)],[14517]) ).
thf(14581,plain,
( ( sk36 != t )
| ( ( sk21 @ sk33 )
!= sk35 ) ),
inference(simp,[status(thm)],[14518]) ).
thf(43,plain,
! [D: a > $o,C: a > $o,B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ A )
| ~ ( ( C @ B )
| ( D @ B ) )
| ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ ^ [E: a] :
( ( A @ E )
| ( B = E ) ) )
| ~ ( sk4
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) ) ) ),
inference(prim_subst,[status(thm)],[16:[bind(A,$thf( ^ [F: a] : ( ( D @ F ) | ( E @ F ) ) ))]]) ).
thf(58,plain,
! [D: a > $o,C: a > $o,B: a,A: a > $o] :
( ( sk1
| ~ ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ A )
| ~ ( C @ B )
| ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ ^ [E: a] :
( ( A @ E )
| ( B = E ) ) )
| ~ ( sk4
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) ) ) )
& ( sk1
| ~ ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ A )
| ~ ( D @ B )
| ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ ^ [E: a] :
( ( A @ E )
| ( B = E ) ) )
| ~ ( sk4
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) ) ) ) ),
inference(cnf,[status(esa)],[43]) ).
thf(60,plain,
! [D: a > $o,C: a > $o,B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ A )
| ~ ( D @ B )
| ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ ^ [E: a] :
( ( A @ E )
| ( B = E ) ) )
| ~ ( sk4
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) ) ) ),
inference(cnfConj,[status(thm)],[58]) ).
thf(62,plain,
! [D: a > $o,C: a > $o,B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ A )
| ~ ( D @ B )
| ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ ^ [E: a] :
( ( A @ E )
| ( B = E ) ) )
| ~ ( sk4
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) ) ) ),
inference(simp,[status(thm)],[60]) ).
thf(3159,plain,
! [D: a > $o,C: a > $o,B: a,A: a > $o] :
( $false
| ~ ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ A )
| ~ ( D @ B )
| ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ ^ [E: a] :
( ( A @ E )
| ( B = E ) ) )
| ~ ( sk4
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) ) ) ),
inference(rewrite,[status(thm)],[62,90]) ).
thf(3160,plain,
! [D: a > $o,C: a > $o,B: a,A: a > $o] :
( ~ ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ A )
| ~ ( D @ B )
| ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ ^ [E: a] :
( ( A @ E )
| ( B = E ) ) )
| ~ ( sk4
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) ) ) ),
inference(simp,[status(thm)],[3159]) ).
thf(13898,plain,
( ( sk36 != t )
| ~ $true
| ( ( sk3 @ ( sk21 @ t ) )
!= ( sk3 @ sk35 ) ) ),
inference(paramod_ordered,[status(thm)],[13888,6221]) ).
thf(13899,plain,
( ( sk36 != t )
| ( ( sk3 @ ( sk21 @ t ) )
!= ( sk3 @ sk35 ) ) ),
inference(simp,[status(thm)],[13898]) ).
thf(13980,plain,
( ( sk36 != t )
| ( ( sk21 @ t )
!= sk35 ) ),
inference(simp,[status(thm)],[13899]) ).
thf(11150,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ~ $true
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[8292,10768]) ).
thf(11151,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ sk9 ) ) ),
inference(simp,[status(thm)],[11150]) ).
thf(11156,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk43 @ A )
!= sk9 ) ),
inference(simp,[status(thm)],[11151]) ).
thf(11146,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ~ $true
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[1524,10768]) ).
thf(11147,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ sk17 ) ) ),
inference(simp,[status(thm)],[11146]) ).
thf(11158,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk43 @ A )
!= sk17 ) ),
inference(simp,[status(thm)],[11147]) ).
thf(59,plain,
! [D: a > $o,C: a > $o,B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ A )
| ~ ( C @ B )
| ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ ^ [E: a] :
( ( A @ E )
| ( B = E ) ) )
| ~ ( sk4
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) ) ) ),
inference(cnfConj,[status(thm)],[58]) ).
thf(61,plain,
! [D: a > $o,C: a > $o,B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ A )
| ~ ( C @ B )
| ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ ^ [E: a] :
( ( A @ E )
| ( B = E ) ) )
| ~ ( sk4
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) ) ) ),
inference(simp,[status(thm)],[59]) ).
thf(2663,plain,
! [D: a > $o,C: a > $o,B: a,A: a > $o] :
( $false
| ~ ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ A )
| ~ ( C @ B )
| ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ ^ [E: a] :
( ( A @ E )
| ( B = E ) ) )
| ~ ( sk4
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) ) ) ),
inference(rewrite,[status(thm)],[61,90]) ).
thf(2664,plain,
! [D: a > $o,C: a > $o,B: a,A: a > $o] :
( ~ ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ A )
| ~ ( C @ B )
| ( sk5
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) )
@ ^ [E: a] :
( ( A @ E )
| ( B = E ) ) )
| ~ ( sk4
@ ^ [E: a] :
( ( C @ E )
| ( D @ E ) ) ) ),
inference(simp,[status(thm)],[2663]) ).
thf(120,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ( ( B @ A )
!= ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[110]) ).
thf(130,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ( ( B @ A )
!= ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B ) ) ),
inference(simp,[status(thm)],[120]) ).
thf(13936,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ~ $true
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ ( sk21 @ t ) ) ) ),
inference(paramod_ordered,[status(thm)],[13888,10768]) ).
thf(13937,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ ( sk21 @ t ) ) ) ),
inference(simp,[status(thm)],[13936]) ).
thf(13963,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk43 @ A )
!= ( sk21 @ t ) ) ),
inference(simp,[status(thm)],[13937]) ).
thf(13932,plain,
( ~ $true
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ ( sk21 @ t ) )
!= ( sk3 @ sk23 ) ) ),
inference(paramod_ordered,[status(thm)],[13888,4506]) ).
thf(13933,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ ( sk21 @ t ) )
!= ( sk3 @ sk23 ) ) ),
inference(simp,[status(thm)],[13932]) ).
thf(13944,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk21 @ t )
!= sk23 ) ),
inference(simp,[status(thm)],[13933]) ).
thf(39,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [D: a] : ( sk4 @ ( C @ D ) )
@ A )
| ~ ( sk4 @ ( C @ B ) )
| ( sk5
@ ^ [D: a] : ( sk4 @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( sk4 @ ( C @ D ) ) ) ),
inference(prim_subst,[status(thm)],[16:[bind(A,$thf( ^ [E: a] : ( sk4 @ ( D @ E ) ) ))]]) ).
thf(56,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [D: a] : ( sk4 @ ( C @ D ) )
@ A )
| ~ ( sk4 @ ( C @ B ) )
| ( sk5
@ ^ [D: a] : ( sk4 @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( sk4 @ ( C @ D ) ) ) ),
inference(simp,[status(thm)],[39]) ).
thf(2085,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( $false
| ~ ( sk5
@ ^ [D: a] : ( sk4 @ ( C @ D ) )
@ A )
| ~ ( sk4 @ ( C @ B ) )
| ( sk5
@ ^ [D: a] : ( sk4 @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( sk4 @ ( C @ D ) ) ) ),
inference(rewrite,[status(thm)],[56,90]) ).
thf(2086,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( ~ ( sk5
@ ^ [D: a] : ( sk4 @ ( C @ D ) )
@ A )
| ~ ( sk4 @ ( C @ B ) )
| ( sk5
@ ^ [D: a] : ( sk4 @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( sk4 @ ( C @ D ) ) ) ),
inference(simp,[status(thm)],[2085]) ).
thf(5632,plain,
( ~ $true
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ sk33 )
!= ( sk3 @ sk23 ) ) ),
inference(paramod_ordered,[status(thm)],[5611,4506]) ).
thf(5633,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ sk33 )
!= ( sk3 @ sk23 ) ) ),
inference(simp,[status(thm)],[5632]) ).
thf(5646,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( sk33 != sk23 ) ),
inference(simp,[status(thm)],[5633]) ).
thf(186,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ~ ( sk6 @ A )
| ~ ( sk5
@ ^ [B: a] : $true
@ ^ [B: a] : $true )
| ~ $true
| ( ( A @ ( sk7 @ A ) )
!= ( sk4
@ ^ [B: a] : $true ) ) ),
inference(paramod_ordered,[status(thm)],[175,141]) ).
thf(187,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ~ ( sk6 @ A )
| ~ ( sk5
@ ^ [B: a] : $true
@ ^ [B: a] : $true )
| ( ( A @ ( sk7 @ A ) )
!= ( sk4
@ ^ [B: a] : $true ) ) ),
inference(simp,[status(thm)],[186]) ).
thf(241,plain,
( ( sk4
@ ^ [A: a] :
( sk4
@ ^ [B: a] : $true ) )
| ~ ( sk6
@ ^ [A: a] :
( sk4
@ ^ [B: a] : $true ) )
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true ) ),
inference(pre_uni,[status(thm)],[187:[bind(A,$thf( ^ [B: a] : ( sk4 @ ^ [C: a] : $true ) ))]]) ).
thf(14551,plain,
( ~ $true
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ ( sk21 @ sk33 ) )
!= ( sk3 @ sk23 ) ) ),
inference(paramod_ordered,[status(thm)],[14507,4506]) ).
thf(14552,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3 @ ( sk21 @ sk33 ) )
!= ( sk3 @ sk23 ) ) ),
inference(simp,[status(thm)],[14551]) ).
thf(14599,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk21 @ sk33 )
!= sk23 ) ),
inference(simp,[status(thm)],[14552]) ).
thf(12706,plain,
! [B: a,A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ~ $true
| ( sk8 @ A @ B )
| ( ( sk3 @ ( sk21 @ sk17 ) )
!= ( A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[12670,447]) ).
thf(12707,plain,
! [B: a,A: a > $o] :
( ( sk4 @ A )
| ( sk6 @ A )
| ( sk8 @ A @ B )
| ( ( sk3 @ ( sk21 @ sk17 ) )
!= ( A @ B ) ) ),
inference(simp,[status(thm)],[12706]) ).
thf(12779,plain,
( ( sk4
@ ^ [A: a] : ( sk3 @ ( sk21 @ A ) ) )
| ( sk6
@ ^ [A: a] : ( sk3 @ ( sk21 @ A ) ) )
| ( sk8
@ ^ [A: a] : ( sk3 @ ( sk21 @ A ) )
@ sk17 ) ),
inference(pre_uni,[status(thm)],[12707:[bind(A,$thf( ^ [C: a] : ( sk3 @ ( sk21 @ C ) ) )),bind(B,$thf( sk17 ))]]) ).
thf(212,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ~ ( sk6 @ A )
| ( ( A @ ( sk7 @ A ) )
!= ( sk4 @ A ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[175]) ).
thf(226,plain,
! [A: a > $o] :
( ( sk4 @ A )
| ~ ( sk6 @ A )
| ( ( A @ ( sk7 @ A ) )
!= ( sk4 @ A ) ) ),
inference(simp,[status(thm)],[212]) ).
thf(13878,plain,
! [B: a,A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( A != B )
| ( ( sk21 @ B )
!= t )
| ( ( sk21 @ A )
!= ( sk21 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[4451,12450]) ).
thf(13879,plain,
! [A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( A != A )
| ( ( sk21 @ A )
!= t ) ),
inference(pattern_uni,[status(thm)],[13878:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(13884,plain,
! [A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( ( sk21 @ A )
!= t ) ),
inference(simp,[status(thm)],[13879]) ).
thf(11227,plain,
! [A: a] :
( ~ $true
| ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[1524,5025]) ).
thf(11228,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ sk17 ) ) ),
inference(simp,[status(thm)],[11227]) ).
thf(11316,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk30 @ A )
!= sk17 ) ),
inference(simp,[status(thm)],[11228]) ).
thf(16242,plain,
( ~ $true
| ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
!= ( sk3 @ sk33 ) ) ),
inference(paramod_ordered,[status(thm)],[5611,16013]) ).
thf(16243,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : $true ) )
!= ( sk3 @ sk33 ) ) ),
inference(simp,[status(thm)],[16242]) ).
thf(16342,plain,
( ~ ( sk5
@ ^ [A: a] : $true
@ ^ [A: a] : $true )
| ( ( sk7
@ ^ [A: a] : $true )
!= sk33 ) ),
inference(simp,[status(thm)],[16243]) ).
thf(1460,plain,
( ( sk3 @ sk16 )
| ( sk4 @ sk3 ) ),
inference(func_ext,[status(esa)],[1229]) ).
thf(1583,plain,
! [A: a] :
( ( sk3 @ sk16 )
| ~ $true
| ( ( sk4 @ sk3 )
!= ( sk4 @ ( (=) @ a @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[1460,1080]) ).
thf(1584,plain,
! [A: a] :
( ( sk3 @ sk16 )
| ( ( sk4 @ sk3 )
!= ( sk4 @ ( (=) @ a @ A ) ) ) ),
inference(simp,[status(thm)],[1583]) ).
thf(1602,plain,
! [A: a] :
( ( sk3 @ sk16 )
| ( sk3
!= ( (=) @ a @ A ) ) ),
inference(simp,[status(thm)],[1584]) ).
thf(2333,plain,
! [A: a] :
( ( ( sk3 @ ( sk18 @ A ) )
!= ( A
= ( sk18 @ A ) ) )
| ( sk3 @ sk16 ) ),
inference(func_ext,[status(esa)],[1602]) ).
thf(6222,plain,
( ( sk36 != t )
| ~ $true
| ( ( sk3 @ sk35 )
!= ( sk3 @ sk33 ) ) ),
inference(paramod_ordered,[status(thm)],[5611,6221]) ).
thf(6223,plain,
( ( sk36 != t )
| ( ( sk3 @ sk35 )
!= ( sk3 @ sk33 ) ) ),
inference(simp,[status(thm)],[6222]) ).
thf(6238,plain,
( ( sk36 != t )
| ( sk35 != sk33 ) ),
inference(simp,[status(thm)],[6223]) ).
thf(13322,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ~ $true
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ ( sk21 @ sk9 ) ) ) ),
inference(paramod_ordered,[status(thm)],[13274,10768]) ).
thf(13323,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk3 @ ( sk43 @ A ) )
!= ( sk3 @ ( sk21 @ sk9 ) ) ) ),
inference(simp,[status(thm)],[13322]) ).
thf(13367,plain,
! [A: a] :
( ( ( sk44 @ A )
!= t )
| ( ( sk43 @ A )
!= ( sk21 @ sk9 ) ) ),
inference(simp,[status(thm)],[13323]) ).
thf(1090,plain,
! [A: a] :
( ( cA @ ( sk8 @ sk3 ) )
| ~ $true
| ( ( sk4 @ sk3 )
!= ( sk4 @ ( (=) @ a @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[293,1080]) ).
thf(1091,plain,
! [A: a] :
( ( cA @ ( sk8 @ sk3 ) )
| ( ( sk4 @ sk3 )
!= ( sk4 @ ( (=) @ a @ A ) ) ) ),
inference(simp,[status(thm)],[1090]) ).
thf(1094,plain,
! [A: a] :
( ( cA @ ( sk8 @ sk3 ) )
| ( sk3
!= ( (=) @ a @ A ) ) ),
inference(simp,[status(thm)],[1091]) ).
thf(1098,plain,
! [A: a] :
( ( ( sk3 @ ( sk13 @ A ) )
!= ( A
= ( sk13 @ A ) ) )
| ( cA @ ( sk8 @ sk3 ) ) ),
inference(func_ext,[status(esa)],[1094]) ).
thf(5212,plain,
! [A: a > $o] :
( ~ ( sk5 @ sk3 @ A )
| ~ $true
| ( ( sk5 @ sk3
@ ^ [B: a] :
( ( A @ B )
| ( t = B ) ) )
!= ( sk5 @ sk3 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[5181,3995]) ).
thf(5213,plain,
! [A: a > $o] :
( ~ ( sk5 @ sk3 @ A )
| ( ( sk5 @ sk3
@ ^ [B: a] :
( ( A @ B )
| ( t = B ) ) )
!= ( sk5 @ sk3 @ sk3 ) ) ),
inference(simp,[status(thm)],[5212]) ).
thf(5306,plain,
! [A: a > $o] :
( ~ ( sk5 @ sk3 @ A )
| ( sk3 != sk3 )
| ( ( ^ [B: a] :
( ( A @ B )
| ( t = B ) ) )
!= sk3 ) ),
inference(simp,[status(thm)],[5213]) ).
thf(5347,plain,
! [A: a > $o] :
( ~ ( sk5 @ sk3 @ A )
| ( ( ^ [B: a] :
( ( A @ B )
| ( t = B ) ) )
!= sk3 ) ),
inference(simp,[status(thm)],[5306]) ).
thf(11251,plain,
! [A: a] :
( ~ $true
| ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ sk9 ) ) ),
inference(paramod_ordered,[status(thm)],[8292,5025]) ).
thf(11252,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ sk9 ) ) ),
inference(simp,[status(thm)],[11251]) ).
thf(11349,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk30 @ A )
!= sk9 ) ),
inference(simp,[status(thm)],[11252]) ).
thf(10765,plain,
! [A: a] :
( ~ ( sk3 @ ( sk43 @ A ) )
| ( A
!= ( sk44 @ A ) ) ),
inference(cnfConj,[status(thm)],[10764]) ).
thf(10767,plain,
! [A: a] :
( ( ( sk44 @ A )
!= A )
| ~ ( sk3 @ ( sk43 @ A ) ) ),
inference(lifteq,[status(thm)],[10765]) ).
thf(3178,plain,
! [E: a > $o,D: a > $o,C: a > $o,B: a,A: a > $o] :
( ~ ( sk5
@ ^ [F: a] :
( ( C @ F )
| ( D @ F ) )
@ A )
| ~ ( D @ B )
| ~ ( sk4
@ ^ [F: a] :
( ( C @ F )
| ( D @ F ) ) )
| ~ $true
| ~ ( sk4 @ E )
| ( ( sk5
@ ^ [F: a] :
( ( C @ F )
| ( D @ F ) )
@ ^ [F: a] :
( ( A @ F )
| ( B = F ) ) )
!= ( sk5 @ E @ E ) ) ),
inference(paramod_ordered,[status(thm)],[3160,96]) ).
thf(3179,plain,
! [E: a > $o,D: a > $o,C: a > $o,B: a,A: a > $o] :
( ~ ( sk5
@ ^ [F: a] :
( ( C @ F )
| ( D @ F ) )
@ A )
| ~ ( D @ B )
| ~ ( sk4
@ ^ [F: a] :
( ( C @ F )
| ( D @ F ) ) )
| ~ ( sk4 @ E )
| ( ( sk5
@ ^ [F: a] :
( ( C @ F )
| ( D @ F ) )
@ ^ [F: a] :
( ( A @ F )
| ( B = F ) ) )
!= ( sk5 @ E @ E ) ) ),
inference(simp,[status(thm)],[3178]) ).
thf(3180,plain,
! [B: a,A: a > $o] :
( ~ ( sk5
@ ^ [C: a] :
( ( A @ C )
| ( B = C ) )
@ A )
| ( B != B )
| ~ ( sk4
@ ^ [C: a] :
( ( A @ C )
| ( B = C ) ) )
| ~ ( sk4
@ ^ [C: a] :
( ( A @ C )
| ( B = C ) ) ) ),
inference(pattern_uni,[status(thm)],[3179:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( (=) @ a @ B )),bind(E,$thf( ^ [F: a] : ( ( A @ F ) | ( B = F ) ) ))]]) ).
thf(3340,plain,
! [B: a,A: a > $o] :
( ( B != B )
| ~ ( sk5
@ ^ [C: a] :
( ( A @ C )
| ( B = C ) )
@ A )
| ~ ( sk4
@ ^ [C: a] :
( ( A @ C )
| ( B = C ) ) )
| ~ ( sk4
@ ^ [C: a] :
( ( A @ C )
| ( B = C ) ) ) ),
inference(lifteq,[status(thm)],[3180]) ).
thf(3447,plain,
! [B: a,A: a > $o] :
( ~ ( sk5
@ ^ [C: a] :
( ( A @ C )
| ( B = C ) )
@ A )
| ~ ( sk4
@ ^ [C: a] :
( ( A @ C )
| ( B = C ) ) ) ),
inference(simp,[status(thm)],[3340]) ).
thf(16062,plain,
( ( sk4
@ ^ [A: a] : $true )
| ~ $true
| ( ( sk3 @ ( sk21 @ sk33 ) )
!= ( sk3
@ ( sk7
@ ^ [A: a] : $true ) ) ) ),
inference(paramod_ordered,[status(thm)],[14507,15865]) ).
thf(16063,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk3 @ ( sk21 @ sk33 ) )
!= ( sk3
@ ( sk7
@ ^ [A: a] : $true ) ) ) ),
inference(simp,[status(thm)],[16062]) ).
thf(16161,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk21 @ sk33 )
!= ( sk7
@ ^ [A: a] : $true ) ) ),
inference(simp,[status(thm)],[16063]) ).
thf(12680,plain,
( ( sk36 != t )
| ~ $true
| ( ( sk3 @ ( sk21 @ sk17 ) )
!= ( sk3 @ sk35 ) ) ),
inference(paramod_ordered,[status(thm)],[12670,6221]) ).
thf(12681,plain,
( ( sk36 != t )
| ( ( sk3 @ ( sk21 @ sk17 ) )
!= ( sk3 @ sk35 ) ) ),
inference(simp,[status(thm)],[12680]) ).
thf(12775,plain,
( ( sk36 != t )
| ( ( sk21 @ sk17 )
!= sk35 ) ),
inference(simp,[status(thm)],[12681]) ).
thf(14497,plain,
! [B: a,A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( A != B )
| ( ( sk21 @ B )
!= sk33 )
| ( ( sk21 @ A )
!= ( sk21 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[4451,12451]) ).
thf(14498,plain,
! [A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( A != A )
| ( ( sk21 @ A )
!= sk33 ) ),
inference(pattern_uni,[status(thm)],[14497:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(14503,plain,
! [A: a] :
( ( sk3 @ ( sk21 @ A ) )
| ( ( sk21 @ A )
!= sk33 ) ),
inference(simp,[status(thm)],[14498]) ).
thf(40,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ A )
| ~ ( sk6 @ ( C @ B ) )
| ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ),
inference(prim_subst,[status(thm)],[16:[bind(A,$thf( ^ [E: a] : ( sk6 @ ( D @ E ) ) ))]]) ).
thf(57,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ A )
| ~ ( sk6 @ ( C @ B ) )
| ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ),
inference(simp,[status(thm)],[40]) ).
thf(2398,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( $false
| ~ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ A )
| ~ ( sk6 @ ( C @ B ) )
| ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ),
inference(rewrite,[status(thm)],[57,90]) ).
thf(2399,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( ~ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ A )
| ~ ( sk6 @ ( C @ B ) )
| ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ),
inference(simp,[status(thm)],[2398]) ).
thf(178,plain,
! [C: a > $o,B: a,A: a > $o] :
( ( sk4 @ A )
| ~ ( sk6 @ A )
| ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( B = D ) )
@ C )
| ~ $true
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( B = D ) ) )
| ( ( A @ ( sk7 @ A ) )
!= ( C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[175,110]) ).
thf(179,plain,
! [C: a > $o,B: a,A: a > $o] :
( ( sk4 @ A )
| ~ ( sk6 @ A )
| ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( B = D ) )
@ C )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( B = D ) ) )
| ( ( A @ ( sk7 @ A ) )
!= ( C @ B ) ) ),
inference(simp,[status(thm)],[178]) ).
thf(238,plain,
! [C: a > $o,B: a,A: a > $o] :
( ( sk4 @ A )
| ~ ( sk6 @ A )
| ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( B = D ) )
@ C )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( B = D ) ) )
| ( ( A @ ( sk7 @ A ) )
!= ( C @ B ) ) ),
inference(pre_uni,[status(thm)],[179:[]]) ).
thf(239,plain,
! [C: a > $o,B: a,A: a > $o] :
( ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( B = D ) ) )
| ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( B = D ) )
@ C )
| ~ ( sk6 @ A )
| ( sk4 @ A )
| ( ( A @ ( sk7 @ A ) )
!= ( C @ B ) ) ),
inference(pre_uni,[status(thm)],[238:[]]) ).
thf(14532,plain,
! [A: a] :
( ~ $true
| ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ ( sk21 @ sk33 ) ) ) ),
inference(paramod_ordered,[status(thm)],[14507,5025]) ).
thf(14533,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk3 @ ( sk30 @ A ) )
!= ( sk3 @ ( sk21 @ sk33 ) ) ) ),
inference(simp,[status(thm)],[14532]) ).
thf(14563,plain,
! [A: a] :
( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
| ( ( sk30 @ A )
!= ( sk21 @ sk33 ) ) ),
inference(simp,[status(thm)],[14533]) ).
thf(38,plain,
! [C: a > $o,B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [D: a] :
~ ( C @ D )
@ A )
| ~ ~ ( C @ B )
| ( sk5
@ ^ [D: a] :
~ ( C @ D )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] :
~ ( C @ D ) ) ),
inference(prim_subst,[status(thm)],[16:[bind(A,$thf( ^ [E: a] : ~ ( D @ E ) ))]]) ).
thf(54,plain,
! [C: a > $o,B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [D: a] :
~ ( C @ D )
@ A )
| ( C @ B )
| ( sk5
@ ^ [D: a] :
~ ( C @ D )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] :
~ ( C @ D ) ) ),
inference(cnf,[status(esa)],[38]) ).
thf(55,plain,
! [C: a > $o,B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [D: a] :
~ ( C @ D )
@ A )
| ( C @ B )
| ( sk5
@ ^ [D: a] :
~ ( C @ D )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] :
~ ( C @ D ) ) ),
inference(simp,[status(thm)],[54]) ).
thf(1609,plain,
! [C: a > $o,B: a,A: a > $o] :
( $false
| ~ ( sk5
@ ^ [D: a] :
~ ( C @ D )
@ A )
| ( C @ B )
| ( sk5
@ ^ [D: a] :
~ ( C @ D )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] :
~ ( C @ D ) ) ),
inference(rewrite,[status(thm)],[55,90]) ).
thf(1610,plain,
! [C: a > $o,B: a,A: a > $o] :
( ~ ( sk5
@ ^ [D: a] :
~ ( C @ D )
@ A )
| ( C @ B )
| ( sk5
@ ^ [D: a] :
~ ( C @ D )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] :
~ ( C @ D ) ) ),
inference(simp,[status(thm)],[1609]) ).
thf(29,plain,
! [F: a,E: a > $o,D: a > $o,C: a,B: a > $o,A: a > $o] :
( sk1
| ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ~ ( sk4 @ A )
| sk1
| ~ ( sk5 @ D @ E )
| ~ $true
| ( sk5 @ D
@ ^ [G: a] :
( ( E @ G )
| ( F = G ) ) )
| ~ ( sk4 @ D )
| ( ( sk5 @ A
@ ^ [G: a] :
( ( B @ G )
| ( C = G ) ) )
!= ( D @ F ) ) ),
inference(paramod_ordered,[status(thm)],[16,16]) ).
thf(30,plain,
! [F: a,E: a > $o,D: a > $o,C: a,B: a > $o,A: a > $o] :
( sk1
| ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ~ ( sk4 @ A )
| ~ ( sk5 @ D @ E )
| ( sk5 @ D
@ ^ [G: a] :
( ( E @ G )
| ( F = G ) ) )
| ~ ( sk4 @ D )
| ( ( sk5 @ A
@ ^ [G: a] :
( ( B @ G )
| ( C = G ) ) )
!= ( D @ F ) ) ),
inference(simp,[status(thm)],[29]) ).
thf(52,plain,
! [F: a > a > a,E: a > a > $o,D: a > a > $o,C: a,B: a > $o,A: a] :
( sk1
| ~ ( sk5 @ ( D @ C ) @ ( E @ C ) )
| ~ ( D @ C @ A )
| ~ ( sk4 @ ( D @ C ) )
| ~ ( sk5
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) )
@ B )
| ( sk5
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) )
@ ^ [G: a] :
( ( B @ G )
| ( C = G ) ) )
| ~ ( sk4
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) ) )
| ( ( ^ [G: a] : A )
!= ( F @ C ) ) ),
inference(pre_uni,[status(thm)],[30:[bind(A,$thf( G @ F )),bind(B,$thf( I @ F )),bind(C,$thf( C )),bind(D,$thf( ^ [J: a] : ( sk5 @ ( G @ J ) @ ^ [K: a] : ( ( I @ J @ K ) | ( ( K @ J @ K ) = K ) ) ) )),bind(E,$thf( E )),bind(F,$thf( F ))]]) ).
thf(53,plain,
! [F: a > a > a,E: a > a > $o,D: a > a > $o,C: a,B: a > $o,A: a] :
( ~ ( sk4
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) ) )
| ( sk5
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) )
@ ^ [G: a] :
( ( B @ G )
| ( C = G ) ) )
| ~ ( sk5
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) )
@ B )
| ~ ( sk4 @ ( D @ C ) )
| ~ ( D @ C @ A )
| ~ ( sk5 @ ( D @ C ) @ ( E @ C ) )
| sk1
| ( ( ^ [G: a] : A )
!= ( F @ C ) ) ),
inference(pre_uni,[status(thm)],[52:[]]) ).
thf(69,plain,
! [F: a > a > a,E: a > a > $o,D: a > a > $o,C: a,B: a > $o,A: a] :
( ~ ( sk4
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) ) )
| ( sk5
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) )
@ ^ [G: a] :
( ( B @ G )
| ( C = G ) ) )
| ~ ( sk5
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) )
@ B )
| ~ ( sk4 @ ( D @ C ) )
| ~ ( D @ C @ A )
| ~ ( sk5 @ ( D @ C ) @ ( E @ C ) )
| sk1
| ( ( ^ [G: a] : A )
!= ( F @ C ) ) ),
inference(simp,[status(thm)],[53]) ).
thf(5667,plain,
! [F: a > a > a,E: a > a > $o,D: a > a > $o,C: a,B: a > $o,A: a] :
( ~ ( sk4
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) ) )
| ( sk5
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) )
@ ^ [G: a] :
( ( B @ G )
| ( C = G ) ) )
| ~ ( sk5
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) )
@ B )
| ~ ( sk4 @ ( D @ C ) )
| ~ ( D @ C @ A )
| ~ ( sk5 @ ( D @ C ) @ ( E @ C ) )
| $false
| ( ( ^ [G: a] : A )
!= ( F @ C ) ) ),
inference(rewrite,[status(thm)],[69,90]) ).
thf(5668,plain,
! [F: a > a > a,E: a > a > $o,D: a > a > $o,C: a,B: a > $o,A: a] :
( ~ ( sk4
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) ) )
| ( sk5
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) )
@ ^ [G: a] :
( ( B @ G )
| ( C = G ) ) )
| ~ ( sk5
@ ^ [G: a] :
( sk5 @ ( D @ G )
@ ^ [H: a] :
( ( E @ G @ H )
| ( ( F @ G @ H )
= H ) ) )
@ B )
| ~ ( sk4 @ ( D @ C ) )
| ~ ( D @ C @ A )
| ~ ( sk5 @ ( D @ C ) @ ( E @ C ) )
| ( ( ^ [G: a] : A )
!= ( F @ C ) ) ),
inference(simp,[status(thm)],[5667]) ).
thf(26,plain,
! [F: a,E: a > $o,D: a > $o,C: a,B: a > $o,A: a > $o] :
( sk1
| ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ~ ( sk4 @ A )
| sk1
| ~ $true
| ~ ( D @ F )
| ( sk5 @ D
@ ^ [G: a] :
( ( E @ G )
| ( F = G ) ) )
| ~ ( sk4 @ D )
| ( ( sk5 @ A
@ ^ [G: a] :
( ( B @ G )
| ( C = G ) ) )
!= ( sk5 @ D @ E ) ) ),
inference(paramod_ordered,[status(thm)],[16,16]) ).
thf(27,plain,
! [F: a,E: a > $o,D: a > $o,C: a,B: a > $o,A: a > $o] :
( sk1
| ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ~ ( sk4 @ A )
| ~ ( D @ F )
| ( sk5 @ D
@ ^ [G: a] :
( ( E @ G )
| ( F = G ) ) )
| ~ ( sk4 @ D )
| ( ( sk5 @ A
@ ^ [G: a] :
( ( B @ G )
| ( C = G ) ) )
!= ( sk5 @ D @ E ) ) ),
inference(simp,[status(thm)],[26]) ).
thf(28,plain,
! [D: a > $o,C: a,B: a,A: a > $o] :
( sk1
| ~ ( sk5 @ A @ D )
| ~ ( A @ B )
| ~ ( sk4 @ A )
| ~ ( A @ C )
| ( sk5 @ A
@ ^ [E: a] :
( ( D @ E )
| ( B = E )
| ( C = E ) ) )
| ~ ( sk4 @ A ) ),
inference(pattern_uni,[status(thm)],[27:[bind(A,$thf( A )),bind(B,$thf( G )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( ^ [H: a] : ( ( G @ H ) | ( C = H ) ) )),bind(F,$thf( F ))]]) ).
thf(76,plain,
! [D: a > $o,C: a,B: a,A: a > $o] :
( sk1
| ~ ( sk5 @ A @ D )
| ~ ( A @ B )
| ~ ( sk4 @ A )
| ~ ( A @ C )
| ( sk5 @ A
@ ^ [E: a] :
( ( D @ E )
| ( B = E )
| ( C = E ) ) ) ),
inference(simp,[status(thm)],[28]) ).
thf(6328,plain,
! [D: a > $o,C: a,B: a,A: a > $o] :
( $false
| ~ ( sk5 @ A @ D )
| ~ ( A @ B )
| ~ ( sk4 @ A )
| ~ ( A @ C )
| ( sk5 @ A
@ ^ [E: a] :
( ( D @ E )
| ( B = E )
| ( C = E ) ) ) ),
inference(rewrite,[status(thm)],[76,90]) ).
thf(6329,plain,
! [D: a > $o,C: a,B: a,A: a > $o] :
( ~ ( sk5 @ A @ D )
| ~ ( A @ B )
| ~ ( sk4 @ A )
| ~ ( A @ C )
| ( sk5 @ A
@ ^ [E: a] :
( ( D @ E )
| ( B = E )
| ( C = E ) ) ) ),
inference(simp,[status(thm)],[6328]) ).
thf(16124,plain,
( ( sk4
@ ^ [A: a] : $true )
| ~ $true
| ( ( sk3 @ ( sk21 @ sk9 ) )
!= ( sk3
@ ( sk7
@ ^ [A: a] : $true ) ) ) ),
inference(paramod_ordered,[status(thm)],[13274,15865]) ).
thf(16125,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk3 @ ( sk21 @ sk9 ) )
!= ( sk3
@ ( sk7
@ ^ [A: a] : $true ) ) ) ),
inference(simp,[status(thm)],[16124]) ).
thf(16190,plain,
( ( sk4
@ ^ [A: a] : $true )
| ( ( sk21 @ sk9 )
!= ( sk7
@ ^ [A: a] : $true ) ) ),
inference(simp,[status(thm)],[16125]) ).
thf(792,plain,
! [E: a > $o,D: a,C: a,B: a > $o,A: a > $o] :
( ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ( ( sk4 @ A )
!= ( A @ C ) )
| ~ $true
| ~ ( E @ D )
| ~ ( sk4
@ ^ [F: a] :
( ( E @ F )
| ( D = F ) ) )
| ( ( sk5 @ A
@ ^ [F: a] :
( ( B @ F )
| ( C = F ) ) )
!= ( sk5
@ ^ [F: a] :
( ( E @ F )
| ( D = F ) )
@ E ) ) ),
inference(paramod_ordered,[status(thm)],[786,110]) ).
thf(793,plain,
! [E: a > $o,D: a,C: a,B: a > $o,A: a > $o] :
( ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ( ( sk4 @ A )
!= ( A @ C ) )
| ~ ( E @ D )
| ~ ( sk4
@ ^ [F: a] :
( ( E @ F )
| ( D = F ) ) )
| ( ( sk5 @ A
@ ^ [F: a] :
( ( B @ F )
| ( C = F ) ) )
!= ( sk5
@ ^ [F: a] :
( ( E @ F )
| ( D = F ) )
@ E ) ) ),
inference(simp,[status(thm)],[792]) ).
thf(794,plain,
! [C: a > $o,B: a,A: a] :
( ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ~ ( ( C @ A )
| ( A = A )
| ( B = A ) )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ~ ( ( C @ B )
| ( A = B ) )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) ),
inference(pattern_uni,[status(thm)],[793:[bind(A,$thf( ^ [G: a] : ( ( J @ G ) | ( C = G ) | ( D = G ) ) )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( ^ [G: a] : ( ( J @ G ) | ( C = G ) ) ))]]) ).
thf(979,plain,
! [C: a > $o,B: a,A: a] :
( ( ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ~ ( C @ A )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ~ ( C @ B )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) )
& ( ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ~ ( C @ A )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ( A != B )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) )
& ( ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ( A != A )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ~ ( C @ B )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) )
& ( ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ( A != A )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ( A != B )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) )
& ( ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ( B != A )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ~ ( C @ B )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) )
& ( ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ( B != A )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ( A != B )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) ) ),
inference(cnf,[status(esa)],[794]) ).
thf(982,plain,
! [C: a > $o,B: a,A: a] :
( ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ( B != A )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ( A != B )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) ),
inference(cnfConj,[status(thm)],[979]) ).
thf(991,plain,
! [C: a > $o,B: a,A: a] :
( ( B != A )
| ( A != B )
| ~ ( sk5
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) )
@ C )
| ( ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) )
!= ( ( C @ A )
| ( A = A )
| ( B = A ) ) )
| ~ ( sk4
@ ^ [D: a] :
( ( C @ D )
| ( A = D )
| ( B = D ) ) ) ),
inference(lifteq,[status(thm)],[982]) ).
thf(992,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C )
| ( A = C ) )
@ B )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C )
| ( A = C ) ) ) ),
inference(simp,[status(thm)],[991]) ).
thf(45,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [D: a] : ( cA @ ( C @ D ) )
@ A )
| ~ ( cA @ ( C @ B ) )
| ( sk5
@ ^ [D: a] : ( cA @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( cA @ ( C @ D ) ) ) ),
inference(prim_subst,[status(thm)],[16:[bind(A,$thf( ^ [E: a] : ( cA @ ( D @ E ) ) ))]]) ).
thf(64,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( sk1
| ~ ( sk5
@ ^ [D: a] : ( cA @ ( C @ D ) )
@ A )
| ~ ( cA @ ( C @ B ) )
| ( sk5
@ ^ [D: a] : ( cA @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( cA @ ( C @ D ) ) ) ),
inference(simp,[status(thm)],[45]) ).
thf(4238,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( $false
| ~ ( sk5
@ ^ [D: a] : ( cA @ ( C @ D ) )
@ A )
| ~ ( cA @ ( C @ B ) )
| ( sk5
@ ^ [D: a] : ( cA @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( cA @ ( C @ D ) ) ) ),
inference(rewrite,[status(thm)],[64,90]) ).
thf(4239,plain,
! [C: a > a > $o,B: a,A: a > $o] :
( ~ ( sk5
@ ^ [D: a] : ( cA @ ( C @ D ) )
@ A )
| ~ ( cA @ ( C @ B ) )
| ( sk5
@ ^ [D: a] : ( cA @ ( C @ D ) )
@ ^ [D: a] :
( ( A @ D )
| ( B = D ) ) )
| ~ ( sk4
@ ^ [D: a] : ( cA @ ( C @ D ) ) ) ),
inference(simp,[status(thm)],[4238]) ).
thf(121,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ( ( B @ A )
!= ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[110]) ).
thf(131,plain,
! [B: a > $o,A: a] :
( ~ ( sk5
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) )
@ B )
| ~ ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) )
| ( ( B @ A )
!= ( sk4
@ ^ [C: a] :
( ( B @ C )
| ( A = C ) ) ) ) ),
inference(simp,[status(thm)],[121]) ).
thf(4013,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk17 = A ) )
@ sk3 )
| ~ $true
| ( ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk17 = A ) ) )
!= ( sk4 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[3959,1540]) ).
thf(4014,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk17 = A ) )
@ sk3 )
| ( ( sk4
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk17 = A ) ) )
!= ( sk4 @ sk3 ) ) ),
inference(simp,[status(thm)],[4013]) ).
thf(4071,plain,
( ~ ( sk5
@ ^ [A: a] :
( ( sk3 @ A )
| ( sk17 = A ) )
@ sk3 )
| ( ( ^ [A: a] :
( ( sk3 @ A )
| ( sk17 = A ) ) )
!= sk3 ) ),
inference(simp,[status(thm)],[4014]) ).
thf(5047,plain,
! [A: a] :
( ( sk3
!= ( ^ [B: a] : $true ) )
| ~ $true
| ( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
!= ( sk5 @ sk3 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[4876,3995]) ).
thf(5048,plain,
! [A: a] :
( ( sk3
!= ( ^ [B: a] : $true ) )
| ( ( sk5
@ ^ [B: a] : $true
@ ( (=) @ a @ A ) )
!= ( sk5 @ sk3 @ sk3 ) ) ),
inference(simp,[status(thm)],[5047]) ).
thf(5115,plain,
! [A: a] :
( ( sk3
!= ( ^ [B: a] : $true ) )
| ( sk3
!= ( ^ [B: a] : $true ) )
| ( ( (=) @ a @ A )
!= sk3 ) ),
inference(simp,[status(thm)],[5048]) ).
thf(5155,plain,
! [A: a] :
( ( sk3
!= ( ^ [B: a] : $true ) )
| ( ( (=) @ a @ A )
!= sk3 ) ),
inference(simp,[status(thm)],[5115]) ).
thf(99,plain,
! [C: a,B: a > $o,A: a > $o] :
( $false
| ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ( sk5 @ A
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ~ ( sk4 @ A ) ),
inference(rewrite,[status(thm)],[16,90]) ).
thf(100,plain,
! [C: a,B: a > $o,A: a > $o] :
( ~ ( sk5 @ A @ B )
| ~ ( A @ C )
| ( sk5 @ A
@ ^ [D: a] :
( ( B @ D )
| ( C = D ) ) )
| ~ ( sk4 @ A ) ),
inference(simp,[status(thm)],[99]) ).
thf(25696,plain,
$false,
inference(e,[status(thm)],[4041,14567,15874,4447,16013,347,14912,12738,5168,12666,16184,3959,16156,13270,10715,6236,9064,7386,4439,4956,110,5640,6240,1087,4622,13365,4967,16344,3670,12750,4050,11163,13356,12670,6221,1521,8975,16155,3995,16356,102,3735,16183,11339,5611,16072,12764,13269,12450,7799,8446,15578,4048,169,141,16144,8451,1540,4049,11157,13883,5181,96,12449,8555,13366,3937,173,4237,134,13383,4613,1251,5483,11301,12451,2557,14502,391,13952,4060,5449,8452,1524,13888,5610,98,14581,3160,1080,13980,11156,11158,2664,108,130,13963,13944,2086,5646,241,14599,12779,278,226,3,13884,11316,1203,162,5025,16342,2333,6238,295,13367,4961,1098,5347,14507,175,11349,5364,12665,10767,3447,5510,104,15796,16161,12775,8292,14503,786,4451,2399,12448,15865,447,168,5356,239,1033,14563,1610,94,4923,5668,6329,16190,4876,4506,992,4239,131,4071,90,5155,13274,10768,100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU875^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.09/0.22 % Computer : n005.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Tue Sep 29 14:42:01 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.01/0.80 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.18/0.99 % [INFO] Parsing done (191ms).
% 1.18/1.01 % [INFO] Running in sequential loop mode.
% 1.94/1.40 % [INFO] eprover registered as external prover.
% 1.94/1.41 % [INFO] Scanning for conjecture ...
% 2.12/1.51 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.12/1.55 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.12/1.55 % [INFO] Problem is higher-order (TPTP THF).
% 2.12/1.56 % [INFO] Type checking passed.
% 2.12/1.57 % [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 ...
% 86.79/17.90 % External prover 'e' found a proof!
% 86.79/17.90 % [INFO] Killing All external provers ...
% 86.79/17.90 % Time passed: 17537ms (effective reasoning time: 16885ms)
% 86.79/17.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)>
% 86.79/17.90 % Axioms used in derivation (0):
% 86.79/17.90 % No. of inferences in proof: 609
% 86.79/17.90 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 17537 ms resp. 16885 ms w/o parsing
% 88.58/18.22 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 88.58/18.22 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------