// Parikh automata intersection problem, generated by OSTRICH+

counter int R0, R1, R10, R2, R209, R210, R3, 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, R338, R339, R340, R341, R342, R343, R344, R345, R346, R347, R348, R349, R350, R351, R352, R353, R354, R355, R356, R357, R358, R359, R360, R361, R362, R363, R364, R365, R366, R367, R368, R369, R370, R371, R372, R373, R374, R375, R376, R377, R378, R379, R380, R381, R382, R383, R384, R385, R386, R387, R388, R389, R390, R391, R392, R393, R394, R395, R396, R397, R398, R399, R4, R400, R401, R402, R403, R404, R5, R6, R7, R9;

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] { R6 += 1 };

accepting s0;

};

automaton uri_2 {

init s0;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

s3 -> s3 [0, 65535];

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

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

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

s4 -> s4 [0, 65535];

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

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

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

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

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

s5 -> s5 [0, 65535];

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

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

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

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

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

s6 -> s6 [0, 65535];

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

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

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

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

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

s7 -> s7 [0, 65535];

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

accepting s3, s4, s5, s6, s7;

};

automaton uri_3 {

init s0;

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

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

s1 -> s2 [0, 65535];

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

s2 -> s2 [0, 65535];

accepting s0, s1, s2;

};

automaton uri_4 {

init s0;

s0 -> s1 [0, 46] { R376 += 1, R210 += 1 };

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

s0 -> s2 [0, 65535] { R376 += 1, R209 += 1, R210 += 1 };

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

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

s1 -> s1 [0, 46] { R376 += 1, R210 += 1 };

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

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

s2 -> s1 [0, 46] { R376 += 1, R210 += 1 };

s2 -> s2 [0, 65535] { R376 += 1, R209 += 1, R210 += 1 };

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

s2 -> s1 [48, 65535] { R376 += 1, R210 += 1 };

s3 -> s4 [0, 65535];

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

s4 -> s4 [0, 65535];

accepting s3, s4;

};

automaton uri_5 {

init s0;

s0 -> s1 [0, 65535] { R378 += 1, R325 += 1, R326 += 1 };

s0 -> s2 [0, 65535] { R378 += 1, R326 += 1, R2 += 1 };

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

s1 -> s4 [0, 65535];

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

s1 -> s2 [0, 65535] { R378 += 1, R326 += 1, R2 += 1 };

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

s2 -> s4 [0, 65535];

s2 -> s2 [0, 65535] { R378 += 1, R326 += 1, R2 += 1 };

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

s3 -> s4 [0, 65535];

s4 -> s4 [0, 65535];

accepting s3, s4, s2, s1, s0;

};

automaton uri_6 {

init s0;

s0 -> s1 [0, 63] { R380 += 1, R346 += 1 };

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

s0 -> s2 [0, 65535] { R380 += 1, R345 += 1, R346 += 1 };

s0 -> s3 [64, 64] { R380 += 1, R346 += 1 };

s0 -> s1 [65, 65535] { R380 += 1, R346 += 1 };

s1 -> s1 [0, 63] { R380 += 1, R346 += 1 };

s1 -> s3 [64, 64] { R380 += 1, R346 += 1 };

s1 -> s1 [65, 65535] { R380 += 1, R346 += 1 };

s2 -> s1 [0, 63] { R380 += 1, R346 += 1 };

s2 -> s2 [0, 65535] { R380 += 1, R345 += 1, R346 += 1 };

s2 -> s3 [64, 64] { R380 += 1, R346 += 1 };

s2 -> s1 [65, 65535] { R380 += 1, R346 += 1 };

s3 -> s4 [0, 65535];

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

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

s4 -> s4 [0, 65535];

s5 -> s4 [0, 65535];

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

accepting s3, s4, s5;

};

automaton uri_7 {

init s0;

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

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

s0 -> s2 [0, 65535] { R382 += 1, R347 += 1, R348 += 1 };

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

s1 -> s3 [0, 65535];

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

s2 -> s1 [0, 65535] { R382 += 1, R348 += 1, R4 += 1 };

s2 -> s3 [0, 65535];

s2 -> s2 [0, 65535] { R382 += 1, R347 += 1, R348 += 1 };

s3 -> s3 [0, 65535];

s4 -> s3 [0, 65535];

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

accepting s3, s4, s2, s1, s0;

};

