// Testfile dumped by Ultimate at 2018/11/06 15:19:12 // // PetriNet difference = difference(net, nwa, "HEURISTIC"); assert(!isEmpty(difference)); assert(numberOfTransitions(difference) == 1641); assert(numberOfPlaces(difference) == 240); PetriNet differencePod = differencePairwiseOnDemand(net, nwa); assert(!isEmpty(differencePod)); assert(numberOfTransitions(differencePod) == 229); assert(numberOfPlaces(differencePod) == 212); PetriNet net = ( alphabet = {"a33" "a32" "a35" "a34" "a37" "a36" "a39" "a38" "a40" "a42" "a41" "a44" "a43" "a46" "a45" "a48" "a47" "a49" "a51" "a50" "a53" "a52" "a11" "a55" "a10" "a54" "a13" "a57" "a12" "a56" "a15" "a59" "a14" "a58" "a17" "a16" "a19" "a18" "a60" "a62" "a61" "a20" "a64" "a63" "a22" "a66" "a21" "a65" "a24" "a68" "a23" "a67" "a26" "a25" "a69" "a28" "a27" "a29" "a0" "a1" "a2" "a3" "a4" "a5" "a6" "a7" "a8" "a9" "a31" "a30" }, places = {"p160" "p164" "p163" "p157" "p156" "p155" "p154" "p159" "p158" "p153" "p152" "p151" "p150" "p146" "p145" "p144" "p143" "p149" "p148" "p147" "p182" "p181" "p180" "p186" "p183" "p175" "p172" "p167" "p165" "p10" "p12" "p11" "p199" "p14" "p198" "p13" "p16" "p15" "p18" "p17" "p19" "p193" "p192" "p191" "p190" "p197" "p196" "p195" "p21" "p20" "p194" "p23" "p189" "p22" "p25" "p24" "p27" "p26" "p29" "p28" "p30" "p32" "p31" "p34" "p33" "p36" "p35" "p38" "p37" "p39" "p41" "p40" "p43" "p42" "p45" "p44" "p47" "p46" "p49" "p48" "p50" "p52" "p51" "p54" "p53" "p56" "p55" "p58" "p57" "p59" "p61" "p60" "p63" "p62" "p65" "p64" "p67" "p66" "p69" "p68" "p70" "p72" "p71" "p74" "p73" "p76" "p75" "p78" "p212" "p77" "p211" "p210" "p79" "p216" "p215" "p214" "p213" "p217" "p81" "p80" "p83" "p82" "p85" "p84" "p87" "p86" "p89" "p201" "p88" "p200" "p205" "p204" "p203" "p202" "p209" "p208" "p207" "p90" "p92" "p91" "p94" "p93" "p96" "p120" "p95" "p98" "p97" "p113" "p112" "p99" "p111" "p110" "p117" "p116" "p115" "p114" "p119" "p118" "p102" "p101" "p100" "p106" "p105" "p104" "p103" "p109" "p108" "p107" "p0" "p1" "p2" "p3" "p4" "p5" "p6" "p7" "p8" "p9" "p142" "p141" "p140" "p135" "p134" "p133" "p132" "p139" "p138" "p137" "p136" "p131" "p130" "p124" "p123" "p122" "p121" "p128" "p127" "p126" "p125" "p129" }, transitions = { ({"p2" } "a15" {"p4" }) ({"p37" } "a9" {"p56" }) ({"p116" "p209" "p72" "p50" "p93" "p186" "p87" } "a61" {"p23" "p77" "p69" "p165" "p116" "p203" "p93" }) ({"p90" "p92" "p91" "p180" "p50" "p84" "p151" "p76" "p86" "p97" "p124" "p88" "p77" } "a61" {"p90" "p92" "p91" "p180" "p84" "p76" "p86" "p97" "p23" "p88" "p77" "p144" "p126" }) ({"p111" "p126" "p180" "p93" "p51" "p65" "p87" } "a14" {"p0" "p69" "p126" "p81" "p180" "p107" "p97" }) ({"p68" "p204" "p116" "p81" "p50" "p93" "p164" } "a61" {"p23" "p116" "p159" "p208" "p93" "p65" "p86" }) ({"p33" } "a6" {"p35" }) ({"p90" "p92" "p91" "p181" "p50" "p197" "p84" "p151" "p76" "p86" "p88" "p77" "p100" "p111" "p127" } "a61" {"p90" "p92" "p91" "p180" "p152" "p84" "p76" "p86" "p97" "p23" "p88" "p77" "p198" "p105" "p126" }) ({"p134" "p209" "p72" "p50" "p93" "p186" "p130" "p87" } "a61" {"p157" "p23" "p77" "p69" "p165" "p121" "p203" "p93" }) ({"p91" "p164" "p140" "p76" "p135" "p134" "p156" "p112" "p133" "p111" "p79" "p154" "p137" "p136" "p83" "p153" "p87" "p86" "p20" "p150" "p89" "p88" "p144" "p106" "p149" "p203" "p104" } "a2" {"p91" "p186" "p140" "p76" "p135" "p134" "p156" "p112" "p133" "p111" "p79" "p154" "p137" "p136" "p83" "p153" "p87" "p86" "p150" "p89" "p88" "p144" "p106" "p149" "p48" "p104" "p208" }) ({"p11" } "a49" {"p10" }) ({"p41" } "a65" {"p42" }) ({"p90" "p92" "p182" "p91" "p50" "p93" "p153" "p84" "p76" "p86" "p88" "p77" "p119" } "a61" {"p90" "p92" "p182" "p91" "p93" "p84" "p76" "p86" "p23" "p88" "p77" "p128" }) ({"p134" "p69" "p111" "p165" "p116" "p93" "p51" } "a14" {"p0" "p69" "p165" "p121" "p158" "p107" "p97" }) ({"p153" "p164" "p140" "p150" "p20" "p135" "p156" "p134" "p112" "p77" "p133" "p111" "p144" "p154" "p68" "p106" "p149" "p203" "p104" "p137" "p136" } "a2" {"p72" "p153" "p186" "p140" "p150" "p86" "p135" "p156" "p134" "p112" "p133" "p111" "p144" "p154" "p106" "p149" "p48" "p104" "p137" "p136" "p208" }) ({"p69" "p111" "p165" "p121" "p93" "p51" } "a14" {"p0" "p69" "p165" "p121" "p107" "p97" }) ({"p102" "p113" "p69" "p18" "p114" "p109" "p186" "p130" } "a47" {"p102" "p113" "p69" "p13" "p114" "p109" "p186" "p130" }) ({"p44" } "a56" {"p21" }) ({"p102" "p113" "p203" "p18" "p158" "p114" "p109" "p119" "p180" "p65" } "a47" {"p102" "p113" "p13" "p116" "p114" "p109" "p197" "p186" "p65" }) ({"p102" "p113" "p133" "p128" "p18" "p114" "p182" "p109" "p208" "p74" "p86" } "a47" {"p102" "p113" "p199" "p13" "p68" "p114" "p109" "p83" "p164" "p153" "p120" }) ({"p102" "p113" "p133" "p128" "p18" "p114" "p182" "p109" "p208" "p65" } "a47" {"p102" "p113" "p199" "p13" "p114" "p109" "p164" "p153" "p120" "p65" }) ({"p102" "p67" "p112" "p199" "p111" "p110" "p115" "p28" "p114" "p83" "p118" "p163" } "a4" {"p2" "p182" "p85" "p74" "p102" "p112" "p111" "p132" "p110" "p115" "p114" "p119" "p207" }) ({"p102" "p113" "p204" "p18" "p158" "p114" "p109" "p118" "p163" "p65" } "a47" {"p102" "p113" "p13" "p132" "p116" "p159" "p114" "p109" "p207" "p65" }) ({"p90" "p92" "p91" "p9" "p142" "p141" "p140" "p75" "p135" "p113" "p78" "p211" "p156" "p112" "p210" "p155" "p79" "p216" "p139" "p215" "p138" "p214" "p115" "p213" "p136" "p114" "p217" "p193" "p82" "p63" "p131" "p196" "p195" "p150" "p194" "p201" "p89" "p88" "p189" "p143" "p205" "p149" "p148" "p104" "p202" "p147" "p103" "p108" } "a68" {"p90" "p92" "p91" "p12" "p113" "p156" "p112" "p155" "p115" "p114" "p193" "p60" "p196" "p195" "p150" "p194" "p189" "p143" "p149" "p148" "p104" "p147" "p103" "p108" "p142" "p141" "p140" "p75" "p135" "p78" "p211" "p210" "p79" "p216" "p139" "p215" "p138" "p214" "p213" "p136" "p217" "p82" "p131" "p201" "p89" "p88" "p205" "p202" }) ({"p111" "p144" "p119" "p180" "p93" "p51" "p65" "p87" } "a14" {"p0" "p124" "p69" "p81" "p180" "p107" "p97" }) ({"p112" "p77" "p111" "p198" "p68" "p106" "p104" "p129" "p152" "p183" "p20" } "a2" {"p200" "p112" "p111" "p154" "p106" "p127" "p48" "p104" "p181" "p72" "p86" }) ({"p102" "p113" "p68" "p18" "p114" "p109" "p129" "p183" } "a47" {"p102" "p113" "p13" "p68" "p114" "p109" "p129" "p183" }) ({"p111" "p165" "p121" "p93" "p51" "p65" "p87" } "a14" {"p0" "p69" "p165" "p121" "p81" "p107" "p97" }) ({"p111" "p128" "p180" "p93" "p73" "p51" "p151" } "a14" {"p0" "p126" "p180" "p107" "p153" "p73" "p97" }) ({"p102" "p113" "p77" "p203" "p18" "p158" "p114" "p109" "p119" "p180" "p73" } "a47" {"p102" "p113" "p13" "p116" "p114" "p80" "p109" "p72" "p197" "p186" }) ({"p112" "p111" "p128" "p106" "p104" "p182" "p80" "p197" "p74" "p151" "p20" } "a2" {"p112" "p199" "p111" "p106" "p48" "p104" "p126" "p83" "p180" "p153" "p73" }) ({"p21" } "a58" {"p24" }) ({"p61" } "a36" {"p8" }) ({"p110" "p18" "p129" "p74" "p95" "p183" "p86" } "a47" {"p13" "p68" "p109" "p83" "p129" "p96" "p183" }) ({"p0" } "a0" {"p33" }) ({"p90" "p92" "p91" "p50" "p153" "p84" "p95" "p76" "p183" "p86" "p88" "p77" "p199" "p129" "p107" } "a61" {"p90" "p92" "p182" "p91" "p93" "p84" "p76" "p86" "p23" "p200" "p88" "p77" "p154" "p128" "p109" }) ({"p90" "p92" "p91" "p181" "p50" "p197" "p84" "p95" "p151" "p76" "p86" "p88" "p77" "p127" "p107" } "a61" {"p90" "p92" "p91" "p180" "p93" "p152" "p84" "p76" "p86" "p23" "p88" "p77" "p198" "p126" "p109" }) ({"p54" } "a32" {"p38" }) ({"p60" } "a52" {"p34" }) ({"p90" "p92" "p91" "p50" "p175" "p96" "p84" "p76" "p86" "p88" "p77" "p132" "p125" "p207" "p107" } "a61" {"p90" "p92" "p91" "p192" "p93" "p84" "p163" "p76" "p86" "p146" "p23" "p88" "p77" "p110" "p118" }) ({"p5" } "a1" {"p54" }) ({"p102" "p113" "p18" "p114" "p109" "p72" "p186" "p130" } "a47" {"p102" "p113" "p13" "p114" "p109" "p72" "p186" "p130" }) ({"p44" } "a57" {"p47" }) ({"p92" "p141" "p75" "p212" "p135" "p157" "p211" "p134" "p156" "p112" "p77" "p210" "p133" "p155" "p111" "p132" "p110" "p216" "p138" "p137" "p115" "p136" "p114" "p217" "p192" "p191" "p85" "p87" "p86" "p201" "p89" "p146" "p102" "p88" "p145" "p189" "p143" "p203" "p202" "p28" "p209" "p208" "p207" } "a4" {"p2" "p92" "p141" "p75" "p212" "p135" "p157" "p211" "p134" "p156" "p112" "p77" "p210" "p133" "p155" "p111" "p132" "p110" "p216" "p138" "p137" "p115" "p136" "p114" "p217" "p192" "p191" "p85" "p87" "p86" "p201" "p89" "p146" "p102" "p88" "p145" "p189" "p143" "p203" "p202" "p209" "p208" "p207" }) ({"p69" "p111" "p126" "p180" "p93" "p51" } "a14" {"p0" "p69" "p126" "p180" "p107" "p97" }) ({"p102" "p113" "p66" "p117" "p38" "p138" "p90" "p213" "p114" "p160" "p109" } "a26" {"p102" "p113" "p167" "p122" "p205" "p114" "p70" "p109" "p82" "p131" "p40" }) ({"p29" } "a38" {"p1" }) ({"p113" "p167" "p189" "p122" "p143" "p70" "p94" "p40" "p75" } "a27" {"p123" "p138" "p90" "p213" "p108" "p71" "p98" "p172" "p53" }) ({"p6" } "a40" {"p3" }) ({"p68" "p204" "p158" "p81" "p50" "p93" "p164" "p120" } "a61" {"p23" "p133" "p116" "p159" "p208" "p93" "p65" "p86" }) ({"p111" "p126" "p180" "p93" "p73" "p51" } "a14" {"p0" "p126" "p180" "p107" "p73" "p97" }) ({"p88" "p77" "p165" "p121" "p90" "p92" "p91" "p50" "p84" "p76" "p97" "p86" } "a61" {"p90" "p92" "p91" "p84" "p76" "p97" "p86" "p23" "p88" "p77" "p165" "p121" }) ({"p102" "p113" "p18" "p158" "p114" "p182" "p109" "p208" "p119" "p74" "p86" } "a47" {"p102" "p113" "p199" "p13" "p68" "p116" "p114" "p109" "p83" "p164" }) ({"p15" } "a19" {}) ({"p102" "p67" "p113" "p204" "p18" "p158" "p114" "p81" "p109" "p118" "p163" } "a47" {"p102" "p113" "p13" "p132" "p116" "p159" "p114" "p109" "p207" "p85" "p65" }) ({"p158" "p209" "p72" "p50" "p93" "p120" "p186" "p87" } "a61" {"p23" "p77" "p133" "p69" "p165" "p116" "p203" "p93" }) ({"p36" } "a8" {"p37" }) ({"p83" "p175" "p102" "p67" "p200" "p112" "p111" "p154" "p110" "p115" "p125" "p28" "p114" } "a4" {"p2" "p192" "p85" "p74" "p183" "p102" "p146" "p112" "p111" "p110" "p115" "p114" "p129" }) ({"p48" } "a12" {"p51" }) ({"p121" "p209" "p72" "p50" "p186" "p87" "p97" } "a61" {"p23" "p77" "p69" "p165" "p121" "p203" "p97" }) ({"p102" "p113" "p69" "p165" "p121" "p18" "p114" "p109" } "a47" {"p102" "p113" "p69" "p165" "p13" "p121" "p114" "p109" }) ({"p23" } "a62" {"p25" }) ({"p102" "p113" "p18" "p114" "p109" "p129" "p65" "p183" } "a47" {"p102" "p113" "p13" "p114" "p109" "p129" "p65" "p183" }) ({"p111" "p128" "p180" "p93" "p51" "p65" "p151" "p87" } "a14" {"p0" "p69" "p126" "p81" "p180" "p107" "p153" "p97" }) ({"p102" "p113" "p69" "p127" "p18" "p114" "p109" "p181" } "a47" {"p102" "p113" "p69" "p13" "p127" "p114" "p109" "p181" }) ({"p134" "p209" "p72" "p50" "p186" "p130" "p87" "p97" } "a61" {"p157" "p23" "p77" "p69" "p165" "p121" "p203" "p97" }) ({"p127" "p181" "p72" "p50" "p107" "p197" "p96" "p151" "p87" } "a61" {"p23" "p77" "p69" "p198" "p110" "p126" "p180" "p93" "p152" }) ({"p43" } "a10" {"p45" }) ({"p182" "p91" "p140" "p76" "p135" "p134" "p156" "p112" "p133" "p111" "p79" "p154" "p137" "p136" "p83" "p197" "p153" "p87" "p86" "p20" "p150" "p89" "p88" "p144" "p106" "p149" "p104" } "a2" {"p91" "p180" "p140" "p76" "p135" "p134" "p156" "p112" "p199" "p133" "p111" "p79" "p154" "p137" "p136" "p83" "p153" "p87" "p86" "p150" "p89" "p88" "p144" "p106" "p149" "p48" "p104" }) ({"p49" } "a29" {"p46" }) ({"p17" } "a21" {"p43" }) ({"p102" "p113" "p69" "p165" "p116" "p18" "p114" "p109" } "a47" {"p102" "p113" "p69" "p165" "p13" "p116" "p114" "p109" }) ({"p146" "p123" "p57" "p109" "p192" "p71" "p85" "p98" "p172" "p64" } "a66" {"p67" "p113" "p189" "p58" "p143" "p29" "p125" "p175" "p95" "p75" }) ({"p111" "p93" "p186" "p51" "p130" "p65" "p87" } "a14" {"p0" "p69" "p81" "p107" "p186" "p130" "p97" }) ({"p90" "p92" "p91" "p50" "p186" "p84" "p76" "p86" "p97" "p88" "p77" "p121" "p209" } "a61" {"p90" "p92" "p91" "p84" "p76" "p86" "p97" "p23" "p88" "p77" "p121" "p165" "p203" }) ({"p102" "p113" "p18" "p114" "p109" "p186" "p130" "p65" } "a47" {"p102" "p113" "p13" "p114" "p109" "p186" "p130" "p65" }) ({"p134" "p111" "p116" "p93" "p186" "p51" "p65" "p87" } "a14" {"p0" "p69" "p121" "p158" "p81" "p107" "p186" "p97" }) ({"p92" "p85" "p175" "p96" "p87" "p86" "p75" "p89" "p200" "p88" "p77" "p154" "p106" "p125" "p28" } "a4" {"p2" "p92" "p192" "p85" "p87" "p183" "p86" "p75" "p89" "p146" "p88" "p101" "p77" "p110" "p129" }) ({"p102" "p127" "p181" "p73" "p95" "p51" } "a14" {"p0" "p99" "p127" "p109" "p181" "p73" }) ({"p13" } "a48" {"p11" }) ({"p157" "p111" "p72" "p93" "p120" "p186" "p51" } "a14" {"p0" "p133" "p72" "p107" "p186" "p130" "p97" }) ({"p12" } "a18" {"p16" }) ({"p102" "p113" "p69" "p121" "p18" "p114" "p109" "p186" } "a47" {"p102" "p113" "p69" "p13" "p121" "p114" "p109" "p186" }) ({"p35" } "a7" {"p36" }) ({"p126" "p180" "p51" "p65" "p87" "p97" } "a14" {"p0" "p69" "p126" "p81" "p180" "p97" }) ({"p182" "p80" "p197" "p153" "p74" "p140" "p150" "p20" "p135" "p156" "p134" "p112" "p133" "p111" "p144" "p154" "p106" "p149" "p104" "p137" "p136" } "a2" {"p83" "p180" "p153" "p73" "p140" "p150" "p135" "p156" "p134" "p112" "p199" "p133" "p111" "p144" "p154" "p106" "p149" "p48" "p104" "p137" "p136" }) ({"p102" "p113" "p133" "p128" "p203" "p18" "p114" "p109" "p180" "p65" } "a47" {"p102" "p113" "p13" "p114" "p109" "p197" "p153" "p120" "p186" "p65" }) ({"p90" "p92" "p91" "p50" "p186" "p84" "p130" "p76" "p86" "p97" "p88" "p134" "p77" "p209" } "a61" {"p90" "p92" "p91" "p84" "p76" "p86" "p97" "p157" "p23" "p88" "p77" "p121" "p165" "p203" }) ({"p34" } "a53" {"p42" }) ({"p8" } "a17" {"p9" }) ({"p30" } "a23" {"p22" }) ({"p134" "p111" "p165" "p116" "p93" "p51" "p65" "p87" } "a14" {"p0" "p69" "p165" "p121" "p158" "p81" "p107" "p97" }) ({"p102" "p113" "p127" "p18" "p114" "p109" "p181" "p72" } "a47" {"p102" "p113" "p13" "p127" "p114" "p109" "p181" "p72" }) ({"p102" "p157" "p113" "p203" "p18" "p126" "p114" "p109" "p180" "p65" } "a47" {"p102" "p113" "p13" "p114" "p109" "p197" "p186" "p130" "p65" "p151" }) ({"p100" "p127" "p181" "p51" "p65" "p87" } "a14" {"p0" "p69" "p100" "p127" "p81" "p181" }) ({"p24" } "a60" {}) ({"p90" "p92" "p91" "p50" "p93" "p120" "p186" "p84" "p76" "p86" "p88" "p77" "p158" "p209" } "a61" {"p90" "p92" "p91" "p93" "p84" "p76" "p86" "p23" "p88" "p77" "p133" "p165" "p116" "p203" }) ({"p91" "p83" "p152" "p87" "p76" "p183" "p86" "p20" "p89" "p88" "p101" "p79" "p198" "p105" "p129" } "a2" {"p91" "p181" "p83" "p87" "p76" "p86" "p89" "p200" "p88" "p100" "p79" "p154" "p106" "p127" "p48" }) ({"p45" } "a11" {"p32" }) ({"p102" "p113" "p68" "p116" "p18" "p114" "p109" "p164" } "a47" {"p102" "p113" "p13" "p68" "p116" "p114" "p109" "p164" }) ({"p58" } "a34" {"p61" }) ({"p90" "p92" "p91" "p50" "p175" "p84" "p95" "p76" "p86" "p88" "p77" "p132" "p125" "p207" "p107" } "a61" {"p90" "p92" "p91" "p192" "p93" "p84" "p163" "p76" "p86" "p146" "p23" "p88" "p77" "p109" "p118" }) ({"p102" "p113" "p121" "p18" "p114" "p109" "p72" "p186" } "a47" {"p102" "p113" "p13" "p121" "p114" "p109" "p72" "p186" }) ({"p134" "p111" "p116" "p159" "p209" "p93" "p51" "p65" "p87" } "a14" {"p0" "p69" "p165" "p121" "p204" "p158" "p81" "p107" "p97" }) ({"p112" "p111" "p198" "p106" "p104" "p80" "p129" "p74" "p152" "p183" "p20" } "a2" {"p200" "p112" "p111" "p154" "p106" "p127" "p48" "p104" "p181" "p83" "p73" }) ({"p46" } "a28" {"p62" }) ({"p4" } "a16" {"p20" }) ({"p102" "p113" "p116" "p18" "p114" "p109" "p72" "p186" } "a47" {"p102" "p113" "p13" "p116" "p114" "p109" "p72" "p186" }) ({"p102" "p113" "p68" "p18" "p114" "p109" "p164" "p120" } "a47" {"p102" "p113" "p13" "p68" "p114" "p109" "p164" "p120" }) ({"p31" } "a25" {"p17" }) ({"p19" } "a45" {"p18" }) ({"p165" "p121" "p51" "p65" "p87" "p97" } "a14" {"p0" "p69" "p165" "p121" "p81" "p97" }) ({"p88" "p77" "p90" "p126" "p92" "p91" "p180" "p50" "p84" "p76" "p97" "p86" } "a61" {"p90" "p92" "p91" "p180" "p84" "p76" "p97" "p86" "p23" "p88" "p77" "p126" }) ({"p88" "p77" "p128" "p90" "p92" "p182" "p91" "p50" "p93" "p84" "p76" "p86" } "a61" {"p90" "p92" "p182" "p91" "p93" "p84" "p76" "p86" "p23" "p88" "p77" "p128" }) ({"p102" "p157" "p113" "p77" "p203" "p18" "p126" "p114" "p109" "p180" "p73" } "a47" {"p102" "p113" "p13" "p114" "p80" "p109" "p72" "p197" "p186" "p130" "p151" }) ({"p55" } "a46" {}) ({"p99" "p77" "p127" "p105" "p18" "p181" "p73" } "a47" {"p102" "p100" "p13" "p127" "p80" "p181" "p72" }) ({"p102" "p113" "p18" "p114" "p109" "p72" "p120" "p186" } "a47" {"p102" "p113" "p13" "p114" "p109" "p72" "p120" "p186" }) ({"p102" "p124" "p113" "p134" "p77" "p203" "p18" "p114" "p109" "p180" "p73" } "a47" {"p102" "p113" "p144" "p13" "p121" "p114" "p80" "p109" "p72" "p197" "p186" }) ({"p88" "p77" "p90" "p92" "p91" "p50" "p118" "p93" "p84" "p163" "p76" "p86" } "a61" {"p90" "p92" "p91" "p93" "p84" "p163" "p76" "p86" "p23" "p88" "p77" "p118" }) ({"p88" "p77" "p165" "p116" "p90" "p92" "p91" "p50" "p93" "p84" "p76" "p86" } "a61" {"p90" "p92" "p91" "p93" "p84" "p76" "p86" "p23" "p88" "p77" "p165" "p116" }) ({"p53" } "a31" {"p52" }) ({"p92" "p91" "p141" "p51" "p140" "p76" "p157" "p78" "p211" "p134" "p112" "p77" "p155" "p111" "p198" "p216" "p215" "p136" "p114" "p193" "p80" "p191" "p190" "p197" "p152" "p87" "p151" "p194" "p201" "p89" "p102" "p145" "p144" "p105" "p203" "p148" "p147" "p103" "p209" } "a13" {"p92" "p91" "p30" "p141" "p140" "p76" "p157" "p78" "p211" "p134" "p112" "p77" "p155" "p111" "p198" "p216" "p215" "p136" "p114" "p193" "p80" "p191" "p190" "p197" "p152" "p87" "p151" "p194" "p201" "p89" "p102" "p145" "p144" "p105" "p203" "p148" "p147" "p103" "p209" }) ({"p102" "p113" "p165" "p121" "p18" "p114" "p109" "p65" } "a47" {"p102" "p113" "p165" "p13" "p121" "p114" "p109" "p65" }) ({"p102" "p113" "p127" "p18" "p114" "p109" "p181" "p65" } "a47" {"p102" "p113" "p13" "p127" "p114" "p109" "p181" "p65" }) ({"p27" } "a22" {"p5" }) ({"p102" "p157" "p113" "p69" "p203" "p18" "p126" "p114" "p109" "p180" } "a47" {"p102" "p113" "p69" "p13" "p114" "p109" "p197" "p186" "p130" "p151" }) ({"p25" } "a63" {"p39" }) ({"p90" "p92" "p91" "p50" "p93" "p120" "p164" "p84" "p76" "p86" "p88" "p77" "p204" "p158" } "a61" {"p90" "p92" "p91" "p93" "p84" "p76" "p86" "p23" "p88" "p77" "p133" "p116" "p159" "p208" }) ({"p88" "p77" "p128" "p90" "p92" "p91" "p180" "p50" "p93" "p84" "p76" "p86" } "a61" {"p90" "p92" "p91" "p180" "p93" "p84" "p76" "p86" "p23" "p88" "p77" "p128" }) ({"p88" "p77" "p165" "p121" "p90" "p92" "p91" "p50" "p93" "p84" "p76" "p86" } "a61" {"p90" "p92" "p91" "p93" "p84" "p76" "p86" "p23" "p88" "p77" "p165" "p121" }) ({"p92" "p85" "p163" "p87" "p86" "p75" "p89" "p102" "p88" "p112" "p77" "p199" "p111" "p110" "p115" "p28" "p114" "p118" } "a4" {"p2" "p92" "p182" "p85" "p87" "p86" "p75" "p89" "p102" "p88" "p112" "p77" "p111" "p132" "p110" "p115" "p114" "p119" "p207" }) ({"p127" "p105" "p181" "p72" "p96" "p51" } "a14" {"p0" "p100" "p110" "p127" "p181" "p72" }) ({"p182" "p91" "p83" "p197" "p151" "p87" "p76" "p86" "p20" "p89" "p88" "p112" "p111" "p79" "p128" "p106" "p104" } "a2" {"p91" "p83" "p180" "p153" "p87" "p76" "p86" "p89" "p88" "p112" "p199" "p111" "p79" "p106" "p48" "p126" "p104" }) ({"p102" "p113" "p165" "p116" "p18" "p114" "p109" "p65" } "a47" {"p102" "p113" "p165" "p13" "p116" "p114" "p109" "p65" }) ({"p100" "p111" "p127" "p181" "p72" "p50" "p197" "p151" "p87" } "a61" {"p23" "p77" "p69" "p198" "p105" "p126" "p180" "p152" "p97" }) ({"p7" } "a51" {"p6" }) ({"p102" "p113" "p77" "p133" "p128" "p203" "p18" "p114" "p109" "p180" "p73" } "a47" {"p102" "p113" "p13" "p114" "p80" "p109" "p72" "p197" "p153" "p120" "p186" }) ({"p91" "p83" "p120" "p164" "p87" "p76" "p86" "p20" "p157" "p89" "p88" "p112" "p111" "p79" "p106" "p203" "p104" } "a2" {"p91" "p83" "p186" "p130" "p87" "p76" "p86" "p89" "p88" "p112" "p133" "p111" "p79" "p106" "p48" "p104" "p208" }) ({"p59" } "a35" {"p15" }) ({"p199" "p68" "p81" "p50" "p129" "p107" "p96" "p153" "p183" } "a61" {"p23" "p200" "p154" "p110" "p128" "p182" "p93" "p65" "p86" }) ({"p157" "p112" "p77" "p111" "p68" "p106" "p104" "p203" "p164" "p120" "p20" } "a2" {"p112" "p133" "p111" "p106" "p48" "p104" "p208" "p72" "p186" "p130" "p86" }) ({"p90" "p92" "p91" "p50" "p153" "p84" "p76" "p183" "p86" "p88" "p101" "p77" "p199" "p129" "p107" } "a61" {"p90" "p92" "p182" "p91" "p93" "p84" "p76" "p86" "p23" "p200" "p88" "p77" "p154" "p128" "p106" }) ({"p16" } "a20" {"p26" }) ({"p102" "p113" "p18" "p158" "p114" "p182" "p109" "p208" "p119" "p65" } "a47" {"p102" "p113" "p199" "p13" "p116" "p114" "p109" "p164" "p65" }) ({"p123" "p71" "p62" "p98" "p172" } "a37" {"p123" "p71" "p98" "p172" "p31" }) ({"p42" } "a54" {"p44" }) ({"p90" "p92" "p91" "p50" "p93" "p186" "p84" "p130" "p76" "p86" "p88" "p134" "p77" "p209" } "a61" {"p90" "p92" "p91" "p93" "p84" "p76" "p86" "p157" "p23" "p88" "p77" "p121" "p165" "p203" }) ({"p102" "p113" "p116" "p18" "p114" "p109" "p186" "p65" } "a47" {"p102" "p113" "p13" "p116" "p114" "p109" "p186" "p65" }) ({"p102" "p113" "p116" "p18" "p114" "p109" "p164" "p65" } "a47" {"p102" "p113" "p13" "p116" "p114" "p109" "p164" "p65" }) ({"p56" } "a33" {"p59" }) ({"p69" "p111" "p93" "p186" "p51" "p130" } "a14" {"p0" "p69" "p107" "p186" "p130" "p97" }) ({"p1" } "a39" {"p6" }) ({"p88" "p77" "p90" "p126" "p92" "p91" "p180" "p50" "p93" "p84" "p76" "p86" } "a61" {"p90" "p92" "p91" "p180" "p93" "p84" "p76" "p86" "p23" "p88" "p77" "p126" }) ({"p90" "p92" "p91" "p9" "p142" "p141" "p140" "p75" "p135" "p113" "p78" "p211" "p156" "p112" "p210" "p155" "p79" "p216" "p139" "p215" "p138" "p214" "p115" "p213" "p136" "p114" "p217" "p193" "p82" "p131" "p196" "p195" "p150" "p194" "p201" "p89" "p88" "p189" "p143" "p205" "p149" "p148" "p104" "p202" "p147" "p103" "p108" } "a69" {"p90" "p92" "p91" "p142" "p141" "p140" "p75" "p135" "p113" "p78" "p211" "p156" "p112" "p210" "p155" "p79" "p216" "p139" "p215" "p138" "p214" "p115" "p213" "p136" "p114" "p217" "p193" "p82" "p131" "p196" "p195" "p150" "p194" "p201" "p89" "p88" "p189" "p143" "p205" "p149" "p148" "p104" "p202" "p147" "p103" "p108" }) ({"p90" "p92" "p91" "p181" "p50" "p197" "p84" "p151" "p76" "p86" "p99" "p88" "p77" "p111" "p127" } "a61" {"p90" "p92" "p91" "p180" "p152" "p84" "p76" "p86" "p97" "p102" "p23" "p88" "p77" "p198" "p126" }) ({"p102" "p113" "p116" "p18" "p159" "p114" "p109" "p65" } "a47" {"p102" "p113" "p13" "p116" "p159" "p114" "p109" "p65" }) ({"p102" "p124" "p113" "p134" "p69" "p203" "p18" "p114" "p109" "p180" } "a47" {"p102" "p113" "p69" "p144" "p13" "p121" "p114" "p109" "p197" "p186" }) ({"p39" } "a64" {"p41" }) ({"p111" "p144" "p119" "p180" "p93" "p73" "p51" } "a14" {"p0" "p124" "p180" "p107" "p73" "p97" }) ({"p102" "p113" "p18" "p114" "p109" "p120" "p186" "p65" } "a47" {"p102" "p113" "p13" "p114" "p109" "p120" "p186" "p65" }) ({"p102" "p113" "p18" "p114" "p109" "p164" "p120" "p65" } "a47" {"p102" "p113" "p13" "p114" "p109" "p164" "p120" "p65" }) ({"p26" } "a3" {"p28" }) ({"p47" } "a59" {"p50" }) ({"p88" "p77" "p116" "p159" "p90" "p92" "p91" "p50" "p93" "p84" "p76" "p86" } "a61" {"p90" "p92" "p91" "p93" "p84" "p76" "p86" "p23" "p88" "p77" "p116" "p159" }) ({"p3" } "a42" {"p14" }) ({"p134" "p111" "p116" "p72" "p93" "p186" "p51" } "a14" {"p0" "p121" "p158" "p72" "p107" "p186" "p97" }) ({"p90" "p92" "p91" "p50" "p93" "p186" "p84" "p76" "p86" "p88" "p77" "p116" "p209" } "a61" {"p90" "p92" "p91" "p93" "p84" "p76" "p86" "p23" "p88" "p77" "p165" "p116" "p203" }) ({"p186" "p51" "p130" "p65" "p87" "p97" } "a14" {"p0" "p69" "p81" "p186" "p130" "p97" }) ({"p67" "p110" "p18" "p125" "p81" "p175" "p95" } "a47" {"p13" "p125" "p109" "p96" "p85" "p175" "p65" }) ({"p77" "p110" "p127" "p18" "p181" "p73" "p95" } "a47" {"p13" "p127" "p80" "p109" "p181" "p72" "p96" }) ({"p90" "p92" "p91" "p180" "p50" "p93" "p153" "p84" "p76" "p86" "p88" "p77" "p119" } "a61" {"p90" "p92" "p91" "p180" "p93" "p84" "p76" "p86" "p23" "p88" "p77" "p128" }) ({"p111" "p72" "p93" "p186" "p51" "p130" } "a14" {"p0" "p72" "p107" "p186" "p130" "p97" }) ({"p91" "p140" "p76" "p212" "p135" "p211" "p134" "p156" "p112" "p199" "p210" "p133" "p111" "p79" "p154" "p215" "p137" "p136" "p83" "p190" "p153" "p196" "p87" "p195" "p86" "p20" "p150" "p89" "p200" "p88" "p144" "p106" "p149" "p104" "p202" "p209" "p208" } "a2" {"p91" "p140" "p76" "p212" "p135" "p211" "p134" "p156" "p112" "p199" "p210" "p133" "p111" "p79" "p154" "p215" "p137" "p136" "p83" "p190" "p153" "p196" "p87" "p195" "p86" "p150" "p89" "p200" "p88" "p144" "p106" "p149" "p48" "p104" "p202" "p209" "p208" }) ({"p14" } "a44" {"p55" }) ({"p102" "p113" "p18" "p125" "p114" "p109" "p175" "p65" } "a47" {"p102" "p113" "p13" "p125" "p114" "p109" "p175" "p65" }) ({"p10" } "a50" {"p7" }) ({"p52" } "a30" {"p49" }) ({"p90" "p92" "p91" "p50" "p93" "p164" "p84" "p76" "p86" "p88" "p77" "p204" "p116" } "a61" {"p90" "p92" "p91" "p93" "p84" "p76" "p86" "p23" "p88" "p77" "p116" "p159" "p208" }) ({"p157" "p111" "p93" "p120" "p186" "p51" "p65" "p87" } "a14" {"p0" "p133" "p69" "p81" "p107" "p186" "p130" "p97" }) ({"p32" } "a5" {"p57" }) ({"p3" } "a43" {"p19" }) }, initialMarking = {"p90" "p160" "p92" "p91" "p94" "p157" "p113" "p156" "p112" "p155" "p199" "p111" "p154" "p198" "p110" "p117" "p115" "p158" "p114" "p193" "p192" "p191" "p190" "p153" "p197" "p63" "p152" "p196" "p151" "p195" "p150" "p194" "p64" "p146" "p102" "p145" "p189" "p66" "p144" "p143" "p27" "p106" "p149" "p105" "p148" "p104" "p147" "p103" "p109" "p107" "p142" "p141" "p76" "p140" "p75" "p78" "p212" "p135" "p77" "p211" "p134" "p210" "p133" "p79" "p132" "p216" "p139" "p215" "p138" "p214" "p137" "p213" "p136" "p217" "p81" "p80" "p83" "p85" "p84" "p87" "p86" "p89" "p201" "p88" "p200" "p204" "p203" "p202" "p209" "p208" "p207" }, acceptingPlaces = {"p22" } ); // Testfile dumped by Ultimate at 2018/11/06 15:19:19 // // FiniteAutomaton nwa = ( 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 }, states = {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 s19 s20 }, initialStates = {s13 }, finalStates = {s12 }, transitions = { (s0 a46 s0) (s0 a47 s13) (s0 a48 s0) (s0 a49 s0) (s0 a50 s0) (s0 a51 s0) (s0 a0 s0) (s0 a1 s0) (s0 a52 s0) (s0 a53 s0) (s0 a54 s0) (s0 a55 s12) (s0 a2 s0) (s0 a56 s0) (s0 a57 s0) (s0 a58 s0) (s0 a3 s0) (s0 a59 s0) (s0 a60 s0) (s0 a4 s0) (s0 a61 s4) (s0 a62 s0) (s0 a63 s0) (s0 a64 s0) (s0 a65 s0) (s0 a5 s0) (s0 a6 s0) (s0 a7 s0) (s0 a8 s0) (s0 a9 s0) (s0 a10 s0) (s0 a66 s14) (s0 a67 s12) (s0 a11 s0) (s0 a68 s14) (s0 a69 s12) (s0 a12 s0) (s0 a13 s0) (s0 a14 s2) (s0 a15 s0) (s0 a16 s0) (s0 a17 s0) (s0 a18 s0) (s0 a19 s0) (s0 a20 s0) (s0 a21 s0) (s0 a22 s0) (s0 a23 s0) (s0 a24 s12) (s0 a25 s0) (s0 a26 s0) (s0 a27 s0) (s0 a28 s0) (s0 a29 s0) (s0 a30 s0) (s0 a31 s0) (s0 a32 s0) (s0 a33 s0) (s0 a34 s0) (s0 a35 s0) (s0 a36 s0) (s0 a37 s0) (s0 a38 s0) (s0 a39 s0) (s0 a40 s0) (s0 a41 s12) (s0 a42 s0) (s0 a43 s0) (s0 a44 s0) (s0 a45 s0) (s1 a46 s1) (s1 a47 s1) (s1 a48 s1) (s1 a49 s1) (s1 a50 s1) (s1 a51 s1) (s1 a0 s1) (s1 a1 s1) (s1 a52 s1) (s1 a53 s1) (s1 a54 s1) (s1 a55 s12) (s1 a2 s1) (s1 a56 s1) (s1 a57 s1) (s1 a58 s1) (s1 a3 s1) (s1 a59 s1) (s1 a60 s1) (s1 a4 s1) (s1 a61 s18) (s1 a62 s1) (s1 a63 s1) (s1 a64 s1) (s1 a65 s1) (s1 a5 s1) (s1 a6 s1) (s1 a7 s1) (s1 a8 s1) (s1 a9 s1) (s1 a10 s1) (s1 a66 s1) (s1 a67 s1) (s1 a11 s1) (s1 a68 s1) (s1 a69 s1) (s1 a12 s1) (s1 a13 s12) (s1 a14 s1) (s1 a15 s1) (s1 a16 s1) (s1 a17 s1) (s1 a18 s1) (s1 a19 s1) (s1 a20 s1) (s1 a21 s1) (s1 a22 s1) (s1 a23 s1) (s1 a24 s12) (s1 a25 s1) (s1 a26 s11) (s1 a27 s18) (s1 a28 s1) (s1 a29 s1) (s1 a30 s1) (s1 a31 s1) (s1 a32 s1) (s1 a33 s1) (s1 a34 s1) (s1 a35 s1) (s1 a36 s1) (s1 a37 s16) (s1 a38 s1) (s1 a39 s1) (s1 a40 s1) (s1 a41 s12) (s1 a42 s1) (s1 a43 s1) (s1 a44 s1) (s1 a45 s1) (s2 a46 s2) (s2 a47 s19) (s2 a48 s2) (s2 a49 s2) (s2 a50 s2) (s2 a51 s2) (s2 a0 s2) (s2 a1 s2) (s2 a52 s2) (s2 a53 s2) (s2 a54 s2) (s2 a55 s12) (s2 a2 s0) (s2 a56 s2) (s2 a57 s2) (s2 a58 s2) (s2 a3 s2) (s2 a59 s2) (s2 a60 s2) (s2 a4 s2) (s2 a61 s7) (s2 a62 s2) (s2 a63 s2) (s2 a64 s2) (s2 a65 s2) (s2 a5 s2) (s2 a6 s2) (s2 a7 s2) (s2 a8 s2) (s2 a9 s2) (s2 a10 s2) (s2 a66 s5) (s2 a67 s12) (s2 a11 s2) (s2 a68 s5) (s2 a69 s12) (s2 a12 s2) (s2 a13 s12) (s2 a14 s2) (s2 a15 s2) (s2 a16 s2) (s2 a17 s2) (s2 a18 s2) (s2 a19 s2) (s2 a20 s2) (s2 a21 s2) (s2 a22 s2) (s2 a23 s2) (s2 a24 s12) (s2 a25 s2) (s2 a26 s2) (s2 a27 s2) (s2 a28 s2) (s2 a29 s2) (s2 a30 s2) (s2 a31 s2) (s2 a32 s2) (s2 a33 s2) (s2 a34 s2) (s2 a35 s2) (s2 a36 s2) (s2 a37 s0) (s2 a38 s2) (s2 a39 s2) (s2 a40 s2) (s2 a41 s12) (s2 a42 s2) (s2 a43 s2) (s2 a44 s2) (s2 a45 s2) (s3 a46 s3) (s3 a47 s3) (s3 a48 s3) (s3 a49 s3) (s3 a50 s3) (s3 a51 s3) (s3 a0 s3) (s3 a1 s3) (s3 a52 s3) (s3 a53 s3) (s3 a54 s3) (s3 a55 s12) (s3 a2 s1) (s3 a56 s3) (s3 a57 s3) (s3 a58 s3) (s3 a3 s3) (s3 a59 s3) (s3 a60 s3) (s3 a4 s3) (s3 a61 s10) (s3 a62 s3) (s3 a63 s3) (s3 a64 s3) (s3 a65 s3) (s3 a5 s3) (s3 a6 s3) (s3 a7 s3) (s3 a8 s3) (s3 a9 s3) (s3 a10 s3) (s3 a66 s3) (s3 a67 s3) (s3 a11 s3) (s3 a68 s3) (s3 a69 s3) (s3 a12 s3) (s3 a13 s3) (s3 a14 s1) (s3 a15 s3) (s3 a16 s3) (s3 a17 s3) (s3 a18 s3) (s3 a19 s3) (s3 a20 s3) (s3 a21 s3) (s3 a22 s3) (s3 a23 s3) (s3 a24 s12) (s3 a25 s3) (s3 a26 s15) (s3 a27 s10) (s3 a28 s3) (s3 a29 s3) (s3 a30 s3) (s3 a31 s3) (s3 a32 s3) (s3 a33 s3) (s3 a34 s3) (s3 a35 s3) (s3 a36 s3) (s3 a37 s16) (s3 a38 s3) (s3 a39 s3) (s3 a40 s3) (s3 a41 s12) (s3 a42 s3) (s3 a43 s3) (s3 a44 s3) (s3 a45 s3) (s4 a46 s4) (s4 a47 s8) (s4 a48 s4) (s4 a49 s4) (s4 a50 s4) (s4 a51 s4) (s4 a0 s4) (s4 a1 s4) (s4 a52 s4) (s4 a53 s4) (s4 a54 s4) (s4 a55 s12) (s4 a2 s4) (s4 a56 s4) (s4 a57 s4) (s4 a58 s4) (s4 a3 s4) (s4 a59 s4) (s4 a60 s4) (s4 a4 s9) (s4 a61 s4) (s4 a62 s4) (s4 a63 s4) (s4 a64 s4) (s4 a65 s4) (s4 a5 s4) (s4 a6 s4) (s4 a7 s4) (s4 a8 s4) (s4 a9 s4) (s4 a10 s4) (s4 a66 s6) (s4 a67 s12) (s4 a11 s4) (s4 a68 s6) (s4 a69 s12) (s4 a12 s4) (s4 a13 s4) (s4 a14 s7) (s4 a15 s4) (s4 a16 s4) (s4 a17 s4) (s4 a18 s4) (s4 a19 s4) (s4 a20 s4) (s4 a21 s4) (s4 a22 s4) (s4 a23 s4) (s4 a24 s12) (s4 a25 s4) (s4 a26 s4) (s4 a27 s0) (s4 a28 s4) (s4 a29 s4) (s4 a30 s4) (s4 a31 s4) (s4 a32 s4) (s4 a33 s4) (s4 a34 s4) (s4 a35 s4) (s4 a36 s4) (s4 a37 s4) (s4 a38 s4) (s4 a39 s4) (s4 a40 s4) (s4 a41 s12) (s4 a42 s4) (s4 a43 s4) (s4 a44 s4) (s4 a45 s4) (s5 a46 s5) (s5 a47 s18) (s5 a48 s5) (s5 a49 s5) (s5 a50 s5) (s5 a51 s5) (s5 a0 s5) (s5 a1 s5) (s5 a52 s5) (s5 a53 s5) (s5 a54 s5) (s5 a55 s12) (s5 a2 s14) (s5 a56 s5) (s5 a57 s5) (s5 a58 s5) (s5 a3 s5) (s5 a59 s5) (s5 a60 s5) (s5 a4 s5) (s5 a61 s11) (s5 a62 s5) (s5 a63 s5) (s5 a64 s5) (s5 a65 s5) (s5 a5 s5) (s5 a6 s5) (s5 a7 s5) (s5 a8 s5) (s5 a9 s5) (s5 a10 s5) (s5 a66 s5) (s5 a67 s5) (s5 a11 s5) (s5 a68 s5) (s5 a69 s5) (s5 a12 s5) (s5 a13 s12) (s5 a14 s5) (s5 a15 s5) (s5 a16 s5) (s5 a17 s5) (s5 a18 s5) (s5 a19 s5) (s5 a20 s5) (s5 a21 s5) (s5 a22 s5) (s5 a23 s5) (s5 a24 s12) (s5 a25 s5) (s5 a26 s5) (s5 a27 s5) (s5 a28 s5) (s5 a29 s5) (s5 a30 s5) (s5 a31 s5) (s5 a32 s5) (s5 a33 s5) (s5 a34 s5) (s5 a35 s5) (s5 a36 s5) (s5 a37 s14) (s5 a38 s5) (s5 a39 s5) (s5 a40 s5) (s5 a41 s12) (s5 a42 s5) (s5 a43 s5) (s5 a44 s5) (s5 a45 s5) (s6 a46 s6) (s6 a47 s16) (s6 a48 s6) (s6 a49 s6) (s6 a50 s6) (s6 a51 s6) (s6 a0 s6) (s6 a1 s6) (s6 a52 s6) (s6 a53 s6) (s6 a54 s6) (s6 a55 s12) (s6 a2 s6) (s6 a56 s6) (s6 a57 s6) (s6 a58 s6) (s6 a3 s6) (s6 a59 s6) (s6 a60 s6) (s6 a4 s15) (s6 a61 s6) (s6 a62 s6) (s6 a63 s6) (s6 a64 s6) (s6 a65 s6) (s6 a5 s6) (s6 a6 s6) (s6 a7 s6) (s6 a8 s6) (s6 a9 s6) (s6 a10 s6) (s6 a66 s6) (s6 a67 s6) (s6 a11 s6) (s6 a68 s6) (s6 a69 s6) (s6 a12 s6) (s6 a13 s6) (s6 a14 s11) (s6 a15 s6) (s6 a16 s6) (s6 a17 s6) (s6 a18 s6) (s6 a19 s6) (s6 a20 s6) (s6 a21 s6) (s6 a22 s6) (s6 a23 s6) (s6 a24 s12) (s6 a25 s6) (s6 a26 s6) (s6 a27 s14) (s6 a28 s6) (s6 a29 s6) (s6 a30 s6) (s6 a31 s6) (s6 a32 s6) (s6 a33 s6) (s6 a34 s6) (s6 a35 s6) (s6 a36 s6) (s6 a37 s6) (s6 a38 s6) (s6 a39 s6) (s6 a40 s6) (s6 a41 s12) (s6 a42 s6) (s6 a43 s6) (s6 a44 s6) (s6 a45 s6) (s7 a46 s7) (s7 a47 s17) (s7 a48 s7) (s7 a49 s7) (s7 a50 s7) (s7 a51 s7) (s7 a0 s7) (s7 a1 s7) (s7 a52 s7) (s7 a53 s7) (s7 a54 s7) (s7 a55 s12) (s7 a2 s7) (s7 a56 s7) (s7 a57 s7) (s7 a58 s7) (s7 a3 s7) (s7 a59 s7) (s7 a60 s7) (s7 a4 s7) (s7 a61 s7) (s7 a62 s7) (s7 a63 s7) (s7 a64 s7) (s7 a65 s7) (s7 a5 s7) (s7 a6 s7) (s7 a7 s7) (s7 a8 s7) (s7 a9 s7) (s7 a10 s7) (s7 a66 s11) (s7 a67 s12) (s7 a11 s7) (s7 a68 s11) (s7 a69 s12) (s7 a12 s7) (s7 a13 s12) (s7 a14 s7) (s7 a15 s7) (s7 a16 s7) (s7 a17 s7) (s7 a18 s7) (s7 a19 s7) (s7 a20 s7) (s7 a21 s7) (s7 a22 s7) (s7 a23 s7) (s7 a24 s12) (s7 a25 s7) (s7 a26 s7) (s7 a27 s2) (s7 a28 s7) (s7 a29 s7) (s7 a30 s7) (s7 a31 s7) (s7 a32 s7) (s7 a33 s7) (s7 a34 s7) (s7 a35 s7) (s7 a36 s7) (s7 a37 s4) (s7 a38 s7) (s7 a39 s7) (s7 a40 s7) (s7 a41 s12) (s7 a42 s7) (s7 a43 s7) (s7 a44 s7) (s7 a45 s7) (s8 a46 s8) (s8 a47 s8) (s8 a48 s8) (s8 a49 s8) (s8 a50 s8) (s8 a51 s8) (s8 a0 s8) (s8 a1 s8) (s8 a52 s8) (s8 a53 s8) (s8 a54 s8) (s8 a55 s12) (s8 a2 s8) (s8 a56 s8) (s8 a57 s8) (s8 a58 s8) (s8 a3 s8) (s8 a59 s8) (s8 a60 s8) (s8 a4 s20) (s8 a61 s13) (s8 a62 s8) (s8 a63 s8) (s8 a64 s8) (s8 a65 s8) (s8 a5 s8) (s8 a6 s8) (s8 a7 s8) (s8 a8 s8) (s8 a9 s8) (s8 a10 s8) (s8 a66 s16) (s8 a67 s12) (s8 a11 s8) (s8 a68 s16) (s8 a69 s12) (s8 a12 s8) (s8 a13 s8) (s8 a14 s17) (s8 a15 s8) (s8 a16 s8) (s8 a17 s8) (s8 a18 s8) (s8 a19 s8) (s8 a20 s8) (s8 a21 s8) (s8 a22 s8) (s8 a23 s8) (s8 a24 s12) (s8 a25 s8) (s8 a26 s4) (s8 a27 s13) (s8 a28 s8) (s8 a29 s8) (s8 a30 s8) (s8 a31 s8) (s8 a32 s8) (s8 a33 s8) (s8 a34 s8) (s8 a35 s8) (s8 a36 s8) (s8 a37 s8) (s8 a38 s8) (s8 a39 s8) (s8 a40 s8) (s8 a41 s12) (s8 a42 s8) (s8 a43 s8) (s8 a44 s8) (s8 a45 s8) (s9 a46 s9) (s9 a47 s20) (s9 a48 s9) (s9 a49 s9) (s9 a50 s9) (s9 a51 s9) (s9 a0 s9) (s9 a1 s9) (s9 a52 s9) (s9 a53 s9) (s9 a54 s9) (s9 a55 s12) (s9 a2 s7) (s9 a56 s9) (s9 a57 s9) (s9 a58 s9) (s9 a3 s9) (s9 a59 s9) (s9 a60 s9) (s9 a4 s9) (s9 a61 s9) (s9 a62 s9) (s9 a63 s9) (s9 a64 s9) (s9 a65 s9) (s9 a5 s9) (s9 a6 s9) (s9 a7 s9) (s9 a8 s9) (s9 a9 s9) (s9 a10 s9) (s9 a66 s15) (s9 a67 s12) (s9 a11 s9) (s9 a68 s15) (s9 a69 s12) (s9 a12 s9) (s9 a13 s9) (s9 a14 s7) (s9 a15 s9) (s9 a16 s9) (s9 a17 s9) (s9 a18 s9) (s9 a19 s9) (s9 a20 s9) (s9 a21 s9) (s9 a22 s9) (s9 a23 s9) (s9 a24 s12) (s9 a25 s9) (s9 a26 s9) (s9 a27 s0) (s9 a28 s9) (s9 a29 s9) (s9 a30 s9) (s9 a31 s9) (s9 a32 s9) (s9 a33 s9) (s9 a34 s9) (s9 a35 s9) (s9 a36 s9) (s9 a37 s4) (s9 a38 s9) (s9 a39 s9) (s9 a40 s9) (s9 a41 s12) (s9 a42 s9) (s9 a43 s9) (s9 a44 s9) (s9 a45 s9) (s10 a46 s10) (s10 a47 s10) (s10 a48 s10) (s10 a49 s10) (s10 a50 s10) (s10 a51 s10) (s10 a0 s10) (s10 a1 s10) (s10 a52 s10) (s10 a53 s10) (s10 a54 s10) (s10 a55 s12) (s10 a2 s10) (s10 a56 s10) (s10 a57 s10) (s10 a58 s10) (s10 a3 s10) (s10 a59 s10) (s10 a60 s10) (s10 a4 s10) (s10 a61 s10) (s10 a62 s10) (s10 a63 s10) (s10 a64 s10) (s10 a65 s10) (s10 a5 s10) (s10 a6 s10) (s10 a7 s10) (s10 a8 s10) (s10 a9 s10) (s10 a10 s10) (s10 a66 s10) (s10 a67 s10) (s10 a11 s10) (s10 a68 s10) (s10 a69 s10) (s10 a12 s10) (s10 a13 s10) (s10 a14 s18) (s10 a15 s10) (s10 a16 s10) (s10 a17 s10) (s10 a18 s10) (s10 a19 s10) (s10 a20 s10) (s10 a21 s10) (s10 a22 s10) (s10 a23 s10) (s10 a24 s12) (s10 a25 s10) (s10 a26 s14) (s10 a27 s10) (s10 a28 s10) (s10 a29 s10) (s10 a30 s10) (s10 a31 s10) (s10 a32 s10) (s10 a33 s10) (s10 a34 s10) (s10 a35 s10) (s10 a36 s10) (s10 a37 s10) (s10 a38 s10) (s10 a39 s10) (s10 a40 s10) (s10 a41 s12) (s10 a42 s10) (s10 a43 s10) (s10 a44 s10) (s10 a45 s10) (s11 a46 s11) (s11 a47 s1) (s11 a48 s11) (s11 a49 s11) (s11 a50 s11) (s11 a51 s11) (s11 a0 s11) (s11 a1 s11) (s11 a52 s11) (s11 a53 s11) (s11 a54 s11) (s11 a55 s12) (s11 a2 s11) (s11 a56 s11) (s11 a57 s11) (s11 a58 s11) (s11 a3 s11) (s11 a59 s11) (s11 a60 s11) (s11 a4 s11) (s11 a61 s11) (s11 a62 s11) (s11 a63 s11) (s11 a64 s11) (s11 a65 s11) (s11 a5 s11) (s11 a6 s11) (s11 a7 s11) (s11 a8 s11) (s11 a9 s11) (s11 a10 s11) (s11 a66 s11) (s11 a67 s11) (s11 a11 s11) (s11 a68 s11) (s11 a69 s11) (s11 a12 s11) (s11 a13 s12) (s11 a14 s11) (s11 a15 s11) (s11 a16 s11) (s11 a17 s11) (s11 a18 s11) (s11 a19 s11) (s11 a20 s11) (s11 a21 s11) (s11 a22 s11) (s11 a23 s11) (s11 a24 s12) (s11 a25 s11) (s11 a26 s11) (s11 a27 s5) (s11 a28 s11) (s11 a29 s11) (s11 a30 s11) (s11 a31 s11) (s11 a32 s11) (s11 a33 s11) (s11 a34 s11) (s11 a35 s11) (s11 a36 s11) (s11 a37 s6) (s11 a38 s11) (s11 a39 s11) (s11 a40 s11) (s11 a41 s12) (s11 a42 s11) (s11 a43 s11) (s11 a44 s11) (s11 a45 s11) (s12 a46 s12) (s12 a47 s12) (s12 a48 s12) (s12 a49 s12) (s12 a50 s12) (s12 a51 s12) (s12 a0 s12) (s12 a1 s12) (s12 a52 s12) (s12 a53 s12) (s12 a54 s12) (s12 a55 s12) (s12 a2 s12) (s12 a56 s12) (s12 a57 s12) (s12 a58 s12) (s12 a3 s12) (s12 a59 s12) (s12 a60 s12) (s12 a4 s12) (s12 a61 s12) (s12 a62 s12) (s12 a63 s12) (s12 a64 s12) (s12 a65 s12) (s12 a5 s12) (s12 a6 s12) (s12 a7 s12) (s12 a8 s12) (s12 a9 s12) (s12 a10 s12) (s12 a66 s12) (s12 a67 s12) (s12 a11 s12) (s12 a68 s12) (s12 a69 s12) (s12 a12 s12) (s12 a13 s12) (s12 a14 s12) (s12 a15 s12) (s12 a16 s12) (s12 a17 s12) (s12 a18 s12) (s12 a19 s12) (s12 a20 s12) (s12 a21 s12) (s12 a22 s12) (s12 a23 s12) (s12 a24 s12) (s12 a25 s12) (s12 a26 s12) (s12 a27 s12) (s12 a28 s12) (s12 a29 s12) (s12 a30 s12) (s12 a31 s12) (s12 a32 s12) (s12 a33 s12) (s12 a34 s12) (s12 a35 s12) (s12 a36 s12) (s12 a37 s12) (s12 a38 s12) (s12 a39 s12) (s12 a40 s12) (s12 a41 s12) (s12 a42 s12) (s12 a43 s12) (s12 a44 s12) (s12 a45 s12) (s13 a46 s13) (s13 a47 s13) (s13 a48 s13) (s13 a49 s13) (s13 a50 s13) (s13 a51 s13) (s13 a0 s13) (s13 a1 s13) (s13 a52 s13) (s13 a53 s13) (s13 a54 s13) (s13 a55 s12) (s13 a2 s13) (s13 a56 s13) (s13 a57 s13) (s13 a58 s13) (s13 a3 s13) (s13 a59 s13) (s13 a60 s13) (s13 a4 s13) (s13 a61 s13) (s13 a62 s13) (s13 a63 s13) (s13 a64 s13) (s13 a65 s13) (s13 a5 s13) (s13 a6 s13) (s13 a7 s13) (s13 a8 s13) (s13 a9 s13) (s13 a10 s13) (s13 a66 s10) (s13 a67 s12) (s13 a11 s13) (s13 a68 s10) (s13 a69 s12) (s13 a12 s13) (s13 a13 s13) (s13 a14 s19) (s13 a15 s13) (s13 a16 s13) (s13 a17 s13) (s13 a18 s13) (s13 a19 s13) (s13 a20 s13) (s13 a21 s13) (s13 a22 s13) (s13 a23 s13) (s13 a24 s12) (s13 a25 s13) (s13 a26 s0) (s13 a27 s13) (s13 a28 s13) (s13 a29 s13) (s13 a30 s13) (s13 a31 s13) (s13 a32 s13) (s13 a33 s13) (s13 a34 s13) (s13 a35 s13) (s13 a36 s13) (s13 a37 s13) (s13 a38 s13) (s13 a39 s13) (s13 a40 s13) (s13 a41 s12) (s13 a42 s13) (s13 a43 s13) (s13 a44 s13) (s13 a45 s13) (s14 a46 s14) (s14 a47 s10) (s14 a48 s14) (s14 a49 s14) (s14 a50 s14) (s14 a51 s14) (s14 a0 s14) (s14 a1 s14) (s14 a52 s14) (s14 a53 s14) (s14 a54 s14) (s14 a55 s12) (s14 a2 s14) (s14 a56 s14) (s14 a57 s14) (s14 a58 s14) (s14 a3 s14) (s14 a59 s14) (s14 a60 s14) (s14 a4 s14) (s14 a61 s6) (s14 a62 s14) (s14 a63 s14) (s14 a64 s14) (s14 a65 s14) (s14 a5 s14) (s14 a6 s14) (s14 a7 s14) (s14 a8 s14) (s14 a9 s14) (s14 a10 s14) (s14 a66 s14) (s14 a67 s14) (s14 a11 s14) (s14 a68 s14) (s14 a69 s14) (s14 a12 s14) (s14 a13 s14) (s14 a14 s5) (s14 a15 s14) (s14 a16 s14) (s14 a17 s14) (s14 a18 s14) (s14 a19 s14) (s14 a20 s14) (s14 a21 s14) (s14 a22 s14) (s14 a23 s14) (s14 a24 s12) (s14 a25 s14) (s14 a26 s14) (s14 a27 s14) (s14 a28 s14) (s14 a29 s14) (s14 a30 s14) (s14 a31 s14) (s14 a32 s14) (s14 a33 s14) (s14 a34 s14) (s14 a35 s14) (s14 a36 s14) (s14 a37 s14) (s14 a38 s14) (s14 a39 s14) (s14 a40 s14) (s14 a41 s12) (s14 a42 s14) (s14 a43 s14) (s14 a44 s14) (s14 a45 s14) (s15 a46 s15) (s15 a47 s3) (s15 a48 s15) (s15 a49 s15) (s15 a50 s15) (s15 a51 s15) (s15 a0 s15) (s15 a1 s15) (s15 a52 s15) (s15 a53 s15) (s15 a54 s15) (s15 a55 s12) (s15 a2 s11) (s15 a56 s15) (s15 a57 s15) (s15 a58 s15) (s15 a3 s15) (s15 a59 s15) (s15 a60 s15) (s15 a4 s15) (s15 a61 s15) (s15 a62 s15) (s15 a63 s15) (s15 a64 s15) (s15 a65 s15) (s15 a5 s15) (s15 a6 s15) (s15 a7 s15) (s15 a8 s15) (s15 a9 s15) (s15 a10 s15) (s15 a66 s15) (s15 a67 s15) (s15 a11 s15) (s15 a68 s15) (s15 a69 s15) (s15 a12 s15) (s15 a13 s15) (s15 a14 s11) (s15 a15 s15) (s15 a16 s15) (s15 a17 s15) (s15 a18 s15) (s15 a19 s15) (s15 a20 s15) (s15 a21 s15) (s15 a22 s15) (s15 a23 s15) (s15 a24 s12) (s15 a25 s15) (s15 a26 s15) (s15 a27 s14) (s15 a28 s15) (s15 a29 s15) (s15 a30 s15) (s15 a31 s15) (s15 a32 s15) (s15 a33 s15) (s15 a34 s15) (s15 a35 s15) (s15 a36 s15) (s15 a37 s6) (s15 a38 s15) (s15 a39 s15) (s15 a40 s15) (s15 a41 s12) (s15 a42 s15) (s15 a43 s15) (s15 a44 s15) (s15 a45 s15) (s16 a46 s16) (s16 a47 s16) (s16 a48 s16) (s16 a49 s16) (s16 a50 s16) (s16 a51 s16) (s16 a0 s16) (s16 a1 s16) (s16 a52 s16) (s16 a53 s16) (s16 a54 s16) (s16 a55 s12) (s16 a2 s16) (s16 a56 s16) (s16 a57 s16) (s16 a58 s16) (s16 a3 s16) (s16 a59 s16) (s16 a60 s16) (s16 a4 s3) (s16 a61 s10) (s16 a62 s16) (s16 a63 s16) (s16 a64 s16) (s16 a65 s16) (s16 a5 s16) (s16 a6 s16) (s16 a7 s16) (s16 a8 s16) (s16 a9 s16) (s16 a10 s16) (s16 a66 s16) (s16 a67 s16) (s16 a11 s16) (s16 a68 s16) (s16 a69 s16) (s16 a12 s16) (s16 a13 s16) (s16 a14 s1) (s16 a15 s16) (s16 a16 s16) (s16 a17 s16) (s16 a18 s16) (s16 a19 s16) (s16 a20 s16) (s16 a21 s16) (s16 a22 s16) (s16 a23 s16) (s16 a24 s12) (s16 a25 s16) (s16 a26 s6) (s16 a27 s10) (s16 a28 s16) (s16 a29 s16) (s16 a30 s16) (s16 a31 s16) (s16 a32 s16) (s16 a33 s16) (s16 a34 s16) (s16 a35 s16) (s16 a36 s16) (s16 a37 s16) (s16 a38 s16) (s16 a39 s16) (s16 a40 s16) (s16 a41 s12) (s16 a42 s16) (s16 a43 s16) (s16 a44 s16) (s16 a45 s16) (s17 a46 s17) (s17 a47 s17) (s17 a48 s17) (s17 a49 s17) (s17 a50 s17) (s17 a51 s17) (s17 a0 s17) (s17 a1 s17) (s17 a52 s17) (s17 a53 s17) (s17 a54 s17) (s17 a55 s12) (s17 a2 s17) (s17 a56 s17) (s17 a57 s17) (s17 a58 s17) (s17 a3 s17) (s17 a59 s17) (s17 a60 s17) (s17 a4 s17) (s17 a61 s19) (s17 a62 s17) (s17 a63 s17) (s17 a64 s17) (s17 a65 s17) (s17 a5 s17) (s17 a6 s17) (s17 a7 s17) (s17 a8 s17) (s17 a9 s17) (s17 a10 s17) (s17 a66 s1) (s17 a67 s12) (s17 a11 s17) (s17 a68 s1) (s17 a69 s12) (s17 a12 s17) (s17 a13 s12) (s17 a14 s17) (s17 a15 s17) (s17 a16 s17) (s17 a17 s17) (s17 a18 s17) (s17 a19 s17) (s17 a20 s17) (s17 a21 s17) (s17 a22 s17) (s17 a23 s17) (s17 a24 s12) (s17 a25 s17) (s17 a26 s7) (s17 a27 s19) (s17 a28 s17) (s17 a29 s17) (s17 a30 s17) (s17 a31 s17) (s17 a32 s17) (s17 a33 s17) (s17 a34 s17) (s17 a35 s17) (s17 a36 s17) (s17 a37 s8) (s17 a38 s17) (s17 a39 s17) (s17 a40 s17) (s17 a41 s12) (s17 a42 s17) (s17 a43 s17) (s17 a44 s17) (s17 a45 s17) (s18 a46 s18) (s18 a47 s18) (s18 a48 s18) (s18 a49 s18) (s18 a50 s18) (s18 a51 s18) (s18 a0 s18) (s18 a1 s18) (s18 a52 s18) (s18 a53 s18) (s18 a54 s18) (s18 a55 s12) (s18 a2 s10) (s18 a56 s18) (s18 a57 s18) (s18 a58 s18) (s18 a3 s18) (s18 a59 s18) (s18 a60 s18) (s18 a4 s10) (s18 a61 s18) (s18 a62 s18) (s18 a63 s18) (s18 a64 s18) (s18 a65 s18) (s18 a5 s18) (s18 a6 s18) (s18 a7 s18) (s18 a8 s18) (s18 a9 s18) (s18 a10 s18) (s18 a66 s18) (s18 a67 s18) (s18 a11 s18) (s18 a68 s18) (s18 a69 s18) (s18 a12 s18) (s18 a13 s12) (s18 a14 s18) (s18 a15 s18) (s18 a16 s18) (s18 a17 s18) (s18 a18 s18) (s18 a19 s18) (s18 a20 s18) (s18 a21 s18) (s18 a22 s18) (s18 a23 s18) (s18 a24 s12) (s18 a25 s18) (s18 a26 s5) (s18 a27 s18) (s18 a28 s18) (s18 a29 s18) (s18 a30 s18) (s18 a31 s18) (s18 a32 s18) (s18 a33 s18) (s18 a34 s18) (s18 a35 s18) (s18 a36 s18) (s18 a37 s10) (s18 a38 s18) (s18 a39 s18) (s18 a40 s18) (s18 a41 s12) (s18 a42 s18) (s18 a43 s18) (s18 a44 s18) (s18 a45 s18) (s19 a46 s19) (s19 a47 s19) (s19 a48 s19) (s19 a49 s19) (s19 a50 s19) (s19 a51 s19) (s19 a0 s19) (s19 a1 s19) (s19 a52 s19) (s19 a53 s19) (s19 a54 s19) (s19 a55 s12) (s19 a2 s13) (s19 a56 s19) (s19 a57 s19) (s19 a58 s19) (s19 a3 s19) (s19 a59 s19) (s19 a60 s19) (s19 a4 s13) (s19 a61 s19) (s19 a62 s19) (s19 a63 s19) (s19 a64 s19) (s19 a65 s19) (s19 a5 s19) (s19 a6 s19) (s19 a7 s19) (s19 a8 s19) (s19 a9 s19) (s19 a10 s19) (s19 a66 s18) (s19 a67 s12) (s19 a11 s19) (s19 a68 s18) (s19 a69 s12) (s19 a12 s19) (s19 a13 s12) (s19 a14 s19) (s19 a15 s19) (s19 a16 s19) (s19 a17 s19) (s19 a18 s19) (s19 a19 s19) (s19 a20 s19) (s19 a21 s19) (s19 a22 s19) (s19 a23 s19) (s19 a24 s12) (s19 a25 s19) (s19 a26 s2) (s19 a27 s19) (s19 a28 s19) (s19 a29 s19) (s19 a30 s19) (s19 a31 s19) (s19 a32 s19) (s19 a33 s19) (s19 a34 s19) (s19 a35 s19) (s19 a36 s19) (s19 a37 s13) (s19 a38 s19) (s19 a39 s19) (s19 a40 s19) (s19 a41 s12) (s19 a42 s19) (s19 a43 s19) (s19 a44 s19) (s19 a45 s19) (s20 a46 s20) (s20 a47 s20) (s20 a48 s20) (s20 a49 s20) (s20 a50 s20) (s20 a51 s20) (s20 a0 s20) (s20 a1 s20) (s20 a52 s20) (s20 a53 s20) (s20 a54 s20) (s20 a55 s12) (s20 a2 s17) (s20 a56 s20) (s20 a57 s20) (s20 a58 s20) (s20 a3 s20) (s20 a59 s20) (s20 a60 s20) (s20 a4 s20) (s20 a61 s13) (s20 a62 s20) (s20 a63 s20) (s20 a64 s20) (s20 a65 s20) (s20 a5 s20) (s20 a6 s20) (s20 a7 s20) (s20 a8 s20) (s20 a9 s20) (s20 a10 s20) (s20 a66 s3) (s20 a67 s12) (s20 a11 s20) (s20 a68 s3) (s20 a69 s12) (s20 a12 s20) (s20 a13 s20) (s20 a14 s17) (s20 a15 s20) (s20 a16 s20) (s20 a17 s20) (s20 a18 s20) (s20 a19 s20) (s20 a20 s20) (s20 a21 s20) (s20 a22 s20) (s20 a23 s20) (s20 a24 s12) (s20 a25 s20) (s20 a26 s9) (s20 a27 s13) (s20 a28 s20) (s20 a29 s20) (s20 a30 s20) (s20 a31 s20) (s20 a32 s20) (s20 a33 s20) (s20 a34 s20) (s20 a35 s20) (s20 a36 s20) (s20 a37 s8) (s20 a38 s20) (s20 a39 s20) (s20 a40 s20) (s20 a41 s12) (s20 a42 s20) (s20 a43 s20) (s20 a44 s20) (s20 a45 s20) } );