NO
* Step 1: UnsatPaths NO
    + Considered Problem:
        Rules:
          0.  evalrealheapsortstep2start(A,B,C,D)    -> evalrealheapsortstep2entryin(A,B,C,D)     True               (1,1)
          1.  evalrealheapsortstep2entryin(A,B,C,D)  -> evalrealheapsortstep2bbin(A,B,C,D)        [A >= 3]           (?,1)
          2.  evalrealheapsortstep2entryin(A,B,C,D)  -> evalrealheapsortstep2returnin(A,B,C,D)    [2 >= A]           (?,1)
          3.  evalrealheapsortstep2bbin(A,B,C,D)     -> evalrealheapsortstep2bb11in(A,0,C,D)      True               (?,1)
          4.  evalrealheapsortstep2bb11in(A,B,C,D)   -> evalrealheapsortstep2bb1in(A,B,C,D)       [A >= 2 + B]       (?,1)
          5.  evalrealheapsortstep2bb11in(A,B,C,D)   -> evalrealheapsortstep2returnin(A,B,C,D)    [1 + B >= A]       (?,1)
          6.  evalrealheapsortstep2bb1in(A,B,C,D)    -> evalrealheapsortstep2bb9in(A,B,0,D)       True               (?,1)
          7.  evalrealheapsortstep2bb9in(A,B,C,D)    -> evalrealheapsortstep2bb2in(A,B,C,D)       [A >= 3 + B + 2*C] (?,1)
          8.  evalrealheapsortstep2bb9in(A,B,C,D)    -> evalrealheapsortstep2bb10in(A,B,C,D)      [2 + B + 2*C >= A] (?,1)
          9.  evalrealheapsortstep2bb2in(A,B,C,D)    -> evalrealheapsortstep2bb4in(A,B,C,D)       [A = 3 + B + 2*C]  (?,1)
          10. evalrealheapsortstep2bb2in(A,B,C,D)    -> evalrealheapsortstep2bb3in(A,B,C,D)       [A >= 4 + B + 2*C] (?,1)
          11. evalrealheapsortstep2bb2in(A,B,C,D)    -> evalrealheapsortstep2bb3in(A,B,C,D)       [2 + B + 2*C >= A] (?,1)
          12. evalrealheapsortstep2bb3in(A,B,C,D)    -> evalrealheapsortstep2bb4in(A,B,C,D)       True               (?,1)
          13. evalrealheapsortstep2bb3in(A,B,C,D)    -> evalrealheapsortstep2bb5in(A,B,C,D)       True               (?,1)
          14. evalrealheapsortstep2bb4in(A,B,C,D)    -> evalrealheapsortstep2bb6in(A,B,C,1 + 2*C) True               (?,1)
          15. evalrealheapsortstep2bb5in(A,B,C,D)    -> evalrealheapsortstep2bb6in(A,B,C,2 + 2*C) True               (?,1)
          16. evalrealheapsortstep2bb6in(A,B,C,D)    -> evalrealheapsortstep2bb7in(A,B,C,D)       True               (?,1)
          17. evalrealheapsortstep2bb6in(A,B,C,D)    -> evalrealheapsortstep2bb9in(A,B,A,D)       True               (?,1)
          18. evalrealheapsortstep2bb7in(A,B,C,D)    -> evalrealheapsortstep2bb9in(A,B,D,D)       True               (?,1)
          19. evalrealheapsortstep2bb10in(A,B,C,D)   -> evalrealheapsortstep2bb11in(A,1 + B,C,D)  True               (?,1)
          20. evalrealheapsortstep2returnin(A,B,C,D) -> evalrealheapsortstep2stop(A,B,C,D)        True               (?,1)
        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->{20},3->{4,5},4->{6},5->{20},6->{7,8},7->{9,10,11},8->{19},9->{14},10->{12,13},11->{12
          ,13},12->{14},13->{15},14->{16,17},15->{16,17},16->{18},17->{7,8},18->{7,8},19->{4,5},20->{}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(7,11)]
