Select language: english | cesky | deutsch | italiano | simplified chinese | traditional chinese | hindi
Concept:
English word:
Home

and (and)

The truth-functional connective of conjunction.

Ontology

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

OperatoreLogico
is instance of
  and  

Coordinate term(s)

<=>  =>  entails  exists  forall  not  or 

Type restrictions

and(Formula, Formula)

Related WordNet synsets

See more related synsets on a separate page.

Axioms (483)

Se ?é una istanza immediata class, allora non esiste class subclass tale che entity é un' istanza di subclass.
(=>
      (immediateInstance ?ENTITY ?CLASS)
      (not
            (exists
                  (?SUBCLASS)
                  (and
                        (subclass ?SUBCLASS ?CLASS)
                        (instance ?ENTITY ?SUBCLASS)))))

subclass é una sottoclasse di class se e solo se
(<=>
      (subclass ?SUBCLASS ?CLASS)
      (and
            (instance ?SUBCLASS SetOrClass)
            (instance ?CLASS SetOrClass)
            (forall
                  (?INST)
                  (=>
                        (instance ?INST ?SUBCLASS)
                        (instance ?INST ?CLASS)))))

Se class1 é una sottoclasse immediata di class2, allora non esiste class2 class3 tale che class1 é una sottoclasse di class3 e class2 is not uguale a class3 e class1 is not uguale a class3.
(=>
      (immediateSubclass ?CLASS1 ?CLASS2)
      (not
            (exists
                  (?CLASS3)
                  (and
                        (subclass ?CLASS3 ?CLASS2)
                        (subclass ?CLASS1 ?CLASS3)
                        (not
                              (equal ?CLASS2 ?CLASS3))
                        (not
                              (equal ?CLASS1 ?CLASS3))))))

Se pred1 é una sottorelazione di pred2 e pred1 %&ha number argomento(s, allora pred2 %&ha number argomento(s.
(=>
      (and
            (subrelation ?PRED1 ?PRED2)
            (valence ?PRED1 ?NUMBER))
      (valence ?PRED2 ?NUMBER))

Se pred1 é una sottorelazione di pred2 e il numero number argomenti di pred2 é un istanza di class1, allora il numero number argomenti di pred1 é un istanza di class1.
(=>
      (and
            (subrelation ?PRED1 ?PRED2)
            (domain ?PRED2 ?NUMBER ?CLASS1))
      (domain ?PRED1 ?NUMBER ?CLASS1))

Se rel1 é una sottorelazione di rel2 e rel1( vales, allora rel2( vales.
(=>
      (and
            (subrelation ?REL1 ?REL2)
            (holds ?REL1 @ROW))
      (holds ?REL2 @ROW))

Se pred1 é una sottorelazione di pred2 e pred2 é un' istanza di class e class é un' istanza di inheritable relation, allora pred1 é un' istanza di class.
(=>
      (and
            (subrelation ?PRED1 ?PRED2)
            (instance ?PRED2 ?CLASS)
            (instance ?CLASS InheritableRelation))
      (instance ?PRED1 ?CLASS))

Se il numero number argomenti di rel é un istanza di class1 e il numero number argomenti di rel é un istanza di class2, allora class1 é una sottoclasse di class2 o class2 é una sottoclasse di class1.
(=>
      (and
            (domain ?REL ?NUMBER ?CLASS1)
            (domain ?REL ?NUMBER ?CLASS2))
      (or
            (subclass ?CLASS1 ?CLASS2)
            (subclass ?CLASS2 ?CLASS1)))

Se rel1 é una sottorelazione di rel2 e il numero number argomento rel2 é una sottoclasse diclass1, allora il numero number argomento rel1 é una sottoclasse diclass1.
(=>
      (and
            (subrelation ?REL1 ?REL2)
            (domainSubclass ?REL2 ?NUMBER ?CLASS1))
      (domainSubclass ?REL1 ?NUMBER ?CLASS1))

Se il numero number argomento rel é una sottoclasse diclass1 e il numero number argomento rel é una sottoclasse diclass2, allora class1 é una sottoclasse di class2 o class2 é una sottoclasse di class1.
(=>
      (and
            (domainSubclass ?REL ?NUMBER ?CLASS1)
            (domainSubclass ?REL ?NUMBER ?CLASS2))
      (or
            (subclass ?CLASS1 ?CLASS2)
            (subclass ?CLASS2 ?CLASS1)))

(=>
      (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))))

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

Se rango di function é un'istanza di class e "function(" is uguale a value, allora value é un' istanza di class.
(=>
      (and
            (range ?FUNCTION ?CLASS)
            (equal
                  (AssignmentFn ?FUNCTION @ROW)
                  ?VALUE))
      (instance ?VALUE ?CLASS))

Se rel1 é una sottorelazione di rel2 e rango di rel2 é un'istanza di class1, allora rango di rel1 é un'istanza di class1.
(=>
      (and
            (subrelation ?REL1 ?REL2)
            (range ?REL2 ?CLASS1))
      (range ?REL1 ?CLASS1))

Se rango di rel é un'istanza di class1 e rango di rel é un'istanza di class2, allora class1 é una sottoclasse di class2 o class2 é una sottoclasse di class1.
(=>
      (and
            (range ?REL ?CLASS1)
            (range ?REL ?CLASS2))
      (or
            (subclass ?CLASS1 ?CLASS2)
            (subclass ?CLASS2 ?CLASS1)))

Se i valori resi da function sono sottoclassi diclass e "function(" is uguale a value, allora value é una sottoclasse di class.
(=>
      (and
            (rangeSubclass ?FUNCTION ?CLASS)
            (equal
                  (AssignmentFn ?FUNCTION @ROW)
                  ?VALUE))
      (subclass ?VALUE ?CLASS))

Se rel1 é una sottorelazione di rel2 e i valori resi da rel2 sono sottoclassi diclass1, allora i valori resi da rel1 sono sottoclassi diclass1.
(=>
      (and
            (subrelation ?REL1 ?REL2)
            (rangeSubclass ?REL2 ?CLASS1))
      (rangeSubclass ?REL1 ?CLASS1))

Se i valori resi da rel sono sottoclassi diclass1 e i valori resi da rel sono sottoclassi diclass2, allora class1 é una sottoclasse di class2 o class2 é una sottoclasse di class1.
(=>
      (and
            (rangeSubclass ?REL ?CLASS1)
            (rangeSubclass ?REL ?CLASS2))
      (or
            (subclass ?CLASS1 ?CLASS2)
            (subclass ?CLASS2 ?CLASS1)))

class1 é disgiunto da class2 se e solo se
(<=>
      (disjoint ?CLASS1 ?CLASS2)
      (and
            (instance ?CLASS1 SetOrClass)
            (instance ?CLASS2 SetOrClass)
            (forall
                  (?INST)
                  (not
                        (and
                              (instance ?INST ?CLASS1)
                              (instance ?INST ?CLASS2))))))

Se e ? sono disgiunti e rel é un é membro di "(", allora rel é un' istanza di Relazione.
(=>
      (and
            (disjointRelation @ROW)
            (inList
                  ?REL
                  (ListFn @ROW)))
      (instance ?REL Relation))

Se e ? sono disgiunti e rel1 é un é membro di "(" e rel2 é un é membro di "(" e rel1 %&ha number argomento(s, allora rel2 %&ha number argomento(s.
(=>
      (and
            (disjointRelation @ROW)
            (inList
                  ?REL1
                  (ListFn @ROW))
            (inList
                  ?REL2
                  (ListFn @ROW))
            (valence ?REL1 ?NUMBER))
      (valence ?REL2 ?NUMBER))

Se il numero number argomenti di rel1 é un istanza di class1 e il numero number argomenti di rel2 é un istanza di class2 e class1 é disgiunto da class2, allora rel1 e rel2 sono disgiunti.
(=>
      (and
            (domain ?REL1 ?NUMBER ?CLASS1)
            (domain ?REL2 ?NUMBER ?CLASS2)
            (disjoint ?CLASS1 ?CLASS2))
      (disjointRelation ?REL1 ?REL2))

Se il numero number argomento rel1 é una sottoclasse diclass1 e il numero number argomento rel2 é una sottoclasse diclass2 e class1 é disgiunto da class2, allora rel1 e rel2 sono disgiunti.
(=>
      (and
            (domainSubclass ?REL1 ?NUMBER ?CLASS1)
            (domainSubclass ?REL2 ?NUMBER ?CLASS2)
            (disjoint ?CLASS1 ?CLASS2))
      (disjointRelation ?REL1 ?REL2))

Se rango di rel1 é un'istanza di class1 e rango di rel2 é un'istanza di class2 e class1 é disgiunto da class2, allora rel1 e rel2 sono disgiunti.
(=>
      (and
            (range ?REL1 ?CLASS1)
            (range ?REL2 ?CLASS2)
            (disjoint ?CLASS1 ?CLASS2))
      (disjointRelation ?REL1 ?REL2))

Se i valori resi da rel1 sono sottoclassi diclass1 e i valori resi da rel2 sono sottoclassi diclass2 e class1 é disgiunto da class2, allora rel1 e rel2 sono disgiunti.
(=>
      (and
            (rangeSubclass ?REL1 ?CLASS1)
            (rangeSubclass ?REL2 ?CLASS2)
            (disjoint ?CLASS1 ?CLASS2))
      (disjointRelation ?REL1 ?REL2))

Se e ? sono disgiunti e rel1 é un é membro di "(" e rel2 é un é membro di "(" e rel1 is not uguale a rel2 e rel1( vales, allora rel2( non vale.
(=>
      (and
            (disjointRelation @ROW1)
            (inList
                  ?REL1
                  (ListFn @ROW1))
            (inList
                  ?REL2
                  (ListFn @ROW1))
            (not
                  (equal ?REL1 ?REL2))
            (holds ?REL1 @ROW2))
      (not
            (holds ?REL2 @ROW2)))

(=>
      (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))))))

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

é esaustivamente partizionato in se e solo se é coperto da e é scomposto disgiuntivamente in .
(<=>
      (partition @ROW)
      (and
            (exhaustiveDecomposition @ROW)
            (disjointDecomposition @ROW)))

Se attr1 é un sottoattributo di attr2 e attr2 é un' istanza di class, allora attr1 é un' istanza di class.
(=>
      (and
            (subAttribute ?ATTR1 ?ATTR2)
            (instance ?ATTR2 ?CLASS))
      (instance ?ATTR1 ?CLASS))

Se attr1 é un immediato attributo successore di attr2 e "entity ha un attributo attr2" vales durante time1, allora esiste time2 tale che time2 é una parte di"prima time1" e "entity ha un attributo attr1" vales durante time2.
(=>
      (and
            (successorAttribute ?ATTR1 ?ATTR2)
            (holdsDuring
                  ?TIME1
                  (property ?ENTITY ?ATTR2)))
      (exists
            (?TIME2)
            (and
                  (temporalPart
                        ?TIME2
                        (PastFn ?TIME1))
                  (holdsDuring
                        ?TIME2
                        (property ?ENTITY ?ATTR1)))))

Se rel(,inst vales e rel é un' istanza di Funzione, allora "rel(" is uguale a inst.
(=>
      (and
            (holds ?REL @ROW ?INST)
            (instance ?REL Function))
      (equal
            (AssignmentFn ?REL @ROW)
            ?INST))

phys é un' istanza di EntitáConcreta se e solo se esiste loc,time tale che phys é localizzato in loc e phys esistes durante time.
(<=>
      (instance ?PHYS Physical)
      (exists
            (?LOC ?TIME)
            (and
                  (located ?PHYS ?LOC)
                  (time ?PHYS ?TIME))))

obj1 é una Parte propria di obj2 se e solo se obj1 é una parte di obj2 e obj2 é not una parte di obj1.
(<=>
      (properPart ?OBJ1 ?OBJ2)
      (and
            (part ?OBJ1 ?OBJ2)
            (not
                  (part ?OBJ2 ?OBJ1))))

Se objecttype é una sottoclasse di Sostanza e object é un' istanza di objecttype e part é una parte di object, allora part é un' istanza di objecttype.
(=>
      (and
            (subclass ?OBJECTTYPE Substance)
            (instance ?OBJECT ?OBJECTTYPE)
            (part ?PART ?OBJECT))
      (instance ?PART ?OBJECTTYPE))

Se obj é un' istanza di Sostanza e attr is an attribute of obj e part é una parte di obj, allora attr is an attribute of part.
(=>
      (and
            (instance ?OBJ Substance)
            (attribute ?OBJ ?ATTR)
            (part ?PART ?OBJ))
      (attribute ?PART ?ATTR))

Se atom é un' istanza di Atomo, allora esiste Protone proton,Elettrone electron tale che proton é un componente diatom e electron é un componente diatom.
(=>
      (instance ?ATOM Atom)
      (exists
            (?PROTON ?ELECTRON)
            (and
                  (component ?PROTON ?ATOM)
                  (component ?ELECTRON ?ATOM)
                  (instance ?PROTON Proton)
                  (instance ?ELECTRON Electron))))

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

Se particle é un' istanza di ParticellaSubatomica, allora esiste Atomo atom tale che particle é una parte di atom.
(=>
      (instance ?PARTICLE SubatomicParticle)
      (exists
            (?ATOM)
            (and
                  (instance ?ATOM Atom)
                  (part ?PARTICLE ?ATOM))))

Se nucleus é un' istanza di NucleoAtomico, allora esiste Neutrone neutron,Protone proton tale che neutron é un componente dinucleus e proton é un componente dinucleus.
(=>
      (instance ?NUCLEUS AtomicNucleus)
      (exists
            (?NEUTRON ?PROTON)
            (and
                  (component ?NEUTRON ?NUCLEUS)
                  (component ?PROTON ?NUCLEUS)
                  (instance ?NEUTRON Neutron)
                  (instance ?PROTON Proton))))

Se mixture é un' istanza di Mistura, allora esiste SostanzaPura pure1,SostanzaPura pure2 tale che pure1 is not uguale a pure2 e pure1 é un membro di mixture e pure2 é un membro di mixture.
(=>
      (instance ?MIXTURE Mixture)
      (exists
            (?PURE1 ?PURE2)
            (and
                  (subclass ?PURE1 PureSubstance)
                  (subclass ?PURE2 PureSubstance)
                  (not
                        (equal ?PURE1 ?PURE2))
                  (piece ?PURE1 ?MIXTURE)
                  (piece ?PURE2 ?MIXTURE))))

Se obj é un' istanza di OggettoCorpuscolare, allora esiste Sostanza substance1,Sostanza substance2 tale che substance1 é fatto di obj e substance2 é fatto di obj e substance1 is not uguale a substance2.
(=>
      (instance ?OBJ CorpuscularObject)
      (exists
            (?SUBSTANCE1 ?SUBSTANCE2)
            (and
                  (subclass ?SUBSTANCE1 Substance)
                  (subclass ?SUBSTANCE2 Substance)
                  (material ?SUBSTANCE1 ?OBJ)
                  (material ?SUBSTANCE2 ?OBJ)
                  (not
                        (equal ?SUBSTANCE1 ?SUBSTANCE2)))))

coll1 é sottoinsieme un proprio coll2 se e solo se
(<=>
      (subCollection ?COLL1 ?COLL2)
      (and
            (instance ?COLL1 Collection)
            (instance ?COLL2 Collection)
            (forall
                  (?MEMBER)
                  (=>
                        (member ?MEMBER ?COLL1)
                        (member ?MEMBER ?COLL2)))))

Se string é un' istanza di Stringa, allora esiste Carattere part tale che part é una parte di string.
(=>
      (instance ?STRING SymbolicString)
      (exists
            (?PART)
            (and
                  (part ?PART ?STRING)
                  (instance ?PART Character))))

Se lang é un' istanza di LinguaggioAnimale e proc é un agente di agent e lang é uno strumento per proc, allora agent é un' istanza di Animale e agent é not un' istanza di Umano.
(=>
      (and
            (instance ?LANG AnimalLanguage)
            (agent ?PROC ?AGENT)
            (instrument ?PROC ?LANG))
      (and
            (instance ?AGENT Animal)
            (not
                  (instance ?AGENT Human))))

Se lang é un' istanza di LinguaggioMacchina e proc é un agente di agent e lang é uno strumento per proc, allora agent é un' istanza di Macchinario.
(=>
      (and
            (instance ?LANG ComputerLanguage)
            (agent ?PROC ?AGENT)
            (instrument ?PROC ?LANG))
      (instance ?AGENT Machine))

Se lang é un' istanza di LinguaggioUmano e proc é un agente di agent e lang é uno strumento per proc, allora agent é un' istanza di Umano.
(=>
      (and
            (instance ?LANG HumanLanguage)
            (agent ?PROC ?AGENT)
            (instrument ?PROC ?LANG))
      (instance ?AGENT Human))

Se lang é un' istanza di LinguaggioCostruito, allora esiste Pianificazione plan tale che lang é un risultato di plan.
(=>
      (instance ?LANG ConstructedLanguage)
      (exists
            (?PLAN)
            (and
                  (instance ?PLAN Planning)
                  (result ?PLAN ?LANG))))

Se process é un' istanza di ProcessoRelazionale, allora esiste obj1,obj2 tale che obj1 é un paziente di process e obj2 é un paziente di process e obj1 is not uguale a obj2.
(=>
      (instance ?PROCESS DualObjectProcess)
      (exists
            (?OBJ1 ?OBJ2)
            (and
                  (patient ?PROCESS ?OBJ1)
                  (patient ?PROCESS ?OBJ2)
                  (not
                        (equal ?OBJ1 ?OBJ2)))))

Se number é un' istanza di NumeroImmaginario, allora esiste NumeroReale real tale che number is uguale a "real*"la radice quadrata di "".
(=>
      (instance ?NUMBER ImaginaryNumber)
      (exists
            (?REAL)
            (and
                  (instance ?REAL RealNumber)
                  (equal
                        ?NUMBER
                        (MultiplicationFn
                              ?REAL
                              (SquareRootFn -1))))))

number é un' istanza di NumeroRealeNonNegativo se e solo se number é più grande di o uguale a e number é un' istanza di NumeroReale.
(<=>
      (instance ?NUMBER NonnegativeRealNumber)
      (and
            (greaterThanOrEqualTo ?NUMBER 0)
            (instance ?NUMBER RealNumber)))

number é un' istanza di NumeroRealePositivo se e solo se number é più grande di e number é un' istanza di NumeroReale.
(<=>
      (instance ?NUMBER PositiveRealNumber)
      (and
            (greaterThan ?NUMBER 0)
            (instance ?NUMBER RealNumber)))

number é un' istanza di NumeroRealeNegativo se e solo se number é meno di e number é un' istanza di NumeroReale.
(<=>
      (instance ?NUMBER NegativeRealNumber)
      (and
            (lessThan ?NUMBER 0)
            (instance ?NUMBER RealNumber)))

Se number é un' istanza di NumeroComplesso, allora esiste NumeroReale real1,NumeroReale real2 tale che number is uguale a "(real1+"real2*"la radice quadrata di """.
(=>
      (instance ?NUMBER ComplexNumber)
      (exists
            (?REAL1 ?REAL2)
            (and
                  (instance ?REAL1 RealNumber)
                  (instance ?REAL2 RealNumber)
                  (equal
                        ?NUMBER
                        (AdditionFn
                              ?REAL1
                              (MultiplicationFn
                                    ?REAL2
                                    (SquareRootFn -1)))))))

Se function é un' istanza di FunzioneDiQuantitáUnariaECostante, allora il numero argomenti di function é un istanza di QuantitáCostante e rango di function é un'istanza di QuantitáCostante.
(=>
      (instance ?FUNCTION UnaryConstantFunctionQuantity)
      (and
            (domain ?FUNCTION 1 ConstantQuantity)
            (range ?FUNCTION ConstantQuantity)))

rel é un' istanza di RelazioneMonovalente se e solo se per ogni ,item1,item2 vale: se rel(,item1 vales e rel(,item2 vales, allora item1 is uguale a item2.
(<=>
      (instance ?REL SingleValuedRelation)
      (forall
            (@ROW ?ITEM1 ?ITEM2)
            (=>
                  (and
                        (holds ?REL @ROW ?ITEM1)
                        (holds ?REL @ROW ?ITEM2))
                  (equal ?ITEM1 ?ITEM2))))

rel é un' istanza di RelazioneAValoreTotale se e solo se esiste valence tale che rel é un' istanza di Relazione e rel %&ha valence argomento(s e
(<=>
      (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))))))

