MAYBE
MAYBE
TRS:
 {
                mark(and(X1, X2)) -> active(and(mark(X1), X2)),
                     mark(true()) -> active(true()),
                    mark(false()) -> active(false()),
             mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)),
                mark(add(X1, X2)) -> active(add(mark(X1), X2)),
                        mark(0()) -> active(0()),
                       mark(s(X)) -> active(s(X)),
                      mark(nil()) -> active(nil()),
              mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
               mark(cons(X1, X2)) -> active(cons(X1, X2)),
                    mark(from(X)) -> active(from(X)),
           active(and(true(), X)) -> mark(X),
          active(and(false(), Y)) -> mark(false()),
         active(if(true(), X, Y)) -> mark(X),
        active(if(false(), X, Y)) -> mark(Y),
              active(add(0(), X)) -> mark(X),
             active(add(s(X), Y)) -> mark(s(add(X, Y))),
            active(first(0(), X)) -> mark(nil()),
  active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                  active(from(X)) -> mark(cons(X, from(s(X)))),
                and(X1, mark(X2)) -> and(X1, X2),
              and(X1, active(X2)) -> and(X1, X2),
                and(mark(X1), X2) -> and(X1, X2),
              and(active(X1), X2) -> and(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),
                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),
                       s(mark(X)) -> s(X),
                     s(active(X)) -> s(X),
              first(X1, mark(X2)) -> first(X1, X2),
            first(X1, active(X2)) -> first(X1, X2),
              first(mark(X1), X2) -> first(X1, X2),
            first(active(X1), X2) -> first(X1, X2),
               cons(X1, mark(X2)) -> cons(X1, X2),
             cons(X1, active(X2)) -> cons(X1, X2),
               cons(mark(X1), X2) -> cons(X1, X2),
             cons(active(X1), X2) -> cons(X1, X2),
                    from(mark(X)) -> from(X),
                  from(active(X)) -> from(X)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                  mark(and(X1, X2)) -> active(and(mark(X1), X2)),
                       mark(true()) -> active(true()),
                      mark(false()) -> active(false()),
               mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)),
                  mark(add(X1, X2)) -> active(add(mark(X1), X2)),
                          mark(0()) -> active(0()),
                         mark(s(X)) -> active(s(X)),
                        mark(nil()) -> active(nil()),
                mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                 mark(cons(X1, X2)) -> active(cons(X1, X2)),
                      mark(from(X)) -> active(from(X)),
             active(and(true(), X)) -> mark(X),
            active(and(false(), Y)) -> mark(false()),
           active(if(true(), X, Y)) -> mark(X),
          active(if(false(), X, Y)) -> mark(Y),
                active(add(0(), X)) -> mark(X),
               active(add(s(X), Y)) -> mark(s(add(X, Y))),
              active(first(0(), X)) -> mark(nil()),
    active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                    active(from(X)) -> mark(cons(X, from(s(X)))),
                  and(X1, mark(X2)) -> and(X1, X2),
                and(X1, active(X2)) -> and(X1, X2),
                  and(mark(X1), X2) -> and(X1, X2),
                and(active(X1), X2) -> and(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),
                  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),
                         s(mark(X)) -> s(X),
                       s(active(X)) -> s(X),
                first(X1, mark(X2)) -> first(X1, X2),
              first(X1, active(X2)) -> first(X1, X2),
                first(mark(X1), X2) -> first(X1, X2),
              first(active(X1), X2) -> first(X1, X2),
                 cons(X1, mark(X2)) -> cons(X1, X2),
               cons(X1, active(X2)) -> cons(X1, X2),
                 cons(mark(X1), X2) -> cons(X1, X2),
               cons(active(X1), X2) -> cons(X1, X2),
                      from(mark(X)) -> from(X),
                    from(active(X)) -> from(X)
   }
  Fail