equal - Sigma Knowledge base Browser

appearance as argument number 1

No TPTP formula. May not be expressible in strict first order.	Merge.kif 288-289
No TPTP formula. May not be expressible in strict first order.	Merge.kif 286-287
No TPTP formula. May not be expressible in strict first order.	Merge.kif 284-284	The number 1 argument of equal is an instance of entity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 285-285	The number 2 argument of equal is an instance of entity
s__instance(s__BinaryPredicate,s__SetOrClass)	Merge.kif 281-281	equal is an instance of binary predicate
s__instance(s__EquivalenceRelation,s__SetOrClass)	Merge.kif 282-282	equal is an instance of equivalence relation
s__instance(s__RelationExtendedToQuantities,s__SetOrClass)	Merge.kif 283-283	equal is an instance of relation extended to quantities

appearance as argument number 2

No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 297-297
No TPTP formula. May not be expressible in strict first order.	english_format.kif 181-181
No TPTP formula. May not be expressible in strict first order.	french_format.kif 171-171
No TPTP formula. May not be expressible in strict first order.	relations-it.txt 96-96
No TPTP formula. May not be expressible in strict first order.	portuguese_format.kif 123-123
No TPTP formula. May not be expressible in strict first order.	arabic_format.kif 116-116
No TPTP formula. May not be expressible in strict first order.	relations-cz.txt 179-179
No TPTP formula. May not be expressible in strict first order.	relations-de.txt 387-387
No TPTP formula. May not be expressible in strict first order.	relations-hindi.txt 136-136
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 205-205
No TPTP formula. May not be expressible in strict first order.	chinese_format.kif 298-298	"等于" is the printable form of equal in ChineseLanguage
No TPTP formula. May not be expressible in strict first order.	domainEnglishFormat.kif 4141-4141	"equal" is the printable form of equal in english language
No TPTP formula. May not be expressible in strict first order.	arabic_format.kif 566-566	"«مُسَاوٍ لـ»" is the printable form of equal in ar
No TPTP formula. May not be expressible in strict first order.	relations-tg.txt 206-206	"pareho" is the printable form of equal in tg

antecedent

