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