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

(defprotocol nsl3 basic
  (defrole init
    (vars (a b c name) (na0 na1 nb0 nb1 nc0 nc1 text))
    (trace (send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    (uniq-orig na0 na1))
  (defrole mid
    (vars (a b c name) (na0 na1 nb0 nb1 nc0 nc1 text))
    (trace (recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    (uniq-orig nb0 nb1))
  (defrole resp
    (vars (a b c name) (na0 na1 nb0 nb1 nc0 nc1 text))
    (trace
      (recv
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    (uniq-orig nc0 nc1)))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc0 nc1 text) (a b c name))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1)
  (traces
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b)))))
  (label 0)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton nsl3
  (vars (na1 nb0 nb1 nc0 nc1 nb0-0 nb1-0 text) (a b c name))
  (defstrand init 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na1) (na1 na1) (nb0 nb0-0) (nb1 nb1-0) (a a)
    (b b) (c c))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na1 nb0-0 nb1-0)
  (operation nonce-test (added-strand mid 2) na1 (0 1)
    (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
  (traces
    ((send (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1-0 b a (enc na1 a b (pubk c))
          (enc na1 nb0-0 b c (pubk a)) (pubk c)))))
  (label 1)
  (parent 0)
  (seen 3)
  (unrealized (0 1))
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc0 nc1 nb0-0 nb1-0 text) (a b c name))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na1) (nb0 nb0-0) (nb1 nb1-0) (a a)
    (b b) (c c))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nb0-0 nb1-0)
  (operation nonce-test (added-strand mid 2) na0 (0 1)
    (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
  (traces
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1-0 b a (enc na1 a b (pubk c))
          (enc na0 nb0-0 b c (pubk a)) (pubk c)))))
  (label 2)
  (parent 0)
  (seen 3 4)
  (unrealized (0 1))
  (comment "4 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (na1 nb0 nb1 nc0 nc1 nb0-0 nb1-0 nc0-0 nc1-0 text) (a b c name))
  (defstrand init 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na1) (na1 na1) (nb0 nb0-0) (nb1 nb1-0) (a a)
    (b b) (c c))
  (defstrand resp 2 (na0 na1) (na1 na1) (nb0 nb0-0) (nb1 nb1-0)
    (nc0 nc0-0) (nc1 nc1-0) (a a) (b b) (c c))
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na1 nb0-0 nb1-0 nc0-0 nc1-0)
  (operation nonce-test (added-strand resp 2) na1 (0 1)
    (enc na1 a c (enc na1 a b (pubk c)) (pubk b))
    (enc nb1-0 b a (enc na1 a b (pubk c)) (enc na1 nb0-0 b c (pubk a))
      (pubk c)))
  (traces
    ((send (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1-0 b a (enc na1 a b (pubk c))
          (enc na1 nb0-0 b c (pubk a)) (pubk c))))
    ((recv
       (enc nb1-0 b a (enc na1 a b (pubk c))
         (enc na1 nb0-0 b c (pubk a)) (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na1 nb0-0 b c (pubk a))
          (enc nb1-0 nc0-0 c a (pubk b)) (pubk a)))))
  (label 3)
  (parent 1)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc0 nc1 nb0-0 nb1-0 nc0-0 nc1-0 text)
    (a b c name))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na1) (nb0 nb0-0) (nb1 nb1-0) (a a)
    (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb0-0) (nb1 nb1-0)
    (nc0 nc0-0) (nc1 nc1-0) (a a) (b b) (c c))
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nb0-0 nb1-0 nc0-0 nc1-0)
  (operation nonce-test (added-strand resp 2) na0 (0 1)
    (enc na0 a c (enc na1 a b (pubk c)) (pubk b))
    (enc nb1-0 b a (enc na1 a b (pubk c)) (enc na0 nb0-0 b c (pubk a))
      (pubk c)))
  (traces
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1-0 b a (enc na1 a b (pubk c))
          (enc na0 nb0-0 b c (pubk a)) (pubk c))))
    ((recv
       (enc nb1-0 b a (enc na1 a b (pubk c))
         (enc na0 nb0-0 b c (pubk a)) (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na0 nb0-0 b c (pubk a))
          (enc nb1-0 nc0-0 c a (pubk b)) (pubk a)))))
  (label 4)
  (parent 2)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (na1 nb0 nb1 nc0 nc1 text) (a b c name))
  (defstrand init 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (a a) (b b)
    (c c))
  (defstrand resp 2 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na1 nb0 nb1 nc0 nc1)
  (operation nonce-test
    (contracted (nb0-0 nb0) (nb1-0 nb1) (nc0-0 nc0) (nc1-0 nc1)) na1
    (0 1)
    (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a))
    (enc na1 a c (enc na1 a b (pubk c)) (pubk b))
    (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
      (pubk c)))
  (traces
    ((send (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
          (pubk c))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))))
  (label 5)
  (parent 3)
  (seen 6)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc0 nc1 text) (a b c name))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (a a) (b b)
    (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nb0 nb1 nc0 nc1)
  (operation nonce-test
    (contracted (nb0-0 nb0) (nb1-0 nb1) (nc0-0 nc0) (nc1-0 nc1)) na0
    (0 1) (enc na0 a c (enc na1 a b (pubk c)) (pubk b))
    (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a))
    (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
      (pubk c)))
  (traces
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))))
  (label 6)
  (parent 4)
  (unrealized)
  (shape))

