%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU657^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:42 PM UTC 2025
% Result : Theorem 1.59s 1.78s
% Output : Proof 1.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU657^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 : n004.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 :
% 1.59/1.78 % SZS status Theorem
% 1.59/1.78 % Mode: mode506
% 1.59/1.78 % Inferences: 38908
% 1.59/1.78 % SZS output start Proof
% 1.59/1.78 thf(def_iskpair,definition,(iskpair = (^[X1:$i]:(~((![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$i]:(((in @ X3) @ (setunion @ X1)) => (~((X1 = ((setadjoin @ ((setadjoin @ X2) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X2) @ ((setadjoin @ X3) @ emptyset))) @ emptyset)))))))))))))).
% 1.59/1.78 thf(def_kpair,definition,(kpair = (^[X1:$i]:(^[X2:$i]:((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset)))))).
% 1.59/1.78 thf(def_kfstpairEq,definition,(kfstpairEq = (![X1:$i]:(![X2:$i]:((kfst @ ((kpair @ X1) @ X2)) = X1))))).
% 1.59/1.78 thf(def_ksndpairEq,definition,(ksndpairEq = (![X1:$i]:(![X2:$i]:((ksnd @ ((kpair @ X1) @ X2)) = X2))))).
% 1.59/1.78 thf(kpairsurjEq,conjecture,((![X1:$i]:(![X2:$i]:((kfst @ ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))) = X1))) => ((![X1:$i]:(![X2:$i]:((ksnd @ ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))) = X2))) => (![X1:$i]:((~((![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$i]:(((in @ X3) @ (setunion @ X1)) => (~((X1 = ((setadjoin @ ((setadjoin @ X2) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X2) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))))))))) => (((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ (ksnd @ X1)) @ emptyset))) @ emptyset)) = X1)))))).
% 1.59/1.78 thf(h0,negated_conjecture,(~(((![X1:$i]:(![X2:$i]:((kfst @ ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))) = X1))) => ((![X1:$i]:(![X2:$i]:((ksnd @ ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))) = X2))) => (![X1:$i]:((~((![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$i]:(((in @ X3) @ (setunion @ X1)) => (~((X1 = ((setadjoin @ ((setadjoin @ X2) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X2) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))))))))) => (((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ (ksnd @ X1)) @ emptyset))) @ emptyset)) = X1))))))),inference(assume_negation,[status(cth)],[kpairsurjEq])).
% 1.59/1.78 thf(ax1030, axiom, (p1|~(p3)), file('<stdin>', ax1030)).
% 1.59/1.78 thf(ax1032, axiom, ~(p1), file('<stdin>', ax1032)).
% 1.59/1.78 thf(ax1028, axiom, (p3|~(p5)), file('<stdin>', ax1028)).
% 1.59/1.78 thf(ax1020, axiom, (~(p10)|p13), file('<stdin>', ax1020)).
% 1.59/1.78 thf(ax1027, axiom, (p5|~(p6)), file('<stdin>', ax1027)).
% 1.59/1.78 thf(ax637, axiom, (~(p130)|p390), file('<stdin>', ax637)).
% 1.59/1.78 thf(ax1019, axiom, (~(p13)|p14), file('<stdin>', ax1019)).
% 1.59/1.78 thf(ax1024, axiom, p10, file('<stdin>', ax1024)).
% 1.59/1.78 thf(ax1025, axiom, (p6|~(p8)), file('<stdin>', ax1025)).
% 1.59/1.78 thf(ax175, axiom, (~(p390)|p850), file('<stdin>', ax175)).
% 1.59/1.78 thf(ax898, axiom, p130, file('<stdin>', ax898)).
% 1.59/1.78 thf(ax1018, axiom, (~(p14)|~(p9)|p8), file('<stdin>', ax1018)).
% 1.59/1.78 thf(ax174, axiom, (~(p850)|p9|p849), file('<stdin>', ax174)).
% 1.59/1.78 thf(pax2, axiom, (p2=>![X1:$i, X2:$i]:(fkfst @ (fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset)))=(X1)), file('<stdin>', pax2)).
% 1.59/1.78 thf(ax1031, axiom, (p1|p2), file('<stdin>', ax1031)).
% 1.59/1.78 thf(nax6, axiom, (p6<=(~(![X1:$i]:(fin @ X1 @ (fsetunion @ f__0)=>![X2:$i]:(fin @ X2 @ (fsetunion @ f__0)=>~((f__0)=(fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset))))))=>(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ (fksnd @ f__0) @ femptyset)) @ femptyset))=(f__0))), file('<stdin>', nax6)).
% 1.59/1.78 thf(pax4, axiom, (p4=>![X1:$i, X2:$i]:(fksnd @ (fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset)))=(X2)), file('<stdin>', pax4)).
% 1.59/1.78 thf(ax1029, axiom, (p3|p4), file('<stdin>', ax1029)).
% 1.59/1.78 thf(pax849, axiom, (p849=>![X1:$i]:((X1)=(fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ (fksnd @ f__0) @ femptyset))=>~((f__0)=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ X1 @ femptyset))))), file('<stdin>', pax849)).
% 1.59/1.78 thf(c_0_19, plain, (p1|~p3), inference(fof_simplification,[status(thm)],[ax1030])).
% 1.59/1.78 thf(c_0_20, plain, ~p1, inference(fof_simplification,[status(thm)],[ax1032])).
% 1.59/1.78 thf(c_0_21, plain, (p3|~p5), inference(fof_simplification,[status(thm)],[ax1028])).
% 1.59/1.78 thf(c_0_22, plain, (p1|~p3), inference(split_conjunct,[status(thm)],[c_0_19])).
% 1.59/1.78 thf(c_0_23, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_20])).
% 1.59/1.78 thf(c_0_24, plain, (~p10|p13), inference(fof_simplification,[status(thm)],[ax1020])).
% 1.59/1.78 thf(c_0_25, plain, (p5|~p6), inference(fof_simplification,[status(thm)],[ax1027])).
% 1.59/1.78 thf(c_0_26, plain, (p3|~p5), inference(split_conjunct,[status(thm)],[c_0_21])).
% 1.59/1.78 thf(c_0_27, plain, ~p3, inference(sr,[status(thm)],[c_0_22, c_0_23])).
% 1.59/1.78 thf(c_0_28, plain, (~p130|p390), inference(fof_simplification,[status(thm)],[ax637])).
% 1.59/1.78 thf(c_0_29, plain, (~p13|p14), inference(fof_simplification,[status(thm)],[ax1019])).
% 1.59/1.78 thf(c_0_30, plain, (p13|~p10), inference(split_conjunct,[status(thm)],[c_0_24])).
% 1.59/1.78 thf(c_0_31, plain, p10, inference(split_conjunct,[status(thm)],[ax1024])).
% 1.59/1.78 thf(c_0_32, plain, (p6|~p8), inference(fof_simplification,[status(thm)],[ax1025])).
% 1.59/1.78 thf(c_0_33, plain, (p5|~p6), inference(split_conjunct,[status(thm)],[c_0_25])).
% 1.59/1.78 thf(c_0_34, plain, ~p5, inference(sr,[status(thm)],[c_0_26, c_0_27])).
% 1.59/1.78 thf(c_0_35, plain, (~p390|p850), inference(fof_simplification,[status(thm)],[ax175])).
% 1.59/1.78 thf(c_0_36, plain, (p390|~p130), inference(split_conjunct,[status(thm)],[c_0_28])).
% 1.59/1.78 thf(c_0_37, plain, p130, inference(split_conjunct,[status(thm)],[ax898])).
% 1.59/1.78 thf(c_0_38, plain, (~p14|~p9|p8), inference(fof_simplification,[status(thm)],[ax1018])).
% 1.59/1.78 thf(c_0_39, plain, (p14|~p13), inference(split_conjunct,[status(thm)],[c_0_29])).
% 1.59/1.78 thf(c_0_40, plain, p13, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31])])).
% 1.59/1.78 thf(c_0_41, plain, (p6|~p8), inference(split_conjunct,[status(thm)],[c_0_32])).
% 1.59/1.78 thf(c_0_42, plain, ~p6, inference(sr,[status(thm)],[c_0_33, c_0_34])).
% 1.59/1.78 thf(c_0_43, plain, (~p850|p9|p849), inference(fof_simplification,[status(thm)],[ax174])).
% 1.59/1.78 thf(c_0_44, plain, (p850|~p390), inference(split_conjunct,[status(thm)],[c_0_35])).
% 1.59/1.78 thf(c_0_45, plain, p390, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_36, c_0_37])])).
% 1.59/1.78 thf(c_0_46, plain, (p8|~p14|~p9), inference(split_conjunct,[status(thm)],[c_0_38])).
% 1.59/1.78 thf(c_0_47, plain, p14, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_40])])).
% 1.59/1.78 thf(c_0_48, plain, ~p8, inference(sr,[status(thm)],[c_0_41, c_0_42])).
% 1.59/1.78 thf(c_0_49, plain, ![X2548:$i, X2549:$i]:(~p2|(fkfst @ (fsetadjoin @ (fsetadjoin @ X2548 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X2548 @ (fsetadjoin @ X2549 @ femptyset)) @ femptyset)))=(X2548)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax2])])])).
% 1.59/1.78 thf(c_0_50, plain, (p1|p2), inference(split_conjunct,[status(thm)],[ax1031])).
% 1.59/1.78 thf(c_0_51, plain, (((fin @ esk1261_0 @ (fsetunion @ f__0)|p6)&((fin @ esk1262_0 @ (fsetunion @ f__0)|p6)&((f__0)=(fsetadjoin @ (fsetadjoin @ esk1261_0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ esk1261_0 @ (fsetadjoin @ esk1262_0 @ femptyset)) @ femptyset))|p6)))&((fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ (fksnd @ f__0) @ femptyset)) @ femptyset))!=(f__0)|p6)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax6])])])])])).
% 1.59/1.78 thf(c_0_52, plain, ![X2534:$i, X2535:$i]:(~p4|(fksnd @ (fsetadjoin @ (fsetadjoin @ X2534 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X2534 @ (fsetadjoin @ X2535 @ femptyset)) @ femptyset)))=(X2535)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax4])])])).
% 1.59/1.78 thf(c_0_53, plain, (p3|p4), inference(split_conjunct,[status(thm)],[ax1029])).
% 1.59/1.78 thf(c_0_54, plain, ![X178:$i]:(~p849|((X178)!=(fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ (fksnd @ f__0) @ femptyset))|(f__0)!=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ X178 @ femptyset)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax849])])])])).
% 1.59/1.78 thf(c_0_55, plain, (p9|p849|~p850), inference(split_conjunct,[status(thm)],[c_0_43])).
% 1.59/1.78 thf(c_0_56, plain, p850, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_44, c_0_45])])).
% 1.59/1.78 thf(c_0_57, plain, ~p9, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_47])]), c_0_48])).
% 1.59/1.78 thf(c_0_58, plain, ![X2:$i, X1:$i]:((fkfst @ (fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset)))=(X1)|~p2), inference(split_conjunct,[status(thm)],[c_0_49])).
% 1.59/1.78 thf(c_0_59, plain, p2, inference(sr,[status(thm)],[c_0_50, c_0_23])).
% 1.59/1.78 thf(c_0_60, plain, ((f__0)=(fsetadjoin @ (fsetadjoin @ esk1261_0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ esk1261_0 @ (fsetadjoin @ esk1262_0 @ femptyset)) @ femptyset))|p6), inference(split_conjunct,[status(thm)],[c_0_51])).
% 1.59/1.78 thf(c_0_61, plain, ![X1:$i, X2:$i]:((fksnd @ (fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset)))=(X2)|~p4), inference(split_conjunct,[status(thm)],[c_0_52])).
% 1.59/1.78 thf(c_0_62, plain, p4, inference(sr,[status(thm)],[c_0_53, c_0_27])).
% 1.59/1.78 thf(c_0_63, plain, ![X1:$i]:(~p849|(X1)!=(fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ (fksnd @ f__0) @ femptyset))|(f__0)!=(fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ X1 @ femptyset))), inference(split_conjunct,[status(thm)],[c_0_54])).
% 1.59/1.78 thf(c_0_64, plain, p849, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_55, c_0_56])]), c_0_57])).
% 1.59/1.78 thf(c_0_65, plain, ![X2:$i, X1:$i]:(fkfst @ (fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset)))=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_58, c_0_59])])).
% 1.59/1.78 thf(c_0_66, plain, (fsetadjoin @ (fsetadjoin @ esk1261_0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ esk1261_0 @ (fsetadjoin @ esk1262_0 @ femptyset)) @ femptyset))=(f__0), inference(sr,[status(thm)],[c_0_60, c_0_42])).
% 1.59/1.78 thf(c_0_67, plain, ![X1:$i, X2:$i]:(fksnd @ (fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset)))=(X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_61, c_0_62])])).
% 1.59/1.78 thf(c_0_68, plain, (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ femptyset) @ (fsetadjoin @ (fsetadjoin @ (fkfst @ f__0) @ (fsetadjoin @ (fksnd @ f__0) @ femptyset)) @ femptyset))!=(f__0), inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63, c_0_64])])])).
% 1.59/1.78 thf(c_0_69, plain, (fkfst @ f__0)=(esk1261_0), inference(spm,[status(thm)],[c_0_65, c_0_66])).
% 1.59/1.78 thf(c_0_70, plain, (fksnd @ f__0)=(esk1262_0), inference(spm,[status(thm)],[c_0_67, c_0_66])).
% 1.59/1.78 thf(c_0_71, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_69]), c_0_69]), c_0_70]), c_0_66])]), ['proof']).
% 1.59/1.78 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 1.59/1.78 thf(0,theorem,((![X1:$i]:(![X2:$i]:((kfst @ ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))) = X1))) => ((![X1:$i]:(![X2:$i]:((ksnd @ ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))) = X2))) => (![X1:$i]:((~((![X2:$i]:(((in @ X2) @ (setunion @ X1)) => (![X3:$i]:(((in @ X3) @ (setunion @ X1)) => (~((X1 = ((setadjoin @ ((setadjoin @ X2) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X2) @ ((setadjoin @ X3) @ emptyset))) @ emptyset))))))))))) => (((setadjoin @ ((setadjoin @ (kfst @ X1)) @ emptyset)) @ ((setadjoin @ ((setadjoin @ (kfst @ X1)) @ ((setadjoin @ (ksnd @ X1)) @ emptyset))) @ emptyset)) = X1))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 1.59/1.78 % SZS output end Proof
%------------------------------------------------------------------------------