MAYBE
MAYBE
TRS:
 {
                active(p(X)) -> p(active(X)),
              active(p(0())) -> mark(0()),
             active(p(s(X))) -> mark(X),
                active(s(X)) -> s(active(X)),
         active(leq(X1, X2)) -> leq(X1, active(X2)),
         active(leq(X1, X2)) -> leq(active(X1), X2),
         active(leq(0(), Y)) -> mark(true()),
      active(leq(s(X), 0())) -> mark(false()),
     active(leq(s(X), s(Y))) -> mark(leq(X, Y)),
      active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
    active(if(true(), X, Y)) -> mark(X),
   active(if(false(), X, Y)) -> mark(Y),
          active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))),
        active(diff(X1, X2)) -> diff(X1, active(X2)),
        active(diff(X1, X2)) -> diff(active(X1), X2),
                  p(mark(X)) -> mark(p(X)),
                    p(ok(X)) -> ok(p(X)),
                  s(mark(X)) -> mark(s(X)),
                    s(ok(X)) -> ok(s(X)),
           leq(X1, mark(X2)) -> mark(leq(X1, X2)),
           leq(mark(X1), X2) -> mark(leq(X1, X2)),
         leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)),
        if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
  if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
          diff(X1, mark(X2)) -> mark(diff(X1, X2)),
          diff(mark(X1), X2) -> mark(diff(X1, X2)),
        diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)),
                 proper(0()) -> ok(0()),
                proper(p(X)) -> p(proper(X)),
                proper(s(X)) -> s(proper(X)),
              proper(true()) -> ok(true()),
         proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)),
             proper(false()) -> ok(false()),
      proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
        proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)),
                top(mark(X)) -> top(proper(X)),
                  top(ok(X)) -> top(active(X))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                  active(p(X)) -> p(active(X)),
                active(p(0())) -> mark(0()),
               active(p(s(X))) -> mark(X),
                  active(s(X)) -> s(active(X)),
           active(leq(X1, X2)) -> leq(X1, active(X2)),
           active(leq(X1, X2)) -> leq(active(X1), X2),
           active(leq(0(), Y)) -> mark(true()),
        active(leq(s(X), 0())) -> mark(false()),
       active(leq(s(X), s(Y))) -> mark(leq(X, Y)),
        active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
      active(if(true(), X, Y)) -> mark(X),
     active(if(false(), X, Y)) -> mark(Y),
            active(diff(X, Y)) -> mark(if(leq(X, Y), 0(), s(diff(p(X), Y)))),
          active(diff(X1, X2)) -> diff(X1, active(X2)),
          active(diff(X1, X2)) -> diff(active(X1), X2),
                    p(mark(X)) -> mark(p(X)),
                      p(ok(X)) -> ok(p(X)),
                    s(mark(X)) -> mark(s(X)),
                      s(ok(X)) -> ok(s(X)),
             leq(X1, mark(X2)) -> mark(leq(X1, X2)),
             leq(mark(X1), X2) -> mark(leq(X1, X2)),
           leq(ok(X1), ok(X2)) -> ok(leq(X1, X2)),
          if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
    if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
            diff(X1, mark(X2)) -> mark(diff(X1, X2)),
            diff(mark(X1), X2) -> mark(diff(X1, X2)),
          diff(ok(X1), ok(X2)) -> ok(diff(X1, X2)),
                   proper(0()) -> ok(0()),
                  proper(p(X)) -> p(proper(X)),
                  proper(s(X)) -> s(proper(X)),
                proper(true()) -> ok(true()),
           proper(leq(X1, X2)) -> leq(proper(X1), proper(X2)),
               proper(false()) -> ok(false()),
        proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
          proper(diff(X1, X2)) -> diff(proper(X1), proper(X2)),
                  top(mark(X)) -> top(proper(X)),
                    top(ok(X)) -> top(active(X))
   }
  Fail