equal


Sigma KEE  equal
appearance as argument number 1


appearance as argument number 2


s__format(s__ChineseLanguage,s__equal__m,'"%1 %n equal %2"')

chinese_format.kif 297297 

s__format(s__EnglishLanguage,s__equal__m,'"%1 is %n equal to %2"')

english_format.kif 305305 

s__termFormat(s__ChineseLanguage,s__equal__m,'"等于"')

chinese_format.kif 298298 

s__termFormat(s__ChineseTraditionalLanguage,s__equal__m,'"等於"')

domainEnglishFormat.kif 2231022310 

s__termFormat(s__EnglishLanguage,s__equal__m,'"equal"')

domainEnglishFormat.kif 2230922309 

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 = s__SubtractionFn(n__0,V__NUMBER1)))))
&
(((s__instance(V__NUMBER1,s__NonnegativeRealNumber) &
(V__NUMBER1 = V__NUMBER2))

(s__instance(V__NUMBER1,s__NegativeRealNumber) &
(V__NUMBER2 = s__SubtractionFn(n__0,V__NUMBER1))))
=>
((s__AbsoluteValueFn(V__NUMBER1)
= V__NUMBER2)
&
s__instance(V__NUMBER1,s__RealNumber) &
s__instance(V__NUMBER2,s__RealNumber))))
)
)

Merge.kif 45954606 
The absolute value of a real number is equal to a nonnegative real number and the real number is an instance of real number and the nonnegative real number is an instance of real number if and only if the real number is an instance of nonnegative real number and the real number is equal to the nonnegative real number or the real number is an instance of negative real number and the nonnegative real number is equal to (0 and the real number) 
( ! [V__LIST3,V__LIST1,V__LIST2] :
(((s__instance(V__LIST3,s__List) &
s__instance(V__LIST1,s__List) &
s__instance(V__LIST2,s__List))
=>
(((((V__LIST3 = s__ListConcatenateFn(V__LIST1,V__LIST2))
&
~((V__LIST1 = s__NullList))
&
~((V__LIST2 = s__NullList)))
=>
( ! [V__NUMBER1, V__NUMBER2] :
(((s__lessThanOrEqualTo(V__NUMBER1,s__ListLengthFn(V__LIST1))
&
s__lessThanOrEqualTo(V__NUMBER2,s__ListLengthFn(V__LIST2))
&
s__instance(V__NUMBER1,s__PositiveInteger) &
s__instance(V__NUMBER2,s__PositiveInteger))
=>
(((s__ListOrderFn(V__LIST3,V__NUMBER1)
= s__ListOrderFn(V__LIST1,V__NUMBER1))
&
(s__ListOrderFn(V__LIST3,s__AdditionFn(s__ListLengthFn(V__LIST1)
,V__NUMBER2))
= s__ListOrderFn(V__LIST2,V__NUMBER2))))))))
&
(( ! [V__NUMBER1, V__NUMBER2] :
(((s__lessThanOrEqualTo(V__NUMBER1,s__ListLengthFn(V__LIST1))
&
s__lessThanOrEqualTo(V__NUMBER2,s__ListLengthFn(V__LIST2))
&
s__instance(V__NUMBER1,s__PositiveInteger) &
s__instance(V__NUMBER2,s__PositiveInteger))
=>
(((s__ListOrderFn(V__LIST3,V__NUMBER1)
= s__ListOrderFn(V__LIST1,V__NUMBER1))
&
(s__ListOrderFn(V__LIST3,s__AdditionFn(s__ListLengthFn(V__LIST1)
,V__NUMBER2))
= s__ListOrderFn(V__LIST2,V__NUMBER2)))))))
=>
((V__LIST3 = s__ListConcatenateFn(V__LIST1,V__LIST2))
&
~((V__LIST1 = s__NullList))
&
~((V__LIST2 = s__NullList)))))))
)
)

Merge.kif 29792995 
A list is equal to the list composed of another list and a third list and the other list is not equal to null list and the third list is not equal to null list if and only if for all a positive integer and another positive integer 
( ! [V__Agent,V__Account,V__Asset] :
(((s__instance(V__Agent,s__CognitiveAgent) &
s__instance(V__Asset,s__FinancialAsset) &
s__instance(V__Asset,s__Object))
=>
((((s__instance(V__Account,s__FinancialAccount) &
s__possesses(V__Agent,V__Asset)
&
(V__Account = s__AccountFn(V__Asset)))
=>
s__accountHolder(V__Account,V__Agent))
&
(s__accountHolder(V__Account,V__Agent)
=>
(s__instance(V__Account,s__FinancialAccount) &
s__possesses(V__Agent,V__Asset)
&
(V__Account = s__AccountFn(V__Asset)))))))
)
)

FinancialOntology.kif 22912296 
A financial account is an instance of financial account and a cognitive agent possesses a financial asset and the financial account is equal to the account of the financial asset if and only if the cognitive agent holds account the financial account 
( ! [V__AMOUNT,V__UNIT] :
(((s__instance(V__AMOUNT,s__Number) &
s__instance(V__AMOUNT,s__PhysicalQuantity))
=>
((((s__instance(V__UNIT,s__UnitOfMeasure) &
(V__AMOUNT = s__MeasureFn(n__1,s__SquareUnitFn(V__UNIT))))
=>
(V__AMOUNT = s__MultiplicationFn(s__MeasureFn(n__1,V__UNIT)
,s__MeasureFn(n__1,V__UNIT))))
&
((V__AMOUNT = s__MultiplicationFn(s__MeasureFn(n__1,V__UNIT)
,s__MeasureFn(n__1,V__UNIT)))
=>
(s__instance(V__UNIT,s__UnitOfMeasure) &
(V__AMOUNT = s__MeasureFn(n__1,s__SquareUnitFn(V__UNIT))))))))
)
)

