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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - inList
inList

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


s__documentation(s__inList__m,s__ChineseLanguage,'这是类似 Listelementinstance。 (inList ?OBJ ?LIST) 的意思是 ?OBJ 是在 ?LIST List 里。例如: (inList Tuesday (ListFn Monday Tuesday Wednesday)) 是真的')

Merge.kif 3313-3315
s__documentation(s__inList__m,s__EnglishLanguage,'The analog of element and instance for Lists. (inList ?OBJ ?LIST) means that ?OBJ is in the List ?LIST. For example, (inList Tuesday (ListFn Monday Tuesday Wednesday)) would be true.')

Merge.kif 3310-3312
s__domain(s__inList__m,1,s__Entity)

Merge.kif 3308-3308 The number 1 argument of in list is an instance of entity
s__domain(s__inList__m,2,s__List)

Merge.kif 3309-3309 The number 2 argument of in list is an instance of list
s__instance(s__inList__m,s__AsymmetricRelation)

s__instance(s__AsymmetricRelation,s__SetOrClass)

Merge.kif 3306-3306 in list is an instance of asymmetric relation
s__instance(s__inList__m,s__BinaryPredicate)

s__instance(s__BinaryPredicate,s__SetOrClass)

Merge.kif 3304-3304 in list is an instance of binary predicate
s__instance(s__IrreflexiveRelation,s__SetOrClass)

s__instance(s__inList__m,s__IrreflexiveRelation)

Merge.kif 3305-3305 in list is an instance of irreflexive relation
s__instance(s__inList__m,s__PartialValuedRelation)

s__instance(s__PartialValuedRelation,s__SetOrClass)

Merge.kif 3307-3307 in list is an instance of partial valued relation

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


s__format(s__ChineseLanguage,s__inList__m,'%1 %n 是 %2 的 member')

chinese_format.kif 131-131
s__format(s__EnglishLanguage,s__inList__m,'%1 is %n a member of %2')

english_format.kif 92-92
s__subrelation(s__albumTrack__m,s__inList__m)

Music.kif 335-335 album track is a subrelation of in list
s__termFormat(s__ChineseLanguage,s__inList__m,'在列表内')

chinese_format.kif 132-132 "在列表内" is the printable form of in list in ChineseLanguage
s__termFormat(s__EnglishLanguage,s__inList__m,'in list')

domainEnglishFormat.kif 5449-5449 "in list" is the printable form of in list in english language

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


( ! [V__ITEM,V__RESULTS] :
   ((s__inList(V__ITEM,V__RESULTS)
    s__and__ms__instance(V__RESULTS,s__SRPResults))
  s__=>(s__exists__m[V__SRP] :
     (s__instance(V__SRP,s__SearchResultsPage)s__and__ms__component(V__RESULTS,V__SRP))))
)

UXExperimentalTerms.kif 2698-2705
( ! [V__ITEM,V__RESULTS] :
   ((s__inList(V__ITEM,V__RESULTS)
    s__and__ms__instance(V__RESULTS,s__SRPResults))
  s__=>(s__instance(V__ITEM,s__WebListing)s__or__ms__instance(V__ITEM,s__WebPage)))
)

