%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP005^5 : TPTP v9.2.0. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n025.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 01:46:23 PM UTC 2025
% Result : Theorem 164.64s 163.79s
% Output : Proof 164.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.14 % Problem : ITP005^5 : TPTP v9.2.0. Bugfixed v7.5.0.
% 0.15/0.15 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.15/0.36 % Computer : n025.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed Oct 8 18:12:54 EDT 2025
% 0.23/0.37 % CPUTime :
% 164.64/163.79 % SZS status Theorem
% 164.64/163.79 % Mode: mode500:USE_SINE=true:SINE_TOLERANCE=1.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=2.:SINE_DEPTH=0
% 164.64/163.79 % Inferences: 0
% 164.64/163.79 % SZS output start Proof
% 164.64/163.79 thf(conj_thm_2Eset__relation_2Erel__to__reln__inv,conjecture,(![X1:del]:(![X2:del]:(![X3:$i]:(((mem @ X3) @ ((arr @ X1) @ ((arr @ X2) @ bool))) => (((ap @ ((c_2Eset__relation_2Ereln__to__rel @ X1) @ X2)) @ ((ap @ ((c_2Eset__relation_2Erel__to__reln @ X1) @ X2)) @ X3)) = X3)))))).
% 164.64/163.79 thf(h0,negated_conjecture,(~((![X1:del]:(![X2:del]:(![X3:$i]:(((mem @ X3) @ ((arr @ X1) @ ((arr @ X2) @ bool))) => (((ap @ ((c_2Eset__relation_2Ereln__to__rel @ X1) @ X2)) @ ((ap @ ((c_2Eset__relation_2Erel__to__reln @ X1) @ X2)) @ X3)) = X3))))))),inference(assume_negation,[status(cth)],[conj_thm_2Eset__relation_2Erel__to__reln__inv])).
% 164.64/163.79 thf(pax2, axiom, (p2=>![X1:del, X2:del]:(fc_2Eset__relation_2Ereln__to__rel @ X1 @ X2)=(fc_2Epair_2ECURRY @ X1 @ X2 @ fbool)), file('<stdin>', pax2)).
% 164.64/163.79 thf(pax3, axiom, (p3=>![X1:del, X2:del]:(fc_2Eset__relation_2Erel__to__reln @ X1 @ X2)=(fc_2Epair_2EUNCURRY @ X1 @ X2 @ fbool)), file('<stdin>', pax3)).
% 164.64/163.79 thf(nax1, axiom, (p1<=![X1:del, X2:del, X14:$i]:(fmem @ X14 @ (farr @ X1 @ (farr @ X2 @ fbool))=>(fap @ (fc_2Eset__relation_2Ereln__to__rel @ X1 @ X2) @ (fap @ (fc_2Eset__relation_2Erel__to__reln @ X1 @ X2) @ X14))=(X14))), file('<stdin>', nax1)).
% 164.64/163.79 thf(ax55, axiom, p2, file('<stdin>', ax55)).
% 164.64/163.79 thf(ax54, axiom, p3, file('<stdin>', ax54)).
% 164.64/163.79 thf(ax56, axiom, ~(p1), file('<stdin>', ax56)).
% 164.64/163.79 thf(pax50, axiom, (p50=>![X1:del, X2:del, X5:del, X4:$i]:(fmem @ X4 @ (farr @ X1 @ (farr @ X2 @ X5))=>(fap @ (fc_2Epair_2ECURRY @ X1 @ X2 @ X5) @ (fap @ (fc_2Epair_2EUNCURRY @ X1 @ X2 @ X5) @ X4))=(X4))), file('<stdin>', pax50)).
% 164.64/163.79 thf(ax7, axiom, p50, file('<stdin>', ax7)).
% 164.64/163.79 thf(c_0_8, plain, ![X174:del, X175:del]:(~p2|(fc_2Eset__relation_2Ereln__to__rel @ X174 @ X175)=(fc_2Epair_2ECURRY @ X174 @ X175 @ fbool)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax2])])])).
% 164.64/163.79 thf(c_0_9, plain, ![X170:del, X171:del]:(~p3|(fc_2Eset__relation_2Erel__to__reln @ X170 @ X171)=(fc_2Epair_2EUNCURRY @ X170 @ X171 @ fbool)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax3])])])).
% 164.64/163.79 thf(c_0_10, plain, ((fmem @ esk84_0 @ (farr @ esk82_0 @ (farr @ esk83_0 @ fbool))|p1)&((fap @ (fc_2Eset__relation_2Ereln__to__rel @ esk82_0 @ esk83_0) @ (fap @ (fc_2Eset__relation_2Erel__to__reln @ esk82_0 @ esk83_0) @ esk84_0))!=(esk84_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])])])])])).
% 164.64/163.79 thf(c_0_11, plain, ![X1:del, X2:del]:((fc_2Eset__relation_2Ereln__to__rel @ X1 @ X2)=(fc_2Epair_2ECURRY @ X1 @ X2 @ fbool)|~p2), inference(split_conjunct,[status(thm)],[c_0_8])).
% 164.64/163.79 thf(c_0_12, plain, p2, inference(split_conjunct,[status(thm)],[ax55])).
% 164.64/163.79 thf(c_0_13, plain, ![X1:del, X2:del]:((fc_2Eset__relation_2Erel__to__reln @ X1 @ X2)=(fc_2Epair_2EUNCURRY @ X1 @ X2 @ fbool)|~p3), inference(split_conjunct,[status(thm)],[c_0_9])).
% 164.64/163.79 thf(c_0_14, plain, p3, inference(split_conjunct,[status(thm)],[ax54])).
% 164.64/163.79 thf(c_0_15, plain, ~p1, inference(fof_simplification,[status(thm)],[ax56])).
% 164.64/163.79 thf(c_0_16, plain, ![X72:del, X73:del, X74:del, X75:$i]:(~p50|(~fmem @ X75 @ (farr @ X72 @ (farr @ X73 @ X74))|(fap @ (fc_2Epair_2ECURRY @ X72 @ X73 @ X74) @ (fap @ (fc_2Epair_2EUNCURRY @ X72 @ X73 @ X74) @ X75))=(X75))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax50])])])).
% 164.64/163.79 thf(c_0_17, plain, (p1|(fap @ (fc_2Eset__relation_2Ereln__to__rel @ esk82_0 @ esk83_0) @ (fap @ (fc_2Eset__relation_2Erel__to__reln @ esk82_0 @ esk83_0) @ esk84_0))!=(esk84_0)), inference(split_conjunct,[status(thm)],[c_0_10])).
% 164.64/163.79 thf(c_0_18, plain, ![X1:del, X2:del]:(fc_2Eset__relation_2Ereln__to__rel @ X1 @ X2)=(fc_2Epair_2ECURRY @ X1 @ X2 @ fbool), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_11, c_0_12])])).
% 164.64/163.79 thf(c_0_19, plain, ![X1:del, X2:del]:(fc_2Eset__relation_2Erel__to__reln @ X1 @ X2)=(fc_2Epair_2EUNCURRY @ X1 @ X2 @ fbool), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_13, c_0_14])])).
% 164.64/163.79 thf(c_0_20, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_15])).
% 164.64/163.79 thf(c_0_21, plain, ![X1:del, X2:del, X3:$i, X5:del]:((fap @ (fc_2Epair_2ECURRY @ X1 @ X2 @ X5) @ (fap @ (fc_2Epair_2EUNCURRY @ X1 @ X2 @ X5) @ X3))=(X3)|~p50|~fmem @ X3 @ (farr @ X1 @ (farr @ X2 @ X5))), inference(split_conjunct,[status(thm)],[c_0_16])).
% 164.64/163.79 thf(c_0_22, plain, p50, inference(split_conjunct,[status(thm)],[ax7])).
% 164.64/163.79 thf(c_0_23, plain, (fmem @ esk84_0 @ (farr @ esk82_0 @ (farr @ esk83_0 @ fbool))|p1), inference(split_conjunct,[status(thm)],[c_0_10])).
% 164.64/163.79 thf(c_0_24, plain, (fap @ (fc_2Epair_2ECURRY @ esk82_0 @ esk83_0 @ fbool) @ (fap @ (fc_2Epair_2EUNCURRY @ esk82_0 @ esk83_0 @ fbool) @ esk84_0))!=(esk84_0), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_17, c_0_18]), c_0_19]), c_0_20])).
% 164.64/163.79 thf(c_0_25, plain, ![X1:del, X2:del, X3:$i, X5:del]:((fap @ (fc_2Epair_2ECURRY @ X1 @ X2 @ X5) @ (fap @ (fc_2Epair_2EUNCURRY @ X1 @ X2 @ X5) @ X3))=(X3)|~fmem @ X3 @ (farr @ X1 @ (farr @ X2 @ X5))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_22])])).
% 164.64/163.79 thf(c_0_26, plain, fmem @ esk84_0 @ (farr @ esk82_0 @ (farr @ esk83_0 @ fbool)), inference(sr,[status(thm)],[c_0_23, c_0_20])).
% 164.64/163.79 thf(c_0_27, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_25]), c_0_26])]), ['proof']).
% 164.64/163.79 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 164.64/163.79 thf(0,theorem,(![X1:del]:(![X2:del]:(![X3:$i]:(((mem @ X3) @ ((arr @ X1) @ ((arr @ X2) @ bool))) => (((ap @ ((c_2Eset__relation_2Ereln__to__rel @ X1) @ X2)) @ ((ap @ ((c_2Eset__relation_2Erel__to__reln @ X1) @ X2)) @ X3)) = X3))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 164.64/163.79 % SZS output end Proof
%------------------------------------------------------------------------------