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

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

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

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

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

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

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

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

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

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

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

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

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

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

(comment "Nothing left to do")

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

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

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

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

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

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

(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)))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(defskeleton wonthull3
  (vars (x1 y3 y3-0 text) (a a-0 name))
  (defstrand init 3 (x1 y3) (x2 y3) (x3 y3) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 y3) (y3 y3) (a a-0))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3-0) (a a))
  (precedes ((0 1) (2 0)) ((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 47)
  (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 48)
  (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 48)
  (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 (added-strand 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 51)
  (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 71)
  (parent 53)
  (seen 60 73)
  (unrealized (1 0) (3 0))
  (comment "7 in cohort - 1 not yet seen"))

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

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

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

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

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

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

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

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

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

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

(comment "Nothing left to do")