Browsing Interface : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - lessThan
lessThan

appearance as argument number 1
-------------------------


s__documentation(s__lessThan__m,s__ChineseLanguage,'(lessThan ?NUMBER1 ?NUMBER2) 是真的 以防 ?NUMBER1 的 Quantity 比 ?NUMBER2 的 Quantity 要少。')

Merge.kif 1904-1905
s__documentation(s__lessThan__m,s__EnglishLanguage,'(lessThan ?NUMBER1 ?NUMBER2) is true just in case the Quantity ?NUMBER1 is less than the Quantity ?NUMBER2.')

Merge.kif 1902-1903
s__domain(s__lessThan__m,1,s__Quantity)

Merge.kif 1900-1900 The number 1 argument of less than is an instance of quantity
s__domain(s__lessThan__m,2,s__Quantity)

Merge.kif 1901-1901 The number 2 argument of less than is an instance of quantity
s__instance(s__BinaryPredicate,s__SetOrClass)

s__instance(s__lessThan__m,s__BinaryPredicate)

Merge.kif 1895-1895 less than is an instance of binary predicate
s__instance(s__IrreflexiveRelation,s__SetOrClass)

s__instance(s__lessThan__m,s__IrreflexiveRelation)

Merge.kif 1897-1897 less than is an instance of irreflexive relation
s__instance(s__lessThan__m,s__RelationExtendedToQuantities)

s__instance(s__RelationExtendedToQuantities,s__SetOrClass)

Merge.kif 1898-1898 less than is an instance of relation extended to quantities
s__instance(s__lessThan__m,s__TransitiveRelation)

s__instance(s__TransitiveRelation,s__SetOrClass)

Merge.kif 1896-1896 less than is an instance of transitive relation
s__trichotomizingOn(s__lessThan__m,s__RealNumber)

Merge.kif 1899-1899 less than is trichotomizing on real number

appearance as argument number 2
-------------------------


s__format(s__ChineseLanguage,s__lessThan__m,'%1 %n 是 lessThan %2')

chinese_format.kif 141-141
s__format(s__EnglishLanguage,s__lessThan__m,'%1 is %n less than %2')

english_format.kif 97-97
s__inverse(s__greaterThan__m,s__lessThan__m)

Merge.kif 1915-1915 greater than is an inverse of less than
s__termFormat(s__ChineseLanguage,s__lessThan__m,'少于')

chinese_format.kif 142-142 "少于" is the printable form of less than in ChineseLanguage
s__termFormat(s__EnglishLanguage,s__lessThan__m,'less than')

domainEnglishFormat.kif 6109-6109 "less than" is the printable form of less than in english language

antecedent
-------------------------


( ! [V__S,V__LD] :
   (s__instance(V__S,s__RealNumber)s__=>((s__instance(V__LD,s__LiquidDrop)s__and__ms__approximateDiameter(V__LD,s__MeasureFn(V__S,s__Micrometer))
      s__and__ms__lessThan(500,V__S))
  s__<=>
  s__instance(V__LD,s__Droplet)))
)

Geography.kif 6874-6880 A self connected object is an instance of liquid drop and the approximate diameter of the self connected object is a real number micrometer(s) and 500 is less than the real number if and only if the self connected object is an instance of droplet
( ! [V__Time,V__Option] :
   ((s__instance(V__Time,s__Agent)s__and__ms__instance(V__Time,s__TimePosition))
    s__=>((s__exists__m[V__Stock,V__StockPrice,V__StrikePrice] :
         (s__instance(V__Stock,s__FinancialInstrument)s__and__ms__instance(V__StockPrice,s__CurrencyMeasure)s__and__ms__instance(V__StrikePrice,s__CurrencyMeasure)s__and__m(s__instance(V__Option,s__CallOption)s__and__ms__underlier(V__Option,V__Stock)
        s__and__ms__price(V__Stock,V__StockPrice,V__Time)
      s__and__ms__strikePrice(V__Option,V__StrikePrice)
    s__and__ms__lessThan(V__StockPrice,V__StrikePrice))))
s__<=>
s__outOfTheMoney(V__Option,V__Time)))
)

FinancialOntology.kif 2965-2973 There exist a financial instrument, the financial instrumentPrice and another currency measure such that an agreement is an instance of call option and the financial instrument is an underlier of the agreement and the financial instrument price the financial instrumentPrice for an agent and the other currency measure is a strike price of the agreement and the financial instrumentPrice is less than the other currency measure if and only if the agent is an out of the money of the agreement
( ! [V__Time,V__Option] :
   ((s__instance(V__Time,s__Agent)s__and__ms__instance(V__Time,s__TimePosition))
    s__=>((s__exists__m[V__Stock,V__StockPrice,V__StrikePrice] :
         (s__instance(V__Stock,s__FinancialInstrument)s__and__ms__instance(V__StockPrice,s__CurrencyMeasure)s__and__ms__instance(V__StrikePrice,s__CurrencyMeasure)s__and__m(s__instance(V__Option,s__CallOption)s__and__ms__underlier(V__Option,V__Stock)
        s__and__ms__price(V__Stock,V__StockPrice,V__Time)
      s__and__ms__strikePrice(V__Option,V__StrikePrice)
    s__and__ms__lessThan(V__StrikePrice,V__StockPrice))))
s__<=>
s__inTheMoney(V__Option,V__Time)))
)

