=> (=>)

The truth-functional connective of implication.

Ontology

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

logical operator

Coordinate term(s)

<=> and entails exists forall not or

Type restrictions

=>(formula, formula)

Related WordNet synsets

See more related synsets on a separate page.

Axioms (679)

If entity is an immediate instance of class, then there doesn't exist class subclass so that entity is an instance of subclass.

(=>
      (immediateInstance ?ENTITY ?CLASS)
      (not
            (exists
                  (?SUBCLASS)
                  (and
                        (subclass ?SUBCLASS ?CLASS)
                        (instance ?ENTITY ?SUBCLASS)))))

If rel1 is an inverse of rel2, then for all inst1,inst2 holds: rel1(inst1,inst2) holds if and only if rel2(inst2,inst1) holds.

(=>
      (inverse ?REL1 ?REL2)
      (forall
            (?INST1 ?INST2)
            (<=>
                  (holds ?REL1 ?INST1 ?INST2)
                  (holds ?REL2 ?INST2 ?INST1))))

subclass is a subclass of class if and only if

subclass is an instance of set or class
class is an instance of set or class
for all inst holds: if inst is an instance of subclass, then inst is an instance of class

(<=>
      (subclass ?SUBCLASS ?CLASS)
      (and
            (instance ?SUBCLASS SetOrClass)
            (instance ?CLASS SetOrClass)
            (forall
                  (?INST)
                  (=>
                        (instance ?INST ?SUBCLASS)
                        (instance ?INST ?CLASS)))))

If class1 is an immediate subclass of class2, then there doesn't exist class2 class3 so that class1 is a subclass of class3 and class2 is not equal to class3 and class1 is not equal to class3.

(=>
      (immediateSubclass ?CLASS1 ?CLASS2)
      (not
            (exists
                  (?CLASS3)
                  (and
                        (subclass ?CLASS3 ?CLASS2)
                        (subclass ?CLASS1 ?CLASS3)
                        (not
                              (equal ?CLASS2 ?CLASS3))
                        (not
                              (equal ?CLASS1 ?CLASS3))))))

If pred1 is a subrelation of pred2 and pred1 %&has number argument(s), then pred2 %&has number argument(s).

(=>
      (and
            (subrelation ?PRED1 ?PRED2)
            (valence ?PRED1 ?NUMBER))
      (valence ?PRED2 ?NUMBER))

If pred1 is a subrelation of pred2 and the number number argument of pred2 is an instance of class1, then the number number argument of pred1 is an instance of class1.

(=>
      (and
            (subrelation ?PRED1 ?PRED2)
            (domain ?PRED2 ?NUMBER ?CLASS1))
      (domain ?PRED1 ?NUMBER ?CLASS1))

If rel1 is a subrelation of rel2 and rel1() holds, then rel2() holds.

(=>
      (and
            (subrelation ?REL1 ?REL2)
            (holds ?REL1 @ROW))
      (holds ?REL2 @ROW))

If pred1 is a subrelation of pred2 and pred2 is an instance of class and class is an instance of inheritable relation, then pred1 is an instance of class.

(=>
      (and
            (subrelation ?PRED1 ?PRED2)
            (instance ?PRED2 ?CLASS)
            (instance ?CLASS InheritableRelation))
      (instance ?PRED1 ?CLASS))

If the number number argument of rel is an instance of class1 and the number number argument of rel is an instance of class2, then class1 is a subclass of class2 or class2 is a subclass of class1.

(=>
      (and
            (domain ?REL ?NUMBER ?CLASS1)
            (domain ?REL ?NUMBER ?CLASS2))
      (or
            (subclass ?CLASS1 ?CLASS2)
            (subclass ?CLASS2 ?CLASS1)))

If rel1 is a subrelation of rel2 and the number number argument of rel2 is a subclass of class1, then the number number argument of rel1 is a subclass of class1.

(=>
      (and
            (subrelation ?REL1 ?REL2)
            (domainSubclass ?REL2 ?NUMBER ?CLASS1))
      (domainSubclass ?REL1 ?NUMBER ?CLASS1))

If the number number argument of rel is a subclass of class1 and the number number argument of rel is a subclass of class2, then class1 is a subclass of class2 or class2 is a subclass of class1.

(=>
      (and
            (domainSubclass ?REL ?NUMBER ?CLASS1)
            (domainSubclass ?REL ?NUMBER ?CLASS2))
      (or
            (subclass ?CLASS1 ?CLASS2)
            (subclass ?CLASS2 ?CLASS1)))

If thing1 is equal to thing2, then for all attr holds: thing1 has an attribute attr if and only if thing2 has an attribute attr.

(=>
      (equal ?THING1 ?THING2)
      (forall
            (?ATTR)
            (<=>
                  (property ?THING1 ?ATTR)
                  (property ?THING2 ?ATTR))))

If attr1 is equal to attr2, then for all thing holds: thing has an attribute attr1 if and only if thing has an attribute attr2.

(=>
      (equal ?ATTR1 ?ATTR2)
      (forall
            (?THING)
            (<=>
                  (property ?THING ?ATTR1)
                  (property ?THING ?ATTR2))))

If thing1 is equal to thing2, then for all class holds: thing1 is an instance of class if and only if thing2 is an instance of class.

(=>
      (equal ?THING1 ?THING2)
      (forall
            (?CLASS)
            (<=>
                  (instance ?THING1 ?CLASS)
                  (instance ?THING2 ?CLASS))))

If class1 is equal to class2, then for all thing holds: thing is an instance of class1 if and only if thing is an instance of class2.

(=>
      (equal ?CLASS1 ?CLASS2)
      (forall
            (?THING)
            (<=>
                  (instance ?THING ?CLASS1)
                  (instance ?THING ?CLASS2))))

If rel1 is equal to rel2, then for all holds: rel1() holds if and only if rel2() holds.

(=>
      (equal ?REL1 ?REL2)
      (forall
            (@ROW)
            (<=>
                  (holds ?REL1 @ROW)
                  (holds ?REL2 @ROW))))

if obj1 is equal to obj2,
then if obj1 is equal to "numberth element of "()"" and obj2 is equal to "numberth element of "()"" and "()" is equal to "()", then () holds if and only if () holds

(=>
      (equal ?OBJ1 ?OBJ2)
      (=>
            (and
                  (equal
                        ?OBJ1
                        (ListOrderFn
                              (ListFn @ROW1)
                              ?NUMBER))
                  (equal
                        ?OBJ2
                        (ListOrderFn
                              (ListFn @ROW2)
                              ?NUMBER))
                  (equal
                        (ListFn @ROW1)
                        (ListFn @ROW2)))
            (<=>
                  (holds @ROW1)
                  (holds @ROW2))))

if list1 is equal to list2,
then if list1 is equal to "()" and list2 is equal to "()", then for all number holds: "numberth element of "()"" is equal to "numberth element of "()""

(=>
      (equal ?LIST1 ?LIST2)
      (=>
            (and
                  (equal
                        ?LIST1
                        (ListFn @ROW1))
                  (equal
                        ?LIST2
                        (ListFn @ROW2)))
            (forall
                  (?NUMBER)
                  (equal
                        (ListOrderFn
                              (ListFn @ROW1)
                              ?NUMBER)
                        (ListOrderFn
                              (ListFn @ROW2)
                              ?NUMBER)))))

If range of function is an instance of class and "function()" is equal to value, then value is an instance of class.

(=>
      (and
            (range ?FUNCTION ?CLASS)
            (equal
                  (AssignmentFn ?FUNCTION @ROW)
                  ?VALUE))
      (instance ?VALUE ?CLASS))

If rel1 is a subrelation of rel2 and range of rel2 is an instance of class1, then range of rel1 is an instance of class1.

(=>
      (and
            (subrelation ?REL1 ?REL2)
            (range ?REL2 ?CLASS1))
      (range ?REL1 ?CLASS1))

If range of rel is an instance of class1 and range of rel is an instance of class2, then class1 is a subclass of class2 or class2 is a subclass of class1.

(=>
      (and
            (range ?REL ?CLASS1)
            (range ?REL ?CLASS2))
      (or
            (subclass ?CLASS1 ?CLASS2)
            (subclass ?CLASS2 ?CLASS1)))

If the values returned by function are subclasses of class and "function()" is equal to value, then value is a subclass of class.

(=>
      (and
            (rangeSubclass ?FUNCTION ?CLASS)
            (equal
                  (AssignmentFn ?FUNCTION @ROW)
                  ?VALUE))
      (subclass ?VALUE ?CLASS))

If rel1 is a subrelation of rel2 and the values returned by rel2 are subclasses of class1, then the values returned by rel1 are subclasses of class1.

(=>
      (and
            (subrelation ?REL1 ?REL2)
            (rangeSubclass ?REL2 ?CLASS1))
      (rangeSubclass ?REL1 ?CLASS1))

If the values returned by rel are subclasses of class1 and the values returned by rel are subclasses of class2, then class1 is a subclass of class2 or class2 is a subclass of class1.

(=>
      (and
            (rangeSubclass ?REL ?CLASS1)
            (rangeSubclass ?REL ?CLASS2))
      (or
            (subclass ?CLASS1 ?CLASS2)
            (subclass ?CLASS2 ?CLASS1)))

If and ? are disjoint and rel is a member of "()", then rel is an instance of relation.

(=>
      (and
            (disjointRelation @ROW)
            (inList
                  ?REL
                  (ListFn @ROW)))
      (instance ?REL Relation))

If and ? are disjoint and rel1 is a member of "()" and rel2 is a member of "()" and rel1 %&has number argument(s), then rel2 %&has number argument(s).

(=>
      (and
            (disjointRelation @ROW)
            (inList
                  ?REL1
                  (ListFn @ROW))
            (inList
                  ?REL2
                  (ListFn @ROW))
            (valence ?REL1 ?NUMBER))
      (valence ?REL2 ?NUMBER))

If the number number argument of rel1 is an instance of class1 and the number number argument of rel2 is an instance of class2 and class1 is disjoint from class2, then rel1 and rel2 are disjoint.

(=>
      (and
            (domain ?REL1 ?NUMBER ?CLASS1)
            (domain ?REL2 ?NUMBER ?CLASS2)
            (disjoint ?CLASS1 ?CLASS2))
      (disjointRelation ?REL1 ?REL2))

If the number number argument of rel1 is a subclass of class1 and the number number argument of rel2 is a subclass of class2 and class1 is disjoint from class2, then rel1 and rel2 are disjoint.

(=>
      (and
            (domainSubclass ?REL1 ?NUMBER ?CLASS1)
            (domainSubclass ?REL2 ?NUMBER ?CLASS2)
            (disjoint ?CLASS1 ?CLASS2))
      (disjointRelation ?REL1 ?REL2))

If range of rel1 is an instance of class1 and range of rel2 is an instance of class2 and class1 is disjoint from class2, then rel1 and rel2 are disjoint.

(=>
      (and
            (range ?REL1 ?CLASS1)
            (range ?REL2 ?CLASS2)
            (disjoint ?CLASS1 ?CLASS2))
      (disjointRelation ?REL1 ?REL2))

If the values returned by rel1 are subclasses of class1 and the values returned by rel2 are subclasses of class2 and class1 is disjoint from class2, then rel1 and rel2 are disjoint.

(=>
      (and
            (rangeSubclass ?REL1 ?CLASS1)
            (rangeSubclass ?REL2 ?CLASS2)
            (disjoint ?CLASS1 ?CLASS2))
      (disjointRelation ?REL1 ?REL2))

If and ? are disjoint and rel1 is a member of "()" and rel2 is a member of "()" and rel1 is not equal to rel2 and rel1() holds, then rel2() doesn't hold.

(=>
      (and
            (disjointRelation @ROW1)
            (inList
                  ?REL1
                  (ListFn @ROW1))
            (inList
                  ?REL2
                  (ListFn @ROW1))
            (not
                  (equal ?REL1 ?REL2))
            (holds ?REL1 @ROW2))
      (not
            (holds ?REL2 @ROW2)))

if is opposed to ?,
then if element is a member of "()", then element is an instance of attribute

(=>
      (contraryAttribute @ROW)
      (=>
            (inList
                  ?ELEMENT
                  (ListFn @ROW))
            (instance ?ELEMENT Attribute)))

if is opposed to ?,
then for all attr1,attr2 holds:
- if attr1 is equal to "number1th element of "()"" and attr2 is equal to "number2th element of "()"" and number1 is not equal to number2,
- then if obj has an attribute attr1, then obj has not an attribute attr2

(=>
      (contraryAttribute @ROW)
      (forall
            (?ATTR1 ?ATTR2)
            (=>
                  (and
                        (equal
                              ?ATTR1
                              (ListOrderFn
                                    (ListFn @ROW)
                                    ?NUMBER1))
                        (equal
                              ?ATTR2
                              (ListOrderFn
                                    (ListFn @ROW)
                                    ?NUMBER2))
                        (not
                              (equal ?NUMBER1 ?NUMBER2)))
                  (=>
                        (property ?OBJ ?ATTR1)
                        (not
                              (property ?OBJ ?ATTR2))))))

if exhaustive attribute(class,) holds,
then if attr is a member of "()", then attr is an instance of attribute

(=>
      (exhaustiveAttribute ?CLASS @ROW)
      (=>
            (inList
                  ?ATTR
                  (ListFn @ROW))
            (instance ?ATTR Attribute)))

if exhaustive attribute(class,) holds,
then for all obj holds: if attr1 is an instance of class, then there exists attr2 so that attr2 is a member of "()" and attr1 is equal to attr2

(=>
      (exhaustiveAttribute ?CLASS @ROW)
      (forall
            (?OBJ)
            (=>
                  (instance ?ATTR1 ?CLASS)
                  (exists
                        (?ATTR2)
                        (and
                              (inList
                                    ?ATTR2
                                    (ListFn @ROW))
                              (equal ?ATTR1 ?ATTR2))))))

if is covered by ,
then if element is a member of "()", then element is an instance of class

(=>
      (exhaustiveDecomposition @ROW)
      (=>
            (inList
                  ?ELEMENT
                  (ListFn @ROW))
            (instance ?ELEMENT Class)))

if is disjointly decomposed into ,
then if element is a member of "()", then element is an instance of class

(=>
      (disjointDecomposition @ROW)
      (=>
            (inList
                  ?ELEMENT
                  (ListFn @ROW))
            (instance ?ELEMENT Class)))

if attr1 is a subattribute of attr2,
then for all obj holds: if obj has an attribute attr1, then obj has an attribute attr2

(=>
      (subAttribute ?ATTR1 ?ATTR2)
      (forall
            (?OBJ)
            (=>
                  (property ?OBJ ?ATTR1)
                  (property ?OBJ ?ATTR2))))

If attr1 is a subattribute of attr2 and attr2 is an instance of class, then attr1 is an instance of class.

(=>
      (and
            (subAttribute ?ATTR1 ?ATTR2)
            (instance ?ATTR2 ?CLASS))
      (instance ?ATTR1 ?CLASS))

If attr1 is an immediate successor attribute of attr2 and entity has an attribute attr2 during time1, then there exists time2 so that time2 is a part of "before time1" and entity has an attribute attr1 during time2.

(=>
      (and
            (successorAttribute ?ATTR1 ?ATTR2)
            (holdsDuring
                  ?TIME1
                  (property ?ENTITY ?ATTR2)))
      (exists
            (?TIME2)
            (and
                  (temporalPart
                        ?TIME2
                        (PastFn ?TIME1))
                  (holdsDuring
                        ?TIME2
                        (property ?ENTITY ?ATTR1)))))

If attr1 is an immediate successor attribute of attr2, then attr1 is a successor attribute of attr2.

(=>
      (successorAttribute ?ATTR1 ?ATTR2)
      (successorAttributeClosure ?ATTR1 ?ATTR2))

If rel(,inst) holds and rel is an instance of function, then "rel()" is equal to inst.

(=>
      (and
            (holds ?REL @ROW ?INST)
            (instance ?REL Function))
      (equal
            (AssignmentFn ?REL @ROW)
            ?INST))

If class is an instance of class, then class is a subclass of entity.

(=>
      (instance ?CLASS Class)
      (subclass ?CLASS Entity))

If obj is an instance of self connected object, then "the front of obj" is a part of obj.

(=>
      (instance ?OBJ SelfConnectedObject)
      (part
            (FrontFn ?OBJ)
            ?OBJ))

If obj is an instance of self connected object, then "the back of obj" is a part of obj.

(=>
      (instance ?OBJ SelfConnectedObject)
      (part
            (BackFn ?OBJ)
            ?OBJ))

if substance1 is a piece of substance2,
then for all class holds: if substance1 is an instance of class, then substance2 is an instance of class

(=>
      (piece ?SUBSTANCE1 ?SUBSTANCE2)
      (forall
            (?CLASS)
            (=>
                  (instance ?SUBSTANCE1 ?CLASS)
                  (instance ?SUBSTANCE2 ?CLASS))))

If objecttype is a subclass of substance and object is an instance of objecttype and part is a part of object, then part is an instance of objecttype.

(=>
      (and
            (subclass ?OBJECTTYPE Substance)
            (instance ?OBJECT ?OBJECTTYPE)
            (part ?PART ?OBJECT))
      (instance ?PART ?OBJECTTYPE))

If obj is an instance of substance and attr is an attribute of obj and part is a part of obj, then attr is an attribute of part.

(=>
      (and
            (instance ?OBJ Substance)
            (attribute ?OBJ ?ATTR)
            (part ?PART ?OBJ))
      (attribute ?PART ?ATTR))

If atom is an instance of atom, then there exist proton proton,electron electron so that proton is a component of atom and electron is a component of atom.

(=>
      (instance ?ATOM Atom)
      (exists
            (?PROTON ?ELECTRON)
            (and
                  (component ?PROTON ?ATOM)
                  (component ?ELECTRON ?ATOM)
                  (instance ?PROTON Proton)
                  (instance ?ELECTRON Electron))))

if atom is an instance of atom,
then for all nucleus1,nucleus2 holds: if nucleus1 is a component of atom and nucleus2 is a component of atom and nucleus1 is an instance of atomic nucleus and nucleus2 is an instance of atomic nucleus, then nucleus1 is equal to nucleus2

(=>
      (instance ?ATOM Atom)
      (forall
            (?NUCLEUS1 ?NUCLEUS2)
            (=>
                  (and
                        (component ?NUCLEUS1 ?ATOM)
                        (component ?NUCLEUS2 ?ATOM)
                        (instance ?NUCLEUS1 AtomicNucleus)
                        (instance ?NUCLEUS2 AtomicNucleus))
                  (equal ?NUCLEUS1 ?NUCLEUS2))))

If particle is an instance of subatomic particle, then there exists atom atom so that particle is a part of atom.

(=>
      (instance ?PARTICLE SubatomicParticle)
      (exists
            (?ATOM)
            (and
                  (instance ?ATOM Atom)
                  (part ?PARTICLE ?ATOM))))

If nucleus is an instance of atomic nucleus, then there exist neutron neutron,proton proton so that neutron is a component of nucleus and proton is a component of nucleus.

(=>
      (instance ?NUCLEUS AtomicNucleus)
      (exists
            (?NEUTRON ?PROTON)
            (and
                  (component ?NEUTRON ?NUCLEUS)
                  (component ?PROTON ?NUCLEUS)
                  (instance ?NEUTRON Neutron)
                  (instance ?PROTON Proton))))

If mixture is an instance of mixture, then there exist pure substance pure1,pure substance pure2 so that pure1 is not equal to pure2 and pure1 is a piece of mixture and pure2 is a piece of mixture.

(=>
      (instance ?MIXTURE Mixture)
      (exists
            (?PURE1 ?PURE2)
            (and
                  (subclass ?PURE1 PureSubstance)
                  (subclass ?PURE2 PureSubstance)
                  (not
                        (equal ?PURE1 ?PURE2))
                  (piece ?PURE1 ?MIXTURE)
                  (piece ?PURE2 ?MIXTURE))))

If obj is an instance of corpuscular object, then there exist substance substance1,substance substance2 so that substance1 is made of obj and substance2 is made of obj and substance1 is not equal to substance2.

(=>
      (instance ?OBJ CorpuscularObject)
      (exists
            (?SUBSTANCE1 ?SUBSTANCE2)
            (and
                  (subclass ?SUBSTANCE1 Substance)
                  (subclass ?SUBSTANCE2 Substance)
                  (material ?SUBSTANCE1 ?OBJ)
                  (material ?SUBSTANCE2 ?OBJ)
                  (not
                        (equal ?SUBSTANCE1 ?SUBSTANCE2)))))

If region is an instance of region, then there exists phys so that phys is located at region.

(=>
      (instance ?REGION Region)
      (exists
            (?PHYS)
            (located ?PHYS ?REGION)))

If coll is an instance of collection, then there exists obj so that obj is a member of coll.

(=>
      (instance ?COLL Collection)
      (exists
            (?OBJ)
            (member ?OBJ ?COLL)))

coll1 is a proper sub-collection of coll2 if and only if

coll1 is an instance of collection
coll2 is an instance of collection
for all member holds: if member is a member of coll1, then member is a member of coll2

(<=>
      (subCollection ?COLL1 ?COLL2)
      (and
            (instance ?COLL1 Collection)
            (instance ?COLL2 Collection)
            (forall
                  (?MEMBER)
                  (=>
                        (member ?MEMBER ?COLL1)
                        (member ?MEMBER ?COLL2)))))

If string is an instance of symbolic string, then there exists character part so that part is a part of string.

(=>
      (instance ?STRING SymbolicString)
      (exists
            (?PART)
            (and
                  (part ?PART ?STRING)
                  (instance ?PART Character))))

If lang is an instance of animal language and proc is an agent of agent and lang is an instrument for proc, then agent is an instance of animal and agent is not an instance of human.

(=>
      (and
            (instance ?LANG AnimalLanguage)
            (agent ?PROC ?AGENT)
            (instrument ?PROC ?LANG))
      (and
            (instance ?AGENT Animal)
            (not
                  (instance ?AGENT Human))))

If lang is an instance of computer language and proc is an agent of agent and lang is an instrument for proc, then agent is an instance of machine.

(=>
      (and
            (instance ?LANG ComputerLanguage)
            (agent ?PROC ?AGENT)
            (instrument ?PROC ?LANG))
      (instance ?AGENT Machine))

If lang is an instance of human language and proc is an agent of agent and lang is an instrument for proc, then agent is an instance of human.

(=>
      (and
            (instance ?LANG HumanLanguage)
            (agent ?PROC ?AGENT)
            (instrument ?PROC ?LANG))
      (instance ?AGENT Human))

If lang is an instance of constructed language, then there exists planning plan so that lang is a result of plan.

(=>
      (instance ?LANG ConstructedLanguage)
      (exists
            (?PLAN)
            (and
                  (instance ?PLAN Planning)
                  (result ?PLAN ?LANG))))

If process is an instance of dual object process, then there exist obj1,obj2 so that obj1 is a patient of process and obj2 is a patient of process and obj1 is not equal to obj2.

(=>
      (instance ?PROCESS DualObjectProcess)
      (exists
            (?OBJ1 ?OBJ2)
            (and
                  (patient ?PROCESS ?OBJ1)
                  (patient ?PROCESS ?OBJ2)
                  (not
                        (equal ?OBJ1 ?OBJ2)))))

If number is an instance of imaginary number, then there exists real number real so that number is equal to "real*"the square root of "".

(=>
      (instance ?NUMBER ImaginaryNumber)
      (exists
            (?REAL)
            (and
                  (instance ?REAL RealNumber)
                  (equal
                        ?NUMBER
                        (MultiplicationFn
                              ?REAL
                              (SquareRootFn -1))))))

If number is an instance of complex number, then there exist real number real1,real number real2 so that number is equal to "(real1+"real2*"the square root of "")".

(=>
      (instance ?NUMBER ComplexNumber)
      (exists
            (?REAL1 ?REAL2)
            (and
                  (instance ?REAL1 RealNumber)
                  (instance ?REAL2 RealNumber)
                  (equal
                        ?NUMBER
                        (AdditionFn
                              ?REAL1
                              (MultiplicationFn
                                    ?REAL2
                                    (SquareRootFn -1)))))))

If function is an instance of unary constant functionquantity, then the number argument of function is an instance of constant quantity and range of function is an instance of constant quantity.

(=>
      (instance ?FUNCTION UnaryConstantFunctionQuantity)
      (and
            (domain ?FUNCTION 1 ConstantQuantity)
            (range ?FUNCTION ConstantQuantity)))

If function is an instance of time dependent quantity, then the number argument of function is an instance of time measure.

(=>
      (instance ?FUNCTION TimeDependentQuantity)
      (domain ?FUNCTION 1 TimeMeasure))

If rel is an instance of relation, then rel() holds if and only if rel() holds.

(=>
      (instance ?REL Relation)
      (<=>
            (holds ?REL @ROW)
            (?REL @ROW)))

rel is an instance of single valued relation if and only if for all ,item1,item2 holds: if rel(,item1) holds and rel(,item2) holds, then item1 is equal to item2.

(<=>
      (instance ?REL SingleValuedRelation)
      (forall
            (@ROW ?ITEM1 ?ITEM2)
            (=>
                  (and
                        (holds ?REL @ROW ?ITEM1)
                        (holds ?REL @ROW ?ITEM2))
                  (equal ?ITEM1 ?ITEM2))))

rel is an instance of total valued relation if and only if there exists valence so that rel is an instance of relation and rel %&has valence argument(s) and

if for all number,element,class holds: if number is less than valence and the number number argument of rel is an instance of class and element is equal to "numberth element of "()"", then element is an instance of class,
then there exists item so that rel(,item) holds

(<=>
      (instance ?REL TotalValuedRelation)
      (exists
            (?VALENCE)
            (and
                  (instance ?REL Relation)
                  (valence ?REL ?VALENCE)
                  (=>
                        (forall
                              (?NUMBER ?ELEMENT ?CLASS)
                              (=>
                                    (and
                                          (lessThan ?NUMBER ?VALENCE)
                                          (domain ?REL ?NUMBER ?CLASS)
                                          (equal
                                                ?ELEMENT
                                                (ListOrderFn
                                                      (ListFn @ROW)
                                                      ?NUMBER)))
                                    (instance ?ELEMENT ?CLASS)))
                        (exists
                              (?ITEM)
                              (holds ?REL @ROW ?ITEM))))))

If rel is an instance of binary relation, then there don't exist item1,item2,item3, so that rel(item1,item2,item3,) holds.

(=>
      (instance ?REL BinaryRelation)
      (not
            (exists
                  (?ITEM1 ?ITEM2 ?ITEM3 @ROW)
                  (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 @ROW))))

if rel is an instance of reflexive relation,
then if rel(inst1,inst2) holds or rel(inst2,inst1) holds, then rel(inst1,inst1) holds

(=>
      (instance ?REL ReflexiveRelation)
      (=>
            (or
                  (holds ?REL ?INST1 ?INST2)
                  (holds ?REL ?INST2 ?INST1))
            (holds ?REL ?INST1 ?INST1)))

If rel is an instance of irreflexive relation, then for all inst holds: rel(inst,inst) doesn't hold.

(=>
      (instance ?REL IrreflexiveRelation)
      (forall
            (?INST)
            (not
                  (holds ?REL ?INST ?INST))))

if rel is an instance of symmetric relation,
then for all inst1,inst2 holds: if rel(inst1,inst2) holds, then rel(inst2,inst1) holds

(=>
      (instance ?REL SymmetricRelation)
      (forall
            (?INST1 ?INST2)
            (=>
                  (holds ?REL ?INST1 ?INST2)
                  (holds ?REL ?INST2 ?INST1))))

rel is an instance of binary relation
the number argument of rel is an instance of class1 or the number argument of rel is a subclass of class1
the number argument of rel is an instance of class2 or the number argument of rel is a subclass of class2 or range of rel is an instance of class2 or the values returned by rel are subclasses of class2
class1 is disjoint from class2

, then rel is an instance of asymmetric relation.

(=>
      (and
            (instance ?REL BinaryRelation)
            (or
                  (domain ?REL 1 ?CLASS1)
                  (domainSubclass ?REL 1 ?CLASS1))
            (or
                  (domain ?REL 2 ?CLASS2)
                  (domainSubclass ?REL 2 ?CLASS2)
                  (range ?REL ?CLASS2)
                  (rangeSubclass ?REL ?CLASS2))
            (disjoint ?CLASS1 ?CLASS2))
      (instance ?REL AsymmetricRelation))

if rel is an instance of antisymmetric relation,
then for all inst1,inst2 holds: if rel(inst1,inst2) holds and rel(inst2,inst1) holds, then inst1 is equal to inst2

(=>
      (instance ?REL AntisymmetricRelation)
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (holds ?REL ?INST1 ?INST2)
                        (holds ?REL ?INST2 ?INST1))
                  (equal ?INST1 ?INST2))))

If rel is an instance of trichotomizing relation, then for all inst1,inst2 holds: rel(inst1,inst2) holds or inst1 is equal to inst2 or rel(inst2,inst1) holds.

(=>
      (instance ?REL TrichotomizingRelation)
      (forall
            (?INST1 ?INST2)
            (or
                  (holds ?REL ?INST1 ?INST2)
                  (equal ?INST1 ?INST2)
                  (holds ?REL ?INST2 ?INST1))))

if rel is an instance of transitive relation,
then for all inst1,inst2,inst3 holds: if rel(inst1,inst2) holds and rel(inst2,inst3) holds, then rel(inst1,inst3) holds

(=>
      (instance ?REL TransitiveRelation)
      (forall
            (?INST1 ?INST2 ?INST3)
            (=>
                  (and
                        (holds ?REL ?INST1 ?INST2)
                        (holds ?REL ?INST2 ?INST3))
                  (holds ?REL ?INST1 ?INST3))))

if rel is an instance of intransitive relation,
then for all inst1,inst2,inst3 holds: if rel(inst1,inst2) holds and rel(inst2,inst3) holds, then rel(inst1,inst3) doesn't hold

