%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP023^2 : TPTP v9.2.0. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 9 01:46:42 PM UTC 2025
% Result : Theorem 0.20s 0.45s
% Output : Proof 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ITP023^2 : TPTP v9.2.0. Bugfixed v7.5.0.
% 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n005.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 8 18:06:53 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.20/0.45 % SZS status Theorem
% 0.20/0.45 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 0.20/0.45 % Inferences: 7
% 0.20/0.45 % SZS output start Proof
% 0.20/0.45 thf(ty_del, type, del : $tType).
% 0.20/0.45 thf(ty_tp__ty_2Erealax_2Ereal, type, tp__ty_2Erealax_2Ereal : $tType).
% 0.20/0.45 thf(ty_p, type, p : ($i>$o)).
% 0.20/0.45 thf(ty_c_2Ereal__topology_2Eball, type, c_2Ereal__topology_2Eball : $i).
% 0.20/0.45 thf(ty_mem, type, mem : ($i>del>$o)).
% 0.20/0.45 thf(ty_c_2Epair_2E_2C, type, c_2Epair_2E_2C : (del>del>$i)).
% 0.20/0.45 thf(ty_eigen__1, type, eigen__1 : tp__ty_2Erealax_2Ereal).
% 0.20/0.45 thf(ty_inj__ty_2Erealax_2Ereal, type, inj__ty_2Erealax_2Ereal : (tp__ty_2Erealax_2Ereal>$i)).
% 0.20/0.45 thf(ty_eigen__0, type, eigen__0 : tp__ty_2Erealax_2Ereal).
% 0.20/0.45 thf(ty_ap, type, ap : ($i>$i>$i)).
% 0.20/0.45 thf(ty_bool, type, bool : del).
% 0.20/0.45 thf(ty_ty_2Erealax_2Ereal, type, ty_2Erealax_2Ereal : del).
% 0.20/0.45 thf(ty_c_2Ereal__topology_2Ebounded__def, type, c_2Ereal__topology_2Ebounded__def : $i).
% 0.20/0.45 thf(conj_thm_2Ereal__topology_2EBOUNDED__BALL,conjecture,(![X1:tp__ty_2Erealax_2Ereal]:(![X2:tp__ty_2Erealax_2Ereal]:(p @ ((ap @ c_2Ereal__topology_2Ebounded__def) @ ((ap @ c_2Ereal__topology_2Eball) @ ((ap @ ((ap @ ((c_2Epair_2E_2C @ ty_2Erealax_2Ereal) @ ty_2Erealax_2Ereal)) @ (inj__ty_2Erealax_2Ereal @ X1))) @ (inj__ty_2Erealax_2Ereal @ X2)))))))).
% 0.20/0.45 thf(h0,negated_conjecture,(~((![X1:tp__ty_2Erealax_2Ereal]:(![X2:tp__ty_2Erealax_2Ereal]:(p @ ((ap @ c_2Ereal__topology_2Ebounded__def) @ ((ap @ c_2Ereal__topology_2Eball) @ ((ap @ ((ap @ ((c_2Epair_2E_2C @ ty_2Erealax_2Ereal) @ ty_2Erealax_2Ereal)) @ (inj__ty_2Erealax_2Ereal @ X1))) @ (inj__ty_2Erealax_2Ereal @ X2))))))))),inference(assume_negation,[status(cth)],[conj_thm_2Ereal__topology_2EBOUNDED__BALL])).
% 0.20/0.45 thf(h1,assumption,(~((![X1:tp__ty_2Erealax_2Ereal]:(p @ ((ap @ c_2Ereal__topology_2Ebounded__def) @ ((ap @ c_2Ereal__topology_2Eball) @ ((ap @ ((ap @ ((c_2Epair_2E_2C @ ty_2Erealax_2Ereal) @ ty_2Erealax_2Ereal)) @ (inj__ty_2Erealax_2Ereal @ eigen__0))) @ (inj__ty_2Erealax_2Ereal @ X1)))))))),introduced(assumption,[])).
% 0.20/0.45 thf(h2,assumption,(~((p @ ((ap @ c_2Ereal__topology_2Ebounded__def) @ ((ap @ c_2Ereal__topology_2Eball) @ ((ap @ ((ap @ ((c_2Epair_2E_2C @ ty_2Erealax_2Ereal) @ ty_2Erealax_2Ereal)) @ (inj__ty_2Erealax_2Ereal @ eigen__0))) @ (inj__ty_2Erealax_2Ereal @ eigen__1))))))),introduced(assumption,[])).
% 0.20/0.45 thf(h3,assumption,(~(((![X1:$i]:(((mem @ X1) @ bool) => ((p @ X1) = (p @ X1)))) => (~(($false = $false)))))),introduced(assumption,[])).
% 0.20/0.45 thf(h4,assumption,((~($false)) = (~($false))),introduced(assumption,[])).
% 0.20/0.45 thf(h5,assumption,(![X1:$i]:(((mem @ X1) @ bool) => ((p @ X1) = (p @ X1)))),introduced(assumption,[])).
% 0.20/0.45 thf(h6,assumption,($false = $false),introduced(assumption,[])).
% 0.20/0.45 thf(h7,assumption,$false,introduced(assumption,[])).
% 0.20/0.45 thf(h8,assumption,(~($false)),introduced(assumption,[])).
% 0.20/0.45 thf(1,plain,$false,inference(tab_false,[status(thm),assumptions([h7,h7,h5,h6,h3,h4,h2,h1,h0])],[h7])).
% 0.20/0.45 thf(pax2, axiom, (p2=>![X15:del, X18:del, X17:$i]:(fmem @ X17 @ (farr @ X15 @ X18)=>![X19:$i]:(fmem @ X19 @ X15=>fmem @ (fap @ X17 @ X19) @ X18))), file('<stdin>', pax2)).
% 0.20/0.45 thf(pax12, axiom, (p12=>![X9:del, X10:del]:fmem @ (fc_2Epair_2E_2C @ X9 @ X10) @ (farr @ X9 @ (farr @ X10 @ (fty_2Epair_2Eprod @ X9 @ X10)))), file('<stdin>', pax12)).
% 0.20/0.45 thf(pax31, axiom, (p31=>![X4:$i]:(fmem @ X4 @ (farr @ fty_2Erealax_2Ereal @ fbool)=>![X5:$i]:(fmem @ X5 @ (farr @ fty_2Erealax_2Ereal @ fbool)=>(~((fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ X5)=>~(fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ fty_2Erealax_2Ereal) @ X4) @ X5))))=>fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ X4))))), file('<stdin>', pax31)).
% 0.20/0.45 thf(pax30, axiom, (p30=>![X6:tp__ty_2Erealax_2Ereal, X7:tp__ty_2Erealax_2Ereal]:fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ fty_2Erealax_2Ereal) @ (fap @ fc_2Ereal__topology_2Eball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X6)) @ (finj__ty_2Erealax_2Ereal @ X7)))) @ (fap @ fc_2Ereal__topology_2Ecball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X6)) @ (finj__ty_2Erealax_2Ereal @ X7))))), file('<stdin>', pax30)).
% 0.20/0.45 thf(pax32, axiom, (p32=>![X2:tp__ty_2Erealax_2Ereal, X3:tp__ty_2Erealax_2Ereal]:fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ (fap @ fc_2Ereal__topology_2Ecball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X2)) @ (finj__ty_2Erealax_2Ereal @ X3))))), file('<stdin>', pax32)).
% 0.20/0.45 thf(pax13, axiom, (p13=>fmem @ fc_2Ereal__topology_2Ecball @ (farr @ (fty_2Epair_2Eprod @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (farr @ fty_2Erealax_2Ereal @ fbool))), file('<stdin>', pax13)).
% 0.20/0.45 thf(ax115, axiom, p2, file('<stdin>', ax115)).
% 0.20/0.45 thf(ax105, axiom, p12, file('<stdin>', ax105)).
% 0.20/0.45 thf(nax41, axiom, (p41<=fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ (fap @ fc_2Ereal__topology_2Eball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ f__0)) @ (finj__ty_2Erealax_2Ereal @ f__1))))), file('<stdin>', nax41)).
% 0.20/0.45 thf(ax76, axiom, ~(p41), file('<stdin>', ax76)).
% 0.20/0.45 thf(ax86, axiom, p31, file('<stdin>', ax86)).
% 0.20/0.45 thf(ax87, axiom, p30, file('<stdin>', ax87)).
% 0.20/0.45 thf(ax85, axiom, p32, file('<stdin>', ax85)).
% 0.20/0.45 thf(ax104, axiom, p13, file('<stdin>', ax104)).
% 0.20/0.45 thf(pax11, axiom, (p11=>fmem @ fc_2Ereal__topology_2Eball @ (farr @ (fty_2Epair_2Eprod @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (farr @ fty_2Erealax_2Ereal @ fbool))), file('<stdin>', pax11)).
% 0.20/0.45 thf(pax7, axiom, (p7=>![X14:tp__ty_2Erealax_2Ereal]:fmem @ (finj__ty_2Erealax_2Ereal @ X14) @ fty_2Erealax_2Ereal), file('<stdin>', pax7)).
% 0.20/0.45 thf(ax106, axiom, p11, file('<stdin>', ax106)).
% 0.20/0.45 thf(ax110, axiom, p7, file('<stdin>', ax110)).
% 0.20/0.45 thf(c_0_18, plain, ![X63:del, X64:del, X65:$i, X66:$i]:(~p2|(~fmem @ X65 @ (farr @ X63 @ X64)|(~fmem @ X66 @ X63|fmem @ (fap @ X65 @ X66) @ X64))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax2])])])).
% 0.20/0.45 thf(c_0_19, plain, ![X33:del, X34:del]:(~p12|fmem @ (fc_2Epair_2E_2C @ X33 @ X34) @ (farr @ X33 @ (farr @ X34 @ (fty_2Epair_2Eprod @ X33 @ X34)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax12])])])).
% 0.20/0.45 thf(c_0_20, plain, ![X25:$i, X26:$i]:(~p31|(~fmem @ X25 @ (farr @ fty_2Erealax_2Ereal @ fbool)|(~fmem @ X26 @ (farr @ fty_2Erealax_2Ereal @ fbool)|(~fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ X26)|~fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ fty_2Erealax_2Ereal) @ X25) @ X26)|fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ X25))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax31])])])])).
% 0.20/0.45 thf(c_0_21, plain, ![X29:tp__ty_2Erealax_2Ereal, X30:tp__ty_2Erealax_2Ereal]:(~p30|fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ fty_2Erealax_2Ereal) @ (fap @ fc_2Ereal__topology_2Eball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X29)) @ (finj__ty_2Erealax_2Ereal @ X30)))) @ (fap @ fc_2Ereal__topology_2Ecball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X29)) @ (finj__ty_2Erealax_2Ereal @ X30))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax30])])])).
% 0.20/0.45 thf(c_0_22, plain, ![X21:tp__ty_2Erealax_2Ereal, X22:tp__ty_2Erealax_2Ereal]:(~p32|fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ (fap @ fc_2Ereal__topology_2Ecball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X21)) @ (finj__ty_2Erealax_2Ereal @ X22))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax32])])])).
% 0.20/0.45 thf(c_0_23, plain, (~p13|fmem @ fc_2Ereal__topology_2Ecball @ (farr @ (fty_2Epair_2Eprod @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (farr @ fty_2Erealax_2Ereal @ fbool))), inference(fof_nnf,[status(thm)],[pax13])).
% 0.20/0.45 thf(c_0_24, plain, ![X1:$i, X10:del, X4:$i, X9:del]:(fmem @ (fap @ X1 @ X4) @ X10|~p2|~fmem @ X1 @ (farr @ X9 @ X10)|~fmem @ X4 @ X9), inference(split_conjunct,[status(thm)],[c_0_18])).
% 0.20/0.45 thf(c_0_25, plain, p2, inference(split_conjunct,[status(thm)],[ax115])).
% 0.20/0.45 thf(c_0_26, plain, ![X9:del, X10:del]:(fmem @ (fc_2Epair_2E_2C @ X9 @ X10) @ (farr @ X9 @ (farr @ X10 @ (fty_2Epair_2Eprod @ X9 @ X10)))|~p12), inference(split_conjunct,[status(thm)],[c_0_19])).
% 0.20/0.45 thf(c_0_27, plain, p12, inference(split_conjunct,[status(thm)],[ax105])).
% 0.20/0.45 thf(c_0_28, plain, (~fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ (fap @ fc_2Ereal__topology_2Eball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ f__0)) @ (finj__ty_2Erealax_2Ereal @ f__1))))|p41), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax41])])).
% 0.20/0.45 thf(c_0_29, plain, ~p41, inference(fof_simplification,[status(thm)],[ax76])).
% 0.20/0.45 thf(c_0_30, plain, ![X1:$i, X4:$i]:(fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ X1)|~p31|~fmem @ X1 @ (farr @ fty_2Erealax_2Ereal @ fbool)|~fmem @ X4 @ (farr @ fty_2Erealax_2Ereal @ fbool)|~fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ X4)|~fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ fty_2Erealax_2Ereal) @ X1) @ X4)), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.20/0.45 thf(c_0_31, plain, p31, inference(split_conjunct,[status(thm)],[ax86])).
% 0.20/0.45 thf(c_0_32, plain, ![X2:tp__ty_2Erealax_2Ereal, X3:tp__ty_2Erealax_2Ereal]:(fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ fty_2Erealax_2Ereal) @ (fap @ fc_2Ereal__topology_2Eball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X2)) @ (finj__ty_2Erealax_2Ereal @ X3)))) @ (fap @ fc_2Ereal__topology_2Ecball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X2)) @ (finj__ty_2Erealax_2Ereal @ X3))))|~p30), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.20/0.45 thf(c_0_33, plain, p30, inference(split_conjunct,[status(thm)],[ax87])).
% 0.20/0.45 thf(c_0_34, plain, ![X2:tp__ty_2Erealax_2Ereal, X3:tp__ty_2Erealax_2Ereal]:(fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ (fap @ fc_2Ereal__topology_2Ecball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X2)) @ (finj__ty_2Erealax_2Ereal @ X3))))|~p32), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.20/0.45 thf(c_0_35, plain, p32, inference(split_conjunct,[status(thm)],[ax85])).
% 0.20/0.45 thf(c_0_36, plain, (fmem @ fc_2Ereal__topology_2Ecball @ (farr @ (fty_2Epair_2Eprod @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (farr @ fty_2Erealax_2Ereal @ fbool))|~p13), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.20/0.45 thf(c_0_37, plain, p13, inference(split_conjunct,[status(thm)],[ax104])).
% 0.20/0.45 thf(c_0_38, plain, ![X1:$i, X9:del, X4:$i, X10:del]:(fmem @ (fap @ X1 @ X4) @ X9|~fmem @ X1 @ (farr @ X10 @ X9)|~fmem @ X4 @ X10), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25])])).
% 0.20/0.45 thf(c_0_39, plain, ![X9:del, X10:del]:fmem @ (fc_2Epair_2E_2C @ X9 @ X10) @ (farr @ X9 @ (farr @ X10 @ (fty_2Epair_2Eprod @ X9 @ X10))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_27])])).
% 0.20/0.45 thf(c_0_40, plain, (~p11|fmem @ fc_2Ereal__topology_2Eball @ (farr @ (fty_2Epair_2Eprod @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (farr @ fty_2Erealax_2Ereal @ fbool))), inference(fof_nnf,[status(thm)],[pax11])).
% 0.20/0.45 thf(c_0_41, plain, (p41|~fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ (fap @ fc_2Ereal__topology_2Eball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ f__0)) @ (finj__ty_2Erealax_2Ereal @ f__1))))), inference(split_conjunct,[status(thm)],[c_0_28])).
% 0.20/0.45 thf(c_0_42, plain, ~p41, inference(split_conjunct,[status(thm)],[c_0_29])).
% 0.20/0.45 thf(c_0_43, plain, ![X1:$i, X4:$i]:(fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ X1)|~fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ fty_2Erealax_2Ereal) @ X1) @ X4)|~fmem @ X4 @ (farr @ fty_2Erealax_2Ereal @ fbool)|~fmem @ X1 @ (farr @ fty_2Erealax_2Ereal @ fbool)|~fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ X4)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31])])).
% 0.20/0.45 thf(c_0_44, plain, ![X2:tp__ty_2Erealax_2Ereal, X3:tp__ty_2Erealax_2Ereal]:fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ fty_2Erealax_2Ereal) @ (fap @ fc_2Ereal__topology_2Eball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X2)) @ (finj__ty_2Erealax_2Ereal @ X3)))) @ (fap @ fc_2Ereal__topology_2Ecball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X2)) @ (finj__ty_2Erealax_2Ereal @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_32, c_0_33])])).
% 0.20/0.45 thf(c_0_45, plain, ![X2:tp__ty_2Erealax_2Ereal, X3:tp__ty_2Erealax_2Ereal]:fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ (fap @ fc_2Ereal__topology_2Ecball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X2)) @ (finj__ty_2Erealax_2Ereal @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_34, c_0_35])])).
% 0.20/0.45 thf(c_0_46, plain, fmem @ fc_2Ereal__topology_2Ecball @ (farr @ (fty_2Epair_2Eprod @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (farr @ fty_2Erealax_2Ereal @ fbool)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_36, c_0_37])])).
% 0.20/0.45 thf(c_0_47, plain, ![X1:$i, X10:del, X9:del]:(fmem @ (fap @ (fc_2Epair_2E_2C @ X9 @ X10) @ X1) @ (farr @ X10 @ (fty_2Epair_2Eprod @ X9 @ X10))|~fmem @ X1 @ X9), inference(spm,[status(thm)],[c_0_38, c_0_39])).
% 0.20/0.45 thf(c_0_48, plain, ![X43:tp__ty_2Erealax_2Ereal]:(~p7|fmem @ (finj__ty_2Erealax_2Ereal @ X43) @ fty_2Erealax_2Ereal), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax7])])])).
% 0.20/0.45 thf(c_0_49, plain, (fmem @ fc_2Ereal__topology_2Eball @ (farr @ (fty_2Epair_2Eprod @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (farr @ fty_2Erealax_2Ereal @ fbool))|~p11), inference(split_conjunct,[status(thm)],[c_0_40])).
% 0.20/0.45 thf(c_0_50, plain, p11, inference(split_conjunct,[status(thm)],[ax106])).
% 0.20/0.45 thf(c_0_51, plain, ~fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ (fap @ fc_2Ereal__topology_2Eball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ f__0)) @ (finj__ty_2Erealax_2Ereal @ f__1)))), inference(sr,[status(thm)],[c_0_41, c_0_42])).
% 0.20/0.45 thf(c_0_52, plain, ![X2:tp__ty_2Erealax_2Ereal, X3:tp__ty_2Erealax_2Ereal]:(fp @ (fap @ fc_2Ereal__topology_2Ebounded__def @ (fap @ fc_2Ereal__topology_2Eball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X2)) @ (finj__ty_2Erealax_2Ereal @ X3))))|~fmem @ (fap @ fc_2Ereal__topology_2Ecball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X2)) @ (finj__ty_2Erealax_2Ereal @ X3))) @ (farr @ fty_2Erealax_2Ereal @ fbool)|~fmem @ (fap @ fc_2Ereal__topology_2Eball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ X2)) @ (finj__ty_2Erealax_2Ereal @ X3))) @ (farr @ fty_2Erealax_2Ereal @ fbool)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_44]), c_0_45])])).
% 0.20/0.45 thf(c_0_53, plain, ![X1:$i]:(fmem @ (fap @ fc_2Ereal__topology_2Ecball @ X1) @ (farr @ fty_2Erealax_2Ereal @ fbool)|~fmem @ X1 @ (fty_2Epair_2Eprod @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal)), inference(spm,[status(thm)],[c_0_38, c_0_46])).
% 0.20/0.45 thf(c_0_54, plain, ![X1:$i, X4:$i, X10:del, X9:del]:(fmem @ (fap @ (fap @ (fc_2Epair_2E_2C @ X9 @ X10) @ X1) @ X4) @ (fty_2Epair_2Eprod @ X9 @ X10)|~fmem @ X4 @ X10|~fmem @ X1 @ X9), inference(spm,[status(thm)],[c_0_38, c_0_47])).
% 0.20/0.45 thf(c_0_55, plain, ![X2:tp__ty_2Erealax_2Ereal]:(fmem @ (finj__ty_2Erealax_2Ereal @ X2) @ fty_2Erealax_2Ereal|~p7), inference(split_conjunct,[status(thm)],[c_0_48])).
% 0.20/0.45 thf(c_0_56, plain, p7, inference(split_conjunct,[status(thm)],[ax110])).
% 0.20/0.45 thf(c_0_57, plain, fmem @ fc_2Ereal__topology_2Eball @ (farr @ (fty_2Epair_2Eprod @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (farr @ fty_2Erealax_2Ereal @ fbool)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_49, c_0_50])])).
% 0.20/0.45 thf(c_0_58, plain, (~fmem @ (fap @ fc_2Ereal__topology_2Ecball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ f__0)) @ (finj__ty_2Erealax_2Ereal @ f__1))) @ (farr @ fty_2Erealax_2Ereal @ fbool)|~fmem @ (fap @ fc_2Ereal__topology_2Eball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ f__0)) @ (finj__ty_2Erealax_2Ereal @ f__1))) @ (farr @ fty_2Erealax_2Ereal @ fbool)), inference(spm,[status(thm)],[c_0_51, c_0_52])).
% 0.20/0.45 thf(c_0_59, plain, ![X4:$i, X1:$i]:(fmem @ (fap @ fc_2Ereal__topology_2Ecball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ X1) @ X4)) @ (farr @ fty_2Erealax_2Ereal @ fbool)|~fmem @ X4 @ fty_2Erealax_2Ereal|~fmem @ X1 @ fty_2Erealax_2Ereal), inference(spm,[status(thm)],[c_0_53, c_0_54])).
% 0.20/0.45 thf(c_0_60, plain, ![X2:tp__ty_2Erealax_2Ereal]:fmem @ (finj__ty_2Erealax_2Ereal @ X2) @ fty_2Erealax_2Ereal, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_55, c_0_56])])).
% 0.20/0.45 thf(c_0_61, plain, ![X1:$i]:(fmem @ (fap @ fc_2Ereal__topology_2Eball @ X1) @ (farr @ fty_2Erealax_2Ereal @ fbool)|~fmem @ X1 @ (fty_2Epair_2Eprod @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal)), inference(spm,[status(thm)],[c_0_38, c_0_57])).
% 0.20/0.45 thf(c_0_62, plain, ~fmem @ (fap @ fc_2Ereal__topology_2Eball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ (finj__ty_2Erealax_2Ereal @ f__0)) @ (finj__ty_2Erealax_2Ereal @ f__1))) @ (farr @ fty_2Erealax_2Ereal @ fbool), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_59]), c_0_60]), c_0_60])])).
% 0.20/0.45 thf(c_0_63, plain, ![X4:$i, X1:$i]:(fmem @ (fap @ fc_2Ereal__topology_2Eball @ (fap @ (fap @ (fc_2Epair_2E_2C @ fty_2Erealax_2Ereal @ fty_2Erealax_2Ereal) @ X1) @ X4)) @ (farr @ fty_2Erealax_2Ereal @ fbool)|~fmem @ X4 @ fty_2Erealax_2Ereal|~fmem @ X1 @ fty_2Erealax_2Ereal), inference(spm,[status(thm)],[c_0_61, c_0_54])).
% 0.20/0.45 thf(c_0_64, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_63]), c_0_60]), c_0_60])]), ['proof']).
% 0.20/0.45 thf(2,plain,$false,inference(eprover,[status(thm),assumptions([h8,h8,h8,h8,h5,h6,h3,h4,h2,h1,h0])],[])).
% 0.20/0.45 thf(3,plain,$false,inference(tab_false,[status(thm),assumptions([h7,h7,h8,h8,h5,h6,h3,h4,h2,h1,h0])],[h7])).
% 0.20/0.45 thf(4,plain,$false,inference(tab_bq,[status(thm),assumptions([h8,h8,h5,h6,h3,h4,h2,h1,h0]),tab_bq(discharge,[h8,h8]),tab_bq(discharge,[h7,h7])],[h4,2,3,h8,h8,h7,h7])).
% 0.20/0.45 thf(5,plain,$false,inference(tab_bq,[status(thm),assumptions([h5,h6,h3,h4,h2,h1,h0]),tab_bq(discharge,[h7,h7]),tab_bq(discharge,[h8,h8])],[h6,1,4,h7,h7,h8,h8])).
% 0.20/0.45 thf(6,plain,$false,inference(tab_negimp,[status(thm),assumptions([h3,h4,h2,h1,h0]),tab_negimp(discharge,[h5,h6])],[h3,5,h5,h6])).
% 0.20/0.45 thf(conj_thm_2Ebool_2ENOT__CLAUSES,axiom,(~(((~(((![X1:$i]:(((mem @ X1) @ bool) => ((p @ X1) = (p @ X1)))) => (~(($false = $false)))))) => (~(((~($false)) = (~($false))))))))).
% 0.20/0.45 thf(7,plain,$false,inference(tab_negimp,[status(thm),assumptions([h2,h1,h0]),tab_negimp(discharge,[h3,h4])],[conj_thm_2Ebool_2ENOT__CLAUSES,6,h3,h4])).
% 0.20/0.45 thf(8,plain,$false,inference(tab_negall,[status(thm),assumptions([h1,h0]),tab_negall(discharge,[h2]),tab_negall(eigenvar,eigen__1)],[h1,7,h2])).
% 0.20/0.45 thf(9,plain,$false,inference(tab_negall,[status(thm),assumptions([h0]),tab_negall(discharge,[h1]),tab_negall(eigenvar,eigen__0)],[h0,8,h1])).
% 0.20/0.45 thf(0,theorem,(![X1:tp__ty_2Erealax_2Ereal]:(![X2:tp__ty_2Erealax_2Ereal]:(p @ ((ap @ c_2Ereal__topology_2Ebounded__def) @ ((ap @ c_2Ereal__topology_2Eball) @ ((ap @ ((ap @ ((c_2Epair_2E_2C @ ty_2Erealax_2Ereal) @ ty_2Erealax_2Ereal)) @ (inj__ty_2Erealax_2Ereal @ X1))) @ (inj__ty_2Erealax_2Ereal @ X2))))))),inference(contra,[status(thm),contra(discharge,[h0])],[9,h0])).
% 0.20/0.45 % SZS output end Proof
%------------------------------------------------------------------------------