(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalbinsearchStepSize2start)) (VAR A B C D E F G H I) (RULES evalbinsearchStepSize2start(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2entryin(A, B, C, D, E, F, G, H, I)) evalbinsearchStepSize2entryin(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bbin(0, 0, 4, A, E, F, G, H, I)) evalbinsearchStepSize2bbin(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2returnin(A, B, C, D, E, F, G, H, I)) [ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ C = 1 ] evalbinsearchStepSize2bbin(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb1in(A, B, C, D, J, F, G, H, I)) [ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ 0 >= C ] evalbinsearchStepSize2bbin(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb1in(A, B, C, D, J, F, G, H, I)) [ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ C >= 2 ] evalbinsearchStepSize2bb1in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb2in(A, B, C, D, E, F, G, H, I)) [ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ B >= 1 ] evalbinsearchStepSize2bb1in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb3in(A, B, C, D, E, C, G, H, I)) [ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ B = 0 ] evalbinsearchStepSize2bb2in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb3in(A, B, C, D, E, 0, G, H, I)) [ -C + 4 >= 0 /\ B - C + 3 >= 0 /\ A - C + 4 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ A >= 0 /\ C = 0 ] evalbinsearchStepSize2bb2in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb3in(A, B, C, D, E, J, G, H, I)) [ -C + 4 >= 0 /\ B - C + 3 >= 0 /\ A - C + 4 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ A >= 0 /\ C >= 1 /\ J >= 0 /\ C >= 2*J /\ 2*J + 1 >= C ] evalbinsearchStepSize2bb2in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb3in(A, B, C, D, E, J, G, H, I)) [ -C + 4 >= 0 /\ B - C + 3 >= 0 /\ A - C + 4 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ A >= 0 /\ 0 >= C + 1 /\ 0 >= J /\ 2*J >= C /\ C + 1 >= 2*J ] evalbinsearchStepSize2bb3in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb4in(A, B, C, D, E, F, G, H, I)) [ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ E >= G + 1 ] evalbinsearchStepSize2bb3in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb9in(A, B, C, D, E, F, G, H, I)) [ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ G >= E ] evalbinsearchStepSize2bb4in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb6in(A, B, C, D, E, F, G, H, I)) [ E - G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ A = 1 /\ B = 0 ] evalbinsearchStepSize2bb4in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb7in(A, B, C, D, E, F, G, B, F)) [ E - G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ 0 >= A ] evalbinsearchStepSize2bb4in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb7in(A, B, C, D, E, F, G, B, F)) [ E - G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ A >= 2 ] evalbinsearchStepSize2bb4in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb7in(A, B, C, D, E, F, G, B, F)) [ E - G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ B >= 1 ] evalbinsearchStepSize2bb6in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb7in(A, B, C, D, E, F, G, 1, 0)) [ E - G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ -B - F + 4 >= 0 /\ A - F + 3 >= 0 /\ -A - F + 5 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 5 >= 0 /\ -B >= 0 /\ A - B - 1 >= 0 /\ -A - B + 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ -A + B + 1 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ F = 0 ] evalbinsearchStepSize2bb6in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb7in(A, B, C, D, E, F, G, 1, J)) [ E - G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ -B - F + 4 >= 0 /\ A - F + 3 >= 0 /\ -A - F + 5 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 5 >= 0 /\ -B >= 0 /\ A - B - 1 >= 0 /\ -A - B + 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ -A + B + 1 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ F >= 1 /\ J >= 0 /\ F >= 2*J /\ 2*J + 1 >= F ] evalbinsearchStepSize2bb6in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb7in(A, B, C, D, E, F, G, 1, J)) [ E - G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ -B - F + 4 >= 0 /\ A - F + 3 >= 0 /\ -A - F + 5 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 5 >= 0 /\ -B >= 0 /\ A - B - 1 >= 0 /\ -A - B + 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ -A + B + 1 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ 0 >= F + 1 /\ 0 >= J /\ 2*J >= F /\ F + 1 >= 2*J ] evalbinsearchStepSize2bb7in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2returnin(A, B, C, D, E, F, G, H, I)) [ -I + 4 >= 0 /\ H - I + 4 >= 0 /\ -F - I + 8 >= 0 /\ -C - I + 8 >= 0 /\ B - I + 4 >= 0 /\ A - I + 4 >= 0 /\ -F + I + 4 >= 0 /\ -C + I + 4 >= 0 /\ B - H + 1 >= 0 /\ H >= 0 /\ -F + H + 4 >= 0 /\ -C + H + 4 >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ A + H >= 0 /\ E - G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ D + I >= 256 ] evalbinsearchStepSize2bb7in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bbin(2, H, I, D + I, E, F, G, H, I)) [ -I + 4 >= 0 /\ H - I + 4 >= 0 /\ -F - I + 8 >= 0 /\ -C - I + 8 >= 0 /\ B - I + 4 >= 0 /\ A - I + 4 >= 0 /\ -F + I + 4 >= 0 /\ -C + I + 4 >= 0 /\ B - H + 1 >= 0 /\ H >= 0 /\ -F + H + 4 >= 0 /\ -C + H + 4 >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ A + H >= 0 /\ E - G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ 255 >= D + I ] evalbinsearchStepSize2bb9in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb10in(A, B, C, D, E, F, G, H, I)) [ -E + G >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ G >= E + 1 ] evalbinsearchStepSize2bb9in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2returnin(A, B, C, D, E, F, G, H, I)) [ -E + G >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ E >= G ] evalbinsearchStepSize2bb10in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb12in(A, B, C, D, E, F, G, H, I)) [ -E + G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ A = 2 /\ B = 0 ] evalbinsearchStepSize2bb10in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb13in(A, B, C, D, E, F, G, B, F)) [ -E + G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ 1 >= A ] evalbinsearchStepSize2bb10in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb13in(A, B, C, D, E, F, G, B, F)) [ -E + G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ A >= 3 ] evalbinsearchStepSize2bb10in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb13in(A, B, C, D, E, F, G, B, F)) [ -E + G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ B >= 1 ] evalbinsearchStepSize2bb12in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb13in(A, B, C, D, E, F, G, 1, 0)) [ -E + G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ -B - F + 4 >= 0 /\ A - F + 2 >= 0 /\ -A - F + 6 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 6 >= 0 /\ -B >= 0 /\ A - B - 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ A + B - 2 >= 0 /\ -A + B + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ F = 0 ] evalbinsearchStepSize2bb12in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb13in(A, B, C, D, E, F, G, 1, J)) [ -E + G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ -B - F + 4 >= 0 /\ A - F + 2 >= 0 /\ -A - F + 6 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 6 >= 0 /\ -B >= 0 /\ A - B - 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ A + B - 2 >= 0 /\ -A + B + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ F >= 1 /\ J >= 0 /\ F >= 2*J /\ 2*J + 1 >= F ] evalbinsearchStepSize2bb12in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bb13in(A, B, C, D, E, F, G, 1, J)) [ -E + G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ -B - F + 4 >= 0 /\ A - F + 2 >= 0 /\ -A - F + 6 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 4 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 6 >= 0 /\ -B >= 0 /\ A - B - 2 >= 0 /\ -A - B + 2 >= 0 /\ B >= 0 /\ A + B - 2 >= 0 /\ -A + B + 2 >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 /\ 0 >= F + 1 /\ 0 >= J /\ 2*J >= F /\ F + 1 >= 2*J ] evalbinsearchStepSize2bb13in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2returnin(A, B, C, D, E, F, G, H, I)) [ -I + 4 >= 0 /\ H - I + 4 >= 0 /\ -F - I + 8 >= 0 /\ -C - I + 8 >= 0 /\ B - I + 4 >= 0 /\ A - I + 4 >= 0 /\ -F + I + 4 >= 0 /\ -C + I + 4 >= 0 /\ B - H + 1 >= 0 /\ H >= 0 /\ -F + H + 4 >= 0 /\ -C + H + 4 >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ A + H >= 0 /\ -E + G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ I >= D + 1 ] evalbinsearchStepSize2bb13in(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2bbin(1, H, I, D - I, E, F, G, H, I)) [ -I + 4 >= 0 /\ H - I + 4 >= 0 /\ -F - I + 8 >= 0 /\ -C - I + 8 >= 0 /\ B - I + 4 >= 0 /\ A - I + 4 >= 0 /\ -F + I + 4 >= 0 /\ -C + I + 4 >= 0 /\ B - H + 1 >= 0 /\ H >= 0 /\ -F + H + 4 >= 0 /\ -C + H + 4 >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ A + H >= 0 /\ -E + G - 1 >= 0 /\ -F + 4 >= 0 /\ -C - F + 8 >= 0 /\ B - F + 4 >= 0 /\ A - F + 4 >= 0 /\ -C + F + 4 >= 0 /\ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ D >= I ] evalbinsearchStepSize2returnin(A, B, C, D, E, F, G, H, I) -> Com_1(evalbinsearchStepSize2stop(A, B, C, D, E, F, G, H, I)) [ -C + 4 >= 0 /\ B - C + 4 >= 0 /\ A - C + 4 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 ] )