( ! [V__NUMBER1,V__NUMBER2] : (((s__AbsoluteValueFn(V__NUMBER1) = V__NUMBER2) & s__instance(V__NUMBER1,s__RealNumber) & s__instance(V__NUMBER2,s__RealNumber)) <=> ((s__instance(V__NUMBER1,s__NonnegativeRealNumber) & (V__NUMBER1 = V__NUMBER2)) \| (s__instance(V__NUMBER1,s__NegativeRealNumber) & (V__NUMBER2 = minus(0,V__NUMBER1))))) )	Merge.kif 4894-4905	The absolute value of ?NUMBER1 is equal to ?NUMBER2 and ?NUMBER1 is an instance of real number and ?NUMBER2 is an instance of real number if and only if ?NUMBER1 is an instance of nonnegative real number and ?NUMBER1 is equal to ?NUMBER2 or ?NUMBER1 is an instance of negative real number and ?NUMBER2 is equal to (0 and ?NUMBER1)
( ! [V__Account,V__Agent,V__Asset] : ((s__instance(V__Account,s__FinancialAccount) & s__possesses(V__Agent,V__Asset) & (V__Account = s__AccountFn(V__Asset))) <=> s__accountHolder(V__Account,V__Agent)) )	FinancialOntology.kif 2252-2257	?Account is an instance of financial account and ?Agent possesses ?Asset and ?Account is equal to the account of ?Asset if and only if ?Agent holds account ?Account
( ! [V__UNIT,V__AMOUNT] : ((s__instance(V__UNIT,s__UnitOfMeasure) & (V__AMOUNT = s__MeasureFn(1,s__SquareUnitFn(V__UNIT)))) <=> (V__AMOUNT = times(s__MeasureFn(1,V__UNIT) ,s__MeasureFn(1,V__UNIT)))) )	Geography.kif 3748-3752	?UNIT is an instance of unit of measure and ?AMOUNT is equal to 1 the square unit of ?UNIT(s) if and only if ?AMOUNT is equal to 1 ?UNIT(s) and 1 ?UNIT(s)
( ! [V__AREA,V__YEAR,V__REALNUMBER,V__THOUSANDS,V__BIRTHCOUNT,V__BIRTH,V__INFANT] : ((s__BirthsPerThousandFn(V__AREA,s__YearFn(V__YEAR)) = V__REALNUMBER) <=> ((divide(s__PopulationFn(V__AREA) ,1000) = V__THOUSANDS) & (V__BIRTHCOUNT = s__CardinalityFn(s__KappaFn(V__BIRTH,'(s__instance(V__BIRTH,s__Birth) & s__experiencer(V__BIRTH,V__INFANT) & s__instance(V__INFANT,s__Human) & s__during(s__WhenFn(V__BIRTH),s__YearFn(V__YEAR)) & (s__WhereFn(V__BIRTH,s__WhenFn(V__BIRTH)) = V__AREA))'))) & (divide(V__BIRTHCOUNT,V__THOUSANDS) = V__REALNUMBER))) )	People.kif 104-117	The births per thousand of ?AREA and the year ?YEAR is equal to ?REALNUMBER if and only if the population of ?AREA and 1000 is equal to ?THOUSANDS and ?BIRTHCOUNT is equal to the number of instances in the class described by ?BIRTH and ?BIRTHCOUNT and ?THOUSANDS is equal to ?REALNUMBER
( ! [V__AREA,V__YEAR,V__REALNUMBER,V__THOUSANDS,V__DEATHCOUNT,V__DEATH,V__PERSON] : ((s__DeathsPerThousandFn(V__AREA,s__YearFn(V__YEAR)) = V__REALNUMBER) <=> ((divide(s__PopulationFn(V__AREA) ,1000) = V__THOUSANDS) & (V__DEATHCOUNT = s__CardinalityFn(s__KappaFn(V__DEATH,'(s__instance(V__DEATH,s__Death) & s__experiencer(V__DEATH,V__PERSON) & s__instance(V__PERSON,s__Human) & s__during(s__WhenFn(V__DEATH),s__YearFn(V__YEAR)) & (s__WhereFn(V__DEATH,s__WhenFn(V__DEATH)) = V__AREA))'))) & (divide(V__DEATHCOUNT,V__THOUSANDS) = V__REALNUMBER))) )	People.kif 138-151	The deaths per thousand of ?AREA and the year ?YEAR is equal to ?REALNUMBER if and only if the population of ?AREA and 1000 is equal to ?THOUSANDS and ?DEATHCOUNT is equal to the number of instances in the class described by ?DEATH and ?DEATHCOUNT and ?THOUSANDS is equal to ?REALNUMBER
( ! [V__AREA,V__YEAR,V__REALNUMBER,V__BIRTHCOUNT,V__BIRTH,V__INFANT,V__THOUSANDSOFBIRTHS,V__INFANTDEATHCOUNT,V__DEATH,V__AGE] : ((s__DeathsPerThousandLiveBirthsFn(V__AREA,s__YearFn(V__YEAR)) = V__REALNUMBER) <=> ((V__BIRTHCOUNT = s__CardinalityFn(s__KappaFn(V__BIRTH,'(s__instance(V__BIRTH,s__Birth) & s__experiencer(V__BIRTH,V__INFANT) & s__instance(V__INFANT,s__Human) & s__during(s__WhenFn(V__BIRTH),s__YearFn(V__YEAR)) & (s__WhereFn(V__BIRTH,s__WhenFn(V__BIRTH)) = V__AREA))'))) & (divide(V__BIRTHCOUNT,1000) = V__THOUSANDSOFBIRTHS) & (V__INFANTDEATHCOUNT = s__CardinalityFn(s__KappaFn(V__DEATH,'(s__instance(V__DEATH,s__Death) & s__experiencer(V__DEATH,V__INFANT) & s__instance(V__INFANT,s__Human) & s__age(V__INFANT,s__MeasureFn(V__AGE,s__YearDuration)) & less(V__AGE,1) & s__during(s__WhenFn(V__DEATH),s__YearFn(V__YEAR)) & (s__WhereFn(V__DEATH,s__WhenFn(V__DEATH)) = V__AREA))'))) & (divide(V__INFANTDEATHCOUNT,V__THOUSANDSOFBIRTHS) = V__REALNUMBER))) )	People.kif 253-277	The deaths per thousand live births of ?AREA and the year ?YEAR is equal to ?REALNUMBER if and only if ?BIRTHCOUNT is equal to the number of instances in the class described by ?BIRTH and ?BIRTHCOUNT and 1000 is equal to ?THOUSANDSOFBIRTHS and ?INFANTDEATHCOUNT is equal to the number of instances in the class described by ?DEATH and ?INFANTDEATHCOUNT and ?THOUSANDSOFBIRTHS is equal to ?REALNUMBER
( ! [V__AREA,V__YEAR,V__REALNUMBER,V__COUNT,V__LIFEEXPECTANCYAGE,V__BIRTH,V__INDIVIDUAL,V__DEATH] : ((s__FemaleLifeExpectancyAtBirthFn(V__AREA,s__YearFn(V__YEAR)) = V__REALNUMBER) <=> (? [V__LIST] : (s__instance(V__LIST,s__List) & s__instance(s__ListLengthFn(V__LIST) ,V__COUNT) & (! [V__LISTITEM] : (s__inList(V__LISTITEM,V__LIST) => (s__instance(V__LISTITEM,V__LIFEEXPECTANCYAGE) & (~ (? [V__NUMBER] : (s__instance(V__NUMBER,V__LIFEEXPECTANCYAGE) & (~ s__inList(V__NUMBER,V__LIST))))) & (V__COUNT = s__CardinalityFn(s__KappaFn(V__LIFEEXPECTANCYAGE,'(s__instance(V__BIRTH,s__Birth) & s__experiencer(V__BIRTH,V__INDIVIDUAL) & s__instance(V__INDIVIDUAL,s__Human) & s__attribute(V__INDIVIDUAL,s__Female) & s__during(s__WhenFn(V__BIRTH),s__YearFn(V__YEAR)) & (s__WhereFn(V__BIRTH,s__WhenFn(V__BIRTH)) = V__AREA) & s__instance(V__DEATH,s__Death) & s__experiencer(V__DEATH,V__INDIVIDUAL) & s__holdsDuring(s__WhenFn(V__DEATH),s__age(V__INDIVIDUAL,s__MeasureFn(V__LIFEEXPECTANCYAGE,s__YearDuration))))')))))) & s__average(V__LIST,V__REALNUMBER)))) )	People.kif 411-442	The female life expectancy at birth of ?AREA and the year ?YEAR is equal to ?REALNUMBER if and only if there exists ?LIST such that ?LIST is an instance of list and length of ?LIST is an instance of ?COUNT and for all ?LISTITEM if ?LISTITEM is a member of ?LIST, then ?LISTITEM is an instance of ?LIFEEXPECTANCYAGE and there doesn't exist ?NUMBER such that ?NUMBER is an instance of ?LIFEEXPECTANCYAGE and ?NUMBER is not a member of ?LIST and ?COUNT is equal to the number of instances in the class described by ?LIFEEXPECTANCYAGE and ?REALNUMBER is an average of ?LIST
( ! [V__LIST,V__ITEM] : ((s__LastFn(V__LIST) = V__ITEM) <=> (? [V__NUMBER] : ((s__ListLengthFn(V__LIST) = V__NUMBER) & (s__ListOrderFn(V__LIST,V__NUMBER) = V__ITEM)))) )	Mid-level-ontology.kif 6342-6347	The last of ?LIST is equal to ?ITEM if and only if there exists ?NUMBER such that length of ?LIST is equal to ?NUMBER and ?NUMBERth element of ?LIST is equal to ?ITEM
( ! [V__AREA,V__YEAR,V__REALNUMBER,V__COUNT,V__LIFEEXPECTANCYAGE,V__BIRTH,V__INDIVIDUAL,V__DEATH] : ((s__LifeExpectancyAtBirthFn(V__AREA,s__YearFn(V__YEAR)) = V__REALNUMBER) <=> (? [V__LIST] : (s__instance(V__LIST,s__List) & s__instance(s__ListLengthFn(V__LIST) ,V__COUNT) & (! [V__LISTITEM] : (s__inList(V__LISTITEM,V__LIST) => (s__instance(V__LISTITEM,V__LIFEEXPECTANCYAGE) & (~ (? [V__NUMBER] : (s__instance(V__NUMBER,V__LIFEEXPECTANCYAGE) & (~ s__inList(V__NUMBER,V__LIST))))) & (V__COUNT = s__CardinalityFn(s__KappaFn(V__LIFEEXPECTANCYAGE,'(s__instance(V__BIRTH,s__Birth) & s__experiencer(V__BIRTH,V__INDIVIDUAL) & s__instance(V__INDIVIDUAL,s__Human) & s__during(s__WhenFn(V__BIRTH),s__YearFn(V__YEAR)) & (s__WhereFn(V__BIRTH,s__WhenFn(V__BIRTH)) = V__AREA) & s__instance(V__DEATH,s__Death) & s__experiencer(V__DEATH,V__INDIVIDUAL) & s__holdsDuring(s__WhenFn(V__DEATH),s__age(V__INDIVIDUAL,s__MeasureFn(V__LIFEEXPECTANCYAGE,s__YearDuration))))')))))) & s__average(V__LIST,V__REALNUMBER)))) )	People.kif 323-353	The life expectancy at birth of ?AREA and the year ?YEAR is equal to ?REALNUMBER if and only if there exists ?LIST such that ?LIST is an instance of list and length of ?LIST is an instance of ?COUNT and for all ?LISTITEM if ?LISTITEM is a member of ?LIST, then ?LISTITEM is an instance of ?LIFEEXPECTANCYAGE and there doesn't exist ?NUMBER such that ?NUMBER is an instance of ?LIFEEXPECTANCYAGE and ?NUMBER is not a member of ?LIST and ?COUNT is equal to the number of instances in the class described by ?LIFEEXPECTANCYAGE and ?REALNUMBER is an average of ?LIST
( ! [V__AREA,V__YEAR,V__REALNUMBER,V__COUNT,V__LIFEEXPECTANCYAGE,V__BIRTH,V__INDIVIDUAL,V__DEATH] : ((s__MaleLifeExpectancyAtBirthFn(V__AREA,s__YearFn(V__YEAR)) = V__REALNUMBER) <=> (? [V__LIST] : (s__instance(V__LIST,s__List) & s__instance(s__ListLengthFn(V__LIST) ,V__COUNT) & (! [V__LISTITEM] : (s__inList(V__LISTITEM,V__LIST) => (s__instance(V__LISTITEM,V__LIFEEXPECTANCYAGE) & (~ (? [V__NUMBER] : (s__instance(V__NUMBER,V__LIFEEXPECTANCYAGE) & (~ s__inList(V__NUMBER,V__LIST))))) & (V__COUNT = s__CardinalityFn(s__KappaFn(V__LIFEEXPECTANCYAGE,'(s__instance(V__BIRTH,s__Birth) & s__experiencer(V__BIRTH,V__INDIVIDUAL) & s__instance(V__INDIVIDUAL,s__Human) & s__attribute(V__INDIVIDUAL,s__Male) & s__during(s__WhenFn(V__BIRTH),s__YearFn(V__YEAR)) & (s__WhereFn(V__BIRTH,s__WhenFn(V__BIRTH)) = V__AREA) & s__instance(V__DEATH,s__Death) & s__experiencer(V__DEATH,V__INDIVIDUAL) & s__holdsDuring(s__WhenFn(V__DEATH),s__age(V__INDIVIDUAL,s__MeasureFn(V__LIFEEXPECTANCYAGE,s__YearDuration))))')))))) & s__average(V__LIST,V__REALNUMBER)))) )	People.kif 367-398	The male life expectancy at birth of ?AREA and the year ?YEAR is equal to ?REALNUMBER if and only if there exists ?LIST such that ?LIST is an instance of list and length of ?LIST is an instance of ?COUNT and for all ?LISTITEM if ?LISTITEM is a member of ?LIST, then ?LISTITEM is an instance of ?LIFEEXPECTANCYAGE and there doesn't exist ?NUMBER such that ?NUMBER is an instance of ?LIFEEXPECTANCYAGE and ?NUMBER is not a member of ?LIST and ?COUNT is equal to the number of instances in the class described by ?LIFEEXPECTANCYAGE and ?REALNUMBER is an average of ?LIST
( ! [V__AREA,V__REALNUMBER,V__MALECOUNT,V__MALE,V__FEMALECOUNT,V__FEMALE] : ((s__MaleToFemaleRatioFn(V__AREA) = V__REALNUMBER) <=> ((V__MALECOUNT = s__CardinalityFn(s__KappaFn(V__MALE,'(s__instance(V__MALE,s__Human) & s__attribute(V__MALE,s__Male) & s__inhabits(V__MALE,V__AREA))'))) & (V__FEMALECOUNT = s__CardinalityFn(s__KappaFn(V__FEMALE,'(s__instance(V__FEMALE,s__Human) & s__attribute(V__FEMALE,s__Female) & s__inhabits(V__FEMALE,V__AREA))'))) & (divide(V__MALECOUNT,V__FEMALECOUNT) = V__REALNUMBER))) )	People.kif 221-238	The male to female ratio of ?AREA is equal to ?REALNUMBER if and only if ?MALECOUNT is equal to the number of instances in the class described by ?MALE and ?FEMALECOUNT is equal to the number of instances in the class described by ?FEMALE and ?MALECOUNT and ?FEMALECOUNT is equal to ?REALNUMBER
( ! [V__AREA,V__YEAR,V__REALNUMBER,V__PREVIOUSYEAR,V__POPULATION,V__THOUSANDS,V__IMMIGRATION,V__PERSON,V__EMMIGRATION,V__MIGRATIONCOUNT] : ((s__MigrantsPerThousandFn(V__AREA,s__YearFn(V__YEAR)) = V__REALNUMBER) <=> ((minus(V__YEAR,V__PREVIOUSYEAR) = 1) & s__holdsDuring(s__YearFn(V__YEAR) ,'(s__PopulationFn(V__AREA) = V__POPULATION)') & (divide(V__POPULATION,1000) = V__THOUSANDS) & (V__IMMIGRATION = s__CardinalityFn(s__KappaFn(V__PERSON,'(s__instance(V__PERSON,s__Human) & s__holdsDuring(s__YearFn(V__PREVIOUSYEAR),(~ s__inhabits(V__PERSON,V__AREA))) & s__holdsDuring(s__YearFn(V__YEAR),s__inhabits(V__PERSON,V__AREA)))'))) & (V__EMMIGRATION = s__CardinalityFn(s__KappaFn(V__PERSON,'(s__instance(V__PERSON,s__Human) & s__holdsDuring(s__YearFn(V__PREVIOUSYEAR),s__inhabits(V__PERSON,V__AREA)) & s__holdsDuring(s__YearFn(V__YEAR),(~ s__inhabits(V__PERSON,V__AREA))))'))) & (minus(V__IMMIGRATION,V__EMMIGRATION) = V__MIGRATIONCOUNT) & (divide(V__MIGRATIONCOUNT,V__THOUSANDS) = V__REALNUMBER))) )	People.kif 174-202	The migrants per thousand of ?AREA and the year ?YEAR is equal to ?REALNUMBER if and only if (?YEAR and ?PREVIOUSYEAR) is equal to 1 and the population of ?AREA is equal to ?POPULATION holds during the year ?YEAR and ?POPULATION and 1000 is equal to ?THOUSANDS and ?IMMIGRATION is equal to the number of instances in the class described by ?PERSON and ?EMMIGRATION is equal to the number of instances in the class described by ?PERSON and (?IMMIGRATION and ?EMMIGRATION) is equal to ?MIGRATIONCOUNT and ?MIGRATIONCOUNT and ?THOUSANDS is equal to ?REALNUMBER
( ! [V__AREA,V__YEAR,V__ADJUSTEDPERCENT,V__PREVIOUSYEAR,V__POPULATION,V__PREVIOUSPOPULATION,V__PERCENT] : ((s__PopulationGrowthFn(V__AREA,s__YearFn(V__YEAR)) = V__ADJUSTEDPERCENT) <=> ((minus(V__YEAR,V__PREVIOUSYEAR) = 1) & s__holdsDuring(s__YearFn(V__YEAR) ,'(s__PopulationFn(V__AREA) = V__POPULATION)') & s__holdsDuring(s__YearFn(V__PREVIOUSYEAR) ,'(s__PopulationFn(V__AREA) = V__PREVIOUSPOPULATION)') & (divide(V__POPULATION,V__PREVIOUSPOPULATION) = V__PERCENT) & (minus(V__PERCENT,1) = V__ADJUSTEDPERCENT))) )	People.kif 77-86	The population growth of ?AREA and the year ?YEAR is equal to ?ADJUSTEDPERCENT if and only if (?YEAR and ?PREVIOUSYEAR) is equal to 1 and the population of ?AREA is equal to ?POPULATION holds during the year ?YEAR and the population of ?AREA is equal to ?PREVIOUSPOPULATION holds during the year ?PREVIOUSYEAR and ?POPULATION and ?PREVIOUSPOPULATION is equal to ?PERCENT and (?PERCENT and 1) is equal to ?ADJUSTEDPERCENT
( ! [V__NUMBER1,V__NUMBER2,V__NUMBER] : ((s__RemainderFn(V__NUMBER1,V__NUMBER2) = V__NUMBER) <=> (plus(times(s__FloorFn(divide(V__NUMBER1,V__NUMBER2)) ,V__NUMBER2) ,V__NUMBER) = V__NUMBER1)) )	Merge.kif 5226-5228	?NUMBER1 Mod ?NUMBER2 is equal to ?NUMBER if and only if (the largest integer less than or equal to ?NUMBER1 and ?NUMBER2 and ?NUMBER2 and ?NUMBER) is equal to ?NUMBER1
( ! [V__PERSON,V__AMOUNT] : ((s__WealthFn(V__PERSON) = V__AMOUNT) <=> s__monetaryValue(s__PropertyFn(V__PERSON) ,V__AMOUNT)) )	Merge.kif 7963-7965	Value of belongings of ?PERSON is equal to ?AMOUNT if and only if value of belongings of ?PERSON is ?AMOUNT
( ! [V__THING,V__TIME,V__REGION] : ((s__WhereFn(V__THING,V__TIME) = V__REGION) <=> s__holdsDuring(V__TIME,'s__exactlyLocated(V__THING,V__REGION)')) )	Merge.kif 4339-4341	The place where ?THING was at ?TIME is equal to ?REGION if and only if ?THING is exactly located in ?REGION holds during ?TIME
( ! [V__Agent,V__Activity,V__ATIncome] : ((? [V__Income,V__Tax,V__TaxAmount] : (s__incomeEarned(V__Agent,V__Income,V__Activity) & s__amountCharged(V__Tax,V__TaxAmount) & s__causes(V__Activity,V__Tax) & (V__ATIncome = minus(V__Income,V__TaxAmount)))) <=> s__afterTaxIncome(V__Agent,V__ATIncome,V__Activity)) )	FinancialOntology.kif 3222-3229	There exist ?Income, ?Tax and ?TaxAmount such that ?Agent income earned ?Income for ?Activity and ?TaxAmount is the amount charged in ?Tax and ?Activity causes ?Tax and ?ATIncome is equal to (?Income and ?TaxAmount) if and only if the after tax income derived by ?Agent from ?Activity is ?ATIncome
( ! [V__Option,V__Time] : ((? [V__Stock,V__StockPrice,V__StrikePrice] : (s__instance(V__Option,s__Option) & s__underlier(V__Option,V__Stock) & s__price(V__Stock,V__StockPrice,V__Time) & s__strikePrice(V__Option,V__StrikePrice) & (V__StockPrice = V__StrikePrice))) <=> s__atTheMoney(V__Option,V__Time)) )	FinancialOntology.kif 2948-2956	There exist ?Stock, ?StockPrice and ?StrikePrice such that ?Option is an instance of option and ?Stock is an underlier of ?Option and ?Stock price ?StockPrice for ?Time and ?StrikePrice is a strike price of ?Option and ?StockPrice is equal to ?StrikePrice if and only if ?Time is an at the money of ?Option
( ! [V__PROP,V__ATTR,V__AGREEMENT,V__AGENT] : ((s__agreementClause(V__PROP,V__ATTR,V__AGREEMENT,V__AGENT) & ((V__ATTR = s__Obligation) \| (V__ATTR = s__Promise))) => s__modalAttribute('(? [V__PROC] : (s__realization(V__PROC,V__PROP) & s__agent(V__PROC,V__AGENT)))',s__Likely)) )	Mid-level-ontology.kif 11422-11432	If ?AGENT has the responsibility to make ?PROP ?ATTR in ?AGREEMENT and ?ATTR is equal to obligation or ?ATTR is equal to promise, then the statement there exists ?PROC such that ?PROC expresses the content of ?PROP and ?AGENT is an agent of ?PROC has the modal force of likely
( ! [V__REGION,V__FRACTION,V__TOTAL,V__UNIT,V__AMOUNT] : ((s__arableLandArea(V__REGION,V__FRACTION) & greatereq(V__FRACTION,0) & s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT)) & s__instance(V__UNIT,s__UnitOfArea) & (V__AMOUNT = s__MeasureFn(times(V__FRACTION,V__TOTAL) ,V__UNIT))) => s__arableLandArea(V__REGION,V__AMOUNT)) )	Geography.kif 2028-2035	If ?FRACTION is an arable land area of ?REGION and ?FRACTION is greater than or equal to 0 and ?TOTAL ?UNIT(s) is a total area of ?REGION and ?UNIT is an instance of UnitOfArea and ?AMOUNT is equal to ?FRACTION and ?TOTAL ?UNIT(s), then ?AMOUNT is an arable land area of ?REGION
( ! [V__REGION,V__FRACTION,V__TOTAL,V__AMOUNT] : ((s__arableLandArea(V__REGION,V__FRACTION) & greatereq(V__FRACTION,0) & s__totalArea(V__REGION,V__TOTAL) & s__instance(V__TOTAL,s__AreaMeasure) & (V__AMOUNT = times(V__FRACTION,V__TOTAL))) => s__arableLandArea(V__REGION,V__AMOUNT)) )	Geography.kif 2019-2026	If ?FRACTION is an arable land area of ?REGION and ?FRACTION is greater than or equal to 0 and ?TOTAL is a total area of ?REGION and ?TOTAL is an instance of area measure and ?AMOUNT is equal to ?FRACTION and ?TOTAL, then ?AMOUNT is an arable land area of ?REGION
( ! [V__H,V__W,V__Y,V__C] : ((s__attribute(V__H,s__Muslim) & (s__WealthFn(V__H) = V__W)) => s__modalAttribute('(? [V__Z,V__T] : (s__instance(V__Z,s__Zakat) & s__instance(V__Y,s__Year) & s__during(V__Y,s__WhenFn(V__H)) & s__holdsDuring(V__Y,s__attribute(V__H,s__FullyFormed)) & s__agent(V__Z,V__H) & s__patient(V__Z,V__T) & s__monetaryValue(V__T,V__C) & greater(V__C,times(V__W,0.025))))',s__Obligation)) )	ArabicCulture.kif 193-210	If muslim is an attribute of ?H and value of belongings of ?H is equal to ?W, then the statement there exist ?Z and ?T such that ?Z is an instance of zakat and ?Y is an instance of year and ?Y takes place during the time of existence of ?H and fully formed is an attribute of ?H holds during ?Y and ?H is an agent of ?Z and ?T is a patient of ?Z and value of ?T is ?C and ?C is greater than ?W and 0.025 has the modal force of obligation
( ! [V__A3,V__CURRENCY,V__A2,V__AREA] : ((s__codeMapping(s__ISO_4217_A,V__A3,V__CURRENCY) & s__codeMapping(s__ISO_3166_1_alpha_2,V__A2,V__AREA) & s__subclass(V__AREA,s__GeopoliticalArea) & (V__A2 = s__SubstringFn(V__A3,0,2))) => s__currencyType(V__AREA,V__CURRENCY)) )	Media.kif 2859-2865	If ?A3 in ISO-4217-A denotes ?CURRENCY and ?A2 in ISO-3166-1-alpha-2 denotes ?AREA and ?AREA is a subclass of geopolitical area and ?A2 is equal to the sub-string of ?A3 from 0 to 2, then ?CURRENCY is a currency type of ?AREA
( ! [V__EXPERIMENT,V__CONFIDENCE,V__EXPERIMENTING,V__FORMULA] : ((s__confidenceInterval(V__EXPERIMENT,V__CONFIDENCE) & s__instance(V__EXPERIMENT,V__EXPERIMENTING) & s__instance(V__FORMULA,s__Formula) & s__patient(V__EXPERIMENT,V__FORMULA) & (V__CONFIDENCE = 100)) => s__truth(V__FORMULA,'$false__m')) )	UXExperimentalTerms.kif 681-688	If ?CONFIDENCE is the confidence in ?EXPERIMENT and ?EXPERIMENT is an instance of ?EXPERIMENTING and ?FORMULA is an instance of formula and ?FORMULA is a patient of ?EXPERIMENT and ?CONFIDENCE is equal to 100, then ?FORMULA is false
( ! [V__EXPERIMENT,V__CONFIDENCE,V__EXPERIMENTING,V__FORMULA] : ((s__confidenceInterval(V__EXPERIMENT,V__CONFIDENCE) & s__instance(V__EXPERIMENT,V__EXPERIMENTING) & s__instance(V__FORMULA,s__Formula) & s__patient(V__EXPERIMENT,V__FORMULA) & (V__CONFIDENCE = 100)) => s__truth(V__FORMULA,'$true__m')) )	UXExperimentalTerms.kif 672-679	If ?CONFIDENCE is the confidence in ?EXPERIMENT and ?EXPERIMENT is an instance of ?EXPERIMENTING and ?FORMULA is an instance of formula and ?FORMULA is a patient of ?EXPERIMENT and ?CONFIDENCE is equal to 100, then ?FORMULA is true

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

