YES
Time: 0.002695
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:
  DP:
   {    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)}
  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))}
  EDG:
   {(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)
    (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))
    (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# 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)
    (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 (2):
    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 (2):
     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, y)}
      EDG:
       {(and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, y))}
       SCCS (1):
        Scc:
         {and#(x, or(y, z)) -> and#(x, y)}
        SCC (1):
         Strict:
          {and#(x, or(y, z)) -> and#(x, 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(and#) = 1
          Strict:
           {}
          Qed
    SCC (4):
     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 (1):
        Scc:
         { not# or(x, y) -> not# x,
           not# or(x, y) -> not# y,
          not# and(x, y) -> not# y}
        SCC (3):
         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# or(x, y) -> not# x, not# and(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# y, not# and(x, y) -> not# y)}
           SCCS (1):
            Scc:
             { not# or(x, y) -> not# x,
              not# and(x, y) -> not# y}
            SCC (2):
             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 (1):
                Scc:
                 {not# and(x, y) -> not# y}
                SCC (1):
                 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