automaton uri_8 {

init s0;

s0 -> s1 [0, 36] { R384 += 1, R350 += 1, R322 += 1 };

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

s0 -> s2 [0, 65535] { R384 += 1, R350 += 1, R321 += 1, R322 += 1 };

s0 -> s3 [0, 65535] { R384 += 1, R349 += 1, R350 += 1 };

s0 -> s1 [38, 42] { R384 += 1, R350 += 1, R322 += 1 };

s0 -> s1 [44, 57] { R384 += 1, R350 += 1, R322 += 1 };

s0 -> s1 [59, 63] { R384 += 1, R350 += 1, R322 += 1 };

s0 -> s1 [65, 65535] { R384 += 1, R350 += 1, R322 += 1 };

s1 -> s1 [0, 36] { R384 += 1, R350 += 1, R322 += 1 };

s1 -> s1 [0, 65535] { R384 += 1, R350 += 1 };

s1 -> s4 [0, 65535];

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

s1 -> s1 [38, 42] { R384 += 1, R350 += 1, R322 += 1 };

s1 -> s1 [44, 57] { R384 += 1, R350 += 1, R322 += 1 };

s1 -> s1 [59, 63] { R384 += 1, R350 += 1, R322 += 1 };

s1 -> s1 [65, 65535] { R384 += 1, R350 += 1, R322 += 1 };

s2 -> s1 [0, 36] { R384 += 1, R350 += 1, R322 += 1 };

s2 -> s4 [0, 65535];

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

s2 -> s2 [0, 65535] { R384 += 1, R350 += 1, R321 += 1, R322 += 1 };

s2 -> s1 [38, 42] { R384 += 1, R350 += 1, R322 += 1 };

s2 -> s1 [44, 57] { R384 += 1, R350 += 1, R322 += 1 };

s2 -> s1 [59, 63] { R384 += 1, R350 += 1, R322 += 1 };

s2 -> s1 [65, 65535] { R384 += 1, R350 += 1, R322 += 1 };

s3 -> s1 [0, 36] { R384 += 1, R350 += 1, R322 += 1 };

s3 -> s4 [0, 65535];

s3 -> s2 [0, 65535] { R384 += 1, R350 += 1, R321 += 1, R322 += 1 };

s3 -> s3 [0, 65535] { R384 += 1, R349 += 1, R350 += 1 };

s3 -> s1 [38, 42] { R384 += 1, R350 += 1, R322 += 1 };

s3 -> s1 [44, 57] { R384 += 1, R350 += 1, R322 += 1 };

s3 -> s1 [59, 63] { R384 += 1, R350 += 1, R322 += 1 };

s3 -> s1 [65, 65535] { R384 += 1, R350 += 1, R322 += 1 };

s4 -> s4 [0, 65535];

s5 -> s4 [0, 65535];

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

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

};

automaton uri_9 {

init s0;

s0 -> s1 [0, 65535] { R386 += 1, R352 += 1, R324 += 1, R1 += 1 };

s0 -> s2 [0, 65535] { R386 += 1, R351 += 1, R352 += 1 };

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

s0 -> s3 [0, 65535] { R386 += 1, R352 += 1, R323 += 1, R324 += 1 };

s1 -> s1 [0, 65535] { R386 += 1, R352 += 1, R324 += 1, R1 += 1 };

s1 -> s4 [0, 65535];

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

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

s2 -> s1 [0, 65535] { R386 += 1, R352 += 1, R324 += 1, R1 += 1 };

s2 -> s2 [0, 65535] { R386 += 1, R351 += 1, R352 += 1 };

s2 -> s4 [0, 65535];

s2 -> s3 [0, 65535] { R386 += 1, R352 += 1, R323 += 1, R324 += 1 };

s3 -> s1 [0, 65535] { R386 += 1, R352 += 1, R324 += 1, R1 += 1 };

s3 -> s4 [0, 65535];

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

s3 -> s3 [0, 65535] { R386 += 1, R352 += 1, R323 += 1, R324 += 1 };

s4 -> s4 [0, 65535];

s5 -> s4 [0, 65535];

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

s6 -> s4 [0, 65535];

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

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

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

};

