MAYBE
Time: 0.002496
TRS:
 {  mark f(X1, X2) -> active f(mark X1, X2),
          mark a() -> active a(),
          mark b() -> active b(),
    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),
    active f(X, X) -> mark f(a(), b()),
        active b() -> mark a()}
 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# a() -> active# a(),
            mark# b() -> active# b(),
      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),
      active# f(X, X) -> mark# f(a(), b()),
      active# f(X, X) -> f#(a(), b()),
          active# b() -> mark# a()}
  TRS:
  {  mark f(X1, X2) -> active f(mark X1, X2),
           mark a() -> active a(),
           mark b() -> active b(),
     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),
     active f(X, X) -> mark f(a(), b()),
         active b() -> mark a()}
  UR:
   {  mark f(X1, X2) -> active f(mark X1, X2),
            mark a() -> active a(),
            mark b() -> active b(),
      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),
      active f(X, X) -> mark f(a(), b()),
          active b() -> mark a()}
   EDG:
    {(active# f(X, X) -> f#(a(), b()), f#(active X1, X2) -> f#(X1, X2))
     (active# f(X, X) -> f#(a(), b()), f#(mark X1, X2) -> f#(X1, X2))
     (active# f(X, X) -> f#(a(), b()), f#(X1, active X2) -> f#(X1, X2))
     (active# f(X, X) -> f#(a(), b()), f#(X1, mark X2) -> f#(X1, X2))
     (f#(X1, mark X2) -> f#(X1, X2), f#(active X1, 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#(X1, active X2) -> f#(X1, X2))
     (f#(X1, mark X2) -> f#(X1, X2), f#(X1, mark X2) -> f#(X1, X2))
     (f#(mark X1, X2) -> f#(X1, X2), f#(active X1, 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#(X1, active X2) -> f#(X1, X2))
     (f#(mark X1, X2) -> f#(X1, X2), f#(X1, mark X2) -> f#(X1, X2))
     (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))
     (mark# a() -> active# a(), active# b() -> mark# a())
     (mark# a() -> active# a(), active# f(X, X) -> f#(a(), b()))
     (mark# a() -> active# a(), active# f(X, X) -> mark# f(a(), b()))
     (active# b() -> mark# a(), mark# b() -> active# b())
     (active# b() -> mark# a(), mark# a() -> active# a())
     (active# b() -> mark# a(), mark# f(X1, X2) -> active# f(mark X1, X2))
     (active# b() -> mark# a(), mark# f(X1, X2) -> f#(mark X1, X2))
     (active# b() -> mark# a(), mark# f(X1, X2) -> mark# X1)
     (mark# b() -> active# b(), active# f(X, X) -> mark# f(a(), b()))
     (mark# b() -> active# b(), active# f(X, X) -> f#(a(), b()))
     (mark# b() -> active# b(), active# b() -> mark# a())
     (active# f(X, X) -> mark# f(a(), b()), mark# f(X1, X2) -> mark# X1)
     (active# f(X, X) -> mark# f(a(), b()), mark# f(X1, X2) -> f#(mark X1, X2))
     (active# f(X, X) -> mark# f(a(), b()), mark# f(X1, X2) -> active# f(mark X1, X2))
     (active# f(X, X) -> mark# f(a(), b()), mark# a() -> active# a())
     (active# f(X, X) -> mark# f(a(), b()), mark# b() -> active# b())
     (f#(active X1, X2) -> f#(X1, X2), f#(X1, mark 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#(mark X1, X2) -> f#(X1, X2))
     (f#(active X1, X2) -> f#(X1, X2), f#(active X1, X2) -> f#(X1, X2))
     (f#(X1, active X2) -> f#(X1, X2), f#(X1, mark 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#(mark X1, X2) -> f#(X1, X2))
     (f#(X1, active X2) -> f#(X1, X2), f#(active X1, X2) -> f#(X1, X2))
     (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1)
     (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> f#(mark X1, X2))
     (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> active# f(mark X1, X2))
     (mark# f(X1, X2) -> mark# X1, mark# a() -> active# a())
     (mark# f(X1, X2) -> mark# X1, mark# b() -> active# b())
     (mark# f(X1, X2) -> active# f(mark X1, X2), active# f(X, X) -> mark# f(a(), b()))
     (mark# f(X1, X2) -> active# f(mark X1, X2), active# f(X, X) -> f#(a(), b()))
     (mark# f(X1, X2) -> active# f(mark X1, X2), active# b() -> mark# a())}
    STATUS:
     arrows: 0.666667
     SCCS (2):
      Scc:
       {mark# f(X1, X2) -> mark# X1,
        mark# f(X1, X2) -> active# f(mark X1, X2),
              mark# a() -> active# a(),
              mark# b() -> active# b(),
        active# f(X, X) -> mark# f(a(), b()),
            active# b() -> mark# a()}
      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 (6):
       Strict:
        {mark# f(X1, X2) -> mark# X1,
         mark# f(X1, X2) -> active# f(mark X1, X2),
               mark# a() -> active# a(),
               mark# b() -> active# b(),
         active# f(X, X) -> mark# f(a(), b()),
             active# b() -> mark# a()}
       Weak:
       {  mark f(X1, X2) -> active f(mark X1, X2),
                mark a() -> active a(),
                mark b() -> active b(),
          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),
          active f(X, X) -> mark f(a(), b()),
              active b() -> mark a()}
       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 a() -> active a(),
                mark b() -> active b(),
          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),
          active f(X, X) -> mark f(a(), b()),
              active b() -> mark a()}
       Open