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

YES