MAYBE
MAYBE
TRS:
 {
       mark(if(X1, X2, X3)) -> active(if(mark(X1), mark(X2), X3)),
                  mark(c()) -> active(c()),
                 mark(f(X)) -> active(f(mark(X))),
               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),
                 f(mark(X)) -> f(X),
               f(active(X)) -> f(X),
   active(if(true(), X, Y)) -> mark(X),
  active(if(false(), X, Y)) -> mark(Y),
               active(f(X)) -> mark(if(X, c(), f(true())))
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
         mark(if(X1, X2, X3)) -> active(if(mark(X1), mark(X2), X3)),
                    mark(c()) -> active(c()),
                   mark(f(X)) -> active(f(mark(X))),
                 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),
                   f(mark(X)) -> f(X),
                 f(active(X)) -> f(X),
     active(if(true(), X, Y)) -> mark(X),
    active(if(false(), X, Y)) -> mark(Y),
                 active(f(X)) -> mark(if(X, c(), f(true())))
   }
  Fail