WORST_CASE(?,O(n^2))
* Step 1: TrivialSCCs WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  matrixmult0(A,B,C,D)  -> transAcc(B,B,0,D)                                                  True                                   (?,1)
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                           True                                   (?,1)
          2.  matrixmult2(A,B,C,D)  -> makeBase(A,B,C,D)                                                  True                                   (?,1)
          3.  matrixmult(A,B,C,D)   -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (?,1)
          4.  transAcc0(A,B,C,D)    -> attach(-1 + A + D,B,C,-1 + D)                                      True                                   (?,1)
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                             True                                   (?,1)
          6.  transAcc(A,B,C,D)     -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B))                          [B >= 1]                               (?,1)
          7.  out1transAcc(A,B,C,D) -> out1transAcc(A,-1 + B,C,D)                                         [B >= 1]                               (?,1)
          8.  out2transAcc(A,B,C,D) -> out2transAcc(A,-1 + B,C,D)                                         [B >= 1]                               (?,1)
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                          [B >= 1]                               (?,1)
          10. makeBase(A,B,C,D)     -> mkBase(A,D,C,D)                                                    [B >= 1]                               (?,1)
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                               [B >= 1]                               (?,1)
          12. out1split(A,B,C,D)    -> out1split(A,-1 + B,C,D)                                            [B >= 1]                               (?,1)
          13. out2split(A,B,C,D)    -> out2split(A,-1 + B,C,D)                                            [B >= 1]                               (?,1)
          14. out3split(A,B,C,D)    -> out3split(A,-1 + B,C,D)                                            [B >= 1]                               (?,1)
          15. split(A,B,C,D)        -> split(A,-1 + B,C,D)                                                [B >= 1]                               (?,1)
          16. out1makeBase(A,B,C,D) -> outmkBase(A,D,C,D)                                                 [B = 0]                                (?,1)
          17. outmkBase(A,B,C,D)    -> outmkBase(A,-1 + B,C,D)                                            [B >= 1]                               (?,1)
          18. matrixmult3(A,B,C,D)  -> matrixmult(A,B,C,D)                                                True                                   (?,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                                  True                                   (?,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                          True                                   (?,1)
          21. matrixmultp(A,B,C,D)  -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                    [B >= 1]                               (?,1)
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                      True                                   (?,1)
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                             True                                   (?,1)
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                          [D >= 1]                               (?,1)
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                            [B >= 1 && D >= 1]                     (?,1)
          26. transpose(A,B,C,D)    -> split(A,B,C,D)                                                     [B >= 1 && D = 1]                      (?,1)
          27. transpose0(A,B,C,D)   -> split(A,B,C,D)                                                     True                                   (?,1)
          28. transpose1(A,B,C,D)   -> transpose(A,B,C,-1 + D)                                            True                                   (?,1)
          29. transpose(A,B,C,D)    -> c2(transpose0(A,B,C,D),transpose1(A,B,C,D))                        [B >= 1 && D >= 2]                     (?,1)
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                True                                   (1,1)
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},7->{7},8->{8},9->{9},10->{11},11->{11},12->{12}
          ,13->{13},14->{14},15->{15},16->{17},17->{17},18->{3},19->{24},20->{21},21->{19,20},22->{25},23->{24}
          ,24->{22,23},25->{25},26->{15},27->{15},28->{26,29},29->{27,28},30->{3}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  matrixmult0(A,B,C,D)  -> transAcc(B,B,0,D)                                                  True                                   (?,1)
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                           True                                   (?,1)
          2.  matrixmult2(A,B,C,D)  -> makeBase(A,B,C,D)                                                  True                                   (?,1)
          3.  matrixmult(A,B,C,D)   -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (?,1)
          4.  transAcc0(A,B,C,D)    -> attach(-1 + A + D,B,C,-1 + D)                                      True                                   (?,1)
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                             True                                   (?,1)
          6.  transAcc(A,B,C,D)     -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B))                          [B >= 1]                               (?,1)
          7.  out1transAcc(A,B,C,D) -> out1transAcc(A,-1 + B,C,D)                                         [B >= 1]                               (?,1)
          8.  out2transAcc(A,B,C,D) -> out2transAcc(A,-1 + B,C,D)                                         [B >= 1]                               (?,1)
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                          [B >= 1]                               (?,1)
          10. makeBase(A,B,C,D)     -> mkBase(A,D,C,D)                                                    [B >= 1]                               (?,1)
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                               [B >= 1]                               (?,1)
          12. out1split(A,B,C,D)    -> out1split(A,-1 + B,C,D)                                            [B >= 1]                               (?,1)
          13. out2split(A,B,C,D)    -> out2split(A,-1 + B,C,D)                                            [B >= 1]                               (?,1)
          14. out3split(A,B,C,D)    -> out3split(A,-1 + B,C,D)                                            [B >= 1]                               (?,1)
          15. split(A,B,C,D)        -> split(A,-1 + B,C,D)                                                [B >= 1]                               (?,1)
          16. out1makeBase(A,B,C,D) -> outmkBase(A,D,C,D)                                                 [B = 0]                                (1,1)
          17. outmkBase(A,B,C,D)    -> outmkBase(A,-1 + B,C,D)                                            [B >= 1]                               (?,1)
          18. matrixmult3(A,B,C,D)  -> matrixmult(A,B,C,D)                                                True                                   (1,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                                  True                                   (?,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                          True                                   (?,1)
          21. matrixmultp(A,B,C,D)  -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                    [B >= 1]                               (?,1)
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                      True                                   (?,1)
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                             True                                   (?,1)
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                          [D >= 1]                               (?,1)
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                            [B >= 1 && D >= 1]                     (?,1)
          26. transpose(A,B,C,D)    -> split(A,B,C,D)                                                     [B >= 1 && D = 1]                      (?,1)
          27. transpose0(A,B,C,D)   -> split(A,B,C,D)                                                     True                                   (?,1)
          28. transpose1(A,B,C,D)   -> transpose(A,B,C,-1 + D)                                            True                                   (?,1)
          29. transpose(A,B,C,D)    -> c2(transpose0(A,B,C,D),transpose1(A,B,C,D))                        [B >= 1 && D >= 2]                     (?,1)
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                True                                   (1,1)
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},7->{7},8->{8},9->{9},10->{11},11->{11},12->{12}
          ,13->{13},14->{14},15->{15},16->{17},17->{17},18->{3},19->{24},20->{21},21->{19,20},22->{25},23->{24}
          ,24->{22,23},25->{25},26->{15},27->{15},28->{26,29},29->{27,28},30->{3}]
        
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [7
                                                                                              ,8
                                                                                              ,12
                                                                                              ,13
                                                                                              ,14
                                                                                              ,15
                                                                                              ,16
                                                                                              ,17
                                                                                              ,18
                                                                                              ,26
                                                                                              ,27
                                                                                              ,28
                                                                                              ,29]
