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)) 是真的"')

chinese_format.kif 1973-1975
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 2997-2999
s__domain(s__inList__m,n__1,s__Entity)

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

Merge.kif 2995-2995 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 2992-2992 in list is an instance of asymmetric relation
s__instance(s__inList__m,s__BinaryPredicate)

s__instance(s__BinaryPredicate,s__SetOrClass)

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

s__instance(s__inList__m,s__IrreflexiveRelation)

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

s__instance(s__PartialValuedRelation,s__SetOrClass)

Merge.kif 2993-2993 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 132-132
s__subrelation(s__albumTrack__m,s__inList__m)

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

domainEnglishFormat.kif 30091-30091
s__termFormat(s__ChineseLanguage,s__inList__m,'"在列表内"')

chinese_format.kif 132-132
s__termFormat(s__ChineseTraditionalLanguage,s__inList__m,'"在列表中"')

domainEnglishFormat.kif 30090-30090
s__termFormat(s__EnglishLanguage,s__inList__m,'"in list"')

domainEnglishFormat.kif 30089-30089

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


( ! [V__ROW5,V__ROW3,V__ATTR,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Attribute) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     (s__exhaustiveAttribute__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
     &
     s__inList(V__ATTR,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)))
=>
s__instance(V__ATTR,V__CLASS)
)
)

( ! [V__ATTR,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     (s__exhaustiveAttribute__2(V__CLASS,V__ROW2)
     &
     s__inList(V__ATTR,s__ListFn__1Fn(V__ROW2)))
=>
s__instance(V__ATTR,V__CLASS)
)
)

( ! [V__ROW3,V__ATTR,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     (s__exhaustiveAttribute__3(V__CLASS,V__ROW2,V__ROW3)
     &
     s__inList(V__ATTR,s__ListFn__2Fn(V__ROW2,V__ROW3)))
=>
s__instance(V__ATTR,V__CLASS)
)
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ATTR,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW7,s__Attribute) &
       s__instance(V__ROW5,s__Attribute) &
       s__instance(V__ROW6,s__Attribute) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     (s__exhaustiveAttribute__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
     &
     s__inList(V__ATTR,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)))
=>
s__instance(V__ATTR,V__CLASS)
)
)

( ! [V__ROW3,V__ATTR,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     (s__exhaustiveAttribute__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
     &
     s__inList(V__ATTR,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)))
=>
s__instance(V__ATTR,V__CLASS)
)
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ATTR,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW7,s__Attribute) &
       s__instance(V__ROW8,s__Attribute) &
       s__instance(V__ROW5,s__Attribute) &
       s__instance(V__ROW6,s__Attribute) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     (s__exhaustiveAttribute__8(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
     &
     s__inList(V__ATTR,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)))
=>
s__instance(V__ATTR,V__CLASS)
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ATTR,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Attribute) &
       s__instance(V__ROW6,s__Attribute) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     (s__exhaustiveAttribute__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
     &
     s__inList(V__ATTR,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)))
=>
s__instance(V__ATTR,V__CLASS)
)
)

Merge.kif 504-508
( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ATTR,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW7,s__Attribute) &
       s__instance(V__ROW8,s__Attribute) &
       s__instance(V__ROW5,s__Attribute) &
       s__instance(V__ROW6,s__Attribute) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute))
     =>
     (s__exhaustiveAttribute__8(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
     &
     s__inList(V__ATTR,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)))
=>
s__instance(V__ATTR,s__Attribute) )
)

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

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

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

( ! [V__ROW3,V__ATTR,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute))
     =>
     (s__exhaustiveAttribute__3(V__CLASS,V__ROW2,V__ROW3)
     &
     s__inList(V__ATTR,s__ListFn__2Fn(V__ROW2,V__ROW3)))
=>
s__instance(V__ATTR,s__Attribute) )
)

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

( ! [V__ROW3,V__ATTR,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute))
     =>
     (s__exhaustiveAttribute__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
     &
     s__inList(V__ATTR,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)))
=>
s__instance(V__ATTR,s__Attribute) )
)

Merge.kif 498-502
( ! [V__RESULTS,V__ITEM] :
   ((s__inList(V__ITEM,V__RESULTS)
     &
     s__instance(V__RESULTS,s__SRPResults))
   =>
   ( ? [V__SRP] :
     ((s__instance(V__SRP,s__SearchResultsPage) &
         s__component(V__RESULTS,V__SRP))))
)
)

UXExperimentalTerms.kif 2696-2703
( ! [V__RESULTS,V__ITEM] :
   ((s__inList(V__ITEM,V__RESULTS)
     &
     s__instance(V__RESULTS,s__SRPResults))
   =>
   (s__instance(V__ITEM,s__WebListing) |
     s__instance(V__ITEM,s__WebPage))
   )
)

