%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU585^2 : TPTP v9.2.0. Released v3.7.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 02:43:49 PM UTC 2025
% Result : Theorem 108.89s 108.68s
% Output : Proof 108.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : SEU585^2 : TPTP v9.2.0. Released v3.7.0.
% 0.13/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.35 % Computer : n005.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Oct 8 21:00:38 EDT 2025
% 0.13/0.35 % CPUTime :
% 108.89/108.68 % SZS status Theorem
% 108.89/108.68 % Mode: mode447
% 108.89/108.68 % Inferences: 164
% 108.89/108.68 % SZS output start Proof
% 108.89/108.68 thf(ty_eigen__2, type, eigen__2 : $i).
% 108.89/108.68 thf(ty_setunion, type, setunion : ($i>$i)).
% 108.89/108.68 thf(ty_eigen__1, type, eigen__1 : $i).
% 108.89/108.68 thf(ty_eigen__0, type, eigen__0 : $i).
% 108.89/108.68 thf(ty_emptyset, type, emptyset : $i).
% 108.89/108.68 thf(ty_eigen__3, type, eigen__3 : $o).
% 108.89/108.68 thf(ty_in, type, in : ($i>$i>$o)).
% 108.89/108.68 thf(ty_setadjoin, type, setadjoin : ($i>$i>$i)).
% 108.89/108.68 thf(sP1,plain,sP1 <=> eigen__3,introduced(definition,[new_symbols(definition,[sP1])])).
% 108.89/108.68 thf(def_setadjoinE,definition,(setadjoinE = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ X2)) => (![X4:$o]:(((X3 = X1) => X4) => ((((in @ X3) @ X2) => X4) => X4))))))))).
% 108.89/108.68 thf(def_setunionE,definition,(setunionE = (![X1:$i]:(![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$o]:((![X4:$i]:(((in @ X2) @ X4) => (((in @ X4) @ X1) => X3))) => X3))))))).
% 108.89/108.68 thf(def_uniqinunit,definition,(uniqinunit = (![X1:$i]:(![X2:$i]:(((in @ X1) @ ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))))).
% 108.89/108.68 thf(def_binunion,definition,(binunion = (^[X1:$i]:(^[X2:$i]:(setunion @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))))))).
% 108.89/108.68 thf(binunionEcases,conjecture,((![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ X2)) => (![X4:$o]:(((X3 = X1) => X4) => ((((in @ X3) @ X2) => X4) => X4))))))) => ((![X1:$i]:(![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$o]:((![X4:$i]:(((in @ X2) @ X4) => (((in @ X4) @ X1) => X3))) => X3))))) => ((![X1:$i]:(![X2:$i]:(((in @ X1) @ ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))) => (![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$o]:(((in @ X3) @ (setunion @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset)))) => ((((in @ X3) @ X1) => X4) => ((((in @ X3) @ X2) => X4) => X4))))))))))).
% 108.89/108.68 thf(h0,negated_conjecture,(~(((![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ X2)) => (![X4:$o]:(((X3 = X1) => X4) => ((((in @ X3) @ X2) => X4) => X4))))))) => ((![X1:$i]:(![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$o]:((![X4:$i]:(((in @ X2) @ X4) => (((in @ X4) @ X1) => X3))) => X3))))) => ((![X1:$i]:(![X2:$i]:(((in @ X1) @ ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))) => (![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$o]:(((in @ X3) @ (setunion @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset)))) => ((((in @ X3) @ X1) => X4) => ((((in @ X3) @ X2) => X4) => X4)))))))))))),inference(assume_negation,[status(cth)],[binunionEcases])).
% 108.89/108.68 thf(h1,assumption,(![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ X2)) => (![X4:$o]:(((X3 = X1) => X4) => ((((in @ X3) @ X2) => X4) => X4))))))),introduced(assumption,[])).
% 108.89/108.68 thf(h2,assumption,(~(((![X1:$i]:(![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$o]:((![X4:$i]:(((in @ X2) @ X4) => (((in @ X4) @ X1) => X3))) => X3))))) => ((![X1:$i]:(![X2:$i]:(((in @ X1) @ ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))) => (![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$o]:(((in @ X3) @ (setunion @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset)))) => ((((in @ X3) @ X1) => X4) => ((((in @ X3) @ X2) => X4) => X4))))))))))),introduced(assumption,[])).
% 108.89/108.68 thf(h3,assumption,(![X1:$i]:(![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$o]:((![X4:$i]:(((in @ X2) @ X4) => (((in @ X4) @ X1) => X3))) => X3))))),introduced(assumption,[])).
% 108.89/108.68 thf(h4,assumption,(~(((![X1:$i]:(![X2:$i]:(((in @ X1) @ ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))) => (![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$o]:(((in @ X3) @ (setunion @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset)))) => ((((in @ X3) @ X1) => X4) => ((((in @ X3) @ X2) => X4) => X4)))))))))),introduced(assumption,[])).
% 108.89/108.68 thf(h5,assumption,(![X1:$i]:(![X2:$i]:(((in @ X1) @ ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))),introduced(assumption,[])).
% 108.89/108.68 thf(h6,assumption,(~((![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$o]:(((in @ X3) @ (setunion @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset)))) => ((((in @ X3) @ X1) => X4) => ((((in @ X3) @ X2) => X4) => X4))))))))),introduced(assumption,[])).
% 108.89/108.68 thf(h7,assumption,(~((![X1:$i]:(![X2:$i]:(![X3:$o]:(((in @ X2) @ (setunion @ ((setadjoin @ eigen__0) @ ((setadjoin @ X1) @ emptyset)))) => ((((in @ X2) @ eigen__0) => X3) => ((((in @ X2) @ X1) => X3) => X3)))))))),introduced(assumption,[])).
% 108.89/108.68 thf(h8,assumption,(~((![X1:$i]:(![X2:$o]:(((in @ X1) @ (setunion @ ((setadjoin @ eigen__0) @ ((setadjoin @ eigen__1) @ emptyset)))) => ((((in @ X1) @ eigen__0) => X2) => ((((in @ X1) @ eigen__1) => X2) => X2))))))),introduced(assumption,[])).
% 108.89/108.68 thf(h9,assumption,(~((![X1:$o]:(((in @ eigen__2) @ (setunion @ ((setadjoin @ eigen__0) @ ((setadjoin @ eigen__1) @ emptyset)))) => ((((in @ eigen__2) @ eigen__0) => X1) => ((((in @ eigen__2) @ eigen__1) => X1) => X1)))))),introduced(assumption,[])).
% 108.89/108.68 thf(h10,assumption,(~((((in @ eigen__2) @ (setunion @ ((setadjoin @ eigen__0) @ ((setadjoin @ eigen__1) @ emptyset)))) => ((((in @ eigen__2) @ eigen__0) => sP1) => ((((in @ eigen__2) @ eigen__1) => sP1) => sP1))))),introduced(assumption,[])).
% 108.89/108.68 thf(h11,assumption,((in @ eigen__2) @ (setunion @ ((setadjoin @ eigen__0) @ ((setadjoin @ eigen__1) @ emptyset)))),introduced(assumption,[])).
% 108.89/108.68 thf(h12,assumption,(~(((((in @ eigen__2) @ eigen__0) => sP1) => ((((in @ eigen__2) @ eigen__1) => sP1) => sP1)))),introduced(assumption,[])).
% 108.89/108.68 thf(h13,assumption,(((in @ eigen__2) @ eigen__0) => sP1),introduced(assumption,[])).
% 108.89/108.68 thf(h14,assumption,(~(((((in @ eigen__2) @ eigen__1) => sP1) => sP1))),introduced(assumption,[])).
% 108.89/108.68 thf(h15,assumption,(~(((in @ eigen__2) @ eigen__0))),introduced(assumption,[])).
% 108.89/108.68 thf(h16,assumption,sP1,introduced(assumption,[])).
% 108.89/108.68 thf(h17,assumption,(((in @ eigen__2) @ eigen__1) => sP1),introduced(assumption,[])).
% 108.89/108.68 thf(h18,assumption,(~(sP1)),introduced(assumption,[])).
% 108.89/108.68 thf(h19,assumption,(~(((in @ eigen__2) @ eigen__1))),introduced(assumption,[])).
% 108.89/108.68 thf(ax331, axiom, (~(p6)|p10), file('<stdin>', ax331)).
% 108.89/108.68 thf(ax332, axiom, (~(p10)|p9), file('<stdin>', ax332)).
% 108.89/108.68 thf(ax335, axiom, p6, file('<stdin>', ax335)).
% 108.89/108.68 thf(ax333, axiom, (~(p9)|~(p4)|p8), file('<stdin>', ax333)).
% 108.89/108.68 thf(ax330, axiom, (~(p12)|~(p11)|~(p6)), file('<stdin>', ax330)).
% 108.89/108.68 thf(ax329, axiom, (~(p8)|p12), file('<stdin>', ax329)).
% 108.89/108.68 thf(ax337, axiom, p4, file('<stdin>', ax337)).
% 108.89/108.68 thf(nax36, axiom, (p36<=(f__2)=(f__2)), file('<stdin>', nax36)).
% 108.89/108.68 thf(ax293, axiom, (p11|~(p49)), file('<stdin>', ax293)).
% 108.89/108.68 thf(ax313, axiom, (~(p7)|p28), file('<stdin>', ax313)).
% 108.89/108.68 thf(ax52, axiom, (~(p76)|p3|~(p36)|~(p281)), file('<stdin>', ax52)).
% 108.89/108.68 thf(ax338, axiom, ~(p3), file('<stdin>', ax338)).
% 108.89/108.68 thf(ax42, axiom, (~(p28)|p292), file('<stdin>', ax42)).
% 108.89/108.68 thf(ax334, axiom, p7, file('<stdin>', ax334)).
% 108.89/108.68 thf(ax266, axiom, (p49|p76), file('<stdin>', ax266)).
% 108.89/108.68 thf(ax43, axiom, (~(p292)|p291), file('<stdin>', ax43)).
% 108.89/108.68 thf(ax265, axiom, (p49|~(p77)), file('<stdin>', ax265)).
% 108.89/108.68 thf(ax204, axiom, (~(p8)|p138), file('<stdin>', ax204)).
% 108.89/108.68 thf(nax281, axiom, (p281<=(f__4)=(f__0)), file('<stdin>', nax281)).
% 108.89/108.68 thf(ax44, axiom, (~(p291)|~(p142)|p290), file('<stdin>', ax44)).
% 108.89/108.68 thf(ax205, axiom, (~(p138)|~(p137)|~(p76)), file('<stdin>', ax205)).
% 108.89/108.68 thf(nax293, axiom, (p293<=((f__4)=(f__0)=>![X1:$i]:(fin @ f__2 @ X1=>(fin @ X1 @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))=>~(fin @ f__2 @ f__4))))), file('<stdin>', nax293)).
% 108.89/108.68 thf(ax200, axiom, (p77|p142), file('<stdin>', ax200)).
% 108.89/108.68 thf(ax40, axiom, (~(p296)|~(p293)|p295), file('<stdin>', ax40)).
% 108.89/108.68 thf(ax39, axiom, (~(p290)|p296), file('<stdin>', ax39)).
% 108.89/108.68 thf(ax41, axiom, (~(p295)|~(p294)|p137), file('<stdin>', ax41)).
% 108.89/108.68 thf(ax51, axiom, (~(p76)|p2|~(p36)|~(p282)), file('<stdin>', ax51)).
% 108.89/108.68 thf(ax339, axiom, ~(p2), file('<stdin>', ax339)).
% 108.89/108.68 thf(pax5, axiom, (p5=>![X1:$i, X2:$i]:(fin @ X1 @ (fsetadjoin @ X2 @ femptyset)=>(X1)=(X2))), file('<stdin>', pax5)).
% 108.89/108.68 thf(nax294, axiom, (p294<=(fin @ f__4 @ (fsetadjoin @ f__1 @ femptyset)=>![X1:$i]:(fin @ f__2 @ X1=>(fin @ X1 @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))=>~(fin @ f__2 @ f__4))))), file('<stdin>', nax294)).
% 108.89/108.68 thf(nax282, axiom, (p282<=(f__4)=(f__1)), file('<stdin>', nax282)).
% 108.89/108.68 thf(ax336, axiom, p5, file('<stdin>', ax336)).
% 108.89/108.68 thf(c_0_32, plain, (~p6|p10), inference(fof_simplification,[status(thm)],[ax331])).
% 108.89/108.68 thf(c_0_33, plain, (~p10|p9), inference(fof_simplification,[status(thm)],[ax332])).
% 108.89/108.68 thf(c_0_34, plain, (p10|~p6), inference(split_conjunct,[status(thm)],[c_0_32])).
% 108.89/108.68 thf(c_0_35, plain, p6, inference(split_conjunct,[status(thm)],[ax335])).
% 108.89/108.68 thf(c_0_36, plain, (~p9|~p4|p8), inference(fof_simplification,[status(thm)],[ax333])).
% 108.89/108.68 thf(c_0_37, plain, (p9|~p10), inference(split_conjunct,[status(thm)],[c_0_33])).
% 108.89/108.68 thf(c_0_38, plain, p10, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_34, c_0_35])])).
% 108.89/108.68 thf(c_0_39, plain, (~p12|~p11|~p6), inference(fof_simplification,[status(thm)],[ax330])).
% 108.89/108.68 thf(c_0_40, plain, (~p8|p12), inference(fof_simplification,[status(thm)],[ax329])).
% 108.89/108.68 thf(c_0_41, plain, (p8|~p9|~p4), inference(split_conjunct,[status(thm)],[c_0_36])).
% 108.89/108.68 thf(c_0_42, plain, p4, inference(split_conjunct,[status(thm)],[ax337])).
% 108.89/108.68 thf(c_0_43, plain, p9, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38])])).
% 108.89/108.68 thf(c_0_44, plain, (~p12|~p11|~p6), inference(split_conjunct,[status(thm)],[c_0_39])).
% 108.89/108.68 thf(c_0_45, plain, (p12|~p8), inference(split_conjunct,[status(thm)],[c_0_40])).
% 108.89/108.68 thf(c_0_46, plain, p8, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_42]), c_0_43])])).
% 108.89/108.68 thf(c_0_47, plain, ((f__2)!=(f__2)|p36), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax36])])).
% 108.89/108.68 thf(c_0_48, plain, (p11|~p49), inference(fof_simplification,[status(thm)],[ax293])).
% 108.89/108.68 thf(c_0_49, plain, (~p11|~p12), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_44, c_0_35])])).
% 108.89/108.68 thf(c_0_50, plain, p12, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_46])])).
% 108.89/108.68 thf(c_0_51, plain, (~p7|p28), inference(fof_simplification,[status(thm)],[ax313])).
% 108.89/108.68 thf(c_0_52, plain, (~p76|p3|~p36|~p281), inference(fof_simplification,[status(thm)],[ax52])).
% 108.89/108.68 thf(c_0_53, plain, (p36|(f__2)!=(f__2)), inference(split_conjunct,[status(thm)],[c_0_47])).
% 108.89/108.68 thf(c_0_54, plain, ~p3, inference(fof_simplification,[status(thm)],[ax338])).
% 108.89/108.68 thf(c_0_55, plain, (p11|~p49), inference(split_conjunct,[status(thm)],[c_0_48])).
% 108.89/108.68 thf(c_0_56, plain, ~p11, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_49, c_0_50])])).
% 108.89/108.68 thf(c_0_57, plain, (~p28|p292), inference(fof_simplification,[status(thm)],[ax42])).
% 108.89/108.68 thf(c_0_58, plain, (p28|~p7), inference(split_conjunct,[status(thm)],[c_0_51])).
% 108.89/108.68 thf(c_0_59, plain, p7, inference(split_conjunct,[status(thm)],[ax334])).
% 108.89/108.68 thf(c_0_60, plain, (p3|~p76|~p36|~p281), inference(split_conjunct,[status(thm)],[c_0_52])).
% 108.89/108.68 thf(c_0_61, plain, p36, inference(cn,[status(thm)],[c_0_53])).
% 108.89/108.68 thf(c_0_62, plain, ~p3, inference(split_conjunct,[status(thm)],[c_0_54])).
% 108.89/108.68 thf(c_0_63, plain, (p49|p76), inference(split_conjunct,[status(thm)],[ax266])).
% 108.89/108.68 thf(c_0_64, plain, ~p49, inference(sr,[status(thm)],[c_0_55, c_0_56])).
% 108.89/108.68 thf(c_0_65, plain, (~p292|p291), inference(fof_simplification,[status(thm)],[ax43])).
% 108.89/108.68 thf(c_0_66, plain, (p292|~p28), inference(split_conjunct,[status(thm)],[c_0_57])).
% 108.89/108.68 thf(c_0_67, plain, p28, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_58, c_0_59])])).
% 108.89/108.68 thf(c_0_68, plain, (p49|~p77), inference(fof_simplification,[status(thm)],[ax265])).
% 108.89/108.68 thf(c_0_69, plain, (~p8|p138), inference(fof_simplification,[status(thm)],[ax204])).
% 108.89/108.68 thf(c_0_70, plain, ((f__4)!=(f__0)|p281), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax281])])).
% 108.89/108.68 thf(c_0_71, plain, (~p76|~p281), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_60, c_0_61])]), c_0_62])).
% 108.89/108.68 thf(c_0_72, plain, p76, inference(sr,[status(thm)],[c_0_63, c_0_64])).
% 108.89/108.68 thf(c_0_73, plain, (~p291|~p142|p290), inference(fof_simplification,[status(thm)],[ax44])).
% 108.89/108.68 thf(c_0_74, plain, (p291|~p292), inference(split_conjunct,[status(thm)],[c_0_65])).
% 108.89/108.68 thf(c_0_75, plain, p292, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_66, c_0_67])])).
% 108.89/108.68 thf(c_0_76, plain, (p49|~p77), inference(split_conjunct,[status(thm)],[c_0_68])).
% 108.89/108.68 thf(c_0_77, plain, (~p138|~p137|~p76), inference(fof_simplification,[status(thm)],[ax205])).
% 108.89/108.68 thf(c_0_78, plain, (p138|~p8), inference(split_conjunct,[status(thm)],[c_0_69])).
% 108.89/108.68 thf(c_0_79, plain, (((f__4)=(f__0)|p293)&((fin @ f__2 @ esk7_0|p293)&((fin @ esk7_0 @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))|p293)&(fin @ f__2 @ f__4|p293)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax293])])])])])).
% 108.89/108.68 thf(c_0_80, plain, (p281|(f__4)!=(f__0)), inference(split_conjunct,[status(thm)],[c_0_70])).
% 108.89/108.68 thf(c_0_81, plain, ~p281, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_71, c_0_72])])).
% 108.89/108.68 thf(c_0_82, plain, (p290|~p291|~p142), inference(split_conjunct,[status(thm)],[c_0_73])).
% 108.89/108.68 thf(c_0_83, plain, p291, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_74, c_0_75])])).
% 108.89/108.68 thf(c_0_84, plain, (p77|p142), inference(split_conjunct,[status(thm)],[ax200])).
% 108.89/108.68 thf(c_0_85, plain, ~p77, inference(sr,[status(thm)],[c_0_76, c_0_64])).
% 108.89/108.68 thf(c_0_86, plain, (~p138|~p137|~p76), inference(split_conjunct,[status(thm)],[c_0_77])).
% 108.89/108.68 thf(c_0_87, plain, p138, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_78, c_0_46])])).
% 108.89/108.68 thf(c_0_88, plain, (~p296|~p293|p295), inference(fof_simplification,[status(thm)],[ax40])).
% 108.89/108.68 thf(c_0_89, plain, ((f__4)=(f__0)|p293), inference(split_conjunct,[status(thm)],[c_0_79])).
% 108.89/108.68 thf(c_0_90, plain, (f__4)!=(f__0), inference(sr,[status(thm)],[c_0_80, c_0_81])).
% 108.89/108.68 thf(c_0_91, plain, (~p290|p296), inference(fof_simplification,[status(thm)],[ax39])).
% 108.89/108.68 thf(c_0_92, plain, (p290|~p142), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_82, c_0_83])])).
% 108.89/108.68 thf(c_0_93, plain, p142, inference(sr,[status(thm)],[c_0_84, c_0_85])).
% 108.89/108.68 thf(c_0_94, plain, (~p295|~p294|p137), inference(fof_simplification,[status(thm)],[ax41])).
% 108.89/108.68 thf(c_0_95, plain, (~p76|~p137), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_86, c_0_87])])).
% 108.89/108.68 thf(c_0_96, plain, (p295|~p296|~p293), inference(split_conjunct,[status(thm)],[c_0_88])).
% 108.89/108.68 thf(c_0_97, plain, p293, inference(sr,[status(thm)],[c_0_89, c_0_90])).
% 108.89/108.68 thf(c_0_98, plain, (p296|~p290), inference(split_conjunct,[status(thm)],[c_0_91])).
% 108.89/108.68 thf(c_0_99, plain, p290, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_92, c_0_93])])).
% 108.89/108.68 thf(c_0_100, plain, (~p76|p2|~p36|~p282), inference(fof_simplification,[status(thm)],[ax51])).
% 108.89/108.68 thf(c_0_101, plain, ~p2, inference(fof_simplification,[status(thm)],[ax339])).
% 108.89/108.68 thf(c_0_102, plain, (p137|~p295|~p294), inference(split_conjunct,[status(thm)],[c_0_94])).
% 108.89/108.68 thf(c_0_103, plain, ~p137, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_95, c_0_72])])).
% 108.89/108.68 thf(c_0_104, plain, (p295|~p296), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_96, c_0_97])])).
% 108.89/108.68 thf(c_0_105, plain, p296, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_98, c_0_99])])).
% 108.89/108.68 thf(c_0_106, plain, (p2|~p76|~p36|~p282), inference(split_conjunct,[status(thm)],[c_0_100])).
% 108.89/108.68 thf(c_0_107, plain, ~p2, inference(split_conjunct,[status(thm)],[c_0_101])).
% 108.89/108.68 thf(c_0_108, plain, ![X663:$i, X664:$i]:(~p5|(~fin @ X663 @ (fsetadjoin @ X664 @ femptyset)|(X663)=(X664))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax5])])])).
% 108.89/108.68 thf(c_0_109, plain, ((fin @ f__4 @ (fsetadjoin @ f__1 @ femptyset)|p294)&((fin @ f__2 @ esk6_0|p294)&((fin @ esk6_0 @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))|p294)&(fin @ f__2 @ f__4|p294)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax294])])])])])).
% 108.89/108.68 thf(c_0_110, plain, (~p294|~p295), inference(sr,[status(thm)],[c_0_102, c_0_103])).
% 108.89/108.68 thf(c_0_111, plain, p295, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_104, c_0_105])])).
% 108.89/108.68 thf(c_0_112, plain, ((f__4)!=(f__1)|p282), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax282])])).
% 108.89/108.68 thf(c_0_113, plain, (~p76|~p282), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_106, c_0_61])]), c_0_107])).
% 108.89/108.68 thf(c_0_114, plain, ![X1:$i, X2:$i]:((X1)=(X2)|~p5|~fin @ X1 @ (fsetadjoin @ X2 @ femptyset)), inference(split_conjunct,[status(thm)],[c_0_108])).
% 108.89/108.68 thf(c_0_115, plain, p5, inference(split_conjunct,[status(thm)],[ax336])).
% 108.89/108.68 thf(c_0_116, plain, (fin @ f__4 @ (fsetadjoin @ f__1 @ femptyset)|p294), inference(split_conjunct,[status(thm)],[c_0_109])).
% 108.89/108.68 thf(c_0_117, plain, ~p294, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_110, c_0_111])])).
% 108.89/108.68 thf(c_0_118, plain, (p282|(f__4)!=(f__1)), inference(split_conjunct,[status(thm)],[c_0_112])).
% 108.89/108.68 thf(c_0_119, plain, ~p282, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_113, c_0_72])])).
% 108.89/108.68 thf(c_0_120, plain, ![X1:$i, X2:$i]:((X1)=(X2)|~fin @ X1 @ (fsetadjoin @ X2 @ femptyset)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_114, c_0_115])])).
% 108.89/108.68 thf(c_0_121, plain, fin @ f__4 @ (fsetadjoin @ f__1 @ femptyset), inference(sr,[status(thm)],[c_0_116, c_0_117])).
% 108.89/108.68 thf(c_0_122, plain, (f__4)!=(f__1), inference(sr,[status(thm)],[c_0_118, c_0_119])).
% 108.89/108.68 thf(c_0_123, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_120, c_0_121]), c_0_122]), ['proof']).
% 108.89/108.68 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h19,h17,h18,h15,h13,h14,h11,h12,h10,h9,h8,h7,h5,h6,h3,h4,h1,h2,h0])],[])).
% 108.89/108.68 thf(2,plain,$false,inference(tab_conflict,[status(thm),assumptions([h16,h17,h18,h15,h13,h14,h11,h12,h10,h9,h8,h7,h5,h6,h3,h4,h1,h2,h0])],[h16,h18])).
% 108.89/108.68 thf(3,plain,$false,inference(tab_imp,[status(thm),assumptions([h17,h18,h15,h13,h14,h11,h12,h10,h9,h8,h7,h5,h6,h3,h4,h1,h2,h0]),tab_imp(discharge,[h19]),tab_imp(discharge,[h16])],[h17,1,2,h19,h16])).
% 108.89/108.68 thf(4,plain,$false,inference(tab_negimp,[status(thm),assumptions([h15,h13,h14,h11,h12,h10,h9,h8,h7,h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h17,h18])],[h14,3,h17,h18])).
% 108.89/108.68 thf(5,plain,$false,inference(tab_conflict,[status(thm),assumptions([h19,h17,h18,h16,h13,h14,h11,h12,h10,h9,h8,h7,h5,h6,h3,h4,h1,h2,h0])],[h16,h18])).
% 108.89/108.68 thf(6,plain,$false,inference(tab_conflict,[status(thm),assumptions([h16,h17,h18,h16,h13,h14,h11,h12,h10,h9,h8,h7,h5,h6,h3,h4,h1,h2,h0])],[h16,h18])).
% 108.89/108.68 thf(7,plain,$false,inference(tab_imp,[status(thm),assumptions([h17,h18,h16,h13,h14,h11,h12,h10,h9,h8,h7,h5,h6,h3,h4,h1,h2,h0]),tab_imp(discharge,[h19]),tab_imp(discharge,[h16])],[h17,5,6,h19,h16])).
% 108.89/108.68 thf(8,plain,$false,inference(tab_negimp,[status(thm),assumptions([h16,h13,h14,h11,h12,h10,h9,h8,h7,h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h17,h18])],[h14,7,h17,h18])).
% 108.89/108.68 thf(9,plain,$false,inference(tab_imp,[status(thm),assumptions([h13,h14,h11,h12,h10,h9,h8,h7,h5,h6,h3,h4,h1,h2,h0]),tab_imp(discharge,[h15]),tab_imp(discharge,[h16])],[h13,4,8,h15,h16])).
% 108.89/108.68 thf(10,plain,$false,inference(tab_negimp,[status(thm),assumptions([h11,h12,h10,h9,h8,h7,h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h13,h14])],[h12,9,h13,h14])).
% 108.89/108.68 thf(11,plain,$false,inference(tab_negimp,[status(thm),assumptions([h10,h9,h8,h7,h5,h6,h3,h4,h1,h2,h0]),tab_negimp(discharge,[h11,h12])],[h10,10,h11,h12])).
% 108.89/108.68 thf(12,plain,$false,inference(tab_negall,[status(thm),assumptions([h9,h8,h7,h5,h6,h3,h4,h1,h2,h0]),tab_negall(discharge,[h10]),tab_negall(eigenvar,eigen__3)],[h9,11,h10])).
% 108.89/108.68 thf(13,plain,$false,inference(tab_negall,[status(thm),assumptions([h8,h7,h5,h6,h3,h4,h1,h2,h0]),tab_negall(discharge,[h9]),tab_negall(eigenvar,eigen__2)],[h8,12,h9])).
% 108.89/108.68 thf(14,plain,$false,inference(tab_negall,[status(thm),assumptions([h7,h5,h6,h3,h4,h1,h2,h0]),tab_negall(discharge,[h8]),tab_negall(eigenvar,eigen__1)],[h7,13,h8])).
% 108.89/108.68 thf(15,plain,$false,inference(tab_negall,[status(thm),assumptions([h5,h6,h3,h4,h1,h2,h0]),tab_negall(discharge,[h7]),tab_negall(eigenvar,eigen__0)],[h6,14,h7])).
% 108.89/108.68 thf(16,plain,$false,inference(tab_negimp,[status(thm),assumptions([h3,h4,h1,h2,h0]),tab_negimp(discharge,[h5,h6])],[h4,15,h5,h6])).
% 108.89/108.68 thf(17,plain,$false,inference(tab_negimp,[status(thm),assumptions([h1,h2,h0]),tab_negimp(discharge,[h3,h4])],[h2,16,h3,h4])).
% 108.89/108.68 thf(18,plain,$false,inference(tab_negimp,[status(thm),assumptions([h0]),tab_negimp(discharge,[h1,h2])],[h0,17,h1,h2])).
% 108.89/108.68 thf(0,theorem,((![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ X2)) => (![X4:$o]:(((X3 = X1) => X4) => ((((in @ X3) @ X2) => X4) => X4))))))) => ((![X1:$i]:(![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$o]:((![X4:$i]:(((in @ X2) @ X4) => (((in @ X4) @ X1) => X3))) => X3))))) => ((![X1:$i]:(![X2:$i]:(((in @ X1) @ ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))) => (![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$o]:(((in @ X3) @ (setunion @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset)))) => ((((in @ X3) @ X1) => X4) => ((((in @ X3) @ X2) => X4) => X4)))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[18,h0])).
% 108.89/108.68 % SZS output end Proof
%------------------------------------------------------------------------------