consequent

(=>     (and         (instance ?GRAPH DirectedGraph)         (instance ?ARC GraphArc)         (graphPart ?ARC ?GRAPH))     (exists (?NODE1 ?NODE2)         (and             (equal                 (InitialNodeFn ?ARC) ?NODE1)             (equal                 (TerminalNodeFn ?ARC) ?NODE2))))	Merge.kif 5795-5803	If X is an instance of directed graph, Y is an instance of graph arc, and Y is a part of X, then there exist Z, W such that equal the starting node of Y, Z, equal the terminal node of Y, and W
(=>     (instance ?GRAPH Tree)     (not         (exists (?ARC1 ?ARC2 ?NODE)             (and                 (graphPart ?ARC1 ?GRAPH)                 (graphPart ?ARC2 ?GRAPH)                 (graphPart ?NODE ?GRAPH)                 (equal                     (TerminalNodeFn ?ARC1) ?NODE)                 (equal                     (TerminalNodeFn ?ARC2) ?NODE)                 (not                     (equal ?ARC1 ?ARC2))))))	Merge.kif 5826-5836	If X is an instance of tree, then All of the following hold: (1) there don't exist Y, Z (2) W such that Y is a part of X (3) Z is a part of X (4) W is a part of X (5) equal the terminal node of Y (6) W (7) equal the terminal node of Z (8) W (9) equal Y (10) Z
(=>     (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))))))	Merge.kif 5859-5870	If X is an instance of graph path, Y is an instance of graph arc, Y is a part of X, and equal the terminal node of Y and Z, then there doesn't exist W such that equal the terminal node of W, Z, equal W, and Y

Show simplified definition (without tree view)
Show simplified definition (with tree view)