(<=>
(attribute ?WATER OpenSea)
(and
(instance ?WATER SaltWaterArea)
(not
(instance ?WATER LandlockedWater))
(distance ?LAND ?WATER
(MeasureFn ?DIST NauticalMile))
(greaterThan ?DIST 5.0))) 
Geography.kif 46144622 
Open sea is an attribute of an object if and only if the object is an instance of salt water area and the object is not an instance of landlocked water and the distance between a physical and the object is a real number nautical mile(s) and the real number is greater than 5.0 
(<=>
(average ?LIST1 ?AVERAGE)
(exists (?LIST2 ?LASTPLACE)
(and
(equal
(ListLengthFn ?LIST2)
(ListLengthFn ?LIST1))
(equal
(ListOrderFn ?LIST2 1)
(ListOrderFn ?LIST1 1))
(forall (?ITEMFROM2)
(=>
(inList ?ITEMFROM2 ?LIST2)
(exists (?POSITION ?POSITIONMINUSONE ?ITEMFROM1 ?PRIORFROM2)
(and
(greaterThan ?POSITION 1)
(lessThanOrEqualTo ?POSITION
(ListLengthFn ?LIST2))
(equal
(ListOrderFn ?LIST2 ?ITEMFROM2) ?POSITION)
(inList ?ITEMFROM1 ?LIST1)
(equal ?POSITION
(ListOrderFn ?LIST1 ?ITEMFROM1))
(inList ?PRIORFROM2 ?LIST2)
(equal ?POSITIONMINUSONE
(SubtractionFn ?POSITION 1))
(equal ?POSITIONMINUSONE
(ListOrderFn ?LIST2 ?PRIORFROM2))
(equal ?ITEMFROM2
(AdditionFn ?ITEMFROM1 ?PRIORFROM2))))))
(equal ?LASTPLACE
(ListLengthFn ?LIST2))
(equal ?AVERAGE
(DivisionFn
(ListOrderFn ?LIST2 ?LASTPLACE) ?LASTPLACE))))) 
People.kif 298319 
A real number is an average of a list if and only if there exist another list and a positive integer 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 another positive integer and the positive integer is equal to length of the other list and the real number is equal to the positive integerth element of the other list and the positive integer 
(<=>
(greaterThanOrEqualTo ?NUMBER1 ?NUMBER2)
(or
(equal ?NUMBER1 ?NUMBER2)
(greaterThan ?NUMBER1 ?NUMBER2))) 
Merge.kif 18721876 
A real number is greater than or equal to another real number if and only if the real number is equal to the other real number or the real number is greater than the other real number 
(<=>
(instance ?NUMBER PositiveRealNumber)
(and
(greaterThan ?NUMBER 0)
(instance ?NUMBER RealNumber))) 
Merge.kif 19241928 
A real number is an instance of positive real number if and only if the real number is greater than 0 and the real number is an instance of real number 
(<=>
(larger ?OBJ1 ?OBJ2)
(forall (?QUANT1 ?QUANT2 ?UNIT)
(=>
(and
(measure ?OBJ1
(MeasureFn ?QUANT1 ?UNIT))
(measure ?OBJ2
(MeasureFn ?QUANT2 ?UNIT))
(instance ?UNIT UnitOfLength))
(greaterThan ?QUANT1 ?QUANT2)))) 
Merge.kif 77447752 
An object is larger than another object if and only if for all a real number, another real number and an unit of measure 
(=>
(and
(attribute ?AREA FlatTerrain)
(part ?ZONE ?AREA)
(slopeGradient ?ZONE ?SLOPE))
(greaterThan 0.005 ?SLOPE)) 
Geography.kif 17521757 

(=>
(and
(attribute ?AREA LowTerrain)
(part ?ZONE ?AREA)
(slopeGradient ?ZONE ?SLOPE))
(greaterThan 0.03 ?SLOPE)) 
Geography.kif 17641769 

(=>
(and
(attribute ?FOOD1 FamilyStylePortion)
(measure ?FOOD1
(MeasureFn ?MEAS1 ?U))
(not
(attribute ?FOOD2 FamilyStylePortion))
(measure ?FOOD2
(MeasureFn ?MEAS2 ?U))
(instance ?FOOD1 ?CLASS)
(instance ?FOOD2 ?CLASS)
(instance ?U UnitOfMeasure))
(greaterThan ?MEAS1 ?MEAS2)) 
Dining.kif 11651176 

