MAYBE
MAYBE
TRS:
 {
                        cons(mark(X1), X2) -> mark(cons(X1, X2)),
                      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                             from(mark(X)) -> mark(from(X)),
                               from(ok(X)) -> ok(from(X)),
                                s(mark(X)) -> mark(s(X)),
                                  s(ok(X)) -> ok(s(X)),
                      active(cons(X1, X2)) -> cons(active(X1), X2),
                           active(from(X)) -> mark(cons(X, from(s(X)))),
                           active(from(X)) -> from(active(X)),
                              active(s(X)) -> s(active(X)),
                       active(sel(X1, X2)) -> sel(X1, active(X2)),
                       active(sel(X1, X2)) -> sel(active(X1), X2),
            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(X1, X2)) -> minus(X1, active(X2)),
                     active(minus(X1, X2)) -> minus(active(X1), X2),
                 active(minus(s(X), s(Y))) -> mark(minus(X, Y)),
                      active(quot(X1, X2)) -> quot(X1, active(X2)),
                      active(quot(X1, X2)) -> quot(active(X1), X2),
                  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(X1, X2)) -> zWquot(X1, active(X2)),
                    active(zWquot(X1, X2)) -> zWquot(active(X1), X2),
  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)) -> mark(sel(X1, X2)),
                         sel(mark(X1), X2) -> mark(sel(X1, X2)),
                       sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                       minus(X1, mark(X2)) -> mark(minus(X1, X2)),
                       minus(mark(X1), X2) -> mark(minus(X1, X2)),
                     minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)),
                        quot(X1, mark(X2)) -> mark(quot(X1, X2)),
                        quot(mark(X1), X2) -> mark(quot(X1, X2)),
                      quot(ok(X1), ok(X2)) -> ok(quot(X1, X2)),
                      zWquot(X1, mark(X2)) -> mark(zWquot(X1, X2)),
                      zWquot(mark(X1), X2) -> mark(zWquot(X1, X2)),
                    zWquot(ok(X1), ok(X2)) -> ok(zWquot(X1, X2)),
                      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                           proper(from(X)) -> from(proper(X)),
                              proper(s(X)) -> s(proper(X)),
                       proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                               proper(0()) -> ok(0()),
                     proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)),
                      proper(quot(X1, X2)) -> quot(proper(X1), proper(X2)),
                             proper(nil()) -> ok(nil()),
                    proper(zWquot(X1, X2)) -> zWquot(proper(X1), proper(X2)),
                              top(mark(X)) -> top(proper(X)),
                                top(ok(X)) -> top(active(X))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                          cons(mark(X1), X2) -> mark(cons(X1, X2)),
                        cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                               from(mark(X)) -> mark(from(X)),
                                 from(ok(X)) -> ok(from(X)),
                                  s(mark(X)) -> mark(s(X)),
                                    s(ok(X)) -> ok(s(X)),
                        active(cons(X1, X2)) -> cons(active(X1), X2),
                             active(from(X)) -> mark(cons(X, from(s(X)))),
                             active(from(X)) -> from(active(X)),
                                active(s(X)) -> s(active(X)),
                         active(sel(X1, X2)) -> sel(X1, active(X2)),
                         active(sel(X1, X2)) -> sel(active(X1), X2),
              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(X1, X2)) -> minus(X1, active(X2)),
                       active(minus(X1, X2)) -> minus(active(X1), X2),
                   active(minus(s(X), s(Y))) -> mark(minus(X, Y)),
                        active(quot(X1, X2)) -> quot(X1, active(X2)),
                        active(quot(X1, X2)) -> quot(active(X1), X2),
                    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(X1, X2)) -> zWquot(X1, active(X2)),
                      active(zWquot(X1, X2)) -> zWquot(active(X1), X2),
    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)) -> mark(sel(X1, X2)),
                           sel(mark(X1), X2) -> mark(sel(X1, X2)),
                         sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                         minus(X1, mark(X2)) -> mark(minus(X1, X2)),
                         minus(mark(X1), X2) -> mark(minus(X1, X2)),
                       minus(ok(X1), ok(X2)) -> ok(minus(X1, X2)),
                          quot(X1, mark(X2)) -> mark(quot(X1, X2)),
                          quot(mark(X1), X2) -> mark(quot(X1, X2)),
                        quot(ok(X1), ok(X2)) -> ok(quot(X1, X2)),
                        zWquot(X1, mark(X2)) -> mark(zWquot(X1, X2)),
                        zWquot(mark(X1), X2) -> mark(zWquot(X1, X2)),
                      zWquot(ok(X1), ok(X2)) -> ok(zWquot(X1, X2)),
                        proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                             proper(from(X)) -> from(proper(X)),
                                proper(s(X)) -> s(proper(X)),
                         proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                 proper(0()) -> ok(0()),
                       proper(minus(X1, X2)) -> minus(proper(X1), proper(X2)),
                        proper(quot(X1, X2)) -> quot(proper(X1), proper(X2)),
                               proper(nil()) -> ok(nil()),
                      proper(zWquot(X1, X2)) ->
    zWquot(proper(X1), proper(X2)),
                                top(mark(X)) -> top(proper(X)),
                                  top(ok(X)) -> top(active(X))
   }
  Fail