%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP076^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n011.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:06:40 AM UTC 2026
% Result : Theorem 100.35s 23.11s
% Output : Refutation 102.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 53
% Syntax : Number of formulae : 420 ( 181 unt; 0 typ; 21 def)
% Number of atoms : 1286 ( 478 equ; 4 cnn)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 4116 ( 417 ~; 302 |; 108 &;3206 @)
% ( 0 <=>; 83 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 174 ( 174 >; 0 *; 0 +; 0 <<)
% Number of symbols : 41 ( 37 usr; 8 con; 0-4 aty)
% Number of variables : 1062 ( 97 ^; 851 !; 93 ?;1062 :)
% ( 0 !>; 0 ?*; 0 @-; 21 @+)
% Comments :
%------------------------------------------------------------------------------
thf(hF_Mirabelle_hf_type,type,
hF_Mirabelle_hf: $tType ).
thf(nat_type,type,
nat: $tType ).
thf(hF_Mir1687042746ollect_decl,type,
hF_Mir1687042746ollect: ( hF_Mirabelle_hf > $o ) > hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(hF_Mirabelle_HUnion_decl,type,
hF_Mirabelle_HUnion: hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(hF_Mir569462966eplace_decl,type,
hF_Mir569462966eplace: hF_Mirabelle_hf > ( hF_Mirabelle_hf > hF_Mirabelle_hf > $o ) > hF_Mirabelle_hf ).
thf(hF_Mirabelle_RepFun_decl,type,
hF_Mirabelle_RepFun: hF_Mirabelle_hf > ( hF_Mirabelle_hf > hF_Mirabelle_hf ) > hF_Mirabelle_hf ).
thf(hF_Mirabelle_Replace_decl,type,
hF_Mirabelle_Replace: hF_Mirabelle_hf > ( hF_Mirabelle_hf > hF_Mirabelle_hf > $o ) > hF_Mirabelle_hf ).
thf(hF_Mirabelle_hfst_decl,type,
hF_Mirabelle_hfst: hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(hF_Mir859708136nction_decl,type,
hF_Mir859708136nction: hF_Mirabelle_hf > $o ).
thf(hF_Mirabelle_hmem_decl,type,
hF_Mirabelle_hmem: hF_Mirabelle_hf > hF_Mirabelle_hf > $o ).
thf(hF_Mirabelle_hpair_decl,type,
hF_Mirabelle_hpair: hF_Mirabelle_hf > hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(hF_Mir1093797708lation_decl,type,
hF_Mir1093797708lation: hF_Mirabelle_hf > $o ).
thf(hF_Mir165288108strict_decl,type,
hF_Mir165288108strict: hF_Mirabelle_hf > hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(hF_Mirabelle_hsnd_decl,type,
hF_Mirabelle_hsnd: hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(hF_Mirabelle_hsplit_decl,type,
hF_Mirabelle_hsplit:
!>[TA: $tType] : ( ( hF_Mirabelle_hf > hF_Mirabelle_hf > TA ) > hF_Mirabelle_hf > TA ) ).
thf(hF_Mir796903520_hpair_decl,type,
hF_Mir796903520_hpair: hF_Mirabelle_hf > $o ).
thf(r_decl,type,
r: hF_Mirabelle_hf ).
thf(x_decl,type,
x: hF_Mirabelle_hf ).
thf(sk1_decl,type,
sk1: ( hF_Mirabelle_hf > hF_Mirabelle_hf > $o ) > hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk2_decl,type,
sk2: ( hF_Mirabelle_hf > hF_Mirabelle_hf > $o ) > hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk3_decl,type,
sk3: ( hF_Mirabelle_hf > hF_Mirabelle_hf > $o ) > hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk4_decl,type,
sk4: ( hF_Mirabelle_hf > hF_Mirabelle_hf > $o ) > ( hF_Mirabelle_hf > hF_Mirabelle_hf > $o ) > hF_Mirabelle_hf > hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk5_decl,type,
sk5: ( hF_Mirabelle_hf > hF_Mirabelle_hf > $o ) > ( hF_Mirabelle_hf > hF_Mirabelle_hf > $o ) > hF_Mirabelle_hf > hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk6_decl,type,
sk6: hF_Mirabelle_hf > hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk7_decl,type,
sk7: hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk8_decl,type,
sk8: ( hF_Mirabelle_hf > hF_Mirabelle_hf ) > ( hF_Mirabelle_hf > hF_Mirabelle_hf ) > hF_Mirabelle_hf > hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk10_decl,type,
sk10: hF_Mirabelle_hf > hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk11_decl,type,
sk11: hF_Mirabelle_hf > hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk24_decl,type,
sk24: hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk76_decl,type,
sk76: hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk77_decl,type,
sk77: hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk95_decl,type,
sk95: hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk96_decl,type,
sk96: hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk112_decl,type,
sk112: hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk128_decl,type,
sk128: hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk129_decl,type,
sk129: hF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(sk148_decl,type,
sk148: hF_Mirabelle_hf ).
thf(sk149_decl,type,
sk149: hF_Mirabelle_hf ).
thf(sk150_decl,type,
sk150: hF_Mirabelle_hf ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf] :
@+[C: hF_Mirabelle_hf] :
~ ( ( hF_Mirabelle_hmem @ C @ B )
=> ! [D: hF_Mirabelle_hf] :
( ( A @ C @ D )
=> ! [E: hF_Mirabelle_hf] :
( ( A @ C @ E )
=> ( E = D ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf] :
@+[C: hF_Mirabelle_hf] :
~ ( ( A @ ( sk1 @ A @ B ) @ C )
=> ! [D: hF_Mirabelle_hf] :
( ( A @ ( sk1 @ A @ B ) @ D )
=> ( D = C ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf] :
@+[C: hF_Mirabelle_hf] :
~ ( ( A @ ( sk1 @ A @ B ) @ C )
=> ( C
= ( sk2 @ A @ B ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( ^ [A: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,C: hF_Mirabelle_hf,D: hF_Mirabelle_hf] :
@+[E: hF_Mirabelle_hf] :
~ ( ( hF_Mirabelle_hmem @ E @ C )
=> ! [F: hF_Mirabelle_hf] :
( ( B @ E @ F )
= ( A @ E @ F ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,C: hF_Mirabelle_hf,D: hF_Mirabelle_hf] :
@+[E: hF_Mirabelle_hf] :
( ( B @ ( sk4 @ A @ B @ C @ D ) @ E )
!= ( A @ ( sk4 @ A @ B @ C @ D ) @ E ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
@+[C: hF_Mirabelle_hf] :
! [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ C )
= ( ( hF_Mirabelle_hmem @ D @ B )
| ( hF_Mirabelle_hmem @ D @ A ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: hF_Mirabelle_hf] :
@+[B: hF_Mirabelle_hf] :
! [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ B )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( hF_Mirabelle_hmem @ C @ D ) ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: hF_Mirabelle_hf > hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf,C: hF_Mirabelle_hf,D: hF_Mirabelle_hf] :
@+[E: hF_Mirabelle_hf] :
~ ( ( hF_Mirabelle_hmem @ E @ C )
=> ( ( B @ E )
= ( A @ E ) ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( @+[A: hF_Mirabelle_hf > hF_Mirabelle_hf > hF_Mirabelle_hf] :
! [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( ( A @ C @ ( hF_Mirabelle_hpair @ B @ C ) )
= B ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( @+[A: hF_Mirabelle_hf > hF_Mirabelle_hf > hF_Mirabelle_hf] :
! [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( ( A @ B @ ( hF_Mirabelle_hpair @ B @ C ) )
= C ) ) ) ).
thf(sk24_def,definition,
( sk24
= ( ^ [A: hF_Mirabelle_hf] :
@+[B: hF_Mirabelle_hf] :
~ ( ( hF_Mirabelle_hmem @ B @ A )
=> ( hF_Mir796903520_hpair @ B ) ) ) ) ).
thf(sk76_def,definition,
( sk76
= ( ^ [A: hF_Mirabelle_hf] :
@+[B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk24 @ ( hF_Mirabelle_HUnion @ A ) ) @ B ) ) ) ) ).
thf(sk77_def,definition,
( sk77
= ( ^ [A: hF_Mirabelle_hf] :
@+[B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk24 @ ( hF_Mirabelle_HUnion @ A ) ) @ B ) ) ) ) ).
thf(sk95_def,definition,
( sk95
= ( ^ [A: hF_Mirabelle_hf] :
@+[B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk24 @ ( sk7 @ A ) ) @ B ) ) ) ) ).
thf(sk96_def,definition,
( sk96
= ( ^ [A: hF_Mirabelle_hf] :
@+[B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk24 @ ( sk7 @ A ) ) @ B ) ) ) ) ).
thf(sk112_def,definition,
( sk112
= ( ^ [A: hF_Mirabelle_hf] :
@+[B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk76 @ ( hF_Mirabelle_HUnion @ A ) ) @ B ) ) ) ) ).
thf(sk128_def,definition,
( sk128
= ( ^ [A: hF_Mirabelle_hf] :
@+[B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk24 @ ( hF_Mirabelle_HUnion @ A ) ) @ B ) ) ) ) ).
thf(sk129_def,definition,
( sk129
= ( ^ [A: hF_Mirabelle_hf] :
@+[B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk24 @ ( hF_Mirabelle_HUnion @ A ) ) @ B ) ) ) ) ).
thf(sk148_def,definition,
( sk148
= ( @+[A: hF_Mirabelle_hf] :
~ ! [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ A @ B ) @ ( hF_Mir165288108strict @ r @ x ) )
=> ! [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ A @ C ) @ ( hF_Mir165288108strict @ r @ x ) )
=> ( B = C ) ) ) ) ) ).
thf(sk149_def,definition,
( sk149
= ( @+[A: hF_Mirabelle_hf] :
~ ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ A ) @ ( hF_Mir165288108strict @ r @ x ) )
=> ! [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ B ) @ ( hF_Mir165288108strict @ r @ x ) )
=> ( A = B ) ) ) ) ) ).
thf(sk150_def,definition,
( sk150
= ( @+[A: hF_Mirabelle_hf] :
~ ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ A ) @ ( hF_Mir165288108strict @ r @ x ) )
=> ( sk149 = A ) ) ) ) ).
thf(4,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,C: hF_Mirabelle_hf] :
( ! [D: hF_Mirabelle_hf,E: hF_Mirabelle_hf,F: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
=> ( ( B @ D @ E )
=> ( ( B @ D @ F )
=> ( F = E ) ) ) )
=> ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_PrimReplace__iff) ).
thf(37,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,C: hF_Mirabelle_hf] :
( ! [D: hF_Mirabelle_hf,E: hF_Mirabelle_hf,F: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
=> ( ( B @ D @ E )
=> ( ( B @ D @ F )
=> ( F = E ) ) ) )
=> ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(10,axiom,
( hF_Mir796903520_hpair
= ( ^ [A: hF_Mirabelle_hf] :
? [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( A
= ( hF_Mirabelle_hpair @ B @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_is__hpair__def) ).
thf(69,plain,
( hF_Mir796903520_hpair
= ( ^ [A: hF_Mirabelle_hf] :
? [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( A
= ( hF_Mirabelle_hpair @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(18,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_RepFun @ B @ C ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ B )
& ( A
= ( C @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_RepFun__iff) ).
thf(101,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_RepFun @ B @ C ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ B )
& ( A
= ( C @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(5,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,D: hF_Mirabelle_hf > hF_Mirabelle_hf > $o] :
( ( A = B )
=> ( ! [E: hF_Mirabelle_hf,F: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ E @ B )
=> ( ( C @ E @ F )
= ( D @ E @ F ) ) )
=> ( ( hF_Mirabelle_Replace @ A @ C )
= ( hF_Mirabelle_Replace @ B @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_Replace__cong) ).
thf(48,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,D: hF_Mirabelle_hf > hF_Mirabelle_hf > $o] :
( ( A = B )
=> ( ! [E: hF_Mirabelle_hf,F: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ E @ B )
=> ( ( C @ E @ F )
= ( D @ E @ F ) ) )
=> ( ( hF_Mirabelle_Replace @ A @ C )
= ( hF_Mirabelle_Replace @ B @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(49,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( A = B )
=> ! [C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,D: hF_Mirabelle_hf > hF_Mirabelle_hf > $o] :
( ! [E: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ E @ B )
=> ! [F: hF_Mirabelle_hf] :
( ( C @ E @ F )
= ( D @ E @ F ) ) )
=> ( ( hF_Mirabelle_Replace @ A @ C )
= ( hF_Mirabelle_Replace @ B @ D ) ) ) ),
inference(miniscope,[status(thm)],[48]) ).
thf(50,plain,
! [D: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( A != B )
| ( hF_Mirabelle_hmem @ ( sk4 @ D @ C @ B @ A ) @ B )
| ( ( hF_Mirabelle_Replace @ A @ C )
= ( hF_Mirabelle_Replace @ B @ D ) ) )
& ( ( A != B )
| ( ( C @ ( sk4 @ D @ C @ B @ A ) @ ( sk5 @ D @ C @ B @ A ) )
!= ( D @ ( sk4 @ D @ C @ B @ A ) @ ( sk5 @ D @ C @ B @ A ) ) )
| ( ( hF_Mirabelle_Replace @ A @ C )
= ( hF_Mirabelle_Replace @ B @ D ) ) ) ),
inference(cnf,[status(esa)],[49]) ).
thf(51,plain,
! [D: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( A != B )
| ( hF_Mirabelle_hmem @ ( sk4 @ D @ C @ B @ A ) @ B )
| ( ( hF_Mirabelle_Replace @ A @ C )
= ( hF_Mirabelle_Replace @ B @ D ) ) ),
inference(cnfConj,[status(thm)],[50]) ).
thf(53,plain,
! [D: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( A != B )
| ( ( hF_Mirabelle_Replace @ A @ C )
= ( hF_Mirabelle_Replace @ B @ D ) )
| ( hF_Mirabelle_hmem @ ( sk4 @ D @ C @ B @ A ) @ B ) ),
inference(lifteq,[status(thm)],[51]) ).
thf(54,plain,
! [C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_Replace @ A @ B )
= ( hF_Mirabelle_Replace @ A @ C ) )
| ( hF_Mirabelle_hmem @ ( sk4 @ C @ B @ A @ A ) @ A ) ),
inference(simp,[status(thm)],[53]) ).
thf(38,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o] :
( ! [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ A )
=> ! [D: hF_Mirabelle_hf] :
( ( B @ C @ D )
=> ! [E: hF_Mirabelle_hf] :
( ( B @ C @ E )
=> ( E = D ) ) ) )
=> ! [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) ) ),
inference(miniscope,[status(thm)],[37]) ).
thf(39,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hmem @ ( sk1 @ B @ A ) @ A )
| ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) ) )
& ( ( B @ ( sk1 @ B @ A ) @ ( sk2 @ B @ A ) )
| ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) ) )
& ( ( B @ ( sk1 @ B @ A ) @ ( sk3 @ B @ A ) )
| ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) ) )
& ( ( ( sk3 @ B @ A )
!= ( sk2 @ B @ A ) )
| ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) ) ) ),
inference(cnf,[status(esa)],[38]) ).
thf(41,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( B @ ( sk1 @ B @ A ) @ ( sk2 @ B @ A ) )
| ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(45,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) )
| ( B @ ( sk1 @ B @ A ) @ ( sk2 @ B @ A ) ) ),
inference(lifteq,[status(thm)],[41]) ).
thf(430,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hmem @ B
@ ( hF_Mir569462966eplace @ A
@ ^ [C: hF_Mirabelle_hf,D: hF_Mirabelle_hf] : $false ) )
= ( ? [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ A )
& $false ) ) )
| $false ),
inference(prim_subst,[status(thm)],[45:[bind(A,$thf( A )),bind(B,$thf( ^ [D: hF_Mirabelle_hf] : ^ [E: hF_Mirabelle_hf] : $false ))]]) ).
thf(534,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ B
@ ( hF_Mir569462966eplace @ A
@ ^ [C: hF_Mirabelle_hf,D: hF_Mirabelle_hf] : $false ) ),
inference(simp,[status(thm)],[430]) ).
thf(2383,plain,
! [E: hF_Mirabelle_hf,D: hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_Replace @ A @ B )
= ( hF_Mirabelle_Replace @ A @ C ) )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( sk4 @ C @ B @ A @ A ) @ A )
!= ( hF_Mirabelle_hmem @ E
@ ( hF_Mir569462966eplace @ D
@ ^ [F: hF_Mirabelle_hf,G: hF_Mirabelle_hf] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[54,534]) ).
thf(2384,plain,
! [E: hF_Mirabelle_hf,D: hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_Replace @ A @ B )
= ( hF_Mirabelle_Replace @ A @ C ) )
| ( ( hF_Mirabelle_hmem @ ( sk4 @ C @ B @ A @ A ) @ A )
!= ( hF_Mirabelle_hmem @ E
@ ( hF_Mir569462966eplace @ D
@ ^ [F: hF_Mirabelle_hf,G: hF_Mirabelle_hf] : $false ) ) ) ),
inference(simp,[status(thm)],[2383]) ).
thf(2385,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf > hF_Mirabelle_hf > $o] :
( ( hF_Mirabelle_Replace
@ ( hF_Mir569462966eplace @ C
@ ^ [D: hF_Mirabelle_hf,E: hF_Mirabelle_hf] : $false )
@ B )
= ( hF_Mirabelle_Replace
@ ( hF_Mir569462966eplace @ C
@ ^ [D: hF_Mirabelle_hf,E: hF_Mirabelle_hf] : $false )
@ A ) ),
inference(pattern_uni,[status(thm)],[2384:[bind(A,$thf( hF_Mir569462966eplace @ J @ ^ [G: hF_Mirabelle_hf] : ^ [H: hF_Mirabelle_hf] : $false )),bind(B,$thf( G )),bind(C,$thf( F )),bind(D,$thf( J )),bind(E,$thf( sk4 @ F @ G @ ( hF_Mir569462966eplace @ J @ ^ [I: hF_Mirabelle_hf] : ^ [J: hF_Mirabelle_hf] : $false ) @ ( hF_Mir569462966eplace @ J @ ^ [I: hF_Mirabelle_hf] : ^ [J: hF_Mirabelle_hf] : $false ) ))]]) ).
thf(2480,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf > hF_Mirabelle_hf > $o] :
( ( hF_Mirabelle_Replace
@ ( hF_Mir569462966eplace @ C
@ ^ [D: hF_Mirabelle_hf,E: hF_Mirabelle_hf] : $false )
@ B )
= ( hF_Mirabelle_Replace
@ ( hF_Mir569462966eplace @ C
@ ^ [D: hF_Mirabelle_hf,E: hF_Mirabelle_hf] : $false )
@ A ) ),
inference(simp,[status(thm)],[2385]) ).
thf(16,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf,D: hF_Mirabelle_hf > hF_Mirabelle_hf] :
( ( A = B )
=> ( ! [E: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ E @ B )
=> ( ( C @ E )
= ( D @ E ) ) )
=> ( ( hF_Mirabelle_RepFun @ A @ C )
= ( hF_Mirabelle_RepFun @ B @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_RepFun__cong) ).
thf(88,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf,D: hF_Mirabelle_hf > hF_Mirabelle_hf] :
( ( A = B )
=> ( ! [E: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ E @ B )
=> ( ( C @ E )
= ( D @ E ) ) )
=> ( ( hF_Mirabelle_RepFun @ A @ C )
= ( hF_Mirabelle_RepFun @ B @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(32,axiom,
( hF_Mir859708136nction
= ( ^ [A: hF_Mirabelle_hf] :
! [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ B @ C ) @ A )
=> ! [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ B @ D ) @ A )
=> ( C = D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_hfunction__def) ).
thf(157,plain,
( hF_Mir859708136nction
= ( ^ [A: hF_Mirabelle_hf] :
! [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ B @ C ) @ A )
=> ! [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ B @ D ) @ A )
=> ( C = D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(158,plain,
( hF_Mir859708136nction
= ( ^ [A: hF_Mirabelle_hf] :
! [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ B @ C ) @ A )
=> ! [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ B @ D ) @ A )
=> ( C = D ) ) ) ) ),
inference(lifteq,[status(thm)],[157]) ).
thf(203,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir859708136nction @ A )
= ( ! [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ B @ C ) @ A )
=> ! [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ B @ D ) @ A )
=> ( C = D ) ) ) ) ),
inference(func_ext,[status(esa)],[158]) ).
thf(1,conjecture,
hF_Mir859708136nction @ ( hF_Mir165288108strict @ r @ x ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
thf(2,negated_conjecture,
~ ( hF_Mir859708136nction @ ( hF_Mir165288108strict @ r @ x ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(34,plain,
~ ( hF_Mir859708136nction @ ( hF_Mir165288108strict @ r @ x ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(2830,plain,
! [A: hF_Mirabelle_hf] :
( ~ ! [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ B @ C ) @ A )
=> ! [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ B @ D ) @ A )
=> ( C = D ) ) )
| ( ( hF_Mir859708136nction @ A )
!= ( hF_Mir859708136nction @ ( hF_Mir165288108strict @ r @ x ) ) ) ),
inference(paramod_ordered,[status(thm)],[203,34]) ).
thf(2831,plain,
~ ! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ A @ B ) @ ( hF_Mir165288108strict @ r @ x ) )
=> ! [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ A @ C ) @ ( hF_Mir165288108strict @ r @ x ) )
=> ( B = C ) ) ),
inference(pattern_uni,[status(thm)],[2830:[bind(A,$thf( hF_Mir165288108strict @ r @ x ))]]) ).
thf(2894,plain,
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
& ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
& ( sk149 != sk150 ) ),
inference(cnf,[status(esa)],[2831]) ).
thf(2895,plain,
hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ),
inference(cnfConj,[status(thm)],[2894]) ).
thf(12,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
? [C: hF_Mirabelle_hf] :
! [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ C )
= ( ( hF_Mirabelle_hmem @ D @ A )
| ( hF_Mirabelle_hmem @ D @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_binary__union) ).
thf(74,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
? [C: hF_Mirabelle_hf] :
! [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ C )
= ( ( hF_Mirabelle_hmem @ D @ A )
| ( hF_Mirabelle_hmem @ D @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(75,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ ( sk6 @ B @ A ) )
= ( ( hF_Mirabelle_hmem @ C @ A )
| ( hF_Mirabelle_hmem @ C @ B ) ) ),
inference(cnf,[status(esa)],[74]) ).
thf(76,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ ( sk6 @ B @ A ) )
= ( ( hF_Mirabelle_hmem @ C @ A )
| ( hF_Mirabelle_hmem @ C @ B ) ) ),
inference(lifteq,[status(thm)],[75]) ).
thf(20,axiom,
! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_hmem__not__refl) ).
thf(107,plain,
! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(108,plain,
~ ? [A: hF_Mirabelle_hf] : ( hF_Mirabelle_hmem @ A @ A ),
inference(miniscope,[status(thm)],[107]) ).
thf(109,plain,
! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ A ),
inference(cnf,[status(esa)],[108]) ).
thf(5884,plain,
! [D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( ( hF_Mirabelle_hmem @ C @ A )
| ( hF_Mirabelle_hmem @ C @ B ) )
| ( ( hF_Mirabelle_hmem @ C @ ( sk6 @ B @ A ) )
!= ( hF_Mirabelle_hmem @ D @ D ) ) ),
inference(paramod_ordered,[status(thm)],[76,109]) ).
thf(5885,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ B )
| ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ A ) ),
inference(pattern_uni,[status(thm)],[5884:[bind(A,$thf( F )),bind(B,$thf( E )),bind(C,$thf( sk6 @ E @ F )),bind(D,$thf( sk6 @ E @ F ))]]) ).
thf(6205,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ B )
& ~ ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ A ) ),
inference(cnf,[status(esa)],[5885]) ).
thf(6206,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ B ),
inference(cnfConj,[status(thm)],[6205]) ).
thf(6208,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ B ),
inference(simp,[status(thm)],[6206]) ).
thf(6257,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[2895,6208]) ).
thf(6258,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ B ) ),
inference(simp,[status(thm)],[6257]) ).
thf(6309,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( sk6 @ A @ B )
!= ( hF_Mirabelle_hpair @ sk148 @ sk149 ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= B ) ),
inference(simp,[status(thm)],[6258]) ).
thf(6338,plain,
! [A: hF_Mirabelle_hf] :
( ( sk6 @ A @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ),
inference(simp,[status(thm)],[6309]) ).
thf(22,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ B )
=> ( A != B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_hmem__ne) ).
thf(120,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ B )
=> ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(52,plain,
! [D: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( A != B )
| ( ( C @ ( sk4 @ D @ C @ B @ A ) @ ( sk5 @ D @ C @ B @ A ) )
!= ( D @ ( sk4 @ D @ C @ B @ A ) @ ( sk5 @ D @ C @ B @ A ) ) )
| ( ( hF_Mirabelle_Replace @ A @ C )
= ( hF_Mirabelle_Replace @ B @ D ) ) ),
inference(cnfConj,[status(thm)],[50]) ).
thf(55,plain,
! [D: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( A != B )
| ( ( C @ ( sk4 @ D @ C @ B @ A ) @ ( sk5 @ D @ C @ B @ A ) )
!= ( D @ ( sk4 @ D @ C @ B @ A ) @ ( sk5 @ D @ C @ B @ A ) ) )
| ( ( hF_Mirabelle_Replace @ A @ C )
= ( hF_Mirabelle_Replace @ B @ D ) ) ),
inference(lifteq,[status(thm)],[52]) ).
thf(56,plain,
! [C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( B @ ( sk4 @ C @ B @ A @ A ) @ ( sk5 @ C @ B @ A @ A ) )
!= ( C @ ( sk4 @ C @ B @ A @ A ) @ ( sk5 @ C @ B @ A @ A ) ) )
| ( ( hF_Mirabelle_Replace @ A @ B )
= ( hF_Mirabelle_Replace @ A @ C ) ) ),
inference(simp,[status(thm)],[55]) ).
thf(30,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] : ( hF_Mir1093797708lation @ ( hF_Mir165288108strict @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_hrelation__restr) ).
thf(152,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] : ( hF_Mir1093797708lation @ ( hF_Mir165288108strict @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(153,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] : ( hF_Mir1093797708lation @ ( hF_Mir165288108strict @ A @ B ) ),
inference(cnf,[status(esa)],[152]) ).
thf(21,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf,D: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ A @ B )
= ( hF_Mirabelle_hpair @ C @ D ) )
=> ~ ( ( A = C )
=> ( B != D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_hpair__inject) ).
thf(110,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf,D: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ A @ B )
= ( hF_Mirabelle_hpair @ C @ D ) )
=> ~ ( ( A = C )
=> ( B != D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(15,axiom,
! [A: hF_Mirabelle_hf] :
? [B: hF_Mirabelle_hf] :
! [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ B )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( hF_Mirabelle_hmem @ C @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_union__of__set) ).
thf(85,plain,
! [A: hF_Mirabelle_hf] :
? [B: hF_Mirabelle_hf] :
! [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ B )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( hF_Mirabelle_hmem @ C @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(86,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ ( sk7 @ A ) )
= ( ? [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ A )
& ( hF_Mirabelle_hmem @ B @ C ) ) ) ),
inference(cnf,[status(esa)],[85]) ).
thf(87,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ ( sk7 @ A ) )
= ( ? [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ A )
& ( hF_Mirabelle_hmem @ B @ C ) ) ) ),
inference(lifteq,[status(thm)],[86]) ).
thf(1663,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( hF_Mirabelle_hmem @ B @ D ) )
| ( ( hF_Mirabelle_hmem @ B @ ( sk7 @ A ) )
!= ( hF_Mirabelle_hmem @ C @ C ) ) ),
inference(paramod_ordered,[status(thm)],[87,109]) ).
thf(1664,plain,
! [A: hF_Mirabelle_hf] :
~ ? [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ B ) ),
inference(pattern_uni,[status(thm)],[1663:[bind(A,$thf( D )),bind(B,$thf( sk7 @ D )),bind(C,$thf( sk7 @ D ))]]) ).
thf(1762,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ~ ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ B ) ),
inference(cnf,[status(esa)],[1664]) ).
thf(1763,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ~ ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ B ) ),
inference(simp,[status(thm)],[1762]) ).
thf(3002,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[2895,1763]) ).
thf(3003,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ B ) ) ),
inference(simp,[status(thm)],[3002]) ).
thf(3030,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ( ( hF_Mirabelle_hpair @ sk148 @ sk149 )
!= ( sk7 @ A ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= B ) ),
inference(simp,[status(thm)],[3003]) ).
thf(3099,plain,
! [A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ A )
| ( ( hF_Mirabelle_hpair @ sk148 @ sk149 )
!= ( sk7 @ A ) ) ),
inference(simp,[status(thm)],[3030]) ).
thf(42,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( B @ ( sk1 @ B @ A ) @ ( sk3 @ B @ A ) )
| ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(46,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) )
| ( B @ ( sk1 @ B @ A ) @ ( sk3 @ B @ A ) ) ),
inference(lifteq,[status(thm)],[42]) ).
thf(6,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_HUnion @ B ) )
= ( ? [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ B )
& ( hF_Mirabelle_hmem @ A @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_HUnion__iff) ).
thf(57,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_HUnion @ B ) )
= ( ? [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ B )
& ( hF_Mirabelle_hmem @ A @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(3,axiom,
( hF_Mir1093797708lation
= ( ^ [A: hF_Mirabelle_hf] :
! [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
=> ( hF_Mir796903520_hpair @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_hrelation__def) ).
thf(35,plain,
( hF_Mir1093797708lation
= ( ^ [A: hF_Mirabelle_hf] :
! [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
=> ( hF_Mir796903520_hpair @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(36,plain,
( hF_Mir1093797708lation
= ( ^ [A: hF_Mirabelle_hf] :
! [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
=> ( hF_Mir796903520_hpair @ B ) ) ) ),
inference(lifteq,[status(thm)],[35]) ).
thf(163,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
= ( ! [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
=> ( hF_Mir796903520_hpair @ B ) ) ) ),
inference(func_ext,[status(esa)],[36]) ).
thf(345,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ~ ! [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
=> ( hF_Mir796903520_hpair @ B ) ) ),
inference(bool_ext,[status(thm)],[163]) ).
thf(361,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mir1093797708lation @ A )
| ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A ) )
& ( ( hF_Mir1093797708lation @ A )
| ~ ( hF_Mir796903520_hpair @ ( sk24 @ A ) ) ) ),
inference(cnf,[status(esa)],[345]) ).
thf(362,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A ) ),
inference(cnfConj,[status(thm)],[361]) ).
thf(58,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_HUnion @ B ) )
= ( ? [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ B )
& ( hF_Mirabelle_hmem @ A @ C ) ) ) ),
inference(cnf,[status(esa)],[57]) ).
thf(59,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_HUnion @ B ) )
= ( ? [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ B )
& ( hF_Mirabelle_hmem @ A @ C ) ) ) ),
inference(lifteq,[status(thm)],[58]) ).
thf(1316,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ C )
& ( hF_Mirabelle_hmem @ B @ D ) )
| ( ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ B @ ( hF_Mirabelle_HUnion @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[362,59]) ).
thf(1317,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ? [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk24 @ ( hF_Mirabelle_HUnion @ A ) ) @ B ) ) ),
inference(pattern_uni,[status(thm)],[1316:[bind(A,$thf( hF_Mirabelle_HUnion @ E )),bind(B,$thf( sk24 @ ( hF_Mirabelle_HUnion @ E ) )),bind(C,$thf( E ))]]) ).
thf(1426,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk77 @ A ) @ A ) )
& ( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk24 @ ( hF_Mirabelle_HUnion @ A ) ) @ ( sk77 @ A ) ) ) ),
inference(cnf,[status(esa)],[1317]) ).
thf(1427,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk77 @ A ) @ A ) ),
inference(cnfConj,[status(thm)],[1426]) ).
thf(1429,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk77 @ A ) @ A ) ),
inference(simp,[status(thm)],[1427]) ).
thf(2896,plain,
hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ),
inference(cnfConj,[status(thm)],[2894]) ).
thf(8,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
~ ( ( hF_Mirabelle_hmem @ A @ B )
& ( hF_Mirabelle_hmem @ B @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_hmem__not__sym) ).
thf(63,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
~ ( ( hF_Mirabelle_hmem @ A @ B )
& ( hF_Mirabelle_hmem @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(64,plain,
~ ? [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ B )
& ( hF_Mirabelle_hmem @ B @ A ) ),
inference(miniscope,[status(thm)],[63]) ).
thf(65,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ A @ B )
| ~ ( hF_Mirabelle_hmem @ B @ A ) ),
inference(cnf,[status(esa)],[64]) ).
thf(3120,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ~ ( hF_Mirabelle_hmem @ B @ A )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[2896,65]) ).
thf(3121,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ A @ B ) ) ),
inference(simp,[status(thm)],[3120]) ).
thf(3122,plain,
~ ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ),
inference(pattern_uni,[status(thm)],[3121:[bind(A,$thf( hF_Mirabelle_hpair @ sk148 @ sk150 )),bind(B,$thf( hF_Mir165288108strict @ r @ x ))]]) ).
thf(3457,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( sk77 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) ) ),
inference(paramod_ordered,[status(thm)],[1429,3122]) ).
thf(3458,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( ( hF_Mirabelle_hmem @ ( sk77 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) ) ),
inference(simp,[status(thm)],[3457]) ).
thf(3519,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( ( sk77 @ A )
!= ( hF_Mir165288108strict @ r @ x ) )
| ( A
!= ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) ),
inference(simp,[status(thm)],[3458]) ).
thf(3602,plain,
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= ( sk77 @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) ) ),
inference(simp,[status(thm)],[3519]) ).
thf(6280,plain,
! [E: hF_Mirabelle_hf,D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( ( hF_Mirabelle_hmem @ C @ A )
| ( hF_Mirabelle_hmem @ C @ B ) )
| ( ( hF_Mirabelle_hmem @ C @ ( sk6 @ B @ A ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ D @ E ) @ E ) ) ),
inference(paramod_ordered,[status(thm)],[76,6208]) ).
thf(6281,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ C )
| ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ B ) ),
inference(pattern_uni,[status(thm)],[6280:[bind(A,$thf( I )),bind(B,$thf( H )),bind(C,$thf( sk6 @ F @ ( sk6 @ H @ I ) )),bind(D,$thf( F )),bind(E,$thf( sk6 @ H @ I ))]]) ).
thf(6315,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ C )
& ~ ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ B ) ),
inference(cnf,[status(esa)],[6281]) ).
thf(6317,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ B ),
inference(cnfConj,[status(thm)],[6315]) ).
thf(6319,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ B ),
inference(simp,[status(thm)],[6317]) ).
thf(8791,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[2895,6319]) ).
thf(8792,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ B ) ),
inference(simp,[status(thm)],[8791]) ).
thf(8844,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( sk6 @ A @ ( sk6 @ B @ C ) )
!= ( hF_Mirabelle_hpair @ sk148 @ sk149 ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= B ) ),
inference(simp,[status(thm)],[8792]) ).
thf(8870,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( sk6 @ A @ ( sk6 @ ( hF_Mir165288108strict @ r @ x ) @ B ) )
!= ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ),
inference(simp,[status(thm)],[8844]) ).
thf(70,plain,
( hF_Mir796903520_hpair
= ( ^ [A: hF_Mirabelle_hf] :
? [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( A
= ( hF_Mirabelle_hpair @ B @ C ) ) ) ),
inference(lifteq,[status(thm)],[69]) ).
thf(164,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir796903520_hpair @ A )
= ( ? [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( A
= ( hF_Mirabelle_hpair @ B @ C ) ) ) ),
inference(func_ext,[status(esa)],[70]) ).
thf(33,axiom,
hF_Mir859708136nction @ r,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(159,plain,
hF_Mir859708136nction @ r,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(7,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf > $o,C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mir1687042746ollect @ B @ C ) )
= ( ( B @ A )
& ( hF_Mirabelle_hmem @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_HCollect__iff) ).
thf(60,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf > $o,C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mir1687042746ollect @ B @ C ) )
= ( ( B @ A )
& ( hF_Mirabelle_hmem @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(61,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mir1687042746ollect @ B @ C ) )
= ( ( B @ A )
& ( hF_Mirabelle_hmem @ A @ C ) ) ),
inference(cnf,[status(esa)],[60]) ).
thf(62,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mir1687042746ollect @ B @ C ) )
= ( ( B @ A )
& ( hF_Mirabelle_hmem @ A @ C ) ) ),
inference(lifteq,[status(thm)],[61]) ).
thf(3720,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hmem @ A @ ( hF_Mir1687042746ollect @ B @ C ) )
= ( $true
& ( hF_Mirabelle_hmem @ A @ C ) ) )
| ( ( hF_Mir859708136nction @ r )
!= ( B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[159,62]) ).
thf(3721,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hmem @ A @ ( hF_Mir1687042746ollect @ B @ C ) )
= ( hF_Mirabelle_hmem @ A @ C ) )
| ( ( hF_Mir859708136nction @ r )
!= ( B @ A ) ) ),
inference(simp,[status(thm)],[3720]) ).
thf(3918,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ r @ ( hF_Mir1687042746ollect @ hF_Mir859708136nction @ A ) )
= ( hF_Mirabelle_hmem @ r @ A ) ),
inference(pre_uni,[status(thm)],[3721:[bind(A,$thf( r )),bind(B,$thf( hF_Mir859708136nction )),bind(C,$thf( C ))]]) ).
thf(4050,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ r @ ( hF_Mir1687042746ollect @ hF_Mir859708136nction @ A ) )
= ( hF_Mirabelle_hmem @ r @ A ) ),
inference(simp,[status(thm)],[3918]) ).
thf(14,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ B )
=> ( ( hF_Mirabelle_HUnion @ A )
!= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_hmem__Sup__ne) ).
thf(81,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ B )
=> ( ( hF_Mirabelle_HUnion @ A )
!= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(82,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ A @ B )
| ( ( hF_Mirabelle_HUnion @ A )
!= B ) ),
inference(cnf,[status(esa)],[81]) ).
thf(83,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_HUnion @ A )
!= B )
| ~ ( hF_Mirabelle_hmem @ A @ B ) ),
inference(lifteq,[status(thm)],[82]) ).
thf(84,plain,
! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_HUnion @ A ) ),
inference(simp,[status(thm)],[83]) ).
thf(3150,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ~ ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ B )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2896,1763]) ).
thf(3151,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ B )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ B @ A ) ) ),
inference(simp,[status(thm)],[3150]) ).
thf(3152,plain,
~ ( hF_Mirabelle_hmem @ ( sk7 @ ( hF_Mir165288108strict @ r @ x ) ) @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ),
inference(pattern_uni,[status(thm)],[3151:[bind(A,$thf( hF_Mir165288108strict @ r @ x )),bind(B,$thf( hF_Mirabelle_hpair @ sk148 @ sk150 ))]]) ).
thf(1288,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ B )
& ( hF_Mirabelle_hmem @ A @ D ) )
| ( ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_HUnion @ B ) )
!= ( hF_Mirabelle_hmem @ C @ C ) ) ),
inference(paramod_ordered,[status(thm)],[59,109]) ).
thf(1289,plain,
! [A: hF_Mirabelle_hf] :
~ ? [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ A ) @ B ) ),
inference(pattern_uni,[status(thm)],[1288:[bind(A,$thf( hF_Mirabelle_HUnion @ D )),bind(B,$thf( D )),bind(C,$thf( hF_Mirabelle_HUnion @ D ))]]) ).
thf(1380,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ~ ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ A ) @ B ) ),
inference(cnf,[status(esa)],[1289]) ).
thf(1381,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ~ ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ A ) @ B ) ),
inference(simp,[status(thm)],[1380]) ).
thf(2962,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ~ ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ A ) @ B )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2895,1381]) ).
thf(2963,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ A ) @ B )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ B @ A ) ) ),
inference(simp,[status(thm)],[2962]) ).
thf(2964,plain,
~ ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ ( hF_Mir165288108strict @ r @ x ) ) @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ),
inference(pattern_uni,[status(thm)],[2963:[bind(A,$thf( hF_Mir165288108strict @ r @ x )),bind(B,$thf( hF_Mirabelle_hpair @ sk148 @ sk149 ))]]) ).
thf(26,axiom,
( ( (=) @ hF_Mirabelle_hf )
= ( ^ [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
! [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ A )
= ( hF_Mirabelle_hmem @ C @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_hf__ext) ).
thf(133,plain,
( ( (=) @ hF_Mirabelle_hf )
= ( ^ [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
! [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ A )
= ( hF_Mirabelle_hmem @ C @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(1694,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ C )
| ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( hF_Mirabelle_hmem @ B @ D ) )
| ( ( hF_Mirabelle_hmem @ B @ ( sk7 @ A ) )
!= ( hF_Mirabelle_hmem @ ( sk24 @ C ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[87,362]) ).
thf(1695,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( sk7 @ A ) )
| ? [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk24 @ ( sk7 @ A ) ) @ B ) ) ),
inference(pattern_uni,[status(thm)],[1694:[bind(A,$thf( E )),bind(B,$thf( sk24 @ ( sk7 @ E ) )),bind(C,$thf( sk7 @ E ))]]) ).
thf(1778,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mir1093797708lation @ ( sk7 @ A ) )
| ( hF_Mirabelle_hmem @ ( sk95 @ A ) @ A ) )
& ( ( hF_Mir1093797708lation @ ( sk7 @ A ) )
| ( hF_Mirabelle_hmem @ ( sk24 @ ( sk7 @ A ) ) @ ( sk95 @ A ) ) ) ),
inference(cnf,[status(esa)],[1695]) ).
thf(1779,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( sk7 @ A ) )
| ( hF_Mirabelle_hmem @ ( sk95 @ A ) @ A ) ),
inference(cnfConj,[status(thm)],[1778]) ).
thf(1781,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( sk7 @ A ) )
| ( hF_Mirabelle_hmem @ ( sk95 @ A ) @ A ) ),
inference(simp,[status(thm)],[1779]) ).
thf(5537,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( sk7 @ A ) )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( sk95 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ C
@ ( hF_Mir569462966eplace @ B
@ ^ [D: hF_Mirabelle_hf,E: hF_Mirabelle_hf] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[1781,534]) ).
thf(5538,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( sk7 @ A ) )
| ( ( hF_Mirabelle_hmem @ ( sk95 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ C
@ ( hF_Mir569462966eplace @ B
@ ^ [D: hF_Mirabelle_hf,E: hF_Mirabelle_hf] : $false ) ) ) ),
inference(simp,[status(thm)],[5537]) ).
thf(5539,plain,
! [A: hF_Mirabelle_hf] :
( hF_Mir1093797708lation
@ ( sk7
@ ( hF_Mir569462966eplace @ A
@ ^ [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] : $false ) ) ),
inference(pattern_uni,[status(thm)],[5538:[bind(A,$thf( hF_Mir569462966eplace @ E @ ^ [E: hF_Mirabelle_hf] : ^ [F: hF_Mirabelle_hf] : $false )),bind(B,$thf( E )),bind(C,$thf( sk95 @ ( hF_Mir569462966eplace @ E @ ^ [E: hF_Mirabelle_hf] : ^ [F: hF_Mirabelle_hf] : $false ) ))]]) ).
thf(5665,plain,
! [A: hF_Mirabelle_hf] :
( hF_Mir1093797708lation
@ ( sk7
@ ( hF_Mir569462966eplace @ A
@ ^ [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] : $false ) ) ),
inference(simp,[status(thm)],[5539]) ).
thf(6207,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ A ),
inference(cnfConj,[status(thm)],[6205]) ).
thf(6209,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ A ),
inference(simp,[status(thm)],[6207]) ).
thf(7014,plain,
! [E: hF_Mirabelle_hf,D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( ( hF_Mirabelle_hmem @ C @ A )
| ( hF_Mirabelle_hmem @ C @ B ) )
| ( ( hF_Mirabelle_hmem @ C @ ( sk6 @ B @ A ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ D @ E ) @ D ) ) ),
inference(paramod_ordered,[status(thm)],[76,6209]) ).
thf(7015,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( ( hF_Mirabelle_hmem @ ( sk6 @ ( sk6 @ B @ C ) @ A ) @ C )
| ( hF_Mirabelle_hmem @ ( sk6 @ ( sk6 @ B @ C ) @ A ) @ B ) ),
inference(pattern_uni,[status(thm)],[7014:[bind(A,$thf( I )),bind(B,$thf( H )),bind(C,$thf( sk6 @ ( sk6 @ H @ I ) @ G )),bind(D,$thf( sk6 @ H @ I )),bind(E,$thf( G ))]]) ).
thf(7075,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ ( sk6 @ ( sk6 @ B @ C ) @ A ) @ C )
& ~ ( hF_Mirabelle_hmem @ ( sk6 @ ( sk6 @ B @ C ) @ A ) @ B ) ),
inference(cnf,[status(esa)],[7015]) ).
thf(7076,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk6 @ ( sk6 @ B @ C ) @ A ) @ C ),
inference(cnfConj,[status(thm)],[7075]) ).
thf(7078,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk6 @ ( sk6 @ B @ C ) @ A ) @ C ),
inference(simp,[status(thm)],[7076]) ).
thf(2975,plain,
! [A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2895,109]) ).
thf(2976,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ A @ A ) ),
inference(simp,[status(thm)],[2975]) ).
thf(3008,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ sk148 @ sk149 )
!= A )
| ( ( hF_Mir165288108strict @ r @ x )
!= A ) ),
inference(simp,[status(thm)],[2976]) ).
thf(3037,plain,
( ( hF_Mir165288108strict @ r @ x )
!= ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ),
inference(simp,[status(thm)],[3008]) ).
thf(2969,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ~ ( hF_Mirabelle_hmem @ B @ A )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[2895,65]) ).
thf(2970,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ A @ B ) ) ),
inference(simp,[status(thm)],[2969]) ).
thf(2971,plain,
~ ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ),
inference(pattern_uni,[status(thm)],[2970:[bind(A,$thf( hF_Mirabelle_hpair @ sk148 @ sk149 )),bind(B,$thf( hF_Mir165288108strict @ r @ x ))]]) ).
thf(3327,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) ) ),
inference(paramod_ordered,[status(thm)],[362,2971]) ).
thf(3328,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ( ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) ) ),
inference(simp,[status(thm)],[3327]) ).
thf(3350,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ( ( sk24 @ A )
!= ( hF_Mir165288108strict @ r @ x ) )
| ( A
!= ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) ),
inference(simp,[status(thm)],[3328]) ).
thf(3371,plain,
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= ( sk24 @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) ) ),
inference(simp,[status(thm)],[3350]) ).
thf(134,plain,
( ( (=) @ hF_Mirabelle_hf )
= ( ^ [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
! [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ A )
= ( hF_Mirabelle_hmem @ C @ B ) ) ) ),
inference(lifteq,[status(thm)],[133]) ).
thf(165,plain,
! [A: hF_Mirabelle_hf] :
( ( (=) @ hF_Mirabelle_hf @ A )
= ( ^ [B: hF_Mirabelle_hf] :
! [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ A )
= ( hF_Mirabelle_hmem @ C @ B ) ) ) ),
inference(func_ext,[status(esa)],[134]) ).
thf(111,plain,
! [D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( ( hF_Mirabelle_hpair @ A @ B )
!= ( hF_Mirabelle_hpair @ C @ D ) )
| ( A = C ) )
& ( ( ( hF_Mirabelle_hpair @ A @ B )
!= ( hF_Mirabelle_hpair @ C @ D ) )
| ( B = D ) ) ),
inference(cnf,[status(esa)],[110]) ).
thf(112,plain,
! [D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ A @ B )
!= ( hF_Mirabelle_hpair @ C @ D ) )
| ( A = C ) ),
inference(cnfConj,[status(thm)],[111]) ).
thf(114,plain,
! [D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ A @ B )
!= ( hF_Mirabelle_hpair @ C @ D ) )
| ( A = C ) ),
inference(lifteq,[status(thm)],[112]) ).
thf(115,plain,
? [A: hF_Mirabelle_hf > hF_Mirabelle_hf > hF_Mirabelle_hf] :
! [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( ( A @ C @ ( hF_Mirabelle_hpair @ B @ C ) )
= B ),
inference(detectInverse,[status(thm)],[114]) ).
thf(116,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( sk10 @ B @ ( hF_Mirabelle_hpair @ A @ B ) )
= A ),
inference(cnf,[status(esa)],[115]) ).
thf(1032,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( sk10 @ B @ ( hF_Mirabelle_hpair @ A @ B ) )
= A ),
inference(lifteq,[status(thm)],[116]) ).
thf(2965,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ A ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[2895,1381]) ).
thf(2966,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ A ) @ B ) ) ),
inference(simp,[status(thm)],[2965]) ).
thf(3020,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ( ( hF_Mirabelle_hpair @ sk148 @ sk149 )
!= ( hF_Mirabelle_HUnion @ A ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= B ) ),
inference(simp,[status(thm)],[2966]) ).
thf(3065,plain,
! [A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ A )
| ( ( hF_Mirabelle_hpair @ sk148 @ sk149 )
!= ( hF_Mirabelle_HUnion @ A ) ) ),
inference(simp,[status(thm)],[3020]) ).
thf(17,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hpair @ A @ B )
!= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_hpair__neq__snd) ).
thf(97,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hpair @ A @ B )
!= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(3116,plain,
! [A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_HUnion @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[2896,84]) ).
thf(3117,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_HUnion @ A ) ) ),
inference(simp,[status(thm)],[3116]) ).
thf(3186,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ sk148 @ sk150 )
!= A )
| ( ( hF_Mir165288108strict @ r @ x )
!= ( hF_Mirabelle_HUnion @ A ) ) ),
inference(simp,[status(thm)],[3117]) ).
thf(3254,plain,
( ( hF_Mir165288108strict @ r @ x )
!= ( hF_Mirabelle_HUnion @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) ),
inference(simp,[status(thm)],[3186]) ).
thf(2999,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ~ ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ B )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2895,1763]) ).
thf(3000,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ B )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ B @ A ) ) ),
inference(simp,[status(thm)],[2999]) ).
thf(3001,plain,
~ ( hF_Mirabelle_hmem @ ( sk7 @ ( hF_Mir165288108strict @ r @ x ) ) @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ),
inference(pattern_uni,[status(thm)],[3000:[bind(A,$thf( hF_Mir165288108strict @ r @ x )),bind(B,$thf( hF_Mirabelle_hpair @ sk148 @ sk149 ))]]) ).
thf(13,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hpair @ A @ B )
!= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_hpair__neq__fst) ).
thf(77,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hpair @ A @ B )
!= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(1314,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ C )
| ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ B )
& ( hF_Mirabelle_hmem @ A @ D ) )
| ( ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_HUnion @ B ) )
!= ( hF_Mirabelle_hmem @ ( sk24 @ C ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[59,362]) ).
thf(1315,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ? [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk24 @ ( hF_Mirabelle_HUnion @ A ) ) @ B ) ) ),
inference(pattern_uni,[status(thm)],[1314:[bind(A,$thf( sk24 @ ( hF_Mirabelle_HUnion @ E ) )),bind(B,$thf( E )),bind(C,$thf( hF_Mirabelle_HUnion @ E ))]]) ).
thf(1421,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk76 @ A ) @ A ) )
& ( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk24 @ ( hF_Mirabelle_HUnion @ A ) ) @ ( sk76 @ A ) ) ) ),
inference(cnf,[status(esa)],[1315]) ).
thf(1422,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk76 @ A ) @ A ) ),
inference(cnfConj,[status(thm)],[1421]) ).
thf(1424,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk76 @ A ) @ A ) ),
inference(simp,[status(thm)],[1422]) ).
thf(89,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( A = B )
=> ! [C: hF_Mirabelle_hf > hF_Mirabelle_hf,D: hF_Mirabelle_hf > hF_Mirabelle_hf] :
( ! [E: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ E @ B )
=> ( ( C @ E )
= ( D @ E ) ) )
=> ( ( hF_Mirabelle_RepFun @ A @ C )
= ( hF_Mirabelle_RepFun @ B @ D ) ) ) ),
inference(miniscope,[status(thm)],[88]) ).
thf(90,plain,
! [D: hF_Mirabelle_hf > hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( A != B )
| ( hF_Mirabelle_hmem @ ( sk8 @ D @ C @ B @ A ) @ B )
| ( ( hF_Mirabelle_RepFun @ A @ C )
= ( hF_Mirabelle_RepFun @ B @ D ) ) )
& ( ( A != B )
| ( ( C @ ( sk8 @ D @ C @ B @ A ) )
!= ( D @ ( sk8 @ D @ C @ B @ A ) ) )
| ( ( hF_Mirabelle_RepFun @ A @ C )
= ( hF_Mirabelle_RepFun @ B @ D ) ) ) ),
inference(cnf,[status(esa)],[89]) ).
thf(92,plain,
! [D: hF_Mirabelle_hf > hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( A != B )
| ( ( C @ ( sk8 @ D @ C @ B @ A ) )
!= ( D @ ( sk8 @ D @ C @ B @ A ) ) )
| ( ( hF_Mirabelle_RepFun @ A @ C )
= ( hF_Mirabelle_RepFun @ B @ D ) ) ),
inference(cnfConj,[status(thm)],[90]) ).
thf(95,plain,
! [D: hF_Mirabelle_hf > hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( A != B )
| ( ( C @ ( sk8 @ D @ C @ B @ A ) )
!= ( D @ ( sk8 @ D @ C @ B @ A ) ) )
| ( ( hF_Mirabelle_RepFun @ A @ C )
= ( hF_Mirabelle_RepFun @ B @ D ) ) ),
inference(lifteq,[status(thm)],[92]) ).
thf(96,plain,
! [C: hF_Mirabelle_hf > hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( B @ ( sk8 @ C @ B @ A @ A ) )
!= ( C @ ( sk8 @ C @ B @ A @ A ) ) )
| ( ( hF_Mirabelle_RepFun @ A @ B )
= ( hF_Mirabelle_RepFun @ A @ C ) ) ),
inference(simp,[status(thm)],[95]) ).
thf(23,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hfst @ ( hF_Mirabelle_hpair @ A @ B ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_hfst__conv) ).
thf(124,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hfst @ ( hF_Mirabelle_hpair @ A @ B ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(1689,plain,
! [D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hmem @ B @ ( sk7 @ A ) )
= ( hF_Mirabelle_hmem @ C @ ( hF_Mirabelle_HUnion @ D ) ) )
| ( ( ? [E: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ E @ A )
& ( hF_Mirabelle_hmem @ B @ E ) ) )
!= ( ? [E: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ E @ D )
& ( hF_Mirabelle_hmem @ C @ E ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[87,59]) ).
thf(1690,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ ( sk7 @ A ) )
= ( hF_Mirabelle_hmem @ B @ ( hF_Mirabelle_HUnion @ A ) ) ),
inference(pattern_uni,[status(thm)],[1689:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(1874,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ ( hF_Mirabelle_HUnion @ A ) )
| ( ( hF_Mirabelle_hmem @ B @ ( sk7 @ A ) )
!= ( hF_Mirabelle_hmem @ C @ C ) ) ),
inference(paramod_ordered,[status(thm)],[1690,109]) ).
thf(1875,plain,
! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ ( hF_Mirabelle_HUnion @ A ) ),
inference(pattern_uni,[status(thm)],[1874:[bind(A,$thf( D )),bind(B,$thf( sk7 @ D )),bind(C,$thf( sk7 @ D ))]]) ).
thf(1942,plain,
! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ ( hF_Mirabelle_HUnion @ A ) ),
inference(simp,[status(thm)],[1875]) ).
thf(2960,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ B
@ ( hF_Mir569462966eplace @ A
@ ^ [C: hF_Mirabelle_hf,D: hF_Mirabelle_hf] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[2895,534]) ).
thf(2961,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ B
@ ( hF_Mir569462966eplace @ A
@ ^ [C: hF_Mirabelle_hf,D: hF_Mirabelle_hf] : $false ) ) ),
inference(simp,[status(thm)],[2960]) ).
thf(3019,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ sk148 @ sk149 )
!= B )
| ( ( hF_Mir165288108strict @ r @ x )
!= ( hF_Mir569462966eplace @ A
@ ^ [C: hF_Mirabelle_hf,D: hF_Mirabelle_hf] : $false ) ) ),
inference(simp,[status(thm)],[2961]) ).
thf(3064,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir165288108strict @ r @ x )
!= ( hF_Mir569462966eplace @ A
@ ^ [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] : $false ) ),
inference(simp,[status(thm)],[3019]) ).
thf(11,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_Replace @ B @ C ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ B )
& ( C @ D @ A )
& ! [E: hF_Mirabelle_hf] :
( ( C @ D @ E )
=> ( E = A ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_Replace__iff) ).
thf(71,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_Replace @ B @ C ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ B )
& ( C @ D @ A )
& ! [E: hF_Mirabelle_hf] :
( ( C @ D @ E )
=> ( E = A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(72,plain,
! [C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_Replace @ B @ C ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ B )
& ( C @ D @ A )
& ! [E: hF_Mirabelle_hf] :
( ( C @ D @ E )
=> ( E = A ) ) ) ) ),
inference(cnf,[status(esa)],[71]) ).
thf(73,plain,
! [C: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_Replace @ B @ C ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ B )
& ( C @ D @ A )
& ! [E: hF_Mirabelle_hf] :
( ( C @ D @ E )
=> ( E = A ) ) ) ) ),
inference(lifteq,[status(thm)],[72]) ).
thf(3644,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hmem @ A @ ( hF_Mir1687042746ollect @ B @ C ) )
= ( $true
& ( hF_Mirabelle_hmem @ A @ C ) ) )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2895,62]) ).
thf(3645,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hmem @ A @ ( hF_Mir1687042746ollect @ B @ C ) )
= ( hF_Mirabelle_hmem @ A @ C ) )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( B @ A ) ) ),
inference(simp,[status(thm)],[3644]) ).
thf(3900,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ sk149
@ ( hF_Mir1687042746ollect
@ ^ [B: hF_Mirabelle_hf] : ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ B ) @ ( hF_Mir165288108strict @ r @ x ) )
@ A ) )
= ( hF_Mirabelle_hmem @ sk149 @ A ) ),
inference(pre_uni,[status(thm)],[3645:[bind(A,$thf( sk149 )),bind(B,$thf( ^ [D: hF_Mirabelle_hf] : ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ D ) @ ( hF_Mir165288108strict @ r @ x ) ) )),bind(C,$thf( C ))]]) ).
thf(3999,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ sk149
@ ( hF_Mir1687042746ollect
@ ^ [B: hF_Mirabelle_hf] : ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ B ) @ ( hF_Mir165288108strict @ r @ x ) )
@ A ) )
= ( hF_Mirabelle_hmem @ sk149 @ A ) ),
inference(simp,[status(thm)],[3900]) ).
thf(166,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( A = B )
= ( ! [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ A )
= ( hF_Mirabelle_hmem @ C @ B ) ) ) ),
inference(func_ext,[status(esa)],[134]) ).
thf(29,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ! [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ A )
= ( hF_Mirabelle_hmem @ C @ B ) )
=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_hf__equalityI) ).
thf(149,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ! [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ A )
= ( hF_Mirabelle_hmem @ C @ B ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(40,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( sk1 @ B @ A ) @ A )
| ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(44,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) )
| ( hF_Mirabelle_hmem @ ( sk1 @ B @ A ) @ A ) ),
inference(lifteq,[status(thm)],[40]) ).
thf(1866,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ ( hF_Mirabelle_HUnion @ A ) )
= ( ? [C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ A )
& ( hF_Mirabelle_hmem @ B @ C ) ) ) ),
inference(rewrite,[status(thm)],[87,1690]) ).
thf(2578,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ C )
| ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( hF_Mirabelle_hmem @ B @ D ) )
| ( ( hF_Mirabelle_hmem @ B @ ( hF_Mirabelle_HUnion @ A ) )
!= ( hF_Mirabelle_hmem @ ( sk24 @ C ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[1866,362]) ).
thf(2579,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ? [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk24 @ ( hF_Mirabelle_HUnion @ A ) ) @ B ) ) ),
inference(pattern_uni,[status(thm)],[2578:[bind(A,$thf( E )),bind(B,$thf( sk24 @ ( hF_Mirabelle_HUnion @ E ) )),bind(C,$thf( hF_Mirabelle_HUnion @ E ))]]) ).
thf(2671,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk128 @ A ) @ A ) )
& ( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk24 @ ( hF_Mirabelle_HUnion @ A ) ) @ ( sk128 @ A ) ) ) ),
inference(cnf,[status(esa)],[2579]) ).
thf(2672,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk128 @ A ) @ A ) ),
inference(cnfConj,[status(thm)],[2671]) ).
thf(2674,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk128 @ A ) @ A ) ),
inference(simp,[status(thm)],[2672]) ).
thf(1696,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ B )
& ( hF_Mirabelle_hmem @ C @ D ) )
| ( ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ C @ ( sk7 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[362,87]) ).
thf(1697,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( sk7 @ A ) )
| ? [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk24 @ ( sk7 @ A ) ) @ B ) ) ),
inference(pattern_uni,[status(thm)],[1696:[bind(A,$thf( sk7 @ E )),bind(B,$thf( E )),bind(C,$thf( sk24 @ ( sk7 @ E ) ))]]) ).
thf(1783,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mir1093797708lation @ ( sk7 @ A ) )
| ( hF_Mirabelle_hmem @ ( sk96 @ A ) @ A ) )
& ( ( hF_Mir1093797708lation @ ( sk7 @ A ) )
| ( hF_Mirabelle_hmem @ ( sk24 @ ( sk7 @ A ) ) @ ( sk96 @ A ) ) ) ),
inference(cnf,[status(esa)],[1697]) ).
thf(1784,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( sk7 @ A ) )
| ( hF_Mirabelle_hmem @ ( sk96 @ A ) @ A ) ),
inference(cnfConj,[status(thm)],[1783]) ).
thf(1786,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( sk7 @ A ) )
| ( hF_Mirabelle_hmem @ ( sk96 @ A ) @ A ) ),
inference(simp,[status(thm)],[1784]) ).
thf(2195,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( sk76 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ C
@ ( hF_Mir569462966eplace @ B
@ ^ [D: hF_Mirabelle_hf,E: hF_Mirabelle_hf] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[1424,534]) ).
thf(2196,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( ( hF_Mirabelle_hmem @ ( sk76 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ C
@ ( hF_Mir569462966eplace @ B
@ ^ [D: hF_Mirabelle_hf,E: hF_Mirabelle_hf] : $false ) ) ) ),
inference(simp,[status(thm)],[2195]) ).
thf(2197,plain,
! [A: hF_Mirabelle_hf] :
( hF_Mir1093797708lation
@ ( hF_Mirabelle_HUnion
@ ( hF_Mir569462966eplace @ A
@ ^ [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] : $false ) ) ),
inference(pattern_uni,[status(thm)],[2196:[bind(A,$thf( hF_Mir569462966eplace @ E @ ^ [E: hF_Mirabelle_hf] : ^ [F: hF_Mirabelle_hf] : $false )),bind(B,$thf( E )),bind(C,$thf( sk76 @ ( hF_Mir569462966eplace @ E @ ^ [E: hF_Mirabelle_hf] : ^ [F: hF_Mirabelle_hf] : $false ) ))]]) ).
thf(2293,plain,
! [A: hF_Mirabelle_hf] :
( hF_Mir1093797708lation
@ ( hF_Mirabelle_HUnion
@ ( hF_Mir569462966eplace @ A
@ ^ [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] : $false ) ) ),
inference(simp,[status(thm)],[2197]) ).
thf(2967,plain,
! [A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_HUnion @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[2895,84]) ).
thf(2968,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_HUnion @ A ) ) ),
inference(simp,[status(thm)],[2967]) ).
thf(3024,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ sk148 @ sk149 )
!= A )
| ( ( hF_Mir165288108strict @ r @ x )
!= ( hF_Mirabelle_HUnion @ A ) ) ),
inference(simp,[status(thm)],[2968]) ).
thf(3077,plain,
( ( hF_Mir165288108strict @ r @ x )
!= ( hF_Mirabelle_HUnion @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) ),
inference(simp,[status(thm)],[3024]) ).
thf(580,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir796903520_hpair @ A )
| ~ ? [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( A
= ( hF_Mirabelle_hpair @ B @ C ) ) ),
inference(bool_ext,[status(thm)],[164]) ).
thf(609,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir796903520_hpair @ A )
| ( A
!= ( hF_Mirabelle_hpair @ B @ C ) ) ),
inference(cnf,[status(esa)],[580]) ).
thf(610,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( A
!= ( hF_Mirabelle_hpair @ B @ C ) )
| ( hF_Mir796903520_hpair @ A ) ),
inference(lifteq,[status(thm)],[609]) ).
thf(611,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] : ( hF_Mir796903520_hpair @ ( hF_Mirabelle_hpair @ A @ B ) ),
inference(simp,[status(thm)],[610]) ).
thf(3126,plain,
! [A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2896,109]) ).
thf(3127,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ A @ A ) ),
inference(simp,[status(thm)],[3126]) ).
thf(3169,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ sk148 @ sk150 )
!= A )
| ( ( hF_Mir165288108strict @ r @ x )
!= A ) ),
inference(simp,[status(thm)],[3127]) ).
thf(3208,plain,
( ( hF_Mir165288108strict @ r @ x )
!= ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ),
inference(simp,[status(thm)],[3169]) ).
thf(3316,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( sk76 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) ) ),
inference(paramod_ordered,[status(thm)],[1424,2971]) ).
thf(3317,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( ( hF_Mirabelle_hmem @ ( sk76 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) ) ),
inference(simp,[status(thm)],[3316]) ).
thf(3336,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( ( sk76 @ A )
!= ( hF_Mir165288108strict @ r @ x ) )
| ( A
!= ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) ),
inference(simp,[status(thm)],[3317]) ).
thf(3352,plain,
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= ( sk76 @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) ) ),
inference(simp,[status(thm)],[3336]) ).
thf(2580,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ B )
& ( hF_Mirabelle_hmem @ C @ D ) )
| ( ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ C @ ( hF_Mirabelle_HUnion @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[362,1866]) ).
thf(2581,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ? [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk24 @ ( hF_Mirabelle_HUnion @ A ) ) @ B ) ) ),
inference(pattern_uni,[status(thm)],[2580:[bind(A,$thf( hF_Mirabelle_HUnion @ E )),bind(B,$thf( E )),bind(C,$thf( sk24 @ ( hF_Mirabelle_HUnion @ E ) ))]]) ).
thf(2676,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk129 @ A ) @ A ) )
& ( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk24 @ ( hF_Mirabelle_HUnion @ A ) ) @ ( sk129 @ A ) ) ) ),
inference(cnf,[status(esa)],[2581]) ).
thf(2677,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk129 @ A ) @ A ) ),
inference(cnfConj,[status(thm)],[2676]) ).
thf(2679,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( hF_Mirabelle_hmem @ ( sk129 @ A ) @ A ) ),
inference(simp,[status(thm)],[2677]) ).
thf(169,plain,
! [D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( sk1 @ B @ A ) @ A )
| ~ ? [E: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ E @ A )
& ( B @ E @ C ) )
| ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
!= ( hF_Mirabelle_hmem @ D @ ( hF_Mirabelle_HUnion @ D ) ) ) ),
inference(paramod_ordered,[status(thm)],[44,84]) ).
thf(180,plain,
! [D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( sk1 @ B @ A ) @ A )
| ~ ? [E: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ E @ A )
& ( B @ E @ C ) )
| ( C != D )
| ( ( hF_Mir569462966eplace @ A @ B )
!= ( hF_Mirabelle_HUnion @ D ) ) ),
inference(simp,[status(thm)],[169]) ).
thf(193,plain,
! [E: hF_Mirabelle_hf,D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( sk1 @ B @ A ) @ A )
| ~ ( hF_Mirabelle_hmem @ E @ A )
| ~ ( B @ E @ C )
| ( C != D )
| ( ( hF_Mir569462966eplace @ A @ B )
!= ( hF_Mirabelle_HUnion @ D ) ) ),
inference(cnf,[status(esa)],[180]) ).
thf(194,plain,
! [D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( sk1 @ B @ A ) @ A )
| ~ ( hF_Mirabelle_hmem @ D @ A )
| ~ ( B @ D @ C )
| ( ( hF_Mir569462966eplace @ A @ B )
!= ( hF_Mirabelle_HUnion @ C ) ) ),
inference(simp,[status(thm)],[193]) ).
thf(237,plain,
! [E: hF_Mirabelle_hf,D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ D @ A )
| ~ ( B @ D @ C )
| ( ( hF_Mir569462966eplace @ A @ B )
!= ( hF_Mirabelle_HUnion @ C ) )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( sk1 @ B @ A ) @ A )
!= ( hF_Mirabelle_hmem @ E @ E ) ) ),
inference(paramod_ordered,[status(thm)],[194,109]) ).
thf(238,plain,
! [E: hF_Mirabelle_hf,D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ D @ A )
| ~ ( B @ D @ C )
| ( ( hF_Mir569462966eplace @ A @ B )
!= ( hF_Mirabelle_HUnion @ C ) )
| ( ( hF_Mirabelle_hmem @ ( sk1 @ B @ A ) @ A )
!= ( hF_Mirabelle_hmem @ E @ E ) ) ),
inference(simp,[status(thm)],[237]) ).
thf(283,plain,
! [E: hF_Mirabelle_hf,D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ D @ A )
| ~ ( B @ D @ C )
| ( ( hF_Mir569462966eplace @ A @ B )
!= ( hF_Mirabelle_HUnion @ C ) )
| ( ( sk1 @ B @ A )
!= E )
| ( A != E ) ),
inference(simp,[status(thm)],[238]) ).
thf(318,plain,
! [D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ D @ A )
| ~ ( B @ D @ C )
| ( ( hF_Mir569462966eplace @ A @ B )
!= ( hF_Mirabelle_HUnion @ C ) )
| ( ( sk1 @ B @ A )
!= A ) ),
inference(simp,[status(thm)],[283]) ).
thf(102,plain,
! [C: hF_Mirabelle_hf > hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_RepFun @ B @ C ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ B )
& ( A
= ( C @ D ) ) ) ) ),
inference(cnf,[status(esa)],[101]) ).
thf(103,plain,
! [C: hF_Mirabelle_hf > hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mirabelle_RepFun @ B @ C ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ B )
& ( A
= ( C @ D ) ) ) ) ),
inference(lifteq,[status(thm)],[102]) ).
thf(9,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hsnd @ ( hF_Mirabelle_hpair @ A @ B ) )
= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_hsnd__conv) ).
thf(66,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hsnd @ ( hF_Mirabelle_hpair @ A @ B ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(2058,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ A ) @ B )
!= ( hF_Mirabelle_hmem @ B @ A ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[1381]) ).
thf(2061,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ( ( hF_Mirabelle_HUnion @ A )
!= B )
| ( B != A ) ),
inference(simp,[status(thm)],[2058]) ).
thf(2075,plain,
! [A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ A ) @ A )
| ( ( hF_Mirabelle_HUnion @ A )
!= A ) ),
inference(simp,[status(thm)],[2061]) ).
thf(25,axiom,
! [TA: $tType,A: hF_Mirabelle_hf > hF_Mirabelle_hf > TA,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hsplit @ TA @ A @ ( hF_Mirabelle_hpair @ B @ C ) )
= ( A @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_hsplit) ).
thf(130,plain,
! [TA: $tType,A: hF_Mirabelle_hf > hF_Mirabelle_hf > TA,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hsplit @ TA @ A @ ( hF_Mirabelle_hpair @ B @ C ) )
= ( A @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(27,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o] :
( ! [C: hF_Mirabelle_hf,D: hF_Mirabelle_hf,E: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ A )
=> ( ( B @ C @ D )
=> ( ( B @ C @ E )
=> ( E = D ) ) ) )
=> ? [C: hF_Mirabelle_hf] :
! [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ C )
= ( ? [E: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ E @ A )
& ( B @ E @ D ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_replacement) ).
thf(135,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o] :
( ! [C: hF_Mirabelle_hf,D: hF_Mirabelle_hf,E: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ C @ A )
=> ( ( B @ C @ D )
=> ( ( B @ C @ E )
=> ( E = D ) ) ) )
=> ? [C: hF_Mirabelle_hf] :
! [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ C )
= ( ? [E: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ E @ A )
& ( B @ E @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(78,plain,
~ ? [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hpair @ A @ B )
= A ),
inference(miniscope,[status(thm)],[77]) ).
thf(79,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hpair @ A @ B )
!= A ),
inference(cnf,[status(esa)],[78]) ).
thf(80,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hpair @ A @ B )
!= A ),
inference(lifteq,[status(thm)],[79]) ).
thf(6282,plain,
! [D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ ( hF_Mirabelle_HUnion @ A ) )
| ( ( hF_Mirabelle_hmem @ B @ ( sk7 @ A ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ C @ D ) @ D ) ) ),
inference(paramod_ordered,[status(thm)],[1690,6208]) ).
thf(6283,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk7 @ B ) ) @ ( hF_Mirabelle_HUnion @ B ) ),
inference(pattern_uni,[status(thm)],[6282:[bind(A,$thf( G )),bind(B,$thf( sk6 @ E @ ( sk7 @ G ) )),bind(C,$thf( E )),bind(D,$thf( sk7 @ G ))]]) ).
thf(6320,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk7 @ B ) ) @ ( hF_Mirabelle_HUnion @ B ) ),
inference(simp,[status(thm)],[6283]) ).
thf(6316,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ C ),
inference(cnfConj,[status(thm)],[6315]) ).
thf(6318,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ C ),
inference(simp,[status(thm)],[6316]) ).
thf(7838,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[2896,6318]) ).
thf(7839,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ C ) ),
inference(simp,[status(thm)],[7838]) ).
thf(7853,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( sk6 @ A @ ( sk6 @ B @ C ) )
!= ( hF_Mirabelle_hpair @ sk148 @ sk150 ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= C ) ),
inference(simp,[status(thm)],[7839]) ).
thf(7896,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( sk6 @ A @ ( sk6 @ B @ ( hF_Mir165288108strict @ r @ x ) ) )
!= ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ),
inference(simp,[status(thm)],[7853]) ).
thf(160,plain,
( ~ $true
| ( ( hF_Mir859708136nction @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mir859708136nction @ r ) ) ),
inference(paramod_ordered,[status(thm)],[159,34]) ).
thf(161,plain,
( ( hF_Mir859708136nction @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mir859708136nction @ r ) ),
inference(simp,[status(thm)],[160]) ).
thf(162,plain,
( ( hF_Mir165288108strict @ r @ x )
!= r ),
inference(simp,[status(thm)],[161]) ).
thf(669,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ B @ B ) ) ),
inference(paramod_ordered,[status(thm)],[362,109]) ).
thf(670,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ( ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ B @ B ) ) ),
inference(simp,[status(thm)],[669]) ).
thf(686,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ( ( sk24 @ A )
!= B )
| ( A != B ) ),
inference(simp,[status(thm)],[670]) ).
thf(712,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ( ( sk24 @ A )
!= A ) ),
inference(simp,[status(thm)],[686]) ).
thf(7018,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2896,6209]) ).
thf(7019,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ A ) ),
inference(simp,[status(thm)],[7018]) ).
thf(7045,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( sk6 @ A @ B )
!= ( hF_Mirabelle_hpair @ sk148 @ sk150 ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= A ) ),
inference(simp,[status(thm)],[7019]) ).
thf(7055,plain,
! [A: hF_Mirabelle_hf] :
( ( sk6 @ ( hF_Mir165288108strict @ r @ x ) @ A )
!= ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ),
inference(simp,[status(thm)],[7045]) ).
thf(3742,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hmem @ A @ ( hF_Mir1687042746ollect @ B @ C ) )
= ( $true
& ( hF_Mirabelle_hmem @ A @ C ) ) )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2896,62]) ).
thf(3743,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hmem @ A @ ( hF_Mir1687042746ollect @ B @ C ) )
= ( hF_Mirabelle_hmem @ A @ C ) )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( B @ A ) ) ),
inference(simp,[status(thm)],[3742]) ).
thf(3863,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ sk150
@ ( hF_Mir1687042746ollect
@ ^ [B: hF_Mirabelle_hf] : ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ B ) @ ( hF_Mir165288108strict @ r @ x ) )
@ A ) )
= ( hF_Mirabelle_hmem @ sk150 @ A ) ),
inference(pre_uni,[status(thm)],[3743:[bind(A,$thf( sk150 )),bind(B,$thf( ^ [D: hF_Mirabelle_hf] : ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ D ) @ ( hF_Mir165288108strict @ r @ x ) ) )),bind(C,$thf( C ))]]) ).
thf(3940,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ sk150
@ ( hF_Mir1687042746ollect
@ ^ [B: hF_Mirabelle_hf] : ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ B ) @ ( hF_Mir165288108strict @ r @ x ) )
@ A ) )
= ( hF_Mirabelle_hmem @ sk150 @ A ) ),
inference(simp,[status(thm)],[3863]) ).
thf(660,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ C
@ ( hF_Mir569462966eplace @ B
@ ^ [D: hF_Mirabelle_hf,E: hF_Mirabelle_hf] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[362,534]) ).
thf(661,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ( ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ C
@ ( hF_Mir569462966eplace @ B
@ ^ [D: hF_Mirabelle_hf,E: hF_Mirabelle_hf] : $false ) ) ) ),
inference(simp,[status(thm)],[660]) ).
thf(662,plain,
! [A: hF_Mirabelle_hf] :
( hF_Mir1093797708lation
@ ( hF_Mir569462966eplace @ A
@ ^ [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] : $false ) ),
inference(pattern_uni,[status(thm)],[661:[bind(A,$thf( hF_Mir569462966eplace @ E @ ^ [E: hF_Mirabelle_hf] : ^ [F: hF_Mirabelle_hf] : $false )),bind(B,$thf( E )),bind(C,$thf( sk24 @ ( hF_Mir569462966eplace @ E @ ^ [E: hF_Mirabelle_hf] : ^ [F: hF_Mirabelle_hf] : $false ) ))]]) ).
thf(717,plain,
! [A: hF_Mirabelle_hf] :
( hF_Mir1093797708lation
@ ( hF_Mir569462966eplace @ A
@ ^ [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] : $false ) ),
inference(simp,[status(thm)],[662]) ).
thf(24,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf,D: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ A @ B )
= ( hF_Mirabelle_hpair @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_hpair__iff) ).
thf(127,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf,D: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ A @ B )
= ( hF_Mirabelle_hpair @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(31,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mir165288108strict @ B @ C ) )
= ( ( hF_Mirabelle_hmem @ A @ B )
& ? [D: hF_Mirabelle_hf,E: hF_Mirabelle_hf] :
( ( A
= ( hF_Mirabelle_hpair @ D @ E ) )
& ( hF_Mirabelle_hmem @ D @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_hrestrict__iff) ).
thf(154,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ A @ ( hF_Mir165288108strict @ B @ C ) )
= ( ( hF_Mirabelle_hmem @ A @ B )
& ? [D: hF_Mirabelle_hf,E: hF_Mirabelle_hf] :
( ( A
= ( hF_Mirabelle_hpair @ D @ E ) )
& ( hF_Mirabelle_hmem @ D @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(2223,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ C )
& ( hF_Mirabelle_hmem @ B @ D ) )
| ( ( hF_Mirabelle_hmem @ ( sk76 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ B @ ( hF_Mirabelle_HUnion @ C ) ) ) ),
inference(paramod_ordered,[status(thm)],[1424,59]) ).
thf(2224,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ ( hF_Mirabelle_HUnion @ A ) ) )
| ? [B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ B @ A )
& ( hF_Mirabelle_hmem @ ( sk76 @ ( hF_Mirabelle_HUnion @ A ) ) @ B ) ) ),
inference(pattern_uni,[status(thm)],[2223:[bind(A,$thf( hF_Mirabelle_HUnion @ E )),bind(B,$thf( sk76 @ ( hF_Mirabelle_HUnion @ E ) )),bind(C,$thf( E ))]]) ).
thf(2317,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ ( hF_Mirabelle_HUnion @ A ) ) )
| ( hF_Mirabelle_hmem @ ( sk112 @ A ) @ A ) )
& ( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ ( hF_Mirabelle_HUnion @ A ) ) )
| ( hF_Mirabelle_hmem @ ( sk76 @ ( hF_Mirabelle_HUnion @ A ) ) @ ( sk112 @ A ) ) ) ),
inference(cnf,[status(esa)],[2224]) ).
thf(2318,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ ( hF_Mirabelle_HUnion @ A ) ) )
| ( hF_Mirabelle_hmem @ ( sk112 @ A ) @ A ) ),
inference(cnfConj,[status(thm)],[2317]) ).
thf(2320,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ ( hF_Mirabelle_HUnion @ A ) ) )
| ( hF_Mirabelle_hmem @ ( sk112 @ A ) @ A ) ),
inference(simp,[status(thm)],[2318]) ).
thf(7807,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[2895,6318]) ).
thf(7808,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ C ) ),
inference(simp,[status(thm)],[7807]) ).
thf(7866,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( sk6 @ A @ ( sk6 @ B @ C ) )
!= ( hF_Mirabelle_hpair @ sk148 @ sk149 ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= C ) ),
inference(simp,[status(thm)],[7808]) ).
thf(7908,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( sk6 @ A @ ( sk6 @ B @ ( hF_Mir165288108strict @ r @ x ) ) )
!= ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ),
inference(simp,[status(thm)],[7866]) ).
thf(3128,plain,
! [A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ ( hF_Mirabelle_HUnion @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[2896,1942]) ).
thf(3129,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ ( hF_Mirabelle_HUnion @ A ) ) ),
inference(simp,[status(thm)],[3128]) ).
thf(3168,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ sk148 @ sk150 )
!= ( sk7 @ A ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= ( hF_Mirabelle_HUnion @ A ) ) ),
inference(simp,[status(thm)],[3129]) ).
thf(363,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ~ ( hF_Mir796903520_hpair @ ( sk24 @ A ) ) ),
inference(cnfConj,[status(thm)],[361]) ).
thf(19,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf > $o] :
? [C: hF_Mirabelle_hf] :
! [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ C )
= ( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_comprehension) ).
thf(104,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf > $o] :
? [C: hF_Mirabelle_hf] :
! [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ C )
= ( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(3500,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( sk77 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) ) ),
inference(paramod_ordered,[status(thm)],[1429,2971]) ).
thf(3501,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( ( hF_Mirabelle_hmem @ ( sk77 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) ) ),
inference(simp,[status(thm)],[3500]) ).
thf(3512,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( ( sk77 @ A )
!= ( hF_Mir165288108strict @ r @ x ) )
| ( A
!= ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) ),
inference(simp,[status(thm)],[3501]) ).
thf(3593,plain,
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= ( sk77 @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ) ) ),
inference(simp,[status(thm)],[3512]) ).
thf(3153,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[2896,1763]) ).
thf(3154,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ B ) ) ),
inference(simp,[status(thm)],[3153]) ).
thf(3176,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ( ( hF_Mirabelle_hpair @ sk148 @ sk150 )
!= ( sk7 @ A ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= B ) ),
inference(simp,[status(thm)],[3154]) ).
thf(3220,plain,
! [A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ A )
| ( ( hF_Mirabelle_hpair @ sk148 @ sk150 )
!= ( sk7 @ A ) ) ),
inference(simp,[status(thm)],[3176]) ).
thf(7016,plain,
! [D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ ( hF_Mirabelle_HUnion @ A ) )
| ( ( hF_Mirabelle_hmem @ B @ ( sk7 @ A ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ C @ D ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[1690,6209]) ).
thf(7017,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk6 @ ( sk7 @ B ) @ A ) @ ( hF_Mirabelle_HUnion @ B ) ),
inference(pattern_uni,[status(thm)],[7016:[bind(A,$thf( G )),bind(B,$thf( sk6 @ ( sk7 @ G ) @ F )),bind(C,$thf( sk7 @ G )),bind(D,$thf( F ))]]) ).
thf(7080,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ ( sk6 @ ( sk7 @ B ) @ A ) @ ( hF_Mirabelle_HUnion @ B ) ),
inference(simp,[status(thm)],[7017]) ).
thf(675,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ B @ ( hF_Mirabelle_HUnion @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[362,84]) ).
thf(676,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ( ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ B @ ( hF_Mirabelle_HUnion @ B ) ) ) ),
inference(simp,[status(thm)],[675]) ).
thf(690,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ( ( sk24 @ A )
!= B )
| ( A
!= ( hF_Mirabelle_HUnion @ B ) ) ),
inference(simp,[status(thm)],[676]) ).
thf(716,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ( ( hF_Mirabelle_HUnion @ ( sk24 @ A ) )
!= A ) ),
inference(simp,[status(thm)],[690]) ).
thf(8824,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[2896,6319]) ).
thf(8825,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ ( sk6 @ B @ C ) ) @ B ) ),
inference(simp,[status(thm)],[8824]) ).
thf(8860,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( sk6 @ A @ ( sk6 @ B @ C ) )
!= ( hF_Mirabelle_hpair @ sk148 @ sk150 ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= B ) ),
inference(simp,[status(thm)],[8825]) ).
thf(8886,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( sk6 @ A @ ( sk6 @ ( hF_Mir165288108strict @ r @ x ) @ B ) )
!= ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ),
inference(simp,[status(thm)],[8860]) ).
thf(28,axiom,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf] :
? [C: hF_Mirabelle_hf] :
! [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ C )
= ( ? [E: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ E @ A )
& ( D
= ( B @ E ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_replacement__fun) ).
thf(146,plain,
! [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf] :
? [C: hF_Mirabelle_hf] :
! [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ C )
= ( ? [E: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ E @ A )
& ( D
= ( B @ E ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(2977,plain,
! [A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ ( hF_Mirabelle_HUnion @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[2895,1942]) ).
thf(2978,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk7 @ A ) @ ( hF_Mirabelle_HUnion @ A ) ) ),
inference(simp,[status(thm)],[2977]) ).
thf(3015,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ sk148 @ sk149 )
!= ( sk7 @ A ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= ( hF_Mirabelle_HUnion @ A ) ) ),
inference(simp,[status(thm)],[2978]) ).
thf(125,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hfst @ ( hF_Mirabelle_hpair @ A @ B ) )
= A ),
inference(cnf,[status(esa)],[124]) ).
thf(126,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hfst @ ( hF_Mirabelle_hpair @ A @ B ) )
= A ),
inference(lifteq,[status(thm)],[125]) ).
thf(113,plain,
! [D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ A @ B )
!= ( hF_Mirabelle_hpair @ C @ D ) )
| ( B = D ) ),
inference(cnfConj,[status(thm)],[111]) ).
thf(117,plain,
! [D: hF_Mirabelle_hf,C: hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hpair @ A @ B )
!= ( hF_Mirabelle_hpair @ C @ D ) )
| ( B = D ) ),
inference(lifteq,[status(thm)],[113]) ).
thf(118,plain,
? [A: hF_Mirabelle_hf > hF_Mirabelle_hf > hF_Mirabelle_hf] :
! [B: hF_Mirabelle_hf,C: hF_Mirabelle_hf] :
( ( A @ B @ ( hF_Mirabelle_hpair @ B @ C ) )
= C ),
inference(detectInverse,[status(thm)],[117]) ).
thf(119,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( sk11 @ A @ ( hF_Mirabelle_hpair @ A @ B ) )
= B ),
inference(cnf,[status(esa)],[118]) ).
thf(1033,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( sk11 @ A @ ( hF_Mirabelle_hpair @ A @ B ) )
= B ),
inference(lifteq,[status(thm)],[119]) ).
thf(3379,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( sk76 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) ) ),
inference(paramod_ordered,[status(thm)],[1424,3122]) ).
thf(3380,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( ( hF_Mirabelle_hmem @ ( sk76 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) ) ),
inference(simp,[status(thm)],[3379]) ).
thf(3404,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ A ) )
| ( ( sk76 @ A )
!= ( hF_Mir165288108strict @ r @ x ) )
| ( A
!= ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) ),
inference(simp,[status(thm)],[3380]) ).
thf(3424,plain,
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_HUnion @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= ( sk76 @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) ) ),
inference(simp,[status(thm)],[3404]) ).
thf(91,plain,
! [D: hF_Mirabelle_hf > hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( A != B )
| ( hF_Mirabelle_hmem @ ( sk8 @ D @ C @ B @ A ) @ B )
| ( ( hF_Mirabelle_RepFun @ A @ C )
= ( hF_Mirabelle_RepFun @ B @ D ) ) ),
inference(cnfConj,[status(thm)],[90]) ).
thf(93,plain,
! [D: hF_Mirabelle_hf > hF_Mirabelle_hf,C: hF_Mirabelle_hf > hF_Mirabelle_hf,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( A != B )
| ( ( hF_Mirabelle_RepFun @ A @ C )
= ( hF_Mirabelle_RepFun @ B @ D ) )
| ( hF_Mirabelle_hmem @ ( sk8 @ D @ C @ B @ A ) @ B ) ),
inference(lifteq,[status(thm)],[91]) ).
thf(94,plain,
! [C: hF_Mirabelle_hf > hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_RepFun @ A @ B )
= ( hF_Mirabelle_RepFun @ A @ C ) )
| ( hF_Mirabelle_hmem @ ( sk8 @ C @ B @ A @ A ) @ A ) ),
inference(simp,[status(thm)],[93]) ).
thf(6284,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[2896,6208]) ).
thf(6285,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ B ) ),
inference(simp,[status(thm)],[6284]) ).
thf(6299,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( sk6 @ A @ B )
!= ( hF_Mirabelle_hpair @ sk148 @ sk150 ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= B ) ),
inference(simp,[status(thm)],[6285]) ).
thf(6329,plain,
! [A: hF_Mirabelle_hf] :
( ( sk6 @ A @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ),
inference(simp,[status(thm)],[6299]) ).
thf(2897,plain,
sk149 != sk150,
inference(cnfConj,[status(thm)],[2894]) ).
thf(2898,plain,
sk150 != sk149,
inference(lifteq,[status(thm)],[2897]) ).
thf(43,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( sk3 @ B @ A )
!= ( sk2 @ B @ A ) )
| ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(47,plain,
! [C: hF_Mirabelle_hf,B: hF_Mirabelle_hf > hF_Mirabelle_hf > $o,A: hF_Mirabelle_hf] :
( ( ( sk3 @ B @ A )
!= ( sk2 @ B @ A ) )
| ( ( hF_Mirabelle_hmem @ C @ ( hF_Mir569462966eplace @ A @ B ) )
= ( ? [D: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ D @ A )
& ( B @ D @ C ) ) ) ) ),
inference(lifteq,[status(thm)],[43]) ).
thf(67,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hsnd @ ( hF_Mirabelle_hpair @ A @ B ) )
= B ),
inference(cnf,[status(esa)],[66]) ).
thf(68,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hsnd @ ( hF_Mirabelle_hpair @ A @ B ) )
= B ),
inference(lifteq,[status(thm)],[67]) ).
thf(3111,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ~ ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ A ) @ B )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ B @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2896,1381]) ).
thf(3112,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ A ) @ B )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ B @ A ) ) ),
inference(simp,[status(thm)],[3111]) ).
thf(3113,plain,
~ ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ ( hF_Mir165288108strict @ r @ x ) ) @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ),
inference(pattern_uni,[status(thm)],[3112:[bind(A,$thf( hF_Mir165288108strict @ r @ x )),bind(B,$thf( hF_Mirabelle_hpair @ sk148 @ sk150 ))]]) ).
thf(6989,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2895,6209]) ).
thf(6990,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk149 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( sk6 @ A @ B ) @ A ) ),
inference(simp,[status(thm)],[6989]) ).
thf(7034,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( sk6 @ A @ B )
!= ( hF_Mirabelle_hpair @ sk148 @ sk149 ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= A ) ),
inference(simp,[status(thm)],[6990]) ).
thf(7088,plain,
! [A: hF_Mirabelle_hf] :
( ( sk6 @ ( hF_Mir165288108strict @ r @ x ) @ A )
!= ( hF_Mirabelle_hpair @ sk148 @ sk149 ) ),
inference(simp,[status(thm)],[7034]) ).
thf(3114,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ A ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[2896,1381]) ).
thf(3115,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ( ( hF_Mirabelle_hmem @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) @ ( hF_Mir165288108strict @ r @ x ) )
!= ( hF_Mirabelle_hmem @ ( hF_Mirabelle_HUnion @ A ) @ B ) ) ),
inference(simp,[status(thm)],[3114]) ).
thf(3179,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ B @ A )
| ( ( hF_Mirabelle_hpair @ sk148 @ sk150 )
!= ( hF_Mirabelle_HUnion @ A ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= B ) ),
inference(simp,[status(thm)],[3115]) ).
thf(3227,plain,
! [A: hF_Mirabelle_hf] :
( ~ ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ A )
| ( ( hF_Mirabelle_hpair @ sk148 @ sk150 )
!= ( hF_Mirabelle_HUnion @ A ) ) ),
inference(simp,[status(thm)],[3179]) ).
thf(3390,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ~ $true
| ( ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) ) ),
inference(paramod_ordered,[status(thm)],[362,3122]) ).
thf(3391,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ( ( hF_Mirabelle_hmem @ ( sk24 @ A ) @ A )
!= ( hF_Mirabelle_hmem @ ( hF_Mir165288108strict @ r @ x ) @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) ) ),
inference(simp,[status(thm)],[3390]) ).
thf(3411,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mir1093797708lation @ A )
| ( ( sk24 @ A )
!= ( hF_Mir165288108strict @ r @ x ) )
| ( A
!= ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) ),
inference(simp,[status(thm)],[3391]) ).
thf(3432,plain,
( ( hF_Mir1093797708lation @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) )
| ( ( hF_Mir165288108strict @ r @ x )
!= ( sk24 @ ( hF_Mirabelle_hpair @ sk148 @ sk150 ) ) ) ),
inference(simp,[status(thm)],[3411]) ).
thf(98,plain,
~ ? [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hpair @ A @ B )
= B ),
inference(miniscope,[status(thm)],[97]) ).
thf(99,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hpair @ A @ B )
!= B ),
inference(cnf,[status(esa)],[98]) ).
thf(100,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_hpair @ A @ B )
!= B ),
inference(lifteq,[status(thm)],[99]) ).
thf(18292,plain,
$false,
inference(e,[status(thm)],[37,69,101,2480,88,6338,120,56,153,110,6208,157,3099,46,152,57,3602,8870,164,4050,84,3152,2964,133,5665,74,60,85,534,7078,3037,70,3371,165,1032,65,3065,97,3254,3122,2895,3001,109,77,1424,96,124,1942,1429,3064,134,73,3999,166,34,45,149,44,2674,59,71,1786,54,2293,3077,611,3208,159,3352,2679,81,318,362,76,1690,2896,103,66,6319,1381,2075,130,135,80,35,6320,7896,162,194,48,712,63,7055,3940,717,127,1763,6318,154,2320,7908,3168,363,203,1781,104,1866,3593,158,3220,2971,7080,716,8886,36,146,3015,107,126,1033,3424,94,6329,2898,6209,47,68,62,3113,7088,163,3227,3432,100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP076^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.09/0.22 % Computer : n011.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.23 % CPULimit : 300
% 0.09/0.23 % WCLimit : 300
% 0.09/0.23 % DateTime : Tue Sep 29 19:48:01 UTC 2026
% 0.09/0.23 % CPUTime :
% 0.09/0.23 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.88/0.79 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.43/1.20 % [INFO] Parsing done (406ms).
% 2.43/1.22 % [INFO] Running in sequential loop mode.
% 3.68/1.62 % [INFO] eprover registered as external prover.
% 3.68/1.62 % [INFO] Scanning for conjecture ...
% 3.86/1.76 % [INFO] Found a conjecture (or negated_conjecture) and 298 axioms. Running axiom selection ...
% 4.08/1.83 % [INFO] Axiom selection finished. Selected 31 axioms (removed 267 axioms).
% 4.41/1.91 % [INFO] Problem is higher-order (TPTP THF).
% 4.41/1.93 % [INFO] Type checking passed.
% 4.41/1.93 % [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 ...
% 100.35/23.10 % External prover 'e' found a proof!
% 100.35/23.10 % [INFO] Killing All external provers ...
% 100.35/23.11 % Time passed: 22740ms (effective reasoning time: 21875ms)
% 100.35/23.11 % 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)>
% 100.35/23.11 % Axioms used in derivation (31): fact_19_hfst__conv, fact_30_Replace__cong, fact_27_RepFun__iff, fact_22_is__hpair__def, fact_31_hmem__Sup__ne, fact_25_Replace__iff, fact_13_comprehension, fact_15_hpair__neq__fst, fact_5_hf__equalityI, fact_16_hpair__neq__snd, fact_24_HUnion__iff, fact_2_hrestrict__iff, fact_3_hpair__iff, fact_7_hmem__ne, fact_18_hsplit, fact_29_RepFun__cong, fact_10_hmem__not__sym, fact_17_replacement__fun, fact_20_hsnd__conv, fact_14_hmem__not__refl, fact_12_union__of__set, fact_0_hrelation__restr, fact_26_HCollect__iff, fact_8_replacement, fact_6_hf__ext, fact_11_hpair__inject, fact_1_hfunction__def, conj_0, fact_9_binary__union, fact_23_PrimReplace__iff, fact_21_hrelation__def
% 100.35/23.11 % No. of inferences in proof: 399
% 100.35/23.11 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 22740 ms resp. 21875 ms w/o parsing
% 102.18/23.42 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 102.18/23.42 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------