MAYBE
MAYBE
TRS:
 {
        if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
  if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
               zero(mark(X)) -> mark(zero(X)),
                 zero(ok(X)) -> ok(zero(X)),
                  s(mark(X)) -> mark(s(X)),
                    s(ok(X)) -> ok(s(X)),
          prod(X1, mark(X2)) -> mark(prod(X1, X2)),
          prod(mark(X1), X2) -> mark(prod(X1, X2)),
        prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
               fact(mark(X)) -> mark(fact(X)),
                 fact(ok(X)) -> ok(fact(X)),
                  p(mark(X)) -> mark(p(X)),
                    p(ok(X)) -> ok(p(X)),
      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(zero(X)) -> zero(active(X)),
          active(zero(s(X))) -> mark(false()),
           active(zero(0())) -> mark(true()),
                active(s(X)) -> s(active(X)),
        active(prod(X1, X2)) -> prod(X1, active(X2)),
        active(prod(X1, X2)) -> prod(active(X1), X2),
       active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
        active(prod(0(), X)) -> mark(0()),
             active(fact(X)) ->
  mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
             active(fact(X)) -> fact(active(X)),
                active(p(X)) -> p(active(X)),
             active(p(s(X))) -> mark(X),
         active(add(X1, X2)) -> add(X1, active(X2)),
         active(add(X1, X2)) -> add(active(X1), X2),
        active(add(s(X), Y)) -> mark(s(add(X, Y))),
         active(add(0(), X)) -> mark(X),
           add(X1, mark(X2)) -> mark(add(X1, X2)),
           add(mark(X1), X2) -> mark(add(X1, X2)),
         add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
      proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
             proper(zero(X)) -> zero(proper(X)),
                proper(s(X)) -> s(proper(X)),
                 proper(0()) -> ok(0()),
        proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
             proper(fact(X)) -> fact(proper(X)),
                proper(p(X)) -> p(proper(X)),
         proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
              proper(true()) -> ok(true()),
             proper(false()) -> ok(false()),
                top(mark(X)) -> top(proper(X)),
                  top(ok(X)) -> top(active(X))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
          if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
    if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                 zero(mark(X)) -> mark(zero(X)),
                   zero(ok(X)) -> ok(zero(X)),
                    s(mark(X)) -> mark(s(X)),
                      s(ok(X)) -> ok(s(X)),
            prod(X1, mark(X2)) -> mark(prod(X1, X2)),
            prod(mark(X1), X2) -> mark(prod(X1, X2)),
          prod(ok(X1), ok(X2)) -> ok(prod(X1, X2)),
                 fact(mark(X)) -> mark(fact(X)),
                   fact(ok(X)) -> ok(fact(X)),
                    p(mark(X)) -> mark(p(X)),
                      p(ok(X)) -> ok(p(X)),
        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(zero(X)) -> zero(active(X)),
            active(zero(s(X))) -> mark(false()),
             active(zero(0())) -> mark(true()),
                  active(s(X)) -> s(active(X)),
          active(prod(X1, X2)) -> prod(X1, active(X2)),
          active(prod(X1, X2)) -> prod(active(X1), X2),
         active(prod(s(X), Y)) -> mark(add(Y, prod(X, Y))),
          active(prod(0(), X)) -> mark(0()),
               active(fact(X)) ->
    mark(if(zero(X), s(0()), prod(X, fact(p(X))))),
               active(fact(X)) -> fact(active(X)),
                  active(p(X)) -> p(active(X)),
               active(p(s(X))) -> mark(X),
           active(add(X1, X2)) -> add(X1, active(X2)),
           active(add(X1, X2)) -> add(active(X1), X2),
          active(add(s(X), Y)) -> mark(s(add(X, Y))),
           active(add(0(), X)) -> mark(X),
             add(X1, mark(X2)) -> mark(add(X1, X2)),
             add(mark(X1), X2) -> mark(add(X1, X2)),
           add(ok(X1), ok(X2)) -> ok(add(X1, X2)),
        proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
               proper(zero(X)) -> zero(proper(X)),
                  proper(s(X)) -> s(proper(X)),
                   proper(0()) -> ok(0()),
          proper(prod(X1, X2)) -> prod(proper(X1), proper(X2)),
               proper(fact(X)) -> fact(proper(X)),
                  proper(p(X)) -> p(proper(X)),
           proper(add(X1, X2)) -> add(proper(X1), proper(X2)),
                proper(true()) -> ok(true()),
               proper(false()) -> ok(false()),
                  top(mark(X)) -> top(proper(X)),
                    top(ok(X)) -> top(active(X))
   }
  Fail