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

instance (instance)

An object is an instance of a SetOrClass if it is included in that SetOrClass. An individual may be an instance of many classes, some of which may be subclasses of others. Thus, there is no assumption in the meaning of instance about specificity or uniqueness.

Ontology

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

Classe
is instance of
  inheritable relation  
is instance of
  PredicatoBinario  
is instance of
  instance  

Subrelation(s)

immediate instance  element 

Coordinate term(s)

arc weight  authors  before or equal  causes  causes subclass  citizen  closed on  connected  contains information  cooccur  copy  date  decreases likelihood  developmental form  disjoint  distributes  documentation  duration  earlier  editor  element  employs  equal  equivalence relation on  exploits  expressed in language  faces  family relation  finishes  frequency  graph part  greater than  greater than or equal to  has purpose  has skill  holds during  holds obligation  holds right  hole  identity element  in list  in scope of interest  increases likelihood  independent probability  inhabits  inhibits  initial list  inverse  irreflexive on  larger  less than  less than or equal to  material  measure  meets temporally  modal attribute  overlaps temporally  parent  partial ordering on  partly located  path length  possesses  precondition  prevents  property  publishes  range  range subclass  refers  reflexive on  related internal concept  sibling  smaller  starts  sub attribute  sub collection  sub graph  sub list  sub process  sub proposition  subclass  subrelation  subsumes content class  subsumes content instance  successor attribute  successor attribute closure  temporal part  time  total ordering on  trichotomizing on  uses  valence  version 

Type restrictions

instance(Entitá, InsiemeOClasse)

Related WordNet synsets

member
anything that belongs to a set or class: "snakes are members of the class Reptilia"; "members of the opposite sex"
member is kind of (all)...   member is kind of...  
be
have the quality of being; (copula, used with an adjective or a predicate noun); "John is rich"; "This is not a good answer"
kinds of be...   kinds of be (all)...  
See more related synsets on a separate page.

Axioms (537)

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 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 thing1 is uguale a thing2, allora per ogni class vale: thing1 é un' istanza di class se e solo se thing2 é un' istanza di class.
(=>
      (equal ?THING1 ?THING2)
      (forall
            (?CLASS)
            (<=>
                  (instance ?THING1 ?CLASS)
                  (instance ?THING2 ?CLASS))))

Se class1 is uguale a class2, allora per ogni thing vale: thing é un' istanza di class1 se e solo se thing é un' istanza di class2.
(=>
      (equal ?CLASS1 ?CLASS2)
      (forall
            (?THING)
            (<=>
                  (instance ?THING ?CLASS1)
                  (instance ?THING ?CLASS2))))

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

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

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

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

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

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

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

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

Esiste thing tale che thing é un' istanza di Entitá.
(exists
      (?THING)
      (instance ?THING Entity))

Se class é un' istanza di Classe, allora class é una sottoclasse di Entitá.
(=>
      (instance ?CLASS Class)
      (subclass ?CLASS Entity))

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

Se obj é un' istanza di OggettoIntegro, allora "il davanti di obj" é una parte di obj.
(=>
      (instance ?OBJ SelfConnectedObject)
      (part
            (FrontFn ?OBJ)
            ?OBJ))

Se obj é un' istanza di OggettoIntegro, allora "il dietro di obj" é una parte di obj.
(=>
      (instance ?OBJ SelfConnectedObject)
      (part
            (BackFn ?OBJ)
            ?OBJ))

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

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

Se region é un' istanza di Regione, allora esiste phys tale che phys é localizzato in region.
(=>
      (instance ?REGION Region)
      (exists
            (?PHYS)
            (located ?PHYS ?REGION)))

Se coll é un' istanza di InsiemeConcreto, allora esiste obj tale che obj é un membro di coll.
(=>
      (instance ?COLL Collection)
      (exists
            (?OBJ)
            (member ?OBJ ?COLL)))

member é interamente correlato a instance.
(relatedInternalConcept member instance)

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

agent é un' istanza di Agente se e solo se esiste proc tale che proc é un agente di agent.
(<=>
      (instance ?AGENT Agent)
      (exists
            (?PROC)
            (agent ?PROC ?AGENT)))

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

abs é un' istanza di Astratto se e solo se non esiste point tale che abs é localizzato in point o abs esistes durante point.
(<=>
      (instance ?ABS Abstract)
      (not
            (exists
                  (?POINT)
                  (or
                        (located ?ABS ?POINT)
                        (time ?ABS ?POINT)))))

