// Testfile dumped by Ultimate at 2012/01/05 14:38:31

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

PetriNet net = (
	alphabet = {a0 a1 a2 a4 a3 a7 a6 a5 a9 a8 a11 a10 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a27 a26 a28 a29 a30 a31 a32 a33 a36 a35 a34 a37 a39 a38 a40 a41 a42 },
	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 },
	transitions = {
		( {p36 p15 p77 } a11 {p74 p13 p19 } )
		( {p29 p27 p67 p58 } a10 {p25 p27 p67 p58 } )
		( {p41 p18 p23 } a1 {p33 p10 p24 } )
		( {p7 p30 p27 p78 p67 p58 } a26 {p38 p56 p55 p40 p39 p58 } )
		( {p21 p71 p64 p51 p46 } a29 {p41 p18 p23 p51 p46 } )
		( {p0 } a7 {p29 } )
		( {p7 p55 p39 p57 p62 } a26 {p38 p55 p39 p61 p58 } )
		( {p54 p4 p3 p43 } a39 {p35 p9 p5 p43 } )
		( {p75 p72 p17 p4 p3 p45 p44 } a17 {p21 p71 p64 p9 p5 p47 p43 } )
		( {p50 p27 p39 p62 } a18 {p7 p27 p39 p62 } )
		( {p53 p47 p43 } a6 {p68 p45 p44 } )
		( {p76 p27 p67 p58 } a9 {p26 p27 p67 p58 } )
		( {p29 p27 p40 p39 p58 } a10 {p25 p27 p78 p67 p58 } )
		( {p26 } a3 {p53 } )
		( {p0 p77 p19 p27 p55 p39 p67 p3 p5 p51 p44 p43 p46 p58 p62 } a4 {p34 p77 p19 p27 p55 p39 p67 p3 p5 p51 p44 p43 p46 p58 p62 } )
		( {p37 p27 p78 p67 p61 p58 } a31 {p0 p27 p40 p39 p57 p62 } )
		( {p76 p27 p67 p57 p62 } a9 {p26 p27 p67 p61 p58 } )
		( {p21 p71 p64 p51 p49 p44 } a29 {p41 p18 p23 p51 p47 p46 } )
		( {p37 p27 p39 p61 p58 } a31 {p0 p27 p39 p57 p62 } )
		( {p75 p72 p17 p4 p3 p43 } a17 {p21 p71 p64 p9 p5 p43 } )
		( {p60 p77 } a25 {p12 p77 } )
		( {p35 p77 p19 p27 p55 p39 p67 p3 p5 p51 p44 p43 p46 p58 p62 } a33 {p73 p77 p19 p27 p55 p39 p67 p3 p5 p51 p44 p43 p46 p58 p62 } )
		( {p1 p30 p27 p39 p58 } a42 {p59 p56 p55 p39 p58 } )
		( {p21 p71 p64 p52 p3 p49 p44 } a29 {p41 p18 p23 p9 p51 p47 p46 } )
		( {p37 p27 p39 p62 } a31 {p0 p27 p39 p62 } )
		( {p11 p4 p3 } a0 {p50 p9 p5 } )
		( {p12 p56 p55 p78 p67 p62 } a20 {p63 p30 p27 p40 p39 p62 } )
		( {p6 p15 p77 } a41 {p60 p13 p19 } )
		( {p76 p56 p55 p40 p39 p57 p62 } a9 {p26 p30 p27 p78 p67 p61 p58 } )
		( {p76 p27 p40 p39 p57 p62 } a9 {p26 p27 p78 p67 p61 p58 } )
		( {p7 p30 p27 p39 p57 p62 } a26 {p38 p56 p55 p39 p61 p58 } )
		( {p59 p19 } a5 {p16 p19 } )
		( {p70 p27 p40 p39 p58 } a28 {p25 p27 p78 p67 p58 } )
		( {p7 p55 p78 p67 p57 p62 } a26 {p38 p55 p40 p39 p61 p58 } )
		( {p1 p55 p39 p58 } a42 {p59 p55 p39 p58 } )
		( {p38 } a37 {p20 } )
		( {p54 p4 p3 p45 p44 } a39 {p35 p9 p5 p47 p43 } )
		( {p54 p5 p43 } a39 {p35 p5 p43 } )
		( {p59 p13 p19 } a15 {p6 p15 p77 } )
		( {p74 p13 p19 } a23 {p37 p15 p77 } )
		( {p76 p56 p55 p67 p57 p62 } a9 {p26 p30 p27 p67 p61 p58 } )
		( {p7 p30 p27 p78 p67 p57 p62 } a26 {p38 p56 p55 p40 p39 p61 p58 } )
		( {p74 p77 } a23 {p37 p77 } )
		( {p12 p56 p55 p78 p67 p61 p58 } a20 {p63 p30 p27 p40 p39 p57 p62 } )
		( {p53 p44 } a6 {p68 p44 } )
		( {p29 p39 } a13 {p69 p39 } )
		( {p68 p43 } a40 {p70 p43 } )
		( {p7 p30 p27 p39 p58 } a26 {p38 p56 p55 p39 p58 } )
		( {p25 p77 } a36 {p36 p77 } )
		( {p25 p13 p19 } a36 {p36 p15 p77 } )
		( {p36 p19 } a11 {p74 p19 } )
		( {p65 } a38 {p66 } )
		( {p76 p56 p55 p67 p58 } a9 {p26 p30 p27 p67 p58 } )
		( {p42 p32 p8 p13 p19 } a2 {p75 p72 p17 p15 p77 } )
		( {p37 p56 p55 p78 p67 p61 p58 } a31 {p0 p30 p27 p40 p39 p57 p62 } )
		( {p73 } a14 {p48 } )
		( {p75 p72 p17 p5 p43 } a17 {p21 p71 p64 p5 p43 } )
		( {p25 p19 } a19 {p22 p19 } )
		( {p2 p27 p39 p62 } a35 {p76 p27 p39 p62 } )
		( {p12 p27 p78 p67 p61 p58 } a20 {p63 p27 p40 p39 p57 p62 } )
		( {p7 p55 p39 p58 } a26 {p38 p55 p39 p58 } )
		( {p63 p77 p19 p27 p55 p39 p67 p3 p5 p51 p44 p43 p46 p58 p62 } a12 {p65 p77 p19 p27 p55 p39 p67 p3 p5 p51 p44 p43 p46 p58 p62 } )
		( {p63 } a34 {p31 } )
		( {p31 p30 p27 p39 p58 } a8 {p59 p56 p55 p39 p58 } )
		( {p11 p5 } a0 {p50 p5 } )
		( {p7 p55 p78 p67 p58 } a26 {p38 p55 p40 p39 p58 } )
		( {p37 p27 p78 p67 p62 } a31 {p0 p27 p40 p39 p62 } )
		( {p50 p27 p39 p61 p58 } a18 {p7 p27 p39 p57 p62 } )
		( {p33 p10 p24 } a27 {p0 p35 p63 } )
		( {p37 p56 p55 p39 p62 } a31 {p0 p30 p27 p39 p62 } )
		( {p14 p5 } a32 {p1 p5 } )
		( {p69 p43 } a30 {p2 p43 } )
		( {p2 p27 p39 p61 p58 } a35 {p76 p27 p39 p57 p62 } )
		( {p37 p56 p55 p39 p61 p58 } a31 {p0 p30 p27 p39 p57 p62 } )
		( {p54 p5 p45 p44 } a39 {p35 p5 p47 p43 } )
		( {p12 p27 p39 p62 } a20 {p63 p27 p39 p62 } )
		( {p76 p56 p55 p40 p39 p58 } a9 {p26 p30 p27 p78 p67 p58 } )
		( {p60 p13 p19 } a25 {p12 p15 p77 } )
		( {p20 p9 p5 } a16 {p14 p4 p3 } )
		( {p37 p56 p55 p78 p67 p62 } a31 {p0 p30 p27 p40 p39 p62 } )
		( {p35 } a22 {p54 } )
		( {p21 p71 p64 p52 p3 p46 } a29 {p41 p18 p23 p9 p51 p46 } )
		( {p12 p56 p55 p39 p62 } a20 {p63 p30 p27 p39 p62 } )
		( {p59 p77 } a15 {p6 p77 } )
		( {p69 p45 p44 } a30 {p2 p47 p43 } )
		( {p12 p27 p39 p61 p58 } a20 {p63 p27 p39 p57 p62 } )
		( {p42 p32 p8 p77 } a2 {p75 p72 p17 p77 } )
		( {p20 p3 } a16 {p14 p3 } )
		( {p31 p55 p39 p58 } a8 {p59 p55 p39 p58 } )
		( {p75 p72 p17 p5 p45 p44 } a17 {p21 p71 p64 p5 p47 p43 } )
		( {p12 p56 p55 p39 p61 p58 } a20 {p63 p30 p27 p39 p57 p62 } )
		( {p31 p27 } a21 {p11 p27 } )
		( {p6 p19 } a41 {p60 p19 } )
		( {p12 p27 p78 p67 p62 } a20 {p63 p27 p40 p39 p62 } )
		( {p34 } a24 {p28 } )
		( {p70 p27 p67 p58 } a28 {p25 p27 p67 p58 } )
		( {p76 p27 p40 p39 p58 } a9 {p26 p27 p78 p67 p58 } )
	},
	initialMarking = {p27 p3 p30 p5 p32 p8 p58 p13 p61 p39 p40 p42 p43 p19 p44 p49 p52 },
	acceptingPlaces = {p16 p22 }
);