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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - instance
instance

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


s__documentation(s__instance__m,s__ChineseLanguage,'如果一个物体属于一个SetOrClass, 这物体就那个 SetOrClass的一个instance。 一个个体可以是许多类别的一个instance, 其中有一些可以是其他类别 的子类别,所以对于instance并没有假设任何具体或独特的含义。')

Merge.kif 90-90
s__documentation(s__instance__m,s__EnglishLanguage,'An object is an instance of a SetOrClass if it is included in that SetOrClass. An individual may be an instance of many classes, some of which may be subclasses of others. Thus, there is no assumption in the meaning of instance about specificity or uniqueness.')

Merge.kif 85-88
s__domain(s__instance__m,1,s__Entity)

Merge.kif 82-82 The number 1 argument of instance is an instance of entity
s__domain(s__instance__m,2,s__SetOrClass)

Merge.kif 83-83 The number 2 argument of instance is an instance of set or class
s__instance(s__BinaryPredicate,s__SetOrClass)

s__instance(s__instance__m,s__BinaryPredicate)

Merge.kif 81-81 instance is an instance of binary predicate

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


s__format(s__ChineseLanguage,s__instance__m,'%1 %n 是 %2 的 instance')

chinese_format.kif 305-305
s__format(s__EnglishLanguage,s__instance__m,'%1 is %n an instance of %2')

english_format.kif 185-185
s__format(s__FrenchLanguage,s__instance__m,'%1 est %n une instance de %2')

french_format.kif 175-175
s__format(s__ItalianLanguage,s__instance__m,'%1 � %n un istanza di %2')

relations-it.txt 149-149
s__format(s__PortugueseLanguage,s__instance__m,'%1 e %n uma instancia de %2')

portuguese_format.kif 127-127
s__format(s__ar__m,s__instance__m,'%1 هو %n مِثَال عن %2')

arabic_format.kif 120-120
s__format(s__cz__m,s__instance__m,'%1 %p{je} %n{nen�} instanc� t��dy %2')

relations-cz.txt 173-173
s__format(s__de__m,s__instance__m,'%1 ist ein fall von %2 %n{nicht}')

relations-de.txt 400-400
s__format(s__hi__m,s__instance__m,'%1 %2 kaa drishhTaanta %n hai')

relations-hindi.txt 188-188
s__format(s__tg__m,s__instance__m,'%1 %n ay ang kasapi sa %2')

relations-tg.txt 302-302
s__relatedInternalConcept(s__member__m,s__instance__m)

Merge.kif 1298-1298 member is internally related to instance
s__subrelation(s__element__m,s__instance__m)

Merge.kif 5472-5472 element is a subrelation of instance
s__subrelation(s__immediateInstance__m,s__instance__m)

Merge.kif 93-93 immediate instance is a subrelation of instance
s__termFormat(s__ChineseLanguage,s__instance__m,'实例')

chinese_format.kif 306-306 "实例" is the printable form of instance in ChineseLanguage
s__termFormat(s__EnglishLanguage,s__instance__m,'instance')

domainEnglishFormat.kif 5458-5458 "instance" is the printable form of instance in english language
s__termFormat(s__ar__m,s__instance__m,'«مِثَال عن»')

arabic_format.kif 570-570 "«مِثَال عن»" is the printable form of instance in ar
s__termFormat(s__tg__m,s__instance__m,'halimbawa')

relations-tg.txt 303-303 "halimbawa" is the printable form of instance in tg

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


( ! [V__Account,V__Agent] :
   ((s__accountHolder(V__Account,V__Agent)
     &
     s__instance(V__Agent,s__Corporation))
   <=>
   s__instance(V__Account,s__CorporateAccount))
)

FinancialOntology.kif 963-967 ?Agent holds account ?Account and ?Agent is an instance of corporation if and only if ?Account is an instance of corporate account
( ! [V__Account,V__Agent] :
   ((s__accountHolder(V__Account,V__Agent)
     &
     s__instance(V__Agent,s__Human))
   <=>
   s__instance(V__Account,s__PersonalAccount))
)

FinancialOntology.kif 941-945 ?Agent holds account ?Account and ?Agent is an instance of human if and only if ?Account is an instance of personal account
( ! [V__AIRCRAFT,V__OBJ2,V__QUANTITY] :
   ((s__altitude(V__AIRCRAFT,V__OBJ2,V__QUANTITY)
     &
     s__surface(V__OBJ2,s__PlanetEarth) &
     s__instance(V__AIRCRAFT,s__Aircraft))
   <=>
   s__absoluteHeight(V__AIRCRAFT,V__QUANTITY))
)

MilitaryDevices.kif 1461-1466 The altitude of ?AIRCRAFT is ?OBJ2 and ?OBJ2 is a surface of planet earth and ?AIRCRAFT is an instance of aircraft if and only if ?QUANTITY is the absolute height of ?AIRCRAFT
( ! [V__INDIVIDUAL,V__CH] :
   ((s__attribute(V__INDIVIDUAL,V__CH)
     &
     s__instance(V__CH,s__Christian))
   <=>
   s__member(V__INDIVIDUAL,s__Christianity))
)

People.kif 797-801 ?CH is an attribute of ?INDIVIDUAL and ?CH is an instance of christian if and only if ?INDIVIDUAL is a member of christianity
( ! [V__NUMBER1,V__NUMBER2] :
   (((s__AbsoluteValueFn(V__NUMBER1)
       = V__NUMBER2)
     &
     s__instance(V__NUMBER1,s__RealNumber) &
     s__instance(V__NUMBER2,s__RealNumber))
   <=>
   ((s__instance(V__NUMBER1,s__NonnegativeRealNumber) &
       (V__NUMBER1 = V__NUMBER2))
     |
     (s__instance(V__NUMBER1,s__NegativeRealNumber) &
       (V__NUMBER2 = minus(0,V__NUMBER1)))))
)

Merge.kif 4894-4905 The absolute value of ?NUMBER1 is equal to ?NUMBER2 and ?NUMBER1 is an instance of real number and ?NUMBER2 is an instance of real number if and only if ?NUMBER1 is an instance of nonnegative real number and ?NUMBER1 is equal to ?NUMBER2 or ?NUMBER1 is an instance of negative real number and ?NUMBER2 is equal to (0 and ?NUMBER1)
( ! [V__AGENT] :
   ((s__instance(V__AGENT,s__SentientAgent) &
       s__attribute(V__AGENT,s__Living))
     <=>
     (? [V__ATTR] :
       (s__instance(V__ATTR,s__ConsciousnessAttribute) &
         s__attribute(V__AGENT,V__ATTR))))
)

Merge.kif 18564-18571 ?AGENT is an instance of sentient agent and living is an attribute of ?AGENT if and only if there exists ?ATTR such that ?ATTR is an instance of consciousness attribute and ?ATTR is an attribute of ?AGENT
( ! [V__Account,V__Agent,V__Asset] :
   ((s__instance(V__Account,s__FinancialAccount) &
       s__possesses(V__Agent,V__Asset)
     &
     (V__Account = s__AccountFn(V__Asset)))
<=>
s__accountHolder(V__Account,V__Agent))
)

FinancialOntology.kif 2252-2257 ?Account is an instance of financial account and ?Agent possesses ?Asset and ?Account is equal to the account of ?Asset if and only if ?Agent holds account ?Account
( ! [V__Account,V__Agent] :
   ((s__instance(V__Account,s__PersonalAccount) &
       greater(s__CardinalityFn(s__KappaFn(V__Agent,'s__accountHolder(V__Account,V__Agent)'))
    ,1))
<=>
s__instance(V__Account,s__JointAccount))
)

FinancialOntology.kif 952-956 ?Account is an instance of personal account and the number of instances in the class described by ?Agent is greater than 1 if and only if ?Account is an instance of joint account
( ! [V__B,V__T] :
   ((s__instance(V__B,s__BodyPart) &
       s__holdsDuring(V__T,'s__attribute(V__B,s__Bare)'))
   <=>
   s__holdsDuring(V__T,'(~ (? [V__C] : (s__instance(V__C,s__Clothing) & s__covers(V__C,V__B))))'))
)

Mid-level-ontology.kif 27891-27901 ?B is an instance of body part and Bare is an attribute of ?B holds during ?T if and only if there doesn't exist ?C such that ?C is an instance of clothing and ?C covers ?B holds during ?T
( ! [V__COMBINE,V__OBJ1,V__OBJ2] :
   ((s__instance(V__COMBINE,s__Combining) &
       s__resource(V__COMBINE,V__OBJ1)
     &
     s__result(V__COMBINE,V__OBJ2))
<=>
(s__holdsDuring(s__BeginFn(s__WhenFn(V__COMBINE))
,'(~ s__part(V__OBJ1,V__OBJ2))')
&
s__holdsDuring(s__EndFn(s__WhenFn(V__COMBINE))
,'s__part(V__OBJ1,V__OBJ2)')))
)

