GM10d

Premises:

; Graph of Exercise 2.1

; R represents directed arcs in the graph
;  (R q r) denotes an arc directed from 'q' to 'r'

; The vertex out-order is not greater than 1
;  (successors are unique to their predecessor)
(forall (?X ?Y ?Z)
 (=>
  (and (R ?X ?Y) (R ?X ?Z))
  (= ?Y ?Z)))

; The vertex in-order is not greater than 1
;  (predecessors are unique to their successor)
(forall (?X ?Y ?Z)
 (=>
  (and (R ?Y ?X) (R ?Z ?X))
  (= ?Y ?Z)))

; R is anti-reflexive
(forall ?X
 (not (R ?X ?X)))

; Arcs in the graph
;  The graph is a cyclic connection of four vertices:
;   'a', 'b', 'c' and 'd'
(R a b)
(R b c)
(R c d)
(R d a)

; P represents a colored or marked vertex in the graph
(P a)
(P b)
(not (P c))
(not (P d))

; Each vertex name denotes a distinct vertex in the graph
(not (= a b))
(not (= a c))
(not (= a d))
(not (= b c))
(not (= b d))
(not (= c d))

; Definition of a function, MURev, mapping
; connected pairs of dissimilarly marked
; vertices to each other:
(forall (?Node ?Rev)
 (<=>
  (= (MURev ?Node) ?Rev)
  (or
    (and
     (P ?Node)
     (not (P ?Rev))
     (or
      (R ?Node ?Rev)
      (R ?Rev ?Node)))
    (and
     (not (P ?Node))
     (P ?Rev)
     (or
      (R ?Node ?Rev)
      (R ?Rev ?Node))))))

GM10d

Premises:

Conclusion: