MELD features/Appendix A/2

From Public Domain Knowledge Bank
Jump to: navigation, search
<< MELD features/Appendix A/1 MELD features >> MELD features/Appendix A/3

Contents

History

  • version 1 put ASSERTION-num in for Assertions
  • version 2 put CONSTANT-num in for Constants


    • name Assertion-### for each assertion

Appendix A: Formulas true in every MELD KB

As we remarked above, the syntactic component of MELD includes a large number of constant terms (you can think of these as "reserved words" in the MELD language), and the semantic component of MELD includes a large number of sentences involving and interrelating these terms. This set of sentences forms a coherent self-sufficient KB -- the MELD_features/A -- which forms the upper (most general) part of every MELD KB, including, e.g., the Cyc KB, the HPKB IKB, etc.

Herewith is that list of approximately 650 sentences -- each is a closed, well-formed MELD formula.

All of the MELD constants mentioned in these assertions should be thought of as MELD "reserved words." These terms, of which there are about 160, occur below on comment lines, just before the set of mandatory formulas involving them; each of those comment lines begins with three semicolons in a row; e.g., ;;; CONSTANT-001 #$AntiSymmetricBinaryPredicate.

The formulas, and terms, are not commented or explained, below. If one browses through the Cyc KB or the HPKB IKB, one can read the documentation for each of these terms, etc. That is how you, a human reader, can most easily become familiar with the ontology and the semantics of MELD. Just as the BNF in Appendix C, the long list of formulas below (here in Appendix B) is provided more to be machine- than human- readable.

We've arranged these in such a fashion that (most) duplicates have been eliminated. Thus, in the case of one of the first few assertions,

