MAYBE
* Step 1: TrivialSCCs MAYBE
    + Considered Problem:
        Rules:
          0. f18(A,B,C,D,E,F,G,H,I,J,K) -> f24(A,B,C,D,E,F,G,H,I,J,K) [0 >= A]                  (?,1)
          1. f32(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,B,C,D,E,F,G,H,I,J,K) True                      (?,1)
          2. f34(A,B,C,D,E,F,G,H,I,J,K) -> f37(A,B,C,D,E,F,G,H,I,J,K) True                      (?,1)
          3. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,L,C,D,E,F,G,H,I,J,K) [A >= 1]                  (?,1)
          4. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,M,C,L,L,F,G,H,I,J,K) [0 >= A && 999 + C >= L]  (?,1)
          5. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(1,M,C,L,L,F,G,H,I,J,K) [0 >= A && L >= 1000 + C] (?,1)
          6. f18(A,B,C,D,E,F,G,H,I,J,K) -> f24(0,B,L,D,E,L,G,H,I,J,K) [A >= 1]                  (?,1)
          7. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,M,I,J,K) [0 >= M]                  (1,1)
          8. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,0,1,M,M) [M >= 1 && N >= 1]        (1,1)
          9. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f32(1,B,C,D,E,F,L,0,1,M,M) [0 >= M && N >= 1]        (1,1)
        Signature:
          {(f0,11);(f18,11);(f24,11);(f32,11);(f34,11);(f37,11)}
        Flow Graph:
          [0->{3,4,5},1->{1},2->{},3->{1},4->{1},5->{1},6->{3,4,5},7->{0,6},8->{0,6},9->{1}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: UnsatPaths MAYBE
    + Considered Problem:
        Rules:
          0. f18(A,B,C,D,E,F,G,H,I,J,K) -> f24(A,B,C,D,E,F,G,H,I,J,K) [0 >= A]                  (1,1)
          1. f32(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,B,C,D,E,F,G,H,I,J,K) True                      (?,1)
          2. f34(A,B,C,D,E,F,G,H,I,J,K) -> f37(A,B,C,D,E,F,G,H,I,J,K) True                      (1,1)
          3. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,L,C,D,E,F,G,H,I,J,K) [A >= 1]                  (1,1)
          4. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,M,C,L,L,F,G,H,I,J,K) [0 >= A && 999 + C >= L]  (1,1)
          5. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(1,M,C,L,L,F,G,H,I,J,K) [0 >= A && L >= 1000 + C] (1,1)
          6. f18(A,B,C,D,E,F,G,H,I,J,K) -> f24(0,B,L,D,E,L,G,H,I,J,K) [A >= 1]                  (1,1)
          7. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,M,I,J,K) [0 >= M]                  (1,1)
          8. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,0,1,M,M) [M >= 1 && N >= 1]        (1,1)
          9. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f32(1,B,C,D,E,F,L,0,1,M,M) [0 >= M && N >= 1]        (1,1)
        Signature:
          {(f0,11);(f18,11);(f24,11);(f32,11);(f34,11);(f37,11)}
        Flow Graph:
          [0->{3,4,5},1->{1},2->{},3->{1},4->{1},5->{1},6->{3,4,5},7->{0,6},8->{0,6},9->{1}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(0,3),(6,3),(7,0),(8,0)]
