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

(defprotocol wonthull2 basic
  (defrole init
    (vars (a name) (x1 x2 x3 x4 text))
    (trace (send (cat (enc x1 x3 (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 wonthull2
  (vars (x1 x2 x3 x4 text) (a name))
  (defstrand init 2 (x1 x1) (x2 x2) (x3 x3) (x4 x4) (a a))
  (non-orig (privk a))
  (uniq-orig x3)
  (traces
    ((send (cat (enc x1 x3 (pubk a)) (enc x3 x2 (pubk a))))
      (recv (enc "okay" x3 x4 (pubk a)))))
  (label 0)
  (unrealized (0 1))
  (origs (x3 (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

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

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

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

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

(defskeleton wonthull2
  (vars (x1 x2 y3 text) (a name))
  (defstrand init 2 (x1 x1) (x2 x2) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x2) (y3 y3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (x3 y3) (x4 y3)) y3 (0 1)
    (enc "okay" y3 y3 (pubk a)) (enc x1 y3 (pubk a))
    (enc y3 x2 (pubk a)))
  (traces
    ((send (cat (enc x1 y3 (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 5)
  (parent 2)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (x1 x1) (x2 x2) (x3 y3) (x4 y3))))
  (origs (y3 (0 0))))

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

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

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

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

(defskeleton wonthull2
  (vars (x2 y3 text) (a name))
  (defstrand init 2 (x1 y3) (x2 x2) (x3 y3) (x4 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x2) (y3 y3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation generalization deleted (1 0))
  (traces
    ((send (cat (enc y3 y3 (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 7)
  (seen 5)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")

(defprotocol wonthull2 basic
  (defrole init
    (vars (a name) (x1 x2 x3 x4 text))
    (trace (send (cat (enc x1 x3 (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 wonthull2
  (vars (x1 x3 x1-0 x3-0 text) (a a-0 name))
  (defstrand init 2 (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 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x3-0)
  (traces
    ((send (cat (enc x1-0 x3-0 (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 11)
  (seen 12)
  (unrealized (0 1))
  (origs (x3-0 (0 0)))
  (comment "7 in cohort - 5 not yet seen"))

(defskeleton wonthull2
  (vars (x1 x3 x1-0 text) (a a-0 name))
  (defstrand init 2 (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 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand init 1) x3 (0 1)
    (enc x3 x3 (pubk a)) (enc x1-0 x3 (pubk a)))
  (traces
    ((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 12)
  (parent 11)
  (unrealized (1 0))
  (origs (x3 (0 0)))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton wonthull2
  (vars (x1 x3 x1-0 y3 text) (a a-0 name))
  (defstrand init 2 (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 x1-0) (y3 y3) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x1-0)
  (operation nonce-test (added-strand resp 2) x1-0 (0 1)
    (enc x1-0 x3 (pubk a)) (enc x1-0 x1-0 (pubk a)))
  (traces
    ((send (cat (enc x1-0 x1-0 (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 x1-0 (pubk a)))
      (send (enc "okay" y3 x1-0 (pubk a)))))
  (label 13)
  (parent 11)
  (seen 21)
  (unrealized (0 1))
  (comment "8 in cohort - 5 not yet seen"))

(defskeleton wonthull2
  (vars (x3 text) (a name))
  (defstrand init 2 (x1 x3) (x2 x3) (x3 x3) (x4 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (displaced 2 1 resp 2) x1 (0 1)
    (enc x1 x3 (pubk a-0)) (enc x1 x1 (pubk a-0)))
  (traces
    ((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)))))
  (label 14)
  (parent 11)
  (seen 18)
  (unrealized)
  (origs (x3 (0 0)))
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (x1 x3 x1-0 x3-0 y3 text) (a a-0 name))
  (defstrand init 2 (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) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x3-0)
  (operation nonce-test (added-strand resp 2) x3-0 (0 1)
    (enc x1-0 x3-0 (pubk a)) (enc x3-0 x3 (pubk a)))
  (traces
    ((send (cat (enc x1-0 x3-0 (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 11)
  (seen 21 22 24 26)
  (unrealized (0 1))
  (comment "8 in cohort - 3 not yet seen"))

(defskeleton wonthull2
  (vars (x1 x3 x1-0 text) (a name))
  (defstrand init 2 (x1 x1-0) (x2 x3) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (displaced 2 1 resp 2) x3-0 (0 1)
    (enc x1-0 x3-0 (pubk a-0)) (enc x3-0 x3 (pubk a-0)))
  (traces
    ((send (cat (enc x1-0 x1 (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 16)
  (parent 11)
  (seen 14 18 23 27)
  (unrealized (0 1))
  (origs (x1 (0 0)))
  (comment "7 in cohort - 0 not yet seen"))

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

(defskeleton wonthull2
  (vars (x3 y3 text) (a a-0 name))
  (defstrand init 2 (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 y3) (y3 y3) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (x1 y3) (x1-0 y3)) y3 (0 1)
    (enc "okay" y3 y3 (pubk a)) (enc y3 x3 (pubk a))
    (enc y3 y3 (pubk a)))
  (traces
    ((send (cat (enc y3 y3 (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 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 20)
  (parent 13)
  (seen 34)
  (unrealized (1 0))
  (comment "6 in cohort - 5 not yet seen"))

(defskeleton wonthull2
  (vars (x1 x3 y3 text) (a a-0 name))
  (defstrand init 2 (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 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand init 1) x3 (0 1)
    (enc "okay" y3 x3 (pubk a)) (enc x3 x3 (pubk a)))
  (traces
    ((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 21)
  (parent 13)
  (seen 24 35)
  (unrealized (1 0))
  (comment "4 in cohort - 2 not yet seen"))

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

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

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

(defskeleton wonthull2
  (vars (x3 x1 y3 text) (a a-0 name))
  (defstrand init 2 (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 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (x1-0 y3) (x3-0 y3)) y3 (0 1)
    (enc "okay" y3 y3 (pubk a)) (enc x1 y3 (pubk a))
    (enc y3 x3 (pubk a)))
  (traces
    ((send (cat (enc x1 y3 (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 25)
  (parent 15)
  (seen 32 45)
  (unrealized (1 0))
  (comment "6 in cohort - 4 not yet seen"))

(defskeleton wonthull2
  (vars (x1 x3 x1-0 y3 text) (a a-0 name))
  (defstrand init 2 (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) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand init 1) x3 (0 1)
    (enc "okay" y3 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1-0 x3 (pubk a)))
  (traces
    ((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 26)
  (parent 15)
  (seen 19)
  (unrealized (1 0))
  (comment "5 in cohort - 3 not yet seen"))

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

(defskeleton wonthull2
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 2 (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 0) (2 0)) ((1 1) (0 1)) ((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 "okay" y3 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1 x3 (pubk a)))
  (traces
    ((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 28)
  (parent 19)
  (seen 17)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 2 (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 0) (2 0)) ((1 1) (0 1)) ((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 "okay" y3 x3 (pubk a)) (enc x3 x3 (pubk a))
    (enc x1 x3 (pubk a)))
  (traces
    ((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 18)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

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

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

(defskeleton wonthull2
  (vars (x3 y3 y3-0 text) (a a-0 name))
  (defstrand init 2 (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 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3-0) (a a))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (added-strand resp 2) y3 (1 0)
    (enc y3 x3 (pubk a)) (enc y3 y3 (pubk a)))
  (traces
    ((send (cat (enc y3 y3 (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 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 33)
  (parent 20)
  (seen 51 52 56)
  (unrealized (1 0))
  (comment "5 in cohort - 2 not yet seen"))

(defskeleton wonthull2
  (vars (x3 y3 text) (a a-0 name))
  (defstrand init 2 (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 y3) (y3 y3) (a a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (displaced 3 2 resp 2) y3 (1 0)
    (enc y3 x3 (pubk a)) (enc y3 y3 (pubk a)))
  (traces
    ((send (cat (enc y3 y3 (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 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 34)
  (parent 20)
  (seen 53 56)
  (unrealized (1 0))
  (comment "3 in cohort - 1 not yet seen"))

(defskeleton wonthull2
  (vars (x1 x3 y3 text) (a a-0 name))
  (defstrand init 2 (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 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand resp 2) x3 (1 0)
    (enc x3 x3 (pubk a)))
  (traces
    ((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 35)
  (parent 21)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

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

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

(defskeleton wonthull2
  (vars (x3 y3 y3-0 text) (a a-0 name))
  (defstrand init 2 (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 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 0) (1 0)) ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (x1 y3) (x1-0 y3)) y3 (0 1)
    (enc "okay" y3 y3 (pubk a)) (enc "okay" y3-0 y3 (pubk a))
    (enc y3 x3 (pubk a)) (enc y3 y3 (pubk a)))
  (traces
    ((send (cat (enc y3 y3 (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 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 38)
  (parent 22)
  (seen 31 62 64 68)
  (unrealized (1 0))
  (comment "9 in cohort - 4 not yet seen"))

(defskeleton wonthull2
  (vars (x1 x3 y3 y3-0 text) (a a-0 name))
  (defstrand init 2 (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) (1 0)) ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (added-strand init 1) x3 (0 1)
    (enc "okay" y3 x3 (pubk a)) (enc "okay" y3-0 x3 (pubk a))
    (enc x3 x3 (pubk a)))
  (traces
    ((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 39)
  (parent 22)
  (seen 24 35 70)
  (unrealized (1 0))
  (comment "6 in cohort - 1 not yet seen"))

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

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

(defskeleton wonthull2
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 2 (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 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (a-0 a)) y3 (1 0)
    (enc x1 y3 (pubk a)) (enc y3 x3 (pubk a)))
  (traces
    ((send (cat (enc x1 y3 (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 42)
  (parent 25)
  (seen 18)
  (unrealized)
  (shape)
  (maps ((0 1) ((x1 y3) (x3 x3) (a a) (x1-0 x1) (x3-0 y3) (a-0 a))))
  (origs (y3 (0 0)))
  (comment "1 in cohort - 0 not yet seen"))

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

(defskeleton wonthull2
  (vars (x3 x1 y3 y3-0 text) (a a-0 name))
  (defstrand init 2 (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) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (added-strand resp 2) y3 (1 0)
    (enc x1 y3 (pubk a)) (enc y3 x3 (pubk a)))
  (traces
    ((send (cat (enc x1 y3 (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 44)
  (parent 25)
  (seen 51 72 75)
  (unrealized (1 0))
  (comment "5 in cohort - 2 not yet seen"))

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

(defskeleton wonthull2
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 2 (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 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (x1-0 x1) (a-0 a)) x3 (1 0)
    (enc x3 x3 (pubk a)) (enc x1 x3 (pubk a)))
  (traces
    ((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 46)
  (parent 26)
  (seen 17)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (x3 x1 y3 text) (a name))
  (defstrand init 2 (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 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (x1-0 x3) (a-0 a)) x3 (1 0)
    (enc x3 x3 (pubk a)) (enc x1 x3 (pubk a)))
  (traces
    ((send (cat (enc x1 x3 (pubk a)) (enc x3 x3 (pubk a))))
      (recv (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" y3 x3 (pubk a)))))
  (label 47)
  (parent 26)
  (seen 18)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

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

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

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

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

(defskeleton wonthull2
  (vars (x3 y3 y3-0 text) (a a-0 name))
  (defstrand init 2 (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 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((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 "okay" y3-0 y3 (pubk a)) (enc y3 x3 (pubk a))
    (enc y3 y3 (pubk a)))
  (traces
    ((send (cat (enc y3 y3 (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 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 53)
  (parent 31)
  (seen 83)
  (unrealized (1 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton wonthull2
  (vars (y3 text) (a name))
  (defstrand init 2 (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 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (a-0 a)) y3 (1 0)
    (enc "okay" y3 y3 (pubk a)) (enc y3 y3 (pubk a)))
  (traces
    ((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 54)
  (parent 32)
  (seen 14)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

(defskeleton wonthull2
  (vars (x3 y3 y3-0 text) (a a-0 name))
  (defstrand init 2 (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 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3-0) (a a))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((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 "okay" y3-0 y3 (pubk a)) (enc y3 x3 (pubk a))
    (enc y3 y3 (pubk a)))
  (traces
    ((send (cat (enc y3 y3 (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 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 56)
  (parent 33)
  (seen 83)
  (unrealized (1 0))
  (comment "2 in cohort - 1 not yet seen"))

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

(defskeleton wonthull2
  (vars (x3 y3 text) (a name))
  (defstrand init 2 (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 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation nonce-test (contracted (x1 x3) (a-0 a)) x3 (1 0)
    (enc "okay" y3 x3 (pubk a)) (enc x3 x3 (pubk a)))
  (traces
    ((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 58)
  (parent 35)
  (seen 14)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (x1 y3 y3-0 text) (a a-0 name))
  (defstrand init 2 (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) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((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 "okay" y3 y3 (pubk a)) (enc y3 y3 (pubk a)))
  (traces
    ((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 59)
  (parent 36)
  (seen 81)
  (unrealized (1 0))
  (comment "1 in cohort - 0 not yet seen"))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(defskeleton wonthull2
  (vars (x1 y3 text) (a name))
  (defstrand init 2 (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 0) (2 0)) ((1 1) (0 1)) ((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 "okay" y3 y3 (pubk a)) (enc x1 y3 (pubk a))
    (enc y3 y3 (pubk a)))
  (traces
    ((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 77)
  (parent 48)
  (seen 18)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (x1 y3 text) (a name))
  (defstrand init 2 (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 0) (2 0)) ((1 1) (0 1)) ((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 "okay" y3 y3 (pubk a)) (enc x1 y3 (pubk a))
    (enc y3 y3 (pubk a)))
  (traces
    ((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 78)
  (parent 48)
  (seen 17)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (x1 x1-0 y3 y3-0 text) (a a-0 name))
  (defstrand init 2 (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) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((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 "okay" y3 y3 (pubk a)) (enc x1-0 y3 (pubk a))
    (enc y3 y3 (pubk a)))
  (traces
    ((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 79)
  (parent 48)
  (unrealized (1 0))
  (comment "2 in cohort - 2 not yet seen"))

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

(defskeleton wonthull2
  (vars (y3 y3-0 text) (a name))
  (defstrand init 2 (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 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((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 "okay" y3 y3 (pubk a)) (enc "okay" y3-0 y3 (pubk a))
    (enc y3 y3 (pubk a)))
  (traces
    ((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 81)
  (parent 51)
  (seen 58)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

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

(defskeleton wonthull2
  (vars (x3 y3 y3-0 text) (a name))
  (defstrand init 2 (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 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-0) (a a))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((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 "okay" y3 y3 (pubk a)) (enc "okay" y3-0 y3 (pubk a))
    (enc y3 x3 (pubk a)) (enc y3 y3 (pubk a)))
  (traces
    ((send (cat (enc y3 y3 (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 y3 (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 53)
  (seen 57)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (x3 y3 y3-0 text) (a name))
  (defstrand init 2 (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 y3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3-0) (a a))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((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 "okay" y3 y3 (pubk a)) (enc "okay" y3-0 y3 (pubk a))
    (enc y3 x3 (pubk a)) (enc y3 y3 (pubk a)))
  (traces
    ((send (cat (enc y3 y3 (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 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 56)
  (seen 57)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (x3 y3 text) (a name))
  (defstrand init 2 (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 0) (1 0)) ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation generalization deleted (2 0))
  (traces
    ((send (cat (enc y3 y3 (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 86)
  (parent 60)
  (seen 42)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(defskeleton wonthull2
  (vars (x3 y3 y3-0 text) (a a-0 name))
  (defstrand init 2 (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 y3) (y3 y3) (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 0) (2 0)) ((0 0) (3 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (added-strand resp 2) y3 (1 0)
    (enc "okay" y3 y3 (pubk a)) (enc y3 x3 (pubk a))
    (enc y3 y3 (pubk a)))
  (traces
    ((send (cat (enc y3 y3 (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 y3 (pubk a))) (send (enc "okay" y3 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 101)
  (parent 69)
  (seen 119)
  (unrealized (1 0))
  (comment "2 in cohort - 1 not yet seen"))

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

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

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

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

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

(defskeleton wonthull2
  (vars (x1 y3 y3-0 text) (a name))
  (defstrand init 2 (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 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((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 "okay" y3 y3 (pubk a)) (enc "okay" y3-0 y3 (pubk a))
    (enc x1 y3 (pubk a)) (enc y3 y3 (pubk a)))
  (traces
    ((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 107)
  (parent 79)
  (seen 29)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (x1 y3 y3-0 text) (a name))
  (defstrand init 2 (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 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((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 "okay" y3 y3 (pubk a)) (enc "okay" y3-0 y3 (pubk a))
    (enc x1 y3 (pubk a)) (enc y3 y3 (pubk a)))
  (traces
    ((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 108)
  (parent 79)
  (seen 28)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

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

(defskeleton wonthull2
  (vars (x3 y3 y3-0 text) (a name))
  (defstrand init 2 (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 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (0 1))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation generalization deleted (2 0))
  (traces
    ((send (cat (enc y3 y3 (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 111)
  (parent 87)
  (seen 86)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

(defskeleton wonthull2
  (vars (x3 y3 y3-0 text) (a name))
  (defstrand init 2 (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 y3) (y3 y3) (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 0) (2 0)) ((0 0) (3 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (1 0)) ((3 1) (0 1)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (a-0 a)) y3 (1 0)
    (enc "okay" y3 y3 (pubk a)) (enc "okay" y3-0 y3 (pubk a))
    (enc y3 x3 (pubk a)) (enc y3 y3 (pubk a)))
  (traces
    ((send (cat (enc y3 y3 (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 y3 (pubk a))) (send (enc "okay" y3 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 113)
  (parent 90)
  (seen 111)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

(defskeleton wonthull2
  (vars (x3 y3 text) (a name))
  (defstrand init 2 (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 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation generalization deleted (2 0))
  (traces
    ((send (cat (enc y3 y3 (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 115)
  (parent 91)
  (seen 86)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

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

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

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

(defskeleton wonthull2
  (vars (x3 y3 y3-0 text) (a name))
  (defstrand init 2 (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 y3) (y3 y3) (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 0) (2 0)) ((0 0) (3 0)) ((0 0) (4 0)) ((1 1) (0 1))
    ((2 1) (0 1)) ((3 1) (1 0)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation nonce-test (contracted (a-0 a)) y3 (1 0)
    (enc "okay" y3 y3 (pubk a)) (enc "okay" y3-0 y3 (pubk a))
    (enc y3 x3 (pubk a)) (enc y3 y3 (pubk a)))
  (traces
    ((send (cat (enc y3 y3 (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 y3 (pubk a))) (send (enc "okay" y3 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 120)
  (parent 101)
  (seen 122)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

(defskeleton wonthull2
  (vars (x3 y3 y3-0 text) (a name))
  (defstrand init 2 (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 0) (2 0)) ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3)
  (operation generalization deleted (2 0))
  (traces
    ((send (cat (enc y3 y3 (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 122)
  (parent 112)
  (seen 115)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

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

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

(comment "Nothing left to do")