UXExperimentalTerms.kif 2690-2696
( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__CognitiveAgent)s__and__ms__instance(V__ROW2,s__Formula))
    s__=>((s__instance(s__desires__m,s__IntentionalRelation)s__and__ms__desires(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__CognitiveAgent)s__and__ms__instance(V__ROW2,s__Object))
    s__=>((s__instance(s__dislikes__m,s__IntentionalRelation)s__and__ms__dislikes(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   (s__instance(V__AGENT,s__CognitiveAgent)s__=>((s__instance(s__inScopeOfInterest__m,s__IntentionalRelation)s__and__ms__inScopeOfInterest(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__CognitiveAgent)s__and__ms__instance(V__ROW2,s__Formula))
    s__=>((s__instance(s__believes__m,s__IntentionalRelation)s__and__ms__believes(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__CognitiveAgent)s__and__ms__instance(V__ROW2,s__Formula))
    s__=>((s__instance(s__knows__m,s__IntentionalRelation)s__and__ms__knows(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__Human)s__and__ms__instance(V__ROW2,s__Human))
    s__=>((s__instance(s__cohabitant__m,s__IntentionalRelation)s__and__ms__cohabitant(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__ServiceProcess)s__and__ms__instance(V__AGENT,s__CognitiveAgent)s__and__ms__instance(V__ROW2,s__CognitiveAgent))
    s__=>((s__instance(s__serviceRecipient__m,s__IntentionalRelation)s__and__ms__serviceRecipient(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__CognitiveAgent)s__and__ms__instance(V__ROW2,s__Formula))
    s__=>((s__instance(s__doubts__m,s__IntentionalRelation)s__and__ms__doubts(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__Human)s__and__ms__instance(V__ROW2,s__Human))
    s__=>((s__instance(s__friend__m,s__IntentionalRelation)s__and__ms__friend(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW3,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__CognitiveAgent)s__and__ms__instance(V__ROW3,s__Formula)s__and__ms__instance(V__ROW2,s__Formula))
    s__=>((s__instance(s__prefers__m,s__IntentionalRelation)s__and__ms__prefers(V__AGENT,V__ROW2,V__ROW3)
      s__and__ms__inList(V__OBJ,s__ListFn__2Fn(V__ROW2,V__ROW3)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__CognitiveAgent)s__and__ms__instance(V__ROW2,s__Formula))
    s__=>((s__instance(s__disapproves__m,s__IntentionalRelation)s__and__ms__disapproves(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__Human)s__and__ms__instance(V__ROW2,s__Human))
    s__=>((s__instance(s__domesticPartner__m,s__IntentionalRelation)s__and__ms__domesticPartner(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__CognitiveAgent)s__and__ms__instance(V__ROW2,s__Agent))
    s__=>((s__instance(s__enemy__m,s__IntentionalRelation)s__and__ms__enemy(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__ServiceProcess)s__and__ms__instance(V__AGENT,s__CognitiveAgent)s__and__ms__instance(V__ROW2,s__CognitiveAgent))
    s__=>((s__instance(s__serviceProvider__m,s__IntentionalRelation)s__and__ms__serviceProvider(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__CognitiveAgent)s__and__ms__instance(V__ROW2,s__Formula))
    s__=>((s__instance(s__considers__m,s__IntentionalRelation)s__and__ms__considers(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__CognitiveAgent)s__and__ms__instance(V__ROW2,s__Physical))
    s__=>((s__instance(s__needs__m,s__IntentionalRelation)s__and__ms__needs(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

( ! [V__AGENT,V__ROW2,V__OBJ] :
   ((s__instance(V__AGENT,s__CognitiveAgent)s__and__ms__instance(V__ROW2,s__Physical))
    s__=>((s__instance(s__wants__m,s__IntentionalRelation)s__and__ms__wants(V__AGENT,V__ROW2)
      s__and__ms__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
s__=>s__inScopeOfInterest(V__AGENT,V__OBJ)))
)

Merge.kif 2859-2864
( ! [V__ROW7,V__ROW5,V__OBJ1,V__ROW6,V__OBJ2,V__ROW3,V__ROW4,V__ROW2,V__ATTR1,V__ATTR2] :
   ((s__instance(V__ROW7,s__Attribute)s__and__ms__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__OBJ1,s__Object)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__OBJ2,s__Object)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__instance(V__ATTR1,s__PositionalAttribute)s__and__ms__instance(V__ATTR2,s__PositionalAttribute))
    s__=>((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
      s__and__ms__contraryAttribute__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__and__ms__inList(V__ATTR1,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
s__and__ms__inList(V__ATTR2,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
s__and__m(s__not__m(V__ATTR1s__equal__mV__ATTR2)))
s__=>(s__not__ms__orientation(V__OBJ1,V__OBJ2,V__ATTR2))))
)

( ! [V__OBJ1,V__OBJ2,V__ROW3,V__ROW4,V__ROW2,V__ATTR1,V__ATTR2] :
   ((s__instance(V__OBJ1,s__Object)s__and__ms__instance(V__OBJ2,s__Object)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__instance(V__ATTR1,s__PositionalAttribute)s__and__ms__instance(V__ATTR2,s__PositionalAttribute))
    s__=>((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
      s__and__ms__contraryAttribute__3(V__ROW2,V__ROW3,V__ROW4)
    s__and__ms__inList(V__ATTR1,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
s__and__ms__inList(V__ATTR2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
s__and__m(s__not__m(V__ATTR1s__equal__mV__ATTR2)))
s__=>(s__not__ms__orientation(V__OBJ1,V__OBJ2,V__ATTR2))))
)

( ! [V__ROW5,V__OBJ1,V__ROW6,V__OBJ2,V__ROW3,V__ROW4,V__ROW2,V__ATTR1,V__ATTR2] :
   ((s__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__OBJ1,s__Object)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__OBJ2,s__Object)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__instance(V__ATTR1,s__PositionalAttribute)s__and__ms__instance(V__ATTR2,s__PositionalAttribute))
    s__=>((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
      s__and__ms__contraryAttribute__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    s__and__ms__inList(V__ATTR1,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
s__and__ms__inList(V__ATTR2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
s__and__m(s__not__m(V__ATTR1s__equal__mV__ATTR2)))
s__=>(s__not__ms__orientation(V__OBJ1,V__OBJ2,V__ATTR2))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__OBJ1,V__ROW6,V__OBJ2,V__ROW3,V__ROW4,V__ROW2,V__ATTR1,V__ATTR2] :
   ((s__instance(V__ROW7,s__Attribute)s__and__ms__instance(V__ROW8,s__Attribute)s__and__ms__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__OBJ1,s__Object)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__OBJ2,s__Object)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__instance(V__ATTR1,s__PositionalAttribute)s__and__ms__instance(V__ATTR2,s__PositionalAttribute))
    s__=>((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
      s__and__ms__contraryAttribute__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
    s__and__ms__inList(V__ATTR1,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
s__and__ms__inList(V__ATTR2,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
s__and__m(s__not__m(V__ATTR1s__equal__mV__ATTR2)))
s__=>(s__not__ms__orientation(V__OBJ1,V__OBJ2,V__ATTR2))))
)

( ! [V__ROW5,V__OBJ1,V__OBJ2,V__ROW3,V__ROW4,V__ROW2,V__ATTR1,V__ATTR2] :
   ((s__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__OBJ1,s__Object)s__and__ms__instance(V__OBJ2,s__Object)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__instance(V__ATTR1,s__PositionalAttribute)s__and__ms__instance(V__ATTR2,s__PositionalAttribute))
    s__=>((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
      s__and__ms__contraryAttribute__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__and__ms__inList(V__ATTR1,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
s__and__ms__inList(V__ATTR2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
s__and__m(s__not__m(V__ATTR1s__equal__mV__ATTR2)))
s__=>(s__not__ms__orientation(V__OBJ1,V__OBJ2,V__ATTR2))))
)

( ! [V__OBJ1,V__OBJ2,V__ROW2,V__ATTR1,V__ATTR2] :
   ((s__instance(V__OBJ1,s__Object)s__and__ms__instance(V__OBJ2,s__Object)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__instance(V__ATTR1,s__PositionalAttribute)s__and__ms__instance(V__ATTR2,s__PositionalAttribute))
    s__=>((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
      s__and__ms__contraryAttribute__1(V__ROW2)
    s__and__ms__inList(V__ATTR1,s__ListFn__1Fn(V__ROW2))
s__and__ms__inList(V__ATTR2,s__ListFn__1Fn(V__ROW2))
s__and__m(s__not__m(V__ATTR1s__equal__mV__ATTR2)))
s__=>(s__not__ms__orientation(V__OBJ1,V__OBJ2,V__ATTR2))))
)

( ! [V__OBJ1,V__OBJ2,V__ROW3,V__ROW2,V__ATTR1,V__ATTR2] :
   ((s__instance(V__OBJ1,s__Object)s__and__ms__instance(V__OBJ2,s__Object)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__instance(V__ATTR1,s__PositionalAttribute)s__and__ms__instance(V__ATTR2,s__PositionalAttribute))
    s__=>((s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
      s__and__ms__contraryAttribute__2(V__ROW2,V__ROW3)
    s__and__ms__inList(V__ATTR1,s__ListFn__2Fn(V__ROW2,V__ROW3))
s__and__ms__inList(V__ATTR2,s__ListFn__2Fn(V__ROW2,V__ROW3))
s__and__m(s__not__m(V__ATTR1s__equal__mV__ATTR2)))
s__=>(s__not__ms__orientation(V__OBJ1,V__OBJ2,V__ATTR2))))
)

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

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

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

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

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

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

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

QoSontology.kif 690-698
( ! [V__ACESSING,V__USER,V__ACCESSING,V__LIST] :
   ((s__instance(V__ACESSING,s__Process)s__and__ms__instance(V__USER,s__Agent)s__and__ms__instance(V__ACCESSING,s__Process)s__and__ms__instance(V__LIST,s__List))
    s__=>((s__viewedItemList(V__USER,V__LIST)
      s__and__ms__inList(V__ACCESSING,V__LIST))
  s__=>(s__instance(V__ACCESSING,s__AccessingWebPage)s__and__ms__agent(V__ACESSING,V__USER)
  s__and__m(s__exists__m[V__DEST] :
   (s__instance(V__DEST,s__WebPage)s__and__ms__destination(V__ACCESSING,s__WebPage))))))
)

UXExperimentalTerms.kif 961-971
( ! [V__LIST,V__ITEM] :
   (s__instance(V__LIST,s__List)s__=>(s__inList(V__ITEM,V__LIST)
    s__=>(s__exists__m[V__NUMBER] :
       (s__instance(V__NUMBER,s__PositiveInteger)s__and__m(s__ListOrderFn(V__LIST,V__NUMBER)
      s__equal__mV__ITEM)))))
)

Merge.kif 3317-3320

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


( ! [V__LASTPLACE,V__LIST1,V__AVERAGE] :
   ((s__instance(V__LASTPLACE,s__PositiveInteger)s__and__ms__instance(V__LIST1,s__List)s__and__ms__instance(V__AVERAGE,s__RealNumber))
    s__=>(s__average(V__LIST1,V__AVERAGE)
    s__<=>
    (s__exists__m[V__LIST2] :
       (s__instance(V__LIST2,s__List)s__and__m((s__ListLengthFn(V__LIST2)
        s__equal__ms__ListLengthFn(V__LIST1))
    s__and__m(s__ListOrderFn(V__LIST2,1)
  s__equal__ms__ListOrderFn(V__LIST1,1))
s__and__m(s__forall__m[V__ITEMFROM2] :
(s__instance(V__ITEMFROM2,s__PositiveInteger)s__=>(s__inList(V__ITEMFROM2,V__LIST2)
s__=>(s__exists__m[V__POSITION,V__POSITIONMINUSONE,V__ITEMFROM1,V__PRIORFROM2] :
   (s__instance(V__POSITION,s__Quantity)s__and__ms__instance(V__POSITIONMINUSONE,s__Quantity)s__and__ms__instance(V__ITEMFROM1,s__PositiveInteger)s__and__ms__instance(V__PRIORFROM2,s__PositiveInteger)s__and__m(s__greaterThan(V__POSITION,1)
  s__and__ms__lessThanOrEqualTo(V__POSITION,s__ListLengthFn(V__LIST2))
s__and__m(s__ListOrderFn(V__LIST2,V__ITEMFROM2)
s__equal__mV__POSITION)s__and__ms__inList(V__ITEMFROM1,V__LIST1)
s__and__m(V__POSITIONs__equal__ms__ListOrderFn(V__LIST1,V__ITEMFROM1))
s__and__ms__inList(V__PRIORFROM2,V__LIST2)
s__and__m(V__POSITIONMINUSONEs__equal__ms__SubtractionFn(V__POSITION,1))
s__and__m(V__POSITIONMINUSONEs__equal__ms__ListOrderFn(V__LIST2,V__PRIORFROM2))
s__and__m(V__ITEMFROM2s__equal__ms__AdditionFn(V__ITEMFROM1,V__PRIORFROM2))))))))
s__and__m(V__LASTPLACEs__equal__ms__ListLengthFn(V__LIST2))
s__and__m(V__AVERAGEs__equal__ms__DivisionFn(s__ListOrderFn(V__LIST2,V__LASTPLACE)
,V__LASTPLACE)))))))
)

People.kif 285-306 A real number is an average of a list if and only if there exists another list such that length of the other list is equal to length of the list and 1th element of the other list is equal to 1th element of the list and for all a positive integer and a fourth positive integer is equal to length of the other list and the real number is equal to the fourth positive integerth element of the other list and the fourth positive integer
No TPTP formula. May not be expressible in strict first order. People.kif 411-442 The female life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order. People.kif 323-353 The life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order. People.kif 367-398 The male life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
( ! [V__P,V__A] :
   ((s__instance(V__P,s__CognitiveAgent)s__and__ms__instance(V__A,s__Album))
    s__=>(s__albumArtist(V__A,V__P)
    s__=>(s__exists__m[V__R,V__M] :
       (s__instance(V__M,s__Process)s__and__m(s__instance(V__R,s__Recording)s__and__ms__inList(V__R,V__A)
      s__and__ms__record(V__R,V__M)
    s__and__ms__agent(V__M,V__P))))))
)

Music.kif 274-281
( ! [V__A,V__D,V__DS,V__X] :
   ((s__instance(V__A,s__Album)s__and__ms__subclass(V__D,s__DataStorageDevice)s__and__ms__instance(V__D,s__DataStorageDevice)s__and__ms__instance(V__D,s__SetOrClass)s__and__ms__subclass(V__DS,s__DataStorageDevice))
    s__=>(((V__Ds__equal__ms__AlbumCopiesFn(V__A,V__DS))
      s__and__ms__instance(V__X,V__D))
  s__=>(s__forall__m[V__S] :
     (s__instance(V__S,s__Object)s__=>(s__inList(V__S,V__A)
      s__=>(s__exists__m[V__C] :
         (s__instance(V__C,s__ContentBearingObject)s__and__m(s__copy(V__C,V__S)
        s__and__ms__stored(V__C,V__D)))))))))
)

Music.kif 936-946
( ! [V__A,V__M,V__ATTR] :
   ((s__instance(V__A,s__Album)s__and__ms__instance(V__M,s__List))
    s__=>((s__instance(V__ATTR,s__RecordingAttribute)s__and__ms__albumType(V__A,V__ATTR))
    s__=>(s__forall__m[V__R] :
       (s__instance(V__R,s__Object)s__=>(s__inList(V__R,V__M)
        s__=>s__attribute(V__R,V__A))))))
)

Music.kif 291-298
( ! [V__OBJ,V__PART,V__NUM] :
   ((s__instance(V__OBJ,s__DigitalDataStorageDevice)s__and__ms__part(V__PART,V__OBJ)
    s__and__ms__instance(V__PART,s__DigitalData))
  s__=>(s__exists__m[V__SCHEME,V__LIST] :
     (s__instance(V__SCHEME,s__CodeMap)s__and__ms__instance(V__LIST,s__List)s__and__m(s__codeMapping(V__SCHEME,V__PART,V__NUM)
    s__and__ms__represents(V__LIST,V__SCHEME)
  s__and__m(s__inList(V__NUM,V__LIST)
s__=>s__instance(V__NUM,s__BinaryNumber))))))
)

Media.kif 801-812
( ! [V__LIST,V__AVERAGE] :
   ((s__instance(V__LIST,s__List)s__and__ms__instance(V__AVERAGE,s__RealNumber))
    s__=>(s__average(V__LIST,V__AVERAGE)
    s__=>(s__forall__m[V__LISTITEM] :
       (s__inList(V__LISTITEM,V__LIST)
      s__=>s__instance(V__LISTITEM,s__RealNumber)))))
)

Merge.kif 5465-5470
( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Attribute)s__and__ms__instance(V__ROW8,s__Attribute)s__and__ms__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute))
    s__=>(s__contraryAttribute__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
    s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
  s__=>s__instance(V__ELEMENT,s__Attribute))))
)

( ! [V__ROW2,V__ELEMENT] :
   (s__instance(V__ROW2,s__Attribute)s__=>(s__contraryAttribute__1(V__ROW2)
    s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
  s__=>s__instance(V__ELEMENT,s__Attribute))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute))
    s__=>(s__contraryAttribute__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
  s__=>s__instance(V__ELEMENT,s__Attribute))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Attribute)s__and__ms__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute))
    s__=>(s__contraryAttribute__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
  s__=>s__instance(V__ELEMENT,s__Attribute))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute))
    s__=>(s__contraryAttribute__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
  s__=>s__instance(V__ELEMENT,s__Attribute))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute))
    s__=>(s__contraryAttribute__3(V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
  s__=>s__instance(V__ELEMENT,s__Attribute))))
)

( ! [V__ROW3,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute))
    s__=>(s__contraryAttribute__2(V__ROW2,V__ROW3)
    s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
  s__=>s__instance(V__ELEMENT,s__Attribute))))
)

Merge.kif 516-520
( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__disjointDecomposition__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    s__=>(s__forall__m[V__ITEM] :
       (s__instance(V__ITEM,s__SetOrClass)s__=>(s__inList(V__ITEM,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
      s__=>s__subclass(V__ITEM,V__CLASS))))))
)

( ! [V__ROW3,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__disjointDecomposition__3(V__CLASS,V__ROW2,V__ROW3)
    s__=>(s__forall__m[V__ITEM] :
       (s__instance(V__ITEM,s__SetOrClass)s__=>(s__inList(V__ITEM,s__ListFn__2Fn(V__ROW2,V__ROW3))
      s__=>s__subclass(V__ITEM,V__CLASS))))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__disjointDecomposition__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__forall__m[V__ITEM] :
       (s__instance(V__ITEM,s__SetOrClass)s__=>(s__inList(V__ITEM,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
      s__=>s__subclass(V__ITEM,V__CLASS))))))
)

( ! [V__ROW2,V__CLASS] :
   ((s__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__disjointDecomposition__2(V__CLASS,V__ROW2)
    s__=>(s__forall__m[V__ITEM] :
       (s__instance(V__ITEM,s__SetOrClass)s__=>(s__inList(V__ITEM,s__ListFn__1Fn(V__ROW2))
      s__=>s__subclass(V__ITEM,V__CLASS))))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__disjointDecomposition__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__forall__m[V__ITEM] :
       (s__instance(V__ITEM,s__SetOrClass)s__=>(s__inList(V__ITEM,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
      s__=>s__subclass(V__ITEM,V__CLASS))))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW7,s__Class)s__and__ms__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__disjointDecomposition__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__forall__m[V__ITEM] :
       (s__instance(V__ITEM,s__SetOrClass)s__=>(s__inList(V__ITEM,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
      s__=>s__subclass(V__ITEM,V__CLASS))))))
)

Merge.kif 3146-3151
( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class))
    s__=>(s__disjointDecomposition__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__forall__m[V__ITEM1,V__ITEM2] :
       ((s__instance(V__ITEM1,s__SetOrClass)s__and__ms__instance(V__ITEM2,s__SetOrClass))
        s__=>((s__inList(V__ITEM1,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
        s__and__ms__inList(V__ITEM2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
    s__and__m(s__not__m(V__ITEM1s__equal__mV__ITEM2)))
s__=>s__disjoint(V__ITEM1,V__ITEM2))))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW7,s__Class)s__and__ms__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class))
    s__=>(s__disjointDecomposition__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__forall__m[V__ITEM1,V__ITEM2] :
       ((s__instance(V__ITEM1,s__SetOrClass)s__and__ms__instance(V__ITEM2,s__SetOrClass))
        s__=>((s__inList(V__ITEM1,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
        s__and__ms__inList(V__ITEM2,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
    s__and__m(s__not__m(V__ITEM1s__equal__mV__ITEM2)))
s__=>s__disjoint(V__ITEM1,V__ITEM2))))))
)

( ! [V__ROW2,V__CLASS] :
   ((s__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class))
    s__=>(s__disjointDecomposition__2(V__CLASS,V__ROW2)
    s__=>(s__forall__m[V__ITEM1,V__ITEM2] :
       ((s__instance(V__ITEM1,s__SetOrClass)s__and__ms__instance(V__ITEM2,s__SetOrClass))
        s__=>((s__inList(V__ITEM1,s__ListFn__1Fn(V__ROW2))
        s__and__ms__inList(V__ITEM2,s__ListFn__1Fn(V__ROW2))
    s__and__m(s__not__m(V__ITEM1s__equal__mV__ITEM2)))
s__=>s__disjoint(V__ITEM1,V__ITEM2))))))
)

( ! [V__ROW3,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class))
    s__=>(s__disjointDecomposition__3(V__CLASS,V__ROW2,V__ROW3)
    s__=>(s__forall__m[V__ITEM1,V__ITEM2] :
       ((s__instance(V__ITEM1,s__SetOrClass)s__and__ms__instance(V__ITEM2,s__SetOrClass))
        s__=>((s__inList(V__ITEM1,s__ListFn__2Fn(V__ROW2,V__ROW3))
        s__and__ms__inList(V__ITEM2,s__ListFn__2Fn(V__ROW2,V__ROW3))
    s__and__m(s__not__m(V__ITEM1s__equal__mV__ITEM2)))
s__=>s__disjoint(V__ITEM1,V__ITEM2))))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class))
    s__=>(s__disjointDecomposition__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    s__=>(s__forall__m[V__ITEM1,V__ITEM2] :
       ((s__instance(V__ITEM1,s__SetOrClass)s__and__ms__instance(V__ITEM2,s__SetOrClass))
        s__=>((s__inList(V__ITEM1,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
        s__and__ms__inList(V__ITEM2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
    s__and__m(s__not__m(V__ITEM1s__equal__mV__ITEM2)))
s__=>s__disjoint(V__ITEM1,V__ITEM2))))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class))
    s__=>(s__disjointDecomposition__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__forall__m[V__ITEM1,V__ITEM2] :
       ((s__instance(V__ITEM1,s__SetOrClass)s__and__ms__instance(V__ITEM2,s__SetOrClass))
        s__=>((s__inList(V__ITEM1,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
        s__and__ms__inList(V__ITEM2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
    s__and__m(s__not__m(V__ITEM1s__equal__mV__ITEM2)))
s__=>s__disjoint(V__ITEM1,V__ITEM2))))))
)

Merge.kif 3153-3162
( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__disjointDecomposition__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__disjointDecomposition__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Class)s__and__ms__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__disjointDecomposition__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__disjointDecomposition__3(V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW3,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__disjointDecomposition__2(V__ROW2,V__ROW3)
    s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Class)s__and__ms__instance(V__ROW8,s__Class)s__and__ms__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__disjointDecomposition__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
    s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW2,V__ELEMENT] :
   (s__instance(V__ROW2,s__Class)s__=>(s__disjointDecomposition__1(V__ROW2)
    s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

Merge.kif 628-632
( ! [V__ROW3,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__2Fn(V__ROW2,V__ROW3)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__1Fn(V__ROW2)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW8,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

Merge.kif 5016-5021
( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
        s__=>(s__RemainderFn(V__ELEMENT,V__NUMBER)
        s__equal__m0))))))
)

