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