MAYBE
* Step 1: TrivialSCCs MAYBE
    + 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:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: UnsatPaths MAYBE
    + 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,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,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,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,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,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,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,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,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 3: UnreachableRules MAYBE
    + 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,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,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,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,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,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,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,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,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 4: AddSinks MAYBE
    + 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,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,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,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,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,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,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,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:
        AddSinks
    + Details:
        ()
* Step 5: UnsatPaths MAYBE
    + 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)
          11. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True                              (?,1)
        Signature:
          {(exitus616,22);(f0,22);(f11,22);(f37,22);(f51,22);(f53,22);(f56,22)}
        Flow Graph:
          [0->{0,11},2->{0,11},3->{0,11},4->{0,11},5->{0,11},6->{0,11},7->{3,4,5},8->{3,4,5},9->{2,6,7,8,9},10->{2,6
          ,7,8,9},11->{}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(7,4),(8,3),(8,5)]
* Step 6: Failure MAYBE
  + 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)
        11. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True                              (?,1)
      Signature:
        {(exitus616,22);(f0,22);(f11,22);(f37,22);(f51,22);(f53,22);(f56,22)}
      Flow Graph:
        [0->{0,11},2->{0,11},3->{0,11},4->{0,11},5->{0,11},6->{0,11},7->{3,5},8->{4},9->{2,6,7,8,9},10->{2,6,7,8
        ,9},11->{}]
      
  + Applied Processor:
      LooptreeTransformer
  + Details:
      We construct a looptree:
        P: [0,2,3,4,5,6,7,8,9,10,11]
        |
        +- p:[9] c: [9]
        |
        `- p:[0] c: []
MAYBE