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