%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEV094^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 : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:36:50 AM UTC 2026
% Result : Theorem 86.17s 18.42s
% Output : Refutation 74.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 8
% Syntax : Number of formulae : 734 ( 117 unt; 0 typ; 7 def)
% Number of atoms : 2697 ( 758 equ; 0 cnn)
% Maximal formula atoms : 28 ( 3 avg)
% Number of connectives : 8481 (1367 ~;1040 |; 60 &;5971 @)
% ( 0 <=>; 43 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 425 ( 425 >; 0 *; 0 +; 0 <<)
% Number of symbols : 25 ( 22 usr; 16 con; 0-2 aty)
% Number of variables : 2458 (1909 ^; 520 !; 22 ?;2458 :)
% ( 0 !>; 0 ?*; 0 @-; 7 @+)
% Comments :
%------------------------------------------------------------------------------
thf(a_type,type,
a: $tType ).
thf(sk1_decl,type,
sk1: a > $o ).
thf(sk2_decl,type,
sk2: a > $o ).
thf(sk3_decl,type,
sk3: a > a ).
thf(sk4_decl,type,
sk4: a > a ).
thf(sk5_decl,type,
sk5: ( a > a ) > $o ).
thf(sk6_decl,type,
sk6: ( a > a ) > a ).
thf(sk7_decl,type,
sk7: ( a > a ) > a ).
thf(sk8_decl,type,
sk8: a > ( a > a ) > a ).
thf(sk11_decl,type,
sk11: a ).
thf(sk12_decl,type,
sk12: a ).
thf(sk13_decl,type,
sk13: a ).
thf(sk14_decl,type,
sk14: a ).
thf(sk15_decl,type,
sk15: a ).
thf(sk16_decl,type,
sk16: a ).
thf(sk17_decl,type,
sk17: a ).
thf(sk19_decl,type,
sk19: a ).
thf(sk20_decl,type,
sk20: a ).
thf(sk21_decl,type,
sk21: a ).
thf(sk22_decl,type,
sk22: a ).
thf(sk23_decl,type,
sk23: a ).
thf(sk24_decl,type,
sk24: a ).
thf(sk25_decl,type,
sk25: a ).
thf(sk1_def,definition,
( sk1
= ( @+[A: a > $o] :
~ ! [B: a > $o] :
( ? [C: a > a] :
( ! [D: a] :
( ( A @ D )
=> ( B @ ( C @ D ) ) )
& ! [D: a] :
( ( B @ D )
=> ? [E: a] :
( ( A @ E )
& ( D
= ( C @ E ) )
& ! [F: a] :
( ( ( A @ F )
& ( D
= ( C @ F ) ) )
=> ( F = E ) ) ) ) )
=> ? [C: a > a] :
( ! [D: a] :
( ( B @ D )
=> ( A @ ( C @ D ) ) )
& ! [D: a] :
( ( A @ D )
=> ? [E: a] :
( ( B @ E )
& ( D
= ( C @ E ) )
& ! [F: a] :
( ( ( B @ F )
& ( D
= ( C @ F ) ) )
=> ( F = E ) ) ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: a > $o] :
~ ( ? [B: a > a] :
( ! [C: a] :
( ( sk1 @ C )
=> ( A @ ( B @ C ) ) )
& ! [C: a] :
( ( A @ C )
=> ? [D: a] :
( ( sk1 @ D )
& ( C
= ( B @ D ) )
& ! [E: a] :
( ( ( sk1 @ E )
& ( C
= ( B @ E ) ) )
=> ( E = D ) ) ) ) )
=> ? [B: a > a] :
( ! [C: a] :
( ( A @ C )
=> ( sk1 @ ( B @ C ) ) )
& ! [C: a] :
( ( sk1 @ C )
=> ? [D: a] :
( ( A @ D )
& ( C
= ( B @ D ) )
& ! [E: a] :
( ( ( A @ E )
& ( C
= ( B @ E ) ) )
=> ( E = D ) ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: a > a] :
( ! [B: a] :
( ( sk1 @ B )
=> ( sk2 @ ( A @ B ) ) )
& ! [B: a] :
( ( sk2 @ B )
=> ? [C: a] :
( ( sk1 @ C )
& ( B
= ( A @ C ) )
& ! [D: a] :
( ( ( sk1 @ D )
& ( B
= ( A @ D ) ) )
=> ( D = C ) ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: a] :
@+[B: a] :
( ( sk1 @ B )
& ( A
= ( sk3 @ B ) )
& ! [C: a] :
( ( ( sk1 @ C )
& ( A
= ( sk3 @ C ) ) )
=> ( C = B ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: a > a] :
@+[B: a] :
~ ( ( sk2 @ B )
=> ( sk1 @ ( A @ B ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: a > a] :
@+[B: a] :
~ ( ( sk1 @ B )
=> ? [C: a] :
( ( sk2 @ C )
& ( B
= ( A @ C ) )
& ! [D: a] :
( ( ( sk2 @ D )
& ( B
= ( A @ D ) ) )
=> ( D = C ) ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: a,B: a > a] :
@+[C: a] :
~ ( ( ( sk2 @ C )
& ( ( sk7 @ B )
= ( B @ C ) ) )
=> ( C = A ) ) ) ) ).
thf(1,conjecture,
! [A: a > $o,B: a > $o] :
( ? [C: a > a] :
( ! [D: a] :
( ( A @ D )
=> ( B @ ( C @ D ) ) )
& ! [D: a] :
( ( B @ D )
=> ? [E: a] :
( ( A @ E )
& ( D
= ( C @ E ) )
& ! [F: a] :
( ( ( A @ F )
& ( D
= ( C @ F ) ) )
=> ( F = E ) ) ) ) )
=> ? [C: a > a] :
( ! [D: a] :
( ( B @ D )
=> ( A @ ( C @ D ) ) )
& ! [D: a] :
( ( A @ D )
=> ? [E: a] :
( ( B @ E )
& ( D
= ( C @ E ) )
& ! [F: a] :
( ( ( B @ F )
& ( D
= ( C @ F ) ) )
=> ( F = E ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cEQP1_1B_pme) ).
thf(2,negated_conjecture,
~ ! [A: a > $o,B: a > $o] :
( ? [C: a > a] :
( ! [D: a] :
( ( A @ D )
=> ( B @ ( C @ D ) ) )
& ! [D: a] :
( ( B @ D )
=> ? [E: a] :
( ( A @ E )
& ( D
= ( C @ E ) )
& ! [F: a] :
( ( ( A @ F )
& ( D
= ( C @ F ) ) )
=> ( F = E ) ) ) ) )
=> ? [C: a > a] :
( ! [D: a] :
( ( B @ D )
=> ( A @ ( C @ D ) ) )
& ! [D: a] :
( ( A @ D )
=> ? [E: a] :
( ( B @ E )
& ( D
= ( C @ E ) )
& ! [F: a] :
( ( ( B @ F )
& ( D
= ( C @ F ) ) )
=> ( F = E ) ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ! [A: a > $o,B: a > $o] :
( ? [C: a > a] :
( ! [D: a] :
( ( A @ D )
=> ( B @ ( C @ D ) ) )
& ! [D: a] :
( ( B @ D )
=> ? [E: a] :
( ( A @ E )
& ( D
= ( C @ E ) )
& ! [F: a] :
( ( ( A @ F )
& ( D
= ( C @ F ) ) )
=> ( F = E ) ) ) ) )
=> ? [C: a > a] :
( ! [D: a] :
( ( B @ D )
=> ( A @ ( C @ D ) ) )
& ! [D: a] :
( ( A @ D )
=> ? [E: a] :
( ( B @ E )
& ( D
= ( C @ E ) )
& ! [F: a] :
( ( ( B @ F )
& ( D
= ( C @ F ) ) )
=> ( F = E ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
! [E: a,D: a > a,C: a,B: a,A: a] :
( ( ~ ( sk1 @ A )
| ( sk2 @ ( sk3 @ A ) ) )
& ( ~ ( sk2 @ B )
| ( sk1 @ ( sk4 @ B ) ) )
& ( ~ ( sk2 @ B )
| ( B
= ( sk3 @ ( sk4 @ B ) ) ) )
& ( ~ ( sk2 @ B )
| ~ ( sk1 @ C )
| ( B
!= ( sk3 @ C ) )
| ( C
= ( sk4 @ B ) ) )
& ( ( sk2 @ ( sk6 @ D ) )
| ~ ( sk5 @ D ) )
& ( ~ ( sk1 @ ( D @ ( sk6 @ D ) ) )
| ~ ( sk5 @ D ) )
& ( ( sk5 @ D )
| ( sk1 @ ( sk7 @ D ) ) )
& ( ( sk5 @ D )
| ~ ( sk2 @ E )
| ( ( sk7 @ D )
!= ( D @ E ) )
| ( sk2 @ ( sk8 @ E @ D ) ) )
& ( ( sk5 @ D )
| ~ ( sk2 @ E )
| ( ( sk7 @ D )
!= ( D @ E ) )
| ( ( sk7 @ D )
= ( D @ ( sk8 @ E @ D ) ) ) )
& ( ( sk5 @ D )
| ~ ( sk2 @ E )
| ( ( sk7 @ D )
!= ( D @ E ) )
| ( ( sk8 @ E @ D )
!= E ) ) ),
inference(cnf,[status(esa)],[3]) ).
thf(6,plain,
! [A: a] :
( ~ ( sk1 @ A )
| ( sk2 @ ( sk3 @ A ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(14,plain,
! [A: a] :
( ~ ( sk2 @ A )
| ( sk1 @ ( sk4 @ A ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(19,plain,
! [A: a] :
( ~ ( sk2 @ A )
| ( sk1 @ ( sk4 @ A ) ) ),
inference(simp,[status(thm)],[14]) ).
thf(7,plain,
! [A: a > a] :
( ~ ( sk1 @ ( A @ ( sk6 @ A ) ) )
| ~ ( sk5 @ A ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(25,plain,
! [A: a > a] :
( ~ ( sk1 @ ( A @ ( sk6 @ A ) ) )
| ~ ( sk5 @ A ) ),
inference(simp,[status(thm)],[7]) ).
thf(53,plain,
! [B: a > a,A: a] :
( ~ ( sk2 @ A )
| ~ $true
| ~ ( sk5 @ B )
| ( ( sk1 @ ( sk4 @ A ) )
!= ( sk1 @ ( B @ ( sk6 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,25]) ).
thf(54,plain,
! [B: a > a,A: a] :
( ~ ( sk2 @ A )
| ~ ( sk5 @ B )
| ( ( sk1 @ ( sk4 @ A ) )
!= ( sk1 @ ( B @ ( sk6 @ B ) ) ) ) ),
inference(simp,[status(thm)],[53]) ).
thf(56,plain,
! [A: a > a] :
( ~ ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) )
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ),
inference(pre_uni,[status(thm)],[54:[bind(A,$thf( C @ ( sk6 @ ^ [D: a] : ( sk4 @ ( C @ D ) ) ) )),bind(B,$thf( ^ [D: a] : ( sk4 @ ( C @ D ) ) ))]]) ).
thf(58,plain,
! [A: a > a] :
( ~ ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) )
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ),
inference(simp,[status(thm)],[56]) ).
thf(59,plain,
! [B: a > a,A: a] :
( ~ ( sk1 @ A )
| ~ $true
| ~ ( sk5
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) )
| ( ( sk2
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) ) )
!= ( sk2 @ ( sk3 @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[6,58]) ).
thf(60,plain,
! [B: a > a,A: a] :
( ~ ( sk1 @ A )
| ~ ( sk5
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) )
| ( ( sk2
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) ) )
!= ( sk2 @ ( sk3 @ A ) ) ) ),
inference(simp,[status(thm)],[59]) ).
thf(66,plain,
! [A: a > a] :
( ~ ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) )
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ),
inference(pre_uni,[status(thm)],[60:[bind(A,$thf( C @ ( sk6 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( C @ D ) ) ) ) )),bind(B,$thf( ^ [D: a] : ( sk3 @ ( C @ D ) ) ))]]) ).
thf(69,plain,
! [A: a > a] :
( ~ ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) )
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ),
inference(simp,[status(thm)],[66]) ).
thf(8,plain,
! [B: a,A: a > a] :
( ( sk5 @ A )
| ~ ( sk2 @ B )
| ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( sk7 @ A )
= ( A @ ( sk8 @ B @ A ) ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(27,plain,
! [B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( A @ ( sk8 @ B @ A ) )
= ( sk7 @ A ) )
| ( sk5 @ A )
| ~ ( sk2 @ B ) ),
inference(lifteq,[status(thm)],[8]) ).
thf(28,plain,
! [B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( A @ ( sk8 @ B @ A ) )
= ( sk7 @ A ) )
| ( sk5 @ A )
| ~ ( sk2 @ B ) ),
inference(simp,[status(thm)],[27]) ).
thf(5,plain,
! [B: a,A: a > a] :
( ( sk5 @ A )
| ~ ( sk2 @ B )
| ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( sk8 @ B @ A )
!= B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(15,plain,
! [B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( sk8 @ B @ A )
!= B )
| ( sk5 @ A )
| ~ ( sk2 @ B ) ),
inference(lifteq,[status(thm)],[5]) ).
thf(16,plain,
! [B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( sk8 @ B @ A )
!= B )
| ( sk5 @ A )
| ~ ( sk2 @ B ) ),
inference(simp,[status(thm)],[15]) ).
thf(872,plain,
! [D: a,C: a > a,B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( sk5 @ A )
| ~ ( sk2 @ B )
| ( ( sk7 @ C )
!= ( C @ D ) )
| ( ( sk7 @ A )
!= D )
| ( sk5 @ C )
| ~ ( sk2 @ D )
| ( ( A @ ( sk8 @ B @ A ) )
!= ( sk8 @ D @ C ) ) ),
inference(paramod_ordered,[status(thm)],[28,16]) ).
thf(1195,plain,
! [A: a] :
( ( ( sk7
@ ^ [B: a] : B )
!= A )
| ( sk5
@ ^ [B: a] : B )
| ~ ( sk2 @ A )
| ( ( sk7
@ ^ [B: a] : B )
!= A )
| ( ( sk7
@ ^ [B: a] : B )
!= A )
| ( sk5
@ ^ [B: a] : B )
| ~ ( sk2 @ A ) ),
inference(pre_uni,[status(thm)],[872:[bind(A,$thf( ^ [E: a] : E )),bind(B,$thf( D )),bind(C,$thf( ^ [E: a] : E ))]]) ).
thf(1196,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( sk5
@ ^ [A: a] : A )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( sk5
@ ^ [A: a] : A ) ),
inference(pattern_uni,[status(thm)],[1195:[bind(A,$thf( sk7 @ ^ [B: a] : B ))]]) ).
thf(1358,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( sk5
@ ^ [A: a] : A ) ),
inference(simp,[status(thm)],[1196]) ).
thf(13,plain,
! [A: a > a] :
( ( sk5 @ A )
| ( sk1 @ ( sk7 @ A ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(22,plain,
! [A: a > a] :
( ( sk5 @ A )
| ( sk1 @ ( sk7 @ A ) ) ),
inference(simp,[status(thm)],[13]) ).
thf(37,plain,
! [B: a,A: a > a] :
( ( sk5 @ A )
| ~ $true
| ( sk2 @ ( sk3 @ B ) )
| ( ( sk1 @ ( sk7 @ A ) )
!= ( sk1 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[22,6]) ).
thf(38,plain,
! [B: a,A: a > a] :
( ( sk5 @ A )
| ( sk2 @ ( sk3 @ B ) )
| ( ( sk1 @ ( sk7 @ A ) )
!= ( sk1 @ B ) ) ),
inference(simp,[status(thm)],[37]) ).
thf(39,plain,
! [A: a > a] :
( ( sk5 @ A )
| ( sk2 @ ( sk3 @ ( sk7 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[38:[bind(A,$thf( C )),bind(B,$thf( sk7 @ C ))]]) ).
thf(40,plain,
! [A: a > a] :
( ( sk5 @ A )
| ( sk2 @ ( sk3 @ ( sk7 @ A ) ) ) ),
inference(simp,[status(thm)],[39]) ).
thf(11,plain,
! [A: a > a] :
( ( sk2 @ ( sk6 @ A ) )
| ~ ( sk5 @ A ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(26,plain,
! [A: a > a] :
( ( sk2 @ ( sk6 @ A ) )
| ~ ( sk5 @ A ) ),
inference(simp,[status(thm)],[11]) ).
thf(64,plain,
! [B: a > a,A: a > a] :
( ~ ( sk5 @ A )
| ~ $true
| ~ ( sk5
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) )
| ( ( sk2 @ ( sk6 @ A ) )
!= ( sk2
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[26,58]) ).
thf(65,plain,
! [B: a > a,A: a > a] :
( ~ ( sk5 @ A )
| ~ ( sk5
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) )
| ( ( sk2 @ ( sk6 @ A ) )
!= ( sk2
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[64]) ).
thf(68,plain,
( ~ ( sk5 @ sk4 )
| ~ ( sk5 @ sk4 ) ),
inference(pre_uni,[status(thm)],[65:[bind(A,$thf( sk4 )),bind(B,$thf( ^ [C: a] : C ))]]) ).
thf(71,plain,
~ ( sk5 @ sk4 ),
inference(simp,[status(thm)],[68]) ).
thf(91,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5 @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[22,71]) ).
thf(92,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5 @ sk4 ) ) ),
inference(simp,[status(thm)],[91]) ).
thf(93,plain,
sk1 @ ( sk7 @ sk4 ),
inference(pattern_uni,[status(thm)],[92:[bind(A,$thf( sk4 ))]]) ).
thf(97,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5 @ A )
| ( ( sk1 @ ( sk7 @ sk4 ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[93,25]) ).
thf(98,plain,
! [A: a > a] :
( ~ ( sk5 @ A )
| ( ( sk1 @ ( sk7 @ sk4 ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[97]) ).
thf(102,plain,
~ ( sk5
@ ^ [A: a] : ( sk7 @ sk4 ) ),
inference(pre_uni,[status(thm)],[98:[bind(A,$thf( ^ [B: a] : ( sk7 @ sk4 ) ))]]) ).
thf(132,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,102]) ).
thf(133,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[132]) ).
thf(134,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) ),
inference(pattern_uni,[status(thm)],[133:[bind(A,$thf( ^ [B: a] : ( sk7 @ sk4 ) ))]]) ).
thf(170,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[134,58]) ).
thf(171,plain,
! [A: a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[170]) ).
thf(175,plain,
~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ) ),
inference(pre_uni,[status(thm)],[171:[bind(A,$thf( ^ [B: a] : ( sk3 @ ( sk7 @ ^ [C: a] : ( sk7 @ sk4 ) ) ) ))]]) ).
thf(1837,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,175]) ).
thf(1838,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1837]) ).
thf(1879,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1838]) ).
thf(51,plain,
! [B: a > a,A: a > a] :
( ( sk5 @ A )
| ~ $true
| ~ ( sk5 @ B )
| ( ( sk1 @ ( sk7 @ A ) )
!= ( sk1 @ ( B @ ( sk6 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,25]) ).
thf(52,plain,
! [B: a > a,A: a > a] :
( ( sk5 @ A )
| ~ ( sk5 @ B )
| ( ( sk1 @ ( sk7 @ A ) )
!= ( sk1 @ ( B @ ( sk6 @ B ) ) ) ) ),
inference(simp,[status(thm)],[51]) ).
thf(55,plain,
! [A: a > a > a] :
( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
| ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ),
inference(pre_uni,[status(thm)],[52:[bind(A,$thf( C @ ( sk6 @ ^ [D: a] : ( sk7 @ ( C @ D ) ) ) )),bind(B,$thf( ^ [D: a] : ( sk7 @ ( C @ D ) ) ))]]) ).
thf(57,plain,
! [A: a > a > a] :
( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
| ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ),
inference(simp,[status(thm)],[55]) ).
thf(79,plain,
! [B: a > a,A: a > a] :
( ( sk5 @ A )
| ~ $true
| ~ ( sk5
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
!= ( sk2
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,58]) ).
thf(80,plain,
! [B: a > a,A: a > a] :
( ( sk5 @ A )
| ~ ( sk5
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
!= ( sk2
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[79]) ).
thf(87,plain,
! [A: a > a > a] :
( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ( A @ B ) ) ) ) ) ) )
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ( A @ B ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[80:[bind(A,$thf( D @ ( sk6 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk7 @ ( D @ D ) ) ) ) ) )),bind(B,$thf( ^ [D: a] : ( sk3 @ ( sk7 @ ( D @ D ) ) ) ))]]) ).
thf(89,plain,
! [A: a > a > a] :
( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ( A @ B ) ) ) ) ) ) )
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ( A @ B ) ) ) ) ) ),
inference(simp,[status(thm)],[87]) ).
thf(67,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk6 @ ( A @ B ) ) ) ) ) )
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk6 @ ( A @ B ) ) ) ) ),
inference(pre_uni,[status(thm)],[65:[bind(A,$thf( C @ ( sk6 @ ^ [D: a] : ( sk4 @ ( sk6 @ ( C @ D ) ) ) ) )),bind(B,$thf( ^ [D: a] : ( sk6 @ ( C @ D ) ) ))]]) ).
thf(70,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk6 @ ( A @ B ) ) ) ) ) )
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk6 @ ( A @ B ) ) ) ) ),
inference(simp,[status(thm)],[67]) ).
thf(7138,plain,
! [B: a > a > a,A: a > a > a] :
( ~ ( sk5
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ( A @ C ) ) ) ) )
| ~ ( sk5
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( sk6 @ ( B @ C ) ) ) ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ( A @ C ) ) ) ) ) ) )
!= ( sk5
@ ^ [C: a] : ( sk4 @ ( sk6 @ ( B @ C ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[89,70]) ).
thf(7139,plain,
! [B: a > a > a,A: a > a > a] :
( ~ ( sk5
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ( A @ C ) ) ) ) )
| ~ ( sk5
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( sk6 @ ( B @ C ) ) ) ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ( A @ C ) ) ) ) ) ) )
!= ( sk5
@ ^ [C: a] : ( sk4 @ ( sk6 @ ( B @ C ) ) ) ) ) ),
inference(simp,[status(thm)],[7138]) ).
thf(7199,plain,
( ~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
| ~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[7139:[bind(A,$thf( ^ [C: a] : ^ [D: a] : ( sk4 @ C ) )),bind(B,$thf( ^ [C: a] : ^ [D: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [E: a] : ( sk4 @ D ) ) ) ) ))]]) ).
thf(7244,plain,
~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ),
inference(simp,[status(thm)],[7199]) ).
thf(7255,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,7244]) ).
thf(7256,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[7255]) ).
thf(7272,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[7256:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [D: a] : ( sk4 @ C ) ) ) ) ))]]) ).
thf(4706,plain,
! [B: a > a > a,A: a > a > a] :
( ~ ( sk5
@ ^ [C: a] : ( sk7 @ ( A @ C ) ) )
| ~ ( sk5
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( sk6 @ ( B @ C ) ) ) ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [C: a] : ( sk7 @ ( A @ C ) ) ) ) )
!= ( sk5
@ ^ [C: a] : ( sk4 @ ( sk6 @ ( B @ C ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,70]) ).
thf(4707,plain,
! [B: a > a > a,A: a > a > a] :
( ~ ( sk5
@ ^ [C: a] : ( sk7 @ ( A @ C ) ) )
| ~ ( sk5
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( sk6 @ ( B @ C ) ) ) ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [C: a] : ( sk7 @ ( A @ C ) ) ) ) )
!= ( sk5
@ ^ [C: a] : ( sk4 @ ( sk6 @ ( B @ C ) ) ) ) ) ),
inference(simp,[status(thm)],[4706]) ).
thf(4742,plain,
( ~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) )
| ~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ),
inference(pre_uni,[status(thm)],[4707:[bind(A,$thf( ^ [C: a] : ^ [D: a] : ( sk4 @ C ) )),bind(B,$thf( ^ [C: a] : ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk4 @ D ) ) ))]]) ).
thf(4750,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ),
inference(simp,[status(thm)],[4742]) ).
thf(4769,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,4750]) ).
thf(4770,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ),
inference(simp,[status(thm)],[4769]) ).
thf(4771,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ),
inference(pattern_uni,[status(thm)],[4770:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ B ) ) ))]]) ).
thf(1797,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5 @ sk4 )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,71]) ).
thf(1798,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5 @ sk4 )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1797]) ).
thf(1861,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( sk4
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1798]) ).
thf(5005,plain,
( ~ $true
| ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4771,1861]) ).
thf(5006,plain,
( ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[5005]) ).
thf(5028,plain,
( ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[5006]) ).
thf(81,plain,
! [B: a,A: a > a] :
( ( sk5 @ A )
| ~ $true
| ( sk1 @ ( sk4 @ B ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[40,19]) ).
thf(82,plain,
! [B: a,A: a > a] :
( ( sk5 @ A )
| ( sk1 @ ( sk4 @ B ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[81]) ).
thf(83,plain,
! [A: a > a] :
( ( sk5 @ A )
| ( sk1 @ ( sk4 @ ( sk3 @ ( sk7 @ A ) ) ) ) ),
inference(pattern_uni,[status(thm)],[82:[bind(A,$thf( D )),bind(B,$thf( sk3 @ ( sk7 @ D ) ))]]) ).
thf(88,plain,
! [A: a > a] :
( ( sk5 @ A )
| ( sk1 @ ( sk4 @ ( sk3 @ ( sk7 @ A ) ) ) ) ),
inference(simp,[status(thm)],[83]) ).
thf(127,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,102]) ).
thf(128,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[127]) ).
thf(129,plain,
( sk1
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[128:[bind(A,$thf( ^ [B: a] : ( sk7 @ sk4 ) ))]]) ).
thf(145,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5 @ A )
| ( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[129,25]) ).
thf(146,plain,
! [A: a > a] :
( ~ ( sk5 @ A )
| ( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[145]) ).
thf(150,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ),
inference(pre_uni,[status(thm)],[146:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ sk4 ) ) ))]]) ).
thf(156,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,150]) ).
thf(157,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ),
inference(simp,[status(thm)],[156]) ).
thf(158,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ) ),
inference(pattern_uni,[status(thm)],[157:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ sk4 ) ) ))]]) ).
thf(243,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[158,19]) ).
thf(244,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[243]) ).
thf(245,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[244:[bind(A,$thf( sk3 @ ( sk7 @ ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ sk4 ) ) ) ))]]) ).
thf(479,plain,
! [A: a] :
( ~ $true
| ( sk2 @ ( sk3 @ A ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[245,6]) ).
thf(480,plain,
! [A: a] :
( ( sk2 @ ( sk3 @ A ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[479]) ).
thf(481,plain,
( sk2
@ ( sk3
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[480:[bind(A,$thf( sk4 @ ( sk3 @ ( sk7 @ ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ))]]) ).
thf(41,plain,
! [B: a,A: a > a] :
( ~ ( sk5 @ A )
| ~ $true
| ( sk1 @ ( sk4 @ B ) )
| ( ( sk2 @ ( sk6 @ A ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[26,19]) ).
thf(42,plain,
! [B: a,A: a > a] :
( ~ ( sk5 @ A )
| ( sk1 @ ( sk4 @ B ) )
| ( ( sk2 @ ( sk6 @ A ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[41]) ).
thf(43,plain,
! [A: a > a] :
( ~ ( sk5 @ A )
| ( sk1 @ ( sk4 @ ( sk6 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[42:[bind(A,$thf( C )),bind(B,$thf( sk6 @ C ))]]) ).
thf(47,plain,
! [A: a > a] :
( ~ ( sk5 @ A )
| ( sk1 @ ( sk4 @ ( sk6 @ A ) ) ) ),
inference(simp,[status(thm)],[43]) ).
thf(3124,plain,
! [A: a > a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ~ $true
| ( sk1 @ ( sk4 @ ( sk6 @ A ) ) )
| ( ( sk5
@ ^ [B: a] : B )
!= ( sk5 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,47]) ).
thf(3125,plain,
! [A: a > a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ( sk1 @ ( sk4 @ ( sk6 @ A ) ) )
| ( ( sk5
@ ^ [B: a] : B )
!= ( sk5 @ A ) ) ),
inference(simp,[status(thm)],[3124]) ).
thf(3126,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( sk1
@ ( sk4
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(pattern_uni,[status(thm)],[3125:[bind(A,$thf( ^ [B: a] : B ))]]) ).
thf(32,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A )
| ~ $true
| ( sk1 @ ( sk4 @ B ) )
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[6,19]) ).
thf(33,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A )
| ( sk1 @ ( sk4 @ B ) )
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[32]) ).
thf(34,plain,
! [A: a] :
( ~ ( sk1 @ A )
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[33:[bind(A,$thf( C )),bind(B,$thf( sk3 @ C ))]]) ).
thf(35,plain,
! [A: a] :
( ~ ( sk1 @ A )
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) ) ),
inference(simp,[status(thm)],[34]) ).
thf(3315,plain,
! [A: a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ~ $true
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3126,35]) ).
thf(3316,plain,
! [A: a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[3315]) ).
thf(3317,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( sk1
@ ( sk4
@ ( sk3
@ ( sk4
@ ( sk6
@ ^ [A: a] : A ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[3316:[bind(A,$thf( sk4 @ ( sk6 @ ^ [B: a] : B ) ))]]) ).
thf(94,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5 @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[40,71]) ).
thf(95,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5 @ sk4 ) ) ),
inference(simp,[status(thm)],[94]) ).
thf(96,plain,
sk2 @ ( sk3 @ ( sk7 @ sk4 ) ),
inference(pattern_uni,[status(thm)],[95:[bind(A,$thf( sk4 ))]]) ).
thf(1818,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] : ( sk7 @ sk4 ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,102]) ).
thf(1819,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] : ( sk7 @ sk4 ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1818]) ).
thf(1873,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] : ( sk7 @ sk4 ) )
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1819]) ).
thf(2205,plain,
( ~ $true
| ( ( ^ [A: a] : ( sk7 @ sk4 ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,1873]) ).
thf(2206,plain,
( ( ( ^ [A: a] : ( sk7 @ sk4 ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[2205]) ).
thf(2244,plain,
( ( ( ^ [A: a] : ( sk7 @ sk4 ) )
!= ( ^ [A: a] : A ) )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[2206]) ).
thf(4515,plain,
( ( ( sk7 @ sk4 )
!= sk20 )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(func_ext,[status(esa)],[2244]) ).
thf(4762,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,4750]) ).
thf(4763,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ),
inference(simp,[status(thm)],[4762]) ).
thf(4764,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[4763:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ B ) ) ))]]) ).
thf(48,plain,
! [B: a > a,A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ ( sk1 @ ( B @ ( sk6 @ B ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[22,25]) ).
thf(49,plain,
! [B: a > a,A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ ( sk1 @ ( B @ ( sk6 @ B ) ) )
| ( ( sk5 @ A )
!= ( sk5 @ B ) ) ),
inference(simp,[status(thm)],[48]) ).
thf(50,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ ( sk1 @ ( A @ ( sk6 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[49:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(4792,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[4764,50]) ).
thf(4793,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[4792]) ).
thf(4799,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ),
inference(pre_uni,[status(thm)],[4793:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ C ) ) ) ))]]) ).
thf(5064,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[4799,50]) ).
thf(5065,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[5064]) ).
thf(5069,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[5065:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk4 @ D ) ) ) ) ))]]) ).
thf(151,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,150]) ).
thf(152,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ),
inference(simp,[status(thm)],[151]) ).
thf(153,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ),
inference(pattern_uni,[status(thm)],[152:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ sk4 ) ) ))]]) ).
thf(224,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5 @ A )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[153,25]) ).
thf(225,plain,
! [A: a > a] :
( ~ ( sk5 @ A )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[224]) ).
thf(229,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ),
inference(pre_uni,[status(thm)],[225:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ sk4 ) ) ) ))]]) ).
thf(230,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,229]) ).
thf(231,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ),
inference(simp,[status(thm)],[230]) ).
thf(232,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ),
inference(pattern_uni,[status(thm)],[231:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ sk4 ) ) ) ))]]) ).
thf(394,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5 @ A )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[232,25]) ).
thf(395,plain,
! [A: a > a] :
( ~ ( sk5 @ A )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[394]) ).
thf(399,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ),
inference(pre_uni,[status(thm)],[395:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ sk4 ) ) ) ) ))]]) ).
thf(1829,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,399]) ).
thf(1830,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1829]) ).
thf(1882,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1830]) ).
thf(10,plain,
! [A: a] :
( ~ ( sk2 @ A )
| ( A
= ( sk3 @ ( sk4 @ A ) ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(17,plain,
! [A: a] :
( ( ( sk3 @ ( sk4 @ A ) )
= A )
| ~ ( sk2 @ A ) ),
inference(lifteq,[status(thm)],[10]) ).
thf(18,plain,
! [A: a] :
( ( ( sk3 @ ( sk4 @ A ) )
= A )
| ~ ( sk2 @ A ) ),
inference(simp,[status(thm)],[17]) ).
thf(203,plain,
! [B: a,A: a > a] :
( ( sk5 @ A )
| ( ( sk3 @ ( sk4 @ B ) )
= B )
| ~ $true
| ( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[40,18]) ).
thf(204,plain,
! [B: a,A: a > a] :
( ( sk5 @ A )
| ( ( sk3 @ ( sk4 @ B ) )
= B )
| ( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[203]) ).
thf(205,plain,
! [A: a > a] :
( ( sk5 @ A )
| ( ( sk3 @ ( sk4 @ ( sk3 @ ( sk7 @ A ) ) ) )
= ( sk3 @ ( sk7 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[204:[bind(A,$thf( D )),bind(B,$thf( sk3 @ ( sk7 @ D ) ))]]) ).
thf(217,plain,
! [A: a > a] :
( ( sk5 @ A )
| ( ( sk3 @ ( sk4 @ ( sk3 @ ( sk7 @ A ) ) ) )
= ( sk3 @ ( sk7 @ A ) ) ) ),
inference(simp,[status(thm)],[205]) ).
thf(1809,plain,
! [A: a > a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ~ ( sk1 @ ( A @ ( sk6 @ A ) ) )
| ~ $true
| ( ( sk5
@ ^ [B: a] : B )
!= ( sk5 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,25]) ).
thf(1810,plain,
! [A: a > a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ~ ( sk1 @ ( A @ ( sk6 @ A ) ) )
| ( ( sk5
@ ^ [B: a] : B )
!= ( sk5 @ A ) ) ),
inference(simp,[status(thm)],[1809]) ).
thf(1811,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ),
inference(pattern_uni,[status(thm)],[1810:[bind(A,$thf( ^ [B: a] : B ))]]) ).
thf(2131,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk1 @ ( sk7 @ sk4 ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[93,1811]) ).
thf(2132,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk1 @ ( sk7 @ sk4 ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[2131]) ).
thf(2195,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk7 @ sk4 )
!= ( sk6
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[2132]) ).
thf(4992,plain,
( ~ $true
| ( ( ^ [A: a] : ( sk7 @ sk4 ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4771,1873]) ).
thf(4993,plain,
( ( ( ^ [A: a] : ( sk7 @ sk4 ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[4992]) ).
thf(5037,plain,
( ( ( ^ [A: a] : ( sk7 @ sk4 ) )
!= ( ^ [A: a] : A ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4993]) ).
thf(3285,plain,
! [A: a > a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ~ $true
| ~ ( sk5 @ A )
| ( ( sk1
@ ( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3126,25]) ).
thf(3286,plain,
! [A: a > a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ~ ( sk5 @ A )
| ( ( sk1
@ ( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[3285]) ).
thf(3332,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) ) ),
inference(pre_uni,[status(thm)],[3286:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk6 @ ^ [C: a] : C ) ) ))]]) ).
thf(138,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,58]) ).
thf(139,plain,
! [A: a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[138]) ).
thf(143,plain,
~ ( sk5
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ),
inference(pre_uni,[status(thm)],[139:[bind(A,$thf( ^ [B: a] : ( sk3 @ ( sk7 @ sk4 ) ) ))]]) ).
thf(159,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,143]) ).
thf(160,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ),
inference(simp,[status(thm)],[159]) ).
thf(161,plain,
( sk1
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ),
inference(pattern_uni,[status(thm)],[160:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ))]]) ).
thf(251,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5 @ A )
| ( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[161,25]) ).
thf(252,plain,
! [A: a > a] :
( ~ ( sk5 @ A )
| ( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[251]) ).
thf(257,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ),
inference(pre_uni,[status(thm)],[252:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ))]]) ).
thf(269,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,257]) ).
thf(270,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(simp,[status(thm)],[269]) ).
thf(271,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[270:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ))]]) ).
thf(602,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5 @ A )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[271,25]) ).
thf(603,plain,
! [A: a > a] :
( ~ ( sk5 @ A )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[602]) ).
thf(608,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[603:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ))]]) ).
thf(668,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,608]) ).
thf(669,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[668]) ).
thf(670,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[669:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ))]]) ).
thf(4758,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,4750]) ).
thf(4759,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ),
inference(simp,[status(thm)],[4758]) ).
thf(4772,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ),
inference(pre_uni,[status(thm)],[4759:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ C ) ) ))]]) ).
thf(4813,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] : A )
!= ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1358,4772]) ).
thf(4814,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] : A )
!= ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ),
inference(simp,[status(thm)],[4813]) ).
thf(4818,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ),
inference(simp,[status(thm)],[4814]) ).
thf(4884,plain,
( ( ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) )
!= sk22 )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(func_ext,[status(esa)],[4818]) ).
thf(140,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[96,19]) ).
thf(141,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[140]) ).
thf(142,plain,
sk1 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[141:[bind(A,$thf( sk3 @ ( sk7 @ sk4 ) ))]]) ).
thf(4767,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] : A )
!= ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1358,4750]) ).
thf(4768,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] : A )
!= ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ),
inference(simp,[status(thm)],[4767]) ).
thf(4773,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ),
inference(simp,[status(thm)],[4768]) ).
thf(4837,plain,
( ~ $true
| ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,4773]) ).
thf(4838,plain,
( ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[4837]) ).
thf(4870,plain,
( ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4838]) ).
thf(172,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[134,19]) ).
thf(173,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[172]) ).
thf(174,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) ) ),
inference(pattern_uni,[status(thm)],[173:[bind(A,$thf( sk3 @ ( sk7 @ ^ [B: a] : ( sk7 @ sk4 ) ) ))]]) ).
thf(12,plain,
! [B: a,A: a > a] :
( ( sk5 @ A )
| ~ ( sk2 @ B )
| ( ( sk7 @ A )
!= ( A @ B ) )
| ( sk2 @ ( sk8 @ B @ A ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(23,plain,
! [B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( sk5 @ A )
| ~ ( sk2 @ B )
| ( sk2 @ ( sk8 @ B @ A ) ) ),
inference(lifteq,[status(thm)],[12]) ).
thf(24,plain,
! [B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( sk5 @ A )
| ~ ( sk2 @ B )
| ( sk2 @ ( sk8 @ B @ A ) ) ),
inference(simp,[status(thm)],[23]) ).
thf(4789,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[4764,35]) ).
thf(4790,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[4789]) ).
thf(4791,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[4790:[bind(A,$thf( sk7 @ ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ B ) ) ))]]) ).
thf(5693,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[4791,69]) ).
thf(5694,plain,
! [A: a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5693]) ).
thf(5723,plain,
~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[5694:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ))]]) ).
thf(2125,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[153,1811]) ).
thf(2126,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[2125]) ).
thf(2173,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) )
!= ( sk6
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[2126]) ).
thf(1887,plain,
( ( ( sk4 @ sk11 )
!= sk11 )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(func_ext,[status(esa)],[1861]) ).
thf(2570,plain,
( ( ( sk4 @ sk11 )
!= sk11 )
| ~ $true
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,1887]) ).
thf(2571,plain,
( ( ( sk4 @ sk11 )
!= sk11 )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[2570]) ).
thf(2603,plain,
( ( ( sk4 @ sk11 )
!= sk11 )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[2571]) ).
thf(3843,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk6
@ ^ [C: a] : C ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,3332]) ).
thf(3844,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk6
@ ^ [C: a] : C ) ) ) ) ),
inference(simp,[status(thm)],[3843]) ).
thf(3906,plain,
( ~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk6
@ ^ [C: a] : C ) ) ) )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(pre_uni,[status(thm)],[3844:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk4 @ ( sk6 @ ^ [D: a] : D ) ) ))]]) ).
thf(5287,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk6
@ ^ [C: a] : C ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,3906]) ).
thf(5288,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk6
@ ^ [C: a] : C ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[5287]) ).
thf(5306,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk6
@ ^ [C: a] : C ) ) ) )
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[5288]) ).
thf(4302,plain,
! [A: a > a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ~ $true
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) )
!= ( sk1
@ ( sk4
@ ( sk6
@ ^ [B: a] : B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3126,69]) ).
thf(4303,plain,
! [A: a > a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) )
!= ( sk1
@ ( sk4
@ ( sk6
@ ^ [B: a] : B ) ) ) ) ),
inference(simp,[status(thm)],[4302]) ).
thf(4374,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk4
@ ( sk6
@ ^ [B: a] : B ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[4303:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk6 @ ^ [C: a] : C ) ) ))]]) ).
thf(12799,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk4
@ ( sk6
@ ^ [B: a] : B ) ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,4374]) ).
thf(12800,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk4
@ ( sk6
@ ^ [B: a] : B ) ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[12799]) ).
thf(12832,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] :
( sk4
@ ( sk3
@ ( sk4
@ ( sk6
@ ^ [B: a] : B ) ) ) ) )
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[12800]) ).
thf(4774,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) )
!= ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[4764,69]) ).
thf(4775,plain,
! [A: a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) )
!= ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[4774]) ).
thf(4794,plain,
~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[4775:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ C ) ) ) ))]]) ).
thf(5737,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,4794]) ).
thf(5738,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5737]) ).
thf(5759,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[5738:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ))]]) ).
thf(119,plain,
! [C: a,B: a > a,A: a > a] :
( ~ ( sk5 @ A )
| ( ( sk7 @ B )
!= ( B @ C ) )
| ( ( sk8 @ C @ B )
!= C )
| ( sk5 @ B )
| ~ $true
| ( ( sk2 @ ( sk6 @ A ) )
!= ( sk2 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[26,16]) ).
thf(120,plain,
! [C: a,B: a > a,A: a > a] :
( ~ ( sk5 @ A )
| ( ( sk7 @ B )
!= ( B @ C ) )
| ( ( sk8 @ C @ B )
!= C )
| ( sk5 @ B )
| ( ( sk2 @ ( sk6 @ A ) )
!= ( sk2 @ C ) ) ),
inference(simp,[status(thm)],[119]) ).
thf(121,plain,
! [B: a > a,A: a > a] :
( ~ ( sk5 @ B )
| ( ( sk7 @ A )
!= ( A @ ( sk6 @ B ) ) )
| ( ( sk8 @ ( sk6 @ B ) @ A )
!= ( sk6 @ B ) )
| ( sk5 @ A ) ),
inference(pattern_uni,[status(thm)],[120:[bind(A,$thf( D )),bind(B,$thf( B )),bind(C,$thf( sk6 @ D ))]]) ).
thf(125,plain,
! [B: a > a,A: a > a] :
( ~ ( sk5 @ B )
| ( ( sk7 @ A )
!= ( A @ ( sk6 @ B ) ) )
| ( ( sk8 @ ( sk6 @ B ) @ A )
!= ( sk6 @ B ) )
| ( sk5 @ A ) ),
inference(simp,[status(thm)],[121]) ).
thf(4803,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,4772]) ).
thf(4804,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ),
inference(simp,[status(thm)],[4803]) ).
thf(4819,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ),
inference(pre_uni,[status(thm)],[4804:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk4 @ D ) ) ) ))]]) ).
thf(5196,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,4819]) ).
thf(5197,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5196]) ).
thf(5214,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[5197:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ ^ [F: a] : ( sk4 @ E ) ) ) ) ))]]) ).
thf(44,plain,
! [B: a > a,A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( sk2 @ ( sk6 @ B ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[22,26]) ).
thf(45,plain,
! [B: a > a,A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( sk2 @ ( sk6 @ B ) )
| ( ( sk5 @ A )
!= ( sk5 @ B ) ) ),
inference(simp,[status(thm)],[44]) ).
thf(46,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( sk2 @ ( sk6 @ A ) ) ),
inference(pattern_uni,[status(thm)],[45:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(3867,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,608]) ).
thf(3868,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3867]) ).
thf(3902,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[3868:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ))]]) ).
thf(1793,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,229]) ).
thf(1794,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1793]) ).
thf(1875,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) )
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1794]) ).
thf(259,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,175]) ).
thf(260,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(simp,[status(thm)],[259]) ).
thf(261,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[260:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ))]]) ).
thf(241,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[158,58]) ).
thf(242,plain,
! [A: a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[241]) ).
thf(250,plain,
~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[242:[bind(A,$thf( ^ [B: a] : ( sk3 @ ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ))]]) ).
thf(446,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,250]) ).
thf(447,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[446]) ).
thf(448,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[447:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ))]]) ).
thf(4339,plain,
! [B: a > a,A: a > a] :
( ~ ( sk5 @ A )
| ~ $true
| ~ ( sk5
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( B @ C ) ) ) )
| ( ( sk1 @ ( sk4 @ ( sk6 @ A ) ) )
!= ( sk1
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( B @ C ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[47,69]) ).
thf(4340,plain,
! [B: a > a,A: a > a] :
( ~ ( sk5 @ A )
| ~ ( sk5
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( B @ C ) ) ) )
| ( ( sk1 @ ( sk4 @ ( sk6 @ A ) ) )
!= ( sk1
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( B @ C ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[4339]) ).
thf(4350,plain,
( ~ ( sk5
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) )
| ~ ( sk5
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) ),
inference(pre_uni,[status(thm)],[4340:[bind(A,$thf( ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) )),bind(B,$thf( sk4 ))]]) ).
thf(4389,plain,
~ ( sk5
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ),
inference(simp,[status(thm)],[4350]) ).
thf(4396,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,4389]) ).
thf(4397,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) ),
inference(simp,[status(thm)],[4396]) ).
thf(4398,plain,
( sk1
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) ),
inference(pattern_uni,[status(thm)],[4397:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ))]]) ).
thf(4408,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[4398,69]) ).
thf(4409,plain,
! [A: a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[4408]) ).
thf(4432,plain,
~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[4409:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ))]]) ).
thf(4815,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,4772]) ).
thf(4816,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ),
inference(simp,[status(thm)],[4815]) ).
thf(4817,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[4816:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ C ) ) ) ))]]) ).
thf(61,plain,
! [B: a > a,A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ ( sk2
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,58]) ).
thf(62,plain,
! [B: a > a,A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ ( sk2
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) ) ),
inference(simp,[status(thm)],[61]) ).
thf(63,plain,
! [A: a > a] :
( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) )
| ~ ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[62:[bind(A,$thf( ^ [D: a] : ( sk4 @ ( C @ D ) ) )),bind(B,$thf( C ))]]) ).
thf(72,plain,
! [A: a > a] :
( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) )
| ~ ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ),
inference(simp,[status(thm)],[63]) ).
thf(5973,plain,
! [A: a > a] :
( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) )
| ~ $true
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[4817,72]) ).
thf(5974,plain,
! [A: a > a] :
( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5973]) ).
thf(6002,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[5974:[bind(A,$thf( ^ [B: a] : ( sk3 @ ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ))]]) ).
thf(7266,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] : A )
!= ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1358,7244]) ).
thf(7267,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] : A )
!= ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ) ),
inference(simp,[status(thm)],[7266]) ).
thf(7273,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ) ),
inference(simp,[status(thm)],[7267]) ).
thf(4988,plain,
( ~ $true
| ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4771,4773]) ).
thf(4989,plain,
( ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[4988]) ).
thf(5027,plain,
( ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4989]) ).
thf(4392,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,4389]) ).
thf(4393,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) ),
inference(simp,[status(thm)],[4392]) ).
thf(4406,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ),
inference(pre_uni,[status(thm)],[4393:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ))]]) ).
thf(4437,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,4406]) ).
thf(4438,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[4437]) ).
thf(4454,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[4438:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk4 @ D ) ) ) ) ))]]) ).
thf(9805,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,5759]) ).
thf(9806,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[9805]) ).
thf(9837,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[9806:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [E: a] : ( sk7 @ ^ [F: a] : ( sk4 @ E ) ) ) ) ) ) ))]]) ).
thf(1823,plain,
( ~ $true
| ( sk5
@ ^ [A: a] : A )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[134,1358]) ).
thf(1824,plain,
( ( sk5
@ ^ [A: a] : A )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[1823]) ).
thf(1858,plain,
( ( sk5
@ ^ [A: a] : A )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1824]) ).
thf(2143,plain,
( ~ $true
| ~ ( sk1
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[134,1811]) ).
thf(2144,plain,
( ~ ( sk1
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[2143]) ).
thf(2178,plain,
( ~ ( sk1
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[2144]) ).
thf(199,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A )
| ( ( sk3 @ ( sk4 @ B ) )
= B )
| ~ $true
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[6,18]) ).
thf(200,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A )
| ( ( sk3 @ ( sk4 @ B ) )
= B )
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[199]) ).
thf(201,plain,
! [A: a] :
( ~ ( sk1 @ A )
| ( ( sk3 @ ( sk4 @ ( sk3 @ A ) ) )
= ( sk3 @ A ) ) ),
inference(pattern_uni,[status(thm)],[200:[bind(A,$thf( C )),bind(B,$thf( sk3 @ C ))]]) ).
thf(216,plain,
! [A: a] :
( ~ ( sk1 @ A )
| ( ( sk3 @ ( sk4 @ ( sk3 @ A ) ) )
= ( sk3 @ A ) ) ),
inference(simp,[status(thm)],[201]) ).
thf(7261,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,7244]) ).
thf(7262,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[7261]) ).
thf(7263,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[7262:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [C: a] : ( sk4 @ B ) ) ) ) ))]]) ).
thf(73,plain,
! [B: a > a,A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ ( sk1 @ ( B @ ( sk6 @ B ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[40,25]) ).
thf(74,plain,
! [B: a > a,A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ ( sk1 @ ( B @ ( sk6 @ B ) ) )
| ( ( sk5 @ A )
!= ( sk5 @ B ) ) ),
inference(simp,[status(thm)],[73]) ).
thf(75,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ ( sk1 @ ( A @ ( sk6 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[74:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(7295,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[7263,75]) ).
thf(7296,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[7295]) ).
thf(7300,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[7296:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ))]]) ).
thf(235,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,229]) ).
thf(236,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ),
inference(simp,[status(thm)],[235]) ).
thf(237,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[236:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ sk4 ) ) ) ))]]) ).
thf(434,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[237,58]) ).
thf(435,plain,
! [A: a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[434]) ).
thf(443,plain,
~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[435:[bind(A,$thf( ^ [B: a] : ( sk3 @ ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ sk4 ) ) ) ) ) ))]]) ).
thf(4426,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[4398,50]) ).
thf(4427,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[4426]) ).
thf(4433,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[4427:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ))]]) ).
thf(5351,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[4433,35]) ).
thf(5352,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[5351]) ).
thf(5353,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[5352:[bind(A,$thf( sk7 @ ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ))]]) ).
thf(3390,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,3332]) ).
thf(3391,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[3390]) ).
thf(3419,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[3391]) ).
thf(3556,plain,
( ~ $true
| ( ( ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,3419]) ).
thf(3557,plain,
( ( ( ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[3556]) ).
thf(3593,plain,
( ( ( ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[3557]) ).
thf(5220,plain,
( ( ( sk4
@ ( sk6
@ ^ [A: a] : A ) )
!= sk23 )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(func_ext,[status(esa)],[3593]) ).
thf(3355,plain,
( ~ $true
| ~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,3332]) ).
thf(3356,plain,
( ~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[3355]) ).
thf(3421,plain,
( ~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[3356]) ).
thf(193,plain,
! [C: a,B: a > a,A: a] :
( ~ ( sk2 @ A )
| ( A
!= ( sk7 @ B ) )
| ( ( sk8 @ C @ B )
!= C )
| ( sk5 @ B )
| ~ ( sk2 @ C )
| ( ( sk3 @ ( sk4 @ A ) )
!= ( B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[18,16]) ).
thf(211,plain,
! [A: a] :
( ~ ( sk2 @ A )
| ( ( sk7 @ sk3 )
!= A )
| ( ( sk8 @ ( sk4 @ A ) @ sk3 )
!= ( sk4 @ A ) )
| ( sk5 @ sk3 )
| ~ ( sk2 @ ( sk4 @ A ) ) ),
inference(pre_uni,[status(thm)],[193:[bind(A,$thf( A )),bind(B,$thf( sk3 )),bind(C,$thf( sk4 @ A ))]]) ).
thf(221,plain,
( ~ ( sk2 @ ( sk7 @ sk3 ) )
| ( ( sk8 @ ( sk4 @ ( sk7 @ sk3 ) ) @ sk3 )
!= ( sk4 @ ( sk7 @ sk3 ) ) )
| ( sk5 @ sk3 )
| ~ ( sk2 @ ( sk4 @ ( sk7 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[211]) ).
thf(2204,plain,
( ( ( sk7 @ sk4 )
!= sk12 )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(func_ext,[status(esa)],[1873]) ).
thf(2933,plain,
( ( ( sk7 @ sk4 )
!= sk12 )
| ~ $true
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,2204]) ).
thf(2934,plain,
( ( ( sk7 @ sk4 )
!= sk12 )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[2933]) ).
thf(2982,plain,
( ( ( sk7 @ sk4 )
!= sk12 )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[2934]) ).
thf(4403,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,4389]) ).
thf(4404,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) ),
inference(simp,[status(thm)],[4403]) ).
thf(4405,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[4404:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ))]]) ).
thf(5123,plain,
! [A: a > a] :
( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) )
| ~ $true
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[4405,72]) ).
thf(5124,plain,
! [A: a > a] :
( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5123]) ).
thf(5169,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[5124:[bind(A,$thf( ^ [B: a] : ( sk3 @ ( sk7 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) ))]]) ).
thf(4401,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,4389]) ).
thf(4402,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4401]) ).
thf(4407,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) )
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4402]) ).
thf(6470,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[5069,50]) ).
thf(6471,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[6470]) ).
thf(6482,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[6471:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ ^ [F: a] : ( sk4 @ E ) ) ) ) ) ))]]) ).
thf(5049,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4799,1811]) ).
thf(5050,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[5049]) ).
thf(5070,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) )
!= ( sk6
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[5050]) ).
thf(210,plain,
! [B: a > a,A: a] :
( ~ ( sk2 @ ( B @ A ) )
| ( ( B @ A )
!= ( sk7
@ ^ [C: a] : ( sk3 @ ( sk4 @ ( B @ C ) ) ) ) )
| ( ( sk8 @ A
@ ^ [C: a] : ( sk3 @ ( sk4 @ ( B @ C ) ) ) )
!= A )
| ( sk5
@ ^ [C: a] : ( sk3 @ ( sk4 @ ( B @ C ) ) ) )
| ~ ( sk2 @ A ) ),
inference(pre_uni,[status(thm)],[193:[bind(A,$thf( E @ C )),bind(B,$thf( ^ [E: a] : ( sk3 @ ( sk4 @ ( E @ E ) ) ) )),bind(C,$thf( C ))]]) ).
thf(220,plain,
! [B: a > a,A: a] :
( ~ ( sk2 @ ( B @ A ) )
| ( ( B @ A )
!= ( sk7
@ ^ [C: a] : ( sk3 @ ( sk4 @ ( B @ C ) ) ) ) )
| ( ( sk8 @ A
@ ^ [C: a] : ( sk3 @ ( sk4 @ ( B @ C ) ) ) )
!= A )
| ( sk5
@ ^ [C: a] : ( sk3 @ ( sk4 @ ( B @ C ) ) ) )
| ~ ( sk2 @ A ) ),
inference(simp,[status(thm)],[210]) ).
thf(2643,plain,
( ~ $true
| ( ( sk7 @ sk4 )
!= ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,2195]) ).
thf(2644,plain,
( ( ( sk7 @ sk4 )
!= ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[2643]) ).
thf(2673,plain,
( ( ( sk7 @ sk4 )
!= ( sk6
@ ^ [A: a] : A ) )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[2644]) ).
thf(5045,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[4799,69]) ).
thf(5046,plain,
! [A: a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5045]) ).
thf(5072,plain,
~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[5046:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk4 @ D ) ) ) ) ))]]) ).
thf(8618,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,5072]) ).
thf(8619,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[8618]) ).
thf(8645,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[8619:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ ^ [F: a] : ( sk4 @ E ) ) ) ) ) ) ))]]) ).
thf(5366,plain,
( ( ( sk7
@ ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= sk24 )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(func_ext,[status(esa)],[5306]) ).
thf(190,plain,
! [A: a] :
( ( ( sk3 @ ( sk4 @ A ) )
= A )
| ~ $true
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[134,18]) ).
thf(191,plain,
! [A: a] :
( ( ( sk3 @ ( sk4 @ A ) )
= A )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[190]) ).
thf(192,plain,
( ( sk3
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) ) )
= ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) ),
inference(pattern_uni,[status(thm)],[191:[bind(A,$thf( sk3 @ ( sk7 @ ^ [B: a] : ( sk7 @ sk4 ) ) ))]]) ).
thf(405,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,399]) ).
thf(406,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(simp,[status(thm)],[405]) ).
thf(407,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[406:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ sk4 ) ) ) ) ))]]) ).
thf(9,plain,
! [B: a,A: a] :
( ~ ( sk2 @ A )
| ~ ( sk1 @ B )
| ( A
!= ( sk3 @ B ) )
| ( B
= ( sk4 @ A ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(20,plain,
! [B: a,A: a] :
( ( A
!= ( sk3 @ B ) )
| ( B
= ( sk4 @ A ) )
| ~ ( sk2 @ A )
| ~ ( sk1 @ B ) ),
inference(lifteq,[status(thm)],[9]) ).
thf(21,plain,
! [A: a] :
( ( ( sk4 @ ( sk3 @ A ) )
= A )
| ~ ( sk2 @ ( sk3 @ A ) )
| ~ ( sk1 @ A ) ),
inference(simp,[status(thm)],[20]) ).
thf(135,plain,
! [B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( sk8 @ B @ A )
!= B )
| ( sk5 @ A )
| ~ $true
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[96,16]) ).
thf(136,plain,
! [B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( sk8 @ B @ A )
!= B )
| ( sk5 @ A )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[135]) ).
thf(137,plain,
! [A: a > a] :
( ( ( sk7 @ A )
!= ( A @ ( sk3 @ ( sk7 @ sk4 ) ) ) )
| ( ( sk8 @ ( sk3 @ ( sk7 @ sk4 ) ) @ A )
!= ( sk3 @ ( sk7 @ sk4 ) ) )
| ( sk5 @ A ) ),
inference(pattern_uni,[status(thm)],[136:[bind(A,$thf( A )),bind(B,$thf( sk3 @ ( sk7 @ sk4 ) ))]]) ).
thf(6833,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] :
( sk7
@ ^ [F: a] : ( sk4 @ E ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,5214]) ).
thf(6834,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] :
( sk7
@ ^ [F: a] : ( sk4 @ E ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[6833]) ).
thf(6852,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] :
( sk7
@ ^ [F: a] : ( sk4 @ E ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[6834:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ ^ [F: a] : ( sk7 @ ^ [G: a] : ( sk4 @ F ) ) ) ) ) ))]]) ).
thf(206,plain,
! [B: a,A: a > a] :
( ~ ( sk5 @ A )
| ( ( sk3 @ ( sk4 @ B ) )
= B )
| ~ $true
| ( ( sk2 @ ( sk6 @ A ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[26,18]) ).
thf(207,plain,
! [B: a,A: a > a] :
( ~ ( sk5 @ A )
| ( ( sk3 @ ( sk4 @ B ) )
= B )
| ( ( sk2 @ ( sk6 @ A ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[206]) ).
thf(208,plain,
! [A: a > a] :
( ~ ( sk5 @ A )
| ( ( sk3 @ ( sk4 @ ( sk6 @ A ) ) )
= ( sk6 @ A ) ) ),
inference(pattern_uni,[status(thm)],[207:[bind(A,$thf( C )),bind(B,$thf( sk6 @ C ))]]) ).
thf(218,plain,
! [A: a > a] :
( ~ ( sk5 @ A )
| ( ( sk3 @ ( sk4 @ ( sk6 @ A ) ) )
= ( sk6 @ A ) ) ),
inference(simp,[status(thm)],[208]) ).
thf(15294,plain,
! [A: a > a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ~ $true
| ( ( sk3 @ ( sk4 @ ( sk6 @ A ) ) )
= ( sk6 @ A ) )
| ( ( sk5
@ ^ [B: a] : B )
!= ( sk5 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,218]) ).
thf(15295,plain,
! [A: a > a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ( ( sk3 @ ( sk4 @ ( sk6 @ A ) ) )
= ( sk6 @ A ) )
| ( ( sk5
@ ^ [B: a] : B )
!= ( sk5 @ A ) ) ),
inference(simp,[status(thm)],[15294]) ).
thf(15296,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk3
@ ( sk4
@ ( sk6
@ ^ [A: a] : A ) ) )
= ( sk6
@ ^ [A: a] : A ) ) ),
inference(pattern_uni,[status(thm)],[15295:[bind(A,$thf( ^ [B: a] : B ))]]) ).
thf(5671,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk4 @ D ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,4454]) ).
thf(5672,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk4 @ D ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5671]) ).
thf(5690,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk4 @ D ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[5672:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk4 @ ( sk3 @ ( sk4 @ E ) ) ) ) ) ))]]) ).
thf(1849,plain,
! [A: a > a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ( sk2 @ ( sk6 @ A ) )
| ~ $true
| ( ( sk5
@ ^ [B: a] : B )
!= ( sk5 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,26]) ).
thf(1850,plain,
! [A: a > a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ( sk2 @ ( sk6 @ A ) )
| ( ( sk5
@ ^ [B: a] : B )
!= ( sk5 @ A ) ) ),
inference(simp,[status(thm)],[1849]) ).
thf(1851,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( sk2
@ ( sk6
@ ^ [A: a] : A ) ) ),
inference(pattern_uni,[status(thm)],[1850:[bind(A,$thf( ^ [B: a] : B ))]]) ).
thf(4975,plain,
( ~ $true
| ( sk2
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4771,1851]) ).
thf(4976,plain,
( ( sk2
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[4975]) ).
thf(5038,plain,
( ( sk2
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4976]) ).
thf(3385,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk6
@ ^ [C: a] : C ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,3332]) ).
thf(3386,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk6
@ ^ [C: a] : C ) ) ) ) ),
inference(simp,[status(thm)],[3385]) ).
thf(3387,plain,
( ( sk1
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) ) )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(pattern_uni,[status(thm)],[3386:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk6 @ ^ [C: a] : C ) ) ))]]) ).
thf(6104,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[3387,1811]) ).
thf(6105,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk1
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[6104]) ).
thf(6168,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk7
@ ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( sk6
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[6105]) ).
thf(1839,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,143]) ).
thf(1840,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1839]) ).
thf(1856,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) )
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1840]) ).
thf(186,plain,
! [A: a] :
( ( ( sk3 @ ( sk4 @ A ) )
= A )
| ~ $true
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[96,18]) ).
thf(187,plain,
! [A: a] :
( ( ( sk3 @ ( sk4 @ A ) )
= A )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[186]) ).
thf(188,plain,
( ( sk3 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) )
= ( sk3 @ ( sk7 @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[187:[bind(A,$thf( sk3 @ ( sk7 @ sk4 ) ))]]) ).
thf(5354,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[4433,50]) ).
thf(5355,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[5354]) ).
thf(5362,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[5355:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk4 @ D ) ) ) ) ) ))]]) ).
thf(167,plain,
! [B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( sk8 @ B @ A )
!= B )
| ( sk5 @ A )
| ~ $true
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[134,16]) ).
thf(168,plain,
! [B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( sk8 @ B @ A )
!= B )
| ( sk5 @ A )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[167]) ).
thf(169,plain,
! [A: a > a] :
( ( ( sk7 @ A )
!= ( A
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ) )
| ( ( sk8
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) )
@ A )
!= ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) )
| ( sk5 @ A ) ),
inference(pattern_uni,[status(thm)],[168:[bind(A,$thf( A )),bind(B,$thf( sk3 @ ( sk7 @ ^ [C: a] : ( sk7 @ sk4 ) ) ))]]) ).
thf(3883,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,250]) ).
thf(3884,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3883]) ).
thf(3916,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[3884:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ sk4 ) ) ) ) ) ))]]) ).
thf(164,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,143]) ).
thf(165,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ),
inference(simp,[status(thm)],[164]) ).
thf(166,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[165:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ))]]) ).
thf(418,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[166,19]) ).
thf(419,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[418]) ).
thf(420,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[419:[bind(A,$thf( sk3 @ ( sk7 @ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ))]]) ).
thf(113,plain,
! [C: a,B: a > a,A: a > a] :
( ( sk5 @ A )
| ( ( sk7 @ B )
!= ( B @ C ) )
| ( ( sk8 @ C @ B )
!= C )
| ( sk5 @ B )
| ~ $true
| ( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
!= ( sk2 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[40,16]) ).
thf(114,plain,
! [C: a,B: a > a,A: a > a] :
( ( sk5 @ A )
| ( ( sk7 @ B )
!= ( B @ C ) )
| ( ( sk8 @ C @ B )
!= C )
| ( sk5 @ B )
| ( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
!= ( sk2 @ C ) ) ),
inference(simp,[status(thm)],[113]) ).
thf(115,plain,
! [B: a > a,A: a > a] :
( ( sk5 @ B )
| ( ( sk7 @ A )
!= ( A @ ( sk3 @ ( sk7 @ B ) ) ) )
| ( ( sk8 @ ( sk3 @ ( sk7 @ B ) ) @ A )
!= ( sk3 @ ( sk7 @ B ) ) )
| ( sk5 @ A ) ),
inference(pattern_uni,[status(thm)],[114:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( sk3 @ ( sk7 @ E ) ))]]) ).
thf(124,plain,
! [B: a > a,A: a > a] :
( ( sk5 @ B )
| ( ( sk7 @ A )
!= ( A @ ( sk3 @ ( sk7 @ B ) ) ) )
| ( ( sk8 @ ( sk3 @ ( sk7 @ B ) ) @ A )
!= ( sk3 @ ( sk7 @ B ) ) )
| ( sk5 @ A ) ),
inference(simp,[status(thm)],[115]) ).
thf(4423,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[4398,35]) ).
thf(4424,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[4423]) ).
thf(4425,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[4424:[bind(A,$thf( sk7 @ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ))]]) ).
thf(4839,plain,
( ~ $true
| ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[134,4773]) ).
thf(4840,plain,
( ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[4839]) ).
thf(4867,plain,
( ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4840]) ).
thf(4457,plain,
( ( ( sk4 @ ( sk3 @ ( sk4 @ sk19 ) ) )
!= sk19 )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(func_ext,[status(esa)],[4407]) ).
thf(5061,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[4799,35]) ).
thf(5062,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[5061]) ).
thf(5063,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[5062:[bind(A,$thf( sk7 @ ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ C ) ) ) ))]]) ).
thf(4471,plain,
( ~ $true
| ( ( ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,4407]) ).
thf(4472,plain,
( ( ( ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[4471]) ).
thf(4508,plain,
( ( ( ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4472]) ).
thf(5087,plain,
! [A: a > a] :
( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) )
| ~ $true
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[4771,72]) ).
thf(5088,plain,
! [A: a > a] :
( ( sk1
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5087]) ).
thf(5159,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[5088:[bind(A,$thf( ^ [B: a] : ( sk3 @ ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ C ) ) ) ) ))]]) ).
thf(8682,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[5159,50]) ).
thf(8683,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[8682]) ).
thf(8690,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[8683:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ))]]) ).
thf(4899,plain,
( ~ $true
| ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,4818]) ).
thf(4900,plain,
( ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[4899]) ).
thf(4934,plain,
( ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4900]) ).
thf(1835,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,150]) ).
thf(1836,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1835]) ).
thf(1874,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) )
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1836]) ).
thf(1795,plain,
( ~ $true
| ( sk5
@ ^ [A: a] : A )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,1358]) ).
thf(1796,plain,
( ( sk5
@ ^ [A: a] : A )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[1795]) ).
thf(1857,plain,
( ( sk5
@ ^ [A: a] : A )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1796]) ).
thf(103,plain,
! [C: a > a,B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( sk8 @ B @ A )
!= B )
| ~ ( sk2 @ B )
| ~ ( sk1 @ ( C @ ( sk6 @ C ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[16,25]) ).
thf(104,plain,
! [C: a > a,B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( sk8 @ B @ A )
!= B )
| ~ ( sk2 @ B )
| ~ ( sk1 @ ( C @ ( sk6 @ C ) ) )
| ( ( sk5 @ A )
!= ( sk5 @ C ) ) ),
inference(simp,[status(thm)],[103]) ).
thf(105,plain,
! [B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( sk8 @ B @ A )
!= B )
| ~ ( sk2 @ B )
| ~ ( sk1 @ ( A @ ( sk6 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[104:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A ))]]) ).
thf(2111,plain,
( ~ $true
| ~ ( sk1
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,1811]) ).
thf(2112,plain,
( ~ ( sk1
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[2111]) ).
thf(2176,plain,
( ~ ( sk1
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[2112]) ).
thf(5335,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[4433,69]) ).
thf(5336,plain,
! [A: a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5335]) ).
thf(5359,plain,
~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[5336:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk4 @ D ) ) ) ) ) ))]]) ).
thf(1913,plain,
( ~ $true
| ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[158,1861]) ).
thf(1914,plain,
( ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[1913]) ).
thf(1927,plain,
( ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1914]) ).
thf(7893,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,4432]) ).
thf(7894,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[7893]) ).
thf(7920,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[7894:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk4 @ D ) ) ) ) ) ) ))]]) ).
thf(5713,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[4791,35]) ).
thf(5714,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[5713]) ).
thf(5715,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[5714:[bind(A,$thf( sk4 @ ( sk3 @ ( sk7 @ ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ B ) ) ) ) ))]]) ).
thf(4447,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,4406]) ).
thf(4448,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4447]) ).
thf(4453,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) )
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4448]) ).
thf(4778,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4764,1811]) ).
thf(4779,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[4778]) ).
thf(4797,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) )
!= ( sk6
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4779]) ).
thf(6467,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[5069,35]) ).
thf(6468,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[6467]) ).
thf(6469,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[6468:[bind(A,$thf( sk7 @ ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk4 @ D ) ) ) ) ))]]) ).
thf(400,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,399]) ).
thf(401,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(simp,[status(thm)],[400]) ).
thf(402,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[401:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ sk4 ) ) ) ) ))]]) ).
thf(178,plain,
! [A: a] :
( ~ $true
| ( sk2 @ ( sk3 @ A ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[142,6]) ).
thf(179,plain,
! [A: a] :
( ( sk2 @ ( sk3 @ A ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[178]) ).
thf(180,plain,
sk2 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ),
inference(pattern_uni,[status(thm)],[179:[bind(A,$thf( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ))]]) ).
thf(292,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ A ) )
| ( ( sk2 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[180,19]) ).
thf(293,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ A ) )
| ( ( sk2 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[292]) ).
thf(294,plain,
sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ),
inference(pattern_uni,[status(thm)],[293:[bind(A,$thf( sk3 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ))]]) ).
thf(643,plain,
! [A: a] :
( ~ $true
| ( sk2 @ ( sk3 @ A ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[294,6]) ).
thf(644,plain,
! [A: a] :
( ( sk2 @ ( sk3 @ A ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[643]) ).
thf(645,plain,
sk2 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[644:[bind(A,$thf( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ))]]) ).
thf(2859,plain,
sk2 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ),
inference(rewrite,[status(thm)],[645,188]) ).
thf(4584,plain,
( ~ $true
| ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4405,1861]) ).
thf(4585,plain,
( ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[4584]) ).
thf(4605,plain,
( ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4585]) ).
thf(116,plain,
! [C: a > a,B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( sk8 @ B @ A )
!= B )
| ~ ( sk2 @ B )
| ( sk2 @ ( sk6 @ C ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[16,26]) ).
thf(117,plain,
! [C: a > a,B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( sk8 @ B @ A )
!= B )
| ~ ( sk2 @ B )
| ( sk2 @ ( sk6 @ C ) )
| ( ( sk5 @ A )
!= ( sk5 @ C ) ) ),
inference(simp,[status(thm)],[116]) ).
thf(118,plain,
! [B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( ( sk8 @ B @ A )
!= B )
| ~ ( sk2 @ B )
| ( sk2 @ ( sk6 @ A ) ) ),
inference(pattern_uni,[status(thm)],[117:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A ))]]) ).
thf(29,plain,
! [B: a,A: a] :
( ~ ( sk2 @ A )
| ~ $true
| ( sk2 @ ( sk3 @ B ) )
| ( ( sk1 @ ( sk4 @ A ) )
!= ( sk1 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[19,6]) ).
thf(30,plain,
! [B: a,A: a] :
( ~ ( sk2 @ A )
| ( sk2 @ ( sk3 @ B ) )
| ( ( sk1 @ ( sk4 @ A ) )
!= ( sk1 @ B ) ) ),
inference(simp,[status(thm)],[29]) ).
thf(31,plain,
! [A: a] :
( ~ ( sk2 @ A )
| ( sk2 @ ( sk3 @ ( sk4 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[30:[bind(A,$thf( C )),bind(B,$thf( sk4 @ C ))]]) ).
thf(36,plain,
! [A: a] :
( ~ ( sk2 @ A )
| ( sk2 @ ( sk3 @ ( sk4 @ A ) ) ) ),
inference(simp,[status(thm)],[31]) ).
thf(4588,plain,
! [A: a] :
( ~ $true
| ( sk2 @ ( sk3 @ ( sk4 @ A ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[4405,36]) ).
thf(4589,plain,
! [A: a] :
( ( sk2 @ ( sk3 @ ( sk4 @ A ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[4588]) ).
thf(4590,plain,
( sk2
@ ( sk3
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[4589:[bind(A,$thf( sk3 @ ( sk7 @ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ))]]) ).
thf(2287,plain,
( ~ $true
| ( sk2
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,1851]) ).
thf(2288,plain,
( ( sk2
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[2287]) ).
thf(2326,plain,
( ( sk2
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[2288]) ).
thf(1854,plain,
( ~ $true
| ( sk5
@ ^ [A: a] : A )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[158,1358]) ).
thf(1855,plain,
( ( sk5
@ ^ [A: a] : A )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[1854]) ).
thf(1865,plain,
( ( sk5
@ ^ [A: a] : A )
| ( ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1855]) ).
thf(3289,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk1
@ ( sk4
@ ( sk6
@ ^ [A: a] : A ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[3126,1811]) ).
thf(3290,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk1
@ ( sk4
@ ( sk6
@ ^ [A: a] : A ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[3289]) ).
thf(3340,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk4
@ ( sk6
@ ^ [A: a] : A ) )
!= ( sk6
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[3290]) ).
thf(84,plain,
! [B: a > a,A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( sk2 @ ( sk6 @ B ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[40,26]) ).
thf(85,plain,
! [B: a > a,A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( sk2 @ ( sk6 @ B ) )
| ( ( sk5 @ A )
!= ( sk5 @ B ) ) ),
inference(simp,[status(thm)],[84]) ).
thf(86,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( sk2 @ ( sk6 @ A ) ) ),
inference(pattern_uni,[status(thm)],[85:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(5009,plain,
! [A: a] :
( ~ $true
| ( sk2 @ ( sk3 @ ( sk4 @ A ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[4771,36]) ).
thf(5010,plain,
! [A: a] :
( ( sk2 @ ( sk3 @ ( sk4 @ A ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[5009]) ).
thf(5011,plain,
( sk2
@ ( sk3
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[5010:[bind(A,$thf( sk3 @ ( sk7 @ ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ B ) ) ) ))]]) ).
thf(7268,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,7244]) ).
thf(7269,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[7268]) ).
thf(7270,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[7269:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [C: a] : ( sk4 @ B ) ) ) ) ))]]) ).
thf(7310,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,7272]) ).
thf(7311,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[7310]) ).
thf(7330,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[7311:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ))]]) ).
thf(5682,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,4454]) ).
thf(5683,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[5682]) ).
thf(5689,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) )
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[5683]) ).
thf(2123,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[142,1811]) ).
thf(2124,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[2123]) ).
thf(2182,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk6
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[2124]) ).
thf(7293,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[7263,50]) ).
thf(7294,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[7293]) ).
thf(7297,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[7294:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ))]]) ).
thf(2113,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[129,1811]) ).
thf(2114,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk1
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[2113]) ).
thf(2171,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) )
!= ( sk6
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[2114]) ).
thf(3618,plain,
( ~ $true
| ( ( sk4
@ ( sk6
@ ^ [A: a] : A ) )
!= ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,3340]) ).
thf(3619,plain,
( ( ( sk4
@ ( sk6
@ ^ [A: a] : A ) )
!= ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[3618]) ).
thf(3674,plain,
( ( ( sk4
@ ( sk6
@ ^ [A: a] : A ) )
!= ( sk6
@ ^ [A: a] : A ) )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[3619]) ).
thf(265,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,175]) ).
thf(266,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(simp,[status(thm)],[265]) ).
thf(267,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[266:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ))]]) ).
thf(436,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[237,19]) ).
thf(437,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[436]) ).
thf(438,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[437:[bind(A,$thf( sk3 @ ( sk7 @ ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ))]]) ).
thf(683,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5 @ A )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[402,25]) ).
thf(684,plain,
! [A: a > a] :
( ~ ( sk5 @ A )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[683]) ).
thf(688,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk7 @ sk4 ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[684:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ ^ [F: a] : ( sk7 @ sk4 ) ) ) ) ) ))]]) ).
thf(3885,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] :
( sk7
@ ^ [F: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,688]) ).
thf(3886,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] :
( sk7
@ ^ [F: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3885]) ).
thf(3908,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] :
( sk7
@ ^ [F: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[3886:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ ^ [F: a] : ( sk7 @ ^ [G: a] : ( sk7 @ sk4 ) ) ) ) ) ))]]) ).
thf(6450,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[5069,69]) ).
thf(6451,plain,
! [A: a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( A @ B ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[6450]) ).
thf(6476,plain,
~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[6451:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ ^ [F: a] : ( sk4 @ E ) ) ) ) ) ))]]) ).
thf(195,plain,
! [B: a > a,A: a] :
( ~ ( sk2 @ A )
| ~ ( sk2 @ A )
| ~ ( sk5
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) )
| ( ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) )
!= ( sk3 @ ( sk4 @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[18,58]) ).
thf(196,plain,
! [B: a > a,A: a] :
( ~ ( sk2 @ A )
| ~ ( sk5
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) )
| ( ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) )
!= ( sk3 @ ( sk4 @ A ) ) ) ),
inference(simp,[status(thm)],[195]) ).
thf(215,plain,
! [A: a > a] :
( ~ ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ ( A @ B ) ) ) ) ) ) )
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ ( A @ B ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[196:[bind(A,$thf( D @ ( sk6 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk4 @ ( D @ D ) ) ) ) ) )),bind(B,$thf( ^ [D: a] : ( sk3 @ ( sk4 @ ( D @ D ) ) ) ))]]) ).
thf(223,plain,
! [A: a > a] :
( ~ ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ ( A @ B ) ) ) ) ) ) )
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ ( A @ B ) ) ) ) ) ),
inference(simp,[status(thm)],[215]) ).
thf(1411,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] :
( sk7
@ ^ [F: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,688]) ).
thf(1412,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] :
( sk7
@ ^ [F: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[1411]) ).
thf(1413,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[1412:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ ^ [F: a] : ( sk7 @ sk4 ) ) ) ) ) ))]]) ).
thf(416,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[166,58]) ).
thf(417,plain,
! [A: a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[416]) ).
thf(426,plain,
~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[417:[bind(A,$thf( ^ [B: a] : ( sk3 @ ( sk7 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ))]]) ).
thf(4986,plain,
( ~ $true
| ( ( ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4771,3419]) ).
thf(4987,plain,
( ( ( ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[4986]) ).
thf(5025,plain,
( ( ( ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4987]) ).
thf(3291,plain,
! [A: a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ~ $true
| ( sk2 @ ( sk3 @ A ) )
| ( ( sk1
@ ( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3126,6]) ).
thf(3292,plain,
! [A: a] :
( ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ( sk2 @ ( sk3 @ A ) )
| ( ( sk1
@ ( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[3291]) ).
thf(3293,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( sk2
@ ( sk3
@ ( sk4
@ ( sk6
@ ^ [A: a] : A ) ) ) ) ),
inference(pattern_uni,[status(thm)],[3292:[bind(A,$thf( sk4 @ ( sk6 @ ^ [B: a] : B ) ))]]) ).
thf(6845,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] : A )
!= ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1358,5214]) ).
thf(6846,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] : A )
!= ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[6845]) ).
thf(6853,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[6846]) ).
thf(122,plain,
! [B: a,A: a > a] :
( ( ( sk7 @ A )
!= ( A @ B ) )
| ( sk5 @ A )
| ~ ( sk2 @ B )
| ( ( sk8 @ B @ A )
!= ( A @ B ) )
| ( B
!= ( sk7 @ A ) ) ),
inference(eqfactor_ordered,[status(thm)],[16]) ).
thf(123,plain,
! [A: a > a] :
( ( sk5 @ A )
| ( ( A @ ( sk7 @ A ) )
!= ( sk7 @ A ) )
| ~ ( sk2 @ ( sk7 @ A ) )
| ( ( sk8 @ ( sk7 @ A ) @ A )
!= ( A @ ( sk7 @ A ) ) ) ),
inference(simp,[status(thm)],[122]) ).
thf(5975,plain,
( ~ $true
| ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4817,1861]) ).
thf(5976,plain,
( ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[5975]) ).
thf(5991,plain,
( ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[5976]) ).
thf(2513,plain,
( ( ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) )
!= sk13 )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(func_ext,[status(esa)],[1874]) ).
thf(3553,plain,
( ( ( sk4
@ ( sk6
@ ^ [A: a] : A ) )
!= sk17 )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(func_ext,[status(esa)],[3419]) ).
thf(3777,plain,
( ( ( sk4
@ ( sk6
@ ^ [A: a] : A ) )
!= sk17 )
| ~ $true
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,3553]) ).
thf(3778,plain,
( ( ( sk4
@ ( sk6
@ ^ [A: a] : A ) )
!= sk17 )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[3777]) ).
thf(3833,plain,
( ( ( sk4
@ ( sk6
@ ^ [A: a] : A ) )
!= sk17 )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[3778]) ).
thf(6472,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[5069,75]) ).
thf(6473,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[6472]) ).
thf(6481,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[6473:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ ^ [F: a] : ( sk4 @ E ) ) ) ) ) ))]]) ).
thf(4961,plain,
( ~ $true
| ~ ( sk1
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4771,1811]) ).
thf(4962,plain,
( ~ ( sk1
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[4961]) ).
thf(5018,plain,
( ~ ( sk1
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4962]) ).
thf(9127,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk4 @ D ) ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[5362,50]) ).
thf(9128,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk4 @ D ) ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[9127]) ).
thf(9138,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk4 @ D ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[9128:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk4 @ ( sk3 @ ( sk4 @ E ) ) ) ) ) ) ))]]) ).
thf(5386,plain,
( ~ $true
| ( ( ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk6
@ ^ [C: a] : C ) ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,5306]) ).
thf(5387,plain,
( ( ( ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk6
@ ^ [C: a] : C ) ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[5386]) ).
thf(5418,plain,
( ( ( ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk6
@ ^ [C: a] : C ) ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[5387]) ).
thf(5719,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[4791,75]) ).
thf(5720,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[5719]) ).
thf(5731,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[5720:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ))]]) ).
thf(3279,plain,
( ~ $true
| ( sk1
@ ( sk4
@ ( sk6
@ ^ [A: a] : A ) ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,3126]) ).
thf(3280,plain,
( ( sk1
@ ( sk4
@ ( sk6
@ ^ [A: a] : A ) ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[3279]) ).
thf(3329,plain,
( ( sk1
@ ( sk4
@ ( sk6
@ ^ [A: a] : A ) ) )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[3280]) ).
thf(491,plain,
! [A: a > a] :
( ~ $true
| ~ ( sk5 @ A )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[261,25]) ).
thf(492,plain,
! [A: a > a] :
( ~ ( sk5 @ A )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[491]) ).
thf(497,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[492:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ))]]) ).
thf(654,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,497]) ).
thf(655,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[654]) ).
thf(656,plain,
( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[655:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ))]]) ).
thf(9598,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ ( sk3 @ ( sk4 @ E ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,5690]) ).
thf(9599,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ ( sk3 @ ( sk4 @ E ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[9598]) ).
thf(9622,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ ( sk3 @ ( sk4 @ E ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[9599:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk7 @ ^ [F: a] : ( sk4 @ ( sk3 @ ( sk4 @ F ) ) ) ) ) ) ))]]) ).
thf(1812,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,257]) ).
thf(1813,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1812]) ).
thf(1881,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) )
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1813]) ).
thf(4412,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4398,1811]) ).
thf(4413,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk1
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) )
!= ( sk1
@ ( sk6
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[4412]) ).
thf(4431,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) )
!= ( sk6
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4413]) ).
thf(5979,plain,
! [A: a] :
( ~ $true
| ( sk2 @ ( sk3 @ ( sk4 @ A ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[4817,36]) ).
thf(5980,plain,
! [A: a] :
( ( sk2 @ ( sk3 @ ( sk4 @ A ) ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[5979]) ).
thf(5981,plain,
( sk2
@ ( sk3
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[5980:[bind(A,$thf( sk3 @ ( sk7 @ ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ C ) ) ) ) ))]]) ).
thf(1888,plain,
( ~ $true
| ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,1861]) ).
thf(1889,plain,
( ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[1888]) ).
thf(1917,plain,
( ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1889]) ).
thf(2626,plain,
( ( ( sk4 @ sk14 )
!= sk14 )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(func_ext,[status(esa)],[1917]) ).
thf(7257,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ( A @ B ) ) ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ( A @ B ) ) ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[89,7244]) ).
thf(7258,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ( A @ B ) ) ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ( A @ B ) ) ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[7257]) ).
thf(7271,plain,
~ ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[7258:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [D: a] : ( sk4 @ C ) ) ) ) ))]]) ).
thf(5255,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk6
@ ^ [D: a] : D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,3906]) ).
thf(5256,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk6
@ ^ [D: a] : D ) ) ) ) ) ),
inference(simp,[status(thm)],[5255]) ).
thf(5308,plain,
( ~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk6
@ ^ [D: a] : D ) ) ) ) )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(pre_uni,[status(thm)],[5256:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ ( sk6 @ ^ [E: a] : E ) ) ) ))]]) ).
thf(17112,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk6
@ ^ [D: a] : D ) ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(paramod_ordered,[status(thm)],[1358,5308]) ).
thf(17113,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk6
@ ^ [D: a] : D ) ) ) ) )
!= ( sk5
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[17112]) ).
thf(17155,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk6
@ ^ [D: a] : D ) ) ) ) )
!= ( ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[17113]) ).
thf(2988,plain,
( ( ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= sk15 )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(func_ext,[status(esa)],[1856]) ).
thf(4823,plain,
( ( ( sk7
@ ^ [A: a] : ( sk4 @ sk21 ) )
!= sk21 )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(func_ext,[status(esa)],[4773]) ).
thf(4449,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,4406]) ).
thf(4450,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[4449]) ).
thf(4451,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk4 @ B ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[4450:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ))]]) ).
thf(5520,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[4433,75]) ).
thf(5521,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk1
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk6 @ A ) ) ) ) ),
inference(simp,[status(thm)],[5520]) ).
thf(5600,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk4 @ C ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[5521:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk4 @ D ) ) ) ) ) ))]]) ).
thf(5209,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,4819]) ).
thf(5210,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] :
( sk7
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5209]) ).
thf(5211,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[5210:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ ^ [E: a] : ( sk4 @ D ) ) ) ) ))]]) ).
thf(2300,plain,
( ~ $true
| ( sk2
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[134,1851]) ).
thf(2301,plain,
( ( sk2
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[2300]) ).
thf(2315,plain,
( ( sk2
@ ( sk6
@ ^ [A: a] : A ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[2301]) ).
thf(3881,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ~ $true
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[57,497]) ).
thf(3882,plain,
! [A: a > a > a] :
( ~ ( sk5
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) )
| ( ( sk5
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk7 @ ( A @ B ) ) ) ) )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3881]) ).
thf(3907,plain,
~ ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[3882:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [E: a] : ( sk7 @ sk4 ) ) ) ) ) ))]]) ).
thf(4582,plain,
( ~ $true
| ( sk5
@ ^ [A: a] : A )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4405,1358]) ).
thf(4583,plain,
( ( sk5
@ ^ [A: a] : A )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[4582]) ).
thf(4597,plain,
( ( sk5
@ ^ [A: a] : A )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[4583]) ).
thf(5753,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] : A )
!= ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1358,4794]) ).
thf(5754,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] : A )
!= ( sk5
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5753]) ).
thf(5760,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5754]) ).
thf(5003,plain,
( ~ $true
| ( sk5
@ ^ [A: a] : A )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4771,1358]) ).
thf(5004,plain,
( ( sk5
@ ^ [A: a] : A )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[5003]) ).
thf(5041,plain,
( ( sk5
@ ^ [A: a] : A )
| ( ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[5004]) ).
thf(106,plain,
! [C: a,B: a > a,A: a] :
( ~ ( sk1 @ A )
| ( ( sk7 @ B )
!= ( B @ C ) )
| ( ( sk8 @ C @ B )
!= C )
| ( sk5 @ B )
| ~ $true
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[6,16]) ).
thf(107,plain,
! [C: a,B: a > a,A: a] :
( ~ ( sk1 @ A )
| ( ( sk7 @ B )
!= ( B @ C ) )
| ( ( sk8 @ C @ B )
!= C )
| ( sk5 @ B )
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ C ) ) ),
inference(simp,[status(thm)],[106]) ).
thf(108,plain,
! [B: a,A: a > a] :
( ~ ( sk1 @ B )
| ( ( sk7 @ A )
!= ( A @ ( sk3 @ B ) ) )
| ( ( sk8 @ ( sk3 @ B ) @ A )
!= ( sk3 @ B ) )
| ( sk5 @ A ) ),
inference(pattern_uni,[status(thm)],[107:[bind(A,$thf( D )),bind(B,$thf( B )),bind(C,$thf( sk3 @ D ))]]) ).
thf(126,plain,
! [B: a,A: a > a] :
( ~ ( sk1 @ B )
| ( ( sk7 @ A )
!= ( A @ ( sk3 @ B ) ) )
| ( ( sk8 @ ( sk3 @ B ) @ A )
!= ( sk3 @ B ) )
| ( sk5 @ A ) ),
inference(simp,[status(thm)],[108]) ).
thf(5971,plain,
( ~ $true
| ( sk5
@ ^ [A: a] : A )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[4817,1358]) ).
thf(5972,plain,
( ( sk5
@ ^ [A: a] : A )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[5971]) ).
thf(5990,plain,
( ( sk5
@ ^ [A: a] : A )
| ( ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[5972]) ).
thf(5207,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ~ $true
| ( ( sk5
@ ^ [A: a] : A )
!= ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1358,4819]) ).
thf(5208,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( sk5
@ ^ [A: a] : A )
!= ( sk5
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5207]) ).
thf(5215,plain,
( ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) )
| ( ( ^ [A: a] : A )
!= ( ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[5208]) ).
thf(3572,plain,
( ~ $true
| ( ( ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[134,3419]) ).
thf(3573,plain,
( ( ( ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[3572]) ).
thf(3605,plain,
( ( ( ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[3573]) ).
thf(5278,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ $true
| ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk6
@ ^ [D: a] : D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,3906]) ).
thf(5279,plain,
! [A: a > a] :
( ( sk1 @ ( sk7 @ A ) )
| ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] :
( sk4
@ ( sk6
@ ^ [D: a] : D ) ) ) ) ) ),
inference(simp,[status(thm)],[5278]) ).
thf(5280,plain,
( ( sk1
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] :
( sk4
@ ( sk6
@ ^ [C: a] : C ) ) ) ) )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(pattern_uni,[status(thm)],[5279:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ ( sk6 @ ^ [D: a] : D ) ) ) ))]]) ).
thf(1901,plain,
( ~ $true
| ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[134,1861]) ).
thf(1902,plain,
( ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[1901]) ).
thf(1925,plain,
( ( sk4
!= ( ^ [A: a] : A ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[1902]) ).
thf(7250,plain,
! [A: a > a] :
( ( sk1 @ ( sk4 @ ( sk3 @ ( sk7 @ A ) ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[88,7244]) ).
thf(7251,plain,
! [A: a > a] :
( ( sk1 @ ( sk4 @ ( sk3 @ ( sk7 @ A ) ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[7250]) ).
thf(7252,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[7251:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [C: a] : ( sk4 @ B ) ) ) ) ))]]) ).
thf(5768,plain,
( ( ( sk7
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) )
!= sk25 )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(func_ext,[status(esa)],[4453]) ).
thf(275,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,257]) ).
thf(276,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(simp,[status(thm)],[275]) ).
thf(277,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[276:[bind(A,$thf( ^ [B: a] : ( sk7 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk7 @ sk4 ) ) ) ) ))]]) ).
thf(3392,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk6
@ ^ [C: a] : C ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,3332]) ).
thf(3393,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ ( sk2
@ ( sk7
@ ^ [B: a] : B ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk6
@ ^ [C: a] : C ) ) ) ) ),
inference(simp,[status(thm)],[3392]) ).
thf(3394,plain,
( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk6
@ ^ [B: a] : B ) ) ) ) )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(pattern_uni,[status(thm)],[3393:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk6 @ ^ [C: a] : C ) ) ))]]) ).
thf(76,plain,
! [B: a > a,A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ ( sk2
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,58]) ).
thf(77,plain,
! [B: a > a,A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ ( sk2
@ ( B
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [C: a] : ( sk4 @ ( B @ C ) ) ) ) ),
inference(simp,[status(thm)],[76]) ).
thf(78,plain,
! [A: a > a] :
( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) )
| ~ ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[77:[bind(A,$thf( ^ [D: a] : ( sk4 @ ( C @ D ) ) )),bind(B,$thf( C ))]]) ).
thf(90,plain,
! [A: a > a] :
( ( sk2
@ ( sk3
@ ( sk7
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) )
| ~ ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( A @ B ) ) ) ) ) ),
inference(simp,[status(thm)],[78]) ).
thf(2516,plain,
( ~ $true
| ( ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[96,1874]) ).
thf(2517,plain,
( ( ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2 @ ( sk3 @ ( sk7 @ sk4 ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[2516]) ).
thf(2563,plain,
( ( ( ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) )
!= ( ^ [A: a] : A ) )
| ( ( sk3 @ ( sk7 @ sk4 ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[2517]) ).
thf(3212,plain,
( ( ( sk7
@ ^ [A: a] :
( sk7
@ ^ [B: a] : ( sk7 @ sk4 ) ) )
!= sk16 )
| ~ ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ),
inference(func_ext,[status(esa)],[1875]) ).
thf(2219,plain,
( ~ $true
| ( ( ^ [A: a] : ( sk7 @ sk4 ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(paramod_ordered,[status(thm)],[134,1873]) ).
thf(2220,plain,
( ( ( ^ [A: a] : ( sk7 @ sk4 ) )
!= ( ^ [A: a] : A ) )
| ( ( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) ) )
!= ( sk2
@ ( sk7
@ ^ [A: a] : A ) ) ) ),
inference(simp,[status(thm)],[2219]) ).
thf(2238,plain,
( ( ( ^ [A: a] : ( sk7 @ sk4 ) )
!= ( ^ [A: a] : A ) )
| ( ( sk3
@ ( sk7
@ ^ [A: a] : ( sk7 @ sk4 ) ) )
!= ( sk7
@ ^ [A: a] : A ) ) ),
inference(simp,[status(thm)],[2220]) ).
thf(452,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ~ $true
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,250]) ).
thf(453,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk7 @ A ) ) )
| ( ( sk5 @ A )
!= ( sk5
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [C: a] :
( sk7
@ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[452]) ).
thf(454,plain,
( sk2
@ ( sk3
@ ( sk7
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk7
@ ^ [B: a] :
( sk7
@ ^ [C: a] : ( sk7 @ sk4 ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[453:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk7 @ ^ [C: a] : ( sk7 @ ^ [D: a] : ( sk7 @ sk4 ) ) ) ) ) ))]]) ).
thf(184,plain,
! [B: a > a,A: a] :
( ~ ( sk2 @ A )
| ~ ( sk1 @ A )
| ~ ( sk5 @ B )
| ( ( sk3 @ ( sk4 @ A ) )
!= ( B @ ( sk6 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[18,25]) ).
thf(214,plain,
! [A: a > a] :
( ~ ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk3 @ ( sk4 @ ( A @ B ) ) ) ) ) )
| ~ ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk3 @ ( sk4 @ ( A @ B ) ) ) ) ) )
| ~ ( sk5
@ ^ [B: a] : ( sk3 @ ( sk4 @ ( A @ B ) ) ) ) ),
inference(pre_uni,[status(thm)],[184:[bind(A,$thf( D @ ( sk6 @ ^ [D: a] : ( sk3 @ ( sk4 @ ( D @ D ) ) ) ) )),bind(B,$thf( ^ [D: a] : ( sk3 @ ( sk4 @ ( D @ D ) ) ) ))]]) ).
thf(222,plain,
! [A: a > a] :
( ~ ( sk2
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk3 @ ( sk4 @ ( A @ B ) ) ) ) ) )
| ~ ( sk1
@ ( A
@ ( sk6
@ ^ [B: a] : ( sk3 @ ( sk4 @ ( A @ B ) ) ) ) ) )
| ~ ( sk5
@ ^ [B: a] : ( sk3 @ ( sk4 @ ( A @ B ) ) ) ) ),
inference(simp,[status(thm)],[214]) ).
thf(21583,plain,
$false,
inference(e,[status(thm)],[69,1879,7272,5028,88,481,3317,4515,5069,1882,217,2195,5037,3332,153,670,4884,142,4870,174,24,5723,2173,25,1887,257,2603,5306,12832,5759,125,5214,46,93,3902,1875,4771,261,448,57,4432,6002,7273,1811,5027,4454,9837,1858,2178,216,7300,443,5353,5220,3421,221,3906,2982,89,5169,6,2204,4407,6482,5070,220,102,2673,28,8645,70,5366,7244,192,407,21,137,229,6852,15296,5690,5038,6168,1851,1856,188,5362,169,3916,420,4817,124,4772,4425,4389,4750,4406,4867,4457,96,5063,3126,4508,8690,4934,129,1874,134,1857,237,105,2176,5359,166,1927,161,7920,5715,4453,4797,6469,3387,402,2859,22,4605,118,4590,71,2326,1865,3340,4764,4433,86,5011,7270,3419,7330,245,5689,4773,271,4374,2182,4818,7297,399,2171,3674,2244,3,267,438,3908,35,6476,223,608,1413,4405,1873,426,5025,3293,6853,123,5991,2513,150,3833,6481,5018,9138,18,50,4398,5418,5731,16,3329,1358,656,175,9622,1881,4819,4431,72,143,497,250,5981,2626,688,7271,17155,3593,218,5308,2988,40,26,158,4791,4823,4451,5600,1861,75,58,5072,5211,2315,4794,3907,36,19,4597,5760,5041,126,5159,5990,5215,4799,3605,5280,1925,7263,7252,5768,47,277,3394,90,2563,3212,2238,1917,454,232,222,3553]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV094^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.11/0.23 % Computer : n005.cluster.edu
% 0.11/0.23 % Model : x86_64 x86_64
% 0.11/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.23 % Memory : 8046.5625MB
% 0.11/0.23 % OS : Linux 6.8.0-71-generic
% 0.11/0.23 % CPULimit : 300
% 0.11/0.23 % WCLimit : 300
% 0.11/0.23 % DateTime : Tue Sep 29 15:09:46 UTC 2026
% 0.11/0.23 % CPUTime :
% 0.11/0.23 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.80 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.26/0.99 % [INFO] Parsing done (184ms).
% 1.26/1.00 % [INFO] Running in sequential loop mode.
% 2.18/1.40 % [INFO] eprover registered as external prover.
% 2.18/1.41 % [INFO] Scanning for conjecture ...
% 2.39/1.52 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.39/1.58 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.39/1.58 % [INFO] Problem is higher-order (TPTP THF).
% 2.39/1.58 % [INFO] Type checking passed.
% 2.39/1.59 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 86.17/18.42 % External prover 'e' found a proof!
% 86.17/18.42 % [INFO] Killing All external provers ...
% 86.17/18.42 % Time passed: 18044ms (effective reasoning time: 17411ms)
% 86.17/18.42 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 86.17/18.42 % Axioms used in derivation (0):
% 86.17/18.42 % No. of inferences in proof: 727
% 86.17/18.42 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 18044 ms resp. 17411 ms w/o parsing
% 74.20/18.85 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 74.20/18.85 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------