MAYBE Initial complexity problem: 1: T: (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_3, Fresh_204, Fresh_205, Ar_3, 0, Fresh_206, Fresh_207, Fresh_208, Fresh_209, Fresh_210, Fresh_211, Ar_2, Ar_2, Ar_2, Fresh_212, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_206 >= 2 /\ 0 >= Ar_2 + 1 /\ Fresh_212 >= Fresh_206 /\ Ar_3 >= Fresh_206 /\ Ar_4 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_3, Fresh_195, Fresh_196, Ar_3, 0, Fresh_197, Fresh_198, Fresh_199, Fresh_200, Fresh_201, Fresh_202, Ar_2, Ar_2, Ar_2, Fresh_203, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_197 >= 2 /\ Ar_2 >= 1 /\ Fresh_203 >= Fresh_197 /\ Ar_3 >= Fresh_197 /\ Ar_4 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_10, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_10, Fresh_193, Ar_11, Ar_12, Ar_13, Ar_14, Fresh_194, Ar_0, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_1 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, 1, Fresh_189, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_190, Fresh_190, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_191, Ar_3 + 1, Fresh_192, Ar_3, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_0 >= 0 /\ Fresh_189 >= 2 /\ 0 >= Ar_13 + 1 /\ R1 >= Fresh_189 /\ 0 >= Fresh_190 + 1 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, 1, Fresh_185, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_186, Fresh_186, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_187, Ar_3 + 1, Fresh_188, Ar_3, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_0 >= 0 /\ Fresh_185 >= 2 /\ 0 >= Ar_13 + 1 /\ R1 >= Fresh_185 /\ Fresh_186 >= 1 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, 1, Fresh_181, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_182, Fresh_182, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_183, Ar_3 + 1, Fresh_184, Ar_3, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_0 >= 0 /\ Fresh_181 >= 2 /\ Ar_13 >= 1 /\ R1 >= Fresh_181 /\ 0 >= Fresh_182 + 1 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, 1, Fresh_177, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_178, Fresh_178, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_179, Ar_3 + 1, Fresh_180, Ar_3, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_0 >= 0 /\ Fresh_177 >= 2 /\ Ar_13 >= 1 /\ R1 >= Fresh_177 /\ Fresh_178 >= 1 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_173, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_174, Fresh_174, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Fresh_175, Fresh_176, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_20 >= 0 /\ Fresh_173 >= 2 /\ 0 >= Ar_13 + 1 /\ 0 >= Fresh_174 + 1 /\ 0 >= Fresh_176 + 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_169, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_170, Fresh_170, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Fresh_171, Fresh_172, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_20 >= 0 /\ Fresh_169 >= 2 /\ 0 >= Ar_13 + 1 /\ 0 >= Fresh_170 + 1 /\ Fresh_172 >= 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_165, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_166, Fresh_166, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Fresh_167, Fresh_168, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_20 >= 0 /\ Fresh_165 >= 2 /\ 0 >= Ar_13 + 1 /\ Fresh_166 >= 1 /\ 0 >= Fresh_168 + 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_161, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_162, Fresh_162, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Fresh_163, Fresh_164, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_20 >= 0 /\ Fresh_161 >= 2 /\ 0 >= Ar_13 + 1 /\ Fresh_162 >= 1 /\ Fresh_164 >= 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_157, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_158, Fresh_158, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Fresh_159, Fresh_160, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_20 >= 0 /\ Fresh_157 >= 2 /\ Ar_13 >= 1 /\ 0 >= Fresh_158 + 1 /\ 0 >= Fresh_160 + 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_153, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_154, Fresh_154, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Fresh_155, Fresh_156, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_20 >= 0 /\ Fresh_153 >= 2 /\ Ar_13 >= 1 /\ 0 >= Fresh_154 + 1 /\ Fresh_156 >= 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_149, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_150, Fresh_150, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Fresh_151, Fresh_152, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_20 >= 0 /\ Fresh_149 >= 2 /\ Ar_13 >= 1 /\ Fresh_150 >= 1 /\ 0 >= Fresh_152 + 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_145, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_146, Fresh_146, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Fresh_147, Fresh_148, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_20 >= 0 /\ Fresh_145 >= 2 /\ Ar_13 >= 1 /\ Fresh_146 >= 1 /\ Fresh_148 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Fresh_141, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_142, Fresh_142, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_143, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_13, Fresh_144, Ar_4 + 1, Ar_3 - 1, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_141 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_142 + 1 /\ 0 >= Fresh_144 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Fresh_137, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_138, Fresh_138, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_139, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_13, Fresh_140, Ar_4 + 1, Ar_3 - 1, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_137 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_138 + 1 /\ Fresh_140 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Fresh_133, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_134, Fresh_134, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_135, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_13, Fresh_136, Ar_4 + 1, Ar_3 - 1, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_133 >= 2 /\ 0 >= R1 + 1 /\ Fresh_134 >= 1 /\ 0 >= Fresh_136 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Fresh_129, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_130, Fresh_130, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_131, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_13, Fresh_132, Ar_4 + 1, Ar_3 - 1, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_129 >= 2 /\ 0 >= R1 + 1 /\ Fresh_130 >= 1 /\ Fresh_132 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Fresh_125, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_126, Fresh_126, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_127, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_13, Fresh_128, Ar_4 + 1, Ar_3 - 1, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_125 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_126 + 1 /\ 0 >= Fresh_128 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Fresh_121, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_122, Fresh_122, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_123, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_13, Fresh_124, Ar_4 + 1, Ar_3 - 1, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_121 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_122 + 1 /\ Fresh_124 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Fresh_117, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_118, Fresh_118, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_119, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_13, Fresh_120, Ar_4 + 1, Ar_3 - 1, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_117 >= 2 /\ R1 >= 1 /\ Fresh_118 >= 1 /\ 0 >= Fresh_120 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Fresh_113, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_114, Fresh_114, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_115, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_13, Fresh_116, Ar_4 + 1, Ar_3 - 1, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_113 >= 2 /\ R1 >= 1 /\ Fresh_114 >= 1 /\ Fresh_116 >= 1 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_111, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_112, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_112, 0, Fresh_112, Ar_27, Ar_34, Ar_35, Ar_36, Ar_37)) [ P1 >= Ar_27 + 1 /\ Ar_28 >= 0 /\ Fresh_111 >= 2 /\ Fresh_112 >= P1 + 1 /\ 0 >= Fresh_112 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_109, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_110, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_110, 0, Fresh_110, Ar_27, Ar_34, Ar_35, Ar_36, Ar_37)) [ P1 >= Ar_27 + 1 /\ Ar_28 >= 0 /\ Fresh_109 >= 2 /\ Fresh_110 >= P1 + 1 /\ Fresh_110 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_107, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_108, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_108, 0, Fresh_108, Ar_27, Ar_34, Ar_35, Ar_36, Ar_37)) [ P1 >= Ar_27 + 1 /\ Ar_28 >= 0 /\ Fresh_107 >= 2 /\ P1 >= Fresh_108 + 1 /\ 0 >= Fresh_108 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_105, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_106, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_106, 0, Fresh_106, Ar_27, Ar_34, Ar_35, Ar_36, Ar_37)) [ P1 >= Ar_27 + 1 /\ Ar_28 >= 0 /\ Fresh_105 >= 2 /\ P1 >= Fresh_106 + 1 /\ Fresh_106 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_103, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_104, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_104, 0, Fresh_104, Ar_27, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_27 >= P1 + 1 /\ Ar_28 >= 0 /\ Fresh_103 >= 2 /\ Fresh_104 >= P1 + 1 /\ 0 >= Fresh_104 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_101, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_102, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_102, 0, Fresh_102, Ar_27, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_27 >= P1 + 1 /\ Ar_28 >= 0 /\ Fresh_101 >= 2 /\ Fresh_102 >= P1 + 1 /\ Fresh_102 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_99, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_100, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_100, 0, Fresh_100, Ar_27, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_27 >= P1 + 1 /\ Ar_28 >= 0 /\ Fresh_99 >= 2 /\ P1 >= Fresh_100 + 1 /\ 0 >= Fresh_100 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_97, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_98, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_98, 0, Fresh_98, Ar_27, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_27 >= P1 + 1 /\ Ar_28 >= 0 /\ Fresh_97 >= 2 /\ P1 >= Fresh_98 + 1 /\ Fresh_98 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_88, Ar_6, Fresh_89, Ar_8, Ar_9, Ar_10, Fresh_90, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Fresh_91, Ar_28, Fresh_92, Fresh_93, Fresh_94, Fresh_95, Fresh_96, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_28 >= 0 /\ 0 >= Fresh_90 + 1 /\ Fresh_88 >= 2 /\ Ar_29 = Ar_27 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_79, Ar_6, Fresh_80, Ar_8, Ar_9, Ar_10, Fresh_81, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Fresh_82, Ar_28, Fresh_83, Fresh_84, Fresh_85, Fresh_86, Fresh_87, Ar_34, Ar_35, Ar_36, Ar_37)) [ Ar_28 >= 0 /\ Fresh_81 >= 1 /\ Fresh_79 >= 2 /\ Ar_29 = Ar_27 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_76, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_77, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_78, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_77, 0, Fresh_77, Ar_27, Ar_34 - 1, Ar_34 - 1, Ar_36, Ar_37)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_76 >= 2 /\ Fresh_77 >= Q1 + 1 /\ 0 >= Fresh_77 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_73, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_74, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_75, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_74, 0, Fresh_74, Ar_27, Ar_34 - 1, Ar_34 - 1, Ar_36, Ar_37)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_73 >= 2 /\ Fresh_74 >= Q1 + 1 /\ Fresh_74 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_70, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_71, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_72, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_71, 0, Fresh_71, Ar_27, Ar_34 - 1, Ar_34 - 1, Ar_36, Ar_37)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_70 >= 2 /\ Q1 >= Fresh_71 + 1 /\ 0 >= Fresh_71 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_67, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_68, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_69, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_68, 0, Fresh_68, Ar_27, Ar_34 - 1, Ar_34 - 1, Ar_36, Ar_37)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_67 >= 2 /\ Q1 >= Fresh_68 + 1 /\ Fresh_68 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_64, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_65, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_66, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_65, 0, Fresh_65, Ar_27, Ar_34 - 1, Ar_34 - 1, Ar_36, Ar_37)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_64 >= 2 /\ Fresh_65 >= Q1 + 1 /\ 0 >= Fresh_65 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_61, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_62, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_63, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_62, 0, Fresh_62, Ar_27, Ar_34 - 1, Ar_34 - 1, Ar_36, Ar_37)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_61 >= 2 /\ Fresh_62 >= Q1 + 1 /\ Fresh_62 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_58, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_59, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_60, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_59, 0, Fresh_59, Ar_27, Ar_34 - 1, Ar_34 - 1, Ar_36, Ar_37)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_58 >= 2 /\ Q1 >= Fresh_59 + 1 /\ 0 >= Fresh_59 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_55, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Fresh_56, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Fresh_57, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, 0, Fresh_56, 0, Fresh_56, Ar_27, Ar_34 - 1, Ar_34 - 1, Ar_36, Ar_37)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_55 >= 2 /\ Q1 >= Fresh_56 + 1 /\ Fresh_56 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Fresh_47, Ar_6, Fresh_48, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Fresh_49, Ar_28, Fresh_50, Fresh_51, Fresh_52, Fresh_53, Fresh_54, Ar_34, Ar_35, Ar_36, Ar_37)) [ Fresh_47 >= 2 /\ Ar_34 >= 0 /\ Ar_29 = Ar_27 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f1(2, Fresh_42, Fresh_43, Ar_3, Ar_4, Fresh_42, Ar_6, Ar_7, Fresh_43, Fresh_43, Fresh_44, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Fresh_45, Fresh_46)) [ Fresh_42 >= 2 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f16(Fresh_24, Fresh_25, Fresh_26, Ar_3, Ar_4, Fresh_27, Fresh_28, Fresh_29, Fresh_30, Fresh_31, Fresh_32, 0, Fresh_33, Fresh_34, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Fresh_35, Ar_28, Fresh_36, Fresh_37, Fresh_38, Fresh_39, Fresh_40, Ar_34, Ar_35, Fresh_41, Ar_37)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_27 /\ 0 >= X1' ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Fresh_21, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Fresh_22, Fresh_23, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_11, Ar_34, 0, Ar_11, 0, Ar_11, Ar_11, Ar_34, Ar_35, Ar_36, Ar_37)) [ Q1 >= 2 /\ Fresh_21 >= 2 /\ Ar_20 >= 0 /\ Ar_11 >= 1 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Fresh_18, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Fresh_19, Fresh_20, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_11, Ar_34, 0, Ar_11, 0, Ar_11, Ar_11, Ar_34, Ar_35, Ar_36, Ar_37)) [ Q1 >= 2 /\ Fresh_18 >= 2 /\ Ar_20 >= 0 /\ Ar_11 >= 1 /\ Ar_13 = 0 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Fresh_15, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Fresh_16, Fresh_17, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_11, Ar_34, 0, Ar_11, 0, Ar_11, Ar_11, Ar_34, Ar_35, Ar_36, Ar_37)) [ Q1 >= 2 /\ Fresh_15 >= 2 /\ Ar_20 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Fresh_12, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Fresh_13, Fresh_14, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_11, Ar_34, 0, Ar_11, 0, Ar_11, Ar_11, Ar_34, Ar_35, Ar_36, Ar_37)) [ Q1 >= 2 /\ Fresh_12 >= 2 /\ Ar_20 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_11 >= 1 /\ Ar_13 = 0 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Fresh_9, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Fresh_10, Fresh_11, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_11, Ar_34, 0, Ar_11, 0, Ar_11, Ar_11, Ar_34, Ar_35, Ar_36, Ar_37)) [ Q1 >= 2 /\ Fresh_9 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ Ar_11 >= 1 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Fresh_6, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Fresh_7, Fresh_8, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_11, Ar_34, 0, Ar_11, 0, Ar_11, Ar_11, Ar_34, Ar_35, Ar_36, Ar_37)) [ Q1 >= 2 /\ Fresh_6 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ Ar_11 >= 1 /\ Ar_13 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Fresh_3, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Fresh_4, Fresh_5, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_11, Ar_34, 0, Ar_11, 0, Ar_11, Ar_11, Ar_34, Ar_35, Ar_36, Ar_37)) [ Q1 >= 2 /\ Fresh_3 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Fresh_0, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Fresh_1, Fresh_2, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_11, Ar_34, 0, Ar_11, 0, Ar_11, Ar_11, Ar_34, Ar_35, Ar_36, Ar_37)) [ Q1 >= 2 /\ Fresh_0 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_11 >= 1 /\ Ar_13 = 0 ] (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34]. We thus obtain the following problem: 2: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ 0 <= 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_2, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_0 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_11 >= 1 /\ Ar_13 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_5, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_3 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_8, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_6 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ Ar_11 >= 1 /\ Ar_13 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_11, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_9 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ Ar_11 >= 1 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_14, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_12 >= 2 /\ Ar_20 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_11 >= 1 /\ Ar_13 = 0 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_17, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_15 >= 2 /\ Ar_20 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_20, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_18 >= 2 /\ Ar_20 >= 0 /\ Ar_11 >= 1 /\ Ar_13 = 0 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_23, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_21 >= 2 /\ Ar_20 >= 0 /\ Ar_11 >= 1 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f16(Fresh_24, Fresh_25, Fresh_26, Ar_3, Ar_4, Fresh_32, 0, Fresh_34, Ar_20, Fresh_35, Ar_28, Fresh_36, Ar_34)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_27 /\ 0 >= X1' ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f1(2, Fresh_42, Fresh_43, Ar_3, Ar_4, Fresh_44, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Fresh_42 >= 2 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Fresh_49, Ar_28, Fresh_50, Ar_34)) [ Fresh_47 >= 2 /\ Ar_34 >= 0 /\ Ar_29 = Ar_27 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_56, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_55 >= 2 /\ Q1 >= Fresh_56 + 1 /\ Fresh_56 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_59, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_58 >= 2 /\ Q1 >= Fresh_59 + 1 /\ 0 >= Fresh_59 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_62, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_61 >= 2 /\ Fresh_62 >= Q1 + 1 /\ Fresh_62 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_65, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_64 >= 2 /\ Fresh_65 >= Q1 + 1 /\ 0 >= Fresh_65 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_68, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_67 >= 2 /\ Q1 >= Fresh_68 + 1 /\ Fresh_68 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_71, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_70 >= 2 /\ Q1 >= Fresh_71 + 1 /\ 0 >= Fresh_71 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_74, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_73 >= 2 /\ Fresh_74 >= Q1 + 1 /\ Fresh_74 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_77, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_76 >= 2 /\ Fresh_77 >= Q1 + 1 /\ 0 >= Fresh_77 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_81, Ar_13, Ar_20, Fresh_82, Ar_28, Fresh_83, Ar_34)) [ Ar_28 >= 0 /\ Fresh_81 >= 1 /\ Fresh_79 >= 2 /\ Ar_29 = Ar_27 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_90, Ar_13, Ar_20, Fresh_91, Ar_28, Fresh_92, Ar_34)) [ Ar_28 >= 0 /\ 0 >= Fresh_90 + 1 /\ Fresh_88 >= 2 /\ Ar_29 = Ar_27 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_98, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ Ar_27 >= P1 + 1 /\ Ar_28 >= 0 /\ Fresh_97 >= 2 /\ P1 >= Fresh_98 + 1 /\ Fresh_98 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_100, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ Ar_27 >= P1 + 1 /\ Ar_28 >= 0 /\ Fresh_99 >= 2 /\ P1 >= Fresh_100 + 1 /\ 0 >= Fresh_100 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_102, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ Ar_27 >= P1 + 1 /\ Ar_28 >= 0 /\ Fresh_101 >= 2 /\ Fresh_102 >= P1 + 1 /\ Fresh_102 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_104, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ Ar_27 >= P1 + 1 /\ Ar_28 >= 0 /\ Fresh_103 >= 2 /\ Fresh_104 >= P1 + 1 /\ 0 >= Fresh_104 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_106, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ P1 >= Ar_27 + 1 /\ Ar_28 >= 0 /\ Fresh_105 >= 2 /\ P1 >= Fresh_106 + 1 /\ Fresh_106 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_108, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ P1 >= Ar_27 + 1 /\ Ar_28 >= 0 /\ Fresh_107 >= 2 /\ P1 >= Fresh_108 + 1 /\ 0 >= Fresh_108 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_110, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ P1 >= Ar_27 + 1 /\ Ar_28 >= 0 /\ Fresh_109 >= 2 /\ Fresh_110 >= P1 + 1 /\ Fresh_110 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_112, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ P1 >= Ar_27 + 1 /\ Ar_28 >= 0 /\ Fresh_111 >= 2 /\ Fresh_112 >= P1 + 1 /\ 0 >= Fresh_112 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_114, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_113 >= 2 /\ R1 >= 1 /\ Fresh_114 >= 1 /\ Fresh_116 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_118, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_117 >= 2 /\ R1 >= 1 /\ Fresh_118 >= 1 /\ 0 >= Fresh_120 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_122, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_121 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_122 + 1 /\ Fresh_124 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_126, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_125 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_126 + 1 /\ 0 >= Fresh_128 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_130, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_129 >= 2 /\ 0 >= R1 + 1 /\ Fresh_130 >= 1 /\ Fresh_132 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_134, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_133 >= 2 /\ 0 >= R1 + 1 /\ Fresh_134 >= 1 /\ 0 >= Fresh_136 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_138, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_137 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_138 + 1 /\ Fresh_140 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_142, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_141 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_142 + 1 /\ 0 >= Fresh_144 + 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_146, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_145 >= 2 /\ Ar_13 >= 1 /\ Fresh_146 >= 1 /\ Fresh_148 >= 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_150, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_149 >= 2 /\ Ar_13 >= 1 /\ Fresh_150 >= 1 /\ 0 >= Fresh_152 + 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_154, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_153 >= 2 /\ Ar_13 >= 1 /\ 0 >= Fresh_154 + 1 /\ Fresh_156 >= 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_158, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_157 >= 2 /\ Ar_13 >= 1 /\ 0 >= Fresh_158 + 1 /\ 0 >= Fresh_160 + 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_162, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_161 >= 2 /\ 0 >= Ar_13 + 1 /\ Fresh_162 >= 1 /\ Fresh_164 >= 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_166, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_165 >= 2 /\ 0 >= Ar_13 + 1 /\ Fresh_166 >= 1 /\ 0 >= Fresh_168 + 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_170, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_169 >= 2 /\ 0 >= Ar_13 + 1 /\ 0 >= Fresh_170 + 1 /\ Fresh_172 >= 1 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_174, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_173 >= 2 /\ 0 >= Ar_13 + 1 /\ 0 >= Fresh_174 + 1 /\ 0 >= Fresh_176 + 1 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, 1, Ar_10, Fresh_178, Ar_13, Ar_3, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_0 >= 0 /\ Fresh_177 >= 2 /\ Ar_13 >= 1 /\ R1 >= Fresh_177 /\ Fresh_178 >= 1 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, 1, Ar_10, Fresh_182, Ar_13, Ar_3, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_0 >= 0 /\ Fresh_181 >= 2 /\ Ar_13 >= 1 /\ R1 >= Fresh_181 /\ 0 >= Fresh_182 + 1 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, 1, Ar_10, Fresh_186, Ar_13, Ar_3, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_0 >= 0 /\ Fresh_185 >= 2 /\ 0 >= Ar_13 + 1 /\ R1 >= Fresh_185 /\ Fresh_186 >= 1 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, 1, Ar_10, Fresh_190, Ar_13, Ar_3, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_0 >= 0 /\ Fresh_189 >= 2 /\ 0 >= Ar_13 + 1 /\ R1 >= Fresh_189 /\ 0 >= Fresh_190 + 1 /\ Ar_4 = 1 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_10, Ar_3, Ar_4, Fresh_193, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_1 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_195, Fresh_196, Ar_3, 0, Fresh_202, Ar_2, Ar_2, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_197 >= 2 /\ Ar_2 >= 1 /\ Fresh_203 >= Fresh_197 /\ Ar_3 >= Fresh_197 /\ Ar_4 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_204, Fresh_205, Ar_3, 0, Fresh_211, Ar_2, Ar_2, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_206 >= 2 /\ 0 >= Ar_2 + 1 /\ Fresh_212 >= Fresh_206 /\ Ar_3 >= Fresh_206 /\ Ar_4 = 0 ] start location: koat_start leaf cost: 0 Testing for reachability in the complexity graph removes the following transitions from problem 2: f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_2, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_0 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_11 >= 1 /\ Ar_13 = 0 ] f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_11, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_9 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ Ar_11 >= 1 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 ] f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_14, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_12 >= 2 /\ Ar_20 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_11 >= 1 /\ Ar_13 = 0 /\ Ar_4 = 1 ] f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_17, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_15 >= 2 /\ Ar_20 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 /\ Ar_4 = 1 ] f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_20, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_18 >= 2 /\ Ar_20 >= 0 /\ Ar_11 >= 1 /\ Ar_13 = 0 /\ Ar_4 = 1 ] f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_23, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_21 >= 2 /\ Ar_20 >= 0 /\ Ar_11 >= 1 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 /\ Ar_4 = 1 ] f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_81, Ar_13, Ar_20, Fresh_82, Ar_28, Fresh_83, Ar_34)) [ Ar_28 >= 0 /\ Fresh_81 >= 1 /\ Fresh_79 >= 2 /\ Ar_29 = Ar_27 ] f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_90, Ar_13, Ar_20, Fresh_91, Ar_28, Fresh_92, Ar_34)) [ Ar_28 >= 0 /\ 0 >= Fresh_90 + 1 /\ Fresh_88 >= 2 /\ Ar_29 = Ar_27 ] f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_98, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ Ar_27 >= P1 + 1 /\ Ar_28 >= 0 /\ Fresh_97 >= 2 /\ P1 >= Fresh_98 + 1 /\ Fresh_98 >= 1 /\ Ar_29 = 0 ] f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_100, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ Ar_27 >= P1 + 1 /\ Ar_28 >= 0 /\ Fresh_99 >= 2 /\ P1 >= Fresh_100 + 1 /\ 0 >= Fresh_100 + 1 /\ Ar_29 = 0 ] f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_102, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ Ar_27 >= P1 + 1 /\ Ar_28 >= 0 /\ Fresh_101 >= 2 /\ Fresh_102 >= P1 + 1 /\ Fresh_102 >= 1 /\ Ar_29 = 0 ] f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_104, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ Ar_27 >= P1 + 1 /\ Ar_28 >= 0 /\ Fresh_103 >= 2 /\ Fresh_104 >= P1 + 1 /\ 0 >= Fresh_104 + 1 /\ Ar_29 = 0 ] f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_106, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ P1 >= Ar_27 + 1 /\ Ar_28 >= 0 /\ Fresh_105 >= 2 /\ P1 >= Fresh_106 + 1 /\ Fresh_106 >= 1 /\ Ar_29 = 0 ] f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_108, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ P1 >= Ar_27 + 1 /\ Ar_28 >= 0 /\ Fresh_107 >= 2 /\ P1 >= Fresh_108 + 1 /\ 0 >= Fresh_108 + 1 /\ Ar_29 = 0 ] f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_110, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ P1 >= Ar_27 + 1 /\ Ar_28 >= 0 /\ Fresh_109 >= 2 /\ Fresh_110 >= P1 + 1 /\ Fresh_110 >= 1 /\ Ar_29 = 0 ] f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_112, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34)) [ P1 >= Ar_27 + 1 /\ Ar_28 >= 0 /\ Fresh_111 >= 2 /\ Fresh_112 >= P1 + 1 /\ 0 >= Fresh_112 + 1 /\ Ar_29 = 0 ] f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_146, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_145 >= 2 /\ Ar_13 >= 1 /\ Fresh_146 >= 1 /\ Fresh_148 >= 1 ] f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_150, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_149 >= 2 /\ Ar_13 >= 1 /\ Fresh_150 >= 1 /\ 0 >= Fresh_152 + 1 ] f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_154, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_153 >= 2 /\ Ar_13 >= 1 /\ 0 >= Fresh_154 + 1 /\ Fresh_156 >= 1 ] f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_158, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_157 >= 2 /\ Ar_13 >= 1 /\ 0 >= Fresh_158 + 1 /\ 0 >= Fresh_160 + 1 ] f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_162, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_161 >= 2 /\ 0 >= Ar_13 + 1 /\ Fresh_162 >= 1 /\ Fresh_164 >= 1 ] f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_166, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_165 >= 2 /\ 0 >= Ar_13 + 1 /\ Fresh_166 >= 1 /\ 0 >= Fresh_168 + 1 ] f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_170, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_169 >= 2 /\ 0 >= Ar_13 + 1 /\ 0 >= Fresh_170 + 1 /\ Fresh_172 >= 1 ] f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_174, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_20 >= 0 /\ Fresh_173 >= 2 /\ 0 >= Ar_13 + 1 /\ 0 >= Fresh_174 + 1 /\ 0 >= Fresh_176 + 1 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, 1, Ar_10, Fresh_178, Ar_13, Ar_3, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_0 >= 0 /\ Fresh_177 >= 2 /\ Ar_13 >= 1 /\ R1 >= Fresh_177 /\ Fresh_178 >= 1 /\ Ar_4 = 1 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, 1, Ar_10, Fresh_182, Ar_13, Ar_3, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_0 >= 0 /\ Fresh_181 >= 2 /\ Ar_13 >= 1 /\ R1 >= Fresh_181 /\ 0 >= Fresh_182 + 1 /\ Ar_4 = 1 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, 1, Ar_10, Fresh_186, Ar_13, Ar_3, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_0 >= 0 /\ Fresh_185 >= 2 /\ 0 >= Ar_13 + 1 /\ R1 >= Fresh_185 /\ Fresh_186 >= 1 /\ Ar_4 = 1 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3, 1, Ar_10, Fresh_190, Ar_13, Ar_3, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_0 >= 0 /\ Fresh_189 >= 2 /\ 0 >= Ar_13 + 1 /\ R1 >= Fresh_189 /\ 0 >= Fresh_190 + 1 /\ Ar_4 = 1 ] We thus obtain the following problem: 3: T: (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Fresh_49, Ar_28, Fresh_50, Ar_34)) [ Fresh_47 >= 2 /\ Ar_34 >= 0 /\ Ar_29 = Ar_27 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_56, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_55 >= 2 /\ Q1 >= Fresh_56 + 1 /\ Fresh_56 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_77, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_76 >= 2 /\ Fresh_77 >= Q1 + 1 /\ 0 >= Fresh_77 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_74, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_73 >= 2 /\ Fresh_74 >= Q1 + 1 /\ Fresh_74 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_71, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_70 >= 2 /\ Q1 >= Fresh_71 + 1 /\ 0 >= Fresh_71 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_68, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_67 >= 2 /\ Q1 >= Fresh_68 + 1 /\ Fresh_68 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_65, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_64 >= 2 /\ Fresh_65 >= Q1 + 1 /\ 0 >= Fresh_65 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_62, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_61 >= 2 /\ Fresh_62 >= Q1 + 1 /\ Fresh_62 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_59, Ar_13, Ar_20, Ar_27, Ar_28, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_58 >= 2 /\ Q1 >= Fresh_59 + 1 /\ 0 >= Fresh_59 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_5, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_3 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_8, Ar_20, Ar_11, Ar_34, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_6 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ Ar_11 >= 1 /\ Ar_13 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_142, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_141 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_142 + 1 /\ 0 >= Fresh_144 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_138, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_137 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_138 + 1 /\ Fresh_140 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_134, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_133 >= 2 /\ 0 >= R1 + 1 /\ Fresh_134 >= 1 /\ 0 >= Fresh_136 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_130, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_129 >= 2 /\ 0 >= R1 + 1 /\ Fresh_130 >= 1 /\ Fresh_132 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_126, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_125 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_126 + 1 /\ 0 >= Fresh_128 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_122, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_121 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_122 + 1 /\ Fresh_124 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_118, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_117 >= 2 /\ R1 >= 1 /\ Fresh_118 >= 1 /\ 0 >= Fresh_120 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_114, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_113 >= 2 /\ R1 >= 1 /\ Fresh_114 >= 1 /\ Fresh_116 >= 1 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_204, Fresh_205, Ar_3, 0, Fresh_211, Ar_2, Ar_2, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_206 >= 2 /\ 0 >= Ar_2 + 1 /\ Fresh_212 >= Fresh_206 /\ Ar_3 >= Fresh_206 /\ Ar_4 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_195, Fresh_196, Ar_3, 0, Fresh_202, Ar_2, Ar_2, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_197 >= 2 /\ Ar_2 >= 1 /\ Fresh_203 >= Fresh_197 /\ Ar_3 >= Fresh_197 /\ Ar_4 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_10, Ar_3, Ar_4, Fresh_193, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Ar_1 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f1(2, Fresh_42, Fresh_43, Ar_3, Ar_4, Fresh_44, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ Fresh_42 >= 2 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f16(Fresh_24, Fresh_25, Fresh_26, Ar_3, Ar_4, Fresh_32, 0, Fresh_34, Ar_20, Fresh_35, Ar_28, Fresh_36, Ar_34)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_27 /\ 0 >= X1' ] (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_20, Ar_27, Ar_28, Ar_29, Ar_34)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 3 produces the following problem: 4: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Fresh_24, Fresh_25, Fresh_26, Ar_3, Ar_4, Fresh_32, 0, Fresh_34, Fresh_35, Fresh_36, Ar_34)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_27 /\ 0 >= X1' ] (Comp: 1, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f1(2, Fresh_42, Fresh_43, Ar_3, Ar_4, Fresh_44, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ Fresh_42 >= 2 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_10, Ar_3, Ar_4, Fresh_193, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_1 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_195, Fresh_196, Ar_3, 0, Fresh_202, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_197 >= 2 /\ Ar_2 >= 1 /\ Fresh_203 >= Fresh_197 /\ Ar_3 >= Fresh_197 /\ Ar_4 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_204, Fresh_205, Ar_3, 0, Fresh_211, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_206 >= 2 /\ 0 >= Ar_2 + 1 /\ Fresh_212 >= Fresh_206 /\ Ar_3 >= Fresh_206 /\ Ar_4 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_114, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_113 >= 2 /\ R1 >= 1 /\ Fresh_114 >= 1 /\ Fresh_116 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_118, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_117 >= 2 /\ R1 >= 1 /\ Fresh_118 >= 1 /\ 0 >= Fresh_120 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_122, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_121 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_122 + 1 /\ Fresh_124 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_126, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_125 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_126 + 1 /\ 0 >= Fresh_128 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_130, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_129 >= 2 /\ 0 >= R1 + 1 /\ Fresh_130 >= 1 /\ Fresh_132 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_134, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_133 >= 2 /\ 0 >= R1 + 1 /\ Fresh_134 >= 1 /\ 0 >= Fresh_136 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_138, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_137 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_138 + 1 /\ Fresh_140 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_142, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_141 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_142 + 1 /\ 0 >= Fresh_144 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_8, Ar_11, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_6 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ Ar_11 >= 1 /\ Ar_13 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_5, Ar_11, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_3 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_59, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_58 >= 2 /\ Q1 >= Fresh_59 + 1 /\ 0 >= Fresh_59 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_62, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_61 >= 2 /\ Fresh_62 >= Q1 + 1 /\ Fresh_62 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_65, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_64 >= 2 /\ Fresh_65 >= Q1 + 1 /\ 0 >= Fresh_65 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_68, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_67 >= 2 /\ Q1 >= Fresh_68 + 1 /\ Fresh_68 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_71, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_70 >= 2 /\ Q1 >= Fresh_71 + 1 /\ 0 >= Fresh_71 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_74, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_73 >= 2 /\ Fresh_74 >= Q1 + 1 /\ Fresh_74 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_77, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_76 >= 2 /\ Fresh_77 >= Q1 + 1 /\ 0 >= Fresh_77 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_56, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_55 >= 2 /\ Q1 >= Fresh_56 + 1 /\ Fresh_56 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Fresh_49, Fresh_50, Ar_34)) [ Fresh_47 >= 2 /\ Ar_34 >= 0 /\ Ar_29 = Ar_27 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 3 Pol(f15) = 3 Pol(f16) = 0 Pol(f1) = 3 Pol(f14) = 2 Pol(f8) = 1 orients all transitions weakly and the transitions f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Fresh_49, Fresh_50, Ar_34)) [ Fresh_47 >= 2 /\ Ar_34 >= 0 /\ Ar_29 = Ar_27 ] f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_8, Ar_11, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_6 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ Ar_11 >= 1 /\ Ar_13 = 0 ] f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_5, Ar_11, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_3 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 ] f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_195, Fresh_196, Ar_3, 0, Fresh_202, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_197 >= 2 /\ Ar_2 >= 1 /\ Fresh_203 >= Fresh_197 /\ Ar_3 >= Fresh_197 /\ Ar_4 = 0 ] strictly and produces the following problem: 5: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Fresh_24, Fresh_25, Fresh_26, Ar_3, Ar_4, Fresh_32, 0, Fresh_34, Fresh_35, Fresh_36, Ar_34)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_27 /\ 0 >= X1' ] (Comp: 1, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f1(2, Fresh_42, Fresh_43, Ar_3, Ar_4, Fresh_44, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ Fresh_42 >= 2 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_10, Ar_3, Ar_4, Fresh_193, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_1 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: 3, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_195, Fresh_196, Ar_3, 0, Fresh_202, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_197 >= 2 /\ Ar_2 >= 1 /\ Fresh_203 >= Fresh_197 /\ Ar_3 >= Fresh_197 /\ Ar_4 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_204, Fresh_205, Ar_3, 0, Fresh_211, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_206 >= 2 /\ 0 >= Ar_2 + 1 /\ Fresh_212 >= Fresh_206 /\ Ar_3 >= Fresh_206 /\ Ar_4 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_114, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_113 >= 2 /\ R1 >= 1 /\ Fresh_114 >= 1 /\ Fresh_116 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_118, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_117 >= 2 /\ R1 >= 1 /\ Fresh_118 >= 1 /\ 0 >= Fresh_120 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_122, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_121 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_122 + 1 /\ Fresh_124 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_126, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_125 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_126 + 1 /\ 0 >= Fresh_128 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_130, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_129 >= 2 /\ 0 >= R1 + 1 /\ Fresh_130 >= 1 /\ Fresh_132 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_134, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_133 >= 2 /\ 0 >= R1 + 1 /\ Fresh_134 >= 1 /\ 0 >= Fresh_136 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_138, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_137 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_138 + 1 /\ Fresh_140 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_142, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_141 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_142 + 1 /\ 0 >= Fresh_144 + 1 ] (Comp: 3, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_8, Ar_11, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_6 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ Ar_11 >= 1 /\ Ar_13 = 0 ] (Comp: 3, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_5, Ar_11, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_3 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_59, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_58 >= 2 /\ Q1 >= Fresh_59 + 1 /\ 0 >= Fresh_59 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_62, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_61 >= 2 /\ Fresh_62 >= Q1 + 1 /\ Fresh_62 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_65, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_64 >= 2 /\ Fresh_65 >= Q1 + 1 /\ 0 >= Fresh_65 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_68, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_67 >= 2 /\ Q1 >= Fresh_68 + 1 /\ Fresh_68 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_71, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_70 >= 2 /\ Q1 >= Fresh_71 + 1 /\ 0 >= Fresh_71 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_74, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_73 >= 2 /\ Fresh_74 >= Q1 + 1 /\ Fresh_74 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_77, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_76 >= 2 /\ Fresh_77 >= Q1 + 1 /\ 0 >= Fresh_77 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_56, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_55 >= 2 /\ Q1 >= Fresh_56 + 1 /\ Fresh_56 >= 1 /\ Ar_29 = 0 ] (Comp: 3, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Fresh_49, Fresh_50, Ar_34)) [ Fresh_47 >= 2 /\ Ar_34 >= 0 /\ Ar_29 = Ar_27 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 1 Pol(f15) = 1 Pol(f16) = 0 Pol(f1) = 1 Pol(f14) = 0 Pol(f8) = 0 orients all transitions weakly and the transition f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_204, Fresh_205, Ar_3, 0, Fresh_211, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_206 >= 2 /\ 0 >= Ar_2 + 1 /\ Fresh_212 >= Fresh_206 /\ Ar_3 >= Fresh_206 /\ Ar_4 = 0 ] strictly and produces the following problem: 6: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Fresh_24, Fresh_25, Fresh_26, Ar_3, Ar_4, Fresh_32, 0, Fresh_34, Fresh_35, Fresh_36, Ar_34)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_27 /\ 0 >= X1' ] (Comp: 1, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f1(2, Fresh_42, Fresh_43, Ar_3, Ar_4, Fresh_44, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ Fresh_42 >= 2 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_10, Ar_3, Ar_4, Fresh_193, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_1 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: 3, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_195, Fresh_196, Ar_3, 0, Fresh_202, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_197 >= 2 /\ Ar_2 >= 1 /\ Fresh_203 >= Fresh_197 /\ Ar_3 >= Fresh_197 /\ Ar_4 = 0 ] (Comp: 1, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_204, Fresh_205, Ar_3, 0, Fresh_211, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_206 >= 2 /\ 0 >= Ar_2 + 1 /\ Fresh_212 >= Fresh_206 /\ Ar_3 >= Fresh_206 /\ Ar_4 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_114, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_113 >= 2 /\ R1 >= 1 /\ Fresh_114 >= 1 /\ Fresh_116 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_118, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_117 >= 2 /\ R1 >= 1 /\ Fresh_118 >= 1 /\ 0 >= Fresh_120 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_122, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_121 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_122 + 1 /\ Fresh_124 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_126, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_125 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_126 + 1 /\ 0 >= Fresh_128 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_130, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_129 >= 2 /\ 0 >= R1 + 1 /\ Fresh_130 >= 1 /\ Fresh_132 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_134, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_133 >= 2 /\ 0 >= R1 + 1 /\ Fresh_134 >= 1 /\ 0 >= Fresh_136 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_138, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_137 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_138 + 1 /\ Fresh_140 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_142, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_141 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_142 + 1 /\ 0 >= Fresh_144 + 1 ] (Comp: 3, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_8, Ar_11, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_6 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ Ar_11 >= 1 /\ Ar_13 = 0 ] (Comp: 3, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_5, Ar_11, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_3 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_59, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_58 >= 2 /\ Q1 >= Fresh_59 + 1 /\ 0 >= Fresh_59 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_62, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_61 >= 2 /\ Fresh_62 >= Q1 + 1 /\ Fresh_62 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_65, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_64 >= 2 /\ Fresh_65 >= Q1 + 1 /\ 0 >= Fresh_65 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_68, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_67 >= 2 /\ Q1 >= Fresh_68 + 1 /\ Fresh_68 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_71, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_70 >= 2 /\ Q1 >= Fresh_71 + 1 /\ 0 >= Fresh_71 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_74, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_73 >= 2 /\ Fresh_74 >= Q1 + 1 /\ Fresh_74 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_77, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_76 >= 2 /\ Fresh_77 >= Q1 + 1 /\ 0 >= Fresh_77 + 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_56, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_55 >= 2 /\ Q1 >= Fresh_56 + 1 /\ Fresh_56 >= 1 /\ Ar_29 = 0 ] (Comp: 3, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Fresh_49, Fresh_50, Ar_34)) [ Fresh_47 >= 2 /\ Ar_34 >= 0 /\ Ar_29 = Ar_27 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = V_11 + 1 Pol(f15) = V_11 + 1 Pol(f16) = V_11 Pol(f1) = V_11 + 1 Pol(f14) = V_11 + 1 Pol(f8) = V_11 + 1 orients all transitions weakly and the transitions f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_77, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_76 >= 2 /\ Fresh_77 >= Q1 + 1 /\ 0 >= Fresh_77 + 1 /\ Ar_29 = 0 ] f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_74, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_73 >= 2 /\ Fresh_74 >= Q1 + 1 /\ Fresh_74 >= 1 /\ Ar_29 = 0 ] f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_71, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_70 >= 2 /\ Q1 >= Fresh_71 + 1 /\ 0 >= Fresh_71 + 1 /\ Ar_29 = 0 ] f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_68, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_67 >= 2 /\ Q1 >= Fresh_68 + 1 /\ Fresh_68 >= 1 /\ Ar_29 = 0 ] f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_62, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_61 >= 2 /\ Fresh_62 >= Q1 + 1 /\ Fresh_62 >= 1 /\ Ar_29 = 0 ] f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_59, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_58 >= 2 /\ Q1 >= Fresh_59 + 1 /\ 0 >= Fresh_59 + 1 /\ Ar_29 = 0 ] f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_56, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_55 >= 2 /\ Q1 >= Fresh_56 + 1 /\ Fresh_56 >= 1 /\ Ar_29 = 0 ] strictly and produces the following problem: 7: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Fresh_24, Fresh_25, Fresh_26, Ar_3, Ar_4, Fresh_32, 0, Fresh_34, Fresh_35, Fresh_36, Ar_34)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_27 /\ 0 >= X1' ] (Comp: 1, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f1(2, Fresh_42, Fresh_43, Ar_3, Ar_4, Fresh_44, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ Fresh_42 >= 2 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_10, Ar_3, Ar_4, Fresh_193, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_1 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: 3, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_195, Fresh_196, Ar_3, 0, Fresh_202, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_197 >= 2 /\ Ar_2 >= 1 /\ Fresh_203 >= Fresh_197 /\ Ar_3 >= Fresh_197 /\ Ar_4 = 0 ] (Comp: 1, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_204, Fresh_205, Ar_3, 0, Fresh_211, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_206 >= 2 /\ 0 >= Ar_2 + 1 /\ Fresh_212 >= Fresh_206 /\ Ar_3 >= Fresh_206 /\ Ar_4 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_114, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_113 >= 2 /\ R1 >= 1 /\ Fresh_114 >= 1 /\ Fresh_116 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_118, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_117 >= 2 /\ R1 >= 1 /\ Fresh_118 >= 1 /\ 0 >= Fresh_120 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_122, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_121 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_122 + 1 /\ Fresh_124 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_126, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_125 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_126 + 1 /\ 0 >= Fresh_128 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_130, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_129 >= 2 /\ 0 >= R1 + 1 /\ Fresh_130 >= 1 /\ Fresh_132 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_134, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_133 >= 2 /\ 0 >= R1 + 1 /\ Fresh_134 >= 1 /\ 0 >= Fresh_136 + 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_138, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_137 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_138 + 1 /\ Fresh_140 >= 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_142, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_141 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_142 + 1 /\ 0 >= Fresh_144 + 1 ] (Comp: 3, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_8, Ar_11, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_6 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ Ar_11 >= 1 /\ Ar_13 = 0 ] (Comp: 3, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_5, Ar_11, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_3 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_59, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_58 >= 2 /\ Q1 >= Fresh_59 + 1 /\ 0 >= Fresh_59 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_62, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_61 >= 2 /\ Fresh_62 >= Q1 + 1 /\ Fresh_62 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_65, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_64 >= 2 /\ Fresh_65 >= Q1 + 1 /\ 0 >= Fresh_65 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_68, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_67 >= 2 /\ Q1 >= Fresh_68 + 1 /\ Fresh_68 >= 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_71, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_70 >= 2 /\ Q1 >= Fresh_71 + 1 /\ 0 >= Fresh_71 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_74, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_73 >= 2 /\ Fresh_74 >= Q1 + 1 /\ Fresh_74 >= 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_77, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_76 >= 2 /\ Fresh_77 >= Q1 + 1 /\ 0 >= Fresh_77 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_56, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_55 >= 2 /\ Q1 >= Fresh_56 + 1 /\ Fresh_56 >= 1 /\ Ar_29 = 0 ] (Comp: 3, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Fresh_49, Fresh_50, Ar_34)) [ Fresh_47 >= 2 /\ Ar_34 >= 0 /\ Ar_29 = Ar_27 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = V_4 + 1 Pol(f15) = V_4 + 1 Pol(f16) = V_4 Pol(f1) = V_4 + 1 Pol(f14) = V_4 + 1 Pol(f8) = V_4 + 1 orients all transitions weakly and the transitions f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_142, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_141 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_142 + 1 /\ 0 >= Fresh_144 + 1 ] f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_138, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_137 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_138 + 1 /\ Fresh_140 >= 1 ] f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_134, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_133 >= 2 /\ 0 >= R1 + 1 /\ Fresh_134 >= 1 /\ 0 >= Fresh_136 + 1 ] f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_130, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_129 >= 2 /\ 0 >= R1 + 1 /\ Fresh_130 >= 1 /\ Fresh_132 >= 1 ] f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_126, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_125 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_126 + 1 /\ 0 >= Fresh_128 + 1 ] f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_122, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_121 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_122 + 1 /\ Fresh_124 >= 1 ] f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_118, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_117 >= 2 /\ R1 >= 1 /\ Fresh_118 >= 1 /\ 0 >= Fresh_120 + 1 ] f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_114, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_113 >= 2 /\ R1 >= 1 /\ Fresh_114 >= 1 /\ Fresh_116 >= 1 ] strictly and produces the following problem: 8: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Fresh_24, Fresh_25, Fresh_26, Ar_3, Ar_4, Fresh_32, 0, Fresh_34, Fresh_35, Fresh_36, Ar_34)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_27 /\ 0 >= X1' ] (Comp: 1, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f1(2, Fresh_42, Fresh_43, Ar_3, Ar_4, Fresh_44, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ Fresh_42 >= 2 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_10, Ar_3, Ar_4, Fresh_193, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_1 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: 3, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_195, Fresh_196, Ar_3, 0, Fresh_202, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_197 >= 2 /\ Ar_2 >= 1 /\ Fresh_203 >= Fresh_197 /\ Ar_3 >= Fresh_197 /\ Ar_4 = 0 ] (Comp: 1, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_204, Fresh_205, Ar_3, 0, Fresh_211, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_206 >= 2 /\ 0 >= Ar_2 + 1 /\ Fresh_212 >= Fresh_206 /\ Ar_3 >= Fresh_206 /\ Ar_4 = 0 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_114, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_113 >= 2 /\ R1 >= 1 /\ Fresh_114 >= 1 /\ Fresh_116 >= 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_118, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_117 >= 2 /\ R1 >= 1 /\ Fresh_118 >= 1 /\ 0 >= Fresh_120 + 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_122, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_121 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_122 + 1 /\ Fresh_124 >= 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_126, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_125 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_126 + 1 /\ 0 >= Fresh_128 + 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_130, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_129 >= 2 /\ 0 >= R1 + 1 /\ Fresh_130 >= 1 /\ Fresh_132 >= 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_134, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_133 >= 2 /\ 0 >= R1 + 1 /\ Fresh_134 >= 1 /\ 0 >= Fresh_136 + 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_138, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_137 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_138 + 1 /\ Fresh_140 >= 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_142, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_141 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_142 + 1 /\ 0 >= Fresh_144 + 1 ] (Comp: 3, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_8, Ar_11, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_6 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ Ar_11 >= 1 /\ Ar_13 = 0 ] (Comp: 3, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_5, Ar_11, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_3 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_59, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_58 >= 2 /\ Q1 >= Fresh_59 + 1 /\ 0 >= Fresh_59 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_62, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_61 >= 2 /\ Fresh_62 >= Q1 + 1 /\ Fresh_62 >= 1 /\ Ar_29 = 0 ] (Comp: ?, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_65, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_64 >= 2 /\ Fresh_65 >= Q1 + 1 /\ 0 >= Fresh_65 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_68, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_67 >= 2 /\ Q1 >= Fresh_68 + 1 /\ Fresh_68 >= 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_71, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_70 >= 2 /\ Q1 >= Fresh_71 + 1 /\ 0 >= Fresh_71 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_74, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_73 >= 2 /\ Fresh_74 >= Q1 + 1 /\ Fresh_74 >= 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_77, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_76 >= 2 /\ Fresh_77 >= Q1 + 1 /\ 0 >= Fresh_77 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_56, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_55 >= 2 /\ Q1 >= Fresh_56 + 1 /\ Fresh_56 >= 1 /\ Ar_29 = 0 ] (Comp: 3, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Fresh_49, Fresh_50, Ar_34)) [ Fresh_47 >= 2 /\ Ar_34 >= 0 /\ Ar_29 = Ar_27 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = V_11 + 1 Pol(f15) = V_11 + 1 Pol(f16) = V_11 Pol(f1) = V_11 + 1 Pol(f14) = V_11 + 1 Pol(f8) = V_11 + 1 orients all transitions weakly and the transition f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_65, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_64 >= 2 /\ Fresh_65 >= Q1 + 1 /\ 0 >= Fresh_65 + 1 /\ Ar_29 = 0 ] strictly and produces the following problem: 9: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Fresh_24, Fresh_25, Fresh_26, Ar_3, Ar_4, Fresh_32, 0, Fresh_34, Fresh_35, Fresh_36, Ar_34)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_27 /\ 0 >= X1' ] (Comp: 1, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f1(2, Fresh_42, Fresh_43, Ar_3, Ar_4, Fresh_44, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ Fresh_42 >= 2 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_10, Ar_3, Ar_4, Fresh_193, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_1 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: 3, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_195, Fresh_196, Ar_3, 0, Fresh_202, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_197 >= 2 /\ Ar_2 >= 1 /\ Fresh_203 >= Fresh_197 /\ Ar_3 >= Fresh_197 /\ Ar_4 = 0 ] (Comp: 1, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_204, Fresh_205, Ar_3, 0, Fresh_211, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_206 >= 2 /\ 0 >= Ar_2 + 1 /\ Fresh_212 >= Fresh_206 /\ Ar_3 >= Fresh_206 /\ Ar_4 = 0 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_114, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_113 >= 2 /\ R1 >= 1 /\ Fresh_114 >= 1 /\ Fresh_116 >= 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_118, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_117 >= 2 /\ R1 >= 1 /\ Fresh_118 >= 1 /\ 0 >= Fresh_120 + 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_122, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_121 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_122 + 1 /\ Fresh_124 >= 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_126, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_125 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_126 + 1 /\ 0 >= Fresh_128 + 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_130, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_129 >= 2 /\ 0 >= R1 + 1 /\ Fresh_130 >= 1 /\ Fresh_132 >= 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_134, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_133 >= 2 /\ 0 >= R1 + 1 /\ Fresh_134 >= 1 /\ 0 >= Fresh_136 + 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_138, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_137 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_138 + 1 /\ Fresh_140 >= 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_142, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 >= 0 /\ Fresh_141 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_142 + 1 /\ 0 >= Fresh_144 + 1 ] (Comp: 3, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_8, Ar_11, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_6 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ Ar_11 >= 1 /\ Ar_13 = 0 ] (Comp: 3, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_5, Ar_11, 0, Ar_34)) [ Q1 >= 2 /\ Fresh_3 >= 2 /\ Ar_3 >= 0 /\ Ar_4 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_59, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_58 >= 2 /\ Q1 >= Fresh_59 + 1 /\ 0 >= Fresh_59 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_62, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_61 >= 2 /\ Fresh_62 >= Q1 + 1 /\ Fresh_62 >= 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_65, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_64 >= 2 /\ Fresh_65 >= Q1 + 1 /\ 0 >= Fresh_65 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_68, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_67 >= 2 /\ Q1 >= Fresh_68 + 1 /\ Fresh_68 >= 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_71, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_70 >= 2 /\ Q1 >= Fresh_71 + 1 /\ 0 >= Fresh_71 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_74, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_73 >= 2 /\ Fresh_74 >= Q1 + 1 /\ Fresh_74 >= 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_77, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_76 >= 2 /\ Fresh_77 >= Q1 + 1 /\ 0 >= Fresh_77 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_56, Ar_13, Ar_27, 0, Ar_34 - 1)) [ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_55 >= 2 /\ Q1 >= Fresh_56 + 1 /\ Fresh_56 >= 1 /\ Ar_29 = 0 ] (Comp: 3, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Fresh_49, Fresh_50, Ar_34)) [ Fresh_47 >= 2 /\ Ar_34 >= 0 /\ Ar_29 = Ar_27 ] start location: koat_start leaf cost: 0 Applied AI with 'oct' on problem 9 to obtain the following invariants: For symbol f1: X_2 - 2 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ -X_1 + X_2 >= 0 /\ X_1 - 2 >= 0 For symbol f14: X_5 >= 0 /\ X_4 + X_5 - 2 >= 0 /\ X_1 + X_5 - 2 >= 0 /\ X_1 - X_4 >= 0 /\ X_1 - 2 >= 0 For symbol f8: -X_11 + X_5 - 1 >= 0 /\ X_1 - X_4 >= 0 /\ X_4 >= 0 /\ X_10 + X_4 >= 0 /\ -X_10 + X_4 >= 0 /\ X_1 + X_4 - 2 >= 0 /\ -X_10 >= 0 /\ X_1 - X_10 - 2 >= 0 /\ X_10 >= 0 /\ X_1 + X_10 - 2 >= 0 /\ X_1 - 2 >= 0 This yielded the following problem: 10: T: (Comp: 3, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Fresh_49, Fresh_50, Ar_34)) [ -Ar_34 + Ar_4 - 1 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_3 >= 0 /\ Ar_29 + Ar_3 >= 0 /\ -Ar_29 + Ar_3 >= 0 /\ Ar_0 + Ar_3 - 2 >= 0 /\ -Ar_29 >= 0 /\ Ar_0 - Ar_29 - 2 >= 0 /\ Ar_29 >= 0 /\ Ar_0 + Ar_29 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ Fresh_47 >= 2 /\ Ar_34 >= 0 /\ Ar_29 = Ar_27 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_56, Ar_13, Ar_27, 0, Ar_34 - 1)) [ -Ar_34 + Ar_4 - 1 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_3 >= 0 /\ Ar_29 + Ar_3 >= 0 /\ -Ar_29 + Ar_3 >= 0 /\ Ar_0 + Ar_3 - 2 >= 0 /\ -Ar_29 >= 0 /\ Ar_0 - Ar_29 - 2 >= 0 /\ Ar_29 >= 0 /\ Ar_0 + Ar_29 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_55 >= 2 /\ Q1 >= Fresh_56 + 1 /\ Fresh_56 >= 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_77, Ar_13, Ar_27, 0, Ar_34 - 1)) [ -Ar_34 + Ar_4 - 1 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_3 >= 0 /\ Ar_29 + Ar_3 >= 0 /\ -Ar_29 + Ar_3 >= 0 /\ Ar_0 + Ar_3 - 2 >= 0 /\ -Ar_29 >= 0 /\ Ar_0 - Ar_29 - 2 >= 0 /\ Ar_29 >= 0 /\ Ar_0 + Ar_29 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_76 >= 2 /\ Fresh_77 >= Q1 + 1 /\ 0 >= Fresh_77 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_74, Ar_13, Ar_27, 0, Ar_34 - 1)) [ -Ar_34 + Ar_4 - 1 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_3 >= 0 /\ Ar_29 + Ar_3 >= 0 /\ -Ar_29 + Ar_3 >= 0 /\ Ar_0 + Ar_3 - 2 >= 0 /\ -Ar_29 >= 0 /\ Ar_0 - Ar_29 - 2 >= 0 /\ Ar_29 >= 0 /\ Ar_0 + Ar_29 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_73 >= 2 /\ Fresh_74 >= Q1 + 1 /\ Fresh_74 >= 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_71, Ar_13, Ar_27, 0, Ar_34 - 1)) [ -Ar_34 + Ar_4 - 1 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_3 >= 0 /\ Ar_29 + Ar_3 >= 0 /\ -Ar_29 + Ar_3 >= 0 /\ Ar_0 + Ar_3 - 2 >= 0 /\ -Ar_29 >= 0 /\ Ar_0 - Ar_29 - 2 >= 0 /\ Ar_29 >= 0 /\ Ar_0 + Ar_29 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_70 >= 2 /\ Q1 >= Fresh_71 + 1 /\ 0 >= Fresh_71 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_68, Ar_13, Ar_27, 0, Ar_34 - 1)) [ -Ar_34 + Ar_4 - 1 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_3 >= 0 /\ Ar_29 + Ar_3 >= 0 /\ -Ar_29 + Ar_3 >= 0 /\ Ar_0 + Ar_3 - 2 >= 0 /\ -Ar_29 >= 0 /\ Ar_0 - Ar_29 - 2 >= 0 /\ Ar_29 >= 0 /\ Ar_0 + Ar_29 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ Q1 >= Ar_27 + 1 /\ Ar_34 >= 0 /\ Fresh_67 >= 2 /\ Q1 >= Fresh_68 + 1 /\ Fresh_68 >= 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_65, Ar_13, Ar_27, 0, Ar_34 - 1)) [ -Ar_34 + Ar_4 - 1 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_3 >= 0 /\ Ar_29 + Ar_3 >= 0 /\ -Ar_29 + Ar_3 >= 0 /\ Ar_0 + Ar_3 - 2 >= 0 /\ -Ar_29 >= 0 /\ Ar_0 - Ar_29 - 2 >= 0 /\ Ar_29 >= 0 /\ Ar_0 + Ar_29 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_64 >= 2 /\ Fresh_65 >= Q1 + 1 /\ 0 >= Fresh_65 + 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_62, Ar_13, Ar_27, 0, Ar_34 - 1)) [ -Ar_34 + Ar_4 - 1 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_3 >= 0 /\ Ar_29 + Ar_3 >= 0 /\ -Ar_29 + Ar_3 >= 0 /\ Ar_0 + Ar_3 - 2 >= 0 /\ -Ar_29 >= 0 /\ Ar_0 - Ar_29 - 2 >= 0 /\ Ar_29 >= 0 /\ Ar_0 + Ar_29 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_61 >= 2 /\ Fresh_62 >= Q1 + 1 /\ Fresh_62 >= 1 /\ Ar_29 = 0 ] (Comp: Ar_34 + 1, Cost: 1) f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Fresh_59, Ar_13, Ar_27, 0, Ar_34 - 1)) [ -Ar_34 + Ar_4 - 1 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_3 >= 0 /\ Ar_29 + Ar_3 >= 0 /\ -Ar_29 + Ar_3 >= 0 /\ Ar_0 + Ar_3 - 2 >= 0 /\ -Ar_29 >= 0 /\ Ar_0 - Ar_29 - 2 >= 0 /\ Ar_29 >= 0 /\ Ar_0 + Ar_29 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_27 >= Q1 + 1 /\ Ar_34 >= 0 /\ Fresh_58 >= 2 /\ Q1 >= Fresh_59 + 1 /\ 0 >= Fresh_59 + 1 /\ Ar_29 = 0 ] (Comp: 3, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_5, Ar_11, 0, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 + Ar_4 - 2 >= 0 /\ Ar_0 + Ar_4 - 2 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_0 - 2 >= 0 /\ Q1 >= 2 /\ Fresh_3 >= 2 /\ Ar_3 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_13 = 0 ] (Comp: 3, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f8(Ar_0, Ar_1, Ar_2, Ar_3, Ar_34 + 1, Ar_10, Ar_11, Fresh_8, Ar_11, 0, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 + Ar_4 - 2 >= 0 /\ Ar_0 + Ar_4 - 2 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_0 - 2 >= 0 /\ Q1 >= 2 /\ Fresh_6 >= 2 /\ Ar_3 >= 0 /\ Ar_11 >= 1 /\ Ar_13 = 0 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_142, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 + Ar_4 - 2 >= 0 /\ Ar_0 + Ar_4 - 2 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_3 >= 0 /\ Fresh_141 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_142 + 1 /\ 0 >= Fresh_144 + 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_138, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 + Ar_4 - 2 >= 0 /\ Ar_0 + Ar_4 - 2 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_3 >= 0 /\ Fresh_137 >= 2 /\ 0 >= R1 + 1 /\ 0 >= Fresh_138 + 1 /\ Fresh_140 >= 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_134, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 + Ar_4 - 2 >= 0 /\ Ar_0 + Ar_4 - 2 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_3 >= 0 /\ Fresh_133 >= 2 /\ 0 >= R1 + 1 /\ Fresh_134 >= 1 /\ 0 >= Fresh_136 + 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_130, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 + Ar_4 - 2 >= 0 /\ Ar_0 + Ar_4 - 2 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_3 >= 0 /\ Fresh_129 >= 2 /\ 0 >= R1 + 1 /\ Fresh_130 >= 1 /\ Fresh_132 >= 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_126, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 + Ar_4 - 2 >= 0 /\ Ar_0 + Ar_4 - 2 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_3 >= 0 /\ Fresh_125 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_126 + 1 /\ 0 >= Fresh_128 + 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_122, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 + Ar_4 - 2 >= 0 /\ Ar_0 + Ar_4 - 2 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_3 >= 0 /\ Fresh_121 >= 2 /\ R1 >= 1 /\ 0 >= Fresh_122 + 1 /\ Fresh_124 >= 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_118, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 + Ar_4 - 2 >= 0 /\ Ar_0 + Ar_4 - 2 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_3 >= 0 /\ Fresh_117 >= 2 /\ R1 >= 1 /\ Fresh_118 >= 1 /\ 0 >= Fresh_120 + 1 ] (Comp: Ar_3 + 1, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Ar_3 - 1, Ar_4 + 1, Ar_10, Fresh_114, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_4 >= 0 /\ Ar_3 + Ar_4 - 2 >= 0 /\ Ar_0 + Ar_4 - 2 >= 0 /\ Ar_0 - Ar_3 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_3 >= 0 /\ Fresh_113 >= 2 /\ R1 >= 1 /\ Fresh_114 >= 1 /\ Fresh_116 >= 1 ] (Comp: 1, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_204, Fresh_205, Ar_3, 0, Fresh_211, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ -Ar_0 + Ar_1 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_206 >= 2 /\ 0 >= Ar_2 + 1 /\ Fresh_212 >= Fresh_206 /\ Ar_3 >= Fresh_206 /\ Ar_4 = 0 ] (Comp: 3, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f14(Ar_3, Fresh_195, Fresh_196, Ar_3, 0, Fresh_202, Ar_2, Ar_2, Ar_27, Ar_29, Ar_34)) [ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ -Ar_0 + Ar_1 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_0 >= Ar_1 /\ Ar_0 >= 0 /\ Fresh_197 >= 2 /\ Ar_2 >= 1 /\ Fresh_203 >= Fresh_197 /\ Ar_3 >= Fresh_197 /\ Ar_4 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f1(Ar_0 + 1, Ar_1, Ar_10, Ar_3, Ar_4, Fresh_193, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ -Ar_0 + Ar_1 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_1 >= Ar_0 + 1 /\ Ar_0 >= 0 ] (Comp: 1, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f1(2, Fresh_42, Fresh_43, Ar_3, Ar_4, Fresh_44, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ Fresh_42 >= 2 ] (Comp: 1, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f16(Fresh_24, Fresh_25, Fresh_26, Ar_3, Ar_4, Fresh_32, 0, Fresh_34, Fresh_35, Fresh_36, Ar_34)) [ 0 >= V1 /\ 0 >= W1 /\ 0 >= Fresh_27 /\ 0 >= X1' ] (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_10, Ar_11, Ar_13, Ar_27, Ar_29, Ar_34)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Complexity upper bound ? Time: 31.080 sec (SMT: 27.824 sec)