%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP020^2 : 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 : n018.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:38 PM UTC 2025
% Result : Theorem 166.97s 164.79s
% Output : Proof 166.97s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : ITP020^2 : TPTP v9.2.0. Bugfixed v7.5.0.
% 0.13/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.35 % Computer : n018.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Oct 8 18:21:08 EDT 2025
% 0.13/0.35 % CPUTime :
% 166.97/164.79 % SZS status Theorem
% 166.97/164.79 % Mode: mode500:USE_SINE=true:SINE_TOLERANCE=1.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=2.:SINE_DEPTH=0
% 166.97/164.79 % Inferences: 94
% 166.97/164.79 % SZS output start Proof
% 166.97/164.79 thf(conj_thm_2Eutil__prob_2ENUM__2D__BIJ__INV,conjecture,(~((![X1:$i]:(((mem @ X1) @ ((arr @ ty_2Enum_2Enum) @ ((ty_2Epair_2Eprod @ ty_2Enum_2Enum) @ ty_2Enum_2Enum))) => (~((p @ ((ap @ ((ap @ ((ap @ ((c_2Epred__set_2EBIJ @ ty_2Enum_2Enum) @ ((ty_2Epair_2Eprod @ ty_2Enum_2Enum) @ ty_2Enum_2Enum))) @ X1)) @ (c_2Epred__set_2EUNIV @ ty_2Enum_2Enum))) @ ((ap @ ((ap @ ((c_2Epred__set_2ECROSS @ ty_2Enum_2Enum) @ ty_2Enum_2Enum)) @ (c_2Epred__set_2EUNIV @ ty_2Enum_2Enum))) @ (c_2Epred__set_2EUNIV @ ty_2Enum_2Enum))))))))))).
% 166.97/164.79 thf(h0,negated_conjecture,(![X1:$i]:(((mem @ X1) @ ((arr @ ty_2Enum_2Enum) @ ((ty_2Epair_2Eprod @ ty_2Enum_2Enum) @ ty_2Enum_2Enum))) => (~((p @ ((ap @ ((ap @ ((ap @ ((c_2Epred__set_2EBIJ @ ty_2Enum_2Enum) @ ((ty_2Epair_2Eprod @ ty_2Enum_2Enum) @ ty_2Enum_2Enum))) @ X1)) @ (c_2Epred__set_2EUNIV @ ty_2Enum_2Enum))) @ ((ap @ ((ap @ ((c_2Epred__set_2ECROSS @ ty_2Enum_2Enum) @ ty_2Enum_2Enum)) @ (c_2Epred__set_2EUNIV @ ty_2Enum_2Enum))) @ (c_2Epred__set_2EUNIV @ ty_2Enum_2Enum)))))))),inference(assume_negation,[status(cth)],[conj_thm_2Eutil__prob_2ENUM__2D__BIJ__INV])).
% 166.97/164.79 thf(ax32, axiom, (~(p12)|p122), file('<stdin>', ax32)).
% 166.97/164.79 thf(ax105, axiom, (~(p38)|p54), file('<stdin>', ax105)).
% 166.97/164.79 thf(ax0, axiom, (~(p122)|p153), file('<stdin>', ax0)).
% 166.97/164.79 thf(ax147, axiom, p12, file('<stdin>', ax147)).
% 166.97/164.79 thf(ax9, axiom, (~(p149)|p148), file('<stdin>', ax9)).
% 166.97/164.79 thf(ax2, axiom, (~(p152)|~(p54)|p151), file('<stdin>', ax2)).
% 166.97/164.79 thf(ax121, axiom, p38, file('<stdin>', ax121)).
% 166.97/164.79 thf(ax1, axiom, (~(p153)|p152), file('<stdin>', ax1)).
% 166.97/164.79 thf(ax8, axiom, (~(p148)|p147), file('<stdin>', ax8)).
% 166.97/164.79 thf(ax10, axiom, p149, file('<stdin>', ax10)).
% 166.97/164.79 thf(ax7, axiom, (~(p147)|p2|p146), file('<stdin>', ax7)).
% 166.97/164.79 thf(ax157, axiom, ~(p2), file('<stdin>', ax157)).
% 166.97/164.79 thf(pax40, axiom, (p40=>![X3:del, X6:del, X4:$i]:(fmem @ X4 @ (farr @ X3 @ X6)=>![X5:$i]:(fmem @ X5 @ X3=>fmem @ (fap @ X4 @ X5) @ X6))), file('<stdin>', pax40)).
% 166.97/164.79 thf(pax37, axiom, (p37=>![X3:del, X6:del]:fmem @ (fc_2Epred__set_2ECROSS @ X3 @ X6) @ (farr @ (farr @ X3 @ fbool) @ (farr @ (farr @ X6 @ fbool) @ (farr @ (fty_2Epair_2Eprod @ X3 @ X6) @ fbool)))), file('<stdin>', pax37)).
% 166.97/164.79 thf(ax3, axiom, (~(p151)|p150), file('<stdin>', ax3)).
% 166.97/164.79 thf(ax5, axiom, (~(p145)|~(p144)|~(p1)), file('<stdin>', ax5)).
% 166.97/164.79 thf(ax6, axiom, (~(p146)|p145), file('<stdin>', ax6)).
% 166.97/164.79 thf(ax119, axiom, p40, file('<stdin>', ax119)).
% 166.97/164.79 thf(ax122, axiom, p37, file('<stdin>', ax122)).
% 166.97/164.79 thf(ax4, axiom, (~(p150)|~(p134)|p144), file('<stdin>', ax4)).
% 166.97/164.79 thf(ax158, axiom, p1, file('<stdin>', ax158)).
% 166.97/164.79 thf(pax38, axiom, (p38=>![X3:del]:fmem @ (fc_2Epred__set_2EUNIV @ X3) @ (farr @ X3 @ fbool)), file('<stdin>', pax38)).
% 166.97/164.79 thf(nax134, axiom, (p134<=fmem @ (fap @ (fap @ (fc_2Epred__set_2ECROSS @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum)) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum)) @ (farr @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fbool)), file('<stdin>', nax134)).
% 166.97/164.79 thf(c_0_23, plain, (~p12|p122), inference(fof_simplification,[status(thm)],[ax32])).
% 166.97/164.79 thf(c_0_24, plain, (~p38|p54), inference(fof_simplification,[status(thm)],[ax105])).
% 166.97/164.79 thf(c_0_25, plain, (~p122|p153), inference(fof_simplification,[status(thm)],[ax0])).
% 166.97/164.79 thf(c_0_26, plain, (p122|~p12), inference(split_conjunct,[status(thm)],[c_0_23])).
% 166.97/164.79 thf(c_0_27, plain, p12, inference(split_conjunct,[status(thm)],[ax147])).
% 166.97/164.79 thf(c_0_28, plain, (~p149|p148), inference(fof_simplification,[status(thm)],[ax9])).
% 166.97/164.79 thf(c_0_29, plain, (~p152|~p54|p151), inference(fof_simplification,[status(thm)],[ax2])).
% 166.97/164.79 thf(c_0_30, plain, (p54|~p38), inference(split_conjunct,[status(thm)],[c_0_24])).
% 166.97/164.79 thf(c_0_31, plain, p38, inference(split_conjunct,[status(thm)],[ax121])).
% 166.97/164.79 thf(c_0_32, plain, (~p153|p152), inference(fof_simplification,[status(thm)],[ax1])).
% 166.97/164.79 thf(c_0_33, plain, (p153|~p122), inference(split_conjunct,[status(thm)],[c_0_25])).
% 166.97/164.79 thf(c_0_34, plain, p122, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_27])])).
% 166.97/164.79 thf(c_0_35, plain, (~p148|p147), inference(fof_simplification,[status(thm)],[ax8])).
% 166.97/164.79 thf(c_0_36, plain, (p148|~p149), inference(split_conjunct,[status(thm)],[c_0_28])).
% 166.97/164.79 thf(c_0_37, plain, p149, inference(split_conjunct,[status(thm)],[ax10])).
% 166.97/164.79 thf(c_0_38, plain, (p151|~p152|~p54), inference(split_conjunct,[status(thm)],[c_0_29])).
% 166.97/164.79 thf(c_0_39, plain, p54, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31])])).
% 166.97/164.79 thf(c_0_40, plain, (p152|~p153), inference(split_conjunct,[status(thm)],[c_0_32])).
% 166.97/164.79 thf(c_0_41, plain, p153, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 166.97/164.79 thf(c_0_42, plain, (~p147|p2|p146), inference(fof_simplification,[status(thm)],[ax7])).
% 166.97/164.79 thf(c_0_43, plain, (p147|~p148), inference(split_conjunct,[status(thm)],[c_0_35])).
% 166.97/164.79 thf(c_0_44, plain, p148, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_36, c_0_37])])).
% 166.97/164.79 thf(c_0_45, plain, ~p2, inference(fof_simplification,[status(thm)],[ax157])).
% 166.97/164.79 thf(c_0_46, plain, ![X92:del, X93:del, X94:$i, X95:$i]:(~p40|(~fmem @ X94 @ (farr @ X92 @ X93)|(~fmem @ X95 @ X92|fmem @ (fap @ X94 @ X95) @ X93))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax40])])])).
% 166.97/164.79 thf(c_0_47, plain, ![X112:del, X113:del]:(~p37|fmem @ (fc_2Epred__set_2ECROSS @ X112 @ X113) @ (farr @ (farr @ X112 @ fbool) @ (farr @ (farr @ X113 @ fbool) @ (farr @ (fty_2Epair_2Eprod @ X112 @ X113) @ fbool)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax37])])])).
% 166.97/164.79 thf(c_0_48, plain, (~p151|p150), inference(fof_simplification,[status(thm)],[ax3])).
% 166.97/164.79 thf(c_0_49, plain, (p151|~p152), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_38, c_0_39])])).
% 166.97/164.79 thf(c_0_50, plain, p152, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_40, c_0_41])])).
% 166.97/164.79 thf(c_0_51, plain, (~p145|~p144|~p1), inference(fof_simplification,[status(thm)],[ax5])).
% 166.97/164.79 thf(c_0_52, plain, (~p146|p145), inference(fof_simplification,[status(thm)],[ax6])).
% 166.97/164.79 thf(c_0_53, plain, (p2|p146|~p147), inference(split_conjunct,[status(thm)],[c_0_42])).
% 166.97/164.79 thf(c_0_54, plain, p147, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_44])])).
% 166.97/164.79 thf(c_0_55, plain, ~p2, inference(split_conjunct,[status(thm)],[c_0_45])).
% 166.97/164.79 thf(c_0_56, plain, ![X1:$i, X2:$i, X6:del, X3:del]:(fmem @ (fap @ X1 @ X2) @ X6|~p40|~fmem @ X1 @ (farr @ X3 @ X6)|~fmem @ X2 @ X3), inference(split_conjunct,[status(thm)],[c_0_46])).
% 166.97/164.79 thf(c_0_57, plain, p40, inference(split_conjunct,[status(thm)],[ax119])).
% 166.97/164.79 thf(c_0_58, plain, ![X3:del, X6:del]:(fmem @ (fc_2Epred__set_2ECROSS @ X3 @ X6) @ (farr @ (farr @ X3 @ fbool) @ (farr @ (farr @ X6 @ fbool) @ (farr @ (fty_2Epair_2Eprod @ X3 @ X6) @ fbool)))|~p37), inference(split_conjunct,[status(thm)],[c_0_47])).
% 166.97/164.79 thf(c_0_59, plain, p37, inference(split_conjunct,[status(thm)],[ax122])).
% 166.97/164.79 thf(c_0_60, plain, (~p150|~p134|p144), inference(fof_simplification,[status(thm)],[ax4])).
% 166.97/164.79 thf(c_0_61, plain, (p150|~p151), inference(split_conjunct,[status(thm)],[c_0_48])).
% 166.97/164.79 thf(c_0_62, plain, p151, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_49, c_0_50])])).
% 166.97/164.79 thf(c_0_63, plain, (~p145|~p144|~p1), inference(split_conjunct,[status(thm)],[c_0_51])).
% 166.97/164.79 thf(c_0_64, plain, p1, inference(split_conjunct,[status(thm)],[ax158])).
% 166.97/164.79 thf(c_0_65, plain, (p145|~p146), inference(split_conjunct,[status(thm)],[c_0_52])).
% 166.97/164.79 thf(c_0_66, plain, p146, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_53, c_0_54])]), c_0_55])).
% 166.97/164.79 thf(c_0_67, plain, ![X1:$i, X2:$i, X3:del, X6:del]:(fmem @ (fap @ X1 @ X2) @ X3|~fmem @ X1 @ (farr @ X6 @ X3)|~fmem @ X2 @ X6), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_57])])).
% 166.97/164.79 thf(c_0_68, plain, ![X3:del, X6:del]:fmem @ (fc_2Epred__set_2ECROSS @ X3 @ X6) @ (farr @ (farr @ X3 @ fbool) @ (farr @ (farr @ X6 @ fbool) @ (farr @ (fty_2Epair_2Eprod @ X3 @ X6) @ fbool))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_58, c_0_59])])).
% 166.97/164.79 thf(c_0_69, plain, ![X110:del]:(~p38|fmem @ (fc_2Epred__set_2EUNIV @ X110) @ (farr @ X110 @ fbool)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax38])])])).
% 166.97/164.79 thf(c_0_70, plain, (p144|~p150|~p134), inference(split_conjunct,[status(thm)],[c_0_60])).
% 166.97/164.79 thf(c_0_71, plain, p150, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_61, c_0_62])])).
% 166.97/164.79 thf(c_0_72, plain, (~p144|~p145), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63, c_0_64])])).
% 166.97/164.79 thf(c_0_73, plain, p145, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_65, c_0_66])])).
% 166.97/164.79 thf(c_0_74, plain, (~fmem @ (fap @ (fap @ (fc_2Epred__set_2ECROSS @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum)) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum)) @ (farr @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fbool)|p134), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax134])])).
% 166.97/164.79 thf(c_0_75, plain, ![X1:$i, X6:del, X3:del]:(fmem @ (fap @ (fc_2Epred__set_2ECROSS @ X3 @ X6) @ X1) @ (farr @ (farr @ X6 @ fbool) @ (farr @ (fty_2Epair_2Eprod @ X3 @ X6) @ fbool))|~fmem @ X1 @ (farr @ X3 @ fbool)), inference(spm,[status(thm)],[c_0_67, c_0_68])).
% 166.97/164.79 thf(c_0_76, plain, ![X3:del]:(fmem @ (fc_2Epred__set_2EUNIV @ X3) @ (farr @ X3 @ fbool)|~p38), inference(split_conjunct,[status(thm)],[c_0_69])).
% 166.97/164.79 thf(c_0_77, plain, (p144|~p134), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_70, c_0_71])])).
% 166.97/164.79 thf(c_0_78, plain, ~p144, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_72, c_0_73])])).
% 166.97/164.79 thf(c_0_79, plain, (p134|~fmem @ (fap @ (fap @ (fc_2Epred__set_2ECROSS @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum)) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum)) @ (farr @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fbool)), inference(split_conjunct,[status(thm)],[c_0_74])).
% 166.97/164.79 thf(c_0_80, plain, ![X2:$i, X1:$i, X6:del, X3:del]:(fmem @ (fap @ (fap @ (fc_2Epred__set_2ECROSS @ X3 @ X6) @ X1) @ X2) @ (farr @ (fty_2Epair_2Eprod @ X3 @ X6) @ fbool)|~fmem @ X2 @ (farr @ X6 @ fbool)|~fmem @ X1 @ (farr @ X3 @ fbool)), inference(spm,[status(thm)],[c_0_67, c_0_75])).
% 166.97/164.79 thf(c_0_81, plain, ![X3:del]:fmem @ (fc_2Epred__set_2EUNIV @ X3) @ (farr @ X3 @ fbool), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_76, c_0_31])])).
% 166.97/164.79 thf(c_0_82, plain, ~p134, inference(sr,[status(thm)],[c_0_77, c_0_78])).
% 166.97/164.79 thf(c_0_83, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79, c_0_80]), c_0_81])]), c_0_82]), ['proof']).
% 166.97/164.79 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 166.97/164.79 thf(0,theorem,(~((![X1:$i]:(((mem @ X1) @ ((arr @ ty_2Enum_2Enum) @ ((ty_2Epair_2Eprod @ ty_2Enum_2Enum) @ ty_2Enum_2Enum))) => (~((p @ ((ap @ ((ap @ ((ap @ ((c_2Epred__set_2EBIJ @ ty_2Enum_2Enum) @ ((ty_2Epair_2Eprod @ ty_2Enum_2Enum) @ ty_2Enum_2Enum))) @ X1)) @ (c_2Epred__set_2EUNIV @ ty_2Enum_2Enum))) @ ((ap @ ((ap @ ((c_2Epred__set_2ECROSS @ ty_2Enum_2Enum) @ ty_2Enum_2Enum)) @ (c_2Epred__set_2EUNIV @ ty_2Enum_2Enum))) @ (c_2Epred__set_2EUNIV @ ty_2Enum_2Enum)))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 166.97/164.79 % SZS output end Proof
%------------------------------------------------------------------------------