YES
Time: 0.017717
TRS:
 {a b a x -> b a x}
 DP:
  DP:
   {}
  TRS:
  {a b a x -> b a x}
  Qed