Merge.kif 12240-12247 ?COMBINE is an instance of combining and ?OBJ1 is a resource for ?COMBINE and ?OBJ2 is a result of ?COMBINE if and only if ?OBJ1 is not a part of ?OBJ2 holds during the beginning of the time of existence of ?COMBINE and ?OBJ1 is a part of ?OBJ2 holds during the end of the time of existence of ?COMBINE
( ! [V__LD,V__Size] :
   ((s__instance(V__LD,s__LiquidDrop) &
       s__approximateDiameter(V__LD,s__MeasureFn(V__Size,s__Micrometer))
     &
     less(500,V__Size))
   <=>
   s__instance(V__LD,s__Droplet))
)

Geography.kif 6901-6907 ?LD is an instance of liquid drop and the approximate diameter of ?LD is ?Size micrometer(s) and 500 is less than ?Size if and only if ?LD is an instance of droplet
( ! [V__PERSON] :
   ((s__instance(V__PERSON,s__Human) &
       (! [V__ORG] :
         (~ s__employs(V__ORG,V__PERSON))))
   <=>
   s__attribute(V__PERSON,s__Unemployed))
)

Merge.kif 17467-17473 ?PERSON is an instance of human and for all ?ORG ?ORG doesn't employ ?PERSON if and only if unemployed is an attribute of ?PERSON
( ! [V__PM,V__Particle,V__Size] :
   ((s__instance(V__PM,s__ParticulateMatter) &
       s__part(V__Particle,V__PM)
     &
     s__approximateDiameter(V__Particle,s__MeasureFn(V__Size,s__Micrometer))
   &
   greater(10,V__Size)
   &
   greater(V__Size,2.5))
<=>
(? [V__PM10] :
   s__instance(V__PM10,s__CoarseParticulateMatter)))
)

Geography.kif 6821-6830 ?PM is an instance of PM and ?Particle is a part of ?PM and the approximate diameter of ?Particle is ?Size micrometer(s) and 10 is greater than ?Size and ?Size is greater than 2.5 if and only if there exists ?PM10 such that ?PM10 is an instance of PM10
( ! [V__PM,V__Particle,V__Size] :
   ((s__instance(V__PM,s__ParticulateMatter) &
       s__part(V__Particle,V__PM)
     &
     s__approximateDiameter(V__Particle,s__MeasureFn(V__Size,s__Micrometer))
   &
   greatereq(V__Size,2.5))
<=>
(? [V__PM25] :
   s__instance(V__PM25,s__FineParticulateMatter)))
)

