YES
Time: 0.014915
TRS:
 {    a__f X -> f X,
  a__f f a() -> c f g f a(),
    mark c X -> c X,
    mark f X -> a__f mark X,
    mark g X -> g mark X,
    mark a() -> a()}
 DP:
  DP:
   {mark# f X -> a__f# mark X,
    mark# f X -> mark# X,
    mark# g X -> mark# X}
  TRS:
  {    a__f X -> f X,
   a__f f a() -> c f g f a(),
     mark c X -> c X,
     mark f X -> a__f mark X,
     mark g X -> g mark X,
     mark a() -> a()}
  EDG:
   {(mark# g X -> mark# X, mark# g X -> mark# X)
    (mark# g X -> mark# X, mark# f X -> mark# X)
    (mark# g X -> mark# X, mark# f X -> a__f# mark X)
    (mark# f X -> mark# X, mark# f X -> a__f# mark X)
    (mark# f X -> mark# X, mark# f X -> mark# X)
    (mark# f X -> mark# X, mark# g X -> mark# X)}
   STATUS:
    arrows: 0.333333
    SCCS (1):
     Scc:
      {mark# f X -> mark# X,
       mark# g X -> mark# X}
     
     SCC (2):
      Strict:
       {mark# f X -> mark# X,
        mark# g X -> mark# X}
      Weak:
      {    a__f X -> f X,
       a__f f a() -> c f g f a(),
         mark c X -> c X,
         mark f X -> a__f mark X,
         mark g X -> g mark X,
         mark a() -> a()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [c](x0) = x0,
        
        [f](x0) = x0,
        
        [g](x0) = x0 + 1,
        
        [a__f](x0) = x0 + 1,
        
        [mark](x0) = 0,
        
        [a] = 1,
        
        [mark#](x0) = x0
       Strict:
        mark# g X -> mark# X
        1 + 1X >= 0 + 1X
        mark# f X -> mark# X
        0 + 1X >= 0 + 1X
       Weak:
        mark a() -> a()
        0 >= 1
        mark g X -> g mark X
        0 + 0X >= 1 + 0X
        mark f X -> a__f mark X
        0 + 0X >= 1 + 0X
        mark c X -> c X
        0 + 0X >= 0 + 1X
        a__f f a() -> c f g f a()
        2 >= 2
        a__f X -> f X
        1 + 1X >= 0 + 1X
      SCCS (1):
       Scc:
        {mark# f X -> mark# X}
       
       SCC (1):
        Strict:
         {mark# f X -> mark# X}
        Weak:
        {    a__f X -> f X,
         a__f f a() -> c f g f a(),
           mark c X -> c X,
           mark f X -> a__f mark X,
           mark g X -> g mark X,
           mark a() -> a()}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [c](x0) = 0,
          
          [f](x0) = x0 + 1,
          
          [g](x0) = 0,
          
          [a__f](x0) = 0,
          
          [mark](x0) = 0,
          
          [a] = 1,
          
          [mark#](x0) = x0
         Strict:
          mark# f X -> mark# X
          1 + 1X >= 0 + 1X
         Weak:
          mark a() -> a()
          0 >= 1
          mark g X -> g mark X
          0 + 0X >= 0 + 0X
          mark f X -> a__f mark X
          0 + 0X >= 0 + 0X
          mark c X -> c X
          0 + 0X >= 0 + 0X
          a__f f a() -> c f g f a()
          0 >= 0
          a__f X -> f X
          0 + 0X >= 1 + 1X
        Qed