"la descrizione di class" is uguale a attr se e solo se per ogni inst vale: inst é un' istanza di class se e solo se inst ha un attributo attr.
(<=>
      (equal
            (AbstractionFn ?CLASS)
            ?ATTR)
      (forall
            (?INST)
            (<=>
                  (instance ?INST ?CLASS)
                  (property ?INST ?ATTR))))

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

Se function é un' istanza di QuantitáDipendenteDalTempo, allora il numero argomenti di function é un istanza di MisuraTemporale.
(=>
      (instance ?FUNCTION TimeDependentQuantity)
      (domain ?FUNCTION 1 TimeMeasure))

Se rel é un' istanza di Relazione, allora rel( vales se e solo se rel() vale.
(=>
      (instance ?REL Relation)
      (<=>
            (holds ?REL @ROW)
            (?REL @ROW)))

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 rel é un' istanza di RelazioneBinaria, allora non esiste item1,item2,item3, tale che rel(item1,item2,item3, vales.
(=>
      (instance ?REL BinaryRelation)
      (not
            (exists
                  (?ITEM1 ?ITEM2 ?ITEM3 @ROW)
                  (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 @ROW))))

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

Se rel é un' istanza di RelazioneNonRiflessiva, allora per ogni inst vale: rel(inst,inst non vale.
(=>
      (instance ?REL IrreflexiveRelation)
      (forall
            (?INST)
            (not
                  (holds ?REL ?INST ?INST))))

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

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

Se rel é un' istanza di RelazioneTricotomizzante, allora per ogni inst1,inst2 vale: rel(inst1,inst2 vales o inst1 is uguale a inst2 o rel(inst2,inst1 vales.
(=>
      (instance ?REL TrichotomizingRelation)
      (forall
            (?INST1 ?INST2)
            (or
                  (holds ?REL ?INST1 ?INST2)
                  (equal ?INST1 ?INST2)
                  (holds ?REL ?INST2 ?INST1))))

(=>
      (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 rel é un' istanza di RelazioneDiOrdineTotale, allora per ogni inst1,inst2 vale: rel(inst1,inst2 vales o rel(inst2,inst1 vales.
(=>
      (instance ?REL TotalOrderingRelation)
      (forall
            (?INST1 ?INST2)
            (or
                  (holds ?REL ?INST1 ?INST2)
                  (holds ?REL ?INST2 ?INST1))))

Se process é un' istanza di Processo, allora esiste cause tale che process é un agente di cause.
(=>
      (instance ?PROCESS Process)
      (exists
            (?CAUSE)
            (agent ?PROCESS ?CAUSE)))

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

Se rel é un' istanza di RelazioneTernaria, allora non esiste item1,item2,item3,item4, tale che rel(item1,item2,item3,item4, vales.
(=>
      (instance ?REL TernaryRelation)
      (not
            (exists
                  (?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 @ROW)
                  (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 @ROW))))

Se rel é un' istanza di RelazioneQuaternaria, allora non esiste item1,item2,item3,item4,item5, tale che rel(item1,item2,item3,item4,item5, vales.
(=>
      (instance ?REL QuaternaryRelation)
      (not
            (exists
                  (?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 @ROW)
                  (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 @ROW))))

Se rel é un' istanza di RelazioneQuinquenaria, allora non esiste item1,item2,item3,item4,item5,item6, tale che rel(item1,item2,item3,item4,item5,item6, vales.
(=>
      (instance ?REL QuintaryRelation)
      (not
            (exists
                  (?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 ?ITEM6 @ROW)
                  (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 ?ITEM6 @ROW))))

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

list é un' istanza di ListaUnica se e solo se per ogni number1,number2 vale: se "number1th elemento di list" is uguale a "number2th elemento di list", allora number1 is uguale a number2.
(<=>
      (instance ?LIST UniqueList)
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (equal
                        (ListOrderFn ?LIST ?NUMBER1)
                        (ListOrderFn ?LIST ?NUMBER2))
                  (equal ?NUMBER1 ?NUMBER2))))

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

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

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

Se function é un' istanza di FunzioneUnaria, allora function %&ha argomento(s.
(=>
      (instance ?FUNCTION UnaryFunction)
      (valence ?FUNCTION 1))

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

Se function é un' istanza di FunzioneBinaria, allora function %&ha argomento(s.
(=>
      (instance ?FUNCTION BinaryFunction)
      (valence ?FUNCTION 2))

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

Se function é un' istanza di FunzioneTernaria, allora function %&ha argomento(s.
(=>
      (instance ?FUNCTION TernaryFunction)
      (valence ?FUNCTION 3))

Se function é un' istanza di FunzioneQuaternaria, allora function %&ha argomento(s.
(=>
      (instance ?FUNCTION QuaternaryFunction)
      (valence ?FUNCTION 4))