UXExperimentalTerms.kif 2688-2694
( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) &
       s__instance(V__ROW2,s__Agent))
     =>
     (s__instance(s__enemy__m,s__IntentionalRelation) &
       s__enemy(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) &
       s__instance(V__ROW2,s__Formula))
     =>
     (s__instance(s__believes__m,s__IntentionalRelation) &
       s__believes(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) &
       s__instance(V__ROW2,s__Formula))
     =>
     (s__instance(s__doubts__m,s__IntentionalRelation) &
       s__doubts(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW3,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) &
       s__instance(V__ROW3,s__Formula) &
       s__instance(V__ROW2,s__Formula))
     =>
     (s__instance(s__prefers__m,s__IntentionalRelation) &
       s__prefers(V__AGENT,V__ROW2,V__ROW3)
     &
     s__inList(V__OBJ,s__ListFn__2Fn(V__ROW2,V__ROW3)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) &
       s__instance(V__ROW2,s__Physical))
     =>
     (s__instance(s__needs__m,s__IntentionalRelation) &
       s__needs(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) &
       s__instance(V__ROW2,s__Physical))
     =>
     (s__instance(s__wants__m,s__IntentionalRelation) &
       s__wants(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (s__instance(V__AGENT,s__CognitiveAgent) =>
     (s__instance(s__inScopeOfInterest__m,s__IntentionalRelation) &
       s__inScopeOfInterest(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) &
       s__instance(V__ROW2,s__Formula))
     =>
     (s__instance(s__disapproves__m,s__IntentionalRelation) &
       s__disapproves(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__Human) &
       s__instance(V__ROW2,s__Human))
     =>
     (s__instance(s__domesticPartner__m,s__IntentionalRelation) &
       s__domesticPartner(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   (s__instance(V__AGENT,s__CognitiveAgent) =>
     (s__instance(s__lacks__m,s__IntentionalRelation) &
       s__lacks(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__Human) &
       s__instance(V__ROW2,s__Human))
     =>
     (s__instance(s__friend__m,s__IntentionalRelation) &
       s__friend(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) &
       s__instance(V__ROW2,s__Formula))
     =>
     (s__instance(s__desires__m,s__IntentionalRelation) &
       s__desires(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) &
       s__instance(V__ROW2,s__Formula))
     =>
     (s__instance(s__considers__m,s__IntentionalRelation) &
       s__considers(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__Human) &
       s__instance(V__ROW2,s__Human))
     =>
     (s__instance(s__cohabitant__m,s__IntentionalRelation) &
       s__cohabitant(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__ServiceProcess) &
       s__instance(V__AGENT,s__CognitiveAgent) &
       s__instance(V__ROW2,s__CognitiveAgent))
     =>
     (s__instance(s__serviceProvider__m,s__IntentionalRelation) &
       s__serviceProvider(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__ServiceProcess) &
       s__instance(V__AGENT,s__CognitiveAgent) &
       s__instance(V__ROW2,s__CognitiveAgent))
     =>
     (s__instance(s__serviceRecipient__m,s__IntentionalRelation) &
       s__serviceRecipient(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) &
       s__instance(V__ROW2,s__Object))
     =>
     (s__instance(s__dislikes__m,s__IntentionalRelation) &
       s__dislikes(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) &
       s__instance(V__ROW2,s__Formula))
     =>
     (s__instance(s__knows__m,s__IntentionalRelation) &
       s__knows(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) &
       s__instance(V__ROW2,s__CognitiveAgent))
     =>
     (s__instance(s__approves__m,s__IntentionalRelation) &
       s__approves(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

( ! [V__AGENT,V__OBJ,V__ROW2] :
   ((s__instance(V__AGENT,s__CognitiveAgent) &
       s__subclass(V__ROW2,s__IntentionalProcess))
     =>
     (s__instance(s__enjoys__m,s__IntentionalRelation) &
       s__enjoys(V__AGENT,V__ROW2)
     &
     s__inList(V__OBJ,s__ListFn__1Fn(V__ROW2)))
=>
s__inScopeOfInterest(V__AGENT,V__OBJ)
)
)

Merge.kif 2578-2583
( ! [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__instance(V__ROW5,s__Attribute) &
       s__instance(V__OBJ1,s__Object) &
       s__instance(V__ROW6,s__Attribute) &
       s__instance(V__OBJ2,s__Object) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__instance(V__ATTR1,s__PositionalAttribute) &
       s__instance(V__ATTR2,s__PositionalAttribute))
     =>
     (s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
     &
     s__contraryAttribute__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
   &
   s__inList(V__ATTR1,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
&
s__inList(V__ATTR2,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
&
~((V__ATTR1 = V__ATTR2)))
=>
~(s__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__instance(V__OBJ1,s__Object) &
       s__instance(V__OBJ2,s__Object) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__instance(V__ATTR1,s__PositionalAttribute) &
       s__instance(V__ATTR2,s__PositionalAttribute))
     =>
     (s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
     &
     s__contraryAttribute__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
   &
   s__inList(V__ATTR1,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
&
s__inList(V__ATTR2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
&
~((V__ATTR1 = V__ATTR2)))
=>
~(s__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__instance(V__OBJ2,s__Object) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__instance(V__ATTR1,s__PositionalAttribute) &
       s__instance(V__ATTR2,s__PositionalAttribute))
     =>
     (s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
     &
     s__contraryAttribute__3(V__ROW2,V__ROW3,V__ROW4)
   &
   s__inList(V__ATTR1,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
&
s__inList(V__ATTR2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
&
~((V__ATTR1 = V__ATTR2)))
=>
~(s__orientation(V__OBJ1,V__OBJ2,V__ATTR2))
)
)

( ! [V__OBJ1,V__OBJ2,V__ROW2,V__ATTR1,V__ATTR2] :
   ((s__instance(V__OBJ1,s__Object) &
       s__instance(V__OBJ2,s__Object) &
       s__instance(V__ROW2,s__Attribute) &
       s__instance(V__ATTR1,s__PositionalAttribute) &
       s__instance(V__ATTR2,s__PositionalAttribute))
     =>
     (s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
     &
     s__contraryAttribute__1(V__ROW2)
   &
   s__inList(V__ATTR1,s__ListFn__1Fn(V__ROW2))
&
s__inList(V__ATTR2,s__ListFn__1Fn(V__ROW2))
&
~((V__ATTR1 = V__ATTR2)))
=>
~(s__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__instance(V__ROW8,s__Attribute) &
       s__instance(V__ROW5,s__Attribute) &
       s__instance(V__OBJ1,s__Object) &
       s__instance(V__ROW6,s__Attribute) &
       s__instance(V__OBJ2,s__Object) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__instance(V__ATTR1,s__PositionalAttribute) &
       s__instance(V__ATTR2,s__PositionalAttribute))
     =>
     (s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
     &
     s__contraryAttribute__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
   &
   s__inList(V__ATTR1,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
&
s__inList(V__ATTR2,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
&
~((V__ATTR1 = V__ATTR2)))
=>
~(s__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__instance(V__OBJ1,s__Object) &
       s__instance(V__ROW6,s__Attribute) &
       s__instance(V__OBJ2,s__Object) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__instance(V__ATTR1,s__PositionalAttribute) &
       s__instance(V__ATTR2,s__PositionalAttribute))
     =>
     (s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
     &
     s__contraryAttribute__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
   &
   s__inList(V__ATTR1,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
&
s__inList(V__ATTR2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
&
~((V__ATTR1 = V__ATTR2)))
=>
~(s__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__instance(V__OBJ2,s__Object) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__instance(V__ATTR1,s__PositionalAttribute) &
       s__instance(V__ATTR2,s__PositionalAttribute))
     =>
     (s__orientation(V__OBJ1,V__OBJ2,V__ATTR1)
     &
     s__contraryAttribute__2(V__ROW2,V__ROW3)
   &
   s__inList(V__ATTR1,s__ListFn__2Fn(V__ROW2,V__ROW3))
&
s__inList(V__ATTR2,s__ListFn__2Fn(V__ROW2,V__ROW3))
&
~((V__ATTR1 = V__ATTR2)))
=>
~(s__orientation(V__OBJ1,V__OBJ2,V__ATTR2))
)
)

Merge.kif 15715-15723
( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   ((s__instance(V__Process1,s__Physical) &
       s__instance(V__Process2,s__Physical) &
       s__instance(V__Number1,s__PositiveInteger) &
       s__instance(V__Number2,s__PositiveInteger))
     =>
     (s__processList__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
     &
     s__inList(V__Process1,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
&
s__inList(V__Process2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
&
(s__ListOrderFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))
)
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   ((s__instance(V__Process1,s__Physical) &
       s__instance(V__Process2,s__Physical) &
       s__instance(V__Number1,s__PositiveInteger) &
       s__instance(V__Number2,s__PositiveInteger))
     =>
     (s__processList__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
     &
     s__inList(V__Process1,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
&
s__inList(V__Process2,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
&
(s__ListOrderFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))
)
)

( ! [V__ROW3,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   ((s__instance(V__Process1,s__Physical) &
       s__instance(V__Process2,s__Physical) &
       s__instance(V__Number1,s__PositiveInteger) &
       s__instance(V__Number2,s__PositiveInteger))
     =>
     (s__processList__2(V__ROW2,V__ROW3)
     &
     s__inList(V__Process1,s__ListFn__2Fn(V__ROW2,V__ROW3))
&
s__inList(V__Process2,s__ListFn__2Fn(V__ROW2,V__ROW3))
&
(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   ((s__instance(V__Process1,s__Physical) &
       s__instance(V__Process2,s__Physical) &
       s__instance(V__Number1,s__PositiveInteger) &
       s__instance(V__Number2,s__PositiveInteger))
     =>
     (s__processList__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
     &
     s__inList(V__Process1,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
&
s__inList(V__Process2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
&
(s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))
)
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   ((s__instance(V__Process1,s__Physical) &
       s__instance(V__Process2,s__Physical) &
       s__instance(V__Number1,s__PositiveInteger) &
       s__instance(V__Number2,s__PositiveInteger))
     =>
     (s__processList__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
     &
     s__inList(V__Process1,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
&
s__inList(V__Process2,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
&
(s__ListOrderFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))
)
)

( ! [V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   ((s__instance(V__Process1,s__Physical) &
       s__instance(V__Process2,s__Physical) &
       s__instance(V__Number1,s__PositiveInteger) &
       s__instance(V__Number2,s__PositiveInteger))
     =>
     (s__processList__1(V__ROW2)
     &
     s__inList(V__Process1,s__ListFn__1Fn(V__ROW2))
&
s__inList(V__Process2,s__ListFn__1Fn(V__ROW2))
&
(s__ListOrderFn(s__ListFn__1Fn(V__ROW2)
,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__1Fn(V__ROW2)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))
)
)

( ! [V__ROW3,V__ROW4,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   ((s__instance(V__Process1,s__Physical) &
       s__instance(V__Process2,s__Physical) &
       s__instance(V__Number1,s__PositiveInteger) &
       s__instance(V__Number2,s__PositiveInteger))
     =>
     (s__processList__3(V__ROW2,V__ROW3,V__ROW4)
     &
     s__inList(V__Process1,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
&
s__inList(V__Process2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
&
(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))
)
)

QoSontology.kif 692-708
( ! [V__USER,V__ACCESSING,V__LIST] :
   ((s__instance(V__USER,s__Agent) &
       s__instance(V__ACCESSING,s__Process) &
       s__instance(V__LIST,s__List))
     =>
     (s__viewedItemList(V__USER,V__LIST)
     &
     s__inList(V__ACCESSING,V__LIST))
=>
(s__instance(V__ACCESSING,s__AccessingWebPage) &
   s__agent(V__ACCESSING,V__USER)
&
( ? [V__DEST] :
   ((s__instance(V__DEST,s__WebPage) &
       s__destination(V__ACCESSING,s__WebPage)))))
)
)

UXExperimentalTerms.kif 957-967
( ! [V__LIST,V__ITEM] :
   (s__instance(V__LIST,s__List) =>
     s__inList(V__ITEM,V__LIST)
   =>
   ( ? [V__NUMBER] :
     ((s__instance(V__NUMBER,s__PositiveInteger) &
         (s__ListOrderFn(V__LIST,V__NUMBER)
         = V__ITEM))))
)
)

Merge.kif 3001-3004

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


( ! [V__LASTPLACE,V__LIST1,V__AVERAGE] :
   ((s__instance(V__LASTPLACE,s__PositiveInteger) &
       s__instance(V__LIST1,s__List) &
       s__instance(V__AVERAGE,s__RealNumber))
     =>
     (s__average(V__LIST1,V__AVERAGE)
     =>
     ( ? [V__LIST2] :
       ((s__instance(V__LIST2,s__List) &
           ((s__ListLengthFn(V__LIST2)
             = s__ListLengthFn(V__LIST1))
         &
         (s__ListOrderFn(V__LIST2,n__1)
         = s__ListOrderFn(V__LIST1,n__1))
     &
     ( ! [V__ITEMFROM2] :
       (s__instance(V__ITEMFROM2,s__PositiveInteger) =>
         s__inList(V__ITEMFROM2,V__LIST2)
       =>
       ( ? [V__POSITION, V__POSITIONMINUSONE, V__ITEMFROM1, V__PRIORFROM2] :
         ((s__instance(V__POSITION,s__Quantity) &
             s__instance(V__POSITIONMINUSONE,s__Quantity) &
             s__instance(V__ITEMFROM1,s__PositiveInteger) &
             s__instance(V__PRIORFROM2,s__PositiveInteger) &
             (s__greaterThan(V__POSITION,n__1)
             &
             s__lessThanOrEqualTo(V__POSITION,s__ListLengthFn(V__LIST2))
         &
         (s__ListOrderFn(V__LIST2,V__ITEMFROM2)
         = V__POSITION)
       &
       s__inList(V__ITEMFROM1,V__LIST1)
     &
     (V__POSITION = s__ListOrderFn(V__LIST1,V__ITEMFROM1))
   &
   s__inList(V__PRIORFROM2,V__LIST2)
&
(V__POSITIONMINUSONE = s__SubtractionFn(V__POSITION,n__1))
&
(V__POSITIONMINUSONE = s__ListOrderFn(V__LIST2,V__PRIORFROM2))
&
(V__ITEMFROM2 = s__AdditionFn(V__ITEMFROM1,V__PRIORFROM2))))))))
&
(V__LASTPLACE = s__ListLengthFn(V__LIST2))
&
(V__AVERAGE = s__DivisionFn(s__ListOrderFn(V__LIST2,V__LASTPLACE)
,V__LASTPLACE)))))))
&
(( ? [V__LIST2] :
((s__instance(V__LIST2,s__List) &
((s__ListLengthFn(V__LIST2)
= s__ListLengthFn(V__LIST1))
&
(s__ListOrderFn(V__LIST2,n__1)
= s__ListOrderFn(V__LIST1,n__1))
&
( ! [V__ITEMFROM2] :
(s__instance(V__ITEMFROM2,s__PositiveInteger) =>
s__inList(V__ITEMFROM2,V__LIST2)
=>
( ? [V__POSITION, V__POSITIONMINUSONE, V__ITEMFROM1, V__PRIORFROM2] :
((s__instance(V__POSITION,s__Quantity) &
s__instance(V__POSITIONMINUSONE,s__Quantity) &
s__instance(V__ITEMFROM1,s__PositiveInteger) &
s__instance(V__PRIORFROM2,s__PositiveInteger) &
(s__greaterThan(V__POSITION,n__1)
&
s__lessThanOrEqualTo(V__POSITION,s__ListLengthFn(V__LIST2))
&
(s__ListOrderFn(V__LIST2,V__ITEMFROM2)
= V__POSITION)
&
s__inList(V__ITEMFROM1,V__LIST1)
&
(V__POSITION = s__ListOrderFn(V__LIST1,V__ITEMFROM1))
&
s__inList(V__PRIORFROM2,V__LIST2)
&
(V__POSITIONMINUSONE = s__SubtractionFn(V__POSITION,n__1))
&
(V__POSITIONMINUSONE = s__ListOrderFn(V__LIST2,V__PRIORFROM2))
&
(V__ITEMFROM2 = s__AdditionFn(V__ITEMFROM1,V__PRIORFROM2))))))))
&
(V__LASTPLACE = s__ListLengthFn(V__LIST2))
&
(V__AVERAGE = s__DivisionFn(s__ListOrderFn(V__LIST2,V__LASTPLACE)
,V__LASTPLACE))))))
=>
s__average(V__LIST1,V__AVERAGE))
)
)

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__instance(V__A,s__Album))
     =>
     s__albumArtist(V__A,V__P)
   =>
   ( ? [V__R, V__M] :
     ((s__instance(V__M,s__Process) &
         (s__instance(V__R,s__Recording) &
           s__inList(V__R,V__A)
         &
         s__record(V__R,V__M)
       &
       s__agent(V__M,V__P)))))
)
)

Music.kif 277-284
( ! [V__A,V__D,V__X,V__DS] :
   ((s__instance(V__A,s__Album) &
       s__subclass(V__D,s__DataStorageDevice) &
       s__instance(V__D,s__DataStorageDevice) &
       s__instance(V__D,s__SetOrClass) &
       s__subclass(V__DS,s__DataStorageDevice))
     =>
     ((V__D = s__AlbumCopiesFn(V__A,V__DS))
     &
     s__instance(V__X,V__D))
=>
( ! [V__S] :
   (s__instance(V__S,s__Object) =>
     s__inList(V__S,V__A)
   =>
   ( ? [V__C] :
     ((s__instance(V__C,s__ContentBearingObject) &
         (s__copy(V__C,V__S)
         &
         s__stored(V__C,V__D)))))))
)
)

Music.kif 930-940
( ! [V__OBJ,V__NUM,V__PART] :
   ((s__instance(V__OBJ,s__DigitalDataStorageDevice) &
       s__part(V__PART,V__OBJ)
     &
     s__instance(V__PART,s__DigitalData))
   =>
   ( ? [V__SCHEME, V__LIST] :
     ((s__instance(V__SCHEME,s__CodeMap) &
         s__instance(V__LIST,s__List) &
         (s__codeMapping(V__SCHEME,V__PART,V__NUM)
         &
         s__represents(V__LIST,V__SCHEME)
       &
       s__inList(V__NUM,V__LIST)
     =>
     s__instance(V__NUM,s__BinaryNumber)))))
)
)

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

Merge.kif 5044-5049
( ! [V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   ((s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute))
     =>
     s__contraryAttribute__3(V__ROW2,V__ROW3,V__ROW4)
   =>
   s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
=>
s__instance(V__ELEMENT,s__Attribute) )
)

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

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

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

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

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   ((s__instance(V__ROW7,s__Attribute) &
       s__instance(V__ROW8,s__Attribute) &
       s__instance(V__ROW5,s__Attribute) &
       s__instance(V__ROW6,s__Attribute) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute))
     =>
     s__contraryAttribute__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
   =>
   s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
=>
s__instance(V__ELEMENT,s__Attribute) )
)

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

Merge.kif 463-467
( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Class) &
       s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW4,s__Class) &
       s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__disjointDecomposition__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
   =>
   ( ! [V__ITEM] :
     (s__instance(V__ITEM,s__SetOrClass) =>
       s__inList(V__ITEM,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
   =>
   s__subclass(V__ITEM,V__CLASS)))
)
)

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

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

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Class) &
       s__instance(V__ROW6,s__Class) &
       s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW4,s__Class) &
       s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__disjointDecomposition__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
   =>
   ( ! [V__ITEM] :
     (s__instance(V__ITEM,s__SetOrClass) =>
       s__inList(V__ITEM,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
   =>
   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__instance(V__ROW5,s__Class) &
       s__instance(V__ROW6,s__Class) &
       s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW4,s__Class) &
       s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__disjointDecomposition__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
   =>
   ( ! [V__ITEM] :
     (s__instance(V__ITEM,s__SetOrClass) =>
       s__inList(V__ITEM,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
   =>
   s__subclass(V__ITEM,V__CLASS)))
)
)

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

Merge.kif 2839-2844
( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Class) &
       s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW4,s__Class) &
       s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class))
     =>
     s__disjointDecomposition__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
   =>
   ( ! [V__ITEM1, V__ITEM2] :
     ((s__instance(V__ITEM1,s__SetOrClass) &
         s__instance(V__ITEM2,s__SetOrClass))
       =>
       (s__inList(V__ITEM1,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
     &
     s__inList(V__ITEM2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
&
~((V__ITEM1 = V__ITEM2)))
=>
s__disjoint(V__ITEM1,V__ITEM2)))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW4,s__Class) &
       s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class))
     =>
     s__disjointDecomposition__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
   =>
   ( ! [V__ITEM1, V__ITEM2] :
     ((s__instance(V__ITEM1,s__SetOrClass) &
         s__instance(V__ITEM2,s__SetOrClass))
       =>
       (s__inList(V__ITEM1,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
     &
     s__inList(V__ITEM2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
&
~((V__ITEM1 = V__ITEM2)))
=>
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__instance(V__ROW5,s__Class) &
       s__instance(V__ROW6,s__Class) &
       s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW4,s__Class) &
       s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class))
     =>
     s__disjointDecomposition__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
   =>
   ( ! [V__ITEM1, V__ITEM2] :
     ((s__instance(V__ITEM1,s__SetOrClass) &
         s__instance(V__ITEM2,s__SetOrClass))
       =>
       (s__inList(V__ITEM1,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
     &
     s__inList(V__ITEM2,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
&
~((V__ITEM1 = V__ITEM2)))
=>
s__disjoint(V__ITEM1,V__ITEM2)))
)
)

( ! [V__ROW2,V__CLASS] :
   ((s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class))
     =>
     s__disjointDecomposition__2(V__CLASS,V__ROW2)
   =>
   ( ! [V__ITEM1, V__ITEM2] :
     ((s__instance(V__ITEM1,s__SetOrClass) &
         s__instance(V__ITEM2,s__SetOrClass))
       =>
       (s__inList(V__ITEM1,s__ListFn__1Fn(V__ROW2))
     &
     s__inList(V__ITEM2,s__ListFn__1Fn(V__ROW2))
&
~((V__ITEM1 = V__ITEM2)))
=>
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__instance(V__ROW6,s__Class) &
       s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW4,s__Class) &
       s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class))
     =>
     s__disjointDecomposition__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
   =>
   ( ! [V__ITEM1, V__ITEM2] :
     ((s__instance(V__ITEM1,s__SetOrClass) &
         s__instance(V__ITEM2,s__SetOrClass))
       =>
       (s__inList(V__ITEM1,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
     &
     s__inList(V__ITEM2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
&
~((V__ITEM1 = V__ITEM2)))
=>
s__disjoint(V__ITEM1,V__ITEM2)))
)
)

( ! [V__ROW3,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class))
     =>
     s__disjointDecomposition__3(V__CLASS,V__ROW2,V__ROW3)
   =>
   ( ! [V__ITEM1, V__ITEM2] :
     ((s__instance(V__ITEM1,s__SetOrClass) &
         s__instance(V__ITEM2,s__SetOrClass))
       =>
       (s__inList(V__ITEM1,s__ListFn__2Fn(V__ROW2,V__ROW3))
     &
     s__inList(V__ITEM2,s__ListFn__2Fn(V__ROW2,V__ROW3))
&
~((V__ITEM1 = V__ITEM2)))
=>
s__disjoint(V__ITEM1,V__ITEM2)))
)
)

Merge.kif 2846-2855
( ! [V__ELEMENT,V__ROW3,V__ROW2] :
   ((s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW2,s__Class))
     =>
     s__disjointDecomposition__2(V__ROW2,V__ROW3)
   =>
   s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
=>
s__instance(V__ELEMENT,s__Class) )
)

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

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

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

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

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

( ! [V__ROW5,V__ROW6,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   ((s__instance(V__ROW5,s__Class) &
       s__instance(V__ROW6,s__Class) &
       s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW4,s__Class) &
       s__instance(V__ROW2,s__Class))
     =>
     s__disjointDecomposition__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
   =>
   s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
=>
s__instance(V__ELEMENT,s__Class) )
)

Merge.kif 574-578
( ! [V__ELEMENT,V__ROW3,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__2Fn(V__ROW2,V__ROW3)
     = V__NUMBER)
   =>
   s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
=>
s__instance(V__ELEMENT,s__Number) )
)

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

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

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

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

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

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

Merge.kif 4623-4628
( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW6,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
     = V__NUMBER)
   =>
   ( ! [V__ELEMENT] :
     (s__instance(V__ELEMENT,s__Integer) =>
       s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
   =>
   (s__RemainderFn(V__ELEMENT,V__NUMBER)
   = n__0)))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
     = V__NUMBER)
   =>
   ( ! [V__ELEMENT] :
     (s__instance(V__ELEMENT,s__Integer) =>
       s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
   =>
   (s__RemainderFn(V__ELEMENT,V__NUMBER)
   = n__0)))
)
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer) &
       s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW6,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
     = V__NUMBER)
   =>
   ( ! [V__ELEMENT] :
     (s__instance(V__ELEMENT,s__Integer) =>
       s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
   =>
   (s__RemainderFn(V__ELEMENT,V__NUMBER)
   = n__0)))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
     = V__NUMBER)
   =>
   ( ! [V__ELEMENT] :
     (s__instance(V__ELEMENT,s__Integer) =>
       s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
   =>
   (s__RemainderFn(V__ELEMENT,V__NUMBER)
   = n__0)))
)
)

( ! [V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__1Fn(V__ROW2)
     = V__NUMBER)
   =>
   ( ! [V__ELEMENT] :
     (s__instance(V__ELEMENT,s__Integer) =>
       s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
   =>
   (s__RemainderFn(V__ELEMENT,V__NUMBER)
   = n__0)))
)
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer) &
       s__instance(V__ROW8,s__Integer) &
       s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW6,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
     = V__NUMBER)
   =>
   ( ! [V__ELEMENT] :
     (s__instance(V__ELEMENT,s__Integer) =>
       s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
   =>
   (s__RemainderFn(V__ELEMENT,V__NUMBER)
   = n__0)))
)
)

( ! [V__ROW3,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__2Fn(V__ROW2,V__ROW3)
     = V__NUMBER)
   =>
   ( ! [V__ELEMENT] :
     (s__instance(V__ELEMENT,s__Integer) =>
       s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
   =>
   (s__RemainderFn(V__ELEMENT,V__NUMBER)
   = n__0)))
)
)

Merge.kif 4630-4635
( ! [V__ROW3,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__2Fn(V__ROW2,V__ROW3)
     = V__NUMBER)
   =>
   ~(( ? [V__GREATER] :
       ((s__instance(V__GREATER,s__Integer) &
           (s__greaterThan(V__GREATER,V__NUMBER)
           &
           ( ! [V__ELEMENT] :
             (s__instance(V__ELEMENT,s__Integer) =>
               s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
           =>
           (s__RemainderFn(V__ELEMENT,V__GREATER)
           = n__0))))))))
)
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer) &
       s__instance(V__ROW8,s__Integer) &
       s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW6,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
     = V__NUMBER)
   =>
   ~(( ? [V__GREATER] :
       ((s__instance(V__GREATER,s__Integer) &
           (s__greaterThan(V__GREATER,V__NUMBER)
           &
           ( ! [V__ELEMENT] :
             (s__instance(V__ELEMENT,s__Integer) =>
               s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
           =>
           (s__RemainderFn(V__ELEMENT,V__GREATER)
           = n__0))))))))
)
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer) &
       s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW6,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
     = V__NUMBER)
   =>
   ~(( ? [V__GREATER] :
       ((s__instance(V__GREATER,s__Integer) &
           (s__greaterThan(V__GREATER,V__NUMBER)
           &
           ( ! [V__ELEMENT] :
             (s__instance(V__ELEMENT,s__Integer) =>
               s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
           =>
           (s__RemainderFn(V__ELEMENT,V__GREATER)
           = n__0))))))))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW6,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
     = V__NUMBER)
   =>
   ~(( ? [V__GREATER] :
       ((s__instance(V__GREATER,s__Integer) &
           (s__greaterThan(V__GREATER,V__NUMBER)
           &
           ( ! [V__ELEMENT] :
             (s__instance(V__ELEMENT,s__Integer) =>
               s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
           =>
           (s__RemainderFn(V__ELEMENT,V__GREATER)
           = n__0))))))))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
     = V__NUMBER)
   =>
   ~(( ? [V__GREATER] :
       ((s__instance(V__GREATER,s__Integer) &
           (s__greaterThan(V__GREATER,V__NUMBER)
           &
           ( ! [V__ELEMENT] :
             (s__instance(V__ELEMENT,s__Integer) =>
               s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
           =>
           (s__RemainderFn(V__ELEMENT,V__GREATER)
           = n__0))))))))
)
)

