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