Se rel é un' istanza di PredicatoBinario, allora rel %&ha argomento(s.
(=>
      (instance ?REL BinaryPredicate)
      (valence ?REL 2))

Se rel é un' istanza di PredicatoTernario, allora rel %&ha argomento(s.
(=>
      (instance ?REL TernaryPredicate)
      (valence ?REL 3))

Se rel é un' istanza di PredicatoQuaternario, allora rel %&ha argomento(s.
(=>
      (instance ?REL QuaternaryPredicate)
      (valence ?REL 4))

Se rel é un' istanza di PredicatoQuinquenario, allora rel %&ha argomento(s.
(=>
      (instance ?REL QuintaryPredicate)
      (valence ?REL 5))

Se rel é un' istanza di RelazioneAdAritáVariabile, allora non esiste int tale che rel %&ha int argomento(s.
(=>
      (instance ?REL VariableArityRelation)
      (not
            (exists
                  (?INT)
                  (valence ?REL ?INT))))

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

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

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

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

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

Se proc1 é un' istanza di Processo, allora esiste proc2 tale che proc2 causas proc1.
(=>
      (instance ?PROC1 Process)
      (exists
            (?PROC2)
            (causes ?PROC2 ?PROC1)))

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

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

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

obj é un' istanza di "appartenenze di person" se e solo se person possiedees obj.
(<=>
      (instance
            ?OBJ
            (PropertyFn ?PERSON))
      (possesses ?PERSON ?OBJ))

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

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

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

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

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

Se number é un' istanza di Quantitá, allora "il reciproco di number" is uguale a "number elevato a potenza ".
(=>
      (instance ?NUMBER Quantity)
      (equal
            (ReciprocalFn ?NUMBER)
            (ExponentiationFn ?NUMBER -1)))

Se number é un' istanza di Quantitá, allora is uguale a "number*"il reciproco di number"".
(=>
      (instance ?NUMBER Quantity)
      (equal
            1
            (MultiplicationFn
                  ?NUMBER
                  (ReciprocalFn ?NUMBER))))

Se number é un' istanza di NumeroInteroPari, allora "number mod " is uguale a .
(=>
      (instance ?NUMBER EvenInteger)
      (equal
            (RemainderFn ?NUMBER 2)
            0))

Se number é un' istanza di NumeroInteroDispari, allora "number mod " is uguale a .
(=>
      (instance ?NUMBER OddInteger)
      (equal
            (RemainderFn ?NUMBER 2)
            1))

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

Se number é un' istanza di NumeroRealeNonNegativo, allora "il segno di number" is uguale a o "il segno di number" is uguale a .
(=>
      (instance ?NUMBER NonnegativeRealNumber)
      (or
            (equal
                  (SignumFn ?NUMBER)
                  1)
            (equal
                  (SignumFn ?NUMBER)
                  0)))

Se number é un' istanza di NumeroRealePositivo, allora "il segno di number" is uguale a .
(=>
      (instance ?NUMBER PositiveRealNumber)
      (equal
            (SignumFn ?NUMBER)
            1))

Se number é un' istanza di NumeroRealeNegativo, allora "il segno di number" is uguale a .
(=>
      (instance ?NUMBER NegativeRealNumber)
      (equal
            (SignumFn ?NUMBER)
            -1))

Se degree é un' istanza di MisuraDiAngoloPiano, allora "la tangente di degree" is uguale a ""il seno di degree"/"il coseno di degree"".
(=>
      (instance ?DEGREE PlaneAngleMeasure)
      (equal
            (TangentFn ?DEGREE)
            (DivisionFn
                  (SineFn ?DEGREE)
                  (CosineFn ?DEGREE))))

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

Se int é un' istanza di NumeroIntero, allora int é meno di"(int+1".
(=>
      (instance ?INT Integer)
      (lessThan
            ?INT
            (SuccessorFn ?INT)))

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 int é un' istanza di NumeroIntero, allora int is uguale a "("(int+2"+1".
(=>
      (instance ?INT Integer)
      (equal
            ?INT
            (SuccessorFn
                  (PredecessorFn ?INT))))

Se int é un' istanza di NumeroIntero, allora int is uguale a "("(int+1"+2".
(=>
      (instance ?INT Integer)
      (equal
            ?INT
            (PredecessorFn
                  (SuccessorFn ?INT))))

