MAYBE * Step 1: TrivialSCCs 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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: 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,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,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,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,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,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,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 3: AddSinks 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,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,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,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,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,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,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: AddSinks + Details: () * Step 4: 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) 33. evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H,I) True (?,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) ;(exitus616,9)} Flow Graph: [0->{1},1->{2,3,4},2->{32,33},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,33},20->{2,3,4},21->{23,24,25,26},22->{32,33},23->{27,28,29},24->{30,31},25->{30,31} ,26->{30,31},27->{30,31},28->{30,31},29->{30,31},30->{32,33},31->{2,3,4},32->{},33->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,2),(1,3)] * Step 5: Failure 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) 33. evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H,I) True (?,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) ;(exitus616,9)} Flow Graph: [0->{1},1->{4},2->{32,33},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,33},20->{2,3,4},21->{23,24,25,26},22->{32,33},23->{27,28,29},24->{30,31},25->{30,31},26->{30 ,31},27->{30,31},28->{30,31},29->{30,31},30->{32,33},31->{2,3,4},32->{},33->{}] + Applied Processor: LooptreeTransformer + 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] | `- p:[4,20,13,10,6,3,31,24,21,11,7,5,8,9,25,26,27,23,28,29,14,15,16,12,17,18] c: [29] | `- p:[3,20,13,10,6,4,31,24,21,11,7,5,8,9,25,26,27,23,28,14,15,16,12,17,18] c: [28] | `- p:[3,20,13,10,6,4,31,24,21,11,7,5,8,9,25,26,27,23,14,15,16,12,17,18] c: [27] | `- p:[3,20,13,10,6,4,31,24,21,11,7,5,8,9,25,26,14,15,16,12,17,18] c: [18] | `- p:[3,20,13,10,6,4,31,24,21,11,7,5,8,9,25,26,14,15,16,12,17] c: [17] | `- p:[3,20,13,10,6,4,31,24,21,11,7,5,8,9,25,26,14,15,16,12] c: [16] | `- p:[3,20,13,10,6,4,31,24,21,11,7,5,8,9,25,26,14,15] c: [] MAYBE