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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - subclass
subclass

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


s__documentation(s__subclass__m,s__ChineseLanguage,'"(subclass ?CLASS1 ?CLASS2) 的意思是 ?CLASS1 是 ?CLASS2 的 subclass,也就是说, ?CLASS1 的每一个 instance 同时也是 ?CLASS2 的一个 instance。一个 Class 可以具有多个超类别和子类别。"')

chinese_format.kif 1371-1373
s__documentation(s__subclass__m,s__EnglishLanguage,'"(subclass ?CLASS1 ?CLASS2) means that ?CLASS1 is a subclass of ?CLASS2, i.e. every instance of ?CLASS1 is also an instance of ?CLASS2. A Class may have multiple superclasses and subclasses."')

Merge.kif 132-134
s__domain(s__subclass__m,n__1,s__SetOrClass)

Merge.kif 130-130 The number 1 argument of subclass is an instance of set or class
s__domain(s__subclass__m,n__2,s__SetOrClass)

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

s__instance(s__BinaryPredicate,s__SetOrClass)

Merge.kif 128-128 subclass is an instance of binary predicate
s__instance(s__subclass__m,s__PartialOrderingRelation)

s__instance(s__PartialOrderingRelation,s__SetOrClass)

Merge.kif 129-129 subclass is an instance of partial ordering relation

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


s__format(s__ChineseLanguage,s__subclass__m,'"%1 %n 是 %2 的 subclass"')

chinese_format.kif 319-319
s__format(s__EnglishLanguage,s__subclass__m,'"%1 is %n a subclass of %2"')

english_format.kif 327-327
s__subrelation(s__subset__m,s__subclass__m)

Merge.kif 5066-5066 subset is a subrelation of subclass
s__termFormat(s__ChineseLanguage,s__subclass__m,'"子类"')

domainEnglishFormat.kif 55597-55597
s__termFormat(s__ChineseLanguage,s__subclass__m,'"子类别"')

chinese_format.kif 320-320
s__termFormat(s__ChineseTraditionalLanguage,s__subclass__m,'"子類"')

domainEnglishFormat.kif 55596-55596
s__termFormat(s__EnglishLanguage,s__subclass__m,'"subclass"')

domainEnglishFormat.kif 55595-55595

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


( ∀ [V__ROOM,V__HOTELUNIT]
   ((s__instance(V__ROOM,s__Object) ∧
       s__instance(V__HOTELUNIT,s__SetOrClass))
     ⇒
     (s__attribute(V__ROOM,s__Oversized) ∧
       s__immediateInstance(V__ROOM,V__HOTELUNIT)
     ∧
     s__subclass(V__HOTELUNIT,s__HotelUnit))
   ⇒
   ( ∃ [V__NORMAL, V__AREA1, V__AREA2]
     ((s__instance(V__NORMAL,s__Object) ∧
         (s__immediateInstance(V__NORMAL,V__HOTELUNIT)
         ∧
         s__measure(V__NORMAL,V__AREA1)
       ∧
       s__measure(V__ROOM,V__AREA2)
     ∧
     s__instance(V__AREA1,s__AreaMeasure) ∧
     s__instance(V__AREA2,s__AreaMeasure) ∧
     s__greaterThan(V__AREA2,V__AREA1)))))
)
)

Hotel.kif 1140-1152
( ∀ [V__AGENT,V__CLASS]
   ((s__instance(V__AGENT,s__Agent) ∧
       s__subclass(V__CLASS,s__ContentBearingObject) ∧
       s__subclass(V__CLASS,s__MusicalComposition) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__authors(V__AGENT,V__CLASS)
     ∧
     s__subclass(V__CLASS,s__MusicalComposition))
   ⇒
   s__composer(V__AGENT,V__CLASS)
)
)

Media.kif 1853-1857
( ∀ [V__AGENT,V__PROCESS,V__SUB]
   ((s__subclass(V__AGENT,s__BiochemicalAgent) ∧
       s__instance(V__PROCESS,s__SetOrClass) ∧
       s__subclass(V__PROCESS,s__Process) ∧
       s__instance(V__SUB,s__SetOrClass) ∧
       s__subclass(V__SUB,s__Process))
     ⇒
     (s__biochemicalAgentDelivery(V__AGENT,V__PROCESS)
     ∧
     s__subclass(V__SUB,V__PROCESS))

s__biochemicalAgentDelivery(V__AGENT,V__SUB)
)
)

WMD.kif 784-788
( ∀ [V__AGENT,V__ORGANISM,V__SUB]
   ((s__subclass(V__AGENT,s__BiologicalAgent) ∧
       s__subclass(V__ORGANISM,s__Organism) ∧
       s__instance(V__ORGANISM,s__SetOrClass) ∧
       s__subclass(V__SUB,s__Organism) ∧
       s__instance(V__SUB,s__SetOrClass))
     ⇒
     (s__biologicalAgentCarrier(V__AGENT,V__ORGANISM)
     ∧
     s__subclass(V__SUB,V__ORGANISM))

s__biologicalAgentCarrier(V__AGENT,V__SUB)
)
)

WMD.kif 931-935
( ∀ [V__PC,V__MV,V__ROLE]
   ((s__instance(V__PC,s__SetOrClass) ∧
       s__subclass(V__PC,s__Process) ∧
       s__instance(V__MV,s__Object) ∧
       s__instance(V__ROLE,s__CaseRole))
     ⇒
     (s__capability(V__PC,V__ROLE,V__MV)
     ∧
     s__subclass(V__PC,s__Shooting))
   ⇒
   ( ∃ [V__WEAPON]
     ((s__instance(V__WEAPON,s__Weapon) ∧
         s__part(V__WEAPON,V__MV)
       ∧
       s__capability(V__PC,V__ROLE,V__WEAPON))))
)
)

MilitaryDevices.kif 48-56
( ∀ [V__A2,V__A3,V__CURRENCY,V__AREA]
   ((s__instance(V__A2,s__SymbolicString) ∧
       s__instance(V__A3,s__SymbolicString) ∧
       s__instance(V__CURRENCY,s__UnitOfCurrency) ∧
       s__instance(V__AREA,s__GeopoliticalArea) ∧
       s__instance(V__AREA,s__SetOrClass))
     ⇒
     (s__codeMapping(s__ISO_4217_A,V__A3,V__CURRENCY)
     ∧
     s__codeMapping(s__ISO_3166_1_alpha_2,V__A2,V__AREA)
   ∧
   s__subclass(V__AREA,s__GeopoliticalArea) ∧
   (V__A2 = s__SubstringFn(V__A3,n__0,n__2)))

s__currencyType(V__AREA,V__CURRENCY)
)
)

Media.kif 2859-2865
( ∀ [V__DAY,V__MONTH,V__HOLIDAY,V__LATER_YEAR,V__DATE,V__YEAR]
   ((s__instance(V__DAY,s__PositiveInteger) ∧
       s__subclass(V__MONTH,s__Month) ∧
       s__instance(V__HOLIDAY,s__Holiday) ∧
       s__instance(V__HOLIDAY,s__SetOrClass) ∧
       s__instance(V__LATER_YEAR,s__Integer) ∧
       s__instance(V__YEAR,s__Integer))
     ⇒
     (s__commemoratesDate(V__HOLIDAY,s__DayFn(V__DAY,s__MonthFn(V__MONTH,s__YearFn(V__YEAR))))

s__instance(V__DATE,V__HOLIDAY)

s__subclass(V__HOLIDAY,s__FixedHoliday) ∧
s__lessThanOrEqualTo(V__YEAR,V__LATER_YEAR))

s__instance(V__DATE,s__DayFn(V__DAY,s__MonthFn(V__MONTH,s__YearFn(V__LATER_YEAR))))
)
)

Government.kif 606-612
No TPTP formula. May not be expressible in strict first order. Hotel.kif 480-496
No TPTP formula. May not be expressible in strict first order. Hotel.kif 498-514
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11147-11158
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11118-11129
( ∀ [V__PROCESS,V__SUBSTANCE,V__DISEASE,V__SUB]
   ((s__instance(V__PROCESS,s__SetOrClass) ∧
       s__subclass(V__PROCESS,s__Process) ∧
       s__subclass(V__SUBSTANCE,s__BiologicallyActiveSubstance) ∧
       s__instance(V__DISEASE,s__DiseaseOrSyndrome) ∧
       s__instance(V__SUB,s__SetOrClass) ∧
       s__subclass(V__SUB,s__Process))
     ⇒
     (s__diseaseTreatment(V__DISEASE,V__SUBSTANCE,V__PROCESS)
     ∧
     s__subclass(V__SUB,V__PROCESS))

s__diseaseTreatment(V__DISEASE,V__SUBSTANCE,V__SUB)
)
)

