MAYBE
* Step 1: TrivialSCCs MAYBE
    + 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:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: UnsatPaths MAYBE
    + 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,1)
          2.  evalrealheapsortstep2entryin(A,B,C,D)  -> evalrealheapsortstep2returnin(A,B,C,D)    [2 >= A]           (1,1)
          3.  evalrealheapsortstep2bbin(A,B,C,D)     -> evalrealheapsortstep2bb11in(A,0,C,D)      True               (1,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,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,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 3: UnreachableRules MAYBE
    + 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,1)
          2.  evalrealheapsortstep2entryin(A,B,C,D)  -> evalrealheapsortstep2returnin(A,B,C,D)    [2 >= A]           (1,1)
          3.  evalrealheapsortstep2bbin(A,B,C,D)     -> evalrealheapsortstep2bb11in(A,0,C,D)      True               (1,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,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,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 4: AddSinks MAYBE
    + 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,1)
          2.  evalrealheapsortstep2entryin(A,B,C,D)  -> evalrealheapsortstep2returnin(A,B,C,D)    [2 >= A]           (1,1)
          3.  evalrealheapsortstep2bbin(A,B,C,D)     -> evalrealheapsortstep2bb11in(A,0,C,D)      True               (1,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,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,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:
        AddSinks
    + Details:
        ()
* Step 5: Failure MAYBE
  + 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)
        21. evalrealheapsortstep2returnin(A,B,C,D) -> exitus616(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)
        ;(exitus616,4)}
      Flow Graph:
        [0->{1,2},1->{3},2->{20,21},3->{4,5},4->{6},5->{20,21},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->{},21->{}]
      
  + Applied Processor:
      LooptreeTransformer
  + Details:
      We construct a looptree:
        P: [0,1,2,3,4,5,6,7,8,9,10,12,13,14,15,16,17,18,19,20,21]
        |
        `- p:[4,19,8,6,17,14,9,7,18,16,15,13,10,12] c: [4]
           |
           `- p:[7,17,14,9,12,10,15,13,18,16] c: []
MAYBE