automaton uri_10 {

init s0;

s0 -> s1 [0, 43] { R388 += 1, R354 += 1, R328 += 1 };

s0 -> s2 [0, 65535] { R388 += 1, R353 += 1, R354 += 1 };

s0 -> s3 [0, 65535] { R388 += 1, R354 += 1, R327 += 1, R328 += 1 };

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

s0 -> s1 [45, 57] { R388 += 1, R354 += 1, R328 += 1 };

s0 -> s4 [58, 58] { R388 += 1, R354 += 1, R328 += 1 };

s0 -> s1 [59, 65535] { R388 += 1, R354 += 1, R328 += 1 };

s1 -> s1 [0, 43] { R388 += 1, R354 += 1, R328 += 1 };

s1 -> s1 [45, 57] { R388 += 1, R354 += 1, R328 += 1 };

s1 -> s4 [58, 58] { R388 += 1, R354 += 1, R328 += 1 };

s1 -> s1 [59, 65535] { R388 += 1, R354 += 1, R328 += 1 };

s2 -> s1 [0, 43] { R388 += 1, R354 += 1, R328 += 1 };

s2 -> s2 [0, 65535] { R388 += 1, R353 += 1, R354 += 1 };

s2 -> s3 [0, 65535] { R388 += 1, R354 += 1, R327 += 1, R328 += 1 };

s2 -> s1 [45, 57] { R388 += 1, R354 += 1, R328 += 1 };

s2 -> s4 [58, 58] { R388 += 1, R354 += 1, R328 += 1 };

s2 -> s1 [59, 65535] { R388 += 1, R354 += 1, R328 += 1 };

s3 -> s1 [0, 43] { R388 += 1, R354 += 1, R328 += 1 };

s3 -> s3 [0, 65535] { R388 += 1, R354 += 1, R327 += 1, R328 += 1 };

s3 -> s1 [45, 57] { R388 += 1, R354 += 1, R328 += 1 };

s3 -> s4 [58, 58] { R388 += 1, R354 += 1, R328 += 1 };

s3 -> s1 [59, 65535] { R388 += 1, R354 += 1, R328 += 1 };

s4 -> s4 [0, 43] { R388 += 1, R354 += 1, R328 += 1 };

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

s4 -> s6 [0, 65535];

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

s4 -> s4 [45, 65535] { R388 += 1, R354 += 1, R328 += 1 };

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

s5 -> s6 [0, 65535];

s6 -> s6 [0, 65535];

accepting s4, s5, s6;

};

automaton uri_11 {

init s0;

s0 -> s1 [0, 65535] { R390 += 1, R356 += 1, R329 += 1, R330 += 1 };

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

s0 -> s2 [0, 65535] { R390 += 1, R356 += 1, R330 += 1, R3 += 1 };

s0 -> s3 [0, 65535] { R390 += 1, R355 += 1, R356 += 1 };

s1 -> s4 [0, 65535];

s1 -> s1 [0, 65535] { R390 += 1, R356 += 1, R329 += 1, R330 += 1 };

s1 -> s2 [0, 65535] { R390 += 1, R356 += 1, R330 += 1, R3 += 1 };

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

s2 -> s4 [0, 65535];

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

s2 -> s2 [0, 65535] { R390 += 1, R356 += 1, R330 += 1, R3 += 1 };

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

s3 -> s4 [0, 65535];

s3 -> s1 [0, 65535] { R390 += 1, R356 += 1, R329 += 1, R330 += 1 };

s3 -> s2 [0, 65535] { R390 += 1, R356 += 1, R330 += 1, R3 += 1 };

s3 -> s3 [0, 65535] { R390 += 1, R355 += 1, R356 += 1 };

s4 -> s4 [0, 65535];

s5 -> s4 [0, 65535];

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

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

s6 -> s4 [0, 65535];

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

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

};

