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