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) [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 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) [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: 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) [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: 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.35(A,B,C,D,E,F,G,H ,I) [C = 1] evalbinsearchStepSize2bbin.3(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.5(A,B,C,D,J,F,G,H ,I) [0 >= C] evalbinsearchStepSize2bbin.3(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.6(A,B,C,D,J,F,G,H ,I) [0 >= C] evalbinsearchStepSize2bbin.3(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.7(A,B,C,D,J,F,G,H ,I) [0 >= C] evalbinsearchStepSize2bbin.4(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.5(A,B,C,D,J,F,G,H ,I) [C >= 2] evalbinsearchStepSize2bbin.4(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.6(A,B,C,D,J,F,G,H ,I) [C >= 2] evalbinsearchStepSize2bbin.4(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.7(A,B,C,D,J,F,G,H ,I) [C >= 2] evalbinsearchStepSize2bb1in.5(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.8(A,B,C,D,E,F,G,H ,I) [0 >= 1 + B] evalbinsearchStepSize2bb1in.5(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.9(A,B,C,D,E,F,G,H ,I) [0 >= 1 + B] evalbinsearchStepSize2bb1in.5(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.10(A,B,C,D,E,F,G,H ,I) [0 >= 1 + B] evalbinsearchStepSize2bb1in.6(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.8(A,B,C,D,E,F,G,H ,I) [B >= 1] evalbinsearchStepSize2bb1in.6(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.9(A,B,C,D,E,F,G,H ,I) [B >= 1] evalbinsearchStepSize2bb1in.6(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.10(A,B,C,D,E,F,G,H ,I) [B >= 1] evalbinsearchStepSize2bb1in.7(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,C,G,H ,I) [B = 0] evalbinsearchStepSize2bb1in.7(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.12(A,B,C,D,E,C,G,H ,I) [B = 0] evalbinsearchStepSize2bb2in.8(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,0,G,H ,I) [C = 0] evalbinsearchStepSize2bb2in.8(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.12(A,B,C,D,E,0,G,H ,I) [C = 0] evalbinsearchStepSize2bb2in.9(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,J,G,H ,I) [C >= 1 && J >= 0 && C >= 2*J && 1 + 2*J >= C] evalbinsearchStepSize2bb2in.9(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.12(A,B,C,D,E,J,G,H ,I) [C >= 1 && J >= 0 && C >= 2*J && 1 + 2*J >= C] evalbinsearchStepSize2bb2in.10(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,J,G,H ,I) [0 >= 1 + C && 0 >= J && 2*J >= C && 1 + C >= 2*J] evalbinsearchStepSize2bb2in.10(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.12(A,B,C,D,E,J,G,H ,I) [0 >= 1 + C && 0 >= J && 2*J >= C && 1 + C >= 2*J] evalbinsearchStepSize2bb3in.11(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.13(A,B,C,D,E,F,G,H ,I) [E >= 1 + G] evalbinsearchStepSize2bb3in.11(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.14(A,B,C,D,E,F,G,H ,I) [E >= 1 + G] evalbinsearchStepSize2bb3in.11(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.15(A,B,C,D,E,F,G,H ,I) [E >= 1 + G] evalbinsearchStepSize2bb3in.11(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.16(A,B,C,D,E,F,G,H ,I) [E >= 1 + G] evalbinsearchStepSize2bb3in.11(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.17(A,B,C,D,E,F,G,H ,I) [E >= 1 + G] evalbinsearchStepSize2bb3in.12(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb9in.23(A,B,C,D,E,F,G,H ,I) [G >= E] evalbinsearchStepSize2bb3in.12(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb9in.24(A,B,C,D,E,F,G,H ,I) [G >= E] evalbinsearchStepSize2bb4in.13(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in.18(A,B,C,D,E,F,G,H ,I) [A = 1 && B = 0] evalbinsearchStepSize2bb4in.13(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in.19(A,B,C,D,E,F,G,H ,I) [A = 1 && B = 0] evalbinsearchStepSize2bb4in.13(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in.20(A,B,C,D,E,F,G,H ,I) [A = 1 && B = 0] evalbinsearchStepSize2bb4in.14(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,B ,F) [0 >= A] evalbinsearchStepSize2bb4in.14(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,B ,F) [0 >= A] evalbinsearchStepSize2bb4in.15(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,B ,F) [A >= 2] evalbinsearchStepSize2bb4in.15(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,B ,F) [A >= 2] evalbinsearchStepSize2bb4in.16(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,B ,F) [0 >= 1 + B] evalbinsearchStepSize2bb4in.16(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,B ,F) [0 >= 1 + B] evalbinsearchStepSize2bb4in.17(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,B ,F) [B >= 1] evalbinsearchStepSize2bb4in.17(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,B ,F) [B >= 1] evalbinsearchStepSize2bb6in.18(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,1 ,0) [F = 0] evalbinsearchStepSize2bb6in.18(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,1 ,0) [F = 0] evalbinsearchStepSize2bb6in.19(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,1 ,J) [F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb6in.19(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,1 ,J) [F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb6in.20(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,1 ,J) [0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb6in.20(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,1 ,J) [0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin.35(A,B,C,D,E,F,G,H ,I) [D + I >= 256] evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.2(2,H,I,D + I,E,F,G,H ,I) [255 >= D + I] evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.3(2,H,I,D + I,E,F,G,H ,I) [255 >= D + I] evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.4(2,H,I,D + I,E,F,G,H ,I) [255 >= D + I] evalbinsearchStepSize2bb9in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.25(A,B,C,D,E,F,G,H ,I) [G >= 1 + E] evalbinsearchStepSize2bb9in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.26(A,B,C,D,E,F,G,H ,I) [G >= 1 + E] evalbinsearchStepSize2bb9in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.27(A,B,C,D,E,F,G,H ,I) [G >= 1 + E] evalbinsearchStepSize2bb9in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.28(A,B,C,D,E,F,G,H ,I) [G >= 1 + E] evalbinsearchStepSize2bb9in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.29(A,B,C,D,E,F,G,H ,I) [G >= 1 + E] evalbinsearchStepSize2bb9in.24(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin.35(A,B,C,D,E,F,G,H ,I) [E >= G] evalbinsearchStepSize2bb10in.25(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in.30(A,B,C,D,E,F,G,H ,I) [A = 2 && B = 0] evalbinsearchStepSize2bb10in.25(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in.31(A,B,C,D,E,F,G,H ,I) [A = 2 && B = 0] evalbinsearchStepSize2bb10in.25(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in.32(A,B,C,D,E,F,G,H ,I) [A = 2 && B = 0] evalbinsearchStepSize2bb10in.26(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,B ,F) [1 >= A] evalbinsearchStepSize2bb10in.26(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,B ,F) [1 >= A] evalbinsearchStepSize2bb10in.27(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,B ,F) [A >= 3] evalbinsearchStepSize2bb10in.27(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,B ,F) [A >= 3] evalbinsearchStepSize2bb10in.28(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,B ,F) [0 >= 1 + B] evalbinsearchStepSize2bb10in.28(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,B ,F) [0 >= 1 + B] evalbinsearchStepSize2bb10in.29(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,B ,F) [B >= 1] evalbinsearchStepSize2bb10in.29(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,B ,F) [B >= 1] evalbinsearchStepSize2bb12in.30(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,1 ,0) [F = 0] evalbinsearchStepSize2bb12in.30(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,1 ,0) [F = 0] evalbinsearchStepSize2bb12in.31(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,1 ,J) [F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb12in.31(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,1 ,J) [F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb12in.32(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,1 ,J) [0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb12in.32(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,1 ,J) [0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin.35(A,B,C,D,E,F,G,H ,I) [I >= 1 + D] evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.2(1,H,I,D + -1*I,E,F,G,H ,I) [D >= I] evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.3(1,H,I,D + -1*I,E,F,G,H ,I) [D >= I] evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.4(1,H,I,D + -1*I,E,F,G,H ,I) [D >= I] evalbinsearchStepSize2returnin.35(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H ,I) True Signature: {(evalbinsearchStepSize2bb10in.25,9) ;(evalbinsearchStepSize2bb10in.26,9) ;(evalbinsearchStepSize2bb10in.27,9) ;(evalbinsearchStepSize2bb10in.28,9) ;(evalbinsearchStepSize2bb10in.29,9) ;(evalbinsearchStepSize2bb12in.30,9) ;(evalbinsearchStepSize2bb12in.31,9) ;(evalbinsearchStepSize2bb12in.32,9) ;(evalbinsearchStepSize2bb13in.33,9) ;(evalbinsearchStepSize2bb13in.34,9) ;(evalbinsearchStepSize2bb1in.5,9) ;(evalbinsearchStepSize2bb1in.6,9) ;(evalbinsearchStepSize2bb1in.7,9) ;(evalbinsearchStepSize2bb2in.10,9) ;(evalbinsearchStepSize2bb2in.8,9) ;(evalbinsearchStepSize2bb2in.9,9) ;(evalbinsearchStepSize2bb3in.11,9) ;(evalbinsearchStepSize2bb3in.12,9) ;(evalbinsearchStepSize2bb4in.13,9) ;(evalbinsearchStepSize2bb4in.14,9) ;(evalbinsearchStepSize2bb4in.15,9) ;(evalbinsearchStepSize2bb4in.16,9) ;(evalbinsearchStepSize2bb4in.17,9) ;(evalbinsearchStepSize2bb6in.18,9) ;(evalbinsearchStepSize2bb6in.19,9) ;(evalbinsearchStepSize2bb6in.20,9) ;(evalbinsearchStepSize2bb7in.21,9) ;(evalbinsearchStepSize2bb7in.22,9) ;(evalbinsearchStepSize2bb9in.23,9) ;(evalbinsearchStepSize2bb9in.24,9) ;(evalbinsearchStepSize2bbin.2,9) ;(evalbinsearchStepSize2bbin.3,9) ;(evalbinsearchStepSize2bbin.4,9) ;(evalbinsearchStepSize2entryin.1,9) ;(evalbinsearchStepSize2returnin.35,9) ;(evalbinsearchStepSize2start.0,9) ;(evalbinsearchStepSize2stop.36,9)} Rule Graph: [0->{1},1->{6,7,8},2->{78},3->{9,10,11},4->{12,13,14},5->{15,16},6->{9,10,11},7->{12,13,14},8->{15,16} ,9->{17,18},10->{19,20},11->{21,22},12->{17,18},13->{19,20},14->{21,22},15->{23,24,25,26,27},16->{28,29} ,17->{23,24,25,26,27},18->{28,29},19->{23,24,25,26,27},20->{28,29},21->{23,24,25,26,27},22->{28,29},23->{30 ,31,32},24->{33,34},25->{35,36},26->{37,38},27->{39,40},28->{51,52,53,54,55},29->{56},30->{41,42},31->{43 ,44},32->{45,46},33->{47},34->{48,49,50},35->{47},36->{48,49,50},37->{47},38->{48,49,50},39->{47},40->{48,49 ,50},41->{47},42->{48,49,50},43->{47},44->{48,49,50},45->{47},46->{48,49,50},47->{78},48->{2},49->{3,4,5} ,50->{6,7,8},51->{57,58,59},52->{60,61},53->{62,63},54->{64,65},55->{66,67},56->{78},57->{68,69},58->{70,71} ,59->{72,73},60->{74},61->{75,76,77},62->{74},63->{75,76,77},64->{74},65->{75,76,77},66->{74},67->{75,76,77} ,68->{74},69->{75,76,77},70->{74},71->{75,76,77},72->{74},73->{75,76,77},74->{78},75->{2},76->{3,4,5},77->{6 ,7,8},78->{}] + 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.35(A,B,C,D,E,F,G,H ,I) [C = 1] evalbinsearchStepSize2bbin.3(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.5(A,B,C,D,J,F,G,H ,I) [0 >= C] evalbinsearchStepSize2bbin.3(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.6(A,B,C,D,J,F,G,H ,I) [0 >= C] evalbinsearchStepSize2bbin.3(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.7(A,B,C,D,J,F,G,H ,I) [0 >= C] evalbinsearchStepSize2bbin.4(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.5(A,B,C,D,J,F,G,H ,I) [C >= 2] evalbinsearchStepSize2bbin.4(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.6(A,B,C,D,J,F,G,H ,I) [C >= 2] evalbinsearchStepSize2bbin.4(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb1in.7(A,B,C,D,J,F,G,H ,I) [C >= 2] evalbinsearchStepSize2bb1in.5(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.8(A,B,C,D,E,F,G,H ,I) [0 >= 1 + B] evalbinsearchStepSize2bb1in.5(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.9(A,B,C,D,E,F,G,H ,I) [0 >= 1 + B] evalbinsearchStepSize2bb1in.5(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.10(A,B,C,D,E,F,G,H ,I) [0 >= 1 + B] evalbinsearchStepSize2bb1in.6(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.8(A,B,C,D,E,F,G,H ,I) [B >= 1] evalbinsearchStepSize2bb1in.6(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.9(A,B,C,D,E,F,G,H ,I) [B >= 1] evalbinsearchStepSize2bb1in.6(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb2in.10(A,B,C,D,E,F,G,H ,I) [B >= 1] evalbinsearchStepSize2bb1in.7(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,C,G,H ,I) [B = 0] evalbinsearchStepSize2bb1in.7(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.12(A,B,C,D,E,C,G,H ,I) [B = 0] evalbinsearchStepSize2bb2in.8(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,0,G,H ,I) [C = 0] evalbinsearchStepSize2bb2in.8(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.12(A,B,C,D,E,0,G,H ,I) [C = 0] evalbinsearchStepSize2bb2in.9(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,J,G,H ,I) [C >= 1 && J >= 0 && C >= 2*J && 1 + 2*J >= C] evalbinsearchStepSize2bb2in.9(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.12(A,B,C,D,E,J,G,H ,I) [C >= 1 && J >= 0 && C >= 2*J && 1 + 2*J >= C] evalbinsearchStepSize2bb2in.10(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.11(A,B,C,D,E,J,G,H ,I) [0 >= 1 + C && 0 >= J && 2*J >= C && 1 + C >= 2*J] evalbinsearchStepSize2bb2in.10(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb3in.12(A,B,C,D,E,J,G,H ,I) [0 >= 1 + C && 0 >= J && 2*J >= C && 1 + C >= 2*J] evalbinsearchStepSize2bb3in.11(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.13(A,B,C,D,E,F,G,H ,I) [E >= 1 + G] evalbinsearchStepSize2bb3in.11(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.14(A,B,C,D,E,F,G,H ,I) [E >= 1 + G] evalbinsearchStepSize2bb3in.11(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.15(A,B,C,D,E,F,G,H ,I) [E >= 1 + G] evalbinsearchStepSize2bb3in.11(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.16(A,B,C,D,E,F,G,H ,I) [E >= 1 + G] evalbinsearchStepSize2bb3in.11(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb4in.17(A,B,C,D,E,F,G,H ,I) [E >= 1 + G] evalbinsearchStepSize2bb3in.12(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb9in.23(A,B,C,D,E,F,G,H ,I) [G >= E] evalbinsearchStepSize2bb3in.12(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb9in.24(A,B,C,D,E,F,G,H ,I) [G >= E] evalbinsearchStepSize2bb4in.13(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in.18(A,B,C,D,E,F,G,H ,I) [A = 1 && B = 0] evalbinsearchStepSize2bb4in.13(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in.19(A,B,C,D,E,F,G,H ,I) [A = 1 && B = 0] evalbinsearchStepSize2bb4in.13(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb6in.20(A,B,C,D,E,F,G,H ,I) [A = 1 && B = 0] evalbinsearchStepSize2bb4in.14(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,B ,F) [0 >= A] evalbinsearchStepSize2bb4in.14(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,B ,F) [0 >= A] evalbinsearchStepSize2bb4in.15(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,B ,F) [A >= 2] evalbinsearchStepSize2bb4in.15(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,B ,F) [A >= 2] evalbinsearchStepSize2bb4in.16(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,B ,F) [0 >= 1 + B] evalbinsearchStepSize2bb4in.16(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,B ,F) [0 >= 1 + B] evalbinsearchStepSize2bb4in.17(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,B ,F) [B >= 1] evalbinsearchStepSize2bb4in.17(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,B ,F) [B >= 1] evalbinsearchStepSize2bb6in.18(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,1 ,0) [F = 0] evalbinsearchStepSize2bb6in.18(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,1 ,0) [F = 0] evalbinsearchStepSize2bb6in.19(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,1 ,J) [F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb6in.19(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,1 ,J) [F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb6in.20(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,1 ,J) [0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb6in.20(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,1 ,J) [0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb7in.21(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin.35(A,B,C,D,E,F,G,H ,I) [D + I >= 256] evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.2(2,H,I,D + I,E,F,G,H ,I) [255 >= D + I] evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.3(2,H,I,D + I,E,F,G,H ,I) [255 >= D + I] evalbinsearchStepSize2bb7in.22(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.4(2,H,I,D + I,E,F,G,H ,I) [255 >= D + I] evalbinsearchStepSize2bb9in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.25(A,B,C,D,E,F,G,H ,I) [G >= 1 + E] evalbinsearchStepSize2bb9in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.26(A,B,C,D,E,F,G,H ,I) [G >= 1 + E] evalbinsearchStepSize2bb9in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.27(A,B,C,D,E,F,G,H ,I) [G >= 1 + E] evalbinsearchStepSize2bb9in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.28(A,B,C,D,E,F,G,H ,I) [G >= 1 + E] evalbinsearchStepSize2bb9in.23(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb10in.29(A,B,C,D,E,F,G,H ,I) [G >= 1 + E] evalbinsearchStepSize2bb9in.24(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin.35(A,B,C,D,E,F,G,H ,I) [E >= G] evalbinsearchStepSize2bb10in.25(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in.30(A,B,C,D,E,F,G,H ,I) [A = 2 && B = 0] evalbinsearchStepSize2bb10in.25(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in.31(A,B,C,D,E,F,G,H ,I) [A = 2 && B = 0] evalbinsearchStepSize2bb10in.25(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb12in.32(A,B,C,D,E,F,G,H ,I) [A = 2 && B = 0] evalbinsearchStepSize2bb10in.26(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,B ,F) [1 >= A] evalbinsearchStepSize2bb10in.26(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,B ,F) [1 >= A] evalbinsearchStepSize2bb10in.27(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,B ,F) [A >= 3] evalbinsearchStepSize2bb10in.27(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,B ,F) [A >= 3] evalbinsearchStepSize2bb10in.28(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,B ,F) [0 >= 1 + B] evalbinsearchStepSize2bb10in.28(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,B ,F) [0 >= 1 + B] evalbinsearchStepSize2bb10in.29(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,B ,F) [B >= 1] evalbinsearchStepSize2bb10in.29(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,B ,F) [B >= 1] evalbinsearchStepSize2bb12in.30(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,1 ,0) [F = 0] evalbinsearchStepSize2bb12in.30(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,1 ,0) [F = 0] evalbinsearchStepSize2bb12in.31(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,1 ,J) [F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb12in.31(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,1 ,J) [F >= 1 && J >= 0 && F >= 2*J && 1 + 2*J >= F] evalbinsearchStepSize2bb12in.32(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,1 ,J) [0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb12in.32(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,1 ,J) [0 >= 1 + F && 0 >= J && 2*J >= F && 1 + F >= 2*J] evalbinsearchStepSize2bb13in.33(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2returnin.35(A,B,C,D,E,F,G,H ,I) [I >= 1 + D] evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.2(1,H,I,D + -1*I,E,F,G,H ,I) [D >= I] evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.3(1,H,I,D + -1*I,E,F,G,H ,I) [D >= I] evalbinsearchStepSize2bb13in.34(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2bbin.4(1,H,I,D + -1*I,E,F,G,H ,I) [D >= I] evalbinsearchStepSize2returnin.35(A,B,C,D,E,F,G,H,I) -> evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True evalbinsearchStepSize2stop.36(A,B,C,D,E,F,G,H,I) -> exitus616(A,B,C,D,E,F,G,H ,I) True Signature: {(evalbinsearchStepSize2bb10in.25,9) ;(evalbinsearchStepSize2bb10in.26,9) ;(evalbinsearchStepSize2bb10in.27,9) ;(evalbinsearchStepSize2bb10in.28,9) ;(evalbinsearchStepSize2bb10in.29,9) ;(evalbinsearchStepSize2bb12in.30,9) ;(evalbinsearchStepSize2bb12in.31,9) ;(evalbinsearchStepSize2bb12in.32,9) ;(evalbinsearchStepSize2bb13in.33,9) ;(evalbinsearchStepSize2bb13in.34,9) ;(evalbinsearchStepSize2bb1in.5,9) ;(evalbinsearchStepSize2bb1in.6,9) ;(evalbinsearchStepSize2bb1in.7,9) ;(evalbinsearchStepSize2bb2in.10,9) ;(evalbinsearchStepSize2bb2in.8,9) ;(evalbinsearchStepSize2bb2in.9,9) ;(evalbinsearchStepSize2bb3in.11,9) ;(evalbinsearchStepSize2bb3in.12,9) ;(evalbinsearchStepSize2bb4in.13,9) ;(evalbinsearchStepSize2bb4in.14,9) ;(evalbinsearchStepSize2bb4in.15,9) ;(evalbinsearchStepSize2bb4in.16,9) ;(evalbinsearchStepSize2bb4in.17,9) ;(evalbinsearchStepSize2bb6in.18,9) ;(evalbinsearchStepSize2bb6in.19,9) ;(evalbinsearchStepSize2bb6in.20,9) ;(evalbinsearchStepSize2bb7in.21,9) ;(evalbinsearchStepSize2bb7in.22,9) ;(evalbinsearchStepSize2bb9in.23,9) ;(evalbinsearchStepSize2bb9in.24,9) ;(evalbinsearchStepSize2bbin.2,9) ;(evalbinsearchStepSize2bbin.3,9) ;(evalbinsearchStepSize2bbin.4,9) ;(evalbinsearchStepSize2entryin.1,9) ;(evalbinsearchStepSize2returnin.35,9) ;(evalbinsearchStepSize2start.0,9) ;(evalbinsearchStepSize2stop.36,9) ;(exitus616,9)} Rule Graph: [0->{1},1->{6,7,8},2->{78},3->{9,10,11},4->{12,13,14},5->{15,16},6->{9,10,11},7->{12,13,14},8->{15,16} ,9->{17,18},10->{19,20},11->{21,22},12->{17,18},13->{19,20},14->{21,22},15->{23,24,25,26,27},16->{28,29} ,17->{23,24,25,26,27},18->{28,29},19->{23,24,25,26,27},20->{28,29},21->{23,24,25,26,27},22->{28,29},23->{30 ,31,32},24->{33,34},25->{35,36},26->{37,38},27->{39,40},28->{51,52,53,54,55},29->{56},30->{41,42},31->{43 ,44},32->{45,46},33->{47},34->{48,49,50},35->{47},36->{48,49,50},37->{47},38->{48,49,50},39->{47},40->{48,49 ,50},41->{47},42->{48,49,50},43->{47},44->{48,49,50},45->{47},46->{48,49,50},47->{78},48->{2},49->{3,4,5} ,50->{6,7,8},51->{57,58,59},52->{60,61},53->{62,63},54->{64,65},55->{66,67},56->{78},57->{68,69},58->{70,71} ,59->{72,73},60->{74},61->{75,76,77},62->{74},63->{75,76,77},64->{74},65->{75,76,77},66->{74},67->{75,76,77} ,68->{74},69->{75,76,77},70->{74},71->{75,76,77},72->{74},73->{75,76,77},74->{78},75->{2},76->{3,4,5},77->{6 ,7,8},78->{79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95}] + 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,83,84,85,86,87,88,89,90,91,92,93,94,95] | `- p:[6,50,34,24,15,5,49,36,25,17,9,3,76,61,52,28,16,8,77,63,53,65,54,67,55,69,57,51,71,58,73,59,18,12,4,7,20,10,13,22,11,14,19,21,38,26,40,27,42,30,23,44,31,46,32] c: [30,31,32,42,44,46,51,57,58,59,69,71,73] | `- p:[3,49,34,24,15,5,76,61,52,28,16,8,50,36,25,17,9,6,77,63,53,65,54,67,55,12,4,7,19,10,13,21,11,14,38,26,40,27,18,20,22] c: [] MAYBE