(=>
      (instance ?REL IntransitiveRelation)
      (forall
            (?INST1 ?INST2 ?INST3)
            (=>
                  (and
                        (holds ?REL ?INST1 ?INST2)
                        (holds ?REL ?INST2 ?INST3))
                  (not
                        (holds ?REL ?INST1 ?INST3)))))

If rel is an instance of total ordering relation, then for all inst1,inst2 holds: rel(inst1,inst2) holds or rel(inst2,inst1) holds.

(=>
      (instance ?REL TotalOrderingRelation)
      (forall
            (?INST1 ?INST2)
            (or
                  (holds ?REL ?INST1 ?INST2)
                  (holds ?REL ?INST2 ?INST1))))

If process is an instance of process, then there exists cause so that process is an agent of cause.

(=>
      (instance ?PROCESS Process)
      (exists
            (?CAUSE)
            (agent ?PROCESS ?CAUSE)))

If formula1 increases likelihood of formula2 and "the probability of formula2" is equal to number1 and probability of formula1 provided that formula2 holds is formula2, then number2 is greater than number1.

(=>
      (and
            (increasesLikelihood ?FORMULA1 ?FORMULA2)
            (equal
                  (ProbabilityFn ?FORMULA2)
                  ?NUMBER1)
            (conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
      (greaterThan ?NUMBER2 ?NUMBER1))

If formula1 decreases likelihood of formula2 and "the probability of formula2" is equal to number1 and probability of formula1 provided that formula2 holds is formula2, then number2 is less than number1.

(=>
      (and
            (decreasesLikelihood ?FORMULA1 ?FORMULA2)
            (equal
                  (ProbabilityFn ?FORMULA2)
                  ?NUMBER1)
            (conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
      (lessThan ?NUMBER2 ?NUMBER1))

If probability of formula1 and formula2 is independent and "the probability of formula2" is equal to number1 and probability of formula1 provided that formula2 holds is formula2, then number2 is equal to number1.

(=>
      (and
            (independentProbability ?FORMULA1 ?FORMULA2)
            (equal
                  (ProbabilityFn ?FORMULA2)
                  ?NUMBER1)
            (conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
      (equal ?NUMBER2 ?NUMBER1))

If formula1 is an instance of formula and formula2 is an instance of formula, then formula1 increases likelihood of formula2 or formula1 decreases likelihood of formula2 or probability of formula1 and formula2 is independent.

(=>
      (and
            (instance ?FORMULA1 Formula)
            (instance ?FORMULA2 Formula))
      (or
            (increasesLikelihood ?FORMULA1 ?FORMULA2)
            (decreasesLikelihood ?FORMULA1 ?FORMULA2)
            (independentProbability ?FORMULA1 ?FORMULA2)))

If rel is an instance of intentional relation and rel(agent,) holds and obj is a member of "()", then agent is interested in obj.

(=>
      (and
            (instance ?REL IntentionalRelation)
            (holds ?REL ?AGENT @ROW)
            (inList
                  ?OBJ
                  (ListFn @ROW)))
      (inScopeOfInterest ?AGENT ?OBJ))

if agent prefers formula1 over formula2,
then if formula1 is true, then formula2 is false

(=>
      (prefers ?AGENT ?FORMULA1 ?FORMULA2)
      (=>
            (true ?FORMULA1 True)
            (true ?FORMULA2 False)))

If agent needs object, then agent wants object.

(=>
      (needs ?AGENT ?OBJECT)
      (wants ?AGENT ?OBJECT))

If agent wants obj, then there exists purp so that obj has &n purpose purp for agent.

(=>
      (wants ?AGENT ?OBJ)
      (exists
            (?PURP)
            (hasPurposeForAgent ?OBJ ?PURP ?AGENT)))

If agent wants obj, then agent desires "agent posesses obj".

(=>
      (wants ?AGENT ?OBJ)
      (desires
            ?AGENT
            (possesses ?AGENT ?OBJ)))

If agent believes formula, then there exists time so that agent considers formula during time.

(=>
      (believes ?AGENT ?FORMULA)
      (exists
            (?TIME)
            (holdsDuring
                  ?TIME
                  (considers ?AGENT ?FORMULA))))

If agent knows formula, then agent believes formula.

(=>
      (knows ?AGENT ?FORMULA)
      (believes ?AGENT ?FORMULA))

If agent knows formula, then formula is true.

(=>
      (knows ?AGENT ?FORMULA)
      (true ?FORMULA True))

If rel is an instance of ternary relation, then there don't exist item1,item2,item3,item4, so that rel(item1,item2,item3,item4,) holds.

(=>
      (instance ?REL TernaryRelation)
      (not
            (exists
                  (?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 @ROW)
                  (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 @ROW))))

If rel is an instance of quaternary relation, then there don't exist item1,item2,item3,item4,item5, so that rel(item1,item2,item3,item4,item5,) holds.

(=>
      (instance ?REL QuaternaryRelation)
      (not
            (exists
                  (?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 @ROW)
                  (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 @ROW))))

If rel is an instance of quintary relation, then there don't exist item1,item2,item3,item4,item5,item6, so that rel(item1,item2,item3,item4,item5,item6,) holds.

(=>
      (instance ?REL QuintaryRelation)
      (not
            (exists
                  (?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 ?ITEM6 @ROW)
                  (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 ?ITEM6 @ROW))))

if list is an instance of list,
then there exists number1 so that there exists item1 so that "number1th element of list" is not equal to item1 and for all number2 holds: if number2 is an instance of positive integer and number2 is less than number1, then there exists item2 so that "number2th element of list" is equal to item2

(=>
      (instance ?LIST List)
      (exists
            (?NUMBER1)
            (exists
                  (?ITEM1)
                  (and
                        (not
                              (equal
                                    (ListOrderFn ?LIST ?NUMBER1)
                                    ?ITEM1))
                        (forall
                              (?NUMBER2)
                              (=>
                                    (and
                                          (instance ?NUMBER2 PositiveInteger)
                                          (lessThan ?NUMBER2 ?NUMBER1))
                                    (exists
                                          (?ITEM2)
                                          (equal
                                                (ListOrderFn ?LIST ?NUMBER2)
                                                ?ITEM2))))))))

list is an instance of unique list if and only if for all number1,number2 holds: if "number1th element of list" is equal to "number2th element of list", then number1 is equal to number2.

(<=>
      (instance ?LIST UniqueList)
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (equal
                        (ListOrderFn ?LIST ?NUMBER1)
                        (ListOrderFn ?LIST ?NUMBER2))
                  (equal ?NUMBER1 ?NUMBER2))))

if class is covered by ,
then for all obj holds: if obj is an instance of class, then there exists item so that item is a member of "()" and obj is an instance of item

(=>
      (exhaustiveDecomposition ?CLASS @ROW)
      (forall
            (?OBJ)
            (=>
                  (instance ?OBJ ?CLASS)
                  (exists
                        (?ITEM)
                        (and
                              (inList
                                    ?ITEM
                                    (ListFn @ROW))
                              (instance ?OBJ ?ITEM))))))

if class is disjointly decomposed into ,
then for all item holds: if item is a member of "()", then item is a subclass of class

(=>
      (disjointDecomposition ?CLASS @ROW)
      (forall
            (?ITEM)
            (=>
                  (inList
                        ?ITEM
                        (ListFn @ROW))
                  (subclass ?ITEM ?CLASS))))

if class is disjointly decomposed into ,
then for all item1,item2 holds: if item1 is a member of "()" and item2 is a member of "()" and item1 is not equal to item2, then item1 is disjoint from item2

(=>
      (disjointDecomposition ?CLASS @ROW)
      (forall
            (?ITEM1 ?ITEM2)
            (=>
                  (and
                        (inList
                              ?ITEM1
                              (ListFn @ROW))
                        (inList
                              ?ITEM2
                              (ListFn @ROW))
                        (not
                              (equal ?ITEM1 ?ITEM2)))
                  (disjoint ?ITEM1 ?ITEM2))))

If list1 is an instance of list and list2 is an instance of list and for all number holds: "numberth element of list1" is equal to "numberth element of list2", then list1 is equal to list2.

(=>
      (and
            (instance ?LIST1 List)
            (instance ?LIST2 List)
            (forall
                  (?NUMBER)
                  (equal
                        (ListOrderFn ?LIST1 ?NUMBER)
                        (ListOrderFn ?LIST2 ?NUMBER))))
      (equal ?LIST1 ?LIST2))

If the number number argument of rel is an instance of class and rel() holds, then "numberth element of "()"" is an instance of class.

(=>
      (and
            (domain ?REL ?NUMBER ?CLASS)
            (holds ?REL @ROW))
      (instance
            (ListOrderFn
                  (ListFn @ROW)
                  ?NUMBER)
            ?CLASS))

If the number number argument of rel is a subclass of class and rel() holds, then "numberth element of "()"" is a subclass of class.

(=>
      (and
            (domainSubclass ?REL ?NUMBER ?CLASS)
            (holds ?REL @ROW))
      (subclass
            (ListOrderFn
                  (ListFn @ROW)
                  ?NUMBER)
            ?CLASS))

If "length of list" is equal to number1, then for all number2 holds: there exists item so that "number2th element of list" is equal to item if and only if number2 is less than or equal to number1.

(=>
      (equal
            (ListLengthFn ?LIST)
            ?NUMBER1)
      (forall
            (?NUMBER2)
            (<=>
                  (exists
                        (?ITEM)
                        (equal
                              (ListOrderFn ?LIST ?NUMBER2)
                              ?ITEM))
                  (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))

if rel %&has number argument(s),
then for all holds: if rel() holds, then "length of "()"" is equal to number

(=>
      (valence ?REL ?NUMBER)
      (forall
            (@ROW)
            (=>
                  (holds ?REL @ROW)
                  (equal
                        (ListLengthFn
                              (ListFn @ROW))
                        ?NUMBER))))

If "length of list1" is equal to number, then there exists list2 so that list1 starts list2 and "(number+1)" is equal to "length of list2" and ""(number+1)"th element of list2" is equal to item.

(=>
      (equal
            (ListLengthFn ?LIST1)
            ?NUMBER)
      (exists
            (?LIST2)
            (and
                  (initialList ?LIST1 ?LIST2)
                  (equal
                        (SuccessorFn ?NUMBER)
                        (ListLengthFn ?LIST2))
                  (equal
                        (ListOrderFn
                              ?LIST2
                              (SuccessorFn ?NUMBER))
                        ?ITEM))))

list3 is equal to "the list composed of list1 and list2" if and only if for all number1,number2 holds: if number1 is less than or equal to "length of list1" and number2 is less than or equal to "length of list2" and number1 is an instance of positive integer and number2 is an instance of positive integer, then "number1th element of list3" is equal to "number1th element of list1" and ""("length of list1"+number2)"th element of list3" is equal to "number2th element of list2".

(<=>
      (equal
            ?LIST3
            (ListConcatenateFn ?LIST1 ?LIST2))
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (and
                        (lessThanOrEqualTo
                              ?NUMBER1
                              (ListLengthFn ?LIST1))
                        (lessThanOrEqualTo
                              ?NUMBER2
                              (ListLengthFn ?LIST2))
                        (instance ?NUMBER1 PositiveInteger)
                        (instance ?NUMBER2 PositiveInteger))
                  (and
                        (equal
                              (ListOrderFn ?LIST3 ?NUMBER1)
                              (ListOrderFn ?LIST1 ?NUMBER1))
                        (equal
                              (ListOrderFn
                                    ?LIST3
                                    (AdditionFn
                                          (ListLengthFn ?LIST1)
                                          ?NUMBER2))
                              (ListOrderFn ?LIST2 ?NUMBER2))))))

if list1 is a sublist of list2,
then for all item holds: if item is a member of list1, then item is a member of list2

(=>
      (subList ?LIST1 ?LIST2)
      (forall
            (?ITEM)
            (=>
                  (inList ?ITEM ?LIST1)
                  (inList ?ITEM ?LIST2))))

if list1 is a sublist of list2,
then there exists number3 so that for all item holds: if item is a member of list1, then there exist number1,number2 so that "number1th element of list1" is equal to item and "number2th element of list2" is equal to item and number2 is equal to "(number1+number3)"

(=>
      (subList ?LIST1 ?LIST2)
      (exists
            (?NUMBER3)
            (forall
                  (?ITEM)
                  (=>
                        (inList ?ITEM ?LIST1)
                        (exists
                              (?NUMBER1 ?NUMBER2)
                              (and
                                    (equal
                                          (ListOrderFn ?LIST1 ?NUMBER1)
                                          ?ITEM)
                                    (equal
                                          (ListOrderFn ?LIST2 ?NUMBER2)
                                          ?ITEM)
                                    (equal
                                          ?NUMBER2
                                          (AdditionFn ?NUMBER1 ?NUMBER3))))))))

if list1 starts list2,
then for all number1,number2 holds: if "length of list1" is equal to number1 and number2 is less than or equal to number1, then "number2th element of list1" is equal to "number2th element of list2"

(=>
      (initialList ?LIST1 ?LIST2)
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (and
                        (equal
                              (ListLengthFn ?LIST1)
                              ?NUMBER1)
                        (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))
                  (equal
                        (ListOrderFn ?LIST1 ?NUMBER2)
                        (ListOrderFn ?LIST2 ?NUMBER2)))))

If function is an instance of unary function, then function %&has argument(s).

(=>
      (instance ?FUNCTION UnaryFunction)
      (valence ?FUNCTION 1))

if fun is an instance of one to one function,
then for all arg1,arg2 holds: if the number argument of fun is an instance of class and arg1 is an instance of class and arg2 is an instance of class and arg1 is not equal to arg2, then "fun(arg1)" is not equal to "fun(arg2)"

(=>
      (instance ?FUN OneToOneFunction)
      (forall
            (?ARG1 ?ARG2)
            (=>
                  (and
                        (domain ?FUN 1 ?CLASS)
                        (instance ?ARG1 ?CLASS)
                        (instance ?ARG2 ?CLASS)
                        (not
                              (equal ?ARG1 ?ARG2)))
                  (not
                        (equal
                              (AssignmentFn ?FUN ?ARG1)
                              (AssignmentFn ?FUN ?ARG2))))))

If seq is an instance of sequence function and range of seq is an instance of class, then class is a subclass of integer.

(=>
      (and
            (instance ?SEQ SequenceFunction)
            (range ?SEQ ?CLASS))
      (subclass ?CLASS Integer))

If function is an instance of binary function, then function %&has argument(s).

(=>
      (instance ?FUNCTION BinaryFunction)
      (valence ?FUNCTION 2))

if function is an instance of associative function,
then for all inst1,inst2,inst3 holds: if the number argument of function is an instance of class and inst1 is an instance of class and inst2 is an instance of class and inst3 is an instance of class, then "function(inst1,"function(inst2,inst3)")" is equal to "function("function(inst1,inst2)",inst3)"

(=>
      (instance ?FUNCTION AssociativeFunction)
      (forall
            (?INST1 ?INST2 ?INST3)
            (=>
                  (and
                        (domain ?FUNCTION 1 ?CLASS)
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?CLASS)
                        (instance ?INST3 ?CLASS))
                  (equal
                        (AssignmentFn
                              ?FUNCTION
                              ?INST1
                              (AssignmentFn ?FUNCTION ?INST2 ?INST3))
                        (AssignmentFn
                              ?FUNCTION
                              (AssignmentFn ?FUNCTION ?INST1 ?INST2)
                              ?INST3)))))

if function is an instance of commutative function,
then for all inst1,inst2 holds: if the number argument of function is an instance of class and inst1 is an instance of class and inst2 is an instance of class, then "function(inst1,inst2)" is equal to "function(inst2,inst1)"

(=>
      (instance ?FUNCTION CommutativeFunction)
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (domain ?FUNCTION 1 ?CLASS)
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?CLASS))
                  (equal
                        (AssignmentFn ?FUNCTION ?INST1 ?INST2)
                        (AssignmentFn ?FUNCTION ?INST2 ?INST1)))))

If function is an instance of ternary function, then function %&has argument(s).

(=>
      (instance ?FUNCTION TernaryFunction)
      (valence ?FUNCTION 3))

If function is an instance of quaternary function, then function %&has argument(s).

(=>
      (instance ?FUNCTION QuaternaryFunction)
      (valence ?FUNCTION 4))

If rel is an instance of binary predicate, then rel %&has argument(s).

(=>
      (instance ?REL BinaryPredicate)
      (valence ?REL 2))

If rel is an instance of ternary predicate, then rel %&has argument(s).

(=>
      (instance ?REL TernaryPredicate)
      (valence ?REL 3))

If rel is an instance of quaternary predicate, then rel %&has argument(s).

(=>
      (instance ?REL QuaternaryPredicate)
      (valence ?REL 4))

If rel is an instance of quintary predicate, then rel %&has argument(s).

(=>
      (instance ?REL QuintaryPredicate)
      (valence ?REL 5))

If rel is an instance of variable arity relation, then there doesn't exist int so that rel %&has int argument(s).

(=>
      (instance ?REL VariableArityRelation)
      (not
            (exists
                  (?INT)
                  (valence ?REL ?INT))))

if function is closed on class and function is an instance of unary function,
then for all inst holds: if inst is an instance of class, then "function(inst)" is an instance of class

(=>
      (and
            (closedOn ?FUNCTION ?CLASS)
            (instance ?FUNCTION UnaryFunction))
      (forall
            (?INST)
            (=>
                  (instance ?INST ?CLASS)
                  (instance
                        (AssignmentFn ?FUNCTION ?INST)
                        ?CLASS))))

if function is closed on class and function is an instance of binary function,
then for all inst1,inst2 holds: if inst1 is an instance of class and inst2 is an instance of class, then "function(inst1,inst2)" is an instance of class

(=>
      (and
            (closedOn ?FUNCTION ?CLASS)
            (instance ?FUNCTION BinaryFunction))
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?CLASS))
                  (instance
                        (AssignmentFn ?FUNCTION ?INST1 ?INST2)
                        ?CLASS))))

if relation is reflexive on class,
then for all inst holds: if inst is an instance of class, then relation(inst,inst) holds

(=>
      (reflexiveOn ?RELATION ?CLASS)
      (forall
            (?INST)
            (=>
                  (instance ?INST ?CLASS)
                  (holds ?RELATION ?INST ?INST))))

if relation is irreflexive on class,
then for all inst holds: if inst is an instance of class, then relation(inst,inst) doesn't hold

(=>
      (irreflexiveOn ?RELATION ?CLASS)
      (forall
            (?INST)
            (=>
                  (instance ?INST ?CLASS)
                  (not
                        (holds ?RELATION ?INST ?INST)))))

If relation is partial ordering on class, then relation is reflexive on class and relation is an instance of transitive relation and relation is an instance of antisymmetric relation.

(=>
      (partialOrderingOn ?RELATION ?CLASS)
      (and
            (reflexiveOn ?RELATION ?CLASS)
            (instance ?RELATION TransitiveRelation)
            (instance ?RELATION AntisymmetricRelation)))

if relation is trichotomizing on class,
then for all inst1,inst2 holds: if inst1 is an instance of class and inst2 is an instance of class, then relation(inst1,inst2) holds or relation(inst2,inst1) holds or inst1 is equal to inst2

(=>
      (trichotomizingOn ?RELATION ?CLASS)
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?CLASS))
                  (or
                        (holds ?RELATION ?INST1 ?INST2)
                        (holds ?RELATION ?INST2 ?INST1)
                        (equal ?INST1 ?INST2)))))

If relation is equivalence relation on class, then relation is an instance of transitive relation and relation is an instance of symmetric relation and relation is reflexive on class.

(=>
      (equivalenceRelationOn ?RELATION ?CLASS)
      (and
            (instance ?RELATION TransitiveRelation)
            (instance ?RELATION SymmetricRelation)
            (reflexiveOn ?RELATION ?CLASS)))

if function1 is distributive over function2,
then for all inst1,inst2,inst3 holds: if the number argument of function1 is an instance of class1 and inst1 is an instance of class1 and inst2 is an instance of class1 and inst3 is an instance of class1 and the number argument of function2 is an instance of class2 and inst1 is an instance of class2 and inst2 is an instance of class2 and inst3 is an instance of class2, then "function1(inst1,"function2(inst2,inst3)")" is equal to "function2("function1(inst1,inst2)","function1(inst1,inst3)")"

(=>
      (distributes ?FUNCTION1 ?FUNCTION2)
      (forall
            (?INST1 ?INST2 ?INST3)
            (=>
                  (and
                        (domain ?FUNCTION1 1 ?CLASS1)
                        (instance ?INST1 ?CLASS1)
                        (instance ?INST2 ?CLASS1)
                        (instance ?INST3 ?CLASS1)
                        (domain ?FUNCTION2 1 ?CLASS2)
                        (instance ?INST1 ?CLASS2)
                        (instance ?INST2 ?CLASS2)
                        (instance ?INST3 ?CLASS2))
                  (equal
                        (AssignmentFn
                              ?FUNCTION1
                              ?INST1
                              (AssignmentFn ?FUNCTION2 ?INST2 ?INST3))
                        (AssignmentFn
                              ?FUNCTION2
                              (AssignmentFn ?FUNCTION1 ?INST1 ?INST2)
                              (AssignmentFn ?FUNCTION1 ?INST1 ?INST3))))))

If proc1 is an instance of process, then there exists proc2 so that proc2 causes proc1.

(=>
      (instance ?PROC1 Process)
      (exists
            (?PROC2)
            (causes ?PROC2 ?PROC1)))

if causes subclass(proc1,proc2) holds,
then for all inst2 holds: if inst2 is an instance of proc2, then there exists proc1 inst1 so that inst1 causes inst2

(=>
      (causesSubclass ?PROC1 ?PROC2)
      (forall
            (?INST2)
            (=>
                  (instance ?INST2 ?PROC2)
                  (exists
                        (?INST1)
                        (and
                              (instance ?INST1 ?PROC1)
                              (causes ?INST1 ?INST2))))))

if obj1 is an exact copy of obj2,
then for all attr holds: if attr is an attribute of obj1, then attr is an attribute of obj2

(=>
      (copy ?OBJ1 ?OBJ2)
      (forall
            (?ATTR)
            (=>
                  (attribute ?OBJ1 ?ATTR)
                  (attribute ?OBJ2 ?ATTR))))

If situation1 holds during time and situation1 entails situation2, then situation2 holds during time.

(=>
      (and
            (holdsDuring ?TIME ?SITUATION1)
            (entails ?SITUATION1 ?SITUATION2))
      (holdsDuring ?TIME ?SITUATION2))

If situation during time, then situation holds during time.

(=>
      (holdsDuring
            ?TIME
            (not ?SITUATION))
      (not
            (holdsDuring ?TIME ?SITUATION)))

If role is an instance of case role and role(arg1,arg2) holds and arg1 is an instance of proc, then arg2 is capable to do proc in role role.

(=>
      (and
            (instance ?ROLE CaseRole)
            (holds ?ROLE ?ARG1 ?ARG2)
            (instance ?ARG1 ?PROC))
      (capability ?PROC ?ROLE ?ARG2))

If obj exploits agent, then there exists process so that process is an agent of agent and obj is a resource for process.

(=>
      (exploits ?OBJ ?AGENT)
      (exists
            (?PROCESS)
            (and
                  (agent ?PROCESS ?AGENT)
                  (resource ?PROCESS ?OBJ))))

If thing has purpose purpose, then there exists agent so that thing has &n purpose purpose for agent.

(=>
      (hasPurpose ?THING ?PURPOSE)
      (exists
            (?AGENT)
            (hasPurposeForAgent ?THING ?PURPOSE ?AGENT)))

If agent has &n skill to do proc, then agent is capable to do proc in role agent.

(=>
      (hasSkill ?PROC ?AGENT)
      (capability ?PROC agent ?AGENT))

If agent has the right to perform process, then agent is capable to do process in role agent.

(=>
      (holdsRight ?PROCESS ?AGENT)
      (capability ?PROCESS agent ?AGENT))

If agent1 allows agent2 to perform task of the type process, then agent2 has the right to perform process.

(=>
      (confersRight ?PROCESS ?AGENT1 ?AGENT2)
      (holdsRight ?PROCESS ?AGENT2))

If agent is obliged to perform tasks of type process, then agent is capable to do process in role agent.

(=>
      (holdsObligation ?PROCESS ?AGENT)
      (capability ?PROCESS agent ?AGENT))

If agent1 obligates agent2 to perform task of the type process, then agent2 is obliged to perform tasks of type process.

(=>
      (confersObligation ?PROCESS ?AGENT1 ?AGENT2)
      (holdsObligation ?PROCESS ?AGENT2))

if obj is located at region,
then for all subobj holds: if subobj is a part of obj, then subobj is located at region

(=>
      (located ?OBJ ?REGION)
      (forall
            (?SUBOBJ)
            (=>
                  (part ?SUBOBJ ?OBJ)
                  (located ?SUBOBJ ?REGION))))

If obj is partly located in region, then there exists subobj so that subobj is a part of obj and subobj is exactly located in region.

(=>
      (partlyLocated ?OBJ ?REGION)
      (exists
            (?SUBOBJ)
            (and
                  (part ?SUBOBJ ?OBJ)
                  (exactlyLocated ?SUBOBJ ?REGION))))

If obj is exactly located in region, then there doesn't exist otherobj so that otherobj is exactly located in region and otherobj is not equal to obj.

(=>
      (exactlyLocated ?OBJ ?REGION)
      (not
            (exists
                  (?OTHEROBJ)
                  (and
                        (exactlyLocated ?OTHEROBJ ?REGION)
                        (not
                              (equal ?OTHEROBJ ?OBJ))))))

If obj1 traverses obj2, then obj1 crosses obj2 or obj1 penetrates obj2.

(=>
      (traverses ?OBJ1 ?OBJ2)
      (or
            (crosses ?OBJ1 ?OBJ2)
            (penetrates ?OBJ1 ?OBJ2)))

if person posesses obj,
then there exists type so that type has the right to perform person and for all process holds: if process is an instance of type, then obj is a patient of process

(=>
      (possesses ?PERSON ?OBJ)
      (exists
            (?TYPE)
            (and
                  (holdsRight ?PERSON ?TYPE)
                  (forall
                        (?PROCESS)
                        (=>
                              (instance ?PROCESS ?TYPE)
                              (patient ?PROCESS ?OBJ))))))

If time is an instance of time position and agent1 posesses obj during time and agent2 posesses obj during time, then agent1 is equal to agent2.

(=>
      (and
            (instance ?TIME TimePosition)
            (holdsDuring
                  ?TIME
                  (possesses ?AGENT1 ?OBJ))
            (holdsDuring
                  ?TIME
                  (possesses ?AGENT2 ?OBJ)))
      (equal ?AGENT1 ?AGENT2))

if proc1 is a precondition of proc2,
then if there exists inst2 so that inst2 is an instance of proc2, then there exists inst1 so that inst1 is an instance of proc1

(=>
      (precondition ?PROC1 ?PROC2)
      (=>
            (exists
                  (?INST2)
                  (instance ?INST2 ?PROC2))
            (exists
                  (?INST1)
                  (instance ?INST1 ?PROC1))))

If proc1 inhibits proc2, then for all time,place holds: "there exists proc1 inst1 so that inst1 is located at place during time" decreases likelihood of "there exists proc2 inst2 so that inst2 is located at place during time".

(=>
      (inhibits ?PROC1 ?PROC2)
      (forall
            (?TIME ?PLACE)
            (decreasesLikelihood
                  (holdsDuring
                        ?TIME
                        (exists
                              (?INST1)
                              (and
                                    (instance ?INST1 ?PROC1)
                                    (located ?INST1 ?PLACE))))
                  (holdsDuring
                        ?TIME
                        (exists
                              (?INST2)
                              (and
                                    (instance ?INST2 ?PROC2)
                                    (located ?INST2 ?PLACE)))))))

if proc1 prevents the occurrence of proc2,
then for all time,place holds: if there exists proc1 inst1 so that inst1 is located at place during time, then there exists proc2 inst2 so that inst2 is located at place during time

(=>
      (prevents ?PROC1 ?PROC2)
      (forall
            (?TIME ?PLACE)
            (=>
                  (holdsDuring
                        ?TIME
                        (exists
                              (?INST1)
                              (and
                                    (instance ?INST1 ?PROC1)
                                    (located ?INST1 ?PLACE))))
                  (not
                        (holdsDuring
                              ?TIME
                              (exists
                                    (?INST2)
                                    (and
                                          (instance ?INST2 ?PROC2)
                                          (located ?INST2 ?PLACE))))))))

If agent uses rep to stand for entity, then rep expresses entity.

(=>
      (representsForAgent ?REP ?ENTITY ?AGENT)
      (represents ?REP ?ENTITY))

If rep represents entity in the language language, then there exists agent so that agent uses rep to stand for entity.

(=>
      (representsInLanguage ?REP ?ENTITY ?LANGUAGE)
      (exists
            (?AGENT)
            (representsForAgent ?REP ?ENTITY ?AGENT)))

class1 subsumes the content of class2 if and only if for all obj2,info holds: if obj2 is an instance of class2 and obj2 contains information info, then there exists class1 obj1 so that obj1 contains information info.

(<=>
      (subsumesContentClass ?CLASS1 ?CLASS2)
      (forall
            (?OBJ2 ?INFO)
            (=>
                  (and
                        (instance ?OBJ2 ?CLASS2)
                        (containsInformation ?OBJ2 ?INFO))
                  (exists
                        (?OBJ1)
                        (and
                              (instance ?OBJ1 ?CLASS1)
                              (containsInformation ?OBJ1 ?INFO))))))

obj1 subsumes the content of obj2 if and only if for all info holds: if obj2 contains information info, then obj1 contains information info.

(<=>
      (subsumesContentInstance ?OBJ1 ?OBJ2)
      (forall
            (?INFO)
            (=>
                  (containsInformation ?OBJ2 ?INFO)
                  (containsInformation ?OBJ1 ?INFO))))

If process expresses the content of prop, then there exists content bearing object obj so that obj contains information prop.

(=>
      (realization ?PROCESS ?PROP)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ ContentBearingObject)
                  (containsInformation ?OBJ ?PROP))))

if prop1 is a sub-proposition of prop2,
then for all obj1,obj2 holds: if obj1 contains information prop1 and obj2 contains information prop2, then obj2 subsumes the content of obj1