Geography.kif 38043808 
An unit of measure is an instance of unit of measure and a number is equal to 1 the square unit of the unit of measure(s) if and only if the number is equal to 1 the unit of measure(s) and 1 the unit of measure(s) 
No TPTP formula. May not be expressible in strict first order. 
People.kif 104117 
The births per thousand of a geopolitical area and the year an integer is equal to a real number if and only if the population of the geopolitical area and 1000 is equal to a number and another integer is equal to the number of instances in the class described by a symbolic string and the other integer and the number is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
People.kif 138151 
The deaths per thousand of a geopolitical area and the year an integer is equal to a real number if and only if the population of the geopolitical area and 1000 is equal to a number and another integer is equal to the number of instances in the class described by a symbolic string and the other integer and the number is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
People.kif 253277 
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 number 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 number is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
People.kif 411442 
The female life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list 
( ! [V__LIST,V__ITEM] :
((s__instance(V__LIST,s__List) =>
((((s__LastFn(V__LIST)
= V__ITEM)
=>
( ? [V__NUMBER] :
((s__instance(V__NUMBER,s__PositiveInteger) &
((s__ListLengthFn(V__LIST)
= V__NUMBER)
&
(s__ListOrderFn(V__LIST,V__NUMBER)
= V__ITEM))))))
&
(( ? [V__NUMBER] :
((s__instance(V__NUMBER,s__PositiveInteger) &
((s__ListLengthFn(V__LIST)
= V__NUMBER)
&
(s__ListOrderFn(V__LIST,V__NUMBER)
= V__ITEM)))))
=>
(s__LastFn(V__LIST)
= V__ITEM)))))
)
)

Merge.kif 31073112 
The last of a list is equal to an entity if and only if there exists a positive integer such that length of the list is equal to the positive integer and the positive integerth element of the list is equal to the entity 
No TPTP formula. May not be expressible in strict first order. 
People.kif 323353 
The life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list 
No TPTP formula. May not be expressible in strict first order. 
People.kif 367398 
The male life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list 
No TPTP formula. May not be expressible in strict first order. 
People.kif 221238 
The male to female ratio of a geopolitical area is equal to a real number if and only if an integer is equal to the number of instances in the class described by a symbolic string and another integer is equal to the number of instances in the class described by another symbolic string and the integer and the other integer is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
People.kif 174202 
The migrants per thousand of a geopolitical area and the year an integer is equal to a real number if and only if (the integer and a number) is equal to 1 and the population of the geopolitical area is equal to another number holds during the year the integer and the other number and 1000 is equal to a third number and another integer is equal to the number of instances in the class described by a symbolic string and a third integer is equal to the number of instances in the class described by the symbolic string and (the other integer and the third integer) is equal to a fourth number and the fourth number and the third number is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
People.kif 7786 
The population growth of a geopolitical area and the year an integer is equal to a real number if and only if (the integer and another integer) is equal to 1 and the population of the geopolitical area is equal to a number holds during the year the integer and the population of the geopolitical area is equal to another number holds during the year the other integer and the number and the other number is equal to a third number and (the third number and 1) is equal to the real number 
( ! [V__NUMBER1,V__NUMBER2,V__NUMBER] :
(((s__instance(V__NUMBER1,s__Integer) &
s__instance(V__NUMBER2,s__Integer) &
s__instance(V__NUMBER,s__Integer))
=>
((((s__RemainderFn(V__NUMBER1,V__NUMBER2)
= V__NUMBER)
=>
(s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
,V__NUMBER2)
,V__NUMBER)
= V__NUMBER1))
&
((s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
,V__NUMBER2)
,V__NUMBER)
= V__NUMBER1)
=>
(s__RemainderFn(V__NUMBER1,V__NUMBER2)
= V__NUMBER)))))
)
)

Merge.kif 49084910 
An integer mod another integer is equal to a third integer if and only if (the largest integer less than or equal to the integer and the other integer and the other integer and the third integer) is equal to the integer 
( ! [V__AMOUNT,V__PERSON] :
(((s__instance(V__AMOUNT,s__CurrencyMeasure) &
s__instance(V__PERSON,s__Agent))
=>
((((s__WealthFn(V__PERSON)
= V__AMOUNT)
=>
s__monetaryValue(s__PropertyFn(V__PERSON)
,V__AMOUNT))
&
(s__monetaryValue(s__PropertyFn(V__PERSON)
,V__AMOUNT)
=>
(s__WealthFn(V__PERSON)
= V__AMOUNT)))))
)
)

Merge.kif 75467548 
Value of belongings of an agent is equal to a currency measure if and only if value of belongings of the agent is the currency measure 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 40944096 
The place where a physical was at a time point is equal to a region if and only if the physical is exactly located in the region holds during the time point 
( ! [V__SD,V__L] :
(((s__instance(V__SD,s__RealNumber) &
s__instance(V__L,s__List))
=>
((((V__SD = s__StandardDeviationFn(V__L))
=>
(V__SD = s__SquareRootFn(s__VarianceFn(V__L))))
&
((V__SD = s__SquareRootFn(s__VarianceFn(V__L)))
=>
(V__SD = s__StandardDeviationFn(V__L))))))
)
)

Weather.kif 15071512 
A real number is equal to The StandardDeviationFn of a list if and only if the real number is equal to the squareRoot of The VarianceFn the list 
( ! [V__SPEED,V__NUM] :
(((s__instance(V__SPEED,s__FunctionQuantity) &
s__instance(V__NUM,s__RealNumber))
=>
((((V__SPEED = s__MeasureFn(V__NUM,s__MilesPerHour))
=>
(V__SPEED = s__SpeedFn(s__MeasureFn(V__NUM,s__Mile),s__MeasureFn(n__1,s__HourDuration))))
&
((V__SPEED = s__SpeedFn(s__MeasureFn(V__NUM,s__Mile),s__MeasureFn(n__1,s__HourDuration)))
=>
(V__SPEED = s__MeasureFn(V__NUM,s__MilesPerHour))))))
)
)