WMD.kif 912-916
( ∀ [V__PROCESS,V__SUBSTANCE,V__DISEASE,V__SUB]
   ((s__subclass(V__PROCESS,s__Process) ∧
       s__subclass(V__SUBSTANCE,s__BiologicallyActiveSubstance) ∧
       s__instance(V__SUBSTANCE,s__SetOrClass) ∧
       s__instance(V__DISEASE,s__DiseaseOrSyndrome) ∧
       s__subclass(V__SUB,s__BiologicallyActiveSubstance) ∧
       s__instance(V__SUB,s__SetOrClass))
     ⇒
     (s__diseaseTreatment(V__DISEASE,V__SUBSTANCE,V__PROCESS)
     ∧
     s__subclass(V__SUB,V__SUBSTANCE))

s__diseaseTreatment(V__DISEASE,V__SUB,V__PROCESS)
)
)

WMD.kif 918-922
No TPTP formula. May not be expressible in strict first order. Economy.kif 2116-2125
No TPTP formula. May not be expressible in strict first order. Economy.kif 2160-2169
No TPTP formula. May not be expressible in strict first order. Economy.kif 2206-2215
No TPTP formula. May not be expressible in strict first order. Economy.kif 1984-1993
( ∀ [V__CLASS2,V__CLASS1,V__OBJCLASS2,V__OBJCLASS1]
   ((s__subclass(V__CLASS2,s__Getting) ∧
       s__instance(V__CLASS2,s__SetOrClass) ∧
       s__subclass(V__CLASS1,s__Getting) ∧
       s__instance(V__CLASS1,s__SetOrClass) ∧
       s__subclass(V__OBJCLASS2,s__Object) ∧
       s__instance(V__OBJCLASS2,s__SetOrClass) ∧
       s__subclass(V__OBJCLASS1,s__Object) ∧
       s__instance(V__OBJCLASS1,s__SetOrClass))
     ⇒
     ((V__CLASS1 = s__ReceivingAnObjectFn(V__OBJCLASS1))
     ∧
     (V__CLASS2 = s__ReceivingAnObjectFn(V__OBJCLASS2))
   ∧
   s__subclass(V__OBJCLASS1,V__OBJCLASS2))

s__subclass(V__CLASS1,V__CLASS2)
)
)

Media.kif 195-200
( ∀ [V__COMP,V__PHYS,V__DEP]
   ((s__instance(V__COMP,s__Organization) ∧
       s__instance(V__PHYS,s__SetOrClass) ∧
       s__subclass(V__PHYS,s__Process) ∧
       s__instance(V__DEP)
     ∧
     s__instance(V__DEP,s__Agent))
   ⇒
   ((V__DEP = s__DepartmentOfPreventingFn(V__COMP,V__PHYS))
   ∧
   s__subclass(V__PHYS,s__Process))

s__inhibits(V__DEP,V__PHYS)
)
)

Mid-level-ontology.kif 16064-16068
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 16070-16079
No TPTP formula. May not be expressible in strict first order. Economy.kif 2281-2290
( ∀ [V__O,V__P,V__R,V__ROOM,V__OBJ,V__GUEST,V__HOTEL]
   ((s__instance(V__O,s__Object) ∧
       s__instance(V__R,s__TemporaryResidence) ∧
       s__instance(V__ROOM,s__SetOrClass) ∧
       s__subclass(V__ROOM,s__HotelUnit) ∧
       s__instance(V__OBJ,s__SetOrClass) ∧
       s__instance(V__GUEST,s__Human) ∧
       s__instance(V__HOTEL,s__Agent))
     ⇒
     (s__freeRoomAmenity(V__ROOM,V__OBJ)
     ∧
     s__subclass(V__OBJ,s__Object) ∧
     s__instance(V__R,V__ROOM)
   ∧
   s__stays(V__GUEST,V__R)

s__element(V__R,s__PropertyFn(V__HOTEL))

s__instance(V__O,V__OBJ)

s__located(V__O,V__R)

s__instance(V__P,s__Process) ∧
s__agent(V__P,V__GUEST)

(s__patient(V__P,V__O)

s__instrument(V__P,V__O)

s__resource(V__P,V__O)))

s__price(V__P,s__MeasureFn(n__0,s__UnitedStatesDollar),V__HOTEL)
)
)

Hotel.kif 334-349
( ∀ [V__P,V__R,V__ROOM,V__S,V__PROC,V__GUEST,V__HOTEL]
   ((s__instance(V__P,s__Process) ∧
       s__instance(V__R,s__TemporaryResidence) ∧
       s__instance(V__ROOM,s__SetOrClass) ∧
       s__subclass(V__ROOM,s__HotelUnit) ∧
       s__instance(V__S,s__Process) ∧
       s__instance(V__PROC,s__SetOrClass) ∧
       s__instance(V__GUEST,s__Human) ∧
       s__instance(V__HOTEL,s__Agent))
     ⇒
     (s__freeRoomAmenity(V__ROOM,V__PROC)
     ∧
     s__subclass(V__PROC,s__Process) ∧
     s__instance(V__R,V__ROOM)
   ∧
   s__stays(V__GUEST,V__R)

s__element(V__R,s__PropertyFn(V__HOTEL))

s__patient(V__P,V__GUEST)

(s__instance(V__P,V__PROC)

(s__instance(V__S,V__PROC)

s__subProcess(V__P,V__S)))

s__located(V__P,V__R))

s__price(V__P,s__MeasureFn(n__0,s__UnitedStatesDollar),V__HOTEL)
)
)

Hotel.kif 351-365
No TPTP formula. May not be expressible in strict first order. Hotel.kif 784-805
No TPTP formula. May not be expressible in strict first order. Hotel.kif 289-308

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


( ∀ [V__CLASS]
   ((s__instance(V__CLASS,s__Class) ⇒
       s__subclass(V__CLASS,s__Entity))
     ∧
     (s__subclass(V__CLASS,s__Entity) ⇒
       s__instance(V__CLASS,s__Class))
     )
   )

Merge.kif 793-795 A set or class is an instance of class if and only if the set or class is a subclass of entity
( ∀ [V__CLASS2,V__CLASS1,V__REL,V__NUMBER]
   ((s__instance(V__CLASS2,s__SetOrClass) ∧
       s__instance(V__CLASS1,s__SetOrClass) ∧
       s__instance(V__REL,s__Relation) ∧
       s__instance(V__NUMBER,s__PositiveInteger))
     ⇒
     (s__domain(V__REL,V__NUMBER,V__CLASS1)
     ∧
     s__domain(V__REL,V__NUMBER,V__CLASS2))

(s__subclass(V__CLASS1,V__CLASS2)

s__subclass(V__CLASS2,V__CLASS1))
)
)

Merge.kif 219-225
( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__PositiveInteger) ∧
       s__instance(V__ROW2,s__ComputerPath) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__slidingWindowSize__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__slidingWindowSize__m,s__Predicate) ∧
     s__slidingWindowSize(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Computer) ∧
       s__instance(V__ROW2,s__SymbolicString) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__hardwareType__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__hardwareType__m,s__Predicate) ∧
     s__hardwareType(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TimePosition) ∧
       s__instance(V__ROW2,s__Option) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__outOfTheMoney__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__outOfTheMoney__m,s__Predicate) ∧
     s__outOfTheMoney(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__SymbolicString) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__internetCountryCode__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__internetCountryCode__m,s__Predicate) ∧
     s__internetCountryCode(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__VolumeMeasure) ∧
       s__instance(V__ROW2,s__IntermittentCombustionEngine) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__engineDisplacement__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__engineDisplacement__m,s__Predicate) ∧
     s__engineDisplacement(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__GeopoliticalArea) ∧
       s__instance(V__ROW2,s__City) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__capitalCity__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__capitalCity__m,s__Predicate) ∧
     s__capitalCity(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Object) ∧
       s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__carries__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__carries__m,s__Predicate) ∧
     s__carries(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW4,s__TimeInterval) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__militaryExpendituresInUSDollarsInPeriod__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__militaryExpendituresInUSDollarsInPeriod__m,s__Predicate) ∧
     s__militaryExpendituresInUSDollarsInPeriod(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,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__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__exhaustiveDecomposition__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__exhaustiveDecomposition__m,s__Predicate) ∧
     s__exhaustiveDecomposition__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))

