MAYBE
Time: 0.000644
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)}
  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