MAYBE Initial complexity problem: 1: T: (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) -> Com_1(f15(Ar_0, Ar_1 + 1, Ar_3, Fresh_450, Ar_3, Fresh_451, Ar_1, 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_0 >= Ar_1 + 1 /\ Ar_1 >= 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) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7 + 1, Ar_8 - 1, Fresh_437, Fresh_438, Fresh_439, Fresh_439, Fresh_440, Fresh_441, 0, Fresh_442, Fresh_443, Fresh_444, Fresh_445, Fresh_446, Fresh_447, 0, Fresh_448, Ar_25, Ar_25, Fresh_449, Ar_7 + 1, Ar_8 - 1, 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_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_437 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_439 + 1 /\ 0 >= Fresh_449 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7 + 1, Ar_8 - 1, Fresh_424, Fresh_425, Fresh_426, Fresh_426, Fresh_427, Fresh_428, 0, Fresh_429, Fresh_430, Fresh_431, Fresh_432, Fresh_433, Fresh_434, 0, Fresh_435, Ar_25, Ar_25, Fresh_436, Ar_7 + 1, Ar_8 - 1, 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_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_424 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_426 + 1 /\ Fresh_436 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7 + 1, Ar_8 - 1, Fresh_411, Fresh_412, Fresh_413, Fresh_413, Fresh_414, Fresh_415, 0, Fresh_416, Fresh_417, Fresh_418, Fresh_419, Fresh_420, Fresh_421, 0, Fresh_422, Ar_25, Ar_25, Fresh_423, Ar_7 + 1, Ar_8 - 1, 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_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_411 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_413 >= 1 /\ 0 >= Fresh_423 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7 + 1, Ar_8 - 1, Fresh_398, Fresh_399, Fresh_400, Fresh_400, Fresh_401, Fresh_402, 0, Fresh_403, Fresh_404, Fresh_405, Fresh_406, Fresh_407, Fresh_408, 0, Fresh_409, Ar_25, Ar_25, Fresh_410, Ar_7 + 1, Ar_8 - 1, 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_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_398 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_400 >= 1 /\ Fresh_410 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7 + 1, Ar_8 - 1, Fresh_385, Fresh_386, Fresh_387, Fresh_387, Fresh_388, Fresh_389, 0, Fresh_390, Fresh_391, Fresh_392, Fresh_393, Fresh_394, Fresh_395, 0, Fresh_396, Ar_25, Ar_25, Fresh_397, Ar_7 + 1, Ar_8 - 1, 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_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_385 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_387 + 1 /\ 0 >= Fresh_397 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7 + 1, Ar_8 - 1, Fresh_372, Fresh_373, Fresh_374, Fresh_374, Fresh_375, Fresh_376, 0, Fresh_377, Fresh_378, Fresh_379, Fresh_380, Fresh_381, Fresh_382, 0, Fresh_383, Ar_25, Ar_25, Fresh_384, Ar_7 + 1, Ar_8 - 1, 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_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_372 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_374 + 1 /\ Fresh_384 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7 + 1, Ar_8 - 1, Fresh_359, Fresh_360, Fresh_361, Fresh_361, Fresh_362, Fresh_363, 0, Fresh_364, Fresh_365, Fresh_366, Fresh_367, Fresh_368, Fresh_369, 0, Fresh_370, Ar_25, Ar_25, Fresh_371, Ar_7 + 1, Ar_8 - 1, 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_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_359 >= 2 /\ Z1 >= 1 /\ Fresh_361 >= 1 /\ 0 >= Fresh_371 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7 + 1, Ar_8 - 1, Fresh_346, Fresh_347, Fresh_348, Fresh_348, Fresh_349, Fresh_350, 0, Fresh_351, Fresh_352, Fresh_353, Fresh_354, Fresh_355, Fresh_356, 0, Fresh_357, Ar_25, Ar_25, Fresh_358, Ar_7 + 1, Ar_8 - 1, 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_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_346 >= 2 /\ Z1 >= 1 /\ Fresh_348 >= 1 /\ Fresh_358 >= 1 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_344, Ar_10, Fresh_345, 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, 0, Fresh_345, 0, Fresh_345, Ar_29, 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)) [ A2 >= Ar_29 + 1 /\ Ar_30 >= 0 /\ Fresh_344 >= 2 /\ Fresh_345 >= A2 + 1 /\ 0 >= Fresh_345 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_342, Ar_10, Fresh_343, 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, 0, Fresh_343, 0, Fresh_343, Ar_29, 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)) [ A2 >= Ar_29 + 1 /\ Ar_30 >= 0 /\ Fresh_342 >= 2 /\ Fresh_343 >= A2 + 1 /\ Fresh_343 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_340, Ar_10, Fresh_341, 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, 0, Fresh_341, 0, Fresh_341, Ar_29, 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)) [ A2 >= Ar_29 + 1 /\ Ar_30 >= 0 /\ Fresh_340 >= 2 /\ A2 >= Fresh_341 + 1 /\ 0 >= Fresh_341 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_338, Ar_10, Fresh_339, 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, 0, Fresh_339, 0, Fresh_339, Ar_29, 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)) [ A2 >= Ar_29 + 1 /\ Ar_30 >= 0 /\ Fresh_338 >= 2 /\ A2 >= Fresh_339 + 1 /\ Fresh_339 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_336, Ar_10, Fresh_337, 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, 0, Fresh_337, 0, Fresh_337, Ar_29, 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_29 >= A2 + 1 /\ Ar_30 >= 0 /\ Fresh_336 >= 2 /\ Fresh_337 >= A2 + 1 /\ 0 >= Fresh_337 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_334, Ar_10, Fresh_335, 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, 0, Fresh_335, 0, Fresh_335, Ar_29, 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_29 >= A2 + 1 /\ Ar_30 >= 0 /\ Fresh_334 >= 2 /\ Fresh_335 >= A2 + 1 /\ Fresh_335 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_332, Ar_10, Fresh_333, 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, 0, Fresh_333, 0, Fresh_333, Ar_29, 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_29 >= A2 + 1 /\ Ar_30 >= 0 /\ Fresh_332 >= 2 /\ A2 >= Fresh_333 + 1 /\ 0 >= Fresh_333 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_330, Ar_10, Fresh_331, 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, 0, Fresh_331, 0, Fresh_331, Ar_29, 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_29 >= A2 + 1 /\ Ar_30 >= 0 /\ Fresh_330 >= 2 /\ A2 >= Fresh_331 + 1 /\ Fresh_331 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_321, Fresh_322, Fresh_323, 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_324, Ar_30, Fresh_325, Fresh_326, Fresh_327, Fresh_328, Fresh_329, 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_30 >= 0 /\ 0 >= Fresh_323 + 1 /\ Fresh_321 >= 2 /\ Ar_31 = Ar_29 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_312, Fresh_313, Fresh_314, 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_315, Ar_30, Fresh_316, Fresh_317, Fresh_318, Fresh_319, Fresh_320, 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_30 >= 0 /\ Fresh_314 >= 1 /\ Fresh_312 >= 2 /\ Ar_31 = Ar_29 ] (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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_309, Ar_10, Fresh_310, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Fresh_311, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, 0, Fresh_310, 0, Fresh_310, Ar_29, Ar_36 - 1, Ar_36 - 1, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_309 >= 2 /\ Fresh_310 >= C2 + 1 /\ 0 >= Fresh_310 + 1 /\ Ar_31 = 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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_306, Ar_10, Fresh_307, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Fresh_308, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, 0, Fresh_307, 0, Fresh_307, Ar_29, Ar_36 - 1, Ar_36 - 1, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_306 >= 2 /\ Fresh_307 >= C2 + 1 /\ Fresh_307 >= 1 /\ Ar_31 = 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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_303, Ar_10, Fresh_304, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Fresh_305, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, 0, Fresh_304, 0, Fresh_304, Ar_29, Ar_36 - 1, Ar_36 - 1, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_303 >= 2 /\ C2 >= Fresh_304 + 1 /\ 0 >= Fresh_304 + 1 /\ Ar_31 = 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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_300, Ar_10, Fresh_301, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Fresh_302, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, 0, Fresh_301, 0, Fresh_301, Ar_29, Ar_36 - 1, Ar_36 - 1, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_300 >= 2 /\ C2 >= Fresh_301 + 1 /\ Fresh_301 >= 1 /\ Ar_31 = 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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_297, Ar_10, Fresh_298, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Fresh_299, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, 0, Fresh_298, 0, Fresh_298, Ar_29, Ar_36 - 1, Ar_36 - 1, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_297 >= 2 /\ Fresh_298 >= C2 + 1 /\ 0 >= Fresh_298 + 1 /\ Ar_31 = 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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_294, Ar_10, Fresh_295, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Fresh_296, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, 0, Fresh_295, 0, Fresh_295, Ar_29, Ar_36 - 1, Ar_36 - 1, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_294 >= 2 /\ Fresh_295 >= C2 + 1 /\ Fresh_295 >= 1 /\ Ar_31 = 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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_291, Ar_10, Fresh_292, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Fresh_293, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, 0, Fresh_292, 0, Fresh_292, Ar_29, Ar_36 - 1, Ar_36 - 1, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_291 >= 2 /\ C2 >= Fresh_292 + 1 /\ 0 >= Fresh_292 + 1 /\ Ar_31 = 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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_288, Ar_10, Fresh_289, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Fresh_290, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, 0, Fresh_289, 0, Fresh_289, Ar_29, Ar_36 - 1, Ar_36 - 1, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_288 >= 2 /\ C2 >= Fresh_289 + 1 /\ Fresh_289 >= 1 /\ Ar_31 = 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) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_280, Fresh_281, 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_282, Ar_30, Fresh_283, Fresh_284, Fresh_285, Fresh_286, Fresh_287, 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)) [ Fresh_280 >= 2 /\ Ar_36 >= 0 /\ Ar_31 = Ar_29 ] (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, 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) -> Com_1(f15(Fresh_275, 2, Fresh_276, Fresh_277, Fresh_276, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_275, 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, Fresh_278, Fresh_276, Fresh_279, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48)) [ Fresh_275 >= 2 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_1(f13(Fresh_253, Fresh_254, Fresh_255, Fresh_256, Fresh_257, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_258, Fresh_259, Fresh_260, Fresh_260, Fresh_261, Fresh_262, 0, Fresh_263, Fresh_264, Fresh_265, Fresh_266, Fresh_267, Fresh_268, 0, Ar_23, Ar_24, Ar_2, 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, Fresh_269, Ar_40, Ar_41, Fresh_270, Fresh_271, Fresh_272, Fresh_273, Fresh_274, Ar_47, Ar_48)) [ L2 >= 2 /\ Fresh_272 >= L2 /\ Fresh_258 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_274 + 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_260 + 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) -> Com_1(f13(Fresh_231, Fresh_232, Fresh_233, Fresh_234, Fresh_235, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_236, Fresh_237, Fresh_238, Fresh_238, Fresh_239, Fresh_240, 0, Fresh_241, Fresh_242, Fresh_243, Fresh_244, Fresh_245, Fresh_246, 0, Ar_23, Ar_24, Ar_2, 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, Fresh_247, Ar_40, Ar_41, Fresh_248, Fresh_249, Fresh_250, Fresh_251, Fresh_252, Ar_47, Ar_48)) [ L2 >= 2 /\ Fresh_250 >= L2 /\ Fresh_236 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_252 + 1 /\ 0 >= Ar_2 + 1 /\ Fresh_238 >= 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) -> Com_1(f13(Fresh_209, Fresh_210, Fresh_211, Fresh_212, Fresh_213, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_214, Fresh_215, Fresh_216, Fresh_216, Fresh_217, Fresh_218, 0, Fresh_219, Fresh_220, Fresh_221, Fresh_222, Fresh_223, Fresh_224, 0, Ar_23, Ar_24, Ar_2, 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, Fresh_225, Ar_40, Ar_41, Fresh_226, Fresh_227, Fresh_228, Fresh_229, Fresh_230, Ar_47, Ar_48)) [ L2 >= 2 /\ Fresh_228 >= L2 /\ Fresh_214 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_230 + 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_216 + 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) -> Com_1(f13(Fresh_187, Fresh_188, Fresh_189, Fresh_190, Fresh_191, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_192, Fresh_193, Fresh_194, Fresh_194, Fresh_195, Fresh_196, 0, Fresh_197, Fresh_198, Fresh_199, Fresh_200, Fresh_201, Fresh_202, 0, Ar_23, Ar_24, Ar_2, 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, Fresh_203, Ar_40, Ar_41, Fresh_204, Fresh_205, Fresh_206, Fresh_207, Fresh_208, Ar_47, Ar_48)) [ L2 >= 2 /\ Fresh_206 >= L2 /\ Fresh_192 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_208 + 1 /\ Ar_2 >= 1 /\ Fresh_194 >= 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) -> Com_1(f13(Fresh_165, Fresh_166, Fresh_167, Fresh_168, Fresh_169, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_170, Fresh_171, Fresh_172, Fresh_172, Fresh_173, Fresh_174, 0, Fresh_175, Fresh_176, Fresh_177, Fresh_178, Fresh_179, Fresh_180, 0, Ar_23, Ar_24, Ar_2, 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, Fresh_181, Ar_40, Ar_41, Fresh_182, Fresh_183, Fresh_184, Fresh_185, Fresh_186, Ar_47, Ar_48)) [ L2 >= 2 /\ Fresh_184 >= L2 /\ Fresh_170 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_186 >= 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_172 + 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) -> Com_1(f13(Fresh_143, Fresh_144, Fresh_145, Fresh_146, Fresh_147, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_148, Fresh_149, Fresh_150, Fresh_150, Fresh_151, Fresh_152, 0, Fresh_153, Fresh_154, Fresh_155, Fresh_156, Fresh_157, Fresh_158, 0, Ar_23, Ar_24, Ar_2, 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, Fresh_159, Ar_40, Ar_41, Fresh_160, Fresh_161, Fresh_162, Fresh_163, Fresh_164, Ar_47, Ar_48)) [ L2 >= 2 /\ Fresh_162 >= L2 /\ Fresh_148 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_164 >= 1 /\ 0 >= Ar_2 + 1 /\ Fresh_150 >= 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) -> Com_1(f13(Fresh_121, Fresh_122, Fresh_123, Fresh_124, Fresh_125, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_126, Fresh_127, Fresh_128, Fresh_128, Fresh_129, Fresh_130, 0, Fresh_131, Fresh_132, Fresh_133, Fresh_134, Fresh_135, Fresh_136, 0, Ar_23, Ar_24, Ar_2, 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, Fresh_137, Ar_40, Ar_41, Fresh_138, Fresh_139, Fresh_140, Fresh_141, Fresh_142, Ar_47, Ar_48)) [ L2 >= 2 /\ Fresh_140 >= L2 /\ Fresh_126 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_142 >= 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_128 + 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) -> Com_1(f13(Fresh_99, Fresh_100, Fresh_101, Fresh_102, Fresh_103, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_104, Fresh_105, Fresh_106, Fresh_106, Fresh_107, Fresh_108, 0, Fresh_109, Fresh_110, Fresh_111, Fresh_112, Fresh_113, Fresh_114, 0, Ar_23, Ar_24, Ar_2, 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, Fresh_115, Ar_40, Ar_41, Fresh_116, Fresh_117, Fresh_118, Fresh_119, Fresh_120, Ar_47, Ar_48)) [ L2 >= 2 /\ Fresh_118 >= L2 /\ Fresh_104 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_120 >= 1 /\ Ar_2 >= 1 /\ Fresh_106 >= 1 ] (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, 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) -> Com_1(f0(Fresh_68, Fresh_69, Fresh_70, Fresh_71, Fresh_72, Ar_5, Ar_6, Ar_7, Ar_8, Fresh_73, Fresh_74, 0, Fresh_75, Fresh_76, Fresh_77, Fresh_78, Fresh_79, Fresh_80, Fresh_81, Fresh_82, Fresh_83, Fresh_84, Fresh_85, Ar_23, Ar_24, Fresh_86, Ar_26, Ar_27, Ar_28, Fresh_87, Ar_30, Fresh_88, Fresh_89, Fresh_90, Fresh_91, Fresh_92, Ar_36, Ar_37, Fresh_93, Fresh_94, Ar_40, Ar_41, Fresh_95, Fresh_96, Ar_44, Ar_45, Ar_46, Fresh_97, Fresh_98)) [ 0 >= U2 /\ 0 >= Fresh_73 /\ 0 >= V2 ] (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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_36 + 1, Ar_8, Fresh_51, Fresh_52, Ar_11, Fresh_53, Fresh_54, Fresh_55, Fresh_56, Fresh_57, Fresh_58, Fresh_59, Fresh_60, Fresh_61, Fresh_62, Fresh_63, Ar_23, Ar_24, Fresh_64, Ar_26, Ar_27, Ar_28, Ar_11, Ar_36, 0, Ar_11, 0, Ar_11, Ar_11, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Fresh_65, Ar_44, Ar_45, Ar_46, Fresh_66, Fresh_67)) [ Q2 >= 2 /\ Fresh_51 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ Ar_11 >= 1 /\ 0 >= Ar_11 + 1 /\ Ar_25 = 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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_36 + 1, Ar_8, Fresh_34, Fresh_35, Ar_11, Fresh_36, Fresh_37, Fresh_38, Fresh_39, Fresh_40, Fresh_41, Fresh_42, Fresh_43, Fresh_44, Fresh_45, Fresh_46, Ar_23, Ar_24, Fresh_47, Ar_26, Ar_27, Ar_28, Ar_11, Ar_36, 0, Ar_11, 0, Ar_11, Ar_11, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Fresh_48, Ar_44, Ar_45, Ar_46, Fresh_49, Fresh_50)) [ Q2 >= 2 /\ Fresh_34 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ Ar_11 >= 1 /\ Ar_25 = 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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_36 + 1, Ar_8, Fresh_17, Fresh_18, Ar_11, Fresh_19, Fresh_20, Fresh_21, Fresh_22, Fresh_23, Fresh_24, Fresh_25, Fresh_26, Fresh_27, Fresh_28, Fresh_29, Ar_23, Ar_24, Fresh_30, Ar_26, Ar_27, Ar_28, Ar_11, Ar_36, 0, Ar_11, 0, Ar_11, Ar_11, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Fresh_31, Ar_44, Ar_45, Ar_46, Fresh_32, Fresh_33)) [ Q2 >= 2 /\ Fresh_17 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_25 = 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) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_36 + 1, Ar_8, Fresh_0, Fresh_1, Ar_11, Fresh_2, Fresh_3, Fresh_4, Fresh_5, Fresh_6, Fresh_7, Fresh_8, Fresh_9, Fresh_10, Fresh_11, Fresh_12, Ar_23, Ar_24, Fresh_13, Ar_26, Ar_27, Ar_28, Ar_11, Ar_36, 0, Ar_11, 0, Ar_11, Ar_11, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Fresh_14, Ar_44, Ar_45, Ar_46, Fresh_15, Fresh_16)) [ Q2 >= 2 /\ Fresh_0 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_11 >= 1 /\ Ar_25 = 0 ] (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4, Ar_5, Ar_6, Ar_7, Ar_8, Ar_9, Ar_10, Ar_11, Ar_12, Ar_13, Ar_14, Ar_15, Ar_16, Ar_17, Ar_18, Ar_19, Ar_20, Ar_21, Ar_22, Ar_23, Ar_24, Ar_25, Ar_26, Ar_27, Ar_28, Ar_29, Ar_30, Ar_31, Ar_32, Ar_33, Ar_34, Ar_35, Ar_36, Ar_37, Ar_38, Ar_39, Ar_40, Ar_41, Ar_42, Ar_43, Ar_44, Ar_45, Ar_46, Ar_47, Ar_48) -> Com_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, 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)) [ 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_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41]. We thus obtain the following problem: 2: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ 0 <= 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_13, Ar_11, Ar_36, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_0 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_11 >= 1 /\ Ar_25 = 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_30, Ar_11, Ar_36, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_17 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_25 = 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_47, Ar_11, Ar_36, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_34 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ Ar_11 >= 1 /\ Ar_25 = 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_64, Ar_11, Ar_36, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_51 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ Ar_11 >= 1 /\ 0 >= Ar_11 + 1 /\ Ar_25 = 0 ] (Comp: ?, Cost: 1) f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Fresh_68, Fresh_69, Fresh_70, Fresh_71, Ar_7, Ar_8, 0, Fresh_86, Fresh_87, Ar_30, Fresh_88, Ar_36, Ar_41)) [ 0 >= U2 /\ 0 >= Fresh_73 /\ 0 >= V2 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_99, Fresh_100, Fresh_101, Fresh_102, Ar_7, Ar_8, Fresh_106, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_118 >= L2 /\ Fresh_104 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_120 >= 1 /\ Ar_2 >= 1 /\ Fresh_106 >= 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_121, Fresh_122, Fresh_123, Fresh_124, Ar_7, Ar_8, Fresh_128, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_140 >= L2 /\ Fresh_126 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_142 >= 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_128 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_143, Fresh_144, Fresh_145, Fresh_146, Ar_7, Ar_8, Fresh_150, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_162 >= L2 /\ Fresh_148 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_164 >= 1 /\ 0 >= Ar_2 + 1 /\ Fresh_150 >= 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_165, Fresh_166, Fresh_167, Fresh_168, Ar_7, Ar_8, Fresh_172, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_184 >= L2 /\ Fresh_170 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_186 >= 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_172 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_187, Fresh_188, Fresh_189, Fresh_190, Ar_7, Ar_8, Fresh_194, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_206 >= L2 /\ Fresh_192 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_208 + 1 /\ Ar_2 >= 1 /\ Fresh_194 >= 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_209, Fresh_210, Fresh_211, Fresh_212, Ar_7, Ar_8, Fresh_216, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_228 >= L2 /\ Fresh_214 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_230 + 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_216 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_231, Fresh_232, Fresh_233, Fresh_234, Ar_7, Ar_8, Fresh_238, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_250 >= L2 /\ Fresh_236 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_252 + 1 /\ 0 >= Ar_2 + 1 /\ Fresh_238 >= 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_253, Fresh_254, Fresh_255, Fresh_256, Ar_7, Ar_8, Fresh_260, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_272 >= L2 /\ Fresh_258 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_274 + 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_260 + 1 ] (Comp: ?, Cost: 1) f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f15(Fresh_275, 2, Fresh_276, Fresh_277, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Fresh_275 >= 2 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Fresh_282, Ar_30, Fresh_283, Ar_36, Ar_41)) [ Fresh_280 >= 2 /\ Ar_36 >= 0 /\ Ar_31 = Ar_29 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_289, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_288 >= 2 /\ C2 >= Fresh_289 + 1 /\ Fresh_289 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_292, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_291 >= 2 /\ C2 >= Fresh_292 + 1 /\ 0 >= Fresh_292 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_295, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_294 >= 2 /\ Fresh_295 >= C2 + 1 /\ Fresh_295 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_298, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_297 >= 2 /\ Fresh_298 >= C2 + 1 /\ 0 >= Fresh_298 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_301, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_300 >= 2 /\ C2 >= Fresh_301 + 1 /\ Fresh_301 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_304, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_303 >= 2 /\ C2 >= Fresh_304 + 1 /\ 0 >= Fresh_304 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_307, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_306 >= 2 /\ Fresh_307 >= C2 + 1 /\ Fresh_307 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_310, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_309 >= 2 /\ Fresh_310 >= C2 + 1 /\ 0 >= Fresh_310 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_314, Ar_25, Fresh_315, Ar_30, Fresh_316, Ar_36, Ar_41)) [ Ar_30 >= 0 /\ Fresh_314 >= 1 /\ Fresh_312 >= 2 /\ Ar_31 = Ar_29 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_323, Ar_25, Fresh_324, Ar_30, Fresh_325, Ar_36, Ar_41)) [ Ar_30 >= 0 /\ 0 >= Fresh_323 + 1 /\ Fresh_321 >= 2 /\ Ar_31 = Ar_29 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_331, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ Ar_29 >= A2 + 1 /\ Ar_30 >= 0 /\ Fresh_330 >= 2 /\ A2 >= Fresh_331 + 1 /\ Fresh_331 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_333, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ Ar_29 >= A2 + 1 /\ Ar_30 >= 0 /\ Fresh_332 >= 2 /\ A2 >= Fresh_333 + 1 /\ 0 >= Fresh_333 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_335, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ Ar_29 >= A2 + 1 /\ Ar_30 >= 0 /\ Fresh_334 >= 2 /\ Fresh_335 >= A2 + 1 /\ Fresh_335 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_337, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ Ar_29 >= A2 + 1 /\ Ar_30 >= 0 /\ Fresh_336 >= 2 /\ Fresh_337 >= A2 + 1 /\ 0 >= Fresh_337 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_339, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ A2 >= Ar_29 + 1 /\ Ar_30 >= 0 /\ Fresh_338 >= 2 /\ A2 >= Fresh_339 + 1 /\ Fresh_339 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_341, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ A2 >= Ar_29 + 1 /\ Ar_30 >= 0 /\ Fresh_340 >= 2 /\ A2 >= Fresh_341 + 1 /\ 0 >= Fresh_341 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_343, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ A2 >= Ar_29 + 1 /\ Ar_30 >= 0 /\ Fresh_342 >= 2 /\ Fresh_343 >= A2 + 1 /\ Fresh_343 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_345, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ A2 >= Ar_29 + 1 /\ Ar_30 >= 0 /\ Fresh_344 >= 2 /\ Fresh_345 >= A2 + 1 /\ 0 >= Fresh_345 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_348, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_346 >= 2 /\ Z1 >= 1 /\ Fresh_348 >= 1 /\ Fresh_358 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_361, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_359 >= 2 /\ Z1 >= 1 /\ Fresh_361 >= 1 /\ 0 >= Fresh_371 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_374, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_372 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_374 + 1 /\ Fresh_384 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_387, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_385 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_387 + 1 /\ 0 >= Fresh_397 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_400, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_398 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_400 >= 1 /\ Fresh_410 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_413, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_411 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_413 >= 1 /\ 0 >= Fresh_423 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_426, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_424 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_426 + 1 /\ Fresh_436 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_439, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_437 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_439 + 1 /\ 0 >= Fresh_449 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f15(Ar_0, Ar_1 + 1, Ar_3, Fresh_450, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_0 >= Ar_1 + 1 /\ Ar_1 >= 0 ] start location: koat_start leaf cost: 0 Testing for reachability in the complexity graph removes the following transitions from problem 2: f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_13, Ar_11, Ar_36, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_0 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_11 >= 1 /\ Ar_25 = 0 ] f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_64, Ar_11, Ar_36, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_51 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ Ar_11 >= 1 /\ 0 >= Ar_11 + 1 /\ Ar_25 = 0 ] f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_314, Ar_25, Fresh_315, Ar_30, Fresh_316, Ar_36, Ar_41)) [ Ar_30 >= 0 /\ Fresh_314 >= 1 /\ Fresh_312 >= 2 /\ Ar_31 = Ar_29 ] f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_323, Ar_25, Fresh_324, Ar_30, Fresh_325, Ar_36, Ar_41)) [ Ar_30 >= 0 /\ 0 >= Fresh_323 + 1 /\ Fresh_321 >= 2 /\ Ar_31 = Ar_29 ] f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_331, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ Ar_29 >= A2 + 1 /\ Ar_30 >= 0 /\ Fresh_330 >= 2 /\ A2 >= Fresh_331 + 1 /\ Fresh_331 >= 1 /\ Ar_31 = 0 ] f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_333, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ Ar_29 >= A2 + 1 /\ Ar_30 >= 0 /\ Fresh_332 >= 2 /\ A2 >= Fresh_333 + 1 /\ 0 >= Fresh_333 + 1 /\ Ar_31 = 0 ] f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_335, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ Ar_29 >= A2 + 1 /\ Ar_30 >= 0 /\ Fresh_334 >= 2 /\ Fresh_335 >= A2 + 1 /\ Fresh_335 >= 1 /\ Ar_31 = 0 ] f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_337, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ Ar_29 >= A2 + 1 /\ Ar_30 >= 0 /\ Fresh_336 >= 2 /\ Fresh_337 >= A2 + 1 /\ 0 >= Fresh_337 + 1 /\ Ar_31 = 0 ] f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_339, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ A2 >= Ar_29 + 1 /\ Ar_30 >= 0 /\ Fresh_338 >= 2 /\ A2 >= Fresh_339 + 1 /\ Fresh_339 >= 1 /\ Ar_31 = 0 ] f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_341, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ A2 >= Ar_29 + 1 /\ Ar_30 >= 0 /\ Fresh_340 >= 2 /\ A2 >= Fresh_341 + 1 /\ 0 >= Fresh_341 + 1 /\ Ar_31 = 0 ] f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_343, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ A2 >= Ar_29 + 1 /\ Ar_30 >= 0 /\ Fresh_342 >= 2 /\ Fresh_343 >= A2 + 1 /\ Fresh_343 >= 1 /\ Ar_31 = 0 ] f9(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_345, Ar_25, Ar_29, Ar_30, 0, Ar_36, Ar_41)) [ A2 >= Ar_29 + 1 /\ Ar_30 >= 0 /\ Fresh_344 >= 2 /\ Fresh_345 >= A2 + 1 /\ 0 >= Fresh_345 + 1 /\ Ar_31 = 0 ] We thus obtain the following problem: 3: T: (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Fresh_282, Ar_30, Fresh_283, Ar_36, Ar_41)) [ Fresh_280 >= 2 /\ Ar_36 >= 0 /\ Ar_31 = Ar_29 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_289, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_288 >= 2 /\ C2 >= Fresh_289 + 1 /\ Fresh_289 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_310, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_309 >= 2 /\ Fresh_310 >= C2 + 1 /\ 0 >= Fresh_310 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_307, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_306 >= 2 /\ Fresh_307 >= C2 + 1 /\ Fresh_307 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_304, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_303 >= 2 /\ C2 >= Fresh_304 + 1 /\ 0 >= Fresh_304 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_301, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_300 >= 2 /\ C2 >= Fresh_301 + 1 /\ Fresh_301 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_298, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_297 >= 2 /\ Fresh_298 >= C2 + 1 /\ 0 >= Fresh_298 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_295, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_294 >= 2 /\ Fresh_295 >= C2 + 1 /\ Fresh_295 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_292, Ar_25, Ar_29, Ar_30, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_291 >= 2 /\ C2 >= Fresh_292 + 1 /\ 0 >= Fresh_292 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_30, Ar_11, Ar_36, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_17 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_25 = 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_47, Ar_11, Ar_36, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_34 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ Ar_11 >= 1 /\ Ar_25 = 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_439, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_437 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_439 + 1 /\ 0 >= Fresh_449 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_426, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_424 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_426 + 1 /\ Fresh_436 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_413, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_411 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_413 >= 1 /\ 0 >= Fresh_423 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_400, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_398 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_400 >= 1 /\ Fresh_410 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_387, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_385 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_387 + 1 /\ 0 >= Fresh_397 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_374, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_372 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_374 + 1 /\ Fresh_384 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_361, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_359 >= 2 /\ Z1 >= 1 /\ Fresh_361 >= 1 /\ 0 >= Fresh_371 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_348, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_346 >= 2 /\ Z1 >= 1 /\ Fresh_348 >= 1 /\ Fresh_358 >= 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f15(Ar_0, Ar_1 + 1, Ar_3, Fresh_450, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Ar_0 >= Ar_1 + 1 /\ Ar_1 >= 0 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_253, Fresh_254, Fresh_255, Fresh_256, Ar_7, Ar_8, Fresh_260, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_272 >= L2 /\ Fresh_258 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_274 + 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_260 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_231, Fresh_232, Fresh_233, Fresh_234, Ar_7, Ar_8, Fresh_238, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_250 >= L2 /\ Fresh_236 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_252 + 1 /\ 0 >= Ar_2 + 1 /\ Fresh_238 >= 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_209, Fresh_210, Fresh_211, Fresh_212, Ar_7, Ar_8, Fresh_216, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_228 >= L2 /\ Fresh_214 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_230 + 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_216 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_187, Fresh_188, Fresh_189, Fresh_190, Ar_7, Ar_8, Fresh_194, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_206 >= L2 /\ Fresh_192 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_208 + 1 /\ Ar_2 >= 1 /\ Fresh_194 >= 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_165, Fresh_166, Fresh_167, Fresh_168, Ar_7, Ar_8, Fresh_172, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_184 >= L2 /\ Fresh_170 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_186 >= 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_172 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_143, Fresh_144, Fresh_145, Fresh_146, Ar_7, Ar_8, Fresh_150, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_162 >= L2 /\ Fresh_148 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_164 >= 1 /\ 0 >= Ar_2 + 1 /\ Fresh_150 >= 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_121, Fresh_122, Fresh_123, Fresh_124, Ar_7, Ar_8, Fresh_128, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_140 >= L2 /\ Fresh_126 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_142 >= 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_128 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_99, Fresh_100, Fresh_101, Fresh_102, Ar_7, Ar_8, Fresh_106, Ar_2, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_118 >= L2 /\ Fresh_104 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_120 >= 1 /\ Ar_2 >= 1 /\ Fresh_106 >= 1 ] (Comp: ?, Cost: 1) f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f15(Fresh_275, 2, Fresh_276, Fresh_277, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ Fresh_275 >= 2 ] (Comp: ?, Cost: 1) f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Fresh_68, Fresh_69, Fresh_70, Fresh_71, Ar_7, Ar_8, 0, Fresh_86, Fresh_87, Ar_30, Fresh_88, Ar_36, Ar_41)) [ 0 >= U2 /\ 0 >= Fresh_73 /\ 0 >= V2 ] (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41) -> Com_1(f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_30, Ar_31, Ar_36, Ar_41)) [ 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_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Fresh_68, Fresh_69, Fresh_70, Fresh_71, Ar_7, Ar_8, 0, Fresh_86, Fresh_87, Fresh_88, Ar_36, Ar_41)) [ 0 >= U2 /\ 0 >= Fresh_73 /\ 0 >= V2 ] (Comp: 1, Cost: 1) f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f15(Fresh_275, 2, Fresh_276, Fresh_277, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Fresh_275 >= 2 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_99, Fresh_100, Fresh_101, Fresh_102, Ar_7, Ar_8, Fresh_106, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_118 >= L2 /\ Fresh_104 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_120 >= 1 /\ Ar_2 >= 1 /\ Fresh_106 >= 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_121, Fresh_122, Fresh_123, Fresh_124, Ar_7, Ar_8, Fresh_128, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_140 >= L2 /\ Fresh_126 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_142 >= 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_128 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_143, Fresh_144, Fresh_145, Fresh_146, Ar_7, Ar_8, Fresh_150, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_162 >= L2 /\ Fresh_148 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_164 >= 1 /\ 0 >= Ar_2 + 1 /\ Fresh_150 >= 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_165, Fresh_166, Fresh_167, Fresh_168, Ar_7, Ar_8, Fresh_172, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_184 >= L2 /\ Fresh_170 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_186 >= 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_172 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_187, Fresh_188, Fresh_189, Fresh_190, Ar_7, Ar_8, Fresh_194, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_206 >= L2 /\ Fresh_192 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_208 + 1 /\ Ar_2 >= 1 /\ Fresh_194 >= 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_209, Fresh_210, Fresh_211, Fresh_212, Ar_7, Ar_8, Fresh_216, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_228 >= L2 /\ Fresh_214 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_230 + 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_216 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_231, Fresh_232, Fresh_233, Fresh_234, Ar_7, Ar_8, Fresh_238, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_250 >= L2 /\ Fresh_236 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_252 + 1 /\ 0 >= Ar_2 + 1 /\ Fresh_238 >= 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_253, Fresh_254, Fresh_255, Fresh_256, Ar_7, Ar_8, Fresh_260, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_272 >= L2 /\ Fresh_258 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_274 + 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_260 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f15(Ar_0, Ar_1 + 1, Ar_3, Fresh_450, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_0 >= Ar_1 + 1 /\ Ar_1 >= 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_348, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_346 >= 2 /\ Z1 >= 1 /\ Fresh_348 >= 1 /\ Fresh_358 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_361, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_359 >= 2 /\ Z1 >= 1 /\ Fresh_361 >= 1 /\ 0 >= Fresh_371 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_374, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_372 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_374 + 1 /\ Fresh_384 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_387, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_385 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_387 + 1 /\ 0 >= Fresh_397 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_400, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_398 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_400 >= 1 /\ Fresh_410 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_413, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_411 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_413 >= 1 /\ 0 >= Fresh_423 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_426, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_424 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_426 + 1 /\ Fresh_436 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_439, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_437 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_439 + 1 /\ 0 >= Fresh_449 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_47, Ar_11, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_34 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ Ar_11 >= 1 /\ Ar_25 = 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_30, Ar_11, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_17 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_25 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_292, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_291 >= 2 /\ C2 >= Fresh_292 + 1 /\ 0 >= Fresh_292 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_295, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_294 >= 2 /\ Fresh_295 >= C2 + 1 /\ Fresh_295 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_298, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_297 >= 2 /\ Fresh_298 >= C2 + 1 /\ 0 >= Fresh_298 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_301, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_300 >= 2 /\ C2 >= Fresh_301 + 1 /\ Fresh_301 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_304, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_303 >= 2 /\ C2 >= Fresh_304 + 1 /\ 0 >= Fresh_304 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_307, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_306 >= 2 /\ Fresh_307 >= C2 + 1 /\ Fresh_307 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_310, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_309 >= 2 /\ Fresh_310 >= C2 + 1 /\ 0 >= Fresh_310 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_289, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_288 >= 2 /\ C2 >= Fresh_289 + 1 /\ Fresh_289 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Fresh_282, Fresh_283, Ar_36, Ar_41)) [ Fresh_280 >= 2 /\ Ar_36 >= 0 /\ Ar_31 = Ar_29 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = 3 Pol(f17) = 3 Pol(f0) = 0 Pol(f15) = 3 Pol(f13) = 2 Pol(f10) = 1 orients all transitions weakly and the transitions f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_99, Fresh_100, Fresh_101, Fresh_102, Ar_7, Ar_8, Fresh_106, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_118 >= L2 /\ Fresh_104 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_120 >= 1 /\ Ar_2 >= 1 /\ Fresh_106 >= 1 ] f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_253, Fresh_254, Fresh_255, Fresh_256, Ar_7, Ar_8, Fresh_260, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_272 >= L2 /\ Fresh_258 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_274 + 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_260 + 1 ] f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_231, Fresh_232, Fresh_233, Fresh_234, Ar_7, Ar_8, Fresh_238, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_250 >= L2 /\ Fresh_236 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_252 + 1 /\ 0 >= Ar_2 + 1 /\ Fresh_238 >= 1 ] f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_209, Fresh_210, Fresh_211, Fresh_212, Ar_7, Ar_8, Fresh_216, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_228 >= L2 /\ Fresh_214 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_230 + 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_216 + 1 ] f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_187, Fresh_188, Fresh_189, Fresh_190, Ar_7, Ar_8, Fresh_194, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_206 >= L2 /\ Fresh_192 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_208 + 1 /\ Ar_2 >= 1 /\ Fresh_194 >= 1 ] f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_165, Fresh_166, Fresh_167, Fresh_168, Ar_7, Ar_8, Fresh_172, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_184 >= L2 /\ Fresh_170 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_186 >= 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_172 + 1 ] f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_143, Fresh_144, Fresh_145, Fresh_146, Ar_7, Ar_8, Fresh_150, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_162 >= L2 /\ Fresh_148 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_164 >= 1 /\ 0 >= Ar_2 + 1 /\ Fresh_150 >= 1 ] f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_121, Fresh_122, Fresh_123, Fresh_124, Ar_7, Ar_8, Fresh_128, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_140 >= L2 /\ Fresh_126 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_142 >= 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_128 + 1 ] f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_47, Ar_11, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_34 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ Ar_11 >= 1 /\ Ar_25 = 0 ] f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_30, Ar_11, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_17 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_25 = 0 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Fresh_282, Fresh_283, Ar_36, Ar_41)) [ Fresh_280 >= 2 /\ Ar_36 >= 0 /\ Ar_31 = Ar_29 ] 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_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Fresh_68, Fresh_69, Fresh_70, Fresh_71, Ar_7, Ar_8, 0, Fresh_86, Fresh_87, Fresh_88, Ar_36, Ar_41)) [ 0 >= U2 /\ 0 >= Fresh_73 /\ 0 >= V2 ] (Comp: 1, Cost: 1) f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f15(Fresh_275, 2, Fresh_276, Fresh_277, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Fresh_275 >= 2 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_99, Fresh_100, Fresh_101, Fresh_102, Ar_7, Ar_8, Fresh_106, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_118 >= L2 /\ Fresh_104 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_120 >= 1 /\ Ar_2 >= 1 /\ Fresh_106 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_121, Fresh_122, Fresh_123, Fresh_124, Ar_7, Ar_8, Fresh_128, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_140 >= L2 /\ Fresh_126 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_142 >= 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_128 + 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_143, Fresh_144, Fresh_145, Fresh_146, Ar_7, Ar_8, Fresh_150, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_162 >= L2 /\ Fresh_148 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_164 >= 1 /\ 0 >= Ar_2 + 1 /\ Fresh_150 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_165, Fresh_166, Fresh_167, Fresh_168, Ar_7, Ar_8, Fresh_172, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_184 >= L2 /\ Fresh_170 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_186 >= 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_172 + 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_187, Fresh_188, Fresh_189, Fresh_190, Ar_7, Ar_8, Fresh_194, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_206 >= L2 /\ Fresh_192 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_208 + 1 /\ Ar_2 >= 1 /\ Fresh_194 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_209, Fresh_210, Fresh_211, Fresh_212, Ar_7, Ar_8, Fresh_216, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_228 >= L2 /\ Fresh_214 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_230 + 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_216 + 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_231, Fresh_232, Fresh_233, Fresh_234, Ar_7, Ar_8, Fresh_238, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_250 >= L2 /\ Fresh_236 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_252 + 1 /\ 0 >= Ar_2 + 1 /\ Fresh_238 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_253, Fresh_254, Fresh_255, Fresh_256, Ar_7, Ar_8, Fresh_260, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_272 >= L2 /\ Fresh_258 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_274 + 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_260 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f15(Ar_0, Ar_1 + 1, Ar_3, Fresh_450, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_0 >= Ar_1 + 1 /\ Ar_1 >= 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_348, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_346 >= 2 /\ Z1 >= 1 /\ Fresh_348 >= 1 /\ Fresh_358 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_361, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_359 >= 2 /\ Z1 >= 1 /\ Fresh_361 >= 1 /\ 0 >= Fresh_371 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_374, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_372 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_374 + 1 /\ Fresh_384 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_387, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_385 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_387 + 1 /\ 0 >= Fresh_397 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_400, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_398 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_400 >= 1 /\ Fresh_410 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_413, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_411 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_413 >= 1 /\ 0 >= Fresh_423 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_426, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_424 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_426 + 1 /\ Fresh_436 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_439, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_437 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_439 + 1 /\ 0 >= Fresh_449 + 1 ] (Comp: 3, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_47, Ar_11, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_34 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ Ar_11 >= 1 /\ Ar_25 = 0 ] (Comp: 3, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_30, Ar_11, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_17 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_25 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_292, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_291 >= 2 /\ C2 >= Fresh_292 + 1 /\ 0 >= Fresh_292 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_295, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_294 >= 2 /\ Fresh_295 >= C2 + 1 /\ Fresh_295 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_298, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_297 >= 2 /\ Fresh_298 >= C2 + 1 /\ 0 >= Fresh_298 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_301, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_300 >= 2 /\ C2 >= Fresh_301 + 1 /\ Fresh_301 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_304, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_303 >= 2 /\ C2 >= Fresh_304 + 1 /\ 0 >= Fresh_304 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_307, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_306 >= 2 /\ Fresh_307 >= C2 + 1 /\ Fresh_307 >= 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_310, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_309 >= 2 /\ Fresh_310 >= C2 + 1 /\ 0 >= Fresh_310 + 1 /\ Ar_31 = 0 ] (Comp: ?, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_289, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_288 >= 2 /\ C2 >= Fresh_289 + 1 /\ Fresh_289 >= 1 /\ Ar_31 = 0 ] (Comp: 3, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Fresh_282, Fresh_283, Ar_36, Ar_41)) [ Fresh_280 >= 2 /\ Ar_36 >= 0 /\ Ar_31 = Ar_29 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = V_11 + 1 Pol(f17) = V_11 + 1 Pol(f0) = V_11 Pol(f15) = V_11 + 1 Pol(f13) = V_11 + 1 Pol(f10) = V_11 + 1 orients all transitions weakly and the transitions f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_310, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_309 >= 2 /\ Fresh_310 >= C2 + 1 /\ 0 >= Fresh_310 + 1 /\ Ar_31 = 0 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_307, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_306 >= 2 /\ Fresh_307 >= C2 + 1 /\ Fresh_307 >= 1 /\ Ar_31 = 0 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_304, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_303 >= 2 /\ C2 >= Fresh_304 + 1 /\ 0 >= Fresh_304 + 1 /\ Ar_31 = 0 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_301, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_300 >= 2 /\ C2 >= Fresh_301 + 1 /\ Fresh_301 >= 1 /\ Ar_31 = 0 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_298, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_297 >= 2 /\ Fresh_298 >= C2 + 1 /\ 0 >= Fresh_298 + 1 /\ Ar_31 = 0 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_295, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_294 >= 2 /\ Fresh_295 >= C2 + 1 /\ Fresh_295 >= 1 /\ Ar_31 = 0 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_292, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_291 >= 2 /\ C2 >= Fresh_292 + 1 /\ 0 >= Fresh_292 + 1 /\ Ar_31 = 0 ] f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_289, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_288 >= 2 /\ C2 >= Fresh_289 + 1 /\ Fresh_289 >= 1 /\ Ar_31 = 0 ] 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_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Fresh_68, Fresh_69, Fresh_70, Fresh_71, Ar_7, Ar_8, 0, Fresh_86, Fresh_87, Fresh_88, Ar_36, Ar_41)) [ 0 >= U2 /\ 0 >= Fresh_73 /\ 0 >= V2 ] (Comp: 1, Cost: 1) f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f15(Fresh_275, 2, Fresh_276, Fresh_277, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Fresh_275 >= 2 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_99, Fresh_100, Fresh_101, Fresh_102, Ar_7, Ar_8, Fresh_106, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_118 >= L2 /\ Fresh_104 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_120 >= 1 /\ Ar_2 >= 1 /\ Fresh_106 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_121, Fresh_122, Fresh_123, Fresh_124, Ar_7, Ar_8, Fresh_128, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_140 >= L2 /\ Fresh_126 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_142 >= 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_128 + 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_143, Fresh_144, Fresh_145, Fresh_146, Ar_7, Ar_8, Fresh_150, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_162 >= L2 /\ Fresh_148 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_164 >= 1 /\ 0 >= Ar_2 + 1 /\ Fresh_150 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_165, Fresh_166, Fresh_167, Fresh_168, Ar_7, Ar_8, Fresh_172, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_184 >= L2 /\ Fresh_170 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_186 >= 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_172 + 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_187, Fresh_188, Fresh_189, Fresh_190, Ar_7, Ar_8, Fresh_194, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_206 >= L2 /\ Fresh_192 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_208 + 1 /\ Ar_2 >= 1 /\ Fresh_194 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_209, Fresh_210, Fresh_211, Fresh_212, Ar_7, Ar_8, Fresh_216, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_228 >= L2 /\ Fresh_214 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_230 + 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_216 + 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_231, Fresh_232, Fresh_233, Fresh_234, Ar_7, Ar_8, Fresh_238, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_250 >= L2 /\ Fresh_236 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_252 + 1 /\ 0 >= Ar_2 + 1 /\ Fresh_238 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_253, Fresh_254, Fresh_255, Fresh_256, Ar_7, Ar_8, Fresh_260, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_272 >= L2 /\ Fresh_258 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_274 + 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_260 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f15(Ar_0, Ar_1 + 1, Ar_3, Fresh_450, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_0 >= Ar_1 + 1 /\ Ar_1 >= 0 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_348, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_346 >= 2 /\ Z1 >= 1 /\ Fresh_348 >= 1 /\ Fresh_358 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_361, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_359 >= 2 /\ Z1 >= 1 /\ Fresh_361 >= 1 /\ 0 >= Fresh_371 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_374, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_372 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_374 + 1 /\ Fresh_384 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_387, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_385 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_387 + 1 /\ 0 >= Fresh_397 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_400, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_398 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_400 >= 1 /\ Fresh_410 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_413, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_411 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_413 >= 1 /\ 0 >= Fresh_423 + 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_426, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_424 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_426 + 1 /\ Fresh_436 >= 1 ] (Comp: ?, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_439, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_437 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_439 + 1 /\ 0 >= Fresh_449 + 1 ] (Comp: 3, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_47, Ar_11, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_34 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ Ar_11 >= 1 /\ Ar_25 = 0 ] (Comp: 3, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_30, Ar_11, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_17 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_25 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_292, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_291 >= 2 /\ C2 >= Fresh_292 + 1 /\ 0 >= Fresh_292 + 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_295, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_294 >= 2 /\ Fresh_295 >= C2 + 1 /\ Fresh_295 >= 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_298, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_297 >= 2 /\ Fresh_298 >= C2 + 1 /\ 0 >= Fresh_298 + 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_301, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_300 >= 2 /\ C2 >= Fresh_301 + 1 /\ Fresh_301 >= 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_304, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_303 >= 2 /\ C2 >= Fresh_304 + 1 /\ 0 >= Fresh_304 + 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_307, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_306 >= 2 /\ Fresh_307 >= C2 + 1 /\ Fresh_307 >= 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_310, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_309 >= 2 /\ Fresh_310 >= C2 + 1 /\ 0 >= Fresh_310 + 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_289, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_288 >= 2 /\ C2 >= Fresh_289 + 1 /\ Fresh_289 >= 1 /\ Ar_31 = 0 ] (Comp: 3, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Fresh_282, Fresh_283, Ar_36, Ar_41)) [ Fresh_280 >= 2 /\ Ar_36 >= 0 /\ Ar_31 = Ar_29 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = V_6 + 1 Pol(f17) = V_6 + 1 Pol(f0) = V_6 Pol(f15) = V_6 + 1 Pol(f13) = V_6 + 1 Pol(f10) = V_6 orients all transitions weakly and the transitions f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_439, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_437 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_439 + 1 /\ 0 >= Fresh_449 + 1 ] f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_426, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_424 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_426 + 1 /\ Fresh_436 >= 1 ] f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_413, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_411 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_413 >= 1 /\ 0 >= Fresh_423 + 1 ] f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_400, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_398 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_400 >= 1 /\ Fresh_410 >= 1 ] f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_387, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_385 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_387 + 1 /\ 0 >= Fresh_397 + 1 ] f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_374, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_372 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_374 + 1 /\ Fresh_384 >= 1 ] f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_361, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_359 >= 2 /\ Z1 >= 1 /\ Fresh_361 >= 1 /\ 0 >= Fresh_371 + 1 ] f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_348, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_346 >= 2 /\ Z1 >= 1 /\ Fresh_348 >= 1 /\ Fresh_358 >= 1 ] 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_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ 0 <= 0 ] (Comp: 1, Cost: 1) f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Fresh_68, Fresh_69, Fresh_70, Fresh_71, Ar_7, Ar_8, 0, Fresh_86, Fresh_87, Fresh_88, Ar_36, Ar_41)) [ 0 >= U2 /\ 0 >= Fresh_73 /\ 0 >= V2 ] (Comp: 1, Cost: 1) f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f15(Fresh_275, 2, Fresh_276, Fresh_277, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Fresh_275 >= 2 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_99, Fresh_100, Fresh_101, Fresh_102, Ar_7, Ar_8, Fresh_106, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_118 >= L2 /\ Fresh_104 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_120 >= 1 /\ Ar_2 >= 1 /\ Fresh_106 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_121, Fresh_122, Fresh_123, Fresh_124, Ar_7, Ar_8, Fresh_128, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_140 >= L2 /\ Fresh_126 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_142 >= 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_128 + 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_143, Fresh_144, Fresh_145, Fresh_146, Ar_7, Ar_8, Fresh_150, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_162 >= L2 /\ Fresh_148 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_164 >= 1 /\ 0 >= Ar_2 + 1 /\ Fresh_150 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_165, Fresh_166, Fresh_167, Fresh_168, Ar_7, Ar_8, Fresh_172, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_184 >= L2 /\ Fresh_170 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_186 >= 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_172 + 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_187, Fresh_188, Fresh_189, Fresh_190, Ar_7, Ar_8, Fresh_194, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_206 >= L2 /\ Fresh_192 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_208 + 1 /\ Ar_2 >= 1 /\ Fresh_194 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_209, Fresh_210, Fresh_211, Fresh_212, Ar_7, Ar_8, Fresh_216, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_228 >= L2 /\ Fresh_214 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_230 + 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_216 + 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_231, Fresh_232, Fresh_233, Fresh_234, Ar_7, Ar_8, Fresh_238, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_250 >= L2 /\ Fresh_236 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_252 + 1 /\ 0 >= Ar_2 + 1 /\ Fresh_238 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_253, Fresh_254, Fresh_255, Fresh_256, Ar_7, Ar_8, Fresh_260, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ L2 >= 2 /\ Fresh_272 >= L2 /\ Fresh_258 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_274 + 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_260 + 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f15(Ar_0, Ar_1 + 1, Ar_3, Fresh_450, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_0 >= Ar_1 + 1 /\ Ar_1 >= 0 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_348, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_346 >= 2 /\ Z1 >= 1 /\ Fresh_348 >= 1 /\ Fresh_358 >= 1 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_361, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_359 >= 2 /\ Z1 >= 1 /\ Fresh_361 >= 1 /\ 0 >= Fresh_371 + 1 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_374, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_372 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_374 + 1 /\ Fresh_384 >= 1 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_387, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_385 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_387 + 1 /\ 0 >= Fresh_397 + 1 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_400, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_398 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_400 >= 1 /\ Fresh_410 >= 1 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_413, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_411 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_413 >= 1 /\ 0 >= Fresh_423 + 1 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_426, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_424 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_426 + 1 /\ Fresh_436 >= 1 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_439, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_437 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_439 + 1 /\ 0 >= Fresh_449 + 1 ] (Comp: 3, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_47, Ar_11, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_34 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ Ar_11 >= 1 /\ Ar_25 = 0 ] (Comp: 3, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_30, Ar_11, 0, Ar_36, Ar_41)) [ Q2 >= 2 /\ Fresh_17 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_25 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_292, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_291 >= 2 /\ C2 >= Fresh_292 + 1 /\ 0 >= Fresh_292 + 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_295, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_294 >= 2 /\ Fresh_295 >= C2 + 1 /\ Fresh_295 >= 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_298, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_297 >= 2 /\ Fresh_298 >= C2 + 1 /\ 0 >= Fresh_298 + 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_301, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_300 >= 2 /\ C2 >= Fresh_301 + 1 /\ Fresh_301 >= 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_304, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_303 >= 2 /\ C2 >= Fresh_304 + 1 /\ 0 >= Fresh_304 + 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_307, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_306 >= 2 /\ Fresh_307 >= C2 + 1 /\ Fresh_307 >= 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_310, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_309 >= 2 /\ Fresh_310 >= C2 + 1 /\ 0 >= Fresh_310 + 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_289, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_288 >= 2 /\ C2 >= Fresh_289 + 1 /\ Fresh_289 >= 1 /\ Ar_31 = 0 ] (Comp: 3, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Fresh_282, Fresh_283, Ar_36, Ar_41)) [ Fresh_280 >= 2 /\ Ar_36 >= 0 /\ Ar_31 = Ar_29 ] start location: koat_start leaf cost: 0 Applied AI with 'oct' on problem 7 to obtain the following invariants: For symbol f10: X_6 >= 0 /\ X_12 + X_6 >= 0 /\ X_10 + X_6 >= 0 /\ -X_10 + X_6 >= 0 /\ -X_11 + X_5 - 1 >= 0 /\ X_12 >= 0 /\ X_10 + X_12 >= 0 /\ -X_10 + X_12 >= 0 /\ -X_10 >= 0 /\ X_10 >= 0 For symbol f13: X_12 >= 0 For symbol f15: X_1 - X_2 >= 0 /\ X_2 - 2 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 2 >= 0 This yielded the following problem: 8: T: (Comp: 3, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Fresh_282, Fresh_283, Ar_36, Ar_41)) [ Ar_8 >= 0 /\ Ar_41 + Ar_8 >= 0 /\ Ar_31 + Ar_8 >= 0 /\ -Ar_31 + Ar_8 >= 0 /\ -Ar_36 + Ar_7 - 1 >= 0 /\ Ar_41 >= 0 /\ Ar_31 + Ar_41 >= 0 /\ -Ar_31 + Ar_41 >= 0 /\ -Ar_31 >= 0 /\ Ar_31 >= 0 /\ Fresh_280 >= 2 /\ Ar_36 >= 0 /\ Ar_31 = Ar_29 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_289, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_8 >= 0 /\ Ar_41 + Ar_8 >= 0 /\ Ar_31 + Ar_8 >= 0 /\ -Ar_31 + Ar_8 >= 0 /\ -Ar_36 + Ar_7 - 1 >= 0 /\ Ar_41 >= 0 /\ Ar_31 + Ar_41 >= 0 /\ -Ar_31 + Ar_41 >= 0 /\ -Ar_31 >= 0 /\ Ar_31 >= 0 /\ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_288 >= 2 /\ C2 >= Fresh_289 + 1 /\ Fresh_289 >= 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_310, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_8 >= 0 /\ Ar_41 + Ar_8 >= 0 /\ Ar_31 + Ar_8 >= 0 /\ -Ar_31 + Ar_8 >= 0 /\ -Ar_36 + Ar_7 - 1 >= 0 /\ Ar_41 >= 0 /\ Ar_31 + Ar_41 >= 0 /\ -Ar_31 + Ar_41 >= 0 /\ -Ar_31 >= 0 /\ Ar_31 >= 0 /\ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_309 >= 2 /\ Fresh_310 >= C2 + 1 /\ 0 >= Fresh_310 + 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_307, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_8 >= 0 /\ Ar_41 + Ar_8 >= 0 /\ Ar_31 + Ar_8 >= 0 /\ -Ar_31 + Ar_8 >= 0 /\ -Ar_36 + Ar_7 - 1 >= 0 /\ Ar_41 >= 0 /\ Ar_31 + Ar_41 >= 0 /\ -Ar_31 + Ar_41 >= 0 /\ -Ar_31 >= 0 /\ Ar_31 >= 0 /\ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_306 >= 2 /\ Fresh_307 >= C2 + 1 /\ Fresh_307 >= 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_304, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_8 >= 0 /\ Ar_41 + Ar_8 >= 0 /\ Ar_31 + Ar_8 >= 0 /\ -Ar_31 + Ar_8 >= 0 /\ -Ar_36 + Ar_7 - 1 >= 0 /\ Ar_41 >= 0 /\ Ar_31 + Ar_41 >= 0 /\ -Ar_31 + Ar_41 >= 0 /\ -Ar_31 >= 0 /\ Ar_31 >= 0 /\ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_303 >= 2 /\ C2 >= Fresh_304 + 1 /\ 0 >= Fresh_304 + 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_301, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_8 >= 0 /\ Ar_41 + Ar_8 >= 0 /\ Ar_31 + Ar_8 >= 0 /\ -Ar_31 + Ar_8 >= 0 /\ -Ar_36 + Ar_7 - 1 >= 0 /\ Ar_41 >= 0 /\ Ar_31 + Ar_41 >= 0 /\ -Ar_31 + Ar_41 >= 0 /\ -Ar_31 >= 0 /\ Ar_31 >= 0 /\ C2 >= Ar_29 + 1 /\ Ar_36 >= 0 /\ Fresh_300 >= 2 /\ C2 >= Fresh_301 + 1 /\ Fresh_301 >= 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_298, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_8 >= 0 /\ Ar_41 + Ar_8 >= 0 /\ Ar_31 + Ar_8 >= 0 /\ -Ar_31 + Ar_8 >= 0 /\ -Ar_36 + Ar_7 - 1 >= 0 /\ Ar_41 >= 0 /\ Ar_31 + Ar_41 >= 0 /\ -Ar_31 + Ar_41 >= 0 /\ -Ar_31 >= 0 /\ Ar_31 >= 0 /\ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_297 >= 2 /\ Fresh_298 >= C2 + 1 /\ 0 >= Fresh_298 + 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_295, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_8 >= 0 /\ Ar_41 + Ar_8 >= 0 /\ Ar_31 + Ar_8 >= 0 /\ -Ar_31 + Ar_8 >= 0 /\ -Ar_36 + Ar_7 - 1 >= 0 /\ Ar_41 >= 0 /\ Ar_31 + Ar_41 >= 0 /\ -Ar_31 + Ar_41 >= 0 /\ -Ar_31 >= 0 /\ Ar_31 >= 0 /\ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_294 >= 2 /\ Fresh_295 >= C2 + 1 /\ Fresh_295 >= 1 /\ Ar_31 = 0 ] (Comp: Ar_36 + 1, Cost: 1) f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Fresh_292, Ar_25, Ar_29, 0, Ar_36 - 1, Ar_41)) [ Ar_8 >= 0 /\ Ar_41 + Ar_8 >= 0 /\ Ar_31 + Ar_8 >= 0 /\ -Ar_31 + Ar_8 >= 0 /\ -Ar_36 + Ar_7 - 1 >= 0 /\ Ar_41 >= 0 /\ Ar_31 + Ar_41 >= 0 /\ -Ar_31 + Ar_41 >= 0 /\ -Ar_31 >= 0 /\ Ar_31 >= 0 /\ Ar_29 >= C2 + 1 /\ Ar_36 >= 0 /\ Fresh_291 >= 2 /\ C2 >= Fresh_292 + 1 /\ 0 >= Fresh_292 + 1 /\ Ar_31 = 0 ] (Comp: 3, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_30, Ar_11, 0, Ar_36, Ar_41)) [ Ar_41 >= 0 /\ Q2 >= 2 /\ Fresh_17 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ 0 >= Ar_11 + 1 /\ Ar_25 = 0 ] (Comp: 3, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f10(Ar_0, Ar_1, Ar_2, Ar_3, Ar_36 + 1, Ar_8, Ar_11, Fresh_47, Ar_11, 0, Ar_36, Ar_41)) [ Ar_41 >= 0 /\ Q2 >= 2 /\ Fresh_34 >= 2 /\ Ar_8 >= 0 /\ Ar_7 >= 0 /\ Ar_11 >= 1 /\ Ar_25 = 0 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_439, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_41 >= 0 /\ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_437 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_439 + 1 /\ 0 >= Fresh_449 + 1 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_426, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_41 >= 0 /\ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_424 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= Fresh_426 + 1 /\ Fresh_436 >= 1 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_413, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_41 >= 0 /\ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_411 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_413 >= 1 /\ 0 >= Fresh_423 + 1 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_400, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_41 >= 0 /\ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_398 >= 2 /\ 0 >= Z1 + 1 /\ Fresh_400 >= 1 /\ Fresh_410 >= 1 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_387, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_41 >= 0 /\ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_385 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_387 + 1 /\ 0 >= Fresh_397 + 1 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_374, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_41 >= 0 /\ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_372 >= 2 /\ Z1 >= 1 /\ 0 >= Fresh_374 + 1 /\ Fresh_384 >= 1 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_361, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_41 >= 0 /\ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_359 >= 2 /\ Z1 >= 1 /\ Fresh_361 >= 1 /\ 0 >= Fresh_371 + 1 ] (Comp: Ar_8 + 1, Cost: 1) f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7 + 1, Ar_8 - 1, Fresh_348, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_41 >= 0 /\ Ar_7 >= 0 /\ Ar_8 >= 0 /\ Fresh_346 >= 2 /\ Z1 >= 1 /\ Fresh_348 >= 1 /\ Fresh_358 >= 1 ] (Comp: ?, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f15(Ar_0, Ar_1 + 1, Ar_3, Fresh_450, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_0 - Ar_1 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ Ar_0 - 2 >= 0 /\ Ar_0 >= Ar_1 + 1 /\ Ar_1 >= 0 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_253, Fresh_254, Fresh_255, Fresh_256, Ar_7, Ar_8, Fresh_260, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_0 - Ar_1 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ Ar_0 - 2 >= 0 /\ L2 >= 2 /\ Fresh_272 >= L2 /\ Fresh_258 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_274 + 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_260 + 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_231, Fresh_232, Fresh_233, Fresh_234, Ar_7, Ar_8, Fresh_238, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_0 - Ar_1 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ Ar_0 - 2 >= 0 /\ L2 >= 2 /\ Fresh_250 >= L2 /\ Fresh_236 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_252 + 1 /\ 0 >= Ar_2 + 1 /\ Fresh_238 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_209, Fresh_210, Fresh_211, Fresh_212, Ar_7, Ar_8, Fresh_216, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_0 - Ar_1 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ Ar_0 - 2 >= 0 /\ L2 >= 2 /\ Fresh_228 >= L2 /\ Fresh_214 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_230 + 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_216 + 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_187, Fresh_188, Fresh_189, Fresh_190, Ar_7, Ar_8, Fresh_194, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_0 - Ar_1 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ Ar_0 - 2 >= 0 /\ L2 >= 2 /\ Fresh_206 >= L2 /\ Fresh_192 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ 0 >= Fresh_208 + 1 /\ Ar_2 >= 1 /\ Fresh_194 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_165, Fresh_166, Fresh_167, Fresh_168, Ar_7, Ar_8, Fresh_172, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_0 - Ar_1 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ Ar_0 - 2 >= 0 /\ L2 >= 2 /\ Fresh_184 >= L2 /\ Fresh_170 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_186 >= 1 /\ 0 >= Ar_2 + 1 /\ 0 >= Fresh_172 + 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_143, Fresh_144, Fresh_145, Fresh_146, Ar_7, Ar_8, Fresh_150, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_0 - Ar_1 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ Ar_0 - 2 >= 0 /\ L2 >= 2 /\ Fresh_162 >= L2 /\ Fresh_148 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_164 >= 1 /\ 0 >= Ar_2 + 1 /\ Fresh_150 >= 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_121, Fresh_122, Fresh_123, Fresh_124, Ar_7, Ar_8, Fresh_128, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_0 - Ar_1 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ Ar_0 - 2 >= 0 /\ L2 >= 2 /\ Fresh_140 >= L2 /\ Fresh_126 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_142 >= 1 /\ Ar_2 >= 1 /\ 0 >= Fresh_128 + 1 ] (Comp: 3, Cost: 1) f15(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f13(Fresh_99, Fresh_100, Fresh_101, Fresh_102, Ar_7, Ar_8, Fresh_106, Ar_2, Ar_29, Ar_31, Ar_36, Ar_41)) [ Ar_0 - Ar_1 >= 0 /\ Ar_1 - 2 >= 0 /\ Ar_0 + Ar_1 - 4 >= 0 /\ Ar_0 - 2 >= 0 /\ L2 >= 2 /\ Fresh_118 >= L2 /\ Fresh_104 >= 2 /\ Ar_1 >= Ar_0 /\ Ar_1 >= 0 /\ Ar_41 >= 0 /\ Fresh_120 >= 1 /\ Ar_2 >= 1 /\ Fresh_106 >= 1 ] (Comp: 1, Cost: 1) f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f15(Fresh_275, 2, Fresh_276, Fresh_277, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ Fresh_275 >= 2 ] (Comp: 1, Cost: 1) f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f0(Fresh_68, Fresh_69, Fresh_70, Fresh_71, Ar_7, Ar_8, 0, Fresh_86, Fresh_87, Fresh_88, Ar_36, Ar_41)) [ 0 >= U2 /\ 0 >= Fresh_73 /\ 0 >= V2 ] (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41) -> Com_1(f17(Ar_0, Ar_1, Ar_2, Ar_3, Ar_7, Ar_8, Ar_11, Ar_25, Ar_29, Ar_31, Ar_36, Ar_41)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Complexity upper bound ? Time: 39.624 sec (SMT: 34.088 sec)