// Parikh automata intersection problem, generated by OSTRICH+

counter int R0, R1, R10, R100, R101, R102, R103, R104, R105, R106, R107, R108, R109, R110, R111, R112, R113, R114, R115, R116, R117, R118, R119, R120, R121, R122, R123, R124, R125, R126, R127, R128, R129, R130, R131, R132, R133, R134, R135, R136, R137, R138, R139, R14, R15, R2, R3, R4, R5, R6, R7, R78, R79, R8, R80, R81, R82, R83, R84, R85, R86, R87, R88, R89, R9, R90, R91, R92, R93, R94, R95, R96, R97, R98, R99;

synchronised { // Automata constraining P25

automaton P25_0 {

init s0;

s0 -> s1 [9, 9];

accepting s1;

};

};

synchronised { // Automata constraining value1

automaton value1_0 {

init s0;

s0 -> s0 [0, 43];

s0 -> s0 [45, 60];

s0 -> s1 [61, 61];

s0 -> s0 [62, 65535];

s1 -> s1 [0, 43];

s1 -> s1 [45, 65535];

accepting s1;

};

automaton value1_1 {

init s0;

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

accepting s0;

};

automaton value1_2 {

init s0;

s0 -> s1 [0, 60] { R15 += 1 };

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

s0 -> s2 [61, 61];

s0 -> s1 [62, 65535] { R15 += 1 };

s1 -> s1 [0, 60] { R15 += 1 };

s1 -> s2 [61, 61];

s1 -> s1 [62, 65535] { R15 += 1 };

s2 -> s2 [0, 65535];

accepting s2;

};

automaton value1_3 {

init s0;

s0 -> s1 [0, 65535] { R107 += 1, R0 += 1 };

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

s1 -> s1 [0, 65535] { R107 += 1, R0 += 1 };

s1 -> s2 [0, 65535];

s2 -> s2 [0, 65535];

accepting s0, s1, s2;

};

automaton value1_4 {

init s0;

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

s0 -> s1 [0, 65535] { R109 += 1, R80 += 1, R81 += 1 };

s0 -> s2 [11, 11] { R109 += 1, R81 += 1 };

s1 -> s1 [0, 65535] { R109 += 1, R80 += 1, R81 += 1 };

s1 -> s2 [11, 11] { R109 += 1, R81 += 1 };

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

s2 -> s3 [0, 65535];

s3 -> s3 [0, 65535];

accepting s2, s3;

};

automaton value1_5 {

init s0;

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

s0 -> s2 [0, 65535] { R111 += 1, R82 += 1, R83 += 1 };

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

s1 -> s3 [0, 65535];

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

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

s2 -> s3 [0, 65535];

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

s2 -> s2 [0, 65535] { R111 += 1, R82 += 1, R83 += 1 };

s3 -> s3 [0, 65535];

s4 -> s3 [0, 65535];

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

accepting s3, s4, s2, s1, s0;

};

automaton value1_6 {

init s0;

s0 -> s1 [0, 64] { R117 += 1 };

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

s0 -> s2 [69, 69] { R117 += 1 };

s0 -> s1 [70, 65535] { R117 += 1 };

s1 -> s1 [0, 64] { R117 += 1 };

s1 -> s2 [69, 69] { R117 += 1 };

s1 -> s1 [70, 65535] { R117 += 1 };

s2 -> s2 [0, 64] { R117 += 1 };

s2 -> s2 [0, 65535];

s2 -> s2 [69, 65535] { R117 += 1 };

accepting s2;

};

automaton value1_7 {

init s0;

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

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

s1 -> s2 [0, 65535];

s1 -> s1 [0, 65535] { R119 += 1, R2 += 1 };

s2 -> s2 [0, 65535];

accepting s0, s1, s2;

};

automaton value1_8 {

init s0;

s0 -> s1 [0, 68] { R121 += 1 };

s0 -> s2 [0, 65535] { R121 += 1, R10 += 1 };

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

s0 -> s3 [69, 69] { R121 += 1 };

s0 -> s1 [70, 65535] { R121 += 1 };

s1 -> s1 [0, 68] { R121 += 1 };

s1 -> s1 [0, 65535];

s1 -> s3 [69, 69] { R121 += 1 };

s1 -> s1 [70, 65535] { R121 += 1 };

s2 -> s1 [0, 68] { R121 += 1 };

s2 -> s2 [0, 65535] { R121 += 1, R10 += 1 };

s2 -> s4 [0, 65535];

s2 -> s3 [69, 69] { R121 += 1 };

s2 -> s1 [70, 65535] { R121 += 1 };

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

s4 -> s4 [0, 65535];

accepting s0, s1, s2, s4;

};

automaton value1_9 {

init s0;

s0 -> s1 [0, 8] { R123 += 1, R93 += 1 };

s0 -> s2 [0, 65535] { R123 += 1, R92 += 1, R93 += 1 };

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

s0 -> s3 [9, 13] { R123 += 1, R93 += 1 };

s0 -> s1 [14, 31] { R123 += 1, R93 += 1 };

s0 -> s3 [32, 32] { R123 += 1, R93 += 1 };

s0 -> s1 [33, 65535] { R123 += 1, R93 += 1 };

s1 -> s1 [0, 65535] { R123 += 1, R93 += 1 };

s1 -> s4 [0, 65535];

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

s2 -> s1 [0, 8] { R123 += 1, R93 += 1 };

s2 -> s4 [0, 65535];

s2 -> s2 [0, 65535] { R123 += 1, R92 += 1, R93 += 1 };

s2 -> s3 [9, 13] { R123 += 1, R93 += 1 };

s2 -> s1 [14, 31] { R123 += 1, R93 += 1 };

s2 -> s3 [32, 32] { R123 += 1, R93 += 1 };

s2 -> s1 [33, 65535] { R123 += 1, R93 += 1 };

s3 -> s1 [0, 65535] { R123 += 1, R93 += 1 };

s4 -> s4 [0, 65535];

s5 -> s4 [0, 65535];

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

accepting s4, s5, s2, s1, s0;

};

automaton value1_10 {

init s0;

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

s0 -> s1 [0, 65535] { R125 += 1, R94 += 1, R95 += 1 };

s0 -> s2 [0, 65535] { R125 += 1, R95 += 1, R7 += 1 };

s1 -> s1 [0, 65535] { R125 += 1, R94 += 1, R95 += 1 };

s1 -> s4 [0, 65535];

s1 -> s2 [0, 65535] { R125 += 1, R95 += 1, R7 += 1 };

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

s2 -> s4 [0, 65535];

s2 -> s2 [0, 65535] { R125 += 1, R95 += 1, R7 += 1 };

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

s3 -> s4 [0, 65535];

s4 -> s4 [0, 65535];

accepting s3, s4, s2, s1, s0;

};

automaton value1_11 {

init s0;

s0 -> s1 [0, 8] { R127 += 1, R97 += 1 };

s0 -> s2 [0, 65535] { R127 += 1, R96 += 1, R97 += 1 };

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

s0 -> s3 [9, 13] { R127 += 1, R97 += 1 };

s0 -> s1 [14, 31] { R127 += 1, R97 += 1 };

s0 -> s3 [32, 32] { R127 += 1, R97 += 1 };

s0 -> s1 [33, 65535] { R127 += 1, R97 += 1 };

s1 -> s4 [0, 65535];

s1 -> s1 [0, 65535] { R127 += 1, R97 += 1 };

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

s2 -> s1 [0, 8] { R127 += 1, R97 += 1 };

s2 -> s4 [0, 65535];

s2 -> s2 [0, 65535] { R127 += 1, R96 += 1, R97 += 1 };

s2 -> s3 [9, 13] { R127 += 1, R97 += 1 };

s2 -> s1 [14, 31] { R127 += 1, R97 += 1 };

s2 -> s3 [32, 32] { R127 += 1, R97 += 1 };

s2 -> s1 [33, 65535] { R127 += 1, R97 += 1 };

s3 -> s1 [0, 65535] { R127 += 1, R97 += 1 };

s4 -> s4 [0, 65535];

s5 -> s4 [0, 65535];

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

accepting s4, s5, s2, s1, s0;

};

automaton value1_12 {

init s0;

s0 -> s1 [0, 65535] { R129 += 1, R98 += 1, R99 += 1 };

s0 -> s2 [0, 65535] { R129 += 1, R99 += 1, R8 += 1 };

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

s1 -> s1 [0, 65535] { R129 += 1, R98 += 1, R99 += 1 };

s1 -> s2 [0, 65535] { R129 += 1, R99 += 1, R8 += 1 };

s1 -> s3 [0, 65535];

s2 -> s2 [0, 65535] { R129 += 1, R99 += 1, R8 += 1 };

s2 -> s3 [0, 65535];

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

s3 -> s3 [0, 65535];

s4 -> s3 [0, 65535];

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

accepting s3, s4, s2, s1, s0;

};

automaton value1_13 {

init s0;

s0 -> s1 [0, 68] { R131 += 1, R101 += 1 };

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

s0 -> s2 [0, 65535] { R131 += 1, R100 += 1, R101 += 1 };

s0 -> s1 [70, 65535] { R131 += 1, R101 += 1 };

s1 -> s1 [0, 68] { R131 += 1, R101 += 1 };

s1 -> s3 [0, 65535];

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

s1 -> s1 [70, 65535] { R131 += 1, R101 += 1 };

s2 -> s1 [0, 68] { R131 += 1, R101 += 1 };

s2 -> s3 [0, 65535];

s2 -> s2 [0, 65535] { R131 += 1, R100 += 1, R101 += 1 };

s2 -> s1 [70, 65535] { R131 += 1, R101 += 1 };

s3 -> s3 [0, 65535];

accepting s0, s1, s2, s3;

};

automaton value1_14 {

init s0;

s0 -> s1 [0, 65535] { R133 += 1, R102 += 1, R103 += 1 };

s0 -> s2 [0, 65535] { R133 += 1, R103 += 1, R78 += 1 };

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

s1 -> s1 [0, 65535] { R133 += 1, R102 += 1, R103 += 1 };

s1 -> s3 [0, 65535];

s1 -> s2 [0, 65535] { R133 += 1, R103 += 1, R78 += 1 };

s2 -> s3 [0, 65535];

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

s2 -> s2 [0, 65535] { R133 += 1, R103 += 1, R78 += 1 };

s3 -> s3 [0, 65535];

s4 -> s3 [0, 65535];

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

accepting s3, s4, s2, s1, s0;

};

automaton value1_15 {

init s0;

s0 -> s1 [0, 69] { R135 += 1, R105 += 1 };

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

s0 -> s2 [0, 65535] { R135 += 1, R104 += 1, R105 += 1 };

s0 -> s1 [91, 65535] { R135 += 1, R105 += 1 };

s1 -> s1 [0, 69] { R135 += 1, R105 += 1 };

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

s1 -> s3 [0, 65535];

s1 -> s1 [91, 65535] { R135 += 1, R105 += 1 };

s2 -> s1 [0, 69] { R135 += 1, R105 += 1 };

s2 -> s3 [0, 65535];

s2 -> s2 [0, 65535] { R135 += 1, R104 += 1, R105 += 1 };

s2 -> s1 [91, 65535] { R135 += 1, R105 += 1 };

s3 -> s3 [0, 65535];

accepting s0, s1, s2, s3;

};

automaton value1_16 {

init s0;

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

s0 -> s1 [0, 65535] { R137 += 1, R112 += 1, R113 += 1 };

s0 -> s2 [0, 65535] { R137 += 1, R113 += 1, R79 += 1 };

s1 -> s3 [0, 65535];

s1 -> s1 [0, 65535] { R137 += 1, R112 += 1, R113 += 1 };

s1 -> s2 [0, 65535] { R137 += 1, R113 += 1, R79 += 1 };

s2 -> s3 [0, 65535];

s2 -> s2 [0, 65535] { R137 += 1, R113 += 1, R79 += 1 };

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

s3 -> s3 [0, 65535];

s4 -> s3 [0, 65535];

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

accepting s3, s4, s2, s1, s0;

};

automaton value1_17 {

init s0;

s0 -> s1 [0, 68] { R139 += 1, R115 += 1 };

s0 -> s2 [0, 65535] { R139 += 1, R114 += 1, R115 += 1 };

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

s0 -> s3 [69, 69] { R139 += 1, R115 += 1 };

s0 -> s4 [69, 69] { R139 += 1, R115 += 1 };

s0 -> s1 [91, 65535] { R139 += 1, R115 += 1 };

s1 -> s1 [0, 68] { R139 += 1, R115 += 1 };

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

s1 -> s5 [0, 65535];

s1 -> s3 [69, 69] { R139 += 1, R115 += 1 };

s1 -> s4 [69, 69] { R139 += 1, R115 += 1 };

s1 -> s1 [91, 65535] { R139 += 1, R115 += 1 };

s2 -> s1 [0, 68] { R139 += 1, R115 += 1 };

s2 -> s5 [0, 65535];

s2 -> s2 [0, 65535] { R139 += 1, R114 += 1, R115 += 1 };

s2 -> s3 [69, 69] { R139 += 1, R115 += 1 };

s2 -> s4 [69, 69] { R139 += 1, R115 += 1 };

s2 -> s1 [91, 65535] { R139 += 1, R115 += 1 };

s3 -> s3 [0, 69] { R139 += 1, R115 += 1 };

s3 -> s5 [0, 65535];

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

s3 -> s3 [91, 65535] { R139 += 1, R115 += 1 };

s4 -> s5 [0, 65535];

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

s5 -> s5 [0, 65535];

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

};

};

