Categories – UNR
The UNR category is concerned with the "unique normal forms with respect to reduction" property (UNR) of firstorder rewrite systems.
Format
The input is a firstorder rewrite system without conditions, specified in the ARI TRS format. The question to be answered is whether the rewrite system has the property that no term rewrites to different normal forms.
Examples

(format TRS) (fun a 0) (fun c 0) (fun f 1) (fun h 2) (rule a (h (f a) c)) (rule a (f c))
The correct answer isNO
. 
(format TRS) (fun a 0) (fun b 0) (fun f 2) (fun g 1) (rule (f a a) (g (f a a))) (rule a b) (rule (f b x) (g (f x x))) (rule (f x b) (g (f x x)))
The correct answer isYES
.
Problem Selection
Problems are selected from those in the ARI database with the 'trs' tag. Problems that were shown confluent by at least one participating tool in the CoCo 2023 full run are not considered.