%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP020^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 : n023.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:39 PM UTC 2025
% Result : Theorem 261.67s 260.68s
% Output : Proof 261.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : ITP020^5 : TPTP v9.2.0. Bugfixed v7.5.0.
% 0.06/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n023.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 8 17:50:10 EDT 2025
% 0.12/0.34 % CPUTime :
% 261.67/260.68 % SZS status Theorem
% 261.67/260.68 % Mode: mode444:USE_SINE=true:SINE_TOLERANCE=1.0:SINE_GENERALITY_THRESHOLD=4:SINE_RANK_LIMIT=1.:SINE_DEPTH=0
% 261.67/260.68 % Inferences: 241
% 261.67/260.68 % SZS output start Proof
% 261.67/260.68 thf(ty_del, type, del : $tType).
% 261.67/260.68 thf(ty_c_2Epred__set_2ECROSS, type, c_2Epred__set_2ECROSS : (del>del>$i)).
% 261.67/260.68 thf(ty_p, type, p : ($i>$o)).
% 261.67/260.68 thf(ty_mem, type, mem : ($i>del>$o)).
% 261.67/260.68 thf(ty_c_2Epred__set_2EUNIV, type, c_2Epred__set_2EUNIV : (del>$i)).
% 261.67/260.68 thf(ty_eigen__0, type, eigen__0 : $i).
% 261.67/260.68 thf(ty_ap, type, ap : ($i>$i>$i)).
% 261.67/260.68 thf(ty_ty_2Epair_2Eprod, type, ty_2Epair_2Eprod : (del>del>del)).
% 261.67/260.68 thf(ty_c_2Epred__set_2EBIJ, type, c_2Epred__set_2EBIJ : (del>del>$i)).
% 261.67/260.68 thf(ty_ty_2Enum_2Enum, type, ty_2Enum_2Enum : del).
% 261.67/260.68 thf(ty_arr, type, arr : (del>del>del)).
% 261.67/260.68 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))))))))))).
% 261.67/260.68 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])).
% 261.67/260.68 thf(h1,assumption,(~((((mem @ eigen__0) @ ((arr @ ((ty_2Epair_2Eprod @ ty_2Enum_2Enum) @ ty_2Enum_2Enum)) @ ty_2Enum_2Enum)) => (~((p @ ((ap @ ((ap @ ((ap @ ((c_2Epred__set_2EBIJ @ ((ty_2Epair_2Eprod @ ty_2Enum_2Enum) @ ty_2Enum_2Enum)) @ ty_2Enum_2Enum)) @ eigen__0)) @ ((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)))) @ (c_2Epred__set_2EUNIV @ ty_2Enum_2Enum)))))))),introduced(assumption,[])).
% 261.67/260.68 thf(h2,assumption,((mem @ eigen__0) @ ((arr @ ((ty_2Epair_2Eprod @ ty_2Enum_2Enum) @ ty_2Enum_2Enum)) @ ty_2Enum_2Enum)),introduced(assumption,[])).
% 261.67/260.68 thf(h3,assumption,(p @ ((ap @ ((ap @ ((ap @ ((c_2Epred__set_2EBIJ @ ((ty_2Epair_2Eprod @ ty_2Enum_2Enum) @ ty_2Enum_2Enum)) @ ty_2Enum_2Enum)) @ eigen__0)) @ ((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)))) @ (c_2Epred__set_2EUNIV @ ty_2Enum_2Enum))),introduced(assumption,[])).
% 261.67/260.68 thf(pax68, axiom, (p68=>![X58:del, X72:del]:(fc_2Epred__set_2EUNIV @ (fty_2Epair_2Eprod @ X58 @ X72))=(fap @ (fap @ (fc_2Epred__set_2ECROSS @ X58 @ X72) @ (fc_2Epred__set_2EUNIV @ X58)) @ (fc_2Epred__set_2EUNIV @ X72))), file('<stdin>', pax68)).
% 261.67/260.68 thf(pax1, axiom, (p1=>![X93:$i]:(fmem @ X93 @ (farr @ fty_2Enum_2Enum @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum))=>~(fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ fty_2Enum_2Enum @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum)) @ X93) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum)) @ (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)))))), file('<stdin>', pax1)).
% 261.67/260.68 thf(ax262, axiom, p68, file('<stdin>', ax262)).
% 261.67/260.68 thf(pax94, axiom, (p94=>![X58:del, X61:del, X66:$i]:(fmem @ X66 @ (farr @ X58 @ X61)=>![X43:$i]:(fmem @ X43 @ (farr @ X58 @ fbool)=>![X45:$i]:(fmem @ X45 @ (farr @ X61 @ fbool)=>(fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ X58 @ X61) @ X66) @ X43) @ X45)=>~(![X9:$i]:(~((~((fmem @ X9 @ (farr @ X61 @ X58)=>~(fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ X61 @ X58) @ X9) @ X45) @ X43))))=>~(![X31:$i]:(fmem @ X31 @ X58=>(fp @ (fap @ (fap @ (fc_2Ebool_2EIN @ X58) @ X31) @ X43)=>(fap @ (fap @ (fap @ (fc_2Ecombin_2Eo @ X58 @ X58 @ X61) @ X9) @ X66) @ X31)=(X31))))))=>~(![X31:$i]:(fmem @ X31 @ X61=>(fp @ (fap @ (fap @ (fc_2Ebool_2EIN @ X61) @ X31) @ X45)=>(fap @ (fap @ (fap @ (fc_2Ecombin_2Eo @ X61 @ X61 @ X58) @ X66) @ X9) @ X31)=(X31))))))))))), file('<stdin>', pax94)).
% 261.67/260.68 thf(pax113, axiom, (p113=>![X58:del]:fmem @ (fc_2Epred__set_2EUNIV @ X58) @ (farr @ X58 @ fbool)), file('<stdin>', pax113)).
% 261.67/260.68 thf(ax329, axiom, p1, file('<stdin>', ax329)).
% 261.67/260.68 thf(ax236, axiom, p94, file('<stdin>', ax236)).
% 261.67/260.68 thf(ax217, axiom, p113, file('<stdin>', ax217)).
% 261.67/260.68 thf(pax2, axiom, (p2=>fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fty_2Enum_2Enum) @ f__0) @ (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))) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum))), file('<stdin>', pax2)).
% 261.67/260.68 thf(pax3, axiom, (p3=>fmem @ f__0 @ (farr @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fty_2Enum_2Enum)), file('<stdin>', pax3)).
% 261.67/260.68 thf(ax328, axiom, p2, file('<stdin>', ax328)).
% 261.67/260.68 thf(ax327, axiom, p3, file('<stdin>', ax327)).
% 261.67/260.68 thf(c_0_12, plain, ![X2150:del, X2151:del]:(~p68|(fc_2Epred__set_2EUNIV @ (fty_2Epair_2Eprod @ X2150 @ X2151))=(fap @ (fap @ (fc_2Epred__set_2ECROSS @ X2150 @ X2151) @ (fc_2Epred__set_2EUNIV @ X2150)) @ (fc_2Epred__set_2EUNIV @ X2151))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax68])])])).
% 261.67/260.68 thf(c_0_13, plain, ![X2340:$i]:(~p1|(~fmem @ X2340 @ (farr @ fty_2Enum_2Enum @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum))|~fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ fty_2Enum_2Enum @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum)) @ X2340) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum)) @ (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))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax1])])])])).
% 261.67/260.68 thf(c_0_14, plain, ![X6:del, X8:del]:((fc_2Epred__set_2EUNIV @ (fty_2Epair_2Eprod @ X6 @ X8))=(fap @ (fap @ (fc_2Epred__set_2ECROSS @ X6 @ X8) @ (fc_2Epred__set_2EUNIV @ X6)) @ (fc_2Epred__set_2EUNIV @ X8))|~p68), inference(split_conjunct,[status(thm)],[c_0_12])).
% 261.67/260.68 thf(c_0_15, plain, p68, inference(split_conjunct,[status(thm)],[ax262])).
% 261.67/260.68 thf(c_0_16, plain, ![X1982:del, X1983:del, X1984:$i, X1985:$i, X1986:$i, X1988:$i, X1989:$i]:((((fmem @ (esk945_5 @ X1982 @ X1983 @ X1984 @ X1985 @ X1986) @ (farr @ X1983 @ X1982)|~fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ X1982 @ X1983) @ X1984) @ X1985) @ X1986)|~fmem @ X1986 @ (farr @ X1983 @ fbool)|~fmem @ X1985 @ (farr @ X1982 @ fbool)|~fmem @ X1984 @ (farr @ X1982 @ X1983)|~p94)&(fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ X1983 @ X1982) @ (esk945_5 @ X1982 @ X1983 @ X1984 @ X1985 @ X1986)) @ X1986) @ X1985)|~fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ X1982 @ X1983) @ X1984) @ X1985) @ X1986)|~fmem @ X1986 @ (farr @ X1983 @ fbool)|~fmem @ X1985 @ (farr @ X1982 @ fbool)|~fmem @ X1984 @ (farr @ X1982 @ X1983)|~p94))&(~fmem @ X1988 @ X1982|(~fp @ (fap @ (fap @ (fc_2Ebool_2EIN @ X1982) @ X1988) @ X1985)|(fap @ (fap @ (fap @ (fc_2Ecombin_2Eo @ X1982 @ X1982 @ X1983) @ (esk945_5 @ X1982 @ X1983 @ X1984 @ X1985 @ X1986)) @ X1984) @ X1988)=(X1988))|~fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ X1982 @ X1983) @ X1984) @ X1985) @ X1986)|~fmem @ X1986 @ (farr @ X1983 @ fbool)|~fmem @ X1985 @ (farr @ X1982 @ fbool)|~fmem @ X1984 @ (farr @ X1982 @ X1983)|~p94))&(~fmem @ X1989 @ X1983|(~fp @ (fap @ (fap @ (fc_2Ebool_2EIN @ X1983) @ X1989) @ X1986)|(fap @ (fap @ (fap @ (fc_2Ecombin_2Eo @ X1983 @ X1983 @ X1982) @ X1984) @ (esk945_5 @ X1982 @ X1983 @ X1984 @ X1985 @ X1986)) @ X1989)=(X1989))|~fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ X1982 @ X1983) @ X1984) @ X1985) @ X1986)|~fmem @ X1986 @ (farr @ X1983 @ fbool)|~fmem @ X1985 @ (farr @ X1982 @ fbool)|~fmem @ X1984 @ (farr @ X1982 @ X1983)|~p94)), 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)],[pax94])])])])])])).
% 261.67/260.68 thf(c_0_17, plain, ![X1878:del]:(~p113|fmem @ (fc_2Epred__set_2EUNIV @ X1878) @ (farr @ X1878 @ fbool)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax113])])])).
% 261.67/260.68 thf(c_0_18, plain, ![X1:$i]:(~p1|~fmem @ X1 @ (farr @ fty_2Enum_2Enum @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum))|~fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ fty_2Enum_2Enum @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum)) @ X1) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum)) @ (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)))), inference(split_conjunct,[status(thm)],[c_0_13])).
% 261.67/260.68 thf(c_0_19, plain, p1, inference(split_conjunct,[status(thm)],[ax329])).
% 261.67/260.68 thf(c_0_20, plain, ![X6:del, X8:del]:(fap @ (fap @ (fc_2Epred__set_2ECROSS @ X6 @ X8) @ (fc_2Epred__set_2EUNIV @ X6)) @ (fc_2Epred__set_2EUNIV @ X8))=(fc_2Epred__set_2EUNIV @ (fty_2Epair_2Eprod @ X6 @ X8)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_14, c_0_15])])).
% 261.67/260.68 thf(c_0_21, plain, ![X2:$i, X1:$i, X3:$i, X8:del, X6:del]:(fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ X6 @ X8) @ (esk945_5 @ X8 @ X6 @ X1 @ X2 @ X3)) @ X3) @ X2)|~fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ X8 @ X6) @ X1) @ X2) @ X3)|~fmem @ X3 @ (farr @ X6 @ fbool)|~fmem @ X2 @ (farr @ X8 @ fbool)|~fmem @ X1 @ (farr @ X8 @ X6)|~p94), inference(split_conjunct,[status(thm)],[c_0_16])).
% 261.67/260.68 thf(c_0_22, plain, p94, inference(split_conjunct,[status(thm)],[ax236])).
% 261.67/260.68 thf(c_0_23, plain, ![X6:del]:(fmem @ (fc_2Epred__set_2EUNIV @ X6) @ (farr @ X6 @ fbool)|~p113), inference(split_conjunct,[status(thm)],[c_0_17])).
% 261.67/260.68 thf(c_0_24, plain, p113, inference(split_conjunct,[status(thm)],[ax217])).
% 261.67/260.68 thf(c_0_25, plain, ![X1:$i]:(~fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ fty_2Enum_2Enum @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum)) @ X1) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum)) @ (fc_2Epred__set_2EUNIV @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum)))|~fmem @ X1 @ (farr @ fty_2Enum_2Enum @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_18, c_0_19]), c_0_20])])).
% 261.67/260.68 thf(c_0_26, plain, ![X2:$i, X1:$i, X3:$i, X8:del, X6:del]:(fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ X6 @ X8) @ (esk945_5 @ X8 @ X6 @ X1 @ X2 @ X3)) @ X3) @ X2)|~fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ X8 @ X6) @ X1) @ X2) @ X3)|~fmem @ X3 @ (farr @ X6 @ fbool)|~fmem @ X2 @ (farr @ X8 @ fbool)|~fmem @ X1 @ (farr @ X8 @ X6)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_22])])).
% 261.67/260.68 thf(c_0_27, plain, ![X6:del]:fmem @ (fc_2Epred__set_2EUNIV @ X6) @ (farr @ X6 @ fbool), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_24])])).
% 261.67/260.68 thf(c_0_28, plain, ![X1:$i, X3:$i, X2:$i, X6:del, X8:del]:(fmem @ (esk945_5 @ X6 @ X8 @ X1 @ X2 @ X3) @ (farr @ X8 @ X6)|~fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ X6 @ X8) @ X1) @ X2) @ X3)|~fmem @ X3 @ (farr @ X8 @ fbool)|~fmem @ X2 @ (farr @ X6 @ fbool)|~fmem @ X1 @ (farr @ X6 @ X8)|~p94), inference(split_conjunct,[status(thm)],[c_0_16])).
% 261.67/260.68 thf(c_0_29, plain, (~p2|fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fty_2Enum_2Enum) @ f__0) @ (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))) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum))), inference(fof_nnf,[status(thm)],[pax2])).
% 261.67/260.68 thf(c_0_30, plain, (~p3|fmem @ f__0 @ (farr @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fty_2Enum_2Enum)), inference(fof_nnf,[status(thm)],[pax3])).
% 261.67/260.68 thf(c_0_31, plain, ![X1:$i]:(~fmem @ (esk945_5 @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fty_2Enum_2Enum @ X1 @ (fc_2Epred__set_2EUNIV @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum)) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum)) @ (farr @ fty_2Enum_2Enum @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum))|~fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fty_2Enum_2Enum) @ X1) @ (fc_2Epred__set_2EUNIV @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum))) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum))|~fmem @ X1 @ (farr @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fty_2Enum_2Enum)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25, c_0_26]), c_0_27]), c_0_27])])).
% 261.67/260.68 thf(c_0_32, plain, ![X1:$i, X3:$i, X2:$i, X6:del, X8:del]:(fmem @ (esk945_5 @ X6 @ X8 @ X1 @ X2 @ X3) @ (farr @ X8 @ X6)|~fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ X6 @ X8) @ X1) @ X2) @ X3)|~fmem @ X3 @ (farr @ X8 @ fbool)|~fmem @ X2 @ (farr @ X6 @ fbool)|~fmem @ X1 @ (farr @ X6 @ X8)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_22])])).
% 261.67/260.68 thf(c_0_33, plain, (fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fty_2Enum_2Enum) @ f__0) @ (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))) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum))|~p2), inference(split_conjunct,[status(thm)],[c_0_29])).
% 261.67/260.68 thf(c_0_34, plain, p2, inference(split_conjunct,[status(thm)],[ax328])).
% 261.67/260.68 thf(c_0_35, plain, (fmem @ f__0 @ (farr @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fty_2Enum_2Enum)|~p3), inference(split_conjunct,[status(thm)],[c_0_30])).
% 261.67/260.68 thf(c_0_36, plain, p3, inference(split_conjunct,[status(thm)],[ax327])).
% 261.67/260.68 thf(c_0_37, plain, ![X1:$i]:(~fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fty_2Enum_2Enum) @ X1) @ (fc_2Epred__set_2EUNIV @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum))) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum))|~fmem @ X1 @ (farr @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fty_2Enum_2Enum)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_32]), c_0_27]), c_0_27])])).
% 261.67/260.68 thf(c_0_38, plain, fp @ (fap @ (fap @ (fap @ (fc_2Epred__set_2EBIJ @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fty_2Enum_2Enum) @ f__0) @ (fc_2Epred__set_2EUNIV @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum))) @ (fc_2Epred__set_2EUNIV @ fty_2Enum_2Enum)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_20]), c_0_34])])).
% 261.67/260.68 thf(c_0_39, plain, fmem @ f__0 @ (farr @ (fty_2Epair_2Eprod @ fty_2Enum_2Enum @ fty_2Enum_2Enum) @ fty_2Enum_2Enum), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 261.67/260.68 thf(c_0_40, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39])]), ['proof']).
% 261.67/260.68 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h2,h3,h1,h0])],[])).
% 261.67/260.68 thf(2,plain,$false,inference(tab_negimp,[status(thm),assumptions([h1,h0]),tab_negimp(discharge,[h2,h3])],[h1,1,h2,h3])).
% 261.67/260.68 thf(conj_thm_2Eutil__prob_2ENUM__2D__BIJ,axiom,(~((![X1:$i]:(((mem @ X1) @ ((arr @ ((ty_2Epair_2Eprod @ ty_2Enum_2Enum) @ ty_2Enum_2Enum)) @ ty_2Enum_2Enum)) => (~((p @ ((ap @ ((ap @ ((ap @ ((c_2Epred__set_2EBIJ @ ((ty_2Epair_2Eprod @ ty_2Enum_2Enum) @ ty_2Enum_2Enum)) @ ty_2Enum_2Enum)) @ X1)) @ ((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)))) @ (c_2Epred__set_2EUNIV @ ty_2Enum_2Enum)))))))))).
% 261.67/260.68 thf(3,plain,$false,inference(tab_negall,[status(thm),assumptions([h0]),tab_negall(discharge,[h1]),tab_negall(eigenvar,eigen__0)],[conj_thm_2Eutil__prob_2ENUM__2D__BIJ,2,h1])).
% 261.67/260.68 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])],[3,h0])).
% 261.67/260.68 % SZS output end Proof
%------------------------------------------------------------------------------