(=>
      (subProposition ?PROP1 ?PROP2)
      (forall
            (?OBJ1 ?OBJ2)
            (=>
                  (and
                        (containsInformation ?OBJ1 ?PROP1)
                        (containsInformation ?OBJ2 ?PROP2))
                  (subsumesContentInstance ?OBJ2 ?OBJ1))))

If agent uses obj, then there exists proc so that proc is an agent of agent and obj is an instrument for proc.

(=>
      (uses ?OBJ ?AGENT)
      (exists
            (?PROC)
            (and
                  (agent ?PROC ?AGENT)
                  (instrument ?PROC ?OBJ))))

If number is an instance of rational number, then there exist integer int1,integer int2 so that number is equal to "int1/int2".

(=>
      (instance ?NUMBER RationalNumber)
      (exists
            (?INT1 ?INT2)
            (and
                  (instance ?INT1 Integer)
                  (instance ?INT2 Integer)
                  (equal
                        ?NUMBER
                        (DivisionFn ?INT1 ?INT2)))))

If "the ceiling of number" is equal to int, then there doesn't exist integer otherint so that otherint is greater than or equal to number and otherint is less than int.

(=>
      (equal
            (CeilingFn ?NUMBER)
            ?INT)
      (not
            (exists
                  (?OTHERINT)
                  (and
                        (instance ?OTHERINT Integer)
                        (greaterThanOrEqualTo ?OTHERINT ?NUMBER)
                        (lessThan ?OTHERINT ?INT)))))

If "the largest integer less than or equal to number" is equal to int, then there doesn't exist integer otherint so that otherint is less than or equal to number and otherint is greater than int.

(=>
      (equal
            (FloorFn ?NUMBER)
            ?INT)
      (not
            (exists
                  (?OTHERINT)
                  (and
                        (instance ?OTHERINT Integer)
                        (lessThanOrEqualTo ?OTHERINT ?NUMBER)
                        (greaterThan ?OTHERINT ?INT)))))

if "the greatest common divisor of " is equal to number,
then for all element holds: if element is a member of "()", then "element mod number" is equal to

(=>
      (equal
            (GreatestCommonDivisorFn @ROW)
            ?NUMBER)
      (forall
            (?ELEMENT)
            (=>
                  (inList
                        ?ELEMENT
                        (ListFn @ROW))
                  (equal
                        (RemainderFn ?ELEMENT ?NUMBER)
                        0))))

if "the greatest common divisor of " is equal to number,
then there doesn't exist greater so that greater is greater than number and for all element holds: if element is a member of "()", then "element mod greater" is equal to

(=>
      (equal
            (GreatestCommonDivisorFn @ROW)
            ?NUMBER)
      (not
            (exists
                  (?GREATER)
                  (and
                        (greaterThan ?GREATER ?NUMBER)
                        (forall
                              (?ELEMENT)
                              (=>
                                    (inList
                                          ?ELEMENT
                                          (ListFn @ROW))
                                    (equal
                                          (RemainderFn ?ELEMENT ?GREATER)
                                          0)))))))

If number is an instance of complex number, then there exist part1,part2 so that part1 is equal to "the real part of number" and part2 is equal to "the imaginary part of number".

(=>
      (instance ?NUMBER ComplexNumber)
      (exists
            (?PART1 ?PART2)
            (and
                  (equal
                        ?PART1
                        (RealNumberFn ?NUMBER))
                  (equal
                        ?PART2
                        (ImaginaryPartFn ?NUMBER)))))

if "the least common multiple of " is equal to number,
then for all element holds: if element is a member of "()", then "number mod element" is equal to

(=>
      (equal
            (LeastCommonMultipleFn @ROW)
            ?NUMBER)
      (forall
            (?ELEMENT)
            (=>
                  (inList
                        ?ELEMENT
                        (ListFn @ROW))
                  (equal
                        (RemainderFn ?NUMBER ?ELEMENT)
                        0))))

if "the least common multiple of " is equal to number,
then there doesn't exist less so that less is less than number and for all element holds: if element is a member of "()", then "less mod element" is equal to

(=>
      (equal
            (LeastCommonMultipleFn @ROW)
            ?NUMBER)
      (not
            (exists
                  (?LESS)
                  (and
                        (lessThan ?LESS ?NUMBER)
                        (forall
                              (?ELEMENT)
                              (=>
                                    (inList
                                          ?ELEMENT
                                          (ListFn @ROW))
                                    (equal
                                          (RemainderFn ?LESS ?ELEMENT)
                                          0)))))))

If "the larger of number1 and number2" is equal to number, then

number is equal to number1 and number1 is greater than number2
number is equal to number2 and number2 is greater than number1
number is equal to number1 and number is equal to number2

(=>
      (equal
            (MaxFn ?NUMBER1 ?NUMBER2)
            ?NUMBER)
      (or
            (and
                  (equal ?NUMBER ?NUMBER1)
                  (greaterThan ?NUMBER1 ?NUMBER2))
            (and
                  (equal ?NUMBER ?NUMBER2)
                  (greaterThan ?NUMBER2 ?NUMBER1))
            (and
                  (equal ?NUMBER ?NUMBER1)
                  (equal ?NUMBER ?NUMBER2))))

If "the smaller of number1 and number2" is equal to number, then

number is equal to number1 and number1 is less than number2
number is equal to number2 and number2 is less than number1
number is equal to number1 and number is equal to number2

(=>
      (equal
            (MinFn ?NUMBER1 ?NUMBER2)
            ?NUMBER)
      (or
            (and
                  (equal ?NUMBER ?NUMBER1)
                  (lessThan ?NUMBER1 ?NUMBER2))
            (and
                  (equal ?NUMBER ?NUMBER2)
                  (lessThan ?NUMBER2 ?NUMBER1))
            (and
                  (equal ?NUMBER ?NUMBER1)
                  (equal ?NUMBER ?NUMBER2))))

If number is an instance of quantity, then "the reciprocal of number" is equal to "number raised to the power ".

(=>
      (instance ?NUMBER Quantity)
      (equal
            (ReciprocalFn ?NUMBER)
            (ExponentiationFn ?NUMBER -1)))

If number is an instance of quantity, then is equal to "number*"the reciprocal of number"".

(=>
      (instance ?NUMBER Quantity)
      (equal
            1
            (MultiplicationFn
                  ?NUMBER
                  (ReciprocalFn ?NUMBER))))

If "number1 mod number2" is equal to number, then "the sign of number2" is equal to "the sign of number".

(=>
      (equal
            (RemainderFn ?NUMBER1 ?NUMBER2)
            ?NUMBER)
      (equal
            (SignumFn ?NUMBER2)
            (SignumFn ?NUMBER)))

If number is an instance of even integer, then "number mod " is equal to .

(=>
      (instance ?NUMBER EvenInteger)
      (equal
            (RemainderFn ?NUMBER 2)
            0))

If number is an instance of odd integer, then "number mod " is equal to .

(=>
      (instance ?NUMBER OddInteger)
      (equal
            (RemainderFn ?NUMBER 2)
            1))

if prime is an instance of prime number,
then for all number holds: if "prime mod number" is equal to , then number is equal to or number is equal to prime

(=>
      (instance ?PRIME PrimeNumber)
      (forall
            (?NUMBER)
            (=>
                  (equal
                        (RemainderFn ?PRIME ?NUMBER)
                        0)
                  (or
                        (equal ?NUMBER 1)
                        (equal ?NUMBER ?PRIME)))))

if "number1 rounded" is equal to number2,
then
- if "(number1-"the largest integer less than or equal to number1")" is less than , then number2 is equal to "the largest integer less than or equal to number1"
- if "(number1-"the largest integer less than or equal to number1")" is greater than or equal to , then number2 is equal to "the ceiling of number1"

(=>
      (equal
            (RoundFn ?NUMBER1)
            ?NUMBER2)
      (or
            (=>
                  (lessThan
                        (SubtractionFn
                              ?NUMBER1
                              (FloorFn ?NUMBER1))
                        0.5)
                  (equal
                        ?NUMBER2
                        (FloorFn ?NUMBER1)))
            (=>
                  (greaterThanOrEqualTo
                        (SubtractionFn
                              ?NUMBER1
                              (FloorFn ?NUMBER1))
                        0.5)
                  (equal
                        ?NUMBER2
                        (CeilingFn ?NUMBER1)))))

If number is an instance of nonnegative real number, then "the sign of number" is equal to or "the sign of number" is equal to .

(=>
      (instance ?NUMBER NonnegativeRealNumber)
      (or
            (equal
                  (SignumFn ?NUMBER)
                  1)
            (equal
                  (SignumFn ?NUMBER)
                  0)))

If number is an instance of positive real number, then "the sign of number" is equal to .

(=>
      (instance ?NUMBER PositiveRealNumber)
      (equal
            (SignumFn ?NUMBER)
            1))

If number is an instance of negative real number, then "the sign of number" is equal to .

(=>
      (instance ?NUMBER NegativeRealNumber)
      (equal
            (SignumFn ?NUMBER)
            -1))

If "the square root of number1" is equal to number2, then "number2*number2" is equal to number1.

(=>
      (equal
            (SquareRootFn ?NUMBER1)
            ?NUMBER2)
      (equal
            (MultiplicationFn ?NUMBER2 ?NUMBER2)
            ?NUMBER1))

If degree is an instance of plane angle measure, then "the tangent of degree" is equal to ""the sine of degree"/"the cosine of degree"".

(=>
      (instance ?DEGREE PlaneAngleMeasure)
      (equal
            (TangentFn ?DEGREE)
            (DivisionFn
                  (SineFn ?DEGREE)
                  (CosineFn ?DEGREE))))

if id is an identity element of function,
then for all inst holds: if the number argument of function is an instance of class and inst is an instance of class, then "function(id,inst)" is equal to inst

(=>
      (identityElement ?FUNCTION ?ID)
      (forall
            (?INST)
            (=>
                  (and
                        (domain ?FUNCTION 1 ?CLASS)
                        (instance ?INST ?CLASS))
                  (equal
                        (AssignmentFn ?FUNCTION ?ID ?INST)
                        ?INST))))

If "(int1+1)" is equal to "(int2+1)", then int1 is equal to int2.

(=>
      (equal
            (SuccessorFn ?INT1)
            (SuccessorFn ?INT2))
      (equal ?INT1 ?INT2))

If int is an instance of integer, then int is less than "(int+1)".

(=>
      (instance ?INT Integer)
      (lessThan
            ?INT
            (SuccessorFn ?INT)))

If int1 is an instance of integer and int2 is an instance of integer, then int1 is not less than int2 or int2 is not less than "(int1+1)".

(=>
      (and
            (instance ?INT1 Integer)
            (instance ?INT2 Integer))
      (not
            (and
                  (lessThan ?INT1 ?INT2)
                  (lessThan
                        ?INT2
                        (SuccessorFn ?INT1)))))

If int is an instance of integer, then int is equal to "("(int+2)"+1)".

(=>
      (instance ?INT Integer)
      (equal
            ?INT
            (SuccessorFn
                  (PredecessorFn ?INT))))

If int is an instance of integer, then int is equal to "("(int+1)"+2)".

(=>
      (instance ?INT Integer)
      (equal
            ?INT
            (PredecessorFn
                  (SuccessorFn ?INT))))

If "(int1+2)" is equal to "(int2+2)", then int1 is equal to int2.

(=>
      (equal
            (PredecessorFn ?INT1)
            (PredecessorFn ?INT2))
      (equal ?INT1 ?INT2))

If int is an instance of integer, then int is greater than "(int+2)".

(=>
      (instance ?INT Integer)
      (greaterThan
            ?INT
            (PredecessorFn ?INT)))

If int1 is an instance of integer and int2 is an instance of integer, then int2 is not less than int1 or "(int1+2)" is not less than int2.

(=>
      (and
            (instance ?INT1 Integer)
            (instance ?INT2 Integer))
      (not
            (and
                  (lessThan ?INT2 ?INT1)
                  (lessThan
                        (PredecessorFn ?INT1)
                        ?INT2))))

if subset is a subset of set,
then for all element holds: if element is an element of subset, then element is an element of set

(=>
      (subset ?SUBSET ?SET)
      (forall
            (?ELEMENT)
            (=>
                  (element ?ELEMENT ?SUBSET)
                  (element ?ELEMENT ?SET))))

If for all element holds: element is an element of set1 if and only if element is an element of set2, then set1 is equal to set2.

(=>
      (forall
            (?ELEMENT)
            (<=>
                  (element ?ELEMENT ?SET1)
                  (element ?ELEMENT ?SET2)))
      (equal ?SET1 ?SET2))

If set is an instance of finite set, then there exists nonnegative integer number so that number is equal to "the number of instances in set".

(=>
      (instance ?SET FiniteSet)
      (exists
            (?NUMBER)
            (and
                  (instance ?NUMBER NonnegativeInteger)
                  (equal
                        ?NUMBER
                        (CardinalityFn ?SET)))))

if superclass is an instance of pairwise disjoint class,
then for all class1,class2 holds: if class1 is an instance of superclass and class2 is an instance of superclass, then class1 is equal to class2 or class1 is disjoint from class2

(=>
      (instance ?SUPERCLASS PairwiseDisjointClass)
      (forall
            (?CLASS1 ?CLASS2)
            (=>
                  (and
                        (instance ?CLASS1 ?SUPERCLASS)
                        (instance ?CLASS2 ?SUPERCLASS))
                  (or
                        (equal ?CLASS1 ?CLASS2)
                        (disjoint ?CLASS1 ?CLASS2)))))

if class is an instance of mutually disjoint class,
then for all inst1,inst2 holds: if inst1 is an instance of class and inst2 is an instance of inst1, then there exists class inst3 so that inst2 is not an instance of inst3

(=>
      (instance ?CLASS MutuallyDisjointClass)
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?INST1))
                  (exists
                        (?INST3)
                        (and
                              (instance ?INST3 ?CLASS)
                              (not
                                    (instance ?INST2 ?INST3)))))))

If graph is an instance of graph and node1 is an instance of graph node and node2 is an instance of graph node and node1 is a part of graph and node2 is a part of graph and node1 is not equal to node2, then there exist arc,path so that

arc links node1 and node2
- path is a subgraph of graph
- path is an instance of graph path
- - "the beginning of path" is equal to node1 and "the end of path" is equal to node2
  - "the beginning of path" is equal to node2 and "the end of path" is equal to node1

(=>
      (and
            (instance ?GRAPH Graph)
            (instance ?NODE1 GraphNode)
            (instance ?NODE2 GraphNode)
            (graphPart ?NODE1 ?GRAPH)
            (graphPart ?NODE2 ?GRAPH)
            (not
                  (equal ?NODE1 ?NODE2)))
      (exists
            (?ARC ?PATH)
            (or
                  (links ?NODE1 ?NODE2 ?ARC)
                  (and
                        (subGraph ?PATH ?GRAPH)
                        (instance ?PATH GraphPath)
                        (or
                              (and
                                    (equal
                                          (BeginNodeFn ?PATH)
                                          ?NODE1)
                                    (equal
                                          (EndNodeFn ?PATH)
                                          ?NODE2))
                              (and
                                    (equal
                                          (BeginNodeFn ?PATH)
                                          ?NODE2)
                                    (equal
                                          (EndNodeFn ?PATH)
                                          ?NODE1)))))))

If graph is an instance of graph, then there exist node1,node2,node3,arc1,arc2 so that node1 is a part of graph and node2 is a part of graph and node3 is a part of graph and arc1 is a part of graph and arc2 is a part of graph and node2 links arc1 and node1 and node3 links arc2 and node2 and node1 is not equal to node2 and node2 is not equal to node3 and node1 is not equal to node3 and arc1 is not equal to arc2.

(=>
      (instance ?GRAPH Graph)
      (exists
            (?NODE1 ?NODE2 ?NODE3 ?ARC1 ?ARC2)
            (and
                  (graphPart ?NODE1 ?GRAPH)
                  (graphPart ?NODE2 ?GRAPH)
                  (graphPart ?NODE3 ?GRAPH)
                  (graphPart ?ARC1 ?GRAPH)
                  (graphPart ?ARC2 ?GRAPH)
                  (links ?ARC1 ?NODE1 ?NODE2)
                  (links ?ARC2 ?NODE2 ?NODE3)
                  (not
                        (equal ?NODE1 ?NODE2))
                  (not
                        (equal ?NODE2 ?NODE3))
                  (not
                        (equal ?NODE1 ?NODE3))
                  (not
                        (equal ?ARC1 ?ARC2)))))

If graph is an instance of directed graph and arc is an instance of graph arc and arc is a part of graph, then there exist node1,node2 so that "the starting node of arc" is equal to node1 and "the terminal node of arc" is equal to node2.

(=>
      (and
            (instance ?GRAPH DirectedGraph)
            (instance ?ARC GraphArc)
            (graphPart ?ARC ?GRAPH))
      (exists
            (?NODE1 ?NODE2)
            (and
                  (equal
                        (InitialNodeFn ?ARC)
                        ?NODE1)
                  (equal
                        (TerminalNodeFn ?ARC)
                        ?NODE2))))

If graph is an instance of tree, then there doesn't exist graph loop loop so that loop is a part of graph.

(=>
      (instance ?GRAPH Tree)
      (not
            (exists
                  (?LOOP)
                  (and
                        (instance ?LOOP GraphLoop)
                        (graphPart ?LOOP ?GRAPH)))))

if graph is an instance of graph path and arc is an instance of graph arc and arc is a part of graph,
then if "the starting node of arc" is equal to node, then there doesn't exist other so that "the starting node of other" is equal to node and other is not equal to arc

(=>
      (and
            (instance ?GRAPH GraphPath)
            (instance ?ARC GraphArc)
            (graphPart ?ARC ?GRAPH))
      (=>
            (equal
                  (InitialNodeFn ?ARC)
                  ?NODE)
            (not
                  (exists
                        (?OTHER)
                        (and
                              (equal
                                    (InitialNodeFn ?OTHER)
                                    ?NODE)
                              (not
                                    (equal ?OTHER ?ARC)))))))

if graph is an instance of graph path and arc is an instance of graph arc and arc is a part of graph,
then if "the terminal node of arc" is equal to node, then there doesn't exist other so that "the terminal node of other" is equal to node and other is not equal to arc

(=>
      (and
            (instance ?GRAPH GraphPath)
            (instance ?ARC GraphArc)
            (graphPart ?ARC ?GRAPH))
      (=>
            (equal
                  (TerminalNodeFn ?ARC)
                  ?NODE)
            (not
                  (exists
                        (?OTHER)
                        (and
                              (equal
                                    (TerminalNodeFn ?OTHER)
                                    ?NODE)
                              (not
                                    (equal ?OTHER ?ARC)))))))

If part is an instance of graph element, then there exists graph graph so that part is a part of graph.

(=>
      (instance ?PART GraphElement)
      (exists
            (?GRAPH)
            (and
                  (instance ?GRAPH Graph)
                  (graphPart ?PART ?GRAPH))))

If node is an instance of graph node, then there exist other,arc so that arc links node and other.

(=>
      (instance ?NODE GraphNode)
      (exists
            (?OTHER ?ARC)
            (links ?NODE ?OTHER ?ARC)))

If arc is an instance of graph arc, then there exist node1,node2 so that arc links node1 and node2.

(=>
      (instance ?ARC GraphArc)
      (exists
            (?NODE1 ?NODE2)
            (links ?NODE1 ?NODE2 ?ARC)))

If "the starting node of arc" is equal to node and "the terminal node of arc" is equal to node, then arc is an instance of graph loop.

(=>
      (and
            (equal
                  (InitialNodeFn ?ARC)
                  ?NODE)
            (equal
                  (TerminalNodeFn ?ARC)
                  ?NODE))
      (instance ?ARC GraphLoop))

If arc links node1 and node2, then arc links node2 and node1.

(=>
      (links ?NODE1 ?NODE2 ?ARC)
      (links ?NODE2 ?NODE1 ?ARC))

If graph1 is a subgraph of graph2 and element is a part of graph1, then element is a part of graph2.

(=>
      (and
            (subGraph ?GRAPH1 ?GRAPH2)
            (graphPart ?ELEMENT ?GRAPH1))
      (graphPart ?ELEMENT ?GRAPH2))

if
- "the value of path" is equal to sum
- subpath is a subgraph of path
- arc1 is a part of path
- the value of arc1 is number1
- for all arc2 holds: if arc2 is a part of path, then arc2 is a part of subpath or arc2 is equal to arc1
,
then sum is equal to "("the value of subpath"+number1)"

(=>
      (and
            (equal
                  (PathWeightFn ?PATH)
                  ?SUM)
            (subGraph ?SUBPATH ?PATH)
            (graphPart ?ARC1 ?PATH)
            (arcWeight ?ARC1 ?NUMBER1)
            (forall
                  (?ARC2)
                  (=>
                        (graphPart ?ARC2 ?PATH)
                        (or
                              (graphPart ?ARC2 ?SUBPATH)
                              (equal ?ARC2 ?ARC1)))))
      (equal
            ?SUM
            (AdditionFn
                  (PathWeightFn ?SUBPATH)
                  ?NUMBER1)))

if
- "the value of path" is equal to sum
- arc1 is a part of path
- arc2 is a part of path
- the value of arc1 is number1
- the value of arc2 is number2
- for all arc3 holds: if arc3 is a part of path, then arc3 is equal to arc1 or arc3 is equal to arc2
,
then "the value of path" is equal to "(number1+number2)"

(=>
      (and
            (equal
                  (PathWeightFn ?PATH)
                  ?SUM)
            (graphPart ?ARC1 ?PATH)
            (graphPart ?ARC2 ?PATH)
            (arcWeight ?ARC1 ?NUMBER1)
            (arcWeight ?ARC2 ?NUMBER2)
            (forall
                  (?ARC3)
                  (=>
                        (graphPart ?ARC3 ?PATH)
                        (or
                              (equal ?ARC3 ?ARC1)
                              (equal ?ARC3 ?ARC2)))))
      (equal
            (PathWeightFn ?PATH)
            (AdditionFn ?NUMBER1 ?NUMBER2)))

If "the lowest cost path between node1 and node2" is equal to path, then path is an instance of "the set of paths between node1 and node2".

(=>
      (equal
            (MinimalWeightedPathFn ?NODE1 ?NODE2)
            ?PATH)
      (instance
            ?PATH
            (GraphPathFn ?NODE1 ?NODE2)))

if "the lowest cost path between node1 and node2" is equal to path and "the value of path" is equal to number,
then for all path2 holds: if path2 is an instance of "the set of paths between node1 and node2" and "the value of path2" is equal to number2, then number2 is greater than or equal to number1

(=>
      (and
            (equal
                  (MinimalWeightedPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (PathWeightFn ?PATH)
                  ?NUMBER))
      (forall
            (?PATH2)
            (=>
                  (and
                        (instance
                              ?PATH2
                              (GraphPathFn ?NODE1 ?NODE2))
                        (equal
                              (PathWeightFn ?PATH2)
                              ?NUMBER2))
                  (greaterThanOrEqualTo ?NUMBER2 ?NUMBER1))))

If "the highest cost path between node1 and node2" is equal to path, then path is an instance of "the set of paths between node1 and node2".

(=>
      (equal
            (MaximalWeightedPathFn ?NODE1 ?NODE2)
            ?PATH)
      (instance
            ?PATH
            (GraphPathFn ?NODE1 ?NODE2)))

if "the highest cost path between node1 and node2" is equal to path and "the value of path" is equal to number,
then for all path2 holds: if path2 is an instance of "the set of paths between node1 and node2" and "the value of path2" is equal to number2, then number2 is less than or equal to number1

(=>
      (and
            (equal
                  (MaximalWeightedPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (PathWeightFn ?PATH)
                  ?NUMBER))
      (forall
            (?PATH2)
            (=>
                  (and
                        (instance
                              ?PATH2
                              (GraphPathFn ?NODE1 ?NODE2))
                        (equal
                              (PathWeightFn ?PATH2)
                              ?NUMBER2))
                  (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))

If path is a part of graph and graph is not an instance of directed graph, then "the set of paths between node1 and node2" is equal to path if and only if "the set of paths between node2 and node1" is equal to path.

(=>
      (and
            (graphPart ?PATH ?GRAPH)
            (not
                  (instance ?GRAPH DirectedGraph)))
      (<=>
            (equal
                  (GraphPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (GraphPathFn ?NODE2 ?NODE1)
                  ?PATH)))

If graph is an instance of graph, then "the set of minimal paths that partition graph into two separate graphs" is a subclass of "the set of paths that partition graph into two separate graphs".

(=>
      (instance ?GRAPH Graph)
      (subclass
            (MinimalCutSetFn ?GRAPH)
            (CutSetFn ?GRAPH)))

if "the set of minimal paths that partition graph into two separate graphs" is equal to pathclass,
then there exists number so that for all path holds: if path is an instance of pathclass, then the length of path is number

(=>
      (equal
            (MinimalCutSetFn ?GRAPH)
            ?PATHCLASS)
      (exists
            (?NUMBER)
            (forall
                  (?PATH)
                  (=>
                        (instance ?PATH ?PATHCLASS)
                        (pathLength ?PATH ?NUMBER)))))

If "number unit(s)" is equal to quant and unit is a subclass of quanttype, then quant is an instance of quanttype.

(=>
      (and
            (equal
                  (MeasureFn ?NUMBER ?UNIT)
                  ?QUANT)
            (subclass ?UNIT ?QUANTTYPE))
      (instance ?QUANT ?QUANTTYPE))

if rel is an instance of relation extended to quantities and rel is an instance of ternary relation and number1 is an instance of real number and number2 is an instance of real number and rel(number1,number2,value) holds,
then for all unit holds: if unit is an instance of unit of measure, then rel("number1 unit(s)","number2 unit(s)","value unit(s)") holds

(=>
      (and
            (instance ?REL RelationExtendedToQuantities)
            (instance ?REL TernaryRelation)
            (instance ?NUMBER1 RealNumber)
            (instance ?NUMBER2 RealNumber)
            (holds ?REL ?NUMBER1 ?NUMBER2 ?VALUE))
      (forall
            (?UNIT)
            (=>
                  (instance ?UNIT UnitOfMeasure)
                  (holds
                        ?REL
                        (MeasureFn ?NUMBER1 ?UNIT)
                        (MeasureFn ?NUMBER2 ?UNIT)
                        (MeasureFn ?VALUE ?UNIT)))))

if rel is an instance of relation extended to quantities and rel is an instance of binary relation and number1 is an instance of real number and number2 is an instance of real number and rel(number1,number2) holds,
then for all unit holds: if unit is an instance of unit of measure, then rel("number1 unit(s)","number2 unit(s)") holds

(=>
      (and
            (instance ?REL RelationExtendedToQuantities)
            (instance ?REL BinaryRelation)
            (instance ?NUMBER1 RealNumber)
            (instance ?NUMBER2 RealNumber)
            (holds ?REL ?NUMBER1 ?NUMBER2))
      (forall
            (?UNIT)
            (=>
                  (instance ?UNIT UnitOfMeasure)
                  (holds
                        ?REL
                        (MeasureFn ?NUMBER1 ?UNIT)
                        (MeasureFn ?NUMBER2 ?UNIT)))))

If unit is an instance of unit of measure, then "1 thousand units" is equal to " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (KiloFn ?UNIT)
            (MeasureFn 1000 ?UNIT)))

If unit is an instance of unit of measure, then "1 million units" is equal to " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MegaFn ?UNIT)
            (MeasureFn 1000000 ?UNIT)))

If unit is an instance of unit of measure, then "1 billion units " is equal to " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (GigaFn ?UNIT)
            (MeasureFn 1000000000 ?UNIT)))

If unit is an instance of unit of measure, then "1 trillion units" is equal to " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (TeraFn ?UNIT)
            (MeasureFn 1000000000000 ?UNIT)))

If unit is an instance of unit of measure, then "one thousandth of a unit" is equal to " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MilliFn ?UNIT)
            (MeasureFn 0.001 ?UNIT)))

If unit is an instance of unit of measure, then "one millionth of a unit" is equal to " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MicroFn ?UNIT)
            (MeasureFn 0.000001 ?UNIT)))

If unit is an instance of unit of measure, then "one billionth of a unit" is equal to " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (NanoFn ?UNIT)
            (MeasureFn 0.000000001 ?UNIT)))

If unit is an instance of unit of measure, then "one trillionth of a unit" is equal to " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (PicoFn ?UNIT)
            (MeasureFn 0.000000000001 ?UNIT)))

If number is an instance of real number and unit is an instance of unit of measure, then "the magnitude of "number unit(s)"" is equal to number.

(=>
      (and
            (instance ?NUMBER RealNumber)
            (instance ?UNIT UnitOfMeasure))
      (equal
            (MagnitudeFn
                  (MeasureFn ?NUMBER ?UNIT))
            ?NUMBER))

If the measure of object is "distance per time in ref in the direction direction", then the measure of object is "distance per time".

(=>
      (measure
            ?OBJECT
            (VelocityFn ?DISTANCE ?TIME ?REF ?DIRECTION))
      (measure
            ?OBJECT
            (SpeedFn ?DISTANCE ?TIME)))

If number is an instance of real number, then "number centimeter(s)" is equal to ""number*" meter(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Centimeter)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  Meter)))

If number is an instance of real number, then "number celsius degree(s)" is equal to ""(number-)" kelvin degree(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER CelsiusDegree)
            (MeasureFn
                  (SubtractionFn ?NUMBER 273.15)
                  KelvinDegree)))

