%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SET914^7 : TPTP v9.2.0. Released v5.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 02:26:33 PM UTC 2025
% Result : Theorem 168.66s 164.86s
% Output : Proof 168.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SET914^7 : TPTP v9.2.0. Released v5.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 14:28:23 EDT 2025
% 0.12/0.34 % CPUTime :
% 62.51/59.90 slave returned with unknown status
% 168.66/164.86 % SZS status Theorem
% 168.66/164.86 % Mode: mode500:USE_SINE=true:SINE_TOLERANCE=1.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=2.:SINE_DEPTH=0
% 168.66/164.86 % Inferences: 5
% 168.66/164.86 % SZS output start Proof
% 168.66/164.86 thf(def_mnot,definition,(mnot = (^[X1:$i>$o]:(^[X2:$i]:(~((X1 @ X2))))))).
% 168.66/164.86 thf(def_mor,definition,(mor = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:((~((X1 @ X3))) => (X2 @ X3))))))).
% 168.66/164.86 thf(def_mand,definition,(mand = (^[X1:$i>$o]:(^[X2:$i>$o]:(mnot @ ((mor @ (mnot @ X1)) @ (mnot @ X2))))))).
% 168.66/164.86 thf(def_mimplies,definition,(mimplies = (^[X1:$i>$o]:(mor @ (mnot @ X1))))).
% 168.66/164.86 thf(def_mequiv,definition,(mequiv = (^[X1:$i>$o]:(^[X2:$i>$o]:((mand @ ((mimplies @ X1) @ X2)) @ ((mimplies @ X2) @ X1)))))).
% 168.66/164.86 thf(def_mforall_ind,definition,(mforall_ind = (^[X1:mu>$i>$o]:(^[X2:$i]:(![X3:mu]:(((exists_in_world @ X3) @ X2) => ((X1 @ X3) @ X2))))))).
% 168.66/164.86 thf(def_mexists_ind,definition,(mexists_ind = (^[X1:mu>$i>$o]:(mnot @ (mforall_ind @ (^[X2:mu]:(mnot @ (X1 @ X2)))))))).
% 168.66/164.86 thf(def_mvalid,definition,(mvalid = (!!))).
% 168.66/164.86 thf(t55_zfmisc_1,conjecture,(![X1:$i]:(![X2:mu]:(((exists_in_world @ X2) @ X1) => (![X3:mu]:(((exists_in_world @ X3) @ X1) => (![X4:mu]:(((exists_in_world @ X4) @ X1) => (~((~(((~((~((((disjoint @ ((unordered_pair @ X2) @ X3)) @ X4) @ X1))))) => (~((((in @ X2) @ X4) @ X1)))))))))))))))).
% 168.66/164.86 thf(h0,negated_conjecture,(~((![X1:$i]:(![X2:mu]:(((exists_in_world @ X2) @ X1) => (![X3:mu]:(((exists_in_world @ X3) @ X1) => (![X4:mu]:(((exists_in_world @ X4) @ X1) => ((((disjoint @ ((unordered_pair @ X2) @ X3)) @ X4) @ X1) => (~((((in @ X2) @ X4) @ X1))))))))))))),inference(assume_negation,[status(cth)],[t55_zfmisc_1])).
% 168.66/164.86 thf(pax25, axiom, (p25=>![X9:$i, X10:mu]:(fexists_in_world @ X10 @ X9=>fqmltpeq @ X10 @ X10 @ X9)), file('<stdin>', pax25)).
% 168.66/164.86 thf(pax27, axiom, (p27=>![X9:$i, X10:mu, X11:mu]:fexists_in_world @ (fset_intersection2 @ X10 @ X11) @ X9), file('<stdin>', pax27)).
% 168.66/164.86 thf(pax8, axiom, (p8=>![X9:$i, X10:mu]:(fexists_in_world @ X10 @ X9=>![X11:mu]:(fexists_in_world @ X11 @ X9=>![X12:mu]:(fexists_in_world @ X12 @ X9=>~(((fqmltpeq @ X12 @ (fset_intersection2 @ X10 @ X11) @ X9=>![X13:mu]:(fexists_in_world @ X13 @ X9=>~(((fin @ X13 @ X12 @ X9=>~((fin @ X13 @ X10 @ X9=>~(fin @ X13 @ X11 @ X9))))=>~((~((fin @ X13 @ X10 @ X9=>~(fin @ X13 @ X11 @ X9)))=>fin @ X13 @ X12 @ X9))))))=>~((![X13:mu]:(fexists_in_world @ X13 @ X9=>~(((fin @ X13 @ X12 @ X9=>~((fin @ X13 @ X10 @ X9=>~(fin @ X13 @ X11 @ X9))))=>~((~((fin @ X13 @ X10 @ X9=>~(fin @ X13 @ X11 @ X9)))=>fin @ X13 @ X12 @ X9)))))=>fqmltpeq @ X12 @ (fset_intersection2 @ X10 @ X11) @ X9)))))))), file('<stdin>', pax8)).
% 168.66/164.86 thf(ax6, axiom, p25, file('<stdin>', ax6)).
% 168.66/164.86 thf(ax4, axiom, p27, file('<stdin>', ax4)).
% 168.66/164.86 thf(pax10, axiom, (p10=>![X9:$i, X10:mu]:(fexists_in_world @ X10 @ X9=>~(((fqmltpeq @ X10 @ fempty_set @ X9=>![X11:mu]:(fexists_in_world @ X11 @ X9=>~(fin @ X11 @ X10 @ X9)))=>~((![X11:mu]:(fexists_in_world @ X11 @ X9=>~(fin @ X11 @ X10 @ X9))=>fqmltpeq @ X10 @ fempty_set @ X9)))))), file('<stdin>', pax10)).
% 168.66/164.86 thf(ax23, axiom, p8, file('<stdin>', ax23)).
% 168.66/164.86 thf(ax21, axiom, p10, file('<stdin>', ax21)).
% 168.66/164.86 thf(pax7, axiom, (p7=>![X9:$i, X10:mu]:(fexists_in_world @ X10 @ X9=>![X11:mu]:(fexists_in_world @ X11 @ X9=>~(((fdisjoint @ X10 @ X11 @ X9=>fqmltpeq @ (fset_intersection2 @ X10 @ X11) @ fempty_set @ X9)=>~((fqmltpeq @ (fset_intersection2 @ X10 @ X11) @ fempty_set @ X9=>fdisjoint @ X10 @ X11 @ X9))))))), file('<stdin>', pax7)).
% 168.66/164.86 thf(ax24, axiom, p7, file('<stdin>', ax24)).
% 168.66/164.86 thf(nax1, axiom, (p1<=![X9:$i, X10:mu]:(fexists_in_world @ X10 @ X9=>![X11:mu]:(fexists_in_world @ X11 @ X9=>![X12:mu]:(fexists_in_world @ X12 @ X9=>(fdisjoint @ (funordered_pair @ X10 @ X11) @ X12 @ X9=>~(fin @ X10 @ X12 @ X9)))))), file('<stdin>', nax1)).
% 168.66/164.86 thf(ax30, axiom, ~(p1), file('<stdin>', ax30)).
% 168.66/164.86 thf(pax26, axiom, (p26=>![X9:$i, X10:mu, X11:mu]:fexists_in_world @ (funordered_pair @ X10 @ X11) @ X9), file('<stdin>', pax26)).
% 168.66/164.86 thf(pax9, axiom, (p9=>![X9:$i, X10:mu]:(fexists_in_world @ X10 @ X9=>![X11:mu]:(fexists_in_world @ X11 @ X9=>![X12:mu]:(fexists_in_world @ X12 @ X9=>~(((fqmltpeq @ X12 @ (funordered_pair @ X10 @ X11) @ X9=>![X13:mu]:(fexists_in_world @ X13 @ X9=>~(((fin @ X13 @ X12 @ X9=>(~(fqmltpeq @ X13 @ X10 @ X9)=>fqmltpeq @ X13 @ X11 @ X9))=>~(((~(fqmltpeq @ X13 @ X10 @ X9)=>fqmltpeq @ X13 @ X11 @ X9)=>fin @ X13 @ X12 @ X9))))))=>~((![X13:mu]:(fexists_in_world @ X13 @ X9=>~(((fin @ X13 @ X12 @ X9=>(~(fqmltpeq @ X13 @ X10 @ X9)=>fqmltpeq @ X13 @ X11 @ X9))=>~(((~(fqmltpeq @ X13 @ X10 @ X9)=>fqmltpeq @ X13 @ X11 @ X9)=>fin @ X13 @ X12 @ X9)))))=>fqmltpeq @ X12 @ (funordered_pair @ X10 @ X11) @ X9)))))))), file('<stdin>', pax9)).
% 168.66/164.86 thf(ax5, axiom, p26, file('<stdin>', ax5)).
% 168.66/164.86 thf(ax22, axiom, p9, file('<stdin>', ax22)).
% 168.66/164.86 thf(c_0_16, plain, ![X12:mu, X11:mu, X10:mu, X9:$i]:(epred2_4 @ X9 @ X10 @ X11 @ X12<=>~(((fqmltpeq @ X12 @ (fset_intersection2 @ X10 @ X11) @ X9=>![X13:mu]:(fexists_in_world @ X13 @ X9=>~(((fin @ X13 @ X12 @ X9=>~((fin @ X13 @ X10 @ X9=>~(fin @ X13 @ X11 @ X9))))=>~((~((fin @ X13 @ X10 @ X9=>~(fin @ X13 @ X11 @ X9)))=>fin @ X13 @ X12 @ X9))))))=>~((![X13:mu]:(fexists_in_world @ X13 @ X9=>~(((fin @ X13 @ X12 @ X9=>~((fin @ X13 @ X10 @ X9=>~(fin @ X13 @ X11 @ X9))))=>~((~((fin @ X13 @ X10 @ X9=>~(fin @ X13 @ X11 @ X9)))=>fin @ X13 @ X12 @ X9)))))=>fqmltpeq @ X12 @ (fset_intersection2 @ X10 @ X11) @ X9))))), introduced(definition)).
% 168.66/164.86 thf(c_0_17, plain, ![X12:mu, X11:mu, X10:mu, X9:$i]:(epred2_4 @ X9 @ X10 @ X11 @ X12=>~(((fqmltpeq @ X12 @ (fset_intersection2 @ X10 @ X11) @ X9=>![X13:mu]:(fexists_in_world @ X13 @ X9=>~(((fin @ X13 @ X12 @ X9=>~((fin @ X13 @ X10 @ X9=>~(fin @ X13 @ X11 @ X9))))=>~((~((fin @ X13 @ X10 @ X9=>~(fin @ X13 @ X11 @ X9)))=>fin @ X13 @ X12 @ X9))))))=>~((![X13:mu]:(fexists_in_world @ X13 @ X9=>~(((fin @ X13 @ X12 @ X9=>~((fin @ X13 @ X10 @ X9=>~(fin @ X13 @ X11 @ X9))))=>~((~((fin @ X13 @ X10 @ X9=>~(fin @ X13 @ X11 @ X9)))=>fin @ X13 @ X12 @ X9)))))=>fqmltpeq @ X12 @ (fset_intersection2 @ X10 @ X11) @ X9))))), inference(split_equiv,[status(thm)],[c_0_16])).
% 168.66/164.86 thf(c_0_18, plain, ![X42:$i, X43:mu]:(~p25|(~fexists_in_world @ X43 @ X42|fqmltpeq @ X43 @ X43 @ X42)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax25])])])).
% 168.66/164.86 thf(c_0_19, plain, ![X30:$i, X31:mu, X32:mu]:(~p27|fexists_in_world @ (fset_intersection2 @ X31 @ X32) @ X30), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax27])])])).
% 168.66/164.86 thf(c_0_20, axiom, (p8=>![X9:$i, X10:mu]:(fexists_in_world @ X10 @ X9=>![X11:mu]:(fexists_in_world @ X11 @ X9=>![X12:mu]:(fexists_in_world @ X12 @ X9=>epred2_4 @ X9 @ X10 @ X11 @ X12)))), inference(apply_def,[status(thm)],[pax8, c_0_16])).
% 168.66/164.86 thf(c_0_21, plain, ![X212:mu, X213:mu, X214:mu, X215:$i, X216:mu]:((((fin @ X216 @ X214 @ X215|~fin @ X216 @ X212 @ X215|~fexists_in_world @ X216 @ X215|~fqmltpeq @ X212 @ (fset_intersection2 @ X214 @ X213) @ X215|~epred2_4 @ X215 @ X214 @ X213 @ X212)&(fin @ X216 @ X213 @ X215|~fin @ X216 @ X212 @ X215|~fexists_in_world @ X216 @ X215|~fqmltpeq @ X212 @ (fset_intersection2 @ X214 @ X213) @ X215|~epred2_4 @ X215 @ X214 @ X213 @ X212))&(~fin @ X216 @ X214 @ X215|~fin @ X216 @ X213 @ X215|fin @ X216 @ X212 @ X215|~fexists_in_world @ X216 @ X215|~fqmltpeq @ X212 @ (fset_intersection2 @ X214 @ X213) @ X215|~epred2_4 @ X215 @ X214 @ X213 @ X212))&((fexists_in_world @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X215|fqmltpeq @ X212 @ (fset_intersection2 @ X214 @ X213) @ X215|~epred2_4 @ X215 @ X214 @ X213 @ X212)&((((fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X214 @ X215|fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X212 @ X215|fqmltpeq @ X212 @ (fset_intersection2 @ X214 @ X213) @ X215|~epred2_4 @ X215 @ X214 @ X213 @ X212)&(fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X213 @ X215|fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X212 @ X215|fqmltpeq @ X212 @ (fset_intersection2 @ X214 @ X213) @ X215|~epred2_4 @ X215 @ X214 @ X213 @ X212))&(~fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X212 @ X215|fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X212 @ X215|fqmltpeq @ X212 @ (fset_intersection2 @ X214 @ X213) @ X215|~epred2_4 @ X215 @ X214 @ X213 @ X212))&(((fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X214 @ X215|(~fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X214 @ X215|~fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X213 @ X215)|fqmltpeq @ X212 @ (fset_intersection2 @ X214 @ X213) @ X215|~epred2_4 @ X215 @ X214 @ X213 @ X212)&(fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X213 @ X215|(~fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X214 @ X215|~fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X213 @ X215)|fqmltpeq @ X212 @ (fset_intersection2 @ X214 @ X213) @ X215|~epred2_4 @ X215 @ X214 @ X213 @ X212))&(~fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X212 @ X215|(~fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X214 @ X215|~fin @ (esk98_4 @ X212 @ X213 @ X214 @ X215) @ X213 @ X215)|fqmltpeq @ X212 @ (fset_intersection2 @ X214 @ X213) @ X215|~epred2_4 @ X215 @ X214 @ X213 @ X212))))), 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)],[c_0_17])])])])])])).
% 168.66/164.86 thf(c_0_22, plain, ![X3:mu, X1:$i]:(fqmltpeq @ X3 @ X3 @ X1|~p25|~fexists_in_world @ X3 @ X1), inference(split_conjunct,[status(thm)],[c_0_18])).
% 168.66/164.86 thf(c_0_23, plain, p25, inference(split_conjunct,[status(thm)],[ax6])).
% 168.66/164.86 thf(c_0_24, plain, ![X5:mu, X3:mu, X1:$i]:(fexists_in_world @ (fset_intersection2 @ X3 @ X5) @ X1|~p27), inference(split_conjunct,[status(thm)],[c_0_19])).
% 168.66/164.86 thf(c_0_25, plain, p27, inference(split_conjunct,[status(thm)],[ax4])).
% 168.66/164.86 thf(c_0_26, plain, ![X164:$i, X165:mu, X166:mu, X167:mu]:(~p8|(~fexists_in_world @ X165 @ X164|(~fexists_in_world @ X166 @ X164|(~fexists_in_world @ X167 @ X164|epred2_4 @ X164 @ X165 @ X166 @ X167)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_20])])])).
% 168.66/164.86 thf(c_0_27, plain, ![X148:$i, X149:mu, X150:mu]:((~fqmltpeq @ X149 @ fempty_set @ X148|(~fexists_in_world @ X150 @ X148|~fin @ X150 @ X149 @ X148)|~fexists_in_world @ X149 @ X148|~p10)&((fexists_in_world @ (esk68_2 @ X148 @ X149) @ X148|fqmltpeq @ X149 @ fempty_set @ X148|~fexists_in_world @ X149 @ X148|~p10)&(fin @ (esk68_2 @ X148 @ X149) @ X149 @ X148|fqmltpeq @ X149 @ fempty_set @ X148|~fexists_in_world @ X149 @ X148|~p10))), 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)],[pax10])])])])])])).
% 168.66/164.86 thf(c_0_28, plain, ![X3:mu, X1:$i, X5:mu, X6:mu, X10:mu]:(fin @ X3 @ X10 @ X1|~fin @ X3 @ X5 @ X1|~fin @ X3 @ X6 @ X1|~fexists_in_world @ X3 @ X1|~fqmltpeq @ X10 @ (fset_intersection2 @ X5 @ X6) @ X1|~epred2_4 @ X1 @ X5 @ X6 @ X10), inference(split_conjunct,[status(thm)],[c_0_21])).
% 168.66/164.86 thf(c_0_29, plain, ![X3:mu, X1:$i]:(fqmltpeq @ X3 @ X3 @ X1|~fexists_in_world @ X3 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
% 168.66/164.86 thf(c_0_30, plain, ![X5:mu, X3:mu, X1:$i]:fexists_in_world @ (fset_intersection2 @ X3 @ X5) @ X1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25])])).
% 168.66/164.86 thf(c_0_31, plain, ![X5:mu, X6:mu, X3:mu, X1:$i]:(epred2_4 @ X1 @ X3 @ X5 @ X6|~p8|~fexists_in_world @ X3 @ X1|~fexists_in_world @ X5 @ X1|~fexists_in_world @ X6 @ X1), inference(split_conjunct,[status(thm)],[c_0_26])).
% 168.66/164.86 thf(c_0_32, plain, p8, inference(split_conjunct,[status(thm)],[ax23])).
% 168.66/164.86 thf(c_0_33, plain, ![X5:mu, X3:mu, X1:$i]:(~fqmltpeq @ X3 @ fempty_set @ X1|~fexists_in_world @ X5 @ X1|~fin @ X5 @ X3 @ X1|~fexists_in_world @ X3 @ X1|~p10), inference(split_conjunct,[status(thm)],[c_0_27])).
% 168.66/164.86 thf(c_0_34, plain, p10, inference(split_conjunct,[status(thm)],[ax21])).
% 168.66/164.86 thf(c_0_35, plain, ![X6:mu, X5:mu, X3:mu, X1:$i]:(fin @ X3 @ (fset_intersection2 @ X5 @ X6) @ X1|~epred2_4 @ X1 @ X5 @ X6 @ (fset_intersection2 @ X5 @ X6)|~fin @ X3 @ X6 @ X1|~fin @ X3 @ X5 @ X1|~fexists_in_world @ X3 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_29]), c_0_30])])).
% 168.66/164.86 thf(c_0_36, plain, ![X6:mu, X5:mu, X3:mu, X1:$i]:(epred2_4 @ X1 @ X3 @ X5 @ X6|~fexists_in_world @ X6 @ X1|~fexists_in_world @ X5 @ X1|~fexists_in_world @ X3 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32])])).
% 168.66/164.86 thf(c_0_37, plain, ![X172:$i, X173:mu, X174:mu]:((~fdisjoint @ X173 @ X174 @ X172|fqmltpeq @ (fset_intersection2 @ X173 @ X174) @ fempty_set @ X172|~fexists_in_world @ X174 @ X172|~fexists_in_world @ X173 @ X172|~p7)&(~fqmltpeq @ (fset_intersection2 @ X173 @ X174) @ fempty_set @ X172|fdisjoint @ X173 @ X174 @ X172|~fexists_in_world @ X174 @ X172|~fexists_in_world @ X173 @ X172|~p7)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax7])])])])).
% 168.66/164.86 thf(c_0_38, plain, ![X12:mu, X11:mu, X10:mu, X9:$i]:(epred1_4 @ X9 @ X10 @ X11 @ X12<=>~(((fqmltpeq @ X12 @ (funordered_pair @ X10 @ X11) @ X9=>![X13:mu]:(fexists_in_world @ X13 @ X9=>~(((fin @ X13 @ X12 @ X9=>(~(fqmltpeq @ X13 @ X10 @ X9)=>fqmltpeq @ X13 @ X11 @ X9))=>~(((~(fqmltpeq @ X13 @ X10 @ X9)=>fqmltpeq @ X13 @ X11 @ X9)=>fin @ X13 @ X12 @ X9))))))=>~((![X13:mu]:(fexists_in_world @ X13 @ X9=>~(((fin @ X13 @ X12 @ X9=>(~(fqmltpeq @ X13 @ X10 @ X9)=>fqmltpeq @ X13 @ X11 @ X9))=>~(((~(fqmltpeq @ X13 @ X10 @ X9)=>fqmltpeq @ X13 @ X11 @ X9)=>fin @ X13 @ X12 @ X9)))))=>fqmltpeq @ X12 @ (funordered_pair @ X10 @ X11) @ X9))))), introduced(definition)).
% 168.66/164.86 thf(c_0_39, plain, ![X5:mu, X3:mu, X1:$i]:(~fqmltpeq @ X3 @ fempty_set @ X1|~fin @ X5 @ X3 @ X1|~fexists_in_world @ X5 @ X1|~fexists_in_world @ X3 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 168.66/164.86 thf(c_0_40, plain, ![X6:mu, X5:mu, X3:mu, X1:$i]:(fin @ X3 @ (fset_intersection2 @ X5 @ X6) @ X1|~fin @ X3 @ X6 @ X1|~fin @ X3 @ X5 @ X1|~fexists_in_world @ X3 @ X1|~fexists_in_world @ X6 @ X1|~fexists_in_world @ X5 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_36]), c_0_30])])).
% 168.66/164.86 thf(c_0_41, plain, ![X5:mu, X3:mu, X1:$i]:(fqmltpeq @ (fset_intersection2 @ X3 @ X5) @ fempty_set @ X1|~fdisjoint @ X3 @ X5 @ X1|~fexists_in_world @ X5 @ X1|~fexists_in_world @ X3 @ X1|~p7), inference(split_conjunct,[status(thm)],[c_0_37])).
% 168.66/164.86 thf(c_0_42, plain, p7, inference(split_conjunct,[status(thm)],[ax24])).
% 168.66/164.86 thf(c_0_43, plain, ((fexists_in_world @ esk94_0 @ esk93_0|p1)&((fexists_in_world @ esk95_0 @ esk93_0|p1)&((fexists_in_world @ esk96_0 @ esk93_0|p1)&((fdisjoint @ (funordered_pair @ esk94_0 @ esk95_0) @ esk96_0 @ esk93_0|p1)&(fin @ esk94_0 @ esk96_0 @ esk93_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])])])])])).
% 168.66/164.86 thf(c_0_44, plain, ~p1, inference(fof_simplification,[status(thm)],[ax30])).
% 168.66/164.86 thf(c_0_45, plain, ![X12:mu, X11:mu, X10:mu, X9:$i]:(epred1_4 @ X9 @ X10 @ X11 @ X12=>~(((fqmltpeq @ X12 @ (funordered_pair @ X10 @ X11) @ X9=>![X13:mu]:(fexists_in_world @ X13 @ X9=>~(((fin @ X13 @ X12 @ X9=>(~(fqmltpeq @ X13 @ X10 @ X9)=>fqmltpeq @ X13 @ X11 @ X9))=>~(((~(fqmltpeq @ X13 @ X10 @ X9)=>fqmltpeq @ X13 @ X11 @ X9)=>fin @ X13 @ X12 @ X9))))))=>~((![X13:mu]:(fexists_in_world @ X13 @ X9=>~(((fin @ X13 @ X12 @ X9=>(~(fqmltpeq @ X13 @ X10 @ X9)=>fqmltpeq @ X13 @ X11 @ X9))=>~(((~(fqmltpeq @ X13 @ X10 @ X9)=>fqmltpeq @ X13 @ X11 @ X9)=>fin @ X13 @ X12 @ X9)))))=>fqmltpeq @ X12 @ (funordered_pair @ X10 @ X11) @ X9))))), inference(split_equiv,[status(thm)],[c_0_38])).
% 168.66/164.86 thf(c_0_46, plain, ![X36:$i, X37:mu, X38:mu]:(~p26|fexists_in_world @ (funordered_pair @ X37 @ X38) @ X36), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax26])])])).
% 168.66/164.86 thf(c_0_47, axiom, (p9=>![X9:$i, X10:mu]:(fexists_in_world @ X10 @ X9=>![X11:mu]:(fexists_in_world @ X11 @ X9=>![X12:mu]:(fexists_in_world @ X12 @ X9=>epred1_4 @ X9 @ X10 @ X11 @ X12)))), inference(apply_def,[status(thm)],[pax9, c_0_38])).
% 168.66/164.86 thf(c_0_48, plain, ![X6:mu, X5:mu, X3:mu, X1:$i]:(~fqmltpeq @ (fset_intersection2 @ X3 @ X5) @ fempty_set @ X1|~fin @ X6 @ X5 @ X1|~fin @ X6 @ X3 @ X1|~fexists_in_world @ X6 @ X1|~fexists_in_world @ X5 @ X1|~fexists_in_world @ X3 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_30])])).
% 168.66/164.86 thf(c_0_49, plain, ![X5:mu, X3:mu, X1:$i]:(fqmltpeq @ (fset_intersection2 @ X3 @ X5) @ fempty_set @ X1|~fdisjoint @ X3 @ X5 @ X1|~fexists_in_world @ X5 @ X1|~fexists_in_world @ X3 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_42])])).
% 168.66/164.86 thf(c_0_50, plain, (fin @ esk94_0 @ esk96_0 @ esk93_0|p1), inference(split_conjunct,[status(thm)],[c_0_43])).
% 168.66/164.86 thf(c_0_51, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_44])).
% 168.66/164.86 thf(c_0_52, plain, (fexists_in_world @ esk94_0 @ esk93_0|p1), inference(split_conjunct,[status(thm)],[c_0_43])).
% 168.66/164.86 thf(c_0_53, plain, (fexists_in_world @ esk96_0 @ esk93_0|p1), inference(split_conjunct,[status(thm)],[c_0_43])).
% 168.66/164.86 thf(c_0_54, plain, ![X206:mu, X207:mu, X208:mu, X209:$i, X210:mu]:(((~fin @ X210 @ X206 @ X209|(fqmltpeq @ X210 @ X208 @ X209|fqmltpeq @ X210 @ X207 @ X209)|~fexists_in_world @ X210 @ X209|~fqmltpeq @ X206 @ (funordered_pair @ X208 @ X207) @ X209|~epred1_4 @ X209 @ X208 @ X207 @ X206)&((~fqmltpeq @ X210 @ X208 @ X209|fin @ X210 @ X206 @ X209|~fexists_in_world @ X210 @ X209|~fqmltpeq @ X206 @ (funordered_pair @ X208 @ X207) @ X209|~epred1_4 @ X209 @ X208 @ X207 @ X206)&(~fqmltpeq @ X210 @ X207 @ X209|fin @ X210 @ X206 @ X209|~fexists_in_world @ X210 @ X209|~fqmltpeq @ X206 @ (funordered_pair @ X208 @ X207) @ X209|~epred1_4 @ X209 @ X208 @ X207 @ X206)))&((fexists_in_world @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X209|fqmltpeq @ X206 @ (funordered_pair @ X208 @ X207) @ X209|~epred1_4 @ X209 @ X208 @ X207 @ X206)&(((fqmltpeq @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X208 @ X209|fqmltpeq @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X207 @ X209|fin @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X206 @ X209|fqmltpeq @ X206 @ (funordered_pair @ X208 @ X207) @ X209|~epred1_4 @ X209 @ X208 @ X207 @ X206)&(~fin @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X206 @ X209|fin @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X206 @ X209|fqmltpeq @ X206 @ (funordered_pair @ X208 @ X207) @ X209|~epred1_4 @ X209 @ X208 @ X207 @ X206))&(((fqmltpeq @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X208 @ X209|fqmltpeq @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X207 @ X209|~fqmltpeq @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X208 @ X209|fqmltpeq @ X206 @ (funordered_pair @ X208 @ X207) @ X209|~epred1_4 @ X209 @ X208 @ X207 @ X206)&(~fin @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X206 @ X209|~fqmltpeq @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X208 @ X209|fqmltpeq @ X206 @ (funordered_pair @ X208 @ X207) @ X209|~epred1_4 @ X209 @ X208 @ X207 @ X206))&((fqmltpeq @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X208 @ X209|fqmltpeq @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X207 @ X209|~fqmltpeq @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X207 @ X209|fqmltpeq @ X206 @ (funordered_pair @ X208 @ X207) @ X209|~epred1_4 @ X209 @ X208 @ X207 @ X206)&(~fin @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X206 @ X209|~fqmltpeq @ (esk97_4 @ X206 @ X207 @ X208 @ X209) @ X207 @ X209|fqmltpeq @ X206 @ (funordered_pair @ X208 @ X207) @ X209|~epred1_4 @ X209 @ X208 @ X207 @ X206)))))), 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)],[c_0_45])])])])])])).
% 168.66/164.86 thf(c_0_55, plain, ![X5:mu, X3:mu, X1:$i]:(fexists_in_world @ (funordered_pair @ X3 @ X5) @ X1|~p26), inference(split_conjunct,[status(thm)],[c_0_46])).
% 168.66/164.86 thf(c_0_56, plain, p26, inference(split_conjunct,[status(thm)],[ax5])).
% 168.66/164.86 thf(c_0_57, plain, ![X156:$i, X157:mu, X158:mu, X159:mu]:(~p9|(~fexists_in_world @ X157 @ X156|(~fexists_in_world @ X158 @ X156|(~fexists_in_world @ X159 @ X156|epred1_4 @ X156 @ X157 @ X158 @ X159)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_47])])])).
% 168.66/164.86 thf(c_0_58, plain, ![X5:mu, X6:mu, X3:mu, X1:$i]:(~fin @ X3 @ X5 @ X1|~fin @ X3 @ X6 @ X1|~fdisjoint @ X6 @ X5 @ X1|~fexists_in_world @ X3 @ X1|~fexists_in_world @ X5 @ X1|~fexists_in_world @ X6 @ X1), inference(spm,[status(thm)],[c_0_48, c_0_49])).
% 168.66/164.86 thf(c_0_59, plain, fin @ esk94_0 @ esk96_0 @ esk93_0, inference(sr,[status(thm)],[c_0_50, c_0_51])).
% 168.66/164.86 thf(c_0_60, plain, fexists_in_world @ esk94_0 @ esk93_0, inference(sr,[status(thm)],[c_0_52, c_0_51])).
% 168.66/164.86 thf(c_0_61, plain, fexists_in_world @ esk96_0 @ esk93_0, inference(sr,[status(thm)],[c_0_53, c_0_51])).
% 168.66/164.86 thf(c_0_62, plain, (fdisjoint @ (funordered_pair @ esk94_0 @ esk95_0) @ esk96_0 @ esk93_0|p1), inference(split_conjunct,[status(thm)],[c_0_43])).
% 168.66/164.86 thf(c_0_63, plain, ![X3:mu, X1:$i, X5:mu, X10:mu, X6:mu]:(fin @ X3 @ X6 @ X1|~fqmltpeq @ X3 @ X5 @ X1|~fexists_in_world @ X3 @ X1|~fqmltpeq @ X6 @ (funordered_pair @ X5 @ X10) @ X1|~epred1_4 @ X1 @ X5 @ X10 @ X6), inference(split_conjunct,[status(thm)],[c_0_54])).
% 168.66/164.86 thf(c_0_64, plain, ![X5:mu, X3:mu, X1:$i]:fexists_in_world @ (funordered_pair @ X3 @ X5) @ X1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_55, c_0_56])])).
% 168.66/164.86 thf(c_0_65, plain, ![X5:mu, X6:mu, X3:mu, X1:$i]:(epred1_4 @ X1 @ X3 @ X5 @ X6|~p9|~fexists_in_world @ X3 @ X1|~fexists_in_world @ X5 @ X1|~fexists_in_world @ X6 @ X1), inference(split_conjunct,[status(thm)],[c_0_57])).
% 168.66/164.86 thf(c_0_66, plain, p9, inference(split_conjunct,[status(thm)],[ax22])).
% 168.66/164.86 thf(c_0_67, plain, ![X3:mu]:(~fin @ esk94_0 @ X3 @ esk93_0|~fdisjoint @ X3 @ esk96_0 @ esk93_0|~fexists_in_world @ X3 @ esk93_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_59]), c_0_60]), c_0_61])])).
% 168.66/164.86 thf(c_0_68, plain, fdisjoint @ (funordered_pair @ esk94_0 @ esk95_0) @ esk96_0 @ esk93_0, inference(sr,[status(thm)],[c_0_62, c_0_51])).
% 168.66/164.86 thf(c_0_69, plain, ![X6:mu, X5:mu, X3:mu, X1:$i]:(fin @ X3 @ (funordered_pair @ X5 @ X6) @ X1|~epred1_4 @ X1 @ X5 @ X6 @ (funordered_pair @ X5 @ X6)|~fqmltpeq @ X3 @ X5 @ X1|~fexists_in_world @ X3 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_29]), c_0_64])])).
% 168.66/164.86 thf(c_0_70, plain, ![X6:mu, X5:mu, X3:mu, X1:$i]:(epred1_4 @ X1 @ X3 @ X5 @ X6|~fexists_in_world @ X6 @ X1|~fexists_in_world @ X5 @ X1|~fexists_in_world @ X3 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_65, c_0_66])])).
% 168.66/164.86 thf(c_0_71, plain, (fexists_in_world @ esk95_0 @ esk93_0|p1), inference(split_conjunct,[status(thm)],[c_0_43])).
% 168.66/164.86 thf(c_0_72, plain, ~fin @ esk94_0 @ (funordered_pair @ esk94_0 @ esk95_0) @ esk93_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_68]), c_0_64])])).
% 168.66/164.86 thf(c_0_73, plain, ![X6:mu, X5:mu, X3:mu, X1:$i]:(fin @ X3 @ (funordered_pair @ X5 @ X6) @ X1|~fqmltpeq @ X3 @ X5 @ X1|~fexists_in_world @ X3 @ X1|~fexists_in_world @ X6 @ X1|~fexists_in_world @ X5 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_70]), c_0_64])])).
% 168.66/164.86 thf(c_0_74, plain, fexists_in_world @ esk95_0 @ esk93_0, inference(sr,[status(thm)],[c_0_71, c_0_51])).
% 168.66/164.86 thf(c_0_75, plain, ~fqmltpeq @ esk94_0 @ esk94_0 @ esk93_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_73]), c_0_60]), c_0_74])])).
% 168.66/164.86 thf(c_0_76, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_29]), c_0_60])]), ['proof']).
% 168.66/164.86 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 168.66/164.86 thf(0,theorem,(![X1:$i]:(![X2:mu]:(((exists_in_world @ X2) @ X1) => (![X3:mu]:(((exists_in_world @ X3) @ X1) => (![X4:mu]:(((exists_in_world @ X4) @ X1) => (~((~(((~((~((((disjoint @ ((unordered_pair @ X2) @ X3)) @ X4) @ X1))))) => (~((((in @ X2) @ X4) @ X1))))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 168.66/164.86 % SZS output end Proof
%------------------------------------------------------------------------------