Weather.kif 17011707 
A function quantity is equal to a real number miles per hour(s) if and only if the function quantity is equal to the real number mile(s) per 1 hour duration(s) 
( ! [V__Agent,V__Activity,V__ATIncome] :
(((s__instance(V__Agent,s__Human) &
s__instance(V__Activity,s__OrganizationalProcess) &
s__instance(V__ATIncome,s__Number) &
s__instance(V__ATIncome,s__CurrencyMeasure))
=>
(((( ? [V__Income, V__Tax, V__TaxAmount] :
((s__instance(V__Income,s__Number) &
s__instance(V__Income,s__CurrencyMeasure) &
s__instance(V__Tax,s__ChargingAFee) &
s__instance(V__TaxAmount,s__Number) &
s__instance(V__TaxAmount,s__CurrencyMeasure) &
(s__incomeEarned(V__Agent,V__Income,V__Activity)
&
s__amountCharged(V__Tax,V__TaxAmount)
&
s__causes(V__Activity,V__Tax)
&
(V__ATIncome = s__SubtractionFn(V__Income,V__TaxAmount))))))
=>
s__afterTaxIncome(V__Agent,V__ATIncome,V__Activity))
&
(s__afterTaxIncome(V__Agent,V__ATIncome,V__Activity)
=>
( ? [V__Income, V__Tax, V__TaxAmount] :
((s__instance(V__Income,s__Number) &
s__instance(V__Income,s__CurrencyMeasure) &
s__instance(V__Tax,s__ChargingAFee) &
s__instance(V__TaxAmount,s__Number) &
s__instance(V__TaxAmount,s__CurrencyMeasure) &
(s__incomeEarned(V__Agent,V__Income,V__Activity)
&
s__amountCharged(V__Tax,V__TaxAmount)
&
s__causes(V__Activity,V__Tax)
&
(V__ATIncome = s__SubtractionFn(V__Income,V__TaxAmount))))))))))
)
)

FinancialOntology.kif 32923299 
There exist a number, a chargingA fee and the chargingA feeAmount such that a human is income earned the number for an organizational process and the chargingA feeAmount is the amount charged in the chargingA fee and the organizational process causes the chargingA fee and a third number is equal to (the number and the chargingA feeAmount) if and only if the after tax income derived by the human from the organizational process is the third number 
( ! [V__Time,V__Option] :
(((s__instance(V__Time,s__Agent) &
s__instance(V__Time,s__TimePosition))
=>
(((( ? [V__Stock, V__StockPrice, V__StrikePrice] :
((s__instance(V__Stock,s__FinancialInstrument) &
s__instance(V__StockPrice,s__CurrencyMeasure) &
s__instance(V__StrikePrice,s__CurrencyMeasure) &
(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))
&
(s__atTheMoney(V__Option,V__Time)
=>
( ? [V__Stock, V__StockPrice, V__StrikePrice] :
((s__instance(V__Stock,s__FinancialInstrument) &
s__instance(V__StockPrice,s__CurrencyMeasure) &
s__instance(V__StrikePrice,s__CurrencyMeasure) &
(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)))))))))
)
)

FinancialOntology.kif 29953003 
There exist a financial instrument, the financial instrumentPrice and another currency measure such that an agreement is an instance of option and the financial instrument is an underlier of the agreement and the financial instrument is price the financial instrumentPrice for an agent and the other currency measure is a strike price of the agreement and the financial instrumentPrice is equal to the other currency measure if and only if the agent is an at the money of the agreement 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1292912939 

( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION,V__UNIT] :
(((s__instance(V__REGION,s__GeographicArea) &
s__instance(V__AMOUNT,s__ConstantQuantity) &
s__instance(V__TOTAL,s__RealNumber) &
s__instance(V__FRACTION,s__Number) &
s__instance(V__FRACTION,s__ConstantQuantity))
=>
(((s__arableLandArea(V__REGION,V__FRACTION)
&
s__greaterThanOrEqualTo(V__FRACTION,n__0)
&
s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))
&
s__instance(V__UNIT,s__UnitOfArea) &
(V__AMOUNT = s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT)))
=>
(s__arableLandArea(V__REGION,V__AMOUNT)))))
)
)

Geography.kif 20612068 

( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION] :
(((s__instance(V__REGION,s__GeographicArea) &
s__instance(V__AMOUNT,s__Number) &
s__instance(V__AMOUNT,s__ConstantQuantity) &
s__instance(V__FRACTION,s__Number) &
s__instance(V__FRACTION,s__ConstantQuantity))
=>
(((s__arableLandArea(V__REGION,V__FRACTION)
&
s__greaterThanOrEqualTo(V__FRACTION,n__0)
&
s__totalArea(V__REGION,V__TOTAL)
&
s__instance(V__TOTAL,s__AreaMeasure) &
(V__AMOUNT = s__MultiplicationFn(V__FRACTION,V__TOTAL)))
=>
(s__arableLandArea(V__REGION,V__AMOUNT)))))
)
)

Geography.kif 20522059 

No TPTP formula. May not be expressible in strict first order. 
ArabicCulture.kif 193212 

 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 = s__SubtractionFn(n__0,V__NUMBER1)))))
&
(((s__instance(V__NUMBER1,s__NonnegativeRealNumber) &
(V__NUMBER1 = V__NUMBER2))

(s__instance(V__NUMBER1,s__NegativeRealNumber) &
(V__NUMBER2 = s__SubtractionFn(n__0,V__NUMBER1))))
=>
((s__AbsoluteValueFn(V__NUMBER1)
= V__NUMBER2)
&
s__instance(V__NUMBER1,s__RealNumber) &
s__instance(V__NUMBER2,s__RealNumber))))
)
)

