MAYBE
* Step 1: UnsatPaths MAYBE
    + Considered Problem:
        Rules:
          0. f0(A,B) -> f2(3,C)       True                                                                     (1,1)
          1. f0(A,B) -> f2(C,D)       [C >= 1 && C >= 5 && C >= 2 && C >= 3]                                   (1,1)
          2. f2(A,B) -> f2(4 + 6*B,C) [-3 + A >= 0 && 6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1)
          3. f2(A,B) -> f2(B,C)       [-3 + A >= 0 && B = 3 && A = 6]                                          (?,1)
          4. f2(A,B) -> f2(B,C)       [-3 + A >= 0 && B >= 5 && B >= 2 && B >= 3 && A = 2*B]                   (?,1)
        Signature:
          {(f0,2);(f2,2)}
        Flow Graph:
          [0->{2,3,4},1->{2,3,4},2->{2,3,4},3->{2,3,4},4->{2,3,4}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(0,3),(0,4),(2,3),(3,3),(3,4)]
* Step 2: FromIts MAYBE
    + Considered Problem:
        Rules:
          0. f0(A,B) -> f2(3,C)       True                                                                     (1,1)
          1. f0(A,B) -> f2(C,D)       [C >= 1 && C >= 5 && C >= 2 && C >= 3]                                   (1,1)
          2. f2(A,B) -> f2(4 + 6*B,C) [-3 + A >= 0 && 6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B] (?,1)
          3. f2(A,B) -> f2(B,C)       [-3 + A >= 0 && B = 3 && A = 6]                                          (?,1)
          4. f2(A,B) -> f2(B,C)       [-3 + A >= 0 && B >= 5 && B >= 2 && B >= 3 && A = 2*B]                   (?,1)
        Signature:
          {(f0,2);(f2,2)}
        Flow Graph:
          [0->{2},1->{2,3,4},2->{2,4},3->{2},4->{2,3,4}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: Unfold MAYBE
    + Considered Problem:
        Rules:
          f0(A,B) -> f2(3,C)        True
          f0(A,B) -> f2(C,D)        [C >= 1 && C >= 5 && C >= 2 && C >= 3]
          f2(A,B) -> f2(4 + 6*B,C)  [-3 + A >= 0 && 6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B]
          f2(A,B) -> f2(B,C)        [-3 + A >= 0 && B = 3 && A = 6]
          f2(A,B) -> f2(B,C)        [-3 + A >= 0 && B >= 5 && B >= 2 && B >= 3 && A = 2*B]
        Signature:
          {(f0,2);(f2,2)}
        Rule Graph:
          [0->{2},1->{2,3,4},2->{2,4},3->{2},4->{2,3,4}]
    + Applied Processor:
        Unfold
    + Details:
        ()
* Step 4: AddSinks MAYBE
    + Considered Problem:
        Rules:
          f0.0(A,B) -> f2.2(3,C)        True
          f0.1(A,B) -> f2.2(C,D)        [C >= 1 && C >= 5 && C >= 2 && C >= 3]
          f0.1(A,B) -> f2.3(C,D)        [C >= 1 && C >= 5 && C >= 2 && C >= 3]
          f0.1(A,B) -> f2.4(C,D)        [C >= 1 && C >= 5 && C >= 2 && C >= 3]
          f2.2(A,B) -> f2.2(4 + 6*B,C)  [-3 + A >= 0 && 6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B]
          f2.2(A,B) -> f2.4(4 + 6*B,C)  [-3 + A >= 0 && 6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B]
          f2.3(A,B) -> f2.2(B,C)        [-3 + A >= 0 && B = 3 && A = 6]
          f2.4(A,B) -> f2.2(B,C)        [-3 + A >= 0 && B >= 5 && B >= 2 && B >= 3 && A = 2*B]
          f2.4(A,B) -> f2.3(B,C)        [-3 + A >= 0 && B >= 5 && B >= 2 && B >= 3 && A = 2*B]
          f2.4(A,B) -> f2.4(B,C)        [-3 + A >= 0 && B >= 5 && B >= 2 && B >= 3 && A = 2*B]
        Signature:
          {(f0.0,2);(f0.1,2);(f2.2,2);(f2.3,2);(f2.4,2)}
        Rule Graph:
          [0->{4,5},1->{4,5},2->{6},3->{7,8,9},4->{4,5},5->{7,8,9},6->{4,5},7->{4,5},8->{6},9->{7,8,9}]
    + Applied Processor:
        AddSinks
    + Details:
        ()
* Step 5: Failure MAYBE
  + Considered Problem:
      Rules:
        f0.0(A,B) -> f2.2(3,C)        True
        f0.1(A,B) -> f2.2(C,D)        [C >= 1 && C >= 5 && C >= 2 && C >= 3]
        f0.1(A,B) -> f2.3(C,D)        [C >= 1 && C >= 5 && C >= 2 && C >= 3]
        f0.1(A,B) -> f2.4(C,D)        [C >= 1 && C >= 5 && C >= 2 && C >= 3]
        f2.2(A,B) -> f2.2(4 + 6*B,C)  [-3 + A >= 0 && 6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B]
        f2.2(A,B) -> f2.4(4 + 6*B,C)  [-3 + A >= 0 && 6*B >= 1 && 2 + 6*B >= 0 && 1 + 6*B >= 0 && A = 1 + 2*B]
        f2.3(A,B) -> f2.2(B,C)        [-3 + A >= 0 && B = 3 && A = 6]
        f2.4(A,B) -> f2.2(B,C)        [-3 + A >= 0 && B >= 5 && B >= 2 && B >= 3 && A = 2*B]
        f2.4(A,B) -> f2.3(B,C)        [-3 + A >= 0 && B >= 5 && B >= 2 && B >= 3 && A = 2*B]
        f2.4(A,B) -> f2.4(B,C)        [-3 + A >= 0 && B >= 5 && B >= 2 && B >= 3 && A = 2*B]
        f2.2(A,B) -> exitus616(A,B)   True
        f2.2(A,B) -> exitus616(A,B)   True
        f2.3(A,B) -> exitus616(A,B)   True
        f2.4(A,B) -> exitus616(A,B)   True
        f2.2(A,B) -> exitus616(A,B)   True
        f2.4(A,B) -> exitus616(A,B)   True
        f2.2(A,B) -> exitus616(A,B)   True
        f2.2(A,B) -> exitus616(A,B)   True
        f2.3(A,B) -> exitus616(A,B)   True
        f2.4(A,B) -> exitus616(A,B)   True
        f2.2(A,B) -> exitus616(A,B)   True
        f2.4(A,B) -> exitus616(A,B)   True
        f2.2(A,B) -> exitus616(A,B)   True
        f2.2(A,B) -> exitus616(A,B)   True
        f2.3(A,B) -> exitus616(A,B)   True
        f2.4(A,B) -> exitus616(A,B)   True
        f2.2(A,B) -> exitus616(A,B)   True
        f2.4(A,B) -> exitus616(A,B)   True
        f2.2(A,B) -> exitus616(A,B)   True
        f2.2(A,B) -> exitus616(A,B)   True
        f2.3(A,B) -> exitus616(A,B)   True
        f2.4(A,B) -> exitus616(A,B)   True
        f2.2(A,B) -> exitus616(A,B)   True
        f2.4(A,B) -> exitus616(A,B)   True
      Signature:
        {(exitus616,2);(f0.0,2);(f0.1,2);(f2.2,2);(f2.3,2);(f2.4,2)}
      Rule Graph:
        [0->{4,5},1->{4,5},2->{6},3->{7,8,9},4->{4,5,10,16,22,28},5->{7,8,9,13,19,25,31},6->{4,5,11,17,23,29}
        ,7->{4,5,14,20,26,32},8->{6,12,18,24,30},9->{7,8,9,15,21,27,33}]
  + Applied Processor:
      Decompose Greedy
  + Details:
      We construct a looptree:
        P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33]
        |
        `- p:[4,6,8,5,7,9] c: []
MAYBE