( ! [V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__1Fn(V__ROW2)
     = V__NUMBER)
   =>
   ~(( ? [V__GREATER] :
       ((s__instance(V__GREATER,s__Integer) &
           (s__greaterThan(V__GREATER,V__NUMBER)
           &
           ( ! [V__ELEMENT] :
             (s__instance(V__ELEMENT,s__Integer) =>
               s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
           =>
           (s__RemainderFn(V__ELEMENT,V__GREATER)
           = n__0))))))))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__GreatestCommonDivisorFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
     = V__NUMBER)
   =>
   ~(( ? [V__GREATER] :
       ((s__instance(V__GREATER,s__Integer) &
           (s__greaterThan(V__GREATER,V__NUMBER)
           &
           ( ! [V__ELEMENT] :
             (s__instance(V__ELEMENT,s__Integer) =>
               s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
           =>
           (s__RemainderFn(V__ELEMENT,V__GREATER)
           = n__0))))))))
)
)

Merge.kif 4637-4645
( ! [V__ELEMENT,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
     = V__NUMBER)
   =>
   s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
=>
s__instance(V__ELEMENT,s__Number) )
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer) &
       s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW6,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
     = V__NUMBER)
   =>
   s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
=>
s__instance(V__ELEMENT,s__Number) )
)

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

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

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

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

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

