( ! [V__OBJ1,V__OBJ2] :
(s__larger(V__OBJ1,V__OBJ2)
<=>
(! [V__QUANT1,V__QUANT2,V__UNIT] :
((s__measure(V__OBJ1,s__MeasureFn(V__QUANT1,V__UNIT))
&
s__measure(V__OBJ2,s__MeasureFn(V__QUANT2,V__UNIT))
&
s__instance(V__UNIT,s__UnitOfLength))
=>
s__greaterThan(V__QUANT1,V__QUANT2))))
)

Merge.kif 79467954 
An object is larger than another object if and only if for all a real number, another real number and an unit of measure 
( ! [V__O,V__A] :
(s__measure(V__O,s__MeasureFn(V__A,s__MetricTon))
<=>
s__measure(V__O,s__MeasureFn(s__MultiplicationFn(V__A,2205)
,s__PoundMass)))
)

Midlevelontology.kif 1119911205 
The measure of an object is a real number metric ton(s) if and only if the measure of the object is the real number and 2205 pound mass(s) 
( ! [V__OBJ,V__DEG] :
(s__measure(V__OBJ,s__MeasureFn(V__DEG,s__AngularDegree))
<=>
s__measure(V__OBJ,s__MeasureFn(s__MultiplicationFn(60,V__DEG)
,s__ArcMinute)))
)

Geography.kif 378380 
The measure of an object is a real number angular degree(s) if and only if the measure of the object is 60 and the real number arc minute(s) 
( ! [V__OBJ,V__DEG] :
(s__measure(V__OBJ,s__MeasureFn(V__DEG,s__ArcMinute))
<=>
s__measure(V__OBJ,s__MeasureFn(s__MultiplicationFn(60,V__DEG)
,s__ArcSecond)))
)

Geography.kif 397399 
The measure of an object is a real number arc minute(s) if and only if the measure of the object is 60 and the real number arc second(s) 
( ! [V__OBJECT,V__NUMBER] :
(s__measure(V__OBJECT,s__MeasureFn(V__NUMBER,s__OunceMass))
<=>
s__measure(V__OBJECT,s__MeasureFn(s__DivisionFn(V__NUMBER,16)
,s__PoundMass)))
)

Midlevelontology.kif 1093910944 
The measure of an object is a real number Ounce(s) if and only if the measure of the object is the real number and 16 pound mass(s) 
( ! [V__REGION,V__FRACTION,V__TOTAL,V__UNIT] :
((s__arableLandArea(V__REGION,V__FRACTION)
&
s__greaterThanOrEqualTo(V__FRACTION,0)
&
s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))
&
s__instance(V__UNIT,s__UnitOfArea))
=>
(? [V__ARABLE] :
(s__instance(V__ARABLE,s__ArableLand) &
s__geographicSubregion(V__ARABLE,V__REGION)
&
s__measure(V__ARABLE,s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT)))))
)

Geography.kif 20372047 

( ! [V__ROOM,V__HOTELUNIT] :
((s__attribute(V__ROOM,s__Oversized) &
s__immediateInstance(V__ROOM,V__HOTELUNIT)
&
s__subclass(V__HOTELUNIT,s__HotelUnit))
=>
(? [V__NORMAL,V__AREA1,V__AREA2] :
(s__immediateInstance(V__NORMAL,V__HOTELUNIT)
&
s__measure(V__NORMAL,V__AREA1)
&
s__measure(V__ROOM,V__AREA2)
&
s__instance(V__AREA1,s__AreaMeasure) &
s__instance(V__AREA2,s__AreaMeasure) &
s__greaterThan(V__AREA2,V__AREA1))))
)

Hotel.kif 11361148 

( ! [V__X,V__Y] :
((s__attribute(V__X,V__Y)
&
s__instance(V__Y,s__TemperatureAttribute) &
s__instance(V__X,s__Object))
=>
(? [V__TEMP] :
(s__measure(V__X,V__TEMP)
&
s__instance(V__TEMP,s__TemperatureMeasure) &
s__attribute(V__TEMP,V__Y))))
)

