MAYBE
Time: 0.593098
TRS:
 {                h(x, x) -> h(a(), b()),
  h(h(f f x, y), h(z, v)) -> h(h(f z, f f f y), h(v, x)),
          g(g(x, a()), y) -> g(g(a(), y), g(a(), x)),
                f g(x, y) -> g(g(f f y, h(a(), a())), x)}
 DP:
  DP:
   {                h#(x, x) -> h#(a(), b()),
    h#(h(f f x, y), h(z, v)) -> h#(v, x),
    h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)),
    h#(h(f f x, y), h(z, v)) -> h#(f z, f f f y),
    h#(h(f f x, y), h(z, v)) -> f# y,
    h#(h(f f x, y), h(z, v)) -> f# z,
    h#(h(f f x, y), h(z, v)) -> f# f y,
    h#(h(f f x, y), h(z, v)) -> f# f f y,
            g#(g(x, a()), y) -> g#(a(), x),
            g#(g(x, a()), y) -> g#(a(), y),
            g#(g(x, a()), y) -> g#(g(a(), y), g(a(), x)),
                  f# g(x, y) -> h#(a(), a()),
                  f# g(x, y) -> g#(g(f f y, h(a(), a())), x),
                  f# g(x, y) -> g#(f f y, h(a(), a())),
                  f# g(x, y) -> f# y,
                  f# g(x, y) -> f# f y}
  TRS:
  {                h(x, x) -> h(a(), b()),
   h(h(f f x, y), h(z, v)) -> h(h(f z, f f f y), h(v, x)),
           g(g(x, a()), y) -> g(g(a(), y), g(a(), x)),
                 f g(x, y) -> g(g(f f y, h(a(), a())), x)}
  EDG:
   {(f# g(x, y) -> f# f y, f# g(x, y) -> f# f y)
    (f# g(x, y) -> f# f y, f# g(x, y) -> f# y)
    (f# g(x, y) -> f# f y, f# g(x, y) -> g#(f f y, h(a(), a())))
    (f# g(x, y) -> f# f y, f# g(x, y) -> g#(g(f f y, h(a(), a())), x))
    (f# g(x, y) -> f# f y, f# g(x, y) -> h#(a(), a()))
    (f# g(x, y) -> h#(a(), a()), h#(x, x) -> h#(a(), b()))
    (f# g(x, y) -> f# y, f# g(x, y) -> f# f y)
    (f# g(x, y) -> f# y, f# g(x, y) -> f# y)
    (f# g(x, y) -> f# y, f# g(x, y) -> g#(f f y, h(a(), a())))
    (f# g(x, y) -> f# y, f# g(x, y) -> g#(g(f f y, h(a(), a())), x))
    (f# g(x, y) -> f# y, f# g(x, y) -> h#(a(), a()))
    (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(h(f f x, y), h(z, v)) -> f# f f y)
    (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(h(f f x, y), h(z, v)) -> f# f y)
    (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(h(f f x, y), h(z, v)) -> f# z)
    (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(h(f f x, y), h(z, v)) -> f# y)
    (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(h(f f x, y), h(z, v)) -> h#(f z, f f f y))
    (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)))
    (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(h(f f x, y), h(z, v)) -> h#(v, x))
    (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(x, x) -> h#(a(), b()))
    (h#(h(f f x, y), h(z, v)) -> f# z, f# g(x, y) -> f# f y)
    (h#(h(f f x, y), h(z, v)) -> f# z, f# g(x, y) -> f# y)
    (h#(h(f f x, y), h(z, v)) -> f# z, f# g(x, y) -> g#(f f y, h(a(), a())))
    (h#(h(f f x, y), h(z, v)) -> f# z, f# g(x, y) -> g#(g(f f y, h(a(), a())), x))
    (h#(h(f f x, y), h(z, v)) -> f# z, f# g(x, y) -> h#(a(), a()))
    (f# g(x, y) -> g#(g(f f y, h(a(), a())), x), g#(g(x, a()), y) -> g#(g(a(), y), g(a(), x)))
    (f# g(x, y) -> g#(g(f f y, h(a(), a())), x), g#(g(x, a()), y) -> g#(a(), y))
    (f# g(x, y) -> g#(g(f f y, h(a(), a())), x), g#(g(x, a()), y) -> g#(a(), x))
    (g#(g(x, a()), y) -> g#(g(a(), y), g(a(), x)), g#(g(x, a()), y) -> g#(a(), x))
    (g#(g(x, a()), y) -> g#(g(a(), y), g(a(), x)), g#(g(x, a()), y) -> g#(a(), y))
    (g#(g(x, a()), y) -> g#(g(a(), y), g(a(), x)), g#(g(x, a()), y) -> g#(g(a(), y), g(a(), x)))
    (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(x, x) -> h#(a(), b()))
    (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(h(f f x, y), h(z, v)) -> h#(v, x))
    (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)))
    (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(h(f f x, y), h(z, v)) -> h#(f z, f f f y))
    (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(h(f f x, y), h(z, v)) -> f# y)
    (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(h(f f x, y), h(z, v)) -> f# z)
    (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(h(f f x, y), h(z, v)) -> f# f y)
    (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(h(f f x, y), h(z, v)) -> f# f f y)
    (h#(h(f f x, y), h(z, v)) -> f# f f y, f# g(x, y) -> h#(a(), a()))
    (h#(h(f f x, y), h(z, v)) -> f# f f y, f# g(x, y) -> g#(g(f f y, h(a(), a())), x))
    (h#(h(f f x, y), h(z, v)) -> f# f f y, f# g(x, y) -> g#(f f y, h(a(), a())))
    (h#(h(f f x, y), h(z, v)) -> f# f f y, f# g(x, y) -> f# y)
    (h#(h(f f x, y), h(z, v)) -> f# f f y, f# g(x, y) -> f# f y)
    (f# g(x, y) -> g#(f f y, h(a(), a())), g#(g(x, a()), y) -> g#(a(), x))
    (f# g(x, y) -> g#(f f y, h(a(), a())), g#(g(x, a()), y) -> g#(a(), y))
    (f# g(x, y) -> g#(f f y, h(a(), a())), g#(g(x, a()), y) -> g#(g(a(), y), g(a(), x)))
    (h#(h(f f x, y), h(z, v)) -> f# y, f# g(x, y) -> h#(a(), a()))
    (h#(h(f f x, y), h(z, v)) -> f# y, f# g(x, y) -> g#(g(f f y, h(a(), a())), x))
    (h#(h(f f x, y), h(z, v)) -> f# y, f# g(x, y) -> g#(f f y, h(a(), a())))
    (h#(h(f f x, y), h(z, v)) -> f# y, f# g(x, y) -> f# y)
    (h#(h(f f x, y), h(z, v)) -> f# y, f# g(x, y) -> f# f y)
    (h#(h(f f x, y), h(z, v)) -> f# f y, f# g(x, y) -> h#(a(), a()))
    (h#(h(f f x, y), h(z, v)) -> f# f y, f# g(x, y) -> g#(g(f f y, h(a(), a())), x))
    (h#(h(f f x, y), h(z, v)) -> f# f y, f# g(x, y) -> g#(f f y, h(a(), a())))
    (h#(h(f f x, y), h(z, v)) -> f# f y, f# g(x, y) -> f# y)
    (h#(h(f f x, y), h(z, v)) -> f# f y, f# g(x, y) -> f# f y)
    (h#(h(f f x, y), h(z, v)) -> h#(f z, f f f y), h#(x, x) -> h#(a(), b()))}
   EDG:
    {(f# g(x, y) -> f# f y, f# g(x, y) -> f# f y)
     (f# g(x, y) -> f# f y, f# g(x, y) -> f# y)
     (f# g(x, y) -> f# f y, f# g(x, y) -> g#(f f y, h(a(), a())))
     (f# g(x, y) -> f# f y, f# g(x, y) -> g#(g(f f y, h(a(), a())), x))
     (f# g(x, y) -> f# f y, f# g(x, y) -> h#(a(), a()))
     (f# g(x, y) -> h#(a(), a()), h#(x, x) -> h#(a(), b()))
     (f# g(x, y) -> f# y, f# g(x, y) -> f# f y)
     (f# g(x, y) -> f# y, f# g(x, y) -> f# y)
     (f# g(x, y) -> f# y, f# g(x, y) -> g#(f f y, h(a(), a())))
     (f# g(x, y) -> f# y, f# g(x, y) -> g#(g(f f y, h(a(), a())), x))
     (f# g(x, y) -> f# y, f# g(x, y) -> h#(a(), a()))
     (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(h(f f x, y), h(z, v)) -> f# f f y)
     (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(h(f f x, y), h(z, v)) -> f# f y)
     (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(h(f f x, y), h(z, v)) -> f# z)
     (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(h(f f x, y), h(z, v)) -> f# y)
     (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(h(f f x, y), h(z, v)) -> h#(f z, f f f y))
     (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)))
     (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(h(f f x, y), h(z, v)) -> h#(v, x))
     (h#(h(f f x, y), h(z, v)) -> h#(v, x), h#(x, x) -> h#(a(), b()))
     (h#(h(f f x, y), h(z, v)) -> f# z, f# g(x, y) -> f# f y)
     (h#(h(f f x, y), h(z, v)) -> f# z, f# g(x, y) -> f# y)
     (h#(h(f f x, y), h(z, v)) -> f# z, f# g(x, y) -> g#(f f y, h(a(), a())))
     (h#(h(f f x, y), h(z, v)) -> f# z, f# g(x, y) -> g#(g(f f y, h(a(), a())), x))
     (h#(h(f f x, y), h(z, v)) -> f# z, f# g(x, y) -> h#(a(), a()))
     (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(x, x) -> h#(a(), b()))
     (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(h(f f x, y), h(z, v)) -> h#(v, x))
     (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)))
     (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(h(f f x, y), h(z, v)) -> h#(f z, f f f y))
     (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(h(f f x, y), h(z, v)) -> f# y)
     (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(h(f f x, y), h(z, v)) -> f# z)
     (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(h(f f x, y), h(z, v)) -> f# f y)
     (h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x)), h#(h(f f x, y), h(z, v)) -> f# f f y)
     (h#(h(f f x, y), h(z, v)) -> f# f f y, f# g(x, y) -> h#(a(), a()))
     (h#(h(f f x, y), h(z, v)) -> f# f f y, f# g(x, y) -> g#(g(f f y, h(a(), a())), x))
     (h#(h(f f x, y), h(z, v)) -> f# f f y, f# g(x, y) -> g#(f f y, h(a(), a())))
     (h#(h(f f x, y), h(z, v)) -> f# f f y, f# g(x, y) -> f# y)
     (h#(h(f f x, y), h(z, v)) -> f# f f y, f# g(x, y) -> f# f y)
     (h#(h(f f x, y), h(z, v)) -> f# y, f# g(x, y) -> h#(a(), a()))
     (h#(h(f f x, y), h(z, v)) -> f# y, f# g(x, y) -> g#(g(f f y, h(a(), a())), x))
     (h#(h(f f x, y), h(z, v)) -> f# y, f# g(x, y) -> g#(f f y, h(a(), a())))
     (h#(h(f f x, y), h(z, v)) -> f# y, f# g(x, y) -> f# y)
     (h#(h(f f x, y), h(z, v)) -> f# y, f# g(x, y) -> f# f y)
     (h#(h(f f x, y), h(z, v)) -> f# f y, f# g(x, y) -> h#(a(), a()))
     (h#(h(f f x, y), h(z, v)) -> f# f y, f# g(x, y) -> g#(g(f f y, h(a(), a())), x))
     (h#(h(f f x, y), h(z, v)) -> f# f y, f# g(x, y) -> g#(f f y, h(a(), a())))
     (h#(h(f f x, y), h(z, v)) -> f# f y, f# g(x, y) -> f# y)
     (h#(h(f f x, y), h(z, v)) -> f# f y, f# g(x, y) -> f# f y)}
    STATUS:
     arrows: 0.816406
     SCCS (2):
      Scc:
       {h#(h(f f x, y), h(z, v)) -> h#(v, x),
        h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x))}
      Scc:
       {f# g(x, y) -> f# y,
        f# g(x, y) -> f# f y}
      
      
      
      SCC (2):
       Strict:
        {h#(h(f f x, y), h(z, v)) -> h#(v, x),
         h#(h(f f x, y), h(z, v)) -> h#(h(f z, f f f y), h(v, x))}
       Weak:
       {                h(x, x) -> h(a(), b()),
        h(h(f f x, y), h(z, v)) -> h(h(f z, f f f y), h(v, x)),
                g(g(x, a()), y) -> g(g(a(), y), g(a(), x)),
                      f g(x, y) -> g(g(f f y, h(a(), a())), x)}
       Open
      
      
      
      
      SCC (2):
       Strict:
        {f# g(x, y) -> f# y,
         f# g(x, y) -> f# f y}
       Weak:
       {                h(x, x) -> h(a(), b()),
        h(h(f f x, y), h(z, v)) -> h(h(f z, f f f y), h(v, x)),
                g(g(x, a()), y) -> g(g(a(), y), g(a(), x)),
                      f g(x, y) -> g(g(f f y, h(a(), a())), x)}
       Open