MAYBE
Time: 0.005999
TRS:
 {    f(a x, b()) -> f(b(), a x),
            a a x -> f(b(), a f(a x, b())),
  a a f(b(), a x) -> f(a a a x, b())}
 DP:
  DP:
   {    f#(a x, b()) -> f#(b(), a x),
              a# a x -> f#(a x, b()),
              a# a x -> f#(b(), a f(a x, b())),
              a# a x -> a# f(a x, b()),
    a# a f(b(), a x) -> f#(a a a x, b()),
    a# a f(b(), a x) -> a# a x,
    a# a f(b(), a x) -> a# a a x}
  TRS:
  {    f(a x, b()) -> f(b(), a x),
             a a x -> f(b(), a f(a x, b())),
   a a f(b(), a x) -> f(a a a x, b())}
  UR:
   {    f(a x, b()) -> f(b(), a x),
              a a x -> f(b(), a f(a x, b())),
    a a f(b(), a x) -> f(a a a x, b())}
   EDG:
    {(a# a x -> f#(a x, b()), f#(a x, b()) -> f#(b(), a x))
     (f#(a x, b()) -> f#(b(), a x), f#(a x, b()) -> f#(b(), a x))
     (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> a# a a x)
     (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> a# a x)
     (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> f#(a a a x, b()))
     (a# a f(b(), a x) -> a# a x, a# a x -> a# f(a x, b()))
     (a# a f(b(), a x) -> a# a x, a# a x -> f#(b(), a f(a x, b())))
     (a# a f(b(), a x) -> a# a x, a# a x -> f#(a x, b()))
     (a# a x -> a# f(a x, b()), a# a x -> f#(a x, b()))
     (a# a x -> a# f(a x, b()), a# a x -> f#(b(), a f(a x, b())))
     (a# a x -> a# f(a x, b()), a# a x -> a# f(a x, b()))
     (a# a x -> a# f(a x, b()), a# a f(b(), a x) -> f#(a a a x, b()))
     (a# a x -> a# f(a x, b()), a# a f(b(), a x) -> a# a x)
     (a# a x -> a# f(a x, b()), a# a f(b(), a x) -> a# a a x)
     (a# a x -> f#(b(), a f(a x, b())), f#(a x, b()) -> f#(b(), a x))
     (a# a f(b(), a x) -> f#(a a a x, b()), f#(a x, b()) -> f#(b(), a x))
     (a# a f(b(), a x) -> a# a a x, a# a x -> f#(a x, b()))
     (a# a f(b(), a x) -> a# a a x, a# a x -> f#(b(), a f(a x, b())))
     (a# a f(b(), a x) -> a# a a x, a# a x -> a# f(a x, b()))
     (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> f#(a a a x, b()))
     (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> a# a x)
     (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> a# a a x)}
    EDG:
     {(a# a x -> f#(a x, b()), f#(a x, b()) -> f#(b(), a x))
      (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> a# a a x)
      (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> a# a x)
      (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> f#(a a a x, b()))
      (a# a f(b(), a x) -> a# a x, a# a x -> a# f(a x, b()))
      (a# a f(b(), a x) -> a# a x, a# a x -> f#(b(), a f(a x, b())))
      (a# a f(b(), a x) -> a# a x, a# a x -> f#(a x, b()))
      (a# a f(b(), a x) -> f#(a a a x, b()), f#(a x, b()) -> f#(b(), a x))
      (a# a f(b(), a x) -> a# a a x, a# a x -> f#(a x, b()))
      (a# a f(b(), a x) -> a# a a x, a# a x -> f#(b(), a f(a x, b())))
      (a# a f(b(), a x) -> a# a a x, a# a x -> a# f(a x, b()))
      (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> f#(a a a x, b()))
      (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> a# a x)
      (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> a# a a x)}
     EDG:
      {(a# a x -> f#(a x, b()), f#(a x, b()) -> f#(b(), a x))
       (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> a# a a x)
       (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> a# a x)
       (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> f#(a a a x, b()))
       (a# a f(b(), a x) -> a# a x, a# a x -> a# f(a x, b()))
       (a# a f(b(), a x) -> a# a x, a# a x -> f#(b(), a f(a x, b())))
       (a# a f(b(), a x) -> a# a x, a# a x -> f#(a x, b()))
       (a# a f(b(), a x) -> f#(a a a x, b()), f#(a x, b()) -> f#(b(), a x))
       (a# a f(b(), a x) -> a# a a x, a# a x -> f#(a x, b()))
       (a# a f(b(), a x) -> a# a a x, a# a x -> f#(b(), a f(a x, b())))
       (a# a f(b(), a x) -> a# a a x, a# a x -> a# f(a x, b()))
       (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> f#(a a a x, b()))
       (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> a# a x)
       (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> a# a a x)}
      EDG:
       {(a# a x -> f#(a x, b()), f#(a x, b()) -> f#(b(), a x))
        (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> a# a a x)
        (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> a# a x)
        (a# a f(b(), a x) -> a# a x, a# a f(b(), a x) -> f#(a a a x, b()))
        (a# a f(b(), a x) -> a# a x, a# a x -> a# f(a x, b()))
        (a# a f(b(), a x) -> a# a x, a# a x -> f#(b(), a f(a x, b())))
        (a# a f(b(), a x) -> a# a x, a# a x -> f#(a x, b()))
        (a# a f(b(), a x) -> f#(a a a x, b()), f#(a x, b()) -> f#(b(), a x))
        (a# a f(b(), a x) -> a# a a x, a# a x -> f#(a x, b()))
        (a# a f(b(), a x) -> a# a a x, a# a x -> f#(b(), a f(a x, b())))
        (a# a f(b(), a x) -> a# a a x, a# a x -> a# f(a x, b()))
        (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> f#(a a a x, b()))
        (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> a# a x)
        (a# a f(b(), a x) -> a# a a x, a# a f(b(), a x) -> a# a a x)}
       STATUS:
        arrows: 0.714286
        SCCS (1):
         Scc:
          {a# a f(b(), a x) -> a# a x,
           a# a f(b(), a x) -> a# a a x}
         
         SCC (2):
          Strict:
           {a# a f(b(), a x) -> a# a x,
            a# a f(b(), a x) -> a# a a x}
          Weak:
          {    f(a x, b()) -> f(b(), a x),
                     a a x -> f(b(), a f(a x, b())),
           a a f(b(), a x) -> f(a a a x, b())}
          Open