%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEV089^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 : n001.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 87.84s 21.31s
% Output : Refutation 85.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 7
% Syntax : Number of formulae : 303 ( 43 unt; 0 typ; 6 def)
% Number of atoms : 1499 ( 580 equ; 102 cnn)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 4929 ( 542 ~; 522 |; 119 &;3717 @)
% ( 0 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 8 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 293 ( 293 >; 0 *; 0 +; 0 <<)
% Number of symbols : 15 ( 11 usr; 3 con; 0-2 aty)
% Number of variables : 1069 ( 619 ^; 422 !; 22 ?;1069 :)
% ( 0 !>; 0 ?*; 0 @-; 6 @+)
% 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 ) > a ).
thf(sk6_decl,type,
sk6: ( a > a ) > a ).
thf(sk7_decl,type,
sk7: a > ( a > a ) > a ).
thf(sk8_decl,type,
sk8: ( a > a > a ) > a > a ).
thf(sk9_decl,type,
sk9: a > ( a > a ) > a ).
thf(sk14_decl,type,
sk14: a > a > a ).
thf(sk26_decl,type,
sk26: a > 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] :
( ( ^ [F: a] :
( ( A @ F )
& ( D
= ( C @ F ) ) ) )
= ( (=) @ a @ E ) ) ) )
=> ? [C: a > a] :
( ! [D: a] :
( ( B @ D )
=> ( A @ ( C @ D ) ) )
& ! [D: a] :
( ( A @ D )
=> ? [E: a] :
( ( ^ [F: a] :
( ( B @ F )
& ( D
= ( C @ F ) ) ) )
= ( (=) @ a @ 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] :
( ( ^ [E: a] :
( ( sk1 @ E )
& ( C
= ( B @ E ) ) ) )
= ( (=) @ a @ D ) ) ) )
=> ? [B: a > a] :
( ! [C: a] :
( ( A @ C )
=> ( sk1 @ ( B @ C ) ) )
& ! [C: a] :
( ( sk1 @ C )
=> ? [D: a] :
( ( ^ [E: a] :
( ( A @ E )
& ( C
= ( B @ E ) ) ) )
= ( (=) @ a @ D ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: a > a] :
( ! [B: a] :
( ( sk1 @ B )
=> ( sk2 @ ( A @ B ) ) )
& ! [B: a] :
( ( sk2 @ B )
=> ? [C: a] :
( ( ^ [D: a] :
( ( sk1 @ D )
& ( B
= ( A @ D ) ) ) )
= ( (=) @ a @ C ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: a] :
@+[B: a] :
( ( ^ [C: a] :
( ( sk1 @ C )
& ( A
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ B ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: a > a] :
@+[B: a] :
~ ( ( sk2 @ B )
=> ( sk1 @ ( A @ B ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: a > a] :
@+[B: a] :
~ ( ( sk1 @ B )
=> ? [C: a] :
( ( ^ [D: a] :
( ( sk2 @ D )
& ( B
= ( A @ D ) ) ) )
= ( (=) @ a @ C ) ) ) ) ) ).
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] :
( ( ^ [F: a] :
( ( A @ F )
& ( D
= ( C @ F ) ) ) )
= ( (=) @ a @ E ) ) ) )
=> ? [C: a > a] :
( ! [D: a] :
( ( B @ D )
=> ( A @ ( C @ D ) ) )
& ! [D: a] :
( ( A @ D )
=> ? [E: a] :
( ( ^ [F: a] :
( ( B @ F )
& ( D
= ( C @ F ) ) ) )
= ( (=) @ a @ E ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cEQP_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] :
( ( ^ [F: a] :
( ( A @ F )
& ( D
= ( C @ F ) ) ) )
= ( (=) @ a @ E ) ) ) )
=> ? [C: a > a] :
( ! [D: a] :
( ( B @ D )
=> ( A @ ( C @ D ) ) )
& ! [D: a] :
( ( A @ D )
=> ? [E: a] :
( ( ^ [F: a] :
( ( B @ F )
& ( D
= ( C @ F ) ) ) )
= ( (=) @ a @ 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] :
( ( ^ [F: a] :
( ( A @ F )
& ( D
= ( C @ F ) ) ) )
= ( (=) @ a @ E ) ) ) )
=> ? [C: a > a] :
( ! [D: a] :
( ( B @ D )
=> ( A @ ( C @ D ) ) )
& ! [D: a] :
( ( A @ D )
=> ? [E: a] :
( ( ^ [F: a] :
( ( B @ F )
& ( D
= ( C @ F ) ) ) )
= ( (=) @ a @ E ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
! [D: a,C: a > a,B: a,A: a] :
( ( ~ ( sk1 @ A )
| ( sk2 @ ( sk3 @ A ) ) )
& ( ~ ( sk2 @ B )
| ( ( ^ [E: a] :
( ( sk1 @ E )
& ( B
= ( sk3 @ E ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) ) )
& ( ( sk2 @ ( sk5 @ C ) )
| ( sk1 @ ( sk6 @ C ) ) )
& ( ( sk2 @ ( sk5 @ C ) )
| ( ( ^ [E: a] :
( ( sk2 @ E )
& ( ( sk6 @ C )
= ( C @ E ) ) ) )
!= ( (=) @ a @ D ) ) )
& ( ~ ( sk1 @ ( C @ ( sk5 @ C ) ) )
| ( sk1 @ ( sk6 @ C ) ) )
& ( ~ ( sk1 @ ( C @ ( sk5 @ C ) ) )
| ( ( ^ [E: a] :
( ( sk2 @ E )
& ( ( sk6 @ C )
= ( C @ E ) ) ) )
!= ( (=) @ a @ D ) ) ) ),
inference(cnf,[status(esa)],[3]) ).
thf(9,plain,
! [A: a] :
( ~ ( sk2 @ A )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( A
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ A ) ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(15,plain,
! [A: a] :
( ( ( ^ [B: a] :
( ( sk1 @ B )
& ( A
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ A ) ) )
| ~ ( sk2 @ A ) ),
inference(lifteq,[status(thm)],[9]) ).
thf(16,plain,
! [A: a] :
( ( ( ^ [B: a] :
( ( sk1 @ B )
& ( A
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ A ) ) )
| ~ ( sk2 @ A ) ),
inference(simp,[status(thm)],[15]) ).
thf(10,plain,
! [B: a,A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6 @ A )
= ( A @ C ) ) ) )
!= ( (=) @ a @ B ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(11,plain,
! [B: a,A: a > a] :
( ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6 @ A )
= ( A @ C ) ) ) )
!= ( (=) @ a @ B ) )
| ~ ( sk1 @ ( A @ ( sk5 @ A ) ) ) ),
inference(lifteq,[status(thm)],[10]) ).
thf(12,plain,
! [B: a,A: a > a] :
( ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6 @ A )
= ( A @ C ) ) ) )
!= ( (=) @ a @ B ) )
| ~ ( sk1 @ ( A @ ( sk5 @ A ) ) ) ),
inference(simp,[status(thm)],[11]) ).
thf(103,plain,
! [C: a,B: a > a,A: a] :
( ~ ( sk2 @ A )
| ( ( (=) @ a @ ( sk4 @ A ) )
!= ( (=) @ a @ C ) )
| ~ ( sk1 @ ( B @ ( sk5 @ B ) ) )
| ( ( ^ [D: a] :
( ( sk1 @ D )
& ( A
= ( sk3 @ D ) ) ) )
!= ( ^ [D: a] :
( ( sk2 @ D )
& ( ( sk6 @ B )
= ( B @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[16,12]) ).
thf(116,plain,
! [C: a,B: a > a,A: a] :
( ~ ( sk2 @ A )
| ( ( (=) @ a @ ( sk4 @ A ) )
!= ( (=) @ a @ C ) )
| ~ ( sk1 @ ( B @ ( sk5 @ B ) ) )
| ( sk2 != sk1 )
| ( ( ^ [D: a] :
( A
= ( sk3 @ D ) ) )
!= ( ^ [D: a] :
( ( sk6 @ B )
= ( B @ D ) ) ) ) ),
inference(simp,[status(thm)],[103]) ).
thf(7,plain,
! [A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( sk1 @ ( sk6 @ A ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(17,plain,
! [A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( sk1 @ ( sk6 @ A ) ) ),
inference(simp,[status(thm)],[7]) ).
thf(5,plain,
! [A: a] :
( ~ ( sk1 @ A )
| ( sk2 @ ( sk3 @ A ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(19,plain,
! [B: a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ~ $true
| ( sk2 @ ( sk3 @ B ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[17,5]) ).
thf(20,plain,
! [B: a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( sk2 @ ( sk3 @ B ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ B ) ) ),
inference(simp,[status(thm)],[19]) ).
thf(21,plain,
! [A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( sk2 @ ( sk3 @ ( sk6 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[20:[bind(A,$thf( C )),bind(B,$thf( sk6 @ C ))]]) ).
thf(22,plain,
! [A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( sk2 @ ( sk3 @ ( sk6 @ A ) ) ) ),
inference(simp,[status(thm)],[21]) ).
thf(85,plain,
! [B: a,A: a] :
( ( ( ( sk1 @ B )
& ( A
= ( sk3 @ B ) ) )
= ( ( sk4 @ A )
= B ) )
| ~ ( sk2 @ A ) ),
inference(func_ext,[status(esa)],[16]) ).
thf(1682,plain,
! [B: a,A: a] :
( ~ ( sk2 @ A )
| ( ( sk1 @ B )
& ( A
= ( sk3 @ B ) ) )
| ( ( sk4 @ A )
!= B ) ),
inference(bool_ext,[status(thm)],[85]) ).
thf(1748,plain,
! [B: a,A: a] :
( ( ( sk4 @ A )
!= B )
| ~ ( sk2 @ A )
| ( ( sk1 @ B )
& ( A
= ( sk3 @ B ) ) ) ),
inference(lifteq,[status(thm)],[1682]) ).
thf(1764,plain,
! [B: a,A: a] :
( ( ( ( sk4 @ A )
!= B )
| ~ ( sk2 @ A )
| ( sk1 @ B ) )
& ( ( ( sk4 @ A )
!= B )
| ~ ( sk2 @ A )
| ( A
= ( sk3 @ B ) ) ) ),
inference(cnf,[status(esa)],[1748]) ).
thf(1765,plain,
! [B: a,A: a] :
( ( ( sk4 @ A )
!= B )
| ~ ( sk2 @ A )
| ( sk1 @ B ) ),
inference(cnfConj,[status(thm)],[1764]) ).
thf(1767,plain,
! [A: a] :
( ~ ( sk2 @ A )
| ( sk1 @ ( sk4 @ A ) ) ),
inference(simp,[status(thm)],[1765]) ).
thf(1804,plain,
! [B: a,A: a > a] :
( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ~ $true
| ( sk1 @ ( sk4 @ B ) )
| ( ( sk2 @ ( sk5 @ A ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[22,1767]) ).
thf(1805,plain,
! [B: a,A: a > a] :
( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ( sk1 @ ( sk4 @ B ) )
| ( ( sk2 @ ( sk5 @ A ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[1804]) ).
thf(1806,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ( sk1 @ ( sk4 @ ( sk5 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[1805:[bind(A,$thf( C )),bind(B,$thf( sk5 @ C ))]]) ).
thf(1917,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ( sk1 @ ( sk4 @ ( sk5 @ A ) ) ) ),
inference(simp,[status(thm)],[1806]) ).
thf(8,plain,
! [A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( sk1 @ ( sk6 @ A ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(18,plain,
! [A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( sk1 @ ( sk6 @ A ) ) ),
inference(simp,[status(thm)],[8]) ).
thf(30,plain,
! [B: a,A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ~ $true
| ( sk2 @ ( sk3 @ B ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[18,5]) ).
thf(31,plain,
! [B: a,A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( sk2 @ ( sk3 @ B ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ B ) ) ),
inference(simp,[status(thm)],[30]) ).
thf(32,plain,
! [A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( sk2 @ ( sk3 @ ( sk6 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[31:[bind(A,$thf( C )),bind(B,$thf( sk6 @ C ))]]) ).
thf(35,plain,
! [A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( sk2 @ ( sk3 @ ( sk6 @ A ) ) ) ),
inference(simp,[status(thm)],[32]) ).
thf(3143,plain,
! [B: a > a,A: a > a] :
( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ~ $true
| ( sk2 @ ( sk3 @ ( sk6 @ B ) ) )
| ( ( sk1 @ ( sk4 @ ( sk5 @ A ) ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1917,35]) ).
thf(3144,plain,
! [B: a > a,A: a > a] :
( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ( sk2 @ ( sk3 @ ( sk6 @ B ) ) )
| ( ( sk1 @ ( sk4 @ ( sk5 @ A ) ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(simp,[status(thm)],[3143]) ).
thf(3195,plain,
( ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) )
| ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ),
inference(pre_uni,[status(thm)],[3144:[bind(A,$thf( sk4 )),bind(B,$thf( sk4 ))]]) ).
thf(3265,plain,
sk2 @ ( sk3 @ ( sk6 @ sk4 ) ),
inference(simp,[status(thm)],[3195]) ).
thf(3275,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ A ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3265,1767]) ).
thf(3276,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ A ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[3275]) ).
thf(3277,plain,
sk1 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[3276:[bind(A,$thf( sk3 @ ( sk6 @ sk4 ) ))]]) ).
thf(3589,plain,
! [A: a > a] :
( ~ $true
| ( sk1 @ ( sk6 @ A ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
!= ( sk1 @ ( A @ ( sk5 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3277,18]) ).
thf(3590,plain,
! [A: a > a] :
( ( sk1 @ ( sk6 @ A ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
!= ( sk1 @ ( A @ ( sk5 @ A ) ) ) ) ),
inference(simp,[status(thm)],[3589]) ).
thf(3602,plain,
( sk1
@ ( sk6
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ),
inference(pre_uni,[status(thm)],[3590:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ))]]) ).
thf(41,plain,
! [C: a,B: a > a,A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( ( ^ [D: a] :
( ( sk2 @ D )
& ( ( sk6 @ B )
= ( B @ D ) ) ) )
!= ( (=) @ a @ C ) )
| ~ $true
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[18,12]) ).
thf(42,plain,
! [C: a,B: a > a,A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( ( ^ [D: a] :
( ( sk2 @ D )
& ( ( sk6 @ B )
= ( B @ D ) ) ) )
!= ( (=) @ a @ C ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(simp,[status(thm)],[41]) ).
thf(44,plain,
! [B: a > a > a,A: a] :
( ~ ( sk1
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) )
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) ) ) )
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] : ( sk6 @ ( B @ D ) ) )
= ( sk6 @ ( B @ C ) ) ) ) )
!= ( (=) @ a @ A ) ) ),
inference(pre_uni,[status(thm)],[42:[bind(A,$thf( D @ ( sk5 @ ^ [E: a] : ( sk6 @ ( D @ E ) ) ) )),bind(B,$thf( ^ [E: a] : ( sk6 @ ( D @ E ) ) ))]]) ).
thf(46,plain,
! [B: a > a > a,A: a] :
( ~ ( sk1
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) )
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) ) ) )
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] : ( sk6 @ ( B @ D ) ) )
= ( sk6 @ ( B @ C ) ) ) ) )
!= ( (=) @ a @ A ) ) ),
inference(simp,[status(thm)],[44]) ).
thf(3914,plain,
! [B: a > a > a,A: a] :
( ~ $true
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] : ( sk6 @ ( B @ D ) ) )
= ( sk6 @ ( B @ C ) ) ) ) )
!= ( (=) @ a @ A ) )
| ( ( sk1
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) )
!= ( sk1
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) )
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3602,46]) ).
thf(3915,plain,
! [B: a > a > a,A: a] :
( ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] : ( sk6 @ ( B @ D ) ) )
= ( sk6 @ ( B @ C ) ) ) ) )
!= ( (=) @ a @ A ) )
| ( ( sk1
@ ( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) )
!= ( sk1
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) )
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3914]) ).
thf(3975,plain,
! [A: a] :
( ( ^ [B: a] :
( ( sk2 @ B )
& ( ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) )
= ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ) ) )
!= ( (=) @ a @ A ) ),
inference(pre_uni,[status(thm)],[3915:[bind(A,$thf( A )),bind(B,$thf( ^ [C: a] : ^ [D: a] : ( sk6 @ ^ [E: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ))]]) ).
thf(26,plain,
! [B: a > a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ~ $true
| ( sk1 @ ( sk6 @ B ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,18]) ).
thf(27,plain,
! [B: a > a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( sk1 @ ( sk6 @ B ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(simp,[status(thm)],[26]) ).
thf(33,plain,
! [A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) )
| ( sk1
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ),
inference(pre_uni,[status(thm)],[27:[bind(A,$thf( C @ ( sk5 @ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) )),bind(B,$thf( ^ [D: a] : ( sk6 @ ( C @ D ) ) ))]]) ).
thf(36,plain,
! [A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) )
| ( sk1
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ),
inference(simp,[status(thm)],[33]) ).
thf(56,plain,
! [B: a,A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) ) ) )
| ~ $true
| ( sk2 @ ( sk3 @ B ) )
| ( ( sk1
@ ( sk6
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) )
!= ( sk1 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[36,5]) ).
thf(57,plain,
! [B: a,A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) ) ) )
| ( sk2 @ ( sk3 @ B ) )
| ( ( sk1
@ ( sk6
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) )
!= ( sk1 @ B ) ) ),
inference(simp,[status(thm)],[56]) ).
thf(58,plain,
! [A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) )
| ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[57:[bind(A,$thf( D )),bind(B,$thf( sk6 @ ^ [D: a] : ( sk6 @ ( D @ D ) ) ))]]) ).
thf(71,plain,
! [A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) )
| ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ),
inference(simp,[status(thm)],[58]) ).
thf(161,plain,
! [B: a,A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) ) ) )
| ( ( ^ [C: a] :
( ( sk1 @ C )
& ( B
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) )
| ~ $true
| ( ( sk2
@ ( sk3
@ ( sk6
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[71,16]) ).
thf(162,plain,
! [B: a,A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) ) ) )
| ( ( ^ [C: a] :
( ( sk1 @ C )
& ( B
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) )
| ( ( sk2
@ ( sk3
@ ( sk6
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[161]) ).
thf(163,plain,
! [A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( ( sk3
@ ( sk6
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) )
= ( sk3 @ B ) ) ) )
= ( (=) @ a
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[162:[bind(A,$thf( E )),bind(B,$thf( sk3 @ ( sk6 @ ^ [D: a] : ( sk6 @ ( E @ D ) ) ) ))]]) ).
thf(175,plain,
! [A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( ( sk3
@ ( sk6
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) )
= ( sk3 @ B ) ) ) )
= ( (=) @ a
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[163]) ).
thf(3532,plain,
! [B: a > a > a,A: a] :
( ~ $true
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] : ( sk6 @ ( B @ D ) ) )
= ( sk6 @ ( B @ C ) ) ) ) )
!= ( (=) @ a @ A ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
!= ( sk1
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) )
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3277,46]) ).
thf(3533,plain,
! [B: a > a > a,A: a] :
( ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] : ( sk6 @ ( B @ D ) ) )
= ( sk6 @ ( B @ C ) ) ) ) )
!= ( (=) @ a @ A ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
!= ( sk1
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) )
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3532]) ).
thf(3625,plain,
! [A: a] :
( ( ^ [B: a] :
( ( sk2 @ B )
& ( ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) )
= ( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ) )
!= ( (=) @ a @ A ) ),
inference(pre_uni,[status(thm)],[3533:[bind(A,$thf( A )),bind(B,$thf( ^ [C: a] : ^ [D: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ))]]) ).
thf(74,plain,
! [B: a > a,A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ~ $true
| ( sk2 @ ( sk3 @ ( sk6 @ B ) ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[18,35]) ).
thf(75,plain,
! [B: a > a,A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( sk2 @ ( sk3 @ ( sk6 @ B ) ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(simp,[status(thm)],[74]) ).
thf(79,plain,
! [A: a > a > a] :
( ~ ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) )
| ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[75:[bind(A,$thf( C @ ( sk5 @ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) )),bind(B,$thf( ^ [D: a] : ( sk6 @ ( C @ D ) ) ))]]) ).
thf(83,plain,
! [A: a > a > a] :
( ~ ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) )
| ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ),
inference(simp,[status(thm)],[79]) ).
thf(3166,plain,
! [B: a > a > a,A: a > a] :
( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ~ $true
| ( sk2
@ ( sk3
@ ( sk6
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) )
| ( ( sk1 @ ( sk4 @ ( sk5 @ A ) ) )
!= ( sk1
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) )
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1917,83]) ).
thf(3167,plain,
! [B: a > a > a,A: a > a] :
( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ( sk2
@ ( sk3
@ ( sk6
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) )
| ( ( sk1 @ ( sk4 @ ( sk5 @ A ) ) )
!= ( sk1
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) )
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3166]) ).
thf(3169,plain,
( ( sk2
@ ( sk3
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] : ( sk4 @ A ) ) ) ) )
| ( sk2
@ ( sk3
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[3167:[bind(A,$thf( ^ [C: a] : ( sk6 @ ^ [D: a] : ( sk4 @ C ) ) )),bind(B,$thf( ^ [C: a] : ^ [D: a] : ( sk4 @ C ) ))]]) ).
thf(3255,plain,
( sk2
@ ( sk3
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ),
inference(simp,[status(thm)],[3169]) ).
thf(3347,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ A ) )
| ( ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3255,1767]) ).
thf(3348,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ A ) )
| ( ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[3347]) ).
thf(3349,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[3348:[bind(A,$thf( sk3 @ ( sk6 @ ^ [B: a] : ( sk6 @ ^ [C: a] : ( sk4 @ B ) ) ) ))]]) ).
thf(3746,plain,
! [B: a,A: a > a] :
( ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6 @ A )
= ( A @ C ) ) ) )
!= ( (=) @ a @ B ) )
| ~ $true
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk5 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3349,12]) ).
thf(3747,plain,
! [B: a,A: a > a] :
( ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6 @ A )
= ( A @ C ) ) ) )
!= ( (=) @ a @ B ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk5 @ A ) ) ) ) ),
inference(simp,[status(thm)],[3746]) ).
thf(3777,plain,
! [A: a] :
( ( ^ [B: a] :
( ( sk2 @ B )
& ( ( sk6
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) )
= ( sk4
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ) )
!= ( (=) @ a @ A ) ),
inference(pre_uni,[status(thm)],[3747:[bind(A,$thf( ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ ^ [D: a] : ( sk6 @ ^ [E: a] : ( sk4 @ D ) ) ) ) ) )),bind(B,$thf( B ))]]) ).
thf(3798,plain,
! [A: a] :
( ( ^ [B: a] :
( ( sk2 @ B )
& ( ( sk6
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) )
= ( sk4
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ) )
!= ( (=) @ a @ A ) ),
inference(simp,[status(thm)],[3777]) ).
thf(117,plain,
! [C: a,B: a > a,A: a] :
( ~ ( sk2 @ A )
| ( ( ^ [D: a] : ( sk4 @ A ) )
!= ( ^ [D: a] : C ) )
| ( ( ^ [D: a] : D )
!= ( ^ [D: a] : D ) )
| ~ ( sk1 @ ( B @ ( sk5 @ B ) ) )
| ( sk2 != sk1 )
| ( ( ^ [D: a] :
( A
= ( sk3 @ D ) ) )
!= ( ^ [D: a] :
( ( sk6 @ B )
= ( B @ D ) ) ) ) ),
inference(simp,[status(thm)],[103]) ).
thf(128,plain,
! [C: a,B: a > a,A: a] :
( ~ ( sk2 @ A )
| ( ( ^ [D: a] : ( sk4 @ A ) )
!= ( ^ [D: a] : C ) )
| ~ ( sk1 @ ( B @ ( sk5 @ B ) ) )
| ( sk2 != sk1 )
| ( ( ^ [D: a] :
( A
= ( sk3 @ D ) ) )
!= ( ^ [D: a] :
( ( sk6 @ B )
= ( B @ D ) ) ) ) ),
inference(simp,[status(thm)],[117]) ).
thf(176,plain,
! [C: a,B: a > a,A: a] :
( ~ ( sk2 @ A )
| ( ( ^ [D: a] : ( sk4 @ A ) )
!= ( ^ [D: a] : C ) )
| ~ ( sk1 @ ( B @ ( sk5 @ B ) ) )
| ( sk2 != sk1 )
| ( ( ^ [D: a] : A )
!= ( ^ [D: a] : ( sk6 @ B ) ) )
| ( sk3 != B ) ),
inference(simp,[status(thm)],[128]) ).
thf(216,plain,
! [B: a,A: a] :
( ~ ( sk2 @ A )
| ( ( ^ [C: a] : ( sk4 @ A ) )
!= ( ^ [C: a] : B ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [C: a] : A )
!= ( ^ [C: a] : ( sk6 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[176]) ).
thf(228,plain,
! [B: a,A: a] :
( ( ( sk4 @ A )
!= B )
| ( ( sk2 @ ( sk14 @ B @ A ) )
!= ( sk1 @ ( sk14 @ B @ A ) ) )
| ( ( sk6 @ sk3 )
!= A )
| ~ ( sk2 @ A )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) ) ),
inference(func_ext,[status(esa)],[216]) ).
thf(267,plain,
( ( ( sk2 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
!= ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) ) )
| ~ ( sk2 @ ( sk6 @ sk3 ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[228]) ).
thf(525,plain,
( ~ ( sk2 @ ( sk6 @ sk3 ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ~ ( sk2 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
| ~ ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) ) ),
inference(bool_ext,[status(thm)],[267]) ).
thf(661,plain,
( ~ ( sk2 @ ( sk6 @ sk3 ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ~ ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
| ( ( sk2 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
!= ( sk2 @ ( sk6 @ sk3 ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[525]) ).
thf(666,plain,
( ~ ( sk2 @ ( sk6 @ sk3 ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ~ ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
| ( ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) )
!= ( sk6 @ sk3 ) ) ),
inference(simp,[status(thm)],[661]) ).
thf(1820,plain,
! [B: a,A: a] :
( ~ ( sk2 @ A )
| ~ $true
| ( sk2 @ ( sk3 @ B ) )
| ( ( sk1 @ ( sk4 @ A ) )
!= ( sk1 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[1767,5]) ).
thf(1821,plain,
! [B: a,A: a] :
( ~ ( sk2 @ A )
| ( sk2 @ ( sk3 @ B ) )
| ( ( sk1 @ ( sk4 @ A ) )
!= ( sk1 @ B ) ) ),
inference(simp,[status(thm)],[1820]) ).
thf(1822,plain,
! [A: a] :
( ~ ( sk2 @ A )
| ( sk2 @ ( sk3 @ ( sk4 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[1821:[bind(A,$thf( C )),bind(B,$thf( sk4 @ C ))]]) ).
thf(1921,plain,
! [A: a] :
( ~ ( sk2 @ A )
| ( sk2 @ ( sk3 @ ( sk4 @ A ) ) ) ),
inference(simp,[status(thm)],[1822]) ).
thf(2264,plain,
! [B: a,A: a] :
( ~ ( sk2 @ A )
| ~ $true
| ( sk1 @ ( sk4 @ B ) )
| ( ( sk2 @ ( sk3 @ ( sk4 @ A ) ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[1921,1767]) ).
thf(2265,plain,
! [B: a,A: a] :
( ~ ( sk2 @ A )
| ( sk1 @ ( sk4 @ B ) )
| ( ( sk2 @ ( sk3 @ ( sk4 @ A ) ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[2264]) ).
thf(2266,plain,
! [A: a] :
( ~ ( sk2 @ A )
| ( sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) ),
inference(pattern_uni,[status(thm)],[2265:[bind(A,$thf( D )),bind(B,$thf( sk3 @ ( sk4 @ D ) ))]]) ).
thf(2363,plain,
! [A: a] :
( ~ ( sk2 @ A )
| ( sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) ) ),
inference(simp,[status(thm)],[2266]) ).
thf(1823,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A )
| ~ $true
| ( sk1 @ ( sk4 @ B ) )
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[5,1767]) ).
thf(1824,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A )
| ( sk1 @ ( sk4 @ B ) )
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[1823]) ).
thf(1825,plain,
! [A: a] :
( ~ ( sk1 @ A )
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[1824:[bind(A,$thf( C )),bind(B,$thf( sk3 @ C ))]]) ).
thf(1924,plain,
! [A: a] :
( ~ ( sk1 @ A )
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) ) ),
inference(simp,[status(thm)],[1825]) ).
thf(97,plain,
! [B: a,A: a > a] :
( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ( ( ^ [C: a] :
( ( sk1 @ C )
& ( B
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) )
| ~ $true
| ( ( sk2 @ ( sk5 @ A ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[22,16]) ).
thf(98,plain,
! [B: a,A: a > a] :
( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ( ( ^ [C: a] :
( ( sk1 @ C )
& ( B
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) )
| ( ( sk2 @ ( sk5 @ A ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[97]) ).
thf(99,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( ( sk5 @ A )
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ ( sk5 @ A ) ) ) ) ),
inference(pattern_uni,[status(thm)],[98:[bind(A,$thf( C )),bind(B,$thf( sk5 @ C ))]]) ).
thf(120,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( ( sk5 @ A )
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ ( sk5 @ A ) ) ) ) ),
inference(simp,[status(thm)],[99]) ).
thf(229,plain,
! [C: a,B: a,A: a] :
( ~ ( sk1 @ A )
| ~ $true
| ( ( ^ [D: a] : ( sk4 @ B ) )
!= ( ^ [D: a] : C ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [D: a] : B )
!= ( ^ [D: a] : ( sk6 @ sk3 ) ) )
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[5,216]) ).
thf(230,plain,
! [C: a,B: a,A: a] :
( ~ ( sk1 @ A )
| ( ( ^ [D: a] : ( sk4 @ B ) )
!= ( ^ [D: a] : C ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [D: a] : B )
!= ( ^ [D: a] : ( sk6 @ sk3 ) ) )
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[229]) ).
thf(231,plain,
! [B: a,A: a] :
( ~ ( sk1 @ B )
| ( ( ^ [C: a] : ( sk4 @ ( sk3 @ B ) ) )
!= ( ^ [C: a] : A ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [C: a] : ( sk3 @ B ) )
!= ( ^ [C: a] : ( sk6 @ sk3 ) ) ) ),
inference(pattern_uni,[status(thm)],[230:[bind(A,$thf( D )),bind(B,$thf( sk3 @ D ))]]) ).
thf(269,plain,
! [B: a,A: a] :
( ~ ( sk1 @ B )
| ( ( ^ [C: a] : ( sk4 @ ( sk3 @ B ) ) )
!= ( ^ [C: a] : A ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [C: a] : ( sk3 @ B ) )
!= ( ^ [C: a] : ( sk6 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[231]) ).
thf(1766,plain,
! [B: a,A: a] :
( ( ( sk4 @ A )
!= B )
| ~ ( sk2 @ A )
| ( A
= ( sk3 @ B ) ) ),
inference(cnfConj,[status(thm)],[1764]) ).
thf(1768,plain,
! [B: a,A: a] :
( ( A
= ( sk3 @ B ) )
| ( ( sk4 @ A )
!= B )
| ~ ( sk2 @ A ) ),
inference(lifteq,[status(thm)],[1766]) ).
thf(1769,plain,
! [A: a] :
( ( ( sk3 @ ( sk4 @ A ) )
= A )
| ~ ( sk2 @ A ) ),
inference(simp,[status(thm)],[1768]) ).
thf(6870,plain,
! [A: a] :
( ( ( sk3 @ ( sk4 @ A ) )
= A )
| ~ $true
| ( ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3265,1769]) ).
thf(6871,plain,
! [A: a] :
( ( ( sk3 @ ( sk4 @ A ) )
= A )
| ( ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[6870]) ).
thf(6872,plain,
( ( sk3 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
= ( sk3 @ ( sk6 @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[6871:[bind(A,$thf( sk3 @ ( sk6 @ sk4 ) ))]]) ).
thf(23,plain,
! [A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
!= ( sk2 @ ( sk5 @ A ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[22]) ).
thf(24,plain,
! [A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
!= ( sk2 @ ( sk5 @ A ) ) ) ),
inference(simp,[status(thm)],[23]) ).
thf(28,plain,
! [B: a > a,A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ~ $true
| ( sk1 @ ( sk6 @ B ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[18,18]) ).
thf(29,plain,
! [B: a > a,A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( sk1 @ ( sk6 @ B ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(simp,[status(thm)],[28]) ).
thf(34,plain,
! [A: a > a > a] :
( ~ ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) )
| ( sk1
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ),
inference(pre_uni,[status(thm)],[29:[bind(A,$thf( C @ ( sk5 @ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) )),bind(B,$thf( ^ [D: a] : ( sk6 @ ( C @ D ) ) ))]]) ).
thf(37,plain,
! [A: a > a > a] :
( ~ ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) )
| ( sk1
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ),
inference(simp,[status(thm)],[34]) ).
thf(25,plain,
! [A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( ( sk3 @ ( sk6 @ A ) )
!= ( sk5 @ A ) ) ),
inference(simp,[status(thm)],[23]) ).
thf(6,plain,
! [B: a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6 @ A )
= ( A @ C ) ) ) )
!= ( (=) @ a @ B ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(13,plain,
! [B: a,A: a > a] :
( ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6 @ A )
= ( A @ C ) ) ) )
!= ( (=) @ a @ B ) )
| ( sk2 @ ( sk5 @ A ) ) ),
inference(lifteq,[status(thm)],[6]) ).
thf(14,plain,
! [B: a,A: a > a] :
( ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6 @ A )
= ( A @ C ) ) ) )
!= ( (=) @ a @ B ) )
| ( sk2 @ ( sk5 @ A ) ) ),
inference(simp,[status(thm)],[13]) ).
thf(93,plain,
! [C: a > a > a,B: a,A: a] :
( ~ ( sk2 @ A )
| ~ ( sk1
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) )
@ ( sk5
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ) ) ) )
| ( ( (=) @ a @ ( sk4 @ A ) )
!= ( (=) @ a @ B ) )
| ( ( ^ [D: a] :
( ( sk2 @ D )
& ( ( sk6
@ ^ [E: a] : ( sk6 @ ( C @ E ) ) )
= ( sk6 @ ( C @ D ) ) ) ) )
!= ( ^ [D: a] :
( ( sk1 @ D )
& ( A
= ( sk3 @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[16,46]) ).
thf(110,plain,
! [C: a > a > a,B: a,A: a] :
( ~ ( sk2 @ A )
| ~ ( sk1
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) )
@ ( sk5
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ) ) ) )
| ( ( (=) @ a @ ( sk4 @ A ) )
!= ( (=) @ a @ B ) )
| ( sk2 != sk1 )
| ( ( ^ [D: a] :
( ( sk6
@ ^ [E: a] : ( sk6 @ ( C @ E ) ) )
= ( sk6 @ ( C @ D ) ) ) )
!= ( ^ [D: a] :
( A
= ( sk3 @ D ) ) ) ) ),
inference(simp,[status(thm)],[93]) ).
thf(3361,plain,
! [B: a,A: a] :
( ~ $true
| ( ( ^ [C: a] : ( sk4 @ A ) )
!= ( ^ [C: a] : B ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [C: a] : A )
!= ( ^ [C: a] : ( sk6 @ sk3 ) ) )
| ( ( sk2
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3255,216]) ).
thf(3362,plain,
! [B: a,A: a] :
( ( ( ^ [C: a] : ( sk4 @ A ) )
!= ( ^ [C: a] : B ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [C: a] : A )
!= ( ^ [C: a] : ( sk6 @ sk3 ) ) )
| ( ( sk2
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[3361]) ).
thf(3363,plain,
! [A: a] :
( ( ( ^ [B: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) )
!= ( ^ [B: a] : A ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [B: a] :
( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) )
!= ( ^ [B: a] : ( sk6 @ sk3 ) ) ) ),
inference(pattern_uni,[status(thm)],[3362:[bind(A,$thf( sk3 @ ( sk6 @ ^ [C: a] : ( sk6 @ ^ [D: a] : ( sk4 @ C ) ) ) )),bind(B,$thf( B ))]]) ).
thf(3410,plain,
! [A: a] :
( ( ( ^ [B: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) )
!= ( ^ [B: a] : A ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [B: a] :
( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) )
!= ( ^ [B: a] : ( sk6 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[3363]) ).
thf(3759,plain,
! [A: a > a] :
( ~ $true
| ( sk1 @ ( sk6 @ A ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk5 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3349,18]) ).
thf(3760,plain,
! [A: a > a] :
( ( sk1 @ ( sk6 @ A ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk5 @ A ) ) ) ) ),
inference(simp,[status(thm)],[3759]) ).
thf(3788,plain,
( sk1
@ ( sk6
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[3760:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ ^ [C: a] : ( sk6 @ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ))]]) ).
thf(4567,plain,
! [A: a > a > a] :
( ~ $true
| ( sk1
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3788,37]) ).
thf(4568,plain,
! [A: a > a > a] :
( ( sk1
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[4567]) ).
thf(4622,plain,
( sk1
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[4568:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk6 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk6 @ ^ [E: a] : ( sk6 @ ^ [F: a] : ( sk4 @ E ) ) ) ) ) ) ))]]) ).
thf(3560,plain,
! [A: a > a > a] :
( ~ $true
| ( sk1
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3277,37]) ).
thf(3561,plain,
! [A: a > a > a] :
( ( sk1
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3560]) ).
thf(3603,plain,
( sk1
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[3561:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ))]]) ).
thf(4292,plain,
! [A: a > a > a] :
( ~ $true
| ( sk1
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3603,37]) ).
thf(4293,plain,
! [A: a > a > a] :
( ( sk1
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[4292]) ).
thf(4368,plain,
( sk1
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[4293:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk6 @ ^ [D: a] : ( sk6 @ ^ [E: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ))]]) ).
thf(665,plain,
( ~ ( sk2 @ ( sk6 @ sk3 ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ~ ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
| ( ( sk2 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
!= ( sk2 @ ( sk6 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[661]) ).
thf(3297,plain,
( ~ ( sk2 @ ( sk6 @ sk3 ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ~ ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
| ~ ( sk2 @ ( sk6 @ sk3 ) )
| ( ( sk2 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
!= ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3265,665]) ).
thf(3298,plain,
( ~ ( sk2 @ ( sk6 @ sk3 ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ~ ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
| ( ( sk2 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
!= ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ),
inference(simp,[status(thm)],[3297]) ).
thf(3322,plain,
( ~ ( sk2 @ ( sk6 @ sk3 ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ~ ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
| ( ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) )
!= ( sk3 @ ( sk6 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[3298]) ).
thf(3280,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3265,2363]) ).
thf(3281,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[3280]) ).
thf(3282,plain,
sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ),
inference(pattern_uni,[status(thm)],[3281:[bind(A,$thf( sk3 @ ( sk6 @ sk4 ) ))]]) ).
thf(4004,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3282,1924]) ).
thf(4005,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[4004]) ).
thf(4006,plain,
sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[4005:[bind(A,$thf( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ))]]) ).
thf(7786,plain,
sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ),
inference(rewrite,[status(thm)],[4006,6872]) ).
thf(100,plain,
! [B: a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( ( ^ [C: a] :
( ( sk1 @ C )
& ( B
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) )
| ~ $true
| ( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[22,16]) ).
thf(101,plain,
! [B: a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( ( ^ [C: a] :
( ( sk1 @ C )
& ( B
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[100]) ).
thf(102,plain,
! [A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( ( sk3 @ ( sk6 @ A ) )
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ ( sk3 @ ( sk6 @ A ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[101:[bind(A,$thf( D )),bind(B,$thf( sk3 @ ( sk6 @ D ) ))]]) ).
thf(121,plain,
! [A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( ( sk3 @ ( sk6 @ A ) )
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ ( sk3 @ ( sk6 @ A ) ) ) ) ) ),
inference(simp,[status(thm)],[102]) ).
thf(84,plain,
! [B: a,A: a > a] :
( ( ( ( sk2 @ ( sk9 @ B @ A ) )
& ( ( sk6 @ A )
= ( A @ ( sk9 @ B @ A ) ) ) )
!= ( B
= ( sk9 @ B @ A ) ) )
| ( sk2 @ ( sk5 @ A ) ) ),
inference(func_ext,[status(esa)],[14]) ).
thf(3912,plain,
! [A: a > a > a] :
( ~ $true
| ( sk1
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3602,37]) ).
thf(3913,plain,
! [A: a > a > a] :
( ( sk1
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3912]) ).
thf(3984,plain,
( sk1
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[3913:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk6 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ))]]) ).
thf(38,plain,
! [B: a,A: a > a] :
( ( ( ( sk2 @ ( sk7 @ B @ A ) )
& ( ( sk6 @ A )
= ( A @ ( sk7 @ B @ A ) ) ) )
!= ( B
= ( sk7 @ B @ A ) ) )
| ~ ( sk1 @ ( A @ ( sk5 @ A ) ) ) ),
inference(func_ext,[status(esa)],[12]) ).
thf(63,plain,
! [B: a > a,A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) ) ) )
| ~ $true
| ( sk1 @ ( sk6 @ B ) )
| ( ( sk1
@ ( sk6
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[36,18]) ).
thf(64,plain,
! [B: a > a,A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) ) ) )
| ( sk1 @ ( sk6 @ B ) )
| ( ( sk1
@ ( sk6
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(simp,[status(thm)],[63]) ).
thf(67,plain,
! [A: a > a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk6 @ ( A @ B @ C ) ) ) )
@ ( sk5
@ ^ [B: a] :
( sk6
@ ( A
@ ( sk5
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk6 @ ( A @ C @ D ) ) ) )
@ B ) ) ) ) ) )
| ( sk1
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk6 @ ( A @ B @ C ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[64:[bind(A,$thf( D @ ( sk5 @ ^ [D: a] : ( sk6 @ ^ [E: a] : ( sk6 @ ( D @ D @ E ) ) ) ) )),bind(B,$thf( ^ [D: a] : ( sk6 @ ^ [E: a] : ( sk6 @ ( D @ D @ E ) ) ) ))]]) ).
thf(70,plain,
! [A: a > a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk6 @ ( A @ B @ C ) ) ) )
@ ( sk5
@ ^ [B: a] :
( sk6
@ ( A
@ ( sk5
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk6 @ ( A @ C @ D ) ) ) )
@ B ) ) ) ) ) )
| ( sk1
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk6 @ ( A @ B @ C ) ) ) ) ) ),
inference(simp,[status(thm)],[67]) ).
thf(3753,plain,
! [A: a > a] :
( ~ $true
| ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk5 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3349,35]) ).
thf(3754,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1 @ ( A @ ( sk5 @ A ) ) ) ) ),
inference(simp,[status(thm)],[3753]) ).
thf(3778,plain,
( sk2
@ ( sk3
@ ( sk6
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[3754:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ ^ [C: a] : ( sk6 @ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ))]]) ).
thf(1851,plain,
! [B: a,A: a > a] :
( ( sk1 @ ( sk6 @ A ) )
| ~ $true
| ( sk1 @ ( sk4 @ B ) )
| ( ( sk2 @ ( sk5 @ A ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[17,1767]) ).
thf(1852,plain,
! [B: a,A: a > a] :
( ( sk1 @ ( sk6 @ A ) )
| ( sk1 @ ( sk4 @ B ) )
| ( ( sk2 @ ( sk5 @ A ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[1851]) ).
thf(1853,plain,
! [A: a > a] :
( ( sk1 @ ( sk6 @ A ) )
| ( sk1 @ ( sk4 @ ( sk5 @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[1852:[bind(A,$thf( C )),bind(B,$thf( sk5 @ C ))]]) ).
thf(1938,plain,
! [A: a > a] :
( ( sk1 @ ( sk6 @ A ) )
| ( sk1 @ ( sk4 @ ( sk5 @ A ) ) ) ),
inference(simp,[status(thm)],[1853]) ).
thf(136,plain,
! [B: a > a,A: a] :
( ~ ( sk1 @ A )
| ( sk2 @ ( sk5 @ B ) )
| ~ ( sk2 @ ( sk3 @ ( sk6 @ B ) ) )
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ ( sk5 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[5,24]) ).
thf(157,plain,
! [B: a > a,A: a] :
( ( sk2 @ ( sk5 @ B ) )
| ~ ( sk1 @ A )
| ~ ( sk2 @ ( sk3 @ ( sk6 @ B ) ) )
| ( ( sk3 @ A )
!= ( sk5 @ B ) ) ),
inference(simp,[status(thm)],[136]) ).
thf(774,plain,
! [C: a > a,B: a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( sk2 @ ( sk5 @ C ) )
| ~ ( sk1 @ B )
| ~ $true
| ( ( sk3 @ B )
!= ( sk5 @ C ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
!= ( sk2 @ ( sk3 @ ( sk6 @ C ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[22,157]) ).
thf(775,plain,
! [C: a > a,B: a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( sk2 @ ( sk5 @ C ) )
| ~ ( sk1 @ B )
| ( ( sk3 @ B )
!= ( sk5 @ C ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
!= ( sk2 @ ( sk3 @ ( sk6 @ C ) ) ) ) ),
inference(simp,[status(thm)],[774]) ).
thf(776,plain,
! [B: a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( sk2 @ ( sk5 @ A ) )
| ~ ( sk1 @ B )
| ( ( sk3 @ B )
!= ( sk5 @ A ) ) ),
inference(pattern_uni,[status(thm)],[775:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A ))]]) ).
thf(842,plain,
! [B: a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ~ ( sk1 @ B )
| ( ( sk3 @ B )
!= ( sk5 @ A ) ) ),
inference(simp,[status(thm)],[776]) ).
thf(2269,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A )
| ~ $true
| ( sk2 @ ( sk3 @ ( sk4 @ B ) ) )
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[5,1921]) ).
thf(2270,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A )
| ( sk2 @ ( sk3 @ ( sk4 @ B ) ) )
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[2269]) ).
thf(2271,plain,
! [A: a] :
( ~ ( sk1 @ A )
| ( sk2 @ ( sk3 @ ( sk4 @ ( sk3 @ A ) ) ) ) ),
inference(pattern_uni,[status(thm)],[2270:[bind(A,$thf( C )),bind(B,$thf( sk3 @ C ))]]) ).
thf(2365,plain,
! [A: a] :
( ~ ( sk1 @ A )
| ( sk2 @ ( sk3 @ ( sk4 @ ( sk3 @ A ) ) ) ) ),
inference(simp,[status(thm)],[2271]) ).
thf(3748,plain,
! [A: a] :
( ~ $true
| ( sk2 @ ( sk3 @ ( sk4 @ ( sk3 @ A ) ) ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3349,2365]) ).
thf(3749,plain,
! [A: a] :
( ( sk2 @ ( sk3 @ ( sk4 @ ( sk3 @ A ) ) ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[3748]) ).
thf(3750,plain,
( sk2
@ ( sk3
@ ( sk4
@ ( sk3
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[3749:[bind(A,$thf( sk4 @ ( sk3 @ ( sk6 @ ^ [B: a] : ( sk6 @ ^ [C: a] : ( sk4 @ B ) ) ) ) ))]]) ).
thf(3730,plain,
! [A: a > a > a] :
( ~ $true
| ( sk1
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3349,37]) ).
thf(3731,plain,
! [A: a > a > a] :
( ( sk1
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3730]) ).
thf(3775,plain,
( sk1
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[3731:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ ^ [D: a] : ( sk6 @ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ))]]) ).
thf(3006,plain,
! [B: a,A: a] :
( ( ( ^ [C: a] : ( sk4 @ ( sk3 @ B ) ) )
!= ( ^ [C: a] : A ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [C: a] : ( sk3 @ B ) )
!= ( ^ [C: a] : ( sk6 @ sk3 ) ) )
| ( ( sk1 @ B )
!= ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[269]) ).
thf(3010,plain,
! [A: a] :
( ( ( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk3 @ ( sk5 @ sk3 ) ) ) ) )
!= ( ^ [B: a] : A ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [B: a] : ( sk6 @ sk3 ) )
!= ( ^ [B: a] : ( sk3 @ ( sk3 @ ( sk5 @ sk3 ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[3006:[bind(A,$thf( A )),bind(B,$thf( sk3 @ ( sk5 @ sk3 ) ))]]) ).
thf(3702,plain,
! [B: a > a > a,A: a] :
( ~ $true
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] : ( sk6 @ ( B @ D ) ) )
= ( sk6 @ ( B @ C ) ) ) ) )
!= ( (=) @ a @ A ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) )
!= ( sk1
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) )
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3349,46]) ).
thf(3703,plain,
! [B: a > a > a,A: a] :
( ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] : ( sk6 @ ( B @ D ) ) )
= ( sk6 @ ( B @ C ) ) ) ) )
!= ( (=) @ a @ A ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) )
!= ( sk1
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) )
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3702]) ).
thf(3787,plain,
! [A: a] :
( ( ^ [B: a] :
( ( sk2 @ B )
& ( ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [E: a] :
( sk6
@ ^ [F: a] : ( sk4 @ E ) ) ) ) ) ) )
= ( sk6
@ ^ [C: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ) ) ) )
!= ( (=) @ a @ A ) ),
inference(pre_uni,[status(thm)],[3703:[bind(A,$thf( A )),bind(B,$thf( ^ [C: a] : ^ [D: a] : ( sk4 @ ( sk3 @ ( sk6 @ ^ [E: a] : ( sk6 @ ^ [F: a] : ( sk4 @ E ) ) ) ) ) ))]]) ).
thf(3352,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) )
| ( ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3255,2363]) ).
thf(3353,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ A ) ) ) )
| ( ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[3352]) ).
thf(3354,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[3353:[bind(A,$thf( sk3 @ ( sk6 @ ^ [B: a] : ( sk6 @ ^ [C: a] : ( sk4 @ B ) ) ) ))]]) ).
thf(3935,plain,
! [A: a] :
( ~ $true
| ( sk2 @ ( sk3 @ ( sk4 @ ( sk3 @ A ) ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3602,2365]) ).
thf(3936,plain,
! [A: a] :
( ( sk2 @ ( sk3 @ ( sk4 @ ( sk3 @ A ) ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[3935]) ).
thf(3937,plain,
( sk2
@ ( sk3
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[3936:[bind(A,$thf( sk6 @ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ))]]) ).
thf(86,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A )
| ( ( ^ [C: a] :
( ( sk1 @ C )
& ( B
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) )
| ~ $true
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[5,16]) ).
thf(87,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A )
| ( ( ^ [C: a] :
( ( sk1 @ C )
& ( B
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) )
| ( ( sk2 @ ( sk3 @ A ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[86]) ).
thf(88,plain,
! [A: a] :
( ~ ( sk1 @ A )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( ( sk3 @ A )
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ ( sk3 @ A ) ) ) ) ),
inference(pattern_uni,[status(thm)],[87:[bind(A,$thf( C )),bind(B,$thf( sk3 @ C ))]]) ).
thf(129,plain,
! [A: a] :
( ~ ( sk1 @ A )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( ( sk3 @ A )
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ ( sk3 @ A ) ) ) ) ),
inference(simp,[status(thm)],[88]) ).
thf(3576,plain,
! [B: a,A: a > a] :
( ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6 @ A )
= ( A @ C ) ) ) )
!= ( (=) @ a @ B ) )
| ~ $true
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
!= ( sk1 @ ( A @ ( sk5 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3277,12]) ).
thf(3577,plain,
! [B: a,A: a > a] :
( ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6 @ A )
= ( A @ C ) ) ) )
!= ( (=) @ a @ B ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
!= ( sk1 @ ( A @ ( sk5 @ A ) ) ) ) ),
inference(simp,[status(thm)],[3576]) ).
thf(3599,plain,
! [A: a] :
( ( ^ [B: a] :
( ( sk2 @ B )
& ( ( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
= ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) )
!= ( (=) @ a @ A ) ),
inference(pre_uni,[status(thm)],[3577:[bind(A,$thf( ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )),bind(B,$thf( B ))]]) ).
thf(3628,plain,
! [A: a] :
( ( ^ [B: a] :
( ( sk2 @ B )
& ( ( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
= ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) )
!= ( (=) @ a @ A ) ),
inference(simp,[status(thm)],[3599]) ).
thf(3901,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3602,1924]) ).
thf(3902,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[3901]) ).
thf(3903,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[3902:[bind(A,$thf( sk6 @ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ))]]) ).
thf(3583,plain,
! [A: a > a] :
( ~ $true
| ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
!= ( sk1 @ ( A @ ( sk5 @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3277,35]) ).
thf(3584,plain,
! [A: a > a] :
( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
!= ( sk1 @ ( A @ ( sk5 @ A ) ) ) ) ),
inference(simp,[status(thm)],[3583]) ).
thf(3624,plain,
( sk2
@ ( sk3
@ ( sk6
@ ^ [A: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[3584:[bind(A,$thf( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ))]]) ).
thf(1202,plain,
( ~ ( sk2 @ ( sk6 @ sk3 ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) )
!= ( sk6 @ sk3 ) )
| ( ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
!= ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[666]) ).
thf(1219,plain,
( ~ ( sk2 @ ( sk6 @ sk3 ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) )
!= ( sk6 @ sk3 ) )
| ( ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) )
!= ( sk3 @ ( sk5 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[1202]) ).
thf(39,plain,
! [C: a,B: a > a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( ( ^ [D: a] :
( ( sk2 @ D )
& ( ( sk6 @ B )
= ( B @ D ) ) ) )
!= ( (=) @ a @ C ) )
| ~ $true
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,12]) ).
thf(40,plain,
! [C: a,B: a > a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( ( ^ [D: a] :
( ( sk2 @ D )
& ( ( sk6 @ B )
= ( B @ D ) ) ) )
!= ( (=) @ a @ C ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(simp,[status(thm)],[39]) ).
thf(43,plain,
! [B: a > a > a,A: a] :
( ( sk2
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) ) )
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] : ( sk6 @ ( B @ D ) ) )
= ( sk6 @ ( B @ C ) ) ) ) )
!= ( (=) @ a @ A ) ) ),
inference(pre_uni,[status(thm)],[40:[bind(A,$thf( D @ ( sk5 @ ^ [E: a] : ( sk6 @ ( D @ E ) ) ) )),bind(B,$thf( ^ [E: a] : ( sk6 @ ( D @ E ) ) ))]]) ).
thf(45,plain,
! [B: a > a > a,A: a] :
( ( sk2
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) ) )
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] : ( sk6 @ ( B @ D ) ) )
= ( sk6 @ ( B @ C ) ) ) ) )
!= ( (=) @ a @ A ) ) ),
inference(simp,[status(thm)],[43]) ).
thf(3289,plain,
! [B: a,A: a] :
( ~ $true
| ( ( ^ [C: a] : ( sk4 @ A ) )
!= ( ^ [C: a] : B ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [C: a] : A )
!= ( ^ [C: a] : ( sk6 @ sk3 ) ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3265,216]) ).
thf(3290,plain,
! [B: a,A: a] :
( ( ( ^ [C: a] : ( sk4 @ A ) )
!= ( ^ [C: a] : B ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [C: a] : A )
!= ( ^ [C: a] : ( sk6 @ sk3 ) ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[3289]) ).
thf(3291,plain,
! [A: a] :
( ( ( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
!= ( ^ [B: a] : A ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [B: a] : ( sk3 @ ( sk6 @ sk4 ) ) )
!= ( ^ [B: a] : ( sk6 @ sk3 ) ) ) ),
inference(pattern_uni,[status(thm)],[3290:[bind(A,$thf( sk3 @ ( sk6 @ sk4 ) )),bind(B,$thf( B ))]]) ).
thf(3336,plain,
! [A: a] :
( ( ( ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
!= ( ^ [B: a] : A ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( sk2 != sk1 )
| ( ( ^ [B: a] : ( sk3 @ ( sk6 @ sk4 ) ) )
!= ( ^ [B: a] : ( sk6 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[3291]) ).
thf(3851,plain,
! [A: a] :
( ( ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) )
!= A )
| ( ( sk2 @ ( sk26 @ A ) )
!= ( sk1 @ ( sk26 @ A ) ) )
| ( ( sk3 @ ( sk6 @ sk4 ) )
!= ( sk6 @ sk3 ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) ) ),
inference(func_ext,[status(esa)],[3336]) ).
thf(3888,plain,
( ( ( sk2 @ ( sk26 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) )
!= ( sk1 @ ( sk26 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) )
| ( ( sk3 @ ( sk6 @ sk4 ) )
!= ( sk6 @ sk3 ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[3851]) ).
thf(3597,plain,
! [A: a > a > a] :
( ~ $true
| ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3277,83]) ).
thf(3598,plain,
! [A: a > a > a] :
( ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3597]) ).
thf(3604,plain,
( sk2
@ ( sk3
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[3598:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ))]]) ).
thf(4281,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3603,1924]) ).
thf(4282,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[4281]) ).
thf(4283,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[4282:[bind(A,$thf( sk6 @ ^ [B: a] : ( sk6 @ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ))]]) ).
thf(4556,plain,
! [A: a] :
( ~ $true
| ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3788,1924]) ).
thf(4557,plain,
! [A: a] :
( ( sk1 @ ( sk4 @ ( sk3 @ A ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[4556]) ).
thf(4558,plain,
( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [A: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[4557:[bind(A,$thf( sk6 @ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ ^ [C: a] : ( sk6 @ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ))]]) ).
thf(48,plain,
! [C: a > a > a,B: a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ~ $true
| ( ( ^ [D: a] :
( ( sk2 @ D )
& ( ( sk6
@ ^ [E: a] : ( sk6 @ ( C @ E ) ) )
= ( sk6 @ ( C @ D ) ) ) ) )
!= ( (=) @ a @ B ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) )
@ ( sk5
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,46]) ).
thf(49,plain,
! [C: a > a > a,B: a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( ( ^ [D: a] :
( ( sk2 @ D )
& ( ( sk6
@ ^ [E: a] : ( sk6 @ ( C @ E ) ) )
= ( sk6 @ ( C @ D ) ) ) ) )
!= ( (=) @ a @ B ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) )
@ ( sk5
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[48]) ).
thf(52,plain,
! [B: a > a > a > a,A: a] :
( ( sk2
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk6 @ ( B @ C @ D ) ) ) )
@ ( sk5
@ ^ [C: a] :
( sk6
@ ( B
@ ( sk5
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk6 @ ( B @ D @ E ) ) ) )
@ C ) ) ) ) ) )
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk6 @ ( B @ D @ E ) ) ) )
= ( sk6
@ ^ [D: a] : ( sk6 @ ( B @ C @ D ) ) ) ) ) )
!= ( (=) @ a @ A ) ) ),
inference(pre_uni,[status(thm)],[49:[bind(A,$thf( D @ ( sk5 @ ^ [E: a] : ( sk6 @ ^ [F: a] : ( sk6 @ ( D @ E @ F ) ) ) ) @ ( sk5 @ ^ [E: a] : ( sk6 @ ( D @ ( sk5 @ ^ [F: a] : ( sk6 @ ^ [G: a] : ( sk6 @ ( D @ F @ G ) ) ) ) @ E ) ) ) )),bind(B,$thf( B )),bind(C,$thf( ^ [E: a] : ^ [F: a] : ( sk6 @ ( D @ E @ F ) ) ))]]) ).
thf(54,plain,
! [B: a > a > a > a,A: a] :
( ( sk2
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk6 @ ( B @ C @ D ) ) ) )
@ ( sk5
@ ^ [C: a] :
( sk6
@ ( B
@ ( sk5
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk6 @ ( B @ D @ E ) ) ) )
@ C ) ) ) ) ) )
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk6 @ ( B @ D @ E ) ) ) )
= ( sk6
@ ^ [D: a] : ( sk6 @ ( B @ C @ D ) ) ) ) ) )
!= ( (=) @ a @ A ) ) ),
inference(simp,[status(thm)],[52]) ).
thf(92,plain,
! [C: a,B: a > a,A: a] :
( ~ ( sk2 @ A )
| ( ( (=) @ a @ ( sk4 @ A ) )
!= ( (=) @ a @ C ) )
| ( sk2 @ ( sk5 @ B ) )
| ( ( ^ [D: a] :
( ( sk1 @ D )
& ( A
= ( sk3 @ D ) ) ) )
!= ( ^ [D: a] :
( ( sk2 @ D )
& ( ( sk6 @ B )
= ( B @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[16,14]) ).
thf(113,plain,
! [C: a,B: a > a,A: a] :
( ( sk2 @ ( sk5 @ B ) )
| ~ ( sk2 @ A )
| ( ( (=) @ a @ ( sk4 @ A ) )
!= ( (=) @ a @ C ) )
| ( sk2 != sk1 )
| ( ( ^ [D: a] :
( A
= ( sk3 @ D ) ) )
!= ( ^ [D: a] :
( ( sk6 @ B )
= ( B @ D ) ) ) ) ),
inference(simp,[status(thm)],[92]) ).
thf(76,plain,
! [B: a > a,A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) ) ) )
| ~ $true
| ( sk2 @ ( sk3 @ ( sk6 @ B ) ) )
| ( ( sk1
@ ( sk6
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[36,35]) ).
thf(77,plain,
! [B: a > a,A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) ) ) )
| ( sk2 @ ( sk3 @ ( sk6 @ B ) ) )
| ( ( sk1
@ ( sk6
@ ^ [C: a] : ( sk6 @ ( A @ C ) ) ) )
!= ( sk1 @ ( B @ ( sk5 @ B ) ) ) ) ),
inference(simp,[status(thm)],[76]) ).
thf(80,plain,
! [A: a > a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk6 @ ( A @ B @ C ) ) ) )
@ ( sk5
@ ^ [B: a] :
( sk6
@ ( A
@ ( sk5
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk6 @ ( A @ C @ D ) ) ) )
@ B ) ) ) ) ) )
| ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk6 @ ( A @ B @ C ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[77:[bind(A,$thf( D @ ( sk5 @ ^ [D: a] : ( sk6 @ ^ [E: a] : ( sk6 @ ( D @ D @ E ) ) ) ) )),bind(B,$thf( ^ [D: a] : ( sk6 @ ^ [E: a] : ( sk6 @ ( D @ D @ E ) ) ) ))]]) ).
thf(81,plain,
! [A: a > a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk6 @ ( A @ B @ C ) ) ) )
@ ( sk5
@ ^ [B: a] :
( sk6
@ ( A
@ ( sk5
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk6 @ ( A @ C @ D ) ) ) )
@ B ) ) ) ) ) )
| ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk6 @ ( A @ B @ C ) ) ) ) ) ) ),
inference(simp,[status(thm)],[80]) ).
thf(89,plain,
! [B: a,A: a > a] :
( ( ( sk3 @ ( sk6 @ A ) )
!= ( sk5 @ A ) )
| ( ( ^ [C: a] :
( ( sk1 @ C )
& ( B
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) )
| ~ $true
| ( ( sk2 @ ( sk5 @ A ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[25,16]) ).
thf(90,plain,
! [B: a,A: a > a] :
( ( ( sk3 @ ( sk6 @ A ) )
!= ( sk5 @ A ) )
| ( ( ^ [C: a] :
( ( sk1 @ C )
& ( B
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) )
| ( ( sk2 @ ( sk5 @ A ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[89]) ).
thf(91,plain,
! [A: a > a] :
( ( ( sk3 @ ( sk6 @ A ) )
!= ( sk5 @ A ) )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( ( sk5 @ A )
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ ( sk5 @ A ) ) ) ) ),
inference(pattern_uni,[status(thm)],[90:[bind(A,$thf( C )),bind(B,$thf( sk5 @ C ))]]) ).
thf(130,plain,
! [A: a > a] :
( ( ( sk3 @ ( sk6 @ A ) )
!= ( sk5 @ A ) )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( ( sk5 @ A )
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ ( sk5 @ A ) ) ) ) ),
inference(simp,[status(thm)],[91]) ).
thf(4954,plain,
( ( ( sk3 @ ( sk6 @ sk4 ) )
!= ( sk6 @ sk3 ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ~ ( sk2 @ ( sk26 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) )
| ~ ( sk1 @ ( sk26 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ),
inference(bool_ext,[status(thm)],[3888]) ).
thf(1399,plain,
! [C: a,B: a > a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( sk2 @ ( sk5 @ B ) )
| ~ $true
| ( ( sk3 @ C )
!= ( sk5 @ B ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ C ) ) ),
inference(paramod_ordered,[status(thm)],[17,842]) ).
thf(1400,plain,
! [C: a,B: a > a,A: a > a] :
( ( sk2 @ ( sk5 @ A ) )
| ( sk2 @ ( sk5 @ B ) )
| ( ( sk3 @ C )
!= ( sk5 @ B ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1 @ C ) ) ),
inference(simp,[status(thm)],[1399]) ).
thf(1401,plain,
! [B: a > a,A: a > a] :
( ( sk2 @ ( sk5 @ B ) )
| ( sk2 @ ( sk5 @ A ) )
| ( ( sk3 @ ( sk6 @ B ) )
!= ( sk5 @ A ) ) ),
inference(pattern_uni,[status(thm)],[1400:[bind(A,$thf( D )),bind(B,$thf( B )),bind(C,$thf( sk6 @ D ))]]) ).
thf(1452,plain,
! [B: a > a,A: a > a] :
( ( sk2 @ ( sk5 @ B ) )
| ( sk2 @ ( sk5 @ A ) )
| ( ( sk3 @ ( sk6 @ B ) )
!= ( sk5 @ A ) ) ),
inference(simp,[status(thm)],[1401]) ).
thf(1218,plain,
( ~ ( sk2 @ ( sk6 @ sk3 ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) )
!= ( sk6 @ sk3 ) )
| ( ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
!= ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) ) ) ),
inference(simp,[status(thm)],[1202]) ).
thf(50,plain,
! [C: a > a > a,B: a,A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ~ $true
| ( ( ^ [D: a] :
( ( sk2 @ D )
& ( ( sk6
@ ^ [E: a] : ( sk6 @ ( C @ E ) ) )
= ( sk6 @ ( C @ D ) ) ) ) )
!= ( (=) @ a @ B ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) )
@ ( sk5
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[18,46]) ).
thf(51,plain,
! [C: a > a > a,B: a,A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( ( ^ [D: a] :
( ( sk2 @ D )
& ( ( sk6
@ ^ [E: a] : ( sk6 @ ( C @ E ) ) )
= ( sk6 @ ( C @ D ) ) ) ) )
!= ( (=) @ a @ B ) )
| ( ( sk1 @ ( sk6 @ A ) )
!= ( sk1
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) )
@ ( sk5
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[50]) ).
thf(53,plain,
! [B: a > a > a > a,A: a] :
( ~ ( sk1
@ ( B
@ ( sk5
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk6 @ ( B @ C @ D ) ) ) )
@ ( sk5
@ ^ [C: a] :
( sk6
@ ( B
@ ( sk5
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk6 @ ( B @ D @ E ) ) ) )
@ C ) ) )
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk6 @ ( B @ C @ D ) ) ) )
@ ( sk5
@ ^ [C: a] :
( sk6
@ ( B
@ ( sk5
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk6 @ ( B @ D @ E ) ) ) )
@ C ) ) ) ) ) ) )
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk6 @ ( B @ D @ E ) ) ) )
= ( sk6
@ ^ [D: a] : ( sk6 @ ( B @ C @ D ) ) ) ) ) )
!= ( (=) @ a @ A ) ) ),
inference(pre_uni,[status(thm)],[51:[bind(A,$thf( D @ ( sk5 @ ^ [E: a] : ( sk6 @ ^ [F: a] : ( sk6 @ ( D @ E @ F ) ) ) ) @ ( sk5 @ ^ [E: a] : ( sk6 @ ( D @ ( sk5 @ ^ [F: a] : ( sk6 @ ^ [G: a] : ( sk6 @ ( D @ F @ G ) ) ) ) @ E ) ) ) )),bind(B,$thf( B )),bind(C,$thf( ^ [E: a] : ^ [F: a] : ( sk6 @ ( D @ E @ F ) ) ))]]) ).
thf(55,plain,
! [B: a > a > a > a,A: a] :
( ~ ( sk1
@ ( B
@ ( sk5
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk6 @ ( B @ C @ D ) ) ) )
@ ( sk5
@ ^ [C: a] :
( sk6
@ ( B
@ ( sk5
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk6 @ ( B @ D @ E ) ) ) )
@ C ) ) )
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk6 @ ( B @ C @ D ) ) ) )
@ ( sk5
@ ^ [C: a] :
( sk6
@ ( B
@ ( sk5
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk6 @ ( B @ D @ E ) ) ) )
@ C ) ) ) ) ) ) )
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk6 @ ( B @ D @ E ) ) ) )
= ( sk6
@ ^ [D: a] : ( sk6 @ ( B @ C @ D ) ) ) ) ) )
!= ( (=) @ a @ A ) ) ),
inference(simp,[status(thm)],[53]) ).
thf(169,plain,
! [A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) )
| ( ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) )
!= ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[71]) ).
thf(171,plain,
! [A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) )
| ( ( sk3
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) )
!= ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ),
inference(simp,[status(thm)],[169]) ).
thf(7794,plain,
! [A: a] :
( ~ $true
| ( sk2 @ ( sk3 @ A ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[7786,5]) ).
thf(7795,plain,
! [A: a] :
( ( sk2 @ ( sk3 @ A ) )
| ( ( sk1 @ ( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) )
!= ( sk1 @ A ) ) ),
inference(simp,[status(thm)],[7794]) ).
thf(7796,plain,
sk2 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[7795:[bind(A,$thf( sk4 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ))]]) ).
thf(7912,plain,
sk2 @ ( sk3 @ ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ),
inference(rewrite,[status(thm)],[7796,6872]) ).
thf(94,plain,
! [B: a,A: a > a] :
( ( sk1 @ ( sk6 @ A ) )
| ( ( ^ [C: a] :
( ( sk1 @ C )
& ( B
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) )
| ~ $true
| ( ( sk2 @ ( sk5 @ A ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[17,16]) ).
thf(95,plain,
! [B: a,A: a > a] :
( ( sk1 @ ( sk6 @ A ) )
| ( ( ^ [C: a] :
( ( sk1 @ C )
& ( B
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) )
| ( ( sk2 @ ( sk5 @ A ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[94]) ).
thf(96,plain,
! [A: a > a] :
( ( sk1 @ ( sk6 @ A ) )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( ( sk5 @ A )
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ ( sk5 @ A ) ) ) ) ),
inference(pattern_uni,[status(thm)],[95:[bind(A,$thf( C )),bind(B,$thf( sk5 @ C ))]]) ).
thf(119,plain,
! [A: a > a] :
( ( sk1 @ ( sk6 @ A ) )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( ( sk5 @ A )
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ ( sk5 @ A ) ) ) ) ),
inference(simp,[status(thm)],[96]) ).
thf(3767,plain,
! [A: a > a > a] :
( ~ $true
| ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3349,83]) ).
thf(3768,plain,
! [A: a > a > a] :
( ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) )
| ( ( sk1
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3767]) ).
thf(3793,plain,
( sk2
@ ( sk3
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] :
( sk4
@ ( sk3
@ ( sk6
@ ^ [C: a] :
( sk6
@ ^ [D: a] : ( sk4 @ C ) ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[3768:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ ^ [D: a] : ( sk6 @ ^ [E: a] : ( sk4 @ D ) ) ) ) ) ))]]) ).
thf(3302,plain,
( ( ( sk2 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
!= ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) ) )
| ~ $true
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) )
!= ( sk2 @ ( sk6 @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[3265,267]) ).
thf(3303,plain,
( ( ( sk2 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
!= ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) )
!= ( sk2 @ ( sk6 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[3302]) ).
thf(3328,plain,
( ( ( sk2 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
!= ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) ) )
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ( ( sk3 @ ( sk6 @ sk4 ) )
!= ( sk6 @ sk3 ) ) ),
inference(simp,[status(thm)],[3303]) ).
thf(3304,plain,
( ~ $true
| ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ~ ( sk2 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
| ~ ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) )
!= ( sk2 @ ( sk6 @ sk3 ) ) ) ),
inference(paramod_ordered,[status(thm)],[3265,525]) ).
thf(3305,plain,
( ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ~ ( sk2 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
| ~ ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ sk4 ) ) )
!= ( sk2 @ ( sk6 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[3304]) ).
thf(3323,plain,
( ~ ( sk1 @ ( sk3 @ ( sk5 @ sk3 ) ) )
| ~ ( sk2 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
| ~ ( sk1 @ ( sk14 @ ( sk4 @ ( sk6 @ sk3 ) ) @ ( sk6 @ sk3 ) ) )
| ( ( sk3 @ ( sk6 @ sk4 ) )
!= ( sk6 @ sk3 ) ) ),
inference(simp,[status(thm)],[3305]) ).
thf(3358,plain,
! [A: a] :
( ~ $true
| ( sk2 @ ( sk3 @ ( sk4 @ A ) ) )
| ( ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3255,1921]) ).
thf(3359,plain,
! [A: a] :
( ( sk2 @ ( sk3 @ ( sk4 @ A ) ) )
| ( ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ B ) ) ) ) )
!= ( sk2 @ A ) ) ),
inference(simp,[status(thm)],[3358]) ).
thf(3360,plain,
( sk2
@ ( sk3
@ ( sk4
@ ( sk3
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] : ( sk4 @ A ) ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[3359:[bind(A,$thf( sk3 @ ( sk6 @ ^ [B: a] : ( sk6 @ ^ [C: a] : ( sk4 @ B ) ) ) ))]]) ).
thf(3956,plain,
! [A: a > a > a] :
( ~ $true
| ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[3602,83]) ).
thf(3957,plain,
! [A: a > a > a] :
( ( sk2
@ ( sk3
@ ( sk6
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) )
| ( ( sk1
@ ( sk6
@ ^ [B: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) )
!= ( sk1
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) )
@ ( sk5
@ ( A
@ ( sk5
@ ^ [B: a] : ( sk6 @ ( A @ B ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[3956]) ).
thf(3965,plain,
( sk2
@ ( sk3
@ ( sk6
@ ^ [A: a] :
( sk6
@ ^ [B: a] :
( sk6
@ ^ [C: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ) ) ) ),
inference(pre_uni,[status(thm)],[3957:[bind(A,$thf( ^ [B: a] : ^ [C: a] : ( sk6 @ ^ [D: a] : ( sk4 @ ( sk3 @ ( sk6 @ sk4 ) ) ) ) ))]]) ).
thf(47,plain,
! [B: a > a > a,A: a] :
( ( ( ( sk2 @ ( sk8 @ B @ A ) )
& ( ( sk6
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) )
= ( sk6 @ ( B @ ( sk8 @ B @ A ) ) ) ) )
!= ( A
= ( sk8 @ B @ A ) ) )
| ~ ( sk1
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) )
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] : ( sk6 @ ( B @ C ) ) ) ) ) ) ) ),
inference(func_ext,[status(esa)],[46]) ).
thf(59,plain,
! [C: a > a > a,B: a,A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( A @ D ) ) ) ) ) )
| ~ $true
| ( ( ^ [D: a] :
( ( sk2 @ D )
& ( ( sk6
@ ^ [E: a] : ( sk6 @ ( C @ E ) ) )
= ( sk6 @ ( C @ D ) ) ) ) )
!= ( (=) @ a @ B ) )
| ( ( sk1
@ ( sk6
@ ^ [D: a] : ( sk6 @ ( A @ D ) ) ) )
!= ( sk1
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) )
@ ( sk5
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[36,46]) ).
thf(60,plain,
! [C: a > a > a,B: a,A: a > a > a] :
( ( sk2
@ ( sk5
@ ( A
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( A @ D ) ) ) ) ) )
| ( ( ^ [D: a] :
( ( sk2 @ D )
& ( ( sk6
@ ^ [E: a] : ( sk6 @ ( C @ E ) ) )
= ( sk6 @ ( C @ D ) ) ) ) )
!= ( (=) @ a @ B ) )
| ( ( sk1
@ ( sk6
@ ^ [D: a] : ( sk6 @ ( A @ D ) ) ) )
!= ( sk1
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) )
@ ( sk5
@ ( C
@ ( sk5
@ ^ [D: a] : ( sk6 @ ( C @ D ) ) ) ) ) ) ) ) ),
inference(simp,[status(thm)],[59]) ).
thf(65,plain,
! [B: a > a > a > a > a,A: a] :
( ( sk2
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] :
( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk6 @ ( B @ C @ D @ E ) ) ) ) )
@ ( sk5
@ ^ [C: a] :
( sk6
@ ^ [D: a] :
( sk6
@ ( B
@ ( sk5
@ ^ [E: a] :
( sk6
@ ^ [F: a] :
( sk6
@ ^ [G: a] : ( sk6 @ ( B @ E @ F @ G ) ) ) ) )
@ C
@ D ) ) ) )
@ ( sk5
@ ^ [C: a] :
( sk6
@ ( B
@ ( sk5
@ ^ [D: a] :
( sk6
@ ^ [E: a] :
( sk6
@ ^ [F: a] : ( sk6 @ ( B @ D @ E @ F ) ) ) ) )
@ ( sk5
@ ^ [D: a] :
( sk6
@ ^ [E: a] :
( sk6
@ ( B
@ ( sk5
@ ^ [F: a] :
( sk6
@ ^ [G: a] :
( sk6
@ ^ [H: a] : ( sk6 @ ( B @ F @ G @ H ) ) ) ) )
@ D
@ E ) ) ) )
@ C ) ) ) ) ) )
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] :
( sk6
@ ^ [F: a] : ( sk6 @ ( B @ D @ E @ F ) ) ) ) )
= ( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk6 @ ( B @ C @ D @ E ) ) ) ) ) ) )
!= ( (=) @ a @ A ) ) ),
inference(pre_uni,[status(thm)],[60:[bind(A,$thf( E @ ( sk5 @ ^ [E: a] : ( sk6 @ ^ [F: a] : ( sk6 @ ^ [G: a] : ( sk6 @ ( E @ E @ F @ G ) ) ) ) ) @ ( sk5 @ ^ [E: a] : ( sk6 @ ^ [F: a] : ( sk6 @ ( E @ ( sk5 @ ^ [G: a] : ( sk6 @ ^ [H: a] : ( sk6 @ ^ [I: a] : ( sk6 @ ( E @ G @ H @ I ) ) ) ) ) @ E @ F ) ) ) ) )),bind(B,$thf( B )),bind(C,$thf( ^ [E: a] : ^ [F: a] : ( sk6 @ ^ [G: a] : ( sk6 @ ( E @ E @ F @ G ) ) ) ))]]) ).
thf(68,plain,
! [B: a > a > a > a > a,A: a] :
( ( sk2
@ ( sk5
@ ( B
@ ( sk5
@ ^ [C: a] :
( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk6 @ ( B @ C @ D @ E ) ) ) ) )
@ ( sk5
@ ^ [C: a] :
( sk6
@ ^ [D: a] :
( sk6
@ ( B
@ ( sk5
@ ^ [E: a] :
( sk6
@ ^ [F: a] :
( sk6
@ ^ [G: a] : ( sk6 @ ( B @ E @ F @ G ) ) ) ) )
@ C
@ D ) ) ) )
@ ( sk5
@ ^ [C: a] :
( sk6
@ ( B
@ ( sk5
@ ^ [D: a] :
( sk6
@ ^ [E: a] :
( sk6
@ ^ [F: a] : ( sk6 @ ( B @ D @ E @ F ) ) ) ) )
@ ( sk5
@ ^ [D: a] :
( sk6
@ ^ [E: a] :
( sk6
@ ( B
@ ( sk5
@ ^ [F: a] :
( sk6
@ ^ [G: a] :
( sk6
@ ^ [H: a] : ( sk6 @ ( B @ F @ G @ H ) ) ) ) )
@ D
@ E ) ) ) )
@ C ) ) ) ) ) )
| ( ( ^ [C: a] :
( ( sk2 @ C )
& ( ( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] :
( sk6
@ ^ [F: a] : ( sk6 @ ( B @ D @ E @ F ) ) ) ) )
= ( sk6
@ ^ [D: a] :
( sk6
@ ^ [E: a] : ( sk6 @ ( B @ C @ D @ E ) ) ) ) ) ) )
!= ( (=) @ a @ A ) ) ),
inference(simp,[status(thm)],[65]) ).
thf(104,plain,
! [B: a,A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( ( ^ [C: a] :
( ( sk1 @ C )
& ( B
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) )
| ~ $true
| ( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
!= ( sk2 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[35,16]) ).
thf(105,plain,
! [B: a,A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( ( ^ [C: a] :
( ( sk1 @ C )
& ( B
= ( sk3 @ C ) ) ) )
= ( (=) @ a @ ( sk4 @ B ) ) )
| ( ( sk2 @ ( sk3 @ ( sk6 @ A ) ) )
!= ( sk2 @ B ) ) ),
inference(simp,[status(thm)],[104]) ).
thf(106,plain,
! [A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( ( sk3 @ ( sk6 @ A ) )
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ ( sk3 @ ( sk6 @ A ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[105:[bind(A,$thf( D )),bind(B,$thf( sk3 @ ( sk6 @ D ) ))]]) ).
thf(122,plain,
! [A: a > a] :
( ~ ( sk1 @ ( A @ ( sk5 @ A ) ) )
| ( ( ^ [B: a] :
( ( sk1 @ B )
& ( ( sk3 @ ( sk6 @ A ) )
= ( sk3 @ B ) ) ) )
= ( (=) @ a @ ( sk4 @ ( sk3 @ ( sk6 @ A ) ) ) ) ) ),
inference(simp,[status(thm)],[106]) ).
thf(12797,plain,
$false,
inference(e,[status(thm)],[116,3975,175,3625,36,1767,3798,666,2363,1924,5,120,269,6872,24,1921,37,25,14,110,3410,46,4622,4368,3602,3788,216,3322,7786,121,84,85,3984,3265,3603,38,70,3778,1938,665,842,3750,3349,3775,3010,3787,3354,3937,129,3628,3903,128,3624,1219,45,3888,17,3604,22,4283,3255,71,12,4558,54,113,81,130,2365,267,35,3,4954,525,18,1452,16,1218,3336,55,171,7912,119,3793,3328,3277,3323,3360,3965,47,68,122,83,1769,1917]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV089^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21 % Computer : n001.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Tue Sep 29 15:13:05 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.05/0.80 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.24/0.98 % [INFO] Parsing done (183ms).
% 1.24/1.00 % [INFO] Running in sequential loop mode.
% 2.06/1.40 % [INFO] eprover registered as external prover.
% 2.06/1.41 % [INFO] Scanning for conjecture ...
% 2.25/1.51 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.25/1.56 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.25/1.57 % [INFO] Problem is higher-order (TPTP THF).
% 2.25/1.58 % [INFO] Type checking passed.
% 2.25/1.58 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 87.84/21.31 % External prover 'e' found a proof!
% 87.84/21.31 % [INFO] Killing All external provers ...
% 87.84/21.31 % Time passed: 20943ms (effective reasoning time: 20307ms)
% 87.84/21.31 % 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)>
% 87.84/21.31 % Axioms used in derivation (0):
% 87.84/21.31 % No. of inferences in proof: 297
% 87.84/21.31 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 20943 ms resp. 20307 ms w/o parsing
% 85.18/21.59 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 85.18/21.59 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------