%------------------------------------------------------------------------------ % File : Satallax---3.5 % Problem : SYO064^4.003 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s % Computer : n024.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 03:24:48 PM UTC 2025 % Result : Theorem 1.10s 1.50s % Output : Proof 1.10s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYO064^4.003 : TPTP v9.2.0. Released v4.0.0. % 0.11/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s % 0.12/0.34 % Computer : n024.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 : Thu Oct 9 00:27:23 EDT 2025 % 0.12/0.34 % CPUTime : % 1.10/1.50 % SZS status Theorem % 1.10/1.50 % Mode: mode506 % 1.10/1.50 % Inferences: 41945 % 1.10/1.50 % SZS output start Proof % 1.10/1.50 thf(ty_a, type, a : ($i>$o)). % 1.10/1.50 thf(ty_eigen__6, type, eigen__6 : $i). % 1.10/1.50 thf(ty_a3, type, a3 : ($i>$o)). % 1.10/1.50 thf(ty_eigen__2, type, eigen__2 : $i). % 1.10/1.50 thf(ty_a1, type, a1 : ($i>$o)). % 1.10/1.50 thf(ty_eigen__1, type, eigen__1 : $i). % 1.10/1.50 thf(ty_a2, type, a2 : ($i>$o)). % 1.10/1.50 thf(ty_b, type, b : ($i>$o)). % 1.10/1.50 thf(ty_eigen__0, type, eigen__0 : $i). % 1.10/1.50 thf(ty_b2, type, b2 : ($i>$o)). % 1.10/1.50 thf(ty_eigen__5, type, eigen__5 : $i). % 1.10/1.50 thf(ty_eigen__3, type, eigen__3 : $i). % 1.10/1.50 thf(ty_b1, type, b1 : ($i>$o)). % 1.10/1.50 thf(ty_irel, type, irel : ($i>$i>$o)). % 1.10/1.50 thf(h0, assumption, (![X1:$i>$o]:(![X2:$i]:((X1 @ X2) => (X1 @ (eps__0 @ X1))))),introduced(assumption,[])). % 1.10/1.50 thf(eigendef_eigen__3, definition, eigen__3 = (eps__0 @ (^[X1:$i]:(~((((irel @ eigen__2) @ X1) => (~(((b2 @ X1) => (~((a3 @ X1))))))))))), introduced(definition,[new_symbols(definition,[eigen__3])])). % 1.10/1.50 thf(eigendef_eigen__1, definition, eigen__1 = (eps__0 @ (^[X1:$i]:(~((((irel @ eigen__0) @ X1) => ((~((![X2:$i]:(((irel @ X1) @ X2) => (~(((b @ X2) => (~((a1 @ X2)))))))))) => (![X2:$i]:(((irel @ X1) @ X2) => ((~((![X3:$i]:(((irel @ X2) @ X3) => (~(((b1 @ X3) => (~((a2 @ X3)))))))))) => (![X3:$i]:(((irel @ X2) @ X3) => (~(((b2 @ X3) => (~((a3 @ X3))))))))))))))))), introduced(definition,[new_symbols(definition,[eigen__1])])). % 1.10/1.50 thf(eigendef_eigen__6, definition, eigen__6 = (eps__0 @ (^[X1:$i]:(~((((irel @ eigen__1) @ X1) => (~(((b @ X1) => (~((a1 @ X1))))))))))), introduced(definition,[new_symbols(definition,[eigen__6])])). % 1.10/1.50 thf(eigendef_eigen__0, definition, eigen__0 = (eps__0 @ (^[X1:$i]:(~(((~((![X2:$i]:(((irel @ X1) @ X2) => (a @ X2))))) => (![X2:$i]:(((irel @ X1) @ X2) => ((~((![X3:$i]:(((irel @ X2) @ X3) => (~(((b @ X3) => (~((a1 @ X3)))))))))) => (![X3:$i]:(((irel @ X2) @ X3) => ((~((![X4:$i]:(((irel @ X3) @ X4) => (~(((b1 @ X4) => (~((a2 @ X4)))))))))) => (![X4:$i]:(((irel @ X3) @ X4) => (~(((b2 @ X4) => (~((a3 @ X4))))))))))))))))))), introduced(definition,[new_symbols(definition,[eigen__0])])). % 1.10/1.50 thf(eigendef_eigen__2, definition, eigen__2 = (eps__0 @ (^[X1:$i]:(~((((irel @ eigen__1) @ X1) => ((~((![X2:$i]:(((irel @ X1) @ X2) => (~(((b1 @ X2) => (~((a2 @ X2)))))))))) => (![X2:$i]:(((irel @ X1) @ X2) => (~(((b2 @ X2) => (~((a3 @ X2)))))))))))))), introduced(definition,[new_symbols(definition,[eigen__2])])). % 1.10/1.50 thf(eigendef_eigen__5, definition, eigen__5 = (eps__0 @ (^[X1:$i]:(~((((irel @ eigen__2) @ X1) => (~(((b1 @ X1) => (~((a2 @ X1))))))))))), introduced(definition,[new_symbols(definition,[eigen__5])])). % 1.10/1.50 thf(sP1,plain,sP1 <=> (![X1:$i]:(((irel @ eigen__2) @ X1) => (~(((b2 @ X1) => (~((a3 @ X1)))))))),introduced(definition,[new_symbols(definition,[sP1])])). % 1.10/1.50 thf(sP2,plain,sP2 <=> (![X1:$i]:((irel @ X1) @ X1)),introduced(definition,[new_symbols(definition,[sP2])])). % 1.10/1.50 thf(sP3,plain,sP3 <=> (((irel @ eigen__1) @ eigen__1) => ((~((![X1:$i]:(((irel @ eigen__1) @ X1) => (b1 @ X1))))) => (![X1:$i]:(((irel @ eigen__1) @ X1) => (a1 @ X1))))),introduced(definition,[new_symbols(definition,[sP3])])). % 1.10/1.50 thf(sP4,plain,sP4 <=> (![X1:$i]:((~((![X2:$i]:(((irel @ X1) @ X2) => ((~((![X3:$i]:(((irel @ X2) @ X3) => (b @ X3))))) => (![X3:$i]:(((irel @ X2) @ X3) => (a @ X3)))))))) => (![X2:$i]:(((irel @ X1) @ X2) => (b @ X2))))),introduced(definition,[new_symbols(definition,[sP4])])). % 1.10/1.50 thf(sP5,plain,sP5 <=> (![X1:$i]:(((irel @ eigen__0) @ X1) => ((~((![X2:$i]:(((irel @ X1) @ X2) => (~(((b @ X2) => (~((a1 @ X2)))))))))) => (![X2:$i]:(((irel @ X1) @ X2) => ((~((![X3:$i]:(((irel @ X2) @ X3) => (~(((b1 @ X3) => (~((a2 @ X3)))))))))) => (![X3:$i]:(((irel @ X2) @ X3) => (~(((b2 @ X3) => (~((a3 @ X3)))))))))))))),introduced(definition,[new_symbols(definition,[sP5])])). % 1.10/1.50 thf(sP6,plain,sP6 <=> (((irel @ eigen__1) @ eigen__2) => (~(((irel @ eigen__2) @ eigen__5)))),introduced(definition,[new_symbols(definition,[sP6])])). % 1.10/1.50 thf(sP7,plain,sP7 <=> ((~((![X1:$i]:(((irel @ eigen__2) @ X1) => (b2 @ X1))))) => (![X1:$i]:(((irel @ eigen__2) @ X1) => (a2 @ X1)))),introduced(definition,[new_symbols(definition,[sP7])])). % 1.10/1.50 thf(sP8,plain,sP8 <=> (((irel @ eigen__2) @ eigen__5) => (a2 @ eigen__5)),introduced(definition,[new_symbols(definition,[sP8])])). % 1.10/1.50 thf(sP9,plain,sP9 <=> ((b @ eigen__6) => (~((a1 @ eigen__6)))),introduced(definition,[new_symbols(definition,[sP9])])). % 1.10/1.50 thf(sP10,plain,sP10 <=> (![X1:$i]:((~((((irel @ eigen__0) @ eigen__1) => (~(((irel @ eigen__1) @ X1)))))) => ((irel @ eigen__0) @ X1))),introduced(definition,[new_symbols(definition,[sP10])])). % 1.10/1.50 thf(sP11,plain,sP11 <=> ((irel @ eigen__1) @ eigen__1),introduced(definition,[new_symbols(definition,[sP11])])). % 1.10/1.50 thf(sP12,plain,sP12 <=> (![X1:$i]:(((irel @ eigen__2) @ X1) => (b2 @ X1))),introduced(definition,[new_symbols(definition,[sP12])])). % 1.10/1.50 thf(sP13,plain,sP13 <=> ((irel @ eigen__0) @ eigen__6),introduced(definition,[new_symbols(definition,[sP13])])). % 1.10/1.50 thf(sP14,plain,sP14 <=> (![X1:$i]:((![X2:$i]:(((irel @ X1) @ X2) => (b1 @ X2))) => (![X2:$i]:(((irel @ X1) @ X2) => ((~((![X3:$i]:(((irel @ X2) @ X3) => ((~((![X4:$i]:(((irel @ X3) @ X4) => (b2 @ X4))))) => (![X4:$i]:(((irel @ X3) @ X4) => (a2 @ X4)))))))) => (![X3:$i]:(((irel @ X2) @ X3) => (b2 @ X3)))))))),introduced(definition,[new_symbols(definition,[sP14])])). % 1.10/1.50 thf(sP15,plain,sP15 <=> (![X1:$i]:(((irel @ eigen__1) @ X1) => (b1 @ X1))),introduced(definition,[new_symbols(definition,[sP15])])). % 1.10/1.50 thf(sP16,plain,sP16 <=> ((b1 @ eigen__5) => (~((a2 @ eigen__5)))),introduced(definition,[new_symbols(definition,[sP16])])). % 1.10/1.50 thf(sP17,plain,sP17 <=> ((~((![X1:$i]:(((irel @ eigen__1) @ X1) => ((~((![X2:$i]:(((irel @ X1) @ X2) => (b1 @ X2))))) => (![X2:$i]:(((irel @ X1) @ X2) => (a1 @ X2)))))))) => sP15),introduced(definition,[new_symbols(definition,[sP17])])). % 1.10/1.50 thf(sP18,plain,sP18 <=> (![X1:$i]:(![X2:$i]:((~((((irel @ eigen__1) @ X1) => (~(((irel @ X1) @ X2)))))) => ((irel @ eigen__1) @ X2)))),introduced(definition,[new_symbols(definition,[sP18])])). % 1.10/1.50 thf(sP19,plain,sP19 <=> ((~((((irel @ eigen__0) @ eigen__1) => (~(((irel @ eigen__1) @ eigen__6)))))) => sP13),introduced(definition,[new_symbols(definition,[sP19])])). % 1.10/1.50 thf(sP20,plain,sP20 <=> (![X1:$i]:((~((((irel @ eigen__1) @ eigen__2) => (~(((irel @ eigen__2) @ X1)))))) => ((irel @ eigen__1) @ X1))),introduced(definition,[new_symbols(definition,[sP20])])). % 1.10/1.50 thf(sP21,plain,sP21 <=> ((irel @ eigen__2) @ eigen__3),introduced(definition,[new_symbols(definition,[sP21])])). % 1.10/1.50 thf(sP22,plain,sP22 <=> (((irel @ eigen__0) @ eigen__0) => ((~((![X1:$i]:(((irel @ eigen__0) @ X1) => (b @ X1))))) => (![X1:$i]:(((irel @ eigen__0) @ X1) => (a @ X1))))),introduced(definition,[new_symbols(definition,[sP22])])). % 1.10/1.50 thf(sP23,plain,sP23 <=> (![X1:$i]:(((irel @ eigen__2) @ X1) => ((~((![X2:$i]:(((irel @ X1) @ X2) => (b2 @ X2))))) => (![X2:$i]:(((irel @ X1) @ X2) => (a2 @ X2)))))),introduced(definition,[new_symbols(definition,[sP23])])). % 1.10/1.50 thf(sP24,plain,sP24 <=> (((irel @ eigen__2) @ eigen__2) => sP7),introduced(definition,[new_symbols(definition,[sP24])])). % 1.10/1.50 thf(sP25,plain,sP25 <=> (![X1:$i]:(((irel @ eigen__2) @ X1) => (a2 @ X1))),introduced(definition,[new_symbols(definition,[sP25])])). % 1.10/1.50 thf(sP26,plain,sP26 <=> (sP21 => (b2 @ eigen__3)),introduced(definition,[new_symbols(definition,[sP26])])). % 1.10/1.50 thf(sP27,plain,sP27 <=> (![X1:$i]:(((irel @ eigen__0) @ X1) => ((~((![X2:$i]:(((irel @ X1) @ X2) => (b @ X2))))) => (![X2:$i]:(((irel @ X1) @ X2) => (a @ X2)))))),introduced(definition,[new_symbols(definition,[sP27])])). % 1.10/1.50 thf(sP28,plain,sP28 <=> (b1 @ eigen__5),introduced(definition,[new_symbols(definition,[sP28])])). % 1.10/1.50 thf(sP29,plain,sP29 <=> (![X1:$i]:((![X2:$i]:(((irel @ X1) @ X2) => (b @ X2))) => (![X2:$i]:(((irel @ X1) @ X2) => ((~((![X3:$i]:(((irel @ X2) @ X3) => ((~((![X4:$i]:(((irel @ X3) @ X4) => (b1 @ X4))))) => (![X4:$i]:(((irel @ X3) @ X4) => (a1 @ X4)))))))) => (![X3:$i]:(((irel @ X2) @ X3) => (b1 @ X3)))))))),introduced(definition,[new_symbols(definition,[sP29])])). % 1.10/1.50 thf(sP30,plain,sP30 <=> (![X1:$i]:(((irel @ eigen__0) @ X1) => ((~((![X2:$i]:(((irel @ X1) @ X2) => ((~((![X3:$i]:(((irel @ X2) @ X3) => (b1 @ X3))))) => (![X3:$i]:(((irel @ X2) @ X3) => (a1 @ X3)))))))) => (![X2:$i]:(((irel @ X1) @ X2) => (b1 @ X2)))))),introduced(definition,[new_symbols(definition,[sP30])])). % 1.10/1.50 thf(sP31,plain,sP31 <=> ((irel @ eigen__1) @ eigen__5),introduced(definition,[new_symbols(definition,[sP31])])). % 1.10/1.50 thf(sP32,plain,sP32 <=> (![X1:$i]:(((irel @ eigen__1) @ X1) => ((~((![X2:$i]:(((irel @ X1) @ X2) => ((~((![X3:$i]:(((irel @ X2) @ X3) => (b2 @ X3))))) => (![X3:$i]:(((irel @ X2) @ X3) => (a2 @ X3)))))))) => (![X2:$i]:(((irel @ X1) @ X2) => (b2 @ X2)))))),introduced(definition,[new_symbols(definition,[sP32])])). % 1.10/1.50 thf(sP33,plain,sP33 <=> (((irel @ eigen__1) @ eigen__2) => ((~(sP23)) => sP12)),introduced(definition,[new_symbols(definition,[sP33])])). % 1.10/1.50 thf(sP34,plain,sP34 <=> (![X1:$i]:(((irel @ eigen__1) @ X1) => (a1 @ X1))),introduced(definition,[new_symbols(definition,[sP34])])). % 1.10/1.50 thf(sP35,plain,sP35 <=> ((~(sP15)) => sP34),introduced(definition,[new_symbols(definition,[sP35])])). % 1.10/1.50 thf(sP36,plain,sP36 <=> ((irel @ eigen__1) @ eigen__2),introduced(definition,[new_symbols(definition,[sP36])])). % 1.10/1.50 thf(sP37,plain,sP37 <=> (![X1:$i]:(((irel @ eigen__2) @ X1) => (~(((b1 @ X1) => (~((a2 @ X1)))))))),introduced(definition,[new_symbols(definition,[sP37])])). % 1.10/1.50 thf(sP38,plain,sP38 <=> (((irel @ eigen__0) @ eigen__1) => (~(((irel @ eigen__1) @ eigen__6)))),introduced(definition,[new_symbols(definition,[sP38])])). % 1.10/1.50 thf(sP39,plain,sP39 <=> ((~((![X1:$i]:(((irel @ eigen__1) @ X1) => (~(((b @ X1) => (~((a1 @ X1)))))))))) => (![X1:$i]:(((irel @ eigen__1) @ X1) => ((~((![X2:$i]:(((irel @ X1) @ X2) => (~(((b1 @ X2) => (~((a2 @ X2)))))))))) => (![X2:$i]:(((irel @ X1) @ X2) => (~(((b2 @ X2) => (~((a3 @ X2)))))))))))),introduced(definition,[new_symbols(definition,[sP39])])). % 1.10/1.50 thf(sP40,plain,sP40 <=> (![X1:$i]:(((irel @ eigen__0) @ X1) => (a @ X1))),introduced(definition,[new_symbols(definition,[sP40])])). % 1.10/1.50 thf(sP41,plain,sP41 <=> (((irel @ eigen__0) @ eigen__1) => sP39),introduced(definition,[new_symbols(definition,[sP41])])). % 1.10/1.50 thf(sP42,plain,sP42 <=> ((irel @ eigen__1) @ eigen__6),introduced(definition,[new_symbols(definition,[sP42])])). % 1.10/1.50 thf(sP43,plain,sP43 <=> ((![X1:$i]:(((irel @ eigen__0) @ X1) => (b @ X1))) => sP30),introduced(definition,[new_symbols(definition,[sP43])])). % 1.10/1.50 thf(sP44,plain,sP44 <=> (sP42 => (a1 @ eigen__6)),introduced(definition,[new_symbols(definition,[sP44])])). % 1.10/1.50 thf(sP45,plain,sP45 <=> (sP31 => sP28),introduced(definition,[new_symbols(definition,[sP45])])). % 1.10/1.50 thf(sP46,plain,sP46 <=> ((irel @ eigen__2) @ eigen__2),introduced(definition,[new_symbols(definition,[sP46])])). % 1.10/1.50 thf(sP47,plain,sP47 <=> ((~(sP6)) => sP31),introduced(definition,[new_symbols(definition,[sP47])])). % 1.10/1.50 thf(sP48,plain,sP48 <=> (sP21 => (~(((b2 @ eigen__3) => (~((a3 @ eigen__3))))))),introduced(definition,[new_symbols(definition,[sP48])])). % 1.10/1.50 thf(sP49,plain,sP49 <=> (a2 @ eigen__5),introduced(definition,[new_symbols(definition,[sP49])])). % 1.10/1.50 thf(sP50,plain,sP50 <=> (sP36 => ((~(sP37)) => sP1)),introduced(definition,[new_symbols(definition,[sP50])])). % 1.10/1.50 thf(sP51,plain,sP51 <=> (b2 @ eigen__3),introduced(definition,[new_symbols(definition,[sP51])])). % 1.10/1.50 thf(sP52,plain,sP52 <=> (![X1:$i]:(![X2:$i]:(![X3:$i]:((~((((irel @ X1) @ X2) => (~(((irel @ X2) @ X3)))))) => ((irel @ X1) @ X3))))),introduced(definition,[new_symbols(definition,[sP52])])). % 1.10/1.50 thf(sP53,plain,sP53 <=> (sP51 => (~((a3 @ eigen__3)))),introduced(definition,[new_symbols(definition,[sP53])])). % 1.10/1.50 thf(sP54,plain,sP54 <=> (![X1:$i]:((~((![X2:$i]:(((irel @ X1) @ X2) => (a @ X2))))) => (![X2:$i]:(((irel @ X1) @ X2) => ((~((![X3:$i]:(((irel @ X2) @ X3) => (~(((b @ X3) => (~((a1 @ X3)))))))))) => (![X3:$i]:(((irel @ X2) @ X3) => ((~((![X4:$i]:(((irel @ X3) @ X4) => (~(((b1 @ X4) => (~((a2 @ X4)))))))))) => (![X4:$i]:(((irel @ X3) @ X4) => (~(((b2 @ X4) => (~((a3 @ X4)))))))))))))))),introduced(definition,[new_symbols(definition,[sP54])])). % 1.10/1.50 thf(sP55,plain,sP55 <=> ((~(sP23)) => sP12),introduced(definition,[new_symbols(definition,[sP55])])). % 1.10/1.50 thf(sP56,plain,sP56 <=> ((~((![X1:$i]:(((irel @ eigen__0) @ X1) => (b @ X1))))) => sP40),introduced(definition,[new_symbols(definition,[sP56])])). % 1.10/1.50 thf(sP57,plain,sP57 <=> ((~(sP27)) => (![X1:$i]:(((irel @ eigen__0) @ X1) => (b @ X1)))),introduced(definition,[new_symbols(definition,[sP57])])). % 1.10/1.50 thf(sP58,plain,sP58 <=> ((~(sP40)) => sP5),introduced(definition,[new_symbols(definition,[sP58])])). % 1.10/1.50 thf(sP59,plain,sP59 <=> (sP13 => (b @ eigen__6)),introduced(definition,[new_symbols(definition,[sP59])])). % 1.10/1.50 thf(sP60,plain,sP60 <=> ((irel @ eigen__0) @ eigen__1),introduced(definition,[new_symbols(definition,[sP60])])). % 1.10/1.50 thf(sP61,plain,sP61 <=> (sP42 => (~(sP9))),introduced(definition,[new_symbols(definition,[sP61])])). % 1.10/1.50 thf(sP62,plain,sP62 <=> ((irel @ eigen__2) @ eigen__5),introduced(definition,[new_symbols(definition,[sP62])])). % 1.10/1.50 thf(sP63,plain,sP63 <=> (sP15 => sP32),introduced(definition,[new_symbols(definition,[sP63])])). % 1.10/1.50 thf(sP64,plain,sP64 <=> (![X1:$i]:(![X2:$i]:((~((((irel @ eigen__0) @ X1) => (~(((irel @ X1) @ X2)))))) => ((irel @ eigen__0) @ X2)))),introduced(definition,[new_symbols(definition,[sP64])])). % 1.10/1.50 thf(sP65,plain,sP65 <=> (sP60 => sP17),introduced(definition,[new_symbols(definition,[sP65])])). % 1.10/1.50 thf(sP66,plain,sP66 <=> (sP62 => (~(sP16))),introduced(definition,[new_symbols(definition,[sP66])])). % 1.10/1.50 thf(sP67,plain,sP67 <=> (![X1:$i]:(((irel @ eigen__1) @ X1) => ((~((![X2:$i]:(((irel @ X1) @ X2) => (b1 @ X2))))) => (![X2:$i]:(((irel @ X1) @ X2) => (a1 @ X2)))))),introduced(definition,[new_symbols(definition,[sP67])])). % 1.10/1.50 thf(sP68,plain,sP68 <=> (![X1:$i]:(((irel @ eigen__1) @ X1) => ((~((![X2:$i]:(((irel @ X1) @ X2) => (~(((b1 @ X2) => (~((a2 @ X2)))))))))) => (![X2:$i]:(((irel @ X1) @ X2) => (~(((b2 @ X2) => (~((a3 @ X2))))))))))),introduced(definition,[new_symbols(definition,[sP68])])). % 1.10/1.50 thf(sP69,plain,sP69 <=> (b @ eigen__6),introduced(definition,[new_symbols(definition,[sP69])])). % 1.10/1.50 thf(sP70,plain,sP70 <=> (![X1:$i]:(((irel @ eigen__1) @ X1) => (~(((b @ X1) => (~((a1 @ X1)))))))),introduced(definition,[new_symbols(definition,[sP70])])). % 1.10/1.50 thf(sP71,plain,sP71 <=> (a1 @ eigen__6),introduced(definition,[new_symbols(definition,[sP71])])). % 1.10/1.50 thf(sP72,plain,sP72 <=> ((!!) @ a3),introduced(definition,[new_symbols(definition,[sP72])])). % 1.10/1.50 thf(sP73,plain,sP73 <=> (![X1:$i]:(((irel @ eigen__0) @ X1) => (b @ X1))),introduced(definition,[new_symbols(definition,[sP73])])). % 1.10/1.50 thf(sP74,plain,sP74 <=> (a3 @ eigen__3),introduced(definition,[new_symbols(definition,[sP74])])). % 1.10/1.50 thf(sP75,plain,sP75 <=> ((~(sP37)) => sP1),introduced(definition,[new_symbols(definition,[sP75])])). % 1.10/1.50 thf(sP76,plain,sP76 <=> ((irel @ eigen__0) @ eigen__0),introduced(definition,[new_symbols(definition,[sP76])])). % 1.10/1.50 thf(def_mnot,definition,(mnot = (^[X1:$i>$o]:(^[X2:$i]:(~((X1 @ X2))))))). % 1.10/1.50 thf(def_mor,definition,(mor = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:((~((X1 @ X3))) => (X2 @ X3))))))). % 1.10/1.50 thf(def_mand,definition,(mand = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:(~(((X1 @ X3) => (~((X2 @ X3))))))))))). % 1.10/1.50 thf(def_mimplies,definition,(mimplies = (^[X1:$i>$o]:(mor @ (mnot @ X1))))). % 1.10/1.50 thf(def_mbox_s4,definition,(mbox_s4 = (^[X1:$i>$o]:(^[X2:$i]:(![X3:$i]:(((irel @ X2) @ X3) => (X1 @ X3))))))). % 1.10/1.50 thf(def_iatom,definition,(iatom = (^[X1:$i>$o]:X1))). % 1.10/1.50 thf(def_inot,definition,(inot = (^[X1:$i>$o]:(mnot @ (mbox_s4 @ X1))))). % 1.10/1.50 thf(def_itrue,definition,(itrue = (^[X1:$i]:(~($false))))). % 1.10/1.50 thf(def_ifalse,definition,(ifalse = (inot @ itrue))). % 1.10/1.50 thf(def_iand,definition,(iand = mand)). % 1.10/1.50 thf(def_ior,definition,(ior = (^[X1:$i>$o]:(^[X2:$i>$o]:((mor @ (mbox_s4 @ X1)) @ (mbox_s4 @ X2)))))). % 1.10/1.50 thf(def_iimplies,definition,(iimplies = (^[X1:$i>$o]:(^[X2:$i>$o]:((mimplies @ (mbox_s4 @ X1)) @ (mbox_s4 @ X2)))))). % 1.10/1.50 thf(def_iimplied,definition,(iimplied = (^[X1:$i>$o]:(^[X2:$i>$o]:((iimplies @ X2) @ X1))))). % 1.10/1.50 thf(def_iequiv,definition,(iequiv = (^[X1:$i>$o]:(^[X2:$i>$o]:((iand @ ((iimplies @ X1) @ X2)) @ ((iimplies @ X2) @ X1)))))). % 1.10/1.50 thf(def_ixor,definition,(ixor = (^[X1:$i>$o]:(^[X2:$i>$o]:(inot @ ((iequiv @ X1) @ X2)))))). % 1.10/1.50 thf(def_ivalid,definition,(ivalid = (!!))). % 1.10/1.50 thf(def_isatisfiable,definition,(isatisfiable = (^[X1:$i>$o]:(~((![X2:$i]:(~((X1 @ X2))))))))). % 1.10/1.50 thf(def_icountersatisfiable,definition,(icountersatisfiable = (^[X1:$i>$o]:(~(((!!) @ X1)))))). % 1.10/1.50 thf(def_iinvalid,definition,(iinvalid = (^[X1:$i>$o]:(![X2:$i]:(~((X1 @ X2))))))). % 1.10/1.50 thf(con,conjecture,sP54). % 1.10/1.50 thf(h1,negated_conjecture,(~(sP54)),inference(assume_negation,[status(cth)],[con])). % 1.10/1.50 thf(1,plain,((~(sP8) | ~(sP62)) | sP49),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(2,plain,(~(sP20) | sP47),inference(all_rule,[status(thm)],[])). % 1.10/1.50 thf(3,plain,((~(sP47) | sP6) | sP31),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(4,plain,((~(sP6) | ~(sP36)) | ~(sP62)),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(5,plain,(~(sP25) | sP8),inference(all_rule,[status(thm)],[])). % 1.10/1.50 thf(6,plain,(~(sP15) | sP45),inference(all_rule,[status(thm)],[])). % 1.10/1.50 thf(7,plain,((~(sP45) | ~(sP31)) | sP28),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(8,plain,((~(sP44) | ~(sP42)) | sP71),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(9,plain,(~(sP10) | sP19),inference(all_rule,[status(thm)],[])). % 1.10/1.50 thf(10,plain,((~(sP19) | sP38) | sP13),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(11,plain,((~(sP38) | ~(sP60)) | ~(sP42)),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(12,plain,(~(sP34) | sP44),inference(all_rule,[status(thm)],[])). % 1.10/1.50 thf(13,plain,(~(sP73) | sP59),inference(all_rule,[status(thm)],[])). % 1.10/1.50 thf(14,plain,((~(sP59) | ~(sP13)) | sP69),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(15,plain,(~(sP64) | sP10),inference(all_rule,[status(thm)],[])). % 1.10/1.50 thf(16,plain,(~(sP18) | sP20),inference(all_rule,[status(thm)],[])). % 1.10/1.50 thf(17,plain,((~(sP9) | ~(sP69)) | ~(sP71)),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(18,plain,(sP61 | sP9),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(19,plain,(sP61 | sP42),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(20,plain,((~(sP16) | ~(sP28)) | ~(sP49)),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(21,plain,(sP66 | sP16),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(22,plain,(sP66 | sP62),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(23,plain,(~(sP27) | sP22),inference(all_rule,[status(thm)],[])). % 1.10/1.50 thf(24,plain,((~(sP22) | ~(sP76)) | sP56),inference(prop_rule,[status(thm)],[])). % 1.10/1.50 thf(25,plain,(~(sP52) | sP64),inference(all_rule,[status(thm)],[])). % 1.10/1.50 thf(26,plain,(~(sP2) | sP76),inference(all_rule,[status(thm)],[])). % 1.10/1.50 thf(27,plain,(~(sP29) | sP43),inference(all_rule,[status(thm)],[])). % 1.10/1.50 thf(28,plain,((~(sP43) | ~(sP73)) | sP30),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(29,plain,(~(sP30) | sP65),inference(all_rule,[status(thm)],[])). % 1.10/1.51 thf(30,plain,((~(sP65) | ~(sP60)) | sP17),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(31,plain,(~(sP4) | sP57),inference(all_rule,[status(thm)],[])). % 1.10/1.51 thf(32,plain,((~(sP57) | sP27) | sP73),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(33,plain,((~(sP56) | sP73) | sP40),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(34,plain,(sP70 | ~(sP61)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__6])). % 1.10/1.51 thf(35,plain,(~(sP67) | sP3),inference(all_rule,[status(thm)],[])). % 1.10/1.51 thf(36,plain,((~(sP3) | ~(sP11)) | sP35),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(37,plain,(~(sP52) | sP18),inference(all_rule,[status(thm)],[])). % 1.10/1.51 thf(38,plain,(~(sP2) | sP11),inference(all_rule,[status(thm)],[])). % 1.10/1.51 thf(39,plain,(~(sP14) | sP63),inference(all_rule,[status(thm)],[])). % 1.10/1.51 thf(40,plain,((~(sP63) | ~(sP15)) | sP32),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(41,plain,(~(sP32) | sP33),inference(all_rule,[status(thm)],[])). % 1.10/1.51 thf(42,plain,((~(sP33) | ~(sP36)) | sP55),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(43,plain,((~(sP35) | sP15) | sP34),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(44,plain,((~(sP17) | sP67) | sP15),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(45,plain,(sP37 | ~(sP66)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__5])). % 1.10/1.51 thf(46,plain,(~(sP23) | sP24),inference(all_rule,[status(thm)],[])). % 1.10/1.51 thf(47,plain,((~(sP24) | ~(sP46)) | sP7),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(48,plain,(~(sP2) | sP46),inference(all_rule,[status(thm)],[])). % 1.10/1.51 thf(49,plain,((~(sP55) | sP23) | sP12),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(50,plain,((~(sP7) | sP12) | sP25),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(51,plain,(~(sP12) | sP26),inference(all_rule,[status(thm)],[])). % 1.10/1.51 thf(52,plain,((~(sP26) | ~(sP21)) | sP51),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(53,plain,(~(sP72) | sP74),inference(all_rule,[status(thm)],[])). % 1.10/1.51 thf(54,plain,((~(sP53) | ~(sP51)) | ~(sP74)),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(55,plain,(sP48 | sP53),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(56,plain,(sP48 | sP21),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(57,plain,(sP1 | ~(sP48)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__3])). % 1.10/1.51 thf(58,plain,(sP75 | ~(sP1)),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(59,plain,(sP75 | ~(sP37)),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(60,plain,(sP50 | ~(sP75)),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(61,plain,(sP50 | sP36),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(62,plain,(sP68 | ~(sP50)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__2])). % 1.10/1.51 thf(63,plain,(sP39 | ~(sP68)),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(64,plain,(sP39 | ~(sP70)),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(65,plain,(sP41 | ~(sP39)),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(66,plain,(sP41 | sP60),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(67,plain,(sP5 | ~(sP41)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__1])). % 1.10/1.51 thf(68,plain,(sP58 | ~(sP5)),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(69,plain,(sP58 | ~(sP40)),inference(prop_rule,[status(thm)],[])). % 1.10/1.51 thf(70,plain,(sP54 | ~(sP58)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__0])). % 1.10/1.51 thf(axiom4,axiom,(ivalid @ ((ior @ ((ior @ (iatom @ b)) @ (iatom @ a))) @ (iatom @ b)))). % 1.10/1.51 thf(71,plain,sP4,inference(preprocess,[status(thm)],[axiom4]). % 1.10/1.51 thf(axiom3,axiom,(ivalid @ ((iimplies @ (iatom @ b)) @ ((ior @ ((ior @ (iatom @ b1)) @ (iatom @ a1))) @ (iatom @ b1))))). % 1.10/1.51 thf(72,plain,sP29,inference(preprocess,[status(thm)],[axiom3]). % 1.10/1.51 thf(axiom2,axiom,(ivalid @ ((iimplies @ (iatom @ b1)) @ ((ior @ ((ior @ (iatom @ b2)) @ (iatom @ a2))) @ (iatom @ b2))))). % 1.10/1.51 thf(73,plain,sP14,inference(preprocess,[status(thm)],[axiom2]). % 1.10/1.51 thf(axiom1,axiom,(ivalid @ (iatom @ a3))). % 1.10/1.51 thf(74,plain,sP72,inference(preprocess,[status(thm)],[axiom1]). % 1.10/1.51 thf(trans_axiom,axiom,sP52). % 1.10/1.51 thf(refl_axiom,axiom,sP2). % 1.10/1.51 thf(75,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,trans_axiom,refl_axiom,h1])). % 1.10/1.51 thf(76,plain,$false,inference(eigenvar_choice,[status(thm),assumptions([h1]),eigenvar_choice(discharge,[h0])],[75,h0])). % 1.10/1.51 thf(0,theorem,sP54,inference(contra,[status(thm),contra(discharge,[h1])],[75,h1])). % 1.10/1.51 % SZS output end Proof %------------------------------------------------------------------------------