(comment "CPSA 2.3.4")
(comment "All input read from wonthull3.scm")

(defprotocol wonthull3 basic
  (defrole init
    (vars (a name) (x1 x2 x3 x4 text))
    (trace (send (enc x3 (pubk a)))
      (send (cat (enc x1 x2 (pubk a)) (enc x3 x2 (pubk a))))
      (recv (enc "okay" x3 x4 (pubk a))))
    (non-orig (privk a))
    (uniq-orig x3))
  (defrole resp
    (vars (a name) (y1 y2 y3 text))
    (trace (recv (enc y1 y2 (pubk a)))
      (send (enc "okay" y3 y1 (pubk a))))))

(defskeleton wonthull3
  (vars (x1 x2 x3 x4 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x2) (x3 x3) (x4 x4) (a a))
  (non-orig (privk a))
  (uniq-orig x3)
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x2 (pubk a)) (enc x3 x2 (pubk a))))
      (recv (enc "okay" x3 x4 (pubk a)))))
  (label 0)
  (unrealized (0 2))
  (origs (x3 (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x2 x4 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x2) (x3 x2) (x4 x4) (a a))
  (non-orig (privk a))
  (uniq-orig x2)
  (operation nonce-test (displaced 1 0 init 2) x3 (0 2)
    (enc x3 (pubk a)) (enc x3 x2 (pubk a)))
  (traces
    ((send (enc x2 (pubk a)))
      (send (cat (enc x1 x2 (pubk a)) (enc x2 x2 (pubk a))))
      (recv (enc "okay" x2 x4 (pubk a)))))
  (label 1)
  (parent 0)
  (unrealized (0 2))
  (origs (x2 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x2 x3 x4 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x2) (x3 x3) (x4 x4) (a a))
  (defstrand resp 2 (y1 x3) (y2 x2) (y3 y3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand resp 2) x3 (0 2) (enc x3 (pubk a))
    (enc x3 x2 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x2 (pubk a)) (enc x3 x2 (pubk a))))
      (recv (enc "okay" x3 x4 (pubk a))))
    ((recv (enc x3 x2 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 2)
  (parent 0)
  (unrealized (0 2) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x2 x4 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x2) (x3 x2) (x4 x4) (a a))
  (defstrand resp 2 (y1 x2) (y2 x2) (y3 y3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x2)
  (operation nonce-test (added-strand resp 2) x2 (0 2) (enc x2 (pubk a))
    (enc x1 x2 (pubk a)) (enc x2 x2 (pubk a)))
  (traces
    ((send (enc x2 (pubk a)))
      (send (cat (enc x1 x2 (pubk a)) (enc x2 x2 (pubk a))))
      (recv (enc "okay" x2 x4 (pubk a))))
    ((recv (enc x2 x2 (pubk a))) (send (enc "okay" y3 x2 (pubk a)))))
  (label 3)
  (parent 1)
  (unrealized (0 2) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x2 x3 x4 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x2) (x3 x3) (x4 x4) (a a))
  (defstrand resp 2 (y1 x3) (y2 x2) (y3 y3) (a a))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 2 0 init 2) x3 (1 0)
    (enc x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x2 (pubk a)) (enc x3 x2 (pubk a))))
      (recv (enc "okay" x3 x4 (pubk a))))
    ((recv (enc x3 x2 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 4)
  (parent 2)
  (seen 5)
  (unrealized (0 2))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x2 x4 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x2) (x3 x2) (x4 x4) (a a))
  (defstrand resp 2 (y1 x2) (y2 x2) (y3 y3) (a a))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x2)
  (operation nonce-test (displaced 2 0 init 2) x2 (1 0)
    (enc x2 (pubk a)))
  (traces
    ((send (enc x2 (pubk a)))
      (send (cat (enc x1 x2 (pubk a)) (enc x2 x2 (pubk a))))
      (recv (enc "okay" x2 x4 (pubk a))))
    ((recv (enc x2 x2 (pubk a))) (send (enc "okay" y3 x2 (pubk a)))))
  (label 5)
  (parent 3)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x2 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x2) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x2) (y3 y3) (a a))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (x3 y3) (x4 y3)) y3 (0 2)
    (enc y3 (pubk a)) (enc "okay" y3 y3 (pubk a)) (enc y3 x2 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x2 (pubk a)) (enc y3 x2 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x2 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 6)
  (parent 4)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (x1 x1) (x2 x2) (x3 y3) (x4 y3))))
  (origs (y3 (0 0))))

