(<=>
(and
(instance ?REL TotalValuedRelation)
(instance ?REL Predicate))
(exists (?VALENCE)
(and
(instance ?REL Relation)
(valence ?REL ?VALENCE)
(=>
(forall (?NUMBER ?ELEMENT ?CLASS)
(=>
(and
(lessThan ?NUMBER ?VALENCE)
(domain ?REL ?NUMBER ?CLASS)
(equal ?ELEMENT
(ListOrderFn
(ListFn @ROW) ?NUMBER)))
(instance ?ELEMENT ?CLASS)))
(exists (?ITEM)
(?REL @ROW ?ITEM)))))) 
Merge.kif 23082325 
A relation is an instance of total valued relation and the relation is an instance of predicate if and only if there exists a positive integer such that the relation is an instance of relation and the relation %&has the positive integer argument(s) and 
(<=>
(attribute ?WATER OpenSea)
(forall (?LAND)
(and
(instance ?AREA SaltWaterArea)
(not
(instance ?WATER LandlockedWater))
(distance ?LAND ?WATER ?DIST)
(greaterThan ?DIST
(MeasureFn 5 NauticalMile))))) 
Geography.kif 44094416 
Open sea is an attribute of an object if and only if for all a physical an entity is an instance of salt water area and the object is not an instance of landlocked water and the distance between the physical and the object is a length measure and the length measure is greater than 5 nautical mile(s) 
(<=>
(average ?LIST1 ?AVERAGE)
(exists (?LIST2)
(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 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 
(<=>
(equal
(FemaleLifeExpectancyAtBirthFn ?AREA
(YearFn ?YEAR)) ?REALNUMBER)
(exists (?LIST)
(and
(instance ?LIST List)
(instance
(ListLengthFn ?LIST) ?COUNT)
(forall (?LISTITEM)
(=>
(inList ?LISTITEM ?LIST)
(and
(instance ?LISTITEM ?LIFEEXPECTANCYAGE)
(not
(exists (?NUMBER)
(and
(instance ?NUMBER ?LIFEEXPECTANCYAGE)
(not
(inList ?NUMBER ?LIST)))))
(equal ?COUNT
(CardinalityFn
(KappaFn ?LIFEEXPECTANCYAGE
(and
(instance ?BIRTH Birth)
(experiencer ?BIRTH ?INDIVIDUAL)
(instance ?INDIVIDUAL Human)
(attribute ?INDIVIDUAL Female)
(during
(WhenFn ?BIRTH)
(YearFn ?YEAR))
(equal
(WhereFn ?BIRTH
(WhenFn ?BIRTH)) ?AREA)
(instance ?DEATH Death)
(experiencer ?DEATH ?INDIVIDUAL)
(holdsDuring
(WhenFn ?DEATH)
(age ?INDIVIDUAL
(MeasureFn ?LIFEEXPECTANCYAGE YearDuration))))))))))
(average ?LIST ?REALNUMBER)))) 
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 a number and for all the listITEM and the real number is an average of the list 
(<=>
(equal
(LifeExpectancyAtBirthFn ?AREA
(YearFn ?YEAR)) ?REALNUMBER)
(exists (?LIST)
(and
(instance ?LIST List)
(instance
(ListLengthFn ?LIST) ?COUNT)
(forall (?LISTITEM)
(=>
(inList ?LISTITEM ?LIST)
(and
(instance ?LISTITEM ?LIFEEXPECTANCYAGE)
(not
(exists (?NUMBER)
(and
(instance ?NUMBER ?LIFEEXPECTANCYAGE)
(not
(inList ?NUMBER ?LIST)))))
(equal ?COUNT
(CardinalityFn
(KappaFn ?LIFEEXPECTANCYAGE
(and
(instance ?BIRTH Birth)
(experiencer ?BIRTH ?INDIVIDUAL)
(instance ?INDIVIDUAL Human)
(during
(WhenFn ?BIRTH)
(YearFn ?YEAR))
(equal
(WhereFn ?BIRTH
(WhenFn ?BIRTH)) ?AREA)
(instance ?DEATH Death)
(experiencer ?DEATH ?INDIVIDUAL)
(holdsDuring
(WhenFn ?DEATH)
(age ?INDIVIDUAL
(MeasureFn ?LIFEEXPECTANCYAGE YearDuration))))))))))
(average ?LIST ?REALNUMBER)))) 
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 a number and for all the listITEM and the real number is an average of the list 
(<=>
(equal
(MaleLifeExpectancyAtBirthFn ?AREA
(YearFn ?YEAR)) ?REALNUMBER)
(exists (?LIST)
(and
(instance ?LIST List)
(instance
(ListLengthFn ?LIST) ?COUNT)
(forall (?LISTITEM)
(=>
(inList ?LISTITEM ?LIST)
(and
(instance ?LISTITEM ?LIFEEXPECTANCYAGE)
(not
(exists (?NUMBER)
(and
(instance ?NUMBER ?LIFEEXPECTANCYAGE)
(not
(inList ?NUMBER ?LIST)))))
(equal ?COUNT
(CardinalityFn
(KappaFn ?LIFEEXPECTANCYAGE
(and
(instance ?BIRTH Birth)
(experiencer ?BIRTH ?INDIVIDUAL)
(instance ?INDIVIDUAL Human)
(attribute ?INDIVIDUAL Male)
(during
(WhenFn ?BIRTH)
(YearFn ?YEAR))
(equal
(WhereFn ?BIRTH
(WhenFn ?BIRTH)) ?AREA)
(instance ?DEATH Death)
(experiencer ?DEATH ?INDIVIDUAL)
(holdsDuring
(WhenFn ?DEATH)
(age ?INDIVIDUAL
(MeasureFn ?LIFEEXPECTANCYAGE YearDuration))))))))))
(average ?LIST ?REALNUMBER)))) 
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 a number and for all the listITEM and the real number is an average of the list 
(<=>
(instance ?OBJ SelfConnectedObject)
(forall (?PART1 ?PART2)
(=>
(equal ?OBJ
(MereologicalSumFn ?PART1 ?PART2))
(connected ?PART1 ?PART2)))) 
Merge.kif 94139418 
An object is an instance of self connected object if and only if for all another object and a third object 
(<=>
(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 79147922 
An object is larger than another object if and only if for all a real number, another real number and an unit of measure 
(<=>
(subCollection ?COLL1 ?COLL2)
(forall (?MEMBER)
(=>
(member ?MEMBER ?COLL1)
(member ?MEMBER ?COLL2)))) 
Merge.kif 13171322 
A collection is a proper subcollection of another collection if and only if for all an object 
(=>
(allRoomsPhysicalAmenity ?INV ?OBJ)
(forall (?X)
(=>
(memberType ?INV ?X)
(roomAmenity ?X ?OBJ)))) 
Hotel.kif 166171 

(=>
(allRoomsPolicy ?INV ?POLICY)
(forall (?X)
(=>
(memberType ?INV ?X)
(roomPolicy ?X ?POLICY)))) 
Hotel.kif 228233 

(=>
(allRoomsServiceAmenity ?INV ?OBJ)
(forall (?X)
(=>
(memberType ?INV ?X)
(roomAmenity ?X ?OBJ)))) 
Hotel.kif 213218 

(=>
(and
(attribute ?OBJ ?SPHERE)
(instance ?SPHERE Sphere))
(exists (?CENTER ?DIST)
(forall (?PT)
(=>
(pointOfFigure ?PT ?OBJ)
(geometricDistance ?PT ?CENTER ?DIST))))) 
Midlevelontology.kif 52885296 

(=>
(and
(attribute ?OBJ Monochromatic)
(superficialPart ?PART ?OBJ)
(attribute ?PART ?COLOR)
(instance ?COLOR PrimaryColor))
(forall (?ELEMENT)
(=>
(superficialPart ?ELEMENT ?OBJ)
(attribute ?ELEMENT ?COLOR)))) 
Merge.kif 1799118000 

(=>
(and
(attribute ?X DutyFree)
(instance ?X Store))
(forall (?OBJ)
(=>
(and
(instance ?SELL Selling)
(patient ?SELL ?OBJ)
(located ?SELL ?X)
(instance ?OBJ Product))
(attribute ?OBJ DutyFree)))) 
Hotel.kif 14231434 

(=>
(and
(citizen ?AGENT ?POLITY)
(subProposition UniversalSuffrageLaw
(RegionalLawFn ?POLITY)))
(confersRight
(forall (?VOTINGAGE ?AGE ?ELECTION)
(=>
(and
(citizen ?AGENT ?POLITY)
(suffrageAgeMinimum ?POLITY ?VOTINGAGE)
(age ?AGENT ?AGE)
(greaterThanOrEqualTo ?AGE ?VOTINGAGE)
(instance ?ELECTION
(ElectionFn ?POLITY)))
(exists (?VOTING)
(and
(instance ?VOTING
(VotingFn ?ELECTION))
(agent ?VOTING ?AGENT)))))
(RegionalLawFn ?POLITY) ?AGENT)) 
Government.kif 11031121 

(=>
(and
(element ?X
(PropertyFn ?HOTEL))
(instance ?X RoomInventory))
(forall (?Y)
(=>
(member ?Y ?X)
(element ?Y
(PropertyFn ?HOTEL))))) 
Hotel.kif 142149 

(=>
(and
(equal
(MaximalWeightedPathFn ?NODE1 ?NODE2) ?PATH)
(equal
(PathWeightFn ?PATH) ?NUMBER1))
(forall (?PATH2)
(=>
(and
(instance ?PATH2
(GraphPathFn ?NODE1 ?NODE2))
(equal
(PathWeightFn ?PATH2) ?NUMBER2))
(lessThanOrEqualTo ?NUMBER2 ?NUMBER1)))) 
Merge.kif 61356144 

(=>
(and
(equal
(MinimalWeightedPathFn ?NODE1 ?NODE2) ?PATH)
(equal
(PathWeightFn ?PATH) ?NUMBER1))
(forall (?PATH2)
(=>
(and
(instance ?PATH2
(GraphPathFn ?NODE1 ?NODE2))
(equal
(PathWeightFn ?PATH2) ?NUMBER2))
(greaterThanOrEqualTo ?NUMBER2 ?NUMBER1)))) 
Merge.kif 61096118 

(=>
(and
(equal ?D
(AlbumCopiesFn ?A ?DS))
(instance ?X ?D))
(forall (?S)
(=>
(inList ?S ?A)
(exists (?C)
(and
(copy ?C ?S)
(stored ?C ?D)))))) 
Music.kif 952962 

(=>
(and
(hole ?HOLE1 ?OBJ)
(hole ?HOLE2 ?OBJ))
(forall (?HOLE3)
(=>
(part ?HOLE3
(MereologicalSumFn ?HOLE1 ?HOLE2))
(hole ?HOLE3 ?OBJ)))) 
Merge.kif 97829789 

(=>
(and
(instance ?AGENT Agent)
(instance ?SITE WebSite))
(exists (?COLL)
(and
(instance ?COLL Collection)
(forall (?LISTING)
(=>
(and
(instance ?LISTING WebListing)
(hostedOn ?LISTING ?SITE)
(listingSeller ?LISTING ?AGENT))
(member ?LISTING ?COLL)))
(equal
(SellersItemsFn ?AGENT ?SITE) ?COLL)))) 
UXExperimentalTerms.kif 11891205 

(=>
(and
(instance ?ATTR RecordingAttribute)
(albumType ?A ?ATTR))
(forall (?R)
(=>
(inList ?R ?M)
(attribute ?R ?A)))) 
Music.kif 307314 

(=>
(and
(instance ?INTERVAL TimeInterval)
(instance ?SITE WebSite))
(exists (?NEWBUYERS)
(and
(instance ?NEWBUYERS Collection)
(instance ?BEFORE TimeInterval)
(forall (?AGENT)
(=>
(member ?AGENT ?NEWBUYERS)
(and
(exists (?BUYING)
(and
(instance ?AGENT Agent)
(instance ?BUYING Buying)
(agent ?BUYING ?AGENT)
(instrument ?BUYING ?SITE)
(during ?BUYING ?INTERVAL)))
(not
(exists (?INTERVAL_BEFORE)
(and
(instance ?INTERVAL_BEFORE TimeInterval)
(earlier ?INTERVAL_BEFORE ?INTERVAL)
(holdsDuring ?INTERVAL_BEFORE
(exists (?BUYING_BEFORE)
(and
(instance ?BUYING_BEFORE Buying)
(agent ?BUYING_BEFORE ?AGENT)
(instrument ?BUYING_BEFORE ?SITE)
(during ?BUYING_BEFORE ?INTERVAL))))))))))
(equal
(SiteWideNewBuyersFn ?INTERVAL ?SITE) ?NEWBUYERS)))) 
UXExperimentalTerms.kif 35713604 

(=>
(and
(instance ?INTERVAL TimeInterval)
(instance ?SITE WebSite))
(exists (?NEWREGISTRATIONS)
(and
(instance ?NEWREGISTRATIONS Collection)
(forall (?USER)
(=>
(and
(instance ?USER Human)
(not
(exists (?INTERVAL_BEFORE)
(and
(instance ?INTERVAL_BEFORE TimeInterval)
(earlier ?INTERVAL_BEFORE ?INTERVAL)
(holdsDuring ?INTERVAL_BEFORE
(registeredUser ?USER ?SITE)))))
(exists (?INTERVAL_DURING)
(and
(instance ?INSTERVAL_DURING TimeInterval)
(during ?INTERVAL_DURING ?INTERVAL)
(holdsDuring ?INTERVAL
(registeredUser ?USER ?SITE)))))
(member ?USER ?NEWREGISTRATIONS)))
(equal ?NEWREGISTRATIONS
(SiteWideNewRegistrationsFn ?INTERVAL ?SITE))))) 
UXExperimentalTerms.kif 36243651 


Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 