MAYBE
Time: 0.013333
TRS:
 {                  g(x, x, x) -> g(c(), d(), e()),
                    g(x, y, x) -> g(c(), d(), e()),
    f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)),
           f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))),
  f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()),
                           s y -> b(),
                     s f(x, y) -> f(y, f(s s x, a())),
             h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))),
               h(h(x, a()), y) -> h(h(a(), y), h(a(), x))}
 DP:
  DP:
   {                  g#(x, x, x) -> g#(c(), d(), e()),
                      g#(x, y, x) -> g#(c(), d(), e()),
      f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y),
      f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)),
      f#(x, g(x, a(), f(s x, y))) -> h#(x, b()),
             f#(x, f(y, f(x, y))) -> f#(x, f(y, b())),
             f#(x, f(y, f(x, y))) -> f#(y, b()),
             f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))),
    f#(h(a(), y), g(x, b(), a())) -> f#(x, s y),
    f#(h(a(), y), g(x, b(), a())) -> s# y,
    f#(h(a(), y), g(x, b(), a())) -> s# b(),
    f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()),
                       s# f(x, y) -> f#(y, f(s s x, a())),
                       s# f(x, y) -> f#(s s x, a()),
                       s# f(x, y) -> s# x,
                       s# f(x, y) -> s# s x,
               h#(f(x, s y), b()) -> g#(y, a(), f(s x, a())),
               h#(f(x, s y), b()) -> f#(s x, a()),
               h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))),
               h#(f(x, s y), b()) -> s# x,
                 h#(h(x, a()), y) -> h#(a(), x),
                 h#(h(x, a()), y) -> h#(a(), y),
                 h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))}
  TRS:
  {                  g(x, x, x) -> g(c(), d(), e()),
                     g(x, y, x) -> g(c(), d(), e()),
     f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)),
            f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))),
   f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()),
                            s y -> b(),
                      s f(x, y) -> f(y, f(s s x, a())),
              h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))),
                h(h(x, a()), y) -> h(h(a(), y), h(a(), x))}
  EDG:
   {(s# f(x, y) -> s# s x, s# f(x, y) -> s# s x)
    (s# f(x, y) -> s# s x, s# f(x, y) -> s# x)
    (s# f(x, y) -> s# s x, s# f(x, y) -> f#(s s x, a()))
    (s# f(x, y) -> s# s x, s# f(x, y) -> f#(y, f(s s x, a())))
    (h#(f(x, s y), b()) -> g#(y, a(), f(s x, a())), g#(x, y, x) -> g#(c(), d(), e()))
    (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()))
    (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(h(a(), y), g(x, b(), a())) -> s# b())
    (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(h(a(), y), g(x, b(), a())) -> s# y)
    (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(h(a(), y), g(x, b(), a())) -> f#(x, s y))
    (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))))
    (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, f(y, f(x, y))) -> f#(y, b()))
    (f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())))
    (s# f(x, y) -> s# x, s# f(x, y) -> s# s x)
    (s# f(x, y) -> s# x, s# f(x, y) -> s# x)
    (s# f(x, y) -> s# x, s# f(x, y) -> f#(s s x, a()))
    (s# f(x, y) -> s# x, s# f(x, y) -> f#(y, f(s s x, a())))
    (f#(h(a(), y), g(x, b(), a())) -> s# y, s# f(x, y) -> s# s x)
    (f#(h(a(), y), g(x, b(), a())) -> s# y, s# f(x, y) -> s# x)
    (f#(h(a(), y), g(x, b(), a())) -> s# y, s# f(x, y) -> f#(s s x, a()))
    (f#(h(a(), y), g(x, b(), a())) -> s# y, s# f(x, y) -> f#(y, f(s s x, a())))
    (f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> g#(y, a(), f(s x, a())))
    (f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(s x, a()))
    (f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))))
    (f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()), h#(f(x, s y), b()) -> s# x)
    (f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())))
    (f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(x, f(y, f(x, y))) -> f#(y, b()))
    (f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))))
    (f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y), g#(x, y, x) -> g#(c(), d(), e()))
    (h#(f(x, s y), b()) -> s# x, s# f(x, y) -> f#(y, f(s s x, a())))
    (h#(f(x, s y), b()) -> s# x, s# f(x, y) -> f#(s s x, a()))
    (h#(f(x, s y), b()) -> s# x, s# f(x, y) -> s# x)
    (h#(f(x, s y), b()) -> s# x, s# f(x, y) -> s# s x)
    (h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)), h#(h(x, a()), y) -> h#(a(), x))
    (h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)), h#(h(x, a()), y) -> h#(a(), y))
    (h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)))
    (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(x, g(x, a(), f(s x, y))) -> g#(a(), b(), y))
    (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)))
    (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(x, g(x, a(), f(s x, y))) -> h#(x, b()))
    (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())))
    (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(x, f(y, f(x, y))) -> f#(y, b()))
    (h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))))
    (f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(x, f(y, f(x, y))) -> f#(x, f(y, b())))
    (f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(x, f(y, f(x, y))) -> f#(y, b()))
    (f#(h(a(), y), g(x, b(), a())) -> f#(x, s y), f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b()))))
    (f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), h#(f(x, s y), b()) -> g#(y, a(), f(s x, a())))
    (f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), h#(f(x, s y), b()) -> f#(s x, a()))
    (f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a()))))
    (f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), h#(f(x, s y), b()) -> s# x)
    (f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), h#(h(x, a()), y) -> h#(a(), x))
    (f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), h#(h(x, a()), y) -> h#(a(), y))
    (f#(x, g(x, a(), f(s x, y))) -> h#(x, b()), h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x)))}
   STATUS:
    arrows: 0.903592
    SCCS (4):
     Scc:
      {  f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)),
         f#(x, g(x, a(), f(s x, y))) -> h#(x, b()),
       f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()),
                  h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a())))}
     Scc:
      {h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))}
     Scc:
      {f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b())))}
     Scc:
      {s# f(x, y) -> s# x,
       s# f(x, y) -> s# s x}
     
     SCC (4):
      Strict:
       {  f#(x, g(x, a(), f(s x, y))) -> f#(h(x, b()), g(a(), b(), y)),
          f#(x, g(x, a(), f(s x, y))) -> h#(x, b()),
        f#(h(a(), y), g(x, b(), a())) -> h#(f(x, s y), s b()),
                   h#(f(x, s y), b()) -> f#(a(), g(y, a(), f(s x, a())))}
      Weak:
      {                  g(x, x, x) -> g(c(), d(), e()),
                         g(x, y, x) -> g(c(), d(), e()),
         f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)),
                f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))),
       f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()),
                                s y -> b(),
                          s f(x, y) -> f(y, f(s s x, a())),
                  h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))),
                    h(h(x, a()), y) -> h(h(a(), y), h(a(), x))}
      Open
     SCC (1):
      Strict:
       {h#(h(x, a()), y) -> h#(h(a(), y), h(a(), x))}
      Weak:
      {                  g(x, x, x) -> g(c(), d(), e()),
                         g(x, y, x) -> g(c(), d(), e()),
         f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)),
                f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))),
       f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()),
                                s y -> b(),
                          s f(x, y) -> f(y, f(s s x, a())),
                  h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))),
                    h(h(x, a()), y) -> h(h(a(), y), h(a(), x))}
      Open
     
     
     
     
     
     SCC (1):
      Strict:
       {f#(x, f(y, f(x, y))) -> f#(a(), f(x, f(y, b())))}
      Weak:
      {                  g(x, x, x) -> g(c(), d(), e()),
                         g(x, y, x) -> g(c(), d(), e()),
         f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)),
                f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))),
       f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()),
                                s y -> b(),
                          s f(x, y) -> f(y, f(s s x, a())),
                  h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))),
                    h(h(x, a()), y) -> h(h(a(), y), h(a(), x))}
      Open
     
     
     
     
     SCC (2):
      Strict:
       {s# f(x, y) -> s# x,
        s# f(x, y) -> s# s x}
      Weak:
      {                  g(x, x, x) -> g(c(), d(), e()),
                         g(x, y, x) -> g(c(), d(), e()),
         f(x, g(x, a(), f(s x, y))) -> f(h(x, b()), g(a(), b(), y)),
                f(x, f(y, f(x, y))) -> f(a(), f(x, f(y, b()))),
       f(h(a(), y), g(x, b(), a())) -> h(f(x, s y), s b()),
                                s y -> b(),
                          s f(x, y) -> f(y, f(s s x, a())),
                  h(f(x, s y), b()) -> f(a(), g(y, a(), f(s x, a()))),
                    h(h(x, a()), y) -> h(h(a(), y), h(a(), x))}
      Open