(defskeleton wonthull3
  (vars (x1 x2 x3 x4 y3 y3-0 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x2) (x3 x3) (x4 x4) (a a))
  (defstrand resp 2 (y1 x3) (y2 x2) (y3 y3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x2) (y3 y3-0) (a a))
  (precedes ((0 0) (2 0)) ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand resp 2) x3 (0 2) (enc x3 (pubk a))
    (enc "okay" y3 x3 (pubk a)) (enc x3 x2 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x2 (pubk a)) (enc x3 x2 (pubk a))))
      (recv (enc "okay" x3 x4 (pubk a))))
    ((recv (enc x3 x2 (pubk a))) (send (enc "okay" y3 x3 (pubk a))))
    ((recv (enc x3 x2 (pubk a))) (send (enc "okay" y3-0 x3 (pubk a)))))
  (label 7)
  (parent 4)
  (seen 4)
  (unrealized (0 2) (2 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 y3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (a a))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (x2 y3) (x4 y3)) y3 (0 2)
    (enc y3 (pubk a)) (enc "okay" y3 y3 (pubk a)) (enc x1 y3 (pubk a))
    (enc y3 y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 y3 (pubk a)) (enc y3 y3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 8)
  (parent 5)
  (seen 6)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x2 x4 y3 y3-0 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x2) (x3 x2) (x4 x4) (a a))
  (defstrand resp 2 (y1 x2) (y2 x2) (y3 y3) (a a))
  (defstrand resp 2 (y1 x2) (y2 x2) (y3 y3-0) (a a))
  (precedes ((0 0) (2 0)) ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x2)
  (operation nonce-test (added-strand resp 2) x2 (0 2) (enc x2 (pubk a))
    (enc "okay" y3 x2 (pubk a)) (enc x1 x2 (pubk a))
    (enc x2 x2 (pubk a)))
  (traces
    ((send (enc x2 (pubk a)))
      (send (cat (enc x1 x2 (pubk a)) (enc x2 x2 (pubk a))))
      (recv (enc "okay" x2 x4 (pubk a))))
    ((recv (enc x2 x2 (pubk a))) (send (enc "okay" y3 x2 (pubk a))))
    ((recv (enc x2 x2 (pubk a))) (send (enc "okay" y3-0 x2 (pubk a)))))
  (label 9)
  (parent 5)
  (seen 5)
  (unrealized (0 2) (2 0))
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")

