(comment "CPSA 2.2.11")
(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 "3 in cohort - 3 not yet seen"))

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

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

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

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

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

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

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

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

(comment "Nothing left to do")

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

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

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

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

(defskeleton wonthull3
  (vars (x1 x3 x1-0 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (1 0)) ((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) x3-0 (2 0)
    (enc x3-0 (pubk a)))
  (traces
    ((send (enc x3 (pubk a)))
      (send (cat (enc x1-0 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 21)
  (parent 15)
  (seen 25 27)
  (unrealized (1 0))
  (comment "5 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x3 x1-0 x3-0 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x3) (x3 x3-0) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3-0) (y2 x3) (y3 y3) (a a))
  (precedes ((0 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 22)
  (parent 15)
  (seen 21 28)
  (unrealized (0 2))
  (comment "4 in cohort - 1 not yet seen"))

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

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

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

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

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

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

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 1) (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 35)
  (parent 22)
  (seen 43 54)
  (unrealized (1 0))
  (comment "5 in cohort - 3 not yet seen"))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(defskeleton wonthull3
  (vars (x3 x1 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (precedes ((0 1) (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 53)
  (parent 35)
  (seen 17 71)
  (unrealized (1 0))
  (comment "7 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 54)
  (parent 35)
  (seen 71)
  (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 55)
  (parent 35)
  (seen 61)
  (unrealized (1 0) (3 0))
  (comment "4 in cohort - 3 not yet seen"))

(defskeleton wonthull3
  (vars (x1 x1-0 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 x1-0) (x2 x1-0) (x3 x1-0) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1-0) (y3 x1-0) (a a-0))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3-0) (a a))
  (precedes ((0 1) (3 0)) ((1 1) (2 0)) ((2 1) (0 2)) ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1-0)
  (operation nonce-test (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 56)
  (parent 37)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

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

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

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

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

(defskeleton wonthull3
  (vars (x3 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 y3) (x2 x3) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 1) (2 0)) ((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 y3 x3 (pubk a)) (enc y3 x3 (pubk a))))
      (recv (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a-0))) (send (enc "okay" x3 y3 (pubk a-0))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 61)
  (parent 45)
  (seen 81)
  (unrealized (1 0))
  (comment "3 in cohort - 1 not yet seen"))

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

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

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

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

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

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

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

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

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

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 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 72)
  (parent 53)
  (seen 62 75)
  (unrealized (1 0) (3 0))
  (comment "4 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 73)
  (parent 54)
  (seen 43)
  (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 74)
  (parent 54)
  (seen 77 81)
  (unrealized (1 0) (3 0))
  (comment "4 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 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) y3-0 (3 0)
    (enc y3-0 (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 75)
  (parent 55)
  (seen 40 91)
  (unrealized (1 0))
  (comment "3 in cohort - 0 not yet seen"))

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

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

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

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

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

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

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

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

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

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

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

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

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 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 89)
  (parent 71)
  (seen 82 90 91)
  (unrealized (1 0) (3 0))
  (comment "4 in cohort - 0 not yet seen"))

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

(defskeleton wonthull3
  (vars (x3 x1 y3 text) (a a-0 name))
  (defstrand init 3 (x1 x1) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (precedes ((0 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) y3-0 (3 0)
    (enc y3-0 (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 91)
  (parent 74)
  (seen 87)
  (unrealized (1 0))
  (comment "1 in cohort - 0 not yet seen"))

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

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

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

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

(comment "Nothing left to do")