YES
Time: 0.004793
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))}
  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)}
   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:
       
     Qed