%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU653^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 : n004.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:36 PM UTC 2025
% Result : Theorem 23.99s 24.01s
% Output : Proof 23.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SEU653^2 : TPTP v9.2.0. Released v3.7.0.
% 0.10/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.34 % Computer : n004.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed Oct 8 21:29:23 EDT 2025
% 0.14/0.34 % CPUTime :
% 23.99/24.01 % SZS status Theorem
% 23.99/24.01 % Mode: mode371
% 23.99/24.01 % Inferences: 4098
% 23.99/24.01 % SZS output start Proof
% 23.99/24.01 thf(def_secondinupair,definition,(secondinupair = (![X1:$i]:(![X2:$i]:((in @ X2) @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))))))).
% 23.99/24.01 thf(def_upairset2E,definition,(upairset2E = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) => ((~((X3 = X1))) => (X3 = X2)))))))).
% 23.99/24.01 thf(def_setukpairinjL2,definition,(setukpairinjL2 = (![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))) => (X1 = X3)))))))).
% 23.99/24.01 thf(def_setukpairinjR1,definition,(setukpairinjR1 = (![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))))))))).
% 23.99/24.01 thf(def_upairequniteq,definition,(upairequniteq = (![X1:$i]:(![X2:$i]:(![X3:$i]:((((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset)) = ((setadjoin @ X3) @ emptyset)) => (X1 = X2))))))).
% 23.99/24.01 thf(setukpairinjR2,conjecture,(secondinupair => (upairset2E => (setukpairinjL2 => (setukpairinjR1 => (upairequniteq => (![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))) => (X2 = X4)))))))))))).
% 23.99/24.01 thf(h0,negated_conjecture,(~((secondinupair => (upairset2E => (setukpairinjL2 => (setukpairinjR1 => (upairequniteq => (![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))) => (X2 = X4))))))))))))),inference(assume_negation,[status(cth)],[setukpairinjR2])).
% 23.99/24.01 thf(ax59, axiom, (p1|~(p8)), file('<stdin>', ax59)).
% 23.99/24.01 thf(ax66, axiom, ~(p1), file('<stdin>', ax66)).
% 23.99/24.01 thf(ax57, axiom, (p8|~(p10)), file('<stdin>', ax57)).
% 23.99/24.01 thf(ax55, axiom, (p10|~(p12)), file('<stdin>', ax55)).
% 23.99/24.01 thf(ax53, axiom, (p12|~(p14)), file('<stdin>', ax53)).
% 23.99/24.01 thf(ax51, axiom, (p14|~(p16)), file('<stdin>', ax51)).
% 23.99/24.01 thf(ax50, axiom, (p16|~(p17)), file('<stdin>', ax50)).
% 23.99/24.01 thf(nax1, axiom, (p1<=(fsecondinupair=>(fupairset2E=>(fsetukpairinjL2=>(fsetukpairinjR1=>(fupairequniteq=>![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))=>(X2)=(X4)))))))), file('<stdin>', nax1)).
% 23.99/24.01 thf(ax49, axiom, (p17|~(p18)), file('<stdin>', ax49)).
% 23.99/24.01 thf(nax11, axiom, (p11<=fsetukpairinjL2), file('<stdin>', nax11)).
% 23.99/24.01 thf(ax48, axiom, (p18|~(p19)), file('<stdin>', ax48)).
% 23.99/24.01 thf(ax3, axiom, (~(p4)|~(p11)|p56), file('<stdin>', ax3)).
% 23.99/24.01 thf(ax47, axiom, (p19|~(p20)), file('<stdin>', ax47)).
% 23.99/24.01 thf(pax56, axiom, (p56=>![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))=>(X1)=(X3))), file('<stdin>', pax56)).
% 23.99/24.01 thf(ax63, axiom, p4, file('<stdin>', ax63)).
% 23.99/24.01 thf(nax20, axiom, (p20<=((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__1)=(f__3))), file('<stdin>', nax20)).
% 23.99/24.01 thf(nax7, axiom, (p7<=fsecondinupair), file('<stdin>', nax7)).
% 23.99/24.01 thf(nax9, axiom, (p9<=fupairset2E), file('<stdin>', nax9)).
% 23.99/24.01 thf(ax23, axiom, (~(p2)|~(p7)|p40), file('<stdin>', ax23)).
% 23.99/24.01 thf(ax13, axiom, (~(p3)|~(p9)|p48), file('<stdin>', ax13)).
% 23.99/24.01 thf(nax19, axiom, (p19<=![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__1)=(X1))), file('<stdin>', nax19)).
% 23.99/24.01 thf(pax40, axiom, (p40=>![X1:$i, X2:$i]:fin @ X2 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset))), file('<stdin>', pax40)).
% 23.99/24.01 thf(ax65, axiom, p2, file('<stdin>', ax65)).
% 23.99/24.01 thf(pax48, axiom, (p48=>![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset))=>(~((X3)=(X1))=>(X3)=(X2)))), file('<stdin>', pax48)).
% 23.99/24.01 thf(ax64, axiom, p3, file('<stdin>', ax64)).
% 23.99/24.01 thf(c_0_25, plain, (p1|~p8), inference(fof_simplification,[status(thm)],[ax59])).
% 23.99/24.01 thf(c_0_26, plain, ~p1, inference(fof_simplification,[status(thm)],[ax66])).
% 23.99/24.01 thf(c_0_27, plain, (p8|~p10), inference(fof_simplification,[status(thm)],[ax57])).
% 23.99/24.01 thf(c_0_28, plain, (p1|~p8), inference(split_conjunct,[status(thm)],[c_0_25])).
% 23.99/24.01 thf(c_0_29, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_26])).
% 23.99/24.01 thf(c_0_30, plain, (p10|~p12), inference(fof_simplification,[status(thm)],[ax55])).
% 23.99/24.01 thf(c_0_31, plain, (p8|~p10), inference(split_conjunct,[status(thm)],[c_0_27])).
% 23.99/24.01 thf(c_0_32, plain, ~p8, inference(sr,[status(thm)],[c_0_28, c_0_29])).
% 23.99/24.01 thf(c_0_33, plain, (p12|~p14), inference(fof_simplification,[status(thm)],[ax53])).
% 23.99/24.01 thf(c_0_34, plain, (p10|~p12), inference(split_conjunct,[status(thm)],[c_0_30])).
% 23.99/24.01 thf(c_0_35, plain, ~p10, inference(sr,[status(thm)],[c_0_31, c_0_32])).
% 23.99/24.01 thf(c_0_36, plain, (p14|~p16), inference(fof_simplification,[status(thm)],[ax51])).
% 23.99/24.01 thf(c_0_37, plain, (p12|~p14), inference(split_conjunct,[status(thm)],[c_0_33])).
% 23.99/24.01 thf(c_0_38, plain, ~p12, inference(sr,[status(thm)],[c_0_34, c_0_35])).
% 23.99/24.01 thf(c_0_39, plain, (p16|~p17), inference(fof_simplification,[status(thm)],[ax50])).
% 23.99/24.01 thf(c_0_40, plain, (p14|~p16), inference(split_conjunct,[status(thm)],[c_0_36])).
% 23.99/24.01 thf(c_0_41, plain, ~p14, inference(sr,[status(thm)],[c_0_37, c_0_38])).
% 23.99/24.01 thf(c_0_42, plain, ((fsecondinupair|p1)&((fupairset2E|p1)&((fsetukpairinjL2|p1)&((fsetukpairinjR1|p1)&((fupairequniteq|p1)&(((fsetadjoin @ (fsetadjoin @ esk54_0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ esk54_0 @ (fsetadjoin @ esk55_0 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ esk56_0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ esk56_0 @ (fsetadjoin @ esk57_0 @ femptyset)) @ femptyset))|p1)&((esk55_0)!=(esk57_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])])])])])).
% 23.99/24.01 thf(c_0_43, plain, (p17|~p18), inference(fof_simplification,[status(thm)],[ax49])).
% 23.99/24.01 thf(c_0_44, plain, (p16|~p17), inference(split_conjunct,[status(thm)],[c_0_39])).
% 23.99/24.01 thf(c_0_45, plain, ~p16, inference(sr,[status(thm)],[c_0_40, c_0_41])).
% 23.99/24.01 thf(c_0_46, plain, (~fsetukpairinjL2|p11), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax11])])).
% 23.99/24.01 thf(c_0_47, plain, (fsetukpairinjL2|p1), inference(split_conjunct,[status(thm)],[c_0_42])).
% 23.99/24.01 thf(c_0_48, plain, (p18|~p19), inference(fof_simplification,[status(thm)],[ax48])).
% 23.99/24.01 thf(c_0_49, plain, (p17|~p18), inference(split_conjunct,[status(thm)],[c_0_43])).
% 23.99/24.01 thf(c_0_50, plain, ~p17, inference(sr,[status(thm)],[c_0_44, c_0_45])).
% 23.99/24.01 thf(c_0_51, plain, (~p4|~p11|p56), inference(fof_simplification,[status(thm)],[ax3])).
% 23.99/24.01 thf(c_0_52, plain, (p11|~fsetukpairinjL2), inference(split_conjunct,[status(thm)],[c_0_46])).
% 23.99/24.01 thf(c_0_53, plain, fsetukpairinjL2, inference(sr,[status(thm)],[c_0_47, c_0_29])).
% 23.99/24.01 thf(c_0_54, plain, (p19|~p20), inference(fof_simplification,[status(thm)],[ax47])).
% 23.99/24.01 thf(c_0_55, plain, (p18|~p19), inference(split_conjunct,[status(thm)],[c_0_48])).
% 23.99/24.01 thf(c_0_56, plain, ~p18, inference(sr,[status(thm)],[c_0_49, c_0_50])).
% 23.99/24.01 thf(c_0_57, plain, ![X17:$i, X18:$i, X19:$i, X20:$i]:(~p56|((fsetadjoin @ (fsetadjoin @ X17 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X17 @ (fsetadjoin @ X18 @ femptyset)) @ femptyset))!=(fsetadjoin @ (fsetadjoin @ X19 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X19 @ (fsetadjoin @ X20 @ femptyset)) @ femptyset))|(X17)=(X19))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax56])])])).
% 23.99/24.01 thf(c_0_58, plain, (p56|~p4|~p11), inference(split_conjunct,[status(thm)],[c_0_51])).
% 23.99/24.01 thf(c_0_59, plain, p4, inference(split_conjunct,[status(thm)],[ax63])).
% 23.99/24.01 thf(c_0_60, plain, p11, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_52, c_0_53])])).
% 23.99/24.01 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))|p20)&((f__1)!=(f__3)|p20)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax20])])])).
% 23.99/24.01 thf(c_0_62, plain, (p19|~p20), inference(split_conjunct,[status(thm)],[c_0_54])).
% 23.99/24.01 thf(c_0_63, plain, ~p19, inference(sr,[status(thm)],[c_0_55, c_0_56])).
% 23.99/24.01 thf(c_0_64, plain, (~fsecondinupair|p7), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax7])])).
% 23.99/24.01 thf(c_0_65, plain, (fsecondinupair|p1), inference(split_conjunct,[status(thm)],[c_0_42])).
% 23.99/24.01 thf(c_0_66, plain, (~fupairset2E|p9), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax9])])).
% 23.99/24.01 thf(c_0_67, plain, (fupairset2E|p1), inference(split_conjunct,[status(thm)],[c_0_42])).
% 23.99/24.01 thf(c_0_68, plain, ![X1:$i, X2:$i, X3:$i, X4:$i]:((X1)=(X3)|~p56|(fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset))!=(fsetadjoin @ (fsetadjoin @ X3 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X3 @ (fsetadjoin @ X4 @ femptyset)) @ femptyset))), inference(split_conjunct,[status(thm)],[c_0_57])).
% 23.99/24.01 thf(c_0_69, plain, p56, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_58, c_0_59]), c_0_60])])).
% 23.99/24.01 thf(c_0_70, 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))|p20), inference(split_conjunct,[status(thm)],[c_0_61])).
% 23.99/24.01 thf(c_0_71, plain, ~p20, inference(sr,[status(thm)],[c_0_62, c_0_63])).
% 23.99/24.01 thf(c_0_72, plain, (~p2|~p7|p40), inference(fof_simplification,[status(thm)],[ax23])).
% 23.99/24.01 thf(c_0_73, plain, (p7|~fsecondinupair), inference(split_conjunct,[status(thm)],[c_0_64])).
% 23.99/24.01 thf(c_0_74, plain, fsecondinupair, inference(sr,[status(thm)],[c_0_65, c_0_29])).
% 23.99/24.01 thf(c_0_75, plain, (~p3|~p9|p48), inference(fof_simplification,[status(thm)],[ax13])).
% 23.99/24.01 thf(c_0_76, plain, (p9|~fupairset2E), inference(split_conjunct,[status(thm)],[c_0_66])).
% 23.99/24.01 thf(c_0_77, plain, fupairset2E, inference(sr,[status(thm)],[c_0_67, c_0_29])).
% 23.99/24.01 thf(c_0_78, 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 @ esk28_0 @ femptyset)) @ femptyset))|p19)&((f__1)!=(esk28_0)|p19)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax19])])])])])).
% 23.99/24.01 thf(c_0_79, plain, ![X1:$i, X2:$i, X3:$i, X4:$i]:((X1)=(X2)|(fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X3 @ femptyset)) @ femptyset))!=(fsetadjoin @ (fsetadjoin @ X2 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X2 @ (fsetadjoin @ X4 @ femptyset)) @ femptyset))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_69])])).
% 23.99/24.01 thf(c_0_80, plain, (fsetadjoin @ (fsetadjoin @ f__2 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset)), inference(sr,[status(thm)],[c_0_70, c_0_71])).
% 23.99/24.01 thf(c_0_81, plain, ![X43:$i, X44:$i]:(~p40|fin @ X44 @ (fsetadjoin @ X43 @ (fsetadjoin @ X44 @ femptyset))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax40])])])).
% 23.99/24.01 thf(c_0_82, plain, (p40|~p2|~p7), inference(split_conjunct,[status(thm)],[c_0_72])).
% 23.99/24.01 thf(c_0_83, plain, p2, inference(split_conjunct,[status(thm)],[ax65])).
% 23.99/24.01 thf(c_0_84, plain, p7, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_73, c_0_74])])).
% 23.99/24.01 thf(c_0_85, plain, ![X33:$i, X34:$i, X35:$i]:(~p48|(~fin @ X35 @ (fsetadjoin @ X33 @ (fsetadjoin @ X34 @ femptyset))|((X35)=(X33)|(X35)=(X34)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax48])])])])).
% 23.99/24.01 thf(c_0_86, plain, (p48|~p3|~p9), inference(split_conjunct,[status(thm)],[c_0_75])).
% 23.99/24.01 thf(c_0_87, plain, p3, inference(split_conjunct,[status(thm)],[ax64])).
% 23.99/24.01 thf(c_0_88, plain, p9, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_76, c_0_77])])).
% 23.99/24.01 thf(c_0_89, 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 @ esk28_0 @ femptyset)) @ femptyset))|p19), inference(split_conjunct,[status(thm)],[c_0_78])).
% 23.99/24.01 thf(c_0_90, plain, ![X1:$i, X2:$i]:((X1)=(f__2)|(fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset))!=(fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset))), inference(spm,[status(thm)],[c_0_79, c_0_80])).
% 23.99/24.01 thf(c_0_91, plain, ![X2:$i, X1:$i]:(fin @ X1 @ (fsetadjoin @ X2 @ (fsetadjoin @ X1 @ femptyset))|~p40), inference(split_conjunct,[status(thm)],[c_0_81])).
% 23.99/24.01 thf(c_0_92, plain, p40, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_82, c_0_83]), c_0_84])])).
% 23.99/24.01 thf(c_0_93, plain, ![X1:$i, X2:$i, X3:$i]:((X1)=(X2)|(X1)=(X3)|~p48|~fin @ X1 @ (fsetadjoin @ X2 @ (fsetadjoin @ X3 @ femptyset))), inference(split_conjunct,[status(thm)],[c_0_85])).
% 23.99/24.01 thf(c_0_94, plain, p48, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_86, c_0_87]), c_0_88])])).
% 23.99/24.01 thf(c_0_95, plain, (fsetadjoin @ (fsetadjoin @ f__2 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__2 @ (fsetadjoin @ esk28_0 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset)), inference(sr,[status(thm)],[c_0_89, c_0_63])).
% 23.99/24.01 thf(c_0_96, plain, (f__2)=(f__0), inference(er,[status(thm)],[c_0_90])).
% 23.99/24.01 thf(c_0_97, plain, ![X2:$i, X1:$i]:fin @ X1 @ (fsetadjoin @ X2 @ (fsetadjoin @ X1 @ femptyset)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_91, c_0_92])])).
% 23.99/24.01 thf(c_0_98, 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_93, c_0_94])])).
% 23.99/24.01 thf(c_0_99, plain, (fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ esk28_0 @ femptyset)) @ femptyset))=(fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_95, c_0_96]), c_0_96])).
% 23.99/24.01 thf(c_0_100, plain, fin @ (fsetadjoin @ f__2 @ (fsetadjoin @ f__3 @ femptyset)) @ (fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset)), inference(spm,[status(thm)],[c_0_97, c_0_80])).
% 23.99/24.01 thf(c_0_101, plain, ![X1:$i]:((X1)=(fsetadjoin @ f__0 @ (fsetadjoin @ esk28_0 @ femptyset))|(X1)=(fsetadjoin @ f__0 @ femptyset)|~fin @ X1 @ (fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset))), inference(spm,[status(thm)],[c_0_98, c_0_99])).
% 23.99/24.01 thf(c_0_102, plain, fin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__3 @ femptyset)) @ (fsetadjoin @ (fsetadjoin @ f__0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset)) @ femptyset)), inference(rw,[status(thm)],[c_0_100, c_0_96])).
% 23.99/24.01 thf(c_0_103, plain, ((fsetadjoin @ f__0 @ (fsetadjoin @ esk28_0 @ femptyset))=(fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))|(fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))=(fsetadjoin @ f__0 @ femptyset)), inference(spm,[status(thm)],[c_0_101, c_0_97])).
% 23.99/24.01 thf(c_0_104, plain, (p19|(f__1)!=(esk28_0)), inference(split_conjunct,[status(thm)],[c_0_78])).
% 23.99/24.01 thf(c_0_105, plain, ((fsetadjoin @ f__0 @ (fsetadjoin @ f__3 @ femptyset))=(fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))|(fsetadjoin @ f__0 @ (fsetadjoin @ f__3 @ femptyset))=(fsetadjoin @ f__0 @ femptyset)), inference(spm,[status(thm)],[c_0_98, c_0_102])).
% 23.99/24.01 thf(c_0_106, plain, (p20|(f__1)!=(f__3)), inference(split_conjunct,[status(thm)],[c_0_61])).
% 23.99/24.01 thf(c_0_107, plain, ((fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))=(fsetadjoin @ f__0 @ femptyset)|fin @ esk28_0 @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))), inference(spm,[status(thm)],[c_0_97, c_0_103])).
% 23.99/24.01 thf(c_0_108, plain, (esk28_0)!=(f__1), inference(sr,[status(thm)],[c_0_104, c_0_63])).
% 23.99/24.01 thf(c_0_109, plain, ((fsetadjoin @ f__0 @ (fsetadjoin @ f__3 @ femptyset))=(fsetadjoin @ f__0 @ femptyset)|fin @ f__3 @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))), inference(spm,[status(thm)],[c_0_97, c_0_105])).
% 23.99/24.01 thf(c_0_110, plain, (f__3)!=(f__1), inference(sr,[status(thm)],[c_0_106, c_0_71])).
% 23.99/24.01 thf(c_0_111, plain, ((fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))=(fsetadjoin @ f__0 @ femptyset)|(esk28_0)=(f__0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_98, c_0_107]), c_0_108])).
% 23.99/24.01 thf(c_0_112, plain, ((fsetadjoin @ f__0 @ (fsetadjoin @ f__3 @ femptyset))=(fsetadjoin @ f__0 @ femptyset)|(f__3)=(f__0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_98, c_0_109]), c_0_110])).
% 23.99/24.01 thf(c_0_113, plain, ![X1:$i]:((fsetadjoin @ f__0 @ (fsetadjoin @ f__3 @ femptyset))=(fsetadjoin @ f__0 @ femptyset)|(X1)=(f__0)|(X1)=(f__3)|~fin @ X1 @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))), inference(spm,[status(thm)],[c_0_98, c_0_105])).
% 23.99/24.01 thf(c_0_114, plain, ![X1:$i]:((esk28_0)=(f__0)|(X1)=(f__0)|(X1)=(f__1)|~fin @ X1 @ (fsetadjoin @ f__0 @ femptyset)), inference(spm,[status(thm)],[c_0_98, c_0_111])).
% 23.99/24.01 thf(c_0_115, plain, ((f__3)=(f__0)|fin @ f__3 @ (fsetadjoin @ f__0 @ femptyset)), inference(spm,[status(thm)],[c_0_97, c_0_112])).
% 23.99/24.01 thf(c_0_116, plain, ((fsetadjoin @ f__0 @ (fsetadjoin @ f__3 @ femptyset))=(fsetadjoin @ f__0 @ femptyset)|(f__1)=(f__0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_113, c_0_97]), c_0_110])).
% 23.99/24.01 thf(c_0_117, plain, ((f__3)=(f__0)|(esk28_0)=(f__0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_114, c_0_115]), c_0_110])).
% 23.99/24.01 thf(c_0_118, plain, ![X1:$i]:((f__1)=(f__0)|(X1)=(f__0)|(X1)=(f__3)|~fin @ X1 @ (fsetadjoin @ f__0 @ femptyset)), inference(spm,[status(thm)],[c_0_98, c_0_116])).
% 23.99/24.01 thf(c_0_119, plain, ((esk28_0)=(f__0)|fin @ f__1 @ (fsetadjoin @ f__0 @ femptyset)), inference(spm,[status(thm)],[c_0_97, c_0_111])).
% 23.99/24.01 thf(c_0_120, plain, ((f__3)=(f__0)|(f__1)!=(f__0)), inference(spm,[status(thm)],[c_0_108, c_0_117])).
% 23.99/24.01 thf(c_0_121, plain, ((esk28_0)=(f__0)|(f__1)=(f__0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_118, c_0_119]), c_0_110])).
% 23.99/24.01 thf(c_0_122, plain, (f__1)!=(f__0), inference(spm,[status(thm)],[c_0_110, c_0_120])).
% 23.99/24.01 thf(c_0_123, plain, (esk28_0)=(f__0), inference(sr,[status(thm)],[c_0_121, c_0_122])).
% 23.99/24.01 thf(c_0_124, plain, ((fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))=(fsetadjoin @ f__0 @ (fsetadjoin @ f__0 @ femptyset))|(fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))=(fsetadjoin @ f__0 @ femptyset)), inference(rw,[status(thm)],[c_0_103, c_0_123])).
% 23.99/24.01 thf(c_0_125, plain, ((fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))=(fsetadjoin @ f__0 @ femptyset)|fin @ f__1 @ (fsetadjoin @ f__0 @ (fsetadjoin @ f__0 @ femptyset))), inference(spm,[status(thm)],[c_0_97, c_0_124])).
% 23.99/24.01 thf(c_0_126, plain, (fsetadjoin @ f__0 @ (fsetadjoin @ f__3 @ femptyset))=(fsetadjoin @ f__0 @ femptyset), inference(sr,[status(thm)],[c_0_116, c_0_122])).
% 23.99/24.01 thf(c_0_127, plain, (fsetadjoin @ f__0 @ (fsetadjoin @ f__1 @ femptyset))=(fsetadjoin @ f__0 @ femptyset), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_98, c_0_125]), c_0_122])).
% 23.99/24.01 thf(c_0_128, plain, ![X1:$i]:((X1)=(f__0)|(X1)=(f__3)|~fin @ X1 @ (fsetadjoin @ f__0 @ femptyset)), inference(spm,[status(thm)],[c_0_98, c_0_126])).
% 23.99/24.01 thf(c_0_129, plain, fin @ f__1 @ (fsetadjoin @ f__0 @ femptyset), inference(spm,[status(thm)],[c_0_97, c_0_127])).
% 23.99/24.01 thf(c_0_130, plain, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_128, c_0_129]), c_0_122]), c_0_110]), ['proof']).
% 23.99/24.01 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 23.99/24.01 thf(0,theorem,(secondinupair => (upairset2E => (setukpairinjL2 => (setukpairinjR1 => (upairequniteq => (![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))) => (X2 = X4))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 23.99/24.01 % SZS output end Proof
%------------------------------------------------------------------------------