%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : PHI007^5 : TPTP v9.3.1. Released v6.4.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 : n004.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 94.04s 39.43s
% Output : Refutation 94.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 49
% Syntax : Number of formulae : 473 ( 117 unt; 0 typ; 39 def)
% Number of atoms : 2049 ( 409 equ; 0 cnn)
% Maximal formula atoms : 7 ( 4 avg)
% Number of connectives : 5339 ( 890 ~; 497 |; 41 &;3512 @)
% ( 0 <=>; 399 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 724 ( 724 >; 0 *; 0 +; 0 <<)
% Number of symbols : 71 ( 68 usr; 39 con; 0-3 aty)
% Number of variables : 1499 ( 558 ^; 776 !; 126 ?;1499 :)
% ( 0 !>; 0 ?*; 0 @-; 39 @+)
% Comments :
%------------------------------------------------------------------------------
thf(qML_mu_type,type,
qML_mu: $tType ).
thf(qML_i_type,type,
qML_i: $tType ).
thf(inconsistency_G_decl,type,
inconsistency_G: qML_mu > qML_i > $o ).
thf(incons1905966852QML_mu_decl,type,
incons1905966852QML_mu: qML_mu > qML_i > $o ).
thf(inconsistency_P_decl,type,
inconsistency_P: ( qML_mu > qML_i > $o ) > qML_i > $o ).
thf(incons1389517216QML_mu_decl,type,
incons1389517216QML_mu: ( qML_mu > qML_i > $o ) > qML_mu > qML_i > $o ).
thf(qML_r_decl,type,
qML_r: qML_i > qML_i > $o ).
thf(sk1_decl,type,
sk1: ( qML_mu > qML_i > $o ) > ( qML_mu > qML_i > $o ) > qML_i > qML_i ).
thf(sk2_decl,type,
sk2: ( qML_mu > qML_i > $o ) > ( qML_mu > qML_i > $o ) > qML_i > qML_mu ).
thf(sk3_decl,type,
sk3: qML_mu ).
thf(sk4_decl,type,
sk4: qML_i ).
thf(sk5_decl,type,
sk5: qML_mu ).
thf(sk6_decl,type,
sk6: qML_i ).
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 > qML_i > $o ).
thf(sk18_decl,type,
sk18: qML_mu > qML_i > $o ).
thf(sk21_decl,type,
sk21: qML_mu > qML_i > $o ).
thf(sk22_decl,type,
sk22: qML_mu > qML_i > $o ).
thf(sk23_decl,type,
sk23: qML_mu ).
thf(sk24_decl,type,
sk24: qML_i ).
thf(sk26_decl,type,
sk26: qML_mu ).
thf(sk27_decl,type,
sk27: qML_i ).
thf(sk28_decl,type,
sk28: qML_mu ).
thf(sk29_decl,type,
sk29: qML_i ).
thf(sk30_decl,type,
sk30: qML_mu ).
thf(sk31_decl,type,
sk31: qML_i ).
thf(sk36_decl,type,
sk36: qML_mu ).
thf(sk37_decl,type,
sk37: qML_i ).
thf(sk41_decl,type,
sk41: qML_mu > qML_i > $o ).
thf(sk42_decl,type,
sk42: qML_i ).
thf(sk44_decl,type,
sk44: qML_mu > qML_i > $o ).
thf(sk45_decl,type,
sk45: qML_i ).
thf(sk53_decl,type,
sk53: qML_mu > qML_i > $o ).
thf(sk54_decl,type,
sk54: qML_i ).
thf(sk56_decl,type,
sk56: qML_mu > qML_i > $o ).
thf(sk57_decl,type,
sk57: qML_i ).
thf(sk63_decl,type,
sk63: qML_mu > qML_i > $o ).
thf(sk65_decl,type,
sk65: qML_mu > qML_i > $o ).
thf(sk67_decl,type,
sk67: qML_mu > qML_i > $o ).
thf(sk75_decl,type,
sk75: qML_mu > qML_i > $o ).
thf(sk76_decl,type,
sk76: qML_i ).
thf(sk88_decl,type,
sk88: qML_mu > qML_i > $o ).
thf(sk89_decl,type,
sk89: qML_i ).
thf(sk110_decl,type,
sk110: qML_mu > qML_i > $o ).
thf(sk111_decl,type,
sk111: qML_i ).
thf(sk123_decl,type,
sk123: qML_mu > qML_i > $o ).
thf(sk124_decl,type,
sk124: qML_i ).
thf(sk125_decl,type,
sk125: qML_mu > qML_i > $o ).
thf(sk132_decl,type,
sk132: qML_mu > qML_i > $o ).
thf(sk134_decl,type,
sk134: qML_mu > qML_i > $o ).
thf(sk135_decl,type,
sk135: qML_mu > qML_i > $o ).
thf(sk136_decl,type,
sk136: qML_mu > qML_i > $o ).
thf(sk137_decl,type,
sk137: qML_i ).
thf(sk141_decl,type,
sk141: qML_mu > qML_i > $o ).
thf(sk142_decl,type,
sk142: qML_i ).
thf(sk145_decl,type,
sk145: qML_mu > qML_i > $o ).
thf(sk146_decl,type,
sk146: qML_i ).
thf(sk150_decl,type,
sk150: qML_mu > qML_i > $o ).
thf(sk151_decl,type,
sk151: qML_i ).
thf(sk155_decl,type,
sk155: qML_mu > qML_i > $o ).
thf(sk156_decl,type,
sk156: qML_i ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,C: qML_i] :
@+[D: qML_i] :
~ ( ( qML_r @ C @ D )
=> ! [E: qML_mu] :
( ( B @ E @ D )
=> ( A @ E @ D ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,C: qML_i] :
@+[D: qML_mu] :
~ ( ( B @ D @ ( sk1 @ A @ B @ C ) )
=> ( A @ D @ ( sk1 @ A @ B @ C ) ) ) ) ) ).
thf(sk17_def,definition,
( sk17
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( inconsistency_P @ A @ sk8 )
=> ( A @ sk7 @ sk8 ) ) ) ) ).
thf(sk18_def,definition,
( sk18
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( inconsistency_P @ A @ sk10 )
=> ( A @ sk9 @ sk10 ) ) ) ) ).
thf(sk21_def,definition,
( sk21
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( inconsistency_P @ A @ sk12 )
=> ( A @ sk11 @ sk12 ) ) ) ) ).
thf(sk22_def,definition,
( sk22
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( inconsistency_P @ A @ sk14 )
=> ( A @ sk13 @ sk14 ) ) ) ) ).
thf(sk41_def,definition,
( sk41
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( incons1389517216QML_mu @ A @ sk15 @ sk16 )
=> ! [B: qML_i] :
( ( qML_r @ sk16 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ) ).
thf(sk42_def,definition,
( sk42
= ( @+[A: qML_i] :
~ ( ( qML_r @ sk16 @ A )
=> ? [B: qML_mu] : ( sk41 @ B @ A ) ) ) ) ).
thf(sk44_def,definition,
( sk44
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( incons1389517216QML_mu @ A @ sk26 @ sk27 )
=> ! [B: qML_i] :
( ( qML_r @ sk27 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ) ).
thf(sk45_def,definition,
( sk45
= ( @+[A: qML_i] :
~ ( ( qML_r @ sk27 @ A )
=> ? [B: qML_mu] : ( sk44 @ B @ A ) ) ) ) ).
thf(sk53_def,definition,
( sk53
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( incons1389517216QML_mu @ A @ sk28 @ sk29 )
=> ! [B: qML_i] :
( ( qML_r @ sk29 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ) ).
thf(sk54_def,definition,
( sk54
= ( @+[A: qML_i] :
~ ( ( qML_r @ sk29 @ A )
=> ? [B: qML_mu] : ( sk53 @ B @ A ) ) ) ) ).
thf(sk56_def,definition,
( sk56
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( incons1389517216QML_mu @ A @ sk30 @ sk31 )
=> ! [B: qML_i] :
( ( qML_r @ sk31 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ) ).
thf(sk57_def,definition,
( sk57
= ( @+[A: qML_i] :
~ ( ( qML_r @ sk31 @ A )
=> ? [B: qML_mu] : ( sk56 @ B @ A ) ) ) ) ).
thf(sk63_def,definition,
( sk63
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( inconsistency_P @ A @ sk6 )
=> ( A @ sk5 @ sk6 ) ) ) ) ).
thf(sk65_def,definition,
( sk65
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( inconsistency_P @ A @ sk4 )
=> ( A @ sk3 @ sk4 ) ) ) ) ).
thf(sk67_def,definition,
( sk67
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( inconsistency_P @ A @ sk4 )
=> ( A @ sk3 @ sk4 ) ) ) ) ).
thf(sk75_def,definition,
( sk75
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( incons1389517216QML_mu @ A @ sk23 @ sk24 )
=> ! [B: qML_i] :
( ( qML_r @ sk24 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ) ).
thf(sk76_def,definition,
( sk76
= ( @+[A: qML_i] :
~ ( ( qML_r @ sk24 @ A )
=> ? [B: qML_mu] : ( sk75 @ B @ A ) ) ) ) ).
thf(sk88_def,definition,
( sk88
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( incons1389517216QML_mu @ A @ sk36 @ sk37 )
=> ! [B: qML_i] :
( ( qML_r @ sk37 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ) ).
thf(sk89_def,definition,
( sk89
= ( @+[A: qML_i] :
~ ( ( qML_r @ sk37 @ A )
=> ? [B: qML_mu] : ( sk88 @ B @ A ) ) ) ) ).
thf(sk110_def,definition,
( sk110
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( incons1389517216QML_mu @ A @ sk3 @ sk4 )
=> ! [B: qML_i] :
( ( qML_r @ sk4 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ) ).
thf(sk111_def,definition,
( sk111
= ( @+[A: qML_i] :
~ ( ( qML_r @ sk4 @ A )
=> ? [B: qML_mu] : ( sk110 @ B @ A ) ) ) ) ).
thf(sk123_def,definition,
( sk123
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( incons1389517216QML_mu @ A @ sk5 @ sk6 )
=> ! [B: qML_i] :
( ( qML_r @ sk6 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ) ).
thf(sk124_def,definition,
( sk124
= ( @+[A: qML_i] :
~ ( ( qML_r @ sk6 @ A )
=> ? [B: qML_mu] : ( sk123 @ B @ A ) ) ) ) ).
thf(sk125_def,definition,
( sk125
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( inconsistency_P @ A @ sk37 )
=> ( A @ sk36 @ sk37 ) ) ) ) ).
thf(sk132_def,definition,
( sk132
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( inconsistency_P @ A @ sk29 )
=> ( A @ sk28 @ sk29 ) ) ) ) ).
thf(sk134_def,definition,
( sk134
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( inconsistency_P @ A @ sk16 )
=> ( A @ sk15 @ sk16 ) ) ) ) ).
thf(sk135_def,definition,
( sk135
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( inconsistency_P @ A @ sk24 )
=> ( A @ sk23 @ sk24 ) ) ) ) ).
thf(sk136_def,definition,
( sk136
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( incons1389517216QML_mu @ A @ sk13 @ sk14 )
=> ! [B: qML_i] :
( ( qML_r @ sk14 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ) ).
thf(sk137_def,definition,
( sk137
= ( @+[A: qML_i] :
~ ( ( qML_r @ sk14 @ A )
=> ? [B: qML_mu] : ( sk136 @ B @ A ) ) ) ) ).
thf(sk141_def,definition,
( sk141
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( incons1389517216QML_mu @ A @ sk13 @ sk14 )
=> ! [B: qML_i] :
( ( qML_r @ sk14 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ) ).
thf(sk142_def,definition,
( sk142
= ( @+[A: qML_i] :
~ ( ( qML_r @ sk14 @ A )
=> ? [B: qML_mu] : ( sk141 @ B @ A ) ) ) ) ).
thf(sk145_def,definition,
( sk145
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( incons1389517216QML_mu @ A @ sk7 @ sk8 )
=> ! [B: qML_i] :
( ( qML_r @ sk8 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ) ).
thf(sk146_def,definition,
( sk146
= ( @+[A: qML_i] :
~ ( ( qML_r @ sk8 @ A )
=> ? [B: qML_mu] : ( sk145 @ B @ A ) ) ) ) ).
thf(sk150_def,definition,
( sk150
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( incons1389517216QML_mu @ A @ sk3 @ sk4 )
=> ! [B: qML_i] :
( ( qML_r @ sk4 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ) ).
thf(sk151_def,definition,
( sk151
= ( @+[A: qML_i] :
~ ( ( qML_r @ sk4 @ A )
=> ? [B: qML_mu] : ( sk150 @ B @ A ) ) ) ) ).
thf(sk155_def,definition,
( sk155
= ( @+[A: qML_mu > qML_i > $o] :
~ ( ( incons1389517216QML_mu @ A @ sk5 @ sk6 )
=> ! [B: qML_i] :
( ( qML_r @ sk6 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ) ).
thf(sk156_def,definition,
( sk156
= ( @+[A: qML_i] :
~ ( ( qML_r @ sk6 @ A )
=> ? [B: qML_mu] : ( sk155 @ B @ A ) ) ) ) ).
thf(8,axiom,
! [A: qML_i] : ( inconsistency_P @ incons1905966852QML_mu @ A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_A5) ).
thf(26,plain,
! [A: qML_i] : ( inconsistency_P @ incons1905966852QML_mu @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(27,plain,
! [A: qML_i] : ( inconsistency_P @ incons1905966852QML_mu @ A ),
inference(cnf,[status(esa)],[26]) ).
thf(6,axiom,
! [A: qML_i] : ( inconsistency_P @ inconsistency_G @ A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_A3) ).
thf(22,plain,
! [A: qML_i] : ( inconsistency_P @ inconsistency_G @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(23,plain,
! [A: qML_i] : ( inconsistency_P @ inconsistency_G @ A ),
inference(cnf,[status(esa)],[22]) ).
thf(3,axiom,
! [A: qML_i,B: qML_mu > qML_i > $o] :
( ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A )
=> ~ ( inconsistency_P @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_A1a) ).
thf(13,plain,
! [A: qML_i,B: qML_mu > qML_i > $o] :
( ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A )
=> ~ ( inconsistency_P @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(14,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A )
| ~ ( inconsistency_P @ B @ A ) ),
inference(cnf,[status(esa)],[13]) ).
thf(52,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ~ $true
| ( ( inconsistency_P @ inconsistency_G @ A )
!= ( inconsistency_P @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[23,14]) ).
thf(53,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ( ( inconsistency_P @ inconsistency_G @ A )
!= ( inconsistency_P @ C @ B ) ) ),
inference(simp,[status(thm)],[52]) ).
thf(54,plain,
! [A: qML_i] :
~ ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ),
inference(pattern_uni,[status(thm)],[53:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( inconsistency_G ))]]) ).
thf(92,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( inconsistency_P @ incons1905966852QML_mu @ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( inconsistency_G @ C @ D )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[27,54]) ).
thf(93,plain,
! [B: qML_i,A: qML_i] :
( ( inconsistency_P @ incons1905966852QML_mu @ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( inconsistency_G @ C @ D )
@ B ) ),
inference(simp,[status(thm)],[92]) ).
thf(97,plain,
! [B: qML_i,A: qML_i] :
( ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( inconsistency_G @ C @ D ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[93]) ).
thf(100,plain,
( incons1905966852QML_mu
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( inconsistency_G @ A @ B ) ) ),
inference(simp,[status(thm)],[97]) ).
thf(119,plain,
( ( incons1905966852QML_mu @ sk5 @ sk6 )
!= ( ~ ( inconsistency_G @ sk5 @ sk6 ) ) ),
inference(func_ext,[status(esa)],[100]) ).
thf(136,plain,
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ~ ( inconsistency_G @ sk5 @ sk6 ) ),
inference(bool_ext,[status(thm)],[119]) ).
thf(138,plain,
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ~ ( inconsistency_G @ sk5 @ sk6 ) ),
inference(cnf,[status(esa)],[136]) ).
thf(10,axiom,
( incons1905966852QML_mu
= ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_7_NE__def) ).
thf(30,plain,
( incons1905966852QML_mu
= ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(31,plain,
( incons1905966852QML_mu
= ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ),
inference(lifteq,[status(thm)],[30]) ).
thf(82,plain,
! [A: qML_i] :
( ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ D @ B @ C )
=> ! [E: qML_i] :
( ( qML_r @ C @ E )
=> ? [F: qML_mu] : ( D @ F @ E ) ) )
@ A )
| ( incons1905966852QML_mu != incons1905966852QML_mu ) ),
inference(paramod_ordered,[status(thm)],[31,27]) ).
thf(83,plain,
! [A: qML_i] :
( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ D @ B @ C )
=> ! [E: qML_i] :
( ( qML_r @ C @ E )
=> ? [F: qML_mu] : ( D @ F @ E ) ) )
@ A ),
inference(pattern_uni,[status(thm)],[82:[]]) ).
thf(560,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ~ $true
| ( ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ F @ D @ E )
=> ! [G: qML_i] :
( ( qML_r @ E @ G )
=> ? [H: qML_mu] : ( F @ H @ G ) ) )
@ A )
!= ( inconsistency_P @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[83,14]) ).
thf(561,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ( ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ F @ D @ E )
=> ! [G: qML_i] :
( ( qML_r @ E @ G )
=> ? [H: qML_mu] : ( F @ H @ G ) ) )
@ A )
!= ( inconsistency_P @ C @ B ) ) ),
inference(simp,[status(thm)],[560]) ).
thf(562,plain,
! [A: qML_i] :
~ ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ! [D: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ D @ B @ C )
=> ! [E: qML_i] :
( ( qML_r @ C @ E )
=> ? [F: qML_mu] : ( D @ F @ E ) ) )
@ A ),
inference(pattern_uni,[status(thm)],[561:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( ^ [D: qML_mu] : ^ [E: qML_i] : ! [F: qML_mu > qML_i > $o] : ( ( incons1389517216QML_mu @ F @ D @ E ) => ! [G: qML_i] : ( ( qML_r @ E @ G ) => ? [H: qML_mu] : ( F @ H @ G ) ) ) ))]]) ).
thf(611,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( inconsistency_P @ incons1905966852QML_mu @ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
( ( qML_r @ D @ F )
=> ? [G: qML_mu] : ( E @ G @ F ) ) )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[27,562]) ).
thf(612,plain,
! [B: qML_i,A: qML_i] :
( ( inconsistency_P @ incons1905966852QML_mu @ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
( ( qML_r @ D @ F )
=> ? [G: qML_mu] : ( E @ G @ F ) ) )
@ B ) ),
inference(simp,[status(thm)],[611]) ).
thf(622,plain,
! [B: qML_i,A: qML_i] :
( ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
( ( qML_r @ D @ F )
=> ? [G: qML_mu] : ( E @ G @ F ) ) ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[612]) ).
thf(628,plain,
( incons1905966852QML_mu
!= ( ^ [A: qML_mu,B: qML_i] :
~ ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ),
inference(simp,[status(thm)],[622]) ).
thf(9,axiom,
( inconsistency_G
= ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_6_G__def) ).
thf(28,plain,
( inconsistency_G
= ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(29,plain,
( inconsistency_G
= ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
inference(lifteq,[status(thm)],[28]) ).
thf(35,plain,
! [B: qML_i,A: qML_mu] :
( ( inconsistency_G @ A @ B )
= ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
inference(func_ext,[status(esa)],[29]) ).
thf(47,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ~ $true
| ( ( inconsistency_P @ incons1905966852QML_mu @ A )
!= ( inconsistency_P @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[27,14]) ).
thf(48,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ( ( inconsistency_P @ incons1905966852QML_mu @ A )
!= ( inconsistency_P @ C @ B ) ) ),
inference(simp,[status(thm)],[47]) ).
thf(49,plain,
! [A: qML_i] :
~ ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ),
inference(pattern_uni,[status(thm)],[48:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( incons1905966852QML_mu ))]]) ).
thf(69,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( inconsistency_P @ inconsistency_G @ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( incons1905966852QML_mu @ C @ D )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[23,49]) ).
thf(70,plain,
! [B: qML_i,A: qML_i] :
( ( inconsistency_P @ inconsistency_G @ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( incons1905966852QML_mu @ C @ D )
@ B ) ),
inference(simp,[status(thm)],[69]) ).
thf(73,plain,
! [B: qML_i,A: qML_i] :
( ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( incons1905966852QML_mu @ C @ D ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[70]) ).
thf(76,plain,
( inconsistency_G
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( incons1905966852QML_mu @ A @ B ) ) ),
inference(simp,[status(thm)],[73]) ).
thf(87,plain,
( ( inconsistency_G @ sk3 @ sk4 )
!= ( ~ ( incons1905966852QML_mu @ sk3 @ sk4 ) ) ),
inference(func_ext,[status(esa)],[76]) ).
thf(933,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ~ ( incons1905966852QML_mu @ sk3 @ sk4 ) ) )
| ( ( inconsistency_G @ A @ B )
!= ( inconsistency_G @ sk3 @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[35,87]) ).
thf(934,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk4 )
=> ( A @ sk3 @ sk4 ) ) )
!= ( ~ ( incons1905966852QML_mu @ sk3 @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[933:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(1010,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk4 )
=> ( A @ sk3 @ sk4 ) )
| ~ ~ ( incons1905966852QML_mu @ sk3 @ sk4 ) ),
inference(bool_ext,[status(thm)],[934]) ).
thf(1033,plain,
( ( ( inconsistency_P @ sk67 @ sk4 )
| ( incons1905966852QML_mu @ sk3 @ sk4 ) )
& ( ~ ( sk67 @ sk3 @ sk4 )
| ( incons1905966852QML_mu @ sk3 @ sk4 ) ) ),
inference(cnf,[status(esa)],[1010]) ).
thf(1034,plain,
( ( inconsistency_P @ sk67 @ sk4 )
| ( incons1905966852QML_mu @ sk3 @ sk4 ) ),
inference(cnfConj,[status(thm)],[1033]) ).
thf(50,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ $true
| ~ ( inconsistency_P @ C @ B )
| ( ( inconsistency_P @ inconsistency_G @ A )
!= ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[23,14]) ).
thf(51,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P @ C @ B )
| ( ( inconsistency_P @ inconsistency_G @ A )
!= ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(simp,[status(thm)],[50]) ).
thf(60,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P @ C @ B )
| ( inconsistency_G
!= ( ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[51]) ).
thf(64,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( inconsistency_P @ B @ A )
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) ) ),
inference(simp,[status(thm)],[60]) ).
thf(2075,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ~ $true
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk67 @ sk4 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1034,64]) ).
thf(2076,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk67 @ sk4 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[2075]) ).
thf(2077,plain,
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( inconsistency_G
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( sk67 @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[2076:[bind(A,$thf( sk4 )),bind(B,$thf( sk67 ))]]) ).
thf(4,axiom,
! [A: qML_i,B: qML_mu > qML_i > $o] :
( ~ ( inconsistency_P @ B @ A )
=> ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_A1b) ).
thf(15,plain,
! [A: qML_i,B: qML_mu > qML_i > $o] :
( ~ ( inconsistency_P @ B @ A )
=> ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(16,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_P @ B @ A )
| ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A ) ),
inference(cnf,[status(esa)],[15]) ).
thf(114,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_P @ B @ A )
| ( ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A )
!= ( inconsistency_P @ B @ A ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[16]) ).
thf(115,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_P @ B @ A )
| ( ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[114]) ).
thf(78,plain,
! [B: qML_i,A: qML_mu] :
( ( incons1905966852QML_mu @ A @ B )
= ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ),
inference(func_ext,[status(esa)],[31]) ).
thf(36,plain,
! [A: qML_i] :
( ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( inconsistency_P @ D @ C )
=> ( D @ B @ C ) )
@ A )
| ( inconsistency_G != inconsistency_G ) ),
inference(paramod_ordered,[status(thm)],[29,23]) ).
thf(37,plain,
! [A: qML_i] :
( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( inconsistency_P @ D @ C )
=> ( D @ B @ C ) )
@ A ),
inference(pattern_uni,[status(thm)],[36:[]]) ).
thf(42,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ~ $true
| ( ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( inconsistency_P @ F @ E )
=> ( F @ D @ E ) )
@ A )
!= ( inconsistency_P @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[37,14]) ).
thf(43,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B )
| ( ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( inconsistency_P @ F @ E )
=> ( F @ D @ E ) )
@ A )
!= ( inconsistency_P @ C @ B ) ) ),
inference(simp,[status(thm)],[42]) ).
thf(44,plain,
! [A: qML_i] :
~ ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ! [D: qML_mu > qML_i > $o] :
( ( inconsistency_P @ D @ C )
=> ( D @ B @ C ) )
@ A ),
inference(pattern_uni,[status(thm)],[43:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( ^ [D: qML_mu] : ^ [E: qML_i] : ! [F: qML_mu > qML_i > $o] : ( ( inconsistency_P @ F @ E ) => ( F @ D @ E ) ) ))]]) ).
thf(171,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( inconsistency_P @ incons1905966852QML_mu @ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[27,44]) ).
thf(172,plain,
! [B: qML_i,A: qML_i] :
( ( inconsistency_P @ incons1905966852QML_mu @ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) )
@ B ) ),
inference(simp,[status(thm)],[171]) ).
thf(178,plain,
! [B: qML_i,A: qML_i] :
( ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[172]) ).
thf(181,plain,
( incons1905966852QML_mu
!= ( ^ [A: qML_mu,B: qML_i] :
~ ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
inference(simp,[status(thm)],[178]) ).
thf(185,plain,
( ( incons1905966852QML_mu @ sk13 @ sk14 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk14 )
=> ( A @ sk13 @ sk14 ) ) ) ),
inference(func_ext,[status(esa)],[181]) ).
thf(1442,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ~ ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ sk14 )
=> ( C @ sk13 @ sk14 ) ) ) )
| ( ( incons1905966852QML_mu @ A @ B )
!= ( incons1905966852QML_mu @ sk13 @ sk14 ) ) ),
inference(paramod_ordered,[status(thm)],[78,185]) ).
thf(1443,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk13 @ sk14 )
=> ! [B: qML_i] :
( ( qML_r @ sk14 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk14 )
=> ( A @ sk13 @ sk14 ) ) ) ),
inference(pattern_uni,[status(thm)],[1442:[bind(A,$thf( sk13 )),bind(B,$thf( sk14 ))]]) ).
thf(603,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( inconsistency_P @ inconsistency_G @ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
( ( qML_r @ D @ F )
=> ? [G: qML_mu] : ( E @ G @ F ) ) )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[23,562]) ).
thf(604,plain,
! [B: qML_i,A: qML_i] :
( ( inconsistency_P @ inconsistency_G @ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
( ( qML_r @ D @ F )
=> ? [G: qML_mu] : ( E @ G @ F ) ) )
@ B ) ),
inference(simp,[status(thm)],[603]) ).
thf(620,plain,
! [B: qML_i,A: qML_i] :
( ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
( ( qML_r @ D @ F )
=> ? [G: qML_mu] : ( E @ G @ F ) ) ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[604]) ).
thf(626,plain,
( inconsistency_G
!= ( ^ [A: qML_mu,B: qML_i] :
~ ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ),
inference(simp,[status(thm)],[620]) ).
thf(630,plain,
( ( inconsistency_G @ sk28 @ sk29 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk28 @ sk29 )
=> ! [B: qML_i] :
( ( qML_r @ sk29 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ),
inference(func_ext,[status(esa)],[626]) ).
thf(1460,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ( incons1905966852QML_mu @ A @ B ) )
!= ( inconsistency_G @ sk28 @ sk29 ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ sk28 @ sk29 )
=> ! [D: qML_i] :
( ( qML_r @ sk29 @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[78,630]) ).
thf(1461,plain,
( ( ~ ( incons1905966852QML_mu @ sk28 @ sk29 ) )
!= ( inconsistency_G @ sk28 @ sk29 ) ),
inference(pattern_uni,[status(thm)],[1460:[bind(A,$thf( sk28 )),bind(B,$thf( sk29 ))]]) ).
thf(1570,plain,
( ~ ( incons1905966852QML_mu @ sk28 @ sk29 )
| ( inconsistency_G @ sk28 @ sk29 ) ),
inference(bool_ext,[status(thm)],[1461]) ).
thf(1591,plain,
( ~ ( incons1905966852QML_mu @ sk28 @ sk29 )
| ( inconsistency_G @ sk28 @ sk29 ) ),
inference(cnf,[status(esa)],[1570]) ).
thf(169,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( inconsistency_P @ inconsistency_G @ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[23,44]) ).
thf(170,plain,
! [B: qML_i,A: qML_i] :
( ( inconsistency_P @ inconsistency_G @ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) )
@ B ) ),
inference(simp,[status(thm)],[169]) ).
thf(177,plain,
! [B: qML_i,A: qML_i] :
( ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[170]) ).
thf(180,plain,
( inconsistency_G
!= ( ^ [A: qML_mu,B: qML_i] :
~ ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
inference(simp,[status(thm)],[177]) ).
thf(182,plain,
( ( inconsistency_G @ sk11 @ sk12 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk12 )
=> ( A @ sk11 @ sk12 ) ) ) ),
inference(func_ext,[status(esa)],[180]) ).
thf(387,plain,
( ( inconsistency_G @ sk11 @ sk12 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk12 )
=> ( A @ sk11 @ sk12 ) ) ),
inference(bool_ext,[status(thm)],[182]) ).
thf(395,plain,
( ( ( inconsistency_G @ sk11 @ sk12 )
| ( inconsistency_P @ sk21 @ sk12 ) )
& ( ( inconsistency_G @ sk11 @ sk12 )
| ~ ( sk21 @ sk11 @ sk12 ) ) ),
inference(cnf,[status(esa)],[387]) ).
thf(396,plain,
( ( inconsistency_G @ sk11 @ sk12 )
| ( inconsistency_P @ sk21 @ sk12 ) ),
inference(cnfConj,[status(thm)],[395]) ).
thf(45,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ $true
| ~ ( inconsistency_P @ C @ B )
| ( ( inconsistency_P @ incons1905966852QML_mu @ A )
!= ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[27,14]) ).
thf(46,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P @ C @ B )
| ( ( inconsistency_P @ incons1905966852QML_mu @ A )
!= ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(simp,[status(thm)],[45]) ).
thf(56,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P @ C @ B )
| ( incons1905966852QML_mu
!= ( ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[46]) ).
thf(61,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( inconsistency_P @ B @ A )
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) ) ),
inference(simp,[status(thm)],[56]) ).
thf(1267,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_G @ sk11 @ sk12 )
| ~ $true
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk21 @ sk12 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[396,61]) ).
thf(1268,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_G @ sk11 @ sk12 )
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk21 @ sk12 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[1267]) ).
thf(1269,plain,
( ( inconsistency_G @ sk11 @ sk12 )
| ( incons1905966852QML_mu
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( sk21 @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1268:[bind(A,$thf( sk12 )),bind(B,$thf( sk21 ))]]) ).
thf(186,plain,
( ( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) ) )
| ( incons1905966852QML_mu != incons1905966852QML_mu ) ),
inference(paramod_ordered,[status(thm)],[31,181]) ).
thf(187,plain,
( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[186:[]]) ).
thf(422,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk23 @ sk24 )
=> ! [B: qML_i] :
( ( qML_r @ sk24 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk24 )
=> ( A @ sk23 @ sk24 ) ) ) ),
inference(func_ext,[status(esa)],[187]) ).
thf(1052,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ( inconsistency_G @ A @ B ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ sk23 @ sk24 )
=> ! [D: qML_i] :
( ( qML_r @ sk24 @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ sk24 )
=> ( C @ sk23 @ sk24 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[35,422]) ).
thf(1053,plain,
( ( ~ ( inconsistency_G @ sk23 @ sk24 ) )
!= ( ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk23 @ sk24 )
=> ! [B: qML_i] :
( ( qML_r @ sk24 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ),
inference(pattern_uni,[status(thm)],[1052:[bind(A,$thf( sk23 )),bind(B,$thf( sk24 ))]]) ).
thf(1485,plain,
! [B: qML_i,A: qML_mu] :
( ( ( incons1905966852QML_mu @ A @ B )
!= ( ~ ( inconsistency_G @ sk23 @ sk24 ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ sk23 @ sk24 )
=> ! [D: qML_i] :
( ( qML_r @ sk24 @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[78,1053]) ).
thf(1486,plain,
( ( incons1905966852QML_mu @ sk23 @ sk24 )
!= ( ~ ( inconsistency_G @ sk23 @ sk24 ) ) ),
inference(pattern_uni,[status(thm)],[1485:[bind(A,$thf( sk23 )),bind(B,$thf( sk24 ))]]) ).
thf(120,plain,
( ( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( inconsistency_G @ A @ B ) ) )
| ( incons1905966852QML_mu != incons1905966852QML_mu ) ),
inference(paramod_ordered,[status(thm)],[31,100]) ).
thf(121,plain,
( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( inconsistency_G @ A @ B ) ) ),
inference(pattern_uni,[status(thm)],[120:[]]) ).
thf(188,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk15 @ sk16 )
=> ! [B: qML_i] :
( ( qML_r @ sk16 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) )
!= ( ~ ( inconsistency_G @ sk15 @ sk16 ) ) ),
inference(func_ext,[status(esa)],[121]) ).
thf(1469,plain,
! [B: qML_i,A: qML_mu] :
( ( ( incons1905966852QML_mu @ A @ B )
!= ( ~ ( inconsistency_G @ sk15 @ sk16 ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ sk15 @ sk16 )
=> ! [D: qML_i] :
( ( qML_r @ sk16 @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[78,188]) ).
thf(1470,plain,
( ( incons1905966852QML_mu @ sk15 @ sk16 )
!= ( ~ ( inconsistency_G @ sk15 @ sk16 ) ) ),
inference(pattern_uni,[status(thm)],[1469:[bind(A,$thf( sk15 )),bind(B,$thf( sk16 ))]]) ).
thf(1594,plain,
( ~ ( incons1905966852QML_mu @ sk15 @ sk16 )
| ~ ~ ( inconsistency_G @ sk15 @ sk16 ) ),
inference(bool_ext,[status(thm)],[1470]) ).
thf(1608,plain,
( ~ ( incons1905966852QML_mu @ sk15 @ sk16 )
| ( inconsistency_G @ sk15 @ sk16 ) ),
inference(cnf,[status(esa)],[1594]) ).
thf(912,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ( inconsistency_G @ A @ B ) )
!= ( incons1905966852QML_mu @ sk13 @ sk14 ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ sk14 )
=> ( C @ sk13 @ sk14 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[35,185]) ).
thf(913,plain,
( ( incons1905966852QML_mu @ sk13 @ sk14 )
!= ( ~ ( inconsistency_G @ sk13 @ sk14 ) ) ),
inference(pattern_uni,[status(thm)],[912:[bind(A,$thf( sk13 )),bind(B,$thf( sk14 ))]]) ).
thf(65,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) )
@ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( incons1905966852QML_mu @ C @ D )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[37,49]) ).
thf(66,plain,
! [B: qML_i,A: qML_i] :
( ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) )
@ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( incons1905966852QML_mu @ C @ D )
@ B ) ),
inference(simp,[status(thm)],[65]) ).
thf(71,plain,
! [B: qML_i,A: qML_i] :
( ( ( ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) ) )
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( incons1905966852QML_mu @ C @ D ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[66]) ).
thf(74,plain,
( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( incons1905966852QML_mu @ A @ B ) ) ),
inference(simp,[status(thm)],[71]) ).
thf(122,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk8 )
=> ( A @ sk7 @ sk8 ) ) )
!= ( ~ ( incons1905966852QML_mu @ sk7 @ sk8 ) ) ),
inference(func_ext,[status(esa)],[74]) ).
thf(936,plain,
! [B: qML_i,A: qML_mu] :
( ( ( inconsistency_G @ A @ B )
!= ( ~ ( incons1905966852QML_mu @ sk7 @ sk8 ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ sk8 )
=> ( C @ sk7 @ sk8 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[35,122]) ).
thf(937,plain,
( ( inconsistency_G @ sk7 @ sk8 )
!= ( ~ ( incons1905966852QML_mu @ sk7 @ sk8 ) ) ),
inference(pattern_uni,[status(thm)],[936:[bind(A,$thf( sk7 )),bind(B,$thf( sk8 ))]]) ).
thf(1452,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( inconsistency_G @ sk7 @ sk8 ) )
| ( ( incons1905966852QML_mu @ A @ B )
!= ( incons1905966852QML_mu @ sk7 @ sk8 ) ) ),
inference(paramod_ordered,[status(thm)],[78,937]) ).
thf(1453,plain,
( ( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk7 @ sk8 )
=> ! [B: qML_i] :
( ( qML_r @ sk8 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) )
!= ( inconsistency_G @ sk7 @ sk8 ) ),
inference(pattern_uni,[status(thm)],[1452:[bind(A,$thf( sk7 )),bind(B,$thf( sk8 ))]]) ).
thf(1938,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk7 @ sk8 )
=> ! [B: qML_i] :
( ( qML_r @ sk8 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) )
| ( inconsistency_G @ sk7 @ sk8 ) ),
inference(bool_ext,[status(thm)],[1453]) ).
thf(1952,plain,
! [A: qML_mu] :
( ( ( incons1389517216QML_mu @ sk145 @ sk7 @ sk8 )
| ( inconsistency_G @ sk7 @ sk8 ) )
& ( ( qML_r @ sk8 @ sk146 )
| ( inconsistency_G @ sk7 @ sk8 ) )
& ( ~ ( sk145 @ A @ sk146 )
| ( inconsistency_G @ sk7 @ sk8 ) ) ),
inference(cnf,[status(esa)],[1938]) ).
thf(1954,plain,
( ( qML_r @ sk8 @ sk146 )
| ( inconsistency_G @ sk7 @ sk8 ) ),
inference(cnfConj,[status(thm)],[1952]) ).
thf(1352,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_G @ sk11 @ sk12 )
| ~ $true
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk21 @ sk12 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[396,64]) ).
thf(1353,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_G @ sk11 @ sk12 )
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk21 @ sk12 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[1352]) ).
thf(1354,plain,
( ( inconsistency_G @ sk11 @ sk12 )
| ( inconsistency_G
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( sk21 @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1353:[bind(A,$thf( sk12 )),bind(B,$thf( sk21 ))]]) ).
thf(656,plain,
! [A: qML_i] :
( ( inconsistency_G @ sk11 @ sk12 )
| ~ $true
| ( ( inconsistency_P @ sk21 @ sk12 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[396,54]) ).
thf(657,plain,
! [A: qML_i] :
( ( inconsistency_G @ sk11 @ sk12 )
| ( ( inconsistency_P @ sk21 @ sk12 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ) ) ),
inference(simp,[status(thm)],[656]) ).
thf(663,plain,
! [A: qML_i] :
( ( inconsistency_G @ sk11 @ sk12 )
| ( sk21
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C ) ) )
| ( sk12 != A ) ),
inference(simp,[status(thm)],[657]) ).
thf(670,plain,
( ( inconsistency_G @ sk11 @ sk12 )
| ( sk21
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( inconsistency_G @ A @ B ) ) ) ),
inference(simp,[status(thm)],[663]) ).
thf(762,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk15 @ sk16 )
=> ! [B: qML_i] :
( ( qML_r @ sk16 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) )
| ~ ~ ( inconsistency_G @ sk15 @ sk16 ) ),
inference(bool_ext,[status(thm)],[188]) ).
thf(780,plain,
! [A: qML_mu] :
( ( ( incons1389517216QML_mu @ sk41 @ sk15 @ sk16 )
| ( inconsistency_G @ sk15 @ sk16 ) )
& ( ( qML_r @ sk16 @ sk42 )
| ( inconsistency_G @ sk15 @ sk16 ) )
& ( ~ ( sk41 @ A @ sk42 )
| ( inconsistency_G @ sk15 @ sk16 ) ) ),
inference(cnf,[status(esa)],[762]) ).
thf(782,plain,
( ( qML_r @ sk16 @ sk42 )
| ( inconsistency_G @ sk15 @ sk16 ) ),
inference(cnfConj,[status(thm)],[780]) ).
thf(1440,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ~ ( inconsistency_G @ sk13 @ sk14 ) ) )
| ( ( incons1905966852QML_mu @ A @ B )
!= ( incons1905966852QML_mu @ sk13 @ sk14 ) ) ),
inference(paramod_ordered,[status(thm)],[78,913]) ).
thf(1441,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk13 @ sk14 )
=> ! [B: qML_i] :
( ( qML_r @ sk14 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) )
!= ( ~ ( inconsistency_G @ sk13 @ sk14 ) ) ),
inference(pattern_uni,[status(thm)],[1440:[bind(A,$thf( sk13 )),bind(B,$thf( sk14 ))]]) ).
thf(401,plain,
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk14 )
=> ( A @ sk13 @ sk14 ) ) ),
inference(bool_ext,[status(thm)],[185]) ).
thf(415,plain,
( ( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ( inconsistency_P @ sk22 @ sk14 ) )
& ( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ~ ( sk22 @ sk13 @ sk14 ) ) ),
inference(cnf,[status(esa)],[401]) ).
thf(417,plain,
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ~ ( sk22 @ sk13 @ sk14 ) ),
inference(cnfConj,[status(thm)],[415]) ).
thf(7,axiom,
! [A: qML_i,B: qML_mu > qML_i > $o] :
( ( inconsistency_P @ B @ A )
=> ! [C: qML_i] :
( ( qML_r @ A @ C )
=> ( inconsistency_P @ B @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4_A4) ).
thf(24,plain,
! [A: qML_i,B: qML_mu > qML_i > $o] :
( ( inconsistency_P @ B @ A )
=> ! [C: qML_i] :
( ( qML_r @ A @ C )
=> ( inconsistency_P @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(132,plain,
( ( inconsistency_G @ sk3 @ sk4 )
| ~ ( incons1905966852QML_mu @ sk3 @ sk4 ) ),
inference(bool_ext,[status(thm)],[87]) ).
thf(134,plain,
( ( inconsistency_G @ sk3 @ sk4 )
| ~ ( incons1905966852QML_mu @ sk3 @ sk4 ) ),
inference(cnf,[status(esa)],[132]) ).
thf(1471,plain,
! [B: qML_i,A: qML_mu] :
( ( inconsistency_G @ sk3 @ sk4 )
| ~ ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) )
| ( ( incons1905966852QML_mu @ A @ B )
!= ( incons1905966852QML_mu @ sk3 @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[78,134]) ).
thf(1472,plain,
( ( inconsistency_G @ sk3 @ sk4 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk3 @ sk4 )
=> ! [B: qML_i] :
( ( qML_r @ sk4 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1471:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(1516,plain,
! [A: qML_mu] :
( ( ( inconsistency_G @ sk3 @ sk4 )
| ( incons1389517216QML_mu @ sk110 @ sk3 @ sk4 ) )
& ( ( inconsistency_G @ sk3 @ sk4 )
| ( qML_r @ sk4 @ sk111 ) )
& ( ( inconsistency_G @ sk3 @ sk4 )
| ~ ( sk110 @ A @ sk111 ) ) ),
inference(cnf,[status(esa)],[1472]) ).
thf(1518,plain,
( ( inconsistency_G @ sk3 @ sk4 )
| ( qML_r @ sk4 @ sk111 ) ),
inference(cnfConj,[status(thm)],[1516]) ).
thf(925,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ sk15 @ sk16 )
=> ! [D: qML_i] :
( ( qML_r @ sk16 @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) )
| ( ( inconsistency_G @ A @ B )
!= ( inconsistency_G @ sk15 @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[35,188]) ).
thf(926,plain,
( ( ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk16 )
=> ( A @ sk15 @ sk16 ) ) )
!= ( ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk15 @ sk16 )
=> ! [B: qML_i] :
( ( qML_r @ sk16 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ),
inference(pattern_uni,[status(thm)],[925:[bind(A,$thf( sk15 )),bind(B,$thf( sk16 ))]]) ).
thf(1481,plain,
! [B: qML_i,A: qML_mu] :
( ( ( incons1905966852QML_mu @ A @ B )
!= ( ~ ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ sk16 )
=> ( C @ sk15 @ sk16 ) ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ sk15 @ sk16 )
=> ! [D: qML_i] :
( ( qML_r @ sk16 @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[78,926]) ).
thf(1482,plain,
( ( incons1905966852QML_mu @ sk15 @ sk16 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk16 )
=> ( A @ sk15 @ sk16 ) ) ) ),
inference(pattern_uni,[status(thm)],[1481:[bind(A,$thf( sk15 )),bind(B,$thf( sk16 ))]]) ).
thf(25,plain,
! [C: qML_i,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( inconsistency_P @ B @ A )
| ~ ( qML_r @ A @ C )
| ( inconsistency_P @ B @ C ) ),
inference(cnf,[status(esa)],[24]) ).
thf(579,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
( ( qML_r @ D @ F )
=> ? [G: qML_mu] : ( E @ G @ F ) ) )
@ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( incons1905966852QML_mu @ C @ D )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[83,49]) ).
thf(580,plain,
! [B: qML_i,A: qML_i] :
( ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
( ( qML_r @ D @ F )
=> ? [G: qML_mu] : ( E @ G @ F ) ) )
@ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( incons1905966852QML_mu @ C @ D )
@ B ) ),
inference(simp,[status(thm)],[579]) ).
thf(586,plain,
! [B: qML_i,A: qML_i] :
( ( ( ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
( ( qML_r @ D @ F )
=> ? [G: qML_mu] : ( E @ G @ F ) ) ) )
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( incons1905966852QML_mu @ C @ D ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[580]) ).
thf(593,plain,
( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( incons1905966852QML_mu @ A @ B ) ) ),
inference(simp,[status(thm)],[586]) ).
thf(596,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk26 @ sk27 )
=> ! [B: qML_i] :
( ( qML_r @ sk27 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) )
!= ( ~ ( incons1905966852QML_mu @ sk26 @ sk27 ) ) ),
inference(func_ext,[status(esa)],[593]) ).
thf(785,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk26 @ sk27 )
=> ! [B: qML_i] :
( ( qML_r @ sk27 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) )
| ~ ~ ( incons1905966852QML_mu @ sk26 @ sk27 ) ),
inference(bool_ext,[status(thm)],[596]) ).
thf(800,plain,
! [A: qML_mu] :
( ( ( incons1389517216QML_mu @ sk44 @ sk26 @ sk27 )
| ( incons1905966852QML_mu @ sk26 @ sk27 ) )
& ( ( qML_r @ sk27 @ sk45 )
| ( incons1905966852QML_mu @ sk26 @ sk27 ) )
& ( ~ ( sk44 @ A @ sk45 )
| ( incons1905966852QML_mu @ sk26 @ sk27 ) ) ),
inference(cnf,[status(esa)],[785]) ).
thf(802,plain,
( ( qML_r @ sk27 @ sk45 )
| ( incons1905966852QML_mu @ sk26 @ sk27 ) ),
inference(cnfConj,[status(thm)],[800]) ).
thf(1492,plain,
! [B: qML_i,A: qML_mu] :
( ( ( incons1905966852QML_mu @ A @ B )
!= ( ~ ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ sk24 )
=> ( C @ sk23 @ sk24 ) ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ sk23 @ sk24 )
=> ! [D: qML_i] :
( ( qML_r @ sk24 @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[78,422]) ).
thf(1493,plain,
( ( incons1905966852QML_mu @ sk23 @ sk24 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk24 )
=> ( A @ sk23 @ sk24 ) ) ) ),
inference(pattern_uni,[status(thm)],[1492:[bind(A,$thf( sk23 )),bind(B,$thf( sk24 ))]]) ).
thf(1803,plain,
( ( incons1905966852QML_mu @ sk23 @ sk24 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk24 )
=> ( A @ sk23 @ sk24 ) ) ),
inference(bool_ext,[status(thm)],[1493]) ).
thf(1824,plain,
( ( ( incons1905966852QML_mu @ sk23 @ sk24 )
| ( inconsistency_P @ sk135 @ sk24 ) )
& ( ( incons1905966852QML_mu @ sk23 @ sk24 )
| ~ ( sk135 @ sk23 @ sk24 ) ) ),
inference(cnf,[status(esa)],[1803]) ).
thf(1826,plain,
( ( incons1905966852QML_mu @ sk23 @ sk24 )
| ~ ( sk135 @ sk23 @ sk24 ) ),
inference(cnfConj,[status(thm)],[1824]) ).
thf(5,axiom,
! [A: qML_i,B: qML_mu > qML_i > $o,C: qML_mu > qML_i > $o] :
( ( ( inconsistency_P @ B @ A )
& ! [D: qML_i] :
( ( qML_r @ A @ D )
=> ! [E: qML_mu] :
( ( B @ E @ D )
=> ( C @ E @ D ) ) ) )
=> ( inconsistency_P @ C @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_A2) ).
thf(17,plain,
! [A: qML_i,B: qML_mu > qML_i > $o,C: qML_mu > qML_i > $o] :
( ( ( inconsistency_P @ B @ A )
& ! [D: qML_i] :
( ( qML_r @ A @ D )
=> ! [E: qML_mu] :
( ( B @ E @ D )
=> ( C @ E @ D ) ) ) )
=> ( inconsistency_P @ C @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(18,plain,
! [C: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,A: qML_i] :
( ( ~ ( inconsistency_P @ B @ A )
| ( qML_r @ A @ ( sk1 @ C @ B @ A ) )
| ( inconsistency_P @ C @ A ) )
& ( ~ ( inconsistency_P @ B @ A )
| ( B @ ( sk2 @ C @ B @ A ) @ ( sk1 @ C @ B @ A ) )
| ( inconsistency_P @ C @ A ) )
& ( ~ ( inconsistency_P @ B @ A )
| ~ ( C @ ( sk2 @ C @ B @ A ) @ ( sk1 @ C @ B @ A ) )
| ( inconsistency_P @ C @ A ) ) ),
inference(cnf,[status(esa)],[17]) ).
thf(20,plain,
! [C: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( inconsistency_P @ B @ A )
| ( B @ ( sk2 @ C @ B @ A ) @ ( sk1 @ C @ B @ A ) )
| ( inconsistency_P @ C @ A ) ),
inference(cnfConj,[status(thm)],[18]) ).
thf(416,plain,
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ( inconsistency_P @ sk22 @ sk14 ) ),
inference(cnfConj,[status(thm)],[415]) ).
thf(920,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ~ ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ sk28 @ sk29 )
=> ! [D: qML_i] :
( ( qML_r @ sk29 @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) )
| ( ( inconsistency_G @ A @ B )
!= ( inconsistency_G @ sk28 @ sk29 ) ) ),
inference(paramod_ordered,[status(thm)],[35,630]) ).
thf(921,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk29 )
=> ( A @ sk28 @ sk29 ) ) )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk28 @ sk29 )
=> ! [B: qML_i] :
( ( qML_r @ sk29 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ),
inference(pattern_uni,[status(thm)],[920:[bind(A,$thf( sk28 )),bind(B,$thf( sk29 ))]]) ).
thf(1478,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ( incons1905966852QML_mu @ A @ B ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ sk29 )
=> ( C @ sk28 @ sk29 ) ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ sk28 @ sk29 )
=> ! [D: qML_i] :
( ( qML_r @ sk29 @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[78,921]) ).
thf(1479,plain,
( ( ~ ( incons1905966852QML_mu @ sk28 @ sk29 ) )
!= ( ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk29 )
=> ( A @ sk28 @ sk29 ) ) ) ),
inference(pattern_uni,[status(thm)],[1478:[bind(A,$thf( sk28 )),bind(B,$thf( sk29 ))]]) ).
thf(1595,plain,
( ( incons1905966852QML_mu @ sk15 @ sk16 )
| ~ ( inconsistency_G @ sk15 @ sk16 ) ),
inference(bool_ext,[status(thm)],[1470]) ).
thf(1609,plain,
( ( incons1905966852QML_mu @ sk15 @ sk16 )
| ~ ( inconsistency_G @ sk15 @ sk16 ) ),
inference(cnf,[status(esa)],[1595]) ).
thf(1488,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( inconsistency_G @ sk3 @ sk4 ) )
| ( ( incons1905966852QML_mu @ A @ B )
!= ( incons1905966852QML_mu @ sk3 @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[78,87]) ).
thf(1489,plain,
( ( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk3 @ sk4 )
=> ! [B: qML_i] :
( ( qML_r @ sk4 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) )
!= ( inconsistency_G @ sk3 @ sk4 ) ),
inference(pattern_uni,[status(thm)],[1488:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(19,plain,
! [C: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( inconsistency_P @ B @ A )
| ( qML_r @ A @ ( sk1 @ C @ B @ A ) )
| ( inconsistency_P @ C @ A ) ),
inference(cnfConj,[status(thm)],[18]) ).
thf(151,plain,
! [D: qML_mu > qML_i > $o,C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ $true
| ( qML_r @ B @ ( sk1 @ D @ C @ B ) )
| ( inconsistency_P @ D @ B )
| ( ( inconsistency_P
@ ^ [E: qML_mu,F: qML_i] :
! [G: qML_mu > qML_i > $o] :
( ( inconsistency_P @ G @ F )
=> ( G @ E @ F ) )
@ A )
!= ( inconsistency_P @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[37,19]) ).
thf(152,plain,
! [D: qML_mu > qML_i > $o,C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ( qML_r @ B @ ( sk1 @ D @ C @ B ) )
| ( inconsistency_P @ D @ B )
| ( ( inconsistency_P
@ ^ [E: qML_mu,F: qML_i] :
! [G: qML_mu > qML_i > $o] :
( ( inconsistency_P @ G @ F )
=> ( G @ E @ F ) )
@ A )
!= ( inconsistency_P @ C @ B ) ) ),
inference(simp,[status(thm)],[151]) ).
thf(153,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( qML_r @ A
@ ( sk1 @ B
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) )
@ A ) )
| ( inconsistency_P @ B @ A ) ),
inference(pattern_uni,[status(thm)],[152:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( ^ [E: qML_mu] : ^ [F: qML_i] : ! [G: qML_mu > qML_i > $o] : ( ( inconsistency_P @ G @ F ) => ( G @ E @ F ) ) )),bind(D,$thf( D ))]]) ).
thf(164,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( qML_r @ A
@ ( sk1 @ B
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) )
@ A ) )
| ( inconsistency_P @ B @ A ) ),
inference(simp,[status(thm)],[153]) ).
thf(910,plain,
! [B: qML_i,A: qML_mu] :
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ~ ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) )
| ( ( inconsistency_G @ A @ B )
!= ( inconsistency_G @ sk5 @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[35,138]) ).
thf(911,plain,
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk6 )
=> ( A @ sk5 @ sk6 ) ) ),
inference(pattern_uni,[status(thm)],[910:[bind(A,$thf( sk5 )),bind(B,$thf( sk6 ))]]) ).
thf(958,plain,
( ( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ( inconsistency_P @ sk63 @ sk6 ) )
& ( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ~ ( sk63 @ sk5 @ sk6 ) ) ),
inference(cnf,[status(esa)],[911]) ).
thf(959,plain,
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ( inconsistency_P @ sk63 @ sk6 ) ),
inference(cnfConj,[status(thm)],[958]) ).
thf(1688,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ~ $true
| ( ( inconsistency_P @ sk63 @ sk6 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[959,49]) ).
thf(1689,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ( ( inconsistency_P @ sk63 @ sk6 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ) ) ),
inference(simp,[status(thm)],[1688]) ).
thf(1705,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ( sk63
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C ) ) )
| ( sk6 != A ) ),
inference(simp,[status(thm)],[1689]) ).
thf(1714,plain,
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ( sk63
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( incons1905966852QML_mu @ A @ B ) ) ) ),
inference(simp,[status(thm)],[1705]) ).
thf(81,plain,
( ( incons1905966852QML_mu = inconsistency_G )
| ( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,31]) ).
thf(84,plain,
( ( incons1905966852QML_mu = inconsistency_G )
| ( ( ^ [A: qML_mu,B: qML_i,C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ^ [A: qML_mu,B: qML_i,C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ) ),
inference(simp,[status(thm)],[81]) ).
thf(397,plain,
( ( inconsistency_G @ sk11 @ sk12 )
| ~ ( sk21 @ sk11 @ sk12 ) ),
inference(cnfConj,[status(thm)],[395]) ).
thf(131,plain,
( ~ ( inconsistency_G @ sk3 @ sk4 )
| ~ ~ ( incons1905966852QML_mu @ sk3 @ sk4 ) ),
inference(bool_ext,[status(thm)],[87]) ).
thf(133,plain,
( ~ ( inconsistency_G @ sk3 @ sk4 )
| ( incons1905966852QML_mu @ sk3 @ sk4 ) ),
inference(cnf,[status(esa)],[131]) ).
thf(918,plain,
! [B: qML_i,A: qML_mu] :
( ~ ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) )
| ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( ( inconsistency_G @ A @ B )
!= ( inconsistency_G @ sk3 @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[35,133]) ).
thf(919,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk4 )
=> ( A @ sk3 @ sk4 ) )
| ( incons1905966852QML_mu @ sk3 @ sk4 ) ),
inference(pattern_uni,[status(thm)],[918:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(970,plain,
( ( ( inconsistency_P @ sk65 @ sk4 )
| ( incons1905966852QML_mu @ sk3 @ sk4 ) )
& ( ~ ( sk65 @ sk3 @ sk4 )
| ( incons1905966852QML_mu @ sk3 @ sk4 ) ) ),
inference(cnf,[status(esa)],[919]) ).
thf(971,plain,
( ( inconsistency_P @ sk65 @ sk4 )
| ( incons1905966852QML_mu @ sk3 @ sk4 ) ),
inference(cnfConj,[status(thm)],[970]) ).
thf(1856,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ~ $true
| ( ( inconsistency_P @ sk65 @ sk4 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[971,54]) ).
thf(1857,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( ( inconsistency_P @ sk65 @ sk4 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ) ) ),
inference(simp,[status(thm)],[1856]) ).
thf(1876,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( sk65
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C ) ) )
| ( sk4 != A ) ),
inference(simp,[status(thm)],[1857]) ).
thf(1886,plain,
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( sk65
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( inconsistency_G @ A @ B ) ) ) ),
inference(simp,[status(thm)],[1876]) ).
thf(90,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) )
@ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( inconsistency_G @ C @ D )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[37,54]) ).
thf(91,plain,
! [B: qML_i,A: qML_i] :
( ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) )
@ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( inconsistency_G @ C @ D )
@ B ) ),
inference(simp,[status(thm)],[90]) ).
thf(96,plain,
! [B: qML_i,A: qML_i] :
( ( ( ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) ) )
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( inconsistency_G @ C @ D ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[91]) ).
thf(99,plain,
( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( inconsistency_G @ A @ B ) ) ),
inference(simp,[status(thm)],[96]) ).
thf(126,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk10 )
=> ( A @ sk9 @ sk10 ) ) )
!= ( ~ ( inconsistency_G @ sk9 @ sk10 ) ) ),
inference(func_ext,[status(esa)],[99]) ).
thf(202,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk10 )
=> ( A @ sk9 @ sk10 ) )
| ~ ~ ( inconsistency_G @ sk9 @ sk10 ) ),
inference(bool_ext,[status(thm)],[126]) ).
thf(204,plain,
( ( ( inconsistency_P @ sk18 @ sk10 )
| ( inconsistency_G @ sk9 @ sk10 ) )
& ( ~ ( sk18 @ sk9 @ sk10 )
| ( inconsistency_G @ sk9 @ sk10 ) ) ),
inference(cnf,[status(esa)],[202]) ).
thf(205,plain,
( ( inconsistency_P @ sk18 @ sk10 )
| ( inconsistency_G @ sk9 @ sk10 ) ),
inference(cnfConj,[status(thm)],[204]) ).
thf(440,plain,
! [A: qML_i] :
( ( inconsistency_G @ sk9 @ sk10 )
| ~ $true
| ( ( inconsistency_P @ sk18 @ sk10 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[205,54]) ).
thf(441,plain,
! [A: qML_i] :
( ( inconsistency_G @ sk9 @ sk10 )
| ( ( inconsistency_P @ sk18 @ sk10 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ) ) ),
inference(simp,[status(thm)],[440]) ).
thf(447,plain,
! [A: qML_i] :
( ( inconsistency_G @ sk9 @ sk10 )
| ( sk18
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C ) ) )
| ( sk10 != A ) ),
inference(simp,[status(thm)],[441]) ).
thf(453,plain,
( ( inconsistency_G @ sk9 @ sk10 )
| ( sk18
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( inconsistency_G @ A @ B ) ) ) ),
inference(simp,[status(thm)],[447]) ).
thf(206,plain,
( ~ ( sk18 @ sk9 @ sk10 )
| ( inconsistency_G @ sk9 @ sk10 ) ),
inference(cnfConj,[status(thm)],[204]) ).
thf(142,plain,
( ~ ( inconsistency_G @ sk3 @ sk4 )
| ~ ~ ( inconsistency_G @ sk5 @ sk6 )
| ( ( incons1905966852QML_mu @ sk5 @ sk6 )
!= ( incons1905966852QML_mu @ sk3 @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[133,119]) ).
thf(143,plain,
( ~ ( inconsistency_G @ sk3 @ sk4 )
| ( inconsistency_G @ sk5 @ sk6 )
| ( ( incons1905966852QML_mu @ sk5 @ sk6 )
!= ( incons1905966852QML_mu @ sk3 @ sk4 ) ) ),
inference(simp,[status(thm)],[142]) ).
thf(147,plain,
( ( inconsistency_G @ sk5 @ sk6 )
| ~ ( inconsistency_G @ sk3 @ sk4 )
| ( sk5 != sk3 )
| ( sk6 != sk4 ) ),
inference(simp,[status(thm)],[143]) ).
thf(1841,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ~ $true
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk65 @ sk4 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[971,61]) ).
thf(1842,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk65 @ sk4 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[1841]) ).
thf(1843,plain,
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( incons1905966852QML_mu
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( sk65 @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1842:[bind(A,$thf( sk4 )),bind(B,$thf( sk65 ))]]) ).
thf(11,axiom,
( incons1389517216QML_mu
= ( ^ [A: qML_mu > qML_i > $o,B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i] :
( ( qML_r @ C @ E )
=> ! [F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_8_ess__def) ).
thf(32,plain,
( incons1389517216QML_mu
= ( ^ [A: qML_mu > qML_i > $o,B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i] :
( ( qML_r @ C @ E )
=> ! [F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(33,plain,
( incons1389517216QML_mu
= ( ^ [A: qML_mu > qML_i > $o,B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i] :
( ( qML_r @ C @ E )
=> ! [F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) ) ),
inference(lifteq,[status(thm)],[32]) ).
thf(139,plain,
! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A )
= ( ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i] :
( ( qML_r @ C @ E )
=> ! [F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) ) ),
inference(func_ext,[status(esa)],[33]) ).
thf(1188,plain,
! [A: qML_mu > qML_i > $o] :
( ( ( incons1389517216QML_mu @ A )
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C ) ) )
| ( ( ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i] :
( ( qML_r @ C @ E )
=> ! [F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) )
!= ( ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( inconsistency_P @ D @ C )
=> ( D @ B @ C ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,74]) ).
thf(1206,plain,
! [A: qML_mu > qML_i > $o] :
( ( ( incons1389517216QML_mu @ A )
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C ) ) )
| ( ( ^ [B: qML_mu,C: qML_i,D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i] :
( ( qML_r @ C @ E )
=> ! [F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) )
!= ( ^ [B: qML_mu,C: qML_i,D: qML_mu > qML_i > $o] :
( ( inconsistency_P @ D @ C )
=> ( D @ B @ C ) ) ) ) ),
inference(simp,[status(thm)],[1188]) ).
thf(605,plain,
! [B: qML_i,A: qML_i] :
( ~ $true
| ( ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) )
@ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
( ( qML_r @ D @ F )
=> ? [G: qML_mu] : ( E @ G @ F ) ) )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[37,562]) ).
thf(606,plain,
! [B: qML_i,A: qML_i] :
( ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) )
@ A )
!= ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
( ( qML_r @ D @ F )
=> ? [G: qML_mu] : ( E @ G @ F ) ) )
@ B ) ),
inference(simp,[status(thm)],[605]) ).
thf(618,plain,
! [B: qML_i,A: qML_i] :
( ( ( ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) ) )
!= ( ^ [C: qML_mu,D: qML_i] :
~ ! [E: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
( ( qML_r @ D @ F )
=> ? [G: qML_mu] : ( E @ G @ F ) ) ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[606]) ).
thf(624,plain,
( ( ^ [A: qML_mu,B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ^ [A: qML_mu,B: qML_i] :
~ ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ),
inference(simp,[status(thm)],[618]) ).
thf(757,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk37 )
=> ( A @ sk36 @ sk37 ) ) )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk36 @ sk37 )
=> ! [B: qML_i] :
( ( qML_r @ sk37 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ),
inference(func_ext,[status(esa)],[624]) ).
thf(1216,plain,
! [B: qML_i,A: qML_mu] :
( ( ( inconsistency_G @ A @ B )
!= ( ~ ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ sk36 @ sk37 )
=> ! [D: qML_i] :
( ( qML_r @ sk37 @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ sk37 )
=> ( C @ sk36 @ sk37 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[35,757]) ).
thf(1217,plain,
( ( inconsistency_G @ sk36 @ sk37 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk36 @ sk37 )
=> ! [B: qML_i] :
( ( qML_r @ sk37 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ),
inference(pattern_uni,[status(thm)],[1216:[bind(A,$thf( sk36 )),bind(B,$thf( sk37 ))]]) ).
thf(154,plain,
! [D: qML_mu > qML_i > $o,C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ $true
| ( qML_r @ B @ ( sk1 @ D @ C @ B ) )
| ( inconsistency_P @ D @ B )
| ( ( inconsistency_P @ incons1905966852QML_mu @ A )
!= ( inconsistency_P @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[27,19]) ).
thf(155,plain,
! [D: qML_mu > qML_i > $o,C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ( qML_r @ B @ ( sk1 @ D @ C @ B ) )
| ( inconsistency_P @ D @ B )
| ( ( inconsistency_P @ incons1905966852QML_mu @ A )
!= ( inconsistency_P @ C @ B ) ) ),
inference(simp,[status(thm)],[154]) ).
thf(156,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( qML_r @ A @ ( sk1 @ B @ incons1905966852QML_mu @ A ) )
| ( inconsistency_P @ B @ A ) ),
inference(pattern_uni,[status(thm)],[155:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( incons1905966852QML_mu )),bind(D,$thf( D ))]]) ).
thf(165,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( qML_r @ A @ ( sk1 @ B @ incons1905966852QML_mu @ A ) )
| ( inconsistency_P @ B @ A ) ),
inference(simp,[status(thm)],[156]) ).
thf(21,plain,
! [C: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( inconsistency_P @ B @ A )
| ~ ( C @ ( sk2 @ C @ B @ A ) @ ( sk1 @ C @ B @ A ) )
| ( inconsistency_P @ C @ A ) ),
inference(cnfConj,[status(thm)],[18]) ).
thf(135,plain,
( ~ ( incons1905966852QML_mu @ sk5 @ sk6 )
| ~ ~ ( inconsistency_G @ sk5 @ sk6 ) ),
inference(bool_ext,[status(thm)],[119]) ).
thf(137,plain,
( ~ ( incons1905966852QML_mu @ sk5 @ sk6 )
| ( inconsistency_G @ sk5 @ sk6 ) ),
inference(cnf,[status(esa)],[135]) ).
thf(633,plain,
( ( incons1905966852QML_mu @ sk30 @ sk31 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk30 @ sk31 )
=> ! [B: qML_i] :
( ( qML_r @ sk31 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ),
inference(func_ext,[status(esa)],[628]) ).
thf(832,plain,
( ( incons1905966852QML_mu @ sk30 @ sk31 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk30 @ sk31 )
=> ! [B: qML_i] :
( ( qML_r @ sk31 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ),
inference(bool_ext,[status(thm)],[633]) ).
thf(845,plain,
! [A: qML_mu] :
( ( ( incons1905966852QML_mu @ sk30 @ sk31 )
| ( incons1389517216QML_mu @ sk56 @ sk30 @ sk31 ) )
& ( ( incons1905966852QML_mu @ sk30 @ sk31 )
| ( qML_r @ sk31 @ sk57 ) )
& ( ( incons1905966852QML_mu @ sk30 @ sk31 )
| ~ ( sk56 @ A @ sk57 ) ) ),
inference(cnf,[status(esa)],[832]) ).
thf(847,plain,
( ( incons1905966852QML_mu @ sk30 @ sk31 )
| ( qML_r @ sk31 @ sk57 ) ),
inference(cnfConj,[status(thm)],[845]) ).
thf(1610,plain,
( ~ ( incons1905966852QML_mu @ sk23 @ sk24 )
| ~ ~ ( inconsistency_G @ sk23 @ sk24 ) ),
inference(bool_ext,[status(thm)],[1486]) ).
thf(1624,plain,
( ~ ( incons1905966852QML_mu @ sk23 @ sk24 )
| ( inconsistency_G @ sk23 @ sk24 ) ),
inference(cnf,[status(esa)],[1610]) ).
thf(879,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ~ $true
| ( ( inconsistency_P @ sk22 @ sk14 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[416,49]) ).
thf(880,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ( ( inconsistency_P @ sk22 @ sk14 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ) ) ),
inference(simp,[status(thm)],[879]) ).
thf(882,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ( sk22
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C ) ) )
| ( sk14 != A ) ),
inference(simp,[status(thm)],[880]) ).
thf(889,plain,
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ( sk22
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( incons1905966852QML_mu @ A @ B ) ) ) ),
inference(simp,[status(thm)],[882]) ).
thf(4063,plain,
! [A: qML_mu > qML_i > $o] :
( ( ( incons1389517216QML_mu @ A )
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C ) ) )
| ( ( ^ [B: qML_mu,C: qML_i,D: qML_mu > qML_i > $o] : ( D @ B @ C ) )
!= ( ^ [B: qML_mu,C: qML_i,D: qML_mu > qML_i > $o] : ( inconsistency_P @ D @ C ) ) )
| ( ( ^ [B: qML_mu,C: qML_i,D: qML_mu > qML_i > $o] :
! [E: qML_i] :
( ( qML_r @ C @ E )
=> ! [F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) )
!= ( ^ [B: qML_mu,C: qML_i,D: qML_mu > qML_i > $o] : ( D @ B @ C ) ) ) ),
inference(simp,[status(thm)],[1206]) ).
thf(1849,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ~ $true
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk65 @ sk4 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[971,64]) ).
thf(1850,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk65 @ sk4 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[1849]) ).
thf(1851,plain,
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( inconsistency_G
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( sk65 @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1850:[bind(A,$thf( sk4 )),bind(B,$thf( sk65 ))]]) ).
thf(987,plain,
( ~ ( inconsistency_G @ sk7 @ sk8 )
| ~ ~ ( incons1905966852QML_mu @ sk7 @ sk8 ) ),
inference(bool_ext,[status(thm)],[937]) ).
thf(1006,plain,
( ~ ( inconsistency_G @ sk7 @ sk8 )
| ( incons1905966852QML_mu @ sk7 @ sk8 ) ),
inference(cnf,[status(esa)],[987]) ).
thf(141,plain,
! [C: qML_i,B: qML_mu,A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ B @ C )
= ( ! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i] :
( ( qML_r @ C @ E )
=> ! [F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) ) ),
inference(func_ext,[status(esa)],[33]) ).
thf(1458,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ( incons1905966852QML_mu @ A @ B ) )
!= ( inconsistency_G @ sk36 @ sk37 ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ sk36 @ sk37 )
=> ! [D: qML_i] :
( ( qML_r @ sk37 @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[78,1217]) ).
thf(1459,plain,
( ( ~ ( incons1905966852QML_mu @ sk36 @ sk37 ) )
!= ( inconsistency_G @ sk36 @ sk37 ) ),
inference(pattern_uni,[status(thm)],[1458:[bind(A,$thf( sk36 )),bind(B,$thf( sk37 ))]]) ).
thf(1545,plain,
( ~ ( incons1905966852QML_mu @ sk36 @ sk37 )
| ( inconsistency_G @ sk36 @ sk37 ) ),
inference(bool_ext,[status(thm)],[1459]) ).
thf(1567,plain,
( ~ ( incons1905966852QML_mu @ sk36 @ sk37 )
| ( inconsistency_G @ sk36 @ sk37 ) ),
inference(cnf,[status(esa)],[1545]) ).
thf(77,plain,
! [A: qML_mu] :
( ( incons1905966852QML_mu @ A )
= ( ^ [B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ),
inference(func_ext,[status(esa)],[31]) ).
thf(2084,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ~ $true
| ( ( inconsistency_P @ sk67 @ sk4 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[1034,49]) ).
thf(2085,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( ( inconsistency_P @ sk67 @ sk4 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ) ) ),
inference(simp,[status(thm)],[2084]) ).
thf(2098,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( sk67
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C ) ) )
| ( sk4 != A ) ),
inference(simp,[status(thm)],[2085]) ).
thf(2108,plain,
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( sk67
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( incons1905966852QML_mu @ A @ B ) ) ) ),
inference(simp,[status(thm)],[2098]) ).
thf(1445,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ sk4 )
=> ( C @ sk3 @ sk4 ) ) ) )
| ( ( incons1905966852QML_mu @ A @ B )
!= ( incons1905966852QML_mu @ sk3 @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[78,934]) ).
thf(1446,plain,
( ( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk3 @ sk4 )
=> ! [B: qML_i] :
( ( qML_r @ sk4 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) )
!= ( ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk4 )
=> ( A @ sk3 @ sk4 ) ) ) ),
inference(pattern_uni,[status(thm)],[1445:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(1825,plain,
( ( incons1905966852QML_mu @ sk23 @ sk24 )
| ( inconsistency_P @ sk135 @ sk24 ) ),
inference(cnfConj,[status(thm)],[1824]) ).
thf(973,plain,
( ~ ( incons1905966852QML_mu @ sk13 @ sk14 )
| ~ ~ ( inconsistency_G @ sk13 @ sk14 ) ),
inference(bool_ext,[status(thm)],[913]) ).
thf(985,plain,
( ~ ( incons1905966852QML_mu @ sk13 @ sk14 )
| ( inconsistency_G @ sk13 @ sk14 ) ),
inference(cnf,[status(esa)],[973]) ).
thf(1264,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ~ $true
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk22 @ sk14 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[416,61]) ).
thf(1265,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk22 @ sk14 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[1264]) ).
thf(1266,plain,
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ( incons1905966852QML_mu
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( sk22 @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1265:[bind(A,$thf( sk14 )),bind(B,$thf( sk22 ))]]) ).
thf(1775,plain,
( ( incons1905966852QML_mu @ sk15 @ sk16 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk16 )
=> ( A @ sk15 @ sk16 ) ) ),
inference(bool_ext,[status(thm)],[1482]) ).
thf(1797,plain,
( ( ( incons1905966852QML_mu @ sk15 @ sk16 )
| ( inconsistency_P @ sk134 @ sk16 ) )
& ( ( incons1905966852QML_mu @ sk15 @ sk16 )
| ~ ( sk134 @ sk15 @ sk16 ) ) ),
inference(cnf,[status(esa)],[1775]) ).
thf(1799,plain,
( ( incons1905966852QML_mu @ sk15 @ sk16 )
| ~ ( sk134 @ sk15 @ sk16 ) ),
inference(cnfConj,[status(thm)],[1797]) ).
thf(193,plain,
( ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk8 )
=> ( A @ sk7 @ sk8 ) )
| ~ ( incons1905966852QML_mu @ sk7 @ sk8 ) ),
inference(bool_ext,[status(thm)],[122]) ).
thf(200,plain,
! [A: qML_mu > qML_i > $o] :
( ~ ( inconsistency_P @ A @ sk8 )
| ( A @ sk7 @ sk8 )
| ~ ( incons1905966852QML_mu @ sk7 @ sk8 ) ),
inference(cnf,[status(esa)],[193]) ).
thf(4967,plain,
( ~ ( inconsistency_P
@ ^ [A: qML_mu,B: qML_i] : $false
@ sk8 )
| $false
| ~ ( incons1905966852QML_mu @ sk7 @ sk8 ) ),
inference(prim_subst,[status(thm)],[200:[bind(A,$thf( ^ [B: qML_mu] : ^ [C: qML_i] : $false ))]]) ).
thf(5153,plain,
( ~ ( inconsistency_P
@ ^ [A: qML_mu,B: qML_i] : $false
@ sk8 )
| ~ ( incons1905966852QML_mu @ sk7 @ sk8 ) ),
inference(simp,[status(thm)],[4967]) ).
thf(1193,plain,
! [A: qML_mu > qML_i > $o] :
( ( ( incons1389517216QML_mu @ A )
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C ) ) )
| ( ( ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i] :
( ( qML_r @ C @ E )
=> ! [F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) )
!= ( ^ [B: qML_mu,C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( inconsistency_P @ D @ C )
=> ( D @ B @ C ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[139,99]) ).
thf(1202,plain,
! [A: qML_mu > qML_i > $o] :
( ( ( incons1389517216QML_mu @ A )
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C ) ) )
| ( ( ^ [B: qML_mu,C: qML_i,D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i] :
( ( qML_r @ C @ E )
=> ! [F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) )
!= ( ^ [B: qML_mu,C: qML_i,D: qML_mu > qML_i > $o] :
( ( inconsistency_P @ D @ C )
=> ( D @ B @ C ) ) ) ) ),
inference(simp,[status(thm)],[1193]) ).
thf(1035,plain,
( ~ ( sk67 @ sk3 @ sk4 )
| ( incons1905966852QML_mu @ sk3 @ sk4 ) ),
inference(cnfConj,[status(thm)],[1033]) ).
thf(192,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk8 )
=> ( A @ sk7 @ sk8 ) )
| ~ ~ ( incons1905966852QML_mu @ sk7 @ sk8 ) ),
inference(bool_ext,[status(thm)],[122]) ).
thf(197,plain,
( ( ( inconsistency_P @ sk17 @ sk8 )
| ( incons1905966852QML_mu @ sk7 @ sk8 ) )
& ( ~ ( sk17 @ sk7 @ sk8 )
| ( incons1905966852QML_mu @ sk7 @ sk8 ) ) ),
inference(cnf,[status(esa)],[192]) ).
thf(198,plain,
( ( inconsistency_P @ sk17 @ sk8 )
| ( incons1905966852QML_mu @ sk7 @ sk8 ) ),
inference(cnfConj,[status(thm)],[197]) ).
thf(1276,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk7 @ sk8 )
| ~ $true
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk17 @ sk8 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[198,61]) ).
thf(1277,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk7 @ sk8 )
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk17 @ sk8 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[1276]) ).
thf(1278,plain,
( ( incons1905966852QML_mu @ sk7 @ sk8 )
| ( incons1905966852QML_mu
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( sk17 @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1277:[bind(A,$thf( sk8 )),bind(B,$thf( sk17 ))]]) ).
thf(1467,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ( incons1905966852QML_mu @ A @ B ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ sk37 )
=> ( C @ sk36 @ sk37 ) ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ sk36 @ sk37 )
=> ! [D: qML_i] :
( ( qML_r @ sk37 @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[78,757]) ).
thf(1468,plain,
( ( ~ ( incons1905966852QML_mu @ sk36 @ sk37 ) )
!= ( ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk37 )
=> ( A @ sk36 @ sk37 ) ) ) ),
inference(pattern_uni,[status(thm)],[1467:[bind(A,$thf( sk36 )),bind(B,$thf( sk37 ))]]) ).
thf(1626,plain,
( ~ ~ ( incons1905966852QML_mu @ sk36 @ sk37 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk37 )
=> ( A @ sk36 @ sk37 ) ) ),
inference(bool_ext,[status(thm)],[1468]) ).
thf(1647,plain,
( ( ( incons1905966852QML_mu @ sk36 @ sk37 )
| ( inconsistency_P @ sk125 @ sk37 ) )
& ( ( incons1905966852QML_mu @ sk36 @ sk37 )
| ~ ( sk125 @ sk36 @ sk37 ) ) ),
inference(cnf,[status(esa)],[1626]) ).
thf(1648,plain,
( ( incons1905966852QML_mu @ sk36 @ sk37 )
| ( inconsistency_P @ sk125 @ sk37 ) ),
inference(cnfConj,[status(thm)],[1647]) ).
thf(1740,plain,
( ~ ~ ( incons1905966852QML_mu @ sk28 @ sk29 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk29 )
=> ( A @ sk28 @ sk29 ) ) ),
inference(bool_ext,[status(thm)],[1479]) ).
thf(1762,plain,
( ( ( incons1905966852QML_mu @ sk28 @ sk29 )
| ( inconsistency_P @ sk132 @ sk29 ) )
& ( ( incons1905966852QML_mu @ sk28 @ sk29 )
| ~ ( sk132 @ sk28 @ sk29 ) ) ),
inference(cnf,[status(esa)],[1740]) ).
thf(1764,plain,
( ( incons1905966852QML_mu @ sk28 @ sk29 )
| ~ ( sk132 @ sk28 @ sk29 ) ),
inference(cnfConj,[status(thm)],[1762]) ).
thf(157,plain,
! [D: qML_mu > qML_i > $o,C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ $true
| ( qML_r @ B @ ( sk1 @ D @ C @ B ) )
| ( inconsistency_P @ D @ B )
| ( ( inconsistency_P @ inconsistency_G @ A )
!= ( inconsistency_P @ C @ B ) ) ),
inference(paramod_ordered,[status(thm)],[23,19]) ).
thf(158,plain,
! [D: qML_mu > qML_i > $o,C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ( qML_r @ B @ ( sk1 @ D @ C @ B ) )
| ( inconsistency_P @ D @ B )
| ( ( inconsistency_P @ inconsistency_G @ A )
!= ( inconsistency_P @ C @ B ) ) ),
inference(simp,[status(thm)],[157]) ).
thf(159,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( qML_r @ A @ ( sk1 @ B @ inconsistency_G @ A ) )
| ( inconsistency_P @ B @ A ) ),
inference(pattern_uni,[status(thm)],[158:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( inconsistency_G )),bind(D,$thf( D ))]]) ).
thf(166,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( qML_r @ A @ ( sk1 @ B @ inconsistency_G @ A ) )
| ( inconsistency_P @ B @ A ) ),
inference(simp,[status(thm)],[159]) ).
thf(34,plain,
! [A: qML_mu] :
( ( inconsistency_G @ A )
= ( ^ [B: qML_i] :
! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) ) ),
inference(func_ext,[status(esa)],[29]) ).
thf(1,conjecture,
$false,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(2,negated_conjecture,
~ $false,
inference(neg_conjecture,[status(cth)],[1]) ).
thf(12,plain,
~ $false,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(1347,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ~ $true
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk22 @ sk14 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[416,64]) ).
thf(1348,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk22 @ sk14 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[1347]) ).
thf(1349,plain,
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ( inconsistency_G
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( sk22 @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1348:[bind(A,$thf( sk14 )),bind(B,$thf( sk22 ))]]) ).
thf(220,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk7 @ sk8 )
| ~ $true
| ( ( inconsistency_P @ sk17 @ sk8 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[198,49]) ).
thf(221,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk7 @ sk8 )
| ( ( inconsistency_P @ sk17 @ sk8 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ) ) ),
inference(simp,[status(thm)],[220]) ).
thf(223,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk7 @ sk8 )
| ( sk17
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C ) ) )
| ( sk8 != A ) ),
inference(simp,[status(thm)],[221]) ).
thf(230,plain,
( ( incons1905966852QML_mu @ sk7 @ sk8 )
| ( sk17
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( incons1905966852QML_mu @ A @ B ) ) ) ),
inference(simp,[status(thm)],[223]) ).
thf(1464,plain,
! [B: qML_i,A: qML_mu] :
( ~ ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) )
| ( inconsistency_G @ sk5 @ sk6 )
| ( ( incons1905966852QML_mu @ A @ B )
!= ( incons1905966852QML_mu @ sk5 @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[78,137]) ).
thf(1465,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk5 @ sk6 )
=> ! [B: qML_i] :
( ( qML_r @ sk6 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) )
| ( inconsistency_G @ sk5 @ sk6 ) ),
inference(pattern_uni,[status(thm)],[1464:[bind(A,$thf( sk5 )),bind(B,$thf( sk6 ))]]) ).
thf(1540,plain,
! [A: qML_mu] :
( ( ( incons1389517216QML_mu @ sk123 @ sk5 @ sk6 )
| ( inconsistency_G @ sk5 @ sk6 ) )
& ( ( qML_r @ sk6 @ sk124 )
| ( inconsistency_G @ sk5 @ sk6 ) )
& ( ~ ( sk123 @ A @ sk124 )
| ( inconsistency_G @ sk5 @ sk6 ) ) ),
inference(cnf,[status(esa)],[1465]) ).
thf(1542,plain,
( ( qML_r @ sk6 @ sk124 )
| ( inconsistency_G @ sk5 @ sk6 ) ),
inference(cnfConj,[status(thm)],[1540]) ).
thf(2082,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ~ $true
| ( ( inconsistency_P @ sk67 @ sk4 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[1034,54]) ).
thf(2083,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( ( inconsistency_P @ sk67 @ sk4 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ) ) ),
inference(simp,[status(thm)],[2082]) ).
thf(2102,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( sk67
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C ) ) )
| ( sk4 != A ) ),
inference(simp,[status(thm)],[2083]) ).
thf(2111,plain,
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( sk67
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( inconsistency_G @ A @ B ) ) ) ),
inference(simp,[status(thm)],[2102]) ).
thf(140,plain,
! [B: qML_mu,A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ B )
= ( ^ [C: qML_i] :
! [D: qML_mu > qML_i > $o] :
( ( D @ B @ C )
=> ! [E: qML_i] :
( ( qML_r @ C @ E )
=> ! [F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) ) ) ),
inference(func_ext,[status(esa)],[33]) ).
thf(817,plain,
( ( inconsistency_G @ sk28 @ sk29 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk28 @ sk29 )
=> ! [B: qML_i] :
( ( qML_r @ sk29 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ),
inference(bool_ext,[status(thm)],[630]) ).
thf(825,plain,
! [A: qML_mu] :
( ( ( inconsistency_G @ sk28 @ sk29 )
| ( incons1389517216QML_mu @ sk53 @ sk28 @ sk29 ) )
& ( ( inconsistency_G @ sk28 @ sk29 )
| ( qML_r @ sk29 @ sk54 ) )
& ( ( inconsistency_G @ sk28 @ sk29 )
| ~ ( sk53 @ A @ sk54 ) ) ),
inference(cnf,[status(esa)],[817]) ).
thf(827,plain,
( ( inconsistency_G @ sk28 @ sk29 )
| ( qML_r @ sk29 @ sk54 ) ),
inference(cnfConj,[status(thm)],[825]) ).
thf(974,plain,
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ~ ( inconsistency_G @ sk13 @ sk14 ) ),
inference(bool_ext,[status(thm)],[913]) ).
thf(986,plain,
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ~ ( inconsistency_G @ sk13 @ sk14 ) ),
inference(cnf,[status(esa)],[974]) ).
thf(218,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk7 @ sk8 )
| ~ $true
| ( ( inconsistency_P @ sk17 @ sk8 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[198,54]) ).
thf(219,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk7 @ sk8 )
| ( ( inconsistency_P @ sk17 @ sk8 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ) ) ),
inference(simp,[status(thm)],[218]) ).
thf(224,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk7 @ sk8 )
| ( sk17
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C ) ) )
| ( sk8 != A ) ),
inference(simp,[status(thm)],[219]) ).
thf(226,plain,
( ( incons1905966852QML_mu @ sk7 @ sk8 )
| ( sk17
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( inconsistency_G @ A @ B ) ) ) ),
inference(simp,[status(thm)],[224]) ).
thf(2067,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ~ $true
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk67 @ sk4 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1034,61]) ).
thf(2068,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk67 @ sk4 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[2067]) ).
thf(2069,plain,
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( incons1905966852QML_mu
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( sk67 @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[2068:[bind(A,$thf( sk4 )),bind(B,$thf( sk67 ))]]) ).
thf(1490,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ~ ( inconsistency_G @ sk5 @ sk6 ) ) )
| ( ( incons1905966852QML_mu @ A @ B )
!= ( incons1905966852QML_mu @ sk5 @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[78,119]) ).
thf(1491,plain,
( ( ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk5 @ sk6 )
=> ! [B: qML_i] :
( ( qML_r @ sk6 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) )
!= ( ~ ( inconsistency_G @ sk5 @ sk6 ) ) ),
inference(pattern_uni,[status(thm)],[1490:[bind(A,$thf( sk5 )),bind(B,$thf( sk6 ))]]) ).
thf(1979,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk5 @ sk6 )
=> ! [B: qML_i] :
( ( qML_r @ sk6 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) )
| ~ ~ ( inconsistency_G @ sk5 @ sk6 ) ),
inference(bool_ext,[status(thm)],[1491]) ).
thf(2003,plain,
! [A: qML_mu] :
( ( ( incons1389517216QML_mu @ sk155 @ sk5 @ sk6 )
| ( inconsistency_G @ sk5 @ sk6 ) )
& ( ( qML_r @ sk6 @ sk156 )
| ( inconsistency_G @ sk5 @ sk6 ) )
& ( ~ ( sk155 @ A @ sk156 )
| ( inconsistency_G @ sk5 @ sk6 ) ) ),
inference(cnf,[status(esa)],[1979]) ).
thf(2005,plain,
( ( qML_r @ sk6 @ sk156 )
| ( inconsistency_G @ sk5 @ sk6 ) ),
inference(cnfConj,[status(thm)],[2003]) ).
thf(558,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ $true
| ~ ( inconsistency_P @ C @ B )
| ( ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ F @ D @ E )
=> ! [G: qML_i] :
( ( qML_r @ E @ G )
=> ? [H: qML_mu] : ( F @ H @ G ) ) )
@ A )
!= ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[83,14]) ).
thf(559,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P @ C @ B )
| ( ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ F @ D @ E )
=> ! [G: qML_i] :
( ( qML_r @ E @ G )
=> ? [H: qML_mu] : ( F @ H @ G ) ) )
@ A )
!= ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(simp,[status(thm)],[558]) ).
thf(583,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P @ C @ B )
| ( ( ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ F @ D @ E )
=> ! [G: qML_i] :
( ( qML_r @ E @ G )
=> ? [H: qML_mu] : ( F @ H @ G ) ) ) )
!= ( ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[559]) ).
thf(589,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( inconsistency_P @ B @ A )
| ( ( ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ E @ C @ D )
=> ! [F: qML_i] :
( ( qML_r @ D @ F )
=> ? [G: qML_mu] : ( E @ G @ F ) ) ) )
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) ) ),
inference(simp,[status(thm)],[583]) ).
thf(1896,plain,
! [B: qML_i,A: qML_mu] :
( ~ ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) )
| ( inconsistency_G @ sk13 @ sk14 )
| ( ( incons1905966852QML_mu @ A @ B )
!= ( incons1905966852QML_mu @ sk13 @ sk14 ) ) ),
inference(paramod_ordered,[status(thm)],[78,985]) ).
thf(1897,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk13 @ sk14 )
=> ! [B: qML_i] :
( ( qML_r @ sk14 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) )
| ( inconsistency_G @ sk13 @ sk14 ) ),
inference(pattern_uni,[status(thm)],[1896:[bind(A,$thf( sk13 )),bind(B,$thf( sk14 ))]]) ).
thf(1903,plain,
! [A: qML_mu] :
( ( ( incons1389517216QML_mu @ sk136 @ sk13 @ sk14 )
| ( inconsistency_G @ sk13 @ sk14 ) )
& ( ( qML_r @ sk14 @ sk137 )
| ( inconsistency_G @ sk13 @ sk14 ) )
& ( ~ ( sk136 @ A @ sk137 )
| ( inconsistency_G @ sk13 @ sk14 ) ) ),
inference(cnf,[status(esa)],[1897]) ).
thf(1905,plain,
( ( qML_r @ sk14 @ sk137 )
| ( inconsistency_G @ sk13 @ sk14 ) ),
inference(cnfConj,[status(thm)],[1903]) ).
thf(1798,plain,
( ( incons1905966852QML_mu @ sk15 @ sk16 )
| ( inconsistency_P @ sk134 @ sk16 ) ),
inference(cnfConj,[status(thm)],[1797]) ).
thf(5546,plain,
! [A: qML_i] :
( ~ $true
| ~ ( incons1905966852QML_mu @ sk7 @ sk8 )
| ( ( inconsistency_P @ inconsistency_G @ A )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ sk8 ) ) ),
inference(paramod_ordered,[status(thm)],[23,5153]) ).
thf(5547,plain,
! [A: qML_i] :
( ~ ( incons1905966852QML_mu @ sk7 @ sk8 )
| ( ( inconsistency_P @ inconsistency_G @ A )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] : $false
@ sk8 ) ) ),
inference(simp,[status(thm)],[5546]) ).
thf(5568,plain,
! [A: qML_i] :
( ~ ( incons1905966852QML_mu @ sk7 @ sk8 )
| ( inconsistency_G
!= ( ^ [B: qML_mu,C: qML_i] : $false ) )
| ( A != sk8 ) ),
inference(simp,[status(thm)],[5547]) ).
thf(5607,plain,
( ~ ( incons1905966852QML_mu @ sk7 @ sk8 )
| ( inconsistency_G
!= ( ^ [A: qML_mu,B: qML_i] : $false ) ) ),
inference(simp,[status(thm)],[5568]) ).
thf(1763,plain,
( ( incons1905966852QML_mu @ sk28 @ sk29 )
| ( inconsistency_P @ sk132 @ sk29 ) ),
inference(cnfConj,[status(thm)],[1762]) ).
thf(1988,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ B )
=> ( C @ A @ B ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ sk5 @ sk6 )
=> ! [D: qML_i] :
( ( qML_r @ sk6 @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) )
| ( ( inconsistency_G @ A @ B )
!= ( inconsistency_G @ sk5 @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[35,1491]) ).
thf(1989,plain,
( ( ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk6 )
=> ( A @ sk5 @ sk6 ) ) )
!= ( ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk5 @ sk6 )
=> ! [B: qML_i] :
( ( qML_r @ sk6 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ) ),
inference(pattern_uni,[status(thm)],[1988:[bind(A,$thf( sk5 )),bind(B,$thf( sk6 ))]]) ).
thf(2321,plain,
! [B: qML_i,A: qML_mu] :
( ( ( incons1905966852QML_mu @ A @ B )
!= ( ~ ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ sk6 )
=> ( C @ sk5 @ sk6 ) ) ) )
| ( ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ sk5 @ sk6 )
=> ! [D: qML_i] :
( ( qML_r @ sk6 @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[78,1989]) ).
thf(2322,plain,
( ( incons1905966852QML_mu @ sk5 @ sk6 )
!= ( ~ ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk6 )
=> ( A @ sk5 @ sk6 ) ) ) ),
inference(pattern_uni,[status(thm)],[2321:[bind(A,$thf( sk5 )),bind(B,$thf( sk6 ))]]) ).
thf(1686,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ~ $true
| ( ( inconsistency_P @ sk63 @ sk6 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[959,54]) ).
thf(1687,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ( ( inconsistency_P @ sk63 @ sk6 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ) ) ),
inference(simp,[status(thm)],[1686]) ).
thf(1702,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ( sk63
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C ) ) )
| ( sk6 != A ) ),
inference(simp,[status(thm)],[1687]) ).
thf(1711,plain,
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ( sk63
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( inconsistency_G @ A @ B ) ) ) ),
inference(simp,[status(thm)],[1702]) ).
thf(199,plain,
( ~ ( sk17 @ sk7 @ sk8 )
| ( incons1905966852QML_mu @ sk7 @ sk8 ) ),
inference(cnfConj,[status(thm)],[197]) ).
thf(658,plain,
! [A: qML_i] :
( ( inconsistency_G @ sk11 @ sk12 )
| ~ $true
| ( ( inconsistency_P @ sk21 @ sk12 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[396,49]) ).
thf(659,plain,
! [A: qML_i] :
( ( inconsistency_G @ sk11 @ sk12 )
| ( ( inconsistency_P @ sk21 @ sk12 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ) ) ),
inference(simp,[status(thm)],[658]) ).
thf(665,plain,
! [A: qML_i] :
( ( inconsistency_G @ sk11 @ sk12 )
| ( sk21
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C ) ) )
| ( sk12 != A ) ),
inference(simp,[status(thm)],[659]) ).
thf(673,plain,
( ( inconsistency_G @ sk11 @ sk12 )
| ( sk21
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( incons1905966852QML_mu @ A @ B ) ) ) ),
inference(simp,[status(thm)],[665]) ).
thf(1908,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk13 @ sk14 )
=> ! [B: qML_i] :
( ( qML_r @ sk14 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) )
| ~ ~ ( inconsistency_G @ sk13 @ sk14 ) ),
inference(bool_ext,[status(thm)],[1441]) ).
thf(1932,plain,
! [A: qML_mu] :
( ( ( incons1389517216QML_mu @ sk141 @ sk13 @ sk14 )
| ( inconsistency_G @ sk13 @ sk14 ) )
& ( ( qML_r @ sk14 @ sk142 )
| ( inconsistency_G @ sk13 @ sk14 ) )
& ( ~ ( sk141 @ A @ sk142 )
| ( inconsistency_G @ sk13 @ sk14 ) ) ),
inference(cnf,[status(esa)],[1908]) ).
thf(1934,plain,
( ( qML_r @ sk14 @ sk142 )
| ( inconsistency_G @ sk13 @ sk14 ) ),
inference(cnfConj,[status(thm)],[1932]) ).
thf(988,plain,
( ( inconsistency_G @ sk7 @ sk8 )
| ~ ( incons1905966852QML_mu @ sk7 @ sk8 ) ),
inference(bool_ext,[status(thm)],[937]) ).
thf(1008,plain,
( ( inconsistency_G @ sk7 @ sk8 )
| ~ ( incons1905966852QML_mu @ sk7 @ sk8 ) ),
inference(cnf,[status(esa)],[988]) ).
thf(1270,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_G @ sk9 @ sk10 )
| ~ $true
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk18 @ sk10 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[205,61]) ).
thf(1271,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_G @ sk9 @ sk10 )
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk18 @ sk10 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[1270]) ).
thf(1272,plain,
( ( inconsistency_G @ sk9 @ sk10 )
| ( incons1905966852QML_mu
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( sk18 @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1271:[bind(A,$thf( sk10 )),bind(B,$thf( sk18 ))]]) ).
thf(877,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ~ $true
| ( ( inconsistency_P @ sk22 @ sk14 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[416,54]) ).
thf(878,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ( ( inconsistency_P @ sk22 @ sk14 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C )
@ A ) ) ),
inference(simp,[status(thm)],[877]) ).
thf(883,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ( sk22
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C ) ) )
| ( sk14 != A ) ),
inference(simp,[status(thm)],[878]) ).
thf(891,plain,
( ( incons1905966852QML_mu @ sk13 @ sk14 )
| ( sk22
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( inconsistency_G @ A @ B ) ) ) ),
inference(simp,[status(thm)],[883]) ).
thf(1649,plain,
( ( incons1905966852QML_mu @ sk36 @ sk37 )
| ~ ( sk125 @ sk36 @ sk37 ) ),
inference(cnfConj,[status(thm)],[1647]) ).
thf(442,plain,
! [A: qML_i] :
( ( inconsistency_G @ sk9 @ sk10 )
| ~ $true
| ( ( inconsistency_P @ sk18 @ sk10 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[205,49]) ).
thf(443,plain,
! [A: qML_i] :
( ( inconsistency_G @ sk9 @ sk10 )
| ( ( inconsistency_P @ sk18 @ sk10 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ) ) ),
inference(simp,[status(thm)],[442]) ).
thf(444,plain,
! [A: qML_i] :
( ( inconsistency_G @ sk9 @ sk10 )
| ( sk18
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C ) ) )
| ( sk10 != A ) ),
inference(simp,[status(thm)],[443]) ).
thf(450,plain,
( ( inconsistency_G @ sk9 @ sk10 )
| ( sk18
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( incons1905966852QML_mu @ A @ B ) ) ) ),
inference(simp,[status(thm)],[444]) ).
thf(1569,plain,
( ~ ~ ( incons1905966852QML_mu @ sk28 @ sk29 )
| ~ ( inconsistency_G @ sk28 @ sk29 ) ),
inference(bool_ext,[status(thm)],[1461]) ).
thf(1590,plain,
( ( incons1905966852QML_mu @ sk28 @ sk29 )
| ~ ( inconsistency_G @ sk28 @ sk29 ) ),
inference(cnf,[status(esa)],[1569]) ).
thf(1228,plain,
( ( inconsistency_G @ sk36 @ sk37 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk36 @ sk37 )
=> ! [B: qML_i] :
( ( qML_r @ sk37 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ),
inference(bool_ext,[status(thm)],[1217]) ).
thf(1242,plain,
! [A: qML_mu] :
( ( ( inconsistency_G @ sk36 @ sk37 )
| ( incons1389517216QML_mu @ sk88 @ sk36 @ sk37 ) )
& ( ( inconsistency_G @ sk36 @ sk37 )
| ( qML_r @ sk37 @ sk89 ) )
& ( ( inconsistency_G @ sk36 @ sk37 )
| ~ ( sk88 @ A @ sk89 ) ) ),
inference(cnf,[status(esa)],[1228]) ).
thf(1244,plain,
( ( inconsistency_G @ sk36 @ sk37 )
| ( qML_r @ sk37 @ sk89 ) ),
inference(cnfConj,[status(thm)],[1242]) ).
thf(55,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( inconsistency_P @ B @ A )
| ( ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A )
!= ( inconsistency_P @ B @ A ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[14]) ).
thf(58,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( inconsistency_P @ B @ A )
| ( ( inconsistency_P
@ ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D )
@ A )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[55]) ).
thf(1611,plain,
( ( incons1905966852QML_mu @ sk23 @ sk24 )
| ~ ( inconsistency_G @ sk23 @ sk24 ) ),
inference(bool_ext,[status(thm)],[1486]) ).
thf(1625,plain,
( ( incons1905966852QML_mu @ sk23 @ sk24 )
| ~ ( inconsistency_G @ sk23 @ sk24 ) ),
inference(cnf,[status(esa)],[1611]) ).
thf(1671,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ~ $true
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk63 @ sk6 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[959,61]) ).
thf(1672,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ( incons1905966852QML_mu
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk63 @ sk6 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[1671]) ).
thf(1673,plain,
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ( incons1905966852QML_mu
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( sk63 @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1672:[bind(A,$thf( sk6 )),bind(B,$thf( sk63 ))]]) ).
thf(1361,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk7 @ sk8 )
| ~ $true
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk17 @ sk8 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[198,64]) ).
thf(1362,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk7 @ sk8 )
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk17 @ sk8 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[1361]) ).
thf(1363,plain,
( ( incons1905966852QML_mu @ sk7 @ sk8 )
| ( inconsistency_G
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( sk17 @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1362:[bind(A,$thf( sk8 )),bind(B,$thf( sk17 ))]]) ).
thf(960,plain,
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ~ ( sk63 @ sk5 @ sk6 ) ),
inference(cnfConj,[status(thm)],[958]) ).
thf(3506,plain,
! [A: qML_mu > qML_i > $o] :
( ( ( incons1389517216QML_mu @ A )
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( inconsistency_G @ B @ C ) ) )
| ( ( ^ [B: qML_mu,C: qML_i,D: qML_mu > qML_i > $o] : ( D @ B @ C ) )
!= ( ^ [B: qML_mu,C: qML_i,D: qML_mu > qML_i > $o] : ( inconsistency_P @ D @ C ) ) )
| ( ( ^ [B: qML_mu,C: qML_i,D: qML_mu > qML_i > $o] :
! [E: qML_i] :
( ( qML_r @ C @ E )
=> ! [F: qML_mu] :
( ( A @ F @ E )
=> ( D @ F @ E ) ) ) )
!= ( ^ [B: qML_mu,C: qML_i,D: qML_mu > qML_i > $o] : ( D @ B @ C ) ) ) ),
inference(simp,[status(thm)],[1202]) ).
thf(1959,plain,
( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk3 @ sk4 )
=> ! [B: qML_i] :
( ( qML_r @ sk4 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) )
| ( inconsistency_G @ sk3 @ sk4 ) ),
inference(bool_ext,[status(thm)],[1489]) ).
thf(1975,plain,
! [A: qML_mu] :
( ( ( incons1389517216QML_mu @ sk150 @ sk3 @ sk4 )
| ( inconsistency_G @ sk3 @ sk4 ) )
& ( ( qML_r @ sk4 @ sk151 )
| ( inconsistency_G @ sk3 @ sk4 ) )
& ( ~ ( sk150 @ A @ sk151 )
| ( inconsistency_G @ sk3 @ sk4 ) ) ),
inference(cnf,[status(esa)],[1959]) ).
thf(1977,plain,
( ( qML_r @ sk4 @ sk151 )
| ( inconsistency_G @ sk3 @ sk4 ) ),
inference(cnfConj,[status(thm)],[1975]) ).
thf(1355,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_G @ sk9 @ sk10 )
| ~ $true
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk18 @ sk10 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[205,64]) ).
thf(1356,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_G @ sk9 @ sk10 )
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk18 @ sk10 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[1355]) ).
thf(1357,plain,
( ( inconsistency_G @ sk9 @ sk10 )
| ( inconsistency_G
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( sk18 @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1356:[bind(A,$thf( sk10 )),bind(B,$thf( sk18 ))]]) ).
thf(1499,plain,
! [B: qML_i,A: qML_mu] :
( ( ( ~ ! [C: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ C @ A @ B )
=> ! [D: qML_i] :
( ( qML_r @ B @ D )
=> ? [E: qML_mu] : ( C @ E @ D ) ) ) )
!= ( ! [C: qML_mu > qML_i > $o] :
( ( inconsistency_P @ C @ sk8 )
=> ( C @ sk7 @ sk8 ) ) ) )
| ( ( incons1905966852QML_mu @ A @ B )
!= ( incons1905966852QML_mu @ sk7 @ sk8 ) ) ),
inference(paramod_ordered,[status(thm)],[78,122]) ).
thf(1500,plain,
( ( ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk7 @ sk8 )
=> ! [B: qML_i] :
( ( qML_r @ sk8 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) )
!= ( ! [A: qML_mu > qML_i > $o] :
( ( inconsistency_P @ A @ sk8 )
=> ( A @ sk7 @ sk8 ) ) ) ),
inference(pattern_uni,[status(thm)],[1499:[bind(A,$thf( sk7 )),bind(B,$thf( sk8 ))]]) ).
thf(40,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ $true
| ~ ( inconsistency_P @ C @ B )
| ( ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( inconsistency_P @ F @ E )
=> ( F @ D @ E ) )
@ A )
!= ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(paramod_ordered,[status(thm)],[37,14]) ).
thf(41,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P @ C @ B )
| ( ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( inconsistency_P @ F @ E )
=> ( F @ D @ E ) )
@ A )
!= ( inconsistency_P
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ B ) ) ),
inference(simp,[status(thm)],[40]) ).
thf(57,plain,
! [C: qML_mu > qML_i > $o,B: qML_i,A: qML_i] :
( ~ ( inconsistency_P @ C @ B )
| ( ( ^ [D: qML_mu,E: qML_i] :
! [F: qML_mu > qML_i > $o] :
( ( inconsistency_P @ F @ E )
=> ( F @ D @ E ) ) )
!= ( ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[41]) ).
thf(62,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ~ ( inconsistency_P @ B @ A )
| ( ( ^ [C: qML_mu,D: qML_i] :
! [E: qML_mu > qML_i > $o] :
( ( inconsistency_P @ E @ D )
=> ( E @ C @ D ) ) )
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) ) ),
inference(simp,[status(thm)],[57]) ).
thf(1858,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ~ $true
| ( ( inconsistency_P @ sk65 @ sk4 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[971,49]) ).
thf(1859,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( ( inconsistency_P @ sk65 @ sk4 )
!= ( inconsistency_P
@ ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C )
@ A ) ) ),
inference(simp,[status(thm)],[1858]) ).
thf(1875,plain,
! [A: qML_i] :
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( sk65
!= ( ^ [B: qML_mu,C: qML_i] :
~ ( incons1905966852QML_mu @ B @ C ) ) )
| ( sk4 != A ) ),
inference(simp,[status(thm)],[1859]) ).
thf(1885,plain,
( ( incons1905966852QML_mu @ sk3 @ sk4 )
| ( sk65
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( incons1905966852QML_mu @ A @ B ) ) ) ),
inference(simp,[status(thm)],[1875]) ).
thf(160,plain,
! [E: qML_mu > qML_i > $o,D: qML_mu > qML_i > $o,C: qML_i,B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_P @ B @ A )
| ~ $true
| ( qML_r @ C @ ( sk1 @ E @ D @ C ) )
| ( inconsistency_P @ E @ C )
| ( ( inconsistency_P
@ ^ [F: qML_mu,G: qML_i] :
~ ( B @ F @ G )
@ A )
!= ( inconsistency_P @ D @ C ) ) ),
inference(paramod_ordered,[status(thm)],[16,19]) ).
thf(161,plain,
! [E: qML_mu > qML_i > $o,D: qML_mu > qML_i > $o,C: qML_i,B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_P @ B @ A )
| ( qML_r @ C @ ( sk1 @ E @ D @ C ) )
| ( inconsistency_P @ E @ C )
| ( ( inconsistency_P
@ ^ [F: qML_mu,G: qML_i] :
~ ( B @ F @ G )
@ A )
!= ( inconsistency_P @ D @ C ) ) ),
inference(simp,[status(thm)],[160]) ).
thf(162,plain,
! [C: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_P @ C @ A )
| ( qML_r @ A
@ ( sk1 @ B
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ A ) )
| ( inconsistency_P @ B @ A ) ),
inference(pattern_uni,[status(thm)],[161:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( A )),bind(D,$thf( ^ [G: qML_mu] : ^ [H: qML_i] : ~ ( F @ G @ H ) ))]]) ).
thf(163,plain,
! [C: qML_mu > qML_i > $o,B: qML_mu > qML_i > $o,A: qML_i] :
( ( inconsistency_P @ C @ A )
| ( qML_r @ A
@ ( sk1 @ B
@ ^ [D: qML_mu,E: qML_i] :
~ ( C @ D @ E )
@ A ) )
| ( inconsistency_P @ B @ A ) ),
inference(simp,[status(thm)],[162]) ).
thf(1679,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ~ $true
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk63 @ sk6 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[959,64]) ).
thf(1680,plain,
! [B: qML_mu > qML_i > $o,A: qML_i] :
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ( inconsistency_G
!= ( ^ [C: qML_mu,D: qML_i] :
~ ( B @ C @ D ) ) )
| ( ( inconsistency_P @ sk63 @ sk6 )
!= ( inconsistency_P @ B @ A ) ) ),
inference(simp,[status(thm)],[1679]) ).
thf(1681,plain,
( ( incons1905966852QML_mu @ sk5 @ sk6 )
| ( inconsistency_G
!= ( ^ [A: qML_mu,B: qML_i] :
~ ( sk63 @ A @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[1680:[bind(A,$thf( sk6 )),bind(B,$thf( sk63 ))]]) ).
thf(1544,plain,
( ~ ~ ( incons1905966852QML_mu @ sk36 @ sk37 )
| ~ ( inconsistency_G @ sk36 @ sk37 ) ),
inference(bool_ext,[status(thm)],[1459]) ).
thf(1565,plain,
( ( incons1905966852QML_mu @ sk36 @ sk37 )
| ~ ( inconsistency_G @ sk36 @ sk37 ) ),
inference(cnf,[status(esa)],[1544]) ).
thf(1064,plain,
( ~ ~ ( inconsistency_G @ sk23 @ sk24 )
| ~ ! [A: qML_mu > qML_i > $o] :
( ( incons1389517216QML_mu @ A @ sk23 @ sk24 )
=> ! [B: qML_i] :
( ( qML_r @ sk24 @ B )
=> ? [C: qML_mu] : ( A @ C @ B ) ) ) ),
inference(bool_ext,[status(thm)],[1053]) ).
thf(1086,plain,
! [A: qML_mu] :
( ( ( inconsistency_G @ sk23 @ sk24 )
| ( incons1389517216QML_mu @ sk75 @ sk23 @ sk24 ) )
& ( ( inconsistency_G @ sk23 @ sk24 )
| ( qML_r @ sk24 @ sk76 ) )
& ( ( inconsistency_G @ sk23 @ sk24 )
| ~ ( sk75 @ A @ sk76 ) ) ),
inference(cnf,[status(esa)],[1064]) ).
thf(1088,plain,
( ( inconsistency_G @ sk23 @ sk24 )
| ( qML_r @ sk24 @ sk76 ) ),
inference(cnfConj,[status(thm)],[1086]) ).
thf(972,plain,
( ~ ( sk65 @ sk3 @ sk4 )
| ( incons1905966852QML_mu @ sk3 @ sk4 ) ),
inference(cnfConj,[status(thm)],[970]) ).
thf(6560,plain,
$false,
inference(e,[status(thm)],[138,628,2077,115,1443,1591,1269,1486,1608,913,1954,1354,670,185,782,1441,417,24,37,1518,1482,25,14,802,1826,934,20,416,78,29,1479,1609,1489,164,1714,121,937,84,397,61,1886,453,396,133,74,206,147,1843,1206,1470,28,1217,630,165,33,21,137,847,1624,889,757,4063,1851,188,1006,593,141,1567,1493,77,1461,2108,1446,1825,985,1266,1799,13,134,5153,1202,633,205,921,1035,926,1278,1648,1764,166,64,180,17,32,34,562,22,44,27,12,54,49,181,187,1349,76,230,1542,2111,140,626,198,959,827,986,226,35,2069,2005,1034,589,1905,1798,5607,971,182,16,1763,2322,31,1711,1053,199,673,1934,1008,1272,87,891,1453,1649,450,1459,99,1590,26,23,139,1244,1491,119,58,30,1625,422,19,1673,1363,960,3506,126,1989,624,1977,596,1357,1500,15,62,1885,163,200,122,83,1681,1565,1088,1468,100,972]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PHI007^5 : TPTP v9.3.1. Released v6.4.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.22 % Computer : n004.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % 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 13:19:52 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
% 0.64/0.52 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 0.85/0.62 % [INFO] Parsing done (106ms).
% 1.04/0.63 % [INFO] Running in sequential loop mode.
% 1.40/0.82 % [INFO] eprover registered as external prover.
% 1.40/0.82 % [INFO] Scanning for conjecture ...
% 1.40/0.86 % [INFO] Found a conjecture (or negated_conjecture) and 9 axioms. Running axiom selection ...
% 1.40/0.88 % [INFO] Axiom selection finished. Selected 9 axioms (removed 0 axioms).
% 1.67/0.90 % [INFO] Problem is higher-order (TPTP THF).
% 1.67/0.91 % [INFO] Type checking passed.
% 1.67/0.91 % [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 ...
% 94.04/39.43 % External prover 'e' found a proof!
% 94.04/39.43 % [INFO] Killing All external provers ...
% 94.04/39.43 % Time passed: 39119ms (effective reasoning time: 38793ms)
% 94.04/39.43 % 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)>
% 94.04/39.43 % Axioms used in derivation (9): fact_7_NE__def, fact_8_ess__def, fact_1_A1b, fact_4_A4, fact_2_A2, fact_0_A1a, fact_6_G__def, fact_3_A3, fact_5_A5
% 94.04/39.43 % No. of inferences in proof: 434
% 94.04/39.43 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 39119 ms resp. 38793 ms w/o parsing
% 94.70/39.68 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 94.70/39.68 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------