( ! [V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__1Fn(V__ROW2)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
        s__=>(s__RemainderFn(V__ELEMENT,V__NUMBER)
        s__equal__m0))))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
        s__=>(s__RemainderFn(V__ELEMENT,V__NUMBER)
        s__equal__m0))))))
)

( ! [V__ROW3,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__2Fn(V__ROW2,V__ROW3)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
        s__=>(s__RemainderFn(V__ELEMENT,V__NUMBER)
        s__equal__m0))))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW8,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
        s__=>(s__RemainderFn(V__ELEMENT,V__NUMBER)
        s__equal__m0))))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
        s__=>(s__RemainderFn(V__ELEMENT,V__NUMBER)
        s__equal__m0))))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
        s__=>(s__RemainderFn(V__ELEMENT,V__NUMBER)
        s__equal__m0))))))
)

Merge.kif 5023-5028
( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__GREATER] :
         (s__instance(V__GREATER,s__Integer)s__and__m(s__greaterThan(V__GREATER,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
        s__=>(s__RemainderFn(V__ELEMENT,V__GREATER)
        s__equal__m0))))))))))
)

( ! [V__ROW3,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__2Fn(V__ROW2,V__ROW3)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__GREATER] :
         (s__instance(V__GREATER,s__Integer)s__and__m(s__greaterThan(V__GREATER,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
        s__=>(s__RemainderFn(V__ELEMENT,V__GREATER)
        s__equal__m0))))))))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__GREATER] :
         (s__instance(V__GREATER,s__Integer)s__and__m(s__greaterThan(V__GREATER,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
        s__=>(s__RemainderFn(V__ELEMENT,V__GREATER)
        s__equal__m0))))))))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__GREATER] :
         (s__instance(V__GREATER,s__Integer)s__and__m(s__greaterThan(V__GREATER,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
        s__=>(s__RemainderFn(V__ELEMENT,V__GREATER)
        s__equal__m0))))))))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW8,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__GREATER] :
         (s__instance(V__GREATER,s__Integer)s__and__m(s__greaterThan(V__GREATER,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
        s__=>(s__RemainderFn(V__ELEMENT,V__GREATER)
        s__equal__m0))))))))))
)

