YES
TRS:
 {   not(not(x)) -> x,
  not(and(x, y)) -> or(not(not(not(x))), not(not(not(y)))),
   not(or(x, y)) -> and(not(not(not(x))), not(not(not(y))))}
 DP:
  Strict:
   {not#(and(x, y)) -> not#(x),
    not#(and(x, y)) -> not#(y),
    not#(and(x, y)) -> not#(not(x)),
    not#(and(x, y)) -> not#(not(y)),
    not#(and(x, y)) -> not#(not(not(x))),
    not#(and(x, y)) -> not#(not(not(y))),
     not#(or(x, y)) -> not#(x),
     not#(or(x, y)) -> not#(y),
     not#(or(x, y)) -> not#(not(x)),
     not#(or(x, y)) -> not#(not(y)),
     not#(or(x, y)) -> not#(not(not(x))),
     not#(or(x, y)) -> not#(not(not(y)))}
  Weak:
  {   not(not(x)) -> x,
   not(and(x, y)) -> or(not(not(not(x))), not(not(not(y)))),
    not(or(x, y)) -> and(not(not(not(x))), not(not(not(y))))}
  EDG:
   {(not#(and(x, y)) -> not#(not(not(y))), not#(or(x, y)) -> not#(not(not(y))))
    (not#(and(x, y)) -> not#(not(not(y))), not#(or(x, y)) -> not#(not(not(x))))
    (not#(and(x, y)) -> not#(not(not(y))), not#(or(x, y)) -> not#(not(y)))
    (not#(and(x, y)) -> not#(not(not(y))), not#(or(x, y)) -> not#(not(x)))
    (not#(and(x, y)) -> not#(not(not(y))), not#(or(x, y)) -> not#(y))
    (not#(and(x, y)) -> not#(not(not(y))), not#(or(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(not(not(y))), not#(and(x, y)) -> not#(not(not(y))))
    (not#(and(x, y)) -> not#(not(not(y))), not#(and(x, y)) -> not#(not(not(x))))
    (not#(and(x, y)) -> not#(not(not(y))), not#(and(x, y)) -> not#(not(y)))
    (not#(and(x, y)) -> not#(not(not(y))), not#(and(x, y)) -> not#(not(x)))
    (not#(and(x, y)) -> not#(not(not(y))), not#(and(x, y)) -> not#(y))
    (not#(and(x, y)) -> not#(not(not(y))), not#(and(x, y)) -> not#(x))
    (not#(or(x, y)) -> not#(not(not(y))), not#(or(x, y)) -> not#(not(not(y))))
    (not#(or(x, y)) -> not#(not(not(y))), not#(or(x, y)) -> not#(not(not(x))))
    (not#(or(x, y)) -> not#(not(not(y))), not#(or(x, y)) -> not#(not(y)))
    (not#(or(x, y)) -> not#(not(not(y))), not#(or(x, y)) -> not#(not(x)))
    (not#(or(x, y)) -> not#(not(not(y))), not#(or(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(not(not(y))), not#(or(x, y)) -> not#(x))
    (not#(or(x, y)) -> not#(not(not(y))), not#(and(x, y)) -> not#(not(not(y))))
    (not#(or(x, y)) -> not#(not(not(y))), not#(and(x, y)) -> not#(not(not(x))))
    (not#(or(x, y)) -> not#(not(not(y))), not#(and(x, y)) -> not#(not(y)))
    (not#(or(x, y)) -> not#(not(not(y))), not#(and(x, y)) -> not#(not(x)))
    (not#(or(x, y)) -> not#(not(not(y))), not#(and(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(not(not(y))), not#(and(x, y)) -> not#(x))
    (not#(or(x, y)) -> not#(x), not#(or(x, y)) -> not#(not(not(y))))
    (not#(or(x, y)) -> not#(x), not#(or(x, y)) -> not#(not(not(x))))
    (not#(or(x, y)) -> not#(x), not#(or(x, y)) -> not#(not(y)))
    (not#(or(x, y)) -> not#(x), not#(or(x, y)) -> not#(not(x)))
    (not#(or(x, y)) -> not#(x), not#(or(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(x), not#(or(x, y)) -> not#(x))
    (not#(or(x, y)) -> not#(x), not#(and(x, y)) -> not#(not(not(y))))
    (not#(or(x, y)) -> not#(x), not#(and(x, y)) -> not#(not(not(x))))
    (not#(or(x, y)) -> not#(x), not#(and(x, y)) -> not#(not(y)))
    (not#(or(x, y)) -> not#(x), not#(and(x, y)) -> not#(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#(y), not#(or(x, y)) -> not#(not(not(y))))
    (not#(or(x, y)) -> not#(y), not#(or(x, y)) -> not#(not(not(x))))
    (not#(or(x, y)) -> not#(y), not#(or(x, y)) -> not#(not(y)))
    (not#(or(x, y)) -> not#(y), not#(or(x, y)) -> not#(not(x)))
    (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#(y), not#(and(x, y)) -> not#(not(not(y))))
    (not#(or(x, y)) -> not#(y), not#(and(x, y)) -> not#(not(not(x))))
    (not#(or(x, y)) -> not#(y), not#(and(x, y)) -> not#(not(y)))
    (not#(or(x, y)) -> not#(y), not#(and(x, y)) -> not#(not(x)))
    (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#(not(y)), not#(or(x, y)) -> not#(not(not(y))))
    (not#(or(x, y)) -> not#(not(y)), not#(or(x, y)) -> not#(not(not(x))))
    (not#(or(x, y)) -> not#(not(y)), not#(or(x, y)) -> not#(not(y)))
    (not#(or(x, y)) -> not#(not(y)), not#(or(x, y)) -> not#(not(x)))
    (not#(or(x, y)) -> not#(not(y)), not#(or(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(not(y)), not#(or(x, y)) -> not#(x))
    (not#(or(x, y)) -> not#(not(y)), not#(and(x, y)) -> not#(not(not(y))))
    (not#(or(x, y)) -> not#(not(y)), not#(and(x, y)) -> not#(not(not(x))))
    (not#(or(x, y)) -> not#(not(y)), not#(and(x, y)) -> not#(not(y)))
    (not#(or(x, y)) -> not#(not(y)), not#(and(x, y)) -> not#(not(x)))
    (not#(or(x, y)) -> not#(not(y)), not#(and(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(not(y)), not#(and(x, y)) -> not#(x))
    (not#(or(x, y)) -> not#(not(x)), not#(or(x, y)) -> not#(not(not(y))))
    (not#(or(x, y)) -> not#(not(x)), not#(or(x, y)) -> not#(not(not(x))))
    (not#(or(x, y)) -> not#(not(x)), not#(or(x, y)) -> not#(not(y)))
    (not#(or(x, y)) -> not#(not(x)), not#(or(x, y)) -> not#(not(x)))
    (not#(or(x, y)) -> not#(not(x)), not#(or(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(not(x)), not#(or(x, y)) -> not#(x))
    (not#(or(x, y)) -> not#(not(x)), not#(and(x, y)) -> not#(not(not(y))))
    (not#(or(x, y)) -> not#(not(x)), not#(and(x, y)) -> not#(not(not(x))))
    (not#(or(x, y)) -> not#(not(x)), not#(and(x, y)) -> not#(not(y)))
    (not#(or(x, y)) -> not#(not(x)), not#(and(x, y)) -> not#(not(x)))
    (not#(or(x, y)) -> not#(not(x)), not#(and(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(not(x)), not#(and(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(not(x)), not#(and(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(not(x)), not#(and(x, y)) -> not#(y))
    (not#(and(x, y)) -> not#(not(x)), not#(and(x, y)) -> not#(not(x)))
    (not#(and(x, y)) -> not#(not(x)), not#(and(x, y)) -> not#(not(y)))
    (not#(and(x, y)) -> not#(not(x)), not#(and(x, y)) -> not#(not(not(x))))
    (not#(and(x, y)) -> not#(not(x)), not#(and(x, y)) -> not#(not(not(y))))
    (not#(and(x, y)) -> not#(not(x)), not#(or(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(not(x)), not#(or(x, y)) -> not#(y))
    (not#(and(x, y)) -> not#(not(x)), not#(or(x, y)) -> not#(not(x)))
    (not#(and(x, y)) -> not#(not(x)), not#(or(x, y)) -> not#(not(y)))
    (not#(and(x, y)) -> not#(not(x)), not#(or(x, y)) -> not#(not(not(x))))
    (not#(and(x, y)) -> not#(not(x)), not#(or(x, y)) -> not#(not(not(y))))
    (not#(and(x, y)) -> not#(not(y)), not#(and(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(not(y)), not#(and(x, y)) -> not#(y))
    (not#(and(x, y)) -> not#(not(y)), not#(and(x, y)) -> not#(not(x)))
    (not#(and(x, y)) -> not#(not(y)), not#(and(x, y)) -> not#(not(y)))
    (not#(and(x, y)) -> not#(not(y)), not#(and(x, y)) -> not#(not(not(x))))
    (not#(and(x, y)) -> not#(not(y)), not#(and(x, y)) -> not#(not(not(y))))
    (not#(and(x, y)) -> not#(not(y)), not#(or(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(not(y)), not#(or(x, y)) -> not#(y))
    (not#(and(x, y)) -> not#(not(y)), not#(or(x, y)) -> not#(not(x)))
    (not#(and(x, y)) -> not#(not(y)), not#(or(x, y)) -> not#(not(y)))
    (not#(and(x, y)) -> not#(not(y)), not#(or(x, y)) -> not#(not(not(x))))
    (not#(and(x, y)) -> not#(not(y)), not#(or(x, y)) -> not#(not(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#(and(x, y)) -> not#(y), not#(and(x, y)) -> not#(not(x)))
    (not#(and(x, y)) -> not#(y), not#(and(x, y)) -> not#(not(y)))
    (not#(and(x, y)) -> not#(y), not#(and(x, y)) -> not#(not(not(x))))
    (not#(and(x, y)) -> not#(y), not#(and(x, y)) -> not#(not(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)) -> not#(not(x)))
    (not#(and(x, y)) -> not#(y), not#(or(x, y)) -> not#(not(y)))
    (not#(and(x, y)) -> not#(y), not#(or(x, y)) -> not#(not(not(x))))
    (not#(and(x, y)) -> not#(y), not#(or(x, y)) -> not#(not(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#(x), not#(and(x, y)) -> not#(not(x)))
    (not#(and(x, y)) -> not#(x), not#(and(x, y)) -> not#(not(y)))
    (not#(and(x, y)) -> not#(x), not#(and(x, y)) -> not#(not(not(x))))
    (not#(and(x, y)) -> not#(x), not#(and(x, y)) -> not#(not(not(y))))
    (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)) -> not#(not(x)))
    (not#(and(x, y)) -> not#(x), not#(or(x, y)) -> not#(not(y)))
    (not#(and(x, y)) -> not#(x), not#(or(x, y)) -> not#(not(not(x))))
    (not#(and(x, y)) -> not#(x), not#(or(x, y)) -> not#(not(not(y))))
    (not#(or(x, y)) -> not#(not(not(x))), not#(and(x, y)) -> not#(x))
    (not#(or(x, y)) -> not#(not(not(x))), not#(and(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(not(not(x))), not#(and(x, y)) -> not#(not(x)))
    (not#(or(x, y)) -> not#(not(not(x))), not#(and(x, y)) -> not#(not(y)))
    (not#(or(x, y)) -> not#(not(not(x))), not#(and(x, y)) -> not#(not(not(x))))
    (not#(or(x, y)) -> not#(not(not(x))), not#(and(x, y)) -> not#(not(not(y))))
    (not#(or(x, y)) -> not#(not(not(x))), not#(or(x, y)) -> not#(x))
    (not#(or(x, y)) -> not#(not(not(x))), not#(or(x, y)) -> not#(y))
    (not#(or(x, y)) -> not#(not(not(x))), not#(or(x, y)) -> not#(not(x)))
    (not#(or(x, y)) -> not#(not(not(x))), not#(or(x, y)) -> not#(not(y)))
    (not#(or(x, y)) -> not#(not(not(x))), not#(or(x, y)) -> not#(not(not(x))))
    (not#(or(x, y)) -> not#(not(not(x))), not#(or(x, y)) -> not#(not(not(y))))
    (not#(and(x, y)) -> not#(not(not(x))), not#(and(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(not(not(x))), not#(and(x, y)) -> not#(y))
    (not#(and(x, y)) -> not#(not(not(x))), not#(and(x, y)) -> not#(not(x)))
    (not#(and(x, y)) -> not#(not(not(x))), not#(and(x, y)) -> not#(not(y)))
    (not#(and(x, y)) -> not#(not(not(x))), not#(and(x, y)) -> not#(not(not(x))))
    (not#(and(x, y)) -> not#(not(not(x))), not#(and(x, y)) -> not#(not(not(y))))
    (not#(and(x, y)) -> not#(not(not(x))), not#(or(x, y)) -> not#(x))
    (not#(and(x, y)) -> not#(not(not(x))), not#(or(x, y)) -> not#(y))
    (not#(and(x, y)) -> not#(not(not(x))), not#(or(x, y)) -> not#(not(x)))
    (not#(and(x, y)) -> not#(not(not(x))), not#(or(x, y)) -> not#(not(y)))
    (not#(and(x, y)) -> not#(not(not(x))), not#(or(x, y)) -> not#(not(not(x))))
    (not#(and(x, y)) -> not#(not(not(x))), not#(or(x, y)) -> not#(not(not(y))))}
   SCCS:
    Scc:
     {not#(and(x, y)) -> not#(x),
      not#(and(x, y)) -> not#(y),
      not#(and(x, y)) -> not#(not(x)),
      not#(and(x, y)) -> not#(not(y)),
      not#(and(x, y)) -> not#(not(not(x))),
      not#(and(x, y)) -> not#(not(not(y))),
       not#(or(x, y)) -> not#(x),
       not#(or(x, y)) -> not#(y),
       not#(or(x, y)) -> not#(not(x)),
       not#(or(x, y)) -> not#(not(y)),
       not#(or(x, y)) -> not#(not(not(x))),
       not#(or(x, y)) -> not#(not(not(y)))}
    SCC:
     Strict:
      {not#(and(x, y)) -> not#(x),
       not#(and(x, y)) -> not#(y),
       not#(and(x, y)) -> not#(not(x)),
       not#(and(x, y)) -> not#(not(y)),
       not#(and(x, y)) -> not#(not(not(x))),
       not#(and(x, y)) -> not#(not(not(y))),
        not#(or(x, y)) -> not#(x),
        not#(or(x, y)) -> not#(y),
        not#(or(x, y)) -> not#(not(x)),
        not#(or(x, y)) -> not#(not(y)),
        not#(or(x, y)) -> not#(not(not(x))),
        not#(or(x, y)) -> not#(not(not(y)))}
     Weak:
     {   not(not(x)) -> x,
      not(and(x, y)) -> or(not(not(not(x))), not(not(not(y)))),
       not(or(x, y)) -> and(not(not(not(x))), not(not(not(y))))}
     POLY:
      Argument Filtering:
       pi(or) = [0,1], pi(and) = [0,1], pi(not#) = [0], pi(not) = 0
      Usable Rules:
       {}
      Interpretation:
       [not#](x0) = x0 + 1,
       [or](x0, x1) = x0 + x1 + 1,
       [and](x0, x1) = x0 + x1 + 1
      Strict:
       {}
      Weak:
       {   not(not(x)) -> x,
        not(and(x, y)) -> or(not(not(not(x))), not(not(not(y)))),
         not(or(x, y)) -> and(not(not(not(x))), not(not(not(y))))}
      Qed