Se int é un' istanza di NumeroIntero, allora int é più grande di "(int+2".
(=>
      (instance ?INT Integer)
      (greaterThan
            ?INT
            (PredecessorFn ?INT)))

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 node é un' istanza di NodoDelGrafo, allora esiste other,arc tale che arc legas node e other.
(=>
      (instance ?NODE GraphNode)
      (exists
            (?OTHER ?ARC)
            (links ?NODE ?OTHER ?ARC)))

Se arc é un' istanza di ArcoDelGrafo, allora esiste node1,node2 tale che arc legas node1 e node2.
(=>
      (instance ?ARC GraphArc)
      (exists
            (?NODE1 ?NODE2)
            (links ?NODE1 ?NODE2 ?ARC)))

loop é un' istanza di GrafoCiclico se e solo se esiste node tale che loop legas node e node.
(<=>
      (instance ?LOOP GraphLoop)
      (exists
            (?NODE)
            (links ?NODE ?NODE ?LOOP)))

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 "il cammino col minor costo tra node1 e node2" is uguale a path, allora path é un' istanza di "l' insieme di cammini tra node1 e node2".
(=>
      (equal
            (MinimalWeightedPathFn ?NODE1 ?NODE2)
            ?PATH)
      (instance
            ?PATH
            (GraphPathFn ?NODE1 ?NODE2)))

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

Se "il il cammino col costo maggiore tra node1 e node2" is uguale a path, allora path é un' istanza di "l' insieme di cammini tra node1 e node2".
(=>
      (equal
            (MaximalWeightedPathFn ?NODE1 ?NODE2)
            ?PATH)
      (instance
            ?PATH
            (GraphPathFn ?NODE1 ?NODE2)))

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

Se graph é un' istanza di Grafo, allora "l' insieme di cammini minimi che partiziona graphin due separati grafi" é una sottoclasse di "l' insieme di cammini che partiziona graph in due grafi separati".
(=>
      (instance ?GRAPH Graph)
      (subclass
            (MinimalCutSetFn ?GRAPH)
            (CutSetFn ?GRAPH)))

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

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

Se unit é un' istanza di UnitáDiMisura, allora "1 mille units" is uguale a " unit(s".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (KiloFn ?UNIT)
            (MeasureFn 1000 ?UNIT)))

Se unit é un' istanza di UnitáDiMisura, allora "1 milione units" is uguale a " unit(s".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MegaFn ?UNIT)
            (MeasureFn 1000000 ?UNIT)))

Se unit é un' istanza di UnitáDiMisura, allora "1 miliardo units " is uguale a " unit(s".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (GigaFn ?UNIT)
            (MeasureFn 1000000000 ?UNIT)))

Se unit é un' istanza di UnitáDiMisura, allora "1 trilione units" is uguale a " unit(s".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (TeraFn ?UNIT)
            (MeasureFn 1000000000000 ?UNIT)))

Se unit é un' istanza di UnitáDiMisura, allora "unmillesimo di un unit" is uguale a " unit(s".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MilliFn ?UNIT)
            (MeasureFn 0.001 ?UNIT)))

Se unit é un' istanza di UnitáDiMisura, allora "un milionesimo di unit" is uguale a " unit(s".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MicroFn ?UNIT)
            (MeasureFn 0.000001 ?UNIT)))

Se unit é un' istanza di UnitáDiMisura, allora "un miliardesimo di un unit" is uguale a " unit(s".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (NanoFn ?UNIT)
            (MeasureFn 0.000000001 ?UNIT)))

Se unit é un' istanza di UnitáDiMisura, allora "un trilionesimo di un unit" is uguale a " unit(s".
(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (PicoFn ?UNIT)
            (MeasureFn 0.000000000001 ?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 number é un' istanza di NumeroReale, allora "number centimeter(s" is uguale a ""number*" meter(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Centimeter)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  Meter)))

Se number é un' istanza di NumeroReale, allora "number celsius degree(s" is uguale a ""(number-" kelvin degree(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER CelsiusDegree)
            (MeasureFn
                  (SubtractionFn ?NUMBER 273.15)
                  KelvinDegree)))

Se number é un' istanza di NumeroReale, allora "number celsius degree(s" is uguale a """(number-"/" fahrenheit degree(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER CelsiusDegree)
            (MeasureFn
                  (DivisionFn
                        (SubtractionFn ?NUMBER 32)
                        1.8)
                  FahrenheitDegree)))

Se number é un' istanza di NumeroReale, allora "number day duration(s" is uguale a ""number*" hour duration(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER DayDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 24)
                  HourDuration)))

Se number é un' istanza di NumeroReale, allora "number hour duration(s" is uguale a ""number*" minute duration(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER HourDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 60)
                  MinuteDuration)))

