lessThan - Sigma Knowledge base Browser

appearance as argument number 1

s__documentation(s__lessThan__m,s__ChineseLanguage,'(lessThan ?NUMBER1 ?NUMBER2) 是真的以防 ?NUMBER1 的 Quantity 比 ?NUMBER2 的 Quantity 要少。')	Merge.kif 1904-1905
s__documentation(s__lessThan__m,s__EnglishLanguage,'(lessThan ?NUMBER1 ?NUMBER2) is true just in case the Quantity ?NUMBER1 is less than the Quantity ?NUMBER2.')	Merge.kif 1902-1903
s__domain(s__lessThan__m,1,s__Quantity)	Merge.kif 1900-1900	The number 1 argument of less than is an instance of quantity
s__domain(s__lessThan__m,2,s__Quantity)	Merge.kif 1901-1901	The number 2 argument of less than is an instance of quantity
s__instance(s__BinaryPredicate,s__SetOrClass) s__instance(s__lessThan__m,s__BinaryPredicate)	Merge.kif 1895-1895	less than is an instance of binary predicate
s__instance(s__IrreflexiveRelation,s__SetOrClass) s__instance(s__lessThan__m,s__IrreflexiveRelation)	Merge.kif 1897-1897	less than is an instance of irreflexive relation
s__instance(s__lessThan__m,s__RelationExtendedToQuantities) s__instance(s__RelationExtendedToQuantities,s__SetOrClass)	Merge.kif 1898-1898	less than is an instance of relation extended to quantities
s__instance(s__lessThan__m,s__TransitiveRelation) s__instance(s__TransitiveRelation,s__SetOrClass)	Merge.kif 1896-1896	less than is an instance of transitive relation
s__trichotomizingOn(s__lessThan__m,s__RealNumber)	Merge.kif 1899-1899	less than is trichotomizing on real number

appearance as argument number 2

s__format(s__ChineseLanguage,s__lessThan__m,'%1 %n 是 lessThan %2')	chinese_format.kif 141-141
s__format(s__EnglishLanguage,s__lessThan__m,'%1 is %n less than %2')	english_format.kif 97-97
s__inverse(s__greaterThan__m,s__lessThan__m)	Merge.kif 1915-1915	greater than is an inverse of less than
s__termFormat(s__ChineseLanguage,s__lessThan__m,'少于')	chinese_format.kif 142-142	"少于" is the printable form of less than in ChineseLanguage
s__termFormat(s__EnglishLanguage,s__lessThan__m,'less than')	domainEnglishFormat.kif 6109-6109	"less than" is the printable form of less than in english language

antecedent

