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