synchronised { // Automata constraining c7

automaton c7_0 {

init s0;

s0 -> s1 [101, 101];

accepting s1;

};

};

synchronised { // Automata constraining P24

automaton P24_0 {

init s0;

s0 -> s1 [32, 32];

accepting s1;

};

};

synchronised { // Automata constraining P27

automaton P27_0 {

init s0;

s0 -> s1 [13, 13];

accepting s1;

};

};

synchronised { // Automata constraining P26

automaton P26_0 {

init s0;

s0 -> s1 [10, 10];

accepting s1;

};

};

synchronised { // Automata constraining value2

automaton value2_0 {

init s0;

s0 -> s0 [0, 43];

s0 -> s0 [45, 64];

s0 -> s0 [91, 65535];

accepting s0;

};

automaton value2_1 {

init s0;

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

accepting s0;

};

automaton value2_2 {

init s0;

s0 -> s1 [0, 60];

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

s0 -> s2 [61, 61];

s0 -> s1 [62, 65535];

s1 -> s1 [0, 60];

s1 -> s2 [61, 61];

s1 -> s1 [62, 65535];

s2 -> s2 [0, 65535];

accepting s0, s1;

};

automaton value2_3 {

init s0;

s0 -> s1 [0, 8] { R85 += 1 };

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

s0 -> s2 [9, 13] { R85 += 1 };

s0 -> s1 [14, 31] { R85 += 1 };

s0 -> s2 [32, 32] { R85 += 1 };

s0 -> s1 [33, 65535] { R85 += 1 };

s1 -> s3 [0, 65535];

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

s2 -> s1 [0, 65535] { R85 += 1 };

s3 -> s3 [0, 65535];

accepting s0, s1, s3;

};

automaton value2_4 {

init s0;

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

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

s1 -> s2 [0, 65535];

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

s2 -> s2 [0, 65535];

accepting s0, s1, s2;

};

automaton value2_5 {

init s0;

s0 -> s1 [0, 8] { R89 += 1 };

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

s0 -> s2 [9, 13] { R89 += 1 };

s0 -> s1 [14, 31] { R89 += 1 };

s0 -> s2 [32, 32] { R89 += 1 };

s0 -> s1 [33, 65535] { R89 += 1 };

s1 -> s3 [0, 65535];

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

s2 -> s1 [0, 65535] { R89 += 1 };

s3 -> s3 [0, 65535];

accepting s0, s1, s3;

};

automaton value2_6 {

init s0;

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

s0 -> s1 [0, 65535] { R91 += 1, R6 += 1 };

s1 -> s2 [0, 65535];

s1 -> s1 [0, 65535] { R91 += 1, R6 += 1 };

s2 -> s2 [0, 65535];

accepting s0, s1, s2;

};

};

