NO
* Step 1: UnsatPaths NO
    + Considered Problem:
        Rules:
          0. f18(A,B,C,D,E,F,G,H,I,J) -> f24(A,B,C,D,E,F,G,H,I,J) [0 >= A]                  (?,1)
          1. f31(A,B,C,D,E,F,G,H,I,J) -> f31(A,B,C,D,E,F,G,H,I,J) True                      (?,1)
          2. f33(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,D,E,F,G,H,I,J) True                      (?,1)
          3. f24(A,B,C,D,E,F,G,H,I,J) -> f31(A,K,C,D,E,F,G,H,I,J) [A >= 1]                  (?,1)
          4. f24(A,B,C,D,E,F,G,H,I,J) -> f31(A,L,C,K,E,F,G,H,I,J) [0 >= A && 999 + C >= K]  (?,1)
          5. f24(A,B,C,D,E,F,G,H,I,J) -> f31(1,L,C,K,E,F,G,H,I,J) [0 >= A && K >= 1000 + C] (?,1)
          6. f18(A,B,C,D,E,F,G,H,I,J) -> f24(0,B,K,D,K,F,G,H,I,J) [A >= 1]                  (?,1)
          7. f0(A,B,C,D,E,F,G,H,I,J)  -> f18(1,B,C,D,E,K,K,H,I,J) [0 >= K]                  (1,1)
          8. f0(A,B,C,D,E,F,G,H,I,J)  -> f18(1,B,C,D,E,K,0,1,L,L) [K >= 1 && L >= 1]        (1,1)
          9. f0(A,B,C,D,E,F,G,H,I,J)  -> f31(1,B,C,D,E,K,0,1,L,L) [K >= 1 && 0 >= L]        (1,1)
        Signature:
          {(f0,10);(f18,10);(f24,10);(f31,10);(f33,10);(f36,10)}
        Flow Graph:
          [0->{3,4,5},1->{1},2->{},3->{1},4->{1},5->{1},6->{3,4,5},7->{0,6},8->{0,6},9->{1}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(0,3),(6,3),(7,0),(8,0)]
* Step 2: UnreachableRules NO
    + Considered Problem:
        Rules:
          0. f18(A,B,C,D,E,F,G,H,I,J) -> f24(A,B,C,D,E,F,G,H,I,J) [0 >= A]                  (?,1)
          1. f31(A,B,C,D,E,F,G,H,I,J) -> f31(A,B,C,D,E,F,G,H,I,J) True                      (?,1)
          2. f33(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,D,E,F,G,H,I,J) True                      (?,1)
          3. f24(A,B,C,D,E,F,G,H,I,J) -> f31(A,K,C,D,E,F,G,H,I,J) [A >= 1]                  (?,1)
          4. f24(A,B,C,D,E,F,G,H,I,J) -> f31(A,L,C,K,E,F,G,H,I,J) [0 >= A && 999 + C >= K]  (?,1)
          5. f24(A,B,C,D,E,F,G,H,I,J) -> f31(1,L,C,K,E,F,G,H,I,J) [0 >= A && K >= 1000 + C] (?,1)
          6. f18(A,B,C,D,E,F,G,H,I,J) -> f24(0,B,K,D,K,F,G,H,I,J) [A >= 1]                  (?,1)
          7. f0(A,B,C,D,E,F,G,H,I,J)  -> f18(1,B,C,D,E,K,K,H,I,J) [0 >= K]                  (1,1)
          8. f0(A,B,C,D,E,F,G,H,I,J)  -> f18(1,B,C,D,E,K,0,1,L,L) [K >= 1 && L >= 1]        (1,1)
          9. f0(A,B,C,D,E,F,G,H,I,J)  -> f31(1,B,C,D,E,K,0,1,L,L) [K >= 1 && 0 >= L]        (1,1)
        Signature:
          {(f0,10);(f18,10);(f24,10);(f31,10);(f33,10);(f36,10)}
        Flow Graph:
          [0->{4,5},1->{1},2->{},3->{1},4->{1},5->{1},6->{4,5},7->{6},8->{6},9->{1}]
        
    + Applied Processor:
        UnreachableRules
    + Details:
        Following transitions are not reachable from the starting states and are revomed: [0,2,3]
* Step 3: FromIts NO
    + Considered Problem:
        Rules:
          1. f31(A,B,C,D,E,F,G,H,I,J) -> f31(A,B,C,D,E,F,G,H,I,J) True                      (?,1)
          4. f24(A,B,C,D,E,F,G,H,I,J) -> f31(A,L,C,K,E,F,G,H,I,J) [0 >= A && 999 + C >= K]  (?,1)
          5. f24(A,B,C,D,E,F,G,H,I,J) -> f31(1,L,C,K,E,F,G,H,I,J) [0 >= A && K >= 1000 + C] (?,1)
          6. f18(A,B,C,D,E,F,G,H,I,J) -> f24(0,B,K,D,K,F,G,H,I,J) [A >= 1]                  (?,1)
          7. f0(A,B,C,D,E,F,G,H,I,J)  -> f18(1,B,C,D,E,K,K,H,I,J) [0 >= K]                  (1,1)
          8. f0(A,B,C,D,E,F,G,H,I,J)  -> f18(1,B,C,D,E,K,0,1,L,L) [K >= 1 && L >= 1]        (1,1)
          9. f0(A,B,C,D,E,F,G,H,I,J)  -> f31(1,B,C,D,E,K,0,1,L,L) [K >= 1 && 0 >= L]        (1,1)
        Signature:
          {(f0,10);(f18,10);(f24,10);(f31,10);(f33,10);(f36,10)}
        Flow Graph:
          [1->{1},4->{1},5->{1},6->{4,5},7->{6},8->{6},9->{1}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 4: CloseWith NO
    + Considered Problem:
        Rules:
          f31(A,B,C,D,E,F,G,H,I,J) -> f31(A,B,C,D,E,F,G,H,I,J)  True
          f24(A,B,C,D,E,F,G,H,I,J) -> f31(A,L,C,K,E,F,G,H,I,J)  [0 >= A && 999 + C >= K]
          f24(A,B,C,D,E,F,G,H,I,J) -> f31(1,L,C,K,E,F,G,H,I,J)  [0 >= A && K >= 1000 + C]
          f18(A,B,C,D,E,F,G,H,I,J) -> f24(0,B,K,D,K,F,G,H,I,J)  [A >= 1]
          f0(A,B,C,D,E,F,G,H,I,J)  -> f18(1,B,C,D,E,K,K,H,I,J)  [0 >= K]
          f0(A,B,C,D,E,F,G,H,I,J)  -> f18(1,B,C,D,E,K,0,1,L,L)  [K >= 1 && L >= 1]
          f0(A,B,C,D,E,F,G,H,I,J)  -> f31(1,B,C,D,E,K,0,1,L,L)  [K >= 1 && 0 >= L]
        Signature:
          {(f0,10);(f18,10);(f24,10);(f31,10);(f33,10);(f36,10)}
        Rule Graph:
          [1->{1},4->{1},5->{1},6->{4,5},7->{6},8->{6},9->{1}]
    + Applied Processor:
        CloseWith False
    + Details:
        ()

NO