(=>
(and
(attribute ?H Muslim)
(equal
(WealthFn ?H) ?W))
(modalAttribute
(exists (?Z ?T ?U ?Y ?C)
(and
(instance ?Z Zakat)
(instance ?Y Year)
(during ?Y
(WhenFn ?H))
(holdsDuring ?Y
(attribute ?H FullyFormed))
(agent ?Z ?H)
(patient ?Z ?T)
(monetaryValue ?T
(MeasureFn ?C ?U))
(instance ?U UnitOfCurrency)
(greaterThan ?C
(MultiplicationFn ?W 0.025)))) Obligation)) 
ArabicCulture.kif 204223 

(=>
(and
(attribute ?ROOM Oversized)
(immediateInstance ?ROOM ?HOTELUNIT)
(subclass ?HOTELUNIT HotelUnit))
(exists (?NORMAL ?AREA1 ?AREA2 ?U)
(and
(immediateInstance ?NORMAL ?HOTELUNIT)
(instance ?U UnitOfArea)
(measure ?NORMAL
(MeasureFn ?AREA1 ?U))
(measure ?ROOM
(MeasureFn ?AREA2 ?U))
(instance ?AREA1 AreaMeasure)
(instance ?AREA2 AreaMeasure)
(greaterThan ?AREA2 ?AREA1)))) 
Hotel.kif 11861201 

(=>
(and
(birthdate ?A ?DAY)
(instance ?DAY
(DayFn ?D
(MonthFn ?M
(YearFn ?Y)))))
(exists (?CLASS ?FUTURE)
(and
(birthday ?A ?CLASS)
(subclass ?CLASS Day)
(instance ?FUTURE Integer)
(equal ?CLASS
(DayFn ?D
(MonthFn ?M
(YearFn ?FUTURE))))
(greaterThan ?FUTURE ?Y)))) 
Midlevelontology.kif 2431224322 

(=>
(and
(capitalExpendituresOfAreaInPeriod ?AREA
(MeasureFn ?CAPAMOUNT ?UNIT) ?PERIOD)
(annualExpendituresOfAreaInPeriod ?AREA
(MeasureFn ?TOTALAMOUNT ?UNIT) ?PERIOD))
(greaterThan ?TOTALAMOUNT ?CAPAMOUNT)) 
Economy.kif 15541560 

(=>
(and
(climateTypeInArea ?AREA ColdClimateZone)
(forall (?MO)
(and
(instance ?MO Month)
(averageTemperatureForPeriod ?AREA ?MO
(MeasureFn ?TEMP CelsiusDegree)))))
(greaterThan 10.0 ?TEMP)) 
Geography.kif 15211529 

(=>
(and
(climateTypeInArea ?AREA PolarTypeFClimateZone)
(instance ?TIME TimePosition)
(holdsDuring ?TIME
(airTemperature ?AREA
(MeasureFn ?TEMP CelsiusDegree))))
(holdsDuring ?TIME
(greaterThan 10.0 ?TEMP))) 
Geography.kif 15951601 

(=>
(and
(dampingRatio ?P ?R)
(greaterThan ?R 0)
(instance ?T Tremor)
(patient ?T ?P)
(instance ?U UnitOfLength)
(holdsDuring ?T1
(physicalAmplitude ?T
(MeasureFn ?A1 ?U)))
(holdsDuring ?T2
(physicalAmplitude ?T
(MeasureFn ?A2 ?U)))
(during ?T1 ?T)
(during ?T2 ?T)
(earlier ?T1 ?T2))
(greaterThan ?A1 ?A2)) 
Cars.kif 809825 

(=>
(and
(defaultMaxValue ?REL ?ARG ?N)
(?REL @ARGS)
(equal ?VAL
(ListOrderFn
(ListFn @ARGS) ?ARG)))
(modalAttribute
(greaterThan ?N ?VAL) Likely)) 
Merge.kif 1832718332 

(=>
(and
(defaultMaximumMeasure ?OBJECT
(MeasureFn ?Q ?UNIT))
(instance ?UNIT CompositeUnitOfMeasure))
(modalAttribute
(exists (?INST ?QUANTITY)
(and
(instance ?INST ?OBJECT)
(measure ?INST
(MeasureFn ?QUANTITY ?UNIT))
(greaterThan ?QUANTITY ?Q))) Unlikely)) 
Midlevelontology.kif 1340613415 