FinancialOntology.kif 2922-2930 There exist a financial instrument, the financial instrumentPrice and another currency measure such that an agreement is an instance of call option and the financial instrument is an underlier of the agreement and the financial instrument price the financial instrumentPrice for an agent and the other currency measure is a strike price of the agreement and the other currency measure is less than the financial instrumentPrice if and only if the agent is an in the money of the agreement
( ! [V__Time,V__Option] :
   ((s__instance(V__Time,s__Agent)s__and__ms__instance(V__Time,s__TimePosition))
    s__=>((s__exists__m[V__Stock,V__StockPrice,V__StrikePrice] :
         (s__instance(V__Stock,s__FinancialInstrument)s__and__ms__instance(V__StockPrice,s__CurrencyMeasure)s__and__ms__instance(V__StrikePrice,s__CurrencyMeasure)s__and__m(s__instance(V__Option,s__PutOption)s__and__ms__underlier(V__Option,V__Stock)
        s__and__ms__price(V__Stock,V__StockPrice,V__Time)
      s__and__ms__strikePrice(V__Option,V__StrikePrice)
    s__and__ms__lessThan(V__StockPrice,V__StrikePrice))))
s__<=>
s__inTheMoney(V__Option,V__Time)))
)

FinancialOntology.kif 2932-2940 There exist a financial instrument, the financial instrumentPrice and another currency measure such that an agreement is an instance of put option and the financial instrument is an underlier of the agreement and the financial instrument price the financial instrumentPrice for an agent and the other currency measure is a strike price of the agreement and the financial instrumentPrice is less than the other currency measure if and only if the agent is an in the money of the agreement
( ! [V__Time,V__Option] :
   ((s__instance(V__Time,s__Agent)s__and__ms__instance(V__Time,s__TimePosition))
    s__=>((s__exists__m[V__Stock,V__StockPrice,V__StrikePrice] :
         (s__instance(V__Stock,s__FinancialInstrument)s__and__ms__instance(V__StockPrice,s__CurrencyMeasure)s__and__ms__instance(V__StrikePrice,s__CurrencyMeasure)s__and__m(s__instance(V__Option,s__PutOption)s__and__ms__underlier(V__Option,V__Stock)
        s__and__ms__price(V__Stock,V__StockPrice,V__Time)
      s__and__ms__strikePrice(V__Option,V__StrikePrice)
    s__and__ms__lessThan(V__StrikePrice,V__StockPrice))))
s__<=>
s__outOfTheMoney(V__Option,V__Time)))
)

FinancialOntology.kif 2975-2983 There exist a financial instrument, the financial instrumentPrice and another currency measure such that an agreement is an instance of put option and the financial instrument is an underlier of the agreement and the financial instrument price the financial instrumentPrice for an agent and the other currency measure is a strike price of the agreement and the other currency measure is less than the financial instrumentPrice if and only if the agent is an out of the money of the agreement
( ! [V__Date,V__Balance,V__Account,V__Overdraft] :
   ((s__instance(V__Date,s__Day)s__and__ms__instance(V__Balance,s__RealNumber)s__and__ms__instance(V__Account,s__FinancialAccount)s__and__ms__instance(V__Overdraft,s__RealNumber))
    s__=>((s__currentAccountBalance(V__Account,V__Date,s__MeasureFn(V__Balance,s__UnitedStatesDollar))
      s__and__ms__lessThan(V__Balance,0)
    s__and__m(V__Overdrafts__equal__ms__SubtractionFn(0,V__Balance)))
s__=>s__overdraft(V__Account,s__MeasureFn(V__Overdraft,s__UnitedStatesDollar),V__Date)))
)

FinancialOntology.kif 733-738
( ! [V__Amount,V__Date,V__Balance,V__Account,V__FinancialAccount] :
   ((s__instance(V__Amount,s__CurrencyMeasure)s__and__ms__instance(V__Date,s__Day)s__and__ms__instance(V__Balance,s__CurrencyMeasure)s__and__ms__instance(V__Account,s__FinancialAccount)s__and__ms__instance(V__FinancialAccount,s__SetOrClass))
    s__=>((s__instance(V__Account,V__FinancialAccount)
      s__and__ms__minimumBalance(V__Account,s__UsingAnAccount,V__Balance)
    s__and__ms__currentAccountBalance(V__Account,V__Date,V__Amount)
  s__and__ms__lessThan(V__Amount,V__Balance))
s__=>(s__exists__m[V__Penalty] :
(s__instance(V__Penalty,s__Penalty)s__and__ms__date(V__Penalty,V__Date)
s__and__ms__destination(V__Penalty,s__CurrencyFn(V__Account))))))
)

FinancialOntology.kif 658-668
( ! [V__Amount,V__MinPayment,V__Account] :
   ((s__instance(V__Amount,s__CurrencyMeasure)s__and__ms__instance(V__MinPayment,s__CurrencyMeasure))
    s__=>((s__instance(V__Account,s__LiabilityAccount)s__and__ms__minimumPayment(V__Account,V__MinPayment,s__MonthDuration)s__and__m(s__exists__m[V__Payment,V__Month] :
         (s__instance(V__Payment,s__Process)s__and__m(s__instance(V__Month,s__Month)s__and__ms__destination(V__Payment,s__CurrencyFn(V__Account))
      s__and__ms__paymentsPerPeriod(V__Account,V__Amount,V__Month)
    s__and__ms__lessThan(V__Amount,V__MinPayment)))))
s__=>(s__exists__m[V__Penalty] :
(s__instance(V__Penalty,s__Penalty)s__and__ms__destination(V__Penalty,s__CurrencyFn(V__Account))))))
)

