MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I) True (1,1) 1. evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin(0,0,4,A,E,F,G,H,I) True (?,1) 2. evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && C = 1] (?,1) 3. evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in(A,B,C,D,J,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= C] (?,1) 4. evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in(A,B,C,D,J,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && C >= 2] (?,1) 5. evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] (?,1) 6. evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,C,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B = 0] (?,1) 7. evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,0,G,H,I) [4 + -1*C >= 0 (?,1) && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C = 0] 8. evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,J,G,H,I) [4 + -1*C >= 0 (?,1) && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C >= 1 && J >= 0 && C >= 2*J && 1 + 2*J >= C] 9. evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,J,G,H,I) [4 + -1*C >= 0 (?,1) && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && 0 >= 1 + C && 0 >= J && 2*J >= C && 1 + C >= 2*J] 10. evalbinsearchStepSize2bb3in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) [4 + -1*F >= 0 (?,1) && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= 1 + G] 11. evalbinsearchStepSize2bb3in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) [4 + -1*F >= 0 (?,1) && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= E] 12. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) [-1 + E + -1*G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 1 && B = 0] 13. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [-1 + E + -1*G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= A] 14. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [-1 + E + -1*G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A >= 2] 15. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [-1 + E + -1*G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] 16. evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,0) [-1 + E + -1*G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F = 0] 17. evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,J) [-1 + E + -1*G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] 18. evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,J) [-1 + E + -1*G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] 19. evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [4 + -1*I >= 0 (?,1) && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && D + I >= 256] 20. evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin(2,H,I,D + I,E,F,G,H,I) [4 + -1*I >= 0 (?,1) && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 255 >= D + I] 21. evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) [-1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= 1 + E] 22. evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [-1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= G] 23. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) [-1 + -1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 2 && B = 0] 24. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [-1 + -1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 1 >= A] 25. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [-1 + -1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A >= 3] 26. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [-1 + -1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] 27. evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,0) [-1 + -1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && F = 0] 28. evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,J) [-1 + -1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] 29. evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,J) [-1 + -1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && 0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] 30. evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [4 + -1*I >= 0 (?,1) && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && I >= 1 + D] 31. evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin(1,H,I,D + -1*I,E,F,G,H,I) [4 + -1*I >= 0 (?,1) && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && D >= I] 32. evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2stop(A,B,C,D,E,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0] (?,1) Signature: {(evalbinsearchStepSize2bb10in,9) ;(evalbinsearchStepSize2bb12in,9) ;(evalbinsearchStepSize2bb13in,9) ;(evalbinsearchStepSize2bb1in,9) ;(evalbinsearchStepSize2bb2in,9) ;(evalbinsearchStepSize2bb3in,9) ;(evalbinsearchStepSize2bb4in,9) ;(evalbinsearchStepSize2bb6in,9) ;(evalbinsearchStepSize2bb7in,9) ;(evalbinsearchStepSize2bb9in,9) ;(evalbinsearchStepSize2bbin,9) ;(evalbinsearchStepSize2entryin,9) ;(evalbinsearchStepSize2returnin,9) ;(evalbinsearchStepSize2start,9) ;(evalbinsearchStepSize2stop,9)} Flow Graph: [0->{1},1->{2,3,4},2->{32},3->{5,6},4->{5,6},5->{7,8,9},6->{10,11},7->{10,11},8->{10,11},9->{10,11} ,10->{12,13,14,15},11->{21,22},12->{16,17,18},13->{19,20},14->{19,20},15->{19,20},16->{19,20},17->{19,20} ,18->{19,20},19->{32},20->{2,3,4},21->{23,24,25,26},22->{32},23->{27,28,29},24->{30,31},25->{30,31},26->{30 ,31},27->{30,31},28->{30,31},29->{30,31},30->{32},31->{2,3,4},32->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,2),(1,3)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I) True (1,1) 1. evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin(0,0,4,A,E,F,G,H,I) True (?,1) 2. evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && C = 1] (?,1) 3. evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in(A,B,C,D,J,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= C] (?,1) 4. evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in(A,B,C,D,J,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && C >= 2] (?,1) 5. evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] (?,1) 6. evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,C,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B = 0] (?,1) 7. evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,0,G,H,I) [4 + -1*C >= 0 (?,1) && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C = 0] 8. evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,J,G,H,I) [4 + -1*C >= 0 (?,1) && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C >= 1 && J >= 0 && C >= 2*J && 1 + 2*J >= C] 9. evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,J,G,H,I) [4 + -1*C >= 0 (?,1) && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && 0 >= 1 + C && 0 >= J && 2*J >= C && 1 + C >= 2*J] 10. evalbinsearchStepSize2bb3in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) [4 + -1*F >= 0 (?,1) && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= 1 + G] 11. evalbinsearchStepSize2bb3in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) [4 + -1*F >= 0 (?,1) && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= E] 12. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) [-1 + E + -1*G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 1 && B = 0] 13. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [-1 + E + -1*G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= A] 14. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [-1 + E + -1*G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A >= 2] 15. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [-1 + E + -1*G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] 16. evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,0) [-1 + E + -1*G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F = 0] 17. evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,J) [-1 + E + -1*G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] 18. evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,J) [-1 + E + -1*G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] 19. evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [4 + -1*I >= 0 (?,1) && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && D + I >= 256] 20. evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin(2,H,I,D + I,E,F,G,H,I) [4 + -1*I >= 0 (?,1) && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 255 >= D + I] 21. evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) [-1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= 1 + E] 22. evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [-1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= G] 23. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) [-1 + -1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 2 && B = 0] 24. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [-1 + -1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 1 >= A] 25. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [-1 + -1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A >= 3] 26. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [-1 + -1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] 27. evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,0) [-1 + -1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && F = 0] 28. evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,J) [-1 + -1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] 29. evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,J) [-1 + -1*E + G >= 0 (?,1) && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && 0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] 30. evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [4 + -1*I >= 0 (?,1) && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && I >= 1 + D] 31. evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin(1,H,I,D + -1*I,E,F,G,H,I) [4 + -1*I >= 0 (?,1) && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && D >= I] 32. evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2stop(A,B,C,D,E,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0] (?,1) Signature: {(evalbinsearchStepSize2bb10in,9) ;(evalbinsearchStepSize2bb12in,9) ;(evalbinsearchStepSize2bb13in,9) ;(evalbinsearchStepSize2bb1in,9) ;(evalbinsearchStepSize2bb2in,9) ;(evalbinsearchStepSize2bb3in,9) ;(evalbinsearchStepSize2bb4in,9) ;(evalbinsearchStepSize2bb6in,9) ;(evalbinsearchStepSize2bb7in,9) ;(evalbinsearchStepSize2bb9in,9) ;(evalbinsearchStepSize2bbin,9) ;(evalbinsearchStepSize2entryin,9) ;(evalbinsearchStepSize2returnin,9) ;(evalbinsearchStepSize2start,9) ;(evalbinsearchStepSize2stop,9)} Flow Graph: [0->{1},1->{4},2->{32},3->{5,6},4->{5,6},5->{7,8,9},6->{10,11},7->{10,11},8->{10,11},9->{10,11},10->{12,13 ,14,15},11->{21,22},12->{16,17,18},13->{19,20},14->{19,20},15->{19,20},16->{19,20},17->{19,20},18->{19,20} ,19->{32},20->{2,3,4},21->{23,24,25,26},22->{32},23->{27,28,29},24->{30,31},25->{30,31},26->{30,31},27->{30 ,31},28->{30,31},29->{30,31},30->{32},31->{2,3,4},32->{}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: evalbinsearchStepSize2start(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2entryin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin(0,0,4,A,E,F,G,H,I) True evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && C = 1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in(A,B,C,D,J,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= C] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in(A,B,C,D,J,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && C >= 2] evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,C,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B = 0] evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,0,G,H,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C = 0] evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,J,G,H,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C >= 1 && J >= 0 && C >= 2*J && 1 + 2*J >= C] evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,J,G,H,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && 0 >= 1 + C && 0 >= J && 2*J >= C && 1 + C >= 2*J] evalbinsearchStepSize2bb3in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) [4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= 1 + G] evalbinsearchStepSize2bb3in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) [4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= E] evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 1 && B = 0] evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= A] evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A >= 2] evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,0) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F = 0] evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,J) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,J) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && D + I >= 256] evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin(2,H,I,D + I,E,F,G,H,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 255 >= D + I] evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) [-1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= 1 + E] evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [-1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= G] evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 2 && B = 0] evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 1 >= A] evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A >= 3] evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,0) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && F = 0] evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,J) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,J) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && 0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && I >= 1 + D] evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin(1,H,I,D + -1*I,E,F,G,H,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && D >= I] evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2stop(A,B,C,D,E,F,G,H,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0] Signature: {(evalbinsearchStepSize2bb10in,9) ;(evalbinsearchStepSize2bb12in,9) ;(evalbinsearchStepSize2bb13in,9) ;(evalbinsearchStepSize2bb1in,9) ;(evalbinsearchStepSize2bb2in,9) ;(evalbinsearchStepSize2bb3in,9) ;(evalbinsearchStepSize2bb4in,9) ;(evalbinsearchStepSize2bb6in,9) ;(evalbinsearchStepSize2bb7in,9) ;(evalbinsearchStepSize2bb9in,9) ;(evalbinsearchStepSize2bbin,9) ;(evalbinsearchStepSize2entryin,9) ;(evalbinsearchStepSize2returnin,9) ;(evalbinsearchStepSize2start,9) ;(evalbinsearchStepSize2stop,9)} Rule Graph: [0->{1},1->{4},2->{32},3->{5,6},4->{5,6},5->{7,8,9},6->{10,11},7->{10,11},8->{10,11},9->{10,11},10->{12,13 ,14,15},11->{21,22},12->{16,17,18},13->{19,20},14->{19,20},15->{19,20},16->{19,20},17->{19,20},18->{19,20} ,19->{32},20->{2,3,4},21->{23,24,25,26},22->{32},23->{27,28,29},24->{30,31},25->{30,31},26->{30,31},27->{30 ,31},28->{30,31},29->{30,31},30->{32},31->{2,3,4},32->{}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: evalbinsearchStepSize2start.0(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2entryin.1(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2entryin.1(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.4(0,0,4,A,E,F,G,H ,I) True evalbinsearchStepSize2bbin.2(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin.32(A,B,C,D,E,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && C = 1] evalbinsearchStepSize2bbin.3(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.5(A,B,C,D,J,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= C] evalbinsearchStepSize2bbin.3(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.6(A,B,C,D,J,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= C] evalbinsearchStepSize2bbin.4(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.5(A,B,C,D,J,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && C >= 2] evalbinsearchStepSize2bbin.4(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.6(A,B,C,D,J,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && C >= 2] evalbinsearchStepSize2bb1in.5(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.7(A,B,C,D,E,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb1in.5(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.8(A,B,C,D,E,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb1in.5(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.9(A,B,C,D,E,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb1in.6(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.10(A,B,C,D,E,C,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B = 0] evalbinsearchStepSize2bb1in.6(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,C,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B = 0] evalbinsearchStepSize2bb2in.7(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.10(A,B,C,D,E,0,G,H ,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C = 0] evalbinsearchStepSize2bb2in.7(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,0,G,H ,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C = 0] evalbinsearchStepSize2bb2in.8(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.10(A,B,C,D,E,J,G,H ,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C >= 1 && J >= 0 && C >= 2*J && 1 + 2*J >= C] evalbinsearchStepSize2bb2in.8(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,J,G,H ,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C >= 1 && J >= 0 && C >= 2*J && 1 + 2*J >= C] evalbinsearchStepSize2bb2in.9(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.10(A,B,C,D,E,J,G,H ,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && 0 >= 1 + C && 0 >= J && 2*J >= C && 1 + C >= 2*J] evalbinsearchStepSize2bb2in.9(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,J,G,H ,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && 0 >= 1 + C && 0 >= J && 2*J >= C && 1 + C >= 2*J] evalbinsearchStepSize2bb3in.10(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.12(A,B,C,D,E,F,G,H ,I) [4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= 1 + G] evalbinsearchStepSize2bb3in.10(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.13(A,B,C,D,E,F,G,H ,I) [4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= 1 + G] evalbinsearchStepSize2bb3in.10(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.14(A,B,C,D,E,F,G,H ,I) [4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= 1 + G] evalbinsearchStepSize2bb3in.10(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.15(A,B,C,D,E,F,G,H ,I) [4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= 1 + G] evalbinsearchStepSize2bb3in.11(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb9in.21(A,B,C,D,E,F,G,H ,I) [4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= E] evalbinsearchStepSize2bb3in.11(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb9in.22(A,B,C,D,E,F,G,H ,I) [4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= E] evalbinsearchStepSize2bb4in.12(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in.16(A,B,C,D,E,F,G,H ,I) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 1 && B = 0] evalbinsearchStepSize2bb4in.12(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in.17(A,B,C,D,E,F,G,H ,I) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 1 && B = 0] evalbinsearchStepSize2bb4in.12(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in.18(A,B,C,D,E,F,G,H ,I) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 1 && B = 0] evalbinsearchStepSize2bb4in.13(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.19(A,B,C,D,E,F,G,B ,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= A] evalbinsearchStepSize2bb4in.13(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,B ,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= A] evalbinsearchStepSize2bb4in.14(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.19(A,B,C,D,E,F,G,B ,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A >= 2] evalbinsearchStepSize2bb4in.14(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,B ,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A >= 2] evalbinsearchStepSize2bb4in.15(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.19(A,B,C,D,E,F,G,B ,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb4in.15(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,B ,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb6in.16(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.19(A,B,C,D,E,F,G,1 ,0) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F = 0] evalbinsearchStepSize2bb6in.16(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,1 ,0) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F = 0] evalbinsearchStepSize2bb6in.17(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.19(A,B,C,D,E,F,G,1 ,J) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb6in.17(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,1 ,J) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb6in.18(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.19(A,B,C,D,E,F,G,1 ,J) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb6in.18(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,1 ,J) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb7in.19(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin.32(A,B,C,D,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && D + I >= 256] evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.2(2,H,I,D + I,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 255 >= D + I] evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.3(2,H,I,D + I,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 255 >= D + I] evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.4(2,H,I,D + I,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 255 >= D + I] evalbinsearchStepSize2bb9in.21(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.23(A,B,C,D,E,F,G,H ,I) [-1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= 1 + E] evalbinsearchStepSize2bb9in.21(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.24(A,B,C,D,E,F,G,H ,I) [-1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= 1 + E] evalbinsearchStepSize2bb9in.21(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.25(A,B,C,D,E,F,G,H ,I) [-1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= 1 + E] evalbinsearchStepSize2bb9in.21(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.26(A,B,C,D,E,F,G,H ,I) [-1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= 1 + E] evalbinsearchStepSize2bb9in.22(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin.32(A,B,C,D,E,F,G,H ,I) [-1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= G] evalbinsearchStepSize2bb10in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in.27(A,B,C,D,E,F,G,H ,I) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 2 && B = 0] evalbinsearchStepSize2bb10in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in.28(A,B,C,D,E,F,G,H ,I) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 2 && B = 0] evalbinsearchStepSize2bb10in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in.29(A,B,C,D,E,F,G,H ,I) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 2 && B = 0] evalbinsearchStepSize2bb10in.24(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.30(A,B,C,D,E,F,G,B ,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 1 >= A] evalbinsearchStepSize2bb10in.24(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,B ,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 1 >= A] evalbinsearchStepSize2bb10in.25(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.30(A,B,C,D,E,F,G,B ,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A >= 3] evalbinsearchStepSize2bb10in.25(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,B ,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A >= 3] evalbinsearchStepSize2bb10in.26(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.30(A,B,C,D,E,F,G,B ,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb10in.26(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,B ,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb12in.27(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.30(A,B,C,D,E,F,G,1 ,0) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && F = 0] evalbinsearchStepSize2bb12in.27(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,1 ,0) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && F = 0] evalbinsearchStepSize2bb12in.28(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.30(A,B,C,D,E,F,G,1 ,J) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb12in.28(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,1 ,J) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb12in.29(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.30(A,B,C,D,E,F,G,1 ,J) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && 0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb12in.29(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,1 ,J) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && 0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb13in.30(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin.32(A,B,C,D,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && I >= 1 + D] evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.2(1,H,I,D + -1*I,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && D >= I] evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.3(1,H,I,D + -1*I,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && D >= I] evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.4(1,H,I,D + -1*I,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && D >= I] evalbinsearchStepSize2returnin.32(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0] Signature: {(evalbinsearchStepSize2bb10in.23,9) ;(evalbinsearchStepSize2bb10in.24,9) ;(evalbinsearchStepSize2bb10in.25,9) ;(evalbinsearchStepSize2bb10in.26,9) ;(evalbinsearchStepSize2bb12in.27,9) ;(evalbinsearchStepSize2bb12in.28,9) ;(evalbinsearchStepSize2bb12in.29,9) ;(evalbinsearchStepSize2bb13in.30,9) ;(evalbinsearchStepSize2bb13in.31,9) ;(evalbinsearchStepSize2bb1in.5,9) ;(evalbinsearchStepSize2bb1in.6,9) ;(evalbinsearchStepSize2bb2in.7,9) ;(evalbinsearchStepSize2bb2in.8,9) ;(evalbinsearchStepSize2bb2in.9,9) ;(evalbinsearchStepSize2bb3in.10,9) ;(evalbinsearchStepSize2bb3in.11,9) ;(evalbinsearchStepSize2bb4in.12,9) ;(evalbinsearchStepSize2bb4in.13,9) ;(evalbinsearchStepSize2bb4in.14,9) ;(evalbinsearchStepSize2bb4in.15,9) ;(evalbinsearchStepSize2bb6in.16,9) ;(evalbinsearchStepSize2bb6in.17,9) ;(evalbinsearchStepSize2bb6in.18,9) ;(evalbinsearchStepSize2bb7in.19,9) ;(evalbinsearchStepSize2bb7in.20,9) ;(evalbinsearchStepSize2bb9in.21,9) ;(evalbinsearchStepSize2bb9in.22,9) ;(evalbinsearchStepSize2bbin.2,9) ;(evalbinsearchStepSize2bbin.3,9) ;(evalbinsearchStepSize2bbin.4,9) ;(evalbinsearchStepSize2entryin.1,9) ;(evalbinsearchStepSize2returnin.32,9) ;(evalbinsearchStepSize2start.0,9) ;(evalbinsearchStepSize2stop.33,9)} Rule Graph: [0->{1},1->{5,6},2->{67},3->{7,8,9},4->{10,11},5->{7,8,9},6->{10,11},7->{12,13},8->{14,15},9->{16,17} ,10->{18,19,20,21},11->{22,23},12->{18,19,20,21},13->{22,23},14->{18,19,20,21},15->{22,23},16->{18,19,20,21} ,17->{22,23},18->{24,25,26},19->{27,28},20->{29,30},21->{31,32},22->{43,44,45,46},23->{47},24->{33,34} ,25->{35,36},26->{37,38},27->{39},28->{40,41,42},29->{39},30->{40,41,42},31->{39},32->{40,41,42},33->{39} ,34->{40,41,42},35->{39},36->{40,41,42},37->{39},38->{40,41,42},39->{67},40->{2},41->{3,4},42->{5,6},43->{48 ,49,50},44->{51,52},45->{53,54},46->{55,56},47->{67},48->{57,58},49->{59,60},50->{61,62},51->{63},52->{64,65 ,66},53->{63},54->{64,65,66},55->{63},56->{64,65,66},57->{63},58->{64,65,66},59->{63},60->{64,65,66} ,61->{63},62->{64,65,66},63->{67},64->{2},65->{3,4},66->{5,6},67->{}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: evalbinsearchStepSize2start.0(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2entryin.1(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2entryin.1(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.4(0,0,4,A,E,F,G,H ,I) True evalbinsearchStepSize2bbin.2(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin.32(A,B,C,D,E,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && C = 1] evalbinsearchStepSize2bbin.3(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.5(A,B,C,D,J,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= C] evalbinsearchStepSize2bbin.3(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.6(A,B,C,D,J,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= C] evalbinsearchStepSize2bbin.4(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.5(A,B,C,D,J,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && C >= 2] evalbinsearchStepSize2bbin.4(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.6(A,B,C,D,J,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && C >= 2] evalbinsearchStepSize2bb1in.5(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.7(A,B,C,D,E,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb1in.5(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.8(A,B,C,D,E,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb1in.5(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.9(A,B,C,D,E,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb1in.6(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.10(A,B,C,D,E,C,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B = 0] evalbinsearchStepSize2bb1in.6(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,C,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B = 0] evalbinsearchStepSize2bb2in.7(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.10(A,B,C,D,E,0,G,H ,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C = 0] evalbinsearchStepSize2bb2in.7(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,0,G,H ,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C = 0] evalbinsearchStepSize2bb2in.8(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.10(A,B,C,D,E,J,G,H ,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C >= 1 && J >= 0 && C >= 2*J && 1 + 2*J >= C] evalbinsearchStepSize2bb2in.8(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,J,G,H ,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C >= 1 && J >= 0 && C >= 2*J && 1 + 2*J >= C] evalbinsearchStepSize2bb2in.9(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.10(A,B,C,D,E,J,G,H ,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && 0 >= 1 + C && 0 >= J && 2*J >= C && 1 + C >= 2*J] evalbinsearchStepSize2bb2in.9(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,J,G,H ,I) [4 + -1*C >= 0 && 3 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && 0 >= 1 + C && 0 >= J && 2*J >= C && 1 + C >= 2*J] evalbinsearchStepSize2bb3in.10(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.12(A,B,C,D,E,F,G,H ,I) [4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= 1 + G] evalbinsearchStepSize2bb3in.10(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.13(A,B,C,D,E,F,G,H ,I) [4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= 1 + G] evalbinsearchStepSize2bb3in.10(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.14(A,B,C,D,E,F,G,H ,I) [4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= 1 + G] evalbinsearchStepSize2bb3in.10(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.15(A,B,C,D,E,F,G,H ,I) [4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= 1 + G] evalbinsearchStepSize2bb3in.11(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb9in.21(A,B,C,D,E,F,G,H ,I) [4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= E] evalbinsearchStepSize2bb3in.11(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb9in.22(A,B,C,D,E,F,G,H ,I) [4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= E] evalbinsearchStepSize2bb4in.12(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in.16(A,B,C,D,E,F,G,H ,I) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 1 && B = 0] evalbinsearchStepSize2bb4in.12(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in.17(A,B,C,D,E,F,G,H ,I) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 1 && B = 0] evalbinsearchStepSize2bb4in.12(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in.18(A,B,C,D,E,F,G,H ,I) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 1 && B = 0] evalbinsearchStepSize2bb4in.13(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.19(A,B,C,D,E,F,G,B ,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= A] evalbinsearchStepSize2bb4in.13(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,B ,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 0 >= A] evalbinsearchStepSize2bb4in.14(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.19(A,B,C,D,E,F,G,B ,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A >= 2] evalbinsearchStepSize2bb4in.14(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,B ,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A >= 2] evalbinsearchStepSize2bb4in.15(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.19(A,B,C,D,E,F,G,B ,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb4in.15(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,B ,F) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb6in.16(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.19(A,B,C,D,E,F,G,1 ,0) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F = 0] evalbinsearchStepSize2bb6in.16(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,1 ,0) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F = 0] evalbinsearchStepSize2bb6in.17(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.19(A,B,C,D,E,F,G,1 ,J) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb6in.17(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,1 ,J) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb6in.18(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.19(A,B,C,D,E,F,G,1 ,J) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb6in.18(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,1 ,J) [-1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 3 + A + -1*F >= 0 && 5 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 3 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && -1*B >= 0 && -1 + A + -1*B >= 0 && 1 + -1*A + -1*B >= 0 && B >= 0 && -1 + A + B >= 0 && 1 + -1*A + B >= 0 && 1 + -1*A >= 0 && -1 + A >= 0 && 0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb7in.19(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin.32(A,B,C,D,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && D + I >= 256] evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.2(2,H,I,D + I,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 255 >= D + I] evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.3(2,H,I,D + I,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 255 >= D + I] evalbinsearchStepSize2bb7in.20(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.4(2,H,I,D + I,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + E + -1*G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 255 >= D + I] evalbinsearchStepSize2bb9in.21(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.23(A,B,C,D,E,F,G,H ,I) [-1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= 1 + E] evalbinsearchStepSize2bb9in.21(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.24(A,B,C,D,E,F,G,H ,I) [-1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= 1 + E] evalbinsearchStepSize2bb9in.21(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.25(A,B,C,D,E,F,G,H ,I) [-1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= 1 + E] evalbinsearchStepSize2bb9in.21(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.26(A,B,C,D,E,F,G,H ,I) [-1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && G >= 1 + E] evalbinsearchStepSize2bb9in.22(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin.32(A,B,C,D,E,F,G,H ,I) [-1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && E >= G] evalbinsearchStepSize2bb10in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in.27(A,B,C,D,E,F,G,H ,I) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 2 && B = 0] evalbinsearchStepSize2bb10in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in.28(A,B,C,D,E,F,G,H ,I) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 2 && B = 0] evalbinsearchStepSize2bb10in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in.29(A,B,C,D,E,F,G,H ,I) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A = 2 && B = 0] evalbinsearchStepSize2bb10in.24(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.30(A,B,C,D,E,F,G,B ,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 1 >= A] evalbinsearchStepSize2bb10in.24(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,B ,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && 1 >= A] evalbinsearchStepSize2bb10in.25(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.30(A,B,C,D,E,F,G,B ,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A >= 3] evalbinsearchStepSize2bb10in.25(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,B ,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && A >= 3] evalbinsearchStepSize2bb10in.26(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.30(A,B,C,D,E,F,G,B ,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb10in.26(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,B ,F) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && B >= 1] evalbinsearchStepSize2bb12in.27(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.30(A,B,C,D,E,F,G,1 ,0) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && F = 0] evalbinsearchStepSize2bb12in.27(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,1 ,0) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && F = 0] evalbinsearchStepSize2bb12in.28(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.30(A,B,C,D,E,F,G,1 ,J) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb12in.28(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,1 ,J) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb12in.29(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.30(A,B,C,D,E,F,G,1 ,J) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && 0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb12in.29(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,1 ,J) [-1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + -1*B + -1*F >= 0 && 2 + A + -1*F >= 0 && 6 + -1*A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + -1*B + -1*C >= 0 && 2 + A + -1*C >= 0 && 6 + -1*A + -1*C >= 0 && -1*B >= 0 && -2 + A + -1*B >= 0 && 2 + -1*A + -1*B >= 0 && B >= 0 && -2 + A + B >= 0 && 2 + -1*A + B >= 0 && 2 + -1*A >= 0 && -2 + A >= 0 && 0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb13in.30(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin.32(A,B,C,D,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && I >= 1 + D] evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.2(1,H,I,D + -1*I,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && D >= I] evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.3(1,H,I,D + -1*I,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && D >= I] evalbinsearchStepSize2bb13in.31(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.4(1,H,I,D + -1*I,E,F,G,H ,I) [4 + -1*I >= 0 && 4 + H + -1*I >= 0 && 8 + -1*F + -1*I >= 0 && 8 + -1*C + -1*I >= 0 && 4 + B + -1*I >= 0 && 4 + A + -1*I >= 0 && 4 + -1*F + I >= 0 && 4 + -1*C + I >= 0 && 1 + B + -1*H >= 0 && H >= 0 && 4 + -1*F + H >= 0 && 4 + -1*C + H >= 0 && B + H >= 0 && -1*B + H >= 0 && A + H >= 0 && -1 + -1*E + G >= 0 && 4 + -1*F >= 0 && 8 + -1*C + -1*F >= 0 && 4 + B + -1*F >= 0 && 4 + A + -1*F >= 0 && 4 + -1*C + F >= 0 && 4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0 && D >= I] evalbinsearchStepSize2returnin.32(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H ,I) [4 + -1*C >= 0 && 4 + B + -1*C >= 0 && 4 + A + -1*C >= 0 && B >= 0 && A + B >= 0 && A >= 0] evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.33(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True Signature: {(evalbinsearchStepSize2bb10in.23,9) ;(evalbinsearchStepSize2bb10in.24,9) ;(evalbinsearchStepSize2bb10in.25,9) ;(evalbinsearchStepSize2bb10in.26,9) ;(evalbinsearchStepSize2bb12in.27,9) ;(evalbinsearchStepSize2bb12in.28,9) ;(evalbinsearchStepSize2bb12in.29,9) ;(evalbinsearchStepSize2bb13in.30,9) ;(evalbinsearchStepSize2bb13in.31,9) ;(evalbinsearchStepSize2bb1in.5,9) ;(evalbinsearchStepSize2bb1in.6,9) ;(evalbinsearchStepSize2bb2in.7,9) ;(evalbinsearchStepSize2bb2in.8,9) ;(evalbinsearchStepSize2bb2in.9,9) ;(evalbinsearchStepSize2bb3in.10,9) ;(evalbinsearchStepSize2bb3in.11,9) ;(evalbinsearchStepSize2bb4in.12,9) ;(evalbinsearchStepSize2bb4in.13,9) ;(evalbinsearchStepSize2bb4in.14,9) ;(evalbinsearchStepSize2bb4in.15,9) ;(evalbinsearchStepSize2bb6in.16,9) ;(evalbinsearchStepSize2bb6in.17,9) ;(evalbinsearchStepSize2bb6in.18,9) ;(evalbinsearchStepSize2bb7in.19,9) ;(evalbinsearchStepSize2bb7in.20,9) ;(evalbinsearchStepSize2bb9in.21,9) ;(evalbinsearchStepSize2bb9in.22,9) ;(evalbinsearchStepSize2bbin.2,9) ;(evalbinsearchStepSize2bbin.3,9) ;(evalbinsearchStepSize2bbin.4,9) ;(evalbinsearchStepSize2entryin.1,9) ;(evalbinsearchStepSize2returnin.32,9) ;(evalbinsearchStepSize2start.0,9) ;(evalbinsearchStepSize2stop.33,9) ;(exitus616,9)} Rule Graph: [0->{1},1->{5,6},2->{67},3->{7,8,9},4->{10,11},5->{7,8,9},6->{10,11},7->{12,13},8->{14,15},9->{16,17} ,10->{18,19,20,21},11->{22,23},12->{18,19,20,21},13->{22,23},14->{18,19,20,21},15->{22,23},16->{18,19,20,21} ,17->{22,23},18->{24,25,26},19->{27,28},20->{29,30},21->{31,32},22->{43,44,45,46},23->{47},24->{33,34} ,25->{35,36},26->{37,38},27->{39},28->{40,41,42},29->{39},30->{40,41,42},31->{39},32->{40,41,42},33->{39} ,34->{40,41,42},35->{39},36->{40,41,42},37->{39},38->{40,41,42},39->{67},40->{2},41->{3,4},42->{5,6},43->{48 ,49,50},44->{51,52},45->{53,54},46->{55,56},47->{67},48->{57,58},49->{59,60},50->{61,62},51->{63},52->{64,65 ,66},53->{63},54->{64,65,66},55->{63},56->{64,65,66},57->{63},58->{64,65,66},59->{63},60->{64,65,66} ,61->{63},62->{64,65,66},63->{67},64->{2},65->{3,4},66->{5,6},67->{68,69,70,71,72,73,74,75,76,77,78,79,80,81 ,82}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82] | `- p:[5,42,28,19,10,4,41,30,20,12,7,3,65,52,44,22,11,6,66,54,45,56,46,58,48,43,60,49,62,50,13,15,8,17,9,14,16,32,21,34,24,18,36,25,38,26] c: [24,25,26,34,36,38,43,48,49,50,58,60,62] | `- p:[3,41,28,19,10,4,65,52,44,22,11,6,42,30,20,12,7,5,66,54,45,56,46,14,8,16,9,32,21,13,15,17] c: [] MAYBE