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