NO
* Step 1: UnsatPaths NO
    + Considered Problem:
        Rules:
          0.  f8(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f32(A,B,N,D,E,F,G,H,I,J,K,L,M)      [A >= B]                   (?,1)
          1.  f15(A,B,C,D,E,F,G,H,I,J,K,L,M)  -> f8(A,B,C,N,E,F,G,H,I,J,K,L,M)       True                       (1,1)
          2.  f300(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f8(1 + A,B,C,D,E,F,G,H,I,J,K,L,M)   [B >= E]                   (?,1)
          3.  f8(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f8(1 + A,B,C,D,E,F,G,H,I,J,K,L,M)   [B >= 1 + A && B >= E]     (?,1)
          4.  f13(A,B,C,D,E,F,G,H,I,J,K,L,M)  -> f1(A,B,N,D,E,O,P,0,2,0,0,L,M)       True                       (?,1)
          5.  f12(A,B,C,D,E,F,G,H,I,J,K,L,M)  -> f1(A,B,N,D,E,O,P,0,I,0,0,1 + I,M)   [4 >= I]                   (?,1)
          6.  f10(A,B,C,D,E,F,G,H,I,J,K,L,M)  -> f1(A,B,N,D,E,O,P,0,I,0,0,L,2)       True                       (?,1)
          7.  f8(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M)       [B >= 1 + A && E >= 1 + B] (?,1)
          8.  f1(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M)       [E >= 1 + B && 4 >= M]     (?,1)
          9.  f300(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M)       [E >= 1 + B]               (?,1)
          10. f12(A,B,C,D,E,F,G,H,I,J,K,L,M)  -> f300(A,1 + B,N,D,E,O,G,1,I,1,1,L,M) [I >= 5]                   (?,1)
          11. f1(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f300(A,1 + B,N,D,E,O,G,1,I,1,1,L,M) [E >= 1 + B && M >= 5]     (?,1)
        Signature:
          {(f1,13);(f10,13);(f12,13);(f13,13);(f15,13);(f300,13);(f32,13);(f8,13)}
        Flow Graph:
          [0->{},1->{0,3,7},2->{0,3,7},3->{0,3,7},4->{8,11},5->{8,11},6->{8,11},7->{8,11},8->{8,11},9->{8,11},10->{2
          ,9},11->{2,9}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(2,7),(3,7),(6,11),(8,11)]
* Step 2: UnreachableRules NO
    + Considered Problem:
        Rules:
          0.  f8(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f32(A,B,N,D,E,F,G,H,I,J,K,L,M)      [A >= B]                   (?,1)
          1.  f15(A,B,C,D,E,F,G,H,I,J,K,L,M)  -> f8(A,B,C,N,E,F,G,H,I,J,K,L,M)       True                       (1,1)
          2.  f300(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f8(1 + A,B,C,D,E,F,G,H,I,J,K,L,M)   [B >= E]                   (?,1)
          3.  f8(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f8(1 + A,B,C,D,E,F,G,H,I,J,K,L,M)   [B >= 1 + A && B >= E]     (?,1)
          4.  f13(A,B,C,D,E,F,G,H,I,J,K,L,M)  -> f1(A,B,N,D,E,O,P,0,2,0,0,L,M)       True                       (?,1)
          5.  f12(A,B,C,D,E,F,G,H,I,J,K,L,M)  -> f1(A,B,N,D,E,O,P,0,I,0,0,1 + I,M)   [4 >= I]                   (?,1)
          6.  f10(A,B,C,D,E,F,G,H,I,J,K,L,M)  -> f1(A,B,N,D,E,O,P,0,I,0,0,L,2)       True                       (?,1)
          7.  f8(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M)       [B >= 1 + A && E >= 1 + B] (?,1)
          8.  f1(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M)       [E >= 1 + B && 4 >= M]     (?,1)
          9.  f300(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M)       [E >= 1 + B]               (?,1)
          10. f12(A,B,C,D,E,F,G,H,I,J,K,L,M)  -> f300(A,1 + B,N,D,E,O,G,1,I,1,1,L,M) [I >= 5]                   (?,1)
          11. f1(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f300(A,1 + B,N,D,E,O,G,1,I,1,1,L,M) [E >= 1 + B && M >= 5]     (?,1)
        Signature:
          {(f1,13);(f10,13);(f12,13);(f13,13);(f15,13);(f300,13);(f32,13);(f8,13)}
        Flow Graph:
          [0->{},1->{0,3,7},2->{0,3},3->{0,3},4->{8,11},5->{8,11},6->{8},7->{8,11},8->{8},9->{8,11},10->{2,9},11->{2
          ,9}]
        
    + Applied Processor:
        UnreachableRules
    + Details:
        Following transitions are not reachable from the starting states and are revomed: [4,5,6,10]
* Step 3: FromIts NO
    + Considered Problem:
        Rules:
          0.  f8(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f32(A,B,N,D,E,F,G,H,I,J,K,L,M)      [A >= B]                   (?,1)
          1.  f15(A,B,C,D,E,F,G,H,I,J,K,L,M)  -> f8(A,B,C,N,E,F,G,H,I,J,K,L,M)       True                       (1,1)
          2.  f300(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f8(1 + A,B,C,D,E,F,G,H,I,J,K,L,M)   [B >= E]                   (?,1)
          3.  f8(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f8(1 + A,B,C,D,E,F,G,H,I,J,K,L,M)   [B >= 1 + A && B >= E]     (?,1)
          7.  f8(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M)       [B >= 1 + A && E >= 1 + B] (?,1)
          8.  f1(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M)       [E >= 1 + B && 4 >= M]     (?,1)
          9.  f300(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M)       [E >= 1 + B]               (?,1)
          11. f1(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f300(A,1 + B,N,D,E,O,G,1,I,1,1,L,M) [E >= 1 + B && M >= 5]     (?,1)
        Signature:
          {(f1,13);(f10,13);(f12,13);(f13,13);(f15,13);(f300,13);(f32,13);(f8,13)}
        Flow Graph:
          [0->{},1->{0,3,7},2->{0,3},3->{0,3},7->{8,11},8->{8},9->{8,11},11->{2,9}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 4: CloseWith NO
    + Considered Problem:
        Rules:
          f8(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f32(A,B,N,D,E,F,G,H,I,J,K,L,M)        [A >= B]
          f15(A,B,C,D,E,F,G,H,I,J,K,L,M)  -> f8(A,B,C,N,E,F,G,H,I,J,K,L,M)         True
          f300(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f8(1 + A,B,C,D,E,F,G,H,I,J,K,L,M)     [B >= E]
          f8(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f8(1 + A,B,C,D,E,F,G,H,I,J,K,L,M)     [B >= 1 + A && B >= E]
          f8(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M)         [B >= 1 + A && E >= 1 + B]
          f1(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M)         [E >= 1 + B && 4 >= M]
          f300(A,B,C,D,E,F,G,H,I,J,K,L,M) -> f1(A,B,N,D,E,O,P,0,I,0,0,L,M)         [E >= 1 + B]
          f1(A,B,C,D,E,F,G,H,I,J,K,L,M)   -> f300(A,1 + B,N,D,E,O,G,1,I,1,1,L,M)   [E >= 1 + B && M >= 5]
        Signature:
          {(f1,13);(f10,13);(f12,13);(f13,13);(f15,13);(f300,13);(f32,13);(f8,13)}
        Rule Graph:
          [0->{},1->{0,3,7},2->{0,3},3->{0,3},7->{8,11},8->{8},9->{8,11},11->{2,9}]
    + Applied Processor:
        CloseWith False
    + Details:
        ()

NO