s__subclass(s__ListOrderFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__LengthMeasure) ∧
       s__instance(V__ROW2,s__WaterArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__navigableForDraft__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__navigableForDraft__m,s__Predicate) ∧
     s__navigableForDraft(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TimeInterval) ∧
       s__instance(V__ROW2,s__MusicChart) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__musicChartPeriod__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__musicChartPeriod__m,s__Predicate) ∧
     s__musicChartPeriod(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__musicGenre__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__musicGenre__m,s__Predicate) ∧
     s__musicGenre(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Organism) ∧
       s__instance(V__ROW2,s__Organism) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__sibling__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__sibling__m,s__Predicate) ∧
     s__sibling(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__LengthMeasure) ∧
       s__subclass(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__defaultMaximumHeight__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__defaultMaximumHeight__m,s__Predicate) ∧
     s__defaultMaximumHeight(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__RealNumber) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__highestDecileShareOfHouseholdIncome__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__highestDecileShareOfHouseholdIncome__m,s__Predicate) ∧
     s__highestDecileShareOfHouseholdIncome(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__ConstantQuantity) ∧
       s__instance(V__ROW2,s__GeographicArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__irrigatedLandArea__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__irrigatedLandArea__m,s__Predicate) ∧
     s__irrigatedLandArea(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__ComputerProgram) ∧
       s__instance(V__ROW2,s__ComputerFile) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__programCopy__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__programCopy__m,s__Predicate) ∧
     s__programCopy(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__LengthMeasure) ∧
       s__instance(V__ROW2,s__Circle) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__radius__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__radius__m,s__Predicate) ∧
     s__radius(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Human) ∧
       s__instance(V__ROW2,s__Experimenting) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__qualifiedExperiment__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__qualifiedExperiment__m,s__Predicate) ∧
     s__qualifiedExperiment(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Human) ∧
       s__instance(V__ROW4,s__WebSite) ∧
       s__instance(V__ROW2,s__Collection) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__webPurchases__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__webPurchases__m,s__Predicate) ∧
     s__webPurchases(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Quantity) ∧
       s__instance(V__ROW2,s__GraphArc) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__arcWeight__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__arcWeight__m,s__Predicate) ∧
     s__arcWeight(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Proposition) ∧
       s__instance(V__ROW2,s__Argument) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__premise__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__premise__m,s__Predicate) ∧
     s__premise(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__GeopoliticalArea) ∧
       s__instance(V__ROW4,s__PositiveInteger) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__importPartnerByRank__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__importPartnerByRank__m,s__Predicate) ∧
     s__importPartnerByRank(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW4,s__Agent) ∧
       s__instance(V__ROW2,s__Physical) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__price__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__price__m,s__Predicate) ∧
     s__price(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW5,s__CognitiveAgent) ∧
       s__instance(V__ROW3,s__DeonticAttribute) ∧
       s__instance(V__ROW4,s__Agreement) ∧
       s__instance(V__ROW2,s__Proposition) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__agreementClause__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__agreementClause__m,s__Predicate) ∧
     s__agreementClause(V__ROW2,V__ROW3,V__ROW4,V__ROW5))

s__subclass(s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__PhysicalQuantity) ∧
       s__instance(V__ROW2,s__WaterVehicle) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__vesselGrossRegisteredTonnage__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__vesselGrossRegisteredTonnage__m,s__Predicate) ∧
     s__vesselGrossRegisteredTonnage(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((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__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__partition__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__partition__m,s__Predicate) ∧
     s__partition__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))

s__subclass(s__ListOrderFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__LengthMeasure) ∧
       s__instance(V__ROW2,s__WaterArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__waterDepth__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__waterDepth__m,s__Predicate) ∧
     s__waterDepth(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__PositiveInteger) ∧
       s__instance(V__ROW2,s__PureSubstance) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__protonNumber__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__protonNumber__m,s__Predicate) ∧
     s__protonNumber(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TaskRelationAttribute) ∧
       s__instance(V__ROW2,s__RealtimeSystem) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__taskRelation__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__taskRelation__m,s__Predicate) ∧
     s__taskRelation(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__GeometricFigure) ∧
       s__instance(V__ROW2,s__OneDimensionalFigure) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__sideOfFigure__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__sideOfFigure__m,s__Predicate) ∧
     s__sideOfFigure(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__completelyFills__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__completelyFills__m,s__Predicate) ∧
     s__completelyFills(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TruthValue) ∧
       s__instance(V__ROW2,s__Sentence) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__truth__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__truth__m,s__Predicate) ∧
     s__truth(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Quantity) ∧
       s__instance(V__ROW2,s__Quantity) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__greaterThan__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__greaterThan__m,s__Predicate) ∧
     s__greaterThan(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__SymbolicString) ∧
       s__instance(V__ROW2,s__MonitoringProgram) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__dataID__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__dataID__m,s__Predicate) ∧
     s__dataID(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__NonnegativeRealNumber) ∧
       s__instance(V__ROW2,s__Region) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__cloudCoverFraction__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__cloudCoverFraction__m,s__Predicate) ∧
     s__cloudCoverFraction(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TemperatureMeasure) ∧
       s__instance(V__ROW2,s__Device) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__maxDeviceStorageTemp__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__maxDeviceStorageTemp__m,s__Predicate) ∧
     s__maxDeviceStorageTemp(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Object) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__exportCommodityType__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__exportCommodityType__m,s__Predicate) ∧
     s__exportCommodityType(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Integer) ∧
       s__instance(V__ROW4,s__Integer) ∧
       s__instance(V__ROW2,s__Relation) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__maxCardinality__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__maxCardinality__m,s__Predicate) ∧
     s__maxCardinality(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__LengthMeasure) ∧
       s__instance(V__ROW2,s__Tremor) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__physicalAmplitude__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__physicalAmplitude__m,s__Predicate) ∧
     s__physicalAmplitude(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW5,s__CurrencyMeasure) ∧
       s__instance(V__ROW3,s__Human) ∧
       s__instance(V__ROW4,s__TimeDuration) ∧
       s__instance(V__ROW2,s__Organization) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__monetaryWage__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__monetaryWage__m,s__Predicate) ∧
     s__monetaryWage(V__ROW2,V__ROW3,V__ROW4,V__ROW5))

