MAYBE Initial complexity problem: 1: T: (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f18(Ar_0, Ar_1, Fresh_122 - 1, 1, -1, Fresh_122 - 1, Ar_7, Ar_7, Fresh_123, Ar_7 + 1, Fresh_124, Fresh_125, Fresh_123, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_0 >= 2 /\ X2' >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_122 >= 1 /\ Ar_3 = 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f27(Ar_0, Ar_1, Ar_2, 1, Ar_4, Ar_5, Ar_6, Ar_6, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_0 >= 2 /\ 0 >= Ar_2 /\ Ar_7 >= 0 /\ Ar_6 = Ar_7 /\ Ar_3 = 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f18(Ar_0, Ar_1, Fresh_116 - 1, 2, Ar_4, Ar_5, Fresh_117, Fresh_117 - 1, Ar_8, Ar_9, Ar_10, Ar_11, Fresh_118, -1, Fresh_116 - 1, 2, Fresh_119, Fresh_120, Fresh_121, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Fresh_116 >= 1 /\ Ar_6 >= 0 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f27(Ar_0, Ar_1, Ar_2, Fresh_114, Ar_4, Ar_5, Ar_6, Fresh_115, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Fresh_114, Fresh_115, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_3 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_2 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f18(Ar_0, Ar_1, Ar_2 - 1, Ar_3 + 1, Ar_4, Ar_5, Ar_6, Ar_7 - 1, 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_3 + 1, Ar_7 - 1, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ Ar_21 >= 1 /\ Ar_7 >= 0 /\ Ar_2 = Ar_21 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f18(Ar_0, Ar_1, Fresh_112, 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, Fresh_113, Ar_3, Ar_7, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ 0 >= Ar_24 /\ Ar_7 >= 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f1(Ar_0, Ar_1 + 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_30, Fresh_111, Ar_30, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_1 >= 0 /\ Ar_28 >= Ar_1 + 1 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Fresh_110, Ar_34, Ar_34, Fresh_110 - 1, -1, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_32 >= 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f20(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, Fresh_103, Fresh_104, Ar_35, Ar_36, Fresh_105, Fresh_106, Fresh_107, Fresh_108, Fresh_109, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_32 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_34, Ar_34, Ar_35 - 1, Ar_36, 0, Ar_43, 0, Ar_43, Ar_41, 0, Ar_43, Ar_35 - 1, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_0 >= 2 /\ Ar_35 >= 0 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f20(Fresh_95, 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, Fresh_96, Fresh_97, Ar_35, Ar_36, Fresh_98, Fresh_99, Fresh_100, Fresh_101, Fresh_102, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_35 >= 0 /\ Ar_37 = Ar_34 ] (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, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_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_34, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Fresh_94, Fresh_94 - 1, -1, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_45 >= 0 ] (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, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f20(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, Fresh_87, Fresh_88, Ar_35, Ar_36, Fresh_89, Fresh_90, Fresh_91, Fresh_92, Fresh_93, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_45 >= 0 /\ Ar_37 = Ar_34 ] (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, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_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_34, Ar_34, Ar_35, Ar_36, 0, Ar_43, 0, Ar_43, Ar_41, 0, Ar_43, Ar_44, Ar_45, Ar_46 - 1, Ar_47, Ar_46 - 1, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_0 >= 2 /\ Ar_46 >= 0 /\ 0 >= Ar_2 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] (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, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f20(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, Fresh_80, Fresh_81, Ar_35, Ar_36, Fresh_82, Fresh_83, Fresh_84, Fresh_85, Fresh_86, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_46 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f18(Ar_0, Fresh_76, Fresh_77, 0, Ar_4, Ar_5, Ar_6, Ar_1, 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, Fresh_78, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_42, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_1, Fresh_76, Fresh_79, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Fresh_79 >= Ar_0 /\ Ar_0 >= 2 /\ Ar_7 >= Ar_0 /\ 0 >= Ar_2 /\ Ar_7 >= 0 /\ Ar_42 = Ar_43 /\ Ar_1 = Ar_7 /\ Ar_3 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f18(Ar_0, Fresh_65, Fresh_66, 0, 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, Fresh_67, Ar_26, Ar_27, Fresh_68, Fresh_69, Fresh_70, Fresh_71, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Fresh_72, Ar_29, Ar_29, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Fresh_65, Fresh_73, Fresh_74, Fresh_75, Ar_7, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ F3 >= Ar_0 /\ Fresh_73 >= Ar_0 /\ Ar_1 >= Ar_28 /\ Ar_0 >= 2 /\ Ar_7 >= Ar_0 /\ Ar_7 >= 0 /\ Ar_1 >= 0 /\ Ar_3 = 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, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f16(1, Ar_1, Fresh_62, 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, Fresh_63, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_42, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_56, Fresh_64, Fresh_64, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ 0 >= Ar_2 /\ Ar_42 = Ar_43 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_35 + 1, Ar_4, Ar_5, 0, 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_35, Ar_43, Ar_43, Ar_35, Ar_36, 0, Ar_43, 0, Ar_43, Ar_41, 0, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Fresh_61, -1, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Fresh_61 >= 0 /\ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_6 = 0 /\ Ar_3 = 1 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_35 + 1, 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_35, Ar_43, Ar_43, Ar_35, Ar_36, 0, Ar_43, 0, Ar_43, Ar_41, 0, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Fresh_59, -1, Fresh_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Fresh_59 >= 0 /\ Fresh_60 >= 0 /\ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_46 + 1, 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_43, Ar_43, Ar_35, Ar_36, 0, Ar_43, 0, Ar_43, Ar_41, 0, Ar_43, Ar_44, Ar_46, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Fresh_58, -1, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Fresh_58 >= 0 /\ Ar_0 >= 2 /\ 0 >= Ar_2 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f1(Fresh_52, 2, 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, Fresh_53, Ar_26, Ar_27, Fresh_52, Ar_30, Fresh_54, Ar_30, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_30, Ar_53, Ar_54, Ar_55, Fresh_55, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Fresh_56, 2, Fresh_57, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Fresh_52 >= 2 /\ Ar_30 = Ar_52 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f16(1, Fresh_39, Fresh_40, 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, Fresh_41, Ar_26, Ar_27, Fresh_42, Fresh_43, Fresh_44, Fresh_45, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Fresh_46, Ar_30, Ar_30, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Fresh_47, Fresh_48, Ar_54, Ar_55, Fresh_49, Fresh_49, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Fresh_50, Ar_64, Ar_65, Fresh_51, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ Ar_30 = Ar_52 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f20(Fresh_23, Fresh_24, 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, Fresh_25, Ar_26, Ar_27, Fresh_26, Fresh_27, Fresh_28, Fresh_29, Ar_32, Fresh_30, Fresh_31, Ar_35, Ar_36, Fresh_32, Fresh_33, Fresh_34, Fresh_35, Fresh_36, 0, 0, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Fresh_37, Fresh_38, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ 0 >= Fresh_23 ] (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, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f20(1, Ar_1, Fresh_11 - 1, 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, Fresh_12, Fresh_13, Ar_35, Ar_36, Fresh_14, Fresh_15, Fresh_16, Fresh_17, Fresh_18, 0, 0, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Fresh_19, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, -1, Fresh_11 - 1, Fresh_20, Fresh_21, Fresh_22, Fresh_19, Ar_73, Ar_74)) [ Ar_2 >= 1 /\ Fresh_11 >= 2 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 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, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f20(1, Ar_1, 0, 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, Fresh_0, Fresh_1, Ar_35, Ar_36, Fresh_2, Fresh_3, Fresh_4, Fresh_5, Fresh_6, 0, 0, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Fresh_7, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, -1, 0, Fresh_8, Fresh_9, Ar_71, Ar_72, Fresh_10, Fresh_7)) [ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 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, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48, Ar_49, Ar_50, Ar_51, Ar_52, Ar_53, Ar_54, Ar_55, Ar_56, Ar_57, Ar_58, Ar_59, Ar_60, Ar_61, Ar_62, Ar_63, Ar_64, Ar_65, Ar_66, Ar_67, Ar_68, Ar_69, Ar_70, Ar_71, Ar_72, Ar_73, Ar_74)) [ 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_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52]. We thus obtain the following problem: 2: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ 0 <= 0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, 0, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Fresh_1, Ar_35, Fresh_2, Fresh_3, Fresh_4, Fresh_5, 0, 0, Ar_45, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, Fresh_11 - 1, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Fresh_13, Ar_35, Fresh_14, Fresh_15, Fresh_16, Fresh_17, 0, 0, Ar_45, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Fresh_11 >= 2 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f20(Fresh_23, Fresh_24, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Fresh_26, Fresh_27, Fresh_28, Ar_32, Fresh_31, Ar_35, Fresh_32, Fresh_33, Fresh_34, Fresh_35, 0, 0, Ar_45, Ar_46, Fresh_37)) [ 0 >= Fresh_23 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f16(1, Fresh_39, Fresh_40, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Fresh_42, Fresh_43, Fresh_44, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_30, Ar_30, Ar_45, Ar_46, Fresh_47)) [ Ar_30 = Ar_52 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f1(Fresh_52, 2, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Fresh_52, Ar_30, Fresh_54, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_30)) [ Fresh_52 >= 2 /\ Ar_30 = Ar_52 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_46 + 1, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_46, Ar_52)) [ Fresh_58 >= 0 /\ Ar_0 >= 2 /\ 0 >= Ar_2 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_35 + 1, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_35, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_45, Ar_46, Ar_52)) [ Fresh_59 >= 0 /\ Fresh_60 >= 0 /\ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_35 + 1, 0, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_35, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_45, Ar_46, Ar_52)) [ Fresh_61 >= 0 /\ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_6 = 0 /\ Ar_3 = 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f16(1, Ar_1, Fresh_62, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_42, Ar_45, Ar_46, Ar_52)) [ 0 >= Ar_2 /\ Ar_42 = Ar_43 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Fresh_65, Fresh_66, 0, Ar_6, Ar_7, Ar_21, Ar_24, Fresh_68, Fresh_69, Fresh_70, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_29, Ar_29, Ar_45, Ar_46, Fresh_74)) [ F3 >= Ar_0 /\ Fresh_73 >= Ar_0 /\ Ar_1 >= Ar_28 /\ Ar_0 >= 2 /\ Ar_7 >= Ar_0 /\ Ar_7 >= 0 /\ Ar_1 >= 0 /\ Ar_3 = 0 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Fresh_76, Fresh_77, 0, Ar_6, Ar_1, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_42, Ar_45, Ar_46, Ar_52)) [ Fresh_79 >= Ar_0 /\ Ar_0 >= 2 /\ Ar_7 >= Ar_0 /\ 0 >= Ar_2 /\ Ar_7 >= 0 /\ Ar_42 = Ar_43 /\ Ar_1 = Ar_7 /\ Ar_3 = 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f20(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Fresh_81, Ar_35, Fresh_82, Fresh_83, Fresh_84, Fresh_85, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_46 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_45, Ar_46 - 1, Ar_52)) [ Ar_0 >= 2 /\ Ar_46 >= 0 /\ 0 >= Ar_2 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] (Comp: ?, Cost: 1) f12(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f20(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Fresh_88, Ar_35, Fresh_89, Fresh_90, Fresh_91, Fresh_92, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_45 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f12(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Fresh_94, Fresh_94 - 1, Ar_52)) [ Ar_45 >= 0 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f20(Fresh_95, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Fresh_97, Ar_35, Fresh_98, Fresh_99, Fresh_100, Fresh_101, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_35 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35 - 1, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_35 >= 0 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f20(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Fresh_104, Ar_35, Fresh_105, Fresh_106, Fresh_107, Fresh_108, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_32 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_110, Ar_34, Fresh_110 - 1, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_32 >= 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_30, Fresh_111, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_1 >= 0 /\ Ar_28 >= Ar_1 + 1 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Fresh_112, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ 0 >= Ar_24 /\ Ar_7 >= 0 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Ar_2 - 1, Ar_3 + 1, Ar_6, Ar_7 - 1, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ Ar_21 >= 1 /\ Ar_7 >= 0 /\ Ar_2 = Ar_21 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f27(Ar_0, Ar_1, Ar_2, Fresh_114, Ar_6, Fresh_115, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_3 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_2 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Fresh_116 - 1, 2, Fresh_117, Fresh_117 - 1, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Fresh_116 >= 1 /\ Ar_6 >= 0 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f27(Ar_0, Ar_1, Ar_2, 1, Ar_6, Ar_6, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ 0 >= Ar_2 /\ Ar_7 >= 0 /\ Ar_6 = Ar_7 /\ Ar_3 = 1 ] (Comp: ?, Cost: 1) f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Fresh_122 - 1, 1, Ar_7, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ X2' >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_122 >= 1 /\ Ar_3 = 1 ] start location: koat_start leaf cost: 0 Testing for reachability in the complexity graph removes the following transitions from problem 2: f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_35 + 1, 0, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_35, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_45, Ar_46, Ar_52)) [ Fresh_61 >= 0 /\ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_6 = 0 /\ Ar_3 = 1 ] f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Fresh_76, Fresh_77, 0, Ar_6, Ar_1, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_42, Ar_45, Ar_46, Ar_52)) [ Fresh_79 >= Ar_0 /\ Ar_0 >= 2 /\ Ar_7 >= Ar_0 /\ 0 >= Ar_2 /\ Ar_7 >= 0 /\ Ar_42 = Ar_43 /\ Ar_1 = Ar_7 /\ Ar_3 = 0 ] f12(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f20(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Fresh_88, Ar_35, Fresh_89, Fresh_90, Fresh_91, Fresh_92, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_45 >= 0 /\ Ar_37 = Ar_34 ] f12(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Fresh_94, Fresh_94 - 1, Ar_52)) [ Ar_45 >= 0 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f20(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Fresh_104, Ar_35, Fresh_105, Fresh_106, Fresh_107, Fresh_108, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_32 >= 0 /\ Ar_37 = Ar_34 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_110, Ar_34, Fresh_110 - 1, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_32 >= 0 ] f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Fresh_116 - 1, 2, Fresh_117, Fresh_117 - 1, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Fresh_116 >= 1 /\ Ar_6 >= 0 ] f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f27(Ar_0, Ar_1, Ar_2, 1, Ar_6, Ar_6, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ 0 >= Ar_2 /\ Ar_7 >= 0 /\ Ar_6 = Ar_7 /\ Ar_3 = 1 ] f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Fresh_122 - 1, 1, Ar_7, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ X2' >= Ar_0 /\ Ar_1 >= 0 /\ Ar_2 >= 1 /\ Fresh_122 >= 1 /\ Ar_3 = 1 ] We thus obtain the following problem: 3: T: (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_45, Ar_46 - 1, Ar_52)) [ Ar_0 >= 2 /\ Ar_46 >= 0 /\ 0 >= Ar_2 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f20(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Fresh_81, Ar_35, Fresh_82, Fresh_83, Fresh_84, Fresh_85, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_46 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Fresh_112, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ 0 >= Ar_24 /\ Ar_7 >= 0 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_46 + 1, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_46, Ar_52)) [ Fresh_58 >= 0 /\ Ar_0 >= 2 /\ 0 >= Ar_2 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35 - 1, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_35 >= 0 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f20(Fresh_95, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Fresh_97, Ar_35, Fresh_98, Fresh_99, Fresh_100, Fresh_101, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_35 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f27(Ar_0, Ar_1, Ar_2, Fresh_114, Ar_6, Fresh_115, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_3 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_2 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Ar_2 - 1, Ar_3 + 1, Ar_6, Ar_7 - 1, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ Ar_21 >= 1 /\ Ar_7 >= 0 /\ Ar_2 = Ar_21 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_35 + 1, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_35, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_45, Ar_46, Ar_52)) [ Fresh_59 >= 0 /\ Fresh_60 >= 0 /\ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_30, Fresh_111, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ Ar_1 >= 0 /\ Ar_28 >= Ar_1 + 1 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Fresh_65, Fresh_66, 0, Ar_6, Ar_7, Ar_21, Ar_24, Fresh_68, Fresh_69, Fresh_70, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_29, Ar_29, Ar_45, Ar_46, Fresh_74)) [ F3 >= Ar_0 /\ Fresh_73 >= Ar_0 /\ Ar_1 >= Ar_28 /\ Ar_0 >= 2 /\ Ar_7 >= Ar_0 /\ Ar_7 >= 0 /\ Ar_1 >= 0 /\ Ar_3 = 0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f16(1, Ar_1, Fresh_62, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_42, Ar_45, Ar_46, Ar_52)) [ 0 >= Ar_2 /\ Ar_42 = Ar_43 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, Fresh_11 - 1, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Fresh_13, Ar_35, Fresh_14, Fresh_15, Fresh_16, Fresh_17, 0, 0, Ar_45, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Fresh_11 >= 2 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, 0, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Fresh_1, Ar_35, Fresh_2, Fresh_3, Fresh_4, Fresh_5, 0, 0, Ar_45, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f1(Fresh_52, 2, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Fresh_52, Ar_30, Fresh_54, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_30)) [ Fresh_52 >= 2 /\ Ar_30 = Ar_52 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f16(1, Fresh_39, Fresh_40, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Fresh_42, Fresh_43, Fresh_44, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_30, Ar_30, Ar_45, Ar_46, Fresh_47)) [ Ar_30 = Ar_52 ] (Comp: ?, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f20(Fresh_23, Fresh_24, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Fresh_26, Fresh_27, Fresh_28, Ar_32, Fresh_31, Ar_35, Fresh_32, Fresh_33, Fresh_34, Fresh_35, 0, 0, Ar_45, Ar_46, Fresh_37)) [ 0 >= Fresh_23 ] (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_6, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_32, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_45, Ar_46, Ar_52)) [ 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_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_23, Fresh_24, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_26, Fresh_27, Fresh_28, Fresh_31, Ar_35, Fresh_32, Fresh_33, Fresh_34, Fresh_35, 0, 0, Ar_46, Fresh_37)) [ 0 >= Fresh_23 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f16(1, Fresh_39, Fresh_40, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_42, Fresh_43, Fresh_44, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_30, Ar_30, Ar_46, Fresh_47)) [ Ar_30 = Ar_52 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f1(Fresh_52, 2, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_52, Ar_30, Fresh_54, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_30)) [ Fresh_52 >= 2 /\ Ar_30 = Ar_52 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, 0, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_1, Ar_35, Fresh_2, Fresh_3, Fresh_4, Fresh_5, 0, 0, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, Fresh_11 - 1, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_13, Ar_35, Fresh_14, Fresh_15, Fresh_16, Fresh_17, 0, 0, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Fresh_11 >= 2 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f16(1, Ar_1, Fresh_62, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_42, Ar_46, Ar_52)) [ 0 >= Ar_2 /\ Ar_42 = Ar_43 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Fresh_65, Fresh_66, 0, Ar_7, Ar_21, Ar_24, Fresh_68, Fresh_69, Fresh_70, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_29, Ar_29, Ar_46, Fresh_74)) [ F3 >= Ar_0 /\ Fresh_73 >= Ar_0 /\ Ar_1 >= Ar_28 /\ Ar_0 >= 2 /\ Ar_7 >= Ar_0 /\ Ar_7 >= 0 /\ Ar_1 >= 0 /\ Ar_3 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_30, Fresh_111, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_1 >= 0 /\ Ar_28 >= Ar_1 + 1 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_35 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Fresh_59 >= 0 /\ Fresh_60 >= 0 /\ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Ar_2 - 1, Ar_3 + 1, Ar_7 - 1, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ Ar_21 >= 1 /\ Ar_7 >= 0 /\ Ar_2 = Ar_21 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f27(Ar_0, Ar_1, Ar_2, Fresh_114, Fresh_115, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_3 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_2 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_95, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_97, Ar_35, Fresh_98, Fresh_99, Fresh_100, Fresh_101, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_35 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35 - 1, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_35 >= 0 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_46 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Fresh_58 >= 0 /\ Ar_0 >= 2 /\ 0 >= Ar_2 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Fresh_112, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ 0 >= Ar_24 /\ Ar_7 >= 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_81, Ar_35, Fresh_82, Fresh_83, Fresh_84, Fresh_85, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_46 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46 - 1, Ar_52)) [ Ar_0 >= 2 /\ Ar_46 >= 0 /\ 0 >= Ar_2 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 3 Pol(f19) = 3 Pol(f20) = 0 Pol(f16) = 1 Pol(f1) = 3 Pol(f18) = 2 Pol(f11) = 1 Pol(f27) = 2 Pol(f13) = 1 orients all transitions weakly and the transitions f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_46 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Fresh_58 >= 0 /\ Ar_0 >= 2 /\ 0 >= Ar_2 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_35 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Fresh_59 >= 0 /\ Fresh_60 >= 0 /\ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, Fresh_11 - 1, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_13, Ar_35, Fresh_14, Fresh_15, Fresh_16, Fresh_17, 0, 0, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Fresh_11 >= 2 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_81, Ar_35, Fresh_82, Fresh_83, Fresh_84, Fresh_85, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_46 >= 0 /\ Ar_37 = Ar_34 ] f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_95, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_97, Ar_35, Fresh_98, Fresh_99, Fresh_100, Fresh_101, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_35 >= 0 /\ Ar_37 = Ar_34 ] strictly and produces the following problem: 5: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_23, Fresh_24, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_26, Fresh_27, Fresh_28, Fresh_31, Ar_35, Fresh_32, Fresh_33, Fresh_34, Fresh_35, 0, 0, Ar_46, Fresh_37)) [ 0 >= Fresh_23 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f16(1, Fresh_39, Fresh_40, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_42, Fresh_43, Fresh_44, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_30, Ar_30, Ar_46, Fresh_47)) [ Ar_30 = Ar_52 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f1(Fresh_52, 2, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_52, Ar_30, Fresh_54, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_30)) [ Fresh_52 >= 2 /\ Ar_30 = Ar_52 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, 0, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_1, Ar_35, Fresh_2, Fresh_3, Fresh_4, Fresh_5, 0, 0, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: 3, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, Fresh_11 - 1, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_13, Ar_35, Fresh_14, Fresh_15, Fresh_16, Fresh_17, 0, 0, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Fresh_11 >= 2 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f16(1, Ar_1, Fresh_62, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_42, Ar_46, Ar_52)) [ 0 >= Ar_2 /\ Ar_42 = Ar_43 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Fresh_65, Fresh_66, 0, Ar_7, Ar_21, Ar_24, Fresh_68, Fresh_69, Fresh_70, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_29, Ar_29, Ar_46, Fresh_74)) [ F3 >= Ar_0 /\ Fresh_73 >= Ar_0 /\ Ar_1 >= Ar_28 /\ Ar_0 >= 2 /\ Ar_7 >= Ar_0 /\ Ar_7 >= 0 /\ Ar_1 >= 0 /\ Ar_3 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_30, Fresh_111, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_1 >= 0 /\ Ar_28 >= Ar_1 + 1 ] (Comp: 3, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_35 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Fresh_59 >= 0 /\ Fresh_60 >= 0 /\ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Ar_2 - 1, Ar_3 + 1, Ar_7 - 1, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ Ar_21 >= 1 /\ Ar_7 >= 0 /\ Ar_2 = Ar_21 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f27(Ar_0, Ar_1, Ar_2, Fresh_114, Fresh_115, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_3 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_2 ] (Comp: 3, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_95, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_97, Ar_35, Fresh_98, Fresh_99, Fresh_100, Fresh_101, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_35 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35 - 1, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_35 >= 0 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] (Comp: 3, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_46 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Fresh_58 >= 0 /\ Ar_0 >= 2 /\ 0 >= Ar_2 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Fresh_112, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ 0 >= Ar_24 /\ Ar_7 >= 0 ] (Comp: 3, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_81, Ar_35, Fresh_82, Fresh_83, Fresh_84, Fresh_85, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_46 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46 - 1, Ar_52)) [ Ar_0 >= 2 /\ Ar_46 >= 0 /\ 0 >= Ar_2 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 1 Pol(f19) = 1 Pol(f20) = 0 Pol(f16) = 1 Pol(f1) = 1 Pol(f18) = 0 Pol(f11) = 0 Pol(f27) = 0 Pol(f13) = 0 orients all transitions weakly and the transition f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, 0, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_1, Ar_35, Fresh_2, Fresh_3, Fresh_4, Fresh_5, 0, 0, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] strictly and produces the following problem: 6: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_23, Fresh_24, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_26, Fresh_27, Fresh_28, Fresh_31, Ar_35, Fresh_32, Fresh_33, Fresh_34, Fresh_35, 0, 0, Ar_46, Fresh_37)) [ 0 >= Fresh_23 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f16(1, Fresh_39, Fresh_40, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_42, Fresh_43, Fresh_44, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_30, Ar_30, Ar_46, Fresh_47)) [ Ar_30 = Ar_52 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f1(Fresh_52, 2, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_52, Ar_30, Fresh_54, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_30)) [ Fresh_52 >= 2 /\ Ar_30 = Ar_52 ] (Comp: 1, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, 0, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_1, Ar_35, Fresh_2, Fresh_3, Fresh_4, Fresh_5, 0, 0, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: 3, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, Fresh_11 - 1, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_13, Ar_35, Fresh_14, Fresh_15, Fresh_16, Fresh_17, 0, 0, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Fresh_11 >= 2 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f16(1, Ar_1, Fresh_62, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_42, Ar_46, Ar_52)) [ 0 >= Ar_2 /\ Ar_42 = Ar_43 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Fresh_65, Fresh_66, 0, Ar_7, Ar_21, Ar_24, Fresh_68, Fresh_69, Fresh_70, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_29, Ar_29, Ar_46, Fresh_74)) [ F3 >= Ar_0 /\ Fresh_73 >= Ar_0 /\ Ar_1 >= Ar_28 /\ Ar_0 >= 2 /\ Ar_7 >= Ar_0 /\ Ar_7 >= 0 /\ Ar_1 >= 0 /\ Ar_3 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_30, Fresh_111, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_1 >= 0 /\ Ar_28 >= Ar_1 + 1 ] (Comp: 3, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_35 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Fresh_59 >= 0 /\ Fresh_60 >= 0 /\ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Ar_2 - 1, Ar_3 + 1, Ar_7 - 1, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ Ar_21 >= 1 /\ Ar_7 >= 0 /\ Ar_2 = Ar_21 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f27(Ar_0, Ar_1, Ar_2, Fresh_114, Fresh_115, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_3 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_2 ] (Comp: 3, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_95, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_97, Ar_35, Fresh_98, Fresh_99, Fresh_100, Fresh_101, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_35 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35 - 1, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_35 >= 0 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] (Comp: 3, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_46 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Fresh_58 >= 0 /\ Ar_0 >= 2 /\ 0 >= Ar_2 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Fresh_112, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ 0 >= Ar_24 /\ Ar_7 >= 0 ] (Comp: 3, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_81, Ar_35, Fresh_82, Fresh_83, Fresh_84, Fresh_85, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_46 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46 - 1, Ar_52)) [ Ar_0 >= 2 /\ Ar_46 >= 0 /\ 0 >= Ar_2 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 1 Pol(f19) = 1 Pol(f20) = 0 Pol(f16) = 0 Pol(f1) = 1 Pol(f18) = 0 Pol(f11) = 0 Pol(f27) = 0 Pol(f13) = 0 orients all transitions weakly and the transition f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Fresh_65, Fresh_66, 0, Ar_7, Ar_21, Ar_24, Fresh_68, Fresh_69, Fresh_70, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_29, Ar_29, Ar_46, Fresh_74)) [ F3 >= Ar_0 /\ Fresh_73 >= Ar_0 /\ Ar_1 >= Ar_28 /\ Ar_0 >= 2 /\ Ar_7 >= Ar_0 /\ Ar_7 >= 0 /\ Ar_1 >= 0 /\ Ar_3 = 0 ] strictly and produces the following problem: 7: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_23, Fresh_24, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_26, Fresh_27, Fresh_28, Fresh_31, Ar_35, Fresh_32, Fresh_33, Fresh_34, Fresh_35, 0, 0, Ar_46, Fresh_37)) [ 0 >= Fresh_23 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f16(1, Fresh_39, Fresh_40, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_42, Fresh_43, Fresh_44, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_30, Ar_30, Ar_46, Fresh_47)) [ Ar_30 = Ar_52 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f1(Fresh_52, 2, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_52, Ar_30, Fresh_54, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_30)) [ Fresh_52 >= 2 /\ Ar_30 = Ar_52 ] (Comp: 1, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, 0, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_1, Ar_35, Fresh_2, Fresh_3, Fresh_4, Fresh_5, 0, 0, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: 3, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, Fresh_11 - 1, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_13, Ar_35, Fresh_14, Fresh_15, Fresh_16, Fresh_17, 0, 0, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Fresh_11 >= 2 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f16(1, Ar_1, Fresh_62, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_42, Ar_46, Ar_52)) [ 0 >= Ar_2 /\ Ar_42 = Ar_43 /\ Ar_0 = 1 ] (Comp: 1, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Fresh_65, Fresh_66, 0, Ar_7, Ar_21, Ar_24, Fresh_68, Fresh_69, Fresh_70, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_29, Ar_29, Ar_46, Fresh_74)) [ F3 >= Ar_0 /\ Fresh_73 >= Ar_0 /\ Ar_1 >= Ar_28 /\ Ar_0 >= 2 /\ Ar_7 >= Ar_0 /\ Ar_7 >= 0 /\ Ar_1 >= 0 /\ Ar_3 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_30, Fresh_111, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_1 >= 0 /\ Ar_28 >= Ar_1 + 1 ] (Comp: 3, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_35 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Fresh_59 >= 0 /\ Fresh_60 >= 0 /\ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Ar_2 - 1, Ar_3 + 1, Ar_7 - 1, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ Ar_21 >= 1 /\ Ar_7 >= 0 /\ Ar_2 = Ar_21 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f27(Ar_0, Ar_1, Ar_2, Fresh_114, Fresh_115, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_3 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_2 ] (Comp: 3, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_95, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_97, Ar_35, Fresh_98, Fresh_99, Fresh_100, Fresh_101, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_35 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35 - 1, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_35 >= 0 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] (Comp: 3, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_46 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Fresh_58 >= 0 /\ Ar_0 >= 2 /\ 0 >= Ar_2 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Fresh_112, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ 0 >= Ar_24 /\ Ar_7 >= 0 ] (Comp: 3, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_81, Ar_35, Fresh_82, Fresh_83, Fresh_84, Fresh_85, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_46 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46 - 1, Ar_52)) [ Ar_0 >= 2 /\ Ar_46 >= 0 /\ 0 >= Ar_2 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = V_19 + 2 Pol(f19) = V_19 + 2 Pol(f20) = V_19 Pol(f16) = V_19 Pol(f1) = V_19 + 2 Pol(f18) = V_19 + 2 Pol(f11) = V_19 Pol(f27) = V_19 + 2 Pol(f13) = V_19 + 1 orients all transitions weakly and the transition f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46 - 1, Ar_52)) [ Ar_0 >= 2 /\ Ar_46 >= 0 /\ 0 >= Ar_2 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] strictly and produces the following problem: 8: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_23, Fresh_24, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_26, Fresh_27, Fresh_28, Fresh_31, Ar_35, Fresh_32, Fresh_33, Fresh_34, Fresh_35, 0, 0, Ar_46, Fresh_37)) [ 0 >= Fresh_23 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f16(1, Fresh_39, Fresh_40, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_42, Fresh_43, Fresh_44, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_30, Ar_30, Ar_46, Fresh_47)) [ Ar_30 = Ar_52 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f1(Fresh_52, 2, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_52, Ar_30, Fresh_54, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_30)) [ Fresh_52 >= 2 /\ Ar_30 = Ar_52 ] (Comp: 1, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, 0, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_1, Ar_35, Fresh_2, Fresh_3, Fresh_4, Fresh_5, 0, 0, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: 3, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, Fresh_11 - 1, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_13, Ar_35, Fresh_14, Fresh_15, Fresh_16, Fresh_17, 0, 0, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Fresh_11 >= 2 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f16(1, Ar_1, Fresh_62, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_42, Ar_46, Ar_52)) [ 0 >= Ar_2 /\ Ar_42 = Ar_43 /\ Ar_0 = 1 ] (Comp: 1, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Fresh_65, Fresh_66, 0, Ar_7, Ar_21, Ar_24, Fresh_68, Fresh_69, Fresh_70, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_29, Ar_29, Ar_46, Fresh_74)) [ F3 >= Ar_0 /\ Fresh_73 >= Ar_0 /\ Ar_1 >= Ar_28 /\ Ar_0 >= 2 /\ Ar_7 >= Ar_0 /\ Ar_7 >= 0 /\ Ar_1 >= 0 /\ Ar_3 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_30, Fresh_111, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_1 >= 0 /\ Ar_28 >= Ar_1 + 1 ] (Comp: 3, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_35 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Fresh_59 >= 0 /\ Fresh_60 >= 0 /\ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Ar_2 - 1, Ar_3 + 1, Ar_7 - 1, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ Ar_21 >= 1 /\ Ar_7 >= 0 /\ Ar_2 = Ar_21 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f27(Ar_0, Ar_1, Ar_2, Fresh_114, Fresh_115, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_3 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_2 ] (Comp: 3, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_95, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_97, Ar_35, Fresh_98, Fresh_99, Fresh_100, Fresh_101, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_35 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35 - 1, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_35 >= 0 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] (Comp: 3, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_46 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Fresh_58 >= 0 /\ Ar_0 >= 2 /\ 0 >= Ar_2 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Fresh_112, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ 0 >= Ar_24 /\ Ar_7 >= 0 ] (Comp: 3, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_81, Ar_35, Fresh_82, Fresh_83, Fresh_84, Fresh_85, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_46 >= 0 /\ Ar_37 = Ar_34 ] (Comp: Ar_46 + 2, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46 - 1, Ar_52)) [ Ar_0 >= 2 /\ Ar_46 >= 0 /\ 0 >= Ar_2 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = V_12 + 2 Pol(f19) = V_12 + 2 Pol(f20) = V_12 + 2 Pol(f16) = V_12 + 2 Pol(f1) = V_12 + 2 Pol(f18) = V_12 + 2 Pol(f11) = V_12 + 2 Pol(f27) = V_12 + 2 Pol(f13) = V_12 + 2 orients all transitions weakly and the transition f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35 - 1, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_35 >= 0 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] strictly and produces the following problem: 9: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_23, Fresh_24, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_26, Fresh_27, Fresh_28, Fresh_31, Ar_35, Fresh_32, Fresh_33, Fresh_34, Fresh_35, 0, 0, Ar_46, Fresh_37)) [ 0 >= Fresh_23 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f16(1, Fresh_39, Fresh_40, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_42, Fresh_43, Fresh_44, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_30, Ar_30, Ar_46, Fresh_47)) [ Ar_30 = Ar_52 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f1(Fresh_52, 2, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_52, Ar_30, Fresh_54, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_30)) [ Fresh_52 >= 2 /\ Ar_30 = Ar_52 ] (Comp: 1, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, 0, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_1, Ar_35, Fresh_2, Fresh_3, Fresh_4, Fresh_5, 0, 0, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: 3, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, Fresh_11 - 1, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_13, Ar_35, Fresh_14, Fresh_15, Fresh_16, Fresh_17, 0, 0, Ar_46, Ar_52)) [ Ar_2 >= 1 /\ Fresh_11 >= 2 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f16(1, Ar_1, Fresh_62, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_42, Ar_46, Ar_52)) [ 0 >= Ar_2 /\ Ar_42 = Ar_43 /\ Ar_0 = 1 ] (Comp: 1, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Fresh_65, Fresh_66, 0, Ar_7, Ar_21, Ar_24, Fresh_68, Fresh_69, Fresh_70, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_29, Ar_29, Ar_46, Fresh_74)) [ F3 >= Ar_0 /\ Fresh_73 >= Ar_0 /\ Ar_1 >= Ar_28 /\ Ar_0 >= 2 /\ Ar_7 >= Ar_0 /\ Ar_7 >= 0 /\ Ar_1 >= 0 /\ Ar_3 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_30, Fresh_111, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_1 >= 0 /\ Ar_28 >= Ar_1 + 1 ] (Comp: 3, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_35 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Fresh_59 >= 0 /\ Fresh_60 >= 0 /\ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Ar_2 - 1, Ar_3 + 1, Ar_7 - 1, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ Ar_21 >= 1 /\ Ar_7 >= 0 /\ Ar_2 = Ar_21 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f27(Ar_0, Ar_1, Ar_2, Fresh_114, Fresh_115, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_3 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_2 ] (Comp: 3, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_95, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_97, Ar_35, Fresh_98, Fresh_99, Fresh_100, Fresh_101, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_35 >= 0 /\ Ar_37 = Ar_34 ] (Comp: Ar_35 + 2, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35 - 1, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_35 >= 0 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] (Comp: 3, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_46 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Fresh_58 >= 0 /\ Ar_0 >= 2 /\ 0 >= Ar_2 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Fresh_112, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_0 >= 2 /\ Ar_3 >= 0 /\ 0 >= Ar_24 /\ Ar_7 >= 0 ] (Comp: 3, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_81, Ar_35, Fresh_82, Fresh_83, Fresh_84, Fresh_85, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_46 >= 0 /\ Ar_37 = Ar_34 ] (Comp: Ar_46 + 2, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46 - 1, Ar_52)) [ Ar_0 >= 2 /\ Ar_46 >= 0 /\ 0 >= Ar_2 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] start location: koat_start leaf cost: 0 Applied AI with 'oct' on problem 9 to obtain the following invariants: For symbol f1: X_8 - 2 >= 0 /\ X_2 + X_8 - 4 >= 0 /\ -X_2 + X_8 >= 0 /\ X_2 - 2 >= 0 For symbol f11: X_5 >= 0 /\ X_3 + X_5 - 1 >= 0 /\ X_18 + X_5 >= 0 /\ -X_18 + X_5 >= 0 /\ X_17 + X_5 >= 0 /\ -X_17 + X_5 >= 0 /\ X_16 + X_5 >= 0 /\ -X_16 + X_5 >= 0 /\ X_15 + X_5 >= 0 /\ -X_15 + X_5 >= 0 /\ X_14 + X_5 >= 0 /\ -X_14 + X_5 >= 0 /\ X_13 + X_5 >= 0 /\ -X_13 + X_5 >= 0 /\ X_11 + X_5 >= 0 /\ -X_11 + X_5 >= 0 /\ X_1 + X_5 - 2 >= 0 /\ -X_12 + X_4 - 1 >= 0 /\ X_3 - 1 >= 0 /\ X_18 + X_3 - 1 >= 0 /\ -X_18 + X_3 - 1 >= 0 /\ X_17 + X_3 - 1 >= 0 /\ -X_17 + X_3 - 1 >= 0 /\ X_16 + X_3 - 1 >= 0 /\ -X_16 + X_3 - 1 >= 0 /\ X_15 + X_3 - 1 >= 0 /\ -X_15 + X_3 - 1 >= 0 /\ X_14 + X_3 - 1 >= 0 /\ -X_14 + X_3 - 1 >= 0 /\ X_13 + X_3 - 1 >= 0 /\ -X_13 + X_3 - 1 >= 0 /\ X_11 + X_3 - 1 >= 0 /\ -X_11 + X_3 - 1 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ -X_18 >= 0 /\ X_17 - X_18 >= 0 /\ -X_17 - X_18 >= 0 /\ X_16 - X_18 >= 0 /\ -X_16 - X_18 >= 0 /\ X_15 - X_18 >= 0 /\ -X_15 - X_18 >= 0 /\ X_14 - X_18 >= 0 /\ -X_14 - X_18 >= 0 /\ X_13 - X_18 >= 0 /\ -X_13 - X_18 >= 0 /\ X_11 - X_18 >= 0 /\ -X_11 - X_18 >= 0 /\ X_1 - X_18 - 2 >= 0 /\ X_18 >= 0 /\ X_17 + X_18 >= 0 /\ -X_17 + X_18 >= 0 /\ X_16 + X_18 >= 0 /\ -X_16 + X_18 >= 0 /\ X_15 + X_18 >= 0 /\ -X_15 + X_18 >= 0 /\ X_14 + X_18 >= 0 /\ -X_14 + X_18 >= 0 /\ X_13 + X_18 >= 0 /\ -X_13 + X_18 >= 0 /\ X_11 + X_18 >= 0 /\ -X_11 + X_18 >= 0 /\ X_1 + X_18 - 2 >= 0 /\ -X_17 >= 0 /\ X_16 - X_17 >= 0 /\ -X_16 - X_17 >= 0 /\ X_15 - X_17 >= 0 /\ -X_15 - X_17 >= 0 /\ X_14 - X_17 >= 0 /\ -X_14 - X_17 >= 0 /\ X_13 - X_17 >= 0 /\ -X_13 - X_17 >= 0 /\ X_11 - X_17 >= 0 /\ -X_11 - X_17 >= 0 /\ X_1 - X_17 - 2 >= 0 /\ X_17 >= 0 /\ X_16 + X_17 >= 0 /\ -X_16 + X_17 >= 0 /\ X_15 + X_17 >= 0 /\ -X_15 + X_17 >= 0 /\ X_14 + X_17 >= 0 /\ -X_14 + X_17 >= 0 /\ X_13 + X_17 >= 0 /\ -X_13 + X_17 >= 0 /\ X_11 + X_17 >= 0 /\ -X_11 + X_17 >= 0 /\ X_1 + X_17 - 2 >= 0 /\ -X_16 >= 0 /\ X_15 - X_16 >= 0 /\ -X_15 - X_16 >= 0 /\ X_14 - X_16 >= 0 /\ -X_14 - X_16 >= 0 /\ X_13 - X_16 >= 0 /\ -X_13 - X_16 >= 0 /\ X_11 - X_16 >= 0 /\ -X_11 - X_16 >= 0 /\ X_1 - X_16 - 2 >= 0 /\ X_16 >= 0 /\ X_15 + X_16 >= 0 /\ -X_15 + X_16 >= 0 /\ X_14 + X_16 >= 0 /\ -X_14 + X_16 >= 0 /\ X_13 + X_16 >= 0 /\ -X_13 + X_16 >= 0 /\ X_11 + X_16 >= 0 /\ -X_11 + X_16 >= 0 /\ X_1 + X_16 - 2 >= 0 /\ -X_15 >= 0 /\ X_14 - X_15 >= 0 /\ -X_14 - X_15 >= 0 /\ X_13 - X_15 >= 0 /\ -X_13 - X_15 >= 0 /\ X_11 - X_15 >= 0 /\ -X_11 - X_15 >= 0 /\ X_1 - X_15 - 2 >= 0 /\ X_15 >= 0 /\ X_14 + X_15 >= 0 /\ -X_14 + X_15 >= 0 /\ X_13 + X_15 >= 0 /\ -X_13 + X_15 >= 0 /\ X_11 + X_15 >= 0 /\ -X_11 + X_15 >= 0 /\ X_1 + X_15 - 2 >= 0 /\ -X_14 >= 0 /\ X_13 - X_14 >= 0 /\ -X_13 - X_14 >= 0 /\ X_11 - X_14 >= 0 /\ -X_11 - X_14 >= 0 /\ X_1 - X_14 - 2 >= 0 /\ X_14 >= 0 /\ X_13 + X_14 >= 0 /\ -X_13 + X_14 >= 0 /\ X_11 + X_14 >= 0 /\ -X_11 + X_14 >= 0 /\ X_1 + X_14 - 2 >= 0 /\ -X_13 >= 0 /\ X_11 - X_13 >= 0 /\ -X_11 - X_13 >= 0 /\ X_1 - X_13 - 2 >= 0 /\ X_13 >= 0 /\ X_11 + X_13 >= 0 /\ -X_11 + X_13 >= 0 /\ X_1 + X_13 - 2 >= 0 /\ -X_11 >= 0 /\ X_1 - X_11 - 2 >= 0 /\ X_11 >= 0 /\ X_1 + X_11 - 2 >= 0 /\ X_1 - 2 >= 0 For symbol f13: X_5 >= 0 /\ -X_3 + X_5 >= 0 /\ X_18 + X_5 >= 0 /\ -X_18 + X_5 >= 0 /\ X_17 + X_5 >= 0 /\ -X_17 + X_5 >= 0 /\ X_16 + X_5 >= 0 /\ -X_16 + X_5 >= 0 /\ X_15 + X_5 >= 0 /\ -X_15 + X_5 >= 0 /\ X_14 + X_5 >= 0 /\ -X_14 + X_5 >= 0 /\ X_13 + X_5 >= 0 /\ -X_13 + X_5 >= 0 /\ X_11 + X_5 >= 0 /\ -X_11 + X_5 >= 0 /\ X_1 + X_5 - 2 >= 0 /\ -X_19 + X_4 - 1 >= 0 /\ -X_3 >= 0 /\ X_18 - X_3 >= 0 /\ -X_18 - X_3 >= 0 /\ X_17 - X_3 >= 0 /\ -X_17 - X_3 >= 0 /\ X_16 - X_3 >= 0 /\ -X_16 - X_3 >= 0 /\ X_15 - X_3 >= 0 /\ -X_15 - X_3 >= 0 /\ X_14 - X_3 >= 0 /\ -X_14 - X_3 >= 0 /\ X_13 - X_3 >= 0 /\ -X_13 - X_3 >= 0 /\ X_11 - X_3 >= 0 /\ -X_11 - X_3 >= 0 /\ X_1 - X_3 - 2 >= 0 /\ -X_18 >= 0 /\ X_17 - X_18 >= 0 /\ -X_17 - X_18 >= 0 /\ X_16 - X_18 >= 0 /\ -X_16 - X_18 >= 0 /\ X_15 - X_18 >= 0 /\ -X_15 - X_18 >= 0 /\ X_14 - X_18 >= 0 /\ -X_14 - X_18 >= 0 /\ X_13 - X_18 >= 0 /\ -X_13 - X_18 >= 0 /\ X_11 - X_18 >= 0 /\ -X_11 - X_18 >= 0 /\ X_1 - X_18 - 2 >= 0 /\ X_18 >= 0 /\ X_17 + X_18 >= 0 /\ -X_17 + X_18 >= 0 /\ X_16 + X_18 >= 0 /\ -X_16 + X_18 >= 0 /\ X_15 + X_18 >= 0 /\ -X_15 + X_18 >= 0 /\ X_14 + X_18 >= 0 /\ -X_14 + X_18 >= 0 /\ X_13 + X_18 >= 0 /\ -X_13 + X_18 >= 0 /\ X_11 + X_18 >= 0 /\ -X_11 + X_18 >= 0 /\ X_1 + X_18 - 2 >= 0 /\ -X_17 >= 0 /\ X_16 - X_17 >= 0 /\ -X_16 - X_17 >= 0 /\ X_15 - X_17 >= 0 /\ -X_15 - X_17 >= 0 /\ X_14 - X_17 >= 0 /\ -X_14 - X_17 >= 0 /\ X_13 - X_17 >= 0 /\ -X_13 - X_17 >= 0 /\ X_11 - X_17 >= 0 /\ -X_11 - X_17 >= 0 /\ X_1 - X_17 - 2 >= 0 /\ X_17 >= 0 /\ X_16 + X_17 >= 0 /\ -X_16 + X_17 >= 0 /\ X_15 + X_17 >= 0 /\ -X_15 + X_17 >= 0 /\ X_14 + X_17 >= 0 /\ -X_14 + X_17 >= 0 /\ X_13 + X_17 >= 0 /\ -X_13 + X_17 >= 0 /\ X_11 + X_17 >= 0 /\ -X_11 + X_17 >= 0 /\ X_1 + X_17 - 2 >= 0 /\ -X_16 >= 0 /\ X_15 - X_16 >= 0 /\ -X_15 - X_16 >= 0 /\ X_14 - X_16 >= 0 /\ -X_14 - X_16 >= 0 /\ X_13 - X_16 >= 0 /\ -X_13 - X_16 >= 0 /\ X_11 - X_16 >= 0 /\ -X_11 - X_16 >= 0 /\ X_1 - X_16 - 2 >= 0 /\ X_16 >= 0 /\ X_15 + X_16 >= 0 /\ -X_15 + X_16 >= 0 /\ X_14 + X_16 >= 0 /\ -X_14 + X_16 >= 0 /\ X_13 + X_16 >= 0 /\ -X_13 + X_16 >= 0 /\ X_11 + X_16 >= 0 /\ -X_11 + X_16 >= 0 /\ X_1 + X_16 - 2 >= 0 /\ -X_15 >= 0 /\ X_14 - X_15 >= 0 /\ -X_14 - X_15 >= 0 /\ X_13 - X_15 >= 0 /\ -X_13 - X_15 >= 0 /\ X_11 - X_15 >= 0 /\ -X_11 - X_15 >= 0 /\ X_1 - X_15 - 2 >= 0 /\ X_15 >= 0 /\ X_14 + X_15 >= 0 /\ -X_14 + X_15 >= 0 /\ X_13 + X_15 >= 0 /\ -X_13 + X_15 >= 0 /\ X_11 + X_15 >= 0 /\ -X_11 + X_15 >= 0 /\ X_1 + X_15 - 2 >= 0 /\ -X_14 >= 0 /\ X_13 - X_14 >= 0 /\ -X_13 - X_14 >= 0 /\ X_11 - X_14 >= 0 /\ -X_11 - X_14 >= 0 /\ X_1 - X_14 - 2 >= 0 /\ X_14 >= 0 /\ X_13 + X_14 >= 0 /\ -X_13 + X_14 >= 0 /\ X_11 + X_14 >= 0 /\ -X_11 + X_14 >= 0 /\ X_1 + X_14 - 2 >= 0 /\ -X_13 >= 0 /\ X_11 - X_13 >= 0 /\ -X_11 - X_13 >= 0 /\ X_1 - X_13 - 2 >= 0 /\ X_13 >= 0 /\ X_11 + X_13 >= 0 /\ -X_11 + X_13 >= 0 /\ X_1 + X_13 - 2 >= 0 /\ -X_11 >= 0 /\ X_1 - X_11 - 2 >= 0 /\ X_11 >= 0 /\ X_1 + X_11 - 2 >= 0 /\ X_1 - 2 >= 0 For symbol f16: X_17 - X_18 >= 0 /\ -X_17 + X_18 >= 0 /\ -X_1 + 1 >= 0 /\ X_1 - 1 >= 0 For symbol f18: X_4 >= 0 /\ X_1 + X_4 - 2 >= 0 /\ X_17 - X_18 >= 0 /\ -X_17 + X_18 >= 0 /\ X_1 - 2 >= 0 For symbol f27: -X_3 >= 0 /\ X_1 - X_3 - 2 >= 0 /\ X_17 - X_18 >= 0 /\ -X_17 + X_18 >= 0 /\ X_1 - 2 >= 0 This yielded the following problem: 10: T: (Comp: Ar_46 + 2, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46 - 1, Ar_52)) [ Ar_7 >= 0 /\ -Ar_2 + Ar_7 >= 0 /\ Ar_43 + Ar_7 >= 0 /\ -Ar_43 + Ar_7 >= 0 /\ Ar_42 + Ar_7 >= 0 /\ -Ar_42 + Ar_7 >= 0 /\ Ar_40 + Ar_7 >= 0 /\ -Ar_40 + Ar_7 >= 0 /\ Ar_39 + Ar_7 >= 0 /\ -Ar_39 + Ar_7 >= 0 /\ Ar_38 + Ar_7 >= 0 /\ -Ar_38 + Ar_7 >= 0 /\ Ar_37 + Ar_7 >= 0 /\ -Ar_37 + Ar_7 >= 0 /\ Ar_34 + Ar_7 >= 0 /\ -Ar_34 + Ar_7 >= 0 /\ Ar_0 + Ar_7 - 2 >= 0 /\ -Ar_46 + Ar_3 - 1 >= 0 /\ -Ar_2 >= 0 /\ Ar_43 - Ar_2 >= 0 /\ -Ar_43 - Ar_2 >= 0 /\ Ar_42 - Ar_2 >= 0 /\ -Ar_42 - Ar_2 >= 0 /\ Ar_40 - Ar_2 >= 0 /\ -Ar_40 - Ar_2 >= 0 /\ Ar_39 - Ar_2 >= 0 /\ -Ar_39 - Ar_2 >= 0 /\ Ar_38 - Ar_2 >= 0 /\ -Ar_38 - Ar_2 >= 0 /\ Ar_37 - Ar_2 >= 0 /\ -Ar_37 - Ar_2 >= 0 /\ Ar_34 - Ar_2 >= 0 /\ -Ar_34 - Ar_2 >= 0 /\ Ar_0 - Ar_2 - 2 >= 0 /\ -Ar_43 >= 0 /\ Ar_42 - Ar_43 >= 0 /\ -Ar_42 - Ar_43 >= 0 /\ Ar_40 - Ar_43 >= 0 /\ -Ar_40 - Ar_43 >= 0 /\ Ar_39 - Ar_43 >= 0 /\ -Ar_39 - Ar_43 >= 0 /\ Ar_38 - Ar_43 >= 0 /\ -Ar_38 - Ar_43 >= 0 /\ Ar_37 - Ar_43 >= 0 /\ -Ar_37 - Ar_43 >= 0 /\ Ar_34 - Ar_43 >= 0 /\ -Ar_34 - Ar_43 >= 0 /\ Ar_0 - Ar_43 - 2 >= 0 /\ Ar_43 >= 0 /\ Ar_42 + Ar_43 >= 0 /\ -Ar_42 + Ar_43 >= 0 /\ Ar_40 + Ar_43 >= 0 /\ -Ar_40 + Ar_43 >= 0 /\ Ar_39 + Ar_43 >= 0 /\ -Ar_39 + Ar_43 >= 0 /\ Ar_38 + Ar_43 >= 0 /\ -Ar_38 + Ar_43 >= 0 /\ Ar_37 + Ar_43 >= 0 /\ -Ar_37 + Ar_43 >= 0 /\ Ar_34 + Ar_43 >= 0 /\ -Ar_34 + Ar_43 >= 0 /\ Ar_0 + Ar_43 - 2 >= 0 /\ -Ar_42 >= 0 /\ Ar_40 - Ar_42 >= 0 /\ -Ar_40 - Ar_42 >= 0 /\ Ar_39 - Ar_42 >= 0 /\ -Ar_39 - Ar_42 >= 0 /\ Ar_38 - Ar_42 >= 0 /\ -Ar_38 - Ar_42 >= 0 /\ Ar_37 - Ar_42 >= 0 /\ -Ar_37 - Ar_42 >= 0 /\ Ar_34 - Ar_42 >= 0 /\ -Ar_34 - Ar_42 >= 0 /\ Ar_0 - Ar_42 - 2 >= 0 /\ Ar_42 >= 0 /\ Ar_40 + Ar_42 >= 0 /\ -Ar_40 + Ar_42 >= 0 /\ Ar_39 + Ar_42 >= 0 /\ -Ar_39 + Ar_42 >= 0 /\ Ar_38 + Ar_42 >= 0 /\ -Ar_38 + Ar_42 >= 0 /\ Ar_37 + Ar_42 >= 0 /\ -Ar_37 + Ar_42 >= 0 /\ Ar_34 + Ar_42 >= 0 /\ -Ar_34 + Ar_42 >= 0 /\ Ar_0 + Ar_42 - 2 >= 0 /\ -Ar_40 >= 0 /\ Ar_39 - Ar_40 >= 0 /\ -Ar_39 - Ar_40 >= 0 /\ Ar_38 - Ar_40 >= 0 /\ -Ar_38 - Ar_40 >= 0 /\ Ar_37 - Ar_40 >= 0 /\ -Ar_37 - Ar_40 >= 0 /\ Ar_34 - Ar_40 >= 0 /\ -Ar_34 - Ar_40 >= 0 /\ Ar_0 - Ar_40 - 2 >= 0 /\ Ar_40 >= 0 /\ Ar_39 + Ar_40 >= 0 /\ -Ar_39 + Ar_40 >= 0 /\ Ar_38 + Ar_40 >= 0 /\ -Ar_38 + Ar_40 >= 0 /\ Ar_37 + Ar_40 >= 0 /\ -Ar_37 + Ar_40 >= 0 /\ Ar_34 + Ar_40 >= 0 /\ -Ar_34 + Ar_40 >= 0 /\ Ar_0 + Ar_40 - 2 >= 0 /\ -Ar_39 >= 0 /\ Ar_38 - Ar_39 >= 0 /\ -Ar_38 - Ar_39 >= 0 /\ Ar_37 - Ar_39 >= 0 /\ -Ar_37 - Ar_39 >= 0 /\ Ar_34 - Ar_39 >= 0 /\ -Ar_34 - Ar_39 >= 0 /\ Ar_0 - Ar_39 - 2 >= 0 /\ Ar_39 >= 0 /\ Ar_38 + Ar_39 >= 0 /\ -Ar_38 + Ar_39 >= 0 /\ Ar_37 + Ar_39 >= 0 /\ -Ar_37 + Ar_39 >= 0 /\ Ar_34 + Ar_39 >= 0 /\ -Ar_34 + Ar_39 >= 0 /\ Ar_0 + Ar_39 - 2 >= 0 /\ -Ar_38 >= 0 /\ Ar_37 - Ar_38 >= 0 /\ -Ar_37 - Ar_38 >= 0 /\ Ar_34 - Ar_38 >= 0 /\ -Ar_34 - Ar_38 >= 0 /\ Ar_0 - Ar_38 - 2 >= 0 /\ Ar_38 >= 0 /\ Ar_37 + Ar_38 >= 0 /\ -Ar_37 + Ar_38 >= 0 /\ Ar_34 + Ar_38 >= 0 /\ -Ar_34 + Ar_38 >= 0 /\ Ar_0 + Ar_38 - 2 >= 0 /\ -Ar_37 >= 0 /\ Ar_34 - Ar_37 >= 0 /\ -Ar_34 - Ar_37 >= 0 /\ Ar_0 - Ar_37 - 2 >= 0 /\ Ar_37 >= 0 /\ Ar_34 + Ar_37 >= 0 /\ -Ar_34 + Ar_37 >= 0 /\ Ar_0 + Ar_37 - 2 >= 0 /\ -Ar_34 >= 0 /\ Ar_0 - Ar_34 - 2 >= 0 /\ Ar_34 >= 0 /\ Ar_0 + Ar_34 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_0 >= 2 /\ Ar_46 >= 0 /\ 0 >= Ar_2 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] (Comp: 3, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_81, Ar_35, Fresh_82, Fresh_83, Fresh_84, Fresh_85, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_7 >= 0 /\ -Ar_2 + Ar_7 >= 0 /\ Ar_43 + Ar_7 >= 0 /\ -Ar_43 + Ar_7 >= 0 /\ Ar_42 + Ar_7 >= 0 /\ -Ar_42 + Ar_7 >= 0 /\ Ar_40 + Ar_7 >= 0 /\ -Ar_40 + Ar_7 >= 0 /\ Ar_39 + Ar_7 >= 0 /\ -Ar_39 + Ar_7 >= 0 /\ Ar_38 + Ar_7 >= 0 /\ -Ar_38 + Ar_7 >= 0 /\ Ar_37 + Ar_7 >= 0 /\ -Ar_37 + Ar_7 >= 0 /\ Ar_34 + Ar_7 >= 0 /\ -Ar_34 + Ar_7 >= 0 /\ Ar_0 + Ar_7 - 2 >= 0 /\ -Ar_46 + Ar_3 - 1 >= 0 /\ -Ar_2 >= 0 /\ Ar_43 - Ar_2 >= 0 /\ -Ar_43 - Ar_2 >= 0 /\ Ar_42 - Ar_2 >= 0 /\ -Ar_42 - Ar_2 >= 0 /\ Ar_40 - Ar_2 >= 0 /\ -Ar_40 - Ar_2 >= 0 /\ Ar_39 - Ar_2 >= 0 /\ -Ar_39 - Ar_2 >= 0 /\ Ar_38 - Ar_2 >= 0 /\ -Ar_38 - Ar_2 >= 0 /\ Ar_37 - Ar_2 >= 0 /\ -Ar_37 - Ar_2 >= 0 /\ Ar_34 - Ar_2 >= 0 /\ -Ar_34 - Ar_2 >= 0 /\ Ar_0 - Ar_2 - 2 >= 0 /\ -Ar_43 >= 0 /\ Ar_42 - Ar_43 >= 0 /\ -Ar_42 - Ar_43 >= 0 /\ Ar_40 - Ar_43 >= 0 /\ -Ar_40 - Ar_43 >= 0 /\ Ar_39 - Ar_43 >= 0 /\ -Ar_39 - Ar_43 >= 0 /\ Ar_38 - Ar_43 >= 0 /\ -Ar_38 - Ar_43 >= 0 /\ Ar_37 - Ar_43 >= 0 /\ -Ar_37 - Ar_43 >= 0 /\ Ar_34 - Ar_43 >= 0 /\ -Ar_34 - Ar_43 >= 0 /\ Ar_0 - Ar_43 - 2 >= 0 /\ Ar_43 >= 0 /\ Ar_42 + Ar_43 >= 0 /\ -Ar_42 + Ar_43 >= 0 /\ Ar_40 + Ar_43 >= 0 /\ -Ar_40 + Ar_43 >= 0 /\ Ar_39 + Ar_43 >= 0 /\ -Ar_39 + Ar_43 >= 0 /\ Ar_38 + Ar_43 >= 0 /\ -Ar_38 + Ar_43 >= 0 /\ Ar_37 + Ar_43 >= 0 /\ -Ar_37 + Ar_43 >= 0 /\ Ar_34 + Ar_43 >= 0 /\ -Ar_34 + Ar_43 >= 0 /\ Ar_0 + Ar_43 - 2 >= 0 /\ -Ar_42 >= 0 /\ Ar_40 - Ar_42 >= 0 /\ -Ar_40 - Ar_42 >= 0 /\ Ar_39 - Ar_42 >= 0 /\ -Ar_39 - Ar_42 >= 0 /\ Ar_38 - Ar_42 >= 0 /\ -Ar_38 - Ar_42 >= 0 /\ Ar_37 - Ar_42 >= 0 /\ -Ar_37 - Ar_42 >= 0 /\ Ar_34 - Ar_42 >= 0 /\ -Ar_34 - Ar_42 >= 0 /\ Ar_0 - Ar_42 - 2 >= 0 /\ Ar_42 >= 0 /\ Ar_40 + Ar_42 >= 0 /\ -Ar_40 + Ar_42 >= 0 /\ Ar_39 + Ar_42 >= 0 /\ -Ar_39 + Ar_42 >= 0 /\ Ar_38 + Ar_42 >= 0 /\ -Ar_38 + Ar_42 >= 0 /\ Ar_37 + Ar_42 >= 0 /\ -Ar_37 + Ar_42 >= 0 /\ Ar_34 + Ar_42 >= 0 /\ -Ar_34 + Ar_42 >= 0 /\ Ar_0 + Ar_42 - 2 >= 0 /\ -Ar_40 >= 0 /\ Ar_39 - Ar_40 >= 0 /\ -Ar_39 - Ar_40 >= 0 /\ Ar_38 - Ar_40 >= 0 /\ -Ar_38 - Ar_40 >= 0 /\ Ar_37 - Ar_40 >= 0 /\ -Ar_37 - Ar_40 >= 0 /\ Ar_34 - Ar_40 >= 0 /\ -Ar_34 - Ar_40 >= 0 /\ Ar_0 - Ar_40 - 2 >= 0 /\ Ar_40 >= 0 /\ Ar_39 + Ar_40 >= 0 /\ -Ar_39 + Ar_40 >= 0 /\ Ar_38 + Ar_40 >= 0 /\ -Ar_38 + Ar_40 >= 0 /\ Ar_37 + Ar_40 >= 0 /\ -Ar_37 + Ar_40 >= 0 /\ Ar_34 + Ar_40 >= 0 /\ -Ar_34 + Ar_40 >= 0 /\ Ar_0 + Ar_40 - 2 >= 0 /\ -Ar_39 >= 0 /\ Ar_38 - Ar_39 >= 0 /\ -Ar_38 - Ar_39 >= 0 /\ Ar_37 - Ar_39 >= 0 /\ -Ar_37 - Ar_39 >= 0 /\ Ar_34 - Ar_39 >= 0 /\ -Ar_34 - Ar_39 >= 0 /\ Ar_0 - Ar_39 - 2 >= 0 /\ Ar_39 >= 0 /\ Ar_38 + Ar_39 >= 0 /\ -Ar_38 + Ar_39 >= 0 /\ Ar_37 + Ar_39 >= 0 /\ -Ar_37 + Ar_39 >= 0 /\ Ar_34 + Ar_39 >= 0 /\ -Ar_34 + Ar_39 >= 0 /\ Ar_0 + Ar_39 - 2 >= 0 /\ -Ar_38 >= 0 /\ Ar_37 - Ar_38 >= 0 /\ -Ar_37 - Ar_38 >= 0 /\ Ar_34 - Ar_38 >= 0 /\ -Ar_34 - Ar_38 >= 0 /\ Ar_0 - Ar_38 - 2 >= 0 /\ Ar_38 >= 0 /\ Ar_37 + Ar_38 >= 0 /\ -Ar_37 + Ar_38 >= 0 /\ Ar_34 + Ar_38 >= 0 /\ -Ar_34 + Ar_38 >= 0 /\ Ar_0 + Ar_38 - 2 >= 0 /\ -Ar_37 >= 0 /\ Ar_34 - Ar_37 >= 0 /\ -Ar_34 - Ar_37 >= 0 /\ Ar_0 - Ar_37 - 2 >= 0 /\ Ar_37 >= 0 /\ Ar_34 + Ar_37 >= 0 /\ -Ar_34 + Ar_37 >= 0 /\ Ar_0 + Ar_37 - 2 >= 0 /\ -Ar_34 >= 0 /\ Ar_0 - Ar_34 - 2 >= 0 /\ Ar_34 >= 0 /\ Ar_0 + Ar_34 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_46 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Fresh_112, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ -Ar_2 >= 0 /\ Ar_0 - Ar_2 - 2 >= 0 /\ Ar_42 - Ar_43 >= 0 /\ -Ar_42 + Ar_43 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_0 >= 2 /\ Ar_3 >= 0 /\ 0 >= Ar_24 /\ Ar_7 >= 0 ] (Comp: 3, Cost: 1) f27(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_46 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ -Ar_2 >= 0 /\ Ar_0 - Ar_2 - 2 >= 0 /\ Ar_42 - Ar_43 >= 0 /\ -Ar_42 + Ar_43 >= 0 /\ Ar_0 - 2 >= 0 /\ Fresh_58 >= 0 /\ Ar_0 >= 2 /\ 0 >= Ar_2 /\ Ar_3 >= 0 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: Ar_35 + 2, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35 - 1, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Ar_7 >= 0 /\ Ar_2 + Ar_7 - 1 >= 0 /\ Ar_43 + Ar_7 >= 0 /\ -Ar_43 + Ar_7 >= 0 /\ Ar_42 + Ar_7 >= 0 /\ -Ar_42 + Ar_7 >= 0 /\ Ar_40 + Ar_7 >= 0 /\ -Ar_40 + Ar_7 >= 0 /\ Ar_39 + Ar_7 >= 0 /\ -Ar_39 + Ar_7 >= 0 /\ Ar_38 + Ar_7 >= 0 /\ -Ar_38 + Ar_7 >= 0 /\ Ar_37 + Ar_7 >= 0 /\ -Ar_37 + Ar_7 >= 0 /\ Ar_34 + Ar_7 >= 0 /\ -Ar_34 + Ar_7 >= 0 /\ Ar_0 + Ar_7 - 2 >= 0 /\ -Ar_35 + Ar_3 - 1 >= 0 /\ Ar_2 - 1 >= 0 /\ Ar_43 + Ar_2 - 1 >= 0 /\ -Ar_43 + Ar_2 - 1 >= 0 /\ Ar_42 + Ar_2 - 1 >= 0 /\ -Ar_42 + Ar_2 - 1 >= 0 /\ Ar_40 + Ar_2 - 1 >= 0 /\ -Ar_40 + Ar_2 - 1 >= 0 /\ Ar_39 + Ar_2 - 1 >= 0 /\ -Ar_39 + Ar_2 - 1 >= 0 /\ Ar_38 + Ar_2 - 1 >= 0 /\ -Ar_38 + Ar_2 - 1 >= 0 /\ Ar_37 + Ar_2 - 1 >= 0 /\ -Ar_37 + Ar_2 - 1 >= 0 /\ Ar_34 + Ar_2 - 1 >= 0 /\ -Ar_34 + Ar_2 - 1 >= 0 /\ Ar_0 + Ar_2 - 3 >= 0 /\ -Ar_43 >= 0 /\ Ar_42 - Ar_43 >= 0 /\ -Ar_42 - Ar_43 >= 0 /\ Ar_40 - Ar_43 >= 0 /\ -Ar_40 - Ar_43 >= 0 /\ Ar_39 - Ar_43 >= 0 /\ -Ar_39 - Ar_43 >= 0 /\ Ar_38 - Ar_43 >= 0 /\ -Ar_38 - Ar_43 >= 0 /\ Ar_37 - Ar_43 >= 0 /\ -Ar_37 - Ar_43 >= 0 /\ Ar_34 - Ar_43 >= 0 /\ -Ar_34 - Ar_43 >= 0 /\ Ar_0 - Ar_43 - 2 >= 0 /\ Ar_43 >= 0 /\ Ar_42 + Ar_43 >= 0 /\ -Ar_42 + Ar_43 >= 0 /\ Ar_40 + Ar_43 >= 0 /\ -Ar_40 + Ar_43 >= 0 /\ Ar_39 + Ar_43 >= 0 /\ -Ar_39 + Ar_43 >= 0 /\ Ar_38 + Ar_43 >= 0 /\ -Ar_38 + Ar_43 >= 0 /\ Ar_37 + Ar_43 >= 0 /\ -Ar_37 + Ar_43 >= 0 /\ Ar_34 + Ar_43 >= 0 /\ -Ar_34 + Ar_43 >= 0 /\ Ar_0 + Ar_43 - 2 >= 0 /\ -Ar_42 >= 0 /\ Ar_40 - Ar_42 >= 0 /\ -Ar_40 - Ar_42 >= 0 /\ Ar_39 - Ar_42 >= 0 /\ -Ar_39 - Ar_42 >= 0 /\ Ar_38 - Ar_42 >= 0 /\ -Ar_38 - Ar_42 >= 0 /\ Ar_37 - Ar_42 >= 0 /\ -Ar_37 - Ar_42 >= 0 /\ Ar_34 - Ar_42 >= 0 /\ -Ar_34 - Ar_42 >= 0 /\ Ar_0 - Ar_42 - 2 >= 0 /\ Ar_42 >= 0 /\ Ar_40 + Ar_42 >= 0 /\ -Ar_40 + Ar_42 >= 0 /\ Ar_39 + Ar_42 >= 0 /\ -Ar_39 + Ar_42 >= 0 /\ Ar_38 + Ar_42 >= 0 /\ -Ar_38 + Ar_42 >= 0 /\ Ar_37 + Ar_42 >= 0 /\ -Ar_37 + Ar_42 >= 0 /\ Ar_34 + Ar_42 >= 0 /\ -Ar_34 + Ar_42 >= 0 /\ Ar_0 + Ar_42 - 2 >= 0 /\ -Ar_40 >= 0 /\ Ar_39 - Ar_40 >= 0 /\ -Ar_39 - Ar_40 >= 0 /\ Ar_38 - Ar_40 >= 0 /\ -Ar_38 - Ar_40 >= 0 /\ Ar_37 - Ar_40 >= 0 /\ -Ar_37 - Ar_40 >= 0 /\ Ar_34 - Ar_40 >= 0 /\ -Ar_34 - Ar_40 >= 0 /\ Ar_0 - Ar_40 - 2 >= 0 /\ Ar_40 >= 0 /\ Ar_39 + Ar_40 >= 0 /\ -Ar_39 + Ar_40 >= 0 /\ Ar_38 + Ar_40 >= 0 /\ -Ar_38 + Ar_40 >= 0 /\ Ar_37 + Ar_40 >= 0 /\ -Ar_37 + Ar_40 >= 0 /\ Ar_34 + Ar_40 >= 0 /\ -Ar_34 + Ar_40 >= 0 /\ Ar_0 + Ar_40 - 2 >= 0 /\ -Ar_39 >= 0 /\ Ar_38 - Ar_39 >= 0 /\ -Ar_38 - Ar_39 >= 0 /\ Ar_37 - Ar_39 >= 0 /\ -Ar_37 - Ar_39 >= 0 /\ Ar_34 - Ar_39 >= 0 /\ -Ar_34 - Ar_39 >= 0 /\ Ar_0 - Ar_39 - 2 >= 0 /\ Ar_39 >= 0 /\ Ar_38 + Ar_39 >= 0 /\ -Ar_38 + Ar_39 >= 0 /\ Ar_37 + Ar_39 >= 0 /\ -Ar_37 + Ar_39 >= 0 /\ Ar_34 + Ar_39 >= 0 /\ -Ar_34 + Ar_39 >= 0 /\ Ar_0 + Ar_39 - 2 >= 0 /\ -Ar_38 >= 0 /\ Ar_37 - Ar_38 >= 0 /\ -Ar_37 - Ar_38 >= 0 /\ Ar_34 - Ar_38 >= 0 /\ -Ar_34 - Ar_38 >= 0 /\ Ar_0 - Ar_38 - 2 >= 0 /\ Ar_38 >= 0 /\ Ar_37 + Ar_38 >= 0 /\ -Ar_37 + Ar_38 >= 0 /\ Ar_34 + Ar_38 >= 0 /\ -Ar_34 + Ar_38 >= 0 /\ Ar_0 + Ar_38 - 2 >= 0 /\ -Ar_37 >= 0 /\ Ar_34 - Ar_37 >= 0 /\ -Ar_34 - Ar_37 >= 0 /\ Ar_0 - Ar_37 - 2 >= 0 /\ Ar_37 >= 0 /\ Ar_34 + Ar_37 >= 0 /\ -Ar_34 + Ar_37 >= 0 /\ Ar_0 + Ar_37 - 2 >= 0 /\ -Ar_34 >= 0 /\ Ar_0 - Ar_34 - 2 >= 0 /\ Ar_34 >= 0 /\ Ar_0 + Ar_34 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_0 >= 2 /\ Ar_35 >= 0 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = Ar_40 /\ Ar_39 = 0 /\ Ar_38 = Ar_40 /\ Ar_37 = 0 ] (Comp: 3, Cost: 1) f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_95, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_97, Ar_35, Fresh_98, Fresh_99, Fresh_100, Fresh_101, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_7 >= 0 /\ Ar_2 + Ar_7 - 1 >= 0 /\ Ar_43 + Ar_7 >= 0 /\ -Ar_43 + Ar_7 >= 0 /\ Ar_42 + Ar_7 >= 0 /\ -Ar_42 + Ar_7 >= 0 /\ Ar_40 + Ar_7 >= 0 /\ -Ar_40 + Ar_7 >= 0 /\ Ar_39 + Ar_7 >= 0 /\ -Ar_39 + Ar_7 >= 0 /\ Ar_38 + Ar_7 >= 0 /\ -Ar_38 + Ar_7 >= 0 /\ Ar_37 + Ar_7 >= 0 /\ -Ar_37 + Ar_7 >= 0 /\ Ar_34 + Ar_7 >= 0 /\ -Ar_34 + Ar_7 >= 0 /\ Ar_0 + Ar_7 - 2 >= 0 /\ -Ar_35 + Ar_3 - 1 >= 0 /\ Ar_2 - 1 >= 0 /\ Ar_43 + Ar_2 - 1 >= 0 /\ -Ar_43 + Ar_2 - 1 >= 0 /\ Ar_42 + Ar_2 - 1 >= 0 /\ -Ar_42 + Ar_2 - 1 >= 0 /\ Ar_40 + Ar_2 - 1 >= 0 /\ -Ar_40 + Ar_2 - 1 >= 0 /\ Ar_39 + Ar_2 - 1 >= 0 /\ -Ar_39 + Ar_2 - 1 >= 0 /\ Ar_38 + Ar_2 - 1 >= 0 /\ -Ar_38 + Ar_2 - 1 >= 0 /\ Ar_37 + Ar_2 - 1 >= 0 /\ -Ar_37 + Ar_2 - 1 >= 0 /\ Ar_34 + Ar_2 - 1 >= 0 /\ -Ar_34 + Ar_2 - 1 >= 0 /\ Ar_0 + Ar_2 - 3 >= 0 /\ -Ar_43 >= 0 /\ Ar_42 - Ar_43 >= 0 /\ -Ar_42 - Ar_43 >= 0 /\ Ar_40 - Ar_43 >= 0 /\ -Ar_40 - Ar_43 >= 0 /\ Ar_39 - Ar_43 >= 0 /\ -Ar_39 - Ar_43 >= 0 /\ Ar_38 - Ar_43 >= 0 /\ -Ar_38 - Ar_43 >= 0 /\ Ar_37 - Ar_43 >= 0 /\ -Ar_37 - Ar_43 >= 0 /\ Ar_34 - Ar_43 >= 0 /\ -Ar_34 - Ar_43 >= 0 /\ Ar_0 - Ar_43 - 2 >= 0 /\ Ar_43 >= 0 /\ Ar_42 + Ar_43 >= 0 /\ -Ar_42 + Ar_43 >= 0 /\ Ar_40 + Ar_43 >= 0 /\ -Ar_40 + Ar_43 >= 0 /\ Ar_39 + Ar_43 >= 0 /\ -Ar_39 + Ar_43 >= 0 /\ Ar_38 + Ar_43 >= 0 /\ -Ar_38 + Ar_43 >= 0 /\ Ar_37 + Ar_43 >= 0 /\ -Ar_37 + Ar_43 >= 0 /\ Ar_34 + Ar_43 >= 0 /\ -Ar_34 + Ar_43 >= 0 /\ Ar_0 + Ar_43 - 2 >= 0 /\ -Ar_42 >= 0 /\ Ar_40 - Ar_42 >= 0 /\ -Ar_40 - Ar_42 >= 0 /\ Ar_39 - Ar_42 >= 0 /\ -Ar_39 - Ar_42 >= 0 /\ Ar_38 - Ar_42 >= 0 /\ -Ar_38 - Ar_42 >= 0 /\ Ar_37 - Ar_42 >= 0 /\ -Ar_37 - Ar_42 >= 0 /\ Ar_34 - Ar_42 >= 0 /\ -Ar_34 - Ar_42 >= 0 /\ Ar_0 - Ar_42 - 2 >= 0 /\ Ar_42 >= 0 /\ Ar_40 + Ar_42 >= 0 /\ -Ar_40 + Ar_42 >= 0 /\ Ar_39 + Ar_42 >= 0 /\ -Ar_39 + Ar_42 >= 0 /\ Ar_38 + Ar_42 >= 0 /\ -Ar_38 + Ar_42 >= 0 /\ Ar_37 + Ar_42 >= 0 /\ -Ar_37 + Ar_42 >= 0 /\ Ar_34 + Ar_42 >= 0 /\ -Ar_34 + Ar_42 >= 0 /\ Ar_0 + Ar_42 - 2 >= 0 /\ -Ar_40 >= 0 /\ Ar_39 - Ar_40 >= 0 /\ -Ar_39 - Ar_40 >= 0 /\ Ar_38 - Ar_40 >= 0 /\ -Ar_38 - Ar_40 >= 0 /\ Ar_37 - Ar_40 >= 0 /\ -Ar_37 - Ar_40 >= 0 /\ Ar_34 - Ar_40 >= 0 /\ -Ar_34 - Ar_40 >= 0 /\ Ar_0 - Ar_40 - 2 >= 0 /\ Ar_40 >= 0 /\ Ar_39 + Ar_40 >= 0 /\ -Ar_39 + Ar_40 >= 0 /\ Ar_38 + Ar_40 >= 0 /\ -Ar_38 + Ar_40 >= 0 /\ Ar_37 + Ar_40 >= 0 /\ -Ar_37 + Ar_40 >= 0 /\ Ar_34 + Ar_40 >= 0 /\ -Ar_34 + Ar_40 >= 0 /\ Ar_0 + Ar_40 - 2 >= 0 /\ -Ar_39 >= 0 /\ Ar_38 - Ar_39 >= 0 /\ -Ar_38 - Ar_39 >= 0 /\ Ar_37 - Ar_39 >= 0 /\ -Ar_37 - Ar_39 >= 0 /\ Ar_34 - Ar_39 >= 0 /\ -Ar_34 - Ar_39 >= 0 /\ Ar_0 - Ar_39 - 2 >= 0 /\ Ar_39 >= 0 /\ Ar_38 + Ar_39 >= 0 /\ -Ar_38 + Ar_39 >= 0 /\ Ar_37 + Ar_39 >= 0 /\ -Ar_37 + Ar_39 >= 0 /\ Ar_34 + Ar_39 >= 0 /\ -Ar_34 + Ar_39 >= 0 /\ Ar_0 + Ar_39 - 2 >= 0 /\ -Ar_38 >= 0 /\ Ar_37 - Ar_38 >= 0 /\ -Ar_37 - Ar_38 >= 0 /\ Ar_34 - Ar_38 >= 0 /\ -Ar_34 - Ar_38 >= 0 /\ Ar_0 - Ar_38 - 2 >= 0 /\ Ar_38 >= 0 /\ Ar_37 + Ar_38 >= 0 /\ -Ar_37 + Ar_38 >= 0 /\ Ar_34 + Ar_38 >= 0 /\ -Ar_34 + Ar_38 >= 0 /\ Ar_0 + Ar_38 - 2 >= 0 /\ -Ar_37 >= 0 /\ Ar_34 - Ar_37 >= 0 /\ -Ar_34 - Ar_37 >= 0 /\ Ar_0 - Ar_37 - 2 >= 0 /\ Ar_37 >= 0 /\ Ar_34 + Ar_37 >= 0 /\ -Ar_34 + Ar_37 >= 0 /\ Ar_0 + Ar_37 - 2 >= 0 /\ -Ar_34 >= 0 /\ Ar_0 - Ar_34 - 2 >= 0 /\ Ar_34 >= 0 /\ Ar_0 + Ar_34 - 2 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_35 >= 0 /\ Ar_37 = Ar_34 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f27(Ar_0, Ar_1, Ar_2, Fresh_114, Fresh_115, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_3 >= 0 /\ Ar_0 + Ar_3 - 2 >= 0 /\ Ar_42 - Ar_43 >= 0 /\ -Ar_42 + Ar_43 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_2 ] (Comp: ?, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Ar_1, Ar_2 - 1, Ar_3 + 1, Ar_7 - 1, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_3 >= 0 /\ Ar_0 + Ar_3 - 2 >= 0 /\ Ar_42 - Ar_43 >= 0 /\ -Ar_42 + Ar_43 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_0 >= 2 /\ Ar_21 >= 1 /\ Ar_7 >= 0 /\ Ar_2 = Ar_21 ] (Comp: 3, Cost: 1) f18(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f11(Ar_0, Ar_1, Ar_2, Ar_35 + 1, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_43, Ar_35, 0, Ar_43, 0, Ar_43, 0, Ar_43, Ar_46, Ar_52)) [ Ar_3 >= 0 /\ Ar_0 + Ar_3 - 2 >= 0 /\ Ar_42 - Ar_43 >= 0 /\ -Ar_42 + Ar_43 >= 0 /\ Ar_0 - 2 >= 0 /\ Fresh_59 >= 0 /\ Fresh_60 >= 0 /\ Ar_0 >= 2 /\ Ar_2 >= 1 /\ Ar_7 >= 0 /\ Ar_42 = 0 ] (Comp: ?, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f1(Ar_0, Ar_1 + 1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_30, Fresh_111, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ Ar_28 - 2 >= 0 /\ Ar_1 + Ar_28 - 4 >= 0 /\ -Ar_1 + Ar_28 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_1 >= 0 /\ Ar_28 >= Ar_1 + 1 ] (Comp: 1, Cost: 1) f1(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f18(Ar_0, Fresh_65, Fresh_66, 0, Ar_7, Ar_21, Ar_24, Fresh_68, Fresh_69, Fresh_70, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_29, Ar_29, Ar_46, Fresh_74)) [ Ar_28 - 2 >= 0 /\ Ar_1 + Ar_28 - 4 >= 0 /\ -Ar_1 + Ar_28 >= 0 /\ Ar_1 - 2 >= 0 /\ F3 >= Ar_0 /\ Fresh_73 >= Ar_0 /\ Ar_1 >= Ar_28 /\ Ar_0 >= 2 /\ Ar_7 >= Ar_0 /\ Ar_7 >= 0 /\ Ar_1 >= 0 /\ Ar_3 = 0 ] (Comp: ?, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f16(1, Ar_1, Fresh_62, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_42, Ar_46, Ar_52)) [ Ar_42 - Ar_43 >= 0 /\ -Ar_42 + Ar_43 >= 0 /\ -Ar_0 + 1 >= 0 /\ Ar_0 - 1 >= 0 /\ 0 >= Ar_2 /\ Ar_42 = Ar_43 /\ Ar_0 = 1 ] (Comp: 3, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, Fresh_11 - 1, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_13, Ar_35, Fresh_14, Fresh_15, Fresh_16, Fresh_17, 0, 0, Ar_46, Ar_52)) [ Ar_42 - Ar_43 >= 0 /\ -Ar_42 + Ar_43 >= 0 /\ -Ar_0 + 1 >= 0 /\ Ar_0 - 1 >= 0 /\ Ar_2 >= 1 /\ Fresh_11 >= 2 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: 1, Cost: 1) f16(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(1, Ar_1, 0, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Fresh_1, Ar_35, Fresh_2, Fresh_3, Fresh_4, Fresh_5, 0, 0, Ar_46, Ar_52)) [ Ar_42 - Ar_43 >= 0 /\ -Ar_42 + Ar_43 >= 0 /\ -Ar_0 + 1 >= 0 /\ Ar_0 - 1 >= 0 /\ Ar_2 >= 1 /\ Ar_42 = 0 /\ Ar_43 = 0 /\ Ar_0 = 1 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f1(Fresh_52, 2, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_52, Ar_30, Fresh_54, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_30)) [ Fresh_52 >= 2 /\ Ar_30 = Ar_52 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f16(1, Fresh_39, Fresh_40, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_42, Fresh_43, Fresh_44, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_30, Ar_30, Ar_46, Fresh_47)) [ Ar_30 = Ar_52 ] (Comp: 1, Cost: 1) f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f20(Fresh_23, Fresh_24, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Fresh_26, Fresh_27, Fresh_28, Fresh_31, Ar_35, Fresh_32, Fresh_33, Fresh_34, Fresh_35, 0, 0, Ar_46, Fresh_37)) [ 0 >= Fresh_23 ] (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52) -> Com_1(f19(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_21, Ar_24, Ar_28, Ar_29, Ar_30, Ar_34, Ar_35, Ar_37, Ar_38, Ar_39, Ar_40, Ar_42, Ar_43, Ar_46, Ar_52)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Complexity upper bound ? Time: 19.630 sec (SMT: 16.595 sec)