automaton uri_12 {

init s0;

s0 -> s1 [0, 57] { R392 += 1, R358 += 1, R332 += 1, R10 += 1 };

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

s0 -> s2 [0, 65535] { R392 += 1, R357 += 1, R358 += 1 };

s0 -> s3 [0, 65535] { R392 += 1, R358 += 1, R331 += 1, R332 += 1 };

s0 -> s4 [0, 65535] { R392 += 1, R358 += 1, R332 += 1, R9 += 1, R10 += 1 };

s0 -> s5 [58, 58] { R392 += 1, R358 += 1, R332 += 1 };

s0 -> s1 [59, 65535] { R392 += 1, R358 += 1, R332 += 1, R10 += 1 };

s1 -> s1 [0, 57] { R392 += 1, R358 += 1, R332 += 1, R10 += 1 };

s1 -> s5 [58, 58] { R392 += 1, R358 += 1, R332 += 1 };

s1 -> s1 [59, 65535] { R392 += 1, R358 += 1, R332 += 1, R10 += 1 };

s2 -> s1 [0, 57] { R392 += 1, R358 += 1, R332 += 1, R10 += 1 };

s2 -> s2 [0, 65535] { R392 += 1, R357 += 1, R358 += 1 };

s2 -> s3 [0, 65535] { R392 += 1, R358 += 1, R331 += 1, R332 += 1 };

s2 -> s4 [0, 65535] { R392 += 1, R358 += 1, R332 += 1, R9 += 1, R10 += 1 };

s2 -> s5 [58, 58] { R392 += 1, R358 += 1, R332 += 1 };

s2 -> s1 [59, 65535] { R392 += 1, R358 += 1, R332 += 1, R10 += 1 };

s3 -> s1 [0, 57] { R392 += 1, R358 += 1, R332 += 1, R10 += 1 };

s3 -> s3 [0, 65535] { R392 += 1, R358 += 1, R331 += 1, R332 += 1 };

s3 -> s4 [0, 65535] { R392 += 1, R358 += 1, R332 += 1, R9 += 1, R10 += 1 };

s3 -> s5 [58, 58] { R392 += 1, R358 += 1, R332 += 1 };

s3 -> s1 [59, 65535] { R392 += 1, R358 += 1, R332 += 1, R10 += 1 };

s4 -> s1 [0, 57] { R392 += 1, R358 += 1, R332 += 1, R10 += 1 };

s4 -> s4 [0, 65535] { R392 += 1, R358 += 1, R332 += 1, R9 += 1, R10 += 1 };

s4 -> s5 [58, 58] { R392 += 1, R358 += 1, R332 += 1 };

s4 -> s1 [59, 65535] { R392 += 1, R358 += 1, R332 += 1, R10 += 1 };

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

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

s5 -> s8 [0, 65535];

s5 -> s5 [0, 65535] { R392 += 1, R358 += 1, R332 += 1 };

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

s6 -> s8 [0, 65535];

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

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

s7 -> s8 [0, 65535];

s8 -> s8 [0, 65535];

accepting s5, s6, s7, s8;

};

