YES
Time: 0.008142
TRS:
 {     or(x, x) -> x,
      and(x, x) -> x,
   not or(x, y) -> and(not x, not y),
  not and(x, y) -> or(not x, not y),
      not not x -> x}
 DP:
  DP:
   { not# or(x, y) -> and#(not x, not y),
     not# or(x, y) -> not# x,
     not# or(x, y) -> not# y,
    not# and(x, y) -> or#(not x, not y),
    not# and(x, y) -> not# x,
    not# and(x, y) -> not# y}
  TRS:
  {     or(x, x) -> x,
       and(x, x) -> x,
    not or(x, y) -> and(not x, not y),
   not and(x, y) -> or(not x, not y),
       not not x -> x}
  EDG:
   {(not# and(x, y) -> not# y, not# and(x, y) -> not# y)
    (not# and(x, y) -> not# y, not# and(x, y) -> not# x)
    (not# and(x, y) -> not# y, not# and(x, y) -> or#(not x, not y))
    (not# and(x, y) -> not# y, not# or(x, y) -> not# y)
    (not# and(x, y) -> not# y, not# or(x, y) -> not# x)
    (not# and(x, y) -> not# y, not# or(x, y) -> and#(not x, not y))
    (not# and(x, y) -> not# x, not# and(x, y) -> not# y)
    (not# and(x, y) -> not# x, not# and(x, y) -> not# x)
    (not# and(x, y) -> not# x, not# and(x, y) -> or#(not x, not y))
    (not# and(x, y) -> not# x, not# or(x, y) -> not# y)
    (not# and(x, y) -> not# x, not# or(x, y) -> not# x)
    (not# and(x, y) -> not# x, not# or(x, y) -> and#(not x, not y))
    (not# or(x, y) -> not# x, not# or(x, y) -> and#(not x, not y))
    (not# or(x, y) -> not# x, not# or(x, y) -> not# x)
    (not# or(x, y) -> not# x, not# or(x, y) -> not# y)
    (not# or(x, y) -> not# x, not# and(x, y) -> or#(not x, not y))
    (not# or(x, y) -> not# x, not# and(x, y) -> not# x)
    (not# or(x, y) -> not# x, not# and(x, y) -> not# y)
    (not# or(x, y) -> not# y, not# or(x, y) -> and#(not x, not y))
    (not# or(x, y) -> not# y, not# or(x, y) -> not# x)
    (not# or(x, y) -> not# y, not# or(x, y) -> not# y)
    (not# or(x, y) -> not# y, not# and(x, y) -> or#(not x, not y))
    (not# or(x, y) -> not# y, not# and(x, y) -> not# x)
    (not# or(x, y) -> not# y, not# and(x, y) -> not# y)}
   STATUS:
    arrows: 0.333333
    SCCS (1):
     Scc:
      { not# or(x, y) -> not# x,
        not# or(x, y) -> not# y,
       not# and(x, y) -> not# x,
       not# and(x, y) -> not# y}
     
     SCC (4):
      Strict:
       { not# or(x, y) -> not# x,
         not# or(x, y) -> not# y,
        not# and(x, y) -> not# x,
        not# and(x, y) -> not# y}
      Weak:
      {     or(x, x) -> x,
           and(x, x) -> x,
        not or(x, y) -> and(not x, not y),
       not and(x, y) -> or(not x, not y),
           not not x -> x}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [or](x0, x1) = x0 + x1 + 1,
        
        [and](x0, x1) = x0 + x1 + 1,
        
        [not](x0) = 0,
        
        [not#](x0) = x0
       Strict:
        not# and(x, y) -> not# y
        1 + 1x + 1y >= 0 + 1y
        not# and(x, y) -> 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
       Weak:
        not not x -> x
        0 + 0x >= 1x
        not and(x, y) -> or(not x, not y)
        0 + 0x + 0y >= 1 + 0x + 0y
        not or(x, y) -> and(not x, not y)
        0 + 0x + 0y >= 1 + 0x + 0y
        and(x, x) -> x
        1 + 2x >= 1x
        or(x, x) -> x
        1 + 2x >= 1x
      Qed