%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU651^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 : n023.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:35 PM UTC 2025
% Result : Theorem 24.11s 24.09s
% Output : Proof 24.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU651^2 : TPTP v9.2.0. Released v3.7.0.
% 0.03/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n023.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 20:43:08 EDT 2025
% 0.13/0.34 % CPUTime :
% 24.11/24.09 % SZS status Theorem
% 24.11/24.09 % Mode: mode371
% 24.11/24.09 % Inferences: 4099
% 24.11/24.09 % SZS output start Proof
% 24.11/24.09 thf(def_uniqinunit,definition,(uniqinunit = (![X1:$i]:(![X2:$i]:(((in @ X1) @ ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))))).
% 24.11/24.09 thf(def_secondinupair,definition,(secondinupair = (![X1:$i]:(![X2:$i]:((in @ X2) @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))))))).
% 24.11/24.09 thf(def_setukpairinjR12,definition,(setukpairinjR12 = (![X1:$i]:(![X2:$i]:((X1 = X2) => (((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset)) = ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ emptyset))))))).
% 24.11/24.09 thf(setukpairinjR1,conjecture,(uniqinunit => (secondinupair => (setukpairinjR12 => (![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset)) = ((setadjoin @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ emptyset))) => ((X3 = X4) => (X2 = X4))))))))))).
% 24.11/24.09 thf(h0,negated_conjecture,(~((uniqinunit => (secondinupair => (setukpairinjR12 => (![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset)) = ((setadjoin @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ emptyset))) => ((X3 = X4) => (X2 = X4)))))))))))),inference(assume_negation,[status(cth)],[setukpairinjR1])).
% 24.11/24.09 thf(ax61, axiom, (p1|~(p6)), file('<stdin>', ax61)).
% 24.11/24.09 thf(ax66, axiom, ~(p1), file('<stdin>', ax66)).
% 24.11/24.09 thf(ax59, axiom, (p6|~(p8)), file('<stdin>', ax59)).
% 24.11/24.09 thf(ax57, axiom, (p8|~(p10)), file('<stdin>', ax57)).
% 24.11/24.09 thf(ax56, axiom, (p10|~(p11)), file('<stdin>', ax56)).
% 24.11/24.09 thf(ax55, axiom, (p11|~(p12)), file('<stdin>', ax55)).
% 24.11/24.09 thf(nax1, axiom, (p1<=(funiqinunit=>(fsecondinupair=>(fsetukpairinjR12=>![X1:$i, X2:$i, X3:$i, X4:$i]:((fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ X3 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X3 @ (fsetadjoin @ X4 @ femptyset)) @ femptyset))=>((X3)=(X4)=>(X2)=(X4))))))), file('<stdin>', nax1)).
% 24.11/24.09 thf(ax54, axiom, (p12|~(p13)), file('<stdin>', ax54)).
% 24.11/24.09 thf(nax9, axiom, (p9<=fsetukpairinjR12), file('<stdin>', nax9)).
% 24.11/24.09 thf(nax7, axiom, (p7<=fsecondinupair), file('<stdin>', nax7)).
% 24.11/24.09 thf(ax53, axiom, (p13|~(p14)), file('<stdin>', ax53)).
% 24.11/24.09 thf(ax0, axiom, (~(p4)|~(p9)|p58), file('<stdin>', ax0)).
% 24.11/24.09 thf(nax5, axiom, (p5<=funiqinunit), file('<stdin>', nax5)).
% 24.11/24.09 thf(ax10, axiom, (~(p3)|~(p7)|p50), file('<stdin>', ax10)).
% 24.11/24.09 thf(nax14, axiom, (p14<=((fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ f__2 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset)) @ femptyset))=>((f__2)=(f__3)=>(f__1)=(f__3)))), file('<stdin>', nax14)).
% 24.11/24.09 thf(pax58, axiom, (p58=>![X1:$i, X2:$i]:((X1)=(X2)=>(fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ femptyset))), file('<stdin>', pax58)).
% 24.11/24.09 thf(ax63, axiom, p4, file('<stdin>', ax63)).
% 24.11/24.09 thf(ax22, axiom, (~(p2)|~(p5)|p40), file('<stdin>', ax22)).
% 24.11/24.09 thf(nax13, axiom, (p13<=![X1:$i]:((fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ f__2 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__2 @ (fsetadjoin @ X1 @ femptyset)) @ femptyset))=>((f__2)=(X1)=>(f__1)=(X1)))), file('<stdin>', nax13)).
% 24.11/24.09 thf(pax50, axiom, (p50=>![X1:$i, X2:$i]:fin @ X2 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset))), file('<stdin>', pax50)).
% 24.11/24.09 thf(ax64, axiom, p3, file('<stdin>', ax64)).
% 24.11/24.09 thf(pax15, axiom, (p15=>(fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ f__2 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset)) @ femptyset))), file('<stdin>', pax15)).
% 24.11/24.09 thf(ax52, axiom, (p14|p15), file('<stdin>', ax52)).
% 24.11/24.09 thf(ax19, axiom, (~(p40)|p43), file('<stdin>', ax19)).
% 24.11/24.09 thf(ax65, axiom, p2, file('<stdin>', ax65)).
% 24.11/24.09 thf(pax40, axiom, (p40=>![X1:$i, X2:$i]:(fin @ X1 @ (fsetadjoin @ X2 @ femptyset)=>(X1)=(X2))), file('<stdin>', pax40)).
% 24.11/24.09 thf(ax20, axiom, (~(p43)|p42), file('<stdin>', ax20)).
% 24.11/24.09 thf(pax42, axiom, (p42=>(fin @ f__1 @ (fsetadjoin @ f__3 @ femptyset)=>(f__1)=(f__3))), file('<stdin>', pax42)).
% 24.11/24.09 thf(c_0_28, plain, (p1|~p6), inference(fof_simplification,[status(thm)],[ax61])).
% 24.11/24.09 thf(c_0_29, plain, ~p1, inference(fof_simplification,[status(thm)],[ax66])).
% 24.11/24.09 thf(c_0_30, plain, (p6|~p8), inference(fof_simplification,[status(thm)],[ax59])).
% 24.11/24.09 thf(c_0_31, plain, (p1|~p6), inference(split_conjunct,[status(thm)],[c_0_28])).
% 24.11/24.09 thf(c_0_32, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_29])).
% 24.11/24.09 thf(c_0_33, plain, (p8|~p10), inference(fof_simplification,[status(thm)],[ax57])).
% 24.11/24.09 thf(c_0_34, plain, (p6|~p8), inference(split_conjunct,[status(thm)],[c_0_30])).
% 24.11/24.09 thf(c_0_35, plain, ~p6, inference(sr,[status(thm)],[c_0_31, c_0_32])).
% 24.11/24.09 thf(c_0_36, plain, (p10|~p11), inference(fof_simplification,[status(thm)],[ax56])).
% 24.11/24.09 thf(c_0_37, plain, (p8|~p10), inference(split_conjunct,[status(thm)],[c_0_33])).
% 24.11/24.09 thf(c_0_38, plain, ~p8, inference(sr,[status(thm)],[c_0_34, c_0_35])).
% 24.11/24.09 thf(c_0_39, plain, (p11|~p12), inference(fof_simplification,[status(thm)],[ax55])).
% 24.11/24.09 thf(c_0_40, plain, (p10|~p11), inference(split_conjunct,[status(thm)],[c_0_36])).
% 24.11/24.09 thf(c_0_41, plain, ~p10, inference(sr,[status(thm)],[c_0_37, c_0_38])).
% 24.11/24.09 thf(c_0_42, plain, ((funiqinunit|p1)&((fsecondinupair|p1)&((fsetukpairinjR12|p1)&(((fsetadjoin @ (fsetadjoin @ esk36_0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ esk36_0 @ (fsetadjoin @ esk37_0 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ esk38_0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ esk38_0 @ (fsetadjoin @ esk39_0 @ femptyset)) @ femptyset))|p1)&(((esk38_0)=(esk39_0)|p1)&((esk37_0)!=(esk39_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])])])])])).
% 24.11/24.09 thf(c_0_43, plain, (p12|~p13), inference(fof_simplification,[status(thm)],[ax54])).
% 24.11/24.09 thf(c_0_44, plain, (p11|~p12), inference(split_conjunct,[status(thm)],[c_0_39])).
% 24.11/24.09 thf(c_0_45, plain, ~p11, inference(sr,[status(thm)],[c_0_40, c_0_41])).
% 24.11/24.09 thf(c_0_46, plain, (~fsetukpairinjR12|p9), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax9])])).
% 24.11/24.09 thf(c_0_47, plain, (fsetukpairinjR12|p1), inference(split_conjunct,[status(thm)],[c_0_42])).
% 24.11/24.09 thf(c_0_48, plain, (~fsecondinupair|p7), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax7])])).
% 24.11/24.09 thf(c_0_49, plain, (fsecondinupair|p1), inference(split_conjunct,[status(thm)],[c_0_42])).
% 24.11/24.09 thf(c_0_50, plain, (p13|~p14), inference(fof_simplification,[status(thm)],[ax53])).
% 24.11/24.09 thf(c_0_51, plain, (p12|~p13), inference(split_conjunct,[status(thm)],[c_0_43])).
% 24.11/24.09 thf(c_0_52, plain, ~p12, inference(sr,[status(thm)],[c_0_44, c_0_45])).
% 24.11/24.09 thf(c_0_53, plain, (~p4|~p9|p58), inference(fof_simplification,[status(thm)],[ax0])).
% 24.11/24.09 thf(c_0_54, plain, (p9|~fsetukpairinjR12), inference(split_conjunct,[status(thm)],[c_0_46])).
% 24.11/24.09 thf(c_0_55, plain, fsetukpairinjR12, inference(sr,[status(thm)],[c_0_47, c_0_32])).
% 24.11/24.09 thf(c_0_56, plain, (~funiqinunit|p5), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax5])])).
% 24.11/24.09 thf(c_0_57, plain, (funiqinunit|p1), inference(split_conjunct,[status(thm)],[c_0_42])).
% 24.11/24.09 thf(c_0_58, plain, (~p3|~p7|p50), inference(fof_simplification,[status(thm)],[ax10])).
% 24.11/24.09 thf(c_0_59, plain, (p7|~fsecondinupair), inference(split_conjunct,[status(thm)],[c_0_48])).
% 24.11/24.09 thf(c_0_60, plain, fsecondinupair, inference(sr,[status(thm)],[c_0_49, c_0_32])).
% 24.11/24.09 thf(c_0_61, plain, (((fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ f__2 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset)) @ femptyset))|p14)&(((f__2)=(f__3)|p14)&((f__1)!=(f__3)|p14))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax14])])])).
% 24.11/24.09 thf(c_0_62, plain, (p13|~p14), inference(split_conjunct,[status(thm)],[c_0_50])).
% 24.11/24.09 thf(c_0_63, plain, ~p13, inference(sr,[status(thm)],[c_0_51, c_0_52])).
% 24.11/24.09 thf(c_0_64, plain, ![X5:$i, X6:$i]:(~p58|((X5)!=(X6)|(fsetadjoin @ (fsetadjoin @ X5 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X5 @ (fsetadjoin @ X6 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ X5 @ femptyset) @ femptyset))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax58])])])).
% 24.11/24.09 thf(c_0_65, plain, (p58|~p4|~p9), inference(split_conjunct,[status(thm)],[c_0_53])).
% 24.11/24.09 thf(c_0_66, plain, p4, inference(split_conjunct,[status(thm)],[ax63])).
% 24.11/24.09 thf(c_0_67, plain, p9, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_54, c_0_55])])).
% 24.11/24.09 thf(c_0_68, plain, (~p2|~p5|p40), inference(fof_simplification,[status(thm)],[ax22])).
% 24.11/24.09 thf(c_0_69, plain, (p5|~funiqinunit), inference(split_conjunct,[status(thm)],[c_0_56])).
% 24.11/24.09 thf(c_0_70, plain, funiqinunit, inference(sr,[status(thm)],[c_0_57, c_0_32])).
% 24.11/24.09 thf(c_0_71, plain, (((fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ f__2 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__2 @ (fsetadjoin @ esk18_0 @ femptyset)) @ femptyset))|p13)&(((f__2)=(esk18_0)|p13)&((f__1)!=(esk18_0)|p13))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax13])])])])])).
% 24.11/24.09 thf(c_0_72, plain, ![X13:$i, X14:$i]:(~p50|fin @ X14 @ (fsetadjoin @ X13 @ (fsetadjoin @ X14 @ femptyset))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax50])])])).
% 24.11/24.09 thf(c_0_73, plain, (p50|~p3|~p7), inference(split_conjunct,[status(thm)],[c_0_58])).
% 24.11/24.09 thf(c_0_74, plain, p3, inference(split_conjunct,[status(thm)],[ax64])).
% 24.11/24.09 thf(c_0_75, plain, p7, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_59, c_0_60])])).
% 24.11/24.09 thf(c_0_76, plain, (~p15|(fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ f__2 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset)) @ femptyset))), inference(fof_nnf,[status(thm)],[pax15])).
% 24.11/24.09 thf(c_0_77, plain, ((f__2)=(f__3)|p14), inference(split_conjunct,[status(thm)],[c_0_61])).
% 24.11/24.09 thf(c_0_78, plain, ~p14, inference(sr,[status(thm)],[c_0_62, c_0_63])).
% 24.11/24.09 thf(c_0_79, plain, ![X1:$i, X2:$i]:((fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ femptyset)|~p58|(X1)!=(X2)), inference(split_conjunct,[status(thm)],[c_0_64])).
% 24.11/24.09 thf(c_0_80, plain, p58, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_65, c_0_66]), c_0_67])])).
% 24.11/24.09 thf(c_0_81, plain, (p14|p15), inference(split_conjunct,[status(thm)],[ax52])).
% 24.11/24.09 thf(c_0_82, plain, (~p40|p43), inference(fof_simplification,[status(thm)],[ax19])).
% 24.11/24.09 thf(c_0_83, plain, (p40|~p2|~p5), inference(split_conjunct,[status(thm)],[c_0_68])).
% 24.11/24.09 thf(c_0_84, plain, p2, inference(split_conjunct,[status(thm)],[ax65])).
% 24.11/24.09 thf(c_0_85, plain, p5, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_69, c_0_70])])).
% 24.11/24.09 thf(c_0_86, plain, ((f__2)=(esk18_0)|p13), inference(split_conjunct,[status(thm)],[c_0_71])).
% 24.11/24.09 thf(c_0_87, plain, ![X21:$i, X22:$i]:(~p40|(~fin @ X21 @ (fsetadjoin @ X22 @ femptyset)|(X21)=(X22))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax40])])])).
% 24.11/24.09 thf(c_0_88, plain, ![X2:$i, X1:$i]:(fin @ X1 @ (fsetadjoin @ X2 @ (fsetadjoin @ X1 @ femptyset))|~p50), inference(split_conjunct,[status(thm)],[c_0_72])).
% 24.11/24.09 thf(c_0_89, plain, p50, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_73, c_0_74]), c_0_75])])).
% 24.11/24.09 thf(c_0_90, plain, ((fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ f__2 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset)) @ femptyset))|~p15), inference(split_conjunct,[status(thm)],[c_0_76])).
% 24.11/24.09 thf(c_0_91, plain, (f__2)=(f__3), inference(sr,[status(thm)],[c_0_77, c_0_78])).
% 24.11/24.09 thf(c_0_92, plain, ![X1:$i]:(fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X1 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ femptyset), inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_79, c_0_80])])])).
% 24.11/24.09 thf(c_0_93, plain, p15, inference(sr,[status(thm)],[c_0_81, c_0_78])).
% 24.11/24.09 thf(c_0_94, plain, (~p43|p42), inference(fof_simplification,[status(thm)],[ax20])).
% 24.11/24.09 thf(c_0_95, plain, (p43|~p40), inference(split_conjunct,[status(thm)],[c_0_82])).
% 24.11/24.09 thf(c_0_96, plain, p40, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_83, c_0_84]), c_0_85])])).
% 24.11/24.09 thf(c_0_97, plain, (p13|(f__1)!=(esk18_0)), inference(split_conjunct,[status(thm)],[c_0_71])).
% 24.11/24.09 thf(c_0_98, plain, (esk18_0)=(f__2), inference(sr,[status(thm)],[c_0_86, c_0_63])).
% 24.11/24.09 thf(c_0_99, plain, ![X1:$i, X2:$i]:((X1)=(X2)|~p40|~fin @ X1 @ (fsetadjoin @ X2 @ femptyset)), inference(split_conjunct,[status(thm)],[c_0_87])).
% 24.11/24.09 thf(c_0_100, plain, ![X2:$i, X1:$i]:fin @ X1 @ (fsetadjoin @ X2 @ (fsetadjoin @ X1 @ femptyset)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_88, c_0_89])])).
% 24.11/24.09 thf(c_0_101, plain, (fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ f__3 @ femptyset) @ femptyset), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_90, c_0_91]), c_0_91]), c_0_92]), c_0_93])])).
% 24.11/24.09 thf(c_0_102, plain, (~p42|(~fin @ f__1 @ (fsetadjoin @ f__3 @ femptyset)|(f__1)=(f__3))), inference(fof_nnf,[status(thm)],[pax42])).
% 24.11/24.09 thf(c_0_103, plain, (p42|~p43), inference(split_conjunct,[status(thm)],[c_0_94])).
% 24.11/24.09 thf(c_0_104, plain, p43, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_95, c_0_96])])).
% 24.11/24.09 thf(c_0_105, plain, (f__1)!=(f__2), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_97, c_0_98]), c_0_63])).
% 24.11/24.09 thf(c_0_106, plain, ![X1:$i, X2:$i]:((X1)=(X2)|~fin @ X1 @ (fsetadjoin @ X2 @ femptyset)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_99, c_0_96])])).
% 24.11/24.09 thf(c_0_107, plain, fin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ (fsetadjoin @ (fsetadjoin @ f__3 @ femptyset) @ femptyset), inference(spm,[status(thm)],[c_0_100, c_0_101])).
% 24.11/24.09 thf(c_0_108, plain, ((f__1)=(f__3)|~p42|~fin @ f__1 @ (fsetadjoin @ f__3 @ femptyset)), inference(split_conjunct,[status(thm)],[c_0_102])).
% 24.11/24.09 thf(c_0_109, plain, p42, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_103, c_0_104])])).
% 24.11/24.09 thf(c_0_110, plain, (f__1)!=(f__3), inference(rw,[status(thm)],[c_0_105, c_0_91])).
% 24.11/24.09 thf(c_0_111, plain, (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))=(fsetadjoin @ f__3 @ femptyset), inference(spm,[status(thm)],[c_0_106, c_0_107])).
% 24.11/24.09 thf(c_0_112, plain, ~fin @ f__1 @ (fsetadjoin @ f__3 @ femptyset), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_108, c_0_109])]), c_0_110])).
% 24.11/24.09 thf(c_0_113, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_100, c_0_111]), c_0_112]), ['proof']).
% 24.11/24.09 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 24.11/24.09 thf(0,theorem,(uniqinunit => (secondinupair => (setukpairinjR12 => (![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset)) = ((setadjoin @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X3) @ ((setadjoin @ X4) @ emptyset))) @ emptyset))) => ((X3 = X4) => (X2 = X4)))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 24.11/24.09 % SZS output end Proof
%------------------------------------------------------------------------------