Merge.kif 45954606 
The absolute value of a real number is equal to a nonnegative real number and the real number is an instance of real number and the nonnegative real number is an instance of real number if and only if the real number is an instance of nonnegative real number and the real number is equal to the nonnegative real number or the real number is an instance of negative real number and the nonnegative real number is equal to (0 and the real number) 
( ! [V__LIST3,V__LIST1,V__LIST2] :
(((s__instance(V__LIST3,s__List) &
s__instance(V__LIST1,s__List) &
s__instance(V__LIST2,s__List))
=>
(((((V__LIST3 = s__ListConcatenateFn(V__LIST1,V__LIST2))
&
~((V__LIST1 = s__NullList))
&
~((V__LIST2 = s__NullList)))
=>
( ! [V__NUMBER1, V__NUMBER2] :
(((s__lessThanOrEqualTo(V__NUMBER1,s__ListLengthFn(V__LIST1))
&
s__lessThanOrEqualTo(V__NUMBER2,s__ListLengthFn(V__LIST2))
&
s__instance(V__NUMBER1,s__PositiveInteger) &
s__instance(V__NUMBER2,s__PositiveInteger))
=>
(((s__ListOrderFn(V__LIST3,V__NUMBER1)
= s__ListOrderFn(V__LIST1,V__NUMBER1))
&
(s__ListOrderFn(V__LIST3,s__AdditionFn(s__ListLengthFn(V__LIST1)
,V__NUMBER2))
= s__ListOrderFn(V__LIST2,V__NUMBER2))))))))
&
(( ! [V__NUMBER1, V__NUMBER2] :
(((s__lessThanOrEqualTo(V__NUMBER1,s__ListLengthFn(V__LIST1))
&
s__lessThanOrEqualTo(V__NUMBER2,s__ListLengthFn(V__LIST2))
&
s__instance(V__NUMBER1,s__PositiveInteger) &
s__instance(V__NUMBER2,s__PositiveInteger))
=>
(((s__ListOrderFn(V__LIST3,V__NUMBER1)
= s__ListOrderFn(V__LIST1,V__NUMBER1))
&
(s__ListOrderFn(V__LIST3,s__AdditionFn(s__ListLengthFn(V__LIST1)
,V__NUMBER2))
= s__ListOrderFn(V__LIST2,V__NUMBER2)))))))
=>
((V__LIST3 = s__ListConcatenateFn(V__LIST1,V__LIST2))
&
~((V__LIST1 = s__NullList))
&
~((V__LIST2 = s__NullList)))))))
)
)

Merge.kif 29792995 
A list is equal to the list composed of another list and a third list and the other list is not equal to null list and the third list is not equal to null list if and only if for all a positive integer and another positive integer 
( ! [V__AMOUNT,V__UNIT] :
(((s__instance(V__AMOUNT,s__Number) &
s__instance(V__AMOUNT,s__PhysicalQuantity))
=>
((((s__instance(V__UNIT,s__UnitOfMeasure) &
(V__AMOUNT = s__MeasureFn(n__1,s__SquareUnitFn(V__UNIT))))
=>
(V__AMOUNT = s__MultiplicationFn(s__MeasureFn(n__1,V__UNIT)
,s__MeasureFn(n__1,V__UNIT))))
&
((V__AMOUNT = s__MultiplicationFn(s__MeasureFn(n__1,V__UNIT)
,s__MeasureFn(n__1,V__UNIT)))
=>
(s__instance(V__UNIT,s__UnitOfMeasure) &
(V__AMOUNT = s__MeasureFn(n__1,s__SquareUnitFn(V__UNIT))))))))
)
)

Geography.kif 38043808 
An unit of measure is an instance of unit of measure and a number is equal to 1 the square unit of the unit of measure(s) if and only if the number is equal to 1 the unit of measure(s) and 1 the unit of measure(s) 
( ! [V__MUSIC] :
(((s__instance(V__MUSIC,s__Object) &
s__instance(V__MUSIC,s__Process))
=>
(((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)))))
&
(( ? [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))))
=>
s__attribute(V__MUSIC,s__PolyphonicMusic)))))
)
)

Midlevelontology.kif 695706 
Polyphonic music is an attribute of an object if and only if there exist a process and another process such that the object is an instance of making music and the process is an instance of making music and the other process is an instance of making music and the process is a subprocess of the object and the other process is a subprocess of the object and the process is not equal to the other process and the process occurs at the same time as the object and the other process occurs at the same time as the object 
( ! [V__LASTPLACE,V__LIST1,V__AVERAGE] :
(((s__instance(V__LASTPLACE,s__PositiveInteger) &
s__instance(V__LIST1,s__List) &
s__instance(V__AVERAGE,s__RealNumber))
=>
(((s__average(V__LIST1,V__AVERAGE)
=>
( ? [V__LIST2] :
((s__instance(V__LIST2,s__List) &
((s__ListLengthFn(V__LIST2)
= s__ListLengthFn(V__LIST1))
&
(s__ListOrderFn(V__LIST2,n__1)
= s__ListOrderFn(V__LIST1,n__1))
&
( ! [V__ITEMFROM2] :
((s__instance(V__ITEMFROM2,s__PositiveInteger) =>
((s__inList(V__ITEMFROM2,V__LIST2)
=>
(( ? [V__POSITION, V__POSITIONMINUSONE, V__ITEMFROM1, V__PRIORFROM2] :
((s__instance(V__POSITION,s__Number) &
s__instance(V__POSITIONMINUSONE,s__Number) &
s__instance(V__ITEMFROM1,s__PositiveInteger) &
s__instance(V__PRIORFROM2,s__PositiveInteger) &
(s__greaterThan(V__POSITION,n__1)
&
s__lessThanOrEqualTo(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 = s__SubtractionFn(V__POSITION,n__1))
&
(V__POSITIONMINUSONE = s__ListOrderFn(V__LIST2,V__PRIORFROM2))
&
(V__ITEMFROM2 = s__AdditionFn(V__ITEMFROM1,V__PRIORFROM2))))))))))))
&
(V__LASTPLACE = s__ListLengthFn(V__LIST2))
&
(V__AVERAGE = s__DivisionFn(s__ListOrderFn(V__LIST2,V__LASTPLACE)
,V__LASTPLACE)))))))
&
(( ? [V__LIST2] :
((s__instance(V__LIST2,s__List) &
((s__ListLengthFn(V__LIST2)
= s__ListLengthFn(V__LIST1))
&
(s__ListOrderFn(V__LIST2,n__1)
= s__ListOrderFn(V__LIST1,n__1))
&
( ! [V__ITEMFROM2] :
((s__instance(V__ITEMFROM2,s__PositiveInteger) =>
((s__inList(V__ITEMFROM2,V__LIST2)
=>
(( ? [V__POSITION, V__POSITIONMINUSONE, V__ITEMFROM1, V__PRIORFROM2] :
((s__instance(V__POSITION,s__Number) &
s__instance(V__POSITIONMINUSONE,s__Number) &
s__instance(V__ITEMFROM1,s__PositiveInteger) &
s__instance(V__PRIORFROM2,s__PositiveInteger) &
(s__greaterThan(V__POSITION,n__1)
&
s__lessThanOrEqualTo(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 = s__SubtractionFn(V__POSITION,n__1))
&
(V__POSITIONMINUSONE = s__ListOrderFn(V__LIST2,V__PRIORFROM2))
&
(V__ITEMFROM2 = s__AdditionFn(V__ITEMFROM1,V__PRIORFROM2))))))))))))
&
(V__LASTPLACE = s__ListLengthFn(V__LIST2))
&
(V__AVERAGE = s__DivisionFn(s__ListOrderFn(V__LIST2,V__LASTPLACE)
,V__LASTPLACE))))))
=>
s__average(V__LIST1,V__AVERAGE)))))
)
)