* Step 3: LocalSizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  matrixmult0(A,B,C,D)  -> transAcc(B,B,0,D)                                                  True                                   (?,1)
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                           True                                   (?,1)
          2.  matrixmult2(A,B,C,D)  -> makeBase(A,B,C,D)                                                  True                                   (?,1)
          3.  matrixmult(A,B,C,D)   -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (?,1)
          4.  transAcc0(A,B,C,D)    -> attach(-1 + A + D,B,C,-1 + D)                                      True                                   (?,1)
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                             True                                   (?,1)
          6.  transAcc(A,B,C,D)     -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B))                          [B >= 1]                               (?,1)
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                          [B >= 1]                               (?,1)
          10. makeBase(A,B,C,D)     -> mkBase(A,D,C,D)                                                    [B >= 1]                               (?,1)
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                               [B >= 1]                               (?,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                                  True                                   (?,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                          True                                   (?,1)
          21. matrixmultp(A,B,C,D)  -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                    [B >= 1]                               (?,1)
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                      True                                   (?,1)
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                             True                                   (?,1)
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                          [D >= 1]                               (?,1)
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                            [B >= 1 && D >= 1]                     (?,1)
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                True                                   (1,1)
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},9->{9},10->{11},11->{11},19->{24},20->{21}
          ,21->{19,20},22->{25},23->{24},24->{22,23},25->{25},30->{3}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (< 0,0,A>,         B, .= 0) (< 0,0,B>,     B, .= 0) (< 0,0,C>,     0, .= 0) (< 0,0,D>,     D, .= 0) 
          (< 1,0,A>,         B, .= 0) (< 1,0,B>,     A, .= 0) (< 1,0,C>, A + D, .* 0) (< 1,0,D>,     C, .= 0) 
          (< 2,0,A>,         A, .= 0) (< 2,0,B>,     B, .= 0) (< 2,0,C>,     C, .= 0) (< 2,0,D>,     D, .= 0) 
          (< 3,0,A>,         B, .= 0) (< 3,0,B>,     A, .= 0) (< 3,0,C>,     D, .= 0) (< 3,0,D>,     C, .= 0) 
          (< 3,1,A>,         B, .= 0) (< 3,1,B>,     A, .= 0) (< 3,1,C>,     D, .= 0) (< 3,1,D>,     C, .= 0) 
          (< 3,2,A>,         B, .= 0) (< 3,2,B>,     A, .= 0) (< 3,2,C>,     D, .= 0) (< 3,2,D>,     C, .= 0) 
          (< 4,0,A>, 1 + A + D, .* 1) (< 4,0,B>,     B, .= 0) (< 4,0,C>,     C, .= 0) (< 4,0,D>, 1 + D, .+ 1) 
          (< 5,0,A>,         C, .= 0) (< 5,0,B>, 1 + D, .+ 1) (< 5,0,C>,     A, .= 0) (< 5,0,D>,     B, .= 0) 
          (< 6,0,A>,         C, .= 0) (< 6,0,B>,     D, .= 0) (< 6,0,C>,     A, .= 0) (< 6,0,D>,     B, .= 0) 
          (< 6,1,A>,         C, .= 0) (< 6,1,B>,     D, .= 0) (< 6,1,C>,     A, .= 0) (< 6,1,D>,     B, .= 0) 
          (< 9,0,A>,         A, .= 0) (< 9,0,B>, 1 + B, .+ 1) (< 9,0,C>,     C, .= 0) (< 9,0,D>, 1 + D, .+ 1) 
          (<10,0,A>,         A, .= 0) (<10,0,B>,     D, .= 0) (<10,0,C>,     C, .= 0) (<10,0,D>,     D, .= 0) 
          (<11,0,A>,         A, .= 0) (<11,0,B>, 1 + B, .+ 1) (<11,0,C>,     C, .= 0) (<11,0,D>,     D, .= 0) 
          (<19,0,A>,         A, .= 0) (<19,0,B>,     B, .= 0) (<19,0,C>,     C, .= 0) (<19,0,D>,     D, .= 0) 
          (<20,0,A>,         D, .= 0) (<20,0,B>, 1 + C, .+ 1) (<20,0,C>,     A, .= 0) (<20,0,D>,     B, .= 0) 
          (<21,0,A>,         C, .= 0) (<21,0,B>,     D, .= 0) (<21,0,C>,     B, .= 0) (<21,0,D>,     A, .= 0) 
          (<21,1,A>,         C, .= 0) (<21,1,B>,     D, .= 0) (<21,1,C>,     B, .= 0) (<21,1,D>,     A, .= 0) 
          (<22,0,A>,         A, .= 0) (<22,0,B>,     B, .= 0) (<22,0,C>,     C, .= 0) (<22,0,D>,     D, .= 0) 
          (<23,0,A>,         D, .= 0) (<23,0,B>,     B, .= 0) (<23,0,C>,     C, .= 0) (<23,0,D>, 1 + A, .+ 1) 
          (<24,0,A>,         D, .= 0) (<24,0,B>,     B, .= 0) (<24,0,C>,     C, .= 0) (<24,0,D>,     A, .= 0) 
          (<24,1,A>,         D, .= 0) (<24,1,B>,     B, .= 0) (<24,1,C>,     C, .= 0) (<24,1,D>,     A, .= 0) 
          (<25,0,A>,         A, .= 0) (<25,0,B>, 1 + B, .+ 1) (<25,0,C>,     C, .= 0) (<25,0,D>, 1 + D, .+ 1) 
          (<30,0,A>,         A, .= 0) (<30,0,B>,     B, .= 0) (<30,0,C>,     C, .= 0) (<30,0,D>,     D, .= 0) 
* Step 4: SizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  matrixmult0(A,B,C,D)  -> transAcc(B,B,0,D)                                                  True                                   (?,1)
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                           True                                   (?,1)
          2.  matrixmult2(A,B,C,D)  -> makeBase(A,B,C,D)                                                  True                                   (?,1)
          3.  matrixmult(A,B,C,D)   -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (?,1)
          4.  transAcc0(A,B,C,D)    -> attach(-1 + A + D,B,C,-1 + D)                                      True                                   (?,1)
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                             True                                   (?,1)
          6.  transAcc(A,B,C,D)     -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B))                          [B >= 1]                               (?,1)
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                          [B >= 1]                               (?,1)
          10. makeBase(A,B,C,D)     -> mkBase(A,D,C,D)                                                    [B >= 1]                               (?,1)
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                               [B >= 1]                               (?,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                                  True                                   (?,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                          True                                   (?,1)
          21. matrixmultp(A,B,C,D)  -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                    [B >= 1]                               (?,1)
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                      True                                   (?,1)
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                             True                                   (?,1)
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                          [D >= 1]                               (?,1)
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                            [B >= 1 && D >= 1]                     (?,1)
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                True                                   (1,1)
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},9->{9},10->{11},11->{11},19->{24},20->{21}
          ,21->{19,20},22->{25},23->{24},24->{22,23},25->{25},30->{3}]
        Sizebounds:
          (< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) 
          (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) 
          (< 3,1,A>, ?) (< 3,1,B>, ?) (< 3,1,C>, ?) (< 3,1,D>, ?) 
          (< 3,2,A>, ?) (< 3,2,B>, ?) (< 3,2,C>, ?) (< 3,2,D>, ?) 
          (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) 
          (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) 
          (< 6,1,A>, ?) (< 6,1,B>, ?) (< 6,1,C>, ?) (< 6,1,D>, ?) 
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) 
          (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) 
          (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) 
          (<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) 
          (<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?) 
          (<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?) 
          (<21,1,A>, ?) (<21,1,B>, ?) (<21,1,C>, ?) (<21,1,D>, ?) 
          (<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?) (<22,0,D>, ?) 
          (<23,0,A>, ?) (<23,0,B>, ?) (<23,0,C>, ?) (<23,0,D>, ?) 
          (<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?) (<24,0,D>, ?) 
          (<24,1,A>, ?) (<24,1,B>, ?) (<24,1,C>, ?) (<24,1,D>, ?) 
          (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) 
          (<30,0,A>, ?) (<30,0,B>, ?) (<30,0,C>, ?) (<30,0,D>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (< 0,0,A>,     A) (< 0,0,B>, A) (< 0,0,C>,     0) (< 0,0,D>,     C) 
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 2,0,A>,     B) (< 2,0,B>, A) (< 2,0,C>,     D) (< 2,0,D>,     C) 
          (< 3,0,A>,     B) (< 3,0,B>, A) (< 3,0,C>,     D) (< 3,0,D>,     C) 
          (< 3,1,A>,     B) (< 3,1,B>, A) (< 3,1,C>,     D) (< 3,1,D>,     C) 
          (< 3,2,A>,     B) (< 3,2,B>, A) (< 3,2,C>,     D) (< 3,2,D>,     C) 
          (< 4,0,A>,     ?) (< 4,0,B>, C) (< 4,0,C>,     A) (< 4,0,D>,     ?) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 6,0,A>,     0) (< 6,0,B>, C) (< 6,0,C>,     A) (< 6,0,D>,     ?) 
          (< 6,1,A>,     0) (< 6,1,B>, C) (< 6,1,C>,     A) (< 6,1,D>,     ?) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<10,0,A>,     B) (<10,0,B>, C) (<10,0,C>,     D) (<10,0,D>,     C) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>,     ?) (<19,0,D>,     A) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>,     ?) (<21,0,D>,     A) 
          (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>,     ?) (<21,1,D>,     A) 
          (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<24,0,A>,     ?) (<24,0,B>, D) (<24,0,C>,     ?) (<24,0,D>, B + C) 
          (<24,1,A>,     ?) (<24,1,B>, D) (<24,1,C>,     ?) (<24,1,D>, B + C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
* Step 5: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  matrixmult0(A,B,C,D)  -> transAcc(B,B,0,D)                                                  True                                   (?,1)
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                           True                                   (?,1)
          2.  matrixmult2(A,B,C,D)  -> makeBase(A,B,C,D)                                                  True                                   (?,1)
          3.  matrixmult(A,B,C,D)   -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (?,1)
          4.  transAcc0(A,B,C,D)    -> attach(-1 + A + D,B,C,-1 + D)                                      True                                   (?,1)
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                             True                                   (?,1)
          6.  transAcc(A,B,C,D)     -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B))                          [B >= 1]                               (?,1)
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                          [B >= 1]                               (?,1)
          10. makeBase(A,B,C,D)     -> mkBase(A,D,C,D)                                                    [B >= 1]                               (?,1)
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                               [B >= 1]                               (?,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                                  True                                   (?,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                          True                                   (?,1)
          21. matrixmultp(A,B,C,D)  -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                    [B >= 1]                               (?,1)
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                      True                                   (?,1)
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                             True                                   (?,1)
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                          [D >= 1]                               (?,1)
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                            [B >= 1 && D >= 1]                     (?,1)
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                True                                   (1,1)
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},9->{9},10->{11},11->{11},19->{24},20->{21}
          ,21->{19,20},22->{25},23->{24},24->{22,23},25->{25},30->{3}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>, A) (< 0,0,C>,     0) (< 0,0,D>,     C) 
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 2,0,A>,     B) (< 2,0,B>, A) (< 2,0,C>,     D) (< 2,0,D>,     C) 
          (< 3,0,A>,     B) (< 3,0,B>, A) (< 3,0,C>,     D) (< 3,0,D>,     C) 
          (< 3,1,A>,     B) (< 3,1,B>, A) (< 3,1,C>,     D) (< 3,1,D>,     C) 
          (< 3,2,A>,     B) (< 3,2,B>, A) (< 3,2,C>,     D) (< 3,2,D>,     C) 
          (< 4,0,A>,     ?) (< 4,0,B>, C) (< 4,0,C>,     A) (< 4,0,D>,     ?) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 6,0,A>,     0) (< 6,0,B>, C) (< 6,0,C>,     A) (< 6,0,D>,     ?) 
          (< 6,1,A>,     0) (< 6,1,B>, C) (< 6,1,C>,     A) (< 6,1,D>,     ?) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<10,0,A>,     B) (<10,0,B>, C) (<10,0,C>,     D) (<10,0,D>,     C) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>,     ?) (<19,0,D>,     A) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>,     ?) (<21,0,D>,     A) 
          (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>,     ?) (<21,1,D>,     A) 
          (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<24,0,A>,     ?) (<24,0,B>, D) (<24,0,C>,     ?) (<24,0,D>, B + C) 
          (<24,1,A>,     ?) (<24,1,B>, D) (<24,1,C>,     ?) (<24,1,D>, B + C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
                p(attach) = 0
              p(linemult) = 0
             p(linemult0) = 0
             p(linemult1) = 0
              p(makeBase) = 1
            p(matrixmult) = 2
           p(matrixmult0) = 0
           p(matrixmult1) = 1
           p(matrixmult2) = 1
           p(matrixmultp) = 1
          p(matrixmultp0) = 0
          p(matrixmultp1) = 1
                p(mkBase) = 0
                  p(mult) = 0
                 p(start) = 2
              p(transAcc) = 0
             p(transAcc0) = 0
             p(transAcc1) = 0
        
        The following rules are strictly oriented:
                   [B >= 1] ==>                
          makeBase(A,B,C,D)   = 1              
                              > 0              
                              = mkBase(A,D,C,D)
        
        
        The following rules are weakly oriented:
                                          True ==>                                                                   
                          matrixmult0(A,B,C,D)   = 0                                                                 
                                                >= 0                                                                 
                                                 = transAcc(B,B,0,D)                                                 
        
                                          True ==>                                                                   
                          matrixmult1(A,B,C,D)   = 1                                                                 
                                                >= 1                                                                 
                                                 = matrixmultp(B,A,A + D,C)                                          
        
                                          True ==>                                                                   
                          matrixmult2(A,B,C,D)   = 1                                                                 
                                                >= 1                                                                 
                                                 = makeBase(A,B,C,D)                                                 
        
        [B >= 0 && D >= 0 && A >= 0 && C >= 0] ==>                                                                   
                           matrixmult(A,B,C,D)   = 2                                                                 
                                                >= 2                                                                 
                                                 = c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C))
        
                                          True ==>                                                                   
                            transAcc0(A,B,C,D)   = 0                                                                 
                                                >= 0                                                                 
                                                 = attach(-1 + A + D,B,C,-1 + D)                                     
        
                                          True ==>                                                                   
                            transAcc1(A,B,C,D)   = 0                                                                 
                                                >= 0                                                                 
                                                 = transAcc(C,-1 + D,A,B)                                            
        
                                      [B >= 1] ==>                                                                   
                             transAcc(A,B,C,D)   = 0                                                                 
                                                >= 0                                                                 
                                                 = c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B))                         
        
                                      [B >= 1] ==>                                                                   
                               attach(A,B,C,D)   = 0                                                                 
                                                >= 0                                                                 
                                                 = attach(A,-1 + B,C,-1 + D)                                         
        
                                      [B >= 1] ==>                                                                   
                               mkBase(A,B,C,D)   = 0                                                                 
                                                >= 0                                                                 
                                                 = mkBase(A,-1 + B,C,D)                                              
        
                                          True ==>                                                                   
                         matrixmultp0(A,B,C,D)   = 0                                                                 
                                                >= 0                                                                 
                                                 = linemult(A,B,C,D)                                                 
        
                                          True ==>                                                                   
                         matrixmultp1(A,B,C,D)   = 1                                                                 
                                                >= 1                                                                 
                                                 = matrixmultp(D,-1 + C,A,B)                                         
        
                                      [B >= 1] ==>                                                                   
                          matrixmultp(A,B,C,D)   = 1                                                                 
                                                >= 1                                                                 
                                                 = c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                   
        
                                          True ==>                                                                   
                            linemult0(A,B,C,D)   = 0                                                                 
                                                >= 0                                                                 
                                                 = mult(A,B,C,D)                                                     
        
                                          True ==>                                                                   
                            linemult1(A,B,C,D)   = 0                                                                 
                                                >= 0                                                                 
                                                 = linemult(D,B,C,-1 + A)                                            
        
                                      [D >= 1] ==>                                                                   
                             linemult(A,B,C,D)   = 0                                                                 
                                                >= 0                                                                 
                                                 = c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                         
        
                            [B >= 1 && D >= 1] ==>                                                                   
                                 mult(A,B,C,D)   = 0                                                                 
                                                >= 0                                                                 
                                                 = mult(A,-1 + B,C,-1 + D)                                           
        
                                          True ==>                                                                   
                                start(A,B,C,D)   = 2                                                                 
                                                >= 2                                                                 
                                                 = matrixmult(A,B,C,D)                                               
        
        
