(<=>
(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 298319 
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 
(=>
(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 58995912 

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

(=>
(and
(equal
(RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)
(not
(equal ?NUMBER2 0)))
(equal
(AdditionFn
(MultiplicationFn
(FloorFn
(DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) 
Merge.kif 50165027 

(=>
(and
(equal ?A
(ListSumFn ?L))
(greaterThan
(ListLengthFn ?L) 1))
(equal ?A
(AdditionFn
(FirstFn ?L)
(ListSumFn
(SubListFn 2
(ListLengthFn ?L) ?L))))) 
Merge.kif 31953205 

(=>
(and
(equal ?LIST3
(ListConcatenateFn ?LIST1 ?LIST2))
(not
(equal ?LIST1 NullList))
(not
(equal ?LIST2 NullList))
(lessThanOrEqualTo ?NUMBER1
(ListLengthFn ?LIST1))
(lessThanOrEqualTo ?NUMBER2
(ListLengthFn ?LIST2))
(instance ?NUMBER1 PositiveInteger)
(instance ?NUMBER2 PositiveInteger))
(and
(equal
(ListOrderFn ?LIST3 ?NUMBER1)
(ListOrderFn ?LIST1 ?NUMBER1))
(equal
(ListOrderFn ?LIST3
(AdditionFn
(ListLengthFn ?LIST1) ?NUMBER2))
(ListOrderFn ?LIST2 ?NUMBER2)))) 
Merge.kif 30193038 

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

(=>
(and
(equal ?R
(SubListFn ?S ?E ?L))
(greaterThan
(SubtractionFn ?E ?S) 1))
(equal ?R
(ListConcatenateFn
(ListFn
(ListOrderFn ?L ?S))
(SubListFn
(AdditionFn 1 ?S) ?E ?L)))) 
Merge.kif 31263138 

(=>
(and
(equal ?VA
(VarianceAverageFn ?M ?L))
(greaterThan
(ListLengthFn ?L) 1))
(equal ?VA
(AdditionFn
(VarianceAverageFn ?M
(ListOrderFn ?L 1))
(VarianceAverageFn ?M
(SubListFn 2
(ListLengthFn ?L) ?L))))) 
Weather.kif 14521464 

(=>
(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
(instance ?UTC
(HourFn ?H1
(DayFn ?D
(MonthFn ?M
(YearFn ?Y)))))
(instance ?CST
(HourFn ?H2
(DayFn ?D
(MonthFn ?M
(YearFn ?Y)))))
(equal
(RelativeTimeFn ?UTC CentralTimeZone) ?CST))
(equal ?H2
(AdditionFn ?H1 6))) 
Merge.kif 1695316959 

(=>
(and
(instance ?UTC
(HourFn ?H1
(DayFn ?D
(MonthFn ?M
(YearFn ?Y)))))
(instance ?EST
(HourFn ?H2
(DayFn ?D
(MonthFn ?M
(YearFn ?Y)))))
(equal
(RelativeTimeFn ?UTC EasternTimeZone) ?EST))
(equal ?H2
(AdditionFn ?H1 5))) 
Merge.kif 1696516971 

(=>
(and
(instance ?UTC
(HourFn ?H1
(DayFn ?D
(MonthFn ?M
(YearFn ?Y)))))
(instance ?MST
(HourFn ?H2
(DayFn ?D
(MonthFn ?M
(YearFn ?Y)))))
(equal
(RelativeTimeFn ?UTC MountainTimeZone) ?MST))
(equal ?H2
(AdditionFn ?H1 7))) 
Merge.kif 1694116947 

(=>
(and
(instance ?UTC
(HourFn ?H1
(DayFn ?D
(MonthFn ?M
(YearFn ?Y)))))
(instance ?PST
(HourFn ?H2
(DayFn ?D
(MonthFn ?M
(YearFn ?Y)))))
(equal
(RelativeTimeFn ?UTC PacificTimeZone) ?PST))
(equal ?H2
(AdditionFn ?H1 8))) 
Merge.kif 1692916935 

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

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

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