If number is an instance of real number, then "number celsius degree(s)" is equal to """(number-)"/" fahrenheit degree(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER CelsiusDegree)
            (MeasureFn
                  (DivisionFn
                        (SubtractionFn ?NUMBER 32)
                        1.8)
                  FahrenheitDegree)))

If number is an instance of real number, then "number day duration(s)" is equal to ""number*" hour duration(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER DayDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 24)
                  HourDuration)))

If number is an instance of real number, then "number hour duration(s)" is equal to ""number*" minute duration(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER HourDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 60)
                  MinuteDuration)))

If number is an instance of real number, then "number minute duration(s)" is equal to ""number*" second duration(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER MinuteDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 60)
                  SecondDuration)))

If number is an instance of real number, then "number week duration(s)" is equal to ""number*" day duration(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER WeekDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 7)
                  DayDuration)))

If number is an instance of real number, then "number year duration(s)" is equal to ""number*" day duration(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER YearDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 365)
                  DayDuration)))

If number is an instance of real number, then "number amu(s)" is equal to ""number**" gram(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Amu)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.6605402 E-24)
                  Gram)))

If number is an instance of real number, then "number electron volt(s)" is equal to ""number**" joule(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER ElectronVolt)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.60217733 E-19)
                  Joule)))

If number is an instance of real number, then "number angstrom(s)" is equal to ""number**" meter(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Angstrom)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.0 E-10)
                  Meter)))

If number is an instance of real number, then "number foot(s)" is equal to ""number*" meter(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Foot)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.3048)
                  Meter)))

If number is an instance of real number, then "number inch(s)" is equal to ""number*" meter(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Inch)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.0254)
                  Meter)))

If number is an instance of real number, then "number mile(s)" is equal to ""number*" meter(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Mile)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1609.344)
                  Meter)))

If number is an instance of real number, then "number united states gallon(s)" is equal to ""number*" liter(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedStatesGallon)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 3.785411784)
                  Liter)))

If number is an instance of real number, then "number quart(s)" is equal to ""number/" united states gallon(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Quart)
            (MeasureFn
                  (DivisionFn ?NUMBER 4)
                  UnitedStatesGallon)))

If number is an instance of real number, then "number pint(s)" is equal to ""number/" quart(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Pint)
            (MeasureFn
                  (DivisionFn ?NUMBER 2)
                  Quart)))

If number is an instance of real number, then "number cup(s)" is equal to ""number/" pint(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Cup)
            (MeasureFn
                  (DivisionFn ?NUMBER 2)
                  Pint)))

If number is an instance of real number, then "number ounce(s)" is equal to ""number/" cup(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Ounce)
            (MeasureFn
                  (DivisionFn ?NUMBER 8)
                  Cup)))

If number is an instance of real number, then "number united kingdom gallon(s)" is equal to ""number*" liter(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedKingdomGallon)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.54609)
                  Liter)))

If number is an instance of real number, then "number pound mass(s)" is equal to ""number*" gram(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER PoundMass)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 453.59237)
                  Gram)))

If number is an instance of real number, then "number slug(s)" is equal to ""number*" gram(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Slug)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 14593.90)
                  Gram)))

If number is an instance of real number, then "number rankine degree(s)" is equal to ""number*" kelvin degree(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER RankineDegree)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.8)
                  KelvinDegree)))

If number is an instance of real number, then "number pound force(s)" is equal to ""number*" newton(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER PoundForce)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.448222)
                  Newton)))

If number is an instance of real number, then "number calorie(s)" is equal to ""number*" joule(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Calorie)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.1868)
                  Joule)))

If number is an instance of real number, then "number british thermal unit(s)" is equal to ""number*" joule(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER BritishThermalUnit)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1055.05585262)
                  Joule)))

If number is an instance of real number, then "number angular degree(s)" is equal to ""number*"pi/"" radian(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER AngularDegree)
            (MeasureFn
                  (MultiplicationFn
                        ?NUMBER
                        (DivisionFn Pi 180))
                  Radian)))

If number is an instance of real number, then "number united states cent(s)" is equal to ""number*" united states dollar(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedStatesCent)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  UnitedStatesDollar)))

If number is an instance of real number, then "number euro cent(s)" is equal to ""number*" euro dollar(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER EuroCent)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  EuroDollar)))

If number is an instance of real number, then "number byte(s)" is equal to ""number*" bit(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Byte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 8)
                  Bit)))

If number is an instance of real number, then "number kilo byte(s)" is equal to ""number*" byte(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER KiloByte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1024)
                  Byte)))

If number is an instance of real number, then "number mega byte(s)" is equal to ""number*" kilo byte(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER MegaByte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1024)
                  KiloByte)))

If the distance between obj1 and obj2 is quant, then the distance between obj2 and obj1 is quant.

(=>
      (distance ?OBJ1 ?OBJ2 ?QUANT)
      (distance ?OBJ2 ?OBJ1 ?QUANT))

If the altitude of obj1 is obj2, then obj1 is above to obj2.

(=>
      (altitude ?OBJ1 ?OBJ2 ?HEIGHT)
      (orientation ?OBJ1 ?OBJ2 Above))

If the altitude of obj1 is obj2, then there exists top so that the top of obj1 is top and the distance between top and obj2 is height.

(=>
      (altitude ?OBJ1 ?OBJ2 ?HEIGHT)
      (exists
            (?TOP)
            (and
                  (top ?TOP ?OBJ1)
                  (distance ?TOP ?OBJ2 ?HEIGHT))))

If depth(obj1,obj2,depth) holds, then obj1 is below to obj2.

(=>
      (depth ?OBJ1 ?OBJ2 ?DEPTH)
      (orientation ?OBJ1 ?OBJ2 Below))

If depth(obj1,obj2,depth) holds, then there exists bottom so that the bottom of obj1 is bottom and the distance between bottom and obj2 is depth.

(=>
      (depth ?OBJ1 ?OBJ2 ?DEPTH)
      (exists
            (?BOTTOM)
            (and
                  (bottom ?BOTTOM ?OBJ1)
                  (distance ?BOTTOM ?OBJ2 ?DEPTH))))

if obj1 is larger than obj2,
then for all quant1,quant2 holds: if the measure of obj1 is "quant1 length measure(s)" and the measure of obj2 is "quant2 length measure(s)", then quant1 is greater than quant2

(=>
      (larger ?OBJ1 ?OBJ2)
      (forall
            (?QUANT1 ?QUANT2)
            (=>
                  (and
                        (measure
                              ?OBJ1
                              (MeasureFn ?QUANT1 LengthMeasure))
                        (measure
                              ?OBJ2
                              (MeasureFn ?QUANT2 LengthMeasure)))
                  (greaterThan ?QUANT1 ?QUANT2))))

If point is an instance of time point and point is not equal to positive infinity, then point happen?{s} before positive infinity.

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT PositiveInfinity)))
      (before ?POINT PositiveInfinity))

If point is an instance of time point and point is not equal to positive infinity, then there exists otherpoint so that otherpoint is between point and positive infinity.

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT PositiveInfinity)))
      (exists
            (?OTHERPOINT)
            (temporallyBetween ?POINT ?OTHERPOINT PositiveInfinity)))

If point is an instance of time point and point is not equal to negative infinity, then negative infinity happen?{s} before point.

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT NegativeInfinity)))
      (before NegativeInfinity ?POINT))

If point is an instance of time point and point is not equal to negative infinity, then there exists otherpoint so that otherpoint is between negative infinity and point.

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT NegativeInfinity)))
      (exists
            (?OTHERPOINT)
            (temporallyBetween NegativeInfinity ?OTHERPOINT ?POINT)))

if proc occurs every time1,
then for all time2 holds: if duration of time2 is time1, then there exists position so that position is a part of time2 and there exists inst so that inst is an instance of proc during position

(=>
      (frequency ?PROC ?TIME1)
      (forall
            (?TIME2)
            (=>
                  (duration ?TIME2 ?TIME1)
                  (exists
                        (?POSITION)
                        (and
                              (temporalPart ?POSITION ?TIME2)
                              (holdsDuring
                                    ?POSITION
                                    (exists
                                          (?INST)
                                          (instance ?INST ?PROC))))))))

If point is an instance of time point, then there exists time interval interval so that point is a part of interval.

(=>
      (instance ?POINT TimePoint)
      (exists
            (?INTERVAL)
            (and
                  (instance ?INTERVAL TimeInterval)
                  (temporalPart ?POINT ?INTERVAL))))

If interval is an instance of time interval, then there exists time point point so that point is a part of interval.

(=>
      (instance ?INTERVAL TimeInterval)
      (exists
            (?POINT)
            (and
                  (instance ?POINT TimePoint)
                  (temporalPart ?POINT ?INTERVAL))))

If situation holds during time1 and time2 is a part of time1, then situation holds during time2.

(=>
      (and
            (holdsDuring ?TIME1 ?SITUATION)
            (temporalPart ?TIME2 ?TIME1))
      (holdsDuring ?TIME2 ?SITUATION))

If rel(inst1,inst2) holds during interval and inst1 is an instance of physical and inst2 is an instance of physical, then inst1 exists during interval and inst2 exists during interval.

(=>
      (and
            (holdsDuring
                  ?INTERVAL
                  (holds ?REL ?INST1 ?INST2))
            (instance ?INST1 Physical)
            (instance ?INST2 Physical))
      (and
            (time ?INST1 ?INTERVAL)
            (time ?INST2 ?INTERVAL)))

if "the beginning of interval" is equal to point,
then for all otherpoint holds: if otherpoint is a part of interval and otherpoint is not equal to point, then point happen?{s} before otherpoint

(=>
      (equal
            (BeginFn ?INTERVAL)
            ?POINT)
      (forall
            (?OTHERPOINT)
            (=>
                  (and
                        (temporalPart ?OTHERPOINT ?INTERVAL)
                        (not
                              (equal ?OTHERPOINT ?POINT)))
                  (before ?POINT ?OTHERPOINT))))

If process origins at obj, then "the place where process was at "the beginning of "the time of existence of process""" is located at "the place where obj was at "the beginning of "the time of existence of obj""".

(=>
      (origin ?PROCESS ?OBJ)
      (located
            (WhereFn
                  ?PROCESS
                  (BeginFn
                        (WhenFn ?PROCESS)))
            (WhereFn
                  ?OBJ
                  (BeginFn
                        (WhenFn ?OBJ)))))

if "the end of interval" is equal to point,
then for all otherpoint holds: if otherpoint is a part of interval and otherpoint is not equal to point, then otherpoint happen?{s} before point

(=>
      (equal
            (EndFn ?INTERVAL)
            ?POINT)
      (forall
            (?OTHERPOINT)
            (=>
                  (and
                        (temporalPart ?OTHERPOINT ?INTERVAL)
                        (not
                              (equal ?OTHERPOINT ?POINT)))
                  (before ?OTHERPOINT ?POINT))))

if obj is an instance of object,
then there exist time point time1,time point time2 so that time1 happen?{s} before time2 and for all time holds: if time1 happen?{s} before or at time and time happen?{s} before or at time2, then obj exists during time

(=>
      (instance ?OBJ Object)
      (exists
            (?TIME1 ?TIME2)
            (and
                  (instance ?TIME1 TimePoint)
                  (instance ?TIME2 TimePoint)
                  (before ?TIME1 ?TIME2)
                  (forall
                        (?TIME)
                        (=>
                              (and
                                    (beforeOrEqual ?TIME1 ?TIME)
                                    (beforeOrEqual ?TIME ?TIME2))
                              (time ?OBJ ?TIME))))))

if obj is a result of proc,
then for all time holds: if time happen?{s} before "the beginning of "the time of existence of proc"", then obj doesn't exist during time

(=>
      (result ?PROC ?OBJ)
      (forall
            (?TIME)
            (=>
                  (before
                        ?TIME
                        (BeginFn
                              (WhenFn ?PROC)))
                  (not
                        (time ?OBJ ?TIME)))))

If point1 happen?{s} before or at point2, then point1 happen?{s} before point2 or point1 is equal to point2.

(=>
      (beforeOrEqual ?POINT1 ?POINT2)
      (or
            (before ?POINT1 ?POINT2)
            (equal ?POINT1 ?POINT2)))

If rel is an instance of spatial relation and rel(obj1,obj2) holds, then "the time of existence of obj2" overlaps "the time of existence of obj1".

(=>
      (and
            (instance ?REL SpatialRelation)
            (holds ?REL ?OBJ1 ?OBJ2))
      (overlapsTemporally
            (WhenFn ?OBJ1)
            (WhenFn ?OBJ2)))

If interval1 takes place during interval2, then "the end of interval1" happen?{s} before "the end of interval2" and "the beginning of interval2" happen?{s} before "the beginning of interval1".

(=>
      (during ?INTERVAL1 ?INTERVAL2)
      (and
            (before
                  (EndFn ?INTERVAL1)
                  (EndFn ?INTERVAL2))
            (before
                  (BeginFn ?INTERVAL2)
                  (BeginFn ?INTERVAL1))))

If "the beginning of interval1" is equal to "the beginning of interval2" and "the end of interval1" is equal to "the end of interval2", then interval1 is equal to interval2.

(=>
      (and
            (equal
                  (BeginFn ?INTERVAL1)
                  (BeginFn ?INTERVAL2))
            (equal
                  (EndFn ?INTERVAL1)
                  (EndFn ?INTERVAL2)))
      (equal ?INTERVAL1 ?INTERVAL2))

If "interval between point1 and point2" is equal to interval, then "the beginning of interval" is equal to point1 and "the end of interval" is equal to point2.

(=>
      (equal
            (TimeIntervalFn ?POINT1 ?POINT2)
            ?INTERVAL)
      (and
            (equal
                  (BeginFn ?INTERVAL)
                  ?POINT1)
            (equal
                  (EndFn ?INTERVAL)
                  ?POINT2)))

If "interval between point1 and point2" is equal to interval, then for all point holds: point is between or at point1 and point2 if and only if point is a part of interval.

(=>
      (equal
            (TimeIntervalFn ?POINT1 ?POINT2)
            ?INTERVAL)
      (forall
            (?POINT)
            (<=>
                  (temporallyBetweenOrEqual ?POINT1 ?POINT ?POINT2)
                  (temporalPart ?POINT ?INTERVAL))))

If interval is an instance of "the recurring period from timeclass1 to timeclass2", then there exist timeclass1 time1,timeclass2 time2 so that time1 starts interval and time2 finishes interval.

(=>
      (instance
            ?INTERVAL
            (RecurrentTimeIntervalFn ?TIMECLASS1 ?TIMECLASS2))
      (exists
            (?TIME1 ?TIME2)
            (and
                  (instance ?TIME1 ?TIMECLASS1)
                  (instance ?TIME2 ?TIMECLASS2)
                  (starts ?TIME1 ?INTERVAL)
                  (finishes ?TIME2 ?INTERVAL))))

If thing is an instance of physical, then "the beginning of "the time of existence of thing"" happen?{s} before "the end of "the time of existence of thing"".

(=>
      (instance ?THING Physical)
      (before
            (BeginFn
                  (WhenFn ?THING))
            (EndFn
                  (WhenFn ?THING))))

If thing is an instance of physical, then "before "the time of existence of thing"" meets "the time of existence of thing".

(=>
      (instance ?THING Physical)
      (meetsTemporally
            (PastFn
                  (WhenFn ?THING))
            (WhenFn ?THING)))

If process is an instance of physical, then "before "the time of existence of process"" is equal to "interval between negative infinity and "the beginning of "the time of existence of process""".

(=>
      (instance ?PROCESS Physical)
      (equal
            (PastFn
                  (WhenFn ?PROCESS))
            (TimeIntervalFn
                  NegativeInfinity
                  (BeginFn
                        (WhenFn ?PROCESS)))))

If thing is an instance of physical, then "immediately before "the time of existence of thing"" finishes "before "the time of existence of thing"".

(=>
      (instance ?THING Physical)
      (finishes
            (ImmediatePastFn
                  (WhenFn ?THING))
            (PastFn
                  (WhenFn ?THING))))

If obj is a resource for proc and the measure of obj is quant1 immediately before "the time of existence of proc" and the measure of obj is quant2 immediately after "the time of existence of proc", then quant1 is greater than quant2.

(=>
      (and
            (resource ?PROC ?OBJ)
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?PROC))
                  (measure ?OBJ ?QUANT1))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?PROC))
                  (measure ?OBJ ?QUANT2)))
      (greaterThan ?QUANT1 ?QUANT2))

If thing is an instance of physical, then "the time of existence of thing" meets "after "the time of existence of thing"".

(=>
      (instance ?THING Physical)
      (meetsTemporally
            (WhenFn ?THING)
            (FutureFn
                  (WhenFn ?THING))))

If process is an instance of physical, then "after "the time of existence of process"" is equal to "interval between "the end of "the time of existence of process"" and positive infinity".

(=>
      (instance ?PROCESS Physical)
      (equal
            (FutureFn
                  (WhenFn ?PROCESS))
            (TimeIntervalFn
                  (EndFn
                        (WhenFn ?PROCESS))
                  PositiveInfinity)))

If thing is an instance of physical, then "immediately after "the time of existence of thing"" starts "after "the time of existence of thing"".

(=>
      (instance ?THING Physical)
      (starts
            (ImmediateFutureFn
                  (WhenFn ?THING))
            (FutureFn
                  (WhenFn ?THING))))

If day is an instance of "the day number", then number is less than or equal to .

(=>
      (instance
            ?DAY
            (DayFn ?NUMBER ?MONTH))
      (lessThanOrEqualTo ?NUMBER 31))

If day1 is an instance of "the day number1" and day2 is an instance of "the day number2" and "(number2-number1)" is equal to , then day1 meets day2.

(=>
      (and
            (instance
                  ?DAY1
                  (DayFn ?NUMBER1 ?MONTH))
            (instance
                  ?DAY2
                  (DayFn ?NUMBER2 ?MONTH))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?DAY1 ?DAY2))

If hour is an instance of "the hour number", then number is less than .

(=>
      (instance
            ?HOUR
            (HourFn ?NUMBER ?DAY))
      (lessThan ?NUMBER 24))

If hour1 is an instance of "the hour number1" and hour2 is an instance of "the hour number2" and "(number2-number1)" is equal to , then hour1 meets hour2.

(=>
      (and
            (instance
                  ?HOUR1
                  (HourFn ?NUMBER1 ?DAY))
            (instance
                  ?HOUR2
                  (HourFn ?NUMBER2 ?DAY))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?HOUR1 ?HOUR2))

If minute is an instance of "the minute number", then number is less than .

(=>
      (instance
            ?MINUTE
            (MinuteFn ?NUMBER ?HOUR))
      (lessThan ?NUMBER 60))

If minute1 is an instance of "the minute number1" and minute2 is an instance of "the minute number2" and "(number2-number1)" is equal to , then minute1 meets minute2.

(=>
      (and
            (instance
                  ?MINUTE1
                  (MinuteFn ?NUMBER1 ?HOUR))
            (instance
                  ?MINUTE2
                  (MinuteFn ?NUMBER2 ?HOUR))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?MINUTE1 ?MINUTE2))

If second is an instance of "the second number", then number is less than .

(=>
      (instance
            ?SECOND
            (SecondFn ?NUMBER ?MINUTE))
      (lessThan ?NUMBER 60))

If second1 is an instance of "the second number1" and second2 is an instance of "the second number2" and "(number2-number1)" is equal to , then second1 meets second2.

(=>
      (and
            (instance
                  ?SECOND1
                  (SecondFn ?NUMBER1 ?MINUTE))
            (instance
                  ?SECOND2
                  (SecondFn ?NUMBER2 ?MINUTE))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?SECOND1 ?SECOND2))

If year is an instance of year, then duration of year is " year duration(s)".

(=>
      (instance ?YEAR Year)
      (duration
            ?YEAR
            (MeasureFn 1 YearDuration)))

If year1 is an instance of year and year2 is an instance of year and "(year2-year1)" is equal to , then year1 meets year2.

(=>
      (and
            (instance ?YEAR1 Year)
            (instance ?YEAR2 Year)
            (equal
                  (SubtractionFn ?YEAR2 ?YEAR1)
                  1))
      (meetsTemporally ?YEAR1 ?YEAR2))

If leap is an instance of leap year and leap is equal to "number year(s)", then

"number mod " is equal to and "number mod " is not equal to
"number mod " is equal to

(=>
      (and
            (instance ?LEAP LeapYear)
            (equal
                  ?LEAP
                  (MeasureFn ?NUMBER Year)))
      (or
            (and
                  (equal
                        (RemainderFn ?NUMBER 4)
                        0)
                  (not
                        (equal
                              (RemainderFn ?NUMBER 100)
                              0)))
            (equal
                  (RemainderFn ?NUMBER 400)
                  0)))

If month is an instance of january, then duration of month is " day duration(s)".

(=>
      (instance ?MONTH January)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month1 is equal to "the month january" and month2 is equal to "the month february", then month1 meets month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn January ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn February ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If "the month february" is equal to month and year is not an instance of leap year, then duration of month is " day duration(s)".

(=>
      (and
            (equal
                  (MonthFn February ?YEAR)
                  ?MONTH)
            (not
                  (instance ?YEAR LeapYear)))
      (duration
            ?MONTH
            (MeasureFn 28 DayDuration)))

If "the month february" is equal to month and year is an instance of leap year, then duration of month is " day duration(s)".

(=>
      (and
            (equal
                  (MonthFn February ?YEAR)
                  ?MONTH)
            (instance ?YEAR LeapYear))
      (duration
            ?MONTH
            (MeasureFn 29 DayDuration)))

If month1 is equal to "the month february" and month2 is equal to "the month march", then month1 meets month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn February ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn March ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month is an instance of march, then duration of month is " day duration(s)".

(=>
      (instance ?MONTH March)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month1 is equal to "the month march" and month2 is equal to "the month april", then month1 meets month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn March ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn April ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month is an instance of april, then duration of month is " day duration(s)".

(=>
      (instance ?MONTH April)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

If month1 is equal to "the month april" and month2 is equal to "the month may", then month1 meets month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn April ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn May ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month is an instance of may, then duration of month is " day duration(s)".

(=>
      (instance ?MONTH May)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month1 is equal to "the month may" and month2 is equal to "the month june", then month1 meets month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn May ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn June ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month is an instance of june, then duration of month is " day duration(s)".

(=>
      (instance ?MONTH June)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

If month1 is equal to "the month june" and month2 is equal to "the month july", then month1 meets month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn June ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn July ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month is an instance of july, then duration of month is " day duration(s)".

(=>
      (instance ?MONTH July)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month1 is equal to "the month july" and month2 is equal to "the month august", then month1 meets month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn July ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn August ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month is an instance of august, then duration of month is " day duration(s)".

(=>
      (instance ?MONTH August)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month1 is equal to "the month august" and month2 is equal to "the month september", then month1 meets month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn August ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn September ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month is an instance of september, then duration of month is " day duration(s)".

(=>
      (instance ?MONTH September)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

If month1 is equal to "the month september" and month2 is equal to "the month october", then month1 meets month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn September ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn October ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month is an instance of october, then duration of month is " day duration(s)".

(=>
      (instance ?MONTH October)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month1 is equal to "the month october" and month2 is equal to "the month november", then month1 meets month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn October ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn November ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month is an instance of november, then duration of month is " day duration(s)".

(=>
      (instance ?MONTH November)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

If month1 is equal to "the month november" and month2 is equal to "the month december", then month1 meets month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn November ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn December ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month is an instance of december, then duration of month is " day duration(s)".

(=>
      (instance ?MONTH December)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month1 is equal to "the month december" and month2 is equal to "the month january" and year1 meets year2, then month1 meets month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn December ?YEAR1))
            (equal
                  ?MONTH2
                  (MonthFn January ?YEAR2))
            (meetsTemporally ?YEAR1 ?YEAR2))
      (meetsTemporally ?MONTH1 ?MONTH2))

If day is an instance of day, then duration of day is " day duration(s)".

(=>
      (instance ?DAY Day)
      (duration
            ?DAY
            (MeasureFn 1 DayDuration)))

If day1 is an instance of monday and day2 is an instance of tuesday and week is an instance of week and day1 is a part of week and day2 is a part of week, then day1 meets day2.

(=>
      (and
            (instance ?DAY1 Monday)
            (instance ?DAY2 Tuesday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

If day1 is an instance of tuesday and day2 is an instance of wednesday and week is an instance of week and day1 is a part of week and day2 is a part of week, then day1 meets day2.

(=>
      (and
            (instance ?DAY1 Tuesday)
            (instance ?DAY2 Wednesday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

If day1 is an instance of wednesday and day2 is an instance of thursday and week is an instance of week and day1 is a part of week and day2 is a part of week, then day1 meets day2.

(=>
      (and
            (instance ?DAY1 Wednesday)
            (instance ?DAY2 Thursday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

If day1 is an instance of thursday and day2 is an instance of friday and week is an instance of week and day1 is a part of week and day2 is a part of week, then day1 meets day2.

(=>
      (and
            (instance ?DAY1 Thursday)
            (instance ?DAY2 Friday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

If day1 is an instance of friday and day2 is an instance of saturday and week is an instance of week and day1 is a part of week and day2 is a part of week, then day1 meets day2.

(=>
      (and
            (instance ?DAY1 Friday)
            (instance ?DAY2 Saturday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

If day1 is an instance of saturday and day2 is an instance of sunday and week is an instance of week and day1 is a part of week and day2 is a part of week, then day1 meets day2.

(=>
      (and
            (instance ?DAY1 Saturday)
            (instance ?DAY2 Sunday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

If day1 is an instance of sunday and day2 is an instance of monday and week1 is an instance of week and week2 is an instance of week and day1 is a part of week1 and day2 is a part of week2 and week1 meets week2, then day1 meets day2.

(=>
      (and
            (instance ?DAY1 Sunday)
            (instance ?DAY2 Monday)
            (instance ?WEEK1 Week)
            (instance ?WEEK2 Week)
            (temporalPart ?DAY1 ?WEEK1)
            (temporalPart ?DAY2 ?WEEK2)
            (meetsTemporally ?WEEK1 ?WEEK2))
      (meetsTemporally ?DAY1 ?DAY2))

If week is an instance of week, then duration of week is " week duration(s)".

(=>
      (instance ?WEEK Week)
      (duration
            ?WEEK
            (MeasureFn 1 WeekDuration)))

If hour is an instance of hour, then duration of hour is " hour duration(s)".

(=>
      (instance ?HOUR Hour)
      (duration
            ?HOUR
            (MeasureFn 1 HourDuration)))

If minute is an instance of minute, then duration of minute is " minute duration(s)".

(=>
      (instance ?MINUTE Minute)
      (duration
            ?MINUTE
            (MeasureFn 1 MinuteDuration)))

If second is an instance of second, then duration of second is " second duration(s)".

(=>
      (instance ?SECOND Second)
      (duration
            ?SECOND
            (MeasureFn 1 SecondDuration)))

if "decomposition of interval into ? interval-types" is equal to class,
then for all time1,time2 holds: if time1 is an instance of interval-type and time2 is an instance of class, then there exists duration so that duration of time1 is duration and duration of time2 is duration

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1 ?TIME2)
            (=>
                  (and
                        (instance ?TIME1 ?INTERVAL-TYPE)
                        (instance ?TIME2 ?CLASS))
                  (exists
                        (?DURATION)
                        (and
                              (duration ?TIME1 ?DURATION)
                              (duration ?TIME2 ?DURATION))))))

if "decomposition of interval into ? interval-types" is equal to class,
then for all time1,time2 holds: if time1 is an instance of class and time2 is an instance of class and time1 is not equal to time2, then time1 meets time2 or time2 meets time1 or time1 happens earlier than time2 or time2 happens earlier than time1

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1 ?TIME2)
            (=>
                  (and
                        (instance ?TIME1 ?CLASS)
                        (instance ?TIME2 ?CLASS)
                        (not
                              (equal ?TIME1 ?TIME2)))
                  (or
                        (meetsTemporally ?TIME1 ?TIME2)
                        (meetsTemporally ?TIME2 ?TIME1)
                        (earlier ?TIME1 ?TIME2)
                        (earlier ?TIME2 ?TIME1)))))

If "decomposition of interval into ? interval-types" is equal to class, then there exists class time so that time starts interval.

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (exists
            (?TIME)
            (and
                  (instance ?TIME ?CLASS)
                  (starts ?TIME ?INTERVAL))))

If "decomposition of interval into ? interval-types" is equal to class, then there exists class time so that time finishes interval.

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (exists
            (?TIME)
            (and
                  (instance ?TIME ?CLASS)
                  (finishes ?TIME ?INTERVAL))))

if "decomposition of interval into ? interval-types" is equal to class,
then for all time1 holds: if time1 is an instance of class and time1 doesn't finish interval, then there exists class time2 so that time1 meets time2

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1)
            (=>
                  (and
                        (instance ?TIME1 ?CLASS)
                        (not
                              (finishes ?TIME1 ?INTERVAL)))
                  (exists
                        (?TIME2)
                        (and
                              (instance ?TIME2 ?CLASS)
                              (meetsTemporally ?TIME1 ?TIME2))))))

if "decomposition of interval into ? interval-types" is equal to class,
then for all time1 holds: if time1 is an instance of class and time1 doesn't start interval, then there exists class time2 so that time2 meets time1

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1)
            (=>
                  (and
                        (instance ?TIME1 ?CLASS)
                        (not
                              (starts ?TIME1 ?INTERVAL)))
                  (exists
                        (?TIME2)
                        (and
                              (instance ?TIME2 ?CLASS)
                              (meetsTemporally ?TIME2 ?TIME1))))))

if "decomposition of interval into ? interval-types" is equal to class,
then for all time holds: if time is an instance of time point and time is a part of interval, then there exists class instance so that time is a part of instance

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME)
            (=>
                  (and
                        (instance ?TIME TimePoint)
                        (temporalPart ?TIME ?INTERVAL))
                  (exists
                        (?INSTANCE)
                        (and
                              (instance ?INSTANCE ?CLASS)
                              (temporalPart ?TIME ?INSTANCE))))))

If year is an instance of year, then "the number of instances in "decomposition of year into ? months"" is equal to .

(=>
      (instance ?YEAR Year)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?YEAR Month))
            12))

If month is an instance of month and duration of month is "number day duration(s)", then "the number of instances in "decomposition of month into ? days"" is equal to number.

(=>
      (and
            (instance ?MONTH Month)
            (duration
                  ?MONTH
                  (MeasureFn ?NUMBER DayDuration)))
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?MONTH Day))
            ?NUMBER))

If week is an instance of week, then "the number of instances in "decomposition of week into ? days"" is equal to .

(=>
      (instance ?WEEK Week)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?WEEK Day))
            7))

