%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU627^2 : TPTP v9.2.0. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : 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:44:15 PM UTC 2025
% Result : Theorem 25.00s 25.66s
% Output : Proof 25.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU627^2 : TPTP v9.2.0. Released v3.7.0.
% 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n015.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 8 21:27:53 EDT 2025
% 0.13/0.34 % CPUTime :
% 25.00/25.66 % SZS status Theorem
% 25.00/25.66 % Mode: mode371
% 25.00/25.66 % Inferences: 4102
% 25.00/25.66 % SZS output start Proof
% 25.00/25.66 thf(def_subsetI2,definition,(subsetI2 = (![X1:$i]:(![X2:$i]:((![X3:$i]:(((in @ X3) @ X1) => ((in @ X3) @ X2))) => ((subset @ X1) @ X2)))))).
% 25.00/25.66 thf(def_singletoninpowunion,definition,(singletoninpowunion = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X1) => ((in @ ((setadjoin @ X3) @ emptyset)) @ (powerset @ ((binunion @ X1) @ X2))))))))).
% 25.00/25.66 thf(def_upairset2E,definition,(upairset2E = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) => ((~((X3 = X1))) => (X3 = X2)))))))).
% 25.00/25.66 thf(def_upairinpowunion,definition,(upairinpowunion = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X1) => (![X4:$i]:(((in @ X4) @ X2) => ((in @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ (powerset @ ((binunion @ X1) @ X2))))))))))).
% 25.00/25.66 thf(ubforcartprodlem1,conjecture,(subsetI2 => (singletoninpowunion => (upairset2E => (upairinpowunion => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X1) => (![X4:$i]:(((in @ X4) @ X2) => ((subset @ ((setadjoin @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ emptyset))) @ (powerset @ ((binunion @ X1) @ X2)))))))))))))).
% 25.00/25.66 thf(h0,negated_conjecture,(~((subsetI2 => (singletoninpowunion => (upairset2E => (upairinpowunion => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X1) => (![X4:$i]:(((in @ X4) @ X2) => ((subset @ ((setadjoin @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ emptyset))) @ (powerset @ ((binunion @ X1) @ X2))))))))))))))),inference(assume_negation,[status(cth)],[ubforcartprodlem1])).
% 25.00/25.66 thf(ax127, axiom, (p1|~(p7)), file('<stdin>', ax127)).
% 25.00/25.66 thf(ax133, axiom, ~(p1), file('<stdin>', ax133)).
% 25.00/25.66 thf(ax125, axiom, (p7|~(p9)), file('<stdin>', ax125)).
% 25.00/25.66 thf(ax123, axiom, (p9|~(p11)), file('<stdin>', ax123)).
% 25.00/25.66 thf(nax1, axiom, (p1<=(fsubsetI2=>(fsingletoninpowunion=>(fupairset2E=>(fupairinpowunion=>![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ X1=>![X4:$i]:(fin @ X4 @ X2=>fsubset @ (fsetadjoin @ (fsetadjoin @ X3 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X3 @ (fsetadjoin @ X4 @ femptyset)) @ femptyset)) @ (fpowerset @ (fbinunion @ X1 @ X2))))))))), file('<stdin>', nax1)).
% 25.00/25.66 thf(ax121, axiom, (p11|~(p13)), file('<stdin>', ax121)).
% 25.00/25.66 thf(nax6, axiom, (p6<=fsubsetI2), file('<stdin>', nax6)).
% 25.00/25.66 thf(ax120, axiom, (p13|~(p14)), file('<stdin>', ax120)).
% 25.00/25.66 thf(ax104, axiom, (~(p2)|~(p6)|p28), file('<stdin>', ax104)).
% 25.00/25.66 thf(ax119, axiom, (p14|~(p15)), file('<stdin>', ax119)).
% 25.00/25.66 thf(nax10, axiom, (p10<=fupairset2E), file('<stdin>', nax10)).
% 25.00/25.66 thf(ax101, axiom, (~(p28)|p31), file('<stdin>', ax101)).
% 25.00/25.66 thf(ax132, axiom, p2, file('<stdin>', ax132)).
% 25.00/25.66 thf(ax118, axiom, (p15|~(p16)), file('<stdin>', ax118)).
% 25.00/25.66 thf(ax43, axiom, (~(p4)|~(p10)|p84), file('<stdin>', ax43)).
% 25.00/25.66 thf(ax102, axiom, (~(p31)|p30), file('<stdin>', ax102)).
% 25.00/25.66 thf(ax116, axiom, (p16|~(p18)), file('<stdin>', ax116)).
% 25.00/25.66 thf(ax38, axiom, (~(p84)|p90), file('<stdin>', ax38)).
% 25.00/25.66 thf(ax130, axiom, p4, file('<stdin>', ax130)).
% 25.00/25.66 thf(ax103, axiom, (~(p30)|~(p29)|p21), file('<stdin>', ax103)).
% 25.00/25.66 thf(ax115, axiom, (p18|~(p19)), file('<stdin>', ax115)).
% 25.00/25.66 thf(ax39, axiom, (~(p90)|p89), file('<stdin>', ax39)).
% 25.00/25.66 thf(ax113, axiom, (p19|~(p21)), file('<stdin>', ax113)).
% 25.00/25.66 thf(ax40, axiom, (~(p89)|p88), file('<stdin>', ax40)).
% 25.00/25.66 thf(ax99, axiom, (p29|~(p33)), file('<stdin>', ax99)).
% 25.00/25.66 thf(ax41, axiom, (~(p88)|~(p34)|p87), file('<stdin>', ax41)).
% 25.00/25.66 thf(nax8, axiom, (p8<=fsingletoninpowunion), file('<stdin>', nax8)).
% 25.00/25.66 thf(ax98, axiom, (p33|p34), file('<stdin>', ax98)).
% 25.00/25.66 thf(ax59, axiom, (~(p3)|~(p8)|p70), file('<stdin>', ax59)).
% 25.00/25.66 thf(pax87, axiom, (p87=>(~((f__4)=(fsetadjoin @ f__2 @ femptyset))=>(f__4)=(fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset)))), file('<stdin>', pax87)).
% 25.00/25.66 thf(pax70, axiom, (p70=>![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ X1=>fin @ (fsetadjoin @ X3 @ femptyset) @ (fpowerset @ (fbinunion @ X1 @ X2)))), file('<stdin>', pax70)).
% 25.00/25.66 thf(ax131, axiom, p3, file('<stdin>', ax131)).
% 25.00/25.66 thf(nax85, axiom, (p85<=(f__4)=(fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset))), file('<stdin>', nax85)).
% 25.00/25.66 thf(pax17, axiom, (p17=>fin @ f__2 @ f__0), file('<stdin>', pax17)).
% 25.00/25.66 thf(ax117, axiom, (p16|p17), file('<stdin>', ax117)).
% 25.00/25.66 thf(nax12, axiom, (p12<=fupairinpowunion), file('<stdin>', nax12)).
% 25.00/25.66 thf(nax33, axiom, (p33<=(fin @ f__4 @ (fsetadjoin @ (fsetadjoin @ f__2 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset)) @ femptyset))=>fin @ f__4 @ (fpowerset @ (fbinunion @ f__0 @ f__1)))), file('<stdin>', nax33)).
% 25.00/25.66 thf(ax8, axiom, (~(p5)|~(p12)|p116), file('<stdin>', ax8)).
% 25.00/25.66 thf(pax116, axiom, (p116=>![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ X1=>![X4:$i]:(fin @ X4 @ X2=>fin @ (fsetadjoin @ X3 @ (fsetadjoin @ X4 @ femptyset)) @ (fpowerset @ (fbinunion @ X1 @ X2))))), file('<stdin>', pax116)).
% 25.00/25.66 thf(ax129, axiom, p5, file('<stdin>', ax129)).
% 25.00/25.66 thf(pax85, axiom, (p85=>(f__4)=(fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset))), file('<stdin>', pax85)).
% 25.00/25.66 thf(pax20, axiom, (p20=>fin @ f__3 @ f__1), file('<stdin>', pax20)).
% 25.00/25.66 thf(ax114, axiom, (p19|p20), file('<stdin>', ax114)).
% 25.00/25.66 thf(c_0_43, plain, (p1|~p7), inference(fof_simplification,[status(thm)],[ax127])).
% 25.00/25.66 thf(c_0_44, plain, ~p1, inference(fof_simplification,[status(thm)],[ax133])).
% 25.00/25.66 thf(c_0_45, plain, (p7|~p9), inference(fof_simplification,[status(thm)],[ax125])).
% 25.00/25.66 thf(c_0_46, plain, (p1|~p7), inference(split_conjunct,[status(thm)],[c_0_43])).
% 25.00/25.66 thf(c_0_47, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_44])).
% 25.00/25.66 thf(c_0_48, plain, (p9|~p11), inference(fof_simplification,[status(thm)],[ax123])).
% 25.00/25.66 thf(c_0_49, plain, (p7|~p9), inference(split_conjunct,[status(thm)],[c_0_45])).
% 25.00/25.66 thf(c_0_50, plain, ~p7, inference(sr,[status(thm)],[c_0_46, c_0_47])).
% 25.00/25.66 thf(c_0_51, plain, ((fsubsetI2|p1)&((fsingletoninpowunion|p1)&((fupairset2E|p1)&((fupairinpowunion|p1)&((fin @ esk133_0 @ esk131_0|p1)&((fin @ esk134_0 @ esk132_0|p1)&(~fsubset @ (fsetadjoin @ (fsetadjoin @ esk133_0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ esk133_0 @ (fsetadjoin @ esk134_0 @ femptyset)) @ femptyset)) @ (fpowerset @ (fbinunion @ esk131_0 @ esk132_0))|p1))))))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])])])])])).
% 25.00/25.66 thf(c_0_52, plain, (p11|~p13), inference(fof_simplification,[status(thm)],[ax121])).
% 25.00/25.66 thf(c_0_53, plain, (p9|~p11), inference(split_conjunct,[status(thm)],[c_0_48])).
% 25.00/25.66 thf(c_0_54, plain, ~p9, inference(sr,[status(thm)],[c_0_49, c_0_50])).
% 25.00/25.66 thf(c_0_55, plain, (~fsubsetI2|p6), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax6])])).
% 25.00/25.66 thf(c_0_56, plain, (fsubsetI2|p1), inference(split_conjunct,[status(thm)],[c_0_51])).
% 25.00/25.66 thf(c_0_57, plain, (p13|~p14), inference(fof_simplification,[status(thm)],[ax120])).
% 25.00/25.66 thf(c_0_58, plain, (p11|~p13), inference(split_conjunct,[status(thm)],[c_0_52])).
% 25.00/25.66 thf(c_0_59, plain, ~p11, inference(sr,[status(thm)],[c_0_53, c_0_54])).
% 25.00/25.66 thf(c_0_60, plain, (~p2|~p6|p28), inference(fof_simplification,[status(thm)],[ax104])).
% 25.00/25.66 thf(c_0_61, plain, (p6|~fsubsetI2), inference(split_conjunct,[status(thm)],[c_0_55])).
% 25.00/25.66 thf(c_0_62, plain, fsubsetI2, inference(sr,[status(thm)],[c_0_56, c_0_47])).
% 25.00/25.66 thf(c_0_63, plain, (p14|~p15), inference(fof_simplification,[status(thm)],[ax119])).
% 25.00/25.66 thf(c_0_64, plain, (p13|~p14), inference(split_conjunct,[status(thm)],[c_0_57])).
% 25.00/25.66 thf(c_0_65, plain, ~p13, inference(sr,[status(thm)],[c_0_58, c_0_59])).
% 25.00/25.66 thf(c_0_66, plain, (~fupairset2E|p10), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax10])])).
% 25.00/25.66 thf(c_0_67, plain, (fupairset2E|p1), inference(split_conjunct,[status(thm)],[c_0_51])).
% 25.00/25.66 thf(c_0_68, plain, (~p28|p31), inference(fof_simplification,[status(thm)],[ax101])).
% 25.00/25.66 thf(c_0_69, plain, (p28|~p2|~p6), inference(split_conjunct,[status(thm)],[c_0_60])).
% 25.00/25.66 thf(c_0_70, plain, p2, inference(split_conjunct,[status(thm)],[ax132])).
% 25.00/25.66 thf(c_0_71, plain, p6, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_61, c_0_62])])).
% 25.00/25.66 thf(c_0_72, plain, (p15|~p16), inference(fof_simplification,[status(thm)],[ax118])).
% 25.00/25.66 thf(c_0_73, plain, (p14|~p15), inference(split_conjunct,[status(thm)],[c_0_63])).
% 25.00/25.66 thf(c_0_74, plain, ~p14, inference(sr,[status(thm)],[c_0_64, c_0_65])).
% 25.00/25.66 thf(c_0_75, plain, (~p4|~p10|p84), inference(fof_simplification,[status(thm)],[ax43])).
% 25.00/25.66 thf(c_0_76, plain, (p10|~fupairset2E), inference(split_conjunct,[status(thm)],[c_0_66])).
% 25.00/25.66 thf(c_0_77, plain, fupairset2E, inference(sr,[status(thm)],[c_0_67, c_0_47])).
% 25.00/25.66 thf(c_0_78, plain, (~p31|p30), inference(fof_simplification,[status(thm)],[ax102])).
% 25.00/25.66 thf(c_0_79, plain, (p31|~p28), inference(split_conjunct,[status(thm)],[c_0_68])).
% 25.00/25.66 thf(c_0_80, plain, p28, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_69, c_0_70]), c_0_71])])).
% 25.00/25.66 thf(c_0_81, plain, (p16|~p18), inference(fof_simplification,[status(thm)],[ax116])).
% 25.00/25.66 thf(c_0_82, plain, (p15|~p16), inference(split_conjunct,[status(thm)],[c_0_72])).
% 25.00/25.66 thf(c_0_83, plain, ~p15, inference(sr,[status(thm)],[c_0_73, c_0_74])).
% 25.00/25.66 thf(c_0_84, plain, (~p84|p90), inference(fof_simplification,[status(thm)],[ax38])).
% 25.00/25.66 thf(c_0_85, plain, (p84|~p4|~p10), inference(split_conjunct,[status(thm)],[c_0_75])).
% 25.00/25.66 thf(c_0_86, plain, p4, inference(split_conjunct,[status(thm)],[ax130])).
% 25.00/25.66 thf(c_0_87, plain, p10, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_76, c_0_77])])).
% 25.00/25.66 thf(c_0_88, plain, (~p30|~p29|p21), inference(fof_simplification,[status(thm)],[ax103])).
% 25.00/25.66 thf(c_0_89, plain, (p30|~p31), inference(split_conjunct,[status(thm)],[c_0_78])).
% 25.00/25.66 thf(c_0_90, plain, p31, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_79, c_0_80])])).
% 25.00/25.66 thf(c_0_91, plain, (p18|~p19), inference(fof_simplification,[status(thm)],[ax115])).
% 25.00/25.66 thf(c_0_92, plain, (p16|~p18), inference(split_conjunct,[status(thm)],[c_0_81])).
% 25.00/25.66 thf(c_0_93, plain, ~p16, inference(sr,[status(thm)],[c_0_82, c_0_83])).
% 25.00/25.66 thf(c_0_94, plain, (~p90|p89), inference(fof_simplification,[status(thm)],[ax39])).
% 25.00/25.66 thf(c_0_95, plain, (p90|~p84), inference(split_conjunct,[status(thm)],[c_0_84])).
% 25.00/25.66 thf(c_0_96, plain, p84, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_85, c_0_86]), c_0_87])])).
% 25.00/25.66 thf(c_0_97, plain, (p19|~p21), inference(fof_simplification,[status(thm)],[ax113])).
% 25.00/25.66 thf(c_0_98, plain, (p21|~p30|~p29), inference(split_conjunct,[status(thm)],[c_0_88])).
% 25.00/25.66 thf(c_0_99, plain, p30, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_89, c_0_90])])).
% 25.00/25.66 thf(c_0_100, plain, (p18|~p19), inference(split_conjunct,[status(thm)],[c_0_91])).
% 25.00/25.66 thf(c_0_101, plain, ~p18, inference(sr,[status(thm)],[c_0_92, c_0_93])).
% 25.00/25.66 thf(c_0_102, plain, (~p89|p88), inference(fof_simplification,[status(thm)],[ax40])).
% 25.00/25.66 thf(c_0_103, plain, (p89|~p90), inference(split_conjunct,[status(thm)],[c_0_94])).
% 25.00/25.66 thf(c_0_104, plain, p90, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_95, c_0_96])])).
% 25.00/25.66 thf(c_0_105, plain, (p19|~p21), inference(split_conjunct,[status(thm)],[c_0_97])).
% 25.00/25.66 thf(c_0_106, plain, (p21|~p29), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_98, c_0_99])])).
% 25.00/25.66 thf(c_0_107, plain, ~p19, inference(sr,[status(thm)],[c_0_100, c_0_101])).
% 25.00/25.66 thf(c_0_108, plain, (p29|~p33), inference(fof_simplification,[status(thm)],[ax99])).
% 25.00/25.66 thf(c_0_109, plain, (~p88|~p34|p87), inference(fof_simplification,[status(thm)],[ax41])).
% 25.00/25.66 thf(c_0_110, plain, (p88|~p89), inference(split_conjunct,[status(thm)],[c_0_102])).
% 25.00/25.66 thf(c_0_111, plain, p89, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_103, c_0_104])])).
% 25.00/25.66 thf(c_0_112, plain, ~p29, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_105, c_0_106]), c_0_107])).
% 25.00/25.66 thf(c_0_113, plain, (p29|~p33), inference(split_conjunct,[status(thm)],[c_0_108])).
% 25.00/25.66 thf(c_0_114, plain, (~fsingletoninpowunion|p8), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax8])])).
% 25.00/25.66 thf(c_0_115, plain, (fsingletoninpowunion|p1), inference(split_conjunct,[status(thm)],[c_0_51])).
% 25.00/25.66 thf(c_0_116, plain, (p87|~p88|~p34), inference(split_conjunct,[status(thm)],[c_0_109])).
% 25.00/25.66 thf(c_0_117, plain, p88, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_110, c_0_111])])).
% 25.00/25.66 thf(c_0_118, plain, (p33|p34), inference(split_conjunct,[status(thm)],[ax98])).
% 25.00/25.66 thf(c_0_119, plain, ~p33, inference(spm,[status(thm)],[c_0_112, c_0_113])).
% 25.00/25.66 thf(c_0_120, plain, (~p3|~p8|p70), inference(fof_simplification,[status(thm)],[ax59])).
% 25.00/25.66 thf(c_0_121, plain, (p8|~fsingletoninpowunion), inference(split_conjunct,[status(thm)],[c_0_114])).
% 25.00/25.66 thf(c_0_122, plain, fsingletoninpowunion, inference(sr,[status(thm)],[c_0_115, c_0_47])).
% 25.00/25.66 thf(c_0_123, plain, (~p87|((f__4)=(fsetadjoin @ f__2 @ femptyset)|(f__4)=(fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset)))), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax87])])).
% 25.00/25.66 thf(c_0_124, plain, (p87|~p34), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_116, c_0_117])])).
% 25.00/25.66 thf(c_0_125, plain, p34, inference(sr,[status(thm)],[c_0_118, c_0_119])).
% 25.00/25.66 thf(c_0_126, plain, ![X163:$i, X164:$i, X165:$i]:(~p70|(~fin @ X165 @ X163|fin @ (fsetadjoin @ X165 @ femptyset) @ (fpowerset @ (fbinunion @ X163 @ X164)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax70])])])).
% 25.00/25.66 thf(c_0_127, plain, (p70|~p3|~p8), inference(split_conjunct,[status(thm)],[c_0_120])).
% 25.00/25.66 thf(c_0_128, plain, p3, inference(split_conjunct,[status(thm)],[ax131])).
% 25.00/25.66 thf(c_0_129, plain, p8, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_121, c_0_122])])).
% 25.00/25.66 thf(c_0_130, plain, ((f__4)!=(fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset))|p85), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax85])])).
% 25.00/25.66 thf(c_0_131, plain, ((f__4)=(fsetadjoin @ f__2 @ femptyset)|(f__4)=(fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset))|~p87), inference(split_conjunct,[status(thm)],[c_0_123])).
% 25.00/25.66 thf(c_0_132, plain, p87, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_124, c_0_125])])).
% 25.00/25.66 thf(c_0_133, plain, ![X1:$i, X3:$i, X2:$i]:(fin @ (fsetadjoin @ X1 @ femptyset) @ (fpowerset @ (fbinunion @ X2 @ X3))|~p70|~fin @ X1 @ X2), inference(split_conjunct,[status(thm)],[c_0_126])).
% 25.00/25.66 thf(c_0_134, plain, p70, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_127, c_0_128]), c_0_129])])).
% 25.00/25.66 thf(c_0_135, plain, (p85|(f__4)!=(fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset))), inference(split_conjunct,[status(thm)],[c_0_130])).
% 25.00/25.66 thf(c_0_136, plain, ((fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset))=(f__4)|(fsetadjoin @ f__2 @ femptyset)=(f__4)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_131, c_0_132])])).
% 25.00/25.66 thf(c_0_137, plain, (~p17|fin @ f__2 @ f__0), inference(fof_nnf,[status(thm)],[pax17])).
% 25.00/25.66 thf(c_0_138, plain, (p16|p17), inference(split_conjunct,[status(thm)],[ax117])).
% 25.00/25.66 thf(c_0_139, plain, (~fupairinpowunion|p12), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax12])])).
% 25.00/25.66 thf(c_0_140, plain, (fupairinpowunion|p1), inference(split_conjunct,[status(thm)],[c_0_51])).
% 25.00/25.66 thf(c_0_141, plain, ((fin @ f__4 @ (fsetadjoin @ (fsetadjoin @ f__2 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset)) @ femptyset))|p33)&(~fin @ f__4 @ (fpowerset @ (fbinunion @ f__0 @ f__1))|p33)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax33])])])).
% 25.00/25.66 thf(c_0_142, plain, ![X1:$i, X3:$i, X2:$i]:(fin @ (fsetadjoin @ X1 @ femptyset) @ (fpowerset @ (fbinunion @ X2 @ X3))|~fin @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_133, c_0_134])])).
% 25.00/25.66 thf(c_0_143, plain, ((fsetadjoin @ f__2 @ femptyset)=(f__4)|p85), inference(spm,[status(thm)],[c_0_135, c_0_136])).
% 25.00/25.66 thf(c_0_144, plain, (fin @ f__2 @ f__0|~p17), inference(split_conjunct,[status(thm)],[c_0_137])).
% 25.00/25.66 thf(c_0_145, plain, p17, inference(sr,[status(thm)],[c_0_138, c_0_93])).
% 25.00/25.66 thf(c_0_146, plain, (~p5|~p12|p116), inference(fof_simplification,[status(thm)],[ax8])).
% 25.00/25.66 thf(c_0_147, plain, (p12|~fupairinpowunion), inference(split_conjunct,[status(thm)],[c_0_139])).
% 25.00/25.66 thf(c_0_148, plain, fupairinpowunion, inference(sr,[status(thm)],[c_0_140, c_0_47])).
% 25.00/25.66 thf(c_0_149, plain, (p33|~fin @ f__4 @ (fpowerset @ (fbinunion @ f__0 @ f__1))), inference(split_conjunct,[status(thm)],[c_0_141])).
% 25.00/25.66 thf(c_0_150, plain, ![X2:$i, X1:$i]:(fin @ f__4 @ (fpowerset @ (fbinunion @ X1 @ X2))|p85|~fin @ f__2 @ X1), inference(spm,[status(thm)],[c_0_142, c_0_143])).
% 25.00/25.66 thf(c_0_151, plain, fin @ f__2 @ f__0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_144, c_0_145])])).
% 25.00/25.66 thf(c_0_152, plain, ![X59:$i, X60:$i, X61:$i, X62:$i]:(~p116|(~fin @ X61 @ X59|(~fin @ X62 @ X60|fin @ (fsetadjoin @ X61 @ (fsetadjoin @ X62 @ femptyset)) @ (fpowerset @ (fbinunion @ X59 @ X60))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax116])])])).
% 25.00/25.66 thf(c_0_153, plain, (p116|~p5|~p12), inference(split_conjunct,[status(thm)],[c_0_146])).
% 25.00/25.66 thf(c_0_154, plain, p5, inference(split_conjunct,[status(thm)],[ax129])).
% 25.00/25.66 thf(c_0_155, plain, p12, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_147, c_0_148])])).
% 25.00/25.66 thf(c_0_156, plain, (~p85|(f__4)=(fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset))), inference(fof_nnf,[status(thm)],[pax85])).
% 25.00/25.66 thf(c_0_157, plain, ~fin @ f__4 @ (fpowerset @ (fbinunion @ f__0 @ f__1)), inference(sr,[status(thm)],[c_0_149, c_0_119])).
% 25.00/25.66 thf(c_0_158, plain, ![X1:$i]:(fin @ f__4 @ (fpowerset @ (fbinunion @ f__0 @ X1))|p85), inference(spm,[status(thm)],[c_0_150, c_0_151])).
% 25.00/25.66 thf(c_0_159, plain, ![X1:$i, X2:$i, X3:$i, X4:$i]:(fin @ (fsetadjoin @ X1 @ (fsetadjoin @ X3 @ femptyset)) @ (fpowerset @ (fbinunion @ X2 @ X4))|~p116|~fin @ X1 @ X2|~fin @ X3 @ X4), inference(split_conjunct,[status(thm)],[c_0_152])).
% 25.00/25.66 thf(c_0_160, plain, p116, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_153, c_0_154]), c_0_155])])).
% 25.00/25.66 thf(c_0_161, plain, ((f__4)=(fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset))|~p85), inference(split_conjunct,[status(thm)],[c_0_156])).
% 25.00/25.66 thf(c_0_162, plain, p85, inference(spm,[status(thm)],[c_0_157, c_0_158])).
% 25.00/25.66 thf(c_0_163, plain, (~p20|fin @ f__3 @ f__1), inference(fof_nnf,[status(thm)],[pax20])).
% 25.00/25.66 thf(c_0_164, plain, (p19|p20), inference(split_conjunct,[status(thm)],[ax114])).
% 25.00/25.66 thf(c_0_165, plain, ![X2:$i, X1:$i, X4:$i, X3:$i]:(fin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ (fpowerset @ (fbinunion @ X3 @ X4))|~fin @ X2 @ X4|~fin @ X1 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_159, c_0_160])])).
% 25.00/25.66 thf(c_0_166, plain, (fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset))=(f__4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_161, c_0_162])])).
% 25.00/25.66 thf(c_0_167, plain, (fin @ f__3 @ f__1|~p20), inference(split_conjunct,[status(thm)],[c_0_163])).
% 25.00/25.66 thf(c_0_168, plain, p20, inference(sr,[status(thm)],[c_0_164, c_0_107])).
% 25.00/25.66 thf(c_0_169, plain, ![X2:$i, X1:$i]:(fin @ f__4 @ (fpowerset @ (fbinunion @ X1 @ X2))|~fin @ f__3 @ X2|~fin @ f__2 @ X1), inference(spm,[status(thm)],[c_0_165, c_0_166])).
% 25.00/25.66 thf(c_0_170, plain, fin @ f__3 @ f__1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_167, c_0_168])])).
% 25.00/25.66 thf(c_0_171, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_157, c_0_169]), c_0_170]), c_0_151])]), ['proof']).
% 25.00/25.66 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 25.00/25.66 thf(0,theorem,(subsetI2 => (singletoninpowunion => (upairset2E => (upairinpowunion => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X1) => (![X4:$i]:(((in @ X4) @ X2) => ((subset @ ((setadjoin @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ emptyset))) @ (powerset @ ((binunion @ X1) @ X2))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 25.00/25.66 % SZS output end Proof
%------------------------------------------------------------------------------