%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU625^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 : n006.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:14 PM UTC 2025
% Result : Theorem 25.64s 25.81s
% Output : Proof 25.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SEU625^2 : TPTP v9.2.0. Released v3.7.0.
% 0.07/0.14 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.35 % Computer : n006.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Oct 8 21:49:23 EDT 2025
% 0.13/0.35 % CPUTime :
% 25.64/25.81 % SZS status Theorem
% 25.64/25.81 % Mode: mode371
% 25.64/25.81 % Inferences: 4105
% 25.64/25.81 % SZS output start Proof
% 25.64/25.81 thf(def_subsetI2,definition,(subsetI2 = (![X1:$i]:(![X2:$i]:((![X3:$i]:(((in @ X3) @ X1) => ((in @ X3) @ X2))) => ((subset @ X1) @ X2)))))).
% 25.64/25.81 thf(def_subsetE,definition,(subsetE = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((subset @ X1) @ X2) => (((in @ X3) @ X1) => ((in @ X3) @ X2)))))))).
% 25.64/25.81 thf(def_binunionLsub,definition,(binunionLsub = (![X1:$i]:(![X2:$i]:((subset @ X1) @ ((binunion @ X1) @ X2)))))).
% 25.64/25.81 thf(def_binunionRsub,definition,(binunionRsub = (![X1:$i]:(![X2:$i]:((subset @ X2) @ ((binunion @ X1) @ X2)))))).
% 25.64/25.81 thf(def_upairset2E,definition,(upairset2E = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) => ((~((X3 = X1))) => (X3 = X2)))))))).
% 25.64/25.81 thf(upairsubunion,conjecture,(subsetI2 => (subsetE => (binunionLsub => (binunionRsub => (upairset2E => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X1) => (![X4:$i]:(((in @ X4) @ X2) => ((subset @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ ((binunion @ X1) @ X2)))))))))))))).
% 25.64/25.81 thf(h0,negated_conjecture,(~((subsetI2 => (subsetE => (binunionLsub => (binunionRsub => (upairset2E => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X1) => (![X4:$i]:(((in @ X4) @ X2) => ((subset @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ ((binunion @ X1) @ X2))))))))))))))),inference(assume_negation,[status(cth)],[upairsubunion])).
% 25.64/25.81 thf(ax124, axiom, (p1|~(p8)), file('<stdin>', ax124)).
% 25.64/25.81 thf(ax131, axiom, ~(p1), file('<stdin>', ax131)).
% 25.64/25.81 thf(ax122, axiom, (p8|~(p10)), file('<stdin>', ax122)).
% 25.64/25.81 thf(ax120, axiom, (p10|~(p12)), file('<stdin>', ax120)).
% 25.64/25.81 thf(ax118, axiom, (p12|~(p14)), file('<stdin>', ax118)).
% 25.64/25.81 thf(nax1, axiom, (p1<=(fsubsetI2=>(fsubsetE=>(fbinunionLsub=>(fbinunionRsub=>(fupairset2E=>![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ X1=>![X4:$i]:(fin @ X4 @ X2=>fsubset @ (fsetadjoin @ X3 @ (fsetadjoin @ X4 @ femptyset)) @ (fbinunion @ X1 @ X2))))))))), file('<stdin>', nax1)).
% 25.64/25.81 thf(ax116, axiom, (p14|~(p16)), file('<stdin>', ax116)).
% 25.64/25.81 thf(nax7, axiom, (p7<=fsubsetI2), file('<stdin>', nax7)).
% 25.64/25.81 thf(ax115, axiom, (p16|~(p17)), file('<stdin>', ax115)).
% 25.64/25.81 thf(ax99, axiom, (~(p2)|~(p7)|p31), file('<stdin>', ax99)).
% 25.64/25.81 thf(ax114, axiom, (p17|~(p18)), file('<stdin>', ax114)).
% 25.64/25.81 thf(ax96, axiom, (~(p31)|p34), file('<stdin>', ax96)).
% 25.64/25.81 thf(ax130, axiom, p2, file('<stdin>', ax130)).
% 25.64/25.81 thf(ax113, axiom, (p18|~(p19)), file('<stdin>', ax113)).
% 25.64/25.81 thf(ax97, axiom, (~(p34)|p33), file('<stdin>', ax97)).
% 25.64/25.81 thf(ax111, axiom, (p19|~(p21)), file('<stdin>', ax111)).
% 25.64/25.81 thf(nax15, axiom, (p15<=fupairset2E), file('<stdin>', nax15)).
% 25.64/25.81 thf(ax98, axiom, (~(p33)|~(p32)|p24), file('<stdin>', ax98)).
% 25.64/25.81 thf(ax110, axiom, (p21|~(p22)), file('<stdin>', ax110)).
% 25.64/25.81 thf(nax9, axiom, (p9<=fsubsetE), file('<stdin>', nax9)).
% 25.64/25.81 thf(ax8, axiom, (~(p6)|~(p15)|p113), file('<stdin>', ax8)).
% 25.64/25.81 thf(ax108, axiom, (p22|~(p24)), file('<stdin>', ax108)).
% 25.64/25.81 thf(ax54, axiom, (~(p3)|~(p9)|p73), file('<stdin>', ax54)).
% 25.64/25.81 thf(nax13, axiom, (p13<=fbinunionRsub), file('<stdin>', nax13)).
% 25.64/25.81 thf(pax113, axiom, (p113=>![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset))=>(~((X3)=(X1))=>(X3)=(X2)))), file('<stdin>', pax113)).
% 25.64/25.81 thf(ax126, axiom, p6, file('<stdin>', ax126)).
% 25.64/25.81 thf(nax32, axiom, (p32<=![X1:$i]:(fin @ X1 @ (fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset))=>fin @ X1 @ (fbinunion @ f__0 @ f__1))), file('<stdin>', nax32)).
% 25.64/25.81 thf(pax73, axiom, (p73=>![X1:$i, X2:$i, X3:$i]:(fsubset @ X1 @ X2=>(fin @ X3 @ X1=>fin @ X3 @ X2))), file('<stdin>', pax73)).
% 25.64/25.81 thf(ax129, axiom, p3, file('<stdin>', ax129)).
% 25.64/25.81 thf(pax23, axiom, (p23=>fin @ f__3 @ f__1), file('<stdin>', pax23)).
% 25.64/25.81 thf(ax109, axiom, (p22|p23), file('<stdin>', ax109)).
% 25.64/25.81 thf(ax23, axiom, (~(p5)|~(p13)|p100), file('<stdin>', ax23)).
% 25.64/25.81 thf(nax11, axiom, (p11<=fbinunionLsub), file('<stdin>', nax11)).
% 25.64/25.81 thf(pax100, axiom, (p100=>![X1:$i, X2:$i]:fsubset @ X2 @ (fbinunion @ X1 @ X2)), file('<stdin>', pax100)).
% 25.64/25.81 thf(ax127, axiom, p5, file('<stdin>', ax127)).
% 25.64/25.81 thf(pax20, axiom, (p20=>fin @ f__2 @ f__0), file('<stdin>', pax20)).
% 25.64/25.81 thf(ax112, axiom, (p19|p20), file('<stdin>', ax112)).
% 25.64/25.81 thf(ax38, axiom, (~(p4)|~(p11)|p87), file('<stdin>', ax38)).
% 25.64/25.81 thf(pax87, axiom, (p87=>![X1:$i, X2:$i]:fsubset @ X1 @ (fbinunion @ X1 @ X2)), file('<stdin>', pax87)).
% 25.64/25.81 thf(ax128, axiom, p4, file('<stdin>', ax128)).
% 25.64/25.81 thf(c_0_40, plain, (p1|~p8), inference(fof_simplification,[status(thm)],[ax124])).
% 25.64/25.81 thf(c_0_41, plain, ~p1, inference(fof_simplification,[status(thm)],[ax131])).
% 25.64/25.81 thf(c_0_42, plain, (p8|~p10), inference(fof_simplification,[status(thm)],[ax122])).
% 25.64/25.81 thf(c_0_43, plain, (p1|~p8), inference(split_conjunct,[status(thm)],[c_0_40])).
% 25.64/25.81 thf(c_0_44, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_41])).
% 25.64/25.81 thf(c_0_45, plain, (p10|~p12), inference(fof_simplification,[status(thm)],[ax120])).
% 25.64/25.81 thf(c_0_46, plain, (p8|~p10), inference(split_conjunct,[status(thm)],[c_0_42])).
% 25.64/25.81 thf(c_0_47, plain, ~p8, inference(sr,[status(thm)],[c_0_43, c_0_44])).
% 25.64/25.81 thf(c_0_48, plain, (p12|~p14), inference(fof_simplification,[status(thm)],[ax118])).
% 25.64/25.81 thf(c_0_49, plain, (p10|~p12), inference(split_conjunct,[status(thm)],[c_0_45])).
% 25.64/25.81 thf(c_0_50, plain, ~p10, inference(sr,[status(thm)],[c_0_46, c_0_47])).
% 25.64/25.81 thf(c_0_51, plain, ((fsubsetI2|p1)&((fsubsetE|p1)&((fbinunionLsub|p1)&((fbinunionRsub|p1)&((fupairset2E|p1)&((fin @ esk106_0 @ esk104_0|p1)&((fin @ esk107_0 @ esk105_0|p1)&(~fsubset @ (fsetadjoin @ esk106_0 @ (fsetadjoin @ esk107_0 @ femptyset)) @ (fbinunion @ esk104_0 @ esk105_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.64/25.81 thf(c_0_52, plain, (p14|~p16), inference(fof_simplification,[status(thm)],[ax116])).
% 25.64/25.81 thf(c_0_53, plain, (p12|~p14), inference(split_conjunct,[status(thm)],[c_0_48])).
% 25.64/25.81 thf(c_0_54, plain, ~p12, inference(sr,[status(thm)],[c_0_49, c_0_50])).
% 25.64/25.81 thf(c_0_55, plain, (~fsubsetI2|p7), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax7])])).
% 25.64/25.81 thf(c_0_56, plain, (fsubsetI2|p1), inference(split_conjunct,[status(thm)],[c_0_51])).
% 25.64/25.81 thf(c_0_57, plain, (p16|~p17), inference(fof_simplification,[status(thm)],[ax115])).
% 25.64/25.81 thf(c_0_58, plain, (p14|~p16), inference(split_conjunct,[status(thm)],[c_0_52])).
% 25.64/25.81 thf(c_0_59, plain, ~p14, inference(sr,[status(thm)],[c_0_53, c_0_54])).
% 25.64/25.81 thf(c_0_60, plain, (~p2|~p7|p31), inference(fof_simplification,[status(thm)],[ax99])).
% 25.64/25.81 thf(c_0_61, plain, (p7|~fsubsetI2), inference(split_conjunct,[status(thm)],[c_0_55])).
% 25.64/25.81 thf(c_0_62, plain, fsubsetI2, inference(sr,[status(thm)],[c_0_56, c_0_44])).
% 25.64/25.81 thf(c_0_63, plain, (p17|~p18), inference(fof_simplification,[status(thm)],[ax114])).
% 25.64/25.81 thf(c_0_64, plain, (p16|~p17), inference(split_conjunct,[status(thm)],[c_0_57])).
% 25.64/25.81 thf(c_0_65, plain, ~p16, inference(sr,[status(thm)],[c_0_58, c_0_59])).
% 25.64/25.81 thf(c_0_66, plain, (~p31|p34), inference(fof_simplification,[status(thm)],[ax96])).
% 25.64/25.81 thf(c_0_67, plain, (p31|~p2|~p7), inference(split_conjunct,[status(thm)],[c_0_60])).
% 25.64/25.81 thf(c_0_68, plain, p2, inference(split_conjunct,[status(thm)],[ax130])).
% 25.64/25.81 thf(c_0_69, plain, p7, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_61, c_0_62])])).
% 25.64/25.81 thf(c_0_70, plain, (p18|~p19), inference(fof_simplification,[status(thm)],[ax113])).
% 25.64/25.81 thf(c_0_71, plain, (p17|~p18), inference(split_conjunct,[status(thm)],[c_0_63])).
% 25.64/25.81 thf(c_0_72, plain, ~p17, inference(sr,[status(thm)],[c_0_64, c_0_65])).
% 25.64/25.81 thf(c_0_73, plain, (~p34|p33), inference(fof_simplification,[status(thm)],[ax97])).
% 25.64/25.81 thf(c_0_74, plain, (p34|~p31), inference(split_conjunct,[status(thm)],[c_0_66])).
% 25.64/25.81 thf(c_0_75, plain, p31, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_67, c_0_68]), c_0_69])])).
% 25.64/25.81 thf(c_0_76, plain, (p19|~p21), inference(fof_simplification,[status(thm)],[ax111])).
% 25.64/25.81 thf(c_0_77, plain, (p18|~p19), inference(split_conjunct,[status(thm)],[c_0_70])).
% 25.64/25.81 thf(c_0_78, plain, ~p18, inference(sr,[status(thm)],[c_0_71, c_0_72])).
% 25.64/25.81 thf(c_0_79, plain, (~fupairset2E|p15), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax15])])).
% 25.64/25.81 thf(c_0_80, plain, (fupairset2E|p1), inference(split_conjunct,[status(thm)],[c_0_51])).
% 25.64/25.81 thf(c_0_81, plain, (~p33|~p32|p24), inference(fof_simplification,[status(thm)],[ax98])).
% 25.64/25.81 thf(c_0_82, plain, (p33|~p34), inference(split_conjunct,[status(thm)],[c_0_73])).
% 25.64/25.81 thf(c_0_83, plain, p34, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_74, c_0_75])])).
% 25.64/25.81 thf(c_0_84, plain, (p21|~p22), inference(fof_simplification,[status(thm)],[ax110])).
% 25.64/25.81 thf(c_0_85, plain, (p19|~p21), inference(split_conjunct,[status(thm)],[c_0_76])).
% 25.64/25.81 thf(c_0_86, plain, ~p19, inference(sr,[status(thm)],[c_0_77, c_0_78])).
% 25.64/25.81 thf(c_0_87, plain, (~fsubsetE|p9), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax9])])).
% 25.64/25.81 thf(c_0_88, plain, (fsubsetE|p1), inference(split_conjunct,[status(thm)],[c_0_51])).
% 25.64/25.81 thf(c_0_89, plain, (~p6|~p15|p113), inference(fof_simplification,[status(thm)],[ax8])).
% 25.64/25.81 thf(c_0_90, plain, (p15|~fupairset2E), inference(split_conjunct,[status(thm)],[c_0_79])).
% 25.64/25.81 thf(c_0_91, plain, fupairset2E, inference(sr,[status(thm)],[c_0_80, c_0_44])).
% 25.64/25.81 thf(c_0_92, plain, (p22|~p24), inference(fof_simplification,[status(thm)],[ax108])).
% 25.64/25.81 thf(c_0_93, plain, (p24|~p33|~p32), inference(split_conjunct,[status(thm)],[c_0_81])).
% 25.64/25.81 thf(c_0_94, plain, p33, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_82, c_0_83])])).
% 25.64/25.81 thf(c_0_95, plain, (p21|~p22), inference(split_conjunct,[status(thm)],[c_0_84])).
% 25.64/25.81 thf(c_0_96, plain, ~p21, inference(sr,[status(thm)],[c_0_85, c_0_86])).
% 25.64/25.81 thf(c_0_97, plain, (~p3|~p9|p73), inference(fof_simplification,[status(thm)],[ax54])).
% 25.64/25.81 thf(c_0_98, plain, (p9|~fsubsetE), inference(split_conjunct,[status(thm)],[c_0_87])).
% 25.64/25.81 thf(c_0_99, plain, fsubsetE, inference(sr,[status(thm)],[c_0_88, c_0_44])).
% 25.64/25.81 thf(c_0_100, plain, (~fbinunionRsub|p13), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax13])])).
% 25.64/25.81 thf(c_0_101, plain, (fbinunionRsub|p1), inference(split_conjunct,[status(thm)],[c_0_51])).
% 25.64/25.81 thf(c_0_102, plain, ![X27:$i, X28:$i, X29:$i]:(~p113|(~fin @ X29 @ (fsetadjoin @ X27 @ (fsetadjoin @ X28 @ femptyset))|((X29)=(X27)|(X29)=(X28)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax113])])])])).
% 25.64/25.81 thf(c_0_103, plain, (p113|~p6|~p15), inference(split_conjunct,[status(thm)],[c_0_89])).
% 25.64/25.81 thf(c_0_104, plain, p6, inference(split_conjunct,[status(thm)],[ax126])).
% 25.64/25.81 thf(c_0_105, plain, p15, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_90, c_0_91])])).
% 25.64/25.81 thf(c_0_106, plain, ((fin @ esk73_0 @ (fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset))|p32)&(~fin @ esk73_0 @ (fbinunion @ f__0 @ f__1)|p32)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax32])])])])])).
% 25.64/25.81 thf(c_0_107, plain, (p22|~p24), inference(split_conjunct,[status(thm)],[c_0_92])).
% 25.64/25.81 thf(c_0_108, plain, (p24|~p32), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_93, c_0_94])])).
% 25.64/25.81 thf(c_0_109, plain, ~p22, inference(sr,[status(thm)],[c_0_95, c_0_96])).
% 25.64/25.81 thf(c_0_110, plain, ![X101:$i, X102:$i, X103:$i]:(~p73|(~fsubset @ X101 @ X102|(~fin @ X103 @ X101|fin @ X103 @ X102))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax73])])])).
% 25.64/25.81 thf(c_0_111, plain, (p73|~p3|~p9), inference(split_conjunct,[status(thm)],[c_0_97])).
% 25.64/25.81 thf(c_0_112, plain, p3, inference(split_conjunct,[status(thm)],[ax129])).
% 25.64/25.81 thf(c_0_113, plain, p9, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_98, c_0_99])])).
% 25.64/25.81 thf(c_0_114, plain, (~p23|fin @ f__3 @ f__1), inference(fof_nnf,[status(thm)],[pax23])).
% 25.64/25.81 thf(c_0_115, plain, (p22|p23), inference(split_conjunct,[status(thm)],[ax109])).
% 25.64/25.81 thf(c_0_116, plain, (~p5|~p13|p100), inference(fof_simplification,[status(thm)],[ax23])).
% 25.64/25.81 thf(c_0_117, plain, (p13|~fbinunionRsub), inference(split_conjunct,[status(thm)],[c_0_100])).
% 25.64/25.81 thf(c_0_118, plain, fbinunionRsub, inference(sr,[status(thm)],[c_0_101, c_0_44])).
% 25.64/25.81 thf(c_0_119, plain, (~fbinunionLsub|p11), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax11])])).
% 25.64/25.81 thf(c_0_120, plain, (fbinunionLsub|p1), inference(split_conjunct,[status(thm)],[c_0_51])).
% 25.64/25.81 thf(c_0_121, plain, ![X1:$i, X2:$i, X3:$i]:((X1)=(X2)|(X1)=(X3)|~p113|~fin @ X1 @ (fsetadjoin @ X2 @ (fsetadjoin @ X3 @ femptyset))), inference(split_conjunct,[status(thm)],[c_0_102])).
% 25.64/25.81 thf(c_0_122, plain, p113, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_103, c_0_104]), c_0_105])])).
% 25.64/25.81 thf(c_0_123, plain, (fin @ esk73_0 @ (fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset))|p32), inference(split_conjunct,[status(thm)],[c_0_106])).
% 25.64/25.81 thf(c_0_124, plain, ~p32, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_107, c_0_108]), c_0_109])).
% 25.64/25.81 thf(c_0_125, plain, ![X3:$i, X2:$i, X1:$i]:(fin @ X3 @ X2|~p73|~fsubset @ X1 @ X2|~fin @ X3 @ X1), inference(split_conjunct,[status(thm)],[c_0_110])).
% 25.64/25.81 thf(c_0_126, plain, p73, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_111, c_0_112]), c_0_113])])).
% 25.64/25.81 thf(c_0_127, plain, (fin @ f__3 @ f__1|~p23), inference(split_conjunct,[status(thm)],[c_0_114])).
% 25.64/25.81 thf(c_0_128, plain, p23, inference(sr,[status(thm)],[c_0_115, c_0_109])).
% 25.64/25.81 thf(c_0_129, plain, ![X47:$i, X48:$i]:(~p100|fsubset @ X48 @ (fbinunion @ X47 @ X48)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax100])])])).
% 25.64/25.81 thf(c_0_130, plain, (p100|~p5|~p13), inference(split_conjunct,[status(thm)],[c_0_116])).
% 25.64/25.81 thf(c_0_131, plain, p5, inference(split_conjunct,[status(thm)],[ax127])).
% 25.64/25.81 thf(c_0_132, plain, p13, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_117, c_0_118])])).
% 25.64/25.81 thf(c_0_133, plain, (~p20|fin @ f__2 @ f__0), inference(fof_nnf,[status(thm)],[pax20])).
% 25.64/25.81 thf(c_0_134, plain, (p19|p20), inference(split_conjunct,[status(thm)],[ax112])).
% 25.64/25.81 thf(c_0_135, plain, (~p4|~p11|p87), inference(fof_simplification,[status(thm)],[ax38])).
% 25.64/25.81 thf(c_0_136, plain, (p11|~fbinunionLsub), inference(split_conjunct,[status(thm)],[c_0_119])).
% 25.64/25.81 thf(c_0_137, plain, fbinunionLsub, inference(sr,[status(thm)],[c_0_120, c_0_44])).
% 25.64/25.81 thf(c_0_138, plain, (p32|~fin @ esk73_0 @ (fbinunion @ f__0 @ f__1)), inference(split_conjunct,[status(thm)],[c_0_106])).
% 25.64/25.81 thf(c_0_139, plain, ![X1:$i, X2:$i, X3:$i]:((X1)=(X2)|(X1)=(X3)|~fin @ X1 @ (fsetadjoin @ X2 @ (fsetadjoin @ X3 @ femptyset))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_121, c_0_122])])).
% 25.64/25.81 thf(c_0_140, plain, fin @ esk73_0 @ (fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset)), inference(sr,[status(thm)],[c_0_123, c_0_124])).
% 25.64/25.81 thf(c_0_141, plain, ![X1:$i, X3:$i, X2:$i]:(fin @ X1 @ X2|~fin @ X1 @ X3|~fsubset @ X3 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_125, c_0_126])])).
% 25.64/25.81 thf(c_0_142, plain, fin @ f__3 @ f__1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_127, c_0_128])])).
% 25.64/25.81 thf(c_0_143, plain, ![X2:$i, X1:$i]:(fsubset @ X1 @ (fbinunion @ X2 @ X1)|~p100), inference(split_conjunct,[status(thm)],[c_0_129])).
% 25.64/25.81 thf(c_0_144, plain, p100, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_130, c_0_131]), c_0_132])])).
% 25.64/25.81 thf(c_0_145, plain, (fin @ f__2 @ f__0|~p20), inference(split_conjunct,[status(thm)],[c_0_133])).
% 25.64/25.81 thf(c_0_146, plain, p20, inference(sr,[status(thm)],[c_0_134, c_0_86])).
% 25.64/25.81 thf(c_0_147, plain, ![X65:$i, X66:$i]:(~p87|fsubset @ X65 @ (fbinunion @ X65 @ X66)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax87])])])).
% 25.64/25.81 thf(c_0_148, plain, (p87|~p4|~p11), inference(split_conjunct,[status(thm)],[c_0_135])).
% 25.64/25.81 thf(c_0_149, plain, p4, inference(split_conjunct,[status(thm)],[ax128])).
% 25.64/25.81 thf(c_0_150, plain, p11, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_136, c_0_137])])).
% 25.64/25.81 thf(c_0_151, plain, ~fin @ esk73_0 @ (fbinunion @ f__0 @ f__1), inference(sr,[status(thm)],[c_0_138, c_0_124])).
% 25.64/25.81 thf(c_0_152, plain, ((esk73_0)=(f__2)|(esk73_0)=(f__3)), inference(spm,[status(thm)],[c_0_139, c_0_140])).
% 25.64/25.81 thf(c_0_153, plain, ![X1:$i]:(fin @ f__3 @ X1|~fsubset @ f__1 @ X1), inference(spm,[status(thm)],[c_0_141, c_0_142])).
% 25.64/25.81 thf(c_0_154, plain, ![X2:$i, X1:$i]:fsubset @ X1 @ (fbinunion @ X2 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_143, c_0_144])])).
% 25.64/25.81 thf(c_0_155, plain, fin @ f__2 @ f__0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_145, c_0_146])])).
% 25.64/25.81 thf(c_0_156, plain, ![X1:$i, X2:$i]:(fsubset @ X1 @ (fbinunion @ X1 @ X2)|~p87), inference(split_conjunct,[status(thm)],[c_0_147])).
% 25.64/25.81 thf(c_0_157, plain, p87, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_148, c_0_149]), c_0_150])])).
% 25.64/25.81 thf(c_0_158, plain, ((esk73_0)=(f__2)|~fin @ f__3 @ (fbinunion @ f__0 @ f__1)), inference(spm,[status(thm)],[c_0_151, c_0_152])).
% 25.64/25.81 thf(c_0_159, plain, ![X1:$i]:fin @ f__3 @ (fbinunion @ X1 @ f__1), inference(spm,[status(thm)],[c_0_153, c_0_154])).
% 25.64/25.81 thf(c_0_160, plain, ![X1:$i]:(fin @ f__2 @ X1|~fsubset @ f__0 @ X1), inference(spm,[status(thm)],[c_0_141, c_0_155])).
% 25.64/25.81 thf(c_0_161, plain, ![X1:$i, X2:$i]:fsubset @ X1 @ (fbinunion @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_156, c_0_157])])).
% 25.64/25.81 thf(c_0_162, plain, (esk73_0)=(f__2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_158, c_0_159])])).
% 25.64/25.81 thf(c_0_163, plain, ![X1:$i]:fin @ f__2 @ (fbinunion @ f__0 @ X1), inference(spm,[status(thm)],[c_0_160, c_0_161])).
% 25.64/25.81 thf(c_0_164, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_151, c_0_162]), c_0_163])]), ['proof']).
% 25.64/25.81 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 25.64/25.81 thf(0,theorem,(subsetI2 => (subsetE => (binunionLsub => (binunionRsub => (upairset2E => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X1) => (![X4:$i]:(((in @ X4) @ X2) => ((subset @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ ((binunion @ X1) @ X2))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 25.64/25.81 % SZS output end Proof
%------------------------------------------------------------------------------