Merge.kif 4696-4701
( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer) &
       s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW6,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
     = V__NUMBER)
   =>
   ( ! [V__ELEMENT] :
     (s__instance(V__ELEMENT,s__Integer) =>
       s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
   =>
   (s__RemainderFn(V__NUMBER,V__ELEMENT)
   = n__0)))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
     = V__NUMBER)
   =>
   ( ! [V__ELEMENT] :
     (s__instance(V__ELEMENT,s__Integer) =>
       s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
   =>
   (s__RemainderFn(V__NUMBER,V__ELEMENT)
   = n__0)))
)
)

( ! [V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__1Fn(V__ROW2)
     = V__NUMBER)
   =>
   ( ! [V__ELEMENT] :
     (s__instance(V__ELEMENT,s__Integer) =>
       s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
   =>
   (s__RemainderFn(V__NUMBER,V__ELEMENT)
   = n__0)))
)
)

( ! [V__ROW3,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__2Fn(V__ROW2,V__ROW3)
     = V__NUMBER)
   =>
   ( ! [V__ELEMENT] :
     (s__instance(V__ELEMENT,s__Integer) =>
       s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
   =>
   (s__RemainderFn(V__NUMBER,V__ELEMENT)
   = n__0)))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW6,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
     = V__NUMBER)
   =>
   ( ! [V__ELEMENT] :
     (s__instance(V__ELEMENT,s__Integer) =>
       s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
   =>
   (s__RemainderFn(V__NUMBER,V__ELEMENT)
   = n__0)))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
     = V__NUMBER)
   =>
   ( ! [V__ELEMENT] :
     (s__instance(V__ELEMENT,s__Integer) =>
       s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
   =>
   (s__RemainderFn(V__NUMBER,V__ELEMENT)
   = n__0)))
)
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer) &
       s__instance(V__ROW8,s__Integer) &
       s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW6,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
     = V__NUMBER)
   =>
   ( ! [V__ELEMENT] :
     (s__instance(V__ELEMENT,s__Integer) =>
       s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
   =>
   (s__RemainderFn(V__NUMBER,V__ELEMENT)
   = n__0)))
)
)