(=>
(and
(defaultMaximumMeasure ?OBJECT
(MeasureFn ?Q ?UNIT1))
(subclass ?UNITCLASS NonCompositeUnitOfMeasure)
(instance ?UNIT1 ?UNITCLASS))
(modalAttribute
(exists (?INST ?QUANTITY ?UNIT2)
(and
(instance ?INST ?OBJECT)
(measure ?INST
(MeasureFn ?QUANTITY ?UNIT2))
(instance ?UNIT2 ?UNITCLASS)
(greaterThan
(MeasureFn ?QUANTITY ?UNIT2)
(MeasureFn ?Q ?UNIT1)))) Unlikely)) 
Midlevelontology.kif 1341713428 

(=>
(and
(defaultMaximumSphereRadius ?OBJECT
(MeasureFn ?R ?U))
(instance ?INST ?OBJECT)
(attribute ?INST Sphere))
(modalAttribute
(exists (?RADIUS)
(and
(sphereRadius ?INST
(MeasureFn ?RADIUS ?U))
(greaterThan ?RADIUS ?R))) Unlikely)) 
Midlevelontology.kif 1335613367 

(=>
(and
(defaultMeasure ?OBJECT
(MeasureFn ?Q ?UNIT))
(instance ?UNIT CompositeUnitOfMeasure))
(modalAttribute
(exists (?INST ?QUANTITY)
(and
(instance ?INST ?OBJECT)
(measure ?INST
(MeasureFn ?QUANTITY ?UNIT))
(greaterThan ?QUANTITY
(MultiplicationFn ?Q 1.5)))) Unlikely)) 
Midlevelontology.kif 1343613445 

(=>
(and
(defaultMinValue ?REL ?ARG ?N)
(?REL @ARGS)
(equal ?VAL
(ListOrderFn
(ListFn @ARGS) ?ARG)))
(modalAttribute
(greaterThan ?VAL ?N) Likely)) 
Merge.kif 1831018315 

(=>
(and
(engineIdleSpeed ?E
(RotationFn
(MeasureFn ?N1 MilesPerHour) ?M))
(instance ?A Automobile)
(instance ?P GasPedal)
(instance ?P Pushing)
(destination ?P ?GP)
(part ?E ?A)
(part ?GP ?A)
(instance ?C Crankshaft)
(part ?C ?E)
(holdsDuring
(WhenFn ?P)
(measure ?C
(RotationFn
(MeasureFn ?N2 MilesPerHour) ?M))))
(modalAttribute
(greaterThan ?N2 ?N1) Likely)) 
Cars.kif 25852603 

(=>
(and
(equal
(GreatestCommonDivisorFn @ROW) ?NUMBER)
(not
(equal ?NUMBER 0)))
(not
(exists (?GREATER)
(and
(greaterThan ?GREATER ?NUMBER)
(forall (?ELEMENT)
(=>
(inList ?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?GREATER) 0))))))) 
Merge.kif 48604874 

(=>
(and
(equal ?DEP
(DepartmentOfFn ?COMP ?PHYS))
(subOrganization ?DEP2 ?COMP)
(not
(equal ?DEP ?DEP2))
(instance ?I ?PHYS)
(inScopeOfInterest ?P ?I)
(equal ?P1
(ProbabilityFn
(agent ?P ?DEP)))
(equal ?P2
(ProbabilityFn
(agent ?P ?DEP2))))
(greaterThan ?P1 ?P2)) 
Midlevelontology.kif 1818218196 

(=>
(and
(governorSpeed ?V ?Q)
(equal
(MeasureFn ?FAST MilesPerHour)
(SpeedFn ?L1 ?T1))
(equal
(MeasureFn ?SLOW MilesPerHour)
(SpeedFn ?L2 ?T2))
(greaterThan ?FAST ?SLOW)
(equal ?FASTPROB
(ProbabilityFn
(measure ?V
(MeasureFn ?FAST MilesPerHour))))
(equal ?SLOWPROB
(ProbabilityFn
(measure ?V
(MeasureFn ?SLOW MilesPerHour)))))
(greaterThan ?SLOWPROB ?FASTPROB)) 
Cars.kif 28842902 


Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 