%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU642^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 : n005.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:26 PM UTC 2025
% Result : Theorem 20.10s 19.87s
% Output : Proof 20.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SEU642^2 : TPTP v9.2.0. Released v3.7.0.
% 0.10/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.33 % Computer : n005.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Oct 8 20:38:23 EDT 2025
% 0.12/0.34 % CPUTime :
% 4.81/4.53 slave returned with unknown status
% 20.10/19.87 % SZS status Theorem
% 20.10/19.87 % Mode: mode485
% 20.10/19.87 % Inferences: 35
% 20.10/19.87 % SZS output start Proof
% 20.10/19.87 thf(def_setadjoinIL,definition,(setadjoinIL = (![X1:$i]:(![X2:$i]:((in @ X1) @ ((setadjoin @ X1) @ X2)))))).
% 20.10/19.87 thf(def_uniqinunit,definition,(uniqinunit = (![X1:$i]:(![X2:$i]:(((in @ X1) @ ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))))).
% 20.10/19.87 thf(def_upairset2E,definition,(upairset2E = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) => ((~((X3 = X1))) => (X3 = X2)))))))).
% 20.10/19.87 thf(def_singletonsuniq,definition,(singletonsuniq = (![X1:$i]:(![X2:$i]:((((setadjoin @ X1) @ emptyset) = ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))))).
% 20.10/19.87 thf(setukpairinjL1,conjecture,((![X1:$i]:(![X2:$i]:((in @ X1) @ ((setadjoin @ X1) @ X2)))) => ((![X1:$i]:(![X2:$i]:(((in @ X1) @ ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))) => ((![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) => ((~((X3 = X1))) => (X3 = X2)))))) => ((![X1:$i]:(![X2:$i]:((((setadjoin @ X1) @ emptyset) = ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))) => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))) => (X1 = X3)))))))))).
% 20.10/19.87 thf(h0,negated_conjecture,(~(((![X1:$i]:(![X2:$i]:((in @ X1) @ ((setadjoin @ X1) @ X2)))) => ((![X1:$i]:(![X2:$i]:(((in @ X1) @ ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))) => ((![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) => ((~((X3 = X1))) => (X3 = X2)))))) => ((![X1:$i]:(![X2:$i]:((((setadjoin @ X1) @ emptyset) = ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))) => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))) => (X1 = X3))))))))))),inference(assume_negation,[status(cth)],[setukpairinjL1])).
% 20.10/19.87 thf(ax1378, axiom, (p1|~(p3)), file('<stdin>', ax1378)).
% 20.10/19.87 thf(ax1380, axiom, ~(p1), file('<stdin>', ax1380)).
% 20.10/19.87 thf(ax1376, axiom, (p3|~(p5)), file('<stdin>', ax1376)).
% 20.10/19.87 thf(pax10, axiom, (p10=>![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset))=>(~((X3)=(X1))=>(X3)=(X2)))), file('<stdin>', pax10)).
% 20.10/19.87 thf(ax1371, axiom, (p5|p10), file('<stdin>', ax1371)).
% 20.10/19.87 thf(nax1, axiom, (p1<=(![X1:$i, X2:$i]:fin @ X1 @ (fsetadjoin @ X1 @ X2)=>(![X1:$i, X2:$i]:(fin @ X1 @ (fsetadjoin @ X2 @ femptyset)=>(X1)=(X2))=>(![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset))=>(~((X3)=(X1))=>(X3)=(X2)))=>(![X1:$i, X2:$i]:((fsetadjoin @ X1 @ femptyset)=(fsetadjoin @ X2 @ femptyset)=>(X1)=(X2))=>![X1:$i, X2:$i, X3:$i]:(fin @ (fsetadjoin @ X3 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ X1 @ (fsetadjoin @ X2 @ femptyset)) @ femptyset))=>(X1)=(X3))))))), file('<stdin>', nax1)).
% 20.10/19.87 thf(pax2, axiom, (p2=>![X1:$i, X2:$i]:fin @ X1 @ (fsetadjoin @ X1 @ X2)), file('<stdin>', pax2)).
% 20.10/19.87 thf(ax1379, axiom, (p1|p2), file('<stdin>', ax1379)).
% 20.10/19.87 thf(pax4, axiom, (p4=>![X1:$i, X2:$i]:(fin @ X1 @ (fsetadjoin @ X2 @ femptyset)=>(X1)=(X2))), file('<stdin>', pax4)).
% 20.10/19.87 thf(ax1377, axiom, (p3|p4), file('<stdin>', ax1377)).
% 20.10/19.87 thf(c_0_10, plain, (p1|~p3), inference(fof_simplification,[status(thm)],[ax1378])).
% 20.10/19.87 thf(c_0_11, plain, ~p1, inference(fof_simplification,[status(thm)],[ax1380])).
% 20.10/19.87 thf(c_0_12, plain, (p3|~p5), inference(fof_simplification,[status(thm)],[ax1376])).
% 20.10/19.87 thf(c_0_13, plain, (p1|~p3), inference(split_conjunct,[status(thm)],[c_0_10])).
% 20.10/19.87 thf(c_0_14, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_11])).
% 20.10/19.87 thf(c_0_15, plain, (p3|~p5), inference(split_conjunct,[status(thm)],[c_0_12])).
% 20.10/19.87 thf(c_0_16, plain, ~p3, inference(sr,[status(thm)],[c_0_13, c_0_14])).
% 20.10/19.87 thf(c_0_17, plain, ![X6387:$i, X6388:$i, X6389:$i]:(~p10|(~fin @ X6389 @ (fsetadjoin @ X6387 @ (fsetadjoin @ X6388 @ femptyset))|((X6389)=(X6387)|(X6389)=(X6388)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax10])])])])).
% 20.10/19.87 thf(c_0_18, plain, (p5|p10), inference(split_conjunct,[status(thm)],[ax1371])).
% 20.10/19.87 thf(c_0_19, plain, ~p5, inference(sr,[status(thm)],[c_0_15, c_0_16])).
% 20.10/19.87 thf(c_0_20, plain, ![X6457:$i, X6458:$i, X6459:$i, X6460:$i, X6461:$i, X6462:$i, X6463:$i, X6464:$i, X6465:$i]:((fin @ X6457 @ (fsetadjoin @ X6457 @ X6458)|p1)&((~fin @ X6459 @ (fsetadjoin @ X6460 @ femptyset)|(X6459)=(X6460)|p1)&((~fin @ X6463 @ (fsetadjoin @ X6461 @ (fsetadjoin @ X6462 @ femptyset))|((X6463)=(X6461)|(X6463)=(X6462))|p1)&(((fsetadjoin @ X6464 @ femptyset)!=(fsetadjoin @ X6465 @ femptyset)|(X6464)=(X6465)|p1)&((fin @ (fsetadjoin @ esk3232_0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ esk3230_0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ esk3230_0 @ (fsetadjoin @ esk3231_0 @ femptyset)) @ femptyset))|p1)&((esk3230_0)!=(esk3232_0)|p1)))))), 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)],[nax1])])])])])])).
% 20.10/19.87 thf(c_0_21, plain, ![X6441:$i, X6442:$i]:(~p2|fin @ X6441 @ (fsetadjoin @ X6441 @ X6442)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax2])])])).
% 20.10/19.87 thf(c_0_22, plain, (p1|p2), inference(split_conjunct,[status(thm)],[ax1379])).
% 20.10/19.87 thf(c_0_23, plain, ![X1:$i, X2:$i, X3:$i]:((X1)=(X2)|(X1)=(X3)|~p10|~fin @ X1 @ (fsetadjoin @ X2 @ (fsetadjoin @ X3 @ femptyset))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 20.10/19.87 thf(c_0_24, plain, p10, inference(sr,[status(thm)],[c_0_18, c_0_19])).
% 20.10/19.87 thf(c_0_25, plain, (fin @ (fsetadjoin @ esk3232_0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ esk3230_0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ esk3230_0 @ (fsetadjoin @ esk3231_0 @ femptyset)) @ femptyset))|p1), inference(split_conjunct,[status(thm)],[c_0_20])).
% 20.10/19.87 thf(c_0_26, plain, ![X6417:$i, X6418:$i]:(~p4|(~fin @ X6417 @ (fsetadjoin @ X6418 @ femptyset)|(X6417)=(X6418))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax4])])])).
% 20.10/19.87 thf(c_0_27, plain, (p3|p4), inference(split_conjunct,[status(thm)],[ax1377])).
% 20.10/19.87 thf(c_0_28, plain, ![X1:$i, X2:$i]:(fin @ X1 @ (fsetadjoin @ X1 @ X2)|~p2), inference(split_conjunct,[status(thm)],[c_0_21])).
% 20.10/19.87 thf(c_0_29, plain, p2, inference(sr,[status(thm)],[c_0_22, c_0_14])).
% 20.10/19.87 thf(c_0_30, 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_23, c_0_24])])).
% 20.10/19.87 thf(c_0_31, plain, fin @ (fsetadjoin @ esk3232_0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ esk3230_0 @ femptyset) @ (fsetadjoin @ (fsetadjoin @ esk3230_0 @ (fsetadjoin @ esk3231_0 @ femptyset)) @ femptyset)), inference(sr,[status(thm)],[c_0_25, c_0_14])).
% 20.10/19.87 thf(c_0_32, plain, ![X1:$i, X2:$i]:((X1)=(X2)|~p4|~fin @ X1 @ (fsetadjoin @ X2 @ femptyset)), inference(split_conjunct,[status(thm)],[c_0_26])).
% 20.10/19.87 thf(c_0_33, plain, p4, inference(sr,[status(thm)],[c_0_27, c_0_16])).
% 20.10/19.87 thf(c_0_34, plain, ![X1:$i, X2:$i]:fin @ X1 @ (fsetadjoin @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_29])])).
% 20.10/19.87 thf(c_0_35, plain, ((fsetadjoin @ esk3230_0 @ (fsetadjoin @ esk3231_0 @ femptyset))=(fsetadjoin @ esk3232_0 @ femptyset)|(fsetadjoin @ esk3232_0 @ femptyset)=(fsetadjoin @ esk3230_0 @ femptyset)), inference(spm,[status(thm)],[c_0_30, c_0_31])).
% 20.10/19.87 thf(c_0_36, plain, (p1|(esk3230_0)!=(esk3232_0)), inference(split_conjunct,[status(thm)],[c_0_20])).
% 20.10/19.87 thf(c_0_37, plain, ![X1:$i, X2:$i]:((X1)=(X2)|~fin @ X1 @ (fsetadjoin @ X2 @ femptyset)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_32, c_0_33])])).
% 20.10/19.87 thf(c_0_38, plain, ((fsetadjoin @ esk3232_0 @ femptyset)=(fsetadjoin @ esk3230_0 @ femptyset)|fin @ esk3230_0 @ (fsetadjoin @ esk3232_0 @ femptyset)), inference(spm,[status(thm)],[c_0_34, c_0_35])).
% 20.10/19.87 thf(c_0_39, plain, (esk3232_0)!=(esk3230_0), inference(sr,[status(thm)],[c_0_36, c_0_14])).
% 20.10/19.87 thf(c_0_40, plain, (fsetadjoin @ esk3232_0 @ femptyset)=(fsetadjoin @ esk3230_0 @ femptyset), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39])).
% 20.10/19.87 thf(c_0_41, plain, ![X1:$i]:((X1)=(esk3232_0)|~fin @ X1 @ (fsetadjoin @ esk3230_0 @ femptyset)), inference(spm,[status(thm)],[c_0_37, c_0_40])).
% 20.10/19.87 thf(c_0_42, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_34]), c_0_39]), ['proof']).
% 20.10/19.87 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 20.10/19.87 thf(0,theorem,((![X1:$i]:(![X2:$i]:((in @ X1) @ ((setadjoin @ X1) @ X2)))) => ((![X1:$i]:(![X2:$i]:(((in @ X1) @ ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))) => ((![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) => ((~((X3 = X1))) => (X3 = X2)))))) => ((![X1:$i]:(![X2:$i]:((((setadjoin @ X1) @ emptyset) = ((setadjoin @ X2) @ emptyset)) => (X1 = X2)))) => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ ((setadjoin @ X3) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ emptyset)) @ ((setadjoin @ ((setadjoin @ X1) @ ((setadjoin @ X2) @ emptyset))) @ emptyset))) => (X1 = X3))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 20.10/19.87 % SZS output end Proof
%------------------------------------------------------------------------------