MAYBE
* Step 1: UnsatPaths MAYBE
    + Considered Problem:
        Rules:
          0. f0(A,B,C,D,E) -> f1(F,1,0,D,E)            True                                     (1,1)
          1. f1(A,B,C,D,E) -> f1(-10 + A,-1 + B,C,D,E) [C >= 0 && B >= 1 && A >= 101]           (?,1)
          2. f1(A,B,C,D,E) -> f1(11 + A,1 + B,C,D,E)   [C >= 0 && B >= 1 && 100 >= A]           (?,1)
          3. f1(A,B,C,D,E) -> f1(-10 + A,-1 + B,1,A,B) [C >= 0 && A >= 101 && 0 >= C && B >= 1] (?,1)
          4. f1(A,B,C,D,E) -> f1(11 + A,1 + B,1,A,B)   [C >= 0 && 100 >= A && 0 >= C && B >= 1] (?,1)
          5. f1(A,B,C,D,E) -> f2(A,B,C,D,E)            [C >= 0 && D >= A && C >= 1 && B >= E]   (?,1)
        Signature:
          {(f0,5);(f1,5);(f2,5)}
        Flow Graph:
          [0->{1,2,3,4,5},1->{1,2,3,4,5},2->{1,2,3,4,5},3->{1,2,3,4,5},4->{1,2,3,4,5},5->{}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(0,5),(3,3),(3,4),(3,5),(4,3),(4,4),(4,5)]