(comment "Nothing left to do")

(defprotocol nsl3 basic
  (defrole init
    (vars (a b c name) (na0 na1 nb0 nb1 nc0 nc1 text))
    (trace (send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    (uniq-orig na0 na1))
  (defrole mid
    (vars (a b c name) (na0 na1 nb0 nb1 nc0 nc1 text))
    (trace (recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    (uniq-orig nb0 nb1))
  (defrole resp
    (vars (a b c name) (na0 na1 nb0 nb1 nc0 nc1 text))
    (trace
      (recv
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    (uniq-orig nc0 nc1)))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc0 nc1 text) (a b c name))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nb0 nb1)
  (traces
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c)))))
  (label 7)
  (seen 8)
  (unrealized (0 2))
  (comment "5 in cohort - 2 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc0 nc1 nc0-0 nc1-0 text) (a b c name))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0-0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nb0 nb1 nc0-0 nc1-0)
  (operation nonce-test (added-strand resp 2) nb0 (0 2)
    (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0-0 c a (pubk b)) (pubk a)))))
  (label 8)
  (parent 7)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb1 nc0 nc1 nc0-0 nc1-0 text) (a b c name))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb1) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb1) (nb1 nb1) (nc0 nc0-0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nb1 nc0-0 nc1-0)
  (operation nonce-test (added-strand resp 2) nb1 (0 2)
    (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb1 b c (pubk a))
      (pubk c)))
  (traces
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb1 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb1 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb1 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na0 nb1 b c (pubk a))
          (enc nb1 nc0-0 c a (pubk b)) (pubk a)))))
  (label 9)
  (parent 7)
  (seen 10)
  (unrealized (0 2))
  (comment "4 in cohort - 0 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb1 nc0 nc1 nc0-0 nc1-0 text) (a b c name))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb1) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb1) (nb1 nb1) (nc0 nc0-0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb1) (nb1 nb1) (nc0 nc0-0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((2 0) (0 0)) ((2 2) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nb1 nc0-0 nc1-0)
  (operation nonce-test (added-strand init 3) nb1 (0 2)
    (enc na1 nc1-0 c b (enc na0 nb1 b c (pubk a))
      (enc nb1 nc0-0 c a (pubk b)) (pubk a))
    (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb1 b c (pubk a))
      (pubk c)))
  (traces
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb1 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb1 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb1 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na0 nb1 b c (pubk a))
          (enc nb1 nc0-0 c a (pubk b)) (pubk a))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1-0 c b (enc na0 nb1 b c (pubk a))
          (enc nb1 nc0-0 c a (pubk b)) (pubk a)))
      (send
        (enc nb1 (enc nb1 nc0-0 c a (pubk b)) (enc nc1-0 (pubk c))
          (pubk b)))))
  (label 10)
  (parent 8)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc0 nc1 nc0-0 nc1-0 text) (a b c name))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0-0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0-0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((2 0) (0 0)) ((2 2) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nb0 nb1 nc0-0 nc1-0)
  (operation nonce-test (added-strand init 3) nb0 (0 2)
    (enc na1 nc1-0 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc0-0 c a (pubk b)) (pubk a))
    (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0-0 c a (pubk b)) (pubk a))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1-0 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0-0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0-0 c a (pubk b)) (enc nc1-0 (pubk c))
          (pubk b)))))
  (label 11)
  (parent 8)
  (unrealized (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb1 nc0 nc1 text) (a b c name))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb1) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb1) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb1) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((2 0) (0 0)) ((2 2) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nb1 nc0 nc1)
  (operation nonce-test (contracted (nc0-0 nc0) (nc1-0 nc1)) nb1 (0 2)
    (enc na1 nc1 c b (enc na0 nb1 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a))
    (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb1 b c (pubk a))
      (pubk c))
    (enc nb1 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c)) (pubk b)))
  (traces
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb1 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb1 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb1 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb1 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb1 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb1 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b)))))
  (label 12)
  (parent 10)
  (seen 13)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc0 nc1 text) (a b c name))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((2 0) (0 0)) ((2 2) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nb0 nb1 nc0 nc1)
  (operation nonce-test (contracted (nc0-0 nc0) (nc1-0 nc1)) nb0 (0 2)
    (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a))
    (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c)) (pubk b))
    (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b)))))
  (label 13)
  (parent 11)
  (unrealized)
  (shape))