Se , allora rel é un' istanza di RelazioneAsimmetrica.
(=>
      (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))

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

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

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

Se formula1 aumentas la verosimiglianza di formula2 e "la probabilitá diformula2" is uguale a number1 e probabilitá di formula1 ammesso che formula2 valga é formula2, allora number2 é più grande di number1.
(=>
      (and
            (increasesLikelihood ?FORMULA1 ?FORMULA2)
            (equal
                  (ProbabilityFn ?FORMULA2)
                  ?NUMBER1)
            (conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
      (greaterThan ?NUMBER2 ?NUMBER1))

Se formula1 decreases likelihood of formula2 e "la probabilitá diformula2" is uguale a number1 e probabilitá di formula1 ammesso che formula2 valga é formula2, allora number2 é meno dinumber1.
(=>
      (and
            (decreasesLikelihood ?FORMULA1 ?FORMULA2)
            (equal
                  (ProbabilityFn ?FORMULA2)
                  ?NUMBER1)
            (conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
      (lessThan ?NUMBER2 ?NUMBER1))

Se probabilitá di formula1 e formula2 é indipendente e "la probabilitá diformula2" is uguale a number1 e probabilitá di formula1 ammesso che formula2 valga é formula2, allora number2 is uguale a number1.
(=>
      (and
            (independentProbability ?FORMULA1 ?FORMULA2)
            (equal
                  (ProbabilityFn ?FORMULA2)
                  ?NUMBER1)
            (conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
      (equal ?NUMBER2 ?NUMBER1))

Se formula1 é un' istanza di Formula e formula2 é un' istanza di Formula, allora formula1 aumentas la verosimiglianza di formula2 o formula1 decreases likelihood of formula2 o probabilitá di formula1 e formula2 é indipendente.
(=>
      (and
            (instance ?FORMULA1 Formula)
            (instance ?FORMULA2 Formula))
      (or
            (increasesLikelihood ?FORMULA1 ?FORMULA2)
            (decreasesLikelihood ?FORMULA1 ?FORMULA2)
            (independentProbability ?FORMULA1 ?FORMULA2)))

Se rel é un' istanza di intentional relation e rel(agent, vales e obj é un é membro di "(", allora agent é interessato a obj.
(=>
      (and
            (instance ?REL IntentionalRelation)
            (holds ?REL ?AGENT @ROW)
            (inList
                  ?OBJ
                  (ListFn @ROW)))
      (inScopeOfInterest ?AGENT ?OBJ))

(=>
      (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))))))))

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

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

Se list1 é un' istanza di Lista e list2 é un' istanza di Lista e per ogni number vale: "numberth elemento di list1" is uguale a "numberth elemento di list2", allora list1 is uguale a list2.
(=>
      (and
            (instance ?LIST1 List)
            (instance ?LIST2 List)
            (forall
                  (?NUMBER)
                  (equal
                        (ListOrderFn ?LIST1 ?NUMBER)
                        (ListOrderFn ?LIST2 ?NUMBER))))
      (equal ?LIST1 ?LIST2))

Se il numero number argomenti di rel é un istanza di class e rel( vales, allora "numberth elemento di "("" é un' istanza di class.
(=>
      (and
            (domain ?REL ?NUMBER ?CLASS)
            (holds ?REL @ROW))
      (instance
            (ListOrderFn
                  (ListFn @ROW)
                  ?NUMBER)
            ?CLASS))

Se il numero number argomento rel é una sottoclasse diclass e rel( vales, allora "numberth elemento di "("" é una sottoclasse di class.
(=>
      (and
            (domainSubclass ?REL ?NUMBER ?CLASS)
            (holds ?REL @ROW))
      (subclass
            (ListOrderFn
                  (ListFn @ROW)
                  ?NUMBER)
            ?CLASS))

Se "lunghezza di list1" is uguale a number, allora esiste list2 tale che list1 inizias list2 e "(number+1" is uguale a "lunghezza di list2" e ""(number+1"th elemento di list2" is uguale a item.
(=>
      (equal
            (ListLengthFn ?LIST1)
            ?NUMBER)
      (exists
            (?LIST2)
            (and
                  (initialList ?LIST1 ?LIST2)
                  (equal
                        (SuccessorFn ?NUMBER)
                        (ListLengthFn ?LIST2))
                  (equal
                        (ListOrderFn
                              ?LIST2
                              (SuccessorFn ?NUMBER))
                        ?ITEM))))

list3 is uguale a "la lista composta di list1 e list2" se e solo se per ogni number1,number2 vale: se number1 é minore o uguale a "lunghezza di list1" e number2 é minore o uguale a "lunghezza di list2" e number1 é un' istanza di NumeroInteroPositivo e number2 é un' istanza di NumeroInteroPositivo, allora "number1th elemento di list3" is uguale a "number1th elemento di list1" e ""("lunghezza di list1"+number2"th elemento di list3" is uguale a "number2th elemento di 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))))))

(=>
      (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))))))))

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

(=>
      (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))))))

Se seq é un' istanza di FunzioneSequenza e rango di seq é un'istanza di class, allora class é una sottoclasse di NumeroIntero.
(=>
      (and
            (instance ?SEQ SequenceFunction)
            (range ?SEQ ?CLASS))
      (subclass ?CLASS Integer))

(=>
      (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)))))

(=>
      (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)))))

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

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

Se relation é ordinamento parziale su class, allora relation é riflessivo su class e relation é un' istanza di RelazioneTransitiva e relation é un' istanza di RelazioneAntisimmetrica.
(=>
      (partialOrderingOn ?RELATION ?CLASS)
      (and
            (reflexiveOn ?RELATION ?CLASS)
            (instance ?RELATION TransitiveRelation)
            (instance ?RELATION AntisymmetricRelation)))

relation é ordinamento totale suclass se e solo se relation é ordinamento parziale su class e relation é tricotomizzante su class.
(<=>
      (totalOrderingOn ?RELATION ?CLASS)
      (and
            (partialOrderingOn ?RELATION ?CLASS)
            (trichotomizingOn ?RELATION ?CLASS)))

(=>
      (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)))))

Se relation é relazione di equivalenza su class, allora relation é un' istanza di RelazioneTransitiva e relation é un' istanza di RelazioneSimmetrica e relation é riflessivo su class.
(=>
      (equivalenceRelationOn ?RELATION ?CLASS)
      (and
            (instance ?RELATION TransitiveRelation)
            (instance ?RELATION SymmetricRelation)
            (reflexiveOn ?RELATION ?CLASS)))

(=>
      (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))))))

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

Se situation1 vales durante time e situation1 implicas situation2, allora situation2 vales durante time.
(=>
      (and
            (holdsDuring ?TIME ?SITUATION1)
            (entails ?SITUATION1 ?SITUATION2))
      (holdsDuring ?TIME ?SITUATION2))

Se role é un' istanza di RuoloSemantico e role(arg1,arg2 vales e arg1 é un' istanza di proc, allora arg2 é capace di fare proc nel ruolo role.
(=>
      (and
            (instance ?ROLE CaseRole)
            (holds ?ROLE ?ARG1 ?ARG2)
            (instance ?ARG1 ?PROC))
      (capability ?PROC ?ROLE ?ARG2))

Se obj utilizzas agent, allora esiste process tale che process é un agente di agent e obj é una risorsa per process.
(=>
      (exploits ?OBJ ?AGENT)
      (exists
            (?PROCESS)
            (and
                  (agent ?PROCESS ?AGENT)
                  (resource ?PROCESS ?OBJ))))

Se obj é in parte localizzato in region, allora esiste subobj tale che subobj é una parte di obj e subobj é esattamente localizzato in region.
(=>
      (partlyLocated ?OBJ ?REGION)
      (exists
            (?SUBOBJ)
            (and
                  (part ?SUBOBJ ?OBJ)
                  (exactlyLocated ?SUBOBJ ?REGION))))

Se obj é esattamente localizzato in region, allora non esiste otherobj tale che otherobj é esattamente localizzato in region e otherobj is not uguale a obj.
(=>
      (exactlyLocated ?OBJ ?REGION)
      (not
            (exists
                  (?OTHEROBJ)
                  (and
                        (exactlyLocated ?OTHEROBJ ?REGION)
                        (not
                              (equal ?OTHEROBJ ?OBJ))))))

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

Se time é un' istanza di PosizioneTemporale e "agent1 possiedees obj" vales durante time e "agent2 possiedees obj" vales durante time, allora agent1 is uguale a agent2.
(=>
      (and
            (instance ?TIME TimePosition)
            (holdsDuring
                  ?TIME
                  (possesses ?AGENT1 ?OBJ))
            (holdsDuring
                  ?TIME
                  (possesses ?AGENT2 ?OBJ)))
      (equal ?AGENT1 ?AGENT2))

Se proc1 inibisce proc2, allora per ogni time,place vale: ""esiste proc1 inst1 tale che inst1 é localizzato in place" vales durante time" decreases likelihood of ""esiste proc2 inst2 tale che inst2 é localizzato in place" vales durante 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)))))))

(=>
      (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))))))))

class1 sussume il contenuto di class2 e class2 sussume il contenuto di class1 se e solo se class1 é equivalente a class2.
(<=>
      (and
            (subsumesContentClass ?CLASS1 ?CLASS2)
            (subsumesContentClass ?CLASS2 ?CLASS1))
      (equivalentContentClass ?CLASS1 ?CLASS2))

class1 sussume il contenuto di class2 se e solo se per ogni obj2,info vale: se obj2 é un' istanza di class2 e obj2 contienes informazione info, allora esiste class1 obj1 tale che obj1 contienes informazione info.
(<=>
      (subsumesContentClass ?CLASS1 ?CLASS2)
      (forall
            (?OBJ2 ?INFO)
            (=>
                  (and
                        (instance ?OBJ2 ?CLASS2)
                        (containsInformation ?OBJ2 ?INFO))
                  (exists
                        (?OBJ1)
                        (and
                              (instance ?OBJ1 ?CLASS1)
                              (containsInformation ?OBJ1 ?INFO))))))

obj1 sussume il contenuto di obj2 e obj2 sussume il contenuto di obj1 se e solo se obj1 é equivalente a obj2.
(<=>
      (and
            (subsumesContentInstance ?OBJ1 ?OBJ2)
            (subsumesContentInstance ?OBJ2 ?OBJ1))
      (equivalentContentInstance ?OBJ1 ?OBJ2))

Se process esprime il contenuto di prop, allora esiste OggettoSemiotico obj tale che obj contienes informazione prop.
(=>
      (realization ?PROCESS ?PROP)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ ContentBearingObject)
                  (containsInformation ?OBJ ?PROP))))

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

Se agent usa obj, allora esiste proc tale che proc é un agente di agent e obj é uno strumento per proc.
(=>
      (uses ?OBJ ?AGENT)
      (exists
            (?PROC)
            (and
                  (agent ?PROC ?AGENT)
                  (instrument ?PROC ?OBJ))))

Se number é un' istanza di NumeroRazionale, allora esiste NumeroIntero int1,NumeroIntero int2 tale che number is uguale a "int1/int2".
(=>
      (instance ?NUMBER RationalNumber)
      (exists
            (?INT1 ?INT2)
            (and
                  (instance ?INT1 Integer)
                  (instance ?INT2 Integer)
                  (equal
                        ?NUMBER
                        (DivisionFn ?INT1 ?INT2)))))

"ilvalore assoluto dinumber1" is uguale a number2 e number1 é un' istanza di NumeroReale e number2 é un' istanza di NumeroReale se e solo se
(<=>
      (and
            (equal
                  (AbsoluteValueFn ?NUMBER1)
                  ?NUMBER2)
            (instance ?NUMBER1 RealNumber)
            (instance ?NUMBER2 RealNumber))
      (or
            (and
                  (instance ?NUMBER1 NonnegativeRealNumber)
                  (equal ?NUMBER1 ?NUMBER2))
            (and
                  (instance ?NUMBER1 NegativeRealNumber)
                  (equal
                        ?NUMBER2
                        (SubtractionFn 0 ?NUMBER1)))))

Se "il tetto di number" is uguale a int, allora non esiste NumeroIntero otherint tale che otherint é più grande di o uguale a number e otherint é meno diint.
(=>
      (equal
            (CeilingFn ?NUMBER)
            ?INT)
      (not
            (exists
                  (?OTHERINT)
                  (and
                        (instance ?OTHERINT Integer)
                        (greaterThanOrEqualTo ?OTHERINT ?NUMBER)
                        (lessThan ?OTHERINT ?INT)))))

Se "the il maggior numero intero minore o uguale a number" is uguale a int, allora non esiste NumeroIntero otherint tale che otherint é minore o uguale a number e otherint é più grande di int.
(=>
      (equal
            (FloorFn ?NUMBER)
            ?INT)
      (not
            (exists
                  (?OTHERINT)
                  (and
                        (instance ?OTHERINT Integer)
                        (lessThanOrEqualTo ?OTHERINT ?NUMBER)
                        (greaterThan ?OTHERINT ?INT)))))

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

Se number é un' istanza di NumeroComplesso, allora esiste part1,part2 tale che part1 is uguale a "la parte reale di number" e part2 is uguale a "la parte immaginaria di number".
(=>
      (instance ?NUMBER ComplexNumber)
      (exists
            (?PART1 ?PART2)
            (and
                  (equal
                        ?PART1
                        (RealNumberFn ?NUMBER))
                  (equal
                        ?PART2
                        (ImaginaryPartFn ?NUMBER)))))

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

Se "il maggiore di number1 e number2" is uguale a number, allora
(=>
      (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))))

Se "il minore di number1 e number2" is uguale a number, allora
(=>
      (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))))

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

Se int1 é un' istanza di NumeroIntero e int2 é un' istanza di NumeroIntero, allora int1 é not meno diint2 o int2 é not meno di"(int1+1".
(=>
      (and
            (instance ?INT1 Integer)
            (instance ?INT2 Integer))
      (not
            (and
                  (lessThan ?INT1 ?INT2)
                  (lessThan
                        ?INT2
                        (SuccessorFn ?INT1)))))

Se int1 é un' istanza di NumeroIntero e int2 é un' istanza di NumeroIntero, allora int2 é not meno diint1 o "(int1+2" é not meno diint2.
(=>
      (and
            (instance ?INT1 Integer)
            (instance ?INT2 Integer))
      (not
            (and
                  (lessThan ?INT2 ?INT1)
                  (lessThan
                        (PredecessorFn ?INT1)
                        ?INT2))))

Se set é un' istanza di InsiemeFinito, allora esiste NumeroInteroNonNegativo number tale che number is uguale a "il numero di istanzia in set".
(=>
      (instance ?SET FiniteSet)
      (exists
            (?NUMBER)
            (and
                  (instance ?NUMBER NonnegativeInteger)
                  (equal
                        ?NUMBER
                        (CardinalityFn ?SET)))))

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

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

Se graph é un' istanza di Grafo e node1 é un' istanza di NodoDelGrafo e node2 é un' istanza di NodoDelGrafo e node1 é una parte di graph e node2 é una parte di graph e node1 is not uguale a node2, allora esiste arc,path tale che
(=>
      (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)))))))

Se graph é un' istanza di Grafo, allora esiste node1,node2,node3,arc1,arc2 tale che node1 é una parte di graph e node2 é una parte di graph e node3 é una parte di graph e arc1 é una parte di graph e arc2 é una parte di graph e node2 legas arc1 e node1 e node3 legas arc2 e node2 e node1 is not uguale a node2 e node2 is not uguale a node3 e node1 is not uguale a node3 e arc1 is not uguale a 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)))))

Se graph é un' istanza di GrafoDiretto e arc é un' istanza di ArcoDelGrafo e arc é una parte di graph, allora esiste node1,node2 tale che "il nodo iniziale di arc" is uguale a node1 e "il nodo terminale di arc" is uguale a node2.
(=>
      (and
            (instance ?GRAPH DirectedGraph)
            (instance ?ARC GraphArc)
            (graphPart ?ARC ?GRAPH))
      (exists
            (?NODE1 ?NODE2)
            (and
                  (equal
                        (InitialNodeFn ?ARC)
                        ?NODE1)
                  (equal
                        (TerminalNodeFn ?ARC)
                        ?NODE2))))

Se graph é un' istanza di Albero, allora non esiste GrafoCiclico loop tale che loop é una parte di graph.
(=>
      (instance ?GRAPH Tree)
      (not
            (exists
                  (?LOOP)
                  (and
                        (instance ?LOOP GraphLoop)
                        (graphPart ?LOOP ?GRAPH)))))

(=>
      (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)))))))

(=>
      (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)))))))

graph é un' istanza di CircuitoDelGrafo se e solo se esiste node tale che "l' inizio di graph" is uguale a node e "la fine di graph" is uguale a node.
(<=>
      (instance ?GRAPH GraphCircuit)
      (exists
            (?NODE)
            (and
                  (equal
                        (BeginNodeFn ?GRAPH)
                        ?NODE)
                  (equal
                        (EndNodeFn ?GRAPH)
                        ?NODE))))

graph é un' istanza di MultiGrafo se e solo se esiste arc1,arc2,node1,node2 tale che arc1 é una parte di graph e arc2 é una parte di graph e node1 é una parte di graph e node2 é una parte di graph e arc1 legas node1 e node2 e arc2 legas node1 e node2 e arc1 is not uguale a arc2.
(<=>
      (instance ?GRAPH MultiGraph)
      (exists
            (?ARC1 ?ARC2 ?NODE1 ?NODE2)
            (and
                  (graphPart ?ARC1 ?GRAPH)
                  (graphPart ?ARC2 ?GRAPH)
                  (graphPart ?NODE1 ?GRAPH)
                  (graphPart ?NODE2 ?GRAPH)
                  (links ?NODE1 ?NODE2 ?ARC1)
                  (links ?NODE1 ?NODE2 ?ARC2)
                  (not
                        (equal ?ARC1 ?ARC2)))))

graph é un' istanza di PseudoGrafo se e solo se esiste GrafoCiclico loop tale che loop é una parte di graph.
(<=>
      (instance ?GRAPH PseudoGraph)
      (exists
            (?LOOP)
            (and
                  (instance ?LOOP GraphLoop)
                  (graphPart ?LOOP ?GRAPH))))

Se part é un' istanza di ElementoDelGrafo, allora esiste Grafo graph tale che part é una parte di graph.
(=>
      (instance ?PART GraphElement)
      (exists
            (?GRAPH)
            (and
                  (instance ?GRAPH Graph)
                  (graphPart ?PART ?GRAPH))))

Se "il nodo iniziale di arc" is uguale a node e "il nodo terminale di arc" is uguale a node, allora arc é un' istanza di GrafoCiclico.
(=>
      (and
            (equal
                  (InitialNodeFn ?ARC)
                  ?NODE)
            (equal
                  (TerminalNodeFn ?ARC)
                  ?NODE))
      (instance ?ARC GraphLoop))

Se graph1 é un sottografo di graph2 e element é una parte di graph1, allora element é una parte di graph2.
(=>
      (and
            (subGraph ?GRAPH1 ?GRAPH2)
            (graphPart ?ELEMENT ?GRAPH1))
      (graphPart ?ELEMENT ?GRAPH2))

(=>
      (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)))

(=>
      (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)))

(=>
      (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))))

(=>
      (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))))

