YES
Time: 0.000689
TRS:
 {    implies(x, or(y, z)) -> or(y, implies(x, z)),
         implies(not x, y) -> or(x, y),
  implies(not x, or(y, z)) -> implies(y, or(x, z))}
 RUF:
  Strict:
   {implies(x, or(y, z)) -> or(y, implies(x, z))}
  Weak:
   {}
  DP:
   DP:
    {implies#(x, or(y, z)) -> implies#(x, z)}
   TRS:
   {implies(x, or(y, z)) -> or(y, implies(x, z))}
   EDG:
    {(implies#(x, or(y, z)) -> implies#(x, z), implies#(x, or(y, z)) -> implies#(x, z))}
    SCCS (1):
     Scc:
      {implies#(x, or(y, z)) -> implies#(x, z)}
     SCC (1):
      Strict:
       {implies#(x, or(y, z)) -> implies#(x, z)}
      Weak:
      {implies(x, or(y, z)) -> or(y, implies(x, z))}
      SPSC:
       Simple Projection:
        pi(implies#) = 1
       Strict:
        {}
       Qed