automaton uri_13 {

init s0;

s0 -> s1 [0, 90] { R394 += 1, R360 += 1, R334 += 1, R310 += 1 };

s0 -> s2 [0, 65535] { R394 += 1, R360 += 1, R333 += 1, R334 += 1 };

s0 -> s3 [0, 65535] { R394 += 1, R359 += 1, R360 += 1 };

s0 -> s4 [0, 65535] { R394 += 1, R360 += 1, R334 += 1, R309 += 1, R310 += 1 };

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

s0 -> s5 [91, 91] { R394 += 1, R360 += 1, R334 += 1, R310 += 1 };

s0 -> s1 [92, 65535] { R394 += 1, R360 += 1, R334 += 1, R310 += 1 };

s1 -> s6 [0, 65535];

s1 -> s9 [0, 65535] { R394 += 1, R360 += 1, R334 += 1 };

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

s1 -> s1 [0, 65535] { R394 += 1, R360 += 1, R334 += 1, R310 += 1 };

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

s2 -> s1 [0, 90] { R394 += 1, R360 += 1, R334 += 1, R310 += 1 };

s2 -> s2 [0, 65535] { R394 += 1, R360 += 1, R333 += 1, R334 += 1 };

s2 -> s6 [0, 65535];

s2 -> s4 [0, 65535] { R394 += 1, R360 += 1, R334 += 1, R309 += 1, R310 += 1 };

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

s2 -> s5 [91, 91] { R394 += 1, R360 += 1, R334 += 1, R310 += 1 };

s2 -> s1 [92, 65535] { R394 += 1, R360 += 1, R334 += 1, R310 += 1 };

s3 -> s1 [0, 90] { R394 += 1, R360 += 1, R334 += 1, R310 += 1 };

s3 -> s2 [0, 65535] { R394 += 1, R360 += 1, R333 += 1, R334 += 1 };

s3 -> s6 [0, 65535];

s3 -> s3 [0, 65535] { R394 += 1, R359 += 1, R360 += 1 };

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

s3 -> s5 [91, 91] { R394 += 1, R360 += 1, R334 += 1, R310 += 1 };

s3 -> s1 [92, 65535] { R394 += 1, R360 += 1, R334 += 1, R310 += 1 };

s4 -> s1 [0, 90] { R394 += 1, R360 += 1, R334 += 1, R310 += 1 };

s4 -> s6 [0, 65535];

s4 -> s4 [0, 65535] { R394 += 1, R360 += 1, R334 += 1, R309 += 1, R310 += 1 };

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

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

s4 -> s5 [91, 91] { R394 += 1, R360 += 1, R334 += 1, R310 += 1 };

s4 -> s1 [92, 65535] { R394 += 1, R360 += 1, R334 += 1, R310 += 1 };

s5 -> s1 [0, 65535] { R394 += 1, R360 += 1, R334 += 1, R310 += 1 };

s6 -> s6 [0, 65535];

s7 -> s6 [0, 65535];

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

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

s8 -> s6 [0, 65535];

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

s9 -> s6 [0, 65535];

s9 -> s9 [0, 65535] { R394 += 1, R360 += 1, R334 += 1 };

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

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

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

};

automaton uri_14 {

init s0;

s0 -> s1 [0, 65535] { R396 += 1, R362 += 1, R336 += 1, R311 += 1, R312 += 1 };

s0 -> s2 [0, 65535] { R396 += 1, R361 += 1, R362 += 1 };

s0 -> s3 [0, 65535] { R396 += 1, R362 += 1, R336 += 1, R312 += 1, R7 += 1 };

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

s0 -> s4 [0, 65535] { R396 += 1, R362 += 1, R335 += 1, R336 += 1 };

s1 -> s1 [0, 65535] { R396 += 1, R362 += 1, R336 += 1, R311 += 1, R312 += 1 };

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

s1 -> s3 [0, 65535] { R396 += 1, R362 += 1, R336 += 1, R312 += 1, R7 += 1 };

s1 -> s6 [0, 65535];

s1 -> s8 [0, 65535] { R396 += 1, R362 += 1 };

s2 -> s1 [0, 65535] { R396 += 1, R362 += 1, R336 += 1, R311 += 1, R312 += 1 };

s2 -> s2 [0, 65535] { R396 += 1, R361 += 1, R362 += 1 };

s2 -> s3 [0, 65535] { R396 += 1, R362 += 1, R336 += 1, R312 += 1, R7 += 1 };

s2 -> s6 [0, 65535];

s2 -> s4 [0, 65535] { R396 += 1, R362 += 1, R335 += 1, R336 += 1 };

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

s3 -> s3 [0, 65535] { R396 += 1, R362 += 1, R336 += 1, R312 += 1, R7 += 1 };

s3 -> s6 [0, 65535];

s3 -> s7 [0, 65535] { R396 += 1, R362 += 1, R336 += 1 };

s3 -> s8 [0, 65535] { R396 += 1, R362 += 1 };

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

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

s4 -> s3 [0, 65535] { R396 += 1, R362 += 1, R336 += 1, R312 += 1, R7 += 1 };

s4 -> s6 [0, 65535];

s4 -> s4 [0, 65535] { R396 += 1, R362 += 1, R335 += 1, R336 += 1 };

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

s5 -> s6 [0, 65535];

s6 -> s6 [0, 65535];

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

s7 -> s6 [0, 65535];

s7 -> s7 [0, 65535] { R396 += 1, R362 += 1, R336 += 1 };

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

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

s8 -> s6 [0, 65535];

s8 -> s8 [0, 65535] { R396 += 1, R362 += 1 };

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

};

