// Testfile dumped by Ultimate at 2019/12/26 09:43:22 // // BranchingProcess bp = finitePrefix(net); PetriNet net = ( alphabet = {a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31 a32 a33 a34 a35 a36 a37 a38 a39 a40 a41 a42 a43 a44 a45 a46 a47 a48 a49 a50 a51 a52 a53 a54 a55 a56 a57 a58 a59 a60 a61 a62 a63 a64 a65 a66 a67 a68 a69 a70 a71 a72 a73 a74 a75 a76 a77 a78 a79 a80 a81 a82 a83 a84 a85 a86 a87 a88 a89 a90 a91 a92 a93 a94 a95 a96 a97 a98 a99 a100 a101 a102 a103 a104 a105 a106 a107 a108 a109 a110 a111 a112 a113 a114 a115 a116 a117 a118 a119 a120 a121 a122 a123 a124 a125 a126 a127 a128 a129 a130 a131 a132 a133 a134 a135 a136 a137 a138 a139 a140 a141 a142 a143 a144 a145 a146 a147 a148 a149 a150 a151 a152 a153 a154 a155 a156 a157 a158 a159 a160 a161 a162 a163 a164 a165 a166 a167 a168 a169 a170 a171 a172 a173 a174 a175 a176 a177 a178 a179 a180 a181 a182 a183 a184 a185 a186 a187 a188 a189 a190 a191 a192 a193 a194 a195 a196 a197 a198 a199 a200 a201 a202 a203 a204 a205 a206 a207 a208 a209 a210 a211 a212 a213 a214 a215 a216 a217 a218 a219 a220 a221 a222 a223 a224 a225 a226 a227 a228 a229 a230 a231 a232 a233 a234 a235 a236 a237 a238 a239 a240 a241 a242 a243 a244 a245 a246 a247 a248 a249 a250 a251 a252 a253 a254 a255 a256 a257 a258 a259 a260 a261 a262 a263 a264 a265 a266 a267 a268 a269 a270 a271 a272 a273 a274 a275 a276 a277 a278 a279 a280 a281 a282 a283 a284 a285 a286 a287 a288 a289 a290 a291 a292 a293 a294 a295 a296 a297 a298 a299 a300 a301 a302 a303 a304 a305 a306 a307 a308 a309 a310 a311 a312 a313 a314 a315 a316 a317 a318 a319 a320 a321 a322 a323 a324 a325 a326 a327 a328 }, places = {p0 p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22 p23 p24 p25 p26 p27 p28 p29 p30 p31 p32 p33 p34 p35 p36 p37 p38 p39 p40 p41 p42 p43 p44 p45 p46 p47 p48 p49 p50 p51 p52 p53 p54 p55 p56 p57 p58 p59 p60 p61 p62 p63 p64 p65 p66 p67 p68 p69 p70 p71 p72 p73 p74 p75 p76 p77 p78 p79 p80 p81 p82 p83 p84 p85 p86 p87 p88 p89 p90 p91 p92 p93 p94 p95 p96 p97 p98 p99 p100 p101 p102 p103 p104 p105 p106 p107 p108 p109 p110 p111 p112 p113 p114 p115 p116 p117 p118 p119 p120 p121 p122 p123 p124 p125 p126 p127 p128 p129 p130 p131 p132 p133 p134 p135 p136 p137 p138 p139 p140 p141 p142 p143 p144 p145 p146 p147 p148 p149 p150 p151 p152 p153 p154 p155 p156 p157 p158 p159 p160 p161 }, transitions = { ({p52 p3 p83 p131 p149 p133 p41 p65 p138 p122 p20 p74 p49 p89 } a284 {p50 p3 p57 p131 p149 p135 p41 p68 p139 p122 p20 p22 p72 p89 }) ({p30 p113 p24 } a228 {p112 p25 }) ({p16 } a61 {p73 }) ({p27 p40 p1 p51 p42 p137 p128 p148 p121 p18 p70 p21 p79 } a24 {p78 p2 p53 p130 p58 p132 p151 p40 p42 p43 p102 p159 p121 p18 p124 p21 p144 p79 }) ({p77 p154 p52 p68 p157 p57 p140 p71 p143 p94 } a299 {p63 p155 p52 p156 p57 p141 p142 p37 p74 p94 }) ({p78 p101 p2 p53 p109 p18 p22 p21 p79 } a186 {p27 p78 p2 p53 p108 p18 p21 p79 }) ({p76 p100 p155 p6 p156 p23 p143 p72 p74 p79 } a273 {p76 p154 p6 p157 p36 p23 p143 p72 p74 p79 }) ({p30 p113 p22 p86 } a195 {p27 p112 p86 }) ({p91 p112 } a130 {p92 p113 p75 }) ({p78 p40 p100 p15 p157 p69 p143 p38 p93 } a273 {p76 p42 p31 p6 p157 p70 p20 p36 p143 p93 }) ({p77 p76 p52 p156 p57 p142 p72 p74 p93 } a299 {p76 p52 p156 p57 p142 p37 p72 p74 p93 }) ({p154 p54 p157 p140 p143 p79 } a302 {p28 p155 p156 p141 p142 p79 }) ({p27 p40 p42 p43 p2 p130 p58 p132 p121 p18 p151 p21 p86 } a24 {p2 p130 p58 p132 p151 p40 p42 p43 p102 p121 p18 p21 p79 }) ({p110 p36 } a128 {p111 p61 p39 }) ({p78 p101 p2 p53 p109 p18 p22 p21 p79 } a193 {p27 p78 p2 p53 p108 p18 p21 p79 }) ({p40 p42 p107 p151 p22 p37 p86 } a189 {p27 p40 p42 p106 p151 p86 }) ({p101 p7 p109 p86 } a241 {p108 p8 p86 }) ({p154 p158 p47 p86 } a326 {p29 p156 p152 p86 }) ({p41 p65 p52 p3 p83 p139 p131 p149 p122 p20 p74 p49 p90 } a284 {p50 p3 p57 p131 p149 p41 p68 p139 p122 p20 p22 p72 p90 }) ({p28 p111 p22 p93 } a190 {p27 p110 p93 }) ({p126 p97 p135 p117 p130 p122 p114 } a122 {p98 p136 p128 p119 p138 p129 p88 p115 }) ({p102 p157 p143 p93 } a313 {p45 p157 p143 p93 }) ({p77 p65 p154 p157 p140 p143 p49 p90 } a299 {p43 p155 p156 p57 p58 p141 p142 p72 p37 p90 }) ({p27 p43 p2 p31 p130 p58 p132 p121 p18 p151 p21 p93 } a24 {p2 p130 p58 p132 p151 p40 p43 p102 p121 p18 p21 p23 p93 }) ({p64 p52 p57 p141 p142 p79 } a268 {p52 p103 p57 p140 p143 p79 }) ({p40 p42 p107 p151 p22 p37 p86 } a192 {p27 p40 p42 p106 p151 p86 }) ({p76 p157 p96 p143 p72 p74 p79 } a304 {p76 p101 p157 p143 p72 p74 p79 }) ({p28 p111 p22 p93 } a194 {p27 p110 p93 }) ({p76 p13 p4 p68 p108 p55 p103 p20 p90 } a126 {p100 p15 p4 p55 p109 p69 p19 p95 p74 p93 }) ({p78 p100 p15 p157 p69 p35 p143 p93 } a273 {p76 p41 p6 p157 p70 p20 p36 p23 p143 p93 }) ({p76 p155 p156 p141 p96 p142 p72 p74 p79 } a304 {p76 p101 p154 p157 p140 p143 p72 p74 p79 }) ({p28 p7 p111 } a245 {p110 p8 }) ({p77 p76 p154 p52 p157 p57 p140 p143 p72 p74 p93 } a299 {p76 p155 p52 p156 p57 p141 p142 p37 p72 p74 p93 }) ({p101 p7 p109 p86 } a248 {p108 p8 p86 }) ({p77 p76 p52 p156 p57 p142 p72 p74 p94 } a299 {p76 p52 p156 p57 p142 p37 p72 p74 p94 }) ({p3 p6 p58 p149 p131 p132 p87 p116 p43 p139 p159 p124 p23 p144 p79 } a323 {p26 p145 p117 p12 p80 p44 p60 p160 p133 p125 p82 }) ({p28 p7 p111 } a249 {p110 p8 }) ({p9 } a71 {p32 }) ({p40 p100 p68 p17 p157 p18 p71 p143 p38 p94 } a273 {p63 p11 p42 p31 p157 p21 p36 p143 p74 p94 }) ({p28 p111 p22 p94 } a190 {p27 p110 p94 }) ({p92 p79 } a291 {p99 p79 }) ({p52 p3 p83 p131 p149 p133 p41 p65 p119 p138 p123 p20 p74 p49 p89 } a284 {p50 p3 p57 p131 p149 p135 p41 p68 p139 p120 p122 p20 p22 p72 p89 }) ({p28 p111 p22 p94 } a194 {p27 p110 p94 }) ({p63 p27 p40 p42 p2 p137 p130 p46 p121 p18 p151 p21 p90 } a24 {p2 p55 p130 p58 p132 p151 p40 p42 p43 p102 p121 p18 p71 p21 p90 }) ({p77 p76 p154 p52 p157 p57 p140 p143 p72 p74 p94 } a299 {p76 p155 p52 p156 p57 p141 p142 p37 p72 p74 p94 }) ({p41 p43 p3 p83 p139 p58 p131 p149 p122 p20 p79 } a284 {p41 p43 p3 p139 p58 p131 p149 p122 p20 p22 p79 }) ({p27 p40 p51 p42 p2 p137 p130 p121 p18 p70 p151 p21 p79 } a24 {p78 p2 p53 p130 p58 p132 p151 p40 p42 p43 p102 p121 p18 p21 p79 }) ({p155 p47 p79 } a326 {p29 p157 p79 }) ({p27 p51 p2 p31 p130 p132 p121 p18 p70 p151 p21 p93 } a24 {p78 p2 p53 p130 p58 p132 p151 p40 p43 p102 p121 p18 p21 p23 p93 }) ({p63 p78 p13 p2 p53 p108 p103 p46 p20 p161 p90 } a126 {p100 p1 p51 p15 p4 p55 p109 p70 p19 p95 p71 p93 }) ({p156 p33 p153 p88 p89 } a318 {p154 p66 p34 p90 }) ({p40 p42 p107 p151 p22 p37 p90 } a189 {p27 p40 p42 p106 p151 p90 }) ({p76 p155 p156 p96 p143 p72 p74 p93 } a304 {p76 p101 p154 p157 p143 p72 p74 p93 }) ({p40 p42 p107 p151 p22 p37 p90 } a192 {p27 p40 p42 p106 p151 p90 }) ({p101 p109 p99 p86 } a208 {p108 p9 p86 }) ({p29 p105 p22 p79 } a191 {p27 p104 p79 }) ({p63 p27 p40 p42 p118 p2 p130 p46 p18 p151 p21 p134 p90 } a24 {p2 p55 p130 p58 p132 p151 p116 p40 p42 p43 p102 p121 p18 p71 p21 p90 }) ({p52 p3 p83 p131 p149 p133 p41 p65 p119 p138 p123 p20 p74 p49 p90 } a284 {p50 p3 p57 p131 p149 p135 p41 p68 p139 p120 p122 p20 p22 p72 p90 }) ({p156 p142 p62 p79 } a305 {p30 p156 p142 p79 }) ({p30 p7 p113 } a243 {p8 p112 }) ({p107 p7 p37 } a244 {p106 p8 }) ({p27 p40 p51 p42 p118 p2 p130 p18 p70 p151 p21 p134 p79 } a24 {p78 p2 p53 p130 p58 p132 p151 p116 p40 p42 p43 p102 p121 p18 p21 p79 }) ({p77 p78 p154 p52 p157 p57 p69 p140 p143 p93 } a299 {p76 p155 p52 p156 p57 p70 p141 p142 p37 p93 }) ({p107 p7 p37 } a247 {p106 p8 }) ({p84 p79 } a74 {p85 p79 }) ({p95 } a107 {p96 }) ({p145 p41 p44 p138 p83 p60 p122 p160 p133 p20 p125 p82 } a284 {p0 p127 p3 p147 p149 p131 p135 p41 p67 p139 p122 p20 p48 p22 p82 }) ({p13 p4 p108 p55 p103 p20 p71 p74 p90 } a126 {p100 p15 p4 p55 p109 p19 p95 p71 p74 p93 }) ({p28 p99 p111 } a212 {p110 p9 }) ({p13 p102 p156 p158 p122 p35 p142 p90 } a325 {p41 p6 p156 p158 p19 p122 p142 p23 p79 }) ({p27 p41 p43 p2 p130 p58 p132 p121 p18 p151 p21 p38 p93 } a24 {p2 p130 p58 p132 p151 p35 p42 p43 p102 p121 p18 p21 p93 }) ({p101 p109 p99 p86 } a215 {p108 p9 p86 }) ({p63 p11 p27 p43 p2 p31 p130 p132 p121 p151 p94 } a24 {p2 p6 p130 p58 p132 p151 p40 p43 p102 p18 p121 p71 p23 p93 }) ({p30 p7 p113 } a250 {p8 p112 }) ({p41 p154 p6 p102 p157 p140 p122 p143 p79 } a325 {p41 p155 p6 p156 p141 p122 p142 p79 }) ({p40 p42 p107 p151 p22 p37 p93 } a189 {p27 p40 p42 p106 p151 p93 }) ({p28 p99 p111 } a216 {p110 p9 }) ({p76 p155 p156 p96 p143 p72 p74 p94 } a304 {p76 p101 p154 p157 p143 p72 p74 p94 }) ({p63 p78 p13 p53 p4 p108 p103 p46 p20 p90 } a126 {p100 p51 p15 p4 p55 p109 p70 p19 p95 p71 p93 }) ({p76 p40 p100 p17 p157 p18 p143 p72 p38 p74 p94 } a273 {p11 p76 p42 p31 p157 p21 p36 p143 p72 p74 p94 }) ({p40 p42 p107 p151 p22 p37 p93 } a192 {p27 p40 p42 p106 p151 p93 }) ({p61 } a99 {p54 }) ({p154 p157 p140 p143 p62 p79 } a305 {p155 p30 p156 p141 p142 p79 }) ({p157 p143 p39 p79 } a267 {p91 p157 p143 p79 }) ({p76 p40 p100 p155 p156 p17 p18 p141 p142 p72 p38 p74 p94 } a273 {p76 p31 p36 p11 p42 p154 p157 p140 p21 p143 p72 p74 p94 }) ({p11 p27 p43 p2 p31 p130 p58 p132 p121 p151 p94 } a24 {p2 p6 p130 p58 p132 p151 p40 p43 p102 p18 p121 p23 p93 }) ({p155 p156 p141 p142 p39 p79 } a267 {p91 p154 p157 p140 p143 p79 }) ({p41 p6 p102 p156 p158 p122 p142 p93 } a325 {p41 p6 p156 p158 p122 p142 p79 }) ({p54 p156 p142 p86 } a302 {p28 p156 p142 p86 }) ({p98 p89 } a280 {p14 p89 }) ({p8 } a77 {p47 }) ({p5 p79 } a76 {p7 p79 }) ({p27 p43 p2 p31 p130 p132 p121 p18 p70 p151 p21 p93 } a24 {p78 p2 p130 p58 p132 p151 p40 p43 p102 p121 p18 p21 p23 p93 }) ({p76 p13 p2 p53 p68 p108 p103 p46 p20 p161 p90 } a126 {p100 p1 p51 p15 p4 p55 p109 p69 p19 p95 p74 p93 }) ({p40 p42 p107 p151 p22 p37 p94 } a189 {p27 p40 p42 p106 p151 p94 }) ({p101 p109 p85 p79 } a230 {p81 p108 p79 }) ({p119 p133 p73 p90 } a62 {p139 p132 p59 p122 p116 p90 }) ({p101 p109 p24 p79 } a219 {p108 p25 p79 }) ({p40 p42 p107 p151 p22 p37 p94 } a192 {p27 p40 p42 p106 p151 p94 }) ({p15 p102 p156 p158 p122 p35 p142 p93 } a325 {p41 p6 p156 p158 p122 p20 p142 p23 p79 }) ({p76 p40 p100 p155 p15 p156 p143 p72 p38 p74 p93 } a273 {p76 p42 p154 p31 p6 p157 p20 p36 p143 p72 p74 p93 }) ({p135 p120 p121 p73 p90 } a62 {p118 p138 p59 p123 p134 p90 }) ({p77 p76 p52 p156 p57 p142 p72 p74 p79 } a299 {p76 p52 p156 p57 p142 p37 p72 p74 p79 }) ({p64 p143 p49 p90 } a268 {p43 p57 p103 p143 p90 }) ({p101 p109 p85 p79 } a237 {p81 p108 p79 }) ({p107 p99 p37 } a211 {p106 p9 }) ({p30 p99 p113 } a210 {p112 p9 }) ({p154 p54 p157 p140 p143 p86 } a302 {p28 p155 p156 p141 p142 p86 }) ({p98 p90 } a280 {p14 p90 }) ({p101 p109 p24 p79 } a226 {p108 p25 p79 }) ({p107 p99 p37 } a214 {p106 p9 }) ({p28 p111 p22 p79 } a190 {p27 p110 p79 }) ({p102 p157 p143 p79 } a313 {p45 p157 p143 p79 }) ({p27 p43 p2 p31 p130 p58 p132 p121 p18 p151 p21 p79 } a24 {p2 p130 p58 p132 p151 p40 p43 p102 p121 p18 p21 p23 p79 }) ({p27 p40 p42 p43 p2 p130 p58 p132 p121 p18 p151 p21 p94 } a24 {p2 p130 p58 p132 p151 p40 p42 p43 p102 p121 p18 p21 p93 }) ({p32 p79 } a72 {p24 p79 }) ({p76 p13 p53 p4 p68 p108 p103 p46 p20 p90 } a126 {p100 p51 p15 p4 p55 p109 p69 p19 p95 p74 p93 }) ({p30 p99 p113 } a217 {p112 p9 }) ({p65 p157 p96 p143 p93 } a304 {p101 p157 p58 p72 p143 p93 }) ({p28 p111 p22 p79 } a194 {p27 p110 p79 }) ({p76 p100 p155 p15 p156 p35 p143 p72 p74 p93 } a273 {p76 p41 p154 p6 p157 p20 p36 p23 p143 p72 p74 p93 }) ({p76 p157 p96 p143 p72 p74 p86 } a304 {p76 p101 p157 p143 p72 p74 p86 }) ({p97 p135 p117 p129 p122 p114 } a122 {p98 p136 p119 p138 p129 p88 p115 }) ({p77 p76 p154 p52 p157 p57 p140 p143 p72 p74 p79 } a299 {p76 p155 p52 p156 p57 p141 p142 p37 p72 p74 p79 }) ({p25 } a73 {p84 }) ({p76 p155 p156 p141 p96 p142 p72 p74 p86 } a304 {p76 p101 p154 p157 p140 p143 p72 p74 p86 }) ({p41 p6 p102 p140 p122 p152 p143 p79 } a325 {p41 p6 p158 p141 p122 p142 p79 }) ({p76 p100 p6 p157 p23 p143 p72 p74 p79 } a273 {p76 p6 p157 p36 p23 p143 p72 p74 p79 }) ({p76 p100 p155 p6 p156 p141 p142 p23 p72 p74 p79 } a273 {p76 p154 p6 p157 p140 p36 p23 p143 p72 p74 p79 }) ({p27 p40 p51 p42 p2 p130 p132 p121 p18 p70 p151 p21 p93 } a24 {p78 p2 p53 p130 p58 p132 p151 p40 p42 p43 p102 p121 p18 p21 p93 }) ({p41 p146 p106 p59 p34 p151 } a124 {p64 p107 p148 p56 p150 p35 }) ({p77 p50 p154 p68 p55 p157 p140 p71 p143 p90 } a299 {p63 p52 p155 p156 p46 p141 p142 p37 p74 p90 }) ({p92 p86 } a291 {p99 p86 }) ({p56 } a103 {p77 }) ({p42 p43 p3 p83 p139 p58 p131 p149 p122 p20 p35 p90 } a284 {p41 p43 p3 p139 p58 p131 p149 p122 p20 p22 p38 p90 }) ({p42 p43 p3 p15 p83 p139 p58 p131 p149 p122 p35 p21 p93 } a284 {p3 p58 p131 p149 p38 p41 p43 p17 p139 p122 p20 p22 p94 }) ({p27 p51 p2 p31 p130 p132 p121 p18 p70 p151 p21 p79 } a24 {p78 p2 p53 p130 p58 p132 p151 p40 p43 p102 p121 p18 p21 p23 p79 }) ({p155 p47 p86 } a326 {p29 p157 p86 }) ({p54 p156 p142 p93 } a302 {p28 p156 p142 p93 }) ({p30 p113 p22 p79 } a188 {p27 p112 p79 }) ({p76 p155 p156 p96 p143 p72 p74 p79 } a304 {p76 p101 p154 p157 p143 p72 p74 p79 }) ({p41 p106 p59 p150 p34 } a124 {p64 p107 p56 p150 p35 }) ({p68 p157 p96 p71 p143 p94 } a304 {p63 p101 p157 p143 p74 p94 }) ({p64 p52 p57 p141 p142 p90 } a268 {p52 p103 p57 p140 p143 p90 }) ({p30 p113 p22 p79 } a195 {p27 p112 p79 }) ({p27 p40 p1 p51 p42 p137 p128 p148 p121 p18 p70 p21 p93 } a24 {p78 p2 p53 p130 p58 p132 p151 p40 p42 p43 p102 p159 p121 p18 p124 p21 p144 p93 }) ({p29 p105 p22 p86 } a191 {p27 p104 p86 }) ({p156 p142 p62 p86 } a305 {p30 p156 p142 p86 }) ({p78 p101 p2 p53 p109 p18 p22 p21 p93 } a186 {p27 p78 p2 p53 p108 p18 p21 p93 }) ({p154 p54 p157 p140 p143 p93 } a302 {p28 p155 p156 p141 p142 p93 }) ({p84 p86 } a74 {p85 p86 }) ({p54 p156 p142 p94 } a302 {p28 p156 p142 p94 }) ({p40 p42 p107 p151 p22 p37 p79 } a189 {p27 p40 p42 p106 p151 p79 }) ({p101 p7 p109 p79 } a241 {p108 p8 p79 }) ({p154 p158 p47 p79 } a326 {p29 p156 p152 p79 }) ({p78 p101 p2 p53 p109 p18 p22 p21 p93 } a193 {p27 p78 p2 p53 p108 p18 p21 p93 }) ({p65 p42 p43 p3 p83 p139 p131 p149 p122 p20 p35 p74 p90 } a284 {p3 p131 p149 p38 p41 p43 p68 p139 p122 p20 p22 p72 p90 }) ({p40 p42 p107 p151 p22 p37 p79 } a192 {p27 p40 p42 p106 p151 p79 }) ({p41 p154 p6 p102 p157 p140 p122 p143 p93 } a325 {p41 p155 p6 p156 p141 p122 p142 p79 }) ({p3 p83 p131 p149 p35 p65 p42 p43 p15 p139 p122 p21 p74 p93 } a284 {p3 p131 p149 p38 p41 p43 p68 p17 p139 p122 p20 p22 p72 p94 }) ({p76 p157 p96 p143 p72 p74 p93 } a304 {p76 p101 p157 p143 p72 p74 p93 }) ({p100 p65 p15 p157 p35 p143 p93 } a273 {p41 p6 p157 p58 p20 p36 p72 p23 p143 p93 }) ({p154 p157 p140 p143 p62 p86 } a305 {p155 p30 p156 p141 p142 p86 }) ({p101 p7 p109 p79 } a248 {p108 p8 p79 }) ({p76 p155 p156 p141 p96 p142 p72 p74 p93 } a304 {p76 p101 p154 p157 p140 p143 p72 p74 p93 }) ({p27 p43 p2 p31 p130 p132 p121 p18 p70 p151 p21 p79 } a24 {p78 p2 p130 p58 p132 p151 p40 p43 p102 p121 p18 p21 p23 p79 }) ({p157 p143 p39 p93 } a267 {p91 p157 p143 p79 }) ({p154 p54 p157 p140 p143 p94 } a302 {p28 p155 p156 p141 p142 p94 }) ({p97 p117 p129 p138 p122 p114 } a122 {p98 p119 p129 p138 p88 p115 }) ({p154 p15 p102 p157 p140 p122 p35 p143 p93 } a325 {p41 p155 p6 p156 p141 p122 p20 p142 p23 p79 }) ({p5 p86 } a76 {p7 p86 }) ({p155 p156 p141 p142 p39 p93 } a267 {p91 p154 p157 p140 p143 p79 }) ({p136 p119 p73 p90 } a62 {p137 p59 p122 p116 p90 }) ({p66 p14 p115 } a198 {p16 p114 }) ({p101 p109 p85 p86 } a230 {p81 p108 p86 }) ({p101 p109 p24 p86 } a219 {p108 p25 p86 }) ({p27 p40 p42 p43 p2 p130 p58 p132 p121 p18 p151 p21 p79 } a24 {p2 p130 p58 p132 p151 p40 p42 p43 p102 p121 p18 p21 p79 }) ({p77 p65 p154 p52 p157 p57 p140 p143 p90 } a299 {p155 p52 p156 p57 p58 p141 p142 p72 p37 p90 }) ({p76 p157 p96 p143 p72 p74 p94 } a304 {p76 p101 p157 p143 p72 p74 p94 }) ({p77 p76 p52 p156 p57 p142 p72 p74 p86 } a299 {p76 p52 p156 p57 p142 p37 p72 p74 p86 }) ({p50 p64 p55 p143 p90 } a268 {p52 p103 p46 p143 p90 }) ({p76 p155 p156 p141 p96 p142 p72 p74 p94 } a304 {p76 p101 p154 p157 p140 p143 p72 p74 p94 }) ({p28 p111 p85 } a234 {p81 p110 }) ({p13 p102 p156 p140 p158 p122 p35 p143 p90 } a325 {p41 p6 p156 p158 p19 p141 p122 p142 p23 p79 }) ({p101 p109 p85 p86 } a237 {p81 p108 p86 }) ({p27 p40 p51 p42 p2 p137 p130 p121 p18 p70 p151 p21 p93 } a24 {p78 p2 p53 p130 p58 p132 p151 p40 p42 p43 p102 p121 p18 p21 p93 }) ({p66 p14 p115 } a207 {p16 p114 }) ({p28 p111 p24 } a223 {p110 p25 }) ({p101 p109 p24 p86 } a226 {p108 p25 p86 }) ({p76 p40 p100 p155 p156 p17 p18 p143 p72 p38 p74 p94 } a273 {p11 p76 p42 p154 p31 p157 p21 p36 p143 p72 p74 p94 }) ({p28 p111 p85 } a238 {p81 p110 }) ({p28 p111 p22 p86 } a190 {p27 p110 p86 }) ({p41 p43 p3 p83 p139 p58 p131 p149 p122 p20 p93 } a284 {p41 p43 p3 p139 p58 p131 p149 p122 p20 p22 p94 }) ({p28 p111 p24 } a227 {p110 p25 }) ({p26 p10 p145 p12 p44 p57 p60 p19 p160 p152 p72 p125 p82 } a320 {p97 p3 p33 p149 p131 p153 p65 p13 p158 p159 p124 p49 p144 p89 }) ({p101 p109 p99 p79 } a208 {p108 p9 p79 }) ({p32 p86 } a72 {p24 p86 }) ({p78 p157 p69 p96 p143 p93 } a304 {p76 p101 p157 p70 p143 p93 }) ({p77 p154 p52 p68 p157 p57 p140 p71 p143 p90 } a299 {p63 p155 p52 p156 p57 p141 p142 p37 p74 p90 }) ({p28 p111 p22 p86 } a194 {p27 p110 p86 }) ({p63 p11 p27 p43 p2 p31 p130 p132 p121 p151 p86 } a24 {p2 p6 p130 p58 p132 p151 p40 p43 p102 p18 p121 p71 p23 p79 }) ({p77 p65 p154 p52 p157 p57 p140 p143 p93 } a299 {p155 p52 p156 p57 p58 p141 p142 p72 p37 p93 }) ({p77 p76 p154 p52 p157 p57 p140 p143 p72 p74 p86 } a299 {p76 p155 p52 p156 p57 p141 p142 p37 p72 p74 p86 }) ({p4 p108 p55 p103 p19 p71 p74 p79 } a126 {p100 p4 p55 p109 p95 p19 p71 p74 p79 }) ({p27 p40 p51 p42 p118 p2 p130 p18 p70 p151 p21 p134 p93 } a24 {p78 p2 p53 p130 p58 p132 p151 p116 p40 p42 p43 p102 p121 p18 p21 p93 }) ({p75 } a95 {p62 }) ({p81 } a75 {p5 }) ({p52 p3 p83 p131 p149 p35 p65 p42 p139 p122 p20 p74 p49 p90 } a284 {p50 p3 p57 p131 p149 p38 p41 p68 p139 p122 p20 p22 p72 p90 }) ({p26 p0 p127 p52 p147 p4 p129 p150 p152 p10 p12 p67 p19 p48 p74 p82 } a320 {p126 p97 p50 p146 p13 p68 p33 p158 p161 p153 p89 }) ({p76 p40 p100 p15 p157 p143 p72 p38 p74 p93 } a273 {p76 p42 p31 p6 p157 p20 p36 p143 p72 p74 p93 }) ({p101 p109 p99 p79 } a215 {p108 p9 p79 }) ({p27 p40 p51 p42 p2 p130 p132 p121 p18 p70 p151 p21 p79 } a24 {p78 p2 p53 p130 p58 p132 p151 p40 p42 p43 p102 p121 p18 p21 p79 }) ({p63 p27 p40 p42 p2 p130 p46 p132 p121 p18 p151 p21 p90 } a24 {p2 p55 p130 p58 p132 p151 p40 p42 p43 p102 p121 p18 p71 p21 p90 }) ({p76 p40 p100 p155 p15 p156 p141 p142 p72 p38 p74 p93 } a273 {p76 p31 p6 p36 p42 p154 p157 p140 p20 p143 p72 p74 p93 }) ({p11 p27 p43 p2 p31 p130 p58 p132 p121 p151 p86 } a24 {p2 p6 p130 p58 p132 p151 p40 p43 p102 p18 p121 p23 p79 }) ({p157 p143 p39 p94 } a267 {p91 p157 p143 p86 }) ({p15 p102 p156 p140 p158 p122 p35 p143 p93 } a325 {p41 p6 p156 p158 p141 p122 p20 p142 p23 p79 }) ({p155 p156 p141 p142 p39 p94 } a267 {p91 p154 p157 p140 p143 p86 }) ({p41 p6 p102 p156 p158 p122 p142 p79 } a325 {p41 p6 p156 p158 p122 p142 p79 }) ({p63 p78 p13 p4 p108 p55 p103 p20 p90 } a126 {p100 p15 p4 p55 p109 p70 p19 p95 p71 p93 }) ({p107 p85 p37 } a233 {p81 p106 }) ({p30 p85 p113 } a232 {p81 p112 }) ({p76 p100 p15 p157 p35 p143 p72 p74 p93 } a273 {p76 p41 p6 p157 p20 p36 p23 p143 p72 p74 p93 }) ({p80 p104 p82 } a118 {p10 p105 p83 p82 }) ({p54 p156 p142 p79 } a302 {p28 p156 p142 p79 }) ({p107 p24 p37 } a222 {p106 p25 }) ({p30 p113 p24 } a221 {p112 p25 }) ({p107 p85 p37 } a236 {p81 p106 }) ({p76 p100 p155 p15 p156 p141 p35 p142 p72 p74 p93 } a273 {p76 p6 p36 p41 p154 p157 p140 p20 p23 p143 p72 p74 p93 }) ({p30 p113 p22 p86 } a188 {p27 p112 p86 }) ({p107 p24 p37 } a225 {p106 p25 }) ({p30 p85 p113 } a239 {p81 p112 }) }, initialMarking = {p2 p3 p4 p6 p18 p19 p20 p21 p23 p104 p106 p108 p110 p112 p114 p116 p40 p41 p42 p43 p121 p122 p123 p124 p52 p53 p55 p129 p57 p130 p58 p131 p132 p138 p139 p140 p71 p72 p143 p74 p144 p76 p78 p79 p149 p150 p151 p152 p87 p156 p157 p159 }, acceptingPlaces = {p45 } );