MAYBE
* Step 1: TrivialSCCs MAYBE
    + Considered Problem:
        Rules:
          0.  f0(A,B,C,D)    -> f10001(B,1,C,1) True                           (1,1)
          1.  f0(A,B,C,D)    -> f10001(B,B,C,1) True                           (1,1)
          2.  f0(A,B,C,D)    -> f12(B,2,C,D)    True                           (1,1)
          3.  f0(A,B,C,D)    -> f110(1,1,C,D)   True                           (1,1)
          4.  f0(A,B,C,D)    -> f10001(A,1,C,D) True                           (1,1)
          5.  f0(A,B,C,D)    -> f2(A,2,C,D)     True                           (1,1)
          6.  f0(A,B,C,D)    -> f10001(A,B,C,D) True                           (1,1)
          7.  f12(A,B,C,D)   -> f10001(A,B,C,1) [2 + -1*B >= 0 && -2 + B >= 0] (?,1)
          8.  f12(A,B,C,D)   -> f12(A,B,C,D)    [2 + -1*B >= 0 && -2 + B >= 0] (?,1)
          9.  f110(A,B,C,D)  -> f10001(A,B,C,1) [1 + -1*B >= 0                 (?,1)
                                                 && A + -1*B >= 0                   
                                                 && 2 + -1*A + -1*B >= 0            
                                                 && -1 + B >= 0                     
                                                 && -2 + A + B >= 0                 
                                                 && -1*A + B >= 0                   
                                                 && 1 + -1*A >= 0                   
                                                 && -1 + A >= 0]                    
          10. f110(A,B,C,D)  -> f120(A,2,C,D)   [1 + -1*B >= 0                 (?,1)
                                                 && A + -1*B >= 0                   
                                                 && 2 + -1*A + -1*B >= 0            
                                                 && -1 + B >= 0                     
                                                 && -2 + A + B >= 0                 
                                                 && -1*A + B >= 0                   
                                                 && 1 + -1*A >= 0                   
                                                 && -1 + A >= 0]                    
          11. f2(A,B,C,D)    -> f1200(B,B,C,D)  [2 + -1*B >= 0 && -2 + B >= 0] (?,1)
          12. f2(A,B,C,D)    -> f10001(A,B,C,D) [2 + -1*B >= 0 && -2 + B >= 0] (?,1)
          13. f2(A,B,C,D)    -> f2(A,B,C,D)     [2 + -1*B >= 0 && -2 + B >= 0] (?,1)
          14. f120(A,B,C,D)  -> f10001(A,B,C,1) [2 + -1*B >= 0                 (?,1)
                                                 && 1 + A + -1*B >= 0               
                                                 && 3 + -1*A + -1*B >= 0            
                                                 && -2 + B >= 0                     
                                                 && -3 + A + B >= 0                 
                                                 && -1 + -1*A + B >= 0              
                                                 && 1 + -1*A >= 0                   
                                                 && -1 + A >= 0]                    
          15. f120(A,B,C,D)  -> f120(A,B,C,D)   [2 + -1*B >= 0                 (?,1)
                                                 && 1 + A + -1*B >= 0               
                                                 && 3 + -1*A + -1*B >= 0            
                                                 && -2 + B >= 0                     
                                                 && -3 + A + B >= 0                 
                                                 && -1 + -1*A + B >= 0              
                                                 && 1 + -1*A >= 0                   
                                                 && -1 + A >= 0]                    
          16. f1200(A,B,C,D) -> f10001(A,B,C,1) [2 + -1*B >= 0                 (?,1)
                                                 && A + -1*B >= 0                   
                                                 && 4 + -1*A + -1*B >= 0            
                                                 && -2 + B >= 0                     
                                                 && -4 + A + B >= 0                 
                                                 && -1*A + B >= 0                   
                                                 && 2 + -1*A >= 0                   
                                                 && -2 + A >= 0]                    
          17. f1200(A,B,C,D) -> f1200(A,B,C,D)  [2 + -1*B >= 0                 (?,1)
                                                 && A + -1*B >= 0                   
                                                 && 4 + -1*A + -1*B >= 0            
                                                 && -2 + B >= 0                     
                                                 && -4 + A + B >= 0                 
                                                 && -1*A + B >= 0                   
                                                 && 2 + -1*A >= 0                   
                                                 && -2 + A >= 0]                    
        Signature:
          {(f0,4);(f10001,4);(f110,4);(f12,4);(f120,4);(f1200,4);(f2,4)}
        Flow Graph:
          [0->{},1->{},2->{7,8},3->{9,10},4->{},5->{11,12,13},6->{},7->{},8->{7,8},9->{},10->{14,15},11->{16,17}
          ,12->{},13->{11,12,13},14->{},15->{14,15},16->{},17->{16,17}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: Failure MAYBE
  + Considered Problem:
      Rules:
        0.  f0(A,B,C,D)    -> f10001(B,1,C,1) True                           (1,1)
        1.  f0(A,B,C,D)    -> f10001(B,B,C,1) True                           (1,1)
        2.  f0(A,B,C,D)    -> f12(B,2,C,D)    True                           (1,1)
        3.  f0(A,B,C,D)    -> f110(1,1,C,D)   True                           (1,1)
        4.  f0(A,B,C,D)    -> f10001(A,1,C,D) True                           (1,1)
        5.  f0(A,B,C,D)    -> f2(A,2,C,D)     True                           (1,1)
        6.  f0(A,B,C,D)    -> f10001(A,B,C,D) True                           (1,1)
        7.  f12(A,B,C,D)   -> f10001(A,B,C,1) [2 + -1*B >= 0 && -2 + B >= 0] (1,1)
        8.  f12(A,B,C,D)   -> f12(A,B,C,D)    [2 + -1*B >= 0 && -2 + B >= 0] (?,1)
        9.  f110(A,B,C,D)  -> f10001(A,B,C,1) [1 + -1*B >= 0                 (1,1)
                                               && A + -1*B >= 0                   
                                               && 2 + -1*A + -1*B >= 0            
                                               && -1 + B >= 0                     
                                               && -2 + A + B >= 0                 
                                               && -1*A + B >= 0                   
                                               && 1 + -1*A >= 0                   
                                               && -1 + A >= 0]                    
        10. f110(A,B,C,D)  -> f120(A,2,C,D)   [1 + -1*B >= 0                 (1,1)
                                               && A + -1*B >= 0                   
                                               && 2 + -1*A + -1*B >= 0            
                                               && -1 + B >= 0                     
                                               && -2 + A + B >= 0                 
                                               && -1*A + B >= 0                   
                                               && 1 + -1*A >= 0                   
                                               && -1 + A >= 0]                    
        11. f2(A,B,C,D)    -> f1200(B,B,C,D)  [2 + -1*B >= 0 && -2 + B >= 0] (1,1)
        12. f2(A,B,C,D)    -> f10001(A,B,C,D) [2 + -1*B >= 0 && -2 + B >= 0] (1,1)
        13. f2(A,B,C,D)    -> f2(A,B,C,D)     [2 + -1*B >= 0 && -2 + B >= 0] (?,1)
        14. f120(A,B,C,D)  -> f10001(A,B,C,1) [2 + -1*B >= 0                 (1,1)
                                               && 1 + A + -1*B >= 0               
                                               && 3 + -1*A + -1*B >= 0            
                                               && -2 + B >= 0                     
                                               && -3 + A + B >= 0                 
                                               && -1 + -1*A + B >= 0              
                                               && 1 + -1*A >= 0                   
                                               && -1 + A >= 0]                    
        15. f120(A,B,C,D)  -> f120(A,B,C,D)   [2 + -1*B >= 0                 (?,1)
                                               && 1 + A + -1*B >= 0               
                                               && 3 + -1*A + -1*B >= 0            
                                               && -2 + B >= 0                     
                                               && -3 + A + B >= 0                 
                                               && -1 + -1*A + B >= 0              
                                               && 1 + -1*A >= 0                   
                                               && -1 + A >= 0]                    
        16. f1200(A,B,C,D) -> f10001(A,B,C,1) [2 + -1*B >= 0                 (1,1)
                                               && A + -1*B >= 0                   
                                               && 4 + -1*A + -1*B >= 0            
                                               && -2 + B >= 0                     
                                               && -4 + A + B >= 0                 
                                               && -1*A + B >= 0                   
                                               && 2 + -1*A >= 0                   
                                               && -2 + A >= 0]                    
        17. f1200(A,B,C,D) -> f1200(A,B,C,D)  [2 + -1*B >= 0                 (?,1)
                                               && A + -1*B >= 0                   
                                               && 4 + -1*A + -1*B >= 0            
                                               && -2 + B >= 0                     
                                               && -4 + A + B >= 0                 
                                               && -1*A + B >= 0                   
                                               && 2 + -1*A >= 0                   
                                               && -2 + A >= 0]                    
      Signature:
        {(f0,4);(f10001,4);(f110,4);(f12,4);(f120,4);(f1200,4);(f2,4)}
      Flow Graph:
        [0->{},1->{},2->{7,8},3->{9,10},4->{},5->{11,12,13},6->{},7->{},8->{7,8},9->{},10->{14,15},11->{16,17}
        ,12->{},13->{11,12,13},14->{},15->{14,15},16->{},17->{16,17}]
      
  + Applied Processor:
      Failing "Open problems left."
  + Details:
      Open problems left.
MAYBE