People.kif 285306 
A real number is an average of a list if and only if there exists another list such that length of the other list is equal to length of the list and 1th element of the other list is equal to 1th element of the list and for all a positive integer and a fourth positive integer is equal to length of the other list and the real number is equal to the fourth positive integerth element of the other list and the fourth positive integer 
( ! [V__P,V__P2,V__N1,V__R,V__N2,V__BG,V__N] :
(((s__instance(V__P,s__Physical) &
s__instance(V__P2,s__Physical) &
s__instance(V__N1,s__Integer) &
s__instance(V__R,s__GeographicArea) &
s__instance(V__N2,s__Integer) &
s__instance(V__BG,s__BeliefGroup) &
s__instance(V__N,s__RealNumber))
=>
(((s__beliefGroupPercentInRegion(V__BG,V__N,V__R)
=>
( ? [V__G1, V__G2] :
((s__instance(V__G1,s__Collection) &
s__instance(V__G2,s__Collection) &
(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)
&
(s__DivisionFn(V__N,n__100)
= s__DivisionFn(V__N1,V__N2)))))))
&
(( ? [V__G1, V__G2] :
((s__instance(V__G1,s__Collection) &
s__instance(V__G2,s__Collection) &
(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)
&
(s__DivisionFn(V__N,n__100)
= s__DivisionFn(V__N1,V__N2))))))
=>
s__beliefGroupPercentInRegion(V__BG,V__N,V__R)))))
)
)

People.kif 15311542 
A real number percent of people in a geographic area believe in a belief group if and only if there exist a collection and another collection such that a physical is located at the geographic area and the physical is a member of the belief group and the physical is a member of the collection and the real number1 is a member count of the collection and the physical2 is located at the geographic area and the physical2 is a member of the other collection and the real number2 is a member count of the other collection and the real number and 100 is equal to the real number1 and the real number2 
( ! [V__R,V__E,V__MAX,V__MIN,V__M] :
(((s__instance(V__R,s__RealNumber) &
s__instance(V__E,s__Engine) &
s__instance(V__MAX,s__RealNumber) &
s__instance(V__MIN,s__RealNumber) &
s__instance(V__M,s__UnitOfMeasure))
=>
(((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 = s__DivisionFn(V__MIN,V__MAX))))
&
((s__minCylinderVolume(V__E,s__MeasureFn(V__MIN,V__M))
&
s__maxCylinderVolume(V__E,s__MeasureFn(V__MAX,V__M))
&
(V__R = s__DivisionFn(V__MIN,V__MAX)))
=>
s__compressionRatio(V__E,V__R)))))
)
)

Cars.kif 19281933 
The compression ratio of an engine is a real number if and only if the minimum volume of the cylinders in the engine the engine is another real number an unit of measure(s) and the maximum volume of the cylinders in the engine the engine is the unit of measureAX the unit of measure(s) and the real number is equal to the other real number and the unit of measureAX 
( ! [V__PHYS1,V__PHYS2] :
(((s__instance(V__PHYS1,s__Physical) &
s__instance(V__PHYS2,s__Physical))
=>
(((s__cooccur(V__PHYS1,V__PHYS2)
=>
(s__WhenFn(V__PHYS1)
= s__WhenFn(V__PHYS2)))
&
((s__WhenFn(V__PHYS1)
= s__WhenFn(V__PHYS2))
=>
s__cooccur(V__PHYS1,V__PHYS2)))))
)
)

Merge.kif 80118013 
A physical occurs at the same time as another physical if and only if the time of existence of the physical is equal to the time of existence of the other physical 
No TPTP formula. May not be expressible in strict first order. 
People.kif 104117 
The births per thousand of a geopolitical area and the year an integer is equal to a real number if and only if the population of the geopolitical area and 1000 is equal to a number and another integer is equal to the number of instances in the class described by a symbolic string and the other integer and the number is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
People.kif 138151 
The deaths per thousand of a geopolitical area and the year an integer is equal to a real number if and only if the population of the geopolitical area and 1000 is equal to a number and another integer is equal to the number of instances in the class described by a symbolic string and the other integer and the number is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
People.kif 253277 
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 number 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 number is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
People.kif 411442 
The female life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list 
( ! [V__LIST,V__ITEM] :
((s__instance(V__LIST,s__List) =>
((((s__LastFn(V__LIST)
= V__ITEM)
=>
( ? [V__NUMBER] :
((s__instance(V__NUMBER,s__PositiveInteger) &
((s__ListLengthFn(V__LIST)
= V__NUMBER)
&
(s__ListOrderFn(V__LIST,V__NUMBER)
= V__ITEM))))))
&
(( ? [V__NUMBER] :
((s__instance(V__NUMBER,s__PositiveInteger) &
((s__ListLengthFn(V__LIST)
= V__NUMBER)
&
(s__ListOrderFn(V__LIST,V__NUMBER)
= V__ITEM)))))
=>
(s__LastFn(V__LIST)
= V__ITEM)))))
)
)