Se path é una parte di graph e graph é not un' istanza di GrafoDiretto, allora "l' insieme di cammini tra node1 e node2" is uguale a path se e solo se "l' insieme di cammini tra node2 e node1" is uguale a path.
(=>
      (and
            (graphPart ?PATH ?GRAPH)
            (not
                  (instance ?GRAPH DirectedGraph)))
      (<=>
            (equal
                  (GraphPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (GraphPathFn ?NODE2 ?NODE1)
                  ?PATH)))

Non esiste l' insieme di cammini che partiziona graph in due grafi separati path1,l' insieme di cammini minimi che partiziona graphin due separati grafi path2 tale che la lunghezza di path1 é number1 e la lunghezza di path2 é number2 e number1 é meno dinumber2.
(not
      (exists
            (?PATH1 ?PATH2)
            (and
                  (instance
                        ?PATH1
                        (CutSetFn ?GRAPH))
                  (instance
                        ?PATH2
                        (MinimalCutSetFn ?GRAPH))
                  (pathLength ?PATH1 ?NUMBER1)
                  (pathLength ?PATH2 ?NUMBER2)
                  (lessThan ?NUMBER1 ?NUMBER2))))

Se "number unit(s" is uguale a quant e unit é una sottoclasse di quanttype, allora quant é un' istanza di quanttype.
(=>
      (and
            (equal
                  (MeasureFn ?NUMBER ?UNIT)
                  ?QUANT)
            (subclass ?UNIT ?QUANTTYPE))
      (instance ?QUANT ?QUANTTYPE))

(=>
      (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)))))

(=>
      (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)))))

quantity é un' istanza di "l' intervallo da from a to" se e solo se quantity é più grande di o uguale a from e quantity é minore o uguale a to.
(<=>
      (instance
            ?QUANTITY
            (IntervalFn ?FROM ?TO))
      (and
            (greaterThanOrEqualTo ?QUANTITY ?FROM)
            (lessThanOrEqualTo ?QUANTITY ?TO)))

Se number é un' istanza di NumeroReale e unit é un' istanza di UnitáDiMisura, allora "la magnitudine di "number unit(s"" is uguale a number.
(=>
      (and
            (instance ?NUMBER RealNumber)
            (instance ?UNIT UnitOfMeasure))
      (equal
            (MagnitudeFn
                  (MeasureFn ?NUMBER ?UNIT))
            ?NUMBER))

Se l' altezza diobj1 é obj2, allora esiste top tale che ilvertice obj1 é top e la distanza tra top e obj2 é height.
(=>
      (altitude ?OBJ1 ?OBJ2 ?HEIGHT)
      (exists
            (?TOP)
            (and
                  (top ?TOP ?OBJ1)
                  (distance ?TOP ?OBJ2 ?HEIGHT))))

Se depth(obj1,obj2,depth) vale, allora esiste bottom tale che the bottom of obj1 is bottom e la distanza tra bottom e obj2 é depth.
(=>
      (depth ?OBJ1 ?OBJ2 ?DEPTH)
      (exists
            (?BOTTOM)
            (and
                  (bottom ?BOTTOM ?OBJ1)
                  (distance ?BOTTOM ?OBJ2 ?DEPTH))))

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

Se point é un' istanza di PuntoTemporale e point is not uguale a positive infinity, allora point succede?{s} prima di positive infinity.
(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT PositiveInfinity)))
      (before ?POINT PositiveInfinity))

Se point é un' istanza di PuntoTemporale e point is not uguale a positive infinity, allora esiste otherpoint tale che otherpoint is tra point e positive infinity.
(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT PositiveInfinity)))
      (exists
            (?OTHERPOINT)
            (temporallyBetween ?POINT ?OTHERPOINT PositiveInfinity)))

Se point é un' istanza di PuntoTemporale e point is not uguale a negative infinity, allora negative infinity succede?{s} prima di point.
(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT NegativeInfinity)))
      (before NegativeInfinity ?POINT))

Se point é un' istanza di PuntoTemporale e point is not uguale a negative infinity, allora esiste otherpoint tale che otherpoint is tra negative infinity e point.
(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT NegativeInfinity)))
      (exists
            (?OTHERPOINT)
            (temporallyBetween NegativeInfinity ?OTHERPOINT ?POINT)))

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

Se point é un' istanza di PuntoTemporale, allora esiste IntervalloTemporale interval tale che point é una parte diinterval.
(=>
      (instance ?POINT TimePoint)
      (exists
            (?INTERVAL)
            (and
                  (instance ?INTERVAL TimeInterval)
                  (temporalPart ?POINT ?INTERVAL))))

Se interval é un' istanza di IntervalloTemporale, allora esiste PuntoTemporale point tale che point é una parte diinterval.
(=>
      (instance ?INTERVAL TimeInterval)
      (exists
            (?POINT)
            (and
                  (instance ?POINT TimePoint)
                  (temporalPart ?POINT ?INTERVAL))))

Se situation vales durante time1 e time2 é una parte ditime1, allora situation vales durante time2.
(=>
      (and
            (holdsDuring ?TIME1 ?SITUATION)
            (temporalPart ?TIME2 ?TIME1))
      (holdsDuring ?TIME2 ?SITUATION))

Se "rel(inst1,inst2 vales" vales durante interval e inst1 é un' istanza di EntitáConcreta e inst2 é un' istanza di EntitáConcreta, allora inst1 esistes durante interval e inst2 esistes durante interval.
(=>
      (and
            (holdsDuring
                  ?INTERVAL
                  (holds ?REL ?INST1 ?INST2))
            (instance ?INST1 Physical)
            (instance ?INST2 Physical))
      (and
            (time ?INST1 ?INTERVAL)
            (time ?INST2 ?INTERVAL)))

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

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

interval1 inizias interval2 se e solo se "l' inizio di interval1" is uguale a "l' inizio di interval2" e "la fine di interval1" succede?{s} prima di "la fine di interval2".
(<=>
      (starts ?INTERVAL1 ?INTERVAL2)
      (and
            (equal
                  (BeginFn ?INTERVAL1)
                  (BeginFn ?INTERVAL2))
            (before
                  (EndFn ?INTERVAL1)
                  (EndFn ?INTERVAL2))))

interval1 finiscees interval2 se e solo se "l' inizio di interval2" succede?{s} prima di "l' inizio di interval1" e "la fine di interval2" is uguale a "la fine di interval1".
(<=>
      (finishes ?INTERVAL1 ?INTERVAL2)
      (and
            (before
                  (BeginFn ?INTERVAL2)
                  (BeginFn ?INTERVAL1))
            (equal
                  (EndFn ?INTERVAL2)
                  (EndFn ?INTERVAL1))))

(=>
      (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))))))

point2 is tra point1 e point3 se e solo se point1 succede?{s} prima di point2 e point2 succede?{s} prima di point3.
(<=>
      (temporallyBetween ?POINT1 ?POINT2 ?POINT3)
      (and
            (before ?POINT1 ?POINT2)
            (before ?POINT2 ?POINT3)))

point2 é tra o in point1 e point3 se e solo se point1 succede?{s} prima di o con point2 e point2 succede?{s} prima di o con point3.
(<=>
      (temporallyBetweenOrEqual ?POINT1 ?POINT2 ?POINT3)
      (and
            (beforeOrEqual ?POINT1 ?POINT2)
            (beforeOrEqual ?POINT2 ?POINT3)))

phys esistes durante time e time é un' istanza di PuntoTemporale se e solo se time é tra o in "l' inizio di "il tempo di esistenza di phys"" e "la fine di "il tempo di esistenza di phys"".
(<=>
      (and
            (time ?PHYS ?TIME)
            (instance ?TIME TimePoint))
      (temporallyBetweenOrEqual
            (BeginFn
                  (WhenFn ?PHYS))
            ?TIME
            (EndFn
                  (WhenFn ?PHYS))))

interval2 sovrappones interval1 se e solo se esiste IntervalloTemporale interval3 tale che interval3 é una parte diinterval1 e interval3 é una parte diinterval2.
(<=>
      (overlapsTemporally ?INTERVAL1 ?INTERVAL2)
      (exists
            (?INTERVAL3)
            (and
                  (instance ?INTERVAL3 TimeInterval)
                  (temporalPart ?INTERVAL3 ?INTERVAL1)
                  (temporalPart ?INTERVAL3 ?INTERVAL2))))

Se rel é un' istanza di RelazioneSpaziale e rel(obj1,obj2 vales, allora "il tempo di esistenza di obj2" sovrappones "il tempo di esistenza di obj1".
(=>
      (and
            (instance ?REL SpatialRelation)
            (holds ?REL ?OBJ1 ?OBJ2))
      (overlapsTemporally
            (WhenFn ?OBJ1)
            (WhenFn ?OBJ2)))

Se interval1 has luogodurante interval2, allora "la fine di interval1" succede?{s} prima di "la fine di interval2" e "l' inizio di interval2" succede?{s} prima di "l' inizio di interval1".
(=>
      (during ?INTERVAL1 ?INTERVAL2)
      (and
            (before
                  (EndFn ?INTERVAL1)
                  (EndFn ?INTERVAL2))
            (before
                  (BeginFn ?INTERVAL2)
                  (BeginFn ?INTERVAL1))))

Se "l' inizio di interval1" is uguale a "l' inizio di interval2" e "la fine di interval1" is uguale a "la fine di interval2", allora interval1 is uguale a interval2.
(=>
      (and
            (equal
                  (BeginFn ?INTERVAL1)
                  (BeginFn ?INTERVAL2))
            (equal
                  (EndFn ?INTERVAL1)
                  (EndFn ?INTERVAL2)))
      (equal ?INTERVAL1 ?INTERVAL2))

Se "intervallo tra point1 e point2" is uguale a interval, allora "l' inizio di interval" is uguale a point1 e "la fine di interval" is uguale a point2.
(=>
      (equal
            (TimeIntervalFn ?POINT1 ?POINT2)
            ?INTERVAL)
      (and
            (equal
                  (BeginFn ?INTERVAL)
                  ?POINT1)
            (equal
                  (EndFn ?INTERVAL)
                  ?POINT2)))

Se interval é un' istanza di "il periodo ricorrente da timeclass1 a timeclass2", allora esiste timeclass1 time1,timeclass2 time2 tale che time1 inizias interval e time2 finiscees interval.
(=>
      (instance
            ?INTERVAL
            (RecurrentTimeIntervalFn ?TIMECLASS1 ?TIMECLASS2))
      (exists
            (?TIME1 ?TIME2)
            (and
                  (instance ?TIME1 ?TIMECLASS1)
                  (instance ?TIME2 ?TIMECLASS2)
                  (starts ?TIME1 ?INTERVAL)
                  (finishes ?TIME2 ?INTERVAL))))

Se obj é una risorsa per proc e "lamisura obj é quant1" vales durante "immediatamente prima di "il tempo di esistenza di proc"" e "lamisura obj é quant2" vales durante "immediatamente dopo "il tempo di esistenza di proc"", allora quant1 é più grande di quant2.
(=>
      (and
            (resource ?PROC ?OBJ)
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?PROC))
                  (measure ?OBJ ?QUANT1))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?PROC))
                  (measure ?OBJ ?QUANT2)))
      (greaterThan ?QUANT1 ?QUANT2))

Se day1 é un' istanza di "il giorno number1" e day2 é un' istanza di "il giorno number2" e "(number2-number1" is uguale a , allora day1 incontras day2.
(=>
      (and
            (instance
                  ?DAY1
                  (DayFn ?NUMBER1 ?MONTH))
            (instance
                  ?DAY2
                  (DayFn ?NUMBER2 ?MONTH))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?DAY1 ?DAY2))

Se hour1 é un' istanza di "l' ora number1" e hour2 é un' istanza di "l' ora number2" e "(number2-number1" is uguale a , allora hour1 incontras hour2.
(=>
      (and
            (instance
                  ?HOUR1
                  (HourFn ?NUMBER1 ?DAY))
            (instance
                  ?HOUR2
                  (HourFn ?NUMBER2 ?DAY))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?HOUR1 ?HOUR2))

Se minute1 é un' istanza di "il minutonumber1" e minute2 é un' istanza di "il minutonumber2" e "(number2-number1" is uguale a , allora minute1 incontras minute2.
(=>
      (and
            (instance
                  ?MINUTE1
                  (MinuteFn ?NUMBER1 ?HOUR))
            (instance
                  ?MINUTE2
                  (MinuteFn ?NUMBER2 ?HOUR))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?MINUTE1 ?MINUTE2))

Se second1 é un' istanza di "il secondo number1" e second2 é un' istanza di "il secondo number2" e "(number2-number1" is uguale a , allora second1 incontras second2.
(=>
      (and
            (instance
                  ?SECOND1
                  (SecondFn ?NUMBER1 ?MINUTE))
            (instance
                  ?SECOND2
                  (SecondFn ?NUMBER2 ?MINUTE))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?SECOND1 ?SECOND2))

Se year1 é un' istanza di Anno e year2 é un' istanza di Anno e "(year2-year1" is uguale a , allora year1 incontras year2.
(=>
      (and
            (instance ?YEAR1 Year)
            (instance ?YEAR2 Year)
            (equal
                  (SubtractionFn ?YEAR2 ?YEAR1)
                  1))
      (meetsTemporally ?YEAR1 ?YEAR2))

Se leap é un' istanza di AnnoBisestile e leap is uguale a "number Anno(s", allora
(=>
      (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)))