(defprotocol wonthull3 basic
  (defrole init
    (vars (a name) (x1 x2 x3 x4 text))
    (trace (send (enc x3 (pubk a)))
      (send (cat (enc x1 x2 (pubk a)) (enc x3 x2 (pubk a))))
      (recv (enc "okay" x3 x4 (pubk a))))
    (non-orig (privk a))
    (uniq-orig x3))
  (defrole resp
    (vars (a name) (y1 y2 y3 text))
    (trace (recv (enc y1 y2 (pubk a)))
      (send (enc "okay" y3 y1 (pubk a))))))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 x3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x3-0) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3-0)
  (traces
    ((send (enc x3-0 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x3-0 x3 (pubk a))))
      (recv (enc "okay" x3-0 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0)))
      (send (enc "okay" x3 x1 (pubk a-0)))))
  (label 10)
  (unrealized (0 2))
  (origs (x3-0 (0 0)))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 2 1 resp 2) x3-0 (0 2)
    (enc x3-0 (pubk a)) (enc x3-0 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0)))
      (send (enc "okay" x3 x1 (pubk a-0)))))
  (label 11)
  (parent 10)
  (unrealized (1 0))
  (origs (x3 (0 0)))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 text) (a name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (displaced 2 1 resp 2) x3-0 (0 2)
    (enc x3-0 (pubk a-0)) (enc x3-0 x3 (pubk a-0)))
  (traces
    ((send (enc x1 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x1 x3 (pubk a))))
      (recv (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x3 x1 (pubk a)))))
  (label 12)
  (parent 10)
  (seen 14)
  (unrealized (0 2))
  (origs (x1 (0 0)))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 x3-0 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x3-0) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3-0) (y2 x3) (y3 y3) (a a))
  (precedes ((0 0) (2 0)) ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3-0)
  (operation nonce-test (added-strand resp 2) x3-0 (0 2)
    (enc x3-0 (pubk a)) (enc x3-0 x3 (pubk a)))
  (traces
    ((send (enc x3-0 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x3-0 x3 (pubk a))))
      (recv (enc "okay" x3-0 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x3-0 x3 (pubk a)))
      (send (enc "okay" y3 x3-0 (pubk a)))))
  (label 13)
  (parent 10)
  (unrealized (0 2) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (x1-0 x3) (a-0 a)) x3 (1 0)
    (enc x3 (pubk a)) (enc x3 x3 (pubk a)) (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a)))))
  (label 14)
  (parent 11)
  (unrealized)
  (shape)
  (maps ((0 1) ((x1 x3) (x3 x3) (a a) (x1-0 x1) (x3-0 x3) (a-0 a))))
  (origs (x3 (0 0))))

(defskeleton wonthull3
  (vars (x3 x1 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (x1-0 x1) (a-0 a)) x3 (1 0)
    (enc x3 (pubk a)) (enc x3 x3 (pubk a)) (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x3 x1 (pubk a)))))
  (label 15)
  (parent 11)
  (unrealized)
  (shape)
  (maps ((0 1) ((x1 x1) (x3 x3) (a a) (x1-0 x1) (x3-0 x3) (a-0 a))))
  (origs (x3 (0 0))))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 0) (2 0)) ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand resp 2) x3 (1 0) (enc x3 (pubk a))
    (enc x3 x3 (pubk a)) (enc x1-0 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 16)
  (parent 11)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 y3 text) (a name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 y3) (a a))
  (precedes ((0 0) (2 0)) ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (0 2) (enc x1 (pubk a))
    (enc "okay" x3 x1 (pubk a)) (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x1 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x1 x3 (pubk a))))
      (recv (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3 x1 (pubk a)))))
  (label 17)
  (parent 12)
  (unrealized (0 2) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 x3-0 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x3-0) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3-0) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3-0)
  (operation nonce-test (displaced 3 0 init 2) x3-0 (2 0)
    (enc x3-0 (pubk a)))
  (traces
    ((send (enc x3-0 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x3-0 x3 (pubk a))))
      (recv (enc "okay" x3-0 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x3-0 x3 (pubk a)))
      (send (enc "okay" y3 x3-0 (pubk a)))))
  (label 18)
  (parent 13)
  (seen 20)
  (unrealized (0 2))
  (comment "4 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 3 0 init 2) x3 (2 0)
    (enc x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 19)
  (parent 16)
  (unrealized (1 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 y3 text) (a name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (displaced 3 0 init 2) x1 (2 0)
    (enc x1 (pubk a)))
  (traces
    ((send (enc x1 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x1 x3 (pubk a))))
      (recv (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3 x1 (pubk a)))))
  (label 20)
  (parent 17)
  (unrealized (0 2))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (x1-0 y3) (x3-0 y3)) y3 (0 2)
    (enc y3 (pubk a)) (enc "okay" y3 y3 (pubk a)) (enc y3 x3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a-0))) (send (enc "okay" x3 y3 (pubk a-0))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 21)
  (parent 18)
  (seen 28)
  (unrealized (1 0))
  (comment "4 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 3 1 resp 2) x3-0 (0 2)
    (enc x3-0 (pubk a)) (enc "okay" y3 x3-0 (pubk a))
    (enc x3-0 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 22)
  (parent 18)
  (seen 19 27)
  (unrealized (1 0))
  (comment "4 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 x3-0 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x3-0) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3-0) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x3-0) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 0) (3 0)) ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3-0)
  (operation nonce-test (added-strand resp 2) x3-0 (0 2)
    (enc x3-0 (pubk a)) (enc "okay" y3 x3-0 (pubk a))
    (enc x3-0 x3 (pubk a)))
  (traces
    ((send (enc x3-0 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x3-0 x3 (pubk a))))
      (recv (enc "okay" x3-0 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x3-0 x3 (pubk a))) (send (enc "okay" y3 x3-0 (pubk a))))
    ((recv (enc x3-0 x3 (pubk a)))
      (send (enc "okay" y3-0 x3-0 (pubk a)))))
  (label 23)
  (parent 18)
  (seen 18)
  (unrealized (0 2) (3 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (x1-0 x3) (a-0 a)) x3 (1 0)
    (enc x3 (pubk a)) (enc "okay" y3 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 24)
  (parent 19)
  (seen 14)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (x1-0 x1) (a-0 a)) x3 (1 0)
    (enc x3 (pubk a)) (enc "okay" y3 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 25)
  (parent 19)
  (seen 15)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 0) (3 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand resp 2) x3 (1 0) (enc x3 (pubk a))
    (enc "okay" y3 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1-0 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3-0 x3 (pubk a)))))
  (label 26)
  (parent 19)
  (seen 19)
  (unrealized (1 0) (3 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 3 1 resp 2) x1-0 (0 2)
    (enc x1-0 (pubk a)) (enc "okay" x3 x1-0 (pubk a))
    (enc "okay" y3 x1-0 (pubk a)) (enc x1-0 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 27)
  (parent 20)
  (seen 14)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 3 2 resp 2) x1-0 (0 2)
    (enc x1-0 (pubk a)) (enc "okay" x3 x1-0 (pubk a))
    (enc "okay" y3 x1-0 (pubk a)) (enc x1-0 x3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" x3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 28)
  (parent 20)
  (unrealized)
  (shape)
  (maps ((0 1) ((x1 y3) (x3 x3) (a a) (x1-0 x1) (x3-0 y3) (a-0 a))))
  (origs (y3 (0 0))))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 y3 y3-0 text) (a name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 0) (3 0)) ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (0 2) (enc x1 (pubk a))
    (enc "okay" x3 x1 (pubk a)) (enc "okay" y3 x1 (pubk a))
    (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x1 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x1 x3 (pubk a))))
      (recv (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 29)
  (parent 20)
  (seen 20)
  (unrealized (0 2) (3 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (precedes ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 3 0 init 2) y3 (1 0)
    (enc y3 (pubk a)) (enc y3 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a-0))) (send (enc "okay" x3 x3 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a)))))
  (label 30)
  (parent 21)
  (unrealized (1 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 3 2 resp 2) y3 (1 0)
    (enc y3 (pubk a)) (enc y3 x3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a-0))) (send (enc "okay" x3 y3 (pubk a-0))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 31)
  (parent 21)
  (seen 36)
  (unrealized (1 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 0) (3 0)) ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (added-strand resp 2) y3 (1 0) (enc y3 (pubk a))
    (enc y3 x3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a-0))) (send (enc "okay" x3 y3 (pubk a-0))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 32)
  (parent 21)
  (unrealized (1 0) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (x1-0 x1) (a-0 a)) x3 (1 0)
    (enc x3 (pubk a)) (enc x3 x3 (pubk a)) (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 33)
  (parent 22)
  (seen 15)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 0) (3 0)) ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand resp 2) x3 (1 0) (enc x3 (pubk a))
    (enc x3 x3 (pubk a)) (enc x1-0 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3-0 x3 (pubk a)))))
  (label 34)
  (parent 22)
  (unrealized (1 0) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (precedes ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (a-0 a)) x3 (1 0) (enc x3 (pubk a))
    (enc x3 x3 (pubk a)) (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a)))))
  (label 35)
  (parent 30)
  (seen 14)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 3 2 resp 2) x3 (1 0)
    (enc x3 (pubk a)) (enc x3 x3 (pubk a)) (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a-0))) (send (enc "okay" x3 x3 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a)))))
  (label 36)
  (parent 30)
  (unrealized (1 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 0) (3 0)) ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand resp 2) x3 (1 0) (enc x3 (pubk a))
    (enc x3 x3 (pubk a)) (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a-0))) (send (enc "okay" x3 x3 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 37)
  (parent 30)
  (unrealized (1 0) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (a-0 a)) y3 (1 0) (enc y3 (pubk a))
    (enc "okay" y3 y3 (pubk a)) (enc y3 x3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" x3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 38)
  (parent 31)
  (seen 28)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 0) (3 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (added-strand resp 2) y3 (1 0) (enc y3 (pubk a))
    (enc "okay" y3 y3 (pubk a)) (enc y3 x3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a-0))) (send (enc "okay" x3 y3 (pubk a-0))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 39)
  (parent 31)
  (unrealized (1 0) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (0 2))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 4 0 init 2) y3 (3 0)
    (enc y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a-0))) (send (enc "okay" x3 y3 (pubk a-0))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 40)
  (parent 32)
  (seen 44 45)
  (unrealized (1 0))
  (comment "4 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (0 2))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 4 0 init 2) x3 (3 0)
    (enc x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3-0 x3 (pubk a)))))
  (label 41)
  (parent 34)
  (unrealized (1 0))
  (comment "4 in cohort - 4 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (a-0 a)) x3 (1 0) (enc x3 (pubk a))
    (enc "okay" x3 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a)))))
  (label 42)
  (parent 36)
  (seen 14)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 0) (3 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand resp 2) x3 (1 0) (enc x3 (pubk a))
    (enc "okay" x3 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a-0))) (send (enc "okay" x3 x3 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 43)
  (parent 36)
  (unrealized (1 0) (3 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (0 2))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 4 0 init 2) x3 (3 0)
    (enc x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a-0))) (send (enc "okay" x3 x3 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 44)
  (parent 37)
  (seen 52)
  (unrealized (1 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 4 0 init 2) y3 (3 0)
    (enc y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a-0))) (send (enc "okay" x3 y3 (pubk a-0))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 45)
  (parent 39)
  (seen 36)
  (unrealized (1 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 y3-0 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (0 2))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (a-0 a)) y3 (1 0) (enc y3 (pubk a))
    (enc "okay" y3-0 y3 (pubk a)) (enc y3 x3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" x3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 46)
  (parent 40)
  (seen 28)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 y3-0 y3-1 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-1) (a a))
  (precedes ((0 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (added-strand resp 2) y3 (1 0) (enc y3 (pubk a))
    (enc "okay" y3-0 y3 (pubk a)) (enc y3 x3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a-0))) (send (enc "okay" x3 y3 (pubk a-0))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-1 y3 (pubk a)))))
  (label 47)
  (parent 40)
  (seen 40)
  (unrealized (1 0) (4 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 y3-0 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (0 2))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (x1-0 x3) (a-0 a)) x3 (1 0)
    (enc x3 (pubk a)) (enc "okay" y3-0 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3-0 x3 (pubk a)))))
  (label 48)
  (parent 41)
  (seen 24)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 y3-0 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (0 2))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (x1-0 x1) (a-0 a)) x3 (1 0)
    (enc x3 (pubk a)) (enc "okay" y3-0 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3-0 x3 (pubk a)))))
  (label 49)
  (parent 41)
  (seen 25)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x1-0 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 y3) (x3 y3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 y3) (y3 y3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3-0) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 4 2 resp 2) x3 (1 0)
    (enc x3 (pubk a)) (enc "okay" y3-0 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1-0 x3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1-0 y3 (pubk a)) (enc y3 y3 (pubk a))))
      (recv (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 y3 (pubk a-0))) (send (enc "okay" y3 x1 (pubk a-0))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 50)
  (parent 41)
  (unrealized (1 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 y3 y3-0 y3-1 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3-1) (a a))
  (precedes ((0 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand resp 2) x3 (1 0) (enc x3 (pubk a))
    (enc "okay" y3-0 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1-0 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3-0 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3-1 x3 (pubk a)))))
  (label 51)
  (parent 41)
  (seen 41)
  (unrealized (1 0) (4 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 4 0 init 2) x3 (3 0)
    (enc x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a-0))) (send (enc "okay" x3 x3 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 52)
  (parent 43)
  (seen 58)
  (unrealized (1 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (0 2))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (a-0 a)) x3 (1 0) (enc x3 (pubk a))
    (enc "okay" y3 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 53)
  (parent 44)
  (seen 24)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand resp 2) x3 (1 0) (enc x3 (pubk a))
    (enc "okay" y3 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a-0))) (send (enc "okay" x3 x3 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3-0 x3 (pubk a)))))
  (label 54)
  (parent 44)
  (seen 44)
  (unrealized (1 0) (4 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 y3-0 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (a-0 a)) y3 (1 0) (enc y3 (pubk a))
    (enc "okay" y3 y3 (pubk a)) (enc "okay" y3-0 y3 (pubk a))
    (enc y3 x3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" x3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 55)
  (parent 45)
  (seen 38)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 y3-0 y3-1 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-1) (a a))
  (precedes ((0 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (1 0)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (added-strand resp 2) y3 (1 0) (enc y3 (pubk a))
    (enc "okay" y3 y3 (pubk a)) (enc "okay" y3-0 y3 (pubk a))
    (enc y3 x3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a-0))) (send (enc "okay" x3 y3 (pubk a-0))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-1 y3 (pubk a)))))
  (label 56)
  (parent 45)
  (seen 45)
  (unrealized (1 0) (4 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 y3-0 text) (a name))
  (defstrand init 3 (x1 x1) (x2 y3) (x3 y3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3-0) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (x1-0 x1) (a-0 a)) y3 (1 0)
    (enc y3 (pubk a)) (enc "okay" y3 y3 (pubk a))
    (enc "okay" y3-0 y3 (pubk a)) (enc x1 y3 (pubk a))
    (enc y3 y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 y3 (pubk a)) (enc y3 y3 (pubk a))))
      (recv (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 y3 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 57)
  (parent 50)
  (seen 25)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 y3-0 text) (a name))
  (defstrand init 3 (x1 x1) (x2 y3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3-0) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (x1-0 y3) (a-0 a)) y3 (1 0)
    (enc y3 (pubk a)) (enc "okay" y3 y3 (pubk a))
    (enc "okay" y3-0 y3 (pubk a)) (enc x1 y3 (pubk a))
    (enc y3 y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 y3 (pubk a)) (enc y3 y3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 58)
  (parent 50)
  (seen 24)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x1-0 y3 y3-0 y3-1 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 y3) (x3 y3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 y3) (y3 y3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3-1) (a a))
  (precedes ((0 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (1 0)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (added-strand resp 2) y3 (1 0) (enc y3 (pubk a))
    (enc "okay" y3 y3 (pubk a)) (enc "okay" y3-0 y3 (pubk a))
    (enc x1-0 y3 (pubk a)) (enc y3 y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1-0 y3 (pubk a)) (enc y3 y3 (pubk a))))
      (recv (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 y3 (pubk a-0))) (send (enc "okay" y3 x1 (pubk a-0))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3-1 y3 (pubk a)))))
  (label 59)
  (parent 50)
  (seen 50)
  (unrealized (1 0) (4 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (1 0)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand resp 2) x3 (1 0) (enc x3 (pubk a))
    (enc "okay" x3 x3 (pubk a)) (enc "okay" y3 x3 (pubk a))
    (enc x3 x3 (pubk a)) (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a-0))) (send (enc "okay" x3 x3 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3-0 x3 (pubk a)))))
  (label 60)
  (parent 52)
  (seen 52)
  (unrealized (1 0) (4 0))
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")