NO
* Step 1: UnsatPaths NO
    + Considered Problem:
        Rules:
          0. f18(A,B,C,D,E,F,G,H,I,J,K) -> f24(A,B,C,D,E,F,G,H,I,J,K) [0 >= A]                  (?,1)
          1. f32(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,B,C,D,E,F,G,H,I,J,K) True                      (?,1)
          2. f34(A,B,C,D,E,F,G,H,I,J,K) -> f37(A,B,C,D,E,F,G,H,I,J,K) True                      (?,1)
          3. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,L,C,D,E,F,G,H,I,J,K) [A >= 1]                  (?,1)
          4. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,M,C,L,L,F,G,H,I,J,K) [0 >= A && 999 + C >= L]  (?,1)
          5. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(1,M,C,L,L,F,G,H,I,J,K) [0 >= A && L >= 1000 + C] (?,1)
          6. f18(A,B,C,D,E,F,G,H,I,J,K) -> f24(0,B,L,D,E,L,G,H,I,J,K) [A >= 1]                  (?,1)
          7. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,M,I,J,K) [0 >= M]                  (1,1)
          8. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,0,1,M,M) [M >= 1 && N >= 1]        (1,1)
          9. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f32(1,B,C,D,E,F,L,0,1,M,M) [0 >= M && N >= 1]        (1,1)
        Signature:
          {(f0,11);(f18,11);(f24,11);(f32,11);(f34,11);(f37,11)}
        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,K) -> f24(A,B,C,D,E,F,G,H,I,J,K) [0 >= A]                  (?,1)
          1. f32(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,B,C,D,E,F,G,H,I,J,K) True                      (?,1)
          2. f34(A,B,C,D,E,F,G,H,I,J,K) -> f37(A,B,C,D,E,F,G,H,I,J,K) True                      (?,1)
          3. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,L,C,D,E,F,G,H,I,J,K) [A >= 1]                  (?,1)
          4. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,M,C,L,L,F,G,H,I,J,K) [0 >= A && 999 + C >= L]  (?,1)
          5. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(1,M,C,L,L,F,G,H,I,J,K) [0 >= A && L >= 1000 + C] (?,1)
          6. f18(A,B,C,D,E,F,G,H,I,J,K) -> f24(0,B,L,D,E,L,G,H,I,J,K) [A >= 1]                  (?,1)
          7. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,M,I,J,K) [0 >= M]                  (1,1)
          8. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,0,1,M,M) [M >= 1 && N >= 1]        (1,1)
          9. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f32(1,B,C,D,E,F,L,0,1,M,M) [0 >= M && N >= 1]        (1,1)
        Signature:
          {(f0,11);(f18,11);(f24,11);(f32,11);(f34,11);(f37,11)}
        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. f32(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,B,C,D,E,F,G,H,I,J,K) True                      (?,1)
          4. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,M,C,L,L,F,G,H,I,J,K) [0 >= A && 999 + C >= L]  (?,1)
          5. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(1,M,C,L,L,F,G,H,I,J,K) [0 >= A && L >= 1000 + C] (?,1)
          6. f18(A,B,C,D,E,F,G,H,I,J,K) -> f24(0,B,L,D,E,L,G,H,I,J,K) [A >= 1]                  (?,1)
          7. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,M,I,J,K) [0 >= M]                  (1,1)
          8. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,0,1,M,M) [M >= 1 && N >= 1]        (1,1)
          9. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f32(1,B,C,D,E,F,L,0,1,M,M) [0 >= M && N >= 1]        (1,1)
        Signature:
          {(f0,11);(f18,11);(f24,11);(f32,11);(f34,11);(f37,11)}
        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:
          f32(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,B,C,D,E,F,G,H,I,J,K)  True
          f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,M,C,L,L,F,G,H,I,J,K)  [0 >= A && 999 + C >= L]
          f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(1,M,C,L,L,F,G,H,I,J,K)  [0 >= A && L >= 1000 + C]
          f18(A,B,C,D,E,F,G,H,I,J,K) -> f24(0,B,L,D,E,L,G,H,I,J,K)  [A >= 1]
          f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,M,I,J,K)  [0 >= M]
          f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,0,1,M,M)  [M >= 1 && N >= 1]
          f0(A,B,C,D,E,F,G,H,I,J,K)  -> f32(1,B,C,D,E,F,L,0,1,M,M)  [0 >= M && N >= 1]
        Signature:
          {(f0,11);(f18,11);(f24,11);(f32,11);(f34,11);(f37,11)}
        Rule Graph:
          [1->{1},4->{1},5->{1},6->{4,5},7->{6},8->{6},9->{1}]
    + Applied Processor:
        CloseWith False
    + Details:
        ()

NO