s__subclass(s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Physical) ∧
       s__instance(V__ROW2,s__GeographicArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__naturalHazardTypeInArea__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__naturalHazardTypeInArea__m,s__Predicate) ∧
     s__naturalHazardTypeInArea(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__StrictnessAttribute) ∧
       s__instance(V__ROW2,s__RealtimeSystem) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__strictness__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__strictness__m,s__Predicate) ∧
     s__strictness(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__LengthMeasure) ∧
       s__subclass(V__ROW2,s__Gun) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__caliber__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__caliber__m,s__Predicate) ∧
     s__caliber(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Formula) ∧
       s__instance(V__ROW2,s__CognitiveAgent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__considers__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__considers__m,s__Predicate) ∧
     s__considers(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__ComputerStatus) ∧
       s__instance(V__ROW2,s__Computer) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__hostStatus__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__hostStatus__m,s__Predicate) ∧
     s__hostStatus(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Investment) ∧
       s__instance(V__ROW4,s__CurrencyMeasure) ∧
       s__instance(V__ROW2,s__CognitiveAgent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__potentialLoss__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__potentialLoss__m,s__Predicate) ∧
     s__potentialLoss(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Class) ∧
       s__instance(V__ROW2,s__Class) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__partition__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__partition__m,s__Predicate) ∧
     s__partition__2(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Organization) ∧
       s__instance(V__ROW2,s__HotelPackage) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__accommodationProvider__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__accommodationProvider__m,s__Predicate) ∧
     s__accommodationProvider(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Attribute) ∧
       s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__windRelativePosition__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__windRelativePosition__m,s__Predicate) ∧
     s__windRelativePosition(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Agent) ∧
       s__subclass(V__ROW2,s__Process) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__typicalAction__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__typicalAction__m,s__Predicate) ∧
     s__typicalAction(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__GUIElement) ∧
       s__instance(V__ROW2,s__GUIElement) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__guiElementPartiallyCoveredBy__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__guiElementPartiallyCoveredBy__m,s__Predicate) ∧
     s__guiElementPartiallyCoveredBy(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__NaturalSubstance) ∧
       s__subclass(V__ROW2,s__OrganicObject) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__secretesSubstance__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__secretesSubstance__m,s__Predicate) ∧
     s__secretesSubstance(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__SetOrClass) ∧
       s__instance(V__ROW2,s__SetOrClass) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__subclass__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__subclass__m,s__Predicate) ∧
     s__subclass(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Formula) ∧
       s__instance(V__ROW2,s__Formula) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__decreasesLikelihood__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__decreasesLikelihood__m,s__Predicate) ∧
     s__decreasesLikelihood(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TemperatureMeasure) ∧
       s__subclass(V__ROW2,s__PureSubstance) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__boilingPoint__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__boilingPoint__m,s__Predicate) ∧
     s__boilingPoint(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__FunctionQuantity) ∧
       s__instance(V__ROW2,s__InternalCombustionEngine) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__engineIdleSpeed__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__engineIdleSpeed__m,s__Predicate) ∧
     s__engineIdleSpeed(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Artifact) ∧
       s__subclass(V__ROW2,s__Artifact) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__version__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__version__m,s__Predicate) ∧
     s__version(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW2,s__SymbolicString) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__names__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__names__m,s__Predicate) ∧
     s__names(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Object) ∧
       s__instance(V__ROW2,s__HotelPackage) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__physicalInclusion__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__physicalInclusion__m,s__Predicate) ∧
     s__physicalInclusion(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW4,s__Language) ∧
       s__instance(V__ROW2,s__LinguisticExpression) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__representsInLanguage__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__representsInLanguage__m,s__Predicate) ∧
     s__representsInLanguage(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Formula) ∧
       s__instance(V__ROW2,s__CognitiveAgent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__expects__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__expects__m,s__Predicate) ∧
     s__expects(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__ComputerMenuItem) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__accessibleFromMenuItem__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__accessibleFromMenuItem__m,s__Predicate) ∧
     s__accessibleFromMenuItem(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__ContentBearingPhysical) ∧
       s__instance(V__ROW2,s__Human) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__actedIn__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__actedIn__m,s__Predicate) ∧
     s__actedIn(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Human) ∧
       s__instance(V__ROW2,s__Human) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__stranger__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__stranger__m,s__Predicate) ∧
     s__stranger(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Position) ∧
       s__instance(V__ROW4,s__Agent) ∧
       s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__diplomaticRepresentationType__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__diplomaticRepresentationType__m,s__Predicate) ∧
     s__diplomaticRepresentationType(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__ProcessStatus) ∧
       s__instance(V__ROW2,s__ComputerProcess) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__status__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__status__m,s__Predicate) ∧
     s__status(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Quantity) ∧
       s__instance(V__ROW2,s__Quantity) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__greaterThanOrEqualTo__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__greaterThanOrEqualTo__m,s__Predicate) ∧
     s__greaterThanOrEqualTo(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__subclass(V__ROW4,s__TimeInterval) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__annualRevenuesOfAreaInPeriod__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__annualRevenuesOfAreaInPeriod__m,s__Predicate) ∧
     s__annualRevenuesOfAreaInPeriod(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW4,s__Day) ∧
       s__instance(V__ROW2,s__Stock) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__closingPrice__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__closingPrice__m,s__Predicate) ∧
     s__closingPrice(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW2,s__SymbolicString) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__abbreviation__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__abbreviation__m,s__Predicate) ∧
     s__abbreviation(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__ComputerProgram) ∧
       s__instance(V__ROW2,s__StartupBlock) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__startupOf__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__startupOf__m,s__Predicate) ∧
     s__startupOf(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__SymbolicString) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__flagDescription__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__flagDescription__m,s__Predicate) ∧
     s__flagDescription(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Object) ∧
       s__instance(V__ROW2,s__Process) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__targetInAttack__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__targetInAttack__m,s__Predicate) ∧
     s__targetInAttack(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Agreement) ∧
       s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__unratifiedSignatoryToAgreement__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__unratifiedSignatoryToAgreement__m,s__Predicate) ∧
     s__unratifiedSignatoryToAgreement(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__RelationalAttribute) ∧
       s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__colocatedAgent__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__colocatedAgent__m,s__Predicate) ∧
     s__colocatedAgent(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Agent) ∧
       s__instance(V__ROW2,s__ChangeOfControl) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__losesControl__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__losesControl__m,s__Predicate) ∧
     s__losesControl(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TimeDuration) ∧
       s__instance(V__ROW2,s__UserRequest) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__responseTime__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__responseTime__m,s__Predicate) ∧
     s__responseTime(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__PhysicalQuantity) ∧
       s__instance(V__ROW2,s__ImageFile) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__imageResolution__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__imageResolution__m,s__Predicate) ∧
     s__imageResolution(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Integer) ∧
       s__instance(V__ROW2,s__ComputerProgram) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__criticalityLevel__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__criticalityLevel__m,s__Predicate) ∧
     s__criticalityLevel(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Object) ∧
       s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__larger__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__larger__m,s__Predicate) ∧
     s__larger(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW4,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__representsForAgent__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__representsForAgent__m,s__Predicate) ∧
     s__representsForAgent(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW2,s__BankStatement) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__statementInterest__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__statementInterest__m,s__Predicate) ∧
     s__statementInterest(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__PlaneAngleMeasure) ∧
       s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__headingWRTTrueNorth__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__headingWRTTrueNorth__m,s__Predicate) ∧
     s__headingWRTTrueNorth(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Woman) ∧
       s__instance(V__ROW2,s__Human) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__grandmother__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__grandmother__m,s__Predicate) ∧
     s__grandmother(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Position) ∧
       s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__leaderPosition__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__leaderPosition__m,s__Predicate) ∧
     s__leaderPosition(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__AreaOfConcern) ∧
       s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__organizationalObjective__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__organizationalObjective__m,s__Predicate) ∧
     s__organizationalObjective(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__NonnegativeInteger) ∧
       s__instance(V__ROW2,s__SetOrClass) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__cardinality__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__cardinality__m,s__Predicate) ∧
     s__cardinality(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Object) ∧
       s__instance(V__ROW2,s__Transfer) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__objectTransferred__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__objectTransferred__m,s__Predicate) ∧
     s__objectTransferred(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__SymbolicString) ∧
       s__instance(V__ROW2,s__Organization) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__aimOfOrganization__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__aimOfOrganization__m,s__Predicate) ∧
     s__aimOfOrganization(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__catalyst__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__catalyst__m,s__Predicate) ∧
     s__catalyst(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Formula) ∧
       s__instance(V__ROW2,s__CognitiveAgent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__believes__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__believes__m,s__Predicate) ∧
     s__believes(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__PlaneAngleMeasure) ∧
       s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__headingWRTMagneticNorth__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__headingWRTMagneticNorth__m,s__Predicate) ∧
     s__headingWRTMagneticNorth(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Human) ∧
       s__subclass(V__ROW4,s__MakingMusic) ∧
       s__instance(V__ROW2,s__MusicRecording) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__musician__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__musician__m,s__Predicate) ∧
     s__musician(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Human) ∧
       s__instance(V__ROW2,s__SymbolicString) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__humanName__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__humanName__m,s__Predicate) ∧
     s__humanName(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__RationalNumber) ∧
       s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__contrastRatio__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__contrastRatio__m,s__Predicate) ∧
     s__contrastRatio(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Object) ∧
       s__instance(V__ROW4,s__Object) ∧
       s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__between__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__between__m,s__Predicate) ∧
     s__between(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TimePoint) ∧
       s__instance(V__ROW2,s__Agreement) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__agreementExpirationDate__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__agreementExpirationDate__m,s__Predicate) ∧
     s__agreementExpirationDate(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__SetOrClass) ∧
       s__instance(V__ROW4,s__SetOrClass) ∧
       s__instance(V__ROW2,s__SetOrClass) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__classIntersection__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__classIntersection__m,s__Predicate) ∧
     s__classIntersection(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Human) ∧
       s__instance(V__ROW2,s__Demonstrating) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__attends__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__attends__m,s__Predicate) ∧
     s__attends(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Integer) ∧
       s__instance(V__ROW2,s__Organization) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__yearOfFounding__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__yearOfFounding__m,s__Predicate) ∧
     s__yearOfFounding(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Policy) ∧
       s__instance(V__ROW2,s__PricingScheme) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__pricePolicy__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__pricePolicy__m,s__Predicate) ∧
     s__pricePolicy(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Process) ∧
       s__instance(V__ROW2,s__HotelPackage) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__processInclusion__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__processInclusion__m,s__Predicate) ∧
     s__processInclusion(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW2,s__LegalAction) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__witness__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__witness__m,s__Predicate) ∧
     s__witness(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__FinancialAccount) ∧
       s__instance(V__ROW2,s__BankCard) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__cardAccount__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__cardAccount__m,s__Predicate) ∧
     s__cardAccount(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__ConstantQuantity) ∧
       s__instance(V__ROW2,s__SelfConnectedObject) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__capacity__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__capacity__m,s__Predicate) ∧
     s__capacity(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Physical) ∧
       s__instance(V__ROW2,s__GeographicArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__environmentalProblemTypeInArea__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__environmentalProblemTypeInArea__m,s__Predicate) ∧
     s__environmentalProblemTypeInArea(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Agent) ∧
       s__instance(V__ROW4,s__Agent) ∧
       s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__representativeAgentToAgent__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__representativeAgentToAgent__m,s__Predicate) ∧
     s__representativeAgentToAgent(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__SocialRole) ∧
       s__instance(V__ROW4,s__Agent) ∧
       s__instance(V__ROW2,s__Election) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__candidateForPosition__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__candidateForPosition__m,s__Predicate) ∧
     s__candidateForPosition(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__WebSite) ∧
       s__instance(V__ROW4,s__Collection) ∧
       s__instance(V__ROW2,s__TimeInterval) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__firstTimeSellers__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__firstTimeSellers__m,s__Predicate) ∧
     s__firstTimeSellers(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Holiday) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__nationalCelebration__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__nationalCelebration__m,s__Predicate) ∧
     s__nationalCelebration(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__GeographicArea) ∧
       s__instance(V__ROW2,s__GeographicArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__geographicSubregion__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__geographicSubregion__m,s__Predicate) ∧
     s__geographicSubregion(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Object) ∧
       s__instance(V__ROW2,s__Animal) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__deathplace__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__deathplace__m,s__Predicate) ∧
     s__deathplace(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Experimenting) ∧
       s__instance(V__ROW2,s__WebPage) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__treatedPage__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__treatedPage__m,s__Predicate) ∧
     s__treatedPage(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__SelfConnectedObject) ∧
       s__instance(V__ROW4,s__FunctionQuantity) ∧
       s__instance(V__ROW2,s__Transitway) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__transitwayCapacityRate__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__transitwayCapacityRate__m,s__Predicate) ∧
     s__transitwayCapacityRate(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TimeInterval) ∧
       s__instance(V__ROW2,s__TimeInterval) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__meetsTemporally__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__meetsTemporally__m,s__Predicate) ∧
     s__meetsTemporally(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__TimePosition) ∧
       s__instance(V__ROW4,s__Proposition) ∧
       s__instance(V__ROW2,s__Proposition) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__agreementRevisionDate__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__agreementRevisionDate__m,s__Predicate) ∧
     s__agreementRevisionDate(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Object) ∧
       s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__hasAward__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__hasAward__m,s__Predicate) ∧
     s__hasAward(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__LengthMeasure) ∧
       s__instance(V__ROW2,s__GeographicArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__lengthOfCrudeOilPipeline__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__lengthOfCrudeOilPipeline__m,s__Predicate) ∧
     s__lengthOfCrudeOilPipeline(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__MassMeasure) ∧
       s__instance(V__ROW2,s__SelfConnectedObject) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__weight__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__weight__m,s__Predicate) ∧
     s__weight(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Object) ∧
       s__instance(V__ROW2,s__Experimenting) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__experimentalControl__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__experimentalControl__m,s__Predicate) ∧
     s__experimentalControl(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__LengthMeasure) ∧
       s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__sphereRadius__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__sphereRadius__m,s__Predicate) ∧
     s__sphereRadius(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__PhysicalQuantity) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__annualElectricityConsumption__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__annualElectricityConsumption__m,s__Predicate) ∧
     s__annualElectricityConsumption(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__WebSite) ∧
       s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__confirmedRegisteredUser__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__confirmedRegisteredUser__m,s__Predicate) ∧
     s__confirmedRegisteredUser(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__DirectionalAttribute) ∧
       s__instance(V__ROW4,s__RealNumber) ∧
       s__instance(V__ROW2,s__LandArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__slopeGradientTowardsOrientation__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__slopeGradientTowardsOrientation__m,s__Predicate) ∧
     s__slopeGradientTowardsOrientation(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__SearchQuery) ∧
       s__instance(V__ROW2,s__SearchQuery) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__searchQueryRewrite__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__searchQueryRewrite__m,s__Predicate) ∧
     s__searchQueryRewrite(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__AreaMeasure) ∧
       s__instance(V__ROW2,s__GeographicArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__landAreaOnly__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__landAreaOnly__m,s__Predicate) ∧
     s__landAreaOnly(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Object) ∧
       s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__traverses__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__traverses__m,s__Predicate) ∧
     s__traverses(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__ConstantQuantity) ∧
       s__instance(V__ROW2,s__Precipitation) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__precipitationAmount__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__precipitationAmount__m,s__Predicate) ∧
     s__precipitationAmount(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__paidPropertyAmenity__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__paidPropertyAmenity__m,s__Predicate) ∧
     s__paidPropertyAmenity(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CognitiveAgent) ∧
       s__instance(V__ROW2,s__Human) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__patientMedical__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__patientMedical__m,s__Predicate) ∧
     s__patientMedical(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__ContentBearingPhysical) ∧
       s__instance(V__ROW4,s__Language) ∧
       s__instance(V__ROW2,s__SymbolicString) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__subtitle__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__subtitle__m,s__Predicate) ∧
     s__subtitle(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Interest) ∧
       s__instance(V__ROW2,s__Bond) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__accruedInterest__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__accruedInterest__m,s__Predicate) ∧
     s__accruedInterest(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TimePoint) ∧
       s__subclass(V__ROW2,s__Physical) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__firstInstanceCreated__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__firstInstanceCreated__m,s__Predicate) ∧
     s__firstInstanceCreated(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW4,s__CognitiveAgent) ∧
       s__subclass(V__ROW2,s__Entity) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__productPrice__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__productPrice__m,s__Predicate) ∧
     s__productPrice(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__relatedInternalConcept__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__relatedInternalConcept__m,s__Predicate) ∧
     s__relatedInternalConcept(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__BankCard) ∧
       s__instance(V__ROW2,s__SymbolicString) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__pin__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__pin__m,s__Predicate) ∧
     s__pin(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,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__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__disjointDecomposition__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__disjointDecomposition__m,s__Predicate) ∧
     s__disjointDecomposition__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5))