Merge.kif 4703-4708
( ! [V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
     = V__NUMBER)
   =>
   ~(( ? [V__LESS] :
       ((s__instance(V__LESS,s__Integer) &
           (s__lessThan(V__LESS,V__NUMBER)
           &
           ( ! [V__ELEMENT] :
             (s__instance(V__ELEMENT,s__Integer) =>
               s__inList(V__ELEMENT,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
           =>
           (s__RemainderFn(V__LESS,V__ELEMENT)
           = n__0))))))))
)
)

( ! [V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__1Fn(V__ROW2)
     = V__NUMBER)
   =>
   ~(( ? [V__LESS] :
       ((s__instance(V__LESS,s__Integer) &
           (s__lessThan(V__LESS,V__NUMBER)
           &
           ( ! [V__ELEMENT] :
             (s__instance(V__ELEMENT,s__Integer) =>
               s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
           =>
           (s__RemainderFn(V__LESS,V__ELEMENT)
           = n__0))))))))
)
)

( ! [V__ROW3,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__2Fn(V__ROW2,V__ROW3)
     = V__NUMBER)
   =>
   ~(( ? [V__LESS] :
       ((s__instance(V__LESS,s__Integer) &
           (s__lessThan(V__LESS,V__NUMBER)
           &
           ( ! [V__ELEMENT] :
             (s__instance(V__ELEMENT,s__Integer) =>
               s__inList(V__ELEMENT,s__ListFn__2Fn(V__ROW2,V__ROW3))
           =>
           (s__RemainderFn(V__LESS,V__ELEMENT)
           = n__0))))))))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW6,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
     = V__NUMBER)
   =>
   ~(( ? [V__LESS] :
       ((s__instance(V__LESS,s__Integer) &
           (s__lessThan(V__LESS,V__NUMBER)
           &
           ( ! [V__ELEMENT] :
             (s__instance(V__ELEMENT,s__Integer) =>
               s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
           =>
           (s__RemainderFn(V__LESS,V__ELEMENT)
           = n__0))))))))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
     = V__NUMBER)
   =>
   ~(( ? [V__LESS] :
       ((s__instance(V__LESS,s__Integer) &
           (s__lessThan(V__LESS,V__NUMBER)
           &
           ( ! [V__ELEMENT] :
             (s__instance(V__ELEMENT,s__Integer) =>
               s__inList(V__ELEMENT,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
           =>
           (s__RemainderFn(V__LESS,V__ELEMENT)
           = n__0))))))))
)
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer) &
       s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW6,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
     = V__NUMBER)
   =>
   ~(( ? [V__LESS] :
       ((s__instance(V__LESS,s__Integer) &
           (s__lessThan(V__LESS,V__NUMBER)
           &
           ( ! [V__ELEMENT] :
             (s__instance(V__ELEMENT,s__Integer) =>
               s__inList(V__ELEMENT,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
           =>
           (s__RemainderFn(V__LESS,V__ELEMENT)
           = n__0))))))))
)
)

( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER] :
   ((s__instance(V__ROW7,s__Integer) &
       s__instance(V__ROW8,s__Integer) &
       s__instance(V__ROW5,s__Integer) &
       s__instance(V__ROW6,s__Integer) &
       s__instance(V__ROW3,s__Integer) &
       s__instance(V__ROW4,s__Integer) &
       s__instance(V__ROW2,s__Integer) &
       s__instance(V__NUMBER,s__Integer))
     =>
     (s__LeastCommonMultipleFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
     = V__NUMBER)
   =>
   ~(( ? [V__LESS] :
       ((s__instance(V__LESS,s__Integer) &
           (s__lessThan(V__LESS,V__NUMBER)
           &
           ( ! [V__ELEMENT] :
             (s__instance(V__ELEMENT,s__Integer) =>
               s__inList(V__ELEMENT,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
           =>
           (s__RemainderFn(V__LESS,V__ELEMENT)
           = n__0))))))))
)
)

Merge.kif 4710-4718
( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW7,s__Attribute) &
       s__instance(V__ROW5,s__Attribute) &
       s__instance(V__ROW6,s__Attribute) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__exhaustiveAttribute__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
   =>
   ( ! [V__ATTR1] :
     (s__instance(V__ATTR1,V__CLASS)
     =>
     ( ? [V__ATTR2] :
       ((s__inList(V__ATTR2,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
       &
       (V__ATTR1 = V__ATTR2))))))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Attribute) &
       s__instance(V__ROW6,s__Attribute) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__exhaustiveAttribute__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
   =>
   ( ! [V__ATTR1] :
     (s__instance(V__ATTR1,V__CLASS)
     =>
     ( ? [V__ATTR2] :
       ((s__inList(V__ATTR2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
       &
       (V__ATTR1 = V__ATTR2))))))
)
)