* Step 2: TrivialSCCs MAYBE
    + Considered Problem:
        Rules:
          0. f0(A,B,C,D,E) -> f1(F,1,0,D,E)            True                                     (1,1)
          1. f1(A,B,C,D,E) -> f1(-10 + A,-1 + B,C,D,E) [C >= 0 && B >= 1 && A >= 101]           (?,1)
          2. f1(A,B,C,D,E) -> f1(11 + A,1 + B,C,D,E)   [C >= 0 && B >= 1 && 100 >= A]           (?,1)
          3. f1(A,B,C,D,E) -> f1(-10 + A,-1 + B,1,A,B) [C >= 0 && A >= 101 && 0 >= C && B >= 1] (?,1)
          4. f1(A,B,C,D,E) -> f1(11 + A,1 + B,1,A,B)   [C >= 0 && 100 >= A && 0 >= C && B >= 1] (?,1)
          5. f1(A,B,C,D,E) -> f2(A,B,C,D,E)            [C >= 0 && D >= A && C >= 1 && B >= E]   (?,1)
        Signature:
          {(f0,5);(f1,5);(f2,5)}
        Flow Graph:
          [0->{1,2,3,4},1->{1,2,3,4,5},2->{1,2,3,4,5},3->{1,2},4->{1,2},5->{}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 3: PolyRank MAYBE
    + Considered Problem:
        Rules:
          0. f0(A,B,C,D,E) -> f1(F,1,0,D,E)            True                                     (1,1)
          1. f1(A,B,C,D,E) -> f1(-10 + A,-1 + B,C,D,E) [C >= 0 && B >= 1 && A >= 101]           (?,1)
          2. f1(A,B,C,D,E) -> f1(11 + A,1 + B,C,D,E)   [C >= 0 && B >= 1 && 100 >= A]           (?,1)
          3. f1(A,B,C,D,E) -> f1(-10 + A,-1 + B,1,A,B) [C >= 0 && A >= 101 && 0 >= C && B >= 1] (?,1)
          4. f1(A,B,C,D,E) -> f1(11 + A,1 + B,1,A,B)   [C >= 0 && 100 >= A && 0 >= C && B >= 1] (?,1)
          5. f1(A,B,C,D,E) -> f2(A,B,C,D,E)            [C >= 0 && D >= A && C >= 1 && B >= E]   (1,1)
        Signature:
          {(f0,5);(f1,5);(f2,5)}
        Flow Graph:
          [0->{1,2,3,4},1->{1,2,3,4,5},2->{1,2,3,4,5},3->{1,2},4->{1,2},5->{}]
        
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(f0) = 1        
          p(f1) = 1 + -1*x3
          p(f2) = 1 + -1*x3
        
        Following rules are strictly oriented:
        [C >= 0 && 100 >= A && 0 >= C && B >= 1] ==>                       
                                   f1(A,B,C,D,E)   = 1 + -1*C              
                                                   > 0                     
                                                   = f1(11 + A,1 + B,1,A,B)
        
        
        Following rules are weakly oriented:
                                            True ==>                         
                                   f0(A,B,C,D,E)   = 1                       
                                                  >= 1                       
                                                   = f1(F,1,0,D,E)           
        
                  [C >= 0 && B >= 1 && A >= 101] ==>                         
                                   f1(A,B,C,D,E)   = 1 + -1*C                
                                                  >= 1 + -1*C                
                                                   = f1(-10 + A,-1 + B,C,D,E)
        
                  [C >= 0 && B >= 1 && 100 >= A] ==>                         
                                   f1(A,B,C,D,E)   = 1 + -1*C                
                                                  >= 1 + -1*C                
                                                   = f1(11 + A,1 + B,C,D,E)  
        
        [C >= 0 && A >= 101 && 0 >= C && B >= 1] ==>                         
                                   f1(A,B,C,D,E)   = 1 + -1*C                
                                                  >= 0                       
                                                   = f1(-10 + A,-1 + B,1,A,B)
        
          [C >= 0 && D >= A && C >= 1 && B >= E] ==>                         
                                   f1(A,B,C,D,E)   = 1 + -1*C                
                                                  >= 1 + -1*C                
                                                   = f2(A,B,C,D,E)           
        
        
* Step 4: PolyRank MAYBE
    + Considered Problem:
        Rules:
          0. f0(A,B,C,D,E) -> f1(F,1,0,D,E)            True                                     (1,1)
          1. f1(A,B,C,D,E) -> f1(-10 + A,-1 + B,C,D,E) [C >= 0 && B >= 1 && A >= 101]           (?,1)
          2. f1(A,B,C,D,E) -> f1(11 + A,1 + B,C,D,E)   [C >= 0 && B >= 1 && 100 >= A]           (?,1)
          3. f1(A,B,C,D,E) -> f1(-10 + A,-1 + B,1,A,B) [C >= 0 && A >= 101 && 0 >= C && B >= 1] (?,1)
          4. f1(A,B,C,D,E) -> f1(11 + A,1 + B,1,A,B)   [C >= 0 && 100 >= A && 0 >= C && B >= 1] (1,1)
          5. f1(A,B,C,D,E) -> f2(A,B,C,D,E)            [C >= 0 && D >= A && C >= 1 && B >= E]   (1,1)
        Signature:
          {(f0,5);(f1,5);(f2,5)}
        Flow Graph:
          [0->{1,2,3,4},1->{1,2,3,4,5},2->{1,2,3,4,5},3->{1,2},4->{1,2},5->{}]
        
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
          p(f0) = 1        
          p(f1) = 1 + -1*x3
          p(f2) = 1 + -1*x3
        
        Following rules are strictly oriented:
        [C >= 0 && A >= 101 && 0 >= C && B >= 1] ==>                         
                                   f1(A,B,C,D,E)   = 1 + -1*C                
                                                   > 0                       
                                                   = f1(-10 + A,-1 + B,1,A,B)
        
        [C >= 0 && 100 >= A && 0 >= C && B >= 1] ==>                         
                                   f1(A,B,C,D,E)   = 1 + -1*C                
                                                   > 0                       
                                                   = f1(11 + A,1 + B,1,A,B)  
        
        
        Following rules are weakly oriented:
                                          True ==>                         
                                 f0(A,B,C,D,E)   = 1                       
                                                >= 1                       
                                                 = f1(F,1,0,D,E)           
        
                [C >= 0 && B >= 1 && A >= 101] ==>                         
                                 f1(A,B,C,D,E)   = 1 + -1*C                
                                                >= 1 + -1*C                
                                                 = f1(-10 + A,-1 + B,C,D,E)
        
                [C >= 0 && B >= 1 && 100 >= A] ==>                         
                                 f1(A,B,C,D,E)   = 1 + -1*C                
                                                >= 1 + -1*C                
                                                 = f1(11 + A,1 + B,C,D,E)  
        
        [C >= 0 && D >= A && C >= 1 && B >= E] ==>                         
                                 f1(A,B,C,D,E)   = 1 + -1*C                
                                                >= 1 + -1*C                
                                                 = f2(A,B,C,D,E)           
        
        
* Step 5: Failure MAYBE
  + Considered Problem:
      Rules:
        0. f0(A,B,C,D,E) -> f1(F,1,0,D,E)            True                                     (1,1)
        1. f1(A,B,C,D,E) -> f1(-10 + A,-1 + B,C,D,E) [C >= 0 && B >= 1 && A >= 101]           (?,1)
        2. f1(A,B,C,D,E) -> f1(11 + A,1 + B,C,D,E)   [C >= 0 && B >= 1 && 100 >= A]           (?,1)
        3. f1(A,B,C,D,E) -> f1(-10 + A,-1 + B,1,A,B) [C >= 0 && A >= 101 && 0 >= C && B >= 1] (1,1)
        4. f1(A,B,C,D,E) -> f1(11 + A,1 + B,1,A,B)   [C >= 0 && 100 >= A && 0 >= C && B >= 1] (1,1)
        5. f1(A,B,C,D,E) -> f2(A,B,C,D,E)            [C >= 0 && D >= A && C >= 1 && B >= E]   (1,1)
      Signature:
        {(f0,5);(f1,5);(f2,5)}
      Flow Graph:
        [0->{1,2,3,4},1->{1,2,3,4,5},2->{1,2,3,4,5},3->{1,2},4->{1,2},5->{}]
      
  + Applied Processor:
      Failing "Open problems left."
  + Details:
      Open problems left.
MAYBE