s__subclass(s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CorpuscularObject) ∧
       s__subclass(V__ROW2,s__Substance) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__material__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__material__m,s__Predicate) ∧
     s__material(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__subclass(V__ROW4,s__TimeInterval) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__annualExpendituresOfAreaInPeriod__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__annualExpendituresOfAreaInPeriod__m,s__Predicate) ∧
     s__annualExpendituresOfAreaInPeriod(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__UniformClothing) ∧
       s__instance(V__ROW2,s__Group) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__hasUniform__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__hasUniform__m,s__Predicate) ∧
     s__hasUniform(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__LexiconCategory) ∧
       s__instance(V__ROW4,s__SymbolicString) ∧
       s__instance(V__ROW2,s__SetOrClass) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__lexicon__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__lexicon__m,s__Predicate) ∧
     s__lexicon(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__ServiceProcess) ∧
       s__instance(V__ROW2,s__RoomInventory) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__allRoomsServiceAmenity__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__allRoomsServiceAmenity__m,s__Predicate) ∧
     s__allRoomsServiceAmenity(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__MusicalComposition) ∧
       s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__composer__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__composer__m,s__Predicate) ∧
     s__composer(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__FunctionQuantity) ∧
       s__subclass(V__ROW2,s__BiochemicalAgent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__effectiveDose__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__effectiveDose__m,s__Predicate) ∧
     s__effectiveDose(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__ComputerScreen) ∧
       s__instance(V__ROW2,s__GUIElement) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__screenOfGUIE__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__screenOfGUIE__m,s__Predicate) ∧
     s__screenOfGUIE(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__annualRevenuesOfArea__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__annualRevenuesOfArea__m,s__Predicate) ∧
     s__annualRevenuesOfArea(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__ClimateZone) ∧
       s__instance(V__ROW2,s__GeographicArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__climateTypeInArea__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__climateTypeInArea__m,s__Predicate) ∧
     s__climateTypeInArea(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__RealNumber) ∧
       s__instance(V__ROW2,s__RealNumber) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__approximateValue__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__approximateValue__m,s__Predicate) ∧
     s__approximateValue(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__catalyst__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__catalyst__m,s__Predicate) ∧
     s__catalyst(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))

