%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU515^1 : 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 : n015.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:22 PM UTC 2025
% Result : Theorem 24.01s 24.23s
% Output : Proof 24.01s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SEU515^1 : TPTP v9.2.0. Released v3.7.0.
% 0.03/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.35 % Computer : n015.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:21:23 EDT 2025
% 0.13/0.35 % CPUTime :
% 24.01/24.23 % SZS status Theorem
% 24.01/24.23 % Mode: mode371
% 24.01/24.23 % Inferences: 4148
% 24.01/24.23 % SZS output start Proof
% 24.01/24.23 thf(def_exu,definition,(exu = (^[X1:$i>$o]:(~((![X2:$i]:((X1 @ X2) => (~((![X3:$i]:((X1 @ X3) => (X2 = X3)))))))))))).
% 24.01/24.23 thf(def_setextAx,definition,(setextAx = (![X1:$i]:(![X2:$i]:((![X3:$i]:(((in @ X3) @ X1) = ((in @ X3) @ X2))) => (X1 = X2)))))).
% 24.01/24.23 thf(def_emptysetAx,definition,(emptysetAx = (![X1:$i]:(~(((in @ X1) @ emptyset)))))).
% 24.01/24.23 thf(def_setadjoinAx,definition,(setadjoinAx = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ X2)) = ((~((X3 = X1))) => ((in @ X3) @ X2)))))))).
% 24.01/24.23 thf(def_powersetAx,definition,(powersetAx = (![X1:$i]:(![X2:$i]:(((in @ X2) @ (powerset @ X1)) = (![X3:$i]:(((in @ X3) @ X2) => ((in @ X3) @ X1)))))))).
% 24.01/24.23 thf(def_setunionAx,definition,(setunionAx = (![X1:$i]:(![X2:$i]:(((in @ X2) @ (setunion @ X1)) = (~((![X3:$i]:(((in @ X2) @ X3) => (~(((in @ X3) @ X1)))))))))))).
% 24.01/24.23 thf(def_omega0Ax,definition,(omega0Ax = ((in @ emptyset) @ omega))).
% 24.01/24.23 thf(def_omegaSAx,definition,(omegaSAx = (![X1:$i]:(((in @ X1) @ omega) => ((in @ ((setadjoin @ X1) @ X1)) @ omega))))).
% 24.01/24.23 thf(def_omegaIndAx,definition,(omegaIndAx = (![X1:$i]:((~((((in @ emptyset) @ X1) => (~((![X2:$i]:((~((((in @ X2) @ omega) => (~(((in @ X2) @ X1)))))) => ((in @ ((setadjoin @ X2) @ X2)) @ X1)))))))) => (![X2:$i]:(((in @ X2) @ omega) => ((in @ X2) @ X1))))))).
% 24.01/24.23 thf(def_replAx,definition,(replAx = (![X1:$i>$i>$o]:(![X2:$i]:((![X3:$i]:(((in @ X3) @ X2) => (exu @ (X1 @ X3)))) => (~((![X3:$i]:(~((![X4:$i]:(((in @ X4) @ X3) = (~((![X5:$i]:(((in @ X5) @ X2) => (~(((X1 @ X5) @ X4))))))))))))))))))).
% 24.01/24.23 thf(def_foundationAx,definition,(foundationAx = (![X1:$i]:((~((![X2:$i]:(~(((in @ X2) @ X1)))))) => (~((![X2:$i]:(((in @ X2) @ X1) => (~((![X3:$i]:(((in @ X3) @ X2) => (~(((in @ X3) @ X1))))))))))))))).
% 24.01/24.23 thf(def_wellorderingAx,definition,(wellorderingAx = (![X1:$i]:(~((![X2:$i]:((~(((~(((![X3:$i]:(((in @ X3) @ X2) => (![X4:$i]:(((in @ X4) @ X3) => ((in @ X4) @ X1))))) => (~((![X3:$i]:(![X4:$i]:((~((((in @ X3) @ X1) => (~(((in @ X4) @ X1)))))) => ((![X5:$i]:(((in @ X5) @ X2) => (((in @ X3) @ X5) = ((in @ X4) @ X5)))) => (X3 = X4)))))))))) => (~((![X3:$i]:(![X4:$i]:((~((((in @ X3) @ X2) => (~(((in @ X4) @ X2)))))) => ((~((![X5:$i]:(((in @ X5) @ X3) => ((in @ X5) @ X4))))) => (![X5:$i]:(((in @ X5) @ X4) => ((in @ X5) @ X3)))))))))))) => (~((![X3:$i]:((~(((![X4:$i]:(((in @ X4) @ X3) => ((in @ X4) @ X1))) => (![X4:$i]:(~(((in @ X4) @ X3))))))) => (~((![X4:$i]:(![X5:$i]:((~(((~((((in @ X4) @ X2) => (~(((in @ X5) @ X3)))))) => (~((![X6:$i]:(((in @ X6) @ X4) => (~(((in @ X6) @ X3)))))))))) => (~((![X6:$i]:(((in @ X6) @ X2) => ((~((![X7:$i]:(((in @ X7) @ X6) => ((in @ X7) @ X4))))) => ((in @ X5) @ X6)))))))))))))))))))))).
% 24.01/24.23 thf(def_descrp,definition,(descrp = (![X1:$i>$o]:((exu @ X1) => (X1 @ (descr @ X1)))))).
% 24.01/24.23 thf(def_dsetconstrI,definition,(dsetconstrI = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ X1) => ((X2 @ X3) => ((in @ X3) @ ((dsetconstr @ X1) @ X2))))))))).
% 24.01/24.23 thf(def_dsetconstrEL,definition,(dsetconstrEL = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ ((dsetconstr @ X1) @ X2)) => ((in @ X3) @ X1))))))).
% 24.01/24.23 thf(def_dsetconstrER,definition,(dsetconstrER = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ ((dsetconstr @ X1) @ X2)) => (X2 @ X3))))))).
% 24.01/24.23 thf(def_exuE1,definition,(exuE1 = (![X1:$i>$o]:((exu @ X1) => (~((![X2:$i]:((X1 @ X2) => (~((![X3:$i]:((X1 @ X3) => (X2 = X3))))))))))))).
% 24.01/24.23 thf(def_prop2set,definition,(prop2set = (^[X1:$o]:((dsetconstr @ (powerset @ emptyset)) @ (^[X2:$i]:X1))))).
% 24.01/24.23 thf(def_prop2setE,definition,(prop2setE = (![X1:$o]:(![X2:$i]:(((in @ X2) @ (prop2set @ X1)) => X1))))).
% 24.01/24.23 thf(def_emptysetE,definition,(emptysetE = (![X1:$i]:(((in @ X1) @ emptyset) => (![X2:$o]:X2))))).
% 24.01/24.23 thf(def_emptysetimpfalse,definition,(emptysetimpfalse = (![X1:$i]:(~(((in @ X1) @ emptyset)))))).
% 24.01/24.23 thf(def_notinemptyset,definition,(notinemptyset = (![X1:$i]:(~(((in @ X1) @ emptyset)))))).
% 24.01/24.23 thf(def_exuE3e,definition,(exuE3e = (![X1:$i>$o]:((exu @ X1) => (~((![X2:$i]:(~((X1 @ X2)))))))))).
% 24.01/24.23 thf(def_setext,definition,(setext = (![X1:$i]:(![X2:$i]:((![X3:$i]:(((in @ X3) @ X1) => ((in @ X3) @ X2))) => ((![X3:$i]:(((in @ X3) @ X2) => ((in @ X3) @ X1))) => (X1 = X2))))))).
% 24.01/24.23 thf(def_emptyI,definition,(emptyI = (![X1:$i]:((![X2:$i]:(~(((in @ X2) @ X1)))) => (X1 = emptyset))))).
% 24.01/24.23 thf(def_noeltsimpempty,definition,(noeltsimpempty = (![X1:$i]:((![X2:$i]:(~(((in @ X2) @ X1)))) => (X1 = emptyset))))).
% 24.01/24.23 thf(def_setbeta,definition,(setbeta = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ X1) => (((in @ X3) @ ((dsetconstr @ X1) @ X2)) = (X2 @ X3)))))))).
% 24.01/24.23 thf(def_nonempty,definition,(nonempty = (^[X1:$i]:(~((X1 = emptyset)))))).
% 24.01/24.23 thf(def_nonemptyE1,definition,(nonemptyE1 = (![X1:$i]:((nonempty @ X1) => (~((![X2:$i]:(~(((in @ X2) @ X1)))))))))).
% 24.01/24.23 thf(def_nonemptyI,definition,(nonemptyI = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ X1) => ((X2 @ X3) => (nonempty @ ((dsetconstr @ X1) @ X2))))))))).
% 24.01/24.23 thf(def_nonemptyI1,definition,(nonemptyI1 = (![X1:$i]:((~((![X2:$i]:(~(((in @ X2) @ X1)))))) => (nonempty @ X1))))).
% 24.01/24.23 thf(def_setadjoinIL,definition,(setadjoinIL = (![X1:$i]:(![X2:$i]:((in @ X1) @ ((setadjoin @ X1) @ X2)))))).
% 24.01/24.23 thf(def_emptyinunitempty,definition,(emptyinunitempty = ((in @ emptyset) @ ((setadjoin @ emptyset) @ emptyset)))).
% 24.01/24.23 thf(def_setadjoinIR,definition,(setadjoinIR = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X2) => ((in @ X3) @ ((setadjoin @ X1) @ X2)))))))).
% 24.01/24.23 thf(setadjoinE,conjecture,(setextAx => (emptysetAx => (setadjoinAx => (powersetAx => (setunionAx => (omega0Ax => (omegaSAx => (omegaIndAx => (replAx => (foundationAx => (wellorderingAx => (descrp => (dsetconstrI => (dsetconstrEL => (dsetconstrER => (exuE1 => (prop2setE => (emptysetE => (emptysetimpfalse => (notinemptyset => (exuE3e => (setext => (emptyI => (noeltsimpempty => (setbeta => (nonemptyE1 => (nonemptyI => (nonemptyI1 => (setadjoinIL => (emptyinunitempty => (setadjoinIR => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ X2)) => (![X4:$o]:(((X3 = X1) => X4) => ((((in @ X3) @ X2) => X4) => X4))))))))))))))))))))))))))))))))))))))).
% 24.01/24.23 thf(h0,negated_conjecture,(~((setextAx => (emptysetAx => (setadjoinAx => (powersetAx => (setunionAx => (omega0Ax => (omegaSAx => (omegaIndAx => (replAx => (foundationAx => (wellorderingAx => (descrp => (dsetconstrI => (dsetconstrEL => (dsetconstrER => (exuE1 => (prop2setE => (emptysetE => (emptysetimpfalse => (notinemptyset => (exuE3e => (setext => (emptyI => (noeltsimpempty => (setbeta => (nonemptyE1 => (nonemptyI => (nonemptyI1 => (setadjoinIL => (emptyinunitempty => (setadjoinIR => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ X2)) => (![X4:$o]:(((X3 = X1) => X4) => ((((in @ X3) @ X2) => X4) => X4)))))))))))))))))))))))))))))))))))))))),inference(assume_negation,[status(cth)],[setadjoinE])).
% 24.01/24.23 thf(ax262, axiom, (p1|~(p37)), file('<stdin>', ax262)).
% 24.01/24.23 thf(ax298, axiom, ~(p1), file('<stdin>', ax298)).
% 24.01/24.23 thf(ax260, axiom, (p37|~(p39)), file('<stdin>', ax260)).
% 24.01/24.23 thf(ax258, axiom, (p39|~(p41)), file('<stdin>', ax258)).
% 24.01/24.23 thf(ax256, axiom, (p41|~(p43)), file('<stdin>', ax256)).
% 24.01/24.23 thf(ax254, axiom, (p43|~(p45)), file('<stdin>', ax254)).
% 24.01/24.23 thf(ax252, axiom, (p45|~(p47)), file('<stdin>', ax252)).
% 24.01/24.23 thf(ax250, axiom, (p47|~(p49)), file('<stdin>', ax250)).
% 24.01/24.23 thf(ax248, axiom, (p49|~(p51)), file('<stdin>', ax248)).
% 24.01/24.23 thf(ax246, axiom, (p51|~(p53)), file('<stdin>', ax246)).
% 24.01/24.23 thf(ax244, axiom, (p53|~(p55)), file('<stdin>', ax244)).
% 24.01/24.23 thf(ax242, axiom, (p55|~(p57)), file('<stdin>', ax242)).
% 24.01/24.23 thf(ax240, axiom, (p57|~(p59)), file('<stdin>', ax240)).
% 24.01/24.23 thf(ax238, axiom, (p59|~(p61)), file('<stdin>', ax238)).
% 24.01/24.23 thf(ax236, axiom, (p61|~(p63)), file('<stdin>', ax236)).
% 24.01/24.23 thf(ax234, axiom, (p63|~(p65)), file('<stdin>', ax234)).
% 24.01/24.23 thf(ax232, axiom, (p65|~(p67)), file('<stdin>', ax232)).
% 24.01/24.23 thf(ax230, axiom, (p67|~(p69)), file('<stdin>', ax230)).
% 24.01/24.23 thf(ax228, axiom, (p69|~(p71)), file('<stdin>', ax228)).
% 24.01/24.23 thf(ax226, axiom, (p71|~(p73)), file('<stdin>', ax226)).
% 24.01/24.23 thf(ax224, axiom, (p73|~(p75)), file('<stdin>', ax224)).
% 24.01/24.23 thf(ax222, axiom, (p75|~(p77)), file('<stdin>', ax222)).
% 24.01/24.23 thf(ax220, axiom, (p77|~(p79)), file('<stdin>', ax220)).
% 24.01/24.23 thf(ax218, axiom, (p79|~(p81)), file('<stdin>', ax218)).
% 24.01/24.23 thf(ax216, axiom, (p81|~(p83)), file('<stdin>', ax216)).
% 24.01/24.23 thf(ax214, axiom, (p83|~(p85)), file('<stdin>', ax214)).
% 24.01/24.23 thf(ax212, axiom, (p85|~(p87)), file('<stdin>', ax212)).
% 24.01/24.23 thf(ax210, axiom, (p87|~(p89)), file('<stdin>', ax210)).
% 24.01/24.23 thf(ax208, axiom, (p89|~(p91)), file('<stdin>', ax208)).
% 24.01/24.23 thf(ax206, axiom, (p91|~(p93)), file('<stdin>', ax206)).
% 24.01/24.23 thf(ax204, axiom, (p93|~(p95)), file('<stdin>', ax204)).
% 24.01/24.23 thf(ax202, axiom, (p95|~(p97)), file('<stdin>', ax202)).
% 24.01/24.23 thf(ax201, axiom, (p97|~(p98)), file('<stdin>', ax201)).
% 24.01/24.23 thf(ax200, axiom, (p98|~(p99)), file('<stdin>', ax200)).
% 24.01/24.23 thf(ax199, axiom, (p99|~(p100)), file('<stdin>', ax199)).
% 24.01/24.23 thf(ax38, axiom, (~(p5)|~(p40)|p254), file('<stdin>', ax38)).
% 24.01/24.23 thf(ax259, axiom, (p39|p40), file('<stdin>', ax259)).
% 24.01/24.23 thf(ax197, axiom, (p100|~(p102)), file('<stdin>', ax197)).
% 24.01/24.23 thf(ax29, axiom, (~(p254)|p263), file('<stdin>', ax29)).
% 24.01/24.23 thf(ax294, axiom, p5, file('<stdin>', ax294)).
% 24.01/24.23 thf(ax24, axiom, (~(p261)|p273), file('<stdin>', ax24)).
% 24.01/24.23 thf(ax196, axiom, (p102|~(p103)), file('<stdin>', ax196)).
% 24.01/24.23 thf(ax30, axiom, (~(p263)|p262), file('<stdin>', ax30)).
% 24.01/24.23 thf(ax23, axiom, (~(p273)|p272), file('<stdin>', ax23)).
% 24.01/24.23 thf(ax37, axiom, p261, file('<stdin>', ax37)).
% 24.01/24.23 thf(nax103, axiom, (p103<=(((f__2)=(f__0)=>f__3)=>((fin @ f__2 @ f__1=>f__3)=>f__3))), file('<stdin>', nax103)).
% 24.01/24.23 thf(ax19, axiom, (~(p262)|p269), file('<stdin>', ax19)).
% 24.01/24.23 thf(ax22, axiom, (~(p272)|~(p101)|p271), file('<stdin>', ax22)).
% 24.01/24.23 thf(ax198, axiom, (p100|p101), file('<stdin>', ax198)).
% 24.01/24.23 thf(pax107, axiom, (p107=>f__3), file('<stdin>', pax107)).
% 24.01/24.23 thf(ax183, axiom, (~(p108)|~(p115)|p107), file('<stdin>', ax183)).
% 24.01/24.23 thf(ax20, axiom, (~(p270)|~(p269)|p268), file('<stdin>', ax20)).
% 24.01/24.23 thf(ax21, axiom, (~(p271)|p270), file('<stdin>', ax21)).
% 24.01/24.23 thf(ax194, axiom, (p103|~(p105)), file('<stdin>', ax194)).
% 24.01/24.23 thf(ax192, axiom, (p105|p108), file('<stdin>', ax192)).
% 24.01/24.23 thf(pax268, axiom, (p268=>(~((f__2)=(f__0))=>fin @ f__2 @ f__1)), file('<stdin>', pax268)).
% 24.01/24.23 thf(pax104, axiom, (p104=>((f__2)=(f__0)=>f__3)), file('<stdin>', pax104)).
% 24.01/24.23 thf(ax195, axiom, (p103|p104), file('<stdin>', ax195)).
% 24.01/24.23 thf(nax115, axiom, (p115<=fin @ f__2 @ f__1), file('<stdin>', nax115)).
% 24.01/24.23 thf(c_0_59, plain, (p1|~p37), inference(fof_simplification,[status(thm)],[ax262])).
% 24.01/24.23 thf(c_0_60, plain, ~p1, inference(fof_simplification,[status(thm)],[ax298])).
% 24.01/24.23 thf(c_0_61, plain, (p37|~p39), inference(fof_simplification,[status(thm)],[ax260])).
% 24.01/24.23 thf(c_0_62, plain, (p1|~p37), inference(split_conjunct,[status(thm)],[c_0_59])).
% 24.01/24.23 thf(c_0_63, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_60])).
% 24.01/24.23 thf(c_0_64, plain, (p39|~p41), inference(fof_simplification,[status(thm)],[ax258])).
% 24.01/24.23 thf(c_0_65, plain, (p37|~p39), inference(split_conjunct,[status(thm)],[c_0_61])).
% 24.01/24.23 thf(c_0_66, plain, ~p37, inference(sr,[status(thm)],[c_0_62, c_0_63])).
% 24.01/24.23 thf(c_0_67, plain, (p41|~p43), inference(fof_simplification,[status(thm)],[ax256])).
% 24.01/24.23 thf(c_0_68, plain, (p39|~p41), inference(split_conjunct,[status(thm)],[c_0_64])).
% 24.01/24.23 thf(c_0_69, plain, ~p39, inference(sr,[status(thm)],[c_0_65, c_0_66])).
% 24.01/24.23 thf(c_0_70, plain, (p43|~p45), inference(fof_simplification,[status(thm)],[ax254])).
% 24.01/24.23 thf(c_0_71, plain, (p41|~p43), inference(split_conjunct,[status(thm)],[c_0_67])).
% 24.01/24.23 thf(c_0_72, plain, ~p41, inference(sr,[status(thm)],[c_0_68, c_0_69])).
% 24.01/24.23 thf(c_0_73, plain, (p45|~p47), inference(fof_simplification,[status(thm)],[ax252])).
% 24.01/24.23 thf(c_0_74, plain, (p43|~p45), inference(split_conjunct,[status(thm)],[c_0_70])).
% 24.01/24.23 thf(c_0_75, plain, ~p43, inference(sr,[status(thm)],[c_0_71, c_0_72])).
% 24.01/24.23 thf(c_0_76, plain, (p47|~p49), inference(fof_simplification,[status(thm)],[ax250])).
% 24.01/24.23 thf(c_0_77, plain, (p45|~p47), inference(split_conjunct,[status(thm)],[c_0_73])).
% 24.01/24.23 thf(c_0_78, plain, ~p45, inference(sr,[status(thm)],[c_0_74, c_0_75])).
% 24.01/24.23 thf(c_0_79, plain, (p49|~p51), inference(fof_simplification,[status(thm)],[ax248])).
% 24.01/24.23 thf(c_0_80, plain, (p47|~p49), inference(split_conjunct,[status(thm)],[c_0_76])).
% 24.01/24.23 thf(c_0_81, plain, ~p47, inference(sr,[status(thm)],[c_0_77, c_0_78])).
% 24.01/24.23 thf(c_0_82, plain, (p51|~p53), inference(fof_simplification,[status(thm)],[ax246])).
% 24.01/24.23 thf(c_0_83, plain, (p49|~p51), inference(split_conjunct,[status(thm)],[c_0_79])).
% 24.01/24.23 thf(c_0_84, plain, ~p49, inference(sr,[status(thm)],[c_0_80, c_0_81])).
% 24.01/24.23 thf(c_0_85, plain, (p53|~p55), inference(fof_simplification,[status(thm)],[ax244])).
% 24.01/24.23 thf(c_0_86, plain, (p51|~p53), inference(split_conjunct,[status(thm)],[c_0_82])).
% 24.01/24.23 thf(c_0_87, plain, ~p51, inference(sr,[status(thm)],[c_0_83, c_0_84])).
% 24.01/24.23 thf(c_0_88, plain, (p55|~p57), inference(fof_simplification,[status(thm)],[ax242])).
% 24.01/24.23 thf(c_0_89, plain, (p53|~p55), inference(split_conjunct,[status(thm)],[c_0_85])).
% 24.01/24.23 thf(c_0_90, plain, ~p53, inference(sr,[status(thm)],[c_0_86, c_0_87])).
% 24.01/24.23 thf(c_0_91, plain, (p57|~p59), inference(fof_simplification,[status(thm)],[ax240])).
% 24.01/24.23 thf(c_0_92, plain, (p55|~p57), inference(split_conjunct,[status(thm)],[c_0_88])).
% 24.01/24.23 thf(c_0_93, plain, ~p55, inference(sr,[status(thm)],[c_0_89, c_0_90])).
% 24.01/24.23 thf(c_0_94, plain, (p59|~p61), inference(fof_simplification,[status(thm)],[ax238])).
% 24.01/24.23 thf(c_0_95, plain, (p57|~p59), inference(split_conjunct,[status(thm)],[c_0_91])).
% 24.01/24.23 thf(c_0_96, plain, ~p57, inference(sr,[status(thm)],[c_0_92, c_0_93])).
% 24.01/24.23 thf(c_0_97, plain, (p61|~p63), inference(fof_simplification,[status(thm)],[ax236])).
% 24.01/24.23 thf(c_0_98, plain, (p59|~p61), inference(split_conjunct,[status(thm)],[c_0_94])).
% 24.01/24.23 thf(c_0_99, plain, ~p59, inference(sr,[status(thm)],[c_0_95, c_0_96])).
% 24.01/24.23 thf(c_0_100, plain, (p63|~p65), inference(fof_simplification,[status(thm)],[ax234])).
% 24.01/24.23 thf(c_0_101, plain, (p61|~p63), inference(split_conjunct,[status(thm)],[c_0_97])).
% 24.01/24.23 thf(c_0_102, plain, ~p61, inference(sr,[status(thm)],[c_0_98, c_0_99])).
% 24.01/24.23 thf(c_0_103, plain, (p65|~p67), inference(fof_simplification,[status(thm)],[ax232])).
% 24.01/24.23 thf(c_0_104, plain, (p63|~p65), inference(split_conjunct,[status(thm)],[c_0_100])).
% 24.01/24.23 thf(c_0_105, plain, ~p63, inference(sr,[status(thm)],[c_0_101, c_0_102])).
% 24.01/24.23 thf(c_0_106, plain, (p67|~p69), inference(fof_simplification,[status(thm)],[ax230])).
% 24.01/24.23 thf(c_0_107, plain, (p65|~p67), inference(split_conjunct,[status(thm)],[c_0_103])).
% 24.01/24.23 thf(c_0_108, plain, ~p65, inference(sr,[status(thm)],[c_0_104, c_0_105])).
% 24.01/24.23 thf(c_0_109, plain, (p69|~p71), inference(fof_simplification,[status(thm)],[ax228])).
% 24.01/24.23 thf(c_0_110, plain, (p67|~p69), inference(split_conjunct,[status(thm)],[c_0_106])).
% 24.01/24.23 thf(c_0_111, plain, ~p67, inference(sr,[status(thm)],[c_0_107, c_0_108])).
% 24.01/24.23 thf(c_0_112, plain, (p71|~p73), inference(fof_simplification,[status(thm)],[ax226])).
% 24.01/24.23 thf(c_0_113, plain, (p69|~p71), inference(split_conjunct,[status(thm)],[c_0_109])).
% 24.01/24.23 thf(c_0_114, plain, ~p69, inference(sr,[status(thm)],[c_0_110, c_0_111])).
% 24.01/24.23 thf(c_0_115, plain, (p73|~p75), inference(fof_simplification,[status(thm)],[ax224])).
% 24.01/24.23 thf(c_0_116, plain, (p71|~p73), inference(split_conjunct,[status(thm)],[c_0_112])).
% 24.01/24.23 thf(c_0_117, plain, ~p71, inference(sr,[status(thm)],[c_0_113, c_0_114])).
% 24.01/24.23 thf(c_0_118, plain, (p75|~p77), inference(fof_simplification,[status(thm)],[ax222])).
% 24.01/24.23 thf(c_0_119, plain, (p73|~p75), inference(split_conjunct,[status(thm)],[c_0_115])).
% 24.01/24.23 thf(c_0_120, plain, ~p73, inference(sr,[status(thm)],[c_0_116, c_0_117])).
% 24.01/24.23 thf(c_0_121, plain, (p77|~p79), inference(fof_simplification,[status(thm)],[ax220])).
% 24.01/24.23 thf(c_0_122, plain, (p75|~p77), inference(split_conjunct,[status(thm)],[c_0_118])).
% 24.01/24.23 thf(c_0_123, plain, ~p75, inference(sr,[status(thm)],[c_0_119, c_0_120])).
% 24.01/24.23 thf(c_0_124, plain, (p79|~p81), inference(fof_simplification,[status(thm)],[ax218])).
% 24.01/24.23 thf(c_0_125, plain, (p77|~p79), inference(split_conjunct,[status(thm)],[c_0_121])).
% 24.01/24.23 thf(c_0_126, plain, ~p77, inference(sr,[status(thm)],[c_0_122, c_0_123])).
% 24.01/24.23 thf(c_0_127, plain, (p81|~p83), inference(fof_simplification,[status(thm)],[ax216])).
% 24.01/24.23 thf(c_0_128, plain, (p79|~p81), inference(split_conjunct,[status(thm)],[c_0_124])).
% 24.01/24.23 thf(c_0_129, plain, ~p79, inference(sr,[status(thm)],[c_0_125, c_0_126])).
% 24.01/24.23 thf(c_0_130, plain, (p83|~p85), inference(fof_simplification,[status(thm)],[ax214])).
% 24.01/24.23 thf(c_0_131, plain, (p81|~p83), inference(split_conjunct,[status(thm)],[c_0_127])).
% 24.01/24.23 thf(c_0_132, plain, ~p81, inference(sr,[status(thm)],[c_0_128, c_0_129])).
% 24.01/24.23 thf(c_0_133, plain, (p85|~p87), inference(fof_simplification,[status(thm)],[ax212])).
% 24.01/24.23 thf(c_0_134, plain, (p83|~p85), inference(split_conjunct,[status(thm)],[c_0_130])).
% 24.01/24.23 thf(c_0_135, plain, ~p83, inference(sr,[status(thm)],[c_0_131, c_0_132])).
% 24.01/24.23 thf(c_0_136, plain, (p87|~p89), inference(fof_simplification,[status(thm)],[ax210])).
% 24.01/24.23 thf(c_0_137, plain, (p85|~p87), inference(split_conjunct,[status(thm)],[c_0_133])).
% 24.01/24.23 thf(c_0_138, plain, ~p85, inference(sr,[status(thm)],[c_0_134, c_0_135])).
% 24.01/24.23 thf(c_0_139, plain, (p89|~p91), inference(fof_simplification,[status(thm)],[ax208])).
% 24.01/24.23 thf(c_0_140, plain, (p87|~p89), inference(split_conjunct,[status(thm)],[c_0_136])).
% 24.01/24.23 thf(c_0_141, plain, ~p87, inference(sr,[status(thm)],[c_0_137, c_0_138])).
% 24.01/24.23 thf(c_0_142, plain, (p91|~p93), inference(fof_simplification,[status(thm)],[ax206])).
% 24.01/24.23 thf(c_0_143, plain, (p89|~p91), inference(split_conjunct,[status(thm)],[c_0_139])).
% 24.01/24.23 thf(c_0_144, plain, ~p89, inference(sr,[status(thm)],[c_0_140, c_0_141])).
% 24.01/24.23 thf(c_0_145, plain, (p93|~p95), inference(fof_simplification,[status(thm)],[ax204])).
% 24.01/24.23 thf(c_0_146, plain, (p91|~p93), inference(split_conjunct,[status(thm)],[c_0_142])).
% 24.01/24.23 thf(c_0_147, plain, ~p91, inference(sr,[status(thm)],[c_0_143, c_0_144])).
% 24.01/24.23 thf(c_0_148, plain, (p95|~p97), inference(fof_simplification,[status(thm)],[ax202])).
% 24.01/24.23 thf(c_0_149, plain, (p93|~p95), inference(split_conjunct,[status(thm)],[c_0_145])).
% 24.01/24.23 thf(c_0_150, plain, ~p93, inference(sr,[status(thm)],[c_0_146, c_0_147])).
% 24.01/24.23 thf(c_0_151, plain, (p97|~p98), inference(fof_simplification,[status(thm)],[ax201])).
% 24.01/24.23 thf(c_0_152, plain, (p95|~p97), inference(split_conjunct,[status(thm)],[c_0_148])).
% 24.01/24.23 thf(c_0_153, plain, ~p95, inference(sr,[status(thm)],[c_0_149, c_0_150])).
% 24.01/24.23 thf(c_0_154, plain, (p98|~p99), inference(fof_simplification,[status(thm)],[ax200])).
% 24.01/24.23 thf(c_0_155, plain, (p97|~p98), inference(split_conjunct,[status(thm)],[c_0_151])).
% 24.01/24.23 thf(c_0_156, plain, ~p97, inference(sr,[status(thm)],[c_0_152, c_0_153])).
% 24.01/24.23 thf(c_0_157, plain, (p99|~p100), inference(fof_simplification,[status(thm)],[ax199])).
% 24.01/24.23 thf(c_0_158, plain, (p98|~p99), inference(split_conjunct,[status(thm)],[c_0_154])).
% 24.01/24.23 thf(c_0_159, plain, ~p98, inference(sr,[status(thm)],[c_0_155, c_0_156])).
% 24.01/24.23 thf(c_0_160, plain, (~p5|~p40|p254), inference(fof_simplification,[status(thm)],[ax38])).
% 24.01/24.23 thf(c_0_161, plain, (p39|p40), inference(split_conjunct,[status(thm)],[ax259])).
% 24.01/24.23 thf(c_0_162, plain, (p100|~p102), inference(fof_simplification,[status(thm)],[ax197])).
% 24.01/24.23 thf(c_0_163, plain, (p99|~p100), inference(split_conjunct,[status(thm)],[c_0_157])).
% 24.01/24.23 thf(c_0_164, plain, ~p99, inference(sr,[status(thm)],[c_0_158, c_0_159])).
% 24.01/24.23 thf(c_0_165, plain, (~p254|p263), inference(fof_simplification,[status(thm)],[ax29])).
% 24.01/24.23 thf(c_0_166, plain, (p254|~p5|~p40), inference(split_conjunct,[status(thm)],[c_0_160])).
% 24.01/24.23 thf(c_0_167, plain, p5, inference(split_conjunct,[status(thm)],[ax294])).
% 24.01/24.23 thf(c_0_168, plain, p40, inference(sr,[status(thm)],[c_0_161, c_0_69])).
% 24.01/24.23 thf(c_0_169, plain, (~p261|p273), inference(fof_simplification,[status(thm)],[ax24])).
% 24.01/24.23 thf(c_0_170, plain, (p102|~p103), inference(fof_simplification,[status(thm)],[ax196])).
% 24.01/24.23 thf(c_0_171, plain, (p100|~p102), inference(split_conjunct,[status(thm)],[c_0_162])).
% 24.01/24.23 thf(c_0_172, plain, ~p100, inference(sr,[status(thm)],[c_0_163, c_0_164])).
% 24.01/24.23 thf(c_0_173, plain, (~p263|p262), inference(fof_simplification,[status(thm)],[ax30])).
% 24.01/24.23 thf(c_0_174, plain, (p263|~p254), inference(split_conjunct,[status(thm)],[c_0_165])).
% 24.01/24.23 thf(c_0_175, plain, p254, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_166, c_0_167]), c_0_168])])).
% 24.01/24.23 thf(c_0_176, plain, (~p273|p272), inference(fof_simplification,[status(thm)],[ax23])).
% 24.01/24.23 thf(c_0_177, plain, (p273|~p261), inference(split_conjunct,[status(thm)],[c_0_169])).
% 24.01/24.23 thf(c_0_178, plain, p261, inference(split_conjunct,[status(thm)],[ax37])).
% 24.01/24.23 thf(c_0_179, plain, (((f__2)!=(f__0)|f__3|p103)&((~fin @ f__2 @ f__1|f__3|p103)&(~f__3|p103))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax103])])])).
% 24.01/24.23 thf(c_0_180, plain, (p102|~p103), inference(split_conjunct,[status(thm)],[c_0_170])).
% 24.01/24.23 thf(c_0_181, plain, ~p102, inference(sr,[status(thm)],[c_0_171, c_0_172])).
% 24.01/24.23 thf(c_0_182, plain, (~p262|p269), inference(fof_simplification,[status(thm)],[ax19])).
% 24.01/24.23 thf(c_0_183, plain, (p262|~p263), inference(split_conjunct,[status(thm)],[c_0_173])).
% 24.01/24.23 thf(c_0_184, plain, p263, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_174, c_0_175])])).
% 24.01/24.23 thf(c_0_185, plain, (~p272|~p101|p271), inference(fof_simplification,[status(thm)],[ax22])).
% 24.01/24.23 thf(c_0_186, plain, (p100|p101), inference(split_conjunct,[status(thm)],[ax198])).
% 24.01/24.23 thf(c_0_187, plain, (p272|~p273), inference(split_conjunct,[status(thm)],[c_0_176])).
% 24.01/24.23 thf(c_0_188, plain, p273, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_177, c_0_178])])).
% 24.01/24.23 thf(c_0_189, plain, (~p107|f__3), inference(fof_nnf,[status(thm)],[pax107])).
% 24.01/24.23 thf(c_0_190, plain, (~p108|~p115|p107), inference(fof_simplification,[status(thm)],[ax183])).
% 24.01/24.23 thf(c_0_191, plain, (p103|~f__3), inference(split_conjunct,[status(thm)],[c_0_179])).
% 24.01/24.23 thf(c_0_192, plain, ~p103, inference(sr,[status(thm)],[c_0_180, c_0_181])).
% 24.01/24.23 thf(c_0_193, plain, (~p270|~p269|p268), inference(fof_simplification,[status(thm)],[ax20])).
% 24.01/24.23 thf(c_0_194, plain, (p269|~p262), inference(split_conjunct,[status(thm)],[c_0_182])).
% 24.01/24.23 thf(c_0_195, plain, p262, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_183, c_0_184])])).
% 24.01/24.23 thf(c_0_196, plain, (~p271|p270), inference(fof_simplification,[status(thm)],[ax21])).
% 24.01/24.23 thf(c_0_197, plain, (p271|~p272|~p101), inference(split_conjunct,[status(thm)],[c_0_185])).
% 24.01/24.23 thf(c_0_198, plain, p101, inference(sr,[status(thm)],[c_0_186, c_0_172])).
% 24.01/24.23 thf(c_0_199, plain, p272, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_187, c_0_188])])).
% 24.01/24.23 thf(c_0_200, plain, (f__3|~p107), inference(split_conjunct,[status(thm)],[c_0_189])).
% 24.01/24.23 thf(c_0_201, plain, (p107|~p108|~p115), inference(split_conjunct,[status(thm)],[c_0_190])).
% 24.01/24.23 thf(c_0_202, plain, ~f__3, inference(sr,[status(thm)],[c_0_191, c_0_192])).
% 24.01/24.23 thf(c_0_203, plain, (p268|~p270|~p269), inference(split_conjunct,[status(thm)],[c_0_193])).
% 24.01/24.23 thf(c_0_204, plain, p269, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_194, c_0_195])])).
% 24.01/24.23 thf(c_0_205, plain, (p270|~p271), inference(split_conjunct,[status(thm)],[c_0_196])).
% 24.01/24.23 thf(c_0_206, plain, p271, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_197, c_0_198]), c_0_199])])).
% 24.01/24.23 thf(c_0_207, plain, (p103|~p105), inference(fof_simplification,[status(thm)],[ax194])).
% 24.01/24.23 thf(c_0_208, plain, (~p108|~p115), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_200, c_0_201]), c_0_202])).
% 24.01/24.23 thf(c_0_209, plain, (p105|p108), inference(split_conjunct,[status(thm)],[ax192])).
% 24.01/24.23 thf(c_0_210, plain, (~p268|((f__2)=(f__0)|fin @ f__2 @ f__1)), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax268])])).
% 24.01/24.23 thf(c_0_211, plain, (p268|~p270), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_203, c_0_204])])).
% 24.01/24.23 thf(c_0_212, plain, p270, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_205, c_0_206])])).
% 24.01/24.23 thf(c_0_213, plain, (~p104|((f__2)!=(f__0)|f__3)), inference(fof_nnf,[status(thm)],[pax104])).
% 24.01/24.23 thf(c_0_214, plain, (p103|p104), inference(split_conjunct,[status(thm)],[ax195])).
% 24.01/24.23 thf(c_0_215, plain, (~fin @ f__2 @ f__1|p115), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax115])])).
% 24.01/24.23 thf(c_0_216, plain, (p103|~p105), inference(split_conjunct,[status(thm)],[c_0_207])).
% 24.01/24.23 thf(c_0_217, plain, (p105|~p115), inference(spm,[status(thm)],[c_0_208, c_0_209])).
% 24.01/24.23 thf(c_0_218, plain, ((f__2)=(f__0)|fin @ f__2 @ f__1|~p268), inference(split_conjunct,[status(thm)],[c_0_210])).
% 24.01/24.23 thf(c_0_219, plain, p268, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_211, c_0_212])])).
% 24.01/24.23 thf(c_0_220, plain, (f__3|~p104|(f__2)!=(f__0)), inference(split_conjunct,[status(thm)],[c_0_213])).
% 24.01/24.23 thf(c_0_221, plain, p104, inference(sr,[status(thm)],[c_0_214, c_0_192])).
% 24.01/24.23 thf(c_0_222, plain, (p115|~fin @ f__2 @ f__1), inference(split_conjunct,[status(thm)],[c_0_215])).
% 24.01/24.23 thf(c_0_223, plain, ~p115, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_216, c_0_217]), c_0_192])).
% 24.01/24.23 thf(c_0_224, plain, ((f__0)=(f__2)|fin @ f__2 @ f__1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_218, c_0_219])])).
% 24.01/24.23 thf(c_0_225, plain, (f__0)!=(f__2), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_220, c_0_221])]), c_0_202])).
% 24.01/24.23 thf(c_0_226, plain, ~fin @ f__2 @ f__1, inference(sr,[status(thm)],[c_0_222, c_0_223])).
% 24.01/24.23 thf(c_0_227, plain, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_224, c_0_225]), c_0_226]), ['proof']).
% 24.01/24.23 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 24.01/24.23 thf(0,theorem,(setextAx => (emptysetAx => (setadjoinAx => (powersetAx => (setunionAx => (omega0Ax => (omegaSAx => (omegaIndAx => (replAx => (foundationAx => (wellorderingAx => (descrp => (dsetconstrI => (dsetconstrEL => (dsetconstrER => (exuE1 => (prop2setE => (emptysetE => (emptysetimpfalse => (notinemptyset => (exuE3e => (setext => (emptyI => (noeltsimpempty => (setbeta => (nonemptyE1 => (nonemptyI => (nonemptyI1 => (setadjoinIL => (emptyinunitempty => (setadjoinIR => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ X2)) => (![X4:$o]:(((X3 = X1) => X4) => ((((in @ X3) @ X2) => X4) => X4)))))))))))))))))))))))))))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 24.01/24.23 % SZS output end Proof
%------------------------------------------------------------------------------