Midlevelontology.kif 2352623535 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1113111140 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1114111152 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1116011169 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1117111180 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1110211111 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1111211123 

( ! [V__G,V__M,V__AN,V__AA,V__PN,V__PA,V__N] :
((s__graphMeasure(V__G,V__M)
&
s__instance(V__AN,s__GraphNode) &
s__instance(V__AA,s__GraphArc) &
s__abstractCounterpart(V__AN,V__PN)
&
s__abstractCounterpart(V__AA,V__PA)
&
s__arcWeight(V__AA,s__MeasureFn(V__N,V__M)))
=>
s__measure(V__PA,s__MeasureFn(V__N,V__M)))
)

Merge.kif 62906298 

( ! [V__BIG,V__CLASS,V__NORMAL] :
((s__immediateInstance(V__BIG,V__CLASS)
&
s__immediateInstance(V__NORMAL,V__CLASS)
&
s__attribute(V__BIG,s__Oversized))
=>
(? [V__BIGSIZE,V__NORMALSIZE] :
(s__measure(V__BIG,V__BIGSIZE)
&
s__measure(V__NORMAL,V__NORMALSIZE)
&
s__greaterThan(V__BIGSIZE,V__NORMALSIZE))))
)

Hotel.kif 11251134 

( ! [V__X,V__CLASS,V__Y] :
((s__immediateInstance(V__X,V__CLASS)
&
s__immediateInstance(V__Y,V__CLASS)
&
s__attribute(V__X,s__ColdTemperature) &
s__attribute(V__Y,s__HotTemperature))
=>
(? [V__TEMPX,V__TEMPY] :
(s__measure(V__X,V__TEMPX)
&
s__instance(V__TEMPX,s__TemperatureMeasure) &
s__measure(V__Y,V__TEMPY)
&
s__instance(V__TEMPY,s__TemperatureMeasure) &
s__greaterThan(V__TEMPY,V__TEMPX))))
)

Midlevelontology.kif 2356123573 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1472714737 

( ! [V__ATOM] :
((s__instance(V__ATOM,s__Actinium) &
s__instance(V__ATOM,s__Atom))
=>
s__measure(V__ATOM,s__MeasureFn(227,s__Amu)))
)

Midlevelontology.kif 2690626910 

( ! [V__ATOM] :
((s__instance(V__ATOM,s__Aluminum) &
s__instance(V__ATOM,s__Atom))
=>
s__measure(V__ATOM,s__MeasureFn(26.9815,s__Amu)))
)

Midlevelontology.kif 2564825652 

( ! [V__ATOM] :
((s__instance(V__ATOM,s__Americium) &
s__instance(V__ATOM,s__Atom))
=>
s__measure(V__ATOM,s__MeasureFn(243,s__Amu)))
)

Midlevelontology.kif 2700627010 

( ! [V__ATOM] :
((s__instance(V__ATOM,s__Antimony) &
s__instance(V__ATOM,s__Atom))
=>
s__measure(V__ATOM,s__MeasureFn(121.75,s__Amu)))
)

Midlevelontology.kif 2624426248 

( ! [V__ATOM] :
((s__instance(V__ATOM,s__Argon) &
s__instance(V__ATOM,s__Atom))
=>
s__measure(V__ATOM,s__MeasureFn(39.948,s__Amu)))
)

Midlevelontology.kif 2572625730 

( ! [V__ATOM] :
((s__instance(V__ATOM,s__Arsenic) &
s__instance(V__ATOM,s__Atom))
=>
s__measure(V__ATOM,s__MeasureFn(74.922,s__Amu)))
)

Midlevelontology.kif 2595925963 

( ! [V__ATOM] :
((s__instance(V__ATOM,s__Astatine) &
s__instance(V__ATOM,s__Atom))
=>
s__measure(V__ATOM,s__MeasureFn(210,s__Amu)))
)

Midlevelontology.kif 2684326847 


Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 