(<=>
(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 47624764 
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 36323649 

(=>
(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 55525565 

(=>
(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 55385550 

(=>
(and
(equal ?OUT
(ReverseFn ?IN))
(equal ?LEN
(StringLengthFn ?IN))
(greaterThan ?LEN 1)
(greaterThan ?N 0)
(lessThan ?N ?LEN)
(equal ?PIVOT
(CeilingFn
(DivisionFn
(SubtractionFn ?LEN 1) 2)))
(equal ?NEW
(AdditionFn
(SubtractionFn ?PIVOT ?N) ?PIVOT))
(equal ?S
(SubstringFn ?IN ?N
(AdditionFn 1 ?N))))
(equal ?S
(SubstringFn ?OUT ?NEW
(AdditionFn 1 ?NEW)))) 
Media.kif 30363057 

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

(=>
(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 1588715889 

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

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

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