%------------------------------------------------------------------------------ % File : Satallax---3.5 % Problem : NUM746^4 : TPTP v9.2.0. Released v7.1.0. % Transfm : none % Format : tptp:raw % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s % Computer : n028.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:12:01 PM UTC 2025 % Result : Theorem 196.77s 195.71s % Output : Proof 196.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : NUM746^4 : TPTP v9.2.0. Released v7.1.0. % 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s % 0.13/0.34 % Computer : n028.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Oct 8 22:30:23 EDT 2025 % 0.13/0.34 % CPUTime : % 196.77/195.71 % SZS status Theorem % 196.77/195.71 % Mode: mode449:USE_SINE=true:SINE_TOLERANCE=5.0:SINE_GENERALITY_THRESHOLD=4:SINE_RANK_LIMIT=1.:SINE_DEPTH=0 % 196.77/195.71 % Inferences: 3995 % 196.77/195.71 % SZS output start Proof % 196.77/195.71 thf(ty_n_eq, type, n_eq : ($i>$i>$o)). % 196.77/195.71 thf(ty_d_not, type, d_not : ($o>$o)). % 196.77/195.71 thf(ty_nat, type, nat : $i). % 196.77/195.71 thf(ty_eigen__2, type, eigen__2 : $i). % 196.77/195.71 thf(ty_is_of, type, is_of : ($i>($i>$o)>$o)). % 196.77/195.71 thf(ty_eigen__1, type, eigen__1 : $i). % 196.77/195.71 thf(ty_eigen__0, type, eigen__0 : $i). % 196.77/195.71 thf(ty_l_or, type, l_or : ($o>$o>$o)). % 196.77/195.71 thf(ty_moreq, type, moreq : ($i>$i>$o)). % 196.77/195.71 thf(ty_moref, type, moref : ($i>$i>$o)). % 196.77/195.71 thf(ty_lessf, type, lessf : ($i>$i>$o)). % 196.77/195.71 thf(ty_pair1type, type, pair1type : ($i>$i)). % 196.77/195.71 thf(ty_in, type, in : ($i>$i>$o)). % 196.77/195.71 thf(h0, assumption, (![X1:$i>$o]:(![X2:$i]:((X1 @ X2) => (X1 @ (eps__0 @ X1))))),introduced(assumption,[])). % 196.77/195.71 thf(eigendef_eigen__1, definition, eigen__1 = (eps__0 @ (^[X1:$i]:(~((((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__0) @ X1)) @ ((n_eq @ eigen__0) @ X1)) => (((l_or @ ((lessf @ X1) @ X2)) @ ((n_eq @ X1) @ X2)) => ((l_or @ ((lessf @ eigen__0) @ X2)) @ ((n_eq @ eigen__0) @ X2))))))))))), introduced(definition,[new_symbols(definition,[eigen__1])])). % 196.77/195.71 thf(eigendef_eigen__0, definition, eigen__0 = (eps__0 @ (^[X1:$i]:(~((((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (![X3:$i]:(((is_of @ X3) @ (^[X4:$i]:((in @ X4) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ X1) @ X2)) @ ((n_eq @ X1) @ X2)) => (((l_or @ ((lessf @ X2) @ X3)) @ ((n_eq @ X2) @ X3)) => ((l_or @ ((lessf @ X1) @ X3)) @ ((n_eq @ X1) @ X3))))))))))))), introduced(definition,[new_symbols(definition,[eigen__0])])). % 196.77/195.71 thf(eigendef_eigen__2, definition, eigen__2 = (eps__0 @ (^[X1:$i]:(~((((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__0) @ eigen__1)) @ ((n_eq @ eigen__0) @ eigen__1)) => (((l_or @ ((lessf @ eigen__1) @ X1)) @ ((n_eq @ eigen__1) @ X1)) => ((l_or @ ((lessf @ eigen__0) @ X1)) @ ((n_eq @ eigen__0) @ X1))))))))), introduced(definition,[new_symbols(definition,[eigen__2])])). % 196.77/195.71 thf(sP1,plain,sP1 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__1) @ eigen__1)) @ ((n_eq @ eigen__1) @ eigen__1)) => (((n_eq @ eigen__1) @ eigen__2) => (((n_eq @ eigen__1) @ X1) => ((l_or @ ((lessf @ eigen__2) @ X1)) @ ((n_eq @ eigen__2) @ X1)))))))),introduced(definition,[new_symbols(definition,[sP1])])). % 196.77/195.71 thf(sP2,plain,sP2 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__0) @ eigen__0)) @ ((n_eq @ eigen__0) @ eigen__0)) => (((n_eq @ eigen__0) @ eigen__2) => (((n_eq @ eigen__0) @ X1) => ((l_or @ ((lessf @ eigen__2) @ X1)) @ ((n_eq @ eigen__2) @ X1)))))))),introduced(definition,[new_symbols(definition,[sP2])])). % 196.77/195.71 thf(sP3,plain,sP3 <=> ((d_not @ ((moref @ eigen__0) @ eigen__2)) => ((l_or @ ((lessf @ eigen__0) @ eigen__2)) @ ((n_eq @ eigen__0) @ eigen__2))),introduced(definition,[new_symbols(definition,[sP3])])). % 196.77/195.71 thf(sP4,plain,sP4 <=> ((moref @ eigen__0) @ eigen__0),introduced(definition,[new_symbols(definition,[sP4])])). % 196.77/195.71 thf(sP5,plain,sP5 <=> (((is_of @ eigen__1) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__0) @ eigen__1)) @ ((n_eq @ eigen__0) @ eigen__1)) => (d_not @ ((moref @ eigen__0) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP5])])). % 196.77/195.71 thf(sP6,plain,sP6 <=> (((moref @ eigen__0) @ eigen__1) => (((moreq @ eigen__1) @ eigen__0) => sP4)),introduced(definition,[new_symbols(definition,[sP6])])). % 196.77/195.71 thf(sP7,plain,sP7 <=> ((moref @ eigen__2) @ eigen__2),introduced(definition,[new_symbols(definition,[sP7])])). % 196.77/195.71 thf(sP8,plain,sP8 <=> (((is_of @ eigen__1) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => ((d_not @ ((moref @ eigen__2) @ eigen__1)) => ((l_or @ ((lessf @ eigen__2) @ eigen__1)) @ ((n_eq @ eigen__2) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP8])])). % 196.77/195.71 thf(sP9,plain,sP9 <=> ((l_or @ ((lessf @ eigen__0) @ eigen__1)) @ ((n_eq @ eigen__0) @ eigen__1)),introduced(definition,[new_symbols(definition,[sP9])])). % 196.77/195.71 thf(sP10,plain,sP10 <=> (d_not @ ((moref @ eigen__2) @ eigen__1)),introduced(definition,[new_symbols(definition,[sP10])])). % 196.77/195.71 thf(sP11,plain,sP11 <=> (((moref @ eigen__1) @ eigen__2) = sP4),introduced(definition,[new_symbols(definition,[sP11])])). % 196.77/195.71 thf(sP12,plain,sP12 <=> (d_not @ ((moref @ eigen__0) @ eigen__1)),introduced(definition,[new_symbols(definition,[sP12])])). % 196.77/195.71 thf(sP13,plain,sP13 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (sP7 => (((moreq @ eigen__2) @ X1) => ((moref @ eigen__2) @ X1)))))),introduced(definition,[new_symbols(definition,[sP13])])). % 196.77/195.71 thf(sP14,plain,sP14 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((moref @ eigen__1) @ eigen__1) => (((moreq @ eigen__1) @ X1) => ((moref @ eigen__1) @ X1))))),introduced(definition,[new_symbols(definition,[sP14])])). % 196.77/195.71 thf(sP15,plain,sP15 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__0) @ eigen__0)) @ ((n_eq @ eigen__0) @ eigen__0)) => (((n_eq @ eigen__0) @ eigen__2) => (((n_eq @ eigen__0) @ X1) => ((l_or @ ((lessf @ eigen__2) @ X1)) @ ((n_eq @ eigen__2) @ X1))))))),introduced(definition,[new_symbols(definition,[sP15])])). % 196.77/195.71 thf(sP16,plain,sP16 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__1) @ eigen__0)) @ ((n_eq @ eigen__1) @ eigen__0)) => (((lessf @ eigen__0) @ eigen__2) => ((lessf @ eigen__1) @ eigen__2)))),introduced(definition,[new_symbols(definition,[sP16])])). % 196.77/195.71 thf(sP17,plain,sP17 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__2) @ X1)) @ ((n_eq @ eigen__2) @ X1)) => (d_not @ ((moref @ eigen__2) @ X1))))),introduced(definition,[new_symbols(definition,[sP17])])). % 196.77/195.71 thf(sP18,plain,sP18 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (![X3:$i]:(((is_of @ X3) @ (^[X4:$i]:((in @ X4) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__0) @ X1)) @ ((n_eq @ eigen__0) @ X1)) => (((n_eq @ eigen__0) @ X2) => (((n_eq @ X1) @ X3) => ((l_or @ ((lessf @ X2) @ X3)) @ ((n_eq @ X2) @ X3))))))))))),introduced(definition,[new_symbols(definition,[sP18])])). % 196.77/195.71 thf(sP19,plain,sP19 <=> (((is_of @ eigen__0) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__0) @ X1)) @ ((n_eq @ eigen__0) @ X1)) => (((lessf @ X1) @ X2) => ((lessf @ eigen__0) @ X2)))))))),introduced(definition,[new_symbols(definition,[sP19])])). % 196.77/195.71 thf(sP20,plain,sP20 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((moref @ eigen__1) @ eigen__2) => (((moreq @ eigen__2) @ X1) => ((moref @ eigen__1) @ X1)))))),introduced(definition,[new_symbols(definition,[sP20])])). % 196.77/195.71 thf(sP21,plain,sP21 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (((moref @ eigen__0) @ X1) => (((moreq @ X1) @ X2) => ((moref @ eigen__0) @ X2))))))),introduced(definition,[new_symbols(definition,[sP21])])). % 196.77/195.71 thf(sP22,plain,sP22 <=> (((moref @ eigen__0) @ eigen__2) => (((moreq @ eigen__2) @ eigen__1) => ((moref @ eigen__0) @ eigen__1))),introduced(definition,[new_symbols(definition,[sP22])])). % 196.77/195.71 thf(sP23,plain,sP23 <=> (((is_of @ eigen__0) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__0) @ X1)) @ ((n_eq @ eigen__0) @ X1)) => (((l_or @ ((lessf @ X1) @ X2)) @ ((n_eq @ X1) @ X2)) => ((l_or @ ((lessf @ eigen__0) @ X2)) @ ((n_eq @ eigen__0) @ X2))))))))),introduced(definition,[new_symbols(definition,[sP23])])). % 196.77/195.71 thf(sP24,plain,sP24 <=> (((is_of @ eigen__1) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => ((d_not @ ((moref @ eigen__1) @ eigen__1)) => ((l_or @ ((lessf @ eigen__1) @ eigen__1)) @ ((n_eq @ eigen__1) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP24])])). % 196.77/195.71 thf(sP25,plain,sP25 <=> ((d_not @ sP4) => ((l_or @ ((lessf @ eigen__0) @ eigen__0)) @ ((n_eq @ eigen__0) @ eigen__0))),introduced(definition,[new_symbols(definition,[sP25])])). % 196.77/195.71 thf(sP26,plain,sP26 <=> (((moref @ eigen__1) @ eigen__2) => (((moreq @ eigen__2) @ eigen__1) => ((moref @ eigen__1) @ eigen__1))),introduced(definition,[new_symbols(definition,[sP26])])). % 196.77/195.71 thf(sP27,plain,sP27 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__0) @ eigen__0)) @ ((n_eq @ eigen__0) @ eigen__0)) => (((n_eq @ eigen__0) @ eigen__2) => (((n_eq @ eigen__0) @ eigen__2) => ((l_or @ ((lessf @ eigen__2) @ eigen__2)) @ ((n_eq @ eigen__2) @ eigen__2)))))),introduced(definition,[new_symbols(definition,[sP27])])). % 196.77/195.71 thf(sP28,plain,sP28 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__2) @ eigen__2)) @ ((n_eq @ eigen__2) @ eigen__2)) => (d_not @ sP7))),introduced(definition,[new_symbols(definition,[sP28])])). % 196.77/195.71 thf(sP29,plain,sP29 <=> (((is_of @ eigen__1) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (((moref @ eigen__1) @ X1) => (((moreq @ X1) @ X2) => ((moref @ eigen__1) @ X2)))))))),introduced(definition,[new_symbols(definition,[sP29])])). % 196.77/195.71 thf(sP30,plain,sP30 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (((moref @ eigen__2) @ X1) => (((moreq @ X1) @ X2) => ((moref @ eigen__2) @ X2))))))),introduced(definition,[new_symbols(definition,[sP30])])). % 196.77/195.71 thf(sP31,plain,sP31 <=> (sP10 => ((l_or @ ((lessf @ eigen__2) @ eigen__1)) @ ((n_eq @ eigen__2) @ eigen__1))),introduced(definition,[new_symbols(definition,[sP31])])). % 196.77/195.71 thf(sP32,plain,sP32 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__0) @ X1)) @ ((n_eq @ eigen__0) @ X1)) => ((moreq @ X1) @ eigen__0)))),introduced(definition,[new_symbols(definition,[sP32])])). % 196.77/195.71 thf(sP33,plain,sP33 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => ((d_not @ ((moref @ eigen__0) @ X1)) => ((l_or @ ((lessf @ eigen__0) @ X1)) @ ((n_eq @ eigen__0) @ X1))))),introduced(definition,[new_symbols(definition,[sP33])])). % 196.77/195.71 thf(sP34,plain,sP34 <=> (d_not @ ((moref @ eigen__1) @ eigen__1)),introduced(definition,[new_symbols(definition,[sP34])])). % 196.77/195.71 thf(sP35,plain,sP35 <=> ((((moref @ eigen__0) @ eigen__2) = ((moref @ eigen__1) @ eigen__2)) => (((moref @ eigen__1) @ eigen__2) = ((moref @ eigen__0) @ eigen__2))),introduced(definition,[new_symbols(definition,[sP35])])). % 196.77/195.71 thf(sP36,plain,sP36 <=> (d_not @ sP4),introduced(definition,[new_symbols(definition,[sP36])])). % 196.77/195.71 thf(sP37,plain,sP37 <=> ((moref @ eigen__1) @ eigen__2),introduced(definition,[new_symbols(definition,[sP37])])). % 196.77/195.71 thf(sP38,plain,sP38 <=> ((l_or @ ((lessf @ eigen__2) @ eigen__1)) @ ((n_eq @ eigen__2) @ eigen__1)),introduced(definition,[new_symbols(definition,[sP38])])). % 196.77/195.71 thf(sP39,plain,sP39 <=> ((moref @ eigen__1) @ eigen__0),introduced(definition,[new_symbols(definition,[sP39])])). % 196.77/195.71 thf(sP40,plain,sP40 <=> ((moref @ eigen__1) @ eigen__1),introduced(definition,[new_symbols(definition,[sP40])])). % 196.77/195.71 thf(sP41,plain,sP41 <=> ((moreq @ eigen__1) @ eigen__0),introduced(definition,[new_symbols(definition,[sP41])])). % 196.77/195.71 thf(sP42,plain,sP42 <=> (((n_eq @ eigen__1) @ eigen__2) => (((n_eq @ eigen__1) @ eigen__2) => ((l_or @ ((lessf @ eigen__2) @ eigen__2)) @ ((n_eq @ eigen__2) @ eigen__2)))),introduced(definition,[new_symbols(definition,[sP42])])). % 196.77/195.71 thf(sP43,plain,sP43 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => sP3),introduced(definition,[new_symbols(definition,[sP43])])). % 196.77/195.71 thf(sP44,plain,sP44 <=> (((is_of @ eigen__0) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__0) @ X1)) @ ((n_eq @ eigen__0) @ X1)) => (d_not @ ((moref @ eigen__0) @ X1)))))),introduced(definition,[new_symbols(definition,[sP44])])). % 196.77/195.71 thf(sP45,plain,sP45 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__1) @ eigen__0)) @ ((n_eq @ eigen__1) @ eigen__0)) => (((lessf @ eigen__0) @ X1) => ((lessf @ eigen__1) @ X1))))),introduced(definition,[new_symbols(definition,[sP45])])). % 196.77/195.71 thf(sP46,plain,sP46 <=> ((lessf @ eigen__1) @ eigen__2),introduced(definition,[new_symbols(definition,[sP46])])). % 196.77/195.71 thf(sP47,plain,sP47 <=> ((d_not @ sP39) => ((l_or @ ((lessf @ eigen__1) @ eigen__0)) @ ((n_eq @ eigen__1) @ eigen__0))),introduced(definition,[new_symbols(definition,[sP47])])). % 196.77/195.71 thf(sP48,plain,sP48 <=> (((l_or @ sP46) @ ((n_eq @ eigen__1) @ eigen__2)) => ((moreq @ eigen__2) @ eigen__1)),introduced(definition,[new_symbols(definition,[sP48])])). % 196.77/195.71 thf(sP49,plain,sP49 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (((moref @ eigen__1) @ X1) => (((moreq @ X1) @ X2) => ((moref @ eigen__1) @ X2))))))),introduced(definition,[new_symbols(definition,[sP49])])). % 196.77/195.71 thf(sP50,plain,sP50 <=> ((l_or @ ((lessf @ eigen__1) @ eigen__1)) @ ((n_eq @ eigen__1) @ eigen__1)),introduced(definition,[new_symbols(definition,[sP50])])). % 196.77/195.71 thf(sP51,plain,sP51 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => sP17),introduced(definition,[new_symbols(definition,[sP51])])). % 196.77/195.71 thf(sP52,plain,sP52 <=> (((is_of @ eigen__0) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => sP18),introduced(definition,[new_symbols(definition,[sP52])])). % 196.77/195.71 thf(sP53,plain,sP53 <=> (((moref @ eigen__0) @ eigen__1) => (((moreq @ eigen__1) @ eigen__2) => ((moref @ eigen__0) @ eigen__2))),introduced(definition,[new_symbols(definition,[sP53])])). % 196.77/195.71 thf(sP54,plain,sP54 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__0) @ X1)) @ ((n_eq @ eigen__0) @ X1)) => (((lessf @ X1) @ X2) => ((lessf @ eigen__0) @ X2))))))),introduced(definition,[new_symbols(definition,[sP54])])). % 196.77/195.71 thf(sP55,plain,sP55 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => ((d_not @ ((moref @ X1) @ X2)) => ((l_or @ ((lessf @ X1) @ X2)) @ ((n_eq @ X1) @ X2))))))),introduced(definition,[new_symbols(definition,[sP55])])). % 196.77/195.71 thf(sP56,plain,sP56 <=> (sP7 = ((moref @ eigen__0) @ eigen__2)),introduced(definition,[new_symbols(definition,[sP56])])). % 196.77/195.71 thf(sP57,plain,sP57 <=> (((is_of @ eigen__0) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => sP21),introduced(definition,[new_symbols(definition,[sP57])])). % 196.77/195.71 thf(sP58,plain,sP58 <=> (sP41 => sP39),introduced(definition,[new_symbols(definition,[sP58])])). % 196.77/195.71 thf(sP59,plain,sP59 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (sP9 => (((lessf @ eigen__1) @ X1) => ((lessf @ eigen__0) @ X1))))),introduced(definition,[new_symbols(definition,[sP59])])). % 196.77/195.71 thf(sP60,plain,sP60 <=> (d_not @ sP37),introduced(definition,[new_symbols(definition,[sP60])])). % 196.77/195.71 thf(sP61,plain,sP61 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (![X3:$i]:(((is_of @ X3) @ (^[X4:$i]:((in @ X4) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__1) @ X1)) @ ((n_eq @ eigen__1) @ X1)) => (((n_eq @ eigen__1) @ X2) => (((n_eq @ X1) @ X3) => ((l_or @ ((lessf @ X2) @ X3)) @ ((n_eq @ X2) @ X3))))))))))),introduced(definition,[new_symbols(definition,[sP61])])). % 196.77/195.71 thf(sP62,plain,sP62 <=> ((moref @ eigen__2) @ eigen__1),introduced(definition,[new_symbols(definition,[sP62])])). % 196.77/195.71 thf(sP63,plain,sP63 <=> (((moreq @ eigen__1) @ eigen__2) => ((moref @ eigen__0) @ eigen__2)),introduced(definition,[new_symbols(definition,[sP63])])). % 196.77/195.71 thf(sP64,plain,sP64 <=> (((n_eq @ eigen__1) @ eigen__2) = ((n_eq @ eigen__0) @ eigen__2)),introduced(definition,[new_symbols(definition,[sP64])])). % 196.77/195.71 thf(sP65,plain,sP65 <=> (((is_of @ eigen__0) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => sP33),introduced(definition,[new_symbols(definition,[sP65])])). % 196.77/195.71 thf(sP66,plain,sP66 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (![X3:$i]:(((is_of @ X3) @ (^[X4:$i]:((in @ X4) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ X1) @ X2)) @ ((n_eq @ X1) @ X2)) => (((lessf @ X2) @ X3) => ((lessf @ X1) @ X3))))))))),introduced(definition,[new_symbols(definition,[sP66])])). % 196.77/195.71 thf(sP67,plain,sP67 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__1) @ X1)) @ ((n_eq @ eigen__1) @ X1)) => ((moreq @ X1) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP67])])). % 196.77/195.71 thf(sP68,plain,sP68 <=> (((moreq @ eigen__2) @ eigen__1) => ((moref @ eigen__0) @ eigen__1)),introduced(definition,[new_symbols(definition,[sP68])])). % 196.77/195.71 thf(sP69,plain,sP69 <=> (((is_of @ eigen__1) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__1) @ X1)) @ ((n_eq @ eigen__1) @ X1)) => (d_not @ ((moref @ eigen__1) @ X1)))))),introduced(definition,[new_symbols(definition,[sP69])])). % 196.77/195.71 thf(sP70,plain,sP70 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => ((d_not @ ((moref @ eigen__2) @ X1)) => ((l_or @ ((lessf @ eigen__2) @ X1)) @ ((n_eq @ eigen__2) @ X1))))),introduced(definition,[new_symbols(definition,[sP70])])). % 196.77/195.71 thf(sP71,plain,sP71 <=> (sP41 => sP4),introduced(definition,[new_symbols(definition,[sP71])])). % 196.77/195.71 thf(sP72,plain,sP72 <=> (sP37 = sP62),introduced(definition,[new_symbols(definition,[sP72])])). % 196.77/195.71 thf(sP73,plain,sP73 <=> (((moreq @ eigen__2) @ eigen__1) => sP40),introduced(definition,[new_symbols(definition,[sP73])])). % 196.77/195.71 thf(sP74,plain,sP74 <=> (sP4 = sP39),introduced(definition,[new_symbols(definition,[sP74])])). % 196.77/195.71 thf(sP75,plain,sP75 <=> (((l_or @ sP46) @ ((n_eq @ eigen__1) @ eigen__2)) => ((l_or @ ((lessf @ eigen__0) @ eigen__2)) @ ((n_eq @ eigen__0) @ eigen__2))),introduced(definition,[new_symbols(definition,[sP75])])). % 196.77/195.71 thf(sP76,plain,sP76 <=> (sP46 => ((lessf @ eigen__0) @ eigen__2)),introduced(definition,[new_symbols(definition,[sP76])])). % 196.77/195.71 thf(sP77,plain,sP77 <=> (((n_eq @ eigen__0) @ eigen__2) => (((n_eq @ eigen__0) @ eigen__2) => ((l_or @ ((lessf @ eigen__2) @ eigen__2)) @ ((n_eq @ eigen__2) @ eigen__2)))),introduced(definition,[new_symbols(definition,[sP77])])). % 196.77/195.71 thf(sP78,plain,sP78 <=> (d_not @ ((moref @ eigen__0) @ eigen__2)),introduced(definition,[new_symbols(definition,[sP78])])). % 196.77/195.71 thf(sP79,plain,sP79 <=> ((moreq @ eigen__2) @ eigen__1),introduced(definition,[new_symbols(definition,[sP79])])). % 196.77/195.71 thf(sP80,plain,sP80 <=> (((is_of @ eigen__0) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => sP47),introduced(definition,[new_symbols(definition,[sP80])])). % 196.77/195.71 thf(sP81,plain,sP81 <=> ((l_or @ ((lessf @ eigen__0) @ eigen__2)) @ ((n_eq @ eigen__0) @ eigen__2)),introduced(definition,[new_symbols(definition,[sP81])])). % 196.77/195.71 thf(sP82,plain,sP82 <=> ((is_of @ eigen__0) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))),introduced(definition,[new_symbols(definition,[sP82])])). % 196.77/195.71 thf(sP83,plain,sP83 <=> (((n_eq @ eigen__0) @ eigen__2) => ((l_or @ ((lessf @ eigen__2) @ eigen__2)) @ ((n_eq @ eigen__2) @ eigen__2))),introduced(definition,[new_symbols(definition,[sP83])])). % 196.77/195.71 thf(sP84,plain,sP84 <=> (((l_or @ sP46) @ ((n_eq @ eigen__1) @ eigen__2)) => sP60),introduced(definition,[new_symbols(definition,[sP84])])). % 196.77/195.71 thf(sP85,plain,sP85 <=> (((l_or @ ((lessf @ eigen__0) @ eigen__0)) @ ((n_eq @ eigen__0) @ eigen__0)) => sP77),introduced(definition,[new_symbols(definition,[sP85])])). % 196.77/195.71 thf(sP86,plain,sP86 <=> (((n_eq @ eigen__1) @ eigen__2) => ((l_or @ ((lessf @ eigen__2) @ eigen__2)) @ ((n_eq @ eigen__2) @ eigen__2))),introduced(definition,[new_symbols(definition,[sP86])])). % 196.77/195.71 thf(sP87,plain,sP87 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (sP50 => sP42)),introduced(definition,[new_symbols(definition,[sP87])])). % 196.77/195.71 thf(sP88,plain,sP88 <=> (((moref @ eigen__0) @ eigen__2) = sP7),introduced(definition,[new_symbols(definition,[sP88])])). % 196.77/195.71 thf(sP89,plain,sP89 <=> (sP82 => sP32),introduced(definition,[new_symbols(definition,[sP89])])). % 196.77/195.71 thf(sP90,plain,sP90 <=> (sP82 => sP25),introduced(definition,[new_symbols(definition,[sP90])])). % 196.77/195.71 thf(sP91,plain,sP91 <=> (sP50 => sP42),introduced(definition,[new_symbols(definition,[sP91])])). % 196.77/195.71 thf(sP92,plain,sP92 <=> (((is_of @ eigen__1) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (sP38 => ((moreq @ eigen__1) @ eigen__2))),introduced(definition,[new_symbols(definition,[sP92])])). % 196.77/195.71 thf(sP93,plain,sP93 <=> (sP82 => sP45),introduced(definition,[new_symbols(definition,[sP93])])). % 196.77/195.71 thf(sP94,plain,sP94 <=> (sP9 => sP12),introduced(definition,[new_symbols(definition,[sP94])])). % 196.77/195.71 thf(sP95,plain,sP95 <=> (sP46 = ((lessf @ eigen__0) @ eigen__2)),introduced(definition,[new_symbols(definition,[sP95])])). % 196.77/195.71 thf(sP96,plain,sP96 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (sP50 => (((n_eq @ eigen__1) @ X1) => (((n_eq @ eigen__1) @ X2) => ((l_or @ ((lessf @ X1) @ X2)) @ ((n_eq @ X1) @ X2))))))))),introduced(definition,[new_symbols(definition,[sP96])])). % 196.77/195.71 thf(sP97,plain,sP97 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ X1) @ X2)) @ ((n_eq @ X1) @ X2)) => ((moreq @ X2) @ X1)))))),introduced(definition,[new_symbols(definition,[sP97])])). % 196.77/195.71 thf(sP98,plain,sP98 <=> (sP37 = ((moref @ eigen__0) @ eigen__2)),introduced(definition,[new_symbols(definition,[sP98])])). % 196.77/195.71 thf(sP99,plain,sP99 <=> (![X1:$o]:((((moref @ eigen__0) @ eigen__2) = X1) => (X1 = ((moref @ eigen__0) @ eigen__2)))),introduced(definition,[new_symbols(definition,[sP99])])). % 196.77/195.71 thf(sP100,plain,sP100 <=> ((l_or @ ((lessf @ eigen__1) @ eigen__0)) @ ((n_eq @ eigen__1) @ eigen__0)),introduced(definition,[new_symbols(definition,[sP100])])). % 196.77/195.71 thf(sP101,plain,sP101 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (sP7 => (((moreq @ eigen__2) @ X1) => ((moref @ eigen__2) @ X1))))),introduced(definition,[new_symbols(definition,[sP101])])). % 196.77/195.71 thf(sP102,plain,sP102 <=> ((n_eq @ eigen__0) @ eigen__2),introduced(definition,[new_symbols(definition,[sP102])])). % 196.77/195.71 thf(sP103,plain,sP103 <=> (((moref @ eigen__0) @ eigen__2) = sP37),introduced(definition,[new_symbols(definition,[sP103])])). % 196.77/195.71 thf(sP104,plain,sP104 <=> (d_not @ sP39),introduced(definition,[new_symbols(definition,[sP104])])). % 196.77/195.71 thf(sP105,plain,sP105 <=> (sP82 => (sP40 => sP58)),introduced(definition,[new_symbols(definition,[sP105])])). % 196.77/195.71 thf(sP106,plain,sP106 <=> ((is_of @ eigen__1) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))),introduced(definition,[new_symbols(definition,[sP106])])). % 196.77/195.71 thf(sP107,plain,sP107 <=> (![X1:$o]:(![X2:$o]:((X1 = X2) => (X2 = X1)))),introduced(definition,[new_symbols(definition,[sP107])])). % 196.77/195.71 thf(sP108,plain,sP108 <=> (sP40 => sP58),introduced(definition,[new_symbols(definition,[sP108])])). % 196.77/195.71 thf(sP109,plain,sP109 <=> (sP106 => sP61),introduced(definition,[new_symbols(definition,[sP109])])). % 196.77/195.71 thf(sP110,plain,sP110 <=> (((moref @ eigen__0) @ eigen__1) = ((moref @ eigen__0) @ eigen__2)),introduced(definition,[new_symbols(definition,[sP110])])). % 196.77/195.71 thf(sP111,plain,sP111 <=> (sP106 => (sP7 => (sP79 => sP62))),introduced(definition,[new_symbols(definition,[sP111])])). % 196.77/195.71 thf(sP112,plain,sP112 <=> (sP82 => sP6),introduced(definition,[new_symbols(definition,[sP112])])). % 196.77/195.71 thf(sP113,plain,sP113 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => sP70),introduced(definition,[new_symbols(definition,[sP113])])). % 196.77/195.71 thf(sP114,plain,sP114 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (![X3:$i]:(((is_of @ X3) @ (^[X4:$i]:((in @ X4) @ (pair1type @ nat)))) => (((moref @ X1) @ X2) => (((moreq @ X2) @ X3) => ((moref @ X1) @ X3))))))))),introduced(definition,[new_symbols(definition,[sP114])])). % 196.77/195.71 thf(sP115,plain,sP115 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => sP84),introduced(definition,[new_symbols(definition,[sP115])])). % 196.77/195.71 thf(sP116,plain,sP116 <=> (d_not @ sP7),introduced(definition,[new_symbols(definition,[sP116])])). % 196.77/195.71 thf(sP117,plain,sP117 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (![X3:$i]:(((is_of @ X3) @ (^[X4:$i]:((in @ X4) @ (pair1type @ nat)))) => (![X4:$i]:(((is_of @ X4) @ (^[X5:$i]:((in @ X5) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ X1) @ X2)) @ ((n_eq @ X1) @ X2)) => (((n_eq @ X1) @ X3) => (((n_eq @ X2) @ X4) => ((l_or @ ((lessf @ X3) @ X4)) @ ((n_eq @ X3) @ X4))))))))))))),introduced(definition,[new_symbols(definition,[sP117])])). % 196.77/195.71 thf(sP118,plain,sP118 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__0) @ X1)) @ ((n_eq @ eigen__0) @ X1)) => (d_not @ ((moref @ eigen__0) @ X1))))),introduced(definition,[new_symbols(definition,[sP118])])). % 196.77/195.71 thf(sP119,plain,sP119 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => sP30),introduced(definition,[new_symbols(definition,[sP119])])). % 196.77/195.71 thf(sP120,plain,sP120 <=> (((lessf @ eigen__0) @ eigen__2) => sP46),introduced(definition,[new_symbols(definition,[sP120])])). % 196.77/195.71 thf(sP121,plain,sP121 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__2) @ X1)) @ ((n_eq @ eigen__2) @ X1)) => ((moreq @ X1) @ eigen__2)))),introduced(definition,[new_symbols(definition,[sP121])])). % 196.77/195.71 thf(sP122,plain,sP122 <=> (sP106 => (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((moref @ eigen__0) @ eigen__1) => (((moreq @ eigen__1) @ X1) => ((moref @ eigen__0) @ X1)))))),introduced(definition,[new_symbols(definition,[sP122])])). % 196.77/195.71 thf(sP123,plain,sP123 <=> (sP37 = sP40),introduced(definition,[new_symbols(definition,[sP123])])). % 196.77/195.71 thf(sP124,plain,sP124 <=> ((l_or @ ((lessf @ eigen__0) @ eigen__0)) @ ((n_eq @ eigen__0) @ eigen__0)),introduced(definition,[new_symbols(definition,[sP124])])). % 196.77/195.71 thf(sP125,plain,sP125 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (![X3:$i]:(((is_of @ X3) @ (^[X4:$i]:((in @ X4) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ X1) @ X2)) @ ((n_eq @ X1) @ X2)) => (((l_or @ ((lessf @ X2) @ X3)) @ ((n_eq @ X2) @ X3)) => ((l_or @ ((lessf @ X1) @ X3)) @ ((n_eq @ X1) @ X3)))))))))),introduced(definition,[new_symbols(definition,[sP125])])). % 196.77/195.71 thf(sP126,plain,sP126 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (sP9 => sP76)),introduced(definition,[new_symbols(definition,[sP126])])). % 196.77/195.71 thf(sP127,plain,sP127 <=> (sP106 => (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__1) @ X1)) @ ((n_eq @ eigen__1) @ X1)) => (((lessf @ X1) @ X2) => ((lessf @ eigen__1) @ X2)))))))),introduced(definition,[new_symbols(definition,[sP127])])). % 196.77/195.71 thf(sP128,plain,sP128 <=> (sP106 => sP96),introduced(definition,[new_symbols(definition,[sP128])])). % 196.77/195.71 thf(sP129,plain,sP129 <=> (sP106 => sP59),introduced(definition,[new_symbols(definition,[sP129])])). % 196.77/195.71 thf(sP130,plain,sP130 <=> (sP9 => sP76),introduced(definition,[new_symbols(definition,[sP130])])). % 196.77/195.71 thf(sP131,plain,sP131 <=> (sP106 => (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => ((d_not @ ((moref @ eigen__1) @ X1)) => ((l_or @ ((lessf @ eigen__1) @ X1)) @ ((n_eq @ eigen__1) @ X1)))))),introduced(definition,[new_symbols(definition,[sP131])])). % 196.77/195.71 thf(sP132,plain,sP132 <=> (sP79 => sP62),introduced(definition,[new_symbols(definition,[sP132])])). % 196.77/195.71 thf(sP133,plain,sP133 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => sP53),introduced(definition,[new_symbols(definition,[sP133])])). % 196.77/195.71 thf(sP134,plain,sP134 <=> (sP34 => sP50),introduced(definition,[new_symbols(definition,[sP134])])). % 196.77/195.71 thf(sP135,plain,sP135 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (sP9 => (((l_or @ ((lessf @ eigen__1) @ X1)) @ ((n_eq @ eigen__1) @ X1)) => ((l_or @ ((lessf @ eigen__0) @ X1)) @ ((n_eq @ eigen__0) @ X1)))))),introduced(definition,[new_symbols(definition,[sP135])])). % 196.77/195.71 thf(sP136,plain,sP136 <=> (sP82 => (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (sP124 => (((n_eq @ eigen__0) @ X1) => (((n_eq @ eigen__0) @ X2) => ((l_or @ ((lessf @ X1) @ X2)) @ ((n_eq @ X1) @ X2)))))))))),introduced(definition,[new_symbols(definition,[sP136])])). % 196.77/195.71 thf(sP137,plain,sP137 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((moref @ eigen__0) @ eigen__2) => (((moreq @ eigen__2) @ X1) => ((moref @ eigen__0) @ X1)))))),introduced(definition,[new_symbols(definition,[sP137])])). % 196.77/195.71 thf(sP138,plain,sP138 <=> ((lessf @ eigen__0) @ eigen__2),introduced(definition,[new_symbols(definition,[sP138])])). % 196.77/195.71 thf(sP139,plain,sP139 <=> (sP9 => sP41),introduced(definition,[new_symbols(definition,[sP139])])). % 196.77/195.71 thf(sP140,plain,sP140 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => sP48),introduced(definition,[new_symbols(definition,[sP140])])). % 196.77/195.71 thf(sP141,plain,sP141 <=> (sP88 => sP56),introduced(definition,[new_symbols(definition,[sP141])])). % 196.77/195.71 thf(sP142,plain,sP142 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((moref @ eigen__0) @ eigen__1) => (((moreq @ eigen__1) @ X1) => ((moref @ eigen__0) @ X1))))),introduced(definition,[new_symbols(definition,[sP142])])). % 196.77/195.71 thf(sP143,plain,sP143 <=> (sP106 => sP135),introduced(definition,[new_symbols(definition,[sP143])])). % 196.77/195.71 thf(sP144,plain,sP144 <=> (((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))) => (sP9 => sP75)),introduced(definition,[new_symbols(definition,[sP144])])). % 196.77/195.71 thf(sP145,plain,sP145 <=> (sP106 => sP22),introduced(definition,[new_symbols(definition,[sP145])])). % 196.77/195.71 thf(sP146,plain,sP146 <=> ((is_of @ eigen__2) @ (^[X1:$i]:((in @ X1) @ (pair1type @ nat)))),introduced(definition,[new_symbols(definition,[sP146])])). % 196.77/195.71 thf(sP147,plain,sP147 <=> ((l_or @ sP46) @ ((n_eq @ eigen__1) @ eigen__2)),introduced(definition,[new_symbols(definition,[sP147])])). % 196.77/195.71 thf(sP148,plain,sP148 <=> (sP100 => sP120),introduced(definition,[new_symbols(definition,[sP148])])). % 196.77/195.71 thf(sP149,plain,sP149 <=> (sP38 => ((moreq @ eigen__1) @ eigen__2)),introduced(definition,[new_symbols(definition,[sP149])])). % 196.77/195.71 thf(sP150,plain,sP150 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__1) @ X1)) @ ((n_eq @ eigen__1) @ X1)) => (d_not @ ((moref @ eigen__1) @ X1))))),introduced(definition,[new_symbols(definition,[sP150])])). % 196.77/195.71 thf(sP151,plain,sP151 <=> (((l_or @ ((lessf @ eigen__2) @ eigen__2)) @ ((n_eq @ eigen__2) @ eigen__2)) => sP116),introduced(definition,[new_symbols(definition,[sP151])])). % 196.77/195.71 thf(sP152,plain,sP152 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__1) @ X1)) @ ((n_eq @ eigen__1) @ X1)) => (((lessf @ X1) @ X2) => ((lessf @ eigen__1) @ X2))))))),introduced(definition,[new_symbols(definition,[sP152])])). % 196.77/195.71 thf(sP153,plain,sP153 <=> (sP146 => sP121),introduced(definition,[new_symbols(definition,[sP153])])). % 196.77/195.71 thf(sP154,plain,sP154 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (sP124 => (((n_eq @ eigen__0) @ X1) => (((n_eq @ eigen__0) @ X2) => ((l_or @ ((lessf @ X1) @ X2)) @ ((n_eq @ X1) @ X2))))))))),introduced(definition,[new_symbols(definition,[sP154])])). % 196.77/195.71 thf(sP155,plain,sP155 <=> (sP7 => sP132),introduced(definition,[new_symbols(definition,[sP155])])). % 196.77/195.71 thf(sP156,plain,sP156 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (sP37 => (((moreq @ eigen__2) @ X1) => ((moref @ eigen__1) @ X1))))),introduced(definition,[new_symbols(definition,[sP156])])). % 196.77/195.71 thf(sP157,plain,sP157 <=> (sP106 => sP139),introduced(definition,[new_symbols(definition,[sP157])])). % 196.77/195.71 thf(sP158,plain,sP158 <=> (sP9 => sP75),introduced(definition,[new_symbols(definition,[sP158])])). % 196.77/195.71 thf(sP159,plain,sP159 <=> (sP106 => sP67),introduced(definition,[new_symbols(definition,[sP159])])). % 196.77/195.71 thf(sP160,plain,sP160 <=> ((l_or @ ((lessf @ eigen__2) @ eigen__2)) @ ((n_eq @ eigen__2) @ eigen__2)),introduced(definition,[new_symbols(definition,[sP160])])). % 196.77/195.71 thf(sP161,plain,sP161 <=> ((moreq @ eigen__1) @ eigen__2),introduced(definition,[new_symbols(definition,[sP161])])). % 196.77/195.71 thf(sP162,plain,sP162 <=> ((moref @ eigen__0) @ eigen__1),introduced(definition,[new_symbols(definition,[sP162])])). % 196.77/195.71 thf(sP163,plain,sP163 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (((moref @ eigen__0) @ eigen__2) => (((moreq @ eigen__2) @ X1) => ((moref @ eigen__0) @ X1))))),introduced(definition,[new_symbols(definition,[sP163])])). % 196.77/195.71 thf(sP164,plain,sP164 <=> ((n_eq @ eigen__1) @ eigen__2),introduced(definition,[new_symbols(definition,[sP164])])). % 196.77/195.71 thf(sP165,plain,sP165 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ eigen__0) @ X1)) @ ((n_eq @ eigen__0) @ X1)) => (((l_or @ ((lessf @ X1) @ X2)) @ ((n_eq @ X1) @ X2)) => ((l_or @ ((lessf @ eigen__0) @ X2)) @ ((n_eq @ eigen__0) @ X2)))))))),introduced(definition,[new_symbols(definition,[sP165])])). % 196.77/195.71 thf(sP166,plain,sP166 <=> ((moref @ eigen__0) @ eigen__2),introduced(definition,[new_symbols(definition,[sP166])])). % 196.77/195.71 thf(sP167,plain,sP167 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (sP50 => (sP164 => (((n_eq @ eigen__1) @ X1) => ((l_or @ ((lessf @ eigen__2) @ X1)) @ ((n_eq @ eigen__2) @ X1))))))),introduced(definition,[new_symbols(definition,[sP167])])). % 196.77/195.71 thf(sP168,plain,sP168 <=> (sP106 => sP26),introduced(definition,[new_symbols(definition,[sP168])])). % 196.77/195.71 thf(sP169,plain,sP169 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => (![X2:$i]:(((is_of @ X2) @ (^[X3:$i]:((in @ X3) @ (pair1type @ nat)))) => (((l_or @ ((lessf @ X1) @ X2)) @ ((n_eq @ X1) @ X2)) => (d_not @ ((moref @ X1) @ X2))))))),introduced(definition,[new_symbols(definition,[sP169])])). % 196.77/195.71 thf(sP170,plain,sP170 <=> (![X1:$i]:(((is_of @ X1) @ (^[X2:$i]:((in @ X2) @ (pair1type @ nat)))) => ((d_not @ ((moref @ eigen__1) @ X1)) => ((l_or @ ((lessf @ eigen__1) @ X1)) @ ((n_eq @ eigen__1) @ X1))))),introduced(definition,[new_symbols(definition,[sP170])])). % 196.77/195.71 thf(sP171,plain,sP171 <=> (sP106 => sP14),introduced(definition,[new_symbols(definition,[sP171])])). % 196.77/195.71 thf(def_all_of,definition,(all_of = (^[X1:$i>$o]:(^[X2:$i>$o]:(![X3:$i]:(((is_of @ X3) @ X1) => (X2 @ X3))))))). % 196.77/195.71 thf(def_frac,definition,(frac = (pair1type @ nat))). % 196.77/195.71 thf(def_lesseq,definition,(lesseq = (^[X1:$i]:(^[X2:$i]:((l_or @ ((lessf @ X1) @ X2)) @ ((n_eq @ X1) @ X2)))))). % 196.77/195.71 thf(satz52,conjecture,sP125). % 196.77/195.71 thf(h1,negated_conjecture,(~(sP125)),inference(assume_negation,[status(cth)],[satz52])). % 196.77/195.71 thf(1,plain,(~(sP163) | sP145),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(2,plain,((~(sP145) | ~(sP106)) | sP22),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(3,plain,((~(sP22) | ~(sP166)) | sP68),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(4,plain,((~(sP68) | ~(sP79)) | sP162),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(5,plain,(~(sP142) | sP112),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(6,plain,((~(sP112) | ~(sP82)) | sP6),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(7,plain,((~(sP6) | ~(sP162)) | sP71),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(8,plain,((~(sP71) | ~(sP41)) | sP4),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(9,plain,(~(sP142) | sP133),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(10,plain,((~(sP133) | ~(sP146)) | sP53),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(11,plain,((~(sP53) | ~(sP162)) | sP63),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(12,plain,((~(sP63) | ~(sP161)) | sP166),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(13,plain,(~(sP21) | sP137),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(14,plain,((~(sP137) | ~(sP146)) | sP163),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(15,plain,(~(sP21) | sP122),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(16,plain,((~(sP122) | ~(sP106)) | sP142),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(17,plain,(~(sP156) | sP168),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(18,plain,((~(sP168) | ~(sP106)) | sP26),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(19,plain,((~(sP26) | ~(sP37)) | sP73),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(20,plain,((~(sP73) | ~(sP79)) | sP40),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(21,plain,(~(sP14) | sP105),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(22,plain,((~(sP105) | ~(sP82)) | sP108),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(23,plain,((~(sP108) | ~(sP40)) | sP58),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(24,plain,((~(sP58) | ~(sP41)) | sP39),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(25,plain,(~(sP49) | sP20),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(26,plain,((~(sP20) | ~(sP146)) | sP156),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(27,plain,(~(sP49) | sP171),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(28,plain,((~(sP171) | ~(sP106)) | sP14),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(29,plain,(~(sP101) | sP111),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(30,plain,((~(sP111) | ~(sP106)) | sP155),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(31,plain,((~(sP155) | ~(sP7)) | sP132),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(32,plain,((~(sP132) | ~(sP79)) | sP62),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(33,plain,(~(sP30) | sP13),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(34,plain,((~(sP13) | ~(sP146)) | sP101),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(35,plain,(~(sP114) | sP119),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(36,plain,((~(sP119) | ~(sP146)) | sP30),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(37,plain,(~(sP114) | sP29),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(38,plain,((~(sP29) | ~(sP106)) | sP49),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(39,plain,(~(sP114) | sP57),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(40,plain,((~(sP57) | ~(sP82)) | sP21),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(41,plain,((sP74 | ~(sP4)) | ~(sP39)),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(42,plain,((~(sP36) | sP104) | ~(sP74)),inference(mating_rule,[status(thm)],[])). % 196.77/195.71 thf(43,plain,((~(sP116) | sP78) | ~(sP56)),inference(mating_rule,[status(thm)],[])). % 196.77/195.71 thf(44,plain,((sP103 | sP166) | sP37),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(45,plain,((sP88 | sP166) | sP7),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(46,plain,((~(sP141) | ~(sP88)) | sP56),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(47,plain,(~(sP99) | sP141),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(48,plain,((sP110 | ~(sP162)) | ~(sP166)),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(49,plain,((sP110 | sP162) | sP166),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(50,plain,((~(sP12) | sP78) | ~(sP110)),inference(mating_rule,[status(thm)],[])). % 196.77/195.71 thf(51,plain,((sP123 | ~(sP37)) | ~(sP40)),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(52,plain,((~(sP60) | sP34) | ~(sP123)),inference(mating_rule,[status(thm)],[])). % 196.77/195.71 thf(53,plain,((sP11 | ~(sP37)) | ~(sP4)),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(54,plain,((~(sP60) | sP36) | ~(sP11)),inference(mating_rule,[status(thm)],[])). % 196.77/195.71 thf(55,plain,((sP72 | ~(sP37)) | ~(sP62)),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(56,plain,((~(sP60) | sP10) | ~(sP72)),inference(mating_rule,[status(thm)],[])). % 196.77/195.71 thf(57,plain,((~(sP35) | ~(sP103)) | sP98),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(58,plain,(~(sP99) | sP35),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(59,plain,(~(sP107) | sP99),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(60,plain,((~(sP60) | sP78) | ~(sP98)),inference(mating_rule,[status(thm)],[])). % 196.77/195.71 thf(61,plain,(~(sP17) | sP28),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(62,plain,((~(sP28) | ~(sP146)) | sP151),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(63,plain,((~(sP151) | ~(sP160)) | sP116),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(64,plain,(~(sP118) | sP5),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(65,plain,((~(sP5) | ~(sP106)) | sP94),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(66,plain,((~(sP94) | ~(sP9)) | sP12),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(67,plain,(~(sP150) | sP115),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(68,plain,((~(sP115) | ~(sP146)) | sP84),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(69,plain,((~(sP84) | ~(sP147)) | sP60),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(70,plain,(~(sP169) | sP51),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(71,plain,((~(sP51) | ~(sP146)) | sP17),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(72,plain,(~(sP169) | sP69),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(73,plain,((~(sP69) | ~(sP106)) | sP150),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(74,plain,(~(sP169) | sP44),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(75,plain,((~(sP44) | ~(sP82)) | sP118),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(76,plain,(~(sP33) | sP43),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(77,plain,((~(sP43) | ~(sP146)) | sP3),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(78,plain,((~(sP3) | ~(sP78)) | sP81),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(79,plain,(~(sP70) | sP8),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(80,plain,((~(sP8) | ~(sP106)) | sP31),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(81,plain,((~(sP31) | ~(sP10)) | sP38),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(82,plain,(~(sP33) | sP90),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(83,plain,((~(sP90) | ~(sP82)) | sP25),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(84,plain,((~(sP25) | ~(sP36)) | sP124),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(85,plain,(~(sP170) | sP24),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(86,plain,((~(sP24) | ~(sP106)) | sP134),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(87,plain,((~(sP134) | ~(sP34)) | sP50),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(88,plain,(~(sP170) | sP80),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(89,plain,((~(sP80) | ~(sP82)) | sP47),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(90,plain,((~(sP47) | ~(sP104)) | sP100),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(91,plain,(~(sP55) | sP113),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(92,plain,((~(sP113) | ~(sP146)) | sP70),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(93,plain,(~(sP55) | sP131),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(94,plain,((~(sP131) | ~(sP106)) | sP170),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(95,plain,(~(sP55) | sP65),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(96,plain,((~(sP65) | ~(sP82)) | sP33),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(97,plain,(~(sP67) | sP140),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(98,plain,((~(sP140) | ~(sP146)) | sP48),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(99,plain,((~(sP48) | ~(sP147)) | sP79),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(100,plain,(~(sP32) | sP157),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(101,plain,((~(sP157) | ~(sP106)) | sP139),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(102,plain,((~(sP139) | ~(sP9)) | sP41),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(103,plain,(~(sP121) | sP92),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(104,plain,((~(sP92) | ~(sP106)) | sP149),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(105,plain,((~(sP149) | ~(sP38)) | sP161),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(106,plain,(~(sP97) | sP153),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(107,plain,((~(sP153) | ~(sP146)) | sP121),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(108,plain,(~(sP97) | sP159),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(109,plain,((~(sP159) | ~(sP106)) | sP67),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(110,plain,(~(sP97) | sP89),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(111,plain,((~(sP89) | ~(sP82)) | sP32),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(112,plain,(~(sP59) | sP126),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(113,plain,((~(sP126) | ~(sP146)) | sP130),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(114,plain,((~(sP130) | ~(sP9)) | sP76),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(115,plain,((~(sP76) | ~(sP46)) | sP138),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(116,plain,(~(sP54) | sP129),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(117,plain,((~(sP129) | ~(sP106)) | sP59),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(118,plain,(~(sP45) | sP16),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(119,plain,((~(sP16) | ~(sP146)) | sP148),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(120,plain,((~(sP148) | ~(sP100)) | sP120),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(121,plain,((~(sP120) | ~(sP138)) | sP46),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(122,plain,(~(sP152) | sP93),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(123,plain,((~(sP93) | ~(sP82)) | sP45),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(124,plain,(~(sP66) | sP127),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(125,plain,((~(sP127) | ~(sP106)) | sP152),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(126,plain,(~(sP66) | sP19),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(127,plain,((~(sP19) | ~(sP82)) | sP54),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(128,plain,(~(sP167) | sP87),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(129,plain,((~(sP87) | ~(sP146)) | sP91),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(130,plain,((~(sP91) | ~(sP50)) | sP42),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(131,plain,((~(sP42) | ~(sP164)) | sP86),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(132,plain,(~(sP96) | sP1),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(133,plain,((~(sP1) | ~(sP146)) | sP167),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(134,plain,(~(sP15) | sP27),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(135,plain,((~(sP27) | ~(sP146)) | sP85),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(136,plain,((~(sP85) | ~(sP124)) | sP77),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(137,plain,((~(sP77) | ~(sP102)) | sP83),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(138,plain,(~(sP154) | sP2),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(139,plain,((~(sP2) | ~(sP146)) | sP15),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(140,plain,(~(sP18) | sP136),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(141,plain,((~(sP136) | ~(sP82)) | sP154),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(142,plain,(~(sP61) | sP128),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(143,plain,((~(sP128) | ~(sP106)) | sP96),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(144,plain,((~(sP83) | ~(sP102)) | sP160),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(145,plain,((~(sP86) | ~(sP164)) | sP160),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(146,plain,(~(sP117) | sP109),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(147,plain,((~(sP109) | ~(sP106)) | sP61),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(148,plain,(~(sP117) | sP52),inference(all_rule,[status(thm)],[])). % 196.77/195.71 thf(149,plain,((~(sP52) | ~(sP82)) | sP18),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(150,plain,((sP95 | ~(sP46)) | ~(sP138)),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(151,plain,((sP95 | sP46) | sP138),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(152,plain,((sP64 | sP164) | sP102),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(153,plain,sP107,inference(eq_sym,[status(thm)],[])). % 196.77/195.71 thf(154,plain,(((~(sP147) | sP81) | ~(sP95)) | ~(sP64)),inference(mating_rule,[status(thm)],[])). % 196.77/195.71 thf(155,plain,(sP75 | ~(sP81)),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(156,plain,(sP75 | sP147),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(157,plain,(sP158 | ~(sP75)),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(158,plain,(sP158 | sP9),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(159,plain,(sP144 | ~(sP158)),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(160,plain,(sP144 | sP146),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(161,plain,(sP135 | ~(sP144)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__2])). % 196.77/195.71 thf(162,plain,(sP143 | ~(sP135)),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(163,plain,(sP143 | sP106),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(164,plain,(sP165 | ~(sP143)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__1])). % 196.77/195.71 thf(165,plain,(sP23 | ~(sP165)),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(166,plain,(sP23 | sP82),inference(prop_rule,[status(thm)],[])). % 196.77/195.71 thf(167,plain,(sP125 | ~(sP23)),inference(eigen_choice_rule,[status(thm),assumptions([h0])],[h0,eigendef_eigen__0])). % 196.77/195.71 thf(satz51d,axiom,((all_of @ (^[X1:$i]:((in @ X1) @ frac))) @ (^[X1:$i]:((all_of @ (^[X2:$i]:((in @ X2) @ frac))) @ (^[X2:$i]:((all_of @ (^[X3:$i]:((in @ X3) @ frac))) @ (^[X3:$i]:(((moref @ X1) @ X2) => (((moreq @ X2) @ X3) => ((moref @ X1) @ X3)))))))))). % 196.77/195.71 thf(168,plain,sP114,inference(preprocess,[status(thm)],[satz51d]). % 196.77/195.71 thf(satz51a,axiom,((all_of @ (^[X1:$i]:((in @ X1) @ frac))) @ (^[X1:$i]:((all_of @ (^[X2:$i]:((in @ X2) @ frac))) @ (^[X2:$i]:((all_of @ (^[X3:$i]:((in @ X3) @ frac))) @ (^[X3:$i]:(((lesseq @ X1) @ X2) => (((lessf @ X2) @ X3) => ((lessf @ X1) @ X3)))))))))). % 196.77/195.71 thf(169,plain,sP66,inference(preprocess,[status(thm)],[satz51a]). % 196.77/195.71 thf(satz49,axiom,((all_of @ (^[X1:$i]:((in @ X1) @ frac))) @ (^[X1:$i]:((all_of @ (^[X2:$i]:((in @ X2) @ frac))) @ (^[X2:$i]:(((lesseq @ X1) @ X2) => ((moreq @ X2) @ X1))))))). % 196.77/195.71 thf(170,plain,sP97,inference(preprocess,[status(thm)],[satz49]). % 196.77/195.71 thf(satz47,axiom,((all_of @ (^[X1:$i]:((in @ X1) @ frac))) @ (^[X1:$i]:((all_of @ (^[X2:$i]:((in @ X2) @ frac))) @ (^[X2:$i]:((all_of @ (^[X3:$i]:((in @ X3) @ frac))) @ (^[X3:$i]:((all_of @ (^[X4:$i]:((in @ X4) @ frac))) @ (^[X4:$i]:(((lesseq @ X1) @ X2) => (((n_eq @ X1) @ X3) => (((n_eq @ X2) @ X4) => ((lesseq @ X3) @ X4))))))))))))). % 196.77/195.71 thf(171,plain,sP117,inference(preprocess,[status(thm)],[satz47]). % 196.77/195.71 thf(satz41e,axiom,((all_of @ (^[X1:$i]:((in @ X1) @ frac))) @ (^[X1:$i]:((all_of @ (^[X2:$i]:((in @ X2) @ frac))) @ (^[X2:$i]:((d_not @ ((moref @ X1) @ X2)) => ((lesseq @ X1) @ X2))))))). % 196.77/195.71 thf(172,plain,sP55,inference(preprocess,[status(thm)],[satz41e]). % 196.77/195.71 thf(satz41d,axiom,((all_of @ (^[X1:$i]:((in @ X1) @ frac))) @ (^[X1:$i]:((all_of @ (^[X2:$i]:((in @ X2) @ frac))) @ (^[X2:$i]:(((lesseq @ X1) @ X2) => (d_not @ ((moref @ X1) @ X2)))))))). % 196.77/195.71 thf(173,plain,sP169,inference(preprocess,[status(thm)],[satz41d]). % 196.77/195.71 thf(174,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,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,h1])). % 196.77/195.71 thf(175,plain,$false,inference(eigenvar_choice,[status(thm),assumptions([h1]),eigenvar_choice(discharge,[h0])],[174,h0])). % 196.77/195.71 thf(0,theorem,sP125,inference(contra,[status(thm),contra(discharge,[h1])],[174,h1])). % 196.77/195.71 % SZS output end Proof %------------------------------------------------------------------------------