%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU545^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 : n018.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:33 PM UTC 2025
% Result : Theorem 23.92s 24.12s
% Output : Proof 23.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU545^1 : TPTP v9.2.0. Released v3.7.0.
% 0.07/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.33 % Computer : n018.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Oct 8 20:56:53 EDT 2025
% 0.12/0.34 % CPUTime :
% 23.92/24.12 % SZS status Theorem
% 23.92/24.12 % Mode: mode371
% 23.92/24.12 % Inferences: 134
% 23.92/24.12 % SZS output start Proof
% 23.92/24.12 thf(def_exu,definition,(exu = (^[X1:$i>$o]:(~((![X2:$i]:((X1 @ X2) => (~((![X3:$i]:((X1 @ X3) => (X2 = X3)))))))))))).
% 23.92/24.12 thf(def_setextAx,definition,(setextAx = (![X1:$i]:(![X2:$i]:((![X3:$i]:(((in @ X3) @ X1) = ((in @ X3) @ X2))) => (X1 = X2)))))).
% 23.92/24.12 thf(def_emptysetAx,definition,(emptysetAx = (![X1:$i]:(~(((in @ X1) @ emptyset)))))).
% 23.92/24.12 thf(def_setadjoinAx,definition,(setadjoinAx = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ X2)) = ((~((X3 = X1))) => ((in @ X3) @ X2)))))))).
% 23.92/24.12 thf(def_powersetAx,definition,(powersetAx = (![X1:$i]:(![X2:$i]:(((in @ X2) @ (powerset @ X1)) = (![X3:$i]:(((in @ X3) @ X2) => ((in @ X3) @ X1)))))))).
% 23.92/24.12 thf(def_setunionAx,definition,(setunionAx = (![X1:$i]:(![X2:$i]:(((in @ X2) @ (setunion @ X1)) = (~((![X3:$i]:(((in @ X2) @ X3) => (~(((in @ X3) @ X1)))))))))))).
% 23.92/24.12 thf(def_omega0Ax,definition,(omega0Ax = ((in @ emptyset) @ omega))).
% 23.92/24.12 thf(def_omegaSAx,definition,(omegaSAx = (![X1:$i]:(((in @ X1) @ omega) => ((in @ ((setadjoin @ X1) @ X1)) @ omega))))).
% 23.92/24.12 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))))))).
% 23.92/24.12 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))))))))))))))))))).
% 23.92/24.12 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))))))))))))))).
% 23.92/24.12 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)))))))))))))))))))))).
% 23.92/24.12 thf(def_descrp,definition,(descrp = (![X1:$i>$o]:((exu @ X1) => (X1 @ (descr @ X1)))))).
% 23.92/24.12 thf(def_dsetconstrI,definition,(dsetconstrI = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ X1) => ((X2 @ X3) => ((in @ X3) @ ((dsetconstr @ X1) @ X2))))))))).
% 23.92/24.12 thf(def_dsetconstrEL,definition,(dsetconstrEL = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ ((dsetconstr @ X1) @ X2)) => ((in @ X3) @ X1))))))).
% 23.92/24.12 thf(def_dsetconstrER,definition,(dsetconstrER = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ ((dsetconstr @ X1) @ X2)) => (X2 @ X3))))))).
% 23.92/24.12 thf(def_exuE1,definition,(exuE1 = (![X1:$i>$o]:((exu @ X1) => (~((![X2:$i]:((X1 @ X2) => (~((![X3:$i]:((X1 @ X3) => (X2 = X3))))))))))))).
% 23.92/24.12 thf(def_prop2setE,definition,(prop2setE = (![X1:$o]:(![X2:$i]:(((in @ X2) @ (prop2set @ X1)) => X1))))).
% 23.92/24.12 thf(def_emptysetE,definition,(emptysetE = (![X1:$i]:(((in @ X1) @ emptyset) => (![X2:$o]:X2))))).
% 23.92/24.12 thf(def_emptysetimpfalse,definition,(emptysetimpfalse = (![X1:$i]:(~(((in @ X1) @ emptyset)))))).
% 23.92/24.12 thf(def_notinemptyset,definition,(notinemptyset = (![X1:$i]:(~(((in @ X1) @ emptyset)))))).
% 23.92/24.12 thf(def_exuE3e,definition,(exuE3e = (![X1:$i>$o]:((exu @ X1) => (~((![X2:$i]:(~((X1 @ X2)))))))))).
% 23.92/24.12 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))))))).
% 23.92/24.12 thf(def_emptyI,definition,(emptyI = (![X1:$i]:((![X2:$i]:(~(((in @ X2) @ X1)))) => (X1 = emptyset))))).
% 23.92/24.12 thf(def_noeltsimpempty,definition,(noeltsimpempty = (![X1:$i]:((![X2:$i]:(~(((in @ X2) @ X1)))) => (X1 = emptyset))))).
% 23.92/24.12 thf(def_setbeta,definition,(setbeta = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ X1) => (((in @ X3) @ ((dsetconstr @ X1) @ X2)) = (X2 @ X3)))))))).
% 23.92/24.12 thf(def_nonempty,definition,(nonempty = (^[X1:$i]:(~((X1 = emptyset)))))).
% 23.92/24.12 thf(def_nonemptyE1,definition,(nonemptyE1 = (![X1:$i]:((nonempty @ X1) => (~((![X2:$i]:(~(((in @ X2) @ X1)))))))))).
% 23.92/24.12 thf(def_nonemptyI,definition,(nonemptyI = (![X1:$i]:(![X2:$i>$o]:(![X3:$i]:(((in @ X3) @ X1) => ((X2 @ X3) => (nonempty @ ((dsetconstr @ X1) @ X2))))))))).
% 23.92/24.12 thf(def_nonemptyI1,definition,(nonemptyI1 = (![X1:$i]:((~((![X2:$i]:(~(((in @ X2) @ X1)))))) => (nonempty @ X1))))).
% 23.92/24.12 thf(def_setadjoinIL,definition,(setadjoinIL = (![X1:$i]:(![X2:$i]:((in @ X1) @ ((setadjoin @ X1) @ X2)))))).
% 23.92/24.12 thf(def_emptyinunitempty,definition,(emptyinunitempty = ((in @ emptyset) @ ((setadjoin @ emptyset) @ emptyset)))).
% 23.92/24.12 thf(def_setadjoinIR,definition,(setadjoinIR = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X2) => ((in @ X3) @ ((setadjoin @ X1) @ X2)))))))).
% 23.92/24.12 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))))))))).
% 23.92/24.12 thf(def_setadjoinOr,definition,(setadjoinOr = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ X2)) => ((~((X3 = X1))) => ((in @ X3) @ X2)))))))).
% 23.92/24.12 thf(def_setoftrueEq,definition,(setoftrueEq = (![X1:$i]:(((dsetconstr @ X1) @ (^[X2:$i]:(~($false)))) = X1)))).
% 23.92/24.12 thf(def_powersetI,definition,(powersetI = (![X1:$i]:(![X2:$i]:((![X3:$i]:(((in @ X3) @ X2) => ((in @ X3) @ X1))) => ((in @ X2) @ (powerset @ X1))))))).
% 23.92/24.12 thf(def_emptyinPowerset,definition,(emptyinPowerset = (![X1:$i]:((in @ emptyset) @ (powerset @ X1))))).
% 23.92/24.12 thf(def_emptyInPowerset,definition,(emptyInPowerset = (![X1:$i]:((in @ emptyset) @ (powerset @ X1))))).
% 23.92/24.12 thf(def_powersetE,definition,(powersetE = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X2) @ (powerset @ X1)) => (((in @ X3) @ X2) => ((in @ X3) @ X1)))))))).
% 23.92/24.12 thf(def_setunionI,definition,(setunionI = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X2) @ X3) => (((in @ X3) @ X1) => ((in @ X2) @ (setunion @ X1))))))))).
% 23.92/24.12 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))))))).
% 23.92/24.12 thf(def_subPowSU,definition,(subPowSU = (![X1:$i]:(![X2:$i]:(((in @ X2) @ X1) => ((in @ X2) @ (powerset @ (setunion @ X1)))))))).
% 23.92/24.12 thf(def_exuE2,definition,(exuE2 = (![X1:$i>$o]:((exu @ X1) => (~((![X2:$i]:(~((![X3:$i]:((X1 @ X3) = (X3 = X2)))))))))))).
% 23.92/24.12 thf(def_nonemptyImpWitness,definition,(nonemptyImpWitness = (![X1:$i]:((nonempty @ X1) => (~((![X2:$i]:(~(((in @ X2) @ X1)))))))))).
% 23.92/24.12 thf(def_uniqinunit,definition,(uniqinunit = (![X1:$i]:(![X2:$i]:(((in @ X1) @ ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))))).
% 23.92/24.12 thf(def_notinsingleton,definition,(notinsingleton = (![X1:$i]:(![X2:$i]:((~((X1 = X2))) => (~(((in @ X2) @ ((setadjoin @ X1) @ emptyset))))))))).
% 23.92/24.12 thf(def_eqinunit,definition,(eqinunit = (![X1:$i]:(![X2:$i]:((X1 = X2) => ((in @ X1) @ ((setadjoin @ X2) @ emptyset))))))).
% 23.92/24.12 thf(def_singletonsswitch,definition,(singletonsswitch = (![X1:$i]:(![X2:$i]:(((in @ X1) @ ((setadjoin @ X2) @ emptyset)) => ((in @ X2) @ ((setadjoin @ X1) @ emptyset))))))).
% 23.92/24.12 thf(def_upairsetE,definition,(upairsetE = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) => ((~((X3 = X1))) => (X3 = X2)))))))).
% 23.92/24.12 thf(def_upairsetIL,definition,(upairsetIL = (![X1:$i]:(![X2:$i]:((in @ X1) @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))))))).
% 23.92/24.12 thf(def_upairsetIR,definition,(upairsetIR = (![X1:$i]:(![X2:$i]:((in @ X2) @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))))))).
% 23.92/24.12 thf(def_emptyE1,definition,(emptyE1 = (![X1:$i]:(![X2:$i>$o]:((~((![X3:$i]:(((in @ X3) @ X1) => (~((X2 @ X3))))))) => (~((((dsetconstr @ X1) @ X2) = emptyset)))))))).
% 23.92/24.12 thf(def_vacuousDall,definition,(vacuousDall = (![X1:$i>$o]:(![X2:$i]:(((in @ X2) @ emptyset) => (X1 @ X2)))))).
% 23.92/24.12 thf(def_quantDeMorgan1,definition,(quantDeMorgan1 = (![X1:$i]:(![X2:$i>$o]:((~((![X3:$i]:(((in @ X3) @ X1) => (X2 @ X3))))) => (~((![X3:$i]:(((in @ X3) @ X1) => (X2 @ X3)))))))))).
% 23.92/24.12 thf(def_quantDeMorgan2,definition,(quantDeMorgan2 = (![X1:$i]:(![X2:$i>$o]:((![X3:$i]:(((in @ X3) @ X1) => (~((X2 @ X3))))) => (![X3:$i]:(((in @ X3) @ X1) => (~((X2 @ X3)))))))))).
% 23.92/24.12 thf(def_quantDeMorgan3,definition,(quantDeMorgan3 = (![X1:$i]:(![X2:$i>$o]:((![X3:$i]:(((in @ X3) @ X1) => (~((X2 @ X3))))) => (![X3:$i]:(((in @ X3) @ X1) => (~((X2 @ X3)))))))))).
% 23.92/24.12 thf(def_quantDeMorgan4,definition,(quantDeMorgan4 = (![X1:$i]:(![X2:$i>$o]:((~((![X3:$i]:(((in @ X3) @ X1) => (X2 @ X3))))) => (~((![X3:$i]:(((in @ X3) @ X1) => (X2 @ X3)))))))))).
% 23.92/24.12 thf(def_prop2setI,definition,(prop2setI = (![X1:$o]:(X1 => ((in @ emptyset) @ (prop2set @ X1)))))).
% 23.92/24.12 thf(def_prop2set2propI,definition,(prop2set2propI = (![X1:$o]:(X1 => (set2prop @ (prop2set @ X1)))))).
% 23.92/24.12 thf(def_notdexE,definition,(notdexE = (![X1:$i]:(![X2:$i>$o]:((![X3:$i]:(((in @ X3) @ X1) => (~((X2 @ X3))))) => (![X3:$i]:(((in @ X3) @ X1) => (~((X2 @ X3)))))))))).
% 23.92/24.12 thf(def_notdallE,definition,(notdallE = (![X1:$i]:(![X2:$i>$o]:((~((![X3:$i]:(((in @ X3) @ X1) => (X2 @ X3))))) => (~((![X3:$i]:(((in @ X3) @ X1) => (X2 @ X3)))))))))).
% 23.92/24.12 thf(def_exuI1,definition,(exuI1 = (![X1:$i>$o]:((~((![X2:$i]:((X1 @ X2) => (~((![X3:$i]:((X1 @ X3) => (X2 = X3))))))))) => (exu @ X1))))).
% 23.92/24.12 thf(exuI3,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 => (setadjoinE => (setadjoinOr => (setoftrueEq => (powersetI => (emptyinPowerset => (emptyInPowerset => (powersetE => (setunionI => (setunionE => (subPowSU => (exuE2 => (nonemptyImpWitness => (uniqinunit => (notinsingleton => (eqinunit => (singletonsswitch => (upairsetE => (upairsetIL => (upairsetIR => (emptyE1 => (vacuousDall => (quantDeMorgan1 => (quantDeMorgan2 => (quantDeMorgan3 => (quantDeMorgan4 => (prop2setI => (prop2set2propI => (notdexE => (notdallE => (exuI1 => (![X1:$i>$o]:((~((![X2:$i]:(~((X1 @ X2)))))) => ((![X2:$i]:(![X3:$i]:((X1 @ X2) => ((X1 @ X3) => (X2 = X3))))) => (exu @ X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 23.92/24.12 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 => (setadjoinE => (setadjoinOr => (setoftrueEq => (powersetI => (emptyinPowerset => (emptyInPowerset => (powersetE => (setunionI => (setunionE => (subPowSU => (exuE2 => (nonemptyImpWitness => (uniqinunit => (notinsingleton => (eqinunit => (singletonsswitch => (upairsetE => (upairsetIL => (upairsetIR => (emptyE1 => (vacuousDall => (quantDeMorgan1 => (quantDeMorgan2 => (quantDeMorgan3 => (quantDeMorgan4 => (prop2setI => (prop2set2propI => (notdexE => (notdallE => (exuI1 => (![X1:$i>$o]:((~((![X2:$i]:(~((X1 @ X2)))))) => ((![X2:$i]:(![X3:$i]:((X1 @ X2) => ((X1 @ X3) => (X2 = X3))))) => (exu @ X1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),inference(assume_negation,[status(cth)],[exuI3])).
% 23.92/24.12 thf(ax212, axiom, (p1|~(p66)), file('<stdin>', ax212)).
% 23.92/24.12 thf(ax277, axiom, ~(p1), file('<stdin>', ax277)).
% 23.92/24.12 thf(ax210, axiom, (p66|~(p68)), file('<stdin>', ax210)).
% 23.92/24.12 thf(ax208, axiom, (p68|~(p70)), file('<stdin>', ax208)).
% 23.92/24.12 thf(ax206, axiom, (p70|~(p72)), file('<stdin>', ax206)).
% 23.92/24.12 thf(ax204, axiom, (p72|~(p74)), file('<stdin>', ax204)).
% 23.92/24.12 thf(ax202, axiom, (p74|~(p76)), file('<stdin>', ax202)).
% 23.92/24.12 thf(ax200, axiom, (p76|~(p78)), file('<stdin>', ax200)).
% 23.92/24.12 thf(ax198, axiom, (p78|~(p80)), file('<stdin>', ax198)).
% 23.92/24.12 thf(ax196, axiom, (p80|~(p82)), file('<stdin>', ax196)).
% 23.92/24.12 thf(ax194, axiom, (p82|~(p84)), file('<stdin>', ax194)).
% 23.92/24.12 thf(ax192, axiom, (p84|~(p86)), file('<stdin>', ax192)).
% 23.92/24.12 thf(ax190, axiom, (p86|~(p88)), file('<stdin>', ax190)).
% 23.92/24.12 thf(ax188, axiom, (p88|~(p90)), file('<stdin>', ax188)).
% 23.92/24.12 thf(ax186, axiom, (p90|~(p92)), file('<stdin>', ax186)).
% 23.92/24.12 thf(ax184, axiom, (p92|~(p94)), file('<stdin>', ax184)).
% 23.92/24.12 thf(ax182, axiom, (p94|~(p96)), file('<stdin>', ax182)).
% 23.92/24.12 thf(ax180, axiom, (p96|~(p98)), file('<stdin>', ax180)).
% 23.92/24.12 thf(ax178, axiom, (p98|~(p100)), file('<stdin>', ax178)).
% 23.92/24.12 thf(ax176, axiom, (p100|~(p102)), file('<stdin>', ax176)).
% 23.92/24.12 thf(ax174, axiom, (p102|~(p104)), file('<stdin>', ax174)).
% 23.92/24.12 thf(ax172, axiom, (p104|~(p106)), file('<stdin>', ax172)).
% 23.92/24.12 thf(ax170, axiom, (p106|~(p108)), file('<stdin>', ax170)).
% 23.92/24.12 thf(ax168, axiom, (p108|~(p110)), file('<stdin>', ax168)).
% 23.92/24.12 thf(ax166, axiom, (p110|~(p112)), file('<stdin>', ax166)).
% 23.92/24.12 thf(ax164, axiom, (p112|~(p114)), file('<stdin>', ax164)).
% 23.92/24.12 thf(ax162, axiom, (p114|~(p116)), file('<stdin>', ax162)).
% 23.92/24.12 thf(ax160, axiom, (p116|~(p118)), file('<stdin>', ax160)).
% 23.92/24.12 thf(ax158, axiom, (p118|~(p120)), file('<stdin>', ax158)).
% 23.92/24.12 thf(ax156, axiom, (p120|~(p122)), file('<stdin>', ax156)).
% 23.92/24.12 thf(ax154, axiom, (p122|~(p124)), file('<stdin>', ax154)).
% 23.92/24.12 thf(ax152, axiom, (p124|~(p126)), file('<stdin>', ax152)).
% 23.92/24.12 thf(ax150, axiom, (p126|~(p128)), file('<stdin>', ax150)).
% 23.92/24.12 thf(ax148, axiom, (p128|~(p130)), file('<stdin>', ax148)).
% 23.92/24.12 thf(ax146, axiom, (p130|~(p132)), file('<stdin>', ax146)).
% 23.92/24.12 thf(ax144, axiom, (p132|~(p134)), file('<stdin>', ax144)).
% 23.92/24.12 thf(ax142, axiom, (p134|~(p136)), file('<stdin>', ax142)).
% 23.92/24.12 thf(ax140, axiom, (p136|~(p138)), file('<stdin>', ax140)).
% 23.92/24.12 thf(ax138, axiom, (p138|~(p140)), file('<stdin>', ax138)).
% 23.92/24.12 thf(ax136, axiom, (p140|~(p142)), file('<stdin>', ax136)).
% 23.92/24.12 thf(ax134, axiom, (p142|~(p144)), file('<stdin>', ax134)).
% 23.92/24.12 thf(ax132, axiom, (p144|~(p146)), file('<stdin>', ax132)).
% 23.92/24.12 thf(ax130, axiom, (p146|~(p148)), file('<stdin>', ax130)).
% 23.92/24.12 thf(ax128, axiom, (p148|~(p150)), file('<stdin>', ax128)).
% 23.92/24.12 thf(ax126, axiom, (p150|~(p152)), file('<stdin>', ax126)).
% 23.92/24.12 thf(ax124, axiom, (p152|~(p154)), file('<stdin>', ax124)).
% 23.92/24.12 thf(ax122, axiom, (p154|~(p156)), file('<stdin>', ax122)).
% 23.92/24.12 thf(ax120, axiom, (p156|~(p158)), file('<stdin>', ax120)).
% 23.92/24.12 thf(ax118, axiom, (p158|~(p160)), file('<stdin>', ax118)).
% 23.92/24.12 thf(ax116, axiom, (p160|~(p162)), file('<stdin>', ax116)).
% 23.92/24.12 thf(ax114, axiom, (p162|~(p164)), file('<stdin>', ax114)).
% 23.92/24.12 thf(ax112, axiom, (p164|~(p166)), file('<stdin>', ax112)).
% 23.92/24.12 thf(ax110, axiom, (p166|~(p168)), file('<stdin>', ax110)).
% 23.92/24.12 thf(ax108, axiom, (p168|~(p170)), file('<stdin>', ax108)).
% 23.92/24.12 thf(ax106, axiom, (p170|~(p172)), file('<stdin>', ax106)).
% 23.92/24.12 thf(ax104, axiom, (p172|~(p174)), file('<stdin>', ax104)).
% 23.92/24.12 thf(ax102, axiom, (p174|~(p176)), file('<stdin>', ax102)).
% 23.92/24.12 thf(ax100, axiom, (p176|~(p178)), file('<stdin>', ax100)).
% 23.92/24.12 thf(ax98, axiom, (p178|~(p180)), file('<stdin>', ax98)).
% 23.92/24.12 thf(ax96, axiom, (p180|~(p182)), file('<stdin>', ax96)).
% 23.92/24.12 thf(ax94, axiom, (p182|~(p184)), file('<stdin>', ax94)).
% 23.92/24.12 thf(ax92, axiom, (p184|~(p186)), file('<stdin>', ax92)).
% 23.92/24.12 thf(ax75, axiom, (~(p207)|p206), file('<stdin>', ax75)).
% 23.92/24.12 thf(ax91, axiom, (p186|~(p187)), file('<stdin>', ax91)).
% 23.92/24.12 thf(ax77, axiom, (~(p2)|p200), file('<stdin>', ax77)).
% 23.92/24.12 thf(ax69, axiom, (~(p206)|p211), file('<stdin>', ax69)).
% 23.92/24.12 thf(ax76, axiom, p207, file('<stdin>', ax76)).
% 23.92/24.12 thf(ax89, axiom, (p187|~(p189)), file('<stdin>', ax89)).
% 23.92/24.12 thf(ax90, axiom, (p187|~(p188)), file('<stdin>', ax90)).
% 23.92/24.12 thf(ax70, axiom, (~(p200)|p202), file('<stdin>', ax70)).
% 23.92/24.12 thf(ax276, axiom, p2, file('<stdin>', ax276)).
% 23.92/24.12 thf(ax68, axiom, (~(p211)|p189|p210), file('<stdin>', ax68)).
% 23.92/24.12 thf(ax66, axiom, (~(p209)|~(p202)|~(p208)), file('<stdin>', ax66)).
% 23.92/24.12 thf(ax67, axiom, (~(p210)|p209), file('<stdin>', ax67)).
% 23.92/24.12 thf(ax85, axiom, (~(p191)|p193), file('<stdin>', ax85)).
% 23.92/24.12 thf(ax87, axiom, (p189|p191), file('<stdin>', ax87)).
% 23.92/24.12 thf(pax190, axiom, (p190=>f__0 @ f__1), file('<stdin>', pax190)).
% 23.92/24.12 thf(ax88, axiom, (p188|p190), file('<stdin>', ax88)).
% 23.92/24.12 thf(pax193, axiom, (p193=>![X1:$i]:(f__0 @ f__1=>(f__0 @ X1=>(f__1)=(X1)))), file('<stdin>', pax193)).
% 23.92/24.12 thf(nax208, axiom, (p208<=(![X1:$i, X2:$i]:(f__0 @ X1=>(f__0 @ X2=>(X1)=(X2)))=>~(![X1:$i]:(f__0 @ X1=>~(![X2:$i]:(f__0 @ X2=>(X1)=(X2))))))), file('<stdin>', nax208)).
% 23.92/24.12 thf(c_0_80, plain, (p1|~p66), inference(fof_simplification,[status(thm)],[ax212])).
% 23.92/24.12 thf(c_0_81, plain, ~p1, inference(fof_simplification,[status(thm)],[ax277])).
% 23.92/24.12 thf(c_0_82, plain, (p66|~p68), inference(fof_simplification,[status(thm)],[ax210])).
% 23.92/24.12 thf(c_0_83, plain, (p1|~p66), inference(split_conjunct,[status(thm)],[c_0_80])).
% 23.92/24.12 thf(c_0_84, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_81])).
% 23.92/24.12 thf(c_0_85, plain, (p68|~p70), inference(fof_simplification,[status(thm)],[ax208])).
% 23.92/24.12 thf(c_0_86, plain, (p66|~p68), inference(split_conjunct,[status(thm)],[c_0_82])).
% 23.92/24.12 thf(c_0_87, plain, ~p66, inference(sr,[status(thm)],[c_0_83, c_0_84])).
% 23.92/24.12 thf(c_0_88, plain, (p70|~p72), inference(fof_simplification,[status(thm)],[ax206])).
% 23.92/24.12 thf(c_0_89, plain, (p68|~p70), inference(split_conjunct,[status(thm)],[c_0_85])).
% 23.92/24.12 thf(c_0_90, plain, ~p68, inference(sr,[status(thm)],[c_0_86, c_0_87])).
% 23.92/24.12 thf(c_0_91, plain, (p72|~p74), inference(fof_simplification,[status(thm)],[ax204])).
% 23.92/24.12 thf(c_0_92, plain, (p70|~p72), inference(split_conjunct,[status(thm)],[c_0_88])).
% 23.92/24.12 thf(c_0_93, plain, ~p70, inference(sr,[status(thm)],[c_0_89, c_0_90])).
% 23.92/24.12 thf(c_0_94, plain, (p74|~p76), inference(fof_simplification,[status(thm)],[ax202])).
% 23.92/24.12 thf(c_0_95, plain, (p72|~p74), inference(split_conjunct,[status(thm)],[c_0_91])).
% 23.92/24.12 thf(c_0_96, plain, ~p72, inference(sr,[status(thm)],[c_0_92, c_0_93])).
% 23.92/24.12 thf(c_0_97, plain, (p76|~p78), inference(fof_simplification,[status(thm)],[ax200])).
% 23.92/24.12 thf(c_0_98, plain, (p74|~p76), inference(split_conjunct,[status(thm)],[c_0_94])).
% 23.92/24.12 thf(c_0_99, plain, ~p74, inference(sr,[status(thm)],[c_0_95, c_0_96])).
% 23.92/24.12 thf(c_0_100, plain, (p78|~p80), inference(fof_simplification,[status(thm)],[ax198])).
% 23.92/24.12 thf(c_0_101, plain, (p76|~p78), inference(split_conjunct,[status(thm)],[c_0_97])).
% 23.92/24.12 thf(c_0_102, plain, ~p76, inference(sr,[status(thm)],[c_0_98, c_0_99])).
% 23.92/24.12 thf(c_0_103, plain, (p80|~p82), inference(fof_simplification,[status(thm)],[ax196])).
% 23.92/24.12 thf(c_0_104, plain, (p78|~p80), inference(split_conjunct,[status(thm)],[c_0_100])).
% 23.92/24.12 thf(c_0_105, plain, ~p78, inference(sr,[status(thm)],[c_0_101, c_0_102])).
% 23.92/24.12 thf(c_0_106, plain, (p82|~p84), inference(fof_simplification,[status(thm)],[ax194])).
% 23.92/24.12 thf(c_0_107, plain, (p80|~p82), inference(split_conjunct,[status(thm)],[c_0_103])).
% 23.92/24.12 thf(c_0_108, plain, ~p80, inference(sr,[status(thm)],[c_0_104, c_0_105])).
% 23.92/24.12 thf(c_0_109, plain, (p84|~p86), inference(fof_simplification,[status(thm)],[ax192])).
% 23.92/24.12 thf(c_0_110, plain, (p82|~p84), inference(split_conjunct,[status(thm)],[c_0_106])).
% 23.92/24.12 thf(c_0_111, plain, ~p82, inference(sr,[status(thm)],[c_0_107, c_0_108])).
% 23.92/24.12 thf(c_0_112, plain, (p86|~p88), inference(fof_simplification,[status(thm)],[ax190])).
% 23.92/24.12 thf(c_0_113, plain, (p84|~p86), inference(split_conjunct,[status(thm)],[c_0_109])).
% 23.92/24.12 thf(c_0_114, plain, ~p84, inference(sr,[status(thm)],[c_0_110, c_0_111])).
% 23.92/24.12 thf(c_0_115, plain, (p88|~p90), inference(fof_simplification,[status(thm)],[ax188])).
% 23.92/24.12 thf(c_0_116, plain, (p86|~p88), inference(split_conjunct,[status(thm)],[c_0_112])).
% 23.92/24.12 thf(c_0_117, plain, ~p86, inference(sr,[status(thm)],[c_0_113, c_0_114])).
% 23.92/24.12 thf(c_0_118, plain, (p90|~p92), inference(fof_simplification,[status(thm)],[ax186])).
% 23.92/24.12 thf(c_0_119, plain, (p88|~p90), inference(split_conjunct,[status(thm)],[c_0_115])).
% 23.92/24.12 thf(c_0_120, plain, ~p88, inference(sr,[status(thm)],[c_0_116, c_0_117])).
% 23.92/24.12 thf(c_0_121, plain, (p92|~p94), inference(fof_simplification,[status(thm)],[ax184])).
% 23.92/24.12 thf(c_0_122, plain, (p90|~p92), inference(split_conjunct,[status(thm)],[c_0_118])).
% 23.92/24.12 thf(c_0_123, plain, ~p90, inference(sr,[status(thm)],[c_0_119, c_0_120])).
% 23.92/24.12 thf(c_0_124, plain, (p94|~p96), inference(fof_simplification,[status(thm)],[ax182])).
% 23.92/24.12 thf(c_0_125, plain, (p92|~p94), inference(split_conjunct,[status(thm)],[c_0_121])).
% 23.92/24.12 thf(c_0_126, plain, ~p92, inference(sr,[status(thm)],[c_0_122, c_0_123])).
% 23.92/24.12 thf(c_0_127, plain, (p96|~p98), inference(fof_simplification,[status(thm)],[ax180])).
% 23.92/24.12 thf(c_0_128, plain, (p94|~p96), inference(split_conjunct,[status(thm)],[c_0_124])).
% 23.92/24.12 thf(c_0_129, plain, ~p94, inference(sr,[status(thm)],[c_0_125, c_0_126])).
% 23.92/24.12 thf(c_0_130, plain, (p98|~p100), inference(fof_simplification,[status(thm)],[ax178])).
% 23.92/24.12 thf(c_0_131, plain, (p96|~p98), inference(split_conjunct,[status(thm)],[c_0_127])).
% 23.92/24.12 thf(c_0_132, plain, ~p96, inference(sr,[status(thm)],[c_0_128, c_0_129])).
% 23.92/24.12 thf(c_0_133, plain, (p100|~p102), inference(fof_simplification,[status(thm)],[ax176])).
% 23.92/24.12 thf(c_0_134, plain, (p98|~p100), inference(split_conjunct,[status(thm)],[c_0_130])).
% 23.92/24.12 thf(c_0_135, plain, ~p98, inference(sr,[status(thm)],[c_0_131, c_0_132])).
% 23.92/24.12 thf(c_0_136, plain, (p102|~p104), inference(fof_simplification,[status(thm)],[ax174])).
% 23.92/24.12 thf(c_0_137, plain, (p100|~p102), inference(split_conjunct,[status(thm)],[c_0_133])).
% 23.92/24.12 thf(c_0_138, plain, ~p100, inference(sr,[status(thm)],[c_0_134, c_0_135])).
% 23.92/24.12 thf(c_0_139, plain, (p104|~p106), inference(fof_simplification,[status(thm)],[ax172])).
% 23.92/24.12 thf(c_0_140, plain, (p102|~p104), inference(split_conjunct,[status(thm)],[c_0_136])).
% 23.92/24.12 thf(c_0_141, plain, ~p102, inference(sr,[status(thm)],[c_0_137, c_0_138])).
% 23.92/24.12 thf(c_0_142, plain, (p106|~p108), inference(fof_simplification,[status(thm)],[ax170])).
% 23.92/24.12 thf(c_0_143, plain, (p104|~p106), inference(split_conjunct,[status(thm)],[c_0_139])).
% 23.92/24.12 thf(c_0_144, plain, ~p104, inference(sr,[status(thm)],[c_0_140, c_0_141])).
% 23.92/24.12 thf(c_0_145, plain, (p108|~p110), inference(fof_simplification,[status(thm)],[ax168])).
% 23.92/24.12 thf(c_0_146, plain, (p106|~p108), inference(split_conjunct,[status(thm)],[c_0_142])).
% 23.92/24.12 thf(c_0_147, plain, ~p106, inference(sr,[status(thm)],[c_0_143, c_0_144])).
% 23.92/24.12 thf(c_0_148, plain, (p110|~p112), inference(fof_simplification,[status(thm)],[ax166])).
% 23.92/24.12 thf(c_0_149, plain, (p108|~p110), inference(split_conjunct,[status(thm)],[c_0_145])).
% 23.92/24.12 thf(c_0_150, plain, ~p108, inference(sr,[status(thm)],[c_0_146, c_0_147])).
% 23.92/24.12 thf(c_0_151, plain, (p112|~p114), inference(fof_simplification,[status(thm)],[ax164])).
% 23.92/24.12 thf(c_0_152, plain, (p110|~p112), inference(split_conjunct,[status(thm)],[c_0_148])).
% 23.92/24.12 thf(c_0_153, plain, ~p110, inference(sr,[status(thm)],[c_0_149, c_0_150])).
% 23.92/24.12 thf(c_0_154, plain, (p114|~p116), inference(fof_simplification,[status(thm)],[ax162])).
% 23.92/24.12 thf(c_0_155, plain, (p112|~p114), inference(split_conjunct,[status(thm)],[c_0_151])).
% 23.92/24.12 thf(c_0_156, plain, ~p112, inference(sr,[status(thm)],[c_0_152, c_0_153])).
% 23.92/24.12 thf(c_0_157, plain, (p116|~p118), inference(fof_simplification,[status(thm)],[ax160])).
% 23.92/24.12 thf(c_0_158, plain, (p114|~p116), inference(split_conjunct,[status(thm)],[c_0_154])).
% 23.92/24.12 thf(c_0_159, plain, ~p114, inference(sr,[status(thm)],[c_0_155, c_0_156])).
% 23.92/24.12 thf(c_0_160, plain, (p118|~p120), inference(fof_simplification,[status(thm)],[ax158])).
% 23.92/24.12 thf(c_0_161, plain, (p116|~p118), inference(split_conjunct,[status(thm)],[c_0_157])).
% 23.92/24.12 thf(c_0_162, plain, ~p116, inference(sr,[status(thm)],[c_0_158, c_0_159])).
% 23.92/24.12 thf(c_0_163, plain, (p120|~p122), inference(fof_simplification,[status(thm)],[ax156])).
% 23.92/24.12 thf(c_0_164, plain, (p118|~p120), inference(split_conjunct,[status(thm)],[c_0_160])).
% 23.92/24.12 thf(c_0_165, plain, ~p118, inference(sr,[status(thm)],[c_0_161, c_0_162])).
% 23.92/24.12 thf(c_0_166, plain, (p122|~p124), inference(fof_simplification,[status(thm)],[ax154])).
% 23.92/24.12 thf(c_0_167, plain, (p120|~p122), inference(split_conjunct,[status(thm)],[c_0_163])).
% 23.92/24.12 thf(c_0_168, plain, ~p120, inference(sr,[status(thm)],[c_0_164, c_0_165])).
% 23.92/24.12 thf(c_0_169, plain, (p124|~p126), inference(fof_simplification,[status(thm)],[ax152])).
% 23.92/24.12 thf(c_0_170, plain, (p122|~p124), inference(split_conjunct,[status(thm)],[c_0_166])).
% 23.92/24.12 thf(c_0_171, plain, ~p122, inference(sr,[status(thm)],[c_0_167, c_0_168])).
% 23.92/24.12 thf(c_0_172, plain, (p126|~p128), inference(fof_simplification,[status(thm)],[ax150])).
% 23.92/24.12 thf(c_0_173, plain, (p124|~p126), inference(split_conjunct,[status(thm)],[c_0_169])).
% 23.92/24.12 thf(c_0_174, plain, ~p124, inference(sr,[status(thm)],[c_0_170, c_0_171])).
% 23.92/24.12 thf(c_0_175, plain, (p128|~p130), inference(fof_simplification,[status(thm)],[ax148])).
% 23.92/24.12 thf(c_0_176, plain, (p126|~p128), inference(split_conjunct,[status(thm)],[c_0_172])).
% 23.92/24.12 thf(c_0_177, plain, ~p126, inference(sr,[status(thm)],[c_0_173, c_0_174])).
% 23.92/24.12 thf(c_0_178, plain, (p130|~p132), inference(fof_simplification,[status(thm)],[ax146])).
% 23.92/24.12 thf(c_0_179, plain, (p128|~p130), inference(split_conjunct,[status(thm)],[c_0_175])).
% 23.92/24.12 thf(c_0_180, plain, ~p128, inference(sr,[status(thm)],[c_0_176, c_0_177])).
% 23.92/24.12 thf(c_0_181, plain, (p132|~p134), inference(fof_simplification,[status(thm)],[ax144])).
% 23.92/24.12 thf(c_0_182, plain, (p130|~p132), inference(split_conjunct,[status(thm)],[c_0_178])).
% 23.92/24.12 thf(c_0_183, plain, ~p130, inference(sr,[status(thm)],[c_0_179, c_0_180])).
% 23.92/24.12 thf(c_0_184, plain, (p134|~p136), inference(fof_simplification,[status(thm)],[ax142])).
% 23.92/24.12 thf(c_0_185, plain, (p132|~p134), inference(split_conjunct,[status(thm)],[c_0_181])).
% 23.92/24.12 thf(c_0_186, plain, ~p132, inference(sr,[status(thm)],[c_0_182, c_0_183])).
% 23.92/24.12 thf(c_0_187, plain, (p136|~p138), inference(fof_simplification,[status(thm)],[ax140])).
% 23.92/24.12 thf(c_0_188, plain, (p134|~p136), inference(split_conjunct,[status(thm)],[c_0_184])).
% 23.92/24.12 thf(c_0_189, plain, ~p134, inference(sr,[status(thm)],[c_0_185, c_0_186])).
% 23.92/24.12 thf(c_0_190, plain, (p138|~p140), inference(fof_simplification,[status(thm)],[ax138])).
% 23.92/24.12 thf(c_0_191, plain, (p136|~p138), inference(split_conjunct,[status(thm)],[c_0_187])).
% 23.92/24.12 thf(c_0_192, plain, ~p136, inference(sr,[status(thm)],[c_0_188, c_0_189])).
% 23.92/24.12 thf(c_0_193, plain, (p140|~p142), inference(fof_simplification,[status(thm)],[ax136])).
% 23.92/24.12 thf(c_0_194, plain, (p138|~p140), inference(split_conjunct,[status(thm)],[c_0_190])).
% 23.92/24.12 thf(c_0_195, plain, ~p138, inference(sr,[status(thm)],[c_0_191, c_0_192])).
% 23.92/24.12 thf(c_0_196, plain, (p142|~p144), inference(fof_simplification,[status(thm)],[ax134])).
% 23.92/24.12 thf(c_0_197, plain, (p140|~p142), inference(split_conjunct,[status(thm)],[c_0_193])).
% 23.92/24.12 thf(c_0_198, plain, ~p140, inference(sr,[status(thm)],[c_0_194, c_0_195])).
% 23.92/24.12 thf(c_0_199, plain, (p144|~p146), inference(fof_simplification,[status(thm)],[ax132])).
% 23.92/24.12 thf(c_0_200, plain, (p142|~p144), inference(split_conjunct,[status(thm)],[c_0_196])).
% 23.92/24.12 thf(c_0_201, plain, ~p142, inference(sr,[status(thm)],[c_0_197, c_0_198])).
% 23.92/24.12 thf(c_0_202, plain, (p146|~p148), inference(fof_simplification,[status(thm)],[ax130])).
% 23.92/24.12 thf(c_0_203, plain, (p144|~p146), inference(split_conjunct,[status(thm)],[c_0_199])).
% 23.92/24.12 thf(c_0_204, plain, ~p144, inference(sr,[status(thm)],[c_0_200, c_0_201])).
% 23.92/24.12 thf(c_0_205, plain, (p148|~p150), inference(fof_simplification,[status(thm)],[ax128])).
% 23.92/24.12 thf(c_0_206, plain, (p146|~p148), inference(split_conjunct,[status(thm)],[c_0_202])).
% 23.92/24.12 thf(c_0_207, plain, ~p146, inference(sr,[status(thm)],[c_0_203, c_0_204])).
% 23.92/24.12 thf(c_0_208, plain, (p150|~p152), inference(fof_simplification,[status(thm)],[ax126])).
% 23.92/24.12 thf(c_0_209, plain, (p148|~p150), inference(split_conjunct,[status(thm)],[c_0_205])).
% 23.92/24.12 thf(c_0_210, plain, ~p148, inference(sr,[status(thm)],[c_0_206, c_0_207])).
% 23.92/24.12 thf(c_0_211, plain, (p152|~p154), inference(fof_simplification,[status(thm)],[ax124])).
% 23.92/24.12 thf(c_0_212, plain, (p150|~p152), inference(split_conjunct,[status(thm)],[c_0_208])).
% 23.92/24.12 thf(c_0_213, plain, ~p150, inference(sr,[status(thm)],[c_0_209, c_0_210])).
% 23.92/24.12 thf(c_0_214, plain, (p154|~p156), inference(fof_simplification,[status(thm)],[ax122])).
% 23.92/24.12 thf(c_0_215, plain, (p152|~p154), inference(split_conjunct,[status(thm)],[c_0_211])).
% 23.92/24.12 thf(c_0_216, plain, ~p152, inference(sr,[status(thm)],[c_0_212, c_0_213])).
% 23.92/24.12 thf(c_0_217, plain, (p156|~p158), inference(fof_simplification,[status(thm)],[ax120])).
% 23.92/24.12 thf(c_0_218, plain, (p154|~p156), inference(split_conjunct,[status(thm)],[c_0_214])).
% 23.92/24.12 thf(c_0_219, plain, ~p154, inference(sr,[status(thm)],[c_0_215, c_0_216])).
% 23.92/24.12 thf(c_0_220, plain, (p158|~p160), inference(fof_simplification,[status(thm)],[ax118])).
% 23.92/24.12 thf(c_0_221, plain, (p156|~p158), inference(split_conjunct,[status(thm)],[c_0_217])).
% 23.92/24.12 thf(c_0_222, plain, ~p156, inference(sr,[status(thm)],[c_0_218, c_0_219])).
% 23.92/24.12 thf(c_0_223, plain, (p160|~p162), inference(fof_simplification,[status(thm)],[ax116])).
% 23.92/24.12 thf(c_0_224, plain, (p158|~p160), inference(split_conjunct,[status(thm)],[c_0_220])).
% 23.92/24.12 thf(c_0_225, plain, ~p158, inference(sr,[status(thm)],[c_0_221, c_0_222])).
% 23.92/24.12 thf(c_0_226, plain, (p162|~p164), inference(fof_simplification,[status(thm)],[ax114])).
% 23.92/24.12 thf(c_0_227, plain, (p160|~p162), inference(split_conjunct,[status(thm)],[c_0_223])).
% 23.92/24.12 thf(c_0_228, plain, ~p160, inference(sr,[status(thm)],[c_0_224, c_0_225])).
% 23.92/24.12 thf(c_0_229, plain, (p164|~p166), inference(fof_simplification,[status(thm)],[ax112])).
% 23.92/24.12 thf(c_0_230, plain, (p162|~p164), inference(split_conjunct,[status(thm)],[c_0_226])).
% 23.92/24.12 thf(c_0_231, plain, ~p162, inference(sr,[status(thm)],[c_0_227, c_0_228])).
% 23.92/24.12 thf(c_0_232, plain, (p166|~p168), inference(fof_simplification,[status(thm)],[ax110])).
% 23.92/24.12 thf(c_0_233, plain, (p164|~p166), inference(split_conjunct,[status(thm)],[c_0_229])).
% 23.92/24.12 thf(c_0_234, plain, ~p164, inference(sr,[status(thm)],[c_0_230, c_0_231])).
% 23.92/24.12 thf(c_0_235, plain, (p168|~p170), inference(fof_simplification,[status(thm)],[ax108])).
% 23.92/24.12 thf(c_0_236, plain, (p166|~p168), inference(split_conjunct,[status(thm)],[c_0_232])).
% 23.92/24.12 thf(c_0_237, plain, ~p166, inference(sr,[status(thm)],[c_0_233, c_0_234])).
% 23.92/24.12 thf(c_0_238, plain, (p170|~p172), inference(fof_simplification,[status(thm)],[ax106])).
% 23.92/24.12 thf(c_0_239, plain, (p168|~p170), inference(split_conjunct,[status(thm)],[c_0_235])).
% 23.92/24.12 thf(c_0_240, plain, ~p168, inference(sr,[status(thm)],[c_0_236, c_0_237])).
% 23.92/24.12 thf(c_0_241, plain, (p172|~p174), inference(fof_simplification,[status(thm)],[ax104])).
% 23.92/24.12 thf(c_0_242, plain, (p170|~p172), inference(split_conjunct,[status(thm)],[c_0_238])).
% 23.92/24.12 thf(c_0_243, plain, ~p170, inference(sr,[status(thm)],[c_0_239, c_0_240])).
% 23.92/24.12 thf(c_0_244, plain, (p174|~p176), inference(fof_simplification,[status(thm)],[ax102])).
% 23.92/24.12 thf(c_0_245, plain, (p172|~p174), inference(split_conjunct,[status(thm)],[c_0_241])).
% 23.92/24.12 thf(c_0_246, plain, ~p172, inference(sr,[status(thm)],[c_0_242, c_0_243])).
% 23.92/24.12 thf(c_0_247, plain, (p176|~p178), inference(fof_simplification,[status(thm)],[ax100])).
% 23.92/24.12 thf(c_0_248, plain, (p174|~p176), inference(split_conjunct,[status(thm)],[c_0_244])).
% 23.92/24.12 thf(c_0_249, plain, ~p174, inference(sr,[status(thm)],[c_0_245, c_0_246])).
% 23.92/24.12 thf(c_0_250, plain, (p178|~p180), inference(fof_simplification,[status(thm)],[ax98])).
% 23.92/24.12 thf(c_0_251, plain, (p176|~p178), inference(split_conjunct,[status(thm)],[c_0_247])).
% 23.92/24.12 thf(c_0_252, plain, ~p176, inference(sr,[status(thm)],[c_0_248, c_0_249])).
% 23.92/24.12 thf(c_0_253, plain, (p180|~p182), inference(fof_simplification,[status(thm)],[ax96])).
% 23.92/24.12 thf(c_0_254, plain, (p178|~p180), inference(split_conjunct,[status(thm)],[c_0_250])).
% 23.92/24.12 thf(c_0_255, plain, ~p178, inference(sr,[status(thm)],[c_0_251, c_0_252])).
% 23.92/24.12 thf(c_0_256, plain, (p182|~p184), inference(fof_simplification,[status(thm)],[ax94])).
% 23.92/24.12 thf(c_0_257, plain, (p180|~p182), inference(split_conjunct,[status(thm)],[c_0_253])).
% 23.92/24.12 thf(c_0_258, plain, ~p180, inference(sr,[status(thm)],[c_0_254, c_0_255])).
% 23.92/24.12 thf(c_0_259, plain, (p184|~p186), inference(fof_simplification,[status(thm)],[ax92])).
% 23.92/24.12 thf(c_0_260, plain, (p182|~p184), inference(split_conjunct,[status(thm)],[c_0_256])).
% 23.92/24.12 thf(c_0_261, plain, ~p182, inference(sr,[status(thm)],[c_0_257, c_0_258])).
% 23.92/24.12 thf(c_0_262, plain, (~p207|p206), inference(fof_simplification,[status(thm)],[ax75])).
% 23.92/24.12 thf(c_0_263, plain, (p186|~p187), inference(fof_simplification,[status(thm)],[ax91])).
% 23.92/24.12 thf(c_0_264, plain, (p184|~p186), inference(split_conjunct,[status(thm)],[c_0_259])).
% 23.92/24.12 thf(c_0_265, plain, ~p184, inference(sr,[status(thm)],[c_0_260, c_0_261])).
% 23.92/24.12 thf(c_0_266, plain, (~p2|p200), inference(fof_simplification,[status(thm)],[ax77])).
% 23.92/24.12 thf(c_0_267, plain, (~p206|p211), inference(fof_simplification,[status(thm)],[ax69])).
% 23.92/24.12 thf(c_0_268, plain, (p206|~p207), inference(split_conjunct,[status(thm)],[c_0_262])).
% 23.92/24.12 thf(c_0_269, plain, p207, inference(split_conjunct,[status(thm)],[ax76])).
% 23.92/24.12 thf(c_0_270, plain, (p187|~p189), inference(fof_simplification,[status(thm)],[ax89])).
% 23.92/24.12 thf(c_0_271, plain, (p186|~p187), inference(split_conjunct,[status(thm)],[c_0_263])).
% 23.92/24.12 thf(c_0_272, plain, ~p186, inference(sr,[status(thm)],[c_0_264, c_0_265])).
% 23.92/24.12 thf(c_0_273, plain, (p187|~p188), inference(fof_simplification,[status(thm)],[ax90])).
% 23.92/24.12 thf(c_0_274, plain, (~p200|p202), inference(fof_simplification,[status(thm)],[ax70])).
% 23.92/24.12 thf(c_0_275, plain, (p200|~p2), inference(split_conjunct,[status(thm)],[c_0_266])).
% 23.92/24.12 thf(c_0_276, plain, p2, inference(split_conjunct,[status(thm)],[ax276])).
% 23.92/24.12 thf(c_0_277, plain, (~p211|p189|p210), inference(fof_simplification,[status(thm)],[ax68])).
% 23.92/24.12 thf(c_0_278, plain, (p211|~p206), inference(split_conjunct,[status(thm)],[c_0_267])).
% 23.92/24.12 thf(c_0_279, plain, p206, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_268, c_0_269])])).
% 23.92/24.12 thf(c_0_280, plain, (p187|~p189), inference(split_conjunct,[status(thm)],[c_0_270])).
% 23.92/24.12 thf(c_0_281, plain, ~p187, inference(sr,[status(thm)],[c_0_271, c_0_272])).
% 23.92/24.12 thf(c_0_282, plain, (p187|~p188), inference(split_conjunct,[status(thm)],[c_0_273])).
% 23.92/24.12 thf(c_0_283, plain, (~p209|~p202|~p208), inference(fof_simplification,[status(thm)],[ax66])).
% 23.92/24.12 thf(c_0_284, plain, (p202|~p200), inference(split_conjunct,[status(thm)],[c_0_274])).
% 23.92/24.12 thf(c_0_285, plain, p200, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_275, c_0_276])])).
% 23.92/24.12 thf(c_0_286, plain, (~p210|p209), inference(fof_simplification,[status(thm)],[ax67])).
% 23.92/24.12 thf(c_0_287, plain, (p189|p210|~p211), inference(split_conjunct,[status(thm)],[c_0_277])).
% 23.92/24.12 thf(c_0_288, plain, p211, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_278, c_0_279])])).
% 23.92/24.12 thf(c_0_289, plain, ~p189, inference(sr,[status(thm)],[c_0_280, c_0_281])).
% 23.92/24.12 thf(c_0_290, plain, (~p191|p193), inference(fof_simplification,[status(thm)],[ax85])).
% 23.92/24.12 thf(c_0_291, plain, (p189|p191), inference(split_conjunct,[status(thm)],[ax87])).
% 23.92/24.12 thf(c_0_292, plain, (~p190|f__0 @ f__1), inference(fof_nnf,[status(thm)],[pax190])).
% 23.92/24.12 thf(c_0_293, plain, (p188|p190), inference(split_conjunct,[status(thm)],[ax88])).
% 23.92/24.12 thf(c_0_294, plain, ~p188, inference(sr,[status(thm)],[c_0_282, c_0_281])).
% 23.92/24.12 thf(c_0_295, plain, (~p209|~p202|~p208), inference(split_conjunct,[status(thm)],[c_0_283])).
% 23.92/24.12 thf(c_0_296, plain, p202, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_284, c_0_285])])).
% 23.92/24.12 thf(c_0_297, plain, (p209|~p210), inference(split_conjunct,[status(thm)],[c_0_286])).
% 23.92/24.12 thf(c_0_298, plain, p210, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_287, c_0_288])]), c_0_289])).
% 23.92/24.12 thf(c_0_299, plain, ![X29:$i]:(~p193|(~f__0 @ f__1|(~f__0 @ X29|(f__1)=(X29)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax193])])])).
% 23.92/24.12 thf(c_0_300, plain, (p193|~p191), inference(split_conjunct,[status(thm)],[c_0_290])).
% 23.92/24.12 thf(c_0_301, plain, p191, inference(sr,[status(thm)],[c_0_291, c_0_289])).
% 23.92/24.12 thf(c_0_302, plain, (f__0 @ f__1|~p190), inference(split_conjunct,[status(thm)],[c_0_292])).
% 23.92/24.12 thf(c_0_303, plain, p190, inference(sr,[status(thm)],[c_0_293, c_0_294])).
% 23.92/24.12 thf(c_0_304, plain, ![X21:$i, X22:$i, X23:$i]:((~f__0 @ X21|(~f__0 @ X22|(X21)=(X22))|p208)&((f__0 @ (esk11_1 @ X23)|~f__0 @ X23|p208)&((X23)!=(esk11_1 @ X23)|~f__0 @ X23|p208))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax208])])])])])])).
% 23.92/24.12 thf(c_0_305, plain, (~p208|~p209), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_295, c_0_296])])).
% 23.92/24.12 thf(c_0_306, plain, p209, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_297, c_0_298])])).
% 23.92/24.12 thf(c_0_307, plain, ![X1:$i]:((f__1)=(X1)|~p193|~f__0 @ f__1|~f__0 @ X1), inference(split_conjunct,[status(thm)],[c_0_299])).
% 23.92/24.12 thf(c_0_308, plain, p193, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_300, c_0_301])])).
% 23.92/24.12 thf(c_0_309, plain, f__0 @ f__1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_302, c_0_303])])).
% 23.92/24.12 thf(c_0_310, plain, ![X1:$i]:(f__0 @ (esk11_1 @ X1)|p208|~f__0 @ X1), inference(split_conjunct,[status(thm)],[c_0_304])).
% 23.92/24.12 thf(c_0_311, plain, ~p208, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_305, c_0_306])])).
% 23.92/24.12 thf(c_0_312, plain, ![X1:$i]:(p208|(X1)!=(esk11_1 @ X1)|~f__0 @ X1), inference(split_conjunct,[status(thm)],[c_0_304])).
% 23.92/24.12 thf(c_0_313, plain, ![X1:$i]:((f__1)=(X1)|~f__0 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_307, c_0_308]), c_0_309])])).
% 23.92/24.12 thf(c_0_314, plain, ![X1:$i]:(f__0 @ (esk11_1 @ X1)|~f__0 @ X1), inference(sr,[status(thm)],[c_0_310, c_0_311])).
% 23.92/24.12 thf(c_0_315, plain, ![X1:$i]:((esk11_1 @ X1)!=(X1)|~f__0 @ X1), inference(sr,[status(thm)],[c_0_312, c_0_311])).
% 23.92/24.12 thf(c_0_316, plain, ![X1:$i]:((esk11_1 @ X1)=(f__1)|~f__0 @ X1), inference(spm,[status(thm)],[c_0_313, c_0_314])).
% 23.92/24.12 thf(c_0_317, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_315, c_0_316])]), c_0_309])]), ['proof']).
% 23.92/24.12 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 23.92/24.12 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 => (setadjoinE => (setadjoinOr => (setoftrueEq => (powersetI => (emptyinPowerset => (emptyInPowerset => (powersetE => (setunionI => (setunionE => (subPowSU => (exuE2 => (nonemptyImpWitness => (uniqinunit => (notinsingleton => (eqinunit => (singletonsswitch => (upairsetE => (upairsetIL => (upairsetIR => (emptyE1 => (vacuousDall => (quantDeMorgan1 => (quantDeMorgan2 => (quantDeMorgan3 => (quantDeMorgan4 => (prop2setI => (prop2set2propI => (notdexE => (notdallE => (exuI1 => (![X1:$i>$o]:((~((![X2:$i]:(~((X1 @ X2)))))) => ((![X2:$i]:(![X3:$i]:((X1 @ X2) => ((X1 @ X3) => (X2 = X3))))) => (exu @ X1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 23.92/24.12 % SZS output end Proof
%------------------------------------------------------------------------------