// Testfile dumped by Ultimate at 2018/11/13 15:40:28
//
// Not on-demand
// mix000_power.oepc_false-unreach-call.i_BEv2_AllErrorsAtOnce_Iteration1_AbstractionAfterDifference.ats

BranchingProcess bp = finitePrefix(net);
assert(numberOfConditions(bp) == 80446);

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 },
	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 p162 p163 p164 p165 p166 p167 p168 p169 p170 p171 p172 p173 p174 p175 p176 p177 p178 p179 p180 p181 p182 p183 p184 p185 p186 p187 p188 p189 p190 p191 p192 p193 p194 p195 p196 p197 p198 p199 p200 p201 p202 p203 p204 p205 p206 p207 p208 p209 p210 p211 p212 p213 p214 p215 p216 p217 p218 p219 },
	transitions = {
		({p214 p216 p218 p219 p104 } a67 {p214 p216 p218 p101 p219 })
		({p181 } a85 {p174 })
		({p43 } a55 {p44 })
		({p147 } a125 {p2 })
		({p4 } a240 {p1 })
		({p154 } a76 {p157 })
		({p52 } a230 {p63 })
		({p126 } a146 {p34 })
		({p86 } a185 {p81 })
		({p141 } a80 {p181 })
		({p123 } a208 {p193 })
		({p69 } a48 {p75 })
		({p212 p213 p16 p215 p217 } a156 {p212 p213 p215 p217 p72 })
		({p214 p216 p218 p219 p43 } a54 {p44 p214 p216 p218 p219 })
		({p1 } a243 {p8 })
		({p189 p214 p208 p198 } a148 {p190 p206 p216 p199 p186 })
		({p179 } a16 {p178 })
		({p28 } a158 {p97 })
		({p61 } a231 {p122 })
		({p96 } a194 {p58 })
		({p97 } a195 {p56 })
		({p178 } a10 {p183 })
		({p214 p1 p216 p218 p219 } a244 {p214 p216 p218 p5 p219 })
		({p31 } a116 {p153 })
		({p72 } a177 {p123 })
		({p174 p214 p216 p218 p219 } a91 {p214 p216 p218 p219 p187 })
		({p86 } a184 {p85 })
		({p45 } a165 {p48 })
		({p215 p184 p211 } a89 {p207 p219 p135 })
		({p124 } a209 {p194 })
		({p45 } a166 {p48 })
		({p214 p216 p218 p69 p219 } a47 {p214 p216 p218 p219 p75 })
		({p23 } a41 {p21 })
		({p21 } a37 {p27 })
		({p29 } a159 {p98 })
		({p42 } a72 {p154 })
		({p36 } a245 {p166 })
		({p49 } a170 {p39 })
		({p153 } a120 {p147 })
		({p46 } a167 {p47 })
		({p73 } a178 {p124 })
		({p153 } a121 {p147 })
		({p181 } a84 {p184 })
		({p215 p217 p52 p218 p219 } a229 {p61 p215 p217 p218 p219 })
		({p22 } a124 {p24 })
		({p214 p216 p218 p219 p88 } a187 {p79 p214 p216 p218 p219 })
		({p176 } a222 {p0 })
		({p217 p210 p184 } a89 {p218 p209 p135 })
		({p121 } a145 {p126 })
		({p127 p214 p216 p218 p219 } a100 {p214 p216 p131 p218 p219 })
		({p214 p216 p218 p219 p183 } a4 {p214 p216 p218 p219 p107 })
		({p212 p206 p183 } a4 {p204 p214 p107 })
		({p214 p216 p218 p219 p22 } a123 {p214 p216 p218 p219 p24 })
		({p155 } a251 {p167 })
		({p189 p215 p209 p198 } a148 {p190 p207 p217 p199 p186 })
		({p214 p216 p218 p219 p155 } a252 {p214 p216 p163 p218 p219 })
		({p3 } a70 {p14 })
		({p81 } a181 {p32 })
		({p219 p210 p10 p202 } a150 {p12 p218 p149 p211 p203 })
		({p5 } a249 {p9 })
		({p182 } a95 {p184 })
		({p168 } a86 {p141 })
		({p214 p216 p218 p219 p26 } a118 {p214 p216 p218 p219 p22 })
		({p89 } a189 {p87 })
		({p4 } a239 {p17 })
		({p135 } a94 {p127 })
		({p127 } a99 {p140 })
		({p180 } a136 {p173 })
		({p214 p216 p218 p5 p219 } a248 {p214 p216 p218 p219 p9 })
		({p180 } a137 {p173 })
		({p58 } a175 {p176 })
		({p55 } a30 {p51 })
		({p107 } a9 {p110 })
		({p156 p215 p211 } a135 {p207 p180 p219 })
		({p26 } a117 {p30 })
		({p130 } a21 {p136 })
		({p189 p213 p216 p217 p218 } a149 {p213 p192 p216 p217 p218 })
		({p24 } a126 {p30 })
		({p157 } a81 {p168 })
		({p88 } a188 {p94 })
		({p129 } a49 {p128 })
		({p214 p216 p218 p219 p55 } a29 {p214 p216 p51 p218 p219 })
		({p134 } a19 {p132 })
		({p9 } a253 {p8 })
		({p156 p217 p210 } a135 {p218 p180 p209 })
		({p214 p130 p216 p218 p219 } a20 {p214 p216 p218 p219 p136 })
		({p83 } a27 {p78 })
		({p51 } a34 {p62 })
		({p132 } a13 {p67 })
		({p163 } a3 {p160 })
		({p213 p208 p183 } a4 {p205 p216 p107 })
		({p92 } a190 {p89 })
		({p157 p214 p216 p218 p219 } a82 {p214 p216 p218 p219 p169 })
		({p56 } a174 {p114 })
		({p50 } a172 {p54 })
		({p212 p207 p186 } a228 {p204 p215 p52 })
		({p195 } a0 {p177 })
		({p214 p216 p218 p219 p75 } a50 {p214 p82 p216 p218 p219 })
		({p38 } a162 {p16 })
		({p212 p206 p75 } a50 {p204 p214 p82 })
		({p131 } a106 {p139 })
		({p78 p214 p216 p218 p219 } a33 {p214 p216 p84 p218 p219 })
		({p68 } a176 {p6 })
		({p114 } a202 {p175 })
		({p44 } a56 {p142 })
		({p135 } a93 {p138 })
		({p160 } a7 {p167 })
		({p8 } a247 {p17 })
		({p79 } a180 {p50 })
		({p214 p216 p163 p218 p219 } a2 {p160 p214 p216 p218 p219 })
		({p6 } a153 {p96 })
		({p204 p186 } a228 {p204 p52 })
		({p214 p216 p218 p219 p54 } a173 {p214 p216 p218 p117 p219 })
		({p212 p206 p54 } a173 {p204 p214 p117 })
		({p33 } a161 {p105 })
		({p214 p50 p216 p218 p219 } a171 {p214 p216 p218 p219 p54 })
		({p106 } a43 {p108 })
		({p53 } a115 {p64 })
		({p85 } a182 {p185 })
		({p214 p216 p131 p218 p219 } a105 {p214 p216 p218 p219 p139 })
		({p30 } a122 {p31 })
		({p144 } a211 {p95 })
		({p136 } a25 {p134 })
		({p152 } a214 {p151 })
		({p82 } a51 {p77 })
		({p213 p216 p217 p218 p10 p202 } a150 {p12 p213 p216 p217 p218 p149 p203 })
		({p82 } a52 {p77 })
		({p204 p214 p16 } a156 {p212 p206 p72 })
		({p195 } a254 {p183 })
		({p128 } a44 {p69 })
		({p111 } a199 {p189 })
		({p78 } a32 {p21 })
		({p187 } a97 {p191 })
		({p191 } a101 {p182 })
		({p206 p215 p186 } a228 {p207 p214 p52 })
		({p32 } a160 {p113 })
		({p60 p214 p216 p218 p219 } a109 {p214 p216 p218 p53 p219 })
		({p214 p216 p218 p53 p219 } a114 {p64 p214 p216 p218 p219 })
		({p214 p2 p216 p218 p219 } a127 {p214 p216 p218 p219 p7 })
		({p40 } a164 {p19 })
		({p205 p186 } a228 {p205 p52 })
		({p125 } a210 {p146 })
		({p25 } a62 {p109 })
		({p150 } a40 {p106 })
		({p19 } a157 {p73 })
		({p100 } a197 {p79 })
		({p112 } a200 {p188 })
		({p95 } a193 {p92 })
		({p12 } a154 {p15 })
		({p214 p216 p218 p219 p187 } a96 {p191 p214 p216 p218 p219 })
		({p2 } a128 {p13 })
		({p205 p212 p10 p202 } a150 {p204 p12 p213 p149 p203 })
		({p167 } a1 {p166 })
		({p62 } a28 {p57 })
		({p59 } a144 {p121 })
		({p189 p219 p198 p210 } a148 {p190 p218 p199 p211 p186 })
		({p113 } a201 {p115 })
		({p213 p208 p75 } a50 {p205 p216 p82 })
		({p102 } a236 {p4 })
		({p0 } a152 {p125 })
		({p173 } a138 {p133 })
		({p145 } a212 {p28 })
		({p15 } a155 {p159 })
		({p165 } a92 {p168 })
		({p90 } a234 {p102 })
		({p94 } a191 {p100 })
		({p213 p208 p54 } a173 {p205 p216 p117 })
		({p94 } a192 {p100 })
		({p107 } a8 {p132 })
		({p80 } a112 {p26 })
		({p103 } a66 {p3 })
		({p60 } a108 {p65 })
		({p214 p216 p218 p219 p90 } a235 {p214 p216 p99 p218 p219 })
		({p138 } a98 {p71 })
		({p213 p209 p186 } a228 {p205 p217 p52 })
		({p140 } a104 {p138 })
		({p67 } a17 {p57 })
		({p3 } a69 {p42 })
		({p35 } a61 {p25 })
		({p169 } a88 {p165 })
		({p87 } a186 {p118 })
		({p41 } a77 {p42 })
		({p133 } a140 {p137 })
		({p205 p16 p216 } a156 {p213 p208 p72 })
		({p146 } a213 {p29 })
		({p164 } a133 {p156 })
		({p171 } a219 {p45 })
		({p116 } a204 {p40 })
		({p148 } a59 {p37 })
		({p139 } a110 {p140 })
		({p214 p216 p218 p219 p184 } a89 {p214 p216 p218 p219 p135 })
		({p91 } a64 {p103 })
		({p212 p206 p184 } a89 {p204 p214 p135 })
		({p83 } a26 {p27 })
		({p80 } a111 {p31 })
		({p175 } a221 {p38 })
		({p39 } a163 {p33 })
		({p214 p216 p218 p219 p169 } a87 {p214 p216 p218 p165 p219 })
		({p14 p214 p216 p218 p219 } a74 {p214 p216 p20 p218 p219 })
		({p214 p216 p218 p133 p219 } a139 {p214 p216 p218 p219 p137 })
		({p20 } a79 {p11 })
		({p172 } a220 {p46 })
		({p214 p216 p164 p218 p219 } a132 {p156 p214 p216 p218 p219 })
		({p47 } a168 {p10 })
		({p117 } a205 {p112 })
		({p215 p183 p211 } a4 {p207 p219 p107 })
		({p117 } a206 {p112 })
		({p93 } a241 {p102 })
		({p84 } a39 {p23 })
		({p208 p217 p186 } a228 {p216 p52 p209 })
		({p99 } a238 {p93 })
		({p115 } a203 {p49 })
		({p118 } a207 {p111 })
		({p193 } a226 {p144 })
		({p214 p216 p218 p219 p91 } a65 {p214 p216 p218 p219 p104 })
		({p214 p216 p20 p218 p219 } a78 {p214 p216 p218 p219 p11 })
		({p63 } a233 {p90 })
		({p105 } a198 {p152 })
		({p7 } a129 {p164 })
		({p110 } a14 {p134 })
		({p57 } a22 {p83 })
		({p110 p214 p216 p218 p219 } a15 {p214 p130 p216 p218 p219 })
		({p48 } a169 {p158 })
		({p217 p183 p210 } a4 {p218 p209 p107 })
		({p214 p216 p84 p218 p219 } a38 {p214 p216 p218 p219 p23 })
		({p214 p216 p99 p218 p219 } a237 {p93 p214 p216 p218 p219 })
		({p76 } a179 {p86 })
		({p162 } a218 {p76 })
		({p64 } a119 {p65 })
		({p214 p216 p218 p219 p106 } a42 {p128 p214 p216 p218 p219 })
		({p65 } a113 {p66 })
		({p158 } a215 {p161 })
		({p194 } a227 {p145 })
		({p214 p208 p10 p202 } a150 {p12 p206 p216 p149 p203 })
		({p213 p216 p217 p218 p10 } a151 {p213 p216 p217 p218 p119 })
		({p189 p213 p216 p217 p218 p198 } a148 {p190 p213 p216 p217 p218 p199 p186 })
		({p71 } a103 {p60 })
		({p37 } a60 {p35 })
		({p108 } a45 {p129 })
		({p108 } a46 {p129 })
		({p213 p208 p184 } a89 {p205 p216 p135 })
		({p137 } a141 {p70 })
		({p159 } a216 {p88 })
		({p156 p214 p216 p218 p219 } a135 {p214 p216 p180 p218 p219 })
		({p156 p212 p206 } a135 {p204 p214 p180 })
		({p154 } a75 {p141 })
		({p215 p211 p186 } a228 {p207 p52 p219 })
		({p67 } a18 {p74 })
		({p27 } a31 {p143 })
		({p214 p216 p218 p219 p74 } a24 {p214 p216 p218 p219 p55 })
		({p71 } a102 {p66 })
		({p188 } a224 {p171 })
		({p189 p205 p212 p198 } a148 {p204 p190 p213 p199 p186 })
		({p170 } a12 {p179 })
		({p17 } a242 {p36 })
		({p166 } a250 {p195 })
		({p215 p211 p75 } a50 {p207 p82 p219 })
		({p11 } a83 {p41 })
		({p77 } a53 {p43 })
		({p161 } a217 {p162 })
		({p74 } a23 {p62 })
		({p207 p16 p219 } a156 {p215 p72 p211 })
		({p217 p210 p186 } a228 {p218 p52 p209 })
		({p13 } a130 {p18 })
		({p18 } a134 {p7 })
		({p13 } a131 {p18 })
		({p14 } a73 {p41 })
		({p215 p209 p10 p202 } a150 {p12 p207 p217 p149 p203 })
		({p188 p214 p216 p218 p219 } a223 {p214 p216 p218 p219 p171 })
		({p215 p54 p211 } a173 {p207 p219 p117 })
		({p214 p216 p218 p219 p170 } a11 {p214 p216 p179 p218 p219 })
		({p143 } a35 {p150 })
		({p34 } a147 {p120 })
		({p143 } a36 {p150 })
		({p217 p210 p75 } a50 {p82 p218 p209 })
		({p214 p177 p216 p218 p219 } a6 {p214 p216 p218 p219 p170 })
		({p101 } a71 {p103 })
		({p66 } a107 {p80 })
		({p149 } a63 {p91 })
		({p98 } a196 {p116 })
		({p190 } a225 {p172 })
		({p217 p54 p210 } a173 {p218 p209 p117 })
		({p70 } a142 {p59 })
		({p104 } a68 {p101 })
		({p70 } a143 {p59 })
		({p156 p213 p208 } a135 {p205 p216 p180 })
		({p177 } a5 {p178 })
		({p174 } a90 {p182 })
		({p142 } a57 {p148 })
		({p16 p218 p209 } a156 {p217 p210 p72 })
		({p142 } a58 {p148 })
		({p36 } a246 {p155 })
	},
	initialMarking = {p212 p214 p215 p216 p217 p68 p196 p218 p219 p198 p200 p202 p205 },
	acceptingPlaces = {p185 p122 }
);