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(rnil()) -> active(rnil()),
                       mark(2ndspos(X1, X2)) ->
  active(2ndspos(mark(X1), mark(X2))),
                                   mark(0()) -> active(0()),
                         mark(rcons(X1, X2)) ->
  active(rcons(mark(X1), mark(X2))),
                           mark(posrecip(X)) -> active(posrecip(mark(X))),
                       mark(2ndsneg(X1, X2)) ->
  active(2ndsneg(mark(X1), mark(X2))),
                           mark(negrecip(X)) -> active(negrecip(mark(X))),
                                 mark(pi(X)) -> active(pi(mark(X))),
                          mark(plus(X1, X2)) ->
  active(plus(mark(X1), mark(X2))),
                         mark(times(X1, X2)) ->
  active(times(mark(X1), mark(X2))),
                             mark(square(X)) -> active(square(mark(X))),
                          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(2ndspos(s(N), cons(X, cons(Y, Z)))) ->
  mark(rcons(posrecip(Y), 2ndsneg(N, Z))),
                     active(2ndspos(0(), Z)) -> mark(rnil()),
  active(2ndsneg(s(N), cons(X, cons(Y, Z)))) ->
  mark(rcons(negrecip(Y), 2ndspos(N, Z))),
                     active(2ndsneg(0(), Z)) -> mark(rnil()),
                               active(pi(X)) -> mark(2ndspos(X, from(0()))),
                       active(plus(s(X), Y)) -> mark(s(plus(X, Y))),
                        active(plus(0(), Y)) -> mark(Y),
                      active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))),
                       active(times(0(), Y)) -> mark(0()),
                           active(square(X)) -> mark(times(X, X)),
                       2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2),
                     2ndspos(X1, active(X2)) -> 2ndspos(X1, X2),
                       2ndspos(mark(X1), X2) -> 2ndspos(X1, X2),
                     2ndspos(active(X1), X2) -> 2ndspos(X1, X2),
                         rcons(X1, mark(X2)) -> rcons(X1, X2),
                       rcons(X1, active(X2)) -> rcons(X1, X2),
                         rcons(mark(X1), X2) -> rcons(X1, X2),
                       rcons(active(X1), X2) -> rcons(X1, X2),
                           posrecip(mark(X)) -> posrecip(X),
                         posrecip(active(X)) -> posrecip(X),
                       2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2),
                     2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2),
                       2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2),
                     2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2),
                           negrecip(mark(X)) -> negrecip(X),
                         negrecip(active(X)) -> negrecip(X),
                                 pi(mark(X)) -> pi(X),
                               pi(active(X)) -> pi(X),
                          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),
                         times(X1, mark(X2)) -> times(X1, X2),
                       times(X1, active(X2)) -> times(X1, X2),
                         times(mark(X1), X2) -> times(X1, X2),
                       times(active(X1), X2) -> times(X1, X2),
                             square(mark(X)) -> square(X),
                           square(active(X)) -> square(X)
 }
 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(rnil()) -> active(rnil()),
                         mark(2ndspos(X1, X2)) ->
    active(2ndspos(mark(X1), mark(X2))),
                                     mark(0()) -> active(0()),
                           mark(rcons(X1, X2)) ->
    active(rcons(mark(X1), mark(X2))),
                             mark(posrecip(X)) -> active(posrecip(mark(X))),
                         mark(2ndsneg(X1, X2)) ->
    active(2ndsneg(mark(X1), mark(X2))),
                             mark(negrecip(X)) -> active(negrecip(mark(X))),
                                   mark(pi(X)) -> active(pi(mark(X))),
                            mark(plus(X1, X2)) ->
    active(plus(mark(X1), mark(X2))),
                           mark(times(X1, X2)) ->
    active(times(mark(X1), mark(X2))),
                               mark(square(X)) -> active(square(mark(X))),
                            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(2ndspos(s(N), cons(X, cons(Y, Z)))) ->
    mark(rcons(posrecip(Y), 2ndsneg(N, Z))),
                       active(2ndspos(0(), Z)) -> mark(rnil()),
    active(2ndsneg(s(N), cons(X, cons(Y, Z)))) ->
    mark(rcons(negrecip(Y), 2ndspos(N, Z))),
                       active(2ndsneg(0(), Z)) -> mark(rnil()),
                                 active(pi(X)) -> mark(2ndspos(X, from(0()))),
                         active(plus(s(X), Y)) -> mark(s(plus(X, Y))),
                          active(plus(0(), Y)) -> mark(Y),
                        active(times(s(X), Y)) -> mark(plus(Y, times(X, Y))),
                         active(times(0(), Y)) -> mark(0()),
                             active(square(X)) -> mark(times(X, X)),
                         2ndspos(X1, mark(X2)) -> 2ndspos(X1, X2),
                       2ndspos(X1, active(X2)) -> 2ndspos(X1, X2),
                         2ndspos(mark(X1), X2) -> 2ndspos(X1, X2),
                       2ndspos(active(X1), X2) -> 2ndspos(X1, X2),
                           rcons(X1, mark(X2)) -> rcons(X1, X2),
                         rcons(X1, active(X2)) -> rcons(X1, X2),
                           rcons(mark(X1), X2) -> rcons(X1, X2),
                         rcons(active(X1), X2) -> rcons(X1, X2),
                             posrecip(mark(X)) -> posrecip(X),
                           posrecip(active(X)) -> posrecip(X),
                         2ndsneg(X1, mark(X2)) -> 2ndsneg(X1, X2),
                       2ndsneg(X1, active(X2)) -> 2ndsneg(X1, X2),
                         2ndsneg(mark(X1), X2) -> 2ndsneg(X1, X2),
                       2ndsneg(active(X1), X2) -> 2ndsneg(X1, X2),
                             negrecip(mark(X)) -> negrecip(X),
                           negrecip(active(X)) -> negrecip(X),
                                   pi(mark(X)) -> pi(X),
                                 pi(active(X)) -> pi(X),
                            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),
                           times(X1, mark(X2)) -> times(X1, X2),
                         times(X1, active(X2)) -> times(X1, X2),
                           times(mark(X1), X2) -> times(X1, X2),
                         times(active(X1), X2) -> times(X1, X2),
                               square(mark(X)) -> square(X),
                             square(active(X)) -> square(X)
   }
  Fail