UNC Category

The UNC category deals with the unique normal form property with respect to conversion of first-order term rewrite systems. It is a component category of the UN category.

Input

The input is a TRS, specified in basic TRS format. (Note that extra sections, like the SIG section of the extended TRS format, should be ignored.)

Problem

A TRS has the the unique normal form property with respect to conversion (UNC) if any two convertible normal forms are identical. The problem is to determine whether the input TRS is UNC or not.

Problem Selection

See the corresponding section of UN category.

Output Format

The output format should follow the same rules as for the TRS category.

Scoring

The scoring is the same as for the TRS category.