(#$genls  #$AntiSymmetricBinaryPredicate #$BinaryPredicate), 

that assertion is listed once, under ;;; CONSTANT-001 #$AntiSymmetricBinaryPredicate, not again under ;;; #$BinaryPredicate.

We've prefixed each MELD term with the characters #$. This may facilitate reading mechanically; if you don't care or want this, just do a systematic replace of #$ by the empty string. It will be useful in distinguishing MELD constant names from the names of C (or Lisp) functions which are called to implement some of the low-level bookkeeping, and may be useful in distinguishing MELD constant names from numbers (e.g., distinguishing the MELD constant named 42 from the number 42.)

Let us reiterate that MELD is a declarative language with no procedural information of any kind in any MELD formula, including these formulas.

Finally, you may notice that about 10 of the 160 MELD constant terms below contain the word "Cyc"; this reflects the origins of those terms. We could just as well have called those ten . . .Cyc. . . terms . . .MELD. . . instead; the absolute names are not so important as agreeing on a fixed vocabulary of names for constants.

This is the MELD semantic standard; please do not rename any of these 160 terms, or remove/violate any of these 650 formulas:


;;; CONSTANT-001 #$AntiSymmetricBinaryPredicate

ASSERTION-001
(#$isa  #$AntiSymmetricBinaryPredicate #$Collection )
ASSERTION-002
(#$genls  #$AntiSymmetricBinaryPredicate #$BinaryPredicate )
ASSERTION-003
(#$implies 
   (#$and 
      (#$isa ?SLOT  #$AntiSymmetricBinaryPredicate) 
      (#$isa ?SLOT #$IrreflexiveBinaryPredicate) ) 
   (#$isa ?SLOT #$AsymmetricBinaryPredicate)
)

;;; #$Assertion

ASSERTION-004
(#$isa  #$Assertion #$Collection)
ASSERTION-005
(#$genls  #$Assertion #$CycIndexedTerm)
ASSERTION-006
(#$genls  #$Assertion #$IndividualObject)


;;; #$AsymmetricBinaryPredicate

ASSERTION-007
(#$isa #$AsymmetricBinaryPredicate #$Collection )
ASSERTION-008
(#$genls #$AsymmetricBinaryPredicate  #$AntiSymmetricBinaryPredicate )
ASSERTION-009
(#$genls #$AsymmetricBinaryPredicate]] #$IrreflexiveBinaryPredicate )
ASSERTION-010
(#$not (#$and 
     (#$isa ?PRED #$AsymmetricBinaryPredicate) 
     (?PRED ?ARG1 ?ARG2) 
     (?PRED ?ARG2 ?ARG1)
                       ) )
ASSERTION-011
(#$implies 
   (#$and 
      (#$isa ?Q #$AsymmetricBinaryPredicate) 
      (#$genlPreds ?P ?Q)
   ) 
   (#$isa ?P #$AsymmetricBinaryPredicate)
)
ASSERTION-012
(#$implies 
    (#$isa ?PRED #$AsymmetricBinaryPredicate) 
    (#$negationInverse ?PRED ?PRED)
)

;;; #$AttributeValue

ASSERTION-013
(#$isa #$AttributeValue #$Collection)
ASSERTION-014
(#$genls #$AttributeValue #$IndividualObject)

;;; #$BaseKB

ASSERTION-015
(#$isa #$BaseKB #$BroadMicrotheory)
ASSERTION-016
(#$implies 
   (#$isa ?MIC #$Microtheory) 
   (#$genlMt ?MIC #$BaseKB)
)

;;; #$BinaryPredicate

ASSERTION-017
(#$isa #$BinaryPredicate #$Collection)
ASSERTION-018
(#$genls #$BinaryPredicate #$Predicate)
ASSERTION-019
(#$implies 
    (#$isa ?P #$BinaryPredicate) 
    (#$arity ?P 2 )
)

;;; #$BookkeepingMt

ASSERTION-020
(#$isa #$BookkeepingMt #$Microtheory)
ASSERTION-021
(#$genlMt #$BookkeepingMt #$CyclistsMt)
ASSERTION-022
(#$genlMt #$BookkeepingMt #$BaseKB)

;;; #$BookkeepingPredicate

ASSERTION-023
(#$isa #$BookkeepingPredicate #$Collection)
ASSERTION-024
(#$genls #$BookkeepingPredicate #$Predicate)

;;; #$BroadMicrotheory

ASSERTION-025
(#$isa #$BroadMicrotheory #$Collection)
ASSERTION-026
(#$genls #$BroadMicrotheory #$Microtheory)

;;; #$Collection

see also  ASSERTION-023. ASSERTION-025
ASSERTION-027
(#$isa #$Collection #$Collection)
ASSERTION-028
(#$genls #$Collection #$SetOrCollection)

;;; #$CollectionDenotingFunction

ASSERTION-029
(#$isa #$CollectionDenotingFunction #$Collection)
ASSERTION-030
(#$genls #$CollectionDenotingFunction #$ReifiableFunction )

;;; #$CommutativeRelation

ASSERTION-031
(#$isa #$CommutativeRelation #$Collection)
ASSERTION-032
(#$genls #$CommutativeRelation #$Relationship)

;;; #$CycELVariable

ASSERTION-033
(#$isa #$CycELVariable #$Collection)
ASSERTION-034
(#$genls #$CycELVariable #$CycSystemSymbol)

;;; #$CycExpression

ASSERTION-035
(#$isa #$CycExpression #$Collection )
ASSERTION-036
(#$genls #$CycExpression #$IndividualObject)

;;; #$CycFormula

ASSERTION-037
(#$isa #$CycFormula #$Collection)
ASSERTION-038
(#$genls #$CycFormula #$CycExpression)

;;; #$CycIndexedTerm

ASSERTION-039
(#$isa #$CycIndexedTerm #$Collection)
ASSERTION-040
(#$genls #$CycIndexedTerm]] #$Thing)

;;; #$CycSystemList

ASSERTION-041
(#$isa #$CycSystemList #$Collection)
ASSERTION-042
(#$genls #$CycSystemList #$IndividualObject)

;;; #$CycSystemString

ASSERTION-043
(#$isa #$CycSystemString #$Collection)
ASSERTION-044
(#$genls #$CycSystemString #$IndividualObject)

;;; #$CycSystemSymbol

ASSERTION-045
(#$isa #$CycSystemSymbol #$Collection)
ASSERTION-046
(#$genls #$CycSystemSymbol #$IndividualObject )

;;; #$Cyclist

ASSERTION-047
(#$isa #$Cyclist #$Collection )
ASSERTION-048
(#$genls #$Cyclist #$TemporalObject )

;;; #$CyclistsMt

ASSERTION-049
(#$isa #$CyclistsMt #$Microtheory )
ASSERTION-050
(#$genlMt #$CyclistsMt #$BaseKB)

;;; #$DefaultMonotonicPredicate

ASSERTION-051
(#$isa #$DefaultMonotonicPredicate #$Collection)
ASSERTION-052
(#$genls #$DefaultMonotonicPredicate #$Predicate)

;;; #$EvaluatableFunction

ASSERTION-053
(#$isa #$EvaluatableFunction #$Collection)
ASSERTION-054
(#$genls #$EvaluatableFunction #$FunctionTheMathematicalType )

;;; #$False

ASSERTION-055
(#$isa #$False #$IndividualObject )

;;; #$Format

ASSERTION-056
(#$isa #$Format #$Collection )
ASSERTION-057
(#$genls #$Format #$IndividualObject )

;;; #$ForwardInferencePSC

ASSERTION-058
(#$isa #$ForwardInferencePSC #$ProblemSolvingCntxt )
ASSERTION-059
(#$genlMt #$ForwardInferencePSC #$BaseKB)


;;; #$FunctionTheMathematicalType

ASSERTION-060
(#$isa #$FunctionTheMathematicalType #$Collection)
ASSERTION-061
(#$genls #$FunctionTheMathematicalType #$Relationship)

;;; #$Guest

ASSERTION-062
(#$isa #$Guest #$HumanCyclist ) 

;;; #$HumanCyclist

ASSERTION-063
(#$isa #$HumanCyclist #$Collection )
ASSERTION-064
(#$genls #$HumanCyclist #$Cyclist )

;;; #$IndividualObject

ASSERTION-065
(#$isa #$IndividualObject #$Collection )
ASSERTION-066
(#$genls #$IndividualObject #$Thing )

;;; #$InferenceRelatedBookkeepingPredicate

ASSERTION-067
(#$isa #$InferenceRelatedBookkeepingPredicate #$Collection )
ASSERTION-068
(#$genls #$InferenceRelatedBookkeepingPredicate #$BookkeepingPredicate )

;;; #$Integer

ASSERTION-069
(#$isa #$Integer #$Collection )
ASSERTION-070
( #$genls #$Integer #$RealNumber )


;;; #$IntervalEntry

ASSERTION-071
( #$isa #$IntervalEntry #$Format)

;;; #$IrreflexiveBinaryPredicate

ASSERTION-072
( #$isa #$IrreflexiveBinaryPredicate #$Collection )
ASSERTION-073
( #$genls #$IrreflexiveBinaryPredicate #$BinaryPredicate )
ASSERTION-074
(#$not (#$and 
   (#$isa ?PRED #$IrreflexiveBinaryPredicate) 
   (?PRED ?OBJ ?OBJ)
                 ) )
ASSERTION-075
(#$implies 
   (#$and 
      (#$isa ?Q #$IrreflexiveBinaryPredicate) 
      (#$different ?P ?Q) 
      (#$genlPreds ?P ?Q)
   ) 
   (#$isa ?P #$IrreflexiveBinaryPredicate)
)

;;; #$ListTheFormat

ASSERTION-076
(#$isa #$ListTheFormat #$Format)

;;; #$Microtheory

ASSERTION-077
(#$isa #$Microtheory #$Collection )
ASSERTION-078
(#$genls #$Microtheory #$IndividualObject)

;;; #$NonNegativeInteger

ASSERTION-079
(#$isa #$NonNegativeInteger #$Collection)
ASSERTION-080
(#$genls #$NonNegativeInteger #$Integer)


;;; #$NonPredicateFunction

ASSERTION-081
(#$isa #$NonPredicateFunction #$Collection )
ASSERTION-082
(#$genls #$NonPredicateFunction #$FunctionTheMathematicalType )

;;; #$PositiveInteger

ASSERTION-083
(#$isa #$PositiveInteger #$Collection )
ASSERTION-084
(#$genls #$PositiveInteger #$NonNegativeInteger )

;;; #$Predicate

ASSERTION-085
(#$isa #$Predicate #$Collection)
ASSERTION-086
(#$genls #$Predicate #$FunctionTheMathematicalType )

;;; #$ProblemSolvingCntxt

ASSERTION-087
(#$isa #$ProblemSolvingCntxt #$Collection )
ASSERTION-088
(#$genls #$ProblemSolvingCntxt #$Microtheory )

;;; #$QuaternaryPredicate

ASSERTION-089
(#$isa #$QuaternaryPredicate #$Collection)
ASSERTION-090
(#$genls #$QuaternaryPredicate #$Predicate )
ASSERTION-091
(#$implies 
   (#$isa ?P #$QuaternaryPredicate ) 
   (#$arity ?P 4 )
)

;;; #$QuintaryPredicate

ASSERTION-092
(#$isa #$QuintaryPredicate #$Collection)
ASSERTION-093
(#$genls #$QuintaryPredicate #$Predicate)
ASSERTION-094
 (#$implies 
    (#$isa ?P #$QuintaryPredicate ) 
    (#$arity ?P 5) )

;;; #$RealNumber

ASSERTION-095
(#$isa #$RealNumber #$Collection )
ASSERTION-096
(#$genls #$RealNumber #$AttributeValue )

;;; #$ReflexiveBinaryPredicate

ASSERTION-097
(#$isa #$ReflexiveBinaryPredicate #$Collection )
ASSERTION-098
(#$genls #$ReflexiveBinaryPredicate #$BinaryPredicate )
ASSERTION-099
(#$implies 
    (#$isa ?PRED #$ReflexiveBinaryPredicate ) 
    (?PRED ?OBJ ?OBJ)
)

;;; #$ReifiableFunction

ASSERTION-100
(#$isa #$ReifiableFunction #$Collection )
ASSERTION-101
(#$genls #$ReifiableFunction #$NonPredicateFunction )

;;; #$ReifiableTerm

ASSERTION-102
(#$isa #$ReifiableTerm #$ReifiableTerm )
ASSERTION-103
(#$isa #$ReifiableTerm #$Collection )
ASSERTION-104
(#$genls #$ReifiableTerm #$CycIndexedTerm )

;;; #$Relationship

ASSERTION-105
(#$isa #$Relationship #$Collection)
ASSERTION-106
(#$genls #$Relationship #$IndividualObject )

;;; #$Set-Mathematical

ASSERTION-107
(#$isa #$Set-Mathematical #$Collection)
ASSERTION-108
(#$genls #$Set-Mathematical #$SetOrCollection)

;;; #$SetOrCollection

ASSERTION-109
(#$isa #$SetOrCollection #$Collection )
ASSERTION-110
(#$genls #$SetOrCollection #$Thing )

;;; #$SetTheFormat

ASSERTION-111
(#$isa #$SetTheFormat #$Format)

;;; #$SiblingDisjointAttributeType

ASSERTION-112
(#$isa #$SiblingDisjointAttributeType #$SiblingDisjointCollection)
ASSERTION-113
(#$genls #$SiblingDisjointAttributeType #$Collection)
ASSERTION-114
(#$implies 
    (#$and 
      (#$isa ?C #$SiblingDisjointAttributeType ) 
      (#$isa ?A1 ?C ) 
      (#$isa ?A2 ?C ) 
      (#$different ?A1 ?A2 ) 
      (#$hasAttributes ?G072 ?A1 ) 
      (#$hasAttributes ?G072 ?A2 )
    ) 
    (#$or 
      (#$genlAttributes ?A1 ?A2) 
      (#$genlAttributes ?A2 ?A1)
    )
)

;;; #$SiblingDisjointCollection

ASSERTION-115
(#$isa #$SiblingDisjointCollection #$Collection)
ASSERTION-116
(#$genls #$SiblingDisjointCollection #$Collection)

;;; #$SingleEntry

ASSERTION-117
(#$isa #$SingleEntry #$Format )

;;; #$SkolemFuncN

ASSERTION-118
(#$isa #$SkolemFuncN #$ReifiableFunction)
ASSERTION-119
(#$arity #$SkolemFuncN 3)
ASSERTION-120
(#$arg1Isa #$SkolemFuncN #$CycSystemList)
ASSERTION-121
(#$arg2Isa #$SkolemFuncN #$CycSystemSymbol )
ASSERTION-122
(#$arg3Isa #$SkolemFuncN #$RealNumber)

;;; #$SkolemFunction

ASSERTION-123
(#$isa #$SkolemFunction #$Collection)
ASSERTION-124
(#$genls #$SkolemFunction #$ReifiableFunction)
ASSERTION-125
(#$arity #$SkolemFunction 2 )
ASSERTION-126
(#$arg2Isa #$SkolemFunction #$CycSystemSymbol)
ASSERTION-127
(#$arg1Isa #$SkolemFunction #$CycSystemList)

;;; #$SubAbs

ASSERTION-128
(#$isa #$SubAbs #$Format)

;;; #$SymmetricBinaryPredicate

ASSERTION-129
(#$isa #$SymmetricBinaryPredicate #$Collection)
ASSERTION-130
(#$genls #$SymmetricBinaryPredicate #$CommutativeRelation )
ASSERTION-131
(#$genls #$SymmetricBinaryPredicate #$BinaryPredicate )
ASSERTION-132
(#$implies 
    (#$and 
        (#$isa ?PRED #$SymmetricBinaryPredicate) 
        (?PRED ?ARG1 ?ARG2)
    ) 
    (?PRED ?ARG2 ?ARG1)
)
ASSERTION-133
(#$implies 
    (#$isa ?PRED #$SymmetricBinaryPredicate ) 
    (#$genlInverse ?PRED ?PRED )
)

;;; #$TemporalObject

ASSERTION-134
(#$isa #$TemporalObject #$Collection)
ASSERTION-135
(#$genls #$TemporalObject #$IndividualObject )

;;; #$TernaryPredicate

ASSERTION-136
(#$isa #$TernaryPredicate #$Collection )
ASSERTION-137
(#$genls #$TernaryPredicate #$Predicate )
ASSERTION-138
(#$not      (#$and 
    (#$isa ?X #$TernaryPredicate ) 
    (#$arg4Isa ?X ?Y )
                   )  )
ASSERTION-139
(#$implies 
    (#$isa ?P #$TernaryPredicate ) 
    (#$arity ?P 3 )
)

;;; #$TheSet

ASSERTION-140
(#$isa #$TheSet #$VariableArityRelation )

ASSERTION-141
(#$isa #$TheSet #$NonPredicateFunction)

ASSERTION-142
(#$resultIsa #$TheSet #$Set-Mathematical)

ASSERTION-143
(#$argsIsa #$TheSet #$Thing )


;;; #$TheTerm

ASSERTION-144
(#$isa #$TheTerm #$Collection )
ASSERTION-145
(#$genls #$TheTerm  #$Thing )

;;; #$Thing

ASSERTION-146
(#$isa #$Thing #$Collection )
ASSERTION-147
(#$isa ?OBJ #$Thing)

;;; #$TransitiveBinaryPredicate

ASSERTION-148
(#$isa #$TransitiveBinaryPredicate #$Collection )
ASSERTION-149
(#$genls #$TransitiveBinaryPredicate #$BinaryPredicate)
ASSERTION-150
(#$implies 
    (#$and 
        (#$isa ?U #$TransitiveBinaryPredicate ) 
        ( ?U ?X ?Z ) 
        ( ?U ?Z ?VAR3 )
    ) 
    ( ?U ?X ?VAR3 )
)

;;; #$True

ASSERTION-151
(#$isa #$True #$IndividualObject )

;;; #$UnaryPredicate

ASSERTION-152
(#$isa #$UnaryPredicate #$Collection )
ASSERTION-153
(#$genls #$UnaryPredicate #$Predicate )
ASSERTION-154
(#$implies 
    (#$isa ?P #$UnaryPredicate ) 
    (#$arity ?P 1 )
)

;;; #$UnaryTypePredicate

ASSERTION-155
(#$isa #$UnaryTypePredicate #$Collection )
ASSERTION-156
(#$genls #$UnaryTypePredicate #$UnaryPredicate )
ASSERTION-157
(#$genls #$UnaryTypePredicate #$InferenceRelatedBookkeepingPredicate )

;;; #$VariableArityRelation

ASSERTION-158
(#$isa #$VariableArityRelation #$Collection )
ASSERTION-159
(#$genls #$VariableArityRelation #$Relationship )

;;; #$abnormal

ASSERTION-160
(#$isa #$abnormal #$DefaultMonotonicPredicate )
ASSERTION-161
(#$isa #$abnormal #$BinaryPredicate )
ASSERTION-162
(#$arity #$abnormal 2 )
ASSERTION-163
(#$arg1Isa #$abnormal #$CycSystemList )
ASSERTION-164
(#$arg2Isa #$abnormal  #$Assertion )

;;; #$afterAdding

ASSERTION-165
(#$isa #$afterAdding #$InferenceRelatedBookkeepingPredicate )
ASSERTION-166
(#$isa #$afterAdding #$BinaryPredicate )
ASSERTION-167
(#$arity #$afterAdding 2 )
ASSERTION-168
(#$arg1Isa #$afterAdding #$Predicate )
ASSERTION-169
(#$arg2Isa #$afterAdding #$CycSystemSymbol )

;;; #$afterRemoving

ASSERTION-170
(#$isa #$afterRemoving #$InferenceRelatedBookkeepingPredicate )
ASSERTION-171
(#$isa #$afterRemoving #$BinaryPredicate )
ASSERTION-172
(#$arity #$afterRemoving 2 )
ASSERTION-173
(#$arg1Isa #$afterRemoving #$Predicate )
ASSERTION-174
(#$arg2Isa #$afterRemoving #$CycSystemSymbol)

;;; #$and

ASSERTION-175
(#$isa #$and #$CommutativeRelation )
ASSERTION-176
(#$isa #$and #$VariableArityRelation )
ASSERTION-178
(#$argsIsa #$and #$CycFormula )
ASSERTION-179
(#$resultIsa #$and #$CycFormula )

;;; #$arg1Format

ASSERTION-180
(#$isa #$arg1Format #$BinaryPredicate)
ASSERTION-181
(#$arity #$arg1Format 2 )
ASSERTION-182
(#$arg1Isa #$arg1Format #$Predicate )
ASSERTION-183
(#$arg2Isa #$arg1Format #$Format )

;;; #$arg1Genl

ASSERTION-184
(#$isa #$arg1Genl #$BinaryPredicate )
ASSERTION-185
(#$arity #$arg1Genl 2 )
ASSERTION-186
(#$arg1Isa #$arg1Genl #$Relationship )
ASSERTION-187
(#$arg2Isa #$arg1Genl #$Collection )

;;; #$arg1Isa

ASSERTION-188
(#$isa #$arg1Isa #$DefaultMonotonicPredicate )
ASSERTION-189
(#$isa #$arg1Isa #$BinaryPredicate )
ASSERTION-190
(#$arity #$arg1Isa 2)
ASSERTION-191
(#$arg1Isa #$arg1Isa #$Relationship )
ASSERTION-192
(#$arg2Isa #$arg1Isa #$Collection )


;;; #$arg2Format

ASSERTION-193
(#$isa #$arg2Format #$BinaryPredicate )
ASSERTION-194
(#$arity #$arg2Format 2 )
ASSERTION-195
(#$arg1Isa #$arg2Format #$Predicate )
ASSERTION-196
(#$arg2Isa #$arg2Format #$Format )

;;; #$arg2Genl

ASSERTION-197
(#$isa #$arg2Genl #$BinaryPredicate )
ASSERTION-198
(#$arity #$arg2Genl 2 )
ASSERTION-199
(#$arg1Isa #$arg2Genl #$Relationship )
200
(#$arg2Isa #$arg2Genl #$Collection )

;;; #$arg2Isa

201
(#$isa #$arg2Isa #$DefaultMonotonicPredicate )
202
(#$isa #$arg2Isa #$BinaryPredicate )
203
(#$arity #$arg2Isa 2 )
204
(#$arg1Isa #$arg2Isa #$Relationship )
205
(#$arg2Isa #$arg2Isa #$Collection )

;;; #$arg3Format

206
(#$isa #$arg3Format #$BinaryPredicate)
207
(#$arity #$arg3Format 2 )
208
(#$arg1Isa #$arg3Format #$Predicate )
209
(#$arg2Isa #$arg3Format #$Format )

;;; #$arg3Genl

210
(#$isa #$arg3Genl #$BinaryPredicate)
211
(#$arity #$arg3Genl 2)
212
(#$arg1Isa #$arg3Genl #$Relationship)
213
(#$arg2Isa #$arg3Genl #$Collection)

;;; #$arg3Isa

214
(#$isa #$arg3Isa #$DefaultMonotonicPredicate )
215
(#$isa #$arg3Isa #$BinaryPredicate )
216
(#$arity #$arg3Isa 2 )
217
(#$arg1Isa #$arg3Isa #$Relationship )
218
(#$arg2Isa #$arg3Isa #$Collection )

;;; #$arg4Format

219
(#$isa #$arg4Format #$BinaryPredicate)
220
(#$arity #$arg4Format 2 )
221
(#$arg1Isa #$arg4Format #$Predicate)
222
(#$arg2Isa #$arg4Format #$Format)

;;; #$arg4Genl

223
(#$isa #$arg4Genl #$BinaryPredicate )

224
(#$arity #$arg4Genl 2)
225
(#$arg1Isa #$arg4Genl #$Relationship)
226
(#$arg2Isa #$arg4Genl #$Collection)

;;; #$arg4Isa

227
(#$isa #$arg4Isa #$DefaultMonotonicPredicate)
228
(#$isa #$arg4Isa #$BinaryPredicate)
229
(#$arity #$arg4Isa 2)
230
(#$arg1Isa #$arg4Isa #$Relationship)
231
(#$arg2Isa #$arg4Isa #$Collection)

;;; #$arg5Format

232
(#$isa #$arg5Format #$BinaryPredicate)
233
(#$arity #$arg5Format 2 )
234
(#$arg1Isa #$arg5Format #$Predicate)
235
(#$arg2Isa #$arg5Format #$Format)

;;; #$arg5Genl

236
(#$isa #$arg5Genl #$BinaryPredicate )
237
(#$arity #$arg5Genl 2 )
238
(#$arg1Isa #$arg5Genl #$Relationship )
239
(#$arg2Isa #$arg5Genl #$Collection )

;;; #$arg5Isa

240
(#$isa #$arg5Isa #$DefaultMonotonicPredicate)
241
(#$isa #$arg5Isa #$BinaryPredicate)
242
(#$arity #$arg5Isa 2)
243
(#$arg1Isa #$arg5Isa #$Relationship)
244
(#$arg2Isa #$arg5Isa #$Collection)

;;; #$argsGenl

245
(#$isa #$argsGenl #$BinaryPredicate)
246
(#$arity #$argsGenl 2 )
247
(#$arg1Isa #$argsGenl #$Relationship)
248
(#$arg2Isa #$argsGenl #$Collection)

;;; #$argsIsa

249
(#$isa #$argsIsa #$BinaryPredicate )
250
(#$arity #$argsIsa 2 )
251
(#$arg1Isa #$argsIsa #$Relationship )
252
(#$arg2Isa #$argsIsa #$Collection )

;;; #$arity

253
(#$isa #$arity #$DefaultMonotonicPredicate )
254
(#$isa #$arity #$BinaryPredicate )
255
(#$arity #$arity 2 )
256
(#$arg1Isa #$arity #$Relationship)
257
(#$arg2Isa #$arity #$Integer )

;;; #$coExtensional

258
(#$isa #$coExtensional #$SymmetricBinaryPredicate )
259
(#$isa #$coExtensional #$ReflexiveBinaryPredicate )
260
(#$isa #$coExtensional #$TransitiveBinaryPredicate)
261
(#$genlInverse #$coExtensional #$coExtensional )
262
(#$arity #$coExtensional 2 )
263
(#$arg1Isa #$coExtensional #$Collection )
264
(#$arg2Isa #$coExtensional #$Collection)

;;; #$comment

265
(#$isa #$comment #$BinaryPredicate )
266
(#$arity #$comment 2 )
267
(#$arg1Isa #$comment #$CycIndexedTerm )
268
(#$arg2Isa #$comment #$CycSystemString )

;;; #$cyclistNotes

269
(#$isa #$cyclistNotes #$BinaryPredicate )
270
(#$arity #$cyclistNotes 2 )
271
(#$arg1Isa #$cyclistNotes #$CycIndexedTerm )
272
(#$arg2Isa #$cyclistNotes #$CycSystemString )

;;; #$defnIff

273
(#$isa #$defnIff #$InferenceRelatedBookkeepingPredicate )
274
(#$isa #$defnIff #$BinaryPredicate )
275
(#$arity #$defnIff 2 )
276
(#$arg1Isa #$defnIff #$Collection )
277
(#$arg2Isa #$defnIff #$CycSystemSymbol )
278
(#$implies 
    (#$defnIff ?X ?Y ) 
    (#$defnSufficient ?X ?Y )
)

;;; #$defnNecessary

279
(#$isa #$defnNecessary #$BinaryPredicate)
280
(#$arity #$defnNecessary 2 )
281
(#$arg1Isa #$defnNecessary #$Collection)
282
(#$arg2Isa #$defnNecessary #$CycSystemSymbol)

;;; #$defnSufficient

283
(#$isa #$defnSufficient #$InferenceRelatedBookkeepingPredicate )
284
(#$isa #$defnSufficient #$BinaryPredicate )
285
(#$arity #$defnSufficient 2 )
286
(#$arg1Isa #$defnSufficient #$Collection )
287
(#$arg2Isa #$defnSufficient #$CycSystemSymbol)

;;; #$different

288
(#$isa #$different #$VariableArityRelation )
289
(#$isa #$different #$EvaluatableFunction )
290
(#$isa #$different #$Predicate )
291
(#$argsIsa #$different #$Thing )
292
(#$not 
    (#$different ?OBJ ?OBJ)
)

;;; #$disjointWith

293
(#$isa #$disjointWith #$DefaultMonotonicPredicate )
294
(#$isa #$disjointWith #$SymmetricBinaryPredicate )
295
(#$isa #$disjointWith #$IrreflexiveBinaryPredicate )
296
(#$genlInverse #$disjointWith #$disjointWith )
297
(#$arity #$disjointWith 2 )
298
(#$arg1Isa #$disjointWith #$SetOrCollection )
299
(#$arg2Isa #$disjointWith #$SetOrCollection )
ASSERTION-300
(#$not      (#$and 
       (#$isa ?OBJ ?COL1) 
       (#$isa ?OBJ ?COL2) 
       (#$disjointWith ?COL1 ?COL2)
    )   )
ASSERTION-301
(#$implies 
    (#$and 
        (#$disjointWith ?COL ?SUPERSET ) 
        (#$genls ?SUBSET ?SUPERSET )
    ) 
    (#$disjointWith ?COL ?SUBSET )
)
ASSERTION-302
(#$not  (#$and 
    (#$disjointWith ?X ?Y) 
    (#$genls ?X ?Y)
            )   )

;;; #$elementOf

ASSERTION-303
(#$isa #$elementOf #$BinaryPredicate)
ASSERTION-304
(#$arity #$elementOf 2)
ASSERTION-305
(#$arg1Isa #$elementOf #$Thing)
ASSERTION-306
(#$arg2Isa #$elementOf #$SetOrCollection)

;;; #$equals

ASSERTION-307
(#$isa #$equals #$DefaultMonotonicPredicate )
ASSERTION-308
(#$isa #$equals #$SymmetricBinaryPredicate )
ASSERTION-309
(#$isa #$equals #$ReflexiveBinaryPredicate )
ASSERTION-310
(#$isa #$equals #$TransitiveBinaryPredicate )
ASSERTION-311
(#$genlInverse #$equals #$equals )
ASSERTION-312
(#$arity #$equals 2 )
ASSERTION-313
(#$arg1Isa #$equals #$Thing )
ASSERTION-314
(#$arg2Isa #$equals #$Thing )

;;; #$exceptFor

ASSERTION-315
(#$isa #$exceptFor #$Relatio1nship)
ASSERTION-316
(#$arity #$exceptFor 2)
ASSERTION-317
(#$arg2Isa #$exceptFor  #$Assertion)
ASSERTION-318
(#$arg1Isa #$exceptFor #$ReifiableTerm )

;;; #$exceptWhen

ASSERTION-319
(#$isa #$exceptWhen #$Relationship)
ASSERTION-320
(#$arity #$exceptWhen 2 )
ASSERTION-321
(#$arg2Isa #$exceptWhen  #$Assertion)
ASSERTION-322
(#$arg1Isa #$exceptWhen #$CycFormula)

;;; #$forAll

ASSERTION-323
(#$isa #$forAll #$Relationship )
ASSERTION-324
(#$arity #$forAll 2 )
ASSERTION-325
(#$arg2Isa #$forAll #$CycFormula )
ASSERTION-326
(#$arg1Isa #$forAll #$CycELVariable )

;;; #$genlAttributes

ASSERTION-327
(#$isa #$genlAttributes #$ReflexiveBinaryPredicate)
ASSERTION-328
(#$isa #$genlAttributes #$TransitiveBinaryPredicate)
ASSERTION-329
(#$arity #$genlAttributes 2 )
ASSERTION-330
(#$arg1Isa #$genlAttributes #$AttributeValue )
ASSERTION-331
(#$arg2Isa #$genlAttributes #$AttributeValue)

;;; #$genlInverse

ASSERTION-332
(#$isa #$genlInverse #$BinaryPredicate)
ASSERTION-333
(#$arity #$genlInverse 2 )
ASSERTION-334
(#$arg1Isa #$genlInverse #$BinaryPredicate )
ASSERTION-335
(#$arg2Isa #$genlInverse #$BinaryPredicate )
ASSERTION-336
(#$implies 
    (#$and 
        (#$genlInverse ?PRED ?GEN-PRED) 
        (?PRED ?ARG1 ?ARG2)
    ) 
    (?GEN-PRED ?ARG2 ?ARG1)
)
ASSERTION-337
(#$implies 
    (#$and 
        (#$genlInverse ?SPEC-PRED ?PRED) 
        (#$genlInverse ?PRED ?GENL-PRED)
    ) 
    (#$genlPreds ?SPEC-PRED ?GENL-PRED)
)
ASSERTION-338
(#$implies 
    (#$and 
        (#$genlInverse ?SPEC-PRED ?PRED) 
        (#$genlPreds ?PRED ?GENL-PRED)
    ) 
    (#$genlInverse ?SPEC-PRED ?GENL-PRED)
)
ASSERTION-339
(#$implies 
    (#$and 
        (#$negationPreds ?GENL-PRED ?NEG-PRED ) 
        (#$genlInverse ?SPEC-PRED ?GENL-PRED )
    ) 
    (#$negationInverse ?NEG-PRED ?SPEC-PRED )
)
ASSERTION-340
(#$implies 
    (#$and 
        (#$negationInverse ?GENL-PRED ?NEG-PRED ) 
        (#$genlInverse ?SPEC-PRED ?GENL-PRED )
    ) 
    (#$negationPreds ?NEG-PRED ?SPEC-PRED )
)
ASSERTION-341
(#$implies 
    (#$and 
        (#$genlPreds ?SPEC-PRED ?PRED ) 
        (#$genlInverse ?PRED ?GENL-PRED )
    ) 
    (#$genlInverse ?SPEC-PRED ?GENL-PRED )
)

;;; #$genlMt

ASSERTION-342
(#$isa #$genlMt #$DefaultMonotonicPredicate)
ASSERTION-343
(#$isa #$genlMt  #$AntiSymmetricBinaryPredicate )
ASSERTION-344
(#$isa #$genlMt #$ReflexiveBinaryPredicate )
ASSERTION-345
(#$isa #$genlMt #$TransitiveBinaryPredicate)
ASSERTION-346
(#$arity #$genlMt 2)
ASSERTION-347
(#$arg1Isa #$genlMt #$Microtheory )
ASSERTION-348
(#$arg2Isa #$genlMt #$Microtheory )

;;; #$genlPreds

ASSERTION-349
(#$isa #$genlPreds  #$AntiSymmetricBinaryPredicate )
ASSERTION-350
(#$isa #$genlPreds #$ReflexiveBinaryPredicate )
ASSERTION-351
(#$isa #$genlPreds #$TransitiveBinaryPredicate )
ASSERTION-352
(#$arity #$genlPreds 2 )
ASSERTION-353
(#$arg1Isa #$genlPreds #$Predicate )
ASSERTION-354
(#$arg2Isa #$genlPreds #$Predicate )
ASSERTION-355
(#$implies 
    (#$and 
        (?PRED ?ARG1) 
        (#$genlPreds ?PRED ?GENL-PRED )
    ) 
    (?GENL-PRED ?ARG1)
)
ASSERTION-356
(#$implies 
    (#$and 
        (#$negationPreds ?GENL-PRED ?NEG-PRED ) 
        (#$genlPreds ?SPEC-PRED ?GENL-PRED )
    ) 
    (#$negationPreds ?NEG-PRED ?SPEC-PRED )
)
ASSERTION-357
 (#$implies 
     (#$and 
         (#$negationInverse ?GENL-PRED ?NEG-PRED ) 
         (#$genlPreds ?SPEC-PRED ?GENL-PRED )
     ) 
     (#$negationInverse ?NEG-PRED ?SPEC-PRED )
 )
ASSERTION-358
(#$implies 
    (#$and 
        (#$genlPreds ?PRED ?GENL-PRED ) 
        (?PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4 ?ARG5 )
    ) 
    (?GENL-PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4 ?ARG5 )
)
ASSERTION-359
(#$implies 
    (#$and 
        (#$genlPreds ?PRED ?GENL-PRED) 
        (?PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4)
    ) 
    (?GENL-PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4)
)
ASSERTION-360
(#$implies 
    (#$and 
        (#$genlPreds ?PRED ?GENL-PRED) 
        (?PRED ?ARG1 ?ARG2 ?ARG3)
    ) 
    (?GENL-PRED ?ARG1 ?ARG2 ?ARG3)
)
ASSERTION-361
(#$implies 
    (#$and 
        (#$genlPreds ?PRED ?GENL-PRED) 
        (?PRED ?ARG1 ?ARG2)
    ) 
    (?GENL-PRED ?ARG1 ?ARG2 )
)

;;; #$genls

ASSERTION-362
(#$isa #$genls #$DefaultMonotonicPredicate )
ASSERTION-363
(#$isa #$genls #$ReflexiveBinaryPredicate )
ASSERTION-364
(#$isa #$genls #$TransitiveBinaryPredicate )
ASSERTION-365
(#$arity #$genls 2 )
ASSERTION-366
(#$arg1Isa #$genls #$Collection )
ASSERTION-367
(#$arg2Isa #$genls #$Collection )
ASSERTION-368
(#$implies 
    (#$and 
        (#$isa ?OBJ ?SUBSET ) 
        (#$genls ?SUBSET ?SUPERSET )
    ) 
    (#$isa ?OBJ ?SUPERSET )
)
ASSERTION-369
(#$implies 
    (#$resultgenl ?FUNC ?COLL ) 
    (#$genls 
        (?FUNC ?ARG1 ?ARG2 ?ARG3 ?ARG4 ?ARG5 )
        ?COLL
    )
)
ASSERTION-370
(#$implies 
    (#$resultgenl ?FUNC ?COLL ) 
    (#$genls 
        ( ?FUNC ?ARG1 ?ARG2 ?ARG3 ?ARG4 ) 
        ?COLL
    )
)
ASSERTION-371
(#$implies 
    (#$resultgenl ?FUNC ?COLL) 
    (#$genls 
        (?FUNC ?ARG1 ?ARG2 ?ARG3) 
        ?COLL
    )
)
ASSERTION-372
(#$implies 
    (#$resultgenl ?FUNC ?COLL) 
    (#$genls 
        (?FUNC ?ARG1 ?ARG2) 
        ?COLL
    )
)
ASSERTION-373
(#$implies 
   (#$resultgenl ?FUNC ?COLL) 
   (#$genls 
      (?FUNC ?ARG1) ?COLL)
)

;;; #$hasAttributes

ASSERTION-374
(#$isa #$hasAttributes #$BinaryPredicate )
ASSERTION-375
(#$arity #$hasAttributes 2)
ASSERTION-376
(#$arg1Isa #$hasAttributes #$TemporalObject )
ASSERTION-377
(#$arg2Isa #$hasAttributes #$AttributeValue )
ASSERTION-378
(#$not  (#$and 
    (#$hasAttributes ?Z ?X ) 
    (#$hasAttributes ?Z ?Y ) 
    (#$negationAttribute ?X ?Y )
              ) )

;;; #$holdsIn

ASSERTION-379
(#$isa #$holdsIn #$BinaryPredicate)
ASSERTION-380
(#$arity #$holdsIn 2)
ASSERTION-381
(#$arg1Isa #$holdsIn #$TemporalObject )
ASSERTION-382
(#$arg2Isa #$holdsIn #$CycFormula )

;;; #$implies

ASSERTION-383
(#$isa #$implies #$Relationship )
ASSERTION-384 
(#$arity #$implies 2)
ASSERTION-385 
(#$arg2Isa #$implies #$CycFormula )
ASSERTION-386
(#$arg1Isa #$implies #$CycFormula )
ASSERTION-387
(#$resultIsa #$implies #$CycFormula )

;;; #$interArgIsa1-2

ASSERTION-388
(#$isa #$interArgIsa1-2 #$TernaryPredicate)
ASSERTION-389
(#$arity #$interArgIsa1-2 3)
ASSERTION-390
(#$arg1Isa #$interArgIsa1-2 #$Predicate)
ASSERTION-391
(#$arg2Isa #$interArgIsa1-2 #$Collection)
ASSERTION-392
(#$arg3Isa #$interArgIsa1-2 #$Collection)
ASSERTION-393
(#$implies 
    (#$and 
        (#$requiredArg1Pred ?COL-1 ?PRED ) 
        (#$interArgIsa1-2 ?PRED ?COL-1 ?COL-2 )
    ) 
    (#$relationAllExists ?PRED ?COL-1 ?COL-2 )
)
ASSERTION-394
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL) 
        (?PRED ?INDEP-INS ?DEP-INS) 
        (#$interArgIsa1-2 ?PRED ?INDEP-COL ?DEP-COL)
    ) 
    (#$isa ?DEP-INS ?DEP-COL)
)

;;; #$interArgIsa1-3

ASSERTION-395
(#$isa #$interArgIsa1-3 #$TernaryPredicate)
ASSERTION-396
(#$arity #$interArgIsa1-3 3)
ASSERTION-397
(#$arg1Isa #$interArgIsa1-3 #$Predicate )
ASSERTION-398
(#$arg2Isa #$interArgIsa1-3 #$Collection )
ASSERTION-399
(#$arg3Isa #$interArgIsa1-3 #$Collection )
ASSERTION-400
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa1-3 ?PRED ?INDEP-COL ?DEP-COL ) 
        (?PRED ?INDEP-INS ?ANY-ARG-2 ?DEP-INS)
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)


;;; #$interArgIsa1-4

ASSERTION-401
(#$isa #$interArgIsa1-4 #$TernaryPredicate)
ASSERTION-402
(#$arity #$interArgIsa1-4 3 )
ASSERTION-403
(#$arg1Isa #$interArgIsa1-4 #$Predicate )
ASSERTION-404
(#$arg2Isa #$interArgIsa1-4 #$Collection )
ASSERTION-405
(#$arg3Isa #$interArgIsa1-4 #$Collection)

ASSERTION-406
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL) 
        (#$interArgIsa1-4 ?PRED ?INDEP-COL ?DEP-COL) 
        (?PRED ?INDEP-INS ?ANY-ARG-2 ?ANY-ARG-3 ?DEP-INS)
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$interArgIsa1-5

ASSERTION-407
(#$isa #$interArgIsa1-5 #$TernaryPredicate )
ASSERTION-408
 (#$arity #$interArgIsa1-5 3 )
ASSERTION-409
 (#$arg1Isa #$interArgIsa1-5 #$Predicate )
ASSERTION-410
 (#$arg2Isa #$interArgIsa1-5 #$Collection )
ASSERTION-411
 (#$arg3Isa #$interArgIsa1-5 #$Collection )
ASSERTION-412
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa1-5 ?PRED ?INDEP-COL ?DEP-COL ) 
        ( ?PRED ?INDEP-INS ?ANY-ARG-2 ?ANY-ARG-3 ?ANY-ARG-4 ?DEP-INS )
    ) 
    (#$isa ?DEP-INS ?DEP-COL)
)

;;; #$interArgIsa2-1

ASSERTION-413
(#$isa #$interArgIsa2-1 #$TernaryPredicate )
ASSERTION-414
(#$arity #$interArgIsa2-1 3 )
ASSERTION-415
(#$arg1Isa #$interArgIsa2-1 #$Predicate )
ASSERTION-416
 (#$arg2Isa [[#$interArgIsa2-1 #$Collection)

ASSERTION-417
(#$arg3Isa [[#$interArgIsa2-1 #$Collection)

ASSERTION-418
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (?PRED ?DEP-INS ?INDEP-INS ) 
        (#$interArgIsa2-1 ?PRED ?INDEP-COL ?DEP-COL )
    ) 
    (#$isa ?DEP-INS ?DEP-COL)
)

;;; #$interArgIsa2-3

ASSERTION-419
 (#$isa #$interArgIsa2-3 #$TernaryPredicate )
ASSERTION-420
(#$arity #$interArgIsa2-3 3 )
 ASSERTION-421
(#$arg1Isa #$interArgIsa2-3 #$Predicate )
 ASSERTION-422
(#$arg2Isa #$interArgIsa2-3 #$Collection )
 ASSERTION-423
(#$arg3Isa #$interArgIsa2-3 #$Collection )

 ASSERTION-424
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa2-3 ?PRED ?INDEP-COL ?DEP-COL ) 
        (?PRED ?ANY-ARG-1 ?INDEP-INS ?DEP-INS )
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$interArgIsa2-4

 ASSERTION-425
(#$isa #$interArgIsa2-4 #$TernaryPredicate )
 ASSERTION-426
(#$arity #$interArgIsa2-4 3 )
 ASSERTION-427
(#$arg1Isa #$interArgIsa2-4 #$Predicate )
 ASSERTION-428
(#$arg2Isa #$interArgIsa2-4 #$Collection )
 ASSERTION-429
(#$arg3Isa #$interArgIsa2-4 #$Collection )

ASSERTION-430
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa2-4 ?PRED ?INDEP-COL ?DEP-COL ) 
        (?PRED ?ANY-ARG-1 ?INDEP-INS ?ANY-ARG-3 ?DEP-INS )
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$interArgIsa2-5

 ASSERTION-431
(#$isa #$interArgIsa2-5 #$TernaryPredicate )
 ASSERTION-432
(#$arity #$interArgIsa2-5 3 )
 ASSERTION-433
(#$arg1Isa #$interArgIsa2-5 #$Predicate )
 ASSERTION-434
(#$arg2Isa #$interArgIsa2-5 #$Collection )
 ASSERTION-435
(#$arg3Isa #$interArgIsa2-5 #$Collection )

 ASSERTION-436
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa2-5 ?PRED ?INDEP-COL ?DEP-COL) 
        (?PRED ?ANY-ARG-1 ?INDEP-INS ?ANY-ARG-3 ?ANY-ARG-4 ?DEP-INS ) 
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$interArgIsa3-1

 ASSERTION-437
(#$isa #$interArgIsa3-1 #$TernaryPredicate )
 ASSERTION-438
(#$arity #$interArgIsa3-1 3 )
 ASSERTION-439
(#$arg1Isa #$interArgIsa3-1 #$Predicate )
 ASSERTION-440
(#$arg2Isa #$interArgIsa3-1 #$Collection )
 ASSERTION-441
(#$arg3Isa #$interArgIsa3-1 #$Collection )

 ASSERTION-442
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa3-1 ?PRED ?INDEP-COL ?DEP-COL ) 
        (?PRED ?DEP-INS ?ANY-ARG-2 ?INDEP-INS )
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$interArgIsa3-2

 ASSERTION-443
 (#$isa #$interArgIsa3-2 #$TernaryPredicate )
 ASSERTION-444
(#$arity #$interArgIsa3-2 3 )
 ASSERTION-445
(#$arg1Isa #$interArgIsa3-2 #$Predicate )
 ASSERTION-446
(#$arg2Isa #$interArgIsa3-2 #$Collection)
 ASSERTION-447
(#$arg3Isa #$interArgIsa3-2 #$Collection )
 ASSERTION-448
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa3-2 ?PRED ?INDEP-COL ?DEP-COL ) 
        (?PRED ?ANY-ARG-1 ?DEP-INS ?INDEP-INS )
    ) 
    (#$isa ?DEP-INS ?DEP-COL)
)

;;; #$interArgIsa3-4

 ASSERTION-449
(#$isa #$interArgIsa3-4 #$TernaryPredicate )
 ASSERTION-450
(#$arity #$interArgIsa3-4 3 )
 ASSERTION-451
(#$arg1Isa #$interArgIsa3-4 #$Predicate )
 ASSERTION-452
(#$arg2Isa #$interArgIsa3-4 #$Collection)
 ASSERTION-453
(#$arg3Isa #$interArgIsa3-4 #$Collection )
 ASSERTION-454
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa3-4 ?PRED ?INDEP-COL ?DEP-COL ) 
        (?PRED ?ANY-ARG-1 ?ANY-ARG-2 ?INDEP-INS ?DEP-INS )
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$interArgIsa3-5

 ASSERTION-455
(#$isa #$interArgIsa3-5 #$TernaryPredicate )
 ASSERTION-456
(#$arity #$interArgIsa3-5 3 )
 ASSERTION-457
(#$arg1Isa #$interArgIsa3-5 #$Predicate )
 ASSERTION-458
(#$arg2Isa #$interArgIsa3-5 #$Collection )
 ASSERTION-459
(#$arg3Isa #$interArgIsa3-5 #$Collection)

 ASSERTION-460
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa3-5 ?PRED ?INDEP-COL ?DEP-COL ) 
        (?PRED ?ANY-ARG-1 ?ANY-ARG-2 ?INDEP-INS ?ANY-ARG-4 ?DEP-INS )
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$interArgIsa4-1

ASSERTION-461
(#$isa #$interArgIsa4-1 #$TernaryPredicate )
ASSERTION-462
(#$arity #$interArgIsa4-1 3 )
ASSERTION-463
(#$arg1Isa #$interArgIsa4-1 #$Predicate )
ASSERTION-464
(#$arg2Isa #$interArgIsa4-1 #$Collection )
ASSERTION-465
(#$arg3Isa #$interArgIsa4-1 #$Collection )

ASSERTION-466
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa4-1 ?PRED ?INDEP-COL ?DEP-COL ) 
        (?PRED ?DEP-INS ?ANY-ARG-2 ?ANY-ARG-3 ?INDEP-INS )
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$interArgIsa4-2

ASSERTION-467
(#$isa #$interArgIsa4-2 #$TernaryPredicate )
ASSERTION-468
(#$arity #$interArgIsa4-2 3 )
ASSERTION-469
(#$arg1Isa #$interArgIsa4-2 #$Predicate )
ASSERTION-470
(#$arg2Isa #$interArgIsa4-2 #$Collection )
ASSERTION-471
(#$arg3Isa #$interArgIsa4-2 #$Collection )

ASSERTION-472
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa4-2 ?PRED ?INDEP-COL ?DEP-COL ) 
        (?PRED ?ANY-ARG-1 ?DEP-INS ?ANY-ARG-3 ?INDEP-INS )
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$interArgIsa4-3

ASSERTION-473
(#$isa #$interArgIsa4-3 #$TernaryPredicate )
ASSERTION-474
(#$arity #$interArgIsa4-3 3 )
ASSERTION-475
(#$arg1Isa #$interArgIsa4-3 #$Predicate )
ASSERTION-476
(#$arg2Isa #$interArgIsa4-3 #$Collection )
ASSERTION-477
(#$arg3Isa #$interArgIsa4-3 #$Collection )

ASSERTION-478
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa4-3 ?PRED ?INDEP-COL ?DEP-COL ) 
        (?PRED ?ANY-ARG-1 ?ANY-ARG-2 ?DEP-INS ?INDEP-INS ) 
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$interArgIsa4-5

ASSERTION-479
(#$isa #$interArgIsa4-5 #$TernaryPredicate )
ASSERTION-480
(#$arity #$interArgIsa4-5 3 )
ASSERTION-481
(#$arg1Isa #$interArgIsa4-5 #$Predicate )
ASSERTION-482
(#$arg2Isa #$interArgIsa4-5 #$Collection )
ASSERTION-483
(#$arg3Isa #$interArgIsa4-5 #$Collection )

ASSERTION-484
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa4-5 ?PRED ?INDEP-COL ?DEP-COL ) 
        (?PRED ?ANY-ARG-1 ?ANY-ARG-2 ?ANY-ARG-3 ?INDEP-INS ?DEP-INS  )
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$interArgIsa5-1

ASSERTION-485
(#$isa #$interArgIsa5-1 #$TernaryPredicate )
ASSERTION-486
(#$arity #$interArgIsa5-1 3 )
ASSERTION-487
(#$arg1Isa #$interArgIsa5-1 #$QuintaryPredicate )
ASSERTION-488
(#$arg2Isa #$interArgIsa5-1 #$Collection )
ASSERTION-489
(#$arg3Isa #$interArgIsa5-1 #$Collection )

ASSERTION-490
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL) 
        (#$interArgIsa5-1 ?PRED ?INDEP-COL ?DEP-COL) 
        (?PRED ?DEP-INS ?ANY-ARG-2 ?ANY-ARG-3 ?ANY-ARG-4 ?INDEP-INS )
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$interArgIsa5-2

ASSERTION-491
(#$isa #$interArgIsa5-2 #$TernaryPredicate )
ASSERTION-492
(#$arity #$interArgIsa5-2 3 )
ASSERTION-493
(#$arg1Isa #$interArgIsa5-2 #$QuintaryPredicate )
ASSERTION-494
(#$arg2Isa #$interArgIsa5-2 #$Collection)
ASSERTION-495
(#$arg3Isa #$interArgIsa5-2 #$Collection)
ASSERTION-496
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa5-2 ?PRED ?INDEP-COL ?DEP-COL ) 
        (?PRED ?ANY-ARG-1 ?DEP-INS ?ANY-ARG-3 ?ANY-ARG-4 ?INDEP-INS )
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$interArgIsa5-3

ASSERTION-497
(#$isa #$interArgIsa5-3 #$TernaryPredicate )
ASSERTION-498
(#$arity #$interArgIsa5-3 3 )
ASSERTION-499
(#$arg1Isa #$interArgIsa5-3 #$QuintaryPredicate )
ASSERTION-500
(#$arg2Isa #$interArgIsa5-3 #$Collection )
ASSERTION-501
(#$arg3Isa #$interArgIsa5-3 #$Collection )

ASSERTION-502
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa5-3 ?PRED ?INDEP-COL ?DEP-COL ) 
        (?PRED ?ANY-ARG-1 ?ANY-ARG-2 ?DEP-INS ?ANY-ARG-4 ?INDEP-INS )
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$interArgIsa5-4

ASSERTION-503
(#$isa #$interArgIsa5-4 #$TernaryPredicate )
ASSERTION-504
(#$arity #$interArgIsa5-4 3)
ASSERTION-505
(#$arg1Isa #$interArgIsa5-4 #$QuintaryPredicate )
ASSERTION-506
(#$arg2Isa #$interArgIsa5-4 #$Collection )
ASSERTION-507
(#$arg3Isa #$interArgIsa5-4 #$Collection)

ASSERTION-508
(#$implies 
    (#$and 
        (#$isa ?INDEP-INS ?INDEP-COL ) 
        (#$interArgIsa5-4 ?PRED ?INDEP-COL ?DEP-COL ) 
        (?PRED ?ANY-ARG-1 ?ANY-ARG-2 ?ANY-ARG-3 ?DEP-INS ?INDEP-INS )
    ) 
    (#$isa ?DEP-INS ?DEP-COL )
)

;;; #$relationExistsAll

ASSERTION-509
(#$isa #$relationExistsAll #$TernaryPredicate )
ASSERTION-510
(#$arity #$relationExistsAll 3 )
ASSERTION-511
(#$arg1Isa #$relationExistsAll #$BinaryPredicate )
ASSERTION-512
(#$arg2Isa #$relationExistsAll #$Collection )
ASSERTION-513
(#$arg3Isa #$relationExistsAll #$Collection )

;;; #$relationExistsCountAll

ASSERTION-514
(#$isa #$relationExistsCountAll #$QuaternaryPredicate )
ASSERTION-515
(#$arity #$relationExistsCountAll 4 )
ASSERTION-516
(#$arg1Isa #$relationExistsCountAll #$BinaryPredicate )
ASSERTION-517
(#$arg2Isa #$relationExistsCountAll #$Collection)
ASSERTION-518
(#$arg3Isa #$relationExistsCountAll #$Collection)
ASSERTION-519
(#$arg4Isa #$relationExistsCountAll #$NonNegativeInteger )

;;; #$isa

ASSERTION-520
(#$isa #$isa #$DefaultMonotonicPredicate )
ASSERTION-521
(#$isa #$isa #$BinaryPredicate )
ASSERTION-522
(#$arity #$isa 2 )
ASSERTION-523
(#$arg1Isa #$isa #$ReifiableTerm )
ASSERTION-524
(#$arg2Isa #$isa #$Collection )
ASSERTION-525
(#$implies 
    ( #$resultIsa ?F ?COL ) 
    ( #$isa 
        (?F ?ARG1 ?ARG2 ?ARG3 ) 
        ?COL
    )
)

ASSERTION-526
(#$implies 
    (#$resultIsa ?F ?COL ) 
    (#$isa 
        (?F ?ARG1 ?ARG2 ) 
           ?COL
    )
)

ASSERTION-527
(#$implies 
    (#$resultIsa ?F ?COL) 
    (#$isa 
        (?F ?ARG1 ) 
        ?COL 
    )
)

;;; #$ist

ASSERTION-528
(#$isa #$ist #$BinaryPredicate )
ASSERTION-529
(#$arity #$ist 2 )
ASSERTION-530
(#$arg1Isa #$ist #$Microtheory )
ASSERTION-531
(#$arg2Isa #$ist #$CycFormula )

;;; #$lispDefun

ASSERTION-532
(#$isa #$lispDefun #$BinaryPredicate )
ASSERTION-533
(#$arity #$lispDefun 2 )
ASSERTION-534
(#$arg1Isa #$lispDefun #$EvaluatableFunction )
ASSERTION-535
(#$arg2Isa #$lispDefun #$CycSystemSymbol )

;;; #$minimizeExtent

ASSERTION-536
(#$isa #$minimizeExtent #$UnaryPredicate )
ASSERTION-537
(#$arity #$minimizeExtent 1 )
ASSERTION-538
(#$arg1Isa #$minimizeExtent #$Predicate )

;;; #$mtInferenceFunction

ASSERTION-539
(#$isa #$mtInferenceFunction #$BinaryPredicate )
ASSERTION-540
(#$arity #$mtInferenceFunction 2 )
ASSERTION-541
(#$arg1Isa #$mtInferenceFunction #$Microtheory )
ASSERTION-542
(#$arg2Isa #$mtInferenceFunction #$CycSystemSymbol )

;;; #$myCreationTime

ASSERTION-543
(#$isa #$myCreationTime #$BinaryPredicate )
ASSERTION-544
(#$isa #$myCreationTime #$BookkeepingPredicate )
ASSERTION-545
(#$arity #$myCreationTime 2 )
ASSERTION-546
(#$arg1Isa #$myCreationTime #$Thing )
ASSERTION-547
(#$arg2Isa #$myCreationTime #$PositiveInteger )

;;; #$myCreator

ASSERTION-548
(#$isa #$myCreator #$BinaryPredicate )
ASSERTION-549
(#$isa #$myCreator #$BookkeepingPredicate )
ASSERTION-550
(#$arity #$myCreator 2)
ASSERTION-551
(#$arg1Isa #$myCreator #$Thing )
ASSERTION-552
(#$arg2Isa #$myCreator #$Cyclist )

;;; #$negationAttribute

ASSERTION-553
(#$isa #$negationAttribute #$SymmetricBinaryPredicate )
ASSERTION-554
(#$isa #$negationAttribute #$IrreflexiveBinaryPredicate )
ASSERTION-555
(#$genlInverse #$negationAttribute #$negationAttribute )
ASSERTION-556
(#$arity #$negationAttribute 2)
ASSERTION-557
(#$arg1Isa #$negationAttribute #$AttributeValue )
ASSERTION-558
(#$arg2Isa #$negationAttribute #$AttributeValue )

;;; #$negationInverse

ASSERTION-559
(#$isa #$negationInverse #$SymmetricBinaryPredicate )
ASSERTION-560
(#$isa #$negationInverse #$IrreflexiveBinaryPredicate )
ASSERTION-561
(#$genlInverse #$negationInverse #$negationInverse )
ASSERTION-562
(#$arity #$negationInverse 2 )
ASSERTION-563
(#$arg1Isa #$negationInverse #$BinaryPredicate )
ASSERTION-564
(#$arg2Isa #$negationInverse #$BinaryPredicate )

ASSERTION-565
(#$not   (#$and 
    (#$negationInverse ?GEN-PRED ?PRED) 
    (?PRED ?ARG1 ?ARG2) 
    (?GEN-PRED ?ARG2 ?ARG1)
                )  )

;;; #$negationPreds

ASSERTION-566
(#$isa #$negationPreds #$SymmetricBinaryPredicate )
ASSERTION-567
(#$genlInverse #$negationPreds #$negationPreds)
ASSERTION-568
(#$arity #$negationPreds 2 )
ASSERTION-569
(#$arg1Isa #$negationPreds #$Predicate )
ASSERTION-570
(#$arg2Isa #$negationPreds #$Predicate )

ASSERTION-571
(#$not    (#$and 
   (?PRED ?ARG1) 
   (?NEG-PRED ?ARG1) 
   (#$negationPreds ?NEG-PRED ?PRED )
         )    )

ASSERTION-572
(#$not     (#$and 
   (#$negationPreds ?NEG-PRED ?PRED) 
   (?PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4 ?ARG5) 
   (?NEG-PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4 ?ARG5)
                   )    )

ASSERTION-573
(#$not      (#$and 
   (#$negationPreds ?NEG-PRED ?PRED) 
   (?PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4) 
   (?NEG-PRED ?ARG1 ?ARG2 ?ARG3 ?ARG4 )
                    )     )

ASSERTION-574
(#$not     (#$and 
   (#$negationPreds ?NEG-PRED ?PRED) 
   (?PRED ?ARG1 ?ARG2 ?ARG3) 
   (?NEG-PRED ?ARG1 ?ARG2 ?ARG3)
                )    )

ASSERTION-575
(#$not   (#$and 
   (#$negationPreds ?NEG-PRED ?PRED) 
   (?PRED ?ARG1 ?ARG2) 
   (?NEG-PRED ?ARG1 ?ARG2)
                     )        )

;;; #$not

ASSERTION-576
(#$isa #$not #$Relationship )
ASSERTION-577
(#$arity #$not 1 )
ASSERTION-578
(#$arg1Isa #$not #$CycFormula )
ASSERTION-579
(#$resultIsa #$not #$CycFormula )

;;; #$oldConstantName

ASSERTION-580
(#$isa #$oldConstantName #$BinaryPredicate )
ASSERTION-581
(#$arity #$oldConstantName 2 )
ASSERTION-582
(#$arg1Isa #$oldConstantName #$Thing )
ASSERTION-583
(#$arg2Isa #$oldConstantName #$CycSystemString )

;;; #$or

ASSERTION-584
(#$isa #$or #$CommutativeRelation )
ASSERTION-585
(#$isa #$or #$VariableArityRelation )
ASSERTION-586
(#$argsIsa #$or #$CycFormula )
ASSERTION-587
(#$resultIsa #$or #$CycFormula )

;;; #$relationAllExists

ASSERTION-588
(#$isa #$relationAllExists #$TernaryPredicate )
ASSERTION-589
(#$arity #$relationAllExists 3 )
ASSERTION-590
(#$arg1Isa #$relationAllExists #$BinaryPredicate )
ASSERTION-591
(#$arg2Isa #$relationAllExists #$Collection )
ASSERTION-592
(#$arg3Isa #$relationAllExists #$Collection )

;;; #$relationAllExistsCount

ASSERTION-593
(#$isa #$relationAllExistsCount #$QuaternaryPredicate )
ASSERTION-594
(#$arity #$relationAllExistsCount 4 )
ASSERTION-595
(#$arg1Isa #$relationAllExistsCount #$BinaryPredicate )
ASSERTION-596
(#$arg2Isa #$relationAllExistsCount #$Collection )
ASSERTION-597
(#$arg3Isa #$relationAllExistsCount #$Collection )
ASSERTION-598
(#$arg4Isa #$relationAllExistsCount #$NonNegativeInteger )

;;; #$requiredArg1Pred

ASSERTION-600
(#$isa #$requiredArg1Pred #$BinaryPredicate )
ASSERTION-601
(#$arity #$requiredArg1Pred 2 )
ASSERTION-602
(#$arg1Isa #$requiredArg1Pred #$Collection )
ASSERTION-603
(#$arg2Isa #$requiredArg1Pred #$Predicate )

;;; #$requiredArg2Pred

ASSERTION-604
(#$isa #$requiredArg2Pred #$BinaryPredicate )
ASSERTION-605
(#$arity #$requiredArg2Pred 2 )
ASSERTION-606
(#$arg1Isa #$requiredArg2Pred #$Collection )
ASSERTION-607
(#$arg2Isa #$requiredArg2Pred #$Predicate )

;;; #$resultgenl

ASSERTION-608
(#$isa #$resultgenl #$BinaryPredicate )
ASSERTION-609
(#$arity #$resultGenl 2  )
ASSERTION-610
(#$arg1Isa #$resultGenl #$CollectionDenotingFunction )
ASSERTION-611
(#$arg2Isa #$resultGenl #$Collection )

;;; #$resultIsa

ASSERTION-612
(#$isa #$resultIsa #$BinaryPredicate )
ASSERTION-613
(#$arity #$resultIsa 2 )
ASSERTION-614
(#$arg1Isa #$resultIsa #$Relationship )
ASSERTION-615
(#$arg2Isa #$resultIsa #$Collection )

;;; #$satisfiesDescription

ASSERTION-616
(#$isa #$satisfiesDescription #$TernaryPredicate )
ASSERTION-617
(#$arity #$satisfiesDescription 3 )
ASSERTION-618
(#$arg1Isa #$satisfiesDescription #$CycSystemList )
ASSERTION-619
(#$arg2Isa #$satisfiesDescription #$CycSystemList )
ASSERTION-620
(#$arg3Isa #$satisfiesDescription #$Microtheory )


;;; #$siblingDisjointExceptions

ASSERTION-621
(#$isa #$siblingDisjointExceptions #$SymmetricBinaryPredicate )
ASSERTION-622
(#$isa #$siblingDisjointExceptions #$IrreflexiveBinaryPredicate )
ASSERTION-623
(#$genlInverse]] #$siblingDisjointExceptions #$siblingDisjointExceptions )
ASSERTION-624
(#$arity #$siblingDisjointExceptions 2 )
ASSERTION-625
(#$arg1Isa #$siblingDisjointExceptions #$Collection )
ASSERTION-626
(#$arg2Isa #$siblingDisjointExceptions #$Collection )

ASSERTION-627
(#$implies 
    (#$siblingDisjointExceptions ?C1 ?C2 ) 
    (#$siblingDisjointExceptions ?C1 ?C2 ) 
)

;;; #$termOfUnit

ASSERTION-628
(#$isa #$termOfUnit #$DefaultMonotonicPredicate )
ASSERTION-629
(#$isa #$termOfUnit #$InferenceRelatedBookkeepingPredicate )
ASSERTION-630
(#$isa #$termOfUnit #$BinaryPredicate )
ASSERTION-631
(#$arity #$termOfUnit 2 )
ASSERTION-632
(#$arg1Isa #$termOfUnit #$ReifiableTerm )
ASSERTION-633
(#$arg2Isa #$termOfUnit #$CycSystemList )

;;; #$thereExistAtLeast

ASSERTION-634
(#$isa #$thereExistAtLeast #$Relationship )
ASSERTION-635
(#$arity #$thereExistAtLeast 3 )
ASSERTION-636
(#$resultIsa #$thereExistAtLeast #$CycFormula )
ASSERTION-637
(#$arg3Isa #$thereExistAtLeast #$CycFormula )
ASSERTION-638
(#$arg2Isa #$thereExistAtLeast #$CycELVariable )
ASSERTION-639
(#$arg1Isa #$thereExistAtLeast #$PositiveInteger )

;;; #$thereExistAtMost

ASSERTION-640
(#$isa #$thereExistAtMost #$Relationship )
ASSERTION-641
(#$arity #$thereExistAtMost 3 )
ASSERTION-642
(#$resultIsa #$thereExistAtMost #$CycFormula )
ASSERTION-643
(#$arg3Isa #$thereExistAtMost #$CycFormula )
ASSERTION-644
(#$arg2Isa #$thereExistAtMost #$CycELVariable )
ASSERTION-645
(#$arg1Isa #$thereExistAtMost #$PositiveInteger )

;;; #$thereExistExactly

ASSERTION-646
(#$isa #$thereExistExactly #$Relationship )
ASSERTION-647
(#$arity #$thereExistExactly 3 )
ASSERTION-648
(#$resultIsa #$thereExistExactly #$CycFormula )
ASSERTION-649
(#$arg3Isa #$thereExistExactly #$CycFormula )
ASSERTION-650
(#$arg2Isa #$thereExistExactly #$CycELVariable )
ASSERTION-651
(#$arg1Isa #$thereExistExactly #$PositiveInteger)

;;; #$thereExists

ASSERTION-652
(#$isa #$thereExists #$Relationship )
ASSERTION-653
(#$arity #$thereExists 2 )
ASSERTION-654
(#$arg2Isa #$thereExists #$CycFormula )
ASSERTION-655
(#$arg1Isa #$thereExists #$CycELVariable )