;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Parallel Buttons and Lights
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Components
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (role robot1)
  (role robot2)
  (role robot3)

  (<= (base (p ?k)) (index ?k))
  (<= (base (q ?k)) (index ?k))
  (<= (base (r ?k)) (index ?k))
  (<= (base (step ?k 1)) (index ?k))
  (<= (base (step ?k 2)) (index ?k))
  (<= (base (step ?k 3)) (index ?k))
  (<= (base (step ?k 4)) (index ?k))
  (<= (base (step ?k 5)) (index ?k))
  (<= (base (step ?k 6)) (index ?k))
  (<= (base (step ?k 7)) (index ?k))

  (<= (input robot1 (a ?k)) (index ?k))
  (<= (input robot1 (b ?k)) (index ?k))
  (<= (input robot1 (c ?k)) (index ?k))
  (<= (input robot2 (a ?k)) (index ?k))
  (<= (input robot2 (b ?k)) (index ?k))
  (<= (input robot2 (c ?k)) (index ?k))
  (<= (input robot3 (a ?k)) (index ?k))
  (<= (input robot3 (b ?k)) (index ?k))
  (<= (input robot3 (c ?k)) (index ?k))

  (index 1)
  (index 2)
  (index 3)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; init
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(init (step 1 1))
(init (step 2 1))
(init (step 3 1))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; legal
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(legal robot1 (a 1))
(legal robot1 (b 1))
(legal robot1 (c 1))
(legal robot2 (a 2))
(legal robot2 (b 2))
(legal robot2 (c 2))
(legal robot3 (a 3))
(legal robot3 (b 3))
(legal robot3 (c 3))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; next
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(<= (next (p 1)) (does robot1 (a 1)) (not (true (p 1))))
(<= (next (p 1)) (does robot1 (b 1)) (true (q 1)))
(<= (next (p 1)) (true (p 1)) (not (does robot1 (a 1))) (not (does robot1 (b 1))))

(<= (next (q 1)) (does robot1 (b 1)) (true (p 1)))
(<= (next (q 1)) (does robot1 (c 1)) (true (r 1)))
(<= (next (q 1)) (true (q 1)) (not (does robot1 (b 1))) (not (does robot1 (c 1))))
(<= (next (r 1)) (does robot1 (c 1)) (true (q 1)))
(<= (next (r 1)) (true (r 1)) (not (does robot1 (c 1))))
(<= (next (p 2)) (does robot2 (a 2)) (not (true (p 2))))
(<= (next (p 2)) (does robot2 (b 2)) (true (q 2)))
(<= (next (p 2)) (true (p 2)) (not (does robot2 (a 2))) (not (does robot2 (b 2))))
(<= (next (q 2)) (does robot2 (b 2)) (true (p 2)))
(<= (next (q 2)) (does robot2 (c 2)) (true (r 2)))
(<= (next (q 2)) (true (q 2)) (not (does robot2 (b 2))) (not (does robot2 (c 2))))
(<= (next (r 2)) (does robot2 (c 2)) (true (q 2)))
(<= (next (r 2)) (true (r 2)) (not (does robot2 (c 2))))
(<= (next (p 3)) (does robot3 (a 3)) (not (true (p 3))))
(<= (next (p 3)) (does robot3 (b 3)) (true (q 3)))
(<= (next (p 3)) (true (p 3)) (not (does robot3 (a 3))) (not (does robot3 (b 3))))
(<= (next (q 3)) (does robot3 (b 3)) (true (p 3)))
(<= (next (q 3)) (does robot3 (c 3)) (true (r 3)))
(<= (next (q 3)) (true (q 3)) (not (does robot3 (b 3))) (not (does robot3 (c 3))))
(<= (next (r 3)) (does robot3 (c 3)) (true (q 3)))
(<= (next (r 3)) (true (r 3)) (not (does robot3 (c 3))))

(<= (next (step 1 2)) (does robot1 (a 1)) (true (step 1 1)))
(<= (next (step 1 3)) (does robot1 (a 1)) (true (step 1 2)))
(<= (next (step 1 4)) (does robot1 (a 1)) (true (step 1 3)))
(<= (next (step 1 5)) (does robot1 (a 1)) (true (step 1 4)))
(<= (next (step 1 6)) (does robot1 (a 1)) (true (step 1 5)))
(<= (next (step 1 7)) (does robot1 (a 1)) (true (step 1 6)))
(<= (next (step 1 2)) (does robot1 (b 1)) (true (step 1 1)))
(<= (next (step 1 3)) (does robot1 (b 1)) (true (step 1 2)))
(<= (next (step 1 4)) (does robot1 (b 1)) (true (step 1 3)))
(<= (next (step 1 5)) (does robot1 (b 1)) (true (step 1 4)))
(<= (next (step 1 6)) (does robot1 (b 1)) (true (step 1 5)))
(<= (next (step 1 7)) (does robot1 (b 1)) (true (step 1 6)))
(<= (next (step 1 2)) (does robot1 (c 1)) (true (step 1 1)))
(<= (next (step 1 3)) (does robot1 (c 1)) (true (step 1 2)))
(<= (next (step 1 4)) (does robot1 (c 1)) (true (step 1 3)))
(<= (next (step 1 5)) (does robot1 (c 1)) (true (step 1 4)))
(<= (next (step 1 6)) (does robot1 (c 1)) (true (step 1 5)))
(<= (next (step 1 7)) (does robot1 (c 1)) (true (step 1 6)))

