NO
* Step 1: UnsatPaths NO
    + Considered Problem:
        Rules:
          0.  f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     True                              (?,1)
          1.  f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     True                              (?,1)
          2.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     [A >= B]                          (?,1)
          3.  f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     [E >= 3]                          (?,1)
          4.  f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     [1 >= E]                          (?,1)
          5.  f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     [E = 2]                           (?,1)
          6.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,W,X,Y,Z,D,W,W,W,O,P,Q,R,S,T,U,V)     [W >= 1 && B >= 1 + A]            (?,1)
          7.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [B >= 1 + A && 0 >= W && A1 >= 2] (?,1)
          8.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [B >= 1 + A && 0 >= W && 0 >= A1] (?,1)
          9.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f11(1 + A,B,C,D,1,F,W,X,Y,Z,D,W,W,W,W,Q,Q,1,1,1,0,V) [0 >= W && B >= 1 + A]            (?,1)
          10. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)  -> f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0)     True                              (1,1)
        Signature:
          {(f0,22);(f11,22);(f37,22);(f51,22);(f53,22);(f56,22)}
        Flow Graph:
          [0->{0},1->{},2->{0},3->{0},4->{0},5->{0},6->{0},7->{3,4,5},8->{3,4,5},9->{2,6,7,8,9},10->{2,6,7,8,9}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(7,4),(8,3),(8,5)]
* Step 2: UnreachableRules NO
    + Considered Problem:
        Rules:
          0.  f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     True                              (?,1)
          1.  f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     True                              (?,1)
          2.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     [A >= B]                          (?,1)
          3.  f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     [E >= 3]                          (?,1)
          4.  f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     [1 >= E]                          (?,1)
          5.  f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     [E = 2]                           (?,1)
          6.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,W,X,Y,Z,D,W,W,W,O,P,Q,R,S,T,U,V)     [W >= 1 && B >= 1 + A]            (?,1)
          7.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [B >= 1 + A && 0 >= W && A1 >= 2] (?,1)
          8.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [B >= 1 + A && 0 >= W && 0 >= A1] (?,1)
          9.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f11(1 + A,B,C,D,1,F,W,X,Y,Z,D,W,W,W,W,Q,Q,1,1,1,0,V) [0 >= W && B >= 1 + A]            (?,1)
          10. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)  -> f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0)     True                              (1,1)
        Signature:
          {(f0,22);(f11,22);(f37,22);(f51,22);(f53,22);(f56,22)}
        Flow Graph:
          [0->{0},1->{},2->{0},3->{0},4->{0},5->{0},6->{0},7->{3,5},8->{4},9->{2,6,7,8,9},10->{2,6,7,8,9}]
        
    + Applied Processor:
        UnreachableRules
    + Details:
        Following transitions are not reachable from the starting states and are revomed: [1]
* Step 3: FromIts NO
    + Considered Problem:
        Rules:
          0.  f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     True                              (?,1)
          2.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     [A >= B]                          (?,1)
          3.  f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     [E >= 3]                          (?,1)
          4.  f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     [1 >= E]                          (?,1)
          5.  f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)     [E = 2]                           (?,1)
          6.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,W,X,Y,Z,D,W,W,W,O,P,Q,R,S,T,U,V)     [W >= 1 && B >= 1 + A]            (?,1)
          7.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [B >= 1 + A && 0 >= W && A1 >= 2] (?,1)
          8.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [B >= 1 + A && 0 >= W && 0 >= A1] (?,1)
          9.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f11(1 + A,B,C,D,1,F,W,X,Y,Z,D,W,W,W,W,Q,Q,1,1,1,0,V) [0 >= W && B >= 1 + A]            (?,1)
          10. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)  -> f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0)     True                              (1,1)
        Signature:
          {(f0,22);(f11,22);(f37,22);(f51,22);(f53,22);(f56,22)}
        Flow Graph:
          [0->{0},2->{0},3->{0},4->{0},5->{0},6->{0},7->{3,5},8->{4},9->{2,6,7,8,9},10->{2,6,7,8,9}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 4: CloseWith NO
    + Considered Problem:
        Rules:
          f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)  -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U
          ,V)                                                                                                        
          True
          f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)  -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)      
          [A >= B]
          f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)  -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)      
          [E >= 3]
          f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)  -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)      
          [1 >= E]
          f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)  -> f51(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)      
          [E = 2]
          f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)  -> f51(A,B,0,0,E,F,W,X,Y,Z,D,W,W,W,O,P,Q,R,S,T,U,V)      
          [W >= 1 && B >= 1 + A]
          f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)  -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V)  
          [B >= 1 + A && 0 >= W && A1 >= 2]
          f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)  -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V)  
          [B >= 1 + A && 0 >= W && 0 >= A1]
          f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)  -> f11(1 + A,B,C,D,1,F,W,X,Y,Z,D,W,W,W,W,Q,Q,1,1,1,0,V)  
          [0 >= W && B >= 1 + A]
          f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V)   -> f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0)      
          True
        Signature:
          {(f0,22);(f11,22);(f37,22);(f51,22);(f53,22);(f56,22)}
        Rule Graph:
          [0->{0},2->{0},3->{0},4->{0},5->{0},6->{0},7->{3,5},8->{4},9->{2,6,7,8,9},10->{2,6,7,8,9}]
    + Applied Processor:
        CloseWith False
    + Details:
        ()

NO