( ! [V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__1Fn(V__ROW2)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__GREATER] :
         (s__instance(V__GREATER,s__Integer)s__and__m(s__greaterThan(V__GREATER,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
        s__=>(s__RemainderFn(V__ELEMENT,V__GREATER)
        s__equal__m0))))))))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__GreatestCommonDivisorFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__GREATER] :
         (s__instance(V__GREATER,s__Integer)s__and__m(s__greaterThan(V__GREATER,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
        s__=>(s__RemainderFn(V__ELEMENT,V__GREATER)
        s__equal__m0))))))))))
)

Merge.kif 5030-5038
( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW8,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW3,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__2Fn(V__ROW2,V__ROW3)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

( ! [V__ROW2,V__NUMBER,V__ELEMENT] :
   ((s__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__1Fn(V__ROW2)
      s__equal__mV__NUMBER)s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
    s__=>s__instance(V__ELEMENT,s__Number))))
)

Merge.kif 5095-5100
( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
        s__=>(s__RemainderFn(V__NUMBER,V__ELEMENT)
        s__equal__m0))))))
)

( ! [V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__1Fn(V__ROW2)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
        s__=>(s__RemainderFn(V__NUMBER,V__ELEMENT)
        s__equal__m0))))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
        s__=>(s__RemainderFn(V__NUMBER,V__ELEMENT)
        s__equal__m0))))))
)