Merge.kif 31073112 
The last of a list is equal to an entity if and only if there exists a positive integer such that length of the list is equal to the positive integer and the positive integerth element of the list is equal to the entity 
No TPTP formula. May not be expressible in strict first order. 
People.kif 323353 
The life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list 
No TPTP formula. May not be expressible in strict first order. 
People.kif 367398 
The male life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list 
No TPTP formula. May not be expressible in strict first order. 
People.kif 221238 
The male to female ratio of a geopolitical area is equal to a real number if and only if an integer is equal to the number of instances in the class described by a symbolic string and another integer is equal to the number of instances in the class described by another symbolic string and the integer and the other integer is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
People.kif 174202 
The migrants per thousand of a geopolitical area and the year an integer is equal to a real number if and only if (the integer and a number) is equal to 1 and the population of the geopolitical area is equal to another number holds during the year the integer and the other number and 1000 is equal to a third number and another integer is equal to the number of instances in the class described by a symbolic string and a third integer is equal to the number of instances in the class described by the symbolic string and (the other integer and the third integer) is equal to a fourth number and the fourth number and the third number is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
People.kif 7786 
The population growth of a geopolitical area and the year an integer is equal to a real number if and only if (the integer and another integer) is equal to 1 and the population of the geopolitical area is equal to a number holds during the year the integer and the population of the geopolitical area is equal to another number holds during the year the other integer and the number and the other number is equal to a third number and (the third number and 1) is equal to the real number 
( ! [V__NUMBER1,V__NUMBER2,V__NUMBER] :
(((s__instance(V__NUMBER1,s__Integer) &
s__instance(V__NUMBER2,s__Integer) &
s__instance(V__NUMBER,s__Integer))
=>
((((s__RemainderFn(V__NUMBER1,V__NUMBER2)
= V__NUMBER)
=>
(s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
,V__NUMBER2)
,V__NUMBER)
= V__NUMBER1))
&
((s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
,V__NUMBER2)
,V__NUMBER)
= V__NUMBER1)
=>
(s__RemainderFn(V__NUMBER1,V__NUMBER2)
= V__NUMBER)))))
)
)

Merge.kif 49084910 
An integer mod another integer is equal to a third integer if and only if (the largest integer less than or equal to the integer and the other integer and the other integer and the third integer) is equal to the integer 
( ! [V__SD,V__L] :
(((s__instance(V__SD,s__RealNumber) &
s__instance(V__L,s__List))
=>
((((V__SD = s__StandardDeviationFn(V__L))
=>
(V__SD = s__SquareRootFn(s__VarianceFn(V__L))))
&
((V__SD = s__SquareRootFn(s__VarianceFn(V__L)))
=>
(V__SD = s__StandardDeviationFn(V__L))))))
)
)

Weather.kif 15071512 
A real number is equal to The StandardDeviationFn of a list if and only if the real number is equal to the squareRoot of The VarianceFn the list 
( ! [V__SPEED,V__NUM] :
(((s__instance(V__SPEED,s__FunctionQuantity) &
s__instance(V__NUM,s__RealNumber))
=>
((((V__SPEED = s__MeasureFn(V__NUM,s__MilesPerHour))
=>
(V__SPEED = s__SpeedFn(s__MeasureFn(V__NUM,s__Mile),s__MeasureFn(n__1,s__HourDuration))))
&
((V__SPEED = s__SpeedFn(s__MeasureFn(V__NUM,s__Mile),s__MeasureFn(n__1,s__HourDuration)))
=>
(V__SPEED = s__MeasureFn(V__NUM,s__MilesPerHour))))))
)
)

Weather.kif 17011707 
A function quantity is equal to a real number miles per hour(s) if and only if the function quantity is equal to the real number mile(s) per 1 hour duration(s) 
( ! [V__P,V__P2,V__N1,V__R,V__N2,V__BG,V__N] :
(((s__instance(V__P,s__Physical) &
s__instance(V__P2,s__Physical) &
s__instance(V__N1,s__Integer) &
s__instance(V__R,s__GeographicArea) &
s__instance(V__N2,s__Integer) &
s__instance(V__BG,s__EthnicGroup) &
s__instance(V__N,s__RealNumber))
=>
(((s__ethnicityPercentInRegion(V__BG,V__N,V__R)
=>
( ? [V__G1, V__G2] :
((s__instance(V__G1,s__Collection) &
s__instance(V__G2,s__Collection) &
(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)
&
(s__DivisionFn(V__N,n__100)
= s__DivisionFn(V__N1,V__N2)))))))
&
(( ? [V__G1, V__G2] :
((s__instance(V__G1,s__Collection) &
s__instance(V__G2,s__Collection) &
(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)
&
(s__DivisionFn(V__N,n__100)
= s__DivisionFn(V__N1,V__N2))))))
=>
s__ethnicityPercentInRegion(V__BG,V__N,V__R)))))
)
)

People.kif 15501561 
A real number percent of people in a geographic area are an ethnic group if and only if there exist a collection and another collection such that a physical is located at the geographic area and the physical is a member of the ethnic group and the physical is a member of the collection and the real number1 is a member count of the collection and the physical2 is located at the geographic area and the physical2 is a member of the other collection and the real number2 is a member count of the other collection and the real number and 100 is equal to the real number1 and the real number2 
( ! [V__INTERVAL2,V__INTERVAL1] :
(((s__instance(V__INTERVAL2,s__TimeInterval) &
s__instance(V__INTERVAL1,s__TimeInterval))
=>
(((s__finishes(V__INTERVAL1,V__INTERVAL2)
=>
(s__before(s__BeginFn(V__INTERVAL2)
,s__BeginFn(V__INTERVAL1))
&
(s__EndFn(V__INTERVAL2)
= s__EndFn(V__INTERVAL1))))
&
((s__before(s__BeginFn(V__INTERVAL2)
,s__BeginFn(V__INTERVAL1))
&
(s__EndFn(V__INTERVAL2)
= s__EndFn(V__INTERVAL1)))
=>
s__finishes(V__INTERVAL1,V__INTERVAL2)))))
)
)

