( ! [V__NODE2,V__NODE1,V__GRAPH] :
((s__instance(V__GRAPH,s__Graph) &
s__instance(V__NODE1,s__GraphNode) &
s__instance(V__NODE2,s__GraphNode) &
s__graphPart(V__NODE1,V__GRAPH)
&
s__graphPart(V__NODE2,V__GRAPH)
&
~((V__NODE1 = V__NODE2)))
=>
( ? [V__ARC, V__PATH] :
((s__instance(V__ARC,s__GraphArc) &
(s__links(V__NODE1,V__NODE2,V__ARC)

(s__subGraph(V__PATH,V__GRAPH)
&
s__instance(V__PATH,s__GraphPath) &
(((s__BeginNodeFn(V__PATH)
= V__NODE1)
&
(s__EndNodeFn(V__PATH)
= V__NODE2))

((s__BeginNodeFn(V__PATH)
= V__NODE2)
&
(s__EndNodeFn(V__PATH)
= V__NODE1))))))))
)
)

Merge.kif 53035323 

( ! [V__GRAPH] :
(s__instance(V__GRAPH,s__Graph) =>
( ? [V__NODE1, V__NODE2, V__NODE3, V__ARC1, V__ARC2] :
((s__instance(V__NODE1,s__GraphNode) &
s__instance(V__NODE2,s__GraphNode) &
s__instance(V__NODE3,s__GraphNode) &
s__instance(V__ARC1,s__GraphArc) &
s__instance(V__ARC2,s__GraphArc) &
(s__graphPart(V__NODE1,V__GRAPH)
&
s__graphPart(V__NODE2,V__GRAPH)
&
s__graphPart(V__NODE3,V__GRAPH)
&
s__graphPart(V__ARC1,V__GRAPH)
&
s__graphPart(V__ARC2,V__GRAPH)
&
s__links(V__NODE1,V__NODE2,V__ARC1)
&
s__links(V__NODE2,V__NODE3,V__ARC2)
&
~((V__NODE1 = V__NODE2))
&
~((V__NODE2 = V__NODE3))
&
~((V__NODE1 = V__NODE3))
&
~((V__ARC1 = V__ARC2))))))
)
)

Merge.kif 53255339 
