YES Time: 0.000390 TRS: {a a x -> a b a x} DP: DP: {a# a x -> a# b a x} TRS: {a a x -> a b a x} EDG: {} SCCS (0): Qed