// Parikh automata intersection problem, generated by OSTRICH+

counter int R0, R1, R12, R13, R2, R226, R227, R228, R229, R230, R231, R232, R233, R234, R235, R236, R237, R238, R239, R240, R241, R242, R243, R244, R245, R246, R247, R248, R249, R250, R251, R252, R253, R254, R255, R256, R257, R258, R259, R260, R261, R262, R263, R264, R265, R266, R267, R268, R269, R270, R271, R272, R273, R274, R275, R276, R277, R278, R279, R280, R281, R282, R283, R284, R285, R286, R287, R288, R289, R290, R291, R292, R293, R294, R295, R296, R297, R298, R299, R3, R300, R301, R302, R303, R304, R305, R306, R307, R308, R309, R310, R311, R312, R313, R314, R315, R316, R317, R318, R319, R320, R321, R322, R323, R324, R325, R326, R327, R328, R329, R330, R331, R332, R333, R334, R335, R336, R337, R4, R5, R6, R7, R8;

synchronised { // Automata constraining uri

automaton uri_0 {

init s0;

s0 -> s1 [109, 109];

s1 -> s2 [111, 111];

s2 -> s3 [110, 110];

s3 -> s4 [103, 103];

s4 -> s5 [111, 111];

s5 -> s6 [100, 100];

s6 -> s7 [98, 98];

s7 -> s8 [58, 58];

s8 -> s9 [47, 47];

s9 -> s10 [47, 47];

s10 -> s10 [0, 65535];

accepting s10;

};

automaton uri_1 {

init s0;

s0 -> s0 [0, 65535] { R5 += 1 };

accepting s0;

};

automaton uri_2 {

init s0;

s0 -> s1 [0, 45] { R301 += 1 };

s0 -> s0 [0, 65535] { R300 += 1, R301 += 1 };

s0 -> s2 [46, 46] { R301 += 1 };

s0 -> s3 [47, 47] { R301 += 1 };

s0 -> s1 [48, 65535] { R301 += 1 };

s1 -> s1 [0, 45] { R301 += 1 };

s1 -> s2 [46, 46] { R301 += 1 };

s1 -> s3 [47, 47] { R301 += 1 };

s1 -> s1 [48, 65535] { R301 += 1 };

s2 -> s1 [0, 45] { R301 += 1 };

s2 -> s2 [46, 46] { R301 += 1 };

s2 -> s3 [47, 47] { R301 += 1 };

s2 -> s1 [48, 114] { R301 += 1 };

s2 -> s8 [115, 115] { R301 += 1 };

s2 -> s1 [116, 65535] { R301 += 1 };

s3 -> s3 [0, 45] { R301 += 1 };

s3 -> s3 [0, 65535];

s3 -> s4 [46, 46] { R301 += 1 };

s3 -> s3 [47, 65535] { R301 += 1 };

s4 -> s3 [0, 45] { R301 += 1 };

s4 -> s4 [0, 65535];

s4 -> s4 [46, 46] { R301 += 1 };

s4 -> s3 [47, 114] { R301 += 1 };

s4 -> s5 [115, 115] { R301 += 1 };

s4 -> s3 [116, 65535] { R301 += 1 };

s5 -> s3 [0, 45] { R301 += 1 };

s5 -> s5 [0, 65535];

s5 -> s4 [46, 46] { R301 += 1 };

s5 -> s3 [47, 110] { R301 += 1 };

s5 -> s6 [111, 111] { R301 += 1 };

s5 -> s3 [112, 65535] { R301 += 1 };

s6 -> s3 [0, 45] { R301 += 1 };

s6 -> s6 [0, 65535];

s6 -> s4 [46, 46] { R301 += 1 };

s6 -> s3 [47, 98] { R301 += 1 };

s6 -> s7 [99, 99] { R301 += 1 };

s6 -> s3 [100, 65535] { R301 += 1 };

s7 -> s3 [0, 45] { R301 += 1 };

s7 -> s7 [0, 65535];

s7 -> s4 [46, 46] { R301 += 1 };

s7 -> s3 [47, 106] { R301 += 1 };

s7 -> s3 [108, 65535] { R301 += 1 };

s8 -> s1 [0, 45] { R301 += 1 };

s8 -> s2 [46, 46] { R301 += 1 };

s8 -> s3 [47, 47] { R301 += 1 };

s8 -> s1 [48, 110] { R301 += 1 };

s8 -> s9 [111, 111] { R301 += 1 };

s8 -> s1 [112, 65535] { R301 += 1 };

s9 -> s1 [0, 45] { R301 += 1 };

s9 -> s2 [46, 46] { R301 += 1 };

s9 -> s3 [47, 47] { R301 += 1 };

s9 -> s1 [48, 98] { R301 += 1 };

s9 -> s10 [99, 99] { R301 += 1 };

s9 -> s1 [100, 65535] { R301 += 1 };

s10 -> s1 [0, 45] { R301 += 1 };

s10 -> s2 [46, 46] { R301 += 1 };

s10 -> s3 [47, 47] { R301 += 1 };

s10 -> s1 [48, 106] { R301 += 1 };

s10 -> s1 [108, 65535] { R301 += 1 };

accepting s3, s4, s5, s6, s7;

};

automaton uri_3 {

init s0;

s0 -> s1 [0, 65535] { R303 += 1, R4 += 1 };

s0 -> s0 [0, 65535] { R302 += 1, R303 += 1 };

s1 -> s2 [0, 65535];

s1 -> s1 [0, 65535] { R303 += 1, R4 += 1 };

s2 -> s2 [0, 65535];

accepting s0, s1, s2;

};

automaton uri_4 {

init s0;

s0 -> s1 [0, 46] { R305 += 1, R13 += 1 };

s0 -> s2 [0, 65535] { R305 += 1, R12 += 1, R13 += 1 };

s0 -> s0 [0, 65535] { R304 += 1, R305 += 1 };

s0 -> s3 [47, 47] { R305 += 1 };

s0 -> s1 [48, 65535] { R305 += 1, R13 += 1 };

s1 -> s1 [0, 46] { R305 += 1, R13 += 1 };

s1 -> s3 [47, 47] { R305 += 1 };

s1 -> s1 [48, 65535] { R305 += 1, R13 += 1 };

s2 -> s1 [0, 46] { R305 += 1, R13 += 1 };

s2 -> s2 [0, 65535] { R305 += 1, R12 += 1, R13 += 1 };

s2 -> s3 [47, 47] { R305 += 1 };

s2 -> s1 [48, 65535] { R305 += 1, R13 += 1 };

s3 -> s3 [0, 65535] { R305 += 1 };

s3 -> s4 [0, 65535];

s4 -> s4 [0, 65535];

accepting s3, s4;

};

automaton uri_5 {

init s0;

s0 -> s1 [0, 65535] { R307 += 1, R237 += 1, R1 += 1 };

s0 -> s2 [0, 65535] { R307 += 1, R236 += 1, R237 += 1 };

s0 -> s0 [0, 65535] { R306 += 1, R307 += 1 };

s1 -> s1 [0, 65535] { R307 += 1, R237 += 1, R1 += 1 };

s1 -> s3 [0, 65535];

s1 -> s4 [0, 65535] { R307 += 1 };

s2 -> s1 [0, 65535] { R307 += 1, R237 += 1, R1 += 1 };

s2 -> s3 [0, 65535];

s2 -> s2 [0, 65535] { R307 += 1, R236 += 1, R237 += 1 };

s3 -> s3 [0, 65535];

s4 -> s3 [0, 65535];

s4 -> s4 [0, 65535] { R307 += 1 };

accepting s3, s4, s2, s1, s0;

};

automaton uri_6 {

init s0;

s0 -> s1 [0, 63] { R309 += 1, R271 += 1 };

s0 -> s2 [0, 65535] { R309 += 1, R270 += 1, R271 += 1 };

s0 -> s0 [0, 65535] { R308 += 1, R309 += 1 };

s0 -> s3 [64, 64] { R309 += 1, R271 += 1 };

s0 -> s1 [65, 65535] { R309 += 1, R271 += 1 };

s1 -> s1 [0, 63] { R309 += 1, R271 += 1 };

s1 -> s3 [64, 64] { R309 += 1, R271 += 1 };

s1 -> s1 [65, 65535] { R309 += 1, R271 += 1 };

s2 -> s1 [0, 63] { R309 += 1, R271 += 1 };

s2 -> s2 [0, 65535] { R309 += 1, R270 += 1, R271 += 1 };

s2 -> s3 [64, 64] { R309 += 1, R271 += 1 };

s2 -> s1 [65, 65535] { R309 += 1, R271 += 1 };

s3 -> s4 [0, 65535] { R309 += 1 };

s3 -> s3 [0, 65535] { R309 += 1, R271 += 1 };

s3 -> s5 [0, 65535];

s4 -> s4 [0, 65535] { R309 += 1 };

s4 -> s5 [0, 65535];

s5 -> s5 [0, 65535];

accepting s3, s4, s5;

};

automaton uri_7 {

init s0;

s0 -> s1 [0, 65535] { R311 += 1, R273 += 1, R3 += 1 };

s0 -> s2 [0, 65535] { R311 += 1, R272 += 1, R273 += 1 };

s0 -> s0 [0, 65535] { R310 += 1, R311 += 1 };

s1 -> s4 [0, 65535] { R311 += 1 };

s1 -> s1 [0, 65535] { R311 += 1, R273 += 1, R3 += 1 };

s1 -> s3 [0, 65535];

s2 -> s1 [0, 65535] { R311 += 1, R273 += 1, R3 += 1 };

s2 -> s3 [0, 65535];

s2 -> s2 [0, 65535] { R311 += 1, R272 += 1, R273 += 1 };

s3 -> s3 [0, 65535];

s4 -> s4 [0, 65535] { R311 += 1 };

s4 -> s3 [0, 65535];

accepting s3, s4, s2, s1, s0;

};

automaton uri_8 {

init s0;

s0 -> s1 [0, 36] { R313 += 1, R275 += 1, R233 += 1 };

s0 -> s0 [0, 65535] { R312 += 1, R313 += 1 };

s0 -> s2 [0, 65535] { R313 += 1, R274 += 1, R275 += 1 };

s0 -> s3 [0, 65535] { R313 += 1, R275 += 1, R232 += 1, R233 += 1 };

s0 -> s1 [38, 42] { R313 += 1, R275 += 1, R233 += 1 };

s0 -> s1 [44, 57] { R313 += 1, R275 += 1, R233 += 1 };

s0 -> s1 [59, 63] { R313 += 1, R275 += 1, R233 += 1 };

s0 -> s1 [65, 65535] { R313 += 1, R275 += 1, R233 += 1 };

s1 -> s1 [0, 36] { R313 += 1, R275 += 1, R233 += 1 };

s1 -> s4 [0, 65535];

s1 -> s5 [0, 65535] { R313 += 1 };

s1 -> s1 [0, 65535] { R313 += 1, R275 += 1 };

s1 -> s1 [38, 42] { R313 += 1, R275 += 1, R233 += 1 };

s1 -> s1 [44, 57] { R313 += 1, R275 += 1, R233 += 1 };

s1 -> s1 [59, 63] { R313 += 1, R275 += 1, R233 += 1 };

s1 -> s1 [65, 65535] { R313 += 1, R275 += 1, R233 += 1 };

s2 -> s1 [0, 36] { R313 += 1, R275 += 1, R233 += 1 };

s2 -> s4 [0, 65535];

s2 -> s2 [0, 65535] { R313 += 1, R274 += 1, R275 += 1 };

s2 -> s3 [0, 65535] { R313 += 1, R275 += 1, R232 += 1, R233 += 1 };

s2 -> s1 [38, 42] { R313 += 1, R275 += 1, R233 += 1 };

s2 -> s1 [44, 57] { R313 += 1, R275 += 1, R233 += 1 };

s2 -> s1 [59, 63] { R313 += 1, R275 += 1, R233 += 1 };

s2 -> s1 [65, 65535] { R313 += 1, R275 += 1, R233 += 1 };

s3 -> s1 [0, 36] { R313 += 1, R275 += 1, R233 += 1 };

s3 -> s4 [0, 65535];

s3 -> s5 [0, 65535] { R313 += 1 };

s3 -> s3 [0, 65535] { R313 += 1, R275 += 1, R232 += 1, R233 += 1 };

s3 -> s1 [38, 42] { R313 += 1, R275 += 1, R233 += 1 };

s3 -> s1 [44, 57] { R313 += 1, R275 += 1, R233 += 1 };

s3 -> s1 [59, 63] { R313 += 1, R275 += 1, R233 += 1 };

s3 -> s1 [65, 65535] { R313 += 1, R275 += 1, R233 += 1 };

s4 -> s4 [0, 65535];

s5 -> s4 [0, 65535];

s5 -> s5 [0, 65535] { R313 += 1 };

accepting s3, s4, s5, s2, s1, s0;

};

automaton uri_9 {

init s0;

s0 -> s1 [0, 65535] { R315 += 1, R277 += 1, R234 += 1, R235 += 1 };

s0 -> s0 [0, 65535] { R314 += 1, R315 += 1 };

s0 -> s2 [0, 65535] { R315 += 1, R277 += 1, R235 += 1, R0 += 1 };

s0 -> s3 [0, 65535] { R315 += 1, R276 += 1, R277 += 1 };

s1 -> s1 [0, 65535] { R315 += 1, R277 += 1, R234 += 1, R235 += 1 };

s1 -> s4 [0, 65535];

s1 -> s2 [0, 65535] { R315 += 1, R277 += 1, R235 += 1, R0 += 1 };

s1 -> s6 [0, 65535] { R315 += 1 };

s2 -> s5 [0, 65535] { R315 += 1, R277 += 1 };

s2 -> s4 [0, 65535];

s2 -> s2 [0, 65535] { R315 += 1, R277 += 1, R235 += 1, R0 += 1 };

s2 -> s6 [0, 65535] { R315 += 1 };

s3 -> s1 [0, 65535] { R315 += 1, R277 += 1, R234 += 1, R235 += 1 };

s3 -> s4 [0, 65535];

s3 -> s2 [0, 65535] { R315 += 1, R277 += 1, R235 += 1, R0 += 1 };

s3 -> s3 [0, 65535] { R315 += 1, R276 += 1, R277 += 1 };

s4 -> s4 [0, 65535];

s5 -> s5 [0, 65535] { R315 += 1, R277 += 1 };

s5 -> s4 [0, 65535];

s5 -> s6 [0, 65535] { R315 += 1 };

s6 -> s4 [0, 65535];

s6 -> s6 [0, 65535] { R315 += 1 };

accepting s3, s4, s5, s2, s6, s1, s0;

};

automaton uri_10 {

init s0;

s0 -> s1 [0, 43] { R317 += 1, R279 += 1, R249 += 1 };

s0 -> s2 [0, 65535] { R317 += 1, R278 += 1, R279 += 1 };

s0 -> s3 [0, 65535] { R317 += 1, R279 += 1, R248 += 1, R249 += 1 };

s0 -> s0 [0, 65535] { R316 += 1, R317 += 1 };

s0 -> s1 [45, 64] { R317 += 1, R279 += 1, R249 += 1 };

s0 -> s4 [82, 82] { R317 += 1, R279 += 1, R249 += 1 };

s0 -> s1 [83, 65535] { R317 += 1, R279 += 1, R249 += 1 };

s1 -> s1 [0, 43] { R317 += 1, R279 += 1, R249 += 1 };

s1 -> s1 [45, 64] { R317 += 1, R279 += 1, R249 += 1 };

s1 -> s4 [82, 82] { R317 += 1, R279 += 1, R249 += 1 };

s1 -> s1 [83, 65535] { R317 += 1, R279 += 1, R249 += 1 };

s2 -> s1 [0, 43] { R317 += 1, R279 += 1, R249 += 1 };

s2 -> s2 [0, 65535] { R317 += 1, R278 += 1, R279 += 1 };

s2 -> s3 [0, 65535] { R317 += 1, R279 += 1, R248 += 1, R249 += 1 };

s2 -> s1 [45, 64] { R317 += 1, R279 += 1, R249 += 1 };

s2 -> s4 [82, 82] { R317 += 1, R279 += 1, R249 += 1 };

s2 -> s1 [83, 65535] { R317 += 1, R279 += 1, R249 += 1 };

s3 -> s1 [0, 43] { R317 += 1, R279 += 1, R249 += 1 };

s3 -> s3 [0, 65535] { R317 += 1, R279 += 1, R248 += 1, R249 += 1 };

s3 -> s1 [45, 64] { R317 += 1, R279 += 1, R249 += 1 };

s3 -> s4 [82, 82] { R317 += 1, R279 += 1, R249 += 1 };

s3 -> s1 [83, 65535] { R317 += 1, R279 += 1, R249 += 1 };

s4 -> s4 [0, 43] { R317 += 1, R279 += 1, R249 += 1 };

s4 -> s4 [0, 65535] { R317 += 1, R279 += 1 };

s4 -> s5 [0, 65535];

s4 -> s6 [0, 65535] { R317 += 1 };

s4 -> s4 [45, 64] { R317 += 1, R279 += 1, R249 += 1 };

s4 -> s4 [82, 65535] { R317 += 1, R279 += 1, R249 += 1 };

s5 -> s5 [0, 65535];

s6 -> s5 [0, 65535];

s6 -> s6 [0, 65535] { R317 += 1 };

accepting s4, s5, s6;

};

automaton uri_11 {

init s0;

s0 -> s0 [0, 65535] { R318 += 1, R319 += 1 };

s0 -> s1 [0, 65535] { R319 += 1, R281 += 1, R251 += 1, R2 += 1 };

s0 -> s2 [0, 65535] { R319 += 1, R280 += 1, R281 += 1 };

s0 -> s3 [0, 65535] { R319 += 1, R281 += 1, R250 += 1, R251 += 1 };

s1 -> s1 [0, 65535] { R319 += 1, R281 += 1, R251 += 1, R2 += 1 };

s1 -> s4 [0, 65535] { R319 += 1 };

s1 -> s6 [0, 65535] { R319 += 1, R281 += 1 };

s1 -> s5 [0, 65535];

s2 -> s1 [0, 65535] { R319 += 1, R281 += 1, R251 += 1, R2 += 1 };

s2 -> s2 [0, 65535] { R319 += 1, R280 += 1, R281 += 1 };

s2 -> s3 [0, 65535] { R319 += 1, R281 += 1, R250 += 1, R251 += 1 };

s2 -> s5 [0, 65535];

s3 -> s1 [0, 65535] { R319 += 1, R281 += 1, R251 += 1, R2 += 1 };

s3 -> s4 [0, 65535] { R319 += 1 };

s3 -> s3 [0, 65535] { R319 += 1, R281 += 1, R250 += 1, R251 += 1 };

s3 -> s5 [0, 65535];

s4 -> s4 [0, 65535] { R319 += 1 };

s4 -> s5 [0, 65535];

s5 -> s5 [0, 65535];

s6 -> s4 [0, 65535] { R319 += 1 };

s6 -> s6 [0, 65535] { R319 += 1, R281 += 1 };

s6 -> s5 [0, 65535];

accepting s3, s4, s5, s2, s6, s1, s0;

};

automaton uri_12 {

init s0;

s0 -> s1 [0, 57] { R321 += 1, R283 += 1, R253 += 1 };

s0 -> s0 [0, 65535] { R320 += 1, R321 += 1 };

s0 -> s2 [0, 65535] { R321 += 1, R283 += 1, R253 += 1, R7 += 1 };

s0 -> s3 [0, 65535] { R321 += 1, R283 += 1, R252 += 1, R253 += 1 };

s0 -> s4 [0, 65535] { R321 += 1, R282 += 1, R283 += 1 };

s0 -> s5 [58, 58] { R321 += 1, R283 += 1, R253 += 1 };

s0 -> s1 [59, 65535] { R321 += 1, R283 += 1, R253 += 1 };

s1 -> s1 [0, 57] { R321 += 1, R283 += 1, R253 += 1 };

s1 -> s7 [0, 65535] { R321 += 1 };

s1 -> s6 [0, 65535];

s1 -> s1 [0, 65535] { R321 += 1, R283 += 1 };

s1 -> s5 [58, 58] { R321 += 1, R283 += 1, R253 += 1 };

s1 -> s1 [59, 65535] { R321 += 1, R283 += 1, R253 += 1 };

s2 -> s1 [0, 57] { R321 += 1, R283 += 1, R253 += 1 };

s2 -> s7 [0, 65535] { R321 += 1 };

s2 -> s6 [0, 65535];

s2 -> s2 [0, 65535] { R321 += 1, R283 += 1, R253 += 1, R7 += 1 };

s2 -> s8 [0, 65535] { R321 += 1, R283 += 1 };

s2 -> s5 [58, 58] { R321 += 1, R283 += 1, R253 += 1 };

s2 -> s1 [59, 65535] { R321 += 1, R283 += 1, R253 += 1 };

s3 -> s1 [0, 57] { R321 += 1, R283 += 1, R253 += 1 };

s3 -> s7 [0, 65535] { R321 += 1 };

s3 -> s6 [0, 65535];

s3 -> s2 [0, 65535] { R321 += 1, R283 += 1, R253 += 1, R7 += 1 };

s3 -> s3 [0, 65535] { R321 += 1, R283 += 1, R252 += 1, R253 += 1 };

s3 -> s5 [58, 58] { R321 += 1, R283 += 1, R253 += 1 };

s3 -> s1 [59, 65535] { R321 += 1, R283 += 1, R253 += 1 };

s4 -> s1 [0, 57] { R321 += 1, R283 += 1, R253 += 1 };

s4 -> s6 [0, 65535];

s4 -> s2 [0, 65535] { R321 += 1, R283 += 1, R253 += 1, R7 += 1 };

s4 -> s3 [0, 65535] { R321 += 1, R283 += 1, R252 += 1, R253 += 1 };

s4 -> s4 [0, 65535] { R321 += 1, R282 += 1, R283 += 1 };

s4 -> s5 [58, 58] { R321 += 1, R283 += 1, R253 += 1 };

s4 -> s1 [59, 65535] { R321 += 1, R283 += 1, R253 += 1 };

s5 -> s5 [0, 65535] { R321 += 1, R283 += 1, R253 += 1 };

s6 -> s6 [0, 65535];

s7 -> s7 [0, 65535] { R321 += 1 };

s7 -> s6 [0, 65535];

s8 -> s7 [0, 65535] { R321 += 1 };

s8 -> s6 [0, 65535];

s8 -> s8 [0, 65535] { R321 += 1, R283 += 1 };

accepting s3, s4, s8, s2, s6, s1, s7, s0;

};

automaton uri_13 {

init s0;

s0 -> s1 [0, 81] { R323 += 1, R285 += 1, R255 += 1 };

s0 -> s2 [0, 65535] { R323 += 1, R285 += 1, R255 += 1, R8 += 1 };

s0 -> s0 [0, 65535] { R322 += 1, R323 += 1 };

s0 -> s3 [0, 65535] { R323 += 1, R285 += 1, R254 += 1, R255 += 1 };

s0 -> s4 [0, 65535] { R323 += 1, R284 += 1, R285 += 1 };

s0 -> s5 [82, 82] { R323 += 1, R285 += 1, R255 += 1 };

s0 -> s1 [83, 65535] { R323 += 1, R285 += 1, R255 += 1 };

s1 -> s1 [0, 81] { R323 += 1, R285 += 1, R255 += 1 };

s1 -> s7 [0, 65535] { R323 += 1 };

s1 -> s6 [0, 65535];

s1 -> s1 [0, 65535] { R323 += 1, R285 += 1 };

s1 -> s5 [82, 82] { R323 += 1, R285 += 1, R255 += 1 };

s1 -> s1 [83, 65535] { R323 += 1, R285 += 1, R255 += 1 };

s2 -> s1 [0, 81] { R323 += 1, R285 += 1, R255 += 1 };

s2 -> s7 [0, 65535] { R323 += 1 };

s2 -> s2 [0, 65535] { R323 += 1, R285 += 1, R255 += 1, R8 += 1 };

s2 -> s8 [0, 65535] { R323 += 1, R285 += 1 };

s2 -> s6 [0, 65535];

s2 -> s5 [82, 82] { R323 += 1, R285 += 1, R255 += 1 };

s2 -> s1 [83, 65535] { R323 += 1, R285 += 1, R255 += 1 };

s3 -> s1 [0, 81] { R323 += 1, R285 += 1, R255 += 1 };

s3 -> s7 [0, 65535] { R323 += 1 };

s3 -> s2 [0, 65535] { R323 += 1, R285 += 1, R255 += 1, R8 += 1 };

s3 -> s3 [0, 65535] { R323 += 1, R285 += 1, R254 += 1, R255 += 1 };

s3 -> s6 [0, 65535];

s3 -> s5 [82, 82] { R323 += 1, R285 += 1, R255 += 1 };

s3 -> s1 [83, 65535] { R323 += 1, R285 += 1, R255 += 1 };

s4 -> s1 [0, 81] { R323 += 1, R285 += 1, R255 += 1 };

s4 -> s2 [0, 65535] { R323 += 1, R285 += 1, R255 += 1, R8 += 1 };

s4 -> s3 [0, 65535] { R323 += 1, R285 += 1, R254 += 1, R255 += 1 };

s4 -> s6 [0, 65535];

s4 -> s4 [0, 65535] { R323 += 1, R284 += 1, R285 += 1 };

s4 -> s5 [82, 82] { R323 += 1, R285 += 1, R255 += 1 };

s4 -> s1 [83, 65535] { R323 += 1, R285 += 1, R255 += 1 };

s5 -> s5 [0, 65535] { R323 += 1, R285 += 1, R255 += 1 };

s6 -> s6 [0, 65535];

s7 -> s7 [0, 65535] { R323 += 1 };

s7 -> s6 [0, 65535];

s8 -> s7 [0, 65535] { R323 += 1 };

s8 -> s8 [0, 65535] { R323 += 1, R285 += 1 };

s8 -> s6 [0, 65535];

accepting s3, s4, s8, s2, s6, s1, s7, s0;

};

automaton uri_14 {

init s0;

s0 -> s1 [0, 90] { R325 += 1, R287 += 1, R257 += 1, R229 += 1 };

s0 -> s2 [0, 65535] { R325 += 1, R287 += 1, R257 += 1, R228 += 1, R229 += 1 };

s0 -> s3 [0, 65535] { R325 += 1, R287 += 1, R256 += 1, R257 += 1 };

s0 -> s0 [0, 65535] { R324 += 1, R325 += 1 };

s0 -> s4 [0, 65535] { R325 += 1, R286 += 1, R287 += 1 };

s0 -> s5 [91, 91] { R325 += 1, R287 += 1, R257 += 1, R229 += 1 };

s0 -> s1 [92, 65535] { R325 += 1, R287 += 1, R257 += 1, R229 += 1 };

s1 -> s1 [0, 65535] { R325 += 1, R287 += 1, R257 += 1, R229 += 1 };

s1 -> s7 [0, 65535] { R325 += 1 };

s1 -> s8 [0, 65535] { R325 += 1, R287 += 1 };

s1 -> s6 [0, 65535];

s1 -> s9 [0, 65535] { R325 += 1, R287 += 1, R257 += 1 };

s2 -> s1 [0, 90] { R325 += 1, R287 += 1, R257 += 1, R229 += 1 };

s2 -> s2 [0, 65535] { R325 += 1, R287 += 1, R257 += 1, R228 += 1, R229 += 1 };

s2 -> s7 [0, 65535] { R325 += 1 };

s2 -> s8 [0, 65535] { R325 += 1, R287 += 1 };

s2 -> s6 [0, 65535];

s2 -> s5 [91, 91] { R325 += 1, R287 += 1, R257 += 1, R229 += 1 };

s2 -> s1 [92, 65535] { R325 += 1, R287 += 1, R257 += 1, R229 += 1 };

s3 -> s1 [0, 90] { R325 += 1, R287 += 1, R257 += 1, R229 += 1 };

s3 -> s2 [0, 65535] { R325 += 1, R287 += 1, R257 += 1, R228 += 1, R229 += 1 };

s3 -> s7 [0, 65535] { R325 += 1 };

s3 -> s6 [0, 65535];

s3 -> s3 [0, 65535] { R325 += 1, R287 += 1, R256 += 1, R257 += 1 };

s3 -> s5 [91, 91] { R325 += 1, R287 += 1, R257 += 1, R229 += 1 };

s3 -> s1 [92, 65535] { R325 += 1, R287 += 1, R257 += 1, R229 += 1 };

s4 -> s1 [0, 90] { R325 += 1, R287 += 1, R257 += 1, R229 += 1 };

s4 -> s2 [0, 65535] { R325 += 1, R287 += 1, R257 += 1, R228 += 1, R229 += 1 };

s4 -> s6 [0, 65535];

s4 -> s3 [0, 65535] { R325 += 1, R287 += 1, R256 += 1, R257 += 1 };

s4 -> s4 [0, 65535] { R325 += 1, R286 += 1, R287 += 1 };

s4 -> s5 [91, 91] { R325 += 1, R287 += 1, R257 += 1, R229 += 1 };

s4 -> s1 [92, 65535] { R325 += 1, R287 += 1, R257 += 1, R229 += 1 };

s5 -> s1 [0, 65535] { R325 += 1, R287 += 1, R257 += 1, R229 += 1 };

s6 -> s6 [0, 65535];

s7 -> s7 [0, 65535] { R325 += 1 };

s7 -> s6 [0, 65535];

s8 -> s7 [0, 65535] { R325 += 1 };

s8 -> s8 [0, 65535] { R325 += 1, R287 += 1 };

s8 -> s6 [0, 65535];

s9 -> s7 [0, 65535] { R325 += 1 };

s9 -> s8 [0, 65535] { R325 += 1, R287 += 1 };

s9 -> s6 [0, 65535];

s9 -> s9 [0, 65535] { R325 += 1, R287 += 1, R257 += 1 };

accepting s3, s4, s8, s2, s9, s6, s1, s7, s0;

};

automaton uri_15 {

init s0;

s0 -> s0 [0, 65535] { R326 += 1, R327 += 1 };

s0 -> s1 [0, 65535] { R327 += 1, R289 += 1, R259 += 1, R230 += 1, R231 += 1 };

s0 -> s2 [0, 65535] { R327 += 1, R289 += 1, R259 += 1, R231 += 1, R6 += 1 };

s0 -> s3 [0, 65535] { R327 += 1, R288 += 1, R289 += 1 };

s0 -> s4 [0, 65535] { R327 += 1, R289 += 1, R258 += 1, R259 += 1 };

s1 -> s5 [0, 65535];

s1 -> s1 [0, 65535] { R327 += 1, R289 += 1, R259 += 1, R230 += 1, R231 += 1 };

s1 -> s2 [0, 65535] { R327 += 1, R289 += 1, R259 += 1, R231 += 1, R6 += 1 };

s1 -> s7 [0, 65535] { R327 += 1, R289 += 1 };

s1 -> s6 [0, 65535] { R327 += 1 };

s2 -> s5 [0, 65535];

s2 -> s2 [0, 65535] { R327 += 1, R289 += 1, R259 += 1, R231 += 1, R6 += 1 };

s2 -> s7 [0, 65535] { R327 += 1, R289 += 1 };

s2 -> s6 [0, 65535] { R327 += 1 };

s2 -> s8 [0, 65535] { R327 += 1, R289 += 1, R259 += 1 };

s3 -> s5 [0, 65535];

s3 -> s1 [0, 65535] { R327 += 1, R289 += 1, R259 += 1, R230 += 1, R231 += 1 };

s3 -> s2 [0, 65535] { R327 += 1, R289 += 1, R259 += 1, R231 += 1, R6 += 1 };

s3 -> s3 [0, 65535] { R327 += 1, R288 += 1, R289 += 1 };

s3 -> s4 [0, 65535] { R327 += 1, R289 += 1, R258 += 1, R259 += 1 };

s4 -> s5 [0, 65535];

s4 -> s1 [0, 65535] { R327 += 1, R289 += 1, R259 += 1, R230 += 1, R231 += 1 };

s4 -> s2 [0, 65535] { R327 += 1, R289 += 1, R259 += 1, R231 += 1, R6 += 1 };

s4 -> s4 [0, 65535] { R327 += 1, R289 += 1, R258 += 1, R259 += 1 };

s4 -> s6 [0, 65535] { R327 += 1 };

s5 -> s5 [0, 65535];

s6 -> s5 [0, 65535];

s6 -> s6 [0, 65535] { R327 += 1 };

s7 -> s5 [0, 65535];

s7 -> s7 [0, 65535] { R327 += 1, R289 += 1 };

s7 -> s6 [0, 65535] { R327 += 1 };

s8 -> s5 [0, 65535];

s8 -> s7 [0, 65535] { R327 += 1, R289 += 1 };

s8 -> s6 [0, 65535] { R327 += 1 };

s8 -> s8 [0, 65535] { R327 += 1, R289 += 1, R259 += 1 };

accepting s3, s4, s8, s5, s2, s6, s1, s7, s0;

};

automaton uri_16 {

init s0;

s0 -> s1 [0, 81] { R329 += 1, R291 += 1, R261 += 1, R239 += 1 };

s0 -> s2 [0, 65535] { R329 += 1, R291 += 1, R260 += 1, R261 += 1 };

s0 -> s3 [0, 65535] { R329 += 1, R290 += 1, R291 += 1 };

s0 -> s0 [0, 65535] { R328 += 1, R329 += 1 };

s0 -> s4 [0, 65535] { R329 += 1, R291 += 1, R261 += 1, R238 += 1, R239 += 1 };

s0 -> s1 [83, 65535] { R329 += 1, R291 += 1, R261 += 1, R239 += 1 };

s1 -> s1 [0, 81] { R329 += 1, R291 += 1, R261 += 1, R239 += 1 };

s1 -> s5 [0, 65535] { R329 += 1 };

s1 -> s1 [0, 65535] { R329 += 1, R291 += 1, R261 += 1 };

s1 -> s6 [0, 65535];

s1 -> s7 [0, 65535] { R329 += 1, R291 += 1 };

s1 -> s1 [83, 65535] { R329 += 1, R291 += 1, R261 += 1, R239 += 1 };

s2 -> s1 [0, 81] { R329 += 1, R291 += 1, R261 += 1, R239 += 1 };

s2 -> s2 [0, 65535] { R329 += 1, R291 += 1, R260 += 1, R261 += 1 };

s2 -> s5 [0, 65535] { R329 += 1 };

s2 -> s6 [0, 65535];

s2 -> s4 [0, 65535] { R329 += 1, R291 += 1, R261 += 1, R238 += 1, R239 += 1 };

s2 -> s1 [83, 65535] { R329 += 1, R291 += 1, R261 += 1, R239 += 1 };

s3 -> s1 [0, 81] { R329 += 1, R291 += 1, R261 += 1, R239 += 1 };

s3 -> s2 [0, 65535] { R329 += 1, R291 += 1, R260 += 1, R261 += 1 };

s3 -> s3 [0, 65535] { R329 += 1, R290 += 1, R291 += 1 };

s3 -> s6 [0, 65535];

s3 -> s4 [0, 65535] { R329 += 1, R291 += 1, R261 += 1, R238 += 1, R239 += 1 };

s3 -> s1 [83, 65535] { R329 += 1, R291 += 1, R261 += 1, R239 += 1 };

s4 -> s1 [0, 81] { R329 += 1, R291 += 1, R261 += 1, R239 += 1 };

s4 -> s5 [0, 65535] { R329 += 1 };

s4 -> s6 [0, 65535];

s4 -> s4 [0, 65535] { R329 += 1, R291 += 1, R261 += 1, R238 += 1, R239 += 1 };

s4 -> s7 [0, 65535] { R329 += 1, R291 += 1 };

s4 -> s1 [83, 65535] { R329 += 1, R291 += 1, R261 += 1, R239 += 1 };

s5 -> s5 [0, 65535] { R329 += 1 };

s5 -> s6 [0, 65535];

s6 -> s6 [0, 65535];

s7 -> s5 [0, 65535] { R329 += 1 };

s7 -> s6 [0, 65535];

s7 -> s7 [0, 65535] { R329 += 1, R291 += 1 };

accepting s3, s4, s5, s2, s6, s1, s7, s0;

};

automaton uri_17 {

init s0;

s0 -> s1 [0, 65535] { R331 += 1, R293 += 1, R262 += 1, R263 += 1 };

s0 -> s2 [0, 65535] { R331 += 1, R293 += 1, R263 += 1, R241 += 1, R226 += 1 };

s0 -> s3 [0, 65535] { R331 += 1, R293 += 1, R263 += 1, R240 += 1, R241 += 1 };

s0 -> s0 [0, 65535] { R330 += 1, R331 += 1 };

s0 -> s4 [0, 65535] { R331 += 1, R292 += 1, R293 += 1 };

s1 -> s1 [0, 65535] { R331 += 1, R293 += 1, R262 += 1, R263 += 1 };

s1 -> s7 [0, 65535] { R331 += 1 };

s1 -> s2 [0, 65535] { R331 += 1, R293 += 1, R263 += 1, R241 += 1, R226 += 1 };

s1 -> s3 [0, 65535] { R331 += 1, R293 += 1, R263 += 1, R240 += 1, R241 += 1 };

s1 -> s5 [0, 65535];

s2 -> s6 [0, 65535] { R331 += 1, R293 += 1 };

s2 -> s7 [0, 65535] { R331 += 1 };

s2 -> s2 [0, 65535] { R331 += 1, R293 += 1, R263 += 1, R241 += 1, R226 += 1 };

s2 -> s5 [0, 65535];

s2 -> s8 [0, 65535] { R331 += 1, R293 += 1, R263 += 1 };

s3 -> s6 [0, 65535] { R331 += 1, R293 += 1 };

s3 -> s7 [0, 65535] { R331 += 1 };

s3 -> s2 [0, 65535] { R331 += 1, R293 += 1, R263 += 1, R241 += 1, R226 += 1 };

s3 -> s3 [0, 65535] { R331 += 1, R293 += 1, R263 += 1, R240 += 1, R241 += 1 };

s3 -> s5 [0, 65535];

s4 -> s1 [0, 65535] { R331 += 1, R293 += 1, R262 += 1, R263 += 1 };

s4 -> s2 [0, 65535] { R331 += 1, R293 += 1, R263 += 1, R241 += 1, R226 += 1 };

s4 -> s3 [0, 65535] { R331 += 1, R293 += 1, R263 += 1, R240 += 1, R241 += 1 };

s4 -> s5 [0, 65535];

s4 -> s4 [0, 65535] { R331 += 1, R292 += 1, R293 += 1 };

s5 -> s5 [0, 65535];

s6 -> s6 [0, 65535] { R331 += 1, R293 += 1 };

s6 -> s7 [0, 65535] { R331 += 1 };

s6 -> s5 [0, 65535];

s7 -> s7 [0, 65535] { R331 += 1 };

s7 -> s5 [0, 65535];

s8 -> s6 [0, 65535] { R331 += 1, R293 += 1 };

s8 -> s7 [0, 65535] { R331 += 1 };

s8 -> s5 [0, 65535];

s8 -> s8 [0, 65535] { R331 += 1, R293 += 1, R263 += 1 };

accepting s3, s4, s8, s5, s2, s6, s1, s7, s0;

};

automaton uri_18 {

init s0;

s0 -> s1 [0, 82] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s0 -> s0 [0, 65535] { R332 += 1, R333 += 1 };

s0 -> s2 [0, 65535] { R333 += 1, R295 += 1, R264 += 1, R265 += 1 };

s0 -> s3 [0, 65535] { R333 += 1, R295 += 1, R265 += 1, R242 += 1, R243 += 1 };

s0 -> s4 [0, 65535] { R333 += 1, R294 += 1, R295 += 1 };

s0 -> s5 [84, 84] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s0 -> s1 [85, 65535] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s1 -> s1 [0, 82] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s1 -> s5 [84, 84] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s1 -> s1 [85, 65535] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s2 -> s1 [0, 82] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s2 -> s2 [0, 65535] { R333 += 1, R295 += 1, R264 += 1, R265 += 1 };

s2 -> s3 [0, 65535] { R333 += 1, R295 += 1, R265 += 1, R242 += 1, R243 += 1 };

s2 -> s5 [84, 84] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s2 -> s1 [85, 65535] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s3 -> s1 [0, 82] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s3 -> s3 [0, 65535] { R333 += 1, R295 += 1, R265 += 1, R242 += 1, R243 += 1 };

s3 -> s5 [84, 84] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s3 -> s1 [85, 65535] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s4 -> s1 [0, 82] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s4 -> s2 [0, 65535] { R333 += 1, R295 += 1, R264 += 1, R265 += 1 };

s4 -> s3 [0, 65535] { R333 += 1, R295 += 1, R265 += 1, R242 += 1, R243 += 1 };

s4 -> s4 [0, 65535] { R333 += 1, R294 += 1, R295 += 1 };

s4 -> s5 [84, 84] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s4 -> s1 [85, 65535] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s5 -> s5 [0, 82] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s5 -> s6 [0, 65535] { R333 += 1, R295 += 1 };

s5 -> s7 [0, 65535] { R333 += 1 };

s5 -> s8 [0, 65535];

s5 -> s5 [0, 65535] { R333 += 1, R295 += 1, R265 += 1 };

s5 -> s5 [84, 65535] { R333 += 1, R295 += 1, R265 += 1, R243 += 1 };

s6 -> s6 [0, 65535] { R333 += 1, R295 += 1 };

s6 -> s7 [0, 65535] { R333 += 1 };

s6 -> s8 [0, 65535];

s7 -> s7 [0, 65535] { R333 += 1 };

s7 -> s8 [0, 65535];

s8 -> s8 [0, 65535];

accepting s5, s6, s7, s8;

};

automaton uri_19 {

init s0;

s0 -> s1 [0, 65535] { R335 += 1, R296 += 1, R297 += 1 };

s0 -> s2 [0, 65535] { R335 += 1, R297 += 1, R267 += 1, R245 += 1, R227 += 1 };

s0 -> s0 [0, 65535] { R334 += 1, R335 += 1 };

s0 -> s3 [0, 65535] { R335 += 1, R297 += 1, R267 += 1, R244 += 1, R245 += 1 };

s0 -> s4 [0, 65535] { R335 += 1, R297 += 1, R266 += 1, R267 += 1 };

s1 -> s5 [0, 65535];

s1 -> s1 [0, 65535] { R335 += 1, R296 += 1, R297 += 1 };

s1 -> s2 [0, 65535] { R335 += 1, R297 += 1, R267 += 1, R245 += 1, R227 += 1 };

s1 -> s3 [0, 65535] { R335 += 1, R297 += 1, R267 += 1, R244 += 1, R245 += 1 };

s1 -> s4 [0, 65535] { R335 += 1, R297 += 1, R266 += 1, R267 += 1 };

s2 -> s8 [0, 65535] { R335 += 1, R297 += 1, R267 += 1 };

s2 -> s5 [0, 65535];

s2 -> s2 [0, 65535] { R335 += 1, R297 += 1, R267 += 1, R245 += 1, R227 += 1 };

s2 -> s6 [0, 65535] { R335 += 1 };

s2 -> s7 [0, 65535] { R335 += 1, R297 += 1 };

s3 -> s5 [0, 65535];

s3 -> s2 [0, 65535] { R335 += 1, R297 += 1, R267 += 1, R245 += 1, R227 += 1 };

s3 -> s6 [0, 65535] { R335 += 1 };

s3 -> s3 [0, 65535] { R335 += 1, R297 += 1, R267 += 1, R244 += 1, R245 += 1 };

s3 -> s7 [0, 65535] { R335 += 1, R297 += 1 };

s4 -> s5 [0, 65535];

s4 -> s2 [0, 65535] { R335 += 1, R297 += 1, R267 += 1, R245 += 1, R227 += 1 };

s4 -> s6 [0, 65535] { R335 += 1 };

s4 -> s3 [0, 65535] { R335 += 1, R297 += 1, R267 += 1, R244 += 1, R245 += 1 };

s4 -> s4 [0, 65535] { R335 += 1, R297 += 1, R266 += 1, R267 += 1 };

s5 -> s5 [0, 65535];

s6 -> s5 [0, 65535];

s6 -> s6 [0, 65535] { R335 += 1 };

s7 -> s5 [0, 65535];

s7 -> s6 [0, 65535] { R335 += 1 };

s7 -> s7 [0, 65535] { R335 += 1, R297 += 1 };

s8 -> s8 [0, 65535] { R335 += 1, R297 += 1, R267 += 1 };

s8 -> s5 [0, 65535];

s8 -> s6 [0, 65535] { R335 += 1 };

s8 -> s7 [0, 65535] { R335 += 1, R297 += 1 };

accepting s3, s4, s8, s5, s2, s6, s1, s7, s0;

};

automaton uri_20 {

init s0;

s0 -> s1 [0, 81] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s0 -> s2 [0, 65535] { R337 += 1, R299 += 1, R269 += 1, R246 += 1, R247 += 1 };

s0 -> s3 [0, 65535] { R337 += 1, R298 += 1, R299 += 1 };

s0 -> s0 [0, 65535] { R336 += 1, R337 += 1 };

s0 -> s4 [0, 65535] { R337 += 1, R299 += 1, R268 += 1, R269 += 1 };

s0 -> s5 [82, 82] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s0 -> s6 [82, 82] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s0 -> s1 [85, 65535] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s1 -> s1 [0, 81] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s1 -> s7 [0, 65535] { R337 += 1 };

s1 -> s1 [0, 65535] { R337 += 1, R299 += 1, R269 += 1 };

s1 -> s8 [0, 65535];

s1 -> s9 [0, 65535] { R337 += 1, R299 += 1 };

s1 -> s5 [82, 82] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s1 -> s6 [82, 82] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s1 -> s1 [85, 65535] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s2 -> s1 [0, 81] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s2 -> s7 [0, 65535] { R337 += 1 };

s2 -> s2 [0, 65535] { R337 += 1, R299 += 1, R269 += 1, R246 += 1, R247 += 1 };

s2 -> s8 [0, 65535];

s2 -> s9 [0, 65535] { R337 += 1, R299 += 1 };

s2 -> s5 [82, 82] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s2 -> s6 [82, 82] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s2 -> s1 [85, 65535] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s3 -> s1 [0, 81] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s3 -> s2 [0, 65535] { R337 += 1, R299 += 1, R269 += 1, R246 += 1, R247 += 1 };

s3 -> s3 [0, 65535] { R337 += 1, R298 += 1, R299 += 1 };

s3 -> s8 [0, 65535];

s3 -> s4 [0, 65535] { R337 += 1, R299 += 1, R268 += 1, R269 += 1 };

s3 -> s5 [82, 82] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s3 -> s6 [82, 82] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s3 -> s1 [85, 65535] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s4 -> s1 [0, 81] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s4 -> s7 [0, 65535] { R337 += 1 };

s4 -> s2 [0, 65535] { R337 += 1, R299 += 1, R269 += 1, R246 += 1, R247 += 1 };

s4 -> s8 [0, 65535];

s4 -> s4 [0, 65535] { R337 += 1, R299 += 1, R268 += 1, R269 += 1 };

s4 -> s5 [82, 82] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s4 -> s6 [82, 82] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s4 -> s1 [85, 65535] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s5 -> s5 [0, 82] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s5 -> s7 [0, 65535] { R337 += 1 };

s5 -> s5 [0, 65535] { R337 += 1, R299 += 1, R269 += 1 };

s5 -> s8 [0, 65535];

s5 -> s9 [0, 65535] { R337 += 1, R299 += 1 };

s5 -> s5 [85, 65535] { R337 += 1, R299 += 1, R269 += 1, R247 += 1 };

s6 -> s7 [0, 65535] { R337 += 1 };

s6 -> s6 [0, 65535] { R337 += 1, R299 += 1, R269 += 1 };

s6 -> s8 [0, 65535];

s6 -> s9 [0, 65535] { R337 += 1, R299 += 1 };

s7 -> s7 [0, 65535] { R337 += 1 };

s7 -> s8 [0, 65535];

s8 -> s8 [0, 65535];

s9 -> s7 [0, 65535] { R337 += 1 };

s9 -> s8 [0, 65535];

s9 -> s9 [0, 65535] { R337 += 1, R299 += 1 };

accepting s3, s4, s8, s5, s2, s9, s6, s1, s7, s0;

};

};