If day is an instance of day, then "the number of instances in "decomposition of day into ? hours"" is equal to .

(=>
      (instance ?DAY Day)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?DAY Hour))
            24))

If hour is an instance of hour, then "the number of instances in "decomposition of hour into ? minutes"" is equal to .

(=>
      (instance ?HOUR Hour)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?HOUR Minute))
            60))

If minute is an instance of minute, then "the number of instances in "decomposition of minute into ? seconds"" is equal to .

(=>
      (instance ?MINUTE Minute)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?MINUTE Second))
            60))

If obj1 is connected to obj2, then obj1 meets obj2 or obj1 overlaps with obj2.

(=>
      (connected ?OBJ1 ?OBJ2)
      (or
            (meetsSpatially ?OBJ1 ?OBJ2)
            (overlapsSpatially ?OBJ1 ?OBJ2)))

obj is an instance of self connected object if and only if for all part1,part2 holds: if obj is equal to "the union of the parts of part1 and part2", then part1 is connected to part2.

(<=>
      (instance ?OBJ SelfConnectedObject)
      (forall
            (?PART1 ?PART2)
            (=>
                  (equal
                        ?OBJ
                        (MereologicalSumFn ?PART1 ?PART2))
                  (connected ?PART1 ?PART2))))

If obj is partly located in region, then obj overlaps with region.

(=>
      (partlyLocated ?OBJ ?REGION)
      (overlapsSpatially ?OBJ ?REGION))

If obj1 is a member of coll and obj2 is a member of coll and obj1 is not equal to obj2, then obj1 doesn't overlap with obj2.

(=>
      (and
            (member ?OBJ1 ?COLL)
            (member ?OBJ2 ?COLL)
            (not
                  (equal ?OBJ1 ?OBJ2)))
      (not
            (overlapsSpatially ?OBJ1 ?OBJ2)))

If rel is an instance of case role and rel(process,obj) holds, then there exists time so that "the place where process was at time" overlaps with obj.

(=>
      (and
            (instance ?REL CaseRole)
            (holds ?REL ?PROCESS ?OBJ))
      (exists
            (?TIME)
            (overlapsSpatially
                  (WhereFn ?PROCESS ?TIME)
                  ?OBJ)))

If obj1 is a superficial part of obj2, then obj1 is not a interior part of obj2 and there doesn't exist obj3 so that obj3 is a interior part of obj1.

(=>
      (superficialPart ?OBJ1 ?OBJ2)
      (and
            (not
                  (interiorPart ?OBJ1 ?OBJ2))
            (not
                  (exists
                        (?OBJ3)
                        (interiorPart ?OBJ3 ?OBJ1)))))

if obj1 is a surface of obj2,
then for all obj3 holds: if obj3 is a superficial part of obj2, then obj3 is a part of obj1

(=>
      (surface ?OBJ1 ?OBJ2)
      (forall
            (?OBJ3)
            (=>
                  (superficialPart ?OBJ3 ?OBJ2)
                  (part ?OBJ3 ?OBJ1))))

if obj1 is a interior part of obj2,
then for all part holds: if part is a superficial part of obj2, then obj1 doesn't overlap with part

(=>
      (interiorPart ?OBJ1 ?OBJ2)
      (forall
            (?PART)
            (=>
                  (superficialPart ?PART ?OBJ2)
                  (not
                        (overlapsSpatially ?OBJ1 ?PART)))))

If the bottom of object is bottom and part is a part of object and part is not connected to bottom, then part is above to bottom.

(=>
      (and
            (bottom ?BOTTOM ?OBJECT)
            (part ?PART ?OBJECT)
            (not
                  (connected ?PART ?BOTTOM)))
      (orientation ?PART ?BOTTOM Above))

If the top of object is top and part is a part of object and part is not connected to top, then part is below to top.

(=>
      (and
            (top ?TOP ?OBJECT)
            (part ?PART ?OBJECT)
            (not
                  (connected ?PART ?TOP)))
      (orientation ?PART ?TOP Below))

If a side of object is side and part is a part of object and part is not connected to side, then there exists direct so that side is direct to part.

(=>
      (and
            (side ?SIDE ?OBJECT)
            (part ?PART ?OBJECT)
            (not
                  (connected ?PART ?SIDE)))
      (exists
            (?DIRECT)
            (orientation ?SIDE ?PART ?DIRECT)))

If the height of object is height and the top of object is top and the bottom of object is bottom, then the distance between top and bottom is height.

(=>
      (and
            (height ?OBJECT ?HEIGHT)
            (top ?TOP ?OBJECT)
            (bottom ?BOTTOM ?OBJECT))
      (distance ?TOP ?BOTTOM ?HEIGHT))

If obj3 is equal to "the union of the parts of obj1 and obj2", then for all part holds: part is a part of obj3 if and only if part is a part of obj1 or part is a part of obj2.

(=>
      (equal
            ?OBJ3
            (MereologicalSumFn ?OBJ1 ?OBJ2))
      (forall
            (?PART)
            (<=>
                  (part ?PART ?OBJ3)
                  (or
                        (part ?PART ?OBJ1)
                        (part ?PART ?OBJ2)))))

If obj3 is equal to "the intersection of the parts of obj1 and obj2", then for all part holds: part is a part of obj3 if and only if part is a part of obj1 and part is a part of obj2.

(=>
      (equal
            ?OBJ3
            (MereologicalProductFn ?OBJ1 ?OBJ2))
      (forall
            (?PART)
            (<=>
                  (part ?PART ?OBJ3)
                  (and
                        (part ?PART ?OBJ1)
                        (part ?PART ?OBJ2)))))

If obj3 is equal to "the difference between the parts of obj1 and obj2", then for all part holds: part is a part of obj3 if and only if part is a part of obj1 and part is not a part of obj2.

(=>
      (equal
            ?OBJ3
            (MereologicalDifferenceFn ?OBJ1 ?OBJ2))
      (forall
            (?PART)
            (<=>
                  (part ?PART ?OBJ3)
                  (and
                        (part ?PART ?OBJ1)
                        (not
                              (part ?PART ?OBJ2))))))

If hole is a hole in obj, then obj is not an instance of hole.

(=>
      (hole ?HOLE ?OBJ)
      (not
            (instance ?OBJ Hole)))

If hole is a hole in obj, then hole doesn't overlap with obj.

(=>
      (hole ?HOLE ?OBJ)
      (not
            (overlapsSpatially ?HOLE ?OBJ)))

If hole is a hole in obj1 and hole is a hole in obj2, then there exists obj3 so that obj3 is a properPart of "the intersection of the parts of obj1 and obj2" and hole is a hole in obj3.

(=>
      (and
            (hole ?HOLE ?OBJ1)
            (hole ?HOLE ?OBJ2))
      (exists
            (?OBJ3)
            (and
                  (properPart
                        ?OBJ3
                        (MereologicalProductFn ?OBJ1 ?OBJ2))
                  (hole ?HOLE ?OBJ3))))

if hole1 is a hole in obj and hole2 is a hole in obj,
then for all hole3 holds: if hole3 is a part of "the union of the parts of hole1 and hole2", then hole3 is a hole in obj

(=>
      (and
            (hole ?HOLE1 ?OBJ)
            (hole ?HOLE2 ?OBJ))
      (forall
            (?HOLE3)
            (=>
                  (part
                        ?HOLE3
                        (MereologicalSumFn ?HOLE1 ?HOLE2))
                  (hole ?HOLE3 ?OBJ))))

If hole is a hole in obj1 and obj1 is a part of obj2, then hole overlaps with obj2 or hole is a hole in obj2.

(=>
      (and
            (hole ?HOLE ?OBJ1)
            (part ?OBJ1 ?OBJ2))
      (or
            (overlapsSpatially ?HOLE ?OBJ2)
            (hole ?HOLE ?OBJ2)))

If hole1 is a hole in obj1 and hole2 is a hole in obj2 and hole1 overlaps with hole2, then obj1 overlaps with obj2.

(=>
      (and
            (hole ?HOLE1 ?OBJ1)
            (hole ?HOLE2 ?OBJ2)
            (overlapsSpatially ?HOLE1 ?HOLE2))
      (overlapsSpatially ?OBJ1 ?OBJ2))

If hole1 is an instance of hole, then there exists hole2 so that hole2 is a properPart of hole1.

(=>
      (instance ?HOLE1 Hole)
      (exists
            (?HOLE2)
            (properPart ?HOLE2 ?HOLE1)))

If obj1 is equal to "the host of the hole hole", then for all obj2 holds: obj2 overlaps with obj1 if and only if there exists obj3 so that hole is a hole in obj3 and obj2 overlaps with obj3.

(=>
      (equal
            ?OBJ1
            (PrincipalHostFn ?HOLE))
      (forall
            (?OBJ2)
            (<=>
                  (overlapsSpatially ?OBJ2 ?OBJ1)
                  (exists
                        (?OBJ3)
                        (and
                              (hole ?HOLE ?OBJ3)
                              (overlapsSpatially ?OBJ2 ?OBJ3))))))

If hole is a hole in obj, then hole is connected to obj.

(=>
      (hole ?HOLE ?OBJ)
      (connected ?HOLE ?OBJ))

If hole1 is an instance of hole and hole2 is a properPart of hole1, then there exists obj so that hole1 meets obj and hole2 doesn't meet obj.

(=>
      (and
            (instance ?HOLE1 Hole)
            (properPart ?HOLE2 ?HOLE1))
      (exists
            (?OBJ)
            (and
                  (meetsSpatially ?HOLE1 ?OBJ)
                  (not
                        (meetsSpatially ?HOLE2 ?OBJ)))))

If there exists time so that obj fills hole during time, then fillable is an attribute of hole.

(=>
      (exists
            (?TIME)
            (holdsDuring
                  ?TIME
                  (fills ?OBJ ?HOLE)))
      (attribute ?HOLE Fillable))

If obj partially fills hole1, then there exists hole2 so that hole2 is a part of hole1 and obj completely fills hole2.

(=>
      (partiallyFills ?OBJ ?HOLE1)
      (exists
            (?HOLE2)
            (and
                  (part ?HOLE2 ?HOLE1)
                  (completelyFills ?OBJ ?HOLE2))))

If obj properly fills hole1, then there exists hole2 so that hole2 is a part of hole1 and obj fills hole2.

(=>
      (properlyFills ?OBJ ?HOLE1)
      (exists
            (?HOLE2)
            (and
                  (part ?HOLE2 ?HOLE1)
                  (fills ?OBJ ?HOLE2))))

If obj1 completely fills hole, then there exists obj2 so that obj2 is a part of obj1 and obj2 fills hole.

(=>
      (completelyFills ?OBJ1 ?HOLE)
      (exists
            (?OBJ2)
            (and
                  (part ?OBJ2 ?OBJ1)
                  (fills ?OBJ2 ?HOLE))))

If obj1 fills hole and fillable is an attribute of obj2, then obj1 doesn't overlap with obj2.

(=>
      (and
            (fills ?OBJ1 ?HOLE)
            (attribute ?OBJ2 Fillable))
      (not
            (overlapsSpatially ?OBJ1 ?OBJ2)))

if obj1 completely fills hole,
then for all obj2 holds: if obj2 is connected to hole, then obj2 is connected to obj1

(=>
      (completelyFills ?OBJ1 ?HOLE)
      (forall
            (?OBJ2)
            (=>
                  (connected ?OBJ2 ?HOLE)
                  (connected ?OBJ2 ?OBJ1))))

If obj1 properly fills hole and obj2 is connected to obj1, then hole is connected to obj2.

(=>
      (and
            (properlyFills ?OBJ1 ?HOLE)
            (connected ?OBJ2 ?OBJ1))
      (connected ?HOLE ?OBJ2))

If obj fills hole1 and hole2 is a properPart of hole1, then obj completely fills hole2.

(=>
      (and
            (fills ?OBJ ?HOLE1)
            (properPart ?HOLE2 ?HOLE1))
      (completelyFills ?OBJ ?HOLE2))

If obj1 fills hole and obj2 is a properPart of obj1, then obj2 properly fills hole.

(=>
      (and
            (fills ?OBJ1 ?HOLE)
            (properPart ?OBJ2 ?OBJ1))
      (properlyFills ?OBJ2 ?HOLE))

If obj1 is equal to "the surface of the hole hole", then for all obj2 holds: obj2 overlaps with obj1 if and only if there exists obj3 so that obj3 is a superficial part of "the host of the hole hole" and hole meets obj3 and obj2 overlaps with obj3.

(=>
      (equal
            ?OBJ1
            (SkinFn ?HOLE))
      (forall
            (?OBJ2)
            (<=>
                  (overlapsSpatially ?OBJ2 ?OBJ1)
                  (exists
                        (?OBJ3)
                        (and
                              (superficialPart
                                    ?OBJ3
                                    (PrincipalHostFn ?HOLE))
                              (meetsSpatially ?HOLE ?OBJ3)
                              (overlapsSpatially ?OBJ2 ?OBJ3))))))

If subproc is a subprocess of proc, then "the time of existence of subproc" is equal to "the time of existence of proc" or "the time of existence of subproc" takes place during "the time of existence of proc".

(=>
      (subProcess ?SUBPROC ?PROC)
      (or
            (equal
                  (WhenFn ?SUBPROC)
                  (WhenFn ?PROC))
            (during
                  (WhenFn ?SUBPROC)
                  (WhenFn ?PROC))))

if subproc is a subprocess of proc,
then for all region holds: if proc is located at region, then subproc is located at region

(=>
      (subProcess ?SUBPROC ?PROC)
      (forall
            (?REGION)
            (=>
                  (located ?PROC ?REGION)
                  (located ?SUBPROC ?REGION))))

If proc is an instance of process and subproc is a subprocess of proc, then there exists time so that subproc exists during time.

(=>
      (and
            (instance ?PROC Process)
            (subProcess ?SUBPROC ?PROC))
      (exists
            (?TIME)
            (time ?SUBPROC ?TIME)))

If proc is an instance of biological process, then there exists organism obj so that proc is located at obj.

(=>
      (instance ?PROC BiologicalProcess)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ Organism)
                  (located ?PROC ?OBJ))))

If proc is an instance of biological process and org experiences proc, then org is an instance of organism.

(=>
      (and
            (instance ?PROC BiologicalProcess)
            (experiencer ?PROC ?ORG))
      (instance ?ORG Organism))

If birth is an instance of birth and agent experiences birth, then there exists death death so that agent experiences death.

(=>
      (and
            (instance ?BIRTH Birth)
            (experiencer ?BIRTH ?AGENT))
      (exists
            (?DEATH)
            (and
                  (instance ?DEATH Death)
                  (experiencer ?DEATH ?AGENT))))

If death is an instance of death and agent experiences death, then dead is an attribute of agent after "the time of existence of death".

(=>
      (and
            (instance ?DEATH Death)
            (experiencer ?DEATH ?AGENT))
      (holdsDuring
            (FutureFn
                  (WhenFn ?DEATH))
            (attribute ?AGENT Dead)))

If death is an instance of death and birth is an instance of birth and agent experiences death and agent experiences birth, then there exists time so that "the time of existence of birth" meets time and time meets "the time of existence of death" and living is an attribute of agent during time.

(=>
      (and
            (instance ?DEATH Death)
            (instance ?BIRTH Birth)
            (experiencer ?DEATH ?AGENT)
            (experiencer ?BIRTH ?AGENT))
      (exists
            (?TIME)
            (and
                  (meetsTemporally
                        (WhenFn ?BIRTH)
                        ?TIME)
                  (meetsTemporally
                        ?TIME
                        (WhenFn ?DEATH))
                  (holdsDuring
                        ?TIME
                        (attribute ?AGENT Living)))))

If act is an instance of ingesting and food is a patient of act, then food is an instance of food.

(=>
      (and
            (instance ?ACT Ingesting)
            (patient ?ACT ?FOOD))
      (instance ?FOOD Food))

If act is an instance of eating and food is a patient of act, then solid is an attribute of food.

(=>
      (and
            (instance ?ACT Eating)
            (patient ?ACT ?FOOD))
      (attribute ?FOOD Solid))

If digest is an instance of digesting and digest is an agent of organism, then there exists ingesting ingest so that ingest is an agent of organism and "the time of existence of digest" overlaps "the time of existence of ingest".

(=>
      (and
            (instance ?DIGEST Digesting)
            (agent ?DIGEST ?ORGANISM))
      (exists
            (?INGEST)
            (and
                  (instance ?INGEST Ingesting)
                  (agent ?INGEST ?ORGANISM)
                  (overlapsTemporally
                        (WhenFn ?INGEST)
                        (WhenFn ?DIGEST)))))

If digest is an instance of digesting, then there exists chemical decomposition decomp so that decomp is a subprocess of digest.

(=>
      (instance ?DIGEST Digesting)
      (exists
            (?DECOMP)
            (and
                  (instance ?DECOMP ChemicalDecomposition)
                  (subProcess ?DECOMP ?DIGEST))))

If rep is an instance of replication and rep is an agent of parent and child is a result of rep, then parent is a parent of child.

(=>
      (and
            (instance ?REP Replication)
            (agent ?REP ?PARENT)
            (result ?REP ?CHILD))
      (parent ?CHILD ?PARENT))

If rep is an instance of replication, then there exists reproductive body body so that body is a result of rep.

(=>
      (instance ?REP Replication)
      (exists
            (?BODY)
            (and
                  (instance ?BODY ReproductiveBody)
                  (result ?REP ?BODY))))

If rep is an instance of sexual reproduction and organism is a result of rep, then there don't exist mother,father so that mother is a mother of organism and father is a father of organism.

(=>
      (and
            (instance ?REP SexualReproduction)
            (result ?REP ?ORGANISM))
      (not
            (exists
                  (?MOTHER ?FATHER)
                  (and
                        (mother ?ORGANISM ?MOTHER)
                        (father ?ORGANISM ?FATHER)))))

If rep is an instance of asexual reproduction and organism is a result of rep, then there don't exist parent1,parent2 so that parent1 is a parent of organism and parent2 is a parent of organism and parent1 is not equal to parent2.

(=>
      (and
            (instance ?REP AsexualReproduction)
            (result ?REP ?ORGANISM))
      (not
            (exists
                  (?PARENT1 ?PARENT2)
                  (and
                        (parent ?ORGANISM ?PARENT1)
                        (parent ?ORGANISM ?PARENT2)
                        (not
                              (equal ?PARENT1 ?PARENT2))))))

If process is an instance of psychological process, then there exists animal animal so that animal experiences process.

(=>
      (instance ?PROCESS PsychologicalProcess)
      (exists
            (?ANIMAL)
            (and
                  (instance ?ANIMAL Animal)
                  (experiencer ?PROCESS ?ANIMAL))))

If proc is an instance of organ or tissueprocess, then there exists thing so that proc is located at thing and thing is an instance of organ or thing is an instance of tissue.

(=>
      (instance ?PROC OrganOrTissueProcess)
      (exists
            (?THING)
            (and
                  (located ?PROC ?THING)
                  (or
                        (instance ?THING Organ)
                        (instance ?THING Tissue)))))

If path is an instance of pathologic process and org experiences path, then there exist part,disease or syndrome disease so that part is a part of org and disease is an attribute of part.

(=>
      (and
            (instance ?PATH PathologicProcess)
            (experiencer ?PATH ?ORG))
      (exists
            (?PART ?DISEASE)
            (and
                  (part ?PART ?ORG)
                  (instance ?DISEASE DiseaseOrSyndrome)
                  (attribute ?PART ?DISEASE))))

If inj is an instance of injuring, then there exists anatomical structure struct so that struct is a patient of inj.

(=>
      (instance ?INJ Injuring)
      (exists
            (?STRUCT)
            (and
                  (instance ?STRUCT AnatomicalStructure)
                  (patient ?INJ ?STRUCT))))

If poison is an instance of poisoning, then there exists thing so that thing is a patient of poison and thing is an instance of organism or thing is an instance of anatomical structure.

(=>
      (instance ?POISON Poisoning)
      (exists
            (?THING)
            (and
                  (patient ?POISON ?THING)
                  (or
                        (instance ?THING Organism)
                        (instance ?THING AnatomicalStructure)))))

If poison is an instance of poisoning, then there exists biologically active substance substance so that substance is an instrument for poison.

(=>
      (instance ?POISON Poisoning)
      (exists
            (?SUBSTANCE)
            (and
                  (instance ?SUBSTANCE BiologicallyActiveSubstance)
                  (instrument ?POISON ?SUBSTANCE))))

If proc is an instance of intentional process and proc is an agent of agent, then there exists purp so that proc has &n purpose purp for agent.

(=>
      (and
            (instance ?PROC IntentionalProcess)
            (agent ?PROC ?AGENT))
      (exists
            (?PURP)
            (hasPurposeForAgent ?PROC ?PURP ?AGENT)))

If proc is an instance of intentional process, then there exists cognitive agent agent so that proc is an agent of agent.

(=>
      (instance ?PROC IntentionalProcess)
      (exists
            (?AGENT)
            (and
                  (instance ?AGENT CognitiveAgent)
                  (agent ?PROC ?AGENT))))

If act is an instance of organizational process and act is an agent of agent, then

agent is an instance of organization
there exists organization org so that agent is a member of org

(=>
      (and
            (instance ?ACT OrganizationalProcess)
            (agent ?ACT ?AGENT))
      (or
            (instance ?AGENT Organization)
            (exists
                  (?ORG)
                  (and
                        (instance ?ORG Organization)
                        (member ?AGENT ?ORG)))))

If act is an instance of religious process and act is an agent of agent, then

agent is an instance of religious organization
there exists religious organization org so that agent is a member of org

(=>
      (and
            (instance ?ACT ReligiousProcess)
            (agent ?ACT ?AGENT))
      (or
            (instance ?AGENT ReligiousOrganization)
            (exists
                  (?ORG)
                  (and
                        (member ?AGENT ?ORG)
                        (instance ?ORG ReligiousOrganization)))))

If join is an instance of joining an organization and org is an instance of organization and join is an agent of org and person is a patient of join, then person is a member of org immediately after "the time of existence of join".

(=>
      (and
            (instance ?JOIN JoiningAnOrganization)
            (instance ?ORG Organization)
            (agent ?JOIN ?ORG)
            (patient ?JOIN ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?JOIN))
            (member ?PERSON ?ORG)))

If leave is an instance of leaving an organization and org is an instance of organization and leave is an agent of org and person is a patient of leave, then person is not a member of org immediately after "the time of existence of leave".

(=>
      (and
            (instance ?LEAVE LeavingAnOrganization)
            (instance ?ORG Organization)
            (agent ?LEAVE ?ORG)
            (patient ?LEAVE ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?LEAVE))
            (not
                  (member ?PERSON ?ORG))))

If grad is an instance of graduation and grad is an agent of org and person is a patient of grad, then org is an instance of educational organization.

(=>
      (and
            (instance ?GRAD Graduation)
            (agent ?GRAD ?ORG)
            (patient ?GRAD ?PERSON))
      (instance ?ORG EducationalOrganization))

If mat is an instance of matriculation and mat is an agent of org and person is a patient of mat, then org is an instance of educational organization.

(=>
      (and
            (instance ?MAT Matriculation)
            (agent ?MAT ?ORG)
            (patient ?MAT ?PERSON))
      (instance ?ORG EducationalOrganization))

If hire is an instance of hiring and org is an instance of organization and hire is an agent of org and person is a patient of hire, then org employs person immediately after "the time of existence of hire".

(=>
      (and
            (instance ?HIRE Hiring)
            (instance ?ORG Organization)
            (agent ?HIRE ?ORG)
            (patient ?HIRE ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?HIRE))
            (employs ?ORG ?PERSON)))

If fire is an instance of terminating employment and org is an instance of organization and fire is an agent of org and person is a patient of fire, then org doesn't employ person immediately after "the time of existence of fire".

(=>
      (and
            (instance ?FIRE TerminatingEmployment)
            (instance ?ORG Organization)
            (agent ?FIRE ?ORG)
            (patient ?FIRE ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?FIRE))
            (not
                  (employs ?ORG ?PERSON))))

If proc is an instance of political process, then there exists government gov so that proc is an agent of gov or gov is a patient of proc.

(=>
      (instance ?PROC PoliticalProcess)
      (exists
            (?GOV)
            (and
                  (instance ?GOV Government)
                  (or
                        (agent ?PROC ?GOV)
                        (patient ?PROC ?GOV)))))

If increase is an instance of increasing and obj is a patient of increase, then there exist unit,quant1,quant2 so that "obj unit(s)" is equal to quant1 immediately before "the time of existence of increase" and "obj unit(s)" is equal to quant2 immediately after "the time of existence of increase" and quant2 is greater than quant1.

(=>
      (and
            (instance ?INCREASE Increasing)
            (patient ?INCREASE ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?INCREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?INCREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (greaterThan ?QUANT2 ?QUANT1))))

If heat is an instance of heating and obj is a patient of heat, then there exist temperature measure unit,quant1,quant2 so that "obj unit(s)" is equal to quant1 immediately before "the time of existence of heat" and "obj unit(s)" is equal to quant2 immediately after "the time of existence of heat" and quant2 is greater than quant1.

(=>
      (and
            (instance ?HEAT Heating)
            (patient ?HEAT ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (instance ?UNIT TemperatureMeasure)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?HEAT))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?HEAT))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (greaterThan ?QUANT2 ?QUANT1))))

If decrease is an instance of decreasing and obj is a patient of decrease, then there exist unit,quant1,quant2 so that "obj unit(s)" is equal to quant1 immediately before "the time of existence of decrease" and "obj unit(s)" is equal to quant2 immediately after "the time of existence of decrease" and quant2 is less than quant1.

(=>
      (and
            (instance ?DECREASE Decreasing)
            (patient ?DECREASE ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?DECREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?DECREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (lessThan ?QUANT2 ?QUANT1))))

If cool is an instance of cooling and obj is a patient of cool, then there exist temperature measure unit,quant1,quant2 so that "obj unit(s)" is equal to quant1 immediately before "the time of existence of cool" and "obj unit(s)" is equal to quant2 immediately after "the time of existence of cool" and quant2 is less than quant1.

(=>
      (and
            (instance ?COOL Cooling)
            (patient ?COOL ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (instance ?UNIT TemperatureMeasure)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?COOL))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?COOL))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (lessThan ?QUANT2 ?QUANT1))))

If motion is an instance of motion and obj is a patient of motion and motion origins at place, then obj is located at place immediately before "the time of existence of motion".

(=>
      (and
            (instance ?MOTION Motion)
            (patient ?MOTION ?OBJ)
            (origin ?MOTION ?PLACE))
      (holdsDuring
            (ImmediatePastFn
                  (WhenFn ?MOTION))
            (located ?OBJ ?PLACE)))

If motion is an instance of motion and obj is a patient of motion and motion ends at place, then obj is located at place immediately after "the time of existence of motion".

(=>
      (and
            (instance ?MOTION Motion)
            (patient ?MOTION ?OBJ)
            (destination ?MOTION ?PLACE))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?MOTION))
            (located ?OBJ ?PLACE)))

if
- path1 is path along with process occurs
- process origins at source
- process ends at dest
- the length of path1 is measure1
- there don't exist path2,measure2 so that path2 is path along with process occurs and process origins at origin and process ends at dest and the length of path2 is measure2 and measure2 is less than measure1
,
then for all obj holds: if obj is a part of path1, then obj is between source and dest

(=>
      (and
            (path ?PROCESS ?PATH1)
            (origin ?PROCESS ?SOURCE)
            (destination ?PROCESS ?DEST)
            (length ?PATH1 ?MEASURE1)
            (not
                  (exists
                        (?PATH2 ?MEASURE2)
                        (and
                              (path ?PROCESS ?PATH2)
                              (origin ?PROCESS ?ORIGIN)
                              (destination ?PROCESS ?DEST)
                              (length ?PATH2 ?MEASURE2)
                              (lessThan ?MEASURE2 ?MEASURE1)))))
      (forall
            (?OBJ)
            (=>
                  (part ?OBJ ?PATH1)
                  (between ?SOURCE ?OBJ ?DEST))))

If motion is an instance of body motion, then there exist body part obj,organism agent so that obj is a patient of motion and motion is an agent of agent.

(=>
      (instance ?MOTION BodyMotion)
      (exists
            (?OBJ ?AGENT)
            (and
                  (instance ?OBJ BodyPart)
                  (patient ?MOTION ?OBJ)
                  (instance ?AGENT Organism)
                  (agent ?MOTION ?AGENT))))

If walk is an instance of walking and walk is an agent of agent, then there exists land area area so that agent is located at area.

(=>
      (and
            (instance ?WALK Walking)
            (agent ?WALK ?AGENT))
      (exists
            (?AREA)
            (and
                  (instance ?AREA LandArea)
                  (located ?AGENT ?AREA))))

If swim is an instance of swimming and swim is an agent of agent, then there exists water area area so that agent is located at area.

(=>
      (and
            (instance ?SWIM Swimming)
            (agent ?SWIM ?AGENT))
      (exists
            (?AREA)
            (and
                  (instance ?AREA WaterArea)
                  (located ?AGENT ?AREA))))

If proc is an instance of direction change, then there exists directional attribute attr so that

proc is performed in the manner attr immediately before "the time of existence of proc" and proc is performed in the manner attr immediately after "the time of existence of proc"
proc is performed in the manner attr immediately after "the time of existence of proc" and proc is performed in the manner attr immediately before "the time of existence of proc"

(=>
      (instance ?PROC DirectionChange)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR DirectionalAttribute)
                  (or
                        (and
                              (holdsDuring
                                    (ImmediatePastFn
                                          (WhenFn ?PROC))
                                    (manner ?PROC ?ATTR))
                              (holdsDuring
                                    (ImmediateFutureFn
                                          (WhenFn ?PROC))
                                    (not
                                          (manner ?PROC ?ATTR))))
                        (and
                              (holdsDuring
                                    (ImmediateFutureFn
                                          (WhenFn ?PROC))
                                    (manner ?PROC ?ATTR))
                              (holdsDuring
                                    (ImmediatePastFn
                                          (WhenFn ?PROC))
                                    (not
                                          (manner ?PROC ?ATTR))))))))

