%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : ITP117^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 Oct 7 10:24:10 AM UTC 2026
% Result : Theorem 2.37s 0.59s
% Output : CNFRefutation 2.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 2
% Syntax : Number of formulae : 15 ( 15 unt; 0 typ; 0 def)
% Number of atoms : 39 ( 25 equ; 0 cnn)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 124 ( 2 ~; 0 |; 0 &; 122 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 2 ( 1 avg)
% Number of types : 19 ( 18 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 119 ( 116 usr; 18 con; 0-2 aty)
% Number of variables : 19 ( 14 ^; 5 !; 0 ?; 19 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_extend1728876344nnreal,type,
extend1728876344nnreal: $tType ).
thf(tp_finite1489363574real_n,type,
finite1489363574real_n: $tType ).
thf(tp_finite964658038_int_n,type,
finite964658038_int_n: $tType ).
thf(tp_nat,type,
nat: $tType ).
thf(tp_set_Ex113815278nnreal,type,
set_Ex113815278nnreal: $tType ).
thf(tp_set_Fi1058188332real_n,type,
set_Fi1058188332real_n: $tType ).
thf(tp_set_Fi160064172_int_n,type,
set_Fi160064172_int_n: $tType ).
thf(tp_set_Si1125517487real_n,type,
set_Si1125517487real_n: $tType ).
thf(tp_set_nat,type,
set_nat: $tType ).
thf(tp_set_o,type,
set_o: $tType ).
thf(tp_set_se2111327970real_n,type,
set_se2111327970real_n: $tType ).
thf(tp_set_se820660888real_n,type,
set_se820660888real_n: $tType ).
thf(tp_set_se944069346_int_n,type,
set_se944069346_int_n: $tType ).
thf(tp_set_set_nat,type,
set_set_nat: $tType ).
thf(tp_set_set_o,type,
set_set_o: $tType ).
thf(tp_sigma_1422848389real_n,type,
sigma_1422848389real_n: $tType ).
thf(tp_sigma_1466784463real_n,type,
sigma_1466784463real_n: $tType ).
thf(tp_sigma_measure_o,type,
sigma_measure_o: $tType ).
thf(tp_collec1941932235_int_n,type,
collec1941932235_int_n: ( finite964658038_int_n > $o ) > set_Fi160064172_int_n ).
thf(tp_collec321817931real_n,type,
collec321817931real_n: ( finite1489363574real_n > $o ) > set_Fi1058188332real_n ).
thf(tp_collec452821761real_n,type,
collec452821761real_n: ( set_Fi1058188332real_n > $o ) > set_se2111327970real_n ).
thf(tp_collect_nat,type,
collect_nat: ( nat > $o ) > set_nat ).
thf(tp_collect_o,type,
collect_o: ( $o > $o ) > set_o ).
thf(tp_comple1413366923nnreal,type,
comple1413366923nnreal: set_Ex113815278nnreal > extend1728876344nnreal ).
thf(tp_comple1665300069_set_o,type,
comple1665300069_set_o: set_set_o > set_o ).
thf(tp_comple1682161881et_nat,type,
comple1682161881et_nat: set_set_nat > set_nat ).
thf(tp_comple1917283637real_n,type,
comple1917283637real_n: set_se820660888real_n > set_se2111327970real_n ).
thf(tp_comple2042271945real_n,type,
comple2042271945real_n: set_Fi1058188332real_n > finite1489363574real_n ).
thf(tp_comple230862828real_n,type,
comple230862828real_n: sigma_1466784463real_n > sigma_1466784463real_n ).
thf(tp_comple488165692real_n,type,
comple488165692real_n: set_Si1125517487real_n > sigma_1466784463real_n ).
thf(tp_comple825005695real_n,type,
comple825005695real_n: set_se2111327970real_n > set_Fi1058188332real_n ).
thf(tp_comple970917503_int_n,type,
comple970917503_int_n: set_se944069346_int_n > set_Fi160064172_int_n ).
thf(tp_complete_Sup_Sup_o,type,
complete_Sup_Sup_o: set_o > $o ).
thf(tp_counta1142393929_int_n,type,
counta1142393929_int_n: set_Fi160064172_int_n > nat > finite964658038_int_n ).
thf(tp_f,type,
f: nat > finite964658038_int_n ).
thf(tp_image_1054146965real_n,type,
image_1054146965real_n: ( set_Fi160064172_int_n > set_se2111327970real_n ) > set_se944069346_int_n > set_se820660888real_n ).
thf(tp_image_1085873667et_nat,type,
image_1085873667et_nat: ( finite964658038_int_n > set_nat ) > set_Fi160064172_int_n > set_set_nat ).
thf(tp_image_1278151539_int_n,type,
image_1278151539_int_n: ( finite964658038_int_n > finite964658038_int_n ) > set_Fi160064172_int_n > set_Fi160064172_int_n ).
thf(tp_image_1298280374real_n,type,
image_1298280374real_n: ( sigma_1466784463real_n > set_Fi1058188332real_n ) > set_Si1125517487real_n > set_se2111327970real_n ).
thf(tp_image_1587769199real_n,type,
image_1587769199real_n: ( set_nat > set_se2111327970real_n ) > set_set_nat > set_se820660888real_n ).
thf(tp_image_1599934780real_n,type,
image_1599934780real_n: ( $o > sigma_1466784463real_n ) > set_o > set_Si1125517487real_n ).
thf(tp_image_1648361637al_n_o,type,
image_1648361637al_n_o: ( set_Fi1058188332real_n > $o ) > set_se2111327970real_n > set_o ).
thf(tp_image_1661509983real_n,type,
image_1661509983real_n: ( set_Fi1058188332real_n > set_Fi1058188332real_n ) > set_se2111327970real_n > set_se2111327970real_n ).
thf(tp_image_1681970287al_n_o,type,
image_1681970287al_n_o: ( set_se2111327970real_n > $o ) > set_se820660888real_n > set_o ).
thf(tp_image_1687589765_set_o,type,
image_1687589765_set_o: ( set_Fi1058188332real_n > set_o ) > set_se2111327970real_n > set_set_o ).
thf(tp_image_1759008383real_n,type,
image_1759008383real_n: ( $o > set_Fi1058188332real_n ) > set_o > set_se2111327970real_n ).
thf(tp_image_1819506345_int_n,type,
image_1819506345_int_n: ( finite964658038_int_n > set_Fi160064172_int_n ) > set_Fi160064172_int_n > set_se944069346_int_n ).
thf(tp_image_183184717real_n,type,
image_183184717real_n: ( nat > finite1489363574real_n ) > set_nat > set_Fi1058188332real_n ).
thf(tp_image_1856576259real_n,type,
image_1856576259real_n: ( nat > set_Fi1058188332real_n ) > set_nat > set_se2111327970real_n ).
thf(tp_image_1961920973_int_n,type,
image_1961920973_int_n: ( nat > finite964658038_int_n ) > set_nat > set_Fi160064172_int_n ).
thf(tp_image_2058828787real_n,type,
image_2058828787real_n: ( finite964658038_int_n > finite1489363574real_n ) > set_Fi160064172_int_n > set_Fi1058188332real_n ).
thf(tp_image_2066995319nnreal,type,
image_2066995319nnreal: ( extend1728876344nnreal > extend1728876344nnreal ) > set_Ex113815278nnreal > set_Ex113815278nnreal ).
thf(tp_image_216309723nt_n_o,type,
image_216309723nt_n_o: ( finite964658038_int_n > $o ) > set_Fi160064172_int_n > set_o ).
thf(tp_image_355963305real_n,type,
image_355963305real_n: ( finite964658038_int_n > set_Fi1058188332real_n ) > set_Fi160064172_int_n > set_se2111327970real_n ).
thf(tp_image_439535603real_n,type,
image_439535603real_n: ( finite1489363574real_n > finite1489363574real_n ) > set_Fi1058188332real_n > set_Fi1058188332real_n ).
thf(tp_image_452144437real_n,type,
image_452144437real_n: ( $o > set_se2111327970real_n ) > set_o > set_se820660888real_n ).
thf(tp_image_497739341_n_nat,type,
image_497739341_n_nat: ( finite964658038_int_n > nat ) > set_Fi160064172_int_n > set_nat ).
thf(tp_image_545463721real_n,type,
image_545463721real_n: ( finite1489363574real_n > set_Fi1058188332real_n ) > set_Fi1058188332real_n > set_se2111327970real_n ).
thf(tp_image_792439519real_n,type,
image_792439519real_n: ( set_Fi160064172_int_n > set_Fi1058188332real_n ) > set_se944069346_int_n > set_se2111327970real_n ).
thf(tp_image_797440021real_n,type,
image_797440021real_n: ( set_Fi1058188332real_n > set_se2111327970real_n ) > set_se2111327970real_n > set_se820660888real_n ).
thf(tp_image_933134521real_n,type,
image_933134521real_n: ( set_nat > set_Fi1058188332real_n ) > set_set_nat > set_se2111327970real_n ).
thf(tp_image_968789251_int_n,type,
image_968789251_int_n: ( nat > set_Fi160064172_int_n ) > set_nat > set_se944069346_int_n ).
thf(tp_image_987430492real_n,type,
image_987430492real_n: ( set_Fi1058188332real_n > sigma_1466784463real_n ) > set_se2111327970real_n > set_Si1125517487real_n ).
thf(tp_image_nat_nat,type,
image_nat_nat: ( nat > nat ) > set_nat > set_nat ).
thf(tp_image_nat_o,type,
image_nat_o: ( nat > $o ) > set_nat > set_o ).
thf(tp_image_nat_set_nat,type,
image_nat_set_nat: ( nat > set_nat ) > set_nat > set_set_nat ).
thf(tp_image_o_o,type,
image_o_o: ( $o > $o ) > set_o > set_o ).
thf(tp_image_o_set_o,type,
image_o_set_o: ( $o > set_o ) > set_o > set_set_o ).
thf(tp_image_set_o_o,type,
image_set_o_o: ( set_o > $o ) > set_set_o > set_o ).
thf(tp_inf_in1108485182_int_n,type,
inf_in1108485182_int_n: set_Fi160064172_int_n > set_Fi160064172_int_n > set_Fi160064172_int_n ).
thf(tp_inf_in1974387902real_n,type,
inf_in1974387902real_n: set_Fi1058188332real_n > set_Fi1058188332real_n > set_Fi1058188332real_n ).
thf(tp_inf_in632889204real_n,type,
inf_in632889204real_n: set_se2111327970real_n > set_se2111327970real_n > set_se2111327970real_n ).
thf(tp_inf_inf_set_nat,type,
inf_inf_set_nat: set_nat > set_nat > set_nat ).
thf(tp_inf_inf_set_o,type,
inf_inf_set_o: set_o > set_o > set_o ).
thf(tp_lebesg260170249real_n,type,
lebesg260170249real_n: sigma_1466784463real_n ).
thf(tp_measur1402256771real_n,type,
measur1402256771real_n: sigma_1466784463real_n > set_se2111327970real_n ).
thf(tp_measur2126959417real_n,type,
measur2126959417real_n: sigma_1422848389real_n > set_se820660888real_n ).
thf(tp_measure_null_sets_o,type,
measure_null_sets_o: sigma_measure_o > set_set_o ).
thf(tp_member1000184real_n,type,
member1000184real_n: sigma_1466784463real_n > set_Si1125517487real_n > $o ).
thf(tp_member1217042383nnreal,type,
member1217042383nnreal: extend1728876344nnreal > set_Ex113815278nnreal > $o ).
thf(tp_member1352538125real_n,type,
member1352538125real_n: finite1489363574real_n > set_Fi1058188332real_n > $o ).
thf(tp_member1475136633real_n,type,
member1475136633real_n: set_se2111327970real_n > set_se820660888real_n > $o ).
thf(tp_member223413699real_n,type,
member223413699real_n: set_Fi1058188332real_n > set_se2111327970real_n > $o ).
thf(tp_member27055245_int_n,type,
member27055245_int_n: finite964658038_int_n > set_Fi160064172_int_n > $o ).
thf(tp_member_nat,type,
member_nat: nat > set_nat > $o ).
thf(tp_member_o,type,
member_o: $o > set_o > $o ).
thf(tp_member_set_o,type,
member_set_o: set_o > set_set_o > $o ).
thf(tp_minkow1134813771n_real,type,
minkow1134813771n_real: finite964658038_int_n > finite1489363574real_n ).
thf(tp_minus_1037315151real_n,type,
minus_1037315151real_n: finite1489363574real_n > finite1489363574real_n > finite1489363574real_n ).
thf(tp_minus_1196255695_int_n,type,
minus_1196255695_int_n: finite964658038_int_n > finite964658038_int_n > finite964658038_int_n ).
thf(tp_minus_1686442501real_n,type,
minus_1686442501real_n: set_Fi1058188332real_n > set_Fi1058188332real_n > set_Fi1058188332real_n ).
thf(tp_one_on1253059131real_n,type,
one_on1253059131real_n: finite1489363574real_n ).
thf(tp_one_on705384445nnreal,type,
one_on705384445nnreal: extend1728876344nnreal ).
thf(tp_ord_le2133614988nnreal,type,
ord_le2133614988nnreal: extend1728876344nnreal > extend1728876344nnreal > $o ).
thf(tp_plus_p1654784127_int_n,type,
plus_p1654784127_int_n: finite964658038_int_n > finite964658038_int_n > finite964658038_int_n ).
thf(tp_plus_p1763960001nnreal,type,
plus_p1763960001nnreal: extend1728876344nnreal > extend1728876344nnreal > extend1728876344nnreal ).
thf(tp_plus_p585657087real_n,type,
plus_p585657087real_n: finite1489363574real_n > finite1489363574real_n > finite1489363574real_n ).
thf(tp_r,type,
r: finite964658038_int_n > set_Fi1058188332real_n ).
thf(tp_s,type,
s: set_Fi1058188332real_n ).
thf(tp_sK1_SV2,type,
sK1_SV2: nat ).
thf(tp_sigma_1235138647real_n,type,
sigma_1235138647real_n: sigma_1466784463real_n > set_se2111327970real_n ).
thf(tp_sigma_1536574303real_n,type,
sigma_1536574303real_n: sigma_1466784463real_n > set_Fi1058188332real_n > extend1728876344nnreal ).
thf(tp_sigma_476185326real_n,type,
sigma_476185326real_n: sigma_1466784463real_n > set_Fi1058188332real_n ).
thf(tp_sigma_607186084real_n,type,
sigma_607186084real_n: sigma_1422848389real_n > set_se2111327970real_n ).
thf(tp_sigma_space_o,type,
sigma_space_o: sigma_measure_o > set_o ).
thf(tp_sums_E1192373732nnreal,type,
sums_E1192373732nnreal: ( nat > extend1728876344nnreal ) > extend1728876344nnreal > $o ).
thf(tp_t,type,
t: finite964658038_int_n > set_Fi1058188332real_n ).
thf(tp_t2,type,
t2: finite964658038_int_n > set_Fi1058188332real_n ).
thf(tp_top_to1292442332real_n,type,
top_to1292442332real_n: set_Fi1058188332real_n ).
thf(tp_top_to131672412_int_n,type,
top_to131672412_int_n: set_Fi160064172_int_n ).
thf(tp_top_to1587634578_int_n,type,
top_to1587634578_int_n: set_se944069346_int_n ).
thf(tp_top_to1845833192nnreal,type,
top_to1845833192nnreal: extend1728876344nnreal ).
thf(tp_top_to20708754real_n,type,
top_to20708754real_n: set_se2111327970real_n ).
thf(tp_top_to287930409nt_n_o,type,
top_to287930409nt_n_o: finite964658038_int_n > $o ).
thf(tp_top_top_nat_o,type,
top_top_nat_o: nat > $o ).
thf(tp_top_top_o,type,
top_top_o: $o ).
thf(tp_top_top_set_nat,type,
top_top_set_nat: set_nat ).
thf(tp_top_top_set_o,type,
top_top_set_o: set_o ).
thf(tp_top_top_set_set_nat,type,
top_top_set_set_nat: set_set_nat ).
thf(tp_vimage1122713129_int_n,type,
vimage1122713129_int_n: ( finite964658038_int_n > finite964658038_int_n ) > set_Fi160064172_int_n > set_Fi160064172_int_n ).
thf(tp_vimage1233683625real_n,type,
vimage1233683625real_n: ( finite1489363574real_n > finite1489363574real_n ) > set_Fi1058188332real_n > set_Fi1058188332real_n ).
thf(tp_vimage1276736425real_n,type,
vimage1276736425real_n: ( finite964658038_int_n > finite1489363574real_n ) > set_Fi1058188332real_n > set_Fi160064172_int_n ).
thf(tp_vimage1398021123_n_nat,type,
vimage1398021123_n_nat: ( finite964658038_int_n > nat ) > set_nat > set_Fi160064172_int_n ).
thf(tp_vimage1860757507real_n,type,
vimage1860757507real_n: ( nat > finite1489363574real_n ) > set_Fi1058188332real_n > set_nat ).
thf(tp_vimage3210681real_n,type,
vimage3210681real_n: ( nat > set_Fi1058188332real_n ) > set_se2111327970real_n > set_nat ).
thf(tp_vimage464515423real_n,type,
vimage464515423real_n: ( finite964658038_int_n > set_Fi1058188332real_n ) > set_se2111327970real_n > set_Fi160064172_int_n ).
thf(tp_vimage714719107_int_n,type,
vimage714719107_int_n: ( nat > finite964658038_int_n ) > set_Fi160064172_int_n > set_nat ).
thf(tp_vimage784510485real_n,type,
vimage784510485real_n: ( set_Fi1058188332real_n > set_Fi1058188332real_n ) > set_se2111327970real_n > set_se2111327970real_n ).
thf(tp_vimage851190895al_n_o,type,
vimage851190895al_n_o: ( set_Fi1058188332real_n > $o ) > set_o > set_se2111327970real_n ).
thf(tp_vimage961837641real_n,type,
vimage961837641real_n: ( $o > set_Fi1058188332real_n ) > set_se2111327970real_n > set_o ).
thf(tp_vimage_nat_nat,type,
vimage_nat_nat: ( nat > nat ) > set_nat > set_nat ).
thf(tp_vimage_o_o,type,
vimage_o_o: ( $o > $o ) > set_o > set_o ).
thf(tp_zero_z1963244097nnreal,type,
zero_z1963244097nnreal: extend1728876344nnreal ).
thf(tp_zero_z200130687real_n,type,
zero_z200130687real_n: finite1489363574real_n ).
thf(353,axiom,
! [A: finite964658038_int_n] :
( ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t @ A ) )
= ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t2 @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_emeasure__T_H) ).
thf(354,conjecture,
( ( ^ [N: nat] : ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t2 @ ( f @ N ) ) ) )
= ( ^ [N: nat] : ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t @ ( f @ N ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
thf(355,negated_conjecture,
( ( ( ^ [N: nat] : ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t2 @ ( f @ N ) ) ) )
= ( ^ [N: nat] : ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t @ ( f @ N ) ) ) ) )
= $false ),
inference(negate_conjecture,[status(cth)],[354]) ).
thf(356,plain,
( ( ( ^ [N: nat] : ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t2 @ ( f @ N ) ) ) )
= ( ^ [N: nat] : ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t @ ( f @ N ) ) ) ) )
= $false ),
inference(unfold_def,[status(thm)],[355]) ).
thf(357,plain,
( ( ! [A: finite964658038_int_n] :
( ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t @ A ) )
= ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t2 @ A ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[353]) ).
thf(358,plain,
( ( ( ^ [N: nat] : ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t2 @ ( f @ N ) ) ) )
!= ( ^ [N: nat] : ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t @ ( f @ N ) ) ) ) )
= $true ),
inference(polarity_switch,[status(thm)],[356]) ).
thf(359,plain,
( ( ! [A: finite964658038_int_n] :
( ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t @ A ) )
= ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t2 @ A ) ) ) )
= $true ),
inference(copy,[status(thm)],[357]) ).
thf(360,plain,
( ( ( ^ [N: nat] : ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t2 @ ( f @ N ) ) ) )
!= ( ^ [N: nat] : ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t @ ( f @ N ) ) ) ) )
= $true ),
inference(copy,[status(thm)],[358]) ).
thf(361,plain,
! [SV1: finite964658038_int_n] :
( ( ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t @ SV1 ) )
= ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t2 @ SV1 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[359]) ).
thf(362,plain,
( ( ( ^ [N: nat] : ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t2 @ ( f @ N ) ) ) )
= ( ^ [N: nat] : ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t @ ( f @ N ) ) ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[360]) ).
thf(363,plain,
( ( ! [SV2: nat] :
( ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t2 @ ( f @ SV2 ) ) )
= ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t @ ( f @ SV2 ) ) ) ) )
= $false ),
inference(extcnf_equal_neg,[status(thm)],[362]) ).
thf(364,plain,
( ( ( ^ [N: nat] : ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t2 @ ( f @ N ) ) ) )
= ( ^ [N: nat] : ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t @ ( f @ N ) ) ) ) )
= $false ),
inference(extcnf_equal_neg,[status(thm)],[362]) ).
thf(365,plain,
( ( ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t2 @ ( f @ sK1_SV2 ) ) )
= ( sigma_1536574303real_n @ ( comple230862828real_n @ lebesg260170249real_n ) @ ( t @ ( f @ sK1_SV2 ) ) ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[363]) ).
thf(366,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[361,365,364]) ).
thf(367,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[366]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP117^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.17 % Computer : n009.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Tue Oct 6 11:17:47 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.37/0.59 ..
% 2.37/0.59
% 2.37/0.59 No.of.Axioms: 1
% 2.37/0.59
% 2.37/0.59 Length.of.Defs: 0
% 2.37/0.59
% 2.37/0.59 Contains.Choice.Funs: false
% 2.37/0.59 ...
% 2.37/0.59
% 2.37/0.59 ********************************
% 2.37/0.59 * All subproblems solved! *
% 2.37/0.59 ********************************
% 2.37/0.59 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:1,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:366,loop_count:0,foatp_calls:1,translation:fof_full)
% 2.37/0.59
% 2.37/0.59 %**** Beginning of derivation protocol ****
% 2.37/0.59 % SZS output start CNFRefutation
% See solution above
% 2.37/0.59
% 2.37/0.59 %**** End of derivation protocol ****
% 2.37/0.59 %**** no. of clauses in derivation: 15 ****
% 2.37/0.59 %**** clause counter: 366 ****
% 2.37/0.59
% 2.37/0.59 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:1,axioms:1,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:366,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------