(<=>
(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 272293 
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 
(=>
(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 59936006 

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

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

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

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

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

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

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

(=>
(and
(instance ?M Mixture)
(instance ?Z UnitOfMeasure)
(mixtureRatio ?A ?B ?X ?Y ?Z)
(measure ?M
(MeasureFn ?T ?Z))
(part ?A ?M)
(part ?B ?M)
(measure ?A
(MeasureFn ?X ?Z))
(measure ?B
(MeasureFn ?Y ?Z)))
(equal ?T
(AdditionFn ?X ?Y))) 
Food.kif 12481262 

(=>
(and
(instance ?MIT BarMitzvah)
(patient ?MIT ?X)
(instance ?X Boy)
(member ?X ?GROUP)
(instance ?GROUP Judaism)
(birthdate ?X ?DAY)
(instance ?DAY
(DayFn ?D
(MonthFn ?M
(YearFn ?Y)))))
(exists (?Y13 ?BD13)
(and
(instance ?Y13 Integer)
(equal ?Y13
(AdditionFn ?Y 13))
(instance ?BD13
(DayFn ?D
(MonthFn ?M
(YearFn ?Y13))))
(equal
(WhenFn ?MIT)
(ImmediateFutureFn ?BD13))))) 
Biography.kif 6985 

(=>
(and
(instance ?MIT BatMitzvah)
(patient ?MIT ?X)
(instance ?X Girl)
(member ?X ?GROUP)
(instance ?GROUP Judaism)
(birthdate ?X ?DAY)
(instance ?DAY
(DayFn ?D
(MonthFn ?M
(YearFn ?Y)))))
(exists (?Y13 ?BD13)
(and
(instance ?Y13 Integer)
(equal ?Y13
(AdditionFn ?Y 13))
(instance ?BD13
(DayFn ?D
(MonthFn ?M
(YearFn ?Y13))))
(equal
(WhenFn ?MIT)
(ImmediateFutureFn ?BD13))))) 
Biography.kif 99115 

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

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

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

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

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

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