%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEV267^5 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n019.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 02:56:34 PM UTC 2025
% Result : Theorem 220.77s 220.89s
% Output : Proof 220.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : SEV267^5 : TPTP v9.2.0. Released v4.0.0.
% 0.08/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n019.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 19:24:23 EDT 2025
% 0.12/0.35 % CPUTime :
% 220.77/220.89 % SZS status Theorem
% 220.77/220.89 % Mode: mode518
% 220.77/220.89 % Inferences: 1974
% 220.77/220.89 % SZS output start Proof
% 220.77/220.89 thf(ty_a, type, a : $tType).
% 220.77/220.89 thf(ty_eigen__2, type, eigen__2 : a).
% 220.77/220.89 thf(ty_eigen__1, type, eigen__1 : (a>$o)).
% 220.77/220.89 thf(ty_eigen__0, type, eigen__0 : ((a>$o)>$o)).
% 220.77/220.89 thf(ty_eigen__4, type, eigen__4 : a).
% 220.77/220.89 thf(h0, assumption, (![X1:a>$o]:(![X2:a]:((X1 @ X2) => (X1 @ (eps__0 @ X1))))),introduced(assumption,[])).
% 220.77/220.89 thf(eigendef_eigen__4, definition, eigen__4 = (eps__0 @ (^[X1:a]:(~(((eigen__1 @ X1) => (eigen__1 @ X1)))))), introduced(definition,[new_symbols(definition,[eigen__4])])).
% 220.77/220.89 thf(sP1,plain,sP1 <=> (eigen__1 @ eigen__2),introduced(definition,[new_symbols(definition,[sP1])])).
% 220.77/220.89 thf(sP2,plain,sP2 <=> ((~((![X1:a>$o]:((~(((eigen__0 @ X1) => (~((![X2:a]:((X1 @ X2) => (eigen__1 @ X2)))))))) => (~((X1 @ eigen__2))))))) => (~((![X1:a]:((eigen__1 @ X1) => (eigen__1 @ X1)))))),introduced(definition,[new_symbols(definition,[sP2])])).
% 220.77/220.89 thf(sP3,plain,sP3 <=> (![X1:a>$o]:((~(((eigen__0 @ X1) => (~((![X2:a]:((X1 @ X2) => (eigen__1 @ X2)))))))) => (~((X1 @ eigen__2))))),introduced(definition,[new_symbols(definition,[sP3])])).
% 220.77/220.89 thf(sP4,plain,sP4 <=> (eigen__1 @ eigen__4),introduced(definition,[new_symbols(definition,[sP4])])).
% 220.77/220.89 thf(sP5,plain,sP5 <=> ((eigen__0 @ eigen__1) => (~((![X1:a]:((eigen__1 @ X1) => (eigen__1 @ X1)))))),introduced(definition,[new_symbols(definition,[sP5])])).
% 220.77/220.89 thf(sP6,plain,sP6 <=> (eigen__0 @ eigen__1),introduced(definition,[new_symbols(definition,[sP6])])).
% 220.77/220.89 thf(sP7,plain,sP7 <=> (![X1:a>$o]:((~((![X2:a>$o]:((~(((eigen__0 @ X2) => (~((![X3:a]:((X2 @ X3) => (X1 @ X3)))))))) => (~((X2 @ eigen__2))))))) => (~((![X2:a]:((X1 @ X2) => (eigen__1 @ X2))))))),introduced(definition,[new_symbols(definition,[sP7])])).
% 220.77/220.89 thf(sP8,plain,sP8 <=> (sP4 => sP4),introduced(definition,[new_symbols(definition,[sP8])])).
% 220.77/220.89 thf(sP9,plain,sP9 <=> (![X1:a]:((eigen__1 @ X1) => (eigen__1 @ X1))),introduced(definition,[new_symbols(definition,[sP9])])).
% 220.77/220.89 thf(sP10,plain,sP10 <=> ((~(sP5)) => (~(sP1))),introduced(definition,[new_symbols(definition,[sP10])])).
% 220.77/220.89 thf(cNBHD_THM1_pme,conjecture,(![X1:(a>$o)>$o]:((![X2:a>$o]:(![X3:a>$o]:((~(((![X4:a>$o]:((~(((X1 @ X4) => (~((![X5:a]:((X4 @ X5) => (X2 @ X5)))))))) => (X1 @ X4))) => (~((X3 = (^[X4:a]:(~((![X5:a>$o]:((~(((X1 @ X5) => (~((![X6:a]:((X5 @ X6) => (X2 @ X6)))))))) => (~((X5 @ X4)))))))))))))) => (X1 @ X3)))) => (![X2:a>$o]:((X1 @ X2) = (![X3:a]:((X2 @ X3) => (~((![X4:a>$o]:((~((![X5:a>$o]:((~(((X1 @ X5) => (~((![X6:a]:((X5 @ X6) => (X4 @ X6)))))))) => (~((X5 @ X3))))))) => (~((![X5:a]:((X4 @ X5) => (X2 @ X5)))))))))))))))).
% 220.77/220.89 thf(h1,negated_conjecture,(~((![X1:(a>$o)>$o]:((![X2:a>$o]:(![X3:a>$o]:((~(((![X4:a>$o]:((~(((X1 @ X4) => (~((![X5:a]:((X4 @ X5) => (X2 @ X5)))))))) => (X1 @ X4))) => (~((X3 = (^[X4:a]:(~((![X5:a>$o]:((~(((X1 @ X5) => (~((![X6:a]:((X5 @ X6) => (X2 @ X6)))))))) => (~((X5 @ X4)))))))))))))) => (X1 @ X3)))) => (![X2:a>$o]:((X1 @ X2) = (![X3:a]:((X2 @ X3) => (~((![X4:a>$o]:((~((![X5:a>$o]:((~(((X1 @ X5) => (~((![X6:a]:((X5 @ X6) => (X4 @ X6)))))))) => (~((X5 @ X3))))))) => (~((![X5:a]:((X4 @ X5) => (X2 @ X5))))))))))))))))),inference(assume_negation,[status(cth)],[cNBHD_THM1_pme])).
% 220.77/220.89 thf(h2,assumption,(~(((![X1:a>$o]:(![X2:a>$o]:((~(((![X3:a>$o]:((~(((eigen__0 @ X3) => (~((![X4:a]:((X3 @ X4) => (X1 @ X4)))))))) => (eigen__0 @ X3))) => (~((X2 = (^[X3:a]:(~((![X4:a>$o]:((~(((eigen__0 @ X4) => (~((![X5:a]:((X4 @ X5) => (X1 @ X5)))))))) => (~((X4 @ X3)))))))))))))) => (eigen__0 @ X2)))) => (![X1:a>$o]:((eigen__0 @ X1) = (![X2:a]:((X1 @ X2) => (~((![X3:a>$o]:((~((![X4:a>$o]:((~(((eigen__0 @ X4) => (~((![X5:a]:((X4 @ X5) => (X3 @ X5)))))))) => (~((X4 @ X2))))))) => (~((![X4:a]:((X3 @ X4) => (X1 @ X4)))))))))))))))),introduced(assumption,[])).
% 220.77/220.89 thf(h3,assumption,(![X1:a>$o]:(![X2:a>$o]:((~(((![X3:a>$o]:((~(((eigen__0 @ X3) => (~((![X4:a]:((X3 @ X4) => (X1 @ X4)))))))) => (eigen__0 @ X3))) => (~((X2 = (^[X3:a]:(~((![X4:a>$o]:((~(((eigen__0 @ X4) => (~((![X5:a]:((X4 @ X5) => (X1 @ X5)))))))) => (~((X4 @ X3)))))))))))))) => (eigen__0 @ X2)))),introduced(assumption,[])).
% 220.77/220.89 thf(h4,assumption,(~((![X1:a>$o]:((eigen__0 @ X1) = (![X2:a]:((X1 @ X2) => (~((![X3:a>$o]:((~((![X4:a>$o]:((~(((eigen__0 @ X4) => (~((![X5:a]:((X4 @ X5) => (X3 @ X5)))))))) => (~((X4 @ X2))))))) => (~((![X4:a]:((X3 @ X4) => (X1 @ X4))))))))))))))),introduced(assumption,[])).
% 220.77/220.89 thf(h5,assumption,(~((sP6 = (![X1:a]:((eigen__1 @ X1) => (~((![X2:a>$o]:((~((![X3:a>$o]:((~(((eigen__0 @ X3) => (~((![X4:a]:((X3 @ X4) => (X2 @ X4)))))))) => (~((X3 @ X1))))))) => (~((![X3:a]:((X2 @ X3) => (eigen__1 @ X3)))))))))))))),introduced(assumption,[])).
% 220.77/220.89 thf(h6,assumption,sP6,introduced(assumption,[])).
% 220.77/220.89 thf(h7,assumption,(![X1:a]:((eigen__1 @ X1) => (~((![X2:a>$o]:((~((![X3:a>$o]:((~(((eigen__0 @ X3) => (~((![X4:a]:((X3 @ X4) => (X2 @ X4)))))))) => (~((X3 @ X1))))))) => (~((![X3:a]:((X2 @ X3) => (eigen__1 @ X3))))))))))),introduced(assumption,[])).
% 220.77/220.89 thf(h8,assumption,(~(sP6)),introduced(assumption,[])).
% 220.77/220.89 thf(h9,assumption,(~((![X1:a]:((eigen__1 @ X1) => (~((![X2:a>$o]:((~((![X3:a>$o]:((~(((eigen__0 @ X3) => (~((![X4:a]:((X3 @ X4) => (X2 @ X4)))))))) => (~((X3 @ X1))))))) => (~((![X3:a]:((X2 @ X3) => (eigen__1 @ X3))))))))))))),introduced(assumption,[])).
% 220.77/220.89 thf(h10,assumption,(~((sP1 => (~(sP7))))),introduced(assumption,[])).
% 220.77/220.89 thf(h11,assumption,sP1,introduced(assumption,[])).
% 220.77/220.89 thf(h12,assumption,sP7,introduced(assumption,[])).
% 220.77/220.89 thf(1,plain,(~(sP3) | sP10),inference(all_rule,[status(thm)],[])).
% 220.77/220.89 thf(2,plain,((~(sP10) | sP5) | ~(sP1)),inference(prop_rule,[status(thm)],[])).
% 220.77/220.89 thf(3,plain,((~(sP5) | ~(sP6)) | ~(sP9)),inference(prop_rule,[status(thm)],[])).
% 220.77/220.89 thf(4,plain,(sP8 | ~(sP4)),inference(prop_rule,[status(thm)],[])).
% 220.77/220.89 thf(5,plain,(sP8 | sP4),inference(prop_rule,[status(thm)],[])).
% 220.77/220.89 thf(6,plain,(sP9 | ~(sP8)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__4])).
% 220.77/220.89 thf(7,plain,((~(sP2) | sP3) | ~(sP9)),inference(prop_rule,[status(thm)],[])).
% 220.77/220.89 thf(8,plain,(~(sP7) | sP2),inference(all_rule,[status(thm)],[])).
% 220.77/220.89 thf(9,plain,$false,inference(prop_unsat,[status(thm),assumptions([h11,h12,h10,h6,h7,h5,h3,h4,h2,h1,h0])],[1,2,3,4,5,6,7,8,h6,h11,h12])).
% 220.77/220.89 thf(10,plain,$false,inference(tab_negimp,[status(thm),assumptions([h10,h6,h7,h5,h3,h4,h2,h1,h0]),tab_negimp(discharge,[h11,h12])],[h10,9,h11,h12])).
% 220.77/220.89 thf(11,plain,$false,inference(tab_negall,[status(thm),assumptions([h6,h7,h5,h3,h4,h2,h1,h0]),tab_negall(discharge,[h10]),tab_negall(eigenvar,eigen__2)],[h7,10,h10])).
% 220.77/220.89 thf(ax2521, axiom, (~(p4)|p6), file('<stdin>', ax2521)).
% 220.77/220.89 thf(ax2518, axiom, (~(p6)|p8), file('<stdin>', ax2518)).
% 220.77/220.89 thf(ax2522, axiom, p4, file('<stdin>', ax2522)).
% 220.77/220.89 thf(ax2519, axiom, (~(p8)|p12|p3), file('<stdin>', ax2519)).
% 220.77/220.89 thf(ax2523, axiom, ~(p3), file('<stdin>', ax2523)).
% 220.77/220.89 thf(ax2520, axiom, (~(p12)|~(p7)|~(p27)), file('<stdin>', ax2520)).
% 220.77/220.89 thf(ax2492, axiom, (p27|~(p51)), file('<stdin>', ax2492)).
% 220.77/220.89 thf(ax2491, axiom, (p51|~(p52)), file('<stdin>', ax2491)).
% 220.77/220.89 thf(ax2459, axiom, (p7|~(p77)), file('<stdin>', ax2459)).
% 220.77/220.89 thf(ax2458, axiom, (p77|~(p78)), file('<stdin>', ax2458)).
% 220.77/220.89 thf(ax2457, axiom, (p77|~(p79)), file('<stdin>', ax2457)).
% 220.77/220.89 thf(ax2478, axiom, (p60|~(p62)), file('<stdin>', ax2478)).
% 220.77/220.89 thf(ax2474, axiom, (p62|~(p66)), file('<stdin>', ax2474)).
% 220.77/220.89 thf(ax2476, axiom, (~(p26)|p64), file('<stdin>', ax2476)).
% 220.77/220.89 thf(ax2312, axiom, (p78|p79), file('<stdin>', ax2312)).
% 220.77/220.89 thf(ax2477, axiom, (~(p64)|~(p59)|~(p63)), file('<stdin>', ax2477)).
% 220.77/220.89 thf(ax2524, axiom, p26, file('<stdin>', ax2524)).
% 220.77/220.89 thf(ax2469, axiom, (p65|~(p70)), file('<stdin>', ax2469)).
% 220.77/220.89 thf(ax2289, axiom, (p70|~(p218)), file('<stdin>', ax2289)).
% 220.77/220.89 thf(ax1984, axiom, (~(p463)|~(p67)|p59), file('<stdin>', ax1984)).
% 220.77/220.89 thf(ax1983, axiom, (~(p228)|p463), file('<stdin>', ax1983)).
% 220.77/220.89 thf(ax2483, axiom, (p52|p59|~(p60)), file('<stdin>', ax2483)).
% 220.77/220.89 thf(ax2279, axiom, (p66|p228), file('<stdin>', ax2279)).
% 220.77/220.89 thf(ax2475, axiom, (p63|~(p65)), file('<stdin>', ax2475)).
% 220.77/220.89 thf(ax2208, axiom, (p218|~(p283)), file('<stdin>', ax2208)).
% 220.77/220.89 thf(ax2473, axiom, (p62|p67), file('<stdin>', ax2473)).
% 220.77/220.89 thf(ax2207, axiom, (p218|p284), file('<stdin>', ax2207)).
% 220.77/220.89 thf(ax2482, axiom, (p52|~(p59)|p60), file('<stdin>', ax2482)).
% 220.77/220.89 thf(ax1935, axiom, (p283|p495), file('<stdin>', ax1935)).
% 220.77/220.89 thf(ax1483, axiom, (~(p60)|p867), file('<stdin>', ax1483)).
% 220.77/220.89 thf(ax1493, axiom, (~(p862)|~(p495)|~(p861)), file('<stdin>', ax1493)).
% 220.77/220.89 thf(ax1484, axiom, (~(p867)|p862|~(p284)), file('<stdin>', ax1484)).
% 220.77/220.89 thf(ax1934, axiom, (p283|p496), file('<stdin>', ax1934)).
% 220.77/220.89 thf(ax2468, axiom, (p65|p71), file('<stdin>', ax2468)).
% 220.77/220.89 thf(pax496, axiom, (p496=>![X1:a]:(f__22 @ X1=>f__10 @ X1)), file('<stdin>', pax496)).
% 220.77/220.89 thf(nax861, axiom, (p861<=![X1:a]:(f__22 @ X1=>f__1 @ X1)), file('<stdin>', nax861)).
% 220.77/220.89 thf(pax71, axiom, (p71=>![X1:a]:(f__10 @ X1=>f__1 @ X1)), file('<stdin>', pax71)).
% 220.77/220.89 thf(c_0_37, plain, (~p4|p6), inference(fof_simplification,[status(thm)],[ax2521])).
% 220.77/220.89 thf(c_0_38, plain, (~p6|p8), inference(fof_simplification,[status(thm)],[ax2518])).
% 220.77/220.89 thf(c_0_39, plain, (p6|~p4), inference(split_conjunct,[status(thm)],[c_0_37])).
% 220.77/220.89 thf(c_0_40, plain, p4, inference(split_conjunct,[status(thm)],[ax2522])).
% 220.77/220.89 thf(c_0_41, plain, (~p8|p12|p3), inference(fof_simplification,[status(thm)],[ax2519])).
% 220.77/220.89 thf(c_0_42, plain, (p8|~p6), inference(split_conjunct,[status(thm)],[c_0_38])).
% 220.77/220.89 thf(c_0_43, plain, p6, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_40])])).
% 220.77/220.89 thf(c_0_44, plain, ~p3, inference(fof_simplification,[status(thm)],[ax2523])).
% 220.77/220.89 thf(c_0_45, plain, (~p12|~p7|~p27), inference(fof_simplification,[status(thm)],[ax2520])).
% 220.77/220.89 thf(c_0_46, plain, (p12|p3|~p8), inference(split_conjunct,[status(thm)],[c_0_41])).
% 220.77/220.89 thf(c_0_47, plain, p8, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_42, c_0_43])])).
% 220.77/220.89 thf(c_0_48, plain, ~p3, inference(split_conjunct,[status(thm)],[c_0_44])).
% 220.77/220.89 thf(c_0_49, plain, (p27|~p51), inference(fof_simplification,[status(thm)],[ax2492])).
% 220.77/220.89 thf(c_0_50, plain, (p51|~p52), inference(fof_simplification,[status(thm)],[ax2491])).
% 220.77/220.89 thf(c_0_51, plain, (p7|~p77), inference(fof_simplification,[status(thm)],[ax2459])).
% 220.77/220.89 thf(c_0_52, plain, (p77|~p78), inference(fof_simplification,[status(thm)],[ax2458])).
% 220.77/220.89 thf(c_0_53, plain, (p77|~p79), inference(fof_simplification,[status(thm)],[ax2457])).
% 220.77/220.89 thf(c_0_54, plain, (p60|~p62), inference(fof_simplification,[status(thm)],[ax2478])).
% 220.77/220.89 thf(c_0_55, plain, (p62|~p66), inference(fof_simplification,[status(thm)],[ax2474])).
% 220.77/220.89 thf(c_0_56, plain, (~p12|~p7|~p27), inference(split_conjunct,[status(thm)],[c_0_45])).
% 220.77/220.89 thf(c_0_57, plain, p12, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_47])]), c_0_48])).
% 220.77/220.89 thf(c_0_58, plain, (p27|~p51), inference(split_conjunct,[status(thm)],[c_0_49])).
% 220.77/220.89 thf(c_0_59, plain, (p51|~p52), inference(split_conjunct,[status(thm)],[c_0_50])).
% 220.77/220.89 thf(c_0_60, plain, (p7|~p77), inference(split_conjunct,[status(thm)],[c_0_51])).
% 220.77/220.89 thf(c_0_61, plain, (p77|~p78), inference(split_conjunct,[status(thm)],[c_0_52])).
% 220.77/220.89 thf(c_0_62, plain, (p77|~p79), inference(split_conjunct,[status(thm)],[c_0_53])).
% 220.77/220.89 thf(c_0_63, plain, (~p26|p64), inference(fof_simplification,[status(thm)],[ax2476])).
% 220.77/220.89 thf(c_0_64, plain, (p60|~p62), inference(split_conjunct,[status(thm)],[c_0_54])).
% 220.77/220.89 thf(c_0_65, plain, (p62|~p66), inference(split_conjunct,[status(thm)],[c_0_55])).
% 220.77/220.89 thf(c_0_66, plain, (~p7|~p27), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_57])])).
% 220.77/220.89 thf(c_0_67, plain, (p27|~p52), inference(spm,[status(thm)],[c_0_58, c_0_59])).
% 220.77/220.89 thf(c_0_68, plain, (p7|~p78), inference(spm,[status(thm)],[c_0_60, c_0_61])).
% 220.77/220.89 thf(c_0_69, plain, (p78|p79), inference(split_conjunct,[status(thm)],[ax2312])).
% 220.77/220.89 thf(c_0_70, plain, (p7|~p79), inference(spm,[status(thm)],[c_0_60, c_0_62])).
% 220.77/220.89 thf(c_0_71, plain, (~p64|~p59|~p63), inference(fof_simplification,[status(thm)],[ax2477])).
% 220.77/220.89 thf(c_0_72, plain, (p64|~p26), inference(split_conjunct,[status(thm)],[c_0_63])).
% 220.77/220.89 thf(c_0_73, plain, p26, inference(split_conjunct,[status(thm)],[ax2524])).
% 220.77/220.89 thf(c_0_74, plain, (p65|~p70), inference(fof_simplification,[status(thm)],[ax2469])).
% 220.77/220.89 thf(c_0_75, plain, (p70|~p218), inference(fof_simplification,[status(thm)],[ax2289])).
% 220.77/220.89 thf(c_0_76, plain, (~p463|~p67|p59), inference(fof_simplification,[status(thm)],[ax1984])).
% 220.77/220.89 thf(c_0_77, plain, (~p228|p463), inference(fof_simplification,[status(thm)],[ax1983])).
% 220.77/220.89 thf(c_0_78, plain, (p52|p59|~p60), inference(fof_simplification,[status(thm)],[ax2483])).
% 220.77/220.89 thf(c_0_79, plain, (p60|~p66), inference(spm,[status(thm)],[c_0_64, c_0_65])).
% 220.77/220.89 thf(c_0_80, plain, (p66|p228), inference(split_conjunct,[status(thm)],[ax2279])).
% 220.77/220.89 thf(c_0_81, plain, (~p7|~p52), inference(spm,[status(thm)],[c_0_66, c_0_67])).
% 220.77/220.89 thf(c_0_82, plain, p7, inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_69]), c_0_70])).
% 220.77/220.89 thf(c_0_83, plain, (~p64|~p59|~p63), inference(split_conjunct,[status(thm)],[c_0_71])).
% 220.77/220.89 thf(c_0_84, plain, p64, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_72, c_0_73])])).
% 220.77/220.89 thf(c_0_85, plain, (p63|~p65), inference(fof_simplification,[status(thm)],[ax2475])).
% 220.77/220.89 thf(c_0_86, plain, (p65|~p70), inference(split_conjunct,[status(thm)],[c_0_74])).
% 220.77/220.89 thf(c_0_87, plain, (p70|~p218), inference(split_conjunct,[status(thm)],[c_0_75])).
% 220.77/220.89 thf(c_0_88, plain, (p218|~p283), inference(fof_simplification,[status(thm)],[ax2208])).
% 220.77/220.89 thf(c_0_89, plain, (p59|~p463|~p67), inference(split_conjunct,[status(thm)],[c_0_76])).
% 220.77/220.89 thf(c_0_90, plain, (p463|~p228), inference(split_conjunct,[status(thm)],[c_0_77])).
% 220.77/220.89 thf(c_0_91, plain, (p62|p67), inference(split_conjunct,[status(thm)],[ax2473])).
% 220.77/220.89 thf(c_0_92, plain, (p52|p59|~p60), inference(split_conjunct,[status(thm)],[c_0_78])).
% 220.77/220.89 thf(c_0_93, plain, (p228|p60), inference(spm,[status(thm)],[c_0_79, c_0_80])).
% 220.77/220.89 thf(c_0_94, plain, ~p52, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_81, c_0_82])])).
% 220.77/220.89 thf(c_0_95, plain, (~p59|~p63), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_83, c_0_84])])).
% 220.77/220.89 thf(c_0_96, plain, (p63|~p65), inference(split_conjunct,[status(thm)],[c_0_85])).
% 220.77/220.89 thf(c_0_97, plain, (p65|~p218), inference(spm,[status(thm)],[c_0_86, c_0_87])).
% 220.77/220.89 thf(c_0_98, plain, (p218|~p283), inference(split_conjunct,[status(thm)],[c_0_88])).
% 220.77/220.89 thf(c_0_99, plain, (p59|~p67|~p228), inference(spm,[status(thm)],[c_0_89, c_0_90])).
% 220.77/220.89 thf(c_0_100, plain, (p67|p60), inference(spm,[status(thm)],[c_0_64, c_0_91])).
% 220.77/220.89 thf(c_0_101, plain, (p228|p59), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_92, c_0_93]), c_0_94])).
% 220.77/220.89 thf(c_0_102, plain, (~p59|~p65), inference(spm,[status(thm)],[c_0_95, c_0_96])).
% 220.77/220.89 thf(c_0_103, plain, (p65|~p283), inference(spm,[status(thm)],[c_0_97, c_0_98])).
% 220.77/220.89 thf(c_0_104, plain, (p218|p284), inference(split_conjunct,[status(thm)],[ax2207])).
% 220.77/220.89 thf(c_0_105, plain, (p52|~p59|p60), inference(fof_simplification,[status(thm)],[ax2482])).
% 220.77/220.89 thf(c_0_106, plain, (p60|p59), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_99, c_0_100]), c_0_101])).
% 220.77/220.89 thf(c_0_107, plain, (~p59|~p283), inference(spm,[status(thm)],[c_0_102, c_0_103])).
% 220.77/220.89 thf(c_0_108, plain, (p283|p495), inference(split_conjunct,[status(thm)],[ax1935])).
% 220.77/220.89 thf(c_0_109, plain, (p284|p65), inference(spm,[status(thm)],[c_0_97, c_0_104])).
% 220.77/220.89 thf(c_0_110, plain, (~p60|p867), inference(fof_simplification,[status(thm)],[ax1483])).
% 220.77/220.89 thf(c_0_111, plain, (p52|p60|~p59), inference(split_conjunct,[status(thm)],[c_0_105])).
% 220.77/220.89 thf(c_0_112, plain, p59, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_92, c_0_106]), c_0_94])).
% 220.77/220.89 thf(c_0_113, plain, (~p862|~p495|~p861), inference(fof_simplification,[status(thm)],[ax1493])).
% 220.77/220.89 thf(c_0_114, plain, (p495|~p59), inference(spm,[status(thm)],[c_0_107, c_0_108])).
% 220.77/220.89 thf(c_0_115, plain, (~p867|p862|~p284), inference(fof_simplification,[status(thm)],[ax1484])).
% 220.77/220.89 thf(c_0_116, plain, (p284|~p59), inference(spm,[status(thm)],[c_0_102, c_0_109])).
% 220.77/220.89 thf(c_0_117, plain, (p867|~p60), inference(split_conjunct,[status(thm)],[c_0_110])).
% 220.77/220.89 thf(c_0_118, plain, p60, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_111, c_0_112])]), c_0_94])).
% 220.77/220.89 thf(c_0_119, plain, (p283|p496), inference(split_conjunct,[status(thm)],[ax1934])).
% 220.77/220.89 thf(c_0_120, plain, (~p862|~p495|~p861), inference(split_conjunct,[status(thm)],[c_0_113])).
% 220.77/220.89 thf(c_0_121, plain, p495, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_114, c_0_112])])).
% 220.77/220.89 thf(c_0_122, plain, (p862|~p867|~p284), inference(split_conjunct,[status(thm)],[c_0_115])).
% 220.77/220.89 thf(c_0_123, plain, p284, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_116, c_0_112])])).
% 220.77/220.89 thf(c_0_124, plain, p867, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_117, c_0_118])])).
% 220.77/220.89 thf(c_0_125, plain, (p65|p71), inference(split_conjunct,[status(thm)],[ax2468])).
% 220.77/220.89 thf(c_0_126, plain, ![X45:a]:(~p496|(~f__22 @ X45|f__10 @ X45)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax496])])])).
% 220.77/220.89 thf(c_0_127, plain, (p496|~p59), inference(spm,[status(thm)],[c_0_107, c_0_119])).
% 220.77/220.89 thf(c_0_128, plain, ((f__22 @ esk17_0|p861)&(~f__1 @ esk17_0|p861)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax861])])])])])).
% 220.77/220.89 thf(c_0_129, plain, (~p861|~p862), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_120, c_0_121])])).
% 220.77/220.89 thf(c_0_130, plain, p862, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_122, c_0_123])]), c_0_124])])).
% 220.77/220.89 thf(c_0_131, plain, ![X77:a]:(~p71|(~f__10 @ X77|f__1 @ X77)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax71])])])).
% 220.77/220.89 thf(c_0_132, plain, (p71|~p59), inference(spm,[status(thm)],[c_0_102, c_0_125])).
% 220.77/220.89 thf(c_0_133, plain, ![X1:a]:(f__10 @ X1|~p496|~f__22 @ X1), inference(split_conjunct,[status(thm)],[c_0_126])).
% 220.77/220.89 thf(c_0_134, plain, p496, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_127, c_0_112])])).
% 220.77/220.89 thf(c_0_135, plain, (f__22 @ esk17_0|p861), inference(split_conjunct,[status(thm)],[c_0_128])).
% 220.77/220.89 thf(c_0_136, plain, ~p861, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_129, c_0_130])])).
% 220.77/220.89 thf(c_0_137, plain, ![X1:a]:(f__1 @ X1|~p71|~f__10 @ X1), inference(split_conjunct,[status(thm)],[c_0_131])).
% 220.77/220.89 thf(c_0_138, plain, p71, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_132, c_0_112])])).
% 220.77/220.89 thf(c_0_139, plain, ![X1:a]:(f__10 @ X1|~f__22 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_133, c_0_134])])).
% 220.77/220.89 thf(c_0_140, plain, f__22 @ esk17_0, inference(sr,[status(thm)],[c_0_135, c_0_136])).
% 220.77/220.89 thf(c_0_141, plain, ![X1:a]:(f__1 @ X1|~f__10 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_137, c_0_138])])).
% 220.77/220.89 thf(c_0_142, plain, f__10 @ esk17_0, inference(spm,[status(thm)],[c_0_139, c_0_140])).
% 220.77/220.89 thf(c_0_143, plain, (p861|~f__1 @ esk17_0), inference(split_conjunct,[status(thm)],[c_0_128])).
% 220.77/220.89 thf(c_0_144, plain, f__1 @ esk17_0, inference(spm,[status(thm)],[c_0_141, c_0_142])).
% 220.77/220.89 thf(c_0_145, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_143, c_0_144])]), c_0_136]), ['proof']).
% 220.77/220.89 thf(12,plain,$false,inference(eprover,[status(thm),assumptions([h8,h9,h5,h3,h4,h2,h1,h0])],[])).
% 220.77/220.89 thf(13,plain,$false,inference(tab_be,[status(thm),assumptions([h5,h3,h4,h2,h1,h0]),tab_be(discharge,[h6,h7]),tab_be(discharge,[h8,h9])],[h5,11,12,h6,h7,h8,h9])).
% 220.77/220.89 thf(14,plain,$false,inference(tab_negall,[status(thm),assumptions([h3,h4,h2,h1,h0]),tab_negall(discharge,[h5]),tab_negall(eigenvar,eigen__1)],[h4,13,h5])).
% 220.77/220.89 thf(15,plain,$false,inference(tab_negimp,[status(thm),assumptions([h2,h1,h0]),tab_negimp(discharge,[h3,h4])],[h2,14,h3,h4])).
% 220.77/220.89 thf(16,plain,$false,inference(tab_negall,[status(thm),assumptions([h1,h0]),tab_negall(discharge,[h2]),tab_negall(eigenvar,eigen__0)],[h1,15,h2])).
% 220.77/220.89 thf(17,plain,$false,inference(eigenvar_choice,[status(thm),assumptions([h1]),eigenvar_choice(discharge,[h0])],[16,h0])).
% 220.77/220.89 thf(0,theorem,(![X1:(a>$o)>$o]:((![X2:a>$o]:(![X3:a>$o]:((~(((![X4:a>$o]:((~(((X1 @ X4) => (~((![X5:a]:((X4 @ X5) => (X2 @ X5)))))))) => (X1 @ X4))) => (~((X3 = (^[X4:a]:(~((![X5:a>$o]:((~(((X1 @ X5) => (~((![X6:a]:((X5 @ X6) => (X2 @ X6)))))))) => (~((X5 @ X4)))))))))))))) => (X1 @ X3)))) => (![X2:a>$o]:((X1 @ X2) = (![X3:a]:((X2 @ X3) => (~((![X4:a>$o]:((~((![X5:a>$o]:((~(((X1 @ X5) => (~((![X6:a]:((X5 @ X6) => (X4 @ X6)))))))) => (~((X5 @ X3))))))) => (~((![X5:a]:((X4 @ X5) => (X2 @ X5))))))))))))))),inference(contra,[status(thm),contra(discharge,[h1])],[16,h1])).
% 220.77/220.89 % SZS output end Proof
%------------------------------------------------------------------------------