YES
Time: 0.007807
TRS:
 {      and(x, false()) -> false(),
    and(x, not false()) -> x,
              not not x -> x,
    implies(x, false()) -> not x,
    implies(false(), y) -> not false(),
  implies(not x, not y) -> implies(y, and(x, y))}
 DP:
  DP:
   {  implies#(x, false()) -> not# x,
      implies#(false(), y) -> not# false(),
    implies#(not x, not y) -> and#(x, y),
    implies#(not x, not y) -> implies#(y, and(x, y))}
  TRS:
  {      and(x, false()) -> false(),
     and(x, not false()) -> x,
               not not x -> x,
     implies(x, false()) -> not x,
     implies(false(), y) -> not false(),
   implies(not x, not y) -> implies(y, and(x, y))}
  UR:
   {    and(x, false()) -> false(),
    and(x, not false()) -> x,
                a(z, w) -> z,
                a(z, w) -> w}
   EDG:
    {(implies#(not x, not y) -> implies#(y, and(x, y)), implies#(not x, not y) -> implies#(y, and(x, y)))
     (implies#(not x, not y) -> implies#(y, and(x, y)), implies#(not x, not y) -> and#(x, y))
     (implies#(not x, not y) -> implies#(y, and(x, y)), implies#(false(), y) -> not# false())
     (implies#(not x, not y) -> implies#(y, and(x, y)), implies#(x, false()) -> not# x)}
    STATUS:
     arrows: 0.750000
     SCCS (1):
      Scc:
       {implies#(not x, not y) -> implies#(y, and(x, y))}
      
      SCC (1):
       Strict:
        {implies#(not x, not y) -> implies#(y, and(x, y))}
       Weak:
       {      and(x, false()) -> false(),
          and(x, not false()) -> x,
                    not not x -> x,
          implies(x, false()) -> not x,
          implies(false(), y) -> not false(),
        implies(not x, not y) -> implies(y, and(x, y))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [and](x0, x1) = x0,
         
         [implies](x0, x1) = 0,
         
         [not](x0) = x0 + 1,
         
         [false] = 0,
         
         [implies#](x0, x1) = x0 + x1
        Strict:
         implies#(not x, not y) -> implies#(y, and(x, y))
         2 + 1x + 1y >= 0 + 1x + 1y
        Weak:
         implies(not x, not y) -> implies(y, and(x, y))
         0 + 0x + 0y >= 0 + 0x + 0y
         implies(false(), y) -> not false()
         0 + 0y >= 1
         implies(x, false()) -> not x
         0 + 0x >= 1 + 1x
         not not x -> x
         2 + 1x >= 1x
         and(x, not false()) -> x
         0 + 1x >= 1x
         and(x, false()) -> false()
         0 + 1x >= 0
       Qed