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