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

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

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

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

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

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

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

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

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

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

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

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

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

(comment "Nothing left to do")

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(comment "Nothing left to do")