YES
(ignored inputs)COMMENT doi:10.1017/CBO9781139172752 [4] Exercise 6.17 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
Input:
   [ or(true,true) -> true,
     or(?x,?y) -> or(?y,?x) ]

Make it flat:
   [ or(true,true) -> true,
     or(?x,?y) -> or(?y,?x) ]
Time: 0.000 [s]

Make it Complete (R^):
   [ or(true,true) = true,
     or(?x,?y) = or(?y,?x) ]
Time: 0.000 [s]

The number of normal forms that must be checked: 3
Time: 0.000 [s]

Now checking all the pairs...

Time to check pairs: 0.000 [s]

The TRS has Uniqueness of Normal Forms.
Total Time: 0.000 [s]

problems/4.trs: Success(UNC)
real 0.02
user 0.01
sys 0.01