( ! [V__S,V__LD] : (s__instance(V__S,s__RealNumber)s__=>((s__instance(V__LD,s__LiquidDrop)s__and__ms__approximateDiameter(V__LD,s__MeasureFn(V__S,s__Micrometer)) s__and__ms__lessThan(500,V__S)) s__<=> s__instance(V__LD,s__Droplet))) )	Geography.kif 6874-6880	A self connected object is an instance of liquid drop and the approximate diameter of the self connected object is a real number micrometer(s) and 500 is less than the real number if and only if the self connected object is an instance of droplet
( ! [V__Time,V__Option] : ((s__instance(V__Time,s__Agent)s__and__ms__instance(V__Time,s__TimePosition)) s__=>((s__exists__m[V__Stock,V__StockPrice,V__StrikePrice] : (s__instance(V__Stock,s__FinancialInstrument)s__and__ms__instance(V__StockPrice,s__CurrencyMeasure)s__and__ms__instance(V__StrikePrice,s__CurrencyMeasure)s__and__m(s__instance(V__Option,s__CallOption)s__and__ms__underlier(V__Option,V__Stock) s__and__ms__price(V__Stock,V__StockPrice,V__Time) s__and__ms__strikePrice(V__Option,V__StrikePrice) s__and__ms__lessThan(V__StockPrice,V__StrikePrice)))) s__<=> s__outOfTheMoney(V__Option,V__Time))) )	FinancialOntology.kif 2965-2973	There exist a financial instrument, the financial instrumentPrice and another currency measure such that an agreement is an instance of call option and the financial instrument is an underlier of the agreement and the financial instrument price the financial instrumentPrice for an agent and the other currency measure is a strike price of the agreement and the financial instrumentPrice is less than the other currency measure if and only if the agent is an out of the money of the agreement
( ! [V__Time,V__Option] : ((s__instance(V__Time,s__Agent)s__and__ms__instance(V__Time,s__TimePosition)) s__=>((s__exists__m[V__Stock,V__StockPrice,V__StrikePrice] : (s__instance(V__Stock,s__FinancialInstrument)s__and__ms__instance(V__StockPrice,s__CurrencyMeasure)s__and__ms__instance(V__StrikePrice,s__CurrencyMeasure)s__and__m(s__instance(V__Option,s__CallOption)s__and__ms__underlier(V__Option,V__Stock) s__and__ms__price(V__Stock,V__StockPrice,V__Time) s__and__ms__strikePrice(V__Option,V__StrikePrice) s__and__ms__lessThan(V__StrikePrice,V__StockPrice)))) s__<=> s__inTheMoney(V__Option,V__Time))) )	FinancialOntology.kif 2922-2930	There exist a financial instrument, the financial instrumentPrice and another currency measure such that an agreement is an instance of call option and the financial instrument is an underlier of the agreement and the financial instrument price the financial instrumentPrice for an agent and the other currency measure is a strike price of the agreement and the other currency measure is less than the financial instrumentPrice if and only if the agent is an in the money of the agreement
( ! [V__Time,V__Option] : ((s__instance(V__Time,s__Agent)s__and__ms__instance(V__Time,s__TimePosition)) s__=>((s__exists__m[V__Stock,V__StockPrice,V__StrikePrice] : (s__instance(V__Stock,s__FinancialInstrument)s__and__ms__instance(V__StockPrice,s__CurrencyMeasure)s__and__ms__instance(V__StrikePrice,s__CurrencyMeasure)s__and__m(s__instance(V__Option,s__PutOption)s__and__ms__underlier(V__Option,V__Stock) s__and__ms__price(V__Stock,V__StockPrice,V__Time) s__and__ms__strikePrice(V__Option,V__StrikePrice) s__and__ms__lessThan(V__StockPrice,V__StrikePrice)))) s__<=> s__inTheMoney(V__Option,V__Time))) )	FinancialOntology.kif 2932-2940	There exist a financial instrument, the financial instrumentPrice and another currency measure such that an agreement is an instance of put option and the financial instrument is an underlier of the agreement and the financial instrument price the financial instrumentPrice for an agent and the other currency measure is a strike price of the agreement and the financial instrumentPrice is less than the other currency measure if and only if the agent is an in the money of the agreement
( ! [V__Time,V__Option] : ((s__instance(V__Time,s__Agent)s__and__ms__instance(V__Time,s__TimePosition)) s__=>((s__exists__m[V__Stock,V__StockPrice,V__StrikePrice] : (s__instance(V__Stock,s__FinancialInstrument)s__and__ms__instance(V__StockPrice,s__CurrencyMeasure)s__and__ms__instance(V__StrikePrice,s__CurrencyMeasure)s__and__m(s__instance(V__Option,s__PutOption)s__and__ms__underlier(V__Option,V__Stock) s__and__ms__price(V__Stock,V__StockPrice,V__Time) s__and__ms__strikePrice(V__Option,V__StrikePrice) s__and__ms__lessThan(V__StrikePrice,V__StockPrice)))) s__<=> s__outOfTheMoney(V__Option,V__Time))) )	FinancialOntology.kif 2975-2983	There exist a financial instrument, the financial instrumentPrice and another currency measure such that an agreement is an instance of put option and the financial instrument is an underlier of the agreement and the financial instrument price the financial instrumentPrice for an agent and the other currency measure is a strike price of the agreement and the other currency measure is less than the financial instrumentPrice if and only if the agent is an out of the money of the agreement
( ! [V__Date,V__Balance,V__Account,V__Overdraft] : ((s__instance(V__Date,s__Day)s__and__ms__instance(V__Balance,s__RealNumber)s__and__ms__instance(V__Account,s__FinancialAccount)s__and__ms__instance(V__Overdraft,s__RealNumber)) s__=>((s__currentAccountBalance(V__Account,V__Date,s__MeasureFn(V__Balance,s__UnitedStatesDollar)) s__and__ms__lessThan(V__Balance,0) s__and__m(V__Overdrafts__equal__ms__SubtractionFn(0,V__Balance))) s__=>s__overdraft(V__Account,s__MeasureFn(V__Overdraft,s__UnitedStatesDollar),V__Date))) )	FinancialOntology.kif 733-738	If a financial account current account balance a day for a real number united states dollar(s) and the real number is less than 0 and another real number is equal to (0 and the real number), then the financial account overdraft the other real number united states dollar(s) for the day
( ! [V__Amount,V__Date,V__Balance,V__Account,V__FinancialAccount] : ((s__instance(V__Amount,s__CurrencyMeasure)s__and__ms__instance(V__Date,s__Day)s__and__ms__instance(V__Balance,s__CurrencyMeasure)s__and__ms__instance(V__Account,s__FinancialAccount)s__and__ms__instance(V__FinancialAccount,s__SetOrClass)) s__=>((s__instance(V__Account,V__FinancialAccount) s__and__ms__minimumBalance(V__Account,s__UsingAnAccount,V__Balance) s__and__ms__currentAccountBalance(V__Account,V__Date,V__Amount) s__and__ms__lessThan(V__Amount,V__Balance)) s__=>(s__exists__m[V__Penalty] : (s__instance(V__Penalty,s__Penalty)s__and__ms__date(V__Penalty,V__Date) s__and__ms__destination(V__Penalty,s__CurrencyFn(V__Account)))))) )	FinancialOntology.kif 658-668	If a financial account is an instance of a set or class and the financial account minimum balance using an account for a currency measure and the financial account current account balance a day for another currency measure and the other currency measure is less than the currency measure, then there exists a process such that the process is an instance of penalty and date of the process is the day and the process ends up at the currency of the financial account
( ! [V__Amount,V__MinPayment,V__Account] : ((s__instance(V__Amount,s__CurrencyMeasure)s__and__ms__instance(V__MinPayment,s__CurrencyMeasure)) s__=>((s__instance(V__Account,s__LiabilityAccount)s__and__ms__minimumPayment(V__Account,V__MinPayment,s__MonthDuration)s__and__m(s__exists__m[V__Payment,V__Month] : (s__instance(V__Payment,s__Process)s__and__m(s__instance(V__Month,s__Month)s__and__ms__destination(V__Payment,s__CurrencyFn(V__Account)) s__and__ms__paymentsPerPeriod(V__Account,V__Amount,V__Month) s__and__ms__lessThan(V__Amount,V__MinPayment))))) s__=>(s__exists__m[V__Penalty] : (s__instance(V__Penalty,s__Penalty)s__and__ms__destination(V__Penalty,s__CurrencyFn(V__Account)))))) )	FinancialOntology.kif 712-725	If a liability account is an instance of liability account and the liability account minimum payment a currency measure for month duration and there exist a process and a time interval such that the time interval is an instance of month and the process ends up at the currency of the liability account and the liability account payments per period another currency measure for the time interval and the other currency measure is less than the currency measure, then there exists another process such that the other process is an instance of penalty and the other process ends up at the currency of the liability account
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 492-498	If an entity is an instance of human and the age of the entity is a quantity year duration(s) holds during a time position and the quantity is greater than 12 and the quantity is less than 20, then the entity is an instance of teenager holds during the time position
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 419-424	If an entity is an instance of human and the age of the entity is a quantity year duration(s) holds during a time position and the quantity is less than 18, then the entity is an instance of human youth holds during the time position
No TPTP formula. May not be expressible in strict first order.	Merge.kif 13854-13869	If an entity is an instance of a kind of pure substance and a real number an unit of measure(s) is a boiling point of a kind of pure substance and another real number the unit of measure(s) is a melting point of the kind of pure substance and the unit of measure is an instance of UnitOfTemperature and the measure of the entity is a quantity the unit of measure(s) holds during a time interval and the quantity is greater than the other real number and the quantity is less than the real number, then liquid is an attribute of the entity holds during the time interval or there exists a physical such that the time interval overlaps the time of existence of the physical and the physical is an instance of melting and the entity is a patient of a process
No TPTP formula. May not be expressible in strict first order.	Merge.kif 13871-13884	If an entity is an instance of a kind of pure substance and a real number an unit of measure(s) is a melting point of a kind of pure substance and the measure of the entity is a quantity the unit of measure(s) holds during a time interval and the unit of measure is an instance of UnitOfTemperature and the quantity is less than the real number, then solid is an attribute of the entity holds during the time interval or there exists a process such that the time interval overlaps the time of existence of the process and the process is an instance of freezing and the entity is a patient of the process
( ! [V__DEPTH,V__OBJ,V__DRAFT,V__WATERWAY,V__UNIT] : ((s__instance(V__DEPTH,s__RealNumber)s__and__ms__instance(V__OBJ,s__Physical)s__and__ms__instance(V__DRAFT,s__RealNumber)) s__=>((s__instance(V__WATERWAY,s__Waterway)s__and__ms__depth(V__OBJ,V__WATERWAY,s__MeasureFn(V__DEPTH,V__UNIT)) s__and__ms__instance(V__UNIT,s__UnitOfLength)s__and__ms__lessThan(V__DRAFT,V__DEPTH)) s__=>s__navigableForDraft(V__WATERWAY,s__MeasureFn(V__DRAFT,V__UNIT)))) )	Transportation.kif 2608-2614	If a water area is an instance of waterway and the depth from a physical to the water area is a real number an unit of measure(s) and the unit of measure is an instance of UnitOfLength and another real number is less than the real number, then the other real number the unit of measure(s) is a navigable for draft of the water area
( ! [V__MELT,V__X,V__BOIL,V__Y,V__TEMP] : ((s__instance(V__MELT,s__RealNumber)s__and__ms__instance(V__X,s__Object)s__and__ms__instance(V__BOIL,s__RealNumber)s__and__ms__subclass(V__Y,s__PureSubstance)s__and__ms__instance(V__Y,s__SetOrClass)s__and__ms__instance(V__TEMP,s__RealNumber)) s__=>((s__instance(V__X,V__Y) s__and__ms__subclass(V__Y,s__PureSubstance)s__and__ms__boilingPoint(V__Y,s__MeasureFn(V__BOIL,s__KelvinDegree)) s__and__ms__meltingPoint(V__Y,s__MeasureFn(V__MELT,s__KelvinDegree)) s__and__ms__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree)) s__and__ms__greaterThan(V__TEMP,V__MELT) s__and__ms__lessThan(V__TEMP,V__BOIL)) s__=>s__attribute(V__X,s__Liquid))) )	Merge.kif 13798-13807	If an object is an instance of a kind of pure substance and a kind of pure substance is a subclass of pure substance and a real number kelvin degree(s) is a boiling point of the kind of pure substance and another real number kelvin degree(s) is a melting point of the kind of pure substance and the measure of the object is a third real number kelvin degree(s) and the third real number is greater than the other real number and the third real number is less than the real number, then liquid is an attribute of the object
( ! [V__PRES,V__MELT,V__X,V__Y,V__TEMP] : ((s__instance(V__PRES,s__RealNumber)s__and__ms__instance(V__MELT,s__RealNumber)s__and__ms__instance(V__X,s__Object)s__and__ms__subclass(V__Y,s__PureSubstance)s__and__ms__instance(V__Y,s__SetOrClass)s__and__ms__instance(V__TEMP,s__RealNumber)) s__=>((s__instance(V__X,V__Y) s__and__ms__subclass(V__Y,s__PureSubstance)s__and__ms__meltingPoint(V__Y,s__MeasureFn(V__MELT,s__KelvinDegree)) s__and__ms__barometricPressure(V__X,s__MeasureFn(V__PRES,s__InchMercury)) s__and__ms__greaterThan(V__PRES,29.92) s__and__ms__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree)) s__and__ms__lessThan(V__TEMP,V__MELT)) s__=>s__attribute(V__X,s__Solid))) )	Merge.kif 13809-13818	If an object is an instance of a kind of pure substance and a kind of pure substance is a subclass of pure substance and a real number kelvin degree(s) is a melting point of the kind of pure substance and another real number inch mercury(s) is a barometric pressure of the object and the other real number is greater than 29.92 and the measure of the object is a third real number kelvin degree(s) and the third real number is less than the real number, then solid is an attribute of the object
( ! [V__Process1,V__Process2,V__Number1,V__Number2,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7] : ((s__instance(V__Process1,s__Physical)s__and__ms__instance(V__Process2,s__Physical)s__and__ms__instance(V__Number1,s__PositiveInteger)s__and__ms__instance(V__Number2,s__PositiveInteger)) s__=>((s__processList__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7) s__and__ms__inList(V__Process1,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)) s__and__ms__inList(V__Process2,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)) s__and__m(s__ListOrderFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7) ,V__Number1) s__equal__mV__Process1)s__and__m(s__ListOrderFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7) ,V__Number2) s__equal__mV__Process2)s__and__ms__lessThan(V__Number1,V__Number2)) s__=>s__earlier(s__WhenFn(V__Process1) ,s__WhenFn(V__Process2)))) ) ( ! [V__Process1,V__Process2,V__Number1,V__Number2,V__ROW2] : ((s__instance(V__Process1,s__Physical)s__and__ms__instance(V__Process2,s__Physical)s__and__ms__instance(V__Number1,s__PositiveInteger)s__and__ms__instance(V__Number2,s__PositiveInteger)) s__=>((s__processList__1(V__ROW2) s__and__ms__inList(V__Process1,s__ListFn__1Fn(V__ROW2)) s__and__ms__inList(V__Process2,s__ListFn__1Fn(V__ROW2)) s__and__m(s__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__Number1) s__equal__mV__Process1)s__and__m(s__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__Number2) s__equal__mV__Process2)s__and__ms__lessThan(V__Number1,V__Number2)) s__=>s__earlier(s__WhenFn(V__Process1) ,s__WhenFn(V__Process2)))) ) ( ! [V__Process1,V__Process2,V__Number1,V__Number2,V__ROW2,V__ROW3,V__ROW4,V__ROW5] : ((s__instance(V__Process1,s__Physical)s__and__ms__instance(V__Process2,s__Physical)s__and__ms__instance(V__Number1,s__PositiveInteger)s__and__ms__instance(V__Number2,s__PositiveInteger)) s__=>((s__processList__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5) s__and__ms__inList(V__Process1,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)) s__and__ms__inList(V__Process2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)) s__and__m(s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5) ,V__Number1) s__equal__mV__Process1)s__and__m(s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5) ,V__Number2) s__equal__mV__Process2)s__and__ms__lessThan(V__Number1,V__Number2)) s__=>s__earlier(s__WhenFn(V__Process1) ,s__WhenFn(V__Process2)))) ) ( ! [V__Process1,V__Process2,V__Number1,V__Number2,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8] : ((s__instance(V__Process1,s__Physical)s__and__ms__instance(V__Process2,s__Physical)s__and__ms__instance(V__Number1,s__PositiveInteger)s__and__ms__instance(V__Number2,s__PositiveInteger)) s__=>((s__processList__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8) s__and__ms__inList(V__Process1,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)) s__and__ms__inList(V__Process2,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)) s__and__m(s__ListOrderFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8) ,V__Number1) s__equal__mV__Process1)s__and__m(s__ListOrderFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8) ,V__Number2) s__equal__mV__Process2)s__and__ms__lessThan(V__Number1,V__Number2)) s__=>s__earlier(s__WhenFn(V__Process1) ,s__WhenFn(V__Process2)))) ) ( ! [V__Process1,V__Process2,V__Number1,V__Number2,V__ROW2,V__ROW3,V__ROW4] : ((s__instance(V__Process1,s__Physical)s__and__ms__instance(V__Process2,s__Physical)s__and__ms__instance(V__Number1,s__PositiveInteger)s__and__ms__instance(V__Number2,s__PositiveInteger)) s__=>((s__processList__3(V__ROW2,V__ROW3,V__ROW4) s__and__ms__inList(V__Process1,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)) s__and__ms__inList(V__Process2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)) s__and__m(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4) ,V__Number1) s__equal__mV__Process1)s__and__m(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4) ,V__Number2) s__equal__mV__Process2)s__and__ms__lessThan(V__Number1,V__Number2)) s__=>s__earlier(s__WhenFn(V__Process1) ,s__WhenFn(V__Process2)))) ) ( ! [V__Process1,V__Process2,V__Number1,V__Number2,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6] : ((s__instance(V__Process1,s__Physical)s__and__ms__instance(V__Process2,s__Physical)s__and__ms__instance(V__Number1,s__PositiveInteger)s__and__ms__instance(V__Number2,s__PositiveInteger)) s__=>((s__processList__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6) s__and__ms__inList(V__Process1,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)) s__and__ms__inList(V__Process2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)) s__and__m(s__ListOrderFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6) ,V__Number1) s__equal__mV__Process1)s__and__m(s__ListOrderFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6) ,V__Number2) s__equal__mV__Process2)s__and__ms__lessThan(V__Number1,V__Number2)) s__=>s__earlier(s__WhenFn(V__Process1) ,s__WhenFn(V__Process2)))) ) ( ! [V__Process1,V__Process2,V__Number1,V__Number2,V__ROW2,V__ROW3] : ((s__instance(V__Process1,s__Physical)s__and__ms__instance(V__Process2,s__Physical)s__and__ms__instance(V__Number1,s__PositiveInteger)s__and__ms__instance(V__Number2,s__PositiveInteger)) s__=>((s__processList__2(V__ROW2,V__ROW3) s__and__ms__inList(V__Process1,s__ListFn__2Fn(V__ROW2,V__ROW3)) s__and__ms__inList(V__Process2,s__ListFn__2Fn(V__ROW2,V__ROW3)) s__and__m(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3) ,V__Number1) s__equal__mV__Process1)s__and__m(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3) ,V__Number2) s__equal__mV__Process2)s__and__ms__lessThan(V__Number1,V__Number2)) s__=>s__earlier(s__WhenFn(V__Process1) ,s__WhenFn(V__Process2)))) )	QoSontology.kif 690-698	If the list of processes @ROW and a physical is a member of (@ROW) and another physical is a member of (@ROW) and another entity element of (@ROW) is equal to the physical and a third entity element of (@ROW) is equal to the other physical and a positive integer is less than another positive integer, then the time of existence of the physical happens earlier than the time of existence of the other physical
No TPTP formula. May not be expressible in strict first order.	Catalog.kif 415-427	If a cognitive agent sells a kind of entity for a currency measure and the price of a kind of entity from the cognitive agent according to a pricing scheme is another currency measure and the pricing scheme is valid for a kind of agent and another entity is an instance of the kind of entity and a process is an instance of buying and another agent is an immediate instance of a kind of agent and the other agent is an agent of the process and the process originates at the cognitive agent and the other currency measure is less than the currency measure, then the statement the currency measure is a transaction amount of the process has the modal force of likely
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 3477-3487	If minimum device operating temperature of an entity is another entity and the entity is located at a third entity and device on is an attribute of the entity and a fourth entity is an air temperature of the third entity and the fourth entity is less than the other entity holds during a time position, then the statement DeviceDamaged is an attribute of the entity holds during immediately after the time position has the modal force of likely
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 3500-3510	If minimum device storagqqqe temperature of an entity is another entity and the entity is located at a third entity and device off is an attribute of the entity and a fourth entity is an air temperature of the third entity and the fourth entity is less than the other entity holds during a time position, then the statement DeviceDamaged is an attribute of the entity holds during immediately after the time position has the modal force of likely