* Step 6: KnowledgePropagation WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  matrixmult0(A,B,C,D)  -> transAcc(B,B,0,D)                                                  True                                   (?,1)
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                           True                                   (?,1)
          2.  matrixmult2(A,B,C,D)  -> makeBase(A,B,C,D)                                                  True                                   (?,1)
          3.  matrixmult(A,B,C,D)   -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (?,1)
          4.  transAcc0(A,B,C,D)    -> attach(-1 + A + D,B,C,-1 + D)                                      True                                   (?,1)
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                             True                                   (?,1)
          6.  transAcc(A,B,C,D)     -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B))                          [B >= 1]                               (?,1)
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                          [B >= 1]                               (?,1)
          10. makeBase(A,B,C,D)     -> mkBase(A,D,C,D)                                                    [B >= 1]                               (2,1)
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                               [B >= 1]                               (?,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                                  True                                   (?,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                          True                                   (?,1)
          21. matrixmultp(A,B,C,D)  -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                    [B >= 1]                               (?,1)
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                      True                                   (?,1)
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                             True                                   (?,1)
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                          [D >= 1]                               (?,1)
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                            [B >= 1 && D >= 1]                     (?,1)
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                True                                   (1,1)
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},9->{9},10->{11},11->{11},19->{24},20->{21}
          ,21->{19,20},22->{25},23->{24},24->{22,23},25->{25},30->{3}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>, A) (< 0,0,C>,     0) (< 0,0,D>,     C) 
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 2,0,A>,     B) (< 2,0,B>, A) (< 2,0,C>,     D) (< 2,0,D>,     C) 
          (< 3,0,A>,     B) (< 3,0,B>, A) (< 3,0,C>,     D) (< 3,0,D>,     C) 
          (< 3,1,A>,     B) (< 3,1,B>, A) (< 3,1,C>,     D) (< 3,1,D>,     C) 
          (< 3,2,A>,     B) (< 3,2,B>, A) (< 3,2,C>,     D) (< 3,2,D>,     C) 
          (< 4,0,A>,     ?) (< 4,0,B>, C) (< 4,0,C>,     A) (< 4,0,D>,     ?) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 6,0,A>,     0) (< 6,0,B>, C) (< 6,0,C>,     A) (< 6,0,D>,     ?) 
          (< 6,1,A>,     0) (< 6,1,B>, C) (< 6,1,C>,     A) (< 6,1,D>,     ?) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<10,0,A>,     B) (<10,0,B>, C) (<10,0,C>,     D) (<10,0,D>,     C) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>,     ?) (<19,0,D>,     A) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>,     ?) (<21,0,D>,     A) 
          (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>,     ?) (<21,1,D>,     A) 
          (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<24,0,A>,     ?) (<24,0,B>, D) (<24,0,C>,     ?) (<24,0,D>, B + C) 
          (<24,1,A>,     ?) (<24,1,B>, D) (<24,1,C>,     ?) (<24,1,D>, B + C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 7: PolyRank WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  matrixmult0(A,B,C,D)  -> transAcc(B,B,0,D)                                                  True                                   (1,1)
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                           True                                   (1,1)
          2.  matrixmult2(A,B,C,D)  -> makeBase(A,B,C,D)                                                  True                                   (1,1)
          3.  matrixmult(A,B,C,D)   -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,1)
          4.  transAcc0(A,B,C,D)    -> attach(-1 + A + D,B,C,-1 + D)                                      True                                   (?,1)
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                             True                                   (?,1)
          6.  transAcc(A,B,C,D)     -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B))                          [B >= 1]                               (?,1)
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                          [B >= 1]                               (?,1)
          10. makeBase(A,B,C,D)     -> mkBase(A,D,C,D)                                                    [B >= 1]                               (2,1)
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                               [B >= 1]                               (?,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                                  True                                   (?,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                          True                                   (?,1)
          21. matrixmultp(A,B,C,D)  -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                    [B >= 1]                               (?,1)
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                      True                                   (?,1)
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                             True                                   (?,1)
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                          [D >= 1]                               (?,1)
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                            [B >= 1 && D >= 1]                     (?,1)
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                True                                   (1,1)
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},9->{9},10->{11},11->{11},19->{24},20->{21}
          ,21->{19,20},22->{25},23->{24},24->{22,23},25->{25},30->{3}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>, A) (< 0,0,C>,     0) (< 0,0,D>,     C) 
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 2,0,A>,     B) (< 2,0,B>, A) (< 2,0,C>,     D) (< 2,0,D>,     C) 
          (< 3,0,A>,     B) (< 3,0,B>, A) (< 3,0,C>,     D) (< 3,0,D>,     C) 
          (< 3,1,A>,     B) (< 3,1,B>, A) (< 3,1,C>,     D) (< 3,1,D>,     C) 
          (< 3,2,A>,     B) (< 3,2,B>, A) (< 3,2,C>,     D) (< 3,2,D>,     C) 
          (< 4,0,A>,     ?) (< 4,0,B>, C) (< 4,0,C>,     A) (< 4,0,D>,     ?) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 6,0,A>,     0) (< 6,0,B>, C) (< 6,0,C>,     A) (< 6,0,D>,     ?) 
          (< 6,1,A>,     0) (< 6,1,B>, C) (< 6,1,C>,     A) (< 6,1,D>,     ?) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<10,0,A>,     B) (<10,0,B>, C) (<10,0,C>,     D) (<10,0,D>,     C) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>,     ?) (<19,0,D>,     A) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>,     ?) (<21,0,D>,     A) 
          (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>,     ?) (<21,1,D>,     A) 
          (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<24,0,A>,     ?) (<24,0,B>, D) (<24,0,C>,     ?) (<24,0,D>, B + C) 
          (<24,1,A>,     ?) (<24,1,B>, D) (<24,1,C>,     ?) (<24,1,D>, B + C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [11], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(mkBase) = x2
        
        The following rules are strictly oriented:
                 [B >= 1] ==>                     
          mkBase(A,B,C,D)   = B                   
                            > -1 + B              
                            = mkBase(A,-1 + B,C,D)
        
        
        The following rules are weakly oriented:
        
        We use the following global sizebounds:
        (< 0,0,A>,     A) (< 0,0,B>, A) (< 0,0,C>,     0) (< 0,0,D>,     C) 
        (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
        (< 2,0,A>,     B) (< 2,0,B>, A) (< 2,0,C>,     D) (< 2,0,D>,     C) 
        (< 3,0,A>,     B) (< 3,0,B>, A) (< 3,0,C>,     D) (< 3,0,D>,     C) 
        (< 3,1,A>,     B) (< 3,1,B>, A) (< 3,1,C>,     D) (< 3,1,D>,     C) 
        (< 3,2,A>,     B) (< 3,2,B>, A) (< 3,2,C>,     D) (< 3,2,D>,     C) 
        (< 4,0,A>,     ?) (< 4,0,B>, C) (< 4,0,C>,     A) (< 4,0,D>,     ?) 
        (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
        (< 6,0,A>,     0) (< 6,0,B>, C) (< 6,0,C>,     A) (< 6,0,D>,     ?) 
        (< 6,1,A>,     0) (< 6,1,B>, C) (< 6,1,C>,     A) (< 6,1,D>,     ?) 
        (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
        (<10,0,A>,     B) (<10,0,B>, C) (<10,0,C>,     D) (<10,0,D>,     C) 
        (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
        (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>,     ?) (<19,0,D>,     A) 
        (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
        (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>,     ?) (<21,0,D>,     A) 
        (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>,     ?) (<21,1,D>,     A) 
        (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
        (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
        (<24,0,A>,     ?) (<24,0,B>, D) (<24,0,C>,     ?) (<24,0,D>, B + C) 
        (<24,1,A>,     ?) (<24,1,B>, D) (<24,1,C>,     ?) (<24,1,D>, B + C) 
        (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
        (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
* Step 8: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  matrixmult0(A,B,C,D)  -> transAcc(B,B,0,D)                                                  True                                   (1,1)  
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                           True                                   (1,1)  
          2.  matrixmult2(A,B,C,D)  -> makeBase(A,B,C,D)                                                  True                                   (1,1)  
          3.  matrixmult(A,B,C,D)   -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,1)  
          4.  transAcc0(A,B,C,D)    -> attach(-1 + A + D,B,C,-1 + D)                                      True                                   (?,1)  
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                             True                                   (?,1)  
          6.  transAcc(A,B,C,D)     -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B))                          [B >= 1]                               (?,1)  
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                          [B >= 1]                               (?,1)  
          10. makeBase(A,B,C,D)     -> mkBase(A,D,C,D)                                                    [B >= 1]                               (2,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                               [B >= 1]                               (2*C,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                                  True                                   (?,1)  
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                          True                                   (?,1)  
          21. matrixmultp(A,B,C,D)  -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                    [B >= 1]                               (?,1)  
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                      True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                             True                                   (?,1)  
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                          [D >= 1]                               (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                            [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                True                                   (1,1)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},9->{9},10->{11},11->{11},19->{24},20->{21}
          ,21->{19,20},22->{25},23->{24},24->{22,23},25->{25},30->{3}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>, A) (< 0,0,C>,     0) (< 0,0,D>,     C) 
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 2,0,A>,     B) (< 2,0,B>, A) (< 2,0,C>,     D) (< 2,0,D>,     C) 
          (< 3,0,A>,     B) (< 3,0,B>, A) (< 3,0,C>,     D) (< 3,0,D>,     C) 
          (< 3,1,A>,     B) (< 3,1,B>, A) (< 3,1,C>,     D) (< 3,1,D>,     C) 
          (< 3,2,A>,     B) (< 3,2,B>, A) (< 3,2,C>,     D) (< 3,2,D>,     C) 
          (< 4,0,A>,     ?) (< 4,0,B>, C) (< 4,0,C>,     A) (< 4,0,D>,     ?) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 6,0,A>,     0) (< 6,0,B>, C) (< 6,0,C>,     A) (< 6,0,D>,     ?) 
          (< 6,1,A>,     0) (< 6,1,B>, C) (< 6,1,C>,     A) (< 6,1,D>,     ?) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<10,0,A>,     B) (<10,0,B>, C) (<10,0,C>,     D) (<10,0,D>,     C) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>,     ?) (<19,0,D>,     A) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>,     ?) (<21,0,D>,     A) 
          (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>,     ?) (<21,1,D>,     A) 
          (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<24,0,A>,     ?) (<24,0,B>, D) (<24,0,C>,     ?) (<24,0,D>, B + C) 
          (<24,1,A>,     ?) (<24,1,B>, D) (<24,1,C>,     ?) (<24,1,D>, B + C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
    + Applied Processor:
        ChainProcessor False [0,1,2,3,4,5,6,9,10,11,19,20,21,22,23,24,25,30]
    + Details:
        We chained rule 2 to obtain the rules [31] .
* Step 9: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  matrixmult0(A,B,C,D)  -> transAcc(B,B,0,D)                                                  True                                   (1,1)  
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                           True                                   (1,1)  
          3.  matrixmult(A,B,C,D)   -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,1)  
          4.  transAcc0(A,B,C,D)    -> attach(-1 + A + D,B,C,-1 + D)                                      True                                   (?,1)  
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                             True                                   (?,1)  
          6.  transAcc(A,B,C,D)     -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B))                          [B >= 1]                               (?,1)  
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                          [B >= 1]                               (?,1)  
          10. makeBase(A,B,C,D)     -> mkBase(A,D,C,D)                                                    [B >= 1]                               (2,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                               [B >= 1]                               (2*C,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                                  True                                   (?,1)  
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                          True                                   (?,1)  
          21. matrixmultp(A,B,C,D)  -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                    [B >= 1]                               (?,1)  
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                      True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                             True                                   (?,1)  
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                          [D >= 1]                               (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                            [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                    [B >= 1]                               (1,2)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [0->{6},1->{21},3->{0,1,31},4->{9},5->{6},6->{4,5},9->{9},10->{11},11->{11},19->{24},20->{21},21->{19,20}
          ,22->{25},23->{24},24->{22,23},25->{25},30->{3},31->{11}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>, A) (< 0,0,C>,     0) (< 0,0,D>,     C) 
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 3,0,A>,     B) (< 3,0,B>, A) (< 3,0,C>,     D) (< 3,0,D>,     C) 
          (< 3,1,A>,     B) (< 3,1,B>, A) (< 3,1,C>,     D) (< 3,1,D>,     C) 
          (< 3,2,A>,     B) (< 3,2,B>, A) (< 3,2,C>,     D) (< 3,2,D>,     C) 
          (< 4,0,A>,     ?) (< 4,0,B>, C) (< 4,0,C>,     A) (< 4,0,D>,     ?) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 6,0,A>,     0) (< 6,0,B>, C) (< 6,0,C>,     A) (< 6,0,D>,     ?) 
          (< 6,1,A>,     0) (< 6,1,B>, C) (< 6,1,C>,     A) (< 6,1,D>,     ?) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<10,0,A>,     B) (<10,0,B>, C) (<10,0,C>,     D) (<10,0,D>,     C) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>,     ?) (<19,0,D>,     A) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>,     ?) (<21,0,D>,     A) 
          (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>,     ?) (<21,1,D>,     A) 
          (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<24,0,A>,     ?) (<24,0,B>, D) (<24,0,C>,     ?) (<24,0,D>, B + C) 
          (<24,1,A>,     ?) (<24,1,B>, D) (<24,1,C>,     ?) (<24,1,D>, B + C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [10]
* Step 10: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  matrixmult0(A,B,C,D)  -> transAcc(B,B,0,D)                                                  True                                   (1,1)  
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                           True                                   (1,1)  
          3.  matrixmult(A,B,C,D)   -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,1)  
          4.  transAcc0(A,B,C,D)    -> attach(-1 + A + D,B,C,-1 + D)                                      True                                   (?,1)  
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                             True                                   (?,1)  
          6.  transAcc(A,B,C,D)     -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B))                          [B >= 1]                               (?,1)  
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                          [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                               [B >= 1]                               (2*C,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                                  True                                   (?,1)  
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                          True                                   (?,1)  
          21. matrixmultp(A,B,C,D)  -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                    [B >= 1]                               (?,1)  
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                      True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                             True                                   (?,1)  
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                          [D >= 1]                               (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                            [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                    [B >= 1]                               (1,2)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [0->{6},1->{21},3->{0,1,31},4->{9},5->{6},6->{4,5},9->{9},11->{11},19->{24},20->{21},21->{19,20},22->{25}
          ,23->{24},24->{22,23},25->{25},30->{3},31->{11}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>, A) (< 0,0,C>,     0) (< 0,0,D>,     C) 
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 3,0,A>,     B) (< 3,0,B>, A) (< 3,0,C>,     D) (< 3,0,D>,     C) 
          (< 3,1,A>,     B) (< 3,1,B>, A) (< 3,1,C>,     D) (< 3,1,D>,     C) 
          (< 3,2,A>,     B) (< 3,2,B>, A) (< 3,2,C>,     D) (< 3,2,D>,     C) 
          (< 4,0,A>,     ?) (< 4,0,B>, C) (< 4,0,C>,     A) (< 4,0,D>,     ?) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 6,0,A>,     0) (< 6,0,B>, C) (< 6,0,C>,     A) (< 6,0,D>,     ?) 
          (< 6,1,A>,     0) (< 6,1,B>, C) (< 6,1,C>,     A) (< 6,1,D>,     ?) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>,     ?) (<19,0,D>,     A) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>,     ?) (<21,0,D>,     A) 
          (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>,     ?) (<21,1,D>,     A) 
          (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<24,0,A>,     ?) (<24,0,B>, D) (<24,0,C>,     ?) (<24,0,D>, B + C) 
          (<24,1,A>,     ?) (<24,1,B>, D) (<24,1,C>,     ?) (<24,1,D>, B + C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
    + Applied Processor:
        ChainProcessor False [0,1,3,4,5,6,9,11,19,20,21,22,23,24,25,30,31]
    + Details:
        We chained rule 3 to obtain the rules [32] .
* Step 11: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          0.  matrixmult0(A,B,C,D)  -> transAcc(B,B,0,D)                                               True                                   (1,1)  
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                        True                                   (1,1)  
          4.  transAcc0(A,B,C,D)    -> attach(-1 + A + D,B,C,-1 + D)                                   True                                   (?,1)  
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                          True                                   (?,1)  
          6.  transAcc(A,B,C,D)     -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B))                       [B >= 1]                               (?,1)  
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                       [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                            [B >= 1]                               (2*C,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                               True                                   (?,1)  
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                       True                                   (?,1)  
          21. matrixmultp(A,B,C,D)  -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                 [B >= 1]                               (?,1)  
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                   True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                          True                                   (?,1)  
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                       [D >= 1]                               (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                         [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                             True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                 [B >= 1]                               (1,2)  
          32. matrixmult(A,B,C,D)   -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [0->{6},1->{21},4->{9},5->{6},6->{4,5},9->{9},11->{11},19->{24},20->{21},21->{19,20},22->{25},23->{24}
          ,24->{22,23},25->{25},30->{32},31->{11},32->{1,6,31}]
        Sizebounds:
          (< 0,0,A>,     A) (< 0,0,B>, A) (< 0,0,C>,     0) (< 0,0,D>,     C) 
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 4,0,A>,     ?) (< 4,0,B>, C) (< 4,0,C>,     A) (< 4,0,D>,     ?) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 6,0,A>,     0) (< 6,0,B>, C) (< 6,0,C>,     A) (< 6,0,D>,     ?) 
          (< 6,1,A>,     0) (< 6,1,B>, C) (< 6,1,C>,     A) (< 6,1,D>,     ?) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>,     ?) (<19,0,D>,     A) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>,     ?) (<21,0,D>,     A) 
          (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>,     ?) (<21,1,D>,     A) 
          (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<24,0,A>,     ?) (<24,0,B>, D) (<24,0,C>,     ?) (<24,0,D>, B + C) 
          (<24,1,A>,     ?) (<24,1,B>, D) (<24,1,C>,     ?) (<24,1,D>, B + C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
          (<32,0,A>,     A) (<32,0,B>, A) (<32,0,C>,     0) (<32,0,D>,     C) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [0]
* Step 12: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                        True                                   (1,1)  
          4.  transAcc0(A,B,C,D)    -> attach(-1 + A + D,B,C,-1 + D)                                   True                                   (?,1)  
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                          True                                   (?,1)  
          6.  transAcc(A,B,C,D)     -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B))                       [B >= 1]                               (?,1)  
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                       [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                            [B >= 1]                               (2*C,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                               True                                   (?,1)  
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                       True                                   (?,1)  
          21. matrixmultp(A,B,C,D)  -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                 [B >= 1]                               (?,1)  
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                   True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                          True                                   (?,1)  
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                       [D >= 1]                               (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                         [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                             True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                 [B >= 1]                               (1,2)  
          32. matrixmult(A,B,C,D)   -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [1->{21},4->{9},5->{6},6->{4,5},9->{9},11->{11},19->{24},20->{21},21->{19,20},22->{25},23->{24},24->{22
          ,23},25->{25},30->{32},31->{11},32->{1,6,31}]
        Sizebounds:
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 4,0,A>,     ?) (< 4,0,B>, C) (< 4,0,C>,     A) (< 4,0,D>,     ?) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 6,0,A>,     0) (< 6,0,B>, C) (< 6,0,C>,     A) (< 6,0,D>,     ?) 
          (< 6,1,A>,     0) (< 6,1,B>, C) (< 6,1,C>,     A) (< 6,1,D>,     ?) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>,     ?) (<19,0,D>,     A) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>,     ?) (<21,0,D>,     A) 
          (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>,     ?) (<21,1,D>,     A) 
          (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<24,0,A>,     ?) (<24,0,B>, D) (<24,0,C>,     ?) (<24,0,D>, B + C) 
          (<24,1,A>,     ?) (<24,1,B>, D) (<24,1,C>,     ?) (<24,1,D>, B + C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
          (<32,0,A>,     A) (<32,0,B>, A) (<32,0,C>,     0) (<32,0,D>,     C) 
    + Applied Processor:
        ChainProcessor False [1,4,5,6,9,11,19,20,21,22,23,24,25,30,31,32]
    + Details:
        We chained rule 6 to obtain the rules [33] .
* Step 13: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                        True                                   (1,1)  
          4.  transAcc0(A,B,C,D)    -> attach(-1 + A + D,B,C,-1 + D)                                   True                                   (?,1)  
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                          True                                   (?,1)  
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                       [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                            [B >= 1]                               (2*C,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                               True                                   (?,1)  
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                       True                                   (?,1)  
          21. matrixmultp(A,B,C,D)  -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                 [B >= 1]                               (?,1)  
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                   True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                          True                                   (?,1)  
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                       [D >= 1]                               (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                         [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                             True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                 [B >= 1]                               (1,2)  
          32. matrixmult(A,B,C,D)   -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2)  
          33. transAcc(A,B,C,D)     -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B))            [B >= 1]                               (?,2)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [1->{21},4->{9},5->{33},9->{9},11->{11},19->{24},20->{21},21->{19,20},22->{25},23->{24},24->{22,23}
          ,25->{25},30->{32},31->{11},32->{1,31,33},33->{5,9}]
        Sizebounds:
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 4,0,A>,     ?) (< 4,0,B>, C) (< 4,0,C>,     A) (< 4,0,D>,     ?) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>,     ?) (<19,0,D>,     A) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>,     ?) (<21,0,D>,     A) 
          (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>,     ?) (<21,1,D>,     A) 
          (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<24,0,A>,     ?) (<24,0,B>, D) (<24,0,C>,     ?) (<24,0,D>, B + C) 
          (<24,1,A>,     ?) (<24,1,B>, D) (<24,1,C>,     ?) (<24,1,D>, B + C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
          (<32,0,A>,     A) (<32,0,B>, A) (<32,0,C>,     0) (<32,0,D>,     C) 
          (<33,0,A>,     ?) (<33,0,B>, C) (<33,0,C>,     A) (<33,0,D>,     ?) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [4]
* Step 14: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                        True                                   (1,1)  
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                          True                                   (?,1)  
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                       [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                            [B >= 1]                               (2*C,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                               True                                   (?,1)  
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                       True                                   (?,1)  
          21. matrixmultp(A,B,C,D)  -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A))                 [B >= 1]                               (?,1)  
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                   True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                          True                                   (?,1)  
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                       [D >= 1]                               (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                         [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                             True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                 [B >= 1]                               (1,2)  
          32. matrixmult(A,B,C,D)   -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2)  
          33. transAcc(A,B,C,D)     -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B))            [B >= 1]                               (?,2)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [1->{21},5->{33},9->{9},11->{11},19->{24},20->{21},21->{19,20},22->{25},23->{24},24->{22,23},25->{25}
          ,30->{32},31->{11},32->{1,31,33},33->{5,9}]
        Sizebounds:
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>,     ?) (<19,0,D>,     A) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>,     ?) (<21,0,D>,     A) 
          (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>,     ?) (<21,1,D>,     A) 
          (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<24,0,A>,     ?) (<24,0,B>, D) (<24,0,C>,     ?) (<24,0,D>, B + C) 
          (<24,1,A>,     ?) (<24,1,B>, D) (<24,1,C>,     ?) (<24,1,D>, B + C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
          (<32,0,A>,     A) (<32,0,B>, A) (<32,0,C>,     0) (<32,0,D>,     C) 
          (<33,0,A>,     ?) (<33,0,B>, C) (<33,0,C>,     A) (<33,0,D>,     ?) 
    + Applied Processor:
        ChainProcessor False [1,5,9,11,19,20,21,22,23,24,25,30,31,32,33]
    + Details:
        We chained rule 21 to obtain the rules [34] .
* Step 15: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                        True                                   (1,1)  
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                          True                                   (?,1)  
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                       [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                            [B >= 1]                               (2*C,1)
          19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D)                                               True                                   (?,1)  
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                       True                                   (?,1)  
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                   True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                          True                                   (?,1)  
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                       [D >= 1]                               (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                         [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                             True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                 [B >= 1]                               (1,2)  
          32. matrixmult(A,B,C,D)   -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2)  
          33. transAcc(A,B,C,D)     -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B))            [B >= 1]                               (?,2)  
          34. matrixmultp(A,B,C,D)  -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A))                     [B >= 1]                               (?,2)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [1->{34},5->{33},9->{9},11->{11},19->{24},20->{34},22->{25},23->{24},24->{22,23},25->{25},30->{32}
          ,31->{11},32->{1,31,33},33->{5,9},34->{20,24}]
        Sizebounds:
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>,     ?) (<19,0,D>,     A) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<24,0,A>,     ?) (<24,0,B>, D) (<24,0,C>,     ?) (<24,0,D>, B + C) 
          (<24,1,A>,     ?) (<24,1,B>, D) (<24,1,C>,     ?) (<24,1,D>, B + C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
          (<32,0,A>,     A) (<32,0,B>, A) (<32,0,C>,     0) (<32,0,D>,     C) 
          (<33,0,A>,     ?) (<33,0,B>, C) (<33,0,C>,     A) (<33,0,D>,     ?) 
          (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>,     ?) (<34,0,D>,     A) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [19]
* Step 16: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                        True                                   (1,1)  
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                          True                                   (?,1)  
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                       [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                            [B >= 1]                               (2*C,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                       True                                   (?,1)  
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                   True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                          True                                   (?,1)  
          24. linemult(A,B,C,D)     -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A))                       [D >= 1]                               (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                         [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                             True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                 [B >= 1]                               (1,2)  
          32. matrixmult(A,B,C,D)   -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2)  
          33. transAcc(A,B,C,D)     -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B))            [B >= 1]                               (?,2)  
          34. matrixmultp(A,B,C,D)  -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A))                     [B >= 1]                               (?,2)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [1->{34},5->{33},9->{9},11->{11},20->{34},22->{25},23->{24},24->{22,23},25->{25},30->{32},31->{11},32->{1
          ,31,33},33->{5,9},34->{20,24}]
        Sizebounds:
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<24,0,A>,     ?) (<24,0,B>, D) (<24,0,C>,     ?) (<24,0,D>, B + C) 
          (<24,1,A>,     ?) (<24,1,B>, D) (<24,1,C>,     ?) (<24,1,D>, B + C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
          (<32,0,A>,     A) (<32,0,B>, A) (<32,0,C>,     0) (<32,0,D>,     C) 
          (<33,0,A>,     ?) (<33,0,B>, C) (<33,0,C>,     A) (<33,0,D>,     ?) 
          (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>,     ?) (<34,0,D>,     A) 
    + Applied Processor:
        ChainProcessor False [1,5,9,11,20,22,23,24,25,30,31,32,33,34]
    + Details:
        We chained rule 24 to obtain the rules [35] .
* Step 17: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                        True                                   (1,1)  
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                          True                                   (?,1)  
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                       [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                            [B >= 1]                               (2*C,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                       True                                   (?,1)  
          22. linemult0(A,B,C,D)    -> mult(A,B,C,D)                                                   True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                          True                                   (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                         [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                             True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                 [B >= 1]                               (1,2)  
          32. matrixmult(A,B,C,D)   -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2)  
          33. transAcc(A,B,C,D)     -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B))            [B >= 1]                               (?,2)  
          34. matrixmultp(A,B,C,D)  -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A))                     [B >= 1]                               (?,2)  
          35. linemult(A,B,C,D)     -> c2(mult(D,B,C,A),linemult1(D,B,C,A))                            [D >= 1]                               (?,2)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [1->{34},5->{33},9->{9},11->{11},20->{34},22->{25},23->{35},25->{25},30->{32},31->{11},32->{1,31,33}
          ,33->{5,9},34->{20,35},35->{23,25}]
        Sizebounds:
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<22,0,A>,     ?) (<22,0,B>, D) (<22,0,C>,     ?) (<22,0,D>, B + C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
          (<32,0,A>,     A) (<32,0,B>, A) (<32,0,C>,     0) (<32,0,D>,     C) 
          (<33,0,A>,     ?) (<33,0,B>, C) (<33,0,C>,     A) (<33,0,D>,     ?) 
          (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>,     ?) (<34,0,D>,     A) 
          (<35,0,A>,     ?) (<35,0,B>, D) (<35,0,C>,     ?) (<35,0,D>, B + C) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [22]
* Step 18: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                        True                                   (1,1)  
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                          True                                   (?,1)  
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                       [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                            [B >= 1]                               (2*C,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                       True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                          True                                   (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                         [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                             True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                 [B >= 1]                               (1,2)  
          32. matrixmult(A,B,C,D)   -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2)  
          33. transAcc(A,B,C,D)     -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B))            [B >= 1]                               (?,2)  
          34. matrixmultp(A,B,C,D)  -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A))                     [B >= 1]                               (?,2)  
          35. linemult(A,B,C,D)     -> c2(mult(D,B,C,A),linemult1(D,B,C,A))                            [D >= 1]                               (?,2)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [1->{34},5->{33},9->{9},11->{11},20->{34},23->{35},25->{25},30->{32},31->{11},32->{1,31,33},33->{5,9}
          ,34->{20,35},35->{23,25}]
        Sizebounds:
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
          (<32,0,A>,     A) (<32,0,B>, A) (<32,0,C>,     0) (<32,0,D>,     C) 
          (<33,0,A>,     ?) (<33,0,B>, C) (<33,0,C>,     A) (<33,0,D>,     ?) 
          (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>,     ?) (<34,0,D>,     A) 
          (<35,0,A>,     ?) (<35,0,B>, D) (<35,0,C>,     ?) (<35,0,D>, B + C) 
    + Applied Processor:
        ChainProcessor False [1,5,9,11,20,23,25,30,31,32,33,34,35]
    + Details:
        We chained rule 32 to obtain the rules [36] .