(comment "Nothing left to do")

(defprotocol nsl3 basic
  (defrole init
    (vars (a b c name) (na0 na1 nb0 nb1 nc0 nc1 text))
    (trace (send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    (uniq-orig na0 na1))
  (defrole mid
    (vars (a b c name) (na0 na1 nb0 nb1 nc0 nc1 text))
    (trace (recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    (uniq-orig nb0 nb1))
  (defrole resp
    (vars (a b c name) (na0 na1 nb0 nb1 nc0 nc1 text))
    (trace
      (recv
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    (uniq-orig nc0 nc1)))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc0 nc1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc0 nc1)
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c)))))
  (label 14)
  (seen 15)
  (unrealized (0 2))
  (comment "5 in cohort - 2 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc0 nc1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nc0 nc1)
  (operation nonce-test (added-strand init 3) nc0 (0 2)
    (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b)))))
  (label 15)
  (parent 14)
  (seen 17)
  (unrealized (0 0) (0 2))
  (comment "4 in cohort - 2 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nc1)
  (operation nonce-test (added-strand init 3) nc1 (0 2)
    (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc1 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b)))))
  (label 16)
  (parent 14)
  (seen 19)
  (unrealized (0 0) (0 2))
  (comment "4 in cohort - 2 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc0 nc1 nb0-0 nb1-0 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na1) (nb0 nb0-0) (nb1 nb1-0) (a a)
    (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nc0 nc1 nb0-0 nb1-0)
  (operation nonce-test (added-strand mid 2) na1 (0 0)
    (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1-0 b a (enc na1 a b (pubk c))
          (enc na0 nb0-0 b c (pubk a)) (pubk c)))))
  (label 17)
  (parent 15)
  (unrealized (0 0) (0 2))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton nsl3
  (vars (na0 nb0 nb1 nc0 nc1 nb0-0 nb1-0 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na0) (nb0 nb0-0) (nb1 nb1-0) (a a)
    (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 nc0 nc1 nb0-0 nb1-0)
  (operation nonce-test (added-strand mid 2) na0 (0 0)
    (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
  (traces
    ((recv
       (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (recv
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (send
        (enc nb1-0 b a (enc na0 a b (pubk c))
          (enc na0 nb0-0 b c (pubk a)) (pubk c)))))
  (label 18)
  (parent 15)
  (seen 23)
  (unrealized (0 0) (0 2))
  (comment "5 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc1 nb0-0 nb1-0 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na1) (nb0 nb0-0) (nb1 nb1-0) (a a)
    (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nc1 nb0-0 nb1-0)
  (operation nonce-test (added-strand mid 2) na1 (0 0)
    (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1-0 b a (enc na1 a b (pubk c))
          (enc na0 nb0-0 b c (pubk a)) (pubk c)))))
  (label 19)
  (parent 16)
  (unrealized (0 0) (0 2))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton nsl3
  (vars (na0 nb0 nb1 nc1 nb0-0 nb1-0 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na0) (nb0 nb0-0) (nb1 nb1-0) (a a)
    (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 nc1 nb0-0 nb1-0)
  (operation nonce-test (added-strand mid 2) na0 (0 0)
    (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
  (traces
    ((recv
       (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (recv
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (send
        (enc nb1-0 b a (enc na0 a b (pubk c))
          (enc na0 nb0-0 b c (pubk a)) (pubk c)))))
  (label 20)
  (parent 16)
  (seen 27)
  (unrealized (0 0) (0 2))
  (comment "5 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nc0 nc1 nb0 nb1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (a a) (b b)
    (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nc0 nc1 nb0 nb1)
  (operation nonce-test (contracted (nb0-0 nb0) (nb1-0 nb1)) na1 (0 0)
    (enc na0 a c (enc na1 a b (pubk c)) (pubk b))
    (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))))
  (label 21)
  (parent 17)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc0 nc1 nb0-0 nb1-0 nc0-0 nc1-0 text)
    (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na1) (nb0 nb0-0) (nb1 nb1-0) (a a)
    (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb0-0) (nb1 nb1-0)
    (nc0 nc0-0) (nc1 nc1-0) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (3 0))
    ((3 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nc0 nc1 nb0-0 nb1-0 nc0-0 nc1-0)
  (operation nonce-test (added-strand resp 2) na1 (0 0)
    (enc na0 a c (enc na1 a b (pubk c)) (pubk b))
    (enc nb1-0 b a (enc na1 a b (pubk c)) (enc na0 nb0-0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1-0 b a (enc na1 a b (pubk c))
          (enc na0 nb0-0 b c (pubk a)) (pubk c))))
    ((recv
       (enc nb1-0 b a (enc na1 a b (pubk c))
         (enc na0 nb0-0 b c (pubk a)) (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na0 nb0-0 b c (pubk a))
          (enc nb1-0 nc0-0 c a (pubk b)) (pubk a)))))
  (label 22)
  (parent 17)
  (unrealized (0 0) (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (na0 nb0 nb1 nc0 nc1 nb0-0 nb1-0 nc0-0 nc1-0 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na0) (nb0 nb0-0) (nb1 nb1-0) (a a)
    (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na0) (nb0 nb0-0) (nb1 nb1-0)
    (nc0 nc0-0) (nc1 nc1-0) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (3 0))
    ((3 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 nc0 nc1 nb0-0 nb1-0 nc0-0 nc1-0)
  (operation nonce-test (added-strand resp 2) na0 (0 0)
    (enc na0 a c (enc na0 a b (pubk c)) (pubk b))
    (enc nb1-0 b a (enc na0 a b (pubk c)) (enc na0 nb0-0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv
       (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (recv
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (send
        (enc nb1-0 b a (enc na0 a b (pubk c))
          (enc na0 nb0-0 b c (pubk a)) (pubk c))))
    ((recv
       (enc nb1-0 b a (enc na0 a b (pubk c))
         (enc na0 nb0-0 b c (pubk a)) (pubk c)))
      (send
        (enc na0 nc1-0 c b (enc na0 nb0-0 b c (pubk a))
          (enc nb1-0 nc0-0 c a (pubk b)) (pubk a)))))
  (label 23)
  (parent 17)
  (unrealized (0 0) (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (na0 nc0 nc1 nb0 nb1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (a a) (b b)
    (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 nc0 nc1 nb0 nb1)
  (operation nonce-test (contracted (nb0-0 nb0) (nb1-0 nb1)) na0 (0 0)
    (enc na0 a c (enc na0 a b (pubk c)) (pubk b))
    (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv
       (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (recv
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))))
  (label 24)
  (parent 18)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nc1 nb0 nb1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (a a) (b b)
    (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nc1 nb0 nb1)
  (operation nonce-test (contracted (nb0-0 nb0) (nb1-0 nb1)) na1 (0 0)
    (enc na0 a c (enc na1 a b (pubk c)) (pubk b))
    (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))))
  (label 25)
  (parent 19)
  (seen 29)
  (unrealized (0 2))
  (comment "3 in cohort - 0 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nb0 nb1 nc1 nb0-0 nb1-0 nc0 nc1-0 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na1) (nb0 nb0-0) (nb1 nb1-0) (a a)
    (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb0-0) (nb1 nb1-0)
    (nc0 nc0) (nc1 nc1-0) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (3 0))
    ((3 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nc1 nb0-0 nb1-0 nc0 nc1-0)
  (operation nonce-test (added-strand resp 2) na1 (0 0)
    (enc na0 a c (enc na1 a b (pubk c)) (pubk b))
    (enc nb1-0 b a (enc na1 a b (pubk c)) (enc na0 nb0-0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1-0 b a (enc na1 a b (pubk c))
          (enc na0 nb0-0 b c (pubk a)) (pubk c))))
    ((recv
       (enc nb1-0 b a (enc na1 a b (pubk c))
         (enc na0 nb0-0 b c (pubk a)) (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na0 nb0-0 b c (pubk a))
          (enc nb1-0 nc0 c a (pubk b)) (pubk a)))))
  (label 26)
  (parent 19)
  (unrealized (0 0) (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (na0 nb0 nb1 nc1 nb0-0 nb1-0 nc0 nc1-0 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na0) (nb0 nb0-0) (nb1 nb1-0) (a a)
    (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na0) (nb0 nb0-0) (nb1 nb1-0)
    (nc0 nc0) (nc1 nc1-0) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (3 0))
    ((3 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 nc1 nb0-0 nb1-0 nc0 nc1-0)
  (operation nonce-test (added-strand resp 2) na0 (0 0)
    (enc na0 a c (enc na0 a b (pubk c)) (pubk b))
    (enc nb1-0 b a (enc na0 a b (pubk c)) (enc na0 nb0-0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv
       (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (recv
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (send
        (enc nb1-0 b a (enc na0 a b (pubk c))
          (enc na0 nb0-0 b c (pubk a)) (pubk c))))
    ((recv
       (enc nb1-0 b a (enc na0 a b (pubk c))
         (enc na0 nb0-0 b c (pubk a)) (pubk c)))
      (send
        (enc na0 nc1-0 c b (enc na0 nb0-0 b c (pubk a))
          (enc nb1-0 nc0 c a (pubk b)) (pubk a)))))
  (label 27)
  (parent 19)
  (unrealized (0 0) (0 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (na0 nc1 nb0 nb1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (a a) (b b)
    (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 nc1 nb0 nb1)
  (operation nonce-test (contracted (nb0-0 nb0) (nb1-0 nb1)) na0 (0 0)
    (enc na0 a c (enc na0 a b (pubk c)) (pubk b))
    (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv
       (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (recv
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))))
  (label 28)
  (parent 20)
  (seen 33)
  (unrealized (0 2))
  (comment "3 in cohort - 0 not yet seen"))

(defskeleton nsl3
  (vars (nc1 nb0 nb1 na0 na1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((0 1) (2 2)) ((1 0) (2 0)) ((1 2) (0 2))
    ((2 1) (0 0)) ((2 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc1 nb0 nb1 na0 na1)
  (operation nonce-test (added-strand mid 4) nc1 (0 2)
    (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c)) (pubk b))
    (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc1 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc1 (enc nc1 (pubk c)) (pubk c)))))
  (label 29)
  (parent 21)
  (seen 37)
  (unrealized (2 2))
  (comment "5 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (nc0 nc1 nb0 nb1 na0 na1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((0 1) (2 2)) ((1 0) (2 0)) ((1 2) (0 2))
    ((2 1) (0 0)) ((2 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc0 nc1 nb0 nb1 na0 na1)
  (operation nonce-test (added-strand mid 4) nc0 (0 2)
    (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c)) (pubk b))
    (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c)))))
  (label 30)
  (parent 21)
  (seen 37 38)
  (unrealized (2 2))
  (comment "5 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nc0 nc1 nb0 nb1 nc0-0 nc1-0 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (a a) (b b)
    (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0-0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (3 0))
    ((3 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nc0 nc1 nb0 nb1 nc0-0 nc1-0)
  (operation nonce-test (contracted (nb0-0 nb0) (nb1-0 nb1)) na1 (0 0)
    (enc na0 a c (enc na1 a b (pubk c)) (pubk b))
    (enc na1 nc1-0 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc0-0 c a (pubk b)) (pubk a))
    (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0-0 c a (pubk b)) (pubk a)))))
  (label 31)
  (parent 22)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton nsl3
  (vars (na0 nc0 nc1 nb0 nb1 nc0-0 nc1-0 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (a a) (b b)
    (c c))
  (defstrand resp 2 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc0-0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (3 0))
    ((3 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 nc0 nc1 nb0 nb1 nc0-0 nc1-0)
  (operation nonce-test (contracted (nb0-0 nb0) (nb1-0 nb1)) na0 (0 0)
    (enc na0 nc1-0 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc0-0 c a (pubk b)) (pubk a))
    (enc na0 a c (enc na0 a b (pubk c)) (pubk b))
    (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv
       (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (recv
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c))))
    ((recv
       (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na0 nc1-0 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0-0 c a (pubk b)) (pubk a)))))
  (label 32)
  (parent 23)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton nsl3
  (vars (nc1 nb0 nb1 na1 text) (a b c name))
  (defstrand resp 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((0 1) (2 2)) ((1 0) (2 0)) ((1 2) (0 2))
    ((2 1) (0 0)) ((2 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc1 nb0 nb1 na1)
  (operation nonce-test (added-strand mid 4) nc1 (0 2)
    (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c)) (pubk b))
    (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
      (enc nb1 nc1 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc1 (enc nc1 (pubk c)) (pubk c)))))
  (label 33)
  (parent 24)
  (seen 43)
  (unrealized (2 2))
  (comment "5 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (nc0 nc1 nb0 nb1 na1 text) (a b c name))
  (defstrand resp 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((0 1) (2 2)) ((1 0) (2 0)) ((1 2) (0 2))
    ((2 1) (0 0)) ((2 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc0 nc1 nb0 nb1 na1)
  (operation nonce-test (added-strand mid 4) nc0 (0 2)
    (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c)) (pubk b))
    (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c)))))
  (label 34)
  (parent 24)
  (seen 43 44)
  (unrealized (2 2))
  (comment "5 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (na0 na1 nc1 nb0 nb1 nc0 nc1-0 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (a a) (b b)
    (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (3 0))
    ((3 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 na1 nc1 nb0 nb1 nc0 nc1-0)
  (operation nonce-test (contracted (nb0-0 nb0) (nb1-0 nb1)) na1 (0 0)
    (enc na0 a c (enc na1 a b (pubk c)) (pubk b))
    (enc na1 nc1-0 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a))
    (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))))
  (label 35)
  (parent 26)
  (seen 39)
  (unrealized (0 2))
  (comment "3 in cohort - 0 not yet seen"))

(defskeleton nsl3
  (vars (na0 nc1 nb0 nb1 nc0 nc1-0 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 2 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (a a) (b b)
    (c c))
  (defstrand resp 2 (na0 na0) (na1 na0) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (3 0))
    ((3 1) (0 0)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig na0 nc1 nb0 nb1 nc0 nc1-0)
  (operation nonce-test (contracted (nb0-0 nb0) (nb1-0 nb1)) na0 (0 0)
    (enc na0 nc1-0 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a))
    (enc na0 a c (enc na0 a b (pubk c)) (pubk b))
    (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
      (pubk c)))
  (traces
    ((recv
       (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (recv
        (enc na0 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na0 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c))))
    ((recv
       (enc nb1 b a (enc na0 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na0 nc1-0 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))))
  (label 36)
  (parent 27)
  (seen 41)
  (unrealized (0 2))
  (comment "3 in cohort - 0 not yet seen"))

(defskeleton nsl3
  (vars (nc1 nb0 nb1 na0 na1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (2 2)) ((2 1) (0 0))
    ((2 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc1 nb0 nb1 na0 na1)
  (operation nonce-test (added-strand init 3) nc1 (2 2)
    (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc1 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc1 (enc nc1 (pubk c)) (pubk c)))))
  (label 37)
  (parent 29)
  (seen 38)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton nsl3
  (vars (nc0 nc1 nb0 nb1 na0 na1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (2 2)) ((2 1) (0 0))
    ((2 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc0 nc1 nb0 nb1 na0 na1)
  (operation nonce-test (added-strand init 3) nc0 (2 2)
    (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c)))))
  (label 38)
  (parent 30)
  (unrealized)
  (shape))

(defskeleton nsl3
  (vars (nc1 nb0 nb1 nc0 nc1-0 na0 na1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((0 1) (3 2)) ((1 0) (3 0)) ((1 2) (0 2))
    ((2 1) (0 0)) ((3 1) (2 0)) ((3 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc1 nb0 nb1 nc0 nc1-0 na0 na1)
  (operation nonce-test (added-strand mid 4) nc1 (0 2)
    (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c)) (pubk b))
    (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc1 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc1 (enc nc1 (pubk c)) (pubk c)))))
  (label 39)
  (parent 31)
  (seen 45)
  (unrealized (3 2))
  (comment "5 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (nc0 nc1 nb0 nb1 nc0-0 nc1-0 na0 na1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0-0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((0 1) (3 2)) ((1 0) (3 0)) ((1 2) (0 2))
    ((2 1) (0 0)) ((3 1) (2 0)) ((3 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc0 nc1 nb0 nb1 nc0-0 nc1-0 na0 na1)
  (operation nonce-test (added-strand mid 4) nc0 (0 2)
    (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c)) (pubk b))
    (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0-0 c a (pubk b)) (pubk a))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c)))))
  (label 40)
  (parent 31)
  (seen 45 46)
  (unrealized (3 2))
  (comment "5 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (nc1 nb0 nb1 nc0 nc1-0 na1 text) (a b c name))
  (defstrand resp 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand resp 2 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((0 1) (3 2)) ((1 0) (3 0)) ((1 2) (0 2))
    ((2 1) (0 0)) ((3 1) (2 0)) ((3 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc1 nb0 nb1 nc0 nc1-0 na1)
  (operation nonce-test (added-strand mid 4) nc1 (0 2)
    (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c)) (pubk b))
    (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
      (enc nb1 nc1 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a))))
    ((recv (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc1 (enc nc1 (pubk c)) (pubk c)))))
  (label 41)
  (parent 32)
  (seen 47)
  (unrealized (3 2))
  (comment "5 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (nc0 nc1 nb0 nb1 nc0-0 nc1-0 na1 text) (a b c name))
  (defstrand resp 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand resp 2 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0-0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((0 1) (3 2)) ((1 0) (3 0)) ((1 2) (0 2))
    ((2 1) (0 0)) ((3 1) (2 0)) ((3 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc0 nc1 nb0 nb1 nc0-0 nc1-0 na1)
  (operation nonce-test (added-strand mid 4) nc0 (0 2)
    (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c)) (pubk b))
    (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0-0 c a (pubk b)) (pubk a))))
    ((recv (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c)))))
  (label 42)
  (parent 32)
  (seen 47 48)
  (unrealized (3 2))
  (comment "5 in cohort - 1 not yet seen"))

(defskeleton nsl3
  (vars (nc1 nb0 nb1 na1 text) (a b c name))
  (defstrand resp 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (2 2)) ((2 1) (0 0))
    ((2 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc1 nb0 nb1 na1)
  (operation nonce-test (added-strand init 3) nc1 (2 2)
    (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
      (enc nb1 nc1 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc1 (enc nc1 (pubk c)) (pubk c)))))
  (label 43)
  (parent 33)
  (seen 44)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton nsl3
  (vars (nc0 nc1 nb0 nb1 na1 text) (a b c name))
  (defstrand resp 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (2 2)) ((2 1) (0 0))
    ((2 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc0 nc1 nb0 nb1 na1)
  (operation nonce-test (added-strand init 3) nc0 (2 2)
    (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c)))))
  (label 44)
  (parent 34)
  (seen 38)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton nsl3
  (vars (nc1 nb0 nb1 nc0 nc1-0 na0 na1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (3 0)) ((1 2) (3 2)) ((2 1) (0 0))
    ((3 1) (2 0)) ((3 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc1 nb0 nb1 nc0 nc1-0 na0 na1)
  (operation nonce-test (added-strand init 3) nc1 (3 2)
    (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc1 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc1 (enc nc1 (pubk c)) (pubk c)))))
  (label 45)
  (parent 39)
  (seen 37)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton nsl3
  (vars (nc0 nc1 nb0 nb1 nc0-0 nc1-0 na0 na1 text) (a b c name))
  (defstrand resp 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand resp 2 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0-0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (3 0)) ((1 2) (3 2)) ((2 1) (0 0))
    ((3 1) (2 0)) ((3 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc0 nc1 nb0 nb1 nc0-0 nc1-0 na0 na1)
  (operation nonce-test (added-strand init 3) nc0 (3 2)
    (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na0 nb0 b c (pubk a))
          (enc nb1 nc0-0 c a (pubk b)) (pubk a))))
    ((recv (enc na0 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na0 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c)))))
  (label 46)
  (parent 40)
  (seen 38)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton nsl3
  (vars (nc1 nb0 nb1 nc0 nc1-0 na1 text) (a b c name))
  (defstrand resp 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand resp 2 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc1)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (3 0)) ((1 2) (3 2)) ((2 1) (0 0))
    ((3 1) (2 0)) ((3 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc1 nb0 nb1 nc0 nc1-0 na1)
  (operation nonce-test (added-strand init 3) nc1 (3 2)
    (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
      (enc nb1 nc1 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (recv (enc nc1 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc1 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a))))
    ((recv (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc1 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc1 (enc nc1 (pubk c)) (pubk c)))))
  (label 47)
  (parent 41)
  (seen 43)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton nsl3
  (vars (nc0 nc1 nb0 nb1 nc0-0 nc1-0 na1 text) (a b c name))
  (defstrand resp 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand init 3 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (defstrand resp 2 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0-0)
    (nc1 nc1-0) (a a) (b b) (c c))
  (defstrand mid 4 (na0 na1) (na1 na1) (nb0 nb0) (nb1 nb1) (nc0 nc0)
    (nc1 nc1) (a a) (b b) (c c))
  (precedes ((0 1) (1 1)) ((1 0) (3 0)) ((1 2) (3 2)) ((2 1) (0 0))
    ((3 1) (2 0)) ((3 3) (0 2)))
  (non-orig (privk a) (privk b) (privk c))
  (uniq-orig nc0 nc1 nb0 nb1 nc0-0 nc1-0 na1)
  (operation nonce-test (added-strand init 3) nc0 (3 2)
    (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
      (enc nb1 nc0 c a (pubk b)) (pubk a)))
  (traces
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))
    ((send (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (recv
        (enc na1 nc1 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0 c a (pubk b)) (pubk a)))
      (send
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))))
    ((recv
       (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
         (pubk c)))
      (send
        (enc na1 nc1-0 c b (enc na1 nb0 b c (pubk a))
          (enc nb1 nc0-0 c a (pubk b)) (pubk a))))
    ((recv (enc na1 a c (enc na1 a b (pubk c)) (pubk b)))
      (send
        (enc nb1 b a (enc na1 a b (pubk c)) (enc na1 nb0 b c (pubk a))
          (pubk c)))
      (recv
        (enc nb0 (enc nb1 nc0 c a (pubk b)) (enc nc1 (pubk c))
          (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c)))))
  (label 48)
  (parent 42)
  (seen 44)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")