YES(?,O(n^1))
TRS:
 {
    a__f X -> f X,
  a__f g X -> g X,
    a__c() -> a__f g c(),
    a__c() -> c(),
  mark f X -> a__f X,
  mark g X -> g X,
  mark c() -> a__c()
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
      a__f X -> f X,
    a__f g X -> g X,
      a__c() -> a__f g c(),
      a__c() -> c(),
    mark f X -> a__f X,
    mark g X -> g X,
    mark c() -> a__c()
   }
  Natural interpretation:
   Strict:
    {
       a__f X -> f X,
     a__f g X -> g X,
       a__c() -> a__f g c(),
       a__c() -> c(),
     mark f X -> a__f X,
     mark g X -> g X,
     mark c() -> a__c()
    }
   Weak:
    {}
   Interpretation class: stronglylinear
   [mark](X0) = + 1*X0 + 7
   [a__c] = + 5
   [c] = + 0
   [a__f](X0) = + 1*X0 + 2
   [g](X0) = + 1*X0 + 0
   [f](X0) = + 1*X0 + 1
   
   Qed