The UNR category deals with the unique normal form property with respect to reduction of first-order term rewrite systems. It is a component category of UN category.
A TRS has the unique normal form property with respect to reduction (UNR) if from any term we can reach at most one normal form. The problem is to answer the question whether the input TRS is UNR or not.
Problem SelectionSee the corresponding section of UN category.
The output format should follow the same rule as that of the TRS category.
The scoring is the same as for the TRS category.