Merge.kif 77997807 
A time interval finishes another time interval if and only if the beginning of the other time interval happens before the beginning of the time interval and the end of the other time interval is equal to the end of the time interval 
( ! [V__NUMBER1,V__NUMBER2] :
(((s__instance(V__NUMBER1,s__Quantity) &
s__instance(V__NUMBER2,s__Quantity))
=>
(((s__greaterThanOrEqualTo(V__NUMBER1,V__NUMBER2)
=>
((V__NUMBER1 = V__NUMBER2)

s__greaterThan(V__NUMBER1,V__NUMBER2)))
&
(((V__NUMBER1 = V__NUMBER2)

s__greaterThan(V__NUMBER1,V__NUMBER2))
=>
s__greaterThanOrEqualTo(V__NUMBER1,V__NUMBER2)))))
)
)

Merge.kif 17991803 
A quantity is greater than or equal to another quantity if and only if the quantity is equal to the other quantity or the quantity is greater than the other quantity 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 2892128934 
Alone is an attribute of an entity holds during a time interval if and only if there don't exist the entity2 and a process such that the entity is not equal to the entity2 and the entity2 is an instance of agent and the process is an instance of social interaction and the time of existence of the process takes place during the time interval and the entity is an involved in event of the process and the entity2 is an involved in event of the process 
 Display limited to 25 items. Show next 25 
 Display limited to 25 items. Show next 25 
statement


No TPTP formula. May not be expressible in strict first order. 
Military.kif 928941 
The reaching military age annually male of a geopolitical area and a year is equal to the number of instances in the class described by a symbolic string 
( ! [V__NUMBER] :
((s__instance(V__NUMBER,s__RealNumber) =>
((s__MeasureFn(V__NUMBER,s__OunceMass) = s__MeasureFn(s__DivisionFn(V__NUMBER,n__16)
,s__PoundMass))))))

Midlevelontology.kif 1218912192 
For all a real number the real number Ounce(s) is equal to the real number and 16 pound mass(s) 
( ! [V__NUMBER] :
((s__instance(V__NUMBER,s__Integer) =>
((s__PredecessorFn(V__NUMBER)
= s__SubtractionFn(V__NUMBER,n__1))))))

Merge.kif 45634564 
For all an integer (the integer+2) is equal to (the integer and 1) 
( ! [V__NUMBER] :
((s__instance(V__NUMBER,s__Integer) =>
((s__SuccessorFn(V__NUMBER)
= s__AdditionFn(V__NUMBER,n__1))))))

Merge.kif 45474548 
For all an integer (the integer+1) is equal to (the integer and 1) 
( ! [V__ROW2, V__ROW3, V__ITEM] :
((s__ListLengthFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ITEM))
= s__SuccessorFn(s__ListLengthFn(s__ListFn__2Fn(V__ROW2,V__ROW3))))))
( ! [V__ROW2, V__ITEM] :
((s__ListLengthFn(s__ListFn__2Fn(V__ROW2,V__ITEM))
= s__SuccessorFn(s__ListLengthFn(s__ListFn__1Fn(V__ROW2))))))
( ! [V__ROW2, V__ROW3, V__ROW4, V__ROW5, V__ITEM] :
((s__ListLengthFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ITEM))
= s__SuccessorFn(s__ListLengthFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))))))
( ! [V__ROW2, V__ROW3, V__ROW4, V__ITEM] :
((s__ListLengthFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ITEM))
= s__SuccessorFn(s__ListLengthFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))))))
( ! [V__ROW2, V__ROW3, V__ROW4, V__ROW5, V__ROW6, V__ROW7, V__ITEM] :
((s__ListLengthFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ITEM))
= s__SuccessorFn(s__ListLengthFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))))))
( ! [V__ROW2, V__ROW3, V__ROW4, V__ROW5, V__ROW6, V__ITEM] :
((s__ListLengthFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ITEM))
= s__SuccessorFn(s__ListLengthFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))))))

Merge.kif 29332936 
For all @ROW and another entity length of (@ROW and the other entity) is equal to (length of (@ROW)+1) 
( ! [V__ROW2, V__ITEM] :
((s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ITEM)
,s__ListLengthFn(s__ListFn__2Fn(V__ROW2,V__ITEM)))
= V__ITEM)))
( ! [V__ROW2, V__ROW3, V__ROW4, V__ROW5, V__ITEM] :
((s__ListOrderFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ITEM)
,s__ListLengthFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ITEM)))
= V__ITEM)))
( ! [V__ROW2, V__ROW3, V__ROW4, V__ITEM] :
((s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ITEM)
,s__ListLengthFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ITEM)))
= V__ITEM)))
( ! [V__ROW2, V__ROW3, V__ITEM] :
((s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ITEM)
,s__ListLengthFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ITEM)))
= V__ITEM)))
( ! [V__ROW2, V__ROW3, V__ROW4, V__ROW5, V__ROW6, V__ROW7, V__ITEM] :
((s__ListOrderFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ITEM)
,s__ListLengthFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ITEM)))
= V__ITEM)))
( ! [V__ROW2, V__ROW3, V__ROW4, V__ROW5, V__ROW6, V__ITEM] :
((s__ListOrderFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ITEM)
,s__ListLengthFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ITEM)))
= V__ITEM)))

Merge.kif 29382942 
For all @ROW and another entity length of (@ROW and the other entity)th element of (@ROW and the other entity) is equal to the other entity 
~((s__BigSix = s__GroupOf6))

Government.kif 28862886 
Big six is not equal to group of6 
appearance as argument number 0


( ! [V__X] :
(((s__instance(V__X,s__RealNumber) &
s__instance(V__X,s__PlaneAngleMeasure))
=>
((s__ArcCosineFn(s__CosineFn(V__X))
= V__X)))
)
)

