YES
Time: 0.041505
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))}
  UR:
   {    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)),
             a(w, v) -> w,
             a(w, v) -> v}
   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))}
    STATUS:
     arrows: 0.469388
     SCCS (2):
      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:
       {and#(x, or(y, z)) -> and#(x, y),
        and#(x, or(y, z)) -> and#(x, z)}
      
      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))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [or](x0, x1) = x0 + x1,
         
         [and](x0, x1) = x0 + x1 + 1,
         
         [not](x0) = 0,
         
         [not#](x0) = x0
        Strict:
         not# and(x, y) -> not# y
         1 + 1x + 1y >= 0 + 1y
         not# and(x, y) -> not# x
         1 + 1x + 1y >= 0 + 1x
         not# or(x, y) -> not# y
         0 + 1x + 1y >= 0 + 1y
         not# or(x, y) -> not# x
         0 + 1x + 1y >= 0 + 1x
        Weak:
         and(x, or(y, z)) -> or(and(x, y), and(x, z))
         1 + 1x + 1y + 1z >= 2 + 2x + 1y + 1z
         not and(x, y) -> or(not x, not y)
         0 + 0x + 0y >= 0 + 0x + 0y
         not or(x, y) -> and(not x, not y)
         0 + 0x + 0y >= 1 + 0x + 0y
       SCCS (1):
        Scc:
         {not# or(x, y) -> not# x,
          not# or(x, y) -> not# y}
        
        SCC (2):
         Strict:
          {not# or(x, y) -> not# x,
           not# or(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))}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [or](x0, x1) = x0 + x1 + 1,
           
           [and](x0, x1) = 0,
           
           [not](x0) = x0 + 1,
           
           [not#](x0) = x0
          Strict:
           not# or(x, y) -> not# y
           1 + 1x + 1y >= 0 + 1y
           not# or(x, y) -> not# x
           1 + 1x + 1y >= 0 + 1x
          Weak:
           and(x, or(y, z)) -> or(and(x, y), and(x, z))
           0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z
           not and(x, y) -> or(not x, not y)
           1 + 0x + 0y >= 3 + 1x + 1y
           not or(x, y) -> and(not x, not y)
           2 + 1x + 1y >= 0 + 0x + 0y
         Qed
     
     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))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [or](x0, x1) = x0 + x1 + 1,
        
        [and](x0, x1) = 0,
        
        [not](x0) = x0 + 1,
        
        [and#](x0, x1) = x0
       Strict:
        and#(x, or(y, z)) -> and#(x, z)
        1 + 0x + 1y + 1z >= 0 + 0x + 1z
        and#(x, or(y, z)) -> and#(x, y)
        1 + 0x + 1y + 1z >= 0 + 0x + 1y
       Weak:
        and(x, or(y, z)) -> or(and(x, y), and(x, z))
        0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z
        not and(x, y) -> or(not x, not y)
        1 + 0x + 0y >= 3 + 1x + 1y
        not or(x, y) -> and(not x, not y)
        2 + 1x + 1y >= 0 + 0x + 0y
      Qed