YES
Time: 0.002056
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)}
   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}
     SPSC:
      Simple Projection:
       pi(not#) = 0
      Strict:
       { not# or(x, y) -> not# x,
         not# or(x, y) -> not# y,
        not# and(x, y) -> not# y}
      EDG:
       {(not# and(x, y) -> not# y, not# and(x, y) -> 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# 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) -> 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) -> not# y)}
       SCCS (1):
        Scc:
         { not# or(x, y) -> not# x,
           not# or(x, y) -> not# y,
          not# and(x, y) -> not# y}
        SCC (3):
         Strict:
          { not# or(x, y) -> not# x,
            not# or(x, y) -> not# y,
           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}
         SPSC:
          Simple Projection:
           pi(not#) = 0
          Strict:
           { not# or(x, y) -> not# x,
            not# and(x, y) -> not# y}
          EDG:
           {(not# or(x, y) -> not# x, not# and(x, y) -> not# y)
            (not# or(x, y) -> 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# y, not# and(x, y) -> not# y)}
           SCCS (1):
            Scc:
             { not# or(x, y) -> not# x,
              not# and(x, y) -> not# y}
            SCC (2):
             Strict:
              { not# or(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}
             SPSC:
              Simple Projection:
               pi(not#) = 0
              Strict:
               {not# and(x, y) -> not# y}
              EDG:
               {(not# and(x, y) -> not# y, not# and(x, y) -> not# y)}
               SCCS (1):
                Scc:
                 {not# and(x, y) -> not# y}
                SCC (1):
                 Strict:
                  {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}
                 SPSC:
                  Simple Projection:
                   pi(not#) = 0
                  Strict:
                   {}
                  Qed