Se month1 is uguale a "il mese Gennaio" e month2 is uguale a "il mese Febbraio", allora month1 incontras month2.
(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn January ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn February ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

Se "il mese Febbraio" is uguale a month e year é not un' istanza di AnnoBisestile, allora durata di month é " day duration(s".
(=>
      (and
            (equal
                  (MonthFn February ?YEAR)
                  ?MONTH)
            (not
                  (instance ?YEAR LeapYear)))
      (duration
            ?MONTH
            (MeasureFn 28 DayDuration)))

Se "il mese Febbraio" is uguale a month e year é un' istanza di AnnoBisestile, allora durata di month é " day duration(s".
(=>
      (and
            (equal
                  (MonthFn February ?YEAR)
                  ?MONTH)
            (instance ?YEAR LeapYear))
      (duration
            ?MONTH
            (MeasureFn 29 DayDuration)))

Se month1 is uguale a "il mese Febbraio" e month2 is uguale a "il mese Marzo", allora month1 incontras month2.
(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn February ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn March ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

Se month1 is uguale a "il mese Marzo" e month2 is uguale a "il mese Aprile", allora month1 incontras month2.
(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn March ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn April ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

Se month1 is uguale a "il mese Aprile" e month2 is uguale a "il mese Maggio", allora month1 incontras month2.
(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn April ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn May ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

Se month1 is uguale a "il mese Maggio" e month2 is uguale a "il mese Giugno", allora month1 incontras month2.
(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn May ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn June ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

Se month1 is uguale a "il mese Giugno" e month2 is uguale a "il mese Luglio", allora month1 incontras month2.
(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn June ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn July ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

Se month1 is uguale a "il mese Luglio" e month2 is uguale a "il mese Agosto", allora month1 incontras month2.
(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn July ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn August ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

Se month1 is uguale a "il mese Agosto" e month2 is uguale a "il mese Settembre", allora month1 incontras month2.
(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn August ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn September ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

Se month1 is uguale a "il mese Settembre" e month2 is uguale a "il mese Ottobre", allora month1 incontras month2.
(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn September ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn October ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

Se month1 is uguale a "il mese Ottobre" e month2 is uguale a "il mese Novembre", allora month1 incontras month2.
(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn October ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn November ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

Se month1 is uguale a "il mese Novembre" e month2 is uguale a "il mese Dicembre", allora month1 incontras month2.
(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn November ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn December ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

Se month1 is uguale a "il mese Dicembre" e month2 is uguale a "il mese Gennaio" e year1 incontras year2, allora month1 incontras month2.
(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn December ?YEAR1))
            (equal
                  ?MONTH2
                  (MonthFn January ?YEAR2))
            (meetsTemporally ?YEAR1 ?YEAR2))
      (meetsTemporally ?MONTH1 ?MONTH2))

Se day1 é un' istanza di Lunedí e day2 é un' istanza di Martedí e week é un' istanza di Settimana e day1 é una parte diweek e day2 é una parte diweek, allora day1 incontras day2.
(=>
      (and
            (instance ?DAY1 Monday)
            (instance ?DAY2 Tuesday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

Se day1 é un' istanza di Martedí e day2 é un' istanza di Mercoledí e week é un' istanza di Settimana e day1 é una parte diweek e day2 é una parte diweek, allora day1 incontras day2.
(=>
      (and
            (instance ?DAY1 Tuesday)
            (instance ?DAY2 Wednesday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

Se day1 é un' istanza di Mercoledí e day2 é un' istanza di Giovedí e week é un' istanza di Settimana e day1 é una parte diweek e day2 é una parte diweek, allora day1 incontras day2.
(=>
      (and
            (instance ?DAY1 Wednesday)
            (instance ?DAY2 Thursday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

Se day1 é un' istanza di Giovedí e day2 é un' istanza di Venerdí e week é un' istanza di Settimana e day1 é una parte diweek e day2 é una parte diweek, allora day1 incontras day2.
(=>
      (and
            (instance ?DAY1 Thursday)
            (instance ?DAY2 Friday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

Se day1 é un' istanza di Venerdí e day2 é un' istanza di Sabato e week é un' istanza di Settimana e day1 é una parte diweek e day2 é una parte diweek, allora day1 incontras day2.
(=>
      (and
            (instance ?DAY1 Friday)
            (instance ?DAY2 Saturday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

Se day1 é un' istanza di Sabato e day2 é un' istanza di Domenica e week é un' istanza di Settimana e day1 é una parte diweek e day2 é una parte diweek, allora day1 incontras day2.
(=>
      (and
            (instance ?DAY1 Saturday)
            (instance ?DAY2 Sunday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

Se day1 é un' istanza di Domenica e day2 é un' istanza di Lunedí e week1 é un' istanza di Settimana e week2 é un' istanza di Settimana e day1 é una parte diweek1 e day2 é una parte diweek2 e week1 incontras week2, allora day1 incontras 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))

(=>
      (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))))))

(=>
      (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)))))

Se "decomposizione di interval in ? interval-types" is uguale a class, allora esiste class time tale che time inizias interval.
(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (exists
            (?TIME)
            (and
                  (instance ?TIME ?CLASS)
                  (starts ?TIME ?INTERVAL))))

Se "decomposizione di interval in ? interval-types" is uguale a class, allora esiste class time tale che time finiscees interval.
(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (exists
            (?TIME)
            (and
                  (instance ?TIME ?CLASS)
                  (finishes ?TIME ?INTERVAL))))

(=>
      (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))))))

(=>
      (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))))))

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

Se month é un' istanza di Mese e durata di month é "number day duration(s", allora "il numero di istanzia in "decomposizione di month in ? Giornos"" is uguale a number.
(=>
      (and
            (instance ?MONTH Month)
            (duration
                  ?MONTH
                  (MeasureFn ?NUMBER DayDuration)))
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?MONTH Day))
            ?NUMBER))

obj1 connette obj2 e obj3 se e solo se obj1 é connesso a obj2 e obj1 é connesso a obj3 e obj2 é not connesso a obj3.
(<=>
      (connects ?OBJ1 ?OBJ2 ?OBJ3)
      (and
            (connected ?OBJ1 ?OBJ2)
            (connected ?OBJ1 ?OBJ3)
            (not
                  (connected ?OBJ2 ?OBJ3))))

obj1 si sovrappones a obj2 se e solo se esiste obj3 tale che obj3 é una parte di obj1 e obj3 é una parte di obj2.
(<=>
      (overlapsSpatially ?OBJ1 ?OBJ2)
      (exists
            (?OBJ3)
            (and
                  (part ?OBJ3 ?OBJ1)
                  (part ?OBJ3 ?OBJ2))))

Se obj1 é un membro di coll e obj2 é un membro di coll e obj1 is not uguale a obj2, allora obj1 non si sovrappone a obj2.
(=>
      (and
            (member ?OBJ1 ?COLL)
            (member ?OBJ2 ?COLL)
            (not
                  (equal ?OBJ1 ?OBJ2)))
      (not
            (overlapsSpatially ?OBJ1 ?OBJ2)))

Se rel é un' istanza di RuoloSemantico e rel(process,obj vales, allora esiste time tale che "il luogo dove process era in time" si sovrappones a obj.
(=>
      (and
            (instance ?REL CaseRole)
            (holds ?REL ?PROCESS ?OBJ))
      (exists
            (?TIME)
            (overlapsSpatially
                  (WhereFn ?PROCESS ?TIME)
                  ?OBJ)))

obj1 si sovrappone parzialmente as a obj2 se e solo se
(<=>
      (overlapsPartially ?OBJ1 ?OBJ2)
      (and
            (not
                  (part ?OBJ1 ?OBJ2))
            (not
                  (part ?OBJ2 ?OBJ1))
            (exists
                  (?OBJ3)
                  (and
                        (part ?OBJ3 ?OBJ1)
                        (part ?OBJ3 ?OBJ2)))))

Se obj1 é una parte superficiale di obj2, allora obj1 é not una parte interiore di obj2 e non esiste obj3 tale che obj3 é una parte interiore di obj1.
(=>
      (superficialPart ?OBJ1 ?OBJ2)
      (and
            (not
                  (interiorPart ?OBJ1 ?OBJ2))
            (not
                  (exists
                        (?OBJ3)
                        (interiorPart ?OBJ3 ?OBJ1)))))

Se the bottom of object is bottom e part é una parte di object e part é not connesso a bottom, allora part é above a bottom.
(=>
      (and
            (bottom ?BOTTOM ?OBJECT)
            (part ?PART ?OBJECT)
            (not
                  (connected ?PART ?BOTTOM)))
      (orientation ?PART ?BOTTOM Above))

Se ilvertice object é top e part é una parte di object e part é not connesso a top, allora part é below a top.
(=>
      (and
            (top ?TOP ?OBJECT)
            (part ?PART ?OBJECT)
            (not
                  (connected ?PART ?TOP)))
      (orientation ?PART ?TOP Below))

Se un lato di object é side e part é una parte di object e part é not connesso a side, allora esiste direct tale che side é direct a part.
(=>
      (and
            (side ?SIDE ?OBJECT)
            (part ?PART ?OBJECT)
            (not
                  (connected ?PART ?SIDE)))
      (exists
            (?DIRECT)
            (orientation ?SIDE ?PART ?DIRECT)))

L' ampiezza di object é width se e solo se esiste side1,side2 tale che un lato di object é side1 e un lato di object é side2 e la distanza tra side1 e side2 é width.
(<=>
      (width ?OBJECT ?WIDTH)
      (exists
            (?SIDE1 ?SIDE2)
            (and
                  (side ?SIDE1 ?OBJECT)
                  (side ?SIDE2 ?OBJECT)
                  (distance ?SIDE1 ?SIDE2 ?WIDTH))))

Se l' altezza di object é height e ilvertice object é top e the bottom of object is bottom, allora la distanza tra top e bottom é height.
(=>
      (and
            (height ?OBJECT ?HEIGHT)
            (top ?TOP ?OBJECT)
            (bottom ?BOTTOM ?OBJECT))
      (distance ?TOP ?BOTTOM ?HEIGHT))

Se obj3 is uguale a "l' intersezione delle parti di obj1 e obj2", allora per ogni part vale: part é una parte di obj3 se e solo se part é una parte di obj1 e part é una parte di obj2.
(=>
      (equal
            ?OBJ3
            (MereologicalProductFn ?OBJ1 ?OBJ2))
      (forall
            (?PART)
            (<=>
                  (part ?PART ?OBJ3)
                  (and
                        (part ?PART ?OBJ1)
                        (part ?PART ?OBJ2)))))

Se obj3 is uguale a "la differenza tra le parti di obj1 e obj2", allora per ogni part vale: part é una parte di obj3 se e solo se part é una parte di obj1 e part é not una parte di obj2.
(=>
      (equal
            ?OBJ3
            (MereologicalDifferenceFn ?OBJ1 ?OBJ2))
      (forall
            (?PART)
            (<=>
                  (part ?PART ?OBJ3)
                  (and
                        (part ?PART ?OBJ1)
                        (not
                              (part ?PART ?OBJ2))))))

Se hole é un' apertura in obj1 e hole é un' apertura in obj2, allora esiste obj3 tale che obj3 é una Parte propria di "l' intersezione delle parti di obj1 e obj2" e hole é un' apertura in obj3.
(=>
      (and
            (hole ?HOLE ?OBJ1)
            (hole ?HOLE ?OBJ2))
      (exists
            (?OBJ3)
            (and
                  (properPart
                        ?OBJ3
                        (MereologicalProductFn ?OBJ1 ?OBJ2))
                  (hole ?HOLE ?OBJ3))))

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

Se hole é un' apertura in obj1 e obj1 é una parte di obj2, allora hole si sovrappones a obj2 o hole é un' apertura in obj2.
(=>
      (and
            (hole ?HOLE ?OBJ1)
            (part ?OBJ1 ?OBJ2))
      (or
            (overlapsSpatially ?HOLE ?OBJ2)
            (hole ?HOLE ?OBJ2)))

Se hole1 é un' apertura in obj1 e hole2 é un' apertura in obj2 e hole1 si sovrappones a hole2, allora obj1 si sovrappones a obj2.
(=>
      (and
            (hole ?HOLE1 ?OBJ1)
            (hole ?HOLE2 ?OBJ2)
            (overlapsSpatially ?HOLE1 ?HOLE2))
      (overlapsSpatially ?OBJ1 ?OBJ2))

Se obj1 is uguale a " ció che entra nell'apertura hole", allora per ogni obj2 vale: obj2 si sovrappones a obj1 se e solo se esiste obj3 tale che hole é un' apertura in obj3 e obj2 si sovrappones a obj3.
(=>
      (equal
            ?OBJ1
            (PrincipalHostFn ?HOLE))
      (forall
            (?OBJ2)
            (<=>
                  (overlapsSpatially ?OBJ2 ?OBJ1)
                  (exists
                        (?OBJ3)
                        (and
                              (hole ?HOLE ?OBJ3)
                              (overlapsSpatially ?OBJ2 ?OBJ3))))))

Se hole1 é un' istanza di Apertura e hole2 é una Parte propria di hole1, allora esiste obj tale che hole1 incontras obj e hole2 non incontra obj.
(=>
      (and
            (instance ?HOLE1 Hole)
            (properPart ?HOLE2 ?HOLE1))
      (exists
            (?OBJ)
            (and
                  (meetsSpatially ?HOLE1 ?OBJ)
                  (not
                        (meetsSpatially ?HOLE2 ?OBJ)))))

fillable is an attribute of hole1 se e solo se esiste Apertura hole2 tale che hole1 é una parte di hole2.
(<=>
      (attribute ?HOLE1 Fillable)
      (exists
            (?HOLE2)
            (and
                  (instance ?HOLE2 Hole)
                  (part ?HOLE1 ?HOLE2))))

Se obj riempie parzialmentes hole1, allora esiste hole2 tale che hole2 é una parte di hole1 e obj riempie completamentes hole2.
(=>
      (partiallyFills ?OBJ ?HOLE1)
      (exists
            (?HOLE2)
            (and
                  (part ?HOLE2 ?HOLE1)
                  (completelyFills ?OBJ ?HOLE2))))

Se obj riempie propriamentes hole1, allora esiste hole2 tale che hole2 é una parte di hole1 e obj riempies hole2.
(=>
      (properlyFills ?OBJ ?HOLE1)
      (exists
            (?HOLE2)
            (and
                  (part ?HOLE2 ?HOLE1)
                  (fills ?OBJ ?HOLE2))))

Se obj1 riempie completamentes hole, allora esiste obj2 tale che obj2 é una parte di obj1 e obj2 riempies hole.
(=>
      (completelyFills ?OBJ1 ?HOLE)
      (exists
            (?OBJ2)
            (and
                  (part ?OBJ2 ?OBJ1)
                  (fills ?OBJ2 ?HOLE))))

Se obj1 riempies hole e fillable is an attribute of obj2, allora obj1 non si sovrappone a obj2.
(=>
      (and
            (fills ?OBJ1 ?HOLE)
            (attribute ?OBJ2 Fillable))
      (not
            (overlapsSpatially ?OBJ1 ?OBJ2)))

Se obj1 riempie propriamentes hole e obj2 é connesso a obj1, allora hole é connesso a obj2.
(=>
      (and
            (properlyFills ?OBJ1 ?HOLE)
            (connected ?OBJ2 ?OBJ1))
      (connected ?HOLE ?OBJ2))

Se obj riempies hole1 e hole2 é una Parte propria di hole1, allora obj riempie completamentes hole2.
(=>
      (and
            (fills ?OBJ ?HOLE1)
            (properPart ?HOLE2 ?HOLE1))
      (completelyFills ?OBJ ?HOLE2))

Se obj1 riempies hole e obj2 é una Parte propria di obj1, allora obj2 riempie propriamentes hole.
(=>
      (and
            (fills ?OBJ1 ?HOLE)
            (properPart ?OBJ2 ?OBJ1))
      (properlyFills ?OBJ2 ?HOLE))

Se obj1 is uguale a "la superficie dell'apertura hole", allora per ogni obj2 vale: obj2 si sovrappones a obj1 se e solo se esiste obj3 tale che obj3 é una parte superficiale di " ció che entra nell'apertura hole" e hole incontras obj3 e obj2 si sovrappones a obj3.
(=>
      (equal
            ?OBJ1
            (SkinFn ?HOLE))
      (forall
            (?OBJ2)
            (<=>
                  (overlapsSpatially ?OBJ2 ?OBJ1)
                  (exists
                        (?OBJ3)
                        (and
                              (superficialPart
                                    ?OBJ3
                                    (PrincipalHostFn ?HOLE))
                              (meetsSpatially ?HOLE ?OBJ3)
                              (overlapsSpatially ?OBJ2 ?OBJ3))))))

Se proc é un' istanza di Processo e subproc é un sottoprocesso di proc, allora esiste time tale che subproc esistes durante time.
(=>
      (and
            (instance ?PROC Process)
            (subProcess ?SUBPROC ?PROC))
      (exists
            (?TIME)
            (time ?SUBPROC ?TIME)))

Se proc é un' istanza di ProcesoBiologico, allora esiste Organismo obj tale che proc é localizzato in obj.
(=>
      (instance ?PROC BiologicalProcess)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ Organism)
                  (located ?PROC ?OBJ))))

Se proc é un' istanza di ProcesoBiologico e org esperisces proc, allora org é un' istanza di Organismo.
(=>
      (and
            (instance ?PROC BiologicalProcess)
            (experiencer ?PROC ?ORG))
      (instance ?ORG Organism))

Se birth é un' istanza di Nascita e agent esperisces birth, allora esiste Morte death tale che agent esperisces death.
(=>
      (and
            (instance ?BIRTH Birth)
            (experiencer ?BIRTH ?AGENT))
      (exists
            (?DEATH)
            (and
                  (instance ?DEATH Death)
                  (experiencer ?DEATH ?AGENT))))

Se death é un' istanza di Morte e agent esperisces death, allora "dead is an attribute of agent" vales durante "dopo "il tempo di esistenza di death"".
(=>
      (and
            (instance ?DEATH Death)
            (experiencer ?DEATH ?AGENT))
      (holdsDuring
            (FutureFn
                  (WhenFn ?DEATH))
            (attribute ?AGENT Dead)))

Se death é un' istanza di Morte e birth é un' istanza di Nascita e agent esperisces death e agent esperisces birth, allora esiste time tale che "il tempo di esistenza di birth" incontras time e time incontras "il tempo di esistenza di death" e "living is an attribute of agent" vales durante 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)))))

Se act é un' istanza di Ingestione e food é un paziente di act, allora food é un' istanza di Cibo.
(=>
      (and
            (instance ?ACT Ingesting)
            (patient ?ACT ?FOOD))
      (instance ?FOOD Food))

Se act é un' istanza di Mangiare e food é un paziente di act, allora solid is an attribute of food.
(=>
      (and
            (instance ?ACT Eating)
            (patient ?ACT ?FOOD))
      (attribute ?FOOD Solid))

Se digest é un' istanza di digesting e digest é un agente di organism, allora esiste Ingestione ingest tale che ingest é un agente di organism e "il tempo di esistenza di digest" sovrappones "il tempo di esistenza di ingest".
(=>
      (and
            (instance ?DIGEST Digesting)
            (agent ?DIGEST ?ORGANISM))
      (exists
            (?INGEST)
            (and
                  (instance ?INGEST Ingesting)
                  (agent ?INGEST ?ORGANISM)
                  (overlapsTemporally
                        (WhenFn ?INGEST)
                        (WhenFn ?DIGEST)))))

Se digest é un' istanza di digesting, allora esiste DecomposizioneChimica decomp tale che decomp é un sottoprocesso di digest.
(=>
      (instance ?DIGEST Digesting)
      (exists
            (?DECOMP)
            (and
                  (instance ?DECOMP ChemicalDecomposition)
                  (subProcess ?DECOMP ?DIGEST))))

Se rep é un' istanza di Replicazione e rep é un agente di parent e child é un risultato di rep, allora parent é un parente di child.
(=>
      (and
            (instance ?REP Replication)
            (agent ?REP ?PARENT)
            (result ?REP ?CHILD))
      (parent ?CHILD ?PARENT))

Se rep é un' istanza di Replicazione, allora esiste CorpoRiproduttivo body tale che body é un risultato di rep.
(=>
      (instance ?REP Replication)
      (exists
            (?BODY)
            (and
                  (instance ?BODY ReproductiveBody)
                  (result ?REP ?BODY))))

Se rep é un' istanza di RiproduzioneSessuata e organism é un risultato di rep, allora non esiste mother,father tale che mother é una madre di organism e father é un padre di organism.
(=>
      (and
            (instance ?REP SexualReproduction)
            (result ?REP ?ORGANISM))
      (not
            (exists
                  (?MOTHER ?FATHER)
                  (and
                        (mother ?ORGANISM ?MOTHER)
                        (father ?ORGANISM ?FATHER)))))

Se rep é un' istanza di RiproduzioneAsessuata e organism é un risultato di rep, allora non esiste parent1,parent2 tale che parent1 é un parente di organism e parent2 é un parente di organism e parent1 is not uguale a parent2.
(=>
      (and
            (instance ?REP AsexualReproduction)
            (result ?REP ?ORGANISM))
      (not
            (exists
                  (?PARENT1 ?PARENT2)
                  (and
                        (parent ?ORGANISM ?PARENT1)
                        (parent ?ORGANISM ?PARENT2)
                        (not
                              (equal ?PARENT1 ?PARENT2))))))

Se process é un' istanza di ProcessoPsicologico, allora esiste Animale animal tale che animal esperisces process.
(=>
      (instance ?PROCESS PsychologicalProcess)
      (exists
            (?ANIMAL)
            (and
                  (instance ?ANIMAL Animal)
                  (experiencer ?PROCESS ?ANIMAL))))

Se proc é un' istanza di ProcessoOrganicoOTessutale, allora esiste thing tale che proc é localizzato in thing e thing é un' istanza di Organo o thing é un' istanza di Tessuto.
(=>
      (instance ?PROC OrganOrTissueProcess)
      (exists
            (?THING)
            (and
                  (located ?PROC ?THING)
                  (or
                        (instance ?THING Organ)
                        (instance ?THING Tissue)))))

Se path é un' istanza di ProcessoPatologico e org esperisces path, allora esiste part,MalattiaOSindrome disease tale che part é una parte di org e 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))))

Se inj é un' istanza di Trauma, allora esiste StrutturaAnatomica struct tale che struct é un paziente di inj.
(=>
      (instance ?INJ Injuring)
      (exists
            (?STRUCT)
            (and
                  (instance ?STRUCT AnatomicalStructure)
                  (patient ?INJ ?STRUCT))))

inj é un' istanza di Trauma se e solo se inj é un' istanza di Danneggiare e Organismo é un paziente di inj.
(<=>
      (instance ?INJ Injuring)
      (and
            (instance ?INJ Damaging)
            (patient ?INJ Organism)))

Se poison é un' istanza di Avvelenamento, allora esiste thing tale che thing é un paziente di poison e thing é un' istanza di Organismo o thing é un' istanza di StrutturaAnatomica.
(=>
      (instance ?POISON Poisoning)
      (exists
            (?THING)
            (and
                  (patient ?POISON ?THING)
                  (or
                        (instance ?THING Organism)
                        (instance ?THING AnatomicalStructure)))))

Se poison é un' istanza di Avvelenamento, allora esiste SostanzaBiologicamenteAttiva substance tale che substance é uno strumento per poison.
(=>
      (instance ?POISON Poisoning)
      (exists
            (?SUBSTANCE)
            (and
                  (instance ?SUBSTANCE BiologicallyActiveSubstance)
                  (instrument ?POISON ?SUBSTANCE))))

Se proc é un' istanza di ProcessoIntenzionale e proc é un agente di agent, allora esiste purp tale che proc ha &n scopo purp per agent.
(=>
      (and
            (instance ?PROC IntentionalProcess)
            (agent ?PROC ?AGENT))
      (exists
            (?PURP)
            (hasPurposeForAgent ?PROC ?PURP ?AGENT)))

Se proc é un' istanza di ProcessoIntenzionale, allora esiste AgenteCognitivo agent tale che proc é un agente di agent.
(=>
      (instance ?PROC IntentionalProcess)
      (exists
            (?AGENT)
            (and
                  (instance ?AGENT CognitiveAgent)
                  (agent ?PROC ?AGENT))))

Se act é un' istanza di ProcessoOrganizzativo e act é un agente di agent, allora
(=>
      (and
            (instance ?ACT OrganizationalProcess)
            (agent ?ACT ?AGENT))
      (or
            (instance ?AGENT Organization)
            (exists
                  (?ORG)
                  (and
                        (instance ?ORG Organization)
                        (member ?AGENT ?ORG)))))

Se act é un' istanza di ProcessoReligioso e act é un agente di agent, allora
(=>
      (and
            (instance ?ACT ReligiousProcess)
            (agent ?ACT ?AGENT))
      (or
            (instance ?AGENT ReligiousOrganization)
            (exists
                  (?ORG)
                  (and
                        (member ?AGENT ?ORG)
                        (instance ?ORG ReligiousOrganization)))))

Se join é un' istanza di AdesioneAdUn'Organizzazione e org é un' istanza di Organizzazione e join é un agente di org e person é un paziente di join, allora "person é un membro di org" vales durante "immediatamente dopo "il tempo di esistenza di join"".
(=>
      (and
            (instance ?JOIN JoiningAnOrganization)
            (instance ?ORG Organization)
            (agent ?JOIN ?ORG)
            (patient ?JOIN ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?JOIN))
            (member ?PERSON ?ORG)))

Se leave é un' istanza di AbbandonoDiUn'Organizzazione e org é un' istanza di Organizzazione e leave é un agente di org e person é un paziente di leave, allora "person é not un membro di org" vales durante "immediatamente dopo "il tempo di esistenza di leave"".
(=>
      (and
            (instance ?LEAVE LeavingAnOrganization)
            (instance ?ORG Organization)
            (agent ?LEAVE ?ORG)
            (patient ?LEAVE ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?LEAVE))
            (not
                  (member ?PERSON ?ORG))))

Se grad é un' istanza di ConseguimentoDiplomiAccademici e grad é un agente di org e person é un paziente di grad, allora org é un' istanza di OrganizzazioneEducativa.
(=>
      (and
            (instance ?GRAD Graduation)
            (agent ?GRAD ?ORG)
            (patient ?GRAD ?PERSON))
      (instance ?ORG EducationalOrganization))

Se mat é un' istanza di Iscrizione e mat é un agente di org e person é un paziente di mat, allora org é un' istanza di OrganizzazioneEducativa.
(=>
      (and
            (instance ?MAT Matriculation)
            (agent ?MAT ?ORG)
            (patient ?MAT ?PERSON))
      (instance ?ORG EducationalOrganization))

Se hire é un' istanza di Assunzione e org é un' istanza di Organizzazione e hire é un agente di org e person é un paziente di hire, allora "org impiegas person" vales durante "immediatamente dopo "il tempo di esistenza di hire"".
(=>
      (and
            (instance ?HIRE Hiring)
            (instance ?ORG Organization)
            (agent ?HIRE ?ORG)
            (patient ?HIRE ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?HIRE))
            (employs ?ORG ?PERSON)))

