(<=>
(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
(RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)
(equal
(AdditionFn
(MultiplicationFn
(FloorFn
(DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) 
Merge.kif 52615263 
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 
(=>
(and
(courseWRTMagneticNorth ?OBJ1 ?OBJ2 ?MAGDEGREE)
(partlyLocated ?OBJ1 ?AREA)
(partlyLocated ?OBJ2 ?AREA)
(magneticVariation ?AREA ?DEGREE ?DIRECTION))
(exists (?DIFFDEGREE ?TRUEDEGREE)
(and
(=>
(and
(equal ?DIRECTION East)
(equal ?DIFFDEGREE
(AdditionFn ?MAGDEGREE ?DEGREE)))
(courseWRTTrueNorth ?OBJ1 ?OBJ2 ?TRUEDEGREE))
(=>
(and
(equal ?DIRECTION West)
(equal ?DIFFDEGREE
(SubtractionFn ?MAGDEGREE ?DEGREE)))
(courseWRTTrueNorth ?OBJ1 ?OBJ2 ?TRUEDEGREE))))) 
Geography.kif 36193636 

(=>
(and
(equal
(PathWeightFn ?PATH) ?SUM)
(graphPart ?ARC1 ?PATH)
(graphPart ?ARC2 ?PATH)
(arcWeight ?ARC1 ?NUMBER1)
(arcWeight ?ARC2 ?NUMBER2)
(forall (?ARC3)
(=>
(graphPart ?ARC3 ?PATH)
(or
(equal ?ARC3 ?ARC1)
(equal ?ARC3 ?ARC2)))))
(equal
(PathWeightFn ?PATH)
(AdditionFn ?NUMBER1 ?NUMBER2))) 
Merge.kif 61136126 

(=>
(and
(equal
(PathWeightFn ?PATH) ?SUM)
(subGraph ?SUBPATH ?PATH)
(graphPart ?ARC1 ?PATH)
(arcWeight ?ARC1 ?NUMBER1)
(forall (?ARC2)
(=>
(graphPart ?ARC2 ?PATH)
(or
(graphPart ?ARC2 ?SUBPATH)
(equal ?ARC2 ?ARC1)))))
(equal ?SUM
(AdditionFn
(PathWeightFn ?SUBPATH) ?NUMBER1))) 
Merge.kif 60996111 

(=>
(and
(instance ?UNIT UnitOfArea)
(landAreaOnly ?AREA
(MeasureFn ?LAND ?UNIT))
(waterAreaOnly ?AREA
(MeasureFn ?WATER ?UNIT)))
(totalArea ?AREA
(MeasureFn
(AdditionFn ?LAND ?WATER) ?UNIT))) 
Geography.kif 559564 

(=>
(and
(totalLengthOfHighwaySystem ?AREA
(MeasureFn ?LENGTH ?UNIT))
(lengthOfPavedHighway ?AREA
(MeasureFn ?LENGTH1 ?UNIT))
(lengthOfUnpavedHighway ?AREA
(MeasureFn ?LENGTH2 ?UNIT))
(instance ?UNIT UnitOfLength))
(totalLengthOfHighwaySystem ?AREA
(MeasureFn
(AdditionFn ?LENGTH1 ?LENGTH2) ?UNIT))) 
Transportation.kif 504511 

(=>
(and
(totalLengthOfHighwaySystem ?AREA ?LENGTH)
(lengthOfPavedHighway ?AREA ?LENGTH1)
(lengthOfUnpavedHighway ?AREA ?LENGTH2))
(equal ?LENGTH
(AdditionFn ?LENGTH1 ?LENGTH2))) 
Transportation.kif 497502 

(=>
(conjugate ?COMPOUND1 ?COMPOUND2)
(exists (?NUMBER1 ?NUMBER2)
(and
(protonNumber ?COMPOUND1 ?NUMBER1)
(protonNumber ?COMPOUND2 ?NUMBER2)
(or
(equal ?NUMBER1
(AdditionFn ?NUMBER2 1))
(equal ?NUMBER2
(AdditionFn ?NUMBER1 1)))))) 
Midlevelontology.kif 61896197 

(=>
(equal
(RelativeTimeFn ?TIME1 CentralTimeZone) ?TIME2)
(equal ?TIME2
(AdditionFn ?TIME1
(MeasureFn 6 HourDuration)))) 
Merge.kif 1755417556 

(=>
(equal
(RelativeTimeFn ?TIME1 EasternTimeZone) ?TIME2)
(equal ?TIME2
(AdditionFn ?TIME1
(MeasureFn 5 HourDuration)))) 
Merge.kif 1756317565 

(=>
(equal
(RelativeTimeFn ?TIME1 MountainTimeZone) ?TIME2)
(equal ?TIME2
(AdditionFn ?TIME1
(MeasureFn 7 HourDuration)))) 
Merge.kif 1754517547 

(=>
(equal
(RelativeTimeFn ?TIME1 PacificTimeZone) ?TIME2)
(equal ?TIME2
(AdditionFn ?TIME1
(MeasureFn 8 HourDuration)))) 
Merge.kif 1753617538 
