WORST_CASE(?,O(log(n)*n^1))
* Step 1: UnreachableRules WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          0.  mergeSort0(A,B,C) -> msplit(A,B,C)                                                               True                                                                                 (?,1)
          1.  mergeSort1(A,B,C) -> mergeSort(B,B,C)                                                            True                                                                                 (?,1)
          2.  mergeSort2(A,B,C) -> mergeSort(C,B,C)                                                            True                                                                                 (?,1)
          3.  mergeSort3(A,B,C) -> merge(B,C,C)                                                                True                                                                                 (?,1)
          4.  mergeSort(A,B,C)  -> c4(mergeSort0(A,D,E),mergeSort1(A,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,1)
          5.  out2msplit(A,B,C) -> out2msplit(-2 + A,B,C)                                                      [A >= 2]                                                                             (?,1)
          6.  out1msplit(A,B,C) -> out1msplit(-2 + A,B,C)                                                      [A >= 2]                                                                             (?,1)
          7.  msplit(A,B,C)     -> msplit(-2 + A,B,C)                                                          [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)      -> merge(-1 + A,B,C)                                                           [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)      -> merge(A,-1 + B,C)                                                           [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)      -> mergeSort(A,B,C)                                                            True                                                                                 (1,1)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [0->{7},1->{4},2->{4},3->{8,9},4->{0,1,2,3},5->{5},6->{6},7->{7},8->{8,9},9->{8,9},10->{4}]
        
    + Applied Processor:
        UnreachableRules
    + Details:
        Following transitions are not reachable from the starting states and are removed: [5,6]
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          0.  mergeSort0(A,B,C) -> msplit(A,B,C)                                                               True                                                                                 (?,1)
          1.  mergeSort1(A,B,C) -> mergeSort(B,B,C)                                                            True                                                                                 (?,1)
          2.  mergeSort2(A,B,C) -> mergeSort(C,B,C)                                                            True                                                                                 (?,1)
          3.  mergeSort3(A,B,C) -> merge(B,C,C)                                                                True                                                                                 (?,1)
          4.  mergeSort(A,B,C)  -> c4(mergeSort0(A,D,E),mergeSort1(A,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,1)
          7.  msplit(A,B,C)     -> msplit(-2 + A,B,C)                                                          [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)      -> merge(-1 + A,B,C)                                                           [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)      -> merge(A,-1 + B,C)                                                           [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)      -> mergeSort(A,B,C)                                                            True                                                                                 (1,1)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [0->{7},1->{4},2->{4},3->{8,9},4->{0,1,2,3},7->{7},8->{8,9},9->{8,9},10->{4}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (< 0,0,A>,     A, .= 0) (< 0,0,B>,     B, .= 0) (< 0,0,C>, C, .= 0) 
          (< 1,0,A>,     B, .= 0) (< 1,0,B>,     B, .= 0) (< 1,0,C>, C, .= 0) 
          (< 2,0,A>,     C, .= 0) (< 2,0,B>,     B, .= 0) (< 2,0,C>, C, .= 0) 
          (< 3,0,A>,     B, .= 0) (< 3,0,B>,     C, .= 0) (< 3,0,C>, C, .= 0) 
          (< 4,0,A>,     A, .= 0) (< 4,0,B>, 1 + A, .+ 1) (< 4,0,C>, A, .= 0) 
          (< 4,1,A>,     A, .= 0) (< 4,1,B>, 1 + A, .+ 1) (< 4,1,C>, A, .= 0) 
          (< 4,2,A>,     A, .= 0) (< 4,2,B>, 1 + A, .+ 1) (< 4,2,C>, A, .= 0) 
          (< 4,3,A>,     A, .= 0) (< 4,3,B>, 1 + A, .+ 1) (< 4,3,C>, A, .= 0) 
          (< 7,0,A>, 2 + A, .+ 2) (< 7,0,B>,     B, .= 0) (< 7,0,C>, C, .= 0) 
          (< 8,0,A>, 1 + A, .+ 1) (< 8,0,B>,     B, .= 0) (< 8,0,C>, C, .= 0) 
          (< 9,0,A>,     A, .= 0) (< 9,0,B>, 1 + B, .+ 1) (< 9,0,C>, C, .= 0) 
          (<10,0,A>,     A, .= 0) (<10,0,B>,     B, .= 0) (<10,0,C>, C, .= 0) 
* Step 3: SizeboundsProc WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          0.  mergeSort0(A,B,C) -> msplit(A,B,C)                                                               True                                                                                 (?,1)
          1.  mergeSort1(A,B,C) -> mergeSort(B,B,C)                                                            True                                                                                 (?,1)
          2.  mergeSort2(A,B,C) -> mergeSort(C,B,C)                                                            True                                                                                 (?,1)
          3.  mergeSort3(A,B,C) -> merge(B,C,C)                                                                True                                                                                 (?,1)
          4.  mergeSort(A,B,C)  -> c4(mergeSort0(A,D,E),mergeSort1(A,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,1)
          7.  msplit(A,B,C)     -> msplit(-2 + A,B,C)                                                          [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)      -> merge(-1 + A,B,C)                                                           [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)      -> merge(A,-1 + B,C)                                                           [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)      -> mergeSort(A,B,C)                                                            True                                                                                 (1,1)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [0->{7},1->{4},2->{4},3->{8,9},4->{0,1,2,3},7->{7},8->{8,9},9->{8,9},10->{4}]
        Sizebounds:
          (< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) 
          (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) 
          (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) 
          (< 4,1,A>, ?) (< 4,1,B>, ?) (< 4,1,C>, ?) 
          (< 4,2,A>, ?) (< 4,2,B>, ?) (< 4,2,C>, ?) 
          (< 4,3,A>, ?) (< 4,3,B>, ?) (< 4,3,C>, ?) 
          (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) 
          (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) 
          (< 1,0,A>, ?) (< 1,0,B>, B) (< 1,0,C>, C) 
          (< 2,0,A>, ?) (< 2,0,B>, B) (< 2,0,C>, C) 
          (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) 
          (< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?) 
          (< 4,1,A>, A) (< 4,1,B>, ?) (< 4,1,C>, ?) 
          (< 4,2,A>, A) (< 4,2,B>, ?) (< 4,2,C>, ?) 
          (< 4,3,A>, A) (< 4,3,B>, ?) (< 4,3,C>, ?) 
          (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) 
          (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) 
* Step 4: ChainProcessor WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          0.  mergeSort0(A,B,C) -> msplit(A,B,C)                                                               True                                                                                 (?,1)
          1.  mergeSort1(A,B,C) -> mergeSort(B,B,C)                                                            True                                                                                 (?,1)
          2.  mergeSort2(A,B,C) -> mergeSort(C,B,C)                                                            True                                                                                 (?,1)
          3.  mergeSort3(A,B,C) -> merge(B,C,C)                                                                True                                                                                 (?,1)
          4.  mergeSort(A,B,C)  -> c4(mergeSort0(A,D,E),mergeSort1(A,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,1)
          7.  msplit(A,B,C)     -> msplit(-2 + A,B,C)                                                          [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)      -> merge(-1 + A,B,C)                                                           [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)      -> merge(A,-1 + B,C)                                                           [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)      -> mergeSort(A,B,C)                                                            True                                                                                 (1,1)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [0->{7},1->{4},2->{4},3->{8,9},4->{0,1,2,3},7->{7},8->{8,9},9->{8,9},10->{4}]
        Sizebounds:
          (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) 
          (< 1,0,A>, ?) (< 1,0,B>, B) (< 1,0,C>, C) 
          (< 2,0,A>, ?) (< 2,0,B>, B) (< 2,0,C>, C) 
          (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) 
          (< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, ?) 
          (< 4,1,A>, A) (< 4,1,B>, ?) (< 4,1,C>, ?) 
          (< 4,2,A>, A) (< 4,2,B>, ?) (< 4,2,C>, ?) 
          (< 4,3,A>, A) (< 4,3,B>, ?) (< 4,3,C>, ?) 
          (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) 
          (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) 
    + Applied Processor:
        ChainProcessor False [0,1,2,3,4,7,8,9,10]
    + Details:
        We chained rule 4 to obtain the rules [11] .
* Step 5: UnreachableRules WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          0.  mergeSort0(A,B,C) -> msplit(A,B,C)                                                           True                                                                                 (?,1)
          1.  mergeSort1(A,B,C) -> mergeSort(B,B,C)                                                        True                                                                                 (?,1)
          2.  mergeSort2(A,B,C) -> mergeSort(C,B,C)                                                        True                                                                                 (?,1)
          3.  mergeSort3(A,B,C) -> merge(B,C,C)                                                            True                                                                                 (?,1)
          7.  msplit(A,B,C)     -> msplit(-2 + A,B,C)                                                      [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)      -> merge(-1 + A,B,C)                                                       [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)      -> merge(A,-1 + B,C)                                                       [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)      -> mergeSort(A,B,C)                                                        True                                                                                 (1,1)
          11. mergeSort(A,B,C)  -> c4(msplit(A,D,E),mergeSort1(A,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,2)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [0->{7},1->{11},2->{11},3->{8,9},7->{7},8->{8,9},9->{8,9},10->{11},11->{1,2,3,7}]
        Sizebounds:
          (< 0,0,A>, A) (< 0,0,B>, B) (< 0,0,C>, C) 
          (< 1,0,A>, ?) (< 1,0,B>, B) (< 1,0,C>, C) 
          (< 2,0,A>, ?) (< 2,0,B>, B) (< 2,0,C>, C) 
          (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) 
          (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) 
          (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) 
          (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) 
    + Applied Processor:
        UnreachableRules
    + Details:
        Following transitions are not reachable from the starting states and are removed: [0]
* Step 6: ChainProcessor WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          1.  mergeSort1(A,B,C) -> mergeSort(B,B,C)                                                        True                                                                                 (?,1)
          2.  mergeSort2(A,B,C) -> mergeSort(C,B,C)                                                        True                                                                                 (?,1)
          3.  mergeSort3(A,B,C) -> merge(B,C,C)                                                            True                                                                                 (?,1)
          7.  msplit(A,B,C)     -> msplit(-2 + A,B,C)                                                      [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)      -> merge(-1 + A,B,C)                                                       [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)      -> merge(A,-1 + B,C)                                                       [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)      -> mergeSort(A,B,C)                                                        True                                                                                 (1,1)
          11. mergeSort(A,B,C)  -> c4(msplit(A,D,E),mergeSort1(A,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,2)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [1->{11},2->{11},3->{8,9},7->{7},8->{8,9},9->{8,9},10->{11},11->{1,2,3,7}]
        Sizebounds:
          (< 1,0,A>, ?) (< 1,0,B>, B) (< 1,0,C>, C) 
          (< 2,0,A>, ?) (< 2,0,B>, B) (< 2,0,C>, C) 
          (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) 
          (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) 
          (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) 
          (<11,0,A>, A) (<11,0,B>, B) (<11,0,C>, C) 
    + Applied Processor:
        ChainProcessor False [1,2,3,7,8,9,10,11]
    + Details:
        We chained rule 11 to obtain the rules [12] .
* Step 7: UnreachableRules WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          1.  mergeSort1(A,B,C) -> mergeSort(B,B,C)                                                       True                                                                                 (?,1)
          2.  mergeSort2(A,B,C) -> mergeSort(C,B,C)                                                       True                                                                                 (?,1)
          3.  mergeSort3(A,B,C) -> merge(B,C,C)                                                           True                                                                                 (?,1)
          7.  msplit(A,B,C)     -> msplit(-2 + A,B,C)                                                     [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)      -> merge(-1 + A,B,C)                                                      [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)      -> merge(A,-1 + B,C)                                                      [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)      -> mergeSort(A,B,C)                                                       True                                                                                 (1,1)
          12. mergeSort(A,B,C)  -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,3)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [1->{12},2->{12},3->{8,9},7->{7},8->{8,9},9->{8,9},10->{12},12->{2,3,7,12}]
        Sizebounds:
          (< 1,0,A>, ?) (< 1,0,B>, B) (< 1,0,C>, C) 
          (< 2,0,A>, ?) (< 2,0,B>, B) (< 2,0,C>, C) 
          (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) 
          (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) 
          (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) 
          (<12,0,A>, ?) (<12,0,B>, B) (<12,0,C>, C) 
    + Applied Processor:
        UnreachableRules
    + Details:
        Following transitions are not reachable from the starting states and are removed: [1]
* Step 8: ChainProcessor WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          2.  mergeSort2(A,B,C) -> mergeSort(C,B,C)                                                       True                                                                                 (?,1)
          3.  mergeSort3(A,B,C) -> merge(B,C,C)                                                           True                                                                                 (?,1)
          7.  msplit(A,B,C)     -> msplit(-2 + A,B,C)                                                     [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)      -> merge(-1 + A,B,C)                                                      [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)      -> merge(A,-1 + B,C)                                                      [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)      -> mergeSort(A,B,C)                                                       True                                                                                 (1,1)
          12. mergeSort(A,B,C)  -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort2(A,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,3)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [2->{12},3->{8,9},7->{7},8->{8,9},9->{8,9},10->{12},12->{2,3,7,12}]
        Sizebounds:
          (< 2,0,A>, ?) (< 2,0,B>, B) (< 2,0,C>, C) 
          (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) 
          (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) 
          (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) 
          (<12,0,A>, ?) (<12,0,B>, B) (<12,0,C>, C) 
    + Applied Processor:
        ChainProcessor False [2,3,7,8,9,10,12]
    + Details:
        We chained rule 12 to obtain the rules [13] .
* Step 9: UnreachableRules WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          2.  mergeSort2(A,B,C) -> mergeSort(C,B,C)                                                      True                                                                                 (?,1)
          3.  mergeSort3(A,B,C) -> merge(B,C,C)                                                          True                                                                                 (?,1)
          7.  msplit(A,B,C)     -> msplit(-2 + A,B,C)                                                    [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)      -> merge(-1 + A,B,C)                                                     [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)      -> merge(A,-1 + B,C)                                                     [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)      -> mergeSort(A,B,C)                                                      True                                                                                 (1,1)
          13. mergeSort(A,B,C)  -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,4)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [2->{13},3->{8,9},7->{7},8->{8,9},9->{8,9},10->{13},13->{3,7,13}]
        Sizebounds:
          (< 2,0,A>, ?) (< 2,0,B>, B) (< 2,0,C>, C) 
          (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) 
          (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) 
          (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) 
          (<13,0,A>, ?) (<13,0,B>, B) (<13,0,C>, C) 
    + Applied Processor:
        UnreachableRules
    + Details:
        Following transitions are not reachable from the starting states and are removed: [2]
* Step 10: ChainProcessor WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          3.  mergeSort3(A,B,C) -> merge(B,C,C)                                                          True                                                                                 (?,1)
          7.  msplit(A,B,C)     -> msplit(-2 + A,B,C)                                                    [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)      -> merge(-1 + A,B,C)                                                     [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)      -> merge(A,-1 + B,C)                                                     [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)      -> mergeSort(A,B,C)                                                      True                                                                                 (1,1)
          13. mergeSort(A,B,C)  -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),mergeSort3(A,D,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,4)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [3->{8,9},7->{7},8->{8,9},9->{8,9},10->{13},13->{3,7,13}]
        Sizebounds:
          (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) 
          (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) 
          (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) 
          (<13,0,A>, ?) (<13,0,B>, B) (<13,0,C>, C) 
    + Applied Processor:
        ChainProcessor False [3,7,8,9,10,13]
    + Details:
        We chained rule 13 to obtain the rules [14] .
* Step 11: UnreachableRules WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          3.  mergeSort3(A,B,C) -> merge(B,C,C)                                                     True                                                                                 (?,1)
          7.  msplit(A,B,C)     -> msplit(-2 + A,B,C)                                               [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)      -> merge(-1 + A,B,C)                                                [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)      -> merge(A,-1 + B,C)                                                [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)      -> mergeSort(A,B,C)                                                 True                                                                                 (1,1)
          14. mergeSort(A,B,C)  -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),merge(D,E,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,5)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [3->{8,9},7->{7},8->{8,9},9->{8,9},10->{14},14->{7,8,9,14}]
        Sizebounds:
          (< 3,0,A>, B) (< 3,0,B>, C) (< 3,0,C>, C) 
          (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) 
          (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) 
          (<14,0,A>, B) (<14,0,B>, C) (<14,0,C>, C) 
    + Applied Processor:
        UnreachableRules
    + Details:
        Following transitions are not reachable from the starting states and are removed: [3]
* Step 12: LocalSizeboundsProc WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          7.  msplit(A,B,C)    -> msplit(-2 + A,B,C)                                               [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)     -> merge(-1 + A,B,C)                                                [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)     -> merge(A,-1 + B,C)                                                [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)     -> mergeSort(A,B,C)                                                 True                                                                                 (1,1)
          14. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),merge(D,E,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,5)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [7->{7},8->{8,9},9->{8,9},10->{14},14->{7,8,9,14}]
        Sizebounds:
          (< 7,0,A>, ?) (< 7,0,B>, B) (< 7,0,C>, C) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, C) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, C) 
          (<10,0,A>, A) (<10,0,B>, B) (<10,0,C>, C) 
          (<14,0,A>, B) (<14,0,B>, C) (<14,0,C>, C) 
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (< 7,0,A>, 2 + A, .+ 2) (< 7,0,B>,     B, .= 0) (< 7,0,C>, C, .= 0) 
          (< 8,0,A>, 1 + A, .+ 1) (< 8,0,B>,     B, .= 0) (< 8,0,C>, C, .= 0) 
          (< 9,0,A>,     A, .= 0) (< 9,0,B>, 1 + B, .+ 1) (< 9,0,C>, C, .= 0) 
          (<10,0,A>,     A, .= 0) (<10,0,B>,     B, .= 0) (<10,0,C>, C, .= 0) 
          (<14,0,A>,     A, .= 0) (<14,0,B>, 1 + A, .+ 1) (<14,0,C>, A, .= 0) 
          (<14,1,A>, 1 + A, .+ 1) (<14,1,B>, 1 + A, .+ 1) (<14,1,C>, A, .= 0) 
          (<14,2,A>,     A, .= 0) (<14,2,B>, 1 + A, .+ 1) (<14,2,C>, A, .= 0) 
          (<14,3,A>, 1 + A, .+ 1) (<14,3,B>,     A, .= 0) (<14,3,C>, A, .= 0) 
