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