not (not)
The truth-functional connective of negation.
Ontology
SUMO / STRUCTURAL-ONTOLOGYClass(es)
Coordinate term(s)
<=>
=>
and
entails
exists
forall
or
Type restrictions
not(formula)
Related WordNet synsets
- negation
- the negative of the opposition
- not
- negation of a word or group of words; "he does not speak French"; "she is not going"; "they are not friends"; "not many"; "not much"; "not at all"
- no
- not in any degree or manner; not at all; "he is no better today"
See more related synsets on a separate page.
Axioms (121)
If entity is an immediate instance of class, then there doesn't exist class subclass so that entity is an instance of subclass.
(=>
(immediateInstance ?ENTITY ?CLASS)
(not
(exists
(?SUBCLASS)
(and
(subclass ?SUBCLASS ?CLASS)
(instance ?ENTITY ?SUBCLASS)))))
If class1 is an immediate subclass of class2, then there doesn't exist class2 class3 so that class1 is a subclass of class3 and class2 is not equal to class3 and class1 is not equal to class3.
(=>
(immediateSubclass ?CLASS1 ?CLASS2)
(not
(exists
(?CLASS3)
(and
(subclass ?CLASS3 ?CLASS2)
(subclass ?CLASS1 ?CLASS3)
(not
(equal ?CLASS2 ?CLASS3))
(not
(equal ?CLASS1 ?CLASS3))))))
class1 is disjoint from class2 if and only if
(<=>
(disjoint ?CLASS1 ?CLASS2)
(and
(instance ?CLASS1 SetOrClass)
(instance ?CLASS2 SetOrClass)
(forall
(?INST)
(not
(and
(instance ?INST ?CLASS1)
(instance ?INST ?CLASS2))))))
If and ? are disjoint and rel1 is a member of "()" and rel2 is a member of "()" and rel1 is not equal to rel2 and rel1() holds, then rel2() doesn't hold.
(=>
(and
(disjointRelation @ROW1)
(inList
?REL1
(ListFn @ROW1))
(inList
?REL2
(ListFn @ROW1))
(not
(equal ?REL1 ?REL2))
(holds ?REL1 @ROW2))
(not
(holds ?REL2 @ROW2)))
- if is opposed to ?,
- then for all attr1,attr2 holds:
.
(=>
(contraryAttribute @ROW)
(forall
(?ATTR1 ?ATTR2)
(=>
(and
(equal
?ATTR1
(ListOrderFn
(ListFn @ROW)
?NUMBER1))
(equal
?ATTR2
(ListOrderFn
(ListFn @ROW)
?NUMBER2))
(not
(equal ?NUMBER1 ?NUMBER2)))
(=>
(property ?OBJ ?ATTR1)
(not
(property ?OBJ ?ATTR2))))))
obj1 is a properPart of obj2 if and only if obj1 is a part of obj2 and obj2 is not a part of obj1.
(<=>
(properPart ?OBJ1 ?OBJ2)
(and
(part ?OBJ1 ?OBJ2)
(not
(part ?OBJ2 ?OBJ1))))
If mixture is an instance of mixture, then there exist pure substance pure1,pure substance pure2 so that pure1 is not equal to pure2 and pure1 is a piece of mixture and pure2 is a piece of mixture.
(=>
(instance ?MIXTURE Mixture)
(exists
(?PURE1 ?PURE2)
(and
(subclass ?PURE1 PureSubstance)
(subclass ?PURE2 PureSubstance)
(not
(equal ?PURE1 ?PURE2))
(piece ?PURE1 ?MIXTURE)
(piece ?PURE2 ?MIXTURE))))
If obj is an instance of corpuscular object, then there exist substance substance1,substance substance2 so that substance1 is made of obj and substance2 is made of obj and substance1 is not equal to substance2.
(=>
(instance ?OBJ CorpuscularObject)
(exists
(?SUBSTANCE1 ?SUBSTANCE2)
(and
(subclass ?SUBSTANCE1 Substance)
(subclass ?SUBSTANCE2 Substance)
(material ?SUBSTANCE1 ?OBJ)
(material ?SUBSTANCE2 ?OBJ)
(not
(equal ?SUBSTANCE1 ?SUBSTANCE2)))))
If lang is an instance of animal language and proc is an agent of agent and lang is an instrument for proc, then agent is an instance of animal and agent is not an instance of human.
(=>
(and
(instance ?LANG AnimalLanguage)
(agent ?PROC ?AGENT)
(instrument ?PROC ?LANG))
(and
(instance ?AGENT Animal)
(not
(instance ?AGENT Human))))
If process is an instance of dual object process, then there exist obj1,obj2 so that obj1 is a patient of process and obj2 is a patient of process and obj1 is not equal to obj2.
(=>
(instance ?PROCESS DualObjectProcess)
(exists
(?OBJ1 ?OBJ2)
(and
(patient ?PROCESS ?OBJ1)
(patient ?PROCESS ?OBJ2)
(not
(equal ?OBJ1 ?OBJ2)))))
abs is an instance of abstract if and only if there doesn't exist point so that abs is located at point or abs exists during point.
(<=>
(instance ?ABS Abstract)
(not
(exists
(?POINT)
(or
(located ?ABS ?POINT)
(time ?ABS ?POINT)))))
If rel is an instance of binary relation, then there don't exist item1,item2,item3, so that rel(item1,item2,item3,) holds.
(=>
(instance ?REL BinaryRelation)
(not
(exists
(?ITEM1 ?ITEM2 ?ITEM3 @ROW)
(holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 @ROW))))
If rel is an instance of irreflexive relation, then for all inst holds: rel(inst,inst) doesn't hold.
(=>
(instance ?REL IrreflexiveRelation)
(forall
(?INST)
(not
(holds ?REL ?INST ?INST))))
(=>
(instance ?REL IntransitiveRelation)
(forall
(?INST1 ?INST2 ?INST3)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST3))
(not
(holds ?REL ?INST1 ?INST3)))))
If rel is an instance of ternary relation, then there don't exist item1,item2,item3,item4, so that rel(item1,item2,item3,item4,) holds.
(=>
(instance ?REL TernaryRelation)
(not
(exists
(?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 @ROW)
(holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 @ROW))))
If rel is an instance of quaternary relation, then there don't exist item1,item2,item3,item4,item5, so that rel(item1,item2,item3,item4,item5,) holds.
(=>
(instance ?REL QuaternaryRelation)
(not
(exists
(?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 @ROW)
(holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 @ROW))))
If rel is an instance of quintary relation, then there don't exist item1,item2,item3,item4,item5,item6, so that rel(item1,item2,item3,item4,item5,item6,) holds.
(=>
(instance ?REL QuintaryRelation)
(not
(exists
(?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 ?ITEM6 @ROW)
(holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 ?ITEM6 @ROW))))
- if list is an instance of list,
- then there exists number1 so that there exists item1 so that "number1th element of list" is not equal to item1 and for all number2 holds: if number2 is an instance of positive integer and number2 is less than number1, then there exists item2 so that "number2th element of list" is equal to item2
.
(=>
(instance ?LIST List)
(exists
(?NUMBER1)
(exists
(?ITEM1)
(and
(not
(equal
(ListOrderFn ?LIST ?NUMBER1)
?ITEM1))
(forall
(?NUMBER2)
(=>
(and
(instance ?NUMBER2 PositiveInteger)
(lessThan ?NUMBER2 ?NUMBER1))
(exists
(?ITEM2)
(equal
(ListOrderFn ?LIST ?NUMBER2)
?ITEM2))))))))
list is equal to null list if and only if there doesn't exist item so that item is a member of list.
(<=>
(equal ?LIST NullList)
(not
(exists
(?ITEM)
(inList ?ITEM ?LIST))))
- if class is disjointly decomposed into ,
- then for all item1,item2 holds: if item1 is a member of "()" and item2 is a member of "()" and item1 is not equal to item2, then item1 is disjoint from item2
.
(=>
(disjointDecomposition ?CLASS @ROW)
(forall
(?ITEM1 ?ITEM2)
(=>
(and
(inList
?ITEM1
(ListFn @ROW))
(inList
?ITEM2
(ListFn @ROW))
(not
(equal ?ITEM1 ?ITEM2)))
(disjoint ?ITEM1 ?ITEM2))))
(=>
(instance ?FUN OneToOneFunction)
(forall
(?ARG1 ?ARG2)
(=>
(and
(domain ?FUN 1 ?CLASS)
(instance ?ARG1 ?CLASS)
(instance ?ARG2 ?CLASS)
(not
(equal ?ARG1 ?ARG2)))
(not
(equal
(AssignmentFn ?FUN ?ARG1)
(AssignmentFn ?FUN ?ARG2))))))
If rel is an instance of variable arity relation, then there doesn't exist int so that rel %&has int argument(s).
(=>
(instance ?REL VariableArityRelation)
(not
(exists
(?INT)
(valence ?REL ?INT))))
- if relation is irreflexive on class,
- then for all inst holds: if inst is an instance of class, then relation(inst,inst) doesn't hold
.
(=>
(irreflexiveOn ?RELATION ?CLASS)
(forall
(?INST)
(=>
(instance ?INST ?CLASS)
(not
(holds ?RELATION ?INST ?INST)))))
If situation during time, then situation holds during time.
(=>
(holdsDuring
?TIME
(not ?SITUATION))
(not
(holdsDuring ?TIME ?SITUATION)))
If obj is exactly located in region, then there doesn't exist otherobj so that otherobj is exactly located in region and otherobj is not equal to obj.
(=>
(exactlyLocated ?OBJ ?REGION)
(not
(exists
(?OTHEROBJ)
(and
(exactlyLocated ?OTHEROBJ ?REGION)
(not
(equal ?OTHEROBJ ?OBJ))))))
- if proc1 prevents the occurrence of proc2,
- then for all time,place holds: if there exists proc1 inst1 so that inst1 is located at place during time, then there exists proc2 inst2 so that inst2 is located at place during time
.
(=>
(prevents ?PROC1 ?PROC2)
(forall
(?TIME ?PLACE)
(=>
(holdsDuring
?TIME
(exists
(?INST1)
(and
(instance ?INST1 ?PROC1)
(located ?INST1 ?PLACE))))
(not
(holdsDuring
?TIME
(exists
(?INST2)
(and
(instance ?INST2 ?PROC2)
(located ?INST2 ?PLACE))))))))
If "the ceiling of number" is equal to int, then there doesn't exist integer otherint so that otherint is greater than or equal to number and otherint is less than int.
(=>
(equal
(CeilingFn ?NUMBER)
?INT)
(not
(exists
(?OTHERINT)
(and
(instance ?OTHERINT Integer)
(greaterThanOrEqualTo ?OTHERINT ?NUMBER)
(lessThan ?OTHERINT ?INT)))))
If "the largest integer less than or equal to number" is equal to int, then there doesn't exist integer otherint so that otherint is less than or equal to number and otherint is greater than int.
(=>
(equal
(FloorFn ?NUMBER)
?INT)
(not
(exists
(?OTHERINT)
(and
(instance ?OTHERINT Integer)
(lessThanOrEqualTo ?OTHERINT ?NUMBER)
(greaterThan ?OTHERINT ?INT)))))
- if "the greatest common divisor of " is equal to number,
- then there doesn't exist greater so that greater is greater than number and for all element holds: if element is a member of "()", then "element mod greater" is equal to
.
(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(not
(exists
(?GREATER)
(and
(greaterThan ?GREATER ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?GREATER)
0)))))))
- if "the least common multiple of " is equal to number,
- then there doesn't exist less so that less is less than number and for all element holds: if element is a member of "()", then "less mod element" is equal to
.
(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(not
(exists
(?LESS)
(and
(lessThan ?LESS ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?LESS ?ELEMENT)
0)))))))
If int1 is an instance of integer and int2 is an instance of integer, then int1 is not less than int2 or int2 is not less than "(int1+1)".
(=>
(and
(instance ?INT1 Integer)
(instance ?INT2 Integer))
(not
(and
(lessThan ?INT1 ?INT2)
(lessThan
?INT2
(SuccessorFn ?INT1)))))
If int1 is an instance of integer and int2 is an instance of integer, then int2 is not less than int1 or "(int1+2)" is not less than int2.
(=>
(and
(instance ?INT1 Integer)
(instance ?INT2 Integer))
(not
(and
(lessThan ?INT2 ?INT1)
(lessThan
(PredecessorFn ?INT1)
?INT2))))
There doesn't exist element so that element is an element of null set.
(not
(exists
(?ELEMENT)
(element ?ELEMENT NullSet)))
(=>
(instance ?CLASS MutuallyDisjointClass)
(forall
(?INST1 ?INST2)
(=>
(and
(instance ?INST1 ?CLASS)
(instance ?INST2 ?INST1))
(exists
(?INST3)
(and
(instance ?INST3 ?CLASS)
(not
(instance ?INST2 ?INST3)))))))
If graph is an instance of graph and node1 is an instance of graph node and node2 is an instance of graph node and node1 is a part of graph and node2 is a part of graph and node1 is not equal to node2, then there exist arc,path so that - arc links node1 and node2
or .
(=>
(and
(instance ?GRAPH Graph)
(instance ?NODE1 GraphNode)
(instance ?NODE2 GraphNode)
(graphPart ?NODE1 ?GRAPH)
(graphPart ?NODE2 ?GRAPH)
(not
(equal ?NODE1 ?NODE2)))
(exists
(?ARC ?PATH)
(or
(links ?NODE1 ?NODE2 ?ARC)
(and
(subGraph ?PATH ?GRAPH)
(instance ?PATH GraphPath)
(or
(and
(equal
(BeginNodeFn ?PATH)
?NODE1)
(equal
(EndNodeFn ?PATH)
?NODE2))
(and
(equal
(BeginNodeFn ?PATH)
?NODE2)
(equal
(EndNodeFn ?PATH)
?NODE1)))))))
If graph is an instance of graph, then there exist node1,node2,node3,arc1,arc2 so that node1 is a part of graph and node2 is a part of graph and node3 is a part of graph and arc1 is a part of graph and arc2 is a part of graph and node2 links arc1 and node1 and node3 links arc2 and node2 and node1 is not equal to node2 and node2 is not equal to node3 and node1 is not equal to node3 and arc1 is not equal to arc2.
(=>
(instance ?GRAPH Graph)
(exists
(?NODE1 ?NODE2 ?NODE3 ?ARC1 ?ARC2)
(and
(graphPart ?NODE1 ?GRAPH)
(graphPart ?NODE2 ?GRAPH)
(graphPart ?NODE3 ?GRAPH)
(graphPart ?ARC1 ?GRAPH)
(graphPart ?ARC2 ?GRAPH)
(links ?ARC1 ?NODE1 ?NODE2)
(links ?ARC2 ?NODE2 ?NODE3)
(not
(equal ?NODE1 ?NODE2))
(not
(equal ?NODE2 ?NODE3))
(not
(equal ?NODE1 ?NODE3))
(not
(equal ?ARC1 ?ARC2)))))
If graph is an instance of tree, then there doesn't exist graph loop loop so that loop is a part of graph.
(=>
(instance ?GRAPH Tree)
(not
(exists
(?LOOP)
(and
(instance ?LOOP GraphLoop)
(graphPart ?LOOP ?GRAPH)))))
(=>
(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 is an instance of multi graph if and only if there exist arc1,arc2,node1,node2 so that arc1 is a part of graph and arc2 is a part of graph and node1 is a part of graph and node2 is a part of graph and arc1 links node1 and node2 and arc2 links node1 and node2 and arc1 is not equal to 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)))))
If path is a part of graph and graph is not an instance of directed graph, then "the set of paths between node1 and node2" is equal to path if and only if "the set of paths between node2 and node1" is equal to path.
(=>
(and
(graphPart ?PATH ?GRAPH)
(not
(instance ?GRAPH DirectedGraph)))
(<=>
(equal
(GraphPathFn ?NODE1 ?NODE2)
?PATH)
(equal
(GraphPathFn ?NODE2 ?NODE1)
?PATH)))
There don't exist the set of paths that partition graph into two separate graphs path1,the set of minimal paths that partition graph into two separate graphs path2 so that the length of path1 is number1 and the length of path2 is number2 and number1 is less than number2.
(not
(exists
(?PATH1 ?PATH2)
(and
(instance
?PATH1
(CutSetFn ?GRAPH))
(instance
?PATH2
(MinimalCutSetFn ?GRAPH))
(pathLength ?PATH1 ?NUMBER1)
(pathLength ?PATH2 ?NUMBER2)
(lessThan ?NUMBER1 ?NUMBER2))))
If point is an instance of time point and point is not equal to positive infinity, then point happen?{s} before positive infinity.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT PositiveInfinity)))
(before ?POINT PositiveInfinity))
If point is an instance of time point and point is not equal to positive infinity, then there exists otherpoint so that otherpoint is between point and positive infinity.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT PositiveInfinity)))
(exists
(?OTHERPOINT)
(temporallyBetween ?POINT ?OTHERPOINT PositiveInfinity)))
If point is an instance of time point and point is not equal to negative infinity, then negative infinity happen?{s} before point.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT NegativeInfinity)))
(before NegativeInfinity ?POINT))
If point is an instance of time point and point is not equal to negative infinity, then there exists otherpoint so that otherpoint is between negative infinity and point.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT NegativeInfinity)))
(exists
(?OTHERPOINT)
(temporallyBetween NegativeInfinity ?OTHERPOINT ?POINT)))
- if "the beginning of interval" is equal to point,
- then for all otherpoint holds: if otherpoint is a part of interval and otherpoint is not equal to point, then point happen?{s} before otherpoint
.
(=>
(equal
(BeginFn ?INTERVAL)
?POINT)
(forall
(?OTHERPOINT)
(=>
(and
(temporalPart ?OTHERPOINT ?INTERVAL)
(not
(equal ?OTHERPOINT ?POINT)))
(before ?POINT ?OTHERPOINT))))
- if "the end of interval" is equal to point,
- then for all otherpoint holds: if otherpoint is a part of interval and otherpoint is not equal to point, then otherpoint happen?{s} before point
.
(=>
(equal
(EndFn ?INTERVAL)
?POINT)
(forall
(?OTHERPOINT)
(=>
(and
(temporalPart ?OTHERPOINT ?INTERVAL)
(not
(equal ?OTHERPOINT ?POINT)))
(before ?OTHERPOINT ?POINT))))
- if obj is a result of proc,
- then for all time holds: if time happen?{s} before "the beginning of "the time of existence of proc"", then obj doesn't exist during time
.
(=>
(result ?PROC ?OBJ)
(forall
(?TIME)
(=>
(before
?TIME
(BeginFn
(WhenFn ?PROC)))
(not
(time ?OBJ ?TIME)))))
If leap is an instance of leap year and leap is equal to "number year(s)", then
(=>
(and
(instance ?LEAP LeapYear)
(equal
?LEAP
(MeasureFn ?NUMBER Year)))
(or
(and
(equal
(RemainderFn ?NUMBER 4)
0)
(not
(equal
(RemainderFn ?NUMBER 100)
0)))
(equal
(RemainderFn ?NUMBER 400)
0)))
If "the month february" is equal to month and year is not an instance of leap year, then duration of month is " day duration(s)".
(=>
(and
(equal
(MonthFn February ?YEAR)
?MONTH)
(not
(instance ?YEAR LeapYear)))
(duration
?MONTH
(MeasureFn 28 DayDuration)))
- if "decomposition of interval into ? interval-types" is equal to class,
- then for all time1,time2 holds: if time1 is an instance of class and time2 is an instance of class and time1 is not equal to time2, then time1 meets time2 or time2 meets time1 or time1 happens earlier than time2 or time2 happens earlier than time1
.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(forall
(?TIME1 ?TIME2)
(=>
(and
(instance ?TIME1 ?CLASS)
(instance ?TIME2 ?CLASS)
(not
(equal ?TIME1 ?TIME2)))
(or
(meetsTemporally ?TIME1 ?TIME2)
(meetsTemporally ?TIME2 ?TIME1)
(earlier ?TIME1 ?TIME2)
(earlier ?TIME2 ?TIME1)))))
- if "decomposition of interval into ? interval-types" is equal to class,
- then for all time1 holds: if time1 is an instance of class and time1 doesn't finish interval, then there exists class time2 so that time1 meets time2
.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(forall
(?TIME1)
(=>
(and
(instance ?TIME1 ?CLASS)
(not
(finishes ?TIME1 ?INTERVAL)))
(exists
(?TIME2)
(and
(instance ?TIME2 ?CLASS)
(meetsTemporally ?TIME1 ?TIME2))))))
- if "decomposition of interval into ? interval-types" is equal to class,
- then for all time1 holds: if time1 is an instance of class and time1 doesn't start interval, then there exists class time2 so that time2 meets time1
.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(forall
(?TIME1)
(=>
(and
(instance ?TIME1 ?CLASS)
(not
(starts ?TIME1 ?INTERVAL)))
(exists
(?TIME2)
(and
(instance ?TIME2 ?CLASS)
(meetsTemporally ?TIME2 ?TIME1))))))
obj1 connects obj2 and obj3 if and only if obj1 is connected to obj2 and obj1 is connected to obj3 and obj2 is not connected to obj3.
(<=>
(connects ?OBJ1 ?OBJ2 ?OBJ3)
(and
(connected ?OBJ1 ?OBJ2)
(connected ?OBJ1 ?OBJ3)
(not
(connected ?OBJ2 ?OBJ3))))
If obj1 is a member of coll and obj2 is a member of coll and obj1 is not equal to obj2, then obj1 doesn't overlap with obj2.
(=>
(and
(member ?OBJ1 ?COLL)
(member ?OBJ2 ?COLL)
(not
(equal ?OBJ1 ?OBJ2)))
(not
(overlapsSpatially ?OBJ1 ?OBJ2)))
obj1 partially overlaps with obj2 if and only if - obj1 is not a part of obj2
and - obj2 is not a part of obj1
and - there exists obj3 so that obj3 is a part of obj1 and obj3 is a part of obj2
.
(<=>
(overlapsPartially ?OBJ1 ?OBJ2)
(and
(not
(part ?OBJ1 ?OBJ2))
(not
(part ?OBJ2 ?OBJ1))
(exists
(?OBJ3)
(and
(part ?OBJ3 ?OBJ1)
(part ?OBJ3 ?OBJ2)))))
If obj1 is a superficial part of obj2, then obj1 is not a interior part of obj2 and there doesn't exist obj3 so that obj3 is a interior part of obj1.
(=>
(superficialPart ?OBJ1 ?OBJ2)
(and
(not
(interiorPart ?OBJ1 ?OBJ2))
(not
(exists
(?OBJ3)
(interiorPart ?OBJ3 ?OBJ1)))))
- if obj1 is a interior part of obj2,
- then for all part holds: if part is a superficial part of obj2, then obj1 doesn't overlap with part
.
(=>
(interiorPart ?OBJ1 ?OBJ2)
(forall
(?PART)
(=>
(superficialPart ?PART ?OBJ2)
(not
(overlapsSpatially ?OBJ1 ?PART)))))
If the bottom of object is bottom and part is a part of object and part is not connected to bottom, then part is above to bottom.
(=>
(and
(bottom ?BOTTOM ?OBJECT)
(part ?PART ?OBJECT)
(not
(connected ?PART ?BOTTOM)))
(orientation ?PART ?BOTTOM Above))
If the top of object is top and part is a part of object and part is not connected to top, then part is below to top.
(=>
(and
(top ?TOP ?OBJECT)
(part ?PART ?OBJECT)
(not
(connected ?PART ?TOP)))
(orientation ?PART ?TOP Below))
If a side of object is side and part is a part of object and part is not connected to side, then there exists direct so that side is direct to part.
(=>
(and
(side ?SIDE ?OBJECT)
(part ?PART ?OBJECT)
(not
(connected ?PART ?SIDE)))
(exists
(?DIRECT)
(orientation ?SIDE ?PART ?DIRECT)))
If obj3 is equal to "the difference between the parts of obj1 and obj2", then for all part holds: part is a part of obj3 if and only if part is a part of obj1 and part is not a part of obj2.
(=>
(equal
?OBJ3
(MereologicalDifferenceFn ?OBJ1 ?OBJ2))
(forall
(?PART)
(<=>
(part ?PART ?OBJ3)
(and
(part ?PART ?OBJ1)
(not
(part ?PART ?OBJ2))))))
If hole is a hole in obj, then obj is not an instance of hole.
(=>
(hole ?HOLE ?OBJ)
(not
(instance ?OBJ Hole)))
If hole is a hole in obj, then hole doesn't overlap with obj.
(=>
(hole ?HOLE ?OBJ)
(not
(overlapsSpatially ?HOLE ?OBJ)))
If hole1 is an instance of hole and hole2 is a properPart of hole1, then there exists obj so that hole1 meets obj and hole2 doesn't meet obj.
(=>
(and
(instance ?HOLE1 Hole)
(properPart ?HOLE2 ?HOLE1))
(exists
(?OBJ)
(and
(meetsSpatially ?HOLE1 ?OBJ)
(not
(meetsSpatially ?HOLE2 ?OBJ)))))
If obj1 fills hole and fillable is an attribute of obj2, then obj1 doesn't overlap with obj2.
(=>
(and
(fills ?OBJ1 ?HOLE)
(attribute ?OBJ2 Fillable))
(not
(overlapsSpatially ?OBJ1 ?OBJ2)))
If rep is an instance of sexual reproduction and organism is a result of rep, then there don't exist mother,father so that mother is a mother of organism and father is a father of organism.
(=>
(and
(instance ?REP SexualReproduction)
(result ?REP ?ORGANISM))
(not
(exists
(?MOTHER ?FATHER)
(and
(mother ?ORGANISM ?MOTHER)
(father ?ORGANISM ?FATHER)))))
If rep is an instance of asexual reproduction and organism is a result of rep, then there don't exist parent1,parent2 so that parent1 is a parent of organism and parent2 is a parent of organism and parent1 is not equal to parent2.
(=>
(and
(instance ?REP AsexualReproduction)
(result ?REP ?ORGANISM))
(not
(exists
(?PARENT1 ?PARENT2)
(and
(parent ?ORGANISM ?PARENT1)
(parent ?ORGANISM ?PARENT2)
(not
(equal ?PARENT1 ?PARENT2))))))
If leave is an instance of leaving an organization and org is an instance of organization and leave is an agent of org and person is a patient of leave, then person is not a member of org immediately after "the time of existence of leave".
(=>
(and
(instance ?LEAVE LeavingAnOrganization)
(instance ?ORG Organization)
(agent ?LEAVE ?ORG)
(patient ?LEAVE ?PERSON))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?LEAVE))
(not
(member ?PERSON ?ORG))))
If fire is an instance of terminating employment and org is an instance of organization and fire is an agent of org and person is a patient of fire, then org doesn't employ person immediately after "the time of existence of fire".
(=>
(and
(instance ?FIRE TerminatingEmployment)
(instance ?ORG Organization)
(agent ?FIRE ?ORG)
(patient ?FIRE ?PERSON))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?FIRE))
(not
(employs ?ORG ?PERSON))))
- if
- path1 is path along with process occurs
and - process origins at source
and - process ends at dest
and - the length of path1 is measure1
and - there don't exist path2,measure2 so that path2 is path along with process occurs and process origins at origin and process ends at dest and the length of path2 is measure2 and measure2 is less than measure1
, - then for all obj holds: if obj is a part of path1, then obj is between source and dest
.
(=>
(and
(path ?PROCESS ?PATH1)
(origin ?PROCESS ?SOURCE)
(destination ?PROCESS ?DEST)
(length ?PATH1 ?MEASURE1)
(not
(exists
(?PATH2 ?MEASURE2)
(and
(path ?PROCESS ?PATH2)
(origin ?PROCESS ?ORIGIN)
(destination ?PROCESS ?DEST)
(length ?PATH2 ?MEASURE2)
(lessThan ?MEASURE2 ?MEASURE1)))))
(forall
(?OBJ)
(=>
(part ?OBJ ?PATH1)
(between ?SOURCE ?OBJ ?DEST))))
If proc is an instance of direction change, then there exists directional attribute attr so that - proc is performed in the manner attr immediately before "the time of existence of proc" and proc is performed in the manner attr immediately after "the time of existence of proc"
or - proc is performed in the manner attr immediately after "the time of existence of proc" and proc is performed in the manner attr immediately before "the time of existence of proc"
.
(=>
(instance ?PROC DirectionChange)
(exists
(?ATTR)
(and
(instance ?ATTR DirectionalAttribute)
(or
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?PROC))
(manner ?PROC ?ATTR))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?PROC))
(not
(manner ?PROC ?ATTR))))
(and
(holdsDuring
(ImmediateFutureFn
(WhenFn ?PROC))
(manner ?PROC ?ATTR))
(holdsDuring
(ImmediatePastFn
(WhenFn ?PROC))
(not
(manner ?PROC ?ATTR))))))))
If transfer is an instance of transfer and transfer is an agent of agent and patient is a patient of transfer, then agent is not equal to patient.
(=>
(and
(instance ?TRANSFER Transfer)
(agent ?TRANSFER ?AGENT)
(patient ?TRANSFER ?PATIENT))
(not
(equal ?AGENT ?PATIENT)))
If remove is an instance of removing and remove origins at place and obj is a patient of remove, then obj is located at place immediately before "the time of existence of remove" and obj is not located at place immediately after "the time of existence of remove".
(=>
(and
(instance ?REMOVE Removing)
(origin ?REMOVE ?PLACE)
(patient ?REMOVE ?OBJ))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?REMOVE))
(located ?OBJ ?PLACE))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?REMOVE))
(not
(located ?OBJ ?PLACE)))))
If put is an instance of putting and put ends at place and obj is a patient of put, then obj is not located at place immediately before "the time of existence of put" and obj is located at place immediately after "the time of existence of put".
(=>
(and
(instance ?PUT Putting)
(destination ?PUT ?PLACE)
(patient ?PUT ?OBJ))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?PUT))
(not
(located ?OBJ ?PLACE)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?PUT))
(located ?OBJ ?PLACE))))
If sub is an instance of substituting, then there exist putting put,removing remove,obj1,obj2,place so that put is a subprocess of sub and remove is a subprocess of sub and obj1 is a patient of remove and remove origins at place and obj2 is a patient of put and put ends at place and obj1 is not equal to obj2.
(=>
(instance ?SUB Substituting)
(exists
(?PUT ?REMOVE ?OBJ1 ?OBJ2 ?PLACE)
(and
(instance ?PUT Putting)
(instance ?REMOVE Removing)
(subProcess ?PUT ?SUB)
(subProcess ?REMOVE ?SUB)
(patient ?REMOVE ?OBJ1)
(origin ?REMOVE ?PLACE)
(patient ?PUT ?OBJ2)
(destination ?PUT ?PLACE)
(not
(equal ?OBJ1 ?OBJ2)))))
If change is an instance of change of possession and obj is a patient of change and agent1 posesses obj immediately before "the time of existence of change" and agent2 posesses obj immediately after "the time of existence of change", then agent1 is not equal to agent2.
(=>
(and
(instance ?CHANGE ChangeOfPossession)
(patient ?CHANGE ?OBJ)
(holdsDuring
(ImmediatePastFn
(WhenFn ?CHANGE))
(possesses ?AGENT1 ?OBJ))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?CHANGE))
(possesses ?AGENT2 ?OBJ)))
(not
(equal ?AGENT1 ?AGENT2)))
If give is an instance of unilateral giving, then there doesn't exist transaction trans so that give is a subprocess of trans.
(=>
(instance ?GIVE UnilateralGiving)
(not
(exists
(?TRANS)
(and
(instance ?TRANS Transaction)
(subProcess ?GIVE ?TRANS)))))
If get is an instance of unilateral getting, then there doesn't exist transaction trans so that get is a subprocess of trans.
(=>
(instance ?GET UnilateralGetting)
(not
(exists
(?TRANS)
(and
(instance ?TRANS Transaction)
(subProcess ?GET ?TRANS)))))
If trans is an instance of transaction, then there exist agent1,agent2,giving give1,giving give2,obj1,obj2 so that give1 is a subprocess of trans and give2 is a subprocess of trans and give1 is an agent of agent1 and give2 is an agent of agent2 and obj1 is a patient of give1 and obj2 is a patient of give2 and give1 ends at agent2 and give2 ends at agent1 and agent1 is not equal to agent2 and obj1 is not equal to obj2.
(=>
(instance ?TRANS Transaction)
(exists
(?AGENT1 ?AGENT2 ?GIVE1 ?GIVE2 ?OBJ1 ?OBJ2)
(and
(instance ?GIVE1 Giving)
(instance ?GIVE2 Giving)
(subProcess ?GIVE1 ?TRANS)
(subProcess ?GIVE2 ?TRANS)
(agent ?GIVE1 ?AGENT1)
(agent ?GIVE2 ?AGENT2)
(patient ?GIVE1 ?OBJ1)
(patient ?GIVE2 ?OBJ2)
(destination ?GIVE1 ?AGENT2)
(destination ?GIVE2 ?AGENT1)
(not
(equal ?AGENT1 ?AGENT2))
(not
(equal ?OBJ1 ?OBJ2)))))
If confine is an instance of confining and person is a patient of confine, then person doesn't desire "person is a patient of confine".
(=>
(and
(instance ?CONFINE Confining)
(patient ?CONFINE ?PERSON))
(not
(desires
?PERSON
(patient ?CONFINE ?PERSON))))
process is an instance of destruction if and only if there exists patient so that patient is a patient of process and patient exists during "immediately before "the time of existence of process"" and patient doesn't exist during "immediately after "the time of existence of process"".
(<=>
(instance ?PROCESS Destruction)
(exists
(?PATIENT)
(and
(patient ?PROCESS ?PATIENT)
(time
?PATIENT
(ImmediatePastFn
(WhenFn ?PROCESS)))
(not
(time
?PATIENT
(ImmediateFutureFn
(WhenFn ?PROCESS)))))))
If attach is an instance of attaching and obj1 is a patient of attach and obj2 is a patient of attach, then obj1 is not connected to obj2 immediately before "the time of existence of attach" and obj1 is connected to obj2 immediately after "the time of existence of attach".
(=>
(and
(instance ?ATTACH Attaching)
(patient ?ATTACH ?OBJ1)
(patient ?ATTACH ?OBJ2))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?ATTACH))
(not
(connected ?OBJ1 ?OBJ2)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ATTACH))
(connected ?OBJ1 ?OBJ2))))
If detach is an instance of detaching and obj1 is a patient of detach and obj2 is a patient of detach, then obj1 is connected to obj2 immediately before "the time of existence of detach" and obj1 is not connected to obj2 immediately after "the time of existence of detach".
(=>
(and
(instance ?DETACH Detaching)
(patient ?DETACH ?OBJ1)
(patient ?DETACH ?OBJ2))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?DETACH))
(connected ?OBJ1 ?OBJ2))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?DETACH))
(not
(connected ?OBJ1 ?OBJ2)))))
combine is an instance of combining and obj1 is a resource for combine and obj2 is a result of combine if and only if obj1 is not a part of obj2 immediately before "the time of existence of combine" and obj1 is a part of obj2 immediately after "the time of existence of 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))))
compound is an instance of compound substance if and only if there exist elemental substance element1,elemental substance element2,chemical synthesis process so that element1 is not equal to element2 and element1 is a resource for process and element2 is a resource for process and compound is a result of 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))))
If change is an instance of internal change and obj is a patient of change, then there exists property so that
(=>
(and
(instance ?CHANGE InternalChange)
(patient ?CHANGE ?OBJ))
(exists
(?PROPERTY)
(or
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?CHANGE))
(attribute ?OBJ ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?CHANGE))
(not
(attribute ?OBJ ?PROPERTY))))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?CHANGE))
(not
(attribute ?OBJ ?PROPERTY)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?CHANGE))
(attribute ?OBJ ?PROPERTY))))))
If alt is an instance of surface change and obj is a patient of alt, then there exist part,property so that part is a superficial part of obj and property is an attribute of part immediately before "the time of existence of alt" and property is not an attribute of part immediately after "the time of existence of alt".
(=>
(and
(instance ?ALT SurfaceChange)
(patient ?ALT ?OBJ))
(exists
(?PART ?PROPERTY)
(and
(superficialPart ?PART ?OBJ)
(holdsDuring
(ImmediatePastFn
(WhenFn ?ALT))
(attribute ?PART ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ALT))
(not
(attribute ?PART ?PROPERTY))))))
If alt is an instance of shape change and obj is a patient of alt, then there exists shape attribute property so that
(=>
(and
(instance ?ALT ShapeChange)
(patient ?ALT ?OBJ))
(exists
(?PROPERTY)
(and
(instance ?PROPERTY ShapeAttribute)
(or
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?ALT))
(attribute ?OBJ ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ALT))
(not
(attribute ?OBJ ?PROPERTY))))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?ALT))
(not
(attribute ?OBJ ?PROPERTY)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ALT))
(attribute ?OBJ ?PROPERTY)))))))
If coloring is an instance of coloring and obj is a patient of coloring, then there exists color attribute property so that property is an attribute of obj immediately before "the time of existence of coloring" and property is not an attribute of obj immediately after "the time of existence of coloring".
(=>
(and
(instance ?COLORING Coloring)
(patient ?COLORING ?OBJ))
(exists
(?PROPERTY)
(and
(instance ?PROPERTY ColorAttribute)
(holdsDuring
(ImmediatePastFn
(WhenFn ?COLORING))
(attribute ?OBJ ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?COLORING))
(not
(attribute ?OBJ ?PROPERTY))))))
process is an instance of creation if and only if there exists patient so that patient is a patient of process and patient exists during "immediately after "the time of existence of process"" and patient doesn't exist during "immediately before "the time of existence of process"".
(<=>
(instance ?PROCESS Creation)
(exists
(?PATIENT)
(and
(patient ?PROCESS ?PATIENT)
(time
?PATIENT
(ImmediateFutureFn
(WhenFn ?PROCESS)))
(not
(time
?PATIENT
(ImmediatePastFn
(WhenFn ?PROCESS)))))))
If pursue is an instance of pursuing and pursue is an agent of agent and obj is a patient of pursue, then agent doesn't posess obj during pursue.
(=>
(and
(instance ?PURSUE Pursuing)
(agent ?PURSUE ?AGENT)
(patient ?PURSUE ?OBJ))
(holdsDuring
?PURSUE
(not
(possesses ?AGENT ?OBJ))))
If investigate is an instance of investigating and investigate is an agent of agent and prop is a patient of investigate, then agent doesn't know prop the time of existence of investigate.
(=>
(and
(instance ?INVESTIGATE Investigating)
(agent ?INVESTIGATE ?AGENT)
(patient ?INVESTIGATE ?PROP))
(holdsDuring
(WhenFn ?INVESTIGATE)
(not
(knows ?AGENT ?PROP))))
If interaction is an instance of social interaction, then there exist agent1,agent2 so that interaction is an agent of agent1 and interaction is an agent of agent2 and agent1 is not equal to agent2.
(=>
(instance ?INTERACTION SocialInteraction)
(exists
(?AGENT1 ?AGENT2)
(and
(agent ?INTERACTION ?AGENT1)
(agent ?INTERACTION ?AGENT2)
(not
(equal ?AGENT1 ?AGENT2)))))
If disseminate is an instance of disseminating, then there exist cognitive agent agent1,cognitive agent agent2 so that disseminate ends at agent1 and disseminate ends at agent2 and agent1 is not equal to agent2.
(=>
(instance ?DISSEMINATE Disseminating)
(exists
(?AGENT1 ?AGENT2)
(and
(destination ?DISSEMINATE ?AGENT1)
(instance ?AGENT1 CognitiveAgent)
(destination ?DISSEMINATE ?AGENT2)
(instance ?AGENT2 CognitiveAgent)
(not
(equal ?AGENT1 ?AGENT2)))))
If question is an instance of questioning and question is an agent of agent and formula is a patient of question and formula is an instance of formula, then agent doesn't know formula the time of existence of question.
(=>
(and
(instance ?QUESTION Questioning)
(agent ?QUESTION ?AGENT)
(patient ?QUESTION ?FORMULA)
(instance ?FORMULA Formula))
(holdsDuring
(WhenFn ?QUESTION)
(not
(knows ?AGENT ?FORMULA))))
If contest is an instance of contest, then there exist agent1,agent2,purp1,purp2 so that contest is an agent of agent1 and contest is an agent of agent2 and contest has &n purpose purp1 for agent1 and contest has &n purpose purp2 for agent2 and agent1 is not equal to agent2 and purp1 is not equal to purp2.
(=>
(instance ?CONTEST Contest)
(exists
(?AGENT1 ?AGENT2 ?PURP1 ?PURP2)
(and
(agent ?CONTEST ?AGENT1)
(agent ?CONTEST ?AGENT2)
(hasPurposeForAgent ?CONTEST ?PURP1 ?AGENT1)
(hasPurposeForAgent ?CONTEST ?PURP2 ?AGENT2)
(not
(equal ?AGENT1 ?AGENT2))
(not
(equal ?PURP1 ?PURP2)))))
If process is an instance of state change and obj is a patient of process, then there exist part,physical state state1,physical state state2 so that part is a part of obj and state1 is not equal to state2 and state1 is an attribute of part immediately before "the time of existence of process" and state2 is an attribute of part immediately after "the time of existence of freeze".
(=>
(and
(instance ?PROCESS StateChange)
(patient ?PROCESS ?OBJ))
(exists
(?PART ?STATE1 ?STATE2)
(and
(part ?PART ?OBJ)
(instance ?STATE1 PhysicalState)
(instance ?STATE2 PhysicalState)
(not
(equal ?STATE1 ?STATE2))
(holdsDuring
(ImmediatePastFn
(WhenFn ?PROCESS))
(attribute ?PART ?STATE1))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?FREEZE))
(attribute ?PART ?STATE2)))))
If island is an instance of island, then there don't exist land area area,part1,part2 so that part1 is a part of island and part2 is a part of area and island is not a part of area and area is not a part of island and part1 is connected to part2.
(=>
(instance ?ISLAND Island)
(not
(exists
(?AREA ?PART1 ?PART2)
(and
(instance ?AREA LandArea)
(part ?PART1 ?ISLAND)
(part ?PART2 ?AREA)
(not
(part ?ISLAND ?AREA))
(not
(part ?AREA ?ISLAND))
(connected ?PART1 ?PART2)))))
If part is an instance of body part, then there doesn't exist pathologic process proc so that part is a result of proc.
(=>
(instance ?PART BodyPart)
(not
(exists
(?PROC)
(and
(instance ?PROC PathologicProcess)
(result ?PROC ?PART)))))
If junct is an instance of body junction, then there exist body part struct1,body part struct2 so that junct is connected to struct1 and junct is connected to struct2 and struct1 is not equal to struct2.
(=>
(instance ?JUNCT BodyJunction)
(exists
(?STRUCT1 ?STRUCT2)
(and
(connected ?JUNCT ?STRUCT1)
(connected ?JUNCT ?STRUCT2)
(instance ?STRUCT1 BodyPart)
(instance ?STRUCT2 BodyPart)
(not
(equal ?STRUCT1 ?STRUCT2)))))
If morph is an instance of morpheme, then there doesn't exist morpheme othermorph so that othermorph is a part of morph and othermorph is not equal to morph.
(=>
(instance ?MORPH Morpheme)
(not
(exists
(?OTHERMORPH)
(and
(instance ?OTHERMORPH Morpheme)
(part ?OTHERMORPH ?MORPH)
(not
(equal ?OTHERMORPH ?MORPH))))))
If phrase is an instance of phrase, then there exist word part1,word part2 so that part1 is a part of phrase and part2 is a part of phrase and part1 is not equal to part2.
(=>
(instance ?PHRASE Phrase)
(exists
(?PART1 ?PART2)
(and
(part ?PART1 ?PHRASE)
(part ?PART2 ?PHRASE)
(instance ?PART1 Word)
(instance ?PART2 Word)
(not
(equal ?PART1 ?PART2)))))
If series is an instance of series, then there exist book book1,book book2 so that series subsumes the content of book1 and series subsumes the content of book2 and book1 is not equal to book2.
(=>
(instance ?SERIES Series)
(exists
(?BOOK1 ?BOOK2)
(and
(instance ?BOOK1 Book)
(instance ?BOOK2 Book)
(subsumesContentInstance ?SERIES ?BOOK1)
(subsumesContentInstance ?SERIES ?BOOK2)
(not
(equal ?BOOK1 ?BOOK2)))))
If mole is an instance of molecule, then there exist atom atom1,atom atom2 so that atom1 is a part of mole and atom2 is a part of mole and atom1 is not equal to atom2.
(=>
(instance ?MOLE Molecule)
(exists
(?ATOM1 ?ATOM2)
(and
(instance ?ATOM1 Atom)
(instance ?ATOM2 Atom)
(part ?ATOM1 ?MOLE)
(part ?ATOM2 ?MOLE)
(not
(equal ?ATOM1 ?ATOM2)))))
If comp1 is connected to comp2, then comp1 is a component of comp2 and comp2 is a component of comp1.
(=>
(connectedEngineeringComponents ?COMP1 ?COMP2)
(and
(not
(engineeringSubcomponent ?COMP1 ?COMP2))
(not
(engineeringSubcomponent ?COMP2 ?COMP1))))
If comp1 is connected to comp2, then comp1 is not an instance of engineering connection and comp2 is not an instance of engineering connection.
(=>
(connectedEngineeringComponents ?COMP1 ?COMP2)
(not
(or
(instance ?COMP1 EngineeringConnection)
(instance ?COMP2 EngineeringConnection))))
If obj1 is attr1 to obj2 and is opposed to ? and attr1 is a member of "()" and attr2 is a member of "()" and attr1 is not equal to attr2, then obj1 is not attr2 to obj2.
(=>
(and
(orientation ?OBJ1 ?OBJ2 ?ATTR1)
(contraryAttribute @ROW)
(inList
?ATTR1
(ListFn @ROW))
(inList
?ATTR2
(ListFn @ROW))
(not
(equal ?ATTR1 ?ATTR2)))
(not
(orientation ?OBJ1 ?OBJ2 ?ATTR2)))
If obj1 is attr1 to obj2 and attr1 is an instance of directional attribute and attr2 is an instance of directional attribute and attr1 is not equal to attr2, then obj1 is not attr2 to obj2.
(=>
(and
(orientation ?OBJ1 ?OBJ2 ?ATTR1)
(instance ?ATTR1 DirectionalAttribute)
(instance ?ATTR2 DirectionalAttribute)
(not
(equal ?ATTR1 ?ATTR2)))
(not
(orientation ?OBJ1 ?OBJ2 ?ATTR2)))
If obj1 is above to obj2, then obj1 is not connected to obj2.
(=>
(orientation ?OBJ1 ?OBJ2 Above)
(not
(connected ?OBJ1 ?OBJ2)))
If obj1 is near to obj2, then obj1 is not connected to obj2.
(=>
(orientation ?OBJ1 ?OBJ2 Near)
(not
(connected ?OBJ1 ?OBJ2)))
If obj1 is on to obj2, then obj2 is not on to obj1.
(=>
(orientation ?OBJ1 ?OBJ2 On)
(not
(orientation ?OBJ2 ?OBJ1 On)))
For all org holds: org doesn't employ person and person is an instance of human if and only if unemployed is an attribute of person.
(<=>
(forall
(?ORG)
(and
(not
(employs ?ORG ?PERSON))
(instance ?PERSON Human)))
(attribute ?PERSON Unemployed))
The statement formula has the model force of necessity if and only if the statement "formula" has the model force of possibility.
(<=>
(modalAttribute ?FORMULA Necessity)
(not
(modalAttribute
(not ?FORMULA)
Possibility)))
The statement formula has the model force of obligation if and only if the statement "formula" has the model force of permission.
(<=>
(modalAttribute ?FORMULA Obligation)
(not
(modalAttribute
(not ?FORMULA)
Permission)))
If polychromatic is an attribute of obj, then there exist part1,part2,color attribute color1,color attribute color2 so that part1 is a superficial part of obj and part2 is a superficial part of obj and color1 is an attribute of part1 and color2 is an attribute of part2 and color1 is not equal to color2.
(=>
(attribute ?OBJ Polychromatic)
(exists
(?PART1 ?PART2 ?COLOR1 ?COLOR2)
(and
(superficialPart ?PART1 ?OBJ)
(superficialPart ?PART2 ?OBJ)
(attribute ?PART1 ?COLOR1)
(attribute ?PART2 ?COLOR2)
(instance ?COLOR1 ColorAttribute)
(instance ?COLOR2 ColorAttribute)
(not
(equal ?COLOR1 ?COLOR2)))))
If dry is an attribute of obj, then there doesn't exist subobj so that subobj is a part of obj and liquid is an attribute of subobj.
(=>
(attribute ?OBJ Dry)
(not
(exists
(?SUBOBJ)
(and
(part ?SUBOBJ ?OBJ)
(attribute ?SUBOBJ Liquid)))))
If unbreakable is an attribute of obj, then there doesn't exist damaging damage so that obj is a patient of damage.
(=>
(attribute ?OBJ Unbreakable)
(not
(exists
(?DAMAGE)
(and
(instance ?DAMAGE Damaging)
(patient ?DAMAGE ?OBJ)))))
If embryonic is an attribute of org during time, then there doesn't exist birth birth so that org experiences birth during time.
(=>
(holdsDuring
?TIME
(attribute ?ORG Embryonic))
(holdsDuring
?TIME
(not
(exists
(?BIRTH)
(and
(instance ?BIRTH Birth)
(experiencer ?BIRTH ?ORG))))))
entity is an instance of "the complement of class" if and only if entity is not an instance of class.
(<=>
(instance
?ENTITY
(ComplementFn ?CLASS))
(not
(instance ?ENTITY ?CLASS)))
