%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU807^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 : n001.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:51:13 PM UTC 2025
% Result : Theorem 24.11s 24.22s
% Output : Proof 24.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU807^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.12/0.34 % Computer : n001.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 8 21:46:38 EDT 2025
% 0.12/0.34 % CPUTime :
% 24.11/24.22 % SZS status Theorem
% 24.11/24.22 % Mode: mode371
% 24.11/24.22 % Inferences: 18410
% 24.11/24.22 % SZS output start Proof
% 24.11/24.22 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))))))))))))))).
% 24.11/24.22 thf(def_setadjoinIL,definition,(setadjoinIL = (![X1:$i]:(![X2:$i]:((in @ X1) @ ((setadjoin @ X1) @ X2)))))).
% 24.11/24.22 thf(def_setadjoinIR,definition,(setadjoinIR = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X2) => ((in @ X3) @ ((setadjoin @ X1) @ X2)))))))).
% 24.11/24.22 thf(def_in__Cong,definition,(in__Cong = (![X1:$i]:(![X2:$i]:((X1 = X2) => (![X3:$i]:(![X4:$i]:((X3 = X4) => (((in @ X3) @ X1) = ((in @ X4) @ X2)))))))))).
% 24.11/24.22 thf(def_upairset2E,definition,(upairset2E = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) => ((~((X3 = X1))) => (X3 = X2)))))))).
% 24.11/24.22 thf(notinself2,conjecture,(foundationAx => (setadjoinIL => (setadjoinIR => (in__Cong => (upairset2E => (![X1:$i]:(![X2:$i]:(((in @ X1) @ X2) => (~(((in @ X2) @ X1)))))))))))).
% 24.11/24.22 thf(h0,negated_conjecture,(~((foundationAx => (setadjoinIL => (setadjoinIR => (in__Cong => (upairset2E => (![X1:$i]:(![X2:$i]:(((in @ X1) @ X2) => (~(((in @ X2) @ X1))))))))))))),inference(assume_negation,[status(cth)],[notinself2])).
% 24.11/24.22 thf(nax1, axiom, (p1<=(ffoundationAx=>(fsetadjoinIL=>(fsetadjoinIR=>(fin__Cong=>(fupairset2E=>![X1:$i, X2:$i]:(fin @ X1 @ X2=>~(fin @ X2 @ X1)))))))), file('<stdin>', nax1)).
% 24.11/24.22 thf(ax147, axiom, ~(p1), file('<stdin>', ax147)).
% 24.11/24.22 thf(nax7, axiom, (p7<=ffoundationAx), file('<stdin>', nax7)).
% 24.11/24.22 thf(nax9, axiom, (p9<=fsetadjoinIL), file('<stdin>', nax9)).
% 24.11/24.22 thf(nax15, axiom, (p15<=fupairset2E), file('<stdin>', nax15)).
% 24.11/24.22 thf(ax119, axiom, (~(p2)|~(p7)|p27), file('<stdin>', ax119)).
% 24.11/24.22 thf(ax40, axiom, (~(p3)|~(p9)|p90), file('<stdin>', ax40)).
% 24.11/24.22 thf(ax4, axiom, (~(p6)|~(p15)|p120), file('<stdin>', ax4)).
% 24.11/24.22 thf(pax27, axiom, (p27=>![X1:$i]:(~(![X2:$i]:~(fin @ X2 @ X1))=>~(![X2:$i]:(fin @ X2 @ X1=>~(![X3:$i]:(fin @ X3 @ X2=>~(fin @ X3 @ X1))))))), file('<stdin>', pax27)).
% 24.11/24.22 thf(ax146, axiom, p2, file('<stdin>', ax146)).
% 24.11/24.22 thf(pax90, axiom, (p90=>![X1:$i, X2:$i]:fin @ X1 @ (fsetadjoin @ X1 @ X2)), file('<stdin>', pax90)).
% 24.11/24.22 thf(ax145, axiom, p3, file('<stdin>', ax145)).
% 24.11/24.22 thf(pax120, axiom, (p120=>![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset))=>(~((X3)=(X1))=>(X3)=(X2)))), file('<stdin>', pax120)).
% 24.11/24.22 thf(ax142, axiom, p6, file('<stdin>', ax142)).
% 24.11/24.22 thf(nax11, axiom, (p11<=fsetadjoinIR), file('<stdin>', nax11)).
% 24.11/24.22 thf(ax28, axiom, (~(p4)|~(p11)|p100), file('<stdin>', ax28)).
% 24.11/24.22 thf(pax100, axiom, (p100=>![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ X2=>fin @ X3 @ (fsetadjoin @ X1 @ X2))), file('<stdin>', pax100)).
% 24.11/24.22 thf(ax144, axiom, p4, file('<stdin>', ax144)).
% 24.11/24.22 thf(c_0_18, plain, ((ffoundationAx|p1)&((fsetadjoinIL|p1)&((fsetadjoinIR|p1)&((fin__Cong|p1)&((fupairset2E|p1)&((fin @ esk75_0 @ esk76_0|p1)&(fin @ esk76_0 @ esk75_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.22 thf(c_0_19, plain, ~p1, inference(fof_simplification,[status(thm)],[ax147])).
% 24.11/24.22 thf(c_0_20, plain, (~ffoundationAx|p7), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax7])])).
% 24.11/24.22 thf(c_0_21, plain, (ffoundationAx|p1), inference(split_conjunct,[status(thm)],[c_0_18])).
% 24.11/24.22 thf(c_0_22, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_19])).
% 24.11/24.22 thf(c_0_23, plain, (~fsetadjoinIL|p9), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax9])])).
% 24.11/24.22 thf(c_0_24, plain, (fsetadjoinIL|p1), inference(split_conjunct,[status(thm)],[c_0_18])).
% 24.11/24.22 thf(c_0_25, plain, (~fupairset2E|p15), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax15])])).
% 24.11/24.22 thf(c_0_26, plain, (fupairset2E|p1), inference(split_conjunct,[status(thm)],[c_0_18])).
% 24.11/24.22 thf(c_0_27, plain, (~p2|~p7|p27), inference(fof_simplification,[status(thm)],[ax119])).
% 24.11/24.22 thf(c_0_28, plain, (p7|~ffoundationAx), inference(split_conjunct,[status(thm)],[c_0_20])).
% 24.11/24.22 thf(c_0_29, plain, ffoundationAx, inference(sr,[status(thm)],[c_0_21, c_0_22])).
% 24.11/24.22 thf(c_0_30, plain, (~p3|~p9|p90), inference(fof_simplification,[status(thm)],[ax40])).
% 24.11/24.22 thf(c_0_31, plain, (p9|~fsetadjoinIL), inference(split_conjunct,[status(thm)],[c_0_23])).
% 24.11/24.22 thf(c_0_32, plain, fsetadjoinIL, inference(sr,[status(thm)],[c_0_24, c_0_22])).
% 24.11/24.22 thf(c_0_33, plain, (~p6|~p15|p120), inference(fof_simplification,[status(thm)],[ax4])).
% 24.11/24.22 thf(c_0_34, plain, (p15|~fupairset2E), inference(split_conjunct,[status(thm)],[c_0_25])).
% 24.11/24.22 thf(c_0_35, plain, fupairset2E, inference(sr,[status(thm)],[c_0_26, c_0_22])).
% 24.11/24.22 thf(c_0_36, plain, ![X122:$i, X123:$i, X125:$i]:((fin @ (esk60_1 @ X122) @ X122|~fin @ X123 @ X122|~p27)&(~fin @ X125 @ (esk60_1 @ X122)|~fin @ X125 @ X122|~fin @ X123 @ X122|~p27)), 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)],[pax27])])])])])])).
% 24.11/24.22 thf(c_0_37, plain, (p27|~p2|~p7), inference(split_conjunct,[status(thm)],[c_0_27])).
% 24.11/24.22 thf(c_0_38, plain, p2, inference(split_conjunct,[status(thm)],[ax146])).
% 24.11/24.22 thf(c_0_39, plain, p7, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_29])])).
% 24.11/24.22 thf(c_0_40, plain, ![X62:$i, X63:$i]:(~p90|fin @ X62 @ (fsetadjoin @ X62 @ X63)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax90])])])).
% 24.11/24.22 thf(c_0_41, plain, (p90|~p3|~p9), inference(split_conjunct,[status(thm)],[c_0_30])).
% 24.11/24.22 thf(c_0_42, plain, p3, inference(split_conjunct,[status(thm)],[ax145])).
% 24.11/24.22 thf(c_0_43, plain, p9, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32])])).
% 24.11/24.22 thf(c_0_44, plain, ![X26:$i, X27:$i, X28:$i]:(~p120|(~fin @ X28 @ (fsetadjoin @ X26 @ (fsetadjoin @ X27 @ femptyset))|((X28)=(X26)|(X28)=(X27)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax120])])])])).
% 24.11/24.22 thf(c_0_45, plain, (p120|~p6|~p15), inference(split_conjunct,[status(thm)],[c_0_33])).
% 24.11/24.22 thf(c_0_46, plain, p6, inference(split_conjunct,[status(thm)],[ax142])).
% 24.11/24.22 thf(c_0_47, plain, p15, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_34, c_0_35])])).
% 24.11/24.22 thf(c_0_48, plain, ![X2:$i, X1:$i]:(fin @ (esk60_1 @ X1) @ X1|~fin @ X2 @ X1|~p27), inference(split_conjunct,[status(thm)],[c_0_36])).
% 24.11/24.22 thf(c_0_49, plain, p27, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38]), c_0_39])])).
% 24.11/24.22 thf(c_0_50, plain, ![X1:$i, X2:$i]:(fin @ X1 @ (fsetadjoin @ X1 @ X2)|~p90), inference(split_conjunct,[status(thm)],[c_0_40])).
% 24.11/24.22 thf(c_0_51, plain, p90, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_42]), c_0_43])])).
% 24.11/24.22 thf(c_0_52, plain, ![X1:$i, X2:$i, X3:$i]:((X1)=(X2)|(X1)=(X3)|~p120|~fin @ X1 @ (fsetadjoin @ X2 @ (fsetadjoin @ X3 @ femptyset))), inference(split_conjunct,[status(thm)],[c_0_44])).
% 24.11/24.22 thf(c_0_53, plain, p120, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_46]), c_0_47])])).
% 24.11/24.22 thf(c_0_54, plain, ![X2:$i, X1:$i]:(fin @ (esk60_1 @ X1) @ X1|~fin @ X2 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_48, c_0_49])])).
% 24.11/24.22 thf(c_0_55, plain, ![X1:$i, X2:$i]:fin @ X1 @ (fsetadjoin @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_50, c_0_51])])).
% 24.11/24.22 thf(c_0_56, plain, ![X1:$i, X3:$i, X2:$i]:(~fin @ X1 @ (esk60_1 @ X2)|~fin @ X1 @ X2|~fin @ X3 @ X2|~p27), inference(split_conjunct,[status(thm)],[c_0_36])).
% 24.11/24.22 thf(c_0_57, 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_52, c_0_53])])).
% 24.11/24.22 thf(c_0_58, plain, ![X1:$i, X2:$i]:fin @ (esk60_1 @ (fsetadjoin @ X1 @ X2)) @ (fsetadjoin @ X1 @ X2), inference(spm,[status(thm)],[c_0_54, c_0_55])).
% 24.11/24.22 thf(c_0_59, plain, (~fsetadjoinIR|p11), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax11])])).
% 24.11/24.22 thf(c_0_60, plain, (fsetadjoinIR|p1), inference(split_conjunct,[status(thm)],[c_0_18])).
% 24.11/24.22 thf(c_0_61, plain, ![X1:$i, X3:$i, X2:$i]:(~fin @ X1 @ (esk60_1 @ X2)|~fin @ X3 @ X2|~fin @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_49])])).
% 24.11/24.22 thf(c_0_62, plain, ![X1:$i, X2:$i]:((esk60_1 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)))=(X1)|(esk60_1 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)))=(X2)), inference(spm,[status(thm)],[c_0_57, c_0_58])).
% 24.11/24.22 thf(c_0_63, plain, (~p4|~p11|p100), inference(fof_simplification,[status(thm)],[ax28])).
% 24.11/24.22 thf(c_0_64, plain, (p11|~fsetadjoinIR), inference(split_conjunct,[status(thm)],[c_0_59])).
% 24.11/24.22 thf(c_0_65, plain, fsetadjoinIR, inference(sr,[status(thm)],[c_0_60, c_0_22])).
% 24.11/24.22 thf(c_0_66, plain, ![X1:$i, X4:$i, X3:$i, X2:$i]:((esk60_1 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)))=(X1)|~fin @ X3 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset))|~fin @ X4 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset))|~fin @ X4 @ X2), inference(spm,[status(thm)],[c_0_61, c_0_62])).
% 24.11/24.22 thf(c_0_67, plain, ![X48:$i, X49:$i, X50:$i]:(~p100|(~fin @ X50 @ X49|fin @ X50 @ (fsetadjoin @ X48 @ X49))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax100])])])).
% 24.11/24.22 thf(c_0_68, plain, (p100|~p4|~p11), inference(split_conjunct,[status(thm)],[c_0_63])).
% 24.11/24.22 thf(c_0_69, plain, p4, inference(split_conjunct,[status(thm)],[ax144])).
% 24.11/24.22 thf(c_0_70, plain, p11, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_64, c_0_65])])).
% 24.11/24.22 thf(c_0_71, plain, ![X1:$i, X3:$i, X2:$i]:((esk60_1 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)))=(X1)|~fin @ X3 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset))|~fin @ X3 @ X2), inference(spm,[status(thm)],[c_0_66, c_0_58])).
% 24.11/24.22 thf(c_0_72, plain, ![X1:$i, X3:$i, X2:$i]:(fin @ X1 @ (fsetadjoin @ X3 @ X2)|~p100|~fin @ X1 @ X2), inference(split_conjunct,[status(thm)],[c_0_67])).
% 24.11/24.22 thf(c_0_73, plain, p100, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_69]), c_0_70])])).
% 24.11/24.22 thf(c_0_74, plain, ![X1:$i, X2:$i]:((esk60_1 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)))=(X1)|~fin @ X1 @ X2), inference(spm,[status(thm)],[c_0_71, c_0_55])).
% 24.11/24.22 thf(c_0_75, plain, ![X1:$i, X2:$i, X3:$i]:(fin @ X1 @ (fsetadjoin @ X2 @ X3)|~fin @ X1 @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_72, c_0_73])])).
% 24.11/24.22 thf(c_0_76, plain, ![X1:$i, X2:$i, X4:$i, X3:$i]:(~fin @ X1 @ (fsetadjoin @ X2 @ (fsetadjoin @ X3 @ femptyset))|~fin @ X4 @ (fsetadjoin @ X2 @ (fsetadjoin @ X3 @ femptyset))|~fin @ X4 @ X2|~fin @ X2 @ X3), inference(spm,[status(thm)],[c_0_61, c_0_74])).
% 24.11/24.22 thf(c_0_77, plain, ![X1:$i, X2:$i, X3:$i]:((X1)=(X2)|(X1)=(X3)|~fin @ X1 @ (fsetadjoin @ X3 @ femptyset)), inference(spm,[status(thm)],[c_0_57, c_0_75])).
% 24.11/24.22 thf(c_0_78, plain, ![X1:$i, X2:$i, X3:$i]:(~fin @ X1 @ (fsetadjoin @ X2 @ (fsetadjoin @ X3 @ femptyset))|~fin @ X1 @ X2|~fin @ X2 @ X3), inference(spm,[status(thm)],[c_0_76, c_0_58])).
% 24.11/24.22 thf(c_0_79, plain, ![X1:$i, X2:$i]:((esk60_1 @ (fsetadjoin @ X1 @ femptyset))=(X1)|(esk60_1 @ (fsetadjoin @ X1 @ femptyset))=(X2)), inference(spm,[status(thm)],[c_0_77, c_0_58])).
% 24.11/24.22 thf(c_0_80, plain, ![X1:$i, X3:$i, X2:$i]:(~fin @ X1 @ (fsetadjoin @ X2 @ femptyset)|~fin @ X1 @ X3|~fin @ X3 @ X2), inference(spm,[status(thm)],[c_0_78, c_0_75])).
% 24.11/24.22 thf(c_0_81, plain, ![X1:$i]:(esk60_1 @ (fsetadjoin @ X1 @ femptyset))=(X1), inference(er,[status(thm)],[inference(ef,[status(thm)],[c_0_79])])).
% 24.11/24.22 thf(c_0_82, plain, (fin @ esk75_0 @ esk76_0|p1), inference(split_conjunct,[status(thm)],[c_0_18])).
% 24.11/24.22 thf(c_0_83, plain, (fin @ esk76_0 @ esk75_0|p1), inference(split_conjunct,[status(thm)],[c_0_18])).
% 24.11/24.22 thf(c_0_84, plain, ![X2:$i, X1:$i]:(~fin @ X1 @ X2|~fin @ X2 @ X1), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_80, c_0_58]), c_0_81])).
% 24.11/24.22 thf(c_0_85, plain, fin @ esk75_0 @ esk76_0, inference(sr,[status(thm)],[c_0_82, c_0_22])).
% 24.11/24.22 thf(c_0_86, plain, fin @ esk76_0 @ esk75_0, inference(sr,[status(thm)],[c_0_83, c_0_22])).
% 24.11/24.22 thf(c_0_87, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84, c_0_85]), c_0_86])]), ['proof']).
% 24.11/24.22 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 24.11/24.22 thf(0,theorem,(foundationAx => (setadjoinIL => (setadjoinIR => (in__Cong => (upairset2E => (![X1:$i]:(![X2:$i]:(((in @ X1) @ X2) => (~(((in @ X2) @ X1))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 24.11/24.22 % SZS output end Proof
%------------------------------------------------------------------------------