s__subclass(s__ListOrderFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Human) ∧
       s__instance(V__ROW2,s__Experimenting) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__experimentalSubject__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__experimentalSubject__m,s__Predicate) ∧
     s__experimentalSubject(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Quantity) ∧
       s__subclass(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__defaultMinimumMeasure__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__defaultMinimumMeasure__m,s__Predicate) ∧
     s__defaultMinimumMeasure(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__totalGDP__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__totalGDP__m,s__Predicate) ∧
     s__totalGDP(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__TimeInterval) ∧
       s__instance(V__ROW2,s__GeographicArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__coldSeasonInArea__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__coldSeasonInArea__m,s__Predicate) ∧
     s__coldSeasonInArea(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW4,s__CognitiveAgent) ∧
       s__instance(V__ROW2,s__Formula) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__confersRight__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__confersRight__m,s__Predicate) ∧
     s__confersRight(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Policy) ∧
       s__instance(V__ROW2,s__RoomInventory) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__someRoomsPolicy__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__someRoomsPolicy__m,s__Predicate) ∧
     s__someRoomsPolicy(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__LengthMeasure) ∧
       s__instance(V__ROW2,s__GeographicArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__lengthOfStandardGaugeRailway__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__lengthOfStandardGaugeRailway__m,s__Predicate) ∧
     s__lengthOfStandardGaugeRailway(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW2,s__FinancialAccount) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__originalBalance__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__originalBalance__m,s__Predicate) ∧
     s__originalBalance(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__DiskDrive) ∧
       s__subclass(V__ROW2,s__ComputerDisk) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__diskTypeForDrive__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__diskTypeForDrive__m,s__Predicate) ∧
     s__diskTypeForDrive(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Agent) ∧
       s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__exportPartner__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__exportPartner__m,s__Predicate) ∧
     s__exportPartner(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Class) ∧
       s__instance(V__ROW2,s__Class) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__exhaustiveDecomposition__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__exhaustiveDecomposition__m,s__Predicate) ∧
     s__exhaustiveDecomposition__2(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,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__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__contraryAttribute__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__contraryAttribute__m,s__Predicate) ∧
     s__contraryAttribute__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))

s__subclass(s__ListOrderFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW2,s__Auctioning) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__reservePrice__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__reservePrice__m,s__Predicate) ∧
     s__reservePrice(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Agent) ∧
       s__instance(V__ROW2,s__PlacingUnderArrest) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__arrested__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__arrested__m,s__Predicate) ∧
     s__arrested(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__BankStatement) ∧
       s__instance(V__ROW2,s__FinancialAccount) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__lastStatement__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__lastStatement__m,s__Predicate) ∧
     s__lastStatement(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Human) ∧
       s__instance(V__ROW2,s__Human) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__spouse__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__spouse__m,s__Predicate) ∧
     s__spouse(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Human) ∧
       s__instance(V__ROW2,s__Human) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__coaches__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__coaches__m,s__Predicate) ∧
     s__coaches(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW2,s__HotelFunctionRoom) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__freeFunctionRoomAmenity__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__freeFunctionRoomAmenity__m,s__Predicate) ∧
     s__freeFunctionRoomAmenity(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Quantity) ∧
       s__instance(V__ROW2,s__Class) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__total__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__total__m,s__Predicate) ∧
     s__total(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CognitiveAgent) ∧
       s__instance(V__ROW2,s__CognitiveAgent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__customer__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__customer__m,s__Predicate) ∧
     s__customer(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__WebSite) ∧
       s__instance(V__ROW2,s__Database) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__userDatabase__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__userDatabase__m,s__Predicate) ∧
     s__userDatabase(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW4,s__Language) ∧
       s__instance(V__ROW2,s__SymbolicString) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__groupingTitle__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__groupingTitle__m,s__Predicate) ∧
     s__groupingTitle(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CognitiveAgent) ∧
       s__instance(V__ROW2,s__CognitiveAgent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__guest__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__guest__m,s__Predicate) ∧
     s__guest(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__LengthMeasure) ∧
       s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__linearExtent__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__linearExtent__m,s__Predicate) ∧
     s__linearExtent(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW2,s__FinancialAccount) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__totalBalance__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__totalBalance__m,s__Predicate) ∧
     s__totalBalance(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Integer) ∧
       s__instance(V__ROW2,s__Organization) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__seatsInOrganizationCount__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__seatsInOrganizationCount__m,s__Predicate) ∧
     s__seatsInOrganizationCount(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW2,s__Organism) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__fathersBrothersWife__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__fathersBrothersWife__m,s__Predicate) ∧
     s__fathersBrothersWife(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__GeopoliticalArea) ∧
       s__instance(V__ROW4,s__PositiveRealNumber) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__importPartnerByFraction__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__importPartnerByFraction__m,s__Predicate) ∧
     s__importPartnerByFraction(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__SocialRole) ∧
       s__instance(V__ROW4,s__SocialRole) ∧
       s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__roleApprovesRole__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__roleApprovesRole__m,s__Predicate) ∧
     s__roleApprovesRole(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Object) ∧
       s__instance(V__ROW4,s__Agent) ∧
       s__instance(V__ROW2,s__CurrencyMeasure) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__corkageFee__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__corkageFee__m,s__Predicate) ∧
     s__corkageFee(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TimePoint) ∧
       s__instance(V__ROW4,s__Agent) ∧
       s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__dateUsed__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__dateUsed__m,s__Predicate) ∧
     s__dateUsed(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__SymbolicString) ∧
       s__instance(V__ROW2,s__CodeMap) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__codeMapping__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__codeMapping__m,s__Predicate) ∧
     s__codeMapping(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TimeDuration) ∧
       s__instance(V__ROW2,s__ComputerPath) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__simpleDeadline__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__simpleDeadline__m,s__Predicate) ∧
     s__simpleDeadline(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__ComputerProgram) ∧
       s__instance(V__ROW2,s__ShutdownBlock) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__shutdownOf__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__shutdownOf__m,s__Predicate) ∧
     s__shutdownOf(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW2,s__FinancialAccount) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__lastStatementBalance__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__lastStatementBalance__m,s__Predicate) ∧
     s__lastStatementBalance(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW5,s__TimeInterval) ∧
       s__instance(V__ROW3,s__Organization) ∧
       s__instance(V__ROW4,s__CurrencyMeasure) ∧
       s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__grossMerchandiseSoldInPeriod__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__grossMerchandiseSoldInPeriod__m,s__Predicate) ∧
     s__grossMerchandiseSoldInPeriod(V__ROW2,V__ROW3,V__ROW4,V__ROW5))