* Step 2: UnreachableRules NO
    + Considered Problem:
        Rules:
          0.  evalrealheapsortstep2start(A,B,C,D)    -> evalrealheapsortstep2entryin(A,B,C,D)     True               (1,1)
          1.  evalrealheapsortstep2entryin(A,B,C,D)  -> evalrealheapsortstep2bbin(A,B,C,D)        [A >= 3]           (?,1)
          2.  evalrealheapsortstep2entryin(A,B,C,D)  -> evalrealheapsortstep2returnin(A,B,C,D)    [2 >= A]           (?,1)
          3.  evalrealheapsortstep2bbin(A,B,C,D)     -> evalrealheapsortstep2bb11in(A,0,C,D)      True               (?,1)
          4.  evalrealheapsortstep2bb11in(A,B,C,D)   -> evalrealheapsortstep2bb1in(A,B,C,D)       [A >= 2 + B]       (?,1)
          5.  evalrealheapsortstep2bb11in(A,B,C,D)   -> evalrealheapsortstep2returnin(A,B,C,D)    [1 + B >= A]       (?,1)
          6.  evalrealheapsortstep2bb1in(A,B,C,D)    -> evalrealheapsortstep2bb9in(A,B,0,D)       True               (?,1)
          7.  evalrealheapsortstep2bb9in(A,B,C,D)    -> evalrealheapsortstep2bb2in(A,B,C,D)       [A >= 3 + B + 2*C] (?,1)
          8.  evalrealheapsortstep2bb9in(A,B,C,D)    -> evalrealheapsortstep2bb10in(A,B,C,D)      [2 + B + 2*C >= A] (?,1)
          9.  evalrealheapsortstep2bb2in(A,B,C,D)    -> evalrealheapsortstep2bb4in(A,B,C,D)       [A = 3 + B + 2*C]  (?,1)
          10. evalrealheapsortstep2bb2in(A,B,C,D)    -> evalrealheapsortstep2bb3in(A,B,C,D)       [A >= 4 + B + 2*C] (?,1)
          11. evalrealheapsortstep2bb2in(A,B,C,D)    -> evalrealheapsortstep2bb3in(A,B,C,D)       [2 + B + 2*C >= A] (?,1)
          12. evalrealheapsortstep2bb3in(A,B,C,D)    -> evalrealheapsortstep2bb4in(A,B,C,D)       True               (?,1)
          13. evalrealheapsortstep2bb3in(A,B,C,D)    -> evalrealheapsortstep2bb5in(A,B,C,D)       True               (?,1)
          14. evalrealheapsortstep2bb4in(A,B,C,D)    -> evalrealheapsortstep2bb6in(A,B,C,1 + 2*C) True               (?,1)
          15. evalrealheapsortstep2bb5in(A,B,C,D)    -> evalrealheapsortstep2bb6in(A,B,C,2 + 2*C) True               (?,1)
          16. evalrealheapsortstep2bb6in(A,B,C,D)    -> evalrealheapsortstep2bb7in(A,B,C,D)       True               (?,1)
          17. evalrealheapsortstep2bb6in(A,B,C,D)    -> evalrealheapsortstep2bb9in(A,B,A,D)       True               (?,1)
          18. evalrealheapsortstep2bb7in(A,B,C,D)    -> evalrealheapsortstep2bb9in(A,B,D,D)       True               (?,1)
          19. evalrealheapsortstep2bb10in(A,B,C,D)   -> evalrealheapsortstep2bb11in(A,1 + B,C,D)  True               (?,1)
          20. evalrealheapsortstep2returnin(A,B,C,D) -> evalrealheapsortstep2stop(A,B,C,D)        True               (?,1)
        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->{20},3->{4,5},4->{6},5->{20},6->{7,8},7->{9,10},8->{19},9->{14},10->{12,13},11->{12
          ,13},12->{14},13->{15},14->{16,17},15->{16,17},16->{18},17->{7,8},18->{7,8},19->{4,5},20->{}]
        
    + Applied Processor:
        UnreachableRules
    + Details:
        Following transitions are not reachable from the starting states and are revomed: [11]
