(line (spec (line (declare (line (type (line "S" 2 8 2 9 "otwayrees.eva") (line "principal" 2 12 2 21 "otwayrees.eva")) 2 2 2 21 "otwayrees.eva") (line (type (line "B" 2 5 2 6 "otwayrees.eva") (line "principal" 2 12 2 21 "otwayrees.eva")) 2 2 2 21 "otwayrees.eva") (line (type (line "A" 2 2 2 3 "otwayrees.eva") (line "principal" 2 12 2 21 "otwayrees.eva")) 2 2 2 21 "otwayrees.eva") (line (type (line "Kab" 3 12 3 15 "otwayrees.eva") (line "number" 3 18 3 24 "otwayrees.eva")) 3 2 3 24 "otwayrees.eva") (line (type (line "Kbs" 3 7 3 10 "otwayrees.eva") (line "number" 3 18 3 24 "otwayrees.eva")) 3 2 3 24 "otwayrees.eva") (line (type (line "Kas" 3 2 3 5 "otwayrees.eva") (line "number" 3 18 3 24 "otwayrees.eva")) 3 2 3 24 "otwayrees.eva") (line (type (line "Nb" 4 9 4 11 "otwayrees.eva") (line "number" 4 14 4 20 "otwayrees.eva")) 4 2 4 20 "otwayrees.eva") (line (type (line "Na" 4 5 4 7 "otwayrees.eva") (line "number" 4 14 4 20 "otwayrees.eva")) 4 2 4 20 "otwayrees.eva") (line (type (line "N" 4 2 4 3 "otwayrees.eva") (line "number" 4 14 4 20 "otwayrees.eva")) 4 2 4 20 "otwayrees.eva") (line (knows (line "A" 6 2 6 3 "otwayrees.eva") (line "A" 6 10 6 11 "otwayrees.eva")) 6 2 6 19 "otwayrees.eva") (line (knows (line "A" 6 2 6 3 "otwayrees.eva") (line "B" 6 13 6 14 "otwayrees.eva")) 6 2 6 19 "otwayrees.eva") (line (knows (line "A" 6 2 6 3 "otwayrees.eva") (line "Kas" 6 16 6 19 "otwayrees.eva")) 6 2 6 19 "otwayrees.eva") (line (knows (line "B" 7 2 7 3 "otwayrees.eva") (line "S" 7 10 7 11 "otwayrees.eva")) 7 2 7 16 "otwayrees.eva") (line (knows (line "B" 7 2 7 3 "otwayrees.eva") (line "Kbs" 7 13 7 16 "otwayrees.eva")) 7 2 7 16 "otwayrees.eva") (line (knows (line "S" 8 2 8 3 "otwayrees.eva") (line "Kas" 8 10 8 13 "otwayrees.eva")) 8 2 8 18 "otwayrees.eva") (line (knows (line "S" 8 2 8 3 "otwayrees.eva") (line "Kbs" 8 15 8 18 "otwayrees.eva")) 8 2 8 18 "otwayrees.eva") (line (type (line "s" 10 8 10 9 "otwayrees.eva") (line "principal" 10 12 10 21 "otwayrees.eva")) 10 2 10 21 "otwayrees.eva") (line (type (line "b" 10 5 10 6 "otwayrees.eva") (line "principal" 10 12 10 21 "otwayrees.eva")) 10 2 10 21 "otwayrees.eva") (line (type (line "a" 10 2 10 3 "otwayrees.eva") (line "principal" 10 12 10 21 "otwayrees.eva")) 10 2 10 21 "otwayrees.eva")) 1 0 10 21 "") (line (line (block (line (comm "1." (line "A" 13 7 13 8 "otwayrees.eva") (line "B" 13 12 13 13 "otwayrees.eva") (line (tuple (line "N" 13 16 13 17 "otwayrees.eva") (line "A" 13 19 13 20 "otwayrees.eva") (line "B" 13 22 13 23 "otwayrees.eva") (line (crypt (line (tuple (line "Na" 13 26 13 28 "otwayrees.eva") (line "N" 13 30 13 31 "otwayrees.eva") (line "A" 13 33 13 34 "otwayrees.eva") (line "B" 13 36 13 37 "otwayrees.eva")) 13 26 13 37 "otwayrees.eva") (line "Kas" 13 39 13 42 "otwayrees.eva") (vanilla)) 13 25 13 42 "otwayrees.eva")) 13 16 13 42 "otwayrees.eva")) 13 4 13 42 "otwayrees.eva") (line (comm "2." (line "B" 14 7 14 8 "otwayrees.eva") (line "S" 14 12 14 13 "otwayrees.eva") (line (tuple (line "N" 14 16 14 17 "otwayrees.eva") (line "A" 14 19 14 20 "otwayrees.eva") (line "B" 14 22 14 23 "otwayrees.eva") (line (crypt (line (tuple (line "Na" 14 26 14 28 "otwayrees.eva") (line "N" 14 30 14 31 "otwayrees.eva") (line "A" 14 33 14 34 "otwayrees.eva") (line "B" 14 36 14 37 "otwayrees.eva")) 14 26 14 37 "otwayrees.eva") (line "Kas" 14 39 14 42 "otwayrees.eva") (vanilla)) 14 25 14 42 "otwayrees.eva") (line (crypt (line (tuple (line "Nb" 15 26 15 28 "otwayrees.eva") (line "N" 15 30 15 31 "otwayrees.eva") (line "A" 15 33 15 34 "otwayrees.eva") (line "B" 15 36 15 37 "otwayrees.eva")) 15 26 15 37 "otwayrees.eva") (line "Kbs" 15 39 15 42 "otwayrees.eva") (vanilla)) 15 25 15 42 "otwayrees.eva")) 14 16 15 42 "otwayrees.eva")) 14 4 15 42 "otwayrees.eva") (line (comm "3." (line "S" 16 7 16 8 "otwayrees.eva") (line "B" 16 12 16 13 "otwayrees.eva") (line (tuple (line "N" 16 16 16 17 "otwayrees.eva") (line (crypt (line (tuple (line "Na" 16 20 16 22 "otwayrees.eva") (line "Kab" 16 24 16 27 "otwayrees.eva")) 16 20 16 27 "otwayrees.eva") (line "Kas" 16 29 16 32 "otwayrees.eva") (vanilla)) 16 19 16 32 "otwayrees.eva") (line (crypt (line (tuple (line "Nb" 16 35 16 37 "otwayrees.eva") (line "Kab" 16 39 16 42 "otwayrees.eva")) 16 35 16 42 "otwayrees.eva") (line "Kbs" 16 44 16 47 "otwayrees.eva") (vanilla)) 16 34 16 47 "otwayrees.eva")) 16 16 16 47 "otwayrees.eva")) 16 4 16 47 "otwayrees.eva") (line (comm "4." (line "B" 17 7 17 8 "otwayrees.eva") (line "A" 17 12 17 13 "otwayrees.eva") (line (tuple (line "N" 17 16 17 17 "otwayrees.eva") (line (crypt (line (tuple (line "Na" 17 20 17 22 "otwayrees.eva") (line "Kab" 17 24 17 27 "otwayrees.eva")) 17 20 17 27 "otwayrees.eva") (line "Kas" 17 29 17 32 "otwayrees.eva") (vanilla)) 17 19 17 32 "otwayrees.eva")) 17 16 17 32 "otwayrees.eva")) 17 4 17 32 "otwayrees.eva")) 12 2 18 3 "otwayrees.eva") 12 2 18 3 "otwayrees.eva") (line (sessions (line (session-repeat (line (private (line "Kas" 20 16 20 19 "otwayrees.eva") (line "Kbs" 20 21 20 24 "otwayrees.eva")) 20 15 20 25 "otwayrees.eva") "s1." (line (principals-except) 20 15 20 16 "otwayrees.eva") (line (bind (line "A" 20 26 20 27 "otwayrees.eva") (line "a" 20 28 20 29 "otwayrees.eva")) 20 26 20 29 "otwayrees.eva") (line (bind (line "B" 20 31 20 32 "otwayrees.eva") (line "b" 20 33 20 34 "otwayrees.eva")) 20 31 20 34 "otwayrees.eva") (line (bind (line "S" 20 36 20 37 "otwayrees.eva") (line "s" 20 38 20 39 "otwayrees.eva")) 20 36 20 39 "otwayrees.eva")) 20 2 20 39 "otwayrees.eva")) 18 2 20 39 "") (line (assume (line (secret (line (locate "s1." (line "A" 22 24 22 25 "otwayrees.eva") (line "Kas" 22 17 22 20 "otwayrees.eva")) 22 17 22 25 "otwayrees.eva")) 22 9 22 26 "otwayrees.eva") (line (secret (line (locate "s1." (line "B" 22 43 22 44 "otwayrees.eva") (line "Kbs" 22 36 22 39 "otwayrees.eva")) 22 36 22 44 "otwayrees.eva")) 22 28 22 45 "otwayrees.eva") (line (prop (line "equals" 23 1 23 7 "otwayrees.eva") (line (locate "s1." (line "A" 23 16 23 17 "otwayrees.eva") (line "Kas" 23 9 23 12 "otwayrees.eva")) 23 9 23 17 "otwayrees.eva") (line (locate "s1." (line "S" 23 26 23 27 "otwayrees.eva") (line "Kas" 23 19 23 22 "otwayrees.eva")) 23 19 23 27 "otwayrees.eva")) 23 1 23 28 "otwayrees.eva") (line (prop (line "equals" 23 30 23 36 "otwayrees.eva") (line (locate "s1." (line "B" 23 45 23 46 "otwayrees.eva") (line "Kbs" 23 38 23 41 "otwayrees.eva")) 23 38 23 46 "otwayrees.eva") (line (locate "s1." (line "S" 23 55 23 56 "otwayrees.eva") (line "Kbs" 23 48 23 51 "otwayrees.eva")) 23 48 23 56 "otwayrees.eva")) 23 30 23 57 "otwayrees.eva")) 22 2 23 57 "otwayrees.eva") (line (claim (line (A (line (G (line (secret (line (locate "s1." (line "A" 24 28 24 29 "otwayrees.eva") (line "Kas" 24 21 24 24 "otwayrees.eva")) 24 21 24 29 "otwayrees.eva")) 24 13 24 30 "otwayrees.eva")) 24 10 24 30 "otwayrees.eva")) 24 8 24 30 "otwayrees.eva") (line (A (line (G (line (secret (line (locate "s1." (line "B" 25 21 25 22 "otwayrees.eva") (line "Kbs" 25 14 25 17 "otwayrees.eva")) 25 14 25 22 "otwayrees.eva")) 25 6 25 23 "otwayrees.eva")) 25 3 25 23 "otwayrees.eva")) 25 1 25 23 "otwayrees.eva") (line (A (line (G (line (secret (line (locate "s1." (line "S" 26 21 26 22 "otwayrees.eva") (line "Kas" 26 14 26 17 "otwayrees.eva")) 26 14 26 22 "otwayrees.eva")) 26 6 26 23 "otwayrees.eva")) 26 3 26 23 "otwayrees.eva")) 26 1 26 23 "otwayrees.eva") (line (A (line (G (line (secret (line (locate "s1." (line "S" 27 21 27 22 "otwayrees.eva") (line "Kbs" 27 14 27 17 "otwayrees.eva")) 27 14 27 22 "otwayrees.eva")) 27 6 27 23 "otwayrees.eva")) 27 3 27 23 "otwayrees.eva")) 27 1 27 23 "otwayrees.eva") (line (A (line (G (line (secret (line (locate "s1." (line "A" 28 21 28 22 "otwayrees.eva") (line "Kab" 28 14 28 17 "otwayrees.eva")) 28 14 28 22 "otwayrees.eva")) 28 6 28 23 "otwayrees.eva")) 28 3 28 23 "otwayrees.eva")) 28 1 28 23 "otwayrees.eva") (line (A (line (G (line (secret (line (locate "s1." (line "B" 29 21 29 22 "otwayrees.eva") (line "Kab" 29 14 29 17 "otwayrees.eva")) 29 14 29 22 "otwayrees.eva")) 29 6 29 23 "otwayrees.eva")) 29 3 29 23 "otwayrees.eva")) 29 1 29 23 "otwayrees.eva") (line (A (line (G (line (prop (line "equals" 30 6 30 12 "otwayrees.eva") (line (locate "s1." (line "A" 30 21 30 22 "otwayrees.eva") (line "Kab" 30 14 30 17 "otwayrees.eva")) 30 14 30 22 "otwayrees.eva") (line (locate "s1." (line "B" 30 31 30 32 "otwayrees.eva") (line "Kab" 30 24 30 27 "otwayrees.eva")) 30 24 30 32 "otwayrees.eva")) 30 6 30 33 "otwayrees.eva")) 30 3 30 33 "otwayrees.eva")) 30 1 30 33 "otwayrees.eva")) 24 2 30 33 "otwayrees.eva")) 1 0 23 57 "otwayrees.eva")