s__subclass(s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Roadway) ∧
       s__instance(V__ROW2,s__PostalPlace) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__postStreet__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__postStreet__m,s__Predicate) ∧
     s__postStreet(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Process) ∧
       s__instance(V__ROW2,s__Experimenting) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__successEvent__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__successEvent__m,s__Predicate) ∧
     s__successEvent(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__length__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__length__m,s__Predicate) ∧
     s__length(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__GeopoliticalArea) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__internationalDispute__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__internationalDispute__m,s__Predicate) ∧
     s__internationalDispute(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW4,s__TimeInterval) ∧
       s__instance(V__ROW2,s__FinancialAccount) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__purchasesPerPeriod__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__purchasesPerPeriod__m,s__Predicate) ∧
     s__purchasesPerPeriod(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__subclass(V__ROW4,s__TimeInterval) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__externalDebtInPeriod__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__externalDebtInPeriod__m,s__Predicate) ∧
     s__externalDebtInPeriod(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Integer) ∧
       s__instance(V__ROW2,s__HotelReservation) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__numberOccupant__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__numberOccupant__m,s__Predicate) ∧
     s__numberOccupant(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__GUIElement) ∧
       s__instance(V__ROW2,s__UncoveringGraphicalWindow) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__guiElementUncovered__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__guiElementUncovered__m,s__Predicate) ∧
     s__guiElementUncovered(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__OrganicObject) ∧
       s__instance(V__ROW2,s__GeographicArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__bioindicatorForHabitat__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__bioindicatorForHabitat__m,s__Predicate) ∧
     s__bioindicatorForHabitat(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__List) ∧
       s__instance(V__ROW2,s__ComputerProgram) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__commandLineArguments__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__commandLineArguments__m,s__Predicate) ∧
     s__commandLineArguments(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__GeometricFigure) ∧
       s__instance(V__ROW2,s__GeometricPoint) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__pointOfFigure__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__pointOfFigure__m,s__Predicate) ∧
     s__pointOfFigure(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__GeopoliticalArea) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__geopoliticalSubdivision__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__geopoliticalSubdivision__m,s__Predicate) ∧
     s__geopoliticalSubdivision(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Reservation) ∧
       s__instance(V__ROW2,s__Physical) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__reservationChannel__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__reservationChannel__m,s__Predicate) ∧
     s__reservationChannel(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Proposition) ∧
       s__instance(V__ROW2,s__UserAccount) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__accountInformation__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__accountInformation__m,s__Predicate) ∧
     s__accountInformation(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Organization) ∧
       s__instance(V__ROW2,s__Election) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__electionForOrganization__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__electionForOrganization__m,s__Predicate) ∧
     s__electionForOrganization(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CognitiveAgent) ∧
       s__instance(V__ROW2,s__FinancialAccount) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__administrator__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__administrator__m,s__Predicate) ∧
     s__administrator(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__PhysicalQuantity) ∧
       s__subclass(V__ROW4,s__TimeInterval) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__electricityProductionInPeriod__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__electricityProductionInPeriod__m,s__Predicate) ∧
     s__electricityProductionInPeriod(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Physical) ∧
       s__instance(V__ROW4,s__PlaneAngleMeasure) ∧
       s__instance(V__ROW2,s__Physical) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__courseWRTCompassNorth__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__courseWRTCompassNorth__m,s__Predicate) ∧
     s__courseWRTCompassNorth(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__PermanentResidence) ∧
       s__instance(V__ROW2,s__Human) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__home__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__home__m,s__Predicate) ∧
     s__home(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__GeopoliticalArea) ∧
       s__instance(V__ROW2,s__Organization) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__headquartersOfOrganization__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__headquartersOfOrganization__m,s__Predicate) ∧
     s__headquartersOfOrganization(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Formula) ∧
       s__instance(V__ROW2,s__Experimenting) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__treatedPageDefinition__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__treatedPageDefinition__m,s__Predicate) ∧
     s__treatedPageDefinition(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Reservation) ∧
       s__instance(V__ROW2,s__TimePoint) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__reservationStart__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__reservationStart__m,s__Predicate) ∧
     s__reservationStart(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW2,s__SymbolicString) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__localShortName__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__localShortName__m,s__Predicate) ∧
     s__localShortName(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CognitiveAgent) ∧
       s__instance(V__ROW2,s__FinancialAccount) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__accountHolder__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__accountHolder__m,s__Predicate) ∧
     s__accountHolder(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Organization) ∧
       s__instance(V__ROW2,s__Organization) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__ancestorOrganization__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__ancestorOrganization__m,s__Predicate) ∧
     s__ancestorOrganization(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW4,s__Agreement) ∧
       s__subclass(V__ROW2,s__Entity) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__negotiatedPrice__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__negotiatedPrice__m,s__Predicate) ∧
     s__negotiatedPrice(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__FunctionQuantity) ∧
       s__instance(V__ROW4,s__Agreement) ∧
       s__subclass(V__ROW2,s__Physical) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__contractedRentalPrice__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__contractedRentalPrice__m,s__Predicate) ∧
     s__contractedRentalPrice(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Integer) ∧
       s__instance(V__ROW2,s__Integer) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__multiplicativeFactor__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__multiplicativeFactor__m,s__Predicate) ∧
     s__multiplicativeFactor(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TimeInterval) ∧
       s__instance(V__ROW2,s__Physical) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__anniversary__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__anniversary__m,s__Predicate) ∧
     s__anniversary(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW2,s__Process) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__destination__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__destination__m,s__Predicate) ∧
     s__destination(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__VolumeMeasure) ∧
       s__instance(V__ROW2,s__Engine) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__minCylinderVolume__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__minCylinderVolume__m,s__Predicate) ∧
     s__minCylinderVolume(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__DigitalData) ∧
       s__instance(V__ROW2,s__SymbolicString) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__filename__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__filename__m,s__Predicate) ∧
     s__filename(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW4,s__TimePosition) ∧
       s__instance(V__ROW2,s__FinancialAccount) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__amountDue__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__amountDue__m,s__Predicate) ∧
     s__amountDue(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Computer) ∧
       s__subclass(V__ROW2,s__ComputerProgram) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__canRunOn__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__canRunOn__m,s__Predicate) ∧
     s__canRunOn(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Artifact) ∧
       s__instance(V__ROW2,s__CorpuscularObject) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__powerComponent__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__powerComponent__m,s__Predicate) ∧
     s__powerComponent(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Man) ∧
       s__instance(V__ROW2,s__Human) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__grandfather__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__grandfather__m,s__Predicate) ∧
     s__grandfather(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Physical) ∧
       s__subclass(V__ROW2,s__HotelFunctionRoom) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__functionRoomAmenity__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__functionRoomAmenity__m,s__Predicate) ∧
     s__functionRoomAmenity(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Relation) ∧
       s__instance(V__ROW2,s__Relation) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__disjointRelation__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__disjointRelation__m,s__Predicate) ∧
     s__disjointRelation(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__RealNumber) ∧
       s__instance(V__ROW2,s__Experimenting) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__confidenceInterval__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__confidenceInterval__m,s__Predicate) ∧
     s__confidenceInterval(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__SetOrClass) ∧
       s__instance(V__ROW2,s__BinaryRelation) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__equivalenceRelationOn__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__equivalenceRelationOn__m,s__Predicate) ∧
     s__equivalenceRelationOn(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Month) ∧
       s__instance(V__ROW4,s__LengthMeasure) ∧
       s__instance(V__ROW2,s__GeographicArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__averageRainfallForPeriod__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__averageRainfallForPeriod__m,s__Predicate) ∧
     s__averageRainfallForPeriod(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Human) ∧
       s__instance(V__ROW2,s__Human) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__legalGuardian__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__legalGuardian__m,s__Predicate) ∧
     s__legalGuardian(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__SymbolicString) ∧
       s__instance(V__ROW2,s__Stock) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__stockSymbol__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__stockSymbol__m,s__Predicate) ∧
     s__stockSymbol(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Object) ∧
       s__instance(V__ROW2,s__Motion) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__path__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__path__m,s__Predicate) ∧
     s__path(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__processList__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__processList__m,s__Predicate) ∧
     s__processList__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5))

s__subclass(s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__ComputerDisplay) ∧
       s__instance(V__ROW2,s__Image) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__displayedUpon__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__displayedUpon__m,s__Predicate) ∧
     s__displayedUpon(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW5,s__TimeInterval) ∧
       s__instance(V__ROW3,s__GeopoliticalArea) ∧
       s__instance(V__ROW4,s__PositiveInteger) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__importPartnerByRankInPeriod__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__importPartnerByRankInPeriod__m,s__Predicate) ∧
     s__importPartnerByRankInPeriod(V__ROW2,V__ROW3,V__ROW4,V__ROW5))