(<= (next (step 2 2)) (does robot1 (a 1)) (true (step 2 1)))
(<= (next (step 2 3)) (does robot1 (a 1)) (true (step 2 2)))
(<= (next (step 2 4)) (does robot1 (a 1)) (true (step 2 3)))
(<= (next (step 2 5)) (does robot1 (a 1)) (true (step 2 4)))
(<= (next (step 2 6)) (does robot1 (a 1)) (true (step 2 5)))
(<= (next (step 2 7)) (does robot1 (a 1)) (true (step 2 6)))
(<= (next (step 2 2)) (does robot1 (b 1)) (true (step 2 1)))
(<= (next (step 2 3)) (does robot1 (b 1)) (true (step 2 2)))
(<= (next (step 2 4)) (does robot1 (b 1)) (true (step 2 3)))
(<= (next (step 2 5)) (does robot1 (b 1)) (true (step 2 4)))
(<= (next (step 2 6)) (does robot1 (b 1)) (true (step 2 5)))
(<= (next (step 2 7)) (does robot1 (b 1)) (true (step 2 6)))
(<= (next (step 2 2)) (does robot1 (c 1)) (true (step 2 1)))
(<= (next (step 2 3)) (does robot1 (c 1)) (true (step 2 2)))
(<= (next (step 2 4)) (does robot1 (c 1)) (true (step 2 3)))
(<= (next (step 2 5)) (does robot1 (c 1)) (true (step 2 4)))
(<= (next (step 2 6)) (does robot1 (c 1)) (true (step 2 5)))
(<= (next (step 2 7)) (does robot1 (c 1)) (true (step 2 6)))

(<= (next (step 3 2)) (does robot1 (a 1)) (true (step 3 1)))
(<= (next (step 3 3)) (does robot1 (a 1)) (true (step 3 2)))
(<= (next (step 3 4)) (does robot1 (a 1)) (true (step 3 3)))
(<= (next (step 3 5)) (does robot1 (a 1)) (true (step 3 4)))
(<= (next (step 3 6)) (does robot1 (a 1)) (true (step 3 5)))
(<= (next (step 3 7)) (does robot1 (a 1)) (true (step 3 6)))
(<= (next (step 3 2)) (does robot1 (b 1)) (true (step 3 1)))
(<= (next (step 3 3)) (does robot1 (b 1)) (true (step 3 2)))
(<= (next (step 3 4)) (does robot1 (b 1)) (true (step 3 3)))
(<= (next (step 3 5)) (does robot1 (b 1)) (true (step 3 4)))
(<= (next (step 3 6)) (does robot1 (b 1)) (true (step 3 5)))
(<= (next (step 3 7)) (does robot1 (b 1)) (true (step 3 6)))
(<= (next (step 3 2)) (does robot1 (c 1)) (true (step 3 1)))
(<= (next (step 3 3)) (does robot1 (c 1)) (true (step 3 2)))
(<= (next (step 3 4)) (does robot1 (c 1)) (true (step 3 3)))
(<= (next (step 3 5)) (does robot1 (c 1)) (true (step 3 4)))
(<= (next (step 3 6)) (does robot1 (c 1)) (true (step 3 5)))
(<= (next (step 3 7)) (does robot1 (c 1)) (true (step 3 6)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; goal
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(<= (goal robot1 100) (row 1))
(<= (goal robot2 100) (row 2))
(<= (goal robot3 100) (row 3))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; terminal
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(<= terminal (terminal 1) (terminal 2) (terminal 3))
(<= (terminal 1) (row 1))
(<= (terminal 1) (true (step 1 7)))
(<= (terminal 2) (row 2))
(<= (terminal 2) (true (step 2 7)))
(<= (terminal 3) (row 3))
(<= (terminal 3) (true (step 3 7)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Miscellaneous
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(<= (row 1) (true (p 1)) (true (q 1)) (true (r 1)))
(<= (row 2) (true (p 2)) (true (q 2)) (true (r 2)))
(<= (row 3) (true (p 3)) (true (q 3)) (true (r 3)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;