If transfer is an instance of transfer and transfer is an agent of agent and patient is a patient of transfer, then agent is not equal to patient.

(=>
      (and
            (instance ?TRANSFER Transfer)
            (agent ?TRANSFER ?AGENT)
            (patient ?TRANSFER ?PATIENT))
      (not
            (equal ?AGENT ?PATIENT)))

If remove is an instance of removing and remove origins at place and obj is a patient of remove, then obj is located at place immediately before "the time of existence of remove" and obj is not located at place immediately after "the time of existence of remove".

(=>
      (and
            (instance ?REMOVE Removing)
            (origin ?REMOVE ?PLACE)
            (patient ?REMOVE ?OBJ))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?REMOVE))
                  (located ?OBJ ?PLACE))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?REMOVE))
                  (not
                        (located ?OBJ ?PLACE)))))

If put is an instance of putting and put ends at place and obj is a patient of put, then obj is not located at place immediately before "the time of existence of put" and obj is located at place immediately after "the time of existence of put".

(=>
      (and
            (instance ?PUT Putting)
            (destination ?PUT ?PLACE)
            (patient ?PUT ?OBJ))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?PUT))
                  (not
                        (located ?OBJ ?PLACE)))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?PUT))
                  (located ?OBJ ?PLACE))))

If sub is an instance of substituting, then there exist putting put,removing remove,obj1,obj2,place so that put is a subprocess of sub and remove is a subprocess of sub and obj1 is a patient of remove and remove origins at place and obj2 is a patient of put and put ends at place and obj1 is not equal to obj2.

(=>
      (instance ?SUB Substituting)
      (exists
            (?PUT ?REMOVE ?OBJ1 ?OBJ2 ?PLACE)
            (and
                  (instance ?PUT Putting)
                  (instance ?REMOVE Removing)
                  (subProcess ?PUT ?SUB)
                  (subProcess ?REMOVE ?SUB)
                  (patient ?REMOVE ?OBJ1)
                  (origin ?REMOVE ?PLACE)
                  (patient ?PUT ?OBJ2)
                  (destination ?PUT ?PLACE)
                  (not
                        (equal ?OBJ1 ?OBJ2)))))

If touch is an instance of touching and touch is an agent of obj1 and obj2 is a patient of touch, then obj1 is connected to obj2 immediately after "the time of existence of touch".

(=>
      (and
            (instance ?TOUCH Touching)
            (agent ?TOUCH ?OBJ1)
            (patient ?TOUCH ?OBJ2))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?TOUCH))
            (connected ?OBJ1 ?OBJ2)))

If impact is an instance of impacting and obj is a patient of impact, then there exists impelling impel so that obj is a patient of impel and "the time of existence of impel" happens earlier than "the time of existence of impact".

(=>
      (and
            (instance ?IMPACT Impacting)
            (patient ?IMPACT ?OBJ))
      (exists
            (?IMPEL)
            (and
                  (instance ?IMPEL Impelling)
                  (patient ?IMPEL ?OBJ)
                  (earlier
                        (WhenFn ?IMPEL)
                        (WhenFn ?IMPACT)))))

If trans is an instance of transportation, then there exists transportation device device so that device is an instrument for trans.

(=>
      (instance ?TRANS Transportation)
      (exists
            (?DEVICE)
            (and
                  (instance ?DEVICE TransportationDevice)
                  (instrument ?TRANS ?DEVICE))))

If steer is an instance of steering, then there exists transportation device vehicle so that vehicle is a patient of steer.

(=>
      (instance ?STEER Steering)
      (exists
            (?VEHICLE)
            (and
                  (instance ?VEHICLE TransportationDevice)
                  (patient ?STEER ?VEHICLE))))

If education is an instance of educational process and person is a patient of education, then education has purpose "there exists learning learn so that person is a patient of learn".

(=>
      (and
            (instance ?EDUCATION EducationalProcess)
            (patient ?EDUCATION ?PERSON))
      (hasPurpose
            ?EDUCATION
            (exists
                  (?LEARN)
                  (and
                        (instance ?LEARN Learning)
                        (patient ?LEARN ?PERSON)))))

If change is an instance of change of possession and obj is a patient of change and agent1 posesses obj immediately before "the time of existence of change" and agent2 posesses obj immediately after "the time of existence of change", then agent1 is not equal to agent2.

(=>
      (and
            (instance ?CHANGE ChangeOfPossession)
            (patient ?CHANGE ?OBJ)
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?CHANGE))
                  (possesses ?AGENT1 ?OBJ))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?CHANGE))
                  (possesses ?AGENT2 ?OBJ)))
      (not
            (equal ?AGENT1 ?AGENT2)))

If change is an instance of change of possession and change origins at agent1 and change ends at agent2 and agent2 is an instance of agent and obj is a patient of change, then agent1 posesses obj immediately before "the time of existence of change" and agent2 posesses obj immediately after "the time of existence of change".

(=>
      (and
            (instance ?CHANGE ChangeOfPossession)
            (origin ?CHANGE ?AGENT1)
            (destination ?CHANGE ?AGENT2)
            (instance ?AGENT2 Agent)
            (patient ?CHANGE ?OBJ))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?CHANGE))
                  (possesses ?AGENT1 ?OBJ))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?CHANGE))
                  (possesses ?AGENT2 ?OBJ))))

If give is an instance of giving and give is an agent of agent1 and give ends at agent2 and agent2 is an instance of agent and obj is a patient of give, then there exists getting get so that get is an agent of agent2 and get origins at agent1 and obj is a patient of get.

(=>
      (and
            (instance ?GIVE Giving)
            (agent ?GIVE ?AGENT1)
            (destination ?GIVE ?AGENT2)
            (instance ?AGENT2 Agent)
            (patient ?GIVE ?OBJ))
      (exists
            (?GET)
            (and
                  (instance ?GET Getting)
                  (agent ?GET ?AGENT2)
                  (origin ?GET ?AGENT1)
                  (patient ?GET ?OBJ))))

If give is an instance of giving and give is an agent of agent, then give origins at agent.

(=>
      (and
            (instance ?GIVE Giving)
            (agent ?GIVE ?AGENT))
      (origin ?GIVE ?AGENT))

If give is an instance of unilateral giving, then there doesn't exist transaction trans so that give is a subprocess of trans.

(=>
      (instance ?GIVE UnilateralGiving)
      (not
            (exists
                  (?TRANS)
                  (and
                        (instance ?TRANS Transaction)
                        (subProcess ?GIVE ?TRANS)))))

If get is an instance of getting and get is an agent of agent, then get ends at agent.

(=>
      (and
            (instance ?GET Getting)
            (agent ?GET ?AGENT))
      (destination ?GET ?AGENT))

If get is an instance of unilateral getting, then there doesn't exist transaction trans so that get is a subprocess of trans.

(=>
      (instance ?GET UnilateralGetting)
      (not
            (exists
                  (?TRANS)
                  (and
                        (instance ?TRANS Transaction)
                        (subProcess ?GET ?TRANS)))))

If trans is an instance of transaction, then there exist agent1,agent2,giving give1,giving give2,obj1,obj2 so that give1 is a subprocess of trans and give2 is a subprocess of trans and give1 is an agent of agent1 and give2 is an agent of agent2 and obj1 is a patient of give1 and obj2 is a patient of give2 and give1 ends at agent2 and give2 ends at agent1 and agent1 is not equal to agent2 and obj1 is not equal to obj2.

(=>
      (instance ?TRANS Transaction)
      (exists
            (?AGENT1 ?AGENT2 ?GIVE1 ?GIVE2 ?OBJ1 ?OBJ2)
            (and
                  (instance ?GIVE1 Giving)
                  (instance ?GIVE2 Giving)
                  (subProcess ?GIVE1 ?TRANS)
                  (subProcess ?GIVE2 ?TRANS)
                  (agent ?GIVE1 ?AGENT1)
                  (agent ?GIVE2 ?AGENT2)
                  (patient ?GIVE1 ?OBJ1)
                  (patient ?GIVE2 ?OBJ2)
                  (destination ?GIVE1 ?AGENT2)
                  (destination ?GIVE2 ?AGENT1)
                  (not
                        (equal ?AGENT1 ?AGENT2))
                  (not
                        (equal ?OBJ1 ?OBJ2)))))

If trans is an instance of financial transaction, then there exists currency measure obj so that obj is a patient of trans.

(=>
      (instance ?TRANS FinancialTransaction)
      (exists
            (?OBJ)
            (and
                  (patient ?TRANS ?OBJ)
                  (instance ?OBJ CurrencyMeasure))))

If buy is an instance of buying and buy is an agent of agent, then buy ends at agent.

(=>
      (and
            (instance ?BUY Buying)
            (agent ?BUY ?AGENT))
      (destination ?BUY ?AGENT))

If sell is an instance of selling and sell is an agent of agent, then sell origins at agent.

(=>
      (and
            (instance ?SELL Selling)
            (agent ?SELL ?AGENT))
      (origin ?SELL ?AGENT))

If learn is an instance of learning and learn is an agent of agent, then agent is an instance of cognitive agent.

(=>
      (and
            (instance ?LEARN Learning)
            (agent ?LEARN ?AGENT))
      (instance ?AGENT CognitiveAgent))

If there exists learning learn so that learn is an agent of agent and prop is a patient of learn during time, then agent believes prop immediately after time.

(=>
      (holdsDuring
            ?TIME
            (exists
                  (?LEARN)
                  (and
                        (instance ?LEARN Learning)
                        (agent ?LEARN ?AGENT)
                        (patient ?LEARN ?PROP))))
      (holdsDuring
            (ImmediateFutureFn ?TIME)
            (believes ?AGENT ?PROP)))

If agent is an instance of cognitive agent, then agent is capable to do reasoning in role agent.

(=>
      (instance ?AGENT CognitiveAgent)
      (capability Reasoning agent ?AGENT))

If meas is an instance of measuring and meas is an agent of agent and obj is a patient of meas, then there exist quant,unit so that agent knows "the measure of obj is "quant unit(s)"" immediately after "the time of existence of meas".

(=>
      (and
            (instance ?MEAS Measuring)
            (agent ?MEAS ?AGENT)
            (patient ?MEAS ?OBJ))
      (exists
            (?QUANT ?UNIT)
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?MEAS))
                  (knows
                        ?AGENT
                        (measure
                              ?OBJ
                              (MeasureFn ?QUANT ?UNIT))))))

If count is an instance of counting and count is an agent of agent and entity is a patient of count, then there exists number so that agent knows ""the number of instances in entity" is equal to number".

(=>
      (and
            (instance ?COUNT Counting)
            (agent ?COUNT ?AGENT)
            (patient ?COUNT ?ENTITY))
      (exists
            (?NUMBER)
            (knows
                  ?AGENT
                  (equal
                        (CardinalityFn ?ENTITY)
                        ?NUMBER))))

If predict is an instance of predicting and formula is a patient of predict, then there exists time so that formula holds during time and time happen?{s} before "the time of existence of predict" or time happens earlier than "the time of existence of predict".

(=>
      (and
            (instance ?PREDICT Predicting)
            (patient ?PREDICT ?FORMULA))
      (exists
            (?TIME)
            (and
                  (holdsDuring ?TIME ?FORMULA)
                  (or
                        (before
                              ?TIME
                              (WhenFn ?PREDICT))
                        (earlier
                              ?TIME
                              (WhenFn ?PREDICT))))))

If remember is an instance of remembering and formula is a patient of remember, then there exists time so that formula holds during time and time happen?{s} before "the time of existence of remember" or time happens earlier than "the time of existence of remember".

(=>
      (and
            (instance ?REMEMBER Remembering)
            (patient ?REMEMBER ?FORMULA))
      (exists
            (?TIME)
            (and
                  (holdsDuring ?TIME ?FORMULA)
                  (or
                        (before
                              ?TIME
                              (WhenFn ?REMEMBER))
                        (earlier
                              ?TIME
                              (WhenFn ?REMEMBER))))))

If keep is an instance of keeping and keep is an agent of agent and obj is a patient of keep, then there exists putting put so that put is an agent of agent and obj is a patient of put and "the time of existence of put" happens earlier than "the time of existence of keep".

(=>
      (and
            (instance ?KEEP Keeping)
            (agent ?KEEP ?AGENT)
            (patient ?KEEP ?OBJ))
      (exists
            (?PUT)
            (and
                  (instance ?PUT Putting)
                  (agent ?PUT ?AGENT)
                  (patient ?PUT ?OBJ)
                  (earlier
                        (WhenFn ?PUT)
                        (WhenFn ?KEEP)))))

if keep is an instance of keeping and obj is a patient of keep,
then there exists place so that for all time holds: if time is a part of "the time of existence of keep", then obj is located at place during time

(=>
      (and
            (instance ?KEEP Keeping)
            (patient ?KEEP ?OBJ))
      (exists
            (?PLACE)
            (forall
                  (?TIME)
                  (=>
                        (temporalPart
                              ?TIME
                              (WhenFn ?KEEP))
                        (holdsDuring
                              ?TIME
                              (located ?OBJ ?PLACE))))))

If confine is an instance of confining, then there exists human human so that human is a patient of confine.

(=>
      (instance ?CONFINE Confining)
      (exists
            (?HUMAN)
            (and
                  (instance ?HUMAN Human)
                  (patient ?CONFINE ?HUMAN))))

If confine is an instance of confining and person is a patient of confine, then person doesn't desire "person is a patient of confine".

(=>
      (and
            (instance ?CONFINE Confining)
            (patient ?CONFINE ?PERSON))
      (not
            (desires
                  ?PERSON
                  (patient ?CONFINE ?PERSON))))

If repair is an instance of repairing and obj is a patient of repair, then there exists damaging damage so that obj is a patient of damage and "the time of existence of damage" happens earlier than "the time of existence of repair".

(=>
      (and
            (instance ?REPAIR Repairing)
            (patient ?REPAIR ?OBJ))
      (exists
            (?DAMAGE)
            (and
                  (instance ?DAMAGE Damaging)
                  (patient ?DAMAGE ?OBJ)
                  (earlier
                        (WhenFn ?DAMAGE)
                        (WhenFn ?REPAIR)))))

If proc is an instance of therapeutic process and bio is a patient of proc, then

bio is an instance of organism
there exists organism org so that bio is a part of org

(=>
      (and
            (instance ?PROC TherapeuticProcess)
            (patient ?PROC ?BIO))
      (or
            (instance ?BIO Organism)
            (exists
                  (?ORG)
                  (and
                        (instance ?ORG Organism)
                        (part ?BIO ?ORG)))))

If act is an instance of surgery and animal is a patient of act, then there exists cutting subact so that animal is an instance of animal and cutting is a patient of animal and subact is a subprocess of act.

(=>
      (and
            (instance ?ACT Surgery)
            (patient ?ACT ?ANIMAL))
      (exists
            (?SUBACT)
            (and
                  (instance ?SUBACT Cutting)
                  (instance ?ANIMAL Animal)
                  (patient ?ANIMAL ?CUTTING)
                  (subProcess ?SUBACT ?ACT))))

If kill is an instance of killing and kill is an agent of agent and patient is a patient of kill, then agent is an instance of organism and patient is an instance of organism.

(=>
      (and
            (instance ?KILL Killing)
            (agent ?KILL ?AGENT)
            (patient ?KILL ?PATIENT))
      (and
            (instance ?AGENT Organism)
            (instance ?PATIENT Organism)))

If kill is an instance of killing and patient is a patient of kill, then living is an attribute of patient immediately before "the time of existence of kill" and dead is an attribute of patient after "the time of existence of kill".

(=>
      (and
            (instance ?KILL Killing)
            (patient ?KILL ?PATIENT))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?KILL))
                  (attribute ?PATIENT Living))
            (holdsDuring
                  (FutureFn
                        (WhenFn ?KILL))
                  (attribute ?PATIENT Dead))))

If poke is an instance of poking and poke is an agent of agent and obj is a patient of poke and inst is an instrument for poke, then inst connects agent and obj the time of existence of poke.

(=>
      (and
            (instance ?POKE Poking)
            (agent ?POKE ?AGENT)
            (patient ?POKE ?OBJ)
            (instrument ?POKE ?INST))
      (holdsDuring
            (WhenFn ?POKE)
            (connects ?INST ?AGENT ?OBJ)))

If attach is an instance of attaching and obj1 is a patient of attach and obj2 is a patient of attach, then obj1 is not connected to obj2 immediately before "the time of existence of attach" and obj1 is connected to obj2 immediately after "the time of existence of attach".

(=>
      (and
            (instance ?ATTACH Attaching)
            (patient ?ATTACH ?OBJ1)
            (patient ?ATTACH ?OBJ2))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?ATTACH))
                  (not
                        (connected ?OBJ1 ?OBJ2)))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?ATTACH))
                  (connected ?OBJ1 ?OBJ2))))

If detach is an instance of detaching and obj1 is a patient of detach and obj2 is a patient of detach, then obj1 is connected to obj2 immediately before "the time of existence of detach" and obj1 is not connected to obj2 immediately after "the time of existence of detach".

(=>
      (and
            (instance ?DETACH Detaching)
            (patient ?DETACH ?OBJ1)
            (patient ?DETACH ?OBJ2))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?DETACH))
                  (connected ?OBJ1 ?OBJ2))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?DETACH))
                  (not
                        (connected ?OBJ1 ?OBJ2)))))

proc is an instance of chemical process
stuff is a resource for proc or stuff is a result of proc

, then stuff is an instance of pure substance.

(=>
      (and
            (instance ?PROC ChemicalProcess)
            (or
                  (resource ?PROC ?STUFF)
                  (result ?PROC ?STUFF)))
      (instance ?STUFF PureSubstance))

If substance1 is a resource for proc and substance2 is a result of proc and substance1 is an instance of elemental substance and substance2 is an instance of compound substance, then proc is an instance of chemical synthesis.

(=>
      (and
            (resource ?PROC ?SUBSTANCE1)
            (result ?PROC ?SUBSTANCE2)
            (instance ?SUBSTANCE1 ElementalSubstance)
            (instance ?SUBSTANCE2 CompoundSubstance))
      (instance ?PROC ChemicalSynthesis))

If substance1 is a resource for proc and substance2 is a result of proc and substance1 is an instance of compound substance and substance2 is an instance of elemental substance, then proc is an instance of chemical decomposition.

(=>
      (and
            (resource ?PROC ?SUBSTANCE1)
            (result ?PROC ?SUBSTANCE2)
            (instance ?SUBSTANCE1 CompoundSubstance)
            (instance ?SUBSTANCE2 ElementalSubstance))
      (instance ?PROC ChemicalDecomposition))

If combustion is an instance of combustion, then there exist heating heat,radiating light light so that heat is a subprocess of combustion and light is a subprocess of combustion.

(=>
      (instance ?COMBUSTION Combustion)
      (exists
            (?HEAT ?LIGHT)
            (and
                  (instance ?HEAT Heating)
                  (instance ?LIGHT RadiatingLight)
                  (subProcess ?HEAT ?COMBUSTION)
                  (subProcess ?LIGHT ?COMBUSTION))))

If change is an instance of internal change and obj is a patient of change, then there exists property so that

property is an attribute of obj immediately before "the time of existence of change" and property is not an attribute of obj immediately after "the time of existence of change"
property is not an attribute of obj immediately before "the time of existence of change" and property is an attribute of obj immediately after "the time of existence of change"

(=>
      (and
            (instance ?CHANGE InternalChange)
            (patient ?CHANGE ?OBJ))
      (exists
            (?PROPERTY)
            (or
                  (and
                        (holdsDuring
                              (ImmediatePastFn
                                    (WhenFn ?CHANGE))
                              (attribute ?OBJ ?PROPERTY))
                        (holdsDuring
                              (ImmediateFutureFn
                                    (WhenFn ?CHANGE))
                              (not
                                    (attribute ?OBJ ?PROPERTY))))
                  (and
                        (holdsDuring
                              (ImmediatePastFn
                                    (WhenFn ?CHANGE))
                              (not
                                    (attribute ?OBJ ?PROPERTY)))
                        (holdsDuring
                              (ImmediateFutureFn
                                    (WhenFn ?CHANGE))
                              (attribute ?OBJ ?PROPERTY))))))

If alt is an instance of surface change and obj is a patient of alt, then there exist part,property so that part is a superficial part of obj and property is an attribute of part immediately before "the time of existence of alt" and property is not an attribute of part immediately after "the time of existence of alt".

(=>
      (and
            (instance ?ALT SurfaceChange)
            (patient ?ALT ?OBJ))
      (exists
            (?PART ?PROPERTY)
            (and
                  (superficialPart ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?ALT))
                        (attribute ?PART ?PROPERTY))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?ALT))
                        (not
                              (attribute ?PART ?PROPERTY))))))

If alt is an instance of shape change and obj is a patient of alt, then there exists shape attribute property so that

property is an attribute of obj immediately before "the time of existence of alt" and property is not an attribute of obj immediately after "the time of existence of alt"
property is not an attribute of obj immediately before "the time of existence of alt" and property is an attribute of obj immediately after "the time of existence of alt"

(=>
      (and
            (instance ?ALT ShapeChange)
            (patient ?ALT ?OBJ))
      (exists
            (?PROPERTY)
            (and
                  (instance ?PROPERTY ShapeAttribute)
                  (or
                        (and
                              (holdsDuring
                                    (ImmediatePastFn
                                          (WhenFn ?ALT))
                                    (attribute ?OBJ ?PROPERTY))
                              (holdsDuring
                                    (ImmediateFutureFn
                                          (WhenFn ?ALT))
                                    (not
                                          (attribute ?OBJ ?PROPERTY))))
                        (and
                              (holdsDuring
                                    (ImmediatePastFn
                                          (WhenFn ?ALT))
                                    (not
                                          (attribute ?OBJ ?PROPERTY)))
                              (holdsDuring
                                    (ImmediateFutureFn
                                          (WhenFn ?ALT))
                                    (attribute ?OBJ ?PROPERTY)))))))

If coloring is an instance of coloring and obj is a patient of coloring, then there exists color attribute property so that property is an attribute of obj immediately before "the time of existence of coloring" and property is not an attribute of obj immediately after "the time of existence of coloring".

(=>
      (and
            (instance ?COLORING Coloring)
            (patient ?COLORING ?OBJ))
      (exists
            (?PROPERTY)
            (and
                  (instance ?PROPERTY ColorAttribute)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?COLORING))
                        (attribute ?OBJ ?PROPERTY))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?COLORING))
                        (not
                              (attribute ?OBJ ?PROPERTY))))))

If develop is an instance of content development, then there exists content bearing object obj so that obj is a patient of develop.

(=>
      (instance ?DEVELOP ContentDevelopment)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ ContentBearingObject)
                  (patient ?DEVELOP ?OBJ))))

If read is an instance of reading, then there exist text text,prop so that text contains information prop and read expresses the content of prop.

(=>
      (instance ?READ Reading)
      (exists
            (?TEXT ?PROP)
            (and
                  (instance ?TEXT Text)
                  (containsInformation ?TEXT ?PROP)
                  (realization ?READ ?PROP))))

If decode is an instance of decoding and doc1 is a patient of decode, then there exist encode,doc2,time so that doc2 contains information prop and doc1 contains information prop and time is a part of "before "the time of existence of decode"" and encode is an instance of encoding and doc2 is a patient of encode during time.

(=>
      (and
            (instance ?DECODE Decoding)
            (patient ?DECODE ?DOC1))
      (exists
            (?ENCODE ?DOC2 ?TIME)
            (and
                  (containsInformation ?DOC2 ?PROP)
                  (containsInformation ?DOC1 ?PROP)
                  (temporalPart
                        ?TIME
                        (PastFn
                              (WhenFn ?DECODE)))
                  (holdsDuring
                        ?TIME
                        (and
                              (instance ?ENCODE Encoding)
                              (patient ?ENCODE ?DOC2))))))

If wet is an instance of wetting and obj is a patient of wet, then wet is an attribute of obj or damp is an attribute of obj immediately after "the time of existence of wet".

(=>
      (and
            (instance ?WET Wetting)
            (patient ?WET ?OBJ))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?WET))
            (or
                  (attribute ?OBJ Wet)
                  (attribute ?OBJ Damp))))

If wet is an instance of wetting, then there exists obj so that liquid is an attribute of obj and obj is a patient of wet.

(=>
      (instance ?WET Wetting)
      (exists
            (?OBJ)
            (and
                  (attribute ?OBJ Liquid)
                  (patient ?WET ?OBJ))))

If dry is an instance of drying and obj is a patient of dry, then dry is an attribute of obj immediately after "the time of existence of dry".

(=>
      (and
            (instance ?DRY Drying)
            (patient ?DRY ?OBJ))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?DRY))
            (attribute ?OBJ Dry)))

If action is an instance of creation, then there exists result so that result is a result of action.

(=>
      (instance ?ACTION Creation)
      (exists
            (?RESULT)
            (result ?ACTION ?RESULT)))

If pub is an instance of publication and text is a patient of pub, then text is a subclass of text.

(=>
      (and
            (instance ?PUB Publication)
            (patient ?PUB ?TEXT))
      (subclass ?TEXT Text))

If cook is an instance of cooking, then there exists food food so that food is a result of cook.

(=>
      (instance ?COOK Cooking)
      (exists
            (?FOOD)
            (and
                  (instance ?FOOD Food)
                  (result ?COOK ?FOOD))))

If search is an instance of searching and search is an agent of agent and entity is a patient of search, then agent is interested in entity.

(=>
      (and
            (instance ?SEARCH Searching)
            (agent ?SEARCH ?AGENT)
            (patient ?SEARCH ?ENTITY))
      (inScopeOfInterest ?AGENT ?ENTITY))

If pursue is an instance of pursuing and pursue is an agent of agent and obj is a patient of pursue, then agent wants obj during pursue.

(=>
      (and
            (instance ?PURSUE Pursuing)
            (agent ?PURSUE ?AGENT)
            (patient ?PURSUE ?OBJ))
      (holdsDuring
            ?PURSUE
            (wants ?AGENT ?OBJ)))

If pursue is an instance of pursuing and pursue is an agent of agent and obj is a patient of pursue, then agent doesn't posess obj during pursue.

(=>
      (and
            (instance ?PURSUE Pursuing)
            (agent ?PURSUE ?AGENT)
            (patient ?PURSUE ?OBJ))
      (holdsDuring
            ?PURSUE
            (not
                  (possesses ?AGENT ?OBJ))))

If investigate is an instance of investigating and prop is a patient of investigate, then prop is an instance of formula.

(=>
      (and
            (instance ?INVESTIGATE Investigating)
            (patient ?INVESTIGATE ?PROP))
      (instance ?PROP Formula))

If investigate is an instance of investigating and investigate is an agent of agent and prop is a patient of investigate, then agent doesn't know prop the time of existence of investigate.

(=>
      (and
            (instance ?INVESTIGATE Investigating)
            (agent ?INVESTIGATE ?AGENT)
            (patient ?INVESTIGATE ?PROP))
      (holdsDuring
            (WhenFn ?INVESTIGATE)
            (not
                  (knows ?AGENT ?PROP))))

If proc is an instance of diagnostic process and proc is an agent of agent, then there exists cause so that proc has &n purpose "agent knows "cause causes proc"" for agent.

(=>
      (and
            (instance ?PROC DiagnosticProcess)
            (agent ?PROC ?AGENT))
      (exists
            (?CAUSE)
            (hasPurposeForAgent
                  ?PROC
                  (knows
                        ?AGENT
                        (causes ?CAUSE ?PROC))
                  ?AGENT)))

If interaction is an instance of social interaction, then there exist agent1,agent2 so that interaction is an agent of agent1 and interaction is an agent of agent2 and agent1 is not equal to agent2.

(=>
      (instance ?INTERACTION SocialInteraction)
      (exists
            (?AGENT1 ?AGENT2)
            (and
                  (agent ?INTERACTION ?AGENT1)
                  (agent ?INTERACTION ?AGENT2)
                  (not
                        (equal ?AGENT1 ?AGENT2)))))

If pretend is an instance of pretending, then there exist person,prop so that pretend has purpose "person believes prop" and prop is true.

(=>
      (instance ?PRETEND Pretending)
      (exists
            (?PERSON ?PROP)
            (and
                  (hasPurpose
                        ?PRETEND
                        (believes ?PERSON ?PROP))
                  (true ?PROP True))))

If communicate is an instance of communication, then there exist content bearing object obj,cognitive agent agent1,cognitive agent agent2 so that obj is a patient of communicate and communicate is an agent of agent1 and communicate ends at agent2.

(=>
      (instance ?COMMUNICATE Communication)
      (exists
            (?OBJ ?AGENT1 ?AGENT2)
            (and
                  (instance ?OBJ ContentBearingObject)
                  (patient ?COMMUNICATE ?OBJ)
                  (instance ?AGENT1 CognitiveAgent)
                  (agent ?COMMUNICATE ?AGENT1)
                  (instance ?AGENT2 CognitiveAgent)
                  (destination ?COMMUNICATE ?AGENT2))))

If disseminate is an instance of disseminating, then there exist cognitive agent agent1,cognitive agent agent2 so that disseminate ends at agent1 and disseminate ends at agent2 and agent1 is not equal to agent2.

(=>
      (instance ?DISSEMINATE Disseminating)
      (exists
            (?AGENT1 ?AGENT2)
            (and
                  (destination ?DISSEMINATE ?AGENT1)
                  (instance ?AGENT1 CognitiveAgent)
                  (destination ?DISSEMINATE ?AGENT2)
                  (instance ?AGENT2 CognitiveAgent)
                  (not
                        (equal ?AGENT1 ?AGENT2)))))

If advert is an instance of advertising, then there exists obj so that advert includes a reference to obj and advert has purpose "there exists selling sale so that obj is a patient of sale".

(=>
      (instance ?ADVERT Advertising)
      (exists
            (?OBJ)
            (and
                  (refers ?ADVERT ?OBJ)
                  (hasPurpose
                        ?ADVERT
                        (exists
                              (?SALE)
                              (and
                                    (instance ?SALE Selling)
                                    (patient ?SALE ?OBJ)))))))