Se number é un' istanza di NumeroReale, allora "number minute duration(s" is uguale a ""number*" second duration(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER MinuteDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 60)
                  SecondDuration)))

Se number é un' istanza di NumeroReale, allora "number week duration(s" is uguale a ""number*" day duration(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER WeekDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 7)
                  DayDuration)))

Se number é un' istanza di NumeroReale, allora "number year duration(s" is uguale a ""number*" day duration(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER YearDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 365)
                  DayDuration)))

Se number é un' istanza di NumeroReale, allora "number amu(s" is uguale a ""number**" gram(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Amu)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.6605402 E-24)
                  Gram)))

Se number é un' istanza di NumeroReale, allora "number electron volt(s" is uguale a ""number**" joule(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER ElectronVolt)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.60217733 E-19)
                  Joule)))

Se number é un' istanza di NumeroReale, allora "number angstrom(s" is uguale a ""number**" meter(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Angstrom)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.0 E-10)
                  Meter)))

Se number é un' istanza di NumeroReale, allora "number foot(s" is uguale a ""number*" meter(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Foot)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.3048)
                  Meter)))

Se number é un' istanza di NumeroReale, allora "number inch(s" is uguale a ""number*" meter(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Inch)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.0254)
                  Meter)))

Se number é un' istanza di NumeroReale, allora "number mile(s" is uguale a ""number*" meter(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Mile)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1609.344)
                  Meter)))

Se number é un' istanza di NumeroReale, allora "number united states gallon(s" is uguale a ""number*" liter(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedStatesGallon)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 3.785411784)
                  Liter)))

Se number é un' istanza di NumeroReale, allora "number quart(s" is uguale a ""number/" united states gallon(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Quart)
            (MeasureFn
                  (DivisionFn ?NUMBER 4)
                  UnitedStatesGallon)))

Se number é un' istanza di NumeroReale, allora "number pint(s" is uguale a ""number/" quart(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Pint)
            (MeasureFn
                  (DivisionFn ?NUMBER 2)
                  Quart)))

Se number é un' istanza di NumeroReale, allora "number cup(s" is uguale a ""number/" pint(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Cup)
            (MeasureFn
                  (DivisionFn ?NUMBER 2)
                  Pint)))

Se number é un' istanza di NumeroReale, allora "number ounce(s" is uguale a ""number/" cup(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Ounce)
            (MeasureFn
                  (DivisionFn ?NUMBER 8)
                  Cup)))

Se number é un' istanza di NumeroReale, allora "number united kingdom gallon(s" is uguale a ""number*" liter(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedKingdomGallon)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.54609)
                  Liter)))

Se number é un' istanza di NumeroReale, allora "number pound mass(s" is uguale a ""number*" gram(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER PoundMass)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 453.59237)
                  Gram)))

Se number é un' istanza di NumeroReale, allora "number slug(s" is uguale a ""number*" gram(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Slug)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 14593.90)
                  Gram)))

Se number é un' istanza di NumeroReale, allora "number rankine degree(s" is uguale a ""number*" kelvin degree(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER RankineDegree)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.8)
                  KelvinDegree)))

Se number é un' istanza di NumeroReale, allora "number pound force(s" is uguale a ""number*" newton(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER PoundForce)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.448222)
                  Newton)))

Se number é un' istanza di NumeroReale, allora "number calorie(s" is uguale a ""number*" joule(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Calorie)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.1868)
                  Joule)))

Se number é un' istanza di NumeroReale, allora "number british thermal unit(s" is uguale a ""number*" joule(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER BritishThermalUnit)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1055.05585262)
                  Joule)))

Se number é un' istanza di NumeroReale, allora "number angular degree(s" is uguale a ""number*"PiGreco/"" radian(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER AngularDegree)
            (MeasureFn
                  (MultiplicationFn
                        ?NUMBER
                        (DivisionFn Pi 180))
                  Radian)))

Se number é un' istanza di NumeroReale, allora "number united states cent(s" is uguale a ""number*" united states dollar(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedStatesCent)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  UnitedStatesDollar)))

Se number é un' istanza di NumeroReale, allora "number euro cent(s" is uguale a ""number*" euro dollar(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER EuroCent)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  EuroDollar)))

Se number é un' istanza di NumeroReale, allora "number byte(s" is uguale a ""number*" bit(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Byte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 8)
                  Bit)))

Se number é un' istanza di NumeroReale, allora "number kilo byte(s" is uguale a ""number*" byte(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER KiloByte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1024)
                  Byte)))

