MAYBE
MAYBE
TRS:
 {
    active(and(X1, X2)) -> and(active(X1), X2),
   active(and(tt(), X)) -> mark(X),
   active(plus(N, 0())) -> mark(N),
  active(plus(N, s(M))) -> mark(s(plus(N, M))),
   active(plus(X1, X2)) -> plus(X1, active(X2)),
   active(plus(X1, X2)) -> plus(active(X1), X2),
           active(s(X)) -> s(active(X)),
      active(x(N, 0())) -> mark(0()),
     active(x(N, s(M))) -> mark(plus(x(N, M), N)),
      active(x(X1, X2)) -> x(X1, active(X2)),
      active(x(X1, X2)) -> x(active(X1), X2),
      and(mark(X1), X2) -> mark(and(X1, X2)),
    and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
     plus(X1, mark(X2)) -> mark(plus(X1, X2)),
     plus(mark(X1), X2) -> mark(plus(X1, X2)),
   plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)),
             s(mark(X)) -> mark(s(X)),
               s(ok(X)) -> ok(s(X)),
        x(X1, mark(X2)) -> mark(x(X1, X2)),
        x(mark(X1), X2) -> mark(x(X1, X2)),
      x(ok(X1), ok(X2)) -> ok(x(X1, X2)),
    proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
           proper(tt()) -> ok(tt()),
   proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)),
            proper(0()) -> ok(0()),
           proper(s(X)) -> s(proper(X)),
      proper(x(X1, X2)) -> x(proper(X1), proper(X2)),
           top(mark(X)) -> top(proper(X)),
             top(ok(X)) -> top(active(X))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
      active(and(X1, X2)) -> and(active(X1), X2),
     active(and(tt(), X)) -> mark(X),
     active(plus(N, 0())) -> mark(N),
    active(plus(N, s(M))) -> mark(s(plus(N, M))),
     active(plus(X1, X2)) -> plus(X1, active(X2)),
     active(plus(X1, X2)) -> plus(active(X1), X2),
             active(s(X)) -> s(active(X)),
        active(x(N, 0())) -> mark(0()),
       active(x(N, s(M))) -> mark(plus(x(N, M), N)),
        active(x(X1, X2)) -> x(X1, active(X2)),
        active(x(X1, X2)) -> x(active(X1), X2),
        and(mark(X1), X2) -> mark(and(X1, X2)),
      and(ok(X1), ok(X2)) -> ok(and(X1, X2)),
       plus(X1, mark(X2)) -> mark(plus(X1, X2)),
       plus(mark(X1), X2) -> mark(plus(X1, X2)),
     plus(ok(X1), ok(X2)) -> ok(plus(X1, X2)),
               s(mark(X)) -> mark(s(X)),
                 s(ok(X)) -> ok(s(X)),
          x(X1, mark(X2)) -> mark(x(X1, X2)),
          x(mark(X1), X2) -> mark(x(X1, X2)),
        x(ok(X1), ok(X2)) -> ok(x(X1, X2)),
      proper(and(X1, X2)) -> and(proper(X1), proper(X2)),
             proper(tt()) -> ok(tt()),
     proper(plus(X1, X2)) -> plus(proper(X1), proper(X2)),
              proper(0()) -> ok(0()),
             proper(s(X)) -> s(proper(X)),
        proper(x(X1, X2)) -> x(proper(X1), proper(X2)),
             top(mark(X)) -> top(proper(X)),
               top(ok(X)) -> top(active(X))
   }
  Fail