automaton uri_15 {

init s0;

s0 -> s1 [0, 57] { R398 += 1, R364 += 1, R338 += 1, R314 += 1 };

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

s0 -> s2 [0, 65535] { R398 += 1, R364 += 1, R338 += 1, R313 += 1, R314 += 1 };

s0 -> s3 [0, 65535] { R398 += 1, R364 += 1, R337 += 1, R338 += 1 };

s0 -> s4 [0, 65535] { R398 += 1, R363 += 1, R364 += 1 };

s0 -> s1 [59, 65535] { R398 += 1, R364 += 1, R338 += 1, R314 += 1 };

s1 -> s1 [0, 57] { R398 += 1, R364 += 1, R338 += 1, R314 += 1 };

s1 -> s1 [0, 65535] { R398 += 1, R364 += 1, R338 += 1 };

s1 -> s5 [0, 65535];

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

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

s1 -> s1 [59, 65535] { R398 += 1, R364 += 1, R338 += 1, R314 += 1 };

s2 -> s1 [0, 57] { R398 += 1, R364 += 1, R338 += 1, R314 += 1 };

s2 -> s5 [0, 65535];

s2 -> s2 [0, 65535] { R398 += 1, R364 += 1, R338 += 1, R313 += 1, R314 += 1 };

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

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

s2 -> s1 [59, 65535] { R398 += 1, R364 += 1, R338 += 1, R314 += 1 };

s3 -> s1 [0, 57] { R398 += 1, R364 += 1, R338 += 1, R314 += 1 };

s3 -> s5 [0, 65535];

s3 -> s2 [0, 65535] { R398 += 1, R364 += 1, R338 += 1, R313 += 1, R314 += 1 };

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

s3 -> s3 [0, 65535] { R398 += 1, R364 += 1, R337 += 1, R338 += 1 };

s3 -> s1 [59, 65535] { R398 += 1, R364 += 1, R338 += 1, R314 += 1 };

s4 -> s1 [0, 57] { R398 += 1, R364 += 1, R338 += 1, R314 += 1 };

s4 -> s5 [0, 65535];

s4 -> s2 [0, 65535] { R398 += 1, R364 += 1, R338 += 1, R313 += 1, R314 += 1 };

s4 -> s3 [0, 65535] { R398 += 1, R364 += 1, R337 += 1, R338 += 1 };

s4 -> s4 [0, 65535] { R398 += 1, R363 += 1, R364 += 1 };

s4 -> s1 [59, 65535] { R398 += 1, R364 += 1, R338 += 1, R314 += 1 };

s5 -> s5 [0, 65535];

s6 -> s5 [0, 65535];

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

s7 -> s5 [0, 65535];

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

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

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

};