synchronised { // Automata constraining P56

automaton P56_0 {

init s0;

s0 -> s1 [114, 114];

accepting s1;

};

};

constraint R2 = R243 && R3 = R269 && R4 = R237 && R5 = R337 && R12 = 0 && R13 = R299 && R228 = 0 && R229 = 1 && R230 = 0 && R231 = 1 && R232 = 0 && R233 = 14 && R234 = 0 && R235 = 14 && R236 - R299 = 1 && R238 = 0 && R239 = R243 && R240 = 0 && R241 = R243 && R242 = 0 && R248 = 15 && R249 = R269 && R250 = 15 && R251 = R269 && R252 = 15 && R253 = R269 && R254 = 15 && R255 = R269 && R256 = 15 && R257 = R269 && R258 = 15 && R259 = R269 && R260 = 15 && R261 = R269 && R262 = 15 && R263 = R269 && R264 = 15 && R265 = R269 && R266 = 15 && R267 = R269 && R268 = 15 && R270 = 0 && R271 = R299 && R272 = 0 && R273 = R299 && R274 = 0 && R275 = R299 && R276 = 0 && R277 = R299 && R278 = 0 && R279 = R299 && R280 = 0 && R281 = R299 && R282 = 0 && R283 = R299 && R284 = 0 && R285 = R299 && R286 = 0 && R287 = R299 && R288 = 0 && R289 = R299 && R290 = 0 && R291 = R299 && R292 = 0 && R293 = R299 && R294 = 0 && R295 = R299 && R296 = 0 && R297 = R299 && R298 = 0 && R300 = 10 && R301 = R337 && R302 = 10 && R303 = R337 && R304 = 10 && R305 = R337 && R306 = 10 && R307 = R337 && R308 = 10 && R309 = R337 && R310 = 10 && R311 = R337 && R312 = 10 && R313 = R337 && R314 = 10 && R315 = R337 && R316 = 10 && R317 = R337 && R318 = 10 && R319 = R337 && R320 = 10 && R321 = R337 && R322 = 10 && R323 = R337 && R324 = 10 && R325 = R337 && R326 = 10 && R327 = R337 && R328 = 10 && R329 = R337 && R330 = 10 && R331 = R337 && R332 = 10 && R333 = R337 && R334 = 10 && R335 = R337 && R336 = 10 && R0 != 0 && R1 != 0 && R7 < 1 && R8 < 1 && R299 < R237 && 0 < R243 && 14 < R269 && -1 < R299 && 9 < R337 && (R227 = 0 || (R244 = 0 && R245 = 0)) && (R227 = 0 || (R246 = 0 && R247 = 0));

// End of Parikh automata intersection problem