%------------------------------------------------------------------------------ % File : Satallax---3.5 % Problem : GRA082^1 : TPTP v9.2.0. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s % Computer : n006.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 01:32:38 PM UTC 2025 % Result : Unsatisfiable 85.47s 85.52s % Output : Proof 85.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : GRA082^1 : TPTP v9.2.0. Released v9.0.0. % 0.12/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s % 0.13/0.35 % Computer : n006.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Wed Oct 8 15:42:08 EDT 2025 % 0.13/0.35 % CPUTime : % 85.47/85.52 % SZS status Unsatisfiable % 85.47/85.52 % Mode: mode460 % 85.47/85.52 % Inferences: 23340 % 85.47/85.52 % SZS output start Proof % 85.47/85.52 thf(ty_eigen__1, type, eigen__1 : $i). % 85.47/85.52 thf(ty_b, type, b : ($i>$i>$o)). % 85.47/85.52 thf(ty_eigen__0, type, eigen__0 : ($i>$i)). % 85.47/85.52 thf(ty_r, type, r : ($i>$i>$o)). % 85.47/85.52 thf(sP1,plain,sP1 <=> (![X1:$i]:(![X2:$i]:(((eigen__0 @ X1) = (eigen__0 @ X2)) => (X1 = X2)))),introduced(definition,[new_symbols(definition,[sP1])])). % 85.47/85.52 thf(sP2,plain,sP2 <=> (eigen__1 = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP2])])). % 85.47/85.52 thf(sP3,plain,sP3 <=> ((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP3])])). % 85.47/85.52 thf(sP4,plain,sP4 <=> (![X1:$i]:(![X2:$i]:(![X3:$i]:((~(((~((((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X2)))))) => (~(((r @ X1) @ X2)))))) => (~(((r @ X2) @ X3))))))),introduced(definition,[new_symbols(definition,[sP4])])). % 85.47/85.52 thf(sP5,plain,sP5 <=> ((~(((~(((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))) => ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP5])])). % 85.47/85.52 thf(sP6,plain,sP6 <=> ((~((((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) => (~(((b @ (eigen__0 @ eigen__1)) @ eigen__1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP6])])). % 85.47/85.52 thf(sP7,plain,sP7 <=> ((b @ (eigen__0 @ eigen__1)) @ eigen__1),introduced(definition,[new_symbols(definition,[sP7])])). % 85.47/85.52 thf(sP8,plain,sP8 <=> ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP8])])). % 85.47/85.52 thf(sP9,plain,sP9 <=> ((~((((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP9])])). % 85.47/85.52 thf(sP10,plain,sP10 <=> (((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) => ((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP10])])). % 85.47/85.52 thf(sP11,plain,sP11 <=> (![X1:$i]:((~(((~((((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ eigen__1) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP11])])). % 85.47/85.52 thf(sP12,plain,sP12 <=> ((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = eigen__1),introduced(definition,[new_symbols(definition,[sP12])])). % 85.47/85.52 thf(sP13,plain,sP13 <=> ((~(((~((((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP13])])). % 85.47/85.52 thf(sP14,plain,sP14 <=> (sP7 => (~(((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP14])])). % 85.47/85.52 thf(sP15,plain,sP15 <=> ((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) = eigen__1),introduced(definition,[new_symbols(definition,[sP15])])). % 85.47/85.52 thf(sP16,plain,sP16 <=> (((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP16])])). % 85.47/85.52 thf(sP17,plain,sP17 <=> ((~(((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP17])])). % 85.47/85.52 thf(sP18,plain,sP18 <=> (![X1:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP18])])). % 85.47/85.52 thf(sP19,plain,sP19 <=> ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ eigen__1),introduced(definition,[new_symbols(definition,[sP19])])). % 85.47/85.52 thf(sP20,plain,sP20 <=> (![X1:$i]:(![X2:$i]:((~(((~((((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1)))))) => (~(((r @ (eigen__0 @ eigen__1)) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP20])])). % 85.47/85.52 thf(sP21,plain,sP21 <=> (((b @ eigen__1) @ (eigen__0 @ eigen__1)) => (~(((b @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP21])])). % 85.47/85.52 thf(sP22,plain,sP22 <=> ((~((((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP22])])). % 85.47/85.52 thf(sP23,plain,sP23 <=> ((~((((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP23])])). % 85.47/85.52 thf(sP24,plain,sP24 <=> ((~((((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1)) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP24])])). % 85.47/85.52 thf(sP25,plain,sP25 <=> ((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP25])])). % 85.47/85.52 thf(sP26,plain,sP26 <=> (((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP26])])). % 85.47/85.52 thf(sP27,plain,sP27 <=> ((b @ eigen__1) @ (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP27])])). % 85.47/85.52 thf(sP28,plain,sP28 <=> (![X1:$i]:(![X2:$i]:(![X3:$i]:((~(((~((((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X2)))))) => (~(((r @ X1) @ X2)))))) => (~(((r @ X2) @ X3))))))),introduced(definition,[new_symbols(definition,[sP28])])). % 85.47/85.52 thf(sP29,plain,sP29 <=> (((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => ((eigen__0 @ (eigen__0 @ eigen__1)) = (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP29])])). % 85.47/85.52 thf(sP30,plain,sP30 <=> (![X1:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1)))))) => (~(((b @ (eigen__0 @ eigen__1)) @ X1))))),introduced(definition,[new_symbols(definition,[sP30])])). % 85.47/85.52 thf(sP31,plain,sP31 <=> (((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP31])])). % 85.47/85.52 thf(sP32,plain,sP32 <=> ((~(((~((eigen__1 = (eigen__0 @ eigen__1)))) => ((r @ eigen__1) @ (eigen__0 @ eigen__1))))) => ((b @ eigen__1) @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP32])])). % 85.47/85.52 thf(sP33,plain,sP33 <=> (![X1:$i]:((~(((~(((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) = X1))) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1)))) => ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))),introduced(definition,[new_symbols(definition,[sP33])])). % 85.47/85.52 thf(sP34,plain,sP34 <=> (((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP34])])). % 85.47/85.52 thf(sP35,plain,sP35 <=> ((~(((~(((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = (eigen__0 @ eigen__1)))) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))))) => ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP35])])). % 85.47/85.52 thf(sP36,plain,sP36 <=> (((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP36])])). % 85.47/85.52 thf(sP37,plain,sP37 <=> ((~(((~((((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP37])])). % 85.47/85.52 thf(sP38,plain,sP38 <=> ((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))) => (~(sP25))),introduced(definition,[new_symbols(definition,[sP38])])). % 85.47/85.52 thf(sP39,plain,sP39 <=> ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP39])])). % 85.47/85.52 thf(sP40,plain,sP40 <=> ((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) = (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP40])])). % 85.47/85.52 thf(sP41,plain,sP41 <=> (sP25 => (~(((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP41])])). % 85.47/85.52 thf(sP42,plain,sP42 <=> (![X1:$i]:((~(((~((((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ eigen__1)))))))) => (~(sP8))))) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1))))),introduced(definition,[new_symbols(definition,[sP42])])). % 85.47/85.52 thf(sP43,plain,sP43 <=> ((~(((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) = (eigen__0 @ (eigen__0 @ eigen__1))))) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP43])])). % 85.47/85.52 thf(sP44,plain,sP44 <=> (![X1:$i]:(((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) = (eigen__0 @ X1)) => ((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = X1))),introduced(definition,[new_symbols(definition,[sP44])])). % 85.47/85.52 thf(sP45,plain,sP45 <=> (((b @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(sP27))),introduced(definition,[new_symbols(definition,[sP45])])). % 85.47/85.52 thf(sP46,plain,sP46 <=> ((~((((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1)))))) => (~(sP7))),introduced(definition,[new_symbols(definition,[sP46])])). % 85.47/85.52 thf(sP47,plain,sP47 <=> ((~((((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP47])])). % 85.47/85.52 thf(sP48,plain,sP48 <=> (![X1:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1)))))) => (~(((b @ (eigen__0 @ eigen__1)) @ X1))))),introduced(definition,[new_symbols(definition,[sP48])])). % 85.47/85.52 thf(sP49,plain,sP49 <=> ((~(((~((((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ eigen__1) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))))))) => (~(((r @ eigen__1) @ (eigen__0 @ eigen__1))))))) => (~(((r @ (eigen__0 @ eigen__1)) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP49])])). % 85.47/85.52 thf(sP50,plain,sP50 <=> ((~(((~(((eigen__0 @ eigen__1) = (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) => ((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))) => sP25),introduced(definition,[new_symbols(definition,[sP50])])). % 85.47/85.52 thf(sP51,plain,sP51 <=> (((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = (eigen__0 @ eigen__1)) => ((eigen__0 @ (eigen__0 @ eigen__1)) = eigen__1)),introduced(definition,[new_symbols(definition,[sP51])])). % 85.47/85.52 thf(sP52,plain,sP52 <=> ((~(((~((((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((r @ (eigen__0 @ eigen__1)) @ eigen__1)))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ eigen__1)))))) => (~(((r @ eigen__1) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP52])])). % 85.47/85.52 thf(sP53,plain,sP53 <=> ((~(((~((((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(sP19))),introduced(definition,[new_symbols(definition,[sP53])])). % 85.47/85.52 thf(sP54,plain,sP54 <=> ((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ eigen__1)))))) => (~(sP7))),introduced(definition,[new_symbols(definition,[sP54])])). % 85.47/85.52 thf(sP55,plain,sP55 <=> (![X1:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ eigen__1) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1)))))) => (~(((b @ eigen__1) @ X1))))),introduced(definition,[new_symbols(definition,[sP55])])). % 85.47/85.52 thf(sP56,plain,sP56 <=> ((~((sP7 => (~(((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((b @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP56])])). % 85.47/85.52 thf(sP57,plain,sP57 <=> ((~(((~(((eigen__0 @ eigen__1) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))) => ((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))) => ((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP57])])). % 85.47/85.52 thf(sP58,plain,sP58 <=> (![X1:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1)))))) => (~(((b @ (eigen__0 @ eigen__1)) @ X1))))),introduced(definition,[new_symbols(definition,[sP58])])). % 85.47/85.52 thf(sP59,plain,sP59 <=> (((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP59])])). % 85.47/85.52 thf(sP60,plain,sP60 <=> ((~((((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ eigen__1))) => (~(((r @ eigen__1) @ (eigen__0 @ eigen__1))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP60])])). % 85.47/85.52 thf(sP61,plain,sP61 <=> (![X1:$i]:(![X2:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X2)))))) => (~(((b @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP61])])). % 85.47/85.52 thf(sP62,plain,sP62 <=> ((eigen__0 @ eigen__1) = (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP62])])). % 85.47/85.52 thf(sP63,plain,sP63 <=> (((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP63])])). % 85.47/85.52 thf(sP64,plain,sP64 <=> ((~((((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ eigen__1))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP64])])). % 85.47/85.52 thf(sP65,plain,sP65 <=> (((eigen__0 @ (eigen__0 @ eigen__1)) = (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => ((eigen__0 @ eigen__1) = (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP65])])). % 85.47/85.52 thf(sP66,plain,sP66 <=> (![X1:$i]:((~(((~((((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ eigen__1))) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1))))),introduced(definition,[new_symbols(definition,[sP66])])). % 85.47/85.52 thf(sP67,plain,sP67 <=> ((~(((~((((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP67])])). % 85.47/85.52 thf(sP68,plain,sP68 <=> (![X1:$i]:((~((sP27 => (~(((b @ eigen__1) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1))))),introduced(definition,[new_symbols(definition,[sP68])])). % 85.47/85.52 thf(sP69,plain,sP69 <=> (((b @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((b @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP69])])). % 85.47/85.52 thf(sP70,plain,sP70 <=> (![X1:$i]:(![X2:$i]:((~(((~((((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1)))))) => (~(((r @ eigen__1) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP70])])). % 85.47/85.52 thf(sP71,plain,sP71 <=> ((~(((~(sP40)) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ eigen__1))))) => ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP71])])). % 85.47/85.52 thf(sP72,plain,sP72 <=> ((eigen__1 = (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => sP12),introduced(definition,[new_symbols(definition,[sP72])])). % 85.47/85.52 thf(sP73,plain,sP73 <=> ((~((((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(sP7))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP73])])). % 85.47/85.52 thf(sP74,plain,sP74 <=> ((~(((~((((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))))))) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP74])])). % 85.47/85.52 thf(sP75,plain,sP75 <=> ((b @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP75])])). % 85.47/85.52 thf(sP76,plain,sP76 <=> ((~(((~((((r @ (eigen__0 @ eigen__1)) @ eigen__1) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP76])])). % 85.47/85.52 thf(sP77,plain,sP77 <=> ((~((((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP77])])). % 85.47/85.52 thf(sP78,plain,sP78 <=> ((~(sP12)) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ eigen__1)),introduced(definition,[new_symbols(definition,[sP78])])). % 85.47/85.52 thf(sP79,plain,sP79 <=> (![X1:$i]:((~(((~((((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP79])])). % 85.47/85.52 thf(sP80,plain,sP80 <=> (((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1)) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP80])])). % 85.47/85.52 thf(sP81,plain,sP81 <=> (![X1:$i]:(((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) = (eigen__0 @ X1)) => ((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) = X1))),introduced(definition,[new_symbols(definition,[sP81])])). % 85.47/85.52 thf(sP82,plain,sP82 <=> ((~((((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1))))))) => (~(((r @ eigen__1) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP82])])). % 85.47/85.52 thf(sP83,plain,sP83 <=> ((~((((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP83])])). % 85.47/85.52 thf(sP84,plain,sP84 <=> ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP84])])). % 85.47/85.52 thf(sP85,plain,sP85 <=> ((~((((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ (eigen__0 @ eigen__1)) @ eigen__1)))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP85])])). % 85.47/85.52 thf(sP86,plain,sP86 <=> ((~(((~((eigen__1 = (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) => ((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))) => ((b @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP86])])). % 85.47/85.52 thf(sP87,plain,sP87 <=> ((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP87])])). % 85.47/85.52 thf(sP88,plain,sP88 <=> (((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP88])])). % 85.47/85.52 thf(sP89,plain,sP89 <=> (![X1:$i]:(![X2:$i]:((~((((b @ eigen__1) @ X1) => (~(((b @ eigen__1) @ X2)))))) => (~(((b @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP89])])). % 85.47/85.52 thf(sP90,plain,sP90 <=> ((~(((~(((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) = eigen__1))) => sP19))) => ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ eigen__1)),introduced(definition,[new_symbols(definition,[sP90])])). % 85.47/85.52 thf(sP91,plain,sP91 <=> ((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) = eigen__1),introduced(definition,[new_symbols(definition,[sP91])])). % 85.47/85.52 thf(sP92,plain,sP92 <=> (sP84 => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP92])])). % 85.47/85.52 thf(sP93,plain,sP93 <=> ((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP93])])). % 85.47/85.52 thf(sP94,plain,sP94 <=> (![X1:$i]:((~(((~((((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP94])])). % 85.47/85.52 thf(sP95,plain,sP95 <=> ((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP95])])). % 85.47/85.52 thf(sP96,plain,sP96 <=> ((~((((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP96])])). % 85.47/85.52 thf(sP97,plain,sP97 <=> ((~(((eigen__0 @ eigen__1) = eigen__1))) => ((r @ (eigen__0 @ eigen__1)) @ eigen__1)),introduced(definition,[new_symbols(definition,[sP97])])). % 85.47/85.52 thf(sP98,plain,sP98 <=> ((~(((~((((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP98])])). % 85.47/85.52 thf(sP99,plain,sP99 <=> ((~(((~(((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))) => sP84),introduced(definition,[new_symbols(definition,[sP99])])). % 85.47/85.52 thf(sP100,plain,sP100 <=> ((~((((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP100])])). % 85.47/85.52 thf(sP101,plain,sP101 <=> (((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP101])])). % 85.47/85.52 thf(sP102,plain,sP102 <=> ((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ eigen__1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP102])])). % 85.47/85.52 thf(sP103,plain,sP103 <=> ((eigen__0 @ eigen__1) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP103])])). % 85.47/85.52 thf(sP104,plain,sP104 <=> ((~(((~((((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ eigen__1) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP104])])). % 85.47/85.52 thf(sP105,plain,sP105 <=> (![X1:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ eigen__1))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1))))),introduced(definition,[new_symbols(definition,[sP105])])). % 85.47/85.52 thf(sP106,plain,sP106 <=> (((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP106])])). % 85.47/85.52 thf(sP107,plain,sP107 <=> (((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1)) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP107])])). % 85.47/85.52 thf(sP108,plain,sP108 <=> ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ eigen__1),introduced(definition,[new_symbols(definition,[sP108])])). % 85.47/85.52 thf(sP109,plain,sP109 <=> (((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) = (eigen__0 @ (eigen__0 @ eigen__1))) => ((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP109])])). % 85.47/85.52 thf(sP110,plain,sP110 <=> (![X1:$i]:((~(sP64)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP110])])). % 85.47/85.52 thf(sP111,plain,sP111 <=> ((~((((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(sP87))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP111])])). % 85.47/85.52 thf(sP112,plain,sP112 <=> ((~(((~((((r @ (eigen__0 @ eigen__1)) @ eigen__1) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(sP39))),introduced(definition,[new_symbols(definition,[sP112])])). % 85.47/85.52 thf(sP113,plain,sP113 <=> ((~(((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP113])])). % 85.47/85.52 thf(sP114,plain,sP114 <=> ((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ eigen__1) => (~(sP84))))) => (~(((b @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP114])])). % 85.47/85.52 thf(sP115,plain,sP115 <=> ((~(((~(((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))) => ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP115])])). % 85.47/85.52 thf(sP116,plain,sP116 <=> ((~(sP43)) => ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP116])])). % 85.47/85.52 thf(sP117,plain,sP117 <=> (((r @ (eigen__0 @ eigen__1)) @ eigen__1) => (~(sP87))),introduced(definition,[new_symbols(definition,[sP117])])). % 85.47/85.52 thf(sP118,plain,sP118 <=> ((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1)) => (~(sP84))))) => (~(sP93))),introduced(definition,[new_symbols(definition,[sP118])])). % 85.47/85.52 thf(sP119,plain,sP119 <=> (((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ eigen__1) => (~(sP84))),introduced(definition,[new_symbols(definition,[sP119])])). % 85.47/85.52 thf(sP120,plain,sP120 <=> (![X1:$i]:((~(sP9)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP120])])). % 85.47/85.52 thf(sP121,plain,sP121 <=> ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ eigen__1),introduced(definition,[new_symbols(definition,[sP121])])). % 85.47/85.52 thf(sP122,plain,sP122 <=> ((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(sP84))),introduced(definition,[new_symbols(definition,[sP122])])). % 85.47/85.52 thf(sP123,plain,sP123 <=> (((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP123])])). % 85.47/85.52 thf(sP124,plain,sP124 <=> (((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP124])])). % 85.47/85.52 thf(sP125,plain,sP125 <=> ((~(((~((((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ eigen__1) @ (eigen__0 @ eigen__1))))))) => (~(sP39))))) => (~(((r @ (eigen__0 @ eigen__1)) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP125])])). % 85.47/85.52 thf(sP126,plain,sP126 <=> ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ eigen__1),introduced(definition,[new_symbols(definition,[sP126])])). % 85.47/85.52 thf(sP127,plain,sP127 <=> (![X1:$i]:((~(((~((((r @ (eigen__0 @ eigen__1)) @ eigen__1) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP127])])). % 85.47/85.52 thf(sP128,plain,sP128 <=> (((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP128])])). % 85.47/85.52 thf(sP129,plain,sP129 <=> ((~((((b @ eigen__1) @ (eigen__0 @ eigen__1)) => (~(sP75))))) => (~(((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP129])])). % 85.47/85.52 thf(sP130,plain,sP130 <=> ((~((((r @ (eigen__0 @ eigen__1)) @ eigen__1) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP130])])). % 85.47/85.52 thf(sP131,plain,sP131 <=> (![X1:$i]:((~(sP60)) => (~(((r @ (eigen__0 @ eigen__1)) @ X1))))),introduced(definition,[new_symbols(definition,[sP131])])). % 85.47/85.52 thf(sP132,plain,sP132 <=> (((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(sP25))),introduced(definition,[new_symbols(definition,[sP132])])). % 85.47/85.52 thf(sP133,plain,sP133 <=> (![X1:$i]:(((eigen__0 @ eigen__1) = (eigen__0 @ X1)) => (eigen__1 = X1))),introduced(definition,[new_symbols(definition,[sP133])])). % 85.47/85.52 thf(sP134,plain,sP134 <=> ((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP134])])). % 85.47/85.52 thf(sP135,plain,sP135 <=> ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP135])])). % 85.47/85.52 thf(sP136,plain,sP136 <=> (eigen__1 = (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP136])])). % 85.47/85.52 thf(sP137,plain,sP137 <=> (((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1)) => (~(sP84))),introduced(definition,[new_symbols(definition,[sP137])])). % 85.47/85.52 thf(sP138,plain,sP138 <=> (((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ eigen__1))) => (~(((r @ (eigen__0 @ eigen__1)) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP138])])). % 85.47/85.52 thf(sP139,plain,sP139 <=> ((~(((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP139])])). % 85.47/85.52 thf(sP140,plain,sP140 <=> (((r @ (eigen__0 @ eigen__1)) @ eigen__1) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP140])])). % 85.47/85.52 thf(sP141,plain,sP141 <=> ((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP141])])). % 85.47/85.52 thf(sP142,plain,sP142 <=> ((~((sP108 => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP142])])). % 85.47/85.52 thf(sP143,plain,sP143 <=> (((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP143])])). % 85.47/85.52 thf(sP144,plain,sP144 <=> ((eigen__0 @ eigen__1) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP144])])). % 85.47/85.52 thf(sP145,plain,sP145 <=> ((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP145])])). % 85.47/85.52 thf(sP146,plain,sP146 <=> (((b @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) => (~(((b @ eigen__1) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP146])])). % 85.47/85.52 thf(sP147,plain,sP147 <=> ((~((sP93 => (~(((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP147])])). % 85.47/85.52 thf(sP148,plain,sP148 <=> (((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1) => (~(sP134))),introduced(definition,[new_symbols(definition,[sP148])])). % 85.47/85.52 thf(sP149,plain,sP149 <=> (![X1:$i]:((~(((~((((r @ eigen__1) @ (eigen__0 @ eigen__1)) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP149])])). % 85.47/85.52 thf(sP150,plain,sP150 <=> ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP150])])). % 85.47/85.52 thf(sP151,plain,sP151 <=> (![X1:$i]:((~(sP83)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP151])])). % 85.47/85.52 thf(sP152,plain,sP152 <=> ((~((((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(sP93))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP152])])). % 85.47/85.52 thf(sP153,plain,sP153 <=> ((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) = (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP153])])). % 85.47/85.52 thf(sP154,plain,sP154 <=> ((~(sP59)) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP154])])). % 85.47/85.52 thf(sP155,plain,sP155 <=> (sP93 => (~(((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP155])])). % 85.47/85.52 thf(sP156,plain,sP156 <=> (![X1:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP156])])). % 85.47/85.52 thf(sP157,plain,sP157 <=> ((~((((b @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) => (~(sP75))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP157])])). % 85.47/85.52 thf(sP158,plain,sP158 <=> ((~(sP113)) => ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP158])])). % 85.47/85.52 thf(sP159,plain,sP159 <=> ((~(((~((sP108 => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(sP19))),introduced(definition,[new_symbols(definition,[sP159])])). % 85.47/85.52 thf(sP160,plain,sP160 <=> ((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP160])])). % 85.47/85.52 thf(sP161,plain,sP161 <=> ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ eigen__1),introduced(definition,[new_symbols(definition,[sP161])])). % 85.47/85.52 thf(sP162,plain,sP162 <=> ((~(sP124)) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP162])])). % 85.47/85.52 thf(sP163,plain,sP163 <=> (((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP163])])). % 85.47/85.52 thf(sP164,plain,sP164 <=> ((~(sP47)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP164])])). % 85.47/85.52 thf(sP165,plain,sP165 <=> (![X1:$i]:(![X2:$i]:((~(((~((((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ eigen__1))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1)))))) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP165])])). % 85.47/85.52 thf(sP166,plain,sP166 <=> ((~(((~(sP138)) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1)))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP166])])). % 85.47/85.52 thf(sP167,plain,sP167 <=> ((~((sP108 => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP167])])). % 85.47/85.52 thf(sP168,plain,sP168 <=> ((~(((~(sP117)) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(sP19))),introduced(definition,[new_symbols(definition,[sP168])])). % 85.47/85.52 thf(sP169,plain,sP169 <=> ((b @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP169])])). % 85.47/85.52 thf(sP170,plain,sP170 <=> ((~((((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(sP141))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP170])])). % 85.47/85.52 thf(sP171,plain,sP171 <=> ((~(sP14)) => (~(sP169))),introduced(definition,[new_symbols(definition,[sP171])])). % 85.47/85.52 thf(sP172,plain,sP172 <=> ((r @ (eigen__0 @ eigen__1)) @ eigen__1),introduced(definition,[new_symbols(definition,[sP172])])). % 85.47/85.52 thf(sP173,plain,sP173 <=> ((~(sP24)) => (~(sP8))),introduced(definition,[new_symbols(definition,[sP173])])). % 85.47/85.52 thf(sP174,plain,sP174 <=> ((~((((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP174])])). % 85.47/85.52 thf(sP175,plain,sP175 <=> (sP108 => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP175])])). % 85.47/85.52 thf(sP176,plain,sP176 <=> (![X1:$i]:(![X2:$i]:((~(((~((((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1)))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP176])])). % 85.47/85.52 thf(sP177,plain,sP177 <=> (![X1:$i]:(![X2:$i]:((~(((~((((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1)))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP177])])). % 85.47/85.52 thf(sP178,plain,sP178 <=> ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP178])])). % 85.47/85.52 thf(sP179,plain,sP179 <=> (((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP179])])). % 85.47/85.52 thf(sP180,plain,sP180 <=> (![X1:$i]:((~(((~((((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1))))))) => (~(sP39))))) => (~(((r @ (eigen__0 @ eigen__1)) @ X1))))),introduced(definition,[new_symbols(definition,[sP180])])). % 85.47/85.52 thf(sP181,plain,sP181 <=> (![X1:$i]:(![X2:$i]:((X1 = X2) => (X2 = X1)))),introduced(definition,[new_symbols(definition,[sP181])])). % 85.47/85.52 thf(sP182,plain,sP182 <=> (![X1:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1))))),introduced(definition,[new_symbols(definition,[sP182])])). % 85.47/85.52 thf(sP183,plain,sP183 <=> (![X1:$i]:((~(sP85)) => (~(((r @ eigen__1) @ X1))))),introduced(definition,[new_symbols(definition,[sP183])])). % 85.47/85.52 thf(sP184,plain,sP184 <=> ((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ eigen__1))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))))))) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP184])])). % 85.47/85.52 thf(sP185,plain,sP185 <=> ((~(((~(sP143)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))))))) => (~(sP87))),introduced(definition,[new_symbols(definition,[sP185])])). % 85.47/85.52 thf(sP186,plain,sP186 <=> ((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP186])])). % 85.47/85.52 thf(sP187,plain,sP187 <=> ((~(((~(sP80)) => (~(sP87))))) => (~(sP19))),introduced(definition,[new_symbols(definition,[sP187])])). % 85.47/85.52 thf(sP188,plain,sP188 <=> ((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP188])])). % 85.47/85.52 thf(sP189,plain,sP189 <=> ((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP189])])). % 85.47/85.52 thf(sP190,plain,sP190 <=> (((eigen__0 @ (eigen__0 @ eigen__1)) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => sP62),introduced(definition,[new_symbols(definition,[sP190])])). % 85.47/85.52 thf(sP191,plain,sP191 <=> (![X1:$i]:(![X2:$i]:((~(((~((sP160 => (~(((r @ (eigen__0 @ eigen__1)) @ X1)))))) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP191])])). % 85.47/85.52 thf(sP192,plain,sP192 <=> (((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP192])])). % 85.47/85.52 thf(sP193,plain,sP193 <=> ((~(sP138)) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP193])])). % 85.47/85.52 thf(sP194,plain,sP194 <=> ((~(sP117)) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP194])])). % 85.47/85.52 thf(sP195,plain,sP195 <=> (((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ eigen__1)) => (~(sP135))),introduced(definition,[new_symbols(definition,[sP195])])). % 85.47/85.52 thf(sP196,plain,sP196 <=> (![X1:$i]:((~((((b @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((b @ eigen__1) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1))))),introduced(definition,[new_symbols(definition,[sP196])])). % 85.47/85.52 thf(sP197,plain,sP197 <=> (sP93 => (~(sP7))),introduced(definition,[new_symbols(definition,[sP197])])). % 85.47/85.52 thf(sP198,plain,sP198 <=> ((eigen__0 @ (eigen__0 @ eigen__1)) = (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP198])])). % 85.47/85.52 thf(sP199,plain,sP199 <=> ((~(sP100)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP199])])). % 85.47/85.52 thf(sP200,plain,sP200 <=> ((~(sP92)) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP200])])). % 85.47/85.52 thf(sP201,plain,sP201 <=> ((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP201])])). % 85.47/85.52 thf(sP202,plain,sP202 <=> ((~(((~((eigen__1 = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))) => ((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))) => sP75),introduced(definition,[new_symbols(definition,[sP202])])). % 85.47/85.52 thf(sP203,plain,sP203 <=> (sP160 => (~(sP141))),introduced(definition,[new_symbols(definition,[sP203])])). % 85.47/85.52 thf(sP204,plain,sP204 <=> ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP204])])). % 85.47/85.52 thf(sP205,plain,sP205 <=> (((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ eigen__1))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP205])])). % 85.47/85.52 thf(sP206,plain,sP206 <=> ((~(sP17)) => ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP206])])). % 85.47/85.52 thf(sP207,plain,sP207 <=> (((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(sP93))),introduced(definition,[new_symbols(definition,[sP207])])). % 85.47/85.52 thf(sP208,plain,sP208 <=> ((b @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP208])])). % 85.47/85.52 thf(sP209,plain,sP209 <=> ((eigen__1 = (eigen__0 @ (eigen__0 @ eigen__1))) => ((eigen__0 @ (eigen__0 @ eigen__1)) = eigen__1)),introduced(definition,[new_symbols(definition,[sP209])])). % 85.47/85.52 thf(sP210,plain,sP210 <=> ((~(sP162)) => (~(sP108))),introduced(definition,[new_symbols(definition,[sP210])])). % 85.47/85.52 thf(sP211,plain,sP211 <=> ((~(sP97)) => sP7),introduced(definition,[new_symbols(definition,[sP211])])). % 85.47/85.52 thf(sP212,plain,sP212 <=> ((~(((~(((eigen__0 @ (eigen__0 @ eigen__1)) = eigen__1))) => ((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1)))) => ((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1)),introduced(definition,[new_symbols(definition,[sP212])])). % 85.47/85.52 thf(sP213,plain,sP213 <=> (sP208 => (~(sP169))),introduced(definition,[new_symbols(definition,[sP213])])). % 85.47/85.52 thf(sP214,plain,sP214 <=> ((~(sP85)) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP214])])). % 85.47/85.52 thf(sP215,plain,sP215 <=> ((~((eigen__1 = (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) => ((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP215])])). % 85.47/85.52 thf(sP216,plain,sP216 <=> (![X1:$i]:((~(((~(sP143)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))))))) => (~(((r @ (eigen__0 @ eigen__1)) @ X1))))),introduced(definition,[new_symbols(definition,[sP216])])). % 85.47/85.52 thf(sP217,plain,sP217 <=> (sP27 => (~(sP75))),introduced(definition,[new_symbols(definition,[sP217])])). % 85.47/85.52 thf(sP218,plain,sP218 <=> (![X1:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP218])])). % 85.47/85.52 thf(sP219,plain,sP219 <=> (![X1:$i]:(![X2:$i]:((~(((~((((r @ eigen__1) @ (eigen__0 @ eigen__1)) => (~(((r @ eigen__1) @ X1)))))) => (~(((r @ (eigen__0 @ eigen__1)) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP219])])). % 85.47/85.52 thf(sP220,plain,sP220 <=> ((~(sP192)) => (~(((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP220])])). % 85.47/85.52 thf(sP221,plain,sP221 <=> ((~(sP95)) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP221])])). % 85.47/85.52 thf(sP222,plain,sP222 <=> ((~(((~(sP153)) => sP8))) => ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP222])])). % 85.47/85.52 thf(sP223,plain,sP223 <=> ((~(sP143)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP223])])). % 85.47/85.52 thf(sP224,plain,sP224 <=> ((r @ eigen__1) @ (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP224])])). % 85.47/85.52 thf(sP225,plain,sP225 <=> (((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP225])])). % 85.47/85.52 thf(sP226,plain,sP226 <=> (sP62 => (eigen__1 = (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP226])])). % 85.47/85.52 thf(sP227,plain,sP227 <=> (![X1:$i]:((~(((~(sP148)) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP227])])). % 85.47/85.52 thf(sP228,plain,sP228 <=> ((~(((~((sP141 => (~(sP87))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP228])])). % 85.47/85.52 thf(sP229,plain,sP229 <=> ((~(sP111)) => (~(sP19))),introduced(definition,[new_symbols(definition,[sP229])])). % 85.47/85.52 thf(sP230,plain,sP230 <=> ((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP230])])). % 85.47/85.52 thf(sP231,plain,sP231 <=> (((eigen__0 @ (eigen__0 @ eigen__1)) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) => sP103),introduced(definition,[new_symbols(definition,[sP231])])). % 85.47/85.52 thf(sP232,plain,sP232 <=> ((~(((~((sP230 => (~(sP201))))) => (~(sP39))))) => (~(sP87))),introduced(definition,[new_symbols(definition,[sP232])])). % 85.47/85.52 thf(sP233,plain,sP233 <=> (sP121 => (~(sP204))),introduced(definition,[new_symbols(definition,[sP233])])). % 85.47/85.52 thf(sP234,plain,sP234 <=> ((~(sP31)) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP234])])). % 85.47/85.52 thf(sP235,plain,sP235 <=> ((~((sP27 => (~(sP169))))) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP235])])). % 85.47/85.52 thf(sP236,plain,sP236 <=> (![X1:$i]:(![X2:$i]:((~(((~((((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((r @ eigen__1) @ X1)))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP236])])). % 85.47/85.52 thf(sP237,plain,sP237 <=> (((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP237])])). % 85.47/85.52 thf(sP238,plain,sP238 <=> (((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) => ((eigen__0 @ (eigen__0 @ eigen__1)) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP238])])). % 85.47/85.52 thf(sP239,plain,sP239 <=> (![X1:$i]:(![X2:$i]:(![X3:$i]:((~(((~((((r @ (eigen__0 @ eigen__1)) @ X1) => (~(((r @ (eigen__0 @ eigen__1)) @ X2)))))) => (~(((r @ X1) @ X2)))))) => (~(((r @ X2) @ X3))))))),introduced(definition,[new_symbols(definition,[sP239])])). % 85.47/85.52 thf(sP240,plain,sP240 <=> (![X1:$i]:((~(((~(sP175)) => (~(sP224))))) => (~(((r @ (eigen__0 @ eigen__1)) @ X1))))),introduced(definition,[new_symbols(definition,[sP240])])). % 85.47/85.52 thf(sP241,plain,sP241 <=> (![X1:$i]:((~(sP111)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP241])])). % 85.47/85.52 thf(sP242,plain,sP242 <=> (![X1:$i]:((~(sP194)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP242])])). % 85.47/85.52 thf(sP243,plain,sP243 <=> ((~(sP63)) => (~(((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP243])])). % 85.47/85.52 thf(sP244,plain,sP244 <=> (sP186 => sP95),introduced(definition,[new_symbols(definition,[sP244])])). % 85.47/85.52 thf(sP245,plain,sP245 <=> ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP245])])). % 85.47/85.52 thf(sP246,plain,sP246 <=> (((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP246])])). % 85.47/85.52 thf(sP247,plain,sP247 <=> ((~(sP103)) => ((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP247])])). % 85.47/85.52 thf(sP248,plain,sP248 <=> ((~(sP194)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))),introduced(definition,[new_symbols(definition,[sP248])])). % 85.47/85.52 thf(sP249,plain,sP249 <=> ((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ eigen__1))))))) => (~(sP150))),introduced(definition,[new_symbols(definition,[sP249])])). % 85.47/85.52 thf(sP250,plain,sP250 <=> ((~(((~(sP2)) => ((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))) => sP169),introduced(definition,[new_symbols(definition,[sP250])])). % 85.47/85.52 thf(sP251,plain,sP251 <=> (((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(sP135))),introduced(definition,[new_symbols(definition,[sP251])])). % 85.47/85.52 thf(sP252,plain,sP252 <=> (![X1:$i]:(![X2:$i]:(![X3:$i]:((~(((~((((r @ eigen__1) @ X1) => (~(((r @ eigen__1) @ X2)))))) => (~(((r @ X1) @ X2)))))) => (~(((r @ X2) @ X3))))))),introduced(definition,[new_symbols(definition,[sP252])])). % 85.47/85.52 thf(sP253,plain,sP253 <=> ((eigen__0 @ eigen__1) = (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP253])])). % 85.47/85.52 thf(sP254,plain,sP254 <=> ((~((sP25 => (~(sP7))))) => (~(sP121))),introduced(definition,[new_symbols(definition,[sP254])])). % 85.47/85.52 thf(sP255,plain,sP255 <=> ((~(((~((((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1)) => (~(sP245))))) => (~(((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP255])])). % 85.47/85.52 thf(sP256,plain,sP256 <=> (((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(sP7))),introduced(definition,[new_symbols(definition,[sP256])])). % 85.47/85.52 thf(sP257,plain,sP257 <=> ((~(sP80)) => (~(sP87))),introduced(definition,[new_symbols(definition,[sP257])])). % 85.47/85.52 thf(sP258,plain,sP258 <=> (![X1:$i]:((~(sP162)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1))))),introduced(definition,[new_symbols(definition,[sP258])])). % 85.47/85.52 thf(sP259,plain,sP259 <=> (![X1:$i]:(![X2:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X2)))))) => (~(((b @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP259])])). % 85.47/85.52 thf(sP260,plain,sP260 <=> ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP260])])). % 85.47/85.52 thf(sP261,plain,sP261 <=> ((~(sP60)) => (~(sP172))),introduced(definition,[new_symbols(definition,[sP261])])). % 85.47/85.52 thf(sP262,plain,sP262 <=> ((~((sP141 => (~(sP87))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP262])])). % 85.47/85.52 thf(sP263,plain,sP263 <=> ((r @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP263])])). % 85.47/85.52 thf(sP264,plain,sP264 <=> ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP264])])). % 85.47/85.52 thf(sP265,plain,sP265 <=> (eigen__1 = (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP265])])). % 85.47/85.52 thf(sP266,plain,sP266 <=> ((~(sP130)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP266])])). % 85.47/85.52 thf(sP267,plain,sP267 <=> (![X1:$i]:((~(sP100)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP267])])). % 85.47/85.52 thf(sP268,plain,sP268 <=> ((~((((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(sP224))))) => (~(sP39))),introduced(definition,[new_symbols(definition,[sP268])])). % 85.47/85.52 thf(sP269,plain,sP269 <=> ((eigen__0 @ eigen__1) = eigen__1),introduced(definition,[new_symbols(definition,[sP269])])). % 85.47/85.52 thf(sP270,plain,sP270 <=> ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP270])])). % 85.47/85.52 thf(sP271,plain,sP271 <=> (sP188 => sP186),introduced(definition,[new_symbols(definition,[sP271])])). % 85.47/85.52 thf(sP272,plain,sP272 <=> ((~(sP203)) => (~(sP189))),introduced(definition,[new_symbols(definition,[sP272])])). % 85.47/85.52 thf(sP273,plain,sP273 <=> (![X1:$i]:(![X2:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X2)))))) => (~(((b @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP273])])). % 85.47/85.52 thf(sP274,plain,sP274 <=> ((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP274])])). % 85.47/85.52 thf(sP275,plain,sP275 <=> ((~(sP36)) => (~(sP84))),introduced(definition,[new_symbols(definition,[sP275])])). % 85.47/85.52 thf(sP276,plain,sP276 <=> ((~(sP40)) => sP178),introduced(definition,[new_symbols(definition,[sP276])])). % 85.47/85.52 thf(sP277,plain,sP277 <=> ((~((eigen__1 = (eigen__0 @ (eigen__0 @ eigen__1))))) => ((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP277])])). % 85.47/85.52 thf(sP278,plain,sP278 <=> ((b @ eigen__1) @ (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP278])])). % 85.47/85.52 thf(sP279,plain,sP279 <=> ((~(sP205)) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP279])])). % 85.47/85.52 thf(sP280,plain,sP280 <=> ((~((sP121 => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))))))) => (~(sP278))),introduced(definition,[new_symbols(definition,[sP280])])). % 85.47/85.52 thf(sP281,plain,sP281 <=> ((~(((~(sP253)) => sP160))) => ((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP281])])). % 85.47/85.52 thf(sP282,plain,sP282 <=> ((~(sP15)) => sP126),introduced(definition,[new_symbols(definition,[sP282])])). % 85.47/85.52 thf(sP283,plain,sP283 <=> ((~(((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = (eigen__0 @ eigen__1)))) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP283])])). % 85.47/85.52 thf(sP284,plain,sP284 <=> ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP284])])). % 85.47/85.52 thf(sP285,plain,sP285 <=> (((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(sP224))),introduced(definition,[new_symbols(definition,[sP285])])). % 85.47/85.52 thf(sP286,plain,sP286 <=> (![X1:$i]:((~(sP24)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP286])])). % 85.47/85.52 thf(sP287,plain,sP287 <=> (![X1:$i]:(![X2:$i]:(![X3:$i]:((~((((b @ X1) @ X2) => (~(((b @ X1) @ X3)))))) => (~(((b @ X2) @ X3))))))),introduced(definition,[new_symbols(definition,[sP287])])). % 85.47/85.52 thf(sP288,plain,sP288 <=> (![X1:$i]:((~(sP262)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP288])])). % 85.47/85.52 thf(sP289,plain,sP289 <=> (![X1:$i]:((~(sP47)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1))))),introduced(definition,[new_symbols(definition,[sP289])])). % 85.47/85.52 thf(sP290,plain,sP290 <=> (![X1:$i]:(![X2:$i]:((~(((~((sP263 => (~(((r @ (eigen__0 @ eigen__1)) @ X1)))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP290])])). % 85.47/85.52 thf(sP291,plain,sP291 <=> ((~(sP221)) => ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP291])])). % 85.47/85.52 thf(sP292,plain,sP292 <=> (sP144 => (eigen__1 = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP292])])). % 85.47/85.52 thf(sP293,plain,sP293 <=> ((~(sP175)) => (~(sP224))),introduced(definition,[new_symbols(definition,[sP293])])). % 85.47/85.52 thf(sP294,plain,sP294 <=> ((~(sP188)) => sP270),introduced(definition,[new_symbols(definition,[sP294])])). % 85.47/85.52 thf(sP295,plain,sP295 <=> ((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP295])])). % 85.47/85.52 thf(sP296,plain,sP296 <=> ((~(sP213)) => (~(sP84))),introduced(definition,[new_symbols(definition,[sP296])])). % 85.47/85.52 thf(sP297,plain,sP297 <=> (((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP297])])). % 85.47/85.52 thf(sP298,plain,sP298 <=> ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP298])])). % 85.47/85.52 thf(sP299,plain,sP299 <=> ((~((((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))) => (~(sP25))),introduced(definition,[new_symbols(definition,[sP299])])). % 85.47/85.52 thf(sP300,plain,sP300 <=> (![X1:$i]:(![X2:$i]:((~(((~((sP108 => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1)))))) => (~(((r @ eigen__1) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP300])])). % 85.47/85.52 thf(sP301,plain,sP301 <=> ((~(sP69)) => (~(sP284))),introduced(definition,[new_symbols(definition,[sP301])])). % 85.47/85.52 thf(sP302,plain,sP302 <=> ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP302])])). % 85.47/85.52 thf(sP303,plain,sP303 <=> (![X1:$i]:((~((sP7 => (~(((b @ (eigen__0 @ eigen__1)) @ X1)))))) => (~(((b @ eigen__1) @ X1))))),introduced(definition,[new_symbols(definition,[sP303])])). % 85.47/85.52 thf(sP304,plain,sP304 <=> (sP278 => (~(sP169))),introduced(definition,[new_symbols(definition,[sP304])])). % 85.47/85.52 thf(sP305,plain,sP305 <=> (((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ eigen__1))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP305])])). % 85.47/85.52 thf(sP306,plain,sP306 <=> ((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP306])])). % 85.47/85.52 thf(sP307,plain,sP307 <=> ((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP307])])). % 85.47/85.52 thf(sP308,plain,sP308 <=> ((~(((~((sP141 => (~(sP172))))) => (~(sP108))))) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP308])])). % 85.47/85.52 thf(sP309,plain,sP309 <=> ((~(sP136)) => sP224),introduced(definition,[new_symbols(definition,[sP309])])). % 85.47/85.52 thf(sP310,plain,sP310 <=> (![X1:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1)))))) => (~(((b @ (eigen__0 @ eigen__1)) @ X1))))),introduced(definition,[new_symbols(definition,[sP310])])). % 85.47/85.52 thf(sP311,plain,sP311 <=> (((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) = (eigen__0 @ eigen__1)) => sP12),introduced(definition,[new_symbols(definition,[sP311])])). % 85.47/85.52 thf(sP312,plain,sP312 <=> ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP312])])). % 85.47/85.52 thf(sP313,plain,sP313 <=> (![X1:$i]:(((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = (eigen__0 @ X1)) => ((eigen__0 @ (eigen__0 @ eigen__1)) = X1))),introduced(definition,[new_symbols(definition,[sP313])])). % 85.47/85.52 thf(sP314,plain,sP314 <=> ((~(sP146)) => (~(sP298))),introduced(definition,[new_symbols(definition,[sP314])])). % 85.47/85.52 thf(sP315,plain,sP315 <=> (sP169 => (~(sP75))),introduced(definition,[new_symbols(definition,[sP315])])). % 85.47/85.52 thf(sP316,plain,sP316 <=> (sP263 => (~(sP141))),introduced(definition,[new_symbols(definition,[sP316])])). % 85.47/85.52 thf(sP317,plain,sP317 <=> ((~(sP64)) => (~(sP270))),introduced(definition,[new_symbols(definition,[sP317])])). % 85.47/85.52 thf(sP318,plain,sP318 <=> ((~(sP272)) => (~(sP302))),introduced(definition,[new_symbols(definition,[sP318])])). % 85.47/85.52 thf(sP319,plain,sP319 <=> (![X1:$i]:(![X2:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X2)))))) => (~(((b @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP319])])). % 85.47/85.52 thf(sP320,plain,sP320 <=> (![X1:$i]:(![X2:$i]:((~(((~((sP189 => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1)))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP320])])). % 85.47/85.52 thf(sP321,plain,sP321 <=> ((eigen__0 @ (eigen__0 @ eigen__1)) = (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP321])])). % 85.47/85.52 thf(sP322,plain,sP322 <=> ((~(sP2)) => ((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP322])])). % 85.47/85.52 thf(sP323,plain,sP323 <=> (sP121 => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP323])])). % 85.47/85.52 thf(sP324,plain,sP324 <=> ((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) = (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP324])])). % 85.47/85.52 thf(sP325,plain,sP325 <=> ((~(sP251)) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP325])])). % 85.47/85.52 thf(sP326,plain,sP326 <=> (sP141 => (~(sP172))),introduced(definition,[new_symbols(definition,[sP326])])). % 85.47/85.52 thf(sP327,plain,sP327 <=> ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP327])])). % 85.47/85.52 thf(sP328,plain,sP328 <=> ((~(sP195)) => (~(((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP328])])). % 85.47/85.52 thf(sP329,plain,sP329 <=> (![X1:$i]:((~(((~(sP326)) => (~(sP108))))) => (~(((r @ eigen__1) @ X1))))),introduced(definition,[new_symbols(definition,[sP329])])). % 85.47/85.52 thf(sP330,plain,sP330 <=> (sP263 => (~(sP172))),introduced(definition,[new_symbols(definition,[sP330])])). % 85.47/85.52 thf(sP331,plain,sP331 <=> ((~(sP198)) => sP201),introduced(definition,[new_symbols(definition,[sP331])])). % 85.47/85.52 thf(sP332,plain,sP332 <=> ((~(sP34)) => (~(sP7))),introduced(definition,[new_symbols(definition,[sP332])])). % 85.47/85.52 thf(sP333,plain,sP333 <=> (![X1:$i]:((~(sP77)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP333])])). % 85.47/85.52 thf(sP334,plain,sP334 <=> ((~(sP45)) => (~(sP327))),introduced(definition,[new_symbols(definition,[sP334])])). % 85.47/85.52 thf(sP335,plain,sP335 <=> (![X1:$i]:((~(sP82)) => (~(((r @ (eigen__0 @ eigen__1)) @ X1))))),introduced(definition,[new_symbols(definition,[sP335])])). % 85.47/85.52 thf(sP336,plain,sP336 <=> ((~(((~(((eigen__0 @ (eigen__0 @ eigen__1)) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))) => sP230))) => ((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP336])])). % 85.47/85.52 thf(sP337,plain,sP337 <=> ((~(((~(sP324)) => sP39))) => sP150),introduced(definition,[new_symbols(definition,[sP337])])). % 85.47/85.52 thf(sP338,plain,sP338 <=> ((~(sP148)) => (~(((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP338])])). % 85.47/85.52 thf(sP339,plain,sP339 <=> (((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ eigen__1))) => (~(sP224))),introduced(definition,[new_symbols(definition,[sP339])])). % 85.47/85.52 thf(sP340,plain,sP340 <=> (sP204 => (~(sP84))),introduced(definition,[new_symbols(definition,[sP340])])). % 85.47/85.52 thf(sP341,plain,sP341 <=> (sP27 => (~(sP169))),introduced(definition,[new_symbols(definition,[sP341])])). % 85.47/85.52 thf(sP342,plain,sP342 <=> (sP40 => sP15),introduced(definition,[new_symbols(definition,[sP342])])). % 85.47/85.52 thf(sP343,plain,sP343 <=> ((~(sP21)) => (~(sP25))),introduced(definition,[new_symbols(definition,[sP343])])). % 85.47/85.52 thf(sP344,plain,sP344 <=> (sP245 => (~(sP302))),introduced(definition,[new_symbols(definition,[sP344])])). % 85.47/85.52 thf(sP345,plain,sP345 <=> (sP121 => (~(sP312))),introduced(definition,[new_symbols(definition,[sP345])])). % 85.47/85.52 thf(sP346,plain,sP346 <=> ((~(((~(sP321)) => sP189))) => ((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP346])])). % 85.47/85.52 thf(sP347,plain,sP347 <=> ((~((sP7 => (~(sP25))))) => (~(sP208))),introduced(definition,[new_symbols(definition,[sP347])])). % 85.47/85.52 thf(sP348,plain,sP348 <=> ((~(sP142)) => (~(sP126))),introduced(definition,[new_symbols(definition,[sP348])])). % 85.47/85.52 thf(sP349,plain,sP349 <=> (![X1:$i]:((~((sP75 => (~(((b @ eigen__1) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP349])])). % 85.47/85.52 thf(sP350,plain,sP350 <=> ((~(sP233)) => (~(sP75))),introduced(definition,[new_symbols(definition,[sP350])])). % 85.47/85.52 thf(sP351,plain,sP351 <=> ((~(sP85)) => (~(sP224))),introduced(definition,[new_symbols(definition,[sP351])])). % 85.47/85.52 thf(sP352,plain,sP352 <=> ((~(sP321)) => sP189),introduced(definition,[new_symbols(definition,[sP352])])). % 85.47/85.52 thf(sP353,plain,sP353 <=> ((eigen__0 @ (eigen__0 @ eigen__1)) = eigen__1),introduced(definition,[new_symbols(definition,[sP353])])). % 85.47/85.52 thf(sP354,plain,sP354 <=> (![X1:$i]:((~((sP25 => (~(((b @ (eigen__0 @ eigen__1)) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1))))),introduced(definition,[new_symbols(definition,[sP354])])). % 85.47/85.52 thf(sP355,plain,sP355 <=> ((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP355])])). % 85.47/85.52 thf(sP356,plain,sP356 <=> (![X1:$i]:((~(((~(((eigen__0 @ eigen__1) = X1))) => ((r @ (eigen__0 @ eigen__1)) @ X1)))) => ((b @ (eigen__0 @ eigen__1)) @ X1))),introduced(definition,[new_symbols(definition,[sP356])])). % 85.47/85.52 thf(sP357,plain,sP357 <=> ((~(sP106)) => (~(sP8))),introduced(definition,[new_symbols(definition,[sP357])])). % 85.47/85.52 thf(sP358,plain,sP358 <=> (((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1)) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP358])])). % 85.47/85.52 thf(sP359,plain,sP359 <=> ((~(sP78)) => sP121),introduced(definition,[new_symbols(definition,[sP359])])). % 85.47/85.52 thf(sP360,plain,sP360 <=> ((eigen__0 @ (eigen__0 @ eigen__1)) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP360])])). % 85.47/85.52 thf(sP361,plain,sP361 <=> (![X1:$i]:((~(sP257)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP361])])). % 85.47/85.52 thf(sP362,plain,sP362 <=> ((~(sP153)) => sP8),introduced(definition,[new_symbols(definition,[sP362])])). % 85.47/85.52 thf(sP363,plain,sP363 <=> ((~(sP64)) => (~(sP19))),introduced(definition,[new_symbols(definition,[sP363])])). % 85.47/85.52 thf(sP364,plain,sP364 <=> ((~(sP345)) => (~(sP27))),introduced(definition,[new_symbols(definition,[sP364])])). % 85.47/85.52 thf(sP365,plain,sP365 <=> (sP312 => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP365])])). % 85.47/85.52 thf(sP366,plain,sP366 <=> ((~(((~(sP144)) => sP87))) => sP93),introduced(definition,[new_symbols(definition,[sP366])])). % 85.47/85.52 thf(sP367,plain,sP367 <=> ((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP367])])). % 85.47/85.52 thf(sP368,plain,sP368 <=> (sP95 => sP198),introduced(definition,[new_symbols(definition,[sP368])])). % 85.47/85.52 thf(sP369,plain,sP369 <=> ((~(sP282)) => sP161),introduced(definition,[new_symbols(definition,[sP369])])). % 85.47/85.52 thf(sP370,plain,sP370 <=> ((~(((~(((eigen__0 @ (eigen__0 @ eigen__1)) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))))) => sP134))) => sP295),introduced(definition,[new_symbols(definition,[sP370])])). % 85.47/85.52 thf(sP371,plain,sP371 <=> ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ eigen__1),introduced(definition,[new_symbols(definition,[sP371])])). % 85.47/85.52 thf(sP372,plain,sP372 <=> (sP278 => (~(sP75))),introduced(definition,[new_symbols(definition,[sP372])])). % 85.47/85.52 thf(sP373,plain,sP373 <=> (((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) = (eigen__0 @ (eigen__0 @ eigen__1))) => sP324),introduced(definition,[new_symbols(definition,[sP373])])). % 85.47/85.52 thf(sP374,plain,sP374 <=> ((~(sP326)) => (~(sP108))),introduced(definition,[new_symbols(definition,[sP374])])). % 85.47/85.52 thf(sP375,plain,sP375 <=> (sP141 => (~(sP263))),introduced(definition,[new_symbols(definition,[sP375])])). % 85.47/85.52 thf(sP376,plain,sP376 <=> ((~(sP331)) => ((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP376])])). % 85.47/85.52 thf(sP377,plain,sP377 <=> ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP377])])). % 85.47/85.52 thf(sP378,plain,sP378 <=> (![X1:$i]:(![X2:$i]:((~(((~((sP141 => (~(((r @ (eigen__0 @ eigen__1)) @ X1)))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP378])])). % 85.47/85.52 thf(sP379,plain,sP379 <=> ((eigen__0 @ (eigen__0 @ eigen__1)) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP379])])). % 85.47/85.52 thf(sP380,plain,sP380 <=> (![X1:$i]:((~(((~(sP344)) => (~(sP39))))) => (~(((r @ (eigen__0 @ eigen__1)) @ X1))))),introduced(definition,[new_symbols(definition,[sP380])])). % 85.47/85.52 thf(sP381,plain,sP381 <=> ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP381])])). % 85.47/85.52 thf(sP382,plain,sP382 <=> (sP150 => (~(sP377))),introduced(definition,[new_symbols(definition,[sP382])])). % 85.47/85.52 thf(sP383,plain,sP383 <=> ((~(sP357)) => (~(sP230))),introduced(definition,[new_symbols(definition,[sP383])])). % 85.47/85.52 thf(sP384,plain,sP384 <=> ((~(sP340)) => (~(sP284))),introduced(definition,[new_symbols(definition,[sP384])])). % 85.47/85.52 thf(sP385,plain,sP385 <=> (sP204 => (~(sP381))),introduced(definition,[new_symbols(definition,[sP385])])). % 85.47/85.52 thf(sP386,plain,sP386 <=> (eigen__1 = (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP386])])). % 85.47/85.52 thf(sP387,plain,sP387 <=> ((~(sP379)) => sP134),introduced(definition,[new_symbols(definition,[sP387])])). % 85.47/85.52 thf(sP388,plain,sP388 <=> ((~(sP170)) => (~(sP302))),introduced(definition,[new_symbols(definition,[sP388])])). % 85.47/85.52 thf(sP389,plain,sP389 <=> (sP7 => (~(sP25))),introduced(definition,[new_symbols(definition,[sP389])])). % 85.47/85.52 thf(sP390,plain,sP390 <=> ((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP390])])). % 85.47/85.52 thf(sP391,plain,sP391 <=> (![X1:$i]:((~(((~(((eigen__0 @ (eigen__0 @ eigen__1)) = X1))) => ((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1)))) => ((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1))),introduced(definition,[new_symbols(definition,[sP391])])). % 85.47/85.52 thf(sP392,plain,sP392 <=> (![X1:$i]:((~(sP170)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1))))),introduced(definition,[new_symbols(definition,[sP392])])). % 85.47/85.52 thf(sP393,plain,sP393 <=> (![X1:$i]:((~((sP306 => (~(((b @ (eigen__0 @ eigen__1)) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP393])])). % 85.47/85.52 thf(sP394,plain,sP394 <=> (sP108 => (~(sP245))),introduced(definition,[new_symbols(definition,[sP394])])). % 85.47/85.52 thf(sP395,plain,sP395 <=> (sP198 => sP269),introduced(definition,[new_symbols(definition,[sP395])])). % 85.47/85.52 thf(sP396,plain,sP396 <=> (![X1:$i]:((~((sP93 => (~(((b @ (eigen__0 @ eigen__1)) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP396])])). % 85.47/85.52 thf(sP397,plain,sP397 <=> ((~(sP140)) => (~(sP367))),introduced(definition,[new_symbols(definition,[sP397])])). % 85.47/85.52 thf(sP398,plain,sP398 <=> ((~(sP257)) => (~(sP178))),introduced(definition,[new_symbols(definition,[sP398])])). % 85.47/85.52 thf(sP399,plain,sP399 <=> (![X1:$i]:((~(((~(((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = X1))) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1)))) => ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1))),introduced(definition,[new_symbols(definition,[sP399])])). % 85.47/85.52 thf(sP400,plain,sP400 <=> (![X1:$i]:(![X2:$i]:((~(((~((sP172 => (~(((r @ (eigen__0 @ eigen__1)) @ X1)))))) => (~(((r @ eigen__1) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP400])])). % 85.47/85.52 thf(sP401,plain,sP401 <=> ((~(sP144)) => sP87),introduced(definition,[new_symbols(definition,[sP401])])). % 85.47/85.52 thf(sP402,plain,sP402 <=> ((~(sP91)) => sP19),introduced(definition,[new_symbols(definition,[sP402])])). % 85.47/85.52 thf(sP403,plain,sP403 <=> ((~(sP277)) => sP27),introduced(definition,[new_symbols(definition,[sP403])])). % 85.47/85.52 thf(sP404,plain,sP404 <=> (![X1:$i]:(![X2:$i]:((~((((b @ (eigen__0 @ eigen__1)) @ X1) => (~(((b @ (eigen__0 @ eigen__1)) @ X2)))))) => (~(((b @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP404])])). % 85.47/85.52 thf(sP405,plain,sP405 <=> (![X1:$i]:((~(sP167)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP405])])). % 85.47/85.52 thf(sP406,plain,sP406 <=> ((~(sP9)) => (~(sP270))),introduced(definition,[new_symbols(definition,[sP406])])). % 85.47/85.52 thf(sP407,plain,sP407 <=> (sP136 => sP269),introduced(definition,[new_symbols(definition,[sP407])])). % 85.47/85.52 thf(sP408,plain,sP408 <=> ((~(sP62)) => sP141),introduced(definition,[new_symbols(definition,[sP408])])). % 85.47/85.52 thf(sP409,plain,sP409 <=> (![X1:$i]:(![X2:$i]:((~(((~((X1 = X2))) => ((r @ X1) @ X2)))) => ((b @ X1) @ X2)))),introduced(definition,[new_symbols(definition,[sP409])])). % 85.47/85.52 thf(sP410,plain,sP410 <=> ((~(sP374)) => (~(sP367))),introduced(definition,[new_symbols(definition,[sP410])])). % 85.47/85.52 thf(sP411,plain,sP411 <=> (sP230 => (~(sP189))),introduced(definition,[new_symbols(definition,[sP411])])). % 85.47/85.52 thf(sP412,plain,sP412 <=> ((~(sP77)) => (~(sP178))),introduced(definition,[new_symbols(definition,[sP412])])). % 85.47/85.52 thf(sP413,plain,sP413 <=> (eigen__1 = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))),introduced(definition,[new_symbols(definition,[sP413])])). % 85.47/85.52 thf(sP414,plain,sP414 <=> (![X1:$i]:((~((sP84 => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP414])])). % 85.47/85.52 thf(sP415,plain,sP415 <=> (sP172 => (~(sP141))),introduced(definition,[new_symbols(definition,[sP415])])). % 85.47/85.52 thf(sP416,plain,sP416 <=> ((~(((~((sP224 => (~(sP367))))) => (~(sP263))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP416])])). % 85.47/85.52 thf(sP417,plain,sP417 <=> (sP141 => (~(sP87))),introduced(definition,[new_symbols(definition,[sP417])])). % 85.47/85.52 thf(sP418,plain,sP418 <=> (sP264 => (~(sP298))),introduced(definition,[new_symbols(definition,[sP418])])). % 85.47/85.52 thf(sP419,plain,sP419 <=> ((~(sP360)) => sP230),introduced(definition,[new_symbols(definition,[sP419])])). % 85.47/85.52 thf(sP420,plain,sP420 <=> ((~(sP274)) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))),introduced(definition,[new_symbols(definition,[sP420])])). % 85.47/85.52 thf(sP421,plain,sP421 <=> (sP263 => (~(sP87))),introduced(definition,[new_symbols(definition,[sP421])])). % 85.47/85.52 thf(sP422,plain,sP422 <=> (![X1:$i]:(~(((eigen__0 @ X1) = eigen__1)))),introduced(definition,[new_symbols(definition,[sP422])])). % 85.47/85.52 thf(sP423,plain,sP423 <=> (![X1:$i]:((~((sP169 => (~(((b @ eigen__1) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP423])])). % 85.47/85.52 thf(sP424,plain,sP424 <=> ((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1),introduced(definition,[new_symbols(definition,[sP424])])). % 85.47/85.52 thf(sP425,plain,sP425 <=> (![X1:$i]:(![X2:$i]:((~(((~((sP201 => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1)))))) => (~(((r @ (eigen__0 @ eigen__1)) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP425])])). % 85.47/85.52 thf(sP426,plain,sP426 <=> (![X1:$i]:((~((sP355 => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1))))),introduced(definition,[new_symbols(definition,[sP426])])). % 85.47/85.52 thf(sP427,plain,sP427 <=> ((~(sP324)) => sP39),introduced(definition,[new_symbols(definition,[sP427])])). % 85.47/85.52 thf(sP428,plain,sP428 <=> (((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP428])])). % 85.47/85.52 thf(sP429,plain,sP429 <=> ((~(sP304)) => (~(sP93))),introduced(definition,[new_symbols(definition,[sP429])])). % 85.47/85.52 thf(sP430,plain,sP430 <=> ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP430])])). % 85.47/85.52 thf(sP431,plain,sP431 <=> (sP413 => sP15),introduced(definition,[new_symbols(definition,[sP431])])). % 85.47/85.52 thf(sP432,plain,sP432 <=> (sP298 => (~(sP371))),introduced(definition,[new_symbols(definition,[sP432])])). % 85.47/85.52 thf(sP433,plain,sP433 <=> ((eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))) = (eigen__0 @ eigen__1)),introduced(definition,[new_symbols(definition,[sP433])])). % 85.47/85.52 thf(sP434,plain,sP434 <=> ((~(((~(sP101)) => (~(sP430))))) => (~(sP19))),introduced(definition,[new_symbols(definition,[sP434])])). % 85.47/85.52 thf(sP435,plain,sP435 <=> ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP435])])). % 85.47/85.52 thf(sP436,plain,sP436 <=> (![X1:$i]:((~(((~((eigen__1 = X1))) => ((r @ eigen__1) @ X1)))) => ((b @ eigen__1) @ X1))),introduced(definition,[new_symbols(definition,[sP436])])). % 85.47/85.52 thf(sP437,plain,sP437 <=> ((~(sP82)) => (~(sP172))),introduced(definition,[new_symbols(definition,[sP437])])). % 85.47/85.52 thf(sP438,plain,sP438 <=> (![X1:$i]:(![X2:$i]:((~(((~((((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ eigen__1))) => (~(((r @ eigen__1) @ X1)))))) => (~(((r @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP438])])). % 85.47/85.52 thf(sP439,plain,sP439 <=> (![X1:$i]:((~(((~(((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) = X1))) => ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1)))) => ((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1))),introduced(definition,[new_symbols(definition,[sP439])])). % 85.47/85.52 thf(sP440,plain,sP440 <=> (![X1:$i]:((~((sP161 => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) @ X1)))))) => (~(((b @ eigen__1) @ X1))))),introduced(definition,[new_symbols(definition,[sP440])])). % 85.47/85.52 thf(sP441,plain,sP441 <=> (sP108 => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))))))),introduced(definition,[new_symbols(definition,[sP441])])). % 85.47/85.52 thf(sP442,plain,sP442 <=> ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP442])])). % 85.47/85.52 thf(sP443,plain,sP443 <=> (![X1:$i]:((~((((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1))))),introduced(definition,[new_symbols(definition,[sP443])])). % 85.47/85.52 thf(sP444,plain,sP444 <=> ((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP444])])). % 85.47/85.52 thf(sP445,plain,sP445 <=> ((~((sP230 => (~(sP201))))) => (~(sP39))),introduced(definition,[new_symbols(definition,[sP445])])). % 85.47/85.52 thf(sP446,plain,sP446 <=> (sP253 => sP136),introduced(definition,[new_symbols(definition,[sP446])])). % 85.47/85.52 thf(sP447,plain,sP447 <=> (sP25 => (~(sP7))),introduced(definition,[new_symbols(definition,[sP447])])). % 85.47/85.52 thf(sP448,plain,sP448 <=> ((~(sP217)) => (~(sP355))),introduced(definition,[new_symbols(definition,[sP448])])). % 85.47/85.52 thf(sP449,plain,sP449 <=> ((~((sP161 => (~(sP377))))) => (~(sP208))),introduced(definition,[new_symbols(definition,[sP449])])). % 85.47/85.52 thf(sP450,plain,sP450 <=> (sP230 => (~(sP201))),introduced(definition,[new_symbols(definition,[sP450])])). % 85.47/85.52 thf(sP451,plain,sP451 <=> ((~(sP16)) => (~(sP204))),introduced(definition,[new_symbols(definition,[sP451])])). % 85.47/85.52 thf(sP452,plain,sP452 <=> ((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))),introduced(definition,[new_symbols(definition,[sP452])])). % 85.47/85.52 thf(sP453,plain,sP453 <=> (sP302 => (~(sP245))),introduced(definition,[new_symbols(definition,[sP453])])). % 85.47/85.52 thf(sP454,plain,sP454 <=> (![X1:$i]:((~(sP130)) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1))))),introduced(definition,[new_symbols(definition,[sP454])])). % 85.47/85.52 thf(sP455,plain,sP455 <=> (sP103 => sP265),introduced(definition,[new_symbols(definition,[sP455])])). % 85.47/85.52 thf(sP456,plain,sP456 <=> (![X1:$i]:((eigen__1 = X1) => (X1 = eigen__1))),introduced(definition,[new_symbols(definition,[sP456])])). % 85.47/85.52 thf(sP457,plain,sP457 <=> ((~(((~(sP344)) => (~(sP39))))) => (~(sP172))),introduced(definition,[new_symbols(definition,[sP457])])). % 85.47/85.52 thf(sP458,plain,sP458 <=> ((~(sP253)) => sP160),introduced(definition,[new_symbols(definition,[sP458])])). % 85.47/85.52 thf(sP459,plain,sP459 <=> ((r @ eigen__1) @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP459])])). % 85.47/85.52 thf(sP460,plain,sP460 <=> ((~(sP413)) => sP367),introduced(definition,[new_symbols(definition,[sP460])])). % 85.47/85.52 thf(sP461,plain,sP461 <=> ((~(sP262)) => (~(sP19))),introduced(definition,[new_symbols(definition,[sP461])])). % 85.47/85.52 thf(sP462,plain,sP462 <=> ((~(sP344)) => (~(sP39))),introduced(definition,[new_symbols(definition,[sP462])])). % 85.47/85.52 thf(sP463,plain,sP463 <=> (sP161 => (~(sP377))),introduced(definition,[new_symbols(definition,[sP463])])). % 85.47/85.52 thf(sP464,plain,sP464 <=> (sP224 => (~(sP367))),introduced(definition,[new_symbols(definition,[sP464])])). % 85.47/85.52 thf(sP465,plain,sP465 <=> ((~(sP132)) => (~(sP377))),introduced(definition,[new_symbols(definition,[sP465])])). % 85.47/85.52 thf(sP466,plain,sP466 <=> ((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ eigen__1),introduced(definition,[new_symbols(definition,[sP466])])). % 85.47/85.52 thf(sP467,plain,sP467 <=> ((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP467])])). % 85.47/85.52 thf(sP468,plain,sP468 <=> (![X1:$i]:(![X2:$i]:((~(((~((sP307 => (~(((r @ eigen__1) @ X1)))))) => (~(((r @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1)))))) => (~(((r @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP468])])). % 85.47/85.52 thf(sP469,plain,sP469 <=> (![X1:$i]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((~(((~((((r @ X1) @ X2) => (~(((r @ X1) @ X3)))))) => (~(((r @ X2) @ X3)))))) => (~(((r @ X3) @ X4)))))))),introduced(definition,[new_symbols(definition,[sP469])])). % 85.47/85.52 thf(sP470,plain,sP470 <=> (sP2 => sP91),introduced(definition,[new_symbols(definition,[sP470])])). % 85.47/85.52 thf(sP471,plain,sP471 <=> ((~(sP101)) => (~(sP430))),introduced(definition,[new_symbols(definition,[sP471])])). % 85.47/85.52 thf(sP472,plain,sP472 <=> ((~(sP353)) => sP424),introduced(definition,[new_symbols(definition,[sP472])])). % 85.47/85.52 thf(sP473,plain,sP473 <=> (![X1:$i]:((~(sP268)) => (~(((r @ (eigen__0 @ eigen__1)) @ X1))))),introduced(definition,[new_symbols(definition,[sP473])])). % 85.47/85.52 thf(sP474,plain,sP474 <=> ((~(sP100)) => (~(sP178))),introduced(definition,[new_symbols(definition,[sP474])])). % 85.47/85.52 thf(sP475,plain,sP475 <=> ((~(sP453)) => (~(sP263))),introduced(definition,[new_symbols(definition,[sP475])])). % 85.47/85.52 thf(sP476,plain,sP476 <=> ((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1))))) = (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP476])])). % 85.47/85.52 thf(sP477,plain,sP477 <=> (![X1:$i]:((~((sP278 => (~(((b @ eigen__1) @ X1)))))) => (~(((b @ (eigen__0 @ eigen__1)) @ X1))))),introduced(definition,[new_symbols(definition,[sP477])])). % 85.47/85.52 thf(sP478,plain,sP478 <=> ((b @ (eigen__0 @ eigen__1)) @ (eigen__0 @ (eigen__0 @ eigen__1))),introduced(definition,[new_symbols(definition,[sP478])])). % 85.47/85.52 thf(sP479,plain,sP479 <=> (sP7 => (~(sP306))),introduced(definition,[new_symbols(definition,[sP479])])). % 85.47/85.52 thf(sP480,plain,sP480 <=> ((eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) = (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))))),introduced(definition,[new_symbols(definition,[sP480])])). % 85.47/85.52 thf(sP481,plain,sP481 <=> (![X1:$i]:(((eigen__0 @ (eigen__0 @ eigen__1)) = (eigen__0 @ X1)) => ((eigen__0 @ eigen__1) = X1))),introduced(definition,[new_symbols(definition,[sP481])])). % 85.47/85.52 thf(sP482,plain,sP482 <=> (![X1:$i]:((~(sP193)) => (~(((r @ eigen__1) @ X1))))),introduced(definition,[new_symbols(definition,[sP482])])). % 85.47/85.52 thf(sP483,plain,sP483 <=> ((~(sP428)) => (~(sP121))),introduced(definition,[new_symbols(definition,[sP483])])). % 85.47/85.52 thf(sP484,plain,sP484 <=> ((~(sP83)) => (~(sP435))),introduced(definition,[new_symbols(definition,[sP484])])). % 85.47/85.52 thf(sP485,plain,sP485 <=> ((~(sP464)) => (~(sP263))),introduced(definition,[new_symbols(definition,[sP485])])). % 85.47/85.52 thf(sP486,plain,sP486 <=> (![X1:$i]:((~((sP312 => (~(((b @ (eigen__0 @ (eigen__0 @ (eigen__0 @ eigen__1)))) @ X1)))))) => (~(((b @ (eigen__0 @ (eigen__0 @ eigen__1))) @ X1))))),introduced(definition,[new_symbols(definition,[sP486])])). % 85.47/85.52 thf(def_inj,definition,(inj = (^[X1:$i>$i]:(![X2:$i]:(![X3:$i]:(((X1 @ X2) = (X1 @ X3)) => (X2 = X3))))))). % 85.47/85.52 thf(def_surj,definition,(surj = (^[X1:$i>$i]:(![X2:$i]:(~((![X3:$i]:(~(((X1 @ X3) = X2)))))))))). % 85.47/85.52 thf(h0,assumption,(~((sP1 => (![X1:$i]:(~((![X2:$i]:(~(((eigen__0 @ X2) = X1)))))))))),introduced(assumption,[])). % 85.47/85.52 thf(h1,assumption,sP1,introduced(assumption,[])). % 85.47/85.52 thf(h2,assumption,(~((![X1:$i]:(~((![X2:$i]:(~(((eigen__0 @ X2) = X1))))))))),introduced(assumption,[])). % 85.47/85.52 thf(h3,assumption,sP422,introduced(assumption,[])). % 85.47/85.52 thf(1,plain,((~(sP432) | ~(sP298)) | ~(sP371)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(2,plain,((~(sP195) | ~(sP298)) | ~(sP135)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(3,plain,((~(sP418) | ~(sP264)) | ~(sP298)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(4,plain,((~(sP123) | ~(sP264)) | ~(sP371)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(5,plain,((~(sP251) | ~(sP264)) | ~(sP135)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(6,plain,((~(sP117) | ~(sP172)) | ~(sP87)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(7,plain,((~(sP80) | ~(sP201)) | ~(sP134)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(8,plain,((~(sP148) | ~(sP424)) | ~(sP134)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(9,plain,((~(sP344) | ~(sP245)) | ~(sP302)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(10,plain,((~(sP106) | ~(sP245)) | ~(sP467)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(11,plain,((~(sP450) | ~(sP230)) | ~(sP201)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(12,plain,((~(sP411) | ~(sP230)) | ~(sP189)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(13,plain,((~(sP26) | ~(sP230)) | ~(sP134)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(14,plain,((~(sP330) | ~(sP263)) | ~(sP172)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(15,plain,((~(sP316) | ~(sP263)) | ~(sP141)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(16,plain,((~(sP421) | ~(sP263)) | ~(sP87)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(17,plain,((~(sP325) | sP251) | ~(sP327)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(18,plain,((~(sP102) | sP123) | ~(sP161)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(19,plain,((~(sP249) | sP418) | ~(sP150)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(20,plain,((~(sP328) | sP195) | ~(sP478)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(21,plain,((~(sP54) | sP432) | ~(sP7)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(22,plain,((~(sP225) | ~(sP302)) | ~(sP442)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(23,plain,((~(sP441) | ~(sP108)) | ~(sP442)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(24,plain,((~(sP305) | ~(sP467)) | ~(sP442)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(25,plain,((~(sP417) | ~(sP141)) | ~(sP87)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(26,plain,((~(sP101) | ~(sP367)) | ~(sP459)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(27,plain,((~(sP246) | ~(sP307)) | ~(sP459)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(28,plain,((~(sP339) | ~(sP444)) | ~(sP224)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(29,plain,((~(sP464) | ~(sP224)) | ~(sP367)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(30,plain,((~(sP285) | ~(sP367)) | ~(sP224)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(31,plain,((~(sP338) | sP148) | ~(sP459)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(32,plain,((~(sP257) | sP80) | ~(sP87)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(33,plain,((~(sP31) | ~(sP295)) | ~(sP466)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(34,plain,((~(sP194) | sP117) | ~(sP459)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(35,plain,((~(sP155) | ~(sP93)) | ~(sP306)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(36,plain,((~(sP197) | ~(sP93)) | ~(sP7)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(37,plain,((~(sP294) | sP188) | sP270),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(38,plain,((~(sP276) | sP40) | sP178),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(39,plain,((~(sP402) | sP91) | sP19),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(40,plain,((~(sP43) | sP476) | sP260),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(41,plain,((~(sP163) | ~(sP377)) | ~(sP284)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(42,plain,((~(sP205) | ~(sP327)) | ~(sP377)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(43,plain,((~(sP463) | ~(sP161)) | ~(sP377)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(44,plain,((~(sP382) | ~(sP150)) | ~(sP377)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(45,plain,((~(sP111) | sP421) | ~(sP430)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(46,plain,((~(sP170) | sP316) | ~(sP435)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(47,plain,((~(sP85) | sP330) | ~(sP126)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(48,plain,((~(sP9) | sP26) | ~(sP430)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(49,plain,((~(sP47) | sP411) | ~(sP435)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(50,plain,((~(sP445) | sP450) | ~(sP39)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(51,plain,((~(sP357) | sP106) | ~(sP8)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(52,plain,((~(sP462) | sP344) | ~(sP39)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(53,plain,((~(sP138) | ~(sP160)) | ~(sP172)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(54,plain,((~(sP203) | ~(sP160)) | ~(sP141)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(55,plain,((~(sP143) | ~(sP189)) | ~(sP201)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(56,plain,((~(sP375) | ~(sP141)) | ~(sP263)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(57,plain,((~(sP326) | ~(sP141)) | ~(sP172)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(58,plain,((~(sP140) | ~(sP172)) | ~(sP263)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(59,plain,((~(sP107) | ~(sP201)) | ~(sP230)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(60,plain,((~(sP453) | ~(sP302)) | ~(sP245)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(61,plain,((~(sP394) | ~(sP108)) | ~(sP245)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(62,plain,((~(sP175) | ~(sP108)) | ~(sP302)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(63,plain,((~(sP38) | sP382) | ~(sP25)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(64,plain,((~(sP449) | sP463) | ~(sP208)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(65,plain,((~(sP279) | sP205) | ~(sP452)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(66,plain,((~(sP122) | sP163) | ~(sP84)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(67,plain,(~(sP48) | sP54),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(68,plain,(~(sP48) | sP328),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(69,plain,(~(sP18) | sP249),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(70,plain,(~(sP18) | sP102),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(71,plain,(~(sP18) | sP325),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(72,plain,((~(sP116) | sP43) | sP135),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(73,plain,((~(sP90) | sP402) | sP371),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(74,plain,((~(sP71) | sP276) | sP298),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(75,plain,((~(sP115) | sP294) | sP264),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(76,plain,((~(sP6) | sP197) | ~(sP371)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(77,plain,((~(sP147) | sP155) | ~(sP264)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(78,plain,((~(sP76) | sP194) | ~(sP260)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(79,plain,((~(sP168) | sP194) | ~(sP19)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(80,plain,((~(sP248) | sP194) | ~(sP270)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(81,plain,((~(sP234) | sP31) | ~(sP371)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(82,plain,((~(sP187) | sP257) | ~(sP19)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(83,plain,((~(sP398) | sP257) | ~(sP178)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(84,plain,((~(sP53) | sP338) | ~(sP19)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(85,plain,((~(sP268) | sP285) | ~(sP39)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(86,plain,((~(sP485) | sP464) | ~(sP263)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(87,plain,((~(sP60) | sP339) | ~(sP201)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(88,plain,((~(sP100) | sP246) | ~(sP442)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(89,plain,((~(sP471) | sP101) | ~(sP430)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(90,plain,((~(sP315) | ~(sP169)) | ~(sP75)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(91,plain,((~(sP146) | ~(sP169)) | ~(sP278)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(92,plain,((~(sP262) | sP417) | ~(sP442)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(93,plain,((~(sP64) | sP305) | ~(sP134)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(94,plain,((~(sP167) | sP441) | ~(sP459)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(95,plain,((~(sP77) | sP225) | ~(sP87)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(96,plain,((~(sP92) | ~(sP84)) | ~(sP204)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(97,plain,((~(sP59) | ~(sP84)) | ~(sP121)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(98,plain,((~(sP457) | sP462) | ~(sP172)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(99,plain,((~(sP383) | sP357) | ~(sP230)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(100,plain,((~(sP232) | sP445) | ~(sP87)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(101,plain,((~(sP164) | sP47) | ~(sP245)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(102,plain,((~(sP406) | sP9) | ~(sP270)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(103,plain,((~(sP214) | sP85) | ~(sP459)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(104,plain,((~(sP351) | sP85) | ~(sP224)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(105,plain,((~(sP388) | sP170) | ~(sP302)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(106,plain,((~(sP229) | sP111) | ~(sP19)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(107,plain,((~(sP37) | sP111) | ~(sP178)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(108,plain,((~(sP67) | sP111) | ~(sP270)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(109,plain,((~(sP132) | ~(sP306)) | ~(sP25)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(110,plain,((~(sP207) | ~(sP306)) | ~(sP93)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(111,plain,((~(sP427) | sP324) | sP39),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(112,plain,((~(sP282) | sP15) | sP126),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(113,plain,((~(sP362) | sP153) | sP8),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(114,plain,((~(sP139) | sP186) | sP435),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(115,plain,((~(sP17) | sP480) | sP430),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(116,plain,((~(sP374) | sP326) | ~(sP108)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(117,plain,((~(sP83) | sP375) | ~(sP245)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(118,plain,((~(sP223) | sP143) | ~(sP302)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(119,plain,((~(sP272) | sP203) | ~(sP189)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(120,plain,((~(sP193) | sP138) | ~(sP424)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(121,plain,((~(sP14) | ~(sP7)) | ~(sP93)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(122,plain,((~(sP401) | sP144) | sP87),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(123,plain,((~(sP128) | ~(sP390)) | ~(sP295)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(124,plain,((~(sP293) | sP175) | ~(sP224)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(125,plain,((~(sP142) | sP394) | ~(sP367)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(126,plain,((~(sP475) | sP453) | ~(sP263)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(127,plain,((~(sP385) | ~(sP204)) | ~(sP381)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(128,plain,((~(sP340) | ~(sP204)) | ~(sP84)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(129,plain,((~(sP24) | sP107) | ~(sP263)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(130,plain,((~(sP297) | ~(sP355)) | ~(sP452)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(131,plain,((~(sP237) | ~(sP355)) | ~(sP295)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(132,plain,((~(sP397) | sP140) | ~(sP367)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(133,plain,((~(sP256) | ~(sP306)) | ~(sP7)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(134,plain,((~(sP154) | sP59) | ~(sP371)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(135,plain,((~(sP200) | sP92) | ~(sP264)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(136,plain,((~(sP412) | sP77) | ~(sP178)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(137,plain,((~(sP159) | sP167) | ~(sP19)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(138,plain,((~(sP363) | sP64) | ~(sP19)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(139,plain,((~(sP317) | sP64) | ~(sP270)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(140,plain,((~(sP461) | sP262) | ~(sP19)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(141,plain,((~(sP13) | sP262) | ~(sP178)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(142,plain,((~(sP228) | sP262) | ~(sP270)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(143,plain,((~(sP314) | sP146) | ~(sP298)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(144,plain,((~(sP157) | sP315) | ~(sP264)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(145,plain,((~(sP434) | sP471) | ~(sP19)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(146,plain,((~(sP98) | sP471) | ~(sP270)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(147,plain,((~(sP474) | sP100) | ~(sP178)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(148,plain,((~(sP199) | sP100) | ~(sP270)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(149,plain,((~(sP261) | sP60) | ~(sP172)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(150,plain,((~(sP416) | sP485) | ~(sP435)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(151,plain,((~(sP125) | sP268) | ~(sP172)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(152,plain,(~(sP227) | sP53),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(153,plain,(~(sP361) | sP398),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(154,plain,(~(sP361) | sP187),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(155,plain,((~(sP23) | sP128) | ~(sP93)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(156,plain,(~(sP218) | sP234),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(157,plain,((~(sP366) | sP401) | sP93),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(158,plain,(~(sP242) | sP248),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(159,plain,(~(sP242) | sP168),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(160,plain,(~(sP242) | sP76),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(161,plain,((~(sP171) | sP14) | ~(sP169)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(162,plain,(~(sP396) | sP147),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(163,plain,(~(sP396) | sP6),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(164,plain,(~(sP33) | sP115),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(165,plain,(~(sP33) | sP71),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(166,plain,(~(sP33) | sP90),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(167,plain,(~(sP33) | sP116),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(168,plain,(~(sP61) | sP18),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(169,plain,(~(sP61) | sP48),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(170,plain,((~(sP166) | sP193) | ~(sP367)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(171,plain,((~(sP318) | sP272) | ~(sP302)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(172,plain,((~(sP185) | sP223) | ~(sP87)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(173,plain,((~(sP74) | sP223) | ~(sP263)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(174,plain,((~(sP484) | sP83) | ~(sP435)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(175,plain,((~(sP308) | sP374) | ~(sP459)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(176,plain,((~(sP52) | sP374) | ~(sP224)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(177,plain,((~(sP410) | sP374) | ~(sP367)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(178,plain,(~(sP182) | sP122),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(179,plain,(~(sP105) | sP279),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(180,plain,(~(sP440) | sP449),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(181,plain,(~(sP58) | sP38),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(182,plain,((~(sP206) | sP17) | sP284),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(183,plain,((~(sP5) | sP139) | sP377),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(184,plain,((~(sP222) | sP362) | sP327),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(185,plain,((~(sP369) | sP282) | sP161),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(186,plain,((~(sP337) | sP427) | sP150),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(187,plain,((~(sP271) | ~(sP188)) | sP186),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(188,plain,((~(sP342) | ~(sP40)) | sP15),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(189,plain,((~(sP373) | ~(sP476)) | sP324),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(190,plain,((~(sP152) | sP207) | ~(sP284)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(191,plain,((~(sP465) | sP132) | ~(sP377)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(192,plain,((~(sP73) | sP256) | ~(sP161)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(193,plain,(~(sP241) | sP67),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(194,plain,(~(sP241) | sP37),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(195,plain,(~(sP241) | sP229),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(196,plain,(~(sP392) | sP388),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(197,plain,(~(sP183) | sP351),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(198,plain,(~(sP183) | sP214),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(199,plain,((~(sP112) | sP397) | ~(sP39)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(200,plain,((~(sP96) | sP237) | ~(sP284)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(201,plain,((~(sP174) | sP297) | ~(sP377)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(202,plain,(~(sP120) | sP406),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(203,plain,(~(sP289) | sP164),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(204,plain,(~(sP180) | sP232),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(205,plain,((~(sP173) | sP24) | ~(sP8)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(206,plain,((~(sP384) | sP340) | ~(sP284)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(207,plain,((~(sP3) | sP385) | ~(sP150)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(208,plain,(~(sP42) | sP383),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(209,plain,(~(sP380) | sP457),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(210,plain,((~(sP255) | sP475) | ~(sP435)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(211,plain,((~(sP104) | sP142) | ~(sP435)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(212,plain,((~(sP348) | sP142) | ~(sP126)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(213,plain,((~(sP49) | sP293) | ~(sP172)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(214,plain,((~(sP415) | ~(sP172)) | ~(sP141)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(215,plain,((~(sP124) | ~(sP424)) | ~(sP189)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(216,plain,((~(sP387) | sP379) | sP134),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(217,plain,((~(sP137) | ~(sP381)) | ~(sP84)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(218,plain,((~(sP119) | ~(sP121)) | ~(sP84)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(219,plain,((~(sP420) | sP274) | sP442),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(220,plain,((~(sP41) | ~(sP25)) | ~(sP93)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(221,plain,((~(sP36) | ~(sP452)) | ~(sP295)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(222,plain,((~(sP322) | sP2) | sP459),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(223,plain,((~(sP69) | ~(sP75)) | ~(sP169)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(224,plain,((~(sP304) | ~(sP278)) | ~(sP169)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(225,plain,((~(sP341) | ~(sP27)) | ~(sP169)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(226,plain,((~(sP213) | ~(sP208)) | ~(sP169)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(227,plain,((~(sP217) | ~(sP27)) | ~(sP75)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(228,plain,((~(sP372) | ~(sP278)) | ~(sP75)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(229,plain,((~(sP21) | ~(sP278)) | ~(sP208)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(230,plain,((~(sP343) | sP21) | ~(sP25)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(231,plain,((~(sP129) | sP372) | ~(sP306)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(232,plain,((~(sP448) | sP217) | ~(sP355)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(233,plain,(~(sP473) | sP125),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(234,plain,(~(sP149) | sP416),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(235,plain,(~(sP131) | sP261),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(236,plain,(~(sP267) | sP199),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(237,plain,(~(sP267) | sP474),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(238,plain,(~(sP79) | sP98),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(239,plain,(~(sP79) | sP434),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(240,plain,((~(sP296) | sP213) | ~(sP84)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(241,plain,((~(sP235) | sP341) | ~(sP295)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(242,plain,((~(sP429) | sP304) | ~(sP93)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(243,plain,((~(sP301) | sP69) | ~(sP284)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(244,plain,(~(sP423) | sP157),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(245,plain,(~(sP423) | sP314),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(246,plain,((~(sP250) | sP322) | sP169),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(247,plain,((~(sP275) | sP36) | ~(sP84)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(248,plain,(~(sP288) | sP228),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(249,plain,(~(sP288) | sP13),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(250,plain,(~(sP288) | sP461),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(251,plain,((~(sP22) | sP41) | ~(sP84)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(252,plain,((~(sP99) | sP420) | sP84),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(253,plain,(~(sP110) | sP317),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(254,plain,(~(sP110) | sP363),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(255,plain,(~(sP405) | sP159),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(256,plain,(~(sP333) | sP412),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(257,plain,((~(sP114) | sP119) | ~(sP169)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(258,plain,((~(sP118) | sP137) | ~(sP93)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(259,plain,(~(sP414) | sP200),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(260,plain,(~(sP414) | sP154),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(261,plain,((~(sP370) | sP387) | sP295),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(262,plain,((~(sP162) | sP124) | ~(sP307)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(263,plain,((~(sP428) | ~(sP452)) | ~(sP466)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(264,plain,((~(sP130) | sP415) | ~(sP307)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(265,plain,((~(sP16) | ~(sP25)) | ~(sP306)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(266,plain,((~(sP447) | ~(sP25)) | ~(sP7)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(267,plain,((~(sP479) | ~(sP7)) | ~(sP306)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(268,plain,((~(sP247) | sP103) | sP263),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(269,plain,((~(sP192) | ~(sP390)) | ~(sP355)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(270,plain,((~(sP419) | sP360) | sP230),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(271,plain,((~(sP63) | ~(sP381)) | ~(sP204)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(272,plain,((~(sP233) | ~(sP121)) | ~(sP204)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(273,plain,((~(sP113) | sP145) | sP245),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(274,plain,((~(sP283) | sP433) | sP302),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(275,plain,((~(sP78) | sP12) | sP108),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(276,plain,((~(sP221) | sP95) | sP467),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(277,plain,(~(sP240) | sP49),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(278,plain,((~(sP291) | sP221) | sP312),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(279,plain,((~(sP359) | sP78) | sP121),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(280,plain,((~(sP35) | sP283) | sP381),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(281,plain,((~(sP244) | ~(sP186)) | sP95),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(282,plain,((~(sP311) | ~(sP324)) | sP12),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(283,plain,((~(sP109) | ~(sP153)) | sP433),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(284,plain,((~(sP10) | ~(sP480)) | sP145),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(285,plain,((~(sP158) | sP113) | sP204),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(286,plain,(~(sP11) | sP348),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(287,plain,(~(sP11) | sP104),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(288,plain,(~(sP94) | sP255),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(289,plain,(~(sP176) | sP380),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(290,plain,(~(sP176) | sP42),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(291,plain,((~(sP350) | sP233) | ~(sP75)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(292,plain,((~(sP243) | sP63) | ~(sP306)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(293,plain,(~(sP156) | sP3),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(294,plain,(~(sP156) | sP384),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(295,plain,((~(sP238) | ~(sP274)) | sP360),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(296,plain,((~(sP336) | sP419) | sP355),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(297,plain,(~(sP286) | sP173),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(298,plain,(~(sP177) | sP180),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(299,plain,(~(sP177) | sP289),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(300,plain,(~(sP177) | sP120),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(301,plain,((~(sP220) | sP192) | ~(sP306)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(302,plain,(~(sP426) | sP174),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(303,plain,(~(sP426) | sP96),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(304,plain,((~(sP231) | ~(sP379)) | sP103),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(305,plain,((~(sP57) | sP247) | sP306),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(306,plain,(~(sP127) | sP112),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(307,plain,(~(sP290) | sP183),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(308,plain,(~(sP290) | sP392),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(309,plain,(~(sP290) | sP241),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(310,plain,((~(sP56) | sP479) | ~(sP75)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(311,plain,(~(sP393) | sP73),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(312,plain,(~(sP393) | sP465),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(313,plain,(~(sP393) | sP152),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(314,plain,((~(sP470) | ~(sP2)) | sP91),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(315,plain,(~(sP456) | sP470),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(316,plain,(~(sP81) | sP373),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(317,plain,(~(sP81) | sP342),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(318,plain,(~(sP81) | sP271),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(319,plain,(~(sP439) | sP337),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(320,plain,(~(sP439) | sP369),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(321,plain,(~(sP439) | sP222),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(322,plain,(~(sP439) | sP5),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(323,plain,(~(sP439) | sP206),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(324,plain,(~(sP259) | sP58),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(325,plain,(~(sP259) | sP440),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(326,plain,(~(sP259) | sP105),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(327,plain,(~(sP259) | sP182),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(328,plain,((~(sP254) | sP447) | ~(sP121)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(329,plain,((~(sP451) | sP16) | ~(sP204)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(330,plain,(~(sP329) | sP410),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(331,plain,(~(sP329) | sP52),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(332,plain,(~(sP329) | sP308),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(333,plain,(~(sP151) | sP484),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(334,plain,((~(sP266) | sP130) | ~(sP302)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(335,plain,((~(sP483) | sP428) | ~(sP121)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(336,plain,(~(sP216) | sP74),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(337,plain,(~(sP216) | sP185),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(338,plain,((~(sP210) | sP162) | ~(sP108)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(339,plain,(~(sP66) | sP318),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(340,plain,(~(sP482) | sP166),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(341,plain,((~(sP455) | ~(sP103)) | sP265),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(342,plain,((~(sP226) | ~(sP62)) | sP386),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(343,plain,((~(sP446) | ~(sP253)) | sP136),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(344,plain,(~(sP287) | sP61),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(345,plain,(~(sP409) | sP33),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(346,plain,(~(sP404) | sP396),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(347,plain,(~(sP303) | sP171),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(348,plain,(~(sP400) | sP242),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(349,plain,(~(sP356) | sP366),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(350,plain,(~(sP319) | sP218),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(351,plain,(~(sP30) | sP23),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(352,plain,(~(sP425) | sP361),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(353,plain,(~(sP70) | sP227),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(354,plain,(~(sP391) | sP370),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(355,plain,(~(sP273) | sP414),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(356,plain,(~(sP310) | sP118),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(357,plain,(~(sP55) | sP114),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(358,plain,(~(sP20) | sP333),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(359,plain,(~(sP300) | sP405),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(360,plain,(~(sP165) | sP110),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(361,plain,(~(sP399) | sP99),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(362,plain,(~(sP354) | sP22),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(363,plain,(~(sP378) | sP288),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(364,plain,(~(sP443) | sP275),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(365,plain,(~(sP436) | sP250),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(366,plain,(~(sP89) | sP423),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(367,plain,(~(sP349) | sP301),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(368,plain,(~(sP477) | sP429),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(369,plain,(~(sP68) | sP235),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(370,plain,(~(sP196) | sP296),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(371,plain,(~(sP236) | sP79),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(372,plain,(~(sP468) | sP267),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(373,plain,((~(sP292) | ~(sP144)) | sP413),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(374,plain,((~(sP215) | sP265) | sP307),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(375,plain,((~(sP86) | sP215) | sP208),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(376,plain,((~(sP277) | sP386) | sP444),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(377,plain,((~(sP403) | sP277) | sP27),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(378,plain,((~(sP309) | sP136) | sP224),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(379,plain,((~(sP32) | sP309) | sP278),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(380,plain,((~(sP460) | sP413) | sP367),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(381,plain,((~(sP202) | sP460) | sP75),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(382,plain,(~(sP438) | sP131),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(383,plain,(~(sP219) | sP149),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(384,plain,(~(sP236) | sP473),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(385,plain,(~(sP68) | sP448),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(386,plain,(~(sP477) | sP129),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(387,plain,(~(sP477) | sP343),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(388,plain,((~(sP45) | ~(sP75)) | ~(sP27)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(389,plain,((~(sP334) | sP45) | ~(sP327)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(390,plain,(~(sP349) | sP334),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(391,plain,(~(sP89) | sP349),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(392,plain,(~(sP89) | sP477),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(393,plain,(~(sP89) | sP68),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(394,plain,(~(sP89) | sP196),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(395,plain,(~(sP252) | sP236),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(396,plain,(~(sP252) | sP219),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(397,plain,(~(sP252) | sP438),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(398,plain,(~(sP252) | sP468),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(399,plain,(~(sP436) | sP202),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(400,plain,(~(sP436) | sP32),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(401,plain,(~(sP436) | sP403),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(402,plain,(~(sP436) | sP86),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(403,plain,(~(sP133) | sP292),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(404,plain,(~(sP133) | sP446),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(405,plain,(~(sP133) | sP226),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(406,plain,(~(sP133) | sP455),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(407,plain,((~(sP395) | ~(sP198)) | sP269),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(408,plain,((~(sP65) | ~(sP321)) | sP253),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(409,plain,((~(sP458) | sP253) | sP160),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(410,plain,((~(sP281) | sP458) | sP478),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(411,plain,(~(sP191) | sP482),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(412,plain,(~(sP191) | sP66),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(413,plain,((~(sP51) | ~(sP433)) | sP353),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(414,plain,((~(sP29) | ~(sP145)) | sP321),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(415,plain,((~(sP352) | sP321) | sP189),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(416,plain,((~(sP346) | sP352) | sP452),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(417,plain,(~(sP258) | sP210),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(418,plain,(~(sP320) | sP216),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(419,plain,((~(sP358) | ~(sP390)) | ~(sP452)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(420,plain,((~(sP299) | sP358) | ~(sP25)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(421,plain,(~(sP443) | sP483),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(422,plain,((~(sP190) | ~(sP360)) | sP62),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(423,plain,((~(sP408) | sP62) | sP141),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(424,plain,((~(sP50) | sP408) | sP25),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(425,plain,(~(sP454) | sP266),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(426,plain,(~(sP378) | sP151),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(427,plain,(~(sP378) | sP329),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(428,plain,((~(sP389) | ~(sP7)) | ~(sP25)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(429,plain,((~(sP347) | sP389) | ~(sP208)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(430,plain,(~(sP354) | sP451),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(431,plain,(~(sP354) | sP254),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(432,plain,(~(sP287) | sP259),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(433,plain,(~(sP409) | sP439),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(434,plain,(~(sP1) | sP81),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(435,plain,(~(sP422) | ~(sP91)),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(436,plain,(~(sP404) | sP393),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(437,plain,(~(sP303) | sP56),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(438,plain,(~(sP239) | sP290),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(439,plain,(~(sP400) | sP127),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(440,plain,(~(sP356) | sP57),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(441,plain,(~(sP481) | sP231),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(442,plain,(~(sP319) | sP426),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(443,plain,(~(sP30) | sP220),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(444,plain,(~(sP4) | sP177),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(445,plain,(~(sP425) | sP286),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(446,plain,(~(sP391) | sP336),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(447,plain,(~(sP313) | sP238),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(448,plain,(~(sP273) | sP156),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(449,plain,(~(sP310) | sP243),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(450,plain,(~(sP55) | sP350),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(451,plain,(~(sP28) | sP176),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(452,plain,(~(sP20) | sP94),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(453,plain,(~(sP300) | sP11),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(454,plain,(~(sP399) | sP158),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(455,plain,(~(sP44) | sP10),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(456,plain,((~(sP431) | ~(sP413)) | sP15),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(457,plain,(~(sP456) | sP431),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(458,plain,(~(sP44) | sP109),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(459,plain,(~(sP44) | sP311),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(460,plain,(~(sP44) | sP244),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(461,plain,(~(sP399) | sP35),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(462,plain,(~(sP399) | sP359),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(463,plain,(~(sP399) | sP291),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(464,plain,(~(sP300) | sP240),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(465,plain,(~(sP28) | sP20),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(466,plain,(~(sP28) | sP300),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(467,plain,(~(sP28) | sP165),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(468,plain,((~(sP365) | ~(sP312)) | ~(sP381)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(469,plain,((~(sP184) | sP365) | ~(sP390)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(470,plain,(~(sP486) | sP184),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(471,plain,((~(sP345) | ~(sP121)) | ~(sP312)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(472,plain,((~(sP364) | sP345) | ~(sP27)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(473,plain,((~(sP323) | ~(sP121)) | ~(sP381)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(474,plain,((~(sP280) | sP323) | ~(sP278)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(475,plain,(~(sP55) | sP280),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(476,plain,(~(sP55) | sP364),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(477,plain,((~(sP72) | ~(sP265)) | sP12),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(478,plain,(~(sP456) | sP72),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(479,plain,((~(sP34) | ~(sP381)) | ~(sP121)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(480,plain,((~(sP332) | sP34) | ~(sP7)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(481,plain,(~(sP310) | sP332),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(482,plain,(~(sP273) | sP310),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(483,plain,(~(sP273) | sP55),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(484,plain,(~(sP273) | sP486),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(485,plain,(~(sP287) | sP273),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(486,plain,(~(sP469) | sP28),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(487,plain,(~(sP409) | sP399),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(488,plain,(~(sP1) | sP44),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(489,plain,(~(sP422) | ~(sP15)),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(490,plain,(~(sP404) | sP354),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(491,plain,(~(sP303) | sP347),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(492,plain,(~(sP239) | sP378),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(493,plain,(~(sP400) | sP454),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(494,plain,(~(sP356) | sP50),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(495,plain,(~(sP481) | sP190),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(496,plain,(~(sP319) | sP443),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(497,plain,(~(sP30) | sP299),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(498,plain,(~(sP4) | sP320),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(499,plain,(~(sP70) | sP258),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(500,plain,(~(sP391) | sP346),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(501,plain,(~(sP313) | sP29),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(502,plain,((~(sP368) | ~(sP95)) | sP198),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(503,plain,(~(sP313) | sP368),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(504,plain,(~(sP313) | sP51),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(505,plain,((~(sP472) | sP353) | sP424),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(506,plain,((~(sP212) | sP472) | sP466),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(507,plain,((~(sP331) | sP198) | sP201),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(508,plain,((~(sP376) | sP331) | sP390),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(509,plain,(~(sP391) | sP376),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(510,plain,(~(sP391) | sP212),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(511,plain,((~(sP437) | sP82) | ~(sP172)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(512,plain,((~(sP88) | ~(sP424)) | ~(sP201)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(513,plain,((~(sP82) | sP88) | ~(sP224)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(514,plain,(~(sP335) | sP437),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(515,plain,(~(sP70) | sP335),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(516,plain,(~(sP4) | sP425),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(517,plain,(~(sP4) | sP70),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(518,plain,((~(sP209) | ~(sP386)) | sP353),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(519,plain,(~(sP456) | sP209),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(520,plain,((~(sP179) | ~(sP390)) | ~(sP466)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(521,plain,((~(sP46) | sP179) | ~(sP7)),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(522,plain,(~(sP30) | sP46),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(523,plain,(~(sP319) | sP30),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(524,plain,(~(sP287) | sP319),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(525,plain,(~(sP469) | sP4),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(526,plain,(~(sP409) | sP391),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(527,plain,(~(sP1) | sP313),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(528,plain,(~(sP422) | ~(sP12)),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(529,plain,(~(sP239) | sP191),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(530,plain,(~(sP356) | sP281),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(531,plain,(~(sP481) | sP65),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(532,plain,(~(sP481) | sP395),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(533,plain,((~(sP97) | sP269) | sP172),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(534,plain,((~(sP211) | sP97) | sP7),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(535,plain,(~(sP356) | sP211),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(536,plain,(~(sP239) | sP400),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(537,plain,(~(sP404) | sP303),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(538,plain,(~(sP287) | sP404),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(539,plain,(~(sP469) | sP239),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(540,plain,(~(sP409) | sP356),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(541,plain,(~(sP1) | sP481),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(542,plain,(~(sP422) | ~(sP353)),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(543,plain,((~(sP407) | ~(sP136)) | sP269),inference(prop_rule,[status(thm)],[])). % 85.47/85.52 thf(544,plain,(~(sP456) | sP407),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(545,plain,(~(sP181) | sP456),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(546,plain,sP181,inference(eq_sym,[status(thm)],[])). % 85.47/85.52 thf(547,plain,(~(sP422) | ~(sP269)),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(548,plain,(~(sP1) | sP133),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(549,plain,(~(sP409) | sP436),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(550,plain,(~(sP469) | sP252),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(551,plain,(~(sP287) | sP89),inference(all_rule,[status(thm)],[])). % 85.47/85.52 thf(axb,axiom,sP287). % 85.47/85.52 thf(axr,axiom,sP469). % 85.47/85.52 thf(rb_cov,axiom,sP409). % 85.47/85.52 thf(552,plain,$false,inference(prop_unsat,[status(thm),assumptions([h3,h1,h2,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,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,301,302,303,304,305,306,307,308,309,310,311,312,313,314,315,316,317,318,319,320,321,322,323,324,325,326,327,328,329,330,331,332,333,334,335,336,337,338,339,340,341,342,343,344,345,346,347,348,349,350,351,352,353,354,355,356,357,358,359,360,361,362,363,364,365,366,367,368,369,370,371,372,373,374,375,376,377,378,379,380,381,382,383,384,385,386,387,388,389,390,391,392,393,394,395,396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,448,449,450,451,452,453,454,455,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,472,473,474,475,476,477,478,479,480,481,482,483,484,485,486,487,488,489,490,491,492,493,494,495,496,497,498,499,500,501,502,503,504,505,506,507,508,509,510,511,512,513,514,515,516,517,518,519,520,521,522,523,524,525,526,527,528,529,530,531,532,533,534,535,536,537,538,539,540,541,542,543,544,545,546,547,548,549,550,551,axb,axr,rb_cov,h1,h3])). % 85.47/85.52 thf(553,plain,$false,inference(tab_negall,[status(thm),assumptions([h1,h2,h0]),tab_negall(discharge,[h3]),tab_negall(eigenvar,eigen__1)],[h2,552,h3])). % 85.47/85.52 thf(554,plain,$false,inference(tab_negimp,[status(thm),assumptions([h0]),tab_negimp(discharge,[h1,h2])],[h0,553,h1,h2])). % 85.47/85.52 thf(inf,axiom,(~((![X1:$i>$i]:((inj @ X1) => (surj @ X1)))))). % 85.47/85.52 thf(555,plain,(~((![X1:$i>$i]:((![X2:$i]:(![X3:$i]:(((X1 @ X2) = (X1 @ X3)) => (X2 = X3)))) => (![X2:$i]:(~((![X3:$i]:(~(((X1 @ X3) = X2))))))))))),inference(preprocess,[status(thm)],[inf]). % 85.47/85.52 thf(556,plain,$false,inference(tab_negall,[status(thm),tab_negall(discharge,[h0]),tab_negall(eigenvar,eigen__0)],[555,554,h0])). % 85.47/85.52 % SZS output end Proof %------------------------------------------------------------------------------