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