%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP075^1 : TPTP v9.2.0. Released 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:53 PM UTC 2025
% Result : Theorem 2.88s 3.08s
% Output : Proof 2.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ITP075^1 : TPTP v9.2.0. Released v7.5.0.
% 0.03/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n005.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 8 18:35:53 EDT 2025
% 0.12/0.34 % CPUTime :
% 2.88/3.08 % SZS status Theorem
% 2.88/3.08 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 2.88/3.08 % Inferences: 221
% 2.88/3.08 % SZS output start Proof
% 2.88/3.08 thf(ty_hF_Mirabelle_hf, type, hF_Mirabelle_hf : $tType).
% 2.88/3.08 thf(ty_a, type, a : hF_Mirabelle_hf).
% 2.88/3.08 thf(ty_p, type, p : $o).
% 2.88/3.08 thf(ty_hF_Mirabelle_HBex, type, hF_Mirabelle_HBex : (hF_Mirabelle_hf>(hF_Mirabelle_hf>$o)>$o)).
% 2.88/3.08 thf(ty_eigen__4, type, eigen__4 : hF_Mirabelle_hf).
% 2.88/3.08 thf(ty_hF_Mirabelle_hmem, type, hF_Mirabelle_hmem : (hF_Mirabelle_hf>hF_Mirabelle_hf>$o)).
% 2.88/3.08 thf(sP1,plain,sP1 <=> (![X1:hF_Mirabelle_hf>$o]:(![X2:hF_Mirabelle_hf]:(![X3:hF_Mirabelle_hf]:((X1 @ X2) => (((hF_Mirabelle_hmem @ X2) @ X3) => ((hF_Mirabelle_HBex @ X3) @ X1)))))),introduced(definition,[new_symbols(definition,[sP1])])).
% 2.88/3.08 thf(sP2,plain,sP2 <=> ((hF_Mirabelle_hmem @ eigen__4) @ a),introduced(definition,[new_symbols(definition,[sP2])])).
% 2.88/3.08 thf(sP3,plain,sP3 <=> (![X1:hF_Mirabelle_hf]:(![X2:hF_Mirabelle_hf]:(p => (((hF_Mirabelle_hmem @ X1) @ X2) => ((hF_Mirabelle_HBex @ X2) @ (^[X3:hF_Mirabelle_hf]:p)))))),introduced(definition,[new_symbols(definition,[sP3])])).
% 2.88/3.08 thf(sP4,plain,sP4 <=> (![X1:hF_Mirabelle_hf]:(p => (((hF_Mirabelle_hmem @ eigen__4) @ X1) => ((hF_Mirabelle_HBex @ X1) @ (^[X2:hF_Mirabelle_hf]:p))))),introduced(definition,[new_symbols(definition,[sP4])])).
% 2.88/3.08 thf(sP5,plain,sP5 <=> ((hF_Mirabelle_HBex @ a) @ (^[X1:hF_Mirabelle_hf]:p)),introduced(definition,[new_symbols(definition,[sP5])])).
% 2.88/3.08 thf(sP6,plain,sP6 <=> (p => (sP2 => sP5)),introduced(definition,[new_symbols(definition,[sP6])])).
% 2.88/3.08 thf(sP7,plain,sP7 <=> (sP2 => sP5),introduced(definition,[new_symbols(definition,[sP7])])).
% 2.88/3.08 thf(sP8,plain,sP8 <=> p,introduced(definition,[new_symbols(definition,[sP8])])).
% 2.88/3.08 thf(conj_0,conjecture,(sP5 = (~(((~((![X1:hF_Mirabelle_hf]:(~(((hF_Mirabelle_hmem @ X1) @ a)))))) => (~(sP8))))))).
% 2.88/3.08 thf(h0,negated_conjecture,(~((sP5 = (~(((~((![X1:hF_Mirabelle_hf]:(~(((hF_Mirabelle_hmem @ X1) @ a)))))) => (~(sP8)))))))),inference(assume_negation,[status(cth)],[conj_0])).
% 2.88/3.08 thf(h1,assumption,sP5,introduced(assumption,[])).
% 2.88/3.08 thf(h2,assumption,(~(((~((![X1:hF_Mirabelle_hf]:(~(((hF_Mirabelle_hmem @ X1) @ a)))))) => (~(sP8))))),introduced(assumption,[])).
% 2.88/3.08 thf(h3,assumption,(~(sP5)),introduced(assumption,[])).
% 2.88/3.08 thf(h4,assumption,((~((![X1:hF_Mirabelle_hf]:(~(((hF_Mirabelle_hmem @ X1) @ a)))))) => (~(sP8))),introduced(assumption,[])).
% 2.88/3.08 thf(h5,assumption,(![X1:hF_Mirabelle_hf]:(~(((hF_Mirabelle_hmem @ X1) @ a)))),introduced(assumption,[])).
% 2.88/3.08 thf(h6,assumption,(~(sP8)),introduced(assumption,[])).
% 2.88/3.08 thf(ax42, axiom, (~(p3)|p161), file('<stdin>', ax42)).
% 2.88/3.08 thf(ax44, axiom, (~(p160)|~(p38)|~(p159)), file('<stdin>', ax44)).
% 2.88/3.08 thf(ax43, axiom, (~(p161)|p160), file('<stdin>', ax43)).
% 2.88/3.08 thf(ax206, axiom, p3, file('<stdin>', ax206)).
% 2.88/3.08 thf(ax171, axiom, p38, file('<stdin>', ax171)).
% 2.88/3.08 thf(pax37, axiom, (p37=>![X4:hF_Mirabelle_hf]:~(fhF_Mirabelle_hmem @ X4 @ fa)), file('<stdin>', pax37)).
% 2.88/3.08 thf(nax159, axiom, (p159<=![X1:hF_Mirabelle_hf]:(fhF_Mirabelle_hmem @ X1 @ fa=>~(fp))), file('<stdin>', nax159)).
% 2.88/3.08 thf(ax172, axiom, p37, file('<stdin>', ax172)).
% 2.88/3.08 thf(c_0_8, plain, (~p3|p161), inference(fof_simplification,[status(thm)],[ax42])).
% 2.88/3.08 thf(c_0_9, plain, (~p160|~p38|~p159), inference(fof_simplification,[status(thm)],[ax44])).
% 2.88/3.08 thf(c_0_10, plain, (~p161|p160), inference(fof_simplification,[status(thm)],[ax43])).
% 2.88/3.08 thf(c_0_11, plain, (p161|~p3), inference(split_conjunct,[status(thm)],[c_0_8])).
% 2.88/3.08 thf(c_0_12, plain, p3, inference(split_conjunct,[status(thm)],[ax206])).
% 2.88/3.08 thf(c_0_13, plain, (~p160|~p38|~p159), inference(split_conjunct,[status(thm)],[c_0_9])).
% 2.88/3.08 thf(c_0_14, plain, p38, inference(split_conjunct,[status(thm)],[ax171])).
% 2.88/3.08 thf(c_0_15, plain, (p160|~p161), inference(split_conjunct,[status(thm)],[c_0_10])).
% 2.88/3.08 thf(c_0_16, plain, p161, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_11, c_0_12])])).
% 2.88/3.08 thf(c_0_17, plain, ![X207:hF_Mirabelle_hf]:(~p37|~fhF_Mirabelle_hmem @ X207 @ fa), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax37])])])])).
% 2.88/3.08 thf(c_0_18, plain, ((fhF_Mirabelle_hmem @ esk1_0 @ fa|p159)&(fp|p159)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax159])])])])])).
% 2.88/3.08 thf(c_0_19, plain, (~p159|~p160), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_13, c_0_14])])).
% 2.88/3.08 thf(c_0_20, plain, p160, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_15, c_0_16])])).
% 2.88/3.08 thf(c_0_21, plain, ![X1:hF_Mirabelle_hf]:(~p37|~fhF_Mirabelle_hmem @ X1 @ fa), inference(split_conjunct,[status(thm)],[c_0_17])).
% 2.88/3.08 thf(c_0_22, plain, p37, inference(split_conjunct,[status(thm)],[ax172])).
% 2.88/3.08 thf(c_0_23, plain, (fhF_Mirabelle_hmem @ esk1_0 @ fa|p159), inference(split_conjunct,[status(thm)],[c_0_18])).
% 2.88/3.08 thf(c_0_24, plain, ~p159, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_20])])).
% 2.88/3.08 thf(c_0_25, plain, ![X1:hF_Mirabelle_hf]:~fhF_Mirabelle_hmem @ X1 @ fa, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_22])])).
% 2.88/3.08 thf(c_0_26, plain, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_23, c_0_24]), c_0_25]), ['proof']).
% 2.88/3.08 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h5,h1,h2,h0])],[])).
% 2.88/3.08 thf(ax187, axiom, (~(p3)|p161), file('<stdin>', ax187)).
% 2.88/3.08 thf(ax189, axiom, (~(p160)|~(p38)|~(p159)), file('<stdin>', ax189)).
% 2.88/3.08 thf(ax188, axiom, (~(p161)|p160), file('<stdin>', ax188)).
% 2.88/3.08 thf(ax225, axiom, p3, file('<stdin>', ax225)).
% 2.88/3.08 thf(ax190, axiom, p38, file('<stdin>', ax190)).
% 2.88/3.08 thf(nax159, axiom, (p159<=![X1:hF_Mirabelle_hf]:(fhF_Mirabelle_hmem @ X1 @ fa=>~(fp))), file('<stdin>', nax159)).
% 2.88/3.08 thf(nax208, axiom, (p208<=fp), file('<stdin>', nax208)).
% 2.88/3.08 thf(ax191, axiom, ~(p208), file('<stdin>', ax191)).
% 2.88/3.08 thf(c_0_8, plain, (~p3|p161), inference(fof_simplification,[status(thm)],[ax187])).
% 2.88/3.08 thf(c_0_9, plain, (~p160|~p38|~p159), inference(fof_simplification,[status(thm)],[ax189])).
% 2.88/3.08 thf(c_0_10, plain, (~p161|p160), inference(fof_simplification,[status(thm)],[ax188])).
% 2.88/3.08 thf(c_0_11, plain, (p161|~p3), inference(split_conjunct,[status(thm)],[c_0_8])).
% 2.88/3.08 thf(c_0_12, plain, p3, inference(split_conjunct,[status(thm)],[ax225])).
% 2.88/3.08 thf(c_0_13, plain, (~p160|~p38|~p159), inference(split_conjunct,[status(thm)],[c_0_9])).
% 2.88/3.08 thf(c_0_14, plain, p38, inference(split_conjunct,[status(thm)],[ax190])).
% 2.88/3.08 thf(c_0_15, plain, (p160|~p161), inference(split_conjunct,[status(thm)],[c_0_10])).
% 2.88/3.08 thf(c_0_16, plain, p161, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_11, c_0_12])])).
% 2.88/3.08 thf(c_0_17, plain, ((fhF_Mirabelle_hmem @ esk3_0 @ fa|p159)&(fp|p159)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax159])])])])])).
% 2.88/3.08 thf(c_0_18, plain, (~p159|~p160), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_13, c_0_14])])).
% 2.88/3.08 thf(c_0_19, plain, p160, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_15, c_0_16])])).
% 2.88/3.08 thf(c_0_20, plain, (~fp|p208), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax208])])).
% 2.88/3.08 thf(c_0_21, plain, (fp|p159), inference(split_conjunct,[status(thm)],[c_0_17])).
% 2.88/3.08 thf(c_0_22, plain, ~p159, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18, c_0_19])])).
% 2.88/3.08 thf(c_0_23, plain, ~p208, inference(fof_simplification,[status(thm)],[ax191])).
% 2.88/3.08 thf(c_0_24, plain, (p208|~fp), inference(split_conjunct,[status(thm)],[c_0_20])).
% 2.88/3.08 thf(c_0_25, plain, fp, inference(sr,[status(thm)],[c_0_21, c_0_22])).
% 2.88/3.08 thf(c_0_26, plain, ~p208, inference(split_conjunct,[status(thm)],[c_0_23])).
% 2.88/3.08 thf(c_0_27, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25])]), c_0_26]), ['proof']).
% 2.88/3.08 thf(2,plain,$false,inference(eprover,[status(thm),assumptions([h6,h1,h2,h0])],[])).
% 2.88/3.08 thf(3,plain,$false,inference(tab_imp,[status(thm),assumptions([h1,h2,h0]),tab_imp(discharge,[h5]),tab_imp(discharge,[h6])],[h2,1,2,h5,h6])).
% 2.88/3.08 thf(h7,assumption,(~((![X1:hF_Mirabelle_hf]:(~(((hF_Mirabelle_hmem @ X1) @ a)))))),introduced(assumption,[])).
% 2.88/3.08 thf(h8,assumption,sP8,introduced(assumption,[])).
% 2.88/3.08 thf(h9,assumption,sP2,introduced(assumption,[])).
% 2.88/3.08 thf(4,plain,(~(sP3) | sP4),inference(all_rule,[status(thm)],[])).
% 2.88/3.08 thf(5,plain,(~(sP4) | sP6),inference(all_rule,[status(thm)],[])).
% 2.88/3.08 thf(6,plain,((~(sP6) | ~(sP8)) | sP7),inference(prop_rule,[status(thm)],[])).
% 2.88/3.08 thf(7,plain,((~(sP7) | ~(sP2)) | sP5),inference(prop_rule,[status(thm)],[])).
% 2.88/3.08 thf(8,plain,(~(sP1) | sP3),inference(all_rule,[status(thm)],[])).
% 2.88/3.08 thf(fact_1_hbexI,axiom,sP1).
% 2.88/3.08 thf(9,plain,$false,inference(prop_unsat,[status(thm),assumptions([h9,h7,h8,h3,h4,h0])],[4,5,6,7,8,h3,h9,h8,fact_1_hbexI])).
% 2.88/3.08 thf(10,plain,$false,inference(tab_negall,[status(thm),assumptions([h7,h8,h3,h4,h0]),tab_negall(discharge,[h9]),tab_negall(eigenvar,eigen__4)],[h7,9,h9])).
% 2.88/3.08 thf(11,plain,$false,inference(tab_negimp,[status(thm),assumptions([h3,h4,h0]),tab_negimp(discharge,[h7,h8])],[h4,10,h7,h8])).
% 2.88/3.08 thf(12,plain,$false,inference(tab_be,[status(thm),assumptions([h0]),tab_be(discharge,[h1,h2]),tab_be(discharge,[h3,h4])],[h0,3,11,h1,h2,h3,h4])).
% 2.88/3.08 thf(0,theorem,(sP5 = (~(((~((![X1:hF_Mirabelle_hf]:(~(((hF_Mirabelle_hmem @ X1) @ a)))))) => (~(sP8)))))),inference(contra,[status(thm),contra(discharge,[h0])],[12,h0])).
% 2.88/3.08 % SZS output end Proof
%------------------------------------------------------------------------------