MAYBE
* Step 1: ArgumentFilter MAYBE
    + Considered Problem:
        Rules:
          0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)   -> f2(A,B,C,D,E,F,G,H,S,T,U,V,W,Y,H,H,H,X)   [H >= 1 && G >= 1 + F && 255 >= H] (?,1)
          1. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)   -> f2(A,B,C,D,E,F,G,H,S,T,U,V,W,Y,H,H,H,X)   [H >= 1 && G >= 1 + F && H >= 257] (?,1)
          2. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)   -> f3(A,B,C,D,E,F,G,H,S,T,K,L,M,N,0,0,0,R)   [F >= G]                           (?,1)
          3. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)   -> f1(A,B,C,D,E,F,G,H,S,T,U,V,W,N,O,P,Q,R)   [G >= 1 + F && 0 >= H]             (?,1)
          4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)   -> f1(A,B,C,D,E,F,G,256,S,T,U,V,W,Y,O,P,Q,R) [G >= 1 + F && X >= 1 && H = 256]  (?,1)
          5. f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(S,T,U,V,W,F,G,H,I,J,K,L,M,N,O,P,Q,R)   True                               (1,1)
        Signature:
          {(f1,18);(f2,18);(f3,18);(f300,18)}
        Flow Graph:
          [0->{},1->{},2->{},3->{0,1,2,3,4},4->{0,1,2,3,4},5->{0,1,2,3,4}]
        
    + Applied Processor:
        ArgumentFilter [0,1,2,3,4,8,9,10,11,12,13,14,15,16,17]
    + Details:
        We remove following argument positions: [0,1,2,3,4,8,9,10,11,12,13,14,15,16,17].
* Step 2: UnsatPaths MAYBE
    + Considered Problem:
        Rules:
          0. f1(F,G,H)   -> f2(F,G,H)   [H >= 1 && G >= 1 + F && 255 >= H] (?,1)
          1. f1(F,G,H)   -> f2(F,G,H)   [H >= 1 && G >= 1 + F && H >= 257] (?,1)
          2. f1(F,G,H)   -> f3(F,G,H)   [F >= G]                           (?,1)
          3. f1(F,G,H)   -> f1(F,G,H)   [G >= 1 + F && 0 >= H]             (?,1)
          4. f1(F,G,H)   -> f1(F,G,256) [G >= 1 + F && X >= 1 && H = 256]  (?,1)
          5. f300(F,G,H) -> f1(F,G,H)   True                               (1,1)
        Signature:
          {(f1,18);(f2,18);(f3,18);(f300,18)}
        Flow Graph:
          [0->{},1->{},2->{},3->{0,1,2,3,4},4->{0,1,2,3,4},5->{0,1,2,3,4}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(3,0),(3,1),(3,2),(3,4),(4,0),(4,1),(4,2),(4,3)]
* Step 3: FromIts MAYBE
    + Considered Problem:
        Rules:
          0. f1(F,G,H)   -> f2(F,G,H)   [H >= 1 && G >= 1 + F && 255 >= H] (?,1)
          1. f1(F,G,H)   -> f2(F,G,H)   [H >= 1 && G >= 1 + F && H >= 257] (?,1)
          2. f1(F,G,H)   -> f3(F,G,H)   [F >= G]                           (?,1)
          3. f1(F,G,H)   -> f1(F,G,H)   [G >= 1 + F && 0 >= H]             (?,1)
          4. f1(F,G,H)   -> f1(F,G,256) [G >= 1 + F && X >= 1 && H = 256]  (?,1)
          5. f300(F,G,H) -> f1(F,G,H)   True                               (1,1)
        Signature:
          {(f1,18);(f2,18);(f3,18);(f300,18)}
        Flow Graph:
          [0->{},1->{},2->{},3->{3},4->{4},5->{0,1,2,3,4}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 4: AddSinks MAYBE
    + Considered Problem:
        Rules:
          f1(F,G,H)   -> f2(F,G,H)    [H >= 1 && G >= 1 + F && 255 >= H]
          f1(F,G,H)   -> f2(F,G,H)    [H >= 1 && G >= 1 + F && H >= 257]
          f1(F,G,H)   -> f3(F,G,H)    [F >= G]
          f1(F,G,H)   -> f1(F,G,H)    [G >= 1 + F && 0 >= H]
          f1(F,G,H)   -> f1(F,G,256)  [G >= 1 + F && X >= 1 && H = 256]
          f300(F,G,H) -> f1(F,G,H)    True
        Signature:
          {(f1,18);(f2,18);(f3,18);(f300,18)}
        Rule Graph:
          [0->{},1->{},2->{},3->{3},4->{4},5->{0,1,2,3,4}]
    + Applied Processor:
        AddSinks
    + Details:
        ()
* Step 5: Failure MAYBE
  + Considered Problem:
      Rules:
        f1(F,G,H)   -> f2(F,G,H)         [H >= 1 && G >= 1 + F && 255 >= H]
        f1(F,G,H)   -> f2(F,G,H)         [H >= 1 && G >= 1 + F && H >= 257]
        f1(F,G,H)   -> f3(F,G,H)         [F >= G]
        f1(F,G,H)   -> f1(F,G,H)         [G >= 1 + F && 0 >= H]
        f1(F,G,H)   -> f1(F,G,256)       [G >= 1 + F && X >= 1 && H = 256]
        f300(F,G,H) -> f1(F,G,H)         True
        f1(F,G,H)   -> exitus616(F,G,H)  True
        f1(F,G,H)   -> exitus616(F,G,H)  True
        f3(F,G,H)   -> exitus616(F,G,H)  True
        f2(F,G,H)   -> exitus616(F,G,H)  True
        f2(F,G,H)   -> exitus616(F,G,H)  True
      Signature:
        {(exitus616,3);(f1,18);(f2,18);(f3,18);(f300,18)}
      Rule Graph:
        [0->{10},1->{9},2->{8},3->{3,7},4->{4,6},5->{0,1,2,3,4}]
  + Applied Processor:
      Decompose Greedy
  + Details:
      We construct a looptree:
        P: [0,1,2,3,4,5,6,7,8,9,10]
        |
        +- p:[4] c: []
        |
        `- p:[3] c: []
MAYBE