( ! [V__ROW3,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__2Fn(V__ROW2,V__ROW3)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
        s__=>(s__RemainderFn(V__NUMBER,V__ELEMENT)
        s__equal__m0))))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW8,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
        s__=>(s__RemainderFn(V__NUMBER,V__ELEMENT)
        s__equal__m0))))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
        s__=>(s__RemainderFn(V__NUMBER,V__ELEMENT)
        s__equal__m0))))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
      s__equal__mV__NUMBER)s__=>(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
        s__=>(s__RemainderFn(V__NUMBER,V__ELEMENT)
        s__equal__m0))))))
)

Merge.kif 5102-5107
( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__LESS] :
         (s__instance(V__LESS,s__Integer)s__and__m(s__lessThan(V__LESS,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
        s__=>(s__RemainderFn(V__LESS,V__ELEMENT)
        s__equal__m0))))))))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__LESS] :
         (s__instance(V__LESS,s__Integer)s__and__m(s__lessThan(V__LESS,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
        s__=>(s__RemainderFn(V__LESS,V__ELEMENT)
        s__equal__m0))))))))))
)

( ! [V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__1Fn(V__ROW2)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__LESS] :
         (s__instance(V__LESS,s__Integer)s__and__m(s__lessThan(V__LESS,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
        s__=>(s__RemainderFn(V__LESS,V__ELEMENT)
        s__equal__m0))))))))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW8,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__LESS] :
         (s__instance(V__LESS,s__Integer)s__and__m(s__lessThan(V__LESS,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
        s__=>(s__RemainderFn(V__LESS,V__ELEMENT)
        s__equal__m0))))))))))
)