If communicate is an instance of linguistic communication, then there exists linguistic expression obj so that obj is a patient of communicate.

(=>
      (instance ?COMMUNICATE LinguisticCommunication)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ LinguisticExpression)
                  (patient ?COMMUNICATE ?OBJ))))

If state is an instance of stating and state is an agent of agent and formula is a patient of state and formula is an instance of formula, then agent believes formula the time of existence of state.

(=>
      (and
            (instance ?STATE Stating)
            (agent ?STATE ?AGENT)
            (patient ?STATE ?FORMULA)
            (instance ?FORMULA Formula))
      (holdsDuring
            (WhenFn ?STATE)
            (believes ?AGENT ?FORMULA)))

If order is an instance of ordering and formula is a patient of order, then the statement formula has the model force of obligation.

(=>
      (and
            (instance ?ORDER Ordering)
            (patient ?ORDER ?FORMULA))
      (modalAttribute ?FORMULA Obligation))

If request is an instance of requesting and request is an agent of agent and formula is a patient of request and formula is an instance of formula, then agent desires formula.

(=>
      (and
            (instance ?REQUEST Requesting)
            (agent ?REQUEST ?AGENT)
            (patient ?REQUEST ?FORMULA)
            (instance ?FORMULA Formula))
      (desires ?AGENT ?FORMULA))

If question is an instance of questioning and question is an agent of agent and formula is a patient of question and formula is an instance of formula, then agent doesn't know formula the time of existence of question.

(=>
      (and
            (instance ?QUESTION Questioning)
            (agent ?QUESTION ?AGENT)
            (patient ?QUESTION ?FORMULA)
            (instance ?FORMULA Formula))
      (holdsDuring
            (WhenFn ?QUESTION)
            (not
                  (knows ?AGENT ?FORMULA))))

If commit is an instance of committing and formula is a patient of commit and formula is an instance of formula, then the statement formula has the model force of promise.

(=>
      (and
            (instance ?COMMIT Committing)
            (patient ?COMMIT ?FORMULA)
            (instance ?FORMULA Formula))
      (modalAttribute ?FORMULA Promise))

If express is an instance of expressing and express is an agent of agent, then there exists state of mind state so that state is an attribute of agent and express expresses state.

(=>
      (and
            (instance ?EXPRESS Expressing)
            (agent ?EXPRESS ?AGENT))
      (exists
            (?STATE)
            (and
                  (instance ?STATE StateOfMind)
                  (attribute ?AGENT ?STATE)
                  (represents ?EXPRESS ?STATE))))

If declare is an instance of declaring and declare is an agent of agent1, then there exist proc,agent2 so that declare allows agent2 to perform task of the type proc or declare obligates agent2 to perform task of the type proc.

(=>
      (and
            (instance ?DECLARE Declaring)
            (agent ?DECLARE ?AGENT1))
      (exists
            (?PROC ?AGENT2)
            (or
                  (confersRight ?PROC ?DECLARE ?AGENT2)
                  (confersObligation ?PROC ?DECLARE ?AGENT2))))

if cooperate is an instance of cooperation,
then there exists purp so that for all agent holds: if cooperate is an agent of agent, then cooperate has &n purpose purp for agent

(=>
      (instance ?COOPERATE Cooperation)
      (exists
            (?PURP)
            (forall
                  (?AGENT)
                  (=>
                        (agent ?COOPERATE ?AGENT)
                        (hasPurposeForAgent ?COOPERATE ?PURP ?AGENT)))))

If meet is an instance of meeting and meet is an agent of agent1 and meet is an agent of agent2, then agent1 is near to agent2 the time of existence of meet.

(=>
      (and
            (instance ?MEET Meeting)
            (agent ?MEET ?AGENT1)
            (agent ?MEET ?AGENT2))
      (holdsDuring
            (WhenFn ?MEET)
            (orientation ?AGENT1 ?AGENT2 Near)))

If meet is an instance of meeting, then there exist agent1,agent2 so that meet is an agent of agent1 and meet is an agent of agent2 and meet has purpose "there exists communication comm so that comm is an agent of agent1 and comm is an agent of agent2".

(=>
      (instance ?MEET Meeting)
      (exists
            (?AGENT1 ?AGENT2)
            (and
                  (agent ?MEET ?AGENT1)
                  (agent ?MEET ?AGENT2)
                  (hasPurpose
                        ?MEET
                        (exists
                              (?COMM)
                              (and
                                    (instance ?COMM Communication)
                                    (agent ?COMM ?AGENT1)
                                    (agent ?COMM ?AGENT2)))))))

If contest is an instance of contest, then there exist agent1,agent2,purp1,purp2 so that contest is an agent of agent1 and contest is an agent of agent2 and contest has &n purpose purp1 for agent1 and contest has &n purpose purp2 for agent2 and agent1 is not equal to agent2 and purp1 is not equal to purp2.

(=>
      (instance ?CONTEST Contest)
      (exists
            (?AGENT1 ?AGENT2 ?PURP1 ?PURP2)
            (and
                  (agent ?CONTEST ?AGENT1)
                  (agent ?CONTEST ?AGENT2)
                  (hasPurposeForAgent ?CONTEST ?PURP1 ?AGENT1)
                  (hasPurposeForAgent ?CONTEST ?PURP2 ?AGENT2)
                  (not
                        (equal ?AGENT1 ?AGENT2))
                  (not
                        (equal ?PURP1 ?PURP2)))))

If war is an instance of war, then there exists battle battle so that battle is a subprocess of war.

(=>
      (instance ?WAR War)
      (exists
            (?BATTLE)
            (and
                  (instance ?BATTLE Battle)
                  (subProcess ?BATTLE ?WAR))))

if war is an instance of war and war is an agent of agent,
then
- agent is an instance of nation
- - agent is an instance of organization
  - for all member holds: if member is a member of agent, then member is an instance of nation

(=>
      (and
            (instance ?WAR War)
            (agent ?WAR ?AGENT))
      (or
            (instance ?AGENT Nation)
            (and
                  (instance ?AGENT Organization)
                  (forall
                        (?MEMBER)
                        (=>
                              (member ?MEMBER ?AGENT)
                              (instance ?MEMBER Nation))))))

If battle is an instance of battle, then there exists war war so that battle is a subprocess of war.

(=>
      (instance ?BATTLE Battle)
      (exists
            (?WAR)
            (and
                  (instance ?WAR War)
                  (subProcess ?BATTLE ?WAR))))

If battle is an instance of battle, then there exists violent contest attack so that attack is a subprocess of battle.

(=>
      (instance ?BATTLE Battle)
      (exists
            (?ATTACK)
            (and
                  (instance ?ATTACK ViolentContest)
                  (subProcess ?ATTACK ?BATTLE))))

If move is an instance of maneuver, then there exists contest contest so that move is a subprocess of contest.

(=>
      (instance ?MOVE Maneuver)
      (exists
            (?CONTEST)
            (and
                  (instance ?CONTEST Contest)
                  (subProcess ?MOVE ?CONTEST))))

If percept is an instance of perception and percept is an agent of agent, then agent is an instance of animal.

(=>
      (and
            (instance ?PERCEPT Perception)
            (agent ?PERCEPT ?AGENT))
      (instance ?AGENT Animal))

If percept is an instance of perception and percept is an agent of agent and object is a patient of percept, then agent notices object.

(=>
      (and
            (instance ?PERCEPT Perception)
            (agent ?PERCEPT ?AGENT)
            (patient ?PERCEPT ?OBJECT))
      (notices ?AGENT ?OBJECT))

If agent is an instance of sentient agent, then agent is capable to do perception in role experiencer.

(=>
      (instance ?AGENT SentientAgent)
      (capability Perception experiencer ?AGENT))

If see is an instance of seeing and see is an agent of agent and obj is a patient of see, then

illuminated is an attribute of obj
there exists color attribute prop so that agent knows "prop is an attribute of obj"

(=>
      (and
            (instance ?SEE Seeing)
            (agent ?SEE ?AGENT)
            (patient ?SEE ?OBJ))
      (and
            (attribute ?OBJ Illuminated)
            (exists
                  (?PROP)
                  (and
                        (instance ?PROP ColorAttribute)
                        (knows
                              ?AGENT
                              (attribute ?OBJ ?PROP))))))

If smell is an instance of smelling and obj is a patient of smell, then there exists olfactory attribute attr so that attr is an attribute of obj.

(=>
      (and
            (instance ?SMELL Smelling)
            (patient ?SMELL ?OBJ))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR OlfactoryAttribute)
                  (attribute ?OBJ ?ATTR))))

If taste is an instance of tasting and obj is a patient of taste, then there exists taste attribute attr so that attr is an attribute of obj.

(=>
      (and
            (instance ?TASTE Tasting)
            (patient ?TASTE ?OBJ))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR TasteAttribute)
                  (attribute ?OBJ ?ATTR))))

If hear is an instance of hearing and obj is a patient of hear, then there exists sound attribute attr so that attr is an attribute of obj.

(=>
      (and
            (instance ?HEAR Hearing)
            (patient ?HEAR ?OBJ))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR SoundAttribute)
                  (attribute ?OBJ ?ATTR))))

If tactile is an instance of tactile perception, then there exists touching touch so that touch is a subprocess of tactile.

(=>
      (instance ?TACTILE TactilePerception)
      (exists
            (?TOUCH)
            (and
                  (instance ?TOUCH Touching)
                  (subProcess ?TOUCH ?TACTILE))))

If emit is an instance of radiating sound and emit is an agent of sound, then there exists sound attribute attr so that attr is an attribute of sound.

(=>
      (and
            (instance ?EMIT RadiatingSound)
            (agent ?EMIT ?SOUND))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR SoundAttribute)
                  (attribute ?SOUND ?ATTR))))

If process is an instance of state change and obj is a patient of process, then there exist part,physical state state1,physical state state2 so that part is a part of obj and state1 is not equal to state2 and state1 is an attribute of part immediately before "the time of existence of process" and state2 is an attribute of part immediately after "the time of existence of freeze".

(=>
      (and
            (instance ?PROCESS StateChange)
            (patient ?PROCESS ?OBJ))
      (exists
            (?PART ?STATE1 ?STATE2)
            (and
                  (part ?PART ?OBJ)
                  (instance ?STATE1 PhysicalState)
                  (instance ?STATE2 PhysicalState)
                  (not
                        (equal ?STATE1 ?STATE2))
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?PROCESS))
                        (attribute ?PART ?STATE1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?FREEZE))
                        (attribute ?PART ?STATE2)))))

If melt is an instance of melting, then there exists heating heat so that heat is a subprocess of melt.

(=>
      (instance ?MELT Melting)
      (exists
            (?HEAT)
            (and
                  (instance ?HEAT Heating)
                  (subProcess ?HEAT ?MELT))))

If melt is an instance of melting and obj is a patient of melt, then there exists part so that part is a part of obj and solid is an attribute of part immediately before "the time of existence of melt" and liquid is an attribute of part immediately after "the time of existence of melt".

(=>
      (and
            (instance ?MELT Melting)
            (patient ?MELT ?OBJ))
      (exists
            (?PART)
            (and
                  (part ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?MELT))
                        (attribute ?PART Solid))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?MELT))
                        (attribute ?PART Liquid)))))

If boil is an instance of boiling, then there exists heating heat so that heat is a subprocess of boil.

(=>
      (instance ?BOIL Boiling)
      (exists
            (?HEAT)
            (and
                  (instance ?HEAT Heating)
                  (subProcess ?HEAT ?BOIL))))

If boil is an instance of boiling and obj is a patient of boil, then there exists part so that part is a part of obj and liquid is an attribute of part immediately before "the time of existence of boil" and gas is an attribute of part immediately after "the time of existence of boil".

(=>
      (and
            (instance ?BOIL Boiling)
            (patient ?BOIL ?OBJ))
      (exists
            (?PART)
            (and
                  (part ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?BOIL))
                        (attribute ?PART Liquid))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?BOIL))
                        (attribute ?PART Gas)))))

If cond is an instance of condensing, then there exists cooling cool so that cool is a subprocess of cond.

(=>
      (instance ?COND Condensing)
      (exists
            (?COOL)
            (and
                  (instance ?COOL Cooling)
                  (subProcess ?COOL ?COND))))

If cond is an instance of condensing and obj is a patient of cond, then there exists part so that part is a part of obj and gas is an attribute of part immediately before "the time of existence of cond" and liquid is an attribute of part immediately after "the time of existence of cond".

(=>
      (and
            (instance ?COND Condensing)
            (patient ?COND ?OBJ))
      (exists
            (?PART)
            (and
                  (part ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?COND))
                        (attribute ?PART Gas))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?COND))
                        (attribute ?PART Liquid)))))

If freeze is an instance of freezing, then there exists cooling cool so that cool is a subprocess of freeze.

(=>
      (instance ?FREEZE Freezing)
      (exists
            (?COOL)
            (and
                  (instance ?COOL Cooling)
                  (subProcess ?COOL ?FREEZE))))

If freeze is an instance of freezing and obj is a patient of freeze, then there exists part so that part is a part of obj and liquid is an attribute of part immediately before "the time of existence of freeze" and solid is an attribute of part immediately after "the time of existence of freeze".

(=>
      (and
            (instance ?FREEZE Freezing)
            (patient ?FREEZE ?OBJ))
      (exists
            (?PART)
            (and
                  (part ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?FREEZE))
                        (attribute ?PART Liquid))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?FREEZE))
                        (attribute ?PART Solid)))))

If area is an instance of water area, then there exist bed,hole,water water so that "the host of the hole hole" is equal to bed and water properly fills hole and "the union of the parts of bed and water" is equal to area.

(=>
      (instance ?AREA WaterArea)
      (exists
            (?BED ?HOLE ?WATER)
            (and
                  (equal
                        (PrincipalHostFn ?HOLE)
                        ?BED)
                  (instance ?WATER Water)
                  (properlyFills ?WATER ?HOLE)
                  (equal
                        (MereologicalSumFn ?BED ?WATER)
                        ?AREA))))

If land1 is an instance of land area, then there exists land2 so that land1 is a part of land2 and land2 is an instance of continent or land2 is an instance of island.

(=>
      (instance ?LAND1 LandArea)
      (exists
            (?LAND2)
            (and
                  (part ?LAND1 ?LAND2)
                  (or
                        (instance ?LAND2 Continent)
                        (instance ?LAND2 Island)))))

If island is an instance of island, then there don't exist land area area,part1,part2 so that part1 is a part of island and part2 is a part of area and island is not a part of area and area is not a part of island and part1 is connected to part2.

(=>
      (instance ?ISLAND Island)
      (not
            (exists
                  (?AREA ?PART1 ?PART2)
                  (and
                        (instance ?AREA LandArea)
                        (part ?PART1 ?ISLAND)
                        (part ?PART2 ?AREA)
                        (not
                              (part ?ISLAND ?AREA))
                        (not
                              (part ?AREA ?ISLAND))
                        (connected ?PART1 ?PART2)))))

If state is an instance of state or province, then there exists nation land so that state is a properPart of land.

(=>
      (instance ?STATE StateOrProvince)
      (exists
            (?LAND)
            (and
                  (instance ?LAND Nation)
                  (properPart ?STATE ?LAND))))

If the developmental form of obj is attr1 during time1 and attr2 is a successor attribute of attr1, then there exists time2 so that time2 happens earlier than time1 and the developmental form of obj is attr2 during time2.

(=>
      (and
            (holdsDuring
                  ?TIME1
                  (developmentalForm ?OBJ ?ATTR1))
            (successorAttributeClosure ?ATTR2 ?ATTR1))
      (exists
            (?TIME2)
            (and
                  (earlier ?TIME2 ?TIME1)
                  (holdsDuring
                        ?TIME2
                        (developmentalForm ?OBJ ?ATTR2)))))

If organism is an instance of organism, then there exists birth birth so that organism experiences birth.

(=>
      (instance ?ORGANISM Organism)
      (exists
            (?BIRTH)
            (and
                  (instance ?BIRTH Birth)
                  (experiencer ?BIRTH ?ORGANISM))))

If organism lives in obj, then there exists time so that organism is located at obj during time.

(=>
      (inhabits ?ORGANISM ?OBJ)
      (exists
            (?TIME)
            (holdsDuring
                  ?TIME
                  (located ?ORGANISM ?OBJ))))

If parent is a parent of child, then "the beginning of "the time of existence of parent"" happen?{s} before "the beginning of "the time of existence of child"".

(=>
      (parent ?CHILD ?PARENT)
      (before
            (BeginFn
                  (WhenFn ?PARENT))
            (BeginFn
                  (WhenFn ?CHILD))))

If parent is a parent of child and class is a subclass of organism and parent is an instance of class, then child is an instance of class.

(=>
      (and
            (parent ?CHILD ?PARENT)
            (subclass ?CLASS Organism)
            (instance ?PARENT ?CLASS))
      (instance ?CHILD ?CLASS))

If parent is a parent of child, then parent is a mother of child or parent is a father of child.

(=>
      (parent ?CHILD ?PARENT)
      (or
            (mother ?CHILD ?PARENT)
            (father ?CHILD ?PARENT)))

If organism is an instance of organism, then there exists parent so that parent is a parent of organism.

(=>
      (instance ?ORGANISM Organism)
      (exists
            (?PARENT)
            (parent ?ORGANISM ?PARENT)))

If mother is a mother of child, then female is an attribute of mother.

(=>
      (mother ?CHILD ?MOTHER)
      (attribute ?MOTHER Female))

If father is a father of child, then male is an attribute of father.

(=>
      (father ?CHILD ?FATHER)
      (attribute ?FATHER Male))

If alga is an instance of alga, then there exists water water so that alga lives in water.

(=>
      (instance ?ALGA Alga)
      (exists
            (?WATER)
            (and
                  (inhabits ?ALGA ?WATER)
                  (instance ?WATER Water))))

If fungus is an instance of fungus and fungus lives in obj, then obj is an instance of organism.

(=>
      (and
            (instance ?FUNGUS Fungus)
            (inhabits ?FUNGUS ?OBJ))
      (instance ?OBJ Organism))

if bacterium is an instance of bacterium,
then there exists cell cell1 so that cell1 is a component of bacterium and for all cell2 holds: if cell2 is a component of bacterium and cell2 is an instance of cell, then cell1 is equal to cell2

(=>
      (instance ?BACTERIUM Bacterium)
      (exists
            (?CELL1)
            (and
                  (component ?CELL1 ?BACTERIUM)
                  (instance ?CELL1 Cell)
                  (forall
                        (?CELL2)
                        (=>
                              (and
                                    (component ?CELL2 ?BACTERIUM)
                                    (instance ?CELL2 Cell))
                              (equal ?CELL1 ?CELL2))))))

If bacterium is an instance of bacterium and bacterium lives in obj, then obj is an instance of organism.

(=>
      (and
            (instance ?BACTERIUM Bacterium)
            (inhabits ?BACTERIUM ?OBJ))
      (instance ?OBJ Organism))

if virus is an instance of virus,
then there exists molecule mol1 so that mol1 is a component of virus and for all mol2 holds: if mol2 is a component of virus and mol2 is an instance of molecule, then mol1 is equal to mol2

(=>
      (instance ?VIRUS Virus)
      (exists
            (?MOL1)
            (and
                  (component ?MOL1 ?VIRUS)
                  (instance ?MOL1 Molecule)
                  (forall
                        (?MOL2)
                        (=>
                              (and
                                    (component ?MOL2 ?VIRUS)
                                    (instance ?MOL2 Molecule))
                              (equal ?MOL1 ?MOL2))))))

If virus is an instance of virus and virus lives in obj, then obj is an instance of organism.

(=>
      (and
            (instance ?VIRUS Virus)
            (inhabits ?VIRUS ?OBJ))
      (instance ?OBJ Organism))

If virus is an instance of virus and proc is an instance of replication and proc is an agent of virus, then there exists cell cell so that proc is located at cell.

(=>
      (and
            (instance ?VIRUS Virus)
            (instance ?PROC Replication)
            (agent ?PROC ?VIRUS))
      (exists
            (?CELL)
            (and
                  (located ?PROC ?CELL)
                  (instance ?CELL Cell))))

If fish is an instance of fish, then there exists water water so that fish lives in water.

(=>
      (instance ?FISH Fish)
      (exists
            (?WATER)
            (and
                  (inhabits ?FISH ?WATER)
                  (instance ?WATER Water))))

If organism is an instance of toxic organism, then there exists biologically active substance substance so that substance is a part of organism.

(=>
      (instance ?ORGANISM ToxicOrganism)
      (exists
            (?SUBSTANCE)
            (and
                  (instance ?SUBSTANCE BiologicallyActiveSubstance)
                  (part ?SUBSTANCE ?ORGANISM))))

If food is an instance of food, then there exists nutrient nutrient so that nutrient is a part of food.

(=>
      (instance ?FOOD Food)
      (exists
            (?NUTRIENT)
            (and
                  (instance ?NUTRIENT Nutrient)
                  (part ?NUTRIENT ?FOOD))))

if food is an instance of food,
then for all part1 holds: if part1 is a part of food, then there exist part2,animal animal so that part1 is a part of part2 and part2 is a part of animal

(=>
      (instance ?FOOD Food)
      (forall
            (?PART1)
            (=>
                  (part ?PART1 ?FOOD)
                  (exists
                        (?PART2 ?ANIMAL)
                        (and
                              (part ?PART1 ?PART2)
                              (part ?PART2 ?ANIMAL)
                              (instance ?ANIMAL Animal))))))

if meat is an instance of meat,
then for all part holds: if part is a part of meat, then there exist subpart,time,animal so that subpart is a part of part and animal is an instance of animal and subpart is a part of animal during time

(=>
      (instance ?MEAT Meat)
      (forall
            (?PART)
            (=>
                  (part ?PART ?MEAT)
                  (exists
                        (?SUBPART ?TIME ?ANIMAL)
                        (and
                              (part ?SUBPART ?PART)
                              (holdsDuring
                                    ?TIME
                                    (and
                                          (instance ?ANIMAL Animal)
                                          (part ?SUBPART ?ANIMAL))))))))

if veg is an instance of fruit or vegetable,
then for all part holds: if part is a part of veg, then there exist subpart,time,plant so that subpart is a part of part and plant is an instance of plant and subpart is a part of plant during time

(=>
      (instance ?VEG FruitOrVegetable)
      (forall
            (?PART)
            (=>
                  (part ?PART ?VEG)
                  (exists
                        (?SUBPART ?TIME ?PLANT)
                        (and
                              (part ?SUBPART ?PART)
                              (holdsDuring
                                    ?TIME
                                    (and
                                          (instance ?PLANT Plant)
                                          (part ?SUBPART ?PLANT))))))))

If bev is an instance of beverage, then liquid is an attribute of bev.

(=>
      (instance ?BEV Beverage)
      (attribute ?BEV Liquid))

If drink is an instance of drinking and bev is a patient of drink, then bev is an instance of beverage.

(=>
      (and
            (instance ?DRINK Drinking)
            (patient ?DRINK ?BEV))
      (instance ?BEV Beverage))

If anat is an instance of anatomical structure, then there exists organism organism so that anat is a part of organism.

(=>
      (instance ?ANAT AnatomicalStructure)
      (exists
            (?ORGANISM)
            (and
                  (instance ?ORGANISM Organism)
                  (part ?ANAT ?ORGANISM))))

If part is an instance of anatomical structure, then there exists cell cell so that cell is a part of part.

(=>
      (instance ?PART AnatomicalStructure)
      (exists
            (?CELL)
            (and
                  (instance ?CELL Cell)
                  (part ?CELL ?PART))))

If part is an instance of body part, then there doesn't exist pathologic process proc so that part is a result of proc.

(=>
      (instance ?PART BodyPart)
      (not
            (exists
                  (?PROC)
                  (and
                        (instance ?PROC PathologicProcess)
                        (result ?PROC ?PART)))))

If cover is an instance of body covering, then there exists body so that cover is a superficial part of body and body is an instance of organism or body is an instance of body part.

(=>
      (instance ?COVER BodyCovering)
      (exists
            (?BODY)
            (and
                  (superficialPart ?COVER ?BODY)
                  (or
                        (instance ?BODY Organism)
                        (instance ?BODY BodyPart)))))

If junct is an instance of body junction, then there exists body part struct so that junct is a component of struct.

(=>
      (instance ?JUNCT BodyJunction)
      (exists
            (?STRUCT)
            (and
                  (instance ?STRUCT BodyPart)
                  (component ?JUNCT ?STRUCT))))

If junct is an instance of body junction, then there exist body part struct1,body part struct2 so that junct is connected to struct1 and junct is connected to struct2 and struct1 is not equal to struct2.

(=>
      (instance ?JUNCT BodyJunction)
      (exists
            (?STRUCT1 ?STRUCT2)
            (and
                  (connected ?JUNCT ?STRUCT1)
                  (connected ?JUNCT ?STRUCT2)
                  (instance ?STRUCT1 BodyPart)
                  (instance ?STRUCT2 BodyPart)
                  (not
                        (equal ?STRUCT1 ?STRUCT2)))))

If organ is an instance of organ, then there exists purp so that organ has purpose purp.

(=>
      (instance ?ORGAN Organ)
      (exists
            (?PURP)
            (hasPurpose ?ORGAN ?PURP)))

If stuff is an instance of tissue, then there exists cell part so that part is a part of stuff.

(=>
      (instance ?STUFF Tissue)
      (exists
            (?PART)
            (and
                  (instance ?PART Cell)
                  (part ?PART ?STUFF))))

If stuff is an instance of tissue, then there exists organism organism so that stuff is a part of organism.

(=>
      (instance ?STUFF Tissue)
      (exists
            (?ORGANISM)
            (and
                  (instance ?ORGANISM Organism)
                  (part ?STUFF ?ORGANISM))))

If bone is an instance of bone, then there exists vertebrate vert so that bone is a part of vert.

(=>
      (instance ?BONE Bone)
      (exists
            (?VERT)
            (and
                  (instance ?VERT Vertebrate)
                  (part ?BONE ?VERT))))

If morph is an instance of morpheme, then there doesn't exist morpheme othermorph so that othermorph is a part of morph and othermorph is not equal to morph.

(=>
      (instance ?MORPH Morpheme)
      (not
            (exists
                  (?OTHERMORPH)
                  (and
                        (instance ?OTHERMORPH Morpheme)
                        (part ?OTHERMORPH ?MORPH)
                        (not
                              (equal ?OTHERMORPH ?MORPH))))))

If morph is an instance of morpheme, then there exists word word so that morph is a part of word.

(=>
      (instance ?MORPH Morpheme)
      (exists
            (?WORD)
            (and
                  (instance ?WORD Word)
                  (part ?MORPH ?WORD))))

If word is an instance of word, then there exists morpheme part so that part is a part of word.

(=>
      (instance ?WORD Word)
      (exists
            (?PART)
            (and
                  (part ?PART ?WORD)
                  (instance ?PART Morpheme))))

If phrase is an instance of phrase, then there exist word part1,word part2 so that part1 is a part of phrase and part2 is a part of phrase and part1 is not equal to part2.

(=>
      (instance ?PHRASE Phrase)
      (exists
            (?PART1 ?PART2)
            (and
                  (part ?PART1 ?PHRASE)
                  (part ?PART2 ?PHRASE)
                  (instance ?PART1 Word)
                  (instance ?PART2 Word)
                  (not
                        (equal ?PART1 ?PART2)))))

If sentence is an instance of sentence, then there exist noun phrase phrase1,verb phrase phrase2 so that phrase1 is a part of sentence and phrase2 is a part of sentence.

(=>
      (instance ?SENTENCE Sentence)
      (exists
            (?PHRASE1 ?PHRASE2)
            (and
                  (instance ?PHRASE1 NounPhrase)
                  (instance ?PHRASE2 VerbPhrase)
                  (part ?PHRASE1 ?SENTENCE)
                  (part ?PHRASE2 ?SENTENCE))))

If text is an instance of text, then there exists proposition prop so that text contains information prop.

(=>
      (instance ?TEXT Text)
      (exists
            (?PROP)
            (and
                  (instance ?PROP Proposition)
                  (containsInformation ?TEXT ?PROP))))

If text is an instance of text, then there exists sentence part so that part is a part of text.

(=>
      (instance ?TEXT Text)
      (exists
            (?PART)
            (and
                  (part ?PART ?TEXT)
                  (instance ?PART Sentence))))

If text is an instance of text, then there exists writing write so that text is a result of write.

(=>
      (instance ?TEXT Text)
      (exists
            (?WRITE)
            (and
                  (instance ?WRITE Writing)
                  (result ?WRITE ?TEXT))))

If sent is an instance of sentence, then there exist noun phrase noun,verb phrase verb so that noun is a part of sent and verb is a part of sent.

(=>
      (instance ?SENT Sentence)
      (exists
            (?NOUN ?VERB)
            (and
                  (instance ?NOUN NounPhrase)
                  (instance ?VERB VerbPhrase)
                  (part ?NOUN ?SENT)
                  (part ?VERB ?SENT))))

If agent is the author of text, then there exist process,text instance so that process is an agent of agent and text is a result of process.

(=>
      (authors ?AGENT ?TEXT)
      (exists
            (?PROCESS ?INSTANCE)
            (and
                  (agent ?PROCESS ?AGENT)
                  (instance ?INSTANCE ?TEXT)
                  (result ?PROCESS ?TEXT))))

If "edition int1 of text" is equal to edition1 and "edition int2 of text" is equal to edition2 and int2 is greater than int1 and pub1 is an instance of publication and pub2 is an instance of publication and edition1 is a patient of pub1 and edition2 is a patient of pub2 and date of pub1 is date1 and date of pub2 is date2, then "the end of date1" happen?{s} before "the end of date2".

(=>
      (and
            (equal
                  (EditionFn ?TEXT ?INT1)
                  ?EDITION1)
            (equal
                  (EditionFn ?TEXT ?INT2)
                  ?EDITION2)
            (greaterThan ?INT2 ?INT1)
            (instance ?PUB1 Publication)
            (instance ?PUB2 Publication)
            (patient ?PUB1 ?EDITION1)
            (patient ?PUB2 ?EDITION2)
            (date ?PUB1 ?DATE1)
            (date ?PUB2 ?DATE2))
      (before
            (EndFn ?DATE1)
            (EndFn ?DATE2)))

If "edition number of text1" is equal to text2, then text1 subsumes the content of text2.

(=>
      (equal
            (EditionFn ?TEXT1 ?NUMBER)
            ?TEXT2)
      (subsumesContentClass ?TEXT1 ?TEXT2))

If text is a subclass of periodical and "volume int1 in the series text" is equal to volume1 and "volume int2 in the series text" is equal to volume2 and int2 is greater than int1 and pub1 is an instance of publication and pub2 is an instance of publication and volume1 is a patient of pub1 and volume2 is a patient of pub2 and date of pub1 is date1 and date of pub2 is date2, then "the end of date1" happen?{s} before "the end of date2".

(=>
      (and
            (subclass ?TEXT Periodical)
            (equal
                  (SeriesVolumeFn ?TEXT ?INT1)
                  ?VOLUME1)
            (equal
                  (SeriesVolumeFn ?TEXT ?INT2)
                  ?VOLUME2)
            (greaterThan ?INT2 ?INT1)
            (instance ?PUB1 Publication)
            (instance ?PUB2 Publication)
            (patient ?PUB1 ?VOLUME1)
            (patient ?PUB2 ?VOLUME2)
            (date ?PUB1 ?DATE1)
            (date ?PUB2 ?DATE2))
      (before
            (EndFn ?DATE1)
            (EndFn ?DATE2)))

If "volume number in the series series" is equal to volume, then series subsumes the content of volume.

(=>
      (equal
            (SeriesVolumeFn ?SERIES ?NUMBER)
            ?VOLUME)
      (subsumesContentClass ?SERIES ?VOLUME))

If "the periodical number number of periodical" is equal to issue, then periodical subsumes the content of issue.

(=>
      (equal
            (PeriodicalIssueFn ?PERIODICAL ?NUMBER)
            ?ISSUE)
      (subsumesContentClass ?PERIODICAL ?ISSUE))

If text is an instance of summary, then there exists text text2 so that text2 subsumes the content of text.

(=>
      (instance ?TEXT Summary)
      (exists
            (?TEXT2)
            (and
                  (instance ?TEXT2 Text)
                  (subsumesContentInstance ?TEXT2 ?TEXT))))

If series is an instance of series, then there exist book book1,book book2 so that series subsumes the content of book1 and series subsumes the content of book2 and book1 is not equal to book2.

(=>
      (instance ?SERIES Series)
      (exists
            (?BOOK1 ?BOOK2)
            (and
                  (instance ?BOOK1 Book)
                  (instance ?BOOK2 Book)
                  (subsumesContentInstance ?SERIES ?BOOK1)
                  (subsumesContentInstance ?SERIES ?BOOK2)
                  (not
                        (equal ?BOOK1 ?BOOK2)))))

If article is an instance of article, then there exists book book so that book subsumes the content of article.

(=>
      (instance ?ARTICLE Article)
      (exists
            (?BOOK)
            (and
                  (instance ?BOOK Book)
                  (subsumesContentInstance ?BOOK ?ARTICLE))))

If doc is an instance of certificate and agent posesses doc, then there exists proc so that doc allows agent to perform task of the type proc or doc obligates agent to perform task of the type proc.

(=>
      (and
            (instance ?DOC Certificate)
            (possesses ?AGENT ?DOC))
      (exists
            (?PROC)
            (or
                  (confersRight ?PROC ?DOC ?AGENT)
                  (confersObligation ?PROC ?DOC ?AGENT))))

If mole is an instance of molecule, then there exist atom atom1,atom atom2 so that atom1 is a part of mole and atom2 is a part of mole and atom1 is not equal to atom2.

(=>
      (instance ?MOLE Molecule)
      (exists
            (?ATOM1 ?ATOM2)
            (and
                  (instance ?ATOM1 Atom)
                  (instance ?ATOM2 Atom)
                  (part ?ATOM1 ?MOLE)
                  (part ?ATOM2 ?MOLE)
                  (not
                        (equal ?ATOM1 ?ATOM2)))))

If product is an instance of product, then there exists manufacture manufacture so that product is a result of manufacture.

(=>
      (instance ?PRODUCT Product)
      (exists
            (?MANUFACTURE)
            (and
                  (instance ?MANUFACTURE Manufacture)
                  (result ?MANUFACTURE ?PRODUCT))))

If artifact1 is a version of artifact2, then artifact1 is a subclass of artifact2.

(=>
      (version ?ARTIFACT1 ?ARTIFACT2)
      (subclass ?ARTIFACT1 ?ARTIFACT2))

if artifact is an instance of stationary artifact,
then there exists place so that for all time holds: if time happen?{s} before or at "the end of "the time of existence of artifact"" and "the beginning of "the time of existence of artifact"" happen?{s} before or at time, then "the place where artifact was at time" is equal to place

(=>
      (instance ?ARTIFACT StationaryArtifact)
      (exists
            (?PLACE)
            (forall
                  (?TIME)
                  (=>
                        (and
                              (beforeOrEqual
                                    ?TIME
                                    (EndFn
                                          (WhenFn ?ARTIFACT)))
                              (beforeOrEqual
                                    (BeginFn
                                          (WhenFn ?ARTIFACT))
                                    ?TIME))
                        (equal
                              (WhereFn ?ARTIFACT ?TIME)
                              ?PLACE)))))

If building is an instance of building, then there exists human human so that

human lives in building
there exists act so that act is an agent of human and act is located at building

(=>
      (instance ?BUILDING Building)
      (exists
            (?HUMAN)
            (and
                  (instance ?HUMAN Human)
                  (or
                        (inhabits ?HUMAN ?BUILDING)
                        (exists
                              (?ACT)
                              (and
                                    (agent ?ACT ?HUMAN)
                                    (located ?ACT ?BUILDING)))))))

If room is an instance of room, then there exists building build so that room is a properPart of build.

(=>
      (instance ?ROOM Room)
      (exists
            (?BUILD)
            (and
                  (instance ?BUILD Building)
                  (properPart ?ROOM ?BUILD))))

If clothing is an instance of clothing, then there exists fabric fabric so that fabric is a part of clothing.

(=>
      (instance ?CLOTHING Clothing)
      (exists
            (?FABRIC)
            (and
                  (instance ?FABRIC Fabric)
                  (part ?FABRIC ?CLOTHING))))

If device is an instance of device, then there exists process proc so that device is capable to do proc in role instrument.

(=>
      (instance ?DEVICE Device)
      (exists
            (?PROC)
            (and
                  (subclass ?PROC Process)
                  (capability ?PROC instrument ?DEVICE))))

If device is an instance of device, then there exists process proc so that device has purpose "device is capable to do proc in role instrument".

(=>
      (instance ?DEVICE Device)
      (exists
            (?PROC)
            (and
                  (subclass ?PROC Process)
                  (hasPurpose
                        ?DEVICE
                        (capability ?PROC instrument ?DEVICE)))))

If instrument is an instance of musical instrument, then instrument is capable to do music in role instrument.

(=>
      (instance ?INSTRUMENT MusicalInstrument)
      (capability Music instrument ?INSTRUMENT))

If device is an instance of transportation device, then device is capable to do transportation in role instrument.

(=>
      (instance ?DEVICE TransportationDevice)
      (capability Transportation instrument ?DEVICE))

If weapon is an instance of weapon, then weapon is capable to do damaging in role instrument.

(=>
      (instance ?WEAPON Weapon)
      (capability Damaging instrument ?WEAPON))

If weapon is an instance of weapon, then weapon has purpose "there exist damaging dest,patient so that patient is a patient of dest and

patient is an instance of stationary artifact
patient is an instance of animal
there exists animal animal so that animal lives in patient

(=>
      (instance ?WEAPON Weapon)
      (hasPurpose
            ?WEAPON
            (exists
                  (?DEST ?PATIENT)
                  (and
                        (instance ?DEST Damaging)
                        (patient ?DEST ?PATIENT)
                        (or
                              (instance ?PATIENT StationaryArtifact)
                              (instance ?PATIENT Animal)
                              (exists
                                    (?ANIMAL)
                                    (and
                                          (instance ?ANIMAL Animal)
                                          (inhabits ?ANIMAL ?PATIENT))))))))

if machine is an instance of machine,
then for all proc holds: if machine is an instrument for proc, then there exist resource,result so that resource is a resource for proc and result is a result of proc

(=>
      (instance ?MACHINE Machine)
      (forall
            (?PROC)
            (=>
                  (instrument ?PROC ?MACHINE)
                  (exists
                        (?RESOURCE ?RESULT)
                        (and
                              (resource ?PROC ?RESOURCE)
                              (result ?PROC ?RESULT))))))

If comp is an instance of engineering component, then there exists device device so that comp is a component of device.

(=>
      (instance ?COMP EngineeringComponent)
      (exists
            (?DEVICE)
            (and
                  (instance ?DEVICE Device)
                  (component ?COMP ?DEVICE))))

If comp1 is connected to comp2, then comp1 is a component of comp2 and comp2 is a component of comp1.

(=>
      (connectedEngineeringComponents ?COMP1 ?COMP2)
      (and
            (not
                  (engineeringSubcomponent ?COMP1 ?COMP2))
            (not
                  (engineeringSubcomponent ?COMP2 ?COMP1))))

If comp1 is connected to comp2, then comp1 is not an instance of engineering connection and comp2 is not an instance of engineering connection.

(=>
      (connectedEngineeringComponents ?COMP1 ?COMP2)
      (not
            (or
                  (instance ?COMP1 EngineeringConnection)
                  (instance ?COMP2 EngineeringConnection))))

If connection is an instance of engineering connection, then there exist comp1,comp2 so that connection connects comp1 and comp2.

(=>
      (instance ?CONNECTION EngineeringConnection)
      (exists
            (?COMP1 ?COMP2)
            (connectsEngineeringComponents ?CONNECTION ?COMP1 ?COMP2)))

If group is an instance of group and memb is a member of group, then memb is an instance of agent.

(=>
      (and
            (instance ?GROUP Group)
            (member ?MEMB ?GROUP))
      (instance ?MEMB Agent))

if group is an instance of age group,
then for all memb1,memb2,age1,age2 holds: if memb1 is a member of group and memb2 is a member of group and the age of memb1 is age1 and the age of memb2 is age2, then age1 is equal to age2

(=>
      (instance ?GROUP AgeGroup)
      (forall
            (?MEMB1 ?MEMB2 ?AGE1 ?AGE2)
            (=>
                  (and
                        (member ?MEMB1 ?GROUP)
                        (member ?MEMB2 ?GROUP)
                        (age ?MEMB1 ?AGE1)
                        (age ?MEMB2 ?AGE2))
                  (equal ?AGE1 ?AGE2))))

if group is an instance of family group,
then for all memb1,memb2 holds: if memb1 is a member of group and memb2 is a member of group, then memb1 and memb2 are related

(=>
      (instance ?GROUP FamilyGroup)
      (forall
            (?MEMB1 ?MEMB2)
            (=>
                  (and
                        (member ?MEMB1 ?GROUP)
                        (member ?MEMB2 ?GROUP))
                  (familyRelation ?MEMB1 ?MEMB2))))

If organism1 and organism2 are related, then there exists organism3 so that organism3 and organism1 are related and organism3 and organism2 are related.

(=>
      (familyRelation ?ORGANISM1 ?ORGANISM2)
      (exists
            (?ORGANISM3)
            (and
                  (familyRelation ?ORGANISM3 ?ORGANISM1)
                  (familyRelation ?ORGANISM3 ?ORGANISM2))))

If "the legal organizational entity of unit" is equal to org and attr is an instance of normative attribute, then attr is an attribute of unit if and only if attr is an attribute of org.

(=>
      (and
            (equal
                  (OrganizationFn ?UNIT)
                  ?ORG)
            (instance ?ATTR NormativeAttribute))
      (<=>
            (attribute ?UNIT ?ATTR)
            (attribute ?ORG ?ATTR)))

If org employs person, then person is a member of org.

(=>
      (employs ?ORG ?PERSON)
      (member ?PERSON ?ORG))

If pol is an instance of political organization, then there exists political process proc so that proc is an agent of pol.

(=>
      (instance ?POL PoliticalOrganization)
      (exists
            (?PROC)
            (and
                  (instance ?PROC PoliticalProcess)
                  (agent ?PROC ?POL))))

If plan is an instance of plan and obj is an instance of content bearing object and obj contains information plan, then there exists planning planning so that obj is a result of planning.

(=>
      (and
            (instance ?PLAN Plan)
            (instance ?OBJ ContentBearingObject)
            (containsInformation ?OBJ ?PLAN))
      (exists
            (?PLANNING)
            (and
                  (instance ?PLANNING Planning)
                  (result ?PLANNING ?OBJ))))

If plan is an instance of plan, then there exists purp so that plan has purpose purp.

(=>
      (instance ?PLAN Plan)
      (exists
            (?PURP)
            (hasPurpose ?PLAN ?PURP)))

If obj1 is attr1 to obj2 and is opposed to ? and attr1 is a member of "()" and attr2 is a member of "()" and attr1 is not equal to attr2, then obj1 is not attr2 to obj2.

(=>
      (and
            (orientation ?OBJ1 ?OBJ2 ?ATTR1)
            (contraryAttribute @ROW)
            (inList
                  ?ATTR1
                  (ListFn @ROW))
            (inList
                  ?ATTR2
                  (ListFn @ROW))
            (not
                  (equal ?ATTR1 ?ATTR2)))
      (not
            (orientation ?OBJ1 ?OBJ2 ?ATTR2)))

if entities in the process proc are moving attr1 during time,
then for all attr2 holds: if entities in the process proc are moving attr2 during time, then attr2 is equal to attr1

(=>
      (holdsDuring
            ?TIME
            (direction ?PROC ?ATTR1))
      (forall
            (?ATTR2)
            (=>
                  (holdsDuring
                        ?TIME
                        (direction ?PROC ?ATTR2))
                  (equal ?ATTR2 ?ATTR1))))

if proc faces attr1 during time,
then for all attr2 holds: if proc faces attr2 during time, then attr2 is equal to attr1

(=>
      (holdsDuring
            ?TIME
            (faces ?PROC ?ATTR1))
      (forall
            (?ATTR2)
            (=>
                  (holdsDuring
                        ?TIME
                        (faces ?PROC ?ATTR2))
                  (equal ?ATTR2 ?ATTR1))))

If item has an attribute value and value is an instance of truth value, then item is an instance of sentence or item is an instance of proposition.

(=>
      (and
            (property ?ITEM ?VALUE)
            (instance ?VALUE TruthValue))
      (or
            (instance ?ITEM Sentence)
            (instance ?ITEM Proposition)))

If formula has an attribute likely, then "the probability of "formula is true"" is greater than "the probability of "formula is false"".

(=>
      (property ?FORMULA Likely)
      (greaterThan
            (ProbabilityFn
                  (true ?FORMULA True))
            (ProbabilityFn
                  (true ?FORMULA False))))

If formula has an attribute unlikely, then "the probability of "formula is false"" is greater than "the probability of "formula is true"".

(=>
      (property ?FORMULA Unlikely)
      (greaterThan
            (ProbabilityFn
                  (true ?FORMULA False))
            (ProbabilityFn
                  (true ?FORMULA True))))

If obj1 is attr1 to obj2 and attr1 is an instance of directional attribute and attr2 is an instance of directional attribute and attr1 is not equal to attr2, then obj1 is not attr2 to obj2.

(=>
      (and
            (orientation ?OBJ1 ?OBJ2 ?ATTR1)
            (instance ?ATTR1 DirectionalAttribute)
            (instance ?ATTR2 DirectionalAttribute)
            (not
                  (equal ?ATTR1 ?ATTR2)))
      (not
            (orientation ?OBJ1 ?OBJ2 ?ATTR2)))

If direct is an instance of directional attribute and obj1 is direct to obj2 and obj2 is direct to obj3, then obj2 is between obj1 and obj33.

(=>
      (and
            (instance ?DIRECT DirectionalAttribute)
            (orientation ?OBJ1 ?OBJ2 ?DIRECT)
            (orientation ?OBJ2 ?OBJ3 ?DIRECT))
      (between ?OBJ1 ?OBJ2 ?OBJ33))

If obj1 is above to obj2, then obj1 is not connected to obj2.

(=>
      (orientation ?OBJ1 ?OBJ2 Above)
      (not
            (connected ?OBJ1 ?OBJ2)))

If obj1 is below to obj2, then obj2 is on to obj1 or obj2 is above to obj1.

(=>
      (orientation ?OBJ1 ?OBJ2 Below)
      (or
            (orientation ?OBJ2 ?OBJ1 On)
            (orientation ?OBJ2 ?OBJ1 Above)))

If obj1 is adjacent to obj2, then obj1 is near to obj2 or obj1 is connected to obj2.

(=>
      (orientation ?OBJ1 ?OBJ2 Adjacent)
      (or
            (orientation ?OBJ1 ?OBJ2 Near)
            (connected ?OBJ1 ?OBJ2)))

If obj1 is near to obj2, then obj1 is not connected to obj2.

(=>
      (orientation ?OBJ1 ?OBJ2 Near)
      (not
            (connected ?OBJ1 ?OBJ2)))

If obj1 is near to obj2, then obj2 is near to obj1.

(=>
      (orientation ?OBJ1 ?OBJ2 Near)
      (orientation ?OBJ2 ?OBJ1 Near))

If obj1 is on to obj2, then obj1 is connected to obj2.

(=>
      (orientation ?OBJ1 ?OBJ2 On)
      (connected ?OBJ1 ?OBJ2))

If obj1 is on to obj2, then obj1 is located at obj2.

(=>
      (orientation ?OBJ1 ?OBJ2 On)
      (located ?OBJ1 ?OBJ2))

If obj1 is on to obj2, then obj2 is not on to obj1.

(=>
      (orientation ?OBJ1 ?OBJ2 On)
      (not
            (orientation ?OBJ2 ?OBJ1 On)))

If "relative time fn(time1,pacific time zone)" is equal to time2, then time2 is equal to "(time1+)".

(=>
      (equal
            (RelativeTimeFn ?TIME1 PacificTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 8)))

If "relative time fn(time1,mountain time zone)" is equal to time2, then time2 is equal to "(time1+)".

(=>
      (equal
            (RelativeTimeFn ?TIME1 MountainTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 7)))

If "relative time fn(time1,central time zone)" is equal to time2, then time2 is equal to "(time1+)".

(=>
      (equal
            (RelativeTimeFn ?TIME1 CentralTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 6)))

If "relative time fn(time1,eastern time zone)" is equal to time2, then time2 is equal to "(time1+)".

(=>
      (equal
            (RelativeTimeFn ?TIME1 EasternTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 5)))

If attribute is an attribute of person and attribute is an instance of social role, then person is an instance of human.

(=>
      (and
            (attribute ?PERSON ?ATTRIBUTE)
            (instance ?ATTRIBUTE SocialRole))
      (instance ?PERSON Human))

If org employs person, then there exists position so that person holds the position of position in org.

(=>
      (employs ?ORG ?PERSON)
      (exists
            (?POSITION)
            (occupiesPosition ?PERSON ?POSITION ?ORG)))

If the statement formula1 has the model force of prop and formula1 entails formula2, then the statement formula2 has the model force of prop.

(=>
      (and
            (modalAttribute ?FORMULA1 ?PROP)
            (entails ?FORMULA1 ?FORMULA2))
      (modalAttribute ?FORMULA2 ?PROP))

If agent is obliged to perform tasks of type process, then the statement "there exists process instance so that instance is an agent of agent" has the model force of obligation.

(=>
      (holdsObligation ?PROCESS ?AGENT)
      (modalAttribute
            (exists
                  (?INSTANCE)
                  (and
                        (instance ?INSTANCE ?PROCESS)
                        (agent ?INSTANCE ?AGENT)))
            Obligation))

If agent has the right to perform process, then the statement "there exists process instance so that instance is an agent of agent" has the model force of permission.

(=>
      (holdsRight ?PROCESS ?AGENT)
      (modalAttribute
            (exists
                  (?INSTANCE)
                  (and
                        (instance ?INSTANCE ?PROCESS)
                        (agent ?INSTANCE ?AGENT)))
            Permission))

If attr is an attribute of obj and attr is an instance of contest attribute, then there exists contest contest so that contest is an agent of obj or obj is a patient of contest.

(=>
      (and
            (attribute ?OBJ ?ATTR)
            (instance ?ATTR ContestAttribute))
      (exists
            (?CONTEST)
            (and
                  (instance ?CONTEST Contest)
                  (or
                        (agent ?CONTEST ?OBJ)
                        (patient ?CONTEST ?OBJ)))))

If the statement formula has the model force of necessity, then the statement formula has the model force of possibility.

(=>
      (modalAttribute ?FORMULA Necessity)
      (modalAttribute ?FORMULA Possibility))

If the statement formula has the model force of obligation, then the statement formula has the model force of permission.

(=>
      (modalAttribute ?FORMULA Obligation)
      (modalAttribute ?FORMULA Permission))

If entity has an attribute promise, then entity has an attribute contract or entity has an attribute naked promise.

(=>
      (property ?ENTITY Promise)
      (or
            (property ?ENTITY Contract)
            (property ?ENTITY NakedPromise)))

If obj is an instance of solution, then liquid is an attribute of obj.

(=>
      (instance ?OBJ Solution)
      (attribute ?OBJ Liquid))

If perception is an instance of perception and obj is a patient of perception, then there exists perceptual attribute prop so that prop is an attribute of obj.

(=>
      (and
            (instance ?PERCEPTION Perception)
            (patient ?PERCEPTION ?OBJ))
      (exists
            (?PROP)
            (and
                  (instance ?PROP PerceptualAttribute)
                  (attribute ?OBJ ?PROP))))

If obj is an instance of food, then there exists taste attribute attr so that attr is an attribute of obj.

(=>
      (instance ?OBJ Food)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR TasteAttribute)
                  (attribute ?OBJ ?ATTR))))

if monochromatic is an attribute of obj and part is a superficial part of obj and color is an attribute of part and color is an instance of primary color,
then for all element holds: if element is a superficial part of obj, then color is an attribute of element

(=>
      (and
            (attribute ?OBJ Monochromatic)
            (superficialPart ?PART ?OBJ)
            (attribute ?PART ?COLOR)
            (instance ?COLOR PrimaryColor))
      (forall
            (?ELEMENT)
            (=>
                  (superficialPart ?ELEMENT ?OBJ)
                  (attribute ?ELEMENT ?COLOR))))

If obj is an instance of object, then monochromatic is an attribute of obj or polychromatic is an attribute of obj.

(=>
      (instance ?OBJ Object)
      (or
            (attribute ?OBJ Monochromatic)
            (attribute ?OBJ Polychromatic)))

If polychromatic is an attribute of obj, then there exist part1,part2,color attribute color1,color attribute color2 so that part1 is a superficial part of obj and part2 is a superficial part of obj and color1 is an attribute of part1 and color2 is an attribute of part2 and color1 is not equal to color2.

(=>
      (attribute ?OBJ Polychromatic)
      (exists
            (?PART1 ?PART2 ?COLOR1 ?COLOR2)
            (and
                  (superficialPart ?PART1 ?OBJ)
                  (superficialPart ?PART2 ?OBJ)
                  (attribute ?PART1 ?COLOR1)
                  (attribute ?PART2 ?COLOR2)
                  (instance ?COLOR1 ColorAttribute)
                  (instance ?COLOR2 ColorAttribute)
                  (not
                        (equal ?COLOR1 ?COLOR2)))))

If there exists shape change change so that obj is a patient of change, then pliable is an attribute of obj.

(=>
      (exists
            (?CHANGE)
            (and
                  (instance ?CHANGE ShapeChange)
                  (patient ?CHANGE ?OBJ)))
      (attribute ?OBJ Pliable))

If obj is an instance of self connected object, then pliable is an attribute of obj or rigid is an attribute of obj.

(=>
      (instance ?OBJ SelfConnectedObject)
      (or
            (attribute ?OBJ Pliable)
            (attribute ?OBJ Rigid)))

If attribute is an instance of texture attribute and attribute is an attribute of obj and surface is a surface of obj, then attribute is an attribute of surface.

(=>
      (and
            (instance ?ATTRIBUTE TextureAttribute)
            (attribute ?OBJ ?ATTRIBUTE)
            (surface ?SURFACE ?OBJ))
      (attribute ?SURFACE ?ATTRIBUTE))

If dry is an attribute of obj, then there doesn't exist subobj so that subobj is a part of obj and liquid is an attribute of subobj.

(=>
      (attribute ?OBJ Dry)
      (not
            (exists
                  (?SUBOBJ)
                  (and
                        (part ?SUBOBJ ?OBJ)
                        (attribute ?SUBOBJ Liquid)))))

if wet is an attribute of obj,
then for all part holds: if part is a part of obj, then there exists subpart so that subpart is a part of part and liquid is an attribute of subpart

(=>
      (attribute ?OBJ Wet)
      (forall
            (?PART)
            (=>
                  (part ?PART ?OBJ)
                  (exists
                        (?SUBPART)
                        (and
                              (part ?SUBPART ?PART)
                              (attribute ?SUBPART Liquid))))))

If unbreakable is an attribute of obj, then there doesn't exist damaging damage so that obj is a patient of damage.

(=>
      (attribute ?OBJ Unbreakable)
      (not
            (exists
                  (?DAMAGE)
                  (and
                        (instance ?DAMAGE Damaging)
                        (patient ?DAMAGE ?OBJ)))))

If att is an attribute of org and att is an instance of biological attribute, then org is an instance of organism.

(=>
      (and
            (attribute ?ORG ?ATT)
            (instance ?ATT BiologicalAttribute))
      (instance ?ORG Organism))

If organism is an instance of organism and process is an agent of organism, then living is an attribute of organism the time of existence of process.

(=>
      (and
            (instance ?ORGANISM Organism)
            (agent ?PROCESS ?ORGANISM))
      (holdsDuring
            (WhenFn ?PROCESS)
            (attribute ?ORGANISM Living)))

If org is an instance of organism, then there exists animacy attribute attr so that attr is an attribute of org.

(=>
      (instance ?ORG Organism)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR AnimacyAttribute)
                  (attribute ?ORG ?ATTR))))

If body is an instance of reproductive body and body is a part of org and org is an instance of organism, then female is an attribute of org.

(=>
      (and
            (instance ?BODY ReproductiveBody)
            (part ?BODY ?ORG)
            (instance ?ORG Organism))
      (attribute ?ORG Female))

If animal is an instance of animal, then there exists sex attribute attr so that attr is an attribute of animal.

(=>
      (instance ?ANIMAL Animal)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR SexAttribute)
                  (attribute ?ANIMAL ?ATTR))))

If fully formed is an attribute of obj, then there exists growth growth so that obj experiences growth and non fully formed is an attribute of obj the beginning of "the time of existence of obj".

(=>
      (attribute ?OBJ FullyFormed)
      (exists
            (?GROWTH)
            (and
                  (instance ?GROWTH Growth)
                  (experiencer ?GROWTH ?OBJ)
                  (holdsDuring
                        (BeginFn
                              (WhenFn ?OBJ))
                        (attribute ?OBJ NonFullyFormed)))))

If org is an instance of organism, then there exists developmental attribute attr so that attr is an attribute of org.

(=>
      (instance ?ORG Organism)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR DevelopmentalAttribute)
                  (attribute ?ORG ?ATTR))))

If larval is an attribute of org during time, then there exists birth birth so that org experiences birth before time.

(=>
      (holdsDuring
            ?TIME
            (attribute ?ORG Larval))
      (holdsDuring
            (PastFn ?TIME)
            (exists
                  (?BIRTH)
                  (and
                        (instance ?BIRTH Birth)
                        (experiencer ?BIRTH ?ORG)))))

If embryonic is an attribute of org, then there exists reproductive body body so that org is located at body.

(=>
      (attribute ?ORG Embryonic)
      (exists
            (?BODY)
            (and
                  (instance ?BODY ReproductiveBody)
                  (located ?ORG ?BODY))))

If embryonic is an attribute of org during time, then there doesn't exist birth birth so that org experiences birth during time.

(=>
      (holdsDuring
            ?TIME
            (attribute ?ORG Embryonic))
      (holdsDuring
            ?TIME
            (not
                  (exists
                        (?BIRTH)
                        (and
                              (instance ?BIRTH Birth)
                              (experiencer ?BIRTH ?ORG))))))

if attr is an instance of psychological attribute,
then if attr is an attribute of organism during time, then living is an attribute of organism during time

(=>
      (instance ?ATTR PsychologicalAttribute)
      (=>
            (holdsDuring
                  ?TIME
                  (attribute ?ORGANISM ?ATTR))
            (holdsDuring
                  ?TIME
                  (attribute ?ORGANISM Living))))

If attr is an instance of psychological attribute and attr is an attribute of agent, then agent is an instance of sentient agent.

(=>
      (and
            (instance ?ATTR PsychologicalAttribute)
            (attribute ?AGENT ?ATTR))
      (instance ?AGENT SentientAgent))

If class1 is an instance of set or class and class2 is an instance of set or class, then "the difference between class1 and class2" is equal to "the union of class1 and "the complement of class2"".

(=>
      (and
            (instance ?CLASS1 SetOrClass)
            (instance ?CLASS2 SetOrClass))
      (equal
            (RelativeComplementFn ?CLASS1 ?CLASS2)
            (IntersectionFn
                  ?CLASS1
                  (ComplementFn ?CLASS2))))

entity is an instance of "the intersection of all the elements of superclass" if and only if for all class holds: if class is an instance of superclass, then entity is an instance of class.

(<=>
      (instance
            ?ENTITY
            (GeneralizedIntersectionFn ?SUPERCLASS))
      (forall
            (?CLASS)
            (=>
                  (instance ?CLASS ?SUPERCLASS)
                  (instance ?ENTITY ?CLASS))))