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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - ListOrderFn
ListOrderFn

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


s__documentation(s__ListOrderFn__m,s__ChineseLanguage,'"(ListOrderFn ?LIST ?NUMBER) 表示在 ?LIST List 第?NUMBER个位置的项目。例如: (ListOrderFn (ListFn Monday Tuesday Wednesday) 2) 交出的值会是 Tuesday。"')

chinese_format.kif 1964-1966
s__documentation(s__ListOrderFn__m,s__EnglishLanguage,'"(ListOrderFn ?LIST ?NUMBER) denotes the item that is in the ?NUMBER position in the List ?LIST. For example, (ListOrderFn (ListFn Monday Tuesday Wednesday) 2) would return the value Tuesday."')

Merge.kif 2877-2880
s__domain(s__ListOrderFn__m,n__1,s__List)

Merge.kif 2873-2873 The number 1 argument of list order is an instance of list
s__domain(s__ListOrderFn__m,n__2,s__PositiveInteger)

Merge.kif 2874-2874 The number 2 argument of list order is an instance of positive integer
s__instance(s__BinaryFunction,s__SetOrClass)

s__instance(s__ListOrderFn__m,s__BinaryFunction)

Merge.kif 2871-2871 List order is an instance of binary function
s__instance(s__ListOrderFn__m,s__PartialValuedRelation)

s__instance(s__PartialValuedRelation,s__SetOrClass)

Merge.kif 2872-2872 List order is an instance of partial valued relation
s__range(s__ListOrderFn__m,s__Entity)

Merge.kif 2875-2875 The range of list order is an instance of entity

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


s__format(s__ChineseLanguage,s__ListOrderFn__m,'"%1 的第 %2 几个元素"')

chinese_format.kif 263-263
s__format(s__EnglishLanguage,s__ListOrderFn__m,'"%2th element of %1"')

english_format.kif 271-271
s__termFormat(s__ChineseLanguage,s__ListOrderFn__m,'"找出表列顺序的函数"')

chinese_format.kif 264-264
s__termFormat(s__ChineseLanguage,s__ListOrderFn__m,'"清单顺序"')

domainEnglishFormat.kif 34680-34680
s__termFormat(s__ChineseTraditionalLanguage,s__ListOrderFn__m,'"清單順序"')

domainEnglishFormat.kif 34679-34679
s__termFormat(s__EnglishLanguage,s__ListOrderFn__m,'"list order"')

domainEnglishFormat.kif 34678-34678

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


No TPTP formula. May not be expressible in strict first order. Merge.kif 17589-17594
No TPTP formula. May not be expressible in strict first order. Merge.kif 17573-17578
No TPTP formula. May not be expressible in strict first order. Merge.kif 17606-17611
( ! [V__QLIST,V__QUANT,V__NUM,V__UNIT,V__NLIST,V__N] :
   (((s__instance(V__QLIST,s__PositiveInteger) &
         s__instance(V__QLIST,s__MeasuringResultList) &
         s__instance(V__QUANT,s__PhysicalQuantity) &
         s__instance(V__NUM,s__RealNumber) &
         s__instance(V__UNIT,s__UnitOfMeasure) &
         s__instance(V__NLIST,s__PositiveInteger) &
         s__instance(V__NLIST,s__NumberList) &
         s__instance(V__N,s__List))
       =>
       ((((V__NLIST = s__PhysicalQuantityToNumberFn(V__QLIST))
           &
           (V__QUANT = s__ListOrderFn(V__N,V__QLIST))
         &
         (V__NUM = s__ListOrderFn(V__N,V__NLIST)))
     =>
     ((s__MeasureFn(V__NUM,V__UNIT)
       = V__QUANT)))))
)
)

Weather.kif 1837-1844
( ! [V__SUM,V__S,V__L,V__N] :
   (((s__instance(V__SUM,s__Number) &
         s__instance(V__S,s__PositiveInteger) &
         s__instance(V__L,s__List))
       =>
       ((((V__SUM = s__ListSumFn(V__L))
           &
           (V__N = s__ListOrderFn(V__L,V__S)))
       =>
       (s__instance(V__N,s__Number)))))
)
)

