NO
* Step 1: FromIts NO
    + Considered Problem:
        Rules:
          0.  f0(A,B,C,D,E,F)  -> f12(G,G,G,0,E,F)     True                                    (1,1)
          1.  f12(A,B,C,D,E,F) -> f12(A,B,C,1 + D,G,F) [D >= 0 && C >= 1 + D]                  (?,1)
          2.  f27(A,B,C,D,E,F) -> f27(A,B,C,D,E,G)     [D >= 0 && -1*C + D >= 0 && 0 >= 1 + H] (?,1)
          3.  f27(A,B,C,D,E,F) -> f27(A,B,C,D,E,G)     [D >= 0 && -1*C + D >= 0]               (?,1)
          4.  f42(A,B,C,D,E,F) -> f42(A,B,C,D,E,F)     [D >= 0 && -1*C + D >= 0 && G >= 1 + H] (?,1)
          5.  f42(A,B,C,D,E,F) -> f42(A,B,C,D,E,F)     [D >= 0 && -1*C + D >= 0]               (?,1)
          6.  f55(A,B,C,D,E,F) -> f55(A,B,C,D,E,F)     [D >= 0 && -1*C + D >= 0 && G >= 1 + H] (?,1)
          7.  f55(A,B,C,D,E,F) -> f55(A,B,C,D,E,F)     [D >= 0 && -1*C + D >= 0]               (?,1)
          8.  f55(A,B,C,D,E,F) -> f66(A,B,C,D,E,F)     [D >= 0 && -1*C + D >= 0]               (?,1)
          9.  f42(A,B,C,D,E,F) -> f55(A,B,C,D,E,F)     [D >= 0 && -1*C + D >= 0]               (?,1)
          10. f27(A,B,C,D,E,F) -> f42(A,B,C,D,E,F)     [D >= 0 && -1*C + D >= 0]               (?,1)
          11. f12(A,B,C,D,E,F) -> f27(A,B,C,D,E,F)     [D >= 0 && D >= C]                      (?,1)
        Signature:
          {(f0,6);(f12,6);(f27,6);(f42,6);(f55,6);(f66,6)}
        Flow Graph:
          [0->{1,11},1->{1,11},2->{2,3,10},3->{2,3,10},4->{4,5,9},5->{4,5,9},6->{6,7,8},7->{6,7,8},8->{},9->{6,7,8}
          ,10->{4,5,9},11->{2,3,10}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 2: CloseWith NO
    + Considered Problem:
        Rules:
          f0(A,B,C,D,E,F)  -> f12(G,G,G,0,E,F)      True
          f12(A,B,C,D,E,F) -> f12(A,B,C,1 + D,G,F)  [D >= 0 && C >= 1 + D]
          f27(A,B,C,D,E,F) -> f27(A,B,C,D,E,G)      [D >= 0 && -1*C + D >= 0 && 0 >= 1 + H]
          f27(A,B,C,D,E,F) -> f27(A,B,C,D,E,G)      [D >= 0 && -1*C + D >= 0]
          f42(A,B,C,D,E,F) -> f42(A,B,C,D,E,F)      [D >= 0 && -1*C + D >= 0 && G >= 1 + H]
          f42(A,B,C,D,E,F) -> f42(A,B,C,D,E,F)      [D >= 0 && -1*C + D >= 0]
          f55(A,B,C,D,E,F) -> f55(A,B,C,D,E,F)      [D >= 0 && -1*C + D >= 0 && G >= 1 + H]
          f55(A,B,C,D,E,F) -> f55(A,B,C,D,E,F)      [D >= 0 && -1*C + D >= 0]
          f55(A,B,C,D,E,F) -> f66(A,B,C,D,E,F)      [D >= 0 && -1*C + D >= 0]
          f42(A,B,C,D,E,F) -> f55(A,B,C,D,E,F)      [D >= 0 && -1*C + D >= 0]
          f27(A,B,C,D,E,F) -> f42(A,B,C,D,E,F)      [D >= 0 && -1*C + D >= 0]
          f12(A,B,C,D,E,F) -> f27(A,B,C,D,E,F)      [D >= 0 && D >= C]
        Signature:
          {(f0,6);(f12,6);(f27,6);(f42,6);(f55,6);(f66,6)}
        Rule Graph:
          [0->{1,11},1->{1,11},2->{2,3,10},3->{2,3,10},4->{4,5,9},5->{4,5,9},6->{6,7,8},7->{6,7,8},8->{},9->{6,7,8}
          ,10->{4,5,9},11->{2,3,10}]
    + Applied Processor:
        CloseWith False
    + Details:
        ()

NO