As I already said, this system enjoys normalisation and indeed it enjoys strong normalisation. It means that not only any term has a normal form, but also from any term we get a normal form under any reduction sequence.