consequent

( ! [V__NUMBER1,V__NUMBER2] : (((s__AbsoluteValueFn(V__NUMBER1) = V__NUMBER2) & s__instance(V__NUMBER1,s__RealNumber) & s__instance(V__NUMBER2,s__RealNumber)) <=> ((s__instance(V__NUMBER1,s__NonnegativeRealNumber) & (V__NUMBER1 = V__NUMBER2)) \| (s__instance(V__NUMBER1,s__NegativeRealNumber) & (V__NUMBER2 = minus(0,V__NUMBER1))))) )	Merge.kif 4894-4905	The absolute value of ?NUMBER1 is equal to ?NUMBER2 and ?NUMBER1 is an instance of real number and ?NUMBER2 is an instance of real number if and only if ?NUMBER1 is an instance of nonnegative real number and ?NUMBER1 is equal to ?NUMBER2 or ?NUMBER1 is an instance of negative real number and ?NUMBER2 is equal to (0 and ?NUMBER1)
( ! [V__ROW1] : ((s__instance(s__parent__m,s__TotalValuedRelation) & s__instance(s__parent__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__parent__m,s__Relation) & s__valence(s__parent__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__parent__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__parent(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__protonNumber__m,s__TotalValuedRelation) & s__instance(s__protonNumber__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__protonNumber__m,s__Relation) & s__valence(s__protonNumber__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__protonNumber__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__protonNumber(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__lineMeasure__m,s__TotalValuedRelation) & s__instance(s__lineMeasure__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__lineMeasure__m,s__Relation) & s__valence(s__lineMeasure__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__lineMeasure__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__lineMeasure(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__earlier__m,s__TotalValuedRelation) & s__instance(s__earlier__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__earlier__m,s__Relation) & s__valence(s__earlier__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__earlier__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__earlier(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__conclusion__m,s__TotalValuedRelation) & s__instance(s__conclusion__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__conclusion__m,s__Relation) & s__valence(s__conclusion__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__conclusion__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__conclusion(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__coordinates__m,s__TotalValuedRelation) & s__instance(s__coordinates__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__coordinates__m,s__Relation) & s__valence(s__coordinates__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__coordinates__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__coordinates(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subCollection__m,s__TotalValuedRelation) & s__instance(s__subCollection__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subCollection__m,s__Relation) & s__valence(s__subCollection__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subCollection__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subCollection(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__meetsTemporally__m,s__TotalValuedRelation) & s__instance(s__meetsTemporally__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__meetsTemporally__m,s__Relation) & s__valence(s__meetsTemporally__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__meetsTemporally__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__meetsTemporally(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subrelation__m,s__TotalValuedRelation) & s__instance(s__subrelation__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subrelation__m,s__Relation) & s__valence(s__subrelation__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subrelation__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subrelation(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(greater__m,s__TotalValuedRelation) & s__instance(greater__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(greater__m,s__Relation) & s__valence(greater__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(greater__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : greater(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subAttribute__m,s__TotalValuedRelation) & s__instance(s__subAttribute__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subAttribute__m,s__Relation) & s__valence(s__subAttribute__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subAttribute__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subAttribute(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subclass__m,s__TotalValuedRelation) & s__instance(s__subclass__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subclass__m,s__Relation) & s__valence(s__subclass__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subclass__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subclass(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__larger__m,s__TotalValuedRelation) & s__instance(s__larger__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__larger__m,s__Relation) & s__valence(s__larger__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__larger__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__larger(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__maximumPayloadCapacity__m,s__TotalValuedRelation) & s__instance(s__maximumPayloadCapacity__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__maximumPayloadCapacity__m,s__Relation) & s__valence(s__maximumPayloadCapacity__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__maximumPayloadCapacity__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__maximumPayloadCapacity(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(lesseq__m,s__TotalValuedRelation) & s__instance(lesseq__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(lesseq__m,s__Relation) & s__valence(lesseq__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(lesseq__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : lesseq(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__partlyLocated__m,s__TotalValuedRelation) & s__instance(s__partlyLocated__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__partlyLocated__m,s__Relation) & s__valence(s__partlyLocated__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__partlyLocated__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__partlyLocated(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(greatereq__m,s__TotalValuedRelation) & s__instance(greatereq__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(greatereq__m,s__Relation) & s__valence(greatereq__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(greatereq__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : greatereq(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__moves__m,s__TotalValuedRelation) & s__instance(s__moves__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__moves__m,s__Relation) & s__valence(s__moves__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__moves__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__moves(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__beforeOrEqual__m,s__TotalValuedRelation) & s__instance(s__beforeOrEqual__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__beforeOrEqual__m,s__Relation) & s__valence(s__beforeOrEqual__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__beforeOrEqual__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__beforeOrEqual(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__eventLocated__m,s__TotalValuedRelation) & s__instance(s__eventLocated__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__eventLocated__m,s__Relation) & s__valence(s__eventLocated__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__eventLocated__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__eventLocated(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__smaller__m,s__TotalValuedRelation) & s__instance(s__smaller__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__smaller__m,s__Relation) & s__valence(s__smaller__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__smaller__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__smaller(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__diameter__m,s__TotalValuedRelation) & s__instance(s__diameter__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__diameter__m,s__Relation) & s__valence(s__diameter__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__diameter__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__diameter(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__electronNumber__m,s__TotalValuedRelation) & s__instance(s__electronNumber__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__electronNumber__m,s__Relation) & s__valence(s__electronNumber__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__electronNumber__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__electronNumber(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__personTransportCapability__m,s__TotalValuedRelation) & s__instance(s__personTransportCapability__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__personTransportCapability__m,s__Relation) & s__valence(s__personTransportCapability__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__personTransportCapability__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__personTransportCapability(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__abstractPart__m,s__TotalValuedRelation) & s__instance(s__abstractPart__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__abstractPart__m,s__Relation) & s__valence(s__abstractPart__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__abstractPart__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__abstractPart(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__transactionAmount__m,s__TotalValuedRelation) & s__instance(s__transactionAmount__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__transactionAmount__m,s__Relation) & s__valence(s__transactionAmount__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__transactionAmount__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__transactionAmount(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__time__m,s__TotalValuedRelation) & s__instance(s__time__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__time__m,s__Relation) & s__valence(s__time__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__time__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__time(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__caliber__m,s__TotalValuedRelation) & s__instance(s__caliber__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__caliber__m,s__Relation) & s__valence(s__caliber__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__caliber__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__caliber(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__graphPart__m,s__TotalValuedRelation) & s__instance(s__graphPart__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__graphPart__m,s__Relation) & s__valence(s__graphPart__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__graphPart__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__graphPart(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__geometricPart__m,s__TotalValuedRelation) & s__instance(s__geometricPart__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__geometricPart__m,s__Relation) & s__valence(s__geometricPart__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__geometricPart__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__geometricPart(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__changesLocation__m,s__TotalValuedRelation) & s__instance(s__changesLocation__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__changesLocation__m,s__Relation) & s__valence(s__changesLocation__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__changesLocation__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__changesLocation(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__temporalPart__m,s__TotalValuedRelation) & s__instance(s__temporalPart__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__temporalPart__m,s__Relation) & s__valence(s__temporalPart__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__temporalPart__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__temporalPart(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__path__m,s__TotalValuedRelation) & s__instance(s__path__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__path__m,s__Relation) & s__valence(s__path__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__path__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__path(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__premise__m,s__TotalValuedRelation) & s__instance(s__premise__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__premise__m,s__Relation) & s__valence(s__premise__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__premise__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__premise(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subsumesContentClass__m,s__TotalValuedRelation) & s__instance(s__subsumesContentClass__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subsumesContentClass__m,s__Relation) & s__valence(s__subsumesContentClass__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subsumesContentClass__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subsumesContentClass(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subProcess__m,s__TotalValuedRelation) & s__instance(s__subProcess__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subProcess__m,s__Relation) & s__valence(s__subProcess__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subProcess__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subProcess(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__radius__m,s__TotalValuedRelation) & s__instance(s__radius__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__radius__m,s__Relation) & s__valence(s__radius__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__radius__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__radius(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subsumesContentInstance__m,s__TotalValuedRelation) & s__instance(s__subsumesContentInstance__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subsumesContentInstance__m,s__Relation) & s__valence(s__subsumesContentInstance__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subsumesContentInstance__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subsumesContentInstance(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__contestParticipant__m,s__TotalValuedRelation) & s__instance(s__contestParticipant__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__contestParticipant__m,s__Relation) & s__valence(s__contestParticipant__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__contestParticipant__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__contestParticipant(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__stringLength__m,s__TotalValuedRelation) & s__instance(s__stringLength__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__stringLength__m,s__Relation) & s__valence(s__stringLength__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__stringLength__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__stringLength(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subList__m,s__TotalValuedRelation) & s__instance(s__subList__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subList__m,s__Relation) & s__valence(s__subList__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subList__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subList(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__angularMeasure__m,s__TotalValuedRelation) & s__instance(s__angularMeasure__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__angularMeasure__m,s__Relation) & s__valence(s__angularMeasure__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__angularMeasure__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__angularMeasure(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subLanguage__m,s__TotalValuedRelation) & s__instance(s__subLanguage__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subLanguage__m,s__Relation) & s__valence(s__subLanguage__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subLanguage__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subLanguage(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__duration__m,s__TotalValuedRelation) & s__instance(s__duration__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__duration__m,s__Relation) & s__valence(s__duration__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__duration__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__duration(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__initialList__m,s__TotalValuedRelation) & s__instance(s__initialList__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__initialList__m,s__Relation) & s__valence(s__initialList__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__initialList__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__initialList(V__ROW1,V__ITEM)))))) ) ( ! [V__ROW1] : ((s__instance(s__subString__m,s__TotalValuedRelation) & s__instance(s__subString__m,s__Predicate)) <=> (? [V__VALENCE] : (s__instance(s__subString__m,s__Relation) & s__valence(s__subString__m,V__VALENCE) & ((! [V__NUMBER,V__ELEMENT,V__CLASS] : ((less(V__NUMBER,V__VALENCE) & s__domain(s__subString__m,V__NUMBER,V__CLASS) & (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1) ,V__NUMBER))) => s__instance(V__ELEMENT,V__CLASS))) => (? [V__ITEM] : s__subString(V__ROW1,V__ITEM)))))) )	Merge.kif 2308-2325	?REL is an instance of total valued relation and ?REL is an instance of predicate if and only if there exists ?VALENCE such that ?REL is an instance of relation and ?REL %&has ?VALENCE argument(s) and if for all ?NUMBER, ?ELEMENT and ?CLASS if ?NUMBER is less than ?VALENCE and the number ?NUMBER argument of ?REL is an instance of ?CLASS and ?ELEMENT is equal to ?NUMBERth element of (@ROW), then ?ELEMENT is an instance of ?CLASS , then there exists ?ITEM such that ?REL @ROW and ?ITEM
( ! [V__UNIT,V__AMOUNT] : ((s__instance(V__UNIT,s__UnitOfMeasure) & (V__AMOUNT = s__MeasureFn(1,s__SquareUnitFn(V__UNIT)))) <=> (V__AMOUNT = times(s__MeasureFn(1,V__UNIT) ,s__MeasureFn(1,V__UNIT)))) )	Geography.kif 3748-3752	?UNIT is an instance of unit of measure and ?AMOUNT is equal to 1 the square unit of ?UNIT(s) if and only if ?AMOUNT is equal to 1 ?UNIT(s) and 1 ?UNIT(s)
( ! [V__MUSIC] : (s__attribute(V__MUSIC,s__PolyphonicMusic) <=> (? [V__PART1,V__PART2] : (s__instance(V__MUSIC,s__MakingMusic) & s__instance(V__PART1,s__MakingMusic) & s__instance(V__PART2,s__MakingMusic) & s__subProcess(V__PART1,V__MUSIC) & s__subProcess(V__PART2,V__MUSIC) & (~ (V__PART1 = V__PART2)) & s__cooccur(V__PART1,V__MUSIC) & s__cooccur(V__PART2,V__MUSIC)))) )	Mid-level-ontology.kif 927-938	Polyphonic music is an attribute of ?MUSIC if and only if there exist ?PART1 and ?PART2 such that ?MUSIC is an instance of making music and ?PART1 is an instance of making music and ?PART2 is an instance of making music and ?PART1 is a subprocess of ?MUSIC and ?PART2 is a subprocess of ?MUSIC and ?PART1 is not equal to ?PART2 and ?PART1 occurs at the same time as ?MUSIC and ?PART2 occurs at the same time as ?MUSIC
( ! [V__LIST1,V__AVERAGE,V__LASTPLACE] : (s__average(V__LIST1,V__AVERAGE) <=> (? [V__LIST2] : ((s__ListLengthFn(V__LIST2) = s__ListLengthFn(V__LIST1)) & (s__ListOrderFn(V__LIST2,1) = s__ListOrderFn(V__LIST1,1)) & (! [V__ITEMFROM2] : (s__inList(V__ITEMFROM2,V__LIST2) => (? [V__POSITION,V__POSITIONMINUSONE,V__ITEMFROM1,V__PRIORFROM2] : (greater(V__POSITION,1) & lesseq(V__POSITION,s__ListLengthFn(V__LIST2)) & (s__ListOrderFn(V__LIST2,V__ITEMFROM2) = V__POSITION) & s__inList(V__ITEMFROM1,V__LIST1) & (V__POSITION = s__ListOrderFn(V__LIST1,V__ITEMFROM1)) & s__inList(V__PRIORFROM2,V__LIST2) & (V__POSITIONMINUSONE = minus(V__POSITION,1)) & (V__POSITIONMINUSONE = s__ListOrderFn(V__LIST2,V__PRIORFROM2)) & (V__ITEMFROM2 = plus(V__ITEMFROM1,V__PRIORFROM2)))))) & (V__LASTPLACE = s__ListLengthFn(V__LIST2)) & (V__AVERAGE = divide(s__ListOrderFn(V__LIST2,V__LASTPLACE) ,V__LASTPLACE))))) )	People.kif 285-306	?AVERAGE is an average of ?LIST1 if and only if there exists ?LIST2 such that length of ?LIST2 is equal to length of ?LIST1 and 1th element of ?LIST2 is equal to 1th element of ?LIST1 and for all ?ITEMFROM2 if ?ITEMFROM2 is a member of ?LIST2, then there exist ?POSITION, ?POSITIONMINUSONE,, , ?ITEMFROM1 and ?PRIORFROM2 such that ?POSITION is greater than 1 and ?POSITION is less than or equal to length of ?LIST2 and ?ITEMFROM2th element of ?LIST2 is equal to ?POSITION and ?ITEMFROM1 is a member of ?LIST1 and ?POSITION is equal to ?ITEMFROM1th element of ?LIST1 and ?PRIORFROM2 is a member of ?LIST2 and ?POSITIONMINUSONE is equal to (?POSITION and 1) and ?POSITIONMINUSONE is equal to ?PRIORFROM2th element of ?LIST2 and ?ITEMFROM2 is equal to (?ITEMFROM1 and ?PRIORFROM2) and ?LASTPLACE is equal to length of ?LIST2 and ?AVERAGE is equal to ?LASTPLACEth element of ?LIST2 and ?LASTPLACE
( ! [V__BG,V__N,V__R,V__P,V__N1,V__P2,V__N2] : (s__beliefGroupPercentInRegion(V__BG,V__N,V__R) <=> (? [V__G1,V__G2] : (s__located(V__P,V__R) & s__member(V__P,V__BG) & s__member(V__P,V__G1) & s__memberCount(V__G1,V__N1) & s__located(V__P2,V__R) & s__member(V__P2,V__G2) & s__memberCount(V__G2,V__N2) & (divide(V__N,100) = divide(V__N1,V__N2))))) )	People.kif 1526-1537	?N percent of people in ?R believe in ?BG if and only if there exist ?G1 and ?G2 such that ?P is located at ?R and ?P is a member of ?BG and ?P is a member of ?G1 and ?N1 is a member count of ?G1 and ?P2 is located at ?R and ?P2 is a member of ?G2 and ?N2 is a member count of ?G2 and ?N and 100 is equal to ?N1 and ?N2
( ! [V__E,V__R,V__MIN,V__M,V__MAX] : (s__compressionRatio(V__E,V__R) <=> (s__minCylinderVolume(V__E,s__MeasureFn(V__MIN,V__M)) & s__maxCylinderVolume(V__E,s__MeasureFn(V__MAX,V__M)) & (V__R = divide(V__MIN,V__MAX)))) )	Cars.kif 1958-1963	The compression ratio of ?E is ?R if and only if the minimum volume of the cylinders in the engine ?E is ?MIN ?M(s) and the maximum volume of the cylinders in the engine ?E is ?MAX ?M(s) and ?R is equal to ?MIN and ?MAX
( ! [V__PHYS1,V__PHYS2] : (s__cooccur(V__PHYS1,V__PHYS2) <=> (s__WhenFn(V__PHYS1) = s__WhenFn(V__PHYS2))) )	Merge.kif 8449-8451	?PHYS1 occurs at the same time as ?PHYS2 if and only if the time of existence of ?PHYS1 is equal to the time of existence of ?PHYS2
( ! [V__AREA,V__YEAR,V__REALNUMBER,V__THOUSANDS,V__BIRTHCOUNT,V__BIRTH,V__INFANT] : ((s__BirthsPerThousandFn(V__AREA,s__YearFn(V__YEAR)) = V__REALNUMBER) <=> ((divide(s__PopulationFn(V__AREA) ,1000) = V__THOUSANDS) & (V__BIRTHCOUNT = s__CardinalityFn(s__KappaFn(V__BIRTH,'(s__instance(V__BIRTH,s__Birth) & s__experiencer(V__BIRTH,V__INFANT) & s__instance(V__INFANT,s__Human) & s__during(s__WhenFn(V__BIRTH),s__YearFn(V__YEAR)) & (s__WhereFn(V__BIRTH,s__WhenFn(V__BIRTH)) = V__AREA))'))) & (divide(V__BIRTHCOUNT,V__THOUSANDS) = V__REALNUMBER))) )	People.kif 104-117	The births per thousand of ?AREA and the year ?YEAR is equal to ?REALNUMBER if and only if the population of ?AREA and 1000 is equal to ?THOUSANDS and ?BIRTHCOUNT is equal to the number of instances in the class described by ?BIRTH and ?BIRTHCOUNT and ?THOUSANDS is equal to ?REALNUMBER
( ! [V__AREA,V__YEAR,V__REALNUMBER,V__THOUSANDS,V__DEATHCOUNT,V__DEATH,V__PERSON] : ((s__DeathsPerThousandFn(V__AREA,s__YearFn(V__YEAR)) = V__REALNUMBER) <=> ((divide(s__PopulationFn(V__AREA) ,1000) = V__THOUSANDS) & (V__DEATHCOUNT = s__CardinalityFn(s__KappaFn(V__DEATH,'(s__instance(V__DEATH,s__Death) & s__experiencer(V__DEATH,V__PERSON) & s__instance(V__PERSON,s__Human) & s__during(s__WhenFn(V__DEATH),s__YearFn(V__YEAR)) & (s__WhereFn(V__DEATH,s__WhenFn(V__DEATH)) = V__AREA))'))) & (divide(V__DEATHCOUNT,V__THOUSANDS) = V__REALNUMBER))) )	People.kif 138-151	The deaths per thousand of ?AREA and the year ?YEAR is equal to ?REALNUMBER if and only if the population of ?AREA and 1000 is equal to ?THOUSANDS and ?DEATHCOUNT is equal to the number of instances in the class described by ?DEATH and ?DEATHCOUNT and ?THOUSANDS is equal to ?REALNUMBER
( ! [V__AREA,V__YEAR,V__REALNUMBER,V__BIRTHCOUNT,V__BIRTH,V__INFANT,V__THOUSANDSOFBIRTHS,V__INFANTDEATHCOUNT,V__DEATH,V__AGE] : ((s__DeathsPerThousandLiveBirthsFn(V__AREA,s__YearFn(V__YEAR)) = V__REALNUMBER) <=> ((V__BIRTHCOUNT = s__CardinalityFn(s__KappaFn(V__BIRTH,'(s__instance(V__BIRTH,s__Birth) & s__experiencer(V__BIRTH,V__INFANT) & s__instance(V__INFANT,s__Human) & s__during(s__WhenFn(V__BIRTH),s__YearFn(V__YEAR)) & (s__WhereFn(V__BIRTH,s__WhenFn(V__BIRTH)) = V__AREA))'))) & (divide(V__BIRTHCOUNT,1000) = V__THOUSANDSOFBIRTHS) & (V__INFANTDEATHCOUNT = s__CardinalityFn(s__KappaFn(V__DEATH,'(s__instance(V__DEATH,s__Death) & s__experiencer(V__DEATH,V__INFANT) & s__instance(V__INFANT,s__Human) & s__age(V__INFANT,s__MeasureFn(V__AGE,s__YearDuration)) & less(V__AGE,1) & s__during(s__WhenFn(V__DEATH),s__YearFn(V__YEAR)) & (s__WhereFn(V__DEATH,s__WhenFn(V__DEATH)) = V__AREA))'))) & (divide(V__INFANTDEATHCOUNT,V__THOUSANDSOFBIRTHS) = V__REALNUMBER))) )	People.kif 253-277	The deaths per thousand live births of ?AREA and the year ?YEAR is equal to ?REALNUMBER if and only if ?BIRTHCOUNT is equal to the number of instances in the class described by ?BIRTH and ?BIRTHCOUNT and 1000 is equal to ?THOUSANDSOFBIRTHS and ?INFANTDEATHCOUNT is equal to the number of instances in the class described by ?DEATH and ?INFANTDEATHCOUNT and ?THOUSANDSOFBIRTHS is equal to ?REALNUMBER
( ! [V__AREA,V__YEAR,V__REALNUMBER,V__COUNT,V__LIFEEXPECTANCYAGE,V__BIRTH,V__INDIVIDUAL,V__DEATH] : ((s__FemaleLifeExpectancyAtBirthFn(V__AREA,s__YearFn(V__YEAR)) = V__REALNUMBER) <=> (? [V__LIST] : (s__instance(V__LIST,s__List) & s__instance(s__ListLengthFn(V__LIST) ,V__COUNT) & (! [V__LISTITEM] : (s__inList(V__LISTITEM,V__LIST) => (s__instance(V__LISTITEM,V__LIFEEXPECTANCYAGE) & (~ (? [V__NUMBER] : (s__instance(V__NUMBER,V__LIFEEXPECTANCYAGE) & (~ s__inList(V__NUMBER,V__LIST))))) & (V__COUNT = s__CardinalityFn(s__KappaFn(V__LIFEEXPECTANCYAGE,'(s__instance(V__BIRTH,s__Birth) & s__experiencer(V__BIRTH,V__INDIVIDUAL) & s__instance(V__INDIVIDUAL,s__Human) & s__attribute(V__INDIVIDUAL,s__Female) & s__during(s__WhenFn(V__BIRTH),s__YearFn(V__YEAR)) & (s__WhereFn(V__BIRTH,s__WhenFn(V__BIRTH)) = V__AREA) & s__instance(V__DEATH,s__Death) & s__experiencer(V__DEATH,V__INDIVIDUAL) & s__holdsDuring(s__WhenFn(V__DEATH),s__age(V__INDIVIDUAL,s__MeasureFn(V__LIFEEXPECTANCYAGE,s__YearDuration))))')))))) & s__average(V__LIST,V__REALNUMBER)))) )	People.kif 411-442	The female life expectancy at birth of ?AREA and the year ?YEAR is equal to ?REALNUMBER if and only if there exists ?LIST such that ?LIST is an instance of list and length of ?LIST is an instance of ?COUNT and for all ?LISTITEM if ?LISTITEM is a member of ?LIST, then ?LISTITEM is an instance of ?LIFEEXPECTANCYAGE and there doesn't exist ?NUMBER such that ?NUMBER is an instance of ?LIFEEXPECTANCYAGE and ?NUMBER is not a member of ?LIST and ?COUNT is equal to the number of instances in the class described by ?LIFEEXPECTANCYAGE and ?REALNUMBER is an average of ?LIST
( ! [V__LIST,V__ITEM] : ((s__LastFn(V__LIST) = V__ITEM) <=> (? [V__NUMBER] : ((s__ListLengthFn(V__LIST) = V__NUMBER) & (s__ListOrderFn(V__LIST,V__NUMBER) = V__ITEM)))) )	Mid-level-ontology.kif 6342-6347	The last of ?LIST is equal to ?ITEM if and only if there exists ?NUMBER such that length of ?LIST is equal to ?NUMBER and ?NUMBERth element of ?LIST is equal to ?ITEM
( ! [V__AREA,V__YEAR,V__REALNUMBER,V__COUNT,V__LIFEEXPECTANCYAGE,V__BIRTH,V__INDIVIDUAL,V__DEATH] : ((s__LifeExpectancyAtBirthFn(V__AREA,s__YearFn(V__YEAR)) = V__REALNUMBER) <=> (? [V__LIST] : (s__instance(V__LIST,s__List) & s__instance(s__ListLengthFn(V__LIST) ,V__COUNT) & (! [V__LISTITEM] : (s__inList(V__LISTITEM,V__LIST) => (s__instance(V__LISTITEM,V__LIFEEXPECTANCYAGE) & (~ (? [V__NUMBER] : (s__instance(V__NUMBER,V__LIFEEXPECTANCYAGE) & (~ s__inList(V__NUMBER,V__LIST))))) & (V__COUNT = s__CardinalityFn(s__KappaFn(V__LIFEEXPECTANCYAGE,'(s__instance(V__BIRTH,s__Birth) & s__experiencer(V__BIRTH,V__INDIVIDUAL) & s__instance(V__INDIVIDUAL,s__Human) & s__during(s__WhenFn(V__BIRTH),s__YearFn(V__YEAR)) & (s__WhereFn(V__BIRTH,s__WhenFn(V__BIRTH)) = V__AREA) & s__instance(V__DEATH,s__Death) & s__experiencer(V__DEATH,V__INDIVIDUAL) & s__holdsDuring(s__WhenFn(V__DEATH),s__age(V__INDIVIDUAL,s__MeasureFn(V__LIFEEXPECTANCYAGE,s__YearDuration))))')))))) & s__average(V__LIST,V__REALNUMBER)))) )	People.kif 323-353	The life expectancy at birth of ?AREA and the year ?YEAR is equal to ?REALNUMBER if and only if there exists ?LIST such that ?LIST is an instance of list and length of ?LIST is an instance of ?COUNT and for all ?LISTITEM if ?LISTITEM is a member of ?LIST, then ?LISTITEM is an instance of ?LIFEEXPECTANCYAGE and there doesn't exist ?NUMBER such that ?NUMBER is an instance of ?LIFEEXPECTANCYAGE and ?NUMBER is not a member of ?LIST and ?COUNT is equal to the number of instances in the class described by ?LIFEEXPECTANCYAGE and ?REALNUMBER is an average of ?LIST
( ! [V__AREA,V__YEAR,V__REALNUMBER,V__COUNT,V__LIFEEXPECTANCYAGE,V__BIRTH,V__INDIVIDUAL,V__DEATH] : ((s__MaleLifeExpectancyAtBirthFn(V__AREA,s__YearFn(V__YEAR)) = V__REALNUMBER) <=> (? [V__LIST] : (s__instance(V__LIST,s__List) & s__instance(s__ListLengthFn(V__LIST) ,V__COUNT) & (! [V__LISTITEM] : (s__inList(V__LISTITEM,V__LIST) => (s__instance(V__LISTITEM,V__LIFEEXPECTANCYAGE) & (~ (? [V__NUMBER] : (s__instance(V__NUMBER,V__LIFEEXPECTANCYAGE) & (~ s__inList(V__NUMBER,V__LIST))))) & (V__COUNT = s__CardinalityFn(s__KappaFn(V__LIFEEXPECTANCYAGE,'(s__instance(V__BIRTH,s__Birth) & s__experiencer(V__BIRTH,V__INDIVIDUAL) & s__instance(V__INDIVIDUAL,s__Human) & s__attribute(V__INDIVIDUAL,s__Male) & s__during(s__WhenFn(V__BIRTH),s__YearFn(V__YEAR)) & (s__WhereFn(V__BIRTH,s__WhenFn(V__BIRTH)) = V__AREA) & s__instance(V__DEATH,s__Death) & s__experiencer(V__DEATH,V__INDIVIDUAL) & s__holdsDuring(s__WhenFn(V__DEATH),s__age(V__INDIVIDUAL,s__MeasureFn(V__LIFEEXPECTANCYAGE,s__YearDuration))))')))))) & s__average(V__LIST,V__REALNUMBER)))) )	People.kif 367-398	The male life expectancy at birth of ?AREA and the year ?YEAR is equal to ?REALNUMBER if and only if there exists ?LIST such that ?LIST is an instance of list and length of ?LIST is an instance of ?COUNT and for all ?LISTITEM if ?LISTITEM is a member of ?LIST, then ?LISTITEM is an instance of ?LIFEEXPECTANCYAGE and there doesn't exist ?NUMBER such that ?NUMBER is an instance of ?LIFEEXPECTANCYAGE and ?NUMBER is not a member of ?LIST and ?COUNT is equal to the number of instances in the class described by ?LIFEEXPECTANCYAGE and ?REALNUMBER is an average of ?LIST
( ! [V__AREA,V__REALNUMBER,V__MALECOUNT,V__MALE,V__FEMALECOUNT,V__FEMALE] : ((s__MaleToFemaleRatioFn(V__AREA) = V__REALNUMBER) <=> ((V__MALECOUNT = s__CardinalityFn(s__KappaFn(V__MALE,'(s__instance(V__MALE,s__Human) & s__attribute(V__MALE,s__Male) & s__inhabits(V__MALE,V__AREA))'))) & (V__FEMALECOUNT = s__CardinalityFn(s__KappaFn(V__FEMALE,'(s__instance(V__FEMALE,s__Human) & s__attribute(V__FEMALE,s__Female) & s__inhabits(V__FEMALE,V__AREA))'))) & (divide(V__MALECOUNT,V__FEMALECOUNT) = V__REALNUMBER))) )	People.kif 221-238	The male to female ratio of ?AREA is equal to ?REALNUMBER if and only if ?MALECOUNT is equal to the number of instances in the class described by ?MALE and ?FEMALECOUNT is equal to the number of instances in the class described by ?FEMALE and ?MALECOUNT and ?FEMALECOUNT is equal to ?REALNUMBER
( ! [V__AREA,V__YEAR,V__REALNUMBER,V__PREVIOUSYEAR,V__POPULATION,V__THOUSANDS,V__IMMIGRATION,V__PERSON,V__EMMIGRATION,V__MIGRATIONCOUNT] : ((s__MigrantsPerThousandFn(V__AREA,s__YearFn(V__YEAR)) = V__REALNUMBER) <=> ((minus(V__YEAR,V__PREVIOUSYEAR) = 1) & s__holdsDuring(s__YearFn(V__YEAR) ,'(s__PopulationFn(V__AREA) = V__POPULATION)') & (divide(V__POPULATION,1000) = V__THOUSANDS) & (V__IMMIGRATION = s__CardinalityFn(s__KappaFn(V__PERSON,'(s__instance(V__PERSON,s__Human) & s__holdsDuring(s__YearFn(V__PREVIOUSYEAR),(~ s__inhabits(V__PERSON,V__AREA))) & s__holdsDuring(s__YearFn(V__YEAR),s__inhabits(V__PERSON,V__AREA)))'))) & (V__EMMIGRATION = s__CardinalityFn(s__KappaFn(V__PERSON,'(s__instance(V__PERSON,s__Human) & s__holdsDuring(s__YearFn(V__PREVIOUSYEAR),s__inhabits(V__PERSON,V__AREA)) & s__holdsDuring(s__YearFn(V__YEAR),(~ s__inhabits(V__PERSON,V__AREA))))'))) & (minus(V__IMMIGRATION,V__EMMIGRATION) = V__MIGRATIONCOUNT) & (divide(V__MIGRATIONCOUNT,V__THOUSANDS) = V__REALNUMBER))) )	People.kif 174-202	The migrants per thousand of ?AREA and the year ?YEAR is equal to ?REALNUMBER if and only if (?YEAR and ?PREVIOUSYEAR) is equal to 1 and the population of ?AREA is equal to ?POPULATION holds during the year ?YEAR and ?POPULATION and 1000 is equal to ?THOUSANDS and ?IMMIGRATION is equal to the number of instances in the class described by ?PERSON and ?EMMIGRATION is equal to the number of instances in the class described by ?PERSON and (?IMMIGRATION and ?EMMIGRATION) is equal to ?MIGRATIONCOUNT and ?MIGRATIONCOUNT and ?THOUSANDS is equal to ?REALNUMBER
( ! [V__AREA,V__YEAR,V__ADJUSTEDPERCENT,V__PREVIOUSYEAR,V__POPULATION,V__PREVIOUSPOPULATION,V__PERCENT] : ((s__PopulationGrowthFn(V__AREA,s__YearFn(V__YEAR)) = V__ADJUSTEDPERCENT) <=> ((minus(V__YEAR,V__PREVIOUSYEAR) = 1) & s__holdsDuring(s__YearFn(V__YEAR) ,'(s__PopulationFn(V__AREA) = V__POPULATION)') & s__holdsDuring(s__YearFn(V__PREVIOUSYEAR) ,'(s__PopulationFn(V__AREA) = V__PREVIOUSPOPULATION)') & (divide(V__POPULATION,V__PREVIOUSPOPULATION) = V__PERCENT) & (minus(V__PERCENT,1) = V__ADJUSTEDPERCENT))) )	People.kif 77-86	The population growth of ?AREA and the year ?YEAR is equal to ?ADJUSTEDPERCENT if and only if (?YEAR and ?PREVIOUSYEAR) is equal to 1 and the population of ?AREA is equal to ?POPULATION holds during the year ?YEAR and the population of ?AREA is equal to ?PREVIOUSPOPULATION holds during the year ?PREVIOUSYEAR and ?POPULATION and ?PREVIOUSPOPULATION is equal to ?PERCENT and (?PERCENT and 1) is equal to ?ADJUSTEDPERCENT
( ! [V__NUMBER1,V__NUMBER2,V__NUMBER] : ((s__RemainderFn(V__NUMBER1,V__NUMBER2) = V__NUMBER) <=> (plus(times(s__FloorFn(divide(V__NUMBER1,V__NUMBER2)) ,V__NUMBER2) ,V__NUMBER) = V__NUMBER1)) )	Merge.kif 5226-5228	?NUMBER1 Mod ?NUMBER2 is equal to ?NUMBER if and only if (the largest integer less than or equal to ?NUMBER1 and ?NUMBER2 and ?NUMBER2 and ?NUMBER) is equal to ?NUMBER1
( ! [V__BG,V__N,V__R,V__P,V__N1,V__P2,V__N2] : (s__ethnicityPercentInRegion(V__BG,V__N,V__R) <=> (? [V__G1,V__G2] : (s__located(V__P,V__R) & s__member(V__P,V__BG) & s__member(V__P,V__G1) & s__memberCount(V__G1,V__N1) & s__located(V__P2,V__R) & s__member(V__P2,V__G2) & s__memberCount(V__G2,V__N2) & (divide(V__N,100) = divide(V__N1,V__N2))))) )	People.kif 1545-1556	?N percent of people in ?R are ?BG if and only if there exist ?G1 and ?G2 such that ?P is located at ?R and ?P is a member of ?BG and ?P is a member of ?G1 and ?N1 is a member count of ?G1 and ?P2 is located at ?R and ?P2 is a member of ?G2 and ?N2 is a member count of ?G2 and ?N and 100 is equal to ?N1 and ?N2
( ! [V__INTERVAL1,V__INTERVAL2] : (s__finishes(V__INTERVAL1,V__INTERVAL2) <=> (s__before(s__BeginFn(V__INTERVAL2) ,s__BeginFn(V__INTERVAL1)) & (s__EndFn(V__INTERVAL2) = s__EndFn(V__INTERVAL1)))) )	Merge.kif 8230-8238	?INTERVAL1 finishes ?INTERVAL2 if and only if the beginning of ?INTERVAL2 happens before the beginning of ?INTERVAL1 and the end of ?INTERVAL2 is equal to the end of ?INTERVAL1
( ! [V__NUMBER1,V__NUMBER2] : (greatereq(V__NUMBER1,V__NUMBER2) <=> ((V__NUMBER1 = V__NUMBER2) \| greater(V__NUMBER1,V__NUMBER2))) )	Merge.kif 1930-1934	?NUMBER1 is greater than or equal to ?NUMBER2 if and only if ?NUMBER1 is equal to ?NUMBER2 or ?NUMBER1 is greater than ?NUMBER2
( ! [V__T,V__P,V__H] : (s__holdsDuring(V__T,'s__attribute(V__P,s__Alone)') <=> (~ (? [V__H2,V__SI] : ((~ (V__H = V__H2)) & s__instance(V__H2,s__Agent) & s__instance(V__SI,s__SocialInteraction) & s__involvedInEvent(V__SI,V__H) & s__involvedInEvent(V__SI,V__H2))))) )	Mid-level-ontology.kif 27933-27944	Alone is an attribute of ?P holds during ?T if and only if there don't exist ?H2 and ?SI such that ?H is not equal to ?H2 and ?H2 is an instance of agent and ?SI is an instance of social interaction and ?H is an involved in event of ?SI and ?H2 is an involved in event of ?SI
( ! [V__COMPOUND] : (s__instance(V__COMPOUND,s__CompoundSubstance) <=> (? [V__ELEMENT1,V__ELEMENT2,V__PROCESS] : (s__instance(V__ELEMENT1,s__ElementalSubstance) & s__instance(V__ELEMENT2,s__ElementalSubstance) & (~ (V__ELEMENT1 = V__ELEMENT2)) & s__instance(V__PROCESS,s__ChemicalSynthesis) & s__resource(V__PROCESS,V__ELEMENT1) & s__resource(V__PROCESS,V__ELEMENT2) & s__result(V__PROCESS,V__COMPOUND)))) )	Merge.kif 12313-12323	?COMPOUND is an instance of compound substance if and only if there exist ?ELEMENT1, ?ELEMENT2 and ?PROCESS such that ?ELEMENT1 is an instance of elemental substance and ?ELEMENT2 is an instance of elemental substance and ?ELEMENT1 is not equal to ?ELEMENT2 and ?PROCESS is an instance of chemical synthesis and ?ELEMENT1 is a resource for ?PROCESS and ?ELEMENT2 is a resource for ?PROCESS and ?COMPOUND is a result of ?PROCESS
( ! [V__CONTINENT] : (s__instance(V__CONTINENT,s__Continent) <=> ((s__Africa = V__CONTINENT) \| (s__NorthAmerica = V__CONTINENT) \| (s__SouthAmerica = V__CONTINENT) \| (s__Antarctica = V__CONTINENT) \| (s__Europe = V__CONTINENT) \| (s__Asia = V__CONTINENT) \| (s__Oceania = V__CONTINENT))) )	Geography.kif 3350-3359	?CONTINENT is an instance of continent if and only if africa is equal to ?CONTINENT or north america is equal to ?CONTINENT or south america is equal to ?CONTINENT or antarctica is equal to ?CONTINENT or europe is equal to ?CONTINENT or asia is equal to ?CONTINENT or oceania is equal to ?CONTINENT

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement

( ! [V__AREA,V__YEAR,V__PERSON,V__MILITARYAGE,V__AGEMINUSONE,V__AGE] : (s__ReachingMilitaryAgeAnnuallyMaleFn(V__AREA,V__YEAR) = s__CardinalityFn(s__KappaFn(V__PERSON,'(s__instance(V__PERSON,s__Human) & s__attribute(V__PERSON,s__Male) & s__militaryAge(V__AREA,V__MILITARYAGE) & (V__AGEMINUSONE = minus(V__AGE,1)) & s__holdsDuring(V__YEAR,(s__age(V__PERSON,V__AGEMINUSONE) \| s__age(V__PERSON,V__AGE))) & (V__AGE = V__MILITARYAGE) & s__inhabits(V__PERSON,V__AREA))'))) )	Military.kif 928-941	The reaching military age annually male of ?AREA and ?YEAR is equal to the number of instances in the class described by ?PERSON
(! [V__NUMBER] : (s__MeasureFn(V__NUMBER,s__OunceMass) = s__MeasureFn(divide(V__NUMBER,16) ,s__PoundMass)))	DimensioningAmenities.kif 28-31	For all ?NUMBER ?NUMBER Ounce(s) is equal to ?NUMBER and 16 pound mass(s)
(! [V__NUMBER] : (s__PredecessorFn(V__NUMBER) = minus(V__NUMBER,1)))	Merge.kif 4857-4858	For all ?NUMBER (?NUMBER+2) is equal to (?NUMBER and 1)
(! [V__NUMBER] : (s__SuccessorFn(V__NUMBER) = plus(V__NUMBER,1)))	Merge.kif 4837-4838	For all ?NUMBER (?NUMBER+1) is equal to (?NUMBER and 1)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3214-3217	For all @ROW and ?ITEM length of (@ROW and ?ITEM) is equal to (length of (@ROW)+1)
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3219-3223	For all @ROW and ?ITEM length of (@ROW and ?ITEM)th element of (@ROW and ?ITEM) is equal to ?ITEM
(~ (s__BigSix = s__GroupOf6))	Government.kif 2852-2852	Big six is not equal to group of6

appearance as argument number 0

( ! [V__AREA,V__PERSON,V__MILITARYAGE,V__AGE] : (s__AvailableForMilitaryServiceMaleFn(V__AREA) = s__CardinalityFn(s__KappaFn(V__PERSON,'(s__instance(V__PERSON,s__Human) & s__attribute(V__PERSON,s__Male) & s__militaryAge(V__AREA,V__MILITARYAGE) & s__age(V__PERSON,V__AGE) & greatereq(V__AGE,V__MILITARYAGE) & s__inhabits(V__PERSON,V__AREA))'))) )	Military.kif 867-876	The available for military service male of ?AREA is equal to the number of instances in the class described by ?PERSON
(s__BeginFn(s__BeforeCommonEra) = s__NegativeInfinity)	Mid-level-ontology.kif 7585-7585	The beginning of before common era is equal to negative infinity
(s__CardinalityFn(s__Continent) = 7)	Merge.kif 14066-14066	The number of instances in continent is equal to 7
(s__CardinalityFn(s__NativityMagi) = 3)	Media.kif 2005-2005	The number of instances in NativityMagi is equal to 3
( ! [V__AREA,V__YEAR,V__INFANT,V__BIRTH,V__WOMAN] : (s__ChildrenBornPerWomanFn(V__AREA,s__YearFn(V__YEAR)) = s__CardinalityFn(s__KappaFn(V__INFANT,'(s__instance(V__BIRTH,s__Birth) & s__experiencer(V__BIRTH,V__INFANT) & s__agent(V__BIRTH,V__WOMAN) & s__instance(V__WOMAN,s__Human) & s__attribute(V__WOMAN,s__Female) & s__holdsDuring(s__YearFn(V__YEAR),s__inhabits(V__WOMAN,V__AREA)))'))) )	People.kif 462-472	The children born per woman of ?AREA and the year ?YEAR is equal to the number of instances in the class described by ?INFANT
(s__EndFn(s__CommonEra) = s__PositiveInfinity)	Mid-level-ontology.kif 7593-7593	The end of common era is equal to positive infinity
( ! [V__AREA,V__PERSON,V__PROCESS,V__MILITARYAGE,V__AGE] : (s__FitForMilitaryServiceMaleFn(V__AREA) = s__CardinalityFn(s__KappaFn(V__PERSON,'(s__instance(V__PERSON,s__Human) & s__attribute(V__PERSON,s__Male) & s__instance(V__PROCESS,s__MilitaryProcess) & s__fitForMilitaryService(V__PERSON,V__PROCESS) & s__militaryAge(V__AREA,V__MILITARYAGE) & s__age(V__PERSON,V__AGE) & greatereq(V__AGE,V__MILITARYAGE) & s__inhabits(V__PERSON,V__AREA))'))) )	Military.kif 890-901	The fit for military service male of ?AREA is equal to the number of instances in the class described by ?PERSON
(s__MeasureFn(0,s__AngularDegree) = s__MeasureFn(360,s__AngularDegree))	Merge.kif 7616-7616	0 Angular degree(s) is equal to 360 angular degree(s)
(s__MeasureFn(1,s__AngularDegree) = s__MeasureFn(60,s__ArcMinute))	Geography.kif 382-382	1 Angular degree(s) is equal to 60 arc minute(s)
(s__MeasureFn(1,s__ArcMinute) = s__MeasureFn(60,s__ArcSecond))	Geography.kif 401-401	1 Arc minute(s) is equal to 60 arc second(s)
(s__MeasureFn(1,s__CubicFoot) = times(s__MeasureFn(1,s__FootLength),times(s__MeasureFn(1,s__FootLength),s__MeasureFn(1,s__FootLength))))	Mid-level-ontology.kif 10963-10969	1 Cubic foot(s) is equal to 1 foot length(s) and 1 foot length(s) and 1 foot length(s)
(s__MeasureFn(1,s__Fathom) = s__MeasureFn(6,s__FootLength))	Geography.kif 3664-3664	1 Fathom(s) is equal to 6 foot length(s)
(s__MeasureFn(1,s__KilowattHour) = s__MeasureFn(3.6,s__MegaFn(s__Joule)))	Economy.kif 2012-2012	1 Kilowatt hour(s) is equal to 3.6 1 million joules(s)
(s__MeasureFn(1,s__KilowattHour) = s__MeasureFn(3600000,s__Joule))	Economy.kif 2013-2013	1 Kilowatt hour(s) is equal to 3600000 joule(s)
(s__MeasureFn(1,s__MetricTon) = s__MeasureFn(2205,s__PoundMass))	Mid-level-ontology.kif 10935-10937	1 Metric ton(s) is equal to 2205 pound mass(s)
(s__MeasureFn(1,s__NauticalMile) = s__MeasureFn(1852,s__Meter))	Geography.kif 3684-3684	1 Nautical mile(s) is equal to 1852 meter(s)
(s__MeasureFn(1,s__NauticalMile) = s__MeasureFn(6076.1,s__FootLength))	Geography.kif 3683-3683	1 Nautical mile(s) is equal to 6076.1 foot length(s)
(s__MeasureFn(1,s__SquareKilometer) = times(s__MeasureFn(1,s__KiloFn(s__Meter)) ,s__MeasureFn(1,s__KiloFn(s__Meter))))	Geography.kif 621-622	1 Square kilometer(s) is equal to 1 1 thousand meters(s) and 1 1 thousand meters(s)
(s__MeasureFn(1,s__SquareMeter) = times(s__MeasureFn(1,s__Meter),s__MeasureFn(1,s__Meter)))	Geography.kif 3736-3737	1 Square meter(s) is equal to 1 meter(s) and 1 meter(s)
(s__MeasureFn(1,s__SquareMile) = s__PerFn(s__MeasureFn(1,s__Mile),s__MeasureFn(1,s__Mile)))	Mid-level-ontology.kif 11019-11023	1 Square mile(s) is equal to the per of 1 mile(s) and 1 mile(s)
(s__MeasureFn(1,s__SquareYard) = s__PerFn(s__MeasureFn(1,s__YardLength),s__MeasureFn(1,s__YardLength)))	Mid-level-ontology.kif 11029-11033	1 Square yard(s) is equal to the per of 1 yard length(s) and 1 yard length(s)
( ! [V__DEG] : (s__MeasureFn(V__DEG,s__ArcMinute) = s__MeasureFn(times(60,V__DEG) ,s__ArcSecond)) )	Geography.kif 402-402	?DEG Arc minute(s) is equal to 60 and ?DEG arc second(s)
( ! [V__MUMBER,V__NUMBER] : (s__MeasureFn(V__MUMBER,s__Micrometer) = s__MeasureFn(times(V__NUMBER,0.0000001) ,s__Meter)) )	Geography.kif 6450-6453	?MUMBER Micrometer(s) is equal to ?NUMBER and 0.0000001 meter(s)
( ! [V__NUM] : (s__MeasureFn(V__NUM,s__AngularDegree) = s__MeasureFn(times(60,V__NUM) ,s__ArcMinute)) )	Geography.kif 383-383	?NUM Angular degree(s) is equal to 60 and ?NUM arc minute(s)
( ! [V__NUMBER] : (s__MeasureFn(V__NUMBER,s__Amu) = s__MeasureFn(times(V__NUMBER,1.6605402E-24) ,s__Gram)) )	Merge.kif 7376-7378	?NUMBER Amu(s) is equal to ?NUMBER and 1.6605402E-24 gram(s)

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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: