YES
TRS:
 {      or(x, x) -> x,
       and(x, x) -> x,
   not(or(x, y)) -> and(not(x), not(y)),
  not(and(x, y)) -> or(not(x), not(y)),
     not(not(x)) -> x}
 DP:
  Strict:
   { not#(or(x, y)) -> and#(not(x), not(y)),
     not#(or(x, y)) -> not#(x),
     not#(or(x, y)) -> not#(y),
    not#(and(x, y)) -> or#(not(x), not(y)),
    not#(and(x, y)) -> not#(x),
    not#(and(x, y)) -> not#(y)}
  Weak:
  {      or(x, x) -> x,
        and(x, x) -> x,
    not(or(x, y)) -> and(not(x), not(y)),
   not(and(x, y)) -> or(not(x), not(y)),
      not(not(x)) -> x}
  EDG:
   {(not#(and(x, y)) -> not#(x), not#(and(x, y)) -> not#(y))
    (not#(and(x, y)) -> not#(x), not#(and(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(x), not#(and(x, y)) -> or#(not(x), not(y)))
    (not#(and(x, y)) -> not#(x), not#(or(x, y)) -> not#(y))
    (not#(and(x, y)) -> not#(x), not#(or(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(x), not#(or(x, y)) -> and#(not(x), not(y)))
    (not#(and(x, y)) -> not#(y), not#(and(x, y)) -> not#(y))
    (not#(and(x, y)) -> not#(y), not#(and(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(y), not#(and(x, y)) -> or#(not(x), not(y)))
    (not#(and(x, y)) -> not#(y), not#(or(x, y)) -> not#(y))
    (not#(and(x, y)) -> not#(y), not#(or(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(y), not#(or(x, y)) -> and#(not(x), not(y)))
    (not#(or(x, y)) -> not#(y), not#(or(x, y)) -> and#(not(x), not(y)))
    (not#(or(x, y)) -> not#(y), not#(or(x, y)) -> not#(x))
    (not#(or(x, y)) -> not#(y), not#(or(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(y), not#(and(x, y)) -> or#(not(x), not(y)))
    (not#(or(x, y)) -> not#(y), not#(and(x, y)) -> not#(x))
    (not#(or(x, y)) -> not#(y), not#(and(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(x), not#(or(x, y)) -> and#(not(x), not(y)))
    (not#(or(x, y)) -> not#(x), not#(or(x, y)) -> not#(x))
    (not#(or(x, y)) -> not#(x), not#(or(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(x), not#(and(x, y)) -> or#(not(x), not(y)))
    (not#(or(x, y)) -> not#(x), not#(and(x, y)) -> not#(x))
    (not#(or(x, y)) -> not#(x), not#(and(x, y)) -> not#(y))}
   SCCS:
    Scc:
     { not#(or(x, y)) -> not#(x),
       not#(or(x, y)) -> not#(y),
      not#(and(x, y)) -> not#(x),
      not#(and(x, y)) -> not#(y)}
    SCC:
     Strict:
      { not#(or(x, y)) -> not#(x),
        not#(or(x, y)) -> not#(y),
       not#(and(x, y)) -> not#(x),
       not#(and(x, y)) -> not#(y)}
     Weak:
     {      or(x, x) -> x,
           and(x, x) -> x,
       not(or(x, y)) -> and(not(x), not(y)),
      not(and(x, y)) -> or(not(x), not(y)),
         not(not(x)) -> x}
     SPSC:
      Simple Projection:
       pi(not#) = 0
      Strict:
       { not#(or(x, y)) -> not#(x),
         not#(or(x, y)) -> not#(y),
        not#(and(x, y)) -> not#(y)}
      EDG:
       {(not#(and(x, y)) -> not#(y), not#(and(x, y)) -> not#(y))
        (not#(and(x, y)) -> not#(y), not#(or(x, y)) -> not#(y))
        (not#(and(x, y)) -> not#(y), not#(or(x, y)) -> not#(x))
        (not#(or(x, y)) -> not#(x), not#(or(x, y)) -> not#(x))
        (not#(or(x, y)) -> not#(x), not#(or(x, y)) -> not#(y))
        (not#(or(x, y)) -> not#(x), not#(and(x, y)) -> not#(y))
        (not#(or(x, y)) -> not#(y), not#(or(x, y)) -> not#(x))
        (not#(or(x, y)) -> not#(y), not#(or(x, y)) -> not#(y))
        (not#(or(x, y)) -> not#(y), not#(and(x, y)) -> not#(y))}
       SCCS:
        Scc:
         { not#(or(x, y)) -> not#(x),
           not#(or(x, y)) -> not#(y),
          not#(and(x, y)) -> not#(y)}
        SCC:
         Strict:
          { not#(or(x, y)) -> not#(x),
            not#(or(x, y)) -> not#(y),
           not#(and(x, y)) -> not#(y)}
         Weak:
         {      or(x, x) -> x,
               and(x, x) -> x,
           not(or(x, y)) -> and(not(x), not(y)),
          not(and(x, y)) -> or(not(x), not(y)),
             not(not(x)) -> x}
         SPSC:
          Simple Projection:
           pi(not#) = 0
          Strict:
           { not#(or(x, y)) -> not#(x),
            not#(and(x, y)) -> not#(y)}
          EDG:
           {(not#(and(x, y)) -> not#(y), not#(and(x, y)) -> not#(y))
            (not#(and(x, y)) -> not#(y), not#(or(x, y)) -> not#(x))
            (not#(or(x, y)) -> not#(x), not#(or(x, y)) -> not#(x))
            (not#(or(x, y)) -> not#(x), not#(and(x, y)) -> not#(y))}
           SCCS:
            Scc:
             { not#(or(x, y)) -> not#(x),
              not#(and(x, y)) -> not#(y)}
            SCC:
             Strict:
              { not#(or(x, y)) -> not#(x),
               not#(and(x, y)) -> not#(y)}
             Weak:
             {      or(x, x) -> x,
                   and(x, x) -> x,
               not(or(x, y)) -> and(not(x), not(y)),
              not(and(x, y)) -> or(not(x), not(y)),
                 not(not(x)) -> x}
             SPSC:
              Simple Projection:
               pi(not#) = 0
              Strict:
               {not#(and(x, y)) -> not#(y)}
              EDG:
               {(not#(and(x, y)) -> not#(y), not#(and(x, y)) -> not#(y))}
               SCCS:
                Scc:
                 {not#(and(x, y)) -> not#(y)}
                SCC:
                 Strict:
                  {not#(and(x, y)) -> not#(y)}
                 Weak:
                 {      or(x, x) -> x,
                       and(x, x) -> x,
                   not(or(x, y)) -> and(not(x), not(y)),
                  not(and(x, y)) -> or(not(x), not(y)),
                     not(not(x)) -> x}
                 SPSC:
                  Simple Projection:
                   pi(not#) = 0
                  Strict:
                   {}
                  Qed