MAYBE
Time: 0.036517
TRS:
 {      mark f X -> active f mark X,
        mark g X -> active g X,
        mark a() -> active a(),
        f mark X -> f X,
      f active X -> f X,
        g mark X -> g X,
      g active X -> g X,
  active f f a() -> mark f g f a()}
 DP:
  DP:
   {      mark# f X -> mark# X,
          mark# f X -> f# mark X,
          mark# f X -> active# f mark X,
          mark# g X -> active# g X,
          mark# a() -> active# a(),
          f# mark X -> f# X,
        f# active X -> f# X,
          g# mark X -> g# X,
        g# active X -> g# X,
    active# f f a() -> mark# f g f a(),
    active# f f a() -> f# g f a(),
    active# f f a() -> g# f a()}
  TRS:
  {      mark f X -> active f mark X,
         mark g X -> active g X,
         mark a() -> active a(),
         f mark X -> f X,
       f active X -> f X,
         g mark X -> g X,
       g active X -> g X,
   active f f a() -> mark f g f a()}
  EDG:
   {(active# f f a() -> g# f a(), g# active X -> g# X)
    (active# f f a() -> g# f a(), g# mark X -> g# X)
    (f# mark X -> f# X, f# active X -> f# X)
    (f# mark X -> f# X, f# mark X -> f# X)
    (g# mark X -> g# X, g# active X -> g# X)
    (g# mark X -> g# X, g# mark X -> g# X)
    (mark# f X -> f# mark X, f# active X -> f# X)
    (mark# f X -> f# mark X, f# mark X -> f# X)
    (mark# a() -> active# a(), active# f f a() -> g# f a())
    (mark# a() -> active# a(), active# f f a() -> f# g f a())
    (mark# a() -> active# a(), active# f f a() -> mark# f g f a())
    (active# f f a() -> f# g f a(), f# active X -> f# X)
    (active# f f a() -> f# g f a(), f# mark X -> f# X)
    (active# f f a() -> mark# f g f a(), mark# f X -> mark# X)
    (active# f f a() -> mark# f g f a(), mark# f X -> f# mark X)
    (active# f f a() -> mark# f g f a(), mark# f X -> active# f mark X)
    (active# f f a() -> mark# f g f a(), mark# g X -> active# g X)
    (active# f f a() -> mark# f g f a(), mark# a() -> active# a())
    (mark# g X -> active# g X, active# f f a() -> mark# f g f a())
    (mark# g X -> active# g X, active# f f a() -> f# g f a())
    (mark# g X -> active# g X, active# f f a() -> g# f a())
    (g# active X -> g# X, g# mark X -> g# X)
    (g# active X -> g# X, g# active X -> g# X)
    (f# active X -> f# X, f# mark X -> f# X)
    (f# active X -> f# X, f# active X -> f# X)
    (mark# f X -> mark# X, mark# f X -> mark# X)
    (mark# f X -> mark# X, mark# f X -> f# mark X)
    (mark# f X -> mark# X, mark# f X -> active# f mark X)
    (mark# f X -> mark# X, mark# g X -> active# g X)
    (mark# f X -> mark# X, mark# a() -> active# a())
    (mark# f X -> active# f mark X, active# f f a() -> mark# f g f a())
    (mark# f X -> active# f mark X, active# f f a() -> f# g f a())
    (mark# f X -> active# f mark X, active# f f a() -> g# f a())}
   EDG:
    {(f# mark X -> f# X, f# active X -> f# X)
     (f# mark X -> f# X, f# mark X -> f# X)
     (g# mark X -> g# X, g# active X -> g# X)
     (g# mark X -> g# X, g# mark X -> g# X)
     (mark# f X -> f# mark X, f# active X -> f# X)
     (mark# f X -> f# mark X, f# mark X -> f# X)
     (active# f f a() -> mark# f g f a(), mark# f X -> mark# X)
     (active# f f a() -> mark# f g f a(), mark# f X -> f# mark X)
     (active# f f a() -> mark# f g f a(), mark# f X -> active# f mark X)
     (mark# g X -> active# g X, active# f f a() -> mark# f g f a())
     (mark# g X -> active# g X, active# f f a() -> f# g f a())
     (mark# g X -> active# g X, active# f f a() -> g# f a())
     (g# active X -> g# X, g# mark X -> g# X)
     (g# active X -> g# X, g# active X -> g# X)
     (f# active X -> f# X, f# mark X -> f# X)
     (f# active X -> f# X, f# active X -> f# X)
     (mark# f X -> mark# X, mark# f X -> mark# X)
     (mark# f X -> mark# X, mark# f X -> f# mark X)
     (mark# f X -> mark# X, mark# f X -> active# f mark X)
     (mark# f X -> mark# X, mark# g X -> active# g X)
     (mark# f X -> mark# X, mark# a() -> active# a())
     (mark# f X -> active# f mark X, active# f f a() -> mark# f g f a())
     (mark# f X -> active# f mark X, active# f f a() -> f# g f a())
     (mark# f X -> active# f mark X, active# f f a() -> g# f a())}
    EDG:
     {(mark# f X -> f# mark X, f# active X -> f# X)
      (mark# f X -> f# mark X, f# mark X -> f# X)
      (active# f f a() -> mark# f g f a(), mark# f X -> mark# X)
      (active# f f a() -> mark# f g f a(), mark# f X -> f# mark X)
      (active# f f a() -> mark# f g f a(), mark# f X -> active# f mark X)
      (mark# f X -> mark# X, mark# f X -> mark# X)
      (mark# f X -> mark# X, mark# f X -> f# mark X)
      (mark# f X -> mark# X, mark# f X -> active# f mark X)
      (mark# f X -> mark# X, mark# g X -> active# g X)}
     EDG:
      {(mark# f X -> f# mark X, f# active X -> f# X)
       (mark# f X -> f# mark X, f# mark X -> f# X)
       (active# f f a() -> mark# f g f a(), mark# f X -> mark# X)
       (active# f f a() -> mark# f g f a(), mark# f X -> f# mark X)
       (active# f f a() -> mark# f g f a(), mark# f X -> active# f mark X)
       (mark# f X -> mark# X, mark# f X -> mark# X)
       (mark# f X -> mark# X, mark# f X -> f# mark X)
       (mark# f X -> mark# X, mark# f X -> active# f mark X)
       (mark# f X -> mark# X, mark# g X -> active# g X)}
      STATUS:
       arrows: 0.937500
       SCCS (1):
        Scc:
         {mark# f X -> mark# X}
        
        
        
        
        
        
        SCC (1):
         Strict:
          {mark# f X -> mark# X}
         Weak:
         {      mark f X -> active f mark X,
                mark g X -> active g X,
                mark a() -> active a(),
                f mark X -> f X,
              f active X -> f X,
                g mark X -> g X,
              g active X -> g X,
          active f f a() -> mark f g f a()}
         Open