YES
Time: 0.002002
TRS:
 {               or(x, x) -> x,
          or(x, or(y, y)) -> or(x, y),
         or(x, and(x, y)) -> x,
           or(x, false()) -> x,
  or(or(x, y), and(y, z)) -> or(x, y),
            or(true(), y) -> true(),
                and(x, x) -> x,
         and(x, or(y, z)) -> or(and(x, y), and(x, z)),
        and(x, and(y, y)) -> and(x, y),
           and(x, true()) -> x,
          and(false(), y) -> false()}
 DP:
  DP:
   {  or#(x, or(y, y)) -> or#(x, y),
     and#(x, or(y, z)) -> or#(and(x, y), and(x, z)),
     and#(x, or(y, z)) -> and#(x, y),
     and#(x, or(y, z)) -> and#(x, z),
    and#(x, and(y, y)) -> and#(x, y)}
  TRS:
  {               or(x, x) -> x,
           or(x, or(y, y)) -> or(x, y),
          or(x, and(x, y)) -> x,
            or(x, false()) -> x,
   or(or(x, y), and(y, z)) -> or(x, y),
             or(true(), y) -> true(),
                 and(x, x) -> x,
          and(x, or(y, z)) -> or(and(x, y), and(x, z)),
         and(x, and(y, y)) -> and(x, y),
            and(x, true()) -> x,
           and(false(), y) -> false()}
  EDG:
   {(and#(x, or(y, z)) -> and#(x, y), and#(x, and(y, y)) -> and#(x, y))
    (and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, z))
    (and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, y))
    (and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> or#(and(x, y), and(x, z)))
    (and#(x, or(y, z)) -> or#(and(x, y), and(x, z)), or#(x, or(y, y)) -> or#(x, y))
    (and#(x, or(y, z)) -> and#(x, z), and#(x, or(y, z)) -> or#(and(x, y), and(x, z)))
    (and#(x, or(y, z)) -> and#(x, z), and#(x, or(y, z)) -> and#(x, y))
    (and#(x, or(y, z)) -> and#(x, z), and#(x, or(y, z)) -> and#(x, z))
    (and#(x, or(y, z)) -> and#(x, z), and#(x, and(y, y)) -> and#(x, y))
    (and#(x, and(y, y)) -> and#(x, y), and#(x, or(y, z)) -> or#(and(x, y), and(x, z)))
    (and#(x, and(y, y)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, y))
    (and#(x, and(y, y)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, z))
    (and#(x, and(y, y)) -> and#(x, y), and#(x, and(y, y)) -> and#(x, y))
    (or#(x, or(y, y)) -> or#(x, y), or#(x, or(y, y)) -> or#(x, y))}
   SCCS (2):
    Scc:
     { and#(x, or(y, z)) -> and#(x, y),
       and#(x, or(y, z)) -> and#(x, z),
      and#(x, and(y, y)) -> and#(x, y)}
    Scc:
     {or#(x, or(y, y)) -> or#(x, y)}
    SCC (3):
     Strict:
      { and#(x, or(y, z)) -> and#(x, y),
        and#(x, or(y, z)) -> and#(x, z),
       and#(x, and(y, y)) -> and#(x, y)}
     Weak:
     {               or(x, x) -> x,
              or(x, or(y, y)) -> or(x, y),
             or(x, and(x, y)) -> x,
               or(x, false()) -> x,
      or(or(x, y), and(y, z)) -> or(x, y),
                or(true(), y) -> true(),
                    and(x, x) -> x,
             and(x, or(y, z)) -> or(and(x, y), and(x, z)),
            and(x, and(y, y)) -> and(x, y),
               and(x, true()) -> x,
              and(false(), y) -> false()}
     SPSC:
      Simple Projection:
       pi(and#) = 1
      Strict:
       {and#(x, or(y, z)) -> and#(x, y),
        and#(x, or(y, z)) -> and#(x, z)}
      EDG:
       {(and#(x, or(y, z)) -> and#(x, z), and#(x, or(y, z)) -> and#(x, z))
        (and#(x, or(y, z)) -> and#(x, z), and#(x, or(y, z)) -> and#(x, y))
        (and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, y))
        (and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, z))}
       SCCS (1):
        Scc:
         {and#(x, or(y, z)) -> and#(x, y),
          and#(x, or(y, z)) -> and#(x, z)}
        SCC (2):
         Strict:
          {and#(x, or(y, z)) -> and#(x, y),
           and#(x, or(y, z)) -> and#(x, z)}
         Weak:
         {               or(x, x) -> x,
                  or(x, or(y, y)) -> or(x, y),
                 or(x, and(x, y)) -> x,
                   or(x, false()) -> x,
          or(or(x, y), and(y, z)) -> or(x, y),
                    or(true(), y) -> true(),
                        and(x, x) -> x,
                 and(x, or(y, z)) -> or(and(x, y), and(x, z)),
                and(x, and(y, y)) -> and(x, y),
                   and(x, true()) -> x,
                  and(false(), y) -> false()}
         SPSC:
          Simple Projection:
           pi(and#) = 1
          Strict:
           {and#(x, or(y, z)) -> and#(x, y)}
          EDG:
           {(and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, y))}
           SCCS (1):
            Scc:
             {and#(x, or(y, z)) -> and#(x, y)}
            SCC (1):
             Strict:
              {and#(x, or(y, z)) -> and#(x, y)}
             Weak:
             {               or(x, x) -> x,
                      or(x, or(y, y)) -> or(x, y),
                     or(x, and(x, y)) -> x,
                       or(x, false()) -> x,
              or(or(x, y), and(y, z)) -> or(x, y),
                        or(true(), y) -> true(),
                            and(x, x) -> x,
                     and(x, or(y, z)) -> or(and(x, y), and(x, z)),
                    and(x, and(y, y)) -> and(x, y),
                       and(x, true()) -> x,
                      and(false(), y) -> false()}
             SPSC:
              Simple Projection:
               pi(and#) = 1
              Strict:
               {}
              Qed
    SCC (1):
     Strict:
      {or#(x, or(y, y)) -> or#(x, y)}
     Weak:
     {               or(x, x) -> x,
              or(x, or(y, y)) -> or(x, y),
             or(x, and(x, y)) -> x,
               or(x, false()) -> x,
      or(or(x, y), and(y, z)) -> or(x, y),
                or(true(), y) -> true(),
                    and(x, x) -> x,
             and(x, or(y, z)) -> or(and(x, y), and(x, z)),
            and(x, and(y, y)) -> and(x, y),
               and(x, true()) -> x,
              and(false(), y) -> false()}
     SPSC:
      Simple Projection:
       pi(or#) = 1
      Strict:
       {}
      Qed