MAYBE
TRS:
 {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
         mark(h(X)) -> active(h(mark(X))),
    mark(f(X1, X2)) -> active(f(mark(X1), X2)),
          mark(b()) -> active(b()),
          mark(a()) -> active(a()),
    g(X1, mark(X2)) -> g(X1, X2),
  g(X1, active(X2)) -> g(X1, X2),
    g(mark(X1), X2) -> g(X1, X2),
  g(active(X1), X2) -> g(X1, X2),
  active(g(a(), X)) -> mark(f(b(), X)),
       active(h(X)) -> mark(g(X, X)),
    active(f(X, X)) -> mark(h(a())),
        active(a()) -> mark(b()),
         h(mark(X)) -> h(X),
       h(active(X)) -> h(X),
    f(X1, mark(X2)) -> f(X1, X2),
  f(X1, active(X2)) -> f(X1, X2),
    f(mark(X1), X2) -> f(X1, X2),
  f(active(X1), X2) -> f(X1, X2)}
 DP:
  Strict:
   {  mark#(g(X1, X2)) -> mark#(X1),
      mark#(g(X1, X2)) -> g#(mark(X1), X2),
      mark#(g(X1, X2)) -> active#(g(mark(X1), X2)),
           mark#(h(X)) -> mark#(X),
           mark#(h(X)) -> active#(h(mark(X))),
           mark#(h(X)) -> h#(mark(X)),
      mark#(f(X1, X2)) -> mark#(X1),
      mark#(f(X1, X2)) -> active#(f(mark(X1), X2)),
      mark#(f(X1, X2)) -> f#(mark(X1), X2),
            mark#(b()) -> active#(b()),
            mark#(a()) -> active#(a()),
      g#(X1, mark(X2)) -> g#(X1, X2),
    g#(X1, active(X2)) -> g#(X1, X2),
      g#(mark(X1), X2) -> g#(X1, X2),
    g#(active(X1), X2) -> g#(X1, X2),
    active#(g(a(), X)) -> mark#(f(b(), X)),
    active#(g(a(), X)) -> f#(b(), X),
         active#(h(X)) -> mark#(g(X, X)),
         active#(h(X)) -> g#(X, X),
      active#(f(X, X)) -> mark#(h(a())),
      active#(f(X, X)) -> h#(a()),
          active#(a()) -> mark#(b()),
           h#(mark(X)) -> h#(X),
         h#(active(X)) -> h#(X),
      f#(X1, mark(X2)) -> f#(X1, X2),
    f#(X1, active(X2)) -> f#(X1, X2),
      f#(mark(X1), X2) -> f#(X1, X2),
    f#(active(X1), X2) -> f#(X1, X2)}
  Weak:
  {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
          mark(h(X)) -> active(h(mark(X))),
     mark(f(X1, X2)) -> active(f(mark(X1), X2)),
           mark(b()) -> active(b()),
           mark(a()) -> active(a()),
     g(X1, mark(X2)) -> g(X1, X2),
   g(X1, active(X2)) -> g(X1, X2),
     g(mark(X1), X2) -> g(X1, X2),
   g(active(X1), X2) -> g(X1, X2),
   active(g(a(), X)) -> mark(f(b(), X)),
        active(h(X)) -> mark(g(X, X)),
     active(f(X, X)) -> mark(h(a())),
         active(a()) -> mark(b()),
          h(mark(X)) -> h(X),
        h(active(X)) -> h(X),
     f(X1, mark(X2)) -> f(X1, X2),
   f(X1, active(X2)) -> f(X1, X2),
     f(mark(X1), X2) -> f(X1, X2),
   f(active(X1), X2) -> f(X1, X2)}
  EDG:
   {(active#(h(X)) -> g#(X, X), g#(active(X1), X2) -> g#(X1, X2))
    (active#(h(X)) -> g#(X, X), g#(mark(X1), X2) -> g#(X1, X2))
    (active#(h(X)) -> g#(X, X), g#(X1, active(X2)) -> g#(X1, X2))
    (active#(h(X)) -> g#(X, X), g#(X1, mark(X2)) -> g#(X1, X2))
    (g#(X1, mark(X2)) -> g#(X1, X2), g#(active(X1), X2) -> g#(X1, X2))
    (g#(X1, mark(X2)) -> g#(X1, X2), g#(mark(X1), X2) -> g#(X1, X2))
    (g#(X1, mark(X2)) -> g#(X1, X2), g#(X1, active(X2)) -> g#(X1, X2))
    (g#(X1, mark(X2)) -> g#(X1, X2), g#(X1, mark(X2)) -> g#(X1, X2))
    (g#(mark(X1), X2) -> g#(X1, X2), g#(active(X1), X2) -> g#(X1, X2))
    (g#(mark(X1), X2) -> g#(X1, X2), g#(mark(X1), X2) -> g#(X1, X2))
    (g#(mark(X1), X2) -> g#(X1, X2), g#(X1, active(X2)) -> g#(X1, X2))
    (g#(mark(X1), X2) -> g#(X1, X2), g#(X1, mark(X2)) -> g#(X1, X2))
    (f#(X1, mark(X2)) -> f#(X1, X2), f#(active(X1), X2) -> f#(X1, X2))
    (f#(X1, mark(X2)) -> f#(X1, X2), f#(mark(X1), X2) -> f#(X1, X2))
    (f#(X1, mark(X2)) -> f#(X1, X2), f#(X1, active(X2)) -> f#(X1, X2))
    (f#(X1, mark(X2)) -> f#(X1, X2), f#(X1, mark(X2)) -> f#(X1, X2))
    (f#(mark(X1), X2) -> f#(X1, X2), f#(active(X1), X2) -> f#(X1, X2))
    (f#(mark(X1), X2) -> f#(X1, X2), f#(mark(X1), X2) -> f#(X1, X2))
    (f#(mark(X1), X2) -> f#(X1, X2), f#(X1, active(X2)) -> f#(X1, X2))
    (f#(mark(X1), X2) -> f#(X1, X2), f#(X1, mark(X2)) -> f#(X1, X2))
    (active#(g(a(), X)) -> f#(b(), X), f#(X1, active(X2)) -> f#(X1, X2))
    (active#(g(a(), X)) -> f#(b(), X), f#(X1, mark(X2)) -> f#(X1, X2))
    (mark#(f(X1, X2)) -> active#(f(mark(X1), X2)), active#(f(X, X)) -> h#(a()))
    (mark#(f(X1, X2)) -> active#(f(mark(X1), X2)), active#(f(X, X)) -> mark#(h(a())))
    (mark#(f(X1, X2)) -> active#(f(mark(X1), X2)), active#(h(X)) -> g#(X, X))
    (mark#(f(X1, X2)) -> active#(f(mark(X1), X2)), active#(h(X)) -> mark#(g(X, X)))
    (mark#(f(X1, X2)) -> active#(f(mark(X1), X2)), active#(g(a(), X)) -> f#(b(), X))
    (mark#(f(X1, X2)) -> active#(f(mark(X1), X2)), active#(g(a(), X)) -> mark#(f(b(), X)))
    (active#(h(X)) -> mark#(g(X, X)), mark#(f(X1, X2)) -> f#(mark(X1), X2))
    (active#(h(X)) -> mark#(g(X, X)), mark#(f(X1, X2)) -> active#(f(mark(X1), X2)))
    (active#(h(X)) -> mark#(g(X, X)), mark#(f(X1, X2)) -> mark#(X1))
    (active#(h(X)) -> mark#(g(X, X)), mark#(h(X)) -> h#(mark(X)))
    (active#(h(X)) -> mark#(g(X, X)), mark#(h(X)) -> active#(h(mark(X))))
    (active#(h(X)) -> mark#(g(X, X)), mark#(h(X)) -> mark#(X))
    (active#(h(X)) -> mark#(g(X, X)), mark#(g(X1, X2)) -> active#(g(mark(X1), X2)))
    (active#(h(X)) -> mark#(g(X, X)), mark#(g(X1, X2)) -> g#(mark(X1), X2))
    (active#(h(X)) -> mark#(g(X, X)), mark#(g(X1, X2)) -> mark#(X1))
    (mark#(f(X1, X2)) -> mark#(X1), mark#(a()) -> active#(a()))
    (mark#(f(X1, X2)) -> mark#(X1), mark#(b()) -> active#(b()))
    (mark#(f(X1, X2)) -> mark#(X1), mark#(f(X1, X2)) -> f#(mark(X1), X2))
    (mark#(f(X1, X2)) -> mark#(X1), mark#(f(X1, X2)) -> active#(f(mark(X1), X2)))
    (mark#(f(X1, X2)) -> mark#(X1), mark#(f(X1, X2)) -> mark#(X1))
    (mark#(f(X1, X2)) -> mark#(X1), mark#(h(X)) -> h#(mark(X)))
    (mark#(f(X1, X2)) -> mark#(X1), mark#(h(X)) -> active#(h(mark(X))))
    (mark#(f(X1, X2)) -> mark#(X1), mark#(h(X)) -> mark#(X))
    (mark#(f(X1, X2)) -> mark#(X1), mark#(g(X1, X2)) -> active#(g(mark(X1), X2)))
    (mark#(f(X1, X2)) -> mark#(X1), mark#(g(X1, X2)) -> g#(mark(X1), X2))
    (mark#(f(X1, X2)) -> mark#(X1), mark#(g(X1, X2)) -> mark#(X1))
    (h#(mark(X)) -> h#(X), h#(active(X)) -> h#(X))
    (h#(mark(X)) -> h#(X), h#(mark(X)) -> h#(X))
    (mark#(h(X)) -> h#(mark(X)), h#(active(X)) -> h#(X))
    (mark#(h(X)) -> h#(mark(X)), h#(mark(X)) -> h#(X))
    (mark#(f(X1, X2)) -> f#(mark(X1), X2), f#(active(X1), X2) -> f#(X1, X2))
    (mark#(f(X1, X2)) -> f#(mark(X1), X2), f#(mark(X1), X2) -> f#(X1, X2))
    (mark#(f(X1, X2)) -> f#(mark(X1), X2), f#(X1, active(X2)) -> f#(X1, X2))
    (mark#(f(X1, X2)) -> f#(mark(X1), X2), f#(X1, mark(X2)) -> f#(X1, X2))
    (mark#(a()) -> active#(a()), active#(a()) -> mark#(b()))
    (active#(a()) -> mark#(b()), mark#(b()) -> active#(b()))
    (mark#(g(X1, X2)) -> g#(mark(X1), X2), g#(X1, mark(X2)) -> g#(X1, X2))
    (mark#(g(X1, X2)) -> g#(mark(X1), X2), g#(X1, active(X2)) -> g#(X1, X2))
    (mark#(g(X1, X2)) -> g#(mark(X1), X2), g#(mark(X1), X2) -> g#(X1, X2))
    (mark#(g(X1, X2)) -> g#(mark(X1), X2), g#(active(X1), X2) -> g#(X1, X2))
    (h#(active(X)) -> h#(X), h#(mark(X)) -> h#(X))
    (h#(active(X)) -> h#(X), h#(active(X)) -> h#(X))
    (mark#(h(X)) -> mark#(X), mark#(g(X1, X2)) -> mark#(X1))
    (mark#(h(X)) -> mark#(X), mark#(g(X1, X2)) -> g#(mark(X1), X2))
    (mark#(h(X)) -> mark#(X), mark#(g(X1, X2)) -> active#(g(mark(X1), X2)))
    (mark#(h(X)) -> mark#(X), mark#(h(X)) -> mark#(X))
    (mark#(h(X)) -> mark#(X), mark#(h(X)) -> active#(h(mark(X))))
    (mark#(h(X)) -> mark#(X), mark#(h(X)) -> h#(mark(X)))
    (mark#(h(X)) -> mark#(X), mark#(f(X1, X2)) -> mark#(X1))
    (mark#(h(X)) -> mark#(X), mark#(f(X1, X2)) -> active#(f(mark(X1), X2)))
    (mark#(h(X)) -> mark#(X), mark#(f(X1, X2)) -> f#(mark(X1), X2))
    (mark#(h(X)) -> mark#(X), mark#(b()) -> active#(b()))
    (mark#(h(X)) -> mark#(X), mark#(a()) -> active#(a()))
    (mark#(g(X1, X2)) -> mark#(X1), mark#(g(X1, X2)) -> mark#(X1))
    (mark#(g(X1, X2)) -> mark#(X1), mark#(g(X1, X2)) -> g#(mark(X1), X2))
    (mark#(g(X1, X2)) -> mark#(X1), mark#(g(X1, X2)) -> active#(g(mark(X1), X2)))
    (mark#(g(X1, X2)) -> mark#(X1), mark#(h(X)) -> mark#(X))
    (mark#(g(X1, X2)) -> mark#(X1), mark#(h(X)) -> active#(h(mark(X))))
    (mark#(g(X1, X2)) -> mark#(X1), mark#(h(X)) -> h#(mark(X)))
    (mark#(g(X1, X2)) -> mark#(X1), mark#(f(X1, X2)) -> mark#(X1))
    (mark#(g(X1, X2)) -> mark#(X1), mark#(f(X1, X2)) -> active#(f(mark(X1), X2)))
    (mark#(g(X1, X2)) -> mark#(X1), mark#(f(X1, X2)) -> f#(mark(X1), X2))
    (mark#(g(X1, X2)) -> mark#(X1), mark#(b()) -> active#(b()))
    (mark#(g(X1, X2)) -> mark#(X1), mark#(a()) -> active#(a()))
    (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(g(X1, X2)) -> mark#(X1))
    (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(g(X1, X2)) -> g#(mark(X1), X2))
    (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(g(X1, X2)) -> active#(g(mark(X1), X2)))
    (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(h(X)) -> mark#(X))
    (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(h(X)) -> active#(h(mark(X))))
    (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(h(X)) -> h#(mark(X)))
    (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(f(X1, X2)) -> mark#(X1))
    (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(f(X1, X2)) -> active#(f(mark(X1), X2)))
    (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(f(X1, X2)) -> f#(mark(X1), X2))
    (mark#(g(X1, X2)) -> active#(g(mark(X1), X2)), active#(g(a(), X)) -> mark#(f(b(), X)))
    (mark#(g(X1, X2)) -> active#(g(mark(X1), X2)), active#(g(a(), X)) -> f#(b(), X))
    (mark#(g(X1, X2)) -> active#(g(mark(X1), X2)), active#(h(X)) -> mark#(g(X, X)))
    (mark#(g(X1, X2)) -> active#(g(mark(X1), X2)), active#(h(X)) -> g#(X, X))
    (mark#(g(X1, X2)) -> active#(g(mark(X1), X2)), active#(f(X, X)) -> mark#(h(a())))
    (mark#(g(X1, X2)) -> active#(g(mark(X1), X2)), active#(f(X, X)) -> h#(a()))
    (f#(active(X1), X2) -> f#(X1, X2), f#(X1, mark(X2)) -> f#(X1, X2))
    (f#(active(X1), X2) -> f#(X1, X2), f#(X1, active(X2)) -> f#(X1, X2))
    (f#(active(X1), X2) -> f#(X1, X2), f#(mark(X1), X2) -> f#(X1, X2))
    (f#(active(X1), X2) -> f#(X1, X2), f#(active(X1), X2) -> f#(X1, X2))
    (f#(X1, active(X2)) -> f#(X1, X2), f#(X1, mark(X2)) -> f#(X1, X2))
    (f#(X1, active(X2)) -> f#(X1, X2), f#(X1, active(X2)) -> f#(X1, X2))
    (f#(X1, active(X2)) -> f#(X1, X2), f#(mark(X1), X2) -> f#(X1, X2))
    (f#(X1, active(X2)) -> f#(X1, X2), f#(active(X1), X2) -> f#(X1, X2))
    (g#(active(X1), X2) -> g#(X1, X2), g#(X1, mark(X2)) -> g#(X1, X2))
    (g#(active(X1), X2) -> g#(X1, X2), g#(X1, active(X2)) -> g#(X1, X2))
    (g#(active(X1), X2) -> g#(X1, X2), g#(mark(X1), X2) -> g#(X1, X2))
    (g#(active(X1), X2) -> g#(X1, X2), g#(active(X1), X2) -> g#(X1, X2))
    (g#(X1, active(X2)) -> g#(X1, X2), g#(X1, mark(X2)) -> g#(X1, X2))
    (g#(X1, active(X2)) -> g#(X1, X2), g#(X1, active(X2)) -> g#(X1, X2))
    (g#(X1, active(X2)) -> g#(X1, X2), g#(mark(X1), X2) -> g#(X1, X2))
    (g#(X1, active(X2)) -> g#(X1, X2), g#(active(X1), X2) -> g#(X1, X2))
    (active#(f(X, X)) -> mark#(h(a())), mark#(h(X)) -> mark#(X))
    (active#(f(X, X)) -> mark#(h(a())), mark#(h(X)) -> active#(h(mark(X))))
    (active#(f(X, X)) -> mark#(h(a())), mark#(h(X)) -> h#(mark(X)))
    (mark#(h(X)) -> active#(h(mark(X))), active#(g(a(), X)) -> mark#(f(b(), X)))
    (mark#(h(X)) -> active#(h(mark(X))), active#(g(a(), X)) -> f#(b(), X))
    (mark#(h(X)) -> active#(h(mark(X))), active#(h(X)) -> mark#(g(X, X)))
    (mark#(h(X)) -> active#(h(mark(X))), active#(h(X)) -> g#(X, X))
    (mark#(h(X)) -> active#(h(mark(X))), active#(f(X, X)) -> mark#(h(a())))
    (mark#(h(X)) -> active#(h(mark(X))), active#(f(X, X)) -> h#(a()))}
   SCCS:
    Scc:
     {  f#(X1, mark(X2)) -> f#(X1, X2),
      f#(X1, active(X2)) -> f#(X1, X2),
        f#(mark(X1), X2) -> f#(X1, X2),
      f#(active(X1), X2) -> f#(X1, X2)}
    Scc:
     {  h#(mark(X)) -> h#(X),
      h#(active(X)) -> h#(X)}
    Scc:
     {  g#(X1, mark(X2)) -> g#(X1, X2),
      g#(X1, active(X2)) -> g#(X1, X2),
        g#(mark(X1), X2) -> g#(X1, X2),
      g#(active(X1), X2) -> g#(X1, X2)}
    Scc:
     {  mark#(g(X1, X2)) -> mark#(X1),
        mark#(g(X1, X2)) -> active#(g(mark(X1), X2)),
             mark#(h(X)) -> mark#(X),
             mark#(h(X)) -> active#(h(mark(X))),
        mark#(f(X1, X2)) -> mark#(X1),
        mark#(f(X1, X2)) -> active#(f(mark(X1), X2)),
      active#(g(a(), X)) -> mark#(f(b(), X)),
           active#(h(X)) -> mark#(g(X, X)),
        active#(f(X, X)) -> mark#(h(a()))}
    SCC:
     Strict:
      {  f#(X1, mark(X2)) -> f#(X1, X2),
       f#(X1, active(X2)) -> f#(X1, X2),
         f#(mark(X1), X2) -> f#(X1, X2),
       f#(active(X1), X2) -> f#(X1, X2)}
     Weak:
     {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
             mark(h(X)) -> active(h(mark(X))),
        mark(f(X1, X2)) -> active(f(mark(X1), X2)),
              mark(b()) -> active(b()),
              mark(a()) -> active(a()),
        g(X1, mark(X2)) -> g(X1, X2),
      g(X1, active(X2)) -> g(X1, X2),
        g(mark(X1), X2) -> g(X1, X2),
      g(active(X1), X2) -> g(X1, X2),
      active(g(a(), X)) -> mark(f(b(), X)),
           active(h(X)) -> mark(g(X, X)),
        active(f(X, X)) -> mark(h(a())),
            active(a()) -> mark(b()),
             h(mark(X)) -> h(X),
           h(active(X)) -> h(X),
        f(X1, mark(X2)) -> f(X1, X2),
      f(X1, active(X2)) -> f(X1, X2),
        f(mark(X1), X2) -> f(X1, X2),
      f(active(X1), X2) -> f(X1, X2)}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {  f#(X1, mark(X2)) -> f#(X1, X2),
        f#(X1, active(X2)) -> f#(X1, X2),
          f#(mark(X1), X2) -> f#(X1, X2)}
      EDG:
       {(f#(X1, active(X2)) -> f#(X1, X2), f#(mark(X1), X2) -> f#(X1, X2))
        (f#(X1, active(X2)) -> f#(X1, X2), f#(X1, active(X2)) -> f#(X1, X2))
        (f#(X1, active(X2)) -> f#(X1, X2), f#(X1, mark(X2)) -> f#(X1, X2))
        (f#(mark(X1), X2) -> f#(X1, X2), f#(X1, mark(X2)) -> f#(X1, X2))
        (f#(mark(X1), X2) -> f#(X1, X2), f#(X1, active(X2)) -> f#(X1, X2))
        (f#(mark(X1), X2) -> f#(X1, X2), f#(mark(X1), X2) -> f#(X1, X2))
        (f#(X1, mark(X2)) -> f#(X1, X2), f#(X1, mark(X2)) -> f#(X1, X2))
        (f#(X1, mark(X2)) -> f#(X1, X2), f#(X1, active(X2)) -> f#(X1, X2))
        (f#(X1, mark(X2)) -> f#(X1, X2), f#(mark(X1), X2) -> f#(X1, X2))}
       SCCS:
        Scc:
         {  f#(X1, mark(X2)) -> f#(X1, X2),
          f#(X1, active(X2)) -> f#(X1, X2),
            f#(mark(X1), X2) -> f#(X1, X2)}
        SCC:
         Strict:
          {  f#(X1, mark(X2)) -> f#(X1, X2),
           f#(X1, active(X2)) -> f#(X1, X2),
             f#(mark(X1), X2) -> f#(X1, X2)}
         Weak:
         {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
                 mark(h(X)) -> active(h(mark(X))),
            mark(f(X1, X2)) -> active(f(mark(X1), X2)),
                  mark(b()) -> active(b()),
                  mark(a()) -> active(a()),
            g(X1, mark(X2)) -> g(X1, X2),
          g(X1, active(X2)) -> g(X1, X2),
            g(mark(X1), X2) -> g(X1, X2),
          g(active(X1), X2) -> g(X1, X2),
          active(g(a(), X)) -> mark(f(b(), X)),
               active(h(X)) -> mark(g(X, X)),
            active(f(X, X)) -> mark(h(a())),
                active(a()) -> mark(b()),
                 h(mark(X)) -> h(X),
               h(active(X)) -> h(X),
            f(X1, mark(X2)) -> f(X1, X2),
          f(X1, active(X2)) -> f(X1, X2),
            f(mark(X1), X2) -> f(X1, X2),
          f(active(X1), X2) -> f(X1, X2)}
         SPSC:
          Simple Projection:
           pi(f#) = 1
          Strict:
           {f#(X1, mark(X2)) -> f#(X1, X2),
            f#(mark(X1), X2) -> f#(X1, X2)}
          EDG:
           {(f#(mark(X1), X2) -> f#(X1, X2), f#(mark(X1), X2) -> f#(X1, X2))
            (f#(mark(X1), X2) -> f#(X1, X2), f#(X1, mark(X2)) -> f#(X1, X2))
            (f#(X1, mark(X2)) -> f#(X1, X2), f#(X1, mark(X2)) -> f#(X1, X2))
            (f#(X1, mark(X2)) -> f#(X1, X2), f#(mark(X1), X2) -> f#(X1, X2))}
           SCCS:
            Scc:
             {f#(X1, mark(X2)) -> f#(X1, X2),
              f#(mark(X1), X2) -> f#(X1, X2)}
            SCC:
             Strict:
              {f#(X1, mark(X2)) -> f#(X1, X2),
               f#(mark(X1), X2) -> f#(X1, X2)}
             Weak:
             {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
                     mark(h(X)) -> active(h(mark(X))),
                mark(f(X1, X2)) -> active(f(mark(X1), X2)),
                      mark(b()) -> active(b()),
                      mark(a()) -> active(a()),
                g(X1, mark(X2)) -> g(X1, X2),
              g(X1, active(X2)) -> g(X1, X2),
                g(mark(X1), X2) -> g(X1, X2),
              g(active(X1), X2) -> g(X1, X2),
              active(g(a(), X)) -> mark(f(b(), X)),
                   active(h(X)) -> mark(g(X, X)),
                active(f(X, X)) -> mark(h(a())),
                    active(a()) -> mark(b()),
                     h(mark(X)) -> h(X),
                   h(active(X)) -> h(X),
                f(X1, mark(X2)) -> f(X1, X2),
              f(X1, active(X2)) -> f(X1, X2),
                f(mark(X1), X2) -> f(X1, X2),
              f(active(X1), X2) -> f(X1, X2)}
             SPSC:
              Simple Projection:
               pi(f#) = 0
              Strict:
               {f#(X1, mark(X2)) -> f#(X1, X2)}
              EDG:
               {(f#(X1, mark(X2)) -> f#(X1, X2), f#(X1, mark(X2)) -> f#(X1, X2))}
               SCCS:
                Scc:
                 {f#(X1, mark(X2)) -> f#(X1, X2)}
                SCC:
                 Strict:
                  {f#(X1, mark(X2)) -> f#(X1, X2)}
                 Weak:
                 {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
                         mark(h(X)) -> active(h(mark(X))),
                    mark(f(X1, X2)) -> active(f(mark(X1), X2)),
                          mark(b()) -> active(b()),
                          mark(a()) -> active(a()),
                    g(X1, mark(X2)) -> g(X1, X2),
                  g(X1, active(X2)) -> g(X1, X2),
                    g(mark(X1), X2) -> g(X1, X2),
                  g(active(X1), X2) -> g(X1, X2),
                  active(g(a(), X)) -> mark(f(b(), X)),
                       active(h(X)) -> mark(g(X, X)),
                    active(f(X, X)) -> mark(h(a())),
                        active(a()) -> mark(b()),
                         h(mark(X)) -> h(X),
                       h(active(X)) -> h(X),
                    f(X1, mark(X2)) -> f(X1, X2),
                  f(X1, active(X2)) -> f(X1, X2),
                    f(mark(X1), X2) -> f(X1, X2),
                  f(active(X1), X2) -> f(X1, X2)}
                 SPSC:
                  Simple Projection:
                   pi(f#) = 1
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {  h#(mark(X)) -> h#(X),
       h#(active(X)) -> h#(X)}
     Weak:
     {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
             mark(h(X)) -> active(h(mark(X))),
        mark(f(X1, X2)) -> active(f(mark(X1), X2)),
              mark(b()) -> active(b()),
              mark(a()) -> active(a()),
        g(X1, mark(X2)) -> g(X1, X2),
      g(X1, active(X2)) -> g(X1, X2),
        g(mark(X1), X2) -> g(X1, X2),
      g(active(X1), X2) -> g(X1, X2),
      active(g(a(), X)) -> mark(f(b(), X)),
           active(h(X)) -> mark(g(X, X)),
        active(f(X, X)) -> mark(h(a())),
            active(a()) -> mark(b()),
             h(mark(X)) -> h(X),
           h(active(X)) -> h(X),
        f(X1, mark(X2)) -> f(X1, X2),
      f(X1, active(X2)) -> f(X1, X2),
        f(mark(X1), X2) -> f(X1, X2),
      f(active(X1), X2) -> f(X1, X2)}
     SPSC:
      Simple Projection:
       pi(h#) = 0
      Strict:
       {h#(active(X)) -> h#(X)}
      EDG:
       {(h#(active(X)) -> h#(X), h#(active(X)) -> h#(X))}
       SCCS:
        Scc:
         {h#(active(X)) -> h#(X)}
        SCC:
         Strict:
          {h#(active(X)) -> h#(X)}
         Weak:
         {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
                 mark(h(X)) -> active(h(mark(X))),
            mark(f(X1, X2)) -> active(f(mark(X1), X2)),
                  mark(b()) -> active(b()),
                  mark(a()) -> active(a()),
            g(X1, mark(X2)) -> g(X1, X2),
          g(X1, active(X2)) -> g(X1, X2),
            g(mark(X1), X2) -> g(X1, X2),
          g(active(X1), X2) -> g(X1, X2),
          active(g(a(), X)) -> mark(f(b(), X)),
               active(h(X)) -> mark(g(X, X)),
            active(f(X, X)) -> mark(h(a())),
                active(a()) -> mark(b()),
                 h(mark(X)) -> h(X),
               h(active(X)) -> h(X),
            f(X1, mark(X2)) -> f(X1, X2),
          f(X1, active(X2)) -> f(X1, X2),
            f(mark(X1), X2) -> f(X1, X2),
          f(active(X1), X2) -> f(X1, X2)}
         SPSC:
          Simple Projection:
           pi(h#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {  g#(X1, mark(X2)) -> g#(X1, X2),
       g#(X1, active(X2)) -> g#(X1, X2),
         g#(mark(X1), X2) -> g#(X1, X2),
       g#(active(X1), X2) -> g#(X1, X2)}
     Weak:
     {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
             mark(h(X)) -> active(h(mark(X))),
        mark(f(X1, X2)) -> active(f(mark(X1), X2)),
              mark(b()) -> active(b()),
              mark(a()) -> active(a()),
        g(X1, mark(X2)) -> g(X1, X2),
      g(X1, active(X2)) -> g(X1, X2),
        g(mark(X1), X2) -> g(X1, X2),
      g(active(X1), X2) -> g(X1, X2),
      active(g(a(), X)) -> mark(f(b(), X)),
           active(h(X)) -> mark(g(X, X)),
        active(f(X, X)) -> mark(h(a())),
            active(a()) -> mark(b()),
             h(mark(X)) -> h(X),
           h(active(X)) -> h(X),
        f(X1, mark(X2)) -> f(X1, X2),
      f(X1, active(X2)) -> f(X1, X2),
        f(mark(X1), X2) -> f(X1, X2),
      f(active(X1), X2) -> f(X1, X2)}
     SPSC:
      Simple Projection:
       pi(g#) = 0
      Strict:
       {  g#(X1, mark(X2)) -> g#(X1, X2),
        g#(X1, active(X2)) -> g#(X1, X2),
          g#(mark(X1), X2) -> g#(X1, X2)}
      EDG:
       {(g#(X1, active(X2)) -> g#(X1, X2), g#(mark(X1), X2) -> g#(X1, X2))
        (g#(X1, active(X2)) -> g#(X1, X2), g#(X1, active(X2)) -> g#(X1, X2))
        (g#(X1, active(X2)) -> g#(X1, X2), g#(X1, mark(X2)) -> g#(X1, X2))
        (g#(mark(X1), X2) -> g#(X1, X2), g#(X1, mark(X2)) -> g#(X1, X2))
        (g#(mark(X1), X2) -> g#(X1, X2), g#(X1, active(X2)) -> g#(X1, X2))
        (g#(mark(X1), X2) -> g#(X1, X2), g#(mark(X1), X2) -> g#(X1, X2))
        (g#(X1, mark(X2)) -> g#(X1, X2), g#(X1, mark(X2)) -> g#(X1, X2))
        (g#(X1, mark(X2)) -> g#(X1, X2), g#(X1, active(X2)) -> g#(X1, X2))
        (g#(X1, mark(X2)) -> g#(X1, X2), g#(mark(X1), X2) -> g#(X1, X2))}
       SCCS:
        Scc:
         {  g#(X1, mark(X2)) -> g#(X1, X2),
          g#(X1, active(X2)) -> g#(X1, X2),
            g#(mark(X1), X2) -> g#(X1, X2)}
        SCC:
         Strict:
          {  g#(X1, mark(X2)) -> g#(X1, X2),
           g#(X1, active(X2)) -> g#(X1, X2),
             g#(mark(X1), X2) -> g#(X1, X2)}
         Weak:
         {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
                 mark(h(X)) -> active(h(mark(X))),
            mark(f(X1, X2)) -> active(f(mark(X1), X2)),
                  mark(b()) -> active(b()),
                  mark(a()) -> active(a()),
            g(X1, mark(X2)) -> g(X1, X2),
          g(X1, active(X2)) -> g(X1, X2),
            g(mark(X1), X2) -> g(X1, X2),
          g(active(X1), X2) -> g(X1, X2),
          active(g(a(), X)) -> mark(f(b(), X)),
               active(h(X)) -> mark(g(X, X)),
            active(f(X, X)) -> mark(h(a())),
                active(a()) -> mark(b()),
                 h(mark(X)) -> h(X),
               h(active(X)) -> h(X),
            f(X1, mark(X2)) -> f(X1, X2),
          f(X1, active(X2)) -> f(X1, X2),
            f(mark(X1), X2) -> f(X1, X2),
          f(active(X1), X2) -> f(X1, X2)}
         SPSC:
          Simple Projection:
           pi(g#) = 0
          Strict:
           {  g#(X1, mark(X2)) -> g#(X1, X2),
            g#(X1, active(X2)) -> g#(X1, X2)}
          EDG:
           {(g#(X1, active(X2)) -> g#(X1, X2), g#(X1, active(X2)) -> g#(X1, X2))
            (g#(X1, active(X2)) -> g#(X1, X2), g#(X1, mark(X2)) -> g#(X1, X2))
            (g#(X1, mark(X2)) -> g#(X1, X2), g#(X1, mark(X2)) -> g#(X1, X2))
            (g#(X1, mark(X2)) -> g#(X1, X2), g#(X1, active(X2)) -> g#(X1, X2))}
           SCCS:
            Scc:
             {  g#(X1, mark(X2)) -> g#(X1, X2),
              g#(X1, active(X2)) -> g#(X1, X2)}
            SCC:
             Strict:
              {  g#(X1, mark(X2)) -> g#(X1, X2),
               g#(X1, active(X2)) -> g#(X1, X2)}
             Weak:
             {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
                     mark(h(X)) -> active(h(mark(X))),
                mark(f(X1, X2)) -> active(f(mark(X1), X2)),
                      mark(b()) -> active(b()),
                      mark(a()) -> active(a()),
                g(X1, mark(X2)) -> g(X1, X2),
              g(X1, active(X2)) -> g(X1, X2),
                g(mark(X1), X2) -> g(X1, X2),
              g(active(X1), X2) -> g(X1, X2),
              active(g(a(), X)) -> mark(f(b(), X)),
                   active(h(X)) -> mark(g(X, X)),
                active(f(X, X)) -> mark(h(a())),
                    active(a()) -> mark(b()),
                     h(mark(X)) -> h(X),
                   h(active(X)) -> h(X),
                f(X1, mark(X2)) -> f(X1, X2),
              f(X1, active(X2)) -> f(X1, X2),
                f(mark(X1), X2) -> f(X1, X2),
              f(active(X1), X2) -> f(X1, X2)}
             SPSC:
              Simple Projection:
               pi(g#) = 1
              Strict:
               {g#(X1, active(X2)) -> g#(X1, X2)}
              EDG:
               {(g#(X1, active(X2)) -> g#(X1, X2), g#(X1, active(X2)) -> g#(X1, X2))}
               SCCS:
                Scc:
                 {g#(X1, active(X2)) -> g#(X1, X2)}
                SCC:
                 Strict:
                  {g#(X1, active(X2)) -> g#(X1, X2)}
                 Weak:
                 {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
                         mark(h(X)) -> active(h(mark(X))),
                    mark(f(X1, X2)) -> active(f(mark(X1), X2)),
                          mark(b()) -> active(b()),
                          mark(a()) -> active(a()),
                    g(X1, mark(X2)) -> g(X1, X2),
                  g(X1, active(X2)) -> g(X1, X2),
                    g(mark(X1), X2) -> g(X1, X2),
                  g(active(X1), X2) -> g(X1, X2),
                  active(g(a(), X)) -> mark(f(b(), X)),
                       active(h(X)) -> mark(g(X, X)),
                    active(f(X, X)) -> mark(h(a())),
                        active(a()) -> mark(b()),
                         h(mark(X)) -> h(X),
                       h(active(X)) -> h(X),
                    f(X1, mark(X2)) -> f(X1, X2),
                  f(X1, active(X2)) -> f(X1, X2),
                    f(mark(X1), X2) -> f(X1, X2),
                  f(active(X1), X2) -> f(X1, X2)}
                 SPSC:
                  Simple Projection:
                   pi(g#) = 1
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {  mark#(g(X1, X2)) -> mark#(X1),
         mark#(g(X1, X2)) -> active#(g(mark(X1), X2)),
              mark#(h(X)) -> mark#(X),
              mark#(h(X)) -> active#(h(mark(X))),
         mark#(f(X1, X2)) -> mark#(X1),
         mark#(f(X1, X2)) -> active#(f(mark(X1), X2)),
       active#(g(a(), X)) -> mark#(f(b(), X)),
            active#(h(X)) -> mark#(g(X, X)),
         active#(f(X, X)) -> mark#(h(a()))}
     Weak:
     {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
             mark(h(X)) -> active(h(mark(X))),
        mark(f(X1, X2)) -> active(f(mark(X1), X2)),
              mark(b()) -> active(b()),
              mark(a()) -> active(a()),
        g(X1, mark(X2)) -> g(X1, X2),
      g(X1, active(X2)) -> g(X1, X2),
        g(mark(X1), X2) -> g(X1, X2),
      g(active(X1), X2) -> g(X1, X2),
      active(g(a(), X)) -> mark(f(b(), X)),
           active(h(X)) -> mark(g(X, X)),
        active(f(X, X)) -> mark(h(a())),
            active(a()) -> mark(b()),
             h(mark(X)) -> h(X),
           h(active(X)) -> h(X),
        f(X1, mark(X2)) -> f(X1, X2),
      f(X1, active(X2)) -> f(X1, X2),
        f(mark(X1), X2) -> f(X1, X2),
      f(active(X1), X2) -> f(X1, X2)}
     POLY:
      Argument Filtering:
       pi(a) = [], pi(b) = [], pi(f) = [0], pi(h) = 0, pi(active#) = [0], pi(active) = 0, pi(g) = 0, pi(mark#) = [0], pi(mark) = 0
      Usable Rules:
       {}
      Interpretation:
       [active#](x0) = x0 + 1,
       [mark#](x0) = x0 + 1,
       [f](x0) = x0 + 1,
       [a] = 1,
       [b] = 0
      Strict:
       {  mark#(g(X1, X2)) -> mark#(X1),
          mark#(g(X1, X2)) -> active#(g(mark(X1), X2)),
               mark#(h(X)) -> mark#(X),
               mark#(h(X)) -> active#(h(mark(X))),
          mark#(f(X1, X2)) -> active#(f(mark(X1), X2)),
        active#(g(a(), X)) -> mark#(f(b(), X)),
             active#(h(X)) -> mark#(g(X, X)),
          active#(f(X, X)) -> mark#(h(a()))}
      Weak:
       {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
               mark(h(X)) -> active(h(mark(X))),
          mark(f(X1, X2)) -> active(f(mark(X1), X2)),
                mark(b()) -> active(b()),
                mark(a()) -> active(a()),
          g(X1, mark(X2)) -> g(X1, X2),
        g(X1, active(X2)) -> g(X1, X2),
          g(mark(X1), X2) -> g(X1, X2),
        g(active(X1), X2) -> g(X1, X2),
        active(g(a(), X)) -> mark(f(b(), X)),
             active(h(X)) -> mark(g(X, X)),
          active(f(X, X)) -> mark(h(a())),
              active(a()) -> mark(b()),
               h(mark(X)) -> h(X),
             h(active(X)) -> h(X),
          f(X1, mark(X2)) -> f(X1, X2),
        f(X1, active(X2)) -> f(X1, X2),
          f(mark(X1), X2) -> f(X1, X2),
        f(active(X1), X2) -> f(X1, X2)}
      EDG:
       {(active#(f(X, X)) -> mark#(h(a())), mark#(h(X)) -> active#(h(mark(X))))
        (active#(f(X, X)) -> mark#(h(a())), mark#(h(X)) -> mark#(X))
        (mark#(g(X1, X2)) -> active#(g(mark(X1), X2)), active#(f(X, X)) -> mark#(h(a())))
        (mark#(g(X1, X2)) -> active#(g(mark(X1), X2)), active#(h(X)) -> mark#(g(X, X)))
        (mark#(g(X1, X2)) -> active#(g(mark(X1), X2)), active#(g(a(), X)) -> mark#(f(b(), X)))
        (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(f(X1, X2)) -> active#(f(mark(X1), X2)))
        (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(h(X)) -> active#(h(mark(X))))
        (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(h(X)) -> mark#(X))
        (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(g(X1, X2)) -> active#(g(mark(X1), X2)))
        (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(g(X1, X2)) -> mark#(X1))
        (mark#(h(X)) -> mark#(X), mark#(f(X1, X2)) -> active#(f(mark(X1), X2)))
        (mark#(h(X)) -> mark#(X), mark#(h(X)) -> active#(h(mark(X))))
        (mark#(h(X)) -> mark#(X), mark#(h(X)) -> mark#(X))
        (mark#(h(X)) -> mark#(X), mark#(g(X1, X2)) -> active#(g(mark(X1), X2)))
        (mark#(h(X)) -> mark#(X), mark#(g(X1, X2)) -> mark#(X1))
        (active#(h(X)) -> mark#(g(X, X)), mark#(g(X1, X2)) -> mark#(X1))
        (active#(h(X)) -> mark#(g(X, X)), mark#(g(X1, X2)) -> active#(g(mark(X1), X2)))
        (active#(h(X)) -> mark#(g(X, X)), mark#(h(X)) -> mark#(X))
        (active#(h(X)) -> mark#(g(X, X)), mark#(h(X)) -> active#(h(mark(X))))
        (active#(h(X)) -> mark#(g(X, X)), mark#(f(X1, X2)) -> active#(f(mark(X1), X2)))
        (mark#(f(X1, X2)) -> active#(f(mark(X1), X2)), active#(g(a(), X)) -> mark#(f(b(), X)))
        (mark#(f(X1, X2)) -> active#(f(mark(X1), X2)), active#(h(X)) -> mark#(g(X, X)))
        (mark#(f(X1, X2)) -> active#(f(mark(X1), X2)), active#(f(X, X)) -> mark#(h(a())))
        (mark#(g(X1, X2)) -> mark#(X1), mark#(g(X1, X2)) -> mark#(X1))
        (mark#(g(X1, X2)) -> mark#(X1), mark#(g(X1, X2)) -> active#(g(mark(X1), X2)))
        (mark#(g(X1, X2)) -> mark#(X1), mark#(h(X)) -> mark#(X))
        (mark#(g(X1, X2)) -> mark#(X1), mark#(h(X)) -> active#(h(mark(X))))
        (mark#(g(X1, X2)) -> mark#(X1), mark#(f(X1, X2)) -> active#(f(mark(X1), X2)))
        (mark#(h(X)) -> active#(h(mark(X))), active#(g(a(), X)) -> mark#(f(b(), X)))
        (mark#(h(X)) -> active#(h(mark(X))), active#(h(X)) -> mark#(g(X, X)))
        (mark#(h(X)) -> active#(h(mark(X))), active#(f(X, X)) -> mark#(h(a())))}
       SCCS:
        Scc:
         {  mark#(g(X1, X2)) -> mark#(X1),
            mark#(g(X1, X2)) -> active#(g(mark(X1), X2)),
                 mark#(h(X)) -> mark#(X),
                 mark#(h(X)) -> active#(h(mark(X))),
            mark#(f(X1, X2)) -> active#(f(mark(X1), X2)),
          active#(g(a(), X)) -> mark#(f(b(), X)),
               active#(h(X)) -> mark#(g(X, X)),
            active#(f(X, X)) -> mark#(h(a()))}
        SCC:
         Strict:
          {  mark#(g(X1, X2)) -> mark#(X1),
             mark#(g(X1, X2)) -> active#(g(mark(X1), X2)),
                  mark#(h(X)) -> mark#(X),
                  mark#(h(X)) -> active#(h(mark(X))),
             mark#(f(X1, X2)) -> active#(f(mark(X1), X2)),
           active#(g(a(), X)) -> mark#(f(b(), X)),
                active#(h(X)) -> mark#(g(X, X)),
             active#(f(X, X)) -> mark#(h(a()))}
         Weak:
         {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
                 mark(h(X)) -> active(h(mark(X))),
            mark(f(X1, X2)) -> active(f(mark(X1), X2)),
                  mark(b()) -> active(b()),
                  mark(a()) -> active(a()),
            g(X1, mark(X2)) -> g(X1, X2),
          g(X1, active(X2)) -> g(X1, X2),
            g(mark(X1), X2) -> g(X1, X2),
          g(active(X1), X2) -> g(X1, X2),
          active(g(a(), X)) -> mark(f(b(), X)),
               active(h(X)) -> mark(g(X, X)),
            active(f(X, X)) -> mark(h(a())),
                active(a()) -> mark(b()),
                 h(mark(X)) -> h(X),
               h(active(X)) -> h(X),
            f(X1, mark(X2)) -> f(X1, X2),
          f(X1, active(X2)) -> f(X1, X2),
            f(mark(X1), X2) -> f(X1, X2),
          f(active(X1), X2) -> f(X1, X2)}
         POLY:
          Argument Filtering:
           pi(a) = [], pi(b) = [], pi(f) = [], pi(h) = [0], pi(active#) = 0, pi(active) = 0, pi(g) = [0], pi(mark#) = 0, pi(mark) = 0
          Usable Rules:
           {}
          Interpretation:
           [f] = 1,
           [g](x0) = x0 + 1,
           [h](x0) = x0 + 1,
           [a] = 0
          Strict:
           {  mark#(g(X1, X2)) -> active#(g(mark(X1), X2)),
                   mark#(h(X)) -> active#(h(mark(X))),
              mark#(f(X1, X2)) -> active#(f(mark(X1), X2)),
            active#(g(a(), X)) -> mark#(f(b(), X)),
                 active#(h(X)) -> mark#(g(X, X)),
              active#(f(X, X)) -> mark#(h(a()))}
          Weak:
           {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
                   mark(h(X)) -> active(h(mark(X))),
              mark(f(X1, X2)) -> active(f(mark(X1), X2)),
                    mark(b()) -> active(b()),
                    mark(a()) -> active(a()),
              g(X1, mark(X2)) -> g(X1, X2),
            g(X1, active(X2)) -> g(X1, X2),
              g(mark(X1), X2) -> g(X1, X2),
            g(active(X1), X2) -> g(X1, X2),
            active(g(a(), X)) -> mark(f(b(), X)),
                 active(h(X)) -> mark(g(X, X)),
              active(f(X, X)) -> mark(h(a())),
                  active(a()) -> mark(b()),
                   h(mark(X)) -> h(X),
                 h(active(X)) -> h(X),
              f(X1, mark(X2)) -> f(X1, X2),
            f(X1, active(X2)) -> f(X1, X2),
              f(mark(X1), X2) -> f(X1, X2),
            f(active(X1), X2) -> f(X1, X2)}
          EDG:
           {(mark#(g(X1, X2)) -> active#(g(mark(X1), X2)), active#(f(X, X)) -> mark#(h(a())))
            (mark#(g(X1, X2)) -> active#(g(mark(X1), X2)), active#(h(X)) -> mark#(g(X, X)))
            (mark#(g(X1, X2)) -> active#(g(mark(X1), X2)), active#(g(a(), X)) -> mark#(f(b(), X)))
            (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(f(X1, X2)) -> active#(f(mark(X1), X2)))
            (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(h(X)) -> active#(h(mark(X))))
            (active#(g(a(), X)) -> mark#(f(b(), X)), mark#(g(X1, X2)) -> active#(g(mark(X1), X2)))
            (active#(f(X, X)) -> mark#(h(a())), mark#(h(X)) -> active#(h(mark(X))))
            (active#(h(X)) -> mark#(g(X, X)), mark#(g(X1, X2)) -> active#(g(mark(X1), X2)))
            (active#(h(X)) -> mark#(g(X, X)), mark#(h(X)) -> active#(h(mark(X))))
            (active#(h(X)) -> mark#(g(X, X)), mark#(f(X1, X2)) -> active#(f(mark(X1), X2)))
            (mark#(f(X1, X2)) -> active#(f(mark(X1), X2)), active#(g(a(), X)) -> mark#(f(b(), X)))
            (mark#(f(X1, X2)) -> active#(f(mark(X1), X2)), active#(h(X)) -> mark#(g(X, X)))
            (mark#(f(X1, X2)) -> active#(f(mark(X1), X2)), active#(f(X, X)) -> mark#(h(a())))
            (mark#(h(X)) -> active#(h(mark(X))), active#(g(a(), X)) -> mark#(f(b(), X)))
            (mark#(h(X)) -> active#(h(mark(X))), active#(h(X)) -> mark#(g(X, X)))
            (mark#(h(X)) -> active#(h(mark(X))), active#(f(X, X)) -> mark#(h(a())))}
           SCCS:
            Scc:
             {  mark#(g(X1, X2)) -> active#(g(mark(X1), X2)),
                     mark#(h(X)) -> active#(h(mark(X))),
                mark#(f(X1, X2)) -> active#(f(mark(X1), X2)),
              active#(g(a(), X)) -> mark#(f(b(), X)),
                   active#(h(X)) -> mark#(g(X, X)),
                active#(f(X, X)) -> mark#(h(a()))}
            SCC:
             Strict:
              {  mark#(g(X1, X2)) -> active#(g(mark(X1), X2)),
                      mark#(h(X)) -> active#(h(mark(X))),
                 mark#(f(X1, X2)) -> active#(f(mark(X1), X2)),
               active#(g(a(), X)) -> mark#(f(b(), X)),
                    active#(h(X)) -> mark#(g(X, X)),
                 active#(f(X, X)) -> mark#(h(a()))}
             Weak:
             {  mark(g(X1, X2)) -> active(g(mark(X1), X2)),
                     mark(h(X)) -> active(h(mark(X))),
                mark(f(X1, X2)) -> active(f(mark(X1), X2)),
                      mark(b()) -> active(b()),
                      mark(a()) -> active(a()),
                g(X1, mark(X2)) -> g(X1, X2),
              g(X1, active(X2)) -> g(X1, X2),
                g(mark(X1), X2) -> g(X1, X2),
              g(active(X1), X2) -> g(X1, X2),
              active(g(a(), X)) -> mark(f(b(), X)),
                   active(h(X)) -> mark(g(X, X)),
                active(f(X, X)) -> mark(h(a())),
                    active(a()) -> mark(b()),
                     h(mark(X)) -> h(X),
                   h(active(X)) -> h(X),
                f(X1, mark(X2)) -> f(X1, X2),
              f(X1, active(X2)) -> f(X1, X2),
                f(mark(X1), X2) -> f(X1, X2),
              f(active(X1), X2) -> f(X1, X2)}
             Fail