Merge.kif 50315031 
The arccosine of the cosine of a real number is equal to the real number 
( ! [V__X] :
(((s__instance(V__X,s__RealNumber) &
s__instance(V__X,s__PlaneAngleMeasure))
=>
((s__ArcSineFn(s__SineFn(V__X))
= V__X)))
)
)

Merge.kif 50415041 
The arcsine of the sine of a real number is equal to the real number 
( ! [V__X] :
(((s__instance(V__X,s__RealNumber) &
s__instance(V__X,s__PlaneAngleMeasure))
=>
((s__ArcTangentFn(s__TangentFn(V__X))
= V__X)))
)
)

Merge.kif 50215021 
The arctan of the tangent of a real number is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
Military.kif 867876 
The available for military service male of a geopolitical area is equal to the number of instances in the class described by a symbolic string 
(s__BeginFn(s__BeforeCommonEra) = s__NegativeInfinity)

Midlevelontology.kif 74467446 
The beginning of before common era is equal to negative infinity 
(s__CardinalityFn(s__Continent) = n__7)

Merge.kif 1351113511 
The number of instances in continent is equal to 7 
(s__CardinalityFn(s__NativityMagi) = n__3)

Media.kif 20052005 
The number of instances in NativityMagi is equal to 3 
No TPTP formula. May not be expressible in strict first order. 
People.kif 462472 
The children born per woman of a geopolitical area and the year an integer is equal to the number of instances in the class described by a symbolic string 
(s__EndFn(s__CommonEra) = s__PositiveInfinity)

Midlevelontology.kif 74547454 
The end of common era is equal to positive infinity 
No TPTP formula. May not be expressible in strict first order. 
Military.kif 890901 
The fit for military service male of a geopolitical area is equal to the number of instances in the class described by a symbolic string 
(s__MeasureFn(n__0_0,s__AngularDegree) = s__MeasureFn(n__360_0,s__AngularDegree))

Merge.kif 71307130 
0.0 Angular degree(s) is equal to 360.0 angular degree(s) 
(s__MeasureFn(n__1,s__AngularDegree) = s__MeasureFn(n__60,s__ArcMinute))

Geography.kif 382382 
1 Angular degree(s) is equal to 60 arc minute(s) 
(s__MeasureFn(n__1,s__ArcMinute) = s__MeasureFn(n__60,s__ArcSecond))

Geography.kif 401401 
1 Arc minute(s) is equal to 60 arc second(s) 
(s__MeasureFn(n__1,s__CubicFoot) = s__MultiplicationFn(s__MeasureFn(n__1,s__FootLength),s__MultiplicationFn(s__MeasureFn(n__1,s__FootLength),s__MeasureFn(n__1,s__FootLength))))

Midlevelontology.kif 1249012496 
1 Cubic foot(s) is equal to 1 foot length(s) and 1 foot length(s) and 1 foot length(s) 
(s__MeasureFn(n__1,s__Fathom) = s__MeasureFn(n__6,s__FootLength))

Geography.kif 37203720 
1 Fathom(s) is equal to 6 foot length(s) 
(s__MeasureFn(n__1,s__KilowattHour) = s__MeasureFn(n__3_6,s__MegaFn(s__Joule)))

Economy.kif 20122012 
1 Kilowatt hour(s) is equal to 3.6 1 million joules(s) 
(s__MeasureFn(n__1,s__KilowattHour) = s__MeasureFn(n__3600000,s__Joule))

Economy.kif 20132013 
1 Kilowatt hour(s) is equal to 3600000 joule(s) 
(s__MeasureFn(n__1,s__MetricTon) = s__MeasureFn(n__2205,s__PoundMass))

Midlevelontology.kif 1246212464 
1 Metric ton(s) is equal to 2205 pound mass(s) 
(s__MeasureFn(n__1,s__NauticalMile) = s__MeasureFn(n__1852,s__Meter))

Geography.kif 37403740 
1 Nautical mile(s) is equal to 1852 meter(s) 
(s__MeasureFn(n__1,s__NauticalMile) = s__MeasureFn(n__6076_1,s__FootLength))

Geography.kif 37393739 
1 Nautical mile(s) is equal to 6076.1 foot length(s) 
(s__MeasureFn(n__1,s__SquareKilometer) = s__MultiplicationFn(s__MeasureFn(n__1,s__KiloFn(s__Meter))
,s__MeasureFn(n__1,s__KiloFn(s__Meter))))

Geography.kif 624625 
1 Square kilometer(s) is equal to 1 1 thousand meters(s) and 1 1 thousand meters(s) 
(s__MeasureFn(n__1,s__SquareMeter) = s__MultiplicationFn(s__MeasureFn(n__1,s__Meter),s__MeasureFn(n__1,s__Meter)))

Geography.kif 37923793 
1 Square meter(s) is equal to 1 meter(s) and 1 meter(s) 
(s__MeasureFn(n__1,s__SquareMile) = s__PerFn(s__MeasureFn(n__1,s__Mile),s__MeasureFn(n__1,s__Mile)))

Midlevelontology.kif 1254612550 
1 Square mile(s) is equal to the per of 1 mile(s) and 1 mile(s) 
(s__MeasureFn(n__1,s__SquareYard) = s__PerFn(s__MeasureFn(n__1,s__YardLength),s__MeasureFn(n__1,s__YardLength)))

Midlevelontology.kif 1255612560 
1 Square yard(s) is equal to the per of 1 yard length(s) and 1 yard length(s) 
( ! [V__DEG] :
((s__instance(V__DEG,s__RealNumber) =>
((s__MeasureFn(V__DEG,s__ArcMinute) = s__MeasureFn(s__MultiplicationFn(n__60,V__DEG)
,s__ArcSecond))))
)
)

Geography.kif 402402 
A real number arc minute(s) is equal to 60 and the real number arc second(s) 
 Display limited to 25 items. Show next 25 
 Display limited to 25 items. Show next 25 

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