NO
* Step 1: UnreachableRules NO
    + Considered Problem:
        Rules:
          0.  f0(A,B,C,D)    -> f10001(A,B,C,D) True    (1,1)
          1.  f2(A,B,C,D)    -> f2(A,B,C,D)     True    (?,1)
          2.  f2(A,B,C,D)    -> f10001(A,B,C,D) True    (?,1)
          3.  f2(A,B,C,D)    -> f1200(B,B,C,D)  True    (?,1)
          4.  f2200(A,B,C,D) -> f10000(A,B,0,D) [C = 0] (?,1)
          5.  f12(A,B,C,D)   -> f12(A,B,C,D)    True    (?,1)
          6.  f100(A,B,C,D)  -> f110(A,1,C,D)   True    (?,1)
          7.  f110(A,B,C,D)  -> f120(A,2,C,D)   True    (?,1)
          8.  f120(A,B,C,D)  -> f120(A,B,C,D)   True    (?,1)
          9.  f1200(A,B,C,D) -> f1200(A,B,C,D)  True    (?,1)
          10. f0(A,B,C,D)    -> f2(A,2,C,D)     True    (1,1)
          11. f0(A,B,C,D)    -> f10001(A,1,C,D) True    (1,1)
          12. f0(A,B,C,D)    -> f110(1,1,C,D)   True    (1,1)
          13. f0(A,B,C,D)    -> f12(B,2,C,D)    True    (1,1)
          14. f12(A,B,C,D)   -> f10001(A,B,C,1) True    (?,1)
          15. f0(A,B,C,D)    -> f10001(B,B,C,1) True    (1,1)
          16. f0(A,B,C,D)    -> f10001(B,1,C,1) True    (1,1)
          17. f100(A,B,C,D)  -> f10001(A,B,C,1) True    (?,1)
          18. f110(A,B,C,D)  -> f10001(A,B,C,1) True    (?,1)
          19. f120(A,B,C,D)  -> f10001(A,B,C,1) True    (?,1)
          20. f1000(A,B,C,D) -> f1200(A,2,C,D)  True    (?,1)
          21. f1000(A,B,C,D) -> f10001(A,B,C,1) True    (?,1)
          22. f1200(A,B,C,D) -> f10001(A,B,C,1) True    (?,1)
          23. f1000(A,B,C,D) -> f10001(A,1,C,1) True    (?,1)
        Signature:
          {(f0,4);(f100,4);(f1000,4);(f10000,4);(f10001,4);(f110,4);(f12,4);(f120,4);(f1200,4);(f2,4);(f2200,4)}
        Flow Graph:
          [0->{},1->{1,2,3},2->{},3->{9,22},4->{},5->{5,14},6->{7,18},7->{8,19},8->{8,19},9->{9,22},10->{1,2,3}
          ,11->{},12->{7,18},13->{5,14},14->{},15->{},16->{},17->{},18->{},19->{},20->{9,22},21->{},22->{},23->{}]
        
    + Applied Processor:
        UnreachableRules
    + Details:
        Following transitions are not reachable from the starting states and are revomed: [4,6,17,20,21,23]
* Step 2: FromIts NO
    + Considered Problem:
        Rules:
          0.  f0(A,B,C,D)    -> f10001(A,B,C,D) True (1,1)
          1.  f2(A,B,C,D)    -> f2(A,B,C,D)     True (?,1)
          2.  f2(A,B,C,D)    -> f10001(A,B,C,D) True (?,1)
          3.  f2(A,B,C,D)    -> f1200(B,B,C,D)  True (?,1)
          5.  f12(A,B,C,D)   -> f12(A,B,C,D)    True (?,1)
          7.  f110(A,B,C,D)  -> f120(A,2,C,D)   True (?,1)
          8.  f120(A,B,C,D)  -> f120(A,B,C,D)   True (?,1)
          9.  f1200(A,B,C,D) -> f1200(A,B,C,D)  True (?,1)
          10. f0(A,B,C,D)    -> f2(A,2,C,D)     True (1,1)
          11. f0(A,B,C,D)    -> f10001(A,1,C,D) True (1,1)
          12. f0(A,B,C,D)    -> f110(1,1,C,D)   True (1,1)
          13. f0(A,B,C,D)    -> f12(B,2,C,D)    True (1,1)
          14. f12(A,B,C,D)   -> f10001(A,B,C,1) True (?,1)
          15. f0(A,B,C,D)    -> f10001(B,B,C,1) True (1,1)
          16. f0(A,B,C,D)    -> f10001(B,1,C,1) True (1,1)
          18. f110(A,B,C,D)  -> f10001(A,B,C,1) True (?,1)
          19. f120(A,B,C,D)  -> f10001(A,B,C,1) True (?,1)
          22. f1200(A,B,C,D) -> f10001(A,B,C,1) True (?,1)
        Signature:
          {(f0,4);(f100,4);(f1000,4);(f10000,4);(f10001,4);(f110,4);(f12,4);(f120,4);(f1200,4);(f2,4);(f2200,4)}
        Flow Graph:
          [0->{},1->{1,2,3},2->{},3->{9,22},5->{5,14},7->{8,19},8->{8,19},9->{9,22},10->{1,2,3},11->{},12->{7,18}
          ,13->{5,14},14->{},15->{},16->{},18->{},19->{},22->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: CloseWith NO
    + Considered Problem:
        Rules:
          f0(A,B,C,D)    -> f10001(A,B,C,D)  True
          f2(A,B,C,D)    -> f2(A,B,C,D)      True
          f2(A,B,C,D)    -> f10001(A,B,C,D)  True
          f2(A,B,C,D)    -> f1200(B,B,C,D)   True
          f12(A,B,C,D)   -> f12(A,B,C,D)     True
          f110(A,B,C,D)  -> f120(A,2,C,D)    True
          f120(A,B,C,D)  -> f120(A,B,C,D)    True
          f1200(A,B,C,D) -> f1200(A,B,C,D)   True
          f0(A,B,C,D)    -> f2(A,2,C,D)      True
          f0(A,B,C,D)    -> f10001(A,1,C,D)  True
          f0(A,B,C,D)    -> f110(1,1,C,D)    True
          f0(A,B,C,D)    -> f12(B,2,C,D)     True
          f12(A,B,C,D)   -> f10001(A,B,C,1)  True
          f0(A,B,C,D)    -> f10001(B,B,C,1)  True
          f0(A,B,C,D)    -> f10001(B,1,C,1)  True
          f110(A,B,C,D)  -> f10001(A,B,C,1)  True
          f120(A,B,C,D)  -> f10001(A,B,C,1)  True
          f1200(A,B,C,D) -> f10001(A,B,C,1)  True
        Signature:
          {(f0,4);(f100,4);(f1000,4);(f10000,4);(f10001,4);(f110,4);(f12,4);(f120,4);(f1200,4);(f2,4);(f2200,4)}
        Rule Graph:
          [0->{},1->{1,2,3},2->{},3->{9,22},5->{5,14},7->{8,19},8->{8,19},9->{9,22},10->{1,2,3},11->{},12->{7,18}
          ,13->{5,14},14->{},15->{},16->{},18->{},19->{},22->{}]
    + Applied Processor:
        CloseWith False
    + Details:
        ()

NO