* Step 19: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          1.  matrixmult1(A,B,C,D)  -> matrixmultp(B,A,A + D,C)                                            True                                   (1,1)  
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                              True                                   (?,1)  
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                           [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                                [B >= 1]                               (2*C,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                           True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                              True                                   (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                             [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                 True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                     [B >= 1]                               (1,2)  
          33. transAcc(A,B,C,D)     -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B))                [B >= 1]                               (?,2)  
          34. matrixmultp(A,B,C,D)  -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A))                         [B >= 1]                               (?,2)  
          35. linemult(A,B,C,D)     -> c2(mult(D,B,C,A),linemult1(D,B,C,A))                                [D >= 1]                               (?,2)  
          36. matrixmult(A,B,C,D)   -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [1->{34},5->{33},9->{9},11->{11},20->{34},23->{35},25->{25},30->{36},31->{11},33->{5,9},34->{20,35}
          ,35->{23,25},36->{31,33,34}]
        Sizebounds:
          (< 1,0,A>,     A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>,     D) 
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
          (<33,0,A>,     ?) (<33,0,B>, C) (<33,0,C>,     A) (<33,0,D>,     ?) 
          (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>,     ?) (<34,0,D>,     A) 
          (<35,0,A>,     ?) (<35,0,B>, D) (<35,0,C>,     ?) (<35,0,D>, B + C) 
          (<36,0,A>,     A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>,     D) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [1]
* Step 20: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                              True                                   (?,1)  
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                           [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                                [B >= 1]                               (2*C,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                           True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                              True                                   (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                             [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                 True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                     [B >= 1]                               (1,2)  
          33. transAcc(A,B,C,D)     -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B))                [B >= 1]                               (?,2)  
          34. matrixmultp(A,B,C,D)  -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A))                         [B >= 1]                               (?,2)  
          35. linemult(A,B,C,D)     -> c2(mult(D,B,C,A),linemult1(D,B,C,A))                                [D >= 1]                               (?,2)  
          36. matrixmult(A,B,C,D)   -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [5->{33},9->{9},11->{11},20->{34},23->{35},25->{25},30->{36},31->{11},33->{5,9},34->{20,35},35->{23,25}
          ,36->{31,33,34}]
        Sizebounds:
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
          (<33,0,A>,     ?) (<33,0,B>, C) (<33,0,C>,     A) (<33,0,D>,     ?) 
          (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>,     ?) (<34,0,D>,     A) 
          (<35,0,A>,     ?) (<35,0,B>, D) (<35,0,C>,     ?) (<35,0,D>, B + C) 
          (<36,0,A>,     A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>,     D) 
    + Applied Processor:
        ChainProcessor False [5,9,11,20,23,25,30,31,33,34,35,36]
    + Details:
        We chained rule 33 to obtain the rules [37] .
* Step 21: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          5.  transAcc1(A,B,C,D)    -> transAcc(C,-1 + D,A,B)                                              True                                   (?,1)  
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                           [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                                [B >= 1]                               (2*C,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                           True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                              True                                   (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                             [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                 True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                     [B >= 1]                               (1,2)  
          34. matrixmultp(A,B,C,D)  -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A))                         [B >= 1]                               (?,2)  
          35. linemult(A,B,C,D)     -> c2(mult(D,B,C,A),linemult1(D,B,C,A))                                [D >= 1]                               (?,2)  
          36. matrixmult(A,B,C,D)   -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3)  
          37. transAcc(A,B,C,D)     -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D))   [B >= 1]                               (?,3)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [5->{37},9->{9},11->{11},20->{34},23->{35},25->{25},30->{36},31->{11},34->{20,35},35->{23,25},36->{31,34
          ,37},37->{9,37}]
        Sizebounds:
          (< 5,0,A>,     A) (< 5,0,B>, ?) (< 5,0,C>,     0) (< 5,0,D>,     C) 
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
          (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>,     ?) (<34,0,D>,     A) 
          (<35,0,A>,     ?) (<35,0,B>, D) (<35,0,C>,     ?) (<35,0,D>, B + C) 
          (<36,0,A>,     A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>,     D) 
          (<37,0,A>,     A) (<37,0,B>, ?) (<37,0,C>,     0) (<37,0,D>,     C) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [5]
* Step 22: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                           [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                                [B >= 1]                               (2*C,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                           True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                              True                                   (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                             [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                 True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                     [B >= 1]                               (1,2)  
          34. matrixmultp(A,B,C,D)  -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A))                         [B >= 1]                               (?,2)  
          35. linemult(A,B,C,D)     -> c2(mult(D,B,C,A),linemult1(D,B,C,A))                                [D >= 1]                               (?,2)  
          36. matrixmult(A,B,C,D)   -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3)  
          37. transAcc(A,B,C,D)     -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D))   [B >= 1]                               (?,3)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},20->{34},23->{35},25->{25},30->{36},31->{11},34->{20,35},35->{23,25},36->{31,34,37}
          ,37->{9,37}]
        Sizebounds:
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
          (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>,     ?) (<34,0,D>,     A) 
          (<35,0,A>,     ?) (<35,0,B>, D) (<35,0,C>,     ?) (<35,0,D>, B + C) 
          (<36,0,A>,     A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>,     D) 
          (<37,0,A>,     A) (<37,0,B>, ?) (<37,0,C>,     0) (<37,0,D>,     C) 
    + Applied Processor:
        ChainProcessor False [9,11,20,23,25,30,31,34,35,36,37]
    + Details:
        We chained rule 34 to obtain the rules [38] .
* Step 23: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)       -> attach(A,-1 + B,C,-1 + D)                                           [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)       -> mkBase(A,-1 + B,C,D)                                                [B >= 1]                               (2*C,1)
          20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B)                                           True                                   (?,1)  
          23. linemult1(A,B,C,D)    -> linemult(D,B,C,-1 + A)                                              True                                   (?,1)  
          25. mult(A,B,C,D)         -> mult(A,-1 + B,C,-1 + D)                                             [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)        -> matrixmult(A,B,C,D)                                                 True                                   (1,1)  
          31. matrixmult2(A,B,C,D)  -> mkBase(A,D,C,D)                                                     [B >= 1]                               (1,2)  
          35. linemult(A,B,C,D)     -> c2(mult(D,B,C,A),linemult1(D,B,C,A))                                [D >= 1]                               (?,2)  
          36. matrixmult(A,B,C,D)   -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3)  
          37. transAcc(A,B,C,D)     -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D))   [B >= 1]                               (?,3)  
          38. matrixmultp(A,B,C,D)  -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                     [B >= 1]                               (?,3)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},20->{38},23->{35},25->{25},30->{36},31->{11},35->{23,25},36->{31,37,38},37->{9,37}
          ,38->{35,38}]
        Sizebounds:
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<20,0,A>,     A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>,     D) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
          (<35,0,A>,     ?) (<35,0,B>, D) (<35,0,C>,     ?) (<35,0,D>, B + C) 
          (<36,0,A>,     A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>,     D) 
          (<37,0,A>,     A) (<37,0,B>, ?) (<37,0,C>,     0) (<37,0,D>,     C) 
          (<38,0,A>,     A) (<38,0,B>, ?) (<38,0,C>, B + C) (<38,0,D>,     D) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [20]
* Step 24: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)      -> attach(A,-1 + B,C,-1 + D)                                           [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)      -> mkBase(A,-1 + B,C,D)                                                [B >= 1]                               (2*C,1)
          23. linemult1(A,B,C,D)   -> linemult(D,B,C,-1 + A)                                              True                                   (?,1)  
          25. mult(A,B,C,D)        -> mult(A,-1 + B,C,-1 + D)                                             [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)       -> matrixmult(A,B,C,D)                                                 True                                   (1,1)  
          31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D)                                                     [B >= 1]                               (1,2)  
          35. linemult(A,B,C,D)    -> c2(mult(D,B,C,A),linemult1(D,B,C,A))                                [D >= 1]                               (?,2)  
          36. matrixmult(A,B,C,D)  -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3)  
          37. transAcc(A,B,C,D)    -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D))   [B >= 1]                               (?,3)  
          38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                     [B >= 1]                               (?,3)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},23->{35},25->{25},30->{36},31->{11},35->{23,25},36->{31,37,38},37->{9,37},38->{35,38}]
        Sizebounds:
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>,     ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>,     C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>,     ?) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>,     ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>,     D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>,     C) 
          (<35,0,A>,     ?) (<35,0,B>, D) (<35,0,C>,     ?) (<35,0,D>, B + C) 
          (<36,0,A>,     A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>,     D) 
          (<37,0,A>,     A) (<37,0,B>, ?) (<37,0,C>,     0) (<37,0,D>,     C) 
          (<38,0,A>,     A) (<38,0,B>, ?) (<38,0,C>, B + C) (<38,0,D>,     D) 
    + Applied Processor:
        ChainProcessor False [9,11,23,25,30,31,35,36,37,38]
    + Details:
        We chained rule 35 to obtain the rules [39] .
* Step 25: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)      -> attach(A,-1 + B,C,-1 + D)                                           [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)      -> mkBase(A,-1 + B,C,D)                                                [B >= 1]                               (2*C,1)
          23. linemult1(A,B,C,D)   -> linemult(D,B,C,-1 + A)                                              True                                   (?,1)  
          25. mult(A,B,C,D)        -> mult(A,-1 + B,C,-1 + D)                                             [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)       -> matrixmult(A,B,C,D)                                                 True                                   (1,1)  
          31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D)                                                     [B >= 1]                               (1,2)  
          36. matrixmult(A,B,C,D)  -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3)  
          37. transAcc(A,B,C,D)    -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D))   [B >= 1]                               (?,3)  
          38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                     [B >= 1]                               (?,3)  
          39. linemult(A,B,C,D)    -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D))                            [D >= 1]                               (?,3)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},23->{39},25->{25},30->{36},31->{11},36->{31,37,38},37->{9,37},38->{38,39},39->{25,39}]
        Sizebounds:
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>, ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>, C) 
          (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>,     ?) (<23,0,D>, ?) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>, ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>, D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>, C) 
          (<36,0,A>,     A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>, D) 
          (<37,0,A>,     A) (<37,0,B>, ?) (<37,0,C>,     0) (<37,0,D>, C) 
          (<38,0,A>,     A) (<38,0,B>, ?) (<38,0,C>, B + C) (<38,0,D>, D) 
          (<39,0,A>, B + C) (<39,0,B>, D) (<39,0,C>,     ?) (<39,0,D>, ?) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [23]
* Step 26: ChainProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)      -> attach(A,-1 + B,C,-1 + D)                                           [B >= 1]                               (?,1)  
          11. mkBase(A,B,C,D)      -> mkBase(A,-1 + B,C,D)                                                [B >= 1]                               (2*C,1)
          25. mult(A,B,C,D)        -> mult(A,-1 + B,C,-1 + D)                                             [B >= 1 && D >= 1]                     (?,1)  
          30. start(A,B,C,D)       -> matrixmult(A,B,C,D)                                                 True                                   (1,1)  
          31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D)                                                     [B >= 1]                               (1,2)  
          36. matrixmult(A,B,C,D)  -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3)  
          37. transAcc(A,B,C,D)    -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D))   [B >= 1]                               (?,3)  
          38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                     [B >= 1]                               (?,3)  
          39. linemult(A,B,C,D)    -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D))                            [D >= 1]                               (?,3)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},25->{25},30->{36},31->{11},36->{31,37,38},37->{9,37},38->{38,39},39->{25,39}]
        Sizebounds:
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>, ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>, C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>, ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>, D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>, C) 
          (<36,0,A>,     A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>, D) 
          (<37,0,A>,     A) (<37,0,B>, ?) (<37,0,C>,     0) (<37,0,D>, C) 
          (<38,0,A>,     A) (<38,0,B>, ?) (<38,0,C>, B + C) (<38,0,D>, D) 
          (<39,0,A>, B + C) (<39,0,B>, D) (<39,0,C>,     ?) (<39,0,D>, ?) 
    + Applied Processor:
        ChainProcessor False [9,11,25,30,31,36,37,38,39]
    + Details:
        We chained rule 36 to obtain the rules [40] .
* Step 27: UnreachableRules WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)      -> attach(A,-1 + B,C,-1 + D)                                         [B >= 1]                                         (?,1)  
          11. mkBase(A,B,C,D)      -> mkBase(A,-1 + B,C,D)                                              [B >= 1]                                         (2*C,1)
          25. mult(A,B,C,D)        -> mult(A,-1 + B,C,-1 + D)                                           [B >= 1 && D >= 1]                               (?,1)  
          30. start(A,B,C,D)       -> matrixmult(A,B,C,D)                                               True                                             (1,1)  
          31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D)                                                   [B >= 1]                                         (1,2)  
          37. transAcc(A,B,C,D)    -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1]                                         (?,3)  
          38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                   [B >= 1]                                         (?,3)  
          39. linemult(A,B,C,D)    -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D))                          [D >= 1]                                         (?,3)  
          40. matrixmult(A,B,C,D)  -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C))    [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},25->{25},30->{40},31->{11},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}]
        Sizebounds:
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>, ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>, C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>, ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>, D) 
          (<31,0,A>,     B) (<31,0,B>, C) (<31,0,C>,     D) (<31,0,D>, C) 
          (<37,0,A>,     A) (<37,0,B>, ?) (<37,0,C>,     0) (<37,0,D>, C) 
          (<38,0,A>,     A) (<38,0,B>, ?) (<38,0,C>, B + C) (<38,0,D>, D) 
          (<39,0,A>, B + C) (<39,0,B>, D) (<39,0,C>,     ?) (<39,0,D>, ?) 
          (<40,0,A>,     B) (<40,0,B>, C) (<40,0,C>,     D) (<40,0,D>, C) 
    + Applied Processor:
        UnreachableRules
    + Details:
        The following transitions are not reachable from the starting states and are removed: [31]
* Step 28: LocalSizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)      -> attach(A,-1 + B,C,-1 + D)                                         [B >= 1]                                         (?,1)  
          11. mkBase(A,B,C,D)      -> mkBase(A,-1 + B,C,D)                                              [B >= 1]                                         (2*C,1)
          25. mult(A,B,C,D)        -> mult(A,-1 + B,C,-1 + D)                                           [B >= 1 && D >= 1]                               (?,1)  
          30. start(A,B,C,D)       -> matrixmult(A,B,C,D)                                               True                                             (1,1)  
          37. transAcc(A,B,C,D)    -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1]                                         (?,3)  
          38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                   [B >= 1]                                         (?,3)  
          39. linemult(A,B,C,D)    -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D))                          [D >= 1]                                         (?,3)  
          40. matrixmult(A,B,C,D)  -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C))    [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}]
        Sizebounds:
          (< 9,0,A>,     ?) (< 9,0,B>, ?) (< 9,0,C>,     A) (< 9,0,D>, ?) 
          (<11,0,A>,     B) (<11,0,B>, ?) (<11,0,C>,     D) (<11,0,D>, C) 
          (<25,0,A>,     ?) (<25,0,B>, ?) (<25,0,C>,     ?) (<25,0,D>, ?) 
          (<30,0,A>,     A) (<30,0,B>, B) (<30,0,C>,     C) (<30,0,D>, D) 
          (<37,0,A>,     A) (<37,0,B>, ?) (<37,0,C>,     0) (<37,0,D>, C) 
          (<38,0,A>,     A) (<38,0,B>, ?) (<38,0,C>, B + C) (<38,0,D>, D) 
          (<39,0,A>, B + C) (<39,0,B>, D) (<39,0,C>,     ?) (<39,0,D>, ?) 
          (<40,0,A>,     B) (<40,0,B>, C) (<40,0,C>,     D) (<40,0,D>, C) 
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (< 9,0,A>,         A, .= 0) (< 9,0,B>, 1 + B, .+ 1) (< 9,0,C>,         C, .= 0) (< 9,0,D>, 1 + D, .+ 1) 
          (<11,0,A>,         A, .= 0) (<11,0,B>, 1 + B, .+ 1) (<11,0,C>,         C, .= 0) (<11,0,D>,     D, .= 0) 
          (<25,0,A>,         A, .= 0) (<25,0,B>, 1 + B, .+ 1) (<25,0,C>,         C, .= 0) (<25,0,D>, 1 + D, .+ 1) 
          (<30,0,A>,         A, .= 0) (<30,0,B>,     B, .= 0) (<30,0,C>,         C, .= 0) (<30,0,D>,     D, .= 0) 
          (<37,0,A>, 1 + B + C, .* 1) (<37,0,B>,     D, .= 0) (<37,0,C>,         A, .= 0) (<37,0,D>, 1 + B, .+ 1) 
          (<37,1,A>,         A, .= 0) (<37,1,B>, 2 + B, .+ 2) (<37,1,C>, 1 + B + C, .* 1) (<37,1,D>,     D, .= 0) 
          (<38,0,A>,         C, .= 0) (<38,0,B>,     D, .= 0) (<38,0,C>,         B, .= 0) (<38,0,D>,     A, .= 0) 
          (<38,1,A>,         A, .= 0) (<38,1,B>, 1 + B, .+ 1) (<38,1,C>,         C, .= 0) (<38,1,D>,     D, .= 0) 
          (<39,0,A>,         D, .= 0) (<39,0,B>,     B, .= 0) (<39,0,C>,         C, .= 0) (<39,0,D>,     A, .= 0) 
          (<39,1,A>,         A, .= 0) (<39,1,B>,     B, .= 0) (<39,1,C>,         C, .= 0) (<39,1,D>, 1 + D, .+ 1) 
          (<40,0,A>,         A, .= 0) (<40,0,B>,     A, .= 0) (<40,0,C>,         0, .= 0) (<40,0,D>,     C, .= 0) 
          (<40,1,A>,         A, .= 0) (<40,1,B>,     A, .= 0) (<40,1,C>, 1 + A + C, .* 1) (<40,1,D>,     0, .= 0) 
          (<40,2,A>,         A, .= 0) (<40,2,B>,     C, .= 0) (<40,2,C>,         0, .= 0) (<40,2,D>,     C, .= 0) 
* Step 29: SizeboundsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)      -> attach(A,-1 + B,C,-1 + D)                                         [B >= 1]                                         (?,1)  
          11. mkBase(A,B,C,D)      -> mkBase(A,-1 + B,C,D)                                              [B >= 1]                                         (2*C,1)
          25. mult(A,B,C,D)        -> mult(A,-1 + B,C,-1 + D)                                           [B >= 1 && D >= 1]                               (?,1)  
          30. start(A,B,C,D)       -> matrixmult(A,B,C,D)                                               True                                             (1,1)  
          37. transAcc(A,B,C,D)    -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1]                                         (?,3)  
          38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                   [B >= 1]                                         (?,3)  
          39. linemult(A,B,C,D)    -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D))                          [D >= 1]                                         (?,3)  
          40. matrixmult(A,B,C,D)  -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C))    [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}]
        Sizebounds:
          (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) 
          (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) 
          (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) 
          (<30,0,A>, ?) (<30,0,B>, ?) (<30,0,C>, ?) (<30,0,D>, ?) 
          (<37,0,A>, ?) (<37,0,B>, ?) (<37,0,C>, ?) (<37,0,D>, ?) 
          (<37,1,A>, ?) (<37,1,B>, ?) (<37,1,C>, ?) (<37,1,D>, ?) 
          (<38,0,A>, ?) (<38,0,B>, ?) (<38,0,C>, ?) (<38,0,D>, ?) 
          (<38,1,A>, ?) (<38,1,B>, ?) (<38,1,C>, ?) (<38,1,D>, ?) 
          (<39,0,A>, ?) (<39,0,B>, ?) (<39,0,C>, ?) (<39,0,D>, ?) 
          (<39,1,A>, ?) (<39,1,B>, ?) (<39,1,C>, ?) (<39,1,D>, ?) 
          (<40,0,A>, ?) (<40,0,B>, ?) (<40,0,C>, ?) (<40,0,D>, ?) 
          (<40,1,A>, ?) (<40,1,B>, ?) (<40,1,C>, ?) (<40,1,D>, ?) 
          (<40,2,A>, ?) (<40,2,B>, ?) (<40,2,C>, ?) (<40,2,D>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (< 9,0,A>, ?) (< 9,0,B>,       ?) (< 9,0,C>,         ?) (< 9,0,D>, ?) 
          (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) 
          (<25,0,A>, ?) (<25,0,B>,       ?) (<25,0,C>,         ?) (<25,0,D>, ?) 
          (<30,0,A>, A) (<30,0,B>,       B) (<30,0,C>,         C) (<30,0,D>, D) 
          (<37,0,A>, ?) (<37,0,B>,       ?) (<37,0,C>,         ?) (<37,0,D>, ?) 
          (<37,1,A>, ?) (<37,1,B>,       ?) (<37,1,C>,         ?) (<37,1,D>, ?) 
          (<38,0,A>, ?) (<38,0,B>,       ?) (<38,0,C>,         ?) (<38,0,D>, ?) 
          (<38,1,A>, ?) (<38,1,B>,       ?) (<38,1,C>,         ?) (<38,1,D>, ?) 
          (<39,0,A>, ?) (<39,0,B>,       ?) (<39,0,C>,         ?) (<39,0,D>, ?) 
          (<39,1,A>, ?) (<39,1,B>,       ?) (<39,1,C>,         ?) (<39,1,D>, ?) 
          (<40,0,A>, A) (<40,0,B>,       A) (<40,0,C>,         0) (<40,0,D>, C) 
          (<40,1,A>, A) (<40,1,B>,       A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) 
          (<40,2,A>, A) (<40,2,B>,       C) (<40,2,C>,         0) (<40,2,D>, C) 
* Step 30: LocationConstraintsProc WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)      -> attach(A,-1 + B,C,-1 + D)                                         [B >= 1]                                         (?,1)  
          11. mkBase(A,B,C,D)      -> mkBase(A,-1 + B,C,D)                                              [B >= 1]                                         (2*C,1)
          25. mult(A,B,C,D)        -> mult(A,-1 + B,C,-1 + D)                                           [B >= 1 && D >= 1]                               (?,1)  
          30. start(A,B,C,D)       -> matrixmult(A,B,C,D)                                               True                                             (1,1)  
          37. transAcc(A,B,C,D)    -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1]                                         (?,3)  
          38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                   [B >= 1]                                         (?,3)  
          39. linemult(A,B,C,D)    -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D))                          [D >= 1]                                         (?,3)  
          40. matrixmult(A,B,C,D)  -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C))    [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}]
        Sizebounds:
          (< 9,0,A>, ?) (< 9,0,B>,       ?) (< 9,0,C>,         ?) (< 9,0,D>, ?) 
          (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) 
          (<25,0,A>, ?) (<25,0,B>,       ?) (<25,0,C>,         ?) (<25,0,D>, ?) 
          (<30,0,A>, A) (<30,0,B>,       B) (<30,0,C>,         C) (<30,0,D>, D) 
          (<37,0,A>, ?) (<37,0,B>,       ?) (<37,0,C>,         ?) (<37,0,D>, ?) 
          (<37,1,A>, ?) (<37,1,B>,       ?) (<37,1,C>,         ?) (<37,1,D>, ?) 
          (<38,0,A>, ?) (<38,0,B>,       ?) (<38,0,C>,         ?) (<38,0,D>, ?) 
          (<38,1,A>, ?) (<38,1,B>,       ?) (<38,1,C>,         ?) (<38,1,D>, ?) 
          (<39,0,A>, ?) (<39,0,B>,       ?) (<39,0,C>,         ?) (<39,0,D>, ?) 
          (<39,1,A>, ?) (<39,1,B>,       ?) (<39,1,C>,         ?) (<39,1,D>, ?) 
          (<40,0,A>, A) (<40,0,B>,       A) (<40,0,C>,         0) (<40,0,D>, C) 
          (<40,1,A>, A) (<40,1,B>,       A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) 
          (<40,2,A>, A) (<40,2,B>,       C) (<40,2,C>,         0) (<40,2,D>, C) 
    + Applied Processor:
        LocationConstraintsProc
    + Details:
        We computed the location constraints  9 :  True 11 :  True 25 :  True 30 :  True 37 :  True 38 :  True 39 :  True 40 :  True .
* Step 31: LoopRecurrenceProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)      -> attach(A,-1 + B,C,-1 + D)                                         [B >= 1]                                         (?,1)  
          11. mkBase(A,B,C,D)      -> mkBase(A,-1 + B,C,D)                                              [B >= 1]                                         (2*C,1)
          25. mult(A,B,C,D)        -> mult(A,-1 + B,C,-1 + D)                                           [B >= 1 && D >= 1]                               (?,1)  
          30. start(A,B,C,D)       -> matrixmult(A,B,C,D)                                               True                                             (1,1)  
          37. transAcc(A,B,C,D)    -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1]                                         (?,3)  
          38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                   [B >= 1]                                         (?,3)  
          39. linemult(A,B,C,D)    -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D))                          [D >= 1]                                         (?,3)  
          40. matrixmult(A,B,C,D)  -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C))    [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5)  
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}]
        Sizebounds:
          (< 9,0,A>, ?) (< 9,0,B>,       ?) (< 9,0,C>,         ?) (< 9,0,D>, ?) 
          (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) 
          (<25,0,A>, ?) (<25,0,B>,       ?) (<25,0,C>,         ?) (<25,0,D>, ?) 
          (<30,0,A>, A) (<30,0,B>,       B) (<30,0,C>,         C) (<30,0,D>, D) 
          (<37,0,A>, ?) (<37,0,B>,       ?) (<37,0,C>,         ?) (<37,0,D>, ?) 
          (<37,1,A>, ?) (<37,1,B>,       ?) (<37,1,C>,         ?) (<37,1,D>, ?) 
          (<38,0,A>, ?) (<38,0,B>,       ?) (<38,0,C>,         ?) (<38,0,D>, ?) 
          (<38,1,A>, ?) (<38,1,B>,       ?) (<38,1,C>,         ?) (<38,1,D>, ?) 
          (<39,0,A>, ?) (<39,0,B>,       ?) (<39,0,C>,         ?) (<39,0,D>, ?) 
          (<39,1,A>, ?) (<39,1,B>,       ?) (<39,1,C>,         ?) (<39,1,D>, ?) 
          (<40,0,A>, A) (<40,0,B>,       A) (<40,0,C>,         0) (<40,0,D>, C) 
          (<40,1,A>, A) (<40,1,B>,       A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) 
          (<40,2,A>, A) (<40,2,B>,       C) (<40,2,C>,         0) (<40,2,D>, C) 
    + Applied Processor:
        LoopRecurrenceProcessor [38]
    + Details:
        Applying the recurrence pattern linear * f to the expression B yields the solution 2*A*B + 2*A*B*D + B .
* Step 32: LoopRecurrenceProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)      -> attach(A,-1 + B,C,-1 + D)                                         [B >= 1]                                         (?,1)        
          11. mkBase(A,B,C,D)      -> mkBase(A,-1 + B,C,D)                                              [B >= 1]                                         (2*C,1)      
          25. mult(A,B,C,D)        -> mult(A,-1 + B,C,-1 + D)                                           [B >= 1 && D >= 1]                               (A + 2*A^2,1)
          30. start(A,B,C,D)       -> matrixmult(A,B,C,D)                                               True                                             (1,1)        
          37. transAcc(A,B,C,D)    -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1]                                         (?,3)        
          38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                   [B >= 1]                                         (A + 2*A^2,3)
          39. linemult(A,B,C,D)    -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D))                          [D >= 1]                                         (A + 2*A^2,3)
          40. matrixmult(A,B,C,D)  -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C))    [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5)        
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}]
        Sizebounds:
          (< 9,0,A>, ?) (< 9,0,B>,       ?) (< 9,0,C>,         ?) (< 9,0,D>, ?) 
          (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) 
          (<25,0,A>, ?) (<25,0,B>,       ?) (<25,0,C>,         ?) (<25,0,D>, ?) 
          (<30,0,A>, A) (<30,0,B>,       B) (<30,0,C>,         C) (<30,0,D>, D) 
          (<37,0,A>, ?) (<37,0,B>,       ?) (<37,0,C>,         ?) (<37,0,D>, ?) 
          (<37,1,A>, ?) (<37,1,B>,       ?) (<37,1,C>,         ?) (<37,1,D>, ?) 
          (<38,0,A>, ?) (<38,0,B>,       ?) (<38,0,C>,         ?) (<38,0,D>, ?) 
          (<38,1,A>, ?) (<38,1,B>,       ?) (<38,1,C>,         ?) (<38,1,D>, ?) 
          (<39,0,A>, ?) (<39,0,B>,       ?) (<39,0,C>,         ?) (<39,0,D>, ?) 
          (<39,1,A>, ?) (<39,1,B>,       ?) (<39,1,C>,         ?) (<39,1,D>, ?) 
          (<40,0,A>, A) (<40,0,B>,       A) (<40,0,C>,         0) (<40,0,D>, C) 
          (<40,1,A>, A) (<40,1,B>,       A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) 
          (<40,2,A>, A) (<40,2,B>,       C) (<40,2,C>,         0) (<40,2,D>, C) 
    + Applied Processor:
        LoopRecurrenceProcessor [39]
    + Details:
        Applying the recurrence pattern linear * f to the expression D yields the solution B*D + D .
* Step 33: LoopRecurrenceProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)      -> attach(A,-1 + B,C,-1 + D)                                         [B >= 1]                                         (?,1)        
          11. mkBase(A,B,C,D)      -> mkBase(A,-1 + B,C,D)                                              [B >= 1]                                         (2*C,1)      
          25. mult(A,B,C,D)        -> mult(A,-1 + B,C,-1 + D)                                           [B >= 1 && D >= 1]                               (A + 2*A^2,1)
          30. start(A,B,C,D)       -> matrixmult(A,B,C,D)                                               True                                             (1,1)        
          37. transAcc(A,B,C,D)    -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1]                                         (?,3)        
          38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                   [B >= 1]                                         (A + 2*A^2,3)
          39. linemult(A,B,C,D)    -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D))                          [D >= 1]                                         (A + 2*A^2,3)
          40. matrixmult(A,B,C,D)  -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C))    [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5)        
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}]
        Sizebounds:
          (< 9,0,A>, ?) (< 9,0,B>,       ?) (< 9,0,C>,         ?) (< 9,0,D>, ?) 
          (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) 
          (<25,0,A>, ?) (<25,0,B>,       ?) (<25,0,C>,         ?) (<25,0,D>, ?) 
          (<30,0,A>, A) (<30,0,B>,       B) (<30,0,C>,         C) (<30,0,D>, D) 
          (<37,0,A>, ?) (<37,0,B>,       ?) (<37,0,C>,         ?) (<37,0,D>, ?) 
          (<37,1,A>, ?) (<37,1,B>,       ?) (<37,1,C>,         ?) (<37,1,D>, ?) 
          (<38,0,A>, ?) (<38,0,B>,       ?) (<38,0,C>,         ?) (<38,0,D>, ?) 
          (<38,1,A>, ?) (<38,1,B>,       ?) (<38,1,C>,         ?) (<38,1,D>, ?) 
          (<39,0,A>, ?) (<39,0,B>,       ?) (<39,0,C>,         ?) (<39,0,D>, ?) 
          (<39,1,A>, ?) (<39,1,B>,       ?) (<39,1,C>,         ?) (<39,1,D>, ?) 
          (<40,0,A>, A) (<40,0,B>,       A) (<40,0,C>,         0) (<40,0,D>, C) 
          (<40,1,A>, A) (<40,1,B>,       A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) 
          (<40,2,A>, A) (<40,2,B>,       C) (<40,2,C>,         0) (<40,2,D>, C) 
    + Applied Processor:
        LoopRecurrenceProcessor [37]
    + Details:
        Applying the recurrence pattern linear * f to the expression B yields the solution B + B*D .
* Step 34: LoopRecurrenceProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)      -> attach(A,-1 + B,C,-1 + D)                                         [B >= 1]                                         (A + A*C,1)  
          11. mkBase(A,B,C,D)      -> mkBase(A,-1 + B,C,D)                                              [B >= 1]                                         (2*C,1)      
          25. mult(A,B,C,D)        -> mult(A,-1 + B,C,-1 + D)                                           [B >= 1 && D >= 1]                               (A + 2*A^2,1)
          30. start(A,B,C,D)       -> matrixmult(A,B,C,D)                                               True                                             (1,1)        
          37. transAcc(A,B,C,D)    -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1]                                         (A + A*C,3)  
          38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                   [B >= 1]                                         (A + 2*A^2,3)
          39. linemult(A,B,C,D)    -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D))                          [D >= 1]                                         (A + 2*A^2,3)
          40. matrixmult(A,B,C,D)  -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C))    [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5)        
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}]
        Sizebounds:
          (< 9,0,A>, ?) (< 9,0,B>,       ?) (< 9,0,C>,         ?) (< 9,0,D>, ?) 
          (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) 
          (<25,0,A>, ?) (<25,0,B>,       ?) (<25,0,C>,         ?) (<25,0,D>, ?) 
          (<30,0,A>, A) (<30,0,B>,       B) (<30,0,C>,         C) (<30,0,D>, D) 
          (<37,0,A>, ?) (<37,0,B>,       ?) (<37,0,C>,         ?) (<37,0,D>, ?) 
          (<37,1,A>, ?) (<37,1,B>,       ?) (<37,1,C>,         ?) (<37,1,D>, ?) 
          (<38,0,A>, ?) (<38,0,B>,       ?) (<38,0,C>,         ?) (<38,0,D>, ?) 
          (<38,1,A>, ?) (<38,1,B>,       ?) (<38,1,C>,         ?) (<38,1,D>, ?) 
          (<39,0,A>, ?) (<39,0,B>,       ?) (<39,0,C>,         ?) (<39,0,D>, ?) 
          (<39,1,A>, ?) (<39,1,B>,       ?) (<39,1,C>,         ?) (<39,1,D>, ?) 
          (<40,0,A>, A) (<40,0,B>,       A) (<40,0,C>,         0) (<40,0,D>, C) 
          (<40,1,A>, A) (<40,1,B>,       A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) 
          (<40,2,A>, A) (<40,2,B>,       C) (<40,2,C>,         0) (<40,2,D>, C) 
    + Applied Processor:
        LoopRecurrenceProcessor [25]
    + Details:
        Applying the recurrence pattern linear * f to the expression B yields the solution B .
* Step 35: LoopRecurrenceProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)      -> attach(A,-1 + B,C,-1 + D)                                         [B >= 1]                                         (A + A*C,1)  
          11. mkBase(A,B,C,D)      -> mkBase(A,-1 + B,C,D)                                              [B >= 1]                                         (2*C,1)      
          25. mult(A,B,C,D)        -> mult(A,-1 + B,C,-1 + D)                                           [B >= 1 && D >= 1]                               (A + 2*A^2,1)
          30. start(A,B,C,D)       -> matrixmult(A,B,C,D)                                               True                                             (1,1)        
          37. transAcc(A,B,C,D)    -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1]                                         (A + A*C,3)  
          38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                   [B >= 1]                                         (A + 2*A^2,3)
          39. linemult(A,B,C,D)    -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D))                          [D >= 1]                                         (A + 2*A^2,3)
          40. matrixmult(A,B,C,D)  -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C))    [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5)        
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}]
        Sizebounds:
          (< 9,0,A>, ?) (< 9,0,B>,       ?) (< 9,0,C>,         ?) (< 9,0,D>, ?) 
          (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) 
          (<25,0,A>, ?) (<25,0,B>,       ?) (<25,0,C>,         ?) (<25,0,D>, ?) 
          (<30,0,A>, A) (<30,0,B>,       B) (<30,0,C>,         C) (<30,0,D>, D) 
          (<37,0,A>, ?) (<37,0,B>,       ?) (<37,0,C>,         ?) (<37,0,D>, ?) 
          (<37,1,A>, ?) (<37,1,B>,       ?) (<37,1,C>,         ?) (<37,1,D>, ?) 
          (<38,0,A>, ?) (<38,0,B>,       ?) (<38,0,C>,         ?) (<38,0,D>, ?) 
          (<38,1,A>, ?) (<38,1,B>,       ?) (<38,1,C>,         ?) (<38,1,D>, ?) 
          (<39,0,A>, ?) (<39,0,B>,       ?) (<39,0,C>,         ?) (<39,0,D>, ?) 
          (<39,1,A>, ?) (<39,1,B>,       ?) (<39,1,C>,         ?) (<39,1,D>, ?) 
          (<40,0,A>, A) (<40,0,B>,       A) (<40,0,C>,         0) (<40,0,D>, C) 
          (<40,1,A>, A) (<40,1,B>,       A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) 
          (<40,2,A>, A) (<40,2,B>,       C) (<40,2,C>,         0) (<40,2,D>, C) 
    + Applied Processor:
        LoopRecurrenceProcessor [11]
    + Details:
        Applying the recurrence pattern linear * f to the expression B yields the solution B .
* Step 36: LoopRecurrenceProcessor WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)      -> attach(A,-1 + B,C,-1 + D)                                         [B >= 1]                                         (A + A*C,1)  
          11. mkBase(A,B,C,D)      -> mkBase(A,-1 + B,C,D)                                              [B >= 1]                                         (C,1)        
          25. mult(A,B,C,D)        -> mult(A,-1 + B,C,-1 + D)                                           [B >= 1 && D >= 1]                               (A + 2*A^2,1)
          30. start(A,B,C,D)       -> matrixmult(A,B,C,D)                                               True                                             (1,1)        
          37. transAcc(A,B,C,D)    -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1]                                         (A + A*C,3)  
          38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                   [B >= 1]                                         (A + 2*A^2,3)
          39. linemult(A,B,C,D)    -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D))                          [D >= 1]                                         (A + 2*A^2,3)
          40. matrixmult(A,B,C,D)  -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C))    [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5)        
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}]
        Sizebounds:
          (< 9,0,A>, ?) (< 9,0,B>,       ?) (< 9,0,C>,         ?) (< 9,0,D>, ?) 
          (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) 
          (<25,0,A>, ?) (<25,0,B>,       ?) (<25,0,C>,         ?) (<25,0,D>, ?) 
          (<30,0,A>, A) (<30,0,B>,       B) (<30,0,C>,         C) (<30,0,D>, D) 
          (<37,0,A>, ?) (<37,0,B>,       ?) (<37,0,C>,         ?) (<37,0,D>, ?) 
          (<37,1,A>, ?) (<37,1,B>,       ?) (<37,1,C>,         ?) (<37,1,D>, ?) 
          (<38,0,A>, ?) (<38,0,B>,       ?) (<38,0,C>,         ?) (<38,0,D>, ?) 
          (<38,1,A>, ?) (<38,1,B>,       ?) (<38,1,C>,         ?) (<38,1,D>, ?) 
          (<39,0,A>, ?) (<39,0,B>,       ?) (<39,0,C>,         ?) (<39,0,D>, ?) 
          (<39,1,A>, ?) (<39,1,B>,       ?) (<39,1,C>,         ?) (<39,1,D>, ?) 
          (<40,0,A>, A) (<40,0,B>,       A) (<40,0,C>,         0) (<40,0,D>, C) 
          (<40,1,A>, A) (<40,1,B>,       A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) 
          (<40,2,A>, A) (<40,2,B>,       C) (<40,2,C>,         0) (<40,2,D>, C) 
    + Applied Processor:
        LoopRecurrenceProcessor [9]
    + Details:
        Applying the recurrence pattern linear * f to the expression B yields the solution B .
* Step 37: UnsatPaths WORST_CASE(?,O(n^2))
    + Considered Problem:
        Rules:
          9.  attach(A,B,C,D)      -> attach(A,-1 + B,C,-1 + D)                                         [B >= 1]                                         (A + A*C,1)  
          11. mkBase(A,B,C,D)      -> mkBase(A,-1 + B,C,D)                                              [B >= 1]                                         (C,1)        
          25. mult(A,B,C,D)        -> mult(A,-1 + B,C,-1 + D)                                           [B >= 1 && D >= 1]                               (A + 2*A^2,1)
          30. start(A,B,C,D)       -> matrixmult(A,B,C,D)                                               True                                             (1,1)        
          37. transAcc(A,B,C,D)    -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1]                                         (A + A*C,3)  
          38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D))                   [B >= 1]                                         (A + 2*A^2,3)
          39. linemult(A,B,C,D)    -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D))                          [D >= 1]                                         (A + 2*A^2,3)
          40. matrixmult(A,B,C,D)  -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C))    [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5)        
        Signature:
          {(attach,4)
          ;(linemult,4)
          ;(linemult0,4)
          ;(linemult1,4)
          ;(makeBase,4)
          ;(matrixmult,4)
          ;(matrixmult0,4)
          ;(matrixmult1,4)
          ;(matrixmult2,4)
          ;(matrixmult3,4)
          ;(matrixmultp,4)
          ;(matrixmultp0,4)
          ;(matrixmultp1,4)
          ;(mkBase,4)
          ;(mult,4)
          ;(out1makeBase,4)
          ;(out1split,4)
          ;(out1transAcc,4)
          ;(out2split,4)
          ;(out2transAcc,4)
          ;(out3split,4)
          ;(outmkBase,4)
          ;(split,4)
          ;(start,4)
          ;(transAcc,4)
          ;(transAcc0,4)
          ;(transAcc1,4)
          ;(transpose,4)
          ;(transpose0,4)
          ;(transpose1,4)}
        Flow Graph:
          [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}]
        Sizebounds:
          (< 9,0,A>, ?) (< 9,0,B>,       ?) (< 9,0,C>,         ?) (< 9,0,D>, ?) 
          (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) 
          (<25,0,A>, ?) (<25,0,B>,       ?) (<25,0,C>,         ?) (<25,0,D>, ?) 
          (<30,0,A>, A) (<30,0,B>,       B) (<30,0,C>,         C) (<30,0,D>, D) 
          (<37,0,A>, ?) (<37,0,B>,       ?) (<37,0,C>,         ?) (<37,0,D>, ?) 
          (<37,1,A>, ?) (<37,1,B>,       ?) (<37,1,C>,         ?) (<37,1,D>, ?) 
          (<38,0,A>, ?) (<38,0,B>,       ?) (<38,0,C>,         ?) (<38,0,D>, ?) 
          (<38,1,A>, ?) (<38,1,B>,       ?) (<38,1,C>,         ?) (<38,1,D>, ?) 
          (<39,0,A>, ?) (<39,0,B>,       ?) (<39,0,C>,         ?) (<39,0,D>, ?) 
          (<39,1,A>, ?) (<39,1,B>,       ?) (<39,1,C>,         ?) (<39,1,D>, ?) 
          (<40,0,A>, A) (<40,0,B>,       A) (<40,0,C>,         0) (<40,0,D>, C) 
          (<40,1,A>, A) (<40,1,B>,       A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) 
          (<40,2,A>, A) (<40,2,B>,       C) (<40,2,C>,         0) (<40,2,D>, C) 
    + Applied Processor:
        UnsatPaths
    + Details:
        The problem is already solved.

WORST_CASE(?,O(n^2))