YES
Time: 0.002331
TRS:
 {            f X -> n__f X,
          f f a() -> f g n__f n__a(),
              a() -> n__a(),
       activate X -> X,
  activate n__f X -> f activate X,
  activate n__a() -> a()}
 DP:
  DP:
   {        f# f a() -> f# g n__f n__a(),
    activate# n__f X -> f# activate X,
    activate# n__f X -> activate# X,
    activate# n__a() -> a#()}
  TRS:
  {            f X -> n__f X,
           f f a() -> f g n__f n__a(),
               a() -> n__a(),
        activate X -> X,
   activate n__f X -> f activate X,
   activate n__a() -> a()}
  UR:
   {            f X -> n__f X,
            f f a() -> f g n__f n__a(),
                a() -> n__a(),
         activate X -> X,
    activate n__f X -> f activate X,
    activate n__a() -> a()}
   EDG:
    {(activate# n__f X -> f# activate X, f# f a() -> f# g n__f n__a())
     (f# f a() -> f# g n__f n__a(), f# f a() -> f# g n__f n__a())
     (activate# n__f X -> activate# X, activate# n__f X -> f# activate X)
     (activate# n__f X -> activate# X, activate# n__f X -> activate# X)
     (activate# n__f X -> activate# X, activate# n__a() -> a#())}
    EDG:
     {(activate# n__f X -> f# activate X, f# f a() -> f# g n__f n__a())
      (activate# n__f X -> activate# X, activate# n__f X -> f# activate X)
      (activate# n__f X -> activate# X, activate# n__f X -> activate# X)
      (activate# n__f X -> activate# X, activate# n__a() -> a#())}
     EDG:
      {(activate# n__f X -> f# activate X, f# f a() -> f# g n__f n__a())
       (activate# n__f X -> activate# X, activate# n__a() -> a#())}
      EDG:
       {(activate# n__f X -> f# activate X, f# f a() -> f# g n__f n__a())
        (activate# n__f X -> activate# X, activate# n__a() -> a#())}
       STATUS:
        arrows: 0.875000
        SCCS (0):