%------------------------------------------------------------------------------ % File : Satallax---3.5 % Problem : SET579^3 : TPTP v9.2.0. Released v8.1.0. % Transfm : none % Format : tptp:raw % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s % Computer : n009.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:25:57 PM UTC 2025 % Result : Theorem 21.76s 22.46s % Output : Proof 21.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SET579^3 : TPTP v9.2.0. Released v8.1.0. % 0.06/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s % 0.12/0.32 % Computer : n009.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 14:47:23 EDT 2025 % 0.12/0.32 % CPUTime : % 21.76/22.46 % SZS status Theorem % 21.76/22.46 % Mode: mode459 % 21.76/22.46 % Inferences: 706 % 21.76/22.46 % SZS output start Proof % 21.76/22.46 thf(ty_mworld, type, mworld : $tType). % 21.76/22.46 thf(ty_eigen__6, type, eigen__6 : $i). % 21.76/22.46 thf(ty_subset, type, subset : ($i>$i>mworld>$o)). % 21.76/22.46 thf(ty_eigen__2, type, eigen__2 : $i). % 21.76/22.46 thf(ty_difference, type, difference : ($i>$i>$i)). % 21.76/22.46 thf(ty_eigen__1, type, eigen__1 : $i). % 21.76/22.46 thf(ty_eigen__0, type, eigen__0 : $i). % 21.76/22.46 thf(ty_member, type, member : ($i>$i>mworld>$o)). % 21.76/22.46 thf(ty_eigen__5, type, eigen__5 : $i). % 21.76/22.46 thf(ty_mactual, type, mactual : mworld). % 21.76/22.46 thf(ty_qmltpeq, type, qmltpeq : ($i>$i>mworld>$o)). % 21.76/22.46 thf(h0, assumption, (![X1:$i>$o]:(![X2:$i]:((X1 @ X2) => (X1 @ (eps__0 @ X1))))),introduced(assumption,[])). % 21.76/22.46 thf(eigendef_eigen__1, definition, eigen__1 = (eps__0 @ (^[X1:$i]:(~((![X2:$i]:((![X3:$i]:((((member @ X3) @ eigen__0) @ mactual) = (~(((((member @ X3) @ X1) @ mactual) => (((member @ X3) @ X2) @ mactual)))))) => (((qmltpeq @ eigen__0) @ ((difference @ X1) @ X2)) @ mactual))))))), introduced(definition,[new_symbols(definition,[eigen__1])])). % 21.76/22.46 thf(eigendef_eigen__6, definition, eigen__6 = (eps__0 @ (^[X1:$i]:(~(((((member @ X1) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) => (((member @ X1) @ eigen__0) @ mactual)))))), introduced(definition,[new_symbols(definition,[eigen__6])])). % 21.76/22.46 thf(eigendef_eigen__0, definition, eigen__0 = (eps__0 @ (^[X1:$i]:(~((![X2:$i]:(![X3:$i]:((![X4:$i]:((((member @ X4) @ X1) @ mactual) = (~(((((member @ X4) @ X2) @ mactual) => (((member @ X4) @ X3) @ mactual)))))) => (((qmltpeq @ X1) @ ((difference @ X2) @ X3)) @ mactual)))))))), introduced(definition,[new_symbols(definition,[eigen__0])])). % 21.76/22.46 thf(eigendef_eigen__2, definition, eigen__2 = (eps__0 @ (^[X1:$i]:(~(((![X2:$i]:((((member @ X2) @ eigen__0) @ mactual) = (~(((((member @ X2) @ eigen__1) @ mactual) => (((member @ X2) @ X1) @ mactual)))))) => (((qmltpeq @ eigen__0) @ ((difference @ eigen__1) @ X1)) @ mactual)))))), introduced(definition,[new_symbols(definition,[eigen__2])])). % 21.76/22.46 thf(eigendef_eigen__5, definition, eigen__5 = (eps__0 @ (^[X1:$i]:(~(((((member @ X1) @ eigen__0) @ mactual) => (((member @ X1) @ ((difference @ eigen__1) @ eigen__2)) @ mactual)))))), introduced(definition,[new_symbols(definition,[eigen__5])])). % 21.76/22.46 thf(sP1,plain,sP1 <=> (((qmltpeq @ eigen__0) @ ((difference @ eigen__1) @ eigen__2)) @ mactual),introduced(definition,[new_symbols(definition,[sP1])])). % 21.76/22.46 thf(sP2,plain,sP2 <=> ((((member @ eigen__5) @ eigen__0) @ mactual) = (~(((((member @ eigen__5) @ eigen__1) @ mactual) => (((member @ eigen__5) @ eigen__2) @ mactual))))),introduced(definition,[new_symbols(definition,[sP2])])). % 21.76/22.46 thf(sP3,plain,sP3 <=> ((((member @ eigen__5) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) = (~(((((member @ eigen__5) @ eigen__1) @ mactual) => (((member @ eigen__5) @ eigen__2) @ mactual))))),introduced(definition,[new_symbols(definition,[sP3])])). % 21.76/22.46 thf(sP4,plain,sP4 <=> (![X1:$i]:(![X2:$i]:((((member @ X2) @ ((difference @ eigen__1) @ X1)) @ mactual) = (~(((((member @ X2) @ eigen__1) @ mactual) => (((member @ X2) @ X1) @ mactual))))))),introduced(definition,[new_symbols(definition,[sP4])])). % 21.76/22.46 thf(sP5,plain,sP5 <=> ((((member @ eigen__6) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) => (~(((((member @ eigen__6) @ eigen__1) @ mactual) => (((member @ eigen__6) @ eigen__2) @ mactual))))),introduced(definition,[new_symbols(definition,[sP5])])). % 21.76/22.46 thf(sP6,plain,sP6 <=> ((sP1 = (~(((((subset @ eigen__0) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) => (~((((subset @ ((difference @ eigen__1) @ eigen__2)) @ eigen__0) @ mactual))))))) => (![X1:$o]:(((((subset @ eigen__0) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) = X1) => (sP1 = (~((X1 => (~((((subset @ ((difference @ eigen__1) @ eigen__2)) @ eigen__0) @ mactual)))))))))),introduced(definition,[new_symbols(definition,[sP6])])). % 21.76/22.46 thf(sP7,plain,sP7 <=> (((member @ eigen__5) @ ((difference @ eigen__1) @ eigen__2)) @ mactual),introduced(definition,[new_symbols(definition,[sP7])])). % 21.76/22.46 thf(sP8,plain,sP8 <=> (![X1:$o]:(((((subset @ eigen__0) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) = X1) => (sP1 = (~((X1 => (~((((subset @ ((difference @ eigen__1) @ eigen__2)) @ eigen__0) @ mactual))))))))),introduced(definition,[new_symbols(definition,[sP8])])). % 21.76/22.46 thf(sP9,plain,sP9 <=> (((((subset @ ((difference @ eigen__1) @ eigen__2)) @ eigen__0) @ mactual) = (![X1:$i]:((((member @ X1) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) => (((member @ X1) @ eigen__0) @ mactual)))) => ((![X1:$i]:((((member @ X1) @ eigen__0) @ mactual) => (((member @ X1) @ ((difference @ eigen__1) @ eigen__2)) @ mactual))) => (~((![X1:$i]:((((member @ X1) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) => (((member @ X1) @ eigen__0) @ mactual))))))),introduced(definition,[new_symbols(definition,[sP9])])). % 21.76/22.46 thf(sP10,plain,sP10 <=> (![X1:$o>$o]:((X1 @ (((subset @ eigen__0) @ ((difference @ eigen__1) @ eigen__2)) @ mactual)) => (![X2:$o]:(((((subset @ eigen__0) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) = X2) => (X1 @ X2))))),introduced(definition,[new_symbols(definition,[sP10])])). % 21.76/22.46 thf(sP11,plain,sP11 <=> (![X1:$i]:((((member @ X1) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) = (~(((((member @ X1) @ eigen__1) @ mactual) => (((member @ X1) @ eigen__2) @ mactual)))))),introduced(definition,[new_symbols(definition,[sP11])])). % 21.76/22.46 thf(sP12,plain,sP12 <=> (![X1:$o]:(![X2:$o>$o]:((X2 @ X1) => (![X3:$o]:((X1 = X3) => (X2 @ X3)))))),introduced(definition,[new_symbols(definition,[sP12])])). % 21.76/22.46 thf(sP13,plain,sP13 <=> (sP1 = (~(((((subset @ eigen__0) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) => (~((((subset @ ((difference @ eigen__1) @ eigen__2)) @ eigen__0) @ mactual))))))),introduced(definition,[new_symbols(definition,[sP13])])). % 21.76/22.46 thf(sP14,plain,sP14 <=> (![X1:$o>$o]:((X1 @ (((member @ eigen__6) @ eigen__0) @ mactual)) => (![X2:$o]:(((((member @ eigen__6) @ eigen__0) @ mactual) = X2) => (X1 @ X2))))),introduced(definition,[new_symbols(definition,[sP14])])). % 21.76/22.46 thf(sP15,plain,sP15 <=> (((((subset @ eigen__0) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) = (![X1:$i]:((((member @ X1) @ eigen__0) @ mactual) => (((member @ X1) @ ((difference @ eigen__1) @ eigen__2)) @ mactual)))) => (sP1 = (~(((![X1:$i]:((((member @ X1) @ eigen__0) @ mactual) => (((member @ X1) @ ((difference @ eigen__1) @ eigen__2)) @ mactual))) => (~((((subset @ ((difference @ eigen__1) @ eigen__2)) @ eigen__0) @ mactual)))))))),introduced(definition,[new_symbols(definition,[sP15])])). % 21.76/22.46 thf(sP16,plain,sP16 <=> (![X1:$i]:((((subset @ ((difference @ eigen__1) @ eigen__2)) @ X1) @ mactual) = (![X2:$i]:((((member @ X2) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) => (((member @ X2) @ X1) @ mactual))))),introduced(definition,[new_symbols(definition,[sP16])])). % 21.76/22.46 thf(sP17,plain,sP17 <=> (![X1:$o>$o]:((X1 @ (((subset @ ((difference @ eigen__1) @ eigen__2)) @ eigen__0) @ mactual)) => (![X2:$o]:(((((subset @ ((difference @ eigen__1) @ eigen__2)) @ eigen__0) @ mactual) = X2) => (X1 @ X2))))),introduced(definition,[new_symbols(definition,[sP17])])). % 21.76/22.46 thf(sP18,plain,sP18 <=> ((((member @ eigen__5) @ eigen__0) @ mactual) => sP7),introduced(definition,[new_symbols(definition,[sP18])])). % 21.76/22.46 thf(sP19,plain,sP19 <=> ((((member @ eigen__5) @ eigen__1) @ mactual) => (((member @ eigen__5) @ eigen__2) @ mactual)),introduced(definition,[new_symbols(definition,[sP19])])). % 21.76/22.46 thf(sP20,plain,sP20 <=> (![X1:$i]:((![X2:$i]:((((member @ X2) @ eigen__0) @ mactual) = (~(((((member @ X2) @ eigen__1) @ mactual) => (((member @ X2) @ X1) @ mactual)))))) => (((qmltpeq @ eigen__0) @ ((difference @ eigen__1) @ X1)) @ mactual))),introduced(definition,[new_symbols(definition,[sP20])])). % 21.76/22.46 thf(sP21,plain,sP21 <=> (![X1:$i]:((((member @ X1) @ eigen__0) @ mactual) => (((member @ X1) @ ((difference @ eigen__1) @ eigen__2)) @ mactual))),introduced(definition,[new_symbols(definition,[sP21])])). % 21.76/22.46 thf(sP22,plain,sP22 <=> (![X1:$i]:((((member @ X1) @ eigen__0) @ mactual) = (~(((((member @ X1) @ eigen__1) @ mactual) => (((member @ X1) @ eigen__2) @ mactual)))))),introduced(definition,[new_symbols(definition,[sP22])])). % 21.76/22.46 thf(sP23,plain,sP23 <=> ((sP21 => (~((((subset @ ((difference @ eigen__1) @ eigen__2)) @ eigen__0) @ mactual)))) => (![X1:$o]:(((((subset @ ((difference @ eigen__1) @ eigen__2)) @ eigen__0) @ mactual) = X1) => (sP21 => (~(X1)))))),introduced(definition,[new_symbols(definition,[sP23])])). % 21.76/22.46 thf(sP24,plain,sP24 <=> (((member @ eigen__6) @ ((difference @ eigen__1) @ eigen__2)) @ mactual),introduced(definition,[new_symbols(definition,[sP24])])). % 21.76/22.46 thf(sP25,plain,sP25 <=> (![X1:$i]:((((member @ X1) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) => (((member @ X1) @ eigen__0) @ mactual))),introduced(definition,[new_symbols(definition,[sP25])])). % 21.76/22.46 thf(sP26,plain,sP26 <=> (![X1:$i]:(![X2:$i]:((((qmltpeq @ X1) @ X2) @ mactual) = (~(((((subset @ X1) @ X2) @ mactual) => (~((((subset @ X2) @ X1) @ mactual))))))))),introduced(definition,[new_symbols(definition,[sP26])])). % 21.76/22.46 thf(sP27,plain,sP27 <=> ((~((sP24 => (((member @ eigen__6) @ eigen__0) @ mactual)))) => (![X1:$o]:(((((member @ eigen__6) @ eigen__0) @ mactual) = X1) => (~((sP24 => X1)))))),introduced(definition,[new_symbols(definition,[sP27])])). % 21.76/22.46 thf(sP28,plain,sP28 <=> ((((member @ eigen__6) @ eigen__0) @ mactual) = (~(((((member @ eigen__6) @ eigen__1) @ mactual) => (((member @ eigen__6) @ eigen__2) @ mactual))))),introduced(definition,[new_symbols(definition,[sP28])])). % 21.76/22.46 thf(sP29,plain,sP29 <=> (![X1:$i]:(![X2:$i]:((![X3:$i]:((((member @ X3) @ eigen__0) @ mactual) = (~(((((member @ X3) @ X1) @ mactual) => (((member @ X3) @ X2) @ mactual)))))) => (((qmltpeq @ eigen__0) @ ((difference @ X1) @ X2)) @ mactual)))),introduced(definition,[new_symbols(definition,[sP29])])). % 21.76/22.46 thf(sP30,plain,sP30 <=> ((((subset @ eigen__0) @ ((difference @ eigen__1) @ eigen__2)) @ mactual) = sP21),introduced(definition,[new_symbols(definition,[sP30])])). % 21.76/22.46 thf(sP31,plain,sP31 <=> (![X1:$i]:(![X2:$i]:(![X3:$i]:((![X4:$i]:((((member @ X4) @ X1) @ mactual) = (~(((((member @ X4) @ X2) @ mactual) => (((member @ X4) @ X3) @ mactual)))))) => (((qmltpeq @ X1) @ ((difference @ X2) @ X3)) @ mactual))))),introduced(definition,[new_symbols(definition,[sP31])])). % 21.76/22.46 thf(sP32,plain,sP32 <=> (sP28 => (~(sP5))),introduced(definition,[new_symbols(definition,[sP32])])). % 21.76/22.46 thf(sP33,plain,sP33 <=> (((member @ eigen__5) @ eigen__0) @ mactual),introduced(definition,[new_symbols(definition,[sP33])])). % 21.76/22.46 thf(sP34,plain,sP34 <=> (![X1:$o]:(((((member @ eigen__6) @ eigen__0) @ mactual) = X1) => (~((sP24 => X1))))),introduced(definition,[new_symbols(definition,[sP34])])). % 21.76/22.46 thf(sP35,plain,sP35 <=> (![X1:$i]:(![X2:$i]:(![X3:$i]:((((member @ X3) @ ((difference @ X1) @ X2)) @ mactual) = (~(((((member @ X3) @ X1) @ mactual) => (((member @ X3) @ X2) @ mactual)))))))),introduced(definition,[new_symbols(definition,[sP35])])). % 21.76/22.46 thf(sP36,plain,sP36 <=> (![X1:$i]:((((subset @ eigen__0) @ X1) @ mactual) = (![X2:$i]:((((member @ X2) @ eigen__0) @ mactual) => (((member @ X2) @ X1) @ mactual))))),introduced(definition,[new_symbols(definition,[sP36])])). % 21.76/22.46 thf(sP37,plain,sP37 <=> (sP24 => (((member @ eigen__6) @ eigen__0) @ mactual)),introduced(definition,[new_symbols(definition,[sP37])])). % 21.76/22.46 thf(sP38,plain,sP38 <=> (![X1:$i]:(![X2:$i]:((((subset @ X1) @ X2) @ mactual) = (![X3:$i]:((((member @ X3) @ X1) @ mactual) => (((member @ X3) @ X2) @ mactual)))))),introduced(definition,[new_symbols(definition,[sP38])])). % 21.76/22.46 thf(sP39,plain,sP39 <=> (sP24 = (~(((((member @ eigen__6) @ eigen__1) @ mactual) => (((member @ eigen__6) @ eigen__2) @ mactual))))),introduced(definition,[new_symbols(definition,[sP39])])). % 21.76/22.46 thf(sP40,plain,sP40 <=> (sP1 = (~((sP21 => (~((((subset @ ((difference @ eigen__1) @ eigen__2)) @ eigen__0) @ mactual))))))),introduced(definition,[new_symbols(definition,[sP40])])). % 21.76/22.46 thf(sP41,plain,sP41 <=> (![X1:$i]:((((qmltpeq @ eigen__0) @ X1) @ mactual) = (~(((((subset @ eigen__0) @ X1) @ mactual) => (~((((subset @ X1) @ eigen__0) @ mactual)))))))),introduced(definition,[new_symbols(definition,[sP41])])). % 21.76/22.46 thf(sP42,plain,sP42 <=> (sP21 => (~((((subset @ ((difference @ eigen__1) @ eigen__2)) @ eigen__0) @ mactual)))),introduced(definition,[new_symbols(definition,[sP42])])). % 21.76/22.46 thf(sP43,plain,sP43 <=> (sP21 => (~(sP25))),introduced(definition,[new_symbols(definition,[sP43])])). % 21.76/22.46 thf(sP44,plain,sP44 <=> ((((member @ eigen__6) @ eigen__1) @ mactual) => (((member @ eigen__6) @ eigen__2) @ mactual)),introduced(definition,[new_symbols(definition,[sP44])])). % 21.76/22.46 thf(sP45,plain,sP45 <=> (![X1:$o]:(((((subset @ ((difference @ eigen__1) @ eigen__2)) @ eigen__0) @ mactual) = X1) => (sP21 => (~(X1))))),introduced(definition,[new_symbols(definition,[sP45])])). % 21.76/22.46 thf(sP46,plain,sP46 <=> ((((subset @ ((difference @ eigen__1) @ eigen__2)) @ eigen__0) @ mactual) = sP25),introduced(definition,[new_symbols(definition,[sP46])])). % 21.76/22.46 thf(sP47,plain,sP47 <=> (sP22 => sP1),introduced(definition,[new_symbols(definition,[sP47])])). % 21.76/22.46 thf(def_mlocal,definition,(mlocal = (^[X1:mworld>$o]:(X1 @ mactual)))). % 21.76/22.46 thf(def_mnot,definition,(mnot = (^[X1:mworld>$o]:(^[X2:mworld]:(~((X1 @ X2))))))). % 21.76/22.46 thf(def_mand,definition,(mand = (^[X1:mworld>$o]:(^[X2:mworld>$o]:(^[X3:mworld]:(~(((X1 @ X3) => (~((X2 @ X3))))))))))). % 21.76/22.46 thf(def_mor,definition,(mor = (^[X1:mworld>$o]:(^[X2:mworld>$o]:(^[X3:mworld]:((~((X1 @ X3))) => (X2 @ X3))))))). % 21.76/22.46 thf(def_mimplies,definition,(mimplies = (^[X1:mworld>$o]:(^[X2:mworld>$o]:(^[X3:mworld]:((X1 @ X3) => (X2 @ X3))))))). % 21.76/22.46 thf(def_mequiv,definition,(mequiv = (^[X1:mworld>$o]:(^[X2:mworld>$o]:(^[X3:mworld]:((X1 @ X3) = (X2 @ X3))))))). % 21.76/22.46 thf(def_mbox,definition,(mbox = (^[X1:mworld>$o]:(^[X2:mworld]:(![X3:mworld]:(((mrel @ X2) @ X3) => (X1 @ X3))))))). % 21.76/22.46 thf(def_mdia,definition,(mdia = (^[X1:mworld>$o]:(^[X2:mworld]:(~((![X3:mworld]:(((mrel @ X2) @ X3) => (~((X1 @ X3))))))))))). % 21.76/22.46 thf(def_mforall_di,definition,(mforall_di = (^[X1:$i>mworld>$o]:(^[X2:mworld]:(![X3:$i]:((X1 @ X3) @ X2)))))). % 21.76/22.46 thf(def_mexists_di,definition,(mexists_di = (^[X1:$i>mworld>$o]:(^[X2:mworld]:(~((![X3:$i]:(~(((X1 @ X3) @ X2)))))))))). % 21.76/22.46 thf(prove_th20,conjecture,(![X1:$i]:(![X2:$i]:(![X3:$i]:((![X4:$i]:((((member @ X4) @ X1) @ mactual) = (~(((((member @ X4) @ X2) @ mactual) => (~((~((((member @ X4) @ X3) @ mactual)))))))))) => (((qmltpeq @ X1) @ ((difference @ X2) @ X3)) @ mactual)))))). % 21.76/22.46 thf(h1,negated_conjecture,(~(sP31)),inference(assume_negation,[status(cth)],[prove_th20])). % 21.76/22.46 thf(1,plain,(sP5 | sP44),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(2,plain,((~(sP39) | ~(sP24)) | ~(sP44)),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(3,plain,((~(sP2) | ~(sP33)) | ~(sP19)),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(4,plain,((~(sP3) | sP7) | sP19),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(5,plain,((~(sP43) | ~(sP21)) | ~(sP25)),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(6,plain,(sP37 | sP24),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(7,plain,(~(sP22) | sP28),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(8,plain,((~(sP32) | ~(sP28)) | ~(sP5)),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(9,plain,(~(sP34) | sP32),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(10,plain,((~(sP27) | sP37) | sP34),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(11,plain,(~(sP14) | sP27),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(12,plain,(~(sP12) | sP14),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(13,plain,(~(sP11) | sP39),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(14,plain,(sP18 | ~(sP7)),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(15,plain,(sP18 | sP33),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(16,plain,(~(sP22) | sP2),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(17,plain,(~(sP35) | sP4),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(18,plain,(~(sP4) | sP11),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(19,plain,(~(sP11) | sP3),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(20,plain,((~(sP9) | ~(sP46)) | sP43),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(21,plain,(~(sP45) | sP9),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(22,plain,((~(sP23) | ~(sP42)) | sP45),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(23,plain,(~(sP17) | sP23),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(24,plain,((~(sP40) | sP1) | sP42),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(25,plain,(sP25 | ~(sP37)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__6])). % 21.76/22.46 thf(26,plain,(sP21 | ~(sP18)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__5])). % 21.76/22.46 thf(27,plain,((~(sP15) | ~(sP30)) | sP40),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(28,plain,(~(sP8) | sP15),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(29,plain,((~(sP6) | ~(sP13)) | sP8),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(30,plain,(~(sP10) | sP6),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(31,plain,(~(sP38) | sP16),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(32,plain,(~(sP16) | sP46),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(33,plain,(~(sP12) | sP17),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(34,plain,(~(sP38) | sP36),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(35,plain,(~(sP36) | sP30),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(36,plain,(~(sP12) | sP10),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(37,plain,(~(sP26) | sP41),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(38,plain,(~(sP41) | sP13),inference(all_rule,[status(thm)],[])). % 21.76/22.46 thf(39,plain,sP12,inference(eq_ind,[status(thm)],[])). % 21.76/22.46 thf(40,plain,(sP47 | ~(sP1)),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(41,plain,(sP47 | sP22),inference(prop_rule,[status(thm)],[])). % 21.76/22.46 thf(42,plain,(sP20 | ~(sP47)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__2])). % 21.76/22.46 thf(43,plain,(sP29 | ~(sP20)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__1])). % 21.76/22.46 thf(44,plain,(sP31 | ~(sP29)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__0])). % 21.76/22.46 thf(subset_defn,axiom,(mlocal @ (mforall_di @ (^[X1:$i]:(mforall_di @ (^[X2:$i]:((mequiv @ ((subset @ X1) @ X2)) @ (mforall_di @ (^[X3:$i]:((mimplies @ ((member @ X3) @ X1)) @ ((member @ X3) @ X2))))))))))). % 21.76/22.46 thf(45,plain,sP38,inference(preprocess,[status(thm)],[subset_defn]). % 21.76/22.46 thf(equal_defn,axiom,(mlocal @ (mforall_di @ (^[X1:$i]:(mforall_di @ (^[X2:$i]:((mequiv @ ((qmltpeq @ X1) @ X2)) @ ((mand @ ((subset @ X1) @ X2)) @ ((subset @ X2) @ X1))))))))). % 21.76/22.46 thf(46,plain,sP26,inference(preprocess,[status(thm)],[equal_defn]). % 21.76/22.46 thf(difference_defn,axiom,(mlocal @ (mforall_di @ (^[X1:$i]:(mforall_di @ (^[X2:$i]:(mforall_di @ (^[X3:$i]:((mequiv @ ((member @ X3) @ ((difference @ X1) @ X2))) @ ((mand @ ((member @ X3) @ X1)) @ (mnot @ ((member @ X3) @ X2)))))))))))). % 21.76/22.46 thf(47,plain,sP35,inference(preprocess,[status(thm)],[difference_defn]). % 21.76/22.46 thf(48,plain,$false,inference(prop_unsat,[status(thm),assumptions([h1,h0])],[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,h1])). % 21.76/22.46 thf(49,plain,$false,inference(eigenvar_choice,[status(thm),assumptions([h1]),eigenvar_choice(discharge,[h0])],[48,h0])). % 21.76/22.46 thf(0,theorem,(![X1:$i]:(![X2:$i]:(![X3:$i]:((![X4:$i]:((((member @ X4) @ X1) @ mactual) = (~(((((member @ X4) @ X2) @ mactual) => (~((~((((member @ X4) @ X3) @ mactual)))))))))) => (((qmltpeq @ X1) @ ((difference @ X2) @ X3)) @ mactual))))),inference(contra,[status(thm),contra(discharge,[h1])],[48,h1])). % 21.76/22.46 % SZS output end Proof %------------------------------------------------------------------------------