// Testfile dumped by Ultimate at 2012/01/05 14:34:50

assert(!isEmpty(net));
print(net);

PetriNet net = (
	alphabet = {a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a16 a15 a17 a18 a19 a20 a21 a22 a23 },
	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 },
	transitions = {
		( {p45 p14 p7 p23 p16 } a18 {p8 p17 p6 p23 p16 } )
		( {p26 p29 p15 p22 p16 } a16 {p33 p29 p15 p24 p23 } )
		( {p40 p14 p1 } a21 {p32 p2 p6 } )
		( {p41 p27 p28 p29 p14 p15 p24 p23 } a4 {p30 p5 p34 p35 p0 p6 p22 p16 } )
		( {p43 p2 p15 } a9 {p42 p0 p1 } )
		( {p13 p28 p29 p17 p15 p16 } a2 {p38 p34 p35 p0 p7 p16 } )
		( {p3 p29 p15 p22 p16 } a10 {p13 p29 p15 p24 p23 } )
		( {p41 p27 p28 p29 p6 p7 p16 } a4 {p30 p5 p34 p35 p6 p7 p16 } )
		( {p31 p28 p29 p6 p7 p16 } a6 {p26 p34 p35 p6 p7 p16 } )
		( {p33 p28 p29 p17 p15 p16 } a5 {p40 p34 p35 p0 p7 p16 } )
		( {p11 } a15 {p12 } )
		( {p9 } a14 {p10 } )
		( {p41 p27 p28 p29 p6 p7 p24 p23 } a4 {p30 p5 p34 p35 p6 p7 p22 p16 } )
		( {p3 p34 p35 p0 p6 p22 p16 } a10 {p13 p28 p29 p14 p15 p24 p23 } )
		( {p26 p29 p15 p23 } a16 {p33 p29 p15 p23 } )
		( {p26 p34 p35 p0 p6 p22 p16 } a16 {p33 p28 p29 p14 p15 p24 p23 } )
		( {p26 p34 p35 p0 p6 p23 } a16 {p33 p28 p29 p14 p15 p23 } )
		( {p31 p35 p6 p7 p16 } a6 {p26 p35 p6 p7 p16 } )
		( {p42 p7 p20 p23 } a13 {p36 p7 p22 p21 } )
		( {p3 p34 p35 p15 p22 p16 } a10 {p13 p28 p29 p15 p24 p23 } )
		( {p31 p29 } a8 {p44 p29 } )
		( {p40 p0 p1 } a21 {p32 p2 p15 } )
		( {p41 p27 p35 p6 p7 p16 } a4 {p30 p5 p35 p6 p7 p16 } )
		( {p26 p29 p0 p6 p23 } a16 {p33 p29 p14 p15 p23 } )
		( {p41 p27 p35 p17 p15 p16 } a4 {p30 p5 p35 p0 p7 p16 } )
		( {p45 p6 p24 p21 } a18 {p8 p6 p20 p16 } )
		( {p38 p24 p19 } a20 {p9 p18 p16 } )
		( {p33 p35 p14 p15 p16 } a5 {p40 p35 p0 p6 p16 } )
		( {p40 p17 p1 } a21 {p32 p2 p7 } )
		( {p3 p29 p0 p6 p23 } a10 {p13 p29 p14 p15 p23 } )
		( {p13 p35 p14 p15 p16 } a2 {p38 p35 p0 p6 p16 } )
		( {p13 p28 p29 p6 p7 p16 } a2 {p38 p34 p35 p6 p7 p16 } )
		( {p41 p27 p35 p14 p15 p24 p23 } a4 {p30 p5 p35 p0 p6 p22 p16 } )
		( {p30 p5 } a0 {p32 p9 } )
		( {p9 p35 p29 p15 p6 p1 p7 p21 p23 p19 p16 } a7 {p11 p35 p29 p15 p6 p1 p7 p21 p23 p19 p16 } )
		( {p33 p35 p14 p15 p24 p23 } a5 {p40 p35 p0 p6 p22 p16 } )
		( {p45 p14 p7 p22 p21 } a18 {p8 p17 p6 p20 p23 } )
		( {p13 p35 p6 p7 p16 } a2 {p38 p35 p6 p7 p16 } )
		( {p26 p29 p0 p6 p22 p16 } a16 {p33 p29 p14 p15 p24 p23 } )
		( {p3 p34 p35 p0 p6 p23 } a10 {p13 p28 p29 p14 p15 p23 } )
		( {p13 p28 p29 p17 p15 p24 p23 } a2 {p38 p34 p35 p0 p7 p22 p16 } )
		( {p33 p35 p6 p7 p16 } a5 {p40 p35 p6 p7 p16 } )
		( {p41 p27 p28 p29 p17 p15 p24 p23 } a4 {p30 p5 p34 p35 p0 p7 p22 p16 } )
		( {p38 p22 p19 } a20 {p9 p18 p23 } )
		( {p42 p7 p21 } a13 {p36 p7 p21 } )
		( {p33 p35 p6 p7 p24 p23 } a5 {p40 p35 p6 p7 p22 p16 } )
		( {p8 p7 } a22 {p39 p7 } )
		( {p33 p28 p29 p17 p15 p24 p23 } a5 {p40 p34 p35 p0 p7 p22 p16 } )
		( {p42 p17 p6 p21 } a13 {p36 p14 p7 p21 } )
		( {p42 p17 p6 p20 p23 } a13 {p36 p14 p7 p22 p21 } )
		( {p10 p18 p21 } a12 {p45 p20 p19 } )
		( {p13 p35 p14 p15 p24 p23 } a2 {p38 p35 p0 p6 p22 p16 } )
		( {p13 p28 p29 p6 p7 p24 p23 } a2 {p38 p34 p35 p6 p7 p22 p16 } )
		( {p41 p27 p28 p29 p17 p15 p16 } a4 {p30 p5 p34 p35 p0 p7 p16 } )
		( {p33 p35 p17 p15 p24 p23 } a5 {p40 p35 p0 p7 p22 p16 } )
		( {p33 p28 p29 p6 p7 p24 p23 } a5 {p40 p34 p35 p6 p7 p22 p16 } )
		( {p40 p15 p6 p7 } a21 {p32 p15 p6 p7 } )
		( {p41 p27 p35 p14 p15 p16 } a4 {p30 p5 p35 p0 p6 p16 } )
		( {p13 p35 p17 p15 p16 } a2 {p38 p35 p0 p7 p16 } )
		( {p26 p34 p35 p15 p23 } a16 {p33 p28 p29 p15 p23 } )
		( {p45 p6 p22 p21 } a18 {p8 p6 p20 p23 } )
		( {p43 p1 } a9 {p42 p1 } )
		( {p13 p35 p17 p15 p24 p23 } a2 {p38 p35 p0 p7 p22 p16 } )
		( {p38 p21 p23 p16 } a20 {p9 p21 p23 p16 } )
		( {p37 } a17 {p25 } )
		( {p41 p27 p35 p6 p7 p24 p23 } a4 {p30 p5 p35 p6 p7 p22 p16 } )
		( {p3 p34 p35 p15 p23 } a10 {p13 p28 p29 p15 p23 } )
		( {p36 p23 p16 } a11 {p31 p23 p16 } )
		( {p33 p28 p29 p6 p7 p16 } a5 {p40 p34 p35 p6 p7 p16 } )
		( {p39 p29 } a23 {p4 p29 } )
		( {p13 p35 p6 p7 p24 p23 } a2 {p38 p35 p6 p7 p22 p16 } )
		( {p45 p6 p23 p16 } a18 {p8 p6 p23 p16 } )
		( {p33 p35 p17 p15 p16 } a5 {p40 p35 p0 p7 p16 } )
		( {p10 p19 } a12 {p45 p19 } )
		( {p45 p14 p7 p24 p21 } a18 {p8 p17 p6 p20 p16 } )
		( {p13 p28 p29 p14 p15 p24 p23 } a2 {p38 p34 p35 p0 p6 p22 p16 } )
		( {p32 p35 p29 p15 p6 p1 p7 p21 p23 p19 p16 } a3 {p37 p35 p29 p15 p6 p1 p7 p21 p23 p19 p16 } )
		( {p32 } a19 {p43 } )
		( {p33 p28 p29 p14 p15 p24 p23 } a5 {p40 p34 p35 p0 p6 p22 p16 } )
		( {p33 p28 p29 p14 p15 p16 } a5 {p40 p34 p35 p0 p6 p16 } )
		( {p41 p27 p35 p17 p15 p24 p23 } a4 {p30 p5 p35 p0 p7 p22 p16 } )
		( {p3 p29 p15 p23 } a10 {p13 p29 p15 p23 } )
		( {p41 p27 p28 p29 p14 p15 p16 } a4 {p30 p5 p34 p35 p0 p6 p16 } )
		( {p39 p35 p6 p7 p16 } a1 {p3 p35 p6 p7 p16 } )
		( {p13 p28 p29 p14 p15 p16 } a2 {p38 p34 p35 p0 p6 p16 } )
		( {p38 p20 p19 } a20 {p9 p18 p21 } )
		( {p3 p29 p0 p6 p22 p16 } a10 {p13 p29 p14 p15 p24 p23 } )
		( {p39 p28 p29 p6 p7 p16 } a1 {p3 p34 p35 p6 p7 p16 } )
		( {p26 p34 p35 p15 p22 p16 } a16 {p33 p28 p29 p15 p24 p23 } )
	},
	initialMarking = {p16 p2 p6 p7 p18 p27 p41 p28 p21 p29 p23 p15 },
	acceptingPlaces = {p4 p44 }
);