automaton uri_16 {

init s0;

s0 -> s1 [0, 65535] { R400 += 1, R366 += 1, R340 += 1, R315 += 1, R316 += 1 };

s0 -> s2 [0, 65535] { R400 += 1, R366 += 1, R339 += 1, R340 += 1 };

s0 -> s3 [0, 65535] { R400 += 1, R365 += 1, R366 += 1 };

s0 -> s4 [0, 65535] { R400 += 1, R366 += 1, R340 += 1, R316 += 1, R0 += 1 };

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

s1 -> s1 [0, 65535] { R400 += 1, R366 += 1, R340 += 1, R315 += 1, R316 += 1 };

s1 -> s6 [0, 65535];

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

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

s1 -> s4 [0, 65535] { R400 += 1, R366 += 1, R340 += 1, R316 += 1, R0 += 1 };

s2 -> s1 [0, 65535] { R400 += 1, R366 += 1, R340 += 1, R315 += 1, R316 += 1 };

s2 -> s2 [0, 65535] { R400 += 1, R366 += 1, R339 += 1, R340 += 1 };

s2 -> s6 [0, 65535];

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

s2 -> s4 [0, 65535] { R400 += 1, R366 += 1, R340 += 1, R316 += 1, R0 += 1 };

s3 -> s1 [0, 65535] { R400 += 1, R366 += 1, R340 += 1, R315 += 1, R316 += 1 };

s3 -> s2 [0, 65535] { R400 += 1, R366 += 1, R339 += 1, R340 += 1 };

s3 -> s6 [0, 65535];

s3 -> s3 [0, 65535] { R400 += 1, R365 += 1, R366 += 1 };

s3 -> s4 [0, 65535] { R400 += 1, R366 += 1, R340 += 1, R316 += 1, R0 += 1 };

s4 -> s5 [0, 65535] { R400 += 1, R366 += 1, R340 += 1 };

s4 -> s6 [0, 65535];

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

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

s4 -> s4 [0, 65535] { R400 += 1, R366 += 1, R340 += 1, R316 += 1, R0 += 1 };

s5 -> s5 [0, 65535] { R400 += 1, R366 += 1, R340 += 1 };

s5 -> s6 [0, 65535];

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

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

s6 -> s6 [0, 65535];

s7 -> s6 [0, 65535];

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

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

s8 -> s6 [0, 65535];

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

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

};

automaton uri_17 {

init s0;

s0 -> s1 [0, 64] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

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

s0 -> s2 [0, 65535] { R402 += 1, R367 += 1, R368 += 1 };

s0 -> s3 [0, 65535] { R402 += 1, R368 += 1, R342 += 1, R317 += 1, R318 += 1 };

s0 -> s4 [0, 65535] { R402 += 1, R368 += 1, R341 += 1, R342 += 1 };

s0 -> s5 [88, 88] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s0 -> s1 [89, 65535] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s1 -> s1 [0, 64] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s1 -> s5 [88, 88] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s1 -> s1 [89, 65535] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s2 -> s1 [0, 64] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s2 -> s2 [0, 65535] { R402 += 1, R367 += 1, R368 += 1 };

s2 -> s3 [0, 65535] { R402 += 1, R368 += 1, R342 += 1, R317 += 1, R318 += 1 };

s2 -> s4 [0, 65535] { R402 += 1, R368 += 1, R341 += 1, R342 += 1 };

s2 -> s5 [88, 88] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s2 -> s1 [89, 65535] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s3 -> s1 [0, 64] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s3 -> s3 [0, 65535] { R402 += 1, R368 += 1, R342 += 1, R317 += 1, R318 += 1 };

s3 -> s5 [88, 88] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s3 -> s1 [89, 65535] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s4 -> s1 [0, 64] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s4 -> s3 [0, 65535] { R402 += 1, R368 += 1, R342 += 1, R317 += 1, R318 += 1 };

s4 -> s4 [0, 65535] { R402 += 1, R368 += 1, R341 += 1, R342 += 1 };

s4 -> s5 [88, 88] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s4 -> s1 [89, 65535] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s5 -> s5 [0, 64] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s5 -> s5 [0, 65535] { R402 += 1, R368 += 1, R342 += 1 };

s5 -> s6 [0, 65535];

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

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

s5 -> s5 [88, 65535] { R402 += 1, R368 += 1, R342 += 1, R318 += 1 };

s6 -> s6 [0, 65535];

s7 -> s6 [0, 65535];

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

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

s8 -> s6 [0, 65535];

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

accepting s5, s6, s7, s8;

};