( ! [V__ROW3,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__2Fn(V__ROW2,V__ROW3)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__LESS] :
         (s__instance(V__LESS,s__Integer)s__and__m(s__lessThan(V__LESS,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
        s__=>(s__RemainderFn(V__LESS,V__ELEMENT)
        s__equal__m0))))))))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer)s__and__ms__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW6,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__LESS] :
         (s__instance(V__LESS,s__Integer)s__and__m(s__lessThan(V__LESS,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
        s__=>(s__RemainderFn(V__LESS,V__ELEMENT)
        s__equal__m0))))))))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer)s__and__ms__instance(V__ROW3,s__Integer)s__and__ms__instance(V__ROW4,s__Integer)s__and__ms__instance(V__ROW2,s__Integer)s__and__ms__instance(V__NUMBER,s__Integer))
    s__=>((s__LeastCommonMultipleFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
      s__equal__mV__NUMBER)s__=>(s__not__m(s__exists__m[V__LESS] :
         (s__instance(V__LESS,s__Integer)s__and__m(s__lessThan(V__LESS,V__NUMBER)
        s__and__m(s__forall__m[V__ELEMENT] :
         (s__instance(V__ELEMENT,s__Integer)s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
        s__=>(s__RemainderFn(V__LESS,V__ELEMENT)
        s__equal__m0))))))))))
)

