NO
* Step 1: UnsatPaths NO
    + Considered Problem:
        Rules:
          0. f1(A,B,C,D) -> f300(A,B,C,E)   [A >= B && A >= 1 + B]          (?,1)
          1. f1(A,B,C,D) -> f1(A,A,0,D)     [B >= E && A = B]               (?,1)
          2. f1(A,B,C,D) -> f1(1 + A,A,E,D) [0 >= 1 + E && B >= F && A = B] (?,1)
          3. f1(A,B,C,D) -> f1(1 + A,A,E,D) [E >= 1 && B >= F && A = B]     (?,1)
          4. f1(A,B,C,D) -> f1(A,B,0,D)     [B >= 1 + A]                    (?,1)
          5. f1(A,B,C,D) -> f1(1 + A,B,E,D) [0 >= 1 + E && B >= 1 + A]      (?,1)
          6. f1(A,B,C,D) -> f1(1 + A,B,E,D) [E >= 1 && B >= 1 + A]          (?,1)
          7. f2(A,B,C,D) -> f1(A,B,C,D)     True                            (1,1)
        Signature:
          {(f1,4);(f2,4);(f300,4)}
        Flow Graph:
          [0->{},1->{0,1,2,3,4,5,6},2->{0,1,2,3,4,5,6},3->{0,1,2,3,4,5,6},4->{0,1,2,3,4,5,6},5->{0,1,2,3,4,5,6}
          ,6->{0,1,2,3,4,5,6},7->{0,1,2,3,4,5,6}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(1,0)
                                                             ,(1,4)
                                                             ,(1,5)
                                                             ,(1,6)
                                                             ,(2,1)
                                                             ,(2,2)
                                                             ,(2,3)
                                                             ,(2,4)
                                                             ,(2,5)
                                                             ,(2,6)
                                                             ,(3,1)
                                                             ,(3,2)
                                                             ,(3,3)
                                                             ,(3,4)
                                                             ,(3,5)
                                                             ,(3,6)
                                                             ,(4,0)
                                                             ,(4,1)
                                                             ,(4,2)
                                                             ,(4,3)
                                                             ,(5,0)
                                                             ,(6,0)]
* Step 2: FromIts NO
    + Considered Problem:
        Rules:
          0. f1(A,B,C,D) -> f300(A,B,C,E)   [A >= B && A >= 1 + B]          (?,1)
          1. f1(A,B,C,D) -> f1(A,A,0,D)     [B >= E && A = B]               (?,1)
          2. f1(A,B,C,D) -> f1(1 + A,A,E,D) [0 >= 1 + E && B >= F && A = B] (?,1)
          3. f1(A,B,C,D) -> f1(1 + A,A,E,D) [E >= 1 && B >= F && A = B]     (?,1)
          4. f1(A,B,C,D) -> f1(A,B,0,D)     [B >= 1 + A]                    (?,1)
          5. f1(A,B,C,D) -> f1(1 + A,B,E,D) [0 >= 1 + E && B >= 1 + A]      (?,1)
          6. f1(A,B,C,D) -> f1(1 + A,B,E,D) [E >= 1 && B >= 1 + A]          (?,1)
          7. f2(A,B,C,D) -> f1(A,B,C,D)     True                            (1,1)
        Signature:
          {(f1,4);(f2,4);(f300,4)}
        Flow Graph:
          [0->{},1->{1,2,3},2->{0},3->{0},4->{4,5,6},5->{1,2,3,4,5,6},6->{1,2,3,4,5,6},7->{0,1,2,3,4,5,6}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: CloseWith NO
    + Considered Problem:
        Rules:
          f1(A,B,C,D) -> f300(A,B,C,E)    [A >= B && A >= 1 + B]
          f1(A,B,C,D) -> f1(A,A,0,D)      [B >= E && A = B]
          f1(A,B,C,D) -> f1(1 + A,A,E,D)  [0 >= 1 + E && B >= F && A = B]
          f1(A,B,C,D) -> f1(1 + A,A,E,D)  [E >= 1 && B >= F && A = B]
          f1(A,B,C,D) -> f1(A,B,0,D)      [B >= 1 + A]
          f1(A,B,C,D) -> f1(1 + A,B,E,D)  [0 >= 1 + E && B >= 1 + A]
          f1(A,B,C,D) -> f1(1 + A,B,E,D)  [E >= 1 && B >= 1 + A]
          f2(A,B,C,D) -> f1(A,B,C,D)      True
        Signature:
          {(f1,4);(f2,4);(f300,4)}
        Rule Graph:
          [0->{},1->{1,2,3},2->{0},3->{0},4->{4,5,6},5->{1,2,3,4,5,6},6->{1,2,3,4,5,6},7->{0,1,2,3,4,5,6}]
    + Applied Processor:
        CloseWith False
    + Details:
        ()

NO