%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP072^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n014.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:39 AM UTC 2026
% Result : Theorem 163.09s 94.81s
% Output : Refutation 163.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 24
% Syntax : Number of formulae : 133 ( 75 unt; 0 typ; 6 def)
% Number of atoms : 321 ( 162 equ; 0 cnn)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 780 ( 130 ~; 87 |; 3 &; 528 @)
% ( 0 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Number of types : 6 ( 5 usr)
% Number of type conns : 20 ( 20 >; 0 *; 0 +; 0 <<)
% Number of symbols : 23 ( 20 usr; 9 con; 0-2 aty)
% Number of variables : 183 ( 10 ^; 166 !; 1 ?; 183 :)
% ( 0 !>; 0 ?*; 0 @-; 6 @+)
% Comments :
%------------------------------------------------------------------------------
thf(set_se933006839lle_hf_type,type,
set_se933006839lle_hf: $tType ).
thf(set_HF_Mirabelle_hf_type,type,
set_HF_Mirabelle_hf: $tType ).
thf(hF_Mirabelle_hf_type,type,
hF_Mirabelle_hf: $tType ).
thf(set_nat_type,type,
set_nat: $tType ).
thf(nat_type,type,
nat: $tType ).
thf(finite1213132899lle_hf_decl,type,
finite1213132899lle_hf: set_HF_Mirabelle_hf > nat ).
thf(finite586181922lle_hf_decl,type,
finite586181922lle_hf: set_HF_Mirabelle_hf > $o ).
thf(zero_z189798548lle_hf_decl,type,
zero_z189798548lle_hf: hF_Mirabelle_hf ).
thf(zero_zero_nat_decl,type,
zero_zero_nat: nat ).
thf(hF_Mirabelle_HF_decl,type,
hF_Mirabelle_HF: set_HF_Mirabelle_hf > hF_Mirabelle_hf ).
thf(hF_Mirabelle_hfset_decl,type,
hF_Mirabelle_hfset: hF_Mirabelle_hf > set_HF_Mirabelle_hf ).
thf(hF_Mirabelle_hmem_decl,type,
hF_Mirabelle_hmem: hF_Mirabelle_hf > hF_Mirabelle_hf > $o ).
thf(bot_bot_nat_decl,type,
bot_bot_nat: nat ).
thf(bot_bo53200981lle_hf_decl,type,
bot_bo53200981lle_hf: set_HF_Mirabelle_hf ).
thf(ord_less_eq_nat_decl,type,
ord_less_eq_nat: nat > nat > $o ).
thf(ord_le432112161lle_hf_decl,type,
ord_le432112161lle_hf: set_HF_Mirabelle_hf > set_HF_Mirabelle_hf > $o ).
thf(insert9649339lle_hf_decl,type,
insert9649339lle_hf: hF_Mirabelle_hf > set_HF_Mirabelle_hf > set_HF_Mirabelle_hf ).
thf(member1367349282lle_hf_decl,type,
member1367349282lle_hf: hF_Mirabelle_hf > set_HF_Mirabelle_hf > $o ).
thf(z_decl,type,
z: hF_Mirabelle_hf ).
thf(sk5_decl,type,
sk5: ( nat > nat > $o ) > nat ).
thf(sk6_decl,type,
sk6: ( nat > nat > $o ) > nat ).
thf(sk7_decl,type,
sk7: ( nat > nat > $o ) > nat ).
thf(sk8_decl,type,
sk8: ( nat > nat > $o ) > nat ).
thf(sk60_decl,type,
sk60: hF_Mirabelle_hf ).
thf(sk587_decl,type,
sk587: hF_Mirabelle_hf ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: nat > nat > $o] :
@+[B: nat] :
~ ! [C: nat] :
( ( ord_less_eq_nat @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: nat > nat > $o] :
@+[B: nat] :
~ ( ( ord_less_eq_nat @ ( sk5 @ A ) @ B )
=> ( A @ ( sk5 @ A ) @ B ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: nat > nat > $o] :
@+[B: nat] :
~ ! [C: nat] :
( ( A @ C @ B )
=> ( A @ B @ C ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: nat > nat > $o] :
@+[B: nat] :
~ ( ( A @ B @ ( sk7 @ A ) )
=> ( A @ ( sk7 @ A ) @ B ) ) ) ) ).
thf(sk60_def,definition,
( sk60
= ( @+[A: hF_Mirabelle_hf] :
~ ~ ( hF_Mirabelle_hmem @ A @ z ) ) ) ).
thf(sk587_def,definition,
( sk587
= ( @+[A: hF_Mirabelle_hf] :
~ ~ ( hF_Mirabelle_hmem @ A @ z ) ) ) ).
thf(98,axiom,
! [A: set_HF_Mirabelle_hf] :
( ~ ( finite586181922lle_hf @ A )
=> ( ( finite1213132899lle_hf @ A )
= zero_zero_nat ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_169_card_Oinfinite) ).
thf(630,plain,
! [A: set_HF_Mirabelle_hf] :
( ~ ( finite586181922lle_hf @ A )
=> ( ( finite1213132899lle_hf @ A )
= zero_zero_nat ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[98]) ).
thf(631,plain,
! [A: set_HF_Mirabelle_hf] :
( ( finite586181922lle_hf @ A )
| ( ( finite1213132899lle_hf @ A )
= zero_zero_nat ) ),
inference(cnf,[status(esa)],[630]) ).
thf(632,plain,
! [A: set_HF_Mirabelle_hf] :
( ( ( finite1213132899lle_hf @ A )
= zero_zero_nat )
| ( finite586181922lle_hf @ A ) ),
inference(lifteq,[status(thm)],[631]) ).
thf(131,axiom,
! [A: hF_Mirabelle_hf] : ( finite586181922lle_hf @ ( hF_Mirabelle_hfset @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_107_finite__hfset) ).
thf(757,plain,
! [A: hF_Mirabelle_hf] : ( finite586181922lle_hf @ ( hF_Mirabelle_hfset @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[131]) ).
thf(758,plain,
! [A: hF_Mirabelle_hf] : ( finite586181922lle_hf @ ( hF_Mirabelle_hfset @ A ) ),
inference(cnf,[status(esa)],[757]) ).
thf(24,axiom,
! [A: set_HF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( finite586181922lle_hf @ A )
=> ( ord_less_eq_nat @ ( finite1213132899lle_hf @ A ) @ ( finite1213132899lle_hf @ ( insert9649339lle_hf @ B @ A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_248_card__insert__le) ).
thf(224,plain,
! [A: set_HF_Mirabelle_hf,B: hF_Mirabelle_hf] :
( ( finite586181922lle_hf @ A )
=> ( ord_less_eq_nat @ ( finite1213132899lle_hf @ A ) @ ( finite1213132899lle_hf @ ( insert9649339lle_hf @ B @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(225,plain,
! [A: set_HF_Mirabelle_hf] :
( ( finite586181922lle_hf @ A )
=> ! [B: hF_Mirabelle_hf] : ( ord_less_eq_nat @ ( finite1213132899lle_hf @ A ) @ ( finite1213132899lle_hf @ ( insert9649339lle_hf @ B @ A ) ) ) ),
inference(miniscope,[status(thm)],[224]) ).
thf(226,plain,
! [B: hF_Mirabelle_hf,A: set_HF_Mirabelle_hf] :
( ~ ( finite586181922lle_hf @ A )
| ( ord_less_eq_nat @ ( finite1213132899lle_hf @ A ) @ ( finite1213132899lle_hf @ ( insert9649339lle_hf @ B @ A ) ) ) ),
inference(cnf,[status(esa)],[225]) ).
thf(9241,plain,
! [C: hF_Mirabelle_hf,B: set_HF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ~ $true
| ( ord_less_eq_nat @ ( finite1213132899lle_hf @ B ) @ ( finite1213132899lle_hf @ ( insert9649339lle_hf @ C @ B ) ) )
| ( ( finite586181922lle_hf @ ( hF_Mirabelle_hfset @ A ) )
!= ( finite586181922lle_hf @ B ) ) ),
inference(paramod_ordered,[status(thm)],[758,226]) ).
thf(9242,plain,
! [C: hF_Mirabelle_hf,B: set_HF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ord_less_eq_nat @ ( finite1213132899lle_hf @ B ) @ ( finite1213132899lle_hf @ ( insert9649339lle_hf @ C @ B ) ) )
| ( ( finite586181922lle_hf @ ( hF_Mirabelle_hfset @ A ) )
!= ( finite586181922lle_hf @ B ) ) ),
inference(simp,[status(thm)],[9241]) ).
thf(9243,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] : ( ord_less_eq_nat @ ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ B ) ) @ ( finite1213132899lle_hf @ ( insert9649339lle_hf @ A @ ( hF_Mirabelle_hfset @ B ) ) ) ),
inference(pattern_uni,[status(thm)],[9242:[bind(A,$thf( D )),bind(B,$thf( hF_Mirabelle_hfset @ D ))]]) ).
thf(9357,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] : ( ord_less_eq_nat @ ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ B ) ) @ ( finite1213132899lle_hf @ ( insert9649339lle_hf @ A @ ( hF_Mirabelle_hfset @ B ) ) ) ),
inference(simp,[status(thm)],[9243]) ).
thf(21,axiom,
! [A: nat] :
( ( ord_less_eq_nat @ A @ bot_bot_nat )
=> ( A = bot_bot_nat ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_210_bot_Oextremum__uniqueI) ).
thf(217,plain,
! [A: nat] :
( ( ord_less_eq_nat @ A @ bot_bot_nat )
=> ( A = bot_bot_nat ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(218,plain,
! [A: nat] :
( ~ ( ord_less_eq_nat @ A @ bot_bot_nat )
| ( A = bot_bot_nat ) ),
inference(cnf,[status(esa)],[217]) ).
thf(219,plain,
! [A: nat] :
( ( A = bot_bot_nat )
| ~ ( ord_less_eq_nat @ A @ bot_bot_nat ) ),
inference(lifteq,[status(thm)],[218]) ).
thf(129,axiom,
bot_bot_nat = zero_zero_nat,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_106_bot__nat__def) ).
thf(751,plain,
bot_bot_nat = zero_zero_nat,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[129]) ).
thf(752,plain,
bot_bot_nat = zero_zero_nat,
inference(lifteq,[status(thm)],[751]) ).
thf(1890,plain,
! [A: nat] :
( ( A = zero_zero_nat )
| ~ ( ord_less_eq_nat @ A @ zero_zero_nat ) ),
inference(rewrite,[status(thm)],[219,752]) ).
thf(6,axiom,
! [A: set_HF_Mirabelle_hf,B: set_HF_Mirabelle_hf] :
( ( finite586181922lle_hf @ A )
=> ( ( ord_le432112161lle_hf @ B @ A )
=> ( ( ord_less_eq_nat @ ( finite1213132899lle_hf @ A ) @ ( finite1213132899lle_hf @ B ) )
=> ( B = A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_244_card__seteq) ).
thf(161,plain,
! [A: set_HF_Mirabelle_hf,B: set_HF_Mirabelle_hf] :
( ( finite586181922lle_hf @ A )
=> ( ( ord_le432112161lle_hf @ B @ A )
=> ( ( ord_less_eq_nat @ ( finite1213132899lle_hf @ A ) @ ( finite1213132899lle_hf @ B ) )
=> ( B = A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(162,plain,
! [A: set_HF_Mirabelle_hf] :
( ( finite586181922lle_hf @ A )
=> ! [B: set_HF_Mirabelle_hf] :
( ( ord_le432112161lle_hf @ B @ A )
=> ( ( ord_less_eq_nat @ ( finite1213132899lle_hf @ A ) @ ( finite1213132899lle_hf @ B ) )
=> ( B = A ) ) ) ),
inference(miniscope,[status(thm)],[161]) ).
thf(163,plain,
! [B: set_HF_Mirabelle_hf,A: set_HF_Mirabelle_hf] :
( ~ ( finite586181922lle_hf @ A )
| ~ ( ord_le432112161lle_hf @ B @ A )
| ~ ( ord_less_eq_nat @ ( finite1213132899lle_hf @ A ) @ ( finite1213132899lle_hf @ B ) )
| ( B = A ) ),
inference(cnf,[status(esa)],[162]) ).
thf(164,plain,
! [B: set_HF_Mirabelle_hf,A: set_HF_Mirabelle_hf] :
( ( B = A )
| ~ ( finite586181922lle_hf @ A )
| ~ ( ord_le432112161lle_hf @ B @ A )
| ~ ( ord_less_eq_nat @ ( finite1213132899lle_hf @ A ) @ ( finite1213132899lle_hf @ B ) ) ),
inference(lifteq,[status(thm)],[163]) ).
thf(122,axiom,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_HF @ ( hF_Mirabelle_hfset @ A ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_14_HF__hfset) ).
thf(731,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_HF @ ( hF_Mirabelle_hfset @ A ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[122]) ).
thf(732,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_HF @ ( hF_Mirabelle_hfset @ A ) )
= A ),
inference(cnf,[status(esa)],[731]) ).
thf(733,plain,
! [A: hF_Mirabelle_hf] :
( ( hF_Mirabelle_HF @ ( hF_Mirabelle_hfset @ A ) )
= A ),
inference(lifteq,[status(thm)],[732]) ).
thf(140,axiom,
( zero_z189798548lle_hf
= ( hF_Mirabelle_HF @ bot_bo53200981lle_hf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9_Zero__hf__def) ).
thf(779,plain,
( zero_z189798548lle_hf
= ( hF_Mirabelle_HF @ bot_bo53200981lle_hf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[140]) ).
thf(780,plain,
( ( hF_Mirabelle_HF @ bot_bo53200981lle_hf )
= zero_z189798548lle_hf ),
inference(lifteq,[status(thm)],[779]) ).
thf(1632,plain,
! [A: hF_Mirabelle_hf] :
( ( A = zero_z189798548lle_hf )
| ( ( hF_Mirabelle_HF @ ( hF_Mirabelle_hfset @ A ) )
!= ( hF_Mirabelle_HF @ bot_bo53200981lle_hf ) ) ),
inference(paramod_ordered,[status(thm)],[733,780]) ).
thf(1634,plain,
! [A: hF_Mirabelle_hf] :
( ( A = zero_z189798548lle_hf )
| ( ( hF_Mirabelle_hfset @ A )
!= bot_bo53200981lle_hf ) ),
inference(simp,[status(thm)],[1632]) ).
thf(1,conjecture,
( ( z = zero_z189798548lle_hf )
= ( ! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ z ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(2,negated_conjecture,
( ( z = zero_z189798548lle_hf )
!= ( ! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ z ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(149,plain,
( ( z = zero_z189798548lle_hf )
!= ( ! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ z ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(150,plain,
( ( z = zero_z189798548lle_hf )
!= ( ! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ z ) ) ),
inference(lifteq,[status(thm)],[149]) ).
thf(806,plain,
( ( z != zero_z189798548lle_hf )
| ~ ! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ z ) ),
inference(bool_ext,[status(thm)],[150]) ).
thf(808,plain,
( ( z != zero_z189798548lle_hf )
| ~ ! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ z ) ),
inference(lifteq,[status(thm)],[806]) ).
thf(810,plain,
( ( z != zero_z189798548lle_hf )
| ( hF_Mirabelle_hmem @ sk60 @ z ) ),
inference(cnf,[status(esa)],[808]) ).
thf(143,axiom,
! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ zero_z189798548lle_hf ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_hmem__hempty) ).
thf(786,plain,
! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ zero_z189798548lle_hf ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[143]) ).
thf(787,plain,
~ ? [A: hF_Mirabelle_hf] : ( hF_Mirabelle_hmem @ A @ zero_z189798548lle_hf ),
inference(miniscope,[status(thm)],[786]) ).
thf(788,plain,
! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ zero_z189798548lle_hf ),
inference(cnf,[status(esa)],[787]) ).
thf(902,plain,
! [A: hF_Mirabelle_hf] :
( ( z != zero_z189798548lle_hf )
| ~ $true
| ( ( hF_Mirabelle_hmem @ sk60 @ z )
!= ( hF_Mirabelle_hmem @ A @ zero_z189798548lle_hf ) ) ),
inference(paramod_ordered,[status(thm)],[810,788]) ).
thf(903,plain,
! [A: hF_Mirabelle_hf] :
( ( z != zero_z189798548lle_hf )
| ( ( hF_Mirabelle_hmem @ sk60 @ z )
!= ( hF_Mirabelle_hmem @ A @ zero_z189798548lle_hf ) ) ),
inference(simp,[status(thm)],[902]) ).
thf(905,plain,
! [A: hF_Mirabelle_hf] :
( ( z != zero_z189798548lle_hf )
| ( sk60 != A )
| ( z != zero_z189798548lle_hf ) ),
inference(simp,[status(thm)],[903]) ).
thf(907,plain,
z != zero_z189798548lle_hf,
inference(simp,[status(thm)],[905]) ).
thf(2447,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hfset @ A )
!= bot_bo53200981lle_hf )
| ( zero_z189798548lle_hf != zero_z189798548lle_hf )
| ( A != z ) ),
inference(paramod_ordered,[status(thm)],[1634,907]) ).
thf(2448,plain,
! [A: hF_Mirabelle_hf] :
( ( ( hF_Mirabelle_hfset @ A )
!= bot_bo53200981lle_hf )
| ( A != z ) ),
inference(simp,[status(thm)],[2447]) ).
thf(2449,plain,
( ( hF_Mirabelle_hfset @ z )
!= bot_bo53200981lle_hf ),
inference(pattern_uni,[status(thm)],[2448:[bind(A,$thf( z ))]]) ).
thf(2570,plain,
! [B: set_HF_Mirabelle_hf,A: set_HF_Mirabelle_hf] :
( ~ ( finite586181922lle_hf @ A )
| ~ ( ord_le432112161lle_hf @ B @ A )
| ~ ( ord_less_eq_nat @ ( finite1213132899lle_hf @ A ) @ ( finite1213132899lle_hf @ B ) )
| ( B != bot_bo53200981lle_hf )
| ( A
!= ( hF_Mirabelle_hfset @ z ) ) ),
inference(paramod_ordered,[status(thm)],[164,2449]) ).
thf(2571,plain,
! [A: set_HF_Mirabelle_hf] :
( ~ ( finite586181922lle_hf @ ( hF_Mirabelle_hfset @ z ) )
| ~ ( ord_le432112161lle_hf @ A @ ( hF_Mirabelle_hfset @ z ) )
| ~ ( ord_less_eq_nat @ ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ z ) ) @ ( finite1213132899lle_hf @ A ) )
| ( A != bot_bo53200981lle_hf ) ),
inference(pattern_uni,[status(thm)],[2570:[bind(A,$thf( hF_Mirabelle_hfset @ z )),bind(B,$thf( B ))]]) ).
thf(2573,plain,
( ~ ( finite586181922lle_hf @ ( hF_Mirabelle_hfset @ z ) )
| ~ ( ord_le432112161lle_hf @ bot_bo53200981lle_hf @ ( hF_Mirabelle_hfset @ z ) )
| ~ ( ord_less_eq_nat @ ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ z ) ) @ ( finite1213132899lle_hf @ bot_bo53200981lle_hf ) ) ),
inference(simp,[status(thm)],[2571]) ).
thf(115,axiom,
( ( finite1213132899lle_hf @ bot_bo53200981lle_hf )
= zero_zero_nat ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_168_card_Oempty) ).
thf(704,plain,
( ( finite1213132899lle_hf @ bot_bo53200981lle_hf )
= zero_zero_nat ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[115]) ).
thf(705,plain,
( ( finite1213132899lle_hf @ bot_bo53200981lle_hf )
= zero_zero_nat ),
inference(lifteq,[status(thm)],[704]) ).
thf(71,axiom,
! [A: set_HF_Mirabelle_hf] : ( ord_le432112161lle_hf @ bot_bo53200981lle_hf @ A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_164_empty__subsetI) ).
thf(468,plain,
! [A: set_HF_Mirabelle_hf] : ( ord_le432112161lle_hf @ bot_bo53200981lle_hf @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(469,plain,
! [A: set_HF_Mirabelle_hf] : ( ord_le432112161lle_hf @ bot_bo53200981lle_hf @ A ),
inference(cnf,[status(esa)],[468]) ).
thf(2858,plain,
( ~ $true
| ~ $true
| ~ ( ord_less_eq_nat @ ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ z ) ) @ zero_zero_nat ) ),
inference(rewrite,[status(thm)],[2573,705,469,758]) ).
thf(2859,plain,
~ ( ord_less_eq_nat @ ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ z ) ) @ zero_zero_nat ),
inference(simp,[status(thm)],[2858]) ).
thf(2870,plain,
! [A: nat] :
( ~ ( ord_less_eq_nat @ A @ zero_zero_nat )
| ~ ( ord_less_eq_nat @ ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ z ) ) @ A )
| ( zero_zero_nat != zero_zero_nat ) ),
inference(paramod_ordered,[status(thm)],[1890,2859]) ).
thf(2871,plain,
! [A: nat] :
( ~ ( ord_less_eq_nat @ A @ zero_zero_nat )
| ~ ( ord_less_eq_nat @ ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ z ) ) @ A ) ),
inference(pattern_uni,[status(thm)],[2870:[]]) ).
thf(3,axiom,
! [A: nat] :
( ( ord_less_eq_nat @ A @ bot_bot_nat )
= ( A = bot_bot_nat ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_208_bot_Oextremum__unique) ).
thf(151,plain,
! [A: nat] :
( ( ord_less_eq_nat @ A @ bot_bot_nat )
= ( A = bot_bot_nat ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(152,plain,
! [A: nat] :
( ( ord_less_eq_nat @ A @ bot_bot_nat )
= ( A = bot_bot_nat ) ),
inference(cnf,[status(esa)],[151]) ).
thf(153,plain,
! [A: nat] :
( ( ord_less_eq_nat @ A @ bot_bot_nat )
= ( A = bot_bot_nat ) ),
inference(lifteq,[status(thm)],[152]) ).
thf(828,plain,
! [A: nat] :
( ( ord_less_eq_nat @ A @ zero_zero_nat )
= ( A = zero_zero_nat ) ),
inference(rewrite,[status(thm)],[153,752]) ).
thf(3458,plain,
! [A: nat] :
( ( A != zero_zero_nat )
| ~ ( ord_less_eq_nat @ ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ z ) ) @ A ) ),
inference(rewrite,[status(thm)],[2871,828]) ).
thf(3459,plain,
! [A: nat] :
( ( A != zero_zero_nat )
| ~ ( ord_less_eq_nat @ ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ z ) ) @ A ) ),
inference(lifteq,[status(thm)],[3458]) ).
thf(14886,plain,
! [C: nat,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( C != zero_zero_nat )
| ~ $true
| ( ( ord_less_eq_nat @ ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ B ) ) @ ( finite1213132899lle_hf @ ( insert9649339lle_hf @ A @ ( hF_Mirabelle_hfset @ B ) ) ) )
!= ( ord_less_eq_nat @ ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ z ) ) @ C ) ) ),
inference(paramod_ordered,[status(thm)],[9357,3459]) ).
thf(14887,plain,
! [C: nat,B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( C != zero_zero_nat )
| ( ( ord_less_eq_nat @ ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ B ) ) @ ( finite1213132899lle_hf @ ( insert9649339lle_hf @ A @ ( hF_Mirabelle_hfset @ B ) ) ) )
!= ( ord_less_eq_nat @ ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ z ) ) @ C ) ) ),
inference(simp,[status(thm)],[14886]) ).
thf(14888,plain,
! [A: hF_Mirabelle_hf] :
( ( finite1213132899lle_hf @ ( insert9649339lle_hf @ A @ ( hF_Mirabelle_hfset @ z ) ) )
!= zero_zero_nat ),
inference(pattern_uni,[status(thm)],[14887:[bind(A,$thf( E )),bind(B,$thf( z )),bind(C,$thf( finite1213132899lle_hf @ ( insert9649339lle_hf @ E @ ( hF_Mirabelle_hfset @ z ) ) ))]]) ).
thf(15032,plain,
! [A: hF_Mirabelle_hf] :
( ( finite1213132899lle_hf @ ( insert9649339lle_hf @ A @ ( hF_Mirabelle_hfset @ z ) ) )
!= zero_zero_nat ),
inference(simp,[status(thm)],[14888]) ).
thf(15076,plain,
! [B: hF_Mirabelle_hf,A: set_HF_Mirabelle_hf] :
( ( finite586181922lle_hf @ A )
| ( zero_zero_nat != zero_zero_nat )
| ( ( finite1213132899lle_hf @ A )
!= ( finite1213132899lle_hf @ ( insert9649339lle_hf @ B @ ( hF_Mirabelle_hfset @ z ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[632,15032]) ).
thf(15077,plain,
! [B: hF_Mirabelle_hf,A: set_HF_Mirabelle_hf] :
( ( finite586181922lle_hf @ A )
| ( ( finite1213132899lle_hf @ A )
!= ( finite1213132899lle_hf @ ( insert9649339lle_hf @ B @ ( hF_Mirabelle_hfset @ z ) ) ) ) ),
inference(simp,[status(thm)],[15076]) ).
thf(15078,plain,
! [A: hF_Mirabelle_hf] : ( finite586181922lle_hf @ ( insert9649339lle_hf @ A @ ( hF_Mirabelle_hfset @ z ) ) ),
inference(pattern_uni,[status(thm)],[15077:[bind(A,$thf( insert9649339lle_hf @ C @ ( hF_Mirabelle_hfset @ z ) )),bind(B,$thf( C ))]]) ).
thf(15085,plain,
! [A: hF_Mirabelle_hf] : ( finite586181922lle_hf @ ( insert9649339lle_hf @ A @ ( hF_Mirabelle_hfset @ z ) ) ),
inference(simp,[status(thm)],[15078]) ).
thf(99,axiom,
! [A: hF_Mirabelle_hf,B: set_HF_Mirabelle_hf] :
( ( finite586181922lle_hf @ ( insert9649339lle_hf @ A @ B ) )
= ( finite586181922lle_hf @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_117_finite__insert) ).
thf(633,plain,
! [A: hF_Mirabelle_hf,B: set_HF_Mirabelle_hf] :
( ( finite586181922lle_hf @ ( insert9649339lle_hf @ A @ B ) )
= ( finite586181922lle_hf @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(634,plain,
! [B: set_HF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( finite586181922lle_hf @ ( insert9649339lle_hf @ A @ B ) )
= ( finite586181922lle_hf @ B ) ),
inference(cnf,[status(esa)],[633]) ).
thf(635,plain,
! [B: set_HF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( finite586181922lle_hf @ ( insert9649339lle_hf @ A @ B ) )
= ( finite586181922lle_hf @ B ) ),
inference(lifteq,[status(thm)],[634]) ).
thf(15096,plain,
finite586181922lle_hf @ ( hF_Mirabelle_hfset @ z ),
inference(rewrite,[status(thm)],[15085,635]) ).
thf(116,axiom,
! [A: set_HF_Mirabelle_hf] :
( ( ! [B: hF_Mirabelle_hf] :
~ ( member1367349282lle_hf @ B @ A ) )
= ( A = bot_bo53200981lle_hf ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_20_all__not__in__conv) ).
thf(706,plain,
! [A: set_HF_Mirabelle_hf] :
( ( ! [B: hF_Mirabelle_hf] :
~ ( member1367349282lle_hf @ B @ A ) )
= ( A = bot_bo53200981lle_hf ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(707,plain,
! [A: set_HF_Mirabelle_hf] :
( ( ! [B: hF_Mirabelle_hf] :
~ ( member1367349282lle_hf @ B @ A ) )
= ( A = bot_bo53200981lle_hf ) ),
inference(cnf,[status(esa)],[706]) ).
thf(708,plain,
! [A: set_HF_Mirabelle_hf] :
( ( ! [B: hF_Mirabelle_hf] :
~ ( member1367349282lle_hf @ B @ A ) )
= ( A = bot_bo53200981lle_hf ) ),
inference(lifteq,[status(thm)],[707]) ).
thf(63,axiom,
! [A: set_HF_Mirabelle_hf] :
( ( ( finite1213132899lle_hf @ A )
= zero_zero_nat )
= ( ( A = bot_bo53200981lle_hf )
| ~ ( finite586181922lle_hf @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_228_card__eq__0__iff) ).
thf(442,plain,
! [A: set_HF_Mirabelle_hf] :
( ( ( finite1213132899lle_hf @ A )
= zero_zero_nat )
= ( ( A = bot_bo53200981lle_hf )
| ~ ( finite586181922lle_hf @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(443,plain,
! [A: set_HF_Mirabelle_hf] :
( ( ( finite1213132899lle_hf @ A )
= zero_zero_nat )
= ( ( A = bot_bo53200981lle_hf )
| ~ ( finite586181922lle_hf @ A ) ) ),
inference(cnf,[status(esa)],[442]) ).
thf(444,plain,
! [A: set_HF_Mirabelle_hf] :
( ( ( A = bot_bo53200981lle_hf )
| ~ ( finite586181922lle_hf @ A ) )
= ( ( finite1213132899lle_hf @ A )
= zero_zero_nat ) ),
inference(lifteq,[status(thm)],[443]) ).
thf(21222,plain,
! [B: set_HF_Mirabelle_hf,A: set_HF_Mirabelle_hf] :
( ( ( ! [C: hF_Mirabelle_hf] :
~ ( member1367349282lle_hf @ C @ A )
| ~ ( finite586181922lle_hf @ B ) )
= ( ( finite1213132899lle_hf @ B )
= zero_zero_nat ) )
| ( ( A = bot_bo53200981lle_hf )
!= ( B = bot_bo53200981lle_hf ) ) ),
inference(paramod_ordered,[status(thm)],[708,444]) ).
thf(21223,plain,
! [A: set_HF_Mirabelle_hf] :
( ( ! [B: hF_Mirabelle_hf] :
~ ( member1367349282lle_hf @ B @ A )
| ~ ( finite586181922lle_hf @ A ) )
= ( ( finite1213132899lle_hf @ A )
= zero_zero_nat ) ),
inference(pattern_uni,[status(thm)],[21222:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(45145,plain,
! [A: set_HF_Mirabelle_hf] :
( ( ( ! [B: hF_Mirabelle_hf] :
~ ( member1367349282lle_hf @ B @ A )
| ~ $true )
= ( ( finite1213132899lle_hf @ A )
= zero_zero_nat ) )
| ( ( finite586181922lle_hf @ ( hF_Mirabelle_hfset @ z ) )
!= ( finite586181922lle_hf @ A ) ) ),
inference(paramod_ordered,[status(thm)],[15096,21223]) ).
thf(45146,plain,
! [A: set_HF_Mirabelle_hf] :
( ( ( ! [B: hF_Mirabelle_hf] :
~ ( member1367349282lle_hf @ B @ A ) )
= ( ( finite1213132899lle_hf @ A )
= zero_zero_nat ) )
| ( ( finite586181922lle_hf @ ( hF_Mirabelle_hfset @ z ) )
!= ( finite586181922lle_hf @ A ) ) ),
inference(simp,[status(thm)],[45145]) ).
thf(45147,plain,
( ( ! [A: hF_Mirabelle_hf] :
~ ( member1367349282lle_hf @ A @ ( hF_Mirabelle_hfset @ z ) ) )
= ( ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ z ) )
= zero_zero_nat ) ),
inference(pattern_uni,[status(thm)],[45146:[bind(A,$thf( hF_Mirabelle_hfset @ z ))]]) ).
thf(141,axiom,
( hF_Mirabelle_hmem
= ( ^ [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] : ( member1367349282lle_hf @ A @ ( hF_Mirabelle_hfset @ B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_hmem__def) ).
thf(781,plain,
( hF_Mirabelle_hmem
= ( ^ [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] : ( member1367349282lle_hf @ A @ ( hF_Mirabelle_hfset @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[141]) ).
thf(782,plain,
( ( ^ [A: hF_Mirabelle_hf,B: hF_Mirabelle_hf] : ( member1367349282lle_hf @ A @ ( hF_Mirabelle_hfset @ B ) ) )
= hF_Mirabelle_hmem ),
inference(lifteq,[status(thm)],[781]) ).
thf(840,plain,
! [B: hF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( member1367349282lle_hf @ A @ ( hF_Mirabelle_hfset @ B ) )
= ( hF_Mirabelle_hmem @ A @ B ) ),
inference(func_ext,[status(esa)],[782]) ).
thf(21155,plain,
! [B: set_HF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( ( B = bot_bo53200981lle_hf )
| ~ $true )
= ( ( finite1213132899lle_hf @ B )
= zero_zero_nat ) )
| ( ( finite586181922lle_hf @ ( hF_Mirabelle_hfset @ A ) )
!= ( finite586181922lle_hf @ B ) ) ),
inference(paramod_ordered,[status(thm)],[758,444]) ).
thf(21156,plain,
! [B: set_HF_Mirabelle_hf,A: hF_Mirabelle_hf] :
( ( ( B = bot_bo53200981lle_hf )
= ( ( finite1213132899lle_hf @ B )
= zero_zero_nat ) )
| ( ( finite586181922lle_hf @ ( hF_Mirabelle_hfset @ A ) )
!= ( finite586181922lle_hf @ B ) ) ),
inference(simp,[status(thm)],[21155]) ).
thf(21157,plain,
! [A: hF_Mirabelle_hf] :
( ( ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ A ) )
= zero_zero_nat )
= ( ( hF_Mirabelle_hfset @ A )
= bot_bo53200981lle_hf ) ),
inference(pattern_uni,[status(thm)],[21156:[bind(A,$thf( C )),bind(B,$thf( hF_Mirabelle_hfset @ C ))]]) ).
thf(21356,plain,
! [A: hF_Mirabelle_hf] :
( ( ( finite1213132899lle_hf @ ( hF_Mirabelle_hfset @ A ) )
= zero_zero_nat )
= ( ( hF_Mirabelle_hfset @ A )
= bot_bo53200981lle_hf ) ),
inference(simp,[status(thm)],[21157]) ).
thf(47628,plain,
( ( ! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ z ) )
= ( ( hF_Mirabelle_hfset @ z )
= bot_bo53200981lle_hf ) ),
inference(rewrite,[status(thm)],[45147,840,21356]) ).
thf(20,axiom,
! [A: nat > nat > $o,B: nat,C: nat] :
( ! [D: nat,E: nat] :
( ( ord_less_eq_nat @ D @ E )
=> ( A @ D @ E ) )
=> ( ! [D: nat,E: nat] :
( ( A @ E @ D )
=> ( A @ D @ E ) )
=> ( A @ B @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_174_linorder__wlog) ).
thf(210,plain,
! [A: nat > nat > $o,B: nat,C: nat] :
( ! [D: nat,E: nat] :
( ( ord_less_eq_nat @ D @ E )
=> ( A @ D @ E ) )
=> ( ! [D: nat,E: nat] :
( ( A @ E @ D )
=> ( A @ D @ E ) )
=> ( A @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(211,plain,
! [A: nat > nat > $o] :
( ! [B: nat,C: nat] :
( ( ord_less_eq_nat @ B @ C )
=> ( A @ B @ C ) )
=> ( ! [B: nat,C: nat] :
( ( A @ C @ B )
=> ( A @ B @ C ) )
=> ! [B: nat,C: nat] : ( A @ B @ C ) ) ),
inference(miniscope,[status(thm)],[210]) ).
thf(212,plain,
! [C: nat,B: nat,A: nat > nat > $o] :
( ( ( ord_less_eq_nat @ ( sk5 @ A ) @ ( sk6 @ A ) )
| ( A @ ( sk8 @ A ) @ ( sk7 @ A ) )
| ( A @ B @ C ) )
& ( ( ord_less_eq_nat @ ( sk5 @ A ) @ ( sk6 @ A ) )
| ~ ( A @ ( sk7 @ A ) @ ( sk8 @ A ) )
| ( A @ B @ C ) )
& ( ~ ( A @ ( sk5 @ A ) @ ( sk6 @ A ) )
| ( A @ ( sk8 @ A ) @ ( sk7 @ A ) )
| ( A @ B @ C ) )
& ( ~ ( A @ ( sk5 @ A ) @ ( sk6 @ A ) )
| ~ ( A @ ( sk7 @ A ) @ ( sk8 @ A ) )
| ( A @ B @ C ) ) ),
inference(cnf,[status(esa)],[211]) ).
thf(215,plain,
! [C: nat,B: nat,A: nat > nat > $o] :
( ~ ( A @ ( sk5 @ A ) @ ( sk6 @ A ) )
| ( A @ ( sk8 @ A ) @ ( sk7 @ A ) )
| ( A @ B @ C ) ),
inference(cnfConj,[status(thm)],[212]) ).
thf(47764,plain,
! [C: nat,B: nat,A: nat > nat > $o] :
( ~ ! [D: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ D @ z )
| ( A @ ( sk8 @ A ) @ ( sk7 @ A ) )
| ( A @ B @ C )
| ( ( A @ ( sk5 @ A ) @ ( sk6 @ A ) )
!= ( ( hF_Mirabelle_hfset @ z )
= bot_bo53200981lle_hf ) ) ),
inference(paramod_ordered,[status(thm)],[47628,215]) ).
thf(47876,plain,
( ~ ! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ z )
| ( ( hF_Mirabelle_hfset @ z )
= bot_bo53200981lle_hf )
| ( ( hF_Mirabelle_hfset @ z )
= bot_bo53200981lle_hf ) ),
inference(pre_uni,[status(thm)],[47764:[bind(A,$thf( ^ [D: nat] : ^ [E: nat] : ( ( hF_Mirabelle_hfset @ z ) = bot_bo53200981lle_hf ) )),bind(B,$thf( B )),bind(C,$thf( C ))]]) ).
thf(47920,plain,
( ( hF_Mirabelle_hmem @ sk587 @ z )
| ( ( hF_Mirabelle_hfset @ z )
= bot_bo53200981lle_hf )
| ( ( hF_Mirabelle_hfset @ z )
= bot_bo53200981lle_hf ) ),
inference(cnf,[status(esa)],[47876]) ).
thf(47921,plain,
( ( ( hF_Mirabelle_hfset @ z )
= bot_bo53200981lle_hf )
| ( ( hF_Mirabelle_hfset @ z )
= bot_bo53200981lle_hf )
| ( hF_Mirabelle_hmem @ sk587 @ z ) ),
inference(lifteq,[status(thm)],[47920]) ).
thf(47922,plain,
( ( ( hF_Mirabelle_hfset @ z )
= bot_bo53200981lle_hf )
| ( hF_Mirabelle_hmem @ sk587 @ z ) ),
inference(simp,[status(thm)],[47921]) ).
thf(807,plain,
( ( z = zero_z189798548lle_hf )
| ! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ z ) ),
inference(bool_ext,[status(thm)],[150]) ).
thf(809,plain,
( ( z = zero_z189798548lle_hf )
| ! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ z ) ),
inference(lifteq,[status(thm)],[807]) ).
thf(811,plain,
! [A: hF_Mirabelle_hf] :
( ( z = zero_z189798548lle_hf )
| ~ ( hF_Mirabelle_hmem @ A @ z ) ),
inference(cnf,[status(esa)],[809]) ).
thf(910,plain,
! [A: hF_Mirabelle_hf] :
~ ( hF_Mirabelle_hmem @ A @ z ),
inference(simplifyReflect,[status(thm)],[811,907]) ).
thf(48895,plain,
( ( ( hF_Mirabelle_hfset @ z )
= bot_bo53200981lle_hf )
| $false ),
inference(rewrite,[status(thm)],[47922,910]) ).
thf(48896,plain,
( ( hF_Mirabelle_hfset @ z )
= bot_bo53200981lle_hf ),
inference(simp,[status(thm)],[48895]) ).
thf(48897,plain,
$false,
inference(simplifyReflect,[status(thm)],[48896,2449]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP072^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21 % Computer : n014.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Tue Sep 29 19:47:00 UTC 2026
% 0.10/0.21 % CPUTime :
% 0.10/0.21 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.88/0.78 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.08/1.19 % [INFO] Parsing done (407ms).
% 2.41/1.20 % [INFO] Running in sequential loop mode.
% 3.23/1.58 % [INFO] eprover registered as external prover.
% 3.23/1.59 % [INFO] Scanning for conjecture ...
% 3.63/1.74 % [INFO] Found a conjecture (or negated_conjecture) and 351 axioms. Running axiom selection ...
% 3.83/1.87 % [INFO] Axiom selection finished. Selected 146 axioms (removed 205 axioms).
% 4.46/2.04 % [INFO] Problem is higher-order (TPTP THF).
% 4.46/2.06 % [INFO] Type checking passed.
% 4.46/2.07 % [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 ...
% 163.09/94.80 % [INFO] Killing All external provers ...
% 163.09/94.80 % Time passed: 94450ms (effective reasoning time: 93590ms)
% 163.09/94.80 % 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)>
% 163.09/94.81 % Axioms used in derivation (17): fact_9_Zero__hf__def, fact_14_HF__hfset, fact_106_bot__nat__def, fact_2_hmem__hempty, fact_117_finite__insert, fact_168_card_Oempty, fact_5_hmem__def, fact_20_all__not__in__conv, fact_164_empty__subsetI, fact_248_card__insert__le, fact_244_card__seteq, fact_107_finite__hfset, fact_208_bot_Oextremum__unique, fact_210_bot_Oextremum__uniqueI, fact_228_card__eq__0__iff, fact_174_linorder__wlog, fact_169_card_Oinfinite
% 163.09/94.81 % No. of inferences in proof: 127
% 163.09/94.81 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 94450 ms resp. 93590 ms w/o parsing
% 163.57/94.93 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 163.57/94.93 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------