YES
* Step 1: UnsatRules YES
    + Considered Problem:
        Rules:
          0.  f0(A,B,C,D,E,F,G)  -> f5(0,B,C,D,E,F,G)            True                     (1,1)
          1.  f5(A,B,C,D,E,F,G)  -> f5(1 + A,B,C,D,E,F,G)        [99 >= A]                (?,1)
          2.  f17(A,B,C,D,E,F,G) -> f17(A,B,C,D,E,F,G)           True                     (?,1)
          3.  f17(A,B,C,D,E,F,G) -> f17(A,1 + B,C,D,E,F,G)       [0 >= 1 + H]             (?,1)
          4.  f17(A,B,C,D,E,F,G) -> f17(A,1 + B,C,D,E,F,G)       True                     (?,1)
          5.  f32(A,B,C,D,E,F,G) -> f32(A,B,C,D,E,F,G)           True                     (?,1)
          6.  f32(A,B,C,D,E,F,G) -> f32(A,B,1 + C,D,E,F,G)       [0 >= 1 + H]             (?,1)
          7.  f32(A,B,C,D,E,F,G) -> f32(A,B,1 + C,D,E,F,G)       True                     (?,1)
          8.  f32(A,B,C,D,E,F,G) -> f13(A,B,C,C,C,F,G)           True                     (?,1)
          9.  f17(A,B,C,D,E,F,G) -> f32(A,B,B,B,E,B,H)           [0 >= 1 + I]             (?,1)
          10. f17(A,B,C,D,E,F,G) -> f32(A,B,B,B,E,B,H)           True                     (?,1)
          11. f17(A,B,C,D,E,F,G) -> f13(A,B,C,B,E,B,H)           True                     (?,1)
          12. f5(A,B,C,D,E,F,G)  -> f13(A,B,C,-2 + A,E,F,G)      [A >= 100]               (?,1)
          13. f5(A,B,C,D,E,F,G)  -> f17(A,-2 + A,C,-2 + A,E,F,G) [0 >= 1 + A && A >= 100] (?,1)
        Signature:
          {(f0,7);(f13,7);(f17,7);(f32,7);(f5,7)}
        Flow Graph:
          [0->{1,12,13},1->{1,12,13},2->{2,3,4,9,10,11},3->{2,3,4,9,10,11},4->{2,3,4,9,10,11},5->{5,6,7,8},6->{5,6,7
          ,8},7->{5,6,7,8},8->{},9->{5,6,7,8},10->{5,6,7,8},11->{},12->{},13->{2,3,4,9,10,11}]
        
    + Applied Processor:
        UnsatRules
    + Details:
        Following transitions have unsatisfiable constraints and are removed:  [13]
* Step 2: UnsatPaths YES
    + Considered Problem:
        Rules:
          0.  f0(A,B,C,D,E,F,G)  -> f5(0,B,C,D,E,F,G)       True         (1,1)
          1.  f5(A,B,C,D,E,F,G)  -> f5(1 + A,B,C,D,E,F,G)   [99 >= A]    (?,1)
          2.  f17(A,B,C,D,E,F,G) -> f17(A,B,C,D,E,F,G)      True         (?,1)
          3.  f17(A,B,C,D,E,F,G) -> f17(A,1 + B,C,D,E,F,G)  [0 >= 1 + H] (?,1)
          4.  f17(A,B,C,D,E,F,G) -> f17(A,1 + B,C,D,E,F,G)  True         (?,1)
          5.  f32(A,B,C,D,E,F,G) -> f32(A,B,C,D,E,F,G)      True         (?,1)
          6.  f32(A,B,C,D,E,F,G) -> f32(A,B,1 + C,D,E,F,G)  [0 >= 1 + H] (?,1)
          7.  f32(A,B,C,D,E,F,G) -> f32(A,B,1 + C,D,E,F,G)  True         (?,1)
          8.  f32(A,B,C,D,E,F,G) -> f13(A,B,C,C,C,F,G)      True         (?,1)
          9.  f17(A,B,C,D,E,F,G) -> f32(A,B,B,B,E,B,H)      [0 >= 1 + I] (?,1)
          10. f17(A,B,C,D,E,F,G) -> f32(A,B,B,B,E,B,H)      True         (?,1)
          11. f17(A,B,C,D,E,F,G) -> f13(A,B,C,B,E,B,H)      True         (?,1)
          12. f5(A,B,C,D,E,F,G)  -> f13(A,B,C,-2 + A,E,F,G) [A >= 100]   (?,1)
        Signature:
          {(f0,7);(f13,7);(f17,7);(f32,7);(f5,7)}
        Flow Graph:
          [0->{1,12},1->{1,12},2->{2,3,4,9,10,11},3->{2,3,4,9,10,11},4->{2,3,4,9,10,11},5->{5,6,7,8},6->{5,6,7,8}
          ,7->{5,6,7,8},8->{},9->{5,6,7,8},10->{5,6,7,8},11->{},12->{}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(0,12)]
