NO
* Step 1: FromIts NO
    + Considered Problem:
        Rules:
          0.  f4(A,B,C,D,E,F)  -> f14(A,B,C,D,E,F)      [0 >= A]                         (?,1)
          1.  f13(A,B,C,D,E,F) -> f4(A,B,C,D,E,F)       True                             (?,1)
          2.  f13(A,B,C,D,E,F) -> f400(A,B,C,D,E,F)     [B >= 1 + A]                     (?,1)
          3.  f2(A,B,C,D,E,F)  -> f23(G,I,H,J,1,F)      [G >= 1 && H >= 1 && 0 >= I]     (1,1)
          4.  f2(A,B,C,D,E,F)  -> f23(G,I,H,J,1,0)      [G >= 1 && H >= 1 && I >= 1]     (1,1)
          5.  f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,F)       [E >= C]                         (?,1)
          6.  f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,1)       [C >= 1 + E]                     (?,1)
          7.  f4(A,B,C,D,E,F)  -> f33(-1 + A,B,H,J,C,F) [H >= C && 0 >= B && A >= 1]     (?,1)
          8.  f4(A,B,C,D,E,F)  -> f33(-1 + A,B,H,J,C,0) [H >= C && B >= 1 && A >= 1]     (?,1)
          9.  f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,F)       [E >= C]                         (?,1)
          10. f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,1)       [C >= 1 + E]                     (?,1)
          11. f6(A,B,C,D,E,F)  -> f43(A,B,H,J,C,F)      [H >= C && 0 >= C && 0 >= B]     (?,1)
          12. f6(A,B,C,D,E,F)  -> f43(A,B,H,J,C,0)      [H >= C && 0 >= C && B >= 1]     (?,1)
          13. f43(A,B,C,D,E,F) -> f6(A,B,C,D,C,F)       [C = E]                          (?,1)
          14. f43(A,B,C,D,E,F) -> f6(A,B,C,D,E,1)       [C >= 1 + E]                     (?,1)
          15. f6(A,B,C,D,E,F)  -> f53(A,B,H,J,-1 + C,F) [1 + H >= C && C >= 1 && 0 >= B] (?,1)
          16. f6(A,B,C,D,E,F)  -> f53(A,B,H,J,-1 + C,0) [1 + H >= C && C >= 1 && B >= 1] (?,1)
          17. f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,F)      [E >= C]                         (?,1)
          18. f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,1)      [C >= 1 + E]                     (?,1)
          19. f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,F)      [0 >= B && H >= E]               (?,1)
          20. f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,0)      [B >= 1 && H >= E]               (?,1)
          21. f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,F)  [E >= C]                         (?,1)
          22. f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,1)  [C >= 1 + E]                     (?,1)
          23. f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,F)      [0 >= B && H >= E]               (?,1)
          24. f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,0)      [B >= 1 && H >= E]               (?,1)
          25. f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,F)      [E >= C]                         (?,1)
          26. f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,1)      [C >= 1 + E]                     (?,1)
        Signature:
          {(f13,6)
          ;(f14,6)
          ;(f2,6)
          ;(f23,6)
          ;(f33,6)
          ;(f4,6)
          ;(f400,6)
          ;(f43,6)
          ;(f53,6)
          ;(f6,6)
          ;(f61,6)
          ;(f63,6)
          ;(f71,6)
          ;(f73,6)}
        Flow Graph:
          [0->{},1->{0,7,8},2->{},3->{5,6},4->{5,6},5->{0,7,8},6->{0,7,8},7->{9,10},8->{9,10},9->{11,12,15,16}
          ,10->{11,12,15,16},11->{13,14},12->{13,14},13->{11,12,15,16},14->{11,12,15,16},15->{17,18},16->{17,18}
          ,17->{19,20},18->{19,20},19->{21,22},20->{21,22},21->{23,24},22->{23,24},23->{25,26},24->{25,26},25->{1,2}
          ,26->{1,2}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 2: CloseWith NO
    + Considered Problem:
        Rules:
          f4(A,B,C,D,E,F)  -> f14(A,B,C,D,E,F)       [0 >= A]
          f13(A,B,C,D,E,F) -> f4(A,B,C,D,E,F)        True
          f13(A,B,C,D,E,F) -> f400(A,B,C,D,E,F)      [B >= 1 + A]
          f2(A,B,C,D,E,F)  -> f23(G,I,H,J,1,F)       [G >= 1 && H >= 1 && 0 >= I]
          f2(A,B,C,D,E,F)  -> f23(G,I,H,J,1,0)       [G >= 1 && H >= 1 && I >= 1]
          f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,F)        [E >= C]
          f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,1)        [C >= 1 + E]
          f4(A,B,C,D,E,F)  -> f33(-1 + A,B,H,J,C,F)  [H >= C && 0 >= B && A >= 1]
          f4(A,B,C,D,E,F)  -> f33(-1 + A,B,H,J,C,0)  [H >= C && B >= 1 && A >= 1]
          f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,F)        [E >= C]
          f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,1)        [C >= 1 + E]
          f6(A,B,C,D,E,F)  -> f43(A,B,H,J,C,F)       [H >= C && 0 >= C && 0 >= B]
          f6(A,B,C,D,E,F)  -> f43(A,B,H,J,C,0)       [H >= C && 0 >= C && B >= 1]
          f43(A,B,C,D,E,F) -> f6(A,B,C,D,C,F)        [C = E]
          f43(A,B,C,D,E,F) -> f6(A,B,C,D,E,1)        [C >= 1 + E]
          f6(A,B,C,D,E,F)  -> f53(A,B,H,J,-1 + C,F)  [1 + H >= C && C >= 1 && 0 >= B]
          f6(A,B,C,D,E,F)  -> f53(A,B,H,J,-1 + C,0)  [1 + H >= C && C >= 1 && B >= 1]
          f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,F)       [E >= C]
          f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,1)       [C >= 1 + E]
          f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,F)       [0 >= B && H >= E]
          f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,0)       [B >= 1 && H >= E]
          f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,F)   [E >= C]
          f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,1)   [C >= 1 + E]
          f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,F)       [0 >= B && H >= E]
          f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,0)       [B >= 1 && H >= E]
          f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,F)       [E >= C]
          f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,1)       [C >= 1 + E]
        Signature:
          {(f13,6)
          ;(f14,6)
          ;(f2,6)
          ;(f23,6)
          ;(f33,6)
          ;(f4,6)
          ;(f400,6)
          ;(f43,6)
          ;(f53,6)
          ;(f6,6)
          ;(f61,6)
          ;(f63,6)
          ;(f71,6)
          ;(f73,6)}
        Rule Graph:
          [0->{},1->{0,7,8},2->{},3->{5,6},4->{5,6},5->{0,7,8},6->{0,7,8},7->{9,10},8->{9,10},9->{11,12,15,16}
          ,10->{11,12,15,16},11->{13,14},12->{13,14},13->{11,12,15,16},14->{11,12,15,16},15->{17,18},16->{17,18}
          ,17->{19,20},18->{19,20},19->{21,22},20->{21,22},21->{23,24},22->{23,24},23->{25,26},24->{25,26},25->{1,2}
          ,26->{1,2}]
    + Applied Processor:
        CloseWith False
    + Details:
        ()

NO