WORST_CASE(?, O(1))

Initial complexity problem:
1:	T:
		(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) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2, Fresh_51, Fresh_52, 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, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35)) [ Ar_0 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ K1 >= 1 /\ Ar_2 >= 1 /\ Ar_3 >= 0 /\ Ar_4 = Ar_2 + 1 ]
		(Comp: ?, Cost: 1)    f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Fresh_49 - 1, Ar_4, 0, Fresh_50, Ar_7, Fresh_49, -1, 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_0 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_8 >= Ar_0 /\ Ar_1 >= 0 /\ Fresh_49 >= 1 /\ Ar_4 >= 1 /\ Ar_5 = 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) -> Com_1(f13(1, Ar_1, Ar_2, Ar_3, Ar_10 + 2, Fresh_47, Fresh_48, Ar_7, Ar_8, Ar_9, Ar_10, Ar_12, 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)) [ K1 >= 1 /\ Ar_10 >= 1 /\ Ar_4 = Ar_10 + 1 /\ Ar_0 = 1 ]
		(Comp: ?, Cost: 1)    f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Fresh_43, Ar_13 + 2, Fresh_44, Fresh_45, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Fresh_46, Ar_13 + 1, Fresh_43, 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_0 >= 2 /\ Ar_4 >= 1 /\ Ar_13 >= 1 /\ Fresh_43 >= 0 /\ Ar_3 >= 0 /\ Ar_5 = 0 ]
		(Comp: ?, Cost: 1)    f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Fresh_41, Ar_4, 0, Fresh_42, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_16, Fresh_41, 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_0 >= 2 /\ Ar_4 >= 1 /\ Fresh_41 >= 0 /\ Ar_3 >= 0 /\ Ar_5 = 0 /\ Ar_16 = Ar_17 ]
		(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) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Fresh_38, Ar_19 + 2, Fresh_39, Fresh_40, 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, Fresh_38, 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_0 >= 2 /\ Ar_19 >= 1 /\ N1 >= 1 /\ Fresh_38 >= 0 /\ Ar_3 >= 0 /\ Ar_4 = Ar_19 + 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) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Fresh_36, Ar_4, 0, Fresh_37, 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_16, Fresh_36, 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_0 >= 2 /\ Ar_4 >= 1 /\ Fresh_36 >= 0 /\ Ar_3 >= 0 /\ Ar_5 = 0 /\ Ar_16 = Ar_21 ]
		(Comp: ?, Cost: 1)    f17(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) -> Com_1(f17(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_0, Ar_1 - 1, Ar_28, Ar_25, Ar_28, Fresh_35, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35)) [ Ar_23 >= Ar_1 /\ Ar_23 >= M1 + 1 /\ M1 >= 0 /\ Ar_23 >= 2 /\ Ar_24 + 1 = Ar_1 /\ Ar_0 = Ar_23 /\ Ar_25 = Ar_26 /\ Ar_27 = Ar_26 ]
		(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) -> Com_1(f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Fresh_34, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35)) [ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_4 /\ Ar_0 >= 2 ]
		(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) -> Com_1(f7(1, Ar_1, Ar_2, Ar_3, Ar_4, 0, Fresh_32, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, 0, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Fresh_33, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35)) [ Ar_4 >= 1 /\ Ar_16 = 0 /\ Ar_0 = 1 /\ Ar_5 = 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) -> Com_1(f7(1, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Fresh_31, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35)) [ 0 >= Ar_4 /\ Ar_0 = 1 ]
		(Comp: ?, Cost: 1)    f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35) -> Com_1(f7(Ar_0, Ar_1, Ar_2, 0, Ar_4, 0, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, 0, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Fresh_30, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35)) [ Ar_4 >= 1 /\ Ar_0 >= 2 /\ Ar_16 = 0 /\ Ar_5 = 0 /\ Ar_3 = 0 ]
		(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) -> Com_1(f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Fresh_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35)) [ Ar_3 >= 0 /\ 0 >= Ar_4 /\ Ar_0 >= 2 ]
		(Comp: ?, Cost: 1)    f6(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) -> Com_1(f7(Fresh_19, Fresh_20, Ar_2, Ar_3, 100, Ar_5, Fresh_21, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, 0, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Fresh_22, Ar_24, Fresh_23, Fresh_24, Fresh_25, Fresh_26, Fresh_27, Fresh_28, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35)) [ 0 >= Fresh_19 /\ Ar_16 = 0 /\ Ar_4 = 100 /\ Ar_1 = 0 /\ Ar_0 = Ar_23 /\ Ar_25 = 0 ]
		(Comp: ?, Cost: 1)    f17(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) -> Com_1(f15(Ar_0, Fresh_9, Ar_2, Ar_3, 102, Fresh_10, Fresh_11, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_25, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Fresh_12, Ar_24, Fresh_13, Fresh_14, Fresh_15, Fresh_16, Fresh_17, Fresh_18, 101, Fresh_9, Ar_1, Ar_34, Ar_35)) [ Ar_3 >= 0 /\ Ar_1 >= Ar_23 /\ Ar_1 >= 0 /\ Fresh_9 >= Ar_23 /\ Fresh_9 >= 0 /\ Ar_23 >= 2 /\ Ar_4 = 100 /\ Ar_0 = Ar_23 /\ Ar_25 = Ar_26 /\ Ar_27 = Ar_26 ]
		(Comp: ?, Cost: 1)    f17(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) -> Com_1(f14(Ar_0, Fresh_0, Ar_2, Ar_3, 100, 0, Fresh_1, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_35, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Fresh_2, Ar_24, Fresh_3, Fresh_4, Fresh_5, Fresh_6, Fresh_7, Fresh_8, Ar_31, Ar_32, Ar_1, Ar_34, Ar_35)) [ Ar_3 >= 0 /\ Ar_1 >= Ar_23 /\ Ar_1 >= 0 /\ Fresh_0 >= Ar_23 /\ Fresh_0 >= 0 /\ Ar_23 >= 2 /\ Ar_34 >= Ar_23 /\ Ar_4 = 100 /\ Ar_5 = 0 /\ Ar_0 = Ar_23 /\ Ar_35 = Ar_26 /\ Ar_25 = Ar_26 /\ Ar_27 = Ar_26 ]
		(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) -> Com_1(f6(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)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35].
We thus obtain the following problem:
2:	T:
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ 0 <= 0 ]
		(Comp: ?, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f14(Ar_0, Fresh_0, Ar_2, Ar_3, 100, 0, Ar_8, Ar_10, Ar_13, Ar_35, Ar_17, Ar_19, Ar_21, Fresh_2, Ar_24, Fresh_3, Fresh_4, Fresh_5, Fresh_6, Ar_34, Ar_35)) [ Ar_3 >= 0 /\ Ar_1 >= Ar_23 /\ Ar_1 >= 0 /\ Fresh_0 >= Ar_23 /\ Fresh_0 >= 0 /\ Ar_23 >= 2 /\ Ar_34 >= Ar_23 /\ Ar_4 = 100 /\ Ar_5 = 0 /\ Ar_0 = Ar_23 /\ Ar_35 = Ar_26 /\ Ar_25 = Ar_26 /\ Ar_27 = Ar_26 ]
		(Comp: ?, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f15(Ar_0, Fresh_9, Ar_2, Ar_3, 102, Fresh_10, Ar_8, Ar_10, Ar_13, Ar_25, Ar_17, Ar_19, Ar_21, Fresh_12, Ar_24, Fresh_13, Fresh_14, Fresh_15, Fresh_16, Ar_34, Ar_35)) [ Ar_3 >= 0 /\ Ar_1 >= Ar_23 /\ Ar_1 >= 0 /\ Fresh_9 >= Ar_23 /\ Fresh_9 >= 0 /\ Ar_23 >= 2 /\ Ar_4 = 100 /\ Ar_0 = Ar_23 /\ Ar_25 = Ar_26 /\ Ar_27 = Ar_26 ]
		(Comp: ?, Cost: 1)    f6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f7(Fresh_19, Fresh_20, Ar_2, Ar_3, 100, Ar_5, Ar_8, Ar_10, Ar_13, 0, Ar_17, Ar_19, Ar_21, Fresh_22, Ar_24, Fresh_23, Fresh_24, Fresh_25, Fresh_26, Ar_34, Ar_35)) [ 0 >= Fresh_19 /\ Ar_16 = 0 /\ Ar_4 = 100 /\ Ar_1 = 0 /\ Ar_0 = Ar_23 /\ Ar_25 = 0 ]
		(Comp: ?, Cost: 1)    f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_3 >= 0 /\ 0 >= Ar_4 /\ Ar_0 >= 2 ]
		(Comp: ?, Cost: 1)    f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f7(Ar_0, Ar_1, Ar_2, 0, Ar_4, 0, Ar_8, Ar_10, Ar_13, 0, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_4 >= 1 /\ Ar_0 >= 2 /\ Ar_16 = 0 /\ Ar_5 = 0 /\ Ar_3 = 0 ]
		(Comp: ?, Cost: 1)    f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f7(1, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ 0 >= Ar_4 /\ Ar_0 = 1 ]
		(Comp: ?, Cost: 1)    f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f7(1, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_8, Ar_10, Ar_13, 0, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_4 >= 1 /\ Ar_16 = 0 /\ Ar_0 = 1 /\ Ar_5 = 0 ]
		(Comp: ?, Cost: 1)    f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_4 /\ Ar_0 >= 2 ]
		(Comp: ?, Cost: 1)    f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f17(Ar_0, Ar_1 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_0, Ar_1 - 1, Ar_28, Ar_25, Ar_28, Fresh_35, Ar_34, Ar_35)) [ Ar_23 >= Ar_1 /\ Ar_23 >= M1 + 1 /\ M1 >= 0 /\ Ar_23 >= 2 /\ Ar_24 + 1 = Ar_1 /\ Ar_0 = Ar_23 /\ Ar_25 = Ar_26 /\ Ar_27 = Ar_26 ]
		(Comp: ?, Cost: 1)    f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Fresh_36, Ar_4, 0, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_16, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_0 >= 2 /\ Ar_4 >= 1 /\ Fresh_36 >= 0 /\ Ar_3 >= 0 /\ Ar_5 = 0 /\ Ar_16 = Ar_21 ]
		(Comp: ?, Cost: 1)    f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Fresh_38, Ar_19 + 2, Fresh_39, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_0 >= 2 /\ Ar_19 >= 1 /\ N1 >= 1 /\ Fresh_38 >= 0 /\ Ar_3 >= 0 /\ Ar_4 = Ar_19 + 1 ]
		(Comp: ?, Cost: 1)    f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Fresh_41, Ar_4, 0, Ar_8, Ar_10, Ar_13, Ar_16, Ar_16, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_0 >= 2 /\ Ar_4 >= 1 /\ Fresh_41 >= 0 /\ Ar_3 >= 0 /\ Ar_5 = 0 /\ Ar_16 = Ar_17 ]
		(Comp: ?, Cost: 1)    f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Fresh_43, Ar_13 + 2, Fresh_44, Ar_8, Ar_10, Fresh_46, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_0 >= 2 /\ Ar_4 >= 1 /\ Ar_13 >= 1 /\ Fresh_43 >= 0 /\ Ar_3 >= 0 /\ Ar_5 = 0 ]
		(Comp: ?, Cost: 1)    f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f13(1, Ar_1, Ar_2, Ar_3, Ar_10 + 2, Fresh_47, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ K1 >= 1 /\ Ar_10 >= 1 /\ Ar_4 = Ar_10 + 1 /\ Ar_0 = 1 ]
		(Comp: ?, Cost: 1)    f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Fresh_49 - 1, Ar_4, 0, Fresh_49, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_0 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_8 >= Ar_0 /\ Ar_1 >= 0 /\ Fresh_49 >= 1 /\ Ar_4 >= 1 /\ Ar_5 = 0 ]
		(Comp: ?, Cost: 1)    f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2, Fresh_51, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_0 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ K1 >= 1 /\ Ar_2 >= 1 /\ Ar_3 >= 0 /\ Ar_4 = Ar_2 + 1 ]
	start location:	koat_start
	leaf cost:	0

Testing for reachability in the complexity graph removes the following transitions from problem 2:
	f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f14(Ar_0, Fresh_0, Ar_2, Ar_3, 100, 0, Ar_8, Ar_10, Ar_13, Ar_35, Ar_17, Ar_19, Ar_21, Fresh_2, Ar_24, Fresh_3, Fresh_4, Fresh_5, Fresh_6, Ar_34, Ar_35)) [ Ar_3 >= 0 /\ Ar_1 >= Ar_23 /\ Ar_1 >= 0 /\ Fresh_0 >= Ar_23 /\ Fresh_0 >= 0 /\ Ar_23 >= 2 /\ Ar_34 >= Ar_23 /\ Ar_4 = 100 /\ Ar_5 = 0 /\ Ar_0 = Ar_23 /\ Ar_35 = Ar_26 /\ Ar_25 = Ar_26 /\ Ar_27 = Ar_26 ]
	f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f15(Ar_0, Fresh_9, Ar_2, Ar_3, 102, Fresh_10, Ar_8, Ar_10, Ar_13, Ar_25, Ar_17, Ar_19, Ar_21, Fresh_12, Ar_24, Fresh_13, Fresh_14, Fresh_15, Fresh_16, Ar_34, Ar_35)) [ Ar_3 >= 0 /\ Ar_1 >= Ar_23 /\ Ar_1 >= 0 /\ Fresh_9 >= Ar_23 /\ Fresh_9 >= 0 /\ Ar_23 >= 2 /\ Ar_4 = 100 /\ Ar_0 = Ar_23 /\ Ar_25 = Ar_26 /\ Ar_27 = Ar_26 ]
	f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_3 >= 0 /\ 0 >= Ar_4 /\ Ar_0 >= 2 ]
	f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f7(Ar_0, Ar_1, Ar_2, 0, Ar_4, 0, Ar_8, Ar_10, Ar_13, 0, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_4 >= 1 /\ Ar_0 >= 2 /\ Ar_16 = 0 /\ Ar_5 = 0 /\ Ar_3 = 0 ]
	f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f7(1, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ 0 >= Ar_4 /\ Ar_0 = 1 ]
	f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f7(1, Ar_1, Ar_2, Ar_3, Ar_4, 0, Ar_8, Ar_10, Ar_13, 0, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_4 >= 1 /\ Ar_16 = 0 /\ Ar_0 = 1 /\ Ar_5 = 0 ]
	f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f7(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ 0 >= Ar_4 /\ Ar_0 >= 2 ]
	f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f17(Ar_0, Ar_1 + 1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_0, Ar_1 - 1, Ar_28, Ar_25, Ar_28, Fresh_35, Ar_34, Ar_35)) [ Ar_23 >= Ar_1 /\ Ar_23 >= M1 + 1 /\ M1 >= 0 /\ Ar_23 >= 2 /\ Ar_24 + 1 = Ar_1 /\ Ar_0 = Ar_23 /\ Ar_25 = Ar_26 /\ Ar_27 = Ar_26 ]
	f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Fresh_36, Ar_4, 0, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_16, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_0 >= 2 /\ Ar_4 >= 1 /\ Fresh_36 >= 0 /\ Ar_3 >= 0 /\ Ar_5 = 0 /\ Ar_16 = Ar_21 ]
	f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Fresh_38, Ar_19 + 2, Fresh_39, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_0 >= 2 /\ Ar_19 >= 1 /\ N1 >= 1 /\ Fresh_38 >= 0 /\ Ar_3 >= 0 /\ Ar_4 = Ar_19 + 1 ]
	f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Fresh_41, Ar_4, 0, Ar_8, Ar_10, Ar_13, Ar_16, Ar_16, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_0 >= 2 /\ Ar_4 >= 1 /\ Fresh_41 >= 0 /\ Ar_3 >= 0 /\ Ar_5 = 0 /\ Ar_16 = Ar_17 ]
	f14(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Fresh_43, Ar_13 + 2, Fresh_44, Ar_8, Ar_10, Fresh_46, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_0 >= 2 /\ Ar_4 >= 1 /\ Ar_13 >= 1 /\ Fresh_43 >= 0 /\ Ar_3 >= 0 /\ Ar_5 = 0 ]
	f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f13(1, Ar_1, Ar_2, Ar_3, Ar_10 + 2, Fresh_47, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ K1 >= 1 /\ Ar_10 >= 1 /\ Ar_4 = Ar_10 + 1 /\ Ar_0 = 1 ]
	f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f14(Ar_0, Ar_1, Ar_2, Fresh_49 - 1, Ar_4, 0, Fresh_49, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_0 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_8 >= Ar_0 /\ Ar_1 >= 0 /\ Fresh_49 >= 1 /\ Ar_4 >= 1 /\ Ar_5 = 0 ]
	f11(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2, Fresh_51, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ Ar_0 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ K1 >= 1 /\ Ar_2 >= 1 /\ Ar_3 >= 0 /\ Ar_4 = Ar_2 + 1 ]
