%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP004^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 : n001.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:22 PM UTC 2025
% Result : Theorem 169.21s 168.51s
% Output : Proof 169.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ITP004^5 : TPTP v9.2.0. Bugfixed v7.5.0.
% 0.12/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n001.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 18:10:39 EDT 2025
% 0.19/0.34 % CPUTime :
% 169.21/168.51 % SZS status Theorem
% 169.21/168.51 % Mode: mode500:USE_SINE=true:SINE_TOLERANCE=1.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=2.:SINE_DEPTH=0
% 169.21/168.51 % Inferences: 8
% 169.21/168.51 % SZS output start Proof
% 169.21/168.51 thf(conj_thm_2Epred__set_2EREST__SUBSET,conjecture,(![X1:del]:(![X2:$i]:(((mem @ X2) @ ((arr @ X1) @ bool)) => (p @ ((ap @ ((ap @ (c_2Epred__set_2ESUBSET @ X1)) @ ((ap @ (c_2Epred__set_2EREST @ X1)) @ X2))) @ X2)))))).
% 169.21/168.51 thf(h0,negated_conjecture,(~((![X1:del]:(![X2:$i]:(((mem @ X2) @ ((arr @ X1) @ bool)) => (p @ ((ap @ ((ap @ (c_2Epred__set_2ESUBSET @ X1)) @ ((ap @ (c_2Epred__set_2EREST @ X1)) @ X2))) @ X2))))))),inference(assume_negation,[status(cth)],[conj_thm_2Epred__set_2EREST__SUBSET])).
% 169.21/168.51 thf(pax260, axiom, (p260=>![X2:del, X6:del, X4:$i]:(fmem @ X4 @ (farr @ X2 @ X6)=>![X5:$i]:(fmem @ X5 @ X2=>fmem @ (fap @ X4 @ X5) @ X6))), file('<stdin>', pax260)).
% 169.21/168.51 thf(pax67, axiom, (p67=>![X36:del]:fmem @ (fc_2Epred__set_2ECHOICE @ X36) @ (farr @ (farr @ X36 @ fbool) @ X36)), file('<stdin>', pax67)).
% 169.21/168.51 thf(pax63, axiom, (p63=>![X36:del]:fmem @ (fc_2Epred__set_2EREST @ X36) @ (farr @ (farr @ X36 @ fbool) @ (farr @ X36 @ fbool))), file('<stdin>', pax63)).
% 169.21/168.51 thf(pax15, axiom, (p15=>![X36:del, X37:$i]:(fmem @ X37 @ X36=>![X41:$i]:(fmem @ X41 @ (farr @ X36 @ fbool)=>fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ X36) @ (fap @ (fap @ (fc_2Epred__set_2EDELETE @ X36) @ X41) @ X37)) @ X41)))), file('<stdin>', pax15)).
% 169.21/168.51 thf(pax19, axiom, (p19=>![X36:del, X37:$i]:(fmem @ X37 @ X36=>(fap @ (fap @ (fc_2Epred__set_2EDELETE @ X36) @ (fc_2Epred__set_2EEMPTY @ X36)) @ X37)=(fc_2Epred__set_2EEMPTY @ X36))), file('<stdin>', pax19)).
% 169.21/168.51 thf(pax65, axiom, (p65=>![X36:del]:fmem @ (fc_2Epred__set_2EEMPTY @ X36) @ (farr @ X36 @ fbool)), file('<stdin>', pax65)).
% 169.21/168.51 thf(pax6, axiom, (p6=>![X36:del, X37:$i]:(fmem @ X37 @ (farr @ X36 @ fbool)=>(fap @ (fc_2Epred__set_2EREST @ X36) @ X37)=(fap @ (fap @ (fc_2Epred__set_2EDELETE @ X36) @ X37) @ (fap @ (fc_2Epred__set_2ECHOICE @ X36) @ X37)))), file('<stdin>', pax6)).
% 169.21/168.51 thf(pax12, axiom, (p12=>![X36:del, X37:$i]:(fmem @ X37 @ X36=>![X41:$i]:(fmem @ X41 @ (farr @ X36 @ fbool)=>fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ X36) @ X41) @ (fap @ (fap @ (fc_2Epred__set_2EINSERT @ X36) @ X37) @ X41))))), file('<stdin>', pax12)).
% 169.21/168.51 thf(pax2, axiom, (p2=>![X36:del, X37:$i]:(fmem @ X37 @ (farr @ X36 @ fbool)=>(~((X37)=(fc_2Epred__set_2EEMPTY @ X36))=>(fap @ (fap @ (fc_2Epred__set_2EINSERT @ X36) @ (fap @ (fc_2Epred__set_2ECHOICE @ X36) @ X37)) @ (fap @ (fc_2Epred__set_2EREST @ X36) @ X37))=(X37)))), file('<stdin>', pax2)).
% 169.21/168.51 thf(ax10, axiom, p260, file('<stdin>', ax10)).
% 169.21/168.51 thf(ax203, axiom, p67, file('<stdin>', ax203)).
% 169.21/168.51 thf(ax207, axiom, p63, file('<stdin>', ax207)).
% 169.21/168.51 thf(ax255, axiom, p15, file('<stdin>', ax255)).
% 169.21/168.51 thf(ax251, axiom, p19, file('<stdin>', ax251)).
% 169.21/168.51 thf(ax205, axiom, p65, file('<stdin>', ax205)).
% 169.21/168.51 thf(ax264, axiom, p6, file('<stdin>', ax264)).
% 169.21/168.51 thf(nax1, axiom, (p1<=![X36:del, X37:$i]:(fmem @ X37 @ (farr @ X36 @ fbool)=>fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ X36) @ (fap @ (fc_2Epred__set_2EREST @ X36) @ X37)) @ X37))), file('<stdin>', nax1)).
% 169.21/168.51 thf(ax269, axiom, ~(p1), file('<stdin>', ax269)).
% 169.21/168.51 thf(ax258, axiom, p12, file('<stdin>', ax258)).
% 169.21/168.51 thf(ax268, axiom, p2, file('<stdin>', ax268)).
% 169.21/168.51 thf(c_0_20, plain, ![X59:del, X60:del, X61:$i, X62:$i]:(~p260|(~fmem @ X61 @ (farr @ X59 @ X60)|(~fmem @ X62 @ X59|fmem @ (fap @ X61 @ X62) @ X60))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax260])])])).
% 169.21/168.51 thf(c_0_21, plain, ![X518:del]:(~p67|fmem @ (fc_2Epred__set_2ECHOICE @ X518) @ (farr @ (farr @ X518 @ fbool) @ X518)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax67])])])).
% 169.21/168.51 thf(c_0_22, plain, ![X526:del]:(~p63|fmem @ (fc_2Epred__set_2EREST @ X526) @ (farr @ (farr @ X526 @ fbool) @ (farr @ X526 @ fbool))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax63])])])).
% 169.21/168.51 thf(c_0_23, plain, ![X662:del, X663:$i, X664:$i]:(~p15|(~fmem @ X663 @ X662|(~fmem @ X664 @ (farr @ X662 @ fbool)|fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ X662) @ (fap @ (fap @ (fc_2Epred__set_2EDELETE @ X662) @ X664) @ X663)) @ X664)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax15])])])).
% 169.21/168.51 thf(c_0_24, plain, ![X638:del, X639:$i]:(~p19|(~fmem @ X639 @ X638|(fap @ (fap @ (fc_2Epred__set_2EDELETE @ X638) @ (fc_2Epred__set_2EEMPTY @ X638)) @ X639)=(fc_2Epred__set_2EEMPTY @ X638))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax19])])])).
% 169.21/168.51 thf(c_0_25, plain, ![X522:del]:(~p65|fmem @ (fc_2Epred__set_2EEMPTY @ X522) @ (farr @ X522 @ fbool)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax65])])])).
% 169.21/168.51 thf(c_0_26, plain, ![X708:del, X709:$i]:(~p6|(~fmem @ X709 @ (farr @ X708 @ fbool)|(fap @ (fc_2Epred__set_2EREST @ X708) @ X709)=(fap @ (fap @ (fc_2Epred__set_2EDELETE @ X708) @ X709) @ (fap @ (fc_2Epred__set_2ECHOICE @ X708) @ X709)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax6])])])).
% 169.21/168.51 thf(c_0_27, plain, ![X668:del, X669:$i, X670:$i]:(~p12|(~fmem @ X669 @ X668|(~fmem @ X670 @ (farr @ X668 @ fbool)|fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ X668) @ X670) @ (fap @ (fap @ (fc_2Epred__set_2EINSERT @ X668) @ X669) @ X670))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax12])])])).
% 169.21/168.51 thf(c_0_28, plain, ![X716:del, X717:$i]:(~p2|(~fmem @ X717 @ (farr @ X716 @ fbool)|((X717)=(fc_2Epred__set_2EEMPTY @ X716)|(fap @ (fap @ (fc_2Epred__set_2EINSERT @ X716) @ (fap @ (fc_2Epred__set_2ECHOICE @ X716) @ X717)) @ (fap @ (fc_2Epred__set_2EREST @ X716) @ X717))=(X717)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax2])])])])).
% 169.21/168.51 thf(c_0_29, plain, ![X1:$i, X6:del, X3:$i, X2:del]:(fmem @ (fap @ X1 @ X3) @ X6|~p260|~fmem @ X1 @ (farr @ X2 @ X6)|~fmem @ X3 @ X2), inference(split_conjunct,[status(thm)],[c_0_20])).
% 169.21/168.51 thf(c_0_30, plain, p260, inference(split_conjunct,[status(thm)],[ax10])).
% 169.21/168.51 thf(c_0_31, plain, ![X2:del]:(fmem @ (fc_2Epred__set_2ECHOICE @ X2) @ (farr @ (farr @ X2 @ fbool) @ X2)|~p67), inference(split_conjunct,[status(thm)],[c_0_21])).
% 169.21/168.51 thf(c_0_32, plain, p67, inference(split_conjunct,[status(thm)],[ax203])).
% 169.21/168.51 thf(c_0_33, plain, ![X2:del]:(fmem @ (fc_2Epred__set_2EREST @ X2) @ (farr @ (farr @ X2 @ fbool) @ (farr @ X2 @ fbool))|~p63), inference(split_conjunct,[status(thm)],[c_0_22])).
% 169.21/168.51 thf(c_0_34, plain, p63, inference(split_conjunct,[status(thm)],[ax207])).
% 169.21/168.51 thf(c_0_35, plain, ![X1:$i, X3:$i, X2:del]:(fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ X2) @ (fap @ (fap @ (fc_2Epred__set_2EDELETE @ X2) @ X3) @ X1)) @ X3)|~p15|~fmem @ X1 @ X2|~fmem @ X3 @ (farr @ X2 @ fbool)), inference(split_conjunct,[status(thm)],[c_0_23])).
% 169.21/168.51 thf(c_0_36, plain, p15, inference(split_conjunct,[status(thm)],[ax255])).
% 169.21/168.51 thf(c_0_37, plain, ![X1:$i, X2:del]:((fap @ (fap @ (fc_2Epred__set_2EDELETE @ X2) @ (fc_2Epred__set_2EEMPTY @ X2)) @ X1)=(fc_2Epred__set_2EEMPTY @ X2)|~p19|~fmem @ X1 @ X2), inference(split_conjunct,[status(thm)],[c_0_24])).
% 169.21/168.51 thf(c_0_38, plain, p19, inference(split_conjunct,[status(thm)],[ax251])).
% 169.21/168.51 thf(c_0_39, plain, ![X2:del]:(fmem @ (fc_2Epred__set_2EEMPTY @ X2) @ (farr @ X2 @ fbool)|~p65), inference(split_conjunct,[status(thm)],[c_0_25])).
% 169.21/168.51 thf(c_0_40, plain, p65, inference(split_conjunct,[status(thm)],[ax205])).
% 169.21/168.51 thf(c_0_41, plain, ![X1:$i, X2:del]:((fap @ (fc_2Epred__set_2EREST @ X2) @ X1)=(fap @ (fap @ (fc_2Epred__set_2EDELETE @ X2) @ X1) @ (fap @ (fc_2Epred__set_2ECHOICE @ X2) @ X1))|~p6|~fmem @ X1 @ (farr @ X2 @ fbool)), inference(split_conjunct,[status(thm)],[c_0_26])).
% 169.21/168.51 thf(c_0_42, plain, p6, inference(split_conjunct,[status(thm)],[ax264])).
% 169.21/168.51 thf(c_0_43, plain, ((fmem @ esk340_0 @ (farr @ esk339_0 @ fbool)|p1)&(~fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ esk339_0) @ (fap @ (fc_2Epred__set_2EREST @ esk339_0) @ esk340_0)) @ esk340_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])])])])])).
% 169.21/168.51 thf(c_0_44, plain, ~p1, inference(fof_simplification,[status(thm)],[ax269])).
% 169.21/168.51 thf(c_0_45, plain, ![X1:$i, X3:$i, X2:del]:(fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ X2) @ X3) @ (fap @ (fap @ (fc_2Epred__set_2EINSERT @ X2) @ X1) @ X3))|~p12|~fmem @ X1 @ X2|~fmem @ X3 @ (farr @ X2 @ fbool)), inference(split_conjunct,[status(thm)],[c_0_27])).
% 169.21/168.51 thf(c_0_46, plain, p12, inference(split_conjunct,[status(thm)],[ax258])).
% 169.21/168.51 thf(c_0_47, plain, ![X1:$i, X2:del]:((X1)=(fc_2Epred__set_2EEMPTY @ X2)|(fap @ (fap @ (fc_2Epred__set_2EINSERT @ X2) @ (fap @ (fc_2Epred__set_2ECHOICE @ X2) @ X1)) @ (fap @ (fc_2Epred__set_2EREST @ X2) @ X1))=(X1)|~p2|~fmem @ X1 @ (farr @ X2 @ fbool)), inference(split_conjunct,[status(thm)],[c_0_28])).
% 169.21/168.51 thf(c_0_48, plain, p2, inference(split_conjunct,[status(thm)],[ax268])).
% 169.21/168.51 thf(c_0_49, plain, ![X1:$i, X2:del, X3:$i, X6:del]:(fmem @ (fap @ X1 @ X3) @ X2|~fmem @ X1 @ (farr @ X6 @ X2)|~fmem @ X3 @ X6), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_30])])).
% 169.21/168.51 thf(c_0_50, plain, ![X2:del]:fmem @ (fc_2Epred__set_2ECHOICE @ X2) @ (farr @ (farr @ X2 @ fbool) @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32])])).
% 169.21/168.51 thf(c_0_51, plain, ![X2:del]:fmem @ (fc_2Epred__set_2EREST @ X2) @ (farr @ (farr @ X2 @ fbool) @ (farr @ X2 @ fbool)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 169.21/168.51 thf(c_0_52, plain, ![X1:$i, X3:$i, X2:del]:(fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ X2) @ (fap @ (fap @ (fc_2Epred__set_2EDELETE @ X2) @ X1) @ X3)) @ X1)|~fmem @ X1 @ (farr @ X2 @ fbool)|~fmem @ X3 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 169.21/168.51 thf(c_0_53, plain, ![X1:$i, X2:del]:((fap @ (fap @ (fc_2Epred__set_2EDELETE @ X2) @ (fc_2Epred__set_2EEMPTY @ X2)) @ X1)=(fc_2Epred__set_2EEMPTY @ X2)|~fmem @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38])])).
% 169.21/168.51 thf(c_0_54, plain, ![X2:del]:fmem @ (fc_2Epred__set_2EEMPTY @ X2) @ (farr @ X2 @ fbool), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_40])])).
% 169.21/168.51 thf(c_0_55, plain, ![X1:$i, X2:del]:((fap @ (fap @ (fc_2Epred__set_2EDELETE @ X2) @ X1) @ (fap @ (fc_2Epred__set_2ECHOICE @ X2) @ X1))=(fap @ (fc_2Epred__set_2EREST @ X2) @ X1)|~fmem @ X1 @ (farr @ X2 @ fbool)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_42])])).
% 169.21/168.51 thf(c_0_56, plain, (p1|~fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ esk339_0) @ (fap @ (fc_2Epred__set_2EREST @ esk339_0) @ esk340_0)) @ esk340_0)), inference(split_conjunct,[status(thm)],[c_0_43])).
% 169.21/168.51 thf(c_0_57, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_44])).
% 169.21/168.51 thf(c_0_58, plain, ![X1:$i, X3:$i, X2:del]:(fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ X2) @ X1) @ (fap @ (fap @ (fc_2Epred__set_2EINSERT @ X2) @ X3) @ X1))|~fmem @ X1 @ (farr @ X2 @ fbool)|~fmem @ X3 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_46])])).
% 169.21/168.51 thf(c_0_59, plain, ![X1:$i, X2:del]:((fap @ (fap @ (fc_2Epred__set_2EINSERT @ X2) @ (fap @ (fc_2Epred__set_2ECHOICE @ X2) @ X1)) @ (fap @ (fc_2Epred__set_2EREST @ X2) @ X1))=(X1)|(X1)=(fc_2Epred__set_2EEMPTY @ X2)|~fmem @ X1 @ (farr @ X2 @ fbool)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_47, c_0_48])])).
% 169.21/168.51 thf(c_0_60, plain, ![X1:$i, X2:del]:(fmem @ (fap @ (fc_2Epred__set_2ECHOICE @ X2) @ X1) @ X2|~fmem @ X1 @ (farr @ X2 @ fbool)), inference(spm,[status(thm)],[c_0_49, c_0_50])).
% 169.21/168.51 thf(c_0_61, plain, ![X1:$i, X2:del]:(fmem @ (fap @ (fc_2Epred__set_2EREST @ X2) @ X1) @ (farr @ X2 @ fbool)|~fmem @ X1 @ (farr @ X2 @ fbool)), inference(spm,[status(thm)],[c_0_49, c_0_51])).
% 169.21/168.51 thf(c_0_62, plain, (fmem @ esk340_0 @ (farr @ esk339_0 @ fbool)|p1), inference(split_conjunct,[status(thm)],[c_0_43])).
% 169.21/168.51 thf(c_0_63, plain, ![X1:$i, X2:del]:(fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ X2) @ (fc_2Epred__set_2EEMPTY @ X2)) @ (fc_2Epred__set_2EEMPTY @ X2))|~fmem @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_53]), c_0_54])])).
% 169.21/168.51 thf(c_0_64, plain, ![X2:del]:((fap @ (fc_2Epred__set_2EREST @ X2) @ (fc_2Epred__set_2EEMPTY @ X2))=(fc_2Epred__set_2EEMPTY @ X2)|~fmem @ (fap @ (fc_2Epred__set_2ECHOICE @ X2) @ (fc_2Epred__set_2EEMPTY @ X2)) @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53, c_0_55]), c_0_54])])).
% 169.21/168.51 thf(c_0_65, plain, ~fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ esk339_0) @ (fap @ (fc_2Epred__set_2EREST @ esk339_0) @ esk340_0)) @ esk340_0), inference(sr,[status(thm)],[c_0_56, c_0_57])).
% 169.21/168.51 thf(c_0_66, plain, ![X1:$i, X2:del]:((X1)=(fc_2Epred__set_2EEMPTY @ X2)|fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ X2) @ (fap @ (fc_2Epred__set_2EREST @ X2) @ X1)) @ X1)|~fmem @ X1 @ (farr @ X2 @ fbool)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_59]), c_0_60]), c_0_61])).
% 169.21/168.51 thf(c_0_67, plain, fmem @ esk340_0 @ (farr @ esk339_0 @ fbool), inference(sr,[status(thm)],[c_0_62, c_0_57])).
% 169.21/168.51 thf(c_0_68, plain, ![X1:$i, X2:del]:(fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ X2) @ (fc_2Epred__set_2EEMPTY @ X2)) @ (fc_2Epred__set_2EEMPTY @ X2))|~fmem @ X1 @ (farr @ X2 @ fbool)), inference(spm,[status(thm)],[c_0_63, c_0_60])).
% 169.21/168.51 thf(c_0_69, plain, ![X2:del]:(fap @ (fc_2Epred__set_2EREST @ X2) @ (fc_2Epred__set_2EEMPTY @ X2))=(fc_2Epred__set_2EEMPTY @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_60]), c_0_54])])).
% 169.21/168.51 thf(c_0_70, plain, (fc_2Epred__set_2EEMPTY @ esk339_0)=(esk340_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_66]), c_0_67])])).
% 169.21/168.51 thf(c_0_71, plain, ![X2:del]:fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ X2) @ (fc_2Epred__set_2EEMPTY @ X2)) @ (fc_2Epred__set_2EEMPTY @ X2)), inference(spm,[status(thm)],[c_0_68, c_0_54])).
% 169.21/168.51 thf(c_0_72, plain, (fap @ (fc_2Epred__set_2EREST @ esk339_0) @ esk340_0)=(esk340_0), inference(spm,[status(thm)],[c_0_69, c_0_70])).
% 169.21/168.51 thf(c_0_73, plain, fp @ (fap @ (fap @ (fc_2Epred__set_2ESUBSET @ esk339_0) @ esk340_0) @ esk340_0), inference(spm,[status(thm)],[c_0_71, c_0_70])).
% 169.21/168.51 thf(c_0_74, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_65, c_0_72]), c_0_73])]), ['proof']).
% 169.21/168.51 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 169.21/168.51 thf(0,theorem,(![X1:del]:(![X2:$i]:(((mem @ X2) @ ((arr @ X1) @ bool)) => (p @ ((ap @ ((ap @ (c_2Epred__set_2ESUBSET @ X1)) @ ((ap @ (c_2Epred__set_2EREST @ X1)) @ X2))) @ X2))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 169.21/168.51 % SZS output end Proof
%------------------------------------------------------------------------------