MAYBE
MAYBE
TRS:
 {
    g(mark(X1), X2) -> mark(g(X1, X2)),
  g(ok(X1), ok(X2)) -> ok(g(X1, X2)),
  active(g(X1, X2)) -> g(active(X1), X2),
  active(g(a(), X)) -> mark(f(b(), X)),
       active(h(X)) -> mark(g(X, X)),
       active(h(X)) -> h(active(X)),
    active(f(X, X)) -> mark(h(a())),
  active(f(X1, X2)) -> f(active(X1), X2),
        active(a()) -> mark(b()),
         h(mark(X)) -> mark(h(X)),
           h(ok(X)) -> ok(h(X)),
    f(mark(X1), X2) -> mark(f(X1, X2)),
  f(ok(X1), ok(X2)) -> ok(f(X1, X2)),
  proper(g(X1, X2)) -> g(proper(X1), proper(X2)),
       proper(h(X)) -> h(proper(X)),
  proper(f(X1, X2)) -> f(proper(X1), proper(X2)),
        proper(b()) -> ok(b()),
        proper(a()) -> ok(a()),
       top(mark(X)) -> top(proper(X)),
         top(ok(X)) -> top(active(X))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
      g(mark(X1), X2) -> mark(g(X1, X2)),
    g(ok(X1), ok(X2)) -> ok(g(X1, X2)),
    active(g(X1, X2)) -> g(active(X1), X2),
    active(g(a(), X)) -> mark(f(b(), X)),
         active(h(X)) -> mark(g(X, X)),
         active(h(X)) -> h(active(X)),
      active(f(X, X)) -> mark(h(a())),
    active(f(X1, X2)) -> f(active(X1), X2),
          active(a()) -> mark(b()),
           h(mark(X)) -> mark(h(X)),
             h(ok(X)) -> ok(h(X)),
      f(mark(X1), X2) -> mark(f(X1, X2)),
    f(ok(X1), ok(X2)) -> ok(f(X1, X2)),
    proper(g(X1, X2)) -> g(proper(X1), proper(X2)),
         proper(h(X)) -> h(proper(X)),
    proper(f(X1, X2)) -> f(proper(X1), proper(X2)),
          proper(b()) -> ok(b()),
          proper(a()) -> ok(a()),
         top(mark(X)) -> top(proper(X)),
           top(ok(X)) -> top(active(X))
   }
  Fail