FinancialOntology.kif 712-725
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 492-498
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 419-424
No TPTP formula. May not be expressible in strict first order. Merge.kif 13854-13869
No TPTP formula. May not be expressible in strict first order. Merge.kif 13871-13884
( ! [V__DEPTH,V__OBJ,V__DRAFT,V__WATERWAY,V__UNIT] :
   ((s__instance(V__DEPTH,s__RealNumber)s__and__ms__instance(V__OBJ,s__Physical)s__and__ms__instance(V__DRAFT,s__RealNumber))
    s__=>((s__instance(V__WATERWAY,s__Waterway)s__and__ms__depth(V__OBJ,V__WATERWAY,s__MeasureFn(V__DEPTH,V__UNIT))
    s__and__ms__instance(V__UNIT,s__UnitOfLength)s__and__ms__lessThan(V__DRAFT,V__DEPTH))
s__=>s__navigableForDraft(V__WATERWAY,s__MeasureFn(V__DRAFT,V__UNIT))))
)

Transportation.kif 2608-2614
( ! [V__MELT,V__X,V__BOIL,V__Y,V__TEMP] :
   ((s__instance(V__MELT,s__RealNumber)s__and__ms__instance(V__X,s__Object)s__and__ms__instance(V__BOIL,s__RealNumber)s__and__ms__subclass(V__Y,s__PureSubstance)s__and__ms__instance(V__Y,s__SetOrClass)s__and__ms__instance(V__TEMP,s__RealNumber))
    s__=>((s__instance(V__X,V__Y)
      s__and__ms__subclass(V__Y,s__PureSubstance)s__and__ms__boilingPoint(V__Y,s__MeasureFn(V__BOIL,s__KelvinDegree))
    s__and__ms__meltingPoint(V__Y,s__MeasureFn(V__MELT,s__KelvinDegree))
  s__and__ms__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree))
s__and__ms__greaterThan(V__TEMP,V__MELT)
s__and__ms__lessThan(V__TEMP,V__BOIL))
s__=>s__attribute(V__X,s__Liquid)))
)

Merge.kif 13798-13807
( ! [V__PRES,V__MELT,V__X,V__Y,V__TEMP] :
   ((s__instance(V__PRES,s__RealNumber)s__and__ms__instance(V__MELT,s__RealNumber)s__and__ms__instance(V__X,s__Object)s__and__ms__subclass(V__Y,s__PureSubstance)s__and__ms__instance(V__Y,s__SetOrClass)s__and__ms__instance(V__TEMP,s__RealNumber))
    s__=>((s__instance(V__X,V__Y)
      s__and__ms__subclass(V__Y,s__PureSubstance)s__and__ms__meltingPoint(V__Y,s__MeasureFn(V__MELT,s__KelvinDegree))
    s__and__ms__barometricPressure(V__X,s__MeasureFn(V__PRES,s__InchMercury))
  s__and__ms__greaterThan(V__PRES,29.92)
s__and__ms__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree))
s__and__ms__lessThan(V__TEMP,V__MELT))
s__=>s__attribute(V__X,s__Solid)))
)

Merge.kif 13809-13818
( ! [V__Process1,V__Process2,V__Number1,V__Number2,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7] :
   ((s__instance(V__Process1,s__Physical)s__and__ms__instance(V__Process2,s__Physical)s__and__ms__instance(V__Number1,s__PositiveInteger)s__and__ms__instance(V__Number2,s__PositiveInteger))
    s__=>((s__processList__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
      s__and__ms__inList(V__Process1,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
  s__and__ms__inList(V__Process2,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
s__and__m(s__ListOrderFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
,V__Number1)
s__equal__mV__Process1)s__and__m(s__ListOrderFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
,V__Number2)
s__equal__mV__Process2)s__and__ms__lessThan(V__Number1,V__Number2))
s__=>s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))
)

( ! [V__Process1,V__Process2,V__Number1,V__Number2,V__ROW2] :
   ((s__instance(V__Process1,s__Physical)s__and__ms__instance(V__Process2,s__Physical)s__and__ms__instance(V__Number1,s__PositiveInteger)s__and__ms__instance(V__Number2,s__PositiveInteger))
    s__=>((s__processList__1(V__ROW2)
      s__and__ms__inList(V__Process1,s__ListFn__1Fn(V__ROW2))
  s__and__ms__inList(V__Process2,s__ListFn__1Fn(V__ROW2))
s__and__m(s__ListOrderFn(s__ListFn__1Fn(V__ROW2)
,V__Number1)
s__equal__mV__Process1)s__and__m(s__ListOrderFn(s__ListFn__1Fn(V__ROW2)
,V__Number2)
s__equal__mV__Process2)s__and__ms__lessThan(V__Number1,V__Number2))
s__=>s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))
)

( ! [V__Process1,V__Process2,V__Number1,V__Number2,V__ROW2,V__ROW3,V__ROW4,V__ROW5] :
   ((s__instance(V__Process1,s__Physical)s__and__ms__instance(V__Process2,s__Physical)s__and__ms__instance(V__Number1,s__PositiveInteger)s__and__ms__instance(V__Number2,s__PositiveInteger))
    s__=>((s__processList__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
      s__and__ms__inList(V__Process1,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
  s__and__ms__inList(V__Process2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
s__and__m(s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
,V__Number1)
s__equal__mV__Process1)s__and__m(s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
,V__Number2)
s__equal__mV__Process2)s__and__ms__lessThan(V__Number1,V__Number2))
s__=>s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))
)

( ! [V__Process1,V__Process2,V__Number1,V__Number2,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8] :
   ((s__instance(V__Process1,s__Physical)s__and__ms__instance(V__Process2,s__Physical)s__and__ms__instance(V__Number1,s__PositiveInteger)s__and__ms__instance(V__Number2,s__PositiveInteger))
    s__=>((s__processList__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
      s__and__ms__inList(V__Process1,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
  s__and__ms__inList(V__Process2,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
s__and__m(s__ListOrderFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
,V__Number1)
s__equal__mV__Process1)s__and__m(s__ListOrderFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
,V__Number2)
s__equal__mV__Process2)s__and__ms__lessThan(V__Number1,V__Number2))
s__=>s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))
)

