%------------------------------------------------------------------------------ % File : Satallax---3.5 % Problem : SET004^4 : 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 : n015.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:00 PM UTC 2025 % Result : Theorem 1.10s 1.70s % Output : Proof 1.10s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SET004^4 : TPTP v9.2.0. Released v8.1.0. % 0.03/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s % 0.13/0.33 % Computer : n015.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Wed Oct 8 14:55:08 EDT 2025 % 0.13/0.33 % CPUTime : % 1.10/1.70 % SZS status Theorem % 1.10/1.70 % Mode: mode506 % 1.10/1.70 % Inferences: 10966 % 1.10/1.70 % SZS output start Proof % 1.10/1.70 thf(ty_mworld, type, mworld : $tType). % 1.10/1.70 thf(ty_subset, type, subset : ($i>$i>mworld>$o)). % 1.10/1.70 thf(ty_eigen__2, type, eigen__2 : $i). % 1.10/1.70 thf(ty_difference, type, difference : ($i>$i>$i)). % 1.10/1.70 thf(ty_eigen__1, type, eigen__1 : $i). % 1.10/1.70 thf(ty_eigen__0, type, eigen__0 : $i). % 1.10/1.70 thf(ty_member, type, member : ($i>$i>mworld>$o)). % 1.10/1.70 thf(ty_eigen__4, type, eigen__4 : $i). % 1.10/1.70 thf(ty_equal_set, type, equal_set : ($i>$i>mworld>$o)). % 1.10/1.70 thf(ty_mactual, type, mactual : mworld). % 1.10/1.70 thf(ty_intersection, type, intersection : ($i>$i>$i)). % 1.10/1.70 thf(h0, assumption, (![X1:$i>$o]:(![X2:$i]:((X1 @ X2) => (X1 @ (eps__0 @ X1))))),introduced(assumption,[])). % 1.10/1.70 thf(eigendef_eigen__1, definition, eigen__1 = (eps__0 @ (^[X1:$i]:(~((((equal_set @ ((intersection @ eigen__0) @ X1)) @ ((intersection @ X1) @ eigen__0)) @ mactual))))), introduced(definition,[new_symbols(definition,[eigen__1])])). % 1.10/1.70 thf(eigendef_eigen__0, definition, eigen__0 = (eps__0 @ (^[X1:$i]:(~((![X2:$i]:(((equal_set @ ((intersection @ X1) @ X2)) @ ((intersection @ X2) @ X1)) @ mactual)))))), introduced(definition,[new_symbols(definition,[eigen__0])])). % 1.10/1.70 thf(eigendef_eigen__2, definition, eigen__2 = (eps__0 @ (^[X1:$i]:(~(((((member @ X1) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ X1) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual)))))), introduced(definition,[new_symbols(definition,[eigen__2])])). % 1.10/1.70 thf(eigendef_eigen__4, definition, eigen__4 = (eps__0 @ (^[X1:$i]:(~(((((member @ X1) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (((member @ X1) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual)))))), introduced(definition,[new_symbols(definition,[eigen__4])])). % 1.10/1.70 thf(sP1,plain,sP1 <=> (![X1:$i]:((((subset @ ((intersection @ eigen__1) @ eigen__0)) @ X1) @ mactual) = (![X2:$i]:((((member @ X2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ X2) @ X1) @ mactual))))),introduced(definition,[new_symbols(definition,[sP1])])). % 1.10/1.70 thf(sP2,plain,sP2 <=> ((~(((((member @ eigen__2) @ eigen__1) @ mactual) => (~((((member @ eigen__2) @ eigen__0) @ mactual)))))) => (~(((((member @ eigen__2) @ eigen__0) @ mactual) => (~((((member @ eigen__2) @ eigen__1) @ mactual))))))),introduced(definition,[new_symbols(definition,[sP2])])). % 1.10/1.70 thf(sP3,plain,sP3 <=> (![X1:$o>$o]:((X1 @ (((member @ eigen__4) @ ((difference @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0))) @ mactual)) => (![X2:$o]:(((((member @ eigen__4) @ ((difference @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0))) @ mactual) = X2) => (X1 @ X2))))),introduced(definition,[new_symbols(definition,[sP3])])). % 1.10/1.70 thf(sP4,plain,sP4 <=> (![X1:$i]:((((member @ eigen__4) @ ((intersection @ eigen__0) @ X1)) @ mactual) = (~(((((member @ eigen__4) @ eigen__0) @ mactual) => (~((((member @ eigen__4) @ X1) @ mactual)))))))),introduced(definition,[new_symbols(definition,[sP4])])). % 1.10/1.70 thf(sP5,plain,sP5 <=> (((((member @ eigen__4) @ ((difference @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0))) @ mactual) = (~(((((member @ eigen__4) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual))))) => (![X1:$o]:(((((member @ eigen__4) @ ((difference @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0))) @ mactual) = X1) => (X1 = (~(((((member @ eigen__4) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual)))))))),introduced(definition,[new_symbols(definition,[sP5])])). % 1.10/1.70 thf(sP6,plain,sP6 <=> ((((subset @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (~((![X1:$i]:((((member @ X1) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ X1) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual)))))),introduced(definition,[new_symbols(definition,[sP6])])). % 1.10/1.70 thf(sP7,plain,sP7 <=> ((((equal_set @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) = (~(sP6))),introduced(definition,[new_symbols(definition,[sP7])])). % 1.10/1.70 thf(sP8,plain,sP8 <=> (((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual))))) => ((~(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual)))) = (~(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (~(((((member @ eigen__2) @ eigen__0) @ mactual) => (~((((member @ eigen__2) @ eigen__1) @ mactual))))))))))),introduced(definition,[new_symbols(definition,[sP8])])). % 1.10/1.70 thf(sP9,plain,sP9 <=> (sP6 => (![X1:$o]:(((((subset @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) = X1) => (X1 => (~((![X2:$i]:((((member @ X2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ X2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual))))))))),introduced(definition,[new_symbols(definition,[sP9])])). % 1.10/1.70 thf(sP10,plain,sP10 <=> ((((member @ eigen__2) @ eigen__1) @ mactual) => (~((((member @ eigen__2) @ eigen__0) @ mactual)))),introduced(definition,[new_symbols(definition,[sP10])])). % 1.10/1.70 thf(sP11,plain,sP11 <=> (((equal_set @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual),introduced(definition,[new_symbols(definition,[sP11])])). % 1.10/1.70 thf(sP12,plain,sP12 <=> (sP11 = (~(((((subset @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (~((((subset @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual))))))),introduced(definition,[new_symbols(definition,[sP12])])). % 1.10/1.70 thf(sP13,plain,sP13 <=> ((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (~(((((member @ eigen__2) @ eigen__0) @ mactual) => (~((((member @ eigen__2) @ eigen__1) @ mactual)))))))))),introduced(definition,[new_symbols(definition,[sP13])])). % 1.10/1.70 thf(sP14,plain,sP14 <=> (((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual))))) => ((~(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual)))) = (~(sP2)))),introduced(definition,[new_symbols(definition,[sP14])])). % 1.10/1.70 thf(sP15,plain,sP15 <=> ((((member @ eigen__4) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) = (~(((((member @ eigen__4) @ eigen__0) @ mactual) => (~((((member @ eigen__4) @ eigen__1) @ mactual))))))),introduced(definition,[new_symbols(definition,[sP15])])). % 1.10/1.70 thf(sP16,plain,sP16 <=> (((((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) = (~(((((member @ eigen__2) @ eigen__0) @ mactual) => (~((((member @ eigen__2) @ eigen__1) @ mactual))))))) => sP13),introduced(definition,[new_symbols(definition,[sP16])])). % 1.10/1.70 thf(sP17,plain,sP17 <=> (![X1:$i]:(![X2:$i]:(![X3:$i]:((((member @ X1) @ ((intersection @ X2) @ X3)) @ mactual) = (~(((((member @ X1) @ X2) @ mactual) => (~((((member @ X1) @ X3) @ mactual)))))))))),introduced(definition,[new_symbols(definition,[sP17])])). % 1.10/1.70 thf(sP18,plain,sP18 <=> ((((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) = (~(((((member @ eigen__4) @ eigen__1) @ mactual) => (~((((member @ eigen__4) @ eigen__0) @ mactual))))))),introduced(definition,[new_symbols(definition,[sP18])])). % 1.10/1.70 thf(sP19,plain,sP19 <=> ((((member @ eigen__2) @ eigen__0) @ mactual) => (~((((member @ eigen__2) @ eigen__1) @ mactual)))),introduced(definition,[new_symbols(definition,[sP19])])). % 1.10/1.70 thf(sP20,plain,sP20 <=> (![X1:$i]:(![X2:$i]:((((member @ eigen__4) @ ((difference @ X2) @ X1)) @ mactual) = (~(((((member @ eigen__4) @ X2) @ mactual) => (((member @ eigen__4) @ X1) @ mactual))))))),introduced(definition,[new_symbols(definition,[sP20])])). % 1.10/1.70 thf(sP21,plain,sP21 <=> ((~(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual)))) = (~(sP2))),introduced(definition,[new_symbols(definition,[sP21])])). % 1.10/1.70 thf(sP22,plain,sP22 <=> (![X1:$o>$o]:((X1 @ (((subset @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual)) => (![X2:$o]:(((((subset @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) = X2) => (X1 @ X2))))),introduced(definition,[new_symbols(definition,[sP22])])). % 1.10/1.70 thf(sP23,plain,sP23 <=> (((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(((~(sP10)) => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual))))) => (![X1:$o]:(((((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) = X1) => ((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(((~(sP10)) => X1))))))),introduced(definition,[new_symbols(definition,[sP23])])). % 1.10/1.70 thf(sP24,plain,sP24 <=> ((((subset @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) = (![X1:$i]:((((member @ X1) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (((member @ X1) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual)))),introduced(definition,[new_symbols(definition,[sP24])])). % 1.10/1.70 thf(sP25,plain,sP25 <=> (((~(((((member @ eigen__4) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual)))) = (~(((((member @ eigen__4) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual))))) => (![X1:$o]:(((((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) = X1) => ((~(((((member @ eigen__4) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual)))) = (~(((((member @ eigen__4) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => X1))))))),introduced(definition,[new_symbols(definition,[sP25])])). % 1.10/1.70 thf(sP26,plain,sP26 <=> (![X1:$i]:(![X2:$i]:((((member @ eigen__2) @ ((difference @ X2) @ X1)) @ mactual) = (~(((((member @ eigen__2) @ X2) @ mactual) => (((member @ eigen__2) @ X1) @ mactual))))))),introduced(definition,[new_symbols(definition,[sP26])])). % 1.10/1.70 thf(sP27,plain,sP27 <=> (![X1:$i]:((((member @ X1) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ X1) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual))),introduced(definition,[new_symbols(definition,[sP27])])). % 1.10/1.70 thf(sP28,plain,sP28 <=> (((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual))))) => (![X1:$o]:(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) = X1) => ((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~((X1 => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual)))))))),introduced(definition,[new_symbols(definition,[sP28])])). % 1.10/1.70 thf(sP29,plain,sP29 <=> (![X1:$i]:((((member @ eigen__4) @ ((intersection @ eigen__1) @ X1)) @ mactual) = (~(((((member @ eigen__4) @ eigen__1) @ mactual) => (~((((member @ eigen__4) @ X1) @ mactual)))))))),introduced(definition,[new_symbols(definition,[sP29])])). % 1.10/1.70 thf(sP30,plain,sP30 <=> (![X1:$o>$o]:((X1 @ (((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual)) => (![X2:$o]:(((((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) = X2) => (X1 @ X2))))),introduced(definition,[new_symbols(definition,[sP30])])). % 1.10/1.70 thf(sP31,plain,sP31 <=> (![X1:$i]:((((member @ eigen__2) @ ((difference @ X1) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(((((member @ eigen__2) @ X1) @ mactual) => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual)))))),introduced(definition,[new_symbols(definition,[sP31])])). % 1.10/1.70 thf(sP32,plain,sP32 <=> ((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (~(sP19))),introduced(definition,[new_symbols(definition,[sP32])])). % 1.10/1.70 thf(sP33,plain,sP33 <=> ((((member @ eigen__4) @ ((difference @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0))) @ mactual) = (~(((((member @ eigen__4) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual))))),introduced(definition,[new_symbols(definition,[sP33])])). % 1.10/1.70 thf(sP34,plain,sP34 <=> (![X1:$o]:(((((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) = X1) => ((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => X1)))))),introduced(definition,[new_symbols(definition,[sP34])])). % 1.10/1.70 thf(sP35,plain,sP35 <=> (sP18 => ((~(((((member @ eigen__4) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual)))) = (~(((((member @ eigen__4) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (~(((((member @ eigen__4) @ eigen__1) @ mactual) => (~((((member @ eigen__4) @ eigen__0) @ mactual))))))))))),introduced(definition,[new_symbols(definition,[sP35])])). % 1.10/1.70 thf(sP36,plain,sP36 <=> ((![X1:$i]:((((member @ X1) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (((member @ X1) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual))) => (~(sP27))),introduced(definition,[new_symbols(definition,[sP36])])). % 1.10/1.70 thf(sP37,plain,sP37 <=> ((~(((((member @ eigen__4) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual)))) = (~(((((member @ eigen__4) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (~(((((member @ eigen__4) @ eigen__1) @ mactual) => (~((((member @ eigen__4) @ eigen__0) @ mactual)))))))))),introduced(definition,[new_symbols(definition,[sP37])])). % 1.10/1.70 thf(sP38,plain,sP38 <=> (![X1:$o]:(((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = X1) => (X1 = (~(sP2))))),introduced(definition,[new_symbols(definition,[sP38])])). % 1.10/1.70 thf(sP39,plain,sP39 <=> (![X1:$o]:(((((subset @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) = X1) => (sP11 = (~(((((subset @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (~(X1)))))))),introduced(definition,[new_symbols(definition,[sP39])])). % 1.10/1.70 thf(sP40,plain,sP40 <=> ((((member @ eigen__4) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual)),introduced(definition,[new_symbols(definition,[sP40])])). % 1.10/1.70 thf(sP41,plain,sP41 <=> (sP33 => ((~(sP40)) = (~(sP40)))),introduced(definition,[new_symbols(definition,[sP41])])). % 1.10/1.70 thf(sP42,plain,sP42 <=> (![X1:$o>$o]:((X1 @ (((subset @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual)) => (![X2:$o]:(((((subset @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) = X2) => (X1 @ X2))))),introduced(definition,[new_symbols(definition,[sP42])])). % 1.10/1.70 thf(sP43,plain,sP43 <=> (((((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) = (~(sP19))) => ((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(sP2)))),introduced(definition,[new_symbols(definition,[sP43])])). % 1.10/1.70 thf(sP44,plain,sP44 <=> (![X1:$o]:(((((member @ eigen__4) @ ((difference @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0))) @ mactual) = X1) => (X1 = (~(sP40))))),introduced(definition,[new_symbols(definition,[sP44])])). % 1.10/1.70 thf(sP45,plain,sP45 <=> (((member @ eigen__4) @ eigen__0) @ mactual),introduced(definition,[new_symbols(definition,[sP45])])). % 1.10/1.70 thf(sP46,plain,sP46 <=> (![X1:$i]:(![X2:$i]:((((member @ eigen__2) @ ((intersection @ X1) @ X2)) @ mactual) = (~(((((member @ eigen__2) @ X1) @ mactual) => (~((((member @ eigen__2) @ X2) @ mactual))))))))),introduced(definition,[new_symbols(definition,[sP46])])). % 1.10/1.70 thf(sP47,plain,sP47 <=> (((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual))))) => sP34),introduced(definition,[new_symbols(definition,[sP47])])). % 1.10/1.70 thf(sP48,plain,sP48 <=> (![X1:$i]:((((member @ eigen__4) @ ((difference @ X1) @ ((intersection @ eigen__1) @ eigen__0))) @ mactual) = (~(((((member @ eigen__4) @ X1) @ mactual) => (((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual)))))),introduced(definition,[new_symbols(definition,[sP48])])). % 1.10/1.70 thf(sP49,plain,sP49 <=> (((member @ eigen__2) @ eigen__0) @ mactual),introduced(definition,[new_symbols(definition,[sP49])])). % 1.10/1.70 thf(sP50,plain,sP50 <=> (![X1:$o]:(((((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) = X1) => ((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(((~(sP10)) => X1)))))),introduced(definition,[new_symbols(definition,[sP50])])). % 1.10/1.70 thf(sP51,plain,sP51 <=> (![X1:$i]:(![X2:$i]:((((equal_set @ X1) @ X2) @ mactual) = (~(((((subset @ X1) @ X2) @ mactual) => (~((((subset @ X2) @ X1) @ mactual))))))))),introduced(definition,[new_symbols(definition,[sP51])])). % 1.10/1.70 thf(sP52,plain,sP52 <=> (![X1:$i]:((((subset @ ((intersection @ eigen__0) @ eigen__1)) @ X1) @ mactual) = (![X2:$i]:((((member @ X2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (((member @ X2) @ X1) @ mactual))))),introduced(definition,[new_symbols(definition,[sP52])])). % 1.10/1.70 thf(sP53,plain,sP53 <=> (sP24 => sP36),introduced(definition,[new_symbols(definition,[sP53])])). % 1.10/1.70 thf(sP54,plain,sP54 <=> (((member @ eigen__2) @ eigen__1) @ mactual),introduced(definition,[new_symbols(definition,[sP54])])). % 1.10/1.70 thf(sP55,plain,sP55 <=> (![X1:$i]:(((equal_set @ ((intersection @ eigen__0) @ X1)) @ ((intersection @ X1) @ eigen__0)) @ mactual)),introduced(definition,[new_symbols(definition,[sP55])])). % 1.10/1.70 thf(sP56,plain,sP56 <=> ((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual))))),introduced(definition,[new_symbols(definition,[sP56])])). % 1.10/1.70 thf(sP57,plain,sP57 <=> (((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) = (~(sP10))) => ((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(((~(sP10)) => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual)))))),introduced(definition,[new_symbols(definition,[sP57])])). % 1.10/1.70 thf(sP58,plain,sP58 <=> (((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(sP2))) => sP38),introduced(definition,[new_symbols(definition,[sP58])])). % 1.10/1.70 thf(sP59,plain,sP59 <=> ((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) = (~(sP10))),introduced(definition,[new_symbols(definition,[sP59])])). % 1.10/1.70 thf(sP60,plain,sP60 <=> (![X1:$o]:(![X2:$o>$o]:((X2 @ X1) => (![X3:$o]:((X1 = X3) => (X2 @ X3)))))),introduced(definition,[new_symbols(definition,[sP60])])). % 1.10/1.70 thf(sP61,plain,sP61 <=> (![X1:$i]:(![X2:$i]:(((equal_set @ ((intersection @ X1) @ X2)) @ ((intersection @ X2) @ X1)) @ mactual))),introduced(definition,[new_symbols(definition,[sP61])])). % 1.10/1.70 thf(sP62,plain,sP62 <=> (![X1:$o>$o]:((X1 @ (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual)) => (![X2:$o]:(((((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) = X2) => (X1 @ X2))))),introduced(definition,[new_symbols(definition,[sP62])])). % 1.10/1.70 thf(sP63,plain,sP63 <=> ((~(sP40)) = (~(sP40))),introduced(definition,[new_symbols(definition,[sP63])])). % 1.10/1.70 thf(sP64,plain,sP64 <=> (![X1:$i]:((((equal_set @ ((intersection @ eigen__0) @ eigen__1)) @ X1) @ mactual) = (~(((((subset @ ((intersection @ eigen__0) @ eigen__1)) @ X1) @ mactual) => (~((((subset @ X1) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual)))))))),introduced(definition,[new_symbols(definition,[sP64])])). % 1.10/1.70 thf(sP65,plain,sP65 <=> ((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(sP2))),introduced(definition,[new_symbols(definition,[sP65])])). % 1.10/1.70 thf(sP66,plain,sP66 <=> (![X1:$o]:(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) = X1) => ((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~((X1 => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual))))))),introduced(definition,[new_symbols(definition,[sP66])])). % 1.10/1.70 thf(sP67,plain,sP67 <=> (![X1:$o>$o]:((X1 @ (((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual)) => (![X2:$o]:(((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = X2) => (X1 @ X2))))),introduced(definition,[new_symbols(definition,[sP67])])). % 1.10/1.70 thf(sP68,plain,sP68 <=> (sP12 => sP39),introduced(definition,[new_symbols(definition,[sP68])])). % 1.10/1.70 thf(sP69,plain,sP69 <=> (![X1:$o]:(((((subset @ ((intersection @ eigen__0) @ eigen__1)) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) = X1) => (X1 => (~(sP27))))),introduced(definition,[new_symbols(definition,[sP69])])). % 1.10/1.70 thf(sP70,plain,sP70 <=> (![X1:$i]:((((member @ eigen__2) @ ((intersection @ eigen__1) @ X1)) @ mactual) = (~((sP54 => (~((((member @ eigen__2) @ X1) @ mactual)))))))),introduced(definition,[new_symbols(definition,[sP70])])). % 1.10/1.70 thf(sP71,plain,sP71 <=> ((((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) = (~(sP19))),introduced(definition,[new_symbols(definition,[sP71])])). % 1.10/1.70 thf(sP72,plain,sP72 <=> (((((subset @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) = sP27) => sP7),introduced(definition,[new_symbols(definition,[sP72])])). % 1.10/1.70 thf(sP73,plain,sP73 <=> ((~(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual)))) = (~(sP32))),introduced(definition,[new_symbols(definition,[sP73])])). % 1.10/1.70 thf(sP74,plain,sP74 <=> (![X1:$i]:(![X2:$i]:(![X3:$i]:((((member @ X1) @ ((difference @ X3) @ X2)) @ mactual) = (~(((((member @ X1) @ X3) @ mactual) => (((member @ X1) @ X2) @ mactual)))))))),introduced(definition,[new_symbols(definition,[sP74])])). % 1.10/1.70 thf(sP75,plain,sP75 <=> (((member @ eigen__4) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual),introduced(definition,[new_symbols(definition,[sP75])])). % 1.10/1.70 thf(sP76,plain,sP76 <=> (((member @ eigen__4) @ eigen__1) @ mactual),introduced(definition,[new_symbols(definition,[sP76])])). % 1.10/1.70 thf(sP77,plain,sP77 <=> (![X1:$i]:((((member @ eigen__2) @ ((intersection @ eigen__0) @ X1)) @ mactual) = (~((sP49 => (~((((member @ eigen__2) @ X1) @ mactual)))))))),introduced(definition,[new_symbols(definition,[sP77])])). % 1.10/1.70 thf(sP78,plain,sP78 <=> ((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual)),introduced(definition,[new_symbols(definition,[sP78])])). % 1.10/1.70 thf(sP79,plain,sP79 <=> (![X1:$i]:((((member @ X1) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) => (((member @ X1) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual))),introduced(definition,[new_symbols(definition,[sP79])])). % 1.10/1.70 thf(sP80,plain,sP80 <=> ((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = (~(((~(sP10)) => (((member @ eigen__2) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual))))),introduced(definition,[new_symbols(definition,[sP80])])). % 1.10/1.70 thf(sP81,plain,sP81 <=> (sP13 => (![X1:$o]:(((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = X1) => (X1 = (~(sP32)))))),introduced(definition,[new_symbols(definition,[sP81])])). % 1.10/1.70 thf(sP82,plain,sP82 <=> (sP75 => (~((sP76 => (~(sP45)))))),introduced(definition,[new_symbols(definition,[sP82])])). % 1.10/1.70 thf(sP83,plain,sP83 <=> (![X1:$i]:(![X2:$i]:((((member @ eigen__4) @ ((intersection @ X1) @ X2)) @ mactual) = (~(((((member @ eigen__4) @ X1) @ mactual) => (~((((member @ eigen__4) @ X2) @ mactual))))))))),introduced(definition,[new_symbols(definition,[sP83])])). % 1.10/1.70 thf(sP84,plain,sP84 <=> (![X1:$o]:(((((member @ eigen__4) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) = X1) => ((~(sP40)) = (~((sP75 => X1)))))),introduced(definition,[new_symbols(definition,[sP84])])). % 1.10/1.70 thf(sP85,plain,sP85 <=> ((((subset @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1)) @ mactual) = sP27),introduced(definition,[new_symbols(definition,[sP85])])). % 1.10/1.70 thf(sP86,plain,sP86 <=> (![X1:$o]:(((((member @ eigen__2) @ ((difference @ ((intersection @ eigen__1) @ eigen__0)) @ ((intersection @ eigen__0) @ eigen__1))) @ mactual) = X1) => (X1 = (~(sP32))))),introduced(definition,[new_symbols(definition,[sP86])])). % 1.10/1.70 thf(sP87,plain,sP87 <=> (![X1:$o>$o]:((X1 @ (((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual)) => (![X2:$o]:(((((member @ eigen__2) @ ((intersection @ eigen__1) @ eigen__0)) @ mactual) = X2) => (X1 @ X2))))),introduced(definition,[new_symbols(definition,[sP87])])). % 1.10/1.70 thf(sP88,plain,sP88 <=> (![X1:$i]:(![X2:$i]:((((subset @ X1) @ X2) @ mactual) = (![X3:$i]:((((member @ X3) @ X1) @ mactual) => (((member @ X3) @ X2) @ mactual)))))),introduced(definition,[new_symbols(definition,[sP88])])). % 1.10/1.70 thf(sP89,plain,sP89 <=> (sP76 => (~(sP45))),introduced(definition,[new_symbols(definition,[sP89])])). % 1.10/1.70 thf(sP90,plain,sP90 <=> (sP45 => (~(sP76))),introduced(definition,[new_symbols(definition,[sP90])])). % 1.10/1.70 thf(def_mlocal,definition,(mlocal = (^[X1:mworld>$o]:(X1 @ mactual)))). % 1.10/1.70 thf(def_mnot,definition,(mnot = (^[X1:mworld>$o]:(^[X2:mworld]:(~((X1 @ X2))))))). % 1.10/1.70 thf(def_mand,definition,(mand = (^[X1:mworld>$o]:(^[X2:mworld>$o]:(^[X3:mworld]:(~(((X1 @ X3) => (~((X2 @ X3))))))))))). % 1.10/1.70 thf(def_mor,definition,(mor = (^[X1:mworld>$o]:(^[X2:mworld>$o]:(^[X3:mworld]:((~((X1 @ X3))) => (X2 @ X3))))))). % 1.10/1.70 thf(def_mimplies,definition,(mimplies = (^[X1:mworld>$o]:(^[X2:mworld>$o]:(^[X3:mworld]:((X1 @ X3) => (X2 @ X3))))))). % 1.10/1.70 thf(def_mequiv,definition,(mequiv = (^[X1:mworld>$o]:(^[X2:mworld>$o]:(^[X3:mworld]:((X1 @ X3) = (X2 @ X3))))))). % 1.10/1.70 thf(def_mbox,definition,(mbox = (^[X1:mworld>$o]:(^[X2:mworld]:(![X3:mworld]:(((mrel @ X2) @ X3) => (X1 @ X3))))))). % 1.10/1.70 thf(def_mdia,definition,(mdia = (^[X1:mworld>$o]:(^[X2:mworld]:(~((![X3:mworld]:(((mrel @ X2) @ X3) => (~((X1 @ X3))))))))))). % 1.10/1.70 thf(def_mforall_di,definition,(mforall_di = (^[X1:$i>mworld>$o]:(^[X2:mworld]:(![X3:$i]:((X1 @ X3) @ X2)))))). % 1.10/1.70 thf(def_mexists_di,definition,(mexists_di = (^[X1:$i>mworld>$o]:(^[X2:mworld]:(~((![X3:$i]:(~(((X1 @ X3) @ X2)))))))))). % 1.10/1.70 thf(thI06,conjecture,sP61). % 1.10/1.70 thf(h1,negated_conjecture,(~(sP61)),inference(assume_negation,[status(cth)],[thI06])). % 1.10/1.70 thf(1,plain,(sP90 | sP76),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(2,plain,(sP90 | sP45),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(3,plain,((~(sP15) | ~(sP75)) | ~(sP90)),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(4,plain,(sP82 | sP89),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(5,plain,((~(sP37) | sP40) | ~(sP82)),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(6,plain,((~(sP35) | ~(sP18)) | sP37),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(7,plain,(~(sP84) | sP35),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(8,plain,((~(sP25) | ~(sP63)) | sP84),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(9,plain,(~(sP30) | sP25),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(10,plain,((~(sP41) | ~(sP33)) | sP63),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(11,plain,(~(sP44) | sP41),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(12,plain,((~(sP5) | ~(sP33)) | sP44),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(13,plain,(~(sP3) | sP5),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(14,plain,(~(sP60) | sP3),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(15,plain,((~(sP89) | ~(sP76)) | ~(sP45)),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(16,plain,(sP40 | sP75),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(17,plain,(~(sP74) | sP20),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(18,plain,(~(sP20) | sP48),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(19,plain,(~(sP48) | sP33),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(20,plain,(~(sP83) | sP29),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(21,plain,(~(sP29) | sP18),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(22,plain,(~(sP60) | sP30),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(23,plain,(~(sP17) | sP83),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(24,plain,(~(sP83) | sP4),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(25,plain,(~(sP4) | sP15),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(26,plain,(sP79 | ~(sP40)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__4])). % 1.10/1.70 thf(27,plain,((~(sP14) | ~(sP56)) | sP21),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(28,plain,(~(sP38) | sP14),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(29,plain,((~(sP58) | ~(sP65)) | sP38),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(30,plain,(~(sP67) | sP58),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(31,plain,((~(sP43) | ~(sP71)) | sP65),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(32,plain,(~(sP50) | sP43),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(33,plain,((~(sP23) | ~(sP80)) | sP50),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(34,plain,(~(sP62) | sP23),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(35,plain,((~(sP21) | sP78) | ~(sP2)),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(36,plain,((~(sP8) | ~(sP56)) | sP73),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(37,plain,(~(sP86) | sP8),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(38,plain,((~(sP81) | ~(sP13)) | sP86),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(39,plain,(~(sP67) | sP81),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(40,plain,(sP2 | ~(sP10)),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(41,plain,(sP10 | sP49),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(42,plain,(sP10 | sP54),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(43,plain,(sP32 | sP19),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(44,plain,((~(sP73) | sP78) | ~(sP32)),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(45,plain,(~(sP60) | sP67),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(46,plain,((~(sP16) | ~(sP71)) | sP13),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(47,plain,(~(sP34) | sP16),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(48,plain,((~(sP47) | ~(sP56)) | sP34),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(49,plain,(~(sP62) | sP47),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(50,plain,((~(sP57) | ~(sP59)) | sP80),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(51,plain,(~(sP66) | sP57),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(52,plain,((~(sP28) | ~(sP56)) | sP66),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(53,plain,(~(sP87) | sP28),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(54,plain,((~(sP19) | ~(sP49)) | ~(sP54)),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(55,plain,(~(sP74) | sP26),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(56,plain,(~(sP26) | sP31),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(57,plain,(~(sP31) | sP56),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(58,plain,(~(sP46) | sP77),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(59,plain,(~(sP77) | sP71),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(60,plain,(~(sP60) | sP62),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(61,plain,(~(sP17) | sP46),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(62,plain,(~(sP46) | sP70),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(63,plain,(~(sP70) | sP59),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(64,plain,(~(sP60) | sP87),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(65,plain,((~(sP36) | ~(sP79)) | ~(sP27)),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(66,plain,((~(sP53) | ~(sP24)) | sP36),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(67,plain,(~(sP69) | sP53),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(68,plain,((~(sP9) | ~(sP6)) | sP69),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(69,plain,(~(sP22) | sP9),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(70,plain,((~(sP7) | sP11) | sP6),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(71,plain,(sP27 | ~(sP78)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__2])). % 1.10/1.70 thf(72,plain,((~(sP72) | ~(sP85)) | sP7),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(73,plain,(~(sP39) | sP72),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(74,plain,((~(sP68) | ~(sP12)) | sP39),inference(prop_rule,[status(thm)],[])). % 1.10/1.70 thf(75,plain,(~(sP42) | sP68),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(76,plain,(~(sP88) | sP1),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(77,plain,(~(sP1) | sP85),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(78,plain,(~(sP60) | sP42),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(79,plain,(~(sP88) | sP52),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(80,plain,(~(sP52) | sP24),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(81,plain,(~(sP60) | sP22),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(82,plain,(~(sP51) | sP64),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(83,plain,(~(sP64) | sP12),inference(all_rule,[status(thm)],[])). % 1.10/1.70 thf(84,plain,sP60,inference(eq_ind,[status(thm)],[])). % 1.10/1.70 thf(85,plain,(sP55 | ~(sP11)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__1])). % 1.10/1.70 thf(86,plain,(sP61 | ~(sP55)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__0])). % 1.10/1.70 thf(difference_0,axiom,(mlocal @ (mforall_di @ (^[X1:$i]:(mforall_di @ (^[X2:$i]:(mforall_di @ (^[X3:$i]:((mequiv @ ((member @ X1) @ ((difference @ X3) @ X2))) @ ((mand @ ((member @ X1) @ X3)) @ (mnot @ ((member @ X1) @ X2)))))))))))). % 1.10/1.70 thf(87,plain,sP74,inference(preprocess,[status(thm)],[difference_0]). % 1.10/1.70 thf(intersection_0,axiom,(mlocal @ (mforall_di @ (^[X1:$i]:(mforall_di @ (^[X2:$i]:(mforall_di @ (^[X3:$i]:((mequiv @ ((member @ X1) @ ((intersection @ X2) @ X3))) @ ((mand @ ((member @ X1) @ X2)) @ ((member @ X1) @ X3))))))))))). % 1.10/1.70 thf(88,plain,sP17,inference(preprocess,[status(thm)],[intersection_0]). % 1.10/1.70 thf(equal_set_0,axiom,(mlocal @ (mforall_di @ (^[X1:$i]:(mforall_di @ (^[X2:$i]:((mequiv @ ((equal_set @ X1) @ X2)) @ ((mand @ ((subset @ X1) @ X2)) @ ((subset @ X2) @ X1))))))))). % 1.10/1.70 thf(89,plain,sP51,inference(preprocess,[status(thm)],[equal_set_0]). % 1.10/1.70 thf(subset_0,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))))))))))). % 1.10/1.70 thf(90,plain,sP88,inference(preprocess,[status(thm)],[subset_0]). % 1.10/1.70 thf(91,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,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,h1])). % 1.10/1.70 thf(92,plain,$false,inference(eigenvar_choice,[status(thm),assumptions([h1]),eigenvar_choice(discharge,[h0])],[91,h0])). % 1.10/1.70 thf(0,theorem,sP61,inference(contra,[status(thm),contra(discharge,[h1])],[91,h1])). % 1.10/1.70 % SZS output end Proof %------------------------------------------------------------------------------