* Step 13: SizeboundsProc WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          7.  msplit(A,B,C)    -> msplit(-2 + A,B,C)                                               [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)     -> merge(-1 + A,B,C)                                                [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)     -> merge(A,-1 + B,C)                                                [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)     -> mergeSort(A,B,C)                                                 True                                                                                 (1,1)
          14. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),merge(D,E,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,5)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [7->{7},8->{8,9},9->{8,9},10->{14},14->{7,8,9,14}]
        Sizebounds:
          (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) 
          (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) 
          (<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) 
          (<14,1,A>, ?) (<14,1,B>, ?) (<14,1,C>, ?) 
          (<14,2,A>, ?) (<14,2,B>, ?) (<14,2,C>, ?) 
          (<14,3,A>, ?) (<14,3,B>, ?) (<14,3,C>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (< 7,0,A>, ?) (< 7,0,B>, 1 + A) (< 7,0,C>, A) 
          (< 8,0,A>, ?) (< 8,0,B>,     ?) (< 8,0,C>, A) 
          (< 9,0,A>, ?) (< 9,0,B>,     ?) (< 9,0,C>, A) 
          (<10,0,A>, A) (<10,0,B>,     B) (<10,0,C>, C) 
          (<14,0,A>, ?) (<14,0,B>, 1 + A) (<14,0,C>, A) 
          (<14,1,A>, ?) (<14,1,B>, 1 + A) (<14,1,C>, A) 
          (<14,2,A>, ?) (<14,2,B>, 1 + A) (<14,2,C>, A) 
          (<14,3,A>, ?) (<14,3,B>,     A) (<14,3,C>, A) 
* Step 14: LoopRecurrenceProcessor WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          7.  msplit(A,B,C)    -> msplit(-2 + A,B,C)                                               [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)     -> merge(-1 + A,B,C)                                                [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)     -> merge(A,-1 + B,C)                                                [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)     -> mergeSort(A,B,C)                                                 True                                                                                 (1,1)
          14. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),merge(D,E,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,5)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [7->{7},8->{8,9},9->{8,9},10->{14},14->{7,8,9,14}]
        Sizebounds:
          (< 7,0,A>, ?) (< 7,0,B>, 1 + A) (< 7,0,C>, A) 
          (< 8,0,A>, ?) (< 8,0,B>,     ?) (< 8,0,C>, A) 
          (< 9,0,A>, ?) (< 9,0,B>,     ?) (< 9,0,C>, A) 
          (<10,0,A>, A) (<10,0,B>,     B) (<10,0,C>, C) 
          (<14,0,A>, ?) (<14,0,B>, 1 + A) (<14,0,C>, A) 
          (<14,1,A>, ?) (<14,1,B>, 1 + A) (<14,1,C>, A) 
          (<14,2,A>, ?) (<14,2,B>, 1 + A) (<14,2,C>, A) 
          (<14,3,A>, ?) (<14,3,B>,     A) (<14,3,C>, A) 
    + Applied Processor:
        LoopRecurrenceProcessor [7]
    + Details:
        Applying the recurrence pattern linear * f to the expression A yields the solution 0 .