constraint R2 = R105 && R3 = R111 && R14 = 0 && R15 = R139 && R80 = 0 && R92 - R105 = -1 && R93 = R105 && R94 - R105 = -1 && R95 = R105 && R96 = 0 && R97 = 1 && R98 = 0 && R99 = 1 && R100 = 0 && R101 = R105 && R102 = 0 && R103 = R105 && R104 = 0 && R106 - R139 = 1 && R107 = R111 && R108 - R139 = 1 && R109 = R111 && R110 - R139 = 1 && R116 = 0 && R117 = R139 && R118 = 0 && R119 = R139 && R120 = 0 && R121 = R139 && R122 = 0 && R123 = R139 && R124 = 0 && R125 = R139 && R126 = 0 && R127 = R139 && R128 = 0 && R129 = R139 && R130 = 0 && R131 = R139 && R132 = 0 && R133 = R139 && R134 = 0 && R135 = R139 && R136 = 0 && R137 = R139 && R138 = 0 && R0 != 0 && R1 != 0 && R9 < 1 && R10 < 1 && 0 < R105 && R139 < R111 && -1 < R139 && (R0 != R81 || R81 = 1 || R81 < 0) && (R5 != 0 || ((R1 != R85 || R84 - R85 = -1 || R85 < 0) && (R1 = R85 || R1 < 1))) && (R5 != 0 || ((R1 != R87 || R86 - R87 = -1 || R87 < 0) && (R1 = R87 || R1 < 1))) && (R81 != 1 || -1 < R0) && (R82 != 0 || ((R4 != 0 || ((R0 != R83 || R83 = 1 || R83 < 0) && (R0 = R83 || R83 = 1 || R0 < 1))) && (R4 = 0 || ((R0 != R83 || R83 = 1 || R83 < 0) && (R83 != 1 || -1 < R0) && (R0 = R83 || R83 = 1))))) && (R88 != 0 || ((R6 != 0 || ((R1 != R89 || R89 = 1 || R89 < 0) && (R1 = R89 || R89 = 1 || R1 < 1))) && (R6 = 0 || ((R1 != R89 || R89 = 1 || R89 < 0) && (R89 != 1 || -1 < R1) && (R1 = R89 || R89 = 1))))) && (R90 != 0 || ((R6 != 0 || ((R1 != R91 || R91 = 1 || R91 < 0) && (R1 = R91 || R91 = 1 || R1 < 1))) && (R6 = 0 || ((R1 != R91 || R91 = 1 || R91 < 0) && (R91 != 1 || -1 < R1) && (R1 = R91 || R91 = 1))))) && (R0 = R81 || R81 = 1) && (R5 = 0 || (R1 = R85 && R84 - R85 = -1)) && (R5 = 0 || (R1 = R87 && R86 - R87 = -1)) && (R79 = 0 || (R112 = 0 && R113 = 0)) && (R79 = 0 || (R114 = 0 && R115 = 0)) && (R82 = 0 || (R4 = 0 && R0 < 0)) && (R88 = 0 || (R6 = 0 && R1 < 0)) && (R90 = 0 || (R6 = 0 && R1 < 0));

// End of Parikh automata intersection problem