Merge.kif 5109-5117
( ! [V__ROW3,V__ROW2,V__CLASS,V__ATTR] :
   ((s__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute))
    s__=>(s__exhaustiveAttribute__3(V__CLASS,V__ROW2,V__ROW3)
    s__=>(s__inList(V__ATTR,s__ListFn__2Fn(V__ROW2,V__ROW3))
  s__=>s__instance(V__ATTR,s__Attribute))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS,V__ATTR] :
   ((s__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute))
    s__=>(s__exhaustiveAttribute__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__inList(V__ATTR,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
  s__=>s__instance(V__ATTR,s__Attribute))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS,V__ATTR] :
   ((s__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute))
    s__=>(s__exhaustiveAttribute__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__inList(V__ATTR,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
  s__=>s__instance(V__ATTR,s__Attribute))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS,V__ATTR] :
   ((s__instance(V__ROW7,s__Attribute)s__and__ms__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute))
    s__=>(s__exhaustiveAttribute__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__inList(V__ATTR,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
  s__=>s__instance(V__ATTR,s__Attribute))))
)

( ! [V__ROW2,V__CLASS,V__ATTR] :
   ((s__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute))
    s__=>(s__exhaustiveAttribute__2(V__CLASS,V__ROW2)
    s__=>(s__inList(V__ATTR,s__ListFn__1Fn(V__ROW2))
  s__=>s__instance(V__ATTR,s__Attribute))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS,V__ATTR] :
   ((s__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute))
    s__=>(s__exhaustiveAttribute__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    s__=>(s__inList(V__ATTR,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
  s__=>s__instance(V__ATTR,s__Attribute))))
)

Merge.kif 554-558
( ! [V__ROW3,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveAttribute__3(V__CLASS,V__ROW2,V__ROW3)
    s__=>(s__forall__m[V__ATTR1] :
       (s__instance(V__ATTR1,V__CLASS)
      s__=>(s__exists__m[V__ATTR2] :
         (s__inList(V__ATTR2,s__ListFn__2Fn(V__ROW2,V__ROW3))
      s__and__m(V__ATTR1s__equal__mV__ATTR2)))))))
)

( ! [V__ROW2,V__CLASS] :
   ((s__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveAttribute__2(V__CLASS,V__ROW2)
    s__=>(s__forall__m[V__ATTR1] :
       (s__instance(V__ATTR1,V__CLASS)
      s__=>(s__exists__m[V__ATTR2] :
         (s__inList(V__ATTR2,s__ListFn__1Fn(V__ROW2))
      s__and__m(V__ATTR1s__equal__mV__ATTR2)))))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveAttribute__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__forall__m[V__ATTR1] :
       (s__instance(V__ATTR1,V__CLASS)
      s__=>(s__exists__m[V__ATTR2] :
         (s__inList(V__ATTR2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
      s__and__m(V__ATTR1s__equal__mV__ATTR2)))))))
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveAttribute__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    s__=>(s__forall__m[V__ATTR1] :
       (s__instance(V__ATTR1,V__CLASS)
      s__=>(s__exists__m[V__ATTR2] :
         (s__inList(V__ATTR2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
      s__and__m(V__ATTR1s__equal__mV__ATTR2)))))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveAttribute__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__forall__m[V__ATTR1] :
       (s__instance(V__ATTR1,V__CLASS)
      s__=>(s__exists__m[V__ATTR2] :
         (s__inList(V__ATTR2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
      s__and__m(V__ATTR1s__equal__mV__ATTR2)))))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW7,s__Attribute)s__and__ms__instance(V__ROW5,s__Attribute)s__and__ms__instance(V__ROW6,s__Attribute)s__and__ms__instance(V__ROW3,s__Attribute)s__and__ms__instance(V__ROW4,s__Attribute)s__and__ms__instance(V__ROW2,s__Attribute)s__and__ms__subclass(V__CLASS,s__Attribute)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveAttribute__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__forall__m[V__ATTR1] :
       (s__instance(V__ATTR1,V__CLASS)
      s__=>(s__exists__m[V__ATTR2] :
         (s__inList(V__ATTR2,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
      s__and__m(V__ATTR1s__equal__mV__ATTR2)))))))
)

