YES
TRS:
 {   not(or(x, y)) -> and(not(x), not(y)),
    not(and(x, y)) -> or(not(x), not(y)),
  and(x, or(y, z)) -> or(and(x, y), and(x, z))}
 DP:
  Strict:
   {   not#(or(x, y)) -> not#(x),
       not#(or(x, y)) -> not#(y),
       not#(or(x, y)) -> and#(not(x), not(y)),
      not#(and(x, y)) -> not#(x),
      not#(and(x, y)) -> not#(y),
    and#(x, or(y, z)) -> and#(x, y),
    and#(x, or(y, z)) -> and#(x, z)}
  Weak:
  {   not(or(x, y)) -> and(not(x), not(y)),
     not(and(x, y)) -> or(not(x), not(y)),
   and(x, or(y, z)) -> or(and(x, y), and(x, z))}
  EDG:
   {(and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, z))
    (and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, y))
    (not#(or(x, y)) -> not#(y), not#(and(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(y), not#(and(x, y)) -> not#(x))
    (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#(y))
    (not#(or(x, y)) -> not#(y), not#(or(x, y)) -> not#(x))
    (not#(or(x, y)) -> not#(x), not#(and(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(x), not#(and(x, y)) -> not#(x))
    (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#(y))
    (not#(or(x, y)) -> not#(x), not#(or(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(x), not#(or(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(x), not#(or(x, y)) -> not#(y))
    (not#(and(x, y)) -> not#(x), not#(or(x, y)) -> and#(not(x), not(y)))
    (not#(and(x, y)) -> not#(x), not#(and(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(x), not#(and(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)) -> not#(y))
    (not#(and(x, y)) -> not#(y), not#(or(x, y)) -> and#(not(x), not(y)))
    (not#(and(x, y)) -> not#(y), not#(and(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(y), not#(and(x, y)) -> not#(y))
    (and#(x, or(y, z)) -> and#(x, z), and#(x, or(y, z)) -> and#(x, y))
    (and#(x, or(y, z)) -> and#(x, z), and#(x, or(y, z)) -> and#(x, z))
    (not#(or(x, y)) -> and#(not(x), not(y)), and#(x, or(y, z)) -> and#(x, y))
    (not#(or(x, y)) -> and#(not(x), not(y)), and#(x, or(y, z)) -> and#(x, z))}
   SCCS:
    Scc:
     {and#(x, or(y, z)) -> and#(x, y),
      and#(x, or(y, z)) -> and#(x, z)}
    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:
      {and#(x, or(y, z)) -> and#(x, y),
       and#(x, or(y, z)) -> and#(x, z)}
     Weak:
     {   not(or(x, y)) -> and(not(x), not(y)),
        not(and(x, y)) -> or(not(x), not(y)),
      and(x, or(y, z)) -> or(and(x, y), and(x, z))}
     SPSC:
      Simple Projection:
       pi(and#) = 1
      Strict:
       {and#(x, or(y, z)) -> and#(x, z)}
      EDG:
       {(and#(x, or(y, z)) -> and#(x, z), and#(x, or(y, z)) -> and#(x, z))}
       SCCS:
        Scc:
         {and#(x, or(y, z)) -> and#(x, z)}
        SCC:
         Strict:
          {and#(x, or(y, z)) -> and#(x, z)}
         Weak:
         {   not(or(x, y)) -> and(not(x), not(y)),
            not(and(x, y)) -> or(not(x), not(y)),
          and(x, or(y, z)) -> or(and(x, y), and(x, z))}
         SPSC:
          Simple Projection:
           pi(and#) = 1
          Strict:
           {}
          Qed
    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:
     {   not(or(x, y)) -> and(not(x), not(y)),
        not(and(x, y)) -> or(not(x), not(y)),
      and(x, or(y, z)) -> or(and(x, y), and(x, z))}
     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:
         {   not(or(x, y)) -> and(not(x), not(y)),
            not(and(x, y)) -> or(not(x), not(y)),
          and(x, or(y, z)) -> or(and(x, y), and(x, z))}
         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:
             {   not(or(x, y)) -> and(not(x), not(y)),
                not(and(x, y)) -> or(not(x), not(y)),
              and(x, or(y, z)) -> or(and(x, y), and(x, z))}
             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:
                 {   not(or(x, y)) -> and(not(x), not(y)),
                    not(and(x, y)) -> or(not(x), not(y)),
                  and(x, or(y, z)) -> or(and(x, y), and(x, z))}
                 SPSC:
                  Simple Projection:
                   pi(not#) = 0
                  Strict:
                   {}
                  Qed