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 131-133
s__domain(s__subclass__m,n__1,s__Class)

Merge.kif 129-129 The number 1 argument of subclass is an instance of class
s__domain(s__subclass__m,n__2,s__Class)

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

s__instance(s__BinaryPredicate,s__SetOrClass)

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

s__instance(s__PartialOrderingRelation,s__SetOrClass)

Merge.kif 128-128 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 5158-5158 subset is a subrelation of subclass
s__termFormat(s__ChineseLanguage,s__subclass__m,'"子类"')

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

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

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

domainEnglishFormat.kif 55680-55680

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


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

Hotel.kif 1151-1166
( ∀ [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__Class))
       ⇒
       (((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__Class) ∧
         s__subclass(V__PROCESS,s__Process) ∧
         s__instance(V__SUB,s__Class) ∧
         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__Class) ∧
         s__subclass(V__SUB,s__Organism) ∧
         s__instance(V__SUB,s__Class))
       ⇒
       (((s__biologicalAgentCarrier(V__AGENT,V__ORGANISM)
           ∧
           s__subclass(V__SUB,V__ORGANISM))
       ⇒
       (s__biologicalAgentCarrier(V__AGENT,V__SUB)))))
)
)

WMD.kif 964-968
( ∀ [V__PC,V__MV,V__ROLE]
   (((s__instance(V__PC,s__Class) ∧
         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__Class) ∧
         s__instance(V__AREA,s__GeopoliticalArea))
       ⇒
       (((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__Class) ∧
         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 484-500
No TPTP formula. May not be expressible in strict first order. Hotel.kif 502-518
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11799-11810
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11768-11779
( ∀ [V__PROCESS,V__SUBSTANCE,V__DISEASE,V__SUB]
   (((s__instance(V__PROCESS,s__Class) ∧
         s__subclass(V__PROCESS,s__Process) ∧
         s__subclass(V__SUBSTANCE,s__BiologicallyActiveSubstance) ∧
         s__instance(V__DISEASE,s__DiseaseOrSyndrome) ∧
         s__instance(V__SUB,s__Class) ∧
         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 945-949
( ∀ [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__Class) ∧
         s__instance(V__DISEASE,s__DiseaseOrSyndrome) ∧
         s__subclass(V__SUB,s__BiologicallyActiveSubstance) ∧
         s__instance(V__SUB,s__Class))
       ⇒
       (((s__diseaseTreatment(V__DISEASE,V__SUBSTANCE,V__PROCESS)
           ∧
           s__subclass(V__SUB,V__SUBSTANCE))
       ⇒
       (s__diseaseTreatment(V__DISEASE,V__SUB,V__PROCESS)))))
)
)

WMD.kif 951-955
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__Class) ∧
         s__subclass(V__CLASS1,s__Getting) ∧
         s__instance(V__CLASS1,s__Class) ∧
         s__subclass(V__OBJCLASS2,s__Object) ∧
         s__instance(V__OBJCLASS2,s__Class) ∧
         s__subclass(V__OBJCLASS1,s__Object) ∧
         s__instance(V__OBJCLASS1,s__Class))
       ⇒
       ((((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__Process) ∧
         s__instance(V__PHYS,s__Class) ∧
         s__subclass(V__PHYS,s__Process) ∧
         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 16415-16419
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 16421-16430
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__Class) ∧
         s__subclass(V__ROOM,s__HotelUnit) ∧
         s__instance(V__OBJ,s__Class) ∧
         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__Class) ∧
         s__subclass(V__ROOM,s__HotelUnit) ∧
         s__instance(V__S,s__Process) ∧
         s__instance(V__PROC,s__Class) ∧
         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 790-811
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__O,V__R,V__OC,V__DC]
   (((s__instance(V__O,s__Object) ∧
         s__instance(V__R,s__Relation) ∧
         s__instance(V__OC,s__Class) ∧
         s__instance(V__DC,s__Class))
       ⇒
       (((s__applicableRelation(V__O,V__R)
           ∧
           s__instance(V__O,V__OC)
         ∧
         s__domain(V__R,n__1,V__DC))
     ⇒
     (((V__OC = V__DC)
         ∨
         s__subclass(V__OC,V__DC))))))
)
)

Mid-level-ontology.kif 29345-29352
( ∀ [V__CLASS2,V__CLASS1,V__REL,V__NUMBER]
   (((s__instance(V__CLASS2,s__Class) ∧
         s__instance(V__CLASS1,s__Class) ∧
         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__CareOrganization) ∧
         s__instance(V__ROW2,s__Human) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__medicalPatient__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__medicalPatient__m,s__Predicate) ∧
           s__medicalPatient(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__Class))
       ⇒
       (((s__domainSubclass(s__refers__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__refers__m,s__Predicate) ∧
           s__refers(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__Attribute) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__contraryAttribute__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__contraryAttribute__m,s__Predicate) ∧
           s__contraryAttribute__2(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__UnitOfMeasure) ∧
         s__instance(V__ROW6,s__SymbolicString) ∧
         s__subclass(V__ROW3,s__ComputerComponent) ∧
         s__instance(V__ROW4,s__ComputerComponent) ∧
         s__instance(V__ROW2,s__TimePosition) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__componentDataID__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__componentDataID__m,s__Predicate) ∧
           s__componentDataID(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__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   (((s__instance(V__ROW3,s__RealNumber) ∧
         s__subclass(V__ROW4,s__TimeInterval) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__realGrowthRateOfGDPInPeriod__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__realGrowthRateOfGDPInPeriod__m,s__Predicate) ∧
           s__realGrowthRateOfGDPInPeriod(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__subclass(V__ROW2,s__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__defaultMeasure__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__defaultMeasure__m,s__Predicate) ∧
           s__defaultMeasure(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__Agent) ∧
         s__instance(V__ROW2,s__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__bidPrice__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__bidPrice__m,s__Predicate) ∧
           s__bidPrice(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__GeopoliticalArea) ∧
         s__instance(V__ROW4,s__PositiveInteger) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__TimePosition) ∧
         s__instance(V__ROW2,s__Human) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__compensationPackage__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__compensationPackage__m,s__Predicate) ∧
           s__compensationPackage(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__TelecomNumber) ∧
         s__instance(V__ROW2,s__SymbolicString) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__telecomExtension__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__telecomExtension__m,s__Predicate) ∧
           s__telecomExtension(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__subclass(V__ROW4,s__TimeInterval) ∧
         s__instance(V__ROW2,s__Agent) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__importPartnerInPeriod__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__importPartnerInPeriod__m,s__Predicate) ∧
           s__importPartnerInPeriod(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__Class))
       ⇒
       (((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__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__Class))
       ⇒
       (((s__domainSubclass(s__populationFractionBelowPovertyLine__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__populationFractionBelowPovertyLine__m,s__Predicate) ∧
           s__populationFractionBelowPovertyLine(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__Transportation) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__transported__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__transported__m,s__Predicate) ∧
           s__transported(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__TimeInterval) ∧
         s__instance(V__ROW4,s__FunctionQuantity) ∧
         s__instance(V__ROW2,s__GeographicArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__rainfallIntensity__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__rainfallIntensity__m,s__Predicate) ∧
           s__rainfallIntensity(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__SoftwareSystem) ∧
         s__instance(V__ROW2,s__ResourceManagementProgram) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__rMProgramOf__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__rMProgramOf__m,s__Predicate) ∧
           s__rMProgramOf(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__EngineeringComponent) ∧
         s__subclass(V__ROW2,s__ComputerProtocol) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__protocolForConnector__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__protocolForConnector__m,s__Predicate) ∧
           s__protocolForConnector(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__Object) ∧
         s__subclass(V__ROW4,s__PositiveInteger) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__agriculturalProductTypeByRank__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__agriculturalProductTypeByRank__m,s__Predicate) ∧
           s__agriculturalProductTypeByRank(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__Agent) ∧
         s__instance(V__ROW4,s__Abstract) ∧
         s__instance(V__ROW2,s__Game) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__achievement__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__achievement__m,s__Predicate) ∧
           s__achievement(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__TimeDuration) ∧
         s__instance(V__ROW4,s__NonnegativeRealNumber) ∧
         s__instance(V__ROW2,s__GeographicArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__overcastDaysInPeriod__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__overcastDaysInPeriod__m,s__Predicate) ∧
           s__overcastDaysInPeriod(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__WaterArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__ROW2,s__SymbolicString) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__fullName__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__fullName__m,s__Predicate) ∧
           s__fullName(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__Class))
       ⇒
       (((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__instance(V__ROW3,s__GUIElement) ∧
         s__instance(V__ROW2,s__UncoveringGraphicalWindow) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__ROW5,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   (((s__instance(V__ROW5,s__GeographicArea) ∧
         s__instance(V__ROW3,s__BinaryRelationExtendedToQuantities) ∧
         s__instance(V__ROW4,s__PositiveRealNumber) ∧
         s__instance(V__ROW2,s__GeographicArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__comparativeArea__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__comparativeArea__m,s__Predicate) ∧
           s__comparativeArea(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__TaskRelationAttribute) ∧
         s__instance(V__ROW2,s__RealtimeSystem) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__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__Class))
       ⇒
       (((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__ROW2,V__NUMBER,V__CLASS]
   (((s__instance(V__ROW3,s__Position) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__chiefOfStateType__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__chiefOfStateType__m,s__Predicate) ∧
           s__chiefOfStateType(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__Class))
       ⇒
       (((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__LengthMeasure) ∧
         s__instance(V__ROW2,s__GeographicArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__meanSeaLevel__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__meanSeaLevel__m,s__Predicate) ∧
           s__meanSeaLevel(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__TimePosition) ∧
         s__instance(V__ROW2,s__Proposition) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__agreementAdoptionDate__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__agreementAdoptionDate__m,s__Predicate) ∧
           s__agreementAdoptionDate(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__Organization) ∧
         s__instance(V__ROW4,s__Agent) ∧
         s__instance(V__ROW2,s__Agent) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__diplomaticOrganizationType__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__diplomaticOrganizationType__m,s__Predicate) ∧
           s__diplomaticOrganizationType(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__SelfConnectedObject) ∧
         s__instance(V__ROW2,s__SelfConnectedObject) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__bottom__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__bottom__m,s__Predicate) ∧
           s__bottom(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__RatingAttribute) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__ratingsAgent__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__ratingsAgent__m,s__Predicate) ∧
           s__ratingsAgent(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__Class))
       ⇒
       (((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__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__annualElectricityProduction__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__annualElectricityProduction__m,s__Predicate) ∧
           s__annualElectricityProduction(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__PositiveRealNumber) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__importPartnerByFractionInPeriod__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__importPartnerByFractionInPeriod__m,s__Predicate) ∧
           s__importPartnerByFractionInPeriod(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__PositiveRealNumber) ∧
         s__instance(V__ROW2,s__Computer) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__thresholdOf__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__thresholdOf__m,s__Predicate) ∧
           s__thresholdOf(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__PartiallyCoveringGraphicalWindow) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__guiElementPartiallyCovered__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__guiElementPartiallyCovered__m,s__Predicate) ∧
           s__guiElementPartiallyCovered(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__Class))
       ⇒
       (((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__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__Class))
       ⇒
       (((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__ROW2,s__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__most__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__most__m,s__Predicate) ∧
           s__most(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__Class))
       ⇒
       (((s__domainSubclass(s__chamberOfLegislature__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__chamberOfLegislature__m,s__Predicate) ∧
           s__chamberOfLegislature(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__Class))
       ⇒
       (((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__ROW2,V__NUMBER,V__CLASS]
   (((s__subclass(V__ROW3,s__Object) ∧
         s__instance(V__ROW2,s__Process) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__resultType__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__resultType__m,s__Predicate) ∧
           s__resultType(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__Collection) ∧
         s__instance(V__ROW2,s__ContentBearingObject) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__inventory__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__inventory__m,s__Predicate) ∧
           s__inventory(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__Class))
       ⇒
       (((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__Object) ∧
         s__instance(V__ROW2,s__SelfConnectedObject) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__contains__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__contains__m,s__Predicate) ∧
           s__contains(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__Music) ∧
         s__instance(V__ROW2,s__MusicRecording) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__musicInterpretation__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__musicInterpretation__m,s__Predicate) ∧
           s__musicInterpretation(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__Class))
       ⇒
       (((s__domainSubclass(s__resource__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__resource__m,s__Predicate) ∧
           s__resource(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__Class))
       ⇒
       (((s__domainSubclass(s__approves__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__approves__m,s__Predicate) ∧
           s__approves(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__RadiationMeasure) ∧
         s__instance(V__ROW2,s__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__absorbedDose__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__absorbedDose__m,s__Predicate) ∧
           s__absorbedDose(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__Class))
       ⇒
       (((s__domainSubclass(s__coolSeasonInArea__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__coolSeasonInArea__m,s__Predicate) ∧
           s__coolSeasonInArea(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__FormOfGovernment) ∧
         s__instance(V__ROW2,s__Organization) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__ideologicalAffiliationOfOrganization__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__ideologicalAffiliationOfOrganization__m,s__Predicate) ∧
           s__ideologicalAffiliationOfOrganization(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__Formula) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__holdsObligation__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__holdsObligation__m,s__Predicate) ∧
           s__holdsObligation(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__AchievingControl) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__controlled__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__controlled__m,s__Predicate) ∧
           s__controlled(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__Class))
       ⇒
       (((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__LengthMeasure) ∧
         s__instance(V__ROW2,s__SelfConnectedObject) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__height__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__height__m,s__Predicate) ∧
           s__height(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__Class))
       ⇒
       (((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__subclass(V__ROW3,s__ServiceProcess) ∧
         s__instance(V__ROW2,s__RoomInventory) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__instance(V__ROW3,s__GroupOfPeople) ∧
         s__instance(V__ROW2,s__Human) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__groupMember__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__groupMember__m,s__Predicate) ∧
           s__groupMember(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__Human) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__income__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__income__m,s__Predicate) ∧
           s__income(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__Reservation) ∧
         s__instance(V__ROW2,s__TimePoint) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__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__Class))
       ⇒
       (((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__ROW3,s__CurrencyMeasure) ∧
         s__instance(V__ROW2,s__Collateral) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__appraisedValue__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__appraisedValue__m,s__Predicate) ∧
           s__appraisedValue(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__Attribute) ∧
         s__instance(V__ROW4,s__BinaryPredicate) ∧
         s__instance(V__ROW2,s__Attribute) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__contraryAttributeWRT__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__contraryAttributeWRT__m,s__Predicate) ∧
           s__contraryAttributeWRT(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__TimePoint) ∧
         s__instance(V__ROW2,s__TimePoint) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__temporallyBetween__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__temporallyBetween__m,s__Predicate) ∧
           s__temporallyBetween(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__Collection) ∧
         s__instance(V__ROW4,s__TimePosition) ∧
         s__instance(V__ROW2,s__SelfConnectedObject) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__memberAtTime__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__memberAtTime__m,s__Predicate) ∧
           s__memberAtTime(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__Year) ∧
         s__instance(V__ROW2,s__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__yearBuilt__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__yearBuilt__m,s__Predicate) ∧
           s__yearBuilt(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__Sentence) ∧
         s__instance(V__ROW2,s__NounPhrase) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__sententialSubject__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__sententialSubject__m,s__Predicate) ∧
           s__sententialSubject(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__Class))
       ⇒
       (((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__ROW3,s__CrossFunctionalTeam) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__crossFunctionalTeamFocus__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__crossFunctionalTeamFocus__m,s__Predicate) ∧
           s__crossFunctionalTeamFocus(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__Class))
       ⇒
       (((s__domainSubclass(s__relatedExternalConcept__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__relatedExternalConcept__m,s__Predicate) ∧
           s__relatedExternalConcept(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__FinancialAccount) ∧
         s__instance(V__ROW2,s__Check) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__checkAccount__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__checkAccount__m,s__Predicate) ∧
           s__checkAccount(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__Agent) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__activityCapability__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__activityCapability__m,s__Predicate) ∧
           s__activityCapability(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__Class))
       ⇒
       (((s__domainSubclass(s__lengthOfUnpavedHighway__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__lengthOfUnpavedHighway__m,s__Predicate) ∧
           s__lengthOfUnpavedHighway(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__Discography) ∧
         s__instance(V__ROW2,s__CognitiveAgent) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__discography__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__discography__m,s__Predicate) ∧
           s__discography(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__Device) ∧
         s__instance(V__ROW2,s__Artifact) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__equipmentType__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__equipmentType__m,s__Predicate) ∧
           s__equipmentType(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__instance(V__ROW4,s__DirectionalAttribute) ∧
         s__instance(V__ROW2,s__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__surfaceWindVelocity__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__surfaceWindVelocity__m,s__Predicate) ∧
           s__surfaceWindVelocity(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__ROW2,s__SymbolicString) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__subsumingExternalConcept__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__subsumingExternalConcept__m,s__Predicate) ∧
           s__subsumingExternalConcept(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__Agent) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__enemy__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__enemy__m,s__Predicate) ∧
           s__enemy(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__Physical) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__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__Class))
       ⇒
       (((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__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__Class))
       ⇒
       (((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__Organization) ∧
         s__instance(V__ROW2,s__Organization) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__GeopoliticalArea) ∧
         s__instance(V__ROW4,s__PositiveInteger) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__exportPartnerByRank__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__exportPartnerByRank__m,s__Predicate) ∧
           s__exportPartnerByRank(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__Circle) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__Proposition) ∧
         s__instance(V__ROW2,s__Reservation) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__reservedPackage__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__reservedPackage__m,s__Predicate) ∧
           s__reservedPackage(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__Class))
       ⇒
       (((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__subclass(V__ROW3,s__IntentionalProcess) ∧
         s__instance(V__ROW2,s__IndustryAttribute) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__industryServiceType__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__industryServiceType__m,s__Predicate) ∧
           s__industryServiceType(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__IllicitDrug) ∧
         s__instance(V__ROW4,s__GeopoliticalArea) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__illicitDrugShipmentDestination__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__illicitDrugShipmentDestination__m,s__Predicate) ∧
           s__illicitDrugShipmentDestination(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__LegalAction) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__NonnegativeRealNumber) ∧
         s__instance(V__ROW2,s__LandArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__slopeGradient__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__slopeGradient__m,s__Predicate) ∧
           s__slopeGradient(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__Loan) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__loanInterest__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__loanInterest__m,s__Predicate) ∧
           s__loanInterest(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__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__viewType__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__viewType__m,s__Predicate) ∧
           s__viewType(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__PowerSource) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__voltageMeasure__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__voltageMeasure__m,s__Predicate) ∧
           s__voltageMeasure(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__Class) ∧
         s__instance(V__ROW4,s__Class) ∧
         s__instance(V__ROW2,s__Class) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__exhaustiveDecomposition__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__exhaustiveDecomposition__m,s__Predicate) ∧
           s__exhaustiveDecomposition__3(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__Organization) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__legislativeBranch__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__legislativeBranch__m,s__Predicate) ∧
           s__legislativeBranch(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__IntentionalProcess) ∧
         s__instance(V__ROW2,s__Organization) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__organizationServiceType__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__organizationServiceType__m,s__Predicate) ∧
           s__organizationServiceType(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__GeographicArea) ∧
         s__instance(V__ROW4,s__LengthMeasure) ∧
         s__instance(V__ROW2,s__GeographicArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__sharedBorderLength__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__sharedBorderLength__m,s__Predicate) ∧
           s__sharedBorderLength(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__Abstract) ∧
         s__instance(V__ROW2,s__Agent) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__offers__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__offers__m,s__Predicate) ∧
           s__offers(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__AmbienceAttribute) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__dressCode__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__dressCode__m,s__Predicate) ∧
           s__dressCode(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__Class))
       ⇒
       (((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__PhysicalQuantity) ∧
         s__instance(V__ROW2,s__WaterVehicle) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__vesselDisplacement__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__vesselDisplacement__m,s__Predicate) ∧
           s__vesselDisplacement(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__ROW2,s__SymbolicString) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__subsumedExternalConcept__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__subsumedExternalConcept__m,s__Predicate) ∧
           s__subsumedExternalConcept(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__Organism) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__mothersSistersHusband__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__mothersSistersHusband__m,s__Predicate) ∧
           s__mothersSistersHusband(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__TelecomNumber) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__personalPhoneNumber__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__personalPhoneNumber__m,s__Predicate) ∧
           s__personalPhoneNumber(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__instance(V__ROW2,s__CognitiveAgent) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__checkOutTime__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__checkOutTime__m,s__Predicate) ∧
           s__checkOutTime(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__Class))
       ⇒
       (((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__TimeDuration) ∧
         s__instance(V__ROW2,s__ComputerPath) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__batchInterArrival__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__batchInterArrival__m,s__Predicate) ∧
           s__batchInterArrival(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__Class))
       ⇒
       (((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__ROW3,V__ROW2,V__NUMBER,V__CLASS]
   (((s__instance(V__ROW2,s__SymbolicString) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__subclass(V__ROW3,s__Year) ∧
         s__instance(V__ROW2,s__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__TimeDuration) ∧
         s__instance(V__ROW2,s__Recording) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__Woman) ∧
         s__instance(V__ROW2,s__Human) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__stepmother__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__stepmother__m,s__Predicate) ∧
           s__stepmother(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__Class))
       ⇒
       (((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__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__immediateInstance__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__immediateInstance__m,s__Predicate) ∧
           s__immediateInstance(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__TerrainAttribute) ∧
         s__instance(V__ROW2,s__GeographicArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__terrainInArea__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__terrainInArea__m,s__Predicate) ∧
           s__terrainInArea(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__PlacingUnderArrest) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__arrestingOfficer__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__arrestingOfficer__m,s__Predicate) ∧
           s__arrestingOfficer(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__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__uses__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__uses__m,s__Predicate) ∧
           s__uses(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__Album) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__albumArtist__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__albumArtist__m,s__Predicate) ∧
           s__albumArtist(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__Class))
       ⇒
       (((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__Collection) ∧
         s__instance(V__ROW2,s__Physical) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__member__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__member__m,s__Predicate) ∧
           s__member(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__Class))
       ⇒
       (((s__domainSubclass(s__conversionEvent__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__conversionEvent__m,s__Predicate) ∧
           s__conversionEvent(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__UniformResourceLocator) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__urlString__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__urlString__m,s__Predicate) ∧
           s__urlString(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__TimeDuration) ∧
         s__instance(V__ROW4,s__ConstantQuantity) ∧
         s__instance(V__ROW2,s__GeographicArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__averagePrecipitationForPeriod__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__averagePrecipitationForPeriod__m,s__Predicate) ∧
           s__averagePrecipitationForPeriod(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__TimeDuration) ∧
         s__instance(V__ROW4,s__TemperatureMeasure) ∧
         s__instance(V__ROW2,s__GeographicArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__highestTemperatureForPeriod__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__highestTemperatureForPeriod__m,s__Predicate) ∧
           s__highestTemperatureForPeriod(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__ComputerProtocol) ∧
         s__instance(V__ROW2,s__ComputerProgram) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__implementsProtocol__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__implementsProtocol__m,s__Predicate) ∧
           s__implementsProtocol(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__SymbolicString) ∧
         s__instance(V__ROW4,s__SymbolicString) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__comment__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__comment__m,s__Predicate) ∧
           s__comment(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__FinancialAccount) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__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__Class))
       ⇒
       (((s__domainSubclass(s__electricityConsumptionInPeriod__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__electricityConsumptionInPeriod__m,s__Predicate) ∧
           s__electricityConsumptionInPeriod(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__GeographicArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__lengthOfPavedHighway__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__lengthOfPavedHighway__m,s__Predicate) ∧
           s__lengthOfPavedHighway(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__Class))
       ⇒
       (((s__domainSubclass(s__son__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__son__m,s__Predicate) ∧
           s__son(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__TimePosition) ∧
         s__instance(V__ROW2,s__Proposition) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__dateOpenedForSignature__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__dateOpenedForSignature__m,s__Predicate) ∧
           s__dateOpenedForSignature(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__MonitoringProgram) ∧
         s__instance(V__ROW4,s__Quantity) ∧
         s__instance(V__ROW2,s__ComputationalSystem) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__benchmarkPerformance__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__benchmarkPerformance__m,s__Predicate) ∧
           s__benchmarkPerformance(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__WearableItem) ∧
         s__instance(V__ROW2,s__Animal) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__wears__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__wears__m,s__Predicate) ∧
           s__wears(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__Class))
       ⇒
       (((s__domainSubclass(s__mother__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__mother__m,s__Predicate) ∧
           s__mother(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__IndustryAttribute) ∧
         s__instance(V__ROW4,s__PositiveInteger) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__industryRankByOutput__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__industryRankByOutput__m,s__Predicate) ∧
           s__industryRankByOutput(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__FinancialTransaction) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__transactionAmount__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__transactionAmount__m,s__Predicate) ∧
           s__transactionAmount(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__Class))
       ⇒
       (((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__Hole) ∧
         s__instance(V__ROW2,s__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__fills__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__fills__m,s__Predicate) ∧
           s__fills(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__Class))
       ⇒
       (((s__domainSubclass(s__maternalAunt__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__maternalAunt__m,s__Predicate) ∧
           s__maternalAunt(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__Class))
       ⇒
       (((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__ROW3,s__PermanentResidence) ∧
         s__instance(V__ROW2,s__Agent) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__landlord__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__landlord__m,s__Predicate) ∧
           s__landlord(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__Radiating) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__wavelength__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__wavelength__m,s__Predicate) ∧
           s__wavelength(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__Loan) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__borrower__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__borrower__m,s__Predicate) ∧
           s__borrower(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__Class))
       ⇒
       (((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__Translocation) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__changesLocation__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__changesLocation__m,s__Predicate) ∧
           s__changesLocation(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__Human) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__treatedUser__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__treatedUser__m,s__Predicate) ∧
           s__treatedUser(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__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__Class))
       ⇒
       (((s__domainSubclass(s__contraryAttribute__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__contraryAttribute__m,s__Predicate) ∧
           s__contraryAttribute__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__instance(V__ROW3,s__Human) ∧
         s__instance(V__ROW2,s__Human) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__domesticPartner__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__domesticPartner__m,s__Predicate) ∧
           s__domesticPartner(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__ComputerProcess) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__computerRunning__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__computerRunning__m,s__Predicate) ∧
           s__computerRunning(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__Class))
       ⇒
       (((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__ComputerProcess) ∧
         s__instance(V__ROW2,s__Abort) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__processAborted__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__processAborted__m,s__Predicate) ∧
           s__processAborted(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__Class))
       ⇒
       (((s__domainSubclass(s__primaryGeopoliticalSubdivision__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__primaryGeopoliticalSubdivision__m,s__Predicate) ∧
           s__primaryGeopoliticalSubdivision(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__Agent) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__viewedItemList__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__viewedItemList__m,s__Predicate) ∧
           s__viewedItemList(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__Substance) ∧
         s__instance(V__ROW2,s__ChemicalProcess) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__reagent__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__reagent__m,s__Predicate) ∧
           s__reagent(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__Virus) ∧
         s__instance(V__ROW2,s__ViralCellInvasion) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__invadingVirus__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__invadingVirus__m,s__Predicate) ∧
           s__invadingVirus(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__Class))
       ⇒
       (((s__domainSubclass(s__familyRelation__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__familyRelation__m,s__Predicate) ∧
           s__familyRelation(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__Class))
       ⇒
       (((s__domainSubclass(s__hotSeasonInArea__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__hotSeasonInArea__m,s__Predicate) ∧
           s__hotSeasonInArea(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__Class))
       ⇒
       (((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__ROW2,V__NUMBER,V__CLASS]
   (((s__instance(V__ROW2,s__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__third__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__third__m,s__Predicate) ∧
           s__third(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__MealPlan) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__includedMeal__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__includedMeal__m,s__Predicate) ∧
           s__includedMeal(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__FinancialTransaction) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__eCommerceSite__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__eCommerceSite__m,s__Predicate) ∧
           s__eCommerceSite(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__Class))
       ⇒
       (((s__domainSubclass(s__minDeviceStorageTemp__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__minDeviceStorageTemp__m,s__Predicate) ∧
           s__minDeviceStorageTemp(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__Class))
       ⇒
       (((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__Class) ∧
         s__instance(V__ROW2,s__BinaryRelation) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__partialOrderingOn__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__partialOrderingOn__m,s__Predicate) ∧
           s__partialOrderingOn(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__Formula) ∧
         s__instance(V__ROW4,s__RealNumber) ∧
         s__instance(V__ROW2,s__Formula) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__conditionalProbability__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__conditionalProbability__m,s__Predicate) ∧
           s__conditionalProbability(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__FunctionQuantity) ∧
         s__instance(V__ROW2,s__SpeedGovernor) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__governorSpeed__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__governorSpeed__m,s__Predicate) ∧
           s__governorSpeed(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__Man) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__brother__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__brother__m,s__Predicate) ∧
           s__brother(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__Class))
       ⇒
       (((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__subclass(V__ROW3,s__Substance) ∧
         s__instance(V__ROW2,s__LandArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__groundSurfaceType__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__groundSurfaceType__m,s__Predicate) ∧
           s__groundSurfaceType(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__Process) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__hinders__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__hinders__m,s__Predicate) ∧
           s__hinders(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__Class))
       ⇒
       (((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__Attribute) ∧
         s__instance(V__ROW2,s__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__instance(V__ROW3,s__RealNumber) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__lowestDecileShareOfHouseholdIncome__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__lowestDecileShareOfHouseholdIncome__m,s__Predicate) ∧
           s__lowestDecileShareOfHouseholdIncome(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__instance(V__ROW2,s__Agreement) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__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__Class))
       ⇒
       (((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__Agent) ∧
         s__instance(V__ROW2,s__SymbolicString) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__dayPhone__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__dayPhone__m,s__Predicate) ∧
           s__dayPhone(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__Class))
       ⇒
       (((s__domainSubclass(s__grandparent__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__grandparent__m,s__Predicate) ∧
           s__grandparent(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__Class))
       ⇒
       (((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__ROW4,s__SymbolicString) ∧
         s__instance(V__ROW2,s__Language) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__termFormat__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__termFormat__m,s__Predicate) ∧
           s__termFormat(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__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   (((s__instance(V__ROW7,s__Attribute) ∧
         s__instance(V__ROW8,s__Attribute) ∧
         s__instance(V__ROW5,s__Attribute) ∧
         s__instance(V__ROW6,s__Attribute) ∧
         s__instance(V__ROW3,s__Attribute) ∧
         s__instance(V__ROW4,s__Attribute) ∧
         s__subclass(V__ROW2,s__Attribute) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__exhaustiveAttribute__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__exhaustiveAttribute__m,s__Predicate) ∧
           s__exhaustiveAttribute__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__ROW2,s__CriminalAction) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__perpetrator__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__perpetrator__m,s__Predicate) ∧
           s__perpetrator(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__ComputerResponse) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__responseRate__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__responseRate__m,s__Predicate) ∧
           s__responseRate(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__UserAccount) ∧
         s__instance(V__ROW2,s__ComputerProcess) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__accountUsed__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__accountUsed__m,s__Predicate) ∧
           s__accountUsed(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__TimePosition) ∧
         s__instance(V__ROW4,s__Object) ∧
         s__instance(V__ROW2,s__SentientAgent) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__detainedAtTimeInPlace__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__detainedAtTimeInPlace__m,s__Predicate) ∧
           s__detainedAtTimeInPlace(V__ROW2,V__ROW3,V__ROW4))
       ⇒
       (s__subclass(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
      ,V__NUMBER)
    ,V__CLASS)))))
)
)

( ∀ [V__ROW2,V__NUMBER,V__CLASS]
   (((s__instance(V__ROW2,s__Attribute) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__contraryAttribute__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__contraryAttribute__m,s__Predicate) ∧
           s__contraryAttribute__1(V__ROW2))
       ⇒
       (s__subclass(s__ListOrderFn(s__ListFn__1Fn(V__ROW2)
      ,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__Class))
       ⇒
       (((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__Woman) ∧
         s__instance(V__ROW2,s__Human) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__CurrencyMeasure) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__capitalExpendituresOfArea__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__capitalExpendituresOfArea__m,s__Predicate) ∧
           s__capitalExpendituresOfArea(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__Process) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__judge__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__judge__m,s__Predicate) ∧
           s__judge(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__Class))
       ⇒
       (((s__domainSubclass(s__meltingPoint__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__meltingPoint__m,s__Predicate) ∧
           s__meltingPoint(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__ChargingAFee) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__amountCharged__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__amountCharged__m,s__Predicate) ∧
           s__amountCharged(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__Physical) ∧
         s__instance(V__ROW2,s__CognitiveAgent) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__needs__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__needs__m,s__Predicate) ∧
           s__needs(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__Attribute) ∧
         s__instance(V__ROW6,s__Attribute) ∧
         s__instance(V__ROW3,s__Attribute) ∧
         s__instance(V__ROW4,s__Attribute) ∧
         s__subclass(V__ROW2,s__Attribute) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__exhaustiveAttribute__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__exhaustiveAttribute__m,s__Predicate) ∧
           s__exhaustiveAttribute__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__ROW4,V__ROW2,V__NUMBER,V__CLASS]
   (((s__subclass(V__ROW3,s__Day) ∧
         s__instance(V__ROW4,s__TimeDuration) ∧
         s__instance(V__ROW2,s__Region) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__daylightHoursTotal__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__daylightHoursTotal__m,s__Predicate) ∧
           s__daylightHoursTotal(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__AreaMeasure) ∧
         s__instance(V__ROW2,s__GeographicArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__waterAreaOnly__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__waterAreaOnly__m,s__Predicate) ∧
           s__waterAreaOnly(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__Class))
       ⇒
       (((s__domainSubclass(s__annualImportTotal__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__annualImportTotal__m,s__Predicate) ∧
           s__annualImportTotal(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__Motion) ∧
         s__instance(V__ROW2,s__Wind) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__windDrivenMotion__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__windDrivenMotion__m,s__Predicate) ∧
           s__windDrivenMotion(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__PriorityAttribute) ∧
         s__instance(V__ROW2,s__ComputationalSystem) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__priority__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__priority__m,s__Predicate) ∧
           s__priority(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__Class))
       ⇒
       (((s__domainSubclass(s__exactCardinality__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__exactCardinality__m,s__Predicate) ∧
           s__exactCardinality(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__Woman) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__aunt__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__aunt__m,s__Predicate) ∧
           s__aunt(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__ShipRegister) ∧
         s__instance(V__ROW2,s__MerchantMarine) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__marineInventory__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__marineInventory__m,s__Predicate) ∧
           s__marineInventory(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__Class))
       ⇒
       (((s__domainSubclass(s__displayTitle__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__displayTitle__m,s__Predicate) ∧
           s__displayTitle(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__Position) ∧
         s__instance(V__ROW4,s__Human) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__chiefOfState__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__chiefOfState__m,s__Predicate) ∧
           s__chiefOfState(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__Physical) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__maritimeHazard__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__maritimeHazard__m,s__Predicate) ∧
           s__maritimeHazard(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__Interest) ∧
         s__instance(V__ROW2,s__Bond) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__ROW2,s__Physical) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__tributary__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__tributary__m,s__Predicate) ∧
           s__tributary(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__Class))
       ⇒
       (((s__domainSubclass(s__registeredUser__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__registeredUser__m,s__Predicate) ∧
           s__registeredUser(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__Woman) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__sister__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__sister__m,s__Predicate) ∧
           s__sister(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__IndustryAttribute) ∧
         s__instance(V__ROW4,s__RealNumber) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__sectorCompositionOfGDP__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__sectorCompositionOfGDP__m,s__Predicate) ∧
           s__sectorCompositionOfGDP(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__LengthMeasure) ∧
         s__instance(V__ROW4,s__LengthMeasure) ∧
         s__instance(V__ROW2,s__Vehicle) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__maximumPayloadHeightWidth__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__maximumPayloadHeightWidth__m,s__Predicate) ∧
           s__maximumPayloadHeightWidth(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__BodyPart) ∧
         s__subclass(V__ROW2,s__BodyPart) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__connectedBodyPart__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__connectedBodyPart__m,s__Predicate) ∧
           s__connectedBodyPart(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__Substance) ∧
         s__instance(V__ROW2,s__LandArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__groundSubsurfaceType__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__groundSubsurfaceType__m,s__Predicate) ∧
           s__groundSubsurfaceType(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__Class))
       ⇒
       (((s__domainSubclass(s__abbreviatedDisplayTitle__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__abbreviatedDisplayTitle__m,s__Predicate) ∧
           s__abbreviatedDisplayTitle(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__Experimenting) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__qualifiedTreatment__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__qualifiedTreatment__m,s__Predicate) ∧
           s__qualifiedTreatment(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__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__prohibitedItem__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__prohibitedItem__m,s__Predicate) ∧
           s__prohibitedItem(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__Class))
       ⇒
       (((s__domainSubclass(s__lessThan__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__lessThan__m,s__Predicate) ∧
           s__lessThan(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__Interest) ∧
         s__instance(V__ROW4,s__TimeInterval) ∧
         s__instance(V__ROW2,s__FinancialAccount) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__interestEarned__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__interestEarned__m,s__Predicate) ∧
           s__interestEarned(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__Collection) ∧
         s__instance(V__ROW4,s__WebSite) ∧
         s__instance(V__ROW2,s__Agent) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__watchingListings__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__watchingListings__m,s__Predicate) ∧
           s__watchingListings(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__Class))
       ⇒
       (((s__domainSubclass(s__numberAdultOccupant__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__numberAdultOccupant__m,s__Predicate) ∧
           s__numberAdultOccupant(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__TimeDuration) ∧
         s__instance(V__ROW2,s__FinancialAccount) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__periodicPayment__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__periodicPayment__m,s__Predicate) ∧
           s__periodicPayment(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__Reservation) ∧
         s__instance(V__ROW2,s__Agent) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__reservingEntity__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__reservingEntity__m,s__Predicate) ∧
           s__reservingEntity(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__PowerGeneration) ∧
         s__instance(V__ROW4,s__RealNumber) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__electricityFractionFromSource__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__electricityFractionFromSource__m,s__Predicate) ∧
           s__electricityFractionFromSource(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__MilitaryRank) ∧
         s__subclass(V__ROW2,s__MilitaryUnit) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__commandRankOfEchelon__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__commandRankOfEchelon__m,s__Predicate) ∧
           s__commandRankOfEchelon(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__Animal) ∧
         s__subclass(V__ROW2,s__OrganicObject) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__productOfAnimal__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__productOfAnimal__m,s__Predicate) ∧
           s__productOfAnimal(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__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__relativeHumidity__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__relativeHumidity__m,s__Predicate) ∧
           s__relativeHumidity(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__Class))
       ⇒
       (((s__domainSubclass(s__smaller__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__smaller__m,s__Predicate) ∧
           s__smaller(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__Day) ∧
         s__instance(V__ROW2,s__Stock) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((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__ROW3,s__CurrencyMeasure) ∧
         s__instance(V__ROW2,s__Loan) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__floorLoan__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__floorLoan__m,s__Predicate) ∧
           s__floorLoan(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__Class))
       ⇒
       (((s__domainSubclass(s__annualExpendituresOfArea__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__annualExpendituresOfArea__m,s__Predicate) ∧
           s__annualExpendituresOfArea(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__Class))
       ⇒
       (((s__domainSubclass(s__disapproves__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__disapproves__m,s__Predicate) ∧
           s__disapproves(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__subclass(V__ROW2,s__Process) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__frequency__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__frequency__m,s__Predicate) ∧
           s__frequency(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__Game) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__plays__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__plays__m,s__Predicate) ∧
           s__plays(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__WaterArea) ∧
         s__instance(V__ROW2,s__WaterMotion) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__flowCurrent__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__flowCurrent__m,s__Predicate) ∧
           s__flowCurrent(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__IllicitDrug) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__illicitDrugProducer__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__illicitDrugProducer__m,s__Predicate) ∧
           s__illicitDrugProducer(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__Class))
       ⇒
       (((s__domainSubclass(s__subString__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__subString__m,s__Predicate) ∧
           s__subString(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__Object) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__highAltitudeWindSpeed__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__highAltitudeWindSpeed__m,s__Predicate) ∧
           s__highAltitudeWindSpeed(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__subclass(V__ROW2,s__StationaryArtifact) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__maxRoomCapacity__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__maxRoomCapacity__m,s__Predicate) ∧
           s__maxRoomCapacity(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__Set) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__element__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__element__m,s__Predicate) ∧
           s__element(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__Class))
       ⇒
       (((s__domainSubclass(s__connects__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__connects__m,s__Predicate) ∧
           s__connects(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__ROW4,s__Language) ∧
         s__instance(V__ROW2,s__SymbolicString) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__alternativeTitle__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__alternativeTitle__m,s__Predicate) ∧
           s__alternativeTitle(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__RealNumber) ∧
         s__subclass(V__ROW4,s__TimeInterval) ∧
         s__instance(V__ROW2,s__GeopoliticalArea) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__industrialProductionGrowthRateInPeriod__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__industrialProductionGrowthRateInPeriod__m,s__Predicate) ∧
           s__industrialProductionGrowthRateInPeriod(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__ComputerDirectory) ∧
         s__instance(V__ROW2,s__ComputerFile) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__directoryOf__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__directoryOf__m,s__Predicate) ∧
           s__directoryOf(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__Class))
       ⇒
       (((s__domainSubclass(s__origin__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__origin__m,s__Predicate) ∧
           s__origin(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__Recording) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__recordingCompany__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__recordingCompany__m,s__Predicate) ∧
           s__recordingCompany(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__Class))
       ⇒
       (((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__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__Class))
       ⇒
       (((s__domainSubclass(s__increasesLikelihood__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__increasesLikelihood__m,s__Predicate) ∧
           s__increasesLikelihood(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__Man) ∧
         s__instance(V__NUMBER,s__PositiveInteger) ∧
         s__instance(V__CLASS,s__Class))
       ⇒
       (((s__domainSubclass(s__nephew__m,V__NUMBER,V__CLASS)
           ∧
           s__instance(s__nephew__m,s__Predicate) ∧