NO
* Step 1: FromIts NO
    + Considered Problem:
        Rules:
          0. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,C1,D1,E,E,G,G,A,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1)             [A >= 0 && C1 >= 2]                                                         (?,1)
          1. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1)  -> f1(A,B,C,D,E,F,G,H,I,1 + J,L,C1,L,D1,J,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1)          [I >= 1 + J && J >= 0]                                                      (?,1)
          2. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1)  -> f1(A,C1,C,D,E,F,G,H,C1,2,E1,F1,E1,N,O,D1,E1,G1,2,T,U,V,W,X,Y,Z,A1,B1)        [C1 >= 2]                                                                   (1,1)
          3. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1)  -> f9(A,C1,0,D,0,F,G,H,N1,L1,O1,R1,Q1,N,O,M1,P1,R,S,D1,E1,F1,G1,K1,S1,T1,U1,B1) [0 >= H1 && 0 >= I1 && 0 >= C1 && 0 >= J1]                                  (1,1)
          4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1)  -> f12(A,C1,D1,D,K,F,G,H,G1,F1,K1,N1,M1,N,O,P,L1,R,S,T,U,V,W,X,O1,P1,A1,E1)     [J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && C1 >= 2 && E1 >= C1] (?,1)
          5. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f9(A,C1,0,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,D1,E1,F1,G1,K1,Y,L1,M1,B1)         [N1 >= 2 && O1 >= 2 && A >= 0 && C1 >= 2 && E = 0 && C = 0]                 (?,1)
          6. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1)  -> f9(A,1,K1,D,0,F,G,H,N1,L1,O1,R1,Q1,N,O,M1,P1,R,S,C1,D1,E1,F1,G1,S1,T1,U1,B1) [L = 0]                                                                     (1,1)
        Signature:
          {(f1,28);(f12,28);(f8,28);(f9,28)}
        Flow Graph:
          [0->{0,5},1->{1,4},2->{1,4},3->{},4->{0,5},5->{},6->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 2: CloseWith NO
    + Considered Problem:
        Rules:
          f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1)  -> f12(A,C1,D1,E,E,G,G,A,I,J,K,L,M,N,O,P,Q
          ,R,S,T,U,V,W,X,Y,Z,A1
          ,B1)                                                                                                                                              
          [A >= 0 && C1 >= 2]
          f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1)   -> f1(A,B,C,D,E,F,G,H,I,1 + J,L,C1,L,D1,J,P
          ,Q,R,S,T,U,V,W,X,Y,Z,A1
          ,B1)                                                                                                                                              
          [I >= 1 + J && J >= 0]
          f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1)   -> f1(A,C1,C,D,E,F,G,H,C1,2,E1,F1,E1,N,O,D1
          ,E1,G1,2,T,U,V,W,X,Y,Z,A1
          ,B1)                                                                                                                                              
          [C1 >= 2]
          f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1)   -> f9(A,C1,0,D,0,F,G,H,N1,L1,O1,R1,Q1,N,O,M1
          ,P1,R,S,D1,E1,F1,G1,K1,S1,T1,U1
          ,B1)                                                                                                                                              
          [0 >= H1 && 0 >= I1 && 0 >= C1 && 0 >= J1]
          f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1)   -> f12(A,C1,D1,D,K,F,G,H,G1,F1,K1,N1,M1,N,O
          ,P,L1,R,S,T,U,V,W,X,O1,P1,A1
          ,E1)                                                                                                                                              
          [J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && C1 >= 2 && E1 >= C1]
          f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1)  -> f9(A,C1,0,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S
          ,D1,E1,F1,G1,K1,Y,L1,M1
          ,B1)                                                                                                                                              
          [N1 >= 2 && O1 >= 2 && A >= 0 && C1 >= 2 && E = 0 && C = 0]
          f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1)   -> f9(A,1,K1,D,0,F,G,H,N1,L1,O1,R1,Q1,N,O,M1
          ,P1,R,S,C1,D1,E1,F1,G1,S1,T1,U1
          ,B1)                                                                                                                                              
          [L = 0]
        Signature:
          {(f1,28);(f12,28);(f8,28);(f9,28)}
        Rule Graph:
          [0->{0,5},1->{1,4},2->{1,4},3->{},4->{0,5},5->{},6->{}]
    + Applied Processor:
        CloseWith False
    + Details:
        ()

NO