Se fire é un' istanza di CessazioneDiRapportoLavorativo e org é un' istanza di Organizzazione e fire é un agente di org e person é un paziente di fire, allora "org non impiega person" vales durante "immediatamente dopo "il tempo di esistenza di fire"".
(=>
      (and
            (instance ?FIRE TerminatingEmployment)
            (instance ?ORG Organization)
            (agent ?FIRE ?ORG)
            (patient ?FIRE ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?FIRE))
            (not
                  (employs ?ORG ?PERSON))))

Se proc é un' istanza di ProcessoPolitico, allora esiste Governo gov tale che proc é un agente di gov o gov é un paziente di proc.
(=>
      (instance ?PROC PoliticalProcess)
      (exists
            (?GOV)
            (and
                  (instance ?GOV Government)
                  (or
                        (agent ?PROC ?GOV)
                        (patient ?PROC ?GOV)))))

Se increase é un' istanza di Aumento e obj é un paziente di increase, allora esiste unit,quant1,quant2 tale che ""obj unit(s" is uguale a quant1" vales durante "immediatamente prima di "il tempo di esistenza di increase"" e ""obj unit(s" is uguale a quant2" vales durante "immediatamente dopo "il tempo di esistenza di increase"" e quant2 é più grande di 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))))

Se heat é un' istanza di Riscaldamento e obj é un paziente di heat, allora esiste MisuraDiTemperatura unit,quant1,quant2 tale che ""obj unit(s" is uguale a quant1" vales durante "immediatamente prima di "il tempo di esistenza di heat"" e ""obj unit(s" is uguale a quant2" vales durante "immediatamente dopo "il tempo di esistenza di heat"" e quant2 é più grande di 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))))

Se decrease é un' istanza di Diminuzione e obj é un paziente di decrease, allora esiste unit,quant1,quant2 tale che ""obj unit(s" is uguale a quant1" vales durante "immediatamente prima di "il tempo di esistenza di decrease"" e ""obj unit(s" is uguale a quant2" vales durante "immediatamente dopo "il tempo di esistenza di decrease"" e quant2 é meno diquant1.
(=>
      (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))))

Se cool é un' istanza di Raffreddamento e obj é un paziente di cool, allora esiste MisuraDiTemperatura unit,quant1,quant2 tale che ""obj unit(s" is uguale a quant1" vales durante "immediatamente prima di "il tempo di esistenza di cool"" e ""obj unit(s" is uguale a quant2" vales durante "immediatamente dopo "il tempo di esistenza di cool"" e quant2 é meno diquant1.
(=>
      (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))))

Se motion é un' istanza di Movimento e obj é un paziente di motion e motion si originas in place, allora "obj é localizzato in place" vales durante "immediatamente prima di "il tempo di esistenza di motion"".
(=>
      (and
            (instance ?MOTION Motion)
            (patient ?MOTION ?OBJ)
            (origin ?MOTION ?PLACE))
      (holdsDuring
            (ImmediatePastFn
                  (WhenFn ?MOTION))
            (located ?OBJ ?PLACE)))

Se motion é un' istanza di Movimento e obj é un paziente di motion e motion fines in place, allora "obj é localizzato in place" vales durante "immediatamente dopo "il tempo di esistenza di motion"".
(=>
      (and
            (instance ?MOTION Motion)
            (patient ?MOTION ?OBJ)
            (destination ?MOTION ?PLACE))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?MOTION))
            (located ?OBJ ?PLACE)))

(=>
      (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))))

Se motion é un' istanza di MovimentoCorporeo, allora esiste ParteDelCorpo obj,Organismo agent tale che obj é un paziente di motion e motion é un agente di agent.
(=>
      (instance ?MOTION BodyMotion)
      (exists
            (?OBJ ?AGENT)
            (and
                  (instance ?OBJ BodyPart)
                  (patient ?MOTION ?OBJ)
                  (instance ?AGENT Organism)
                  (agent ?MOTION ?AGENT))))

Se walk é un' istanza di Camminare e walk é un agente di agent, allora esiste SuperficieTerrestre area tale che agent é localizzato in area.
(=>
      (and
            (instance ?WALK Walking)
            (agent ?WALK ?AGENT))
      (exists
            (?AREA)
            (and
                  (instance ?AREA LandArea)
                  (located ?AGENT ?AREA))))

Se swim é un' istanza di Nuotare e swim é un agente di agent, allora esiste SuperficieAcquatica area tale che agent é localizzato in area.
(=>
      (and
            (instance ?SWIM Swimming)
            (agent ?SWIM ?AGENT))
      (exists
            (?AREA)
            (and
                  (instance ?AREA WaterArea)
                  (located ?AGENT ?AREA))))

Se proc é un' istanza di CambioDiDirezione, allora esiste AttributoDirezionale attr tale che
(=>
      (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))))))))

Se transfer é un' istanza di Trasferimento e transfer é un agente di agent e patient é un paziente di transfer, allora agent is not uguale a patient.
(=>
      (and
            (instance ?TRANSFER Transfer)
            (agent ?TRANSFER ?AGENT)
            (patient ?TRANSFER ?PATIENT))
      (not
            (equal ?AGENT ?PATIENT)))

Se remove é un' istanza di Spostamento e remove si originas in place e obj é un paziente di remove, allora "obj é localizzato in place" vales durante "immediatamente prima di "il tempo di esistenza di remove"" e "obj é not localizzato in place" vales durante "immediatamente dopo "il tempo di esistenza di 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)))))

Se put é un' istanza di Porre e put fines in place e obj é un paziente di put, allora "obj é not localizzato in place" vales durante "immediatamente prima di "il tempo di esistenza di put"" e "obj é localizzato in place" vales durante "immediatamente dopo "il tempo di esistenza di 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))))

Se sub é un' istanza di Sostituzione, allora esiste Porre put,Spostamento remove,obj1,obj2,place tale che put é un sottoprocesso di sub e remove é un sottoprocesso di sub e obj1 é un paziente di remove e remove si originas in place e obj2 é un paziente di put e put fines in place e obj1 is not uguale a 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)))))

Se touch é un' istanza di Toccare e touch é un agente di obj1 e obj2 é un paziente di touch, allora "obj1 é connesso a obj2" vales durante "immediatamente dopo "il tempo di esistenza di touch"".
(=>
      (and
            (instance ?TOUCH Touching)
            (agent ?TOUCH ?OBJ1)
            (patient ?TOUCH ?OBJ2))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?TOUCH))
            (connected ?OBJ1 ?OBJ2)))

Se impact é un' istanza di Impatto e obj é un paziente di impact, allora esiste Spinta impel tale che obj é un paziente di impel e "il tempo di esistenza di impel" accades prima di "il tempo di esistenza di impact".
(=>
      (and
            (instance ?IMPACT Impacting)
            (patient ?IMPACT ?OBJ))
      (exists
            (?IMPEL)
            (and
                  (instance ?IMPEL Impelling)
                  (patient ?IMPEL ?OBJ)
                  (earlier
                        (WhenFn ?IMPEL)
                        (WhenFn ?IMPACT)))))

Se trans é un' istanza di Trasporto, allora esiste MezzoDiTrasporto device tale che device é uno strumento per trans.
(=>
      (instance ?TRANS Transportation)
      (exists
            (?DEVICE)
            (and
                  (instance ?DEVICE TransportationDevice)
                  (instrument ?TRANS ?DEVICE))))

Se steer é un' istanza di Pilotare, allora esiste MezzoDiTrasporto vehicle tale che vehicle é un paziente di steer.
(=>
      (instance ?STEER Steering)
      (exists
            (?VEHICLE)
            (and
                  (instance ?VEHICLE TransportationDevice)
                  (patient ?STEER ?VEHICLE))))

Se education é un' istanza di ProcessoEducazionale e person é un paziente di education, allora education ha scopo "esiste Apprendere learn tale che person é un paziente di learn".
(=>
      (and
            (instance ?EDUCATION EducationalProcess)
            (patient ?EDUCATION ?PERSON))
      (hasPurpose
            ?EDUCATION
            (exists
                  (?LEARN)
                  (and
                        (instance ?LEARN Learning)
                        (patient ?LEARN ?PERSON)))))

Se change é un' istanza di CambiamentodiPossesso e obj é un paziente di change e "agent1 possiedees obj" vales durante "immediatamente prima di "il tempo di esistenza di change"" e "agent2 possiedees obj" vales durante "immediatamente dopo "il tempo di esistenza di change"", allora agent1 is not uguale a 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)))

Se change é un' istanza di CambiamentodiPossesso e change si originas in agent1 e change fines in agent2 e agent2 é un' istanza di Agente e obj é un paziente di change, allora "agent1 possiedees obj" vales durante "immediatamente prima di "il tempo di esistenza di change"" e "agent2 possiedees obj" vales durante "immediatamente dopo "il tempo di esistenza di 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))))

Se give é un' istanza di Dare e give é un agente di agent1 e give fines in agent2 e agent2 é un' istanza di Agente e obj é un paziente di give, allora esiste Ottenere get tale che get é un agente di agent2 e get si originas in agent1 e obj é un paziente di 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))))

Se give é un' istanza di Dare e give é un agente di agent, allora give si originas in agent.
(=>
      (and
            (instance ?GIVE Giving)
            (agent ?GIVE ?AGENT))
      (origin ?GIVE ?AGENT))

Se give é un' istanza di Donazione, allora non esiste Scambio trans tale che give é un sottoprocesso di trans.
(=>
      (instance ?GIVE UnilateralGiving)
      (not
            (exists
                  (?TRANS)
                  (and
                        (instance ?TRANS Transaction)
                        (subProcess ?GIVE ?TRANS)))))

Esiste PrendereInPrestito borrow tale che borrow é un agente di agent1 e borrow si originas in agent2 e object é un paziente di borrow se e solo se esiste DareInPrestito lend tale che lend é un agente di agent2 e lend fines in agent1 e object é un paziente di lend.
(<=>
      (exists
            (?BORROW)
            (and
                  (instance ?BORROW Borrowing)
                  (agent ?BORROW ?AGENT1)
                  (origin ?BORROW ?AGENT2)
                  (patient ?BORROW ?OBJECT)))
      (exists
            (?LEND)
            (and
                  (instance ?LEND Lending)
                  (agent ?LEND ?AGENT2)
                  (destination ?LEND ?AGENT1)
                  (patient ?LEND ?OBJECT))))

Se get é un' istanza di Ottenere e get é un agente di agent, allora get fines in agent.
(=>
      (and
            (instance ?GET Getting)
            (agent ?GET ?AGENT))
      (destination ?GET ?AGENT))

Se get é un' istanza di PrenderePossesso, allora non esiste Scambio trans tale che get é un sottoprocesso di trans.
(=>
      (instance ?GET UnilateralGetting)
      (not
            (exists
                  (?TRANS)
                  (and
                        (instance ?TRANS Transaction)
                        (subProcess ?GET ?TRANS)))))

Se trans é un' istanza di Scambio, allora esiste agent1,agent2,Dare give1,Dare give2,obj1,obj2 tale che give1 é un sottoprocesso di trans e give2 é un sottoprocesso di trans e give1 é un agente di agent1 e give2 é un agente di agent2 e obj1 é un paziente di give1 e obj2 é un paziente di give2 e give1 fines in agent2 e give2 fines in agent1 e agent1 is not uguale a agent2 e obj1 is not uguale a 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)))))

Se trans é un' istanza di ScambioFinanziario, allora esiste MisuraMonetaria obj tale che obj é un paziente di trans.
(=>
      (instance ?TRANS FinancialTransaction)
      (exists
            (?OBJ)
            (and
                  (patient ?TRANS ?OBJ)
                  (instance ?OBJ CurrencyMeasure))))

Se buy é un' istanza di Acquistare e buy é un agente di agent, allora buy fines in agent.
(=>
      (and
            (instance ?BUY Buying)
            (agent ?BUY ?AGENT))
      (destination ?BUY ?AGENT))

Esiste Acquistare buy tale che buy é un agente di agent1 e buy si originas in agent2 e object é un paziente di buy se e solo se esiste Vendere sell tale che sell é un agente di agent2 e sell fines in agent1 e object é un paziente di sell.
(<=>
      (exists
            (?BUY)
            (and
                  (instance ?BUY Buying)
                  (agent ?BUY ?AGENT1)
                  (origin ?BUY ?AGENT2)
                  (patient ?BUY ?OBJECT)))
      (exists
            (?SELL)
            (and
                  (instance ?SELL Selling)
                  (agent ?SELL ?AGENT2)
                  (destination ?SELL ?AGENT1)
                  (patient ?SELL ?OBJECT))))

Se sell é un' istanza di Vendere e sell é un agente di agent, allora sell si originas in agent.
(=>
      (and
            (instance ?SELL Selling)
            (agent ?SELL ?AGENT))
      (origin ?SELL ?AGENT))

Se learn é un' istanza di Apprendere e learn é un agente di agent, allora agent é un' istanza di AgenteCognitivo.
(=>
      (and
            (instance ?LEARN Learning)
            (agent ?LEARN ?AGENT))
      (instance ?AGENT CognitiveAgent))

Se "esiste Apprendere learn tale che learn é un agente di agent e prop é un paziente di learn" vales durante time, allora "agent believes prop" vales durante "immediatamente dopo time".
(=>
      (holdsDuring
            ?TIME
            (exists
                  (?LEARN)
                  (and
                        (instance ?LEARN Learning)
                        (agent ?LEARN ?AGENT)
                        (patient ?LEARN ?PROP))))
      (holdsDuring
            (ImmediateFutureFn ?TIME)
            (believes ?AGENT ?PROP)))

Se meas é un' istanza di Misurare e meas é un agente di agent e obj é un paziente di meas, allora esiste quant,unit tale che "agent conosces "lamisura obj é "quant unit(s""" vales durante "immediatamente dopo "il tempo di esistenza di 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))))))

Se count é un' istanza di Contare e count é un agente di agent e entity é un paziente di count, allora esiste number tale che agent conosces ""il numero di istanzia in entity" is uguale a number".
(=>
      (and
            (instance ?COUNT Counting)
            (agent ?COUNT ?AGENT)
            (patient ?COUNT ?ENTITY))
      (exists
            (?NUMBER)
            (knows
                  ?AGENT
                  (equal
                        (CardinalityFn ?ENTITY)
                        ?NUMBER))))

Se predict é un' istanza di Prevedere e formula é un paziente di predict, allora esiste time tale che formula vales durante time e time succede?{s} prima di "il tempo di esistenza di predict" o time accades prima di "il tempo di esistenza di predict".
(=>
      (and
            (instance ?PREDICT Predicting)
            (patient ?PREDICT ?FORMULA))
      (exists
            (?TIME)
            (and
                  (holdsDuring ?TIME ?FORMULA)
                  (or
                        (before
                              ?TIME
                              (WhenFn ?PREDICT))
                        (earlier
                              ?TIME
                              (WhenFn ?PREDICT))))))

Se remember é un' istanza di Ricordare e formula é un paziente di remember, allora esiste time tale che formula vales durante time e time succede?{s} prima di "il tempo di esistenza di remember" o time accades prima di "il tempo di esistenza di remember".
(=>
      (and
            (instance ?REMEMBER Remembering)
            (patient ?REMEMBER ?FORMULA))
      (exists
            (?TIME)
            (and
                  (holdsDuring ?TIME ?FORMULA)
                  (or
                        (before
                              ?TIME
                              (WhenFn ?REMEMBER))
                        (earlier
                              ?TIME
                              (WhenFn ?REMEMBER))))))

Se keep é un' istanza di Trattenere e keep é un agente di agent e obj é un paziente di keep, allora esiste Porre put tale che put é un agente di agent e obj é un paziente di put e "il tempo di esistenza di put" accades prima di "il tempo di esistenza di 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)))))

(=>
      (and
            (instance ?KEEP Keeping)
            (patient ?KEEP ?OBJ))
      (exists
            (?PLACE)
            (forall
                  (?TIME)
                  (=>
                        (temporalPart
                              ?TIME
                              (WhenFn ?KEEP))
                        (holdsDuring
                              ?TIME
                              (located ?OBJ ?PLACE))))))

Se confine é un' istanza di Imprigionare, allora esiste Umano human tale che human é un paziente di confine.
(=>
      (instance ?CONFINE Confining)
      (exists
            (?HUMAN)
            (and
                  (instance ?HUMAN Human)
                  (patient ?CONFINE ?HUMAN))))

Se confine é un' istanza di Imprigionare e person é un paziente di confine, allora person non desidera "person é un paziente di confine".
(=>
      (and
            (instance ?CONFINE Confining)
            (patient ?CONFINE ?PERSON))
      (not
            (desires
                  ?PERSON
                  (patient ?CONFINE ?PERSON))))

Se repair é un' istanza di Riparare e obj é un paziente di repair, allora esiste Danneggiare damage tale che obj é un paziente di damage e "il tempo di esistenza di damage" accades prima di "il tempo di esistenza di repair".
(=>
      (and
            (instance ?REPAIR Repairing)
            (patient ?REPAIR ?OBJ))
      (exists
            (?DAMAGE)
            (and
                  (instance ?DAMAGE Damaging)
                  (patient ?DAMAGE ?OBJ)
                  (earlier
                        (WhenFn ?DAMAGE)
                        (WhenFn ?REPAIR)))))

Se proc é un' istanza di ProcessoTerapeutico e bio é un paziente di proc, allora
(=>
      (and
            (instance ?PROC TherapeuticProcess)
            (patient ?PROC ?BIO))
      (or
            (instance ?BIO Organism)
            (exists
                  (?ORG)
                  (and
                        (instance ?ORG Organism)
                        (part ?BIO ?ORG)))))

Se act é un' istanza di InterventoChirurgico e animal é un paziente di act, allora esiste Tagliare subact tale che animal é un' istanza di Animale e cutting é un paziente di animal e subact é un sottoprocesso di act.
(=>
      (and
            (instance ?ACT Surgery)
            (patient ?ACT ?ANIMAL))
      (exists
            (?SUBACT)
            (and
                  (instance ?SUBACT Cutting)
                  (instance ?ANIMAL Animal)
                  (patient ?ANIMAL ?CUTTING)
                  (subProcess ?SUBACT ?ACT))))

process é un' istanza di Distruggere se e solo se esiste patient tale che patient é un paziente di process e patient esistes durante "immediatamente prima di "il tempo di esistenza di process"" e patient non esiste durante "immediatamente dopo "il tempo di esistenza di process"".
(<=>
      (instance ?PROCESS Destruction)
      (exists
            (?PATIENT)
            (and
                  (patient ?PROCESS ?PATIENT)
                  (time
                        ?PATIENT
                        (ImmediatePastFn
                              (WhenFn ?PROCESS)))
                  (not
                        (time
                              ?PATIENT
                              (ImmediateFutureFn
                                    (WhenFn ?PROCESS)))))))

Se kill é un' istanza di Uccidere e kill é un agente di agent e patient é un paziente di kill, allora agent é un' istanza di Organismo e patient é un' istanza di Organismo.
(=>
      (and
            (instance ?KILL Killing)
            (agent ?KILL ?AGENT)
            (patient ?KILL ?PATIENT))
      (and
            (instance ?AGENT Organism)
            (instance ?PATIENT Organism)))

Se kill é un' istanza di Uccidere e patient é un paziente di kill, allora "living is an attribute of patient" vales durante "immediatamente prima di "il tempo di esistenza di kill"" e "dead is an attribute of patient" vales durante "dopo "il tempo di esistenza di kill"".
(=>
      (and
            (instance ?KILL Killing)
            (patient ?KILL ?PATIENT))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?KILL))
                  (attribute ?PATIENT Living))
            (holdsDuring
                  (FutureFn
                        (WhenFn ?KILL))
                  (attribute ?PATIENT Dead))))

Se poke é un' istanza di Perforare e poke é un agente di agent e obj é un paziente di poke e inst é uno strumento per poke, allora "inst connette agent e obj" vales durante "il tempo di esistenza di poke".
(=>
      (and
            (instance ?POKE Poking)
            (agent ?POKE ?AGENT)
            (patient ?POKE ?OBJ)
            (instrument ?POKE ?INST))
      (holdsDuring
            (WhenFn ?POKE)
            (connects ?INST ?AGENT ?OBJ)))

