NO * Step 1: UnsatPaths NO + 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) [C = 1] (?,1) 3. evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in(A,B,C,D,J,F,G,H,I) [0 >= C] (?,1) 4. evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in(A,B,C,D,J,F,G,H,I) [C >= 2] (?,1) 5. evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) [0 >= 1 + B] (?,1) 6. evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) [B >= 1] (?,1) 7. evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,C,G,H,I) [B = 0] (?,1) 8. evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,0,G,H,I) [C = 0] (?,1) 9. evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,J,G,H,I) [C >= 1 && J >= 0 && C >= 2*J && 1 + 2*J >= C] (?,1) 10. evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,J,G,H,I) [0 >= 1 + C && 0 >= J && 2*J >= C && 1 + C >= 2*J] (?,1) 11. evalbinsearchStepSize2bb3in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) [E >= 1 + G] (?,1) 12. evalbinsearchStepSize2bb3in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) [G >= E] (?,1) 13. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) [A = 1 && B = 0] (?,1) 14. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [0 >= A] (?,1) 15. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [A >= 2] (?,1) 16. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [0 >= 1 + B] (?,1) 17. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [B >= 1] (?,1) 18. evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,0) [F = 0] (?,1) 19. evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,J) [F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] (?,1) 20. evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,J) [0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] (?,1) 21. evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [D + I >= 256] (?,1) 22. evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin(2,H,I,D + I,E,F,G,H,I) [255 >= D + I] (?,1) 23. evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) [G >= 1 + E] (?,1) 24. evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [E >= G] (?,1) 25. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) [A = 2 && B = 0] (?,1) 26. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [1 >= A] (?,1) 27. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [A >= 3] (?,1) 28. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [0 >= 1 + B] (?,1) 29. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [B >= 1] (?,1) 30. evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,0) [F = 0] (?,1) 31. evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,J) [F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] (?,1) 32. evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,J) [0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] (?,1) 33. evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [I >= 1 + D] (?,1) 34. evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin(1,H,I,D + -1*I,E,F,G,H,I) [D >= I] (?,1) 35. evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2stop(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)} Flow Graph: [0->{1},1->{2,3,4},2->{35},3->{5,6,7},4->{5,6,7},5->{8,9,10},6->{8,9,10},7->{11,12},8->{11,12},9->{11,12} ,10->{11,12},11->{13,14,15,16,17},12->{23,24},13->{18,19,20},14->{21,22},15->{21,22},16->{21,22},17->{21,22} ,18->{21,22},19->{21,22},20->{21,22},21->{35},22->{2,3,4},23->{25,26,27,28,29},24->{35},25->{30,31,32} ,26->{33,34},27->{33,34},28->{33,34},29->{33,34},30->{33,34},31->{33,34},32->{33,34},33->{35},34->{2,3,4} ,35->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,2),(1,3)] * Step 2: FromIts NO + 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) [C = 1] (?,1) 3. evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in(A,B,C,D,J,F,G,H,I) [0 >= C] (?,1) 4. evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in(A,B,C,D,J,F,G,H,I) [C >= 2] (?,1) 5. evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) [0 >= 1 + B] (?,1) 6. evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) [B >= 1] (?,1) 7. evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,C,G,H,I) [B = 0] (?,1) 8. evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,0,G,H,I) [C = 0] (?,1) 9. evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,J,G,H,I) [C >= 1 && J >= 0 && C >= 2*J && 1 + 2*J >= C] (?,1) 10. evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,J,G,H,I) [0 >= 1 + C && 0 >= J && 2*J >= C && 1 + C >= 2*J] (?,1) 11. evalbinsearchStepSize2bb3in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) [E >= 1 + G] (?,1) 12. evalbinsearchStepSize2bb3in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) [G >= E] (?,1) 13. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) [A = 1 && B = 0] (?,1) 14. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [0 >= A] (?,1) 15. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [A >= 2] (?,1) 16. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [0 >= 1 + B] (?,1) 17. evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [B >= 1] (?,1) 18. evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,0) [F = 0] (?,1) 19. evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,J) [F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] (?,1) 20. evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,J) [0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] (?,1) 21. evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [D + I >= 256] (?,1) 22. evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin(2,H,I,D + I,E,F,G,H,I) [255 >= D + I] (?,1) 23. evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) [G >= 1 + E] (?,1) 24. evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [E >= G] (?,1) 25. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) [A = 2 && B = 0] (?,1) 26. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [1 >= A] (?,1) 27. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [A >= 3] (?,1) 28. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [0 >= 1 + B] (?,1) 29. evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [B >= 1] (?,1) 30. evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,0) [F = 0] (?,1) 31. evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,J) [F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] (?,1) 32. evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,J) [0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] (?,1) 33. evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [I >= 1 + D] (?,1) 34. evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin(1,H,I,D + -1*I,E,F,G,H,I) [D >= I] (?,1) 35. evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2stop(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)} Flow Graph: [0->{1},1->{4},2->{35},3->{5,6,7},4->{5,6,7},5->{8,9,10},6->{8,9,10},7->{11,12},8->{11,12},9->{11,12} ,10->{11,12},11->{13,14,15,16,17},12->{23,24},13->{18,19,20},14->{21,22},15->{21,22},16->{21,22},17->{21,22} ,18->{21,22},19->{21,22},20->{21,22},21->{35},22->{2,3,4},23->{25,26,27,28,29},24->{35},25->{30,31,32} ,26->{33,34},27->{33,34},28->{33,34},29->{33,34},30->{33,34},31->{33,34},32->{33,34},33->{35},34->{2,3,4} ,35->{}] + Applied Processor: FromIts + Details: () * Step 3: CloseWith NO + 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) [C = 1] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in(A,B,C,D,J,F,G,H,I) [0 >= C] evalbinsearchStepSize2bbin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in(A,B,C,D,J,F,G,H,I) [C >= 2] evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) [0 >= 1 + B] evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) [B >= 1] evalbinsearchStepSize2bb1in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,C,G,H,I) [B = 0] evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,0,G,H,I) [C = 0] evalbinsearchStepSize2bb2in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in(A,B,C,D,E,J,G,H,I) [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) [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) [E >= 1 + G] evalbinsearchStepSize2bb3in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) [G >= E] evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) [A = 1 && B = 0] evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [0 >= A] evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [A >= 2] evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [0 >= 1 + B] evalbinsearchStepSize2bb4in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,B,F) [B >= 1] evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,0) [F = 0] evalbinsearchStepSize2bb6in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,1,J) [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) [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) [D + I >= 256] evalbinsearchStepSize2bb7in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin(2,H,I,D + I,E,F,G,H,I) [255 >= D + I] evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) [G >= 1 + E] evalbinsearchStepSize2bb9in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) [E >= G] evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) [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 >= A] evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [A >= 3] evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [0 >= 1 + B] evalbinsearchStepSize2bb10in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,B,F) [B >= 1] evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,0) [F = 0] evalbinsearchStepSize2bb12in(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in(A,B,C,D,E,F,G,1,J) [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) [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) [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) [D >= I] evalbinsearchStepSize2returnin(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2stop(A,B,C,D,E,F,G,H,I) True 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->{35},3->{5,6,7},4->{5,6,7},5->{8,9,10},6->{8,9,10},7->{11,12},8->{11,12},9->{11,12} ,10->{11,12},11->{13,14,15,16,17},12->{23,24},13->{18,19,20},14->{21,22},15->{21,22},16->{21,22},17->{21,22} ,18->{21,22},19->{21,22},20->{21,22},21->{35},22->{2,3,4},23->{25,26,27,28,29},24->{35},25->{30,31,32} ,26->{33,34},27->{33,34},28->{33,34},29->{33,34},30->{33,34},31->{33,34},32->{33,34},33->{35},34->{2,3,4} ,35->{}] + Applied Processor: CloseWith False + Details: () NO