%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU514^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 : n010.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.12s 24.34s
% Output : Proof 24.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.13 % Problem : SEU514^1 : TPTP v9.2.0. Released v3.7.0.
% 0.09/0.14 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.36 % Computer : n010.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed Oct 8 21:38:38 EDT 2025
% 0.14/0.36 % CPUTime :
% 24.12/24.34 % SZS status Theorem
% 24.12/24.34 % Mode: mode371
% 24.12/24.34 % Inferences: 4003
% 24.12/24.34 % SZS output start Proof
% 24.12/24.34 thf(def_exu,definition,(exu = (^[X1:$i>$o]:(~((![X2:$i]:((X1 @ X2) => (~((![X3:$i]:((X1 @ X3) => (X2 = X3)))))))))))).
% 24.12/24.34 thf(def_setextAx,definition,(setextAx = (![X1:$i]:(![X2:$i]:((![X3:$i]:(((in @ X3) @ X1) = ((in @ X3) @ X2))) => (X1 = X2)))))).
% 24.12/24.34 thf(def_emptysetAx,definition,(emptysetAx = (![X1:$i]:(~(((in @ X1) @ emptyset)))))).
% 24.12/24.34 thf(def_setadjoinAx,definition,(setadjoinAx = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ X2)) = ((~((X3 = X1))) => ((in @ X3) @ X2)))))))).
% 24.12/24.34 thf(def_powersetAx,definition,(powersetAx = (![X1:$i]:(![X2:$i]:(((in @ X2) @ (powerset @ X1)) = (![X3:$i]:(((in @ X3) @ X2) => ((in @ X3) @ X1)))))))).
% 24.12/24.34 thf(def_setunionAx,definition,(setunionAx = (![X1:$i]:(![X2:$i]:(((in @ X2) @ (setunion @ X1)) = (~((![X3:$i]:(((in @ X2) @ X3) => (~(((in @ X3) @ X1)))))))))))).
% 24.12/24.34 thf(def_omega0Ax,definition,(omega0Ax = ((in @ emptyset) @ omega))).
% 24.12/24.34 thf(def_omegaSAx,definition,(omegaSAx = (![X1:$i]:(((in @ X1) @ omega) => ((in @ ((setadjoin @ X1) @ X1)) @ omega))))).
% 24.12/24.34 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.12/24.34 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.12/24.34 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.12/24.34 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.12/24.34 thf(def_descrp,definition,(descrp = (![X1:$i>$o]:((exu @ X1) => (X1 @ (descr @ X1)))))).
% 24.12/24.34 thf(def_dsetconstrI,definition,(dsetconstrI = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ X1) => ((X2 @ X3) => ((in @ X3) @ ((dsetconstr @ X1) @ X2))))))))).
% 24.12/24.34 thf(def_dsetconstrEL,definition,(dsetconstrEL = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ ((dsetconstr @ X1) @ X2)) => ((in @ X3) @ X1))))))).
% 24.12/24.34 thf(def_dsetconstrER,definition,(dsetconstrER = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ ((dsetconstr @ X1) @ X2)) => (X2 @ X3))))))).
% 24.12/24.34 thf(def_exuE1,definition,(exuE1 = (![X1:$i>$o]:((exu @ X1) => (~((![X2:$i]:((X1 @ X2) => (~((![X3:$i]:((X1 @ X3) => (X2 = X3))))))))))))).
% 24.12/24.34 thf(def_prop2set,definition,(prop2set = (^[X1:$o]:((dsetconstr @ (powerset @ emptyset)) @ (^[X2:$i]:X1))))).
% 24.12/24.34 thf(def_prop2setE,definition,(prop2setE = (![X1:$o]:(![X2:$i]:(((in @ X2) @ (prop2set @ X1)) => X1))))).
% 24.12/24.34 thf(def_emptysetE,definition,(emptysetE = (![X1:$i]:(((in @ X1) @ emptyset) => (![X2:$o]:X2))))).
% 24.12/24.34 thf(def_emptysetimpfalse,definition,(emptysetimpfalse = (![X1:$i]:(~(((in @ X1) @ emptyset)))))).
% 24.12/24.34 thf(def_notinemptyset,definition,(notinemptyset = (![X1:$i]:(~(((in @ X1) @ emptyset)))))).
% 24.12/24.34 thf(def_exuE3e,definition,(exuE3e = (![X1:$i>$o]:((exu @ X1) => (~((![X2:$i]:(~((X1 @ X2)))))))))).
% 24.12/24.34 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.12/24.34 thf(def_emptyI,definition,(emptyI = (![X1:$i]:((![X2:$i]:(~(((in @ X2) @ X1)))) => (X1 = emptyset))))).
% 24.12/24.34 thf(def_noeltsimpempty,definition,(noeltsimpempty = (![X1:$i]:((![X2:$i]:(~(((in @ X2) @ X1)))) => (X1 = emptyset))))).
% 24.12/24.34 thf(def_setbeta,definition,(setbeta = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ X1) => (((in @ X3) @ ((dsetconstr @ X1) @ X2)) = (X2 @ X3)))))))).
% 24.12/24.34 thf(def_nonempty,definition,(nonempty = (^[X1:$i]:(~((X1 = emptyset)))))).
% 24.12/24.34 thf(def_nonemptyE1,definition,(nonemptyE1 = (![X1:$i]:((nonempty @ X1) => (~((![X2:$i]:(~(((in @ X2) @ X1)))))))))).
% 24.12/24.34 thf(def_nonemptyI,definition,(nonemptyI = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ X1) => ((X2 @ X3) => (nonempty @ ((dsetconstr @ X1) @ X2))))))))).
% 24.12/24.34 thf(def_nonemptyI1,definition,(nonemptyI1 = (![X1:$i]:((~((![X2:$i]:(~(((in @ X2) @ X1)))))) => (nonempty @ X1))))).
% 24.12/24.34 thf(def_setadjoinIL,definition,(setadjoinIL = (![X1:$i]:(![X2:$i]:((in @ X1) @ ((setadjoin @ X1) @ X2)))))).
% 24.12/24.34 thf(def_emptyinunitempty,definition,(emptyinunitempty = ((in @ emptyset) @ ((setadjoin @ emptyset) @ emptyset)))).
% 24.12/24.34 thf(setadjoinIR,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 => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X2) => ((in @ X3) @ ((setadjoin @ X1) @ X2))))))))))))))))))))))))))))))))))))).
% 24.12/24.34 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 => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X2) => ((in @ X3) @ ((setadjoin @ X1) @ X2)))))))))))))))))))))))))))))))))))))),inference(assume_negation,[status(cth)],[setadjoinIR])).
% 24.12/24.34 thf(ax202, axiom, (p1|~(p36)), file('<stdin>', ax202)).
% 24.12/24.34 thf(ax237, axiom, ~(p1), file('<stdin>', ax237)).
% 24.12/24.34 thf(ax200, axiom, (p36|~(p38)), file('<stdin>', ax200)).
% 24.12/24.34 thf(ax198, axiom, (p38|~(p40)), file('<stdin>', ax198)).
% 24.12/24.34 thf(ax196, axiom, (p40|~(p42)), file('<stdin>', ax196)).
% 24.12/24.34 thf(ax194, axiom, (p42|~(p44)), file('<stdin>', ax194)).
% 24.12/24.34 thf(ax192, axiom, (p44|~(p46)), file('<stdin>', ax192)).
% 24.12/24.34 thf(ax190, axiom, (p46|~(p48)), file('<stdin>', ax190)).
% 24.12/24.34 thf(ax188, axiom, (p48|~(p50)), file('<stdin>', ax188)).
% 24.12/24.34 thf(ax186, axiom, (p50|~(p52)), file('<stdin>', ax186)).
% 24.12/24.34 thf(ax184, axiom, (p52|~(p54)), file('<stdin>', ax184)).
% 24.12/24.34 thf(ax182, axiom, (p54|~(p56)), file('<stdin>', ax182)).
% 24.12/24.34 thf(ax180, axiom, (p56|~(p58)), file('<stdin>', ax180)).
% 24.12/24.34 thf(ax178, axiom, (p58|~(p60)), file('<stdin>', ax178)).
% 24.12/24.34 thf(ax176, axiom, (p60|~(p62)), file('<stdin>', ax176)).
% 24.12/24.34 thf(ax174, axiom, (p62|~(p64)), file('<stdin>', ax174)).
% 24.12/24.34 thf(ax172, axiom, (p64|~(p66)), file('<stdin>', ax172)).
% 24.12/24.34 thf(ax170, axiom, (p66|~(p68)), file('<stdin>', ax170)).
% 24.12/24.34 thf(ax168, axiom, (p68|~(p70)), file('<stdin>', ax168)).
% 24.12/24.34 thf(ax166, axiom, (p70|~(p72)), file('<stdin>', ax166)).
% 24.12/24.34 thf(ax164, axiom, (p72|~(p74)), file('<stdin>', ax164)).
% 24.12/24.34 thf(ax162, axiom, (p74|~(p76)), file('<stdin>', ax162)).
% 24.12/24.34 thf(ax160, axiom, (p76|~(p78)), file('<stdin>', ax160)).
% 24.12/24.34 thf(ax158, axiom, (p78|~(p80)), file('<stdin>', ax158)).
% 24.12/24.34 thf(nax1, axiom, (p1<=(fsetextAx=>(femptysetAx=>(fsetadjoinAx=>(fpowersetAx=>(fsetunionAx=>(fomega0Ax=>(fomegaSAx=>(fomegaIndAx=>(freplAx=>(ffoundationAx=>(fwellorderingAx=>(fdescrp=>(fdsetconstrI=>(fdsetconstrEL=>(fdsetconstrER=>(fexuE1=>(fprop2setE=>(femptysetE=>(femptysetimpfalse=>(fnotinemptyset=>(fexuE3e=>(fsetext=>(femptyI=>(fnoeltsimpempty=>(fsetbeta=>(fnonemptyE1=>(fnonemptyI=>(fnonemptyI1=>(fsetadjoinIL=>(femptyinunitempty=>![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ X2=>fin @ X3 @ (fsetadjoin @ X1 @ X2))))))))))))))))))))))))))))))))), file('<stdin>', nax1)).
% 24.12/24.34 thf(ax156, axiom, (p80|~(p82)), file('<stdin>', ax156)).
% 24.12/24.34 thf(ax154, axiom, (p82|~(p84)), file('<stdin>', ax154)).
% 24.12/24.34 thf(ax36, axiom, (~(p5)|~(p39)|p193), file('<stdin>', ax36)).
% 24.12/24.34 thf(nax39, axiom, (p39<=fsetadjoinAx), file('<stdin>', nax39)).
% 24.12/24.34 thf(ax152, axiom, (p84|~(p86)), file('<stdin>', ax152)).
% 24.12/24.34 thf(ax233, axiom, p5, file('<stdin>', ax233)).
% 24.12/24.34 thf(ax150, axiom, (p86|~(p88)), file('<stdin>', ax150)).
% 24.12/24.34 thf(ax27, axiom, (~(p193)|p202), file('<stdin>', ax27)).
% 24.12/24.34 thf(ax148, axiom, (p88|~(p90)), file('<stdin>', ax148)).
% 24.12/24.34 thf(ax28, axiom, (~(p202)|p201), file('<stdin>', ax28)).
% 24.12/24.34 thf(ax146, axiom, (p90|~(p92)), file('<stdin>', ax146)).
% 24.12/24.34 thf(ax17, axiom, (~(p201)|p208), file('<stdin>', ax17)).
% 24.12/24.34 thf(ax144, axiom, (p92|~(p94)), file('<stdin>', ax144)).
% 24.12/24.34 thf(ax22, axiom, (~(p200)|p212), file('<stdin>', ax22)).
% 24.12/24.34 thf(ax13, axiom, (~(p214)|~(p208)|~(p213)), file('<stdin>', ax13)).
% 24.12/24.34 thf(nax213, axiom, (p213<=(fin @ f__2 @ f__1=>(~((f__2)=(f__0))=>fin @ f__2 @ f__1))), file('<stdin>', nax213)).
% 24.12/24.34 thf(ax143, axiom, (p94|~(p95)), file('<stdin>', ax143)).
% 24.12/24.34 thf(ax16, axiom, (~(p212)|p216), file('<stdin>', ax16)).
% 24.12/24.34 thf(ax35, axiom, p200, file('<stdin>', ax35)).
% 24.12/24.34 thf(ax142, axiom, (p95|~(p96)), file('<stdin>', ax142)).
% 24.12/24.34 thf(ax15, axiom, (~(p216)|p97|p215), file('<stdin>', ax15)).
% 24.12/24.34 thf(ax14, axiom, (~(p215)|p214), file('<stdin>', ax14)).
% 24.12/24.34 thf(ax141, axiom, (p96|~(p97)), file('<stdin>', ax141)).
% 24.12/24.34 thf(c_0_48, plain, (p1|~p36), inference(fof_simplification,[status(thm)],[ax202])).
% 24.12/24.34 thf(c_0_49, plain, ~p1, inference(fof_simplification,[status(thm)],[ax237])).
% 24.12/24.34 thf(c_0_50, plain, (p36|~p38), inference(fof_simplification,[status(thm)],[ax200])).
% 24.12/24.34 thf(c_0_51, plain, (p1|~p36), inference(split_conjunct,[status(thm)],[c_0_48])).
% 24.12/24.34 thf(c_0_52, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_49])).
% 24.12/24.34 thf(c_0_53, plain, (p38|~p40), inference(fof_simplification,[status(thm)],[ax198])).
% 24.12/24.34 thf(c_0_54, plain, (p36|~p38), inference(split_conjunct,[status(thm)],[c_0_50])).
% 24.12/24.34 thf(c_0_55, plain, ~p36, inference(sr,[status(thm)],[c_0_51, c_0_52])).
% 24.12/24.34 thf(c_0_56, plain, (p40|~p42), inference(fof_simplification,[status(thm)],[ax196])).
% 24.12/24.34 thf(c_0_57, plain, (p38|~p40), inference(split_conjunct,[status(thm)],[c_0_53])).
% 24.12/24.34 thf(c_0_58, plain, ~p38, inference(sr,[status(thm)],[c_0_54, c_0_55])).
% 24.12/24.34 thf(c_0_59, plain, (p42|~p44), inference(fof_simplification,[status(thm)],[ax194])).
% 24.12/24.34 thf(c_0_60, plain, (p40|~p42), inference(split_conjunct,[status(thm)],[c_0_56])).
% 24.12/24.34 thf(c_0_61, plain, ~p40, inference(sr,[status(thm)],[c_0_57, c_0_58])).
% 24.12/24.34 thf(c_0_62, plain, (p44|~p46), inference(fof_simplification,[status(thm)],[ax192])).
% 24.12/24.34 thf(c_0_63, plain, (p42|~p44), inference(split_conjunct,[status(thm)],[c_0_59])).
% 24.12/24.34 thf(c_0_64, plain, ~p42, inference(sr,[status(thm)],[c_0_60, c_0_61])).
% 24.12/24.34 thf(c_0_65, plain, (p46|~p48), inference(fof_simplification,[status(thm)],[ax190])).
% 24.12/24.34 thf(c_0_66, plain, (p44|~p46), inference(split_conjunct,[status(thm)],[c_0_62])).
% 24.12/24.34 thf(c_0_67, plain, ~p44, inference(sr,[status(thm)],[c_0_63, c_0_64])).
% 24.12/24.34 thf(c_0_68, plain, (p48|~p50), inference(fof_simplification,[status(thm)],[ax188])).
% 24.12/24.34 thf(c_0_69, plain, (p46|~p48), inference(split_conjunct,[status(thm)],[c_0_65])).
% 24.12/24.34 thf(c_0_70, plain, ~p46, inference(sr,[status(thm)],[c_0_66, c_0_67])).
% 24.12/24.34 thf(c_0_71, plain, (p50|~p52), inference(fof_simplification,[status(thm)],[ax186])).
% 24.12/24.34 thf(c_0_72, plain, (p48|~p50), inference(split_conjunct,[status(thm)],[c_0_68])).
% 24.12/24.34 thf(c_0_73, plain, ~p48, inference(sr,[status(thm)],[c_0_69, c_0_70])).
% 24.12/24.34 thf(c_0_74, plain, (p52|~p54), inference(fof_simplification,[status(thm)],[ax184])).
% 24.12/24.34 thf(c_0_75, plain, (p50|~p52), inference(split_conjunct,[status(thm)],[c_0_71])).
% 24.12/24.34 thf(c_0_76, plain, ~p50, inference(sr,[status(thm)],[c_0_72, c_0_73])).
% 24.12/24.34 thf(c_0_77, plain, (p54|~p56), inference(fof_simplification,[status(thm)],[ax182])).
% 24.12/24.34 thf(c_0_78, plain, (p52|~p54), inference(split_conjunct,[status(thm)],[c_0_74])).
% 24.12/24.34 thf(c_0_79, plain, ~p52, inference(sr,[status(thm)],[c_0_75, c_0_76])).
% 24.12/24.34 thf(c_0_80, plain, (p56|~p58), inference(fof_simplification,[status(thm)],[ax180])).
% 24.12/24.34 thf(c_0_81, plain, (p54|~p56), inference(split_conjunct,[status(thm)],[c_0_77])).
% 24.12/24.34 thf(c_0_82, plain, ~p54, inference(sr,[status(thm)],[c_0_78, c_0_79])).
% 24.12/24.34 thf(c_0_83, plain, (p58|~p60), inference(fof_simplification,[status(thm)],[ax178])).
% 24.12/24.34 thf(c_0_84, plain, (p56|~p58), inference(split_conjunct,[status(thm)],[c_0_80])).
% 24.12/24.34 thf(c_0_85, plain, ~p56, inference(sr,[status(thm)],[c_0_81, c_0_82])).
% 24.12/24.34 thf(c_0_86, plain, (p60|~p62), inference(fof_simplification,[status(thm)],[ax176])).
% 24.12/24.34 thf(c_0_87, plain, (p58|~p60), inference(split_conjunct,[status(thm)],[c_0_83])).
% 24.12/24.34 thf(c_0_88, plain, ~p58, inference(sr,[status(thm)],[c_0_84, c_0_85])).
% 24.12/24.34 thf(c_0_89, plain, (p62|~p64), inference(fof_simplification,[status(thm)],[ax174])).
% 24.12/24.34 thf(c_0_90, plain, (p60|~p62), inference(split_conjunct,[status(thm)],[c_0_86])).
% 24.12/24.34 thf(c_0_91, plain, ~p60, inference(sr,[status(thm)],[c_0_87, c_0_88])).
% 24.12/24.34 thf(c_0_92, plain, (p64|~p66), inference(fof_simplification,[status(thm)],[ax172])).
% 24.12/24.34 thf(c_0_93, plain, (p62|~p64), inference(split_conjunct,[status(thm)],[c_0_89])).
% 24.12/24.34 thf(c_0_94, plain, ~p62, inference(sr,[status(thm)],[c_0_90, c_0_91])).
% 24.12/24.34 thf(c_0_95, plain, (p66|~p68), inference(fof_simplification,[status(thm)],[ax170])).
% 24.12/24.34 thf(c_0_96, plain, (p64|~p66), inference(split_conjunct,[status(thm)],[c_0_92])).
% 24.12/24.34 thf(c_0_97, plain, ~p64, inference(sr,[status(thm)],[c_0_93, c_0_94])).
% 24.12/24.34 thf(c_0_98, plain, (p68|~p70), inference(fof_simplification,[status(thm)],[ax168])).
% 24.12/24.34 thf(c_0_99, plain, (p66|~p68), inference(split_conjunct,[status(thm)],[c_0_95])).
% 24.12/24.34 thf(c_0_100, plain, ~p66, inference(sr,[status(thm)],[c_0_96, c_0_97])).
% 24.12/24.34 thf(c_0_101, plain, (p70|~p72), inference(fof_simplification,[status(thm)],[ax166])).
% 24.12/24.34 thf(c_0_102, plain, (p68|~p70), inference(split_conjunct,[status(thm)],[c_0_98])).
% 24.12/24.34 thf(c_0_103, plain, ~p68, inference(sr,[status(thm)],[c_0_99, c_0_100])).
% 24.12/24.34 thf(c_0_104, plain, (p72|~p74), inference(fof_simplification,[status(thm)],[ax164])).
% 24.12/24.34 thf(c_0_105, plain, (p70|~p72), inference(split_conjunct,[status(thm)],[c_0_101])).
% 24.12/24.34 thf(c_0_106, plain, ~p70, inference(sr,[status(thm)],[c_0_102, c_0_103])).
% 24.12/24.34 thf(c_0_107, plain, (p74|~p76), inference(fof_simplification,[status(thm)],[ax162])).
% 24.12/24.34 thf(c_0_108, plain, (p72|~p74), inference(split_conjunct,[status(thm)],[c_0_104])).
% 24.12/24.34 thf(c_0_109, plain, ~p72, inference(sr,[status(thm)],[c_0_105, c_0_106])).
% 24.12/24.34 thf(c_0_110, plain, (p76|~p78), inference(fof_simplification,[status(thm)],[ax160])).
% 24.12/24.34 thf(c_0_111, plain, (p74|~p76), inference(split_conjunct,[status(thm)],[c_0_107])).
% 24.12/24.34 thf(c_0_112, plain, ~p74, inference(sr,[status(thm)],[c_0_108, c_0_109])).
% 24.12/24.34 thf(c_0_113, plain, (epred1_0<=>(fomegaIndAx=>(freplAx=>(ffoundationAx=>(fwellorderingAx=>(fdescrp=>(fdsetconstrI=>(fdsetconstrEL=>(fdsetconstrER=>(fexuE1=>(fprop2setE=>(femptysetE=>(femptysetimpfalse=>(fnotinemptyset=>(fexuE3e=>(fsetext=>(femptyI=>(fnoeltsimpempty=>(fsetbeta=>(fnonemptyE1=>(fnonemptyI=>(fnonemptyI1=>(fsetadjoinIL=>(femptyinunitempty=>![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ X2=>fin @ X3 @ (fsetadjoin @ X1 @ X2)))))))))))))))))))))))))), introduced(definition)).
% 24.12/24.34 thf(c_0_114, plain, (p78|~p80), inference(fof_simplification,[status(thm)],[ax158])).
% 24.12/24.34 thf(c_0_115, plain, (p76|~p78), inference(split_conjunct,[status(thm)],[c_0_110])).
% 24.12/24.34 thf(c_0_116, plain, ~p76, inference(sr,[status(thm)],[c_0_111, c_0_112])).
% 24.12/24.34 thf(c_0_117, axiom, (p1<=(fsetextAx=>(femptysetAx=>(fsetadjoinAx=>(fpowersetAx=>(fsetunionAx=>(fomega0Ax=>(fomegaSAx=>epred1_0)))))))), inference(apply_def,[status(thm)],[nax1, c_0_113])).
% 24.12/24.34 thf(c_0_118, plain, (p80|~p82), inference(fof_simplification,[status(thm)],[ax156])).
% 24.12/24.34 thf(c_0_119, plain, (p78|~p80), inference(split_conjunct,[status(thm)],[c_0_114])).
% 24.12/24.34 thf(c_0_120, plain, ~p78, inference(sr,[status(thm)],[c_0_115, c_0_116])).
% 24.12/24.34 thf(c_0_121, plain, ((fsetextAx|p1)&((femptysetAx|p1)&((fsetadjoinAx|p1)&((fpowersetAx|p1)&((fsetunionAx|p1)&((fomega0Ax|p1)&((fomegaSAx|p1)&(~epred1_0|p1)))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_117])])])).
% 24.12/24.34 thf(c_0_122, plain, (p82|~p84), inference(fof_simplification,[status(thm)],[ax154])).
% 24.12/24.34 thf(c_0_123, plain, (p80|~p82), inference(split_conjunct,[status(thm)],[c_0_118])).
% 24.12/24.34 thf(c_0_124, plain, ~p80, inference(sr,[status(thm)],[c_0_119, c_0_120])).
% 24.12/24.34 thf(c_0_125, plain, (~p5|~p39|p193), inference(fof_simplification,[status(thm)],[ax36])).
% 24.12/24.34 thf(c_0_126, plain, (~fsetadjoinAx|p39), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax39])])).
% 24.12/24.34 thf(c_0_127, plain, (fsetadjoinAx|p1), inference(split_conjunct,[status(thm)],[c_0_121])).
% 24.12/24.34 thf(c_0_128, plain, (p84|~p86), inference(fof_simplification,[status(thm)],[ax152])).
% 24.12/24.34 thf(c_0_129, plain, (p82|~p84), inference(split_conjunct,[status(thm)],[c_0_122])).
% 24.12/24.34 thf(c_0_130, plain, ~p82, inference(sr,[status(thm)],[c_0_123, c_0_124])).
% 24.12/24.34 thf(c_0_131, plain, (p193|~p5|~p39), inference(split_conjunct,[status(thm)],[c_0_125])).
% 24.12/24.34 thf(c_0_132, plain, p5, inference(split_conjunct,[status(thm)],[ax233])).
% 24.12/24.34 thf(c_0_133, plain, (p39|~fsetadjoinAx), inference(split_conjunct,[status(thm)],[c_0_126])).
% 24.12/24.34 thf(c_0_134, plain, fsetadjoinAx, inference(sr,[status(thm)],[c_0_127, c_0_52])).
% 24.12/24.34 thf(c_0_135, plain, (p86|~p88), inference(fof_simplification,[status(thm)],[ax150])).
% 24.12/24.34 thf(c_0_136, plain, (p84|~p86), inference(split_conjunct,[status(thm)],[c_0_128])).
% 24.12/24.34 thf(c_0_137, plain, ~p84, inference(sr,[status(thm)],[c_0_129, c_0_130])).
% 24.12/24.34 thf(c_0_138, plain, (~p193|p202), inference(fof_simplification,[status(thm)],[ax27])).
% 24.12/24.34 thf(c_0_139, plain, (p193|~p39), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_131, c_0_132])])).
% 24.12/24.34 thf(c_0_140, plain, p39, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_133, c_0_134])])).
% 24.12/24.34 thf(c_0_141, plain, (p88|~p90), inference(fof_simplification,[status(thm)],[ax148])).
% 24.12/24.34 thf(c_0_142, plain, (p86|~p88), inference(split_conjunct,[status(thm)],[c_0_135])).
% 24.12/24.34 thf(c_0_143, plain, ~p86, inference(sr,[status(thm)],[c_0_136, c_0_137])).
% 24.12/24.34 thf(c_0_144, plain, (~p202|p201), inference(fof_simplification,[status(thm)],[ax28])).
% 24.12/24.34 thf(c_0_145, plain, (p202|~p193), inference(split_conjunct,[status(thm)],[c_0_138])).
% 24.12/24.34 thf(c_0_146, plain, p193, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_139, c_0_140])])).
% 24.12/24.34 thf(c_0_147, plain, (p90|~p92), inference(fof_simplification,[status(thm)],[ax146])).
% 24.12/24.34 thf(c_0_148, plain, (p88|~p90), inference(split_conjunct,[status(thm)],[c_0_141])).
% 24.12/24.34 thf(c_0_149, plain, ~p88, inference(sr,[status(thm)],[c_0_142, c_0_143])).
% 24.12/24.34 thf(c_0_150, plain, (~p201|p208), inference(fof_simplification,[status(thm)],[ax17])).
% 24.12/24.34 thf(c_0_151, plain, (p201|~p202), inference(split_conjunct,[status(thm)],[c_0_144])).
% 24.12/24.34 thf(c_0_152, plain, p202, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_145, c_0_146])])).
% 24.12/24.34 thf(c_0_153, plain, (p92|~p94), inference(fof_simplification,[status(thm)],[ax144])).
% 24.12/24.34 thf(c_0_154, plain, (p90|~p92), inference(split_conjunct,[status(thm)],[c_0_147])).
% 24.12/24.34 thf(c_0_155, plain, ~p90, inference(sr,[status(thm)],[c_0_148, c_0_149])).
% 24.12/24.34 thf(c_0_156, plain, (~p200|p212), inference(fof_simplification,[status(thm)],[ax22])).
% 24.12/24.34 thf(c_0_157, plain, (~p214|~p208|~p213), inference(fof_simplification,[status(thm)],[ax13])).
% 24.12/24.34 thf(c_0_158, plain, (p208|~p201), inference(split_conjunct,[status(thm)],[c_0_150])).
% 24.12/24.34 thf(c_0_159, plain, p201, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_151, c_0_152])])).
% 24.12/24.34 thf(c_0_160, plain, ((fin @ f__2 @ f__1|p213)&(((f__2)!=(f__0)|p213)&(~fin @ f__2 @ f__1|p213))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax213])])])).
% 24.12/24.34 thf(c_0_161, plain, (p94|~p95), inference(fof_simplification,[status(thm)],[ax143])).
% 24.12/24.34 thf(c_0_162, plain, (p92|~p94), inference(split_conjunct,[status(thm)],[c_0_153])).
% 24.12/24.34 thf(c_0_163, plain, ~p92, inference(sr,[status(thm)],[c_0_154, c_0_155])).
% 24.12/24.34 thf(c_0_164, plain, (~p212|p216), inference(fof_simplification,[status(thm)],[ax16])).
% 24.12/24.34 thf(c_0_165, plain, (p212|~p200), inference(split_conjunct,[status(thm)],[c_0_156])).
% 24.12/24.34 thf(c_0_166, plain, p200, inference(split_conjunct,[status(thm)],[ax35])).
% 24.12/24.34 thf(c_0_167, plain, (~p214|~p208|~p213), inference(split_conjunct,[status(thm)],[c_0_157])).
% 24.12/24.34 thf(c_0_168, plain, p208, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_158, c_0_159])])).
% 24.12/24.34 thf(c_0_169, plain, (fin @ f__2 @ f__1|p213), inference(split_conjunct,[status(thm)],[c_0_160])).
% 24.12/24.34 thf(c_0_170, plain, (p213|~fin @ f__2 @ f__1), inference(split_conjunct,[status(thm)],[c_0_160])).
% 24.12/24.34 thf(c_0_171, plain, (p95|~p96), inference(fof_simplification,[status(thm)],[ax142])).
% 24.12/24.34 thf(c_0_172, plain, (p94|~p95), inference(split_conjunct,[status(thm)],[c_0_161])).
% 24.12/24.34 thf(c_0_173, plain, ~p94, inference(sr,[status(thm)],[c_0_162, c_0_163])).
% 24.12/24.34 thf(c_0_174, plain, (~p216|p97|p215), inference(fof_simplification,[status(thm)],[ax15])).
% 24.12/24.34 thf(c_0_175, plain, (p216|~p212), inference(split_conjunct,[status(thm)],[c_0_164])).
% 24.12/24.34 thf(c_0_176, plain, p212, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_165, c_0_166])])).
% 24.12/24.34 thf(c_0_177, plain, (~p215|p214), inference(fof_simplification,[status(thm)],[ax14])).
% 24.12/24.34 thf(c_0_178, plain, (~p213|~p214), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_167, c_0_168])])).
% 24.12/24.34 thf(c_0_179, plain, p213, inference(csr,[status(thm)],[c_0_169, c_0_170])).
% 24.12/24.34 thf(c_0_180, plain, (p96|~p97), inference(fof_simplification,[status(thm)],[ax141])).
% 24.12/24.34 thf(c_0_181, plain, (p95|~p96), inference(split_conjunct,[status(thm)],[c_0_171])).
% 24.12/24.34 thf(c_0_182, plain, ~p95, inference(sr,[status(thm)],[c_0_172, c_0_173])).
% 24.12/24.34 thf(c_0_183, plain, (p97|p215|~p216), inference(split_conjunct,[status(thm)],[c_0_174])).
% 24.12/24.34 thf(c_0_184, plain, p216, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_175, c_0_176])])).
% 24.12/24.34 thf(c_0_185, plain, (p214|~p215), inference(split_conjunct,[status(thm)],[c_0_177])).
% 24.12/24.34 thf(c_0_186, plain, ~p214, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_178, c_0_179])])).
% 24.12/24.34 thf(c_0_187, plain, (p96|~p97), inference(split_conjunct,[status(thm)],[c_0_180])).
% 24.12/24.34 thf(c_0_188, plain, ~p96, inference(sr,[status(thm)],[c_0_181, c_0_182])).
% 24.12/24.34 thf(c_0_189, plain, (p215|p97), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_183, c_0_184])])).
% 24.12/24.34 thf(c_0_190, plain, ~p215, inference(sr,[status(thm)],[c_0_185, c_0_186])).
% 24.12/24.34 thf(c_0_191, plain, ~p97, inference(sr,[status(thm)],[c_0_187, c_0_188])).
% 24.12/24.34 thf(c_0_192, plain, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_189, c_0_190]), c_0_191]), ['proof']).
% 24.12/24.34 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 24.12/24.34 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 => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X2) => ((in @ X3) @ ((setadjoin @ X1) @ X2)))))))))))))))))))))))))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 24.12/24.34 % SZS output end Proof
%------------------------------------------------------------------------------