Se number é un' istanza di NumeroReale, allora "number mega byte(s" is uguale a ""number*" kilo byte(s".
(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER MegaByte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1024)
                  KiloByte)))

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 "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)))

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

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 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 thing é un' istanza di EntitáConcreta, allora "l' inizio di "il tempo di esistenza di thing"" succede?{s} prima di "la fine di "il tempo di esistenza di thing"".
(=>
      (instance ?THING Physical)
      (before
            (BeginFn
                  (WhenFn ?THING))
            (EndFn
                  (WhenFn ?THING))))

Se thing é un' istanza di EntitáConcreta, allora "prima "il tempo di esistenza di thing"" incontras "il tempo di esistenza di thing".
(=>
      (instance ?THING Physical)
      (meetsTemporally
            (PastFn
                  (WhenFn ?THING))
            (WhenFn ?THING)))

Se process é un' istanza di EntitáConcreta, allora "prima "il tempo di esistenza di process"" is uguale a "intervallo tra negative infinity e "l' inizio di "il tempo di esistenza di process""".
(=>
      (instance ?PROCESS Physical)
      (equal
            (PastFn
                  (WhenFn ?PROCESS))
            (TimeIntervalFn
                  NegativeInfinity
                  (BeginFn
                        (WhenFn ?PROCESS)))))

Se thing é un' istanza di EntitáConcreta, allora "immediatamente prima di "il tempo di esistenza di thing"" finiscees "prima "il tempo di esistenza di thing"".
(=>
      (instance ?THING Physical)
      (finishes
            (ImmediatePastFn
                  (WhenFn ?THING))
            (PastFn
                  (WhenFn ?THING))))

Se thing é un' istanza di EntitáConcreta, allora "il tempo di esistenza di thing" incontras "dopo "il tempo di esistenza di thing"".
(=>
      (instance ?THING Physical)
      (meetsTemporally
            (WhenFn ?THING)
            (FutureFn
                  (WhenFn ?THING))))

Se process é un' istanza di EntitáConcreta, allora "dopo "il tempo di esistenza di process"" is uguale a "intervallo tra "la fine di "il tempo di esistenza di process"" e positive infinity".
(=>
      (instance ?PROCESS Physical)
      (equal
            (FutureFn
                  (WhenFn ?PROCESS))
            (TimeIntervalFn
                  (EndFn
                        (WhenFn ?PROCESS))
                  PositiveInfinity)))

Se thing é un' istanza di EntitáConcreta, allora "immediatamente dopo "il tempo di esistenza di thing"" inizias "dopo "il tempo di esistenza di thing"".
(=>
      (instance ?THING Physical)
      (starts
            (ImmediateFutureFn
                  (WhenFn ?THING))
            (FutureFn
                  (WhenFn ?THING))))

