YES
Time: 0.004533
TRS:
 {and(not not x, y, not z) -> and(y, band(x, z), x)}
 DP:
  DP:
   {and#(not not x, y, not z) -> and#(y, band(x, z), x)}
  TRS:
  {and(not not x, y, not z) -> and(y, band(x, z), x)}
  EDG:
   {(and#(not not x, y, not z) -> and#(y, band(x, z), x), and#(not not x, y, not z) -> and#(y, band(x, z), x))}
   SCCS (1):
    Scc:
     {and#(not not x, y, not z) -> and#(y, band(x, z), x)}
    SCC (1):
     Strict:
      {and#(not not x, y, not z) -> and#(y, band(x, z), x)}
     Weak:
     {and(not not x, y, not z) -> and(y, band(x, z), x)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [and](x0, x1, x2) = x0 + 1,
       
       [band](x0, x1) = 0,
       
       [not](x0) = 1,
       
       [and#](x0, x1, x2) = x0 + x1
      Strict:
       and#(not not x, y, not z) -> and#(y, band(x, z), x)
       1 + 1y + 0x + 0z >= 0 + 1y + 0x + 0z
      Weak:
       
     Qed