MAYBE
Time: 0.051404
TRS:
 {    a__f(X, X) -> a__f(a(), b()),
    a__f(X1, X2) -> f(X1, X2),
          a__b() -> a(),
          a__b() -> b(),
        mark a() -> a(),
        mark b() -> a__b(),
  mark f(X1, X2) -> a__f(mark X1, X2)}
 DP:
  DP:
   {    a__f#(X, X) -> a__f#(a(), b()),
          mark# b() -> a__b#(),
    mark# f(X1, X2) -> a__f#(mark X1, X2),
    mark# f(X1, X2) -> mark# X1}
  TRS:
  {    a__f(X, X) -> a__f(a(), b()),
     a__f(X1, X2) -> f(X1, X2),
           a__b() -> a(),
           a__b() -> b(),
         mark a() -> a(),
         mark b() -> a__b(),
   mark f(X1, X2) -> a__f(mark X1, X2)}
  UR:
   {    a__f(X, X) -> a__f(a(), b()),
      a__f(X1, X2) -> f(X1, X2),
            a__b() -> a(),
            a__b() -> b(),
          mark a() -> a(),
          mark b() -> a__b(),
    mark f(X1, X2) -> a__f(mark X1, X2)}
   EDG:
    {(mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> mark# X1)
     (mark# f(X1, X2) -> mark# X1, mark# f(X1, X2) -> a__f#(mark X1, X2))
     (mark# f(X1, X2) -> mark# X1, mark# b() -> a__b#())
     (mark# f(X1, X2) -> a__f#(mark X1, X2), a__f#(X, X) -> a__f#(a(), b()))}
    STATUS:
     arrows: 0.750000
     SCCS (1):
      Scc:
       {mark# f(X1, X2) -> mark# X1}
      
      SCC (1):
       Strict:
        {mark# f(X1, X2) -> mark# X1}
       Weak:
       {    a__f(X, X) -> a__f(a(), b()),
          a__f(X1, X2) -> f(X1, X2),
                a__b() -> a(),
                a__b() -> b(),
              mark a() -> a(),
              mark b() -> a__b(),
        mark f(X1, X2) -> a__f(mark X1, X2)}
       Open