Geography.kif 6848-6856 ?PM is an instance of PM and ?Particle is a part of ?PM and the approximate diameter of ?Particle is ?Size micrometer(s) and ?Size is greater than or equal to 2.5 if and only if there exists ?PM25 such that ?PM25 is an instance of PM2.5
( ! [V__ROW1] :
   ((s__instance(s__parent__m,s__TotalValuedRelation) &
       s__instance(s__parent__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__parent__m,s__Relation) &
         s__valence(s__parent__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__parent__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__parent(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__protonNumber__m,s__TotalValuedRelation) &
       s__instance(s__protonNumber__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__protonNumber__m,s__Relation) &
         s__valence(s__protonNumber__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__protonNumber__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__protonNumber(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__lineMeasure__m,s__TotalValuedRelation) &
       s__instance(s__lineMeasure__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__lineMeasure__m,s__Relation) &
         s__valence(s__lineMeasure__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__lineMeasure__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__lineMeasure(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__earlier__m,s__TotalValuedRelation) &
       s__instance(s__earlier__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__earlier__m,s__Relation) &
         s__valence(s__earlier__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__earlier__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__earlier(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__conclusion__m,s__TotalValuedRelation) &
       s__instance(s__conclusion__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__conclusion__m,s__Relation) &
         s__valence(s__conclusion__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__conclusion__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__conclusion(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__coordinates__m,s__TotalValuedRelation) &
       s__instance(s__coordinates__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__coordinates__m,s__Relation) &
         s__valence(s__coordinates__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__coordinates__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__coordinates(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subCollection__m,s__TotalValuedRelation) &
       s__instance(s__subCollection__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subCollection__m,s__Relation) &
         s__valence(s__subCollection__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subCollection__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subCollection(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__meetsTemporally__m,s__TotalValuedRelation) &
       s__instance(s__meetsTemporally__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__meetsTemporally__m,s__Relation) &
         s__valence(s__meetsTemporally__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__meetsTemporally__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__meetsTemporally(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subrelation__m,s__TotalValuedRelation) &
       s__instance(s__subrelation__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subrelation__m,s__Relation) &
         s__valence(s__subrelation__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subrelation__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subrelation(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(greater__m,s__TotalValuedRelation) &
       s__instance(greater__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(greater__m,s__Relation) &
         s__valence(greater__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(greater__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   greater(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subAttribute__m,s__TotalValuedRelation) &
       s__instance(s__subAttribute__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subAttribute__m,s__Relation) &
         s__valence(s__subAttribute__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subAttribute__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subAttribute(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subclass__m,s__TotalValuedRelation) &
       s__instance(s__subclass__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subclass__m,s__Relation) &
         s__valence(s__subclass__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subclass__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subclass(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__larger__m,s__TotalValuedRelation) &
       s__instance(s__larger__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__larger__m,s__Relation) &
         s__valence(s__larger__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__larger__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__larger(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__maximumPayloadCapacity__m,s__TotalValuedRelation) &
       s__instance(s__maximumPayloadCapacity__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__maximumPayloadCapacity__m,s__Relation) &
         s__valence(s__maximumPayloadCapacity__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__maximumPayloadCapacity__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__maximumPayloadCapacity(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(lesseq__m,s__TotalValuedRelation) &
       s__instance(lesseq__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(lesseq__m,s__Relation) &
         s__valence(lesseq__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(lesseq__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   lesseq(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__partlyLocated__m,s__TotalValuedRelation) &
       s__instance(s__partlyLocated__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__partlyLocated__m,s__Relation) &
         s__valence(s__partlyLocated__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__partlyLocated__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__partlyLocated(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(greatereq__m,s__TotalValuedRelation) &
       s__instance(greatereq__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(greatereq__m,s__Relation) &
         s__valence(greatereq__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(greatereq__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   greatereq(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__moves__m,s__TotalValuedRelation) &
       s__instance(s__moves__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__moves__m,s__Relation) &
         s__valence(s__moves__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__moves__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__moves(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__beforeOrEqual__m,s__TotalValuedRelation) &
       s__instance(s__beforeOrEqual__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__beforeOrEqual__m,s__Relation) &
         s__valence(s__beforeOrEqual__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__beforeOrEqual__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__beforeOrEqual(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__eventLocated__m,s__TotalValuedRelation) &
       s__instance(s__eventLocated__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__eventLocated__m,s__Relation) &
         s__valence(s__eventLocated__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__eventLocated__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__eventLocated(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__smaller__m,s__TotalValuedRelation) &
       s__instance(s__smaller__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__smaller__m,s__Relation) &
         s__valence(s__smaller__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__smaller__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__smaller(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__diameter__m,s__TotalValuedRelation) &
       s__instance(s__diameter__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__diameter__m,s__Relation) &
         s__valence(s__diameter__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__diameter__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__diameter(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__electronNumber__m,s__TotalValuedRelation) &
       s__instance(s__electronNumber__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__electronNumber__m,s__Relation) &
         s__valence(s__electronNumber__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__electronNumber__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__electronNumber(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__personTransportCapability__m,s__TotalValuedRelation) &
       s__instance(s__personTransportCapability__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__personTransportCapability__m,s__Relation) &
         s__valence(s__personTransportCapability__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__personTransportCapability__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__personTransportCapability(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__abstractPart__m,s__TotalValuedRelation) &
       s__instance(s__abstractPart__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__abstractPart__m,s__Relation) &
         s__valence(s__abstractPart__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__abstractPart__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__abstractPart(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__transactionAmount__m,s__TotalValuedRelation) &
       s__instance(s__transactionAmount__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__transactionAmount__m,s__Relation) &
         s__valence(s__transactionAmount__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__transactionAmount__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__transactionAmount(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__time__m,s__TotalValuedRelation) &
       s__instance(s__time__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__time__m,s__Relation) &
         s__valence(s__time__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__time__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__time(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__caliber__m,s__TotalValuedRelation) &
       s__instance(s__caliber__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__caliber__m,s__Relation) &
         s__valence(s__caliber__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__caliber__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__caliber(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__graphPart__m,s__TotalValuedRelation) &
       s__instance(s__graphPart__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__graphPart__m,s__Relation) &
         s__valence(s__graphPart__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__graphPart__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__graphPart(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__geometricPart__m,s__TotalValuedRelation) &
       s__instance(s__geometricPart__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__geometricPart__m,s__Relation) &
         s__valence(s__geometricPart__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__geometricPart__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__geometricPart(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__changesLocation__m,s__TotalValuedRelation) &
       s__instance(s__changesLocation__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__changesLocation__m,s__Relation) &
         s__valence(s__changesLocation__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__changesLocation__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__changesLocation(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__temporalPart__m,s__TotalValuedRelation) &
       s__instance(s__temporalPart__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__temporalPart__m,s__Relation) &
         s__valence(s__temporalPart__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__temporalPart__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__temporalPart(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__path__m,s__TotalValuedRelation) &
       s__instance(s__path__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__path__m,s__Relation) &
         s__valence(s__path__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__path__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__path(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__premise__m,s__TotalValuedRelation) &
       s__instance(s__premise__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__premise__m,s__Relation) &
         s__valence(s__premise__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__premise__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__premise(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subsumesContentClass__m,s__TotalValuedRelation) &
       s__instance(s__subsumesContentClass__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subsumesContentClass__m,s__Relation) &
         s__valence(s__subsumesContentClass__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subsumesContentClass__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subsumesContentClass(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subProcess__m,s__TotalValuedRelation) &
       s__instance(s__subProcess__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subProcess__m,s__Relation) &
         s__valence(s__subProcess__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subProcess__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subProcess(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__radius__m,s__TotalValuedRelation) &
       s__instance(s__radius__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__radius__m,s__Relation) &
         s__valence(s__radius__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__radius__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__radius(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subsumesContentInstance__m,s__TotalValuedRelation) &
       s__instance(s__subsumesContentInstance__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subsumesContentInstance__m,s__Relation) &
         s__valence(s__subsumesContentInstance__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subsumesContentInstance__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subsumesContentInstance(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__contestParticipant__m,s__TotalValuedRelation) &
       s__instance(s__contestParticipant__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__contestParticipant__m,s__Relation) &
         s__valence(s__contestParticipant__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__contestParticipant__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__contestParticipant(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__stringLength__m,s__TotalValuedRelation) &
       s__instance(s__stringLength__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__stringLength__m,s__Relation) &
         s__valence(s__stringLength__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__stringLength__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__stringLength(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subList__m,s__TotalValuedRelation) &
       s__instance(s__subList__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subList__m,s__Relation) &
         s__valence(s__subList__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subList__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subList(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__angularMeasure__m,s__TotalValuedRelation) &
       s__instance(s__angularMeasure__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__angularMeasure__m,s__Relation) &
         s__valence(s__angularMeasure__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__angularMeasure__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__angularMeasure(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subLanguage__m,s__TotalValuedRelation) &
       s__instance(s__subLanguage__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subLanguage__m,s__Relation) &
         s__valence(s__subLanguage__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subLanguage__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subLanguage(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__duration__m,s__TotalValuedRelation) &
       s__instance(s__duration__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__duration__m,s__Relation) &
         s__valence(s__duration__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__duration__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__duration(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__initialList__m,s__TotalValuedRelation) &
       s__instance(s__initialList__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__initialList__m,s__Relation) &
         s__valence(s__initialList__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__initialList__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__initialList(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subString__m,s__TotalValuedRelation) &
       s__instance(s__subString__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subString__m,s__Relation) &
         s__valence(s__subString__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subString__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subString(V__ROW1,V__ITEM))))))
)

Merge.kif 2308-2325 ?REL is an instance of total valued relation and ?REL is an instance of predicate if and only if there exists ?VALENCE such that ?REL is an instance of relation and ?REL %&has ?VALENCE argument(s) and
  • if for all ?NUMBER, ?ELEMENT and ?CLASS
    • if ?NUMBER is less than ?VALENCE and the number ?NUMBER argument of ?REL is an instance of ?CLASS and ?ELEMENT is equal to ?NUMBERth element of (@ROW),
    • then ?ELEMENT is an instance of ?CLASS
    ,
  • then there exists ?ITEM such that ?REL @ROW and ?ITEM
( ! [V__SCROLL] :
   ((s__instance(V__SCROLL,s__WindowScrolling) &
       s__instance(V__SCROLL,s__UserSignifiedGraphicalAction))
     <=>
     s__instance(V__SCROLL,s__WindowScrollingByUser))
   )

ComputerInput.kif 1433-1437 ?SCROLL is an instance of WindowScrolling and ?SCROLL is an instance of UserSignifiedGraphicalAction if and only if ?SCROLL is an instance of WindowScrollingByUser
( ! [V__UNIT,V__AMOUNT] :
   ((s__instance(V__UNIT,s__UnitOfMeasure) &
       (V__AMOUNT = s__MeasureFn(1,s__SquareUnitFn(V__UNIT))))
<=>
(V__AMOUNT = times(s__MeasureFn(1,V__UNIT)
  ,s__MeasureFn(1,V__UNIT))))
)

Geography.kif 3748-3752 ?UNIT is an instance of unit of measure and ?AMOUNT is equal to 1 the square unit of ?UNIT(s) if and only if ?AMOUNT is equal to 1 ?UNIT(s) and 1 ?UNIT(s)
( ! [V__Withdrawal,V__Account] :
   ((s__instance(V__Withdrawal,s__Withdrawal) &
       s__instance(V__Account,s__FinancialAccount) &
       s__origin(V__Withdrawal,s__CurrencyFn(V__Account))
   &
   (~ (? [V__Penalty] :
       (s__instance(V__Penalty,s__Penalty) &
         s__destination(V__Penalty,s__CurrencyFn(V__Account))
     &
     s__causes(V__Withdrawal,V__Penalty)))))
<=>
s__liquidity(V__Account,s__HighLiquidity))
)

FinancialOntology.kif 1756-1766 ?Withdrawal is an instance of withdrawal and ?Account is an instance of financial account and ?Withdrawal originates at the currency of ?Account and there doesn't exist ?Penalty such that ?Penalty is an instance of penalty and ?Penalty ends up at the currency of ?Account and ?Withdrawal causes ?Penalty if and only if the liqudity of ?Account is high liquidity
( ! [V__X,V__T] :
   ((s__instance(V__X,s__Region) &
       s__holdsDuring(V__T,'s__property(V__X,s__StandardAmbientTemperaturePressure)'))
   <=>
   s__holdsDuring(V__T,'(s__airTemperature(V__X,s__MeasureFn(298.15,s__KelvinDegree)) & s__barometricPressure(V__X,s__MeasureFn(29.530,s__InchMercury)))'))
)

Weather.kif 1086-1096 ?X is an instance of region and ?X has an attribute standard ambient temperature and pressure holds during ?T if and only if 298.15 kelvin degree(s) is an air temperature of ?X and 29.530 inch mercury(s) is a barometric pressure of ?X holds during ?T
( ! [V__PLACE,V__AREA] :
   ((s__located(V__PLACE,V__AREA)
     &
     s__instance(V__PLACE,s__PostalPlace) &
     s__instance(V__AREA,s__PostcodeArea))
   <=>
   s__postPostcodeArea(V__PLACE,V__AREA))
)

Mid-level-ontology.kif 22192-22197 ?PLACE is located at ?AREA and ?PLACE is an instance of PostalPlace and ?AREA is an instance of PostcodeArea if and only if ?PLACE is in post code ?AREA
( ! [V__PLACE,V__GEO] :
   ((s__located(V__PLACE,V__GEO)
     &
     s__instance(V__PLACE,s__PostalPlace) &
     s__instance(V__GEO,s__City))
   <=>
   s__postCity(V__PLACE,V__GEO))
)

Mid-level-ontology.kif 22165-22170 ?PLACE is located at ?GEO and ?PLACE is an instance of PostalPlace and ?GEO is an instance of city if and only if ?PLACE is in ?GEO
( ! [V__PLACE,V__GEO] :
   ((s__located(V__PLACE,V__GEO)
     &
     s__instance(V__PLACE,s__PostalPlace) &
     s__instance(V__GEO,s__Neighborhood))
   <=>
   s__postNeighborhood(V__PLACE,V__GEO))
)

Mid-level-ontology.kif 22078-22083 ?PLACE is located at ?GEO and ?PLACE is an instance of PostalPlace and ?GEO is an instance of neighborhood if and only if ?PLACE is in ?GEO
( ! [V__PLACE,V__GEO] :
   ((s__located(V__PLACE,V__GEO)
     &
     s__instance(V__PLACE,s__PostalPlace) &
     s__instance(V__GEO,s__StateOrProvince))
   <=>
   s__postDistrict(V__PLACE,V__GEO))
)

Mid-level-ontology.kif 22149-22154 ?PLACE is located at ?GEO and ?PLACE is an instance of PostalPlace and ?GEO is an instance of state or province if and only if ?PLACE is in ?GEO
( ! [V__PLACE,V__GEO] :
   ((s__located(V__PLACE,V__GEO)
     &
     s__instance(V__PLACE,s__PostalPlace) &
     (s__instance(V__GEO,s__Nation) |
       s__instance(V__GEO,s__DependencyOrSpecialSovereigntyArea)))
   <=>
   s__postCountry(V__PLACE,V__GEO))
)

Mid-level-ontology.kif 22115-22122 ?PLACE is located at ?GEO and ?PLACE is an instance of PostalPlace and ?GEO is an instance of nation or ?GEO is an instance of dependency or special sovereignty area if and only if ?PLACE is in ?GEO
( ! [V__PHYS,V__TIME] :
   ((s__time(V__PHYS,V__TIME)
     &
     s__instance(V__TIME,s__TimePoint))
   <=>
   s__temporallyBetweenOrEqual(s__BeginFn(s__WhenFn(V__PHYS))
,V__TIME,s__EndFn(s__WhenFn(V__PHYS))))
)

Merge.kif 8338-8342 ?PHYS exists during ?TIME and ?TIME is an instance of time point if and only if ?TIME is between or at the beginning of the time of existence of ?PHYS and the end of the time of existence of ?PHYS

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


( ! [V__Account,V__Agent] :
   ((s__accountHolder(V__Account,V__Agent)
     &
     s__instance(V__Agent,s__Corporation))
   <=>
   s__instance(V__Account,s__CorporateAccount))
)

FinancialOntology.kif 963-967 ?Agent holds account ?Account and ?Agent is an instance of corporation if and only if ?Account is an instance of corporate account
( ! [V__Account,V__Agent] :
   ((s__accountHolder(V__Account,V__Agent)
     &
     s__instance(V__Agent,s__Human))
   <=>
   s__instance(V__Account,s__PersonalAccount))
)

FinancialOntology.kif 941-945 ?Agent holds account ?Account and ?Agent is an instance of human if and only if ?Account is an instance of personal account
( ! [V__NUMBER1,V__NUMBER2] :
   (((s__AbsoluteValueFn(V__NUMBER1)
       = V__NUMBER2)
     &
     s__instance(V__NUMBER1,s__RealNumber) &
     s__instance(V__NUMBER2,s__RealNumber))
   <=>
   ((s__instance(V__NUMBER1,s__NonnegativeRealNumber) &
       (V__NUMBER1 = V__NUMBER2))
     |
     (s__instance(V__NUMBER1,s__NegativeRealNumber) &
       (V__NUMBER2 = minus(0,V__NUMBER1)))))
)

Merge.kif 4894-4905 The absolute value of ?NUMBER1 is equal to ?NUMBER2 and ?NUMBER1 is an instance of real number and ?NUMBER2 is an instance of real number if and only if ?NUMBER1 is an instance of nonnegative real number and ?NUMBER1 is equal to ?NUMBER2 or ?NUMBER1 is an instance of negative real number and ?NUMBER2 is equal to (0 and ?NUMBER1)
( ! [V__AGENT] :
   ((s__instance(V__AGENT,s__SentientAgent) &
       s__attribute(V__AGENT,s__Living))
     <=>
     (? [V__ATTR] :
       (s__instance(V__ATTR,s__ConsciousnessAttribute) &
         s__attribute(V__AGENT,V__ATTR))))
)

Merge.kif 18564-18571 ?AGENT is an instance of sentient agent and living is an attribute of ?AGENT if and only if there exists ?ATTR such that ?ATTR is an instance of consciousness attribute and ?ATTR is an attribute of ?AGENT
( ! [V__Account,V__Agent] :
   ((s__instance(V__Account,s__PersonalAccount) &
       greater(s__CardinalityFn(s__KappaFn(V__Agent,'s__accountHolder(V__Account,V__Agent)'))
    ,1))
<=>
s__instance(V__Account,s__JointAccount))
)

FinancialOntology.kif 952-956 ?Account is an instance of personal account and the number of instances in the class described by ?Agent is greater than 1 if and only if ?Account is an instance of joint account
( ! [V__B,V__T] :
   ((s__instance(V__B,s__BodyPart) &
       s__holdsDuring(V__T,'s__attribute(V__B,s__Bare)'))
   <=>
   s__holdsDuring(V__T,'(~ (? [V__C] : (s__instance(V__C,s__Clothing) & s__covers(V__C,V__B))))'))
)

Mid-level-ontology.kif 27891-27901 ?B is an instance of body part and Bare is an attribute of ?B holds during ?T if and only if there doesn't exist ?C such that ?C is an instance of clothing and ?C covers ?B holds during ?T
( ! [V__LD,V__Size] :
   ((s__instance(V__LD,s__LiquidDrop) &
       s__approximateDiameter(V__LD,s__MeasureFn(V__Size,s__Micrometer))
     &
     less(500,V__Size))
   <=>
   s__instance(V__LD,s__Droplet))
)

Geography.kif 6901-6907 ?LD is an instance of liquid drop and the approximate diameter of ?LD is ?Size micrometer(s) and 500 is less than ?Size if and only if ?LD is an instance of droplet
( ! [V__PM,V__Particle,V__Size] :
   ((s__instance(V__PM,s__ParticulateMatter) &
       s__part(V__Particle,V__PM)
     &
     s__approximateDiameter(V__Particle,s__MeasureFn(V__Size,s__Micrometer))
   &
   greater(10,V__Size)
   &
   greater(V__Size,2.5))
<=>
(? [V__PM10] :
   s__instance(V__PM10,s__CoarseParticulateMatter)))
)

Geography.kif 6821-6830 ?PM is an instance of PM and ?Particle is a part of ?PM and the approximate diameter of ?Particle is ?Size micrometer(s) and 10 is greater than ?Size and ?Size is greater than 2.5 if and only if there exists ?PM10 such that ?PM10 is an instance of PM10
( ! [V__PM,V__Particle,V__Size] :
   ((s__instance(V__PM,s__ParticulateMatter) &
       s__part(V__Particle,V__PM)
     &
     s__approximateDiameter(V__Particle,s__MeasureFn(V__Size,s__Micrometer))
   &
   greatereq(V__Size,2.5))
<=>
(? [V__PM25] :
   s__instance(V__PM25,s__FineParticulateMatter)))
)

Geography.kif 6848-6856 ?PM is an instance of PM and ?Particle is a part of ?PM and the approximate diameter of ?Particle is ?Size micrometer(s) and ?Size is greater than or equal to 2.5 if and only if there exists ?PM25 such that ?PM25 is an instance of PM2.5
( ! [V__ROW1] :
   ((s__instance(s__parent__m,s__TotalValuedRelation) &
       s__instance(s__parent__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__parent__m,s__Relation) &
         s__valence(s__parent__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__parent__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__parent(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__protonNumber__m,s__TotalValuedRelation) &
       s__instance(s__protonNumber__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__protonNumber__m,s__Relation) &
         s__valence(s__protonNumber__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__protonNumber__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__protonNumber(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__lineMeasure__m,s__TotalValuedRelation) &
       s__instance(s__lineMeasure__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__lineMeasure__m,s__Relation) &
         s__valence(s__lineMeasure__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__lineMeasure__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__lineMeasure(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__earlier__m,s__TotalValuedRelation) &
       s__instance(s__earlier__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__earlier__m,s__Relation) &
         s__valence(s__earlier__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__earlier__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__earlier(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__conclusion__m,s__TotalValuedRelation) &
       s__instance(s__conclusion__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__conclusion__m,s__Relation) &
         s__valence(s__conclusion__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__conclusion__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__conclusion(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__coordinates__m,s__TotalValuedRelation) &
       s__instance(s__coordinates__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__coordinates__m,s__Relation) &
         s__valence(s__coordinates__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__coordinates__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__coordinates(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subCollection__m,s__TotalValuedRelation) &
       s__instance(s__subCollection__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subCollection__m,s__Relation) &
         s__valence(s__subCollection__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subCollection__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subCollection(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__meetsTemporally__m,s__TotalValuedRelation) &
       s__instance(s__meetsTemporally__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__meetsTemporally__m,s__Relation) &
         s__valence(s__meetsTemporally__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__meetsTemporally__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__meetsTemporally(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subrelation__m,s__TotalValuedRelation) &
       s__instance(s__subrelation__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subrelation__m,s__Relation) &
         s__valence(s__subrelation__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subrelation__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subrelation(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(greater__m,s__TotalValuedRelation) &
       s__instance(greater__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(greater__m,s__Relation) &
         s__valence(greater__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(greater__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   greater(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subAttribute__m,s__TotalValuedRelation) &
       s__instance(s__subAttribute__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subAttribute__m,s__Relation) &
         s__valence(s__subAttribute__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subAttribute__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subAttribute(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subclass__m,s__TotalValuedRelation) &
       s__instance(s__subclass__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subclass__m,s__Relation) &
         s__valence(s__subclass__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subclass__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subclass(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__larger__m,s__TotalValuedRelation) &
       s__instance(s__larger__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__larger__m,s__Relation) &
         s__valence(s__larger__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__larger__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__larger(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__maximumPayloadCapacity__m,s__TotalValuedRelation) &
       s__instance(s__maximumPayloadCapacity__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__maximumPayloadCapacity__m,s__Relation) &
         s__valence(s__maximumPayloadCapacity__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__maximumPayloadCapacity__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__maximumPayloadCapacity(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(lesseq__m,s__TotalValuedRelation) &
       s__instance(lesseq__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(lesseq__m,s__Relation) &
         s__valence(lesseq__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(lesseq__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   lesseq(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__partlyLocated__m,s__TotalValuedRelation) &
       s__instance(s__partlyLocated__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__partlyLocated__m,s__Relation) &
         s__valence(s__partlyLocated__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__partlyLocated__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__partlyLocated(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(greatereq__m,s__TotalValuedRelation) &
       s__instance(greatereq__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(greatereq__m,s__Relation) &
         s__valence(greatereq__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(greatereq__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   greatereq(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__moves__m,s__TotalValuedRelation) &
       s__instance(s__moves__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__moves__m,s__Relation) &
         s__valence(s__moves__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__moves__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__moves(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__beforeOrEqual__m,s__TotalValuedRelation) &
       s__instance(s__beforeOrEqual__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__beforeOrEqual__m,s__Relation) &
         s__valence(s__beforeOrEqual__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__beforeOrEqual__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__beforeOrEqual(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__eventLocated__m,s__TotalValuedRelation) &
       s__instance(s__eventLocated__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__eventLocated__m,s__Relation) &
         s__valence(s__eventLocated__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__eventLocated__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__eventLocated(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__smaller__m,s__TotalValuedRelation) &
       s__instance(s__smaller__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__smaller__m,s__Relation) &
         s__valence(s__smaller__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__smaller__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__smaller(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__diameter__m,s__TotalValuedRelation) &
       s__instance(s__diameter__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__diameter__m,s__Relation) &
         s__valence(s__diameter__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__diameter__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__diameter(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__electronNumber__m,s__TotalValuedRelation) &
       s__instance(s__electronNumber__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__electronNumber__m,s__Relation) &
         s__valence(s__electronNumber__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__electronNumber__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__electronNumber(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__personTransportCapability__m,s__TotalValuedRelation) &
       s__instance(s__personTransportCapability__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__personTransportCapability__m,s__Relation) &
         s__valence(s__personTransportCapability__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__personTransportCapability__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__personTransportCapability(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__abstractPart__m,s__TotalValuedRelation) &
       s__instance(s__abstractPart__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__abstractPart__m,s__Relation) &
         s__valence(s__abstractPart__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__abstractPart__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__abstractPart(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__transactionAmount__m,s__TotalValuedRelation) &
       s__instance(s__transactionAmount__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__transactionAmount__m,s__Relation) &
         s__valence(s__transactionAmount__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__transactionAmount__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__transactionAmount(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__time__m,s__TotalValuedRelation) &
       s__instance(s__time__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__time__m,s__Relation) &
         s__valence(s__time__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__time__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__time(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__caliber__m,s__TotalValuedRelation) &
       s__instance(s__caliber__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__caliber__m,s__Relation) &
         s__valence(s__caliber__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__caliber__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__caliber(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__graphPart__m,s__TotalValuedRelation) &
       s__instance(s__graphPart__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__graphPart__m,s__Relation) &
         s__valence(s__graphPart__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__graphPart__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__graphPart(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__geometricPart__m,s__TotalValuedRelation) &
       s__instance(s__geometricPart__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__geometricPart__m,s__Relation) &
         s__valence(s__geometricPart__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__geometricPart__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__geometricPart(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__changesLocation__m,s__TotalValuedRelation) &
       s__instance(s__changesLocation__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__changesLocation__m,s__Relation) &
         s__valence(s__changesLocation__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__changesLocation__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__changesLocation(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__temporalPart__m,s__TotalValuedRelation) &
       s__instance(s__temporalPart__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__temporalPart__m,s__Relation) &
         s__valence(s__temporalPart__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__temporalPart__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__temporalPart(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__path__m,s__TotalValuedRelation) &
       s__instance(s__path__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__path__m,s__Relation) &
         s__valence(s__path__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__path__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__path(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__premise__m,s__TotalValuedRelation) &
       s__instance(s__premise__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__premise__m,s__Relation) &
         s__valence(s__premise__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__premise__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__premise(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subsumesContentClass__m,s__TotalValuedRelation) &
       s__instance(s__subsumesContentClass__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subsumesContentClass__m,s__Relation) &
         s__valence(s__subsumesContentClass__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subsumesContentClass__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subsumesContentClass(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subProcess__m,s__TotalValuedRelation) &
       s__instance(s__subProcess__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subProcess__m,s__Relation) &
         s__valence(s__subProcess__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subProcess__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subProcess(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__radius__m,s__TotalValuedRelation) &
       s__instance(s__radius__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__radius__m,s__Relation) &
         s__valence(s__radius__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__radius__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__radius(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subsumesContentInstance__m,s__TotalValuedRelation) &
       s__instance(s__subsumesContentInstance__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subsumesContentInstance__m,s__Relation) &
         s__valence(s__subsumesContentInstance__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subsumesContentInstance__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subsumesContentInstance(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__contestParticipant__m,s__TotalValuedRelation) &
       s__instance(s__contestParticipant__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__contestParticipant__m,s__Relation) &
         s__valence(s__contestParticipant__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__contestParticipant__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__contestParticipant(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__stringLength__m,s__TotalValuedRelation) &
       s__instance(s__stringLength__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__stringLength__m,s__Relation) &
         s__valence(s__stringLength__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__stringLength__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__stringLength(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subList__m,s__TotalValuedRelation) &
       s__instance(s__subList__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subList__m,s__Relation) &
         s__valence(s__subList__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subList__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subList(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__angularMeasure__m,s__TotalValuedRelation) &
       s__instance(s__angularMeasure__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__angularMeasure__m,s__Relation) &
         s__valence(s__angularMeasure__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__angularMeasure__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__angularMeasure(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subLanguage__m,s__TotalValuedRelation) &
       s__instance(s__subLanguage__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subLanguage__m,s__Relation) &
         s__valence(s__subLanguage__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subLanguage__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subLanguage(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__duration__m,s__TotalValuedRelation) &
       s__instance(s__duration__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__duration__m,s__Relation) &
         s__valence(s__duration__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__duration__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__duration(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__initialList__m,s__TotalValuedRelation) &
       s__instance(s__initialList__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__initialList__m,s__Relation) &
         s__valence(s__initialList__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__initialList__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__initialList(V__ROW1,V__ITEM))))))
)

( ! [V__ROW1] :
   ((s__instance(s__subString__m,s__TotalValuedRelation) &
       s__instance(s__subString__m,s__Predicate))
     <=>
     (? [V__VALENCE] :
       (s__instance(s__subString__m,s__Relation) &
         s__valence(s__subString__m,V__VALENCE)
       &
       ((! [V__NUMBER,V__ELEMENT,V__CLASS] :
           ((less(V__NUMBER,V__VALENCE)
               &
               s__domain(s__subString__m,V__NUMBER,V__CLASS)
             &
             (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
            ,V__NUMBER)))
       =>
       s__instance(V__ELEMENT,V__CLASS)))
=>
(? [V__ITEM] :
   s__subString(V__ROW1,V__ITEM))))))
)

Merge.kif 2308-2325 ?REL is an instance of total valued relation and ?REL is an instance of predicate if and only if there exists ?VALENCE such that ?REL is an instance of relation and ?REL %&has ?VALENCE argument(s) and
  • if for all ?NUMBER, ?ELEMENT and ?CLASS
    • if ?NUMBER is less than ?VALENCE and the number ?NUMBER argument of ?REL is an instance of ?CLASS and ?ELEMENT is equal to ?NUMBERth element of (@ROW),
    • then ?ELEMENT is an instance of ?CLASS
    ,
  • then there exists ?ITEM such that ?REL @ROW and ?ITEM
( ! [V__SCROLL] :
   ((s__instance(V__SCROLL,s__WindowScrolling) &
       s__instance(V__SCROLL,s__UserSignifiedGraphicalAction))
     <=>
     s__instance(V__SCROLL,s__WindowScrollingByUser))
   )

ComputerInput.kif 1433-1437 ?SCROLL is an instance of WindowScrolling and ?SCROLL is an instance of UserSignifiedGraphicalAction if and only if ?SCROLL is an instance of WindowScrollingByUser
( ! [V__AREA,V__AMOUNT,V__PERIOD] :
   (s__annualExpendituresOfAreaInPeriod(V__AREA,V__AMOUNT,V__PERIOD)
   <=>
   (? [V__TIME] :
     (s__instance(V__TIME,V__PERIOD)
     &
     s__holdsDuring(V__TIME,'s__annualExpendituresOfArea(V__AREA,V__AMOUNT)'))))
)

Economy.kif 1523-1528 ?AREA annual expenditures of area in period ?AMOUNT for ?PERIOD if and only if there exists ?TIME such that ?TIME is an instance of ?PERIOD and ?AMOUNT is an annual expenditures of area of ?AREA holds during ?TIME
( ! [V__AREA,V__AMOUNT,V__PERIOD] :
   (s__annualRevenuesOfAreaInPeriod(V__AREA,V__AMOUNT,V__PERIOD)
   <=>
   (? [V__TIME] :
     (s__instance(V__TIME,V__PERIOD)
     &
     s__holdsDuring(V__TIME,'s__annualRevenuesOfArea(V__AREA,V__AMOUNT)'))))
)

Economy.kif 1494-1499 ?AREA annual revenues of area in period ?AMOUNT for ?PERIOD if and only if there exists ?TIME such that ?TIME is an instance of ?PERIOD and ?AMOUNT is an annual revenues of area of ?AREA holds during ?TIME
( ! [V__HOLE1] :
   (s__attribute(V__HOLE1,s__Fillable) <=>
     (? [V__HOLE2] :
       (s__instance(V__HOLE2,s__Hole) &
         s__part(V__HOLE1,V__HOLE2))))
)

Merge.kif 9855-9860 Fillable is an attribute of ?HOLE1 if and only if there exists ?HOLE2 such that ?HOLE2 is an instance of hole and ?HOLE1 is a part of ?HOLE2
( ! [V__MUSIC] :
   (s__attribute(V__MUSIC,s__PolyphonicMusic) <=>
     (? [V__PART1,V__PART2] :
       (s__instance(V__MUSIC,s__MakingMusic) &
         s__instance(V__PART1,s__MakingMusic) &
         s__instance(V__PART2,s__MakingMusic) &
         s__subProcess(V__PART1,V__MUSIC)
       &
       s__subProcess(V__PART2,V__MUSIC)
     &
     (~ (V__PART1 = V__PART2))
     &
     s__cooccur(V__PART1,V__MUSIC)
   &
   s__cooccur(V__PART2,V__MUSIC))))
)

Mid-level-ontology.kif 927-938 Polyphonic music is an attribute of ?MUSIC if and only if there exist ?PART1 and ?PART2 such that ?MUSIC is an instance of making music and ?PART1 is an instance of making music and ?PART2 is an instance of making music and ?PART1 is a subprocess of ?MUSIC and ?PART2 is a subprocess of ?MUSIC and ?PART1 is not equal to ?PART2 and ?PART1 occurs at the same time as ?MUSIC and ?PART2 occurs at the same time as ?MUSIC
( ! [V__WATER,V__AREA,V__DIST] :
   (s__attribute(V__WATER,s__OpenSea) <=>
     (! [V__LAND] :
       (s__instance(V__AREA,s__SaltWaterArea) &
         (~ s__instance(V__WATER,s__LandlockedWater))
         &
         s__distance(V__LAND,V__WATER,V__DIST)
       &
       greater(V__DIST,s__MeasureFn(5,s__NauticalMile)))))
)

Geography.kif 4409-4416 Open sea is an attribute of ?WATER if and only if for all ?LAND ?AREA is an instance of salt water area and ?WATER is not an instance of landlocked water and the distance between ?LAND and ?WATER is ?DIST and ?DIST is greater than 5 nautical mile(s)
( ! [V__AccountType,V__Bank] :
   (s__bankAccount(V__AccountType,V__Bank)
   <=>
   (? [V__Account] :
     (s__instance(V__Account,V__AccountType)
     &
     s__accountAt(V__Account,V__Bank))))
)

FinancialOntology.kif 3779-3784 ?Bank is a bank account of ?AccountType if and only if there exists ?Account such that ?Account is an instance of ?AccountType and ?Account is held by ?Bank
( ! [V__AREA,V__CAPAMOUNT,V__PERIOD,V__AMOUNT] :
   (s__capitalExpendituresOfAreaInPeriod(V__AREA,V__CAPAMOUNT,V__PERIOD)
   <=>
   (? [V__TIME] :
     (s__instance(V__TIME,V__PERIOD)
     &
     s__holdsDuring(V__TIME,'s__capitalExpendituresOfArea(V__AREA,V__AMOUNT)'))))
)

Economy.kif 1569-1574 ?AREA capital expenditures of area in period ?CAPAMOUNT for ?PERIOD if and only if there exists ?TIME such that ?TIME is an instance of ?PERIOD and ?AMOUNT is a capital expenditures of area of ?AREA holds during ?TIME
( ! [V__AMOUNT,V__PERIOD] :
   (s__currencyExchangePerUSDollar(V__AMOUNT,V__PERIOD)
   <=>
   (? [V__TIME] :
     (s__instance(V__TIME,V__PERIOD)
     &
     s__holdsDuring(V__TIME,'s__currencyExchangeRate(s__UnitedStatesDollar,V__AMOUNT)'))))
)

Economy.kif 3664-3669 ?PERIOD is a currency exchange perUS dollar of ?AMOUNT if and only if there exists ?TIME such that ?TIME is an instance of ?PERIOD and ?AMOUNT is a currency exchange rate of united states dollar holds during ?TIME
( ! [V__UNIT,V__AMOUNT,V__PERIOD] :
   (s__currencyExchangeRateInPeriod(V__UNIT,V__AMOUNT,V__PERIOD)
   <=>
   (? [V__TIME] :
     (s__instance(V__TIME,V__PERIOD)
     &
     s__holdsDuring(V__TIME,'s__currencyExchangeRate(V__UNIT,V__AMOUNT)'))))
)

Economy.kif 3671-3676 ?UNIT currency exchange rate in period ?AMOUNT for ?PERIOD if and only if there exists ?TIME such that ?TIME is an instance of ?PERIOD and ?AMOUNT is a currency exchange rate of ?UNIT holds during ?TIME
( ! [V__AGENT1,V__AGENT2] :
   (s__customer(V__AGENT1,V__AGENT2)
   <=>
   (? [V__SERVICE] :
     (s__instance(V__SERVICE,s__FinancialTransaction) &
       s__agent(V__SERVICE,V__AGENT2)
     &
     s__destination(V__SERVICE,V__AGENT1))))
)

Mid-level-ontology.kif 7426-7432 ?AGENT2 is a customer of ?AGENT1 if and only if there exists ?SERVICE such that ?SERVICE is an instance of financial transaction and ?AGENT2 is an agent of ?SERVICE and ?SERVICE ends up at ?AGENT1
( ! [V__Person1,V__Person2,V__Org] :
   (s__customerRepresentative(V__Person1,V__Person2,V__Org)
   <=>
   (? [V__Service] :
     (s__instance(V__Service,s__FinancialTransaction) &
       s__employs(V__Org,V__Person1)
     &
     s__agent(V__Service,V__Person1)
   &
   s__destination(V__Service,V__Person2))))
)

FinancialOntology.kif 3527-3534 ?Person1 customer representative ?Person2 for ?Org if and only if there exists ?Service such that ?Service is an instance of financial transaction and ?Org employs ?Person1 and ?Person1 is an agent of ?Service and ?Service ends up at ?Person2
( ! [V__COUNTRY,V__AMOUNT,V__PERIOD] :
   (s__economicAidDonatedInPeriod(V__COUNTRY,V__AMOUNT,V__PERIOD)
   <=>
   (? [V__TIME] :
     (s__instance(V__TIME,V__PERIOD)
     &
     s__holdsDuring(V__TIME,'s__economicAidDonated(V__COUNTRY,V__AMOUNT)'))))
)

Economy.kif 2822-2827 ?COUNTRY economic aid donated in period ?AMOUNT for ?PERIOD if and only if there exists ?TIME such that ?TIME is an instance of ?PERIOD and ?AMOUNT is an economic aid donated of ?COUNTRY holds during ?TIME
( ! [V__COUNTRY,V__AMOUNT,V__PERIOD] :
   (s__economicAidReceivedNetInPeriod(V__COUNTRY,V__AMOUNT,V__PERIOD)
   <=>
   (? [V__TIME] :
     (s__instance(V__TIME,V__PERIOD)
     &
     s__holdsDuring(V__TIME,'s__economicAidReceivedNet(V__COUNTRY,V__AMOUNT)'))))
)

Economy.kif 2862-2867 ?COUNTRY economic aid received net in period ?AMOUNT for ?PERIOD if and only if there exists ?TIME such that ?TIME is an instance of ?PERIOD and ?AMOUNT is an economic aid received net of ?COUNTRY holds during ?TIME
( ! [V__AREA,V__SOURCE,V__FRACTION,V__PERIOD] :
   (s__electricityFractionFromSourceInPeriod(V__AREA,V__SOURCE,V__FRACTION,V__PERIOD)
   <=>
   (? [V__TIME] :
     (s__instance(V__TIME,V__PERIOD)
     &
     s__holdsDuring(V__TIME,'s__electricityFractionFromSource(V__AREA,V__SOURCE,V__FRACTION)'))))
)

Economy.kif 2060-2065 ?AREA electricity fraction from source in period ?SOURCE for ?FRACTION with ?PERIOD if and only if there exists ?TIME such that ?TIME is an instance of ?PERIOD and ?AREA electricity fraction from source ?SOURCE for ?FRACTION holds during ?TIME

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


s__containsInformation('(! [V__AGENT,V__VOTER,V__ELECTION,V__VOTING] : ((s__instance(V__ELECTION,s__ElectionFn(V__AGENT)) & s__instance(V__VOTING,s__VotingFn(V__ELECTION)) & s__agent(V__VOTING,V__VOTER)) => s__attribute(V__VOTER,s__Male)))',s__ExclusiveMaleSuffrage)

Government.kif 1202-1209 For all ?AGENT, ?VOTER,, , ?ELECTION and ?VOTING contains information exclusive male suffrage
s__containsInformation('(! [V__COUNTRY,V__ELECTION,V__VOTING,V__VOTER] : ((s__instance(V__COUNTRY,s__Nation) & s__instance(V__ELECTION,s__ElectionFn(V__COUNTRY)) & s__instance(V__VOTING,s__VotingFn(V__ELECTION)) & s__agent(V__VOTING,V__VOTER)) => s__citizen(V__VOTER,V__COUNTRY)))',s__VoterCitizenshipRequirement)

Government.kif 916-924 For all ?COUNTRY, ?ELECTION,, , ?VOTING and ?VOTER contains information voter citizenship requirement
s__containsInformation('(! [V__POLITY,V__AGENT,V__ELECTION,V__VOTINGAGE,V__AGE] : ((s__citizen(V__AGENT,V__POLITY) & s__suffrageAgeMinimum(V__POLITY,V__VOTINGAGE) & s__age(V__AGENT,V__AGE) & greatereq(V__AGE,V__VOTINGAGE) & s__instance(V__ELECTION,s__ElectionFn(V__POLITY))) => s__capability(s__VotingFn(V__ELECTION),s__agent__m,V__AGENT)))',s__UniversalSuffrageLaw)

Government.kif 1069-1078 For all ?POLITY, ?AGENT,, , ?ELECTION,, , ?VOTINGAGE and ?AGE contains information universal suffrage law
s__containsInformation('(! [V__POLITY,V__VOTER,V__ELECTION,V__VOTINGAGE,V__AGE] : ((s__citizen(V__VOTER,V__POLITY) & s__suffrageAgeMinimum(V__POLITY,V__VOTINGAGE) & s__age(V__VOTER,V__AGE) & greatereq(V__AGE,V__VOTINGAGE) & s__instance(V__ELECTION,s__ElectionFn(V__POLITY))) => (? [V__VOTING] : (s__instance(V__VOTING,s__VotingFn(V__ELECTION)) & s__agent(V__VOTING,V__VOTER)))))',s__CompulsorySuffrageLaw)

Government.kif 1129-1141 For all ?POLITY, ?VOTER,, , ?ELECTION,, , ?VOTINGAGE and ?AGE
  • if ?VOTER is a citizen of ?POLITY and ?VOTINGAGE is a suffrage age minimum of ?POLITY and the age of ?VOTER is ?AGE and ?AGE is greater than or equal to ?VOTINGAGE and ?ELECTION is an instance of the election of ?POLITY,
  • then there exists ?VOTING such that ?VOTING is an instance of the voting of ?ELECTION and ?VOTER is an agent of ?VOTING
contains information compulsory suffrage law
( ! [V__AGENT,V__SYMPTOM,V__SUBSTANCE,V__PROCESS,V__SAMPLE,V__THERAPY,V__ORGANISM] :
   s__decreasesLikelihood('(s__biochemicalAgentSyndrome(V__AGENT,V__SYMPTOM) & s__biochemicalAgentAntidote(V__AGENT,V__SUBSTANCE,V__PROCESS) & s__instance(V__SAMPLE,V__SUBSTANCE) & s__instance(V__THERAPY,V__PROCESS) & s__experiencer(V__THERAPY,V__ORGANISM) & s__patient(V__THERAPY,V__SUBSTANCE))','s__attribute(V__ORGANISM,V__SYMPTOM)')
)

WMD.kif 870-878 ?SYMPTOM is a biochemical agent syndrome of ?AGENT and ?AGENT biochemical agent antidote ?SUBSTANCE for ?PROCESS and ?SAMPLE is an instance of ?SUBSTANCE and ?THERAPY is an instance of ?PROCESS and ?ORGANISM experiences ?THERAPY and ?SUBSTANCE is a patient of ?THERAPY decreases likelihood of ?SYMPTOM is an attribute of ?ORGANISM
( ! [V__AREA,V__PERSON,V__MILITARYAGE,V__AGE] :
   (s__AvailableForMilitaryServiceMaleFn(V__AREA)
   = s__CardinalityFn(s__KappaFn(V__PERSON,'(s__instance(V__PERSON,s__Human) & s__attribute(V__PERSON,s__Male) & s__militaryAge(V__AREA,V__MILITARYAGE) & s__age(V__PERSON,V__AGE) & greatereq(V__AGE,V__MILITARYAGE) & s__inhabits(V__PERSON,V__AREA))')))
)

Military.kif 867-876 The available for military service male of ?AREA is equal to the number of instances in the class described by ?PERSON
( ! [V__AREA,V__YEAR,V__INFANT,V__BIRTH,V__WOMAN] :
   (s__ChildrenBornPerWomanFn(V__AREA,s__YearFn(V__YEAR))
= s__CardinalityFn(s__KappaFn(V__INFANT,'(s__instance(V__BIRTH,s__Birth) & s__experiencer(V__BIRTH,V__INFANT) & s__agent(V__BIRTH,V__WOMAN) & s__instance(V__WOMAN,s__Human) & s__attribute(V__WOMAN,s__Female) & s__holdsDuring(s__YearFn(V__YEAR),s__inhabits(V__WOMAN,V__AREA)))')))
)

People.kif 462-472 The children born per woman of ?AREA and the year ?YEAR is equal to the number of instances in the class described by ?INFANT
( ! [V__AREA,V__PERSON,V__PROCESS,V__MILITARYAGE,V__AGE] :
   (s__FitForMilitaryServiceMaleFn(V__AREA)
   = s__CardinalityFn(s__KappaFn(V__PERSON,'(s__instance(V__PERSON,s__Human) & s__attribute(V__PERSON,s__Male) & s__instance(V__PROCESS,s__MilitaryProcess) & s__fitForMilitaryService(V__PERSON,V__PROCESS) & s__militaryAge(V__AREA,V__MILITARYAGE) & s__age(V__PERSON,V__AGE) & greatereq(V__AGE,V__MILITARYAGE) & s__inhabits(V__PERSON,V__AREA))')))
)

Military.kif 890-901 The fit for military service male of ?AREA is equal to the number of instances in the class described by ?PERSON
( ! [V__AREA,V__PERSON] :
   (s__PopulationFn(V__AREA)
   = s__CardinalityFn(s__KappaFn(V__PERSON,'(s__instance(V__PERSON,s__Human) & s__inhabits(V__PERSON,V__AREA))')))
)

People.kif 49-54 The population of ?AREA is equal to the number of instances in the class described by ?PERSON
( ! [V__AREA,V__YEAR,V__PERSON,V__MILITARYAGE,V__AGEMINUSONE,V__AGE] :
   (s__ReachingMilitaryAgeAnnuallyMaleFn(V__AREA,V__YEAR)
   = s__CardinalityFn(s__KappaFn(V__PERSON,'(s__instance(V__PERSON,s__Human) & s__attribute(V__PERSON,s__Male) & s__militaryAge(V__AREA,V__MILITARYAGE) & (V__AGEMINUSONE = minus(V__AGE,1)) & s__holdsDuring(V__YEAR,(s__age(V__PERSON,V__AGEMINUSONE) | s__age(V__PERSON,V__AGE))) & (V__AGE = V__MILITARYAGE) & s__inhabits(V__PERSON,V__AREA))')))
)

Military.kif 928-941 The reaching military age annually male of ?AREA and ?YEAR is equal to the number of instances in the class described by ?PERSON
(? [V__THING] :
   s__instance(V__THING,s__Entity))

Merge.kif 849-850 There exists ?THING such that ?THING is an instance of entity
(? [V__TIME] :
   (s__instance(V__TIME,s__TimeInterval) &
     s__finishes(V__TIME,s__WhenFn(s__JesusOfNazareth))
   &
   s__starts(V__TIME,s__WhenFn(s__TwelveApostles))
&
(! [V__MEM] :
   (s__holdsDuring(V__TIME,'s__member(V__MEM,s__TwelveApostles)')
   =>
   s__holdsDuring(V__TIME,'s__friend(V__MEM,s__JesusOfNazareth)')))))

Media.kif 1972-1980 There exists ?TIME such that ?TIME is an instance of time interval and ?TIME finishes the time of existence of JesusOfNazareth and ?TIME starts the time of existence of TwelveApostles and for all ?MEM
s__holdsDuring(s__FutureFn(s__DayFn(3,s__MonthFn(s__June,s__YearFn(2006))))
,'s__instance(s__Montenegro,s__EuropeanNation)')

Media.kif 2507-2508 Montenegro is an instance of european nation holds during after the day 3
s__holdsDuring(s__FutureFn(s__DayFn(3,s__MonthFn(s__June,s__YearFn(2006))))
,'s__instance(s__Montenegro,s__IndependentState)')

Media.kif 2505-2506 Montenegro is an instance of independent state holds during after the day 3
s__holdsDuring(s__FutureFn(s__DayFn(3,s__MonthFn(s__June,s__YearFn(2006))))
,'(~ s__instance(s__SerbiaAndMontenegro,s__IndependentState))')

Media.kif 2519-2520 Serbia and montenegro is not an instance of independent state holds during after the day 3
s__holdsDuring(s__FutureFn(s__DayFn(5,s__MonthFn(s__June,s__YearFn(2006))))
,'s__instance(s__Serbia,s__EuropeanNation)')

Media.kif 2492-2493 Serbia is an instance of european nation holds during after the day 5
s__holdsDuring(s__FutureFn(s__DayFn(5,s__MonthFn(s__June,s__YearFn(2006))))
,'s__instance(s__Serbia,s__IndependentState)')

Media.kif 2490-2491 Serbia is an instance of independent state holds during after the day 5
( ! [V__AGENT,V__SYMPTOM,V__PROCESSTYPE,V__PROCESS,V__ORGANISM] :
   s__increasesLikelihood('(s__biochemicalAgentSyndrome(V__AGENT,V__SYMPTOM) & s__biochemicalAgentDelivery(V__AGENT,V__PROCESSTYPE) & s__instance(V__PROCESS,V__PROCESSTYPE) & s__experiencer(V__PROCESS,V__ORGANISM))','s__attribute(V__ORGANISM,V__SYMPTOM)')
)

WMD.kif 761-767 ?SYMPTOM is a biochemical agent syndrome of ?AGENT and ?PROCESSTYPE is a biochemical agent delivery of ?AGENT and ?PROCESS is an instance of ?PROCESSTYPE and ?ORGANISM experiences ?PROCESS increases likelihood of ?SYMPTOM is an attribute of ?ORGANISM
( ! [V__WINDOW] :
   (~ (s__hasGUEState(V__WINDOW,s__GUE_NonVisibleState) &
       s__hasGUEState(V__WINDOW,s__GUE_ActiveState) &
       s__instance(V__WINDOW,s__InterfaceWindow)))
   )

ComputerInput.kif 1634-1638 ~{ ?WINDOW has state GUE_NonVisibleState } or ~{ ?WINDOW has state GUE_ActiveState } or ~{ ?WINDOW is an instance of InterfaceWindow }
( ! [V__CURSOR] :
   (~ (s__instance(V__CURSOR,s__Cursor) &
       s__hasGUEState(V__CURSOR,s__GUE_SelectedState)))
   )

ComputerInput.kif 1811-1814 ~{ ?CURSOR is an instance of Cursor } or ~{ ?CURSOR has state GUE_SelectedState }
( ! [V__CURSOR] :
   (~ (s__instance(V__CURSOR,s__MouseCursor) &
       s__hasGUEState(V__CURSOR,s__GUE_ActiveState)))
   )

ComputerInput.kif 1579-1582 ~{ ?CURSOR is an instance of MouseCursor } or ~{ ?CURSOR has state GUE_ActiveState }
( ! [V__GRAPH,V__NUMBER1,V__NUMBER2] :
   (~ (? [V__PATH1,V__PATH2] :
       (s__instance(V__PATH1,s__CutSetFn(V__GRAPH))
     &
     s__instance(V__PATH2,s__MinimalCutSetFn(V__GRAPH))
&
s__pathLength(V__PATH1,V__NUMBER1)
&
s__pathLength(V__PATH2,V__NUMBER2)
&
less(V__NUMBER1,V__NUMBER2))))
)

Merge.kif 6197-6204 There don't exist ?PATH1 and ?PATH2 such that ?PATH1 is an instance of the set of paths that partition ?GRAPH into two separate graphs and ?PATH2 is an instance of the set of minimal paths that partition ?GRAPH into two separate graphs and the length of ?PATH1 is ?NUMBER1 and the length of ?PATH2 is ?NUMBER2 and ?NUMBER1 is less than ?NUMBER2

appearance as argument number 0
-------------------------


( ! [V__VIR,V__PARTTYPE] :
   s__instance(s__CellPartFn(V__VIR,V__PARTTYPE)
,V__PARTTYPE)
)

VirusProteinAndCellPart.kif 591-591 The cell part of an entity and a set or class is an instance of the set or class
( ! [V__VIR,V__PARTTYPE] :
   s__instance(s__ViralPartFn(V__VIR,V__PARTTYPE)
,V__PARTTYPE)
)

VirusProteinAndCellPart.kif 580-580 The viral part of an entity and a set or class is an instance of the set or class
s__instance(s__FinancialRating,s__SetOrClass)

s__instance(s__AAA_Rating,s__FinancialRating)

FinancialOntology.kif 2443-2443 AAA-rating is an instance of financial rating
s__instance(s__ABPFn__m,s__UnaryFunction)

s__instance(s__UnaryFunction,s__SetOrClass)

UXExperimentalTerms.kif 3428-3428 Average buying price is an instance of unary function
s__instance(s__ExperimentAttribute,s__SetOrClass)

s__instance(s__ABTest,s__ExperimentAttribute)

UXExperimentalTerms.kif 4613-4613 A/B test is an instance of experiment attribute
s__instance(s__CentralGreatAndamaneseLanguage,s__SetOrClass)

s__instance(s__APucikwarLanguage,s__CentralGreatAndamaneseLanguage)

Languages.kif 5379-5379 A pucikwar language is an instance of central great andamanese language
s__instance(s__ASEANRegionalForum,s__OrganizationOfNations)

s__instance(s__OrganizationOfNations,s__SetOrClass)

Government.kif 2811-2811 ASEAN regional forum is an instance of organization of nations
s__instance(s__ASPFn__m,s__UnaryFunction)

s__instance(s__UnaryFunction,s__SetOrClass)

UXExperimentalTerms.kif 3471-3471 Average buying price is an instance of unary function
s__instance(s__Archipelago,s__SetOrClass)

s__instance(s__AalandIslands,s__Archipelago)

Media.kif 2530-2530 AalandIslands is an instance of archipelago
s__instance(s__AalandIslands,s__DependencyOrSpecialSovereigntyArea)

s__instance(s__DependencyOrSpecialSovereigntyArea,s__SetOrClass)

Media.kif 2531-2531 AalandIslands is an instance of dependency or special sovereignty area
s__instance(s__UnclassifiedSpokenLanguage,s__SetOrClass)

s__instance(s__AariyaLanguage,s__UnclassifiedSpokenLanguage)

Languages.kif 3771-3771 Aariya language is an instance of unclassified spoken language
s__instance(s__ReligiousPosition,s__SetOrClass)

s__instance(s__Abbot,s__ReligiousPosition)

People.kif 1211-1211 Abbot is an instance of religious position
s__instance(s__AbinomnLanguage,s__SpokenHumanLanguage)

s__instance(s__SpokenHumanLanguage,s__SetOrClass)

Languages.kif 2923-2923 Abinomn language is an instance of spoken human language
s__instance(s__AbishiraLanguage,s__UnclassifiedSpokenLanguage)

s__instance(s__UnclassifiedSpokenLanguage,s__SetOrClass)

Languages.kif 3777-3777 Abishira language is an instance of unclassified spoken language
s__instance(s__NorthCaucasianLanguage,s__SetOrClass)

s__instance(s__AbkhazLanguage,s__NorthCaucasianLanguage)

Languages.kif 14541-14541 AbkhazLanguage is an instance of north caucasian language
s__instance(s__AbortedFn__m,s__BinaryFunction)

s__instance(s__BinaryFunction,s__SetOrClass)

MilitaryProcesses.kif 2377-2377 Aborted is an instance of binary function
s__instance(s__AbortedLaunchFn__m,s__BinaryFunction)

s__instance(s__BinaryFunction,s__SetOrClass)

MilitaryProcesses.kif 2443-2443 Aborted launch is an instance of binary function
s__instance(s__AbortedMissionFn__m,s__BinaryFunction)

s__instance(s__BinaryFunction,s__SetOrClass)

MilitaryProcesses.kif 2397-2397 Aborted mission is an instance of binary function
s__instance(s__Above,s__AntiSymmetricPositionalAttribute)

s__instance(s__AntiSymmetricPositionalAttribute,s__SetOrClass)

Merge.kif 17275-17275 Above is an instance of AntiSymmetricPositionalAttribute
s__instance(s__Above,s__PositionalAttribute)

s__instance(s__PositionalAttribute,s__SetOrClass)

Merge.kif 17274-17274 Above is an instance of positional attribute
s__instance(s__AbsoluteValueFn__m,s__TotalValuedRelation)

s__instance(s__TotalValuedRelation,s__SetOrClass)

Merge.kif 4886-4886 Absolute value is an instance of total valued relation
s__instance(s__AbsoluteValueFn__m,s__UnaryFunction)

s__instance(s__UnaryFunction,s__SetOrClass)

Merge.kif 4885-4885 Absolute value is an instance of unary function
s__instance(s__AbunLanguage,s__NorthBirdsHeadLanguage)

s__instance(s__NorthBirdsHeadLanguage,s__SetOrClass)

Languages.kif 13704-13704 Abun language is an instance of north birds head language
s__instance(s__MusicGenre,s__SetOrClass)

s__instance(s__Acapella,s__MusicGenre)

Music.kif 537-537 Acapella is an instance of music genre
s__instance(s__SubtiabaTlapanecLanguage,s__SetOrClass)

s__instance(s__AcatepecTlapanecoLanguage,s__SubtiabaTlapanecLanguage)

Languages.kif 13142-13142 Acatepec tlapaneco language is an instance of subtiaba tlapanec language

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


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