( ! [V__Process1,V__Process2,V__Number1,V__Number2,V__ROW2,V__ROW3,V__ROW4] :
   ((s__instance(V__Process1,s__Physical)s__and__ms__instance(V__Process2,s__Physical)s__and__ms__instance(V__Number1,s__PositiveInteger)s__and__ms__instance(V__Number2,s__PositiveInteger))
    s__=>((s__processList__3(V__ROW2,V__ROW3,V__ROW4)
      s__and__ms__inList(V__Process1,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
  s__and__ms__inList(V__Process2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
s__and__m(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__Number1)
s__equal__mV__Process1)s__and__m(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__Number2)
s__equal__mV__Process2)s__and__ms__lessThan(V__Number1,V__Number2))
s__=>s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))
)

( ! [V__Process1,V__Process2,V__Number1,V__Number2,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6] :
   ((s__instance(V__Process1,s__Physical)s__and__ms__instance(V__Process2,s__Physical)s__and__ms__instance(V__Number1,s__PositiveInteger)s__and__ms__instance(V__Number2,s__PositiveInteger))
    s__=>((s__processList__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
      s__and__ms__inList(V__Process1,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
  s__and__ms__inList(V__Process2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
s__and__m(s__ListOrderFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
,V__Number1)
s__equal__mV__Process1)s__and__m(s__ListOrderFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
,V__Number2)
s__equal__mV__Process2)s__and__ms__lessThan(V__Number1,V__Number2))
s__=>s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))
)

( ! [V__Process1,V__Process2,V__Number1,V__Number2,V__ROW2,V__ROW3] :
   ((s__instance(V__Process1,s__Physical)s__and__ms__instance(V__Process2,s__Physical)s__and__ms__instance(V__Number1,s__PositiveInteger)s__and__ms__instance(V__Number2,s__PositiveInteger))
    s__=>((s__processList__2(V__ROW2,V__ROW3)
      s__and__ms__inList(V__Process1,s__ListFn__2Fn(V__ROW2,V__ROW3))
  s__and__ms__inList(V__Process2,s__ListFn__2Fn(V__ROW2,V__ROW3))
s__and__m(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__Number1)
s__equal__mV__Process1)s__and__m(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__Number2)
s__equal__mV__Process2)s__and__ms__lessThan(V__Number1,V__Number2))
s__=>s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))
)

QoSontology.kif 690-698
No TPTP formula. May not be expressible in strict first order. Catalog.kif 415-427
No TPTP formula. May not be expressible in strict first order. ComputingBrands.kif 3477-3487
No TPTP formula. May not be expressible in strict first order. ComputingBrands.kif 3500-3510

consequent
-------------------------


