(comment "CPSA 2.1.2")
(comment "All input read")

(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)
  (seen 1)
  (unrealized (0 2))
  (comment "3 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 (added-strand init 2) x2 (0 2) (enc 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)))))
  (label 1)
  (parent 0)
  (unrealized (0 2))
  (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)
  (seen 4 5 6)
  (unrealized (0 2) (1 0))
  (comment "6 in cohort - 3 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)
  (seen 5 7)
  (unrealized (0 2) (1 0))
  (comment "6 in cohort - 1 not yet seen"))

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

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

(defskeleton wonthull3
  (vars (x2 y3 text) (a name))
  (defstrand init 3 (x1 y3) (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 (x1 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 y3 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 8)
  (parent 4)
  (seen 10)
  (unrealized)
  (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 9)
  (parent 5)
  (seen 10)
  (unrealized)
  (comment "1 in cohort - 0 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 10)
  (parent 6)
  (unrealized)
  (shape))

(defskeleton wonthull3
  (vars (y3 text) (a name))
  (defstrand init 3 (x1 y3) (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 (x1 y3) (x4 y3)) y3 (0 2)
    (enc y3 (pubk a)) (enc "okay" y3 y3 (pubk a)) (enc y3 y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc y3 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 11)
  (parent 7)
  (seen 9)
  (unrealized)
  (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 12)
  (seen 13)
  (unrealized (0 2))
  (comment "5 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 (added-strand init 2) x3 (0 2) (enc x3 (pubk a))
    (enc x3 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 13)
  (parent 12)
  (unrealized (1 0))
  (comment "3 in cohort - 3 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 14)
  (parent 12)
  (seen 19 20 21)
  (unrealized (0 2) (2 0))
  (comment "7 in cohort - 4 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 15)
  (parent 12)
  (seen 17)
  (unrealized (0 2))
  (comment "5 in cohort - 1 not yet seen"))

(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 16)
  (parent 13)
  (unrealized)
  (shape))

(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 17)
  (parent 13)
  (unrealized)
  (shape))

(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 18)
  (parent 13)
  (seen 24 25)
  (unrealized (1 0) (2 0))
  (comment "6 in cohort - 2 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 x1-0) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x1-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 x1-0)
  (operation nonce-test (added-strand init 2) x1-0 (2 0)
    (enc x1-0 (pubk a)))
  (traces
    ((send (enc x1-0 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x1-0 x3 (pubk a))))
      (recv (enc "okay" x1-0 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x1-0 x3 (pubk a)))
      (send (enc "okay" y3 x1-0 (pubk a)))))
  (label 19)
  (parent 14)
  (seen 27)
  (unrealized (0 2))
  (comment "5 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 (added-strand 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 20)
  (parent 14)
  (seen 25)
  (unrealized (1 0))
  (comment "5 in cohort - 4 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 (added-strand 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 21)
  (parent 14)
  (seen 20)
  (unrealized (0 2))
  (comment "5 in cohort - 2 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)) ((1 1) (2 0)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 3 1 resp 2) x3-0 (2 0)
    (enc x3-0 (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 14)
  (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 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 23)
  (parent 15)
  (seen 28 30 34 36)
  (unrealized (0 2) (2 0))
  (comment "7 in cohort - 0 not yet seen"))

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

(defskeleton wonthull3
  (vars (x3 y3 text) (a a-0 name))
  (defstrand init 3 (x1 y3) (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 y3) (x1-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 y3 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 26)
  (parent 19)
  (seen 43)
  (unrealized (1 0))
  (comment "4 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x3) (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 (added-strand init 2) x3 (0 2) (enc x3 (pubk a))
    (enc "okay" y3 x3 (pubk a)) (enc x3 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x3 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 27)
  (parent 19)
  (seen 24)
  (unrealized (1 0))
  (comment "4 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 y3 text) (a name))
  (defstrand init 3 (x1 x1) (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 1 resp 2) x1-0 (0 2)
    (enc x1-0 (pubk a-0)) (enc "okay" y3 x1-0 (pubk a-0))
    (enc x1-0 x3 (pubk a-0)))
  (traces
    ((send (enc x1 (pubk a)))
      (send (cat (enc x1 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 28)
  (parent 19)
  (seen 41 44)
  (unrealized (0 2))
  (comment "6 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) (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 29)
  (parent 20)
  (seen 16)
  (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 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 (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))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 30)
  (parent 20)
  (seen 17)
  (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 31)
  (parent 20)
  (seen 47 48)
  (unrealized (1 0) (3 0))
  (comment "7 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x1-0 y3 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))
  (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) x3 (1 0)
    (enc 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)))))
  (label 32)
  (parent 20)
  (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) (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 33)
  (parent 21)
  (seen 54 56)
  (unrealized (1 0))
  (comment "6 in cohort - 4 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 1 resp 2) x3-0 (0 2)
    (enc x3-0 (pubk a-0)) (enc "okay" y3 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))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3 x1 (pubk a)))))
  (label 34)
  (parent 21)
  (seen 30 53)
  (unrealized (0 2))
  (comment "6 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) (1 0)) ((1 1) (2 0)) ((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 35)
  (parent 22)
  (seen 16)
  (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 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)) ((1 1) (2 0)) ((2 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))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 36)
  (parent 22)
  (seen 17)
  (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)) ((1 1) (2 0)) ((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 37)
  (parent 22)
  (seen 57 58)
  (unrealized (1 0) (3 0))
  (comment "6 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x1) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3) (a a))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (contracted (x1-0 x1) (a-0 a)) x1 (1 0)
    (enc x1 (pubk a)) (enc "okay" y3 x1 (pubk a)) (enc x1 x1 (pubk a)))
  (traces
    ((send (enc x1 (pubk a)))
      (send (cat (enc x1 x1 (pubk a)) (enc x1 x1 (pubk a))))
      (recv (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a)))))
  (label 38)
  (parent 24)
  (unrealized)
  (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) (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 39)
  (parent 25)
  (seen 16)
  (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 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 40)
  (parent 25)
  (seen 17)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 y3 text) (a name))
  (defstrand init 3 (x1 y3) (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 (contracted (a-0 a)) y3 (1 0) (enc y3 (pubk a))
    (enc y3 x3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc y3 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 41)
  (parent 26)
  (seen 53)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 y3) (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 y3 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 42)
  (parent 26)
  (seen 60 61)
  (unrealized (1 0) (3 0))
  (comment "7 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x3 y3 text) (a a-0 name))
  (defstrand init 3 (x1 y3) (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 y3 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 43)
  (parent 26)
  (unrealized (1 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x3 y3 text) (a name))
  (defstrand init 3 (x1 x3) (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 (contracted (x1 x3) (a-0 a)) x3 (1 0)
    (enc x3 (pubk a)) (enc x3 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x3 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 44)
  (parent 27)
  (seen 59)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x3) (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)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x3 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 45)
  (parent 27)
  (seen 47)
  (unrealized (1 0) (3 0))
  (comment "7 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 name))
  (defstrand init 3 (x1 y3) (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))
  (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) x3 (1 0)
    (enc x3 (pubk a)) (enc x3 x3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc y3 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)))))
  (label 46)
  (parent 27)
  (unrealized (1 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x1-0 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x1-0) (x3 x1-0) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1-0) (y3 x1-0) (a a-0))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (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 x1-0)
  (operation nonce-test (added-strand init 2) x1-0 (3 0)
    (enc x1-0 (pubk a)))
  (traces
    ((send (enc x1-0 (pubk a)))
      (send (cat (enc x1-0 x1-0 (pubk a)) (enc x1-0 x1-0 (pubk a))))
      (recv (enc "okay" x1-0 x1 (pubk a))))
    ((recv (enc x1 x1-0 (pubk a-0)))
      (send (enc "okay" x1-0 x1 (pubk a-0))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3-0 x1-0 (pubk a)))))
  (label 47)
  (parent 31)
  (unrealized (1 0))
  (comment "3 in cohort - 3 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 (added-strand 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 48)
  (parent 31)
  (unrealized (1 0))
  (comment "4 in cohort - 4 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)) ((1 1) (0 2)) ((2 1) (3 0)) ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 4 2 resp 2) x3 (3 0)
    (enc 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 49)
  (parent 31)
  (unrealized (1 0))
  (comment "2 in cohort - 2 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))
  (defstrand resp 2 (y1 y3) (y2 y3) (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 (x1-0 y3) (a-0 a)) y3 (1 0)
    (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))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 50)
  (parent 32)
  (seen 17)
  (unrealized)
  (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 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))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 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 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)))))
  (label 51)
  (parent 32)
  (seen 16)
  (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 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 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)))))
  (label 52)
  (parent 32)
  (seen 49 70 74)
  (unrealized (1 0) (3 0))
  (comment "7 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 (contracted (a-0 a)) 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))) (send (enc "okay" x3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 53)
  (parent 33)
  (seen 17)
  (unrealized)
  (shape)
  (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 (added-strand init 2) x3 (1 0) (enc x3 (pubk a))
    (enc x3 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 54)
  (parent 33)
  (seen 79)
  (unrealized (1 0))
  (comment "4 in cohort - 3 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 55)
  (parent 33)
  (seen 60 80 81)
  (unrealized (1 0) (3 0))
  (comment "7 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 56)
  (parent 33)
  (seen 79)
  (unrealized (1 0))
  (comment "4 in cohort - 2 not yet seen"))

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

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

(defskeleton wonthull3
  (vars (x3 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 y3) (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 (added-strand init 2) y3 (3 0)
    (enc y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc y3 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 60)
  (parent 42)
  (seen 89)
  (unrealized (1 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x3 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x3) (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 (added-strand init 2) x3 (3 0)
    (enc x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x3 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 61)
  (parent 42)
  (seen 91)
  (unrealized (1 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x3 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 y3) (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)) ((1 1) (0 2)) ((2 1) (3 0)) ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 4 2 resp 2) y3 (3 0)
    (enc y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc y3 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 62)
  (parent 42)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x3 y3 text) (a name))
  (defstrand init 3 (x1 y3) (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 y3 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 63)
  (parent 43)
  (seen 41)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 y3) (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 y3 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 64)
  (parent 43)
  (seen 62 89 91)
  (unrealized (1 0) (3 0))
  (comment "7 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 y3) (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)) ((1 1) (0 2)) ((2 1) (3 0)) ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 4 2 resp 2) x3 (3 0)
    (enc x3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc y3 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 65)
  (parent 45)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (y3 text) (a name))
  (defstrand init 3 (x1 y3) (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))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (x1 y3) (a-0 a)) y3 (1 0)
    (enc y3 (pubk a)) (enc "okay" y3 y3 (pubk a)) (enc y3 y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc y3 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)))))
  (label 66)
  (parent 46)
  (seen 59)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 y3) (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 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 y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc y3 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 67)
  (parent 46)
  (seen 65 70)
  (unrealized (1 0) (3 0))
  (comment "7 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 y3-0 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x1) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (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 x1)
  (operation nonce-test (contracted (x1-0 x1) (a-0 a)) x1 (1 0)
    (enc x1 (pubk a)) (enc "okay" y3-0 x1 (pubk a))
    (enc x1 x1 (pubk a)))
  (traces
    ((send (enc x1 (pubk a)))
      (send (cat (enc x1 x1 (pubk a)) (enc x1 x1 (pubk a))))
      (recv (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 68)
  (parent 47)
  (seen 38)
  (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 x1-0) (x3 x1-0) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1-0) (y3 x1-0) (a a-0))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (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 x1-0)
  (operation nonce-test (displaced 4 2 resp 2) x1-0 (1 0)
    (enc x1-0 (pubk a)) (enc "okay" y3-0 x1-0 (pubk a))
    (enc x1-0 x1-0 (pubk a)))
  (traces
    ((send (enc x1-0 (pubk a)))
      (send (cat (enc x1-0 x1-0 (pubk a)) (enc x1-0 x1-0 (pubk a))))
      (recv (enc "okay" x1-0 x1 (pubk a))))
    ((recv (enc x1 x1-0 (pubk a-0)))
      (send (enc "okay" x1-0 x1 (pubk a-0))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3-0 x1-0 (pubk a)))))
  (label 69)
  (parent 47)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 y3) (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) x1-0 (1 0)
    (enc x1-0 (pubk a)) (enc "okay" y3-0 x1-0 (pubk a))
    (enc x1-0 x1-0 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc y3 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 70)
  (parent 47)
  (unrealized (1 0))
  (comment "1 in cohort - 1 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 71)
  (parent 48)
  (seen 39)
  (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 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 72)
  (parent 48)
  (seen 40)
  (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 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 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 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 73)
  (parent 48)
  (unrealized (1 0))
  (comment "2 in cohort - 2 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 74)
  (parent 48)
  (unrealized (1 0))
  (comment "2 in cohort - 2 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)) ((1 1) (0 2)) ((2 1) (3 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 75)
  (parent 49)
  (seen 40)
  (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 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)) ((1 1) (0 2)) ((2 1) (3 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 76)
  (parent 49)
  (seen 39)
  (unrealized)
  (comment "1 in cohort - 0 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 77)
  (parent 54)
  (seen 17)
  (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) (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 78)
  (parent 54)
  (seen 61 80)
  (unrealized (1 0) (3 0))
  (comment "7 in cohort - 1 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 79)
  (parent 54)
  (seen 50)
  (unrealized (1 0))
  (comment "2 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 (added-strand 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 80)
  (parent 55)
  (seen 103)
  (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) (0 2))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (added-strand 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 81)
  (parent 55)
  (seen 80 105)
  (unrealized (1 0))
  (comment "5 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)) ((1 1) (0 2)) ((2 1) (3 0)) ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 4 2 resp 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 82)
  (parent 55)
  (seen 100)
  (unrealized (1 0))
  (comment "3 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 83)
  (parent 56)
  (seen 53)
  (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 84)
  (parent 56)
  (seen 82 89 103 105)
  (unrealized (1 0) (3 0))
  (comment "7 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 y3-0 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x1) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (precedes ((0 1) (3 0)) ((1 1) (2 0)) ((2 1) (0 2)) ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (contracted (x1-0 x1) (a-0 a)) x1 (1 0)
    (enc x1 (pubk a)) (enc "okay" y3-0 x1 (pubk a))
    (enc x1 x1 (pubk a)))
  (traces
    ((send (enc x1 (pubk a)))
      (send (cat (enc x1 x1 (pubk a)) (enc x1 x1 (pubk a))))
      (recv (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 85)
  (parent 57)
  (seen 38)
  (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) (3 0)) ((1 1) (2 0)) ((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 86)
  (parent 58)
  (seen 39)
  (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 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) (3 0)) ((1 1) (2 0)) ((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 87)
  (parent 58)
  (seen 40)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 y3 y3-0 text) (a name))
  (defstrand init 3 (x1 y3) (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 y3 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 88)
  (parent 60)
  (seen 41)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 y3) (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 2 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 y3 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 89)
  (parent 60)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x3 y3 text) (a name))
  (defstrand init 3 (x1 x3) (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)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x3 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 90)
  (parent 61)
  (seen 38)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x3) (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 2 resp 2) x3 (1 0)
    (enc x3 (pubk a)) (enc "okay" y3 x3 (pubk a)) (enc x3 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x3 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 91)
  (parent 61)
  (seen 95)
  (unrealized (1 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 y3 y3-0 text) (a name))
  (defstrand init 3 (x1 y3) (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)) ((1 1) (0 2)) ((2 1) (3 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 y3 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 92)
  (parent 62)
  (seen 63)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (y3 y3-0 text) (a name))
  (defstrand init 3 (x1 y3) (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)) ((1 1) (0 2)) ((2 1) (3 0)) ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (x1 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 y3 y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc y3 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 93)
  (parent 65)
  (seen 38)
  (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 x1) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (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 x1)
  (operation nonce-test (contracted (x1-0 x1) (a-0 a)) x1 (1 0)
    (enc x1 (pubk a)) (enc "okay" y3 x1 (pubk a))
    (enc "okay" y3-0 x1 (pubk a)) (enc x1 x1 (pubk a)))
  (traces
    ((send (enc x1 (pubk a)))
      (send (cat (enc x1 x1 (pubk a)) (enc x1 x1 (pubk a))))
      (recv (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 94)
  (parent 69)
  (seen 38)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (y3 y3-0 text) (a name))
  (defstrand init 3 (x1 y3) (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 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 y3 y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc y3 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 95)
  (parent 70)
  (seen 38)
  (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) (1 0))
    ((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 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 96)
  (parent 73)
  (seen 39)
  (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 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) (1 0))
    ((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 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 97)
  (parent 73)
  (seen 40)
  (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 98)
  (parent 74)
  (seen 40)
  (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 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 99)
  (parent 74)
  (seen 39)
  (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 1) (2 0)) ((1 1) (0 2)) ((2 1) (3 0)) ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 4 2 resp 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 100)
  (parent 78)
  (seen 75)
  (unrealized (1 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 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 101)
  (parent 79)
  (seen 91 100 103)
  (unrealized (1 0) (3 0))
  (comment "7 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 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 102)
  (parent 80)
  (seen 40)
  (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 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 2 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)))))
  (label 103)
  (parent 80)
  (seen 98)
  (unrealized (1 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) (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 104)
  (parent 81)
  (seen 53)
  (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 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) 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)))))
  (label 105)
  (parent 81)
  (seen 103)
  (unrealized (1 0))
  (comment "3 in cohort - 1 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)) ((1 1) (0 2)) ((2 1) (3 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 106)
  (parent 82)
  (seen 83)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 y3 y3-0 text) (a name))
  (defstrand init 3 (x1 y3) (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 y3 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 107)
  (parent 89)
  (seen 63)
  (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 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 108)
  (parent 105)
  (seen 83)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")