Merge.kif 560-568
( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveDecomposition__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    s__=>(s__forall__m[V__OBJ] :
       (s__instance(V__OBJ,V__CLASS)
      s__=>(s__exists__m[V__ITEM] :
         (s__instance(V__ITEM,s__SetOrClass)s__and__m(s__inList(V__ITEM,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
      s__and__ms__instance(V__OBJ,V__ITEM))))))))
)

( ! [V__ROW2,V__CLASS] :
   ((s__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveDecomposition__2(V__CLASS,V__ROW2)
    s__=>(s__forall__m[V__OBJ] :
       (s__instance(V__OBJ,V__CLASS)
      s__=>(s__exists__m[V__ITEM] :
         (s__instance(V__ITEM,s__SetOrClass)s__and__m(s__inList(V__ITEM,s__ListFn__1Fn(V__ROW2))
      s__and__ms__instance(V__OBJ,V__ITEM))))))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW7,s__Class)s__and__ms__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveDecomposition__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__forall__m[V__OBJ] :
       (s__instance(V__OBJ,V__CLASS)
      s__=>(s__exists__m[V__ITEM] :
         (s__instance(V__ITEM,s__SetOrClass)s__and__m(s__inList(V__ITEM,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
      s__and__ms__instance(V__OBJ,V__ITEM))))))))
)

( ! [V__ROW3,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveDecomposition__3(V__CLASS,V__ROW2,V__ROW3)
    s__=>(s__forall__m[V__OBJ] :
       (s__instance(V__OBJ,V__CLASS)
      s__=>(s__exists__m[V__ITEM] :
         (s__instance(V__ITEM,s__SetOrClass)s__and__m(s__inList(V__ITEM,s__ListFn__2Fn(V__ROW2,V__ROW3))
      s__and__ms__instance(V__OBJ,V__ITEM))))))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveDecomposition__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__forall__m[V__OBJ] :
       (s__instance(V__OBJ,V__CLASS)
      s__=>(s__exists__m[V__ITEM] :
         (s__instance(V__ITEM,s__SetOrClass)s__and__m(s__inList(V__ITEM,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
      s__and__ms__instance(V__OBJ,V__ITEM))))))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class)s__and__ms__instance(V__CLASS,s__Class)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>(s__exhaustiveDecomposition__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__forall__m[V__OBJ] :
       (s__instance(V__OBJ,V__CLASS)
      s__=>(s__exists__m[V__ITEM] :
         (s__instance(V__ITEM,s__SetOrClass)s__and__m(s__inList(V__ITEM,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
      s__and__ms__instance(V__OBJ,V__ITEM))))))))
)

Merge.kif 3136-3144
( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__exhaustiveDecomposition__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
    s__=>(s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW2,V__ELEMENT] :
   (s__instance(V__ROW2,s__Class)s__=>(s__exhaustiveDecomposition__1(V__ROW2)
    s__=>(s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Class)s__and__ms__instance(V__ROW8,s__Class)s__and__ms__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__exhaustiveDecomposition__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
    s__=>(s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW7,s__Class)s__and__ms__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW6,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__exhaustiveDecomposition__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
    s__=>(s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW3,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__exhaustiveDecomposition__2(V__ROW2,V__ROW3)
    s__=>(s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW5,s__Class)s__and__ms__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__exhaustiveDecomposition__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
    s__=>(s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__ELEMENT] :
   ((s__instance(V__ROW3,s__Class)s__and__ms__instance(V__ROW4,s__Class)s__and__ms__instance(V__ROW2,s__Class))
    s__=>(s__exhaustiveDecomposition__3(V__ROW2,V__ROW3,V__ROW4)
    s__=>(s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
  s__=>s__instance(V__ELEMENT,s__Class))))
)

Merge.kif 611-615
( ! [V__L] :
   (s__instance(V__L,s__Album)s__=>(s__forall__m[V__X] :
       (s__inList(V__X,V__L)
      s__=>s__instance(V__X,s__Recording))))
)

Music.kif 53-58
( ! [V__SVC] :
   (s__instance(V__SVC,s__ShuttleService)s__=>(s__exists__m[V__LIST,V__VEHICLE,V__AGENT] :
       (s__instance(V__AGENT,s__Agent)s__and__m(s__agent(V__SVC,V__AGENT)
      s__and__ms__possesses(V__AGENT,V__VEHICLE)
    s__and__ms__instance(V__VEHICLE,s__Automobile)s__and__ms__instance(V__LIST,s__List)s__and__m(s__forall__m[V__X] :
     (s__inList(V__X,V__LIST)
    s__=>(s__instance(V__X,s__PostalPlace)s__and__m(s__exists__m[V__TRANSPORT] :
       (s__instance(V__TRANSPORT,s__Transportation)s__and__ms__agent(V__TRANSPORT,V__AGENT)
      s__and__ms__instrument(V__TRANSPORT,V__VEHICLE)
    s__and__ms__destination(V__TRANSPORT,V__X))))))))))
)

Hotel.kif 1979-1997

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