Se attach é un' istanza di Attaccare e obj1 é un paziente di attach e obj2 é un paziente di attach, allora "obj1 é not connesso a obj2" vales durante "immediatamente prima di "il tempo di esistenza di attach"" e "obj1 é connesso a obj2" vales durante "immediatamente dopo "il tempo di esistenza di 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))))

Se detach é un' istanza di Staccare e obj1 é un paziente di detach e obj2 é un paziente di detach, allora "obj1 é connesso a obj2" vales durante "immediatamente prima di "il tempo di esistenza di detach"" e "obj1 é not connesso a obj2" vales durante "immediatamente dopo "il tempo di esistenza di 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)))))

combine é un' istanza di Combinare e obj1 é una risorsa per combine e obj2 é un risultato di combine se e solo se "obj1 é not una parte di obj2" vales durante "immediatamente prima di "il tempo di esistenza di combine"" e "obj1 é una parte di obj2" vales durante "immediatamente dopo "il tempo di esistenza di combine"".
(<=>
      (and
            (instance ?COMBINE Combining)
            (resource ?COMBINE ?OBJ1)
            (result ?COMBINE ?OBJ2))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?COMBINE))
                  (not
                        (part ?OBJ1 ?OBJ2)))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?COMBINE))
                  (part ?OBJ1 ?OBJ2))))

Se , allora stuff é un' istanza di SostanzaPura.
(=>
      (and
            (instance ?PROC ChemicalProcess)
            (or
                  (resource ?PROC ?STUFF)
                  (result ?PROC ?STUFF)))
      (instance ?STUFF PureSubstance))

Se substance1 é una risorsa per proc e substance2 é un risultato di proc e substance1 é un' istanza di SostanzaElementare e substance2 é un' istanza di Composto, allora proc é un' istanza di SintesiChimica.
(=>
      (and
            (resource ?PROC ?SUBSTANCE1)
            (result ?PROC ?SUBSTANCE2)
            (instance ?SUBSTANCE1 ElementalSubstance)
            (instance ?SUBSTANCE2 CompoundSubstance))
      (instance ?PROC ChemicalSynthesis))

compound é un' istanza di Composto se e solo se esiste SostanzaElementare element1,SostanzaElementare element2,SintesiChimica process tale che element1 is not uguale a element2 e element1 é una risorsa per process e element2 é una risorsa per process e compound é un risultato di process.
(<=>
      (instance ?COMPOUND CompoundSubstance)
      (exists
            (?ELEMENT1 ?ELEMENT2 ?PROCESS)
            (and
                  (instance ?ELEMENT1 ElementalSubstance)
                  (instance ?ELEMENT2 ElementalSubstance)
                  (not
                        (equal ?ELEMENT1 ?ELEMENT2))
                  (instance ?PROCESS ChemicalSynthesis)
                  (resource ?PROCESS ?ELEMENT1)
                  (resource ?PROCESS ?ELEMENT2)
                  (result ?PROCESS ?COMPOUND))))

Se substance1 é una risorsa per proc e substance2 é un risultato di proc e substance1 é un' istanza di Composto e substance2 é un' istanza di SostanzaElementare, allora proc é un' istanza di DecomposizioneChimica.
(=>
      (and
            (resource ?PROC ?SUBSTANCE1)
            (result ?PROC ?SUBSTANCE2)
            (instance ?SUBSTANCE1 CompoundSubstance)
            (instance ?SUBSTANCE2 ElementalSubstance))
      (instance ?PROC ChemicalDecomposition))

Se combustion é un' istanza di Combustione, allora esiste Riscaldamento heat,RadiazioneLuminosa light tale che heat é un sottoprocesso di combustion e light é un sottoprocesso di combustion.
(=>
      (instance ?COMBUSTION Combustion)
      (exists
            (?HEAT ?LIGHT)
            (and
                  (instance ?HEAT Heating)
                  (instance ?LIGHT RadiatingLight)
                  (subProcess ?HEAT ?COMBUSTION)
                  (subProcess ?LIGHT ?COMBUSTION))))

Se change é un' istanza di CambiamentoInterno e obj é un paziente di change, allora esiste property tale che
(=>
      (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))))))

Se alt é un' istanza di CambiamentoDiSuperficie e obj é un paziente di alt, allora esiste part,property tale che part é una parte superficiale di obj e "property is an attribute of part" vales durante "immediatamente prima di "il tempo di esistenza di alt"" e "property is not an attribute of part" vales durante "immediatamente dopo "il tempo di esistenza di 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))))))

Se alt é un' istanza di CambiamentoDiForma e obj é un paziente di alt, allora esiste AttributoDiForma property tale che
(=>
      (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)))))))

Se coloring é un' istanza di Colorare e obj é un paziente di coloring, allora esiste AttributoDiColore property tale che "property is an attribute of obj" vales durante "immediatamente prima di "il tempo di esistenza di coloring"" e "property is not an attribute of obj" vales durante "immediatamente dopo "il tempo di esistenza di 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))))))

Se develop é un' istanza di SviluppoDelContenuto, allora esiste OggettoSemiotico obj tale che obj é un paziente di develop.
(=>
      (instance ?DEVELOP ContentDevelopment)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ ContentBearingObject)
                  (patient ?DEVELOP ?OBJ))))

Se read é un' istanza di Leggere, allora esiste Testo text,prop tale che text contienes informazione prop e read esprime il contenuto di prop.
(=>
      (instance ?READ Reading)
      (exists
            (?TEXT ?PROP)
            (and
                  (instance ?TEXT Text)
                  (containsInformation ?TEXT ?PROP)
                  (realization ?READ ?PROP))))

Se decode é un' istanza di Decodificare e doc1 é un paziente di decode, allora esiste encode,doc2,time tale che doc2 contienes informazione prop e doc1 contienes informazione prop e time é una parte di"prima "il tempo di esistenza di decode"" e "encode é un' istanza di Codificare e doc2 é un paziente di encode" vales durante 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))))))

Se wet é un' istanza di Bagnare e obj é un paziente di wet, allora "wet is an attribute of obj o damp is an attribute of obj" vales durante "immediatamente dopo "il tempo di esistenza di wet"".
(=>
      (and
            (instance ?WET Wetting)
            (patient ?WET ?OBJ))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?WET))
            (or
                  (attribute ?OBJ Wet)
                  (attribute ?OBJ Damp))))

Se wet é un' istanza di Bagnare, allora esiste obj tale che liquid is an attribute of obj e obj é un paziente di wet.
(=>
      (instance ?WET Wetting)
      (exists
            (?OBJ)
            (and
                  (attribute ?OBJ Liquid)
                  (patient ?WET ?OBJ))))

Se dry é un' istanza di Asciugare e obj é un paziente di dry, allora "dry is an attribute of obj" vales durante "immediatamente dopo "il tempo di esistenza di dry"".
(=>
      (and
            (instance ?DRY Drying)
            (patient ?DRY ?OBJ))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?DRY))
            (attribute ?OBJ Dry)))

process é un' istanza di Creazione se e solo se esiste patient tale che patient é un paziente di process e patient esistes durante "immediatamente dopo "il tempo di esistenza di process"" e patient non esiste durante "immediatamente prima di "il tempo di esistenza di process"".
(<=>
      (instance ?PROCESS Creation)
      (exists
            (?PATIENT)
            (and
                  (patient ?PROCESS ?PATIENT)
                  (time
                        ?PATIENT
                        (ImmediateFutureFn
                              (WhenFn ?PROCESS)))
                  (not
                        (time
                              ?PATIENT
                              (ImmediatePastFn
                                    (WhenFn ?PROCESS)))))))

Esiste Costruzione build tale che artifact é un risultato di build se e solo se artifact é un' istanza di ManufattoStatico.
(<=>
      (exists
            (?BUILD)
            (and
                  (instance ?BUILD Constructing)
                  (result ?BUILD ?ARTIFACT)))
      (instance ?ARTIFACT StationaryArtifact))

Se pub é un' istanza di Editoria e text é un paziente di pub, allora text é una sottoclasse di Testo.
(=>
      (and
            (instance ?PUB Publication)
            (patient ?PUB ?TEXT))
      (subclass ?TEXT Text))

Se cook é un' istanza di Cucinare, allora esiste Cibo food tale che food é un risultato di cook.
(=>
      (instance ?COOK Cooking)
      (exists
            (?FOOD)
            (and
                  (instance ?FOOD Food)
                  (result ?COOK ?FOOD))))

Se search é un' istanza di Ricercare e search é un agente di agent e entity é un paziente di search, allora agent é interessato a entity.
(=>
      (and
            (instance ?SEARCH Searching)
            (agent ?SEARCH ?AGENT)
            (patient ?SEARCH ?ENTITY))
      (inScopeOfInterest ?AGENT ?ENTITY))

Se pursue é un' istanza di Cercare e pursue é un agente di agent e obj é un paziente di pursue, allora "agent vuoles obj" vales durante pursue.
(=>
      (and
            (instance ?PURSUE Pursuing)
            (agent ?PURSUE ?AGENT)
            (patient ?PURSUE ?OBJ))
      (holdsDuring
            ?PURSUE
            (wants ?AGENT ?OBJ)))

Se pursue é un' istanza di Cercare e pursue é un agente di agent e obj é un paziente di pursue, allora "agent non possiede obj" vales durante pursue.
(=>
      (and
            (instance ?PURSUE Pursuing)
            (agent ?PURSUE ?AGENT)
            (patient ?PURSUE ?OBJ))
      (holdsDuring
            ?PURSUE
            (not
                  (possesses ?AGENT ?OBJ))))

Se investigate é un' istanza di Investigare e prop é un paziente di investigate, allora prop é un' istanza di Formula.
(=>
      (and
            (instance ?INVESTIGATE Investigating)
            (patient ?INVESTIGATE ?PROP))
      (instance ?PROP Formula))

Se investigate é un' istanza di Investigare e investigate é un agente di agent e prop é un paziente di investigate, allora "agent non conosce prop" vales durante "il tempo di esistenza di investigate".
(=>
      (and
            (instance ?INVESTIGATE Investigating)
            (agent ?INVESTIGATE ?AGENT)
            (patient ?INVESTIGATE ?PROP))
      (holdsDuring
            (WhenFn ?INVESTIGATE)
            (not
                  (knows ?AGENT ?PROP))))

Se proc é un' istanza di ProcessoDiagnostico e proc é un agente di agent, allora esiste cause tale che proc ha &n scopo "agent conosces "cause causas proc"" per agent.
(=>
      (and
            (instance ?PROC DiagnosticProcess)
            (agent ?PROC ?AGENT))
      (exists
            (?CAUSE)
            (hasPurposeForAgent
                  ?PROC
                  (knows
                        ?AGENT
                        (causes ?CAUSE ?PROC))
                  ?AGENT)))

Se interaction é un' istanza di InterazioneSociale, allora esiste agent1,agent2 tale che interaction é un agente di agent1 e interaction é un agente di agent2 e agent1 is not uguale a agent2.
(=>
      (instance ?INTERACTION SocialInteraction)
      (exists
            (?AGENT1 ?AGENT2)
            (and
                  (agent ?INTERACTION ?AGENT1)
                  (agent ?INTERACTION ?AGENT2)
                  (not
                        (equal ?AGENT1 ?AGENT2)))))

Se pretend é un' istanza di Fingere, allora esiste person,prop tale che pretend ha scopo "person believes prop" e prop é true.
(=>
      (instance ?PRETEND Pretending)
      (exists
            (?PERSON ?PROP)
            (and
                  (hasPurpose
                        ?PRETEND
                        (believes ?PERSON ?PROP))
                  (true ?PROP True))))

Se communicate é un' istanza di Comunicazione, allora esiste OggettoSemiotico obj,AgenteCognitivo agent1,AgenteCognitivo agent2 tale che obj é un paziente di communicate e communicate é un agente di agent1 e communicate fines in 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))))

Se disseminate é un' istanza di Diffusione, allora esiste AgenteCognitivo agent1,AgenteCognitivo agent2 tale che disseminate fines in agent1 e disseminate fines in agent2 e agent1 is not uguale a agent2.
(=>
      (instance ?DISSEMINATE Disseminating)
      (exists
            (?AGENT1 ?AGENT2)
            (and
                  (destination ?DISSEMINATE ?AGENT1)
                  (instance ?AGENT1 CognitiveAgent)
                  (destination ?DISSEMINATE ?AGENT2)
                  (instance ?AGENT2 CognitiveAgent)
                  (not
                        (equal ?AGENT1 ?AGENT2)))))

Se advert é un' istanza di Pubblicitá, allora esiste obj tale che advert include un riferimento a obj e advert ha scopo "esiste Vendere sale tale che obj é un paziente di sale".
(=>
      (instance ?ADVERT Advertising)
      (exists
            (?OBJ)
            (and
                  (refers ?ADVERT ?OBJ)
                  (hasPurpose
                        ?ADVERT
                        (exists
                              (?SALE)
                              (and
                                    (instance ?SALE Selling)
                                    (patient ?SALE ?OBJ)))))))

Se communicate é un' istanza di linguistic communication, allora esiste EspressioneLinguistica obj tale che obj é un paziente di communicate.
(=>
      (instance ?COMMUNICATE LinguisticCommunication)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ LinguisticExpression)
                  (patient ?COMMUNICATE ?OBJ))))

Se state é un' istanza di Affermare e state é un agente di agent e formula é un paziente di state e formula é un' istanza di Formula, allora "agent believes formula" vales durante "il tempo di esistenza di state".
(=>
      (and
            (instance ?STATE Stating)
            (agent ?STATE ?AGENT)
            (patient ?STATE ?FORMULA)
            (instance ?FORMULA Formula))
      (holdsDuring
            (WhenFn ?STATE)
            (believes ?AGENT ?FORMULA)))

Se order é un' istanza di Comandare e formula é un paziente di order, allora l'affermazione formula ha il modello di forza di obligation.
(=>
      (and
            (instance ?ORDER Ordering)
            (patient ?ORDER ?FORMULA))
      (modalAttribute ?FORMULA Obligation))

Se request é un' istanza di Richiedere e request é un agente di agent e formula é un paziente di request e formula é un' istanza di Formula, allora agent desideras formula.
(=>
      (and
            (instance ?REQUEST Requesting)
            (agent ?REQUEST ?AGENT)
            (patient ?REQUEST ?FORMULA)
            (instance ?FORMULA Formula))
      (desires ?AGENT ?FORMULA))

Se question é un' istanza di Domandare e question é un agente di agent e formula é un paziente di question e formula é un' istanza di Formula, allora "agent non conosce formula" vales durante "il tempo di esistenza di question".
(=>
      (and
            (instance ?QUESTION Questioning)
            (agent ?QUESTION ?AGENT)
            (patient ?QUESTION ?FORMULA)
            (instance ?FORMULA Formula))
      (holdsDuring
            (WhenFn ?QUESTION)
            (not
                  (knows ?AGENT ?FORMULA))))

Se commit é un' istanza di Impegnarsi e formula é un paziente di commit e formula é un' istanza di Formula, allora l'affermazione formula ha il modello di forza di promise.
(=>
      (and
            (instance ?COMMIT Committing)
            (patient ?COMMIT ?FORMULA)
            (instance ?FORMULA Formula))
      (modalAttribute ?FORMULA Promise))

Se express é un' istanza di Esprimere e express é un agente di agent, allora esiste StatoMentale state tale che state is an attribute of agent e express esprime state.
(=>
      (and
            (instance ?EXPRESS Expressing)
            (agent ?EXPRESS ?AGENT))
      (exists
            (?STATE)
            (and
                  (instance ?STATE StateOfMind)
                  (attribute ?AGENT ?STATE)
                  (represents ?EXPRESS ?STATE))))

Se declare é un' istanza di Dichiarare e declare é un agente di agent1, allora esiste proc,agent2 tale che declare permette a agent2 di compiere il compito di tipo proc o declare obbliga agent2 a compiere il compito di tipo proc.
(=>
      (and
            (instance ?DECLARE Declaring)
            (agent ?DECLARE ?AGENT1))
      (exists
            (?PROC ?AGENT2)
            (or
                  (confersRight ?PROC ?DECLARE ?AGENT2)
                  (confersObligation ?PROC ?DECLARE ?AGENT2))))

Se meet é un' istanza di Incontro e meet é un agente di agent1 e meet é un agente di agent2, allora "agent1 é near a agent2" vales durante "il tempo di esistenza di meet".
(=>
      (and
            (instance ?MEET Meeting)
            (agent ?MEET ?AGENT1)
            (agent ?MEET ?AGENT2))
      (holdsDuring
            (WhenFn ?MEET)
            (orientation ?AGENT1 ?AGENT2 Near)))

Se meet é un' istanza di Incontro, allora esiste agent1,agent2 tale che meet é un agente di agent1 e meet é un agente di agent2 e meet ha scopo "esiste Comunicazione comm tale che comm é un agente di agent1 e comm é un agente di 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)))))))

Se contest é un' istanza di Competizione, allora esiste agent1,agent2,purp1,purp2 tale che contest é un agente di agent1 e contest é un agente di agent2 e contest ha &n scopo purp1 per agent1 e contest ha &n scopo purp2 per agent2 e agent1 is not uguale a agent2 e purp1 is not uguale a 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)))))

Se war é un' istanza di Guerra, allora esiste Battaglia battle tale che battle é un sottoprocesso di war.
(=>
      (instance ?WAR War)
      (exists
            (?BATTLE)
            (and
                  (instance ?BATTLE Battle)
                  (subProcess ?BATTLE ?WAR))))

(=>
      (and
            (instance ?WAR War)
            (agent ?WAR ?AGENT))
      (or
            (instance ?AGENT Nation)
            (and
                  (instance ?AGENT Organization)
                  (forall
                        (?MEMBER)
                        (=>
                              (member ?MEMBER ?AGENT)
                              (instance ?MEMBER Nation))))))

Se battle é un' istanza di Battaglia, allora esiste Guerra war tale che battle é un sottoprocesso di war.
(=>
      (instance ?BATTLE Battle)
      (exists
            (?WAR)
            (and
                  (instance ?WAR War)
                  (subProcess ?BATTLE ?WAR))))

Se battle é un' istanza di Battaglia, allora esiste CompetizioneViolenta attack tale che attack é un sottoprocesso di battle.
(=>
      (instance ?BATTLE Battle)
      (exists
            (?ATTACK)
            (and
                  (instance ?ATTACK ViolentContest)
                  (subProcess ?ATTACK ?BATTLE))))

Se move é un' istanza di Stratagemma, allora esiste Competizione contest tale che move é un sottoprocesso di contest.
(=>
      (instance ?MOVE Maneuver)
      (exists
            (?CONTEST)
            (and
                  (instance ?CONTEST Contest)
                  (subProcess ?MOVE ?CONTEST))))

Se percept é un' istanza di Percezione e percept é un agente di agent, allora agent é un' istanza di Animale.
(=>
      (and
            (instance ?PERCEPT Perception)
            (agent ?PERCEPT ?AGENT))
      (instance ?AGENT Animal))

Se percept é un' istanza di Percezione e percept é un agente di agent e object é un paziente di percept, allora agent notas object.
(=>
      (and
            (instance ?PERCEPT Perception)
            (agent ?PERCEPT ?AGENT)
            (patient ?PERCEPT ?OBJECT))
      (notices ?AGENT ?OBJECT))

Se see é un' istanza di Vista e see é un agente di agent e obj é un paziente di see, allora
(=>
      (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))))))

Se smell é un' istanza di Olfatto e obj é un paziente di smell, allora esiste AttributoOlfattivo attr tale che attr is an attribute of obj.
(=>
      (and
            (instance ?SMELL Smelling)
            (patient ?SMELL ?OBJ))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR OlfactoryAttribute)
                  (attribute ?OBJ ?ATTR))))

Se taste é un' istanza di Gusto e obj é un paziente di taste, allora esiste AttributoDiGusto attr tale che attr is an attribute of obj.
(=>
      (and
            (instance ?TASTE Tasting)
            (patient ?TASTE ?OBJ))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR TasteAttribute)
                  (attribute ?OBJ ?ATTR))))