consequent

( ! [V__ROW2] : (s__instance(V__ROW2,s__TimeInterval)s__=>((s__instance(s__duration__m,s__TotalValuedRelation)s__and__ms__instance(s__duration__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__duration__m,s__Relation)s__and__ms__valence(s__duration__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__duration__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__TimeDuration)s__and__ms__duration(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__GeometricFigure)s__=>((s__instance(s__geometricPart__m,s__TotalValuedRelation)s__and__ms__instance(s__geometricPart__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__geometricPart__m,s__Relation)s__and__ms__valence(s__geometricPart__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__geometricPart__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__GeometricFigure)s__and__ms__geometricPart(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Circle)s__=>((s__instance(s__diameter__m,s__TotalValuedRelation)s__and__ms__instance(s__diameter__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__diameter__m,s__Relation)s__and__ms__valence(s__diameter__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__diameter__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__LengthMeasure)s__and__ms__diameter(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Process)s__=>((s__instance(s__subProcess__m,s__TotalValuedRelation)s__and__ms__instance(s__subProcess__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subProcess__m,s__Relation)s__and__ms__valence(s__subProcess__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__subProcess__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Process)s__and__ms__subProcess(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__SelfConnectedObject)s__=>((s__instance(s__approximateDiameter__m,s__TotalValuedRelation)s__and__ms__instance(s__approximateDiameter__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__approximateDiameter__m,s__Relation)s__and__ms__valence(s__approximateDiameter__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__approximateDiameter__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__LengthMeasure)s__and__ms__approximateDiameter(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__SetOrClass)s__=>((s__instance(s__subclass__m,s__TotalValuedRelation)s__and__ms__instance(s__subclass__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subclass__m,s__Relation)s__and__ms__valence(s__subclass__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__subclass__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__SetOrClass)s__and__ms__subclass(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__subclass(V__ROW2,s__ContentBearingPhysical)s__=>((s__instance(s__subsumesContentClass__m,s__TotalValuedRelation)s__and__ms__instance(s__subsumesContentClass__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subsumesContentClass__m,s__Relation)s__and__ms__valence(s__subsumesContentClass__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__subsumesContentClass__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__subclass(V__ITEM,s__ContentBearingPhysical)s__and__ms__subsumesContentClass(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Quantity)s__=>((s__instance(s__greaterThan__m,s__TotalValuedRelation)s__and__ms__instance(s__greaterThan__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__greaterThan__m,s__Relation)s__and__ms__valence(s__greaterThan__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__greaterThan__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Quantity)s__and__ms__greaterThan(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW3,V__ROW2] : ((s__instance(V__ROW3,s__Physical)s__and__ms__instance(V__ROW2,s__Physical)) s__=>((s__instance(s__distance__m,s__TotalValuedRelation)s__and__ms__instance(s__distance__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__distance__m,s__Relation)s__and__ms__valence(s__distance__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__distance__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__LengthMeasure)s__and__ms__distance(V__ROW2,V__ROW3,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Physical)s__=>((s__instance(s__partlyLocated__m,s__TotalValuedRelation)s__and__ms__instance(s__partlyLocated__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__partlyLocated__m,s__Relation)s__and__ms__valence(s__partlyLocated__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__partlyLocated__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Object)s__and__ms__partlyLocated(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Argument)s__=>((s__instance(s__conclusion__m,s__TotalValuedRelation)s__and__ms__instance(s__conclusion__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__conclusion__m,s__Relation)s__and__ms__valence(s__conclusion__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__conclusion__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Proposition)s__and__ms__conclusion(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Process)s__=>((s__instance(s__eventLocated__m,s__TotalValuedRelation)s__and__ms__instance(s__eventLocated__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__eventLocated__m,s__Relation)s__and__ms__valence(s__eventLocated__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__eventLocated__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : s__eventLocated(V__ROW2,V__ITEM)))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__List)s__=>((s__instance(s__initialList__m,s__TotalValuedRelation)s__and__ms__instance(s__initialList__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__initialList__m,s__Relation)s__and__ms__valence(s__initialList__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__initialList__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : s__initialList(V__ROW2,V__ITEM)))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Relation)s__=>((s__instance(s__subrelation__m,s__TotalValuedRelation)s__and__ms__instance(s__subrelation__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subrelation__m,s__Relation)s__and__ms__valence(s__subrelation__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__subrelation__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Relation)s__and__ms__subrelation(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Motion)s__=>((s__instance(s__path__m,s__TotalValuedRelation)s__and__ms__instance(s__path__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__path__m,s__Relation)s__and__ms__valence(s__path__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__path__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Object)s__and__ms__path(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__TimePosition)s__=>((s__instance(s__temporalPart__m,s__TotalValuedRelation)s__and__ms__instance(s__temporalPart__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__temporalPart__m,s__Relation)s__and__ms__valence(s__temporalPart__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__temporalPart__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__TimePosition)s__and__ms__temporalPart(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__TimeInterval)s__=>((s__instance(s__meetsTemporally__m,s__TotalValuedRelation)s__and__ms__instance(s__meetsTemporally__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__meetsTemporally__m,s__Relation)s__and__ms__valence(s__meetsTemporally__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__meetsTemporally__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__TimeInterval)s__and__ms__meetsTemporally(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Circle)s__=>((s__instance(s__radius__m,s__TotalValuedRelation)s__and__ms__instance(s__radius__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__radius__m,s__Relation)s__and__ms__valence(s__radius__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__radius__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__LengthMeasure)s__and__ms__radius(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Physical)s__=>((s__instance(s__time__m,s__TotalValuedRelation)s__and__ms__instance(s__time__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__time__m,s__Relation)s__and__ms__valence(s__time__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__time__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__TimePosition)s__and__ms__time(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Process)s__=>((s__instance(s__coordinates__m,s__TotalValuedRelation)s__and__ms__instance(s__coordinates__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__coordinates__m,s__Relation)s__and__ms__valence(s__coordinates__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__coordinates__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Process)s__and__ms__coordinates(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Vehicle)s__=>((s__instance(s__maximumPayloadCapacity__m,s__TotalValuedRelation)s__and__ms__instance(s__maximumPayloadCapacity__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__maximumPayloadCapacity__m,s__Relation)s__and__ms__valence(s__maximumPayloadCapacity__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__maximumPayloadCapacity__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__MassMeasure)s__and__ms__maximumPayloadCapacity(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Motion)s__=>((s__instance(s__moves__m,s__TotalValuedRelation)s__and__ms__instance(s__moves__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__moves__m,s__Relation)s__and__ms__valence(s__moves__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__moves__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Object)s__and__ms__moves(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Translocation)s__=>((s__instance(s__changesLocation__m,s__TotalValuedRelation)s__and__ms__instance(s__changesLocation__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__changesLocation__m,s__Relation)s__and__ms__valence(s__changesLocation__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__changesLocation__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Object)s__and__ms__changesLocation(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Argument)s__=>((s__instance(s__premise__m,s__TotalValuedRelation)s__and__ms__instance(s__premise__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__premise__m,s__Relation)s__and__ms__valence(s__premise__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__premise__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Proposition)s__and__ms__premise(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__GraphElement)s__=>((s__instance(s__graphPart__m,s__TotalValuedRelation)s__and__ms__instance(s__graphPart__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__graphPart__m,s__Relation)s__and__ms__valence(s__graphPart__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__graphPart__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Graph)s__and__ms__graphPart(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Contest)s__=>((s__instance(s__contestParticipant__m,s__TotalValuedRelation)s__and__ms__instance(s__contestParticipant__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__contestParticipant__m,s__Relation)s__and__ms__valence(s__contestParticipant__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__contestParticipant__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Agent)s__and__ms__contestParticipant(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW3,V__ROW2] : ((s__subclass(V__ROW3,s__Weapon)s__and__ms__instance(V__ROW2,s__MilitaryVehicle)) s__=>((s__instance(s__weaponCarryingCapability__m,s__TotalValuedRelation)s__and__ms__instance(s__weaponCarryingCapability__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__weaponCarryingCapability__m,s__Relation)s__and__ms__valence(s__weaponCarryingCapability__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__weaponCarryingCapability__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__PositiveInteger)s__and__ms__weaponCarryingCapability(V__ROW2,V__ROW3,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__TimePoint)s__=>((s__instance(s__beforeOrEqual__m,s__TotalValuedRelation)s__and__ms__instance(s__beforeOrEqual__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__beforeOrEqual__m,s__Relation)s__and__ms__valence(s__beforeOrEqual__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__beforeOrEqual__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__TimePoint)s__and__ms__beforeOrEqual(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Organism)s__=>((s__instance(s__parent__m,s__TotalValuedRelation)s__and__ms__instance(s__parent__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__parent__m,s__Relation)s__and__ms__valence(s__parent__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__parent__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Organism)s__and__ms__parent(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__PassengerVehicle)s__=>((s__instance(s__personTransportCapability__m,s__TotalValuedRelation)s__and__ms__instance(s__personTransportCapability__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__personTransportCapability__m,s__Relation)s__and__ms__valence(s__personTransportCapability__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__personTransportCapability__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__PositiveInteger)s__and__ms__personTransportCapability(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__SymbolicString)s__=>((s__instance(s__subString__m,s__TotalValuedRelation)s__and__ms__instance(s__subString__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subString__m,s__Relation)s__and__ms__valence(s__subString__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__subString__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__SymbolicString)s__and__ms__subString(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW3,V__ROW2] : ((s__instance(V__ROW3,s__SymbolicString)s__and__ms__instance(V__ROW2,s__SymbolicString)) s__=>((s__instance(s__stringConcatenation__m,s__TotalValuedRelation)s__and__ms__instance(s__stringConcatenation__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__stringConcatenation__m,s__Relation)s__and__ms__valence(s__stringConcatenation__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__stringConcatenation__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__SymbolicString)s__and__ms__stringConcatenation(V__ROW2,V__ROW3,V__ITEM))))))))) ) ( ! [V__ROW3,V__ROW2] : ((s__instance(V__ROW3,s__GeometricPoint)s__and__ms__instance(V__ROW2,s__GeometricPoint)) s__=>((s__instance(s__geometricDistance__m,s__TotalValuedRelation)s__and__ms__instance(s__geometricDistance__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__geometricDistance__m,s__Relation)s__and__ms__valence(s__geometricDistance__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__geometricDistance__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__LengthMeasure)s__and__ms__geometricDistance(V__ROW2,V__ROW3,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__List)s__=>((s__instance(s__subList__m,s__TotalValuedRelation)s__and__ms__instance(s__subList__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subList__m,s__Relation)s__and__ms__valence(s__subList__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__subList__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__List)s__and__ms__subList(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__ContentBearingPhysical)s__=>((s__instance(s__subsumesContentInstance__m,s__TotalValuedRelation)s__and__ms__instance(s__subsumesContentInstance__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subsumesContentInstance__m,s__Relation)s__and__ms__valence(s__subsumesContentInstance__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__subsumesContentInstance__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__ContentBearingPhysical)s__and__ms__subsumesContentInstance(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Object)s__=>((s__instance(s__smaller__m,s__TotalValuedRelation)s__and__ms__instance(s__smaller__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__smaller__m,s__Relation)s__and__ms__valence(s__smaller__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__smaller__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Object)s__and__ms__smaller(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Quantity)s__=>((s__instance(s__greaterThanOrEqualTo__m,s__TotalValuedRelation)s__and__ms__instance(s__greaterThanOrEqualTo__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__greaterThanOrEqualTo__m,s__Relation)s__and__ms__valence(s__greaterThanOrEqualTo__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__greaterThanOrEqualTo__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Quantity)s__and__ms__greaterThanOrEqualTo(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__FinancialTransaction)s__=>((s__instance(s__transactionAmount__m,s__TotalValuedRelation)s__and__ms__instance(s__transactionAmount__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__transactionAmount__m,s__Relation)s__and__ms__valence(s__transactionAmount__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__transactionAmount__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__CurrencyMeasure)s__and__ms__transactionAmount(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__subclass(V__ROW2,s__Gun)s__=>((s__instance(s__caliber__m,s__TotalValuedRelation)s__and__ms__instance(s__caliber__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__caliber__m,s__Relation)s__and__ms__valence(s__caliber__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__caliber__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__LengthMeasure)s__and__ms__caliber(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Abstract)s__=>((s__instance(s__abstractPart__m,s__TotalValuedRelation)s__and__ms__instance(s__abstractPart__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__abstractPart__m,s__Relation)s__and__ms__valence(s__abstractPart__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__abstractPart__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Abstract)s__and__ms__abstractPart(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Object)s__=>((s__instance(s__larger__m,s__TotalValuedRelation)s__and__ms__instance(s__larger__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__larger__m,s__Relation)s__and__ms__valence(s__larger__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__larger__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Object)s__and__ms__larger(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Language)s__=>((s__instance(s__subLanguage__m,s__TotalValuedRelation)s__and__ms__instance(s__subLanguage__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subLanguage__m,s__Relation)s__and__ms__valence(s__subLanguage__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__subLanguage__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Language)s__and__ms__subLanguage(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW3,V__ROW2] : ((s__instance(V__ROW3,s__LengthMeasure)s__and__ms__instance(V__ROW2,s__Vehicle)) s__=>((s__instance(s__maximumPayloadHeightWidth__m,s__TotalValuedRelation)s__and__ms__instance(s__maximumPayloadHeightWidth__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__maximumPayloadHeightWidth__m,s__Relation)s__and__ms__valence(s__maximumPayloadHeightWidth__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__maximumPayloadHeightWidth__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__LengthMeasure)s__and__ms__maximumPayloadHeightWidth(V__ROW2,V__ROW3,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__TimeInterval)s__=>((s__instance(s__earlier__m,s__TotalValuedRelation)s__and__ms__instance(s__earlier__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__earlier__m,s__Relation)s__and__ms__valence(s__earlier__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__earlier__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__TimeInterval)s__and__ms__earlier(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__OneDimensionalFigure)s__=>((s__instance(s__lineMeasure__m,s__TotalValuedRelation)s__and__ms__instance(s__lineMeasure__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__lineMeasure__m,s__Relation)s__and__ms__valence(s__lineMeasure__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__lineMeasure__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__LengthMeasure)s__and__ms__lineMeasure(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Quantity)s__=>((s__instance(s__lessThanOrEqualTo__m,s__TotalValuedRelation)s__and__ms__instance(s__lessThanOrEqualTo__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__lessThanOrEqualTo__m,s__Relation)s__and__ms__valence(s__lessThanOrEqualTo__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__lessThanOrEqualTo__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Quantity)s__and__ms__lessThanOrEqualTo(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__PureSubstance)s__=>((s__instance(s__protonNumber__m,s__TotalValuedRelation)s__and__ms__instance(s__protonNumber__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__protonNumber__m,s__Relation)s__and__ms__valence(s__protonNumber__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__protonNumber__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__PositiveInteger)s__and__ms__protonNumber(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Collection)s__=>((s__instance(s__subCollection__m,s__TotalValuedRelation)s__and__ms__instance(s__subCollection__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subCollection__m,s__Relation)s__and__ms__valence(s__subCollection__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__subCollection__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Collection)s__and__ms__subCollection(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__PureSubstance)s__=>((s__instance(s__electronNumber__m,s__TotalValuedRelation)s__and__ms__instance(s__electronNumber__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__electronNumber__m,s__Relation)s__and__ms__valence(s__electronNumber__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__electronNumber__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__PositiveInteger)s__and__ms__electronNumber(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__Attribute)s__=>((s__instance(s__subAttribute__m,s__TotalValuedRelation)s__and__ms__instance(s__subAttribute__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subAttribute__m,s__Relation)s__and__ms__valence(s__subAttribute__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__subAttribute__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__Attribute)s__and__ms__subAttribute(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__NonnegativeInteger)s__=>((s__instance(s__stringLength__m,s__TotalValuedRelation)s__and__ms__instance(s__stringLength__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__stringLength__m,s__Relation)s__and__ms__valence(s__stringLength__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__stringLength__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__SymbolicString)s__and__ms__stringLength(V__ROW2,V__ITEM))))))))) ) ( ! [V__ROW2] : (s__instance(V__ROW2,s__TwoDimensionalAngle)s__=>((s__instance(s__angularMeasure__m,s__TotalValuedRelation)s__and__ms__instance(s__angularMeasure__m,s__Predicate)) s__<=> (s__exists__m[V__VALENCE] : (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__angularMeasure__m,s__Relation)s__and__ms__valence(s__angularMeasure__m,V__VALENCE) s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] : ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass)) s__=>((s__lessThan(V__NUMBER,V__VALENCE) s__and__ms__domain(s__angularMeasure__m,V__NUMBER,V__CLASS) s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2) ,V__NUMBER))) s__=>s__instance(V__ELEMENT,V__CLASS)))) s__=>(s__exists__m[V__ITEM] : (s__instance(V__ITEM,s__PlaneAngleMeasure)s__and__ms__angularMeasure(V__ROW2,V__ITEM))))))))) )	Merge.kif 2331-2348	A relation is an instance of total valued relation and the relation is an instance of predicate if and only if there exists a positive integer such that the relation is an instance of relation and the relation %&has the positive integer argument(s) and if for all another positive integer, an entity and a set or class if the other positive integer is less than the positive integer and the number the other positive integer argument of the relation is an instance of the set or class and the entity is equal to the other positive integerth element of (@ROW), then the entity is an instance of the set or class , then there exists a fourth entity such that the relation @ROW and the fourth entity
No TPTP formula. May not be expressible in strict first order.	People.kif 253-277	The deaths per thousand live births of a geopolitical area and the year an integer is equal to a real number if and only if another integer is equal to the number of instances in the class described by a symbolic string and the other integer and 1000 is equal to a quantity and a third integer is equal to the number of instances in the class described by another symbolic string and the third integer and the quantity is equal to the real number
( ! [V__NUMBER] : (s__instance(V__NUMBER,s__NegativeRealNumber)s__<=> (s__lessThan(V__NUMBER,0) s__and__ms__instance(V__NUMBER,s__RealNumber))) )	Merge.kif 2020-2024	A quantity is an instance of negative real number if and only if the quantity is less than 0 and the quantity is an instance of real number
( ! [V__NUMBER1,V__NUMBER2] : ((s__instance(V__NUMBER1,s__Quantity)s__and__ms__instance(V__NUMBER2,s__Quantity)) s__=>(s__lessThanOrEqualTo(V__NUMBER1,V__NUMBER2) s__<=> ((V__NUMBER1s__equal__mV__NUMBER2)s__or__ms__lessThan(V__NUMBER1,V__NUMBER2)))) )	Merge.kif 1934-1938	A quantity is less than or equal to another quantity if and only if the quantity is equal to the other quantity or the quantity is less than the other quantity
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 16311-16319	If college freshman is an attribute of a position and a human holds the position of the position in an organization, then there exists a time position such that the human is a student of the organization holds during the time position and the time position is less than 1 year duration(s)
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 16325-16336	If college junior is an attribute of a position and a human holds the position of the position in an organization, then there exists a time position such that the human is a student of the organization holds during the time position and the time position is greater than or equal to 2 year duration(s) and the time position is less than 3 year duration(s)
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 16342-16353	If college senior is an attribute of a position and a human holds the position of the position in an organization, then there exists a time position such that the human is a student of the organization holds during the time position and the time position is greater than or equal to 3 year duration(s) and the time position is less than 4 year duration(s)
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 16359-16370	If college sophomore is an attribute of a position and a human holds the position of the position in an organization, then there exists a time position such that the human is a student of the organization holds during the time position and the time position is greater than or equal to 1 year duration(s) and the time position is less than 2 year duration(s)
No TPTP formula. May not be expressible in strict first order.	Dining.kif 1102-1110	If probability of comfort food is an attribute of an entity provided that heart-healthy food is an attribute of the entity holds is a real number and probability of comfort food is an attribute of the entity provided that heart-healthy food is not an attribute of the entity holds is another real number, then the real number is less than the other real number
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 3583-3591	If an agent is a day phone of a symbolic string and a kind of day is an instance of day, then there exists a telephone such that the telephone is a phone number of the symbolic string and the agent possesses the telephone holds during the hour the symbolic string and the symbolic string is less than 18
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2800-2805	If a formula decreases likelihood of another formula and the probability of the other formula is equal to a real number and probability of the formula provided that the other formula holds is another real number, then the other real number is less than the real number
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 11171-11180	If the expected value of a kind of object is a real number an unit of measure(s) and the unit of measure is an instance of CompositeUnitOfMeasure, then the statement there exist an entity and the real numberUANTITY such that the entity is an instance of a kind of object and the measure of the entity is the real numberUANTITY the unit of measure(s) and the real numberUANTITY is less than the real number and .5 has the modal force of unlikely
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 11102-11111	If the minimum expected value of a kind of object is a real number an unit of measure(s) and the unit of measure is an instance of CompositeUnitOfMeasure, then the statement there exist an entity and the real numberUANTITY such that the entity is an instance of a kind of object and the measure of the entity is the real numberUANTITY the unit of measure(s) and the real numberUANTITY is less than the real number has the modal force of unlikely
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 11112-11123	If the minimum expected value of a kind of object is a real number an unit of measure(s) and a set or class is a subclass of NonCompositeUnitOfMeasure and the unit of measure is an instance of the set or class, then the statement there exist an entity, the real numberUANTITY and a third entity such that the entity is an instance of a kind of object and the measure of the entity is the real numberUANTITY the third entity(s) and the third entity is an instance of the set or class and the real numberUANTITY the third entity(s) is less than the real number the unit of measure(s) has the modal force of unlikely
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 11069-11077	If the minimum expected radius of a kind of object is a length measure and another object is an instance of a kind of object and sphere is an attribute of the other object, then the statement the radius of the other object is the length measureADIUS and the length measureADIUS is less than the length measure has the modal force of unlikely
( ! [V__N,V__A] : (s__instance(V__N,s__RealNumber)s__=>((s__instance(V__A,s__AcuteAngle)s__and__ms__angularMeasure(V__A,s__MeasureFn(V__N,s__AngularDegree))) s__=>s__lessThan(V__N,90))) )	Mid-level-ontology.kif 5181-5185	If a two dimensional angle is an instance of acute angle and a real number angular degree(s) is an angular measure of the two dimensional angle, then the real number is less than 90
No TPTP formula. May not be expressible in strict first order.	Dining.kif 729-752	If an agent is an instance of agent and a cognitive agent is a potential customer for the agent and the statement an entity is an instance of reserving and the entity ends up at the agent has the modal force of necessity and probability of there exists the entityES1 such that the entityES1 is an instance of reservation and the cognitive agent reserves the entityES1 and the agent fulfills the entityES1 provided that the agent is a customer of the cognitive agent holds is a real number and probability of there doesn't exist the entityES2 such that the entityES2 is an instance of reservation and the cognitive agent reserves the entityES2 and the agent fulfills the entityES2 provided that the agent is a customer of the cognitive agent holds is another real number, then the other real number is less than the real number
( ! [V__AIRPORT] : ((s__instance(V__AIRPORT,s__Airport)s__and__ms__attribute(V__AIRPORT,s__VeryShortRunwayAirport)) s__=>(s__exists__m[V__RUNWAY,V__LENGTH] : (s__instance(V__LENGTH,s__Quantity)s__and__m(s__instance(V__RUNWAY,s__Runway)s__and__ms__part(V__RUNWAY,V__AIRPORT) s__and__ms__length(V__RUNWAY,V__LENGTH) s__and__ms__lessThan(V__LENGTH,s__MeasureFn(914,s__Meter)))))) )	Transportation.kif 1365-1374	If an object is an instance of airport and very short runway airport is an attribute of the object, then there exist another object and a quantity such that the other object is an instance of runway and the other object is a part of the object and the length of the other object is the quantity and the quantity is less than 914 meter(s)
( ! [V__ELEV1,V__AREA] : (s__instance(V__ELEV1,s__LengthMeasure)s__=>((s__instance(V__AREA,s__GeographicArea)s__and__ms__geographicSubregion(s__ElevationLowPointFn(V__AREA) ,V__AREA) s__and__ms__elevation(s__ElevationLowPointFn(V__AREA) ,V__ELEV1)) s__=>(s__not__m(s__exists__m[V__OTHER,V__ELEV2] : (s__instance(V__OTHER,s__GeographicArea)s__and__ms__instance(V__ELEV2,s__LengthMeasure)s__and__m(s__geographicSubregion(V__OTHER,V__AREA) s__and__m(s__not__m(V__OTHERs__equal__ms__ElevationLowPointFn(V__AREA))) s__and__ms__elevation(V__OTHER,V__ELEV2) s__and__ms__lessThan(V__ELEV2,V__ELEV1))))))) )	Geography.kif 1881-1892	If a geographic area is an instance of geographic area and the elevation low point of the geographic area is a geographic subregion of the geographic area and a length measure is an elevation of the elevation low point of the geographic area, then there don't exist another geographic area and another length measure such that the other geographic area is a geographic subregion of the geographic area and the other geographic area is not equal to the elevation low point of the geographic area and the other length measure is an elevation of the other geographic area and the other length measure is less than the length measure
( ! [V__FRACTION,V__AREA,V__WEATHER] : (s__instance(V__FRACTION,s__NonnegativeRealNumber)s__=>((s__instance(V__AREA,s__GeographicArea)s__and__ms__instance(V__WEATHER,s__ClearWeather)s__and__ms__eventLocated(V__WEATHER,V__AREA) s__and__ms__cloudCoverFraction(V__AREA,V__FRACTION)) s__=>s__lessThan(V__FRACTION,0.3))) )	Weather.kif 504-510	If a region is an instance of geographic area and a process is an instance of clear weather and the process is located at 2 and a nonnegative real number is a cloud cover fraction of the region, then the nonnegative real number is less than 0.3
( ! [V__AREA,V__WEATHER] : ((s__instance(V__AREA,s__GeographicArea)s__and__ms__instance(V__WEATHER,s__ClearWeather)s__and__ms__eventLocated(V__WEATHER,V__AREA)) s__=>(s__exists__m[V__FRACTION] : (s__instance(V__FRACTION,s__NonnegativeRealNumber)s__and__m(s__cloudCoverFraction(V__AREA,V__FRACTION) s__and__ms__lessThan(V__FRACTION,0.3))))) )	Weather.kif 494-502	If a region is an instance of geographic area and a process is an instance of clear weather and the process is located at 2, then there exists a nonnegative real number such that the nonnegative real number is a cloud cover fraction of the region and the nonnegative real number is less than 0.3
( ! [V__BOTTOM,V__WIDTH2,V__WIDTH1,V__TOP,V__BOTTLE] : ((s__instance(V__BOTTOM,s__SelfConnectedObject)s__and__ms__instance(V__WIDTH2,s__Quantity)s__and__ms__instance(V__WIDTH1,s__Quantity)s__and__ms__instance(V__TOP,s__SelfConnectedObject)) s__=>((s__instance(V__BOTTLE,s__Bottle)s__and__ms__bottom(V__BOTTOM,V__BOTTLE) s__and__ms__top(V__TOP,V__BOTTLE) s__and__ms__width(V__BOTTOM,V__WIDTH1) s__and__ms__width(V__TOP,V__WIDTH2)) s__=>s__lessThan(V__WIDTH2,V__WIDTH1))) )	Mid-level-ontology.kif 5023-5030	If a self connected object is an instance of bottle and the bottom of the self connected object is another self connected object and the top of the self connected object is a third self connected object and the width of the other self connected object is a quantity and the width of the third self connected object is another quantity, then the other quantity is less than the quantity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 10920-10933	If a process is an instance of cooling and an entity is a patient of the process, then there exist another entity, a quantity and another quantity such that the other entity is an instance of temperature measure and the entity the other entity(s) is equal to the quantity holds during the beginning of the time of existence of the process and the entity the other entity(s) is equal to the other quantity holds during the end of the time of existence of the process and the other quantity is less than the quantity
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 1920-1928	If a computer process is an instance of data compression and a digital data is processed by the computer process and the digital data requires a quantity an entity(s) holds during immediately before the time of existence of the computer process and the digital data requires another quantity the entity(s) holds during immediately after the time of existence of the computer process, then the other quantity is less than the quantity
No TPTP formula. May not be expressible in strict first order.	Dining.kif 511-520	If a process is an instance of delivery service and the process ends up at an entity and a geographic area is the delivery area of an agent and probability of the entity is located at the geographic area provided that the agent is an agent of the process holds is a real number and probability of the entity is not located at the geographic area provided that the agent is an agent of the process holds is another real number, then the other real number is less than the real number

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement

( ! [V__NUMBER1,V__NUMBER2,V__GRAPH] :
   ((s__instance(V__NUMBER1,s__PositiveInteger)s__and__ms__instance(V__NUMBER2,s__PositiveInteger)s__and__ms__instance(V__GRAPH,s__Graph))
    s__=>(s__not__m(s__exists__m[V__PATH1,V__PATH2] :
       (s__instance(V__PATH1,s__GraphPath)s__and__ms__instance(V__PATH2,s__GraphPath)s__and__m(s__instance(V__PATH1,s__CutSetFn(V__GRAPH))
    s__and__ms__instance(V__PATH2,s__MinimalCutSetFn(V__GRAPH))
s__and__ms__pathLength(V__PATH1,V__NUMBER1)
s__and__ms__pathLength(V__PATH2,V__NUMBER2)
s__and__ms__lessThan(V__NUMBER1,V__NUMBER2))))))
)

Merge.kif 6230-6237

There don't exist a graph path and another graph path such that the graph path is an instance of the set of paths that partition a graph into two separate graphs and the other graph path is an instance of the set of minimal paths that partition the graph into two separate graphs and the length of the graph path is a positive integer and the length of the other graph path is another positive integer and the positive integer is less than the other positive integer

Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)

Sigma web home Suggested Upper Merged Ontology (SUMO) web home
Sigma version 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners

KB Term:			Term intersection

English Word: