WORST_CASE(?,O(n^1))
* Step 1: UnsatRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  start(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)              [0 >= 1 + A && B = C && D = E && F = A]                                                 (?,1)
          1.  start(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)              [A >= 0 && C >= 1 + E && B = C && D = E && F = A]                                       (?,1)
          2.  start(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A]                                           (?,1)
          3.  start(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && E >= C && B = C && D = E && F = A]                                           (?,1)
          4.  lbl91(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)              [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A]           (?,1)
          5.  lbl91(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)              [D >= B && 0 >= 1 + A && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1)
          6.  lbl91(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A]               (?,1)
          7.  lbl91(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A]               (?,1)
          8.  lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F)              [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A]           (?,1)
          9.  lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F)              [D >= B && 0 >= 1 + A && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1)
          10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A]               (?,1)
          11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A]               (?,1)
          12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)             True                                                                                    (1,1)
        Signature:
          {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [0->{},1->{},2->{4,5,6,7},3->{8,9,10,11},4->{},5->{},6->{4,5,6,7},7->{8,9,10,11},8->{},9->{},10->{4,5,6,7}
          ,11->{8,9,10,11},12->{0,1,2,3}]
        
    + Applied Processor:
        UnsatRules
    + Details:
        The following transitions have unsatisfiable constraints and are removed:  [5,9]
* Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  start(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)              [0 >= 1 + A && B = C && D = E && F = A]                                       (?,1)
          1.  start(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)              [A >= 0 && C >= 1 + E && B = C && D = E && F = A]                             (?,1)
          2.  start(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A]                                 (?,1)
          3.  start(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && E >= C && B = C && D = E && F = A]                                 (?,1)
          4.  lbl91(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)              [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1)
          6.  lbl91(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A]     (?,1)
          7.  lbl91(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A]     (?,1)
          8.  lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F)              [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1)
          10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A]     (?,1)
          11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A]     (?,1)
          12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)             True                                                                          (1,1)
        Signature:
          {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [0->{},1->{},2->{4,6,7},3->{8,10,11},4->{},6->{4,6,7},7->{8,10,11},8->{},10->{4,6,7},11->{8,10,11},12->{0
          ,1,2,3}]
        
    + Applied Processor:
        LocalSizeboundsProc
    + Details:
        LocalSizebounds generated; rvgraph
          (< 0,0,A>, A, .= 0) (< 0,0,B>,             B, .= 0) (< 0,0,C>, C, .= 0) (< 0,0,D>,         D, .= 0) (< 0,0,E>, E, .= 0) (< 0,0,F>, F, .= 0) 
          (< 1,0,A>, A, .= 0) (< 1,0,B>,             B, .= 0) (< 1,0,C>, C, .= 0) (< 1,0,D>,         D, .= 0) (< 1,0,E>, E, .= 0) (< 1,0,F>, F, .= 0) 
          (< 2,0,A>, A, .= 0) (< 2,0,B>,             B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, 1 + D + F, .* 1) (< 2,0,E>, E, .= 0) (< 2,0,F>, F, .= 0) 
          (< 3,0,A>, A, .= 0) (< 3,0,B>,     1 + B + F, .* 1) (< 3,0,C>, C, .= 0) (< 3,0,D>,         D, .= 0) (< 3,0,E>, E, .= 0) (< 3,0,F>, F, .= 0) 
          (< 4,0,A>, A, .= 0) (< 4,0,B>,             B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>,         D, .= 0) (< 4,0,E>, E, .= 0) (< 4,0,F>, F, .= 0) 
          (< 6,0,A>, A, .= 0) (< 6,0,B>,             B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, 1 + D + F, .* 1) (< 6,0,E>, E, .= 0) (< 6,0,F>, F, .= 0) 
          (< 7,0,A>, A, .= 0) (< 7,0,B>, 1 + B + C + F, .* 1) (< 7,0,C>, C, .= 0) (< 7,0,D>,         D, .= 0) (< 7,0,E>, E, .= 0) (< 7,0,F>, F, .= 0) 
          (< 8,0,A>, A, .= 0) (< 8,0,B>,             B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>,         D, .= 0) (< 8,0,E>, E, .= 0) (< 8,0,F>, F, .= 0) 
          (<10,0,A>, A, .= 0) (<10,0,B>,             B, .= 0) (<10,0,C>, C, .= 0) (<10,0,D>, 1 + D + F, .* 1) (<10,0,E>, E, .= 0) (<10,0,F>, F, .= 0) 
          (<11,0,A>, A, .= 0) (<11,0,B>,     1 + B + F, .* 1) (<11,0,C>, C, .= 0) (<11,0,D>,         D, .= 0) (<11,0,E>, E, .= 0) (<11,0,F>, F, .= 0) 
          (<12,0,A>, A, .= 0) (<12,0,B>,             C, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>,         E, .= 0) (<12,0,E>, E, .= 0) (<12,0,F>, A, .= 0) 
* Step 3: SizeboundsProc WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  start(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)              [0 >= 1 + A && B = C && D = E && F = A]                                       (?,1)
          1.  start(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)              [A >= 0 && C >= 1 + E && B = C && D = E && F = A]                             (?,1)
          2.  start(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A]                                 (?,1)
          3.  start(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && E >= C && B = C && D = E && F = A]                                 (?,1)
          4.  lbl91(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)              [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1)
          6.  lbl91(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A]     (?,1)
          7.  lbl91(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A]     (?,1)
          8.  lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F)              [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1)
          10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A]     (?,1)
          11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A]     (?,1)
          12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)             True                                                                          (1,1)
        Signature:
          {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [0->{},1->{},2->{4,6,7},3->{8,10,11},4->{},6->{4,6,7},7->{8,10,11},8->{},10->{4,6,7},11->{8,10,11},12->{0
          ,1,2,3}]
        Sizebounds:
          (< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,E>, ?) (< 0,0,F>, ?) 
          (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) (< 1,0,E>, ?) (< 1,0,F>, ?) 
          (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 2,0,F>, ?) 
          (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, ?) 
          (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, ?) 
          (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, ?) 
          (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 7,0,F>, ?) 
          (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) 
          (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) 
          (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) 
          (<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) 
    + Applied Processor:
        SizeboundsProc
    + Details:
        Sizebounds computed:
          (< 0,0,A>, A) (< 0,0,B>,             C) (< 0,0,C>, C) (< 0,0,D>,         E) (< 0,0,E>, E) (< 0,0,F>, A) 
          (< 1,0,A>, A) (< 1,0,B>,             C) (< 1,0,C>, C) (< 1,0,D>,         E) (< 1,0,E>, E) (< 1,0,F>, A) 
          (< 2,0,A>, A) (< 2,0,B>,             C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) 
          (< 3,0,A>, A) (< 3,0,B>,     1 + A + C) (< 3,0,C>, C) (< 3,0,D>,         E) (< 3,0,E>, E) (< 3,0,F>, A) 
          (< 4,0,A>, A) (< 4,0,B>,         C + E) (< 4,0,C>, C) (< 4,0,D>, 1 + A + E) (< 4,0,E>, E) (< 4,0,F>, A) 
          (< 6,0,A>, A) (< 6,0,B>,             E) (< 6,0,C>, C) (< 6,0,D>,         E) (< 6,0,E>, E) (< 6,0,F>, A) 
          (< 7,0,A>, A) (< 7,0,B>,         2 + E) (< 7,0,C>, C) (< 7,0,D>,         E) (< 7,0,E>, E) (< 7,0,F>, A) 
          (< 8,0,A>, A) (< 8,0,B>, 2 + A + C + E) (< 8,0,C>, C) (< 8,0,D>,         E) (< 8,0,E>, E) (< 8,0,F>, A) 
          (<10,0,A>, A) (<10,0,B>,             E) (<10,0,C>, C) (<10,0,D>,         E) (<10,0,E>, E) (<10,0,F>, A) 
          (<11,0,A>, A) (<11,0,B>,         2 + E) (<11,0,C>, C) (<11,0,D>,         E) (<11,0,E>, E) (<11,0,F>, A) 
          (<12,0,A>, A) (<12,0,B>,             C) (<12,0,C>, C) (<12,0,D>,         E) (<12,0,E>, E) (<12,0,F>, A) 
* Step 4: LeafRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0.  start(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)              [0 >= 1 + A && B = C && D = E && F = A]                                       (?,1)
          1.  start(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)              [A >= 0 && C >= 1 + E && B = C && D = E && F = A]                             (?,1)
          2.  start(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A]                                 (?,1)
          3.  start(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && E >= C && B = C && D = E && F = A]                                 (?,1)
          4.  lbl91(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)              [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1)
          6.  lbl91(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A]     (?,1)
          7.  lbl91(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A]     (?,1)
          8.  lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F)              [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1)
          10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A]     (?,1)
          11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A]     (?,1)
          12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)             True                                                                          (1,1)
        Signature:
          {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [0->{},1->{},2->{4,6,7},3->{8,10,11},4->{},6->{4,6,7},7->{8,10,11},8->{},10->{4,6,7},11->{8,10,11},12->{0
          ,1,2,3}]
        Sizebounds:
          (< 0,0,A>, A) (< 0,0,B>,             C) (< 0,0,C>, C) (< 0,0,D>,         E) (< 0,0,E>, E) (< 0,0,F>, A) 
          (< 1,0,A>, A) (< 1,0,B>,             C) (< 1,0,C>, C) (< 1,0,D>,         E) (< 1,0,E>, E) (< 1,0,F>, A) 
          (< 2,0,A>, A) (< 2,0,B>,             C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) 
          (< 3,0,A>, A) (< 3,0,B>,     1 + A + C) (< 3,0,C>, C) (< 3,0,D>,         E) (< 3,0,E>, E) (< 3,0,F>, A) 
          (< 4,0,A>, A) (< 4,0,B>,         C + E) (< 4,0,C>, C) (< 4,0,D>, 1 + A + E) (< 4,0,E>, E) (< 4,0,F>, A) 
          (< 6,0,A>, A) (< 6,0,B>,             E) (< 6,0,C>, C) (< 6,0,D>,         E) (< 6,0,E>, E) (< 6,0,F>, A) 
          (< 7,0,A>, A) (< 7,0,B>,         2 + E) (< 7,0,C>, C) (< 7,0,D>,         E) (< 7,0,E>, E) (< 7,0,F>, A) 
          (< 8,0,A>, A) (< 8,0,B>, 2 + A + C + E) (< 8,0,C>, C) (< 8,0,D>,         E) (< 8,0,E>, E) (< 8,0,F>, A) 
          (<10,0,A>, A) (<10,0,B>,             E) (<10,0,C>, C) (<10,0,D>,         E) (<10,0,E>, E) (<10,0,F>, A) 
          (<11,0,A>, A) (<11,0,B>,         2 + E) (<11,0,C>, C) (<11,0,D>,         E) (<11,0,E>, E) (<11,0,F>, A) 
          (<12,0,A>, A) (<12,0,B>,             C) (<12,0,C>, C) (<12,0,D>,         E) (<12,0,E>, E) (<12,0,F>, A) 
    + Applied Processor:
        LeafRules
    + Details:
        The following transitions are estimated by its predecessors and are removed [0,1,4,8]
* Step 5: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          2.  start(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A]                             (?,1)
          3.  start(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && E >= C && B = C && D = E && F = A]                             (?,1)
          6.  lbl91(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1)
          7.  lbl91(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1)
          10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1)
          11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1)
          12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)             True                                                                      (1,1)
        Signature:
          {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [2->{6,7},3->{10,11},6->{6,7},7->{10,11},10->{6,7},11->{10,11},12->{2,3}]
        Sizebounds:
          (< 2,0,A>, A) (< 2,0,B>,         C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) 
          (< 3,0,A>, A) (< 3,0,B>, 1 + A + C) (< 3,0,C>, C) (< 3,0,D>,         E) (< 3,0,E>, E) (< 3,0,F>, A) 
          (< 6,0,A>, A) (< 6,0,B>,         E) (< 6,0,C>, C) (< 6,0,D>,         E) (< 6,0,E>, E) (< 6,0,F>, A) 
          (< 7,0,A>, A) (< 7,0,B>,     2 + E) (< 7,0,C>, C) (< 7,0,D>,         E) (< 7,0,E>, E) (< 7,0,F>, A) 
          (<10,0,A>, A) (<10,0,B>,         E) (<10,0,C>, C) (<10,0,D>,         E) (<10,0,E>, E) (<10,0,F>, A) 
          (<11,0,A>, A) (<11,0,B>,     2 + E) (<11,0,C>, C) (<11,0,D>,         E) (<11,0,E>, E) (<11,0,F>, A) 
          (<12,0,A>, A) (<12,0,B>,         C) (<12,0,C>, C) (<12,0,D>,         E) (<12,0,E>, E) (<12,0,F>, A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(lbl101) = 1 + -1*x2 + x5
           p(lbl91) = -1*x2 + x5    
           p(start) = -1*x2 + x5    
          p(start0) = -1*x3 + x5    
        
        The following rules are strictly oriented:
        [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==>                            
                                                              lbl101(A,B,C,D,E,F)   = 1 + -1*B + E               
                                                                                    > -1*B + E + -1*F            
                                                                                    = lbl101(A,1 + B + F,C,D,E,F)
        
        
        The following rules are weakly oriented:
                                    [A >= 0 && E >= C && B = C && D = E && F = A] ==>                               
                                                               start(A,B,C,D,E,F)   = -1*B + E                      
                                                                                   >= -1*B + E                      
                                                                                    = lbl91(A,B,C,-1 + D + -1*F,E,F)
        
                                    [A >= 0 && E >= C && B = C && D = E && F = A] ==>                               
                                                               start(A,B,C,D,E,F)   = -1*B + E                      
                                                                                   >= -1*B + E + -1*F               
                                                                                    = lbl101(A,1 + B + F,C,D,E,F)   
        
        [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==>                               
                                                               lbl91(A,B,C,D,E,F)   = -1*B + E                      
                                                                                   >= -1*B + E                      
                                                                                    = lbl91(A,B,C,-1 + D + -1*F,E,F)
        
        [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==>                               
                                                               lbl91(A,B,C,D,E,F)   = -1*B + E                      
                                                                                   >= -1*B + E + -1*F               
                                                                                    = lbl101(A,1 + B + F,C,D,E,F)   
        
        [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==>                               
                                                              lbl101(A,B,C,D,E,F)   = 1 + -1*B + E                  
                                                                                   >= -1*B + E                      
                                                                                    = lbl91(A,B,C,-1 + D + -1*F,E,F)
        
                                                                             True ==>                               
                                                              start0(A,B,C,D,E,F)   = -1*C + E                      
                                                                                   >= -1*C + E                      
                                                                                    = start(A,C,C,E,E,A)            
        
        
* Step 6: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          2.  start(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A]                             (?,1)    
          3.  start(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && E >= C && B = C && D = E && F = A]                             (?,1)    
          6.  lbl91(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1)    
          7.  lbl91(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1)    
          10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1)    
          11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1)
          12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)             True                                                                      (1,1)    
        Signature:
          {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [2->{6,7},3->{10,11},6->{6,7},7->{10,11},10->{6,7},11->{10,11},12->{2,3}]
        Sizebounds:
          (< 2,0,A>, A) (< 2,0,B>,         C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) 
          (< 3,0,A>, A) (< 3,0,B>, 1 + A + C) (< 3,0,C>, C) (< 3,0,D>,         E) (< 3,0,E>, E) (< 3,0,F>, A) 
          (< 6,0,A>, A) (< 6,0,B>,         E) (< 6,0,C>, C) (< 6,0,D>,         E) (< 6,0,E>, E) (< 6,0,F>, A) 
          (< 7,0,A>, A) (< 7,0,B>,     2 + E) (< 7,0,C>, C) (< 7,0,D>,         E) (< 7,0,E>, E) (< 7,0,F>, A) 
          (<10,0,A>, A) (<10,0,B>,         E) (<10,0,C>, C) (<10,0,D>,         E) (<10,0,E>, E) (<10,0,F>, A) 
          (<11,0,A>, A) (<11,0,B>,     2 + E) (<11,0,C>, C) (<11,0,D>,         E) (<11,0,E>, E) (<11,0,F>, A) 
          (<12,0,A>, A) (<12,0,B>,         C) (<12,0,C>, C) (<12,0,D>,         E) (<12,0,E>, E) (<12,0,F>, A) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 7: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          2.  start(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A]                             (1,1)    
          3.  start(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && E >= C && B = C && D = E && F = A]                             (1,1)    
          6.  lbl91(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1)    
          7.  lbl91(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1)    
          10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1)    
          11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1)
          12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)             True                                                                      (1,1)    
        Signature:
          {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [2->{6,7},3->{10,11},6->{6,7},7->{10,11},10->{6,7},11->{10,11},12->{2,3}]
        Sizebounds:
          (< 2,0,A>, A) (< 2,0,B>,         C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) 
          (< 3,0,A>, A) (< 3,0,B>, 1 + A + C) (< 3,0,C>, C) (< 3,0,D>,         E) (< 3,0,E>, E) (< 3,0,F>, A) 
          (< 6,0,A>, A) (< 6,0,B>,         E) (< 6,0,C>, C) (< 6,0,D>,         E) (< 6,0,E>, E) (< 6,0,F>, A) 
          (< 7,0,A>, A) (< 7,0,B>,     2 + E) (< 7,0,C>, C) (< 7,0,D>,         E) (< 7,0,E>, E) (< 7,0,F>, A) 
          (<10,0,A>, A) (<10,0,B>,         E) (<10,0,C>, C) (<10,0,D>,         E) (<10,0,E>, E) (<10,0,F>, A) 
          (<11,0,A>, A) (<11,0,B>,     2 + E) (<11,0,C>, C) (<11,0,D>,         E) (<11,0,E>, E) (<11,0,F>, A) 
          (<12,0,A>, A) (<12,0,B>,         C) (<12,0,C>, C) (<12,0,D>,         E) (<12,0,E>, E) (<12,0,F>, A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(lbl101) = 1 + -1*x3 + x4
           p(lbl91) = 1 + -1*x3 + x4
           p(start) = 1 + -1*x3 + x4
          p(start0) = 1 + -1*x3 + x5
        
        The following rules are strictly oriented:
                                    [A >= 0 && E >= C && B = C && D = E && F = A] ==>                               
                                                               start(A,B,C,D,E,F)   = 1 + -1*C + D                  
                                                                                    > -1*C + D + -1*F               
                                                                                    = lbl91(A,B,C,-1 + D + -1*F,E,F)
        
        [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==>                               
                                                              lbl101(A,B,C,D,E,F)   = 1 + -1*C + D                  
                                                                                    > -1*C + D + -1*F               
                                                                                    = lbl91(A,B,C,-1 + D + -1*F,E,F)
        
        
        The following rules are weakly oriented:
                                    [A >= 0 && E >= C && B = C && D = E && F = A] ==>                               
                                                               start(A,B,C,D,E,F)   = 1 + -1*C + D                  
                                                                                   >= 1 + -1*C + D                  
                                                                                    = lbl101(A,1 + B + F,C,D,E,F)   
        
        [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==>                               
                                                               lbl91(A,B,C,D,E,F)   = 1 + -1*C + D                  
                                                                                   >= -1*C + D + -1*F               
                                                                                    = lbl91(A,B,C,-1 + D + -1*F,E,F)
        
        [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==>                               
                                                               lbl91(A,B,C,D,E,F)   = 1 + -1*C + D                  
                                                                                   >= 1 + -1*C + D                  
                                                                                    = lbl101(A,1 + B + F,C,D,E,F)   
        
        [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==>                               
                                                              lbl101(A,B,C,D,E,F)   = 1 + -1*C + D                  
                                                                                   >= 1 + -1*C + D                  
                                                                                    = lbl101(A,1 + B + F,C,D,E,F)   
        
                                                                             True ==>                               
                                                              start0(A,B,C,D,E,F)   = 1 + -1*C + E                  
                                                                                   >= 1 + -1*C + E                  
                                                                                    = start(A,C,C,E,E,A)            
        
        
* Step 8: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          2.  start(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A]                             (1,1)        
          3.  start(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && E >= C && B = C && D = E && F = A]                             (1,1)        
          6.  lbl91(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1)        
          7.  lbl91(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1)        
          10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (1 + C + E,1)
          11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1)    
          12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)             True                                                                      (1,1)        
        Signature:
          {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [2->{6,7},3->{10,11},6->{6,7},7->{10,11},10->{6,7},11->{10,11},12->{2,3}]
        Sizebounds:
          (< 2,0,A>, A) (< 2,0,B>,         C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) 
          (< 3,0,A>, A) (< 3,0,B>, 1 + A + C) (< 3,0,C>, C) (< 3,0,D>,         E) (< 3,0,E>, E) (< 3,0,F>, A) 
          (< 6,0,A>, A) (< 6,0,B>,         E) (< 6,0,C>, C) (< 6,0,D>,         E) (< 6,0,E>, E) (< 6,0,F>, A) 
          (< 7,0,A>, A) (< 7,0,B>,     2 + E) (< 7,0,C>, C) (< 7,0,D>,         E) (< 7,0,E>, E) (< 7,0,F>, A) 
          (<10,0,A>, A) (<10,0,B>,         E) (<10,0,C>, C) (<10,0,D>,         E) (<10,0,E>, E) (<10,0,F>, A) 
          (<11,0,A>, A) (<11,0,B>,     2 + E) (<11,0,C>, C) (<11,0,D>,         E) (<11,0,E>, E) (<11,0,F>, A) 
          (<12,0,A>, A) (<12,0,B>,         C) (<12,0,C>, C) (<12,0,D>,         E) (<12,0,E>, E) (<12,0,F>, A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(lbl101) = 1 + -1*x2 + x5        
           p(lbl91) = 1 + -1*x1 + -1*x2 + x5
           p(start) = 1 + -1*x3 + x5        
          p(start0) = 1 + -1*x3 + x5        
        
        The following rules are strictly oriented:
                                    [A >= 0 && E >= C && B = C && D = E && F = A] ==>                            
                                                               start(A,B,C,D,E,F)   = 1 + -1*C + E               
                                                                                    > -1*B + E + -1*F            
                                                                                    = lbl101(A,1 + B + F,C,D,E,F)
        
        [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==>                            
                                                               lbl91(A,B,C,D,E,F)   = 1 + -1*A + -1*B + E        
                                                                                    > -1*B + E + -1*F            
                                                                                    = lbl101(A,1 + B + F,C,D,E,F)
        
        [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==>                            
                                                              lbl101(A,B,C,D,E,F)   = 1 + -1*B + E               
                                                                                    > -1*B + E + -1*F            
                                                                                    = lbl101(A,1 + B + F,C,D,E,F)
        
        
        The following rules are weakly oriented:
                                    [A >= 0 && E >= C && B = C && D = E && F = A] ==>                               
                                                               start(A,B,C,D,E,F)   = 1 + -1*C + E                  
                                                                                   >= 1 + -1*A + -1*B + E           
                                                                                    = lbl91(A,B,C,-1 + D + -1*F,E,F)
        
        [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==>                               
                                                               lbl91(A,B,C,D,E,F)   = 1 + -1*A + -1*B + E           
                                                                                   >= 1 + -1*A + -1*B + E           
                                                                                    = lbl91(A,B,C,-1 + D + -1*F,E,F)
        
        [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==>                               
                                                              lbl101(A,B,C,D,E,F)   = 1 + -1*B + E                  
                                                                                   >= 1 + -1*A + -1*B + E           
                                                                                    = lbl91(A,B,C,-1 + D + -1*F,E,F)
        
                                                                             True ==>                               
                                                              start0(A,B,C,D,E,F)   = 1 + -1*C + E                  
                                                                                   >= 1 + -1*C + E                  
                                                                                    = start(A,C,C,E,E,A)            
        
        
* Step 9: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          2.  start(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A]                             (1,1)        
          3.  start(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && E >= C && B = C && D = E && F = A]                             (1,1)        
          6.  lbl91(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1)        
          7.  lbl91(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (1 + C + E,1)
          10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (1 + C + E,1)
          11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1)    
          12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)             True                                                                      (1,1)        
        Signature:
          {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [2->{6,7},3->{10,11},6->{6,7},7->{10,11},10->{6,7},11->{10,11},12->{2,3}]
        Sizebounds:
          (< 2,0,A>, A) (< 2,0,B>,         C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) 
          (< 3,0,A>, A) (< 3,0,B>, 1 + A + C) (< 3,0,C>, C) (< 3,0,D>,         E) (< 3,0,E>, E) (< 3,0,F>, A) 
          (< 6,0,A>, A) (< 6,0,B>,         E) (< 6,0,C>, C) (< 6,0,D>,         E) (< 6,0,E>, E) (< 6,0,F>, A) 
          (< 7,0,A>, A) (< 7,0,B>,     2 + E) (< 7,0,C>, C) (< 7,0,D>,         E) (< 7,0,E>, E) (< 7,0,F>, A) 
          (<10,0,A>, A) (<10,0,B>,         E) (<10,0,C>, C) (<10,0,D>,         E) (<10,0,E>, E) (<10,0,F>, A) 
          (<11,0,A>, A) (<11,0,B>,     2 + E) (<11,0,C>, C) (<11,0,D>,         E) (<11,0,E>, E) (<11,0,F>, A) 
          (<12,0,A>, A) (<12,0,B>,         C) (<12,0,C>, C) (<12,0,D>,         E) (<12,0,E>, E) (<12,0,F>, A) 
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(lbl101) = -1*x3 + x4    
           p(lbl91) = 1 + -1*x3 + x4
           p(start) = -1*x3 + x4    
          p(start0) = -1*x3 + x5    
        
        The following rules are strictly oriented:
        [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==>                               
                                                               lbl91(A,B,C,D,E,F)   = 1 + -1*C + D                  
                                                                                    > -1*C + D + -1*F               
                                                                                    = lbl91(A,B,C,-1 + D + -1*F,E,F)
        
        [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==>                               
                                                               lbl91(A,B,C,D,E,F)   = 1 + -1*C + D                  
                                                                                    > -1*C + D                      
                                                                                    = lbl101(A,1 + B + F,C,D,E,F)   
        
        
        The following rules are weakly oriented:
                                    [A >= 0 && E >= C && B = C && D = E && F = A] ==>                               
                                                               start(A,B,C,D,E,F)   = -1*C + D                      
                                                                                   >= -1*C + D + -1*F               
                                                                                    = lbl91(A,B,C,-1 + D + -1*F,E,F)
        
                                    [A >= 0 && E >= C && B = C && D = E && F = A] ==>                               
                                                               start(A,B,C,D,E,F)   = -1*C + D                      
                                                                                   >= -1*C + D                      
                                                                                    = lbl101(A,1 + B + F,C,D,E,F)   
        
        [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==>                               
                                                              lbl101(A,B,C,D,E,F)   = -1*C + D                      
                                                                                   >= -1*C + D + -1*F               
                                                                                    = lbl91(A,B,C,-1 + D + -1*F,E,F)
        
        [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==>                               
                                                              lbl101(A,B,C,D,E,F)   = -1*C + D                      
                                                                                   >= -1*C + D                      
                                                                                    = lbl101(A,1 + B + F,C,D,E,F)   
        
                                                                             True ==>                               
                                                              start0(A,B,C,D,E,F)   = -1*C + E                      
                                                                                   >= -1*C + E                      
                                                                                    = start(A,C,C,E,E,A)            
        
        
* Step 10: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          2.  start(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A]                             (1,1)        
          3.  start(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && E >= C && B = C && D = E && F = A]                             (1,1)        
          6.  lbl91(A,B,C,D,E,F)  -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (C + E,1)    
          7.  lbl91(A,B,C,D,E,F)  -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (C + E,1)    
          10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (1 + C + E,1)
          11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F)    [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1)    
          12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)             True                                                                      (1,1)        
        Signature:
          {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [2->{6,7},3->{10,11},6->{6,7},7->{10,11},10->{6,7},11->{10,11},12->{2,3}]
        Sizebounds:
          (< 2,0,A>, A) (< 2,0,B>,         C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) 
          (< 3,0,A>, A) (< 3,0,B>, 1 + A + C) (< 3,0,C>, C) (< 3,0,D>,         E) (< 3,0,E>, E) (< 3,0,F>, A) 
          (< 6,0,A>, A) (< 6,0,B>,         E) (< 6,0,C>, C) (< 6,0,D>,         E) (< 6,0,E>, E) (< 6,0,F>, A) 
          (< 7,0,A>, A) (< 7,0,B>,     2 + E) (< 7,0,C>, C) (< 7,0,D>,         E) (< 7,0,E>, E) (< 7,0,F>, A) 
          (<10,0,A>, A) (<10,0,B>,         E) (<10,0,C>, C) (<10,0,D>,         E) (<10,0,E>, E) (<10,0,F>, A) 
          (<11,0,A>, A) (<11,0,B>,     2 + E) (<11,0,C>, C) (<11,0,D>,         E) (<11,0,E>, E) (<11,0,F>, A) 
          (<12,0,A>, A) (<12,0,B>,         C) (<12,0,C>, C) (<12,0,D>,         E) (<12,0,E>, E) (<12,0,F>, A) 
    + Applied Processor:
        KnowledgePropagation
    + Details:
        The problem is already solved.

WORST_CASE(?,O(n^1))