Se hear é un' istanza di Udito e obj é un paziente di hear, allora esiste AttributoSonoro attr tale che attr is an attribute of obj.
(=>
      (and
            (instance ?HEAR Hearing)
            (patient ?HEAR ?OBJ))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR SoundAttribute)
                  (attribute ?OBJ ?ATTR))))

Se tactile é un' istanza di Tatto, allora esiste Toccare touch tale che touch é un sottoprocesso di tactile.
(=>
      (instance ?TACTILE TactilePerception)
      (exists
            (?TOUCH)
            (and
                  (instance ?TOUCH Touching)
                  (subProcess ?TOUCH ?TACTILE))))

Esiste RadiazioneLuminosa emit tale che region é un paziente di emit e region é un' istanza di Regione se e solo se illuminated is an attribute of region.
(<=>
      (exists
            (?EMIT)
            (and
                  (instance ?EMIT RadiatingLight)
                  (patient ?EMIT ?REGION)
                  (instance ?REGION Region)))
      (attribute ?REGION Illuminated))

Se emit é un' istanza di OndaSonora e emit é un agente di sound, allora esiste AttributoSonoro attr tale che attr is an attribute of sound.
(=>
      (and
            (instance ?EMIT RadiatingSound)
            (agent ?EMIT ?SOUND))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR SoundAttribute)
                  (attribute ?SOUND ?ATTR))))

Se process é un' istanza di CambiamentoDiStato e obj é un paziente di process, allora esiste part,StatoFisico state1,StatoFisico state2 tale che part é una parte di obj e state1 is not uguale a state2 e "state1 is an attribute of part" vales durante "immediatamente prima di "il tempo di esistenza di process"" e "state2 is an attribute of part" vales durante "immediatamente dopo "il tempo di esistenza di 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)))))

Se melt é un' istanza di Sciogliere, allora esiste Riscaldamento heat tale che heat é un sottoprocesso di melt.
(=>
      (instance ?MELT Melting)
      (exists
            (?HEAT)
            (and
                  (instance ?HEAT Heating)
                  (subProcess ?HEAT ?MELT))))

Se melt é un' istanza di Sciogliere e obj é un paziente di melt, allora esiste part tale che part é una parte di obj e "solid is an attribute of part" vales durante "immediatamente prima di "il tempo di esistenza di melt"" e "liquid is an attribute of part" vales durante "immediatamente dopo "il tempo di esistenza di 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)))))

Se boil é un' istanza di Bollire, allora esiste Riscaldamento heat tale che heat é un sottoprocesso di boil.
(=>
      (instance ?BOIL Boiling)
      (exists
            (?HEAT)
            (and
                  (instance ?HEAT Heating)
                  (subProcess ?HEAT ?BOIL))))

Se boil é un' istanza di Bollire e obj é un paziente di boil, allora esiste part tale che part é una parte di obj e "liquid is an attribute of part" vales durante "immediatamente prima di "il tempo di esistenza di boil"" e "gas is an attribute of part" vales durante "immediatamente dopo "il tempo di esistenza di 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)))))

Se cond é un' istanza di Condensare, allora esiste Raffreddamento cool tale che cool é un sottoprocesso di cond.
(=>
      (instance ?COND Condensing)
      (exists
            (?COOL)
            (and
                  (instance ?COOL Cooling)
                  (subProcess ?COOL ?COND))))

Se cond é un' istanza di Condensare e obj é un paziente di cond, allora esiste part tale che part é una parte di obj e "gas is an attribute of part" vales durante "immediatamente prima di "il tempo di esistenza di cond"" e "liquid is an attribute of part" vales durante "immediatamente dopo "il tempo di esistenza di 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)))))

Se freeze é un' istanza di Congelare, allora esiste Raffreddamento cool tale che cool é un sottoprocesso di freeze.
(=>
      (instance ?FREEZE Freezing)
      (exists
            (?COOL)
            (and
                  (instance ?COOL Cooling)
                  (subProcess ?COOL ?FREEZE))))

Se freeze é un' istanza di Congelare e obj é un paziente di freeze, allora esiste part tale che part é una parte di obj e "liquid is an attribute of part" vales durante "immediatamente prima di "il tempo di esistenza di freeze"" e "solid is an attribute of part" vales durante "immediatamente dopo "il tempo di esistenza di 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)))))

Se area é un' istanza di SuperficieAcquatica, allora esiste bed,hole,Acqua water tale che " ció che entra nell'apertura hole" is uguale a bed e water riempie propriamentes hole e "l' unione delle parti di bed e water" is uguale a area.
(=>
      (instance ?AREA WaterArea)
      (exists
            (?BED ?HOLE ?WATER)
            (and
                  (equal
                        (PrincipalHostFn ?HOLE)
                        ?BED)
                  (instance ?WATER Water)
                  (properlyFills ?WATER ?HOLE)
                  (equal
                        (MereologicalSumFn ?BED ?WATER)
                        ?AREA))))

Se land1 é un' istanza di SuperficieTerrestre, allora esiste land2 tale che land1 é una parte di land2 e land2 é un' istanza di Continente o land2 é un' istanza di Isola.
(=>
      (instance ?LAND1 LandArea)
      (exists
            (?LAND2)
            (and
                  (part ?LAND1 ?LAND2)
                  (or
                        (instance ?LAND2 Continent)
                        (instance ?LAND2 Island)))))

Se island é un' istanza di Isola, allora non esiste SuperficieTerrestre area,part1,part2 tale che part1 é una parte di island e part2 é una parte di area e island é not una parte di area e area é not una parte di island e part1 é connesso a 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)))))

Se state é un' istanza di StatoOProvincia, allora esiste Nazione land tale che state é una Parte propria di land.
(=>
      (instance ?STATE StateOrProvince)
      (exists
            (?LAND)
            (and
                  (instance ?LAND Nation)
                  (properPart ?STATE ?LAND))))

Se "la forma evolutiva di obj é attr1" vales durante time1 e attr2 é un attributo successore di attr1, allora esiste time2 tale che time2 accades prima di time1 e "la forma evolutiva di obj é attr2" vales durante time2.
(=>
      (and
            (holdsDuring
                  ?TIME1
                  (developmentalForm ?OBJ ?ATTR1))
            (successorAttributeClosure ?ATTR2 ?ATTR1))
      (exists
            (?TIME2)
            (and
                  (earlier ?TIME2 ?TIME1)
                  (holdsDuring
                        ?TIME2
                        (developmentalForm ?OBJ ?ATTR2)))))

Se organism é un' istanza di Organismo, allora esiste Nascita birth tale che organism esperisces birth.
(=>
      (instance ?ORGANISM Organism)
      (exists
            (?BIRTH)
            (and
                  (instance ?BIRTH Birth)
                  (experiencer ?BIRTH ?ORGANISM))))

Se parent é un parente di child e class é una sottoclasse di Organismo e parent é un' istanza di class, allora child é un' istanza di class.
(=>
      (and
            (parent ?CHILD ?PARENT)
            (subclass ?CLASS Organism)
            (instance ?PARENT ?CLASS))
      (instance ?CHILD ?CLASS))

animal1 é un fratello germano di animal2 se e solo se esiste father,mother tale che father é un padre di animal1 e father é un padre di animal2 e mother é una madre di animal1 e mother é una madre di animal2.
(<=>
      (sibling ?ANIMAL1 ?ANIMAL2)
      (exists
            (?FATHER ?MOTHER)
            (and
                  (father ?ANIMAL1 ?FATHER)
                  (father ?ANIMAL2 ?FATHER)
                  (mother ?ANIMAL1 ?MOTHER)
                  (mother ?ANIMAL2 ?MOTHER))))

Se alga é un' istanza di Alga, allora esiste Acqua water tale che alga abitas in water.
(=>
      (instance ?ALGA Alga)
      (exists
            (?WATER)
            (and
                  (inhabits ?ALGA ?WATER)
                  (instance ?WATER Water))))

Se fungus é un' istanza di Fungo e fungus abitas in obj, allora obj é un' istanza di Organismo.
(=>
      (and
            (instance ?FUNGUS Fungus)
            (inhabits ?FUNGUS ?OBJ))
      (instance ?OBJ Organism))

(=>
      (instance ?BACTERIUM Bacterium)
      (exists
            (?CELL1)
            (and
                  (component ?CELL1 ?BACTERIUM)
                  (instance ?CELL1 Cell)
                  (forall
                        (?CELL2)
                        (=>
                              (and
                                    (component ?CELL2 ?BACTERIUM)
                                    (instance ?CELL2 Cell))
                              (equal ?CELL1 ?CELL2))))))

Se bacterium é un' istanza di Bacterio e bacterium abitas in obj, allora obj é un' istanza di Organismo.
(=>
      (and
            (instance ?BACTERIUM Bacterium)
            (inhabits ?BACTERIUM ?OBJ))
      (instance ?OBJ Organism))

(=>
      (instance ?VIRUS Virus)
      (exists
            (?MOL1)
            (and
                  (component ?MOL1 ?VIRUS)
                  (instance ?MOL1 Molecule)
                  (forall
                        (?MOL2)
                        (=>
                              (and
                                    (component ?MOL2 ?VIRUS)
                                    (instance ?MOL2 Molecule))
                              (equal ?MOL1 ?MOL2))))))

Se virus é un' istanza di Virus e virus abitas in obj, allora obj é un' istanza di Organismo.
(=>
      (and
            (instance ?VIRUS Virus)
            (inhabits ?VIRUS ?OBJ))
      (instance ?OBJ Organism))

Se virus é un' istanza di Virus e proc é un' istanza di Replicazione e proc é un agente di virus, allora esiste Cellula cell tale che proc é localizzato in cell.
(=>
      (and
            (instance ?VIRUS Virus)
            (instance ?PROC Replication)
            (agent ?PROC ?VIRUS))
      (exists
            (?CELL)
            (and
                  (located ?PROC ?CELL)
                  (instance ?CELL Cell))))

Se fish é un' istanza di Pesce, allora esiste Acqua water tale che fish abitas in water.
(=>
      (instance ?FISH Fish)
      (exists
            (?WATER)
            (and
                  (inhabits ?FISH ?WATER)
                  (instance ?WATER Water))))

Se organism é un' istanza di SostanzaTossica, allora esiste SostanzaBiologicamenteAttiva substance tale che substance é una parte di organism.
(=>
      (instance ?ORGANISM ToxicOrganism)
      (exists
            (?SUBSTANCE)
            (and
                  (instance ?SUBSTANCE BiologicallyActiveSubstance)
                  (part ?SUBSTANCE ?ORGANISM))))

Se food é un' istanza di Cibo, allora esiste Nutriente nutrient tale che nutrient é una parte di food.
(=>
      (instance ?FOOD Food)
      (exists
            (?NUTRIENT)
            (and
                  (instance ?NUTRIENT Nutrient)
                  (part ?NUTRIENT ?FOOD))))

(=>
      (instance ?FOOD Food)
      (forall
            (?PART1)
            (=>
                  (part ?PART1 ?FOOD)
                  (exists
                        (?PART2 ?ANIMAL)
                        (and
                              (part ?PART1 ?PART2)
                              (part ?PART2 ?ANIMAL)
                              (instance ?ANIMAL Animal))))))

(=>
      (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))))))))

(=>
      (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))))))))

Se drink é un' istanza di Bere e bev é un paziente di drink, allora bev é un' istanza di Bevanda.
(=>
      (and
            (instance ?DRINK Drinking)
            (patient ?DRINK ?BEV))
      (instance ?BEV Beverage))

Se anat é un' istanza di StrutturaAnatomica, allora esiste Organismo organism tale che anat é una parte di organism.
(=>
      (instance ?ANAT AnatomicalStructure)
      (exists
            (?ORGANISM)
            (and
                  (instance ?ORGANISM Organism)
                  (part ?ANAT ?ORGANISM))))

Se part é un' istanza di StrutturaAnatomica, allora esiste Cellula cell tale che cell é una parte di part.
(=>
      (instance ?PART AnatomicalStructure)
      (exists
            (?CELL)
            (and
                  (instance ?CELL Cell)
                  (part ?CELL ?PART))))

Se part é un' istanza di ParteDelCorpo, allora non esiste ProcessoPatologico proc tale che part é un risultato di proc.
(=>
      (instance ?PART BodyPart)
      (not
            (exists
                  (?PROC)
                  (and
                        (instance ?PROC PathologicProcess)
                        (result ?PROC ?PART)))))

Se cover é un' istanza di RivestimentoDiOrganismi, allora esiste body tale che cover é una parte superficiale di body e body é un' istanza di Organismo o body é un' istanza di ParteDelCorpo.
(=>
      (instance ?COVER BodyCovering)
      (exists
            (?BODY)
            (and
                  (superficialPart ?COVER ?BODY)
                  (or
                        (instance ?BODY Organism)
                        (instance ?BODY BodyPart)))))

Se junct é un' istanza di Giuntura, allora esiste ParteDelCorpo struct tale che junct é un componente distruct.
(=>
      (instance ?JUNCT BodyJunction)
      (exists
            (?STRUCT)
            (and
                  (instance ?STRUCT BodyPart)
                  (component ?JUNCT ?STRUCT))))

Se junct é un' istanza di Giuntura, allora esiste ParteDelCorpo struct1,ParteDelCorpo struct2 tale che junct é connesso a struct1 e junct é connesso a struct2 e struct1 is not uguale a struct2.
(=>
      (instance ?JUNCT BodyJunction)
      (exists
            (?STRUCT1 ?STRUCT2)
            (and
                  (connected ?JUNCT ?STRUCT1)
                  (connected ?JUNCT ?STRUCT2)
                  (instance ?STRUCT1 BodyPart)
                  (instance ?STRUCT2 BodyPart)
                  (not
                        (equal ?STRUCT1 ?STRUCT2)))))

Se stuff é un' istanza di Tessuto, allora esiste Cellula part tale che part é una parte di stuff.
(=>
      (instance ?STUFF Tissue)
      (exists
            (?PART)
            (and
                  (instance ?PART Cell)
                  (part ?PART ?STUFF))))

Se stuff é un' istanza di Tessuto, allora esiste Organismo organism tale che stuff é una parte di organism.
(=>
      (instance ?STUFF Tissue)
      (exists
            (?ORGANISM)
            (and
                  (instance ?ORGANISM Organism)
                  (part ?STUFF ?ORGANISM))))

Se bone é un' istanza di Osso, allora esiste Vertebrato vert tale che bone é una parte di vert.
(=>
      (instance ?BONE Bone)
      (exists
            (?VERT)
            (and
                  (instance ?VERT Vertebrate)
                  (part ?BONE ?VERT))))

Se morph é un' istanza di Morfema, allora non esiste Morfema othermorph tale che othermorph é una parte di morph e othermorph is not uguale a morph.
(=>
      (instance ?MORPH Morpheme)
      (not
            (exists
                  (?OTHERMORPH)
                  (and
                        (instance ?OTHERMORPH Morpheme)
                        (part ?OTHERMORPH ?MORPH)
                        (not
                              (equal ?OTHERMORPH ?MORPH))))))

Se morph é un' istanza di Morfema, allora esiste Parola word tale che morph é una parte di word.
(=>
      (instance ?MORPH Morpheme)
      (exists
            (?WORD)
            (and
                  (instance ?WORD Word)
                  (part ?MORPH ?WORD))))

Se word é un' istanza di Parola, allora esiste Morfema part tale che part é una parte di word.
(=>
      (instance ?WORD Word)
      (exists
            (?PART)
            (and
                  (part ?PART ?WORD)
                  (instance ?PART Morpheme))))

Se phrase é un' istanza di Sintagma, allora esiste Parola part1,Parola part2 tale che part1 é una parte di phrase e part2 é una parte di phrase e part1 is not uguale a part2.
(=>
      (instance ?PHRASE Phrase)
      (exists
            (?PART1 ?PART2)
            (and
                  (part ?PART1 ?PHRASE)
                  (part ?PART2 ?PHRASE)
                  (instance ?PART1 Word)
                  (instance ?PART2 Word)
                  (not
                        (equal ?PART1 ?PART2)))))

Se sentence é un' istanza di Frase, allora esiste SintagmaNominale phrase1,SintagmaVerbale phrase2 tale che phrase1 é una parte di sentence e phrase2 é una parte di sentence.
(=>
      (instance ?SENTENCE Sentence)
      (exists
            (?PHRASE1 ?PHRASE2)
            (and
                  (instance ?PHRASE1 NounPhrase)
                  (instance ?PHRASE2 VerbPhrase)
                  (part ?PHRASE1 ?SENTENCE)
                  (part ?PHRASE2 ?SENTENCE))))

Se text é un' istanza di Testo, allora esiste Proposizione prop tale che text contienes informazione prop.
(=>
      (instance ?TEXT Text)
      (exists
            (?PROP)
            (and
                  (instance ?PROP Proposition)
                  (containsInformation ?TEXT ?PROP))))

Se text é un' istanza di Testo, allora esiste Frase part tale che part é una parte di text.
(=>
      (instance ?TEXT Text)
      (exists
            (?PART)
            (and
                  (part ?PART ?TEXT)
                  (instance ?PART Sentence))))

Se text é un' istanza di Testo, allora esiste Scrivere write tale che text é un risultato di write.
(=>
      (instance ?TEXT Text)
      (exists
            (?WRITE)
            (and
                  (instance ?WRITE Writing)
                  (result ?WRITE ?TEXT))))

Se sent é un' istanza di Frase, allora esiste SintagmaNominale noun,SintagmaVerbale verb tale che noun é una parte di sent e verb é una parte di sent.
(=>
      (instance ?SENT Sentence)
      (exists
            (?NOUN ?VERB)
            (and
                  (instance ?NOUN NounPhrase)
                  (instance ?VERB VerbPhrase)
                  (part ?NOUN ?SENT)
                  (part ?VERB ?SENT))))

Se agent é l' autore di text, allora esiste process,text instance tale che process é un agente di agent e text é un risultato di process.
(=>
      (authors ?AGENT ?TEXT)
      (exists
            (?PROCESS ?INSTANCE)
            (and
                  (agent ?PROCESS ?AGENT)
                  (instance ?INSTANCE ?TEXT)
                  (result ?PROCESS ?TEXT))))

org pubblica text se e solo se esiste Editoria pub tale che pub é un agente di org e text é un paziente di pub.
(<=>
      (publishes ?ORG ?TEXT)
      (exists
            (?PUB)
            (and
                  (instance ?PUB Publication)
                  (agent ?PUB ?ORG)
                  (patient ?PUB ?TEXT))))

Se "edizione int1 di text" is uguale a edition1 e "edizione int2 di text" is uguale a edition2 e int2 é più grande di int1 e pub1 é un' istanza di Editoria e pub2 é un' istanza di Editoria e edition1 é un paziente di pub1 e edition2 é un paziente di pub2 e data di pub1 é date1 e data di pub2 é date2, allora "la fine di date1" succede?{s} prima di "la fine di 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)))

Se text é una sottoclasse di Periodico e "volume int1 nella serie text" is uguale a volume1 e "volume int2 nella serie text" is uguale a volume2 e int2 é più grande di int1 e pub1 é un' istanza di Editoria e pub2 é un' istanza di Editoria e volume1 é un paziente di pub1 e volume2 é un paziente di pub2 e data di pub1 é date1 e data di pub2 é date2, allora "la fine di date1" succede?{s} prima di "la fine di 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)))

Se text é un' istanza di Riassunto, allora esiste Testo text2 tale che text2 sussume il contenuto di text.
(=>
      (instance ?TEXT Summary)
      (exists
            (?TEXT2)
            (and
                  (instance ?TEXT2 Text)
                  (subsumesContentInstance ?TEXT2 ?TEXT))))

Se series é un' istanza di Serie, allora esiste Libro book1,Libro book2 tale che series sussume il contenuto di book1 e series sussume il contenuto di book2 e book1 is not uguale a book2.
(=>
      (instance ?SERIES Series)
      (exists
            (?BOOK1 ?BOOK2)
            (and
                  (instance ?BOOK1 Book)
                  (instance ?BOOK2 Book)
                  (subsumesContentInstance ?SERIES ?BOOK1)
                  (subsumesContentInstance ?SERIES ?BOOK2)
                  (not
                        (equal ?BOOK1 ?BOOK2)))))

