YES(?,O(1))
* Step 1: TrivialSCCs WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N)  -> f11(100,O,1,D,E,F,G,H,I,J,K,L,M,N)  True                  (1,1)
          1.  f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N)  -> f11(100,O,0,D,E,F,G,H,I,J,K,L,M,N)  True                  (1,1)
          2.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f23(A,B,1,1,1,100,O,1,I,J,K,L,M,N)  [C = 1]               (?,1)
          3.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f23(A,B,1,1,1,100,O,0,I,J,K,L,M,N)  [C = 1]               (?,1)
          4.  f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f26(A,B,C,D,H,F,G,H,100,J,K,L,M,N)  [0 >= H]              (?,1)
          5.  f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f26(A,B,C,D,H,F,G,H,100,J,K,L,M,N)  [H >= 2]              (?,1)
          6.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f36(A,B,C,C,C,F,G,H,I,100,K,L,M,N)  [0 >= C]              (?,1)
          7.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f36(A,B,C,C,C,F,G,H,I,100,K,L,M,N)  [C >= 2]              (?,1)
          8.  f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,O,P,M,N)    [0 >= 2 + O && H = 1] (?,1)
          9.  f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,O,P,M,N)    [O >= 0 && H = 1]     (?,1)
          10. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,-1,L,100,O) [H = 1]               (?,1)
          11. f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N)    [0 >= 1 + O]          (?,1)
          12. f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N)    True                  (?,1)
          13. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N)    [0 >= 1 + O]          (?,1)
          14. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N)    True                  (?,1)
        Signature:
          {(f0,14);(f11,14);(f23,14);(f26,14);(f32,14);(f36,14)}
        Flow Graph:
          [0->{2,3,6,7},1->{2,3,6,7},2->{4,5,8,9,10},3->{4,5,8,9,10},4->{13,14},5->{13,14},6->{11,12},7->{11,12}
          ,8->{},9->{},10->{},11->{},12->{},13->{},14->{}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: UnsatRules WORST_CASE(?,O(1))
    + Considered Problem:
        Rules:
          0.  f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N)  -> f11(100,O,1,D,E,F,G,H,I,J,K,L,M,N)  True                  (1,1)
          1.  f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N)  -> f11(100,O,0,D,E,F,G,H,I,J,K,L,M,N)  True                  (1,1)
          2.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f23(A,B,1,1,1,100,O,1,I,J,K,L,M,N)  [C = 1]               (1,1)
          3.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f23(A,B,1,1,1,100,O,0,I,J,K,L,M,N)  [C = 1]               (1,1)
          4.  f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f26(A,B,C,D,H,F,G,H,100,J,K,L,M,N)  [0 >= H]              (1,1)
          5.  f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f26(A,B,C,D,H,F,G,H,100,J,K,L,M,N)  [H >= 2]              (1,1)
          6.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f36(A,B,C,C,C,F,G,H,I,100,K,L,M,N)  [0 >= C]              (1,1)
          7.  f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f36(A,B,C,C,C,F,G,H,I,100,K,L,M,N)  [C >= 2]              (1,1)
          8.  f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,O,P,M,N)    [0 >= 2 + O && H = 1] (1,1)
          9.  f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,O,P,M,N)    [O >= 0 && H = 1]     (1,1)
          10. f23(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,1,F,G,1,I,J,-1,L,100,O) [H = 1]               (1,1)
          11. f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N)    [0 >= 1 + O]          (1,1)
          12. f36(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N)    True                  (1,1)
          13. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N)    [0 >= 1 + O]          (1,1)
          14. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N)    True                  (1,1)
        Signature:
          {(f0,14);(f11,14);(f23,14);(f26,14);(f32,14);(f36,14)}
        Flow Graph:
          [0->{2,3,6,7},1->{2,3,6,7},2->{4,5,8,9,10},3->{4,5,8,9,10},4->{13,14},5->{13,14},6->{11,12},7->{11,12}
          ,8->{},9->{},10->{},11->{},12->{},13->{},14->{}]
        
    + Applied Processor:
        UnsatRules
    + Details:
        The problem is already solved.

YES(?,O(1))