* Step 3: UnreachableRules MAYBE
    + Considered Problem:
        Rules:
          0. f18(A,B,C,D,E,F,G,H,I,J,K) -> f24(A,B,C,D,E,F,G,H,I,J,K) [0 >= A]                  (1,1)
          1. f32(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,B,C,D,E,F,G,H,I,J,K) True                      (?,1)
          2. f34(A,B,C,D,E,F,G,H,I,J,K) -> f37(A,B,C,D,E,F,G,H,I,J,K) True                      (1,1)
          3. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,L,C,D,E,F,G,H,I,J,K) [A >= 1]                  (1,1)
          4. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,M,C,L,L,F,G,H,I,J,K) [0 >= A && 999 + C >= L]  (1,1)
          5. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(1,M,C,L,L,F,G,H,I,J,K) [0 >= A && L >= 1000 + C] (1,1)
          6. f18(A,B,C,D,E,F,G,H,I,J,K) -> f24(0,B,L,D,E,L,G,H,I,J,K) [A >= 1]                  (1,1)
          7. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,M,I,J,K) [0 >= M]                  (1,1)
          8. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,0,1,M,M) [M >= 1 && N >= 1]        (1,1)
          9. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f32(1,B,C,D,E,F,L,0,1,M,M) [0 >= M && N >= 1]        (1,1)
        Signature:
          {(f0,11);(f18,11);(f24,11);(f32,11);(f34,11);(f37,11)}
        Flow Graph:
          [0->{4,5},1->{1},2->{},3->{1},4->{1},5->{1},6->{4,5},7->{6},8->{6},9->{1}]
        
    + Applied Processor:
        UnreachableRules
    + Details:
        Following transitions are not reachable from the starting states and are revomed: [0,2,3]
* Step 4: AddSinks MAYBE
    + Considered Problem:
        Rules:
          1. f32(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,B,C,D,E,F,G,H,I,J,K) True                      (?,1)
          4. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,M,C,L,L,F,G,H,I,J,K) [0 >= A && 999 + C >= L]  (1,1)
          5. f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(1,M,C,L,L,F,G,H,I,J,K) [0 >= A && L >= 1000 + C] (1,1)
          6. f18(A,B,C,D,E,F,G,H,I,J,K) -> f24(0,B,L,D,E,L,G,H,I,J,K) [A >= 1]                  (1,1)
          7. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,M,I,J,K) [0 >= M]                  (1,1)
          8. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,0,1,M,M) [M >= 1 && N >= 1]        (1,1)
          9. f0(A,B,C,D,E,F,G,H,I,J,K)  -> f32(1,B,C,D,E,F,L,0,1,M,M) [0 >= M && N >= 1]        (1,1)
        Signature:
          {(f0,11);(f18,11);(f24,11);(f32,11);(f34,11);(f37,11)}
        Flow Graph:
          [1->{1},4->{1},5->{1},6->{4,5},7->{6},8->{6},9->{1}]
        
    + Applied Processor:
        AddSinks
    + Details:
        ()
* Step 5: Failure MAYBE
  + Considered Problem:
      Rules:
        1.  f32(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,B,C,D,E,F,G,H,I,J,K)       True                      (?,1)
        4.  f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(A,M,C,L,L,F,G,H,I,J,K)       [0 >= A && 999 + C >= L]  (?,1)
        5.  f24(A,B,C,D,E,F,G,H,I,J,K) -> f32(1,M,C,L,L,F,G,H,I,J,K)       [0 >= A && L >= 1000 + C] (?,1)
        6.  f18(A,B,C,D,E,F,G,H,I,J,K) -> f24(0,B,L,D,E,L,G,H,I,J,K)       [A >= 1]                  (?,1)
        7.  f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,M,I,J,K)       [0 >= M]                  (1,1)
        8.  f0(A,B,C,D,E,F,G,H,I,J,K)  -> f18(1,B,C,D,E,F,L,0,1,M,M)       [M >= 1 && N >= 1]        (1,1)
        9.  f0(A,B,C,D,E,F,G,H,I,J,K)  -> f32(1,B,C,D,E,F,L,0,1,M,M)       [0 >= M && N >= 1]        (1,1)
        10. f32(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True                      (?,1)
      Signature:
        {(exitus616,11);(f0,11);(f18,11);(f24,11);(f32,11);(f34,11);(f37,11)}
      Flow Graph:
        [1->{1,10},4->{1,10},5->{1,10},6->{4,5},7->{6},8->{6},9->{1,10},10->{}]
      
  + Applied Processor:
      LooptreeTransformer
  + Details:
      We construct a looptree:
        P: [1,4,5,6,7,8,9,10]
        |
        `- p:[1] c: []
MAYBE