%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEV245^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:37:03 AM UTC 2026
% Result : Theorem 152.06s 44.72s
% Output : Refutation 153.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 11
% Syntax : Number of formulae : 397 ( 41 unt; 0 typ; 10 def)
% Number of atoms : 2102 ( 326 equ; 9 cnn)
% Maximal formula atoms : 10 ( 5 avg)
% Number of connectives : 5478 ( 679 ~; 720 |; 120 &;3825 @)
% ( 0 <=>; 134 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 8 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 584 ( 584 >; 0 *; 0 +; 0 <<)
% Number of symbols : 20 ( 16 usr; 10 con; 0-2 aty)
% Number of variables : 1300 ( 458 ^; 727 !; 105 ?;1300 :)
% ( 0 !>; 0 ?*; 0 @-; 10 @+)
% Comments :
%------------------------------------------------------------------------------
thf(sk1_decl,type,
sk1: ( $i > $o ) > $i > $o ).
thf(sk2_decl,type,
sk2: ( $i > $o ) > ( $i > $o ) > $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i > $o ).
thf(sk5_decl,type,
sk5: $i ).
thf(sk7_decl,type,
sk7: ( $i > $o ) > $i ).
thf(sk8_decl,type,
sk8: ( $i > $o ) > $i ).
thf(sk9_decl,type,
sk9: $i > $o ).
thf(sk10_decl,type,
sk10: ( $i > $o ) > ( $i > $o ) > $i ).
thf(sk17_decl,type,
sk17: $i ).
thf(sk32_decl,type,
sk32: $i > $o ).
thf(sk33_decl,type,
sk33: $i ).
thf(sk38_decl,type,
sk38: $i ).
thf(sk39_decl,type,
sk39: $i ).
thf(sk88_decl,type,
sk88: $i > $o ).
thf(sk109_decl,type,
sk109: $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: ( $i > $o ) > $i > $o] :
~ ( ! [B: $i > $o,C: $i > $o] :
( ! [D: $i] :
( ( B @ D )
=> ( C @ D ) )
=> ! [D: $i] :
( ( A @ B @ D )
=> ( A @ C @ D ) ) )
=> ! [B: $i] :
( ? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( A @ C @ D ) )
& ( C @ B ) )
=> ( A
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( A @ D @ E ) )
& ( D @ C ) )
@ B ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: $i > $o,B: $i > $o] :
@+[C: $i] :
~ ( ( B @ C )
=> ( A @ C ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
=> ( sk1
@ ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) )
@ A ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i > $o] :
( ! [B: $i] :
( ( A @ B )
=> ( sk1 @ A @ B ) )
& ( A @ sk3 ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: $i > $o] :
@+[B: $i] :
~ ( ( A @ B )
=> ( sk1 @ A @ B ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: $i > $o] :
@+[B: $i] :
~ ( ( A @ B )
=> ( sk1 @ A @ B ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( @+[A: $i > $o] :
( ! [B: $i] :
( ( A @ B )
=> ( sk1 @ A @ B ) )
& ( A @ sk5 ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: $i > $o,B: $i > $o] :
@+[C: $i] :
~ ( ( A @ C )
=> ( sk1 @ A @ C ) ) ) ) ).
thf(sk32_def,definition,
( sk32
= ( @+[A: $i > $o] :
( ! [B: $i] :
( ( A @ B )
=> ( sk1 @ A @ B ) )
& ( A @ sk5 ) ) ) ) ).
thf(sk88_def,definition,
( sk88
= ( @+[A: $i > $o] :
( ! [B: $i] :
( ( A @ B )
=> ( sk1 @ A @ B ) )
& ( A @ sk39 ) ) ) ) ).
thf(1,conjecture,
! [A: ( $i > $o ) > $i > $o] :
( ! [B: $i > $o,C: $i > $o] :
( ! [D: $i] :
( ( B @ D )
=> ( C @ D ) )
=> ! [D: $i] :
( ( A @ B @ D )
=> ( A @ C @ D ) ) )
=> ! [B: $i] :
( ? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( A @ C @ D ) )
& ( C @ B ) )
=> ( A
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( A @ D @ E ) )
& ( D @ C ) )
@ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM2A_TWO_pme) ).
thf(2,negated_conjecture,
~ ! [A: ( $i > $o ) > $i > $o] :
( ! [B: $i > $o,C: $i > $o] :
( ! [D: $i] :
( ( B @ D )
=> ( C @ D ) )
=> ! [D: $i] :
( ( A @ B @ D )
=> ( A @ C @ D ) ) )
=> ! [B: $i] :
( ? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( A @ C @ D ) )
& ( C @ B ) )
=> ( A
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( A @ D @ E ) )
& ( D @ C ) )
@ B ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ! [A: ( $i > $o ) > $i > $o] :
( ! [B: $i > $o,C: $i > $o] :
( ! [D: $i] :
( ( B @ D )
=> ( C @ D ) )
=> ! [D: $i] :
( ( A @ B @ D )
=> ( A @ C @ D ) ) )
=> ! [B: $i] :
( ? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( A @ C @ D ) )
& ( C @ B ) )
=> ( A
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( A @ D @ E ) )
& ( D @ C ) )
@ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
! [D: $i,C: $i,B: $i > $o,A: $i > $o] :
( ( ( A @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ( sk1 @ B @ C ) )
& ( ~ ( B @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ( sk1 @ B @ C ) )
& ( ~ ( sk4 @ D )
| ( sk1 @ sk4 @ D ) )
& ( sk4 @ sk3 )
& ~ ( sk1
@ ^ [E: $i] :
? [F: $i > $o] :
( ! [G: $i] :
( ( F @ G )
=> ( sk1 @ F @ G ) )
& ( F @ E ) )
@ sk3 ) ),
inference(cnf,[status(esa)],[3]) ).
thf(7,plain,
sk4 @ sk3,
inference(cnfConj,[status(thm)],[4]) ).
thf(5,plain,
! [A: $i] :
( ~ ( sk4 @ A )
| ( sk1 @ sk4 @ A ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(10,plain,
! [A: $i] :
( ~ ( sk4 @ A )
| ( sk1 @ sk4 @ A ) ),
inference(simp,[status(thm)],[5]) ).
thf(13,plain,
! [A: $i] :
( ~ $true
| ( sk1 @ sk4 @ A )
| ( ( sk4 @ sk3 )
!= ( sk4 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[7,10]) ).
thf(14,plain,
! [A: $i] :
( ( sk1 @ sk4 @ A )
| ( ( sk4 @ sk3 )
!= ( sk4 @ A ) ) ),
inference(simp,[status(thm)],[13]) ).
thf(15,plain,
sk1 @ sk4 @ sk3,
inference(pattern_uni,[status(thm)],[14:[bind(A,$thf( sk3 ))]]) ).
thf(6,plain,
~ ( sk1
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk3 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(18,plain,
( ~ $true
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[15,6]) ).
thf(19,plain,
( ( sk1 @ sk4 @ sk3 )
!= ( sk1
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk3 ) ),
inference(simp,[status(thm)],[18]) ).
thf(20,plain,
( ( sk4
!= ( ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) ) ) )
| ( sk3 != sk3 ) ),
inference(simp,[status(thm)],[19]) ).
thf(21,plain,
( sk4
!= ( ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) ) ) ),
inference(simp,[status(thm)],[20]) ).
thf(22,plain,
( ( sk4 @ sk5 )
!= ( ? [A: $i > $o] :
( ! [B: $i] :
( ( A @ B )
=> ( sk1 @ A @ B ) )
& ( A @ sk5 ) ) ) ),
inference(func_ext,[status(esa)],[21]) ).
thf(63,plain,
( ( sk4 @ sk5 )
| ? [A: $i > $o] :
( ! [B: $i] :
( ( A @ B )
=> ( sk1 @ A @ B ) )
& ( A @ sk5 ) ) ),
inference(bool_ext,[status(thm)],[22]) ).
thf(80,plain,
! [A: $i] :
( ( ( sk4 @ sk5 )
| ~ ( sk9 @ A )
| ( sk1 @ sk9 @ A ) )
& ( ( sk4 @ sk5 )
| ( sk9 @ sk5 ) ) ),
inference(cnf,[status(esa)],[63]) ).
thf(82,plain,
( ( sk4 @ sk5 )
| ( sk9 @ sk5 ) ),
inference(cnfConj,[status(thm)],[80]) ).
thf(62,plain,
( ~ ( sk4 @ sk5 )
| ~ ? [A: $i > $o] :
( ! [B: $i] :
( ( A @ B )
=> ( sk1 @ A @ B ) )
& ( A @ sk5 ) ) ),
inference(bool_ext,[status(thm)],[22]) ).
thf(77,plain,
! [A: $i > $o] :
( ( ~ ( sk4 @ sk5 )
| ( A @ ( sk8 @ A ) )
| ~ ( A @ sk5 ) )
& ( ~ ( sk4 @ sk5 )
| ~ ( sk1 @ A @ ( sk8 @ A ) )
| ~ ( A @ sk5 ) ) ),
inference(cnf,[status(esa)],[62]) ).
thf(78,plain,
! [A: $i > $o] :
( ~ ( sk4 @ sk5 )
| ( A @ ( sk8 @ A ) )
| ~ ( A @ sk5 ) ),
inference(cnfConj,[status(thm)],[77]) ).
thf(79,plain,
! [A: $i > $o] :
( ~ ( sk4 @ sk5 )
| ~ ( sk1 @ A @ ( sk8 @ A ) )
| ~ ( A @ sk5 ) ),
inference(cnfConj,[status(thm)],[77]) ).
thf(6808,plain,
! [B: $i > $o,A: $i] :
( ~ ( sk4 @ A )
| ~ ( sk4 @ sk5 )
| ~ $true
| ~ ( B @ sk5 )
| ( ( sk1 @ sk4 @ A )
!= ( sk1 @ B @ ( sk8 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[10,79]) ).
thf(6809,plain,
! [B: $i > $o,A: $i] :
( ~ ( sk4 @ A )
| ~ ( sk4 @ sk5 )
| ~ ( B @ sk5 )
| ( ( sk1 @ sk4 @ A )
!= ( sk1 @ B @ ( sk8 @ B ) ) ) ),
inference(simp,[status(thm)],[6808]) ).
thf(6810,plain,
( ~ ( sk4 @ ( sk8 @ sk4 ) )
| ~ ( sk4 @ sk5 )
| ~ ( sk4 @ sk5 ) ),
inference(pattern_uni,[status(thm)],[6809:[bind(A,$thf( sk8 @ sk4 )),bind(B,$thf( sk4 ))]]) ).
thf(7178,plain,
( ~ ( sk4 @ ( sk8 @ sk4 ) )
| ~ ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[6810]) ).
thf(7265,plain,
! [A: $i > $o] :
( ~ ( sk4 @ sk5 )
| ~ ( A @ sk5 )
| ~ $true
| ~ ( sk4 @ sk5 )
| ( ( A @ ( sk8 @ A ) )
!= ( sk4 @ ( sk8 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[78,7178]) ).
thf(7266,plain,
! [A: $i > $o] :
( ~ ( sk4 @ sk5 )
| ~ ( A @ sk5 )
| ( ( A @ ( sk8 @ A ) )
!= ( sk4 @ ( sk8 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[7265]) ).
thf(7323,plain,
( ~ ( sk4 @ sk5 )
| ~ ( sk4 @ sk5 ) ),
inference(pre_uni,[status(thm)],[7266:[bind(A,$thf( sk4 ))]]) ).
thf(7343,plain,
~ ( sk4 @ sk5 ),
inference(simp,[status(thm)],[7323]) ).
thf(7348,plain,
( $false
| ( sk9 @ sk5 ) ),
inference(rewrite,[status(thm)],[82,7343]) ).
thf(7349,plain,
sk9 @ sk5,
inference(simp,[status(thm)],[7348]) ).
thf(81,plain,
! [A: $i] :
( ( sk4 @ sk5 )
| ~ ( sk9 @ A )
| ( sk1 @ sk9 @ A ) ),
inference(cnfConj,[status(thm)],[80]) ).
thf(7441,plain,
! [A: $i] :
( $false
| ~ ( sk9 @ A )
| ( sk1 @ sk9 @ A ) ),
inference(rewrite,[status(thm)],[81,7343]) ).
thf(7442,plain,
! [A: $i] :
( ~ ( sk9 @ A )
| ( sk1 @ sk9 @ A ) ),
inference(simp,[status(thm)],[7441]) ).
thf(7466,plain,
! [A: $i] :
( ~ $true
| ( sk1 @ sk9 @ A )
| ( ( sk9 @ sk5 )
!= ( sk9 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[7349,7442]) ).
thf(7467,plain,
! [A: $i] :
( ( sk1 @ sk9 @ A )
| ( ( sk9 @ sk5 )
!= ( sk9 @ A ) ) ),
inference(simp,[status(thm)],[7466]) ).
thf(7468,plain,
sk1 @ sk9 @ sk5,
inference(pattern_uni,[status(thm)],[7467:[bind(A,$thf( sk5 ))]]) ).
thf(8,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ( sk1 @ B @ C ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(7544,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ $true
| ( sk1 @ B @ C )
| ( ( sk1 @ sk9 @ sk5 )
!= ( sk1 @ A @ C ) ) ),
inference(paramod_ordered,[status(thm)],[7468,8]) ).
thf(7545,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ( sk1 @ B @ C )
| ( ( sk1 @ sk9 @ sk5 )
!= ( sk1 @ A @ C ) ) ),
inference(simp,[status(thm)],[7544]) ).
thf(7546,plain,
! [A: $i > $o] :
( ( sk9 @ ( sk2 @ A @ sk9 ) )
| ( sk1 @ A @ sk5 ) ),
inference(pattern_uni,[status(thm)],[7545:[bind(A,$thf( sk9 )),bind(B,$thf( B )),bind(C,$thf( sk5 ))]]) ).
thf(7569,plain,
! [A: $i > $o] :
( ( sk9 @ ( sk2 @ A @ sk9 ) )
| ( sk1 @ A @ sk5 ) ),
inference(simp,[status(thm)],[7546]) ).
thf(39,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ $true
| ( sk1 @ B @ C )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ A @ C ) ) ),
inference(paramod_ordered,[status(thm)],[15,8]) ).
thf(40,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ( sk1 @ B @ C )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ A @ C ) ) ),
inference(simp,[status(thm)],[39]) ).
thf(41,plain,
! [A: $i > $o] :
( ( sk4 @ ( sk2 @ A @ sk4 ) )
| ( sk1 @ A @ sk3 ) ),
inference(pattern_uni,[status(thm)],[40:[bind(A,$thf( sk4 )),bind(B,$thf( B )),bind(C,$thf( sk3 ))]]) ).
thf(55,plain,
! [A: $i > $o] :
( ( sk4 @ ( sk2 @ A @ sk4 ) )
| ( sk1 @ A @ sk3 ) ),
inference(simp,[status(thm)],[41]) ).
thf(44,plain,
! [B: $i,A: $i > $o] :
( $false
| ~ ( sk1
@ ^ [C: $i] : $false
@ B )
| ( sk1 @ A @ B ) ),
inference(prim_subst,[status(thm)],[8:[bind(A,$thf( ^ [D: $i] : $false ))]]) ).
thf(58,plain,
! [B: $i,A: $i > $o] :
( ~ ( sk1
@ ^ [C: $i] : $false
@ B )
| ( sk1 @ A @ B ) ),
inference(simp,[status(thm)],[44]) ).
thf(1520,plain,
! [B: $i,A: $i > $o] :
( ~ ( sk1
@ ^ [C: $i] : $false
@ B )
| ~ $true
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[58,6]) ).
thf(1521,plain,
! [B: $i,A: $i > $o] :
( ~ ( sk1
@ ^ [C: $i] : $false
@ B )
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ sk3 ) ) ),
inference(simp,[status(thm)],[1520]) ).
thf(1522,plain,
~ ( sk1
@ ^ [A: $i] : $false
@ sk3 ),
inference(pattern_uni,[status(thm)],[1521:[bind(A,$thf( ^ [C: $i] : ? [D: $i > $o] : ( ! [E: $i] : ( ( D @ E ) => ( sk1 @ D @ E ) ) & ( D @ C ) ) )),bind(B,$thf( sk3 ))]]) ).
thf(1654,plain,
! [A: $i > $o] :
( ( sk4 @ ( sk2 @ A @ sk4 ) )
| ~ $true
| ( ( sk1 @ A @ sk3 )
!= ( sk1
@ ^ [B: $i] : $false
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[55,1522]) ).
thf(1655,plain,
! [A: $i > $o] :
( ( sk4 @ ( sk2 @ A @ sk4 ) )
| ( ( sk1 @ A @ sk3 )
!= ( sk1
@ ^ [B: $i] : $false
@ sk3 ) ) ),
inference(simp,[status(thm)],[1654]) ).
thf(1656,plain,
( sk4
@ ( sk2
@ ^ [A: $i] : $false
@ sk4 ) ),
inference(pattern_uni,[status(thm)],[1655:[bind(A,$thf( ^ [B: $i] : $false ))]]) ).
thf(160,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A @ sk3 )
| ~ $true
| ( sk1 @ sk4 @ B )
| ( ( sk4 @ ( sk2 @ A @ sk4 ) )
!= ( sk4 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[55,10]) ).
thf(161,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A @ sk3 )
| ( sk1 @ sk4 @ B )
| ( ( sk4 @ ( sk2 @ A @ sk4 ) )
!= ( sk4 @ B ) ) ),
inference(simp,[status(thm)],[160]) ).
thf(162,plain,
! [A: $i > $o] :
( ( sk1 @ A @ sk3 )
| ( sk1 @ sk4 @ ( sk2 @ A @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[161:[bind(A,$thf( C )),bind(B,$thf( sk2 @ C @ sk4 ))]]) ).
thf(183,plain,
! [A: $i > $o] :
( ( sk1 @ A @ sk3 )
| ( sk1 @ sk4 @ ( sk2 @ A @ sk4 ) ) ),
inference(simp,[status(thm)],[162]) ).
thf(9,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( B @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ( sk1 @ B @ C ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(100,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( B @ ( sk2 @ B @ A ) )
| ~ $true
| ( sk1 @ B @ C )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ A @ C ) ) ),
inference(paramod_ordered,[status(thm)],[15,9]) ).
thf(101,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( B @ ( sk2 @ B @ A ) )
| ( sk1 @ B @ C )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ A @ C ) ) ),
inference(simp,[status(thm)],[100]) ).
thf(102,plain,
! [A: $i > $o] :
( ~ ( A @ ( sk2 @ A @ sk4 ) )
| ( sk1 @ A @ sk3 ) ),
inference(pattern_uni,[status(thm)],[101:[bind(A,$thf( sk4 )),bind(B,$thf( B )),bind(C,$thf( sk3 ))]]) ).
thf(140,plain,
! [A: $i > $o] :
( ~ ( A @ ( sk2 @ A @ sk4 ) )
| ( sk1 @ A @ sk3 ) ),
inference(simp,[status(thm)],[102]) ).
thf(11114,plain,
! [B: $i > $o,A: $i > $o] :
( ( sk1 @ A @ sk3 )
| ~ $true
| ( sk1 @ B @ sk3 )
| ( ( sk1 @ sk4 @ ( sk2 @ A @ sk4 ) )
!= ( B @ ( sk2 @ B @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[183,140]) ).
thf(11115,plain,
! [B: $i > $o,A: $i > $o] :
( ( sk1 @ A @ sk3 )
| ( sk1 @ B @ sk3 )
| ( ( sk1 @ sk4 @ ( sk2 @ A @ sk4 ) )
!= ( B @ ( sk2 @ B @ sk4 ) ) ) ),
inference(simp,[status(thm)],[11114]) ).
thf(11131,plain,
( ( sk1 @ ( sk1 @ sk4 ) @ sk3 )
| ( sk1 @ ( sk1 @ sk4 ) @ sk3 ) ),
inference(pre_uni,[status(thm)],[11115:[bind(A,$thf( sk1 @ sk4 )),bind(B,$thf( sk1 @ sk4 ))]]) ).
thf(11266,plain,
sk1 @ ( sk1 @ sk4 ) @ sk3,
inference(simp,[status(thm)],[11131]) ).
thf(11292,plain,
( ~ $true
| ( ( sk1 @ ( sk1 @ sk4 ) @ sk3 )
!= ( sk1
@ ^ [A: $i] : $false
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[11266,1522]) ).
thf(11293,plain,
( ( sk1 @ ( sk1 @ sk4 ) @ sk3 )
!= ( sk1
@ ^ [A: $i] : $false
@ sk3 ) ),
inference(simp,[status(thm)],[11292]) ).
thf(11338,plain,
( ( ( sk1 @ sk4 )
!= ( ^ [A: $i] : $false ) )
| ( sk3 != sk3 ) ),
inference(simp,[status(thm)],[11293]) ).
thf(11350,plain,
( ( sk1 @ sk4 )
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[11338]) ).
thf(11360,plain,
sk1 @ sk4 @ sk38,
inference(func_ext,[status(esa)],[11350]) ).
thf(118,plain,
! [C: $i > $o,B: $i,A: $i > $o] :
( ~ ~ ( C
@ ( sk2
@ ^ [D: $i] :
~ ( C @ D )
@ A ) )
| ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [D: $i] :
~ ( C @ D )
@ B ) ),
inference(prim_subst,[status(thm)],[9:[bind(A,$thf( A )),bind(B,$thf( ^ [E: $i] : ~ ( D @ E ) ))]]) ).
thf(144,plain,
! [C: $i > $o,B: $i,A: $i > $o] :
( ( C
@ ( sk2
@ ^ [D: $i] :
~ ( C @ D )
@ A ) )
| ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [D: $i] :
~ ( C @ D )
@ B ) ),
inference(cnf,[status(esa)],[118]) ).
thf(145,plain,
! [C: $i > $o,B: $i,A: $i > $o] :
( ( C
@ ( sk2
@ ^ [D: $i] :
~ ( C @ D )
@ A ) )
| ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [D: $i] :
~ ( C @ D )
@ B ) ),
inference(simp,[status(thm)],[144]) ).
thf(106,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A @ C )
| ( sk1 @ B @ C )
| ~ $true
| ~ ( sk1 @ D @ F )
| ( sk1 @ E @ F )
| ( ( A @ ( sk2 @ B @ A ) )
!= ( E @ ( sk2 @ E @ D ) ) ) ),
inference(paramod_ordered,[status(thm)],[8,9]) ).
thf(107,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A @ C )
| ( sk1 @ B @ C )
| ~ ( sk1 @ D @ F )
| ( sk1 @ E @ F )
| ( ( A @ ( sk2 @ B @ A ) )
!= ( E @ ( sk2 @ E @ D ) ) ) ),
inference(simp,[status(thm)],[106]) ).
thf(126,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A @ C )
| ( sk1 @ B @ C )
| ~ ( sk1 @ D @ F )
| ( sk1 @ E @ F )
| ( ( A @ ( sk2 @ B @ A ) )
!= ( E @ ( sk2 @ E @ D ) ) ) ),
inference(pre_uni,[status(thm)],[107:[]]) ).
thf(127,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ( sk1 @ E @ F )
| ~ ( sk1 @ D @ F )
| ( sk1 @ B @ C )
| ~ ( sk1 @ A @ C )
| ( ( A @ ( sk2 @ B @ A ) )
!= ( E @ ( sk2 @ E @ D ) ) ) ),
inference(pre_uni,[status(thm)],[126:[]]) ).
thf(11301,plain,
( ~ $true
| ( ( sk1 @ ( sk1 @ sk4 ) @ sk3 )
!= ( sk1
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[11266,6]) ).
thf(11302,plain,
( ( sk1 @ ( sk1 @ sk4 ) @ sk3 )
!= ( sk1
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk3 ) ),
inference(simp,[status(thm)],[11301]) ).
thf(11341,plain,
( ( ( sk1 @ sk4 )
!= ( ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) ) ) )
| ( sk3 != sk3 ) ),
inference(simp,[status(thm)],[11302]) ).
thf(11353,plain,
( ( sk1 @ sk4 )
!= ( ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) ) ) ),
inference(simp,[status(thm)],[11341]) ).
thf(1791,plain,
! [A: $i] :
( ~ $true
| ( sk1 @ sk4 @ A )
| ( ( sk4
@ ( sk2
@ ^ [B: $i] : $false
@ sk4 ) )
!= ( sk4 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1656,10]) ).
thf(1792,plain,
! [A: $i] :
( ( sk1 @ sk4 @ A )
| ( ( sk4
@ ( sk2
@ ^ [B: $i] : $false
@ sk4 ) )
!= ( sk4 @ A ) ) ),
inference(simp,[status(thm)],[1791]) ).
thf(1793,plain,
( sk1 @ sk4
@ ( sk2
@ ^ [A: $i] : $false
@ sk4 ) ),
inference(pattern_uni,[status(thm)],[1792:[bind(A,$thf( sk2 @ ^ [B: $i] : $false @ sk4 ))]]) ).
thf(7347,plain,
? [A: $i > $o] :
( ! [B: $i] :
( ( A @ B )
=> ( sk1 @ A @ B ) )
& ( A @ sk5 ) ),
inference(rewrite,[status(thm)],[22,7343]) ).
thf(7403,plain,
! [A: $i] :
( ( ~ ( sk32 @ A )
| ( sk1 @ sk32 @ A ) )
& ( sk32 @ sk5 ) ),
inference(cnf,[status(esa)],[7347]) ).
thf(7404,plain,
! [A: $i] :
( ~ ( sk32 @ A )
| ( sk1 @ sk32 @ A ) ),
inference(cnfConj,[status(thm)],[7403]) ).
thf(16327,plain,
! [A: $i] :
( ~ ( sk32 @ A )
| ~ $true
| ( ( sk1 @ sk32 @ A )
!= ( sk1
@ ^ [B: $i] : $false
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[7404,1522]) ).
thf(16328,plain,
! [A: $i] :
( ~ ( sk32 @ A )
| ( ( sk1 @ sk32 @ A )
!= ( sk1
@ ^ [B: $i] : $false
@ sk3 ) ) ),
inference(simp,[status(thm)],[16327]) ).
thf(16403,plain,
! [A: $i] :
( ~ ( sk32 @ A )
| ( sk32
!= ( ^ [B: $i] : $false ) )
| ( A != sk3 ) ),
inference(simp,[status(thm)],[16328]) ).
thf(16437,plain,
( ~ ( sk32 @ sk3 )
| ( sk32
!= ( ^ [A: $i] : $false ) ) ),
inference(simp,[status(thm)],[16403]) ).
thf(7460,plain,
! [A: $i] :
( ~ ( sk9 @ A )
| ~ $true
| ( ( sk1 @ sk9 @ A )
!= ( sk1
@ ^ [B: $i] : $false
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[7442,1522]) ).
thf(7461,plain,
! [A: $i] :
( ~ ( sk9 @ A )
| ( ( sk1 @ sk9 @ A )
!= ( sk1
@ ^ [B: $i] : $false
@ sk3 ) ) ),
inference(simp,[status(thm)],[7460]) ).
thf(7494,plain,
! [A: $i] :
( ~ ( sk9 @ A )
| ( sk9
!= ( ^ [B: $i] : $false ) )
| ( A != sk3 ) ),
inference(simp,[status(thm)],[7461]) ).
thf(7509,plain,
( ~ ( sk9 @ sk3 )
| ( sk9
!= ( ^ [A: $i] : $false ) ) ),
inference(simp,[status(thm)],[7494]) ).
thf(7570,plain,
( ( sk9 @ sk33 )
| ~ ( sk9 @ sk3 ) ),
inference(func_ext,[status(esa)],[7509]) ).
thf(7680,plain,
! [A: $i] :
( ~ ( sk9 @ sk3 )
| ~ $true
| ( sk1 @ sk9 @ A )
| ( ( sk9 @ sk33 )
!= ( sk9 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[7570,7442]) ).
thf(7681,plain,
! [A: $i] :
( ~ ( sk9 @ sk3 )
| ( sk1 @ sk9 @ A )
| ( ( sk9 @ sk33 )
!= ( sk9 @ A ) ) ),
inference(simp,[status(thm)],[7680]) ).
thf(7682,plain,
( ~ ( sk9 @ sk3 )
| ( sk1 @ sk9 @ sk33 ) ),
inference(pattern_uni,[status(thm)],[7681:[bind(A,$thf( sk33 ))]]) ).
thf(96,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ $true
| ~ ( sk1 @ A @ C )
| ( sk1 @ B @ C )
| ( ( B @ ( sk2 @ B @ A ) )
!= ( sk4 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[7,9]) ).
thf(97,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A @ C )
| ( sk1 @ B @ C )
| ( ( B @ ( sk2 @ B @ A ) )
!= ( sk4 @ sk3 ) ) ),
inference(simp,[status(thm)],[96]) ).
thf(132,plain,
! [B: $i,A: $i > $o] :
( ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [C: $i] : ( sk4 @ sk3 )
@ B ) ),
inference(pre_uni,[status(thm)],[97:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : ( sk4 @ sk3 ) )),bind(C,$thf( C ))]]) ).
thf(138,plain,
! [B: $i,A: $i > $o] :
( ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [C: $i] : ( sk4 @ sk3 )
@ B ) ),
inference(simp,[status(thm)],[132]) ).
thf(10468,plain,
! [B: $i,A: $i > $o] :
( ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [C: $i] : $true
@ B ) ),
inference(rewrite,[status(thm)],[138,7]) ).
thf(10593,plain,
! [B: $i,A: $i > $o] :
( ~ ( sk9 @ sk3 )
| ~ $true
| ( sk1
@ ^ [C: $i] : $true
@ B )
| ( ( sk1 @ sk9 @ sk33 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[7682,10468]) ).
thf(10594,plain,
! [B: $i,A: $i > $o] :
( ~ ( sk9 @ sk3 )
| ( sk1
@ ^ [C: $i] : $true
@ B )
| ( ( sk1 @ sk9 @ sk33 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[10593]) ).
thf(10595,plain,
( ~ ( sk9 @ sk3 )
| ( sk1
@ ^ [A: $i] : $true
@ sk33 ) ),
inference(pattern_uni,[status(thm)],[10594:[bind(A,$thf( sk9 )),bind(B,$thf( sk33 ))]]) ).
thf(117,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( B @ ( sk2 @ B @ A ) )
| ( sk1 @ B @ C )
| ( ( sk1 @ A @ C )
!= ( B @ ( sk2 @ B @ A ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[9]) ).
thf(129,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ~ ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ),
inference(pre_uni,[status(thm)],[117:[bind(A,$thf( A )),bind(B,$thf( ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) ) )),bind(C,$thf( E @ ( sk2 @ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) ) @ A ) ))]]) ).
thf(130,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ~ ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ),
inference(pre_uni,[status(thm)],[129:[]]) ).
thf(136,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ~ ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ),
inference(simp,[status(thm)],[130]) ).
thf(10862,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ~ ( sk9 @ sk3 )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ~ $true
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
!= ( sk1
@ ^ [D: $i] : $true
@ sk33 ) ) ),
inference(paramod_ordered,[status(thm)],[10595,136]) ).
thf(10863,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ~ ( sk9 @ sk3 )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
!= ( sk1
@ ^ [D: $i] : $true
@ sk33 ) ) ),
inference(simp,[status(thm)],[10862]) ).
thf(10926,plain,
! [A: $i > $o] :
( ~ ( sk9 @ sk3 )
| ( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : $true
@ sk33 )
@ sk33 )
| ( A
!= ( ^ [B: $i] : $true ) ) ),
inference(pre_uni,[status(thm)],[10863:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : ^ [E: $i] : $true )),bind(C,$thf( ^ [D: $i] : sk33 ))]]) ).
thf(10927,plain,
( ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : $true
@ sk33 )
@ sk33 )
| ~ ( sk9 @ sk3 ) ),
inference(pattern_uni,[status(thm)],[10926:[bind(A,$thf( ^ [B: $i] : $true ))]]) ).
thf(7405,plain,
sk32 @ sk5,
inference(cnfConj,[status(thm)],[7403]) ).
thf(103,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( B @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ( D @ ( sk2 @ E @ D ) )
| ~ $true
| ( sk1 @ E @ F )
| ( ( sk1 @ B @ C )
!= ( sk1 @ D @ F ) ) ),
inference(paramod_ordered,[status(thm)],[9,8]) ).
thf(104,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( B @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ( D @ ( sk2 @ E @ D ) )
| ( sk1 @ E @ F )
| ( ( sk1 @ B @ C )
!= ( sk1 @ D @ F ) ) ),
inference(simp,[status(thm)],[103]) ).
thf(105,plain,
! [D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( B @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ( B @ ( sk2 @ D @ B ) )
| ( sk1 @ D @ C ) ),
inference(pattern_uni,[status(thm)],[104:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( B )),bind(E,$thf( E )),bind(F,$thf( C ))]]) ).
thf(142,plain,
! [D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( B @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ( B @ ( sk2 @ D @ B ) )
| ( sk1 @ D @ C ) ),
inference(simp,[status(thm)],[105]) ).
thf(12341,plain,
( ( sk1 @ sk4 @ sk39 )
!= ( ? [A: $i > $o] :
( ! [B: $i] :
( ( A @ B )
=> ( sk1 @ A @ B ) )
& ( A @ sk39 ) ) ) ),
inference(func_ext,[status(esa)],[11353]) ).
thf(15305,plain,
( ( sk1 @ sk4 @ sk39 )
| ? [A: $i > $o] :
( ! [B: $i] :
( ( A @ B )
=> ( sk1 @ A @ B ) )
& ( A @ sk39 ) ) ),
inference(bool_ext,[status(thm)],[12341]) ).
thf(15644,plain,
! [A: $i] :
( ( ( sk1 @ sk4 @ sk39 )
| ~ ( sk88 @ A )
| ( sk1 @ sk88 @ A ) )
& ( ( sk1 @ sk4 @ sk39 )
| ( sk88 @ sk39 ) ) ),
inference(cnf,[status(esa)],[15305]) ).
thf(15646,plain,
( ( sk1 @ sk4 @ sk39 )
| ( sk88 @ sk39 ) ),
inference(cnfConj,[status(thm)],[15644]) ).
thf(15766,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk88 @ sk39 )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ~ $true
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1 @ sk4 @ sk39 )
!= ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[15646,136]) ).
thf(15767,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk88 @ sk39 )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1 @ sk4 @ sk39 )
!= ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ) ),
inference(simp,[status(thm)],[15766]) ).
thf(15775,plain,
! [A: $i > $o] :
( ( sk88 @ sk39 )
| ( sk1
@ ^ [B: $i] : ( sk1 @ sk4 @ sk39 )
@ sk39 )
| ( A != sk4 ) ),
inference(pre_uni,[status(thm)],[15767:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : sk4 )),bind(C,$thf( ^ [D: $i] : sk39 ))]]) ).
thf(15776,plain,
( ( sk1
@ ^ [A: $i] : ( sk1 @ sk4 @ sk39 )
@ sk39 )
| ( sk88 @ sk39 ) ),
inference(pattern_uni,[status(thm)],[15775:[bind(A,$thf( sk4 ))]]) ).
thf(8931,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ~ $true
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[15,136]) ).
thf(8932,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ) ),
inference(simp,[status(thm)],[8931]) ).
thf(9105,plain,
! [A: $i > $o] :
( ( sk1
@ ^ [B: $i] : ( sk1 @ sk4 @ sk3 )
@ sk3 )
| ( A != sk4 ) ),
inference(pre_uni,[status(thm)],[8932:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : sk4 )),bind(C,$thf( ^ [D: $i] : sk3 ))]]) ).
thf(9106,plain,
( sk1
@ ^ [A: $i] : ( sk1 @ sk4 @ sk3 )
@ sk3 ),
inference(pattern_uni,[status(thm)],[9105:[bind(A,$thf( sk4 ))]]) ).
thf(9279,plain,
( sk1
@ ^ [A: $i] : $true
@ sk3 ),
inference(rewrite,[status(thm)],[9106,15]) ).
thf(88,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( B @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ~ $true
| ( ( sk1 @ B @ C )
!= ( sk1
@ ^ [D: $i] :
? [E: $i > $o] :
( ! [F: $i] :
( ( E @ F )
=> ( sk1 @ E @ F ) )
& ( E @ D ) )
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[9,6]) ).
thf(89,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ~ ( B @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ( ( sk1 @ B @ C )
!= ( sk1
@ ^ [D: $i] :
? [E: $i > $o] :
( ! [F: $i] :
( ( E @ F )
=> ( sk1 @ E @ F ) )
& ( E @ D ) )
@ sk3 ) ) ),
inference(simp,[status(thm)],[88]) ).
thf(90,plain,
! [A: $i > $o] :
( ~ ? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ A ) ) )
| ~ ( sk1 @ A @ sk3 ) ),
inference(pattern_uni,[status(thm)],[89:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : ? [E: $i > $o] : ( ! [F: $i] : ( ( E @ F ) => ( sk1 @ E @ F ) ) & ( E @ D ) ) )),bind(C,$thf( sk3 ))]]) ).
thf(153,plain,
! [B: $i > $o,A: $i > $o] :
( ( ( B @ ( sk10 @ B @ A ) )
| ~ ( B
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ A ) )
| ~ ( sk1 @ A @ sk3 ) )
& ( ~ ( sk1 @ B @ ( sk10 @ B @ A ) )
| ~ ( B
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ A ) )
| ~ ( sk1 @ A @ sk3 ) ) ),
inference(cnf,[status(esa)],[90]) ).
thf(154,plain,
! [B: $i > $o,A: $i > $o] :
( ( B @ ( sk10 @ B @ A ) )
| ~ ( B
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ A ) )
| ~ ( sk1 @ A @ sk3 ) ),
inference(cnfConj,[status(thm)],[153]) ).
thf(21494,plain,
! [B: $i > $o,A: $i > $o] :
( ( B @ ( sk10 @ B @ A ) )
| ~ ( B
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ A ) )
| ~ $true
| ( ( sk1
@ ^ [C: $i] : $true
@ sk3 )
!= ( sk1 @ A @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[9279,154]) ).
thf(21495,plain,
! [B: $i > $o,A: $i > $o] :
( ( B @ ( sk10 @ B @ A ) )
| ~ ( B
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ A ) )
| ( ( sk1
@ ^ [C: $i] : $true
@ sk3 )
!= ( sk1 @ A @ sk3 ) ) ),
inference(simp,[status(thm)],[21494]) ).
thf(21496,plain,
! [A: $i > $o] :
( ( A
@ ( sk10 @ A
@ ^ [B: $i] : $true ) )
| ~ ( A
@ ( sk2
@ ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) )
@ ^ [B: $i] : $true ) ) ),
inference(pattern_uni,[status(thm)],[21495:[bind(A,$thf( ^ [C: $i] : $true ))]]) ).
thf(21695,plain,
( ( ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ^ [A: $i] : $true )
= ( sk10
@ ( (=) @ $i
@ ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ^ [A: $i] : $true ) )
@ ^ [A: $i] : $true ) )
| ( ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ^ [A: $i] : $true )
!= ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ^ [A: $i] : $true ) ) ),
inference(replace_leibeq,[status(thm)],[21496:[bind(A,$thf( (=) @ $i @ ( sk2 @ ^ [B: $i] : ? [C: $i > $o] : ( ! [D: $i] : ( ( C @ D ) => ( sk1 @ C @ D ) ) & ( C @ B ) ) @ ^ [B: $i] : $true ) ))]]) ).
thf(21759,plain,
( ( ( sk10
@ ( (=) @ $i
@ ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ^ [A: $i] : $true ) )
@ ^ [A: $i] : $true )
= ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ^ [A: $i] : $true ) )
| ( ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ^ [A: $i] : $true )
!= ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ^ [A: $i] : $true ) ) ),
inference(lifteq,[status(thm)],[21695]) ).
thf(21935,plain,
( ( sk10
@ ( (=) @ $i
@ ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ^ [A: $i] : $true ) )
@ ^ [A: $i] : $true )
= ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ^ [A: $i] : $true ) ),
inference(pattern_uni,[status(thm)],[21759:[]]) ).
thf(34,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A @ C )
| ( sk1 @ B @ C )
| ( D @ ( sk2 @ E @ D ) )
| ~ $true
| ( sk1 @ E @ F )
| ( ( A @ ( sk2 @ B @ A ) )
!= ( sk1 @ D @ F ) ) ),
inference(paramod_ordered,[status(thm)],[8,8]) ).
thf(35,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A @ C )
| ( sk1 @ B @ C )
| ( D @ ( sk2 @ E @ D ) )
| ( sk1 @ E @ F )
| ( ( A @ ( sk2 @ B @ A ) )
!= ( sk1 @ D @ F ) ) ),
inference(simp,[status(thm)],[34]) ).
thf(49,plain,
! [E: $i > $i,D: $i > $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( sk1
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ B )
| ( sk1 @ A @ B )
| ( D
@ ( sk2 @ A
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) ) )
@ ( sk2 @ C
@ ( D
@ ( sk2 @ A
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) ) ) ) ) )
| ( sk1 @ C
@ ( E
@ ( sk2 @ A
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[35:[bind(A,$thf( ^ [I: $i] : ( sk1 @ ( G @ I ) @ ( H @ I ) ) )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( G @ ( sk2 @ B @ ^ [I: $i] : ( sk1 @ ( G @ I ) @ ( H @ I ) ) ) )),bind(E,$thf( E )),bind(F,$thf( H @ ( sk2 @ B @ ^ [I: $i] : ( sk1 @ ( G @ I ) @ ( H @ I ) ) ) ))]]) ).
thf(52,plain,
! [E: $i > $i,D: $i > $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( sk1
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ B )
| ( sk1 @ A @ B )
| ( D
@ ( sk2 @ A
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) ) )
@ ( sk2 @ C
@ ( D
@ ( sk2 @ A
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) ) ) ) ) )
| ( sk1 @ C
@ ( E
@ ( sk2 @ A
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) ) ) ) ) ),
inference(simp,[status(thm)],[49]) ).
thf(1657,plain,
( ~ $true
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1
@ ^ [A: $i] : $false
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[15,1522]) ).
thf(1658,plain,
( ( sk1 @ sk4 @ sk3 )
!= ( sk1
@ ^ [A: $i] : $false
@ sk3 ) ),
inference(simp,[status(thm)],[1657]) ).
thf(1695,plain,
( ( sk4
!= ( ^ [A: $i] : $false ) )
| ( sk3 != sk3 ) ),
inference(simp,[status(thm)],[1658]) ).
thf(1708,plain,
( sk4
!= ( ^ [A: $i] : $false ) ),
inference(simp,[status(thm)],[1695]) ).
thf(1709,plain,
sk4 @ sk17,
inference(func_ext,[status(esa)],[1708]) ).
thf(9309,plain,
( ~ $true
| ( ( sk1
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk3 )
!= ( sk1
@ ^ [A: $i] : $true
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[9279,6]) ).
thf(9310,plain,
( ( sk1
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk3 )
!= ( sk1
@ ^ [A: $i] : $true
@ sk3 ) ),
inference(simp,[status(thm)],[9309]) ).
thf(9342,plain,
( ( ( ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) ) )
!= ( ^ [A: $i] : $true ) )
| ( sk3 != sk3 ) ),
inference(simp,[status(thm)],[9310]) ).
thf(9360,plain,
( ( ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) ) )
!= ( ^ [A: $i] : $true ) ),
inference(simp,[status(thm)],[9342]) ).
thf(11094,plain,
! [A: $i > $o] :
( ~ ( sk9 @ sk3 )
| ~ $true
| ( sk1 @ A @ sk3 )
| ( ( A @ ( sk2 @ A @ sk4 ) )
!= ( sk1
@ ^ [B: $i] : $true
@ sk33 ) ) ),
inference(paramod_ordered,[status(thm)],[10595,140]) ).
thf(11095,plain,
! [A: $i > $o] :
( ~ ( sk9 @ sk3 )
| ( sk1 @ A @ sk3 )
| ( ( A @ ( sk2 @ A @ sk4 ) )
!= ( sk1
@ ^ [B: $i] : $true
@ sk33 ) ) ),
inference(simp,[status(thm)],[11094]) ).
thf(11200,plain,
( ~ ( sk9 @ sk3 )
| ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : $true
@ sk33 )
@ sk3 ) ),
inference(pre_uni,[status(thm)],[11095:[bind(A,$thf( ^ [B: $i] : ( sk1 @ ^ [C: $i] : $true @ sk33 ) ))]]) ).
thf(17177,plain,
( ( sk32 @ sk109 )
| ~ ( sk32 @ sk3 ) ),
inference(func_ext,[status(esa)],[16437]) ).
thf(17560,plain,
! [A: $i] :
( ~ ( sk32 @ sk3 )
| ~ $true
| ( sk1 @ sk32 @ A )
| ( ( sk32 @ sk109 )
!= ( sk32 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[17177,7404]) ).
thf(17561,plain,
! [A: $i] :
( ~ ( sk32 @ sk3 )
| ( sk1 @ sk32 @ A )
| ( ( sk32 @ sk109 )
!= ( sk32 @ A ) ) ),
inference(simp,[status(thm)],[17560]) ).
thf(17562,plain,
( ~ ( sk32 @ sk3 )
| ( sk1 @ sk32 @ sk109 ) ),
inference(pattern_uni,[status(thm)],[17561:[bind(A,$thf( sk109 ))]]) ).
thf(43,plain,
! [C: $i > $o,B: $i,A: $i > $o] :
( ~ ( C
@ ( sk2 @ A
@ ^ [D: $i] :
~ ( C @ D ) ) )
| ~ ( sk1
@ ^ [D: $i] :
~ ( C @ D )
@ B )
| ( sk1 @ A @ B ) ),
inference(prim_subst,[status(thm)],[8:[bind(A,$thf( ^ [E: $i] : ~ ( D @ E ) ))]]) ).
thf(56,plain,
! [C: $i > $o,B: $i,A: $i > $o] :
( ~ ( C
@ ( sk2 @ A
@ ^ [D: $i] :
~ ( C @ D ) ) )
| ~ ( sk1
@ ^ [D: $i] :
~ ( C @ D )
@ B )
| ( sk1 @ A @ B ) ),
inference(cnf,[status(esa)],[43]) ).
thf(57,plain,
! [C: $i > $o,B: $i,A: $i > $o] :
( ~ ( C
@ ( sk2 @ A
@ ^ [D: $i] :
~ ( C @ D ) ) )
| ~ ( sk1
@ ^ [D: $i] :
~ ( C @ D )
@ B )
| ( sk1 @ A @ B ) ),
inference(simp,[status(thm)],[56]) ).
thf(8977,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ~ $true
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1 @ sk9 @ sk5 )
!= ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[7468,136]) ).
thf(8978,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1 @ sk9 @ sk5 )
!= ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ) ),
inference(simp,[status(thm)],[8977]) ).
thf(9136,plain,
! [A: $i > $o] :
( ( sk1
@ ^ [B: $i] : ( sk1 @ sk9 @ sk5 )
@ sk5 )
| ( A != sk9 ) ),
inference(pre_uni,[status(thm)],[8978:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : sk9 )),bind(C,$thf( ^ [D: $i] : sk5 ))]]) ).
thf(9137,plain,
( sk1
@ ^ [A: $i] : ( sk1 @ sk9 @ sk5 )
@ sk5 ),
inference(pattern_uni,[status(thm)],[9136:[bind(A,$thf( sk9 ))]]) ).
thf(9362,plain,
( sk1
@ ^ [A: $i] : $true
@ sk5 ),
inference(rewrite,[status(thm)],[9137,7468]) ).
thf(121,plain,
! [D: $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( ( C
@ ( sk2
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ A ) )
| ( D
@ ( sk2
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ A ) ) )
| ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ B ) ),
inference(prim_subst,[status(thm)],[9:[bind(A,$thf( A )),bind(B,$thf( ^ [F: $i] : ( ( D @ F ) | ( E @ F ) ) ))]]) ).
thf(148,plain,
! [D: $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ( ~ ( C
@ ( sk2
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ A ) )
| ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ B ) )
& ( ~ ( D
@ ( sk2
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ A ) )
| ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ B ) ) ),
inference(cnf,[status(esa)],[121]) ).
thf(150,plain,
! [D: $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( D
@ ( sk2
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ A ) )
| ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ B ) ),
inference(cnfConj,[status(thm)],[148]) ).
thf(152,plain,
! [D: $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( D
@ ( sk2
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ A ) )
| ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ B ) ),
inference(simp,[status(thm)],[150]) ).
thf(1712,plain,
! [A: $i] :
( ~ $true
| ( sk1 @ sk4 @ A )
| ( ( sk4 @ sk17 )
!= ( sk4 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1709,10]) ).
thf(1713,plain,
! [A: $i] :
( ( sk1 @ sk4 @ A )
| ( ( sk4 @ sk17 )
!= ( sk4 @ A ) ) ),
inference(simp,[status(thm)],[1712]) ).
thf(1714,plain,
sk1 @ sk4 @ sk17,
inference(pattern_uni,[status(thm)],[1713:[bind(A,$thf( sk17 ))]]) ).
thf(163,plain,
! [A: $i > $o] :
( ( sk4 @ ( sk2 @ A @ sk4 ) )
| ~ $true
| ( ( sk1
@ ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) )
@ sk3 )
!= ( sk1 @ A @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[55,6]) ).
thf(164,plain,
! [A: $i > $o] :
( ( sk4 @ ( sk2 @ A @ sk4 ) )
| ( ( sk1
@ ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) )
@ sk3 )
!= ( sk1 @ A @ sk3 ) ) ),
inference(simp,[status(thm)],[163]) ).
thf(165,plain,
( sk4
@ ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 ) ),
inference(pattern_uni,[status(thm)],[164:[bind(A,$thf( ^ [B: $i] : ? [C: $i > $o] : ( ! [D: $i] : ( ( C @ D ) => ( sk1 @ C @ D ) ) & ( C @ B ) ) ))]]) ).
thf(190,plain,
! [A: $i] :
( ~ $true
| ( sk1 @ sk4 @ A )
| ( ( sk4
@ ( sk2
@ ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) )
@ sk4 ) )
!= ( sk4 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[165,10]) ).
thf(191,plain,
! [A: $i] :
( ( sk1 @ sk4 @ A )
| ( ( sk4
@ ( sk2
@ ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) )
@ sk4 ) )
!= ( sk4 @ A ) ) ),
inference(simp,[status(thm)],[190]) ).
thf(192,plain,
( sk1 @ sk4
@ ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 ) ),
inference(pattern_uni,[status(thm)],[191:[bind(A,$thf( sk2 @ ^ [B: $i] : ? [C: $i > $o] : ( ! [D: $i] : ( ( C @ D ) => ( sk1 @ C @ D ) ) & ( C @ B ) ) @ sk4 ))]]) ).
thf(207,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ $true
| ( sk1 @ B @ C )
| ( ( sk1 @ sk4
@ ( sk2
@ ^ [D: $i] :
? [E: $i > $o] :
( ! [F: $i] :
( ( E @ F )
=> ( sk1 @ E @ F ) )
& ( E @ D ) )
@ sk4 ) )
!= ( sk1 @ A @ C ) ) ),
inference(paramod_ordered,[status(thm)],[192,8]) ).
thf(208,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ( sk1 @ B @ C )
| ( ( sk1 @ sk4
@ ( sk2
@ ^ [D: $i] :
? [E: $i > $o] :
( ! [F: $i] :
( ( E @ F )
=> ( sk1 @ E @ F ) )
& ( E @ D ) )
@ sk4 ) )
!= ( sk1 @ A @ C ) ) ),
inference(simp,[status(thm)],[207]) ).
thf(209,plain,
! [A: $i > $o] :
( ( sk4 @ ( sk2 @ A @ sk4 ) )
| ( sk1 @ A
@ ( sk2
@ ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) )
@ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[208:[bind(A,$thf( sk4 )),bind(B,$thf( B )),bind(C,$thf( sk2 @ ^ [D: $i] : ? [E: $i > $o] : ( ! [F: $i] : ( ( E @ F ) => ( sk1 @ E @ F ) ) & ( E @ D ) ) @ sk4 ))]]) ).
thf(211,plain,
! [A: $i > $o] :
( ( sk4 @ ( sk2 @ A @ sk4 ) )
| ( sk1 @ A
@ ( sk2
@ ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) )
@ sk4 ) ) ),
inference(simp,[status(thm)],[209]) ).
thf(46,plain,
! [D: $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ( C
@ ( sk2 @ A
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) ) ) )
| ( D
@ ( sk2 @ A
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) ) ) )
| ~ ( sk1
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ B )
| ( sk1 @ A @ B ) ),
inference(prim_subst,[status(thm)],[8:[bind(A,$thf( ^ [F: $i] : ( ( D @ F ) | ( E @ F ) ) ))]]) ).
thf(60,plain,
! [D: $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ( C
@ ( sk2 @ A
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) ) ) )
| ( D
@ ( sk2 @ A
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) ) ) )
| ~ ( sk1
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ B )
| ( sk1 @ A @ B ) ),
inference(cnf,[status(esa)],[46]) ).
thf(61,plain,
! [D: $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ( C
@ ( sk2 @ A
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) ) ) )
| ( D
@ ( sk2 @ A
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) ) ) )
| ~ ( sk1
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ B )
| ( sk1 @ A @ B ) ),
inference(simp,[status(thm)],[60]) ).
thf(11096,plain,
! [A: $i > $o] :
( ~ ( sk9 @ sk3 )
| ~ $true
| ( sk1 @ A @ sk3 )
| ( ( A @ ( sk2 @ A @ sk4 ) )
!= ( sk9 @ sk33 ) ) ),
inference(paramod_ordered,[status(thm)],[7570,140]) ).
thf(11097,plain,
! [A: $i > $o] :
( ~ ( sk9 @ sk3 )
| ( sk1 @ A @ sk3 )
| ( ( A @ ( sk2 @ A @ sk4 ) )
!= ( sk9 @ sk33 ) ) ),
inference(simp,[status(thm)],[11096]) ).
thf(11136,plain,
( ~ ( sk9 @ sk3 )
| ( sk1
@ ^ [A: $i] : ( sk9 @ sk33 )
@ sk3 ) ),
inference(pre_uni,[status(thm)],[11097:[bind(A,$thf( ^ [B: $i] : ( sk9 @ sk33 ) ))]]) ).
thf(7370,plain,
( ~ $true
| ( ( sk4 @ sk17 )
!= ( sk4 @ sk5 ) ) ),
inference(paramod_ordered,[status(thm)],[1709,7343]) ).
thf(7371,plain,
( ( sk4 @ sk17 )
!= ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[7370]) ).
thf(7393,plain,
sk17 != sk5,
inference(simp,[status(thm)],[7371]) ).
thf(10559,plain,
! [B: $i,A: $i > $o] :
( ~ $true
| ( sk1
@ ^ [C: $i] : $true
@ B )
| ( ( sk1 @ sk4
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ sk4 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[192,10468]) ).
thf(10560,plain,
! [B: $i,A: $i > $o] :
( ( sk1
@ ^ [C: $i] : $true
@ B )
| ( ( sk1 @ sk4
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ sk4 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[10559]) ).
thf(10561,plain,
( sk1
@ ^ [A: $i] : $true
@ ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 ) ),
inference(pattern_uni,[status(thm)],[10560:[bind(A,$thf( sk4 )),bind(B,$thf( sk2 @ ^ [C: $i] : ? [D: $i > $o] : ( ! [E: $i] : ( ( D @ E ) => ( sk1 @ D @ E ) ) & ( D @ C ) ) @ sk4 ))]]) ).
thf(7547,plain,
! [B: $i,A: $i > $o] :
( ~ $true
| ( sk1 @ A @ B )
| ( ( sk1 @ sk9 @ sk5 )
!= ( sk1
@ ^ [C: $i] : $false
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[7468,58]) ).
thf(7548,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A @ B )
| ( ( sk1 @ sk9 @ sk5 )
!= ( sk1
@ ^ [C: $i] : $false
@ B ) ) ),
inference(simp,[status(thm)],[7547]) ).
thf(7558,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A @ B )
| ( sk9
!= ( ^ [C: $i] : $false ) )
| ( sk5 != B ) ),
inference(simp,[status(thm)],[7548]) ).
thf(7565,plain,
! [A: $i > $o] :
( ( sk1 @ A @ sk5 )
| ( sk9
!= ( ^ [B: $i] : $false ) ) ),
inference(simp,[status(thm)],[7558]) ).
thf(91,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( B @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ~ $true
| ~ ( sk1 @ D @ F )
| ( sk1 @ E @ F )
| ( ( sk1 @ B @ C )
!= ( E @ ( sk2 @ E @ D ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,9]) ).
thf(92,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( B @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ~ ( sk1 @ D @ F )
| ( sk1 @ E @ F )
| ( ( sk1 @ B @ C )
!= ( E @ ( sk2 @ E @ D ) ) ) ),
inference(simp,[status(thm)],[91]) ).
thf(131,plain,
! [E: $i > $i,D: $i > $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( D
@ ( sk2
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ B )
@ ( sk2
@ ( D
@ ( sk2
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ B ) )
@ A ) )
| ~ ( sk1 @ A
@ ( E
@ ( sk2
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ B ) ) )
| ~ ( sk1 @ B @ C )
| ( sk1
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ C ) ),
inference(pre_uni,[status(thm)],[92:[bind(A,$thf( A )),bind(B,$thf( G @ ( sk2 @ ^ [I: $i] : ( sk1 @ ( G @ I ) @ ( H @ I ) ) @ D ) )),bind(C,$thf( H @ ( sk2 @ ^ [I: $i] : ( sk1 @ ( G @ I ) @ ( H @ I ) ) @ D ) )),bind(D,$thf( D )),bind(E,$thf( ^ [I: $i] : ( sk1 @ ( G @ I ) @ ( H @ I ) ) ))]]) ).
thf(137,plain,
! [E: $i > $i,D: $i > $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( D
@ ( sk2
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ B )
@ ( sk2
@ ( D
@ ( sk2
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ B ) )
@ A ) )
| ~ ( sk1 @ A
@ ( E
@ ( sk2
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ B ) ) )
| ~ ( sk1 @ B @ C )
| ( sk1
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ C ) ),
inference(simp,[status(thm)],[131]) ).
thf(21617,plain,
! [B: $i > $o,A: $i > $o] :
( ( B @ ( sk10 @ B @ A ) )
| ~ ( B
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ A ) )
| ~ $true
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ A @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[15,154]) ).
thf(21618,plain,
! [B: $i > $o,A: $i > $o] :
( ( B @ ( sk10 @ B @ A ) )
| ~ ( B
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ A ) )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ A @ sk3 ) ) ),
inference(simp,[status(thm)],[21617]) ).
thf(21619,plain,
! [A: $i > $o] :
( ( A @ ( sk10 @ A @ sk4 ) )
| ~ ( A
@ ( sk2
@ ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) )
@ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[21618:[bind(A,$thf( sk4 )),bind(B,$thf( B ))]]) ).
thf(21677,plain,
( ( ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 )
= ( sk10
@ ( (=) @ $i
@ ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 ) )
@ sk4 ) )
| ( ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 )
!= ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 ) ) ),
inference(replace_leibeq,[status(thm)],[21619:[bind(A,$thf( (=) @ $i @ ( sk2 @ ^ [B: $i] : ? [C: $i > $o] : ( ! [D: $i] : ( ( C @ D ) => ( sk1 @ C @ D ) ) & ( C @ B ) ) @ sk4 ) ))]]) ).
thf(21734,plain,
( ( ( sk10
@ ( (=) @ $i
@ ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 ) )
@ sk4 )
= ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 ) )
| ( ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 )
!= ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 ) ) ),
inference(lifteq,[status(thm)],[21677]) ).
thf(22073,plain,
( ( sk10
@ ( (=) @ $i
@ ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 ) )
@ sk4 )
= ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 ) ),
inference(pattern_uni,[status(thm)],[21734:[]]) ).
thf(25,plain,
! [D: $i,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A @ C )
| ( sk1 @ B @ C )
| ~ $true
| ( sk1 @ sk4 @ D )
| ( ( A @ ( sk2 @ B @ A ) )
!= ( sk4 @ D ) ) ),
inference(paramod_ordered,[status(thm)],[8,10]) ).
thf(26,plain,
! [D: $i,C: $i,B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ A @ C )
| ( sk1 @ B @ C )
| ( sk1 @ sk4 @ D )
| ( ( A @ ( sk2 @ B @ A ) )
!= ( sk4 @ D ) ) ),
inference(simp,[status(thm)],[25]) ).
thf(50,plain,
! [C: $i > $i,B: $i,A: $i > $o] :
( ~ ( sk1
@ ^ [D: $i] : ( sk4 @ ( C @ D ) )
@ B )
| ( sk1 @ A @ B )
| ( sk1 @ sk4
@ ( C
@ ( sk2 @ A
@ ^ [D: $i] : ( sk4 @ ( C @ D ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[26:[bind(A,$thf( ^ [F: $i] : ( sk4 @ ( E @ F ) ) )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( E @ ( sk2 @ B @ ^ [F: $i] : ( sk4 @ ( E @ F ) ) ) ))]]) ).
thf(53,plain,
! [C: $i > $i,B: $i,A: $i > $o] :
( ~ ( sk1
@ ^ [D: $i] : ( sk4 @ ( C @ D ) )
@ B )
| ( sk1 @ A @ B )
| ( sk1 @ sk4
@ ( C
@ ( sk2 @ A
@ ^ [D: $i] : ( sk4 @ ( C @ D ) ) ) ) ) ),
inference(simp,[status(thm)],[50]) ).
thf(110,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ~ $true
| ~ ( sk1 @ D @ F )
| ( sk1 @ E @ F )
| ( ( sk1 @ B @ C )
!= ( E @ ( sk2 @ E @ D ) ) ) ),
inference(paramod_ordered,[status(thm)],[8,9]) ).
thf(111,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ~ ( sk1 @ D @ F )
| ( sk1 @ E @ F )
| ( ( sk1 @ B @ C )
!= ( E @ ( sk2 @ E @ D ) ) ) ),
inference(simp,[status(thm)],[110]) ).
thf(134,plain,
! [E: $i > $i,D: $i > $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ( A
@ ( sk2
@ ( D
@ ( sk2
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ B ) )
@ A ) )
| ~ ( sk1 @ A
@ ( E
@ ( sk2
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ B ) ) )
| ~ ( sk1 @ B @ C )
| ( sk1
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ C ) ),
inference(pre_uni,[status(thm)],[111:[bind(A,$thf( A )),bind(B,$thf( G @ ( sk2 @ ^ [I: $i] : ( sk1 @ ( G @ I ) @ ( H @ I ) ) @ D ) )),bind(C,$thf( H @ ( sk2 @ ^ [I: $i] : ( sk1 @ ( G @ I ) @ ( H @ I ) ) @ D ) )),bind(D,$thf( D )),bind(E,$thf( ^ [I: $i] : ( sk1 @ ( G @ I ) @ ( H @ I ) ) ))]]) ).
thf(141,plain,
! [E: $i > $i,D: $i > $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ( A
@ ( sk2
@ ( D
@ ( sk2
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ B ) )
@ A ) )
| ~ ( sk1 @ A
@ ( E
@ ( sk2
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ B ) ) )
| ~ ( sk1 @ B @ C )
| ( sk1
@ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) )
@ C ) ),
inference(simp,[status(thm)],[134]) ).
thf(17563,plain,
! [A: $i > $o] :
( ~ ( sk32 @ sk3 )
| ~ $true
| ( sk1 @ A @ sk3 )
| ( ( A @ ( sk2 @ A @ sk4 ) )
!= ( sk32 @ sk109 ) ) ),
inference(paramod_ordered,[status(thm)],[17177,140]) ).
thf(17564,plain,
! [A: $i > $o] :
( ~ ( sk32 @ sk3 )
| ( sk1 @ A @ sk3 )
| ( ( A @ ( sk2 @ A @ sk4 ) )
!= ( sk32 @ sk109 ) ) ),
inference(simp,[status(thm)],[17563]) ).
thf(17589,plain,
( ~ ( sk32 @ sk3 )
| ( sk1
@ ^ [A: $i] : ( sk32 @ sk109 )
@ sk3 ) ),
inference(pre_uni,[status(thm)],[17564:[bind(A,$thf( ^ [B: $i] : ( sk32 @ sk109 ) ))]]) ).
thf(19303,plain,
( ~ ( sk32 @ sk3 )
| ~ $true
| ( ( sk1
@ ^ [A: $i] : ( sk32 @ sk109 )
@ sk3 )
!= ( sk1
@ ^ [A: $i] : $false
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[17589,1522]) ).
thf(19304,plain,
( ~ ( sk32 @ sk3 )
| ( ( sk1
@ ^ [A: $i] : ( sk32 @ sk109 )
@ sk3 )
!= ( sk1
@ ^ [A: $i] : $false
@ sk3 ) ) ),
inference(simp,[status(thm)],[19303]) ).
thf(19420,plain,
( ~ ( sk32 @ sk3 )
| ( ( ^ [A: $i] : ( sk32 @ sk109 ) )
!= ( ^ [A: $i] : $false ) )
| ( sk3 != sk3 ) ),
inference(simp,[status(thm)],[19304]) ).
thf(19478,plain,
( ~ ( sk32 @ sk3 )
| ( ( ^ [A: $i] : ( sk32 @ sk109 ) )
!= ( ^ [A: $i] : $false ) ) ),
inference(simp,[status(thm)],[19420]) ).
thf(64,plain,
( ~ ? [A: $i > $o] :
( ! [B: $i] :
( ( A @ B )
=> ( sk1 @ A @ B ) )
& ( A @ sk5 ) )
| ( ( sk4 @ sk5 )
!= ( sk4 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[7,22]) ).
thf(68,plain,
( ~ ? [A: $i > $o] :
( ! [B: $i] :
( ( A @ B )
=> ( sk1 @ A @ B ) )
& ( A @ sk5 ) )
| ( sk5 != sk3 ) ),
inference(simp,[status(thm)],[64]) ).
thf(74,plain,
! [A: $i > $o] :
( ( ( A @ ( sk7 @ A ) )
| ~ ( A @ sk5 )
| ( sk5 != sk3 ) )
& ( ~ ( sk1 @ A @ ( sk7 @ A ) )
| ~ ( A @ sk5 )
| ( sk5 != sk3 ) ) ),
inference(cnf,[status(esa)],[68]) ).
thf(76,plain,
! [A: $i > $o] :
( ~ ( sk1 @ A @ ( sk7 @ A ) )
| ~ ( A @ sk5 )
| ( sk5 != sk3 ) ),
inference(cnfConj,[status(thm)],[74]) ).
thf(249,plain,
! [B: $i > $o,A: $i] :
( ~ ( sk4 @ A )
| ~ $true
| ~ ( B @ sk5 )
| ( sk5 != sk3 )
| ( ( sk1 @ sk4 @ A )
!= ( sk1 @ B @ ( sk7 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[10,76]) ).
thf(250,plain,
! [B: $i > $o,A: $i] :
( ~ ( sk4 @ A )
| ~ ( B @ sk5 )
| ( sk5 != sk3 )
| ( ( sk1 @ sk4 @ A )
!= ( sk1 @ B @ ( sk7 @ B ) ) ) ),
inference(simp,[status(thm)],[249]) ).
thf(251,plain,
( ~ ( sk4 @ ( sk7 @ sk4 ) )
| ~ ( sk4 @ sk5 )
| ( sk5 != sk3 ) ),
inference(pattern_uni,[status(thm)],[250:[bind(A,$thf( sk7 @ sk4 )),bind(B,$thf( sk4 ))]]) ).
thf(583,plain,
( ~ ( sk4 @ sk5 )
| ( sk5 != sk3 )
| ( ( sk4 @ ( sk7 @ sk4 ) )
!= ( sk4 @ sk5 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[251]) ).
thf(594,plain,
( ~ ( sk4 @ sk5 )
| ( sk5 != sk3 )
| ( ( sk4 @ ( sk7 @ sk4 ) )
!= ( sk4 @ sk5 ) ) ),
inference(simp,[status(thm)],[583]) ).
thf(4884,plain,
( ~ $true
| ( sk5 != sk3 )
| ( ( sk4 @ ( sk7 @ sk4 ) )
!= ( sk4 @ sk5 ) )
| ( ( sk4 @ sk5 )
!= ( sk4 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[7,594]) ).
thf(4885,plain,
( ( sk5 != sk3 )
| ( ( sk4 @ ( sk7 @ sk4 ) )
!= ( sk4 @ sk5 ) )
| ( ( sk4 @ sk5 )
!= ( sk4 @ sk3 ) ) ),
inference(simp,[status(thm)],[4884]) ).
thf(4938,plain,
( ( sk5 != sk3 )
| ( ( sk4 @ ( sk7 @ sk4 ) )
!= ( sk4 @ sk5 ) )
| ( sk5 != sk3 ) ),
inference(simp,[status(thm)],[4885]) ).
thf(4951,plain,
( ( sk5 != sk3 )
| ( ( sk4 @ ( sk7 @ sk4 ) )
!= ( sk4 @ sk5 ) ) ),
inference(simp,[status(thm)],[4938]) ).
thf(5575,plain,
( ( sk5 != sk3 )
| ( sk4 @ ( sk7 @ sk4 ) )
| ( sk4 @ sk5 ) ),
inference(bool_ext,[status(thm)],[4951]) ).
thf(577,plain,
( ~ ( sk4 @ ( sk7 @ sk4 ) )
| ~ $true
| ( sk5 != sk3 )
| ( ( sk4 @ sk5 )
!= ( sk4 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[7,251]) ).
thf(578,plain,
( ~ ( sk4 @ ( sk7 @ sk4 ) )
| ( sk5 != sk3 )
| ( ( sk4 @ sk5 )
!= ( sk4 @ sk3 ) ) ),
inference(simp,[status(thm)],[577]) ).
thf(587,plain,
( ~ ( sk4 @ ( sk7 @ sk4 ) )
| ( sk5 != sk3 )
| ( sk5 != sk3 ) ),
inference(simp,[status(thm)],[578]) ).
thf(597,plain,
( ~ ( sk4 @ ( sk7 @ sk4 ) )
| ( sk5 != sk3 ) ),
inference(simp,[status(thm)],[587]) ).
thf(5628,plain,
( ( sk5 != sk3 )
| ( sk4 @ sk5 )
| ~ $true
| ( sk5 != sk3 )
| ( ( sk4 @ ( sk7 @ sk4 ) )
!= ( sk4 @ ( sk7 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[5575,597]) ).
thf(5629,plain,
( ( sk5 != sk3 )
| ( sk4 @ sk5 )
| ( ( sk4 @ ( sk7 @ sk4 ) )
!= ( sk4 @ ( sk7 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[5628]) ).
thf(5630,plain,
( ( sk5 != sk3 )
| ( sk4 @ sk5 ) ),
inference(pattern_uni,[status(thm)],[5629:[]]) ).
thf(75,plain,
! [A: $i > $o] :
( ( A @ ( sk7 @ A ) )
| ~ ( A @ sk5 )
| ( sk5 != sk3 ) ),
inference(cnfConj,[status(thm)],[74]) ).
thf(5709,plain,
! [A: $i > $o] :
( ~ ( A @ sk5 )
| ( sk5 != sk3 )
| ~ $true
| ( sk5 != sk3 )
| ( ( A @ ( sk7 @ A ) )
!= ( sk4 @ ( sk7 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[75,597]) ).
thf(5710,plain,
! [A: $i > $o] :
( ~ ( A @ sk5 )
| ( sk5 != sk3 )
| ( ( A @ ( sk7 @ A ) )
!= ( sk4 @ ( sk7 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[5709]) ).
thf(5978,plain,
( ~ ( sk4 @ sk5 )
| ( sk5 != sk3 ) ),
inference(pre_uni,[status(thm)],[5710:[bind(A,$thf( sk4 ))]]) ).
thf(6162,plain,
( ( sk5 != sk3 )
| ~ $true
| ( sk5 != sk3 )
| ( ( sk4 @ sk5 )
!= ( sk4 @ sk5 ) ) ),
inference(paramod_ordered,[status(thm)],[5630,5978]) ).
thf(6163,plain,
( ( sk5 != sk3 )
| ( ( sk4 @ sk5 )
!= ( sk4 @ sk5 ) ) ),
inference(simp,[status(thm)],[6162]) ).
thf(6164,plain,
sk5 != sk3,
inference(pattern_uni,[status(thm)],[6163:[]]) ).
thf(7636,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ( sk9 @ ( sk2 @ A @ sk9 ) )
| ~ $true
| ( sk1 @ B @ C )
| ( ( sk1 @ A @ sk5 )
!= ( sk1
@ ^ [D: $i] : $false
@ C ) ) ),
inference(paramod_ordered,[status(thm)],[7569,58]) ).
thf(7637,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ( sk9 @ ( sk2 @ A @ sk9 ) )
| ( sk1 @ B @ C )
| ( ( sk1 @ A @ sk5 )
!= ( sk1
@ ^ [D: $i] : $false
@ C ) ) ),
inference(simp,[status(thm)],[7636]) ).
thf(7638,plain,
! [A: $i > $o] :
( ( sk9
@ ( sk2
@ ^ [B: $i] : $false
@ sk9 ) )
| ( sk1 @ A @ sk5 ) ),
inference(pattern_uni,[status(thm)],[7637:[bind(A,$thf( ^ [D: $i] : $false )),bind(B,$thf( B )),bind(C,$thf( sk5 ))]]) ).
thf(7661,plain,
! [A: $i > $o] :
( ( sk9
@ ( sk2
@ ^ [B: $i] : $false
@ sk9 ) )
| ( sk1 @ A @ sk5 ) ),
inference(simp,[status(thm)],[7638]) ).
thf(231,plain,
! [D: $i,C: $i > $o,B: $i > $o,A: $i > $o] :
( ( sk1 @ A @ sk3 )
| ( B @ ( sk2 @ C @ B ) )
| ~ $true
| ( sk1 @ C @ D )
| ( ( sk1 @ sk4 @ ( sk2 @ A @ sk4 ) )
!= ( sk1 @ B @ D ) ) ),
inference(paramod_ordered,[status(thm)],[183,8]) ).
thf(232,plain,
! [D: $i,C: $i > $o,B: $i > $o,A: $i > $o] :
( ( sk1 @ A @ sk3 )
| ( B @ ( sk2 @ C @ B ) )
| ( sk1 @ C @ D )
| ( ( sk1 @ sk4 @ ( sk2 @ A @ sk4 ) )
!= ( sk1 @ B @ D ) ) ),
inference(simp,[status(thm)],[231]) ).
thf(233,plain,
! [B: $i > $o,A: $i > $o] :
( ( sk1 @ B @ sk3 )
| ( sk4 @ ( sk2 @ A @ sk4 ) )
| ( sk1 @ A @ ( sk2 @ B @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[232:[bind(A,$thf( F )),bind(B,$thf( sk4 )),bind(C,$thf( C )),bind(D,$thf( sk2 @ F @ sk4 ))]]) ).
thf(244,plain,
! [B: $i > $o,A: $i > $o] :
( ( sk1 @ B @ sk3 )
| ( sk4 @ ( sk2 @ A @ sk4 ) )
| ( sk1 @ A @ ( sk2 @ B @ sk4 ) ) ),
inference(simp,[status(thm)],[233]) ).
thf(7354,plain,
( ~ $true
| ( ( sk4
@ ( sk2
@ ^ [A: $i] : $false
@ sk4 ) )
!= ( sk4 @ sk5 ) ) ),
inference(paramod_ordered,[status(thm)],[1656,7343]) ).
thf(7355,plain,
( ( sk4
@ ( sk2
@ ^ [A: $i] : $false
@ sk4 ) )
!= ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[7354]) ).
thf(7397,plain,
( ( sk2
@ ^ [A: $i] : $false
@ sk4 )
!= sk5 ),
inference(simp,[status(thm)],[7355]) ).
thf(1762,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ $true
| ( sk1 @ B @ C )
| ( ( sk1 @ sk4 @ sk17 )
!= ( sk1 @ A @ C ) ) ),
inference(paramod_ordered,[status(thm)],[1714,8]) ).
thf(1763,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ( sk1 @ B @ C )
| ( ( sk1 @ sk4 @ sk17 )
!= ( sk1 @ A @ C ) ) ),
inference(simp,[status(thm)],[1762]) ).
thf(1764,plain,
! [A: $i > $o] :
( ( sk4 @ ( sk2 @ A @ sk4 ) )
| ( sk1 @ A @ sk17 ) ),
inference(pattern_uni,[status(thm)],[1763:[bind(A,$thf( sk4 )),bind(B,$thf( B )),bind(C,$thf( sk17 ))]]) ).
thf(1784,plain,
! [A: $i > $o] :
( ( sk4 @ ( sk2 @ A @ sk4 ) )
| ( sk1 @ A @ sk17 ) ),
inference(simp,[status(thm)],[1764]) ).
thf(27,plain,
! [D: $i,C: $i > $o,B: $i > $o,A: $i] :
( ~ ( sk4 @ A )
| ( B @ ( sk2 @ C @ B ) )
| ~ $true
| ( sk1 @ C @ D )
| ( ( sk1 @ sk4 @ A )
!= ( sk1 @ B @ D ) ) ),
inference(paramod_ordered,[status(thm)],[10,8]) ).
thf(28,plain,
! [D: $i,C: $i > $o,B: $i > $o,A: $i] :
( ~ ( sk4 @ A )
| ( B @ ( sk2 @ C @ B ) )
| ( sk1 @ C @ D )
| ( ( sk1 @ sk4 @ A )
!= ( sk1 @ B @ D ) ) ),
inference(simp,[status(thm)],[27]) ).
thf(29,plain,
! [B: $i > $o,A: $i] :
( ~ ( sk4 @ A )
| ( sk4 @ ( sk2 @ B @ sk4 ) )
| ( sk1 @ B @ A ) ),
inference(pattern_uni,[status(thm)],[28:[bind(A,$thf( A )),bind(B,$thf( sk4 )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(59,plain,
! [B: $i > $o,A: $i] :
( ~ ( sk4 @ A )
| ( sk4 @ ( sk2 @ B @ sk4 ) )
| ( sk1 @ B @ A ) ),
inference(simp,[status(thm)],[29]) ).
thf(17684,plain,
! [B: $i,A: $i > $o] :
( ~ ( sk32 @ sk3 )
| ~ $true
| ( sk1
@ ^ [C: $i] : $true
@ B )
| ( ( sk1 @ sk32 @ sk109 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[17562,10468]) ).
thf(17685,plain,
! [B: $i,A: $i > $o] :
( ~ ( sk32 @ sk3 )
| ( sk1
@ ^ [C: $i] : $true
@ B )
| ( ( sk1 @ sk32 @ sk109 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[17684]) ).
thf(17686,plain,
( ~ ( sk32 @ sk3 )
| ( sk1
@ ^ [A: $i] : $true
@ sk109 ) ),
inference(pattern_uni,[status(thm)],[17685:[bind(A,$thf( sk32 )),bind(B,$thf( sk109 ))]]) ).
thf(36,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ( D @ ( sk2 @ E @ D ) )
| ~ $true
| ( sk1 @ E @ F )
| ( ( sk1 @ B @ C )
!= ( sk1 @ D @ F ) ) ),
inference(paramod_ordered,[status(thm)],[8,8]) ).
thf(37,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ( D @ ( sk2 @ E @ D ) )
| ( sk1 @ E @ F )
| ( ( sk1 @ B @ C )
!= ( sk1 @ D @ F ) ) ),
inference(simp,[status(thm)],[36]) ).
thf(38,plain,
! [D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ( B @ ( sk2 @ D @ B ) )
| ( sk1 @ D @ C ) ),
inference(pattern_uni,[status(thm)],[37:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( B )),bind(E,$thf( E )),bind(F,$thf( C ))]]) ).
thf(54,plain,
! [D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ( B @ ( sk2 @ D @ B ) )
| ( sk1 @ D @ C ) ),
inference(simp,[status(thm)],[38]) ).
thf(8937,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ~ $true
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1 @ sk4
@ ( sk2
@ ^ [D: $i] : $false
@ sk4 ) )
!= ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1793,136]) ).
thf(8938,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1 @ sk4
@ ( sk2
@ ^ [D: $i] : $false
@ sk4 ) )
!= ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ) ),
inference(simp,[status(thm)],[8937]) ).
thf(9082,plain,
! [A: $i > $o] :
( ( sk1
@ ^ [B: $i] :
( sk1 @ sk4
@ ( sk2
@ ^ [C: $i] : $false
@ sk4 ) )
@ ( sk2
@ ^ [B: $i] : $false
@ sk4 ) )
| ( A != sk4 ) ),
inference(pre_uni,[status(thm)],[8938:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : sk4 )),bind(C,$thf( ^ [D: $i] : ( sk2 @ ^ [E: $i] : $false @ sk4 ) ))]]) ).
thf(9083,plain,
( sk1
@ ^ [A: $i] :
( sk1 @ sk4
@ ( sk2
@ ^ [B: $i] : $false
@ sk4 ) )
@ ( sk2
@ ^ [A: $i] : $false
@ sk4 ) ),
inference(pattern_uni,[status(thm)],[9082:[bind(A,$thf( sk4 ))]]) ).
thf(10279,plain,
( sk1
@ ^ [A: $i] : $true
@ ( sk2
@ ^ [A: $i] : $false
@ sk4 ) ),
inference(rewrite,[status(thm)],[9083,1793]) ).
thf(1755,plain,
! [C: $i > $i,B: $i,A: $i > $o] :
( ~ $true
| ( sk1 @ A @ B )
| ( sk1 @ sk4
@ ( C
@ ( sk2 @ A
@ ^ [D: $i] : ( sk4 @ ( C @ D ) ) ) ) )
| ( ( sk1
@ ^ [D: $i] : ( sk4 @ ( C @ D ) )
@ B )
!= ( sk1 @ sk4 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[1714,53]) ).
thf(1756,plain,
! [C: $i > $i,B: $i,A: $i > $o] :
( ( sk1 @ A @ B )
| ( sk1 @ sk4
@ ( C
@ ( sk2 @ A
@ ^ [D: $i] : ( sk4 @ ( C @ D ) ) ) ) )
| ( ( sk1
@ ^ [D: $i] : ( sk4 @ ( C @ D ) )
@ B )
!= ( sk1 @ sk4 @ sk17 ) ) ),
inference(simp,[status(thm)],[1755]) ).
thf(1757,plain,
! [A: $i > $o] :
( ( sk1 @ A @ sk17 )
| ( sk1 @ sk4 @ ( sk2 @ A @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[1756:[bind(A,$thf( A )),bind(B,$thf( sk17 )),bind(C,$thf( ^ [D: $i] : D ))]]) ).
thf(9019,plain,
! [D: $i > $i,C: $i > $i > $o,B: $i > $o,A: $i > $o] :
( ( sk1 @ A @ sk17 )
| ( sk1
@ ^ [E: $i] : ( sk1 @ ( C @ E ) @ ( D @ E ) )
@ ( D
@ ( sk2
@ ^ [E: $i] : ( sk1 @ ( C @ E ) @ ( D @ E ) )
@ B ) ) )
| ~ $true
| ( B
!= ( C
@ ( sk2
@ ^ [E: $i] : ( sk1 @ ( C @ E ) @ ( D @ E ) )
@ B ) ) )
| ( ( sk1 @ sk4 @ ( sk2 @ A @ sk4 ) )
!= ( sk1
@ ( C
@ ( sk2
@ ^ [E: $i] : ( sk1 @ ( C @ E ) @ ( D @ E ) )
@ B ) )
@ ( D
@ ( sk2
@ ^ [E: $i] : ( sk1 @ ( C @ E ) @ ( D @ E ) )
@ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1757,136]) ).
thf(9020,plain,
! [D: $i > $i,C: $i > $i > $o,B: $i > $o,A: $i > $o] :
( ( sk1 @ A @ sk17 )
| ( sk1
@ ^ [E: $i] : ( sk1 @ ( C @ E ) @ ( D @ E ) )
@ ( D
@ ( sk2
@ ^ [E: $i] : ( sk1 @ ( C @ E ) @ ( D @ E ) )
@ B ) ) )
| ( B
!= ( C
@ ( sk2
@ ^ [E: $i] : ( sk1 @ ( C @ E ) @ ( D @ E ) )
@ B ) ) )
| ( ( sk1 @ sk4 @ ( sk2 @ A @ sk4 ) )
!= ( sk1
@ ( C
@ ( sk2
@ ^ [E: $i] : ( sk1 @ ( C @ E ) @ ( D @ E ) )
@ B ) )
@ ( D
@ ( sk2
@ ^ [E: $i] : ( sk1 @ ( C @ E ) @ ( D @ E ) )
@ B ) ) ) ) ),
inference(simp,[status(thm)],[9019]) ).
thf(9045,plain,
( ( sk1 @ ( sk1 @ sk4 ) @ sk17 )
| ( sk1 @ ( sk1 @ sk4 ) @ ( sk2 @ ( sk1 @ sk4 ) @ sk4 ) )
| ( sk4 != sk4 ) ),
inference(pre_uni,[status(thm)],[9020:[bind(A,$thf( sk1 @ sk4 )),bind(B,$thf( sk4 )),bind(C,$thf( ^ [E: $i] : sk4 )),bind(D,$thf( ^ [E: $i] : E ))]]) ).
thf(9047,plain,
( ( sk1 @ ( sk1 @ sk4 ) @ ( sk2 @ ( sk1 @ sk4 ) @ sk4 ) )
| ( sk1 @ ( sk1 @ sk4 ) @ sk17 ) ),
inference(pattern_uni,[status(thm)],[9045:[]]) ).
thf(21148,plain,
! [B: $i > $o,A: $i > $o] :
( ( B @ ( sk10 @ B @ A ) )
| ~ ( B
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ A ) )
| ~ $true
| ( ( sk1 @ ( sk1 @ sk4 ) @ sk3 )
!= ( sk1 @ A @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[11266,154]) ).
thf(21149,plain,
! [B: $i > $o,A: $i > $o] :
( ( B @ ( sk10 @ B @ A ) )
| ~ ( B
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ A ) )
| ( ( sk1 @ ( sk1 @ sk4 ) @ sk3 )
!= ( sk1 @ A @ sk3 ) ) ),
inference(simp,[status(thm)],[21148]) ).
thf(21150,plain,
! [A: $i > $o] :
( ( A @ ( sk10 @ A @ ( sk1 @ sk4 ) ) )
| ~ ( A
@ ( sk2
@ ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) )
@ ( sk1 @ sk4 ) ) ) ),
inference(pattern_uni,[status(thm)],[21149:[bind(A,$thf( sk1 @ sk4 )),bind(B,$thf( B ))]]) ).
thf(21668,plain,
( ( ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ( sk1 @ sk4 ) )
= ( sk10
@ ( (=) @ $i
@ ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ( sk1 @ sk4 ) ) )
@ ( sk1 @ sk4 ) ) )
| ( ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ( sk1 @ sk4 ) )
!= ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ( sk1 @ sk4 ) ) ) ),
inference(replace_leibeq,[status(thm)],[21150:[bind(A,$thf( (=) @ $i @ ( sk2 @ ^ [B: $i] : ? [C: $i > $o] : ( ! [D: $i] : ( ( C @ D ) => ( sk1 @ C @ D ) ) & ( C @ B ) ) @ ( sk1 @ sk4 ) ) ))]]) ).
thf(21746,plain,
( ( ( sk10
@ ( (=) @ $i
@ ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ( sk1 @ sk4 ) ) )
@ ( sk1 @ sk4 ) )
= ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ( sk1 @ sk4 ) ) )
| ( ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ( sk1 @ sk4 ) )
!= ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ( sk1 @ sk4 ) ) ) ),
inference(lifteq,[status(thm)],[21668]) ).
thf(21978,plain,
( ( sk10
@ ( (=) @ $i
@ ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ( sk1 @ sk4 ) ) )
@ ( sk1 @ sk4 ) )
= ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ ( sk1 @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[21746:[]]) ).
thf(11404,plain,
! [B: $i,A: $i > $o] :
( ~ $true
| ( sk1
@ ^ [C: $i] : $true
@ B )
| ( ( sk1 @ sk4 @ sk38 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[11360,10468]) ).
thf(11405,plain,
! [B: $i,A: $i > $o] :
( ( sk1
@ ^ [C: $i] : $true
@ B )
| ( ( sk1 @ sk4 @ sk38 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[11404]) ).
thf(11406,plain,
( sk1
@ ^ [A: $i] : $true
@ sk38 ),
inference(pattern_uni,[status(thm)],[11405:[bind(A,$thf( sk4 )),bind(B,$thf( sk38 ))]]) ).
thf(339,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ sk4 ) )
| ~ $true
| ( sk1 @ sk4 @ B )
| ( ( sk4 @ ( sk2 @ A @ sk4 ) )
!= ( sk4 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[211,10]) ).
thf(340,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ sk4 ) )
| ( sk1 @ sk4 @ B )
| ( ( sk4 @ ( sk2 @ A @ sk4 ) )
!= ( sk4 @ B ) ) ),
inference(simp,[status(thm)],[339]) ).
thf(341,plain,
! [A: $i > $o] :
( ( sk1 @ A
@ ( sk2
@ ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) )
@ sk4 ) )
| ( sk1 @ sk4 @ ( sk2 @ A @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[340:[bind(A,$thf( C )),bind(B,$thf( sk2 @ C @ sk4 ))]]) ).
thf(367,plain,
! [A: $i > $o] :
( ( sk1 @ A
@ ( sk2
@ ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) )
@ sk4 ) )
| ( sk1 @ sk4 @ ( sk2 @ A @ sk4 ) ) ),
inference(simp,[status(thm)],[341]) ).
thf(155,plain,
! [B: $i > $o,A: $i > $o] :
( ~ ( sk1 @ B @ ( sk10 @ B @ A ) )
| ~ ( B
@ ( sk2
@ ^ [C: $i] :
? [D: $i > $o] :
( ! [E: $i] :
( ( D @ E )
=> ( sk1 @ D @ E ) )
& ( D @ C ) )
@ A ) )
| ~ ( sk1 @ A @ sk3 ) ),
inference(cnfConj,[status(thm)],[153]) ).
thf(8196,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A @ sk5 )
| ~ $true
| ( sk1 @ sk9 @ B )
| ( ( sk9
@ ( sk2
@ ^ [C: $i] : $false
@ sk9 ) )
!= ( sk9 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[7661,7442]) ).
thf(8197,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A @ sk5 )
| ( sk1 @ sk9 @ B )
| ( ( sk9
@ ( sk2
@ ^ [C: $i] : $false
@ sk9 ) )
!= ( sk9 @ B ) ) ),
inference(simp,[status(thm)],[8196]) ).
thf(8198,plain,
! [A: $i > $o] :
( ( sk1 @ A @ sk5 )
| ( sk1 @ sk9
@ ( sk2
@ ^ [B: $i] : $false
@ sk9 ) ) ),
inference(pattern_uni,[status(thm)],[8197:[bind(A,$thf( A )),bind(B,$thf( sk2 @ ^ [C: $i] : $false @ sk9 ))]]) ).
thf(15756,plain,
! [B: $i,A: $i > $o] :
( ( sk88 @ sk39 )
| ~ $true
| ( sk1
@ ^ [C: $i] : $true
@ B )
| ( ( sk1 @ sk4 @ sk39 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[15646,10468]) ).
thf(15757,plain,
! [B: $i,A: $i > $o] :
( ( sk88 @ sk39 )
| ( sk1
@ ^ [C: $i] : $true
@ B )
| ( ( sk1 @ sk4 @ sk39 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[15756]) ).
thf(15758,plain,
( ( sk88 @ sk39 )
| ( sk1
@ ^ [A: $i] : $true
@ sk39 ) ),
inference(pattern_uni,[status(thm)],[15757:[bind(A,$thf( sk4 )),bind(B,$thf( sk39 ))]]) ).
thf(15890,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk88 @ sk39 )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ~ $true
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
!= ( sk1
@ ^ [D: $i] : $true
@ sk39 ) ) ),
inference(paramod_ordered,[status(thm)],[15758,136]) ).
thf(15891,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk88 @ sk39 )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
!= ( sk1
@ ^ [D: $i] : $true
@ sk39 ) ) ),
inference(simp,[status(thm)],[15890]) ).
thf(15897,plain,
! [A: $i > $o] :
( ( sk88 @ sk39 )
| ( sk1
@ ^ [B: $i] :
( sk1
@ ^ [C: $i] : $true
@ sk39 )
@ sk39 )
| ( A
!= ( ^ [B: $i] : $true ) ) ),
inference(pre_uni,[status(thm)],[15891:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : ^ [E: $i] : $true )),bind(C,$thf( ^ [D: $i] : sk39 ))]]) ).
thf(15898,plain,
( ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : $true
@ sk39 )
@ sk39 )
| ( sk88 @ sk39 ) ),
inference(pattern_uni,[status(thm)],[15897:[bind(A,$thf( ^ [B: $i] : $true ))]]) ).
thf(83,plain,
! [D: $i,C: $i > $o,B: $i > $o,A: $i] :
( ~ ( sk4 @ A )
| ~ $true
| ~ ( sk1 @ B @ D )
| ( sk1 @ C @ D )
| ( ( sk1 @ sk4 @ A )
!= ( C @ ( sk2 @ C @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[10,9]) ).
thf(84,plain,
! [D: $i,C: $i > $o,B: $i > $o,A: $i] :
( ~ ( sk4 @ A )
| ~ ( sk1 @ B @ D )
| ( sk1 @ C @ D )
| ( ( sk1 @ sk4 @ A )
!= ( C @ ( sk2 @ C @ B ) ) ) ),
inference(simp,[status(thm)],[83]) ).
thf(128,plain,
! [C: $i > $i,B: $i,A: $i > $o] :
( ~ ( sk4
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ sk4 @ ( C @ D ) )
@ A ) ) )
| ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [D: $i] : ( sk1 @ sk4 @ ( C @ D ) )
@ B ) ),
inference(pre_uni,[status(thm)],[84:[bind(A,$thf( F @ ( sk2 @ ^ [F: $i] : ( sk1 @ sk4 @ ( F @ F ) ) @ B ) )),bind(B,$thf( B )),bind(C,$thf( ^ [F: $i] : ( sk1 @ sk4 @ ( F @ F ) ) )),bind(D,$thf( D ))]]) ).
thf(135,plain,
! [C: $i > $i,B: $i,A: $i > $o] :
( ~ ( sk4
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ sk4 @ ( C @ D ) )
@ A ) ) )
| ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [D: $i] : ( sk1 @ sk4 @ ( C @ D ) )
@ B ) ),
inference(simp,[status(thm)],[128]) ).
thf(7469,plain,
! [A: $i] :
( ~ ( sk9 @ A )
| ~ $true
| ( ( sk1 @ sk9 @ A )
!= ( sk1
@ ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) )
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[7442,6]) ).
thf(7470,plain,
! [A: $i] :
( ~ ( sk9 @ A )
| ( ( sk1 @ sk9 @ A )
!= ( sk1
@ ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) )
@ sk3 ) ) ),
inference(simp,[status(thm)],[7469]) ).
thf(7492,plain,
! [A: $i] :
( ~ ( sk9 @ A )
| ( sk9
!= ( ^ [B: $i] :
? [C: $i > $o] :
( ! [D: $i] :
( ( C @ D )
=> ( sk1 @ C @ D ) )
& ( C @ B ) ) ) )
| ( A != sk3 ) ),
inference(simp,[status(thm)],[7470]) ).
thf(7507,plain,
( ~ ( sk9 @ sk3 )
| ( sk9
!= ( ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) ) ) ) ),
inference(simp,[status(thm)],[7492]) ).
thf(1645,plain,
! [B: $i > $o,A: $i > $o] :
( ( sk4 @ ( sk2 @ A @ sk4 ) )
| ( sk1 @ A @ ( sk2 @ B @ sk4 ) )
| ~ $true
| ( ( sk1 @ B @ sk3 )
!= ( sk1
@ ^ [C: $i] : $false
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[244,1522]) ).
thf(1646,plain,
! [B: $i > $o,A: $i > $o] :
( ( sk4 @ ( sk2 @ A @ sk4 ) )
| ( sk1 @ A @ ( sk2 @ B @ sk4 ) )
| ( ( sk1 @ B @ sk3 )
!= ( sk1
@ ^ [C: $i] : $false
@ sk3 ) ) ),
inference(simp,[status(thm)],[1645]) ).
thf(1647,plain,
! [A: $i > $o] :
( ( sk4 @ ( sk2 @ A @ sk4 ) )
| ( sk1 @ A
@ ( sk2
@ ^ [B: $i] : $false
@ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[1646:[bind(A,$thf( A )),bind(B,$thf( ^ [C: $i] : $false ))]]) ).
thf(15873,plain,
! [A: $i > $o] :
( ( sk88 @ sk39 )
| ~ $true
| ( sk1 @ A @ sk3 )
| ( ( A @ ( sk2 @ A @ sk4 ) )
!= ( sk1
@ ^ [B: $i] : $true
@ sk39 ) ) ),
inference(paramod_ordered,[status(thm)],[15758,140]) ).
thf(15874,plain,
! [A: $i > $o] :
( ( sk88 @ sk39 )
| ( sk1 @ A @ sk3 )
| ( ( A @ ( sk2 @ A @ sk4 ) )
!= ( sk1
@ ^ [B: $i] : $true
@ sk39 ) ) ),
inference(simp,[status(thm)],[15873]) ).
thf(15903,plain,
( ( sk88 @ sk39 )
| ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : $true
@ sk39 )
@ sk3 ) ),
inference(pre_uni,[status(thm)],[15874:[bind(A,$thf( ^ [B: $i] : ( sk1 @ ^ [C: $i] : $true @ sk39 ) ))]]) ).
thf(19583,plain,
( ( sk88 @ sk39 )
| ~ $true
| ( ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : $true
@ sk39 )
@ sk3 )
!= ( sk1
@ ^ [A: $i] : $false
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[15903,1522]) ).
thf(19584,plain,
( ( sk88 @ sk39 )
| ( ( sk1
@ ^ [A: $i] :
( sk1
@ ^ [B: $i] : $true
@ sk39 )
@ sk3 )
!= ( sk1
@ ^ [A: $i] : $false
@ sk3 ) ) ),
inference(simp,[status(thm)],[19583]) ).
thf(19827,plain,
( ( sk88 @ sk39 )
| ( ( ^ [A: $i] :
( sk1
@ ^ [B: $i] : $true
@ sk39 ) )
!= ( ^ [A: $i] : $false ) )
| ( sk3 != sk3 ) ),
inference(simp,[status(thm)],[19584]) ).
thf(19910,plain,
( ( sk88 @ sk39 )
| ( ( ^ [A: $i] :
( sk1
@ ^ [B: $i] : $true
@ sk39 ) )
!= ( ^ [A: $i] : $false ) ) ),
inference(simp,[status(thm)],[19827]) ).
thf(112,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ~ ( E @ ( sk2 @ E @ D ) )
| ~ $true
| ( sk1 @ E @ F )
| ( ( sk1 @ B @ C )
!= ( sk1 @ D @ F ) ) ),
inference(paramod_ordered,[status(thm)],[8,9]) ).
thf(113,plain,
! [F: $i,E: $i > $o,D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ~ ( E @ ( sk2 @ E @ D ) )
| ( sk1 @ E @ F )
| ( ( sk1 @ B @ C )
!= ( sk1 @ D @ F ) ) ),
inference(simp,[status(thm)],[112]) ).
thf(114,plain,
! [D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ~ ( D @ ( sk2 @ D @ B ) )
| ( sk1 @ D @ C ) ),
inference(pattern_uni,[status(thm)],[113:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( B )),bind(E,$thf( E )),bind(F,$thf( C ))]]) ).
thf(143,plain,
! [D: $i > $o,C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ~ ( D @ ( sk2 @ D @ B ) )
| ( sk1 @ D @ C ) ),
inference(simp,[status(thm)],[114]) ).
thf(8979,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ~ ( sk9 @ sk3 )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ~ $true
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1 @ sk9 @ sk33 )
!= ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[7682,136]) ).
thf(8980,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ~ ( sk9 @ sk3 )
| ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1 @ sk9 @ sk33 )
!= ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ) ),
inference(simp,[status(thm)],[8979]) ).
thf(9091,plain,
! [A: $i > $o] :
( ~ ( sk9 @ sk3 )
| ( sk1
@ ^ [B: $i] : ( sk1 @ sk9 @ sk33 )
@ sk33 )
| ( A != sk9 ) ),
inference(pre_uni,[status(thm)],[8980:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : sk9 )),bind(C,$thf( ^ [D: $i] : sk33 ))]]) ).
thf(9092,plain,
( ( sk1
@ ^ [A: $i] : ( sk1 @ sk9 @ sk33 )
@ sk33 )
| ~ ( sk9 @ sk3 ) ),
inference(pattern_uni,[status(thm)],[9091:[bind(A,$thf( sk9 ))]]) ).
thf(7374,plain,
( ~ $true
| ( ( sk4
@ ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 ) )
!= ( sk4 @ sk5 ) ) ),
inference(paramod_ordered,[status(thm)],[165,7343]) ).
thf(7375,plain,
( ( sk4
@ ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 ) )
!= ( sk4 @ sk5 ) ),
inference(simp,[status(thm)],[7374]) ).
thf(7399,plain,
( ( sk2
@ ^ [A: $i] :
? [B: $i > $o] :
( ! [C: $i] :
( ( B @ C )
=> ( sk1 @ B @ C ) )
& ( B @ A ) )
@ sk4 )
!= sk5 ),
inference(simp,[status(thm)],[7375]) ).
thf(149,plain,
! [D: $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( C
@ ( sk2
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ A ) )
| ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ B ) ),
inference(cnfConj,[status(thm)],[148]) ).
thf(151,plain,
! [D: $i > $o,C: $i > $o,B: $i,A: $i > $o] :
( ~ ( C
@ ( sk2
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ A ) )
| ~ ( sk1 @ A @ B )
| ( sk1
@ ^ [E: $i] :
( ( C @ E )
| ( D @ E ) )
@ B ) ),
inference(simp,[status(thm)],[149]) ).
thf(85,plain,
! [D: $i,C: $i > $o,B: $i > $o,A: $i] :
( ~ ( sk4 @ A )
| ~ ( C @ ( sk2 @ C @ B ) )
| ~ $true
| ( sk1 @ C @ D )
| ( ( sk1 @ sk4 @ A )
!= ( sk1 @ B @ D ) ) ),
inference(paramod_ordered,[status(thm)],[10,9]) ).
thf(86,plain,
! [D: $i,C: $i > $o,B: $i > $o,A: $i] :
( ~ ( sk4 @ A )
| ~ ( C @ ( sk2 @ C @ B ) )
| ( sk1 @ C @ D )
| ( ( sk1 @ sk4 @ A )
!= ( sk1 @ B @ D ) ) ),
inference(simp,[status(thm)],[85]) ).
thf(87,plain,
! [B: $i > $o,A: $i] :
( ~ ( sk4 @ A )
| ~ ( B @ ( sk2 @ B @ sk4 ) )
| ( sk1 @ B @ A ) ),
inference(pattern_uni,[status(thm)],[86:[bind(A,$thf( A )),bind(B,$thf( sk4 )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(146,plain,
! [B: $i > $o,A: $i] :
( ~ ( sk4 @ A )
| ~ ( B @ ( sk2 @ B @ sk4 ) )
| ( sk1 @ B @ A ) ),
inference(simp,[status(thm)],[87]) ).
thf(42,plain,
! [C: $i,B: $i > $o,A: $i > $o] :
( ( A @ ( sk2 @ B @ A ) )
| ~ ( sk1 @ A @ C )
| ( ( sk1 @ B @ C )
!= ( A @ ( sk2 @ B @ A ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[8]) ).
thf(47,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk1
@ ( B
@ ( sk2 @ A
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) ) ) )
@ ( C
@ ( sk2 @ A
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) ) ) ) )
| ~ ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2 @ A
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) ) ) ) )
| ( A
!= ( B
@ ( sk2 @ A
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[42:[bind(A,$thf( ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) ) )),bind(B,$thf( B )),bind(C,$thf( E @ ( sk2 @ B @ ^ [F: $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) ) ) ))]]) ).
thf(48,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ~ ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2 @ A
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) ) ) ) )
| ( sk1
@ ( B
@ ( sk2 @ A
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) ) ) )
@ ( C
@ ( sk2 @ A
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) ) ) ) )
| ( A
!= ( B
@ ( sk2 @ A
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[47:[]]) ).
thf(51,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ~ ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2 @ A
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) ) ) ) )
| ( sk1
@ ( B
@ ( sk2 @ A
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) ) ) )
@ ( C
@ ( sk2 @ A
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) ) ) ) )
| ( A
!= ( B
@ ( sk2 @ A
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) ) ) ) ) ),
inference(simp,[status(thm)],[48]) ).
thf(15749,plain,
! [A: $i > $o] :
( ( sk88 @ sk39 )
| ~ $true
| ( sk1 @ A @ sk3 )
| ( ( A @ ( sk2 @ A @ sk4 ) )
!= ( sk1 @ sk4 @ sk39 ) ) ),
inference(paramod_ordered,[status(thm)],[15646,140]) ).
thf(15750,plain,
! [A: $i > $o] :
( ( sk88 @ sk39 )
| ( sk1 @ A @ sk3 )
| ( ( A @ ( sk2 @ A @ sk4 ) )
!= ( sk1 @ sk4 @ sk39 ) ) ),
inference(simp,[status(thm)],[15749]) ).
thf(15781,plain,
( ( sk88 @ sk39 )
| ( sk1
@ ^ [A: $i] : ( sk1 @ sk4 @ sk39 )
@ sk3 ) ),
inference(pre_uni,[status(thm)],[15750:[bind(A,$thf( ^ [B: $i] : ( sk1 @ sk4 @ sk39 ) ))]]) ).
thf(16329,plain,
! [A: $i] :
( ~ $true
| ( sk1 @ sk32 @ A )
| ( ( sk32 @ sk5 )
!= ( sk32 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[7405,7404]) ).
thf(16330,plain,
! [A: $i] :
( ( sk1 @ sk32 @ A )
| ( ( sk32 @ sk5 )
!= ( sk32 @ A ) ) ),
inference(simp,[status(thm)],[16329]) ).
thf(16331,plain,
sk1 @ sk32 @ sk5,
inference(pattern_uni,[status(thm)],[16330:[bind(A,$thf( sk5 ))]]) ).
thf(13524,plain,
( ~ ( sk9 @ sk3 )
| ~ $true
| ( ( sk1
@ ^ [A: $i] : ( sk9 @ sk33 )
@ sk3 )
!= ( sk1
@ ^ [A: $i] : $false
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[11136,1522]) ).
thf(13525,plain,
( ~ ( sk9 @ sk3 )
| ( ( sk1
@ ^ [A: $i] : ( sk9 @ sk33 )
@ sk3 )
!= ( sk1
@ ^ [A: $i] : $false
@ sk3 ) ) ),
inference(simp,[status(thm)],[13524]) ).
thf(13603,plain,
( ~ ( sk9 @ sk3 )
| ( ( ^ [A: $i] : ( sk9 @ sk33 ) )
!= ( ^ [A: $i] : $false ) )
| ( sk3 != sk3 ) ),
inference(simp,[status(thm)],[13525]) ).
thf(13646,plain,
( ~ ( sk9 @ sk3 )
| ( ( ^ [A: $i] : ( sk9 @ sk33 ) )
!= ( ^ [A: $i] : $false ) ) ),
inference(simp,[status(thm)],[13603]) ).
thf(8955,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ~ $true
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1 @ sk4 @ sk17 )
!= ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1714,136]) ).
thf(8956,plain,
! [C: $i > $i,B: $i > $i > $o,A: $i > $o] :
( ( sk1
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( A
!= ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) )
| ( ( sk1 @ sk4 @ sk17 )
!= ( sk1
@ ( B
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) )
@ ( C
@ ( sk2
@ ^ [D: $i] : ( sk1 @ ( B @ D ) @ ( C @ D ) )
@ A ) ) ) ) ),
inference(simp,[status(thm)],[8955]) ).
thf(9053,plain,
! [A: $i > $o] :
( ( sk1
@ ^ [B: $i] : ( sk1 @ sk4 @ sk17 )
@ sk17 )
| ( A != sk4 ) ),
inference(pre_uni,[status(thm)],[8956:[bind(A,$thf( A )),bind(B,$thf( ^ [D: $i] : sk4 )),bind(C,$thf( ^ [D: $i] : sk17 ))]]) ).
thf(9054,plain,
( sk1
@ ^ [A: $i] : ( sk1 @ sk4 @ sk17 )
@ sk17 ),
inference(pattern_uni,[status(thm)],[9053:[bind(A,$thf( sk4 ))]]) ).
thf(9198,plain,
( sk1
@ ^ [A: $i] : $true
@ sk17 ),
inference(rewrite,[status(thm)],[9054,1714]) ).
thf(17248,plain,
( ( sk88 @ sk39 )
| ~ $true
| ( ( sk1
@ ^ [A: $i] : ( sk1 @ sk4 @ sk39 )
@ sk3 )
!= ( sk1
@ ^ [A: $i] : $false
@ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[15781,1522]) ).
thf(17249,plain,
( ( sk88 @ sk39 )
| ( ( sk1
@ ^ [A: $i] : ( sk1 @ sk4 @ sk39 )
@ sk3 )
!= ( sk1
@ ^ [A: $i] : $false
@ sk3 ) ) ),
inference(simp,[status(thm)],[17248]) ).
thf(17440,plain,
( ( sk88 @ sk39 )
| ( ( ^ [A: $i] : ( sk1 @ sk4 @ sk39 ) )
!= ( ^ [A: $i] : $false ) )
| ( sk3 != sk3 ) ),
inference(simp,[status(thm)],[17249]) ).
thf(17484,plain,
( ( sk88 @ sk39 )
| ( ( ^ [A: $i] : ( sk1 @ sk4 @ sk39 ) )
!= ( ^ [A: $i] : $false ) ) ),
inference(simp,[status(thm)],[17440]) ).
thf(17119,plain,
! [B: $i,A: $i > $o] :
( ~ $true
| ( sk1 @ A @ B )
| ( ( sk1 @ sk32 @ sk5 )
!= ( sk1
@ ^ [C: $i] : $false
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[16331,58]) ).
thf(17120,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A @ B )
| ( ( sk1 @ sk32 @ sk5 )
!= ( sk1
@ ^ [C: $i] : $false
@ B ) ) ),
inference(simp,[status(thm)],[17119]) ).
thf(17134,plain,
! [B: $i,A: $i > $o] :
( ( sk1 @ A @ B )
| ( sk32
!= ( ^ [C: $i] : $false ) )
| ( sk5 != B ) ),
inference(simp,[status(thm)],[17120]) ).
thf(17167,plain,
! [A: $i > $o] :
( ( sk1 @ A @ sk5 )
| ( sk32
!= ( ^ [B: $i] : $false ) ) ),
inference(simp,[status(thm)],[17134]) ).
thf(25707,plain,
$false,
inference(e,[status(thm)],[7569,1656,11360,145,127,11350,11353,11266,1793,16437,1522,10927,10,7405,142,15776,7343,21935,52,1709,7349,9360,11200,17562,57,7509,9362,152,1714,211,61,11136,6,7393,10561,1708,192,165,7565,21,137,22073,9,53,141,19478,7468,6164,7404,7682,7661,244,7397,15646,1784,59,17686,54,10279,9047,21978,7,11406,367,140,155,8198,15898,135,3,12341,7507,1647,19910,154,143,17589,9279,10595,9092,15903,7570,10468,55,8,58,7399,151,146,51,183,1757,136,15781,16331,13646,9198,17177,15,15758,17484,17167,7442]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV245^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21 % Computer : n019.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Tue Sep 29 15:27:03 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.06/0.83 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.22/1.02 % [INFO] Parsing done (190ms).
% 1.48/1.03 % [INFO] Running in sequential loop mode.
% 2.01/1.45 % [INFO] eprover registered as external prover.
% 2.01/1.45 % [INFO] Scanning for conjecture ...
% 2.22/1.55 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.22/1.59 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.22/1.59 % [INFO] Problem is higher-order (TPTP THF).
% 2.22/1.59 % [INFO] Type checking passed.
% 2.39/1.60 % [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 ...
% 152.06/44.72 % External prover 'e' found a proof!
% 152.06/44.72 % [INFO] Killing All external provers ...
% 152.06/44.72 % Time passed: 44340ms (effective reasoning time: 43678ms)
% 152.06/44.72 % 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)>
% 152.06/44.72 % Axioms used in derivation (0):
% 152.06/44.72 % No. of inferences in proof: 387
% 152.06/44.72 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 44340 ms resp. 43678 ms w/o parsing
% 153.81/45.15 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 153.81/45.15 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------