MAYBE
* Step 1: UnsatPaths MAYBE
    + Considered Problem:
        Rules:
          0.  evalfstart(A,B)    -> evalfentryin(A,B)      True                   (1,1)
          1.  evalfentryin(A,B)  -> evalfbb3in(B,A)        [A >= 1 && B >= 1 + A] (?,1)
          2.  evalfbb3in(A,B)    -> evalfreturnin(A,B)     [0 >= A]               (?,1)
          3.  evalfbb3in(A,B)    -> evalfbb4in(A,B)        [A >= 1]               (?,1)
          4.  evalfbb4in(A,B)    -> evalfbbin(A,B)         [0 >= 1 + C]           (?,1)
          5.  evalfbb4in(A,B)    -> evalfbbin(A,B)         [C >= 1]               (?,1)
          6.  evalfbb4in(A,B)    -> evalfreturnin(A,B)     True                   (?,1)
          7.  evalfbbin(A,B)     -> evalfbb1in(A,B)        [B >= 1 + A]           (?,1)
          8.  evalfbbin(A,B)     -> evalfbb2in(A,B)        [A >= B]               (?,1)
          9.  evalfbb1in(A,B)    -> evalfbb3in(1 + A,B)    True                   (?,1)
          10. evalfbb2in(A,B)    -> evalfbb3in(A + -1*B,B) True                   (?,1)
          11. evalfreturnin(A,B) -> evalfstop(A,B)         True                   (?,1)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbb4in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [0->{1},1->{2,3},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{2,3},10->{2,3},11->{}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(1,2)]
