MAYBE
Time: 0.007671
TRS:
 {  mark f(X1, X2) -> active f(mark X1, X2),
          mark g X -> active g mark X,
    f(X1, mark X2) -> f(X1, X2),
  f(X1, active X2) -> f(X1, X2),
    f(mark X1, X2) -> f(X1, X2),
  f(active X1, X2) -> f(X1, X2),
          g mark X -> g X,
        g active X -> g X,
  active f(g X, Y) -> mark f(X, f(g X, Y))}
 DP:
  DP:
   {  mark# f(X1, X2) -> mark# X1,
      mark# f(X1, X2) -> f#(mark X1, X2),
      mark# f(X1, X2) -> active# f(mark X1, X2),
            mark# g X -> mark# X,
            mark# g X -> g# mark X,
            mark# g X -> active# g mark X,
      f#(X1, mark X2) -> f#(X1, X2),
    f#(X1, active X2) -> f#(X1, X2),
      f#(mark X1, X2) -> f#(X1, X2),
    f#(active X1, X2) -> f#(X1, X2),
            g# mark X -> g# X,
          g# active X -> g# X,
    active# f(g X, Y) -> mark# f(X, f(g X, Y)),
    active# f(g X, Y) -> f#(X, f(g X, Y))}
  TRS:
  {  mark f(X1, X2) -> active f(mark X1, X2),
           mark g X -> active g mark X,
     f(X1, mark X2) -> f(X1, X2),
   f(X1, active X2) -> f(X1, X2),
     f(mark X1, X2) -> f(X1, X2),
   f(active X1, X2) -> f(X1, X2),
           g mark X -> g X,
         g active X -> g X,
   active f(g X, Y) -> mark f(X, f(g X, Y))}
  UR:
   {  mark f(X1, X2) -> active f(mark X1, X2),
            mark g X -> active g mark X,
      f(X1, mark X2) -> f(X1, X2),
    f(X1, active X2) -> f(X1, X2),
      f(mark X1, X2) -> f(X1, X2),
    f(active X1, X2) -> f(X1, X2),
            g mark X -> g X,
          g active X -> g X,
    active f(g X, Y) -> mark f(X, f(g X, Y))}
   EDG:
    {(active# f(g X, Y) -> f#(X, f(g X, Y)), f#(active X1, X2) -> f#(X1, X2))
     (active# f(g X, Y) -> f#(X, f(g X, Y)), f#(mark X1, X2) -> f#(X1, X2))
     (active# f(g X, Y) -> f#(X, f(g X, Y)), f#(X1, active X2) -> f#(X1, X2))
     (active# f(g X, Y) -> f#(X, f(g X, Y)), f#(X1, mark X2) -> f#(X1, X2))
     (mark# g X -> g# mark X, g# active X -> g# X)
     (mark# g X -> g# mark X, g# mark X -> g# X)
     (f#(X1, active X2) -> f#(X1, X2), f#(active X1, X2) -> f#(X1, X2))
     (f#(X1, active X2) -> f#(X1, X2), f#(mark X1, X2) -> f#(X1, X2))
     (f#(X1, active X2) -> f#(X1, X2), f#(X1, active X2) -> f#(X1, X2))
     (f#(X1, active X2) -> f#(X1, X2), f#(X1, mark X2) -> f#(X1, X2))
     (f#(active X1, X2) -> f#(X1, X2), f#(active X1, X2) -> f#(X1, X2))
     (f#(active X1, X2) -> f#(X1, X2), f#(mark X1, X2) -> f#(X1, X2))
     (f#(active X1, X2) -> f#(X1, X2), f#(X1, active X2) -> f#(X1, X2))
     (f#(active X1, X2) -> f#(X1, X2), f#(X1, mark X2) -> f#(X1, X2))
     (mark# f(X1, X2) -> mark# X1, mark# g X -> active# g mark X)
     (mark# f(X1, X2) -> mark# X1, mark# g X -> g# mark X)
     (mark# f(X1, X2) -> mark# X1, mark# g X -> mark# X)
     (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> active# f(mark X1, X2))
     (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> f#(mark X1, X2))
     (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1)
     (g# mark X -> g# X, g# active X -> g# X)
     (g# mark X -> g# X, g# mark X -> g# X)
     (mark# f(X1, X2) -> f#(mark X1, X2), f#(active X1, X2) -> f#(X1, X2))
     (mark# f(X1, X2) -> f#(mark X1, X2), f#(mark X1, X2) -> f#(X1, X2))
     (mark# f(X1, X2) -> f#(mark X1, X2), f#(X1, active X2) -> f#(X1, X2))
     (mark# f(X1, X2) -> f#(mark X1, X2), f#(X1, mark X2) -> f#(X1, X2))
     (g# active X -> g# X, g# mark X -> g# X)
     (g# active X -> g# X, g# active X -> g# X)
     (mark# g X -> mark# X, mark# f(X1, X2) -> mark# X1)
     (mark# g X -> mark# X, mark# f(X1, X2) -> f#(mark X1, X2))
     (mark# g X -> mark# X, mark# f(X1, X2) -> active# f(mark X1, X2))
     (mark# g X -> mark# X, mark# g X -> mark# X)
     (mark# g X -> mark# X, mark# g X -> g# mark X)
     (mark# g X -> mark# X, mark# g X -> active# g mark X)
     (mark# f(X1, X2) -> active# f(mark X1, X2), active# f(g X, Y) -> mark# f(X, f(g X, Y)))
     (mark# f(X1, X2) -> active# f(mark X1, X2), active# f(g X, Y) -> f#(X, f(g X, Y)))
     (f#(mark X1, X2) -> f#(X1, X2), f#(X1, mark X2) -> f#(X1, X2))
     (f#(mark X1, X2) -> f#(X1, X2), f#(X1, active X2) -> f#(X1, X2))
     (f#(mark X1, X2) -> f#(X1, X2), f#(mark X1, X2) -> f#(X1, X2))
     (f#(mark X1, X2) -> f#(X1, X2), f#(active X1, X2) -> f#(X1, X2))
     (f#(X1, mark X2) -> f#(X1, X2), f#(X1, mark X2) -> f#(X1, X2))
     (f#(X1, mark X2) -> f#(X1, X2), f#(X1, active X2) -> f#(X1, X2))
     (f#(X1, mark X2) -> f#(X1, X2), f#(mark X1, X2) -> f#(X1, X2))
     (f#(X1, mark X2) -> f#(X1, X2), f#(active X1, X2) -> f#(X1, X2))
     (active# f(g X, Y) -> mark# f(X, f(g X, Y)), mark# f(X1, X2) -> mark# X1)
     (active# f(g X, Y) -> mark# f(X, f(g X, Y)), mark# f(X1, X2) -> f#(mark X1, X2))
     (active# f(g X, Y) -> mark# f(X, f(g X, Y)), mark# f(X1, X2) -> active# f(mark X1, X2))
     (active# f(g X, Y) -> mark# f(X, f(g X, Y)), mark# g X -> mark# X)
     (active# f(g X, Y) -> mark# f(X, f(g X, Y)), mark# g X -> g# mark X)
     (active# f(g X, Y) -> mark# f(X, f(g X, Y)), mark# g X -> active# g mark X)
     (mark# g X -> active# g mark X, active# f(g X, Y) -> mark# f(X, f(g X, Y)))
     (mark# g X -> active# g mark X, active# f(g X, Y) -> f#(X, f(g X, Y)))}
    STATUS:
     arrows: 0.734694
     SCCS (3):
      Scc:
       {  mark# f(X1, X2) -> mark# X1,
          mark# f(X1, X2) -> active# f(mark X1, X2),
                mark# g X -> mark# X,
                mark# g X -> active# g mark X,
        active# f(g X, Y) -> mark# f(X, f(g X, Y))}
      Scc:
       {  g# mark X -> g# X,
        g# active X -> g# X}
      Scc:
       {  f#(X1, mark X2) -> f#(X1, X2),
        f#(X1, active X2) -> f#(X1, X2),
          f#(mark X1, X2) -> f#(X1, X2),
        f#(active X1, X2) -> f#(X1, X2)}
      
      SCC (5):
       Strict:
        {  mark# f(X1, X2) -> mark# X1,
           mark# f(X1, X2) -> active# f(mark X1, X2),
                 mark# g X -> mark# X,
                 mark# g X -> active# g mark X,
         active# f(g X, Y) -> mark# f(X, f(g X, Y))}
       Weak:
       {  mark f(X1, X2) -> active f(mark X1, X2),
                mark g X -> active g mark X,
          f(X1, mark X2) -> f(X1, X2),
        f(X1, active X2) -> f(X1, X2),
          f(mark X1, X2) -> f(X1, X2),
        f(active X1, X2) -> f(X1, X2),
                g mark X -> g X,
              g active X -> g X,
        active f(g X, Y) -> mark f(X, f(g X, Y))}
       Open
      
      SCC (2):
       Strict:
        {  g# mark X -> g# X,
         g# active X -> g# X}
       Weak:
       {  mark f(X1, X2) -> active f(mark X1, X2),
                mark g X -> active g mark X,
          f(X1, mark X2) -> f(X1, X2),
        f(X1, active X2) -> f(X1, X2),
          f(mark X1, X2) -> f(X1, X2),
        f(active X1, X2) -> f(X1, X2),
                g mark X -> g X,
              g active X -> g X,
        active f(g X, Y) -> mark f(X, f(g X, Y))}
       Open
      
      
      SCC (4):
       Strict:
        {  f#(X1, mark X2) -> f#(X1, X2),
         f#(X1, active X2) -> f#(X1, X2),
           f#(mark X1, X2) -> f#(X1, X2),
         f#(active X1, X2) -> f#(X1, X2)}
       Weak:
       {  mark f(X1, X2) -> active f(mark X1, X2),
                mark g X -> active g mark X,
          f(X1, mark X2) -> f(X1, X2),
        f(X1, active X2) -> f(X1, X2),
          f(mark X1, X2) -> f(X1, X2),
        f(active X1, X2) -> f(X1, X2),
                g mark X -> g X,
              g active X -> g X,
        active f(g X, Y) -> mark f(X, f(g X, Y))}
       Open