* Step 3: FromIts NO
    + Considered Problem:
        Rules:
          0.  evalrealheapsortstep2start(A,B,C,D)    -> evalrealheapsortstep2entryin(A,B,C,D)     True               (1,1)
          1.  evalrealheapsortstep2entryin(A,B,C,D)  -> evalrealheapsortstep2bbin(A,B,C,D)        [A >= 3]           (?,1)
          2.  evalrealheapsortstep2entryin(A,B,C,D)  -> evalrealheapsortstep2returnin(A,B,C,D)    [2 >= A]           (?,1)
          3.  evalrealheapsortstep2bbin(A,B,C,D)     -> evalrealheapsortstep2bb11in(A,0,C,D)      True               (?,1)
          4.  evalrealheapsortstep2bb11in(A,B,C,D)   -> evalrealheapsortstep2bb1in(A,B,C,D)       [A >= 2 + B]       (?,1)
          5.  evalrealheapsortstep2bb11in(A,B,C,D)   -> evalrealheapsortstep2returnin(A,B,C,D)    [1 + B >= A]       (?,1)
          6.  evalrealheapsortstep2bb1in(A,B,C,D)    -> evalrealheapsortstep2bb9in(A,B,0,D)       True               (?,1)
          7.  evalrealheapsortstep2bb9in(A,B,C,D)    -> evalrealheapsortstep2bb2in(A,B,C,D)       [A >= 3 + B + 2*C] (?,1)
          8.  evalrealheapsortstep2bb9in(A,B,C,D)    -> evalrealheapsortstep2bb10in(A,B,C,D)      [2 + B + 2*C >= A] (?,1)
          9.  evalrealheapsortstep2bb2in(A,B,C,D)    -> evalrealheapsortstep2bb4in(A,B,C,D)       [A = 3 + B + 2*C]  (?,1)
          10. evalrealheapsortstep2bb2in(A,B,C,D)    -> evalrealheapsortstep2bb3in(A,B,C,D)       [A >= 4 + B + 2*C] (?,1)
          12. evalrealheapsortstep2bb3in(A,B,C,D)    -> evalrealheapsortstep2bb4in(A,B,C,D)       True               (?,1)
          13. evalrealheapsortstep2bb3in(A,B,C,D)    -> evalrealheapsortstep2bb5in(A,B,C,D)       True               (?,1)
          14. evalrealheapsortstep2bb4in(A,B,C,D)    -> evalrealheapsortstep2bb6in(A,B,C,1 + 2*C) True               (?,1)
          15. evalrealheapsortstep2bb5in(A,B,C,D)    -> evalrealheapsortstep2bb6in(A,B,C,2 + 2*C) True               (?,1)
          16. evalrealheapsortstep2bb6in(A,B,C,D)    -> evalrealheapsortstep2bb7in(A,B,C,D)       True               (?,1)
          17. evalrealheapsortstep2bb6in(A,B,C,D)    -> evalrealheapsortstep2bb9in(A,B,A,D)       True               (?,1)
          18. evalrealheapsortstep2bb7in(A,B,C,D)    -> evalrealheapsortstep2bb9in(A,B,D,D)       True               (?,1)
          19. evalrealheapsortstep2bb10in(A,B,C,D)   -> evalrealheapsortstep2bb11in(A,1 + B,C,D)  True               (?,1)
          20. evalrealheapsortstep2returnin(A,B,C,D) -> evalrealheapsortstep2stop(A,B,C,D)        True               (?,1)
        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->{20},3->{4,5},4->{6},5->{20},6->{7,8},7->{9,10},8->{19},9->{14},10->{12,13},12->{14}
          ,13->{15},14->{16,17},15->{16,17},16->{18},17->{7,8},18->{7,8},19->{4,5},20->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 4: CloseWith NO
    + Considered Problem:
        Rules:
          evalrealheapsortstep2start(A,B,C,D)     -> evalrealheapsortstep2entryin(A,B,C,D)       True
          evalrealheapsortstep2entryin(A,B,C,D)   -> evalrealheapsortstep2bbin(A,B,C,D)          [A >= 3]
          evalrealheapsortstep2entryin(A,B,C,D)   -> evalrealheapsortstep2returnin(A,B,C,D)      [2 >= A]
          evalrealheapsortstep2bbin(A,B,C,D)      -> evalrealheapsortstep2bb11in(A,0,C,D)        True
          evalrealheapsortstep2bb11in(A,B,C,D)    -> evalrealheapsortstep2bb1in(A,B,C,D)         [A >= 2 + B]
          evalrealheapsortstep2bb11in(A,B,C,D)    -> evalrealheapsortstep2returnin(A,B,C,D)      [1 + B >= A]
          evalrealheapsortstep2bb1in(A,B,C,D)     -> evalrealheapsortstep2bb9in(A,B,0,D)         True
          evalrealheapsortstep2bb9in(A,B,C,D)     -> evalrealheapsortstep2bb2in(A,B,C,D)         [A >= 3 + B + 2*C]
          evalrealheapsortstep2bb9in(A,B,C,D)     -> evalrealheapsortstep2bb10in(A,B,C,D)        [2 + B + 2*C >= A]
          evalrealheapsortstep2bb2in(A,B,C,D)     -> evalrealheapsortstep2bb4in(A,B,C,D)         [A = 3 + B + 2*C]
          evalrealheapsortstep2bb2in(A,B,C,D)     -> evalrealheapsortstep2bb3in(A,B,C,D)         [A >= 4 + B + 2*C]
          evalrealheapsortstep2bb3in(A,B,C,D)     -> evalrealheapsortstep2bb4in(A,B,C,D)         True
          evalrealheapsortstep2bb3in(A,B,C,D)     -> evalrealheapsortstep2bb5in(A,B,C,D)         True
          evalrealheapsortstep2bb4in(A,B,C,D)     -> evalrealheapsortstep2bb6in(A,B,C,1 + 2*C)   True
          evalrealheapsortstep2bb5in(A,B,C,D)     -> evalrealheapsortstep2bb6in(A,B,C,2 + 2*C)   True
          evalrealheapsortstep2bb6in(A,B,C,D)     -> evalrealheapsortstep2bb7in(A,B,C,D)         True
          evalrealheapsortstep2bb6in(A,B,C,D)     -> evalrealheapsortstep2bb9in(A,B,A,D)         True
          evalrealheapsortstep2bb7in(A,B,C,D)     -> evalrealheapsortstep2bb9in(A,B,D,D)         True
          evalrealheapsortstep2bb10in(A,B,C,D)    -> evalrealheapsortstep2bb11in(A,1 + B,C,D)    True
          evalrealheapsortstep2returnin(A,B,C,D)  -> evalrealheapsortstep2stop(A,B,C,D)          True
        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)}
        Rule Graph:
          [0->{1,2},1->{3},2->{20},3->{4,5},4->{6},5->{20},6->{7,8},7->{9,10},8->{19},9->{14},10->{12,13},12->{14}
          ,13->{15},14->{16,17},15->{16,17},16->{18},17->{7,8},18->{7,8},19->{4,5},20->{}]
    + Applied Processor:
        CloseWith False
    + Details:
        ()

NO