MAYBE
MAYBE
TRS:
 {
                        mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                             mark(from(X)) -> active(from(mark(X))),
                                mark(s(X)) -> active(s(mark(X))),
                         mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                                 mark(0()) -> active(0()),
                       mark(minus(X1, X2)) ->
  active(minus(mark(X1), mark(X2))),
                        mark(quot(X1, X2)) ->
  active(quot(mark(X1), mark(X2))),
                               mark(nil()) -> active(nil()),
                      mark(zWquot(X1, X2)) ->
  active(zWquot(mark(X1), mark(X2))),
                        cons(X1, mark(X2)) -> cons(X1, X2),
                      cons(X1, active(X2)) -> cons(X1, X2),
                        cons(mark(X1), X2) -> cons(X1, X2),
                      cons(active(X1), X2) -> cons(X1, X2),
                             from(mark(X)) -> from(X),
                           from(active(X)) -> from(X),
                                s(mark(X)) -> s(X),
                              s(active(X)) -> s(X),
                           active(from(X)) -> mark(cons(X, from(s(X)))),
            active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
             active(sel(0(), cons(X, XS))) -> mark(X),
                     active(minus(X, 0())) -> mark(0()),
                 active(minus(s(X), s(Y))) -> mark(minus(X, Y)),
                  active(quot(s(X), s(Y))) ->
  mark(s(quot(minus(X, Y), s(Y)))),
                   active(quot(0(), s(Y))) -> mark(0()),
                 active(zWquot(XS, nil())) -> mark(nil()),
  active(zWquot(cons(X, XS), cons(Y, YS))) ->
  mark(cons(quot(X, Y), zWquot(XS, YS))),
                 active(zWquot(nil(), XS)) -> mark(nil()),
                         sel(X1, mark(X2)) -> sel(X1, X2),
                       sel(X1, active(X2)) -> sel(X1, X2),
                         sel(mark(X1), X2) -> sel(X1, X2),
                       sel(active(X1), X2) -> sel(X1, X2),
                       minus(X1, mark(X2)) -> minus(X1, X2),
                     minus(X1, active(X2)) -> minus(X1, X2),
                       minus(mark(X1), X2) -> minus(X1, X2),
                     minus(active(X1), X2) -> minus(X1, X2),
                        quot(X1, mark(X2)) -> quot(X1, X2),
                      quot(X1, active(X2)) -> quot(X1, X2),
                        quot(mark(X1), X2) -> quot(X1, X2),
                      quot(active(X1), X2) -> quot(X1, X2),
                      zWquot(X1, mark(X2)) -> zWquot(X1, X2),
                    zWquot(X1, active(X2)) -> zWquot(X1, X2),
                      zWquot(mark(X1), X2) -> zWquot(X1, X2),
                    zWquot(active(X1), X2) -> zWquot(X1, X2)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                          mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                               mark(from(X)) -> active(from(mark(X))),
                                  mark(s(X)) -> active(s(mark(X))),
                           mark(sel(X1, X2)) ->
    active(sel(mark(X1), mark(X2))),
                                   mark(0()) -> active(0()),
                         mark(minus(X1, X2)) ->
    active(minus(mark(X1), mark(X2))),
                          mark(quot(X1, X2)) ->
    active(quot(mark(X1), mark(X2))),
                                 mark(nil()) -> active(nil()),
                        mark(zWquot(X1, X2)) ->
    active(zWquot(mark(X1), mark(X2))),
                          cons(X1, mark(X2)) -> cons(X1, X2),
                        cons(X1, active(X2)) -> cons(X1, X2),
                          cons(mark(X1), X2) -> cons(X1, X2),
                        cons(active(X1), X2) -> cons(X1, X2),
                               from(mark(X)) -> from(X),
                             from(active(X)) -> from(X),
                                  s(mark(X)) -> s(X),
                                s(active(X)) -> s(X),
                             active(from(X)) -> mark(cons(X, from(s(X)))),
              active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
               active(sel(0(), cons(X, XS))) -> mark(X),
                       active(minus(X, 0())) -> mark(0()),
                   active(minus(s(X), s(Y))) -> mark(minus(X, Y)),
                    active(quot(s(X), s(Y))) ->
    mark(s(quot(minus(X, Y), s(Y)))),
                     active(quot(0(), s(Y))) -> mark(0()),
                   active(zWquot(XS, nil())) -> mark(nil()),
    active(zWquot(cons(X, XS), cons(Y, YS))) ->
    mark(cons(quot(X, Y), zWquot(XS, YS))),
                   active(zWquot(nil(), XS)) -> mark(nil()),
                           sel(X1, mark(X2)) -> sel(X1, X2),
                         sel(X1, active(X2)) -> sel(X1, X2),
                           sel(mark(X1), X2) -> sel(X1, X2),
                         sel(active(X1), X2) -> sel(X1, X2),
                         minus(X1, mark(X2)) -> minus(X1, X2),
                       minus(X1, active(X2)) -> minus(X1, X2),
                         minus(mark(X1), X2) -> minus(X1, X2),
                       minus(active(X1), X2) -> minus(X1, X2),
                          quot(X1, mark(X2)) -> quot(X1, X2),
                        quot(X1, active(X2)) -> quot(X1, X2),
                          quot(mark(X1), X2) -> quot(X1, X2),
                        quot(active(X1), X2) -> quot(X1, X2),
                        zWquot(X1, mark(X2)) -> zWquot(X1, X2),
                      zWquot(X1, active(X2)) -> zWquot(X1, X2),
                        zWquot(mark(X1), X2) -> zWquot(X1, X2),
                      zWquot(active(X1), X2) -> zWquot(X1, X2)
   }
  Fail