* Step 2: FromIts MAYBE
    + Considered Problem:
        Rules:
          0.  evalfstart(A,B)    -> evalfentryin(A,B)      True                   (1,1)
          1.  evalfentryin(A,B)  -> evalfbb3in(B,A)        [A >= 1 && B >= 1 + A] (?,1)
          2.  evalfbb3in(A,B)    -> evalfreturnin(A,B)     [0 >= A]               (?,1)
          3.  evalfbb3in(A,B)    -> evalfbb4in(A,B)        [A >= 1]               (?,1)
          4.  evalfbb4in(A,B)    -> evalfbbin(A,B)         [0 >= 1 + C]           (?,1)
          5.  evalfbb4in(A,B)    -> evalfbbin(A,B)         [C >= 1]               (?,1)
          6.  evalfbb4in(A,B)    -> evalfreturnin(A,B)     True                   (?,1)
          7.  evalfbbin(A,B)     -> evalfbb1in(A,B)        [B >= 1 + A]           (?,1)
          8.  evalfbbin(A,B)     -> evalfbb2in(A,B)        [A >= B]               (?,1)
          9.  evalfbb1in(A,B)    -> evalfbb3in(1 + A,B)    True                   (?,1)
          10. evalfbb2in(A,B)    -> evalfbb3in(A + -1*B,B) True                   (?,1)
          11. evalfreturnin(A,B) -> evalfstop(A,B)         True                   (?,1)
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbb4in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Flow Graph:
          [0->{1},1->{3},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{2,3},10->{2,3},11->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: Unfold MAYBE
    + Considered Problem:
        Rules:
          evalfstart(A,B)    -> evalfentryin(A,B)       True
          evalfentryin(A,B)  -> evalfbb3in(B,A)         [A >= 1 && B >= 1 + A]
          evalfbb3in(A,B)    -> evalfreturnin(A,B)      [0 >= A]
          evalfbb3in(A,B)    -> evalfbb4in(A,B)         [A >= 1]
          evalfbb4in(A,B)    -> evalfbbin(A,B)          [0 >= 1 + C]
          evalfbb4in(A,B)    -> evalfbbin(A,B)          [C >= 1]
          evalfbb4in(A,B)    -> evalfreturnin(A,B)      True
          evalfbbin(A,B)     -> evalfbb1in(A,B)         [B >= 1 + A]
          evalfbbin(A,B)     -> evalfbb2in(A,B)         [A >= B]
          evalfbb1in(A,B)    -> evalfbb3in(1 + A,B)     True
          evalfbb2in(A,B)    -> evalfbb3in(A + -1*B,B)  True
          evalfreturnin(A,B) -> evalfstop(A,B)          True
        Signature:
          {(evalfbb1in,2)
          ;(evalfbb2in,2)
          ;(evalfbb3in,2)
          ;(evalfbb4in,2)
          ;(evalfbbin,2)
          ;(evalfentryin,2)
          ;(evalfreturnin,2)
          ;(evalfstart,2)
          ;(evalfstop,2)}
        Rule Graph:
          [0->{1},1->{3},2->{11},3->{4,5,6},4->{7,8},5->{7,8},6->{11},7->{9},8->{10},9->{2,3},10->{2,3},11->{}]
    + Applied Processor:
        Unfold
    + Details:
        ()
* Step 4: AddSinks MAYBE
    + Considered Problem:
        Rules:
          evalfstart.0(A,B)     -> evalfentryin.1(A,B)       True
          evalfentryin.1(A,B)   -> evalfbb3in.3(B,A)         [A >= 1 && B >= 1 + A]
          evalfbb3in.2(A,B)     -> evalfreturnin.11(A,B)     [0 >= A]
          evalfbb3in.3(A,B)     -> evalfbb4in.4(A,B)         [A >= 1]
          evalfbb3in.3(A,B)     -> evalfbb4in.5(A,B)         [A >= 1]
          evalfbb3in.3(A,B)     -> evalfbb4in.6(A,B)         [A >= 1]
          evalfbb4in.4(A,B)     -> evalfbbin.7(A,B)          [0 >= 1 + C]
          evalfbb4in.4(A,B)     -> evalfbbin.8(A,B)          [0 >= 1 + C]
          evalfbb4in.5(A,B)     -> evalfbbin.7(A,B)          [C >= 1]
          evalfbb4in.5(A,B)     -> evalfbbin.8(A,B)          [C >= 1]
          evalfbb4in.6(A,B)     -> evalfreturnin.11(A,B)     True
          evalfbbin.7(A,B)      -> evalfbb1in.9(A,B)         [B >= 1 + A]
          evalfbbin.8(A,B)      -> evalfbb2in.10(A,B)        [A >= B]
          evalfbb1in.9(A,B)     -> evalfbb3in.2(1 + A,B)     True
          evalfbb1in.9(A,B)     -> evalfbb3in.3(1 + A,B)     True
          evalfbb2in.10(A,B)    -> evalfbb3in.2(A + -1*B,B)  True
          evalfbb2in.10(A,B)    -> evalfbb3in.3(A + -1*B,B)  True
          evalfreturnin.11(A,B) -> evalfstop.12(A,B)         True
        Signature:
          {(evalfbb1in.9,2)
          ;(evalfbb2in.10,2)
          ;(evalfbb3in.2,2)
          ;(evalfbb3in.3,2)
          ;(evalfbb4in.4,2)
          ;(evalfbb4in.5,2)
          ;(evalfbb4in.6,2)
          ;(evalfbbin.7,2)
          ;(evalfbbin.8,2)
          ;(evalfentryin.1,2)
          ;(evalfreturnin.11,2)
          ;(evalfstart.0,2)
          ;(evalfstop.12,2)}
        Rule Graph:
          [0->{1},1->{3,4,5},2->{17},3->{6,7},4->{8,9},5->{10},6->{11},7->{12},8->{11},9->{12},10->{17},11->{13,14}
          ,12->{15,16},13->{2},14->{3,4,5},15->{2},16->{3,4,5},17->{}]
    + Applied Processor:
        AddSinks
    + Details:
        ()
* Step 5: Failure MAYBE
  + Considered Problem:
      Rules:
        evalfstart.0(A,B)     -> evalfentryin.1(A,B)       True
        evalfentryin.1(A,B)   -> evalfbb3in.3(B,A)         [A >= 1 && B >= 1 + A]
        evalfbb3in.2(A,B)     -> evalfreturnin.11(A,B)     [0 >= A]
        evalfbb3in.3(A,B)     -> evalfbb4in.4(A,B)         [A >= 1]
        evalfbb3in.3(A,B)     -> evalfbb4in.5(A,B)         [A >= 1]
        evalfbb3in.3(A,B)     -> evalfbb4in.6(A,B)         [A >= 1]
        evalfbb4in.4(A,B)     -> evalfbbin.7(A,B)          [0 >= 1 + C]
        evalfbb4in.4(A,B)     -> evalfbbin.8(A,B)          [0 >= 1 + C]
        evalfbb4in.5(A,B)     -> evalfbbin.7(A,B)          [C >= 1]
        evalfbb4in.5(A,B)     -> evalfbbin.8(A,B)          [C >= 1]
        evalfbb4in.6(A,B)     -> evalfreturnin.11(A,B)     True
        evalfbbin.7(A,B)      -> evalfbb1in.9(A,B)         [B >= 1 + A]
        evalfbbin.8(A,B)      -> evalfbb2in.10(A,B)        [A >= B]
        evalfbb1in.9(A,B)     -> evalfbb3in.2(1 + A,B)     True
        evalfbb1in.9(A,B)     -> evalfbb3in.3(1 + A,B)     True
        evalfbb2in.10(A,B)    -> evalfbb3in.2(A + -1*B,B)  True
        evalfbb2in.10(A,B)    -> evalfbb3in.3(A + -1*B,B)  True
        evalfreturnin.11(A,B) -> evalfstop.12(A,B)         True
        evalfstop.12(A,B)     -> exitus616(A,B)            True
        evalfstop.12(A,B)     -> exitus616(A,B)            True
        evalfstop.12(A,B)     -> exitus616(A,B)            True
      Signature:
        {(evalfbb1in.9,2)
        ;(evalfbb2in.10,2)
        ;(evalfbb3in.2,2)
        ;(evalfbb3in.3,2)
        ;(evalfbb4in.4,2)
        ;(evalfbb4in.5,2)
        ;(evalfbb4in.6,2)
        ;(evalfbbin.7,2)
        ;(evalfbbin.8,2)
        ;(evalfentryin.1,2)
        ;(evalfreturnin.11,2)
        ;(evalfstart.0,2)
        ;(evalfstop.12,2)
        ;(exitus616,2)}
      Rule Graph:
        [0->{1},1->{3,4,5},2->{17},3->{6,7},4->{8,9},5->{10},6->{11},7->{12},8->{11},9->{12},10->{17},11->{13,14}
        ,12->{15,16},13->{2},14->{3,4,5},15->{2},16->{3,4,5},17->{18,19,20}]
  + 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]
        |
        `- p:[3,14,11,6,8,4,16,12,7,9] c: []
MAYBE