s__subclass(s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__TimePoint) ∧
       s__instance(V__ROW2,s__Organization) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__checkInTime__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__checkInTime__m,s__Predicate) ∧
     s__checkInTime(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Agent) ∧
       s__instance(V__ROW4,s__NonnegativeInteger) ∧
       s__instance(V__ROW2,s__Organization) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__seatsHeldInOrganization__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__seatsHeldInOrganization__m,s__Predicate) ∧
     s__seatsHeldInOrganization(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW2,s__SymbolicString) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__acronym__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__acronym__m,s__Predicate) ∧
     s__acronym(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Weapon) ∧
       s__instance(V__ROW4,s__PositiveInteger) ∧
       s__instance(V__ROW2,s__MilitaryVehicle) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__weaponCarryingCapability__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__weaponCarryingCapability__m,s__Predicate) ∧
     s__weaponCarryingCapability(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TimeDuration) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__militaryAge__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__militaryAge__m,s__Predicate) ∧
     s__militaryAge(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW2,s__SymbolicString) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__conventionalLongName__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__conventionalLongName__m,s__Predicate) ∧
     s__conventionalLongName(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__EngineeringComponent) ∧
       s__instance(V__ROW2,s__EngineeringComponent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__engineeringSubcomponent__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__engineeringSubcomponent__m,s__Predicate) ∧
     s__engineeringSubcomponent(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__PhysicalQuantity) ∧
       s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__lowAltitudeWindSpeed__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__lowAltitudeWindSpeed__m,s__Predicate) ∧
     s__lowAltitudeWindSpeed(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Graph) ∧
       s__instance(V__ROW2,s__GraphElement) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__graphPart__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__graphPart__m,s__Predicate) ∧
     s__graphPart(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__PhysicalQuantity) ∧
       s__instance(V__ROW2,s__GeographicArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__totalBiomass__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__totalBiomass__m,s__Predicate) ∧
     s__totalBiomass(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__EnvironmentSoftwareAttribute) ∧
       s__instance(V__ROW2,s__ComputerProgram) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__environmentAttributes__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__environmentAttributes__m,s__Predicate) ∧
     s__environmentAttributes(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Formula) ∧
       s__instance(V__ROW2,s__CognitiveAgent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__desires__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__desires__m,s__Predicate) ∧
     s__desires(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__LengthMeasure) ∧
       s__instance(V__ROW2,s__GeographicArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__totalLandBoundary__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__totalLandBoundary__m,s__Predicate) ∧
     s__totalLandBoundary(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Human) ∧
       s__instance(V__ROW2,s__LegalAction) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__attorney__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__attorney__m,s__Predicate) ∧
     s__attorney(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__RealNumber) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__realGrowthRateOfGDP__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__realGrowthRateOfGDP__m,s__Predicate) ∧
     s__realGrowthRateOfGDP(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__PhysicalQuantity) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__annualElectricityExport__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__annualElectricityExport__m,s__Predicate) ∧
     s__annualElectricityExport(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Holiday) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__nationalHoliday__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__nationalHoliday__m,s__Predicate) ∧
     s__nationalHoliday(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Day) ∧
       s__instance(V__ROW2,s__Human) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__baptismdate__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__baptismdate__m,s__Predicate) ∧
     s__baptismdate(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__processList__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__processList__m,s__Predicate) ∧
     s__processList__2(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Day) ∧
       s__instance(V__ROW2,s__Bond) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__callDate__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__callDate__m,s__Predicate) ∧
     s__callDate(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Process) ∧
       s__instance(V__ROW4,s__GeographicArea) ∧
       s__instance(V__ROW2,s__Agent) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__areaOfResponsibility__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__areaOfResponsibility__m,s__Predicate) ∧
     s__areaOfResponsibility(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__WebSite) ∧
       s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__advertisedOn__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__advertisedOn__m,s__Predicate) ∧
     s__advertisedOn(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__DevelopmentalAttribute) ∧
       s__instance(V__ROW2,s__BiologicalProcess) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__lifeStageAchieved__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__lifeStageAchieved__m,s__Predicate) ∧
     s__lifeStageAchieved(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Computer) ∧
       s__subclass(V__ROW2,s__ComputerProgram) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__deviceOS__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__deviceOS__m,s__Predicate) ∧
     s__deviceOS(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW2,s__FinancialAccount) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__principalAmount__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__principalAmount__m,s__Predicate) ∧
     s__principalAmount(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Organism) ∧
       s__instance(V__ROW2,s__Organism) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__relative__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__relative__m,s__Predicate) ∧
     s__relative(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CognitiveAgent) ∧
       s__instance(V__ROW2,s__LegalAction) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__plaintiff__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__plaintiff__m,s__Predicate) ∧
     s__plaintiff(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Agent) ∧
       s__subclass(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__manufacturer__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__manufacturer__m,s__Predicate) ∧
     s__manufacturer(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__TimeDuration) ∧
       s__instance(V__ROW2,s__Recording) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__recordingLength__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__recordingLength__m,s__Predicate) ∧
     s__recordingLength(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__LengthMeasure) ∧
       s__instance(V__ROW2,s__OneDimensionalFigure) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__lineMeasure__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__lineMeasure__m,s__Predicate) ∧
     s__lineMeasure(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Policy) ∧
       s__instance(V__ROW2,s__RoomInventory) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__allRoomsPolicy__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__allRoomsPolicy__m,s__Predicate) ∧
     s__allRoomsPolicy(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__SymbolicString) ∧
       s__instance(V__ROW2,s__SymbolicString) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__keyName__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__keyName__m,s__Predicate) ∧
     s__keyName(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__GraphNode) ∧
       s__instance(V__ROW4,s__GraphArc) ∧
       s__instance(V__ROW2,s__GraphNode) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__links__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__links__m,s__Predicate) ∧
     s__links(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Agent) ∧
       s__instance(V__ROW2,s__StationaryArtifact) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__contractor__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__contractor__m,s__Predicate) ∧
     s__contractor(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Human) ∧
       s__instance(V__ROW4,s__Human) ∧
       s__instance(V__ROW2,s__Organization) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__subordinateInOrganization__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__subordinateInOrganization__m,s__Predicate) ∧
     s__subordinateInOrganization(V__ROW2,V__ROW3,V__ROW4))

s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Organization) ∧
       s__instance(V__ROW2,s__SymbolicString) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__organizationName__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__organizationName__m,s__Predicate) ∧
     s__organizationName(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Year) ∧
       s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__lastRenovation__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__lastRenovation__m,s__Predicate) ∧
     s__lastRenovation(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__ShapeAttribute) ∧
       s__instance(V__ROW2,s__Physical) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__shape__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__shape__m,s__Predicate) ∧
     s__shape(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Hole) ∧
       s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__properlyFills__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__properlyFills__m,s__Predicate) ∧
     s__properlyFills(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__CurrencyMeasure) ∧
       s__instance(V__ROW2,s__GeopoliticalArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__militaryExpendituresInUSDollars__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__militaryExpendituresInUSDollars__m,s__Predicate) ∧
     s__militaryExpendituresInUSDollars(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW2,s__Object) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__crosses__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__crosses__m,s__Predicate) ∧
     s__crosses(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Formula) ∧
       s__instance(V__ROW2,s__Reservation) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__rateDetail__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__rateDetail__m,s__Predicate) ∧
     s__rateDetail(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__productBrand__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__productBrand__m,s__Predicate) ∧
     s__productBrand(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__Object) ∧
       s__instance(V__ROW2,s__Organization) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__organizationProductType__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__organizationProductType__m,s__Predicate) ∧
     s__organizationProductType(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__instance(V__ROW3,s__Day) ∧
       s__instance(V__ROW2,s__FinancialAccount) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__maturityDate__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__maturityDate__m,s__Predicate) ∧
     s__maturityDate(V__ROW2,V__ROW3))

s__subclass(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,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__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__disjointDecomposition__m,V__NUMBER,V__CLASS)
     ∧
     s__instance(s__disjointDecomposition__m,s__Predicate) ∧
     s__disjointDecomposition__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))

s__subclass(s__ListOrderFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
,V__NUMBER)
,V__CLASS)
)
)

( ∀ [V__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   ((s__subclass(V__ROW3,s__TimeInterval) ∧
       s__instance(V__ROW2,s__GeographicArea) ∧
       s__instance(V__NUMBER,s__PositiveInteger) ∧
       s__instance(V__CLASS,s__SetOrClass))
     ⇒
     (s__domainSubclass(s__warmSeasonInArea__m,V__NUMBER,V__CLASS)
     ∧