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

(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 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 1)
  (parent 0)
  (unrealized (0 1))
  (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 2)
  (parent 0)
  (seen 4)
  (unrealized (0 1))
  (comment "3 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 3)
  (parent 1)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (x1 x1) (x2 x2) (x3 y3) (x4 y3))))
  (origs (y3 (0 0))))

(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 x2) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (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 x2 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 4)
  (parent 1)
  (unrealized (0 1))
  (comment "4 in cohort - 4 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 5)
  (parent 2)
  (unrealized)
  (comment "1 in cohort - 1 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))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 6)
  (parent 2)
  (seen 10)
  (unrealized (0 1))
  (comment "2 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 x2) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (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 x2 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 y3 (pubk a))) (send (enc "okay" y3-0 y3 (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-0) (x2 x2) (x3 y3-0) (x4 y3-0) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 x2) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3-0) (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 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 x2 (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 8)
  (parent 4)
  (seen 5)
  (unrealized)
  (comment "1 in cohort - 0 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 x2) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x2) (y3 x1) (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 (added-strand resp 2) x1 (0 1)
    (enc "okay" y3 x1 (pubk a)) (enc "okay" y3-0 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 x2 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x2 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 9)
  (parent 4)
  (unrealized (0 1))
  (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 x2) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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 (added-strand resp 2) x1 (0 1)
    (enc "okay" y3 x1 (pubk a)) (enc "okay" y3-0 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 x2 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 10)
  (parent 4)
  (unrealized (0 1))
  (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-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 11)
  (parent 5)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

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

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

(defskeleton wonthull2
  (vars (x1 x2 y3 y3-0 text) (a name))
  (defstrand init 2 (x1 x1) (x2 x2) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x2) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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 (contracted (x4 x1)) x1 (0 1)
    (enc "okay" x1 x1 (pubk a)) (enc "okay" y3 x1 (pubk a))
    (enc "okay" y3-0 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 x1 (pubk a))))
    ((recv (enc x1 x2 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 15)
  (parent 10)
  (seen 12)
  (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 16)
  (parent 11)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (x1 y3) (x2 x2) (x3 y3-0) (x4 y3))))
  (origs (y3 (0 0)) (y3-0 (0 0))))

(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 17)
  (unrealized (0 1))
  (origs (x3-0 (0 0)))
  (comment "4 in cohort - 4 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 (displaced 2 1 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 (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 18)
  (parent 17)
  (unrealized (1 0))
  (origs (x3 (0 0)))
  (comment "3 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 19)
  (parent 17)
  (seen 22)
  (unrealized (0 1))
  (origs (x1 (0 0)))
  (comment "3 in cohort - 2 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 20)
  (parent 17)
  (seen 26)
  (unrealized (0 1))
  (comment "4 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 21)
  (parent 17)
  (seen 25 29)
  (unrealized (0 1))
  (comment "5 in cohort - 3 not yet seen"))

(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 22)
  (parent 18)
  (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 (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 23)
  (parent 18)
  (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 (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 24)
  (parent 18)
  (unrealized (1 0))
  (comment "4 in cohort - 4 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 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 (added-strand resp 2) x1 (0 1)
    (enc "okay" x3 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 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a)))))
  (label 25)
  (parent 19)
  (unrealized (0 1))
  (comment "4 in cohort - 4 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 (added-strand resp 2) x1 (0 1)
    (enc "okay" x3 x1 (pubk a)) (enc x1 x3 (pubk a))
    (enc x1-0 x1 (pubk a)))
  (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 26)
  (parent 19)
  (seen 40)
  (unrealized (0 1))
  (comment "3 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) (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 27)
  (parent 20)
  (seen 42)
  (unrealized (1 0))
  (comment "4 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 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 (displaced 3 1 resp 2) x3-0 (0 1)
    (enc "okay" y3 x3-0 (pubk a)) (enc x1-0 x3-0 (pubk a))
    (enc x3-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 28)
  (parent 20)
  (seen 24 41)
  (unrealized (1 0))
  (comment "5 in cohort - 3 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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (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 x3 (pubk a))) (send (enc "okay" y3 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3-0 x1-0 (pubk a)))))
  (label 29)
  (parent 20)
  (seen 32 40)
  (unrealized (0 1))
  (comment "6 in cohort - 4 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 30)
  (parent 21)
  (seen 38)
  (unrealized (1 0))
  (comment "4 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))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 x1-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 x1-0 (pubk a)))
      (send (enc "okay" x1-0 x1-0 (pubk a)))))
  (label 31)
  (parent 21)
  (seen 51)
  (unrealized (0 1))
  (comment "3 in cohort - 2 not yet seen"))

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

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

(defskeleton wonthull2
  (vars (x1 y3 text) (a name))
  (defstrand init 2 (x1 x1) (x2 x1) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3) (a a))
  (precedes ((0 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 2 resp 2) x1 (0 1)
    (enc "okay" x3 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 x1 (pubk a))))
      (recv (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a)))))
  (label 39)
  (parent 25)
  (unrealized)
  (comment "1 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 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 (added-strand resp 2) x1 (0 1)
    (enc "okay" x3 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 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 25)
  (seen 39)
  (unrealized (0 1))
  (comment "5 in cohort - 4 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 (displaced 3 1 resp 2) x1-0 (0 1)
    (enc "okay" x3 x1-0 (pubk a)) (enc "okay" y3 x1-0 (pubk a))
    (enc x1-0 x3 (pubk a)) (enc x1 x1-0 (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 41)
  (parent 26)
  (seen 22)
  (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 (displaced 3 2 resp 2) x1-0 (0 1)
    (enc "okay" x3 x1-0 (pubk a)) (enc "okay" y3 x1-0 (pubk a))
    (enc x1-0 x3 (pubk a)) (enc x1 x1-0 (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 26)
  (unrealized)
  (shape)
  (maps ((0 1) ((x1 y3) (x3 x3) (a a) (x1-0 x1) (x3-0 y3) (a-0 a))))
  (origs (y3 (0 0))))

(defskeleton 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 43)
  (parent 27)
  (unrealized (1 0))
  (comment "3 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 27)
  (seen 72)
  (unrealized (1 0))
  (comment "3 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 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 45)
  (parent 27)
  (seen 73 75)
  (unrealized (1 0))
  (comment "4 in cohort - 2 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 28)
  (seen 23)
  (unrealized)
  (comment "1 in cohort - 0 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))
  (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 (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))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a)))))
  (label 47)
  (parent 28)
  (seen 35)
  (unrealized (1 0))
  (comment "4 in cohort - 3 not yet seen"))

(defskeleton wonthull2
  (vars (x1 x1-0 y3 y3-0 text) (a a-0 name))
  (defstrand init 2 (x1 x1-0) (x2 x1-0) (x3 x1-0) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1-0) (y3 x1-0) (a a-0))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3-0) (a a))
  (precedes ((0 0) (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-0)
  (operation nonce-test (added-strand resp 2) x1-0 (1 0)
    (enc x1-0 x1-0 (pubk a)))
  (traces
    ((send (cat (enc x1-0 x1-0 (pubk a)) (enc x1-0 x1-0 (pubk a))))
      (recv (enc "okay" x1-0 x1 (pubk a))))
    ((recv (enc x1 x1-0 (pubk a-0)))
      (send (enc "okay" x1-0 x1 (pubk a-0))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3-0 x1-0 (pubk a)))))
  (label 48)
  (parent 28)
  (seen 63 64)
  (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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (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 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 49)
  (parent 29)
  (seen 45 70)
  (unrealized (1 0))
  (comment "5 in cohort - 3 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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (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 x3 (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 50)
  (parent 29)
  (seen 55 69)
  (unrealized (1 0))
  (comment "5 in cohort - 3 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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 x1-0) (a a))
  (precedes ((0 0) (1 0)) ((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) (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 "okay" y3-0 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 x3 (pubk a))) (send (enc "okay" y3 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" x1-0 x1-0 (pubk a)))))
  (label 51)
  (parent 29)
  (seen 57)
  (unrealized (0 1))
  (comment "2 in cohort - 1 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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x3) (y3 x1-0) (a a))
  (precedes ((0 0) (1 0)) ((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) (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 "okay" y3-0 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 x3 (pubk a))) (send (enc "okay" y3 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x3 (pubk a)))
      (send (enc "okay" x1-0 x1-0 (pubk a)))))
  (label 52)
  (parent 29)
  (seen 57)
  (unrealized (0 1))
  (comment "2 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))
  (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 53)
  (parent 30)
  (unrealized (1 0))
  (comment "3 in cohort - 3 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 54)
  (parent 30)
  (seen 90)
  (unrealized (1 0))
  (comment "3 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) (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 55)
  (parent 30)
  (seen 91 93)
  (unrealized (1 0))
  (comment "4 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 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a-0))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (precedes ((0 0) (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 (contracted (x1-0 x1)) x1 (0 1)
    (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-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 56)
  (parent 31)
  (seen 37 54)
  (unrealized (1 0))
  (comment "4 in cohort - 2 not yet seen"))

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

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

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

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

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

(defskeleton wonthull2
  (vars (x1 text) (a name))
  (defstrand init 2 (x1 x1) (x2 x1) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation generalization deleted (2 0))
  (traces
    ((send (cat (enc x1 x1 (pubk a)) (enc x1 x1 (pubk a))))
      (recv (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 66)
  (parent 39)
  (seen 22)
  (unrealized)
  (origs (x1 (0 0)))
  (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 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (precedes ((0 0) (1 0)) ((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) (0 1)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (0 1)
    (enc "okay" x3 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 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 67)
  (parent 40)
  (seen 69)
  (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 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (a a))
  (precedes ((0 0) (1 0)) ((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) (0 1)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (0 1)
    (enc "okay" x3 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 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 68)
  (parent 40)
  (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) (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 (displaced 4 2 resp 2) x1 (0 1)
    (enc "okay" x3 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 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 69)
  (parent 40)
  (seen 38)
  (unrealized)
  (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 (displaced 4 3 resp 2) x1 (0 1)
    (enc "okay" x3 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 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 70)
  (parent 40)
  (unrealized)
  (comment "1 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 71)
  (parent 43)
  (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 (added-strand resp 2) 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-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 72)
  (parent 43)
  (unrealized (1 0))
  (comment "2 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 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 (added-strand resp 2) x1 (1 0)
    (enc "okay" x1 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 107)
  (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 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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (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 x3 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 75)
  (parent 44)
  (seen 107)
  (unrealized (1 0))
  (comment "3 in cohort - 2 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 76)
  (parent 45)
  (seen 105)
  (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 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 x1) (y3 x1) (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 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 77)
  (parent 45)
  (seen 110)
  (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 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 (x1-0 x3) (a-0 a)) x3 (1 0)
    (enc "okay" x3 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))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a)))))
  (label 78)
  (parent 47)
  (seen 100)
  (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 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (precedes ((0 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 (x1-0 x1) (a-0 a)) x3 (1 0)
    (enc "okay" x3 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))))
    ((recv (enc x3 x3 (pubk a))) (send (enc "okay" x3 x3 (pubk a)))))
  (label 79)
  (parent 47)
  (seen 101)
  (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 x1-0) (x3 x1-0) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1-0) (y3 x1-0) (a a-0))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 x1-0) (a a))
  (defstrand resp 2 (y1 x1-0) (y2 x1-0) (y3 y3-0) (a a))
  (precedes ((0 0) (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-0)
  (operation nonce-test (added-strand resp 2) x1-0 (1 0)
    (enc "okay" x1-0 x1-0 (pubk a)) (enc x1-0 x1-0 (pubk a)))
  (traces
    ((send (cat (enc x1-0 x1-0 (pubk a)) (enc x1-0 x1-0 (pubk a))))
      (recv (enc "okay" x1-0 x1 (pubk a))))
    ((recv (enc x1 x1-0 (pubk a-0)))
      (send (enc "okay" x1-0 x1 (pubk a-0))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" x1-0 x1-0 (pubk a))))
    ((recv (enc x1-0 x1-0 (pubk a)))
      (send (enc "okay" y3-0 x1-0 (pubk a)))))
  (label 80)
  (parent 47)
  (seen 102)
  (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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (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 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 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 81)
  (parent 49)
  (seen 77)
  (unrealized (1 0))
  (comment "3 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 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)) ((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 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 82)
  (parent 49)
  (seen 73)
  (unrealized (1 0))
  (comment "3 in cohort - 2 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 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)) ((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 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 83)
  (parent 49)
  (seen 75 113 115)
  (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 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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3-0) (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) (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 x3 (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))))
    ((recv (enc y3-0 x3 (pubk a)))
      (send (enc "okay" y3-0 y3-0 (pubk a)))))
  (label 84)
  (parent 50)
  (seen 95)
  (unrealized (1 0))
  (comment "3 in cohort - 2 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 x3) (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) (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 x3 (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 85)
  (parent 50)
  (seen 91)
  (unrealized (1 0))
  (comment "3 in cohort - 2 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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (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 x3 (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))))
    ((recv (enc y3-0 y3-0 (pubk a)))
      (send (enc "okay" y3-1 y3-0 (pubk a)))))
  (label 86)
  (parent 50)
  (seen 93 118 120)
  (unrealized (1 0))
  (comment "4 in cohort - 1 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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (precedes ((0 0) (1 0)) ((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) (0 1)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (contracted (x1-0 x1)) x1 (0 1)
    (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-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 87)
  (parent 51)
  (seen 67 86 97)
  (unrealized (1 0))
  (comment "5 in cohort - 2 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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (a a))
  (precedes ((0 0) (1 0)) ((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) (0 1)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (contracted (x1-0 x1)) x1 (0 1)
    (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-0))) (send (enc "okay" x3 x1 (pubk a-0))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 88)
  (parent 52)
  (seen 68 83)
  (unrealized (1 0))
  (comment "5 in cohort - 3 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 89)
  (parent 53)
  (seen 38)
  (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 (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 y3 (pubk a))) (send (enc "okay" y3-0 y3 (pubk a)))))
  (label 90)
  (parent 53)
  (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) (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 (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-0 y3 (pubk a)))))
  (label 91)
  (parent 53)
  (seen 128)
  (unrealized (1 0))
  (comment "2 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 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 92)
  (parent 54)
  (seen 38)
  (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 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)) ((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 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 93)
  (parent 54)
  (seen 128)
  (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) (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 94)
  (parent 55)
  (seen 38)
  (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-0) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (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 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 95)
  (parent 55)
  (seen 131)
  (unrealized (1 0))
  (comment "2 in cohort - 1 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 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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 (displaced 4 3 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 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 96)
  (parent 56)
  (seen 90)
  (unrealized (1 0))
  (comment "3 in cohort - 2 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 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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) (0 1)) ((4 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 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 97)
  (parent 56)
  (seen 93 134)
  (unrealized (1 0))
  (comment "4 in cohort - 2 not yet seen"))

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

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

(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))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation generalization deleted (2 0))
  (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" x3 x3 (pubk a)))))
  (label 100)
  (parent 60)
  (seen 22)
  (unrealized)
  (comment "1 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))
  (defstrand resp 2 (y1 x3) (y2 x3) (y3 x3) (a a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x3)
  (operation generalization deleted (2 0))
  (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" x3 x3 (pubk a)))))
  (label 101)
  (parent 61)
  (seen 23)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (x1 y3 text) (a name))
  (defstrand init 2 (x1 x1) (x2 x1) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (precedes ((0 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 (x1-0 x1) (a-0 a) (y3-0 y3)) x1
    (1 0) (enc "okay" x1 x1 (pubk a)) (enc "okay" y3 x1 (pubk a))
    (enc x1 x1 (pubk a)))
  (traces
    ((send (cat (enc x1 x1 (pubk a)) (enc x1 x1 (pubk a))))
      (recv (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 102)
  (parent 62)
  (seen 137)
  (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) (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 103)
  (parent 65)
  (unrealized)
  (comment "1 in cohort - 1 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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (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 generalization deleted (2 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 x3 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 104)
  (parent 68)
  (seen 105)
  (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 105)
  (parent 70)
  (seen 42)
  (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 72)
  (seen 71)
  (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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (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 (added-strand resp 2) 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-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 x3 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 107)
  (parent 72)
  (unrealized (1 0))
  (comment "1 in cohort - 1 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 108)
  (parent 73)
  (unrealized)
  (comment "1 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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (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 x3 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 109)
  (parent 75)
  (seen 76)
  (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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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 x1)
  (operation nonce-test (added-strand 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 x3 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 110)
  (parent 75)
  (unrealized (1 0))
  (comment "1 in cohort - 1 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))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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" 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))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 111)
  (parent 77)
  (seen 127)
  (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 y3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (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 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 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 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 112)
  (parent 81)
  (seen 133)
  (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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (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) (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 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 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 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-1 y3 (pubk a)))))
  (label 113)
  (parent 81)
  (seen 110)
  (unrealized (1 0))
  (comment "2 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 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)) ((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 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 114)
  (parent 82)
  (seen 140)
  (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 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)) ((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 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 115)
  (parent 82)
  (seen 107)
  (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 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)) ((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 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 116)
  (parent 83)
  (unrealized)
  (comment "1 in cohort - 1 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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3-0) (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) (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-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 x3 (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))))
    ((recv (enc y3-0 x3 (pubk a)))
      (send (enc "okay" y3-0 y3-0 (pubk a)))))
  (label 117)
  (parent 84)
  (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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 x3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (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) (0 1)) ((4 1) (1 0))
    ((5 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig y3-0)
  (operation nonce-test (added-strand resp 2) 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-0)))
      (send (enc "okay" x3 y3-0 (pubk a-0))))
    ((recv (enc y3-0 x3 (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))))
    ((recv (enc y3-0 x3 (pubk a)))
      (send (enc "okay" y3-0 y3-0 (pubk a))))
    ((recv (enc y3-0 y3-0 (pubk a)))
      (send (enc "okay" y3-1 y3-0 (pubk a)))))
  (label 118)
  (parent 84)
  (seen 131)
  (unrealized (1 0))
  (comment "2 in cohort - 1 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 x3) (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) (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 x3 (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 119)
  (parent 85)
  (seen 89)
  (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-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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (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 (added-strand resp 2) 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-0)))
      (send (enc "okay" x3 y3-0 (pubk a-0))))
    ((recv (enc y3-0 x3 (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))))
    ((recv (enc y3-0 y3-0 (pubk a)))
      (send (enc "okay" y3-1 y3-0 (pubk a)))))
  (label 120)
  (parent 85)
  (seen 128)
  (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-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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (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 x3 (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))))
    ((recv (enc y3-0 y3-0 (pubk a)))
      (send (enc "okay" y3-1 y3-0 (pubk a)))))
  (label 121)
  (parent 86)
  (seen 92)
  (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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (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) (0 1)) ((4 1) (0 1))
    ((5 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" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 122)
  (parent 87)
  (seen 118 136)
  (unrealized (1 0))
  (comment "3 in cohort - 1 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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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 x1)
  (operation nonce-test (displaced 5 4 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" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 123)
  (parent 87)
  (seen 120 134)
  (unrealized (1 0))
  (comment "3 in cohort - 1 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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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) (0 1)) ((4 1) (0 1))
    ((5 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" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 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" x1 x1 (pubk a)))))
  (label 124)
  (parent 88)
  (seen 113)
  (unrealized (1 0))
  (comment "3 in cohort - 2 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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (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) (0 1)) ((4 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" y3 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-0 x1 (pubk a)))))
  (label 125)
  (parent 88)
  (seen 75 151)
  (unrealized (1 0))
  (comment "4 in cohort - 2 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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (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 x1)
  (operation nonce-test (displaced 5 4 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" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 126)
  (parent 88)
  (seen 115 153)
  (unrealized (1 0))
  (comment "3 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 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 127)
  (parent 90)
  (seen 89)
  (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 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)) ((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 (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 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 128)
  (parent 90)
  (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 129)
  (parent 91)
  (seen 89)
  (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 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)) ((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 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 130)
  (parent 93)
  (seen 94)
  (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 y3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-1) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (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-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 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))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 131)
  (parent 93)
  (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))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (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-0 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 132)
  (parent 95)
  (unrealized)
  (comment "1 in cohort - 1 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 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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" x1 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 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 133)
  (parent 96)
  (seen 89)
  (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 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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" x1 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 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 134)
  (parent 96)
  (seen 128)
  (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 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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) (0 1)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (contracted (a-0 a)) x1 (1 0)
    (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 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 135)
  (parent 97)
  (seen 94)
  (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 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (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) (0 1)) ((4 1) (1 0))
    ((5 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (1 0)
    (enc "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 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 136)
  (parent 97)
  (seen 131)
  (unrealized (1 0))
  (comment "2 in cohort - 1 not yet seen"))

(defskeleton wonthull2
  (vars (x1 text) (a name))
  (defstrand init 2 (x1 x1) (x2 x1) (x3 x1) (x4 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation generalization deleted (2 0))
  (traces
    ((send (cat (enc x1 x1 (pubk a)) (enc x1 x1 (pubk a))))
      (recv (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 137)
  (parent 99)
  (seen 66)
  (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 138)
  (parent 103)
  (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))))

(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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (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 x3 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 139)
  (parent 107)
  (seen 108)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton wonthull2
  (vars (x3 x1 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))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation generalization deleted (3 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 x3 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 140)
  (parent 108)
  (seen 105)
  (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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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 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 x3 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 141)
  (parent 110)
  (seen 155)
  (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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3) (y2 y3) (y3 y3) (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) (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-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 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 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3-1 y3 (pubk a)))))
  (label 142)
  (parent 113)
  (seen 158)
  (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 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)) ((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 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 143)
  (parent 115)
  (seen 157)
  (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 (3 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 144)
  (parent 116)
  (seen 105)
  (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 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 y3 (pubk a))) (send (enc "okay" y3 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 145)
  (parent 117)
  (seen 140)
  (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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 x3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (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) (0 1)) ((4 1) (1 0))
    ((5 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 x3 (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))))
    ((recv (enc y3-0 x3 (pubk a)))
      (send (enc "okay" y3-0 y3-0 (pubk a))))
    ((recv (enc y3-0 y3-0 (pubk a)))
      (send (enc "okay" y3-1 y3-0 (pubk a)))))
  (label 146)
  (parent 118)
  (unrealized)
  (comment "1 in cohort - 1 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 x3) (y3 y3) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3-0) (y2 y3-0) (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 x3 (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))))
    ((recv (enc y3-0 y3-0 (pubk a)))
      (send (enc "okay" y3-1 y3-0 (pubk a)))))
  (label 147)
  (parent 120)
  (seen 127)
  (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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (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) (0 1)) ((4 1) (0 1))
    ((5 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 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" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 148)
  (parent 122)
  (unrealized)
  (comment "1 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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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 x1)
  (operation nonce-test (contracted (a-0 a)) x1 (1 0)
    (enc "okay" x1 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" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 149)
  (parent 123)
  (seen 133)
  (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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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) (0 1)) ((4 1) (0 1))
    ((5 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 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" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 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" x1 x1 (pubk a)))))
  (label 150)
  (parent 124)
  (seen 112)
  (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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((0 0) (4 0)) ((0 0) (5 0))
    ((1 1) (0 1)) ((2 1) (0 1)) ((3 1) (0 1)) ((4 1) (1 0))
    ((5 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (added-strand resp 2) x1 (1 0)
    (enc "okay" x1 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" y3 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" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 151)
  (parent 124)
  (seen 110)
  (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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (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) (0 1)) ((4 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (contracted (a-0 a)) x1 (1 0)
    (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" y3 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-0 x1 (pubk a)))))
  (label 152)
  (parent 125)
  (seen 76)
  (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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (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 (displaced 5 3 resp 2) x1 (1 0)
    (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" y3 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-0 x1 (pubk a)))))
  (label 153)
  (parent 125)
  (seen 107)
  (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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (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 x1)
  (operation nonce-test (contracted (a-0 a)) x1 (1 0)
    (enc "okay" x1 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" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 154)
  (parent 126)
  (seen 114)
  (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 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)) ((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 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 155)
  (parent 128)
  (seen 129)
  (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 y3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3-1) (a a))
  (defstrand resp 2 (y1 y3) (y2 x3) (y3 y3) (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 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))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 156)
  (parent 131)
  (seen 139)
  (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-0) (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) (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-0 y3 (pubk a))))
    ((recv (enc y3 x3 (pubk a))) (send (enc "okay" y3 y3 (pubk a)))))
  (label 157)
  (parent 132)
  (seen 140)
  (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 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (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" x1 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 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 158)
  (parent 134)
  (seen 129)
  (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 x1) (y3 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 y3-0) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (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) (0 1)) ((4 1) (1 0))
    ((5 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (contracted (a-0 a)) x1 (1 0)
    (enc "okay" x1 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 x1 (pubk a))) (send (enc "okay" y3 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 159)
  (parent 136)
  (seen 132)
  (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 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 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 160)
  (parent 146)
  (seen 108)
  (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 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 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (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 x1)
  (operation generalization deleted (2 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 x1 (pubk a))) (send (enc "okay" x1 x1 (pubk a))))
    ((recv (enc x1 x3 (pubk a))) (send (enc "okay" x1 x1 (pubk a)))))
  (label 161)
  (parent 148)
  (seen 145)
  (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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (y3 y3-0) (a a))
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((0 0) (4 0)) ((0 0) (5 0))
    ((1 1) (0 1)) ((2 1) (0 1)) ((3 1) (0 1)) ((4 1) (1 0))
    ((5 1) (1 0)))
  (non-orig (privk a))
  (uniq-orig x1)
  (operation nonce-test (contracted (a-0 a)) x1 (1 0)
    (enc "okay" x1 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" y3 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" x1 x1 (pubk a))))
    ((recv (enc x1 x1 (pubk a))) (send (enc "okay" y3-0 x1 (pubk a)))))
  (label 162)
  (parent 151)
  (seen 111)
  (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 y3) (a a))
  (defstrand resp 2 (y1 x1) (y2 x3) (y3 x1) (a a))
  (defstrand resp 2 (y1 x1) (y2 x1) (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" x1 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" y3 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-0 x1 (pubk a)))))
  (label 163)
  (parent 153)
  (seen 108)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")