YES
* Step 1: UnsatRules YES
    + Considered Problem:
        Rules:
          0. start(A,B,C,D,E,F)  -> stop(A,B,C,F,E,F)       [0 >= A && B = C && D = E && F = A]                           (?,1)
          1. start(A,B,C,D,E,F)  -> lbl62(A,-1 + F,C,F,E,F) [A >= 1 && B = C && D = E && F = A]                           (?,1)
          2. lbl72(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)       [A >= 1 && D = 0 && B = 0 && F = A]                           (?,1)
          3. lbl72(A,B,C,D,E,F)  -> lbl72(A,F,C,-1 + D,E,F) [D >= 1 && 0 >= A && D >= 0 && A >= 1 + D && B = 0 && F = A]  (?,1)
          4. lbl72(A,B,C,D,E,F)  -> lbl62(A,-1 + F,C,D,E,F) [A >= 1 && D >= 1 && D >= 0 && A >= 1 + D && B = 0 && F = A]  (?,1)
          5. lbl62(A,B,C,D,E,F)  -> lbl72(A,B,C,-1 + D,E,F) [A >= D && A >= 1 && D >= 1 && B = 0 && F = A]                (?,1)
          6. lbl62(A,B,C,D,E,F)  -> lbl62(A,-1 + B,C,D,E,F) [B >= 1 && A >= D && A >= 1 + B && B >= 0 && D >= 1 && F = A] (?,1)
          7. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)      True                                                          (1,1)
        Signature:
          {(lbl62,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [0->{},1->{5,6},2->{},3->{2,3,4},4->{5,6},5->{2,3,4},6->{5,6},7->{0,1}]
        
    + Applied Processor:
        UnsatRules
    + Details:
        Following transitions have unsatisfiable constraints and are removed:  [3]
* Step 2: UnsatPaths YES
    + Considered Problem:
        Rules:
          0. start(A,B,C,D,E,F)  -> stop(A,B,C,F,E,F)       [0 >= A && B = C && D = E && F = A]                           (?,1)
          1. start(A,B,C,D,E,F)  -> lbl62(A,-1 + F,C,F,E,F) [A >= 1 && B = C && D = E && F = A]                           (?,1)
          2. lbl72(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)       [A >= 1 && D = 0 && B = 0 && F = A]                           (?,1)
          4. lbl72(A,B,C,D,E,F)  -> lbl62(A,-1 + F,C,D,E,F) [A >= 1 && D >= 1 && D >= 0 && A >= 1 + D && B = 0 && F = A]  (?,1)
          5. lbl62(A,B,C,D,E,F)  -> lbl72(A,B,C,-1 + D,E,F) [A >= D && A >= 1 && D >= 1 && B = 0 && F = A]                (?,1)
          6. lbl62(A,B,C,D,E,F)  -> lbl62(A,-1 + B,C,D,E,F) [B >= 1 && A >= D && A >= 1 + B && B >= 0 && D >= 1 && F = A] (?,1)
          7. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)      True                                                          (1,1)
        Signature:
          {(lbl62,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [0->{},1->{5,6},2->{},4->{5,6},5->{2,4},6->{5,6},7->{0,1}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(4,5)]
* Step 3: FromIts YES
    + Considered Problem:
        Rules:
          0. start(A,B,C,D,E,F)  -> stop(A,B,C,F,E,F)       [0 >= A && B = C && D = E && F = A]                           (?,1)
          1. start(A,B,C,D,E,F)  -> lbl62(A,-1 + F,C,F,E,F) [A >= 1 && B = C && D = E && F = A]                           (?,1)
          2. lbl72(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)       [A >= 1 && D = 0 && B = 0 && F = A]                           (?,1)
          4. lbl72(A,B,C,D,E,F)  -> lbl62(A,-1 + F,C,D,E,F) [A >= 1 && D >= 1 && D >= 0 && A >= 1 + D && B = 0 && F = A]  (?,1)
          5. lbl62(A,B,C,D,E,F)  -> lbl72(A,B,C,-1 + D,E,F) [A >= D && A >= 1 && D >= 1 && B = 0 && F = A]                (?,1)
          6. lbl62(A,B,C,D,E,F)  -> lbl62(A,-1 + B,C,D,E,F) [B >= 1 && A >= D && A >= 1 + B && B >= 0 && D >= 1 && F = A] (?,1)
          7. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)      True                                                          (1,1)
        Signature:
          {(lbl62,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Flow Graph:
          [0->{},1->{5,6},2->{},4->{6},5->{2,4},6->{5,6},7->{0,1}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 4: Decompose YES
    + Considered Problem:
        Rules:
          start(A,B,C,D,E,F)  -> stop(A,B,C,F,E,F)        [0 >= A && B = C && D = E && F = A]
          start(A,B,C,D,E,F)  -> lbl62(A,-1 + F,C,F,E,F)  [A >= 1 && B = C && D = E && F = A]
          lbl72(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)        [A >= 1 && D = 0 && B = 0 && F = A]
          lbl72(A,B,C,D,E,F)  -> lbl62(A,-1 + F,C,D,E,F)  [A >= 1 && D >= 1 && D >= 0 && A >= 1 + D && B = 0 && F = A]
          lbl62(A,B,C,D,E,F)  -> lbl72(A,B,C,-1 + D,E,F)  [A >= D && A >= 1 && D >= 1 && B = 0 && F = A]
          lbl62(A,B,C,D,E,F)  -> lbl62(A,-1 + B,C,D,E,F)  [B >= 1
                                                           && A >= D
                                                           && A >= 1 + B
                                                           && B >= 0
                                                           && D >= 1
                                                           && F = A]
          start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)       True
        Signature:
          {(lbl62,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Rule Graph:
          [0->{},1->{5,6},2->{},4->{6},5->{2,4},6->{5,6},7->{0,1}]
    + Applied Processor:
        Decompose NoGreedy
    + Details:
        We construct a looptree:
          P: [0,1,2,4,5,6,7]
          |
          `- p:[5,6,4] c: [4,5]
             |
             `- p:[6] c: [6]
* Step 5: CloseWith YES
    + Considered Problem:
        (Rules:
          start(A,B,C,D,E,F)  -> stop(A,B,C,F,E,F)        [0 >= A && B = C && D = E && F = A]
          start(A,B,C,D,E,F)  -> lbl62(A,-1 + F,C,F,E,F)  [A >= 1 && B = C && D = E && F = A]
          lbl72(A,B,C,D,E,F)  -> stop(A,B,C,D,E,F)        [A >= 1 && D = 0 && B = 0 && F = A]
          lbl72(A,B,C,D,E,F)  -> lbl62(A,-1 + F,C,D,E,F)  [A >= 1 && D >= 1 && D >= 0 && A >= 1 + D && B = 0 && F = A]
          lbl62(A,B,C,D,E,F)  -> lbl72(A,B,C,-1 + D,E,F)  [A >= D && A >= 1 && D >= 1 && B = 0 && F = A]
          lbl62(A,B,C,D,E,F)  -> lbl62(A,-1 + B,C,D,E,F)  [B >= 1
                                                           && A >= D
                                                           && A >= 1 + B
                                                           && B >= 0
                                                           && D >= 1
                                                           && F = A]
          start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A)       True
        Signature:
          {(lbl62,6);(lbl72,6);(start,6);(start0,6);(stop,6)}
        Rule Graph:
          [0->{},1->{5,6},2->{},4->{6},5->{2,4},6->{5,6},7->{0,1}]
        ,We construct a looptree:
          P: [0,1,2,4,5,6,7]
          |
          `- p:[5,6,4] c: [4,5]
             |
             `- p:[6] c: [6])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES