The NFP category deals with the normal form property of first-order term rewrite systems. It is a component category of the UN category.
A TRS has the normal form property (NFP) if any term convertible to a normal form reaches that normal form. The problem is to answer the question whether the input TRS is NFP or not.
See the corresponding section of UN category.
The output format should follow the same rules as for the TRS category.
The scoring is the same as for the TRS category.