( ! [V__ROW2,V__CLASS] :
   ((s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__exhaustiveAttribute__2(V__CLASS,V__ROW2)
   =>
   ( ! [V__ATTR1] :
     (s__instance(V__ATTR1,V__CLASS)
     =>
     ( ? [V__ATTR2] :
       ((s__inList(V__ATTR2,s__ListFn__1Fn(V__ROW2))
       &
       (V__ATTR1 = V__ATTR2))))))
)
)

( ! [V__ROW3,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__exhaustiveAttribute__3(V__CLASS,V__ROW2,V__ROW3)
   =>
   ( ! [V__ATTR1] :
     (s__instance(V__ATTR1,V__CLASS)
     =>
     ( ? [V__ATTR2] :
       ((s__inList(V__ATTR2,s__ListFn__2Fn(V__ROW2,V__ROW3))
       &
       (V__ATTR1 = V__ATTR2))))))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Attribute) &
       s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__exhaustiveAttribute__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
   =>
   ( ! [V__ATTR1] :
     (s__instance(V__ATTR1,V__CLASS)
     =>
     ( ? [V__ATTR2] :
       ((s__inList(V__ATTR2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
       &
       (V__ATTR1 = V__ATTR2))))))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Attribute) &
       s__instance(V__ROW4,s__Attribute) &
       s__instance(V__ROW2,s__Attribute) &
       s__subclass(V__CLASS,s__Attribute) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__exhaustiveAttribute__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
   =>
   ( ! [V__ATTR1] :
     (s__instance(V__ATTR1,V__CLASS)
     =>
     ( ? [V__ATTR2] :
       ((s__inList(V__ATTR2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
       &
       (V__ATTR1 = V__ATTR2))))))
)
)

Merge.kif 510-518
( ! [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Class) &
       s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW4,s__Class) &
       s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__exhaustiveDecomposition__5(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5)
   =>
   ( ! [V__OBJ] :
     (s__instance(V__OBJ,V__CLASS)
     =>
     ( ? [V__ITEM] :
       ((s__instance(V__ITEM,s__SetOrClass) &
           (s__inList(V__ITEM,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
         &
         s__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__instance(V__ROW5,s__Class) &
       s__instance(V__ROW6,s__Class) &
       s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW4,s__Class) &
       s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__exhaustiveDecomposition__7(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
   =>
   ( ! [V__OBJ] :
     (s__instance(V__OBJ,V__CLASS)
     =>
     ( ? [V__ITEM] :
       ((s__instance(V__ITEM,s__SetOrClass) &
           (s__inList(V__ITEM,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
         &
         s__instance(V__OBJ,V__ITEM)))))))
)
)

( ! [V__ROW3,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__exhaustiveDecomposition__3(V__CLASS,V__ROW2,V__ROW3)
   =>
   ( ! [V__OBJ] :
     (s__instance(V__OBJ,V__CLASS)
     =>
     ( ? [V__ITEM] :
       ((s__instance(V__ITEM,s__SetOrClass) &
           (s__inList(V__ITEM,s__ListFn__2Fn(V__ROW2,V__ROW3))
         &
         s__instance(V__OBJ,V__ITEM)))))))
)
)

( ! [V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW4,s__Class) &
       s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__exhaustiveDecomposition__4(V__CLASS,V__ROW2,V__ROW3,V__ROW4)
   =>
   ( ! [V__OBJ] :
     (s__instance(V__OBJ,V__CLASS)
     =>
     ( ? [V__ITEM] :
       ((s__instance(V__ITEM,s__SetOrClass) &
           (s__inList(V__ITEM,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
         &
         s__instance(V__OBJ,V__ITEM)))))))
)
)

( ! [V__ROW2,V__CLASS] :
   ((s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__exhaustiveDecomposition__2(V__CLASS,V__ROW2)
   =>
   ( ! [V__OBJ] :
     (s__instance(V__OBJ,V__CLASS)
     =>
     ( ? [V__ITEM] :
       ((s__instance(V__ITEM,s__SetOrClass) &
           (s__inList(V__ITEM,s__ListFn__1Fn(V__ROW2))
         &
         s__instance(V__OBJ,V__ITEM)))))))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__CLASS] :
   ((s__instance(V__ROW5,s__Class) &
       s__instance(V__ROW6,s__Class) &
       s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW4,s__Class) &
       s__instance(V__ROW2,s__Class) &
       s__instance(V__CLASS,s__Class) &
       s__instance(V__CLASS,s__SetOrClass))
     =>
     s__exhaustiveDecomposition__6(V__CLASS,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
   =>
   ( ! [V__OBJ] :
     (s__instance(V__OBJ,V__CLASS)
     =>
     ( ? [V__ITEM] :
       ((s__instance(V__ITEM,s__SetOrClass) &
           (s__inList(V__ITEM,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
         &
         s__instance(V__OBJ,V__ITEM)))))))
)
)

Merge.kif 2829-2837
( ! [V__ELEMENT,V__ROW2] :
   (s__instance(V__ROW2,s__Class) =>
     s__exhaustiveDecomposition__1(V__ROW2)
   =>
   s__inList(V__ELEMENT,s__ListFn__1Fn(V__ROW2))
=>
s__instance(V__ELEMENT,s__Class) )
)

( ! [V__ROW5,V__ROW6,V__ELEMENT,V__ROW3,V__ROW4,V__ROW2] :
   ((s__instance(V__ROW5,s__Class) &
       s__instance(V__ROW6,s__Class) &
       s__instance(V__ROW3,s__Class) &
       s__instance(V__ROW4,s__Class) &
       s__instance(V__ROW2,s__Class))
     =>
     s__exhaustiveDecomposition__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
   =>
   s__inList(V__ELEMENT,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
=>
s__instance(V__ELEMENT,s__Class) )
)

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

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

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

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

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

Merge.kif 558-562
( ! [V__L] :
   (s__instance(V__L,s__Album) =>
     ( ! [V__X] :
       (s__inList(V__X,V__L)
       =>
       s__instance(V__X,s__Recording)))
   )
)

Music.kif 53-58
( ! [V__SVC] :
   (s__instance(V__SVC,s__ShuttleService) =>
     ( ? [V__LIST, V__VEHICLE, V__AGENT] :
       ((s__instance(V__AGENT,s__Agent) &
           (s__agent(V__SVC,V__AGENT)
           &
           s__possesses(V__AGENT,V__VEHICLE)
         &
         s__instance(V__VEHICLE,s__Automobile) &
         s__instance(V__LIST,s__List) &
         ( ! [V__X] :
           (s__inList(V__X,V__LIST)
           =>
           (s__instance(V__X,s__PostalPlace) &
             ( ? [V__TRANSPORT] :
               ((s__instance(V__TRANSPORT,s__Transportation) &
                   s__agent(V__TRANSPORT,V__AGENT)
                 &
                 s__instrument(V__TRANSPORT,V__VEHICLE)
               &
               s__destination(V__TRANSPORT,V__X)))))))))))
)
)

Hotel.kif 1983-2001
( ! [V__X] :
   (s__instance(V__X,s__AlbumChart) =>
     ( ? [V__A] :
       ((s__instance(V__A,s__Album) &
           s__inList(V__A,V__X))))
   )
)

Music.kif 1141-1146
No TPTP formula. May not be expressible in strict first order. Music.kif 1117-1122

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