Merge.kif 3137-3141
( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__WaterArea) &
         s__instance(V__ARGS2,s__WaterMotion))
       =>
       (((s__exactCardinality(s__flowCurrent__m,V__ARG,n__1)
           &
           s__instance(s__flowCurrent__m,s__Predicate) &
           s__flowCurrent(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__GrammaticalGender) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__NaturalLanguage) &
         s__instance(V__ARGS2,s__Noun))
       =>
       (((s__exactCardinality(s__nounGender__m,V__ARG,n__1)
           &
           s__instance(s__nounGender__m,s__Predicate) &
           s__nounGender(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__TimePoint) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__GeographicArea) &
         s__subclass(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__releaseForConsumption__m,V__ARG,n__1)
           &
           s__instance(s__releaseForConsumption__m,s__Predicate) &
           s__releaseForConsumption(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Proposition) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__TimePosition) &
         s__instance(V__ARGS2,s__Proposition))
       =>
       (((s__exactCardinality(s__agreementRevisionDate__m,V__ARG,n__1)
           &
           s__instance(s__agreementRevisionDate__m,s__Predicate) &
           s__agreementRevisionDate(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__PlaneAngleMeasure) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Physical) &
         s__instance(V__ARGS2,s__Physical))
       =>
       (((s__exactCardinality(s__courseWRTMagneticNorth__m,V__ARG,n__1)
           &
           s__instance(s__courseWRTMagneticNorth__m,s__Predicate) &
           s__courseWRTMagneticNorth(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__UserAccount) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__hasAccount__m,V__ARG,n__1)
           &
           s__instance(s__hasAccount__m,s__Predicate) &
           s__hasAccount(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__RealNumber) &
         s__instance(V__ARGS2,s__Inflation))
       =>
       (((s__exactCardinality(s__inflationRate__m,V__ARG,n__1)
           &
           s__instance(s__inflationRate__m,s__Predicate) &
           s__inflationRate(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__ProcessStatus) &
         s__instance(V__ARGS2,s__ComputerProcess))
       =>
       (((s__exactCardinality(s__status__m,V__ARG,n__1)
           &
           s__instance(s__status__m,s__Predicate) &
           s__status(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Physical) &
         s__instance(V__ARGS2,s__Physical))
       =>
       (((s__exactCardinality(s__flows__m,V__ARG,n__1)
           &
           s__instance(s__flows__m,s__Predicate) &
           s__flows(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__physicalEnd__m,V__ARG,n__1)
           &
           s__instance(s__physicalEnd__m,s__Predicate) &
           s__physicalEnd(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__ComputerProgram) &
         s__instance(V__ARGS2,s__ShutdownBlock))
       =>
       (((s__exactCardinality(s__shutdownOf__m,V__ARG,n__1)
           &
           s__instance(s__shutdownOf__m,s__Predicate) &
           s__shutdownOf(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__Organism))
       =>
       (((s__exactCardinality(s__maternalAunt__m,V__ARG,n__1)
           &
           s__instance(s__maternalAunt__m,s__Predicate) &
           s__maternalAunt(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__ContentBearingPhysical) &
         s__instance(V__ARGS2,s__Human))
       =>
       (((s__exactCardinality(s__actedIn__m,V__ARG,n__1)
           &
           s__instance(s__actedIn__m,s__Predicate) &
           s__actedIn(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Process) &
         s__instance(V__ARGS2,s__Process))
       =>
       (((s__exactCardinality(s__coordinates__m,V__ARG,n__1)
           &
           s__instance(s__coordinates__m,s__Predicate) &
           s__coordinates(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__Organism))
       =>
       (((s__exactCardinality(s__fathersSistersSon__m,V__ARG,n__1)
           &
           s__instance(s__fathersSistersSon__m,s__Predicate) &
           s__fathersSistersSon(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__PhysicalSystem) &
         s__instance(V__ARGS2,s__Physical))
       =>
       (((s__exactCardinality(s__systemPart__m,V__ARG,n__1)
           &
           s__instance(s__systemPart__m,s__Predicate) &
           s__systemPart(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__CurrencyMeasure) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Day) &
         s__instance(V__ARGS2,s__FinancialAccount))
       =>
       (((s__exactCardinality(s__shortBalanceAmount__m,V__ARG,n__1)
           &
           s__instance(s__shortBalanceAmount__m,s__Predicate) &
           s__shortBalanceAmount(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__FunctionQuantity) &
         s__instance(V__ARGS2,s__InternalCombustionEngine))
       =>
       (((s__exactCardinality(s__engineIdleSpeed__m,V__ARG,n__1)
           &
           s__instance(s__engineIdleSpeed__m,s__Predicate) &
           s__engineIdleSpeed(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__IntentionalProcess) &
         s__instance(V__ARGS2,s__CognitiveAgent))
       =>
       (((s__exactCardinality(s__enjoys__m,V__ARG,n__1)
           &
           s__instance(s__enjoys__m,s__Predicate) &
           s__enjoys(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Transfer))
       =>
       (((s__exactCardinality(s__objectTransferred__m,V__ARG,n__1)
           &
           s__instance(s__objectTransferred__m,s__Predicate) &
           s__objectTransferred(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__GeopoliticalArea) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__SymbolicString) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__chanceryAddressInArea__m,V__ARG,n__1)
           &
           s__instance(s__chanceryAddressInArea__m,s__Predicate) &
           s__chanceryAddressInArea(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Process))
       =>
       (((s__exactCardinality(s__origin__m,V__ARG,n__1)
           &
           s__instance(s__origin__m,s__Predicate) &
           s__origin(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__NonnegativeInteger) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Class) &
         s__instance(V__ARGS2,s__GeographicArea))
       =>
       (((s__exactCardinality(s__totalFacilityTypeInArea__m,V__ARG,n__1)
           &
           s__instance(s__totalFacilityTypeInArea__m,s__Predicate) &
           s__totalFacilityTypeInArea(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__UniformResourceLocator) &
         s__instance(V__ARGS2,s__WebPage))
       =>
       (((s__exactCardinality(s__webPageURL__m,V__ARG,n__1)
           &
           s__instance(s__webPageURL__m,s__Predicate) &
           s__webPageURL(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Human) &
         s__instance(V__ARGS2,s__Woman))
       =>
       (((s__exactCardinality(s__sister__m,V__ARG,n__1)
           &
           s__instance(s__sister__m,s__Predicate) &
           s__sister(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__GeopoliticalArea) &
         s__instance(V__ARGS2,s__MilitaryOrganization))
       =>
       (((s__exactCardinality(s__militaryOfArea__m,V__ARG,n__1)
           &
           s__instance(s__militaryOfArea__m,s__Predicate) &
           s__militaryOfArea(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CognitiveAgent) &
         s__instance(V__ARGS2,s__Formula))
       =>
       (((s__exactCardinality(s__holdsObligation__m,V__ARG,n__1)
           &
           s__instance(s__holdsObligation__m,s__Predicate) &
           s__holdsObligation(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CareOrganization) &
         s__instance(V__ARGS2,s__Human))
       =>
       (((s__exactCardinality(s__medicalPatient__m,V__ARG,n__1)
           &
           s__instance(s__medicalPatient__m,s__Predicate) &
           s__medicalPatient(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Region) &
         s__instance(V__ARGS2,s__Human))
       =>
       (((s__exactCardinality(s__baptismplace__m,V__ARG,n__1)
           &
           s__instance(s__baptismplace__m,s__Predicate) &
           s__baptismplace(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS5,V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS5,s__CognitiveAgent) &
         s__instance(V__ARGS4,s__Agreement) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__DeonticAttribute) &
         s__instance(V__ARGS2,s__Proposition))
       =>
       (((s__exactCardinality(s__agreementClause__m,V__ARG,n__1)
           &
           s__instance(s__agreementClause__m,s__Predicate) &
           s__agreementClause(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
         &
         (V__X = s__ListOrderFn(s__ListFn__4Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__4Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__ComputerProgram) &
         s__instance(V__ARGS2,s__TimePosition))
       =>
       (((s__exactCardinality(s__monitorApplicationData__m,V__ARG,n__1)
           &
           s__instance(s__monitorApplicationData__m,s__Predicate) &
           s__monitorApplicationData(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__importCommodityType__m,V__ARG,n__1)
           &
           s__instance(s__importCommodityType__m,s__Predicate) &
           s__importCommodityType(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TimeInterval) &
         s__instance(V__ARGS2,s__TimeInterval))
       =>
       (((s__exactCardinality(s__during__m,V__ARG,n__1)
           &
           s__instance(s__during__m,s__Predicate) &
           s__during(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agent) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__exploits__m,V__ARG,n__1)
           &
           s__instance(s__exploits__m,s__Predicate) &
           s__exploits(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Computer) &
         s__instance(V__ARGS2,s__ComputerProgram))
       =>
       (((s__exactCardinality(s__runsOn__m,V__ARG,n__1)
           &
           s__instance(s__runsOn__m,s__Predicate) &
           s__runsOn(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Human) &
         s__instance(V__ARGS2,s__Human))
       =>
       (((s__exactCardinality(s__cohabitant__m,V__ARG,n__1)
           &
           s__instance(s__cohabitant__m,s__Predicate) &
           s__cohabitant(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Human) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__familyName__m,V__ARG,n__1)
           &
           s__instance(s__familyName__m,s__Predicate) &
           s__familyName(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Formula) &
         s__instance(V__ARGS2,s__CognitiveAgent))
       =>
       (((s__exactCardinality(s__expects__m,V__ARG,n__1)
           &
           s__instance(s__expects__m,s__Predicate) &
           s__expects(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__nameIndexOrder__m,V__ARG,n__1)
           &
           s__instance(s__nameIndexOrder__m,s__Predicate) &
           s__nameIndexOrder(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agreement) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__unratifiedSignatoryToAgreement__m,V__ARG,n__1)
           &
           s__instance(s__unratifiedSignatoryToAgreement__m,s__Predicate) &
           s__unratifiedSignatoryToAgreement(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Language) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__originalTitle__m,V__ARG,n__1)
           &
           s__instance(s__originalTitle__m,s__Predicate) &
           s__originalTitle(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Attribute) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Attribute) &
         s__instance(V__ARGS2,s__Attribute))
       =>
       (((s__exactCardinality(s__contraryAttribute__m,V__ARG,n__1)
           &
           s__instance(s__contraryAttribute__m,s__Predicate) &
           s__contraryAttribute__3(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__agriculturalProductType__m,V__ARG,n__1)
           &
           s__instance(s__agriculturalProductType__m,s__Predicate) &
           s__agriculturalProductType(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__superficialPart__m,V__ARG,n__1)
           &
           s__instance(s__superficialPart__m,s__Predicate) &
           s__superficialPart(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Agent) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Attribute))
       =>
       (((s__exactCardinality(s__subjectiveAttribute__m,V__ARG,n__1)
           &
           s__instance(s__subjectiveAttribute__m,s__Predicate) &
           s__subjectiveAttribute(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CurrencyMeasure) &
         s__instance(V__ARGS2,s__Auctioning))
       =>
       (((s__exactCardinality(s__reservePrice__m,V__ARG,n__1)
           &
           s__instance(s__reservePrice__m,s__Predicate) &
           s__reservePrice(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__PostalPlace) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__postPostOfficeBox__m,V__ARG,n__1)
           &
           s__instance(s__postPostOfficeBox__m,s__Predicate) &
           s__postPostOfficeBox(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__GeographicArea) &
         s__subclass(V__ARGS2,s__Organism))
       =>
       (((s__exactCardinality(s__habitatOfOrganism__m,V__ARG,n__1)
           &
           s__instance(s__habitatOfOrganism__m,s__Predicate) &
           s__habitatOfOrganism(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__freePropertyAmenity__m,V__ARG,n__1)
           &
           s__instance(s__freePropertyAmenity__m,s__Predicate) &
           s__freePropertyAmenity(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Sentence) &
         s__instance(V__ARGS2,s__CognitiveAgent))
       =>
       (((s__exactCardinality(s__states__m,V__ARG,n__1)
           &
           s__instance(s__states__m,s__Predicate) &
           s__states(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__FieldOfStudy) &
         s__instance(V__ARGS2,s__Human))
       =>
       (((s__exactCardinality(s__hasExpertise__m,V__ARG,n__1)
           &
           s__instance(s__hasExpertise__m,s__Predicate) &
           s__hasExpertise(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Holiday) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__nationalCelebration__m,V__ARG,n__1)
           &
           s__instance(s__nationalCelebration__m,s__Predicate) &
           s__nationalCelebration(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agent) &
         s__instance(V__ARGS2,s__AmbienceAttribute))
       =>
       (((s__exactCardinality(s__dressCode__m,V__ARG,n__1)
           &
           s__instance(s__dressCode__m,s__Predicate) &
           s__dressCode(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS5,V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS5,s__Region) &
         s__instance(V__ARGS4,s__Object) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CaseRole) &
         s__subclass(V__ARGS2,s__Process))
       =>
       (((s__exactCardinality(s__capableAtLocation__m,V__ARG,n__1)
           &
           s__instance(s__capableAtLocation__m,s__Predicate) &
           s__capableAtLocation(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
         &
         (V__X = s__ListOrderFn(s__ListFn__4Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__4Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__SocialRole) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__TimePosition) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__electionDatePlannedForPosition__m,V__ARG,n__1)
           &
           s__instance(s__electionDatePlannedForPosition__m,s__Predicate) &
           s__electionDatePlannedForPosition(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__ServiceProcess) &
         s__instance(V__ARGS2,s__RoomInventory))
       =>
       (((s__exactCardinality(s__someRoomsServiceAmenity__m,V__ARG,n__1)
           &
           s__instance(s__someRoomsServiceAmenity__m,s__Predicate) &
           s__someRoomsServiceAmenity(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS6,V__ARGS5,V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS6,s__Class) &
         s__instance(V__ARGS5,s__Class) &
         s__instance(V__ARGS4,s__Class) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Class) &
         s__instance(V__ARGS2,s__Class))
       =>
       (((s__exactCardinality(s__partition__m,V__ARG,n__1)
           &
           s__instance(s__partition__m,s__Predicate) &
           s__partition__5(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6)
         &
         (V__X = s__ListOrderFn(s__ListFn__5Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__5Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Attribute) &
         s__instance(V__ARG,s__PositiveInteger))
       =>
       (((s__exactCardinality(s__greaterThanByQuality__m,V__ARG,n__1)
           &
           s__instance(s__greaterThanByQuality__m,s__Predicate) &
           s__greaterThanByQuality(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agent) &
         s__instance(V__ARGS2,s__Organization))
       =>
       (((s__exactCardinality(s__executiveBranch__m,V__ARG,n__1)
           &
           s__instance(s__executiveBranch__m,s__Predicate) &
           s__executiveBranch(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__PhysicalQuantity) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__lowAltitudeWindSpeed__m,V__ARG,n__1)
           &
           s__instance(s__lowAltitudeWindSpeed__m,s__Predicate) &
           s__lowAltitudeWindSpeed(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CognitiveAgent) &
         s__instance(V__ARGS2,s__Share))
       =>
       (((s__exactCardinality(s__shareHolder__m,V__ARG,n__1)
           &
           s__instance(s__shareHolder__m,s__Predicate) &
           s__shareHolder(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Substance) &
         s__instance(V__ARGS2,s__LandArea))
       =>
       (((s__exactCardinality(s__groundSurfaceType__m,V__ARG,n__1)
           &
           s__instance(s__groundSurfaceType__m,s__Predicate) &
           s__groundSurfaceType(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CurrencyMeasure) &
         s__instance(V__ARGS2,s__ChargingAFee))
       =>
       (((s__exactCardinality(s__amountCharged__m,V__ARG,n__1)
           &
           s__instance(s__amountCharged__m,s__Predicate) &
           s__amountCharged(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__Class))
       =>
       (((s__exactCardinality(s__exhaustiveDecomposition__m,V__ARG,n__1)
           &
           s__instance(s__exhaustiveDecomposition__m,s__Predicate) &
           s__exhaustiveDecomposition__1(V__ARGS2)
         &
         (V__X = s__ListOrderFn(s__ListFn__1Fn(V__ARGS2)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__1Fn(V__ARGS2)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Toxin) &
         s__subclass(V__ARGS2,s__Organism))
       =>
       (((s__exactCardinality(s__secretesToxin__m,V__ARG,n__1)
           &
           s__instance(s__secretesToxin__m,s__Predicate) &
           s__secretesToxin(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Object) &
         s__subclass(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__typicalPart__m,V__ARG,n__1)
           &
           s__instance(s__typicalPart__m,s__Predicate) &
           s__typicalPart(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__RadiationMeasure) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__absorbedDose__m,V__ARG,n__1)
           &
           s__instance(s__absorbedDose__m,s__Predicate) &
           s__absorbedDose(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Text) &
         s__instance(V__ARGS2,s__Organization))
       =>
       (((s__exactCardinality(s__publishes__m,V__ARG,n__1)
           &
           s__instance(s__publishes__m,s__Predicate) &
           s__publishes(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Language) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__sortingTitle__m,V__ARG,n__1)
           &
           s__instance(s__sortingTitle__m,s__Predicate) &
           s__sortingTitle(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__IntentionalProcess) &
         s__instance(V__ARGS2,s__IndustryAttribute))
       =>
       (((s__exactCardinality(s__industryServiceType__m,V__ARG,n__1)
           &
           s__instance(s__industryServiceType__m,s__Predicate) &
           s__industryServiceType(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS7,V__ARGS6,V__ARGS5,V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS7,s__Class) &
         s__instance(V__ARGS6,s__Class) &
         s__instance(V__ARGS5,s__Class) &
         s__instance(V__ARGS4,s__Class) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Class) &
         s__instance(V__ARGS2,s__Class))
       =>
       (((s__exactCardinality(s__disjointDecomposition__m,V__ARG,n__1)
           &
           s__instance(s__disjointDecomposition__m,s__Predicate) &
           s__disjointDecomposition__6(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7)
         &
         (V__X = s__ListOrderFn(s__ListFn__6Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__6Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__IPAddress) &
         s__instance(V__ARGS2,s__Computer))
       =>
       (((s__exactCardinality(s__ipAddressOf__m,V__ARG,n__1)
           &
           s__instance(s__ipAddressOf__m,s__Predicate) &
           s__ipAddressOf(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS5,V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS5,s__TimeInterval) &
         s__instance(V__ARGS4,s__CurrencyMeasure) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Organization) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__grossMerchandiseBoughtInPeriod__m,V__ARG,n__1)
           &
           s__instance(s__grossMerchandiseBoughtInPeriod__m,s__Predicate) &
           s__grossMerchandiseBoughtInPeriod(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
         &
         (V__X = s__ListOrderFn(s__ListFn__4Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__4Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__uniqueIdentifier__m,V__ARG,n__1)
           &
           s__instance(s__uniqueIdentifier__m,s__Predicate) &
           s__uniqueIdentifier(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__traverses__m,V__ARG,n__1)
           &
           s__instance(s__traverses__m,s__Predicate) &
           s__traverses(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__most__m,V__ARG,n__1)
           &
           s__instance(s__most__m,s__Predicate) &
           s__most(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__connected__m,V__ARG,n__1)
           &
           s__instance(s__connected__m,s__Predicate) &
           s__connected(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__AreaOfConcern) &
         s__instance(V__ARGS2,s__GeographicArea))
       =>
       (((s__exactCardinality(s__regionalIssue__m,V__ARG,n__1)
           &
           s__instance(s__regionalIssue__m,s__Predicate) &
           s__regionalIssue(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Collection) &
         s__instance(V__ARGS2,s__Physical))
       =>
       (((s__exactCardinality(s__member__m,V__ARG,n__1)
           &
           s__instance(s__member__m,s__Predicate) &
           s__member(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Human) &
         s__instance(V__ARGS2,s__Human))
       =>
       (((s__exactCardinality(s__grandparent__m,V__ARG,n__1)
           &
           s__instance(s__grandparent__m,s__Predicate) &
           s__grandparent(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__WebSite) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__confirmedRegisteredUser__m,V__ARG,n__1)
           &
           s__instance(s__confirmedRegisteredUser__m,s__Predicate) &
           s__confirmedRegisteredUser(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Integer) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agent) &
         s__instance(V__ARGS2,s__Election))
       =>
       (((s__exactCardinality(s__seatsWonInElection__m,V__ARG,n__1)
           &
           s__instance(s__seatsWonInElection__m,s__Predicate) &
           s__seatsWonInElection(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__GeopoliticalArea) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__IllicitDrug) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__illicitDrugTransshipmentPoint__m,V__ARG,n__1)
           &
           s__instance(s__illicitDrugTransshipmentPoint__m,s__Predicate) &
           s__illicitDrugTransshipmentPoint(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__RealNumber) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__ComputerComponent) &
         s__instance(V__ARGS2,s__MeasuringPerformance))
       =>
       (((s__exactCardinality(s__performanceResult__m,V__ARG,n__1)
           &
           s__instance(s__performanceResult__m,s__Predicate) &
           s__performanceResult(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Reservation) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__fulfillingEntity__m,V__ARG,n__1)
           &
           s__instance(s__fulfillingEntity__m,s__Predicate) &
           s__fulfillingEntity(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS5,V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__subclass(V__ARGS5,s__TimeInterval) &
         s__instance(V__ARGS4,s__RealNumber) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__PowerGeneration) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__electricityFractionFromSourceInPeriod__m,V__ARG,n__1)
           &
           s__instance(s__electricityFractionFromSourceInPeriod__m,s__Predicate) &
           s__electricityFractionFromSourceInPeriod(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
         &
         (V__X = s__ListOrderFn(s__ListFn__4Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__4Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Transportation))
       =>
       (((s__exactCardinality(s__transported__m,V__ARG,n__1)
           &
           s__instance(s__transported__m,s__Predicate) &
           s__transported(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__FunctionQuantity) &
         s__instance(V__ARGS2,s__ComputerNetwork))
       =>
       (((s__exactCardinality(s__bandwidth__m,V__ARG,n__1)
           &
           s__instance(s__bandwidth__m,s__Predicate) &
           s__bandwidth(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Class) &
         s__instance(V__ARGS2,s__BinaryRelation))
       =>
       (((s__exactCardinality(s__irreflexiveOn__m,V__ARG,n__1)
           &
           s__instance(s__irreflexiveOn__m,s__Predicate) &
           s__irreflexiveOn(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__subclass(V__ARGS4,s__TimeInterval) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CurrencyMeasure) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__totalGDPInPeriod__m,V__ARG,n__1)
           &
           s__instance(s__totalGDPInPeriod__m,s__Predicate) &
           s__totalGDPInPeriod(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__ShipRegister) &
         s__instance(V__ARGS2,s__MerchantMarine))
       =>
       (((s__exactCardinality(s__marineInventory__m,V__ARG,n__1)
           &
           s__instance(s__marineInventory__m,s__Predicate) &
           s__marineInventory(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Integer) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__fleetSize__m,V__ARG,n__1)
           &
           s__instance(s__fleetSize__m,s__Predicate) &
           s__fleetSize(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TimePoint) &
         s__instance(V__ARGS2,s__TimePoint))
       =>
       (((s__exactCardinality(s__before__m,V__ARG,n__1)
           &
           s__instance(s__before__m,s__Predicate) &
           s__before(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__FinancialAccountStatus) &
         s__instance(V__ARGS2,s__FinancialAccount))
       =>
       (((s__exactCardinality(s__accountStatus__m,V__ARG,n__1)
           &
           s__instance(s__accountStatus__m,s__Predicate) &
           s__accountStatus(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS6,V__ARGS5,V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS6,s__SymbolicString) &
         s__instance(V__ARGS5,s__UnitOfMeasure) &
         s__instance(V__ARGS4,s__ComputerComponent) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__ComputerComponent) &
         s__instance(V__ARGS2,s__TimePosition))
       =>
       (((s__exactCardinality(s__componentDataID__m,V__ARG,n__1)
           &
           s__instance(s__componentDataID__m,s__Predicate) &
           s__componentDataID(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6)
         &
         (V__X = s__ListOrderFn(s__ListFn__5Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__5Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__LengthMeasure) &
         s__instance(V__ARGS2,s__Engine))
       =>
       (((s__exactCardinality(s__pistonStroke__m,V__ARG,n__1)
           &
           s__instance(s__pistonStroke__m,s__Predicate) &
           s__pistonStroke(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__CognitiveAgent) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CurrencyMeasure) &
         s__subclass(V__ARGS2,s__Entity))
       =>
       (((s__exactCardinality(s__productPrice__m,V__ARG,n__1)
           &
           s__instance(s__productPrice__m,s__Predicate) &
           s__productPrice(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__ContentBearingPhysical) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__titles__m,V__ARG,n__1)
           &
           s__instance(s__titles__m,s__Predicate) &
           s__titles(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Position) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__chiefOfStateType__m,V__ARG,n__1)
           &
           s__instance(s__chiefOfStateType__m,s__Predicate) &
           s__chiefOfStateType(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__Physical))
       =>
       (((s__exactCardinality(s__width__m,V__ARG,n__1)
           &
           s__instance(s__width__m,s__Predicate) &
           s__width(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__PositionalAttribute) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__orientation__m,V__ARG,n__1)
           &
           s__instance(s__orientation__m,s__Predicate) &
           s__orientation(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Formula) &
         s__instance(V__ARGS2,s__Formula))
       =>
       (((s__exactCardinality(s__entails__m,V__ARG,n__1)
           &
           s__instance(s__entails__m,s__Predicate) &
           s__entails(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Woman) &
         s__instance(V__ARGS2,s__Human))
       =>
       (((s__exactCardinality(s__grandmother__m,V__ARG,n__1)
           &
           s__instance(s__grandmother__m,s__Predicate) &
           s__grandmother(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__GeometricFigure) &
         s__instance(V__ARGS2,s__OneDimensionalFigure))
       =>
       (((s__exactCardinality(s__sideOfFigure__m,V__ARG,n__1)
           &
           s__instance(s__sideOfFigure__m,s__Predicate) &
           s__sideOfFigure(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__NonnegativeInteger) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__GeopoliticalArea) &
         s__instance(V__ARGS2,s__MerchantMarine))
       =>
       (((s__exactCardinality(s__fOCShipsByOrigin__m,V__ARG,n__1)
           &
           s__instance(s__fOCShipsByOrigin__m,s__Predicate) &
           s__fOCShipsByOrigin(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Organization) &
         s__instance(V__ARGS2,s__Election))
       =>
       (((s__exactCardinality(s__electionForOrganization__m,V__ARG,n__1)
           &
           s__instance(s__electionForOrganization__m,s__Predicate) &
           s__electionForOrganization(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__half__m,V__ARG,n__1)
           &
           s__instance(s__half__m,s__Predicate) &
           s__half(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Neighborhood) &
         s__instance(V__ARGS2,s__PostalPlace))
       =>
       (((s__exactCardinality(s__postNeighborhood__m,V__ARG,n__1)
           &
           s__instance(s__postNeighborhood__m,s__Predicate) &
           s__postNeighborhood(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TelecomNumber) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__telecomCountryCode__m,V__ARG,n__1)
           &
           s__instance(s__telecomCountryCode__m,s__Predicate) &
           s__telecomCountryCode(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__List) &
         s__instance(V__ARGS2,s__List))
       =>
       (((s__exactCardinality(s__subList__m,V__ARG,n__1)
           &
           s__instance(s__subList__m,s__Predicate) &
           s__subList(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Muscle) &
         s__subclass(V__ARGS2,s__Muscle))
       =>
       (((s__exactCardinality(s__antagonistMuscles__m,V__ARG,n__1)
           &
           s__instance(s__antagonistMuscles__m,s__Predicate) &
           s__antagonistMuscles(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Organism) &
         s__instance(V__ARGS2,s__Organism))
       =>
       (((s__exactCardinality(s__relative__m,V__ARG,n__1)
           &
           s__instance(s__relative__m,s__Predicate) &
           s__relative(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TimeDuration) &
         s__instance(V__ARGS2,s__TimeInterval))
       =>
       (((s__exactCardinality(s__duration__m,V__ARG,n__1)
           &
           s__instance(s__duration__m,s__Predicate) &
           s__duration(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Language) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__translatedTitle__m,V__ARG,n__1)
           &
           s__instance(s__translatedTitle__m,s__Predicate) &
           s__translatedTitle(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Formula) &
         s__instance(V__ARGS2,s__CognitiveAgent))
       =>
       (((s__exactCardinality(s__desires__m,V__ARG,n__1)
           &
           s__instance(s__desires__m,s__Predicate) &
           s__desires(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__NonnegativeInteger) &
         s__instance(V__ARGS2,s__Engine))
       =>
       (((s__exactCardinality(s__engineCylinders__m,V__ARG,n__1)
           &
           s__instance(s__engineCylinders__m,s__Predicate) &
           s__engineCylinders(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agent) &
         s__instance(V__ARGS2,s__Physical))
       =>
       (((s__exactCardinality(s__managedBy__m,V__ARG,n__1)
           &
           s__instance(s__managedBy__m,s__Predicate) &
           s__managedBy(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__BodyPart) &
         s__subclass(V__ARGS2,s__BodyPart))
       =>
       (((s__exactCardinality(s__connectedBodyPart__m,V__ARG,n__1)
           &
           s__instance(s__connectedBodyPart__m,s__Predicate) &
           s__connectedBodyPart(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agent) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__operator__m,V__ARG,n__1)
           &
           s__instance(s__operator__m,s__Predicate) &
           s__operator(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__TimeInterval) &
         s__instance(V__ARGS2,s__GeographicArea))
       =>
       (((s__exactCardinality(s__coldSeasonInArea__m,V__ARG,n__1)
           &
           s__instance(s__coldSeasonInArea__m,s__Predicate) &
           s__coldSeasonInArea(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__subclass(V__ARGS4,s__TimeDuration) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__TimeDuration) &
         s__instance(V__ARGS2,s__DiseaseOrSyndrome))
       =>
       (((s__exactCardinality(s__diseaseIncubation__m,V__ARG,n__1)
           &
           s__instance(s__diseaseIncubation__m,s__Predicate) &
           s__diseaseIncubation(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__FinancialOrganization) &
         s__instance(V__ARGS2,s__FinancialAccount))
       =>
       (((s__exactCardinality(s__accountAt__m,V__ARG,n__1)
           &
           s__instance(s__accountAt__m,s__Predicate) &
           s__accountAt(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Policy) &
         s__instance(V__ARGS2,s__HotelPackage))
       =>
       (((s__exactCardinality(s__policyInclusion__m,V__ARG,n__1)
           &
           s__instance(s__policyInclusion__m,s__Predicate) &
           s__policyInclusion(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__localShortName__m,V__ARG,n__1)
           &
           s__instance(s__localShortName__m,s__Predicate) &
           s__localShortName(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__TimeInterval) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__UserAccount) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__loggedInDuring__m,V__ARG,n__1)
           &
           s__instance(s__loggedInDuring__m,s__Predicate) &
           s__loggedInDuring(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__GeopoliticalArea) &
         s__instance(V__ARGS2,s__PoliticalParty))
       =>
       (((s__exactCardinality(s__politicalPartyOfCountry__m,V__ARG,n__1)
           &
           s__instance(s__politicalPartyOfCountry__m,s__Predicate) &
           s__politicalPartyOfCountry(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__WebSite) &
         s__instance(V__ARGS2,s__UserAccount))
       =>
       (((s__exactCardinality(s__accountAtSite__m,V__ARG,n__1)
           &
           s__instance(s__accountAtSite__m,s__Predicate) &
           s__accountAtSite(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Class) &
         s__instance(V__ARGS2,s__Class))
       =>
       (((s__exactCardinality(s__disjointDecomposition__m,V__ARG,n__1)
           &
           s__instance(s__disjointDecomposition__m,s__Predicate) &
           s__disjointDecomposition__2(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__CurrencyMeasure) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__FinancialTransaction) &
         s__instance(V__ARGS2,s__FinancialAccount))
       =>
       (((s__exactCardinality(s__minimumBalance__m,V__ARG,n__1)
           &
           s__instance(s__minimumBalance__m,s__Predicate) &
           s__minimumBalance(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__LengthMeasure) &
         s__subclass(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__defaultMaximumLength__m,V__ARG,n__1)
           &
           s__instance(s__defaultMaximumLength__m,s__Predicate) &
           s__defaultMaximumLength(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Number) &
         s__instance(V__ARGS2,s__TransportationDevice))
       =>
       (((s__exactCardinality(s__passengerCapacityMaxNumber__m,V__ARG,n__1)
           &
           s__instance(s__passengerCapacityMaxNumber__m,s__Predicate) &
           s__passengerCapacityMaxNumber(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__AcidityMeasure) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__phMeasure__m,V__ARG,n__1)
           &
           s__instance(s__phMeasure__m,s__Predicate) &
           s__phMeasure(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__ComputerProtocol) &
         s__instance(V__ARGS2,s__ComputerProgram))
       =>
       (((s__exactCardinality(s__implementsProtocol__m,V__ARG,n__1)
           &
           s__instance(s__implementsProtocol__m,s__Predicate) &
           s__implementsProtocol(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Woman) &
         s__instance(V__ARGS2,s__Human))
       =>
       (((s__exactCardinality(s__stepmother__m,V__ARG,n__1)
           &
           s__instance(s__stepmother__m,s__Predicate) &
           s__stepmother(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__CurrencyMeasure) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Day) &
         s__instance(V__ARGS2,s__FinancialAccount))
       =>
       (((s__exactCardinality(s__buyingPowerAmount__m,V__ARG,n__1)
           &
           s__instance(s__buyingPowerAmount__m,s__Predicate) &
           s__buyingPowerAmount(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS7,V__ARGS6,V__ARGS5,V__ARGS4,V__ARGS8,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS7,s__Class) &
         s__instance(V__ARGS6,s__Class) &
         s__instance(V__ARGS5,s__Class) &
         s__instance(V__ARGS4,s__Class) &
         s__instance(V__ARGS8,s__Class) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Class) &
         s__instance(V__ARGS2,s__Class))
       =>
       (((s__exactCardinality(s__disjointDecomposition__m,V__ARG,n__1)
           &
           s__instance(s__disjointDecomposition__m,s__Predicate) &
           s__disjointDecomposition__7(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7,V__ARGS8)
         &
         (V__X = s__ListOrderFn(s__ListFn__7Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7,V__ARGS8)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__7Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7,V__ARGS8)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__EducationalOrganization) &
         s__instance(V__ARGS2,s__Human))
       =>
       (((s__exactCardinality(s__student__m,V__ARG,n__1)
           &
           s__instance(s__student__m,s__Predicate) &
           s__student(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS5,V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS5,s__Class) &
         s__instance(V__ARGS4,s__Class) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Class) &
         s__instance(V__ARGS2,s__Class))
       =>
       (((s__exactCardinality(s__disjointDecomposition__m,V__ARG,n__1)
           &
           s__instance(s__disjointDecomposition__m,s__Predicate) &
           s__disjointDecomposition__4(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
         &
         (V__X = s__ListOrderFn(s__ListFn__4Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__4Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Organism) &
         s__instance(V__ARGS2,s__Organism))
       =>
       (((s__exactCardinality(s__sibling__m,V__ARG,n__1)
           &
           s__instance(s__sibling__m,s__Predicate) &
           s__sibling(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Formula) &
         s__instance(V__ARGS2,s__Reservation))
       =>
       (((s__exactCardinality(s__rateDetail__m,V__ARG,n__1)
           &
           s__instance(s__rateDetail__m,s__Predicate) &
           s__rateDetail(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Human) &
         s__instance(V__ARGS2,s__Human))
       =>
       (((s__exactCardinality(s__coaches__m,V__ARG,n__1)
           &
           s__instance(s__coaches__m,s__Predicate) &
           s__coaches(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__AreaMeasure) &
         s__instance(V__ARGS2,s__Region))
       =>
       (((s__exactCardinality(s__totalArea__m,V__ARG,n__1)
           &
           s__instance(s__totalArea__m,s__Predicate) &
           s__totalArea(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__TimeInterval) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__fiscalYearPeriod__m,V__ARG,n__1)
           &
           s__instance(s__fiscalYearPeriod__m,s__Predicate) &
           s__fiscalYearPeriod(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__Organism))
       =>
       (((s__exactCardinality(s__paternalAunt__m,V__ARG,n__1)
           &
           s__instance(s__paternalAunt__m,s__Predicate) &
           s__paternalAunt(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__DevelopmentalAttribute) &
         s__instance(V__ARGS2,s__OrganicObject))
       =>
       (((s__exactCardinality(s__developmentalForm__m,V__ARG,n__1)
           &
           s__instance(s__developmentalForm__m,s__Predicate) &
           s__developmentalForm(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__paidPropertyAmenity__m,V__ARG,n__1)
           &
           s__instance(s__paidPropertyAmenity__m,s__Predicate) &
           s__paidPropertyAmenity(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Proposition) &
         s__instance(V__ARGS2,s__Reservation))
       =>
       (((s__exactCardinality(s__reservedPackage__m,V__ARG,n__1)
           &
           s__instance(s__reservedPackage__m,s__Predicate) &
           s__reservedPackage(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__GeographicArea) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Process) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__areaOfResponsibility__m,V__ARG,n__1)
           &
           s__instance(s__areaOfResponsibility__m,s__Predicate) &
           s__areaOfResponsibility(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Integer) &
         s__instance(V__ARGS2,s__Building))
       =>
       (((s__exactCardinality(s__numberOfFloors__m,V__ARG,n__1)
           &
           s__instance(s__numberOfFloors__m,s__Predicate) &
           s__numberOfFloors(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__ContentBearingPhysical) &
         s__subclass(V__ARGS2,s__ContentBearingPhysical))
       =>
       (((s__exactCardinality(s__subsumesContentClass__m,V__ARG,n__1)
           &
           s__instance(s__subsumesContentClass__m,s__Predicate) &
           s__subsumesContentClass(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agent) &
         s__instance(V__ARGS2,s__Organization))
       =>
       (((s__exactCardinality(s__judicialBranch__m,V__ARG,n__1)
           &
           s__instance(s__judicialBranch__m,s__Predicate) &
           s__judicialBranch(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Physical))
       =>
       (((s__exactCardinality(s__located__m,V__ARG,n__1)
           &
           s__instance(s__located__m,s__Predicate) &
           s__located(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__PositiveInteger) &
         s__subclass(V__ARGS2,s__ElementalSubstance))
       =>
       (((s__exactCardinality(s__atomicNumber__m,V__ARG,n__1)
           &
           s__instance(s__atomicNumber__m,s__Predicate) &
           s__atomicNumber(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__properPart__m,V__ARG,n__1)
           &
           s__instance(s__properPart__m,s__Predicate) &
           s__properPart(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__subclass(V__ARGS4,s__TimeInterval) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CurrencyMeasure) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__economicAidReceivedNetInPeriod__m,V__ARG,n__1)
           &
           s__instance(s__economicAidReceivedNetInPeriod__m,s__Predicate) &
           s__economicAidReceivedNetInPeriod(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TimePosition) &
         s__instance(V__ARGS2,s__TimePosition))
       =>
       (((s__exactCardinality(s__temporalPart__m,V__ARG,n__1)
           &
           s__instance(s__temporalPart__m,s__Predicate) &
           s__temporalPart(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TimeInterval) &
         s__instance(V__ARGS2,s__TimeInterval))
       =>
       (((s__exactCardinality(s__meetsTemporally__m,V__ARG,n__1)
           &
           s__instance(s__meetsTemporally__m,s__Predicate) &
           s__meetsTemporally(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__quarter__m,V__ARG,n__1)
           &
           s__instance(s__quarter__m,s__Predicate) &
           s__quarter(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__LengthMeasure) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__LengthMeasure) &
         s__instance(V__ARGS2,s__Vehicle))
       =>
       (((s__exactCardinality(s__maximumPayloadHeightWidth__m,V__ARG,n__1)
           &
           s__instance(s__maximumPayloadHeightWidth__m,s__Predicate) &
           s__maximumPayloadHeightWidth(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__RealNumber) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__PowerGeneration) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__electricityFractionFromSource__m,V__ARG,n__1)
           &
           s__instance(s__electricityFractionFromSource__m,s__Predicate) &
           s__electricityFractionFromSource(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__RealNumber) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Formula) &
         s__instance(V__ARGS2,s__Formula))
       =>
       (((s__exactCardinality(s__conditionalProbability__m,V__ARG,n__1)
           &
           s__instance(s__conditionalProbability__m,s__Predicate) &
           s__conditionalProbability(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Attribute) &
         s__instance(V__ARGS2,s__Attribute))
       =>
       (((s__exactCardinality(s__contraryAttribute__m,V__ARG,n__1)
           &
           s__instance(s__contraryAttribute__m,s__Predicate) &
           s__contraryAttribute__2(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__TimeInterval) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__RealNumber) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__militaryExpendituresFractionOfGDPInPeriod__m,V__ARG,n__1)
           &
           s__instance(s__militaryExpendituresFractionOfGDPInPeriod__m,s__Predicate) &
           s__militaryExpendituresFractionOfGDPInPeriod(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CognitiveAgent) &
         s__instance(V__ARGS2,s__MusicRecording))
       =>
       (((s__exactCardinality(s__songArtist__m,V__ARG,n__1)
           &
           s__instance(s__songArtist__m,s__Predicate) &
           s__songArtist(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__List) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__viewedItemList__m,V__ARG,n__1)
           &
           s__instance(s__viewedItemList__m,s__Predicate) &
           s__viewedItemList(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CognitiveAgent) &
         s__instance(V__ARGS2,s__LegalAction))
       =>
       (((s__exactCardinality(s__plaintiff__m,V__ARG,n__1)
           &
           s__instance(s__plaintiff__m,s__Predicate) &
           s__plaintiff(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Experimenting) &
         s__instance(V__ARGS2,s__ContentBearingPhysical))
       =>
       (((s__exactCardinality(s__finalExperimentReport__m,V__ARG,n__1)
           &
           s__instance(s__finalExperimentReport__m,s__Predicate) &
           s__finalExperimentReport(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__SymbolicString) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Language) &
         s__instance(V__ARGS2,s__Region))
       =>
       (((s__exactCardinality(s__canonicalPlaceName__m,V__ARG,n__1)
           &
           s__instance(s__canonicalPlaceName__m,s__Predicate) &
           s__canonicalPlaceName(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS5,V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__subclass(V__ARGS5,s__TimeInterval) &
         s__instance(V__ARGS4,s__RealNumber) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__IndustryAttribute) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__sectorCompositionOfGDPInPeriod__m,V__ARG,n__1)
           &
           s__instance(s__sectorCompositionOfGDPInPeriod__m,s__Predicate) &
           s__sectorCompositionOfGDPInPeriod(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
         &
         (V__X = s__ListOrderFn(s__ListFn__4Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__4Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__PlaneAngleMeasure) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Physical) &
         s__instance(V__ARGS2,s__Physical))
       =>
       (((s__exactCardinality(s__courseWRTTrueNorth__m,V__ARG,n__1)
           &
           s__instance(s__courseWRTTrueNorth__m,s__Predicate) &
           s__courseWRTTrueNorth(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__RiskAttribute) &
         s__instance(V__ARGS2,s__Investor))
       =>
       (((s__exactCardinality(s__riskTolerance__m,V__ARG,n__1)
           &
           s__instance(s__riskTolerance__m,s__Predicate) &
           s__riskTolerance(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Quantity) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Integer) &
         s__instance(V__ARGS2,s__Predicate))
       =>
       (((s__exactCardinality(s__defaultMaxValue__m,V__ARG,n__1)
           &
           s__instance(s__defaultMaxValue__m,s__Predicate) &
           s__defaultMaxValue(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__NonnegativeInteger) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__SetOrClass) &
         s__instance(V__ARGS2,s__Collection))
       =>
       (((s__exactCardinality(s__memberTypeCount__m,V__ARG,n__1)
           &
           s__instance(s__memberTypeCount__m,s__Predicate) &
           s__memberTypeCount(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Organization) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__organizationName__m,V__ARG,n__1)
           &
           s__instance(s__organizationName__m,s__Predicate) &
           s__organizationName(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__possesses__m,V__ARG,n__1)
           &
           s__instance(s__possesses__m,s__Predicate) &
           s__possesses(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__GeographicArea) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__agentOperatesInArea__m,V__ARG,n__1)
           &
           s__instance(s__agentOperatesInArea__m,s__Predicate) &
           s__agentOperatesInArea(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__CurrencyMeasure) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__FinancialTransaction) &
         s__instance(V__ARGS2,s__FinancialAccount))
       =>
       (((s__exactCardinality(s__dailyLimit__m,V__ARG,n__1)
           &
           s__instance(s__dailyLimit__m,s__Predicate) &
           s__dailyLimit(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__WearableItem) &
         s__instance(V__ARGS2,s__Animal))
       =>
       (((s__exactCardinality(s__wears__m,V__ARG,n__1)
           &
           s__instance(s__wears__m,s__Predicate) &
           s__wears(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__PositiveInteger) &
         s__instance(V__ARGS2,s__ComputerProgram))
       =>
       (((s__exactCardinality(s__maximumReplications__m,V__ARG,n__1)
           &
           s__instance(s__maximumReplications__m,s__Predicate) &
           s__maximumReplications(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Agent) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CurrencyMeasure) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__bidPrice__m,V__ARG,n__1)
           &
           s__instance(s__bidPrice__m,s__Predicate) &
           s__bidPrice(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS7,V__ARGS6,V__ARGS5,V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS7,s__Class) &
         s__instance(V__ARGS6,s__Class) &
         s__instance(V__ARGS5,s__Class) &
         s__instance(V__ARGS4,s__Class) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Class) &
         s__instance(V__ARGS2,s__Class))
       =>
       (((s__exactCardinality(s__exhaustiveDecomposition__m,V__ARG,n__1)
           &
           s__instance(s__exhaustiveDecomposition__m,s__Predicate) &
           s__exhaustiveDecomposition__6(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7)
         &
         (V__X = s__ListOrderFn(s__ListFn__6Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__6Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Class) &
         s__instance(V__ARGS2,s__Class))
       =>
       (((s__exactCardinality(s__immediateSubclass__m,V__ARG,n__1)
           &
           s__instance(s__immediateSubclass__m,s__Predicate) &
           s__immediateSubclass(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TimeInterval) &
         s__instance(V__ARGS2,s__TimeInterval))
       =>
       (((s__exactCardinality(s__overlapsTemporally__m,V__ARG,n__1)
           &
           s__instance(s__overlapsTemporally__m,s__Predicate) &
           s__overlapsTemporally(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__TransportationDevice))
       =>
       (((s__exactCardinality(s__cargoType__m,V__ARG,n__1)
           &
           s__instance(s__cargoType__m,s__Predicate) &
           s__cargoType(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Experimenting))
       =>
       (((s__exactCardinality(s__experimentalControl__m,V__ARG,n__1)
           &
           s__instance(s__experimentalControl__m,s__Predicate) &
           s__experimentalControl(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__subclass(V__ARGS4,s__TimeInterval) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__RealNumber) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__lowestDecileShareOfHouseholdIncomeInPeriod__m,V__ARG,n__1)
           &
           s__instance(s__lowestDecileShareOfHouseholdIncomeInPeriod__m,s__Predicate) &
           s__lowestDecileShareOfHouseholdIncomeInPeriod(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TimePoint) &
         s__instance(V__ARGS2,s__Agreement))
       =>
       (((s__exactCardinality(s__agreementEffectiveDate__m,V__ARG,n__1)
           &
           s__instance(s__agreementEffectiveDate__m,s__Predicate) &
           s__agreementEffectiveDate(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__GeographicArea))
       =>
       (((s__exactCardinality(s__naturalResourceTypeInArea__m,V__ARG,n__1)
           &
           s__instance(s__naturalResourceTypeInArea__m,s__Predicate) &
           s__naturalResourceTypeInArea(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Recording) &
         s__instance(V__ARGS2,s__Human))
       =>
       (((s__exactCardinality(s__produced__m,V__ARG,n__1)
           &
           s__instance(s__produced__m,s__Predicate) &
           s__produced(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Business) &
         s__instance(V__ARGS2,s__Organization))
       =>
       (((s__exactCardinality(s__businessUnit__m,V__ARG,n__1)
           &
           s__instance(s__businessUnit__m,s__Predicate) &
           s__businessUnit(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__LengthMeasure) &
         s__instance(V__ARGS2,s__Cylinder))
       =>
       (((s__exactCardinality(s__cylinderBore__m,V__ARG,n__1)
           &
           s__instance(s__cylinderBore__m,s__Predicate) &
           s__cylinderBore(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Loan))
       =>
       (((s__exactCardinality(s__loanForPurchase__m,V__ARG,n__1)
           &
           s__instance(s__loanForPurchase__m,s__Predicate) &
           s__loanForPurchase(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__acronym__m,V__ARG,n__1)
           &
           s__instance(s__acronym__m,s__Predicate) &
           s__acronym(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__CurrencyMeasure) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__IndustryAttribute) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__sectorValueOfGDP__m,V__ARG,n__1)
           &
           s__instance(s__sectorValueOfGDP__m,s__Predicate) &
           s__sectorValueOfGDP(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TelecomNumber) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__telecomCode2__m,V__ARG,n__1)
           &
           s__instance(s__telecomCode2__m,s__Predicate) &
           s__telecomCode2(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Formula) &
         s__instance(V__ARGS2,s__Physical))
       =>
       (((s__exactCardinality(s__hasPurpose__m,V__ARG,n__1)
           &
           s__instance(s__hasPurpose__m,s__Predicate) &
           s__hasPurpose(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__PlaneAngleMeasure) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__relativeBearing__m,V__ARG,n__1)
           &
           s__instance(s__relativeBearing__m,s__Predicate) &
           s__relativeBearing(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__SelfConnectedObject) &
         s__instance(V__ARGS2,s__SelfConnectedObject))
       =>
       (((s__exactCardinality(s__surface__m,V__ARG,n__1)
           &
           s__instance(s__surface__m,s__Predicate) &
           s__surface(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__FunctionQuantity) &
         s__instance(V__ARGS2,s__ElectricalTransformer))
       =>
       (((s__exactCardinality(s__voltageRatingPrimary__m,V__ARG,n__1)
           &
           s__instance(s__voltageRatingPrimary__m,s__Predicate) &
           s__voltageRatingPrimary(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Class) &
         s__instance(V__ARGS2,s__Function))
       =>
       (((s__exactCardinality(s__range__m,V__ARG,n__1)
           &
           s__instance(s__range__m,s__Predicate) &
           s__range(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agent) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__alias__m,V__ARG,n__1)
           &
           s__instance(s__alias__m,s__Predicate) &
           s__alias(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CognitiveAgent) &
         s__instance(V__ARGS2,s__FinancialAccount))
       =>
       (((s__exactCardinality(s__administrator__m,V__ARG,n__1)
           &
           s__instance(s__administrator__m,s__Predicate) &
           s__administrator(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Attribute) &
         s__subclass(V__ARGS2,s__Attribute))
       =>
       (((s__exactCardinality(s__exhaustiveAttribute__m,V__ARG,n__1)
           &
           s__instance(s__exhaustiveAttribute__m,s__Predicate) &
           s__exhaustiveAttribute__2(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__MassMeasure) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CorpuscularObject) &
         s__subclass(V__ARGS2,s__Substance))
       =>
       (((s__exactCardinality(s__amount__m,V__ARG,n__1)
           &
           s__instance(s__amount__m,s__Predicate) &
           s__amount(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Formula) &
         s__instance(V__ARGS2,s__CognitiveAgent))
       =>
       (((s__exactCardinality(s__knows__m,V__ARG,n__1)
           &
           s__instance(s__knows__m,s__Predicate) &
           s__knows(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__PhysicalQuantity) &
         s__instance(V__ARGS2,s__PowerSource))
       =>
       (((s__exactCardinality(s__voltageMeasure__m,V__ARG,n__1)
           &
           s__instance(s__voltageMeasure__m,s__Predicate) &
           s__voltageMeasure(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__GeographicArea) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__RealNumber) &
         s__instance(V__ARGS2,s__EthnicGroup))
       =>
       (((s__exactCardinality(s__ethnicityPercentInRegion__m,V__ARG,n__1)
           &
           s__instance(s__ethnicityPercentInRegion__m,s__Predicate) &
           s__ethnicityPercentInRegion(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Formula) &
         s__instance(V__ARGS2,s__CognitiveAgent))
       =>
       (((s__exactCardinality(s__considers__m,V__ARG,n__1)
           &
           s__instance(s__considers__m,s__Predicate) &
           s__considers(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__ComputerProgram) &
         s__instance(V__ARGS2,s__ComputerProgram))
       =>
       (((s__exactCardinality(s__dependencyType__m,V__ARG,n__1)
           &
           s__instance(s__dependencyType__m,s__Predicate) &
           s__dependencyType(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Human) &
         s__instance(V__ARGS2,s__PermanentResidence))
       =>
       (((s__exactCardinality(s__homeAddress__m,V__ARG,n__1)
           &
           s__instance(s__homeAddress__m,s__Predicate) &
           s__homeAddress(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__PhysicalDimension) &
         s__instance(V__ARGS2,s__MultipoleQuantity))
       =>
       (((s__exactCardinality(s__hasDimension__m,V__ARG,n__1)
           &
           s__instance(s__hasDimension__m,s__Predicate) &
           s__hasDimension(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__FinancialCompany) &
         s__instance(V__ARGS2,s__FinancialAccount))
       =>
       (((s__exactCardinality(s__financialAccount__m,V__ARG,n__1)
           &
           s__instance(s__financialAccount__m,s__Predicate) &
           s__financialAccount(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__IPAddress) &
         s__instance(V__ARGS2,s__TimePosition))
       =>
       (((s__exactCardinality(s__monitorConnectivityData__m,V__ARG,n__1)
           &
           s__instance(s__monitorConnectivityData__m,s__Predicate) &
           s__monitorConnectivityData(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agent) &
         s__instance(V__ARGS2,s__PlacingUnderArrest))
       =>
       (((s__exactCardinality(s__arrested__m,V__ARG,n__1)
           &
           s__instance(s__arrested__m,s__Predicate) &
           s__arrested(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__NonnegativeInteger) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agent) &
         s__instance(V__ARGS2,s__Organization))
       =>
       (((s__exactCardinality(s__seatsHeldInOrganization__m,V__ARG,n__1)
           &
           s__instance(s__seatsHeldInOrganization__m,s__Predicate) &
           s__seatsHeldInOrganization(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__RealNumber) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__militaryExpendituresFractionOfGDP__m,V__ARG,n__1)
           &
           s__instance(s__militaryExpendituresFractionOfGDP__m,s__Predicate) &
           s__militaryExpendituresFractionOfGDP(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__FunctionQuantity) &
         s__instance(V__ARGS2,s__ElectricalTransformer))
       =>
       (((s__exactCardinality(s__voltageRatingSecondary__m,V__ARG,n__1)
           &
           s__instance(s__voltageRatingSecondary__m,s__Predicate) &
           s__voltageRatingSecondary(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TimeInterval) &
         s__instance(V__ARGS2,s__PricingScheme))
       =>
       (((s__exactCardinality(s__validityPeriod__m,V__ARG,n__1)
           &
           s__instance(s__validityPeriod__m,s__Predicate) &
           s__validityPeriod(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agent) &
         s__subclass(V__ARGS2,s__Process))
       =>
       (((s__exactCardinality(s__hasSkill__m,V__ARG,n__1)
           &
           s__instance(s__hasSkill__m,s__Predicate) &
           s__hasSkill(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__LengthMeasure) &
         s__instance(V__ARGS2,s__Radiating))
       =>
       (((s__exactCardinality(s__wavelength__m,V__ARG,n__1)
           &
           s__instance(s__wavelength__m,s__Predicate) &
           s__wavelength(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS2,s__HotelFunctionRoom))
       =>
       (((s__exactCardinality(s__freeFunctionRoomAmenity__m,V__ARG,n__1)
           &
           s__instance(s__freeFunctionRoomAmenity__m,s__Predicate) &
           s__freeFunctionRoomAmenity(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__TimeInterval) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Interest) &
         s__instance(V__ARGS2,s__FinancialAccount))
       =>
       (((s__exactCardinality(s__compoundInterest__m,V__ARG,n__1)
           &
           s__instance(s__compoundInterest__m,s__Predicate) &
           s__compoundInterest(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CognitiveAgent) &
         s__instance(V__ARGS2,s__ServiceProcess))
       =>
       (((s__exactCardinality(s__serviceRecipient__m,V__ARG,n__1)
           &
           s__instance(s__serviceRecipient__m,s__Predicate) &
           s__serviceRecipient(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__WebSite) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Formula) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__visitorParameter__m,V__ARG,n__1)
           &
           s__instance(s__visitorParameter__m,s__Predicate) &
           s__visitorParameter(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TimeDuration) &
         s__instance(V__ARGS2,s__ComputerProgram))
       =>
       (((s__exactCardinality(s__softwareHeartBeatRate__m,V__ARG,n__1)
           &
           s__instance(s__softwareHeartBeatRate__m,s__Predicate) &
           s__softwareHeartBeatRate(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__SymbolicString) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__SymbolicString) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__nameAfterKeyName__m,V__ARG,n__1)
           &
           s__instance(s__nameAfterKeyName__m,s__Predicate) &
           s__nameAfterKeyName(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Policy) &
         s__instance(V__ARGS2,s__RoomInventory))
       =>
       (((s__exactCardinality(s__someRoomsPolicy__m,V__ARG,n__1)
           &
           s__instance(s__someRoomsPolicy__m,s__Predicate) &
           s__someRoomsPolicy(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__Object))
       =>
       (((s__exactCardinality(s__third__m,V__ARG,n__1)
           &
           s__instance(s__third__m,s__Predicate) &
           s__third(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TerrainAttribute) &
         s__instance(V__ARGS2,s__GeographicArea))
       =>
       (((s__exactCardinality(s__terrainInArea__m,V__ARG,n__1)
           &
           s__instance(s__terrainInArea__m,s__Predicate) &
           s__terrainInArea(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__subclass(V__ARGS4,s__TimeInterval) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CurrencyMeasure) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__exportTotalInPeriod__m,V__ARG,n__1)
           &
           s__instance(s__exportTotalInPeriod__m,s__Predicate) &
           s__exportTotalInPeriod(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__TimeInterval) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CurrencyMeasure) &
         s__instance(V__ARGS2,s__Human))
       =>
       (((s__exactCardinality(s__income__m,V__ARG,n__1)
           &
           s__instance(s__income__m,s__Predicate) &
           s__income(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agent) &
         s__instance(V__ARGS2,s__Process))
       =>
       (((s__exactCardinality(s__benefits__m,V__ARG,n__1)
           &
           s__instance(s__benefits__m,s__Predicate) &
           s__benefits(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Physical) &
         s__instance(V__ARGS2,s__Physical))
       =>
       (((s__exactCardinality(s__nearOrientation__m,V__ARG,n__1)
           &
           s__instance(s__nearOrientation__m,s__Predicate) &
           s__nearOrientation(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__FinancialRating) &
         s__instance(V__ARGS2,s__CognitiveAgent))
       =>
       (((s__exactCardinality(s__creditRanking__m,V__ARG,n__1)
           &
           s__instance(s__creditRanking__m,s__Predicate) &
           s__creditRanking(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS6,V__ARGS5,V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   ((s__instance(V__ARG,s__PositiveInteger) =>
       (((s__exactCardinality(s__processList__m,V__ARG,n__1)
           &
           s__instance(s__processList__m,s__Predicate) &
           s__processList__5(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6)
         &
         (V__X = s__ListOrderFn(s__ListFn__5Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__5Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__subclass(V__ARGS4,s__TimeInterval) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__RealNumber) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__highestDecileShareOfHouseholdIncomeInPeriod__m,V__ARG,n__1)
           &
           s__instance(s__highestDecileShareOfHouseholdIncomeInPeriod__m,s__Predicate) &
           s__highestDecileShareOfHouseholdIncomeInPeriod(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__WebListing) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__viewedListing__m,V__ARG,n__1)
           &
           s__instance(s__viewedListing__m,s__Predicate) &
           s__viewedListing(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Human) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__leader__m,V__ARG,n__1)
           &
           s__instance(s__leader__m,s__Predicate) &
           s__leader(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TimeInterval) &
         s__instance(V__ARGS2,s__StationaryArtifact))
       =>
       (((s__exactCardinality(s__constructionPeriod__m,V__ARG,n__1)
           &
           s__instance(s__constructionPeriod__m,s__Predicate) &
           s__constructionPeriod(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Language) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Word) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__spellingInLanguage__m,V__ARG,n__1)
           &
           s__instance(s__spellingInLanguage__m,s__Predicate) &
           s__spellingInLanguage(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Organism) &
         s__instance(V__ARGS2,s__Organism))
       =>
       (((s__exactCardinality(s__parent__m,V__ARG,n__1)
           &
           s__instance(s__parent__m,s__Predicate) &
           s__parent(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TemperatureMeasure) &
         s__subclass(V__ARGS2,s__PureSubstance))
       =>
       (((s__exactCardinality(s__meltingPoint__m,V__ARG,n__1)
           &
           s__instance(s__meltingPoint__m,s__Predicate) &
           s__meltingPoint(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Process) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__activityCapability__m,V__ARG,n__1)
           &
           s__instance(s__activityCapability__m,s__Predicate) &
           s__activityCapability(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__LengthMeasure) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Physical) &
         s__instance(V__ARGS2,s__Physical))
       =>
       (((s__exactCardinality(s__altitude__m,V__ARG,n__1)
           &
           s__instance(s__altitude__m,s__Predicate) &
           s__altitude(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Agent) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__SocialRole) &
         s__instance(V__ARGS2,s__Election))
       =>
       (((s__exactCardinality(s__electionWinner__m,V__ARG,n__1)
           &
           s__instance(s__electionWinner__m,s__Predicate) &
           s__electionWinner(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__AreaMeasure) &
         s__instance(V__ARGS2,s__GeographicArea))
       =>
       (((s__exactCardinality(s__landAreaOnly__m,V__ARG,n__1)
           &
           s__instance(s__landAreaOnly__m,s__Predicate) &
           s__landAreaOnly(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__ContentBearingPhysical) &
         s__instance(V__ARGS2,s__ContentBearingPhysical))
       =>
       (((s__exactCardinality(s__subsumesContentInstance__m,V__ARG,n__1)
           &
           s__instance(s__subsumesContentInstance__m,s__Predicate) &
           s__subsumesContentInstance(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__PhysicalQuantity) &
         s__instance(V__ARGS2,s__WaterVehicle))
       =>
       (((s__exactCardinality(s__vesselGrossRegisteredTonnage__m,V__ARG,n__1)
           &
           s__instance(s__vesselGrossRegisteredTonnage__m,s__Predicate) &
           s__vesselGrossRegisteredTonnage(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Policy) &
         s__subclass(V__ARGS2,s__HotelUnit))
       =>
       (((s__exactCardinality(s__roomPolicy__m,V__ARG,n__1)
           &
           s__instance(s__roomPolicy__m,s__Predicate) &
           s__roomPolicy(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   ((s__instance(V__ARG,s__PositiveInteger) =>
       (((s__exactCardinality(s__refers__m,V__ARG,n__1)
           &
           s__instance(s__refers__m,s__Predicate) &
           s__refers(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Language) &
         s__instance(V__ARGS2,s__Language))
       =>
       (((s__exactCardinality(s__subLanguage__m,V__ARG,n__1)
           &
           s__instance(s__subLanguage__m,s__Predicate) &
           s__subLanguage(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__VolumeMeasure) &
         s__instance(V__ARGS2,s__IntermittentCombustionEngine))
       =>
       (((s__exactCardinality(s__engineDisplacement__m,V__ARG,n__1)
           &
           s__instance(s__engineDisplacement__m,s__Predicate) &
           s__engineDisplacement(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CurrencyMeasure) &
         s__instance(V__ARGS2,s__FinancialAccount))
       =>
       (((s__exactCardinality(s__originalBalance__m,V__ARG,n__1)
           &
           s__instance(s__originalBalance__m,s__Predicate) &
           s__originalBalance(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__PhysicalDomain) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__PhysicalDimension) &
         s__instance(V__ARGS2,s__PhysicalDimension))
       =>
       (((s__exactCardinality(s__physicalDomain__m,V__ARG,n__1)
           &
           s__instance(s__physicalDomain__m,s__Predicate) &
           s__physicalDomain(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__PositiveInteger) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__importCommodityTypeByRank__m,V__ARG,n__1)
           &
           s__instance(s__importCommodityTypeByRank__m,s__Predicate) &
           s__importCommodityTypeByRank(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Human) &
         s__instance(V__ARGS2,s__Human))
       =>
       (((s__exactCardinality(s__acquaintance__m,V__ARG,n__1)
           &
           s__instance(s__acquaintance__m,s__Predicate) &
           s__acquaintance(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Contest) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CognitiveAgent))
       =>
       (((s__exactCardinality(s__contestEntry__m,V__ARG,n__1)
           &
           s__instance(s__contestEntry__m,s__Predicate) &
           s__contestEntry(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__IntentionalProcess) &
         s__instance(V__ARGS2,s__Organization))
       =>
       (((s__exactCardinality(s__organizationServiceType__m,V__ARG,n__1)
           &
           s__instance(s__organizationServiceType__m,s__Predicate) &
           s__organizationServiceType(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TimeDuration) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__suffrageAgeMinimum__m,V__ARG,n__1)
           &
           s__instance(s__suffrageAgeMinimum__m,s__Predicate) &
           s__suffrageAgeMinimum(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__TimeDuration) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CurrencyMeasure) &
         s__instance(V__ARGS2,s__FinancialAccount))
       =>
       (((s__exactCardinality(s__periodicPayment__m,V__ARG,n__1)
           &
           s__instance(s__periodicPayment__m,s__Predicate) &
           s__periodicPayment(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__subclass(V__ARGS4,s__Process) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__BiologicallyActiveSubstance) &
         s__instance(V__ARGS2,s__DiseaseOrSyndrome))
       =>
       (((s__exactCardinality(s__diseaseTreatment__m,V__ARG,n__1)
           &
           s__instance(s__diseaseTreatment__m,s__Predicate) &
           s__diseaseTreatment(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__WebSite) &
         s__instance(V__ARGS2,s__Database))
       =>
       (((s__exactCardinality(s__siteCatalog__m,V__ARG,n__1)
           &
           s__instance(s__siteCatalog__m,s__Predicate) &
           s__siteCatalog(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS5,V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS5,s__TimeInterval) &
         s__instance(V__ARGS4,s__Object) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CognitiveAgent) &
         s__instance(V__ARGS2,s__CognitiveAgent))
       =>
       (((s__exactCardinality(s__rents__m,V__ARG,n__1)
           &
           s__instance(s__rents__m,s__Predicate) &
           s__rents(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
         &
         (V__X = s__ListOrderFn(s__ListFn__4Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__4Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CurrencyMeasure) &
         s__instance(V__ARGS2,s__Loan))
       =>
       (((s__exactCardinality(s__loanInterest__m,V__ARG,n__1)
           &
           s__instance(s__loanInterest__m,s__Predicate) &
           s__loanInterest(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Formula) &
         s__instance(V__ARGS2,s__Formula))
       =>
       (((s__exactCardinality(s__independentProbability__m,V__ARG,n__1)
           &
           s__instance(s__independentProbability__m,s__Predicate) &
           s__independentProbability(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Day) &
         s__instance(V__ARGS2,s__BankStatement))
       =>
       (((s__exactCardinality(s__dateOfStatement__m,V__ARG,n__1)
           &
           s__instance(s__dateOfStatement__m,s__Predicate) &
           s__dateOfStatement(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__TemperatureMeasure) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TimeDuration) &
         s__instance(V__ARGS2,s__GeographicArea))
       =>
       (((s__exactCardinality(s__highestTemperatureForPeriod__m,V__ARG,n__1)
           &
           s__instance(s__highestTemperatureForPeriod__m,s__Predicate) &
           s__highestTemperatureForPeriod(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TwoDimensionalObject) &
         s__instance(V__ARGS2,s__OneDimensionalFigure))
       =>
       (((s__exactCardinality(s__tangent__m,V__ARG,n__1)
           &
           s__instance(s__tangent__m,s__Predicate) &
           s__tangent(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Proposition) &
         s__instance(V__ARGS2,s__Argument))
       =>
       (((s__exactCardinality(s__conclusion__m,V__ARG,n__1)
           &
           s__instance(s__conclusion__m,s__Predicate) &
           s__conclusion(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__Organism))
       =>
       (((s__exactCardinality(s__fathersBrothersSon__m,V__ARG,n__1)
           &
           s__instance(s__fathersBrothersSon__m,s__Predicate) &
           s__fathersBrothersSon(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Class) &
         s__instance(V__ARGS2,s__Class))
       =>
       (((s__exactCardinality(s__subclass__m,V__ARG,n__1)
           &
           s__instance(s__subclass__m,s__Predicate) &
           s__subclass(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__PositiveInteger) &
         s__instance(V__ARGS2,s__ComputerProgram))
       =>
       (((s__exactCardinality(s__portNumber__m,V__ARG,n__1)
           &
           s__instance(s__portNumber__m,s__Predicate) &
           s__portNumber(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Organism))
       =>
       (((s__exactCardinality(s__inhabits__m,V__ARG,n__1)
           &
           s__instance(s__inhabits__m,s__Predicate) &
           s__inhabits(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__NaturalSubstance) &
         s__subclass(V__ARGS2,s__OrganicObject))
       =>
       (((s__exactCardinality(s__secretesSubstance__m,V__ARG,n__1)
           &
           s__instance(s__secretesSubstance__m,s__Predicate) &
           s__secretesSubstance(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__FinancialInstrument) &
         s__instance(V__ARGS2,s__Agreement))
       =>
       (((s__exactCardinality(s__underlier__m,V__ARG,n__1)
           &
           s__instance(s__underlier__m,s__Predicate) &
           s__underlier(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__GUIElement) &
         s__instance(V__ARGS2,s__UncoveringGraphicalWindow))
       =>
       (((s__exactCardinality(s__guiElementUncovered__m,V__ARG,n__1)
           &
           s__instance(s__guiElementUncovered__m,s__Predicate) &
           s__guiElementUncovered(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Animal))
       =>
       (((s__exactCardinality(s__grasps__m,V__ARG,n__1)
           &
           s__instance(s__grasps__m,s__Predicate) &
           s__grasps(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Language) &
         s__instance(V__ARGS2,s__LinguisticExpression))
       =>
       (((s__exactCardinality(s__expressedInLanguage__m,V__ARG,n__1)
           &
           s__instance(s__expressedInLanguage__m,s__Predicate) &
           s__expressedInLanguage(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Integer) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Satellite) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__communicationSatelliteForArea__m,V__ARG,n__1)
           &
           s__instance(s__communicationSatelliteForArea__m,s__Predicate) &
           s__communicationSatelliteForArea(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__LengthMeasure) &
         s__instance(V__ARGS2,s__OneDimensionalFigure))
       =>
       (((s__exactCardinality(s__lineMeasure__m,V__ARG,n__1)
           &
           s__instance(s__lineMeasure__m,s__Predicate) &
           s__lineMeasure(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Class))
       =>
       (((s__exactCardinality(s__instance__m,V__ARG,n__1)
           &
           s__instance(s__instance__m,s__Predicate) &
           s__instance(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__ShapeAttribute) &
         s__instance(V__ARGS2,s__Physical))
       =>
       (((s__exactCardinality(s__shape__m,V__ARG,n__1)
           &
           s__instance(s__shape__m,s__Predicate) &
           s__shape(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__LengthMeasure) &
         s__instance(V__ARGS2,s__Railway))
       =>
       (((s__exactCardinality(s__trackWidth__m,V__ARG,n__1)
           &
           s__instance(s__trackWidth__m,s__Predicate) &
           s__trackWidth(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS2,s__HotelUnit))
       =>
       (((s__exactCardinality(s__paidRoomAmenity__m,V__ARG,n__1)
           &
           s__instance(s__paidRoomAmenity__m,s__Predicate) &
           s__paidRoomAmenity(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TransitSystem) &
         s__instance(V__ARGS2,s__Region))
       =>
       (((s__exactCardinality(s__routeEnd__m,V__ARG,n__1)
           &
           s__instance(s__routeEnd__m,s__Predicate) &
           s__routeEnd(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__RealNumber) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__DirectionalAttribute) &
         s__instance(V__ARGS2,s__LandArea))
       =>
       (((s__exactCardinality(s__slopeGradientTowardsOrientation__m,V__ARG,n__1)
           &
           s__instance(s__slopeGradientTowardsOrientation__m,s__Predicate) &
           s__slopeGradientTowardsOrientation(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__PhysicalQuantity) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__annualElectricityConsumption__m,V__ARG,n__1)
           &
           s__instance(s__annualElectricityConsumption__m,s__Predicate) &
           s__annualElectricityConsumption(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__RoomInventory))
       =>
       (((s__exactCardinality(s__someRoomsPhysicalAmenity__m,V__ARG,n__1)
           &
           s__instance(s__someRoomsPhysicalAmenity__m,s__Predicate) &
           s__someRoomsPhysicalAmenity(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agent) &
         s__instance(V__ARGS2,s__TelephonyDevice))
       =>
       (((s__exactCardinality(s__telecomContactDevice__m,V__ARG,n__1)
           &
           s__instance(s__telecomContactDevice__m,s__Predicate) &
           s__telecomContactDevice(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__CurrencyMeasure) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Day) &
         s__instance(V__ARGS2,s__FinancialAccount))
       =>
       (((s__exactCardinality(s__marginBalanceAmount__m,V__ARG,n__1)
           &
           s__instance(s__marginBalanceAmount__m,s__Predicate) &
           s__marginBalanceAmount(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__GeopoliticalArea) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__administrativeCenter__m,V__ARG,n__1)
           &
           s__instance(s__administrativeCenter__m,s__Predicate) &
           s__administrativeCenter(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Collection) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__WebSite) &
         s__instance(V__ARGS2,s__TimeInterval))
       =>
       (((s__exactCardinality(s__firstTimeBuyers__m,V__ARG,n__1)
           &
           s__instance(s__firstTimeBuyers__m,s__Predicate) &
           s__firstTimeBuyers(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Agent) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CurrencyMeasure) &
         s__instance(V__ARGS2,s__Physical))
       =>
       (((s__exactCardinality(s__price__m,V__ARG,n__1)
           &
           s__instance(s__price__m,s__Predicate) &
           s__price(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__subclass(V__ARGS4,s__TimeInterval) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__RealNumber) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__inflationRateOfConsumerPricesInPeriod__m,V__ARG,n__1)
           &
           s__instance(s__inflationRateOfConsumerPricesInPeriod__m,s__Predicate) &
           s__inflationRateOfConsumerPricesInPeriod(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Agent) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Position) &
         s__instance(V__ARGS2,s__Agent))
       =>
       (((s__exactCardinality(s__diplomaticRepresentationType__m,V__ARG,n__1)
           &
           s__instance(s__diplomaticRepresentationType__m,s__Predicate) &
           s__diplomaticRepresentationType(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Agent) &
         s__instance(V__ARGS2,s__Process))
       =>
       (((s__exactCardinality(s__experiencer__m,V__ARG,n__1)
           &
           s__instance(s__experiencer__m,s__Predicate) &
           s__experiencer(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__Transfer))
       =>
       (((s__exactCardinality(s__passenger__m,V__ARG,n__1)
           &
           s__instance(s__passenger__m,s__Predicate) &
           s__passenger(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__Object) &
         s__instance(V__ARGS2,s__Organization))
       =>
       (((s__exactCardinality(s__organizationProductType__m,V__ARG,n__1)
           &
           s__instance(s__organizationProductType__m,s__Predicate) &
           s__organizationProductType(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TransportationDevice) &
         s__instance(V__ARGS2,s__Transportation))
       =>
       (((s__exactCardinality(s__conveyance__m,V__ARG,n__1)
           &
           s__instance(s__conveyance__m,s__Predicate) &
           s__conveyance(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Substance) &
         s__instance(V__ARGS2,s__ChemicalProcess))
       =>
       (((s__exactCardinality(s__reactant__m,V__ARG,n__1)
           &
           s__instance(s__reactant__m,s__Predicate) &
           s__reactant(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__CurrencyMeasure) &
         s__instance(V__ARGS2,s__GeopoliticalArea))
       =>
       (((s__exactCardinality(s__perCapitaGDP__m,V__ARG,n__1)
           &
           s__instance(s__perCapitaGDP__m,s__Predicate) &
           s__perCapitaGDP(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__SystemBehaviorAttribute) &
         s__instance(V__ARGS2,s__RealtimeSystem))
       =>
       (((s__exactCardinality(s__systemBehavior__m,V__ARG,n__1)
           &
           s__instance(s__systemBehavior__m,s__Predicate) &
           s__systemBehavior(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TemperatureMeasure) &
         s__subclass(V__ARGS2,s__PureSubstance))
       =>
       (((s__exactCardinality(s__boilingPoint__m,V__ARG,n__1)
           &
           s__instance(s__boilingPoint__m,s__Predicate) &
           s__boilingPoint(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Interest) &
         s__instance(V__ARGS2,s__Bond))
       =>
       (((s__exactCardinality(s__accruedInterest__m,V__ARG,n__1)
           &
           s__instance(s__accruedInterest__m,s__Predicate) &
           s__accruedInterest(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__Language) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS2,s__SymbolicString))
       =>
       (((s__exactCardinality(s__displayTitle__m,V__ARG,n__1)
           &
           s__instance(s__displayTitle__m,s__Predicate) &
           s__displayTitle(V__ARGS2,V__ARGS3,V__ARGS4)
         &
         (V__X = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__3Fn(V__ARGS2,V__ARGS3,V__ARGS4)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__TimeDuration) &
         s__instance(V__ARGS2,s__RealtimeSystem))
       =>
       (((s__exactCardinality(s__granularity__m,V__ARG,n__1)
           &
           s__instance(s__granularity__m,s__Predicate) &
           s__granularity(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS7,V__ARGS6,V__ARGS5,V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS7,s__Attribute) &
         s__instance(V__ARGS6,s__Attribute) &
         s__instance(V__ARGS5,s__Attribute) &
         s__instance(V__ARGS4,s__Attribute) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Attribute) &
         s__subclass(V__ARGS2,s__Attribute))
       =>
       (((s__exactCardinality(s__exhaustiveAttribute__m,V__ARG,n__1)
           &
           s__instance(s__exhaustiveAttribute__m,s__Predicate) &
           s__exhaustiveAttribute__6(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7)
         &
         (V__X = s__ListOrderFn(s__ListFn__6Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__6Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Attribute) &
         s__instance(V__ARGS2,s__Attribute))
       =>
       (((s__exactCardinality(s__successorAttributeClosure__m,V__ARG,n__1)
           &
           s__instance(s__successorAttributeClosure__m,s__Predicate) &
           s__successorAttributeClosure(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Organism) &
         s__instance(V__ARGS2,s__Organism))
       =>
       (((s__exactCardinality(s__son__m,V__ARG,n__1)
           &
           s__instance(s__son__m,s__Predicate) &
           s__son(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARG,s__PositiveInteger) &
         s__instance(V__ARGS3,s__Physical) &
         s__instance(V__ARGS2,s__Abstract))
       =>
       (((s__exactCardinality(s__abstractCounterpart__m,V__ARG,n__1)
           &
           s__instance(s__abstractCounterpart__m,s__Predicate) &
           s__abstractCounterpart(V__ARGS2,V__ARGS3)
         &
         (V__X = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
        ,V__ARG))
     &
     (V__Y = s__ListOrderFn(s__ListFn__2Fn(V__ARGS2,V__ARGS3)
    ,V__ARG)))
=>
((V__X = V__Y)))))
)
)

( ! [V__ARGS4,V__X,V__ARG,V__Y,V__ARGS3,V__ARGS2] :
   (((s__instance(V__ARGS4,s__GeopoliticalArea) &
         s__instance(V__ARG,s__PositiveInteger) &
         s__subclass(V__ARGS3,s__IllicitDrug) &