We thus obtain the following problem:
3:	T:
		(Comp: ?, Cost: 1)    f6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f7(Fresh_19, Fresh_20, Ar_2, Ar_3, 100, Ar_5, Ar_8, Ar_10, Ar_13, 0, Ar_17, Ar_19, Ar_21, Fresh_22, Ar_24, Fresh_23, Fresh_24, Fresh_25, Fresh_26, Ar_34, Ar_35)) [ 0 >= Fresh_19 /\ Ar_16 = 0 /\ Ar_4 = 100 /\ Ar_1 = 0 /\ Ar_0 = Ar_23 /\ Ar_25 = 0 ]
		(Comp: 1, Cost: 0)    koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35) -> Com_1(f6(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_8, Ar_10, Ar_13, Ar_16, Ar_17, Ar_19, Ar_21, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_34, Ar_35)) [ 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_4, Ar_16, Ar_23, Ar_25) -> Com_1(f6(Ar_0, Ar_1, Ar_4, Ar_16, Ar_23, Ar_25)) [ 0 <= 0 ]
		(Comp: 1, Cost: 1)    f6(Ar_0, Ar_1, Ar_4, Ar_16, Ar_23, Ar_25) -> Com_1(f7(Fresh_19, Fresh_20, 100, 0, Fresh_22, Fresh_23)) [ 0 >= Fresh_19 /\ Ar_16 = 0 /\ Ar_4 = 100 /\ Ar_1 = 0 /\ Ar_0 = Ar_23 /\ Ar_25 = 0 ]
	start location:	koat_start
	leaf cost:	0

Complexity upper bound 1

Time: 0.798 sec (SMT: 0.717 sec)