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