Se day é un' istanza di "il giorno number", allora number é minore o uguale a .
(=>
      (instance
            ?DAY
            (DayFn ?NUMBER ?MONTH))
      (lessThanOrEqualTo ?NUMBER 31))

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 hour é un' istanza di "l' ora number", allora number é meno di.
(=>
      (instance
            ?HOUR
            (HourFn ?NUMBER ?DAY))
      (lessThan ?NUMBER 24))

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 minute é un' istanza di "il minutonumber", allora number é meno di.
(=>
      (instance
            ?MINUTE
            (MinuteFn ?NUMBER ?HOUR))
      (lessThan ?NUMBER 60))

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 second é un' istanza di "il secondo number", allora number é meno di.
(=>
      (instance
            ?SECOND
            (SecondFn ?NUMBER ?MINUTE))
      (lessThan ?NUMBER 60))

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 year é un' istanza di Anno, allora durata di year é " year duration(s".
(=>
      (instance ?YEAR Year)
      (duration
            ?YEAR
            (MeasureFn 1 YearDuration)))

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 month é un' istanza di Gennaio, allora durata di month é " day duration(s".
(=>
      (instance ?MONTH January)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

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 month é un' istanza di Marzo, allora durata di month é " day duration(s".
(=>
      (instance ?MONTH March)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

Se month é un' istanza di Aprile, allora durata di month é " day duration(s".
(=>
      (instance ?MONTH April)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

Se month é un' istanza di Maggio, allora durata di month é " day duration(s".
(=>
      (instance ?MONTH May)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

Se month é un' istanza di Giugno, allora durata di month é " day duration(s".
(=>
      (instance ?MONTH June)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

Se month é un' istanza di Luglio, allora durata di month é " day duration(s".
(=>
      (instance ?MONTH July)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

Se month é un' istanza di Agosto, allora durata di month é " day duration(s".
(=>
      (instance ?MONTH August)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

Se month é un' istanza di Settembre, allora durata di month é " day duration(s".
(=>
      (instance ?MONTH September)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

Se month é un' istanza di Ottobre, allora durata di month é " day duration(s".
(=>
      (instance ?MONTH October)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

Se month é un' istanza di Novembre, allora durata di month é " day duration(s".
(=>
      (instance ?MONTH November)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

Se month é un' istanza di Dicembre, allora durata di month é " day duration(s".
(=>
      (instance ?MONTH December)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

Se day é un' istanza di Giorno, allora durata di day é " day duration(s".
(=>
      (instance ?DAY Day)
      (duration
            ?DAY
            (MeasureFn 1 DayDuration)))

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

Se week é un' istanza di Settimana, allora durata di week é " week duration(s".
(=>
      (instance ?WEEK Week)
      (duration
            ?WEEK
            (MeasureFn 1 WeekDuration)))

Se hour é un' istanza di Ora, allora durata di hour é " hour duration(s".
(=>
      (instance ?HOUR Hour)
      (duration
            ?HOUR
            (MeasureFn 1 HourDuration)))

Se minute é un' istanza di Minuto, allora durata di minute é " minute duration(s".
(=>
      (instance ?MINUTE Minute)
      (duration
            ?MINUTE
            (MeasureFn 1 MinuteDuration)))

Se second é un' istanza di Secondo, allora durata di second é " second duration(s".
(=>
      (instance ?SECOND Second)
      (duration
            ?SECOND
            (MeasureFn 1 SecondDuration)))

(=>
      (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 year é un' istanza di Anno, allora "il numero di istanzia in "decomposizione di year in ? Meses"" is uguale a .
(=>
      (instance ?YEAR Year)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?YEAR Month))
            12))

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

Se week é un' istanza di Settimana, allora "il numero di istanzia in "decomposizione di week in ? Giornos"" is uguale a .
(=>
      (instance ?WEEK Week)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?WEEK Day))
            7))

Se day é un' istanza di Giorno, allora "il numero di istanzia in "decomposizione di day in ? Oras"" is uguale a .
(=>
      (instance ?DAY Day)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?DAY Hour))
            24))

Se hour é un' istanza di Ora, allora "il numero di istanzia in "decomposizione di hour in ? Minutos"" is uguale a .
(=>
      (instance ?HOUR Hour)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?HOUR Minute))
            60))

Se minute é un' istanza di Minuto, allora "il numero di istanzia in "decomposizione di minute in ? Secondos"" is uguale a .
(=>
      (instance ?MINUTE Minute)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?MINUTE Second))
            60))

obj é un' istanza di OggettoIntegro se e solo se per ogni part1,part2 vale: se obj is uguale a "l' unione delle parti di part1 e part2", allora part1 é connesso a part2.
(<=>
      (instance ?OBJ SelfConnectedObject)
      (forall
            (?PART1 ?PART2)
            (=>
                  (equal
                        ?OBJ
                        (MereologicalSumFn ?PART1 ?PART2))
                  (connected ?PART1 ?PART2))))

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

hole é un' istanza di Apertura se e solo se esiste obj tale che hole é un' apertura in obj.
(<=>
      (instance ?HOLE Hole)
      (exists
            (?OBJ)
            (hole ?HOLE ?OBJ)))

Se hole é un' apertura in obj, allora obj é not un' istanza di Apertura.
(=>
      (hole ?HOLE ?OBJ)
      (not
            (instance ?OBJ Hole)))

Se hole1 é un' istanza di Apertura, allora esiste hole2 tale che hole2 é una Parte propria di hole1.
(=>
      (instance ?HOLE1 Hole)
      (exists
            (?HOLE2)
            (properPart ?HOLE2 ?HOLE1)))

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

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 agent é un' istanza di AgenteCognitivo, allora agent é capace di fare Ragionare nel ruolo agent.
(=>
      (instance ?AGENT CognitiveAgent)
      (capability Reasoning agent ?AGENT))

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

Se action é un' istanza di Creazione, allora esiste result tale che result é un risultato di action.
(=>
      (instance ?ACTION Creation)
      (exists
            (?RESULT)
            (result ?ACTION ?RESULT)))

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

(=>
      (instance ?COOPERATE Cooperation)
      (exists
            (?PURP)
            (forall
                  (?AGENT)
                  (=>
                        (agent ?COOPERATE ?AGENT)
                        (hasPurposeForAgent ?COOPERATE ?PURP ?AGENT)))))

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 agent é un' istanza di AgenteSensibile, allora agent é capace di fare Percezione nel ruolo experiencer.
(=>
      (instance ?AGENT SentientAgent)
      (capability Perception experiencer ?AGENT))

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