* Step 15: LoopRecurrenceProcessor WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          7.  msplit(A,B,C)    -> msplit(-2 + A,B,C)                                               [A >= 2]                                                                             (?,1)
          8.  merge(A,B,C)     -> merge(-1 + A,B,C)                                                [A >= 1 && B >= 1]                                                                   (?,1)
          9.  merge(A,B,C)     -> merge(A,-1 + B,C)                                                [A >= 1 && B >= 1]                                                                   (?,1)
          10. start(A,B,C)     -> mergeSort(A,B,C)                                                 True                                                                                 (1,1)
          14. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),merge(D,E,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (?,5)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [7->{7},8->{8,9},9->{8,9},10->{14},14->{7,8,9,14}]
        Sizebounds:
          (< 7,0,A>, ?) (< 7,0,B>, 1 + A) (< 7,0,C>, A) 
          (< 8,0,A>, ?) (< 8,0,B>,     ?) (< 8,0,C>, A) 
          (< 9,0,A>, ?) (< 9,0,B>,     ?) (< 9,0,C>, A) 
          (<10,0,A>, A) (<10,0,B>,     B) (<10,0,C>, C) 
          (<14,0,A>, ?) (<14,0,B>, 1 + A) (<14,0,C>, A) 
          (<14,1,A>, ?) (<14,1,B>, 1 + A) (<14,1,C>, A) 
          (<14,2,A>, ?) (<14,2,B>, 1 + A) (<14,2,C>, A) 
          (<14,3,A>, ?) (<14,3,B>,     A) (<14,3,C>, A) 
    + Applied Processor:
        LoopRecurrenceProcessor [14]
    + Details:
        Applying the recurrence pattern Master Theorem (B) to the expression A yields the solution log(A)^1*(A) + 0 .
* Step 16: UnsatPaths WORST_CASE(?,O(log(n)*n^1))
    + Considered Problem:
        Rules:
          7.  msplit(A,B,C)    -> msplit(-2 + A,B,C)                                               [A >= 2]                                                                             (log(A)^1*(A) + 0,1)
          8.  merge(A,B,C)     -> merge(-1 + A,B,C)                                                [A >= 1 && B >= 1]                                                                   (log(A)^1*(A) + 0,1)
          9.  merge(A,B,C)     -> merge(A,-1 + B,C)                                                [A >= 1 && B >= 1]                                                                   (log(A)^1*(A) + 0,1)
          10. start(A,B,C)     -> mergeSort(A,B,C)                                                 True                                                                                 (1,1)               
          14. mergeSort(A,B,C) -> c4(msplit(A,D,E),mergeSort(D,D,E),mergeSort(E,D,E),merge(D,E,E)) [A >= 2 && D >= 0 && E >= 0 && 1 + A >= 2*D && 2*D >= A && A >= 2*E && 1 + 2*E >= A] (log(A)^1*(A) + 0,5)
        Signature:
          {(merge,3)
          ;(mergeSort,3)
          ;(mergeSort0,3)
          ;(mergeSort1,3)
          ;(mergeSort2,3)
          ;(mergeSort3,3)
          ;(msplit,3)
          ;(out1msplit,3)
          ;(out2msplit,3)
          ;(start,3)}
        Flow Graph:
          [7->{7},8->{8,9},9->{8,9},10->{14},14->{7,8,9,14}]
        Sizebounds:
          (< 7,0,A>, ?) (< 7,0,B>, 1 + A) (< 7,0,C>, A) 
          (< 8,0,A>, ?) (< 8,0,B>,     ?) (< 8,0,C>, A) 
          (< 9,0,A>, ?) (< 9,0,B>,     ?) (< 9,0,C>, A) 
          (<10,0,A>, A) (<10,0,B>,     B) (<10,0,C>, C) 
          (<14,0,A>, ?) (<14,0,B>, 1 + A) (<14,0,C>, A) 
          (<14,1,A>, ?) (<14,1,B>, 1 + A) (<14,1,C>, A) 
          (<14,2,A>, ?) (<14,2,B>, 1 + A) (<14,2,C>, A) 
          (<14,3,A>, ?) (<14,3,B>,     A) (<14,3,C>, A) 
    + Applied Processor:
        UnsatPaths
    + Details:
        The problem is already solved.

WORST_CASE(?,O(log(n)*n^1))