(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS eval_bin_search_StepSize2_start)) (VAR v__0 v_0 v_c_0 v_c_1 v_c_2 v_c_3 v_d_0 v_f_0 v_f_1 v_f_2 v_r v_s) (RULES eval_bin_search_StepSize2_start(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb0_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_bb0_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_0(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_0(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_1(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_1(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_2(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_2(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_3(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_3(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_4(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_4(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_5(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_5(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_6(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_6(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_7(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_7(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_8(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_8(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_9(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_9(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_10(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_10(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_11(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_11(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_12(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_12(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_13(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_13(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_14(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_14(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_15(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_15(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb1_in(v_s, v_0, 4, v_c_1, v_c_2, v_c_3, 0, 0, v_f_1, v_f_2, v_r, v_s)) eval_bin_search_StepSize2_bb1_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_16(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_0 + 4 >= 0 ] eval_bin_search_StepSize2_16(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_17(v__0, nondef_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_0 + 4 >= 0 ] eval_bin_search_StepSize2_17(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb12_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_c_0 = 1 ] eval_bin_search_StepSize2_17(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb2_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_c_0 < 1 ] eval_bin_search_StepSize2_17(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb2_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_c_0 > 1 ] eval_bin_search_StepSize2_bb2_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb3_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_f_0 > 0 ] eval_bin_search_StepSize2_bb2_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb4_in(v__0, v_0, v_c_0, v_c_0, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_f_0 = 0 ] eval_bin_search_StepSize2_bb3_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb4_in(v__0, v_0, v_c_0, nondef_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 - 1 >= 0 /\ v_d_0 + v_f_0 - 1 >= 0 /\ -v_c_0 + v_f_0 + 3 >= 0 /\ v_d_0 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_c_0 = 0 /\ nondef_1 = 0 ] eval_bin_search_StepSize2_bb3_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb4_in(v__0, v_0, v_c_0, nondef_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 - 1 >= 0 /\ v_d_0 + v_f_0 - 1 >= 0 /\ -v_c_0 + v_f_0 + 3 >= 0 /\ v_d_0 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_c_0 > 0 /\ nondef_1 >= 0 /\ v_c_0 - 2*nondef_1 >= 0 /\ v_c_0 - 2*nondef_1 < 2 ] eval_bin_search_StepSize2_bb3_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb4_in(v__0, v_0, v_c_0, nondef_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 - 1 >= 0 /\ v_d_0 + v_f_0 - 1 >= 0 /\ -v_c_0 + v_f_0 + 3 >= 0 /\ v_d_0 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_c_0 < 0 /\ nondef_1 <= 0 /\ -v_c_0 + 2*nondef_1 >= 0 /\ -v_c_0 + 2*nondef_1 < 2 ] eval_bin_search_StepSize2_bb4_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb5_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_0 > v_r ] eval_bin_search_StepSize2_bb4_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb8_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_0 <= v_r ] eval_bin_search_StepSize2_bb5_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb7_in(v__0, v_0, v_c_0, v_c_1, v_c_1, v_c_3, v_d_0, v_f_0, v_f_0, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ -v_r + v_0 - 1 >= 0 /\ v_d_0 < 1 ] eval_bin_search_StepSize2_bb5_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb7_in(v__0, v_0, v_c_0, v_c_1, v_c_1, v_c_3, v_d_0, v_f_0, v_f_0, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ -v_r + v_0 - 1 >= 0 /\ v_d_0 > 1 ] eval_bin_search_StepSize2_bb5_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb7_in(v__0, v_0, v_c_0, v_c_1, v_c_1, v_c_3, v_d_0, v_f_0, v_f_0, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ -v_r + v_0 - 1 >= 0 /\ v_f_0 > 0 ] eval_bin_search_StepSize2_bb5_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb6_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ -v_r + v_0 - 1 >= 0 /\ v_d_0 = 1 /\ v_f_0 = 0 ] eval_bin_search_StepSize2_bb6_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb7_in(v__0, v_0, v_c_0, v_c_1, nondef_2, v_c_3, v_d_0, v_f_0, 1, v_f_2, v_r, v_s)) [ -v_f_0 >= 0 /\ v_d_0 - v_f_0 - 1 >= 0 /\ -v_d_0 - v_f_0 + 1 >= 0 /\ -v_c_1 - v_f_0 + 4 >= 0 /\ -v_c_0 - v_f_0 + 4 >= 0 /\ v_f_0 >= 0 /\ v_d_0 + v_f_0 - 1 >= 0 /\ -v_d_0 + v_f_0 + 1 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ -v_d_0 + 1 >= 0 /\ -v_c_1 - v_d_0 + 5 >= 0 /\ -v_c_0 - v_d_0 + 5 >= 0 /\ v_d_0 - 1 >= 0 /\ -v_c_1 + v_d_0 + 3 >= 0 /\ -v_c_0 + v_d_0 + 3 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ -v_r + v_0 - 1 >= 0 /\ v_c_1 = 0 /\ nondef_2 = 0 ] eval_bin_search_StepSize2_bb6_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb7_in(v__0, v_0, v_c_0, v_c_1, nondef_2, v_c_3, v_d_0, v_f_0, 1, v_f_2, v_r, v_s)) [ -v_f_0 >= 0 /\ v_d_0 - v_f_0 - 1 >= 0 /\ -v_d_0 - v_f_0 + 1 >= 0 /\ -v_c_1 - v_f_0 + 4 >= 0 /\ -v_c_0 - v_f_0 + 4 >= 0 /\ v_f_0 >= 0 /\ v_d_0 + v_f_0 - 1 >= 0 /\ -v_d_0 + v_f_0 + 1 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ -v_d_0 + 1 >= 0 /\ -v_c_1 - v_d_0 + 5 >= 0 /\ -v_c_0 - v_d_0 + 5 >= 0 /\ v_d_0 - 1 >= 0 /\ -v_c_1 + v_d_0 + 3 >= 0 /\ -v_c_0 + v_d_0 + 3 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ -v_r + v_0 - 1 >= 0 /\ v_c_1 > 0 /\ nondef_2 >= 0 /\ v_c_1 - 2*nondef_2 >= 0 /\ v_c_1 - 2*nondef_2 < 2 ] eval_bin_search_StepSize2_bb6_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb7_in(v__0, v_0, v_c_0, v_c_1, nondef_2, v_c_3, v_d_0, v_f_0, 1, v_f_2, v_r, v_s)) [ -v_f_0 >= 0 /\ v_d_0 - v_f_0 - 1 >= 0 /\ -v_d_0 - v_f_0 + 1 >= 0 /\ -v_c_1 - v_f_0 + 4 >= 0 /\ -v_c_0 - v_f_0 + 4 >= 0 /\ v_f_0 >= 0 /\ v_d_0 + v_f_0 - 1 >= 0 /\ -v_d_0 + v_f_0 + 1 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ -v_d_0 + 1 >= 0 /\ -v_c_1 - v_d_0 + 5 >= 0 /\ -v_c_0 - v_d_0 + 5 >= 0 /\ v_d_0 - 1 >= 0 /\ -v_c_1 + v_d_0 + 3 >= 0 /\ -v_c_0 + v_d_0 + 3 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ -v_r + v_0 - 1 >= 0 /\ v_c_1 < 0 /\ nondef_2 <= 0 /\ -v_c_1 + 2*nondef_2 >= 0 /\ -v_c_1 + 2*nondef_2 < 2 ] eval_bin_search_StepSize2_bb7_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb12_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 - v_f_1 + 1 >= 0 /\ v_f_1 >= 0 /\ v_f_0 + v_f_1 >= 0 /\ -v_f_0 + v_f_1 >= 0 /\ v_d_0 + v_f_1 >= 0 /\ -v_c_2 + v_f_1 + 4 >= 0 /\ -v_c_1 + v_f_1 + 4 >= 0 /\ -v_c_0 + v_f_1 + 4 >= 0 /\ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_2 + v_f_0 + 4 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_2 + v_d_0 + 4 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_2 + 4 >= 0 /\ -v_c_1 - v_c_2 + 8 >= 0 /\ -v_c_0 - v_c_2 + 8 >= 0 /\ -v_c_1 + v_c_2 + 4 >= 0 /\ -v_c_0 + v_c_2 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ -v_r + v_0 - 1 >= 0 /\ v__0 + v_c_2 > 255 ] eval_bin_search_StepSize2_bb7_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb1_in(v__0 + v_c_2, v_0, v_c_2, v_c_1, v_c_2, v_c_3, 2, v_f_1, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 - v_f_1 + 1 >= 0 /\ v_f_1 >= 0 /\ v_f_0 + v_f_1 >= 0 /\ -v_f_0 + v_f_1 >= 0 /\ v_d_0 + v_f_1 >= 0 /\ -v_c_2 + v_f_1 + 4 >= 0 /\ -v_c_1 + v_f_1 + 4 >= 0 /\ -v_c_0 + v_f_1 + 4 >= 0 /\ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_2 + v_f_0 + 4 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_2 + v_d_0 + 4 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_2 + 4 >= 0 /\ -v_c_1 - v_c_2 + 8 >= 0 /\ -v_c_0 - v_c_2 + 8 >= 0 /\ -v_c_1 + v_c_2 + 4 >= 0 /\ -v_c_0 + v_c_2 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ -v_r + v_0 - 1 >= 0 /\ v__0 + v_c_2 <= 255 ] eval_bin_search_StepSize2_bb8_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb9_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_r - v_0 >= 0 /\ v_0 < v_r ] eval_bin_search_StepSize2_bb8_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb12_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_r - v_0 >= 0 /\ v_0 >= v_r ] eval_bin_search_StepSize2_bb9_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb11_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_1, v_d_0, v_f_0, v_f_1, v_f_0, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_r - v_0 - 1 >= 0 /\ v_d_0 < 2 ] eval_bin_search_StepSize2_bb9_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb11_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_1, v_d_0, v_f_0, v_f_1, v_f_0, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_r - v_0 - 1 >= 0 /\ v_d_0 > 2 ] eval_bin_search_StepSize2_bb9_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb11_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_1, v_d_0, v_f_0, v_f_1, v_f_0, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_r - v_0 - 1 >= 0 /\ v_f_0 > 0 ] eval_bin_search_StepSize2_bb9_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb10_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_r - v_0 - 1 >= 0 /\ v_d_0 = 2 /\ v_f_0 = 0 ] eval_bin_search_StepSize2_bb10_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb11_in(v__0, v_0, v_c_0, v_c_1, v_c_2, nondef_3, v_d_0, v_f_0, v_f_1, 1, v_r, v_s)) [ -v_f_0 >= 0 /\ v_d_0 - v_f_0 - 2 >= 0 /\ -v_d_0 - v_f_0 + 2 >= 0 /\ -v_c_1 - v_f_0 + 4 >= 0 /\ -v_c_0 - v_f_0 + 4 >= 0 /\ v_f_0 >= 0 /\ v_d_0 + v_f_0 - 2 >= 0 /\ -v_d_0 + v_f_0 + 2 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ -v_d_0 + 2 >= 0 /\ -v_c_1 - v_d_0 + 6 >= 0 /\ -v_c_0 - v_d_0 + 6 >= 0 /\ v_d_0 - 2 >= 0 /\ -v_c_1 + v_d_0 + 2 >= 0 /\ -v_c_0 + v_d_0 + 2 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_r - v_0 - 1 >= 0 /\ v_c_1 = 0 /\ nondef_3 = 0 ] eval_bin_search_StepSize2_bb10_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb11_in(v__0, v_0, v_c_0, v_c_1, v_c_2, nondef_3, v_d_0, v_f_0, v_f_1, 1, v_r, v_s)) [ -v_f_0 >= 0 /\ v_d_0 - v_f_0 - 2 >= 0 /\ -v_d_0 - v_f_0 + 2 >= 0 /\ -v_c_1 - v_f_0 + 4 >= 0 /\ -v_c_0 - v_f_0 + 4 >= 0 /\ v_f_0 >= 0 /\ v_d_0 + v_f_0 - 2 >= 0 /\ -v_d_0 + v_f_0 + 2 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ -v_d_0 + 2 >= 0 /\ -v_c_1 - v_d_0 + 6 >= 0 /\ -v_c_0 - v_d_0 + 6 >= 0 /\ v_d_0 - 2 >= 0 /\ -v_c_1 + v_d_0 + 2 >= 0 /\ -v_c_0 + v_d_0 + 2 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_r - v_0 - 1 >= 0 /\ v_c_1 > 0 /\ nondef_3 >= 0 /\ v_c_1 - 2*nondef_3 >= 0 /\ v_c_1 - 2*nondef_3 < 2 ] eval_bin_search_StepSize2_bb10_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb11_in(v__0, v_0, v_c_0, v_c_1, v_c_2, nondef_3, v_d_0, v_f_0, v_f_1, 1, v_r, v_s)) [ -v_f_0 >= 0 /\ v_d_0 - v_f_0 - 2 >= 0 /\ -v_d_0 - v_f_0 + 2 >= 0 /\ -v_c_1 - v_f_0 + 4 >= 0 /\ -v_c_0 - v_f_0 + 4 >= 0 /\ v_f_0 >= 0 /\ v_d_0 + v_f_0 - 2 >= 0 /\ -v_d_0 + v_f_0 + 2 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ -v_d_0 + 2 >= 0 /\ -v_c_1 - v_d_0 + 6 >= 0 /\ -v_c_0 - v_d_0 + 6 >= 0 /\ v_d_0 - 2 >= 0 /\ -v_c_1 + v_d_0 + 2 >= 0 /\ -v_c_0 + v_d_0 + 2 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_r - v_0 - 1 >= 0 /\ v_c_1 < 0 /\ nondef_3 <= 0 /\ -v_c_1 + 2*nondef_3 >= 0 /\ -v_c_1 + 2*nondef_3 < 2 ] eval_bin_search_StepSize2_bb11_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb12_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_2 - v_f_0 >= 0 /\ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_3 + v_f_0 + 4 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_f_2 + v_f_0 >= 0 /\ -v_f_2 + v_f_0 + 1 >= 0 /\ v_d_0 >= 0 /\ -v_c_3 + v_d_0 + 4 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ v_f_2 + v_d_0 >= 0 /\ -v_c_3 + 4 >= 0 /\ -v_c_1 - v_c_3 + 8 >= 0 /\ -v_c_0 - v_c_3 + 8 >= 0 /\ v_f_2 - v_c_3 + 4 >= 0 /\ -v_c_1 + v_c_3 + 4 >= 0 /\ -v_c_0 + v_c_3 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ v_f_2 - v_c_1 + 4 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_f_2 - v_c_0 + 4 >= 0 /\ v_r - v_0 - 1 >= 0 /\ v_f_2 >= 0 /\ v__0 - v_c_3 < 0 ] eval_bin_search_StepSize2_bb11_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_bb1_in(v__0 - v_c_3, v_0, v_c_3, v_c_1, v_c_2, v_c_3, 1, v_f_2, v_f_1, v_f_2, v_r, v_s)) [ v_f_2 - v_f_0 >= 0 /\ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_3 + v_f_0 + 4 >= 0 /\ -v_c_1 + v_f_0 + 4 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_f_2 + v_f_0 >= 0 /\ -v_f_2 + v_f_0 + 1 >= 0 /\ v_d_0 >= 0 /\ -v_c_3 + v_d_0 + 4 >= 0 /\ -v_c_1 + v_d_0 + 4 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ v_f_2 + v_d_0 >= 0 /\ -v_c_3 + 4 >= 0 /\ -v_c_1 - v_c_3 + 8 >= 0 /\ -v_c_0 - v_c_3 + 8 >= 0 /\ v_f_2 - v_c_3 + 4 >= 0 /\ -v_c_1 + v_c_3 + 4 >= 0 /\ -v_c_0 + v_c_3 + 4 >= 0 /\ -v_c_1 + 4 >= 0 /\ -v_c_0 - v_c_1 + 8 >= 0 /\ v_f_2 - v_c_1 + 4 >= 0 /\ -v_c_0 + v_c_1 + 4 >= 0 /\ -v_c_0 + 4 >= 0 /\ v_f_2 - v_c_0 + 4 >= 0 /\ v_r - v_0 - 1 >= 0 /\ v_f_2 >= 0 /\ v__0 - v_c_3 >= 0 ] eval_bin_search_StepSize2_bb12_in(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s) -> Com_1(eval_bin_search_StepSize2_stop(v__0, v_0, v_c_0, v_c_1, v_c_2, v_c_3, v_d_0, v_f_0, v_f_1, v_f_2, v_r, v_s)) [ v_f_0 >= 0 /\ v_d_0 + v_f_0 >= 0 /\ -v_c_0 + v_f_0 + 4 >= 0 /\ v_d_0 >= 0 /\ -v_c_0 + v_d_0 + 4 >= 0 /\ -v_c_0 + 4 >= 0 ] )