%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : PHI008^4 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n002.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:20:14 AM UTC 2026
% Result : Theorem 93.49s 23.30s
% Output : Refutation 94.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 30
% Syntax : Number of formulae : 374 ( 115 unt; 0 typ; 18 def)
% Number of atoms : 1460 ( 353 equ; 0 cnn)
% Maximal formula atoms : 5 ( 3 avg)
% Number of connectives : 3683 ( 634 ~; 310 |; 27 &;2460 @)
% ( 0 <=>; 252 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 613 ( 613 >; 0 *; 0 +; 0 <<)
% Number of symbols : 73 ( 70 usr; 53 con; 0-3 aty)
% Number of variables : 1308 ( 449 ^; 752 !; 89 ?;1308 :)
% ( 0 !>; 0 ?*; 0 @-; 18 @+)
% Comments :
%------------------------------------------------------------------------------
thf(qML_mu_type,type,
qML_mu: $tType ).
thf(qML_i_type,type,
qML_i: $tType ).
thf(scott_G_decl,type,
scott_G: qML_mu > qML_i > $o ).
thf(scott_NE_QML_mu_decl,type,
scott_NE_QML_mu: qML_mu > qML_i > $o ).
thf(scott_P_decl,type,
scott_P: ( qML_mu > qML_i > $o ) > qML_i > $o ).
thf(scott_ess_QML_mu_decl,type,
scott_ess_QML_mu: ( qML_mu > qML_i > $o ) > qML_mu > qML_i > $o ).
thf(sk1_decl,type,
sk1: qML_i ).
thf(sk2_decl,type,
sk2: qML_i > $o ).
thf(sk3_decl,type,
sk3: qML_i ).
thf(sk4_decl,type,
sk4: qML_i > qML_mu ).
thf(sk5_decl,type,
sk5: ( qML_mu > qML_i > $o ) > ( qML_mu > qML_i > $o ) > qML_i > qML_i ).
thf(sk6_decl,type,
sk6: ( qML_mu > qML_i > $o ) > ( qML_mu > qML_i > $o ) > qML_i > qML_mu ).
thf(sk7_decl,type,
sk7: qML_mu ).
thf(sk8_decl,type,
sk8: qML_i ).
thf(sk9_decl,type,
sk9: qML_mu ).
thf(sk10_decl,type,
sk10: qML_i ).
thf(sk11_decl,type,
sk11: qML_mu ).
thf(sk12_decl,type,
sk12: qML_i ).
thf(sk13_decl,type,
sk13: qML_mu ).
thf(sk14_decl,type,
sk14: qML_i ).
thf(sk15_decl,type,
sk15: qML_mu ).
thf(sk16_decl,type,
sk16: qML_i ).
thf(sk17_decl,type,
sk17: qML_mu ).
thf(sk18_decl,type,
sk18: qML_i ).
thf(sk19_decl,type,
sk19: qML_mu ).
thf(sk20_decl,type,
sk20: qML_i ).
thf(sk22_decl,type,
sk22: qML_mu ).
thf(sk23_decl,type,
sk23: qML_i ).
thf(sk24_decl,type,
sk24: qML_mu ).
thf(sk25_decl,type,
sk25: qML_i ).
thf(sk31_decl,type,
sk31: qML_mu ).
thf(sk32_decl,type,
sk32: qML_i ).
thf(sk33_decl,type,
sk33: qML_mu ).
thf(sk34_decl,type,
sk34: qML_i ).
thf(sk39_decl,type,
sk39: qML_mu > qML_i > $o ).
thf(sk40_decl,type,
sk40: qML_mu > qML_i > $o ).
thf(sk42_decl,type,
sk42: qML_mu > qML_i > $o ).
thf(sk43_decl,type,
sk43: qML_mu > qML_i > $o ).
thf(sk44_decl,type,
sk44: qML_mu ).
thf(sk45_decl,type,
sk45: qML_i ).
thf(sk55_decl,type,
sk55: qML_mu > qML_i > $o ).
thf(sk57_decl,type,
sk57: qML_mu ).
thf(sk58_decl,type,
sk58: qML_i ).
thf(sk59_decl,type,
sk59: qML_mu ).
thf(sk60_decl,type,
sk60: qML_i ).
thf(sk61_decl,type,
sk61: qML_mu ).
thf(sk62_decl,type,
sk62: qML_i ).
thf(sk63_decl,type,
sk63: qML_mu ).
thf(sk64_decl,type,
sk64: qML_i ).
thf(sk70_decl,type,
sk70: qML_mu > qML_i > $o ).
thf(sk71_decl,type,
sk71: qML_i ).
thf(sk93_decl,type,
sk93: qML_mu ).
thf(sk94_decl,type,
sk94: qML_i ).
thf(sk132_decl,type,
sk132: qML_mu > qML_i > $o ).
thf(sk133_decl,type,
sk133: qML_mu ).
thf(sk134_decl,type,
sk134: qML_i ).
thf(sk144_decl,type,
sk144: qML_mu > qML_i > $o ).
thf(sk145_decl,type,
sk145: qML_mu ).
thf(sk146_decl,type,
sk146: qML_i ).
thf(sk167_decl,type,
sk167: qML_mu ).
thf(sk168_decl,type,
sk168: qML_i ).
thf(sk178_decl,type,
sk178: qML_mu > qML_i > $o ).
thf(sk187_decl,type,
sk187: qML_mu ).
thf(sk188_decl,type,
sk188: qML_i ).
thf(sk195_decl,type,
sk195: qML_mu > qML_i > $o ).
thf(sk200_decl,type,
sk200: qML_mu ).
thf(sk201_decl,type,
sk201: qML_i ).
thf(sk202_decl,type,
sk202: qML_mu > qML_i > $o ).
thf(sk207_decl,type,
sk207: qML_mu ).
thf(sk208_decl,type,
sk208: qML_i ).
thf(sk211_decl,type,
sk211: qML_mu ).
thf(sk212_decl,type,
sk212: qML_i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: qML_i] :
~ ! [B: qML_i > $o] :
( ~ ( B @ A )
| ! [C: qML_i] : ( B @ C ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: qML_i > $o] :
~ ( ~ ( A @ sk1 )
| ! [B: qML_i] : ( A @ B ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: qML_i] :
~ ( sk2 @ A ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: qML_i] :
@+[B: qML_mu] : ( scott_G @ B @ A ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,C: qML_i] :
@+[D: qML_i] :
~ ! [E: qML_mu] :
( ( B @ E @ D )
=> ( A @ E @ D ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,C: qML_i] :
@+[D: qML_mu] :
~ ( ( B @ D @ ( sk5 @ A @ B @ C ) )
=> ( A @ D @ ( sk5 @ A @ B @ C ) ) ) ) ) ).
thf(sk39_def,definition,
( sk39
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( scott_P @ A @ sk12 )
=> ( A @ sk11 @ sk12 ) ) ) ) ).
thf(sk40_def,definition,
( sk40
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( scott_P @ A @ sk14 )
=> ( A @ sk13 @ sk14 ) ) ) ) ).
thf(sk42_def,definition,
( sk42
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( scott_P @ A @ sk18 )
=> ( A @ sk17 @ sk18 ) ) ) ) ).
thf(sk43_def,definition,
( sk43
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( scott_P @ A @ sk20 )
=> ( A @ sk19 @ sk20 ) ) ) ) ).
thf(sk55_def,definition,
( sk55
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( scott_P @ A @ sk10 )
=> ( A @ sk9 @ sk10 ) ) ) ) ).
thf(sk70_def,definition,
( sk70
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( scott_ess_QML_mu @ A @ sk15 @ sk16 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) ) ) ).
thf(sk71_def,definition,
( sk71
= ( @+[A: qML_i] :
~ ? [B: qML_mu] : ( sk70 @ B @ A ) ) ) ).
thf(sk132_def,definition,
( sk132
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( scott_P @ A @ sk58 )
=> ( A @ sk57 @ sk58 ) ) ) ) ).
thf(sk144_def,definition,
( sk144
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( scott_P @ A @ sk34 )
=> ( A @ sk33 @ sk34 ) ) ) ) ).
thf(sk178_def,definition,
( sk178
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( scott_P @ A @ sk62 )
=> ( A @ sk61 @ sk62 ) ) ) ) ).
thf(sk195_def,definition,
( sk195
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( scott_P @ A @ sk16 )
=> ( A @ sk15 @ sk16 ) ) ) ) ).
thf(sk202_def,definition,
( sk202
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( scott_P @ A @ sk8 )
=> ( A @ sk7 @ sk8 ) ) ) ) ).
thf(13,axiom,
( scott_NE_QML_mu
= ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_NE__def) ).
thf(40,plain,
( scott_NE_QML_mu
= ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(41,plain,
( scott_NE_QML_mu
= ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) ),
inference(lifteq,[status(thm)],[40]) ).
thf(10,axiom,
! [A: qML_i] : ( scott_P @ scott_NE_QML_mu @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_A5) ).
thf(34,plain,
! [A: qML_i] : ( scott_P @ scott_NE_QML_mu @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(35,plain,
! [A: qML_i] : ( scott_P @ scott_NE_QML_mu @ A ),
inference(cnf,[status(esa)],[34]) ).
thf(8,axiom,
! [A: qML_i,B: qML_mu > qML_i > $o,C: qML_mu > qML_i > $o] :
( ( ( scott_P @ B @ A )
& ! [D: qML_i,E: qML_mu] :
( ( B @ E @ D )
=> ( C @ E @ D ) ) )
=> ( scott_P @ C @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_A2) ).
thf(28,plain,
! [A: qML_i,B: qML_mu > qML_i > $o,C: qML_mu > qML_i > $o] :
( ( ( scott_P @ B @ A )
& ! [D: qML_i,E: qML_mu] :
( ( B @ E @ D )
=> ( C @ E @ D ) ) )
=> ( scott_P @ C @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(29,plain,
! [C: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,A: qML_i] :
( ( ~ ( scott_P @ B @ A )
| ( B @ ( sk6 @ C @ B @ A ) @ ( sk5 @ C @ B @ A ) )
| ( scott_P @ C @ A ) )
& ( ~ ( scott_P @ B @ A )
| ~ ( C @ ( sk6 @ C @ B @ A ) @ ( sk5 @ C @ B @ A ) )
| ( scott_P @ C @ A ) ) ),
inference(cnf,[status(esa)],[28]) ).
thf(30,plain,
! [C: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ( B @ ( sk6 @ C @ B @ A ) @ ( sk5 @ C @ B @ A ) )
| ( scott_P @ C @ A ) ),
inference(cnfConj,[status(thm)],[29]) ).
thf(1,conjecture,
! [A: qML_i,B: qML_i > $o] :
( ~ ( B @ A )
| ! [C: qML_i] : ( B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(2,negated_conjecture,
~ ! [A: qML_i,B: qML_i > $o] :
( ~ ( B @ A )
| ! [C: qML_i] : ( B @ C ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(14,plain,
~ ! [A: qML_i,B: qML_i > $o] :
( ~ ( B @ A )
| ! [C: qML_i] : ( B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(15,plain,
( ( sk2 @ sk1 )
& ~ ( sk2 @ sk3 ) ),
inference(cnf,[status(esa)],[14]) ).
thf(17,plain,
~ ( sk2 @ sk3 ),
inference(cnfConj,[status(thm)],[15]) ).
thf(195,plain,
! [C: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ( scott_P @ C @ A )
| ~ $true
| ( ( B @ ( sk6 @ C @ B @ A ) @ ( sk5 @ C @ B @ A ) )
!= ( sk2 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[30,17]) ).
thf(196,plain,
! [C: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ( scott_P @ C @ A )
| ( ( B @ ( sk6 @ C @ B @ A ) @ ( sk5 @ C @ B @ A ) )
!= ( sk2 @ sk3 ) ) ),
inference(simp,[status(thm)],[195]) ).
thf(232,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P
@ ^ [C: qML_mu,D: qML_i] : ( sk2 @ sk3 )
@ A )
| ( scott_P @ B @ A ) ),
inference(pre_uni,[status(thm)],[196:[bind(A,$thf( A )),bind(B,$thf( ^ [D: qML_mu] : ^ [E: qML_i] : ( sk2 @ sk3 ) )),bind(C,$thf( C ))]]) ).
thf(261,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P
@ ^ [C: qML_mu,D: qML_i] : ( sk2 @ sk3 )
@ A )
| ( scott_P @ B @ A ) ),
inference(simp,[status(thm)],[232]) ).
thf(362,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P
@ ^ [C: qML_mu,D: qML_i] : $false
@ A )
| ( scott_P @ B @ A ) ),
inference(rewrite,[status(thm)],[261,17]) ).
thf(11,axiom,
! [A: qML_i,B: qML_mu > qML_i > $o] :
( ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A )
=> ~ ( scott_P @ B @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_A1a) ).
thf(36,plain,
! [A: qML_i,B: qML_mu > qML_i > $o] :
( ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A )
=> ~ ( scott_P @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(37,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A )
| ~ ( scott_P @ B @ A ) ),
inference(cnf,[status(esa)],[36]) ).
thf(86,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ~ $true
| ( ( scott_P @ scott_NE_QML_mu @ A )
!= ( scott_P @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[35,37]) ).
thf(87,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ( ( scott_P @ scott_NE_QML_mu @ A )
!= ( scott_P @ C @ B ) ) ),
inference(simp,[status(thm)],[86]) ).
thf(88,plain,
! [A: qML_i] :
~ ( scott_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( scott_NE_QML_mu @ B @ C )
@ A ),
inference(pattern_uni,[status(thm)],[87:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( scott_NE_QML_mu ))]]) ).
thf(363,plain,
! [C: qML_i,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P
@ ^ [D: qML_mu,E: qML_i] : $false
@ A )
| ~ $true
| ( ( scott_P @ B @ A )
!= ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( scott_NE_QML_mu @ D @ E )
@ C ) ) ),
inference(paramod_ordered,[status(thm)],[362,88]) ).
thf(364,plain,
! [C: qML_i,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P
@ ^ [D: qML_mu,E: qML_i] : $false
@ A )
| ( ( scott_P @ B @ A )
!= ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( scott_NE_QML_mu @ D @ E )
@ C ) ) ),
inference(simp,[status(thm)],[363]) ).
thf(365,plain,
! [A: qML_i] :
~ ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ),
inference(pattern_uni,[status(thm)],[364:[bind(A,$thf( A )),bind(B,$thf( ^ [D: qML_mu] : ^ [E: qML_i] : ~ ( scott_NE_QML_mu @ D @ E ) )),bind(C,$thf( A ))]]) ).
thf(430,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( scott_P @ scott_NE_QML_mu @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] : $false
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[35,365]) ).
thf(431,plain,
! [B: qML_i,A: qML_i] :
( ( scott_P @ scott_NE_QML_mu @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] : $false
@ B ) ),
inference(simp,[status(thm)],[430]) ).
thf(440,plain,
! [B: qML_i,A: qML_i] :
( ( scott_NE_QML_mu
!= ( ^ [C: qML_mu,D: qML_i] : $false ) )
| ( A != B ) ),
inference(simp,[status(thm)],[431]) ).
thf(446,plain,
( scott_NE_QML_mu
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ),
inference(simp,[status(thm)],[440]) ).
thf(529,plain,
scott_NE_QML_mu @ sk22 @ sk23,
inference(func_ext,[status(esa)],[446]) ).
thf(7,axiom,
( scott_ess_QML_mu
= ( ^ [A: qML_mu > qML_i > $o,B: qML_mu,C: qML_i] :
( ( A @ B @ C )
& ! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i,F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_ess__def) ).
thf(26,plain,
( scott_ess_QML_mu
= ( ^ [A: qML_mu > qML_i > $o,B: qML_mu,C: qML_i] :
( ( A @ B @ C )
& ! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i,F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(27,plain,
( scott_ess_QML_mu
= ( ^ [A: qML_mu > qML_i > $o,B: qML_mu,C: qML_i] :
( ( A @ B @ C )
& ! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i,F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) ) ),
inference(lifteq,[status(thm)],[26]) ).
thf(157,plain,
! [C: qML_i,B: qML_mu,A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ B @ C )
= ( ( A @ B @ C )
& ! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i,F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) ),
inference(func_ext,[status(esa)],[27]) ).
thf(2846,plain,
! [C: qML_i,B: qML_mu,A: qML_mu > qML_i > $o] :
( ( ( $true
& ! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i,F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) )
= ( scott_ess_QML_mu @ A @ B @ C ) )
| ( ( scott_NE_QML_mu @ sk22 @ sk23 )
!= ( A @ B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[529,157]) ).
thf(2847,plain,
! [C: qML_i,B: qML_mu,A: qML_mu > qML_i > $o] :
( ( ( ! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i,F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) )
= ( scott_ess_QML_mu @ A @ B @ C ) )
| ( ( scott_NE_QML_mu @ sk22 @ sk23 )
!= ( A @ B @ C ) ) ),
inference(simp,[status(thm)],[2846]) ).
thf(3018,plain,
( ( scott_ess_QML_mu @ scott_NE_QML_mu @ sk22 @ sk23 )
= ( ! [A: qML_mu > qML_i > $o] :
( ( A @ sk22 @ sk23 )
=> ! [B: qML_i,C: qML_mu] :
( ( scott_NE_QML_mu @ C @ B )
=> ( A @ C @ B ) ) ) ) ),
inference(pre_uni,[status(thm)],[2847:[bind(A,$thf( scott_NE_QML_mu )),bind(B,$thf( sk22 )),bind(C,$thf( sk23 ))]]) ).
thf(3508,plain,
( ( ( scott_ess_QML_mu
@ ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) )
@ sk22
@ sk23 )
= ( ! [A: qML_mu > qML_i > $o] :
( ( A @ sk22 @ sk23 )
=> ! [B: qML_i,C: qML_mu] :
( ( scott_NE_QML_mu @ C @ B )
=> ( A @ C @ B ) ) ) ) )
| ( scott_NE_QML_mu != scott_NE_QML_mu ) ),
inference(paramod_ordered,[status(thm)],[41,3018]) ).
thf(3509,plain,
( ( scott_ess_QML_mu
@ ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) )
@ sk22
@ sk23 )
= ( ! [A: qML_mu > qML_i > $o] :
( ( A @ sk22 @ sk23 )
=> ! [B: qML_i,C: qML_mu] :
( ( scott_NE_QML_mu @ C @ B )
=> ( A @ C @ B ) ) ) ) ),
inference(pattern_uni,[status(thm)],[3508:[]]) ).
thf(6,axiom,
! [A: qML_i] : ( scott_P @ scott_G @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_A3) ).
thf(24,plain,
! [A: qML_i] : ( scott_P @ scott_G @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(25,plain,
! [A: qML_i] : ( scott_P @ scott_G @ A ),
inference(cnf,[status(esa)],[24]) ).
thf(138,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( scott_P @ scott_G @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( scott_NE_QML_mu @ C @ D )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[25,88]) ).
thf(139,plain,
! [B: qML_i,A: qML_i] :
( ( scott_P @ scott_G @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( scott_NE_QML_mu @ C @ D )
@ B ) ),
inference(simp,[status(thm)],[138]) ).
thf(141,plain,
! [B: qML_i,A: qML_i] :
( ( scott_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( scott_NE_QML_mu @ C @ D ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[139]) ).
thf(143,plain,
( scott_G
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( scott_NE_QML_mu @ A @ B ) ) ),
inference(simp,[status(thm)],[141]) ).
thf(144,plain,
( ( scott_G @ sk9 @ sk10 )
!= ( ~ ( scott_NE_QML_mu @ sk9 @ sk10 ) ) ),
inference(func_ext,[status(esa)],[143]) ).
thf(12,axiom,
! [A: qML_i,B: qML_mu] :
( ( scott_G @ B @ A )
=> ( scott_ess_QML_mu @ scott_G @ B @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_T2) ).
thf(38,plain,
! [A: qML_i,B: qML_mu] :
( ( scott_G @ B @ A )
=> ( scott_ess_QML_mu @ scott_G @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(39,plain,
! [B: qML_mu,A: qML_i] :
( ~ ( scott_G @ B @ A )
| ( scott_ess_QML_mu @ scott_G @ B @ A ) ),
inference(cnf,[status(esa)],[38]) ).
thf(3,axiom,
( scott_G
= ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_G__def) ).
thf(18,plain,
( scott_G
= ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(19,plain,
( scott_G
= ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
inference(lifteq,[status(thm)],[18]) ).
thf(66,plain,
! [A: qML_i] :
( ( scott_P
@ ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( scott_P @ D @ C )
=> ( D @ B @ C ) )
@ A )
| ( scott_G != scott_G ) ),
inference(paramod_ordered,[status(thm)],[19,25]) ).
thf(67,plain,
! [A: qML_i] :
( scott_P
@ ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( scott_P @ D @ C )
=> ( D @ B @ C ) )
@ A ),
inference(pattern_uni,[status(thm)],[66:[]]) ).
thf(171,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ~ $true
| ( ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( scott_P @ F @ E )
=> ( F @ D @ E ) )
@ A )
!= ( scott_P @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[67,37]) ).
thf(172,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ( ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( scott_P @ F @ E )
=> ( F @ D @ E ) )
@ A )
!= ( scott_P @ C @ B ) ) ),
inference(simp,[status(thm)],[171]) ).
thf(173,plain,
! [A: qML_i] :
~ ( scott_P
@ ^ [B: qML_mu,C: qML_i] :
~ ! [D: qML_mu > qML_i > $o] :
( ( scott_P @ D @ C )
=> ( D @ B @ C ) )
@ A ),
inference(pattern_uni,[status(thm)],[172:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( ^ [D: qML_mu] : ^ [E: qML_i] : ! [F: qML_mu > qML_i > $o] : ( ( scott_P @ F @ E ) => ( F @ D @ E ) ) ))]]) ).
thf(305,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( scott_P @ scott_NE_QML_mu @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[35,173]) ).
thf(306,plain,
! [B: qML_i,A: qML_i] :
( ( scott_P @ scott_NE_QML_mu @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) )
@ B ) ),
inference(simp,[status(thm)],[305]) ).
thf(312,plain,
! [B: qML_i,A: qML_i] :
( ( scott_NE_QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[306]) ).
thf(315,plain,
( scott_NE_QML_mu
!= ( ^ [A: qML_mu,B: qML_i] :
~ ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
inference(simp,[status(thm)],[312]) ).
thf(317,plain,
( ( scott_NE_QML_mu @ sk17 @ sk18 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk18 )
=> ( A @ sk17 @ sk18 ) ) ) ),
inference(func_ext,[status(esa)],[315]) ).
thf(852,plain,
( ( scott_NE_QML_mu @ sk17 @ sk18 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk18 )
=> ( A @ sk17 @ sk18 ) ) ),
inference(bool_ext,[status(thm)],[317]) ).
thf(865,plain,
( ( ( scott_NE_QML_mu @ sk17 @ sk18 )
| ( scott_P @ sk42 @ sk18 ) )
& ( ( scott_NE_QML_mu @ sk17 @ sk18 )
| ~ ( sk42 @ sk17 @ sk18 ) ) ),
inference(cnf,[status(esa)],[852]) ).
thf(866,plain,
( ( scott_NE_QML_mu @ sk17 @ sk18 )
| ( scott_P @ sk42 @ sk18 ) ),
inference(cnfConj,[status(thm)],[865]) ).
thf(1282,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk17 @ sk18 )
| ~ $true
| ( ( scott_P @ sk42 @ sk18 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[866,365]) ).
thf(1283,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk17 @ sk18 )
| ( ( scott_P @ sk42 @ sk18 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(simp,[status(thm)],[1282]) ).
thf(1314,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk17 @ sk18 )
| ( sk42
!= ( ^ [B: qML_mu,C: qML_i] : $false ) )
| ( sk18 != A ) ),
inference(simp,[status(thm)],[1283]) ).
thf(1322,plain,
( ( scott_NE_QML_mu @ sk17 @ sk18 )
| ( sk42
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ) ),
inference(simp,[status(thm)],[1314]) ).
thf(56,plain,
! [B: qML_i,A: qML_mu] :
( ( scott_NE_QML_mu @ A @ B )
= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) ),
inference(func_ext,[status(esa)],[41]) ).
thf(77,plain,
! [A: qML_i] :
( ( scott_P
@ ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ D @ B @ C )
=> ! [E: qML_i] :
? [F: qML_mu] : ( D @ F @ E ) )
@ A )
| ( scott_NE_QML_mu != scott_NE_QML_mu ) ),
inference(paramod_ordered,[status(thm)],[41,35]) ).
thf(78,plain,
! [A: qML_i] :
( scott_P
@ ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ D @ B @ C )
=> ! [E: qML_i] :
? [F: qML_mu] : ( D @ F @ E ) )
@ A ),
inference(pattern_uni,[status(thm)],[77:[]]) ).
thf(335,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ~ $true
| ( ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ F @ D @ E )
=> ! [G: qML_i] :
? [H: qML_mu] : ( F @ H @ G ) )
@ A )
!= ( scott_P @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[78,37]) ).
thf(336,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ( ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ F @ D @ E )
=> ! [G: qML_i] :
? [H: qML_mu] : ( F @ H @ G ) )
@ A )
!= ( scott_P @ C @ B ) ) ),
inference(simp,[status(thm)],[335]) ).
thf(337,plain,
! [A: qML_i] :
~ ( scott_P
@ ^ [B: qML_mu,C: qML_i] :
~ ! [D: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ D @ B @ C )
=> ! [E: qML_i] :
? [F: qML_mu] : ( D @ F @ E ) )
@ A ),
inference(pattern_uni,[status(thm)],[336:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( ^ [D: qML_mu] : ^ [E: qML_i] : ! [F: qML_mu > qML_i > $o] : ( ( scott_ess_QML_mu @ F @ D @ E ) => ! [G: qML_i] : ? [H: qML_mu] : ( F @ H @ G ) ) ))]]) ).
thf(1062,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) )
@ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[67,337]) ).
thf(1063,plain,
! [B: qML_i,A: qML_i] :
( ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) )
@ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) )
@ B ) ),
inference(simp,[status(thm)],[1062]) ).
thf(1068,plain,
! [B: qML_i,A: qML_i] :
( ( ( ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) ) )
!= ( ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[1063]) ).
thf(1074,plain,
( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) ),
inference(simp,[status(thm)],[1068]) ).
thf(1084,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk62 )
=> ( A @ sk61 @ sk62 ) ) )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk61 @ sk62 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) ) ),
inference(func_ext,[status(esa)],[1074]) ).
thf(1960,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ( scott_NE_QML_mu @ A @ B ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ sk62 )
=> ( C @ sk61 @ sk62 ) ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ sk61 @ sk62 )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[56,1084]) ).
thf(1961,plain,
( ( ~ ( scott_NE_QML_mu @ sk61 @ sk62 ) )
!= ( ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk62 )
=> ( A @ sk61 @ sk62 ) ) ) ),
inference(pattern_uni,[status(thm)],[1960:[bind(A,$thf( sk61 )),bind(B,$thf( sk62 ))]]) ).
thf(1978,plain,
( ~ ~ ( scott_NE_QML_mu @ sk61 @ sk62 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk62 )
=> ( A @ sk61 @ sk62 ) ) ),
inference(bool_ext,[status(thm)],[1961]) ).
thf(2001,plain,
( ( ( scott_NE_QML_mu @ sk61 @ sk62 )
| ( scott_P @ sk178 @ sk62 ) )
& ( ( scott_NE_QML_mu @ sk61 @ sk62 )
| ~ ( sk178 @ sk61 @ sk62 ) ) ),
inference(cnf,[status(esa)],[1978]) ).
thf(2002,plain,
( ( scott_NE_QML_mu @ sk61 @ sk62 )
| ( scott_P @ sk178 @ sk62 ) ),
inference(cnfConj,[status(thm)],[2001]) ).
thf(2251,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk61 @ sk62 )
| ~ $true
| ( ( scott_P @ sk178 @ sk62 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[2002,365]) ).
thf(2252,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk61 @ sk62 )
| ( ( scott_P @ sk178 @ sk62 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(simp,[status(thm)],[2251]) ).
thf(2295,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk61 @ sk62 )
| ( sk178
!= ( ^ [B: qML_mu,C: qML_i] : $false ) )
| ( sk62 != A ) ),
inference(simp,[status(thm)],[2252]) ).
thf(2305,plain,
( ( scott_NE_QML_mu @ sk61 @ sk62 )
| ( sk178
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ) ),
inference(simp,[status(thm)],[2295]) ).
thf(2306,plain,
( ( sk178 @ sk200 @ sk201 )
| ( scott_NE_QML_mu @ sk61 @ sk62 ) ),
inference(func_ext,[status(esa)],[2305]) ).
thf(4,axiom,
! [A: qML_i,B: qML_mu > qML_i > $o] :
( ( scott_P @ B @ A )
=> ! [C: qML_i] : ( scott_P @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_A4) ).
thf(20,plain,
! [A: qML_i,B: qML_mu > qML_i > $o] :
( ( scott_P @ B @ A )
=> ! [C: qML_i] : ( scott_P @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(21,plain,
! [C: qML_i,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ( scott_P @ B @ C ) ),
inference(cnf,[status(esa)],[20]) ).
thf(47,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ( ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A )
!= ( scott_P @ B @ A ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[37]) ).
thf(48,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ( ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A )
!= ( scott_P @ B @ A ) ) ),
inference(simp,[status(thm)],[47]) ).
thf(99,plain,
! [E: qML_mu > qML_i > $o,D: qML_i,C: qML_i,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ~ $true
| ( ( scott_P
@ ^ [F: qML_mu,G: qML_i] :
~ ( E @ F @ G )
@ D )
!= ( scott_P @ E @ D ) )
| ( ( scott_P @ B @ C )
!= ( scott_P @ E @ D ) ) ),
inference(paramod_ordered,[status(thm)],[21,48]) ).
thf(100,plain,
! [E: qML_mu > qML_i > $o,D: qML_i,C: qML_i,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ( ( scott_P
@ ^ [F: qML_mu,G: qML_i] :
~ ( E @ F @ G )
@ D )
!= ( scott_P @ E @ D ) )
| ( ( scott_P @ B @ C )
!= ( scott_P @ E @ D ) ) ),
inference(simp,[status(thm)],[99]) ).
thf(101,plain,
! [C: qML_i,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ( ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( B @ D @ E )
@ C )
!= ( scott_P @ B @ C ) ) ),
inference(pattern_uni,[status(thm)],[100:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( C )),bind(E,$thf( B ))]]) ).
thf(426,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( scott_P @ scott_G @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] : $false
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[25,365]) ).
thf(427,plain,
! [B: qML_i,A: qML_i] :
( ( scott_P @ scott_G @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] : $false
@ B ) ),
inference(simp,[status(thm)],[426]) ).
thf(442,plain,
! [B: qML_i,A: qML_i] :
( ( scott_G
!= ( ^ [C: qML_mu,D: qML_i] : $false ) )
| ( A != B ) ),
inference(simp,[status(thm)],[427]) ).
thf(448,plain,
( scott_G
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ),
inference(simp,[status(thm)],[442]) ).
thf(532,plain,
scott_G @ sk24 @ sk25,
inference(func_ext,[status(esa)],[448]) ).
thf(626,plain,
! [B: qML_mu,A: qML_i] :
( ~ $true
| ( scott_ess_QML_mu @ scott_G @ B @ A )
| ( ( scott_G @ sk24 @ sk25 )
!= ( scott_G @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[532,39]) ).
thf(627,plain,
! [B: qML_mu,A: qML_i] :
( ( scott_ess_QML_mu @ scott_G @ B @ A )
| ( ( scott_G @ sk24 @ sk25 )
!= ( scott_G @ B @ A ) ) ),
inference(simp,[status(thm)],[626]) ).
thf(628,plain,
scott_ess_QML_mu @ scott_G @ sk24 @ sk25,
inference(pattern_uni,[status(thm)],[627:[bind(A,$thf( sk25 )),bind(B,$thf( sk24 ))]]) ).
thf(145,plain,
( ( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( scott_NE_QML_mu @ A @ B ) ) )
| ( scott_G != scott_G ) ),
inference(paramod_ordered,[status(thm)],[19,143]) ).
thf(146,plain,
( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( scott_NE_QML_mu @ A @ B ) ) ),
inference(pattern_uni,[status(thm)],[145:[]]) ).
thf(147,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk12 )
=> ( A @ sk11 @ sk12 ) ) )
!= ( ~ ( scott_NE_QML_mu @ sk11 @ sk12 ) ) ),
inference(func_ext,[status(esa)],[146]) ).
thf(751,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk12 )
=> ( A @ sk11 @ sk12 ) )
| ~ ~ ( scott_NE_QML_mu @ sk11 @ sk12 ) ),
inference(bool_ext,[status(thm)],[147]) ).
thf(774,plain,
( ( ( scott_P @ sk39 @ sk12 )
| ( scott_NE_QML_mu @ sk11 @ sk12 ) )
& ( ~ ( sk39 @ sk11 @ sk12 )
| ( scott_NE_QML_mu @ sk11 @ sk12 ) ) ),
inference(cnf,[status(esa)],[751]) ).
thf(775,plain,
( ( scott_P @ sk39 @ sk12 )
| ( scott_NE_QML_mu @ sk11 @ sk12 ) ),
inference(cnfConj,[status(thm)],[774]) ).
thf(917,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk11 @ sk12 )
| ~ $true
| ( ( scott_P @ sk39 @ sk12 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[775,365]) ).
thf(918,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk11 @ sk12 )
| ( ( scott_P @ sk39 @ sk12 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(simp,[status(thm)],[917]) ).
thf(950,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk11 @ sk12 )
| ( sk39
!= ( ^ [B: qML_mu,C: qML_i] : $false ) )
| ( sk12 != A ) ),
inference(simp,[status(thm)],[918]) ).
thf(960,plain,
( ( scott_NE_QML_mu @ sk11 @ sk12 )
| ( sk39
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ) ),
inference(simp,[status(thm)],[950]) ).
thf(962,plain,
( ( sk39 @ sk44 @ sk45 )
| ( scott_NE_QML_mu @ sk11 @ sk12 ) ),
inference(func_ext,[status(esa)],[960]) ).
thf(1050,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( scott_P @ scott_G @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[25,337]) ).
thf(1051,plain,
! [B: qML_i,A: qML_i] :
( ( scott_P @ scott_G @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) )
@ B ) ),
inference(simp,[status(thm)],[1050]) ).
thf(1069,plain,
! [B: qML_i,A: qML_i] :
( ( scott_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[1051]) ).
thf(1075,plain,
( scott_G
!= ( ^ [A: qML_mu,B: qML_i] :
~ ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) ),
inference(simp,[status(thm)],[1069]) ).
thf(1078,plain,
( ( scott_G @ sk57 @ sk58 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk57 @ sk58 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) ) ),
inference(func_ext,[status(esa)],[1075]) ).
thf(972,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ~ ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ sk18 )
=> ( C @ sk17 @ sk18 ) ) ) )
| ( ( scott_NE_QML_mu @ A @ B )
!= ( scott_NE_QML_mu @ sk17 @ sk18 ) ) ),
inference(paramod_ordered,[status(thm)],[56,317]) ).
thf(973,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk17 @ sk18 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk18 )
=> ( A @ sk17 @ sk18 ) ) ) ),
inference(pattern_uni,[status(thm)],[972:[bind(A,$thf( sk17 )),bind(B,$thf( sk18 ))]]) ).
thf(303,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( scott_P @ scott_G @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[25,173]) ).
thf(304,plain,
! [B: qML_i,A: qML_i] :
( ( scott_P @ scott_G @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) )
@ B ) ),
inference(simp,[status(thm)],[303]) ).
thf(313,plain,
! [B: qML_i,A: qML_i] :
( ( scott_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[304]) ).
thf(316,plain,
( scott_G
!= ( ^ [A: qML_mu,B: qML_i] :
~ ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
inference(simp,[status(thm)],[313]) ).
thf(320,plain,
( ( scott_G @ sk19 @ sk20 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk20 )
=> ( A @ sk19 @ sk20 ) ) ) ),
inference(func_ext,[status(esa)],[316]) ).
thf(46,plain,
! [B: qML_i,A: qML_mu] :
( ( scott_G @ A @ B )
= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
inference(func_ext,[status(esa)],[19]) ).
thf(70,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ~ $true
| ( ( scott_P @ scott_G @ A )
!= ( scott_P @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[25,37]) ).
thf(71,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ( ( scott_P @ scott_G @ A )
!= ( scott_P @ C @ B ) ) ),
inference(simp,[status(thm)],[70]) ).
thf(72,plain,
! [A: qML_i] :
~ ( scott_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( scott_G @ B @ C )
@ A ),
inference(pattern_uni,[status(thm)],[71:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( scott_G ))]]) ).
thf(122,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( scott_P @ scott_NE_QML_mu @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( scott_G @ C @ D )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[35,72]) ).
thf(123,plain,
! [B: qML_i,A: qML_i] :
( ( scott_P @ scott_NE_QML_mu @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( scott_G @ C @ D )
@ B ) ),
inference(simp,[status(thm)],[122]) ).
thf(126,plain,
! [B: qML_i,A: qML_i] :
( ( scott_NE_QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( scott_G @ C @ D ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[123]) ).
thf(128,plain,
( scott_NE_QML_mu
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( scott_G @ A @ B ) ) ),
inference(simp,[status(thm)],[126]) ).
thf(131,plain,
( ( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( scott_G @ A @ B ) ) )
| ( scott_NE_QML_mu != scott_NE_QML_mu ) ),
inference(paramod_ordered,[status(thm)],[41,128]) ).
thf(132,plain,
( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( scott_G @ A @ B ) ) ),
inference(pattern_uni,[status(thm)],[131:[]]) ).
thf(277,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk15 @ sk16 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) )
!= ( ~ ( scott_G @ sk15 @ sk16 ) ) ),
inference(func_ext,[status(esa)],[132]) ).
thf(1165,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ sk15 @ sk16 )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) )
| ( ( scott_G @ A @ B )
!= ( scott_G @ sk15 @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[46,277]) ).
thf(1166,plain,
( ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk16 )
=> ( A @ sk15 @ sk16 ) ) )
!= ( ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk15 @ sk16 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1165:[bind(A,$thf( sk15 )),bind(B,$thf( sk16 ))]]) ).
thf(2188,plain,
! [B: qML_i,A: qML_mu] :
( ( ( scott_NE_QML_mu @ A @ B )
!= ( ~ ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ sk16 )
=> ( C @ sk15 @ sk16 ) ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ sk15 @ sk16 )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[56,1166]) ).
thf(2189,plain,
( ( scott_NE_QML_mu @ sk15 @ sk16 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk16 )
=> ( A @ sk15 @ sk16 ) ) ) ),
inference(pattern_uni,[status(thm)],[2188:[bind(A,$thf( sk15 )),bind(B,$thf( sk16 ))]]) ).
thf(2207,plain,
( ( scott_NE_QML_mu @ sk15 @ sk16 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk16 )
=> ( A @ sk15 @ sk16 ) ) ),
inference(bool_ext,[status(thm)],[2189]) ).
thf(2227,plain,
( ( ( scott_NE_QML_mu @ sk15 @ sk16 )
| ( scott_P @ sk195 @ sk16 ) )
& ( ( scott_NE_QML_mu @ sk15 @ sk16 )
| ~ ( sk195 @ sk15 @ sk16 ) ) ),
inference(cnf,[status(esa)],[2207]) ).
thf(2228,plain,
( ( scott_NE_QML_mu @ sk15 @ sk16 )
| ( scott_P @ sk195 @ sk16 ) ),
inference(cnfConj,[status(thm)],[2227]) ).
thf(2358,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk15 @ sk16 )
| ~ $true
| ( ( scott_P @ sk195 @ sk16 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[2228,365]) ).
thf(2359,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk15 @ sk16 )
| ( ( scott_P @ sk195 @ sk16 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(simp,[status(thm)],[2358]) ).
thf(2401,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk15 @ sk16 )
| ( sk195
!= ( ^ [B: qML_mu,C: qML_i] : $false ) )
| ( sk16 != A ) ),
inference(simp,[status(thm)],[2359]) ).
thf(2405,plain,
( ( scott_NE_QML_mu @ sk15 @ sk16 )
| ( sk195
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ) ),
inference(simp,[status(thm)],[2401]) ).
thf(169,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ $true
| ~ ( scott_P @ C @ B )
| ( ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( scott_P @ F @ E )
=> ( F @ D @ E ) )
@ A )
!= ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[67,37]) ).
thf(170,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P @ C @ B )
| ( ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( scott_P @ F @ E )
=> ( F @ D @ E ) )
@ A )
!= ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(simp,[status(thm)],[169]) ).
thf(178,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P @ C @ B )
| ( ( ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( scott_P @ F @ E )
=> ( F @ D @ E ) ) )
!= ( ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[170]) ).
thf(184,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ( ( ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) ) )
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) ) ),
inference(simp,[status(thm)],[178]) ).
thf(108,plain,
! [E: qML_mu > qML_i > $o,D: qML_i,C: qML_i,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ~ ( scott_P
@ ^ [F: qML_mu,G: qML_i] :
~ ( E @ F @ G )
@ D )
| ~ $true
| ( ( scott_P @ B @ C )
!= ( scott_P @ E @ D ) ) ),
inference(paramod_ordered,[status(thm)],[21,37]) ).
thf(109,plain,
! [E: qML_mu > qML_i > $o,D: qML_i,C: qML_i,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ~ ( scott_P
@ ^ [F: qML_mu,G: qML_i] :
~ ( E @ F @ G )
@ D )
| ( ( scott_P @ B @ C )
!= ( scott_P @ E @ D ) ) ),
inference(simp,[status(thm)],[108]) ).
thf(110,plain,
! [C: qML_i,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ~ ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( B @ D @ E )
@ C ) ),
inference(pattern_uni,[status(thm)],[109:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( C )),bind(E,$thf( B ))]]) ).
thf(1159,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk15 @ sk16 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) )
| ~ ~ ( scott_G @ sk15 @ sk16 ) ),
inference(bool_ext,[status(thm)],[277]) ).
thf(1190,plain,
! [A: qML_mu] :
( ( ( scott_ess_QML_mu @ sk70 @ sk15 @ sk16 )
| ( scott_G @ sk15 @ sk16 ) )
& ( ~ ( sk70 @ A @ sk71 )
| ( scott_G @ sk15 @ sk16 ) ) ),
inference(cnf,[status(esa)],[1159]) ).
thf(1191,plain,
( ( scott_ess_QML_mu @ sk70 @ sk15 @ sk16 )
| ( scott_G @ sk15 @ sk16 ) ),
inference(cnfConj,[status(thm)],[1190]) ).
thf(130,plain,
( ( scott_NE_QML_mu @ sk7 @ sk8 )
!= ( ~ ( scott_G @ sk7 @ sk8 ) ) ),
inference(func_ext,[status(esa)],[128]) ).
thf(537,plain,
( ~ ~ ( scott_G @ sk7 @ sk8 )
| ( ( scott_NE_QML_mu @ sk22 @ sk23 )
!= ( scott_NE_QML_mu @ sk7 @ sk8 ) ) ),
inference(paramod_ordered,[status(thm)],[529,130]) ).
thf(538,plain,
( ( scott_G @ sk7 @ sk8 )
| ( ( scott_NE_QML_mu @ sk22 @ sk23 )
!= ( scott_NE_QML_mu @ sk7 @ sk8 ) ) ),
inference(simp,[status(thm)],[537]) ).
thf(542,plain,
( ( scott_G @ sk7 @ sk8 )
| ( sk22 != sk7 )
| ( sk23 != sk8 ) ),
inference(simp,[status(thm)],[538]) ).
thf(691,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ~ ( scott_NE_QML_mu @ sk9 @ sk10 ) ) )
| ( ( scott_G @ A @ B )
!= ( scott_G @ sk9 @ sk10 ) ) ),
inference(paramod_ordered,[status(thm)],[46,144]) ).
thf(692,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk10 )
=> ( A @ sk9 @ sk10 ) ) )
!= ( ~ ( scott_NE_QML_mu @ sk9 @ sk10 ) ) ),
inference(pattern_uni,[status(thm)],[691:[bind(A,$thf( sk9 )),bind(B,$thf( sk10 ))]]) ).
thf(1020,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk10 )
=> ( A @ sk9 @ sk10 ) )
| ~ ~ ( scott_NE_QML_mu @ sk9 @ sk10 ) ),
inference(bool_ext,[status(thm)],[692]) ).
thf(1041,plain,
( ( ( scott_P @ sk55 @ sk10 )
| ( scott_NE_QML_mu @ sk9 @ sk10 ) )
& ( ~ ( sk55 @ sk9 @ sk10 )
| ( scott_NE_QML_mu @ sk9 @ sk10 ) ) ),
inference(cnf,[status(esa)],[1020]) ).
thf(1042,plain,
( ( scott_P @ sk55 @ sk10 )
| ( scott_NE_QML_mu @ sk9 @ sk10 ) ),
inference(cnfConj,[status(thm)],[1041]) ).
thf(1698,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk9 @ sk10 )
| ~ $true
| ( ( scott_P @ sk55 @ sk10 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[1042,365]) ).
thf(1699,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk9 @ sk10 )
| ( ( scott_P @ sk55 @ sk10 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(simp,[status(thm)],[1698]) ).
thf(1734,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk9 @ sk10 )
| ( sk55
!= ( ^ [B: qML_mu,C: qML_i] : $false ) )
| ( sk10 != A ) ),
inference(simp,[status(thm)],[1699]) ).
thf(1741,plain,
( ( scott_NE_QML_mu @ sk9 @ sk10 )
| ( sk55
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ) ),
inference(simp,[status(thm)],[1734]) ).
thf(1462,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ( scott_NE_QML_mu @ A @ B ) )
!= ( scott_G @ sk57 @ sk58 ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ sk57 @ sk58 )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[56,1078]) ).
thf(1463,plain,
( ( ~ ( scott_NE_QML_mu @ sk57 @ sk58 ) )
!= ( scott_G @ sk57 @ sk58 ) ),
inference(pattern_uni,[status(thm)],[1462:[bind(A,$thf( sk57 )),bind(B,$thf( sk58 ))]]) ).
thf(1501,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ~ ( scott_NE_QML_mu @ sk57 @ sk58 ) ) )
| ( ( scott_G @ A @ B )
!= ( scott_G @ sk57 @ sk58 ) ) ),
inference(paramod_ordered,[status(thm)],[46,1463]) ).
thf(1502,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk58 )
=> ( A @ sk57 @ sk58 ) ) )
!= ( ~ ( scott_NE_QML_mu @ sk57 @ sk58 ) ) ),
inference(pattern_uni,[status(thm)],[1501:[bind(A,$thf( sk57 )),bind(B,$thf( sk58 ))]]) ).
thf(1530,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk58 )
=> ( A @ sk57 @ sk58 ) )
| ~ ~ ( scott_NE_QML_mu @ sk57 @ sk58 ) ),
inference(bool_ext,[status(thm)],[1502]) ).
thf(1554,plain,
( ( ( scott_P @ sk132 @ sk58 )
| ( scott_NE_QML_mu @ sk57 @ sk58 ) )
& ( ~ ( sk132 @ sk57 @ sk58 )
| ( scott_NE_QML_mu @ sk57 @ sk58 ) ) ),
inference(cnf,[status(esa)],[1530]) ).
thf(1555,plain,
( ( scott_P @ sk132 @ sk58 )
| ( scott_NE_QML_mu @ sk57 @ sk58 ) ),
inference(cnfConj,[status(thm)],[1554]) ).
thf(1879,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk57 @ sk58 )
| ~ $true
| ( ( scott_P @ sk132 @ sk58 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[1555,365]) ).
thf(1880,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk57 @ sk58 )
| ( ( scott_P @ sk132 @ sk58 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(simp,[status(thm)],[1879]) ).
thf(1919,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk57 @ sk58 )
| ( sk132
!= ( ^ [B: qML_mu,C: qML_i] : $false ) )
| ( sk58 != A ) ),
inference(simp,[status(thm)],[1880]) ).
thf(1930,plain,
( ( scott_NE_QML_mu @ sk57 @ sk58 )
| ( sk132
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ) ),
inference(simp,[status(thm)],[1919]) ).
thf(1931,plain,
( ( sk132 @ sk167 @ sk168 )
| ( scott_NE_QML_mu @ sk57 @ sk58 ) ),
inference(func_ext,[status(esa)],[1930]) ).
thf(883,plain,
( ( scott_G @ sk19 @ sk20 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk20 )
=> ( A @ sk19 @ sk20 ) ) ),
inference(bool_ext,[status(thm)],[320]) ).
thf(907,plain,
( ( ( scott_G @ sk19 @ sk20 )
| ( scott_P @ sk43 @ sk20 ) )
& ( ( scott_G @ sk19 @ sk20 )
| ~ ( sk43 @ sk19 @ sk20 ) ) ),
inference(cnf,[status(esa)],[883]) ).
thf(908,plain,
( ( scott_G @ sk19 @ sk20 )
| ( scott_P @ sk43 @ sk20 ) ),
inference(cnfConj,[status(thm)],[907]) ).
thf(1560,plain,
! [A: qML_i] :
( ( scott_G @ sk19 @ sk20 )
| ~ $true
| ( ( scott_P @ sk43 @ sk20 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[908,365]) ).
thf(1561,plain,
! [A: qML_i] :
( ( scott_G @ sk19 @ sk20 )
| ( ( scott_P @ sk43 @ sk20 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(simp,[status(thm)],[1560]) ).
thf(1597,plain,
! [A: qML_i] :
( ( scott_G @ sk19 @ sk20 )
| ( sk43
!= ( ^ [B: qML_mu,C: qML_i] : $false ) )
| ( sk20 != A ) ),
inference(simp,[status(thm)],[1561]) ).
thf(1607,plain,
( ( scott_G @ sk19 @ sk20 )
| ( sk43
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ) ),
inference(simp,[status(thm)],[1597]) ).
thf(1609,plain,
( ( sk43 @ sk133 @ sk134 )
| ( scott_G @ sk19 @ sk20 ) ),
inference(func_ext,[status(esa)],[1607]) ).
thf(1962,plain,
! [B: qML_i,A: qML_mu] :
( ( ( scott_G @ A @ B )
!= ( ~ ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ sk61 @ sk62 )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ sk62 )
=> ( C @ sk61 @ sk62 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[46,1084]) ).
thf(1963,plain,
( ( scott_G @ sk61 @ sk62 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk61 @ sk62 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1962:[bind(A,$thf( sk61 )),bind(B,$thf( sk62 ))]]) ).
thf(1464,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ~ ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ sk57 @ sk58 )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) )
| ( ( scott_G @ A @ B )
!= ( scott_G @ sk57 @ sk58 ) ) ),
inference(paramod_ordered,[status(thm)],[46,1078]) ).
thf(1465,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk58 )
=> ( A @ sk57 @ sk58 ) ) )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk57 @ sk58 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1464:[bind(A,$thf( sk57 )),bind(B,$thf( sk58 ))]]) ).
thf(755,plain,
! [B: qML_i,A: qML_mu] :
( ( ( scott_G @ A @ B )
!= ( ~ ( scott_NE_QML_mu @ sk11 @ sk12 ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ sk12 )
=> ( C @ sk11 @ sk12 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[46,147]) ).
thf(756,plain,
( ( scott_G @ sk11 @ sk12 )
!= ( ~ ( scott_NE_QML_mu @ sk11 @ sk12 ) ) ),
inference(pattern_uni,[status(thm)],[755:[bind(A,$thf( sk11 )),bind(B,$thf( sk12 ))]]) ).
thf(645,plain,
( ( scott_ess_QML_mu
@ ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) )
@ sk24
@ sk25 )
| ( scott_G != scott_G ) ),
inference(paramod_ordered,[status(thm)],[19,628]) ).
thf(646,plain,
( scott_ess_QML_mu
@ ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) )
@ sk24
@ sk25 ),
inference(pattern_uni,[status(thm)],[645:[]]) ).
thf(102,plain,
! [E: qML_mu > qML_i > $o,D: qML_i,C: qML_i,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ~ ( scott_P @ E @ D )
| ~ ( scott_P @ E @ D )
| ( ( scott_P @ B @ C )
!= ( scott_P
@ ^ [F: qML_mu,G: qML_i] :
~ ( E @ F @ G )
@ D ) ) ),
inference(paramod_ordered,[status(thm)],[21,48]) ).
thf(103,plain,
! [E: qML_mu > qML_i > $o,D: qML_i,C: qML_i,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ~ ( scott_P @ E @ D )
| ( ( scott_P @ B @ C )
!= ( scott_P
@ ^ [F: qML_mu,G: qML_i] :
~ ( E @ F @ G )
@ D ) ) ),
inference(simp,[status(thm)],[102]) ).
thf(104,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ A )
| ~ ( scott_P @ C @ B ) ),
inference(pattern_uni,[status(thm)],[103:[bind(A,$thf( A )),bind(B,$thf( ^ [G: qML_mu] : ^ [H: qML_i] : ~ ( F @ G @ H ) )),bind(C,$thf( C )),bind(D,$thf( C )),bind(E,$thf( F ))]]) ).
thf(116,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ A )
| ~ ( scott_P @ C @ B ) ),
inference(simp,[status(thm)],[104]) ).
thf(16,plain,
sk2 @ sk1,
inference(cnfConj,[status(thm)],[15]) ).
thf(2888,plain,
! [C: qML_i,B: qML_mu,A: qML_mu > qML_i > $o] :
( ( ( $true
& ! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i,F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) )
= ( scott_ess_QML_mu @ A @ B @ C ) )
| ( ( sk2 @ sk1 )
!= ( A @ B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[16,157]) ).
thf(2889,plain,
! [C: qML_i,B: qML_mu,A: qML_mu > qML_i > $o] :
( ( ( ! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i,F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) )
= ( scott_ess_QML_mu @ A @ B @ C ) )
| ( ( sk2 @ sk1 )
!= ( A @ B @ C ) ) ),
inference(simp,[status(thm)],[2888]) ).
thf(2930,plain,
! [A: qML_mu] :
( ( ! [B: qML_mu > qML_i > $o] :
( ( B @ A @ sk1 )
=> ! [C: qML_i,D: qML_mu] :
( ( sk2 @ C )
=> ( B @ D @ C ) ) ) )
= ( scott_ess_QML_mu
@ ^ [B: qML_mu] : sk2
@ A
@ sk1 ) ),
inference(pre_uni,[status(thm)],[2889:[bind(A,$thf( ^ [D: qML_mu] : sk2 )),bind(B,$thf( B )),bind(C,$thf( sk1 ))]]) ).
thf(3069,plain,
! [A: qML_mu] :
( ( ! [B: qML_mu > qML_i > $o] :
( ( B @ A @ sk1 )
=> ! [C: qML_i,D: qML_mu] :
( ( sk2 @ C )
=> ( B @ D @ C ) ) ) )
= ( scott_ess_QML_mu
@ ^ [B: qML_mu] : sk2
@ A
@ sk1 ) ),
inference(simp,[status(thm)],[2930]) ).
thf(318,plain,
( ( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) ) )
| ( scott_NE_QML_mu != scott_NE_QML_mu ) ),
inference(paramod_ordered,[status(thm)],[41,315]) ).
thf(319,plain,
( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[318:[]]) ).
thf(617,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk33 @ sk34 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk34 )
=> ( A @ sk33 @ sk34 ) ) ) ),
inference(func_ext,[status(esa)],[319]) ).
thf(1641,plain,
! [B: qML_i,A: qML_mu] :
( ( ( scott_NE_QML_mu @ A @ B )
!= ( ~ ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ sk34 )
=> ( C @ sk33 @ sk34 ) ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ sk33 @ sk34 )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[56,617]) ).
thf(1642,plain,
( ( scott_NE_QML_mu @ sk33 @ sk34 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk34 )
=> ( A @ sk33 @ sk34 ) ) ) ),
inference(pattern_uni,[status(thm)],[1641:[bind(A,$thf( sk33 )),bind(B,$thf( sk34 ))]]) ).
thf(1662,plain,
( ( scott_NE_QML_mu @ sk33 @ sk34 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk34 )
=> ( A @ sk33 @ sk34 ) ) ),
inference(bool_ext,[status(thm)],[1642]) ).
thf(1682,plain,
( ( ( scott_NE_QML_mu @ sk33 @ sk34 )
| ( scott_P @ sk144 @ sk34 ) )
& ( ( scott_NE_QML_mu @ sk33 @ sk34 )
| ~ ( sk144 @ sk33 @ sk34 ) ) ),
inference(cnf,[status(esa)],[1662]) ).
thf(1683,plain,
( ( scott_NE_QML_mu @ sk33 @ sk34 )
| ( scott_P @ sk144 @ sk34 ) ),
inference(cnfConj,[status(thm)],[1682]) ).
thf(2080,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk33 @ sk34 )
| ~ $true
| ( ( scott_P @ sk144 @ sk34 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[1683,365]) ).
thf(2081,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk33 @ sk34 )
| ( ( scott_P @ sk144 @ sk34 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(simp,[status(thm)],[2080]) ).
thf(2118,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk33 @ sk34 )
| ( sk144
!= ( ^ [B: qML_mu,C: qML_i] : $false ) )
| ( sk34 != A ) ),
inference(simp,[status(thm)],[2081]) ).
thf(2125,plain,
( ( scott_NE_QML_mu @ sk33 @ sk34 )
| ( sk144
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ) ),
inference(simp,[status(thm)],[2118]) ).
thf(2132,plain,
( ( sk144 @ sk187 @ sk188 )
| ( scott_NE_QML_mu @ sk33 @ sk34 ) ),
inference(func_ext,[status(esa)],[2125]) ).
thf(9,axiom,
! [A: qML_i,B: qML_mu > qML_i > $o] :
( ~ ( scott_P @ B @ A )
=> ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_A1b) ).
thf(32,plain,
! [A: qML_i,B: qML_mu > qML_i > $o] :
( ~ ( scott_P @ B @ A )
=> ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(33,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( scott_P @ B @ A )
| ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A ) ),
inference(cnf,[status(esa)],[32]) ).
thf(988,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ~ ( scott_G @ sk7 @ sk8 ) ) )
| ( ( scott_NE_QML_mu @ A @ B )
!= ( scott_NE_QML_mu @ sk7 @ sk8 ) ) ),
inference(paramod_ordered,[status(thm)],[56,130]) ).
thf(989,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk7 @ sk8 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) )
!= ( ~ ( scott_G @ sk7 @ sk8 ) ) ),
inference(pattern_uni,[status(thm)],[988:[bind(A,$thf( sk7 )),bind(B,$thf( sk8 ))]]) ).
thf(1422,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ sk7 @ sk8 )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) )
| ( ( scott_G @ A @ B )
!= ( scott_G @ sk7 @ sk8 ) ) ),
inference(paramod_ordered,[status(thm)],[46,989]) ).
thf(1423,plain,
( ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk8 )
=> ( A @ sk7 @ sk8 ) ) )
!= ( ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk7 @ sk8 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1422:[bind(A,$thf( sk7 )),bind(B,$thf( sk8 ))]]) ).
thf(3175,plain,
! [C: qML_i,B: qML_mu,A: qML_mu > qML_i > $o] :
( ( scott_G @ sk15 @ sk16 )
| ( ( A @ B @ C )
& ! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i,F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) )
| ( ( scott_ess_QML_mu @ sk70 @ sk15 @ sk16 )
!= ( scott_ess_QML_mu @ A @ B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[1191,157]) ).
thf(3176,plain,
( ( scott_G @ sk15 @ sk16 )
| ( ( sk70 @ sk15 @ sk16 )
& ! [A: qML_mu > qML_i > $o] :
( ( A @ sk15 @ sk16 )
=> ! [B: qML_i,C: qML_mu] :
( ( sk70 @ C @ B )
=> ( A @ C @ B ) ) ) ) ),
inference(pattern_uni,[status(thm)],[3175:[bind(A,$thf( sk70 )),bind(B,$thf( sk15 )),bind(C,$thf( sk16 ))]]) ).
thf(3190,plain,
! [C: qML_mu,B: qML_i,A: qML_mu > qML_i > $o] :
( ( ( scott_G @ sk15 @ sk16 )
| ( sk70 @ sk15 @ sk16 ) )
& ( ( scott_G @ sk15 @ sk16 )
| ~ ( A @ sk15 @ sk16 )
| ~ ( sk70 @ C @ B )
| ( A @ C @ B ) ) ),
inference(cnf,[status(esa)],[3176]) ).
thf(3191,plain,
( ( scott_G @ sk15 @ sk16 )
| ( sk70 @ sk15 @ sk16 ) ),
inference(cnfConj,[status(thm)],[3190]) ).
thf(2233,plain,
! [B: qML_i,A: qML_mu] :
( ( ( scott_NE_QML_mu @ A @ B )
!= ( ~ ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ sk8 )
=> ( C @ sk7 @ sk8 ) ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ sk7 @ sk8 )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[56,1423]) ).
thf(2234,plain,
( ( scott_NE_QML_mu @ sk7 @ sk8 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk8 )
=> ( A @ sk7 @ sk8 ) ) ) ),
inference(pattern_uni,[status(thm)],[2233:[bind(A,$thf( sk7 )),bind(B,$thf( sk8 ))]]) ).
thf(2311,plain,
( ( scott_NE_QML_mu @ sk7 @ sk8 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk8 )
=> ( A @ sk7 @ sk8 ) ) ),
inference(bool_ext,[status(thm)],[2234]) ).
thf(2331,plain,
( ( ( scott_NE_QML_mu @ sk7 @ sk8 )
| ( scott_P @ sk202 @ sk8 ) )
& ( ( scott_NE_QML_mu @ sk7 @ sk8 )
| ~ ( sk202 @ sk7 @ sk8 ) ) ),
inference(cnf,[status(esa)],[2311]) ).
thf(2332,plain,
( ( scott_NE_QML_mu @ sk7 @ sk8 )
| ( scott_P @ sk202 @ sk8 ) ),
inference(cnfConj,[status(thm)],[2331]) ).
thf(2590,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk7 @ sk8 )
| ~ $true
| ( ( scott_P @ sk202 @ sk8 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[2332,365]) ).
thf(2591,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk7 @ sk8 )
| ( ( scott_P @ sk202 @ sk8 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(simp,[status(thm)],[2590]) ).
thf(2642,plain,
! [A: qML_i] :
( ( scott_NE_QML_mu @ sk7 @ sk8 )
| ( sk202
!= ( ^ [B: qML_mu,C: qML_i] : $false ) )
| ( sk8 != A ) ),
inference(simp,[status(thm)],[2591]) ).
thf(2653,plain,
( ( scott_NE_QML_mu @ sk7 @ sk8 )
| ( sk202
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ) ),
inference(simp,[status(thm)],[2642]) ).
thf(156,plain,
! [B: qML_mu,A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ B )
= ( ^ [C: qML_i] :
( ( A @ B @ C )
& ! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i,F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) ) ),
inference(func_ext,[status(esa)],[27]) ).
thf(174,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) )
@ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( scott_G @ C @ D )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[67,72]) ).
thf(175,plain,
! [B: qML_i,A: qML_i] :
( ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) )
@ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( scott_G @ C @ D )
@ B ) ),
inference(simp,[status(thm)],[174]) ).
thf(180,plain,
! [B: qML_i,A: qML_i] :
( ( ( ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) ) )
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( scott_G @ C @ D ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[175]) ).
thf(186,plain,
( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( scott_G @ A @ B ) ) ),
inference(simp,[status(thm)],[180]) ).
thf(272,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk14 )
=> ( A @ sk13 @ sk14 ) ) )
!= ( ~ ( scott_G @ sk13 @ sk14 ) ) ),
inference(func_ext,[status(esa)],[186]) ).
thf(810,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk14 )
=> ( A @ sk13 @ sk14 ) )
| ~ ~ ( scott_G @ sk13 @ sk14 ) ),
inference(bool_ext,[status(thm)],[272]) ).
thf(839,plain,
( ( ( scott_P @ sk40 @ sk14 )
| ( scott_G @ sk13 @ sk14 ) )
& ( ~ ( sk40 @ sk13 @ sk14 )
| ( scott_G @ sk13 @ sk14 ) ) ),
inference(cnf,[status(esa)],[810]) ).
thf(840,plain,
( ( scott_P @ sk40 @ sk14 )
| ( scott_G @ sk13 @ sk14 ) ),
inference(cnfConj,[status(thm)],[839]) ).
thf(1089,plain,
! [A: qML_i] :
( ( scott_G @ sk13 @ sk14 )
| ~ $true
| ( ( scott_P @ sk40 @ sk14 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[840,365]) ).
thf(1090,plain,
! [A: qML_i] :
( ( scott_G @ sk13 @ sk14 )
| ( ( scott_P @ sk40 @ sk14 )
!= ( scott_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ A ) ) ),
inference(simp,[status(thm)],[1089]) ).
thf(1127,plain,
! [A: qML_i] :
( ( scott_G @ sk13 @ sk14 )
| ( sk40
!= ( ^ [B: qML_mu,C: qML_i] : $false ) )
| ( sk14 != A ) ),
inference(simp,[status(thm)],[1090]) ).
thf(1134,plain,
( ( scott_G @ sk13 @ sk14 )
| ( sk40
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ) ),
inference(simp,[status(thm)],[1127]) ).
thf(1138,plain,
( ( sk40 @ sk63 @ sk64 )
| ( scott_G @ sk13 @ sk14 ) ),
inference(func_ext,[status(esa)],[1134]) ).
thf(535,plain,
( ( ( scott_G @ sk9 @ sk10 )
!= ( ~ $true ) )
| ( ( scott_NE_QML_mu @ sk22 @ sk23 )
!= ( scott_NE_QML_mu @ sk9 @ sk10 ) ) ),
inference(paramod_ordered,[status(thm)],[529,144]) ).
thf(536,plain,
( ( scott_G @ sk9 @ sk10 )
| ( ( scott_NE_QML_mu @ sk22 @ sk23 )
!= ( scott_NE_QML_mu @ sk9 @ sk10 ) ) ),
inference(simp,[status(thm)],[535]) ).
thf(541,plain,
( ( scott_G @ sk9 @ sk10 )
| ( sk22 != sk9 )
| ( sk23 != sk10 ) ),
inference(simp,[status(thm)],[536]) ).
thf(667,plain,
( ( sk22 != sk9 )
| ( sk23 != sk10 )
| ~ ~ ( scott_NE_QML_mu @ sk9 @ sk10 )
| ( ( scott_G @ sk9 @ sk10 )
!= ( scott_G @ sk9 @ sk10 ) ) ),
inference(paramod_ordered,[status(thm)],[541,144]) ).
thf(668,plain,
( ( sk22 != sk9 )
| ( sk23 != sk10 )
| ( scott_NE_QML_mu @ sk9 @ sk10 )
| ( ( scott_G @ sk9 @ sk10 )
!= ( scott_G @ sk9 @ sk10 ) ) ),
inference(simp,[status(thm)],[667]) ).
thf(669,plain,
( ( sk22 != sk9 )
| ( sk23 != sk10 )
| ( scott_NE_QML_mu @ sk9 @ sk10 ) ),
inference(pattern_uni,[status(thm)],[668:[]]) ).
thf(1983,plain,
! [B: qML_i,A: qML_mu] :
( ( ( scott_G @ A @ B )
!= ( ~ ( scott_NE_QML_mu @ sk61 @ sk62 ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ sk62 )
=> ( C @ sk61 @ sk62 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[46,1961]) ).
thf(1984,plain,
( ( scott_G @ sk61 @ sk62 )
!= ( ~ ( scott_NE_QML_mu @ sk61 @ sk62 ) ) ),
inference(pattern_uni,[status(thm)],[1983:[bind(A,$thf( sk61 )),bind(B,$thf( sk62 ))]]) ).
thf(983,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ sk12 )
=> ( C @ sk11 @ sk12 ) ) ) )
| ( ( scott_NE_QML_mu @ A @ B )
!= ( scott_NE_QML_mu @ sk11 @ sk12 ) ) ),
inference(paramod_ordered,[status(thm)],[56,147]) ).
thf(984,plain,
( ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk11 @ sk12 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) )
!= ( ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk12 )
=> ( A @ sk11 @ sk12 ) ) ) ),
inference(pattern_uni,[status(thm)],[983:[bind(A,$thf( sk11 )),bind(B,$thf( sk12 ))]]) ).
thf(323,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) )
@ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( scott_NE_QML_mu @ C @ D )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[78,88]) ).
thf(324,plain,
! [B: qML_i,A: qML_i] :
( ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) )
@ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( scott_NE_QML_mu @ C @ D )
@ B ) ),
inference(simp,[status(thm)],[323]) ).
thf(350,plain,
! [B: qML_i,A: qML_i] :
( ( ( ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) ) )
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( scott_NE_QML_mu @ C @ D ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[324]) ).
thf(360,plain,
( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( scott_NE_QML_mu @ A @ B ) ) ),
inference(simp,[status(thm)],[350]) ).
thf(5,axiom,
! [A: qML_i,B: qML_i] :
? [C: qML_mu] : ( scott_G @ C @ B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_T3) ).
thf(22,plain,
! [A: qML_i] :
? [B: qML_mu] : ( scott_G @ B @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(23,plain,
! [A: qML_i] : ( scott_G @ ( sk4 @ A ) @ A ),
inference(cnf,[status(esa)],[22]) ).
thf(631,plain,
! [C: qML_mu,B: qML_i,A: qML_i] :
( ~ $true
| ( scott_ess_QML_mu @ scott_G @ C @ B )
| ( ( scott_G @ ( sk4 @ A ) @ A )
!= ( scott_G @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[23,39]) ).
thf(632,plain,
! [C: qML_mu,B: qML_i,A: qML_i] :
( ( scott_ess_QML_mu @ scott_G @ C @ B )
| ( ( scott_G @ ( sk4 @ A ) @ A )
!= ( scott_G @ C @ B ) ) ),
inference(simp,[status(thm)],[631]) ).
thf(633,plain,
! [A: qML_i] : ( scott_ess_QML_mu @ scott_G @ ( sk4 @ A ) @ A ),
inference(pattern_uni,[status(thm)],[632:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( sk4 @ D ))]]) ).
thf(640,plain,
! [A: qML_i] : ( scott_ess_QML_mu @ scott_G @ ( sk4 @ A ) @ A ),
inference(simp,[status(thm)],[633]) ).
thf(656,plain,
! [A: qML_i] :
( ( scott_ess_QML_mu
@ ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( scott_P @ D @ C )
=> ( D @ B @ C ) )
@ ( sk4 @ A )
@ A )
| ( scott_G != scott_G ) ),
inference(paramod_ordered,[status(thm)],[19,640]) ).
thf(657,plain,
! [A: qML_i] :
( scott_ess_QML_mu
@ ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( scott_P @ D @ C )
=> ( D @ B @ C ) )
@ ( sk4 @ A )
@ A ),
inference(pattern_uni,[status(thm)],[656:[]]) ).
thf(2413,plain,
( ( sk195 @ sk207 @ sk208 )
| ( scott_NE_QML_mu @ sk15 @ sk16 ) ),
inference(func_ext,[status(esa)],[2405]) ).
thf(1747,plain,
( ( sk55 @ sk145 @ sk146 )
| ( scott_NE_QML_mu @ sk9 @ sk10 ) ),
inference(func_ext,[status(esa)],[1741]) ).
thf(428,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) )
@ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] : $false
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[78,365]) ).
thf(429,plain,
! [B: qML_i,A: qML_i] :
( ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) )
@ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] : $false
@ B ) ),
inference(simp,[status(thm)],[428]) ).
thf(438,plain,
! [B: qML_i,A: qML_i] :
( ( ( ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) ) )
!= ( ^ [C: qML_mu,D: qML_i] : $false ) )
| ( A != B ) ),
inference(simp,[status(thm)],[429]) ).
thf(444,plain,
( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ),
inference(simp,[status(thm)],[438]) ).
thf(45,plain,
! [A: qML_mu] :
( ( scott_G @ A )
= ( ^ [B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
inference(func_ext,[status(esa)],[19]) ).
thf(855,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ( scott_G @ A @ B ) )
!= ( scott_NE_QML_mu @ sk17 @ sk18 ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ sk18 )
=> ( C @ sk17 @ sk18 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[46,317]) ).
thf(856,plain,
( ( scott_NE_QML_mu @ sk17 @ sk18 )
!= ( ~ ( scott_G @ sk17 @ sk18 ) ) ),
inference(pattern_uni,[status(thm)],[855:[bind(A,$thf( sk17 )),bind(B,$thf( sk18 ))]]) ).
thf(42,plain,
( ~ $true
| ( ( sk2 @ sk3 )
!= ( sk2 @ sk1 ) ) ),
inference(paramod_ordered,[status(thm)],[16,17]) ).
thf(43,plain,
( ( sk2 @ sk3 )
!= ( sk2 @ sk1 ) ),
inference(simp,[status(thm)],[42]) ).
thf(44,plain,
sk3 != sk1,
inference(simp,[status(thm)],[43]) ).
thf(57,plain,
( ( scott_NE_QML_mu = scott_G )
| ( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[41,19]) ).
thf(59,plain,
( ( scott_NE_QML_mu = scott_G )
| ( ( ^ [A: qML_mu,B: qML_i,C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ^ [A: qML_mu,B: qML_i,C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) ) ) ),
inference(simp,[status(thm)],[57]) ).
thf(2814,plain,
! [C: qML_i,B: qML_mu,A: qML_mu > qML_i > $o] :
( ( ( $true
& ! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i,F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) )
= ( scott_ess_QML_mu @ A @ B @ C ) )
| ( ( scott_ess_QML_mu @ scott_G @ sk24 @ sk25 )
!= ( A @ B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[628,157]) ).
thf(2815,plain,
! [C: qML_i,B: qML_mu,A: qML_mu > qML_i > $o] :
( ( ( ! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i,F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) )
= ( scott_ess_QML_mu @ A @ B @ C ) )
| ( ( scott_ess_QML_mu @ scott_G @ sk24 @ sk25 )
!= ( A @ B @ C ) ) ),
inference(simp,[status(thm)],[2814]) ).
thf(2927,plain,
( ( scott_ess_QML_mu @ ( scott_ess_QML_mu @ scott_G ) @ sk24 @ sk25 )
= ( ! [A: qML_mu > qML_i > $o] :
( ( A @ sk24 @ sk25 )
=> ! [B: qML_i,C: qML_mu] :
( ( scott_ess_QML_mu @ scott_G @ C @ B )
=> ( A @ C @ B ) ) ) ) ),
inference(pre_uni,[status(thm)],[2815:[bind(A,$thf( scott_ess_QML_mu @ scott_G )),bind(B,$thf( sk24 )),bind(C,$thf( sk25 ))]]) ).
thf(3598,plain,
( ( ( scott_ess_QML_mu
@ ( scott_ess_QML_mu
@ ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
@ sk24
@ sk25 )
= ( ! [A: qML_mu > qML_i > $o] :
( ( A @ sk24 @ sk25 )
=> ! [B: qML_i,C: qML_mu] :
( ( scott_ess_QML_mu @ scott_G @ C @ B )
=> ( A @ C @ B ) ) ) ) )
| ( scott_G != scott_G ) ),
inference(paramod_ordered,[status(thm)],[19,2927]) ).
thf(3599,plain,
( ( scott_ess_QML_mu
@ ( scott_ess_QML_mu
@ ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
@ sk24
@ sk25 )
= ( ! [A: qML_mu > qML_i > $o] :
( ( A @ sk24 @ sk25 )
=> ! [B: qML_i,C: qML_mu] :
( ( scott_ess_QML_mu @ scott_G @ C @ B )
=> ( A @ C @ B ) ) ) ) ),
inference(pattern_uni,[status(thm)],[3598:[]]) ).
thf(1666,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ( scott_G @ A @ B ) )
!= ( scott_NE_QML_mu @ sk33 @ sk34 ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ sk34 )
=> ( C @ sk33 @ sk34 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[46,1642]) ).
thf(1667,plain,
( ( scott_NE_QML_mu @ sk33 @ sk34 )
!= ( ~ ( scott_G @ sk33 @ sk34 ) ) ),
inference(pattern_uni,[status(thm)],[1666:[bind(A,$thf( sk33 )),bind(B,$thf( sk34 ))]]) ).
thf(84,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ $true
| ~ ( scott_P @ C @ B )
| ( ( scott_P @ scott_NE_QML_mu @ A )
!= ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[35,37]) ).
thf(85,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P @ C @ B )
| ( ( scott_P @ scott_NE_QML_mu @ A )
!= ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(simp,[status(thm)],[84]) ).
thf(89,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P @ C @ B )
| ( scott_NE_QML_mu
!= ( ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[85]) ).
thf(91,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ( scott_NE_QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) ) ),
inference(simp,[status(thm)],[89]) ).
thf(155,plain,
! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A )
= ( ^ [B: qML_mu,C: qML_i] :
( ( A @ B @ C )
& ! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i,F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) ) ),
inference(func_ext,[status(esa)],[27]) ).
thf(783,plain,
( ~ ~ ( scott_NE_QML_mu @ sk11 @ sk12 )
| ( ( scott_G @ sk24 @ sk25 )
!= ( scott_G @ sk11 @ sk12 ) ) ),
inference(paramod_ordered,[status(thm)],[532,756]) ).
thf(784,plain,
( ( scott_NE_QML_mu @ sk11 @ sk12 )
| ( ( scott_G @ sk24 @ sk25 )
!= ( scott_G @ sk11 @ sk12 ) ) ),
inference(simp,[status(thm)],[783]) ).
thf(799,plain,
( ( scott_NE_QML_mu @ sk11 @ sk12 )
| ( sk24 != sk11 )
| ( sk25 != sk12 ) ),
inference(simp,[status(thm)],[784]) ).
thf(1161,plain,
! [B: qML_i,A: qML_mu] :
( ( ( scott_NE_QML_mu @ A @ B )
!= ( ~ ( scott_G @ sk15 @ sk16 ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ sk15 @ sk16 )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[56,277]) ).
thf(1162,plain,
( ( scott_NE_QML_mu @ sk15 @ sk16 )
!= ( ~ ( scott_G @ sk15 @ sk16 ) ) ),
inference(pattern_uni,[status(thm)],[1161:[bind(A,$thf( sk15 )),bind(B,$thf( sk16 ))]]) ).
thf(544,plain,
( ~ ~ ( scott_NE_QML_mu @ sk9 @ sk10 )
| ( ( scott_G @ sk24 @ sk25 )
!= ( scott_G @ sk9 @ sk10 ) ) ),
inference(paramod_ordered,[status(thm)],[532,144]) ).
thf(545,plain,
( ( scott_NE_QML_mu @ sk9 @ sk10 )
| ( ( scott_G @ sk24 @ sk25 )
!= ( scott_G @ sk9 @ sk10 ) ) ),
inference(simp,[status(thm)],[544]) ).
thf(548,plain,
( ( scott_NE_QML_mu @ sk9 @ sk10 )
| ( sk24 != sk9 )
| ( sk25 != sk10 ) ),
inference(simp,[status(thm)],[545]) ).
thf(331,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P @ C @ B )
| ~ ( scott_P @ C @ B )
| ( ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ F @ D @ E )
=> ! [G: qML_i] :
? [H: qML_mu] : ( F @ H @ G ) )
@ A )
!= ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[78,48]) ).
thf(332,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P @ C @ B )
| ( ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ F @ D @ E )
=> ! [G: qML_i] :
? [H: qML_mu] : ( F @ H @ G ) )
@ A )
!= ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(simp,[status(thm)],[331]) ).
thf(353,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P @ C @ B )
| ( ( ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ F @ D @ E )
=> ! [G: qML_i] :
? [H: qML_mu] : ( F @ H @ G ) ) )
!= ( ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[332]) ).
thf(355,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ( ( ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) ) )
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) ) ),
inference(simp,[status(thm)],[353]) ).
thf(1060,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( scott_P @ scott_NE_QML_mu @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[35,337]) ).
thf(1061,plain,
! [B: qML_i,A: qML_i] :
( ( scott_P @ scott_NE_QML_mu @ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) )
@ B ) ),
inference(simp,[status(thm)],[1060]) ).
thf(1071,plain,
! [B: qML_i,A: qML_i] :
( ( scott_NE_QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
? [G: qML_mu] : ( E @ G @ F ) ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[1061]) ).
thf(1077,plain,
( scott_NE_QML_mu
!= ( ^ [A: qML_mu,B: qML_i] :
~ ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) ),
inference(simp,[status(thm)],[1071]) ).
thf(1081,plain,
( ( scott_NE_QML_mu @ sk59 @ sk60 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk59 @ sk60 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) ) ),
inference(func_ext,[status(esa)],[1077]) ).
thf(31,plain,
! [C: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ~ ( C @ ( sk6 @ C @ B @ A ) @ ( sk5 @ C @ B @ A ) )
| ( scott_P @ C @ A ) ),
inference(cnfConj,[status(thm)],[29]) ).
thf(1022,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ sk10 )
=> ( C @ sk9 @ sk10 ) ) ) )
| ( ( scott_NE_QML_mu @ A @ B )
!= ( scott_NE_QML_mu @ sk9 @ sk10 ) ) ),
inference(paramod_ordered,[status(thm)],[56,692]) ).
thf(1023,plain,
( ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk9 @ sk10 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) )
!= ( ! [A: qML_mu > qML_i > $o] :
( ( scott_P @ A @ sk10 )
=> ( A @ sk9 @ sk10 ) ) ) ),
inference(pattern_uni,[status(thm)],[1022:[bind(A,$thf( sk9 )),bind(B,$thf( sk10 ))]]) ).
thf(612,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk31 @ sk32 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) )
!= ( ~ ( scott_NE_QML_mu @ sk31 @ sk32 ) ) ),
inference(func_ext,[status(esa)],[360]) ).
thf(975,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( scott_G @ sk9 @ sk10 ) )
| ( ( scott_NE_QML_mu @ A @ B )
!= ( scott_NE_QML_mu @ sk9 @ sk10 ) ) ),
inference(paramod_ordered,[status(thm)],[56,144]) ).
thf(976,plain,
( ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk9 @ sk10 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) )
!= ( scott_G @ sk9 @ sk10 ) ),
inference(pattern_uni,[status(thm)],[975:[bind(A,$thf( sk9 )),bind(B,$thf( sk10 ))]]) ).
thf(1645,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ( scott_G @ A @ B ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ sk33 @ sk34 )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ sk34 )
=> ( C @ sk33 @ sk34 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[46,617]) ).
thf(1646,plain,
( ( ~ ( scott_G @ sk33 @ sk34 ) )
!= ( ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk33 @ sk34 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1645:[bind(A,$thf( sk33 )),bind(B,$thf( sk34 ))]]) ).
thf(55,plain,
! [A: qML_mu] :
( ( scott_NE_QML_mu @ A )
= ( ^ [B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) ) ),
inference(func_ext,[status(esa)],[41]) ).
thf(68,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ $true
| ~ ( scott_P @ C @ B )
| ( ( scott_P @ scott_G @ A )
!= ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[25,37]) ).
thf(69,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P @ C @ B )
| ( ( scott_P @ scott_G @ A )
!= ( scott_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(simp,[status(thm)],[68]) ).
thf(73,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( scott_P @ C @ B )
| ( scott_G
!= ( ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[69]) ).
thf(75,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( scott_P @ B @ A )
| ( scott_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) ) ),
inference(simp,[status(thm)],[73]) ).
thf(432,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) )
@ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] : $false
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[67,365]) ).
thf(433,plain,
! [B: qML_i,A: qML_i] :
( ( scott_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) )
@ A )
!= ( scott_P
@ ^ [C: qML_mu,D: qML_i] : $false
@ B ) ),
inference(simp,[status(thm)],[432]) ).
thf(441,plain,
! [B: qML_i,A: qML_i] :
( ( ( ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( scott_P @ E @ D )
=> ( E @ C @ D ) ) )
!= ( ^ [C: qML_mu,D: qML_i] : $false ) )
| ( A != B ) ),
inference(simp,[status(thm)],[433]) ).
thf(447,plain,
( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( scott_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ),
inference(simp,[status(thm)],[441]) ).
thf(781,plain,
( ( ( scott_G @ sk11 @ sk12 )
!= ( ~ $true ) )
| ( ( scott_NE_QML_mu @ sk22 @ sk23 )
!= ( scott_NE_QML_mu @ sk11 @ sk12 ) ) ),
inference(paramod_ordered,[status(thm)],[529,756]) ).
thf(782,plain,
( ( scott_G @ sk11 @ sk12 )
| ( ( scott_NE_QML_mu @ sk22 @ sk23 )
!= ( scott_NE_QML_mu @ sk11 @ sk12 ) ) ),
inference(simp,[status(thm)],[781]) ).
thf(796,plain,
( ( scott_G @ sk11 @ sk12 )
| ( sk22 != sk11 )
| ( sk23 != sk12 ) ),
inference(simp,[status(thm)],[782]) ).
thf(986,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( ~ ( scott_G @ sk17 @ sk18 ) ) )
| ( ( scott_NE_QML_mu @ A @ B )
!= ( scott_NE_QML_mu @ sk17 @ sk18 ) ) ),
inference(paramod_ordered,[status(thm)],[56,856]) ).
thf(987,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk17 @ sk18 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) )
!= ( ~ ( scott_G @ sk17 @ sk18 ) ) ),
inference(pattern_uni,[status(thm)],[986:[bind(A,$thf( sk17 )),bind(B,$thf( sk18 ))]]) ).
thf(981,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ! [C: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
? [E: qML_mu] : ( C @ E @ D ) ) )
!= ( scott_G @ sk11 @ sk12 ) )
| ( ( scott_NE_QML_mu @ A @ B )
!= ( scott_NE_QML_mu @ sk11 @ sk12 ) ) ),
inference(paramod_ordered,[status(thm)],[56,756]) ).
thf(982,plain,
( ( ~ ! [A: qML_mu > qML_i > $o] :
( ( scott_ess_QML_mu @ A @ sk11 @ sk12 )
=> ! [B: qML_i] :
? [C: qML_mu] : ( A @ C @ B ) ) )
!= ( scott_G @ sk11 @ sk12 ) ),
inference(pattern_uni,[status(thm)],[981:[bind(A,$thf( sk11 )),bind(B,$thf( sk12 ))]]) ).
thf(1331,plain,
( ( sk42 @ sk93 @ sk94 )
| ( scott_NE_QML_mu @ sk17 @ sk18 ) ),
inference(func_ext,[status(esa)],[1322]) ).
thf(2655,plain,
( ( sk202 @ sk211 @ sk212 )
| ( scott_NE_QML_mu @ sk7 @ sk8 ) ),
inference(func_ext,[status(esa)],[2653]) ).
thf(7539,plain,
$false,
inference(e,[status(thm)],[3509,144,39,1322,365,2306,101,628,962,88,1078,56,24,973,320,37,2405,25,14,184,110,1191,542,157,20,1741,1931,448,78,46,1609,316,1963,1465,756,646,147,692,866,132,2002,116,1074,529,1042,1502,3069,21,2132,33,28,38,1423,3191,2228,2653,1555,2332,317,156,1138,989,3018,1683,669,1075,2125,1984,41,984,173,128,360,541,657,2189,2413,1747,17,444,32,34,45,856,22,44,59,27,3599,1667,91,155,799,1162,130,35,1166,548,2234,1134,617,355,1081,2927,48,18,640,1961,67,16,840,31,1023,72,446,612,143,1084,976,2305,1646,319,40,26,186,55,23,75,1077,1607,272,1642,447,315,36,146,30,19,960,532,796,1930,987,908,982,277,1331,337,1463,775,2655]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PHI008^4 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21 % Computer : n002.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.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Tue Sep 29 13:22:22 UTC 2026
% 0.10/0.21 % CPUTime :
% 0.10/0.21 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.89/0.79 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.24/1.01 % [INFO] Parsing done (210ms).
% 1.24/1.02 % [INFO] Running in sequential loop mode.
% 2.16/1.44 % [INFO] eprover registered as external prover.
% 2.16/1.45 % [INFO] Scanning for conjecture ...
% 2.37/1.54 % [INFO] Found a conjecture (or negated_conjecture) and 11 axioms. Running axiom selection ...
% 2.37/1.58 % [INFO] Axiom selection finished. Selected 11 axioms (removed 0 axioms).
% 2.54/1.61 % [INFO] Problem is higher-order (TPTP THF).
% 2.54/1.62 % [INFO] Type checking passed.
% 2.54/1.62 % [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 ...
% 93.69/23.29 % External prover 'e' found a proof!
% 93.69/23.29 % [INFO] Killing All external provers ...
% 93.69/23.30 % Time passed: 22939ms (effective reasoning time: 22265ms)
% 93.69/23.30 % 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)>
% 93.49/23.30 % Axioms used in derivation (11): fact_2_T3, fact_3_A3, fact_10_NE__def, fact_0_G__def, fact_5_A2, fact_7_A5, fact_8_A1a, fact_9_T2, fact_6_A1b, fact_1_A4, fact_4_ess__def
% 93.49/23.30 % No. of inferences in proof: 356
% 93.49/23.30 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 22939 ms resp. 22265 ms w/o parsing
% 94.24/23.50 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 94.24/23.51 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------