Se article é un' istanza di Articolo, allora esiste Libro book tale che book sussume il contenuto di article.
(=>
      (instance ?ARTICLE Article)
      (exists
            (?BOOK)
            (and
                  (instance ?BOOK Book)
                  (subsumesContentInstance ?BOOK ?ARTICLE))))

Se doc é un' istanza di Certificato e agent possiedees doc, allora esiste proc tale che doc permette a agent di compiere il compito di tipo proc o doc obbliga agent a compiere il compito di tipo proc.
(=>
      (and
            (instance ?DOC Certificate)
            (possesses ?AGENT ?DOC))
      (exists
            (?PROC)
            (or
                  (confersRight ?PROC ?DOC ?AGENT)
                  (confersObligation ?PROC ?DOC ?AGENT))))

Se mole é un' istanza di Molecola, allora esiste Atomo atom1,Atomo atom2 tale che atom1 é una parte di mole e atom2 é una parte di mole e atom1 is not uguale a atom2.
(=>
      (instance ?MOLE Molecule)
      (exists
            (?ATOM1 ?ATOM2)
            (and
                  (instance ?ATOM1 Atom)
                  (instance ?ATOM2 Atom)
                  (part ?ATOM1 ?MOLE)
                  (part ?ATOM2 ?MOLE)
                  (not
                        (equal ?ATOM1 ?ATOM2)))))

artifact é un' istanza di Manufatto se e solo se esiste Fabbricazione making tale che artifact é un risultato di making.
(<=>
      (instance ?ARTIFACT Artifact)
      (exists
            (?MAKING)
            (and
                  (instance ?MAKING Making)
                  (result ?MAKING ?ARTIFACT))))

Se product é un' istanza di Prodotto, allora esiste Lavorazione manufacture tale che product é un risultato di manufacture.
(=>
      (instance ?PRODUCT Product)
      (exists
            (?MANUFACTURE)
            (and
                  (instance ?MANUFACTURE Manufacture)
                  (result ?MANUFACTURE ?PRODUCT))))

(=>
      (instance ?ARTIFACT StationaryArtifact)
      (exists
            (?PLACE)
            (forall
                  (?TIME)
                  (=>
                        (and
                              (beforeOrEqual
                                    ?TIME
                                    (EndFn
                                          (WhenFn ?ARTIFACT)))
                              (beforeOrEqual
                                    (BeginFn
                                          (WhenFn ?ARTIFACT))
                                    ?TIME))
                        (equal
                              (WhereFn ?ARTIFACT ?TIME)
                              ?PLACE)))))

Se building é un' istanza di Costruzione, allora esiste Umano human tale che
(=>
      (instance ?BUILDING Building)
      (exists
            (?HUMAN)
            (and
                  (instance ?HUMAN Human)
                  (or
                        (inhabits ?HUMAN ?BUILDING)
                        (exists
                              (?ACT)
                              (and
                                    (agent ?ACT ?HUMAN)
                                    (located ?ACT ?BUILDING)))))))

Se room é un' istanza di Stanza, allora esiste Costruzione build tale che room é una Parte propria di build.
(=>
      (instance ?ROOM Room)
      (exists
            (?BUILD)
            (and
                  (instance ?BUILD Building)
                  (properPart ?ROOM ?BUILD))))

Se clothing é un' istanza di Vestito, allora esiste Stoffa fabric tale che fabric é una parte di clothing.
(=>
      (instance ?CLOTHING Clothing)
      (exists
            (?FABRIC)
            (and
                  (instance ?FABRIC Fabric)
                  (part ?FABRIC ?CLOTHING))))

Se device é un' istanza di Dispositivo, allora esiste Processo proc tale che device é capace di fare proc nel ruolo instrument.
(=>
      (instance ?DEVICE Device)
      (exists
            (?PROC)
            (and
                  (subclass ?PROC Process)
                  (capability ?PROC instrument ?DEVICE))))

Se device é un' istanza di Dispositivo, allora esiste Processo proc tale che device ha scopo "device é capace di fare proc nel ruolo instrument".
(=>
      (instance ?DEVICE Device)
      (exists
            (?PROC)
            (and
                  (subclass ?PROC Process)
                  (hasPurpose
                        ?DEVICE
                        (capability ?PROC instrument ?DEVICE)))))

Se weapon é un' istanza di Arma, allora weapon ha scopo "esiste Danneggiare dest,patient tale che patient é un paziente di dest e ".
(=>
      (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))))))))

(=>
      (instance ?MACHINE Machine)
      (forall
            (?PROC)
            (=>
                  (instrument ?PROC ?MACHINE)
                  (exists
                        (?RESOURCE ?RESULT)
                        (and
                              (resource ?PROC ?RESOURCE)
                              (result ?PROC ?RESULT))))))

Se comp é un' istanza di Meccanismo, allora esiste Dispositivo device tale che comp é un componente didevice.
(=>
      (instance ?COMP EngineeringComponent)
      (exists
            (?DEVICE)
            (and
                  (instance ?DEVICE Device)
                  (component ?COMP ?DEVICE))))

Se comp1 é connesso a comp2, allora comp1 é un componente di comp2 e comp2 é un componente di comp1.
(=>
      (connectedEngineeringComponents ?COMP1 ?COMP2)
      (and
            (not
                  (engineeringSubcomponent ?COMP1 ?COMP2))
            (not
                  (engineeringSubcomponent ?COMP2 ?COMP1))))

Se group é un' istanza di Gruppo e memb é un membro di group, allora memb é un' istanza di Agente.
(=>
      (and
            (instance ?GROUP Group)
            (member ?MEMB ?GROUP))
      (instance ?MEMB Agent))

(=>
      (instance ?GROUP AgeGroup)
      (forall
            (?MEMB1 ?MEMB2 ?AGE1 ?AGE2)
            (=>
                  (and
                        (member ?MEMB1 ?GROUP)
                        (member ?MEMB2 ?GROUP)
                        (age ?MEMB1 ?AGE1)
                        (age ?MEMB2 ?AGE2))
                  (equal ?AGE1 ?AGE2))))

(=>
      (instance ?GROUP FamilyGroup)
      (forall
            (?MEMB1 ?MEMB2)
            (=>
                  (and
                        (member ?MEMB1 ?GROUP)
                        (member ?MEMB2 ?GROUP))
                  (familyRelation ?MEMB1 ?MEMB2))))

Se organism1 e organism2 sono parenti, allora esiste organism3 tale che organism3 e organism1 sono parenti e organism3 e organism2 sono parenti.
(=>
      (familyRelation ?ORGANISM1 ?ORGANISM2)
      (exists
            (?ORGANISM3)
            (and
                  (familyRelation ?ORGANISM3 ?ORGANISM1)
                  (familyRelation ?ORGANISM3 ?ORGANISM2))))

Se "la legittima entitá organizzativa di unit" is uguale a org e attr é un' istanza di AttributoNormativo, allora attr is an attribute of unit se e solo se attr is an attribute of org.
(=>
      (and
            (equal
                  (OrganizationFn ?UNIT)
                  ?ORG)
            (instance ?ATTR NormativeAttribute))
      (<=>
            (attribute ?UNIT ?ATTR)
            (attribute ?ORG ?ATTR)))

Se pol é un' istanza di OrganizzazionePolitica, allora esiste ProcessoPolitico proc tale che proc é un agente di pol.
(=>
      (instance ?POL PoliticalOrganization)
      (exists
            (?PROC)
            (and
                  (instance ?PROC PoliticalProcess)
                  (agent ?PROC ?POL))))

Se plan é un' istanza di Programma e obj é un' istanza di OggettoSemiotico e obj contienes informazione plan, allora esiste Pianificazione planning tale che obj é un risultato di planning.
(=>
      (and
            (instance ?PLAN Plan)
            (instance ?OBJ ContentBearingObject)
            (containsInformation ?OBJ ?PLAN))
      (exists
            (?PLANNING)
            (and
                  (instance ?PLANNING Planning)
                  (result ?PLANNING ?OBJ))))

Se obj1 é attr1 a obj2 e é opposto a ? e attr1 é un é membro di "(" e attr2 é un é membro di "(" e attr1 is not uguale a attr2, allora obj1 é not attr2 a 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)))

Se item ha un attributo value e value é un' istanza di ValoreDiVeritá, allora item é un' istanza di Frase o item é un' istanza di Proposizione.
(=>
      (and
            (property ?ITEM ?VALUE)
            (instance ?VALUE TruthValue))
      (or
            (instance ?ITEM Sentence)
            (instance ?ITEM Proposition)))

Se obj1 é attr1 a obj2 e attr1 é un' istanza di AttributoDirezionale e attr2 é un' istanza di AttributoDirezionale e attr1 is not uguale a attr2, allora obj1 é not attr2 a obj2.
(=>
      (and
            (orientation ?OBJ1 ?OBJ2 ?ATTR1)
            (instance ?ATTR1 DirectionalAttribute)
            (instance ?ATTR2 DirectionalAttribute)
            (not
                  (equal ?ATTR1 ?ATTR2)))
      (not
            (orientation ?OBJ1 ?OBJ2 ?ATTR2)))

Se direct é un' istanza di AttributoDirezionale e obj1 é direct a obj2 e obj2 é direct a obj3, allora obj2 is between obj1 and obj33.
(=>
      (and
            (instance ?DIRECT DirectionalAttribute)
            (orientation ?OBJ1 ?OBJ2 ?DIRECT)
            (orientation ?OBJ2 ?OBJ3 ?DIRECT))
      (between ?OBJ1 ?OBJ2 ?OBJ33))

Se attribute is an attribute of person e attribute é un' istanza di RuoloSociale, allora person é un' istanza di Umano.
(=>
      (and
            (attribute ?PERSON ?ATTRIBUTE)
            (instance ?ATTRIBUTE SocialRole))
      (instance ?PERSON Human))

Per ogni org vale: org non impiega person e person é un' istanza di Umano se e solo se unemployed is an attribute of person.
(<=>
      (forall
            (?ORG)
            (and
                  (not
                        (employs ?ORG ?PERSON))
                  (instance ?PERSON Human)))
      (attribute ?PERSON Unemployed))

Se l'affermazione formula1 ha il modello di forza di prop e formula1 implicas formula2, allora l'affermazione formula2 ha il modello di forza di prop.
(=>
      (and
            (modalAttribute ?FORMULA1 ?PROP)
            (entails ?FORMULA1 ?FORMULA2))
      (modalAttribute ?FORMULA2 ?PROP))

Se agent é obbligato a compiere il compito di tipo process, allora l'affermazione "esiste process instance tale che instance é un agente di agent" ha il modello di forza di obligation.
(=>
      (holdsObligation ?PROCESS ?AGENT)
      (modalAttribute
            (exists
                  (?INSTANCE)
                  (and
                        (instance ?INSTANCE ?PROCESS)
                        (agent ?INSTANCE ?AGENT)))
            Obligation))

Se agent ha il diritto di compiere process, allora l'affermazione "esiste process instance tale che instance é un agente di agent" ha il modello di forza di permission.
(=>
      (holdsRight ?PROCESS ?AGENT)
      (modalAttribute
            (exists
                  (?INSTANCE)
                  (and
                        (instance ?INSTANCE ?PROCESS)
                        (agent ?INSTANCE ?AGENT)))
            Permission))

Se attr is an attribute of obj e attr é un' istanza di AttributoDiCompetizione, allora esiste Competizione contest tale che contest é un agente di obj o obj é un paziente di contest.
(=>
      (and
            (attribute ?OBJ ?ATTR)
            (instance ?ATTR ContestAttribute))
      (exists
            (?CONTEST)
            (and
                  (instance ?CONTEST Contest)
                  (or
                        (agent ?CONTEST ?OBJ)
                        (patient ?CONTEST ?OBJ)))))

obj é un' istanza di Sostanza se e solo se esiste StatoFisico attr tale che attr is an attribute of obj.
(<=>
      (instance ?OBJ Substance)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR PhysicalState)
                  (attribute ?OBJ ?ATTR))))

Se perception é un' istanza di Percezione e obj é un paziente di perception, allora esiste AttributoPercettivo prop tale che prop is an attribute of obj.
(=>
      (and
            (instance ?PERCEPTION Perception)
            (patient ?PERCEPTION ?OBJ))
      (exists
            (?PROP)
            (and
                  (instance ?PROP PerceptualAttribute)
                  (attribute ?OBJ ?PROP))))

Se obj é un' istanza di Cibo, allora esiste AttributoDiGusto attr tale che attr is an attribute of obj.
(=>
      (instance ?OBJ Food)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR TasteAttribute)
                  (attribute ?OBJ ?ATTR))))

(=>
      (and
            (attribute ?OBJ Monochromatic)
            (superficialPart ?PART ?OBJ)
            (attribute ?PART ?COLOR)
            (instance ?COLOR PrimaryColor))
      (forall
            (?ELEMENT)
            (=>
                  (superficialPart ?ELEMENT ?OBJ)
                  (attribute ?ELEMENT ?COLOR))))

Se polychromatic is an attribute of obj, allora esiste part1,part2,AttributoDiColore color1,AttributoDiColore color2 tale che part1 é una parte superficiale di obj e part2 é una parte superficiale di obj e color1 is an attribute of part1 e color2 is an attribute of part2 e color1 is not uguale a 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)))))

Se esiste CambiamentoDiForma change tale che obj é un paziente di change, allora pliable is an attribute of obj.
(=>
      (exists
            (?CHANGE)
            (and
                  (instance ?CHANGE ShapeChange)
                  (patient ?CHANGE ?OBJ)))
      (attribute ?OBJ Pliable))

Se attribute é un' istanza di AttributoDiConsistenza e attribute is an attribute of obj e surface é una superficie di obj, allora attribute is an attribute of surface.
(=>
      (and
            (instance ?ATTRIBUTE TextureAttribute)
            (attribute ?OBJ ?ATTRIBUTE)
            (surface ?SURFACE ?OBJ))
      (attribute ?SURFACE ?ATTRIBUTE))

Se dry is an attribute of obj, allora non esiste subobj tale che subobj é una parte di obj e liquid is an attribute of subobj.
(=>
      (attribute ?OBJ Dry)
      (not
            (exists
                  (?SUBOBJ)
                  (and
                        (part ?SUBOBJ ?OBJ)
                        (attribute ?SUBOBJ Liquid)))))

(=>
      (attribute ?OBJ Wet)
      (forall
            (?PART)
            (=>
                  (part ?PART ?OBJ)
                  (exists
                        (?SUBPART)
                        (and
                              (part ?SUBPART ?PART)
                              (attribute ?SUBPART Liquid))))))

Se unbreakable is an attribute of obj, allora non esiste Danneggiare damage tale che obj é un paziente di damage.
(=>
      (attribute ?OBJ Unbreakable)
      (not
            (exists
                  (?DAMAGE)
                  (and
                        (instance ?DAMAGE Damaging)
                        (patient ?DAMAGE ?OBJ)))))

Se att is an attribute of org e att é un' istanza di AttributoBiologico, allora org é un' istanza di Organismo.
(=>
      (and
            (attribute ?ORG ?ATT)
            (instance ?ATT BiologicalAttribute))
      (instance ?ORG Organism))

Se organism é un' istanza di Organismo e process é un agente di organism, allora "living is an attribute of organism" vales durante "il tempo di esistenza di process".
(=>
      (and
            (instance ?ORGANISM Organism)
            (agent ?PROCESS ?ORGANISM))
      (holdsDuring
            (WhenFn ?PROCESS)
            (attribute ?ORGANISM Living)))

Se org é un' istanza di Organismo, allora esiste AttributoVitale attr tale che attr is an attribute of org.
(=>
      (instance ?ORG Organism)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR AnimacyAttribute)
                  (attribute ?ORG ?ATTR))))

Se body é un' istanza di CorpoRiproduttivo e body é una parte di org e org é un' istanza di Organismo, allora female is an attribute of org.
(=>
      (and
            (instance ?BODY ReproductiveBody)
            (part ?BODY ?ORG)
            (instance ?ORG Organism))
      (attribute ?ORG Female))

Se animal é un' istanza di Animale, allora esiste AttributoSessuale attr tale che attr is an attribute of animal.
(=>
      (instance ?ANIMAL Animal)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR SexAttribute)
                  (attribute ?ANIMAL ?ATTR))))

Se fully formed is an attribute of obj, allora esiste Crescita growth tale che obj esperisces growth e "non fully formed is an attribute of obj" vales durante "l' inizio di "il tempo di esistenza di obj"".
(=>
      (attribute ?OBJ FullyFormed)
      (exists
            (?GROWTH)
            (and
                  (instance ?GROWTH Growth)
                  (experiencer ?GROWTH ?OBJ)
                  (holdsDuring
                        (BeginFn
                              (WhenFn ?OBJ))
                        (attribute ?OBJ NonFullyFormed)))))

Se org é un' istanza di Organismo, allora esiste AttributoEvolutivo attr tale che attr is an attribute of org.
(=>
      (instance ?ORG Organism)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR DevelopmentalAttribute)
                  (attribute ?ORG ?ATTR))))

Se "larval is an attribute of org" vales durante time, allora "esiste Nascita birth tale che org esperisces birth" vales durante "prima time".
(=>
      (holdsDuring
            ?TIME
            (attribute ?ORG Larval))
      (holdsDuring
            (PastFn ?TIME)
            (exists
                  (?BIRTH)
                  (and
                        (instance ?BIRTH Birth)
                        (experiencer ?BIRTH ?ORG)))))

Se embryonic is an attribute of org, allora esiste CorpoRiproduttivo body tale che org é localizzato in body.
(=>
      (attribute ?ORG Embryonic)
      (exists
            (?BODY)
            (and
                  (instance ?BODY ReproductiveBody)
                  (located ?ORG ?BODY))))

Se "embryonic is an attribute of org" vales durante time, allora "non esiste Nascita birth tale che org esperisces birth" vales durante time.
(=>
      (holdsDuring
            ?TIME
            (attribute ?ORG Embryonic))
      (holdsDuring
            ?TIME
            (not
                  (exists
                        (?BIRTH)
                        (and
                              (instance ?BIRTH Birth)
                              (experiencer ?BIRTH ?ORG))))))

Se attr é un' istanza di AttributoPsicologico e attr is an attribute of agent, allora agent é un' istanza di AgenteSensibile.
(=>
      (and
            (instance ?ATTR PsychologicalAttribute)
            (attribute ?AGENT ?ATTR))
      (instance ?AGENT SentientAgent))

agent é un' istanza di AgenteSensibile e living is an attribute of agent se e solo se esiste AttributoDiCoscienza attr tale che attr is an attribute of agent.
(<=>
      (and
            (instance ?AGENT SentientAgent)
            (attribute ?AGENT Living))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR ConsciousnessAttribute)
                  (attribute ?AGENT ?ATTR))))

entity é un' istanza di "l' unione di class1 e class2" se e solo se entity é un' istanza di class1 e entity é un' istanza di class2.
(<=>
      (instance
            ?ENTITY
            (IntersectionFn ?CLASS1 ?CLASS2))
      (and
            (instance ?ENTITY ?CLASS1)
            (instance ?ENTITY ?CLASS2)))

Se class1 é un' istanza di InsiemeOClasse e class2 é un' istanza di InsiemeOClasse, allora "la differenza tra class1 e class2" is uguale a "l' unione di class1 e "il complemento di class2"".
(=>
      (and
            (instance ?CLASS1 SetOrClass)
            (instance ?CLASS2 SetOrClass))
      (equal
            (RelativeComplementFn ?CLASS1 ?CLASS2)
            (IntersectionFn
                  ?CLASS1
                  (ComplementFn ?CLASS2))))

entity é un' istanza di "l' unione di tutti gli elementi di superclass" se e solo se esiste superclass class tale che entity é un' istanza di class.
(<=>
      (instance
            ?ENTITY
            (GeneralizedUnionFn ?SUPERCLASS))
      (exists
            (?CLASS)
            (and
                  (instance ?CLASS ?SUPERCLASS)
                  (instance ?ENTITY ?CLASS))))