%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP197^1 : TPTP v9.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n016.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:47:15 PM UTC 2025
% Result : Theorem 168.97s 168.96s
% Output : Proof 168.97s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : ITP197^1 : TPTP v9.2.0. Released v7.5.0.
% 0.11/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.32 % Computer : n016.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Wed Oct 8 17:53:08 EDT 2025
% 0.12/0.32 % CPUTime :
% 168.97/168.96 % SZS status Theorem
% 168.97/168.96 % Mode: mode500:USE_SINE=true:SINE_TOLERANCE=1.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=2.:SINE_DEPTH=0
% 168.97/168.96 % Inferences: 0
% 168.97/168.96 % SZS output start Proof
% 168.97/168.96 thf(conj_0,conjecture,((~(((((type_M1690910139scheme @ s1) @ (type_M876316792e_FVar @ x)) = ((type_M1690910139scheme @ s2) @ (type_M876316792e_FVar @ x))) => (~(((member_nat @ n) @ (type_M1050318637scheme @ (type_M876316792e_FVar @ x)))))))) => ((s1 @ n) = (s2 @ n)))).
% 168.97/168.96 thf(h0,negated_conjecture,(~(((~(((((type_M1690910139scheme @ s1) @ (type_M876316792e_FVar @ x)) = ((type_M1690910139scheme @ s2) @ (type_M876316792e_FVar @ x))) => (~(((member_nat @ n) @ (type_M1050318637scheme @ (type_M876316792e_FVar @ x)))))))) => ((s1 @ n) = (s2 @ n))))),inference(assume_negation,[status(cth)],[conj_0])).
% 168.97/168.96 thf(pax176, axiom, (p176=>![X16:nat]:(ftype_M1050318637scheme @ (ftype_M876316792e_FVar @ X16))=(finsert_nat @ X16 @ fbot_bot_set_nat)), file('<stdin>', pax176)).
% 168.97/168.96 thf(pax132, axiom, (p132=>![X48:nat, X56:nat]:(fmember_nat @ X48 @ (finsert_nat @ X56 @ fbot_bot_set_nat)=>(X48)=(X56))), file('<stdin>', pax132)).
% 168.97/168.96 thf(nax1, axiom, (p1<=(~(((ftype_M1690910139scheme @ fs1 @ (ftype_M876316792e_FVar @ fx))=(ftype_M1690910139scheme @ fs2 @ (ftype_M876316792e_FVar @ fx))=>~(fmember_nat @ fn @ (ftype_M1050318637scheme @ (ftype_M876316792e_FVar @ fx)))))=>(fs1 @ fn)=(fs2 @ fn))), file('<stdin>', nax1)).
% 168.97/168.96 thf(ax8, axiom, p176, file('<stdin>', ax8)).
% 168.97/168.96 thf(ax183, axiom, ~(p1), file('<stdin>', ax183)).
% 168.97/168.96 thf(ax52, axiom, p132, file('<stdin>', ax52)).
% 168.97/168.96 thf(pax171, axiom, (p171=>![X17:nat > type_Mirabelle_typ, X18:type_Mirabelle_typ]:(ftype_M1690910139scheme @ X17 @ (ftype_M1006385707scheme @ X18))=(ftype_M1006385707scheme @ (ftype_M784671311le_typ @ X17 @ X18))), file('<stdin>', pax171)).
% 168.97/168.96 thf(pax49, axiom, (p49=>![X168:nat]:(ftype_M1006385707scheme @ (ftype_Mirabelle_TVar @ X168))=(ftype_M876316792e_FVar @ X168)), file('<stdin>', pax49)).
% 168.97/168.96 thf(pax122, axiom, (p122=>![X61:nat > type_Mirabelle_typ, X62:nat]:(ftype_M784671311le_typ @ X61 @ (ftype_Mirabelle_TVar @ X62))=(X61 @ X62)), file('<stdin>', pax122)).
% 168.97/168.96 thf(ax13, axiom, p171, file('<stdin>', ax13)).
% 168.97/168.96 thf(ax135, axiom, p49, file('<stdin>', ax135)).
% 168.97/168.96 thf(ax62, axiom, p122, file('<stdin>', ax62)).
% 168.97/168.96 thf(pax163, axiom, (p163=>![X30:type_Mirabelle_typ, X32:type_Mirabelle_typ]:((ftype_M1006385707scheme @ X30)=(ftype_M1006385707scheme @ X32)=>(X30)=(X32))), file('<stdin>', pax163)).
% 168.97/168.96 thf(ax21, axiom, p163, file('<stdin>', ax21)).
% 168.97/168.96 thf(c_0_14, plain, ![X250:nat]:(~p176|(ftype_M1050318637scheme @ (ftype_M876316792e_FVar @ X250))=(finsert_nat @ X250 @ fbot_bot_set_nat)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax176])])])).
% 168.97/168.96 thf(c_0_15, plain, ![X374:nat, X375:nat]:(~p132|(~fmember_nat @ X374 @ (finsert_nat @ X375 @ fbot_bot_set_nat)|(X374)=(X375))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax132])])])).
% 168.97/168.96 thf(c_0_16, plain, ((((ftype_M1690910139scheme @ fs1 @ (ftype_M876316792e_FVar @ fx))=(ftype_M1690910139scheme @ fs2 @ (ftype_M876316792e_FVar @ fx))|p1)&(fmember_nat @ fn @ (ftype_M1050318637scheme @ (ftype_M876316792e_FVar @ fx))|p1))&((fs1 @ fn)!=(fs2 @ fn)|p1)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])])])).
% 168.97/168.96 thf(c_0_17, plain, ![X2:nat]:((ftype_M1050318637scheme @ (ftype_M876316792e_FVar @ X2))=(finsert_nat @ X2 @ fbot_bot_set_nat)|~p176), inference(split_conjunct,[status(thm)],[c_0_14])).
% 168.97/168.96 thf(c_0_18, plain, p176, inference(split_conjunct,[status(thm)],[ax8])).
% 168.97/168.96 thf(c_0_19, plain, ~p1, inference(fof_simplification,[status(thm)],[ax183])).
% 168.97/168.96 thf(c_0_20, plain, ![X2:nat, X5:nat]:((X2)=(X5)|~p132|~fmember_nat @ X2 @ (finsert_nat @ X5 @ fbot_bot_set_nat)), inference(split_conjunct,[status(thm)],[c_0_15])).
% 168.97/168.96 thf(c_0_21, plain, p132, inference(split_conjunct,[status(thm)],[ax52])).
% 168.97/168.96 thf(c_0_22, plain, (fmember_nat @ fn @ (ftype_M1050318637scheme @ (ftype_M876316792e_FVar @ fx))|p1), inference(split_conjunct,[status(thm)],[c_0_16])).
% 168.97/168.96 thf(c_0_23, plain, ![X2:nat]:(ftype_M1050318637scheme @ (ftype_M876316792e_FVar @ X2))=(finsert_nat @ X2 @ fbot_bot_set_nat), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_17, c_0_18])])).
% 168.97/168.96 thf(c_0_24, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_19])).
% 168.97/168.96 thf(c_0_25, plain, ![X252:nat > type_Mirabelle_typ, X253:type_Mirabelle_typ]:(~p171|(ftype_M1690910139scheme @ X252 @ (ftype_M1006385707scheme @ X253))=(ftype_M1006385707scheme @ (ftype_M784671311le_typ @ X252 @ X253))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax171])])])).
% 168.97/168.96 thf(c_0_26, plain, ![X678:nat]:(~p49|(ftype_M1006385707scheme @ (ftype_Mirabelle_TVar @ X678))=(ftype_M876316792e_FVar @ X678)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax49])])])).
% 168.97/168.96 thf(c_0_27, plain, ![X396:nat > type_Mirabelle_typ, X397:nat]:(~p122|(ftype_M784671311le_typ @ X396 @ (ftype_Mirabelle_TVar @ X397))=(X396 @ X397)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax122])])])).
% 168.97/168.96 thf(c_0_28, plain, ((ftype_M1690910139scheme @ fs1 @ (ftype_M876316792e_FVar @ fx))=(ftype_M1690910139scheme @ fs2 @ (ftype_M876316792e_FVar @ fx))|p1), inference(split_conjunct,[status(thm)],[c_0_16])).
% 168.97/168.96 thf(c_0_29, plain, ![X2:nat, X5:nat]:((X2)=(X5)|~fmember_nat @ X2 @ (finsert_nat @ X5 @ fbot_bot_set_nat)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_20, c_0_21])])).
% 168.97/168.96 thf(c_0_30, plain, fmember_nat @ fn @ (finsert_nat @ fx @ fbot_bot_set_nat), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23]), c_0_24])).
% 168.97/168.96 thf(c_0_31, plain, ![X1:nat > type_Mirabelle_typ, X9:type_Mirabelle_typ]:((ftype_M1690910139scheme @ X1 @ (ftype_M1006385707scheme @ X9))=(ftype_M1006385707scheme @ (ftype_M784671311le_typ @ X1 @ X9))|~p171), inference(split_conjunct,[status(thm)],[c_0_25])).
% 168.97/168.96 thf(c_0_32, plain, p171, inference(split_conjunct,[status(thm)],[ax13])).
% 168.97/168.96 thf(c_0_33, plain, ![X2:nat]:((ftype_M1006385707scheme @ (ftype_Mirabelle_TVar @ X2))=(ftype_M876316792e_FVar @ X2)|~p49), inference(split_conjunct,[status(thm)],[c_0_26])).
% 168.97/168.96 thf(c_0_34, plain, p49, inference(split_conjunct,[status(thm)],[ax135])).
% 168.97/168.96 thf(c_0_35, plain, ![X1:nat > type_Mirabelle_typ, X2:nat]:((ftype_M784671311le_typ @ X1 @ (ftype_Mirabelle_TVar @ X2))=(X1 @ X2)|~p122), inference(split_conjunct,[status(thm)],[c_0_27])).
% 168.97/168.96 thf(c_0_36, plain, p122, inference(split_conjunct,[status(thm)],[ax62])).
% 168.97/168.96 thf(c_0_37, plain, ![X292:type_Mirabelle_typ, X293:type_Mirabelle_typ]:(~p163|((ftype_M1006385707scheme @ X292)!=(ftype_M1006385707scheme @ X293)|(X292)=(X293))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax163])])])).
% 168.97/168.96 thf(c_0_38, plain, (ftype_M1690910139scheme @ fs1 @ (ftype_M876316792e_FVar @ fx))=(ftype_M1690910139scheme @ fs2 @ (ftype_M876316792e_FVar @ fx)), inference(sr,[status(thm)],[c_0_28, c_0_24])).
% 168.97/168.96 thf(c_0_39, plain, (fx)=(fn), inference(spm,[status(thm)],[c_0_29, c_0_30])).
% 168.97/168.96 thf(c_0_40, plain, ![X1:nat > type_Mirabelle_typ, X9:type_Mirabelle_typ]:(ftype_M1690910139scheme @ X1 @ (ftype_M1006385707scheme @ X9))=(ftype_M1006385707scheme @ (ftype_M784671311le_typ @ X1 @ X9)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32])])).
% 168.97/168.96 thf(c_0_41, plain, ![X2:nat]:(ftype_M1006385707scheme @ (ftype_Mirabelle_TVar @ X2))=(ftype_M876316792e_FVar @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 168.97/168.96 thf(c_0_42, plain, ![X1:nat > type_Mirabelle_typ, X2:nat]:(ftype_M784671311le_typ @ X1 @ (ftype_Mirabelle_TVar @ X2))=(X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 168.97/168.96 thf(c_0_43, plain, ![X9:type_Mirabelle_typ, X15:type_Mirabelle_typ]:((X9)=(X15)|~p163|(ftype_M1006385707scheme @ X9)!=(ftype_M1006385707scheme @ X15)), inference(split_conjunct,[status(thm)],[c_0_37])).
% 168.97/168.96 thf(c_0_44, plain, p163, inference(split_conjunct,[status(thm)],[ax21])).
% 168.97/168.96 thf(c_0_45, plain, (ftype_M1690910139scheme @ fs1 @ (ftype_M876316792e_FVar @ fn))=(ftype_M1690910139scheme @ fs2 @ (ftype_M876316792e_FVar @ fn)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_38, c_0_39]), c_0_39])).
% 168.97/168.96 thf(c_0_46, plain, ![X1:nat > type_Mirabelle_typ, X2:nat]:(ftype_M1690910139scheme @ X1 @ (ftype_M876316792e_FVar @ X2))=(ftype_M1006385707scheme @ (X1 @ X2)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_41]), c_0_42])).
% 168.97/168.96 thf(c_0_47, plain, ![X9:type_Mirabelle_typ, X15:type_Mirabelle_typ]:((X9)=(X15)|(ftype_M1006385707scheme @ X9)!=(ftype_M1006385707scheme @ X15)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_44])])).
% 168.97/168.96 thf(c_0_48, plain, (ftype_M1006385707scheme @ (fs1 @ fn))=(ftype_M1006385707scheme @ (fs2 @ fn)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_46]), c_0_46])).
% 168.97/168.96 thf(c_0_49, plain, (p1|(fs1 @ fn)!=(fs2 @ fn)), inference(split_conjunct,[status(thm)],[c_0_16])).
% 168.97/168.96 thf(c_0_50, plain, ![X9:type_Mirabelle_typ]:((X9)=(fs1 @ fn)|(ftype_M1006385707scheme @ X9)!=(ftype_M1006385707scheme @ (fs2 @ fn))), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 168.97/168.97 thf(c_0_51, plain, (fs1 @ fn)!=(fs2 @ fn), inference(sr,[status(thm)],[c_0_49, c_0_24])).
% 168.97/168.97 thf(c_0_52, plain, ($false), inference(sr,[status(thm)],[inference(er,[status(thm)],[c_0_50]), c_0_51]), ['proof']).
% 168.97/168.97 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 168.97/168.97 thf(0,theorem,((~(((((type_M1690910139scheme @ s1) @ (type_M876316792e_FVar @ x)) = ((type_M1690910139scheme @ s2) @ (type_M876316792e_FVar @ x))) => (~(((member_nat @ n) @ (type_M1050318637scheme @ (type_M876316792e_FVar @ x)))))))) => ((s1 @ n) = (s2 @ n))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 168.97/168.97 % SZS output end Proof
%------------------------------------------------------------------------------