YES
TRS:
 {     not(not(x)) -> x,
    not(and(x, y)) -> or(not(x), not(y)),
     not(or(x, y)) -> and(not(x), not(y)),
  and(x, or(y, z)) -> or(and(x, y), and(x, z)),
  and(or(y, z), x) -> or(and(x, y), and(x, z))}
 DP:
  Strict:
   {  not#(and(x, y)) -> not#(x),
      not#(and(x, y)) -> not#(y),
       not#(or(x, y)) -> not#(x),
       not#(or(x, y)) -> not#(y),
       not#(or(x, y)) -> and#(not(x), not(y)),
    and#(x, or(y, z)) -> and#(x, y),
    and#(x, or(y, z)) -> and#(x, z),
    and#(or(y, z), x) -> and#(x, y),
    and#(or(y, z), x) -> and#(x, z)}
  Weak:
  {     not(not(x)) -> x,
     not(and(x, y)) -> or(not(x), not(y)),
      not(or(x, y)) -> and(not(x), not(y)),
   and(x, or(y, z)) -> or(and(x, y), and(x, z)),
   and(or(y, z), x) -> or(and(x, y), and(x, z))}
  EDG:
   {(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#(y), not#(and(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(y), not#(and(x, y)) -> not#(x))
    (and#(or(y, z), x) -> and#(x, z), and#(or(y, z), x) -> and#(x, z))
    (and#(or(y, z), x) -> and#(x, z), and#(or(y, z), x) -> and#(x, y))
    (and#(or(y, z), x) -> and#(x, z), and#(x, or(y, z)) -> and#(x, z))
    (and#(or(y, z), x) -> and#(x, z), and#(x, or(y, z)) -> and#(x, y))
    (and#(or(y, z), x) -> and#(x, y), and#(or(y, z), x) -> and#(x, z))
    (and#(or(y, z), x) -> and#(x, y), and#(or(y, z), x) -> and#(x, y))
    (and#(or(y, z), x) -> and#(x, y), and#(x, or(y, z)) -> and#(x, z))
    (and#(or(y, z), x) -> and#(x, y), and#(x, or(y, z)) -> and#(x, 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#(y))
    (not#(or(x, y)) -> not#(x), 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)) -> 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))
    (not#(or(x, y)) -> and#(not(x), not(y)), and#(or(y, z), x) -> and#(x, y))
    (not#(or(x, y)) -> and#(not(x), not(y)), and#(or(y, z), x) -> and#(x, z))
    (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#(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)))
    (and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, y))
    (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#(or(y, z), x) -> and#(x, y))
    (and#(x, or(y, z)) -> and#(x, y), and#(or(y, z), x) -> and#(x, z))
    (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))
    (and#(x, or(y, z)) -> and#(x, z), and#(or(y, z), x) -> and#(x, y))
    (and#(x, or(y, z)) -> and#(x, z), and#(or(y, z), x) -> and#(x, z))
    (not#(and(x, y)) -> not#(y), not#(and(x, y)) -> not#(x))
    (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#(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)))}
   SCCS:
    Scc:
     {and#(x, or(y, z)) -> and#(x, y),
      and#(x, or(y, z)) -> and#(x, z),
      and#(or(y, z), x) -> and#(x, y),
      and#(or(y, z), x) -> and#(x, z)}
    Scc:
     {not#(and(x, y)) -> not#(x),
      not#(and(x, y)) -> not#(y),
       not#(or(x, y)) -> not#(x),
       not#(or(x, y)) -> not#(y)}
    SCC:
     Strict:
      {and#(x, or(y, z)) -> and#(x, y),
       and#(x, or(y, z)) -> and#(x, z),
       and#(or(y, z), x) -> and#(x, y),
       and#(or(y, z), x) -> and#(x, z)}
     Weak:
     {     not(not(x)) -> x,
        not(and(x, y)) -> or(not(x), not(y)),
         not(or(x, y)) -> and(not(x), not(y)),
      and(x, or(y, z)) -> or(and(x, y), and(x, z)),
      and(or(y, z), x) -> or(and(x, y), and(x, z))}
     POLY:
      Argument Filtering:
       pi(or) = [0,1], pi(and#) = [0,1], pi(and) = [], pi(not) = []
      Usable Rules:
       {}
      Interpretation:
       [and#](x0, x1) = x0 + x1,
       [or](x0, x1) = x0 + x1 + 1
      Strict:
       {}
      Weak:
       {     not(not(x)) -> x,
          not(and(x, y)) -> or(not(x), not(y)),
           not(or(x, y)) -> and(not(x), not(y)),
        and(x, or(y, z)) -> or(and(x, y), and(x, z)),
        and(or(y, z), x) -> or(and(x, y), and(x, z))}
      Qed
    SCC:
     Strict:
      {not#(and(x, y)) -> not#(x),
       not#(and(x, y)) -> not#(y),
        not#(or(x, y)) -> not#(x),
        not#(or(x, y)) -> not#(y)}
     Weak:
     {     not(not(x)) -> x,
        not(and(x, y)) -> or(not(x), not(y)),
         not(or(x, y)) -> and(not(x), not(y)),
      and(x, or(y, z)) -> or(and(x, y), and(x, z)),
      and(or(y, z), x) -> or(and(x, y), and(x, z))}
     SPSC:
      Simple Projection:
       pi(not#) = 0
      Strict:
       {not#(and(x, y)) -> not#(x),
        not#(and(x, y)) -> not#(y),
         not#(or(x, y)) -> not#(y)}
      EDG:
       {(not#(or(x, y)) -> not#(y), not#(or(x, y)) -> not#(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#(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#(x), not#(or(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)) -> not#(y))
        (not#(and(x, y)) -> not#(y), not#(or(x, y)) -> not#(y))}
       SCCS:
        Scc:
         {not#(and(x, y)) -> not#(x),
          not#(and(x, y)) -> not#(y),
           not#(or(x, y)) -> not#(y)}
        SCC:
         Strict:
          {not#(and(x, y)) -> not#(x),
           not#(and(x, y)) -> not#(y),
            not#(or(x, y)) -> not#(y)}
         Weak:
         {     not(not(x)) -> x,
            not(and(x, y)) -> or(not(x), not(y)),
             not(or(x, y)) -> and(not(x), not(y)),
          and(x, or(y, z)) -> or(and(x, y), and(x, z)),
          and(or(y, z), x) -> or(and(x, y), and(x, z))}
         SPSC:
          Simple Projection:
           pi(not#) = 0
          Strict:
           {not#(and(x, y)) -> not#(x),
             not#(or(x, y)) -> not#(y)}
          EDG:
           {(not#(or(x, y)) -> not#(y), not#(or(x, y)) -> not#(y))
            (not#(or(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)) -> not#(x), not#(or(x, y)) -> not#(y))}
           SCCS:
            Scc:
             {not#(and(x, y)) -> not#(x),
               not#(or(x, y)) -> not#(y)}
            SCC:
             Strict:
              {not#(and(x, y)) -> not#(x),
                not#(or(x, y)) -> not#(y)}
             Weak:
             {     not(not(x)) -> x,
                not(and(x, y)) -> or(not(x), not(y)),
                 not(or(x, y)) -> and(not(x), not(y)),
              and(x, or(y, z)) -> or(and(x, y), and(x, z)),
              and(or(y, z), x) -> or(and(x, y), and(x, z))}
             SPSC:
              Simple Projection:
               pi(not#) = 0
              Strict:
               {not#(or(x, y)) -> not#(y)}
              EDG:
               {(not#(or(x, y)) -> not#(y), not#(or(x, y)) -> not#(y))}
               SCCS:
                Scc:
                 {not#(or(x, y)) -> not#(y)}
                SCC:
                 Strict:
                  {not#(or(x, y)) -> not#(y)}
                 Weak:
                 {     not(not(x)) -> x,
                    not(and(x, y)) -> or(not(x), not(y)),
                     not(or(x, y)) -> and(not(x), not(y)),
                  and(x, or(y, z)) -> or(and(x, y), and(x, z)),
                  and(or(y, z), x) -> or(and(x, y), and(x, z))}
                 SPSC:
                  Simple Projection:
                   pi(not#) = 0
                  Strict:
                   {}
                  Qed