YES
Time: 0.000372
TRS:
 {  d x -> e u x,
  d u x -> c x,
  c u x -> b x,
  b u x -> a e x,
  v e x -> x}
 RUF:
  Strict:
   {c u x -> b x,
    b u x -> a e x}
  Weak:
   {}
  RUF:
   Strict:
    {}
   Weak:
    {}
   Qed