YES * Step 1: TrivialSCCs YES + Considered Problem: Rules: 0. evalrealheapsortstep2start(A,B,C,D) -> evalrealheapsortstep2entryin(A,B,C,D) True (1,1) 1. evalrealheapsortstep2entryin(A,B,C,D) -> evalrealheapsortstep2returnin(A,B,C,D) [2 >= A] (?,1) 2. evalrealheapsortstep2entryin(A,B,C,D) -> evalrealheapsortstep2bbin(A,B,C,D) [A >= 3] (?,1) 3. evalrealheapsortstep2returnin(A,B,C,D) -> evalrealheapsortstep2stop(A,B,C,D) True (?,1) 4. evalrealheapsortstep2bbin(A,B,C,D) -> evalrealheapsortstep2bb11in(A,0,C,D) [-3 + A >= 0] (?,1) 5. evalrealheapsortstep2bb11in(A,B,C,D) -> evalrealheapsortstep2returnin(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] (?,1) 6. evalrealheapsortstep2bb11in(A,B,C,D) -> evalrealheapsortstep2bb1in(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] (?,1) 7. evalrealheapsortstep2bb1in(A,B,C,D) -> evalrealheapsortstep2bb9in(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 8. evalrealheapsortstep2bb9in(A,B,C,D) -> evalrealheapsortstep2bb10in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] (?,1) 9. evalrealheapsortstep2bb9in(A,B,C,D) -> evalrealheapsortstep2bb2in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] (?,1) 10. evalrealheapsortstep2bb10in(A,B,C,D) -> evalrealheapsortstep2bb11in(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 11. evalrealheapsortstep2bb2in(A,B,C,D) -> evalrealheapsortstep2bb3in(A,B,C,D) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] 12. evalrealheapsortstep2bb2in(A,B,C,D) -> evalrealheapsortstep2bb4in(A,B,C,D) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] 13. evalrealheapsortstep2bb3in(A,B,C,D) -> evalrealheapsortstep2bb5in(A,B,C,D) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 14. evalrealheapsortstep2bb3in(A,B,C,D) -> evalrealheapsortstep2bb4in(A,B,C,D) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 15. evalrealheapsortstep2bb4in(A,B,C,D) -> evalrealheapsortstep2bb6in(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 16. evalrealheapsortstep2bb6in(A,B,C,D) -> evalrealheapsortstep2bb9in(A,B,A,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 17. evalrealheapsortstep2bb6in(A,B,C,D) -> evalrealheapsortstep2bb7in(A,B,C,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 18. evalrealheapsortstep2bb5in(A,B,C,D) -> evalrealheapsortstep2bb6in(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 19. evalrealheapsortstep2bb7in(A,B,C,D) -> evalrealheapsortstep2bb9in(A,B,D,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] Signature: {(evalrealheapsortstep2bb10in,4) ;(evalrealheapsortstep2bb11in,4) ;(evalrealheapsortstep2bb1in,4) ;(evalrealheapsortstep2bb2in,4) ;(evalrealheapsortstep2bb3in,4) ;(evalrealheapsortstep2bb4in,4) ;(evalrealheapsortstep2bb5in,4) ;(evalrealheapsortstep2bb6in,4) ;(evalrealheapsortstep2bb7in,4) ;(evalrealheapsortstep2bb9in,4) ;(evalrealheapsortstep2bbin,4) ;(evalrealheapsortstep2entryin,4) ;(evalrealheapsortstep2returnin,4) ;(evalrealheapsortstep2start,4) ;(evalrealheapsortstep2stop,4)} Flow Graph: [0->{1,2},1->{3},2->{4},3->{},4->{5,6},5->{3},6->{7},7->{8,9},8->{10},9->{11,12},10->{5,6},11->{13,14} ,12->{15},13->{18},14->{15},15->{16,17},16->{8,9},17->{19},18->{16,17},19->{8,9}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths YES + Considered Problem: Rules: 0. evalrealheapsortstep2start(A,B,C,D) -> evalrealheapsortstep2entryin(A,B,C,D) True (1,1) 1. evalrealheapsortstep2entryin(A,B,C,D) -> evalrealheapsortstep2returnin(A,B,C,D) [2 >= A] (1,1) 2. evalrealheapsortstep2entryin(A,B,C,D) -> evalrealheapsortstep2bbin(A,B,C,D) [A >= 3] (1,1) 3. evalrealheapsortstep2returnin(A,B,C,D) -> evalrealheapsortstep2stop(A,B,C,D) True (1,1) 4. evalrealheapsortstep2bbin(A,B,C,D) -> evalrealheapsortstep2bb11in(A,0,C,D) [-3 + A >= 0] (1,1) 5. evalrealheapsortstep2bb11in(A,B,C,D) -> evalrealheapsortstep2returnin(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] (1,1) 6. evalrealheapsortstep2bb11in(A,B,C,D) -> evalrealheapsortstep2bb1in(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] (?,1) 7. evalrealheapsortstep2bb1in(A,B,C,D) -> evalrealheapsortstep2bb9in(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 8. evalrealheapsortstep2bb9in(A,B,C,D) -> evalrealheapsortstep2bb10in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] (?,1) 9. evalrealheapsortstep2bb9in(A,B,C,D) -> evalrealheapsortstep2bb2in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] (?,1) 10. evalrealheapsortstep2bb10in(A,B,C,D) -> evalrealheapsortstep2bb11in(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 11. evalrealheapsortstep2bb2in(A,B,C,D) -> evalrealheapsortstep2bb3in(A,B,C,D) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] 12. evalrealheapsortstep2bb2in(A,B,C,D) -> evalrealheapsortstep2bb4in(A,B,C,D) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] 13. evalrealheapsortstep2bb3in(A,B,C,D) -> evalrealheapsortstep2bb5in(A,B,C,D) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 14. evalrealheapsortstep2bb3in(A,B,C,D) -> evalrealheapsortstep2bb4in(A,B,C,D) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 15. evalrealheapsortstep2bb4in(A,B,C,D) -> evalrealheapsortstep2bb6in(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 16. evalrealheapsortstep2bb6in(A,B,C,D) -> evalrealheapsortstep2bb9in(A,B,A,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 17. evalrealheapsortstep2bb6in(A,B,C,D) -> evalrealheapsortstep2bb7in(A,B,C,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 18. evalrealheapsortstep2bb5in(A,B,C,D) -> evalrealheapsortstep2bb6in(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 19. evalrealheapsortstep2bb7in(A,B,C,D) -> evalrealheapsortstep2bb9in(A,B,D,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] Signature: {(evalrealheapsortstep2bb10in,4) ;(evalrealheapsortstep2bb11in,4) ;(evalrealheapsortstep2bb1in,4) ;(evalrealheapsortstep2bb2in,4) ;(evalrealheapsortstep2bb3in,4) ;(evalrealheapsortstep2bb4in,4) ;(evalrealheapsortstep2bb5in,4) ;(evalrealheapsortstep2bb6in,4) ;(evalrealheapsortstep2bb7in,4) ;(evalrealheapsortstep2bb9in,4) ;(evalrealheapsortstep2bbin,4) ;(evalrealheapsortstep2entryin,4) ;(evalrealheapsortstep2returnin,4) ;(evalrealheapsortstep2start,4) ;(evalrealheapsortstep2stop,4)} Flow Graph: [0->{1,2},1->{3},2->{4},3->{},4->{5,6},5->{3},6->{7},7->{8,9},8->{10},9->{11,12},10->{5,6},11->{13,14} ,12->{15},13->{18},14->{15},15->{16,17},16->{8,9},17->{19},18->{16,17},19->{8,9}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,5),(16,9)] * Step 3: Looptree YES + Considered Problem: Rules: 0. evalrealheapsortstep2start(A,B,C,D) -> evalrealheapsortstep2entryin(A,B,C,D) True (1,1) 1. evalrealheapsortstep2entryin(A,B,C,D) -> evalrealheapsortstep2returnin(A,B,C,D) [2 >= A] (1,1) 2. evalrealheapsortstep2entryin(A,B,C,D) -> evalrealheapsortstep2bbin(A,B,C,D) [A >= 3] (1,1) 3. evalrealheapsortstep2returnin(A,B,C,D) -> evalrealheapsortstep2stop(A,B,C,D) True (1,1) 4. evalrealheapsortstep2bbin(A,B,C,D) -> evalrealheapsortstep2bb11in(A,0,C,D) [-3 + A >= 0] (1,1) 5. evalrealheapsortstep2bb11in(A,B,C,D) -> evalrealheapsortstep2returnin(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 1 + B >= A] (1,1) 6. evalrealheapsortstep2bb11in(A,B,C,D) -> evalrealheapsortstep2bb1in(A,B,C,D) [B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 2 + B] (?,1) 7. evalrealheapsortstep2bb1in(A,B,C,D) -> evalrealheapsortstep2bb9in(A,B,0,D) [-2 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 8. evalrealheapsortstep2bb9in(A,B,C,D) -> evalrealheapsortstep2bb10in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && 2 + B + 2*C >= A] (?,1) 9. evalrealheapsortstep2bb9in(A,B,C,D) -> evalrealheapsortstep2bb2in(A,B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 3 + B + 2*C] (?,1) 10. evalrealheapsortstep2bb10in(A,B,C,D) -> evalrealheapsortstep2bb11in(A,1 + B,C,D) [C >= 0 && B + C >= 0 && -3 + A + C >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] (?,1) 11. evalrealheapsortstep2bb2in(A,B,C,D) -> evalrealheapsortstep2bb3in(A,B,C,D) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A >= 4 + B + 2*C] 12. evalrealheapsortstep2bb2in(A,B,C,D) -> evalrealheapsortstep2bb4in(A,B,C,D) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0 && A = 3 + B + 2*C] 13. evalrealheapsortstep2bb3in(A,B,C,D) -> evalrealheapsortstep2bb5in(A,B,C,D) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 14. evalrealheapsortstep2bb3in(A,B,C,D) -> evalrealheapsortstep2bb4in(A,B,C,D) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 15. evalrealheapsortstep2bb4in(A,B,C,D) -> evalrealheapsortstep2bb6in(A,B,C,1 + 2*C) [-3 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 16. evalrealheapsortstep2bb6in(A,B,C,D) -> evalrealheapsortstep2bb9in(A,B,A,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 17. evalrealheapsortstep2bb6in(A,B,C,D) -> evalrealheapsortstep2bb7in(A,B,C,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] 18. evalrealheapsortstep2bb5in(A,B,C,D) -> evalrealheapsortstep2bb6in(A,B,C,2 + 2*C) [-4 + A + -1*C >= 0 (?,1) && C >= 0 && B + C >= 0 && -4 + A + C >= 0 && -4 + A + -1*B >= 0 && B >= 0 && -4 + A + B >= 0 && -4 + A >= 0] 19. evalrealheapsortstep2bb7in(A,B,C,D) -> evalrealheapsortstep2bb9in(A,B,D,D) [-1 + D >= 0 (?,1) && -1 + C + D >= 0 && -1 + -1*C + D >= 0 && -1 + B + D >= 0 && -4 + A + D >= 0 && -3 + A + -1*C >= 0 && C >= 0 && B + C >= 0 && -3 + A + C >= 0 && -3 + A + -1*B >= 0 && B >= 0 && -3 + A + B >= 0 && -3 + A >= 0] Signature: {(evalrealheapsortstep2bb10in,4) ;(evalrealheapsortstep2bb11in,4) ;(evalrealheapsortstep2bb1in,4) ;(evalrealheapsortstep2bb2in,4) ;(evalrealheapsortstep2bb3in,4) ;(evalrealheapsortstep2bb4in,4) ;(evalrealheapsortstep2bb5in,4) ;(evalrealheapsortstep2bb6in,4) ;(evalrealheapsortstep2bb7in,4) ;(evalrealheapsortstep2bb9in,4) ;(evalrealheapsortstep2bbin,4) ;(evalrealheapsortstep2entryin,4) ;(evalrealheapsortstep2returnin,4) ;(evalrealheapsortstep2start,4) ;(evalrealheapsortstep2stop,4)} Flow Graph: [0->{1,2},1->{3},2->{4},3->{},4->{6},5->{3},6->{7},7->{8,9},8->{10},9->{11,12},10->{5,6},11->{13,14} ,12->{15},13->{18},14->{15},15->{16,17},16->{8},17->{19},18->{16,17},19->{8,9}] + Applied Processor: Looptree + 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] | `- p:[6,10,8,7,16,15,12,9,19,17,18,13,11,14] c: [7] | `- p:[9,19,17,15,12,14,11,18,13] c: [19] YES