YES
Time: 0.011479
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:
  DP:
   {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}
  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)}
  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# 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# 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# 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# 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# 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# 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 (1):
    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 (12):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [and](x0, x1) = x0 + x1 + 1,
       
       [or](x0, x1) = x0 + x1 + 1,
       
       [not](x0) = x0,
       
       [not#](x0) = x0
      Strict:
       not# or(x, y) -> not# not not y
       1 + 1x + 1y >= 0 + 1y
       not# or(x, y) -> not# not not x
       1 + 1x + 1y >= 0 + 1x
       not# or(x, y) -> not# not y
       1 + 1x + 1y >= 0 + 1y
       not# or(x, y) -> not# not x
       1 + 1x + 1y >= 0 + 1x
       not# or(x, y) -> not# y
       1 + 1x + 1y >= 0 + 1y
       not# or(x, y) -> not# x
       1 + 1x + 1y >= 0 + 1x
       not# and(x, y) -> not# not not y
       1 + 1x + 1y >= 0 + 1y
       not# and(x, y) -> not# not not x
       1 + 1x + 1y >= 0 + 1x
       not# and(x, y) -> not# not y
       1 + 1x + 1y >= 0 + 1y
       not# and(x, y) -> not# not x
       1 + 1x + 1y >= 0 + 1x
       not# and(x, y) -> not# y
       1 + 1x + 1y >= 0 + 1y
       not# and(x, y) -> not# x
       1 + 1x + 1y >= 0 + 1x
      Weak:
       
     Qed