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

NO