( ! [V__ROW2] :
   (s__instance(V__ROW2,s__TimeInterval)s__=>((s__instance(s__duration__m,s__TotalValuedRelation)s__and__ms__instance(s__duration__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__duration__m,s__Relation)s__and__ms__valence(s__duration__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__duration__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__TimeDuration)s__and__ms__duration(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__GeometricFigure)s__=>((s__instance(s__geometricPart__m,s__TotalValuedRelation)s__and__ms__instance(s__geometricPart__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__geometricPart__m,s__Relation)s__and__ms__valence(s__geometricPart__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__geometricPart__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__GeometricFigure)s__and__ms__geometricPart(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Circle)s__=>((s__instance(s__diameter__m,s__TotalValuedRelation)s__and__ms__instance(s__diameter__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__diameter__m,s__Relation)s__and__ms__valence(s__diameter__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__diameter__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__LengthMeasure)s__and__ms__diameter(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Process)s__=>((s__instance(s__subProcess__m,s__TotalValuedRelation)s__and__ms__instance(s__subProcess__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subProcess__m,s__Relation)s__and__ms__valence(s__subProcess__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__subProcess__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Process)s__and__ms__subProcess(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__SelfConnectedObject)s__=>((s__instance(s__approximateDiameter__m,s__TotalValuedRelation)s__and__ms__instance(s__approximateDiameter__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__approximateDiameter__m,s__Relation)s__and__ms__valence(s__approximateDiameter__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__approximateDiameter__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__LengthMeasure)s__and__ms__approximateDiameter(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__SetOrClass)s__=>((s__instance(s__subclass__m,s__TotalValuedRelation)s__and__ms__instance(s__subclass__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subclass__m,s__Relation)s__and__ms__valence(s__subclass__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__subclass__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__SetOrClass)s__and__ms__subclass(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__subclass(V__ROW2,s__ContentBearingPhysical)s__=>((s__instance(s__subsumesContentClass__m,s__TotalValuedRelation)s__and__ms__instance(s__subsumesContentClass__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subsumesContentClass__m,s__Relation)s__and__ms__valence(s__subsumesContentClass__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__subsumesContentClass__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__subclass(V__ITEM,s__ContentBearingPhysical)s__and__ms__subsumesContentClass(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Quantity)s__=>((s__instance(s__greaterThan__m,s__TotalValuedRelation)s__and__ms__instance(s__greaterThan__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__greaterThan__m,s__Relation)s__and__ms__valence(s__greaterThan__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__greaterThan__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Quantity)s__and__ms__greaterThan(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW3,V__ROW2] :
   ((s__instance(V__ROW3,s__Physical)s__and__ms__instance(V__ROW2,s__Physical))
    s__=>((s__instance(s__distance__m,s__TotalValuedRelation)s__and__ms__instance(s__distance__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__distance__m,s__Relation)s__and__ms__valence(s__distance__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__distance__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__LengthMeasure)s__and__ms__distance(V__ROW2,V__ROW3,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Physical)s__=>((s__instance(s__partlyLocated__m,s__TotalValuedRelation)s__and__ms__instance(s__partlyLocated__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__partlyLocated__m,s__Relation)s__and__ms__valence(s__partlyLocated__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__partlyLocated__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Object)s__and__ms__partlyLocated(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Argument)s__=>((s__instance(s__conclusion__m,s__TotalValuedRelation)s__and__ms__instance(s__conclusion__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__conclusion__m,s__Relation)s__and__ms__valence(s__conclusion__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__conclusion__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Proposition)s__and__ms__conclusion(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Process)s__=>((s__instance(s__eventLocated__m,s__TotalValuedRelation)s__and__ms__instance(s__eventLocated__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__eventLocated__m,s__Relation)s__and__ms__valence(s__eventLocated__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__eventLocated__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
s__eventLocated(V__ROW2,V__ITEM))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__List)s__=>((s__instance(s__initialList__m,s__TotalValuedRelation)s__and__ms__instance(s__initialList__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__initialList__m,s__Relation)s__and__ms__valence(s__initialList__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__initialList__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
s__initialList(V__ROW2,V__ITEM))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Relation)s__=>((s__instance(s__subrelation__m,s__TotalValuedRelation)s__and__ms__instance(s__subrelation__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subrelation__m,s__Relation)s__and__ms__valence(s__subrelation__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__subrelation__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Relation)s__and__ms__subrelation(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Motion)s__=>((s__instance(s__path__m,s__TotalValuedRelation)s__and__ms__instance(s__path__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__path__m,s__Relation)s__and__ms__valence(s__path__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__path__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Object)s__and__ms__path(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__TimePosition)s__=>((s__instance(s__temporalPart__m,s__TotalValuedRelation)s__and__ms__instance(s__temporalPart__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__temporalPart__m,s__Relation)s__and__ms__valence(s__temporalPart__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__temporalPart__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__TimePosition)s__and__ms__temporalPart(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__TimeInterval)s__=>((s__instance(s__meetsTemporally__m,s__TotalValuedRelation)s__and__ms__instance(s__meetsTemporally__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__meetsTemporally__m,s__Relation)s__and__ms__valence(s__meetsTemporally__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__meetsTemporally__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__TimeInterval)s__and__ms__meetsTemporally(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Circle)s__=>((s__instance(s__radius__m,s__TotalValuedRelation)s__and__ms__instance(s__radius__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__radius__m,s__Relation)s__and__ms__valence(s__radius__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__radius__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__LengthMeasure)s__and__ms__radius(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Physical)s__=>((s__instance(s__time__m,s__TotalValuedRelation)s__and__ms__instance(s__time__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__time__m,s__Relation)s__and__ms__valence(s__time__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__time__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__TimePosition)s__and__ms__time(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Process)s__=>((s__instance(s__coordinates__m,s__TotalValuedRelation)s__and__ms__instance(s__coordinates__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__coordinates__m,s__Relation)s__and__ms__valence(s__coordinates__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__coordinates__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Process)s__and__ms__coordinates(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Vehicle)s__=>((s__instance(s__maximumPayloadCapacity__m,s__TotalValuedRelation)s__and__ms__instance(s__maximumPayloadCapacity__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__maximumPayloadCapacity__m,s__Relation)s__and__ms__valence(s__maximumPayloadCapacity__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__maximumPayloadCapacity__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__MassMeasure)s__and__ms__maximumPayloadCapacity(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Motion)s__=>((s__instance(s__moves__m,s__TotalValuedRelation)s__and__ms__instance(s__moves__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__moves__m,s__Relation)s__and__ms__valence(s__moves__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__moves__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Object)s__and__ms__moves(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Translocation)s__=>((s__instance(s__changesLocation__m,s__TotalValuedRelation)s__and__ms__instance(s__changesLocation__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__changesLocation__m,s__Relation)s__and__ms__valence(s__changesLocation__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__changesLocation__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Object)s__and__ms__changesLocation(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Argument)s__=>((s__instance(s__premise__m,s__TotalValuedRelation)s__and__ms__instance(s__premise__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__premise__m,s__Relation)s__and__ms__valence(s__premise__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__premise__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Proposition)s__and__ms__premise(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__GraphElement)s__=>((s__instance(s__graphPart__m,s__TotalValuedRelation)s__and__ms__instance(s__graphPart__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__graphPart__m,s__Relation)s__and__ms__valence(s__graphPart__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__graphPart__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Graph)s__and__ms__graphPart(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Contest)s__=>((s__instance(s__contestParticipant__m,s__TotalValuedRelation)s__and__ms__instance(s__contestParticipant__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__contestParticipant__m,s__Relation)s__and__ms__valence(s__contestParticipant__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__contestParticipant__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Agent)s__and__ms__contestParticipant(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW3,V__ROW2] :
   ((s__subclass(V__ROW3,s__Weapon)s__and__ms__instance(V__ROW2,s__MilitaryVehicle))
    s__=>((s__instance(s__weaponCarryingCapability__m,s__TotalValuedRelation)s__and__ms__instance(s__weaponCarryingCapability__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__weaponCarryingCapability__m,s__Relation)s__and__ms__valence(s__weaponCarryingCapability__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__weaponCarryingCapability__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__PositiveInteger)s__and__ms__weaponCarryingCapability(V__ROW2,V__ROW3,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__TimePoint)s__=>((s__instance(s__beforeOrEqual__m,s__TotalValuedRelation)s__and__ms__instance(s__beforeOrEqual__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__beforeOrEqual__m,s__Relation)s__and__ms__valence(s__beforeOrEqual__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__beforeOrEqual__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__TimePoint)s__and__ms__beforeOrEqual(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Organism)s__=>((s__instance(s__parent__m,s__TotalValuedRelation)s__and__ms__instance(s__parent__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__parent__m,s__Relation)s__and__ms__valence(s__parent__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__parent__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Organism)s__and__ms__parent(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__PassengerVehicle)s__=>((s__instance(s__personTransportCapability__m,s__TotalValuedRelation)s__and__ms__instance(s__personTransportCapability__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__personTransportCapability__m,s__Relation)s__and__ms__valence(s__personTransportCapability__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__personTransportCapability__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__PositiveInteger)s__and__ms__personTransportCapability(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__SymbolicString)s__=>((s__instance(s__subString__m,s__TotalValuedRelation)s__and__ms__instance(s__subString__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subString__m,s__Relation)s__and__ms__valence(s__subString__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__subString__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__SymbolicString)s__and__ms__subString(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW3,V__ROW2] :
   ((s__instance(V__ROW3,s__SymbolicString)s__and__ms__instance(V__ROW2,s__SymbolicString))
    s__=>((s__instance(s__stringConcatenation__m,s__TotalValuedRelation)s__and__ms__instance(s__stringConcatenation__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__stringConcatenation__m,s__Relation)s__and__ms__valence(s__stringConcatenation__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__stringConcatenation__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__SymbolicString)s__and__ms__stringConcatenation(V__ROW2,V__ROW3,V__ITEM)))))))))
)

( ! [V__ROW3,V__ROW2] :
   ((s__instance(V__ROW3,s__GeometricPoint)s__and__ms__instance(V__ROW2,s__GeometricPoint))
    s__=>((s__instance(s__geometricDistance__m,s__TotalValuedRelation)s__and__ms__instance(s__geometricDistance__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__geometricDistance__m,s__Relation)s__and__ms__valence(s__geometricDistance__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__geometricDistance__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__LengthMeasure)s__and__ms__geometricDistance(V__ROW2,V__ROW3,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__List)s__=>((s__instance(s__subList__m,s__TotalValuedRelation)s__and__ms__instance(s__subList__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subList__m,s__Relation)s__and__ms__valence(s__subList__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__subList__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__List)s__and__ms__subList(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__ContentBearingPhysical)s__=>((s__instance(s__subsumesContentInstance__m,s__TotalValuedRelation)s__and__ms__instance(s__subsumesContentInstance__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subsumesContentInstance__m,s__Relation)s__and__ms__valence(s__subsumesContentInstance__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__subsumesContentInstance__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__ContentBearingPhysical)s__and__ms__subsumesContentInstance(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Object)s__=>((s__instance(s__smaller__m,s__TotalValuedRelation)s__and__ms__instance(s__smaller__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__smaller__m,s__Relation)s__and__ms__valence(s__smaller__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__smaller__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Object)s__and__ms__smaller(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Quantity)s__=>((s__instance(s__greaterThanOrEqualTo__m,s__TotalValuedRelation)s__and__ms__instance(s__greaterThanOrEqualTo__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__greaterThanOrEqualTo__m,s__Relation)s__and__ms__valence(s__greaterThanOrEqualTo__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__greaterThanOrEqualTo__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Quantity)s__and__ms__greaterThanOrEqualTo(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__FinancialTransaction)s__=>((s__instance(s__transactionAmount__m,s__TotalValuedRelation)s__and__ms__instance(s__transactionAmount__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__transactionAmount__m,s__Relation)s__and__ms__valence(s__transactionAmount__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__transactionAmount__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__CurrencyMeasure)s__and__ms__transactionAmount(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__subclass(V__ROW2,s__Gun)s__=>((s__instance(s__caliber__m,s__TotalValuedRelation)s__and__ms__instance(s__caliber__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__caliber__m,s__Relation)s__and__ms__valence(s__caliber__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__caliber__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__LengthMeasure)s__and__ms__caliber(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Abstract)s__=>((s__instance(s__abstractPart__m,s__TotalValuedRelation)s__and__ms__instance(s__abstractPart__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__abstractPart__m,s__Relation)s__and__ms__valence(s__abstractPart__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__abstractPart__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Abstract)s__and__ms__abstractPart(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Object)s__=>((s__instance(s__larger__m,s__TotalValuedRelation)s__and__ms__instance(s__larger__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__larger__m,s__Relation)s__and__ms__valence(s__larger__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__larger__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Object)s__and__ms__larger(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Language)s__=>((s__instance(s__subLanguage__m,s__TotalValuedRelation)s__and__ms__instance(s__subLanguage__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subLanguage__m,s__Relation)s__and__ms__valence(s__subLanguage__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__subLanguage__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Language)s__and__ms__subLanguage(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW3,V__ROW2] :
   ((s__instance(V__ROW3,s__LengthMeasure)s__and__ms__instance(V__ROW2,s__Vehicle))
    s__=>((s__instance(s__maximumPayloadHeightWidth__m,s__TotalValuedRelation)s__and__ms__instance(s__maximumPayloadHeightWidth__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__maximumPayloadHeightWidth__m,s__Relation)s__and__ms__valence(s__maximumPayloadHeightWidth__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__maximumPayloadHeightWidth__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__LengthMeasure)s__and__ms__maximumPayloadHeightWidth(V__ROW2,V__ROW3,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__TimeInterval)s__=>((s__instance(s__earlier__m,s__TotalValuedRelation)s__and__ms__instance(s__earlier__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__earlier__m,s__Relation)s__and__ms__valence(s__earlier__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__earlier__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__TimeInterval)s__and__ms__earlier(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__OneDimensionalFigure)s__=>((s__instance(s__lineMeasure__m,s__TotalValuedRelation)s__and__ms__instance(s__lineMeasure__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__lineMeasure__m,s__Relation)s__and__ms__valence(s__lineMeasure__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__lineMeasure__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__LengthMeasure)s__and__ms__lineMeasure(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Quantity)s__=>((s__instance(s__lessThanOrEqualTo__m,s__TotalValuedRelation)s__and__ms__instance(s__lessThanOrEqualTo__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__lessThanOrEqualTo__m,s__Relation)s__and__ms__valence(s__lessThanOrEqualTo__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__lessThanOrEqualTo__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Quantity)s__and__ms__lessThanOrEqualTo(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__PureSubstance)s__=>((s__instance(s__protonNumber__m,s__TotalValuedRelation)s__and__ms__instance(s__protonNumber__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__protonNumber__m,s__Relation)s__and__ms__valence(s__protonNumber__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__protonNumber__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__PositiveInteger)s__and__ms__protonNumber(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Collection)s__=>((s__instance(s__subCollection__m,s__TotalValuedRelation)s__and__ms__instance(s__subCollection__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subCollection__m,s__Relation)s__and__ms__valence(s__subCollection__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__subCollection__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Collection)s__and__ms__subCollection(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__PureSubstance)s__=>((s__instance(s__electronNumber__m,s__TotalValuedRelation)s__and__ms__instance(s__electronNumber__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__electronNumber__m,s__Relation)s__and__ms__valence(s__electronNumber__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__electronNumber__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__PositiveInteger)s__and__ms__electronNumber(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__Attribute)s__=>((s__instance(s__subAttribute__m,s__TotalValuedRelation)s__and__ms__instance(s__subAttribute__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__subAttribute__m,s__Relation)s__and__ms__valence(s__subAttribute__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__subAttribute__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__Attribute)s__and__ms__subAttribute(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__NonnegativeInteger)s__=>((s__instance(s__stringLength__m,s__TotalValuedRelation)s__and__ms__instance(s__stringLength__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__stringLength__m,s__Relation)s__and__ms__valence(s__stringLength__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__stringLength__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__SymbolicString)s__and__ms__stringLength(V__ROW2,V__ITEM)))))))))
)

( ! [V__ROW2] :
   (s__instance(V__ROW2,s__TwoDimensionalAngle)s__=>((s__instance(s__angularMeasure__m,s__TotalValuedRelation)s__and__ms__instance(s__angularMeasure__m,s__Predicate))
      s__<=>
      (s__exists__m[V__VALENCE] :
         (s__instance(V__VALENCE,s__PositiveInteger)s__and__m(s__instance(s__angularMeasure__m,s__Relation)s__and__ms__valence(s__angularMeasure__m,V__VALENCE)
        s__and__m((s__forall__m[V__NUMBER,V__ELEMENT,V__CLASS] :
           ((s__instance(V__NUMBER,s__PositiveInteger)s__and__ms__instance(V__CLASS,s__SetOrClass))
            s__=>((s__lessThan(V__NUMBER,V__VALENCE)
              s__and__ms__domain(s__angularMeasure__m,V__NUMBER,V__CLASS)
            s__and__m(V__ELEMENTs__equal__ms__ListOrderFn(s__ListFn__1Fn(V__ROW2)
          ,V__NUMBER)))
    s__=>s__instance(V__ELEMENT,V__CLASS))))
s__=>(s__exists__m[V__ITEM] :
(s__instance(V__ITEM,s__PlaneAngleMeasure)s__and__ms__angularMeasure(V__ROW2,V__ITEM)))))))))
)

Merge.kif 2331-2348 A relation is an instance of total valued relation and the relation is an instance of predicate if and only if there exists a positive integer such that the relation is an instance of relation and the relation %&has the positive integer argument(s) and
No TPTP formula. May not be expressible in strict first order. People.kif 253-277 The deaths per thousand live births of a geopolitical area and the year an integer is equal to a real number if and only if another integer is equal to the number of instances in the class described by a symbolic string and the other integer and 1000 is equal to a quantity and a third integer is equal to the number of instances in the class described by another symbolic string and the third integer and the quantity is equal to the real number
( ! [V__NUMBER] :
   (s__instance(V__NUMBER,s__NegativeRealNumber)s__<=>
    (s__lessThan(V__NUMBER,0)
    s__and__ms__instance(V__NUMBER,s__RealNumber)))
)

Merge.kif 2020-2024 A quantity is an instance of negative real number if and only if the quantity is less than 0 and the quantity is an instance of real number
( ! [V__NUMBER1,V__NUMBER2] :
   ((s__instance(V__NUMBER1,s__Quantity)s__and__ms__instance(V__NUMBER2,s__Quantity))
    s__=>(s__lessThanOrEqualTo(V__NUMBER1,V__NUMBER2)
    s__<=>
    ((V__NUMBER1s__equal__mV__NUMBER2)s__or__ms__lessThan(V__NUMBER1,V__NUMBER2))))
)

Merge.kif 1934-1938 A quantity is less than or equal to another quantity if and only if the quantity is equal to the other quantity or the quantity is less than the other quantity
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 16311-16319
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 16325-16336
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 16342-16353
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 16359-16370
No TPTP formula. May not be expressible in strict first order. Dining.kif 1102-1110
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 3583-3591
No TPTP formula. May not be expressible in strict first order. Merge.kif 2800-2805
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11171-11180
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11102-11111
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11112-11123
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11069-11077
( ! [V__N,V__A] :
   (s__instance(V__N,s__RealNumber)s__=>((s__instance(V__A,s__AcuteAngle)s__and__ms__angularMeasure(V__A,s__MeasureFn(V__N,s__AngularDegree)))
    s__=>s__lessThan(V__N,90)))
)

Mid-level-ontology.kif 5181-5185
No TPTP formula. May not be expressible in strict first order. Dining.kif 729-752
( ! [V__AIRPORT] :
   ((s__instance(V__AIRPORT,s__Airport)s__and__ms__attribute(V__AIRPORT,s__VeryShortRunwayAirport))
    s__=>(s__exists__m[V__RUNWAY,V__LENGTH] :
       (s__instance(V__LENGTH,s__Quantity)s__and__m(s__instance(V__RUNWAY,s__Runway)s__and__ms__part(V__RUNWAY,V__AIRPORT)
      s__and__ms__length(V__RUNWAY,V__LENGTH)
    s__and__ms__lessThan(V__LENGTH,s__MeasureFn(914,s__Meter))))))
)

Transportation.kif 1365-1374
( ! [V__ELEV1,V__AREA] :
   (s__instance(V__ELEV1,s__LengthMeasure)s__=>((s__instance(V__AREA,s__GeographicArea)s__and__ms__geographicSubregion(s__ElevationLowPointFn(V__AREA)
      ,V__AREA)
    s__and__ms__elevation(s__ElevationLowPointFn(V__AREA)
  ,V__ELEV1))
s__=>(s__not__m(s__exists__m[V__OTHER,V__ELEV2] :
(s__instance(V__OTHER,s__GeographicArea)s__and__ms__instance(V__ELEV2,s__LengthMeasure)s__and__m(s__geographicSubregion(V__OTHER,V__AREA)
s__and__m(s__not__m(V__OTHERs__equal__ms__ElevationLowPointFn(V__AREA)))
s__and__ms__elevation(V__OTHER,V__ELEV2)
s__and__ms__lessThan(V__ELEV2,V__ELEV1)))))))
)

Geography.kif 1881-1892
( ! [V__FRACTION,V__AREA,V__WEATHER] :
   (s__instance(V__FRACTION,s__NonnegativeRealNumber)s__=>((s__instance(V__AREA,s__GeographicArea)s__and__ms__instance(V__WEATHER,s__ClearWeather)s__and__ms__eventLocated(V__WEATHER,V__AREA)
      s__and__ms__cloudCoverFraction(V__AREA,V__FRACTION))
  s__=>s__lessThan(V__FRACTION,0.3)))
)

Weather.kif 504-510
( ! [V__AREA,V__WEATHER] :
   ((s__instance(V__AREA,s__GeographicArea)s__and__ms__instance(V__WEATHER,s__ClearWeather)s__and__ms__eventLocated(V__WEATHER,V__AREA))
  s__=>(s__exists__m[V__FRACTION] :
     (s__instance(V__FRACTION,s__NonnegativeRealNumber)s__and__m(s__cloudCoverFraction(V__AREA,V__FRACTION)
    s__and__ms__lessThan(V__FRACTION,0.3)))))
)

Weather.kif 494-502
( ! [V__BOTTOM,V__WIDTH2,V__WIDTH1,V__TOP,V__BOTTLE] :
   ((s__instance(V__BOTTOM,s__SelfConnectedObject)s__and__ms__instance(V__WIDTH2,s__Quantity)s__and__ms__instance(V__WIDTH1,s__Quantity)s__and__ms__instance(V__TOP,s__SelfConnectedObject))
    s__=>((s__instance(V__BOTTLE,s__Bottle)s__and__ms__bottom(V__BOTTOM,V__BOTTLE)
      s__and__ms__top(V__TOP,V__BOTTLE)
    s__and__ms__width(V__BOTTOM,V__WIDTH1)
  s__and__ms__width(V__TOP,V__WIDTH2))
s__=>s__lessThan(V__WIDTH2,V__WIDTH1)))
)

Mid-level-ontology.kif 5023-5030
No TPTP formula. May not be expressible in strict first order. Merge.kif 10920-10933
No TPTP formula. May not be expressible in strict first order. QoSontology.kif 1920-1928
No TPTP formula. May not be expressible in strict first order. Dining.kif 511-520

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement
-------------------------


( ! [V__NUMBER1,V__NUMBER2,V__GRAPH] :
   ((s__instance(V__NUMBER1,s__PositiveInteger)s__and__ms__instance(V__NUMBER2,s__PositiveInteger)s__and__ms__instance(V__GRAPH,s__Graph))
    s__=>(s__not__m(s__exists__m[V__PATH1,V__PATH2] :
       (s__instance(V__PATH1,s__GraphPath)s__and__ms__instance(V__PATH2,s__GraphPath)s__and__m(s__instance(V__PATH1,s__CutSetFn(V__GRAPH))
    s__and__ms__instance(V__PATH2,s__MinimalCutSetFn(V__GRAPH))
s__and__ms__pathLength(V__PATH1,V__NUMBER1)
s__and__ms__pathLength(V__PATH2,V__NUMBER2)
s__and__ms__lessThan(V__NUMBER1,V__NUMBER2))))))
)

Merge.kif 6230-6237 There don't exist a graph path and another graph path such that the graph path is an instance of the set of paths that partition a graph into two separate graphs and the other graph path is an instance of the set of minimal paths that partition the graph into two separate graphs and the length of the graph path is a positive integer and the length of the other graph path is another positive integer and the positive integer is less than the other positive integer


Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)



Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners