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

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

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

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

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

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

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

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

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

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

(defskeleton wonthull3
  (vars (x1 x4 y3 y3-0 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))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (precedes ((0 0) (2 0)) ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (0 2) (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 x4 (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 10)
  (parent 5)
  (unrealized (0 2) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

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

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

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

(defskeleton wonthull3
  (vars (x1 x4 y3 y3-0 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))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (precedes ((0 0) (3 0)) ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (0 2) (enc x1 (pubk a))
    (enc "okay" x1 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 x4 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3 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-0 x1 (pubk a)))))
  (label 18)
  (parent 11)
  (seen 13)
  (unrealized (0 2) (3 0))
  (comment "1 in cohort - 0 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 nonce-test (contracted (x2 x1) (x4 x1)) x1 (0 2)
    (enc x1 (pubk a)) (enc "okay" x1 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)))))
  (label 19)
  (parent 12)
  (seen 7)
  (unrealized)
  (comment "1 in cohort - 0 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))
  (defstrand resp 2 (y1 x2) (y2 x2) (y3 x1) (a a))
  (defstrand resp 2 (y1 x2) (y2 x2) (y3 x2) (a a))
  (precedes ((0 0) (2 0)) ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x2)
  (operation nonce-test (added-strand resp 2) x2 (0 2) (enc x2 (pubk a))
    (enc "okay" x1 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" x1 x2 (pubk a))))
    ((recv (enc x2 x2 (pubk a))) (send (enc "okay" x2 x2 (pubk a)))))
  (label 20)
  (parent 12)
  (seen 26)
  (unrealized (0 2) (2 0))
  (comment "1 in cohort - 0 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 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (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" x1 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 x4 (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 21)
  (parent 12)
  (seen 13)
  (unrealized (0 2) (2 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x1) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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 (contracted (x4 x1)) x1 (0 2) (enc x1 (pubk a))
    (enc "okay" x1 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" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 22)
  (parent 13)
  (seen 19)
  (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))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 x1) (a a))
  (precedes ((0 1) (1 0)) ((1 1) (2 0)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (x4 y3)) y3 (0 2) (enc y3 (pubk a))
    (enc "okay" x1 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" x1 y3 (pubk a)))))
  (label 23)
  (parent 14)
  (seen 7)
  (unrealized)
  (comment "1 in cohort - 0 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 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 0) (3 0)) ((0 1) (1 0)) ((1 1) (2 0)) ((2 1) (0 2))
    ((3 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (0 2) (enc x1 (pubk a))
    (enc "okay" x1 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 x4 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (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 24)
  (parent 14)
  (unrealized (0 2) (3 0))
  (comment "1 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))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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" 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 x4 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 25)
  (parent 15)
  (seen 13)
  (unrealized (0 2) (2 0))
  (comment "1 in cohort - 0 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))
  (defstrand resp 2 (y1 x2) (y2 x2) (y3 x2) (a a))
  (defstrand resp 2 (y1 x2) (y2 x2) (y3 x1) (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 x2)
  (operation nonce-test (displaced 4 0 init 2) x2 (3 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" x2 x2 (pubk a))))
    ((recv (enc x2 x2 (pubk a))) (send (enc "okay" x1 x2 (pubk a)))))
  (label 26)
  (parent 17)
  (unrealized (0 2))
  (comment "2 in cohort - 2 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))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (precedes ((0 1) (1 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (displaced 4 0 init 2) x2 (3 0)
    (enc x2 (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))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 27)
  (parent 17)
  (seen 22)
  (unrealized (0 2))
  (comment "1 in cohort - 0 not yet seen"))

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

(defskeleton wonthull3
  (vars (x1 x2 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x2) (x3 x2) (x4 x2) (a a))
  (defstrand resp 2 (y1 x2) (y2 x2) (y3 x2) (a a))
  (defstrand resp 2 (y1 x2) (y2 x2) (y3 x1) (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 x2)
  (operation nonce-test (contracted (x4 x2)) x2 (0 2) (enc x2 (pubk a))
    (enc "okay" x1 x2 (pubk a)) (enc "okay" x2 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 x2 (pubk a))))
    ((recv (enc x2 x2 (pubk a))) (send (enc "okay" x2 x2 (pubk a))))
    ((recv (enc x2 x2 (pubk a))) (send (enc "okay" x1 x2 (pubk a)))))
  (label 30)
  (parent 26)
  (seen 7)
  (unrealized)
  (comment "1 in cohort - 0 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 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 0) (3 0)) ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (0 2) (enc x1 (pubk a))
    (enc "okay" x1 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 x4 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (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 31)
  (parent 26)
  (seen 13)
  (unrealized (0 2) (3 0))
  (comment "1 in cohort - 0 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 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 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 0) (4 0)) ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (3 0))
    ((2 1) (0 2)) ((3 1) (0 2)) ((4 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" x1 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 x4 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (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" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a)))))
  (label 32)
  (parent 28)
  (seen 29)
  (unrealized (0 2) (4 0))
  (comment "1 in cohort - 0 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 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3) (a a))
  (precedes ((0 1) (1 0)) ((0 1) (3 0)) ((1 1) (2 0)) ((2 1) (0 2))
    ((3 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (contracted (x4 x1)) x1 (0 2) (enc x1 (pubk a))
    (enc "okay" x1 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" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a)))))
  (label 33)
  (parent 29)
  (seen 22)
  (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 34)
  (unrealized (0 2))
  (origs (x3-0 (0 0)))
  (comment "3 in cohort - 3 not yet seen"))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (1 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (0 2)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (x1-0 x1) (a-0 a)) x3 (1 0)
    (enc x3 (pubk a)) (enc x3 x3 (pubk a)) (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 57)
  (parent 46)
  (seen 39)
  (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 58)
  (parent 46)
  (seen 43)
  (unrealized (1 0) (3 0))
  (comment "2 in cohort - 1 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))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x1-0) (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 4 0 init 2) x3 (3 0)
    (enc x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x1-0 x3 (pubk a)))))
  (label 59)
  (parent 49)
  (unrealized (1 0))
  (comment "4 in cohort - 4 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))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 x1-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 0 init 2) x3 (3 0)
    (enc x3 (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" x1-0 x1-0 (pubk a)))))
  (label 60)
  (parent 49)
  (unrealized (1 0))
  (comment "1 in cohort - 1 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))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 x1-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" x1-0 y3 (pubk a)))))
  (label 61)
  (parent 49)
  (unrealized (1 0))
  (comment "3 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))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 4 0 init 2) x3 (3 0)
    (enc x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1-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" x3 x3 (pubk a)))))
  (label 62)
  (parent 50)
  (unrealized (1 0))
  (comment "4 in cohort - 4 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 (displaced 4 0 init 1) 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)))))
  (label 63)
  (parent 51)
  (unrealized (1 0))
  (comment "2 in cohort - 2 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 64)
  (parent 54)
  (unrealized (1 0))
  (comment "2 in cohort - 2 not yet seen"))

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

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

(defskeleton wonthull3
  (vars (x3 x1 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (0 2))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 4 0 init 2) y3 (3 0)
    (enc y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a-0))) (send (enc "okay" x3 y3 (pubk a-0))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 68)
  (parent 56)
  (seen 86 87)
  (unrealized (1 0))
  (comment "3 in cohort - 1 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 (displaced 4 0 init 2) x3 (3 0)
    (enc x3 (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 58)
  (seen 60 82 83)
  (unrealized (1 0))
  (comment "3 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 x1) (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" x1 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" x1 x3 (pubk a)))))
  (label 70)
  (parent 59)
  (seen 38)
  (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 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x1) (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" x1 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" x1 x3 (pubk a)))))
  (label 71)
  (parent 59)
  (seen 39)
  (unrealized)
  (comment "1 in cohort - 0 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))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x1-0) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (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" x1-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" x1-0 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a)))))
  (label 72)
  (parent 59)
  (unrealized (1 0) (3 0))
  (comment "1 in cohort - 1 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 x1-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (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 x1-0)
  (operation nonce-test (added-strand resp 2) x1-0 (1 0)
    (enc x1-0 (pubk a)) (enc "okay" x1-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" x1-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3 x1-0 (pubk a)))))
  (label 73)
  (parent 59)
  (seen 60)
  (unrealized (1 0) (3 0))
  (comment "1 in cohort - 0 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))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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" x1 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))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 74)
  (parent 60)
  (unrealized)
  (comment "1 in cohort - 1 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))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 x1) (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" x1 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))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" x1 y3 (pubk a)))))
  (label 75)
  (parent 61)
  (seen 71)
  (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))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 x1) (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" x1 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))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" x1 y3 (pubk a)))))
  (label 76)
  (parent 61)
  (seen 70)
  (unrealized)
  (comment "1 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 x1-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 x1-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3) (a a))
  (precedes ((0 0) (4 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (3 0))
    ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1-0)
  (operation nonce-test (added-strand resp 2) x1-0 (1 0)
    (enc x1-0 (pubk a)) (enc "okay" x1-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" x1-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" x1-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3 x1-0 (pubk a)))))
  (label 77)
  (parent 61)
  (unrealized (1 0) (4 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 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 x3) (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" x3 x3 (pubk a))
    (enc "okay" y3 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (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" x3 x3 (pubk a)))))
  (label 78)
  (parent 62)
  (seen 84)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (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" x3 x3 (pubk a))
    (enc "okay" y3 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 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" x3 x3 (pubk a)))))
  (label 79)
  (parent 62)
  (unrealized)
  (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))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x1-0) (a a))
  (precedes ((0 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (1 0)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand resp 2) x3 (1 0) (enc x3 (pubk a))
    (enc "okay" x3 x3 (pubk a)) (enc "okay" y3 x3 (pubk a))
    (enc x3 x3 (pubk a)) (enc x1-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" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x1-0 x3 (pubk a)))))
  (label 80)
  (parent 62)
  (seen 89)
  (unrealized (1 0) (4 0))
  (comment "3 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 x1-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3-0) (a a))
  (precedes ((0 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (1 0)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1-0)
  (operation nonce-test (added-strand resp 2) x1-0 (1 0)
    (enc x1-0 (pubk a)) (enc "okay" x1-0 x1-0 (pubk a))
    (enc "okay" y3 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" x1-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3-0 x1-0 (pubk a)))))
  (label 81)
  (parent 62)
  (seen 60)
  (unrealized (1 0) (4 0))
  (comment "1 in cohort - 0 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 82)
  (parent 63)
  (unrealized)
  (comment "1 in cohort - 1 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))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 x1-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 x1-0)
  (operation nonce-test (added-strand resp 2) x1-0 (1 0)
    (enc x1-0 (pubk a)) (enc "okay" y3 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" x1-0 x1-0 (pubk a)))))
  (label 83)
  (parent 63)
  (seen 60)
  (unrealized (1 0) (3 0))
  (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) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (a-0 a)) x3 (1 0) (enc x3 (pubk a))
    (enc "okay" x3 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a)))))
  (label 84)
  (parent 64)
  (seen 38)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (0 2))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 4 0 init 2) x3 (3 0)
    (enc x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a-0))) (send (enc "okay" x3 x3 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 86)
  (parent 65)
  (seen 47 96)
  (unrealized (1 0))
  (comment "5 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 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 4 0 init 2) y3 (3 0)
    (enc y3 (pubk a)))
  (traces
    ((send (enc y3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a-0))) (send (enc "okay" x3 y3 (pubk a-0))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 87)
  (parent 67)
  (seen 96)
  (unrealized (1 0))
  (comment "2 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)) ((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 88)
  (parent 68)
  (seen 53)
  (unrealized)
  (comment "1 in cohort - 0 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))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x1-0) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 4 0 init 2) x3 (3 0)
    (enc x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1-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" x1-0 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a)))))
  (label 89)
  (parent 72)
  (unrealized (1 0))
  (comment "3 in cohort - 3 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))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (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))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 90)
  (parent 74)
  (seen 95)
  (unrealized)
  (comment "1 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 x1-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 x1-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 1) (3 0))
    ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1-0)
  (operation nonce-test (displaced 5 0 init 2) x1-0 (4 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" x1-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" x1-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3 x1-0 (pubk a)))))
  (label 91)
  (parent 77)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x3 x1 text) (a name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (precedes ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation generalization deleted (2 0))
  (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" x3 x3 (pubk a)))))
  (label 92)
  (parent 79)
  (seen 39)
  (unrealized)
  (comment "1 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))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 x1-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 x1-0) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((0 1) (4 0)) ((1 1) (0 2))
    ((2 1) (1 0)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1-0)
  (operation nonce-test (displaced 5 0 init 2) x3 (4 0)
    (enc x3 (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" x1-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" x1-0 x1-0 (pubk a)))))
  (label 93)
  (parent 80)
  (seen 74)
  (unrealized (1 0))
  (comment "1 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 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) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 x1-0) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (4 0))
    ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 5 2 resp 2) x3 (4 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 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" x1-0 y3 (pubk a)))))
  (label 94)
  (parent 80)
  (seen 75 76)
  (unrealized (1 0))
  (comment "3 in cohort - 1 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 95)
  (parent 82)
  (seen 38)
  (unrealized)
  (origs (x1 (0 0)))
  (comment "1 in cohort - 0 not yet seen"))

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

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

(defskeleton wonthull3
  (vars (x1 y3 y3-0 text) (a a-0 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-0))
  (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 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) 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-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((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 99)
  (parent 86)
  (unrealized (1 0) (4 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 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 100)
  (parent 87)
  (seen 66)
  (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 x1) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (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" x3 x3 (pubk a))
    (enc "okay" x1 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" x1 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a)))))
  (label 101)
  (parent 89)
  (seen 84)
  (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 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x1) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (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" x3 x3 (pubk a))
    (enc "okay" x1 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" x1 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a)))))
  (label 102)
  (parent 89)
  (seen 92)
  (unrealized)
  (comment "1 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 x1-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 x1-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3) (a a))
  (precedes ((0 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (1 0)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1-0)
  (operation nonce-test (added-strand resp 2) x1-0 (1 0)
    (enc x1-0 (pubk a)) (enc "okay" x1-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" x1-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" x1-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3 x1-0 (pubk a)))))
  (label 103)
  (parent 89)
  (seen 60)
  (unrealized (1 0) (4 0))
  (comment "1 in cohort - 0 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 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)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 1) (3 0))
    ((3 1) (1 0)) ((4 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" x1 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" 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 104)
  (parent 91)
  (seen 74)
  (unrealized)
  (comment "1 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 x1-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 x1-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 x1-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3) (a a))
  (precedes ((0 0) (5 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (4 0)) ((3 1) (1 0)) ((4 1) (1 0)) ((5 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1-0)
  (operation nonce-test (added-strand resp 2) x1-0 (1 0)
    (enc x1-0 (pubk a)) (enc "okay" x1-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" x1-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" x1-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" x1-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3 x1-0 (pubk a)))))
  (label 105)
  (parent 94)
  (seen 91)
  (unrealized (1 0) (5 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))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x1) (a a))
  (precedes ((0 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (1 0)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand resp 2) x3 (1 0) (enc x3 (pubk a))
    (enc "okay" x3 x3 (pubk a)) (enc "okay" y3 x3 (pubk a))
    (enc x3 x3 (pubk a)) (enc x1 x3 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a-0))) (send (enc "okay" x3 x3 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x1 x3 (pubk a)))))
  (label 106)
  (parent 96)
  (unrealized (1 0) (4 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 y3-0 text) (a a-0 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-0))
  (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 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (1 0)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (1 0) (enc x1 (pubk a))
    (enc "okay" x1 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-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((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 107)
  (parent 96)
  (unrealized (1 0) (4 0))
  (comment "1 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))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x1) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (0 2))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 5 0 init 2) x3 (4 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" x1 x3 (pubk a)))))
  (label 108)
  (parent 97)
  (seen 70 113)
  (unrealized (1 0))
  (comment "4 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (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 x1) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((0 1) (4 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (displaced 5 0 init 2) x3 (4 0)
    (enc x3 (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-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((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" x1 x1 (pubk a)))))
  (label 109)
  (parent 97)
  (seen 74)
  (unrealized (1 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (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 x1) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (0 2))
    ((3 1) (4 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 5 3 resp 2) x3 (4 0)
    (enc x3 (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-0))) (send (enc "okay" y3 y3 (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 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" x1 y3 (pubk a)))))
  (label 110)
  (parent 97)
  (seen 76)
  (unrealized (1 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (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) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (0 2))
    ((3 1) (4 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 5 3 resp 2) x3 (4 0)
    (enc x3 (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-0))) (send (enc "okay" y3 y3 (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 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 111)
  (parent 98)
  (seen 119)
  (unrealized (1 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (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)) ((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 (displaced 5 0 init 1) x1 (4 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 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((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 112)
  (parent 99)
  (seen 82 116)
  (unrealized (1 0))
  (comment "3 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))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x1) (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 5 0 init 2) x3 (4 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" x1 x3 (pubk a)))))
  (label 113)
  (parent 106)
  (seen 101)
  (unrealized (1 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (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 x1) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((0 1) (4 0)) ((1 1) (0 2))
    ((2 1) (1 0)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (displaced 5 0 init 2) x3 (4 0)
    (enc x3 (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-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((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" x1 x1 (pubk a)))))
  (label 114)
  (parent 106)
  (seen 74)
  (unrealized (1 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (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 x1) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (4 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 5 3 resp 2) x3 (4 0)
    (enc x3 (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-0))) (send (enc "okay" y3 y3 (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 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" x1 y3 (pubk a)))))
  (label 115)
  (parent 106)
  (seen 76)
  (unrealized (1 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (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)) ((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 (displaced 5 0 init 1) x1 (4 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 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((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 116)
  (parent 107)
  (seen 74)
  (unrealized (1 0))
  (comment "1 in cohort - 0 not yet seen"))

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

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 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 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (1 0) (enc x1 (pubk a))
    (enc "okay" x1 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-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((recv (enc x1 x1 (pubk a))) (send (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 118)
  (parent 108)
  (seen 116)
  (unrealized (1 0) (4 0))
  (comment "1 in cohort - 0 not yet seen"))

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

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (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 x1) (a a))
  (precedes ((0 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (0 2)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) 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-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((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" x1 x1 (pubk a)))))
  (label 122)
  (parent 112)
  (seen 116)
  (unrealized (1 0) (4 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 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 0) (4 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (1 0)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (1 0) (enc x1 (pubk a))
    (enc "okay" x1 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-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((recv (enc x1 x1 (pubk a))) (send (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 123)
  (parent 113)
  (seen 116)
  (unrealized (1 0) (4 0))
  (comment "1 in cohort - 0 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))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (4 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (contracted (a-0 a) (y3 x1)) x1 (1 0)
    (enc x1 (pubk a)) (enc "okay" x1 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" 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" x1 x1 (pubk a)))))
  (label 124)
  (parent 115)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 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 0) (5 0)) ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2))
    ((2 1) (1 0)) ((3 1) (4 0)) ((4 1) (1 0)) ((5 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (1 0) (enc x1 (pubk a))
    (enc "okay" x1 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-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((recv (enc x1 x1 (pubk a))) (send (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" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a)))))
  (label 125)
  (parent 115)
  (seen 127 128)
  (unrealized (1 0) (5 0))
  (comment "2 in cohort - 0 not yet seen"))

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

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 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)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 1) (3 0))
    ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (displaced 6 0 init 2) x1 (5 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 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((recv (enc x1 x1 (pubk a))) (send (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 127)
  (parent 119)
  (seen 104)
  (unrealized (1 0))
  (comment "1 in cohort - 0 not yet seen"))

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

(defskeleton wonthull3
  (vars (y3 text) (a a-0 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-0))
  (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) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (0 2))
    ((3 1) (4 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 5 3 resp 2) x1 (4 0)
    (enc x1 (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-0))) (send (enc "okay" y3 y3 (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 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 130)
  (parent 122)
  (seen 131)
  (unrealized (1 0))
  (comment "2 in cohort - 1 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))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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 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))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 131)
  (parent 124)
  (seen 90)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (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 x1)
  (operation nonce-test (added-strand resp 2) x1 (1 0) (enc x1 (pubk a))
    (enc "okay" x1 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-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((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 132)
  (parent 126)
  (seen 116)
  (unrealized (1 0) (3 0))
  (comment "1 in cohort - 0 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 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 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)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (5 0))
    ((3 1) (4 0)) ((4 1) (1 0)) ((5 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (contracted (a-0 a)) x1 (1 0) (enc x1 (pubk a))
    (enc "okay" x1 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" 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" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a)))))
  (label 133)
  (parent 128)
  (seen 104)
  (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) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3-0) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 1) (3 0))
    ((3 1) (1 0)) ((4 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 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 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 134)
  (parent 129)
  (seen 78)
  (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 x1) (x2 y3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (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) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 x1) (a a))
  (precedes ((0 0) (5 0)) ((0 1) (2 0)) ((0 1) (4 0)) ((1 1) (0 2))
    ((2 1) (3 0)) ((3 1) (1 0)) ((4 1) (1 0)) ((5 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (added-strand resp 2) y3 (1 0) (enc y3 (pubk a))
    (enc "okay" y3 y3 (pubk a)) (enc "okay" y3-0 y3 (pubk a))
    (enc x1 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-0))) (send (enc "okay" y3 y3 (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 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" x1 y3 (pubk a)))))
  (label 135)
  (parent 129)
  (unrealized (1 0) (5 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 y3-0 text) (a a-0 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-0))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 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 0) (5 0)) ((0 1) (2 0)) ((0 1) (4 0)) ((1 1) (0 2))
    ((2 1) (3 0)) ((3 1) (1 0)) ((4 1) (1 0)) ((5 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (1 0) (enc x1 (pubk a))
    (enc "okay" x1 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-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((recv (enc x1 x1 (pubk a))) (send (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 136)
  (parent 129)
  (seen 127)
  (unrealized (1 0) (5 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (y3 y3-0 text) (a a-0 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-0))
  (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 0) (4 0)) ((0 1) (2 0)) ((1 1) (0 2)) ((2 1) (3 0))
    ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (added-strand resp 2) y3 (1 0) (enc y3 (pubk a))
    (enc "okay" y3 y3 (pubk a)) (enc 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-0))) (send (enc "okay" y3 y3 (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 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 137)
  (parent 130)
  (seen 127)
  (unrealized (1 0) (4 0))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (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 x1) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 1) (3 0))
    ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 6 0 init 2) y3 (5 0)
    (enc 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-0))) (send (enc "okay" y3 y3 (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 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" x1 y3 (pubk a)))))
  (label 138)
  (parent 135)
  (seen 125)
  (unrealized (1 0))
  (comment "2 in cohort - 1 not yet seen"))

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

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (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) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 x1) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 1) (3 0))
    ((3 1) (1 0)) ((4 1) (5 0)) ((5 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 6 4 resp 2) y3-0 (5 0)
    (enc y3-0 (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-0))) (send (enc "okay" y3 y3 (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 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" x1 y3 (pubk a)))))
  (label 140)
  (parent 135)
  (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))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 x1) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 1) (3 0))
    ((3 1) (1 0)) ((4 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" x1 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))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" x1 y3 (pubk a)))))
  (label 141)
  (parent 138)
  (seen 101)
  (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))
  (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) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 x1) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (4 0)) ((1 1) (0 2)) ((2 1) (3 0))
    ((3 1) (1 0)) ((4 1) (5 0)) ((5 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" x1 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))))
    ((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" x1 y3 (pubk a)))))
  (label 142)
  (parent 140)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 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 0) (6 0)) ((0 1) (2 0)) ((0 1) (4 0)) ((1 1) (0 2))
    ((2 1) (3 0)) ((3 1) (1 0)) ((4 1) (5 0)) ((5 1) (1 0))
    ((6 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (1 0) (enc x1 (pubk a))
    (enc "okay" x1 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-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((recv (enc x1 x1 (pubk a))) (send (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" 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 143)
  (parent 140)
  (unrealized (1 0) (6 0))
  (comment "1 in cohort - 1 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))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 x1) (a a))
  (precedes ((0 1) (2 0)) ((0 1) (3 0)) ((1 1) (0 2)) ((2 1) (1 0))
    ((3 1) (4 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation generalization deleted (2 0))
  (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 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" x1 y3 (pubk a)))))
  (label 144)
  (parent 142)
  (seen 76)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull3
  (vars (x1 y3 text) (a a-0 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-0))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 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)) ((0 1) (4 0)) ((0 1) (6 0)) ((1 1) (0 2))
    ((2 1) (3 0)) ((3 1) (1 0)) ((4 1) (5 0)) ((5 1) (1 0))
    ((6 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (displaced 7 0 init 2) x1 (6 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 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a-0))) (send (enc "okay" x1 x1 (pubk a-0))))
    ((recv (enc x1 x1 (pubk a))) (send (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" 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 145)
  (parent 143)
  (unrealized (1 0))
  (comment "1 in cohort - 1 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 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 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)) ((0 1) (4 0)) ((0 1) (6 0)) ((1 1) (0 2))
    ((2 1) (3 0)) ((3 1) (1 0)) ((4 1) (5 0)) ((5 1) (1 0))
    ((6 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (contracted (a-0 a)) x1 (1 0) (enc x1 (pubk a))
    (enc "okay" x1 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" 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" 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 146)
  (parent 145)
  (unrealized)
  (comment "1 in cohort - 1 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 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 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)) ((0 1) (3 0)) ((0 1) (5 0)) ((1 1) (0 2))
    ((2 1) (1 0)) ((3 1) (4 0)) ((4 1) (1 0)) ((5 1) (1 0)))
  (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))))
    ((recv (enc x1 x1 (pubk a))) (send (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" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a)))))
  (label 147)
  (parent 146)
  (seen 104)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")