MAYBE
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:
  Strict:
   {                              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)))}
  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)))))}
  EDG:
   {(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)))
    (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#(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#(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(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#(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#(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#(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#(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(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(x, g(b(), g(b(), y))))), g#(x, x) -> g#(a(), b()))
    (h#(i(x, y)) -> i#(i(c(), h(h(y))), x), i#(x, x) -> i#(a(), b()))
    (f#(g(s(x), y)) -> g#(x, s(y)), g#(x, x) -> g#(a(), b()))
    (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)))
    (h#(g(x, s(y))) -> g#(s(x), y), g#(x, x) -> g#(a(), b()))
    (f#(g(s(x), y)) -> f#(g(x, s(y))), f#(s(x)) -> f#(h(s(x))))
    (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#(g(s(x), y)) -> f#(g(x, s(y))))
    (f#(g(s(x), y)) -> f#(g(x, s(y))), f#(g(s(x), y)) -> g#(x, s(y)))
    (f#(s(x)) -> f#(h(s(x))), f#(g(s(x), y)) -> g#(x, s(y)))
    (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#(s(x)) -> h#(s(x)))
    (f#(s(x)) -> f#(h(s(x))), f#(s(x)) -> f#(h(s(x))))
    (h#(i(x, y)) -> i#(c(), h(h(y))), i#(x, x) -> i#(a(), b()))
    (g#(a(), g(x, g(b(), g(a(), g(x, y))))) -> g#(b(), 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)))
    (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)))
    (h#(g(x, s(y))) -> h#(g(s(x), y)), h#(i(x, y)) -> i#(i(c(), h(h(y))), x))
    (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)) -> h#(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#(g(x, s(y))) -> 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))) -> h#(g(s(x), y)), h#(s(f(x))) -> h#(f(x)))
    (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()))
    (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(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#(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(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#(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(), g(b(), y)))
    (g#(a(), g(x, g(b(), g(a(), g(x, y))))) -> g#(b(), y), g#(x, x) -> g#(a(), b()))}
   SCCS:
    Scc:
     {f#(g(s(x), y)) -> f#(g(x, s(y))),
            f#(s(x)) -> f#(h(s(x)))}
    Scc:
     {   h#(i(x, y)) -> h#(y),
         h#(i(x, y)) -> h#(h(y)),
      h#(g(x, s(y))) -> h#(g(s(x), y)),
         h#(s(f(x))) -> h#(f(x))}
    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:
     Strict:
      {f#(g(s(x), y)) -> f#(g(x, s(y))),
             f#(s(x)) -> f#(h(s(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)))))}
     POLY:
      Argument Filtering:
       pi(c) = [], pi(s) = [], pi(f#) = 0, pi(f) = [], pi(h) = [], pi(g) = [], pi(b) = [], pi(a) = [], pi(i) = []
      Usable Rules:
       {}
      Interpretation:
       [g] = 0,
       [s] = 1,
       [h] = 0
      Strict:
       {f#(g(s(x), y)) -> f#(g(x, s(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)))))}
      EDG:
       {(f#(g(s(x), y)) -> f#(g(x, s(y))), f#(g(s(x), y)) -> f#(g(x, s(y))))}
       SCCS:
        Scc:
         {f#(g(s(x), y)) -> f#(g(x, s(y)))}
        SCC:
         Strict:
          {f#(g(s(x), y)) -> f#(g(x, s(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)))))}
         POLY:
          Argument Filtering:
           pi(c) = [], pi(s) = [0], pi(f#) = 0, pi(f) = [], pi(h) = [], pi(g) = 0, pi(b) = [], pi(a) = [], pi(i) = []
          Usable Rules:
           {}
          Interpretation:
           [s](x0) = x0 + 1
          Strict:
           {}
          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)))))}
          Qed
    SCC:
     Strict:
      {   h#(i(x, y)) -> h#(y),
          h#(i(x, y)) -> h#(h(y)),
       h#(g(x, s(y))) -> h#(g(s(x), y)),
          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)))))}
     Fail
    SCC:
     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)))))}
     Fail