* Step 3: UnreachableRules YES
    + Considered Problem:
        Rules:
          0.  f0(A,B,C,D,E,F,G)  -> f5(0,B,C,D,E,F,G)       True         (1,1)
          1.  f5(A,B,C,D,E,F,G)  -> f5(1 + A,B,C,D,E,F,G)   [99 >= A]    (?,1)
          2.  f17(A,B,C,D,E,F,G) -> f17(A,B,C,D,E,F,G)      True         (?,1)
          3.  f17(A,B,C,D,E,F,G) -> f17(A,1 + B,C,D,E,F,G)  [0 >= 1 + H] (?,1)
          4.  f17(A,B,C,D,E,F,G) -> f17(A,1 + B,C,D,E,F,G)  True         (?,1)
          5.  f32(A,B,C,D,E,F,G) -> f32(A,B,C,D,E,F,G)      True         (?,1)
          6.  f32(A,B,C,D,E,F,G) -> f32(A,B,1 + C,D,E,F,G)  [0 >= 1 + H] (?,1)
          7.  f32(A,B,C,D,E,F,G) -> f32(A,B,1 + C,D,E,F,G)  True         (?,1)
          8.  f32(A,B,C,D,E,F,G) -> f13(A,B,C,C,C,F,G)      True         (?,1)
          9.  f17(A,B,C,D,E,F,G) -> f32(A,B,B,B,E,B,H)      [0 >= 1 + I] (?,1)
          10. f17(A,B,C,D,E,F,G) -> f32(A,B,B,B,E,B,H)      True         (?,1)
          11. f17(A,B,C,D,E,F,G) -> f13(A,B,C,B,E,B,H)      True         (?,1)
          12. f5(A,B,C,D,E,F,G)  -> f13(A,B,C,-2 + A,E,F,G) [A >= 100]   (?,1)
        Signature:
          {(f0,7);(f13,7);(f17,7);(f32,7);(f5,7)}
        Flow Graph:
          [0->{1},1->{1,12},2->{2,3,4,9,10,11},3->{2,3,4,9,10,11},4->{2,3,4,9,10,11},5->{5,6,7,8},6->{5,6,7,8},7->{5
          ,6,7,8},8->{},9->{5,6,7,8},10->{5,6,7,8},11->{},12->{}]
        
    + Applied Processor:
        UnreachableRules
    + Details:
        Following transitions are not reachable from the starting states and are revomed: [2,3,4,5,6,7,8,9,10,11]
* Step 4: FromIts YES
    + Considered Problem:
        Rules:
          0.  f0(A,B,C,D,E,F,G) -> f5(0,B,C,D,E,F,G)       True       (1,1)
          1.  f5(A,B,C,D,E,F,G) -> f5(1 + A,B,C,D,E,F,G)   [99 >= A]  (?,1)
          12. f5(A,B,C,D,E,F,G) -> f13(A,B,C,-2 + A,E,F,G) [A >= 100] (?,1)
        Signature:
          {(f0,7);(f13,7);(f17,7);(f32,7);(f5,7)}
        Flow Graph:
          [0->{1},1->{1,12},12->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 5: Decompose YES
    + Considered Problem:
        Rules:
          f0(A,B,C,D,E,F,G) -> f5(0,B,C,D,E,F,G)        True
          f5(A,B,C,D,E,F,G) -> f5(1 + A,B,C,D,E,F,G)    [99 >= A]
          f5(A,B,C,D,E,F,G) -> f13(A,B,C,-2 + A,E,F,G)  [A >= 100]
        Signature:
          {(f0,7);(f13,7);(f17,7);(f32,7);(f5,7)}
        Rule Graph:
          [0->{1},1->{1,12},12->{}]
    + Applied Processor:
        Decompose NoGreedy
    + Details:
        We construct a looptree:
          P: [0,1,12]
          |
          `- p:[1] c: [1]
* Step 6: CloseWith YES
    + Considered Problem:
        (Rules:
          f0(A,B,C,D,E,F,G) -> f5(0,B,C,D,E,F,G)        True
          f5(A,B,C,D,E,F,G) -> f5(1 + A,B,C,D,E,F,G)    [99 >= A]
          f5(A,B,C,D,E,F,G) -> f13(A,B,C,-2 + A,E,F,G)  [A >= 100]
        Signature:
          {(f0,7);(f13,7);(f17,7);(f32,7);(f5,7)}
        Rule Graph:
          [0->{1},1->{1,12},12->{}]
        ,We construct a looptree:
          P: [0,1,12]
          |
          `- p:[1] c: [1])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES