(<=>
(and
(equal ?LIST3
(ListConcatenateFn ?LIST1 ?LIST2))
(not
(equal ?LIST1 NullList))
(not
(equal ?LIST2 NullList)))
(forall (?NUMBER1 ?NUMBER2)
(=>
(and
(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 29722988 
A list is equal to the list composed of another list and a third list and the other list is not equal to null list and the third list is not equal to null list if and only if for all a positive integer and another positive integer 
(<=>
(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 48604862 
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 56485661 

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

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

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

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

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

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

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

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