MAYBE
Time: 0.037584
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()}
  EDG:
   {(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))
    (active# b() -> mark# a(), mark# a() -> active# a())
    (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())
    (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()))}
   STATUS:
    arrows: 0.895833
    SCCS (1):
     Scc:
      {mark# f(X1, X2) -> mark# X1,
       mark# f(X1, X2) -> active# f(mark X1, X2),
       active# f(X, X) -> mark# f(a(), b())}
     
     
     
     SCC (3):
      Strict:
       {mark# f(X1, X2) -> mark# X1,
        mark# f(X1, X2) -> active# f(mark X1, X2),
        active# f(X, X) -> mark# f(a(), b())}
      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()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [f](x0, x1) = x0 + 1,
        
        [mark](x0) = x0,
        
        [active](x0) = x0,
        
        [a] = 0,
        
        [b] = 0,
        
        [mark#](x0) = x0,
        
        [active#](x0) = x0
       Strict:
        active# f(X, X) -> mark# f(a(), b())
        1 + 1X >= 1
        mark# f(X1, X2) -> active# f(mark X1, X2)
        1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
        mark# f(X1, X2) -> mark# X1
        1 + 1X1 + 0X2 >= 0 + 1X1
       Weak:
        active b() -> mark a()
        0 >= 0
        active f(X, X) -> mark f(a(), b())
        1 + 1X >= 1
        f(active X1, X2) -> f(X1, X2)
        1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
        f(mark X1, X2) -> f(X1, X2)
        1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
        f(X1, active X2) -> f(X1, X2)
        1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
        f(X1, mark X2) -> f(X1, X2)
        1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
        mark b() -> active b()
        0 >= 0
        mark a() -> active a()
        0 >= 0
        mark f(X1, X2) -> active f(mark X1, X2)
        1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2
      SCCS (1):
       Scc:
        {mark# f(X1, X2) -> active# f(mark X1, X2),
         active# f(X, X) -> mark# f(a(), b())}
       
       SCC (2):
        Strict:
         {mark# f(X1, X2) -> active# f(mark X1, X2),
          active# f(X, X) -> mark# f(a(), b())}
        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()}
        Fail