automaton uri_18 {

init s0;

s0 -> s1 [0, 65535] { R404 += 1, R370 += 1, R344 += 1, R319 += 1, R320 += 1 };

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

s0 -> s2 [0, 65535] { R404 += 1, R370 += 1, R344 += 1, R320 += 1, R308 += 1 };

s0 -> s3 [0, 65535] { R404 += 1, R370 += 1, R343 += 1, R344 += 1 };

s0 -> s4 [0, 65535] { R404 += 1, R369 += 1, R370 += 1 };

s1 -> s1 [0, 65535] { R404 += 1, R370 += 1, R344 += 1, R319 += 1, R320 += 1 };

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

s1 -> s2 [0, 65535] { R404 += 1, R370 += 1, R344 += 1, R320 += 1, R308 += 1 };

s1 -> s5 [0, 65535];

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

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

s2 -> s2 [0, 65535] { R404 += 1, R370 += 1, R344 += 1, R320 += 1, R308 += 1 };

s2 -> s5 [0, 65535];

s2 -> s8 [0, 65535] { R404 += 1, R370 += 1, R344 += 1 };

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

s3 -> s1 [0, 65535] { R404 += 1, R370 += 1, R344 += 1, R319 += 1, R320 += 1 };

s3 -> s2 [0, 65535] { R404 += 1, R370 += 1, R344 += 1, R320 += 1, R308 += 1 };

s3 -> s5 [0, 65535];

s3 -> s3 [0, 65535] { R404 += 1, R370 += 1, R343 += 1, R344 += 1 };

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

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

s4 -> s2 [0, 65535] { R404 += 1, R370 += 1, R344 += 1, R320 += 1, R308 += 1 };

s4 -> s5 [0, 65535];

s4 -> s3 [0, 65535] { R404 += 1, R370 += 1, R343 += 1, R344 += 1 };

s4 -> s4 [0, 65535] { R404 += 1, R369 += 1, R370 += 1 };

s5 -> s5 [0, 65535];

s6 -> s5 [0, 65535];

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

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

s7 -> s5 [0, 65535];

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

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

s8 -> s5 [0, 65535];

s8 -> s8 [0, 65535] { R404 += 1, R370 += 1, R344 += 1 };

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

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

};

};

constraint R3 = R316 && R4 = R344 && R5 = R326 && R6 = R404 && R9 = 0 && R10 = R318 && R209 = 0 && R210 = R370 && R309 = 0 && R310 = 1 && R311 = 0 && R312 = 1 && R313 - R318 = 1 && R314 = R316 && R315 - R318 = 1 && R317 = 0 && R321 = 0 && R322 = 4 && R323 = 0 && R324 = 4 && R325 - R370 = 1 && R327 = 5 && R328 = R344 && R329 = 5 && R330 = R344 && R331 = 5 && R332 = R344 && R333 = 5 && R334 = R344 && R335 = 5 && R336 = R344 && R337 = 5 && R338 = R344 && R339 = 5 && R340 = R344 && R341 = 5 && R342 = R344 && R343 = 5 && R345 = 0 && R346 = R370 && R347 = 0 && R348 = R370 && R349 = 0 && R350 = R370 && R351 = 0 && R352 = R370 && R353 = 0 && R354 = R370 && R355 = 0 && R356 = R370 && R357 = 0 && R358 = R370 && R359 = 0 && R360 = R370 && R361 = 0 && R362 = R370 && R363 = 0 && R364 = R370 && R365 = 0 && R366 = R370 && R367 = 0 && R368 = R370 && R369 = 0 && R371 = 10 && R372 = R404 && R373 = 10 && R374 = R404 && R375 = 10 && R376 = R404 && R377 = 10 && R378 = R404 && R379 = 10 && R380 = R404 && R381 = 10 && R382 = R404 && R383 = 10 && R384 = R404 && R385 = 10 && R386 = R404 && R387 = 10 && R388 = R404 && R389 = 10 && R390 = R404 && R391 = 10 && R392 = R404 && R393 = 10 && R394 = R404 && R395 = 10 && R396 = R404 && R397 = 10 && R398 = R404 && R399 = 10 && R400 = R404 && R401 = 10 && R402 = R404 && R403 = 10 && R0 != 0 && R1 != 0 && R2 != 0 && R318 < R316 && -1 < R318 && R370 < R326 && 4 < R344 && -1 < R370 && 9 < R404 && (R319 != 0 || R318 = R320 || (R308 = 0 && R318 = 0)) && (R319 = 0 || (R308 = 0 && R318 = 0));

// End of Parikh automata intersection problem