Se organism é un' istanza di Organismo, allora esiste parent tale che parent é un parente di organism.
(=>
      (instance ?ORGANISM Organism)
      (exists
            (?PARENT)
            (parent ?ORGANISM ?PARENT)))

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 bev é un' istanza di Bevanda, allora liquid is an attribute of bev.
(=>
      (instance ?BEV Beverage)
      (attribute ?BEV Liquid))

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 organ é un' istanza di Organo, allora esiste purp tale che organ ha scopo purp.
(=>
      (instance ?ORGAN Organ)
      (exists
            (?PURP)
            (hasPurpose ?ORGAN ?PURP)))

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 instrument é un' istanza di StrumentoMusicale, allora instrument é capace di fare Musica nel ruolo instrument.
(=>
      (instance ?INSTRUMENT MusicalInstrument)
      (capability Music instrument ?INSTRUMENT))

Se device é un' istanza di MezzoDiTrasporto, allora device é capace di fare Trasporto nel ruolo instrument.
(=>
      (instance ?DEVICE TransportationDevice)
      (capability Transportation instrument ?DEVICE))

Se weapon é un' istanza di Arma, allora weapon é capace di fare Danneggiare nel ruolo instrument.
(=>
      (instance ?WEAPON Weapon)
      (capability Damaging instrument ?WEAPON))

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 é not un' istanza di MeccanismiDiConnessione e comp2 é not un' istanza di MeccanismiDiConnessione.
(=>
      (connectedEngineeringComponents ?COMP1 ?COMP2)
      (not
            (or
                  (instance ?COMP1 EngineeringConnection)
                  (instance ?COMP2 EngineeringConnection))))

Se connection é un' istanza di MeccanismiDiConnessione, allora esiste comp1,comp2 tale che connection connette comp1 e comp2.
(=>
      (instance ?CONNECTION EngineeringConnection)
      (exists
            (?COMP1 ?COMP2)
            (connectsEngineeringComponents ?CONNECTION ?COMP1 ?COMP2)))

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 "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 plan é un' istanza di Programma, allora esiste purp tale che plan ha scopo purp.
(=>
      (instance ?PLAN Plan)
      (exists
            (?PURP)
            (hasPurpose ?PLAN ?PURP)))

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

Se obj é un' istanza di Soluzione, allora liquid is an attribute of obj.
(=>
      (instance ?OBJ Solution)
      (attribute ?OBJ Liquid))

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 obj é un' istanza di Oggetto, allora monochromatic is an attribute of obj o polychromatic is an attribute of obj.
(=>
      (instance ?OBJ Object)
      (or
            (attribute ?OBJ Monochromatic)
            (attribute ?OBJ Polychromatic)))

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 obj é un' istanza di OggettoIntegro, allora pliable is an attribute of obj o rigid is an attribute of obj.
(=>
      (instance ?OBJ SelfConnectedObject)
      (or
            (attribute ?OBJ Pliable)
            (attribute ?OBJ Rigid)))

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

(=>
      (instance ?ATTR PsychologicalAttribute)
      (=>
            (holdsDuring
                  ?TIME
                  (attribute ?ORGANISM ?ATTR))
            (holdsDuring
                  ?TIME
                  (attribute ?ORGANISM Living))))

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 o entity é un' istanza di class2.
(<=>
      (instance
            ?ENTITY
            (UnionFn ?CLASS1 ?CLASS2))
      (or
            (instance ?ENTITY ?CLASS1)
            (instance ?ENTITY ?CLASS2)))

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

entity é un' istanza di "il complemento di class" se e solo se entity é not un' istanza di class.
(<=>
      (instance
            ?ENTITY
            (ComplementFn ?CLASS))
      (not
            (instance ?ENTITY ?CLASS)))

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

entity é un' istanza di "l' intersezione di tutti gli elementi di superclass" se e solo se per ogni class vale: se class é un' istanza di superclass, allora entity é un' istanza di class.
(<=>
      (instance
            ?ENTITY
            (GeneralizedIntersectionFn ?SUPERCLASS))
      (forall
            (?CLASS)
            (=>
                  (instance ?CLASS ?SUPERCLASS)
                  (instance ?ENTITY ?CLASS))))

subclass é un' istanza di "ogni sottoclasse di class" se e solo se subclass é una sottoclasse di class.
(<=>
      (instance
            ?SUBCLASS
            (PowerSetFn ?CLASS))
      (subclass ?SUBCLASS ?CLASS))